PB'05 competition: run trace

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/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-bell5.opb
MD5SUM	de15576cff54b253255390d90c832bf8
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	948
Biggest coefficient in the objective function	6291456000000000
Number of bits for the biggest coefficient in the objective function	53
Sum of the numbers in the objective function	104362034158211275
Number of bits of the sum of numbers in the objective function	57
Biggest number in a constraint	6291456000000000
Number of bits of the biggest number in a constraint	53
Biggest sum of numbers in a constraint	104362034158211275
Number of bits of the biggest sum of numbers	57
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	3.13352
Number of variables	1244
Total number of constraints	149
Number of constraints which are clauses	15
Number of constraints which are cardinality constraints (but not clauses)	30
Number of constraints which are nor clauses,nor cardinality constraints	104
Minimum length of a constraint	1
Maximum length of a constraint	95

Trace number 34209

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-27 20:47:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18221 boxname=wulflinc15 idbench=1402 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322  /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH:  de15576cff54b253255390d90c832bf8  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bell5.opb
REAL COMMAND:  vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bell5.opb 0
IDLAUNCH: 18221
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        893920 kB
Buffers:          6432 kB
Cached:         112736 kB
SwapCached:        648 kB
Active:          21436 kB
Inactive:        99864 kB
HighTotal:      131008 kB
HighFree:        80724 kB
LowTotal:       903652 kB
LowFree:        813196 kB
SwapTotal:     2097136 kB
SwapFree:      2095604 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5084 kB
Slab:            13976 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 20:47:29 (client local time) WITH STATUS 30 IN 3.13352 SECONDS
stats: 18221 0 3.13352 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 119  (#equs: 0)
Nr of vars set: 122  (#equs: 0)
#decisions: 1303;  #end-nodes: 88;
#proof improvement attempts: 0;  #restarts: 1
Current batch, end-nodes: 7 / 82 (80)
#axs: 115, #non-axs: 6
tight: meta-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:  2229981376 (287227914:>=*);
Model found with constant:
  (pushed:) 4294967295 (2517209291:>=*)

With an increment of the last pushed constant, a proof of false was found.
result: proof of false found (0)
seed: 0
Nr of vars set: 122  (#equs: 0)
Time taken in milliseconds: 2610
times:
0m0.015s 0m0.009s
0m2.365s 0m0.267s
v -d1_bit0 -d2_bit0 -d3_bit0 -d4_bit0 -d5_bit0 -d6_bit0  d7_bit0 -d9_bit0  d10_bit0  d11_bit0 -d12_bit0 -d13_bit0 -d14_bit0 -d16_bit0 -h1_bit0 -h1_bit1  h1_bit2  h1_bit3 -h1_bit4 -h1_bit5 -h1_bit6 -h1_bit7 -h1_bit8 -h1_bit9 -h1_bit10 -h1_bit11 -h1_bit12 -h1_bit13  h2_bit0 -h2_bit1 -h2_bit2 -h2_bit3  h2_bit4 -h2_bit5 -h2_bit6 -h2_bit7 -h2_bit8 -h2_bit9 -h2_bit10 -h2_bit11 -h2_bit12 -h2_bit13  h3_bit0 -h3_bit1  h3_bit2 -h3_bit3 -h3_bit4 -h3_bit5 -h3_bit6 -h3_bit7 -h3_bit8 -h3_bit9 -h3_bit10 -h3_bit11 -h3_bit12 -h3_bit13  h4_bit0 -h4_bit1 -h4_bit2 -h4_bit3  h4_bit4 -h4_bit5 -h4_bit6 -h4_bit7 -h4_bit8 -h4_bit9 -h4_bit10 -h4_bit11 -h4_bit12 -h4_bit13 -h5_bit0 -h5_bit1  h5_bit2  h5_bit3 -h5_bit4 -h5_bit5 -h5_bit6 -h5_bit7 -h5_bit8 -h5_bit9 -h5_bit10 -h5_bit11 -h5_bit12 -h5_bit13 -h6_bit0 -h6_bit1 -h6_bit2 -h6_bit3 -h6_bit4 -h6_bit5 -h6_bit6 -h6_bit7 -h6_bit8 -h6_bit9 -h6_bit10 -h6_bit11 -h6_bit12 -h6_bit13 -h7_bit0  h7_bit1 -h7_bit2 -h7_bit3  h7_bit4 -h7_bit5 -h7_bit6 -h7_bit7 -h7_bit8 -h7_bit9 -h7_bit10 -h7_bit11 -h7_bit12 -h7_bit13 -h9_bit0 -h9_bit1 -h9_bit2 -h9_bit3 -h9_bit4 -h9_bit5 -h9_bit6 -h9_bit7 -h9_bit8 -h9_bit9 -h9_bit10 -h9_bit11 -h9_bit12 -h9_bit13  h10_bit0  h10_bit1  h10_bit2  h10_bit3 -h10_bit4 -h10_bit5 -h10_bit6 -h10_bit7 -h10_bit8 -h10_bit9  h11_bit0  h11_bit1 -h11_bit2 -h11_bit3  h11_bit4 -h11_bit5 -h11_bit6 -h11_bit7 -h11_bit8 -h11_bit9  h12_bit0  h12_bit1 -h12_bit2 -h12_bit3 -h12_bit4 -h12_bit5 -h12_bit6 -h12_bit7 -h12_bit8 -h12_bit9 -h13_bit0 -h13_bit1 -h13_bit2  h13_bit3 -h13_bit4 -h13_bit5 -h13_bit6 -h13_bit7 -h13_bit8 -h13_bit9 -h14_bit0 -h14_bit1 -h14_bit2  h14_bit3 -h14_bit4 -h14_bit5 -h14_bit6 -h14_bit7 -h14_bit8 -h14_bit9 -h16_bit0 -h16_bit1 -h16_bit2 -h16_bit3 -h16_bit4 -h16_bit5 -h16_bit6 -h16_bit7 -h16_bit8 -h16_bit9 -g1_bit0  g1_bit1 -g1_bit2 -g1_bit3  g1_bit4 -g1_bit5 -g1_bit6  g1_bit7  g1_bit8 -g1_bit9 -g2_bit0 -g2_bit1 -g2_bit2 -g2_bit3 -g2_bit4  g2_bit5  g2_bit6 -g2_bit7  g2_bit8 -g2_bit9 -g3_bit0 -g3_bit1 -g3_bit2 -g3_bit3 -g3_bit4 -g3_bit5 -g3_bit6 -g3_bit7  g3_bit8 -g3_bit9 -g4_bit0 -g4_bit1 -g4_bit2 -g4_bit3 -g4_bit4 -g4_bit5 -g4_bit6 -g4_bit7 -g4_bit8  g4_bit9 -g5_bit0  g5_bit1 -g5_bit2 -g5_bit3 -g5_bit4  g5_bit5 -g5_bit6 -g5_bit7  g5_bit8  g5_bit9 -g6_bit0 -g6_bit1 -g6_bit2 -g6_bit3  g6_bit4 -g6_bit5 -g6_bit6 -g6_bit7 -g6_bit8 -g6_bit9 -g7_bit0  g7_bit1  g7_bit2 -g7_bit3 -g7_bit4  g7_bit5  g7_bit6 -g7_bit7  g7_bit8 -g7_bit9 -g9_bit0  g9_bit1  g9_bit2  g9_bit3 -g9_bit4 -g9_bit5 -g9_bit6 -g9_bit7 -g9_bit8  g9_bit9 -g10_bit0  g10_bit1  g10_bit2 -g10_bit3  g10_bit4 -g10_bit5  g10_bit6  g11_bit0  g11_bit1 -g11_bit2 -g11_bit3 -g11_bit4  g11_bit5  g11_bit6 -g12_bit0  g12_bit1  g12_bit2  g12_bit3  g12_bit4 -g12_bit5  g12_bit6 -g13_bit0 -g13_bit1  g13_bit2 -g13_bit3 -g13_bit4  g13_bit5  g13_bit6 -g14_bit0 -g14_bit1  g14_bit2  g14_bit3  g14_bit4 -g14_bit5  g14_bit6  g16_bit0  g16_bit1  g16_bit2  g16_bit3  g16_bit4 -g16_bit5  g16_bit6 -a1_bit_7 -a1_bit_6  a1_bit_5 -a1_bit_4 -a1_bit_3 -a1_bit_2  a1_bit_1 -a1_bit0  a1_bit1 -a1_bit2  a1_bit3  a1_bit4 -a1_bit5  a1_bit6 -a1_bit7 -a1_bit8  a1_bit9 -a1_bit10  a1_bit11  a1_bit12  a2_bit_7 -a2_bit_6  a2_bit_5  a2_bit_4 -a2_bit_3  a2_bit_2  a2_bit_1  a2_bit0 -a2_bit1  a2_bit2  a2_bit3 -a2_bit4 -a2_bit5  a2_bit6  a2_bit7  a2_bit8 -a2_bit9 -a2_bit10  a2_bit11  a2_bit12  a3_bit_7  a3_bit_6 -a3_bit_5 -a3_bit_4 -a3_bit_3 -a3_bit_2 -a3_bit_1  a3_bit0 -a3_bit1 -a3_bit2 -a3_bit3 -a3_bit4 -a3_bit5 -a3_bit6 -a3_bit7  a3_bit8 -a3_bit9 -a3_bit10 -a3_bit11 -a3_bit12 -a4_bit_7 -a4_bit_6 -a4_bit_5 -a4_bit_4 -a4_bit_3 -a4_bit_2 -a4_bit_1 -a4_bit0 -a4_bit1 -a4_bit2 -a4_bit3 -a4_bit4 -a4_bit5 -a4_bit6 -a4_bit7 -a4_bit8 -a4_bit9 -a4_bit10 -a4_bit11 -a4_bit12 -a5_bit_7 -a5_bit_6 -a5_bit_5 -a5_bit_4 -a5_bit_3 -a5_bit_2 -a5_bit_1 -a5_bit0 -a5_bit1 -a5_bit2 -a5_bit3 -a5_bit4 -a5_bit5 -a5_bit6 -a5_bit7 -a5_bit8 -a5_bit9 -a5_bit10 -a5_bit11 -a5_bit12 -a6_bit_7 -a6_bit_6 -a6_bit_5 -a6_bit_4 -a6_bit_3 -a6_bit_2  a6_bit_1 -a6_bit0 -a6_bit1 -a6_bit2 -a6_bit3  a6_bit4 -a6_bit5 -a6_bit6 -a6_bit7 -a6_bit8 -a6_bit9  a6_bit10 -a6_bit11 -a6_bit12  a7_bit_7  a7_bit_6  a7_bit_5  a7_bit_4  a7_bit_3  a7_bit_2  a7_bit_1  a7_bit0  a7_bit1  a7_bit2 -a7_bit3  a7_bit4  a7_bit5  a7_bit6  a7_bit7  a7_bit8  a7_bit9  a7_bit10 -a7_bit11  a7_bit12 -a8_bit_7 -a8_bit_6  a8_bit_5  a8_bit_4 -a8_bit_3 -a8_bit_2 -a8_bit_1  a8_bit0  a8_bit1  a8_bit2 -a8_bit3  a8_bit4 -a8_bit5 -a8_bit6 -a8_bit7 -a8_bit8  a8_bit9  a8_bit10 -a8_bit11  a8_bit12 -a9_bit_7  a9_bit_6 -a9_bit_5 -a9_bit_4 -a9_bit_3 -a9_bit_2  a9_bit_1 -a9_bit0 -a9_bit1 -a9_bit2 -a9_bit3 -a9_bit4 -a9_bit5  a9_bit6 -a9_bit7  a9_bit8 -a9_bit9 -a9_bit10 -a9_bit11 -a9_bit12 -a10_bit_7 -a10_bit_6 -a10_bit_5 -a10_bit_4 -a10_bit_3 -a10_bit_2 -a10_bit_1 -a10_bit0 -a10_bit1 -a10_bit2 -a10_bit3 -a10_bit4 -a10_bit5 -a10_bit6 -a10_bit7 -a10_bit8 -a10_bit9 -a10_bit10 -a10_bit11 -a10_bit12  a11_bit_7  a11_bit_6  a11_bit_5  a11_bit_4  a11_bit_3  a11_bit_2  a11_bit_1 -a11_bit0  a11_bit1  a11_bit2 -a11_bit3  a11_bit4  a11_bit5 -a11_bit6 -a11_bit7 -a11_bit8  a11_bit9  a11_bit10 -a11_bit11 -a11_bit12 -a12_bit_7 -a12_bit_6  a12_bit_5 -a12_bit_4 -a12_bit_3 -a12_bit_2 -a12_bit_1  a12_bit0 -a12_bit1 -a12_bit2  a12_bit3  a12_bit4 -a12_bit5  a12_bit6 -a12_bit7 -a12_bit8 -a12_bit9 -a12_bit10 -a12_bit11 -a12_bit12 -a13_bit_7  a13_bit_6 -a13_bit_5 -a13_bit_4 -a13_bit_3 -a13_bit_2 -a13_bit_1 -a13_bit0  a13_bit1 -a13_bit2 -a13_bit3 -a13_bit4 -a13_bit5  a13_bit6 -a13_bit7 -a13_bit8  a13_bit9  a13_bit10 -a13_bit11 -a13_bit12 -a14_bit_7 -a14_bit_6 -a14_bit_5 -a14_bit_4  a14_bit_3 -a14_bit_2  a14_bit_1  a14_bit0 -a14_bit1 -a14_bit2 -a14_bit3 -a14_bit4 -a14_bit5 -a14_bit6 -a14_bit7 -a14_bit8 -a14_bit9 -a14_bit10 -a14_bit11 -a14_bit12 -a15_bit_7 -a15_bit_6 -a15_bit_5 -a15_bit_4 -a15_bit_3 -a15_bit_2 -a15_bit_1 -a15_bit0 -a15_bit1 -a15_bit2 -a15_bit3 -a15_bit4 -a15_bit5 -a15_bit6 -a15_bit7 -a15_bit8 -a15_bit9  a15_bit10 -a15_bit11 -a15_bit12  a16_bit_7 -a16_bit_6 -a16_bit_5 -a16_bit_4 -a16_bit_3 -a16_bit_2  a16_bit_1 -a16_bit0 -a16_bit1 -a16_bit2 -a16_bit3 -a16_bit4 -a16_bit5 -a16_bit6 -a16_bit7 -a16_bit8 -a16_bit9  a16_bit10 -a16_bit11 -a16_bit12  b1_bit_7 -b1_bit_6  b1_bit_5 -b1_bit_4 -b1_bit_3 -b1_bit_2 -b1_bit_1 -b1_bit0  b1_bit1 -b1_bit2 -b1_bit3 -b1_bit4 -b1_bit5  b1_bit6 -b1_bit7 -b1_bit8  b1_bit9 -b1_bit10 -b1_bit11 -b1_bit12 -b2_bit_7  b2_bit_6 -b2_bit_5  b2_bit_4 -b2_bit_3 -b2_bit_2  b2_bit_1  b2_bit0 -b2_bit1  b2_bit2  b2_bit3 -b2_bit4 -b2_bit5 -b2_bit6 -b2_bit7 -b2_bit8  b2_bit9 -b2_bit10  b2_bit11 -b2_bit12  b3_bit_7 -b3_bit_6 -b3_bit_5 -b3_bit_4  b3_bit_3 -b3_bit_2  b3_bit_1 -b3_bit0 -b3_bit1 -b3_bit2 -b3_bit3  b3_bit4 -b3_bit5 -b3_bit6 -b3_bit7  b3_bit8 -b3_bit9 -b3_bit10 -b3_bit11 -b3_bit12 -b4_bit_7 -b4_bit_6 -b4_bit_5 -b4_bit_4 -b4_bit_3 -b4_bit_2  b4_bit_1 -b4_bit0 -b4_bit1 -b4_bit2 -b4_bit3 -b4_bit4  b4_bit5 -b4_bit6 -b4_bit7 -b4_bit8 -b4_bit9 -b4_bit10 -b4_bit11 -b4_bit12 -b5_bit_7 -b5_bit_6 -b5_bit_5 -b5_bit_4 -b5_bit_3 -b5_bit_2 -b5_bit_1 -b5_bit0 -b5_bit1 -b5_bit2 -b5_bit3 -b5_bit4 -b5_bit5 -b5_bit6 -b5_bit7 -b5_bit8 -b5_bit9 -b5_bit10 -b5_bit11 -b5_bit12 -b6_bit_7 -b6_bit_6 -b6_bit_5 -b6_bit_4 -b6_bit_3 -b6_bit_2 -b6_bit_1 -b6_bit0 -b6_bit1 -b6_bit2 -b6_bit3 -b6_bit4  b6_bit5 -b6_bit6 -b6_bit7  b6_bit8 -b6_bit9 -b6_bit10 -b6_bit11 -b6_bit12  b7_bit_7  b7_bit_6  b7_bit_5 -b7_bit_4  b7_bit_3  b7_bit_2  b7_bit_1  b7_bit0  b7_bit1 -b7_bit2 -b7_bit3 -b7_bit4  b7_bit5 -b7_bit6  b7_bit7 -b7_bit8 -b7_bit9  b7_bit10 -b7_bit11 -b7_bit12  b8_bit_7 -b8_bit_6  b8_bit_5 -b8_bit_4 -b8_bit_3  b8_bit_2  b8_bit_1  b8_bit0 -b8_bit1 -b8_bit2  b8_bit3 -b8_bit4 -b8_bit5  b8_bit6  b8_bit7  b8_bit8  b8_bit9  b8_bit10  b8_bit11  b8_bit12 -b9_bit_7 -b9_bit_6 -b9_bit_5 -b9_bit_4 -b9_bit_3 -b9_bit_2 -b9_bit_1 -b9_bit0 -b9_bit1 -b9_bit2 -b9_bit3 -b9_bit4 -b9_bit5  b9_bit6 -b9_bit7 -b9_bit8 -b9_bit9 -b9_bit10 -b9_bit11  b9_bit12 -b10_bit_7 -b10_bit_6 -b10_bit_5 -b10_bit_4 -b10_bit_3 -b10_bit_2 -b10_bit_1 -b10_bit0 -b10_bit1 -b10_bit2 -b10_bit3 -b10_bit4 -b10_bit5 -b10_bit6 -b10_bit7 -b10_bit8 -b10_bit9 -b10_bit10 -b10_bit11 -b10_bit12 -b11_bit_7 -b11_bit_6  b11_bit_5  b11_bit_4 -b11_bit_3  b11_bit_2 -b11_bit_1  b11_bit0 -b11_bit1 -b11_bit2  b11_bit3 -b11_bit4 -b11_bit5  b11_bit6  b11_bit7  b11_bit8 -b11_bit9  b11_bit10 -b11_bit11 -b11_bit12 -b12_bit_7  b12_bit_6 -b12_bit_5  b12_bit_4 -b12_bit_3 -b12_bit_2 -b12_bit_1 -b12_bit0 -b12_bit1 -b12_bit2  b12_bit3 -b12_bit4 -b12_bit5 -b12_bit6  b12_bit7 -b12_bit8 -b12_bit9 -b12_bit10 -b12_bit11 -b12_bit12 -b13_bit_7 -b13_bit_6 -b13_bit_5 -b13_bit_4 -b13_bit_3 -b13_bit_2 -b13_bit_1 -b13_bit0 -b13_bit1 -b13_bit2 -b13_bit3 -b13_bit4 -b13_bit5 -b13_bit6 -b13_bit7 -b13_bit8 -b13_bit9 -b13_bit10 -b13_bit11 -b13_bit12 -b14_bit_7 -b14_bit_6 -b14_bit_5 -b14_bit_4 -b14_bit_3 -b14_bit_2 -b14_bit_1 -b14_bit0 -b14_bit1 -b14_bit2 -b14_bit3 -b14_bit4 -b14_bit5 -b14_bit6 -b14_bit7 -b14_bit8 -b14_bit9 -b14_bit10 -b14_bit11 -b14_bit12 -b15_bit_7 -b15_bit_6 -b15_bit_5 -b15_bit_4 -b15_bit_3 -b15_bit_2 -b15_bit_1 -b15_bit0 -b15_bit1 -b15_bit2 -b15_bit3 -b15_bit4 -b15_bit5 -b15_bit6 -b15_bit7 -b15_bit8 -b15_bit9 -b15_bit10 -b15_bit11 -b15_bit12 -b16_bit_7  b16_bit_6 -b16_bit_5 -b16_bit_4  b16_bit_3 -b16_bit_2 -b16_bit_1 -b16_bit0  b16_bit1 -b16_bit2 -b16_bit3 -b16_bit4  b16_bit5 -b16_bit6 -b16_bit7  b16_bit8 -b16_bit9 -b16_bit10 -b16_bit11 -b16_bit12  c1_bit0  c2_bit0  c3_bit0  c4_bit0  c5_bit0 -c6_bit0  c7_bit0  c8_bit0 -c9_bit0  c10_bit0  c11_bit0  c12_bit0  c13_bit0  c14_bit0 -c15_bit0 -c16_bit0 -f1_bit_7  f1_bit_6 -f1_bit_5  f1_bit_4  f1_bit_3  f1_bit_2 -f1_bit_1  f1_bit0 -f1_bit1  f1_bit2  f1_bit3 -f1_bit4  f1_bit5  f1_bit6  f1_bit7  f1_bit8  f1_bit9 -f1_bit10  f1_bit11 -f1_bit12  f10_bit_7 -f10_bit_6  f10_bit_5 -f10_bit_4  f10_bit_3 -f10_bit_2 -f10_bit_1 -f10_bit0 -f10_bit1 -f10_bit2  f10_bit3  f10_bit4 -f10_bit5  f10_bit6  f10_bit7  f10_bit8  f10_bit9  f10_bit10 -f10_bit11 -f10_bit12 -f11_bit_7  f11_bit_6  f11_bit_5  f11_bit_4  f11_bit_3  f11_bit_2  f11_bit_1 -f11_bit0  f11_bit1 -f11_bit2  f11_bit3  f11_bit4  f11_bit5  f11_bit6 -f11_bit7 -f11_bit8  f11_bit9 -f11_bit10 -f11_bit11 -f11_bit12  f12_bit_7  f12_bit_6  f12_bit_5 -f12_bit_4  f12_bit_3 -f12_bit_2  f12_bit_1  f12_bit0  f12_bit1  f12_bit2  f12_bit3  f12_bit4 -f12_bit5 -f12_bit6  f12_bit7 -f12_bit8 -f12_bit9 -f12_bit10  f12_bit11 -f12_bit12  f13_bit_7  f13_bit_6  f13_bit_5  f13_bit_4  f13_bit_3  f13_bit_2  f13_bit_1  f13_bit0  f13_bit1  f13_bit2  f13_bit3  f13_bit4 -f13_bit5  f13_bit6 -f13_bit7  f13_bit8 -f13_bit9 -f13_bit10  f13_bit11 -f13_bit12  f14_bit_7  f14_bit_6 -f14_bit_5  f14_bit_4  f14_bit_3  f14_bit_2 -f14_bit_1  f14_bit0 -f14_bit1 -f14_bit2  f14_bit3  f14_bit4  f14_bit5  f14_bit6 -f14_bit7 -f14_bit8 -f14_bit9 -f14_bit10  f14_bit11 -f14_bit12 -f16_bit_7 -f16_bit_6 -f16_bit_5 -f16_bit_4 -f16_bit_3  f16_bit_2 -f16_bit_1 -f16_bit0  f16_bit1 -f16_bit2 -f16_bit3 -f16_bit4 -f16_bit5 -f16_bit6 -f16_bit7  f16_bit8 -f16_bit9 -f16_bit10 -f16_bit11 -f16_bit12  f2_bit_7  f2_bit_6  f2_bit_5  f2_bit_4  f2_bit_3  f2_bit_2  f2_bit_1  f2_bit0  f2_bit1  f2_bit2 -f2_bit3  f2_bit4  f2_bit5  f2_bit6 -f2_bit7  f2_bit8  f2_bit9  f2_bit10  f2_bit11  f2_bit12  f3_bit_7  f3_bit_6  f3_bit_5  f3_bit_4  f3_bit_3 -f3_bit_2 -f3_bit_1  f3_bit0  f3_bit1  f3_bit2  f3_bit3  f3_bit4  f3_bit5 -f3_bit6  f3_bit7  f3_bit8  f3_bit9  f3_bit10 -f3_bit11  f3_bit12  f4_bit_7 -f4_bit_6  f4_bit_5  f4_bit_4 -f4_bit_3 -f4_bit_2  f4_bit_1 -f4_bit0  f4_bit1  f4_bit2  f4_bit3 -f4_bit4 -f4_bit5  f4_bit6  f4_bit7  f4_bit8  f4_bit9 -f4_bit10  f4_bit11 -f4_bit12  f5_bit_7 -f5_bit_6  f5_bit_5  f5_bit_4  f5_bit_3  f5_bit_2 -f5_bit_1  f5_bit0  f5_bit1 -f5_bit2  f5_bit3 -f5_bit4 -f5_bit5  f5_bit6  f5_bit7  f5_bit8  f5_bit9  f5_bit10  f5_bit11  f5_bit12  f6_bit_7  f6_bit_6  f6_bit_5 -f6_bit_4  f6_bit_3  f6_bit_2  f6_bit_1  f6_bit0 -f6_bit1  f6_bit2  f6_bit3 -f6_bit4 -f6_bit5  f6_bit6  f6_bit7 -f6_bit8 -f6_bit9 -f6_bit10 -f6_bit11 -f6_bit12  f7_bit_7  f7_bit_6 -f7_bit_5  f7_bit_4  f7_bit_3 -f7_bit_2  f7_bit_1 -f7_bit0  f7_bit1 -f7_bit2  f7_bit3  f7_bit4  f7_bit5 -f7_bit6  f7_bit7 -f7_bit8  f7_bit9  f7_bit10  f7_bit11  f7_bit12 -f9_bit_7  f9_bit_6  f9_bit_5  f9_bit_4 -f9_bit_3 -f9_bit_2  f9_bit_1  f9_bit0  f9_bit1  f9_bit2  f9_bit3  f9_bit4  f9_bit5  f9_bit6 -f9_bit7  f9_bit8  f9_bit9  f9_bit10  f9_bit11 -f9_bit12 
s OPTIMUM FOUND
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.97 0.99 2/54 29578
Raw data (stat): 29578 (runsolver) R 29577 23514 23513 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 800929470 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+3.50008 s]
Raw data (loadavg): 1.00 0.98 1.00 1/53 29591
Raw data (stat): 29578 (runsolver) R 29577 23514 23513 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 800929470 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 0

Child status: 30
Real time (s): 3.49984
CPU time (s): 3.13352
CPU user time (s): 2.73758
CPU system time (s): 0.395939
CPU usage (%): 89.5332
Max. virtual memory (Kb): 864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	600071642988554
#### END VERIFIER DATA ####