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/radar/normalized-10:20:4.5:0.95:100.opb |
| MD5SUM | f82b685b64af240616b701a750c82883 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 10 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 934 |
| Biggest coefficient in the objective function | 546 |
| Number of bits for the biggest coefficient in the objective function | 10 |
| Sum of the numbers in the objective function | 2594 |
| Number of bits of the sum of numbers in the objective function | 12 |
| Biggest number in a constraint | 546 |
| Number of bits of the biggest number in a constraint | 10 |
| Biggest sum of numbers in a constraint | 2594 |
| Number of bits of the biggest sum of numbers | 12 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1.03784 |
| Number of variables | 934 |
| Total number of constraints | 1996 |
| Number of constraints which are clauses | 879 |
| Number of constraints which are cardinality constraints (but not clauses) | 1117 |
| Number of constraints which are nor clauses,nor cardinality constraints | 0 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 20 |
Trace number 33842
#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-27 16:53:17 (client local time)
PB2005-SCRIPT v4.0
MARKUPS: idlaunch=3302 boxname=wulflinc24 idbench=367 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH: f82b685b64af240616b701a750c82883 /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:100.opb 0
IDLAUNCH: 3302
/proc/cpuinfo:
processor : 0
vendor_id : GenuineIntel
cpu family : 6
model : 7
model name : Pentium III (Katmai)
stepping : 3
cpu MHz : 451.080
cache size : 512 KB
fdiv_bug : no
hlt_bug : no
f00f_bug : no
coma_bug : no
fpu : yes
fpu_exception : yes
cpuid level : 2
wp : yes
flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips : 890.88
processor : 1
vendor_id : GenuineIntel
cpu family : 6
model : 7
model name : Pentium III (Katmai)
stepping : 3
cpu MHz : 451.080
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: 726632 kB
Buffers: 28392 kB
Cached: 258200 kB
SwapCached: 640 kB
Active: 40324 kB
Inactive: 248356 kB
HighTotal: 131008 kB
HighFree: 252 kB
LowTotal: 903652 kB
LowFree: 726380 kB
SwapTotal: 2097892 kB
SwapFree: 2096352 kB
Dirty: 96 kB
Writeback: 0 kB
Mapped: 5120 kB
Slab: 13568 kB
Committed_AS: 63604 kB
PageTables: 316 kB
VmallocTotal: 114680 kB
VmallocUsed: 1368 kB
VmallocChunk: 113252 kB
JOB ENDED THE 2005-05-27 17:13:48 (client local time) WITH STATUS 10 IN 1230.29 SECONDS
stats: 3302 0 1230.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 0 (#equs: 0)
Nr of vars set: 0 (#equs: 0)
#decisions: 364; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1585 (1008:>=*);
#decisions: 356; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1586 (1007:>=*);
#decisions: 355; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1587 (1006:>=*);
#decisions: 421; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1589 (1004:>=*);
#decisions: 354; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1590 (1003:>=*);
#decisions: 418; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1592 (1001:>=*);
#decisions: 347; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1593 (1000:>=*);
#decisions: 346; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1594 (999:>=*);
#decisions: 345; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1595 (998:>=*);
#decisions: 342; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1596 (997:>=*);
#decisions: 340; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1597 (996:>=*);
#decisions: 339; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1598 (995:>=*);
#decisions: 338; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1599 (994:>=*);
#decisions: 411; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1601 (992:>=*);
#decisions: 337; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1602 (991:>=*);
#decisions: 338; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1603 (990:>=*);
#decisions: 337; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1604 (989:>=*);
#decisions: 336; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1605 (988:>=*);
#decisions: 335; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1606 (987:>=*);
#decisions: 334; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1607 (986:>=*);
#decisions: 331; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1608 (985:>=*);
#decisions: 330; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1609 (984:>=*);
#decisions: 331; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1610 (983:>=*);
#decisions: 330; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1611 (982:>=*);
#decisions: 329; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1612 (981:>=*);
#decisions: 329; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1613 (980:>=*);
#decisions: 326; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1614 (979:>=*);
#decisions: 325; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1615 (978:>=*);
#decisions: 324; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1616 (977:>=*);
#decisions: 323; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1617 (976:>=*);
#decisions: 322; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1618 (975:>=*);
#decisions: 321; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1619 (974:>=*);
#decisions: 322; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1620 (973:>=*);
#decisions: 319; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1621 (972:>=*);
#decisions: 319; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1622 (971:>=*);
#decisions: 315; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1623 (970:>=*);
#decisions: 314; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1624 (969:>=*);
#decisions: 388; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1626 (967:>=*);
#decisions: 309; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1627 (966:>=*);
#decisions: 307; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1628 (965:>=*);
#decisions: 308; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1629 (964:>=*);
#decisions: 306; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1630 (963:>=*);
#decisions: 305; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1631 (962:>=*);
#decisions: 304; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1632 (961:>=*);
#decisions: 302; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1633 (960:>=*);
#decisions: 299; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1634 (959:>=*);
#decisions: 298; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1635 (958:>=*);
#decisions: 297; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1636 (957:>=*);
#decisions: 295; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1637 (956:>=*);
#decisions: 296; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1638 (955:>=*);
#decisions: 291; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1639 (954:>=*);
#decisions: 287; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1640 (953:>=*);
#decisions: 284; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1641 (952:>=*);
#decisions: 283; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1642 (951:>=*);
#decisions: 282; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1643 (950:>=*);
#decisions: 281; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1644 (949:>=*);
#decisions: 282; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1645 (948:>=*);
#decisions: 280; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1646 (947:>=*);
#decisions: 279; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1647 (946:>=*);
#decisions: 280; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1648 (945:>=*);
#decisions: 279; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1649 (944:>=*);
#decisions: 277; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1650 (943:>=*);
#decisions: 276; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1651 (942:>=*);
#decisions: 273; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1652 (941:>=*);
#decisions: 270; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1653 (940:>=*);
#decisions: 271; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1654 (939:>=*);
#decisions: 268; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1655 (938:>=*);
#decisions: 266; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1656 (937:>=*);
#decisions: 264; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1657 (936:>=*);
#decisions: 259; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1658 (935:>=*);
#decisions: 258; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1659 (934:>=*);
#decisions: 261; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1660 (933:>=*);
#decisions: 258; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1661 (932:>=*);
#decisions: 257; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1662 (931:>=*);
#decisions: 257; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1663 (930:>=*);
#decisions: 252; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1664 (929:>=*);
#decisions: 249; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1665 (928:>=*);
#decisions: 247; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1666 (927:>=*);
#decisions: 246; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1667 (926:>=*);
#decisions: 245; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1668 (925:>=*);
#decisions: 244; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1669 (924:>=*);
#decisions: 245; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1670 (923:>=*);
#decisions: 244; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1671 (922:>=*);
#decisions: 243; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1672 (921:>=*);
#decisions: 243; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1673 (920:>=*);
#decisions: 240; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1674 (919:>=*);
#decisions: 239; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1675 (918:>=*);
#decisions: 237; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1676 (917:>=*);
#decisions: 236; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1677 (916:>=*);
#decisions: 237; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1678 (915:>=*);
#decisions: 236; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1679 (914:>=*);
#decisions: 235; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1680 (913:>=*);
#decisions: 236; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1681 (912:>=*);
#decisions: 234; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1682 (911:>=*);
#decisions: 233; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1683 (910:>=*);
#decisions: 238; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1684 (909:>=*);
#decisions: 233; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1685 (908:>=*);
#decisions: 232; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1686 (907:>=*);
#decisions: 235; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1687 (906:>=*);
#decisions: 232; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1688 (905:>=*);
#decisions: 230; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1689 (904:>=*);
#decisions: 230; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1690 (903:>=*);
#decisions: 228; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1691 (902:>=*);
#decisions: 227; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1692 (901:>=*);
#decisions: 227; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1693 (900:>=*);
#decisions: 226; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1694 (899:>=*);
#decisions: 225; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1695 (898:>=*);
#decisions: 224; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1696 (897:>=*);
#decisions: 226; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1697 (896:>=*);
#decisions: 224; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1698 (895:>=*);
#decisions: 223; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1699 (894:>=*);
#decisions: 221; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1700 (893:>=*);
#decisions: 218; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1701 (892:>=*);
#decisions: 216; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1702 (891:>=*);
#decisions: 215; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1703 (890:>=*);
#decisions: 215; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1704 (889:>=*);
#decisions: 213; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1705 (888:>=*);
#decisions: 212; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1706 (887:>=*);
#decisions: 213; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1707 (886:>=*);
#decisions: 211; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1708 (885:>=*);
#decisions: 219; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1709 (884:>=*);
#decisions: 211; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1710 (883:>=*);
#decisions: 209; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1711 (882:>=*);
#decisions: 208; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1712 (881:>=*);
#decisions: 205; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1713 (880:>=*);
#decisions: 204; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1714 (879:>=*);
#decisions: 203; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1715 (878:>=*);
#decisions: 207; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1716 (877:>=*);
#decisions: 203; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1717 (876:>=*);
#decisions: 202; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1718 (875:>=*);
#decisions: 202; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1719 (874:>=*);
#decisions: 200; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1720 (873:>=*);
#decisions: 199; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1721 (872:>=*);
#decisions: 198; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1722 (871:>=*);
#decisions: 200; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1723 (870:>=*);
#decisions: 198; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1724 (869:>=*);
#decisions: 197; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1725 (868:>=*);
#decisions: 197; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1726 (867:>=*);
#decisions: 196; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1727 (866:>=*);
#decisions: 195; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1728 (865:>=*);
#decisions: 195; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1729 (864:>=*);
#decisions: 194; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1730 (863:>=*);
#decisions: 194; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1731 (862:>=*);
#decisions: 193; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1732 (861:>=*);
#decisions: 196; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1733 (860:>=*);
#decisions: 191; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1734 (859:>=*);
#decisions: 189; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1735 (858:>=*);
#decisions: 187; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1736 (857:>=*);
#decisions: 194; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1737 (856:>=*);
#decisions: 188; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1738 (855:>=*);
#decisions: 186; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1739 (854:>=*);
#decisions: 189; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1740 (853:>=*);
#decisions: 184; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1741 (852:>=*);
#decisions: 183; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1742 (851:>=*);
#decisions: 182; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1743 (850:>=*);
#decisions: 184; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1744 (849:>=*);
#decisions: 182; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1745 (848:>=*);
#decisions: 181; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1746 (847:>=*);
#decisions: 181; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1747 (846:>=*);
#decisions: 178; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1748 (845:>=*);
#decisions: 177; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1749 (844:>=*);
#decisions: 176; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1750 (843:>=*);
#decisions: 177; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1751 (842:>=*);
#decisions: 175; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1752 (841:>=*);
#decisions: 172; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1753 (840:>=*);
#decisions: 171; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1754 (839:>=*);
#decisions: 177; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1755 (838:>=*);
#decisions: 171; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1756 (837:>=*);
#decisions: 170; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1757 (836:>=*);
#decisions: 174; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1758 (835:>=*);
#decisions: 170; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1759 (834:>=*);
#decisions: 168; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1760 (833:>=*);
#decisions: 169; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1761 (832:>=*);
#decisions: 165; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1762 (831:>=*);
#decisions: 164; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1763 (830:>=*);
#decisions: 164; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1764 (829:>=*);
#decisions: 162; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1765 (828:>=*);
#decisions: 159; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1766 (827:>=*);
#decisions: 158; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1767 (826:>=*);
#decisions: 156; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1768 (825:>=*);
#decisions: 154; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1769 (824:>=*);
#decisions: 154; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1770 (823:>=*);
#decisions: 152; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1771 (822:>=*);
#decisions: 151; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1772 (821:>=*);
#decisions: 151; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1773 (820:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1774 (819:>=*);
#decisions: 148; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1775 (818:>=*);
#decisions: 153; #end-nodes: 5;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 5 / 80 (80)
#axs: 1063, #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: 1776 (817:>=*);
#decisions: 149; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1063, #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: 1777 (816:>=*);
#decisions: 155; #end-nodes: 5;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 5 / 80 (80)
#axs: 1063, #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: 1778 (815:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1779 (814:>=*);
#decisions: 148; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1780 (813:>=*);
#decisions: 150; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1063, #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: 1781 (812:>=*);
#decisions: 155; #end-nodes: 7;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 7 / 80 (80)
#axs: 1063, #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: 1782 (811:>=*);
#decisions: 164; #end-nodes: 16;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 16 / 80 (80)
#axs: 1063, #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: 1783 (810:>=*);
#decisions: 212; #end-nodes: 60;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 60 / 80 (80)
#axs: 1063, #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: 1784 (809:>=*);
#decisions: 150; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1785 (808:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1786 (807:>=*);
#decisions: 151; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1063, #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: 1787 (806:>=*);
#decisions: 165; #end-nodes: 17;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 17 / 80 (80)
#axs: 1063, #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: 1788 (805:>=*);
#decisions: 217; #end-nodes: 69;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 69 / 80 (80)
#axs: 1063, #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: 1789 (804:>=*);
#decisions: 201; #end-nodes: 53;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 53 / 80 (80)
#axs: 1063, #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: 1790 (803:>=*);
#decisions: 6010; #end-nodes: 2168;
#proof improvement attempts: 0; #restarts: 26
Current batch, end-nodes: 4 / 86 (86)
#axs: 1063, #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: 1791 (802:>=*);
#decisions: 154; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1063, #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: 1792 (801:>=*);
#decisions: 203; #end-nodes: 51;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 51 / 80 (80)
#axs: 1063, #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: 1793 (800:>=*);
#decisions: 153; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1063, #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: 1794 (799:>=*);
#decisions: 7397; #end-nodes: 2694;
#proof improvement attempts: 0; #restarts: 32
Current batch, end-nodes: 11 / 88 (88)
#axs: 1063, #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: 1795 (798:>=*);
#decisions: 179; #end-nodes: 28;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 28 / 80 (80)
#axs: 1063, #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: 1796 (797:>=*);
#decisions: 150; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1797 (796:>=*);
#decisions: 10938; #end-nodes: 4026;
#proof improvement attempts: 0; #restarts: 47
Current batch, end-nodes: 1 / 91 (91)
#axs: 1063, #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: 1798 (795:>=*);
#decisions: 147; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1799 (794:>=*);
#decisions: 151; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 1063, #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: 1800 (793:>=*);
#decisions: 146; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1801 (792:>=*);
#decisions: 159; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 1063, #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: 1802 (791:>=*);
#decisions: 148; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1803 (790:>=*);
#decisions: 147; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1804 (789:>=*);
#decisions: 155; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1063, #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: 1805 (788:>=*);
#decisions: 147; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1806 (787:>=*);
#decisions: 22190; #end-nodes: 8707;
#proof improvement attempts: 0; #restarts: 95
Current batch, end-nodes: 1 / 103 (103)
#axs: 1063, #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: 1807 (786:>=*);
#decisions: 155; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1808 (785:>=*);
#decisions: 154; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1809 (784:>=*);
#decisions: 155; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1063, #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: 1810 (783:>=*);
#decisions: 160; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 1063, #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: 1811 (782:>=*);
#decisions: 160; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 1063, #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: 1812 (781:>=*);
#decisions: 159; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 1063, #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: 1813 (780:>=*);
#decisions: 165; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 1063, #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: 1814 (779:>=*);
#decisions: 158; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1815 (778:>=*);
#decisions: 156; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1816 (777:>=*);
#decisions: 155; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1817 (776:>=*);
#decisions: 155; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1818 (775:>=*);
#decisions: 154; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1819 (774:>=*);
#decisions: 153; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1820 (773:>=*);
#decisions: 160; #end-nodes: 7;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 7 / 80 (80)
#axs: 1063, #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: 1821 (772:>=*);
#decisions: 170; #end-nodes: 15;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 15 / 80 (80)
#axs: 1063, #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: 1822 (771:>=*);
#decisions: 154; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1823 (770:>=*);
#decisions: 225; #end-nodes: 71;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 71 / 80 (80)
#axs: 1063, #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: 1824 (769:>=*);
#decisions: 174; #end-nodes: 22;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 22 / 80 (80)
#axs: 1063, #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: 1825 (768:>=*);
#decisions: 17687; #end-nodes: 6986;
#proof improvement attempts: 0; #restarts: 78
Current batch, end-nodes: 1 / 99 (99)
#axs: 1063, #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: 1826 (767:>=*);
#decisions: 210; #end-nodes: 57;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 57 / 80 (80)
#axs: 1063, #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: 1827 (766:>=*);
#decisions: 230; #end-nodes: 76;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 76 / 80 (80)
#axs: 1063, #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: 1828 (765:>=*);
#decisions: 239; #end-nodes: 79;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 79 / 80 (80)
#axs: 1063, #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: 1829 (764:>=*);
#decisions: 155; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1830 (763:>=*);
#decisions: 154; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1831 (762:>=*);
#decisions: 1966196; #end-nodes: 1534046;
#proof improvement attempts: 0; #restarts: 3198
Current batch, end-nodes: 317 / 879 (879)
#axs: 1063, #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: 1832 (761:>=*);
#decisions: 150249; #end-nodes: 78069;
#proof improvement attempts: 0; #restarts: 533
Current batch, end-nodes: 0 / 213 (213)
#axs: 1063, #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: 1833 (760:>=*);
#decisions: 152; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1834 (759:>=*);
#decisions: 151; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1835 (758:>=*);
#decisions: 150; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1836 (757:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1837 (756:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1838 (755:>=*);
#decisions: 180; #end-nodes: 31;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 31 / 80 (80)
#axs: 1063, #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: 1839 (754:>=*);
#decisions: 202; #end-nodes: 52;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 52 / 80 (80)
#axs: 1063, #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: 1840 (753:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1063, #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: 1841 (752:>=*);
#decisions: 752964; #end-nodes: 520057;
#proof improvement attempts: 0; #restarts: 1745
Current batch, end-nodes: 124 / 516 (516)
#axs: 1063, #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: 1842 (751:>=*);
Interupt request received.
#decisions: 18107; #end-nodes: 7280;
#proof improvement attempts: 0; #restarts: 81
Current batch, end-nodes: 0 / 100 (100)
#axs: 1063, #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:) 1842 (751:>=*)
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: 165 (#equs: 0)
Time taken: 20 min, 29 sec
times:
0m0.017s 0m0.006s
20m1.809s 0m28.031s
v -v853 v782 -v197 -v102 v21 v2 -v855 -v103 v1 -v785 -v384 -v272 v196 v20 v3 -v856 -v786 -v76 v55 -v23 v4 -v383 -v275 v202 -v75 v54 v11 -v763 v387 -v276 v200 v56 -v24 -v5 -v762 -v247 -v150 -v77 v57 v26 -v6 -v764 -v613 -v388 v201 -v79 v58 -v39 v27 -v7 v765 -v612 -v513 -v250 -v205 v149 v65 -v38 v766 v618 -v251 -v80 -v59 -v40 v773 v617 -v512 -v326 v155 -v125 v82 -v60 -v41 v767 -v619 v153 -v83 -v61 v42 v768 v623 -v593 -v573 -v518 -v128 -v49 v769 v622 -v577 -v516 -v154 -v129 v43 -v729 v620 -v596 v576 -v158 v44 v621 -v597 -v517 v45 v881 v728 -v521 -v852 v781 -v192 v104 -v17 -v857 -v787 v537 -v468 v271 v198 v22 v14 -v541 -v71 -v25 v15 v859 -v385 -v277 v203 -v108 -v70 v29 v10 -v860 v389 v28 -v790 -v246 -v206 -v145 -v78 -v68 v8 -v204 -v81 -v69 -v811 -v776 -v638 -v508 -v391 -v322 v280 -v252 v151 v85 v64 -v777 -v642 -v614 -v392 v84 v772 -v615 -v514 -v325 v156 -v124 v62 v52 v616 v53 v770 v627 v592 -v519 -v255 -v159 -v130 -v48 -v572 -v157 -v877 -v598 -v574 v522 -v46 v578 -v520 v880 v730 -v133 -v601 -v854 v783 -v464 v267 v105 -v13 -v858 v379 -v191 -v16 v12 v862 -v788 v536 v488 -v467 v378 v273 -v193 -v109 -v18 v861 -v540 -v492 v199 -v107 v19 -v791 -v386 -v278 v242 v195 -v67 -v33 -v789 v390 -v207 v72 -v66 -v807 -v775 -v394 -v301 v281 -v248 v73 v9 -v774 -v393 v279 -v144 v74 -v810 -v637 v321 -v253 -v146 -v120 -v89 -v51 -v641 v507 v152 -v50 v630 -v588 v509 -v327 -v256 v148 -v126 v63 v631 -v515 -v254 -v160 v771 -v626 v594 v511 -v131 -v725 v523 -v876 -v724 v709 -v624 -v599 v330 -v134 -v47 v575 -v132 v882 v731 -v602 v586 -v600 v582 -v900 -v732 v581 -v904 -v733 -v851 v779 -v463 -v422 v106 v850 v784 -v426 v266 -v110 -v866 v780 -v662 v538 v487 -v469 v268 -v177 v36 -v792 -v666 -v542 v491 v380 v274 -v194 v37 v381 -v297 v270 -v222 -v215 -v32 v382 v282 v241 -v226 v211 -v806 -v544 -v472 -v398 -v317 -v300 v243 v210 -v92 -v30 -v545 -v249 -v93 -v812 -v639 v629 v323 v245 -v88 v643 v628 -v257 -v147 -v119 -v913 -v836 -v328 v168 -v121 -v86 -v917 v587 v510 v164 -v127 v872 -v815 -v705 -v645 v589 -v531 -v347 v331 v163 v123 -v646 v595 v527 -v351 v329 v135 -v878 v708 -v625 v591 -v583 v526 -v726 -v603 v585 v95 v883 -v727 v94 -v899 v884 v737 v579 -v903 v885 -v869 v533 -v465 -v421 -v173 -v118 v35 -v870 v778 -v425 -v114 v34 -v865 v800 -v661 v539 v489 -v470 -v212 -v176 -v113 v796 v665 -v543 v493 v269 -v214 -v863 -v802 v795 -v547 -v473 -v450 -v401 -v296 v290 -v221 -v91 -v633 -v546 -v471 -v402 v286 v225 -v90 -v808 -v632 v495 -v397 -v302 v285 v208 -v31 v496 -v316 v244 -v832 -v813 -v752 -v640 -v395 -v318 -v265 v209 v165 v644 v324 v261 v167 -v912 -v835 -v816 -v648 -v528 v320 -v305 v260 -v87 -v916 -v814 -v647 -v530 v332 -v122 -v704 -v346 -v161 v143 v871 v590 -v584 -v350 v139 v873 v710 -v611 v524 -v162 v138 -v879 v607 v875 -v740 v606 -v561 -v525 v886 -v741 -v565 v96 -v901 v736 -v713 -v580 v97 -v905 -v867 -v797 v484 -v461 -v423 -v172 -v117 v799 v532 -v466 -v427 -v213 -v663 v534 v490 v462 -v446 -v400 -v292 v287 -v178 -v111 v667 v535 v494 -v474 -v399 v289 -v864 v793 -v551 v498 -v449 -v429 -v298 -v223 -v112 -v801 v497 -v430 v227 -v803 v794 -v748 -v687 -v669 -v303 v283 -v262 -v181 -v809 -v691 -v670 -v634 -v264 -v166 -v831 v805 -v751 -v635 -v396 v306 -v284 v229 -v817 v636 -v529 -v319 v304 -v230 -v914 v837 -v700 v652 -v340 v258 v140 -v918 -v336 v142 -v706 -v608 -v348 -v335 v259 -v610 -v352 -v920 -v840 -v739 v711 v412 -v371 -v136 -v921 -v896 v874 -v738 -v375 -v895 -v894 v714 v604 -v560 v354 -v137 v890 v712 -v564 -v355 -v902 v889 v734 v605 v100 v906 v101 -v868 -v798 v658 -v424 -v174 -v115 v483 v460 -v428 v288 -v217 -v664 v554 v485 -v482 -v445 v432 -v216 -v179 v668 v555 v486 v478 -v431 -v291 -v672 -v550 v502 v477 -v451 -v293 -v224 -v182 -v671 -v299 -v263 v228 -v180 -v827 -v747 -v686 -v548 v295 v232 -v908 -v804 -v690 v307 v231 -v907 -v833 v825 -v753 v655 -v454 -v337 v821 v656 -v342 -v339 -v141 -v915 v838 v820 v651 -v341 -v919 -v699 -v609 -v923 v841 v756 -v701 v649 -v408 -v349 -v333 -v922 v839 -v707 v353 -v891 v703 v411 -v370 v357 -v334 -v893 v715 -v374 v356 -v562 v99 -v897 v566 v98 -v898 v887 -v735 v553 -v479 v441 -v420 -v170 -v116 v657 v552 -v481 v419 -v175 v659 -v505 -v447 v436 v171 v660 -v506 -v218 -v183 -v743 v676 v501 v475 -v452 -v219 -v294 v220 v822 -v749 -v688 -v654 -v549 v499 v476 -v455 v315 v236 -v826 v824 -v692 -v653 -v453 -v338 v311 -v828 -v754 v310 -v909 -v834 -v910 v830 -v818 v757 v694 -v911 v842 v755 -v695 v343 -v927 -v819 v650 -v407 v344 -v892 -v702 -v557 v345 v723 v556 v413 -v372 v361 -v719 -v376 -v718 v563 v567 -v888 -v568 v416 -v569 -v504 -v480 v437 -v503 v440 v439 -v169 -v679 v442 v435 v190 -v682 -v680 -v448 -v187 -v681 v675 v444 v433 v312 v239 -v186 v823 -v742 -v456 v314 v240 -v744 -v689 v673 v500 v235 -v750 -v693 v746 v697 v308 v233 -v829 v758 v696 -v930 v849 -v405 v309 -v931 v846 -v367 -v926 v845 v720 -v409 -v366 v364 v722 v365 -v924 v414 -v373 v360 v558 -v377 -v932 -v716 v559 v417 v358 v415 -v717 -v678 v438 v189 -v677 v188 -v238 v443 -v313 v237 -v459 -v434 -v184 -v683 v457 -v684 v674 v458 -v185 -v745 v685 -v929 v848 -v761 -v698 -v234 -v928 v847 v759 v760 -v363 -v721 -v404 v362 v843 -v403 v410 -v368 -v925 -v844 v406 -v369 v418 -v571 v933 v359 -v570 one
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.97 0.91 2/54 13141
Raw data (stat): 13141 (runsolver) R 13140 4613 4612 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 857749915 884736 94 4294967295 134512640 135332820 3221224448 3221219612 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.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0008 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0015 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.0036 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13144
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 13179
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.009 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 13197
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.011 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13199
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 13201
Raw data (stat): 13141 (vallstSAT2005PB) S 13140 4613 4612 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857749915 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13207
Raw data (stat): 13141 (vallstSAT2005PB) R 13140 4613 4612 0 -1 0 430 1550 0 0 19 6 120182 2808 20 0 1 0 857749915 2179072 249 4294967295 134512640 135087896 3221224512 3221220988 1074810715 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.48 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 13213
Raw data (stat): 13141 (vallstSAT2005PB) R 13140 4613 4612 0 -1 0 430 1550 0 0 19 6 120182 2808 20 0 1 0 857749915 2179072 249 4294967295 134512640 135087896 3221224512 3221220988 1074810715 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.48
CPU time (s): 1230.29
CPU user time (s): 1202.08
CPU system time (s): 28.2047
CPU usage (%): 99.984
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier: OK 205
#### END VERIFIER DATA ####