Some explanations

1. 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.
2. SOLVER DATA
   This is the output of the solver (stdout and stderr).
3. 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.
4. 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

Trace number 41290

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-09 09:58:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=29360 boxname=wulflinc3 idbench=1144 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  4ceb0b03b7e8a29fb578fb77c2b349b0  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-A1C1S1.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-A1C1S1.opb
IDLAUNCH: 29360
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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		: 451.190
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:        816768 kB
Buffers:         11348 kB
Cached:         185756 kB
SwapCached:        708 kB
Active:          38580 kB
Inactive:       160540 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        816516 kB
SwapTotal:     2097136 kB
SwapFree:      2095380 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5036 kB
Slab:            13048 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-09 10:05:21 (client local time) WITH STATUS 0 IN 384.135 SECONDS
stats: 29360 7 384.135 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
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/wulflinc3/normalized-mps-v2-20-10-A1C1S1.opb
s UNKNOWN
c Exit Code: 0
c Total time: 384.088 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.82 0.92 0.90 1/54 7071
Raw data (stat): 7071 (runsolver) R 7070 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 909370864 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0009 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 7071
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 962 0 0 0 994 3 0 0 25 0 1 0 909370864 16236544 882 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 3964 882 1111 63 0 3901 0
vsize: 15856
[startup+20.0011 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 7071
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 1243 0 0 0 1993 4 0 0 25 0 1 0 909370864 17272832 1163 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4217 1163 1111 63 0 4154 0
vsize: 16868
[startup+30.001 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 7071
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 1529 0 0 0 2992 5 0 0 25 0 1 0 909370864 18444288 1449 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4503 1449 1111 63 0 4440 0
vsize: 18012
[startup+40.0012 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 7071
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 1852 0 0 0 3991 6 0 0 25 0 1 0 909370864 19795968 1772 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4833 1772 1111 63 0 4770 0
vsize: 19332
[startup+50.0017 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 7071
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 2146 0 0 0 4990 7 0 0 25 0 1 0 909370864 20996096 2066 4294967295 134512640 134716908 3221224560 3221222788 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5126 2066 1111 63 0 5063 0
vsize: 20504
[startup+60.0015 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 7071
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 2456 0 0 0 5989 8 0 0 25 0 1 0 909370864 22351872 2376 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5457 2376 1111 63 0 5394 0
vsize: 21828
[startup+70.0107 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 2784 0 0 0 6982 14 0 0 25 0 1 0 909370864 23695360 2704 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5785 2704 1111 63 0 5722 0
vsize: 23140
[startup+80.0125 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 3110 0 0 0 7982 15 0 0 25 0 1 0 909370864 25051136 3030 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6116 3030 1111 63 0 6053 0
vsize: 24464
[startup+90.0119 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 3426 0 0 0 8981 16 0 0 25 0 1 0 909370864 26251264 3346 4294967295 134512640 134716908 3221224560 3221222788 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6409 3346 1111 63 0 6346 0
vsize: 25636
[startup+100.012 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 3751 0 0 0 9981 16 0 0 25 0 1 0 909370864 27574272 3671 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6732 3671 1111 63 0 6669 0
vsize: 26928
[startup+110.013 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 4090 0 0 0 10980 17 0 0 25 0 1 0 909370864 28934144 4010 4294967295 134512640 134716908 3221224560 3221222788 1077414426 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7064 4010 1111 63 0 7001 0
vsize: 28256
[startup+120.013 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 4421 0 0 0 11980 18 0 0 25 0 1 0 909370864 30281728 4341 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7393 4341 1111 63 0 7330 0
vsize: 29572
[startup+130.014 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 4770 0 0 0 12979 19 0 0 25 0 1 0 909370864 31825920 4690 4294967295 134512640 134716908 3221224560 3221222788 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7770 4690 1111 63 0 7707 0
vsize: 31080
[startup+140.013 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 7124
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 5124 0 0 0 13978 20 0 0 25 0 1 0 909370864 33333248 5044 4294967295 134512640 134716908 3221224560 3221222788 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8138 5044 1111 63 0 8075 0
vsize: 32552
[startup+150.014 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 5477 0 0 0 14978 21 0 0 25 0 1 0 909370864 34689024 5397 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8469 5397 1111 63 0 8406 0
vsize: 33876
[startup+160.014 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 5840 0 0 0 15977 21 0 0 25 0 1 0 909370864 36192256 5760 4294967295 134512640 134716908 3221224560 3221222788 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8836 5760 1111 63 0 8773 0
vsize: 35344
[startup+170.014 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 6224 0 0 0 16976 23 0 0 25 0 1 0 909370864 37695488 6144 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9203 6144 1111 63 0 9140 0
vsize: 36812
[startup+180.014 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 6629 0 0 0 17976 23 0 0 25 0 1 0 909370864 39350272 6549 4294967295 134512640 134716908 3221224560 3221222788 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9607 6549 1111 63 0 9544 0
vsize: 38428
[startup+190.015 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 7033 0 0 0 18975 24 0 0 25 0 1 0 909370864 41009152 6953 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10012 6953 1111 63 0 9949 0
vsize: 40048
[startup+200.015 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 7454 0 0 0 19974 25 0 0 25 0 1 0 909370864 42782720 7374 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10445 7374 1111 63 0 10382 0
vsize: 41780
[startup+210.015 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 7875 0 0 0 20974 25 0 0 25 0 1 0 909370864 44441600 7795 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10850 7795 1111 63 0 10787 0
vsize: 43400
[startup+220.015 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 8303 0 0 0 21973 26 0 0 25 0 1 0 909370864 46247936 8223 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11291 8223 1111 63 0 11228 0
vsize: 45164
[startup+230.016 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 8769 0 0 0 22973 26 0 0 25 0 1 0 909370864 48304128 8689 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11793 8689 1111 63 0 11730 0
vsize: 47172
[startup+240.016 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 9212 0 0 0 23973 27 0 0 25 0 1 0 909370864 50077696 9132 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12226 9132 1111 63 0 12163 0
vsize: 48904
[startup+250.017 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 9671 0 0 0 24972 28 0 0 25 0 1 0 909370864 52006912 9591 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12697 9591 1111 63 0 12634 0
vsize: 50788
[startup+260.017 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 10157 0 0 0 25971 29 0 0 25 0 1 0 909370864 53960704 10077 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13174 10077 1111 63 0 13111 0
vsize: 52696
[startup+270.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 10644 0 0 0 26970 30 0 0 25 0 1 0 909370864 55914496 10564 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13651 10564 1111 63 0 13588 0
vsize: 54604
[startup+280.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 11161 0 0 0 27969 31 0 0 25 0 1 0 909370864 58028032 11081 4294967295 134512640 134716908 3221224560 3221222788 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14167 11081 1111 63 0 14104 0
vsize: 56668
[startup+290.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 11663 0 0 0 28968 33 0 0 25 0 1 0 909370864 60133376 11583 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14681 11583 1111 63 0 14618 0
vsize: 58724
[startup+300.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 12229 0 0 0 29968 33 0 0 25 0 1 0 909370864 62390272 12149 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15232 12149 1111 63 0 15169 0
vsize: 60928
[startup+310.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 12806 0 0 0 30967 34 0 0 25 0 1 0 909370864 64798720 12726 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15820 12726 1111 63 0 15757 0
vsize: 63280
[startup+320.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 13425 0 0 0 31966 35 0 0 25 0 1 0 909370864 67207168 13345 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16408 13345 1111 63 0 16345 0
vsize: 65632
[startup+330.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 14126 0 0 0 32965 36 0 0 25 0 1 0 909370864 70066176 14046 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17106 14046 1111 63 0 17043 0
vsize: 68424
[startup+340.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 14908 0 0 0 33964 38 0 0 25 0 1 0 909370864 73371648 14828 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17913 14828 1111 63 0 17850 0
vsize: 71652
[startup+350.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 15786 0 0 0 34962 40 0 0 25 0 1 0 909370864 76955648 15706 4294967295 134512640 134716908 3221224560 3221223216 134527930 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18788 15706 1111 63 0 18725 0
vsize: 75152
[startup+360.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 16761 0 0 0 35960 42 0 0 25 0 1 0 909370864 81203200 16681 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19825 16681 1111 63 0 19762 0
vsize: 79300
[startup+370.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 17778 0 0 0 36958 44 0 0 25 0 1 0 909370864 85262336 17698 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20816 17698 1111 63 0 20753 0
vsize: 83264
[startup+380.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 18891 0 0 0 37956 47 0 0 25 0 1 0 909370864 89776128 18811 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21918 18811 1111 63 0 21855 0
vsize: 87672
[startup+384.124 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 7126
Raw data (stat): 7071 (bsolo_lpr_cuts-) R 7070 20224 20223 0 -1 0 18891 0 0 0 37956 47 0 0 25 0 1 0 909370864 89776128 18811 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21918 18811 1111 63 0 21855 0
vsize: 0

Child status: 0
Real time (s): 384.124
CPU time (s): 384.135
CPU user time (s): 383.6
CPU system time (s): 0.534918
CPU usage (%): 100.003
Max. virtual memory (Kb): 87672
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####