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-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-A1C1S1.opb
MD5SUM	4ceb0b03b7e8a29fb578fb77c2b349b0
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	37632
Biggest coefficient in the objective function	31125091123200
Number of bits for the biggest coefficient in the objective function	45
Sum of the numbers in the objective function	14624065344515792
Number of bits of the sum of numbers in the objective function	54
Biggest number in a constraint	31125091123200
Number of bits of the biggest number in a constraint	45
Biggest sum of numbers in a constraint	14624065344515792
Number of bits of the biggest sum of numbers	54
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.925858
Number of variables	103872
Total number of constraints	3504
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	192
Number of constraints which are nor clauses,nor cardinality constraints	3312
Minimum length of a constraint	1
Maximum length of a constraint	725
Trace number 27948

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-25 00:00:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14862 boxname=wulflinc24 idbench=1144 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  4ceb0b03b7e8a29fb578fb77c2b349b0  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-A1C1S1.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-A1C1S1.opb
IDLAUNCH: 14862
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        812332 kB
Buffers:          2436 kB
Cached:         195912 kB
SwapCached:        620 kB
Active:          36884 kB
Inactive:       164408 kB
HighTotal:      131008 kB
HighFree:        18872 kB
LowTotal:       903652 kB
LowFree:        793460 kB
SwapTotal:     2097892 kB
SwapFree:      2096776 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6300 kB
Slab:            15164 kB
Committed_AS:    64828 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 00:06:35 (client local time) WITH STATUS 0 IN 388.246 SECONDS
stats: 14862 7 388.246 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c ERROR Parsing file!!!
c ERROR parsing line: -32*x__31101_bit_10 -64*x__31101_bit_9 -128*x__31101_bit_8 -256*x__31101_bit_7 -512*x__31101_bit_6 -1024*x__31101_bit_5 -2048*x__31101_bit_4 -4096*x__31101_bit_3 -8192*x__31101_bit_2 -16384*x__31101_bit_1 -32768*x__31101_bit0 -65536*x__31101_bit1 -131072*x__31101_bit2 -262144*x__31101_bit3 -524288*x__31101_bit4 -1048576*x__31101_bit5 -2097152*x__31101_bit6 -4194304*x__31101_bit7 -8388608*x__31101_bit8 -16777216*x__31101_bit9 -33554432*x__31101_bit10 -67108864*x__31101_bit11 -134217728*x__31101_bit12 -268435456*x__31101_bit13 -536870912*x__31101_bit14 -1073741824*x__31101_bit15 -2147483648*x__31101_bit16 -4294967296*x__31101_bit17 -8589934592*x__31101_bit18 -17179869184*x__31101_bit19 -4*x__32101_bit_10 -8*x__32101_bit_9 -16*x__32101_bit_8 -32*x__32101_bit_7 -64*x__32101_bit_6 -128*x__32101_bit_5 -256*x__32101_bit_4 -512*x__32101_bit_3 -1024*x__32101_bit_2 -2048*x__32101_bit_1 -4096*x__32101_bit0 -8192*x__32101_bit1 -16384*x__32101_bit2 -32768*x__32101_bit3 -65536*x__32101_bit4 -131072*x__32101_bit5 -262144*x__32101_bit6 -524288*x__32101_bit7 -1048576*x__32101_bit8 -2097152*x__32101_bit9 -4194304*x__32101_bit10 -8388608*x__32101_bit11 -16777216*x__32101_bit12 -33554432*x__32101_bit13 -67108864*x__32101_bit14 -134217728*x__32101_bit15 -268435456*x__32101_bit16 -536870912*x__32101_bit17 -1073741824*x__32101_bit18 -2147483648*x__32101_bit19 -24*x__35101_bit_10 -48*x__35101_bit_9 -96*x__35101_bit_8 -192*x__35101_bit_7 -384*x__35101_bit_6 -768*x__35101_bit_5 -1536*x__35101_bit_4 -3072*x__35101_bit_3 -6144*x__35101_bit_2 -12288*x__35101_bit_1 -24576*x__35101_bit0 -49152*x__35101_bit1 -98304*x__35101_bit2 -196608*x__35101_bit3 -393216*x__35101_bit4 -786432*x__35101_bit5 -1572864*x__35101_bit6 -3145728*x__35101_bit7 -6291456*x__35101_bit8 -12582912*x__35101_bit9 -25165824*x__35101_bit10 -50331648*x__35101_bit11 -100663296*x__35101_bit12 -201326592*x__35101_bit13 -402653184*x__35101_bit14 -805306368*x__35101_bit15 -1610612736*x__35101_bit16 -3221225472*x__35101_bit17 -6442450944*x__35101_bit18 -12884901888*x__35101_bit19 -4*x__36101_bit_10 -8*x__36101_bit_9 -16*x__36101_bit_8 -32*x__36101_bit_7 -64*x__36101_bit_6 -128*x__36101_bit_5 -256*x__36101_bit_4 -512*x__36101_bit_3 -1024*x__36101_bit_2 -2048*x__36101_bit_1 -4096*x__36101_bit0 -8192*x__36101_bit1 -16384*x__36101_bit2 -32768*x__36101_bit3 -65536*x__36101_bit4 -131072*x__36101_bit5 -262144*x__36101_bit6 -524288*x__36101_bit7 -1048576*x__36101_bit8 -2097152*x__36101_bit9 -4194304*x__36101_bit10 -8388608*x__36101_bit11 -16777216*x__36101_bit12 -33554432*x__36101_bit13 -67108864*x__36101_bit14 -134217728*x__36101_bit15 -268435456*x__36101_bit16 -536870912*x__36101_bit17 -1073741824*x__36101_bit18 -2147483648*x__36101_bit19 -32*x__39101_bit_10 -64*x__39101_bit_9 -128*x__39101_bit_8 -256*x__39101_bit_7 -512*x__39101_bit_6 -1024*x__39101_bit_5 -2048*x__39101_bit_4 -4096*x__39101_bit_3 -8192*x__39101_bit_2 -16384*x__39101_bit_1 -32768*x__39101_bit0 -65536*x__39101_bit1 -131072*x__39101_bit2 -262144*x__39101_bit3 -524288*x__39101_bit4 -1048576*x__39101_bit5 -2097152*x__39101_bit6 -4194304*x__39101_bit7 -8388608*x__39101_bit8 -16777216*x__39101_bit9 -33554432*x__39101_bit10 -67108864*x__39101_bit11 -134217728*x__39101_bit12 -268435456*x__39101_bit13 -536870912*x__39101_bit14 -1073741824*x__39101_bit15 -2147483648*x__39101_bit16 -4294967296*x__39101_bit17 -8589934592*x__39101_bit18 -17179869184*x__39101_bit19 -8*x__40101_bit_10 -16*x__40101_bit_9 -32*x__40101_bit_8 -64*x__40101_bit_7 -128*x__40101_bit_6 -256*x__40101_bit_5 -512*x__40101_bit_4 -1024*x__40101_bit_3 -2048*x__40101_bit_2 -4096*x__40101_bit_1 -8192*x__40101_bit0 -16384*x__40101_bit1 -32768*x__40101_bit2 -65536*x__40101_bit3 -131072*x__40101_bit4 -262144*x__40101_bit5 -524288*x__40101_bit6 -1048576*x__40101_bit7 -2097152*x__40101_bit8 -4194304*x__40101_bit9 -8388608*x__40101_bit10 -16777216*x__40101_bit11 -33554432*x__40101_bit12 -67108864*x__40101_bit13 -134217728*x__40101_bit14 -268435456*x__40101_bit15 -536870912*x__40101_bit16 -1073741824*x__40101_bit17 -2147483648*x__40101_bit18 -4294967296*x__40101_bit19 -24*x__43101_bit_10 -48*x__43101_bit_9 -96*x__43101_bit_8 -192*x__43101_bit_7 -384*x__43101_bit_6 -768*x__43101_bit_5 -1536*x__43101_bit_4 -3072*x__43101_bit_3 -6144*x__43101_bit_2 -12288*x__43101_bit_1 -24576*x__43101_bit0 -49152*x__43101_bit1 -98304*x__43101_bit2 -196608*x__43101_bit3 -393216*x__43101_bit4 -786432*x__43101_bit5 -1572864*x__43101_bit6 -3145728*x__43101_bit7 -6291456*x__43101_bit8 -12582912*x__43101_bit9 -25165824*x__43101_bit10 -50331648*x__43101_bit11 -100663296*x__43101_bit12 -201326592*x__43101_bit13 -402653184*x__43101_bit14 -805306368*x__43101_bit15 -1610612736*x__43101_bit16 -3221225472*x__43101_bit17 -6442450944*x__43101_bit18 -12884901888*x__43101_bit19 -8*x__44101_bit_10 -16*x__44101_bit_9 -32*x__44101_bit_8 -64*x__44101_bit_7 -128*x__44101_bit_6 -256*x__44101_bit_5 -512*x__44101_bit_4 -1024*x__44101_bit_3 -2048*x__44101_bit_2 -4096*x__44101_bit_1 -8192*x__44101_bit0 -16384*x__44101_bit1 -32768*x__44101_bit2 -65536*x__44101_bit3 -131072*x__44101_bit4 -262144*x__44101_bit5 -524288*x__44101_bit6 -1048576*x__44101_bit7 -2097152*x__44101_bit8 -4194304*x__44101_bit9 -8388608*x__44101_bit10 -16777216*x__44101_bit11 -33554432*x__44101_bit12 -67108864*x__44101_bit13 -134217728*x__44101_bit14 -268435456*x__44101_bit15 -536870912*x__44101_bit16 -1073741824*x__44101_bit17 -2147483648*x__44101_bit18 -4294967296*x__44101_bit19 -32*x__47101_bit_10 -64*x__47101_bit_9 -128*x__47101_bit_8 -256*x__47101_bit_7 -512*x__47101_bit_6 -1024*x__47101_bit_5 -2048*x__47101_bit_4 -4096*x__47101_bit_3 -8192*x__47101_bit_2 -16384*x__47101_bit_1 -32768*x__47101_bit0 -65536*x__47101_bit1 -131072*x__47101_bit2 -262144*x__47101_bit3 -524288*x__47101_bit4 -1048576*x__47101_bit5 -2097152*x__47101_bit6 -4194304*x__47101_bit7 -8388608*x__47101_bit8 -16777216*x__47101_bit9 -33554432*x__47101_bit10 -67108864*x__47101_bit11 -134217728*x__47101_bit12 -268435456*x__47101_bit13 -536870912*x__47101_bit14 -1073741824*x__47101_bit15 -2147483648*x__47101_bit16 -4294967296*x__47101_bit17 -8589934592*x__47101_bit18 -17179869184*x__47101_bit19 -6*x__48101_bit_10 -12*x__48101_bit_9 -24*x__48101_bit_8 -48*x__48101_bit_7 -96*x__48101_bit_6 -192*x__48101_bit_5 -384*x__48101_bit_4 -768*x__48101_bit_3 -1536*x__48101_bit_2 -3072*x__48101_bit_1 -6144*x__48101_bit0 -12288*x__48101_bit1 -24576*x__48101_bit2 -49152*x__48101_bit3 -98304*x__48101_bit4 -196608*x__48101_bit5 -393216*x__48101_bit6 -786432*x__48101_bit7 -1572864*x__48101_bit8 -3145728*x__48101_bit9 -6291456*x__48101_bit10 -12582912*x__48101_bit11 -25165824*x__48101_bit12 -50331648*x__48101_bit13 -100663296*x__48101_bit14 -201326592*x__48101_bit15 -402653184*x__48101_bit16 -805306368*x__48101_bit17 -1610612736*x__48101_bit18 -3221225472*x__48101_bit19 -24*x__51101_bit_10 -48*x__51101_bit_9 -96*x__51101_bit_8 -192*x__51101_bit_7 -384*x__51101_bit_6 -768*x__51101_bit_5 -1536*x__51101_bit_4 -3072*x__51101_bit_3 -6144*x__51101_bit_2 -12288*x__51101_bit_1 -24576*x__51101_bit0 -49152*x__51101_bit1 -98304*x__51101_bit2 -196608*x__51101_bit3 -393216*x__51101_bit4 -786432*x__51101_bit5 -1572864*x__51101_bit6 -3145728*x__51101_bit7 -6291456*x__51101_bit8 -12582912*x__51101_bit9 -25165824*x__51101_bit10 -50331648*x__51101_bit11 -100663296*x__51101_bit12 -201326592*x__51101_bit13 -402653184*x__51101_bit14 -805306368*x__51101_bit15 -1610612736*x__51101_bit16 -3221225472*x__51101_bit17 -6442450944*x__51101_bit18 -12884901888*x__51101_bit19 -6*x__52101_bit_10 -12*x__52101_bit_9 -24*x__52101_bit_8 -48*x__52101_bit_7 -96*x__52101_bit_6 -192*x__52101_bit_5 -384*x__52101_bit_4 -768*x__52101_bit_3 -1536*x__52101_bit_2 -3072*x__52101_bit_1 -6144*x__52101_bit0 -12288*x__52101_bit1 -24576*x__52101_bit2 -49152*x__52101_bit3 -98304*x__52101_bit4 -196608*x__52101_bit5 -393216*x__52101_bit6 -786432*x__52101_bit7 -1572864*x__52101_bit8 -3145728*x__52101_bit9 -6291456*x__52101_bit10 -12582912*x__52101_bit11 -25165824*x__52101_bit12 -50331648*x__52101_bit13 -100663296*x__52101_bit14 -201326592*x__52101_bit15 -402653184*x__52101_bit16 -805306368*x__52101_bit17 -1610612736*x__52101_bit18 -3221225472*x__52101_bit19 -10*x__55101_bit_10 -20*x__55101_bit_9 -40*x__55101_bit_8 -80*x__55101_bit_7 -160*x__55101_bit_6 -320*x__55101_bit_5 -640*x__55101_bit_4 -1280*x__55101_bit_3 -2560*x__55101_bit_2 -5120*x__55101_bit_1 -10240*x__55101_bit0 -20480*x__55101_bit1 -40960*x__55101_bit2 -81920*x__55101_bit3 -163840*x__55101_bit4 -327680*x__55101_bit5 -655360*x__55101_bit6 -1310720*x__55101_bit7 -2621440*x__55101_bit8 -5242880*x__55101_bit9 -10485760*x__55101_bit10 -20971520*x__55101_bit11 -41943040*x__55101_bit12 -83886080*x__55101_bit13 -167772160*x__55101_bit14 -335544320*x__55101_bit15 -671088640*x__55101_bit16 -1342177280*x__55101_bit17 -2684354560*x__55101_bit18 -5368709120*x__55101_bit19 -8*x__57101_bit_10 -16*x__57101_bit_9 -32*x__57101_bit_8 -64*x__57101_bit_7 -128*x__57101_bit_6 -256*x__57101_bit_5 -512*x__57101_bit_4 -1024*x__57101_bit_3 -2048*x__57101_bit_2 -4096*x__57101_bit_1 -8192*x__57101_bit0 -16384*x__57101_bit1 -32768*x__57101_bit2 -65536*x__57101_bit3 -131072*x__57101_bit4 -262144*x__57101_bit5 -524288*x__57101_bit6 -1048576*x__57101_bit7 -2097152*x__57101_bit8 -4194304*x__57101_bit9 -8388608*x__57101_bit10 -16777216*x__57101_bit11 -33554432*x__57101_bit12 -67108864*x__57101_bit13 -134217728*x__57101_bit14 -268435456*x__57101_bit15 -536870912*x__57101_bit16 -1073741824*x__57101_bit17 -2147483648*x__57101_bit18 -4294967296*x__57101_bit19 -20*x__59101_bit_10 -40*x__59101_bit_9 -80*x__59101_bit_8 -160*x__59101_bit_7 -320*x__59101_bit_6 -640*x__59101_bit_5 -1280*x__59101_bit_4 -2560*x__59101_bit_3 -5120*x__59101_bit_2 -10240*x__59101_bit_1 -20480*x__59101_bit0 -40960*x__59101_bit1 -81920*x__59101_bit2 -163840*x__59101_bit3 -327680*x__59101_bit4 -655360*x__59101_bit5 -1310720*x__59101_bit6 -2621440*x__59101_bit7 -5242880*x__59101_bit8 -10485760*x__59101_bit9 -20971520*x__59101_bit10 -41943040*x__59101_bit11 -83886080*x__59101_bit12 -167772160*x__59101_bit13 -335544320*x__59101_bit14 -671088640*x__59101_bit15 -1342177280*x__59101_bit16 -2684354560*x__59101_bit17 -5368709120*x__59101_bit18 -10737418240*x__59101_bit19 -16*x__61101_bit_10 -32*x__61101_bit_9 -64*x__61101_bit_8 -128*x__61101_bit_7 -256*x__61101_bit_6 -512*x__61101_bit_5 -1024*x__61101_bit_4 -2048*x__61101_bit_3 -4096*x__61101_bit_2 -8192*x__61101_bit_1 -16384*x__61101_bit0 -32768*x__61101_bit1 -65536*x__61101_bit2 -131072*x__61101_bit3 -262144*x__61101_bit4 -524288*x__61101_bit5 -1048576*x__61101_bit6 -2097152*x__61101_bit7 -4194304*x__61101_bit8 -8388608*x__61101_bit9 -16777216*x__61101_bit10 -33554432*x__61101_bit11 -67108864*x__61101_bit12 -134217728*x__61101_bit13 -268435456*x__61101_bit14 -536870912*x__61101_bit15 -1073741824*x__61101_bit16 -2147483648*x__61101_bit17 -4294967296*x__61101_bit18 -8589934592*x__61101_bit19 -15*x__63101_bit_10 -30*x__63101_bit_9 -60*x__63101_bit_8 -120*x__63101_bit_7 -240*x__63101_bit_6 -480*x__63101_bit_5 -960*x__63101_bit_4 -1920*x__63101_bit_3 -3840*x__63101_bit_2 -7680*x__63101_bit_1 -15360*x__63101_bit0 -30720*x__63101_bit1 -61440*x__63101_bit2 -122880*x__63101_bit3 -245760*x__63101_bit4 -491520*x__63101_bit5 -983040*x__63101_bit6 -1966080*x__63101_bit7 -3932160*x__63101_bit8 -7864320*x__63101_bit9 -15728640*x__63101_bit10 -31457280*x__63101_bit11 -62914560*x__63101_bit12 -125829120*x__63101_bit13 -251658240*x__63101_bit14 -503316480*x__63101_bit15 -1006632960*x__63101_bit16 -2013265920*x__63101_bit17 -4026531840*x__63101_bit18 -8053063680*x__63101_bit19 -12*x__65101_bit_10 -24*x__65101_bit_9 -48*x__65101_bit_8 -96*x__65101_bit_7 -192*x__65101_bit_6 -384*x__65101_bit_5 -768*x__65101_bit_4 -1536*x__65101_bit_3 -3072*x__65101_bit_2 -6144*x__65101_bit_1 -12288*x__65101_bit0 -24576*x__65101_bit1 -49152*x__65101_bit2 -98304*x__65101_bit3 -196608*x__65101_bit4 -393216*x__65101_bit5 -786432*x__65101_bit6 -1572864*x__65101_bit7 -3145728*x__65101_bit8 -6291456*x__65101_bit9 -12582912*x__65101_bit10 -25165824*x__65101_bit11 -50331648*x__65101_bit12 -100663296*x__65101_bit13 -201326592*x__65101_bit14 -402653184*x__65101_bit15 -805306368*x__65101_bit16 -1610612736*x__65101_bit17 -3221225472*x__65101_bit18 -6442450944*x__65101_bit19 -36*x__73101_bit_10 -72*x__73101_bit_9 -144*x__73101_bit_8 -288*x__73101_bit_7 -576*x__73101_bit_6 -1152*x__73101_bit_5 -2304*x__73101_bit_4 -4608*x__73101_bit_3 -9216*x__73101_bit_2 -18432*x__73101_bit_1 -36864*x__73101_bit0 -73728*x__73101_bit1 -147456*x__73101_bit2 -294912*x__73101_bit3 -589824*x__73101_bit4 -1179648*x__73101_bit5 -2359296*x__73101_bit6 -4718592*x__73101_bit7 -9437184*x__73101_bit8 -18874368*x__73101_bit9 -37748736*x__73101_bit10 -75497472*x__73101_bit11 -150994944*x__73101_bit12 -301989888*x__73101_bit13 -603979776*x__73101_bit14 -1207959552*x__73101_bit15 -2415919104*x__73101_bit16 -4831838208*x__73101_bit17 -9663676416*x__73101_bit18 -19327352832*x__73101_bit19 -30*x__74101_bit_10 -60*x__74101_bit_9 -120*x__74101_bit_8 -240*x__74101_bit_7 -480*x__74101_bit_6 -960*x__74101_bit_5 -1920*x__74101_bit_4 -3840*x__74101_bit_3 -7680*x__74101_bit_2 -15360*x__74101_bit_1 -30720*x__74101_bit0 -61440*x__74101_bit1 -122880*x__74101_bit2 -245760*x__74101_bit3 -491520*x__74101_bit4 -983040*x__74101_bit5 -1966080*x__74101_bit6 -3932160*x__74101_bit7 -7864320*x__74101_bit8 -15728640*x__74101_bit9 -31457280*x__74101_bit10 -62914560*x__74101_bit11 -125829120*x__74101_bit12 -251658240*x__74101_bit13 -503316480*x__74101_bit14 -1006632960*x__74101_bit15 -2013265920*x__74101_bit16 -4026531840*x__74101_bit17 -8053063680*x__74101_bit18 -16106127360*x__74101_bit19 -72*x__75101_bit_10 -144*x__75101_bit_9 -288*x__75101_bit_8 -576*x__75101_bit_7 -1152*x__75101_bit_6 -2304*x__75101_bit_5 -4608*x__75101_bit_4 -9216*x__75101_bit_3 -18432*x__75101_bit_2 -36864*x__75101_bit_1 -73728*x__75101_bit0 -147456*x__75101_bit1 -294912*x__75101_bit2 -589824*x__75101_bit3 -1179648*x__75101_bit4 -2359296*x__75101_bit5 -4718592*x__75101_bit6 -9437184*x__75101_bit7 -18874368*x__75101_bit8 -37748736*x__75101_bit9 -75497472*x__75101_bit10 -150994944*x__75101_bit11 -301989888*x__75101_bit12 -603979776*x__75101_bit13 -1207959552*x__75101_bit14 -2415919104*x__75101_bit15 -4831838208*x__75101_bit16 -9663676416*x__75101_bit17 -19327352832*x__75101_bit18 -38654705664*x__75101_bit19 -60*x__76101_bit_10 -120*x__76101_bit_9 -240*x__76101_bit_8 -480*x__76101_bit_7 -960*x__76101_bit_6 -1920*x__76101_bit_5 -3840*x__76101_bit_4 -7680*x__76101_bit_3 -15360*x__76101_bit_2 -30720*x__76101_bit_1 -61440*x__76101_bit0 -122880*x__76101_bit1 -245760*x__76101_bit2 -491520*x__76101_bit3 -983040*x__76101_bit4 -1966080*x__76101_bit5 -3932160*x__76101_bit6 -7864320*x__76101_bit7 -15728640*x__76101_bit8 -31457280*x__76101_bit9 -62914560*x__76101_bit10 -125829120*x__76101_bit11 -251658240*x__76101_bit12 -503316480*x__76101_bit13 -1006632960*x__76101_bit14 -2013265920*x__76101_bit15 -4026531840*x__76101_bit16 -8053063680*x__76101_bit17 -16106127360*x__76101_bit18 -32212254720*x__76101_bit19 -54*x__77101_bit_10 -108*x__77101_bit_9 -216*x__77101_bit_8 -432*x__77101_bit_7 -864*x__77101_bit_6 -1728*x__77101_bit_5 -3456*x__77101_bit_4 -6912*x__77101_bit_3 -13824*x__77101_bit_2 -27648*x__77101_bit_1 -55296*x__77101_bit0 -110592*x__77101_bit1 -221184*x__77101_bit2 -442368*x__77101_bit3 -884736*x__77101_bit4 -1769472*x__77101_bit5 -3538944*x__77101_bit6 -7077888*x__77101_bit7 -14155776*x__77101_bit8 -28311552*x__77101_bit9 -56623104*x__77101_bit10 -113246208*x__77101_bit11 -226492416*x__77101_bit12 -452984832*x__77101_bit13 -905969664*x__77101_bit14 -1811939328*x__77101_bit15 -3623878656*x__77101_bit16 -7247757312*x__77101_bit17 -14495514624*x__77101_bit18 -28991029248*x__77101_bit19 -45*x__78101_bit_10 -90*x__78101_bit_9 -180*x__78101_bit_8 -360*x__78101_bit_7 -720*x__78101_bit_6 -1440*x__78101_bit_5 -2880*x__78101_bit_4 -5760*x__78101_bit_3 -11520*x__78101_bit_2 -23040*x__78101_bit_1 -46080*x__78101_bit0 -92160*x__78101_bit1 -184320*x__78101_bit2 -368640*x__78101_bit3 -737280*x__78101_bit4 -1474560*x__78101_bit5 -2949120*x__78101_bit6 -5898240*x__78101_bit7 -11796480*x__78101_bit8 -23592960*x__78101_bit9 -47185920*x__78101_bit10 -94371840*x__78101_bit11 -188743680*x__78101_bit12 -377487360*x__78101_bit13 -754974720*x__78101_bit14 -1509949440*x__78101_bit15 -3019898880*x__78101_bit16 -6039797760*x__78101_bit17 -12079595520*x__78101_bit18 -24159191040*x__78101_bit19 >= -8192000;
c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-A1C1S1.opb
s UNKNOWN
c Exit Code: 0
c Total time: 388.198 s
#### 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
Raw data (loadavg): 0.79 0.92 0.90 3/57 10285
Raw data (stat): 10285 (runsolver) R 10284 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834387608 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 10303
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 840 0 0 0 994 2 0 0 25 0 1 0 834387608 16232448 818 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 3963 818 1111 63 0 3900 0
vsize: 15852
[startup+20.0006 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 10303
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 1144 0 0 0 1994 3 0 0 25 0 1 0 834387608 17534976 1122 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4281 1122 1111 63 0 4218 0
vsize: 17124
[startup+30.0012 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 10303
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 1468 0 0 0 2993 4 0 0 25 0 1 0 834387608 18862080 1446 4294967295 134512640 134714540 3221224592 3221222820 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4605 1446 1111 63 0 4542 0
vsize: 18420
[startup+40.0016 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 10303
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 1797 0 0 0 3993 4 0 0 25 0 1 0 834387608 20180992 1775 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4927 1775 1111 63 0 4864 0
vsize: 19708
[startup+50.0016 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 10303
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 2114 0 0 0 4993 5 0 0 25 0 1 0 834387608 21508096 2092 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5251 2092 1111 63 0 5188 0
vsize: 21004
[startup+60.0013 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 10303
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 2442 0 0 0 5992 5 0 0 25 0 1 0 834387608 22855680 2420 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5580 2420 1111 63 0 5517 0
vsize: 22320
[startup+70.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 2781 0 0 0 6991 6 0 0 25 0 1 0 834387608 24203264 2759 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5909 2759 1111 63 0 5846 0
vsize: 23636
[startup+80.0027 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 3113 0 0 0 7991 7 0 0 25 0 1 0 834387608 25554944 3091 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6239 3091 1111 63 0 6176 0
vsize: 24956
[startup+90.0034 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 3444 0 0 0 8990 8 0 0 25 0 1 0 834387608 26890240 3422 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6565 3422 1111 63 0 6502 0
vsize: 26260
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 3791 0 0 0 9989 9 0 0 25 0 1 0 834387608 28381184 3769 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6929 3769 1111 63 0 6866 0
vsize: 27716
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 4138 0 0 0 10989 9 0 0 25 0 1 0 834387608 29741056 4116 4294967295 134512640 134714540 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7261 4116 1111 63 0 7198 0
vsize: 29044
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 4502 0 0 0 11988 10 0 0 25 0 1 0 834387608 31277056 4480 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7636 4480 1111 63 0 7573 0
vsize: 30544
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 4848 0 0 0 12988 11 0 0 25 0 1 0 834387608 32636928 4826 4294967295 134512640 134714540 3221224592 3221222820 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7968 4826 1111 63 0 7905 0
vsize: 31872
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 5225 0 0 0 13987 12 0 0 25 0 1 0 834387608 34291712 5203 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8372 5203 1111 63 0 8309 0
vsize: 33488
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 5579 0 0 0 14987 12 0 0 25 0 1 0 834387608 35643392 5557 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8702 5557 1111 63 0 8639 0
vsize: 34808
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 5946 0 0 0 15986 13 0 0 25 0 1 0 834387608 37150720 5924 4294967295 134512640 134714540 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9070 5924 1111 63 0 9007 0
vsize: 36280
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 6338 0 0 0 16985 14 0 0 25 0 1 0 834387608 38809600 6316 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9475 6316 1111 63 0 9412 0
vsize: 37900
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 6707 0 0 0 17985 15 0 0 25 0 1 0 834387608 40308736 6685 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9841 6685 1111 63 0 9778 0
vsize: 39364
[startup+190.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 7099 0 0 0 18985 16 0 0 25 0 1 0 834387608 41816064 7077 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10209 7077 1111 63 0 10146 0
vsize: 40836
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 7506 0 0 0 19984 17 0 0 25 0 1 0 834387608 43589632 7484 4294967295 134512640 134714540 3221224592 3221222820 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10642 7484 1111 63 0 10579 0
vsize: 42568
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 7902 0 0 0 20983 18 0 0 25 0 1 0 834387608 45096960 7880 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11010 7880 1111 63 0 10947 0
vsize: 44040
[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 8307 0 0 0 21983 18 0 0 25 0 1 0 834387608 46751744 8285 4294967295 134512640 134714540 3221224592 3221222820 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11414 8285 1111 63 0 11351 0
vsize: 45656
[startup+230.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 8744 0 0 0 22983 19 0 0 25 0 1 0 834387608 48656384 8722 4294967295 134512640 134714540 3221224592 3221222820 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11879 8722 1111 63 0 11816 0
vsize: 47516
[startup+240.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 9165 0 0 0 23982 19 0 0 25 0 1 0 834387608 50434048 9143 4294967295 134512640 134714540 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12313 9143 1111 63 0 12250 0
vsize: 49252
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 9602 0 0 0 24982 20 0 0 25 0 1 0 834387608 52207616 9580 4294967295 134512640 134714540 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12746 9580 1111 63 0 12683 0
vsize: 50984
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 10058 0 0 0 25981 21 0 0 25 0 1 0 834387608 54013952 10036 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13187 10036 1111 63 0 13124 0
vsize: 52748
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 10517 0 0 0 26980 22 0 0 25 0 1 0 834387608 55971840 10495 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13665 10495 1111 63 0 13602 0
vsize: 54660
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 11005 0 0 0 27980 23 0 0 25 0 1 0 834387608 57933824 10983 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14144 10983 1111 63 0 14081 0
vsize: 56576
[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 11498 0 0 0 28980 24 0 0 25 0 1 0 834387608 59891712 11476 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14622 11476 1111 63 0 14559 0
vsize: 58488
[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 12021 0 0 0 29979 25 0 0 25 0 1 0 834387608 62144512 11999 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15172 11999 1111 63 0 15109 0
vsize: 60688
[startup+310.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 12554 0 0 0 30978 26 0 0 25 0 1 0 834387608 64253952 12532 4294967295 134512640 134714540 3221224592 3221223248 134527930 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15687 12532 1111 63 0 15624 0
vsize: 62748
[startup+320.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 13127 0 0 0 31977 28 0 0 25 0 1 0 834387608 66658304 13105 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16274 13105 1111 63 0 16211 0
vsize: 65096
[startup+330.037 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 10305
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 13784 0 0 0 32976 30 0 0 25 0 1 0 834387608 69218304 13762 4294967295 134512640 134714540 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16899 13762 1111 63 0 16836 0
vsize: 67596
[startup+340.038 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 10307
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 14560 0 0 0 33974 32 0 0 25 0 1 0 834387608 72380416 14538 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17671 14538 1111 63 0 17608 0
vsize: 70684
[startup+350.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10307
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 15399 0 0 0 34973 33 0 0 25 0 1 0 834387608 75808768 15377 4294967295 134512640 134714540 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18508 15377 1111 63 0 18445 0
vsize: 74032
[startup+360.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10307
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 16289 0 0 0 35972 35 0 0 25 0 1 0 834387608 79572992 16267 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19427 16267 1111 63 0 19364 0
vsize: 77708
[startup+370.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10307
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 17275 0 0 0 36970 36 0 0 25 0 1 0 834387608 83816448 17253 4294967295 134512640 134714540 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20463 17253 1111 63 0 20400 0
vsize: 81852
[startup+380.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10307
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 18306 0 0 0 37968 39 0 0 25 0 1 0 834387608 88027136 18284 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21491 18284 1111 63 0 21428 0
vsize: 85964
[startup+388.216 s]
Raw data (loadavg): 1.02 0.99 0.91 1/53 10307
Raw data (stat): 10285 (bsolo_mis) R 10284 4613 4612 0 -1 0 18306 0 0 0 37968 39 0 0 25 0 1 0 834387608 88027136 18284 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21491 18284 1111 63 0 21428 0
vsize: 0

Child status: 0
Real time (s): 388.216
CPU time (s): 388.246
CPU user time (s): 387.785
CPU system time (s): 0.460929
CPU usage (%): 100.008
Max. virtual memory (Kb): 85964
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####