%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN428+1 : TPTP v9.0.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:03:32 PM UTC 2025 % Result : CounterSatisfiable 48.42s 23.15s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SYN428+1 : TPTP v9.0.0. Released v2.1.0. % 0.00/0.10 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.10/0.30 % Computer : n024.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Wed Apr 9 07:25:21 EDT 2025 % 0.10/0.30 % CPUTime : % 48.42/23.14 % 48.42/23.15 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 48.42/23.15 % 48.42/23.15 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 48.42/23.17 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > a2032 > a2031 > a2030 > a2029 > a2028 > a2027 > a2026 > a2025 > a2024 > a2023 > a2022 > a2021 > a2020 > a2019 > a2018 > a2017 > a2016 > a2015 > a2014 > a2013 > a2012 > a2011 > a2010 > a2009 > a2008 > a2007 > a2006 > a2005 > a2004 > a2003 > a2002 > a2001 > a2000 > a1999 > a1998 > a1997 > a1996 > a1995 > a1994 > a1993 > a1992 > a1991 > a1990 > a1989 > a1988 > a1987 > a1986 > a1985 > a1984 > a1983 > a1982 > a1981 > a1980 > a1979 > a1978 > a1977 > a1976 > a1975 > a1974 > a1973 > a1972 > a1971 > a1970 > a1969 > a1968 > a1967 > a1966 > a1965 > a1964 > a1963 > a1962 > a1961 > a1960 > a1959 > a1958 > a1957 > a1956 > a1955 > a1954 > a1953 > a1952 > a1951 > a1950 > a1949 > a1948 > a1947 > a1946 > a1945 > a1944 > a1943 > a1942 > a1941 > a1940 > a1939 > a1938 > a1937 > a1936 > a1935 > a1934 > a1933 > a1932 > a1931 > a1930 > a1929 > a1928 > a1927 > a1926 > a1925 > a1924 > a1923 > a1922 > a1921 > a1920 > a1919 > a1918 > a1917 > a1916 > a1915 > a1914 > a1913 > a1912 > a1911 > a1910 > a1909 > a1908 > a1907 > a1906 > a1905 > a1904 > a1903 > a1902 > a1901 > a1900 > a1899 > a1898 > a1897 > a1896 > a1895 > a1894 > a1893 > a1892 > a1891 > a1890 > a1889 > a1888 > a1887 > a1886 > a1885 > a1884 > a1883 > a1882 > a1881 > a1880 > a1879 > a1878 > a1877 > a1876 > a1875 > a1874 > a1873 > a1872 > a1871 > a1870 > a1869 > a1868 > a1867 > a1866 > a1865 > a1864 > a1863 > a1862 > a1861 > a1860 > a1859 > a1858 > a1857 > a1856 > a1855 > a1854 > a1853 > a1852 > a1851 > a1850 > a1849 > a1848 > a1847 > a1846 > a1845 > a1844 > a1843 > a1842 > a1841 > a1840 > a1839 > a1838 > a1837 > a1836 > a1835 > a1834 % 48.42/23.17 % 48.42/23.17 %Foreground sorts: % 48.42/23.17 % 48.42/23.17 % 48.42/23.17 %Background operators: % 48.42/23.17 % 48.42/23.17 % 48.42/23.17 %Foreground operators: % 48.42/23.17 tff(a1879, type, a1879: $i). % 48.42/23.17 tff(a1960, type, a1960: $i). % 48.42/23.17 tff(a2016, type, a2016: $i). % 48.42/23.17 tff(c7_0, type, c7_0: $o). % 48.42/23.17 tff(a1841, type, a1841: $i). % 48.42/23.17 tff(a2031, type, a2031: $i). % 48.42/23.17 tff(a1903, type, a1903: $i). % 48.42/23.17 tff(a1871, type, a1871: $i). % 48.42/23.17 tff(a1912, type, a1912: $i). % 48.42/23.17 tff(a1839, type, a1839: $i). % 48.42/23.17 tff(a1850, type, a1850: $i). % 48.42/23.17 tff(a1910, type, a1910: $i). % 48.42/23.17 tff(a1929, type, a1929: $i). % 48.42/23.17 tff(a1914, type, a1914: $i). % 48.42/23.17 tff(c4_0, type, c4_0: $o). % 48.42/23.17 tff(a1894, type, a1894: $i). % 48.42/23.17 tff(a1934, type, a1934: $i). % 48.42/23.17 tff(a1943, type, a1943: $i). % 48.42/23.17 tff(a1946, type, a1946: $i). % 48.42/23.17 tff(a1967, type, a1967: $i). % 48.42/23.17 tff(a2019, type, a2019: $i). % 48.42/23.17 tff(a1927, type, a1927: $i). % 48.42/23.17 tff(a1932, type, a1932: $i). % 48.42/23.17 tff(c3_0, type, c3_0: $o). % 48.42/23.17 tff(a2000, type, a2000: $i). % 48.42/23.17 tff(a1852, type, a1852: $i). % 48.42/23.17 tff(a1836, type, a1836: $i). % 48.42/23.17 tff(a1863, type, a1863: $i). % 48.42/23.17 tff(a1904, type, a1904: $i). % 48.42/23.17 tff(c1_2, type, c1_2: ($i * $i) > $o). % 48.42/23.17 tff(a1975, type, a1975: $i). % 48.42/23.17 tff(a2009, type, a2009: $i). % 48.42/23.17 tff(a1840, type, a1840: $i). % 48.42/23.17 tff(a1981, type, a1981: $i). % 48.42/23.17 tff(a1864, type, a1864: $i). % 48.42/23.17 tff(a1875, type, a1875: $i). % 48.42/23.17 tff(a1842, type, a1842: $i). % 48.42/23.17 tff(a1992, type, a1992: $i). % 48.42/23.17 tff(a2024, type, a2024: $i). % 48.42/23.17 tff(a2012, type, a2012: $i). % 48.42/23.17 tff(a2001, type, a2001: $i). % 48.42/23.17 tff(a2022, type, a2022: $i). % 48.42/23.17 tff(a1916, type, a1916: $i). % 48.42/23.17 tff(a1882, type, a1882: $i). % 48.42/23.17 tff(a1951, type, a1951: $i). % 48.42/23.17 tff(a1959, type, a1959: $i). % 48.42/23.17 tff(a1947, type, a1947: $i). % 48.42/23.17 tff(a1996, type, a1996: $i). % 48.42/23.17 tff(a2007, type, a2007: $i). % 48.42/23.17 tff(a2026, type, a2026: $i). % 48.42/23.17 tff(a1851, type, a1851: $i). % 48.42/23.17 tff(a1897, type, a1897: $i). % 48.42/23.17 tff(a2010, type, a2010: $i). % 48.42/23.17 tff(a1931, type, a1931: $i). % 48.42/23.17 tff(a1872, type, a1872: $i). % 48.42/23.17 tff(a2015, type, a2015: $i). % 48.42/23.17 tff(a1887, type, a1887: $i). % 48.42/23.17 tff(a2025, type, a2025: $i). % 48.42/23.17 tff(c8_0, type, c8_0: $o). % 48.42/23.17 tff(a1982, type, a1982: $i). % 48.42/23.17 tff(a1895, type, a1895: $i). % 48.42/23.17 tff(a1965, type, a1965: $i). % 48.42/23.17 tff(a1853, type, a1853: $i). % 48.42/23.17 tff(a1905, type, a1905: $i). % 48.42/23.17 tff(a1890, type, a1890: $i). % 48.42/23.17 tff(a1984, type, a1984: $i). % 48.42/23.17 tff(a1845, type, a1845: $i). % 48.42/23.17 tff(a1849, type, a1849: $i). % 48.42/23.17 tff(a1926, type, a1926: $i). % 48.42/23.17 tff(a1892, type, a1892: $i). % 48.42/23.17 tff(a1936, type, a1936: $i). % 48.42/23.17 tff(a1848, type, a1848: $i). % 48.42/23.17 tff(a1939, type, a1939: $i). % 48.42/23.17 tff(c5_0, type, c5_0: $o). % 48.42/23.17 tff(a2002, type, a2002: $i). % 48.42/23.17 tff(a1837, type, a1837: $i). % 48.42/23.17 tff(a2028, type, a2028: $i). % 48.42/23.17 tff(a1973, type, a1973: $i). % 48.42/23.17 tff(a1979, type, a1979: $i). % 48.42/23.17 tff(a2018, type, a2018: $i). % 48.42/23.17 tff(a1920, type, a1920: $i). % 48.42/23.17 tff(a1886, type, a1886: $i). % 48.42/23.17 tff(a1898, type, a1898: $i). % 48.42/23.17 tff(a1968, type, a1968: $i). % 48.42/23.17 tff(c6_0, type, c6_0: $o). % 48.42/23.17 tff(c8_2, type, c8_2: ($i * $i) > $o). % 48.42/23.17 tff(a1989, type, a1989: $i). % 48.42/23.17 tff(a1847, type, a1847: $i). % 48.42/23.17 tff(a1874, type, a1874: $i). % 48.42/23.17 tff(a1855, type, a1855: $i). % 48.42/23.17 tff(a1944, type, a1944: $i). % 48.42/23.17 tff(a1858, type, a1858: $i). % 48.42/23.17 tff(a2017, type, a2017: $i). % 48.42/23.17 tff(a1995, type, a1995: $i). % 48.42/23.17 tff(a1999, type, a1999: $i). % 48.42/23.17 tff(a2011, type, a2011: $i). % 48.42/23.17 tff(a1866, type, a1866: $i). % 48.42/23.17 tff(a1969, type, a1969: $i). % 48.42/23.17 tff(a1972, type, a1972: $i). % 48.42/23.17 tff(a2021, type, a2021: $i). % 48.42/23.17 tff(a1950, type, a1950: $i). % 48.42/23.17 tff(a1888, type, a1888: $i). % 48.42/23.17 tff(a1962, type, a1962: $i). % 48.42/23.17 tff(a1924, type, a1924: $i). % 48.42/23.17 tff(a1915, type, a1915: $i). % 48.42/23.17 tff(a1956, type, a1956: $i). % 48.42/23.17 tff(a1961, type, a1961: $i). % 48.42/23.17 tff(a1970, type, a1970: $i). % 48.42/23.17 tff(a1891, type, a1891: $i). % 48.42/23.17 tff(c1_0, type, c1_0: $o). % 48.42/23.17 tff(c8_1, type, c8_1: $i > $o). % 48.42/23.17 tff(a1902, type, a1902: $i). % 48.42/23.17 tff(a2032, type, a2032: $i). % 48.42/23.17 tff(a1838, type, a1838: $i). % 48.42/23.17 tff(a1935, type, a1935: $i). % 48.42/23.17 tff(c2_1, type, c2_1: $i > $o). % 48.42/23.17 tff(a1854, type, a1854: $i). % 48.42/23.17 tff(a1922, type, a1922: $i). % 48.42/23.17 tff(a1835, type, a1835: $i). % 48.42/23.17 tff(a1930, type, a1930: $i). % 48.42/23.17 tff(a1925, type, a1925: $i). % 48.42/23.17 tff(ndr1_1, type, ndr1_1: $i > $o). % 48.42/23.17 tff(c2_0, type, c2_0: $o). % 48.42/23.17 tff(c4_1, type, c4_1: $i > $o). % 48.42/23.17 tff(a1843, type, a1843: $i). % 48.42/23.17 tff(a1896, type, a1896: $i). % 48.42/23.17 tff(a1884, type, a1884: $i). % 48.42/23.17 tff(a1873, type, a1873: $i). % 48.42/23.17 tff(a1938, type, a1938: $i). % 48.42/23.17 tff(a1856, type, a1856: $i). % 48.42/23.17 tff(a1883, type, a1883: $i). % 48.42/23.17 tff(a2030, type, a2030: $i). % 48.42/23.17 tff(a1893, type, a1893: $i). % 48.42/23.17 tff(a1867, type, a1867: $i). % 48.42/23.17 tff(a1941, type, a1941: $i). % 48.42/23.17 tff(a2020, type, a2020: $i). % 48.42/23.17 tff(a1861, type, a1861: $i). % 48.42/23.17 tff(a1878, type, a1878: $i). % 48.42/23.17 tff(c9_1, type, c9_1: $i > $o). % 48.42/23.17 tff(a1885, type, a1885: $i). % 48.42/23.17 tff(c10_1, type, c10_1: $i > $o). % 48.42/23.17 tff(c10_0, type, c10_0: $o). % 48.42/23.17 tff(a1869, type, a1869: $i). % 48.42/23.17 tff(a1859, type, a1859: $i). % 48.42/23.17 tff(a1870, type, a1870: $i). % 48.42/23.17 tff(a1993, type, a1993: $i). % 48.42/23.17 tff(c6_2, type, c6_2: ($i * $i) > $o). % 48.42/23.17 tff(a2029, type, a2029: $i). % 48.42/23.17 tff(a1983, type, a1983: $i). % 48.42/23.17 tff(a1917, type, a1917: $i). % 48.42/23.17 tff(a1906, type, a1906: $i). % 48.42/23.17 tff(a1955, type, a1955: $i). % 48.42/23.17 tff(a1919, type, a1919: $i). % 48.42/23.17 tff(a2027, type, a2027: $i). % 48.42/23.17 tff(a1928, type, a1928: $i). % 48.42/23.17 tff(a2003, type, a2003: $i). % 48.42/23.17 tff(a1942, type, a1942: $i). % 48.42/23.17 tff(a1945, type, a1945: $i). % 48.42/23.17 tff(a1857, type, a1857: $i). % 48.42/23.17 tff(a1976, type, a1976: $i). % 48.42/23.17 tff(a1988, type, a1988: $i). % 48.42/23.17 tff(a1963, type, a1963: $i). % 48.42/23.17 tff(ndr1_0, type, ndr1_0: $o). % 48.42/23.17 tff(a1933, type, a1933: $i). % 48.42/23.17 tff(a1881, type, a1881: $i). % 48.42/23.17 tff(a1940, type, a1940: $i). % 48.42/23.17 tff(a1862, type, a1862: $i). % 48.42/23.17 tff(a1908, type, a1908: $i). % 48.42/23.17 tff(c9_2, type, c9_2: ($i * $i) > $o). % 48.42/23.17 tff(a1985, type, a1985: $i). % 48.42/23.17 tff(a1948, type, a1948: $i). % 48.42/23.17 tff(a1909, type, a1909: $i). % 48.42/23.17 tff(c10_2, type, c10_2: ($i * $i) > $o). % 48.42/23.17 tff(a1876, type, a1876: $i). % 48.42/23.17 tff(a1994, type, a1994: $i). % 48.42/23.17 tff(a1991, type, a1991: $i). % 48.42/23.17 tff(a1868, type, a1868: $i). % 48.42/23.17 tff(a1966, type, a1966: $i). % 48.42/23.17 tff(a1877, type, a1877: $i). % 48.42/23.17 tff(c1_1, type, c1_1: $i > $o). % 48.42/23.17 tff(a1889, type, a1889: $i). % 48.42/23.17 tff(a1971, type, a1971: $i). % 48.42/23.17 tff(a1923, type, a1923: $i). % 48.42/23.17 tff(a1987, type, a1987: $i). % 48.42/23.17 tff(a1921, type, a1921: $i). % 48.42/23.17 tff(a1899, type, a1899: $i). % 48.42/23.17 tff(c5_2, type, c5_2: ($i * $i) > $o). % 48.42/23.17 tff(a1846, type, a1846: $i). % 48.42/23.17 tff(c9_0, type, c9_0: $o). % 48.42/23.17 tff(a2004, type, a2004: $i). % 48.42/23.17 tff(a1954, type, a1954: $i). % 48.42/23.17 tff(c7_1, type, c7_1: $i > $o). % 48.42/23.17 tff(a1964, type, a1964: $i). % 48.42/23.17 tff(c6_1, type, c6_1: $i > $o). % 48.42/23.17 tff(a1911, type, a1911: $i). % 48.42/23.17 tff(a1990, type, a1990: $i). % 48.42/23.17 tff(a1953, type, a1953: $i). % 48.42/23.17 tff(a1998, type, a1998: $i). % 48.42/23.17 tff(a1865, type, a1865: $i). % 48.42/23.17 tff(c4_2, type, c4_2: ($i * $i) > $o). % 48.42/23.17 tff(a1860, type, a1860: $i). % 48.42/23.17 tff(a1834, type, a1834: $i). % 48.42/23.17 tff(a2014, type, a2014: $i). % 48.42/23.17 tff(a2005, type, a2005: $i). % 48.42/23.17 tff(a2008, type, a2008: $i). % 48.42/23.17 tff(a1900, type, a1900: $i). % 48.42/23.17 tff(a1918, type, a1918: $i). % 48.42/23.17 tff(a2013, type, a2013: $i). % 48.42/23.17 tff(c5_1, type, c5_1: $i > $o). % 48.42/23.17 tff(a1977, type, a1977: $i). % 48.42/23.17 tff(a1978, type, a1978: $i). % 48.42/23.17 tff(a1952, type, a1952: $i). % 48.42/23.17 tff(a1901, type, a1901: $i). % 48.42/23.17 tff(c7_2, type, c7_2: ($i * $i) > $o). % 48.42/23.17 tff(a1980, type, a1980: $i). % 48.42/23.17 tff(c3_2, type, c3_2: ($i * $i) > $o). % 48.42/23.17 tff(a1844, type, a1844: $i). % 48.42/23.17 tff(a1880, type, a1880: $i). % 48.42/23.17 tff(a1949, type, a1949: $i). % 48.42/23.17 tff(a1957, type, a1957: $i). % 48.42/23.17 tff(c2_2, type, c2_2: ($i * $i) > $o). % 48.42/23.17 tff(a1937, type, a1937: $i). % 48.42/23.17 tff(a2023, type, a2023: $i). % 48.42/23.17 tff(a1986, type, a1986: $i). % 48.42/23.17 tff(a1907, type, a1907: $i). % 48.42/23.17 tff(a1997, type, a1997: $i). % 48.42/23.17 tff(a1958, type, a1958: $i). % 48.42/23.17 tff(a2006, type, a2006: $i). % 48.42/23.17 tff(a1974, type, a1974: $i). % 48.42/23.17 tff(a1913, type, a1913: $i). % 48.42/23.17 tff(c3_1, type, c3_1: $i > $o). % 48.42/23.17 % 48.42/23.17 %Saturated clause set: % 48.42/23.18 tff(c_14658, plain, (~c6_1(a1841))). % 48.42/23.18 tff(c_14657, plain, (~c6_1(a1931))). % 48.42/23.18 tff(c_14609, plain, (~c6_1(a1945))). % 48.42/23.18 tff(c_14656, plain, (~c6_1(a1935))). % 48.42/23.18 tff(c_14632, plain, (~c6_1(a1906))). % 48.42/23.18 tff(c_14641, plain, (~c6_1(a1939))). % 48.42/23.18 tff(c_14655, plain, (~c6_1(a1986))). % 48.42/23.18 tff(c_14638, plain, (~c6_1(a2014))). % 48.42/23.18 tff(c_14616, plain, (~c6_1(a1967))). % 48.42/23.18 tff(c_14623, plain, (~c6_1(a1924))). % 48.42/23.18 tff(c_14635, plain, (~c6_1(a1845))). % 48.42/23.18 tff(c_14654, plain, (~c6_1(a1896))). % 48.42/23.18 tff(c_14647, plain, (~c6_1(a2029))). % 48.42/23.18 tff(c_14644, plain, (~c6_1(a2017))). % 48.42/23.18 tff(c_14653, plain, (~c6_1(a1976))). % 48.42/23.18 tff(c_14650, plain, (~c6_1(a1913))). % 48.42/23.18 tff(c_14612, plain, (~c6_1(a1952))). % 48.42/23.18 tff(c_14628, plain, (~c6_1(a1851))). % 48.66/23.18 tff(c_14620, plain, (~c6_1(a1899))). % 48.66/23.18 tff(c_14540, plain, (![X92_123]: (c9_1(X92_123) | c5_1(X92_123) | ~c6_1(X92_123)))). % 48.66/23.18 tff(c_14538, plain, (c8_2(a1976, a1977))). % 48.66/23.18 tff(c_14536, plain, (~c7_1(a1976))). % 48.66/23.18 tff(c_14529, plain, (~c5_2(a1976, a1977))). % 48.66/23.18 tff(c_14528, plain, (~c6_2(a1976, a1977))). % 48.66/23.19 tff(c_14527, plain, (~c2_2(a1988, a1989))). % 48.66/23.19 tff(c_14472, plain, (c7_2(a1976, a1977))). % 48.66/23.19 tff(c_14370, plain, (![X158_208]: (~c1_2(a1988, X158_208) | ~c2_2(a1988, X158_208) | ~c5_2(a1988, X158_208)))). % 48.66/23.19 tff(c_14336, plain, (![X194_253]: (c3_2(X194_253, a1954) | c1_2(X194_253, a1953) | c10_2(X194_253, a2024) | ~c10_2(X194_253, a1953) | ~c4_1(X194_253) | ~c5_1(X194_253) | c3_2(X194_253, a1953) | ~ndr1_1(X194_253) | ~c7_1(X194_253) | c4_2(X194_253, a1953)))). % 48.66/23.19 tff(c_14365, plain, (~c9_1(a1976))). % 48.66/23.19 tff(c_12332, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c10_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.66/23.19 tff(c_12460, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c10_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.66/23.19 tff(c_14271, plain, (ndr1_1(a1976))). % 48.66/23.19 tff(c_12704, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.66/23.19 tff(c_14269, plain, (~c1_1(a1976))). % 48.66/23.19 tff(c_14268, plain, (~c7_1(a1896))). % 48.66/23.19 tff(c_14260, plain, (~c5_2(a1896, a1897))). % 48.66/23.19 tff(c_14205, plain, (c7_2(a1896, a1897))). % 48.70/23.19 tff(c_14160, plain, (![X194_253]: (c10_2(X194_253, a1954) | c1_2(X194_253, a1953) | c10_2(X194_253, a2024) | ~c10_2(X194_253, a1953) | ~c4_1(X194_253) | ~c5_1(X194_253) | c3_2(X194_253, a1953) | ~ndr1_1(X194_253) | ~c7_1(X194_253) | c4_2(X194_253, a1953)))). % 48.70/23.19 tff(c_14203, plain, (~c3_2(a1896, a1897))). % 48.70/23.19 tff(c_14190, plain, (c6_2(a1896, a1897))). % 48.70/23.19 tff(c_11715, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c10_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.19 tff(c_12189, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c3_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.19 tff(c_14096, plain, (~c2_2(a1896, a1897))). % 48.70/23.19 tff(c_14065, plain, (![X194_253]: (c10_2(X194_253, a1954) | c1_2(X194_253, a1953) | c3_2(X194_253, a2024) | ~c10_2(X194_253, a1953) | ~c4_1(X194_253) | ~c5_1(X194_253) | c3_2(X194_253, a1953) | ~ndr1_1(X194_253) | ~c7_1(X194_253) | c4_2(X194_253, a1953)))). % 48.70/23.19 tff(c_11990, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c3_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.19 tff(c_11920, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c10_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.19 tff(c_13967, plain, (~c9_1(a1896))). % 48.70/23.19 tff(c_12061, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c3_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.19 tff(c_11863, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c10_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.19 tff(c_13864, plain, (ndr1_1(a1896))). % 48.70/23.20 tff(c_13066, plain, (![X194_253, X195_255]: (~c6_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_12118, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c3_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_12946, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_13746, plain, (![X194_253]: (c3_2(X194_253, a1954) | c1_2(X194_253, a1953) | c3_2(X194_253, a2024) | ~c10_2(X194_253, a1953) | ~c4_1(X194_253) | ~c5_1(X194_253) | c3_2(X194_253, a1953) | ~ndr1_1(X194_253) | ~c7_1(X194_253) | c4_2(X194_253, a1953)))). % 48.70/23.20 tff(c_12259, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c3_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_13006, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_12886, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_12522, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c10_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_13645, plain, (~c4_1(a1988))). % 48.70/23.20 tff(c_13531, plain, (c5_2(a1988, a1989))). % 48.70/23.20 tff(c_12390, plain, (![X194_253, X195_255]: (c4_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | c3_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_13188, plain, (![X194_253, X195_255]: (~c6_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_12764, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_13128, plain, (![X194_253, X195_255]: (c10_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_12826, plain, (![X194_253, X195_255]: (~c6_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, X195_255) | ~c6_2(X194_253, a2024) | ~c10_2(X194_253, X195_255) | ~c4_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.70/23.20 tff(c_11864, plain, (![X122_163]: (c10_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | c10_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.70/23.20 tff(c_12947, plain, (![X122_163]: (c10_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.70/23.20 tff(c_12765, plain, (![X122_163]: (c10_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.70/23.20 tff(c_12260, plain, (![X122_163]: (c4_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | c3_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.70/23.20 tff(c_11991, plain, (![X122_163]: (c4_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | c3_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.70/23.20 tff(c_12119, plain, (![X122_163]: (c10_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | c3_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.20 tff(c_13067, plain, (![X122_163]: (~c6_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.20 tff(c_13007, plain, (![X122_163]: (c4_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.20 tff(c_12523, plain, (![X122_163]: (c4_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | c10_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_12827, plain, (![X122_163]: (~c6_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_12190, plain, (![X122_163]: (c10_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | c3_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_12887, plain, (![X122_163]: (c4_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_13129, plain, (![X122_163]: (c10_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_11921, plain, (![X122_163]: (c10_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | c10_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_13189, plain, (![X122_163]: (~c6_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_12705, plain, (![X122_163]: (c4_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | ~c6_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_12333, plain, (![X122_163]: (c4_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | c10_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.76/23.21 tff(c_12644, plain, (![X196_468, X197_469]: (~c6_2(X196_468, a1953) | c5_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12643, plain, (![X196_468, X197_469]: (c10_2(X196_468, a1953) | c10_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12645, plain, (![X196_468, X197_469]: (~c6_2(X196_468, a1953) | c10_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12646, plain, (![X196_468, X197_469]: (c4_2(X196_468, a1953) | c10_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12639, plain, (![X196_468, X197_469]: (c10_2(X196_468, a1953) | c3_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12640, plain, (![X196_468, X197_469]: (c4_2(X196_468, a1953) | c3_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12641, plain, (![X196_468, X197_469]: (~c6_2(X196_468, a1953) | c3_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12642, plain, (![X196_468, X197_469]: (c10_2(X196_468, a1953) | c5_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12638, plain, (![X196_468, X197_469]: (c4_2(X196_468, a1953) | c5_2(X196_468, a1954) | ~c5_2(X196_468, X197_469) | c1_2(X196_468, X197_469) | ~c6_2(X196_468, a2024) | c4_2(X196_468, X197_469) | ~c10_2(X196_468, X197_469) | ~ndr1_1(X196_468) | ~c4_1(X196_468)))). % 48.76/23.21 tff(c_12591, plain, (![X196_256, X197_258]: (~c6_2(X196_256, a2024) | c4_2(X196_256, X197_258) | ~c10_2(X196_256, X197_258) | c7_2(X196_256, X197_258) | ~ndr1_1(X196_256) | ~c4_1(X196_256)))). % 48.76/23.21 tff(c_12062, plain, (![X122_163]: (c10_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | c3_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.21 tff(c_11716, plain, (![X122_163]: (c4_2(X122_163, a1953) | c10_2(X122_163, a1954) | c1_2(X122_163, a1955) | c10_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.21 tff(c_12461, plain, (![X122_163]: (c10_2(X122_163, a1953) | c3_2(X122_163, a1954) | c1_2(X122_163, a1955) | c10_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.21 tff(c_12391, plain, (![X122_163]: (c4_2(X122_163, a1953) | c5_2(X122_163, a1954) | c1_2(X122_163, a1955) | c3_2(X122_163, a2024) | c4_2(X122_163, a1955) | ~c10_2(X122_163, a1955) | ~ndr1_1(X122_163) | ~c4_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.21 tff(c_11637, plain, (![X196_424, X197_425]: (c4_2(X196_424, a1953) | c5_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11643, plain, (![X196_424, X197_425]: (~c6_2(X196_424, a1953) | c5_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11644, plain, (![X196_424, X197_425]: (~c6_2(X196_424, a1953) | c10_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11790, plain, (![X196_428, X197_429]: (~c6_2(X196_428, a1953) | c3_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11638, plain, (![X196_424, X197_425]: (c10_2(X196_424, a1953) | c3_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11787, plain, (![X196_428, X197_429]: (c4_2(X196_428, a1953) | c5_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11640, plain, (![X196_424, X197_425]: (~c6_2(X196_424, a1953) | c3_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11639, plain, (![X196_424, X197_425]: (c4_2(X196_424, a1953) | c3_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11794, plain, (![X196_428, X197_429]: (~c6_2(X196_428, a1953) | c10_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11789, plain, (![X196_428, X197_429]: (c4_2(X196_428, a1953) | c3_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11788, plain, (![X196_428, X197_429]: (c10_2(X196_428, a1953) | c3_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_12137, plain, (~c3_2(a1988, a1989))). % 48.79/23.21 tff(c_11791, plain, (![X196_428, X197_429]: (c10_2(X196_428, a1953) | c5_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11792, plain, (![X196_428, X197_429]: (c10_2(X196_428, a1953) | c10_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11793, plain, (![X196_428, X197_429]: (~c6_2(X196_428, a1953) | c5_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11795, plain, (![X196_428, X197_429]: (c4_2(X196_428, a1953) | c10_2(X196_428, a1954) | ~c5_2(X196_428, X197_429) | c1_2(X196_428, X197_429) | c3_2(X196_428, a2024) | c4_2(X196_428, X197_429) | ~c10_2(X196_428, X197_429) | ~ndr1_1(X196_428) | ~c4_1(X196_428)))). % 48.79/23.21 tff(c_11641, plain, (![X196_424, X197_425]: (c10_2(X196_424, a1953) | c5_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.21 tff(c_11642, plain, (![X196_424, X197_425]: (c10_2(X196_424, a1953) | c10_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.22 tff(c_11740, plain, (![X196_256, X197_258]: (c3_2(X196_256, a2024) | c4_2(X196_256, X197_258) | ~c10_2(X196_256, X197_258) | c7_2(X196_256, X197_258) | ~ndr1_1(X196_256) | ~c4_1(X196_256)))). % 48.79/23.22 tff(c_11737, plain, (~c4_1(a2001))). % 48.79/23.22 tff(c_11736, plain, (~c4_1(a1995))). % 48.79/23.22 tff(c_11735, plain, (~c4_1(a1917))). % 48.79/23.22 tff(c_11734, plain, (~c4_1(a1933))). % 48.79/23.22 tff(c_11645, plain, (![X196_424, X197_425]: (c4_2(X196_424, a1953) | c10_2(X196_424, a1954) | ~c5_2(X196_424, X197_425) | c1_2(X196_424, X197_425) | c10_2(X196_424, a2024) | c4_2(X196_424, X197_425) | ~c10_2(X196_424, X197_425) | ~ndr1_1(X196_424) | ~c4_1(X196_424)))). % 48.79/23.22 tff(c_11663, plain, (~c4_1(a1841))). % 48.79/23.22 tff(c_11662, plain, (~c4_1(a1865))). % 48.79/23.22 tff(c_11590, plain, (![X196_256, X197_258]: (c10_2(X196_256, a2024) | c4_2(X196_256, X197_258) | ~c10_2(X196_256, X197_258) | c7_2(X196_256, X197_258) | ~ndr1_1(X196_256) | ~c4_1(X196_256)))). % 48.79/23.22 tff(c_11587, plain, (~c6_2(a1988, a1989))). % 48.79/23.22 tff(c_11586, plain, (c3_1(a1988))). % 48.79/23.22 tff(c_11582, plain, (~c5_1(a1988))). % 48.79/23.22 tff(c_11581, plain, (ndr1_1(a1988))). % 48.79/23.22 tff(c_11580, plain, (~c1_1(a1945))). % 48.79/23.22 tff(c_11579, plain, (c8_1(a1945))). % 48.79/23.22 tff(c_11578, plain, (c3_1(a1945))). % 48.79/23.22 tff(c_11572, plain, (~c5_1(a1945))). % 48.79/23.22 tff(c_11567, plain, (~c10_1(a1945))). % 48.79/23.22 tff(c_11568, plain, (~c9_1(a1945))). % 48.79/23.22 tff(c_11542, plain, (~ndr1_1(a1945))). % 48.79/23.22 tff(c_10487, plain, (![X194_253]: (c4_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c2_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11536, plain, (![X194_421]: (c4_2(X194_421, a1953) | c10_2(X194_421, a1954) | c1_2(X194_421, a2009) | c3_2(X194_421, a2008) | ~c9_1(X194_421) | ~c5_1(X194_421) | c3_2(X194_421, a2009) | ~ndr1_1(X194_421) | ~c7_1(X194_421)))). % 48.79/23.22 tff(c_10458, plain, (![X194_253]: (c4_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, a2009) | c3_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11502, plain, (![X194_418]: (c10_2(X194_418, a1953) | c10_2(X194_418, a1954) | c1_2(X194_418, a2009) | ~c2_2(X194_418, a2008) | ~c9_1(X194_418) | ~c5_1(X194_418) | c3_2(X194_418, a2009) | ~ndr1_1(X194_418) | ~c7_1(X194_418)))). % 48.79/23.22 tff(c_10529, plain, (![X194_253]: (c10_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c2_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11485, plain, (![X194_415]: (c4_2(X194_415, a1953) | c3_2(X194_415, a1954) | c1_2(X194_415, a2009) | ~c2_2(X194_415, a2008) | ~c9_1(X194_415) | ~c5_1(X194_415) | c3_2(X194_415, a2009) | ~ndr1_1(X194_415) | ~c7_1(X194_415)))). % 48.79/23.22 tff(c_11454, plain, (![X194_413]: (c10_2(X194_413, a1953) | c10_2(X194_413, a1954) | c1_2(X194_413, a2009) | c3_2(X194_413, a2008) | ~c9_1(X194_413) | ~c5_1(X194_413) | c3_2(X194_413, a2009) | ~ndr1_1(X194_413) | ~c7_1(X194_413)))). % 48.79/23.22 tff(c_10548, plain, (![X194_253]: (c10_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, a2009) | c3_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_10446, plain, (![X194_253]: (c10_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c5_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_10538, plain, (![X194_253]: (c4_2(X194_253, a1953) | c10_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c5_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11408, plain, (![X194_408]: (c10_2(X194_408, a1953) | c3_2(X194_408, a1954) | c1_2(X194_408, a2009) | ~c2_2(X194_408, a2008) | ~c9_1(X194_408) | ~c5_1(X194_408) | c3_2(X194_408, a2009) | ~ndr1_1(X194_408) | ~c7_1(X194_408)))). % 48.79/23.22 tff(c_10440, plain, (![X194_253]: (c4_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c5_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11371, plain, (![X194_405]: (c10_2(X194_405, a1953) | c3_2(X194_405, a1954) | c1_2(X194_405, a2009) | c3_2(X194_405, a2008) | ~c9_1(X194_405) | ~c5_1(X194_405) | c3_2(X194_405, a2009) | ~ndr1_1(X194_405) | ~c7_1(X194_405)))). % 48.79/23.22 tff(c_11354, plain, (![X194_403]: (c4_2(X194_403, a1953) | c10_2(X194_403, a1954) | c1_2(X194_403, a2009) | ~c2_2(X194_403, a2008) | ~c9_1(X194_403) | ~c5_1(X194_403) | c3_2(X194_403, a2009) | ~ndr1_1(X194_403) | ~c7_1(X194_403)))). % 48.79/23.22 tff(c_10452, plain, (![X194_253]: (c10_2(X194_253, a1953) | c5_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c5_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11309, plain, (![X65_365]: (c2_1(X65_365) | ~c1_2(X65_365, a2009) | c5_1(X65_365) | ~c2_2(X65_365, a2008) | ~c9_1(X65_365) | ~c2_2(X65_365, a1909) | c10_2(X65_365, a2009) | ~ndr1_1(X65_365) | ~c8_1(X65_365)))). % 48.79/23.22 tff(c_11325, plain, (![X65_369]: (c2_1(X65_369) | ~c1_2(X65_369, a2009) | c5_1(X65_369) | c3_2(X65_369, a2008) | ~c9_1(X65_369) | c10_2(X65_369, a1909) | c10_2(X65_369, a2009) | ~ndr1_1(X65_369) | ~c8_1(X65_369)))). % 48.79/23.22 tff(c_11327, plain, (![X65_365]: (c2_1(X65_365) | ~c1_2(X65_365, a2009) | c5_1(X65_365) | c3_2(X65_365, a2008) | ~c9_1(X65_365) | ~c2_2(X65_365, a1909) | c10_2(X65_365, a2009) | ~ndr1_1(X65_365) | ~c8_1(X65_365)))). % 48.79/23.22 tff(c_11307, plain, (![X65_369]: (c2_1(X65_369) | ~c1_2(X65_369, a2009) | c5_1(X65_369) | ~c2_2(X65_369, a2008) | ~c9_1(X65_369) | c10_2(X65_369, a1909) | c10_2(X65_369, a2009) | ~ndr1_1(X65_369) | ~c8_1(X65_369)))). % 48.79/23.22 tff(c_11291, plain, (![X170_221]: (c2_1(X170_221) | ~c1_2(X170_221, a2009) | ~c3_2(X170_221, a2009) | ~ndr1_1(X170_221) | c5_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.22 tff(c_11290, plain, (![X170_221]: (c2_1(X170_221) | ~c1_2(X170_221, a2009) | ~c3_2(X170_221, a2009) | ~ndr1_1(X170_221) | c5_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.22 tff(c_11289, plain, (![X170_221]: (c2_1(X170_221) | ~c1_2(X170_221, a2009) | ~c3_2(X170_221, a2009) | ~ndr1_1(X170_221) | c5_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.22 tff(c_11292, plain, (![X186_243]: (c2_1(X186_243) | ~c1_2(X186_243, a2018) | ~c3_2(X186_243, a2018) | ~ndr1_1(X186_243) | c5_1(X186_243) | c10_1(X186_243) | c8_1(X186_243)))). % 48.79/23.22 tff(c_11275, plain, (![X75_103, X76_105]: (c2_1(X75_103) | ~c6_2(X75_103, X76_105) | ~c1_2(X75_103, X76_105) | ~c3_2(X75_103, X76_105) | ~ndr1_1(X75_103) | c5_1(X75_103)))). % 48.79/23.22 tff(c_10493, plain, (![X194_253]: (c4_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c5_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_10470, plain, (![X194_253]: (c10_2(X194_253, a1953) | c3_2(X194_253, a1954) | c1_2(X194_253, a2009) | ~c5_2(X194_253, a2008) | ~c9_1(X194_253) | ~c5_1(X194_253) | c4_2(X194_253, a2009) | c3_2(X194_253, a2009) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.22 tff(c_11260, plain, (c8_1(a1899))). % 48.79/23.22 tff(c_11259, plain, (~c10_1(a1899))). % 48.79/23.22 tff(c_11258, plain, (c3_1(a1899))). % 48.79/23.22 tff(c_11254, plain, (~c5_1(a1899))). % 48.79/23.22 tff(c_11225, plain, (~ndr1_1(a1899))). % 48.79/23.22 tff(c_11219, plain, (![X194_388]: (c4_2(X194_388, a1953) | c3_2(X194_388, a1954) | c1_2(X194_388, a2009) | c3_2(X194_388, a2008) | ~c9_1(X194_388) | ~c5_1(X194_388) | c3_2(X194_388, a2009) | ~ndr1_1(X194_388) | ~c7_1(X194_388)))). % 48.79/23.22 tff(c_11223, plain, (~c7_1(a1979))). % 48.79/23.22 tff(c_11203, plain, (~c1_1(a1952))). % 48.79/23.22 tff(c_11200, plain, (c3_1(a1952))). % 48.79/23.22 tff(c_11196, plain, (~c5_1(a1952))). % 48.79/23.22 tff(c_11194, plain, (c8_1(a1952))). % 48.79/23.22 tff(c_11189, plain, (~c9_1(a1952))). % 48.79/23.22 tff(c_11165, plain, (~ndr1_1(a1952))). % 48.79/23.22 tff(c_11131, plain, (![X89_120]: (~c3_2(X89_120, a1929) | ~c2_1(X89_120) | ~c5_1(X89_120)))). % 48.79/23.22 tff(c_11116, plain, (![X23_35]: (~c4_2(X23_35, a1873) | c4_1(X23_35) | ~c10_1(X23_35)))). % 48.79/23.22 tff(c_11110, plain, (![X89_120]: (~c9_2(X89_120, a1929) | ~c2_1(X89_120) | ~c5_1(X89_120)))). % 48.79/23.22 tff(c_11094, plain, (![X23_35]: (c3_2(X23_35, a1873) | c4_1(X23_35) | ~c10_1(X23_35)))). % 48.79/23.22 tff(c_11087, plain, (![X23_35]: (~c10_2(X23_35, a1873) | c4_1(X23_35) | ~c10_1(X23_35)))). % 48.79/23.22 tff(c_11084, plain, (c3_1(a1851))). % 48.79/23.22 tff(c_11080, plain, (~c5_1(a1851))). % 48.79/23.22 tff(c_11073, plain, (![X89_120]: (c8_2(X89_120, a1929) | ~c2_1(X89_120) | ~c5_1(X89_120)))). % 48.79/23.22 tff(c_11068, plain, (~c4_1(a1945))). % 48.79/23.22 tff(c_11045, plain, (![X65_379]: (c7_1(X65_379) | ~c2_2(X65_379, a2008) | ~c9_1(X65_379) | c10_2(X65_379, a1909) | c10_2(X65_379, a2009) | ~ndr1_1(X65_379) | ~c8_1(X65_379)))). % 48.79/23.22 tff(c_11064, plain, (~c3_1(a1846))). % 48.79/23.22 tff(c_11063, plain, (~c3_1(a1979))). % 48.79/23.23 tff(c_11061, plain, (~c3_1(a1869))). % 48.79/23.23 tff(c_11047, plain, (![X190_248]: (~c9_1(X190_248) | ~c10_1(X190_248) | ~c3_1(X190_248)))). % 48.79/23.23 tff(c_10990, plain, (![X65_369]: (~c2_2(X65_369, a2008) | ~c9_1(X65_369) | c10_2(X65_369, a1909) | c10_2(X65_369, a2009) | c3_2(X65_369, a2009) | ~ndr1_1(X65_369) | ~c8_1(X65_369)))). % 48.79/23.23 tff(c_11036, plain, (![X65_377]: (c7_1(X65_377) | c3_2(X65_377, a2008) | ~c9_1(X65_377) | c10_2(X65_377, a1909) | c10_2(X65_377, a2009) | ~ndr1_1(X65_377) | ~c8_1(X65_377)))). % 48.79/23.23 tff(c_10991, plain, (![X65_369]: (c3_2(X65_369, a2008) | ~c9_1(X65_369) | c10_2(X65_369, a1909) | c10_2(X65_369, a2009) | c3_2(X65_369, a2009) | ~ndr1_1(X65_369) | ~c8_1(X65_369)))). % 48.79/23.23 tff(c_11025, plain, (![X65_375]: (c7_1(X65_375) | ~c2_2(X65_375, a2008) | ~c9_1(X65_375) | ~c2_2(X65_375, a1909) | c10_2(X65_375, a2009) | ~ndr1_1(X65_375) | ~c8_1(X65_375)))). % 48.79/23.23 tff(c_10833, plain, (![X65_365]: (~c2_2(X65_365, a2008) | ~c9_1(X65_365) | ~c2_2(X65_365, a1909) | c10_2(X65_365, a2009) | c3_2(X65_365, a2009) | ~ndr1_1(X65_365) | ~c8_1(X65_365)))). % 48.79/23.23 tff(c_11015, plain, (![X65_373]: (c7_1(X65_373) | c3_2(X65_373, a2008) | ~c9_1(X65_373) | ~c2_2(X65_373, a1909) | c10_2(X65_373, a2009) | ~ndr1_1(X65_373) | ~c8_1(X65_373)))). % 48.79/23.23 tff(c_10834, plain, (![X65_365]: (c3_2(X65_365, a2008) | ~c9_1(X65_365) | ~c2_2(X65_365, a1909) | c10_2(X65_365, a2009) | c3_2(X65_365, a2009) | ~ndr1_1(X65_365) | ~c8_1(X65_365)))). % 48.79/23.23 tff(c_10956, plain, (![X65_90, X66_92]: (~c8_2(X65_90, a1909) | c10_2(X65_90, X66_92) | c3_2(X65_90, X66_92) | c4_2(X65_90, X66_92) | ~ndr1_1(X65_90) | ~c8_1(X65_90)))). % 48.79/23.23 tff(c_10903, plain, (![X65_90, X66_92]: (c10_2(X65_90, a1909) | c10_2(X65_90, X66_92) | c3_2(X65_90, X66_92) | c4_2(X65_90, X66_92) | ~ndr1_1(X65_90) | ~c8_1(X65_90)))). % 48.79/23.23 tff(c_10958, plain, (~c8_1(a1979))). % 48.79/23.23 tff(c_10957, plain, (~c8_1(a1865))). % 48.79/23.23 tff(c_10850, plain, (~c8_1(a1917))). % 48.79/23.23 tff(c_10849, plain, (~c8_1(a1900))). % 48.79/23.23 tff(c_10737, plain, (![X65_90, X66_92]: (~c2_2(X65_90, a1909) | c10_2(X65_90, X66_92) | c3_2(X65_90, X66_92) | c4_2(X65_90, X66_92) | ~ndr1_1(X65_90) | ~c8_1(X65_90)))). % 48.79/23.23 tff(c_10799, plain, (c3_1(a1906))). % 48.79/23.23 tff(c_10795, plain, (~c5_1(a1906))). % 48.79/23.23 tff(c_10783, plain, (~c2_1(a1963))). % 48.79/23.23 tff(c_10741, plain, (![X89_120]: (ndr1_1(X89_120) | ~c2_1(X89_120) | ~c5_1(X89_120)))). % 48.79/23.23 tff(c_10747, plain, (c3_1(a1967))). % 48.79/23.23 tff(c_10743, plain, (~c5_1(a1967))). % 48.79/23.23 tff(c_10742, plain, (c8_1(a1967))). % 48.79/23.23 tff(c_10738, plain, (~c1_1(a1967))). % 48.79/23.23 tff(c_10674, plain, (~c10_1(a1967))). % 48.79/23.23 tff(c_10669, plain, (~c9_1(a1967))). % 48.79/23.23 tff(c_10649, plain, (~ndr1_1(a1967))). % 48.79/23.23 tff(c_10602, plain, (![X164_215]: (~c9_1(X164_215) | c10_2(X164_215, a1927) | c2_2(X164_215, a1994) | c8_2(X164_215, a1994) | ~ndr1_1(X164_215) | c2_1(X164_215) | ~c1_1(X164_215) | ~c10_1(X164_215) | c4_1(X164_215)))). % 48.79/23.23 tff(c_10587, plain, (![X85_116, X105_359]: (~c9_1(X85_116) | c10_2(X85_116, a1927) | c2_2(X85_116, X105_359) | c8_2(X85_116, X105_359) | ~c9_2(X85_116, X105_359) | ~ndr1_1(X85_116) | c2_1(X85_116) | ~c1_1(X85_116)))). % 48.79/23.23 tff(c_10589, plain, (~c9_1(a1931))). % 48.79/23.23 tff(c_10588, plain, (c10_2(a1846, a1847))). % 48.79/23.23 tff(c_10573, plain, (![X104_138, X106_142, X105_141]: (~c9_1(X104_138) | ~c1_2(X104_138, X106_142) | c10_2(X104_138, X106_142) | c2_2(X104_138, X105_141) | c8_2(X104_138, X105_141) | ~c9_2(X104_138, X105_141) | ~ndr1_1(X104_138)))). % 48.79/23.23 tff(c_9951, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10113, plain, (![X170_221]: (c10_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_9950, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_9858, plain, (![X170_221]: (c4_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10009, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10008, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10207, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10111, plain, (![X170_221]: (c10_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10007, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_9859, plain, (![X170_221]: (c4_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_9952, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10066, plain, (![X170_221]: (c10_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_9857, plain, (![X170_221]: (c4_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10252, plain, (![X170_221]: (c4_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10251, plain, (![X170_221]: (c4_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10345, plain, (![X170_221]: (c4_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10206, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10208, plain, (![X170_221]: (~c6_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10068, plain, (![X170_221]: (c10_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10298, plain, (![X170_221]: (c10_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10250, plain, (![X170_221]: (c4_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10347, plain, (![X170_221]: (c4_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10112, plain, (![X170_221]: (c10_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10067, plain, (![X170_221]: (c10_2(X170_221, a1953) | c10_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10346, plain, (![X170_221]: (c4_2(X170_221, a1953) | c5_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c5_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10299, plain, (![X170_221]: (c10_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | c3_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10297, plain, (![X170_221]: (c10_2(X170_221, a1953) | c3_2(X170_221, a1954) | ~c5_2(X170_221, a2009) | c1_2(X170_221, a2009) | ~ndr1_1(X170_221) | ~c2_2(X170_221, a2008) | ~c9_1(X170_221)))). % 48.79/23.23 tff(c_10422, plain, (c5_2(a1917, a1918))). % 48.79/23.23 tff(c_10419, plain, (~c10_2(a1869, a1870))). % 48.79/23.23 tff(c_10416, plain, (~c9_2(a1869, a1870))). % 48.79/23.23 tff(c_10413, plain, (~c6_2(a1858, a1859))). % 48.79/23.23 tff(c_10410, plain, (~c3_2(a1960, a1961))). % 48.79/23.23 tff(c_10404, plain, (![X164_215]: (~c10_2(X164_215, a1994) | ~c10_1(X164_215) | c4_1(X164_215)))). % 48.79/23.23 tff(c_10400, plain, (~c1_1(a1917))). % 48.79/23.23 tff(c_10392, plain, (c2_2(a1917, a1918))). % 48.79/23.23 tff(c_10388, plain, (~c10_2(a1858, a1859))). % 48.79/23.23 tff(c_10385, plain, (~c10_2(a1960, a1961))). % 48.79/23.23 tff(c_10382, plain, (~c4_2(a1917, a1918))). % 48.79/23.23 tff(c_10379, plain, (~c2_2(a1869, a1870))). % 48.79/23.23 tff(c_10376, plain, (c4_2(a1858, a1859))). % 48.79/23.23 tff(c_10372, plain, (![X164_215]: (c9_2(X164_215, a1994) | ~c10_1(X164_215) | c4_1(X164_215)))). % 48.79/23.23 tff(c_10369, plain, (~c10_1(a1960))). % 48.79/23.23 tff(c_10366, plain, (c8_1(a1858))). % 48.79/23.23 tff(c_10319, plain, (![X120_160, X121_162]: (c4_2(X120_160, a1953) | c5_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_10317, plain, (ndr1_1(a1869))). % 48.79/23.24 tff(c_10271, plain, (![X120_160, X121_162]: (c10_2(X120_160, a1953) | c3_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_10269, plain, (c3_2(a1915, a1954))). % 48.79/23.24 tff(c_10224, plain, (![X120_160, X121_162]: (c4_2(X120_160, a1953) | c3_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_10180, plain, (![X120_160, X121_162]: (~c6_2(X120_160, a1953) | c3_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_10179, plain, (~c10_1(a2014))). % 48.79/23.24 tff(c_10177, plain, (c4_1(a2029))). % 48.79/23.24 tff(c_10173, plain, (c4_1(a1939))). % 48.79/23.24 tff(c_10135, plain, (![X164_215]: (ndr1_1(X164_215) | ~c10_1(X164_215) | c4_1(X164_215)))). % 48.79/23.24 tff(c_10132, plain, (c4_1(a1869))). % 48.79/23.24 tff(c_10129, plain, (c5_2(a1915, a1954))). % 48.79/23.24 tff(c_10085, plain, (![X120_160, X121_162]: (c10_2(X120_160, a1953) | c5_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_10040, plain, (![X120_160, X121_162]: (c10_2(X120_160, a1953) | c10_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_10039, plain, (ndr1_1(a1858))). % 48.79/23.24 tff(c_10031, plain, (c9_1(a1869))). % 48.79/23.24 tff(c_10025, plain, (~c6_2(a1915, a1953))). % 48.79/23.24 tff(c_9981, plain, (![X120_160, X121_162]: (~c6_2(X120_160, a1953) | c5_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_9976, plain, (ndr1_1(a1960))). % 48.79/23.24 tff(c_9971, plain, (~c10_1(a1858))). % 48.79/23.24 tff(c_9924, plain, (![X120_160, X121_162]: (~c6_2(X120_160, a1953) | c10_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_9922, plain, (c7_1(a1917))). % 48.79/23.24 tff(c_9919, plain, (~c1_1(a1899))). % 48.79/23.24 tff(c_9918, plain, (~c9_1(a1899))). % 48.79/23.24 tff(c_9917, plain, (c3_1(a1960))). % 48.79/23.24 tff(c_9913, plain, (~c5_1(a1960))). % 48.79/23.24 tff(c_9909, plain, (~c1_1(a1924))). % 48.79/23.24 tff(c_9908, plain, (c8_1(a1924))). % 48.79/23.24 tff(c_9906, plain, (~c10_1(a1924))). % 48.79/23.24 tff(c_9901, plain, (~c9_1(a1924))). % 48.79/23.24 tff(c_9885, plain, (~ndr1_1(a1924))). % 48.79/23.24 tff(c_9877, plain, (~c5_2(a2006, a2007))). % 48.79/23.24 tff(c_9876, plain, (c10_2(a1915, a1954))). % 48.79/23.24 tff(c_9875, plain, (c1_2(a1846, a1847))). % 48.79/23.24 tff(c_9831, plain, (![X120_160, X121_162]: (c4_2(X120_160, a1953) | c10_2(X120_160, a1954) | ~c7_2(X120_160, X121_162) | ~c5_2(X120_160, X121_162) | c1_2(X120_160, X121_162) | ~ndr1_1(X120_160)))). % 48.79/23.24 tff(c_9830, plain, (ndr1_1(a1917))). % 48.79/23.24 tff(c_9817, plain, (![X170_221]: (~c2_2(X170_221, a2008) | ~c4_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9795, plain, (![X170_221]: (~c2_2(X170_221, a2008) | c7_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9784, plain, (![X170_221]: (~c5_2(X170_221, a2008) | ~c4_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9778, plain, (![X170_304]: (~c3_2(X170_304, a2009) | ~ndr1_1(X170_304) | c7_1(X170_304) | ~c2_2(X170_304, a2008) | ~c9_1(X170_304)))). % 48.79/23.24 tff(c_9773, plain, (![X170_221]: (~c2_2(X170_221, a2008) | c6_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9768, plain, (![X170_221]: (c3_2(X170_221, a2008) | ~c4_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9745, plain, (![X170_221]: (~c5_2(X170_221, a2008) | c7_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9733, plain, (c8_1(a1963))). % 48.79/23.24 tff(c_9732, plain, (~c1_1(a1963))). % 48.79/23.24 tff(c_9731, plain, (~c10_1(a1963))). % 48.79/23.24 tff(c_9728, plain, (c4_1(a1963))). % 48.79/23.24 tff(c_9724, plain, (~c9_1(a1963))). % 48.79/23.24 tff(c_9708, plain, (~ndr1_1(a1963))). % 48.79/23.24 tff(c_9705, plain, (![X170_300]: (~c3_2(X170_300, a2009) | ~ndr1_1(X170_300) | c7_1(X170_300) | c3_2(X170_300, a2008) | ~c9_1(X170_300)))). % 48.79/23.24 tff(c_9700, plain, (![X170_221]: (c3_2(X170_221, a2008) | c6_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9696, plain, (~c4_2(a1979, a2009))). % 48.79/23.24 tff(c_9695, plain, (~c9_1(a1851))). % 48.79/23.24 tff(c_9693, plain, (~c9_1(a1841))). % 48.79/23.24 tff(c_9674, plain, (![X170_221]: (c3_2(X170_221, a2008) | c7_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9637, plain, (![X170_297]: (~c3_2(X170_297, a2009) | ~ndr1_1(X170_297) | c7_1(X170_297) | ~c5_2(X170_297, a2008) | ~c9_1(X170_297)))). % 48.79/23.24 tff(c_9632, plain, (![X170_221]: (~c5_2(X170_221, a2008) | c6_2(X170_221, a2009) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9619, plain, (~c1_1(a1906))). % 48.79/23.24 tff(c_9618, plain, (c8_1(a1906))). % 48.79/23.24 tff(c_9617, plain, (~c10_1(a1906))). % 48.79/23.24 tff(c_9611, plain, (~c9_1(a1906))). % 48.79/23.24 tff(c_9595, plain, (~ndr1_1(a1906))). % 48.79/23.24 tff(c_9589, plain, (~c10_1(a1952))). % 48.79/23.24 tff(c_9581, plain, (~c7_1(a1871))). % 48.79/23.24 tff(c_9561, plain, (![X194_253, X195_255]: (~c5_1(X194_253) | c4_2(X194_253, X195_255) | c3_2(X194_253, X195_255) | c5_2(X194_253, X195_255) | ~ndr1_1(X194_253) | ~c7_1(X194_253)))). % 48.79/23.24 tff(c_9507, plain, (![X151_200]: (~c10_2(a1979, X151_200) | ~c4_2(a1979, X151_200) | ~c7_2(a1979, X151_200)))). % 48.79/23.24 tff(c_9506, plain, (ndr1_1(a1979))). % 48.79/23.24 tff(c_9480, plain, (![X186_243]: (~c3_2(X186_243, a2018) | ~ndr1_1(X186_243) | c7_1(X186_243) | c10_1(X186_243) | c8_1(X186_243)))). % 48.79/23.24 tff(c_9475, plain, (![X137_180, X138_182]: (~c3_2(X137_180, X138_182) | ~c6_2(X137_180, X138_182) | ~ndr1_1(X137_180) | c7_1(X137_180)))). % 48.79/23.24 tff(c_9459, plain, (c3_1(a1845))). % 48.79/23.24 tff(c_9455, plain, (~c5_1(a1845))). % 48.79/23.24 tff(c_9454, plain, (c2_1(a1845))). % 48.79/23.24 tff(c_9451, plain, (c8_1(a1845))). % 48.79/23.24 tff(c_9446, plain, (~c9_1(a1845))). % 48.79/23.24 tff(c_9430, plain, (~ndr1_1(a1845))). % 48.79/23.24 tff(c_9426, plain, (c8_1(a2014))). % 48.79/23.24 tff(c_9424, plain, (c3_1(a2014))). % 48.79/23.24 tff(c_9420, plain, (~c5_1(a2014))). % 48.79/23.24 tff(c_9414, plain, (~c9_1(a2014))). % 48.79/23.24 tff(c_9398, plain, (~ndr1_1(a2014))). % 48.79/23.24 tff(c_9395, plain, (c7_2(a1931, a1932))). % 48.79/23.24 tff(c_9391, plain, (~c5_2(a1871, a1872))). % 48.79/23.24 tff(c_9378, plain, (~c2_2(a1871, a1872))). % 48.79/23.24 tff(c_9376, plain, (~c9_2(a1931, a1932))). % 48.79/23.24 tff(c_9375, plain, (c1_2(a1931, a1932))). % 48.79/23.24 tff(c_9363, plain, (c3_1(a1939))). % 48.79/23.24 tff(c_9359, plain, (~c5_1(a1939))). % 48.79/23.24 tff(c_9358, plain, (~c1_1(a1939))). % 48.79/23.24 tff(c_9352, plain, (~c7_1(a1939))). % 48.79/23.24 tff(c_9349, plain, (~c9_1(a1939))). % 48.79/23.24 tff(c_9333, plain, (~ndr1_1(a1939))). % 48.79/23.24 tff(c_9329, plain, (ndr1_1(a1931))). % 48.79/23.24 tff(c_9319, plain, (ndr1_1(a1871))). % 48.79/23.24 tff(c_9318, plain, (~c8_1(a1931))). % 48.79/23.24 tff(c_9315, plain, (~c2_2(a1986, a1987))). % 48.79/23.24 tff(c_9314, plain, (~c9_1(a2017))). % 48.79/23.24 tff(c_9313, plain, (~c9_1(a2029))). % 48.79/23.24 tff(c_9312, plain, (~c9_1(a1913))). % 48.79/23.24 tff(c_9301, plain, (![X170_221]: (ndr1_1(X170_221) | ~c9_1(X170_221)))). % 48.79/23.24 tff(c_9295, plain, (c8_1(a1913))). % 48.79/23.24 tff(c_9294, plain, (c3_1(a1913))). % 48.79/23.24 tff(c_9290, plain, (~c5_1(a1913))). % 48.79/23.24 tff(c_9289, plain, (~c10_1(a1913))). % 48.79/23.24 tff(c_9288, plain, (~c1_1(a1913))). % 48.79/23.24 tff(c_9270, plain, (~ndr1_1(a1913))). % 48.79/23.24 tff(c_9263, plain, (c7_2(a1986, a1987))). % 48.79/23.24 tff(c_9262, plain, (~c5_2(a1986, a1987))). % 48.79/23.24 tff(c_9237, plain, (~c9_1(a1986))). % 48.79/23.24 tff(c_9223, plain, (![X122_163]: (c3_2(X122_163, a1955) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.24 tff(c_9219, plain, (ndr1_1(a1986))). % 48.79/23.24 tff(c_9215, plain, (![X122_163]: (~c1_2(X122_163, a1955) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.25 tff(c_9212, plain, (~c7_1(a1986))). % 48.79/23.25 tff(c_9208, plain, (![X122_163]: (c5_2(X122_163, a1955) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.25 tff(c_9190, plain, (![X12_22]: (~c8_2(a1851, X12_22) | c5_2(a1851, X12_22) | c4_2(a1851, X12_22)))). % 48.79/23.25 tff(c_9114, plain, (~c1_1(a2029))). % 48.79/23.25 tff(c_9112, plain, (c3_1(a2029))). % 48.79/23.25 tff(c_9108, plain, (~c5_1(a2029))). % 48.79/23.25 tff(c_9103, plain, (~c7_1(a2029))). % 48.79/23.25 tff(c_9088, plain, (~ndr1_1(a2029))). % 48.79/23.25 tff(c_9069, plain, (~c1_1(a2017))). % 48.79/23.25 tff(c_9063, plain, (~c5_1(a2017))). % 48.79/23.25 tff(c_9062, plain, (~c10_1(a2017))). % 48.79/23.25 tff(c_9044, plain, (~ndr1_1(a2017))). % 48.79/23.25 tff(c_8985, plain, (~c1_1(a1841))). % 48.79/23.25 tff(c_8984, plain, (~c1_1(a1865))). % 48.79/23.25 tff(c_8983, plain, (~c1_1(a1900))). % 48.79/23.25 tff(c_8963, plain, (![X115_153, X116_155]: (~c2_2(X115_153, X116_155) | ~ndr1_1(X115_153) | ~c1_1(X115_153) | c8_1(X115_153)))). % 48.79/23.25 tff(c_8956, plain, (c1_1(a1845))). % 48.79/23.25 tff(c_8936, plain, (![X122_163]: (ndr1_1(X122_163) | ~c7_1(X122_163) | ~c10_1(X122_163)))). % 48.79/23.25 tff(c_8892, plain, (c5_1(a1951))). % 48.79/23.25 tff(c_8885, plain, (![X1_9]: (~c7_2(a1841, X1_9) | ~c2_2(a1841, X1_9)))). % 48.79/23.25 tff(c_8876, plain, (~c1_2(a1995, a1996))). % 48.79/23.25 tff(c_8868, plain, (~c1_1(a1950))). % 48.79/23.25 tff(c_8861, plain, (~c6_2(a1995, a1996))). % 48.79/23.25 tff(c_8848, plain, (~c3_1(a1951))). % 48.79/23.25 tff(c_8844, plain, (c5_2(a1995, a1996))). % 48.79/23.25 tff(c_8828, plain, (![X200_262]: (c3_2(X200_262, a2026) | c4_1(X200_262) | ~c5_1(X200_262)))). % 48.79/23.25 tff(c_8825, plain, (~c6_1(a2027))). % 48.79/23.25 tff(c_8822, plain, (![X200_262]: (c4_2(X200_262, a2026) | c4_1(X200_262) | ~c5_1(X200_262)))). % 48.79/23.25 tff(c_8818, plain, (![X200_262]: (~c10_2(X200_262, a2026) | c4_1(X200_262) | ~c5_1(X200_262)))). % 48.79/23.25 tff(c_8814, plain, (c3_1(a2027))). % 48.79/23.25 tff(c_8812, plain, (ndr1_1(a1995))). % 48.79/23.25 tff(c_8808, plain, (![X186_243]: (~c4_2(X186_243, a2018) | c10_1(X186_243) | c8_1(X186_243)))). % 48.79/23.25 tff(c_8805, plain, (~c4_1(a2027))). % 48.79/23.25 tff(c_8802, plain, (![X186_243]: (~c10_2(X186_243, a2018) | c10_1(X186_243) | c8_1(X186_243)))). % 48.79/23.25 tff(c_8798, plain, (![X186_243]: (c6_2(X186_243, a2018) | c10_1(X186_243) | c8_1(X186_243)))). % 48.79/23.25 tff(c_8793, plain, (c3_1(a1924))). % 48.79/23.25 tff(c_8789, plain, (~c5_1(a1924))). % 48.79/23.25 tff(c_8786, plain, (~c3_1(a1995))). % 48.79/23.25 tff(c_8773, plain, (![X11_21]: (~c7_2(a1851, X11_21) | ~c4_2(a1851, X11_21)))). % 48.79/23.25 tff(c_8768, plain, (![X200_262]: (ndr1_1(X200_262) | c4_1(X200_262) | ~c5_1(X200_262)))). % 48.79/23.25 tff(c_8762, plain, (![X186_243]: (ndr1_1(X186_243) | c10_1(X186_243) | c8_1(X186_243)))). % 48.79/23.25 tff(c_8759, plain, (c4_2(a2006, a2007))). % 48.79/23.25 tff(c_8757, plain, (c2_1(a2014))). % 48.79/23.25 tff(c_8752, plain, (![X85_116]: (c1_2(X85_116, a1927) | c2_1(X85_116) | ~c1_1(X85_116)))). % 48.79/23.25 tff(c_8750, plain, (![X85_116]: (~c9_2(X85_116, a1927) | c2_1(X85_116) | ~c1_1(X85_116)))). % 48.79/23.25 tff(c_8749, plain, (c4_1(a1906))). % 48.79/23.25 tff(c_8748, plain, (c7_2(a2006, a2007))). % 48.79/23.25 tff(c_8742, plain, (c10_1(a1939))). % 48.79/23.25 tff(c_8745, plain, (![X71_97]: (c7_2(a1915, X71_97) | c1_2(a1915, X71_97)))). % 48.79/23.25 tff(c_8740, plain, (~c2_1(a1939))). % 48.79/23.25 tff(c_8739, plain, (~c2_2(a2006, a2007))). % 48.79/23.25 tff(c_8737, plain, (c5_1(a1963))). % 48.79/23.25 tff(c_8733, plain, (~c4_2(a1865, a1866))). % 48.79/23.25 tff(c_8732, plain, (c9_1(a1979))). % 48.79/23.25 tff(c_8730, plain, (~c7_1(a2014))). % 48.79/23.25 tff(c_8727, plain, (c1_1(a1979))). % 48.79/23.25 tff(c_8725, plain, (~c9_2(a1865, a1867))). % 48.79/23.25 tff(c_8721, plain, (ndr1_1(a2006))). % 48.79/23.25 tff(c_8715, plain, (~c5_2(a1865, a1867))). % 48.79/23.25 tff(c_8714, plain, (~c7_2(a1865, a1866))). % 48.79/23.25 tff(c_8710, plain, (![X99_133]: (~c6_1(X99_133) | ~c10_1(X99_133)))). % 48.79/23.25 tff(c_8708, plain, (~c7_2(a1865, a1868))). % 48.79/23.25 tff(c_8707, plain, (~c6_1(a2030))). % 48.79/23.25 tff(c_8703, plain, (c2_2(a1865, a1868))). % 48.79/23.25 tff(c_8698, plain, (~c6_2(a1865, a1868))). % 48.79/23.25 tff(c_8693, plain, (~c7_1(a2030))). % 48.79/23.25 tff(c_8688, plain, (![X85_116]: (ndr1_1(X85_116) | c2_1(X85_116) | ~c1_1(X85_116)))). % 48.79/23.25 tff(c_8677, plain, (c3_2(a1865, a1867))). % 48.79/23.25 tff(c_8674, plain, (c4_1(a2006))). % 48.79/23.25 tff(c_8672, plain, (c8_2(a1865, a1866))). % 48.79/23.25 tff(c_8661, plain, (~c9_1(a1935))). % 48.79/23.25 tff(c_8632, plain, (c5_2(a2001, a2002))). % 48.79/23.25 tff(c_8627, plain, (c8_2(a1846, a1847))). % 48.79/23.25 tff(c_8620, plain, (c4_2(a1841, a1842))). % 48.79/23.25 tff(c_8618, plain, (c7_2(a1846, a1847))). % 48.79/23.25 tff(c_8613, plain, (c5_2(a1846, a1847))). % 48.79/23.25 tff(c_8607, plain, (ndr1_1(a1865))). % 48.79/23.25 tff(c_8585, plain, (c2_2(a1841, a1842))). % 48.79/23.25 tff(c_8568, plain, (c9_2(a2001, a2002))). % 48.79/23.25 tff(c_8565, plain, (~c2_2(a2001, a2002))). % 48.79/23.25 tff(c_8554, plain, (~c9_2(a2015, a2016))). % 48.79/23.25 tff(c_8553, plain, (~c8_2(a2015, a2016))). % 48.79/23.25 tff(c_8552, plain, (c3_1(a1998))). % 48.79/23.25 tff(c_8551, plain, (c3_1(a1876))). % 48.79/23.25 tff(c_8543, plain, (![X8_18]: (c3_1(X8_18) | c5_1(X8_18)))). % 48.79/23.25 tff(c_8541, plain, (ndr1_1(a2001))). % 48.79/23.25 tff(c_8536, plain, (c8_2(a1933, a1934))). % 48.79/23.25 tff(c_8527, plain, (~c9_2(a1915, a1916))). % 48.79/23.25 tff(c_8524, plain, (c5_2(a1933, a1934))). % 48.79/23.25 tff(c_8520, plain, (~c4_2(a1900, a1901))). % 48.79/23.25 tff(c_8519, plain, (~c2_2(a1900, a1901))). % 48.79/23.25 tff(c_8509, plain, (ndr1_1(a1846))). % 48.79/23.25 tff(c_8506, plain, (c9_1(a1846))). % 48.79/23.25 tff(c_8500, plain, (~c2_1(a1913))). % 48.79/23.26 tff(c_8496, plain, (ndr1_1(a1841))). % 48.79/23.26 tff(c_8493, plain, (~c4_2(a1851, a1852))). % 48.79/23.26 tff(c_8490, plain, (c5_2(a1915, a1916))). % 48.79/23.26 tff(c_8486, plain, (c2_2(a1900, a1902))). % 48.79/23.26 tff(c_8485, plain, (~c10_2(a1900, a1902))). % 48.79/23.26 tff(c_8484, plain, (~c5_1(a1876))). % 48.79/23.26 tff(c_8482, plain, (~c5_1(a1998))). % 48.79/23.26 tff(c_8479, plain, (~c2_1(a1876))). % 48.79/23.26 tff(c_8475, plain, (~c10_2(a1900, a1901))). % 48.79/23.26 tff(c_8474, plain, (c2_1(a2001))). % 48.79/23.26 tff(c_8471, plain, (~c1_2(a1933, a1934))). % 48.79/23.26 tff(c_8468, plain, (c9_2(a1900, a1902))). % 48.79/23.26 tff(c_8462, plain, (~c2_2(a1851, a1852))). % 48.79/23.26 tff(c_8459, plain, (~c10_1(a1839))). % 48.79/23.26 tff(c_8457, plain, (~c10_1(a1845))). % 48.79/23.26 tff(c_8454, plain, (~c3_1(a2001))). % 48.79/23.26 tff(c_8451, plain, (c3_2(a1851, a1852))). % 48.79/23.26 tff(c_8444, plain, (ndr1_1(a1915))). % 48.79/23.26 tff(c_8441, plain, (ndr1_1(a1851))). % 48.79/23.26 tff(c_8432, plain, (ndr1_1(a1933))). % 48.79/23.26 tff(c_8430, plain, (c5_1(a1915))). % 48.79/23.26 tff(c_8427, plain, (~c6_1(a1900))). % 48.79/23.26 tff(c_8426, plain, (ndr1_1(a2015))). % 48.79/23.26 tff(c_8414, plain, (~c3_1(a1933))). % 48.79/23.26 tff(c_8408, plain, (~c8_1(a1933))). % 48.79/23.26 tff(c_8399, plain, (ndr1_1(a1900))). % 48.79/23.26 tff(c_8384, plain, (~c6_0)). % 48.79/23.26 tff(c_8380, plain, (c10_1(a2029))). % 48.79/23.26 tff(c_8379, plain, (c5_1(a1907))). % 48.79/23.26 tff(c_8377, plain, (c3_1(a2017))). % 48.79/23.26 tff(c_8376, plain, (~c8_0)). % 48.79/23.26 tff(c_8373, plain, (c8_1(a2017))). % 48.79/23.26 tff(c_8370, plain, (~c10_1(a1907))). % 48.79/23.26 tff(c_8368, plain, (c8_1(a1907))). % 48.79/23.26 tff(c_8364, plain, (~c3_0)). % 48.79/23.26 tff(c_8359, plain, (~c10_0)). % 48.79/23.26 tff(c_8358, plain, (c9_0)). % 48.79/23.26 tff(c_8356, plain, (~c2_0)). % 48.79/23.26 tff(c_8355, plain, (c7_0)). % 48.79/23.26 tff(c_8354, plain, (~c1_0)). % 48.79/23.26 tff(c_8353, plain, (c5_0)). % 48.79/23.26 tff(c_8352, plain, (~c4_0)). % 48.79/23.26 tff(c_330, plain, (ndr1_0)). % 48.79/23.26 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 48.79/23.26 %------------------------------------------------------------------------------