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.5:100.opb |
| MD5SUM | feaa96df552ef9989407735877840272 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 13 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 776 |
| Biggest coefficient in the objective function | 474 |
| Number of bits for the biggest coefficient in the objective function | 9 |
| Sum of the numbers in the objective function | 2127 |
| Number of bits of the sum of numbers in the objective function | 12 |
| Biggest number in a constraint | 474 |
| Number of bits of the biggest number in a constraint | 9 |
| Biggest sum of numbers in a constraint | 2127 |
| 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.04084 |
| Number of variables | 776 |
| Total number of constraints | 1642 |
| Number of constraints which are clauses | 701 |
| Number of constraints which are cardinality constraints (but not clauses) | 941 |
| 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 33844
#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-27 16:53:38 (client local time)
PB2005-SCRIPT v4.0
MARKUPS: idlaunch=3320 boxname=wulflinc19 idbench=369 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH: feaa96df552ef9989407735877840272 /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.5:100.opb 0
IDLAUNCH: 3320
/proc/cpuinfo:
processor : 0
vendor_id : GenuineIntel
cpu family : 6
model : 7
model name : Pentium III (Katmai)
stepping : 3
cpu MHz : 451.037
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.037
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: 751128 kB
Buffers: 28892 kB
Cached: 230088 kB
SwapCached: 3840 kB
Active: 42680 kB
Inactive: 221712 kB
HighTotal: 131008 kB
HighFree: 252 kB
LowTotal: 903652 kB
LowFree: 750876 kB
SwapTotal: 2097892 kB
SwapFree: 2093360 kB
Dirty: 2428 kB
Writeback: 0 kB
Mapped: 5444 kB
Slab: 13512 kB
Committed_AS: 63604 kB
PageTables: 316 kB
VmallocTotal: 114680 kB
VmallocUsed: 1368 kB
VmallocChunk: 113252 kB
JOB ENDED THE 2005-05-27 17:14:09 (client local time) WITH STATUS 10 IN 1230.24 SECONDS
stats: 3320 0 1230.24 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: 294; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-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: 1334 (792:>=*);
#decisions: 287; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1335 (791:>=*);
#decisions: 286; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1336 (790:>=*);
#decisions: 285; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1337 (789:>=*);
#decisions: 282; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1338 (788:>=*);
#decisions: 281; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1339 (787:>=*);
#decisions: 280; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1340 (786:>=*);
#decisions: 276; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1341 (785:>=*);
#decisions: 275; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1342 (784:>=*);
#decisions: 274; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1343 (783:>=*);
#decisions: 272; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1344 (782:>=*);
#decisions: 270; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1345 (781:>=*);
#decisions: 269; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1346 (780:>=*);
#decisions: 264; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1347 (779:>=*);
#decisions: 263; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1348 (778:>=*);
#decisions: 264; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1349 (777:>=*);
#decisions: 262; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1350 (776:>=*);
#decisions: 263; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1351 (775:>=*);
#decisions: 259; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1352 (774:>=*);
#decisions: 255; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1353 (773:>=*);
#decisions: 253; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1354 (772:>=*);
#decisions: 250; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1355 (771:>=*);
#decisions: 249; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1356 (770:>=*);
#decisions: 248; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1357 (769:>=*);
#decisions: 247; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1358 (768:>=*);
#decisions: 245; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1359 (767:>=*);
#decisions: 244; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1360 (766:>=*);
#decisions: 243; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1361 (765:>=*);
#decisions: 243; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1362 (764:>=*);
#decisions: 238; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1363 (763:>=*);
#decisions: 235; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1364 (762:>=*);
#decisions: 233; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1365 (761:>=*);
#decisions: 232; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1366 (760:>=*);
#decisions: 231; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1367 (759:>=*);
#decisions: 231; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1368 (758:>=*);
#decisions: 230; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1369 (757:>=*);
#decisions: 227; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1370 (756:>=*);
#decisions: 235; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1371 (755:>=*);
#decisions: 229; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1372 (754:>=*);
#decisions: 226; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1373 (753:>=*);
#decisions: 225; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1374 (752:>=*);
#decisions: 224; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1375 (751:>=*);
#decisions: 223; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1376 (750:>=*);
#decisions: 225; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1377 (749:>=*);
#decisions: 222; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1378 (748:>=*);
#decisions: 220; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1379 (747:>=*);
#decisions: 213; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1380 (746:>=*);
#decisions: 212; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1381 (745:>=*);
#decisions: 211; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1382 (744:>=*);
#decisions: 212; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1383 (743:>=*);
#decisions: 211; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1384 (742:>=*);
#decisions: 210; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1385 (741:>=*);
#decisions: 209; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1386 (740:>=*);
#decisions: 207; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1387 (739:>=*);
#decisions: 202; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1388 (738:>=*);
#decisions: 200; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1389 (737:>=*);
#decisions: 199; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1390 (736:>=*);
#decisions: 197; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1391 (735:>=*);
#decisions: 197; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1392 (734:>=*);
#decisions: 196; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1393 (733:>=*);
#decisions: 195; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1394 (732:>=*);
#decisions: 194; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1395 (731:>=*);
#decisions: 193; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1396 (730:>=*);
#decisions: 191; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1397 (729:>=*);
#decisions: 189; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1398 (728:>=*);
#decisions: 188; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1399 (727:>=*);
#decisions: 187; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1400 (726:>=*);
#decisions: 192; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1401 (725:>=*);
#decisions: 187; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1402 (724:>=*);
#decisions: 186; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1403 (723:>=*);
#decisions: 185; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1404 (722:>=*);
#decisions: 184; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1405 (721:>=*);
#decisions: 183; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1406 (720:>=*);
#decisions: 187; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1407 (719:>=*);
#decisions: 183; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1408 (718:>=*);
#decisions: 182; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1409 (717:>=*);
#decisions: 181; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1410 (716:>=*);
#decisions: 179; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1411 (715:>=*);
#decisions: 177; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1412 (714:>=*);
#decisions: 176; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1413 (713:>=*);
#decisions: 175; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1414 (712:>=*);
#decisions: 174; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1415 (711:>=*);
#decisions: 175; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1416 (710:>=*);
#decisions: 172; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1417 (709:>=*);
#decisions: 171; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1418 (708:>=*);
#decisions: 174; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1419 (707:>=*);
#decisions: 169; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1420 (706:>=*);
#decisions: 165; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1421 (705:>=*);
#decisions: 160; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1422 (704:>=*);
#decisions: 160; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1423 (703:>=*);
#decisions: 157; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1424 (702:>=*);
#decisions: 156; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1425 (701:>=*);
#decisions: 152; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1426 (700:>=*);
#decisions: 149; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1427 (699:>=*);
#decisions: 146; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1428 (698:>=*);
#decisions: 142; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1429 (697:>=*);
#decisions: 141; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1430 (696:>=*);
#decisions: 140; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1431 (695:>=*);
#decisions: 142; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1432 (694:>=*);
#decisions: 140; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1433 (693:>=*);
#decisions: 139; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1434 (692:>=*);
#decisions: 140; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1435 (691:>=*);
#decisions: 137; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1436 (690:>=*);
#decisions: 136; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1437 (689:>=*);
#decisions: 137; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1438 (688:>=*);
#decisions: 132; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1439 (687:>=*);
#decisions: 128; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1440 (686:>=*);
#decisions: 127; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1441 (685:>=*);
#decisions: 126; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1442 (684:>=*);
#decisions: 124; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1443 (683:>=*);
#decisions: 125; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1444 (682:>=*);
#decisions: 124; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1445 (681:>=*);
#decisions: 123; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1446 (680:>=*);
#decisions: 127; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1447 (679:>=*);
#decisions: 119; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1448 (678:>=*);
#decisions: 116; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1449 (677:>=*);
#decisions: 114; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1450 (676:>=*);
#decisions: 112; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1451 (675:>=*);
#decisions: 110; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1452 (674:>=*);
#decisions: 124; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1453 (673:>=*);
#decisions: 120; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1454 (672:>=*);
#decisions: 117; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1455 (671:>=*);
#decisions: 113; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1456 (670:>=*);
#decisions: 112; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1457 (669:>=*);
#decisions: 111; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1458 (668:>=*);
#decisions: 110; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1459 (667:>=*);
#decisions: 113; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1460 (666:>=*);
#decisions: 113; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1461 (665:>=*);
#decisions: 114; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1462 (664:>=*);
#decisions: 109; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1463 (663:>=*);
#decisions: 117; #end-nodes: 7;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 7 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1464 (662:>=*);
#decisions: 314; #end-nodes: 92;
#proof improvement attempts: 0; #restarts: 1
Current batch, end-nodes: 12 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1465 (661:>=*);
#decisions: 116; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1466 (660:>=*);
#decisions: 714; #end-nodes: 241;
#proof improvement attempts: 0; #restarts: 3
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1467 (659:>=*);
#decisions: 117; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1468 (658:>=*);
#decisions: 116; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1469 (657:>=*);
#decisions: 115; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1470 (656:>=*);
#decisions: 119; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1471 (655:>=*);
#decisions: 114; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1472 (654:>=*);
#decisions: 118; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1473 (653:>=*);
#decisions: 135; #end-nodes: 21;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 21 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1474 (652:>=*);
#decisions: 529; #end-nodes: 170;
#proof improvement attempts: 0; #restarts: 2
Current batch, end-nodes: 10 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1475 (651:>=*);
#decisions: 1799; #end-nodes: 682;
#proof improvement attempts: 0; #restarts: 8
Current batch, end-nodes: 35 / 82 (82)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1476 (650:>=*);
#decisions: 130; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1477 (649:>=*);
#decisions: 153; #end-nodes: 23;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 23 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1478 (648:>=*);
#decisions: 209; #end-nodes: 78;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 78 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1479 (647:>=*);
#decisions: 156; #end-nodes: 25;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 25 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1480 (646:>=*);
#decisions: 175; #end-nodes: 46;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 46 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1481 (645:>=*);
#decisions: 350; #end-nodes: 81;
#proof improvement attempts: 0; #restarts: 1
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1482 (644:>=*);
#decisions: 141; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1483 (643:>=*);
#decisions: 140; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1484 (642:>=*);
#decisions: 141; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1485 (641:>=*);
#decisions: 139; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1486 (640:>=*);
#decisions: 137; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1487 (639:>=*);
#decisions: 138; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1488 (638:>=*);
#decisions: 136; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1489 (637:>=*);
#decisions: 135; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1490 (636:>=*);
#decisions: 134; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1491 (635:>=*);
#decisions: 138; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1492 (634:>=*);
#decisions: 135; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1493 (633:>=*);
#decisions: 133; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1494 (632:>=*);
#decisions: 137; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1495 (631:>=*);
#decisions: 134; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1496 (630:>=*);
#decisions: 132; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1497 (629:>=*);
#decisions: 133; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1498 (628:>=*);
#decisions: 130; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1499 (627:>=*);
#decisions: 129; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1500 (626:>=*);
#decisions: 128; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1501 (625:>=*);
#decisions: 124; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1502 (624:>=*);
#decisions: 123; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1503 (623:>=*);
#decisions: 121; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1504 (622:>=*);
#decisions: 124; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1505 (621:>=*);
#decisions: 120; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1506 (620:>=*);
#decisions: 122; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1507 (619:>=*);
#decisions: 126; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1508 (618:>=*);
#decisions: 122; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1509 (617:>=*);
#decisions: 123; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1510 (616:>=*);
#decisions: 119; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1511 (615:>=*);
#decisions: 12563; #end-nodes: 5520;
#proof improvement attempts: 0; #restarts: 63
Current batch, end-nodes: 2 / 95 (95)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1512 (614:>=*);
#decisions: 121; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1513 (613:>=*);
#decisions: 123; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1514 (612:>=*);
#decisions: 149; #end-nodes: 33;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 33 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1515 (611:>=*);
#decisions: 127; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1516 (610:>=*);
#decisions: 126; #end-nodes: 8;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 8 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1517 (609:>=*);
#decisions: 121; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1518 (608:>=*);
#decisions: 25161; #end-nodes: 11699;
#proof improvement attempts: 0; #restarts: 123
Current batch, end-nodes: 0 / 110 (110)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1519 (607:>=*);
#decisions: 128; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1520 (606:>=*);
#decisions: 128; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1521 (605:>=*);
#decisions: 123; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1522 (604:>=*);
#decisions: 122; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1523 (603:>=*);
#decisions: 121; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1524 (602:>=*);
#decisions: 120; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1525 (601:>=*);
#decisions: 120; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1526 (600:>=*);
#decisions: 119; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1527 (599:>=*);
#decisions: 118; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1528 (598:>=*);
#decisions: 120; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1529 (597:>=*);
#decisions: 118; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1530 (596:>=*);
#decisions: 119; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1531 (595:>=*);
#decisions: 139; #end-nodes: 21;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 21 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1532 (594:>=*);
#decisions: 220042; #end-nodes: 137956;
#proof improvement attempts: 0; #restarts: 778
Current batch, end-nodes: 247 / 274 (274)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1533 (593:>=*);
#decisions: 30394; #end-nodes: 14664;
#proof improvement attempts: 0; #restarts: 149
Current batch, end-nodes: 0 / 117 (117)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1534 (592:>=*);
#decisions: 124; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1535 (591:>=*);
#decisions: 123; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1536 (590:>=*);
#decisions: 122; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1537 (589:>=*);
#decisions: 123; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1538 (588:>=*);
#decisions: 119; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1539 (587:>=*);
#decisions: 118; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1540 (586:>=*);
#decisions: 116; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1541 (585:>=*);
#decisions: 118; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1542 (584:>=*);
#decisions: 115; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1543 (583:>=*);
#decisions: 114; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1544 (582:>=*);
#decisions: 115; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1545 (581:>=*);
#decisions: 118; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1546 (580:>=*);
#decisions: 118; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1547 (579:>=*);
#decisions: 177; #end-nodes: 60;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 60 / 80 (80)
#axs: 867, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1548 (578:>=*);
Interupt request received.
Model found with constant:
(pushed:) 1548 (578:>=*)
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: 0 (#equs: 0)
Time taken: 20 min, 29 sec
times:
0m0.020s 0m0.006s
20m7.114s 0m22.722s
v -v756 -v693 -v588 v262 v241 v56 -v38 v692 v590 -v486 -v263 -v246 v55 -v37 v757 -v700 v589 -v485 -v439 v266 -v245 -v54 -v39 v758 -v694 v594 -v487 -v444 -v264 -v52 v40 v761 -v695 -v612 v593 v488 -v443 -v265 -v248 -v53 -v47 -v759 -v696 v611 v591 v489 -v401 -v249 -v41 -v2 -v760 v613 -v592 v496 v446 -v421 -v400 -v252 v198 -v171 -v42 -v1 -v734 -v616 -v490 v447 v420 -v406 -v385 -v250 -v176 -v43 -v3 -v733 v615 -v491 v450 v422 -v405 -v384 -v273 -v251 v197 -v175 -v137 -v4 v620 -v492 -v448 -v425 -v407 v386 -v366 -v278 -v201 -v155 -v136 -v18 v5 -v735 v619 -v559 -v510 -v449 v424 v411 v387 -v365 -v277 -v178 -v154 -v138 -v87 -v17 -v12 -v737 -v650 -v617 -v515 -v429 v410 v388 -v202 -v179 -v156 v141 -v86 -v23 -v6 -v649 -v618 -v558 v514 -v466 -v428 -v408 v395 -v367 -v280 v182 -v157 v140 -v88 -v66 -v22 -v7 -v738 -v562 -v426 -v409 -v389 v369 -v281 v180 v158 -v145 -v91 -v71 -v24 -v8 -v740 -v651 -v517 -v469 -v427 -v390 -v318 -v284 -v223 -v181 -v165 -v144 -v121 v90 v70 -v28 -v741 -v653 v635 -v563 -v518 -v470 -v391 -v370 v317 -v282 -v159 -v142 v95 -v27 v634 -v521 v372 -v347 v319 -v283 -v222 -v160 -v143 -v120 v94 -v73 -v25 -v654 -v519 v373 v351 -v322 -v226 -v161 v92 -v74 -v26 -v656 v636 -v520 v321 -v124 -v93 v75 -v657 v639 v323 -v227 -v125 v76 -v753 v703 -v64 -v755 v704 -v587 v267 v240 -v60 v754 -v699 -v602 v242 -v59 -v50 v762 v598 v438 -v247 -v51 -v710 -v697 -v597 v499 v440 v244 -v46 -v714 v500 -v445 -v253 v495 v442 -v44 -v729 v614 v451 -v402 -v170 -v728 v628 v493 -v403 v199 -v172 v15 -v624 v423 v404 -v361 -v272 -v203 -v177 v16 -v736 -v623 -v437 v415 v398 -v360 -v274 v174 -v11 -v739 -v645 -v509 -v433 v399 v279 v183 -v139 -v19 -v743 -v644 -v560 -v511 -v465 -v432 v394 -v368 v276 -v205 v168 -v153 -v20 -v9 -v742 -v564 v516 v371 -v285 -v206 v169 -v149 -v89 -v65 -v21 -v652 v513 -v471 v392 v375 -v164 -v148 -v116 -v103 -v67 -v32 -v655 -v630 -v522 v374 v99 v72 -v659 -v629 -v566 -v346 -v224 -v162 -v122 -v98 v69 -v658 -v567 v350 v320 -v228 v77 v637 -v474 -v331 v126 v638 -v327 v701 -v599 v105 -v63 -v49 -v752 -v601 v271 -v48 -v770 v498 v270 -v57 v766 v497 v243 -v765 -v709 -v698 -v595 v261 -v58 -v713 v441 -v257 v193 -v625 -v596 v459 -v302 -v256 v192 -v45 -v14 v627 -v455 v13 v494 -v454 -v434 v418 -v397 v200 -v730 -v554 -v436 v419 v396 -v204 -v173 -v731 -v621 -v553 -v461 v414 -v208 v191 -v167 -v150 v732 -v362 -v275 -v207 -v187 v166 -v152 -v747 -v622 -v561 -v467 -v430 v412 -v363 -v293 -v186 -v100 -v35 -v10 -v646 -v565 -v512 v364 -v289 -v218 -v102 -v36 -v685 -v647 -v569 v530 v472 -v431 v393 -v379 -v288 -v217 -v146 -v31 v648 -v568 v526 -v115 -v68 -v663 v525 -v475 -v348 -v328 -v225 -v163 -v147 -v117 -v96 v85 -v29 -v631 -v473 v352 -v330 -v229 -v123 v81 -v632 -v230 v119 -v97 v80 v633 -v326 -v231 -v127 -v767 -v702 -v600 -v333 v104 -v61 -v769 v268 v258 v260 -v763 -v711 v456 -v299 v269 -v715 -v626 v458 -v764 -v417 -v301 -v254 -v435 v416 v194 v717 -v452 -v255 v195 v188 v718 v196 v190 -v151 v750 -v453 -v290 -v212 -v34 v751 -v555 -v460 -v292 -v101 -v33 -v746 -v681 -v556 v527 -v462 -v413 v382 -v184 v557 v529 -v468 v383 -v343 -v744 -v684 v666 -v573 v464 -v378 -v342 -v286 -v185 v82 v667 -v476 -v329 -v219 v84 -v662 -v534 v523 -v376 v349 -v287 -v220 -v30 -v538 v353 v221 -v118 -v660 v642 -v604 v524 -v354 v235 -v135 -v78 v643 v608 -v355 -v324 v131 -v768 v332 v106 -v62 v706 v259 v705 -v457 v712 -v298 v108 -v716 v720 v303 v719 v189 -v749 v215 -v748 -v291 v216 v677 v381 v306 -v211 v528 v380 -v680 v665 v576 -v209 v664 v577 -v463 v83 -v745 v686 -v572 -v484 v480 -v344 v641 -v570 -v533 v479 -v377 -v345 v238 -v132 v640 -v537 v239 -v134 -v689 -v661 -v603 v234 -v79 v607 -v325 v130 v502 v295 v109 v707 v107 v708 -v546 -v335 -v300 v771 v724 v304 -v214 v213 -v673 v307 v305 -v772 v676 v773 -v575 v574 -v682 -v481 -v210 -v483 v687 v237 v236 -v133 -v690 -v571 -v535 v477 -v358 -v688 -v539 -v359 v605 -v478 v232 v609 v128 v110 v501 -v336 -v334 v294 -v727 v545 v296 v723 v308 v721 -v672 -v582 -v482 -v683 -v532 v679 v531 -v357 -v691 -v356 v536 v540 v606 v233 v610 -v129 -v337 v114 -v726 v503 v113 -v725 v547 v297 -v669 v506 v316 v312 v722 -v674 -v581 v549 v311 v550 v678 v586 -v542 v341 -v541 v504 v340 v111 v548 v507 v313 v112 v505 v315 v580 v552 v668 v551 v670 v583 v309 -v675 v310 v585 v338 -v543 v508 v314 v544 v339 v774 v579 v578 v671 v584 -v775 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
Raw data (loadavg): 0.92 0.98 0.92 2/54 12864
Raw data (stat): 12864 (runsolver) R 12863 10795 10794 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 857746778 884736 93 4294967295 134512640 135332820 3221224448 3221219792 134957970 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 93 205 205 0 11 0
vsize: 864
Current StackSize limit: 67108864 bytes
[startup+9.99986 s]
Raw data (loadavg): 0.93 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0003 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0017 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0012 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0017 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0017 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0031 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.0031 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.005 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 12867
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.009 s]
Raw data (loadavg): 1.07 1.00 0.93 3/58 12908
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.01 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.009 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.04 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.01 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.03 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.03 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 12920
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.01 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12922
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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 1.00 0.93 2/55 12924
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 857746778 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 12932
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 467 1536 0 0 20 5 120712 2277 21 0 1 0 857746778 2179072 253 4294967295 134512640 135087896 3221224512 3221222168 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 253 485 147 0 385 0
vsize: 2128
[startup+1230.42 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 12936
Raw data (stat): 12864 (vallstSAT2005PB) S 12863 10795 10794 0 -1 0 467 1536 0 0 20 5 120712 2277 21 0 1 0 857746778 2179072 253 4294967295 134512640 135087896 3221224512 3221222168 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 253 485 147 0 385 0
vsize: 0
Child status: 10
Real time (s): 1230.42
CPU time (s): 1230.24
CPU user time (s): 1207.35
CPU system time (s): 22.8865
CPU usage (%): 99.9855
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier: OK 104
#### END VERIFIER DATA ####