%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SYN428+1 : TPTP v6.4.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n129.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 06:41:45 EDT 2016
% Result : CounterSatisfiable 166.78s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN428+1 : TPTP v6.4.0. Released v2.1.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.23 % Computer : n129.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 32218.75MB
% 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Fri Apr 8 23:50:39 CDT 2016
% 0.03/0.23 % CPUTime:
% 6.30/5.83 > val it = (): unit
% 7.20/6.80 Trying to find a model that refutes: ~ ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((ALL U.
% 7.20/6.80 bnd_ndr1_0 -->
% 7.20/6.80 (((bnd_ndr1_1 U & ~ bnd_c9_2 U bnd_a1834) &
% 7.20/6.80 ~ bnd_c3_2 U bnd_a1834) &
% 7.20/6.80 bnd_c7_2 U bnd_a1834 |
% 7.20/6.80 (bnd_ndr1_1 U & bnd_c3_2 U bnd_a1835) &
% 7.20/6.80 bnd_c5_2 U bnd_a1835) |
% 7.20/6.80 ((bnd_ndr1_1 U & bnd_c1_2 U bnd_a1836) &
% 7.20/6.80 ~ bnd_c4_2 U bnd_a1836) &
% 7.20/6.80 bnd_c6_2 U bnd_a1836) |
% 7.20/6.80 bnd_c4_0) |
% 7.20/6.80 ~ bnd_c6_0) &
% 7.20/6.80 (((ALL V.
% 7.20/6.80 bnd_ndr1_0 -->
% 7.20/6.80 (ALL W.
% 7.20/6.80 bnd_ndr1_1 V -->
% 7.20/6.80 (~ bnd_c5_2 V W | bnd_c7_2 V W) | bnd_c3_2 V W) |
% 7.20/6.80 bnd_c6_1 V) |
% 7.20/6.80 bnd_c7_0) |
% 7.20/6.80 bnd_c8_0)) &
% 7.20/6.80 (((ALL X.
% 7.20/6.80 bnd_ndr1_0 -->
% 7.20/6.80 (bnd_c4_1 X |
% 7.20/6.80 ((bnd_ndr1_1 X & bnd_c7_2 X bnd_a1837) &
% 7.20/6.80 bnd_c6_2 X bnd_a1837) &
% 7.20/6.80 ~ bnd_c3_2 X bnd_a1837) |
% 7.20/6.80 ((bnd_ndr1_1 X & ~ bnd_c1_2 X bnd_a1838) &
% 7.20/6.80 bnd_c10_2 X bnd_a1838) &
% 7.20/6.80 bnd_c6_2 X bnd_a1838) |
% 7.20/6.80 ~ bnd_c7_0) |
% 7.20/6.80 (ALL Y.
% 7.20/6.80 bnd_ndr1_0 -->
% 7.20/6.80 ((ALL Z.
% 7.20/6.80 bnd_ndr1_1 Y --> ~ bnd_c1_2 Y Z | ~ bnd_c7_2 Y Z) |
% 7.20/6.80 ~ bnd_c6_1 Y) |
% 7.20/6.80 ~ bnd_c10_1 Y))) &
% 7.20/6.80 ((bnd_c8_0 |
% 7.20/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1839) &
% 7.20/6.80 bnd_c8_2 bnd_a1839 bnd_a1840) &
% 7.20/6.80 bnd_c2_2 bnd_a1839 bnd_a1840) &
% 7.20/6.80 bnd_c3_2 bnd_a1839 bnd_a1840) &
% 7.20/6.80 bnd_c2_1 bnd_a1839) &
% 7.20/6.80 ~ bnd_c10_1 bnd_a1839) |
% 7.20/6.80 (((bnd_ndr1_0 &
% 7.20/6.80 (ALL X1.
% 7.20/6.80 bnd_ndr1_1 bnd_a1841 -->
% 7.20/6.80 ~ bnd_c2_2 bnd_a1841 X1 | ~ bnd_c7_2 bnd_a1841 X1)) &
% 7.20/6.80 bnd_ndr1_1 bnd_a1841) &
% 7.20/6.80 bnd_c4_2 bnd_a1841 bnd_a1842) &
% 7.20/6.80 bnd_c2_2 bnd_a1841 bnd_a1842)) &
% 7.20/6.80 ((~ bnd_c8_0 |
% 7.20/6.80 (ALL X2.
% 7.20/6.80 bnd_ndr1_0 -->
% 7.20/6.80 (((bnd_ndr1_1 X2 & bnd_c9_2 X2 bnd_a1843) &
% 7.20/6.80 bnd_c7_2 X2 bnd_a1843) &
% 7.20/6.80 ~ bnd_c3_2 X2 bnd_a1843 |
% 7.20/6.80 ((bnd_ndr1_1 X2 & bnd_c7_2 X2 bnd_a1844) &
% 7.20/6.80 bnd_c10_2 X2 bnd_a1844) &
% 7.20/6.80 bnd_c6_2 X2 bnd_a1844) |
% 7.20/6.80 (ALL X3.
% 7.20/6.80 bnd_ndr1_1 X2 -->
% 7.20/6.80 (bnd_c5_2 X2 X3 | ~ bnd_c6_2 X2 X3) |
% 7.31/6.80 ~ bnd_c4_2 X2 X3))) |
% 7.31/6.80 (ALL X4.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c9_1 X4 | ~ bnd_c3_1 X4) |
% 7.31/6.80 (ALL X5.
% 7.31/6.80 bnd_ndr1_1 X4 -->
% 7.31/6.80 (~ bnd_c4_2 X4 X5 | bnd_c2_2 X4 X5) |
% 7.31/6.80 ~ bnd_c1_2 X4 X5)))) &
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a1845) & ~ bnd_c10_1 bnd_a1845) &
% 7.31/6.80 (ALL X6.
% 7.31/6.80 bnd_ndr1_1 bnd_a1845 -->
% 7.31/6.80 (~ bnd_c4_2 bnd_a1845 X6 | bnd_c5_2 bnd_a1845 X6) |
% 7.31/6.80 ~ bnd_c7_2 bnd_a1845 X6) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_c9_1 bnd_a1846) & bnd_ndr1_1 bnd_a1846) &
% 7.31/6.80 bnd_c5_2 bnd_a1846 bnd_a1847) &
% 7.31/6.80 bnd_c8_2 bnd_a1846 bnd_a1847) &
% 7.31/6.80 bnd_c7_2 bnd_a1846 bnd_a1847) &
% 7.31/6.80 (ALL X7.
% 7.31/6.80 bnd_ndr1_1 bnd_a1846 -->
% 7.31/6.80 bnd_c6_2 bnd_a1846 X7 | bnd_c5_2 bnd_a1846 X7)) |
% 7.31/6.80 ~ bnd_c7_0)) &
% 7.31/6.80 (~ bnd_c5_0 |
% 7.31/6.80 (ALL X8. bnd_ndr1_0 --> bnd_c5_1 X8 | bnd_c3_1 X8))) &
% 7.31/6.80 ((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X9.
% 7.31/6.80 bnd_ndr1_1 bnd_a1848 -->
% 7.31/6.80 (bnd_c3_2 bnd_a1848 X9 | bnd_c1_2 bnd_a1848 X9) |
% 7.31/6.80 ~ bnd_c5_2 bnd_a1848 X9)) &
% 7.31/6.80 (ALL X10.
% 7.31/6.80 bnd_ndr1_1 bnd_a1848 -->
% 7.31/6.80 ~ bnd_c2_2 bnd_a1848 X10 | bnd_c6_2 bnd_a1848 X10)) &
% 7.31/6.80 ~ bnd_c2_1 bnd_a1848 |
% 7.31/6.80 bnd_c9_0) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_c6_1 bnd_a1849) & bnd_ndr1_1 bnd_a1849) &
% 7.31/6.80 bnd_c5_2 bnd_a1849 bnd_a1850) &
% 7.31/6.80 bnd_c7_2 bnd_a1849 bnd_a1850) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1849 bnd_a1850) &
% 7.31/6.80 ~ bnd_c3_1 bnd_a1849)) &
% 7.31/6.80 ((~ bnd_c7_0 | bnd_c4_0) |
% 7.31/6.80 (((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X11.
% 7.31/6.80 bnd_ndr1_1 bnd_a1851 -->
% 7.31/6.80 ~ bnd_c4_2 bnd_a1851 X11 | ~ bnd_c7_2 bnd_a1851 X11)) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1851) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1851 bnd_a1852) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1851 bnd_a1852) &
% 7.31/6.80 bnd_c3_2 bnd_a1851 bnd_a1852) &
% 7.31/6.80 (ALL X12.
% 7.31/6.80 bnd_ndr1_1 bnd_a1851 -->
% 7.31/6.80 (bnd_c4_2 bnd_a1851 X12 | bnd_c5_2 bnd_a1851 X12) |
% 7.31/6.80 ~ bnd_c8_2 bnd_a1851 X12))) &
% 7.31/6.80 ((~ bnd_c6_0 | bnd_c10_0) | ~ bnd_c7_0)) &
% 7.31/6.80 (~ bnd_c4_0 | ~ bnd_c8_0)) &
% 7.31/6.80 ((bnd_c1_0 |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1853) &
% 7.31/6.80 (ALL X13.
% 7.31/6.80 bnd_ndr1_1 bnd_a1853 -->
% 7.31/6.80 (bnd_c10_2 bnd_a1853 X13 | bnd_c3_2 bnd_a1853 X13) |
% 7.31/6.80 bnd_c6_2 bnd_a1853 X13)) &
% 7.31/6.80 bnd_c1_1 bnd_a1853) |
% 7.31/6.80 bnd_c5_0)) &
% 7.31/6.80 ((~ bnd_c4_0 | bnd_c5_0) | ~ bnd_c3_0)) &
% 7.31/6.80 ((~ bnd_c6_0 |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c7_1 bnd_a1854) & bnd_c6_1 bnd_a1854) &
% 7.31/6.80 bnd_c3_1 bnd_a1854) |
% 7.31/6.80 (ALL X14.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X14 & bnd_c10_2 X14 bnd_a1855) &
% 7.31/6.80 bnd_c1_2 X14 bnd_a1855) &
% 7.31/6.80 bnd_c6_2 X14 bnd_a1855 |
% 7.31/6.80 ((bnd_ndr1_1 X14 & ~ bnd_c5_2 X14 bnd_a1856) &
% 7.31/6.80 bnd_c1_2 X14 bnd_a1856) &
% 7.31/6.80 bnd_c10_2 X14 bnd_a1856) |
% 7.31/6.80 bnd_c10_1 X14))) &
% 7.31/6.80 ((~ bnd_c9_0 | ~ bnd_c3_0) | ~ bnd_c4_0)) &
% 7.31/6.80 ((~ bnd_c4_0 | ~ bnd_c1_0) |
% 7.31/6.80 (bnd_ndr1_0 & ~ bnd_c4_1 bnd_a1857) &
% 7.31/6.80 (ALL X15.
% 7.31/6.80 bnd_ndr1_1 bnd_a1857 -->
% 7.31/6.80 ~ bnd_c5_2 bnd_a1857 X15 | bnd_c8_2 bnd_a1857 X15))) &
% 7.31/6.80 ((bnd_c2_0 | ~ bnd_c7_0) | ~ bnd_c10_0)) &
% 7.31/6.80 ((~ bnd_c7_0 |
% 7.31/6.80 (ALL X16.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c7_1 X16 | bnd_c8_1 X16) |
% 7.31/6.80 (ALL X17.
% 7.31/6.80 bnd_ndr1_1 X16 -->
% 7.31/6.80 (bnd_c9_2 X16 X17 | ~ bnd_c7_2 X16 X17) | bnd_c3_2 X16 X17))) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_c8_1 bnd_a1858) & bnd_ndr1_1 bnd_a1858) &
% 7.31/6.80 bnd_c4_2 bnd_a1858 bnd_a1859) &
% 7.31/6.80 ~ bnd_c6_2 bnd_a1858 bnd_a1859) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1858 bnd_a1859) &
% 7.31/6.80 ~ bnd_c10_1 bnd_a1858)) &
% 7.31/6.80 ((~ bnd_c6_0 |
% 7.31/6.80 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1860) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1860 bnd_a1861) &
% 7.31/6.80 ~ bnd_c9_2 bnd_a1860 bnd_a1861) &
% 7.31/6.80 bnd_c5_2 bnd_a1860 bnd_a1861) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1860) &
% 7.31/6.80 bnd_c1_2 bnd_a1860 bnd_a1862) &
% 7.31/6.80 bnd_c3_2 bnd_a1860 bnd_a1862) &
% 7.31/6.80 bnd_c5_2 bnd_a1860 bnd_a1862) &
% 7.31/6.80 (ALL X18.
% 7.31/6.80 bnd_ndr1_1 bnd_a1860 -->
% 7.31/6.80 (bnd_c8_2 bnd_a1860 X18 | ~ bnd_c3_2 bnd_a1860 X18) |
% 7.31/6.80 bnd_c5_2 bnd_a1860 X18)) |
% 7.31/6.80 ~ bnd_c2_0)) &
% 7.31/6.80 ((ALL X19.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X19 & bnd_c8_2 X19 bnd_a1863) & ~ bnd_c3_2 X19 bnd_a1863) &
% 7.31/6.80 ~ bnd_c1_2 X19 bnd_a1863 |
% 7.31/6.80 ~ bnd_c8_1 X19) |
% 7.31/6.80 ((bnd_ndr1_1 X19 & ~ bnd_c1_2 X19 bnd_a1864) & bnd_c8_2 X19 bnd_a1864) &
% 7.31/6.80 bnd_c7_2 X19 bnd_a1864) |
% 7.31/6.80 (((((((((((bnd_ndr1_0 &
% 7.31/6.80 bnd_ndr1_1 bnd_a1865) &
% 7.31/6.80 ~ bnd_c7_2 bnd_a1865 bnd_a1866) &
% 7.31/6.80 bnd_c8_2 bnd_a1865 bnd_a1866) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1865 bnd_a1866) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1865) &
% 7.31/6.80 bnd_c3_2 bnd_a1865 bnd_a1867) &
% 7.31/6.80 ~ bnd_c9_2 bnd_a1865 bnd_a1867) &
% 7.31/6.80 ~ bnd_c5_2 bnd_a1865 bnd_a1867) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1865) &
% 7.31/6.80 bnd_c2_2 bnd_a1865 bnd_a1868) &
% 7.31/6.80 ~ bnd_c7_2 bnd_a1865 bnd_a1868) &
% 7.31/6.80 ~ bnd_c6_2 bnd_a1865 bnd_a1868)) &
% 7.31/6.80 ((~ bnd_c1_0 | bnd_c7_0) | bnd_c8_0)) &
% 7.31/6.80 ((~ bnd_c7_0 |
% 7.31/6.80 (ALL X20.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c10_1 X20 | bnd_c4_1 X20) |
% 7.31/6.80 (ALL X21.
% 7.31/6.80 bnd_ndr1_1 X20 -->
% 7.31/6.80 (bnd_c1_2 X20 X21 | bnd_c10_2 X20 X21) | bnd_c4_2 X20 X21))) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1869) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1869 bnd_a1870) &
% 7.31/6.80 ~ bnd_c9_2 bnd_a1869 bnd_a1870) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1869 bnd_a1870) &
% 7.31/6.80 bnd_c4_1 bnd_a1869) &
% 7.31/6.80 bnd_c9_1 bnd_a1869)) &
% 7.31/6.80 (((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X22.
% 7.31/6.80 bnd_ndr1_1 bnd_a1871 -->
% 7.31/6.80 (bnd_c8_2 bnd_a1871 X22 | bnd_c3_2 bnd_a1871 X22) |
% 7.31/6.80 bnd_c9_2 bnd_a1871 X22)) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1871) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1871 bnd_a1872) &
% 7.31/6.80 ~ bnd_c5_2 bnd_a1871 bnd_a1872 |
% 7.31/6.80 (ALL X23.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c10_1 X23 | bnd_c4_1 X23) |
% 7.31/6.80 ((bnd_ndr1_1 X23 & ~ bnd_c4_2 X23 bnd_a1873) & bnd_c3_2 X23 bnd_a1873) &
% 7.31/6.80 ~ bnd_c10_2 X23 bnd_a1873)) |
% 7.31/6.80 (ALL X24.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X24 &
% 7.31/6.80 ~ bnd_c2_2 X24 bnd_a1874) &
% 7.31/6.80 bnd_c10_2 X24 bnd_a1874) &
% 7.31/6.80 bnd_c1_2 X24 bnd_a1874 |
% 7.31/6.80 bnd_c6_1 X24) |
% 7.31/6.80 bnd_c2_1 X24))) &
% 7.31/6.80 ((((bnd_ndr1_0 & ~ bnd_c10_1 bnd_a1875) &
% 7.31/6.80 (ALL X25.
% 7.31/6.80 bnd_ndr1_1 bnd_a1875 -->
% 7.31/6.80 (~ bnd_c4_2 bnd_a1875 X25 | ~ bnd_c10_2 bnd_a1875 X25) |
% 7.31/6.80 ~ bnd_c8_2 bnd_a1875 X25)) &
% 7.31/6.80 bnd_c6_1 bnd_a1875 |
% 7.31/6.80 bnd_c1_0) |
% 7.31/6.80 (bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1876) &
% 7.31/6.80 ~ bnd_c5_1 bnd_a1876)) &
% 7.31/6.80 (((ALL X26.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (ALL X27.
% 7.31/6.80 bnd_ndr1_1 X26 -->
% 7.31/6.80 (bnd_c6_2 X26 X27 | bnd_c3_2 X26 X27) | ~ bnd_c2_2 X26 X27) |
% 7.31/6.80 ~ bnd_c8_1 X26) |
% 7.31/6.80 ~ bnd_c6_0) |
% 7.31/6.80 bnd_c10_0)) &
% 7.31/6.80 (((ALL X28.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c3_1 X28 | bnd_c2_1 X28) |
% 7.31/6.80 (ALL X29.
% 7.31/6.80 bnd_ndr1_1 X28 --> bnd_c8_2 X28 X29 | bnd_c2_2 X28 X29)) |
% 7.31/6.80 bnd_c9_0) |
% 7.31/6.80 bnd_c3_0)) &
% 7.31/6.80 ((~ bnd_c7_0 |
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c10_1 bnd_a1877) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1877) &
% 7.31/6.80 ~ bnd_c1_2 bnd_a1877 bnd_a1878) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1877 bnd_a1878) &
% 7.31/6.80 bnd_c10_2 bnd_a1877 bnd_a1878) |
% 7.31/6.80 bnd_c9_0)) &
% 7.31/6.80 ((~ bnd_c4_0 |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1879) &
% 7.31/6.80 bnd_c6_2 bnd_a1879 bnd_a1880) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1879 bnd_a1880) &
% 7.31/6.80 bnd_c5_2 bnd_a1879 bnd_a1880) &
% 7.31/6.80 (ALL X30.
% 7.31/6.80 bnd_ndr1_1 bnd_a1879 -->
% 7.31/6.80 bnd_c2_2 bnd_a1879 X30 |
% 7.31/6.80 ~ bnd_c6_2 bnd_a1879 X30)) &
% 7.31/6.80 bnd_c2_1 bnd_a1879) |
% 7.31/6.80 (((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1881) &
% 7.31/6.80 ~ bnd_c3_1 bnd_a1881) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1881) &
% 7.31/6.80 ~ bnd_c8_2 bnd_a1881 bnd_a1882) &
% 7.31/6.80 bnd_c1_2 bnd_a1881 bnd_a1882) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1881 bnd_a1882)) &
% 7.31/6.80 ((~ bnd_c5_0 | ~ bnd_c4_0) |
% 7.31/6.80 (ALL X31.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c4_1 X31 | bnd_c1_1 X31) |
% 7.31/6.80 ((bnd_ndr1_1 X31 & bnd_c9_2 X31 bnd_a1883) &
% 7.31/6.80 bnd_c4_2 X31 bnd_a1883) &
% 7.31/6.80 bnd_c6_2 X31 bnd_a1883))) &
% 7.31/6.80 ((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X32.
% 7.31/6.80 bnd_ndr1_1 bnd_a1884 -->
% 7.31/6.80 (bnd_c9_2 bnd_a1884 X32 |
% 7.31/6.80 ~ bnd_c1_2 bnd_a1884 X32) |
% 7.31/6.80 bnd_c7_2 bnd_a1884 X32)) &
% 7.31/6.80 ~ bnd_c7_1 bnd_a1884) &
% 7.31/6.80 bnd_c10_1 bnd_a1884 |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1885) &
% 7.31/6.80 (ALL X33.
% 7.31/6.80 bnd_ndr1_1 bnd_a1885 -->
% 7.31/6.80 (bnd_c8_2 bnd_a1885 X33 |
% 7.31/6.80 ~ bnd_c2_2 bnd_a1885 X33) |
% 7.31/6.80 ~ bnd_c3_2 bnd_a1885 X33)) &
% 7.31/6.80 ~ bnd_c8_1 bnd_a1885) |
% 7.31/6.80 ~ bnd_c1_0)) &
% 7.31/6.80 (bnd_c5_0 | bnd_c9_0)) &
% 7.31/6.80 (((((((bnd_ndr1_0 & bnd_c7_1 bnd_a1886) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1886) &
% 7.31/6.80 bnd_c4_2 bnd_a1886 bnd_a1887) &
% 7.31/6.80 ~ bnd_c1_2 bnd_a1886 bnd_a1887) &
% 7.31/6.80 bnd_c5_2 bnd_a1886 bnd_a1887) &
% 7.31/6.80 ~ bnd_c9_1 bnd_a1886 |
% 7.31/6.80 ~ bnd_c4_0) |
% 7.31/6.80 ~ bnd_c10_0)) &
% 7.31/6.80 ((~ bnd_c8_0 | ~ bnd_c4_0) | ~ bnd_c10_0)) &
% 7.31/6.80 (((ALL X34.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X34 & ~ bnd_c6_2 X34 bnd_a1888) &
% 7.31/6.80 ~ bnd_c5_2 X34 bnd_a1888) &
% 7.31/6.80 ~ bnd_c7_2 X34 bnd_a1888 |
% 7.31/6.80 ((bnd_ndr1_1 X34 & ~ bnd_c7_2 X34 bnd_a1889) &
% 7.31/6.80 bnd_c6_2 X34 bnd_a1889) &
% 7.31/6.80 ~ bnd_c1_2 X34 bnd_a1889) |
% 7.31/6.80 ~ bnd_c6_1 X34) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1890) &
% 7.31/6.80 bnd_c5_2 bnd_a1890 bnd_a1891) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1890 bnd_a1891) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1890 bnd_a1891) &
% 7.31/6.80 ~ bnd_c6_1 bnd_a1890) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a1890) |
% 7.31/6.80 ~ bnd_c1_0)) &
% 7.31/6.80 (((((((bnd_ndr1_0 & bnd_c4_1 bnd_a1892) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1892) &
% 7.31/6.80 bnd_c3_2 bnd_a1892 bnd_a1893) &
% 7.31/6.80 bnd_c1_2 bnd_a1892 bnd_a1893) &
% 7.31/6.80 bnd_c6_2 bnd_a1892 bnd_a1893) &
% 7.31/6.80 ~ bnd_c8_1 bnd_a1892 |
% 7.31/6.80 ((bnd_ndr1_0 &
% 7.31/6.80 (ALL X35.
% 7.31/6.80 bnd_ndr1_1 bnd_a1894 -->
% 7.31/6.80 ~ bnd_c9_2 bnd_a1894 X35 |
% 7.31/6.80 bnd_c4_2 bnd_a1894 X35)) &
% 7.31/6.80 (ALL X36.
% 7.31/6.80 bnd_ndr1_1 bnd_a1894 -->
% 7.31/6.80 (~ bnd_c6_2 bnd_a1894 X36 |
% 7.31/6.80 ~ bnd_c2_2 bnd_a1894 X36) |
% 7.31/6.80 ~ bnd_c4_2 bnd_a1894 X36)) &
% 7.31/6.80 ~ bnd_c9_1 bnd_a1894) |
% 7.31/6.80 ~ bnd_c6_0)) &
% 7.31/6.80 (((ALL X37.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X38.
% 7.31/6.80 bnd_ndr1_1 X37 -->
% 7.31/6.80 (bnd_c1_2 X37 X38 | bnd_c7_2 X37 X38) |
% 7.31/6.80 ~ bnd_c3_2 X37 X38) |
% 7.31/6.80 bnd_c9_1 X37) |
% 7.31/6.80 (ALL X39.
% 7.31/6.80 bnd_ndr1_1 X37 -->
% 7.31/6.80 bnd_c8_2 X37 X39 | bnd_c10_2 X37 X39)) |
% 7.31/6.80 ~ bnd_c10_0) |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c10_1 bnd_a1895) &
% 7.31/6.80 (ALL X40.
% 7.31/6.80 bnd_ndr1_1 bnd_a1895 -->
% 7.31/6.80 (bnd_c4_2 bnd_a1895 X40 |
% 7.31/6.80 ~ bnd_c10_2 bnd_a1895 X40) |
% 7.31/6.80 bnd_c3_2 bnd_a1895 X40)) &
% 7.31/6.80 bnd_c5_1 bnd_a1895)) &
% 7.31/6.80 (((ALL X41.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X42.
% 7.31/6.80 bnd_ndr1_1 X41 -->
% 7.31/6.80 (bnd_c5_2 X41 X42 | bnd_c10_2 X41 X42) |
% 7.31/6.80 ~ bnd_c9_2 X41 X42) |
% 7.31/6.80 bnd_c10_1 X41) |
% 7.31/6.80 (ALL X43.
% 7.31/6.80 bnd_ndr1_1 X41 -->
% 7.31/6.80 (bnd_c4_2 X41 X43 | bnd_c10_2 X41 X43) |
% 7.31/6.80 ~ bnd_c9_2 X41 X43)) |
% 7.31/6.80 (ALL X44.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c9_1 X44 | bnd_c1_1 X44) |
% 7.31/6.80 (ALL X45.
% 7.31/6.80 bnd_ndr1_1 X44 -->
% 7.31/6.80 bnd_c8_2 X44 X45 | bnd_c2_2 X44 X45))) |
% 7.31/6.80 ((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1896) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1896) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1896 bnd_a1897) &
% 7.31/6.80 bnd_c7_2 bnd_a1896 bnd_a1897) &
% 7.31/6.80 bnd_c6_2 bnd_a1896 bnd_a1897)) &
% 7.31/6.80 ((ALL X46.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X46 & ~ bnd_c1_2 X46 bnd_a1898) &
% 7.31/6.80 ~ bnd_c6_2 X46 bnd_a1898) &
% 7.31/6.80 bnd_c2_2 X46 bnd_a1898 |
% 7.31/6.80 bnd_c2_1 X46) |
% 7.31/6.80 (ALL X47.
% 7.31/6.80 bnd_ndr1_1 X46 -->
% 7.31/6.80 (bnd_c8_2 X46 X47 | bnd_c5_2 X46 X47) |
% 7.31/6.80 ~ bnd_c9_2 X46 X47)) |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1899) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a1899) &
% 7.31/6.80 (ALL X48.
% 7.31/6.80 bnd_ndr1_1 bnd_a1899 -->
% 7.31/6.80 (bnd_c1_2 bnd_a1899 X48 | ~ bnd_c9_2 bnd_a1899 X48) |
% 7.31/6.80 bnd_c2_2 bnd_a1899 X48))) &
% 7.31/6.80 (~ bnd_c4_0 | ~ bnd_c9_0)) &
% 7.31/6.80 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1900) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1900 bnd_a1901) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1900 bnd_a1901) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1900 bnd_a1901) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1900) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1900 bnd_a1902) &
% 7.31/6.80 bnd_c9_2 bnd_a1900 bnd_a1902) &
% 7.31/6.80 bnd_c2_2 bnd_a1900 bnd_a1902) &
% 7.31/6.80 ~ bnd_c6_1 bnd_a1900 |
% 7.31/6.80 bnd_c3_0) |
% 7.31/6.80 bnd_c10_0)) &
% 7.31/6.80 ((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X49.
% 7.31/6.80 bnd_ndr1_1 bnd_a1903 -->
% 7.31/6.80 (bnd_c7_2 bnd_a1903 X49 | ~ bnd_c9_2 bnd_a1903 X49) |
% 7.31/6.80 ~ bnd_c8_2 bnd_a1903 X49)) &
% 7.31/6.80 bnd_c3_1 bnd_a1903) &
% 7.31/6.80 (ALL X50.
% 7.31/6.80 bnd_ndr1_1 bnd_a1903 -->
% 7.31/6.80 (~ bnd_c4_2 bnd_a1903 X50 | bnd_c7_2 bnd_a1903 X50) |
% 7.31/6.80 bnd_c5_2 bnd_a1903 X50) |
% 7.31/6.80 (ALL X51.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X51 & ~ bnd_c8_2 X51 bnd_a1904) &
% 7.31/6.80 ~ bnd_c7_2 X51 bnd_a1904) &
% 7.31/6.80 bnd_c10_2 X51 bnd_a1904 |
% 7.31/6.80 bnd_c6_1 X51) |
% 7.31/6.80 ((bnd_ndr1_1 X51 & ~ bnd_c4_2 X51 bnd_a1905) &
% 7.31/6.80 bnd_c5_2 X51 bnd_a1905) &
% 7.31/6.80 ~ bnd_c10_2 X51 bnd_a1905)) |
% 7.31/6.80 ((bnd_ndr1_0 &
% 7.31/6.80 (ALL X52.
% 7.31/6.80 bnd_ndr1_1 bnd_a1906 -->
% 7.31/6.80 (~ bnd_c3_2 bnd_a1906 X52 | ~ bnd_c2_2 bnd_a1906 X52) |
% 7.31/6.80 ~ bnd_c1_2 bnd_a1906 X52)) &
% 7.31/6.80 bnd_c4_1 bnd_a1906) &
% 7.31/6.80 (ALL X53.
% 7.31/6.80 bnd_ndr1_1 bnd_a1906 -->
% 7.31/6.80 (bnd_c9_2 bnd_a1906 X53 | ~ bnd_c2_2 bnd_a1906 X53) |
% 7.31/6.80 ~ bnd_c1_2 bnd_a1906 X53))) &
% 7.31/6.80 ((bnd_c3_0 | bnd_c9_0) |
% 7.31/6.80 (ALL X54.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c6_1 X54 |
% 7.31/6.80 (ALL X55.
% 7.31/6.80 bnd_ndr1_1 X54 -->
% 7.31/6.80 (~ bnd_c9_2 X54 X55 | bnd_c8_2 X54 X55) |
% 7.31/6.80 ~ bnd_c7_2 X54 X55)) |
% 7.31/6.80 ~ bnd_c3_1 X54))) &
% 7.31/6.80 ((~ bnd_c3_0 |
% 7.31/6.80 (ALL X56.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 bnd_c3_1 X56 |
% 7.31/6.80 (ALL X57.
% 7.31/6.80 bnd_ndr1_1 X56 -->
% 7.31/6.80 (bnd_c1_2 X56 X57 | ~ bnd_c10_2 X56 X57) |
% 7.31/6.80 ~ bnd_c2_2 X56 X57))) |
% 7.31/6.80 (ALL X58. bnd_ndr1_0 --> ~ bnd_c3_1 X58 | bnd_c9_1 X58))) &
% 7.31/6.80 (((ALL X59. bnd_ndr1_0 --> ~ bnd_c3_1 X59 | ~ bnd_c4_1 X59) |
% 7.31/6.80 ~ bnd_c3_0) |
% 7.31/6.80 (ALL X60.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X61.
% 7.31/6.80 bnd_ndr1_1 X60 -->
% 7.31/6.80 ~ bnd_c7_2 X60 X61 | ~ bnd_c4_2 X60 X61) |
% 7.31/6.80 (ALL X62.
% 7.31/6.80 bnd_ndr1_1 X60 -->
% 7.31/6.80 ~ bnd_c2_2 X60 X62 | ~ bnd_c9_2 X60 X62)) |
% 7.31/6.80 (ALL X63.
% 7.31/6.80 bnd_ndr1_1 X60 -->
% 7.31/6.80 (~ bnd_c2_2 X60 X63 | bnd_c3_2 X60 X63) |
% 7.31/6.80 ~ bnd_c4_2 X60 X63)))) &
% 7.31/6.80 (((bnd_ndr1_0 & bnd_c5_1 bnd_a1907) & ~ bnd_c10_1 bnd_a1907) &
% 7.31/6.80 bnd_c8_1 bnd_a1907 |
% 7.31/6.80 ~ bnd_c5_0)) &
% 7.31/6.80 (((ALL X64.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c10_1 X64 | bnd_c7_1 X64) |
% 7.31/6.80 ((bnd_ndr1_1 X64 & bnd_c9_2 X64 bnd_a1908) &
% 7.31/6.80 bnd_c1_2 X64 bnd_a1908) &
% 7.31/6.80 bnd_c3_2 X64 bnd_a1908) |
% 7.31/6.80 bnd_c1_0) |
% 7.31/6.80 (ALL X65.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c8_1 X65 |
% 7.31/6.80 (ALL X66.
% 7.31/6.80 bnd_ndr1_1 X65 -->
% 7.31/6.80 (bnd_c4_2 X65 X66 | bnd_c3_2 X65 X66) |
% 7.31/6.80 bnd_c10_2 X65 X66)) |
% 7.31/6.80 ((bnd_ndr1_1 X65 & bnd_c10_2 X65 bnd_a1909) &
% 7.31/6.80 ~ bnd_c2_2 X65 bnd_a1909) &
% 7.31/6.80 ~ bnd_c8_2 X65 bnd_a1909))) &
% 7.31/6.80 ((bnd_c3_0 | ~ bnd_c8_0) | ~ bnd_c9_0)) &
% 7.31/6.80 ((~ bnd_c3_0 |
% 7.31/6.80 ((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X67.
% 7.31/6.80 bnd_ndr1_1 bnd_a1910 -->
% 7.31/6.80 bnd_c1_2 bnd_a1910 X67 | ~ bnd_c2_2 bnd_a1910 X67)) &
% 7.31/6.80 (ALL X68.
% 7.31/6.80 bnd_ndr1_1 bnd_a1910 -->
% 7.31/6.80 ~ bnd_c7_2 bnd_a1910 X68 | bnd_c4_2 bnd_a1910 X68)) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1910) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1910 bnd_a1911) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1910 bnd_a1911) |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a1912) &
% 7.31/6.80 (ALL X69.
% 7.31/6.80 bnd_ndr1_1 bnd_a1912 -->
% 7.31/6.80 (~ bnd_c5_2 bnd_a1912 X69 | bnd_c7_2 bnd_a1912 X69) |
% 7.31/6.80 bnd_c2_2 bnd_a1912 X69)) &
% 7.31/6.80 bnd_c3_1 bnd_a1912)) &
% 7.31/6.80 ((bnd_c10_0 | ~ bnd_c2_0) | bnd_c7_0)) &
% 7.31/6.80 (((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1913) &
% 7.31/6.80 (ALL X70.
% 7.31/6.80 bnd_ndr1_1 bnd_a1913 -->
% 7.31/6.80 (bnd_c9_2 bnd_a1913 X70 | bnd_c7_2 bnd_a1913 X70) |
% 7.31/6.80 bnd_c3_2 bnd_a1913 X70) |
% 7.31/6.80 bnd_c1_0) |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a1914) & bnd_c9_1 bnd_a1914) &
% 7.31/6.80 bnd_c5_1 bnd_a1914)) &
% 7.31/6.80 ((~ bnd_c9_0 |
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a1915) & bnd_ndr1_1 bnd_a1915) &
% 7.31/6.80 bnd_c5_2 bnd_a1915 bnd_a1916) &
% 7.31/6.80 ~ bnd_c9_2 bnd_a1915 bnd_a1916) &
% 7.31/6.80 (ALL X71.
% 7.31/6.80 bnd_ndr1_1 bnd_a1915 -->
% 7.31/6.80 bnd_c1_2 bnd_a1915 X71 | bnd_c7_2 bnd_a1915 X71)) |
% 7.31/6.80 bnd_c1_0)) &
% 7.31/6.80 ((bnd_c6_0 |
% 7.31/6.80 (ALL X72.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X73.
% 7.31/6.80 bnd_ndr1_1 X72 -->
% 7.31/6.80 (bnd_c9_2 X72 X73 | ~ bnd_c1_2 X72 X73) | bnd_c10_2 X72 X73) |
% 7.31/6.80 bnd_c8_1 X72) |
% 7.31/6.80 (ALL X74.
% 7.31/6.80 bnd_ndr1_1 X72 -->
% 7.31/6.80 (~ bnd_c10_2 X72 X74 | bnd_c2_2 X72 X74) |
% 7.31/6.80 ~ bnd_c7_2 X72 X74))) |
% 7.31/6.80 ~ bnd_c3_0)) &
% 7.31/6.80 (((ALL X75.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c5_1 X75 |
% 7.31/6.80 (ALL X76.
% 7.31/6.80 bnd_ndr1_1 X75 -->
% 7.31/6.80 (~ bnd_c3_2 X75 X76 | ~ bnd_c1_2 X75 X76) |
% 7.31/6.80 ~ bnd_c6_2 X75 X76)) |
% 7.31/6.80 bnd_c2_1 X75) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1917) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1917 bnd_a1918) &
% 7.31/6.80 bnd_c2_2 bnd_a1917 bnd_a1918) &
% 7.31/6.80 bnd_c5_2 bnd_a1917 bnd_a1918) &
% 7.31/6.80 (ALL X77.
% 7.31/6.80 bnd_ndr1_1 bnd_a1917 -->
% 7.31/6.80 (bnd_c10_2 bnd_a1917 X77 | bnd_c4_2 bnd_a1917 X77) |
% 7.31/6.80 ~ bnd_c9_2 bnd_a1917 X77)) &
% 7.31/6.80 bnd_c7_1 bnd_a1917) |
% 7.31/6.80 ~ bnd_c5_0)) &
% 7.31/6.80 (((((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1919) & bnd_ndr1_1 bnd_a1919) &
% 7.31/6.80 bnd_c3_2 bnd_a1919 bnd_a1920) &
% 7.31/6.80 bnd_c9_2 bnd_a1919 bnd_a1920) &
% 7.31/6.80 ~ bnd_c1_2 bnd_a1919 bnd_a1920) &
% 7.31/6.80 ~ bnd_c4_1 bnd_a1919 |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c8_1 bnd_a1921) & bnd_c5_1 bnd_a1921) &
% 7.31/6.80 ~ bnd_c6_1 bnd_a1921) |
% 7.31/6.80 ~ bnd_c4_0)) &
% 7.31/6.80 ((bnd_c4_0 | bnd_c7_0) |
% 7.31/6.80 (((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X78.
% 7.31/6.80 bnd_ndr1_1 bnd_a1922 -->
% 7.31/6.80 (~ bnd_c10_2 bnd_a1922 X78 | ~ bnd_c2_2 bnd_a1922 X78) |
% 7.31/6.80 ~ bnd_c5_2 bnd_a1922 X78)) &
% 7.31/6.80 bnd_c8_1 bnd_a1922) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1922) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1922 bnd_a1923) &
% 7.31/6.80 bnd_c8_2 bnd_a1922 bnd_a1923) &
% 7.31/6.80 ~ bnd_c7_2 bnd_a1922 bnd_a1923)) &
% 7.31/6.80 ((bnd_c1_0 |
% 7.31/6.80 ((bnd_ndr1_0 &
% 7.31/6.80 (ALL X79.
% 7.31/6.80 bnd_ndr1_1 bnd_a1924 -->
% 7.31/6.80 (~ bnd_c7_2 bnd_a1924 X79 | ~ bnd_c10_2 bnd_a1924 X79) |
% 7.31/6.80 ~ bnd_c8_2 bnd_a1924 X79)) &
% 7.31/6.80 ~ bnd_c5_1 bnd_a1924) &
% 7.31/6.80 (ALL X80.
% 7.31/6.80 bnd_ndr1_1 bnd_a1924 -->
% 7.31/6.80 (~ bnd_c8_2 bnd_a1924 X80 | bnd_c1_2 bnd_a1924 X80) |
% 7.31/6.80 ~ bnd_c9_2 bnd_a1924 X80)) |
% 7.31/6.80 (ALL X81.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X81 & bnd_c7_2 X81 bnd_a1925) & bnd_c5_2 X81 bnd_a1925) &
% 7.31/6.80 bnd_c10_2 X81 bnd_a1925 |
% 7.31/6.80 bnd_c6_1 X81) |
% 7.31/6.80 ~ bnd_c7_1 X81))) &
% 7.31/6.80 ((~ bnd_c3_0 |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a1926) & bnd_c5_1 bnd_a1926) &
% 7.31/6.80 ~ bnd_c6_1 bnd_a1926) |
% 7.31/6.80 ~ bnd_c5_0)) &
% 7.31/6.80 ((~ bnd_c10_0 | ~ bnd_c5_0) |
% 7.31/6.80 (ALL X82.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X83.
% 7.31/6.80 bnd_ndr1_1 X82 -->
% 7.31/6.80 (~ bnd_c10_2 X82 X83 | ~ bnd_c1_2 X82 X83) | ~ bnd_c5_2 X82 X83) |
% 7.31/6.80 (ALL X84.
% 7.31/6.80 bnd_ndr1_1 X82 -->
% 7.31/6.80 (~ bnd_c1_2 X82 X84 | bnd_c4_2 X82 X84) | ~ bnd_c5_2 X82 X84)) |
% 7.31/6.80 bnd_c3_1 X82))) &
% 7.31/6.80 ((ALL X85.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((bnd_ndr1_1 X85 & bnd_c1_2 X85 bnd_a1927) & ~ bnd_c9_2 X85 bnd_a1927 |
% 7.31/6.80 ~ bnd_c1_1 X85) |
% 7.31/6.80 bnd_c2_1 X85) |
% 7.31/6.80 bnd_c6_0)) &
% 7.31/6.80 (((bnd_ndr1_0 &
% 7.31/6.80 (ALL X86.
% 7.31/6.80 bnd_ndr1_1 bnd_a1928 -->
% 7.31/6.80 (bnd_c8_2 bnd_a1928 X86 | ~ bnd_c9_2 bnd_a1928 X86) |
% 7.31/6.80 ~ bnd_c10_2 bnd_a1928 X86)) &
% 7.31/6.80 (ALL X87.
% 7.31/6.80 bnd_ndr1_1 bnd_a1928 -->
% 7.31/6.80 (bnd_c3_2 bnd_a1928 X87 | ~ bnd_c9_2 bnd_a1928 X87) |
% 7.31/6.80 bnd_c7_2 bnd_a1928 X87) |
% 7.31/6.80 bnd_c5_0) |
% 7.31/6.80 (ALL X88.
% 7.31/6.80 bnd_ndr1_0 --> bnd_c5_1 X88 | ~ bnd_c6_1 X88))) &
% 7.31/6.80 (((ALL X89.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X89 & ~ bnd_c9_2 X89 bnd_a1929) & bnd_c8_2 X89 bnd_a1929) &
% 7.31/6.80 ~ bnd_c3_2 X89 bnd_a1929 |
% 7.31/6.80 ~ bnd_c5_1 X89) |
% 7.31/6.80 ~ bnd_c2_1 X89) |
% 7.31/6.80 (ALL X90.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c10_1 X90 | bnd_c3_1 X90) |
% 7.31/6.80 ((bnd_ndr1_1 X90 & ~ bnd_c6_2 X90 bnd_a1930) & bnd_c8_2 X90 bnd_a1930) &
% 7.31/6.80 bnd_c7_2 X90 bnd_a1930)) |
% 7.31/6.80 (((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a1931) &
% 7.31/6.80 (ALL X91.
% 7.31/6.80 bnd_ndr1_1 bnd_a1931 -->
% 7.31/6.80 (~ bnd_c2_2 bnd_a1931 X91 | bnd_c5_2 bnd_a1931 X91) |
% 7.31/6.80 ~ bnd_c1_2 bnd_a1931 X91)) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1931) &
% 7.31/6.80 bnd_c1_2 bnd_a1931 bnd_a1932) &
% 7.31/6.80 ~ bnd_c9_2 bnd_a1931 bnd_a1932) &
% 7.31/6.80 bnd_c7_2 bnd_a1931 bnd_a1932)) &
% 7.31/6.80 (((ALL X92.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c6_1 X92 | bnd_c5_1 X92) |
% 7.31/6.80 bnd_c9_1 X92) |
% 7.31/6.80 (ALL X93.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c6_1 X93 |
% 7.31/6.80 (ALL X94.
% 7.31/6.80 bnd_ndr1_1 X93 -->
% 7.31/6.80 (bnd_c5_2 X93 X94 | ~ bnd_c6_2 X93 X94) | ~ bnd_c2_2 X93 X94)) |
% 7.31/6.80 (ALL X95.
% 7.31/6.80 bnd_ndr1_1 X93 -->
% 7.31/6.80 (~ bnd_c6_2 X93 X95 | bnd_c7_2 X93 X95) | bnd_c5_2 X93 X95))) |
% 7.31/6.80 (ALL X96.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c4_1 X96 |
% 7.31/6.80 (ALL X97.
% 7.31/6.80 bnd_ndr1_1 X96 -->
% 7.31/6.80 (~ bnd_c1_2 X96 X97 | bnd_c10_2 X96 X97) | ~ bnd_c8_2 X96 X97)) |
% 7.31/6.80 bnd_c9_1 X96))) &
% 7.31/6.80 ((~ bnd_c5_0 | ~ bnd_c7_0) |
% 7.31/6.80 (((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a1933) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1933) &
% 7.31/6.80 ~ bnd_c1_2 bnd_a1933 bnd_a1934) &
% 7.31/6.80 bnd_c5_2 bnd_a1933 bnd_a1934) &
% 7.31/6.80 bnd_c8_2 bnd_a1933 bnd_a1934) &
% 7.31/6.80 ~ bnd_c3_1 bnd_a1933)) &
% 7.31/6.80 ((bnd_c2_0 |
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1935) &
% 7.31/6.80 ~ bnd_c8_2 bnd_a1935 bnd_a1936) &
% 7.31/6.80 bnd_c5_2 bnd_a1935 bnd_a1936) &
% 7.31/6.80 (ALL X98.
% 7.31/6.80 bnd_ndr1_1 bnd_a1935 -->
% 7.31/6.80 (~ bnd_c8_2 bnd_a1935 X98 |
% 7.31/6.80 bnd_c10_2 bnd_a1935 X98) |
% 7.31/6.80 bnd_c3_2 bnd_a1935 X98)) &
% 7.31/6.80 ~ bnd_c9_1 bnd_a1935) |
% 7.31/6.80 (ALL X99.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ~ bnd_c10_1 X99 | ~ bnd_c6_1 X99))) &
% 7.31/6.80 ((bnd_c10_0 | bnd_c7_0) |
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c2_1 bnd_a1937) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1937) &
% 7.31/6.80 ~ bnd_c7_2 bnd_a1937 bnd_a1938) &
% 7.31/6.80 ~ bnd_c6_2 bnd_a1937 bnd_a1938) &
% 7.31/6.80 ~ bnd_c10_1 bnd_a1937)) &
% 7.31/6.80 (((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1939) &
% 7.31/6.80 bnd_c10_1 bnd_a1939) &
% 7.31/6.80 (ALL X100.
% 7.31/6.80 bnd_ndr1_1 bnd_a1939 -->
% 7.31/6.80 ~ bnd_c8_2 bnd_a1939 X100 |
% 7.31/6.80 ~ bnd_c3_2 bnd_a1939 X100) |
% 7.31/6.80 (ALL X101.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((bnd_ndr1_1 X101 &
% 7.31/6.80 ~ bnd_c6_2 X101 bnd_a1940) &
% 7.31/6.80 bnd_c8_2 X101 bnd_a1940 |
% 7.31/6.80 bnd_c3_1 X101) |
% 7.31/6.80 ~ bnd_c6_1 X101))) &
% 7.31/6.80 ((~ bnd_c3_0 | bnd_c7_0) |
% 7.31/6.80 (bnd_ndr1_0 & ~ bnd_c1_1 bnd_a1941) &
% 7.31/6.80 ~ bnd_c9_1 bnd_a1941)) &
% 7.31/6.80 ((bnd_c7_0 |
% 7.31/6.80 (ALL X102.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c4_1 X102 |
% 7.31/6.80 ((bnd_ndr1_1 X102 &
% 7.31/6.80 ~ bnd_c3_2 X102 bnd_a1942) &
% 7.31/6.80 ~ bnd_c9_2 X102 bnd_a1942) &
% 7.31/6.80 ~ bnd_c6_2 X102 bnd_a1942) |
% 7.31/6.80 bnd_c2_1 X102)) |
% 7.31/6.80 (ALL X103.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c2_1 X103 | ~ bnd_c3_1 X103) |
% 7.31/6.80 ~ bnd_c10_1 X103))) &
% 7.31/6.80 ((bnd_c6_0 | bnd_c1_0) |
% 7.31/6.80 (ALL X104.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X105.
% 7.31/6.80 bnd_ndr1_1 X104 -->
% 7.31/6.80 (~ bnd_c9_2 X104 X105 |
% 7.31/6.80 bnd_c8_2 X104 X105) |
% 7.31/6.80 bnd_c2_2 X104 X105) |
% 7.31/6.80 (ALL X106.
% 7.31/6.80 bnd_ndr1_1 X104 -->
% 7.31/6.80 bnd_c10_2 X104 X106 |
% 7.31/6.80 ~ bnd_c1_2 X104 X106)) |
% 7.31/6.80 ~ bnd_c9_1 X104))) &
% 7.31/6.80 (((((((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a1943) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1943) &
% 7.31/6.80 bnd_c4_2 bnd_a1943 bnd_a1944) &
% 7.31/6.80 ~ bnd_c1_2 bnd_a1943 bnd_a1944) &
% 7.31/6.80 bnd_c10_2 bnd_a1943 bnd_a1944) &
% 7.31/6.80 ~ bnd_c4_1 bnd_a1943 |
% 7.31/6.80 ((bnd_ndr1_0 &
% 7.31/6.80 (ALL X107.
% 7.31/6.80 bnd_ndr1_1 bnd_a1945 -->
% 7.31/6.80 bnd_c2_2 bnd_a1945 X107 |
% 7.31/6.80 ~ bnd_c4_2 bnd_a1945 X107)) &
% 7.31/6.80 (ALL X108.
% 7.31/6.80 bnd_ndr1_1 bnd_a1945 -->
% 7.31/6.80 (~ bnd_c10_2 bnd_a1945 X108 |
% 7.31/6.80 ~ bnd_c5_2 bnd_a1945 X108) |
% 7.31/6.80 ~ bnd_c3_2 bnd_a1945 X108)) &
% 7.31/6.80 ~ bnd_c4_1 bnd_a1945) |
% 7.31/6.80 (ALL X109.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (ALL X110.
% 7.31/6.80 bnd_ndr1_1 X109 -->
% 7.31/6.80 (~ bnd_c3_2 X109 X110 |
% 7.31/6.80 ~ bnd_c8_2 X109 X110) |
% 7.31/6.80 bnd_c1_2 X109 X110) |
% 7.31/6.80 (ALL X111.
% 7.31/6.80 bnd_ndr1_1 X109 -->
% 7.31/6.80 (~ bnd_c6_2 X109 X111 |
% 7.31/6.80 ~ bnd_c8_2 X109 X111) |
% 7.31/6.80 bnd_c3_2 X109 X111)))) &
% 7.31/6.80 (((bnd_ndr1_0 & bnd_c8_1 bnd_a1946) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a1946 |
% 7.31/6.80 bnd_c9_0) |
% 7.31/6.80 (ALL X112.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c10_1 X112 |
% 7.31/6.80 ((bnd_ndr1_1 X112 & bnd_c9_2 X112 bnd_a1947) &
% 7.31/6.80 bnd_c2_2 X112 bnd_a1947) &
% 7.31/6.80 bnd_c7_2 X112 bnd_a1947) |
% 7.31/6.80 ((bnd_ndr1_1 X112 & ~ bnd_c10_2 X112 bnd_a1948) &
% 7.31/6.80 bnd_c7_2 X112 bnd_a1948) &
% 7.31/6.80 ~ bnd_c6_2 X112 bnd_a1948))) &
% 7.31/6.80 (((ALL X113.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c8_1 X113 | bnd_c1_1 X113) |
% 7.31/6.80 ((bnd_ndr1_1 X113 & bnd_c9_2 X113 bnd_a1949) &
% 7.31/6.80 bnd_c7_2 X113 bnd_a1949) &
% 7.31/6.80 bnd_c10_2 X113 bnd_a1949) |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c5_1 bnd_a1950) &
% 7.31/6.80 (ALL X114.
% 7.31/6.80 bnd_ndr1_1 bnd_a1950 -->
% 7.31/6.80 (bnd_c10_2 bnd_a1950 X114 |
% 7.31/6.80 bnd_c3_2 bnd_a1950 X114) |
% 7.31/6.80 ~ bnd_c4_2 bnd_a1950 X114)) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a1950) |
% 7.31/6.80 (bnd_ndr1_0 & ~ bnd_c3_1 bnd_a1951) &
% 7.31/6.80 bnd_c5_1 bnd_a1951)) &
% 7.31/6.80 ((~ bnd_c7_0 |
% 7.31/6.80 (ALL X115.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c8_1 X115 | ~ bnd_c1_1 X115) |
% 7.31/6.80 (ALL X116.
% 7.31/6.80 bnd_ndr1_1 X115 --> ~ bnd_c2_2 X115 X116))) |
% 7.31/6.80 ~ bnd_c5_0)) &
% 7.31/6.80 (((ALL X117.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (ALL X118.
% 7.31/6.80 bnd_ndr1_1 X117 -->
% 7.31/6.80 (~ bnd_c7_2 X117 X118 | ~ bnd_c6_2 X117 X118) |
% 7.31/6.80 ~ bnd_c3_2 X117 X118) |
% 7.31/6.80 bnd_c6_1 X117) |
% 7.31/6.80 ~ bnd_c5_0) |
% 7.31/6.80 (bnd_ndr1_0 & ~ bnd_c10_1 bnd_a1952) &
% 7.31/6.80 (ALL X119.
% 7.31/6.80 bnd_ndr1_1 bnd_a1952 -->
% 7.31/6.80 (~ bnd_c1_2 bnd_a1952 X119 |
% 7.31/6.80 ~ bnd_c7_2 bnd_a1952 X119) |
% 7.31/6.80 bnd_c3_2 bnd_a1952 X119))) &
% 7.31/6.80 (bnd_c3_0 |
% 7.31/6.80 (ALL X120.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X121.
% 7.31/6.80 bnd_ndr1_1 X120 -->
% 7.31/6.80 (bnd_c1_2 X120 X121 | ~ bnd_c5_2 X120 X121) |
% 7.31/6.80 ~ bnd_c7_2 X120 X121) |
% 7.31/6.80 ((bnd_ndr1_1 X120 & bnd_c4_2 X120 bnd_a1953) &
% 7.31/6.80 bnd_c10_2 X120 bnd_a1953) &
% 7.31/6.80 ~ bnd_c6_2 X120 bnd_a1953) |
% 7.31/6.80 ((bnd_ndr1_1 X120 & bnd_c3_2 X120 bnd_a1954) &
% 7.31/6.80 bnd_c10_2 X120 bnd_a1954) &
% 7.31/6.80 bnd_c5_2 X120 bnd_a1954))) &
% 7.31/6.80 (((ALL X122.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c10_1 X122 |
% 7.31/6.80 ((bnd_ndr1_1 X122 & bnd_c5_2 X122 bnd_a1955) &
% 7.31/6.80 bnd_c3_2 X122 bnd_a1955) &
% 7.31/6.80 ~ bnd_c1_2 X122 bnd_a1955) |
% 7.31/6.80 ~ bnd_c7_1 X122) |
% 7.31/6.80 bnd_c8_0) |
% 7.31/6.80 (ALL X123.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X123 & bnd_c8_2 X123 bnd_a1956) &
% 7.31/6.80 bnd_c1_2 X123 bnd_a1956) &
% 7.31/6.80 ~ bnd_c6_2 X123 bnd_a1956 |
% 7.31/6.80 ((bnd_ndr1_1 X123 & ~ bnd_c7_2 X123 bnd_a1957) &
% 7.31/6.80 ~ bnd_c8_2 X123 bnd_a1957) &
% 7.31/6.80 bnd_c6_2 X123 bnd_a1957) |
% 7.31/6.80 ~ bnd_c8_1 X123))) &
% 7.31/6.80 ((bnd_c7_0 | ~ bnd_c3_0) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1958) &
% 7.31/6.80 bnd_c4_2 bnd_a1958 bnd_a1959) &
% 7.31/6.80 ~ bnd_c7_2 bnd_a1958 bnd_a1959) &
% 7.31/6.80 bnd_c8_2 bnd_a1958 bnd_a1959) &
% 7.31/6.80 ~ bnd_c9_1 bnd_a1958) &
% 7.31/6.80 ~ bnd_c5_1 bnd_a1958)) &
% 7.31/6.80 ((bnd_c8_0 |
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1960) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1960 bnd_a1961) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1960 bnd_a1961) &
% 7.31/6.80 ~ bnd_c5_1 bnd_a1960) &
% 7.31/6.80 ~ bnd_c10_1 bnd_a1960) |
% 7.31/6.80 (ALL X124.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c6_1 X124 |
% 7.31/6.80 (ALL X125.
% 7.31/6.80 bnd_ndr1_1 X124 -->
% 7.31/6.80 (bnd_c9_2 X124 X125 | bnd_c1_2 X124 X125) |
% 7.31/6.80 bnd_c8_2 X124 X125)) |
% 7.31/6.80 bnd_c1_1 X124))) &
% 7.31/6.80 ((ALL X126.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c1_1 X126 | bnd_c8_1 X126) |
% 7.31/6.80 ((bnd_ndr1_1 X126 & bnd_c3_2 X126 bnd_a1962) &
% 7.31/6.80 bnd_c6_2 X126 bnd_a1962) &
% 7.31/6.80 ~ bnd_c9_2 X126 bnd_a1962) |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c5_1 bnd_a1963) &
% 7.31/6.80 (ALL X127.
% 7.31/6.80 bnd_ndr1_1 bnd_a1963 -->
% 7.31/6.80 (~ bnd_c10_2 bnd_a1963 X127 |
% 7.31/6.80 ~ bnd_c5_2 bnd_a1963 X127) |
% 7.31/6.80 bnd_c6_2 bnd_a1963 X127)) &
% 7.31/6.80 (ALL X128.
% 7.31/6.80 bnd_ndr1_1 bnd_a1963 -->
% 7.31/6.80 (~ bnd_c9_2 bnd_a1963 X128 | bnd_c4_2 bnd_a1963 X128) |
% 7.31/6.80 bnd_c1_2 bnd_a1963 X128))) &
% 7.31/6.80 (((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1964) &
% 7.31/6.80 bnd_c3_2 bnd_a1964 bnd_a1965) &
% 7.31/6.80 bnd_c9_2 bnd_a1964 bnd_a1965) &
% 7.31/6.80 ~ bnd_c4_2 bnd_a1964 bnd_a1965) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1964) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a1964 bnd_a1966) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1964 bnd_a1966) &
% 7.31/6.80 (ALL X129.
% 7.31/6.80 bnd_ndr1_1 bnd_a1964 -->
% 7.31/6.80 (bnd_c3_2 bnd_a1964 X129 | ~ bnd_c2_2 bnd_a1964 X129) |
% 7.31/6.80 bnd_c9_2 bnd_a1964 X129) |
% 7.31/6.80 ~ bnd_c6_0) |
% 7.31/6.80 bnd_c5_0)) &
% 7.31/6.80 ((ALL X130.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c5_1 X130 |
% 7.31/6.80 (ALL X131.
% 7.31/6.80 bnd_ndr1_1 X130 -->
% 7.31/6.80 (~ bnd_c10_2 X130 X131 | ~ bnd_c4_2 X130 X131) |
% 7.31/6.80 bnd_c6_2 X130 X131)) |
% 7.31/6.80 ~ bnd_c7_1 X130) |
% 7.31/6.80 ((bnd_ndr1_0 &
% 7.31/6.80 (ALL X132.
% 7.31/6.80 bnd_ndr1_1 bnd_a1967 -->
% 7.31/6.80 bnd_c3_2 bnd_a1967 X132 | bnd_c5_2 bnd_a1967 X132)) &
% 7.31/6.80 (ALL X133.
% 7.31/6.80 bnd_ndr1_1 bnd_a1967 -->
% 7.31/6.80 (bnd_c1_2 bnd_a1967 X133 | ~ bnd_c5_2 bnd_a1967 X133) |
% 7.31/6.80 bnd_c8_2 bnd_a1967 X133)) &
% 7.31/6.80 (ALL X134.
% 7.31/6.80 bnd_ndr1_1 bnd_a1967 -->
% 7.31/6.80 (bnd_c4_2 bnd_a1967 X134 | ~ bnd_c10_2 bnd_a1967 X134) |
% 7.31/6.80 ~ bnd_c7_2 bnd_a1967 X134))) &
% 7.31/6.80 (((ALL X135.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c10_1 X135 |
% 7.31/6.80 ((bnd_ndr1_1 X135 & ~ bnd_c7_2 X135 bnd_a1968) &
% 7.31/6.80 ~ bnd_c2_2 X135 bnd_a1968) &
% 7.31/6.80 bnd_c8_2 X135 bnd_a1968) |
% 7.31/6.80 bnd_c1_1 X135) |
% 7.31/6.80 ~ bnd_c2_0) |
% 7.31/6.80 (ALL X136.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c6_1 X136 | bnd_c10_1 X136) | bnd_c4_1 X136))) &
% 7.31/6.80 ((bnd_c7_0 | bnd_c10_0) | ~ bnd_c1_0)) &
% 7.31/6.80 ((ALL X137.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 bnd_c7_1 X137 |
% 7.31/6.80 (ALL X138.
% 7.31/6.80 bnd_ndr1_1 X137 -->
% 7.31/6.80 ~ bnd_c6_2 X137 X138 | ~ bnd_c3_2 X137 X138)) |
% 7.31/6.80 (ALL X139.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c2_1 X139 | bnd_c7_1 X139) |
% 7.31/6.80 ((bnd_ndr1_1 X139 & bnd_c1_2 X139 bnd_a1969) &
% 7.31/6.80 ~ bnd_c5_2 X139 bnd_a1969) &
% 7.31/6.80 ~ bnd_c8_2 X139 bnd_a1969))) &
% 7.31/6.80 ((~ bnd_c4_0 |
% 7.31/6.80 ((bnd_ndr1_0 & ~ bnd_c10_1 bnd_a1970) & ~ bnd_c5_1 bnd_a1970) &
% 7.31/6.80 bnd_c7_1 bnd_a1970) |
% 7.31/6.80 ~ bnd_c1_0)) &
% 7.31/6.80 (((((((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a1971) & bnd_ndr1_1 bnd_a1971) &
% 7.31/6.80 ~ bnd_c8_2 bnd_a1971 bnd_a1972) &
% 7.31/6.80 ~ bnd_c5_2 bnd_a1971 bnd_a1972) &
% 7.31/6.80 ~ bnd_c7_2 bnd_a1971 bnd_a1972) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1971) &
% 7.31/6.80 bnd_c7_2 bnd_a1971 bnd_a1973) &
% 7.31/6.80 bnd_c10_2 bnd_a1971 bnd_a1973 |
% 7.31/6.80 (ALL X140.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X140 & ~ bnd_c1_2 X140 bnd_a1974) &
% 7.31/6.80 ~ bnd_c2_2 X140 bnd_a1974) &
% 7.31/6.80 ~ bnd_c7_2 X140 bnd_a1974 |
% 7.31/6.80 ~ bnd_c6_1 X140) |
% 7.31/6.80 ~ bnd_c10_1 X140)) |
% 7.31/6.80 bnd_c5_0)) &
% 7.31/6.80 (((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a1975) &
% 7.31/6.80 (ALL X141.
% 7.31/6.80 bnd_ndr1_1 bnd_a1975 -->
% 7.31/6.80 (~ bnd_c7_2 bnd_a1975 X141 | ~ bnd_c10_2 bnd_a1975 X141) |
% 7.31/6.80 bnd_c5_2 bnd_a1975 X141) |
% 7.31/6.80 ~ bnd_c3_0) |
% 7.31/6.80 ~ bnd_c7_0)) &
% 7.31/6.80 (((ALL X142.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (ALL X143.
% 7.31/6.80 bnd_ndr1_1 X142 -->
% 7.31/6.80 (bnd_c4_2 X142 X143 | ~ bnd_c1_2 X142 X143) |
% 7.31/6.80 bnd_c10_2 X142 X143) |
% 7.31/6.80 bnd_c6_1 X142) |
% 7.31/6.80 (ALL X144.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 bnd_c5_1 X144 |
% 7.31/6.80 (ALL X145.
% 7.31/6.80 bnd_ndr1_1 X144 -->
% 7.31/6.80 (~ bnd_c1_2 X144 X145 | bnd_c5_2 X144 X145) |
% 7.31/6.80 bnd_c10_2 X144 X145))) |
% 7.31/6.80 ~ bnd_c10_0)) &
% 7.31/6.80 (~ bnd_c2_0 | bnd_c7_0)) &
% 7.31/6.80 ((bnd_c2_0 | ~ bnd_c10_0) | bnd_c9_0)) &
% 7.31/6.80 (((((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1976) & bnd_ndr1_1 bnd_a1976) &
% 7.31/6.80 bnd_c8_2 bnd_a1976 bnd_a1977) &
% 7.31/6.80 bnd_c7_2 bnd_a1976 bnd_a1977) &
% 7.31/6.80 ~ bnd_c6_2 bnd_a1976 bnd_a1977) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a1976 |
% 7.31/6.80 (ALL X146.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X147.
% 7.31/6.80 bnd_ndr1_1 X146 -->
% 7.31/6.80 (~ bnd_c2_2 X146 X147 | ~ bnd_c1_2 X146 X147) |
% 7.31/6.80 ~ bnd_c3_2 X146 X147) |
% 7.31/6.80 bnd_c3_1 X146) |
% 7.31/6.80 (ALL X148.
% 7.31/6.80 bnd_ndr1_1 X146 -->
% 7.31/6.80 (~ bnd_c3_2 X146 X148 | ~ bnd_c7_2 X146 X148) |
% 7.31/6.80 ~ bnd_c8_2 X146 X148))) |
% 7.31/6.80 (ALL X149.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c7_1 X149 |
% 7.31/6.80 (bnd_ndr1_1 X149 & bnd_c5_2 X149 bnd_a1978) &
% 7.31/6.80 bnd_c9_2 X149 bnd_a1978) |
% 7.31/6.80 (ALL X150.
% 7.31/6.80 bnd_ndr1_1 X149 -->
% 7.31/6.80 (~ bnd_c2_2 X149 X150 | bnd_c5_2 X149 X150) |
% 7.31/6.80 bnd_c7_2 X149 X150)))) &
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a1979) & bnd_c9_1 bnd_a1979) &
% 7.31/6.80 (ALL X151.
% 7.31/6.80 bnd_ndr1_1 bnd_a1979 -->
% 7.31/6.80 (~ bnd_c7_2 bnd_a1979 X151 | ~ bnd_c4_2 bnd_a1979 X151) |
% 7.31/6.80 ~ bnd_c10_2 bnd_a1979 X151) |
% 7.31/6.80 bnd_c3_0) |
% 7.31/6.80 (ALL X152.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c10_1 X152 |
% 7.31/6.80 ((bnd_ndr1_1 X152 & bnd_c1_2 X152 bnd_a1980) &
% 7.31/6.80 bnd_c7_2 X152 bnd_a1980) &
% 7.31/6.80 bnd_c4_2 X152 bnd_a1980) |
% 7.31/6.80 ((bnd_ndr1_1 X152 & ~ bnd_c5_2 X152 bnd_a1981) &
% 7.31/6.80 ~ bnd_c2_2 X152 bnd_a1981) &
% 7.31/6.80 bnd_c7_2 X152 bnd_a1981))) &
% 7.31/6.80 (((ALL X153.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 bnd_c3_1 X153 |
% 7.31/6.80 ((bnd_ndr1_1 X153 & bnd_c5_2 X153 bnd_a1982) &
% 7.31/6.80 bnd_c10_2 X153 bnd_a1982) &
% 7.31/6.80 ~ bnd_c9_2 X153 bnd_a1982) |
% 7.31/6.80 bnd_c9_0) |
% 7.31/6.80 ~ bnd_c5_0)) &
% 7.31/6.80 (bnd_c9_0 | bnd_c1_0)) &
% 7.31/6.80 ((~ bnd_c3_0 | ~ bnd_c6_0) |
% 7.31/6.80 ~ bnd_c9_0)) &
% 7.31/6.80 (((ALL X154.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c2_1 X154 | ~ bnd_c5_1 X154) |
% 7.31/6.80 ((bnd_ndr1_1 X154 & ~ bnd_c5_2 X154 bnd_a1983) &
% 7.31/6.80 bnd_c8_2 X154 bnd_a1983) &
% 7.31/6.80 bnd_c1_2 X154 bnd_a1983) |
% 7.31/6.80 (ALL X155.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X155 & bnd_c8_2 X155 bnd_a1984) &
% 7.31/6.80 ~ bnd_c10_2 X155 bnd_a1984) &
% 7.31/6.80 bnd_c9_2 X155 bnd_a1984 |
% 7.31/6.80 bnd_c1_1 X155) |
% 7.31/6.80 ((bnd_ndr1_1 X155 & bnd_c8_2 X155 bnd_a1985) & bnd_c6_2 X155 bnd_a1985) &
% 7.31/6.80 bnd_c3_2 X155 bnd_a1985)) |
% 7.31/6.80 (((((bnd_ndr1_0 &
% 7.31/6.80 bnd_ndr1_1 bnd_a1986) &
% 7.31/6.80 ~ bnd_c5_2 bnd_a1986 bnd_a1987) &
% 7.31/6.80 bnd_c7_2 bnd_a1986 bnd_a1987) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1986 bnd_a1987) &
% 7.31/6.80 ~ bnd_c9_1 bnd_a1986) &
% 7.31/6.80 ~ bnd_c7_1 bnd_a1986)) &
% 7.31/6.80 (((ALL X156.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c4_1 X156 |
% 7.31/6.80 (ALL X157.
% 7.31/6.80 bnd_ndr1_1 X156 -->
% 7.31/6.80 (~ bnd_c1_2 X156 X157 | bnd_c3_2 X156 X157) |
% 7.31/6.80 ~ bnd_c8_2 X156 X157)) |
% 7.31/6.80 bnd_c5_1 X156) |
% 7.31/6.80 (((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X158.
% 7.31/6.80 bnd_ndr1_1 bnd_a1988 -->
% 7.31/6.80 (~ bnd_c5_2 bnd_a1988 X158 | ~ bnd_c2_2 bnd_a1988 X158) |
% 7.31/6.80 ~ bnd_c1_2 bnd_a1988 X158)) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1988) &
% 7.31/6.80 ~ bnd_c3_2 bnd_a1988 bnd_a1989) &
% 7.31/6.80 ~ bnd_c6_2 bnd_a1988 bnd_a1989) &
% 7.31/6.80 bnd_c5_2 bnd_a1988 bnd_a1989) &
% 7.31/6.80 ~ bnd_c5_1 bnd_a1988) |
% 7.31/6.80 (ALL X159.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c9_1 X159 | ~ bnd_c8_1 X159) |
% 7.31/6.80 (ALL X160.
% 7.31/6.80 bnd_ndr1_1 X159 -->
% 7.31/6.80 (~ bnd_c8_2 X159 X160 | bnd_c5_2 X159 X160) | bnd_c10_2 X159 X160)))) &
% 7.31/6.80 ((bnd_c2_0 | ~ bnd_c1_0) |
% 7.31/6.80 (ALL X161.
% 7.31/6.80 bnd_ndr1_0 --> (~ bnd_c6_1 X161 | ~ bnd_c4_1 X161) | bnd_c5_1 X161))) &
% 7.31/6.80 (((ALL X162.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X162 & ~ bnd_c5_2 X162 bnd_a1990) &
% 7.31/6.80 bnd_c10_2 X162 bnd_a1990) &
% 7.31/6.80 ~ bnd_c2_2 X162 bnd_a1990 |
% 7.31/6.80 ~ bnd_c10_1 X162) |
% 7.31/6.80 ((bnd_ndr1_1 X162 & bnd_c1_2 X162 bnd_a1991) & ~ bnd_c9_2 X162 bnd_a1991) &
% 7.31/6.80 ~ bnd_c4_2 X162 bnd_a1991) |
% 7.31/6.80 (ALL X163.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X163 & ~ bnd_c2_2 X163 bnd_a1992) & bnd_c8_2 X163 bnd_a1992) &
% 7.31/6.80 bnd_c10_2 X163 bnd_a1992 |
% 7.31/6.80 ((bnd_ndr1_1 X163 & bnd_c8_2 X163 bnd_a1993) & bnd_c10_2 X163 bnd_a1993) &
% 7.31/6.80 ~ bnd_c9_2 X163 bnd_a1993) |
% 7.31/6.80 bnd_c1_1 X163)) |
% 7.31/6.80 ~ bnd_c6_0)) &
% 7.31/6.80 (((ALL X164.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((bnd_ndr1_1 X164 &
% 7.31/6.80 ~ bnd_c10_2 X164 bnd_a1994) &
% 7.31/6.80 bnd_c9_2 X164 bnd_a1994 |
% 7.31/6.80 bnd_c4_1 X164) |
% 7.31/6.80 ~ bnd_c10_1 X164) |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1995) &
% 7.31/6.80 ~ bnd_c6_2 bnd_a1995 bnd_a1996) &
% 7.31/6.80 bnd_c5_2 bnd_a1995 bnd_a1996) &
% 7.31/6.80 ~ bnd_c1_2 bnd_a1995 bnd_a1996) &
% 7.31/6.80 (ALL X165.
% 7.31/6.80 bnd_ndr1_1 bnd_a1995 -->
% 7.31/6.80 (~ bnd_c3_2 bnd_a1995 X165 | bnd_c2_2 bnd_a1995 X165) |
% 7.31/6.80 bnd_c5_2 bnd_a1995 X165)) &
% 7.31/6.80 ~ bnd_c3_1 bnd_a1995) |
% 7.31/6.80 ~ bnd_c7_0)) &
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c8_1 bnd_a1997) &
% 7.31/6.80 ~ bnd_c3_1 bnd_a1997 |
% 7.31/6.80 ~ bnd_c4_0)) &
% 7.31/6.80 ((((((((((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a1998) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1998) &
% 7.31/6.80 bnd_c10_2 bnd_a1998 bnd_a1999) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a1998 bnd_a1999) &
% 7.31/6.80 bnd_c3_2 bnd_a1998 bnd_a1999) &
% 7.31/6.80 bnd_ndr1_1 bnd_a1998) &
% 7.31/6.80 bnd_c6_2 bnd_a1998 bnd_a2000) &
% 7.31/6.80 bnd_c9_2 bnd_a1998 bnd_a2000) &
% 7.31/6.80 bnd_c1_2 bnd_a1998 bnd_a2000 |
% 7.31/6.80 (((((bnd_ndr1_0 & bnd_c2_1 bnd_a2001) &
% 7.31/6.80 bnd_ndr1_1 bnd_a2001) &
% 7.31/6.80 bnd_c9_2 bnd_a2001 bnd_a2002) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a2001 bnd_a2002) &
% 7.31/6.80 bnd_c5_2 bnd_a2001 bnd_a2002) &
% 7.31/6.80 ~ bnd_c3_1 bnd_a2001) |
% 7.31/6.80 ~ bnd_c5_0)) &
% 7.31/6.80 ((((bnd_ndr1_0 &
% 7.31/6.80 (ALL X166.
% 7.31/6.80 bnd_ndr1_1 bnd_a2003 -->
% 7.31/6.80 (bnd_c3_2 bnd_a2003 X166 |
% 7.31/6.80 bnd_c1_2 bnd_a2003 X166) |
% 7.31/6.80 bnd_c9_2 bnd_a2003 X166)) &
% 7.31/6.80 (ALL X167.
% 7.31/6.80 bnd_ndr1_1 bnd_a2003 -->
% 7.31/6.80 (bnd_c9_2 bnd_a2003 X167 |
% 7.31/6.80 bnd_c4_2 bnd_a2003 X167) |
% 7.31/6.80 bnd_c6_2 bnd_a2003 X167)) &
% 7.31/6.80 bnd_c3_1 bnd_a2003 |
% 7.31/6.80 bnd_c2_0) |
% 7.31/6.80 ~ bnd_c8_0)) &
% 7.31/6.80 ((~ bnd_c6_0 | bnd_c1_0) |
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a2004) &
% 7.31/6.80 bnd_c8_2 bnd_a2004 bnd_a2005) &
% 7.31/6.80 ~ bnd_c10_2 bnd_a2004 bnd_a2005) &
% 7.31/6.80 (ALL X168.
% 7.31/6.80 bnd_ndr1_1 bnd_a2004 -->
% 7.31/6.80 ~ bnd_c1_2 bnd_a2004 X168 |
% 7.31/6.80 bnd_c9_2 bnd_a2004 X168)) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a2004)) &
% 7.31/6.80 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a2006) &
% 7.31/6.80 bnd_c4_2 bnd_a2006 bnd_a2007) &
% 7.31/6.80 bnd_c7_2 bnd_a2006 bnd_a2007) &
% 7.31/6.80 ~ bnd_c2_2 bnd_a2006 bnd_a2007) &
% 7.31/6.80 bnd_c4_1 bnd_a2006) &
% 7.31/6.80 (ALL X169.
% 7.31/6.80 bnd_ndr1_1 bnd_a2006 -->
% 7.31/6.80 bnd_c9_2 bnd_a2006 X169 |
% 7.31/6.80 bnd_c7_2 bnd_a2006 X169) |
% 7.31/6.80 (ALL X170.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c9_1 X170 |
% 7.31/6.80 ((bnd_ndr1_1 X170 &
% 7.31/6.80 ~ bnd_c5_2 X170 bnd_a2008) &
% 7.31/6.80 bnd_c3_2 X170 bnd_a2008) &
% 7.31/6.80 ~ bnd_c2_2 X170 bnd_a2008) |
% 7.31/6.80 ((bnd_ndr1_1 X170 &
% 7.31/6.80 bnd_c6_2 X170 bnd_a2009) &
% 7.31/6.80 ~ bnd_c4_2 X170 bnd_a2009) &
% 7.31/6.80 bnd_c7_2 X170 bnd_a2009)) |
% 7.31/6.80 bnd_c4_0)) &
% 7.31/6.80 (bnd_c6_0 | ~ bnd_c10_0)) &
% 7.31/6.80 ((~ bnd_c6_0 |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c7_1 bnd_a2010) &
% 7.31/6.80 (ALL X171.
% 7.31/6.80 bnd_ndr1_1 bnd_a2010 -->
% 7.31/6.80 (bnd_c1_2 bnd_a2010 X171 |
% 7.31/6.80 bnd_c8_2 bnd_a2010 X171) |
% 7.31/6.80 bnd_c10_2 bnd_a2010 X171)) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a2010) |
% 7.31/6.80 bnd_c1_0)) &
% 7.31/6.80 (((ALL X172.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X172 & bnd_c4_2 X172 bnd_a2011) &
% 7.31/6.80 bnd_c9_2 X172 bnd_a2011) &
% 7.31/6.80 bnd_c2_2 X172 bnd_a2011 |
% 7.31/6.80 bnd_c2_1 X172) |
% 7.31/6.80 (ALL X173.
% 7.31/6.80 bnd_ndr1_1 X172 -->
% 7.31/6.80 (bnd_c7_2 X172 X173 |
% 7.31/6.80 ~ bnd_c4_2 X172 X173) |
% 7.31/6.80 bnd_c2_2 X172 X173)) |
% 7.31/6.80 ~ bnd_c6_0) |
% 7.31/6.80 ~ bnd_c1_0)) &
% 7.31/6.80 (((ALL X174.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X175.
% 7.31/6.80 bnd_ndr1_1 X174 -->
% 7.31/6.80 (bnd_c10_2 X174 X175 |
% 7.31/6.80 bnd_c6_2 X174 X175) |
% 7.31/6.80 bnd_c9_2 X174 X175) |
% 7.31/6.80 bnd_c4_1 X174) |
% 7.31/6.80 (ALL X176.
% 7.31/6.80 bnd_ndr1_1 X174 -->
% 7.31/6.80 (~ bnd_c10_2 X174 X176 |
% 7.31/6.80 ~ bnd_c1_2 X174 X176) |
% 7.31/6.80 ~ bnd_c6_2 X174 X176)) |
% 7.31/6.80 (ALL X177.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c8_1 X177 | ~ bnd_c9_1 X177) |
% 7.31/6.80 (ALL X178.
% 7.31/6.80 bnd_ndr1_1 X177 -->
% 7.31/6.80 (~ bnd_c10_2 X177 X178 |
% 7.31/6.80 ~ bnd_c3_2 X177 X178) |
% 7.31/6.80 ~ bnd_c4_2 X177 X178))) |
% 7.31/6.80 ~ bnd_c6_0)) &
% 7.31/6.80 ((~ bnd_c2_0 |
% 7.31/6.80 (ALL X179.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X180.
% 7.31/6.80 bnd_ndr1_1 X179 -->
% 7.31/6.80 bnd_c1_2 X179 X180 | ~ bnd_c6_2 X179 X180) |
% 7.31/6.80 bnd_c5_1 X179) |
% 7.31/6.80 ((bnd_ndr1_1 X179 & bnd_c2_2 X179 bnd_a2012) &
% 7.31/6.80 ~ bnd_c7_2 X179 bnd_a2012) &
% 7.31/6.80 bnd_c8_2 X179 bnd_a2012)) |
% 7.31/6.80 (ALL X181.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X181 & bnd_c7_2 X181 bnd_a2013) &
% 7.31/6.80 ~ bnd_c4_2 X181 bnd_a2013) &
% 7.31/6.80 bnd_c1_2 X181 bnd_a2013 |
% 7.31/6.80 bnd_c10_1 X181) |
% 7.31/6.80 (ALL X182.
% 7.31/6.80 bnd_ndr1_1 X181 -->
% 7.31/6.80 (~ bnd_c8_2 X181 X182 | bnd_c4_2 X181 X182) |
% 7.31/6.80 bnd_c10_2 X181 X182)))) &
% 7.31/6.80 (((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a2014) &
% 7.31/6.80 bnd_c2_1 bnd_a2014) &
% 7.31/6.80 (ALL X183.
% 7.31/6.80 bnd_ndr1_1 bnd_a2014 -->
% 7.31/6.80 (~ bnd_c3_2 bnd_a2014 X183 |
% 7.31/6.80 bnd_c9_2 bnd_a2014 X183) |
% 7.31/6.80 ~ bnd_c4_2 bnd_a2014 X183) |
% 7.31/6.80 (((bnd_ndr1_0 &
% 7.31/6.80 (ALL X184.
% 7.31/6.80 bnd_ndr1_1 bnd_a2015 -->
% 7.31/6.80 bnd_c2_2 bnd_a2015 X184 |
% 7.31/6.80 ~ bnd_c10_2 bnd_a2015 X184)) &
% 7.31/6.80 bnd_ndr1_1 bnd_a2015) &
% 7.31/6.80 ~ bnd_c8_2 bnd_a2015 bnd_a2016) &
% 7.31/6.80 ~ bnd_c9_2 bnd_a2015 bnd_a2016)) &
% 7.31/6.80 ((bnd_c3_0 | bnd_c7_0) | bnd_c2_0)) &
% 7.31/6.80 (bnd_c2_0 |
% 7.31/6.80 ((bnd_ndr1_0 & bnd_c8_1 bnd_a2017) &
% 7.31/6.80 bnd_c3_1 bnd_a2017) &
% 7.31/6.80 (ALL X185.
% 7.31/6.80 bnd_ndr1_1 bnd_a2017 -->
% 7.31/6.80 (bnd_c4_2 bnd_a2017 X185 | bnd_c7_2 bnd_a2017 X185) |
% 7.31/6.80 bnd_c2_2 bnd_a2017 X185))) &
% 7.31/6.80 ((~ bnd_c9_0 | bnd_c2_0) |
% 7.31/6.80 (ALL X186.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X186 & bnd_c6_2 X186 bnd_a2018) &
% 7.31/6.80 ~ bnd_c10_2 X186 bnd_a2018) &
% 7.31/6.80 ~ bnd_c4_2 X186 bnd_a2018 |
% 7.31/6.80 bnd_c8_1 X186) |
% 7.31/6.80 bnd_c10_1 X186))) &
% 7.31/6.80 (~ bnd_c2_0 | ~ bnd_c3_0)) &
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c4_1 bnd_a2019) &
% 7.31/6.80 (ALL X187.
% 7.31/6.80 bnd_ndr1_1 bnd_a2019 -->
% 7.31/6.80 (bnd_c2_2 bnd_a2019 X187 |
% 7.31/6.80 ~ bnd_c6_2 bnd_a2019 X187) |
% 7.31/6.80 ~ bnd_c3_2 bnd_a2019 X187)) &
% 7.31/6.80 bnd_c3_1 bnd_a2019 |
% 7.31/6.80 (ALL X188.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c6_1 X188 |
% 7.31/6.80 (bnd_ndr1_1 X188 & ~ bnd_c9_2 X188 bnd_a2020) &
% 7.31/6.80 bnd_c5_2 X188 bnd_a2020) |
% 7.31/6.80 (ALL X189.
% 7.31/6.80 bnd_ndr1_1 X188 -->
% 7.31/6.80 (~ bnd_c3_2 X188 X189 | bnd_c2_2 X188 X189) |
% 7.31/6.80 bnd_c1_2 X188 X189))) |
% 7.31/6.80 (ALL X190.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c3_1 X190 | ~ bnd_c10_1 X190) |
% 7.31/6.80 ~ bnd_c9_1 X190))) &
% 7.31/6.80 ((bnd_c4_0 | ~ bnd_c6_0) |
% 7.31/6.80 (ALL X191.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((ALL X192.
% 7.31/6.80 bnd_ndr1_1 X191 -->
% 7.31/6.80 (bnd_c8_2 X191 X192 | ~ bnd_c10_2 X191 X192) |
% 7.31/6.80 ~ bnd_c4_2 X191 X192) |
% 7.31/6.80 bnd_c8_1 X191) |
% 7.31/6.80 ~ bnd_c3_1 X191))) &
% 7.31/6.80 (((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a2021) & ~ bnd_c8_1 bnd_a2021) &
% 7.31/6.80 ~ bnd_c1_1 bnd_a2021 |
% 7.31/6.80 ~ bnd_c3_0)) &
% 7.31/6.80 ((~ bnd_c10_0 |
% 7.31/6.80 (bnd_ndr1_0 & bnd_c3_1 bnd_a2022) & ~ bnd_c7_1 bnd_a2022) |
% 7.31/6.80 bnd_c8_0)) &
% 7.31/6.80 (((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a2023) & ~ bnd_c10_1 bnd_a2023) &
% 7.31/6.80 (ALL X193.
% 7.31/6.80 bnd_ndr1_1 bnd_a2023 -->
% 7.31/6.80 (bnd_c6_2 bnd_a2023 X193 | ~ bnd_c2_2 bnd_a2023 X193) |
% 7.31/6.80 ~ bnd_c5_2 bnd_a2023 X193) |
% 7.31/6.80 ~ bnd_c1_0)) &
% 7.31/6.80 (~ bnd_c9_0 |
% 7.31/6.80 (ALL X194.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c7_1 X194 |
% 7.31/6.80 (ALL X195.
% 7.31/6.80 bnd_ndr1_1 X194 -->
% 7.31/6.80 (bnd_c5_2 X194 X195 | bnd_c3_2 X194 X195) |
% 7.31/6.80 bnd_c4_2 X194 X195)) |
% 7.31/6.80 ~ bnd_c5_1 X194))) &
% 7.31/6.80 (bnd_c7_0 | bnd_c9_0)) &
% 7.31/6.80 (bnd_c3_0 | ~ bnd_c1_0)) &
% 7.31/6.80 (((ALL X196.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c4_1 X196 |
% 7.31/6.80 (ALL X197.
% 7.31/6.80 bnd_ndr1_1 X196 -->
% 7.31/6.80 (bnd_c7_2 X196 X197 | ~ bnd_c10_2 X196 X197) |
% 7.31/6.80 bnd_c4_2 X196 X197)) |
% 7.31/6.80 ((bnd_ndr1_1 X196 & bnd_c3_2 X196 bnd_a2024) &
% 7.31/6.80 bnd_c10_2 X196 bnd_a2024) &
% 7.31/6.80 ~ bnd_c6_2 X196 bnd_a2024) |
% 7.31/6.80 ~ bnd_c7_0) |
% 7.31/6.80 (ALL X198.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (bnd_c10_1 X198 |
% 7.31/6.80 (ALL X199.
% 7.31/6.80 bnd_ndr1_1 X198 -->
% 7.31/6.80 (~ bnd_c8_2 X198 X199 | bnd_c2_2 X198 X199) |
% 7.31/6.80 bnd_c3_2 X198 X199)) |
% 7.31/6.80 ((bnd_ndr1_1 X198 & ~ bnd_c5_2 X198 bnd_a2025) &
% 7.31/6.80 ~ bnd_c6_2 X198 bnd_a2025) &
% 7.31/6.80 bnd_c3_2 X198 bnd_a2025))) &
% 7.31/6.80 (((ALL X200.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (~ bnd_c5_1 X200 | bnd_c4_1 X200) |
% 7.31/6.80 ((bnd_ndr1_1 X200 & ~ bnd_c10_2 X200 bnd_a2026) &
% 7.31/6.80 bnd_c4_2 X200 bnd_a2026) &
% 7.31/6.80 bnd_c3_2 X200 bnd_a2026) |
% 7.31/6.80 ~ bnd_c7_0) |
% 7.31/6.80 bnd_c6_0)) &
% 7.31/6.80 ((((bnd_ndr1_0 & bnd_c3_1 bnd_a2027) & ~ bnd_c4_1 bnd_a2027) &
% 7.31/6.80 ~ bnd_c6_1 bnd_a2027 |
% 7.31/6.80 bnd_c8_0) |
% 7.31/6.80 (ALL X201.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 (((bnd_ndr1_1 X201 & bnd_c2_2 X201 bnd_a2028) &
% 7.31/6.80 ~ bnd_c8_2 X201 bnd_a2028) &
% 7.31/6.80 bnd_c4_2 X201 bnd_a2028 |
% 7.31/6.80 bnd_c2_1 X201) |
% 7.31/6.80 ~ bnd_c6_1 X201))) &
% 7.31/6.80 (((bnd_ndr1_0 & bnd_c10_1 bnd_a2029) &
% 7.31/6.80 (ALL X202.
% 7.31/6.80 bnd_ndr1_1 bnd_a2029 -->
% 7.31/6.80 (~ bnd_c3_2 bnd_a2029 X202 | bnd_c4_2 bnd_a2029 X202) |
% 7.31/6.80 ~ bnd_c8_2 bnd_a2029 X202)) &
% 7.31/6.80 (ALL X203.
% 7.31/6.80 bnd_ndr1_1 bnd_a2029 -->
% 7.31/6.80 (~ bnd_c9_2 bnd_a2029 X203 | ~ bnd_c4_2 bnd_a2029 X203) |
% 7.31/6.80 ~ bnd_c7_2 bnd_a2029 X203) |
% 7.31/6.80 bnd_c4_0)) &
% 7.31/6.80 ((bnd_c3_0 |
% 7.31/6.80 (bnd_ndr1_0 & ~ bnd_c7_1 bnd_a2030) & ~ bnd_c6_1 bnd_a2030) |
% 7.31/6.80 (ALL X204.
% 7.31/6.80 bnd_ndr1_0 -->
% 7.31/6.80 ((bnd_ndr1_1 X204 & bnd_c8_2 X204 bnd_a2031) &
% 7.31/6.80 ~ bnd_c5_2 X204 bnd_a2031 |
% 7.31/6.80 ((bnd_ndr1_1 X204 & bnd_c2_2 X204 bnd_a2032) &
% 7.31/6.80 bnd_c7_2 X204 bnd_a2032) &
% 7.31/6.80 ~ bnd_c1_2 X204 bnd_a2032) |
% 7.31/6.80 bnd_c1_1 X204)))
% 18.32/17.82 Unfolded term: ~ ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((ALL U.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 U & ~ bnd_c9_2 U bnd_a1834) &
% 18.32/17.82 ~ bnd_c3_2 U bnd_a1834) &
% 18.32/17.82 bnd_c7_2 U bnd_a1834 |
% 18.32/17.82 (bnd_ndr1_1 U & bnd_c3_2 U bnd_a1835) &
% 18.32/17.82 bnd_c5_2 U bnd_a1835) |
% 18.32/17.82 ((bnd_ndr1_1 U & bnd_c1_2 U bnd_a1836) &
% 18.32/17.82 ~ bnd_c4_2 U bnd_a1836) &
% 18.32/17.82 bnd_c6_2 U bnd_a1836) |
% 18.32/17.82 bnd_c4_0) |
% 18.32/17.82 ~ bnd_c6_0) &
% 18.32/17.82 (((ALL V.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (ALL W.
% 18.32/17.82 bnd_ndr1_1 V -->
% 18.32/17.82 (~ bnd_c5_2 V W | bnd_c7_2 V W) | bnd_c3_2 V W) |
% 18.32/17.82 bnd_c6_1 V) |
% 18.32/17.82 bnd_c7_0) |
% 18.32/17.82 bnd_c8_0)) &
% 18.32/17.82 (((ALL X.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c4_1 X |
% 18.32/17.82 ((bnd_ndr1_1 X & bnd_c7_2 X bnd_a1837) &
% 18.32/17.82 bnd_c6_2 X bnd_a1837) &
% 18.32/17.82 ~ bnd_c3_2 X bnd_a1837) |
% 18.32/17.82 ((bnd_ndr1_1 X & ~ bnd_c1_2 X bnd_a1838) &
% 18.32/17.82 bnd_c10_2 X bnd_a1838) &
% 18.32/17.82 bnd_c6_2 X bnd_a1838) |
% 18.32/17.82 ~ bnd_c7_0) |
% 18.32/17.82 (ALL Y.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL Z.
% 18.32/17.82 bnd_ndr1_1 Y --> ~ bnd_c1_2 Y Z | ~ bnd_c7_2 Y Z) |
% 18.32/17.82 ~ bnd_c6_1 Y) |
% 18.32/17.82 ~ bnd_c10_1 Y))) &
% 18.32/17.82 ((bnd_c8_0 |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1839) &
% 18.32/17.82 bnd_c8_2 bnd_a1839 bnd_a1840) &
% 18.32/17.82 bnd_c2_2 bnd_a1839 bnd_a1840) &
% 18.32/17.82 bnd_c3_2 bnd_a1839 bnd_a1840) &
% 18.32/17.82 bnd_c2_1 bnd_a1839) &
% 18.32/17.82 ~ bnd_c10_1 bnd_a1839) |
% 18.32/17.82 (((bnd_ndr1_0 &
% 18.32/17.82 (ALL X1.
% 18.32/17.82 bnd_ndr1_1 bnd_a1841 -->
% 18.32/17.82 ~ bnd_c2_2 bnd_a1841 X1 | ~ bnd_c7_2 bnd_a1841 X1)) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1841) &
% 18.32/17.82 bnd_c4_2 bnd_a1841 bnd_a1842) &
% 18.32/17.82 bnd_c2_2 bnd_a1841 bnd_a1842)) &
% 18.32/17.82 ((~ bnd_c8_0 |
% 18.32/17.82 (ALL X2.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X2 & bnd_c9_2 X2 bnd_a1843) &
% 18.32/17.82 bnd_c7_2 X2 bnd_a1843) &
% 18.32/17.82 ~ bnd_c3_2 X2 bnd_a1843 |
% 18.32/17.82 ((bnd_ndr1_1 X2 & bnd_c7_2 X2 bnd_a1844) &
% 18.32/17.82 bnd_c10_2 X2 bnd_a1844) &
% 18.32/17.82 bnd_c6_2 X2 bnd_a1844) |
% 18.32/17.82 (ALL X3.
% 18.32/17.82 bnd_ndr1_1 X2 -->
% 18.32/17.82 (bnd_c5_2 X2 X3 | ~ bnd_c6_2 X2 X3) |
% 18.32/17.82 ~ bnd_c4_2 X2 X3))) |
% 18.32/17.82 (ALL X4.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c9_1 X4 | ~ bnd_c3_1 X4) |
% 18.32/17.82 (ALL X5.
% 18.32/17.82 bnd_ndr1_1 X4 -->
% 18.32/17.82 (~ bnd_c4_2 X4 X5 | bnd_c2_2 X4 X5) |
% 18.32/17.82 ~ bnd_c1_2 X4 X5)))) &
% 18.32/17.82 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a1845) & ~ bnd_c10_1 bnd_a1845) &
% 18.32/17.82 (ALL X6.
% 18.32/17.82 bnd_ndr1_1 bnd_a1845 -->
% 18.32/17.82 (~ bnd_c4_2 bnd_a1845 X6 | bnd_c5_2 bnd_a1845 X6) |
% 18.32/17.82 ~ bnd_c7_2 bnd_a1845 X6) |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_c9_1 bnd_a1846) & bnd_ndr1_1 bnd_a1846) &
% 18.32/17.82 bnd_c5_2 bnd_a1846 bnd_a1847) &
% 18.32/17.82 bnd_c8_2 bnd_a1846 bnd_a1847) &
% 18.32/17.82 bnd_c7_2 bnd_a1846 bnd_a1847) &
% 18.32/17.82 (ALL X7.
% 18.32/17.82 bnd_ndr1_1 bnd_a1846 -->
% 18.32/17.82 bnd_c6_2 bnd_a1846 X7 | bnd_c5_2 bnd_a1846 X7)) |
% 18.32/17.82 ~ bnd_c7_0)) &
% 18.32/17.82 (~ bnd_c5_0 |
% 18.32/17.82 (ALL X8. bnd_ndr1_0 --> bnd_c5_1 X8 | bnd_c3_1 X8))) &
% 18.32/17.82 ((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X9.
% 18.32/17.82 bnd_ndr1_1 bnd_a1848 -->
% 18.32/17.82 (bnd_c3_2 bnd_a1848 X9 | bnd_c1_2 bnd_a1848 X9) |
% 18.32/17.82 ~ bnd_c5_2 bnd_a1848 X9)) &
% 18.32/17.82 (ALL X10.
% 18.32/17.82 bnd_ndr1_1 bnd_a1848 -->
% 18.32/17.82 ~ bnd_c2_2 bnd_a1848 X10 | bnd_c6_2 bnd_a1848 X10)) &
% 18.32/17.82 ~ bnd_c2_1 bnd_a1848 |
% 18.32/17.82 bnd_c9_0) |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_c6_1 bnd_a1849) & bnd_ndr1_1 bnd_a1849) &
% 18.32/17.82 bnd_c5_2 bnd_a1849 bnd_a1850) &
% 18.32/17.82 bnd_c7_2 bnd_a1849 bnd_a1850) &
% 18.32/17.82 ~ bnd_c3_2 bnd_a1849 bnd_a1850) &
% 18.32/17.82 ~ bnd_c3_1 bnd_a1849)) &
% 18.32/17.82 ((~ bnd_c7_0 | bnd_c4_0) |
% 18.32/17.82 (((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X11.
% 18.32/17.82 bnd_ndr1_1 bnd_a1851 -->
% 18.32/17.82 ~ bnd_c4_2 bnd_a1851 X11 | ~ bnd_c7_2 bnd_a1851 X11)) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1851) &
% 18.32/17.82 ~ bnd_c4_2 bnd_a1851 bnd_a1852) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1851 bnd_a1852) &
% 18.32/17.82 bnd_c3_2 bnd_a1851 bnd_a1852) &
% 18.32/17.82 (ALL X12.
% 18.32/17.82 bnd_ndr1_1 bnd_a1851 -->
% 18.32/17.82 (bnd_c4_2 bnd_a1851 X12 | bnd_c5_2 bnd_a1851 X12) |
% 18.32/17.82 ~ bnd_c8_2 bnd_a1851 X12))) &
% 18.32/17.82 ((~ bnd_c6_0 | bnd_c10_0) | ~ bnd_c7_0)) &
% 18.32/17.82 (~ bnd_c4_0 | ~ bnd_c8_0)) &
% 18.32/17.82 ((bnd_c1_0 |
% 18.32/17.82 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1853) &
% 18.32/17.82 (ALL X13.
% 18.32/17.82 bnd_ndr1_1 bnd_a1853 -->
% 18.32/17.82 (bnd_c10_2 bnd_a1853 X13 | bnd_c3_2 bnd_a1853 X13) |
% 18.32/17.82 bnd_c6_2 bnd_a1853 X13)) &
% 18.32/17.82 bnd_c1_1 bnd_a1853) |
% 18.32/17.82 bnd_c5_0)) &
% 18.32/17.82 ((~ bnd_c4_0 | bnd_c5_0) | ~ bnd_c3_0)) &
% 18.32/17.82 ((~ bnd_c6_0 |
% 18.32/17.82 ((bnd_ndr1_0 & bnd_c7_1 bnd_a1854) & bnd_c6_1 bnd_a1854) &
% 18.32/17.82 bnd_c3_1 bnd_a1854) |
% 18.32/17.82 (ALL X14.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X14 & bnd_c10_2 X14 bnd_a1855) &
% 18.32/17.82 bnd_c1_2 X14 bnd_a1855) &
% 18.32/17.82 bnd_c6_2 X14 bnd_a1855 |
% 18.32/17.82 ((bnd_ndr1_1 X14 & ~ bnd_c5_2 X14 bnd_a1856) &
% 18.32/17.82 bnd_c1_2 X14 bnd_a1856) &
% 18.32/17.82 bnd_c10_2 X14 bnd_a1856) |
% 18.32/17.82 bnd_c10_1 X14))) &
% 18.32/17.82 ((~ bnd_c9_0 | ~ bnd_c3_0) | ~ bnd_c4_0)) &
% 18.32/17.82 ((~ bnd_c4_0 | ~ bnd_c1_0) |
% 18.32/17.82 (bnd_ndr1_0 & ~ bnd_c4_1 bnd_a1857) &
% 18.32/17.82 (ALL X15.
% 18.32/17.82 bnd_ndr1_1 bnd_a1857 -->
% 18.32/17.82 ~ bnd_c5_2 bnd_a1857 X15 | bnd_c8_2 bnd_a1857 X15))) &
% 18.32/17.82 ((bnd_c2_0 | ~ bnd_c7_0) | ~ bnd_c10_0)) &
% 18.32/17.82 ((~ bnd_c7_0 |
% 18.32/17.82 (ALL X16.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c7_1 X16 | bnd_c8_1 X16) |
% 18.32/17.82 (ALL X17.
% 18.32/17.82 bnd_ndr1_1 X16 -->
% 18.32/17.82 (bnd_c9_2 X16 X17 | ~ bnd_c7_2 X16 X17) | bnd_c3_2 X16 X17))) |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_c8_1 bnd_a1858) & bnd_ndr1_1 bnd_a1858) &
% 18.32/17.82 bnd_c4_2 bnd_a1858 bnd_a1859) &
% 18.32/17.82 ~ bnd_c6_2 bnd_a1858 bnd_a1859) &
% 18.32/17.82 ~ bnd_c10_2 bnd_a1858 bnd_a1859) &
% 18.32/17.82 ~ bnd_c10_1 bnd_a1858)) &
% 18.32/17.82 ((~ bnd_c6_0 |
% 18.32/17.82 ((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1860) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1860 bnd_a1861) &
% 18.32/17.82 ~ bnd_c9_2 bnd_a1860 bnd_a1861) &
% 18.32/17.82 bnd_c5_2 bnd_a1860 bnd_a1861) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1860) &
% 18.32/17.82 bnd_c1_2 bnd_a1860 bnd_a1862) &
% 18.32/17.82 bnd_c3_2 bnd_a1860 bnd_a1862) &
% 18.32/17.82 bnd_c5_2 bnd_a1860 bnd_a1862) &
% 18.32/17.82 (ALL X18.
% 18.32/17.82 bnd_ndr1_1 bnd_a1860 -->
% 18.32/17.82 (bnd_c8_2 bnd_a1860 X18 | ~ bnd_c3_2 bnd_a1860 X18) |
% 18.32/17.82 bnd_c5_2 bnd_a1860 X18)) |
% 18.32/17.82 ~ bnd_c2_0)) &
% 18.32/17.82 ((ALL X19.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X19 & bnd_c8_2 X19 bnd_a1863) & ~ bnd_c3_2 X19 bnd_a1863) &
% 18.32/17.82 ~ bnd_c1_2 X19 bnd_a1863 |
% 18.32/17.82 ~ bnd_c8_1 X19) |
% 18.32/17.82 ((bnd_ndr1_1 X19 & ~ bnd_c1_2 X19 bnd_a1864) & bnd_c8_2 X19 bnd_a1864) &
% 18.32/17.82 bnd_c7_2 X19 bnd_a1864) |
% 18.32/17.82 (((((((((((bnd_ndr1_0 &
% 18.32/17.82 bnd_ndr1_1 bnd_a1865) &
% 18.32/17.82 ~ bnd_c7_2 bnd_a1865 bnd_a1866) &
% 18.32/17.82 bnd_c8_2 bnd_a1865 bnd_a1866) &
% 18.32/17.82 ~ bnd_c4_2 bnd_a1865 bnd_a1866) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1865) &
% 18.32/17.82 bnd_c3_2 bnd_a1865 bnd_a1867) &
% 18.32/17.82 ~ bnd_c9_2 bnd_a1865 bnd_a1867) &
% 18.32/17.82 ~ bnd_c5_2 bnd_a1865 bnd_a1867) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1865) &
% 18.32/17.82 bnd_c2_2 bnd_a1865 bnd_a1868) &
% 18.32/17.82 ~ bnd_c7_2 bnd_a1865 bnd_a1868) &
% 18.32/17.82 ~ bnd_c6_2 bnd_a1865 bnd_a1868)) &
% 18.32/17.82 ((~ bnd_c1_0 | bnd_c7_0) | bnd_c8_0)) &
% 18.32/17.82 ((~ bnd_c7_0 |
% 18.32/17.82 (ALL X20.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c10_1 X20 | bnd_c4_1 X20) |
% 18.32/17.82 (ALL X21.
% 18.32/17.82 bnd_ndr1_1 X20 -->
% 18.32/17.82 (bnd_c1_2 X20 X21 | bnd_c10_2 X20 X21) | bnd_c4_2 X20 X21))) |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1869) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1869 bnd_a1870) &
% 18.32/17.82 ~ bnd_c9_2 bnd_a1869 bnd_a1870) &
% 18.32/17.82 ~ bnd_c10_2 bnd_a1869 bnd_a1870) &
% 18.32/17.82 bnd_c4_1 bnd_a1869) &
% 18.32/17.82 bnd_c9_1 bnd_a1869)) &
% 18.32/17.82 (((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X22.
% 18.32/17.82 bnd_ndr1_1 bnd_a1871 -->
% 18.32/17.82 (bnd_c8_2 bnd_a1871 X22 | bnd_c3_2 bnd_a1871 X22) |
% 18.32/17.82 bnd_c9_2 bnd_a1871 X22)) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1871) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1871 bnd_a1872) &
% 18.32/17.82 ~ bnd_c5_2 bnd_a1871 bnd_a1872 |
% 18.32/17.82 (ALL X23.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c10_1 X23 | bnd_c4_1 X23) |
% 18.32/17.82 ((bnd_ndr1_1 X23 & ~ bnd_c4_2 X23 bnd_a1873) & bnd_c3_2 X23 bnd_a1873) &
% 18.32/17.82 ~ bnd_c10_2 X23 bnd_a1873)) |
% 18.32/17.82 (ALL X24.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X24 &
% 18.32/17.82 ~ bnd_c2_2 X24 bnd_a1874) &
% 18.32/17.82 bnd_c10_2 X24 bnd_a1874) &
% 18.32/17.82 bnd_c1_2 X24 bnd_a1874 |
% 18.32/17.82 bnd_c6_1 X24) |
% 18.32/17.82 bnd_c2_1 X24))) &
% 18.32/17.82 ((((bnd_ndr1_0 & ~ bnd_c10_1 bnd_a1875) &
% 18.32/17.82 (ALL X25.
% 18.32/17.82 bnd_ndr1_1 bnd_a1875 -->
% 18.32/17.82 (~ bnd_c4_2 bnd_a1875 X25 | ~ bnd_c10_2 bnd_a1875 X25) |
% 18.32/17.82 ~ bnd_c8_2 bnd_a1875 X25)) &
% 18.32/17.82 bnd_c6_1 bnd_a1875 |
% 18.32/17.82 bnd_c1_0) |
% 18.32/17.82 (bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1876) &
% 18.32/17.82 ~ bnd_c5_1 bnd_a1876)) &
% 18.32/17.82 (((ALL X26.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (ALL X27.
% 18.32/17.82 bnd_ndr1_1 X26 -->
% 18.32/17.82 (bnd_c6_2 X26 X27 | bnd_c3_2 X26 X27) | ~ bnd_c2_2 X26 X27) |
% 18.32/17.82 ~ bnd_c8_1 X26) |
% 18.32/17.82 ~ bnd_c6_0) |
% 18.32/17.82 bnd_c10_0)) &
% 18.32/17.82 (((ALL X28.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c3_1 X28 | bnd_c2_1 X28) |
% 18.32/17.82 (ALL X29.
% 18.32/17.82 bnd_ndr1_1 X28 --> bnd_c8_2 X28 X29 | bnd_c2_2 X28 X29)) |
% 18.32/17.82 bnd_c9_0) |
% 18.32/17.82 bnd_c3_0)) &
% 18.32/17.82 ((~ bnd_c7_0 |
% 18.32/17.82 ((((bnd_ndr1_0 & bnd_c10_1 bnd_a1877) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1877) &
% 18.32/17.82 ~ bnd_c1_2 bnd_a1877 bnd_a1878) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1877 bnd_a1878) &
% 18.32/17.82 bnd_c10_2 bnd_a1877 bnd_a1878) |
% 18.32/17.82 bnd_c9_0)) &
% 18.32/17.82 ((~ bnd_c4_0 |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1879) &
% 18.32/17.82 bnd_c6_2 bnd_a1879 bnd_a1880) &
% 18.32/17.82 ~ bnd_c3_2 bnd_a1879 bnd_a1880) &
% 18.32/17.82 bnd_c5_2 bnd_a1879 bnd_a1880) &
% 18.32/17.82 (ALL X30.
% 18.32/17.82 bnd_ndr1_1 bnd_a1879 -->
% 18.32/17.82 bnd_c2_2 bnd_a1879 X30 |
% 18.32/17.82 ~ bnd_c6_2 bnd_a1879 X30)) &
% 18.32/17.82 bnd_c2_1 bnd_a1879) |
% 18.32/17.82 (((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1881) &
% 18.32/17.82 ~ bnd_c3_1 bnd_a1881) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1881) &
% 18.32/17.82 ~ bnd_c8_2 bnd_a1881 bnd_a1882) &
% 18.32/17.82 bnd_c1_2 bnd_a1881 bnd_a1882) &
% 18.32/17.82 ~ bnd_c4_2 bnd_a1881 bnd_a1882)) &
% 18.32/17.82 ((~ bnd_c5_0 | ~ bnd_c4_0) |
% 18.32/17.82 (ALL X31.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c4_1 X31 | bnd_c1_1 X31) |
% 18.32/17.82 ((bnd_ndr1_1 X31 & bnd_c9_2 X31 bnd_a1883) &
% 18.32/17.82 bnd_c4_2 X31 bnd_a1883) &
% 18.32/17.82 bnd_c6_2 X31 bnd_a1883))) &
% 18.32/17.82 ((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X32.
% 18.32/17.82 bnd_ndr1_1 bnd_a1884 -->
% 18.32/17.82 (bnd_c9_2 bnd_a1884 X32 |
% 18.32/17.82 ~ bnd_c1_2 bnd_a1884 X32) |
% 18.32/17.82 bnd_c7_2 bnd_a1884 X32)) &
% 18.32/17.82 ~ bnd_c7_1 bnd_a1884) &
% 18.32/17.82 bnd_c10_1 bnd_a1884 |
% 18.32/17.82 ((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1885) &
% 18.32/17.82 (ALL X33.
% 18.32/17.82 bnd_ndr1_1 bnd_a1885 -->
% 18.32/17.82 (bnd_c8_2 bnd_a1885 X33 |
% 18.32/17.82 ~ bnd_c2_2 bnd_a1885 X33) |
% 18.32/17.82 ~ bnd_c3_2 bnd_a1885 X33)) &
% 18.32/17.82 ~ bnd_c8_1 bnd_a1885) |
% 18.32/17.82 ~ bnd_c1_0)) &
% 18.32/17.82 (bnd_c5_0 | bnd_c9_0)) &
% 18.32/17.82 (((((((bnd_ndr1_0 & bnd_c7_1 bnd_a1886) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1886) &
% 18.32/17.82 bnd_c4_2 bnd_a1886 bnd_a1887) &
% 18.32/17.82 ~ bnd_c1_2 bnd_a1886 bnd_a1887) &
% 18.32/17.82 bnd_c5_2 bnd_a1886 bnd_a1887) &
% 18.32/17.82 ~ bnd_c9_1 bnd_a1886 |
% 18.32/17.82 ~ bnd_c4_0) |
% 18.32/17.82 ~ bnd_c10_0)) &
% 18.32/17.82 ((~ bnd_c8_0 | ~ bnd_c4_0) | ~ bnd_c10_0)) &
% 18.32/17.82 (((ALL X34.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X34 & ~ bnd_c6_2 X34 bnd_a1888) &
% 18.32/17.82 ~ bnd_c5_2 X34 bnd_a1888) &
% 18.32/17.82 ~ bnd_c7_2 X34 bnd_a1888 |
% 18.32/17.82 ((bnd_ndr1_1 X34 & ~ bnd_c7_2 X34 bnd_a1889) &
% 18.32/17.82 bnd_c6_2 X34 bnd_a1889) &
% 18.32/17.82 ~ bnd_c1_2 X34 bnd_a1889) |
% 18.32/17.82 ~ bnd_c6_1 X34) |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1890) &
% 18.32/17.82 bnd_c5_2 bnd_a1890 bnd_a1891) &
% 18.32/17.82 ~ bnd_c3_2 bnd_a1890 bnd_a1891) &
% 18.32/17.82 ~ bnd_c10_2 bnd_a1890 bnd_a1891) &
% 18.32/17.82 ~ bnd_c6_1 bnd_a1890) &
% 18.32/17.82 ~ bnd_c1_1 bnd_a1890) |
% 18.32/17.82 ~ bnd_c1_0)) &
% 18.32/17.82 (((((((bnd_ndr1_0 & bnd_c4_1 bnd_a1892) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1892) &
% 18.32/17.82 bnd_c3_2 bnd_a1892 bnd_a1893) &
% 18.32/17.82 bnd_c1_2 bnd_a1892 bnd_a1893) &
% 18.32/17.82 bnd_c6_2 bnd_a1892 bnd_a1893) &
% 18.32/17.82 ~ bnd_c8_1 bnd_a1892 |
% 18.32/17.82 ((bnd_ndr1_0 &
% 18.32/17.82 (ALL X35.
% 18.32/17.82 bnd_ndr1_1 bnd_a1894 -->
% 18.32/17.82 ~ bnd_c9_2 bnd_a1894 X35 |
% 18.32/17.82 bnd_c4_2 bnd_a1894 X35)) &
% 18.32/17.82 (ALL X36.
% 18.32/17.82 bnd_ndr1_1 bnd_a1894 -->
% 18.32/17.82 (~ bnd_c6_2 bnd_a1894 X36 |
% 18.32/17.82 ~ bnd_c2_2 bnd_a1894 X36) |
% 18.32/17.82 ~ bnd_c4_2 bnd_a1894 X36)) &
% 18.32/17.82 ~ bnd_c9_1 bnd_a1894) |
% 18.32/17.82 ~ bnd_c6_0)) &
% 18.32/17.82 (((ALL X37.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X38.
% 18.32/17.82 bnd_ndr1_1 X37 -->
% 18.32/17.82 (bnd_c1_2 X37 X38 | bnd_c7_2 X37 X38) |
% 18.32/17.82 ~ bnd_c3_2 X37 X38) |
% 18.32/17.82 bnd_c9_1 X37) |
% 18.32/17.82 (ALL X39.
% 18.32/17.82 bnd_ndr1_1 X37 -->
% 18.32/17.82 bnd_c8_2 X37 X39 | bnd_c10_2 X37 X39)) |
% 18.32/17.82 ~ bnd_c10_0) |
% 18.32/17.82 ((bnd_ndr1_0 & bnd_c10_1 bnd_a1895) &
% 18.32/17.82 (ALL X40.
% 18.32/17.82 bnd_ndr1_1 bnd_a1895 -->
% 18.32/17.82 (bnd_c4_2 bnd_a1895 X40 |
% 18.32/17.82 ~ bnd_c10_2 bnd_a1895 X40) |
% 18.32/17.82 bnd_c3_2 bnd_a1895 X40)) &
% 18.32/17.82 bnd_c5_1 bnd_a1895)) &
% 18.32/17.82 (((ALL X41.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X42.
% 18.32/17.82 bnd_ndr1_1 X41 -->
% 18.32/17.82 (bnd_c5_2 X41 X42 | bnd_c10_2 X41 X42) |
% 18.32/17.82 ~ bnd_c9_2 X41 X42) |
% 18.32/17.82 bnd_c10_1 X41) |
% 18.32/17.82 (ALL X43.
% 18.32/17.82 bnd_ndr1_1 X41 -->
% 18.32/17.82 (bnd_c4_2 X41 X43 | bnd_c10_2 X41 X43) |
% 18.32/17.82 ~ bnd_c9_2 X41 X43)) |
% 18.32/17.82 (ALL X44.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c9_1 X44 | bnd_c1_1 X44) |
% 18.32/17.82 (ALL X45.
% 18.32/17.82 bnd_ndr1_1 X44 -->
% 18.32/17.82 bnd_c8_2 X44 X45 | bnd_c2_2 X44 X45))) |
% 18.32/17.82 ((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1896) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1896) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1896 bnd_a1897) &
% 18.32/17.82 bnd_c7_2 bnd_a1896 bnd_a1897) &
% 18.32/17.82 bnd_c6_2 bnd_a1896 bnd_a1897)) &
% 18.32/17.82 ((ALL X46.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X46 & ~ bnd_c1_2 X46 bnd_a1898) &
% 18.32/17.82 ~ bnd_c6_2 X46 bnd_a1898) &
% 18.32/17.82 bnd_c2_2 X46 bnd_a1898 |
% 18.32/17.82 bnd_c2_1 X46) |
% 18.32/17.82 (ALL X47.
% 18.32/17.82 bnd_ndr1_1 X46 -->
% 18.32/17.82 (bnd_c8_2 X46 X47 | bnd_c5_2 X46 X47) |
% 18.32/17.82 ~ bnd_c9_2 X46 X47)) |
% 18.32/17.82 ((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1899) &
% 18.32/17.82 ~ bnd_c1_1 bnd_a1899) &
% 18.32/17.82 (ALL X48.
% 18.32/17.82 bnd_ndr1_1 bnd_a1899 -->
% 18.32/17.82 (bnd_c1_2 bnd_a1899 X48 | ~ bnd_c9_2 bnd_a1899 X48) |
% 18.32/17.82 bnd_c2_2 bnd_a1899 X48))) &
% 18.32/17.82 (~ bnd_c4_0 | ~ bnd_c9_0)) &
% 18.32/17.82 ((((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1900) &
% 18.32/17.82 ~ bnd_c4_2 bnd_a1900 bnd_a1901) &
% 18.32/17.82 ~ bnd_c10_2 bnd_a1900 bnd_a1901) &
% 18.32/17.82 ~ bnd_c2_2 bnd_a1900 bnd_a1901) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1900) &
% 18.32/17.82 ~ bnd_c10_2 bnd_a1900 bnd_a1902) &
% 18.32/17.82 bnd_c9_2 bnd_a1900 bnd_a1902) &
% 18.32/17.82 bnd_c2_2 bnd_a1900 bnd_a1902) &
% 18.32/17.82 ~ bnd_c6_1 bnd_a1900 |
% 18.32/17.82 bnd_c3_0) |
% 18.32/17.82 bnd_c10_0)) &
% 18.32/17.82 ((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X49.
% 18.32/17.82 bnd_ndr1_1 bnd_a1903 -->
% 18.32/17.82 (bnd_c7_2 bnd_a1903 X49 | ~ bnd_c9_2 bnd_a1903 X49) |
% 18.32/17.82 ~ bnd_c8_2 bnd_a1903 X49)) &
% 18.32/17.82 bnd_c3_1 bnd_a1903) &
% 18.32/17.82 (ALL X50.
% 18.32/17.82 bnd_ndr1_1 bnd_a1903 -->
% 18.32/17.82 (~ bnd_c4_2 bnd_a1903 X50 | bnd_c7_2 bnd_a1903 X50) |
% 18.32/17.82 bnd_c5_2 bnd_a1903 X50) |
% 18.32/17.82 (ALL X51.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X51 & ~ bnd_c8_2 X51 bnd_a1904) &
% 18.32/17.82 ~ bnd_c7_2 X51 bnd_a1904) &
% 18.32/17.82 bnd_c10_2 X51 bnd_a1904 |
% 18.32/17.82 bnd_c6_1 X51) |
% 18.32/17.82 ((bnd_ndr1_1 X51 & ~ bnd_c4_2 X51 bnd_a1905) &
% 18.32/17.82 bnd_c5_2 X51 bnd_a1905) &
% 18.32/17.82 ~ bnd_c10_2 X51 bnd_a1905)) |
% 18.32/17.82 ((bnd_ndr1_0 &
% 18.32/17.82 (ALL X52.
% 18.32/17.82 bnd_ndr1_1 bnd_a1906 -->
% 18.32/17.82 (~ bnd_c3_2 bnd_a1906 X52 | ~ bnd_c2_2 bnd_a1906 X52) |
% 18.32/17.82 ~ bnd_c1_2 bnd_a1906 X52)) &
% 18.32/17.82 bnd_c4_1 bnd_a1906) &
% 18.32/17.82 (ALL X53.
% 18.32/17.82 bnd_ndr1_1 bnd_a1906 -->
% 18.32/17.82 (bnd_c9_2 bnd_a1906 X53 | ~ bnd_c2_2 bnd_a1906 X53) |
% 18.32/17.82 ~ bnd_c1_2 bnd_a1906 X53))) &
% 18.32/17.82 ((bnd_c3_0 | bnd_c9_0) |
% 18.32/17.82 (ALL X54.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c6_1 X54 |
% 18.32/17.82 (ALL X55.
% 18.32/17.82 bnd_ndr1_1 X54 -->
% 18.32/17.82 (~ bnd_c9_2 X54 X55 | bnd_c8_2 X54 X55) |
% 18.32/17.82 ~ bnd_c7_2 X54 X55)) |
% 18.32/17.82 ~ bnd_c3_1 X54))) &
% 18.32/17.82 ((~ bnd_c3_0 |
% 18.32/17.82 (ALL X56.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 bnd_c3_1 X56 |
% 18.32/17.82 (ALL X57.
% 18.32/17.82 bnd_ndr1_1 X56 -->
% 18.32/17.82 (bnd_c1_2 X56 X57 | ~ bnd_c10_2 X56 X57) |
% 18.32/17.82 ~ bnd_c2_2 X56 X57))) |
% 18.32/17.82 (ALL X58. bnd_ndr1_0 --> ~ bnd_c3_1 X58 | bnd_c9_1 X58))) &
% 18.32/17.82 (((ALL X59. bnd_ndr1_0 --> ~ bnd_c3_1 X59 | ~ bnd_c4_1 X59) |
% 18.32/17.82 ~ bnd_c3_0) |
% 18.32/17.82 (ALL X60.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X61.
% 18.32/17.82 bnd_ndr1_1 X60 -->
% 18.32/17.82 ~ bnd_c7_2 X60 X61 | ~ bnd_c4_2 X60 X61) |
% 18.32/17.82 (ALL X62.
% 18.32/17.82 bnd_ndr1_1 X60 -->
% 18.32/17.82 ~ bnd_c2_2 X60 X62 | ~ bnd_c9_2 X60 X62)) |
% 18.32/17.82 (ALL X63.
% 18.32/17.82 bnd_ndr1_1 X60 -->
% 18.32/17.82 (~ bnd_c2_2 X60 X63 | bnd_c3_2 X60 X63) |
% 18.32/17.82 ~ bnd_c4_2 X60 X63)))) &
% 18.32/17.82 (((bnd_ndr1_0 & bnd_c5_1 bnd_a1907) & ~ bnd_c10_1 bnd_a1907) &
% 18.32/17.82 bnd_c8_1 bnd_a1907 |
% 18.32/17.82 ~ bnd_c5_0)) &
% 18.32/17.82 (((ALL X64.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c10_1 X64 | bnd_c7_1 X64) |
% 18.32/17.82 ((bnd_ndr1_1 X64 & bnd_c9_2 X64 bnd_a1908) &
% 18.32/17.82 bnd_c1_2 X64 bnd_a1908) &
% 18.32/17.82 bnd_c3_2 X64 bnd_a1908) |
% 18.32/17.82 bnd_c1_0) |
% 18.32/17.82 (ALL X65.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c8_1 X65 |
% 18.32/17.82 (ALL X66.
% 18.32/17.82 bnd_ndr1_1 X65 -->
% 18.32/17.82 (bnd_c4_2 X65 X66 | bnd_c3_2 X65 X66) |
% 18.32/17.82 bnd_c10_2 X65 X66)) |
% 18.32/17.82 ((bnd_ndr1_1 X65 & bnd_c10_2 X65 bnd_a1909) &
% 18.32/17.82 ~ bnd_c2_2 X65 bnd_a1909) &
% 18.32/17.82 ~ bnd_c8_2 X65 bnd_a1909))) &
% 18.32/17.82 ((bnd_c3_0 | ~ bnd_c8_0) | ~ bnd_c9_0)) &
% 18.32/17.82 ((~ bnd_c3_0 |
% 18.32/17.82 ((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X67.
% 18.32/17.82 bnd_ndr1_1 bnd_a1910 -->
% 18.32/17.82 bnd_c1_2 bnd_a1910 X67 | ~ bnd_c2_2 bnd_a1910 X67)) &
% 18.32/17.82 (ALL X68.
% 18.32/17.82 bnd_ndr1_1 bnd_a1910 -->
% 18.32/17.82 ~ bnd_c7_2 bnd_a1910 X68 | bnd_c4_2 bnd_a1910 X68)) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1910) &
% 18.32/17.82 ~ bnd_c3_2 bnd_a1910 bnd_a1911) &
% 18.32/17.82 ~ bnd_c4_2 bnd_a1910 bnd_a1911) |
% 18.32/17.82 ((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a1912) &
% 18.32/17.82 (ALL X69.
% 18.32/17.82 bnd_ndr1_1 bnd_a1912 -->
% 18.32/17.82 (~ bnd_c5_2 bnd_a1912 X69 | bnd_c7_2 bnd_a1912 X69) |
% 18.32/17.82 bnd_c2_2 bnd_a1912 X69)) &
% 18.32/17.82 bnd_c3_1 bnd_a1912)) &
% 18.32/17.82 ((bnd_c10_0 | ~ bnd_c2_0) | bnd_c7_0)) &
% 18.32/17.82 (((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1913) &
% 18.32/17.82 (ALL X70.
% 18.32/17.82 bnd_ndr1_1 bnd_a1913 -->
% 18.32/17.82 (bnd_c9_2 bnd_a1913 X70 | bnd_c7_2 bnd_a1913 X70) |
% 18.32/17.82 bnd_c3_2 bnd_a1913 X70) |
% 18.32/17.82 bnd_c1_0) |
% 18.32/17.82 ((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a1914) & bnd_c9_1 bnd_a1914) &
% 18.32/17.82 bnd_c5_1 bnd_a1914)) &
% 18.32/17.82 ((~ bnd_c9_0 |
% 18.32/17.82 ((((bnd_ndr1_0 & bnd_c5_1 bnd_a1915) & bnd_ndr1_1 bnd_a1915) &
% 18.32/17.82 bnd_c5_2 bnd_a1915 bnd_a1916) &
% 18.32/17.82 ~ bnd_c9_2 bnd_a1915 bnd_a1916) &
% 18.32/17.82 (ALL X71.
% 18.32/17.82 bnd_ndr1_1 bnd_a1915 -->
% 18.32/17.82 bnd_c1_2 bnd_a1915 X71 | bnd_c7_2 bnd_a1915 X71)) |
% 18.32/17.82 bnd_c1_0)) &
% 18.32/17.82 ((bnd_c6_0 |
% 18.32/17.82 (ALL X72.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X73.
% 18.32/17.82 bnd_ndr1_1 X72 -->
% 18.32/17.82 (bnd_c9_2 X72 X73 | ~ bnd_c1_2 X72 X73) | bnd_c10_2 X72 X73) |
% 18.32/17.82 bnd_c8_1 X72) |
% 18.32/17.82 (ALL X74.
% 18.32/17.82 bnd_ndr1_1 X72 -->
% 18.32/17.82 (~ bnd_c10_2 X72 X74 | bnd_c2_2 X72 X74) |
% 18.32/17.82 ~ bnd_c7_2 X72 X74))) |
% 18.32/17.82 ~ bnd_c3_0)) &
% 18.32/17.82 (((ALL X75.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c5_1 X75 |
% 18.32/17.82 (ALL X76.
% 18.32/17.82 bnd_ndr1_1 X75 -->
% 18.32/17.82 (~ bnd_c3_2 X75 X76 | ~ bnd_c1_2 X75 X76) |
% 18.32/17.82 ~ bnd_c6_2 X75 X76)) |
% 18.32/17.82 bnd_c2_1 X75) |
% 18.32/17.82 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1917) &
% 18.32/17.82 ~ bnd_c4_2 bnd_a1917 bnd_a1918) &
% 18.32/17.82 bnd_c2_2 bnd_a1917 bnd_a1918) &
% 18.32/17.82 bnd_c5_2 bnd_a1917 bnd_a1918) &
% 18.32/17.82 (ALL X77.
% 18.32/17.82 bnd_ndr1_1 bnd_a1917 -->
% 18.32/17.82 (bnd_c10_2 bnd_a1917 X77 | bnd_c4_2 bnd_a1917 X77) |
% 18.32/17.82 ~ bnd_c9_2 bnd_a1917 X77)) &
% 18.32/17.82 bnd_c7_1 bnd_a1917) |
% 18.32/17.82 ~ bnd_c5_0)) &
% 18.32/17.82 (((((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1919) & bnd_ndr1_1 bnd_a1919) &
% 18.32/17.82 bnd_c3_2 bnd_a1919 bnd_a1920) &
% 18.32/17.82 bnd_c9_2 bnd_a1919 bnd_a1920) &
% 18.32/17.82 ~ bnd_c1_2 bnd_a1919 bnd_a1920) &
% 18.32/17.82 ~ bnd_c4_1 bnd_a1919 |
% 18.32/17.82 ((bnd_ndr1_0 & bnd_c8_1 bnd_a1921) & bnd_c5_1 bnd_a1921) &
% 18.32/17.82 ~ bnd_c6_1 bnd_a1921) |
% 18.32/17.82 ~ bnd_c4_0)) &
% 18.32/17.82 ((bnd_c4_0 | bnd_c7_0) |
% 18.32/17.82 (((((bnd_ndr1_0 &
% 18.32/17.82 (ALL X78.
% 18.32/17.82 bnd_ndr1_1 bnd_a1922 -->
% 18.32/17.82 (~ bnd_c10_2 bnd_a1922 X78 | ~ bnd_c2_2 bnd_a1922 X78) |
% 18.32/17.82 ~ bnd_c5_2 bnd_a1922 X78)) &
% 18.32/17.82 bnd_c8_1 bnd_a1922) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1922) &
% 18.32/17.82 ~ bnd_c3_2 bnd_a1922 bnd_a1923) &
% 18.32/17.82 bnd_c8_2 bnd_a1922 bnd_a1923) &
% 18.32/17.82 ~ bnd_c7_2 bnd_a1922 bnd_a1923)) &
% 18.32/17.82 ((bnd_c1_0 |
% 18.32/17.82 ((bnd_ndr1_0 &
% 18.32/17.82 (ALL X79.
% 18.32/17.82 bnd_ndr1_1 bnd_a1924 -->
% 18.32/17.82 (~ bnd_c7_2 bnd_a1924 X79 | ~ bnd_c10_2 bnd_a1924 X79) |
% 18.32/17.82 ~ bnd_c8_2 bnd_a1924 X79)) &
% 18.32/17.82 ~ bnd_c5_1 bnd_a1924) &
% 18.32/17.82 (ALL X80.
% 18.32/17.82 bnd_ndr1_1 bnd_a1924 -->
% 18.32/17.82 (~ bnd_c8_2 bnd_a1924 X80 | bnd_c1_2 bnd_a1924 X80) |
% 18.32/17.82 ~ bnd_c9_2 bnd_a1924 X80)) |
% 18.32/17.82 (ALL X81.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X81 & bnd_c7_2 X81 bnd_a1925) & bnd_c5_2 X81 bnd_a1925) &
% 18.32/17.82 bnd_c10_2 X81 bnd_a1925 |
% 18.32/17.82 bnd_c6_1 X81) |
% 18.32/17.82 ~ bnd_c7_1 X81))) &
% 18.32/17.82 ((~ bnd_c3_0 |
% 18.32/17.82 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a1926) & bnd_c5_1 bnd_a1926) &
% 18.32/17.82 ~ bnd_c6_1 bnd_a1926) |
% 18.32/17.82 ~ bnd_c5_0)) &
% 18.32/17.82 ((~ bnd_c10_0 | ~ bnd_c5_0) |
% 18.32/17.82 (ALL X82.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X83.
% 18.32/17.82 bnd_ndr1_1 X82 -->
% 18.32/17.82 (~ bnd_c10_2 X82 X83 | ~ bnd_c1_2 X82 X83) | ~ bnd_c5_2 X82 X83) |
% 18.32/17.82 (ALL X84.
% 18.32/17.82 bnd_ndr1_1 X82 -->
% 18.32/17.82 (~ bnd_c1_2 X82 X84 | bnd_c4_2 X82 X84) | ~ bnd_c5_2 X82 X84)) |
% 18.32/17.82 bnd_c3_1 X82))) &
% 18.32/17.82 ((ALL X85.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((bnd_ndr1_1 X85 & bnd_c1_2 X85 bnd_a1927) & ~ bnd_c9_2 X85 bnd_a1927 |
% 18.32/17.82 ~ bnd_c1_1 X85) |
% 18.32/17.82 bnd_c2_1 X85) |
% 18.32/17.82 bnd_c6_0)) &
% 18.32/17.82 (((bnd_ndr1_0 &
% 18.32/17.82 (ALL X86.
% 18.32/17.82 bnd_ndr1_1 bnd_a1928 -->
% 18.32/17.82 (bnd_c8_2 bnd_a1928 X86 | ~ bnd_c9_2 bnd_a1928 X86) |
% 18.32/17.82 ~ bnd_c10_2 bnd_a1928 X86)) &
% 18.32/17.82 (ALL X87.
% 18.32/17.82 bnd_ndr1_1 bnd_a1928 -->
% 18.32/17.82 (bnd_c3_2 bnd_a1928 X87 | ~ bnd_c9_2 bnd_a1928 X87) |
% 18.32/17.82 bnd_c7_2 bnd_a1928 X87) |
% 18.32/17.82 bnd_c5_0) |
% 18.32/17.82 (ALL X88.
% 18.32/17.82 bnd_ndr1_0 --> bnd_c5_1 X88 | ~ bnd_c6_1 X88))) &
% 18.32/17.82 (((ALL X89.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X89 & ~ bnd_c9_2 X89 bnd_a1929) & bnd_c8_2 X89 bnd_a1929) &
% 18.32/17.82 ~ bnd_c3_2 X89 bnd_a1929 |
% 18.32/17.82 ~ bnd_c5_1 X89) |
% 18.32/17.82 ~ bnd_c2_1 X89) |
% 18.32/17.82 (ALL X90.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c10_1 X90 | bnd_c3_1 X90) |
% 18.32/17.82 ((bnd_ndr1_1 X90 & ~ bnd_c6_2 X90 bnd_a1930) & bnd_c8_2 X90 bnd_a1930) &
% 18.32/17.82 bnd_c7_2 X90 bnd_a1930)) |
% 18.32/17.82 (((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a1931) &
% 18.32/17.82 (ALL X91.
% 18.32/17.82 bnd_ndr1_1 bnd_a1931 -->
% 18.32/17.82 (~ bnd_c2_2 bnd_a1931 X91 | bnd_c5_2 bnd_a1931 X91) |
% 18.32/17.82 ~ bnd_c1_2 bnd_a1931 X91)) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1931) &
% 18.32/17.82 bnd_c1_2 bnd_a1931 bnd_a1932) &
% 18.32/17.82 ~ bnd_c9_2 bnd_a1931 bnd_a1932) &
% 18.32/17.82 bnd_c7_2 bnd_a1931 bnd_a1932)) &
% 18.32/17.82 (((ALL X92.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c6_1 X92 | bnd_c5_1 X92) |
% 18.32/17.82 bnd_c9_1 X92) |
% 18.32/17.82 (ALL X93.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c6_1 X93 |
% 18.32/17.82 (ALL X94.
% 18.32/17.82 bnd_ndr1_1 X93 -->
% 18.32/17.82 (bnd_c5_2 X93 X94 | ~ bnd_c6_2 X93 X94) | ~ bnd_c2_2 X93 X94)) |
% 18.32/17.82 (ALL X95.
% 18.32/17.82 bnd_ndr1_1 X93 -->
% 18.32/17.82 (~ bnd_c6_2 X93 X95 | bnd_c7_2 X93 X95) | bnd_c5_2 X93 X95))) |
% 18.32/17.82 (ALL X96.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c4_1 X96 |
% 18.32/17.82 (ALL X97.
% 18.32/17.82 bnd_ndr1_1 X96 -->
% 18.32/17.82 (~ bnd_c1_2 X96 X97 | bnd_c10_2 X96 X97) | ~ bnd_c8_2 X96 X97)) |
% 18.32/17.82 bnd_c9_1 X96))) &
% 18.32/17.82 ((~ bnd_c5_0 | ~ bnd_c7_0) |
% 18.32/17.82 (((((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a1933) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1933) &
% 18.32/17.82 ~ bnd_c1_2 bnd_a1933 bnd_a1934) &
% 18.32/17.82 bnd_c5_2 bnd_a1933 bnd_a1934) &
% 18.32/17.82 bnd_c8_2 bnd_a1933 bnd_a1934) &
% 18.32/17.82 ~ bnd_c3_1 bnd_a1933)) &
% 18.32/17.82 ((bnd_c2_0 |
% 18.32/17.82 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1935) &
% 18.32/17.82 ~ bnd_c8_2 bnd_a1935 bnd_a1936) &
% 18.32/17.82 bnd_c5_2 bnd_a1935 bnd_a1936) &
% 18.32/17.82 (ALL X98.
% 18.32/17.82 bnd_ndr1_1 bnd_a1935 -->
% 18.32/17.82 (~ bnd_c8_2 bnd_a1935 X98 |
% 18.32/17.82 bnd_c10_2 bnd_a1935 X98) |
% 18.32/17.82 bnd_c3_2 bnd_a1935 X98)) &
% 18.32/17.82 ~ bnd_c9_1 bnd_a1935) |
% 18.32/17.82 (ALL X99.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ~ bnd_c10_1 X99 | ~ bnd_c6_1 X99))) &
% 18.32/17.82 ((bnd_c10_0 | bnd_c7_0) |
% 18.32/17.82 ((((bnd_ndr1_0 & bnd_c2_1 bnd_a1937) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1937) &
% 18.32/17.82 ~ bnd_c7_2 bnd_a1937 bnd_a1938) &
% 18.32/17.82 ~ bnd_c6_2 bnd_a1937 bnd_a1938) &
% 18.32/17.82 ~ bnd_c10_1 bnd_a1937)) &
% 18.32/17.82 (((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a1939) &
% 18.32/17.82 bnd_c10_1 bnd_a1939) &
% 18.32/17.82 (ALL X100.
% 18.32/17.82 bnd_ndr1_1 bnd_a1939 -->
% 18.32/17.82 ~ bnd_c8_2 bnd_a1939 X100 |
% 18.32/17.82 ~ bnd_c3_2 bnd_a1939 X100) |
% 18.32/17.82 (ALL X101.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((bnd_ndr1_1 X101 &
% 18.32/17.82 ~ bnd_c6_2 X101 bnd_a1940) &
% 18.32/17.82 bnd_c8_2 X101 bnd_a1940 |
% 18.32/17.82 bnd_c3_1 X101) |
% 18.32/17.82 ~ bnd_c6_1 X101))) &
% 18.32/17.82 ((~ bnd_c3_0 | bnd_c7_0) |
% 18.32/17.82 (bnd_ndr1_0 & ~ bnd_c1_1 bnd_a1941) &
% 18.32/17.82 ~ bnd_c9_1 bnd_a1941)) &
% 18.32/17.82 ((bnd_c7_0 |
% 18.32/17.82 (ALL X102.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c4_1 X102 |
% 18.32/17.82 ((bnd_ndr1_1 X102 &
% 18.32/17.82 ~ bnd_c3_2 X102 bnd_a1942) &
% 18.32/17.82 ~ bnd_c9_2 X102 bnd_a1942) &
% 18.32/17.82 ~ bnd_c6_2 X102 bnd_a1942) |
% 18.32/17.82 bnd_c2_1 X102)) |
% 18.32/17.82 (ALL X103.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c2_1 X103 | ~ bnd_c3_1 X103) |
% 18.32/17.82 ~ bnd_c10_1 X103))) &
% 18.32/17.82 ((bnd_c6_0 | bnd_c1_0) |
% 18.32/17.82 (ALL X104.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X105.
% 18.32/17.82 bnd_ndr1_1 X104 -->
% 18.32/17.82 (~ bnd_c9_2 X104 X105 |
% 18.32/17.82 bnd_c8_2 X104 X105) |
% 18.32/17.82 bnd_c2_2 X104 X105) |
% 18.32/17.82 (ALL X106.
% 18.32/17.82 bnd_ndr1_1 X104 -->
% 18.32/17.82 bnd_c10_2 X104 X106 |
% 18.32/17.82 ~ bnd_c1_2 X104 X106)) |
% 18.32/17.82 ~ bnd_c9_1 X104))) &
% 18.32/17.82 (((((((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a1943) &
% 18.32/17.82 bnd_ndr1_1 bnd_a1943) &
% 18.32/17.82 bnd_c4_2 bnd_a1943 bnd_a1944) &
% 18.32/17.82 ~ bnd_c1_2 bnd_a1943 bnd_a1944) &
% 18.32/17.82 bnd_c10_2 bnd_a1943 bnd_a1944) &
% 18.32/17.82 ~ bnd_c4_1 bnd_a1943 |
% 18.32/17.82 ((bnd_ndr1_0 &
% 18.32/17.82 (ALL X107.
% 18.32/17.82 bnd_ndr1_1 bnd_a1945 -->
% 18.32/17.82 bnd_c2_2 bnd_a1945 X107 |
% 18.32/17.82 ~ bnd_c4_2 bnd_a1945 X107)) &
% 18.32/17.82 (ALL X108.
% 18.32/17.82 bnd_ndr1_1 bnd_a1945 -->
% 18.32/17.82 (~ bnd_c10_2 bnd_a1945 X108 |
% 18.32/17.82 ~ bnd_c5_2 bnd_a1945 X108) |
% 18.32/17.82 ~ bnd_c3_2 bnd_a1945 X108)) &
% 18.32/17.82 ~ bnd_c4_1 bnd_a1945) |
% 18.32/17.82 (ALL X109.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (ALL X110.
% 18.32/17.82 bnd_ndr1_1 X109 -->
% 18.32/17.82 (~ bnd_c3_2 X109 X110 |
% 18.32/17.82 ~ bnd_c8_2 X109 X110) |
% 18.32/17.82 bnd_c1_2 X109 X110) |
% 18.32/17.82 (ALL X111.
% 18.32/17.82 bnd_ndr1_1 X109 -->
% 18.32/17.82 (~ bnd_c6_2 X109 X111 |
% 18.32/17.82 ~ bnd_c8_2 X109 X111) |
% 18.32/17.82 bnd_c3_2 X109 X111)))) &
% 18.32/17.82 (((bnd_ndr1_0 & bnd_c8_1 bnd_a1946) &
% 18.32/17.82 ~ bnd_c1_1 bnd_a1946 |
% 18.32/17.82 bnd_c9_0) |
% 18.32/17.82 (ALL X112.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c10_1 X112 |
% 18.32/17.82 ((bnd_ndr1_1 X112 & bnd_c9_2 X112 bnd_a1947) &
% 18.32/17.82 bnd_c2_2 X112 bnd_a1947) &
% 18.32/17.82 bnd_c7_2 X112 bnd_a1947) |
% 18.32/17.82 ((bnd_ndr1_1 X112 & ~ bnd_c10_2 X112 bnd_a1948) &
% 18.32/17.82 bnd_c7_2 X112 bnd_a1948) &
% 18.32/17.82 ~ bnd_c6_2 X112 bnd_a1948))) &
% 18.32/17.82 (((ALL X113.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c8_1 X113 | bnd_c1_1 X113) |
% 18.32/17.82 ((bnd_ndr1_1 X113 & bnd_c9_2 X113 bnd_a1949) &
% 18.32/17.82 bnd_c7_2 X113 bnd_a1949) &
% 18.32/17.82 bnd_c10_2 X113 bnd_a1949) |
% 18.32/17.82 ((bnd_ndr1_0 & bnd_c5_1 bnd_a1950) &
% 18.32/17.82 (ALL X114.
% 18.32/17.82 bnd_ndr1_1 bnd_a1950 -->
% 18.32/17.82 (bnd_c10_2 bnd_a1950 X114 |
% 18.32/17.82 bnd_c3_2 bnd_a1950 X114) |
% 18.32/17.82 ~ bnd_c4_2 bnd_a1950 X114)) &
% 18.32/17.82 ~ bnd_c1_1 bnd_a1950) |
% 18.32/17.82 (bnd_ndr1_0 & ~ bnd_c3_1 bnd_a1951) &
% 18.32/17.82 bnd_c5_1 bnd_a1951)) &
% 18.32/17.82 ((~ bnd_c7_0 |
% 18.32/17.82 (ALL X115.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (bnd_c8_1 X115 | ~ bnd_c1_1 X115) |
% 18.32/17.82 (ALL X116.
% 18.32/17.82 bnd_ndr1_1 X115 --> ~ bnd_c2_2 X115 X116))) |
% 18.32/17.82 ~ bnd_c5_0)) &
% 18.32/17.82 (((ALL X117.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (ALL X118.
% 18.32/17.82 bnd_ndr1_1 X117 -->
% 18.32/17.82 (~ bnd_c7_2 X117 X118 | ~ bnd_c6_2 X117 X118) |
% 18.32/17.82 ~ bnd_c3_2 X117 X118) |
% 18.32/17.82 bnd_c6_1 X117) |
% 18.32/17.82 ~ bnd_c5_0) |
% 18.32/17.82 (bnd_ndr1_0 & ~ bnd_c10_1 bnd_a1952) &
% 18.32/17.82 (ALL X119.
% 18.32/17.82 bnd_ndr1_1 bnd_a1952 -->
% 18.32/17.82 (~ bnd_c1_2 bnd_a1952 X119 |
% 18.32/17.82 ~ bnd_c7_2 bnd_a1952 X119) |
% 18.32/17.82 bnd_c3_2 bnd_a1952 X119))) &
% 18.32/17.82 (bnd_c3_0 |
% 18.32/17.82 (ALL X120.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 ((ALL X121.
% 18.32/17.82 bnd_ndr1_1 X120 -->
% 18.32/17.82 (bnd_c1_2 X120 X121 | ~ bnd_c5_2 X120 X121) |
% 18.32/17.82 ~ bnd_c7_2 X120 X121) |
% 18.32/17.82 ((bnd_ndr1_1 X120 & bnd_c4_2 X120 bnd_a1953) &
% 18.32/17.82 bnd_c10_2 X120 bnd_a1953) &
% 18.32/17.82 ~ bnd_c6_2 X120 bnd_a1953) |
% 18.32/17.82 ((bnd_ndr1_1 X120 & bnd_c3_2 X120 bnd_a1954) &
% 18.32/17.82 bnd_c10_2 X120 bnd_a1954) &
% 18.32/17.82 bnd_c5_2 X120 bnd_a1954))) &
% 18.32/17.82 (((ALL X122.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (~ bnd_c10_1 X122 |
% 18.32/17.82 ((bnd_ndr1_1 X122 & bnd_c5_2 X122 bnd_a1955) &
% 18.32/17.82 bnd_c3_2 X122 bnd_a1955) &
% 18.32/17.82 ~ bnd_c1_2 X122 bnd_a1955) |
% 18.32/17.82 ~ bnd_c7_1 X122) |
% 18.32/17.82 bnd_c8_0) |
% 18.32/17.82 (ALL X123.
% 18.32/17.82 bnd_ndr1_0 -->
% 18.32/17.82 (((bnd_ndr1_1 X123 & bnd_c8_2 X123 bnd_a1956) &
% 18.32/17.82 bnd_c1_2 X123 bnd_a1956) &
% 18.32/17.82 ~ bnd_c6_2 X123 bnd_a1956 |
% 18.32/17.82 ((bnd_ndr1_1 X123 & ~ bnd_c7_2 X123 bnd_a1957) &
% 18.32/17.83 ~ bnd_c8_2 X123 bnd_a1957) &
% 18.32/17.83 bnd_c6_2 X123 bnd_a1957) |
% 18.32/17.83 ~ bnd_c8_1 X123))) &
% 18.32/17.83 ((bnd_c7_0 | ~ bnd_c3_0) |
% 18.32/17.83 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1958) &
% 18.32/17.83 bnd_c4_2 bnd_a1958 bnd_a1959) &
% 18.32/17.83 ~ bnd_c7_2 bnd_a1958 bnd_a1959) &
% 18.32/17.83 bnd_c8_2 bnd_a1958 bnd_a1959) &
% 18.32/17.83 ~ bnd_c9_1 bnd_a1958) &
% 18.32/17.83 ~ bnd_c5_1 bnd_a1958)) &
% 18.32/17.83 ((bnd_c8_0 |
% 18.32/17.83 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1960) &
% 18.32/17.83 ~ bnd_c3_2 bnd_a1960 bnd_a1961) &
% 18.32/17.83 ~ bnd_c10_2 bnd_a1960 bnd_a1961) &
% 18.32/17.83 ~ bnd_c5_1 bnd_a1960) &
% 18.32/17.83 ~ bnd_c10_1 bnd_a1960) |
% 18.32/17.83 (ALL X124.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c6_1 X124 |
% 18.32/17.83 (ALL X125.
% 18.32/17.83 bnd_ndr1_1 X124 -->
% 18.32/17.83 (bnd_c9_2 X124 X125 | bnd_c1_2 X124 X125) |
% 18.32/17.83 bnd_c8_2 X124 X125)) |
% 18.32/17.83 bnd_c1_1 X124))) &
% 18.32/17.83 ((ALL X126.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c1_1 X126 | bnd_c8_1 X126) |
% 18.32/17.83 ((bnd_ndr1_1 X126 & bnd_c3_2 X126 bnd_a1962) &
% 18.32/17.83 bnd_c6_2 X126 bnd_a1962) &
% 18.32/17.83 ~ bnd_c9_2 X126 bnd_a1962) |
% 18.32/17.83 ((bnd_ndr1_0 & bnd_c5_1 bnd_a1963) &
% 18.32/17.83 (ALL X127.
% 18.32/17.83 bnd_ndr1_1 bnd_a1963 -->
% 18.32/17.83 (~ bnd_c10_2 bnd_a1963 X127 |
% 18.32/17.83 ~ bnd_c5_2 bnd_a1963 X127) |
% 18.32/17.83 bnd_c6_2 bnd_a1963 X127)) &
% 18.32/17.83 (ALL X128.
% 18.32/17.83 bnd_ndr1_1 bnd_a1963 -->
% 18.32/17.83 (~ bnd_c9_2 bnd_a1963 X128 | bnd_c4_2 bnd_a1963 X128) |
% 18.32/17.83 bnd_c1_2 bnd_a1963 X128))) &
% 18.32/17.83 (((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1964) &
% 18.32/17.83 bnd_c3_2 bnd_a1964 bnd_a1965) &
% 18.32/17.83 bnd_c9_2 bnd_a1964 bnd_a1965) &
% 18.32/17.83 ~ bnd_c4_2 bnd_a1964 bnd_a1965) &
% 18.32/17.83 bnd_ndr1_1 bnd_a1964) &
% 18.32/17.83 ~ bnd_c10_2 bnd_a1964 bnd_a1966) &
% 18.32/17.83 ~ bnd_c3_2 bnd_a1964 bnd_a1966) &
% 18.32/17.83 (ALL X129.
% 18.32/17.83 bnd_ndr1_1 bnd_a1964 -->
% 18.32/17.83 (bnd_c3_2 bnd_a1964 X129 | ~ bnd_c2_2 bnd_a1964 X129) |
% 18.32/17.83 bnd_c9_2 bnd_a1964 X129) |
% 18.32/17.83 ~ bnd_c6_0) |
% 18.32/17.83 bnd_c5_0)) &
% 18.32/17.83 ((ALL X130.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c5_1 X130 |
% 18.32/17.83 (ALL X131.
% 18.32/17.83 bnd_ndr1_1 X130 -->
% 18.32/17.83 (~ bnd_c10_2 X130 X131 | ~ bnd_c4_2 X130 X131) |
% 18.32/17.83 bnd_c6_2 X130 X131)) |
% 18.32/17.83 ~ bnd_c7_1 X130) |
% 18.32/17.83 ((bnd_ndr1_0 &
% 18.32/17.83 (ALL X132.
% 18.32/17.83 bnd_ndr1_1 bnd_a1967 -->
% 18.32/17.83 bnd_c3_2 bnd_a1967 X132 | bnd_c5_2 bnd_a1967 X132)) &
% 18.32/17.83 (ALL X133.
% 18.32/17.83 bnd_ndr1_1 bnd_a1967 -->
% 18.32/17.83 (bnd_c1_2 bnd_a1967 X133 | ~ bnd_c5_2 bnd_a1967 X133) |
% 18.32/17.83 bnd_c8_2 bnd_a1967 X133)) &
% 18.32/17.83 (ALL X134.
% 18.32/17.83 bnd_ndr1_1 bnd_a1967 -->
% 18.32/17.83 (bnd_c4_2 bnd_a1967 X134 | ~ bnd_c10_2 bnd_a1967 X134) |
% 18.32/17.83 ~ bnd_c7_2 bnd_a1967 X134))) &
% 18.32/17.83 (((ALL X135.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c10_1 X135 |
% 18.32/17.83 ((bnd_ndr1_1 X135 & ~ bnd_c7_2 X135 bnd_a1968) &
% 18.32/17.83 ~ bnd_c2_2 X135 bnd_a1968) &
% 18.32/17.83 bnd_c8_2 X135 bnd_a1968) |
% 18.32/17.83 bnd_c1_1 X135) |
% 18.32/17.83 ~ bnd_c2_0) |
% 18.32/17.83 (ALL X136.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c6_1 X136 | bnd_c10_1 X136) | bnd_c4_1 X136))) &
% 18.32/17.83 ((bnd_c7_0 | bnd_c10_0) | ~ bnd_c1_0)) &
% 18.32/17.83 ((ALL X137.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 bnd_c7_1 X137 |
% 18.32/17.83 (ALL X138.
% 18.32/17.83 bnd_ndr1_1 X137 -->
% 18.32/17.83 ~ bnd_c6_2 X137 X138 | ~ bnd_c3_2 X137 X138)) |
% 18.32/17.83 (ALL X139.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c2_1 X139 | bnd_c7_1 X139) |
% 18.32/17.83 ((bnd_ndr1_1 X139 & bnd_c1_2 X139 bnd_a1969) &
% 18.32/17.83 ~ bnd_c5_2 X139 bnd_a1969) &
% 18.32/17.83 ~ bnd_c8_2 X139 bnd_a1969))) &
% 18.32/17.83 ((~ bnd_c4_0 |
% 18.32/17.83 ((bnd_ndr1_0 & ~ bnd_c10_1 bnd_a1970) & ~ bnd_c5_1 bnd_a1970) &
% 18.32/17.83 bnd_c7_1 bnd_a1970) |
% 18.32/17.83 ~ bnd_c1_0)) &
% 18.32/17.83 (((((((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a1971) & bnd_ndr1_1 bnd_a1971) &
% 18.32/17.83 ~ bnd_c8_2 bnd_a1971 bnd_a1972) &
% 18.32/17.83 ~ bnd_c5_2 bnd_a1971 bnd_a1972) &
% 18.32/17.83 ~ bnd_c7_2 bnd_a1971 bnd_a1972) &
% 18.32/17.83 bnd_ndr1_1 bnd_a1971) &
% 18.32/17.83 bnd_c7_2 bnd_a1971 bnd_a1973) &
% 18.32/17.83 bnd_c10_2 bnd_a1971 bnd_a1973 |
% 18.32/17.83 (ALL X140.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X140 & ~ bnd_c1_2 X140 bnd_a1974) &
% 18.32/17.83 ~ bnd_c2_2 X140 bnd_a1974) &
% 18.32/17.83 ~ bnd_c7_2 X140 bnd_a1974 |
% 18.32/17.83 ~ bnd_c6_1 X140) |
% 18.32/17.83 ~ bnd_c10_1 X140)) |
% 18.32/17.83 bnd_c5_0)) &
% 18.32/17.83 (((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a1975) &
% 18.32/17.83 (ALL X141.
% 18.32/17.83 bnd_ndr1_1 bnd_a1975 -->
% 18.32/17.83 (~ bnd_c7_2 bnd_a1975 X141 | ~ bnd_c10_2 bnd_a1975 X141) |
% 18.32/17.83 bnd_c5_2 bnd_a1975 X141) |
% 18.32/17.83 ~ bnd_c3_0) |
% 18.32/17.83 ~ bnd_c7_0)) &
% 18.32/17.83 (((ALL X142.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (ALL X143.
% 18.32/17.83 bnd_ndr1_1 X142 -->
% 18.32/17.83 (bnd_c4_2 X142 X143 | ~ bnd_c1_2 X142 X143) |
% 18.32/17.83 bnd_c10_2 X142 X143) |
% 18.32/17.83 bnd_c6_1 X142) |
% 18.32/17.83 (ALL X144.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 bnd_c5_1 X144 |
% 18.32/17.83 (ALL X145.
% 18.32/17.83 bnd_ndr1_1 X144 -->
% 18.32/17.83 (~ bnd_c1_2 X144 X145 | bnd_c5_2 X144 X145) |
% 18.32/17.83 bnd_c10_2 X144 X145))) |
% 18.32/17.83 ~ bnd_c10_0)) &
% 18.32/17.83 (~ bnd_c2_0 | bnd_c7_0)) &
% 18.32/17.83 ((bnd_c2_0 | ~ bnd_c10_0) | bnd_c9_0)) &
% 18.32/17.83 (((((((bnd_ndr1_0 & ~ bnd_c9_1 bnd_a1976) & bnd_ndr1_1 bnd_a1976) &
% 18.32/17.83 bnd_c8_2 bnd_a1976 bnd_a1977) &
% 18.32/17.83 bnd_c7_2 bnd_a1976 bnd_a1977) &
% 18.32/17.83 ~ bnd_c6_2 bnd_a1976 bnd_a1977) &
% 18.32/17.83 ~ bnd_c1_1 bnd_a1976 |
% 18.32/17.83 (ALL X146.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 ((ALL X147.
% 18.32/17.83 bnd_ndr1_1 X146 -->
% 18.32/17.83 (~ bnd_c2_2 X146 X147 | ~ bnd_c1_2 X146 X147) |
% 18.32/17.83 ~ bnd_c3_2 X146 X147) |
% 18.32/17.83 bnd_c3_1 X146) |
% 18.32/17.83 (ALL X148.
% 18.32/17.83 bnd_ndr1_1 X146 -->
% 18.32/17.83 (~ bnd_c3_2 X146 X148 | ~ bnd_c7_2 X146 X148) |
% 18.32/17.83 ~ bnd_c8_2 X146 X148))) |
% 18.32/17.83 (ALL X149.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c7_1 X149 |
% 18.32/17.83 (bnd_ndr1_1 X149 & bnd_c5_2 X149 bnd_a1978) &
% 18.32/17.83 bnd_c9_2 X149 bnd_a1978) |
% 18.32/17.83 (ALL X150.
% 18.32/17.83 bnd_ndr1_1 X149 -->
% 18.32/17.83 (~ bnd_c2_2 X149 X150 | bnd_c5_2 X149 X150) |
% 18.32/17.83 bnd_c7_2 X149 X150)))) &
% 18.32/17.83 ((((bnd_ndr1_0 & bnd_c1_1 bnd_a1979) & bnd_c9_1 bnd_a1979) &
% 18.32/17.83 (ALL X151.
% 18.32/17.83 bnd_ndr1_1 bnd_a1979 -->
% 18.32/17.83 (~ bnd_c7_2 bnd_a1979 X151 | ~ bnd_c4_2 bnd_a1979 X151) |
% 18.32/17.83 ~ bnd_c10_2 bnd_a1979 X151) |
% 18.32/17.83 bnd_c3_0) |
% 18.32/17.83 (ALL X152.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c10_1 X152 |
% 18.32/17.83 ((bnd_ndr1_1 X152 & bnd_c1_2 X152 bnd_a1980) &
% 18.32/17.83 bnd_c7_2 X152 bnd_a1980) &
% 18.32/17.83 bnd_c4_2 X152 bnd_a1980) |
% 18.32/17.83 ((bnd_ndr1_1 X152 & ~ bnd_c5_2 X152 bnd_a1981) &
% 18.32/17.83 ~ bnd_c2_2 X152 bnd_a1981) &
% 18.32/17.83 bnd_c7_2 X152 bnd_a1981))) &
% 18.32/17.83 (((ALL X153.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 bnd_c3_1 X153 |
% 18.32/17.83 ((bnd_ndr1_1 X153 & bnd_c5_2 X153 bnd_a1982) &
% 18.32/17.83 bnd_c10_2 X153 bnd_a1982) &
% 18.32/17.83 ~ bnd_c9_2 X153 bnd_a1982) |
% 18.32/17.83 bnd_c9_0) |
% 18.32/17.83 ~ bnd_c5_0)) &
% 18.32/17.83 (bnd_c9_0 | bnd_c1_0)) &
% 18.32/17.83 ((~ bnd_c3_0 | ~ bnd_c6_0) |
% 18.32/17.83 ~ bnd_c9_0)) &
% 18.32/17.83 (((ALL X154.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c2_1 X154 | ~ bnd_c5_1 X154) |
% 18.32/17.83 ((bnd_ndr1_1 X154 & ~ bnd_c5_2 X154 bnd_a1983) &
% 18.32/17.83 bnd_c8_2 X154 bnd_a1983) &
% 18.32/17.83 bnd_c1_2 X154 bnd_a1983) |
% 18.32/17.83 (ALL X155.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X155 & bnd_c8_2 X155 bnd_a1984) &
% 18.32/17.83 ~ bnd_c10_2 X155 bnd_a1984) &
% 18.32/17.83 bnd_c9_2 X155 bnd_a1984 |
% 18.32/17.83 bnd_c1_1 X155) |
% 18.32/17.83 ((bnd_ndr1_1 X155 & bnd_c8_2 X155 bnd_a1985) & bnd_c6_2 X155 bnd_a1985) &
% 18.32/17.83 bnd_c3_2 X155 bnd_a1985)) |
% 18.32/17.83 (((((bnd_ndr1_0 &
% 18.32/17.83 bnd_ndr1_1 bnd_a1986) &
% 18.32/17.83 ~ bnd_c5_2 bnd_a1986 bnd_a1987) &
% 18.32/17.83 bnd_c7_2 bnd_a1986 bnd_a1987) &
% 18.32/17.83 ~ bnd_c2_2 bnd_a1986 bnd_a1987) &
% 18.32/17.83 ~ bnd_c9_1 bnd_a1986) &
% 18.32/17.83 ~ bnd_c7_1 bnd_a1986)) &
% 18.32/17.83 (((ALL X156.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c4_1 X156 |
% 18.32/17.83 (ALL X157.
% 18.32/17.83 bnd_ndr1_1 X156 -->
% 18.32/17.83 (~ bnd_c1_2 X156 X157 | bnd_c3_2 X156 X157) |
% 18.32/17.83 ~ bnd_c8_2 X156 X157)) |
% 18.32/17.83 bnd_c5_1 X156) |
% 18.32/17.83 (((((bnd_ndr1_0 &
% 18.32/17.83 (ALL X158.
% 18.32/17.83 bnd_ndr1_1 bnd_a1988 -->
% 18.32/17.83 (~ bnd_c5_2 bnd_a1988 X158 | ~ bnd_c2_2 bnd_a1988 X158) |
% 18.32/17.83 ~ bnd_c1_2 bnd_a1988 X158)) &
% 18.32/17.83 bnd_ndr1_1 bnd_a1988) &
% 18.32/17.83 ~ bnd_c3_2 bnd_a1988 bnd_a1989) &
% 18.32/17.83 ~ bnd_c6_2 bnd_a1988 bnd_a1989) &
% 18.32/17.83 bnd_c5_2 bnd_a1988 bnd_a1989) &
% 18.32/17.83 ~ bnd_c5_1 bnd_a1988) |
% 18.32/17.83 (ALL X159.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c9_1 X159 | ~ bnd_c8_1 X159) |
% 18.32/17.83 (ALL X160.
% 18.32/17.83 bnd_ndr1_1 X159 -->
% 18.32/17.83 (~ bnd_c8_2 X159 X160 | bnd_c5_2 X159 X160) | bnd_c10_2 X159 X160)))) &
% 18.32/17.83 ((bnd_c2_0 | ~ bnd_c1_0) |
% 18.32/17.83 (ALL X161.
% 18.32/17.83 bnd_ndr1_0 --> (~ bnd_c6_1 X161 | ~ bnd_c4_1 X161) | bnd_c5_1 X161))) &
% 18.32/17.83 (((ALL X162.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X162 & ~ bnd_c5_2 X162 bnd_a1990) &
% 18.32/17.83 bnd_c10_2 X162 bnd_a1990) &
% 18.32/17.83 ~ bnd_c2_2 X162 bnd_a1990 |
% 18.32/17.83 ~ bnd_c10_1 X162) |
% 18.32/17.83 ((bnd_ndr1_1 X162 & bnd_c1_2 X162 bnd_a1991) & ~ bnd_c9_2 X162 bnd_a1991) &
% 18.32/17.83 ~ bnd_c4_2 X162 bnd_a1991) |
% 18.32/17.83 (ALL X163.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X163 & ~ bnd_c2_2 X163 bnd_a1992) & bnd_c8_2 X163 bnd_a1992) &
% 18.32/17.83 bnd_c10_2 X163 bnd_a1992 |
% 18.32/17.83 ((bnd_ndr1_1 X163 & bnd_c8_2 X163 bnd_a1993) & bnd_c10_2 X163 bnd_a1993) &
% 18.32/17.83 ~ bnd_c9_2 X163 bnd_a1993) |
% 18.32/17.83 bnd_c1_1 X163)) |
% 18.32/17.83 ~ bnd_c6_0)) &
% 18.32/17.83 (((ALL X164.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 ((bnd_ndr1_1 X164 &
% 18.32/17.83 ~ bnd_c10_2 X164 bnd_a1994) &
% 18.32/17.83 bnd_c9_2 X164 bnd_a1994 |
% 18.32/17.83 bnd_c4_1 X164) |
% 18.32/17.83 ~ bnd_c10_1 X164) |
% 18.32/17.83 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a1995) &
% 18.32/17.83 ~ bnd_c6_2 bnd_a1995 bnd_a1996) &
% 18.32/17.83 bnd_c5_2 bnd_a1995 bnd_a1996) &
% 18.32/17.83 ~ bnd_c1_2 bnd_a1995 bnd_a1996) &
% 18.32/17.83 (ALL X165.
% 18.32/17.83 bnd_ndr1_1 bnd_a1995 -->
% 18.32/17.83 (~ bnd_c3_2 bnd_a1995 X165 | bnd_c2_2 bnd_a1995 X165) |
% 18.32/17.83 bnd_c5_2 bnd_a1995 X165)) &
% 18.32/17.83 ~ bnd_c3_1 bnd_a1995) |
% 18.32/17.83 ~ bnd_c7_0)) &
% 18.32/17.83 ((bnd_ndr1_0 & bnd_c8_1 bnd_a1997) &
% 18.32/17.83 ~ bnd_c3_1 bnd_a1997 |
% 18.32/17.83 ~ bnd_c4_0)) &
% 18.32/17.83 ((((((((((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a1998) &
% 18.32/17.83 bnd_ndr1_1 bnd_a1998) &
% 18.32/17.83 bnd_c10_2 bnd_a1998 bnd_a1999) &
% 18.32/17.83 ~ bnd_c2_2 bnd_a1998 bnd_a1999) &
% 18.32/17.83 bnd_c3_2 bnd_a1998 bnd_a1999) &
% 18.32/17.83 bnd_ndr1_1 bnd_a1998) &
% 18.32/17.83 bnd_c6_2 bnd_a1998 bnd_a2000) &
% 18.32/17.83 bnd_c9_2 bnd_a1998 bnd_a2000) &
% 18.32/17.83 bnd_c1_2 bnd_a1998 bnd_a2000 |
% 18.32/17.83 (((((bnd_ndr1_0 & bnd_c2_1 bnd_a2001) &
% 18.32/17.83 bnd_ndr1_1 bnd_a2001) &
% 18.32/17.83 bnd_c9_2 bnd_a2001 bnd_a2002) &
% 18.32/17.83 ~ bnd_c2_2 bnd_a2001 bnd_a2002) &
% 18.32/17.83 bnd_c5_2 bnd_a2001 bnd_a2002) &
% 18.32/17.83 ~ bnd_c3_1 bnd_a2001) |
% 18.32/17.83 ~ bnd_c5_0)) &
% 18.32/17.83 ((((bnd_ndr1_0 &
% 18.32/17.83 (ALL X166.
% 18.32/17.83 bnd_ndr1_1 bnd_a2003 -->
% 18.32/17.83 (bnd_c3_2 bnd_a2003 X166 |
% 18.32/17.83 bnd_c1_2 bnd_a2003 X166) |
% 18.32/17.83 bnd_c9_2 bnd_a2003 X166)) &
% 18.32/17.83 (ALL X167.
% 18.32/17.83 bnd_ndr1_1 bnd_a2003 -->
% 18.32/17.83 (bnd_c9_2 bnd_a2003 X167 |
% 18.32/17.83 bnd_c4_2 bnd_a2003 X167) |
% 18.32/17.83 bnd_c6_2 bnd_a2003 X167)) &
% 18.32/17.83 bnd_c3_1 bnd_a2003 |
% 18.32/17.83 bnd_c2_0) |
% 18.32/17.83 ~ bnd_c8_0)) &
% 18.32/17.83 ((~ bnd_c6_0 | bnd_c1_0) |
% 18.32/17.83 ((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a2004) &
% 18.32/17.83 bnd_c8_2 bnd_a2004 bnd_a2005) &
% 18.32/17.83 ~ bnd_c10_2 bnd_a2004 bnd_a2005) &
% 18.32/17.83 (ALL X168.
% 18.32/17.83 bnd_ndr1_1 bnd_a2004 -->
% 18.32/17.83 ~ bnd_c1_2 bnd_a2004 X168 |
% 18.32/17.83 bnd_c9_2 bnd_a2004 X168)) &
% 18.32/17.83 ~ bnd_c1_1 bnd_a2004)) &
% 18.32/17.83 (((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a2006) &
% 18.32/17.83 bnd_c4_2 bnd_a2006 bnd_a2007) &
% 18.32/17.83 bnd_c7_2 bnd_a2006 bnd_a2007) &
% 18.32/17.83 ~ bnd_c2_2 bnd_a2006 bnd_a2007) &
% 18.32/17.83 bnd_c4_1 bnd_a2006) &
% 18.32/17.83 (ALL X169.
% 18.32/17.83 bnd_ndr1_1 bnd_a2006 -->
% 18.32/17.83 bnd_c9_2 bnd_a2006 X169 |
% 18.32/17.83 bnd_c7_2 bnd_a2006 X169) |
% 18.32/17.83 (ALL X170.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c9_1 X170 |
% 18.32/17.83 ((bnd_ndr1_1 X170 &
% 18.32/17.83 ~ bnd_c5_2 X170 bnd_a2008) &
% 18.32/17.83 bnd_c3_2 X170 bnd_a2008) &
% 18.32/17.83 ~ bnd_c2_2 X170 bnd_a2008) |
% 18.32/17.83 ((bnd_ndr1_1 X170 &
% 18.32/17.83 bnd_c6_2 X170 bnd_a2009) &
% 18.32/17.83 ~ bnd_c4_2 X170 bnd_a2009) &
% 18.32/17.83 bnd_c7_2 X170 bnd_a2009)) |
% 18.32/17.83 bnd_c4_0)) &
% 18.32/17.83 (bnd_c6_0 | ~ bnd_c10_0)) &
% 18.32/17.83 ((~ bnd_c6_0 |
% 18.32/17.83 ((bnd_ndr1_0 & bnd_c7_1 bnd_a2010) &
% 18.32/17.83 (ALL X171.
% 18.32/17.83 bnd_ndr1_1 bnd_a2010 -->
% 18.32/17.83 (bnd_c1_2 bnd_a2010 X171 |
% 18.32/17.83 bnd_c8_2 bnd_a2010 X171) |
% 18.32/17.83 bnd_c10_2 bnd_a2010 X171)) &
% 18.32/17.83 ~ bnd_c1_1 bnd_a2010) |
% 18.32/17.83 bnd_c1_0)) &
% 18.32/17.83 (((ALL X172.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X172 & bnd_c4_2 X172 bnd_a2011) &
% 18.32/17.83 bnd_c9_2 X172 bnd_a2011) &
% 18.32/17.83 bnd_c2_2 X172 bnd_a2011 |
% 18.32/17.83 bnd_c2_1 X172) |
% 18.32/17.83 (ALL X173.
% 18.32/17.83 bnd_ndr1_1 X172 -->
% 18.32/17.83 (bnd_c7_2 X172 X173 |
% 18.32/17.83 ~ bnd_c4_2 X172 X173) |
% 18.32/17.83 bnd_c2_2 X172 X173)) |
% 18.32/17.83 ~ bnd_c6_0) |
% 18.32/17.83 ~ bnd_c1_0)) &
% 18.32/17.83 (((ALL X174.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 ((ALL X175.
% 18.32/17.83 bnd_ndr1_1 X174 -->
% 18.32/17.83 (bnd_c10_2 X174 X175 |
% 18.32/17.83 bnd_c6_2 X174 X175) |
% 18.32/17.83 bnd_c9_2 X174 X175) |
% 18.32/17.83 bnd_c4_1 X174) |
% 18.32/17.83 (ALL X176.
% 18.32/17.83 bnd_ndr1_1 X174 -->
% 18.32/17.83 (~ bnd_c10_2 X174 X176 |
% 18.32/17.83 ~ bnd_c1_2 X174 X176) |
% 18.32/17.83 ~ bnd_c6_2 X174 X176)) |
% 18.32/17.83 (ALL X177.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c8_1 X177 | ~ bnd_c9_1 X177) |
% 18.32/17.83 (ALL X178.
% 18.32/17.83 bnd_ndr1_1 X177 -->
% 18.32/17.83 (~ bnd_c10_2 X177 X178 |
% 18.32/17.83 ~ bnd_c3_2 X177 X178) |
% 18.32/17.83 ~ bnd_c4_2 X177 X178))) |
% 18.32/17.83 ~ bnd_c6_0)) &
% 18.32/17.83 ((~ bnd_c2_0 |
% 18.32/17.83 (ALL X179.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 ((ALL X180.
% 18.32/17.83 bnd_ndr1_1 X179 -->
% 18.32/17.83 bnd_c1_2 X179 X180 | ~ bnd_c6_2 X179 X180) |
% 18.32/17.83 bnd_c5_1 X179) |
% 18.32/17.83 ((bnd_ndr1_1 X179 & bnd_c2_2 X179 bnd_a2012) &
% 18.32/17.83 ~ bnd_c7_2 X179 bnd_a2012) &
% 18.32/17.83 bnd_c8_2 X179 bnd_a2012)) |
% 18.32/17.83 (ALL X181.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X181 & bnd_c7_2 X181 bnd_a2013) &
% 18.32/17.83 ~ bnd_c4_2 X181 bnd_a2013) &
% 18.32/17.83 bnd_c1_2 X181 bnd_a2013 |
% 18.32/17.83 bnd_c10_1 X181) |
% 18.32/17.83 (ALL X182.
% 18.32/17.83 bnd_ndr1_1 X181 -->
% 18.32/17.83 (~ bnd_c8_2 X181 X182 | bnd_c4_2 X181 X182) |
% 18.32/17.83 bnd_c10_2 X181 X182)))) &
% 18.32/17.83 (((bnd_ndr1_0 & ~ bnd_c7_1 bnd_a2014) &
% 18.32/17.83 bnd_c2_1 bnd_a2014) &
% 18.32/17.83 (ALL X183.
% 18.32/17.83 bnd_ndr1_1 bnd_a2014 -->
% 18.32/17.83 (~ bnd_c3_2 bnd_a2014 X183 |
% 18.32/17.83 bnd_c9_2 bnd_a2014 X183) |
% 18.32/17.83 ~ bnd_c4_2 bnd_a2014 X183) |
% 18.32/17.83 (((bnd_ndr1_0 &
% 18.32/17.83 (ALL X184.
% 18.32/17.83 bnd_ndr1_1 bnd_a2015 -->
% 18.32/17.83 bnd_c2_2 bnd_a2015 X184 |
% 18.32/17.83 ~ bnd_c10_2 bnd_a2015 X184)) &
% 18.32/17.83 bnd_ndr1_1 bnd_a2015) &
% 18.32/17.83 ~ bnd_c8_2 bnd_a2015 bnd_a2016) &
% 18.32/17.83 ~ bnd_c9_2 bnd_a2015 bnd_a2016)) &
% 18.32/17.83 ((bnd_c3_0 | bnd_c7_0) | bnd_c2_0)) &
% 18.32/17.83 (bnd_c2_0 |
% 18.32/17.83 ((bnd_ndr1_0 & bnd_c8_1 bnd_a2017) &
% 18.32/17.83 bnd_c3_1 bnd_a2017) &
% 18.32/17.83 (ALL X185.
% 18.32/17.83 bnd_ndr1_1 bnd_a2017 -->
% 18.32/17.83 (bnd_c4_2 bnd_a2017 X185 | bnd_c7_2 bnd_a2017 X185) |
% 18.32/17.83 bnd_c2_2 bnd_a2017 X185))) &
% 18.32/17.83 ((~ bnd_c9_0 | bnd_c2_0) |
% 18.32/17.83 (ALL X186.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X186 & bnd_c6_2 X186 bnd_a2018) &
% 18.32/17.83 ~ bnd_c10_2 X186 bnd_a2018) &
% 18.32/17.83 ~ bnd_c4_2 X186 bnd_a2018 |
% 18.32/17.83 bnd_c8_1 X186) |
% 18.32/17.83 bnd_c10_1 X186))) &
% 18.32/17.83 (~ bnd_c2_0 | ~ bnd_c3_0)) &
% 18.32/17.83 ((((bnd_ndr1_0 & bnd_c4_1 bnd_a2019) &
% 18.32/17.83 (ALL X187.
% 18.32/17.83 bnd_ndr1_1 bnd_a2019 -->
% 18.32/17.83 (bnd_c2_2 bnd_a2019 X187 |
% 18.32/17.83 ~ bnd_c6_2 bnd_a2019 X187) |
% 18.32/17.83 ~ bnd_c3_2 bnd_a2019 X187)) &
% 18.32/17.83 bnd_c3_1 bnd_a2019 |
% 18.32/17.83 (ALL X188.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c6_1 X188 |
% 18.32/17.83 (bnd_ndr1_1 X188 & ~ bnd_c9_2 X188 bnd_a2020) &
% 18.32/17.83 bnd_c5_2 X188 bnd_a2020) |
% 18.32/17.83 (ALL X189.
% 18.32/17.83 bnd_ndr1_1 X188 -->
% 18.32/17.83 (~ bnd_c3_2 X188 X189 | bnd_c2_2 X188 X189) |
% 18.32/17.83 bnd_c1_2 X188 X189))) |
% 18.32/17.83 (ALL X190.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c3_1 X190 | ~ bnd_c10_1 X190) |
% 18.32/17.83 ~ bnd_c9_1 X190))) &
% 18.32/17.83 ((bnd_c4_0 | ~ bnd_c6_0) |
% 18.32/17.83 (ALL X191.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 ((ALL X192.
% 18.32/17.83 bnd_ndr1_1 X191 -->
% 18.32/17.83 (bnd_c8_2 X191 X192 | ~ bnd_c10_2 X191 X192) |
% 18.32/17.83 ~ bnd_c4_2 X191 X192) |
% 18.32/17.83 bnd_c8_1 X191) |
% 18.32/17.83 ~ bnd_c3_1 X191))) &
% 18.32/17.83 (((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a2021) & ~ bnd_c8_1 bnd_a2021) &
% 18.32/17.83 ~ bnd_c1_1 bnd_a2021 |
% 18.32/17.83 ~ bnd_c3_0)) &
% 18.32/17.83 ((~ bnd_c10_0 |
% 18.32/17.83 (bnd_ndr1_0 & bnd_c3_1 bnd_a2022) & ~ bnd_c7_1 bnd_a2022) |
% 18.32/17.83 bnd_c8_0)) &
% 18.32/17.83 (((bnd_ndr1_0 & ~ bnd_c8_1 bnd_a2023) & ~ bnd_c10_1 bnd_a2023) &
% 18.32/17.83 (ALL X193.
% 18.32/17.83 bnd_ndr1_1 bnd_a2023 -->
% 18.32/17.83 (bnd_c6_2 bnd_a2023 X193 | ~ bnd_c2_2 bnd_a2023 X193) |
% 18.32/17.83 ~ bnd_c5_2 bnd_a2023 X193) |
% 18.32/17.83 ~ bnd_c1_0)) &
% 18.32/17.83 (~ bnd_c9_0 |
% 18.32/17.83 (ALL X194.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c7_1 X194 |
% 18.32/17.83 (ALL X195.
% 18.32/17.83 bnd_ndr1_1 X194 -->
% 18.32/17.83 (bnd_c5_2 X194 X195 | bnd_c3_2 X194 X195) |
% 18.32/17.83 bnd_c4_2 X194 X195)) |
% 18.32/17.83 ~ bnd_c5_1 X194))) &
% 18.32/17.83 (bnd_c7_0 | bnd_c9_0)) &
% 18.32/17.83 (bnd_c3_0 | ~ bnd_c1_0)) &
% 18.32/17.83 (((ALL X196.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c4_1 X196 |
% 18.32/17.83 (ALL X197.
% 18.32/17.83 bnd_ndr1_1 X196 -->
% 18.32/17.83 (bnd_c7_2 X196 X197 | ~ bnd_c10_2 X196 X197) |
% 18.32/17.83 bnd_c4_2 X196 X197)) |
% 18.32/17.83 ((bnd_ndr1_1 X196 & bnd_c3_2 X196 bnd_a2024) &
% 18.32/17.83 bnd_c10_2 X196 bnd_a2024) &
% 18.32/17.83 ~ bnd_c6_2 X196 bnd_a2024) |
% 18.32/17.83 ~ bnd_c7_0) |
% 18.32/17.83 (ALL X198.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (bnd_c10_1 X198 |
% 18.32/17.83 (ALL X199.
% 18.32/17.83 bnd_ndr1_1 X198 -->
% 18.32/17.83 (~ bnd_c8_2 X198 X199 | bnd_c2_2 X198 X199) |
% 18.32/17.83 bnd_c3_2 X198 X199)) |
% 18.32/17.83 ((bnd_ndr1_1 X198 & ~ bnd_c5_2 X198 bnd_a2025) &
% 18.32/17.83 ~ bnd_c6_2 X198 bnd_a2025) &
% 18.32/17.83 bnd_c3_2 X198 bnd_a2025))) &
% 18.32/17.83 (((ALL X200.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (~ bnd_c5_1 X200 | bnd_c4_1 X200) |
% 18.32/17.83 ((bnd_ndr1_1 X200 & ~ bnd_c10_2 X200 bnd_a2026) &
% 18.32/17.83 bnd_c4_2 X200 bnd_a2026) &
% 18.32/17.83 bnd_c3_2 X200 bnd_a2026) |
% 18.32/17.83 ~ bnd_c7_0) |
% 18.32/17.83 bnd_c6_0)) &
% 18.32/17.83 ((((bnd_ndr1_0 & bnd_c3_1 bnd_a2027) & ~ bnd_c4_1 bnd_a2027) &
% 18.32/17.83 ~ bnd_c6_1 bnd_a2027 |
% 18.32/17.83 bnd_c8_0) |
% 18.32/17.83 (ALL X201.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 (((bnd_ndr1_1 X201 & bnd_c2_2 X201 bnd_a2028) &
% 18.32/17.83 ~ bnd_c8_2 X201 bnd_a2028) &
% 18.32/17.83 bnd_c4_2 X201 bnd_a2028 |
% 18.32/17.83 bnd_c2_1 X201) |
% 18.32/17.83 ~ bnd_c6_1 X201))) &
% 18.32/17.83 (((bnd_ndr1_0 & bnd_c10_1 bnd_a2029) &
% 18.32/17.83 (ALL X202.
% 18.32/17.83 bnd_ndr1_1 bnd_a2029 -->
% 18.32/17.83 (~ bnd_c3_2 bnd_a2029 X202 | bnd_c4_2 bnd_a2029 X202) |
% 18.32/17.83 ~ bnd_c8_2 bnd_a2029 X202)) &
% 18.32/17.83 (ALL X203.
% 18.32/17.83 bnd_ndr1_1 bnd_a2029 -->
% 18.32/17.83 (~ bnd_c9_2 bnd_a2029 X203 | ~ bnd_c4_2 bnd_a2029 X203) |
% 18.32/17.83 ~ bnd_c7_2 bnd_a2029 X203) |
% 18.32/17.83 bnd_c4_0)) &
% 18.32/17.83 ((bnd_c3_0 |
% 18.32/17.83 (bnd_ndr1_0 & ~ bnd_c7_1 bnd_a2030) & ~ bnd_c6_1 bnd_a2030) |
% 18.32/17.83 (ALL X204.
% 18.32/17.83 bnd_ndr1_0 -->
% 18.32/17.83 ((bnd_ndr1_1 X204 & bnd_c8_2 X204 bnd_a2031) &
% 18.32/17.83 ~ bnd_c5_2 X204 bnd_a2031 |
% 18.32/17.83 ((bnd_ndr1_1 X204 & bnd_c2_2 X204 bnd_a2032) &
% 18.32/17.83 bnd_c7_2 X204 bnd_a2032) &
% 18.32/17.83 ~ bnd_c1_2 X204 bnd_a2032) |
% 18.32/17.83 bnd_c1_1 X204)))
% 18.32/17.83 Adding axioms...
% 18.32/17.83 Typedef.type_definition_def
% 53.48/52.97 ...done.
% 53.58/53.01 Ground types: ?'b, TPTP_Interpret.ind
% 53.58/53.01 Translating term (sizes: 1, 1) ...
% 82.56/81.94 Invoking SAT solver...
% 82.56/81.95 No model exists.
% 82.56/81.95 Translating term (sizes: 2, 1) ...
% 112.36/111.64 Invoking SAT solver...
% 112.36/111.65 No model exists.
% 112.36/111.65 Translating term (sizes: 1, 2) ...
% 166.07/165.16 Invoking SAT solver...
% 166.78/165.83 Model found:
% 166.78/165.83 Size of types: ?'b: 1, TPTP_Interpret.ind: 2
% 166.78/165.83 bnd_a2032: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2031: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2030: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a2029: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a2028: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2027: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2026: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2025: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2024: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2023: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2022: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2021: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2020: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2019: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2018: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2017: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2016: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2015: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a2014: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2013: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2012: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2011: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2010: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2009: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2008: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2007: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2006: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2005: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2004: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2003: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2002: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2001: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a2000: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1999: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1998: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1997: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1996: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1995: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1994: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1993: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1992: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1991: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1990: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1989: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1988: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1987: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1986: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1985: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1984: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1983: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1982: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1981: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1980: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1979: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1978: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1977: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1976: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1975: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1974: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1973: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1972: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1971: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1970: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1969: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1968: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1967: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1966: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1965: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1964: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1963: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1962: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1961: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1960: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1959: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1958: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1957: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1956: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1955: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1954: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1953: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1952: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1951: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1950: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1949: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1948: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1947: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1946: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1945: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1944: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1943: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1942: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1941: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1940: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1939: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1938: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1937: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1936: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1935: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1934: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1933: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1932: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1931: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1930: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1929: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1928: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1927: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1926: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1925: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1924: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1923: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1922: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1921: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1920: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1919: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1918: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1917: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1916: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1915: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1914: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1913: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1912: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1911: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1910: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1909: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1908: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1907: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1906: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1905: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1904: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1903: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1902: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1901: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1900: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1899: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1898: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1897: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1896: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1895: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1894: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1893: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1892: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1891: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1890: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1889: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1888: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1887: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1886: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1885: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1884: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1883: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1882: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1881: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1880: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1879: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1878: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1877: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1876: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1875: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1874: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1873: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1872: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1871: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1870: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1869: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1868: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1867: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1866: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1865: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1864: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1863: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1862: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1861: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1860: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1859: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1858: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c8_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}
% 166.78/165.83 bnd_c2_0: True
% 166.78/165.83 bnd_a1857: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1856: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1855: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1854: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c7_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 166.78/165.83 bnd_c3_0: False
% 166.78/165.83 bnd_a1853: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_c1_0: False
% 166.78/165.83 bnd_c10_0: False
% 166.78/165.83 bnd_a1852: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1851: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1850: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1849: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c9_0: True
% 166.78/165.83 bnd_a1848: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c5_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 166.78/165.83 bnd_c5_0: False
% 166.78/165.83 bnd_a1847: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1846: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1845: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c1_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 166.78/165.83 bnd_c3_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 166.78/165.83 bnd_c9_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 166.78/165.83 bnd_a1844: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1843: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1842: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_a1841: ??.TPTP_Interpret.ind1
% 166.78/165.83 bnd_c2_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 166.78/165.83 bnd_c2_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_a1840: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c8_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_a1839: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c10_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 166.78/165.83 bnd_c10_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 166.78/165.83 bnd_a1838: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_a1837: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c4_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 166.78/165.83 bnd_c8_0: False
% 166.78/165.83 bnd_c7_0: True
% 166.78/165.83 bnd_c6_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 166.78/165.83 bnd_c6_0: False
% 166.78/165.83 bnd_c4_0: False
% 166.78/165.83 bnd_c6_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}
% 166.78/165.83 bnd_c4_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_a1836: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c1_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_c5_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_a1835: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c7_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)})}
% 166.78/165.83 bnd_c3_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_a1834: ??.TPTP_Interpret.ind0
% 166.78/165.83 bnd_c9_2: {(??.TPTP_Interpret.ind0,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 166.78/165.83 (??.TPTP_Interpret.ind1,
% 166.78/165.83 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)})}
% 166.78/165.83 bnd_ndr1_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 166.78/165.83 bnd_ndr1_0: True
% 166.78/165.83
% 166.78/165.83 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------