PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-protfold.opb
MD5SUM	c5ca7819a7dcae16ff6045242cdd1f87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-23
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	120
Number of bits of the sum of numbers in the objective function	7
Biggest number in a constraint	18
Number of bits of the biggest number in a constraint	5
Biggest sum of numbers in a constraint	900
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1176.86
Number of variables	1835
Total number of constraints	3947
Number of constraints which are clauses	1906
Number of constraints which are cardinality constraints (but not clauses)	1921
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	1
Maximum length of a constraint	882
Trace number 15314

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 03:55:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17932 boxname=wulflinc5 idbench=1380 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c5ca7819a7dcae16ff6045242cdd1f87  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-protfold.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-protfold.opb
IDLAUNCH: 17932
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        420440 kB
Buffers:         35716 kB
Cached:         555108 kB
SwapCached:         96 kB
Active:         180576 kB
Inactive:       413192 kB
HighTotal:      131008 kB
HighFree:        11984 kB
LowTotal:       903652 kB
LowFree:        408456 kB
SwapTotal:     2097136 kB
SwapFree:      2096952 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14580 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:15:34 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 17932 7 1200.42 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2149 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #####################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1908]---> BDD-cost:   98
c ---[1907]---> BDD-cost:   98
c ---[1906]---> BDD-cost:   98
c ---[1905]---> BDD-cost:   98
c ---[1904]---> BDD-cost:   98
c ---[1903]---> BDD-cost:   98
c ---[1902]---> BDD-cost:   98
c ---[1901]---> BDD-cost:   98
c ---[1900]---> BDD-cost:   98
c ---[1899]---> BDD-cost:   98
c ---[1898]---> BDD-cost:   98
c ---[1897]---> BDD-cost:   98
c ---[1896]---> BDD-cost:   98
c ---[1895]---> BDD-cost:   98
c ---[1894]---> BDD-cost:   98
c ---[1893]---> BDD-cost:   98
c ---[1892]---> BDD-cost:   98
c ---[1891]---> BDD-cost:   98
c ---[1890]---> BDD-cost:   98
c ---[1889]---> BDD-cost:   98
c ---[1888]---> BDD-cost:   98
c ---[1887]---> BDD-cost:   98
c ---[1886]---> BDD-cost:   98
c ---[1885]---> BDD-cost:   98
c ---[1884]---> BDD-cost:   98
c ---[1883]---> BDD-cost:   98
c ---[1882]---> BDD-cost:   98
c ---[1881]---> BDD-cost:   98
c ---[1880]---> BDD-cost:   98
c ---[1879]---> BDD-cost:   98
c ---[1878]---> BDD-cost:   98
c ---[1877]---> BDD-cost:   98
c ---[1876]---> BDD-cost:   98
c ---[1875]---> BDD-cost:   98
c ---[1874]---> BDD-cost:   98
c ---[1873]---> BDD-cost:   98
c ---[1872]---> BDD-cost:   98
c ---[1871]---> BDD-cost:   98
c ---[1870]---> BDD-cost:   98
c ---[1869]---> BDD-cost:   98
c ---[1868]---> BDD-cost:   98
c ---[1867]---> BDD-cost:   98
c ---[1866]---> BDD-cost:   98
c ---[1865]---> BDD-cost:   98
c ---[1864]---> BDD-cost:   98
c ---[1863]---> BDD-cost:   98
c ---[1862]---> BDD-cost:   98
c ---[1861]---> BDD-cost:   98
c ---[1860]---> BDD-cost:   98
c ---[1859]---> BDD-cost:   98
c ---[1858]---> BDD-cost:   98
c ---[1857]---> BDD-cost:   98
c ---[1856]---> BDD-cost:   98
c ---[1855]---> BDD-cost:   98
c ---[1854]---> BDD-cost:   98
c ---[1853]---> BDD-cost:   98
c ---[1852]---> BDD-cost:   98
c ---[1851]---> BDD-cost:   98
c ---[1850]---> BDD-cost:   98
c ---[1849]---> BDD-cost:   98
c ---[1848]---> BDD-cost:   98
c ---[1847]---> BDD-cost:   98
c ---[1846]---> BDD-cost:   98
c ---[1845]---> BDD-cost:   98
c ---[1844]---> BDD-cost:   98
c ---[1843]---> BDD-cost:   98
c ---[1842]---> BDD-cost:   98
c ---[1841]---> BDD-cost:   98
c ---[1840]---> BDD-cost:   98
c ---[1839]---> BDD-cost:   98
c ---[1838]---> BDD-cost:   98
c ---[1837]---> BDD-cost:   98
c ---[1836]---> BDD-cost:   98
c ---[1835]---> BDD-cost:   98
c ---[1834]---> BDD-cost:   98
c ---[1833]---> BDD-cost:   98
c ---[1832]---> BDD-cost:   98
c ---[1831]---> BDD-cost:   98
c ---[1830]---> BDD-cost:   98
c ---[1829]---> BDD-cost:   98
c ---[1828]---> BDD-cost:   98
c ---[1827]---> BDD-cost:   98
c ---[1826]---> BDD-cost:   98
c ---[1825]---> BDD-cost:   98
c ---[1824]---> BDD-cost:   98
c ---[1823]---> BDD-cost:   98
c ---[1822]---> BDD-cost:   98
c ---[1821]---> BDD-cost:   98
c ---[1820]---> BDD-cost:   98
c ---[1819]---> BDD-cost:   98
c ---[1818]---> BDD-cost:   98
c ---[1817]---> BDD-cost:   98
c ---[1816]---> BDD-cost:   98
c ---[1815]---> BDD-cost:   98
c ---[1814]---> BDD-cost:   98
c ---[1813]---> BDD-cost:   98
c ---[1812]---> BDD-cost:   98
c ---[1811]---> BDD-cost:   98
c ---[1810]---> BDD-cost:   98
c ---[1809]---> BDD-cost:   98
c ---[1808]---> BDD-cost:   98
c ---[1807]---> BDD-cost:   98
c ---[1806]---> BDD-cost:   98
c ---[1805]---> BDD-cost:   98
c ---[1804]---> BDD-cost:   98
c ---[1803]---> BDD-cost:   98
c ---[1802]---> BDD-cost:   98
c ---[1801]---> BDD-cost:   98
c ---[1800]---> BDD-cost:   98
c ---[1799]---> BDD-cost:   98
c ---[1798]---> BDD-cost:   98
c ---[1797]---> BDD-cost:   98
c ---[1796]---> BDD-cost:   98
c ---[1795]---> BDD-cost:   98
c ---[1794]---> BDD-cost:   98
c ---[1793]---> BDD-cost:   98
c ---[1792]---> BDD-cost:   98
c ---[1791]---> BDD-cost:   98
c ---[1790]---> BDD-cost:   98
c ---[1789]---> BDD-cost:   98
c ---[1787]---> Adder-cost: 1658   maxlim: 816   bits: 10/10
c ---[1785]---> Adder-cost: 1752   maxlim: 864   bits: 10/10
c ---[1783]---> BDD-cost:   95
c ---[1781]---> BDD-cost:   95
c ---[1779]---> BDD-cost:   95
c ---[1777]---> BDD-cost:   95
c ---[1775]---> BDD-cost:   95
c ---[1773]---> BDD-cost:   95
c ---[1771]---> BDD-cost:   95
c ---[1769]---> BDD-cost:   95
c ---[1767]---> BDD-cost:   95
c ---[1765]---> BDD-cost:   95
c ---[1763]---> BDD-cost:   95
c ---[1761]---> BDD-cost:   95
c ---[1759]---> BDD-cost:   95
c ---[1757]---> BDD-cost:   95
c ---[1755]---> BDD-cost:   95
c ---[1753]---> BDD-cost:   95
c ---[1751]---> BDD-cost:   95
c ---[1749]---> BDD-cost:   95
c ---[1747]---> BDD-cost:   95
c ---[1745]---> BDD-cost:   95
c ---[1743]---> BDD-cost:   95
c ---[1741]---> BDD-cost:   95
c ---[1739]---> BDD-cost:   95
c ---[1737]---> BDD-cost:   95
c ---[1735]---> BDD-cost:   95
c ---[1733]---> BDD-cost:   95
c ---[1731]---> BDD-cost:   95
c ---[1729]---> BDD-cost:   95
c ---[1727]---> BDD-cost:   95
c ---[1725]---> BDD-cost:   95
c ---[1723]---> BDD-cost:   95
c ---[1721]---> BDD-cost:   95
c ---[1719]---> BDD-cost:   95
c ---[1717]---> BDD-cost:   95
c ---[1715]---> BDD-cost:   95
c ---[1714]---> BDD-cost:   67
c ---[1713]---> BDD-cost:   67
c ---[1712]---> BDD-cost:   67
c ---[1711]---> BDD-cost:   67
c ---[1710]---> BDD-cost:   67
c ---[1709]---> BDD-cost:   67
c ---[1708]---> BDD-cost:   67
c ---[1707]---> BDD-cost:   67
c ---[1706]---> BDD-cost:   67
c ---[1705]---> BDD-cost:   67
c ---[1704]---> BDD-cost:   67
c ---[1703]---> BDD-cost:   67
c ---[1702]---> BDD-cost:   67
c ---[1701]---> BDD-cost:   67
c ---[1700]---> BDD-cost:   67
c ---[1699]---> BDD-cost:   67
c ---[1698]---> BDD-cost:   67
c ---[1697]---> BDD-cost:   67
c ---[1696]---> BDD-cost:   67
c ---[1695]---> BDD-cost:   67
c ---[1694]---> BDD-cost:   67
c ---[1693]---> BDD-cost:   67
c ---[1692]---> BDD-cost:   67
c ---[1691]---> BDD-cost:   67
c ---[1690]---> BDD-cost:   67
c ---[1689]---> BDD-cost:   67
c ---[1688]---> BDD-cost:   67
c ---[1687]---> BDD-cost:   67
c ---[1686]---> BDD-cost:   67
c ---[1685]---> BDD-cost:   67
c ---[1684]---> BDD-cost:   67
c ---[1683]---> BDD-cost:   67
c ---[1682]---> BDD-cost:   67
c ---[1681]---> BDD-cost:   67
c ---[1680]---> BDD-cost:   67
c ---[1679]---> BDD-cost:   67
c ---[1678]---> BDD-cost:   67
c ---[1677]---> BDD-cost:   67
c ---[1676]---> BDD-cost:   67
c ---[1675]---> BDD-cost:   67
c ---[1674]---> BDD-cost:   67
c ---[1673]---> BDD-cost:   67
c ---[1672]---> BDD-cost:   67
c ---[1671]---> BDD-cost:   67
c ---[1670]---> BDD-cost:   67
c ---[1669]---> BDD-cost:   67
c ---[1668]---> BDD-cost:   67
c ---[1667]---> BDD-cost:   67
c ---[1666]---> BDD-cost:   67
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   73037   226843 |   24345       0        0     nan |  0.000 % |
c |       103 |   73011   226755 |   26779     101     8954    88.7 |  1.045 % |
c ==============================================================================
c [1mFound solution: -19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2744     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       155 |   75766   233266 |   25255     153    12731    83.2 |  1.045 % |
c |       255 |   75766   233266 |   27780     253    17942    70.9 |  0.974 % |
c |       405 |   75766   233266 |   30558     403    34078    84.6 |  0.974 % |
c |       631 |   75766   233266 |   33614     629    53358    84.8 |  0.974 % |
c |       968 |   75766   233266 |   36975     966   113686   117.7 |  0.974 % |
c |      1474 |   75759   233243 |   40673    1471   156890   106.7 |  0.978 % |
c |      2235 |   75759   233243 |   44740    2232   301014   134.9 |  0.978 % |
c |      3375 |   75759   233243 |   49214    3372   428346   127.0 |  0.978 % |
c |      5083 |   75759   233243 |   54136    5080   595434   117.2 |  0.978 % |
c |      7648 |   75759   233243 |   59549    7645  1308768   171.2 |  0.978 % |
c |     11496 |   75759   233243 |   65504   11493  2006373   174.6 |  0.978 % |
c |     17263 |   75759   233243 |   72055   17260  3041655   176.2 |  0.978 % |
c |     25912 |   75759   233243 |   79261   25909  5528810   213.4 |  0.978 % |
c |     38891 |   75759   233243 |   87187   38888  7986840   205.4 |  0.978 % |
c |     58353 |   75759   233243 |   95905   58350 14831501   254.2 |  0.978 % |
c |     87546 |   75759   233243 |  105496   87543 19435262   222.0 |  0.978 % |
c |    131335 |   75752   233220 |  116046   41101  5658706   137.7 |  0.982 % |
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175373 |   75716   233147 |   25238   85136 20802504   244.3 |  0.982 % |
c |    175475 |   75716   233147 |   27761   15435  3944168   255.5 |  1.072 % |
c |    175628 |   75716   233147 |   30537   15588  3971074   254.8 |  1.072 % |
c |    175853 |   75716   233147 |   33591   15813  3997539   252.8 |  1.072 % |
c |    176190 |   75716   233147 |   36950   16150  4033186   249.7 |  1.072 % |
c |    176696 |   75716   233147 |   40646   16656  4118073   247.2 |  1.072 % |
c |    177459 |   75716   233147 |   44710   17419  4348647   249.6 |  1.072 % |
c |    178598 |   75716   233147 |   49181   18558  4497021   242.3 |  1.072 % |
c |    180307 |   75716   233147 |   54099   20267  4760378   234.9 |  1.072 % |
c |    182870 |   75716   233147 |   59509   22830  5498072   240.8 |  1.072 % |
c |    186716 |   75665   233018 |   65460   26673  6332616   237.4 |  1.151 % |
c |    192484 |   75665   233018 |   72006   32441  7694372   237.2 |  1.151 % |
c |    201133 |   75665   233018 |   79207   41090 10631407   258.7 |  1.151 % |
c |    214109 |   75658   232995 |   87128   54065 12859837   237.9 |  1.155 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -N_0x23_1_0x23_2_bit0 -N_0x23_2_0x23_3_bit0 -N_0x23_3_0x23_4_bit0 -N_0x23_4_0x23_5_bit0 -N_0x23_5_0x23_6_bit0 -N_0x23_6_0x23_7_bit0 -N_0x23_8_0x23_9_bit0 -N_0x23_9_0x23_10_bit0 -N_0x23_10_0x23_11_bit0 -N_0x23_11_0x23_12_bit0 -N_0x23_12_0x23_13_bit0 N_0x23_13_0x23_14_bit0 -N_0x23_15_0x23_16_bit0 -N_0x23_16_0x23_17_bit0 N_0x23_17_0x23_18_bit0 -N_0x23_18_0x23_19_bit0 -N_0x23_19_0x23_20_bit0 -N_0x23_20_0x23_21_bit0 -N_0x23_22_0x23_23_bit0 -N_0x23_23_0x23_24_bit0 -N_0x23_24_0x23_25_bit0 -N_0x23_25_0x23_26_bit0 -N_0x23_26_0x23_27_bit0 N_0x23_27_0x23_28_bit0 -N_0x23_29_0x23_30_bit0 -N_0x23_30_0x23_31_bit0 -N_0x23_31_0x23_32_bit0 N_0x23_32_0x23_33_bit0 -N_0x23_33_0x23_34_bit0 -N_0x23_34_0x23_35_bit0 -N_0x23_36_0x23_37_bit0 -N_0x23_37_0x23_38_bit0 N_0x23_38_0x23_39_bit0 N_0x23_39_0x23_40_bit0 -N_0x23_40_0x23_41_bit0 -N_0x23_41_0x23_42_bit0 -N_0x23_43_0x23_44_bit0 -N_0x23_44_0x23_45_bit0 -N_0x23_45_0x23_46_bit0 -N_0x23_46_0x23_47_bit0 -N_0x23_47_0x23_48_bit0 -N_0x23_48_0x23_49_bit0 -N_0x23_1_0x23_8_bit0 -N_0x23_2_0x23_9_bit0 N_0x23_3_0x23_10_bit0 -N_0x23_4_0x23_11_bit0 -N_0x23_5_0x23_12_bit0 -N_0x23_6_0x23_13_bit0 N_0x23_7_0x23_14_bit0 -N_0x23_8_0x23_15_bit0 -N_0x23_9_0x23_16_bit0 N_0x23_10_0x23_17_bit0 -N_0x23_11_0x23_18_bit0 -N_0x23_12_0x23_19_bit0 -N_0x23_13_0x23_20_bit0 -N_0x23_14_0x23_21_bit0 -N_0x23_15_0x23_22_bit0 -N_0x23_16_0x23_23_bit0 -N_0x23_17_0x23_24_bit0 N_0x23_18_0x23_25_bit0 -N_0x23_19_0x23_26_bit0 -N_0x23_20_0x23_27_bit0 -N_0x23_21_0x23_28_bit0 -N_0x23_22_0x23_29_bit0 -N_0x23_23_0x23_30_bit0 -N_0x23_24_0x23_31_bit0 N_0x23_25_0x23_32_bit0 -N_0x23_26_0x23_33_bit0 -N_0x23_27_0x23_34_bit0 N_0x23_28_0x23_35_bit0 -N_0x23_29_0x23_36_bit0 -N_0x23_30_0x23_37_bit0 -N_0x23_31_0x23_38_bit0 N_0x23_32_0x23_39_bit0 N_0x23_33_0x23_40_bit0 -N_0x23_34_0x23_41_bit0 -N_0x23_35_0x23_42_bit0 -N_0x23_36_0x23_43_bit0 -N_0x23_37_0x23_44_bit0 -N_0x23_38_0x23_45_bit0 -N_0x23_39_0x23_46_bit0 -N_0x23_40_0x23_47_bit0 -N_0x23_41_0x23_48_bit0 -N_0x23_42_0x23_49_bit0 -N_0x23_1_0x23_9_bit0 -N_0x23_2_0x23_10_bit0 -N_0x23_3_0x23_11_bit0 -N_0x23_4_0x23_12_bit0 N_0x23_5_0x23_13_bit0 -N_0x23_6_0x23_14_bit0 -N_0x23_8_0x23_16_bit0 -N_0x23_9_0x23_17_bit0 N_0x23_10_0x23_18_bit0 -N_0x23_11_0x23_19_bit0 -N_0x23_12_0x23_20_bit0 -N_0x23_13_0x23_21_bit0 -N_0x23_15_0x23_23_bit0 -N_0x23_16_0x23_24_bit0 N_0x23_17_0x23_25_bit0 -N_0x23_18_0x23_26_bit0 -N_0x23_19_0x23_27_bit0 -N_0x23_20_0x23_28_bit0 -N_0x23_22_0x23_30_bit0 -N_0x23_23_0x23_31_bit0 -N_0x23_24_0x23_32_bit0 N_0x23_25_0x23_33_bit0 -N_0x23_26_0x23_34_bit0 N_0x23_27_0x23_35_bit0 -N_0x23_29_0x23_37_bit0 -N_0x23_30_0x23_38_bit0 -N_0x23_31_0x23_39_bit0 N_0x23_32_0x23_40_bit0 -N_0x23_33_0x23_41_bit0 -N_0x23_34_0x23_42_bit0 -N_0x23_36_0x23_44_bit0 -N_0x23_37_0x23_45_bit0 -N_0x23_38_0x23_46_bit0 -N_0x23_39_0x23_47_bit0 -N_0x23_40_0x23_48_bit0 -N_0x23_41_0x23_49_bit0 -x_0x23_49_0x23_34_bit0 -x_0x23_49_0x23_32_bit0 -x_0x23_49_0x23_30_bit0 -x_0x23_49_0x23_29_bit0 -x_0x23_49_0x23_27_bit0 -x_0x23_49_0x23_26_bit0 -x_0x23_49_0x23_23_bit0 -x_0x23_49_0x23_20_bit0 -x_0x23_49_0x23_18_bit0 -x_0x23_49_0x23_16_bit0 -x_0x23_49_0x23_13_bit0 -x_0x23_49_0x23_11_bit0 -x_0x23_49_0x23_9_bit0 -x_0x23_49_0x23_8_bit0 -x_0x23_49_0x23_6_bit0 -x_0x23_49_0x23_3_bit0 -x_0x23_49_0x23_1_bit0 -x_0x23_48_0x23_34_bit0 -x_0x23_48_0x23_32_bit0 -x_0x23_48_0x23_30_bit0 -x_0x23_48_0x23_29_bit0 -x_0x23_48_0x23_27_bit0 -x_0x23_48_0x23_26_bit0 -x_0x23_48_0x23_23_bit0 -x_0x23_48_0x23_20_bit0 -x_0x23_48_0x23_18_bit0 -x_0x23_48_0x23_16_bit0 -x_0x23_48_0x23_13_bit0 -x_0x23_48_0x23_11_bit0 -x_0x23_48_0x23_9_bit0 -x_0x23_48_0x23_8_bit0 -x_0x23_48_0x23_6_bit0 -x_0x23_48_0x23_3_bit0 -x_0x23_48_0x23_1_bit0 -x_0x23_47_0x23_34_bit0 -x_0x23_47_0x23_32_bit0 -x_0x23_47_0x23_30_bit0 -x_0x23_47_0x23_29_bit0 -x_0x23_47_0x23_27_bit0 -x_0x23_47_0x23_26_bit0 -x_0x23_47_0x23_23_bit0 -x_0x23_47_0x23_20_bit0 -x_0x23_47_0x23_18_bit0 -x_0x23_47_0x23_16_bit0 -x_0x23_47_0x23_13_bit0 -x_0x23_47_0x23_11_bit0 -x_0x23_47_0x23_9_bit0 -x_0x23_47_0x23_8_bit0 -x_0x23_47_0x23_6_bit0 -x_0x23_47_0x23_3_bit0 -x_0x23_47_0x23_1_bit0 -x_0x23_46_0x23_34_bit0 -x_0x23_46_0x23_32_bit0 -x_0x23_46_0x23_30_bit0 -x_0x23_46_0x23_29_bit0 -x_0x23_46_0x23_27_bit0 -x_0x23_46_0x23_26_bit0 -x_0x23_46_0x23_23_bit0 -x_0x23_46_0x23_20_bit0 -x_0x23_46_0x23_18_bit0 -x_0x23_46_0x23_16_bit0 -x_0x23_46_0x23_13_bit0 -x_0x23_46_0x23_11_bit0 -x_0x23_46_0x23_9_bit0 -x_0x23_46_0x23_8_bit0 -x_0x23_46_0x23_6_bit0 -x_0x23_46_0x23_3_bit0 -x_0x23_46_0x23_1_bit0 -x_0x23_45_0x23_34_bit0 -x_0x23_45_0x23_32_bit0 -x_0x23_45_0x23_30_bit0 -x_0x23_45_0x23_29_bit0 -x_0x23_45_0x23_27_bit0 -x_0x23_45_0x23_26_bit0 -x_0x23_45_0x23_23_bit0 -x_0x23_45_0x23_20_bit0 -x_0x23_45_0x23_18_bit0 -x_0x23_45_0x23_16_bit0 -x_0x23_45_0x23_13_bit0 -x_0x23_45_0x23_11_bit0 -x_0x23_45_0x23_9_bit0 -x_0x23_45_0x23_8_bit0 -x_0x23_45_0x23_6_bit0 -x_0x23_45_0x23_3_bit0 -x_0x23_45_0x23_1_bit0 -x_0x23_44_0x23_34_bit0 -x_0x23_44_0x23_32_bit0 -x_0x23_44_0x23_30_bit0 -x_0x23_44_0x23_29_bit0 -x_0x23_44_0x23_27_bit0 -x_0x23_44_0x23_26_bit0 -x_0x23_44_0x23_23_bit0 -x_0x23_44_0x23_20_bit0 -x_0x23_44_0x23_18_bit0 -x_0x23_44_0x23_16_bit0 -x_0x23_44_0x23_13_bit0 -x_0x23_44_0x23_11_bit0 -x_0x23_44_0x23_9_bit0 -x_0x23_44_0x23_8_bit0 -x_0x23_44_0x23_6_bit0 -x_0x23_44_0x23_3_bit0 -x_0x23_44_0x23_1_bit0 -x_0x23_43_0x23_34_bit0 -x_0x23_43_0x23_32_bit0 -x_0x23_43_0x23_30_bit0 -x_0x23_43_0x23_29_bit0 -x_0x23_43_0x23_27_bit0 -x_0x23_43_0x23_26_bit0 -x_0x23_43_0x23_23_bit0 -x_0x23_43_0x23_20_bit0 -x_0x23_43_0x23_18_bit0 -x_0x23_43_0x23_16_bit0 -x_0x23_43_0x23_13_bit0 -x_0x23_43_0x23_11_bit0 -x_0x23_43_0x23_9_bit0 -x_0x23_43_0x23_8_bit0 -x_0x23_43_0x23_6_bit0 -x_0x23_43_0x23_3_bit0 -x_0x23_43_0x23_1_bit0 -x_0x23_42_0x23_34_bit0 -x_0x23_42_0x23_32_bit0 -x_0x23_42_0x23_30_bit0 -x_0x23_42_0x23_29_bit0 -x_0x23_42_0x23_27_bit0 -x_0x23_42_0x23_26_bit0 -x_0x23_42_0x23_23_bit0 -x_0x23_42_0x23_20_bit0 -x_0x23_42_0x23_18_bit0 -x_0x23_42_0x23_16_bit0 -x_0x23_42_0x23_13_bit0 -x_0x23_42_0x23_11_bit0 -x_0x23_42_0x23_9_bit0 -x_0x23_42_0x23_8_bit0 -x_0x23_42_0x23_6_bit0 -x_0x23_42_0x23_3_bit0 -x_0x23_42_0x23_1_bit0 -x_0x23_41_0x23_34_bit0 -x_0x23_41_0x23_32_bit0 -x_0x23_41_0x23_30_bit0 -x_0x23_41_0x23_29_bit0 -x_0x23_41_0x23_27_bit0 -x_0x23_41_0x23_26_bit0 -x_0x23_41_0x23_23_bit0 -x_0x23_41_0x23_20_bit0 -x_0x23_41_0x23_18_bit0 -x_0x23_41_0x23_16_bit0 -x_0x23_41_0x23_13_bit0 -x_0x23_41_0x23_11_bit0 -x_0x23_41_0x23_9_bit0 -x_0x23_41_0x23_8_bit0 -x_0x23_41_0x23_6_bit0 -x_0x23_41_0x23_3_bit0 -x_0x23_41_0x23_1_bit0 -x_0x23_40_0x23_34_bit0 -x_0x23_40_0x23_32_bit0 -x_0x23_40_0x23_30_bit0 -x_0x23_40_0x23_29_bit0 -x_0x23_40_0x23_27_bit0 -x_0x23_40_0x23_26_bit0 -x_0x23_40_0x23_23_bit0 x_0x23_40_0x23_20_bit0 -x_0x23_40_0x23_18_bit0 -x_0x23_40_0x23_16_bit0 -x_0x23_40_0x23_13_bit0 -x_0x23_40_0x23_11_bit0 -x_0x23_40_0x23_9_bit0 -x_0x23_40_0x23_8_bit0 -x_0x23_40_0x23_6_bit0 -x_0x23_40_0x23_3_bit0 -x_0x23_40_0x23_1_bit0 -x_0x23_39_0x23_34_bit0 -x_0x23_39_0x23_32_bit0 -x_0x23_39_0x23_30_bit0 -x_0x23_39_0x23_29_bit0 -x_0x23_39_0x23_27_bit0 -x_0x23_39_0x23_26_bit0 -x_0x23_39_0x23_23_bit0 -x_0x23_39_0x23_20_bit0 x_0x23_39_0x23_18_bit0 -x_0x23_39_0x23_16_bit0 -x_0x23_39_0x23_13_bit0 -x_0x23_39_0x23_11_bit0 -x_0x23_39_0x23_9_bit0 -x_0x23_39_0x23_8_bit0 -x_0x23_39_0x23_6_bit0 -x_0x23_39_0x23_3_bit0 -x_0x23_39_0x23_1_bit0 -x_0x23_38_0x23_34_bit0 -x_0x23_38_0x23_32_bit0 -x_0x23_38_0x23_30_bit0 -x_0x23_38_0x23_29_bit0 -x_0x23_38_0x23_27_bit0 -x_0x23_38_0x23_26_bit0 -x_0x23_38_0x23_23_bit0 -x_0x23_38_0x23_20_bit0 -x_0x23_38_0x23_18_bit0 x_0x23_38_0x23_16_bit0 -x_0x23_38_0x23_13_bit0 -x_0x23_38_0x23_11_bit0 -x_0x23_38_0x23_9_bit0 -x_0x23_38_0x23_8_bit0 -x_0x23_38_0x23_6_bit0 -x_0x23_38_0x23_3_bit0 -x_0x23_38_0x23_1_bit0 -x_0x23_37_0x23_34_bit0 -x_0x23_37_0x23_32_bit0 -x_0x23_37_0x23_30_bit0 -x_0x23_37_0x23_29_bit0 -x_0x23_37_0x23_27_bit0 -x_0x23_37_0x23_26_bit0 -x_0x23_37_0x23_23_bit0 -x_0x23_37_0x23_20_bit0 -x_0x23_37_0x23_18_bit0 -x_0x23_37_0x23_16_bit0 -x_0x23_37_0x23_13_bit0 -x_0x23_37_0x23_11_bit0 -x_0x23_37_0x23_9_bit0 -x_0x23_37_0x23_8_bit0 -x_0x23_37_0x23_6_bit0 -x_0x23_37_0x23_3_bit0 -x_0x23_37_0x23_1_bit0 -x_0x23_36_0x23_34_bit0 -x_0x23_36_0x23_32_bit0 -x_0x23_36_0x23_30_bit0 -x_0x23_36_0x23_29_bit0 -x_0x23_36_0x23_27_bit0 -x_0x23_36_0x23_26_bit0 -x_0x23_36_0x23_23_bit0 -x_0x23_36_0x23_20_bit0 -x_0x23_36_0x23_18_bit0 -x_0x23_36_0x23_16_bit0 -x_0x23_36_0x23_13_bit0 -x_0x23_36_0x23_11_bit0 -x_0x23_36_0x23_9_bit0 -x_0x23_36_0x23_8_bit0 -x_0x23_36_0x23_6_bit0 -x_0x23_36_0x23_3_bit0 -x_0x23_36_0x23_1_bit0 -x_0x23_35_0x23_34_bit0 -x_0x23_35_0x23_32_bit0 -x_0x23_35_0x23_30_bit0 -x_0x23_35_0x23_29_bit0 -x_0x23_35_0x23_27_bit0 x_0x23_35_0x23_26_bit0 -x_0x23_35_0x23_23_bit0 -x_0x23_35_0x23_20_bit0 -x_0x23_35_0x23_18_bit0 -x_0x23_35_0x23_16_bit0 -x_0x23_35_0x23_13_bit0 -x_0x23_35_0x23_11_bit0 -x_0x23_35_0x23_9_bit0 -x_0x23_35_0x23_8_bit0 -x_0x23_35_0x23_6_bit0 -x_0x23_35_0x23_3_bit0 -x_0x23_35_0x23_1_bit0 -x_0x23_34_0x23_34_bit0 -x_0x23_34_0x23_32_bit0 -x_0x23_34_0x23_30_bit0 -x_0x23_34_0x23_29_bit0 -x_0x23_34_0x23_27_bit0 -x_0x23_34_0x23_26_bit0 -x_0x23_34_0x23_23_bit0 -x_0x23_34_0x23_20_bit0 -x_0x23_34_0x23_18_bit0 -x_0x23_34_0x23_16_bit0 -x_0x23_34_0x23_13_bit0 -x_0x23_34_0x23_11_bit0 -x_0x23_34_0x23_9_bit0 -x_0x23_34_0x23_8_bit0 -x_0x23_34_0x23_6_bit0 -x_0x23_34_0x23_3_bit0 -x_0x23_34_0x23_1_bit0 -x_0x23_33_0x23_34_bit0 -x_0x23_33_0x23_32_bit0 -x_0x23_33_0x23_30_bit0 -x_0x23_33_0x23_29_bit0 -x_0x23_33_0x23_27_bit0 -x_0x23_33_0x23_26_bit0 x_0x23_33_0x23_23_bit0 -x_0x23_33_0x23_20_bit0 -x_0x23_33_0x23_18_bit0 -x_0x23_33_0x23_16_bit0 -x_0x23_33_0x23_13_bit0 -x_0x23_33_0x23_11_bit0 -x_0x23_33_0x23_9_bit0 -x_0x23_33_0x23_8_bit0 -x_0x23_33_0x23_6_bit0 -x_0x23_33_0x23_3_bit0 -x_0x23_33_0x23_1_bit0 -x_0x23_32_0x23_34_bit0 -x_0x23_32_0x23_32_bit0 -x_0x23_32_0x23_30_bit0 -x_0x23_32_0x23_29_bit0 -x_0x23_32_0x23_27_bit0 -x_0x23_32_0x23_26_bit0 -x_0x23_32_0x23_23_bit0 -x_0x23_32_0x23_20_bit0 -x_0x23_32_0x23_18_bit0 -x_0x23_32_0x23_16_bit0 x_0x23_32_0x23_13_bit0 -x_0x23_32_0x23_11_bit0 -x_0x23_32_0x23_9_bit0 -x_0x23_32_0x23_8_bit0 -x_0x23_32_0x23_6_bit0 -x_0x23_32_0x23_3_bit0 -x_0x23_32_0x23_1_bit0 -x_0x23_31_0x23_34_bit0 -x_0x23_31_0x23_32_bit0 -x_0x23_31_0x23_30_bit0 -x_0x23_31_0x23_29_bit0 -x_0x23_31_0x23_27_bit0 -x_0x23_31_0x23_26_bit0 -x_0x23_31_0x23_23_bit0 -x_0x23_31_0x23_20_bit0 -x_0x23_31_0x23_18_bit0 -x_0x23_31_0x23_16_bit0 -x_0x23_31_0x23_13_bit0 -x_0x23_31_0x23_11_bit0 -x_0x23_31_0x23_9_bit0 -x_0x23_31_0x23_8_bit0 -x_0x23_31_0x23_6_bit0 -x_0x23_31_0x23_3_bit0 -x_0x23_31_0x23_1_bit0 -x_0x23_30_0x23_34_bit0 -x_0x23_30_0x23_32_bit0 -x_0x23_30_0x23_30_bit0 -x_0x23_30_0x23_29_bit0 -x_0x23_30_0x23_27_bit0 -x_0x23_30_0x23_26_bit0 -x_0x23_30_0x23_23_bit0 -x_0x23_30_0x23_20_bit0 -x_0x23_30_0x23_18_bit0 -x_0x23_30_0x23_16_bit0 -x_0x23_30_0x23_13_bit0 -x_0x23_30_0x23_11_bit0 -x_0x23_30_0x23_9_bit0 -x_0x23_30_0x23_8_bit0 -x_0x23_30_0x23_6_bit0 -x_0x23_30_0x23_3_bit0 -x_0x23_30_0x23_1_bit0 -x_0x23_29_0x23_34_bit0 -x_0x23_29_0x23_32_bit0 -x_0x23_29_0x23_30_bit0 -x_0x23_29_0x23_29_bit0 -x_0x23_29_0x23_27_bit0 -x_0x23_29_0x23_26_bit0 -x_0x23_29_0x23_23_bit0 -x_0x23_29_0x23_20_bit0 -x_0x23_29_0x23_18_bit0 -x_0x23_29_0x23_16_bit0 -x_0x23_29_0x23_13_bit0 -x_0x23_29_0x23_11_bit0 -x_0x23_29_0x23_9_bit0 -x_0x23_29_0x23_8_bit0 -x_0x23_29_0x23_6_bit0 -x_0x23_29_0x23_3_bit0 -x_0x23_29_0x23_1_bit0 -x_0x23_28_0x23_34_bit0 -x_0x23_28_0x23_32_bit0 -x_0x23_28_0x23_30_bit0 -x_0x23_28_0x23_29_bit0 x_0x23_28_0x23_27_bit0 -x_0x23_28_0x23_26_bit0 -x_0x23_28_0x23_23_bit0 -x_0x23_28_0x23_20_bit0 -x_0x23_28_0x23_18_bit0 -x_0x23_28_0x23_16_bit0 -x_0x23_28_0x23_13_bit0 -x_0x23_28_0x23_11_bit0 -x_0x23_28_0x23_9_bit0 -x_0x23_28_0x23_8_bit0 -x_0x23_28_0x23_6_bit0 -x_0x23_28_0x23_3_bit0 -x_0x23_28_0x23_1_bit0 -x_0x23_27_0x23_34_bit0 -x_0x23_27_0x23_32_bit0 -x_0x23_27_0x23_30_bit0 -x_0x23_27_0x23_29_bit0 -x_0x23_27_0x23_27_bit0 -x_0x23_27_0x23_26_bit0 -x_0x23_27_0x23_23_bit0 -x_0x23_27_0x23_20_bit0 -x_0x23_27_0x23_18_bit0 -x_0x23_27_0x23_16_bit0 -x_0x23_27_0x23_13_bit0 -x_0x23_27_0x23_11_bit0 -x_0x23_27_0x23_9_bit0 -x_0x23_27_0x23_8_bit0 -x_0x23_27_0x23_6_bit0 -x_0x23_27_0x23_3_bit0 x_0x23_27_0x23_1_bit0 -x_0x23_26_0x23_34_bit0 -x_0x23_26_0x23_32_bit0 -x_0x23_26_0x23_30_bit0 -x_0x23_26_0x23_29_bit0 -x_0x23_26_0x23_27_bit0 -x_0x23_26_0x23_26_bit0 -x_0x23_26_0x23_23_bit0 -x_0x23_26_0x23_20_bit0 -x_0x23_26_0x23_18_bit0 -x_0x23_26_0x23_16_bit0 -x_0x23_26_0x23_13_bit0 -x_0x23_26_0x23_11_bit0 -x_0x23_26_0x23_9_bit0 -x_0x23_26_0x23_8_bit0 -x_0x23_26_0x23_6_bit0 -x_0x23_26_0x23_3_bit0 -x_0x23_26_0x23_1_bit0 -x_0x23_25_0x23_34_bit0 -x_0x23_25_0x23_32_bit0 -x_0x23_25_0x23_30_bit0 -x_0x23_25_0x23_29_bit0 -x_0x23_25_0x23_27_bit0 -x_0x23_25_0x23_26_bit0 -x_0x23_25_0x23_23_bit0 -x_0x23_25_0x23_20_bit0 -x_0x23_25_0x23_18_bit0 -x_0x23_25_0x23_16_bit0 -x_0x23_25_0x23_13_bit0 x_0x23_25_0x23_11_bit0 -x_0x23_25_0x23_9_bit0 -x_0x23_25_0x23_8_bit0 -x_0x23_25_0x23_6_bit0 -x_0x23_25_0x23_3_bit0 -x_0x23_25_0x23_1_bit0 -x_0x23_24_0x23_34_bit0 -x_0x23_24_0x23_32_bit0 -x_0x23_24_0x23_30_bit0 -x_0x23_24_0x23_29_bit0 -x_0x23_24_0x23_27_bit0 -x_0x23_24_0x23_26_bit0 -x_0x23_24_0x23_23_bit0 -x_0x23_24_0x23_20_bit0 -x_0x23_24_0x23_18_bit0 -x_0x23_24_0x23_16_bit0 -x_0x23_24_0x23_13_bit0 -x_0x23_24_0x23_11_bit0 -x_0x23_24_0x23_9_bit0 -x_0x23_24_0x23_8_bit0 -x_0x23_24_0x23_6_bit0 -x_0x23_24_0x23_3_bit0 -x_0x23_24_0x23_1_bit0 -x_0x23_23_0x23_34_bit0 -x_0x23_23_0x23_32_bit0 -x_0x23_23_0x23_30_bit0 -x_0x23_23_0x23_29_bit0 -x_0x23_23_0x23_27_bit0 -x_0x23_23_0x23_26_bit0 -x_0x23_23_0x23_23_bit0 -x_0x23_23_0x23_20_bit0 -x_0x23_23_0x23_18_bit0 -x_0x23_23_0x23_16_bit0 -x_0x23_23_0x23_13_bit0 -x_0x23_23_0x23_11_bit0 -x_0x23_23_0x23_9_bit0 -x_0x23_23_0x23_8_bit0 -x_0x23_23_0x23_6_bit0 -x_0x23_23_0x23_3_bit0 -x_0x23_23_0x23_1_bit0 -x_0x23_22_0x23_34_bit0 -x_0x23_22_0x23_32_bit0 -x_0x23_22_0x23_30_bit0 -x_0x23_22_0x23_29_bit0 -x_0x23_22_0x23_27_bit0 -x_0x23_22_0x23_26_bit0 -x_0x23_22_0x23_23_bit0 -x_0x23_22_0x23_20_bit0 -x_0x23_22_0x23_18_bit0 -x_0x23_22_0x23_16_bit0 -x_0x23_22_0x23_13_bit0 -x_0x23_22_0x23_11_bit0 -x_0x23_22_0x23_9_bit0 -x_0x23_22_0x23_8_bit0 -x_0x23_22_0x23_6_bit0 -x_0x23_22_0x23_3_bit0 -x_0x23_22_0x23_1_bit0 -x_0x23_21_0x23_34_bit0 -x_0x23_21_0x23_32_bit0 -x_0x23_21_0x23_30_bit0 -x_0x23_21_0x23_29_bit0 -x_0x23_21_0x23_27_bit0 -x_0x23_21_0x23_26_bit0 -x_0x23_21_0x23_23_bit0 -x_0x23_21_0x23_20_bit0 -x_0x23_21_0x23_18_bit0 -x_0x23_21_0x23_16_bit0 -x_0x23_21_0x23_13_bit0 -x_0x23_21_0x23_11_bit0 -x_0x23_21_0x23_9_bit0 -x_0x23_21_0x23_8_bit0 -x_0x23_21_0x23_6_bit0 -x_0x23_21_0x23_3_bit0 -x_0x23_21_0x23_1_bit0 -x_0x23_20_0x23_34_bit0 -x_0x23_20_0x23_32_bit0 -x_0x23_20_0x23_30_bit0 -x_0x23_20_0x23_29_bit0 -x_0x23_20_0x23_27_bit0 -x_0x23_20_0x23_26_bit0 -x_0x23_20_0x23_23_bit0 -x_0x23_20_0x23_20_bit0 -x_0x23_20_0x23_18_bit0 -x_0x23_20_0x23_16_bit0 -x_0x23_20_0x23_13_bit0 -x_0x23_20_0x23_11_bit0 -x_0x23_20_0x23_9_bit0 -x_0x23_20_0x23_8_bit0 -x_0x23_20_0x23_6_bit0 -x_0x23_20_0x23_3_bit0 -x_0x23_20_0x23_1_bit0 -x_0x23_19_0x23_34_bit0 -x_0x23_19_0x23_32_bit0 -x_0x23_19_0x23_30_bit0 -x_0x23_19_0x23_29_bit0 -x_0x23_19_0x23_27_bit0 -x_0x23_19_0x23_26_bit0 -x_0x23_19_0x23_23_bit0 -x_0x23_19_0x23_20_bit0 -x_0x23_19_0x23_18_bit0 -x_0x23_19_0x23_16_bit0 -x_0x23_19_0x23_13_bit0 -x_0x23_19_0x23_11_bit0 -x_0x23_19_0x23_9_bit0 -x_0x23_19_0x23_8_bit0 -x_0x23_19_0x23_6_bit0 -x_0x23_19_0x23_3_bit0 -x_0x23_19_0x23_1_bit0 -x_0x23_18_0x23_34_bit0 -x_0x23_18_0x23_32_bit0 -x_0x23_18_0x23_30_bit0 -x_0x23_18_0x23_29_bit0 -x_0x23_18_0x23_27_bit0 -x_0x23_18_0x23_26_bit0 -x_0x23_18_0x23_23_bit0 -x_0x23_18_0x23_20_bit0 -x_0x23_18_0x23_18_bit0 -x_0x23_18_0x23_16_bit0 -x_0x23_18_0x23_13_bit0 -x_0x23_18_0x23_11_bit0 x_0x23_18_0x23_9_bit0 -x_0x23_18_0x23_8_bit0 -x_0x23_18_0x23_6_bit0 -x_0x23_18_0x23_3_bit0 -x_0x23_18_0x23_1_bit0 -x_0x23_17_0x23_34_bit0 -x_0x23_17_0x23_32_bit0 -x_0x23_17_0x23_30_bit0 -x_0x23_17_0x23_29_bit0 -x_0x23_17_0x23_27_bit0 -x_0x23_17_0x23_26_bit0 -x_0x23_17_0x23_23_bit0 -x_0x23_17_0x23_20_bit0 -x_0x23_17_0x23_18_bit0 -x_0x23_17_0x23_16_bit0 -x_0x23_17_0x23_13_bit0 -x_0x23_17_0x23_11_bit0 -x_0x23_17_0x23_9_bit0 x_0x23_17_0x23_8_bit0 -x_0x23_17_0x23_6_bit0 -x_0x23_17_0x23_3_bit0 -x_0x23_17_0x23_1_bit0 -x_0x23_16_0x23_34_bit0 -x_0x23_16_0x23_32_bit0 -x_0x23_16_0x23_30_bit0 -x_0x23_16_0x23_29_bit0 -x_0x23_16_0x23_27_bit0 -x_0x23_16_0x23_26_bit0 -x_0x23_16_0x23_23_bit0 -x_0x23_16_0x23_20_bit0 -x_0x23_16_0x23_18_bit0 -x_0x23_16_0x23_16_bit0 -x_0x23_16_0x23_13_bit0 -x_0x23_16_0x23_11_bit0 -x_0x23_16_0x23_9_bit0 -x_0x23_16_0x23_8_bit0 -x_0x23_16_0x23_6_bit0 -x_0x23_16_0x23_3_bit0 -x_0x23_16_0x23_1_bit0 -x_0x23_15_0x23_34_bit0 -x_0x23_15_0x23_32_bit0 -x_0x23_15_0x23_30_bit0 -x_0x23_15_0x23_29_bit0 -x_0x23_15_0x23_27_bit0 -x_0x23_15_0x23_26_bit0 -x_0x23_15_0x23_23_bit0 -x_0x23_15_0x23_20_bit0 -x_0x23_15_0x23_18_bit0 -x_0x23_15_0x23_16_bit0 -x_0x23_15_0x23_13_bit0 -x_0x23_15_0x23_11_bit0 -x_0x23_15_0x23_9_bit0 -x_0x23_15_0x23_8_bit0 -x_0x23_15_0x23_6_bit0 -x_0x23_15_0x23_3_bit0 -x_0x23_15_0x23_1_bit0 -x_0x23_14_0x23_34_bit0 -x_0x23_14_0x23_32_bit0 -x_0x23_14_0x23_30_bit0 x_0x23_14_0x23_29_bit0 -x_0x23_14_0x23_27_bit0 -x_0x23_14_0x23_26_bit0 -x_0x23_14_0x23_23_bit0 -x_0x23_14_0x23_20_bit0 -x_0x23_14_0x23_18_bit0 -x_0x23_14_0x23_16_bit0 -x_0x23_14_0x23_13_bit0 -x_0x23_14_0x23_11_bit0 -x_0x23_14_0x23_9_bit0 -x_0x23_14_0x23_8_bit0 -x_0x23_14_0x23_6_bit0 -x_0x23_14_0x23_3_bit0 -x_0x23_14_0x23_1_bit0 -x_0x23_13_0x23_34_bit0 -x_0x23_13_0x23_32_bit0 -x_0x23_13_0x23_30_bit0 -x_0x23_13_0x23_29_bit0 -x_0x23_13_0x23_27_bit0 -x_0x23_13_0x23_26_bit0 -x_0x23_13_0x23_23_bit0 -x_0x23_13_0x23_20_bit0 -x_0x23_13_0x23_18_bit0 -x_0x23_13_0x23_16_bit0 -x_0x23_13_0x23_13_bit0 -x_0x23_13_0x23_11_bit0 -x_0x23_13_0x23_9_bit0 -x_0x23_13_0x23_8_bit0 -x_0x23_13_0x23_6_bit0 x_0x23_13_0x23_3_bit0 -x_0x23_13_0x23_1_bit0 -x_0x23_12_0x23_34_bit0 -x_0x23_12_0x23_32_bit0 -x_0x23_12_0x23_30_bit0 -x_0x23_12_0x23_29_bit0 -x_0x23_12_0x23_27_bit0 -x_0x23_12_0x23_26_bit0 -x_0x23_12_0x23_23_bit0 -x_0x23_12_0x23_20_bit0 -x_0x23_12_0x23_18_bit0 -x_0x23_12_0x23_16_bit0 -x_0x23_12_0x23_13_bit0 -x_0x23_12_0x23_11_bit0 -x_0x23_12_0x23_9_bit0 -x_0x23_12_0x23_8_bit0 -x_0x23_12_0x23_6_bit0 -x_0x23_12_0x23_3_bit0 -x_0x23_12_0x23_1_bit0 -x_0x23_11_0x23_34_bit0 -x_0x23_11_0x23_32_bit0 -x_0x23_11_0x23_30_bit0 -x_0x23_11_0x23_29_bit0 -x_0x23_11_0x23_27_bit0 -x_0x23_11_0x23_26_bit0 -x_0x23_11_0x23_23_bit0 -x_0x23_11_0x23_20_bit0 -x_0x23_11_0x23_18_bit0 -x_0x23_11_0x23_16_bit0 -x_0x23_11_0x23_13_bit0 -x_0x23_11_0x23_11_bit0 -x_0x23_11_0x23_9_bit0 -x_0x23_11_0x23_8_bit0 -x_0x23_11_0x23_6_bit0 -x_0x23_11_0x23_3_bit0 -x_0x23_11_0x23_1_bit0 -x_0x23_10_0x23_34_bit0 -x_0x23_10_0x23_32_bit0 -x_0x23_10_0x23_30_bit0 -x_0x23_10_0x23_29_bit0 -x_0x23_10_0x23_27_bit0 -x_0x23_10_0x23_26_bit0 -x_0x23_10_0x23_23_bit0 -x_0x23_10_0x23_20_bit0 -x_0x23_10_0x23_18_bit0 -x_0x23_10_0x23_16_bit0 -x_0x23_10_0x23_13_bit0 -x_0x23_10_0x23_11_bit0 -x_0x23_10_0x23_9_bit0 -x_0x23_10_0x23_8_bit0 x_0x23_10_0x23_6_bit0 -x_0x23_10_0x23_3_bit0 -x_0x23_10_0x23_1_bit0 -x_0x23_9_0x23_34_bit0 -x_0x23_9_0x23_32_bit0 -x_0x23_9_0x23_30_bit0 -x_0x23_9_0x23_29_bit0 -x_0x23_9_0x23_27_bit0 -x_0x23_9_0x23_26_bit0 -x_0x23_9_0x23_23_bit0 -x_0x23_9_0x23_20_bit0 -x_0x23_9_0x23_18_bit0 -x_0x23_9_0x23_16_bit0 -x_0x23_9_0x23_13_bit0 -x_0x23_9_0x23_11_bit0 -x_0x23_9_0x23_9_bit0 -x_0x23_9_0x23_8_bit0 -x_0x23_9_0x23_6_bit0 -x_0x23_9_0x23_3_bit0 -x_0x23_9_0x23_1_bit0 -x_0x23_8_0x23_34_bit0 -x_0x23_8_0x23_32_bit0 -x_0x23_8_0x23_30_bit0 -x_0x23_8_0x23_29_bit0 -x_0x23_8_0x23_27_bit0 -x_0x23_8_0x23_26_bit0 -x_0x23_8_0x23_23_bit0 -x_0x23_8_0x23_20_bit0 -x_0x23_8_0x23_18_bit0 -x_0x23_8_0x23_16_bit0 -x_0x23_8_0x23_13_bit0 -x_0x23_8_0x23_11_bit0 -x_0x23_8_0x23_9_bit0 -x_0x23_8_0x23_8_bit0 -x_0x23_8_0x23_6_bit0 -x_0x23_8_0x23_3_bit0 -x_0x23_8_0x23_1_bit0 -x_0x23_7_0x23_34_bit0 -x_0x23_7_0x23_32_bit0 x_0x23_7_0x23_30_bit0 -x_0x23_7_0x23_29_bit0 -x_0x23_7_0x23_27_bit0 -x_0x23_7_0x23_26_bit0 -x_0x23_7_0x23_23_bit0 -x_0x23_7_0x23_20_bit0 -x_0x23_7_0x23_18_bit0 -x_0x23_7_0x23_16_bit0 -x_0x23_7_0x23_13_bit0 -x_0x23_7_0x23_11_bit0 -x_0x23_7_0x23_9_bit0 -x_0x23_7_0x23_8_bit0 -x_0x23_7_0x23_6_bit0 -x_0x23_7_0x23_3_bit0 -x_0x23_7_0x23_1_bit0 -x_0x23_6_0x23_34_bit0 -x_0x23_6_0x23_32_bit0 -x_0x23_6_0x23_30_bit0 -x_0x23_6_0x23_29_bit0 -x_0x23_6_0x23_27_bit0 -x_0x23_6_0x23_26_bit0 -x_0x23_6_0x23_23_bit0 -x_0x23_6_0x23_20_bit0 -x_0x23_6_0x23_18_bit0 -x_0x23_6_0x23_16_bit0 -x_0x23_6_0x23_13_bit0 -x_0x23_6_0x23_11_bit0 -x_0x23_6_0x23_9_bit0 -x_0x23_6_0x23_8_bit0 -x_0x23_6_0x23_6_bit0 -x_0x23_6_0x23_3_bit0 -x_0x23_6_0x23_1_bit0 -x_0x23_5_0x23_34_bit0 x_0x23_5_0x23_32_bit0 -x_0x23_5_0x23_30_bit0 -x_0x23_5_0x23_29_bit0 -x_0x23_5_0x23_27_bit0 -x_0x23_5_0x23_26_bit0 -x_0x23_5_0x23_23_bit0 -x_0x23_5_0x23_20_bit0 -x_0x23_5_0x23_18_bit0 -x_0x23_5_0x23_16_bit0 -x_0x23_5_0x23_13_bit0 -x_0x23_5_0x23_11_bit0 -x_0x23_5_0x23_9_bit0 -x_0x23_5_0x23_8_bit0 -x_0x23_5_0x23_6_bit0 -x_0x23_5_0x23_3_bit0 -x_0x23_5_0x23_1_bit0 -x_0x23_4_0x23_34_bit0 -x_0x23_4_0x23_32_bit0 -x_0x23_4_0x23_30_bit0 -x_0x23_4_0x23_29_bit0 -x_0x23_4_0x23_27_bit0 -x_0x23_4_0x23_26_bit0 -x_0x23_4_0x23_23_bit0 -x_0x23_4_0x23_20_bit0 -x_0x23_4_0x23_18_bit0 -x_0x23_4_0x23_16_bit0 -x_0x23_4_0x23_13_bit0 -x_0x23_4_0x23_11_bit0 -x_0x23_4_0x23_9_bit0 -x_0x23_4_0x23_8_bit0 -x_0x23_4_0x23_6_bit0 -x_0x23_4_0x23_3_bit0 -x_0x23_4_0x23_1_bit0 x_0x23_3_0x23_34_bit0 -x_0x23_3_0x23_32_bit0 -x_0x23_3_0x23_30_bit0 -x_0x23_3_0x23_29_bit0 -x_0x23_3_0x23_27_bit0 -x_0x23_3_0x23_26_bit0 -x_0x23_3_0x23_23_bit0 -x_0x23_3_0x23_20_bit0 -x_0x23_3_0x23_18_bit0 -x_0x23_3_0x23_16_bit0 -x_0x23_3_0x23_13_bit0 -x_0x23_3_0x23_11_bit0 -x_0x23_3_0x23_9_bit0 -x_0x23_3_0x23_8_bit0 -x_0x23_3_0x23_6_bit0 -x_0x23_3_0x23_3_bit0 -x_0x23_3_0x23_1_bit0 -x_0x23_2_0x23_34_bit0 -x_0x23_2_0x23_32_bit0 -x_0x23_2_0x23_30_bit0 -x_0x23_2_0x23_29_bit0 -x_0x23_2_0x23_27_bit0 -x_0x23_2_0x23_26_bit0 -x_0x23_2_0x23_23_bit0 -x_0x23_2_0x23_20_bit0 -x_0x23_2_0x23_18_bit0 -x_0x23_2_0x23_16_bit0 -x_0x23_2_0x23_13_bit0 -x_0x23_2_0x23_11_bit0 -x_0x23_2_0x23_9_bit0 -x_0x23_2_0x23_8_bit0 -x_0x23_2_0x23_6_bit0 -x_0x23_2_0x23_3_bit0 -x_0x23_2_0x23_1_bit0 -x_0x23_1_0x23_34_bit0 -x_0x23_1_0x23_32_bit0 -x_0x23_1_0x23_30_bit0 -x_0x23_1_0x23_29_bit0 -x_0x23_1_0x23_27_bit0 -x_0x23_1_0x23_26_bit0 -x_0x23_1_0x23_23_bit0 -x_0x23_1_0x23_20_bit0 -x_0x23_1_0x23_18_bit0 -x_0x23_1_0x23_16_bit0 -x_0x23_1_0x23_13_bit0 -x_0x23_1_0x23_11_bit0 -x_0x23_1_0x23_9_bit0 -x_0x23_1_0x23_8_bit0 -x_0x23_1_0x23_6_bit0 -x_0x23_1_0x23_3_bit0 -x_0x23_1_0x23_1_bit0 -x_0x23_49_0x23_35_bit0 -x_0x23_49_0x23_33_bit0 -x_0x23_49_0x23_31_bit0 -x_0x23_49_0x23_28_bit0 -x_0x23_49_0x23_25_bit0 -x_0x23_49_0x23_24_bit0 -x_0x23_49_0x23_22_bit0 -x_0x23_49_0x23_21_bit0 -x_0x23_49_0x23_19_bit0 -x_0x23_49_0x23_17_bit0 -x_0x23_49_0x23_15_bit0 -x_0x23_49_0x23_14_bit0 -x_0x23_49_0x23_12_bit0 -x_0x23_49_0x23_10_bit0 -x_0x23_49_0x23_7_bit0 -x_0x23_49_0x23_5_bit0 -x_0x23_49_0x23_4_bit0 -x_0x23_49_0x23_2_bit0 -x_0x23_48_0x23_35_bit0 -x_0x23_48_0x23_33_bit0 -x_0x23_48_0x23_31_bit0 -x_0x23_48_0x23_28_bit0 -x_0x23_48_0x23_25_bit0 -x_0x23_48_0x23_24_bit0 -x_0x23_48_0x23_22_bit0 x_0x23_48_0x23_21_bit0 -x_0x23_48_0x23_19_bit0 -x_0x23_48_0x23_17_bit0 -x_0x23_48_0x23_15_bit0 -x_0x23_48_0x23_14_bit0 -x_0x23_48_0x23_12_bit0 -x_0x23_48_0x23_10_bit0 -x_0x23_48_0x23_7_bit0 -x_0x23_48_0x23_5_bit0 -x_0x23_48_0x23_4_bit0 -x_0x23_48_0x23_2_bit0 -x_0x23_47_0x23_35_bit0 -x_0x23_47_0x23_33_bit0 -x_0x23_47_0x23_31_bit0 -x_0x23_47_0x23_28_bit0 -x_0x23_47_0x23_25_bit0 -x_0x23_47_0x23_24_bit0 -x_0x23_47_0x23_22_bit0 -x_0x23_47_0x23_21_bit0 x_0x23_47_0x23_19_bit0 -x_0x23_47_0x23_17_bit0 -x_0x23_47_0x23_15_bit0 -x_0x23_47_0x23_14_bit0 -x_0x23_47_0x23_12_bit0 -x_0x23_47_0x23_10_bit0 -x_0x23_47_0x23_7_bit0 -x_0x23_47_0x23_5_bit0 -x_0x23_47_0x23_4_bit0 -x_0x23_47_0x23_2_bit0 -x_0x23_46_0x23_35_bit0 -x_0x23_46_0x23_33_bit0 -x_0x23_46_0x23_31_bit0 -x_0x23_46_0x23_28_bit0 -x_0x23_46_0x23_25_bit0 -x_0x23_46_0x23_24_bit0 -x_0x23_46_0x23_22_bit0 -x_0x23_46_0x23_21_bit0 -x_0x23_46_0x23_19_bit0 x_0x23_46_0x23_17_bit0 -x_0x23_46_0x23_15_bit0 -x_0x23_46_0x23_14_bit0 -x_0x23_46_0x23_12_bit0 -x_0x23_46_0x23_10_bit0 -x_0x23_46_0x23_7_bit0 -x_0x23_46_0x23_5_bit0 -x_0x23_46_0x23_4_bit0 -x_0x23_46_0x23_2_bit0 -x_0x23_45_0x23_35_bit0 -x_0x23_45_0x23_33_bit0 -x_0x23_45_0x23_31_bit0 -x_0x23_45_0x23_28_bit0 -x_0x23_45_0x23_25_bit0 -x_0x23_45_0x23_24_bit0 -x_0x23_45_0x23_22_bit0 -x_0x23_45_0x23_21_bit0 -x_0x23_45_0x23_19_bit0 -x_0x23_45_0x23_17_bit0 -x_0x23_45_0x23_15_bit0 -x_0x23_45_0x23_14_bit0 -x_0x23_45_0x23_12_bit0 -x_0x23_45_0x23_10_bit0 -x_0x23_45_0x23_7_bit0 -x_0x23_45_0x23_5_bit0 -x_0x23_45_0x23_4_bit0 -x_0x23_45_0x23_2_bit0 -x_0x23_44_0x23_35_bit0 -x_0x23_44_0x23_33_bit0 -x_0x23_44_0x23_31_bit0 -x_0x23_44_0x23_28_bit0 -x_0x23_44_0x23_25_bit0 -x_0x23_44_0x23_24_bit0 -x_0x23_44_0x23_22_bit0 -x_0x23_44_0x23_21_bit0 -x_0x23_44_0x23_19_bit0 -x_0x23_44_0x23_17_bit0 -x_0x23_44_0x23_15_bit0 -x_0x23_44_0x23_14_bit0 -x_0x23_44_0x23_12_bit0 -x_0x23_44_0x23_10_bit0 -x_0x23_44_0x23_7_bit0 -x_0x23_44_0x23_5_bit0 -x_0x23_44_0x23_4_bit0 -x_0x23_44_0x23_2_bit0 -x_0x23_43_0x23_35_bit0 -x_0x23_43_0x23_33_bit0 -x_0x23_43_0x23_31_bit0 -x_0x23_43_0x23_28_bit0 -x_0x23_43_0x23_25_bit0 -x_0x23_43_0x23_24_bit0 -x_0x23_43_0x23_22_bit0 -x_0x23_43_0x23_21_bit0 -x_0x23_43_0x23_19_bit0 -x_0x23_43_0x23_17_bit0 -x_0x23_43_0x23_15_bit0 -x_0x23_43_0x23_14_bit0 -x_0x23_43_0x23_12_bit0 -x_0x23_43_0x23_10_bit0 -x_0x23_43_0x23_7_bit0 -x_0x23_43_0x23_5_bit0 -x_0x23_43_0x23_4_bit0 -x_0x23_43_0x23_2_bit0 -x_0x23_42_0x23_35_bit0 -x_0x23_42_0x23_33_bit0 -x_0x23_42_0x23_31_bit0 -x_0x23_42_0x23_28_bit0 x_0x23_42_0x23_25_bit0 -x_0x23_42_0x23_24_bit0 -x_0x23_42_0x23_22_bit0 -x_0x23_42_0x23_21_bit0 -x_0x23_42_0x23_19_bit0 -x_0x23_42_0x23_17_bit0 -x_0x23_42_0x23_15_bit0 -x_0x23_42_0x23_14_bit0 -x_0x23_42_0x23_12_bit0 -x_0x23_42_0x23_10_bit0 -x_0x23_42_0x23_7_bit0 -x_0x23_42_0x23_5_bit0 -x_0x23_42_0x23_4_bit0 -x_0x23_42_0x23_2_bit0 -x_0x23_41_0x23_35_bit0 -x_0x23_41_0x23_33_bit0 -x_0x23_41_0x23_31_bit0 -x_0x23_41_0x23_28_bit0 -x_0x23_41_0x23_25_bit0 -x_0x23_41_0x23_24_bit0 x_0x23_41_0x23_22_bit0 -x_0x23_41_0x23_21_bit0 -x_0x23_41_0x23_19_bit0 -x_0x23_41_0x23_17_bit0 -x_0x23_41_0x23_15_bit0 -x_0x23_41_0x23_14_bit0 -x_0x23_41_0x23_12_bit0 -x_0x23_41_0x23_10_bit0 -x_0x23_41_0x23_7_bit0 -x_0x23_41_0x23_5_bit0 -x_0x23_41_0x23_4_bit0 -x_0x23_41_0x23_2_bit0 -x_0x23_40_0x23_35_bit0 -x_0x23_40_0x23_33_bit0 -x_0x23_40_0x23_31_bit0 -x_0x23_40_0x23_28_bit0 -x_0x23_40_0x23_25_bit0 -x_0x23_40_0x23_24_bit0 -x_0x23_40_0x23_22_bit0 -x_0x23_40_0x23_21_bit0 -x_0x23_40_0x23_19_bit0 -x_0x23_40_0x23_17_bit0 -x_0x23_40_0x23_15_bit0 -x_0x23_40_0x23_14_bit0 -x_0x23_40_0x23_12_bit0 -x_0x23_40_0x23_10_bit0 -x_0x23_40_0x23_7_bit0 -x_0x23_40_0x23_5_bit0 -x_0x23_40_0x23_4_bit0 -x_0x23_40_0x23_2_bit0 -x_0x23_39_0x23_35_bit0 -x_0x23_39_0x23_33_bit0 -x_0x23_39_0x23_31_bit0 -x_0x23_39_0x23_28_bit0 -x_0x23_39_0x23_25_bit0 -x_0x23_39_0x23_24_bit0 -x_0x23_39_0x23_22_bit0 -x_0x23_39_0x23_21_bit0 -x_0x23_39_0x23_19_bit0 -x_0x23_39_0x23_17_bit0 -x_0x23_39_0x23_15_bit0 -x_0x23_39_0x23_14_bit0 -x_0x23_39_0x23_12_bit0 -x_0x23_39_0x23_10_bit0 -x_0x23_39_0x23_7_bit0 -x_0x23_39_0x23_5_bit0 -x_0x23_39_0x23_4_bit0 -x_0x23_39_0x23_2_bit0 -x_0x23_38_0x23_35_bit0 -x_0x23_38_0x23_33_bit0 -x_0x23_38_0x23_31_bit0 -x_0x23_38_0x23_28_bit0 -x_0x23_38_0x23_25_bit0 -x_0x23_38_0x23_24_bit0 -x_0x23_38_0x23_22_bit0 -x_0x23_38_0x23_21_bit0 -x_0x23_38_0x23_19_bit0 -x_0x23_38_0x23_17_bit0 -x_0x23_38_0x23_15_bit0 -x_0x23_38_0x23_14_bit0 -x_0x23_38_0x23_12_bit0 -x_0x23_38_0x23_10_bit0 -x_0x23_38_0x23_7_bit0 -x_0x23_38_0x23_5_bit0 -x_0x23_38_0x23_4_bit0 -x_0x23_38_0x23_2_bit0 -x_0x23_37_0x23_35_bit0 -x_0x23_37_0x23_33_bit0 -x_0x23_37_0x23_31_bit0 -x_0x23_37_0x23_28_bit0 -x_0x23_37_0x23_25_bit0 -x_0x23_37_0x23_24_bit0 -x_0x23_37_0x23_22_bit0 -x_0x23_37_0x23_21_bit0 -x_0x23_37_0x23_19_bit0 -x_0x23_37_0x23_17_bit0 -x_0x23_37_0x23_15_bit0 -x_0x23_37_0x23_14_bit0 -x_0x23_37_0x23_12_bit0 -x_0x23_37_0x23_10_bit0 -x_0x23_37_0x23_7_bit0 -x_0x23_37_0x23_5_bit0 -x_0x23_37_0x23_4_bit0 -x_0x23_37_0x23_2_bit0 -x_0x23_36_0x23_35_bit0 -x_0x23_36_0x23_33_bit0 -x_0x23_36_0x23_31_bit0 -x_0x23_36_0x23_28_bit0 -x_0x23_36_0x23_25_bit0 -x_0x23_36_0x23_24_bit0 -x_0x23_36_0x23_22_bit0 -x_0x23_36_0x23_21_bit0 -x_0x23_36_0x23_19_bit0 -x_0x23_36_0x23_17_bit0 -x_0x23_36_0x23_15_bit0 -x_0x23_36_0x23_14_bit0 -x_0x23_36_0x23_12_bit0 -x_0x23_36_0x23_10_bit0 -x_0x23_36_0x23_7_bit0 -x_0x23_36_0x23_5_bit0 -x_0x23_36_0x23_4_bit0 -x_0x23_36_0x23_2_bit0 -x_0x23_35_0x23_35_bit0 -x_0x23_35_0x23_33_bit0 -x_0x23_35_0x23_31_bit0 -x_0x23_35_0x23_28_bit0 -x_0x23_35_0x23_25_bit0 -x_0x23_35_0x23_24_bit0 -x_0x23_35_0x23_22_bit0 -x_0x23_35_0x23_21_bit0 -x_0x23_35_0x23_19_bit0 -x_0x23_35_0x23_17_bit0 -x_0x23_35_0x23_15_bit0 -x_0x23_35_0x23_14_bit0 -x_0x23_35_0x23_12_bit0 -x_0x23_35_0x23_10_bit0 -x_0x23_35_0x23_7_bit0 -x_0x23_35_0x23_5_bit0 -x_0x23_35_0x23_4_bit0 -x_0x23_35_0x23_2_bit0 -x_0x23_34_0x23_35_bit0 -x_0x23_34_0x23_33_bit0 -x_0x23_34_0x23_31_bit0 -x_0x23_34_0x23_28_bit0 -x_0x23_34_0x23_25_bit0 x_0x23_34_0x23_24_bit0 -x_0x23_34_0x23_22_bit0 -x_0x23_34_0x23_21_bit0 -x_0x23_34_0x23_19_bit0 -x_0x23_34_0x23_17_bit0 -x_0x23_34_0x23_15_bit0 -x_0x23_34_0x23_14_bit0 -x_0x23_34_0x23_12_bit0 -x_0x23_34_0x23_10_bit0 -x_0x23_34_0x23_7_bit0 -x_0x23_34_0x23_5_bit0 -x_0x23_34_0x23_4_bit0 -x_0x23_34_0x23_2_bit0 -x_0x23_33_0x23_35_bit0 -x_0x23_33_0x23_33_bit0 -x_0x23_33_0x23_31_bit0 -x_0x23_33_0x23_28_bit0 -x_0x23_33_0x23_25_bit0 -x_0x23_33_0x23_24_bit0 -x_0x23_33_0x23_22_bit0 -x_0x23_33_0x23_21_bit0 -x_0x23_33_0x23_19_bit0 -x_0x23_33_0x23_17_bit0 -x_0x23_33_0x23_15_bit0 -x_0x23_33_0x23_14_bit0 -x_0x23_33_0x23_12_bit0 -x_0x23_33_0x23_10_bit0 -x_0x23_33_0x23_7_bit0 -x_0x23_33_0x23_5_bit0 -x_0x23_33_0x23_4_bit0 -x_0x23_33_0x23_2_bit0 -x_0x23_32_0x23_35_bit0 -x_0x23_32_0x23_33_bit0 -x_0x23_32_0x23_31_bit0 -x_0x23_32_0x23_28_bit0 -x_0x23_32_0x23_25_bit0 -x_0x23_32_0x23_24_bit0 -x_0x23_32_0x23_22_bit0 -x_0x23_32_0x23_21_bit0 -x_0x23_32_0x23_19_bit0 -x_0x23_32_0x23_17_bit0 -x_0x23_32_0x23_15_bit0 -x_0x23_32_0x23_14_bit0 -x_0x23_32_0x23_12_bit0 -x_0x23_32_0x23_10_bit0 -x_0x23_32_0x23_7_bit0 -x_0x23_32_0x23_5_bit0 -x_0x23_32_0x23_4_bit0 -x_0x23_32_0x23_2_bit0 -x_0x23_31_0x23_35_bit0 -x_0x23_31_0x23_33_bit0 -x_0x23_31_0x23_31_bit0 -x_0x23_31_0x23_28_bit0 -x_0x23_31_0x23_25_bit0 -x_0x23_31_0x23_24_bit0 -x_0x23_31_0x23_22_bit0 -x_0x23_31_0x23_21_bit0 -x_0x23_31_0x23_19_bit0 -x_0x23_31_0x23_17_bit0 -x_0x23_31_0x23_15_bit0 x_0x23_31_0x23_14_bit0 -x_0x23_31_0x23_12_bit0 -x_0x23_31_0x23_10_bit0 -x_0x23_31_0x23_7_bit0 -x_0x23_31_0x23_5_bit0 -x_0x23_31_0x23_4_bit0 -x_0x23_31_0x23_2_bit0 -x_0x23_30_0x23_35_bit0 -x_0x23_30_0x23_33_bit0 -x_0x23_30_0x23_31_bit0 -x_0x23_30_0x23_28_bit0 -x_0x23_30_0x23_25_bit0 -x_0x23_30_0x23_24_bit0 -x_0x23_30_0x23_22_bit0 -x_0x23_30_0x23_21_bit0 -x_0x23_30_0x23_19_bit0 -x_0x23_30_0x23_17_bit0 x_0x23_30_0x23_15_bit0 -x_0x23_30_0x23_14_bit0 -x_0x23_30_0x23_12_bit0 -x_0x23_30_0x23_10_bit0 -x_0x23_30_0x23_7_bit0 -x_0x23_30_0x23_5_bit0 -x_0x23_30_0x23_4_bit0 -x_0x23_30_0x23_2_bit0 -x_0x23_29_0x23_35_bit0 -x_0x23_29_0x23_33_bit0 -x_0x23_29_0x23_31_bit0 -x_0x23_29_0x23_28_bit0 -x_0x23_29_0x23_25_bit0 -x_0x23_29_0x23_24_bit0 -x_0x23_29_0x23_22_bit0 -x_0x23_29_0x23_21_bit0 -x_0x23_29_0x23_19_bit0 -x_0x23_29_0x23_17_bit0 -x_0x23_29_0x23_15_bit0 -x_0x23_29_0x23_14_bit0 -x_0x23_29_0x23_12_bit0 -x_0x23_29_0x23_10_bit0 -x_0x23_29_0x23_7_bit0 -x_0x23_29_0x23_5_bit0 -x_0x23_29_0x23_4_bit0 -x_0x23_29_0x23_2_bit0 -x_0x23_28_0x23_35_bit0 -x_0x23_28_0x23_33_bit0 -x_0x23_28_0x23_31_bit0 -x_0x23_28_0x23_28_bit0 -x_0x23_28_0x23_25_bit0 -x_0x23_28_0x23_24_bit0 -x_0x23_28_0x23_22_bit0 -x_0x23_28_0x23_21_bit0 -x_0x23_28_0x23_19_bit0 -x_0x23_28_0x23_17_bit0 -x_0x23_28_0x23_15_bit0 -x_0x23_28_0x23_14_bit0 -x_0x23_28_0x23_12_bit0 -x_0x23_28_0x23_10_bit0 -x_0x23_28_0x23_7_bit0 -x_0x23_28_0x23_5_bit0 -x_0x23_28_0x23_4_bit0 -x_0x23_28_0x23_2_bit0 -x_0x23_27_0x23_35_bit0 -x_0x23_27_0x23_33_bit0 -x_0x23_27_0x23_31_bit0 -x_0x23_27_0x23_28_bit0 -x_0x23_27_0x23_25_bit0 -x_0x23_27_0x23_24_bit0 -x_0x23_27_0x23_22_bit0 -x_0x23_27_0x23_21_bit0 -x_0x23_27_0x23_19_bit0 -x_0x23_27_0x23_17_bit0 -x_0x23_27_0x23_15_bit0 -x_0x23_27_0x23_14_bit0 -x_0x23_27_0x23_12_bit0 -x_0x23_27_0x23_10_bit0 -x_0x23_27_0x23_7_bit0 -x_0x23_27_0x23_5_bit0 -x_0x23_27_0x23_4_bit0 -x_0x23_27_0x23_2_bit0 -x_0x23_26_0x23_35_bit0 -x_0x23_26_0x23_33_bit0 -x_0x23_26_0x23_31_bit0 -x_0x23_26_0x23_28_bit0 -x_0x23_26_0x23_25_bit0 -x_0x23_26_0x23_24_bit0 -x_0x23_26_0x23_22_bit0 -x_0x23_26_0x23_21_bit0 -x_0x23_26_0x23_19_bit0 -x_0x23_26_0x23_17_bit0 -x_0x23_26_0x23_15_bit0 -x_0x23_26_0x23_14_bit0 -x_0x23_26_0x23_12_bit0 x_0x23_26_0x23_10_bit0 -x_0x23_26_0x23_7_bit0 -x_0x23_26_0x23_5_bit0 -x_0x23_26_0x23_4_bit0 -x_0x23_26_0x23_2_bit0 -x_0x23_25_0x23_35_bit0 -x_0x23_25_0x23_33_bit0 -x_0x23_25_0x23_31_bit0 -x_0x23_25_0x23_28_bit0 -x_0x23_25_0x23_25_bit0 -x_0x23_25_0x23_24_bit0 -x_0x23_25_0x23_22_bit0 -x_0x23_25_0x23_21_bit0 -x_0x23_25_0x23_19_bit0 -x_0x23_25_0x23_17_bit0 -x_0x23_25_0x23_15_bit0 -x_0x23_25_0x23_14_bit0 -x_0x23_25_0x23_12_bit0 -x_0x23_25_0x23_10_bit0 -x_0x23_25_0x23_7_bit0 -x_0x23_25_0x23_5_bit0 -x_0x23_25_0x23_4_bit0 -x_0x23_25_0x23_2_bit0 -x_0x23_24_0x23_35_bit0 -x_0x23_24_0x23_33_bit0 -x_0x23_24_0x23_31_bit0 -x_0x23_24_0x23_28_bit0 -x_0x23_24_0x23_25_bit0 -x_0x23_24_0x23_24_bit0 -x_0x23_24_0x23_22_bit0 -x_0x23_24_0x23_21_bit0 -x_0x23_24_0x23_19_bit0 -x_0x23_24_0x23_17_bit0 -x_0x23_24_0x23_15_bit0 -x_0x23_24_0x23_14_bit0 x_0x23_24_0x23_12_bit0 -x_0x23_24_0x23_10_bit0 -x_0x23_24_0x23_7_bit0 -x_0x23_24_0x23_5_bit0 -x_0x23_24_0x23_4_bit0 -x_0x23_24_0x23_2_bit0 -x_0x23_23_0x23_35_bit0 -x_0x23_23_0x23_33_bit0 -x_0x23_23_0x23_31_bit0 -x_0x23_23_0x23_28_bit0 -x_0x23_23_0x23_25_bit0 -x_0x23_23_0x23_24_bit0 -x_0x23_23_0x23_22_bit0 -x_0x23_23_0x23_21_bit0 -x_0x23_23_0x23_19_bit0 -x_0x23_23_0x23_17_bit0 -x_0x23_23_0x23_15_bit0 -x_0x23_23_0x23_14_bit0 -x_0x23_23_0x23_12_bit0 -x_0x23_23_0x23_10_bit0 -x_0x23_23_0x23_7_bit0 -x_0x23_23_0x23_5_bit0 -x_0x23_23_0x23_4_bit0 -x_0x23_23_0x23_2_bit0 -x_0x23_22_0x23_35_bit0 -x_0x23_22_0x23_33_bit0 -x_0x23_22_0x23_31_bit0 -x_0x23_22_0x23_28_bit0 -x_0x23_22_0x23_25_bit0 -x_0x23_22_0x23_24_bit0 -x_0x23_22_0x23_22_bit0 -x_0x23_22_0x23_21_bit0 -x_0x23_22_0x23_19_bit0 -x_0x23_22_0x23_17_bit0 -x_0x23_22_0x23_15_bit0 -x_0x23_22_0x23_14_bit0 -x_0x23_22_0x23_12_bit0 -x_0x23_22_0x23_10_bit0 -x_0x23_22_0x23_7_bit0 -x_0x23_22_0x23_5_bit0 -x_0x23_22_0x23_4_bit0 -x_0x23_22_0x23_2_bit0 -x_0x23_21_0x23_35_bit0 -x_0x23_21_0x23_33_bit0 -x_0x23_21_0x23_31_bit0 x_0x23_21_0x23_28_bit0 -x_0x23_21_0x23_25_bit0 -x_0x23_21_0x23_24_bit0 -x_0x23_21_0x23_22_bit0 -x_0x23_21_0x23_21_bit0 -x_0x23_21_0x23_19_bit0 -x_0x23_21_0x23_17_bit0 -x_0x23_21_0x23_15_bit0 -x_0x23_21_0x23_14_bit0 -x_0x23_21_0x23_12_bit0 -x_0x23_21_0x23_10_bit0 -x_0x23_21_0x23_7_bit0 -x_0x23_21_0x23_5_bit0 -x_0x23_21_0x23_4_bit0 -x_0x23_21_0x23_2_bit0 -x_0x23_20_0x23_35_bit0 -x_0x23_20_0x23_33_bit0 -x_0x23_20_0x23_31_bit0 -x_0x23_20_0x23_28_bit0 -x_0x23_20_0x23_25_bit0 -x_0x23_20_0x23_24_bit0 -x_0x23_20_0x23_22_bit0 -x_0x23_20_0x23_21_bit0 -x_0x23_20_0x23_19_bit0 -x_0x23_20_0x23_17_bit0 -x_0x23_20_0x23_15_bit0 -x_0x23_20_0x23_14_bit0 -x_0x23_20_0x23_12_bit0 -x_0x23_20_0x23_10_bit0 -x_0x23_20_0x23_7_bit0 -x_0x23_20_0x23_5_bit0 -x_0x23_20_0x23_4_bit0 x_0x23_20_0x23_2_bit0 -x_0x23_19_0x23_35_bit0 -x_0x23_19_0x23_33_bit0 -x_0x23_19_0x23_31_bit0 -x_0x23_19_0x23_28_bit0 -x_0x23_19_0x23_25_bit0 -x_0x23_19_0x23_24_bit0 -x_0x23_19_0x23_22_bit0 -x_0x23_19_0x23_21_bit0 -x_0x23_19_0x23_19_bit0 -x_0x23_19_0x23_17_bit0 -x_0x23_19_0x23_15_bit0 -x_0x23_19_0x23_14_bit0 -x_0x23_19_0x23_12_bit0 -x_0x23_19_0x23_10_bit0 -x_0x23_19_0x23_7_bit0 -x_0x23_19_0x23_5_bit0 -x_0x23_19_0x23_4_bit0 -x_0x23_19_0x23_2_bit0 -x_0x23_18_0x23_35_bit0 -x_0x23_18_0x23_33_bit0 -x_0x23_18_0x23_31_bit0 -x_0x23_18_0x23_28_bit0 -x_0x23_18_0x23_25_bit0 -x_0x23_18_0x23_24_bit0 -x_0x23_18_0x23_22_bit0 -x_0x23_18_0x23_21_bit0 -x_0x23_18_0x23_19_bit0 -x_0x23_18_0x23_17_bit0 -x_0x23_18_0x23_15_bit0 -x_0x23_18_0x23_14_bit0 -x_0x23_18_0x23_12_bit0 -x_0x23_18_0x23_10_bit0 -x_0x23_18_0x23_7_bit0 -x_0x23_18_0x23_5_bit0 -x_0x23_18_0x23_4_bit0 -x_0x23_18_0x23_2_bit0 -x_0x23_17_0x23_35_bit0 -x_0x23_17_0x23_33_bit0 -x_0x23_17_0x23_31_bit0 -x_0x23_17_0x23_28_bit0 -x_0x23_17_0x23_25_bit0 -x_0x23_17_0x23_24_bit0 -x_0x23_17_0x23_22_bit0 -x_0x23_17_0x23_21_bit0 -x_0x23_17_0x23_19_bit0 -x_0x23_17_0x23_17_bit0 -x_0x23_17_0x23_15_bit0 -x_0x23_17_0x23_14_bit0 -x_0x23_17_0x23_12_bit0 -x_0x23_17_0x23_10_bit0 -x_0x23_17_0x23_7_bit0 -x_0x23_17_0x23_5_bit0 -x_0x23_17_0x23_4_bit0 -x_0x23_17_0x23_2_bit0 -x_0x23_16_0x23_35_bit0 -x_0x23_16_0x23_33_bit0 -x_0x23_16_0x23_31_bit0 -x_0x23_16_0x23_28_bit0 -x_0x23_16_0x23_25_bit0 -x_0x23_16_0x23_24_bit0 -x_0x23_16_0x23_22_bit0 -x_0x23_16_0x23_21_bit0 -x_0x23_16_0x23_19_bit0 -x_0x23_16_0x23_17_bit0 -x_0x23_16_0x23_15_bit0 -x_0x23_16_0x23_14_bit0 -x_0x23_16_0x23_12_bit0 -x_0x23_16_0x23_10_bit0 -x_0x23_16_0x23_7_bit0 -x_0x23_16_0x23_5_bit0 -x_0x23_16_0x23_4_bit0 -x_0x23_16_0x23_2_bit0 -x_0x23_15_0x23_35_bit0 -x_0x23_15_0x23_33_bit0 -x_0x23_15_0x23_31_bit0 -x_0x23_15_0x23_28_bit0 -x_0x23_15_0x23_25_bit0 -x_0x23_15_0x23_24_bit0 -x_0x23_15_0x23_22_bit0 -x_0x23_15_0x23_21_bit0 -x_0x23_15_0x23_19_bit0 -x_0x23_15_0x23_17_bit0 -x_0x23_15_0x23_15_bit0 -x_0x23_15_0x23_14_bit0 -x_0x23_15_0x23_12_bit0 -x_0x23_15_0x23_10_bit0 -x_0x23_15_0x23_7_bit0 -x_0x23_15_0x23_5_bit0 -x_0x23_15_0x23_4_bit0 -x_0x23_15_0x23_2_bit0 -x_0x23_14_0x23_35_bit0 -x_0x23_14_0x23_33_bit0 -x_0x23_14_0x23_31_bit0 -x_0x23_14_0x23_28_bit0 -x_0x23_14_0x23_25_bit0 -x_0x23_14_0x23_24_bit0 -x_0x23_14_0x23_22_bit0 -x_0x23_14_0x23_21_bit0 -x_0x23_14_0x23_19_bit0 -x_0x23_14_0x23_17_bit0 -x_0x23_14_0x23_15_bit0 -x_0x23_14_0x23_14_bit0 -x_0x23_14_0x23_12_bit0 -x_0x23_14_0x23_10_bit0 -x_0x23_14_0x23_7_bit0 -x_0x23_14_0x23_5_bit0 -x_0x23_14_0x23_4_bit0 -x_0x23_14_0x23_2_bit0 -x_0x23_13_0x23_35_bit0 -x_0x23_13_0x23_33_bit0 -x_0x23_13_0x23_31_bit0 -x_0x23_13_0x23_28_bit0 -x_0x23_13_0x23_25_bit0 -x_0x23_13_0x23_24_bit0 -x_0x23_13_0x23_22_bit0 -x_0x23_13_0x23_21_bit0 -x_0x23_13_0x23_19_bit0 -x_0x23_13_0x23_17_bit0 -x_0x23_13_0x23_15_bit0 -x_0x23_13_0x23_14_bit0 -x_0x23_13_0x23_12_bit0 -x_0x23_13_0x23_10_bit0 -x_0x23_13_0x23_7_bit0 -x_0x23_13_0x23_5_bit0 -x_0x23_13_0x23_4_bit0 -x_0x23_13_0x23_2_bit0 -x_0x23_12_0x23_35_bit0 -x_0x23_12_0x23_33_bit0 -x_0x23_12_0x23_31_bit0 -x_0x23_12_0x23_28_bit0 -x_0x23_12_0x23_25_bit0 -x_0x23_12_0x23_24_bit0 -x_0x23_12_0x23_22_bit0 -x_0x23_12_0x23_21_bit0 -x_0x23_12_0x23_19_bit0 -x_0x23_12_0x23_17_bit0 -x_0x23_12_0x23_15_bit0 -x_0x23_12_0x23_14_bit0 -x_0x23_12_0x23_12_bit0 -x_0x23_12_0x23_10_bit0 -x_0x23_12_0x23_7_bit0 -x_0x23_12_0x23_5_bit0 x_0x23_12_0x23_4_bit0 -x_0x23_12_0x23_2_bit0 -x_0x23_11_0x23_35_bit0 -x_0x23_11_0x23_33_bit0 -x_0x23_11_0x23_31_bit0 -x_0x23_11_0x23_28_bit0 -x_0x23_11_0x23_25_bit0 -x_0x23_11_0x23_24_bit0 -x_0x23_11_0x23_22_bit0 -x_0x23_11_0x23_21_bit0 -x_0x23_11_0x23_19_bit0 -x_0x23_11_0x23_17_bit0 -x_0x23_11_0x23_15_bit0 -x_0x23_11_0x23_14_bit0 -x_0x23_11_0x23_12_bit0 -x_0x23_11_0x23_10_bit0 -x_0x23_11_0x23_7_bit0 x_0x23_11_0x23_5_bit0 -x_0x23_11_0x23_4_bit0 -x_0x23_11_0x23_2_bit0 -x_0x23_10_0x23_35_bit0 -x_0x23_10_0x23_33_bit0 -x_0x23_10_0x23_31_bit0 -x_0x23_10_0x23_28_bit0 -x_0x23_10_0x23_25_bit0 -x_0x23_10_0x23_24_bit0 -x_0x23_10_0x23_22_bit0 -x_0x23_10_0x23_21_bit0 -x_0x23_10_0x23_19_bit0 -x_0x23_10_0x23_17_bit0 -x_0x23_10_0x23_15_bit0 -x_0x23_10_0x23_14_bit0 -x_0x23_10_0x23_12_bit0 -x_0x23_10_0x23_10_bit0 -x_0x23_10_0x23_7_bit0 -x_0x23_10_0x23_5_bit0 -x_0x23_10_0x23_4_bit0 -x_0x23_10_0x23_2_bit0 -x_0x23_9_0x23_35_bit0 -x_0x23_9_0x23_33_bit0 -x_0x23_9_0x23_31_bit0 -x_0x23_9_0x23_28_bit0 -x_0x23_9_0x23_25_bit0 -x_0x23_9_0x23_24_bit0 -x_0x23_9_0x23_22_bit0 -x_0x23_9_0x23_21_bit0 -x_0x23_9_0x23_19_bit0 -x_0x23_9_0x23_17_bit0 -x_0x23_9_0x23_15_bit0 -x_0x23_9_0x23_14_bit0 -x_0x23_9_0x23_12_bit0 -x_0x23_9_0x23_10_bit0 x_0x23_9_0x23_7_bit0 -x_0x23_9_0x23_5_bit0 -x_0x23_9_0x23_4_bit0 -x_0x23_9_0x23_2_bit0 -x_0x23_8_0x23_35_bit0 -x_0x23_8_0x23_33_bit0 -x_0x23_8_0x23_31_bit0 -x_0x23_8_0x23_28_bit0 -x_0x23_8_0x23_25_bit0 -x_0x23_8_0x23_24_bit0 -x_0x23_8_0x23_22_bit0 -x_0x23_8_0x23_21_bit0 -x_0x23_8_0x23_19_bit0 -x_0x23_8_0x23_17_bit0 -x_0x23_8_0x23_15_bit0 -x_0x23_8_0x23_14_bit0 -x_0x23_8_0x23_12_bit0 -x_0x23_8_0x23_10_bit0 -x_0x23_8_0x23_7_bit0 -x_0x23_8_0x23_5_bit0 -x_0x23_8_0x23_4_bit0 -x_0x23_8_0x23_2_bit0 -x_0x23_7_0x23_35_bit0 -x_0x23_7_0x23_33_bit0 -x_0x23_7_0x23_31_bit0 -x_0x23_7_0x23_28_bit0 -x_0x23_7_0x23_25_bit0 -x_0x23_7_0x23_24_bit0 -x_0x23_7_0x23_22_bit0 -x_0x23_7_0x23_21_bit0 -x_0x23_7_0x23_19_bit0 -x_0x23_7_0x23_17_bit0 -x_0x23_7_0x23_15_bit0 -x_0x23_7_0x23_14_bit0 -x_0x23_7_0x23_12_bit0 -x_0x23_7_0x23_10_bit0 -x_0x23_7_0x23_7_bit0 -x_0x23_7_0x23_5_bit0 -x_0x23_7_0x23_4_bit0 -x_0x23_7_0x23_2_bit0 -x_0x23_6_0x23_35_bit0 -x_0x23_6_0x23_33_bit0 x_0x23_6_0x23_31_bit0 -x_0x23_6_0x23_28_bit0 -x_0x23_6_0x23_25_bit0 -x_0x23_6_0x23_24_bit0 -x_0x23_6_0x23_22_bit0 -x_0x23_6_0x23_21_bit0 #### 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.92 0.96 0.91 2/54 15959
Raw data (stat): 15959 (runsolver) R 15958 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483782057 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 3486 0 0 0 988 10 0 0 25 0 1 0 483782057 15982592 3329 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3902 3329 603 41 0 3861 0
vsize: 15608
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 4118 0 0 0 1984 13 0 0 25 0 1 0 483782057 18665472 3961 4294967295 134512640 134672761 3221224624 3221223728 134560337 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4557 3961 603 41 0 4516 0
vsize: 18228
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 4750 0 0 0 2982 15 0 0 25 0 1 0 483782057 21245952 4593 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5187 4593 603 41 0 5146 0
vsize: 20748
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 5351 0 0 0 3980 17 0 0 25 0 1 0 483782057 23662592 5194 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5777 5194 603 41 0 5736 0
vsize: 23108
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 5925 0 0 0 4978 19 0 0 25 0 1 0 483782057 25948160 5768 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6335 5768 603 41 0 6294 0
vsize: 25340
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 6469 0 0 0 5977 20 0 0 25 0 1 0 483782057 28262400 6312 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6900 6312 603 41 0 6859 0
vsize: 27600
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 7080 0 0 0 6974 22 0 0 25 0 1 0 483782057 30793728 6923 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7518 6924 603 41 0 7477 0
vsize: 30072
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 7675 0 0 0 7973 23 0 0 25 0 1 0 483782057 33193984 7518 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8104 7518 603 41 0 8063 0
vsize: 32416
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 8202 0 0 0 8971 25 0 0 25 0 1 0 483782057 35311616 8045 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8621 8045 603 41 0 8580 0
vsize: 34484
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 8714 0 0 0 9970 27 0 0 25 0 1 0 483782057 37462016 8557 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9146 8557 603 41 0 9105 0
vsize: 36584
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 9250 0 0 0 10968 28 0 0 25 0 1 0 483782057 39616512 9093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9672 9093 603 41 0 9631 0
vsize: 38688
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 9735 0 0 0 11967 29 0 0 25 0 1 0 483782057 41631744 9578 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10164 9578 603 41 0 10123 0
vsize: 40656
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 10271 0 0 0 12965 31 0 0 25 0 1 0 483782057 43905024 10114 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 10114 603 41 0 10678 0
vsize: 42876
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 10845 0 0 0 13964 33 0 0 25 0 1 0 483782057 46321664 10688 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10688 603 41 0 11268 0
vsize: 45236
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 11337 0 0 0 14963 35 0 0 25 0 1 0 483782057 48345088 11180 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11803 11180 603 41 0 11762 0
vsize: 47212
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 11786 0 0 0 15961 36 0 0 25 0 1 0 483782057 50077696 11629 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12226 11629 603 41 0 12185 0
vsize: 48904
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 12498 0 0 0 16960 38 0 0 25 0 1 0 483782057 53035008 12341 4294967295 134512640 134672761 3221224624 3221223728 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12948 12342 603 41 0 12907 0
vsize: 51792
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 13138 0 0 0 17958 39 0 0 25 0 1 0 483782057 55685120 12981 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13595 12981 603 41 0 13554 0
vsize: 54380
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 13726 0 0 0 18957 40 0 0 25 0 1 0 483782057 58089472 13569 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14182 13569 603 41 0 14141 0
vsize: 56728
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 14302 0 0 0 19956 42 0 0 25 0 1 0 483782057 60350464 14145 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14734 14145 603 41 0 14693 0
vsize: 58936
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 14843 0 0 0 20955 43 0 0 25 0 1 0 483782057 62636032 14686 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15292 14686 603 41 0 15251 0
vsize: 61168
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 15344 0 0 0 21954 45 0 0 25 0 1 0 483782057 64643072 15187 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15782 15187 603 41 0 15741 0
vsize: 63128
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 15841 0 0 0 22953 46 0 0 25 0 1 0 483782057 66654208 15684 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16273 15684 603 41 0 16232 0
vsize: 65092
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 16356 0 0 0 23951 48 0 0 25 0 1 0 483782057 68784128 16199 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16793 16199 603 41 0 16752 0
vsize: 67172
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 16836 0 0 0 24950 49 0 0 25 0 1 0 483782057 70774784 16679 4294967295 134512640 134672761 3221224624 3221223792 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17279 16679 603 41 0 17238 0
vsize: 69116
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 17330 0 0 0 25948 51 0 0 25 0 1 0 483782057 72777728 17173 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17768 17173 603 41 0 17727 0
vsize: 71072
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15959
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 17858 0 0 0 26947 52 0 0 25 0 1 0 483782057 75014144 17701 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18314 17701 603 41 0 18273 0
vsize: 73256
[startup+280.002 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 18363 0 0 0 27945 54 0 0 25 0 1 0 483782057 77008896 18206 4294967295 134512640 134672761 3221224624 3221223728 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18801 18206 603 41 0 18760 0
vsize: 75204
[startup+290.002 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 18728 0 0 0 28944 55 0 0 25 0 1 0 483782057 78475264 18571 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19159 18571 603 41 0 19118 0
vsize: 76636
[startup+300.002 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 19048 0 0 0 29943 56 0 0 25 0 1 0 483782057 79814656 18891 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19486 18891 603 41 0 19445 0
vsize: 77944
[startup+310.002 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 19431 0 0 0 30942 57 0 0 25 0 1 0 483782057 81436672 19274 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19882 19274 603 41 0 19841 0
vsize: 79528
[startup+320.002 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 19738 0 0 0 31940 59 0 0 25 0 1 0 483782057 82911232 19581 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20242 19581 603 41 0 20201 0
vsize: 80968
[startup+330.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 20034 0 0 0 32940 59 0 0 25 0 1 0 483782057 84115456 19877 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20536 19877 603 41 0 20495 0
vsize: 82144
[startup+340.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16012
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 20321 0 0 0 33940 60 0 0 25 0 1 0 483782057 85319680 20164 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20830 20164 603 41 0 20789 0
vsize: 83320
[startup+350.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 20574 0 0 0 34939 61 0 0 25 0 1 0 483782057 86388736 20417 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21091 20417 603 41 0 21050 0
vsize: 84364
[startup+360.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 20847 0 0 0 35938 62 0 0 25 0 1 0 483782057 87461888 20690 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21353 20690 603 41 0 21312 0
vsize: 85412
[startup+370.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 21111 0 0 0 36937 63 0 0 25 0 1 0 483782057 88547328 20954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21618 20954 603 41 0 21577 0
vsize: 86472
[startup+380.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 21398 0 0 0 37937 64 0 0 25 0 1 0 483782057 89751552 21241 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21912 21241 603 41 0 21871 0
vsize: 87648
[startup+390.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 21643 0 0 0 38936 64 0 0 25 0 1 0 483782057 90685440 21486 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22140 21486 603 41 0 22099 0
vsize: 88560
[startup+400.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 21908 0 0 0 39936 65 0 0 25 0 1 0 483782057 91762688 21751 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22403 21751 603 41 0 22362 0
vsize: 89612
[startup+410.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 22196 0 0 0 40935 66 0 0 25 0 1 0 483782057 93007872 22039 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22707 22039 603 41 0 22666 0
vsize: 90828
[startup+420.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 22460 0 0 0 41934 67 0 0 25 0 1 0 483782057 94072832 22303 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22967 22303 603 41 0 22926 0
vsize: 91868
[startup+430.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 22714 0 0 0 42934 67 0 0 25 0 1 0 483782057 95141888 22557 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23228 22557 603 41 0 23187 0
vsize: 92912
[startup+440.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 22942 0 0 0 43934 67 0 0 25 0 1 0 483782057 96092160 22785 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23460 22785 603 41 0 23419 0
vsize: 93840
[startup+450.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 23166 0 0 0 44934 68 0 0 25 0 1 0 483782057 97026048 23009 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23688 23009 603 41 0 23647 0
vsize: 94752
[startup+460.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 23405 0 0 0 45933 68 0 0 25 0 1 0 483782057 97964032 23248 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23917 23248 603 41 0 23876 0
vsize: 95668
[startup+470.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 23688 0 0 0 46932 69 0 0 25 0 1 0 483782057 99180544 23531 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24214 23531 603 41 0 24173 0
vsize: 96856
[startup+480.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 23898 0 0 0 47931 70 0 0 25 0 1 0 483782057 99975168 23741 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24408 23741 603 41 0 24367 0
vsize: 97632
[startup+490.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 24182 0 0 0 48931 71 0 0 25 0 1 0 483782057 101175296 24025 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24701 24025 603 41 0 24660 0
vsize: 98804
[startup+500.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 24503 0 0 0 49929 72 0 0 25 0 1 0 483782057 102514688 24346 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25028 24346 603 41 0 24987 0
vsize: 100112
[startup+510.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 24751 0 0 0 50929 73 0 0 25 0 1 0 483782057 103444480 24594 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25255 24594 603 41 0 25214 0
vsize: 101020
[startup+520.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 24991 0 0 0 51927 75 0 0 25 0 1 0 483782057 104517632 24834 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25517 24834 603 41 0 25476 0
vsize: 102068
[startup+530.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 25258 0 0 0 52927 75 0 0 25 0 1 0 483782057 105590784 25101 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25779 25101 603 41 0 25738 0
vsize: 103116
[startup+540.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 25531 0 0 0 53926 76 0 0 25 0 1 0 483782057 106672128 25374 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26043 25374 603 41 0 26002 0
vsize: 104172
[startup+550.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 25775 0 0 0 54926 77 0 0 25 0 1 0 483782057 107610112 25618 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26272 25618 603 41 0 26231 0
vsize: 105088
[startup+560.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 25973 0 0 0 55926 77 0 0 25 0 1 0 483782057 108429312 25816 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26472 25816 603 41 0 26431 0
vsize: 105888
[startup+570.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26201 0 0 0 56926 78 0 0 25 0 1 0 483782057 109383680 26044 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26705 26044 603 41 0 26664 0
vsize: 106820
[startup+580.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26406 0 0 0 57926 78 0 0 25 0 1 0 483782057 110321664 26249 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26934 26249 603 41 0 26893 0
vsize: 107736
[startup+590.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26612 0 0 0 58925 79 0 0 25 0 1 0 483782057 111120384 26455 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27129 26455 603 41 0 27088 0
vsize: 108516
[startup+600.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16014
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26702 0 0 0 59925 79 0 0 25 0 1 0 483782057 111517696 26545 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26545 603 41 0 27185 0
vsize: 108904
[startup+610.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 60925 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223808 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+620.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 61925 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+630.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 62926 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+640.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 63926 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+650.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 64926 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+660.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 65926 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+670.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 66927 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+680.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 67927 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+690.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 68927 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+700.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 69927 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+710.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26703 0 0 0 70927 79 0 0 25 0 1 0 483782057 111517696 26546 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26546 603 41 0 27185 0
vsize: 108904
[startup+720.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26704 0 0 0 71928 79 0 0 25 0 1 0 483782057 111517696 26547 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26547 603 41 0 27185 0
vsize: 108904
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26704 0 0 0 72928 79 0 0 25 0 1 0 483782057 111517696 26547 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26547 603 41 0 27185 0
vsize: 108904
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 73927 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+750.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 74927 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+760.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 75927 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+770.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 76928 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+780.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 77929 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+790.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 78929 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+800.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 79929 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+810.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 80929 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+820.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 81929 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134555197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+830.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 82930 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+840.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 83930 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+850.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 84930 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+860.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 85930 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+870.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 86931 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+880.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 87932 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+890.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 88933 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+900.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 89934 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+910.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 90934 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+920.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 91934 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+930.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 92935 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+940.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 93935 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+950.086 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 94937 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+960.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 95939 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+970.105 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 96939 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+980.112 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 97940 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+990.123 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 98941 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223728 134560128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+1000.24 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 99953 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+1010.24 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 100954 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+1020.27 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26705 0 0 0 101957 79 0 0 25 0 1 0 483782057 111517696 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26548 603 41 0 27185 0
vsize: 108904
[startup+1030.27 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 102952 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1040.27 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 103952 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1050.28 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 104953 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1060.28 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 105953 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1070.28 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 106953 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1080.28 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 107953 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1090.28 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 108954 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1100.28 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 109954 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1110.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 110954 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1120.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 111954 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1130.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 112954 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1140.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 113955 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223624 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1150.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 114955 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1160.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 115955 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1170.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 116955 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1180.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 117955 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1190.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 118955 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
[startup+1200.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 16016
Raw data (stat): 15959 (minisat+) R 15958 24215 24214 0 -1 0 26707 0 0 0 119956 80 0 0 25 0 1 0 483782057 111517696 26550 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27226 26550 603 41 0 27185 0
vsize: 108904
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.67 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 16016
Raw data (stat): 15959 (minisat+) Z 15958 24215 24214 0 -1 12 26710 0 0 0 119956 85 0 0 23 0 1 0 483782057 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.67
CPU time (s): 1200.42
CPU user time (s): 1199.57
CPU system time (s): 0.85287
CPU usage (%): 99.9788
Max. virtual memory (Kb): 108904
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####