PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bc1.opb
MD5SUM	cf391497c5a28b773d7c43cd006668b6
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	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576000000000000000000
Number of bits of the biggest number in a constraint	80
Biggest sum of numbers in a constraint	3239461173145800120729600
Number of bits of the biggest sum of numbers	82
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	2.33964
Number of variables	19894
Total number of constraints	3627
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	336
Number of constraints which are nor clauses,nor cardinality constraints	3291
Minimum length of a constraint	1
Maximum length of a constraint	4476
Trace number 26945

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-24 18:37:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19397 boxname=wulflinc12 idbench=1493 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  cf391497c5a28b773d7c43cd006668b6  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-bc1.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-bc1.opb
IDLAUNCH: 19397
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
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:        707520 kB
Buffers:         36640 kB
Cached:         268860 kB
SwapCached:        568 kB
Active:         129956 kB
Inactive:       178000 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        707268 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            13416 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-24 18:37:16 (client local time) WITH STATUS 0 IN 2.53861 SECONDS
stats: 19397 7 2.53861 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c ERROR Parsing file!!!
c ERROR parsing line: -193912710000000000*x2_bit_7 -387825420000000000*x2_bit_6 -775650840000000000*x2_bit_5 -1551301680000000000*x2_bit_4 -3102603360000000000*x2_bit_3 -6205206720000000000*x2_bit_2 -12410413440000000000*x2_bit_1 -24820826880000000000*x2_bit0 -49641653760000000000*x2_bit1 -99283307520000000000*x2_bit2 -198566615040000000000*x2_bit3 -632482940000000000*x3_bit_7 -1264965880000000000*x3_bit_6 -2529931760000000000*x3_bit_5 -5059863520000000000*x3_bit_4 -10119727040000000000*x3_bit_3 -20239454080000000000*x3_bit_2 -40478908160000000000*x3_bit_1 -80957816320000000000*x3_bit0 -161915632640000000000*x3_bit1 -323831265280000000000*x3_bit2 -647662530560000000000*x3_bit3 -77582030000*x4_bit_7 -155164060000*x4_bit_6 -310328120000*x4_bit_5 -620656240000*x4_bit_4 -1241312480000*x4_bit_3 -2482624960000*x4_bit_2 -4965249920000*x4_bit_1 -9930499840000*x4_bit0 -19860999680000*x4_bit1 -39721999360000*x4_bit2 -79443998720000*x4_bit3 -1677633000000*x5_bit_7 -3355266000000*x5_bit_6 -6710532000000*x5_bit_5 -13421064000000*x5_bit_4 -26842128000000*x5_bit_3 -53684256000000*x5_bit_2 -107368512000000*x5_bit_1 -214737024000000*x5_bit0 -429474048000000*x5_bit1 -858948096000000*x5_bit2 -1717896192000000*x5_bit3 -277943200000000*x6_bit_7 -555886400000000*x6_bit_6 -1111772800000000*x6_bit_5 -2223545600000000*x6_bit_4 -4447091200000000*x6_bit_3 -8894182400000000*x6_bit_2 -17788364800000000*x6_bit_1 -35576729600000000*x6_bit0 -71153459200000000*x6_bit1 -142306918400000000*x6_bit2 -284613836800000000*x6_bit3 -128075570000000000*x9_bit_7 -256151140000000000*x9_bit_6 -512302280000000000*x9_bit_5 -1024604560000000000*x9_bit_4 -2049209120000000000*x9_bit_3 -4098418240000000000*x9_bit_2 -8196836480000000000*x9_bit_1 -16393672960000000000*x9_bit0 -32787345920000000000*x9_bit1 -65574691840000000000*x9_bit2 -131149383680000000000*x9_bit3 -303109990000000000*x12_bit_7 -606219980000000000*x12_bit_6 -1212439960000000000*x12_bit_5 -2424879920000000000*x12_bit_4 -4849759840000000000*x12_bit_3 -9699519680000000000*x12_bit_2 -19399039360000000000*x12_bit_1 -38798078720000000000*x12_bit0 -77596157440000000000*x12_bit1 -155192314880000000000*x12_bit2 -310384629760000000000*x12_bit3 -4802866053120000*x14_bit_7 -9605732106240000*x14_bit_6 -19211464212480000*x14_bit_5 -38422928424960000*x14_bit_4 -76845856849920000*x14_bit_3 -153691713699840000*x14_bit_2 -307383427399680000*x14_bit_1 -614766854799360000*x14_bit0 -1229533709598720000*x14_bit1 -2459067419197440000*x14_bit2 -4918134838394880000*x14_bit3 -384920360000000000*x15_bit_7 -769840720000000000*x15_bit_6 -1539681440000000000*x15_bit_5 -3079362880000000000*x15_bit_4 -6158725760000000000*x15_bit_3 -12317451520000000000*x15_bit_2 -24634903040000000000*x15_bit_1 -49269806080000000000*x15_bit0 -98539612160000000000*x15_bit1 -197079224320000000000*x15_bit2 -394158448640000000000*x15_bit3 -312615600000*x16_bit_7 -625231200000*x16_bit_6 -1250462400000*x16_bit_5 -2500924800000*x16_bit_4 -5001849600000*x16_bit_3 -10003699200000*x16_bit_2 -20007398400000*x16_bit_1 -40014796800000*x16_bit0 -80029593600000*x16_bit1 -160059187200000*x16_bit2 -320118374400000*x16_bit3 -5729734000000*x17_bit_7 -11459468000000*x17_bit_6 -22918936000000*x17_bit_5 -45837872000000*x17_bit_4 -91675744000000*x17_bit_3 -183351488000000*x17_bit_2 -366702976000000*x17_bit_1 -733405952000000*x17_bit0 -1466811904000000*x17_bit1 -2933623808000000*x17_bit2 -5867247616000000*x17_bit3 -710926900000000*x18_bit_7 -1421853800000000*x18_bit_6 -2843707600000000*x18_bit_5 -5687415200000000*x18_bit_4 -11374830400000000*x18_bit_3 -22749660800000000*x18_bit_2 -45499321600000000*x18_bit_1 -90998643200000000*x18_bit0 -181997286400000000*x18_bit1 -363994572800000000*x18_bit2 -727989145600000000*x18_bit3 -27237640000*x19_bit_7 -54475280000*x19_bit_6 -108950560000*x19_bit_5 -217901120000*x19_bit_4 -435802240000*x19_bit_3 -871604480000*x19_bit_2 -1743208960000*x19_bit_1 -3486417920000*x19_bit0 -6972835840000*x19_bit1 -13945671680000*x19_bit2 -27891343360000*x19_bit3 -666176000000*x20_bit_7 -1332352000000*x20_bit_6 -2664704000000*x20_bit_5 -5329408000000*x20_bit_4 -10658816000000*x20_bit_3 -21317632000000*x20_bit_2 -42635264000000*x20_bit_1 -85270528000000*x20_bit0 -170541056000000*x20_bit1 -341082112000000*x20_bit2 -682164224000000*x20_bit3 -135633900000000*x21_bit_7 -271267800000000*x21_bit_6 -542535600000000*x21_bit_5 -1085071200000000*x21_bit_4 -2170142400000000*x21_bit_3 -4340284800000000*x21_bit_2 -8680569600000000*x21_bit_1 -17361139200000000*x21_bit0 -34722278400000000*x21_bit1 -69444556800000000*x21_bit2 -138889113600000000*x21_bit3 -1866442000*x22_bit_7 -3732884000*x22_bit_6 -7465768000*x22_bit_5 -14931536000*x22_bit_4 -29863072000*x22_bit_3 -59726144000*x22_bit_2 -119452288000*x22_bit_1 -238904576000*x22_bit0 -477809152000*x22_bit1 -955618304000*x22_bit2 -1911236608000*x22_bit3 -59836770000*x23_bit_7 -119673540000*x23_bit_6 -239347080000*x23_bit_5 -478694160000*x23_bit_4 -957388320000*x23_bit_3 -1914776640000*x23_bit_2 -3829553280000*x23_bit_1 -7659106560000*x23_bit0 -15318213120000*x23_bit1 -30636426240000*x23_bit2 -61272852480000*x23_bit3 -20763460000000*x24_bit_7 -41526920000000*x24_bit_6 -83053840000000*x24_bit_5 -166107680000000*x24_bit_4 -332215360000000*x24_bit_3 -664430720000000*x24_bit_2 -1328861440000000*x24_bit_1 -2657722880000000*x24_bit0 -5315445760000000*x24_bit1 -10630891520000000*x24_bit2 -21261783040000000*x24_bit3 -100455000*x25_bit_7 -200910000*x25_bit_6 -401820000*x25_bit_5 -803640000*x25_bit_4 -1607280000*x25_bit_3 -3214560000*x25_bit_2 -6429120000*x25_bit_1 -12858240000*x25_bit0 -25716480000*x25_bit1 -51432960000*x25_bit2 -102865920000*x25_bit3 -4219408000*x26_bit_7 -8438816000*x26_bit_6 -16877632000*x26_bit_5 -33755264000*x26_bit_4 -67510528000*x26_bit_3 -135021056000*x26_bit_2 -270042112000*x26_bit_1 -540084224000*x26_bit0 -1080168448000*x26_bit1 -2160336896000*x26_bit2 -4320673792000*x26_bit3 -2552736000000*x27_bit_7 -5105472000000*x27_bit_6 -10210944000000*x27_bit_5 -20421888000000*x27_bit_4 -40843776000000*x27_bit_3 -81687552000000*x27_bit_2 -163375104000000*x27_bit_1 -326750208000000*x27_bit0 -653500416000000*x27_bit1 -1307000832000000*x27_bit2 -2614001664000000*x27_bit3 -140443*x28_bit_7 -280886*x28_bit_6 -561772*x28_bit_5 -1123544*x28_bit_4 -2247088*x28_bit_3 -4494176*x28_bit_2 -8988352*x28_bit_1 -17976704*x28_bit0 -35953408*x28_bit1 -71906816*x28_bit2 -143813632*x28_bit3 -10236400*x29_bit_7 -20472800*x29_bit_6 -40945600*x29_bit_5 -81891200*x29_bit_4 -163782400*x29_bit_3 -327564800*x29_bit_2 -655129600*x29_bit_1 -1310259200*x29_bit0 -2620518400*x29_bit1 -5241036800*x29_bit2 -10482073600*x29_bit3 -18957700000*x30_bit_7 -37915400000*x30_bit_6 -75830800000*x30_bit_5 -151661600000*x30_bit_4 -303323200000*x30_bit_3 -606646400000*x30_bit_2 -1213292800000*x30_bit_1 -2426585600000*x30_bit0 -4853171200000*x30_bit1 -9706342400000*x30_bit2 -19412684800000*x30_bit3 -471330700000000*x31_bit_7 -942661400000000*x31_bit_6 -1885322800000000*x31_bit_5 -3770645600000000*x31_bit_4 -7541291200000000*x31_bit_3 -15082582400000000*x31_bit_2 -30165164800000000*x31_bit_1 -60330329600000000*x31_bit0 -120660659200000000*x31_bit1 -241321318400000000*x31_bit2 -482642636800000000*x31_bit3 -123952756162560*x32_bit_7 -247905512325120*x32_bit_6 -495811024650240*x32_bit_5 -991622049300480*x32_bit_4 -1983244098600960*x32_bit_3 -3966488197201920*x32_bit_2 -7932976394403840*x32_bit_1 -15865952788807680*x32_bit0 -31731905577615360*x32_bit1 -63463811155230720*x32_bit2 -126927622310461440*x32_bit3 -949549623410688*x35_bit_7 -1899099246821376*x35_bit_6 -3798198493642752*x35_bit_5 -7596396987285504*x35_bit_4 -15192793974571008*x35_bit_3 -30385587949142016*x35_bit_2 -60771175898284032*x35_bit_1 -121542351796568064*x35_bit0 -243084703593136128*x35_bit1 -486169407186272256*x35_bit2 -972338814372544512*x35_bit3 -260637350000000000*x36_bit_7 -521274700000000000*x36_bit_6 -1042549400000000000*x36_bit_5 -2085098800000000000*x36_bit_4 -4170197600000000000*x36_bit_3 -8340395200000000000*x36_bit_2 -16680790400000000000*x36_bit_1 -33361580800000000000*x36_bit0 -66723161600000000000*x36_bit1 -133446323200000000000*x36_bit2 -266892646400000000000*x36_bit3 -87143920000*x37_bit_7 -174287840000*x37_bit_6 -348575680000*x37_bit_5 -697151360000*x37_bit_4 -1394302720000*x37_bit_3 -2788605440000*x37_bit_2 -5577210880000*x37_bit_1 -11154421760000*x37_bit0 -22308843520000*x37_bit1 -44617687040000*x37_bit2 -89235374080000*x37_bit3 -1858748000000*x38_bit_7 -3717496000000*x38_bit_6 -7434992000000*x38_bit_5 -14869984000000*x38_bit_4 -29739968000000*x38_bit_3 -59479936000000*x38_bit_2 -118959872000000*x38_bit_1 -237919744000000*x38_bit0 -475839488000000*x38_bit1 -951678976000000*x38_bit2 -1903357952000000*x38_bit3 -300807200000000*x39_bit_7 -601614400000000*x39_bit_6 -1203228800000000*x39_bit_5 -2406457600000000*x39_bit_4 -4812915200000000*x39_bit_3 -9625830400000000*x39_bit_2 -19251660800000000*x39_bit_1 -38503321600000000*x39_bit0 -77006643200000000*x39_bit1 -154013286400000000*x39_bit2 -308026572800000000*x39_bit3 -30407240000000*x40_bit_7 -60814480000000*x40_bit_6 -121628960000000*x40_bit_5 -243257920000000*x40_bit_4 -486515840000000*x40_bit_3 -973031680000000*x40_bit_2 -1946063360000000*x40_bit_1 -3892126720000000*x40_bit0 -7784253440000000*x40_bit1 -15568506880000000*x40_bit2 -31137013760000000*x40_bit3 -325149500000000*x41_bit_7 -650299000000000*x41_bit_6 -1300598000000000*x41_bit_5 -2601196000000000*x41_bit_4 -5202392000000000*x41_bit_3 -10404784000000000*x41_bit_2 -20809568000000000*x41_bit_1 -41619136000000000*x41_bit0 -83238272000000000*x41_bit1 -166476544000000000*x41_bit2 -332953088000000000*x41_bit3 -106937000000000*x43_bit_7 -213874000000000*x43_bit_6 -427748000000000*x43_bit_5 -855496000000000*x43_bit_4 -1710992000000000*x43_bit_3 -3421984000000000*x43_bit_2 -6843968000000000*x43_bit_1 -13687936000000000*x43_bit0 -27375872000000000*x43_bit1 -54751744000000000*x43_bit2 -109503488000000000*x43_bit3 -963735100000000*x44_bit_7 -1927470200000000*x44_bit_6 -3854940400000000*x44_bit_5 -7709880800000000*x44_bit_4 -15419761600000000*x44_bit_3 -30839523200000000*x44_bit_2 -61679046400000000*x44_bit_1 -123358092800000000*x44_bit0 -246716185600000000*x44_bit1 -493432371200000000*x44_bit2 -986864742400000000*x44_bit3 -663276400000000*x46_bit_7 -1326552800000000*x46_bit_6 -2653105600000000*x46_bit_5 -5306211200000000*x46_bit_4 -10612422400000000*x46_bit_3 -21224844800000000*x46_bit_2 -42449689600000000*x46_bit_1 -84899379200000000*x46_bit0 -169798758400000000*x46_bit1 -339597516800000000*x46_bit2 -679195033600000000*x46_bit3 -165813654913024*x47_bit_7 -331627309826048*x47_bit_6 -663254619652096*x47_bit_5 -1326509239304192*x47_bit_4 -2653018478608384*x47_bit_3 -5306036957216768*x47_bit_2 -10612073914433536*x47_bit_1 -21224147828867072*x47_bit0 -42448295657734144*x47_bit1 -84896591315468288*x47_bit2 -169793182630936576*x47_bit3 -43528419803136*x49_bit_7 -87056839606272*x49_bit_6 -174113679212544*x49_bit_5 -348227358425088*x49_bit_4 -696454716850176*x49_bit_3 -1392909433700352*x49_bit_2 -2785818867400704*x49_bit_1 -5571637734801408*x49_bit0 -11143275469602816*x49_bit1 -22286550939205632*x49_bit2 -44573101878411264*x49_bit3 -261817985138688*x50_bit_7 -523635970277376*x50_bit_6 -1047271940554752*x50_bit_5 -2094543881109504*x50_bit_4 -4189087762219008*x50_bit_3 -8378175524438016*x50_bit_2 -16756351048876032*x50_bit_1 -33512702097752064*x50_bit0 -67025404195504128*x50_bit1 -134050808391008256*x50_bit2 -268101616782016512*x50_bit3 -107477210000000000*x51_bit_7 -214954420000000000*x51_bit_6 -429908840000000000*x51_bit_5 -859817680000000000*x51_bit_4 -1719635360000000000*x51_bit_3 -3439270720000000000*x51_bit_2 -6878541440000000000*x51_bit_1 -13757082880000000000*x51_bit0 -27514165760000000000*x51_bit1 -55028331520000000000*x51_bit2 -110056663040000000000*x51_bit3 -19209560000*x52_bit_7 -38419120000*x52_bit_6 -76838240000*x52_bit_5 -153676480000*x52_bit_4 -307352960000*x52_bit_3 -614705920000*x52_bit_2 -1229411840000*x52_bit_1 -2458823680000*x52_bit0 -4917647360000*x52_bit1 -9835294720000*x52_bit2 -19670589440000*x52_bit3 -489486200000*x53_bit_7 -978972400000*x53_bit_6 -1957944800000*x53_bit_5 -3915889600000*x53_bit_4 -7831779200000*x53_bit_3 -15663558400000*x53_bit_2 -31327116800000*x53_bit_1 -62654233600000*x53_bit0 -125308467200000*x53_bit1 -250616934400000*x53_bit2 -501233868800000*x53_bit3 -106540800000000*x54_bit_7 -213081600000000*x54_bit_6 -426163200000000*x54_bit_5 -852326400000000*x54_bit_4 -1704652800000000*x54_bit_3 -3409305600000000*x54_bit_2 -6818611200000000*x54_bit_1 -13637222400000000*x54_bit0 -27274444800000000*x54_bit1 -54548889600000000*x54_bit2 -109097779200000000*x54_bit3 -112928000*x55_bit_7 -225856000*x55_bit_6 -451712000*x55_bit_5 -903424000*x55_bit_4 -1806848000*x55_bit_3 -3613696000*x55_bit_2 -7227392000*x55_bit_1 -14454784000*x55_bit0 -28909568000*x55_bit1 -57819136000*x55_bit2 -115638272000*x55_bit3 -4693840000*x56_bit_7 -9387680000*x56_bit_6 -18775360000*x56_bit_5 -37550720000*x56_bit_4 -75101440000*x56_bit_3 -150202880000*x56_bit_2 -300405760000*x56_bit_1 -600811520000*x56_bit0 -1201623040000*x56_bit1 -2403246080000*x56_bit2 -4806492160000*x56_bit3 -2778490000000*x57_bit_7 -5556980000000*x57_bit_6 -11113960000000*x57_bit_5 -22227920000000*x57_bit_4 -44455840000000*x57_bit_3 -88911680000000*x57_bit_2 -177823360000000*x57_bit_1 -355646720000000*x57_bit0 -711293440000000*x57_bit1 -1422586880000000*x57_bit2 -2845173760000000*x57_bit3 -6031950*x58_bit_7 -12063900*x58_bit_6 -24127800*x58_bit_5 -48255600*x58_bit_4 -96511200*x58_bit_3 -193022400*x58_bit_2 -386044800*x58_bit_1 -772089600*x58_bit0 -1544179200*x58_bit1 -3088358400*x58_bit2 -6176716800*x58_bit3 -323522000*x59_bit_7 -647044000*x59_bit_6 -1294088000*x59_bit_5 -2588176000*x59_bit_4 -5176352000*x59_bit_3 -10352704000*x59_bit_2 -20705408000*x59_bit_1 -41410816000*x59_bit0 -82821632000*x59_bit1 -165643264000*x59_bit2 -331286528000*x59_bit3 -325773000000*x60_bit_7 -651546000000*x60_bit_6 -1303092000000*x60_bit_5 -2606184000000*x60_bit_4 -5212368000000*x60_bit_3 -10424736000000*x60_bit_2 -20849472000000*x60_bit_1 -41698944000000*x60_bit0 -83397888000000*x60_bit1 -166795776000000*x60_bit2 -333591552000000*x60_bit3 -252908*x61_bit_7 -505816*x61_bit_6 -1011632*x61_bit_5 -2023264*x61_bit_4 -4046528*x61_bit_3 -8093056*x61_bit_2 -16186112*x61_bit_1 -32372224*x61_bit0 -64744448*x61_bit1 -129488896*x61_bit2 -258977792*x61_bit3 -17593400*x62_bit_7 -35186800*x62_bit_6 -70373600*x62_bit_5 -140747200*x62_bit_4 -281494400*x62_bit_3 -562988800*x62_bit_2 -1125977600*x62_bit_1 -2251955200*x62_bit0 -4503910400*x62_bit1 -9007820800*x62_bit2 -18015641600*x62_bit3 -29697180000*x63_bit_7 -59394360000*x63_bit_6 -118788720000*x63_bit_5 -237577440000*x63_bit_4 -475154880000*x63_bit_3 -950309760000*x63_bit_2 -1900619520000*x63_bit_1 -3801239040000*x63_bit0 -7602478080000*x63_bit1 -15204956160000*x63_bit2 -30409912320000*x63_bit3 -753619*x65_bit_7 -1507238*x65_bit_6 -3014476*x65_bit_5 -6028952*x65_bit_4 -12057904*x65_bit_3 -24115808*x65_bit_2 -48231616*x65_bit_1 -96463232*x65_bit0 -192926464*x65_bit1 -385852928*x65_bit2 -771705856*x65_bit3 -2153092000*x66_bit_7 -4306184000*x66_bit_6 -8612368000*x66_bit_5 -17224736000*x66_bit_4 -34449472000*x66_bit_3 -68898944000*x66_bit_2 -137797888000*x66_bit_1 -275595776000*x66_bit0 -551191552000*x66_bit1 -1102383104000*x66_bit2 -2204766208000*x66_bit3 -5466850000000*x67_bit_7 -10933700000000*x67_bit_6 -21867400000000*x67_bit_5 -43734800000000*x67_bit_4 -87469600000000*x67_bit_3 -174939200000000*x67_bit_2 -349878400000000*x67_bit_1 -699756800000000*x67_bit0 -1399513600000000*x67_bit1 -2799027200000000*x67_bit2 -5598054400000000*x67_bit3 -72476160000000*x68_bit_7 -144952320000000*x68_bit_6 -289904640000000*x68_bit_5 -579809280000000*x68_bit_4 -1159618560000000*x68_bit_3 -2319237120000000*x68_bit_2 -4638474240000000*x68_bit_1 -9276948480000000*x68_bit0 -18553896960000000*x68_bit1 -37107793920000000*x68_bit2 -74215587840000000*x68_bit3 -170497316749312*x69_bit_7 -340994633498624*x69_bit_6 -681989266997248*x69_bit_5 -1363978533994496*x69_bit_4 -2727957067988992*x69_bit_3 -5455914135977984*x69_bit_2 -10911828271955968*x69_bit_1 -21823656543911936*x69_bit0 -43647313087823872*x69_bit1 -87294626175647744*x69_bit2 -174589252351295488*x69_bit3 -19241880000000*x70_bit_7 -38483760000000*x70_bit_6 -76967520000000*x70_bit_5 -153935040000000*x70_bit_4 -307870080000000*x70_bit_3 -615740160000000*x70_bit_2 -1231480320000000*x70_bit_1 -2462960640000000*x70_bit0 -4925921280000000*x70_bit1 -9851842560000000*x70_bit2 -19703685120000000*x70_bit3 -218329800000000*x71_bit_7 -436659600000000*x71_bit_6 -873319200000000*x71_bit_5 -1746638400000000*x71_bit_4 -3493276800000000*x71_bit_3 -6986553600000000*x71_bit_2 -13973107200000000*x71_bit_1 -27946214400000000*x71_bit0 -55892428800000000*x71_bit1 -111784857600000000*x71_bit2 -223569715200000000*x71_bit3 -212167000000000*x73_bit_7 -424334000000000*x73_bit_6 -848668000000000*x73_bit_5 -1697336000000000*x73_bit_4 -3394672000000000*x73_bit_3 -6789344000000000*x73_bit_2 -13578688000000000*x73_bit_1 -27157376000000000*x73_bit0 -54314752000000000*x73_bit1 -108629504000000000*x73_bit2 -217259008000000000*x73_bit3 -67810017411072*x74_bit_7 -135620034822144*x74_bit_6 -271240069644288*x74_bit_5 -542480139288576*x74_bit_4 -1084960278577152*x74_bit_3 -2169920557154304*x74_bit_2 -4339841114308608*x74_bit_1 -8679682228617216*x74_bit0 -17359364457234432*x74_bit1 -34718728914468864*x74_bit2 -69437457828937728*x74_bit3 -1215835448279040*x75_bit_7 -2431670896558080*x75_bit_6 -4863341793116160*x75_bit_5 -9726683586232320*x75_bit_4 -19453367172464640*x75_bit_3 -38906734344929280*x75_bit_2 -77813468689858560*x75_bit_1 -155626937379717120*x75_bit0 -311253874759434240*x75_bit1 -622507749518868480*x75_bit2 -1245015499037736960*x75_bit3 -19488800*x76_bit_7 -38977600*x76_bit_6 -77955200*x76_bit_5 -155910400*x76_bit_4 -311820800*x76_bit_3 -623641600*x76_bit_2 -1247283200*x76_bit_1 -2494566400*x76_bit0 -4989132800*x76_bit1 -9978265600*x76_bit2 -19956531200*x76_bit3 -945579000*x77_bit_7 -1891158000*x77_bit_6 -3782316000*x77_bit_5 -7564632000*x77_bit_4 -15129264000*x77_bit_3 -30258528000*x77_bit_2 -60517056000*x77_bit_1 -121034112000*x77_bit0 -242068224000*x77_bit1 -484136448000*x77_bit2 -968272896000*x77_bit3 -774445900000*x78_bit_7 -1548891800000*x78_bit_6 -3097783600000*x78_bit_5 -6195567200000*x78_bit_4 -12391134400000*x78_bit_3 -24782268800000*x78_bit_2 -49564537600000*x78_bit_1 -99129075200000*x78_bit0 -198258150400000*x78_bit1 -396516300800000*x78_bit2 -793032601600000*x78_bit3 -1036390*x79_bit_7 -2072780*x79_bit_6 -4145560*x79_bit_5 -8291120*x79_bit_4 -16582240*x79_bit_3 -33164480*x79_bit_2 -66328960*x79_bit_1 -132657920*x79_bit0 -265315840*x79_bit1 -530631680*x79_bit2 -1061263360*x79_bit3 -64352300*x80_bit_7 -128704600*x80_bit_6 -257409200*x80_bit_5 -514818400*x80_bit_4 -1029636800*x80_bit_3 -2059273600*x80_bit_2 -4118547200*x80_bit_1 -8237094400*x80_bit0 -16474188800*x80_bit1 -32948377600*x80_bit2 -65896755200*x80_bit3 -86635220000*x81_bit_7 -173270440000*x81_bit_6 -346540880000*x81_bit_5 -693081760000*x81_bit_4 -1386163520000*x81_bit_3 -2772327040000*x81_bit_2 -5544654080000*x81_bit_1 -11089308160000*x81_bit0 -22178616320000*x81_bit1 -44357232640000*x81_bit2 -88714465280000*x81_bit3 -146438*x83_bit_7 -292876*x83_bit_6 -585752*x83_bit_5 -1171504*x83_bit_4 -2343008*x83_bit_3 -4686016*x83_bit_2 -9372032*x83_bit_1 -18744064*x83_bit0 -37488128*x83_bit1 -74976256*x83_bit2 -149952512*x83_bit3 -543915000*x84_bit_7 -1087830000*x84_bit_6 -2175660000*x84_bit_5 -4351320000*x84_bit_4 -8702640000*x84_bit_3 -17405280000*x84_bit_2 -34810560000*x84_bit_1 -69621120000*x84_bit0 -139242240000*x84_bit1 -278484480000*x84_bit2 -556968960000*x84_bit3 -784167900000*x85_bit_7 -1568335800000*x85_bit_6 -3136671600000*x85_bit_5 -6273343200000*x85_bit_4 -12546686400000*x85_bit_3 -25093372800000*x85_bit_2 -50186745600000*x85_bit_1 -100373491200000*x85_bit0 -200746982400000*x85_bit1 -401493964800000*x85_bit2 -802987929600000*x85_bit3 -12954940000000*x86_bit_7 -25909880000000*x86_bit_6 -51819760000000*x86_bit_5 -103639520000000*x86_bit_4 -207279040000000*x86_bit_3 -414558080000000*x86_bit_2 -829116160000000*x86_bit_1 -1658232320000000*x86_bit0 -3316464640000000*x86_bit1 -6632929280000000*x86_bit2 -13265858560000000*x86_bit3 -49165564379136*x87_bit_7 -98331128758272*x87_bit_6 -196662257516544*x87_bit_5 -393324515033088*x87_bit_4 -786649030066176*x87_bit_3 -1573298060132352*x87_bit_2 -3146596120264704*x87_bit_1 -6293192240529408*x87_bit0 -12586384481058816*x87_bit1 -25172768962117632*x87_bit2 -50345537924235264*x87_bit3 -2753079000000*x88_bit_7 -5506158000000*x88_bit_6 -11012316000000*x88_bit_5 -22024632000000*x88_bit_4 -44049264000000*x88_bit_3 -88098528000000*x88_bit_2 -176197056000000*x88_bit_1 -352394112000000*x88_bit0 -704788224000000*x88_bit1 -1409576448000000*x88_bit2 -2819152896000000*x88_bit3 -39555810000000*x89_bit_7 -79111620000000*x89_bit_6 -158223240000000*x89_bit_5 -316446480000000*x89_bit_4 -632892960000000*x89_bit_3 -1265785920000000*x89_bit_2 -2531571840000000*x89_bit_1 -5063143680000000*x89_bit0 -10126287360000000*x89_bit1 -20252574720000000*x89_bit2 -40505149440000000*x89_bit3 -7704810000000*x91_bit_7 -15409620000000*x91_bit_6 -30819240000000*x91_bit_5 -61638480000000*x91_bit_4 -123276960000000*x91_bit_3 -246553920000000*x91_bit_2 -493107840000000*x91_bit_1 -986215680000000*x91_bit0 -1972431360000000*x91_bit1 -3944862720000000*x91_bit2 -7889725440000000*x91_bit3 -98004830000000*x92_bit_7 -196009660000000*x92_bit_6 -392019320000000*x92_bit_5 -784038640000000*x92_bit_4 -1568077280000000*x92_bit_3 -3136154560000000*x92_bit_2 -6272309120000000*x92_bit_1 -12544618240000000*x92_bit0 -25089236480000000*x92_bit1 -50178472960000000*x92_bit2 -100356945920000000*x92_bit3 -42854100000000*x94_bit_7 -85708200000000*x94_bit_6 -171416400000000*x94_bit_5 -342832800000000*x94_bit_4 -685665600000000*x94_bit_3 -1371331200000000*x94_bit_2 -2742662400000000*x94_bit_1 -5485324800000000*x94_bit0 -10970649600000000*x94_bit1 -21941299200000000*x94_bit2 -43882598400000000*x94_bit3 -437874900000000*x95_bit_7 -875749800000000*x95_bit_6 -1751499600000000*x95_bit_5 -3502999200000000*x95_bit_4 -7005998400000000*x95_bit_3 -14011996800000000*x95_bit_2 -28023993600000000*x95_bit_1 -56047987200000000*x95_bit0 -112095974400000000*x95_bit1 -224191948800000000*x95_bit2 -448383897600000000*x95_bit3 -112800000*x99_bit_7 -225600000*x99_bit_6 -451200000*x99_bit_5 -902400000*x99_bit_4 -1804800000*x99_bit_3 -3609600000*x99_bit_2 -7219200000*x99_bit_1 -14438400000*x99_bit0 -28876800000*x99_bit1 -57753600000*x99_bit2 -115507200000*x99_bit3 -87143920000*x100_bit_7 -174287840000*x100_bit_6 -348575680000*x100_bit_5 -697151360000*x100_bit_4 -1394302720000*x100_bit_3 -2788605440000*x100_bit_2 -5577210880000*x100_bit_1 -11154421760000*x100_bit0 -22308843520000*x100_bit1 -44617687040000*x100_bit2 -89235374080000*x100_bit3 -1858748000000*x101_bit_7 -3717496000000*x101_bit_6 -7434992000000*x101_bit_5 -14869984000000*x101_bit_4 -29739968000000*x101_bit_3 -59479936000000*x101_bit_2 -118959872000000*x101_bit_1 -237919744000000*x101_bit0 -475839488000000*x101_bit1 -951678976000000*x101_bit2 -1903357952000000*x101_bit3 -300807200000000*x102_bit_7 -601614400000000*x102_bit_6 -1203228800000000*x102_bit_5 -2406457600000000*x102_bit_4 -4812915200000000*x102_bit_3 -9625830400000000*x102_bit_2 -19251660800000000*x102_bit_1 -38503321600000000*x102_bit0 -77006643200000000*x102_bit1 -154013286400000000*x102_bit2 -308026572800000000*x102_bit3 -312615600000*x103_bit_7 -625231200000*x103_bit_6 -1250462400000*x103_bit_5 -2500924800000*x103_bit_4 -5001849600000*x103_bit_3 -10003699200000*x103_bit_2 -20007398400000*x103_bit_1 -40014796800000*x103_bit0 -80029593600000*x103_bit1 -160059187200000*x103_bit2 -320118374400000*x103_bit3 -5729734000000*x104_bit_7 -11459468000000*x104_bit_6 -22918936000000*x104_bit_5 -45837872000000*x104_bit_4 -91675744000000*x104_bit_3 -183351488000000*x104_bit_2 -366702976000000*x104_bit_1 -733405952000000*x104_bit0 -1466811904000000*x104_bit1 -2933623808000000*x104_bit2 -5867247616000000*x104_bit3 -710926900000000*x105_bit_7 -1421853800000000*x105_bit_6 -2843707600000000*x105_bit_5 -5687415200000000*x105_bit_4 -11374830400000000*x105_bit_3 -22749660800000000*x105_bit_2 -45499321600000000*x105_bit_1 -90998643200000000*x105_bit0 -181997286400000000*x105_bit1 -363994572800000000*x105_bit2 -727989145600000000*x105_bit3 -1954127000000*x106_bit_7 -3908254000000*x106_bit_6 -7816508000000*x106_bit_5 -15633016000000*x106_bit_4 -31266032000000*x106_bit_3 -62532064000000*x106_bit_2 -125064128000000*x106_bit_1 -250128256000000*x106_bit0 -500256512000000*x106_bit1 -1000513024000000*x106_bit2 -2001026048000000*x106_bit3 -29195360000000*x107_bit_7 -58390720000000*x107_bit_6 -116781440000000*x107_bit_5 -233562880000000*x107_bit_4 -467125760000000*x107_bit_3 -934251520000000*x107_bit_2 -1868503040000000*x107_bit_1 -3737006080000000*x107_bit0 -7474012160000000*x107_bit1 -14948024320000000*x107_bit2 -29896048640000000*x107_bit3 -3460195000000*x109_bit_7 -6920390000000*x109_bit_6 -13840780000000*x109_bit_5 -27681560000000*x109_bit_4 -55363120000000*x109_bit_3 -110726240000000*x109_bit_2 -221452480000000*x109_bit_1 -442904960000000*x109_bit0 -885809920000000*x109_bit1 -1771619840000000*x109_bit2 -3543239680000000*x109_bit3 -48416790000000*x110_bit_7 -96833580000000*x110_bit_6 -193667160000000*x110_bit_5 -387334320000000*x110_bit_4 -774668640000000*x110_bit_3 -1549337280000000*x110_bit_2 -3098674560000000*x110_bit_1 -6197349120000000*x110_bit0 -12394698240000000*x110_bit1 -24789396480000000*x110_bit2 -49578792960000000*x110_bit3 -127479998054400*x111_bit_7 -254959996108800*x111_bit_6 -509919992217600*x111_bit_5 -1019839984435200*x111_bit_4 -2039679968870400*x111_bit_3 -4079359937740800*x111_bit_2 -8158719875481600*x111_bit_1 -16317439750963200*x111_bit0 -32634879501926400*x111_bit1 -65269759003852800*x111_bit2 -130539518007705600*x111_bit3 -4876073000000*x112_bit_7 -9752146000000*x112_bit_6 -19504292000000*x112_bit_5 -39008584000000*x112_bit_4 -78017168000000*x112_bit_3 -156034336000000*x112_bit_2 -312068672000000*x112_bit_1 -624137344000000*x112_bit0 -1248274688000000*x112_bit1 -2496549376000000*x112_bit2 -4993098752000000*x112_bit3 -65530520000000*x113_bit_7 -131061040000000*x113_bit_6 -262122080000000*x113_bit_5 -524244160000000*x113_bit_4 -1048488320000000*x113_bit_3 -2096976640000000*x113_bit_2 -4193953280000000*x113_bit_1 -8387906560000000*x113_bit0 -16775813120000000*x113_bit1 -33551626240000000*x113_bit2 -67103252480000000*x113_bit3 -284439*x115_bit_7 -568878*x115_bit_6 -1137756*x115_bit_5 -2275512*x115_bit_4 -4551024*x115_bit_3 -9102048*x115_bit_2 -18204096*x115_bit_1 -36408192*x115_bit0 -72816384*x115_bit1 -145632768*x115_bit2 -291265536*x115_bit3 -19604500*x116_bit_7 -39209000*x116_bit_6 -78418000*x116_bit_5 -156836000*x116_bit_4 -313672000*x116_bit_3 -627344000*x116_bit_2 -1254688000*x116_bit_1 -2509376000*x116_bit0 -5018752000*x116_bit1 -10037504000*x116_bit2 -20075008000*x116_bit3 -32480210000*x117_bit_7 -64960420000*x117_bit_6 -129920840000*x117_bit_5 -259841680000*x117_bit_4 -519683360000*x117_bit_3 -1039366720000*x117_bit_2 -2078733440000*x117_bit_1 -4157466880000*x117_bit0 -8314933760000*x117_bit1 -16629867520000*x117_bit2 -33259735040000*x117_bit3 -19129200*x120_bit_7 -38258400*x120_bit_6 -76516800*x120_bit_5 -153033600*x120_bit_4 -306067200*x120_bit_3 -612134400*x120_bit_2 -1224268800*x120_bit_1 -2448537600*x120_bit0 -4897075200*x120_bit1 -9794150400*x120_bit2 -19588300800*x120_bit3 -77582030000*x121_bit_7 -155164060000*x121_bit_6 -310328120000*x121_bit_5 -620656240000*x121_bit_4 -1241312480000*x121_bit_3 -2482624960000*x121_bit_2 -4965249920000*x121_bit_1 -9930499840000*x121_bit0 -19860999680000*x121_bit1 -39721999360000*x121_bit2 -79443998720000*x121_bit3 -1677633000000*x122_bit_7 -3355266000000*x122_bit_6 -6710532000000*x122_bit_5 -13421064000000*x122_bit_4 -26842128000000*x122_bit_3 -53684256000000*x122_bit_2 -107368512000000*x122_bit_1 -214737024000000*x122_bit0 -429474048000000*x122_bit1 -858948096000000*x122_bit2 -1717896192000000*x122_bit3 -277943200000000*x123_bit_7 -555886400000000*x123_bit_6 -1111772800000000*x123_bit_5 -2223545600000000*x123_bit_4 -4447091200000000*x123_bit_3 -8894182400000000*x123_bit_2 -17788364800000000*x123_bit_1 -35576729600000000*x123_bit0 -71153459200000000*x123_bit1 -142306918400000000*x123_bit2 -284613836800000000*x123_bit3 -174963100000*x124_bit_7 -349926200000*x124_bit_6 -699852400000*x124_bit_5 -1399704800000*x124_bit_4 -2799409600000*x124_bit_3 -5598819200000*x124_bit_2 -11197638400000*x124_bit_1 -22395276800000*x124_bit0 -44790553600000*x124_bit1 -89581107200000*x124_bit2 -179162214400000*x124_bit3 -3436476000000*x125_bit_7 -6872952000000*x125_bit_6 -13745904000000*x125_bit_5 -27491808000000*x125_bit_4 -54983616000000*x125_bit_3 -109967232000000*x125_bit_2 -219934464000000*x125_bit_1 -439868928000000*x125_bit0 -879737856000000*x125_bit1 -1759475712000000*x125_bit2 -3518951424000000*x125_bit3 -481942900000000*x126_bit_7 -963885800000000*x126_bit_6 -1927771600000000*x126_bit_5 -3855543200000000*x126_bit_4 -7711086400000000*x126_bit_3 -15422172800000000*x126_bit_2 -30844345600000000*x126_bit_1 -61688691200000000*x126_bit0 -123377382400000000*x126_bit1 -246754764800000000*x126_bit2 -493509529600000000*x126_bit3 -312615600000*x127_bit_7 -625231200000*x127_bit_6 -1250462400000*x127_bit_5 -2500924800000*x127_bit_4 -5001849600000*x127_bit_3 -10003699200000*x127_bit_2 -20007398400000*x127_bit_1 -40014796800000*x127_bit0 -80029593600000*x127_bit1 -160059187200000*x127_bit2 -320118374400000*x127_bit3 -5729734000000*x128_bit_7 -11459468000000*x128_bit_6 -22918936000000*x128_bit_5 -45837872000000*x128_bit_4 -91675744000000*x128_bit_3 -183351488000000*x128_bit_2 -366702976000000*x128_bit_1 -733405952000000*x128_bit0 -1466811904000000*x128_bit1 -2933623808000000*x128_bit2 -5867247616000000*x128_bit3 -710926900000000*x129_bit_7 -1421853800000000*x129_bit_6 -2843707600000000*x129_bit_5 -5687415200000000*x129_bit_4 -11374830400000000*x129_bit_3 -22749660800000000*x129_bit_2 -45499321600000000*x129_bit_1 -90998643200000000*x129_bit0 -181997286400000000*x129_bit1 -363994572800000000*x129_bit2 -727989145600000000*x129_bit3 -442755300000*x130_bit_7 -885510600000*x130_bit_6 -1771021200000*x130_bit_5 -3542042400000*x130_bit_4 -7084084800000*x130_bit_3 -14168169600000*x130_bit_2 -28336339200000*x130_bit_1 -56672678400000*x130_bit0 -113345356800000*x130_bit1 -226690713600000*x130_bit2 -453381427200000*x130_bit3 -7782947000000*x131_bit_7 -15565894000000*x131_bit_6 -31131788000000*x131_bit_5 -62263576000000*x131_bit_4 -124527152000000*x131_bit_3 -249054304000000*x131_bit_2 -498108608000000*x131_bit_1 -996217216000000*x131_bit0 -1992434432000000*x131_bit1 -3984868864000000*x131_bit2 -7969737728000000*x131_bit3 -896012700000000*x132_bit_7 -1792025400000000*x132_bit_6 -3584050800000000*x132_bit_5 -7168101600000000*x132_bit_4 -14336203200000000*x132_bit_3 -28672406400000000*x132_bit_2 -57344812800000000*x132_bit_1 -114689625600000000*x132_bit0 -229379251200000000*x132_bit1 -458758502400000000*x132_bit2 -917517004800000000*x132_bit3 -359823*x133_bit_7 -719646*x133_bit_6 -1439292*x133_bit_5 -2878584*x133_bit_4 -5757168*x133_bit_3 -11514336*x133_bit_2 -23028672*x133_bit_1 -46057344*x133_bit0 -92114688*x133_bit1 -184229376*x133_bit2 -368458752*x133_bit3 -24340300*x134_bit_7 -48680600*x134_bit_6 -97361200*x134_bit_5 -194722400*x134_bit_4 -389444800*x134_bit_3 -778889600*x134_bit_2 -1557779200*x134_bit_1 -3115558400*x134_bit0 -6231116800*x134_bit1 -12462233600*x134_bit2 -24924467200*x134_bit3 -38845690000*x135_bit_7 -77691380000*x135_bit_6 -155382760000*x135_bit_5 -310765520000*x135_bit_4 -621531040000*x135_bit_3 -1243062080000*x135_bit_2 -2486124160000*x135_bit_1 -4972248320000*x135_bit0 -9944496640000*x135_bit1 -19888993280000*x135_bit2 -39777986560000*x135_bit3 -1866442000*x136_bit_7 -3732884000*x136_bit_6 -7465768000*x136_bit_5 -14931536000*x136_bit_4 -29863072000*x136_bit_3 -59726144000*x136_bit_2 -119452288000*x136_bit_1 -238904576000*x136_bit0 -477809152000*x136_bit1 -955618304000*x136_bit2 -1911236608000*x136_bit3 -59836770000*x137_bit_7 -119673540000*x137_bit_6 -239347080000*x137_bit_5 -478694160000*x137_bit_4 -957388320000*x137_bit_3 -1914776640000*x137_bit_2 -3829553280000*x137_bit_1 -7659106560000*x137_bit0 -15318213120000*x137_bit1 -30636426240000*x137_bit2 -61272852480000*x137_bit3 -20763460000000*x138_bit_7 -41526920000000*x138_bit_6 -83053840000000*x138_bit_5 -166107680000000*x138_bit_4 -332215360000000*x138_bit_3 -664430720000000*x138_bit_2 -1328861440000000*x138_bit_1 -2657722880000000*x138_bit0 -5315445760000000*x138_bit1 -10630891520000000*x138_bit2 -21261783040000000*x138_bit3 -5332805000*x139_bit_7 -10665610000*x139_bit_6 -21331220000*x139_bit_5 -42662440000*x139_bit_4 -85324880000*x139_bit_3 -170649760000*x139_bit_2 -341299520000*x139_bit_1 -682599040000*x139_bit0 -1365198080000*x139_bit1 -2730396160000*x139_bit2 -5460792320000*x139_bit3 -154431300000*x140_bit_7 -308862600000*x140_bit_6 -617725200000*x140_bit_5 -1235450400000*x140_bit_4 -2470900800000*x140_bit_3 -4941801600000*x140_bit_2 -9883603200000*x140_bit_1 -19767206400000*x140_bit0 -39534412800000*x140_bit1 -79068825600000*x140_bit2 -158137651200000*x140_bit3 -43568870000000*x141_bit_7 -87137740000000*x141_bit_6 -174275480000000*x141_bit_5 -348550960000000*x141_bit_4 -697101920000000*x141_bit_3 -1394203840000000*x141_bit_2 -2788407680000000*x141_bit_1 -5576815360000000*x141_bit0 -11153630720000000*x141_bit1 -22307261440000000*x141_bit2 -44614522880000000*x141_bit3 -12056530000*x142_bit_7 -24113060000*x142_bit_6 -48226120000*x142_bit_5 -96452240000*x142_bit_4 -192904480000*x142_bit_3 -385808960000*x142_bit_2 -771617920000*x142_bit_1 -1543235840000*x142_bit0 -3086471680000*x142_bit1 -6172943360000*x142_bit2 -12345886720000*x142_bit3 -322000200000*x143_bit_7 -644000400000*x143_bit_6 -1288000800000*x143_bit_5 -2576001600000*x143_bit_4 -5152003200000*x143_bit_3 -10304006400000*x143_bit_2 -20608012800000*x143_bit_1 -41216025600000*x143_bit0 -82432051200000*x143_bit1 -164864102400000*x143_bit2 -329728204800000*x143_bit3 -77088230000000*x144_bit_7 -154176460000000*x144_bit_6 -308352920000000*x144_bit_5 -616705840000000*x144_bit_4 -1233411680000000*x144_bit_3 -2466823360000000*x144_bit_2 -4933646720000000*x144_bit_1 -9867293440000000*x144_bit0 -19734586880000000*x144_bit1 -39469173760000000*x144_bit2 -78938347520000000*x144_bit3 -21581160000*x145_bit_7 -43162320000*x145_bit_6 -86324640000*x145_bit_5 -172649280000*x145_bit_4 -345298560000*x145_bit_3 -690597120000*x145_bit_2 -1381194240000*x145_bit_1 -2762388480000*x145_bit0 -5524776960000*x145_bit1 -11049553920000*x145_bit2 -22099107840000*x145_bit3 -542477200000*x146_bit_7 -1084954400000*x146_bit_6 -2169908800000*x146_bit_5 -4339817600000*x146_bit_4 -8679635200000*x146_bit_3 -17359270400000*x146_bit_2 -34718540800000*x146_bit_1 -69437081600000*x146_bit0 -138874163200000*x146_bit1 -277748326400000*x146_bit2 -555496652800000*x146_bit3 -115483400000000*x147_bit_7 -230966800000000*x147_bit_6 -461933600000000*x147_bit_5 -923867200000000*x147_bit_4 -1847734400000000*x147_bit_3 -3695468800000000*x147_bit_2 -7390937600000000*x147_bit_1 -14781875200000000*x147_bit0 -29563750400000000*x147_bit1 -59127500800000000*x147_bit2 -118255001600000000*x147_bit3 -2008060*x149_bit_7 -4016120*x149_bit_6 -8032240*x149_bit_5 -16064480*x149_bit_4 -32128960*x149_bit_3 -64257920*x149_bit_2 -128515840*x149_bit_1 -257031680*x149_bit0 -514063360*x149_bit1 -1028126720*x149_bit2 -2056253440*x149_bit3 -4886887000*x150_bit_7 -9773774000*x150_bit_6 -19547548000*x150_bit_5 -39095096000*x150_bit_4 -78190192000*x150_bit_3 -156380384000*x150_bit_2 -312760768000*x150_bit_1 -625521536000*x150_bit0 -1251043072000*x150_bit1 -2502086144000*x150_bit2 -5004172288000*x150_bit3 -58780200*x153_bit_7 -117560400*x153_bit_6 -235120800*x153_bit_5 -470241600*x153_bit_4 -940483200*x153_bit_3 -1880966400*x153_bit_2 -3761932800*x153_bit_1 -7523865600*x153_bit0 -15047731200*x153_bit1 -30095462400*x153_bit2 -60190924800*x153_bit3 -296318*x156_bit_7 -592636*x156_bit_6 -1185272*x156_bit_5 -2370544*x156_bit_4 -4741088*x156_bit_3 -9482176*x156_bit_2 -18964352*x156_bit_1 -37928704*x156_bit0 -75857408*x156_bit1 -151714816*x156_bit2 -303429632*x156_bit3 -287900000*x157_bit_7 -575800000*x157_bit_6 -1151600000*x157_bit_5 -2303200000*x157_bit_4 -4606400000*x157_bit_3 -9212800000*x157_bit_2 -18425600000*x157_bit_1 -36851200000*x157_bit0 -73702400000*x157_bit1 -147404800000*x157_bit2 -294809600000*x157_bit3 -10993580000*x158_bit_7 -21987160000*x158_bit_6 -43974320000*x158_bit_5 -87948640000*x158_bit_4 -175897280000*x158_bit_3 -351794560000*x158_bit_2 -703589120000*x158_bit_1 -1407178240000*x158_bit0 -2814356480000*x158_bit1 -5628712960000*x158_bit2 -11257425920000*x158_bit3 -5459485000000*x159_bit_7 -10918970000000*x159_bit_6 -21837940000000*x159_bit_5 -43675880000000*x159_bit_4 -87351760000000*x159_bit_3 -174703520000000*x159_bit_2 -349407040000000*x159_bit_1 -698814080000000*x159_bit0 -1397628160000000*x159_bit1 -2795256320000000*x159_bit2 -5590512640000000*x159_bit3 -652497000*x160_bit_7 -1304994000*x160_bit_6 -2609988000*x160_bit_5 -5219976000*x160_bit_4 -10439952000*x160_bit_3 -20879904000*x160_bit_2 -41759808000*x160_bit_1 -83519616000*x160_bit0 -167039232000*x160_bit1 -334078464000*x160_bit2 -668156928000*x160_bit3 -23101430000*x161_bit_7 -46202860000*x161_bit_6 -92405720000*x161_bit_5 -184811440000*x161_bit_4 -369622880000*x161_bit_3 -739245760000*x161_bit_2 -1478491520000*x161_bit_1 -2956983040000*x161_bit0 -5913966080000*x161_bit1 -11827932160000*x161_bit2 -23655864320000*x161_bit3 -9820125000000*x162_bit_7 -19640250000000*x162_bit_6 -39280500000000*x162_bit_5 -78561000000000*x162_bit_4 -157122000000000*x162_bit_3 -314244000000000*x162_bit_2 -628488000000000*x162_bit_1 -1256976000000000*x162_bit0 -2513952000000000*x162_bit1 -5027904000000000*x162_bit2 -10055808000000000*x162_bit3 -1170076000*x163_bit_7 -2340152000*x163_bit_6 -4680304000*x163_bit_5 -9360608000*x163_bit_4 -18721216000*x163_bit_3 -37442432000*x163_bit_2 -74884864000*x163_bit_1 -149769728000*x163_bit0 -299539456000*x163_bit1 -599078912000*x163_bit2 -1198157824000*x163_bit3 -39215120000*x164_bit_7 -78430240000*x164_bit_6 -156860480000*x164_bit_5 -313720960000*x164_bit_4 -627441920000*x164_bit_3 -1254883840000*x164_bit_2 -2509767680000*x164_bit_1 -5019535360000*x164_bit0 -10039070720000*x164_bit1 -20078141440000*x164_bit2 -40156282880000*x164_bit3 -14899080000000*x165_bit_7 -29798160000000*x165_bit_6 -59596320000000*x165_bit_5 -119192640000000*x165_bit_4 -238385280000000*x165_bit_3 -476770560000000*x165_bit_2 -953541120000000*x165_bit_1 -1907082240000000*x165_bit0 -3814164480000000*x165_bit1 -7628328960000000*x165_bit2 -15256657920000000*x165_bit3 -1660824000*x166_bit_7 -3321648000*x166_bit_6 -6643296000*x166_bit_5 -13286592000*x166_bit_4 -26573184000*x166_bit_3 -53146368000*x166_bit_2 -106292736000*x166_bit_1 -212585472000*x166_bit0 -425170944000*x166_bit1 -850341888000*x166_bit2 -1700683776000*x166_bit3 -53841610000*x167_bit_7 -107683220000*x167_bit_6 -215366440000*x167_bit_5 -430732880000*x167_bit_4 -861465760000*x167_bit_3 -1722931520000*x167_bit_2 -3445863040000*x167_bit_1 -6891726080000*x167_bit0 -13783452160000*x167_bit1 -27566904320000*x167_bit2 -55133808640000*x167_bit3 -19112810000000*x168_bit_7 -38225620000000*x168_bit_6 -76451240000000*x168_bit_5 -152902480000000*x168_bit_4 -305804960000000*x168_bit_3 -611609920000000*x168_bit_2 -1223219840000000*x168_bit_1 -2446439680000000*x168_bit0 -4892879360000000*x168_bit1 -9785758720000000*x168_bit2 -19571517440000000*x168_bit3 -1299290*x170_bit_7 -2598580*x170_bit_6 -5197160*x170_bit_5 -10394320*x170_bit_4 -20788640*x170_bit_3 -41577280*x170_bit_2 -83154560*x170_bit_1 -166309120*x170_bit0 -332618240*x170_bit1 -665236480*x170_bit2 -1330472960*x170_bit3 -3396778000*x171_bit_7 -6793556000*x171_bit_6 -13587112000*x171_bit_5 -27174224000*x171_bit_4 -54348448000*x171_bit_3 -108696896000*x171_bit_2 -217393792000*x171_bit_1 -434787584000*x171_bit0 -869575168000*x171_bit1 -1739150336000*x171_bit2 -3478300672000*x171_bit3 -434097*x174_bit_7 -868194*x174_bit_6 -1736388*x174_bit_5 -3472776*x174_bit_4 -6945552*x174_bit_3 -13891104*x174_bit_2 -27782208*x174_bit_1 -55564416*x174_bit0 -111128832*x174_bit1 -222257664*x174_bit2 -444515328*x174_bit3 -27700300*x178_bit_7 -55400600*x178_bit_6 -110801200*x178_bit_5 -221602400*x178_bit_4 -443204800*x178_bit_3 -886409600*x178_bit_2 -1772819200*x178_bit_1 -3545638400*x178_bit0 -7091276800*x178_bit1 -14182553600*x178_bit2 -28365107200*x178_bit3 -1303603000*x179_bit_7 -2607206000*x179_bit_6 -5214412000*x179_bit_5 -10428824000*x179_bit_4 -20857648000*x179_bit_3 -41715296000*x179_bit_2 -83430592000*x179_bit_1 -166861184000*x179_bit0 -333722368000*x179_bit1 -667444736000*x179_bit2 -1334889472000*x179_bit3 -1000922000000*x180_bit_7 -2001844000000*x180_bit_6 -4003688000000*x180_bit_5 -8007376000000*x180_bit_4 -16014752000000*x180_bit_3 -32029504000000*x180_bit_2 -64059008000000*x180_bit_1 -128118016000000*x180_bit0 -256236032000000*x180_bit1 -512472064000000*x180_bit2 -1024944128000000*x180_bit3 -49759800*x181_bit_7 -99519600*x181_bit_6 -199039200*x181_bit_5 -398078400*x181_bit_4 -796156800*x181_bit_3 -1592313600*x181_bit_2 -3184627200*x181_bit_1 -6369254400*x181_bit0 -12738508800*x181_bit1 -25477017600*x181_bit2 -50954035200*x181_bit3 -2224588000*x182_bit_7 -4449176000*x182_bit_6 -8898352000*x182_bit_5 -17796704000*x182_bit_4 -35593408000*x182_bit_3 -71186816000*x182_bit_2 -142373632000*x182_bit_1 -284747264000*x182_bit0 -569494528000*x182_bit1 -1138989056000*x182_bit2 -2277978112000*x182_bit3 -1533233000000*x183_bit_7 -3066466000000*x183_bit_6 -6132932000000*x183_bit_5 -12265864000000*x183_bit_4 -24531728000000*x183_bit_3 -49063456000000*x183_bit_2 -98126912000000*x183_bit_1 -196253824000000*x183_bit0 -392507648000000*x183_bit1 -785015296000000*x183_bit2 -1570030592000000*x183_bit3 -70705100*x184_bit_7 -141410200*x184_bit_6 -282820400*x184_bit_5 -565640800*x184_bit_4 -1131281600*x184_bit_3 -2262563200*x184_bit_2 -4525126400*x184_bit_1 -9050252800*x184_bit0 -18100505600*x184_bit1 -36201011200*x184_bit2 -72402022400*x184_bit3 -3064242000*x185_bit_7 -6128484000*x185_bit_6 -12256968000*x185_bit_5 -24513936000*x185_bit_4 -49027872000*x185_bit_3 -98055744000*x185_bit_2 -196111488000*x185_bit_1 -392222976000*x185_bit0 -784445952000*x185_bit1 -1568891904000*x185_bit2 -3137783808000*x185_bit3 -1978922000000*x186_bit_7 -3957844000000*x186_bit_6 -7915688000000*x186_bit_5 -15831376000000*x186_bit_4 -31662752000000*x186_bit_3 -63325504000000*x186_bit_2 -126651008000000*x186_bit_1 -253302016000000*x186_bit0 -506604032000000*x186_bit1 -1013208064000000*x186_bit2 -2026416128000000*x186_bit3 -40460500*x189_bit_7 -80921000*x189_bit_6 -161842000*x189_bit_5 -323684000*x189_bit_4 -647368000*x189_bit_3 -1294736000*x189_bit_2 -2589472000*x189_bit_1 -5178944000*x189_bit0 -10357888000*x189_bit1 -20715776000*x189_bit2 -41431552000*x189_bit3 -4660820*x192_bit_7 -9321640*x192_bit_6 -18643280*x192_bit_5 -37286560*x192_bit_4 -74573120*x192_bit_3 -149146240*x192_bit_2 -298292480*x192_bit_1 -596584960*x192_bit0 -1193169920*x192_bit1 -2386339840*x192_bit2 -4772679680*x192_bit3 -3102070*x200_bit_7 -6204140*x200_bit_6 -12408280*x200_bit_5 -24816560*x200_bit_4 -49633120*x200_bit_3 -99266240*x200_bit_2 -198532480*x200_bit_1 -397064960*x200_bit0 -794129920*x200_bit1 -1588259840*x200_bit2 -3176519680*x200_bit3 -7024233000*x201_bit_7 -14048466000*x201_bit_6 -28096932000*x201_bit_5 -56193864000*x201_bit_4 -112387728000*x201_bit_3 -224775456000*x201_bit_2 -449550912000*x201_bit_1 -899101824000*x201_bit0 -1798203648000*x201_bit1 -3596407296000*x201_bit2 -7192814592000*x201_bit3 -140443*x202_bit_7 -280886*x202_bit_6 -561772*x202_bit_5 -1123544*x202_bit_4 -2247088*x202_bit_3 -4494176*x202_bit_2 -8988352*x202_bit_1 -17976704*x202_bit0 -35953408*x202_bit1 -71906816*x202_bit2 -143813632*x202_bit3 -10236400*x203_bit_7 -20472800*x203_bit_6 -40945600*x203_bit_5 -81891200*x203_bit_4 -163782400*x203_bit_3 -327564800*x203_bit_2 -655129600*x203_bit_1 -1310259200*x203_bit0 -2620518400*x203_bit1 -5241036800*x203_bit2 -10482073600*x203_bit3 -18957700000*x204_bit_7 -37915400000*x204_bit_6 -75830800000*x204_bit_5 -151661600000*x204_bit_4 -303323200000*x204_bit_3 -606646400000*x204_bit_2 -1213292800000*x204_bit_1 -2426585600000*x204_bit0 -4853171200000*x204_bit1 -9706342400000*x204_bit2 -19412684800000*x204_bit3 -1658220*x205_bit_7 -3316440*x205_bit_6 -6632880*x205_bit_5 -13265760*x205_bit_4 -26531520*x205_bit_3 -53063040*x205_bit_2 -106126080*x205_bit_1 -212252160*x205_bit0 -424504320*x205_bit1 -849008640*x205_bit2 -1698017280*x205_bit3 -99057400*x206_bit_7 -198114800*x206_bit_6 -396229600*x206_bit_5 -792459200*x206_bit_4 -1584918400*x206_bit_3 -3169836800*x206_bit_2 -6339673600*x206_bit_1 -12679347200*x206_bit0 -25358694400*x206_bit1 -50717388800*x206_bit2 -101434777600*x206_bit3 -123525900000*x207_bit_7 -247051800000*x207_bit_6 -494103600000*x207_bit_5 -988207200000*x207_bit_4 -1976414400000*x207_bit_3 -3952828800000*x207_bit_2 -7905657600000*x207_bit_1 -15811315200000*x207_bit0 -31622630400000*x207_bit1 -63245260800000*x207_bit2 -126490521600000*x207_bit3 -2652320*x208_bit_7 -5304640*x208_bit_6 -10609280*x208_bit_5 -21218560*x208_bit_4 -42437120*x208_bit_3 -84874240*x208_bit_2 -169748480*x208_bit_1 -339496960*x208_bit0 -678993920*x208_bit1 -1357987840*x208_bit2 -2715975680*x208_bit3 -152403000*x209_bit_7 -304806000*x209_bit_6 -609612000*x209_bit_5 -1219224000*x209_bit_4 -2438448000*x209_bit_3 -4876896000*x209_bit_2 -9753792000*x209_bit_1 -19507584000*x209_bit0 -39015168000*x209_bit1 -78030336000*x209_bit2 -156060672000*x209_bit3 -175930100000*x210_bit_7 -351860200000*x210_bit_6 -703720400000*x210_bit_5 -1407440800000*x210_bit_4 -2814881600000*x210_bit_3 -5629763200000*x210_bit_2 -11259526400000*x210_bit_1 -22519052800000*x210_bit0 -45038105600000*x210_bit1 -90076211200000*x210_bit2 -180152422400000*x210_bit3 -1658220*x211_bit_7 -3316440*x211_bit_6 -6632880*x211_bit_5 -13265760*x211_bit_4 -26531520*x211_bit_3 -53063040*x211_bit_2 -106126080*x211_bit_1 -212252160*x211_bit0 -424504320*x211_bit1 -849008640*x211_bit2 -1698017280*x211_bit3 -99057400*x212_bit_7 -198114800*x212_bit_6 -396229600*x212_bit_5 -792459200*x212_bit_4 -1584918400*x212_bit_3 -3169836800*x212_bit_2 -6339673600*x212_bit_1 -12679347200*x212_bit0 -25358694400*x212_bit1 -50717388800*x212_bit2 -101434777600*x212_bit3 -123525900000*x213_bit_7 -247051800000*x213_bit_6 -494103600000*x213_bit_5 -988207200000*x213_bit_4 -1976414400000*x213_bit_3 -3952828800000*x213_bit_2 -7905657600000*x213_bit_1 -15811315200000*x213_bit0 -31622630400000*x213_bit1 -63245260800000*x213_bit2 -126490521600000*x213_bit3 -921485*x214_bit_7 -1842970*x214_bit_6 -3685940*x214_bit_5 -7371880*x214_bit_4 -14743760*x214_bit_3 -29487520*x214_bit_2 -58975040*x214_bit_1 -117950080*x214_bit0 -235900160*x214_bit1 -471800320*x214_bit2 -943600640*x214_bit3 -57769700*x215_bit_7 -115539400*x215_bit_6 -231078800*x215_bit_5 -462157600*x215_bit_4 -924315200*x215_bit_3 -1848630400*x215_bit_2 -3697260800*x215_bit_1 -7394521600*x215_bit0 -14789043200*x215_bit1 -29578086400*x215_bit2 -59156172800*x215_bit3 -79269190000*x216_bit_7 -158538380000*x216_bit_6 -317076760000*x216_bit_5 -634153520000*x216_bit_4 -1268307040000*x216_bit_3 -2536614080000*x216_bit_2 -5073228160000*x216_bit_1 -10146456320000*x216_bit0 -20292912640000*x216_bit1 -40585825280000*x216_bit2 -81171650560000*x216_bit3 -3102070*x218_bit_7 -6204140*x218_bit_6 -12408280*x218_bit_5 -24816560*x218_bit_4 -49633120*x218_bit_3 -99266240*x218_bit_2 -198532480*x218_bit_1 -397064960*x218_bit0 -794129920*x218_bit1 -1588259840*x218_bit2 -3176519680*x218_bit3 -7024233000*x219_bit_7 -14048466000*x219_bit_6 -28096932000*x219_bit_5 -56193864000*x219_bit_4 -112387728000*x219_bit_3 -224775456000*x219_bit_2 -449550912000*x219_bit_1 -899101824000*x219_bit0 -1798203648000*x219_bit1 -3596407296000*x219_bit2 -7192814592000*x219_bit3 -112800000*x222_bit_7 -225600000*x222_bit_6 -451200000*x222_bit_5 -902400000*x222_bit_4 -1804800000*x222_bit_3 -3609600000*x222_bit_2 -7219200000*x222_bit_1 -14438400000*x222_bit0 -28876800000*x222_bit1 -57753600000*x222_bit2 -115507200000*x222_bit3 -19129200*x225_bit_7 -38258400*x225_bit_6 -76516800*x225_bit_5 -153033600*x225_bit_4 -306067200*x225_bit_3 -612134400*x225_bit_2 -1224268800*x225_bit_1 -2448537600*x225_bit0 -4897075200*x225_bit1 -9794150400*x225_bit2 -19588300800*x225_bit3 -296318*x228_bit_7 -592636*x228_bit_6 -1185272*x228_bit_5 -2370544*x228_bit_4 -4741088*x228_bit_3 -9482176*x228_bit_2 -18964352*x228_bit_1 -37928704*x228_bit0 -75857408*x228_bit1 -151714816*x228_bit2 -303429632*x228_bit3 -105471*x239_bit_7 -210942*x239_bit_6 -421884*x239_bit_5 -843768*x239_bit_4 -1687536*x239_bit_3 -3375072*x239_bit_2 -6750144*x239_bit_1 -13500288*x239_bit0 -27000576*x239_bit1 -54001152*x239_bit2 -108002304*x239_bit3 -412491000*x240_bit_7 -824982000*x240_bit_6 -1649964000*x240_bit_5 -3299928000*x240_bit_4 -6599856000*x240_bit_3 -13199712000*x240_bit_2 -26399424000*x240_bit_1 -52798848000*x240_bit0 -105597696000*x240_bit1 -211195392000*x240_bit2 -422390784000*x240_bit3 -937139*x242_bit_7 -1874278*x242_bit_6 -3748556*x242_bit_5 -7497112*x242_bit_4 -14994224*x242_bit_3 -29988448*x242_bit_2 -59976896*x242_bit_1 -119953792*x242_bit0 -239907584*x242_bit1 -479815168*x242_bit2 -959630336*x242_bit3 -2584263000*x243_bit_7 -5168526000*x243_bit_6 -10337052000*x243_bit_5 -20674104000*x243_bit_4 -41348208000*x243_bit_3 -82696416000*x243_bit_2 -165392832000*x243_bit_1 -330785664000*x243_bit0 -661571328000*x243_bit1 -1323142656000*x243_bit2 -2646285312000*x243_bit3 -3458230*x245_bit_7 -6916460*x245_bit_6 -13832920*x245_bit_5 -27665840*x245_bit_4 -55331680*x245_bit_3 -110663360*x245_bit_2 -221326720*x245_bit_1 -442653440*x245_bit0 -885306880*x245_bit1 -1770613760*x245_bit2 -3541227520*x245_bit3 -7690018000*x246_bit_7 -15380036000*x246_bit_6 -30760072000*x246_bit_5 -61520144000*x246_bit_4 -123040288000*x246_bit_3 -246080576000*x246_bit_2 -492161152000*x246_bit_1 -984322304000*x246_bit0 -1968644608000*x246_bit1 -3937289216000*x246_bit2 -7874578432000*x246_bit3 -4790270*x248_bit_7 -9580540*x248_bit_6 -19161080*x248_bit_5 -38322160*x248_bit_4 -76644320*x248_bit_3 -153288640*x248_bit_2 -306577280*x248_bit_1 -613154560*x248_bit0 -1226309120*x248_bit1 -2452618240*x248_bit2 -4905236480*x248_bit3 -10086930000*x249_bit_7 -20173860000*x249_bit_6 -40347720000*x249_bit_5 -80695440000*x249_bit_4 -161390880000*x249_bit_3 -322781760000*x249_bit_2 -645563520000*x249_bit_1 -1291127040000*x249_bit0 -2582254080000*x249_bit1 -5164508160000*x249_bit2 -10329016320000*x249_bit3 -105471*x251_bit_7 -210942*x251_bit_6 -421884*x251_bit_5 -843768*x251_bit_4 -1687536*x251_bit_3 -3375072*x251_bit_2 -6750144*x251_bit_1 -13500288*x251_bit0 -27000576*x251_bit1 -54001152*x251_bit2 -108002304*x251_bit3 -412491000*x252_bit_7 -824982000*x252_bit_6 -1649964000*x252_bit_5 -3299928000*x252_bit_4 -6599856000*x252_bit_3 -13199712000*x252_bit_2 -26399424000*x252_bit_1 -52798848000*x252_bit0 -105597696000*x252_bit1 -211195392000*x252_bit2 -422390784000*x252_bit3 -1023180*x255_bit_7 -2046360*x255_bit_6 -4092720*x255_bit_5 -8185440*x255_bit_4 -16370880*x255_bit_3 -32741760*x255_bit_2 -65483520*x255_bit_1 -130967040*x255_bit0 -261934080*x255_bit1 -523868160*x255_bit2 -1047736320*x255_bit3 -19129200*x267_bit_7 -38258400*x267_bit_6 -76516800*x267_bit_5 -153033600*x267_bit_4 -306067200*x267_bit_3 -612134400*x267_bit_2 -1224268800*x267_bit_1 -2448537600*x267_bit0 -4897075200*x267_bit1 -9794150400*x267_bit2 -19588300800*x267_bit3 -123784000*x270_bit_7 -247568000*x270_bit_6 -495136000*x270_bit_5 -990272000*x270_bit_4 -1980544000*x270_bit_3 -3961088000*x270_bit_2 -7922176000*x270_bit_1 -15844352000*x270_bit0 -31688704000*x270_bit1 -63377408000*x270_bit2 -126754816000*x270_bit3 -236915000*x273_bit_7 -473830000*x273_bit_6 -947660000*x273_bit_5 -1895320000*x273_bit_4 -3790640000*x273_bit_3 -7581280000*x273_bit_2 -15162560000*x273_bit_1 -30325120000*x273_bit0 -60650240000*x273_bit1 -121300480000*x273_bit2 -242600960000*x273_bit3 -376124000*x276_bit_7 -752248000*x276_bit_6 -1504496000*x276_bit_5 -3008992000*x276_bit_4 -6017984000*x276_bit_3 -12035968000*x276_bit_2 -24071936000*x276_bit_1 -48143872000*x276_bit0 -96287744000*x276_bit1 -192575488000*x276_bit2 -385150976000*x276_bit3 -146438*x278_bit_7 -292876*x278_bit_6 -585752*x278_bit_5 -1171504*x278_bit_4 -2343008*x278_bit_3 -4686016*x278_bit_2 -9372032*x278_bit_1 -18744064*x278_bit0 -37488128*x278_bit1 -74976256*x278_bit2 -149952512*x278_bit3 -543915000*x279_bit_7 -1087830000*x279_bit_6 -2175660000*x279_bit_5 -4351320000*x279_bit_4 -8702640000*x279_bit_3 -17405280000*x279_bit_2 -34810560000*x279_bit_1 -69621120000*x279_bit0 -139242240000*x279_bit1 -278484480000*x279_bit2 -556968960000*x279_bit3 -131339*x281_bit_7 -262678*x281_bit_6 -525356*x281_bit_5 -1050712*x281_bit_4 -2101424*x281_bit_3 -4202848*x281_bit_2 -8405696*x281_bit_1 -16811392*x281_bit0 -33622784*x281_bit1 -67245568*x281_bit2 -134491136*x281_bit3 -496037000*x282_bit_7 -992074000*x282_bit_6 -1984148000*x282_bit_5 -3968296000*x282_bit_4 -7936592000*x282_bit_3 -15873184000*x282_bit_2 -31746368000*x282_bit_1 -63492736000*x282_bit0 -126985472000*x282_bit1 -253970944000*x282_bit2 -507941888000*x282_bit3 -1988740*x294_bit_7 -3977480*x294_bit_6 -7954960*x294_bit_5 -15909920*x294_bit_4 -31819840*x294_bit_3 -63639680*x294_bit_2 -127279360*x294_bit_1 -254558720*x294_bit0 -509117440*x294_bit1 -1018234880*x294_bit2 -2036469760*x294_bit3 -19129200*x297_bit_7 -38258400*x297_bit_6 -76516800*x297_bit_5 -153033600*x297_bit_4 -306067200*x297_bit_3 -612134400*x297_bit_2 -1224268800*x297_bit_1 -2448537600*x297_bit0 -4897075200*x297_bit1 -9794150400*x297_bit2 -19588300800*x297_bit3 -19129200*x300_bit_7 -38258400*x300_bit_6 -76516800*x300_bit_5 -153033600*x300_bit_4 -306067200*x300_bit_3 -612134400*x300_bit_2 -1224268800*x300_bit_1 -2448537600*x300_bit0 -4897075200*x300_bit1 -9794150400*x300_bit2 -19588300800*x300_bit3 -9018890*x303_bit_7 -18037780*x303_bit_6 -36075560*x303_bit_5 -72151120*x303_bit_4 -144302240*x303_bit_3 -288604480*x303_bit_2 -577208960*x303_bit_1 -1154417920*x303_bit0 -2308835840*x303_bit1 -4617671680*x303_bit2 -9235343360*x303_bit3 -699218*x306_bit_7 -1398436*x306_bit_6 -2796872*x306_bit_5 -5593744*x306_bit_4 -11187488*x306_bit_3 -22374976*x306_bit_2 -44749952*x306_bit_1 -89499904*x306_bit0 -178999808*x306_bit1 -357999616*x306_bit2 -715999232*x306_bit3 -202060*x309_bit_7 -404120*x309_bit_6 -808240*x309_bit_5 -1616480*x309_bit_4 -3232960*x309_bit_3 -6465920*x309_bit_2 -12931840*x309_bit_1 -25863680*x309_bit0 -51727360*x309_bit1 -103454720*x309_bit2 -206909440*x309_bit3 -269229*x330_bit_7 -538458*x330_bit_6 -1076916*x330_bit_5 -2153832*x330_bit_4 -4307664*x330_bit_3 -8615328*x330_bit_2 -17230656*x330_bit_1 -34461312*x330_bit0 -68922624*x330_bit1 -137845248*x330_bit2 -275690496*x330_bit3 -434097*x333_bit_7 -868194*x333_bit_6 -1736388*x333_bit_5 -3472776*x333_bit_4 -6945552*x333_bit_3 -13891104*x333_bit_2 -27782208*x333_bit_1 -55564416*x333_bit0 -111128832*x333_bit1 -222257664*x333_bit2 -444515328*x333_bit3 -577982*x336_bit_7 -1155964*x336_bit_6 -2311928*x336_bit_5 -4623856*x336_bit_4 -9247712*x336_bit_3 -18495424*x336_bit_2 -36990848*x336_bit_1 -73981696*x336_bit0 -147963392*x336_bit1 -295926784*x336_bit2 -591853568*x336_bit3 -635713*x339_bit_7 -1271426*x339_bit_6 -2542852*x339_bit_5 -5085704*x339_bit_4 -10171408*x339_bit_3 -20342816*x339_bit_2 -40685632*x339_bit_1 -81371264*x339_bit0 -162742528*x339_bit1 -325485056*x339_bit2 -650970112*x339_bit3 -577982*x342_bit_7 -1155964*x342_bit_6 -2311928*x342_bit_5 -4623856*x342_bit_4 -9247712*x342_bit_3 -18495424*x342_bit_2 -36990848*x342_bit_1 -73981696*x342_bit0 -147963392*x342_bit1 -295926784*x342_bit2 -591853568*x342_bit3 -269229*x345_bit_7 -538458*x345_bit_6 -1076916*x345_bit_5 -2153832*x345_bit_4 -4307664*x345_bit_3 -8615328*x345_bit_2 -17230656*x345_bit_1 -34461312*x345_bit0 -68922624*x345_bit1 -137845248*x345_bit2 -275690496*x345_bit3 -137778*x348_bit_7 -275556*x348_bit_6 -551112*x348_bit_5 -1102224*x348_bit_4 -2204448*x348_bit_3 -4408896*x348_bit_2 -8817792*x348_bit_1 -17635584*x348_bit0 -35271168*x348_bit1 -70542336*x348_bit2 -141084672*x348_bit3 +1000000000000000000*x492_bit_7 +2000000000000000000*x492_bit_6 +4000000000000000000*x492_bit_5 +8000000000000000000*x492_bit_4 +16000000000000000000*x492_bit_3 +32000000000000000000*x492_bit_2 +64000000000000000000*x492_bit_1 +128000000000000000000*x492_bit0 +256000000000000000000*x492_bit1 +512000000000000000000*x492_bit2 +1024000000000000000000*x492_bit3 +2048000000000000000000*x492_bit4 +4096000000000000000000*x492_bit5 +8192000000000000000000*x492_bit6 +16384000000000000000000*x492_bit7 +32768000000000000000000*x492_bit8 +65536000000000000000000*x492_bit9 +131072000000000000000000*x492_bit10 +262144000000000000000000*x492_bit11 +524288000000000000000000*x492_bit12 +1048576000000000000000000*x492_bit13 = +1048448000000000000000000;
c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-bc1.opb
s UNKNOWN
c Exit Code: 0
c Total time: 2.492 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.83 0.94 0.95 2/54 2571
Raw data (stat): 2571 (runsolver) R 2570 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 774224318 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 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+2.56954 s]
Raw data (loadavg): 0.83 0.94 0.95 1/53 2571
Raw data (stat): 2571 (runsolver) R 2570 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 774224318 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 0

Child status: 0
Real time (s): 2.56929
CPU time (s): 2.53861
CPU user time (s): 2.01569
CPU system time (s): 0.52292
CPU usage (%): 98.8059
Max. virtual memory (Kb): 1028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####