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-A2C1S1.opb
MD5SUM	84023cc1c9d18b4d21ad2d86c1617614
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.945856
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 27939

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-05-24 23:58:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14874 boxname=wulflinc26 idbench=1145 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  84023cc1c9d18b4d21ad2d86c1617614  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-A2C1S1.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-A2C1S1.opb
IDLAUNCH: 14874
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        801628 kB
Buffers:         29336 kB
Cached:         179856 kB
SwapCached:        656 kB
Active:          55744 kB
Inactive:       155996 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        801376 kB
SwapTotal:     2097892 kB
SwapFree:      2096880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6036 kB
Slab:            15692 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 00:05:00 (client local time) WITH STATUS 0 IN 368.842 SECONDS
stats: 14874 7 368.842 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/wulflinc26/normalized-mps-v2-20-10-A2C1S1.opb
s UNKNOWN
c Exit Code: 0
c Total time: 368.799 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.85 0.94 0.90 2/54 27046
Raw data (stat): 27046 (runsolver) R 27045 20687 20686 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834388935 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 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.87 0.94 0.90 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 974 0 0 0 995 3 0 0 25 0 1 0 834388935 16236544 898 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 3964 898 1111 63 0 3901 0
vsize: 15856
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 1256 0 0 0 1993 5 0 0 25 0 1 0 834388935 17420288 1180 4294967295 134512640 134714508 3221224576 3221222804 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4253 1180 1111 63 0 4190 0
vsize: 17012
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 1551 0 0 0 2993 6 0 0 25 0 1 0 834388935 18591744 1475 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4539 1475 1111 63 0 4476 0
vsize: 18156
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 1865 0 0 0 3991 7 0 0 25 0 1 0 834388935 19943424 1789 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4869 1789 1111 63 0 4806 0
vsize: 19476
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 2151 0 0 0 4991 8 0 0 25 0 1 0 834388935 20996096 2075 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5126 2075 1111 63 0 5063 0
vsize: 20504
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 2453 0 0 0 5990 9 0 0 25 0 1 0 834388935 22351872 2377 4294967295 134512640 134714508 3221224576 3221222804 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5457 2377 1111 63 0 5394 0
vsize: 21828
[startup+70.001 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 27046
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 2761 0 0 0 6989 10 0 0 25 0 1 0 834388935 23543808 2685 4294967295 134512640 134714508 3221224576 3221222804 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5748 2685 1111 63 0 5685 0
vsize: 22992
[startup+80.002 s]
Raw data (loadavg): 1.19 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 3085 0 0 0 7984 14 0 0 25 0 1 0 834388935 24895488 3009 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6078 3009 1111 63 0 6015 0
vsize: 24312
[startup+90.0013 s]
Raw data (loadavg): 1.16 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 3402 0 0 0 8983 15 0 0 25 0 1 0 834388935 26251264 3326 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6409 3326 1111 63 0 6346 0
vsize: 25636
[startup+100.002 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 3720 0 0 0 9983 16 0 0 25 0 1 0 834388935 27426816 3644 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6732 3646 1111 63 0 6669 0
vsize: 26784
[startup+110.003 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 4052 0 0 0 10982 17 0 0 25 0 1 0 834388935 28782592 3976 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7027 3976 1111 63 0 6964 0
vsize: 28108
[startup+120.003 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 4390 0 0 0 11981 18 0 0 25 0 1 0 834388935 30281728 4314 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7393 4314 1111 63 0 7330 0
vsize: 29572
[startup+130.003 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 4740 0 0 0 12981 19 0 0 25 0 1 0 834388935 31678464 4664 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7734 4664 1111 63 0 7671 0
vsize: 30936
[startup+140.003 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 27099
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 5092 0 0 0 13979 20 0 0 25 0 1 0 834388935 33181696 5016 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8101 5016 1111 63 0 8038 0
vsize: 32404
[startup+150.003 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 5461 0 0 0 14978 21 0 0 25 0 1 0 834388935 34689024 5385 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8469 5385 1111 63 0 8406 0
vsize: 33876
[startup+160.003 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 5832 0 0 0 15978 22 0 0 25 0 1 0 834388935 36192256 5756 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8836 5756 1111 63 0 8773 0
vsize: 35344
[startup+170.003 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 6221 0 0 0 16976 24 0 0 25 0 1 0 834388935 37695488 6145 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9203 6145 1111 63 0 9140 0
vsize: 36812
[startup+180.003 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 6614 0 0 0 17975 25 0 0 25 0 1 0 834388935 39350272 6538 4294967295 134512640 134714508 3221224576 3221222804 1077414336 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9607 6538 1111 63 0 9544 0
vsize: 38428
[startup+190.003 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 7018 0 0 0 18974 26 0 0 25 0 1 0 834388935 41009152 6942 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10012 6942 1111 63 0 9949 0
vsize: 40048
[startup+200.004 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 7440 0 0 0 19973 28 0 0 25 0 1 0 834388935 42782720 7364 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10445 7364 1111 63 0 10382 0
vsize: 41780
[startup+210.004 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 7882 0 0 0 20971 30 0 0 25 0 1 0 834388935 44589056 7806 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10886 7806 1111 63 0 10823 0
vsize: 43544
[startup+220.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 8337 0 0 0 21970 31 0 0 25 0 1 0 834388935 46395392 8261 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11327 8261 1111 63 0 11264 0
vsize: 45308
[startup+230.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 8841 0 0 0 22969 33 0 0 25 0 1 0 834388935 48603136 8765 4294967295 134512640 134714508 3221224576 3221222804 1077414374 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11866 8765 1111 63 0 11803 0
vsize: 47464
[startup+240.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 9335 0 0 0 23968 34 0 0 25 0 1 0 834388935 50528256 9259 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12336 9259 1111 63 0 12273 0
vsize: 49344
[startup+250.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 9867 0 0 0 24967 35 0 0 25 0 1 0 834388935 52760576 9791 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 12881 9791 1111 63 0 12818 0
vsize: 51524
[startup+260.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 10405 0 0 0 25966 36 0 0 25 0 1 0 834388935 55013376 10329 4294967295 134512640 134714508 3221224576 3221222804 1077414360 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13431 10329 1111 63 0 13368 0
vsize: 53724
[startup+270.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 10973 0 0 0 26964 38 0 0 25 0 1 0 834388935 57274368 10897 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13983 10897 1111 63 0 13920 0
vsize: 55932
[startup+280.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 11587 0 0 0 27963 39 0 0 25 0 1 0 834388935 59834368 11511 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14608 11511 1111 63 0 14545 0
vsize: 58432
[startup+290.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 12227 0 0 0 28962 41 0 0 25 0 1 0 834388935 62390272 12151 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15232 12151 1111 63 0 15169 0
vsize: 60928
[startup+300.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 12928 0 0 0 29962 42 0 0 25 0 1 0 834388935 65253376 12852 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15931 12852 1111 63 0 15868 0
vsize: 63724
[startup+310.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 13668 0 0 0 30961 43 0 0 25 0 1 0 834388935 68259840 13592 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16665 13592 1111 63 0 16602 0
vsize: 66660
[startup+320.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 14486 0 0 0 31959 45 0 0 25 0 1 0 834388935 71573504 14410 4294967295 134512640 134714508 3221224576 3221222444 1077244338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17474 14410 1111 63 0 17411 0
vsize: 69896
[startup+330.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 15356 0 0 0 32957 47 0 0 25 0 1 0 834388935 75149312 15280 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18347 15280 1111 63 0 18284 0
vsize: 73388
[startup+340.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 16263 0 0 0 33956 49 0 0 25 0 1 0 834388935 78917632 16187 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19267 16187 1111 63 0 19204 0
vsize: 77068
[startup+350.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 17282 0 0 0 34955 50 0 0 25 0 1 0 834388935 83308544 17206 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20339 17206 1111 63 0 20276 0
vsize: 81356
[startup+360.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 18345 0 0 0 35953 52 0 0 25 0 1 0 834388935 87670784 18269 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21404 18269 1111 63 0 21341 0
vsize: 85616
[startup+368.81 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 27101
Raw data (stat): 27046 (bsolo_lpr_cuts) R 27045 20687 20686 0 -1 0 18345 0 0 0 35953 52 0 0 25 0 1 0 834388935 87670784 18269 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21404 18269 1111 63 0 21341 0
vsize: 0

Child status: 0
Real time (s): 368.809
CPU time (s): 368.842
CPU user time (s): 368.236
CPU system time (s): 0.605907
CPU usage (%): 100.009
Max. virtual memory (Kb): 85616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####