%------------------------------------------------------------------------------ % 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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n003.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:33 PM UTC 2025 % Result : Satisfiable 34.24s 12.80s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN428-1 : TPTP v9.0.0. Released v2.1.0. % 0.13/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 07:25:33 EDT 2025 % 0.13/0.34 % CPUTime : % 34.24/12.80 % 34.24/12.80 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.24/12.80 % 34.24/12.80 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.30/12.83 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ssSkP9 > ssSkP8 > ssSkP7 > ssSkP6 > ssSkP5 > ssSkP4 > ssSkP3 > ssSkP2 > ssSkP16 > ssSkP15 > ssSkP14 > ssSkP13 > ssSkP12 > ssSkP11 > ssSkP10 > ssSkP1 > ssSkP0 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ssSkC9 > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC43 > ssSkC42 > ssSkC41 > ssSkC40 > ssSkC4 > ssSkC39 > ssSkC38 > ssSkC37 > ssSkC36 > ssSkC35 > ssSkC34 > ssSkC33 > ssSkC32 > ssSkC31 > ssSkC30 > ssSkC3 > ssSkC29 > ssSkC28 > ssSkC27 > ssSkC26 > ssSkC25 > ssSkC24 > ssSkC23 > ssSkC22 > ssSkC21 > ssSkC20 > ssSkC2 > ssSkC19 > ssSkC18 > ssSkC17 > ssSkC16 > ssSkC15 > ssSkC14 > ssSkC13 > ssSkC12 > ssSkC11 > ssSkC10 > ssSkC1 > ssSkC0 > 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 % 34.30/12.83 % 34.30/12.83 %Foreground sorts: % 34.30/12.83 % 34.30/12.83 % 34.30/12.83 %Background operators: % 34.30/12.83 % 34.30/12.83 % 34.30/12.83 %Foreground operators: % 34.30/12.83 tff(a1879, type, a1879: $i). % 34.30/12.83 tff(a1960, type, a1960: $i). % 34.30/12.83 tff(a2016, type, a2016: $i). % 34.30/12.83 tff(c7_0, type, c7_0: $o). % 34.30/12.83 tff(ssSkP13, type, ssSkP13: $i > $o). % 34.30/12.83 tff(ssSkC8, type, ssSkC8: $o). % 34.30/12.83 tff(a1841, type, a1841: $i). % 34.30/12.83 tff(a2031, type, a2031: $i). % 34.30/12.83 tff(a1903, type, a1903: $i). % 34.30/12.83 tff(a1871, type, a1871: $i). % 34.30/12.83 tff(ssSkC7, type, ssSkC7: $o). % 34.30/12.83 tff(a1912, type, a1912: $i). % 34.30/12.83 tff(a1839, type, a1839: $i). % 34.30/12.83 tff(a1850, type, a1850: $i). % 34.30/12.83 tff(ssSkC21, type, ssSkC21: $o). % 34.30/12.83 tff(a1910, type, a1910: $i). % 34.30/12.83 tff(a1929, type, a1929: $i). % 34.30/12.83 tff(a1914, type, a1914: $i). % 34.30/12.83 tff(c4_0, type, c4_0: $o). % 34.30/12.83 tff(a1894, type, a1894: $i). % 34.30/12.83 tff(a1934, type, a1934: $i). % 34.30/12.83 tff(ssSkC10, type, ssSkC10: $o). % 34.30/12.83 tff(a1943, type, a1943: $i). % 34.30/12.83 tff(a1946, type, a1946: $i). % 34.30/12.83 tff(ssSkP0, type, ssSkP0: $i > $o). % 34.30/12.83 tff(a1967, type, a1967: $i). % 34.30/12.83 tff(a2019, type, a2019: $i). % 34.30/12.83 tff(a1927, type, a1927: $i). % 34.30/12.83 tff(a1932, type, a1932: $i). % 34.30/12.83 tff(ssSkC6, type, ssSkC6: $o). % 34.30/12.83 tff(c3_0, type, c3_0: $o). % 34.30/12.83 tff(a2000, type, a2000: $i). % 34.30/12.83 tff(a1852, type, a1852: $i). % 34.30/12.83 tff(ssSkP7, type, ssSkP7: $i > $o). % 34.30/12.83 tff(a1836, type, a1836: $i). % 34.30/12.83 tff(a1863, type, a1863: $i). % 34.30/12.83 tff(a1904, type, a1904: $i). % 34.30/12.83 tff(c1_2, type, c1_2: ($i * $i) > $o). % 34.30/12.83 tff(a1975, type, a1975: $i). % 34.30/12.83 tff(a2009, type, a2009: $i). % 34.30/12.83 tff(a1840, type, a1840: $i). % 34.30/12.83 tff(a1981, type, a1981: $i). % 34.30/12.83 tff(a1864, type, a1864: $i). % 34.30/12.83 tff(ssSkC23, type, ssSkC23: $o). % 34.30/12.83 tff(ssSkC3, type, ssSkC3: $o). % 34.30/12.83 tff(a1875, type, a1875: $i). % 34.30/12.83 tff(a1842, type, a1842: $i). % 34.30/12.83 tff(a1992, type, a1992: $i). % 34.30/12.83 tff(a2024, type, a2024: $i). % 34.30/12.83 tff(a2012, type, a2012: $i). % 34.30/12.83 tff(a2001, type, a2001: $i). % 34.30/12.83 tff(a2022, type, a2022: $i). % 34.30/12.83 tff(ssSkP2, type, ssSkP2: $i > $o). % 34.30/12.83 tff(a1916, type, a1916: $i). % 34.30/12.83 tff(a1882, type, a1882: $i). % 34.30/12.83 tff(a1951, type, a1951: $i). % 34.30/12.83 tff(ssSkC19, type, ssSkC19: $o). % 34.30/12.83 tff(a1959, type, a1959: $i). % 34.30/12.83 tff(ssSkC40, type, ssSkC40: $o). % 34.30/12.83 tff(ssSkC28, type, ssSkC28: $o). % 34.30/12.83 tff(a1947, type, a1947: $i). % 34.30/12.83 tff(a1996, type, a1996: $i). % 34.30/12.83 tff(a2007, type, a2007: $i). % 34.30/12.83 tff(ssSkC38, type, ssSkC38: $o). % 34.30/12.83 tff(a2026, type, a2026: $i). % 34.30/12.83 tff(ssSkC26, type, ssSkC26: $o). % 34.30/12.83 tff(a1851, type, a1851: $i). % 34.30/12.83 tff(a1897, type, a1897: $i). % 34.30/12.83 tff(a2010, type, a2010: $i). % 34.30/12.83 tff(a1931, type, a1931: $i). % 34.30/12.83 tff(a1872, type, a1872: $i). % 34.30/12.83 tff(a2015, type, a2015: $i). % 34.30/12.83 tff(a1887, type, a1887: $i). % 34.30/12.83 tff(a2025, type, a2025: $i). % 34.30/12.83 tff(ssSkP14, type, ssSkP14: $i > $o). % 34.30/12.83 tff(c8_0, type, c8_0: $o). % 34.30/12.83 tff(a1982, type, a1982: $i). % 34.30/12.83 tff(a1895, type, a1895: $i). % 34.30/12.83 tff(a1965, type, a1965: $i). % 34.30/12.83 tff(a1853, type, a1853: $i). % 34.30/12.83 tff(a1905, type, a1905: $i). % 34.30/12.83 tff(a1890, type, a1890: $i). % 34.30/12.83 tff(ssSkC4, type, ssSkC4: $o). % 34.30/12.83 tff(a1984, type, a1984: $i). % 34.30/12.83 tff(a1845, type, a1845: $i). % 34.30/12.83 tff(a1849, type, a1849: $i). % 34.30/12.83 tff(a1926, type, a1926: $i). % 34.30/12.83 tff(ssSkC37, type, ssSkC37: $o). % 34.30/12.83 tff(a1892, type, a1892: $i). % 34.30/12.83 tff(a1936, type, a1936: $i). % 34.30/12.83 tff(ssSkP15, type, ssSkP15: $i > $o). % 34.30/12.83 tff(a1848, type, a1848: $i). % 34.30/12.83 tff(a1939, type, a1939: $i). % 34.30/12.83 tff(c5_0, type, c5_0: $o). % 34.30/12.83 tff(a2002, type, a2002: $i). % 34.30/12.83 tff(a1837, type, a1837: $i). % 34.30/12.83 tff(a2028, type, a2028: $i). % 34.30/12.83 tff(a1973, type, a1973: $i). % 34.30/12.83 tff(a1979, type, a1979: $i). % 34.30/12.83 tff(ssSkC9, type, ssSkC9: $o). % 34.30/12.83 tff(a2018, type, a2018: $i). % 34.30/12.83 tff(a1920, type, a1920: $i). % 34.30/12.83 tff(ssSkP6, type, ssSkP6: $i > $o). % 34.30/12.83 tff(a1886, type, a1886: $i). % 34.30/12.83 tff(a1898, type, a1898: $i). % 34.30/12.83 tff(a1968, type, a1968: $i). % 34.30/12.83 tff(ssSkP8, type, ssSkP8: $i > $o). % 34.30/12.83 tff(c6_0, type, c6_0: $o). % 34.30/12.83 tff(c8_2, type, c8_2: ($i * $i) > $o). % 34.30/12.83 tff(ssSkC30, type, ssSkC30: $o). % 34.30/12.83 tff(a1989, type, a1989: $i). % 34.30/12.83 tff(a1847, type, a1847: $i). % 34.30/12.83 tff(a1874, type, a1874: $i). % 34.30/12.83 tff(a1855, type, a1855: $i). % 34.30/12.83 tff(ssSkC11, type, ssSkC11: $o). % 34.30/12.83 tff(a1944, type, a1944: $i). % 34.30/12.83 tff(a1858, type, a1858: $i). % 34.30/12.83 tff(a2017, type, a2017: $i). % 34.30/12.83 tff(ssSkC18, type, ssSkC18: $o). % 34.30/12.83 tff(a1995, type, a1995: $i). % 34.30/12.83 tff(a1999, type, a1999: $i). % 34.30/12.83 tff(ssSkC16, type, ssSkC16: $o). % 34.30/12.83 tff(a2011, type, a2011: $i). % 34.30/12.83 tff(a1866, type, a1866: $i). % 34.30/12.83 tff(a1969, type, a1969: $i). % 34.30/12.83 tff(a1972, type, a1972: $i). % 34.30/12.83 tff(a2021, type, a2021: $i). % 34.30/12.83 tff(ssSkP3, type, ssSkP3: $i > $o). % 34.30/12.83 tff(a1950, type, a1950: $i). % 34.30/12.83 tff(ssSkC32, type, ssSkC32: $o). % 34.30/12.83 tff(a1888, type, a1888: $i). % 34.30/12.83 tff(ssSkC24, type, ssSkC24: $o). % 34.30/12.83 tff(a1962, type, a1962: $i). % 34.30/12.83 tff(a1924, type, a1924: $i). % 34.30/12.83 tff(ssSkC17, type, ssSkC17: $o). % 34.30/12.83 tff(a1915, type, a1915: $i). % 34.30/12.83 tff(a1956, type, a1956: $i). % 34.30/12.83 tff(a1961, type, a1961: $i). % 34.30/12.83 tff(ssSkP9, type, ssSkP9: $i > $o). % 34.30/12.83 tff(a1970, type, a1970: $i). % 34.30/12.83 tff(a1891, type, a1891: $i). % 34.30/12.83 tff(c1_0, type, c1_0: $o). % 34.30/12.83 tff(c8_1, type, c8_1: $i > $o). % 34.30/12.83 tff(a1902, type, a1902: $i). % 34.30/12.83 tff(a2032, type, a2032: $i). % 34.30/12.83 tff(a1838, type, a1838: $i). % 34.30/12.83 tff(a1935, type, a1935: $i). % 34.30/12.83 tff(ssSkC29, type, ssSkC29: $o). % 34.30/12.83 tff(ssSkP4, type, ssSkP4: $i > $o). % 34.30/12.83 tff(c2_1, type, c2_1: $i > $o). % 34.30/12.83 tff(a1854, type, a1854: $i). % 34.30/12.83 tff(a1922, type, a1922: $i). % 34.30/12.83 tff(a1835, type, a1835: $i). % 34.30/12.83 tff(a1930, type, a1930: $i). % 34.30/12.83 tff(ssSkC27, type, ssSkC27: $o). % 34.30/12.83 tff(a1925, type, a1925: $i). % 34.30/12.83 tff(ndr1_1, type, ndr1_1: $i > $o). % 34.30/12.83 tff(ssSkC15, type, ssSkC15: $o). % 34.30/12.83 tff(c2_0, type, c2_0: $o). % 34.30/12.83 tff(c4_1, type, c4_1: $i > $o). % 34.30/12.83 tff(ssSkC42, type, ssSkC42: $o). % 34.30/12.83 tff(a1843, type, a1843: $i). % 34.30/12.83 tff(a1896, type, a1896: $i). % 34.30/12.83 tff(a1884, type, a1884: $i). % 34.30/12.83 tff(a1873, type, a1873: $i). % 34.30/12.83 tff(a1938, type, a1938: $i). % 34.30/12.83 tff(a1856, type, a1856: $i). % 34.30/12.83 tff(a1883, type, a1883: $i). % 34.30/12.83 tff(a2030, type, a2030: $i). % 34.30/12.83 tff(a1893, type, a1893: $i). % 34.30/12.83 tff(a1867, type, a1867: $i). % 34.30/12.83 tff(a1941, type, a1941: $i). % 34.30/12.83 tff(a2020, type, a2020: $i). % 34.30/12.83 tff(a1861, type, a1861: $i). % 34.30/12.83 tff(a1878, type, a1878: $i). % 34.30/12.83 tff(ssSkC36, type, ssSkC36: $o). % 34.30/12.83 tff(c9_1, type, c9_1: $i > $o). % 34.30/12.83 tff(a1885, type, a1885: $i). % 34.30/12.83 tff(c10_1, type, c10_1: $i > $o). % 34.30/12.83 tff(c10_0, type, c10_0: $o). % 34.30/12.83 tff(ssSkC12, type, ssSkC12: $o). % 34.30/12.83 tff(a1869, type, a1869: $i). % 34.30/12.83 tff(a1859, type, a1859: $i). % 34.30/12.83 tff(a1870, type, a1870: $i). % 34.30/12.83 tff(a1993, type, a1993: $i). % 34.30/12.83 tff(c6_2, type, c6_2: ($i * $i) > $o). % 34.30/12.83 tff(a2029, type, a2029: $i). % 34.30/12.83 tff(a1983, type, a1983: $i). % 34.30/12.83 tff(a1917, type, a1917: $i). % 34.30/12.83 tff(a1906, type, a1906: $i). % 34.30/12.83 tff(ssSkC20, type, ssSkC20: $o). % 34.30/12.83 tff(a1955, type, a1955: $i). % 34.30/12.83 tff(a1919, type, a1919: $i). % 34.30/12.83 tff(a2027, type, a2027: $i). % 34.30/12.83 tff(a1928, type, a1928: $i). % 34.30/12.83 tff(a2003, type, a2003: $i). % 34.30/12.83 tff(a1942, type, a1942: $i). % 34.30/12.83 tff(a1945, type, a1945: $i). % 34.30/12.83 tff(a1857, type, a1857: $i). % 34.30/12.83 tff(a1976, type, a1976: $i). % 34.30/12.83 tff(a1988, type, a1988: $i). % 34.30/12.83 tff(a1963, type, a1963: $i). % 34.30/12.83 tff(ndr1_0, type, ndr1_0: $o). % 34.30/12.83 tff(a1933, type, a1933: $i). % 34.30/12.83 tff(ssSkC39, type, ssSkC39: $o). % 34.30/12.83 tff(a1881, type, a1881: $i). % 34.30/12.83 tff(a1940, type, a1940: $i). % 34.30/12.83 tff(a1862, type, a1862: $i). % 34.30/12.83 tff(ssSkC14, type, ssSkC14: $o). % 34.30/12.83 tff(a1908, type, a1908: $i). % 34.30/12.83 tff(c9_2, type, c9_2: ($i * $i) > $o). % 34.30/12.83 tff(a1985, type, a1985: $i). % 34.30/12.83 tff(a1948, type, a1948: $i). % 34.30/12.83 tff(ssSkC33, type, ssSkC33: $o). % 34.30/12.83 tff(a1909, type, a1909: $i). % 34.30/12.83 tff(c10_2, type, c10_2: ($i * $i) > $o). % 34.30/12.83 tff(ssSkC34, type, ssSkC34: $o). % 34.30/12.83 tff(a1876, type, a1876: $i). % 34.30/12.83 tff(a1994, type, a1994: $i). % 34.30/12.83 tff(a1991, type, a1991: $i). % 34.30/12.83 tff(a1868, type, a1868: $i). % 34.30/12.83 tff(ssSkC43, type, ssSkC43: $o). % 34.30/12.83 tff(a1966, type, a1966: $i). % 34.30/12.83 tff(a1877, type, a1877: $i). % 34.30/12.83 tff(c1_1, type, c1_1: $i > $o). % 34.30/12.83 tff(a1889, type, a1889: $i). % 34.30/12.83 tff(a1971, type, a1971: $i). % 34.30/12.83 tff(a1923, type, a1923: $i). % 34.30/12.83 tff(ssSkC41, type, ssSkC41: $o). % 34.30/12.83 tff(ssSkP11, type, ssSkP11: $i > $o). % 34.30/12.83 tff(a1987, type, a1987: $i). % 34.30/12.83 tff(a1921, type, a1921: $i). % 34.30/12.83 tff(ssSkC13, type, ssSkC13: $o). % 34.30/12.83 tff(ssSkC25, type, ssSkC25: $o). % 34.30/12.83 tff(a1899, type, a1899: $i). % 34.30/12.83 tff(ssSkC2, type, ssSkC2: $o). % 34.30/12.83 tff(c5_2, type, c5_2: ($i * $i) > $o). % 34.30/12.83 tff(ssSkC31, type, ssSkC31: $o). % 34.30/12.83 tff(a1846, type, a1846: $i). % 34.30/12.83 tff(c9_0, type, c9_0: $o). % 34.30/12.83 tff(ssSkP16, type, ssSkP16: $i > $o). % 34.30/12.83 tff(a2004, type, a2004: $i). % 34.30/12.83 tff(a1954, type, a1954: $i). % 34.30/12.83 tff(c7_1, type, c7_1: $i > $o). % 34.30/12.83 tff(a1964, type, a1964: $i). % 34.30/12.83 tff(c6_1, type, c6_1: $i > $o). % 34.30/12.83 tff(a1911, type, a1911: $i). % 34.30/12.83 tff(a1990, type, a1990: $i). % 34.30/12.83 tff(ssSkC22, type, ssSkC22: $o). % 34.30/12.83 tff(a1953, type, a1953: $i). % 34.30/12.83 tff(a1998, type, a1998: $i). % 34.30/12.83 tff(a1865, type, a1865: $i). % 34.30/12.83 tff(c4_2, type, c4_2: ($i * $i) > $o). % 34.30/12.83 tff(ssSkC1, type, ssSkC1: $o). % 34.30/12.83 tff(a1860, type, a1860: $i). % 34.30/12.83 tff(a1834, type, a1834: $i). % 34.30/12.83 tff(a2014, type, a2014: $i). % 34.30/12.83 tff(ssSkP5, type, ssSkP5: $i > $o). % 34.30/12.83 tff(ssSkC0, type, ssSkC0: $o). % 34.30/12.83 tff(ssSkC5, type, ssSkC5: $o). % 34.30/12.83 tff(a2005, type, a2005: $i). % 34.30/12.83 tff(ssSkP1, type, ssSkP1: $i > $o). % 34.30/12.83 tff(a2008, type, a2008: $i). % 34.30/12.83 tff(a1900, type, a1900: $i). % 34.30/12.83 tff(ssSkC35, type, ssSkC35: $o). % 34.30/12.83 tff(a1918, type, a1918: $i). % 34.30/12.83 tff(a2013, type, a2013: $i). % 34.30/12.83 tff(c5_1, type, c5_1: $i > $o). % 34.30/12.83 tff(a1977, type, a1977: $i). % 34.30/12.83 tff(a1978, type, a1978: $i). % 34.30/12.83 tff(ssSkP12, type, ssSkP12: $i > $o). % 34.30/12.83 tff(a1952, type, a1952: $i). % 34.30/12.83 tff(a1901, type, a1901: $i). % 34.30/12.83 tff(c7_2, type, c7_2: ($i * $i) > $o). % 34.30/12.83 tff(a1980, type, a1980: $i). % 34.30/12.83 tff(c3_2, type, c3_2: ($i * $i) > $o). % 34.30/12.83 tff(a1844, type, a1844: $i). % 34.30/12.83 tff(a1880, type, a1880: $i). % 34.30/12.83 tff(a1949, type, a1949: $i). % 34.30/12.83 tff(a1957, type, a1957: $i). % 34.30/12.83 tff(c2_2, type, c2_2: ($i * $i) > $o). % 34.30/12.83 tff(a1937, type, a1937: $i). % 34.30/12.83 tff(a2023, type, a2023: $i). % 34.30/12.83 tff(a1986, type, a1986: $i). % 34.30/12.83 tff(a1907, type, a1907: $i). % 34.30/12.83 tff(a1997, type, a1997: $i). % 34.30/12.83 tff(a1958, type, a1958: $i). % 34.30/12.83 tff(ssSkP10, type, ssSkP10: $i > $o). % 34.30/12.83 tff(a2006, type, a2006: $i). % 34.30/12.83 tff(a1974, type, a1974: $i). % 34.30/12.83 tff(a1913, type, a1913: $i). % 34.30/12.83 tff(c3_1, type, c3_1: $i > $o). % 34.30/12.83 % 34.30/12.83 %Saturated clause set: % 34.30/12.84 tff(c_9421, plain, (![U_916]: (c10_2(U_916, a1954) | c1_2(U_916, a1949) | ~ssSkP9(U_916) | c10_1(U_916) | c3_2(U_916, a1949) | c2_2(U_916, a1949) | c2_1(U_916) | c1_1(U_916) | c8_1(U_916) | ~c4_2(U_916, a2025) | ~c10_2(U_916, a2025) | c5_1(U_916) | ~c7_1(U_916) | ~ndr1_1(U_916) | ~c4_2(U_916, a1898) | ~c10_2(U_916, a1898)))). % 34.30/12.84 tff(c_9420, plain, (![U_916]: (c3_2(U_916, a1954) | c1_2(U_916, a1949) | ~ssSkP9(U_916) | c10_1(U_916) | c3_2(U_916, a1949) | c2_2(U_916, a1949) | c2_1(U_916) | c1_1(U_916) | c8_1(U_916) | ~c4_2(U_916, a2025) | ~c10_2(U_916, a2025) | c5_1(U_916) | ~c7_1(U_916) | ~ndr1_1(U_916) | ~c4_2(U_916, a1898) | ~c10_2(U_916, a1898)))). % 34.30/12.84 tff(c_9342, plain, (![U_909]: (c3_2(U_909, a1954) | c1_2(U_909, a1843) | ~ssSkP9(U_909) | c10_1(U_909) | c3_2(U_909, a1843) | c2_2(U_909, a1843) | c2_1(U_909) | ssSkP3(U_909) | ~c4_2(U_909, a2025) | ~c10_2(U_909, a2025) | c5_1(U_909) | ~c7_1(U_909) | ~ndr1_1(U_909) | ~c4_2(U_909, a1898) | ~c10_2(U_909, a1898)))). % 34.30/12.84 tff(c_9341, plain, (![U_909]: (c10_2(U_909, a1954) | c1_2(U_909, a1843) | ~ssSkP9(U_909) | c10_1(U_909) | c3_2(U_909, a1843) | c2_2(U_909, a1843) | c2_1(U_909) | ssSkP3(U_909) | ~c4_2(U_909, a2025) | ~c10_2(U_909, a2025) | c5_1(U_909) | ~c7_1(U_909) | ~ndr1_1(U_909) | ~c4_2(U_909, a1898) | ~c10_2(U_909, a1898)))). % 34.30/12.84 tff(c_9280, plain, (![U_905]: (c3_2(U_905, a1954) | c1_2(U_905, a1949) | ~ssSkP9(U_905) | c10_1(U_905) | c3_2(U_905, a1949) | c2_2(U_905, a1949) | c2_1(U_905) | c2_2(U_905, a1898) | c1_1(U_905) | c8_1(U_905) | c5_1(U_905) | ~c7_1(U_905) | ~ndr1_1(U_905) | ~c4_2(U_905, a2025) | ~c10_2(U_905, a2025)))). % 34.30/12.84 tff(c_9315, plain, (![U_907]: (c10_2(U_907, a1954) | c1_2(U_907, a1949) | ~ssSkP9(U_907) | c10_1(U_907) | c3_2(U_907, a2025) | c3_2(U_907, a1949) | c2_2(U_907, a1949) | c2_1(U_907) | c1_1(U_907) | c8_1(U_907) | c5_1(U_907) | ~c7_1(U_907) | ~ndr1_1(U_907) | ~c4_2(U_907, a1898) | ~c10_2(U_907, a1898)))). % 34.30/12.84 tff(c_9297, plain, (![U_906]: (c3_2(U_906, a1954) | c1_2(U_906, a1949) | ~ssSkP9(U_906) | c10_1(U_906) | c3_2(U_906, a1949) | c2_2(U_906, a1949) | c2_1(U_906) | ~c1_2(U_906, a1898) | c1_1(U_906) | c8_1(U_906) | c5_1(U_906) | ~c7_1(U_906) | ~ndr1_1(U_906) | ~c4_2(U_906, a2025) | ~c10_2(U_906, a2025)))). % 34.30/12.84 tff(c_9281, plain, (![U_905]: (c10_2(U_905, a1954) | c1_2(U_905, a1949) | ~ssSkP9(U_905) | c10_1(U_905) | c3_2(U_905, a1949) | c2_2(U_905, a1949) | c2_1(U_905) | c2_2(U_905, a1898) | c1_1(U_905) | c8_1(U_905) | c5_1(U_905) | ~c7_1(U_905) | ~ndr1_1(U_905) | ~c4_2(U_905, a2025) | ~c10_2(U_905, a2025)))). % 34.30/12.84 tff(c_9314, plain, (![U_907]: (c3_2(U_907, a1954) | c1_2(U_907, a1949) | ~ssSkP9(U_907) | c10_1(U_907) | c3_2(U_907, a2025) | c3_2(U_907, a1949) | c2_2(U_907, a1949) | c2_1(U_907) | c1_1(U_907) | c8_1(U_907) | c5_1(U_907) | ~c7_1(U_907) | ~ndr1_1(U_907) | ~c4_2(U_907, a1898) | ~c10_2(U_907, a1898)))). % 34.30/12.84 tff(c_9298, plain, (![U_906]: (c10_2(U_906, a1954) | c1_2(U_906, a1949) | ~ssSkP9(U_906) | c10_1(U_906) | c3_2(U_906, a1949) | c2_2(U_906, a1949) | c2_1(U_906) | ~c1_2(U_906, a1898) | c1_1(U_906) | c8_1(U_906) | c5_1(U_906) | ~c7_1(U_906) | ~ndr1_1(U_906) | ~c4_2(U_906, a2025) | ~c10_2(U_906, a2025)))). % 34.30/12.85 tff(c_9325, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c2_1(U_440) | c5_2(U_440, a1949) | c1_1(U_440) | c8_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.85 tff(c_9198, plain, (![U_896]: (c10_2(U_896, a1954) | c1_2(U_896, a1843) | ~ssSkP9(U_896) | c10_1(U_896) | c3_2(U_896, a1843) | c2_2(U_896, a1843) | c2_1(U_896) | ~c1_2(U_896, a1898) | ssSkP3(U_896) | c5_1(U_896) | ~c7_1(U_896) | ~ndr1_1(U_896) | ~c4_2(U_896, a2025) | ~c10_2(U_896, a2025)))). % 34.30/12.85 tff(c_9162, plain, (![U_892]: (c10_2(U_892, a1954) | c1_2(U_892, a1843) | ~ssSkP9(U_892) | c10_1(U_892) | c3_2(U_892, a2025) | c3_2(U_892, a1843) | c2_2(U_892, a1843) | c2_1(U_892) | ssSkP3(U_892) | c5_1(U_892) | ~c7_1(U_892) | ~ndr1_1(U_892) | ~c4_2(U_892, a1898) | ~c10_2(U_892, a1898)))). % 34.30/12.85 tff(c_9180, plain, (![U_894]: (c10_2(U_894, a1954) | c1_2(U_894, a1843) | ~ssSkP9(U_894) | c10_1(U_894) | c3_2(U_894, a1843) | c2_2(U_894, a1843) | c2_1(U_894) | c2_2(U_894, a1898) | ssSkP3(U_894) | c5_1(U_894) | ~c7_1(U_894) | ~ndr1_1(U_894) | ~c4_2(U_894, a2025) | ~c10_2(U_894, a2025)))). % 34.30/12.85 tff(c_9163, plain, (![U_892]: (c3_2(U_892, a1954) | c1_2(U_892, a1843) | ~ssSkP9(U_892) | c10_1(U_892) | c3_2(U_892, a2025) | c3_2(U_892, a1843) | c2_2(U_892, a1843) | c2_1(U_892) | ssSkP3(U_892) | c5_1(U_892) | ~c7_1(U_892) | ~ndr1_1(U_892) | ~c4_2(U_892, a1898) | ~c10_2(U_892, a1898)))). % 34.30/12.85 tff(c_9181, plain, (![U_894]: (c3_2(U_894, a1954) | c1_2(U_894, a1843) | ~ssSkP9(U_894) | c10_1(U_894) | c3_2(U_894, a1843) | c2_2(U_894, a1843) | c2_1(U_894) | c2_2(U_894, a1898) | ssSkP3(U_894) | c5_1(U_894) | ~c7_1(U_894) | ~ndr1_1(U_894) | ~c4_2(U_894, a2025) | ~c10_2(U_894, a2025)))). % 34.30/12.85 tff(c_9199, plain, (![U_896]: (c3_2(U_896, a1954) | c1_2(U_896, a1843) | ~ssSkP9(U_896) | c10_1(U_896) | c3_2(U_896, a1843) | c2_2(U_896, a1843) | c2_1(U_896) | ~c1_2(U_896, a1898) | ssSkP3(U_896) | c5_1(U_896) | ~c7_1(U_896) | ~ndr1_1(U_896) | ~c4_2(U_896, a2025) | ~c10_2(U_896, a2025)))). % 34.30/12.85 tff(c_9219, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c2_1(U_440) | c5_2(U_440, a1843) | ssSkP3(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.85 tff(c_9002, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c2_1(U_440) | c5_2(U_440, a1949) | ~c6_2(U_440, a1898) | c1_1(U_440) | c8_1(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.85 tff(c_8922, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a2025) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c2_1(U_440) | c5_2(U_440, a1949) | c1_1(U_440) | c8_1(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.85 tff(c_9060, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c2_1(U_440) | c5_2(U_440, a1949) | ~c1_2(U_440, a1898) | c1_1(U_440) | c8_1(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.85 tff(c_9038, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c2_1(U_440) | c2_2(U_440, a1898) | c5_2(U_440, a1949) | c1_1(U_440) | c8_1(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.85 tff(c_8969, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c10_2(U_440, a1956) | ~c9_1(U_440) | c1_1(U_440) | c8_1(U_440) | ssSkP10(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.85 tff(c_8928, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | c10_2(U_440, a1980) | ~c9_1(U_440) | c1_1(U_440) | c8_1(U_440) | ssSkP11(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.85 tff(c_8916, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c10_2(U_440, a1927) | ~c9_1(U_440) | ssSkP3(U_440) | c2_1(U_440) | ~c1_1(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.85 tff(c_9066, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1949) | c2_2(U_440, a1949) | ~c5_2(U_440, a2025) | c2_1(U_440) | c5_2(U_440, a1949) | c1_1(U_440) | c8_1(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.85 tff(c_9051, plain, (![U_878]: (c10_2(U_878, a1954) | c1_2(U_878, a1949) | ~ssSkP9(U_878) | c10_1(U_878) | c3_2(U_878, a2025) | c3_2(U_878, a1949) | c2_2(U_878, a1949) | c2_1(U_878) | c2_2(U_878, a1898) | ~ndr1_1(U_878) | c1_1(U_878) | c8_1(U_878)))). % 34.30/12.85 tff(c_9029, plain, (![U_876]: (c10_2(U_876, a1954) | c1_2(U_876, a1949) | ~ssSkP9(U_876) | c10_1(U_876) | c3_2(U_876, a2025) | c3_2(U_876, a1949) | c2_2(U_876, a1949) | c2_1(U_876) | ~c1_2(U_876, a1898) | ~ndr1_1(U_876) | c1_1(U_876) | c8_1(U_876)))). % 34.30/12.85 tff(c_8713, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c2_1(U_440) | c5_2(U_440, a1843) | ~c6_2(U_440, a1898) | ssSkP3(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.86 tff(c_8792, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | ~c5_2(U_440, a2025) | c2_1(U_440) | c5_2(U_440, a1843) | ssSkP3(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.86 tff(c_8786, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c2_1(U_440) | c5_2(U_440, a1843) | ~c1_2(U_440, a1898) | ssSkP3(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.86 tff(c_9050, plain, (![U_878]: (c3_2(U_878, a1954) | c1_2(U_878, a1949) | ~ssSkP9(U_878) | c10_1(U_878) | c3_2(U_878, a2025) | c3_2(U_878, a1949) | c2_2(U_878, a1949) | c2_1(U_878) | c2_2(U_878, a1898) | ~ndr1_1(U_878) | c1_1(U_878) | c8_1(U_878)))). % 34.30/12.86 tff(c_8744, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c2_1(U_440) | c2_2(U_440, a1898) | c5_2(U_440, a1843) | ssSkP3(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.86 tff(c_9028, plain, (![U_876]: (c3_2(U_876, a1954) | c1_2(U_876, a1949) | ~ssSkP9(U_876) | c10_1(U_876) | c3_2(U_876, a2025) | c3_2(U_876, a1949) | c2_2(U_876, a1949) | c2_1(U_876) | ~c1_2(U_876, a1898) | ~ndr1_1(U_876) | c1_1(U_876) | c8_1(U_876)))). % 34.30/12.86 tff(c_8780, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a2025) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c2_1(U_440) | c5_2(U_440, a1843) | ssSkP3(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.86 tff(c_8725, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c10_2(U_440, a1956) | ~c9_1(U_440) | ssSkP3(U_440) | ssSkP10(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.86 tff(c_8719, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1843) | c2_2(U_440, a1843) | c10_2(U_440, a1980) | ~c9_1(U_440) | ssSkP3(U_440) | ssSkP11(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.86 tff(c_8451, plain, (![U_440]: (c9_1(U_440) | c10_2(U_440, a1843) | ~c4_1(U_440) | ~c1_2(U_440, a1843) | c2_1(U_440) | c5_2(U_440, a1843) | ssSkP3(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.86 tff(c_8601, plain, (![U_440]: (c9_1(U_440) | c10_2(U_440, a1947) | ~c4_1(U_440) | ~c1_2(U_440, a1947) | c2_1(U_440) | c5_2(U_440, a1947) | ssSkP8(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a1898) | ~c10_2(U_440, a1898)))). % 34.30/12.86 tff(c_8808, plain, (![U_853]: (c3_2(U_853, a1954) | c1_2(U_853, a1843) | ~ssSkP9(U_853) | c10_1(U_853) | c3_2(U_853, a2025) | c3_2(U_853, a1843) | c2_2(U_853, a1843) | c2_1(U_853) | ~c1_2(U_853, a1898) | ~ndr1_1(U_853) | ssSkP3(U_853)))). % 34.30/12.86 tff(c_8759, plain, (![U_848]: (c10_2(U_848, a1954) | c1_2(U_848, a1843) | ~ssSkP9(U_848) | c10_1(U_848) | c3_2(U_848, a2025) | c3_2(U_848, a1843) | c2_2(U_848, a1843) | c2_1(U_848) | c2_2(U_848, a1898) | ~ndr1_1(U_848) | ssSkP3(U_848)))). % 34.30/12.86 tff(c_8807, plain, (![U_853]: (c10_2(U_853, a1954) | c1_2(U_853, a1843) | ~ssSkP9(U_853) | c10_1(U_853) | c3_2(U_853, a2025) | c3_2(U_853, a1843) | c2_2(U_853, a1843) | c2_1(U_853) | ~c1_2(U_853, a1898) | ~ndr1_1(U_853) | ssSkP3(U_853)))). % 34.30/12.86 tff(c_8760, plain, (![U_848]: (c3_2(U_848, a1954) | c1_2(U_848, a1843) | ~ssSkP9(U_848) | c10_1(U_848) | c3_2(U_848, a2025) | c3_2(U_848, a1843) | c2_2(U_848, a1843) | c2_1(U_848) | c2_2(U_848, a1898) | ~ndr1_1(U_848) | ssSkP3(U_848)))). % 34.30/12.86 tff(c_8300, plain, (![U_821]: (c10_1(U_821) | c3_2(U_821, a1949) | ~c5_2(U_821, a2025) | c2_2(U_821, a1949) | c10_2(U_821, a1983) | ~c9_1(U_821) | ~ndr1_1(U_821) | c1_1(U_821) | c8_1(U_821) | ~c5_1(U_821) | ~c2_1(U_821)))). % 34.30/12.86 tff(c_8302, plain, (![U_821]: (c10_1(U_821) | c3_2(U_821, a1949) | ~c6_2(U_821, a2025) | c2_2(U_821, a1949) | c10_2(U_821, a1983) | ~c9_1(U_821) | ~ndr1_1(U_821) | c1_1(U_821) | c8_1(U_821) | ~c5_1(U_821) | ~c2_1(U_821)))). % 34.30/12.87 tff(c_8301, plain, (![U_821]: (c10_1(U_821) | c3_2(U_821, a2025) | c3_2(U_821, a1949) | c2_2(U_821, a1949) | c10_2(U_821, a1983) | ~c9_1(U_821) | ~ndr1_1(U_821) | c1_1(U_821) | c8_1(U_821) | ~c5_1(U_821) | ~c2_1(U_821)))). % 34.30/12.87 tff(c_7211, plain, (![U_787]: (c10_1(U_787) | c3_2(U_787, a1949) | c2_2(U_787, a1949) | ~c5_2(U_787, a2025) | c2_1(U_787) | c5_2(U_787, a1949) | ~c6_2(U_787, a1898) | ~ndr1_1(U_787) | c1_1(U_787) | c8_1(U_787)))). % 34.30/12.87 tff(c_7150, plain, (![U_786]: (c10_1(U_786) | c3_2(U_786, a1949) | c2_2(U_786, a1949) | ~c6_2(U_786, a2025) | c2_1(U_786) | c5_2(U_786, a1949) | ~c1_2(U_786, a1898) | ~ndr1_1(U_786) | c1_1(U_786) | c8_1(U_786)))). % 34.30/12.87 tff(c_7288, plain, (![U_790]: (c10_1(U_790) | c3_2(U_790, a2025) | c3_2(U_790, a1949) | c2_2(U_790, a1949) | c2_1(U_790) | c2_2(U_790, a1898) | c5_2(U_790, a1949) | ~ndr1_1(U_790) | c1_1(U_790) | c8_1(U_790)))). % 34.30/12.87 tff(c_7289, plain, (![U_790]: (c10_1(U_790) | c3_2(U_790, a1949) | c2_2(U_790, a1949) | ~c6_2(U_790, a2025) | c2_1(U_790) | c2_2(U_790, a1898) | c5_2(U_790, a1949) | ~ndr1_1(U_790) | c1_1(U_790) | c8_1(U_790)))). % 34.30/12.87 tff(c_7149, plain, (![U_786]: (c10_1(U_786) | c3_2(U_786, a2025) | c3_2(U_786, a1949) | c2_2(U_786, a1949) | c2_1(U_786) | c5_2(U_786, a1949) | ~c1_2(U_786, a1898) | ~ndr1_1(U_786) | c1_1(U_786) | c8_1(U_786)))). % 34.30/12.87 tff(c_7287, plain, (![U_790]: (c10_1(U_790) | c3_2(U_790, a1949) | c2_2(U_790, a1949) | ~c5_2(U_790, a2025) | c2_1(U_790) | c2_2(U_790, a1898) | c5_2(U_790, a1949) | ~ndr1_1(U_790) | c1_1(U_790) | c8_1(U_790)))). % 34.30/12.87 tff(c_7213, plain, (![U_787]: (c10_1(U_787) | c3_2(U_787, a1949) | c2_2(U_787, a1949) | ~c6_2(U_787, a2025) | c2_1(U_787) | c5_2(U_787, a1949) | ~c6_2(U_787, a1898) | ~ndr1_1(U_787) | c1_1(U_787) | c8_1(U_787)))). % 34.30/12.87 tff(c_7148, plain, (![U_786]: (c10_1(U_786) | c3_2(U_786, a1949) | c2_2(U_786, a1949) | ~c5_2(U_786, a2025) | c2_1(U_786) | c5_2(U_786, a1949) | ~c1_2(U_786, a1898) | ~ndr1_1(U_786) | c1_1(U_786) | c8_1(U_786)))). % 34.30/12.87 tff(c_8022, plain, (![U_814]: (c10_1(U_814) | c3_2(U_814, a1949) | ~c5_2(U_814, a2025) | c2_2(U_814, a1949) | c10_2(U_814, a1956) | ~c9_1(U_814) | ~ndr1_1(U_814) | c1_1(U_814) | c8_1(U_814) | ssSkP10(U_814)))). % 34.30/12.87 tff(c_8024, plain, (![U_814]: (c10_1(U_814) | c3_2(U_814, a1949) | ~c6_2(U_814, a2025) | c2_2(U_814, a1949) | c10_2(U_814, a1956) | ~c9_1(U_814) | ~ndr1_1(U_814) | c1_1(U_814) | c8_1(U_814) | ssSkP10(U_814)))). % 34.30/12.87 tff(c_7962, plain, (![U_813]: (c10_1(U_813) | c3_2(U_813, a2025) | c3_2(U_813, a1949) | c2_2(U_813, a1949) | c10_2(U_813, a1980) | ~c9_1(U_813) | ~ndr1_1(U_813) | c1_1(U_813) | c8_1(U_813) | ssSkP11(U_813)))). % 34.30/12.87 tff(c_7961, plain, (![U_813]: (c10_1(U_813) | c3_2(U_813, a1949) | ~c5_2(U_813, a2025) | c2_2(U_813, a1949) | c10_2(U_813, a1980) | ~c9_1(U_813) | ~ndr1_1(U_813) | c1_1(U_813) | c8_1(U_813) | ssSkP11(U_813)))). % 34.30/12.87 tff(c_7829, plain, (![U_809]: (c10_1(U_809) | c3_2(U_809, a1843) | ~c6_2(U_809, a2025) | c2_2(U_809, a1843) | c10_2(U_809, a1983) | ~c9_1(U_809) | ~ndr1_1(U_809) | ssSkP3(U_809) | ~c5_1(U_809) | ~c2_1(U_809)))). % 34.30/12.88 tff(c_8023, plain, (![U_814]: (c10_1(U_814) | c3_2(U_814, a2025) | c3_2(U_814, a1949) | c2_2(U_814, a1949) | c10_2(U_814, a1956) | ~c9_1(U_814) | ~ndr1_1(U_814) | c1_1(U_814) | c8_1(U_814) | ssSkP10(U_814)))). % 34.30/12.88 tff(c_7827, plain, (![U_809]: (c10_1(U_809) | c3_2(U_809, a1843) | ~c5_2(U_809, a2025) | c2_2(U_809, a1843) | c10_2(U_809, a1983) | ~c9_1(U_809) | ~ndr1_1(U_809) | ssSkP3(U_809) | ~c5_1(U_809) | ~c2_1(U_809)))). % 34.30/12.88 tff(c_7828, plain, (![U_809]: (c10_1(U_809) | c3_2(U_809, a2025) | c3_2(U_809, a1843) | c2_2(U_809, a1843) | c10_2(U_809, a1983) | ~c9_1(U_809) | ~ndr1_1(U_809) | ssSkP3(U_809) | ~c5_1(U_809) | ~c2_1(U_809)))). % 34.30/12.88 tff(c_7963, plain, (![U_813]: (c10_1(U_813) | c3_2(U_813, a1949) | ~c6_2(U_813, a2025) | c2_2(U_813, a1949) | c10_2(U_813, a1980) | ~c9_1(U_813) | ~ndr1_1(U_813) | c1_1(U_813) | c8_1(U_813) | ssSkP11(U_813)))). % 34.30/12.88 tff(c_7212, plain, (![U_787]: (c10_1(U_787) | c3_2(U_787, a2025) | c3_2(U_787, a1949) | c2_2(U_787, a1949) | c2_1(U_787) | c5_2(U_787, a1949) | ~c6_2(U_787, a1898) | ~ndr1_1(U_787) | c1_1(U_787) | c8_1(U_787)))). % 34.30/12.88 tff(c_7767, plain, (![U_808]: (c10_1(U_808) | c3_2(U_808, a1843) | ~c6_2(U_808, a2025) | c2_2(U_808, a1843) | c10_2(U_808, a1927) | ~c9_1(U_808) | ~ndr1_1(U_808) | ssSkP3(U_808) | c2_1(U_808) | ~c1_1(U_808)))). % 34.30/12.88 tff(c_7765, plain, (![U_808]: (c10_1(U_808) | c3_2(U_808, a1843) | ~c5_2(U_808, a2025) | c2_2(U_808, a1843) | c10_2(U_808, a1927) | ~c9_1(U_808) | ~ndr1_1(U_808) | ssSkP3(U_808) | c2_1(U_808) | ~c1_1(U_808)))). % 34.30/12.88 tff(c_7766, plain, (![U_808]: (c10_1(U_808) | c3_2(U_808, a2025) | c3_2(U_808, a1843) | c2_2(U_808, a1843) | c10_2(U_808, a1927) | ~c9_1(U_808) | ~ndr1_1(U_808) | ssSkP3(U_808) | c2_1(U_808) | ~c1_1(U_808)))). % 34.30/12.88 tff(c_7249, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1864) | c2_2(U_440, a1864) | ~c8_1(U_440) | ~ssSkP5(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.88 tff(c_7094, plain, (![U_300]: (c10_2(U_300, a1954) | c1_2(U_300, a1949) | ~ssSkP9(U_300) | c1_1(U_300) | c8_1(U_300) | c4_2(U_300, a1949) | c3_2(U_300, a1949) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_7570, plain, (![U_300]: (c3_2(U_300, a1954) | c1_2(U_300, a1864) | ~ssSkP9(U_300) | ~c8_1(U_300) | ~ssSkP5(U_300) | c4_2(U_300, a1864) | c3_2(U_300, a1864) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_7352, plain, (![U_300]: (c3_2(U_300, a1954) | c1_2(U_300, a1949) | ~ssSkP9(U_300) | c1_1(U_300) | c8_1(U_300) | c4_2(U_300, a1949) | c3_2(U_300, a1949) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_7381, plain, (![U_300]: (c10_2(U_300, a1954) | c1_2(U_300, a1864) | ~ssSkP9(U_300) | ~c8_1(U_300) | ~ssSkP5(U_300) | c4_2(U_300, a1864) | c3_2(U_300, a1864) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_6151, plain, (![U_740]: (c10_1(U_740) | c3_2(U_740, a1843) | c2_2(U_740, a1843) | ~c5_2(U_740, a2025) | c2_1(U_740) | c2_2(U_740, a1898) | c5_2(U_740, a1843) | ~ndr1_1(U_740) | ssSkP3(U_740)))). % 34.30/12.88 tff(c_6754, plain, (![U_757]: (c10_1(U_757) | c3_2(U_757, a2025) | c3_2(U_757, a1843) | c2_2(U_757, a1843) | c2_1(U_757) | c5_2(U_757, a1843) | ~c1_2(U_757, a1898) | ~ndr1_1(U_757) | ssSkP3(U_757)))). % 34.30/12.88 tff(c_6545, plain, (![U_748]: (c10_1(U_748) | c3_2(U_748, a1843) | c2_2(U_748, a1843) | ~c5_2(U_748, a2025) | c2_1(U_748) | c5_2(U_748, a1843) | ~c6_2(U_748, a1898) | ~ndr1_1(U_748) | ssSkP3(U_748)))). % 34.30/12.88 tff(c_6755, plain, (![U_757]: (c10_1(U_757) | c3_2(U_757, a1843) | c2_2(U_757, a1843) | ~c6_2(U_757, a2025) | c2_1(U_757) | c5_2(U_757, a1843) | ~c1_2(U_757, a1898) | ~ndr1_1(U_757) | ssSkP3(U_757)))). % 34.30/12.88 tff(c_6546, plain, (![U_748]: (c10_1(U_748) | c3_2(U_748, a2025) | c3_2(U_748, a1843) | c2_2(U_748, a1843) | c2_1(U_748) | c5_2(U_748, a1843) | ~c6_2(U_748, a1898) | ~ndr1_1(U_748) | ssSkP3(U_748)))). % 34.30/12.88 tff(c_6753, plain, (![U_757]: (c10_1(U_757) | c3_2(U_757, a1843) | c2_2(U_757, a1843) | ~c5_2(U_757, a2025) | c2_1(U_757) | c5_2(U_757, a1843) | ~c1_2(U_757, a1898) | ~ndr1_1(U_757) | ssSkP3(U_757)))). % 34.30/12.88 tff(c_6152, plain, (![U_740]: (c10_1(U_740) | c3_2(U_740, a2025) | c3_2(U_740, a1843) | c2_2(U_740, a1843) | c2_1(U_740) | c2_2(U_740, a1898) | c5_2(U_740, a1843) | ~ndr1_1(U_740) | ssSkP3(U_740)))). % 34.30/12.88 tff(c_6153, plain, (![U_740]: (c10_1(U_740) | c3_2(U_740, a1843) | c2_2(U_740, a1843) | ~c6_2(U_740, a2025) | c2_1(U_740) | c2_2(U_740, a1898) | c5_2(U_740, a1843) | ~ndr1_1(U_740) | ssSkP3(U_740)))). % 34.30/12.88 tff(c_6974, plain, (![U_775]: (c10_1(U_775) | c3_2(U_775, a1843) | ~c5_2(U_775, a2025) | c2_2(U_775, a1843) | c10_2(U_775, a1980) | ~c9_1(U_775) | ~ndr1_1(U_775) | ssSkP3(U_775) | ssSkP11(U_775)))). % 34.30/12.88 tff(c_7052, plain, (![U_779]: (c10_1(U_779) | c3_2(U_779, a1843) | ~c6_2(U_779, a2025) | c2_2(U_779, a1843) | c10_2(U_779, a1956) | ~c9_1(U_779) | ~ndr1_1(U_779) | ssSkP3(U_779) | ssSkP10(U_779)))). % 34.30/12.88 tff(c_6976, plain, (![U_775]: (c10_1(U_775) | c3_2(U_775, a1843) | ~c6_2(U_775, a2025) | c2_2(U_775, a1843) | c10_2(U_775, a1980) | ~c9_1(U_775) | ~ndr1_1(U_775) | ssSkP3(U_775) | ssSkP11(U_775)))). % 34.30/12.88 tff(c_6547, plain, (![U_748]: (c10_1(U_748) | c3_2(U_748, a1843) | c2_2(U_748, a1843) | ~c6_2(U_748, a2025) | c2_1(U_748) | c5_2(U_748, a1843) | ~c6_2(U_748, a1898) | ~ndr1_1(U_748) | ssSkP3(U_748)))). % 34.30/12.88 tff(c_7050, plain, (![U_779]: (c10_1(U_779) | c3_2(U_779, a1843) | ~c5_2(U_779, a2025) | c2_2(U_779, a1843) | c10_2(U_779, a1956) | ~c9_1(U_779) | ~ndr1_1(U_779) | ssSkP3(U_779) | ssSkP10(U_779)))). % 34.30/12.88 tff(c_6975, plain, (![U_775]: (c10_1(U_775) | c3_2(U_775, a2025) | c3_2(U_775, a1843) | c2_2(U_775, a1843) | c10_2(U_775, a1980) | ~c9_1(U_775) | ~ndr1_1(U_775) | ssSkP3(U_775) | ssSkP11(U_775)))). % 34.30/12.88 tff(c_7051, plain, (![U_779]: (c10_1(U_779) | c3_2(U_779, a2025) | c3_2(U_779, a1843) | c2_2(U_779, a1843) | c10_2(U_779, a1956) | ~c9_1(U_779) | ~ndr1_1(U_779) | ssSkP3(U_779) | ssSkP10(U_779)))). % 34.30/12.88 tff(c_6813, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1956) | c2_2(U_440, a1956) | ssSkP10(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.88 tff(c_6871, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a2031) | c2_2(U_440, a2031) | ssSkP16(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.88 tff(c_6819, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1992) | c2_2(U_440, a1992) | ssSkP14(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.88 tff(c_6838, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1863) | c2_2(U_440, a1863) | ssSkP5(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.88 tff(c_6877, plain, (![U_440]: (c10_1(U_440) | c3_2(U_440, a1984) | c2_2(U_440, a1984) | ssSkP12(U_440) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, a2025) | ~c10_2(U_440, a2025)))). % 34.30/12.88 tff(c_6236, plain, (![U_300]: (c3_2(U_300, a1954) | c1_2(U_300, a1947) | ~ssSkP9(U_300) | ssSkP8(U_300) | c4_2(U_300, a1947) | c3_2(U_300, a1947) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_6647, plain, (![U_32]: (c9_1(U_32) | c10_2(U_32, a1947) | ~c4_1(U_32) | ~c1_2(U_32, a1947) | c2_1(U_32) | c5_2(U_32, a1947) | ~c6_2(U_32, a1898) | ~ndr1_1(U_32) | ssSkP8(U_32)))). % 34.30/12.88 tff(c_6707, plain, (![U_300]: (c3_2(U_300, a1954) | c1_2(U_300, a1834) | ~ssSkP9(U_300) | ssSkP0(U_300) | c4_2(U_300, a1834) | c3_2(U_300, a1834) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_6109, plain, (![U_300]: (c10_2(U_300, a1954) | c1_2(U_300, a1843) | ~ssSkP9(U_300) | ssSkP3(U_300) | c4_2(U_300, a1843) | c3_2(U_300, a1843) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_6096, plain, (![U_300]: (c10_2(U_300, a1954) | c1_2(U_300, a1834) | ~ssSkP9(U_300) | ssSkP0(U_300) | c4_2(U_300, a1834) | c3_2(U_300, a1834) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_4633, plain, (![U_300]: (c3_2(U_300, a1954) | c1_2(U_300, a1837) | ~ssSkP9(U_300) | ssSkP2(U_300) | c4_2(U_300, a1837) | c3_2(U_300, a1837) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_8491, plain, (~c1_2(a1988, a1947))). % 34.30/12.88 tff(c_6208, plain, (![U_300]: (c10_2(U_300, a1954) | c1_2(U_300, a1837) | ~ssSkP9(U_300) | ssSkP2(U_300) | c4_2(U_300, a1837) | c3_2(U_300, a1837) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.88 tff(c_6646, plain, (![U_32]: (c9_1(U_32) | c10_2(U_32, a1947) | ~c4_1(U_32) | ~c1_2(U_32, a1947) | c2_1(U_32) | c2_2(U_32, a1898) | c5_2(U_32, a1947) | ~ndr1_1(U_32) | ssSkP8(U_32)))). % 34.30/12.88 tff(c_6645, plain, (![U_40]: (c9_1(U_40) | c10_2(U_40, a1843) | ~c4_1(U_40) | ~c1_2(U_40, a1843) | c2_1(U_40) | c5_2(U_40, a1843) | ~c6_2(U_40, a1898) | ~ndr1_1(U_40) | ssSkP3(U_40)))). % 34.30/12.89 tff(c_8445, plain, (~c1_2(a1988, a1898))). % 34.30/12.89 tff(c_6649, plain, (![U_32]: (c9_1(U_32) | c10_2(U_32, a1947) | ~c4_1(U_32) | ~c1_2(U_32, a1947) | c2_1(U_32) | c5_2(U_32, a1947) | ~c1_2(U_32, a1898) | ~ndr1_1(U_32) | ssSkP8(U_32)))). % 34.30/12.89 tff(c_4642, plain, (![U_300]: (c10_2(U_300, a1954) | c1_2(U_300, a1947) | ~ssSkP9(U_300) | ssSkP8(U_300) | c4_2(U_300, a1947) | c3_2(U_300, a1947) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.89 tff(c_6752, plain, (![U_757]: (c9_1(U_757) | c10_2(U_757, a1843) | ~c4_1(U_757) | ~c1_2(U_757, a1843) | c2_1(U_757) | c5_2(U_757, a1843) | ~c1_2(U_757, a1898) | ~ndr1_1(U_757) | ssSkP3(U_757)))). % 34.30/12.89 tff(c_8071, plain, (![U_169]: (c2_2(U_169, a1994) | c8_2(U_169, a1994) | c10_2(U_169, a1983) | ~c9_1(U_169) | ~ndr1_1(U_169) | c4_1(U_169) | ~c10_1(U_169) | ~c5_1(U_169) | ~c2_1(U_169)))). % 34.30/12.89 tff(c_7911, plain, (![U_169]: (c2_2(U_169, a1949) | c8_2(U_169, a1949) | c10_2(U_169, a1983) | ~c9_1(U_169) | ~ndr1_1(U_169) | c1_1(U_169) | c8_1(U_169) | ~c5_1(U_169) | ~c2_1(U_169)))). % 34.30/12.89 tff(c_8072, plain, (![U_109]: (c2_2(U_109, a1994) | c8_2(U_109, a1994) | c10_2(U_109, a1927) | ~c9_1(U_109) | ~ndr1_1(U_109) | c4_1(U_109) | ~c10_1(U_109) | c2_1(U_109) | ~c1_1(U_109)))). % 34.30/12.89 tff(c_8207, plain, (~c1_2(a1988, a1843))). % 34.30/12.89 tff(c_8206, plain, (~c9_1(a2014))). % 34.30/12.89 tff(c_8189, plain, (~c9_1(a1913))). % 34.30/12.89 tff(c_6648, plain, (![U_40]: (c9_1(U_40) | c10_2(U_40, a1843) | ~c4_1(U_40) | ~c1_2(U_40, a1843) | c2_1(U_40) | c2_2(U_40, a1898) | c5_2(U_40, a1843) | ~ndr1_1(U_40) | ssSkP3(U_40)))). % 34.30/12.89 tff(c_8074, plain, (![U_29]: (c2_2(U_29, a1994) | c8_2(U_29, a1994) | c10_2(U_29, a1956) | ~c9_1(U_29) | ~ndr1_1(U_29) | c4_1(U_29) | ~c10_1(U_29) | ssSkP10(U_29)))). % 34.30/12.89 tff(c_8073, plain, (![U_25]: (c2_2(U_25, a1994) | c8_2(U_25, a1994) | c10_2(U_25, a1980) | ~c9_1(U_25) | ~ndr1_1(U_25) | c4_1(U_25) | ~c10_1(U_25) | ssSkP11(U_25)))). % 34.30/12.89 tff(c_5585, plain, (![U_119, V_723]: (c2_2(U_119, a1994) | c8_2(U_119, a1994) | c10_2(U_119, V_723) | ~c9_1(U_119) | ~ndr1_1(U_119) | ~c1_2(U_119, V_723) | c4_1(U_119) | ~c10_1(U_119)))). % 34.30/12.89 tff(c_7914, plain, (![U_29]: (c2_2(U_29, a1949) | c8_2(U_29, a1949) | c10_2(U_29, a1956) | ~c9_1(U_29) | ~ndr1_1(U_29) | c1_1(U_29) | c8_1(U_29) | ssSkP10(U_29)))). % 34.30/12.89 tff(c_7913, plain, (![U_25]: (c2_2(U_25, a1949) | c8_2(U_25, a1949) | c10_2(U_25, a1980) | ~c9_1(U_25) | ~ndr1_1(U_25) | c1_1(U_25) | c8_1(U_25) | ssSkP11(U_25)))). % 34.30/12.89 tff(c_5581, plain, (![U_87, V_723]: (c2_2(U_87, a1949) | c8_2(U_87, a1949) | c10_2(U_87, V_723) | ~c9_1(U_87) | ~ndr1_1(U_87) | ~c1_2(U_87, V_723) | c1_1(U_87) | c8_1(U_87)))). % 34.30/12.89 tff(c_7885, plain, (~c7_1(a2029))). % 34.30/12.89 tff(c_4627, plain, (![U_300]: (c3_2(U_300, a1954) | c1_2(U_300, a1843) | ~ssSkP9(U_300) | ssSkP3(U_300) | c4_2(U_300, a1843) | c3_2(U_300, a1843) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.30/12.89 tff(c_6916, plain, (![U_169]: (c2_2(U_169, a1843) | c8_2(U_169, a1843) | c10_2(U_169, a1983) | ~c9_1(U_169) | ~ndr1_1(U_169) | ssSkP3(U_169) | ~c5_1(U_169) | ~c2_1(U_169)))). % 34.30/12.89 tff(c_6917, plain, (![U_109]: (c2_2(U_109, a1843) | c8_2(U_109, a1843) | c10_2(U_109, a1927) | ~c9_1(U_109) | ~ndr1_1(U_109) | ssSkP3(U_109) | c2_1(U_109) | ~c1_1(U_109)))). % 34.30/12.89 tff(c_7706, plain, (![U_27]: (c2_1(U_27) | ~c1_2(U_27, a1980) | ~c3_2(U_27, a1980) | c5_1(U_27) | ~c7_1(U_27) | ~ndr1_1(U_27) | ~c10_2(U_27, a1980) | ssSkP11(U_27)))). % 34.30/12.89 tff(c_5962, plain, (![U_440, V_441]: (c2_1(U_440) | ~c1_2(U_440, V_441) | ~c3_2(U_440, V_441) | c5_1(U_440) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, V_441) | ~c10_2(U_440, V_441)))). % 34.30/12.89 tff(c_5177, plain, (![U_131]: (c10_1(U_131) | c3_2(U_131, a1864) | c2_2(U_131, a1864) | ~c5_2(U_131, a2025) | ~ndr1_1(U_131) | ~c8_1(U_131) | ~ssSkP5(U_131)))). % 34.30/12.89 tff(c_5084, plain, (![U_173]: (c10_1(U_173) | c3_2(U_173, a2025) | c3_2(U_173, a1929) | c2_2(U_173, a1929) | ~ndr1_1(U_173) | ~c2_1(U_173) | ~c5_1(U_173)))). % 34.30/12.89 tff(c_7624, plain, (~c9_1(a2006))). % 34.30/12.89 tff(c_5176, plain, (![U_173]: (c10_1(U_173) | c3_2(U_173, a1929) | c2_2(U_173, a1929) | ~c5_2(U_173, a2025) | ~ndr1_1(U_173) | ~c2_1(U_173) | ~c5_1(U_173)))). % 34.30/12.89 tff(c_5175, plain, (![U_168]: (c10_1(U_168) | c3_2(U_168, a1983) | c2_2(U_168, a1983) | ~c5_2(U_168, a2025) | ~ndr1_1(U_168) | ~c5_1(U_168) | ~c2_1(U_168)))). % 34.30/12.89 tff(c_7597, plain, (~c9_1(a1871))). % 34.30/12.89 tff(c_4962, plain, (![U_173]: (c10_1(U_173) | c3_2(U_173, a1929) | c2_2(U_173, a1929) | ~c6_2(U_173, a2025) | ~ndr1_1(U_173) | ~c2_1(U_173) | ~c5_1(U_173)))). % 34.30/12.89 tff(c_4961, plain, (![U_168]: (c10_1(U_168) | c3_2(U_168, a1983) | c2_2(U_168, a1983) | ~c6_2(U_168, a2025) | ~ndr1_1(U_168) | ~c5_1(U_168) | ~c2_1(U_168)))). % 34.30/12.89 tff(c_7584, plain, (~c7_1(a2017))). % 34.30/12.89 tff(c_5085, plain, (![U_131]: (c10_1(U_131) | c3_2(U_131, a2025) | c3_2(U_131, a1864) | c2_2(U_131, a1864) | ~ndr1_1(U_131) | ~c8_1(U_131) | ~ssSkP5(U_131)))). % 34.30/12.90 tff(c_7571, plain, (~ssSkP9(a2017))). % 34.30/12.90 tff(c_4450, plain, (![U_132]: (c3_2(U_132, a1954) | c1_2(U_132, a1864) | ~ndr1_1(U_132) | ~c5_2(U_132, a1864) | ~ssSkP9(U_132) | ~c8_1(U_132) | ~ssSkP5(U_132)))). % 34.30/12.90 tff(c_4157, plain, (![U_88]: (c5_2(U_88, a1954) | c1_2(U_88, a1949) | ~ndr1_1(U_88) | ~c5_2(U_88, a1949) | ~ssSkP9(U_88) | c1_1(U_88) | c8_1(U_88)))). % 34.30/12.90 tff(c_7549, plain, (~c10_1(a1851))). % 34.30/12.90 tff(c_7548, plain, (~c3_2(a2029, a1994))). % 34.30/12.90 tff(c_7547, plain, (~c3_2(a1939, a1994))). % 34.30/12.90 tff(c_4236, plain, (![U_119]: (c2_1(U_119) | c2_2(U_119, a1898) | c5_2(U_119, a1994) | c8_2(U_119, a1994) | ~ndr1_1(U_119) | c4_1(U_119) | ~c10_1(U_119)))). % 34.30/12.90 tff(c_4377, plain, (![U_119]: (c2_1(U_119) | c5_2(U_119, a1994) | c8_2(U_119, a1994) | ~c1_2(U_119, a1898) | ~ndr1_1(U_119) | c4_1(U_119) | ~c10_1(U_119)))). % 34.30/12.90 tff(c_4304, plain, (![U_119]: (c2_1(U_119) | c5_2(U_119, a1994) | c8_2(U_119, a1994) | ~c6_2(U_119, a1898) | ~ndr1_1(U_119) | c4_1(U_119) | ~c10_1(U_119)))). % 34.30/12.90 tff(c_4559, plain, (![U_132]: (c10_2(U_132, a1954) | c1_2(U_132, a1864) | ~ndr1_1(U_132) | ~c5_2(U_132, a1864) | ~ssSkP9(U_132) | ~c8_1(U_132) | ~ssSkP5(U_132)))). % 34.30/12.90 tff(c_7356, plain, (~c4_2(a1875, a1949))). % 34.30/12.90 tff(c_7355, plain, (c8_1(a1924))). % 34.30/12.90 tff(c_7354, plain, (~c3_2(a1939, a1949))). % 34.30/12.90 tff(c_7353, plain, (~c3_2(a2029, a1949))). % 34.30/12.90 tff(c_7330, plain, (~c7_1(a1851))). % 34.30/12.90 tff(c_4449, plain, (![U_88]: (c3_2(U_88, a1954) | c1_2(U_88, a1949) | ~ndr1_1(U_88) | ~c5_2(U_88, a1949) | ~ssSkP9(U_88) | c1_1(U_88) | c8_1(U_88)))). % 34.30/12.90 tff(c_7320, plain, (~ssSkP9(a1851))). % 34.30/12.90 tff(c_7312, plain, (c5_2(a1851, a1949))). % 34.30/12.90 tff(c_4232, plain, (![U_87]: (c2_1(U_87) | c2_2(U_87, a1898) | c5_2(U_87, a1949) | c8_2(U_87, a1949) | ~ndr1_1(U_87) | c1_1(U_87) | c8_1(U_87)))). % 34.30/12.90 tff(c_4963, plain, (![U_131]: (c10_1(U_131) | c3_2(U_131, a1864) | c2_2(U_131, a1864) | ~c6_2(U_131, a2025) | ~ndr1_1(U_131) | ~c8_1(U_131) | ~ssSkP5(U_131)))). % 34.30/12.90 tff(c_4158, plain, (![U_132]: (c5_2(U_132, a1954) | c1_2(U_132, a1864) | ~ndr1_1(U_132) | ~c5_2(U_132, a1864) | ~ssSkP9(U_132) | ~c8_1(U_132) | ~ssSkP5(U_132)))). % 34.30/12.90 tff(c_4300, plain, (![U_87]: (c2_1(U_87) | c5_2(U_87, a1949) | c8_2(U_87, a1949) | ~c6_2(U_87, a1898) | ~ndr1_1(U_87) | c1_1(U_87) | c8_1(U_87)))). % 34.30/12.90 tff(c_4373, plain, (![U_87]: (c2_1(U_87) | c5_2(U_87, a1949) | c8_2(U_87, a1949) | ~c1_2(U_87, a1898) | ~ndr1_1(U_87) | c1_1(U_87) | c8_1(U_87)))). % 34.30/12.90 tff(c_5083, plain, (![U_168]: (c10_1(U_168) | c3_2(U_168, a2025) | c3_2(U_168, a1983) | c2_2(U_168, a1983) | ~ndr1_1(U_168) | ~c5_1(U_168) | ~c2_1(U_168)))). % 34.30/12.90 tff(c_7104, plain, (~c7_1(a1988))). % 34.30/12.90 tff(c_7081, plain, (~ssSkP9(a1988))). % 34.30/12.90 tff(c_4558, plain, (![U_88]: (c10_2(U_88, a1954) | c1_2(U_88, a1949) | ~ndr1_1(U_88) | ~c5_2(U_88, a1949) | ~ssSkP9(U_88) | c1_1(U_88) | c8_1(U_88)))). % 34.30/12.90 tff(c_5963, plain, (![U_145]: (c2_1(U_145) | c5_1(U_145) | ~ndr1_1(U_145) | ~c1_2(U_145, a1957) | ~c3_2(U_145, a1957) | ~c8_1(U_145) | ~ssSkP10(U_145)))). % 34.30/12.90 tff(c_5964, plain, (![U_137]: (c2_1(U_137) | c5_1(U_137) | ~ndr1_1(U_137) | ~c1_2(U_137, a2018) | ~c3_2(U_137, a2018) | c10_1(U_137) | c8_1(U_137)))). % 34.30/12.90 tff(c_7077, plain, (![U_122]: (c2_1(U_122) | c5_1(U_122) | ~ndr1_1(U_122) | ~c1_2(U_122, a1962) | c8_1(U_122) | ~c1_1(U_122)))). % 34.30/12.90 tff(c_6919, plain, (![U_29]: (c2_2(U_29, a1843) | c8_2(U_29, a1843) | c10_2(U_29, a1956) | ~c9_1(U_29) | ~ndr1_1(U_29) | ssSkP3(U_29) | ssSkP10(U_29)))). % 34.30/12.90 tff(c_7011, plain, (![U_169]: (c9_1(U_169) | c10_2(U_169, a1983) | ~c4_1(U_169) | ~ndr1_1(U_169) | ~c5_1(U_169) | ~c2_1(U_169)))). % 34.30/12.90 tff(c_6665, plain, (![U_173]: (c9_1(U_173) | c10_2(U_173, a1929) | ~c4_1(U_173) | ~ndr1_1(U_173) | ~c1_2(U_173, a1929) | ~c2_1(U_173) | ~c5_1(U_173)))). % 34.30/12.90 tff(c_6999, plain, (c2_2(a1913, a1898))). % 34.30/12.90 tff(c_6998, plain, (~c1_2(a1913, a1898))). % 34.30/12.90 tff(c_6997, plain, (~c9_1(a1998))). % 34.30/12.90 tff(c_6918, plain, (![U_25]: (c2_2(U_25, a1843) | c8_2(U_25, a1843) | c10_2(U_25, a1980) | ~c9_1(U_25) | ~ndr1_1(U_25) | ssSkP3(U_25) | ssSkP11(U_25)))). % 34.30/12.90 tff(c_6936, plain, (~c10_2(a1913, a1898))). % 34.30/12.90 tff(c_6929, plain, (~c6_2(a1913, a1898))). % 34.30/12.90 tff(c_6928, plain, (~c9_1(a1892))). % 34.30/12.90 tff(c_6927, plain, (~c9_1(a1915))). % 34.30/12.90 tff(c_5586, plain, (![U_40, V_723]: (c2_2(U_40, a1843) | c8_2(U_40, a1843) | c10_2(U_40, V_723) | ~c9_1(U_40) | ~ndr1_1(U_40) | ~c1_2(U_40, V_723) | ssSkP3(U_40)))). % 34.30/12.90 tff(c_5185, plain, (![U_28]: (c10_1(U_28) | c3_2(U_28, a1956) | c2_2(U_28, a1956) | ~c5_2(U_28, a2025) | ~ndr1_1(U_28) | ssSkP10(U_28)))). % 34.30/12.90 tff(c_4965, plain, (![U_23]: (c10_1(U_23) | c3_2(U_23, a1984) | c2_2(U_23, a1984) | ~c6_2(U_23, a2025) | ~ndr1_1(U_23) | ssSkP12(U_23)))). % 34.30/12.90 tff(c_4966, plain, (![U_18]: (c10_1(U_18) | c3_2(U_18, a2031) | c2_2(U_18, a2031) | ~c6_2(U_18, a2025) | ~ndr1_1(U_18) | ssSkP16(U_18)))). % 34.30/12.90 tff(c_5092, plain, (![U_20]: (c10_1(U_20) | c3_2(U_20, a2025) | c3_2(U_20, a1992) | c2_2(U_20, a1992) | ~ndr1_1(U_20) | ssSkP14(U_20)))). % 34.30/12.90 tff(c_5184, plain, (![U_20]: (c10_1(U_20) | c3_2(U_20, a1992) | c2_2(U_20, a1992) | ~c5_2(U_20, a2025) | ~ndr1_1(U_20) | ssSkP14(U_20)))). % 34.30/12.90 tff(c_5180, plain, (![U_18]: (c10_1(U_18) | c3_2(U_18, a2031) | c2_2(U_18, a2031) | ~c5_2(U_18, a2025) | ~ndr1_1(U_18) | ssSkP16(U_18)))). % 34.30/12.90 tff(c_4964, plain, (![U_36]: (c10_1(U_36) | c3_2(U_36, a1863) | c2_2(U_36, a1863) | ~c6_2(U_36, a2025) | ~ndr1_1(U_36) | ssSkP5(U_36)))). % 34.30/12.90 tff(c_5178, plain, (![U_36]: (c10_1(U_36) | c3_2(U_36, a1863) | c2_2(U_36, a1863) | ~c5_2(U_36, a2025) | ~ndr1_1(U_36) | ssSkP5(U_36)))). % 34.30/12.90 tff(c_4970, plain, (![U_20]: (c10_1(U_20) | c3_2(U_20, a1992) | c2_2(U_20, a1992) | ~c6_2(U_20, a2025) | ~ndr1_1(U_20) | ssSkP14(U_20)))). % 34.30/12.90 tff(c_4971, plain, (![U_28]: (c10_1(U_28) | c3_2(U_28, a1956) | c2_2(U_28, a1956) | ~c6_2(U_28, a2025) | ~ndr1_1(U_28) | ssSkP10(U_28)))). % 34.30/12.90 tff(c_5087, plain, (![U_23]: (c10_1(U_23) | c3_2(U_23, a2025) | c3_2(U_23, a1984) | c2_2(U_23, a1984) | ~ndr1_1(U_23) | ssSkP12(U_23)))). % 34.30/12.90 tff(c_6806, plain, (c3_2(a1967, a2025))). % 34.30/12.90 tff(c_5093, plain, (![U_28]: (c10_1(U_28) | c3_2(U_28, a2025) | c3_2(U_28, a1956) | c2_2(U_28, a1956) | ~ndr1_1(U_28) | ssSkP10(U_28)))). % 34.30/12.90 tff(c_5179, plain, (![U_23]: (c10_1(U_23) | c3_2(U_23, a1984) | c2_2(U_23, a1984) | ~c5_2(U_23, a2025) | ~ndr1_1(U_23) | ssSkP12(U_23)))). % 34.30/12.90 tff(c_5088, plain, (![U_18]: (c10_1(U_18) | c3_2(U_18, a2025) | c3_2(U_18, a2031) | c2_2(U_18, a2031) | ~ndr1_1(U_18) | ssSkP16(U_18)))). % 34.30/12.91 tff(c_5086, plain, (![U_36]: (c10_1(U_36) | c3_2(U_36, a2025) | c3_2(U_36, a1863) | c2_2(U_36, a1863) | ~ndr1_1(U_36) | ssSkP5(U_36)))). % 34.30/12.91 tff(c_4378, plain, (![U_40]: (c2_1(U_40) | c5_2(U_40, a1843) | c8_2(U_40, a1843) | ~c1_2(U_40, a1898) | ~ndr1_1(U_40) | ssSkP3(U_40)))). % 34.30/12.91 tff(c_4161, plain, (![U_46]: (c5_2(U_46, a1954) | c1_2(U_46, a1834) | ~ndr1_1(U_46) | ~c5_2(U_46, a1834) | ~ssSkP9(U_46) | ssSkP0(U_46)))). % 34.30/12.91 tff(c_4453, plain, (![U_46]: (c3_2(U_46, a1954) | c1_2(U_46, a1834) | ~ndr1_1(U_46) | ~c5_2(U_46, a1834) | ~ssSkP9(U_46) | ssSkP0(U_46)))). % 34.30/12.91 tff(c_6668, plain, (![U_23]: (c9_1(U_23) | c10_2(U_23, a1984) | ~c4_1(U_23) | ~ndr1_1(U_23) | ~c1_2(U_23, a1984) | ssSkP12(U_23)))). % 34.30/12.91 tff(c_6692, plain, (![U_29]: (c9_1(U_29) | c10_2(U_29, a1956) | ~c4_1(U_29) | ~ndr1_1(U_29) | ssSkP10(U_29)))). % 34.30/12.91 tff(c_6687, plain, (~c1_2(a1871, a1834))). % 34.30/12.91 tff(c_6686, plain, (~c1_2(a1839, a1840))). % 34.30/12.91 tff(c_6685, plain, (~c1_2(a1900, a1902))). % 34.30/12.91 tff(c_6669, plain, (![U_18]: (c9_1(U_18) | c10_2(U_18, a2031) | ~c4_1(U_18) | ~ndr1_1(U_18) | ~c1_2(U_18, a2031) | ssSkP16(U_18)))). % 34.30/12.91 tff(c_6683, plain, (~c4_1(a1998))). % 34.30/12.91 tff(c_6682, plain, (~c1_2(a1976, a1977))). % 34.30/12.91 tff(c_6510, plain, (![U_539, V_543]: (c9_1(U_539) | c10_2(U_539, V_543) | ~c4_1(U_539) | ~ndr1_1(U_539) | ~c8_2(U_539, V_543) | ~c1_2(U_539, V_543)))). % 34.30/12.91 tff(c_6571, plain, (~c4_2(a1875, a1947))). % 34.30/12.91 tff(c_6570, plain, (~c3_2(a2029, a1947))). % 34.30/12.91 tff(c_4305, plain, (![U_40]: (c2_1(U_40) | c5_2(U_40, a1843) | c8_2(U_40, a1843) | ~c6_2(U_40, a1898) | ~ndr1_1(U_40) | ssSkP3(U_40)))). % 34.30/12.91 tff(c_6511, plain, (~c3_2(a1939, a1947))). % 34.30/12.91 tff(c_6507, plain, (~c2_2(a1988, a1835))). % 34.30/12.91 tff(c_6506, plain, (~c2_2(a1988, a1989))). % 34.30/12.91 tff(c_6467, plain, (![Y_547]: (~c1_2(a1988, Y_547) | ~c2_2(a1988, Y_547) | ~c5_2(a1988, Y_547)))). % 34.30/12.91 tff(c_6464, plain, (ssSkP8(a1924))). % 34.30/12.91 tff(c_6463, plain, (ssSkP8(a1851))). % 34.30/12.91 tff(c_4242, plain, (![U_32]: (c2_1(U_32) | c2_2(U_32, a1898) | c5_2(U_32, a1947) | c8_2(U_32, a1947) | ~ndr1_1(U_32) | ssSkP8(U_32)))). % 34.30/12.91 tff(c_6396, plain, (~c6_2(a1875, a1898))). % 34.30/12.91 tff(c_6392, plain, (~c10_2(a2029, a1898))). % 34.30/12.91 tff(c_6395, plain, (~ssSkC30)). % 34.30/12.91 tff(c_6385, plain, (~c6_2(a2029, a1898))). % 34.30/12.91 tff(c_6382, plain, (~c3_2(a1896, a1897))). % 34.30/12.91 tff(c_6381, plain, (~c2_2(a1896, a1897))). % 34.30/12.91 tff(c_6378, plain, (~c7_1(a1896))). % 34.30/12.91 tff(c_6365, plain, (c6_2(a1896, a1897))). % 34.30/12.91 tff(c_6351, plain, (~ssSkP9(a1896))). % 34.30/12.91 tff(c_6350, plain, (~c10_2(a1939, a1898))). % 34.30/12.91 tff(c_6331, plain, (c7_2(a1896, a1897))). % 34.30/12.91 tff(c_6322, plain, (~c6_2(a1939, a1898))). % 34.30/12.91 tff(c_6321, plain, (ndr1_1(a1896))). % 34.30/12.91 tff(c_6318, plain, (~c10_2(a1924, a1898))). % 34.30/12.91 tff(c_6310, plain, (~c6_2(a1924, a1898))). % 34.30/12.91 tff(c_6309, plain, (~c9_1(a1896))). % 34.30/12.91 tff(c_6306, plain, (~c10_2(a1851, a1898))). % 34.30/12.91 tff(c_6305, plain, (c5_2(a1988, a1989))). % 34.30/12.91 tff(c_6295, plain, (~c6_2(a1851, a1898))). % 34.30/12.91 tff(c_4310, plain, (![U_32]: (c2_1(U_32) | c5_2(U_32, a1947) | c8_2(U_32, a1947) | ~c6_2(U_32, a1898) | ~ndr1_1(U_32) | ssSkP8(U_32)))). % 34.30/12.91 tff(c_4451, plain, (![U_34]: (c3_2(U_34, a1954) | c1_2(U_34, a1947) | ~ndr1_1(U_34) | ~c5_2(U_34, a1947) | ~ssSkP9(U_34) | ssSkP8(U_34)))). % 34.30/12.91 tff(c_6223, plain, (~c3_2(a1988, a1989))). % 34.30/12.91 tff(c_6220, plain, (~c10_2(a1988, a1989))). % 34.30/12.91 tff(c_6212, plain, (~c6_2(a1988, a1989))). % 34.30/12.91 tff(c_4162, plain, (![U_41]: (c5_2(U_41, a1954) | c1_2(U_41, a1843) | ~ndr1_1(U_41) | ~c5_2(U_41, a1843) | ~ssSkP9(U_41) | ssSkP3(U_41)))). % 34.30/12.91 tff(c_4561, plain, (![U_42]: (c10_2(U_42, a1954) | c1_2(U_42, a1837) | ~ndr1_1(U_42) | ~c5_2(U_42, a1837) | ~ssSkP9(U_42) | ssSkP2(U_42)))). % 34.30/12.91 tff(c_4159, plain, (![U_34]: (c5_2(U_34, a1954) | c1_2(U_34, a1947) | ~ndr1_1(U_34) | ~c5_2(U_34, a1947) | ~ssSkP9(U_34) | ssSkP8(U_34)))). % 34.30/12.91 tff(c_6182, plain, (~c4_2(a1875, a1843))). % 34.30/12.91 tff(c_6179, plain, (ssSkP3(a1924))). % 34.30/12.91 tff(c_6176, plain, (ssSkP3(a1851))). % 34.30/12.91 tff(c_4237, plain, (![U_40]: (c2_1(U_40) | c2_2(U_40, a1898) | c5_2(U_40, a1843) | c8_2(U_40, a1843) | ~ndr1_1(U_40) | ssSkP3(U_40)))). % 34.30/12.91 tff(c_4160, plain, (![U_42]: (c5_2(U_42, a1954) | c1_2(U_42, a1837) | ~ndr1_1(U_42) | ~c5_2(U_42, a1837) | ~ssSkP9(U_42) | ssSkP2(U_42)))). % 34.30/12.91 tff(c_6116, plain, (c3_1(a1988))). % 34.30/12.91 tff(c_6112, plain, (~c5_1(a1988))). % 34.30/12.91 tff(c_4563, plain, (![U_41]: (c10_2(U_41, a1954) | c1_2(U_41, a1843) | ~ndr1_1(U_41) | ~c5_2(U_41, a1843) | ~ssSkP9(U_41) | ssSkP3(U_41)))). % 34.30/12.91 tff(c_4562, plain, (![U_46]: (c10_2(U_46, a1954) | c1_2(U_46, a1834) | ~ndr1_1(U_46) | ~c5_2(U_46, a1834) | ~ssSkP9(U_46) | ssSkP0(U_46)))). % 34.30/12.91 tff(c_6083, plain, (ndr1_1(a1988))). % 34.30/12.91 tff(c_5873, plain, (![U_726]: (ssSkP10(U_726) | c5_1(U_726) | ~c7_1(U_726) | ~ndr1_1(U_726) | ~c4_2(U_726, a1956) | ~c10_2(U_726, a1956)))). % 34.30/12.91 tff(c_5967, plain, (![U_39]: (c2_1(U_39) | c5_1(U_39) | ~ndr1_1(U_39) | ~c1_2(U_39, a1855) | ~c3_2(U_39, a1855) | ssSkP4(U_39)))). % 34.30/12.91 tff(c_6068, plain, (~c10_2(a2017, a1888))). % 34.30/12.91 tff(c_5871, plain, (![U_726]: (ssSkP6(U_726) | c5_1(U_726) | ~c7_1(U_726) | ~ndr1_1(U_726) | ~c4_2(U_726, a1888) | ~c10_2(U_726, a1888)))). % 34.30/12.91 tff(c_6044, plain, (~c7_1(a1967))). % 34.30/12.91 tff(c_6041, plain, (~c7_1(a1976))). % 34.30/12.91 tff(c_6037, plain, (~c7_1(a2006))). % 34.30/12.91 tff(c_6008, plain, (![U_31]: (c5_1(U_31) | ~c7_1(U_31) | ~ndr1_1(U_31) | ssSkP9(U_31)))). % 34.30/12.91 tff(c_5986, plain, (~c10_2(a1933, a2025))). % 34.30/12.91 tff(c_5983, plain, (~c10_2(a1900, a1898))). % 34.30/12.92 tff(c_5982, plain, (~c10_2(a1919, a1898))). % 34.30/12.92 tff(c_5981, plain, (~c10_2(a1976, a2025))). % 34.30/12.92 tff(c_5978, plain, (c5_1(a1892))). % 34.30/12.92 tff(c_5933, plain, (~c1_2(a1952, a1949))). % 34.30/12.92 tff(c_5930, plain, (![U_446, V_447]: (c2_1(U_446) | c5_1(U_446) | ~ndr1_1(U_446) | ~c6_2(U_446, V_447) | ~c1_2(U_446, V_447) | ~c3_2(U_446, V_447)))). % 34.30/12.92 tff(c_5932, plain, (~c10_2(a1976, a1977))). % 34.30/12.92 tff(c_5931, plain, (~c1_2(a1952, a1834))). % 34.30/12.92 tff(c_5927, plain, (~c1_2(a1952, a1843))). % 34.30/12.92 tff(c_5924, plain, (ssSkP11(a1952))). % 34.30/12.92 tff(c_5920, plain, (~c1_2(a1952, a1980))). % 34.30/12.92 tff(c_5919, plain, (~c1_2(a1952, a1837))). % 34.30/12.92 tff(c_5916, plain, (~c1_2(a1952, a1947))). % 34.30/12.92 tff(c_5879, plain, (![W_445]: (c3_2(a1952, W_445) | ~c7_2(a1952, W_445) | ~c1_2(a1952, W_445)))). % 34.30/12.92 tff(c_5878, plain, (~c10_2(a1998, a2025))). % 34.30/12.92 tff(c_5877, plain, (~c10_2(a2006, a1898))). % 34.30/12.92 tff(c_5794, plain, (![U_440, V_441]: (c5_1(U_440) | c6_2(U_440, V_441) | ~c7_1(U_440) | ~ndr1_1(U_440) | ~c4_2(U_440, V_441) | ~c10_2(U_440, V_441)))). % 34.30/12.92 tff(c_5791, plain, (ndr1_1(a1952))). % 34.30/12.92 tff(c_5750, plain, (~c1_2(a1875, a1898))). % 34.30/12.92 tff(c_5742, plain, (~ssSkP9(a1967))). % 34.30/12.92 tff(c_5738, plain, (~c2_1(a1967))). % 34.30/12.92 tff(c_5737, plain, (c3_2(a1967, a2031))). % 34.30/12.92 tff(c_5736, plain, (c3_2(a1967, a1990))). % 34.30/12.92 tff(c_5733, plain, (c3_2(a1967, a1888))). % 34.30/12.92 tff(c_5685, plain, (![W_420]: (c5_2(a1967, W_420) | c3_2(a1967, W_420)))). % 34.30/12.92 tff(c_5684, plain, (ndr1_1(a1967))). % 34.30/12.92 tff(c_5631, plain, (~ssSkC23)). % 34.30/12.92 tff(c_5628, plain, (~c3_1(a1979))). % 34.30/12.92 tff(c_5627, plain, (~c3_1(a1869))). % 34.30/12.92 tff(c_5617, plain, (![U_427]: (~c9_1(U_427) | ~c10_1(U_427) | ~c3_1(U_427)))). % 34.30/12.92 tff(c_5612, plain, (~c1_1(a1903))). % 34.30/12.92 tff(c_5604, plain, (~c8_1(a1903))). % 34.30/12.92 tff(c_5603, plain, (~c1_1(a1875))). % 34.30/12.92 tff(c_5543, plain, (~c8_1(a1875))). % 34.30/12.92 tff(c_5546, plain, (![U_390, W_392, V_391]: (c2_2(U_390, W_392) | c8_2(U_390, W_392) | c10_2(U_390, V_391) | ~c9_1(U_390) | ~c9_2(U_390, W_392) | ~ndr1_1(U_390) | ~c1_2(U_390, V_391)))). % 34.30/12.92 tff(c_5538, plain, (~c1_1(a1851))). % 34.30/12.92 tff(c_5533, plain, (~c8_1(a1851))). % 34.30/12.92 tff(c_5524, plain, (~c8_1(a1917))). % 34.30/12.92 tff(c_5523, plain, (c4_2(a1858, a1859))). % 34.30/12.92 tff(c_5520, plain, (ssSkP2(a1979))). % 34.52/12.92 tff(c_5516, plain, (c3_2(a1979, a1837))). % 34.52/12.92 tff(c_5512, plain, (c3_2(a1845, a1980))). % 34.52/12.92 tff(c_5515, plain, (c5_2(a1917, a1918))). % 34.52/12.92 tff(c_5511, plain, (~c10_2(a1960, a1961))). % 34.52/12.92 tff(c_5507, plain, (ssSkP0(a1845))). % 34.52/12.92 tff(c_5503, plain, (c3_2(a1845, a1834))). % 34.52/12.92 tff(c_5502, plain, (c3_2(a1979, a1947))). % 34.52/12.92 tff(c_5501, plain, (~c9_2(a1869, a1870))). % 34.52/12.92 tff(c_5498, plain, (ssSkP0(a1979))). % 34.52/12.92 tff(c_5491, plain, (c3_2(a1979, a1834))). % 34.52/12.92 tff(c_5494, plain, (~c2_2(a1869, a1870))). % 34.52/12.92 tff(c_5490, plain, (~c1_1(a1917))). % 34.52/12.92 tff(c_5483, plain, (c2_2(a1917, a1918))). % 34.52/12.92 tff(c_5480, plain, (ssSkP3(a1979))). % 34.52/12.92 tff(c_5476, plain, (c3_2(a1979, a1843))). % 34.52/12.92 tff(c_5475, plain, (~c6_2(a1858, a1859))). % 34.52/12.92 tff(c_5472, plain, (c3_2(a1979, a1980))). % 34.52/12.92 tff(c_5471, plain, (ssSkP2(a1845))). % 34.52/12.92 tff(c_5452, plain, (c3_2(a1845, a1837))). % 34.52/12.92 tff(c_5455, plain, (~c4_2(a1917, a1918))). % 34.52/12.92 tff(c_5447, plain, (c3_2(a1845, a1947))). % 34.52/12.92 tff(c_5451, plain, (~c3_2(a1960, a1961))). % 34.52/12.92 tff(c_5446, plain, (ssSkP3(a1845))). % 34.52/12.92 tff(c_5442, plain, (c3_2(a1845, a1843))). % 34.52/12.92 tff(c_5439, plain, (~c1_1(a2029))). % 34.52/12.92 tff(c_5434, plain, (~c10_2(a1869, a1870))). % 34.52/12.92 tff(c_5431, plain, (~c8_1(a2029))). % 34.52/12.92 tff(c_5430, plain, (~c1_1(a1910))). % 34.52/12.92 tff(c_5425, plain, (~c10_2(a1858, a1859))). % 34.52/12.92 tff(c_5422, plain, (~c8_1(a1910))). % 34.52/12.92 tff(c_5417, plain, (~c8_1(a1900))). % 34.52/12.92 tff(c_5221, plain, (![U_292, V_293]: (c10_2(U_292, a1909) | c10_2(U_292, V_293) | c3_2(U_292, V_293) | c4_2(U_292, V_293) | ~c8_1(U_292) | ~ndr1_1(U_292)))). % 34.52/12.92 tff(c_5212, plain, (c2_2(a1871, a1834))). % 34.52/12.92 tff(c_5201, plain, (c2_2(a1976, a1977))). % 34.52/12.92 tff(c_5204, plain, (ndr1_1(a1858))). % 34.52/12.92 tff(c_5109, plain, (c2_2(a1933, a1934))). % 34.52/12.92 tff(c_5111, plain, (![U_333, V_334]: (c10_1(U_333) | c3_2(U_333, V_334) | c2_2(U_333, V_334) | ~c5_2(U_333, a2025) | ~ndr1_1(U_333) | ~c8_2(U_333, V_334)))). % 34.52/12.92 tff(c_5108, plain, (~c1_1(a1998))). % 34.52/12.92 tff(c_5101, plain, (c2_2(a1998, a2000))). % 34.52/12.92 tff(c_5019, plain, (![U_310, V_311]: (c10_1(U_310) | c3_2(U_310, a2025) | c3_2(U_310, V_311) | c2_2(U_310, V_311) | ~ndr1_1(U_310) | ~c8_2(U_310, V_311)))). % 34.52/12.92 tff(c_5015, plain, (~c1_2(a2029, a1898))). % 34.52/12.92 tff(c_5014, plain, (ndr1_1(a1869))). % 34.52/12.92 tff(c_5011, plain, (~c2_2(a1875, a1909))). % 34.52/12.93 tff(c_5010, plain, (ndr1_1(a1917))). % 34.52/12.93 tff(c_5007, plain, (~c2_2(a1903, a1909))). % 34.52/12.93 tff(c_5006, plain, (~c1_2(a1939, a1898))). % 34.52/12.93 tff(c_5005, plain, (~c10_1(a1960))). % 34.52/12.93 tff(c_5001, plain, (c7_1(a1917))). % 34.52/12.93 tff(c_4998, plain, (c9_1(a1869))). % 34.52/12.93 tff(c_4995, plain, (~c2_2(a1851, a1909))). % 34.52/12.93 tff(c_4990, plain, (~c6_2(a1871, a2025))). % 34.52/12.93 tff(c_4993, plain, (![U_327, V_328]: (c10_2(U_327, V_328) | c3_2(U_327, V_328) | c4_2(U_327, V_328) | ~c8_1(U_327) | ~c8_2(U_327, a1909) | ~ndr1_1(U_327)))). % 34.52/12.93 tff(c_4989, plain, (~c6_2(a1976, a2025))). % 34.52/12.93 tff(c_4988, plain, (~c6_2(a1933, a2025))). % 34.52/12.93 tff(c_4985, plain, (~c1_2(a1924, a1898))). % 34.52/12.93 tff(c_4982, plain, (~c1_2(a1851, a1898))). % 34.52/12.93 tff(c_4979, plain, (~c6_2(a1998, a2025))). % 34.52/12.93 tff(c_4897, plain, (![U_335, V_336]: (c10_1(U_335) | c3_2(U_335, V_336) | c2_2(U_335, V_336) | ~c6_2(U_335, a2025) | ~ndr1_1(U_335) | ~c8_2(U_335, V_336)))). % 34.52/12.93 tff(c_4895, plain, (~c2_2(a1845, a1909))). % 34.52/12.93 tff(c_4892, plain, (~c2_2(a1979, a1909))). % 34.52/12.93 tff(c_4889, plain, (~c2_2(a2029, a1909))). % 34.52/12.93 tff(c_4888, plain, (~c2_2(a1910, a1909))). % 34.52/12.93 tff(c_4887, plain, (~c2_2(a1900, a1909))). % 34.52/12.93 tff(c_4691, plain, (![U_325, V_326]: (c10_2(U_325, V_326) | c3_2(U_325, V_326) | c4_2(U_325, V_326) | ~c8_1(U_325) | ~c2_2(U_325, a1909) | ~ndr1_1(U_325)))). % 34.52/12.93 tff(c_4383, plain, (![U_32]: (c2_1(U_32) | c5_2(U_32, a1947) | c8_2(U_32, a1947) | ~c1_2(U_32, a1898) | ~ndr1_1(U_32) | ssSkP8(U_32)))). % 34.52/12.93 tff(c_4560, plain, (![U_34]: (c10_2(U_34, a1954) | c1_2(U_34, a1947) | ~ndr1_1(U_34) | ~c5_2(U_34, a1947) | ~ssSkP9(U_34) | ssSkP8(U_34)))). % 34.52/12.93 tff(c_4636, plain, (c8_1(a1858))). % 34.52/12.93 tff(c_4452, plain, (![U_42]: (c3_2(U_42, a1954) | c1_2(U_42, a1837) | ~ndr1_1(U_42) | ~c5_2(U_42, a1837) | ~ssSkP9(U_42) | ssSkP2(U_42)))). % 34.52/12.93 tff(c_4454, plain, (![U_41]: (c3_2(U_41, a1954) | c1_2(U_41, a1843) | ~ndr1_1(U_41) | ~c5_2(U_41, a1843) | ~ssSkP9(U_41) | ssSkP3(U_41)))). % 34.52/12.93 tff(c_4621, plain, (~c6_2(a2006, a1898))). % 34.52/12.93 tff(c_4620, plain, (~c10_1(a1858))). % 34.52/12.93 tff(c_4617, plain, (~c1_2(a1871, a1898))). % 34.52/12.93 tff(c_4616, plain, (c4_1(a1869))). % 34.52/12.93 tff(c_4613, plain, (~c6_2(a1871, a1898))). % 34.52/12.93 tff(c_4606, plain, (c2_2(a2006, a1898))). % 34.52/12.93 tff(c_4605, plain, (ndr1_1(a1960))). % 34.52/12.93 tff(c_4601, plain, (~c1_2(a2006, a1898))). % 34.52/12.93 tff(c_4592, plain, (c2_2(a1871, a1898))). % 34.52/12.93 tff(c_4080, plain, (![U_684]: (~c2_1(U_684) | c4_2(U_684, a1983) | c3_2(U_684, a1983) | ~c5_1(U_684) | ~c7_1(U_684) | ~ndr1_1(U_684)))). % 34.52/12.93 tff(c_4582, plain, (~c7_1(a1903))). % 34.52/12.93 tff(c_4590, plain, (c3_1(a1960))). % 34.52/12.93 tff(c_4586, plain, (~c5_1(a1960))). % 34.52/12.93 tff(c_4082, plain, (![U_684]: (ssSkP6(U_684) | c4_2(U_684, a1888) | c3_2(U_684, a1888) | ~c5_1(U_684) | ~c7_1(U_684) | ~ndr1_1(U_684)))). % 34.52/12.93 tff(c_4084, plain, (![U_684]: (ssSkP13(U_684) | c4_2(U_684, a1990) | c3_2(U_684, a1990) | ~c5_1(U_684) | ~c7_1(U_684) | ~ndr1_1(U_684)))). % 34.52/12.93 tff(c_4508, plain, (![U_288, V_289]: (c10_2(U_288, a1954) | c1_2(U_288, V_289) | ~ndr1_1(U_288) | ~c7_2(U_288, V_289) | ~c5_2(U_288, V_289) | ~ssSkP9(U_288)))). % 34.52/12.93 tff(c_4505, plain, (~c7_1(a1875))). % 34.52/12.93 tff(c_4083, plain, (![U_684]: (ssSkP16(U_684) | c4_2(U_684, a2031) | c3_2(U_684, a2031) | ~c5_1(U_684) | ~c7_1(U_684) | ~ndr1_1(U_684)))). % 34.52/12.93 tff(c_3856, plain, (![U_145]: (c7_1(U_145) | ~ndr1_1(U_145) | ~c3_2(U_145, a1957) | ~c8_1(U_145) | ~ssSkP10(U_145)))). % 34.52/12.93 tff(c_4493, plain, (c8_2(a1919, a1920))). % 34.52/12.93 tff(c_4489, plain, (c8_2(a1900, a1902))). % 34.52/12.93 tff(c_3857, plain, (![U_137]: (c7_1(U_137) | ~ndr1_1(U_137) | ~c3_2(U_137, a2018) | c10_1(U_137) | c8_1(U_137)))). % 34.52/12.93 tff(c_4487, plain, (~c6_2(a1900, a1898))). % 34.52/12.93 tff(c_4479, plain, (~ssSkP9(a1976))). % 34.52/12.93 tff(c_4471, plain, (~ssSkP9(a1971))). % 34.52/12.93 tff(c_4465, plain, (~ssSkP9(a2006))). % 34.52/12.93 tff(c_4399, plain, (![U_286, V_287]: (c3_2(U_286, a1954) | c1_2(U_286, V_287) | ~ndr1_1(U_286) | ~c7_2(U_286, V_287) | ~c5_2(U_286, V_287) | ~ssSkP9(U_286)))). % 34.52/12.93 tff(c_4396, plain, (~c1_2(a1919, a1898))). % 34.52/12.93 tff(c_4393, plain, (~c6_2(a1919, a1898))). % 34.52/12.93 tff(c_4390, plain, (c8_2(a1998, a2000))). % 34.52/12.93 tff(c_4325, plain, (![U_306, V_307]: (c2_1(U_306) | c5_2(U_306, V_307) | c8_2(U_306, V_307) | ~c1_2(U_306, a1898) | ~ndr1_1(U_306) | ~c9_2(U_306, V_307)))). % 34.52/12.93 tff(c_4317, plain, (~ssSkP9(a1915))). % 34.52/12.93 tff(c_4252, plain, (![U_308, V_309]: (c2_1(U_308) | c5_2(U_308, V_309) | c8_2(U_308, V_309) | ~c6_2(U_308, a1898) | ~ndr1_1(U_308) | ~c9_2(U_308, V_309)))). % 34.52/12.93 tff(c_4249, plain, (~c7_1(a1971))). % 34.52/12.93 tff(c_4181, plain, (~c7_1(a1871))). % 34.52/12.93 tff(c_4184, plain, (![U_279, V_280]: (c2_1(U_279) | c2_2(U_279, a1898) | c5_2(U_279, V_280) | c8_2(U_279, V_280) | ~ndr1_1(U_279) | ~c9_2(U_279, V_280)))). % 34.52/12.93 tff(c_4178, plain, (ssSkC41)). % 34.52/12.93 tff(c_4107, plain, (![U_290, V_291]: (c5_2(U_290, a1954) | c1_2(U_290, V_291) | ~ndr1_1(U_290) | ~c7_2(U_290, V_291) | ~c5_2(U_290, V_291) | ~ssSkP9(U_290)))). % 34.52/12.93 tff(c_4018, plain, (![U_86]: (c7_1(U_86) | c8_1(U_86) | ~c1_1(U_86)))). % 34.52/12.93 tff(c_4092, plain, (~c1_1(a1884))). % 34.52/12.93 tff(c_4091, plain, (~c1_1(a1933))). % 34.52/12.93 tff(c_4050, plain, (~c1_1(a1943))). % 34.52/12.93 tff(c_4052, plain, (![U_300, V_301]: (c4_2(U_300, V_301) | c3_2(U_300, V_301) | c5_2(U_300, V_301) | ~c5_1(U_300) | ~c7_1(U_300) | ~ndr1_1(U_300)))). % 34.52/12.93 tff(c_4046, plain, (c8_1(a1979))). % 34.52/12.93 tff(c_4049, plain, (~c10_1(a1952))). % 34.52/12.93 tff(c_4045, plain, (c8_1(a1845))). % 34.52/12.93 tff(c_3860, plain, (![U_39]: (c7_1(U_39) | ~ndr1_1(U_39) | ~c3_2(U_39, a1855) | ssSkP4(U_39)))). % 34.52/12.93 tff(c_3873, plain, (~c3_2(a1998, a2000))). % 34.52/12.93 tff(c_3866, plain, (c7_1(a1892))). % 34.52/12.93 tff(c_3830, plain, (![U_281, V_282]: (c7_1(U_281) | ~ndr1_1(U_281) | ~c3_2(U_281, V_282) | ~c6_2(U_281, V_282)))). % 34.52/12.93 tff(c_3809, plain, (ssSkC38)). % 34.52/12.93 tff(c_3792, plain, (~c4_2(a1903, a1957))). % 34.52/12.93 tff(c_3789, plain, (~c2_1(a1875))). % 34.52/12.93 tff(c_3788, plain, (~c10_1(a1903))). % 34.52/12.93 tff(c_3782, plain, (~ssSkP5(a1875))). % 34.52/12.93 tff(c_3781, plain, (~c10_1(a1924))). % 34.52/12.93 tff(c_3773, plain, (~ssSkP5(a1979))). % 34.52/12.94 tff(c_3770, plain, (c3_1(a1851))). % 34.52/12.94 tff(c_3766, plain, (~c5_1(a1851))). % 34.52/12.94 tff(c_3765, plain, (ssSkP16(a1851))). % 34.52/12.94 tff(c_3762, plain, (ssSkP14(a1851))). % 34.52/12.94 tff(c_3761, plain, (ssSkP10(a1851))). % 34.52/12.94 tff(c_3758, plain, (ssSkP12(a1851))). % 34.52/12.94 tff(c_3757, plain, (c4_2(a1851, a1863))). % 34.52/12.94 tff(c_3710, plain, (~c2_1(a2029))). % 34.52/12.94 tff(c_3713, plain, (![U_245]: (c5_2(a1851, U_245) | c4_2(a1851, U_245) | ~c8_2(a1851, U_245)))). % 34.52/12.94 tff(c_3709, plain, (~c1_1(a2014))). % 34.52/12.94 tff(c_3703, plain, (~c3_2(a2014, a1962))). % 34.52/12.94 tff(c_3697, plain, (~ssSkP5(a1845))). % 34.52/12.94 tff(c_3695, plain, (~c8_2(a1924, a1949))). % 34.52/12.94 tff(c_3689, plain, (~ssSkP5(a1924))). % 34.52/12.94 tff(c_3682, plain, (~ssSkP5(a2029))). % 34.52/12.94 tff(c_3681, plain, (~c1_1(a1871))). % 34.52/12.94 tff(c_3678, plain, (~c4_2(a2029, a1949))). % 34.52/12.94 tff(c_3676, plain, (~c4_2(a1875, a1956))). % 34.52/12.94 tff(c_3677, plain, (ssSkC40)). % 34.52/12.94 tff(c_3675, plain, (~c4_2(a1875, a1992))). % 34.52/12.94 tff(c_3674, plain, (~c4_2(a1875, a2031))). % 34.52/12.94 tff(c_3671, plain, (~c4_2(a1875, a1863))). % 34.52/12.94 tff(c_3670, plain, (ssSkC26)). % 34.52/12.94 tff(c_3669, plain, (~c3_2(a2014, a1929))). % 34.52/12.94 tff(c_3668, plain, (ssSkP12(a1924))). % 34.52/12.94 tff(c_3664, plain, (~c8_2(a1924, a1984))). % 34.52/12.94 tff(c_3661, plain, (~c4_2(a2029, a1994))). % 34.52/12.94 tff(c_3636, plain, (~c4_2(a2029, a1947))). % 34.52/12.94 tff(c_3601, plain, (![U_234]: (c9_2(a2014, U_234) | ~c4_2(a2014, U_234) | ~c3_2(a2014, U_234)))). % 34.52/12.94 tff(c_3635, plain, (~c4_2(a2029, a1984))). % 34.52/12.94 tff(c_3634, plain, (~c4_2(a2029, a1843))). % 34.52/12.94 tff(c_3605, plain, (![U_238]: (~c7_2(a2029, U_238) | ~c4_2(a2029, U_238) | ~c9_2(a2029, U_238)))). % 34.52/12.94 tff(c_3602, plain, (ndr1_1(a2014))). % 34.52/12.94 tff(c_3556, plain, (~c8_2(a1924, a1843))). % 34.52/12.94 tff(c_3514, plain, (~c8_2(a1924, a1947))). % 34.52/12.94 tff(c_3479, plain, (![U_256]: (~c8_2(a1875, U_256) | ~c10_2(a1875, U_256) | ~c4_2(a1875, U_256)))). % 34.52/12.94 tff(c_3513, plain, (ssSkP11(a1845))). % 34.52/12.94 tff(c_3509, plain, (~c4_2(a1845, a1980))). % 34.52/12.94 tff(c_3508, plain, (~c4_2(a1845, a1947))). % 34.52/12.94 tff(c_3507, plain, (~c4_2(a1845, a1834))). % 34.52/12.94 tff(c_3227, plain, (![U_235]: (c1_2(a1924, U_235) | ~c9_2(a1924, U_235) | ~c8_2(a1924, U_235)))). % 34.52/12.94 tff(c_3440, plain, (~c4_2(a1845, a1843))). % 34.52/12.94 tff(c_3480, plain, (ndr1_1(a1875))). % 34.52/12.94 tff(c_3439, plain, (~c4_2(a1845, a1837))). % 34.52/12.94 tff(c_3438, plain, (ndr1_1(a1950))). % 34.52/12.94 tff(c_3395, plain, (~c7_2(a1924, a1956))). % 34.52/12.94 tff(c_3357, plain, (~c7_2(a1924, a1992))). % 34.52/12.94 tff(c_3152, plain, (![U_237]: (c5_2(a1845, U_237) | ~c7_2(a1845, U_237) | ~c4_2(a1845, U_237)))). % 34.52/12.94 tff(c_3356, plain, (~c7_2(a1924, a2031))). % 34.52/12.94 tff(c_3355, plain, (~c7_2(a1924, a1863))). % 34.52/12.94 tff(c_3313, plain, (![U_255]: (~c8_2(a1924, U_255) | ~c10_2(a1924, U_255) | ~c7_2(a1924, U_255)))). % 34.52/12.94 tff(c_3310, plain, (ndr1_1(a2019))). % 34.52/12.94 tff(c_3073, plain, (~c1_1(a1913))). % 34.52/12.94 tff(c_3228, plain, (ndr1_1(a1924))). % 34.52/12.94 tff(c_3153, plain, (ndr1_1(a1845))). % 34.52/12.94 tff(c_3067, plain, (~ssSkP10(a2017))). % 34.52/12.94 tff(c_3066, plain, (ssSkP12(a1903))). % 34.52/12.94 tff(c_3062, plain, (~c8_2(a1903, a1984))). % 34.52/12.94 tff(c_3061, plain, (c4_2(a2017, a1904))). % 34.52/12.94 tff(c_3034, plain, (![U_236]: (c7_2(a1903, U_236) | ~c8_2(a1903, U_236) | ~c9_2(a1903, U_236)))). % 34.52/12.94 tff(c_3031, plain, (c4_2(a2017, a1888))). % 34.52/12.94 tff(c_3012, plain, (~c4_2(a1979, a1843))). % 34.52/12.94 tff(c_3009, plain, (![U_184]: (c2_2(a2017, U_184) | c7_2(a2017, U_184) | c4_2(a2017, U_184)))). % 34.52/12.94 tff(c_3011, plain, (~c4_2(a1979, a1834))). % 34.52/12.94 tff(c_3010, plain, (ndr1_1(a2017))). % 34.52/12.94 tff(c_2973, plain, (~c4_2(a1979, a1837))). % 34.52/12.94 tff(c_2909, plain, (~c4_2(a1903, a1888))). % 34.52/12.94 tff(c_2948, plain, (![U_204]: (c3_2(a1913, U_204) | c7_2(a1913, U_204) | c9_2(a1913, U_204)))). % 34.52/12.94 tff(c_2949, plain, (ndr1_1(a1913))). % 34.52/12.94 tff(c_2908, plain, (~c4_2(a1903, a1904))). % 34.52/12.94 tff(c_2907, plain, (~c3_2(a2029, a1956))). % 34.52/12.94 tff(c_2906, plain, (~c3_2(a2029, a1992))). % 34.52/12.94 tff(c_2889, plain, (~c3_2(a2029, a2031))). % 34.52/12.94 tff(c_2887, plain, (![U_219]: (c5_2(a1903, U_219) | c7_2(a1903, U_219) | ~c4_2(a1903, U_219)))). % 34.52/12.94 tff(c_2843, plain, (~c3_2(a2029, a1984))). % 34.52/12.94 tff(c_2888, plain, (ndr1_1(a1903))). % 34.52/12.94 tff(c_2842, plain, (ssSkP11(a1979))). % 34.52/12.94 tff(c_2797, plain, (~c4_2(a1979, a1980))). % 34.52/12.94 tff(c_2795, plain, (![U_222]: (c4_2(a2029, U_222) | ~c8_2(a2029, U_222) | ~c3_2(a2029, U_222)))). % 34.52/12.94 tff(c_2796, plain, (ndr1_1(a2029))). % 34.52/12.94 tff(c_2716, plain, (c8_2(a1871, a1834))). % 34.52/12.94 tff(c_2691, plain, (~c4_2(a1979, a1947))). % 34.52/12.94 tff(c_2694, plain, (![U_205]: (c9_2(a1871, U_205) | c3_2(a1871, U_205) | c8_2(a1871, U_205)))). % 34.52/12.94 tff(c_2652, plain, (![U_254]: (~c10_2(a1979, U_254) | ~c4_2(a1979, U_254) | ~c7_2(a1979, U_254)))). % 34.52/12.94 tff(c_2653, plain, (ndr1_1(a1979))). % 34.52/12.94 tff(c_2578, plain, (![U_33]: (c8_1(U_33) | ~c1_1(U_33) | ~ndr1_1(U_33) | ssSkP8(U_33)))). % 34.52/12.94 tff(c_2583, plain, (~c1_1(a1839))). % 34.52/12.94 tff(c_2582, plain, (~c1_1(a1900))). % 34.52/12.94 tff(c_2564, plain, (![U_261, V_262]: (c8_1(U_261) | ~c1_1(U_261) | ~c2_2(U_261, V_262) | ~ndr1_1(U_261)))). % 34.52/12.94 tff(c_2562, plain, (ssSkC9)). % 34.52/12.94 tff(c_2561, plain, (ndr1_1(a1884))). % 34.52/12.94 tff(c_2479, plain, (~ssSkP10(a1915))). % 34.52/12.94 tff(c_2472, plain, (![U_187]: (~c8_1(U_187) | ~c7_2(U_187, a1957) | ~ssSkP10(U_187)))). % 34.52/12.94 tff(c_2452, plain, (![U_180]: (c4_1(U_180) | c4_2(U_180, a2026) | ~c5_1(U_180)))). % 34.52/12.94 tff(c_2448, plain, (![U_145]: (c6_2(U_145, a1957) | ~c8_1(U_145) | ~ssSkP10(U_145)))). % 34.52/12.94 tff(c_2442, plain, (![U_182]: (c10_1(U_182) | c8_1(U_182) | ~c10_2(U_182, a2018)))). % 34.52/12.94 tff(c_2438, plain, (![U_206]: (c4_1(U_206) | ~c5_1(U_206) | ~c10_2(U_206, a2026)))). % 34.52/12.94 tff(c_2421, plain, (~c4_2(a1851, a1949))). % 34.52/12.94 tff(c_2412, plain, (~ssSkP5(a1851))). % 34.52/12.94 tff(c_2411, plain, (~c4_2(a1851, a1843))). % 34.52/12.94 tff(c_2408, plain, (~c4_2(a1851, a1834))). % 34.52/12.94 tff(c_2407, plain, (~c4_2(a1851, a1837))). % 34.52/12.94 tff(c_2404, plain, (ssSkP11(a1851))). % 34.52/12.95 tff(c_2400, plain, (~c4_2(a1851, a1980))). % 34.52/12.95 tff(c_2398, plain, (~c4_2(a1851, a1947))). % 34.52/12.95 tff(c_2361, plain, (![U_217]: (~c7_2(a1851, U_217) | ~c4_2(a1851, U_217)))). % 34.52/12.95 tff(c_2357, plain, (![U_188]: (~c8_1(U_188) | ~c8_2(U_188, a1957) | ~ssSkP10(U_188)))). % 34.52/12.95 tff(c_2325, plain, (![U_183]: (c10_1(U_183) | c8_1(U_183) | ~c4_2(U_183, a2018)))). % 34.52/12.95 tff(c_2321, plain, (![U_137]: (c10_1(U_137) | c8_1(U_137) | c6_2(U_137, a2018)))). % 34.52/12.95 tff(c_2314, plain, (![U_181]: (c4_1(U_181) | c3_2(U_181, a2026) | ~c5_1(U_181)))). % 34.52/12.95 tff(c_2300, plain, (c1_2(a1915, a1904))). % 34.52/12.95 tff(c_2297, plain, (c1_2(a1915, a1888))). % 34.52/12.95 tff(c_2285, plain, (![U_163]: (c7_2(a1915, U_163) | c1_2(a1915, U_163)))). % 34.52/12.95 tff(c_2271, plain, (![U_203]: (~c2_1(U_203) | ~c5_1(U_203) | ~c3_2(U_203, a1929)))). % 34.52/12.95 tff(c_2265, plain, (![U_87]: (c1_1(U_87) | c8_1(U_87) | c9_2(U_87, a1949)))). % 34.52/12.95 tff(c_2262, plain, (ssSkC2)). % 34.52/12.95 tff(c_2261, plain, (ndr1_1(a1848))). % 34.52/12.95 tff(c_2220, plain, (~ssSkC31)). % 34.52/12.95 tff(c_2213, plain, (![U_122]: (c8_1(U_122) | c3_2(U_122, a1962) | ~c1_1(U_122)))). % 34.52/12.95 tff(c_2207, plain, (![U_123]: (c8_1(U_123) | c6_2(U_123, a1962) | ~c1_1(U_123)))). % 34.52/12.95 tff(c_2196, plain, (![U_170]: (c8_1(U_170) | ~c1_1(U_170) | ~c9_2(U_170, a1962)))). % 34.52/12.95 tff(c_2183, plain, (~ssSkC43)). % 34.52/12.95 tff(c_2178, plain, (![U_102]: (c10_1(U_102) | c8_1(U_102) | ndr1_1(U_102)))). % 34.52/12.95 tff(c_2169, plain, (c3_1(a2006))). % 34.52/12.95 tff(c_2172, plain, (![U_200]: (~c5_1(U_200) | ~c2_1(U_200) | ~c5_2(U_200, a1983)))). % 34.52/12.95 tff(c_2165, plain, (~c5_1(a2006))). % 34.52/12.95 tff(c_2162, plain, (~c1_1(a2006))). % 34.52/12.95 tff(c_2145, plain, (![U_115]: (c7_2(a2006, U_115) | c9_2(a2006, U_115)))). % 34.52/12.95 tff(c_2130, plain, (![U_165]: (c4_1(U_165) | ~c10_1(U_165) | ~c10_2(U_165, a1994)))). % 34.52/12.95 tff(c_2122, plain, (![U_148]: (c2_1(U_148) | ~c1_1(U_148) | ~c9_2(U_148, a1927)))). % 34.52/12.95 tff(c_2119, plain, (~ssSkC37)). % 34.52/12.95 tff(c_2109, plain, (![U_88]: (c1_1(U_88) | c8_1(U_88) | c7_2(U_88, a1949)))). % 34.52/12.95 tff(c_2105, plain, (![U_89]: (c1_1(U_89) | c8_1(U_89) | c10_2(U_89, a1949)))). % 34.52/12.95 tff(c_2098, plain, (![U_136]: (c4_1(U_136) | ndr1_1(U_136) | ~c5_1(U_136)))). % 34.52/12.95 tff(c_2085, plain, (~ssSkP5(a1939))). % 34.52/12.95 tff(c_2084, plain, (~c3_2(a1939, a1992))). % 34.52/12.95 tff(c_2081, plain, (~c3_2(a1939, a1956))). % 34.52/12.95 tff(c_2076, plain, (~c3_2(a1939, a2031))). % 34.52/12.95 tff(c_2079, plain, (![U_119]: (c4_1(U_119) | c9_2(U_119, a1994) | ~c10_1(U_119)))). % 34.52/12.95 tff(c_2075, plain, (~c3_2(a1939, a1984))). % 34.52/12.95 tff(c_2030, plain, (![U_195]: (~c3_2(a1939, U_195) | ~c8_2(a1939, U_195)))). % 34.52/12.95 tff(c_2031, plain, (ndr1_1(a1939))). % 34.52/12.95 tff(c_1994, plain, (~ssSkC5)). % 34.52/12.95 tff(c_1989, plain, (ssSkC6)). % 34.52/12.95 tff(c_1981, plain, (![U_202]: (~c2_1(U_202) | ~c5_1(U_202) | ~c9_2(U_202, a1929)))). % 34.52/12.95 tff(c_1976, plain, (ssSkC8)). % 34.52/12.95 tff(c_1973, plain, (~ssSkC42)). % 34.52/12.95 tff(c_1968, plain, (![U_132]: (c7_2(U_132, a1864) | ~c8_1(U_132) | ~ssSkP5(U_132)))). % 34.52/12.95 tff(c_1964, plain, (![U_168]: (c8_2(U_168, a1983) | ~c5_1(U_168) | ~c2_1(U_168)))). % 34.52/12.95 tff(c_1960, plain, (![U_169]: (c1_2(U_169, a1983) | ~c5_1(U_169) | ~c2_1(U_169)))). % 34.52/12.95 tff(c_1952, plain, (ssSkC16)). % 34.52/12.95 tff(c_1947, plain, (~ssSkC19)). % 34.52/12.95 tff(c_1942, plain, (![U_109]: (c2_1(U_109) | c1_2(U_109, a1927) | ~c1_1(U_109)))). % 34.52/12.95 tff(c_1936, plain, (![U_173]: (c8_2(U_173, a1929) | ~c2_1(U_173) | ~c5_1(U_173)))). % 34.52/12.95 tff(c_1930, plain, (![U_131]: (c8_2(U_131, a1864) | ~c8_1(U_131) | ~ssSkP5(U_131)))). % 34.52/12.95 tff(c_1926, plain, (![U_178]: (~c8_1(U_178) | ~c1_2(U_178, a1864) | ~ssSkP5(U_178)))). % 34.52/12.95 tff(c_1918, plain, (ssSkC34)). % 34.52/12.95 tff(c_1914, plain, (![U_86]: (c8_1(U_86) | ndr1_1(U_86) | ~c1_1(U_86)))). % 34.52/12.95 tff(c_1911, plain, (~c10_1(a1854))). % 34.52/12.95 tff(c_1902, plain, (![U_118]: (~c6_1(U_118) | ~c10_1(U_118)))). % 34.52/12.95 tff(c_1897, plain, (![U_12]: (~c8_1(U_12) | ndr1_1(U_12)))). % 34.52/12.95 tff(c_1886, plain, (![U_77]: (c2_1(U_77) | ndr1_1(U_77) | ~c1_1(U_77)))). % 34.52/12.95 tff(c_1882, plain, (![U_126]: (ndr1_1(U_126) | ~c2_1(U_126) | ~c5_1(U_126)))). % 34.52/12.95 tff(c_1879, plain, (~c9_1(a1935))). % 34.52/12.95 tff(c_1875, plain, (ssSkC14)). % 34.52/12.95 tff(c_1872, plain, (ssSkC21)). % 34.52/12.95 tff(c_1868, plain, (![U_70]: (c1_1(U_70) | c8_1(U_70) | ndr1_1(U_70)))). % 34.52/12.95 tff(c_1863, plain, (ssSkC33)). % 34.52/12.95 tff(c_1860, plain, (ssSkC10)). % 34.52/12.95 tff(c_1857, plain, (ssSkC15)). % 34.52/12.95 tff(c_1852, plain, (ssSkC27)). % 34.52/12.95 tff(c_1847, plain, (~ssSkC22)). % 34.52/12.95 tff(c_1843, plain, (![U_81]: (c4_1(U_81) | ndr1_1(U_81) | ~c10_1(U_81)))). % 34.52/12.95 tff(c_1838, plain, (c3_1(a1924))). % 34.52/12.95 tff(c_1837, plain, (c3_1(a1998))). % 34.52/12.95 tff(c_1829, plain, (![U_67]: (c3_1(U_67) | c5_1(U_67)))). % 34.52/12.95 tff(c_1827, plain, (~c10_2(a1900, a1901))). % 34.52/12.95 tff(c_1826, plain, (c3_2(a1851, a1852))). % 34.52/12.95 tff(c_1820, plain, (c5_2(a1915, a1916))). % 34.52/12.95 tff(c_626, plain, (![U_62]: (ssSkP5(U_62) | ~c1_2(U_62, a1863)))). % 34.52/12.95 tff(c_630, plain, (![U_64]: (ssSkP2(U_64) | ~c3_2(U_64, a1837)))). % 34.52/12.95 tff(c_1813, plain, (~c4_2(a1900, a1901))). % 34.52/12.95 tff(c_412, plain, (![U_36]: (ssSkP5(U_36) | c8_2(U_36, a1863)))). % 34.52/12.95 tff(c_1803, plain, (~c10_2(a1900, a1902))). % 34.52/12.95 tff(c_628, plain, (![U_63]: (ssSkP3(U_63) | ~c3_2(U_63, a1843)))). % 34.52/12.95 tff(c_624, plain, (![U_61]: (ssSkP5(U_61) | ~c3_2(U_61, a1863)))). % 34.52/12.95 tff(c_1784, plain, (~c2_2(a1851, a1852))). % 34.52/12.95 tff(c_368, plain, (![U_34]: (ssSkP8(U_34) | c7_2(U_34, a1947)))). % 34.52/12.95 tff(c_338, plain, (![U_27]: (ssSkP11(U_27) | c4_2(U_27, a1980)))). % 34.52/12.95 tff(c_440, plain, (![U_44]: (ssSkP1(U_44) | c3_2(U_44, a1835)))). % 34.52/12.95 tff(c_330, plain, (![U_23]: (ssSkP12(U_23) | c8_2(U_23, a1984)))). % 34.52/12.95 tff(c_424, plain, (![U_40]: (ssSkP3(U_40) | c9_2(U_40, a1843)))). % 34.52/12.95 tff(c_634, plain, (![U_66]: (ssSkP0(U_66) | ~c3_2(U_66, a1834)))). % 34.52/12.95 tff(c_1768, plain, (~c2_2(a1900, a1901))). % 34.52/12.95 tff(c_1767, plain, (~c4_2(a1851, a1852))). % 34.52/12.95 tff(c_574, plain, (![U_49]: (ssSkP15(U_49) | ~c2_2(U_49, a2008)))). % 34.52/12.95 tff(c_1763, plain, (c2_2(a1900, a1902))). % 34.52/12.95 tff(c_436, plain, (![U_42]: (ssSkP2(U_42) | c7_2(U_42, a1837)))). % 34.52/12.95 tff(c_366, plain, (![U_33]: (ssSkP8(U_33) | c2_2(U_33, a1947)))). % 34.52/12.95 tff(c_306, plain, (![U_19]: (ssSkP15(U_19) | c3_2(U_19, a2008)))). % 34.52/12.95 tff(c_1759, plain, (c9_2(a1900, a1902))). % 34.52/12.95 tff(c_358, plain, (![U_30]: (ssSkP9(U_30) | c4_2(U_30, a1953)))). % 34.52/12.95 tff(c_612, plain, (![U_58]: (ssSkP6(U_58) | ~c6_2(U_58, a1888)))). % 34.52/12.95 tff(c_572, plain, (![U_48]: (ssSkP15(U_48) | ~c5_2(U_48, a2008)))). % 34.52/12.96 tff(c_438, plain, (![U_43]: (ssSkP2(U_43) | c6_2(U_43, a1837)))). % 34.52/12.96 tff(c_580, plain, (![U_50]: (ssSkP14(U_50) | ~c2_2(U_50, a1992)))). % 34.52/12.96 tff(c_444, plain, (![U_46]: (ssSkP0(U_46) | c7_2(U_46, a1834)))). % 34.52/12.96 tff(c_616, plain, (![U_60]: (ssSkP6(U_60) | ~c7_2(U_60, a1888)))). % 34.52/12.96 tff(c_294, plain, (![U_18]: (ssSkP16(U_18) | c8_2(U_18, a2031)))). % 34.52/12.96 tff(c_328, plain, (![U_22]: (ssSkP13(U_22) | c10_2(U_22, a1990)))). % 34.52/12.96 tff(c_1745, plain, (~c9_2(a1915, a1916))). % 34.52/12.96 tff(c_1742, plain, (c8_2(a1933, a1934))). % 34.52/12.96 tff(c_586, plain, (![U_53]: (ssSkP12(U_53) | ~c10_2(U_53, a1984)))). % 34.52/12.96 tff(c_614, plain, (![U_59]: (ssSkP6(U_59) | ~c5_2(U_59, a1888)))). % 34.52/12.96 tff(c_598, plain, (![U_55]: (ssSkP9(U_55) | ~c6_2(U_55, a1953)))). % 34.52/12.96 tff(c_360, plain, (![U_31]: (ssSkP9(U_31) | c10_2(U_31, a1953)))). % 34.52/12.96 tff(c_596, plain, (![U_54]: (ssSkP10(U_54) | ~c6_2(U_54, a1956)))). % 34.52/12.96 tff(c_418, plain, (![U_39]: (ssSkP4(U_39) | c6_2(U_39, a1855)))). % 34.52/12.96 tff(c_610, plain, (![U_57]: (ssSkP7(U_57) | ~c7_2(U_57, a1904)))). % 34.52/12.96 tff(c_414, plain, (![U_37]: (ssSkP4(U_37) | c10_2(U_37, a1855)))). % 34.52/12.96 tff(c_334, plain, (![U_25]: (ssSkP11(U_25) | c1_2(U_25, a1980)))). % 34.52/12.96 tff(c_570, plain, (![U_47]: (ssSkP16(U_47) | ~c5_2(U_47, a2031)))). % 34.52/12.96 tff(c_1725, plain, (c5_2(a1933, a1934))). % 34.52/12.96 tff(c_426, plain, (![U_41]: (ssSkP3(U_41) | c7_2(U_41, a1843)))). % 34.52/12.96 tff(c_584, plain, (![U_52]: (ssSkP13(U_52) | ~c2_2(U_52, a1990)))). % 34.52/12.96 tff(c_332, plain, (![U_24]: (ssSkP12(U_24) | c9_2(U_24, a1984)))). % 34.52/12.96 tff(c_326, plain, (![U_21]: (ssSkP14(U_21) | c10_2(U_21, a1992)))). % 34.52/12.96 tff(c_1716, plain, (~c1_2(a1933, a1934))). % 34.52/12.96 tff(c_608, plain, (![U_56]: (ssSkP7(U_56) | ~c8_2(U_56, a1904)))). % 34.52/12.96 tff(c_632, plain, (![U_65]: (ssSkP0(U_65) | ~c9_2(U_65, a1834)))). % 34.52/12.96 tff(c_356, plain, (![U_29]: (ssSkP10(U_29) | c1_2(U_29, a1956)))). % 34.52/12.96 tff(c_416, plain, (![U_38]: (ssSkP4(U_38) | c1_2(U_38, a1855)))). % 34.52/12.96 tff(c_324, plain, (![U_20]: (ssSkP14(U_20) | c8_2(U_20, a1992)))). % 34.52/12.96 tff(c_364, plain, (![U_32]: (ssSkP8(U_32) | c9_2(U_32, a1947)))). % 34.52/12.96 tff(c_442, plain, (![U_45]: (ssSkP1(U_45) | c5_2(U_45, a1835)))). % 34.52/12.96 tff(c_336, plain, (![U_26]: (ssSkP11(U_26) | c7_2(U_26, a1980)))). % 34.52/12.96 tff(c_394, plain, (![U_35]: (ssSkP7(U_35) | c10_2(U_35, a1904)))). % 34.52/12.96 tff(c_582, plain, (![U_51]: (ssSkP13(U_51) | ~c5_2(U_51, a1990)))). % 34.52/12.96 tff(c_354, plain, (![U_28]: (ssSkP10(U_28) | c8_2(U_28, a1956)))). % 34.52/12.96 tff(c_1702, plain, (~c2_2(a2006, a2007))). % 34.52/12.96 tff(c_1701, plain, (c6_2(a1879, a1880))). % 34.52/12.96 tff(c_1698, plain, (~c8_2(a1971, a1972))). % 34.52/12.96 tff(c_1693, plain, (~c7_2(a1971, a1972))). % 34.52/12.96 tff(c_1692, plain, (~c5_2(a1871, a1872))). % 34.52/12.96 tff(c_1691, plain, (~ssSkC1)). % 34.52/12.96 tff(c_1687, plain, (~ssSkC7)). % 34.52/12.96 tff(c_1685, plain, (c3_2(a1919, a1920))). % 34.52/12.96 tff(c_1684, plain, (c3_2(a1892, a1893))). % 34.52/12.96 tff(c_1683, plain, (~c1_2(a1919, a1920))). % 34.52/12.96 tff(c_1682, plain, (~c6_2(a1976, a1977))). % 34.52/12.96 tff(c_1680, plain, (~c3_2(a1879, a1880))). % 34.52/12.96 tff(c_1679, plain, (c8_2(a1839, a1840))). % 34.52/12.96 tff(c_1675, plain, (~c5_2(a1971, a1972))). % 34.52/12.96 tff(c_1673, plain, (~c3_2(a1910, a1911))). % 34.52/12.96 tff(c_1671, plain, (~c1_2(a1943, a1944))). % 34.52/12.96 tff(c_1668, plain, (~c4_2(a1910, a1911))). % 34.52/12.96 tff(c_1667, plain, (ndr1_1(a1915))). % 34.52/12.96 tff(c_1662, plain, (~c6_1(a1900))). % 34.52/12.96 tff(c_1655, plain, (~c2_2(a1998, a1999))). % 34.52/12.96 tff(c_1653, plain, (~c2_2(a1871, a1872))). % 34.52/12.96 tff(c_1648, plain, (ndr1_1(a1851))). % 34.52/12.96 tff(c_1644, plain, (~ssSkC36)). % 34.52/12.96 tff(c_1640, plain, (c5_1(a1915))). % 34.52/12.96 tff(c_1632, plain, (~ssSkC35)). % 34.52/12.96 tff(c_1628, plain, (c2_2(a1839, a1840))). % 34.52/12.96 tff(c_1627, plain, (ndr1_1(a1933))). % 34.52/12.96 tff(c_1625, plain, (c3_2(a1839, a1840))). % 34.52/12.96 tff(c_218, plain, (![U_17]: (ssSkP0(U_17) | ndr1_1(U_17)))). % 34.52/12.96 tff(c_1623, plain, (c5_2(a1879, a1880))). % 34.52/12.96 tff(c_146, plain, (![U_5]: (ssSkP12(U_5) | ndr1_1(U_5)))). % 34.52/12.96 tff(c_1621, plain, (c1_2(a1892, a1893))). % 34.52/12.96 tff(c_144, plain, (![U_4]: (ssSkP13(U_4) | ndr1_1(U_4)))). % 34.52/12.96 tff(c_1619, plain, (c6_2(a1892, a1893))). % 34.52/12.96 tff(c_1618, plain, (~c8_1(a1933))). % 34.52/12.96 tff(c_160, plain, (![U_8]: (ssSkP9(U_8) | ndr1_1(U_8)))). % 34.52/12.96 tff(c_184, plain, (![U_11]: (ssSkP6(U_11) | ndr1_1(U_11)))). % 34.52/12.96 tff(c_176, plain, (![U_10]: (ssSkP7(U_10) | ndr1_1(U_10)))). % 34.52/12.96 tff(c_1613, plain, (c9_2(a1919, a1920))). % 34.52/12.96 tff(c_1612, plain, (~c3_1(a1933))). % 34.52/12.96 tff(c_158, plain, (![U_7]: (ssSkP10(U_7) | ndr1_1(U_7)))). % 34.52/12.96 tff(c_196, plain, (![U_12]: (ssSkP5(U_12) | ndr1_1(U_12)))). % 34.52/12.96 tff(c_198, plain, (![U_13]: (ssSkP4(U_13) | ndr1_1(U_13)))). % 34.52/12.96 tff(c_134, plain, (![U_2]: (ssSkP15(U_2) | ndr1_1(U_2)))). % 34.52/12.96 tff(c_1604, plain, (c4_2(a2006, a2007))). % 34.52/12.96 tff(c_1603, plain, (~ssSkC13)). % 34.52/12.96 tff(c_1602, plain, (~ssSkC17)). % 34.52/12.96 tff(c_1599, plain, (ndr1_1(a1900))). % 34.52/12.96 tff(c_124, plain, (![U_1]: (ssSkP16(U_1) | ndr1_1(U_1)))). % 34.52/12.96 tff(c_1597, plain, (~ssSkC0)). % 34.52/12.96 tff(c_1595, plain, (~ssSkC20)). % 34.52/12.96 tff(c_1594, plain, (c7_2(a2006, a2007))). % 34.52/12.96 tff(c_216, plain, (![U_16]: (ssSkP1(U_16) | ndr1_1(U_16)))). % 34.52/12.96 tff(c_1586, plain, (c6_2(a1998, a2000))). % 34.52/12.96 tff(c_1585, plain, (c7_2(a1971, a1973))). % 34.52/12.96 tff(c_1584, plain, (~ssSkC25)). % 34.52/12.96 tff(c_1581, plain, (c8_2(a1976, a1977))). % 34.52/12.96 tff(c_1578, plain, (c9_2(a1998, a2000))). % 34.52/12.96 tff(c_1577, plain, (c10_2(a1998, a1999))). % 34.52/12.96 tff(c_1576, plain, (c1_2(a1998, a2000))). % 34.52/12.96 tff(c_1575, plain, (~ssSkC32)). % 34.52/12.96 tff(c_214, plain, (![U_15]: (ssSkP2(U_15) | ndr1_1(U_15)))). % 34.52/12.96 tff(c_208, plain, (![U_14]: (ssSkP3(U_14) | ndr1_1(U_14)))). % 34.52/12.96 tff(c_1570, plain, (c10_2(a1971, a1973))). % 34.52/12.96 tff(c_1569, plain, (c7_2(a1976, a1977))). % 34.52/12.96 tff(c_1568, plain, (c4_2(a1943, a1944))). % 34.52/12.96 tff(c_142, plain, (![U_3]: (ssSkP14(U_3) | ndr1_1(U_3)))). % 34.52/12.96 tff(c_1566, plain, (c10_2(a1943, a1944))). % 34.52/12.96 tff(c_164, plain, (![U_9]: (ssSkP8(U_9) | ndr1_1(U_9)))). % 34.52/12.96 tff(c_1562, plain, (c3_2(a1998, a1999))). % 34.52/12.97 tff(c_148, plain, (![U_6]: (ssSkP11(U_6) | ndr1_1(U_6)))). % 34.52/12.97 tff(c_1560, plain, (c4_1(a1892))). % 34.52/12.97 tff(c_1559, plain, (~ssSkC4)). % 34.52/12.97 tff(c_1558, plain, (ndr1_1(a1839))). % 34.52/12.97 tff(c_1557, plain, (ndr1_1(a1976))). % 34.52/12.97 tff(c_1555, plain, (c10_1(a1884))). % 34.52/12.97 tff(c_1552, plain, (ndr1_1(a2006))). % 34.52/12.97 tff(c_1551, plain, (c10_1(a2029))). % 34.52/12.97 tff(c_1550, plain, (c7_1(a1854))). % 34.52/12.97 tff(c_1549, plain, (ndr1_1(a1943))). % 34.52/12.97 tff(c_1548, plain, (c9_1(a1979))). % 34.52/12.97 tff(c_1545, plain, (c3_1(a2019))). % 34.52/12.97 tff(c_1544, plain, (ndr1_1(a1919))). % 34.52/12.97 tff(c_1542, plain, (ndr1_1(a1892))). % 34.52/12.97 tff(c_1539, plain, (c4_1(a2006))). % 34.52/12.97 tff(c_1538, plain, (c3_1(a2027))). % 34.52/12.97 tff(c_1537, plain, (c4_1(a2019))). % 34.52/12.97 tff(c_1536, plain, (c7_0)). % 34.52/12.97 tff(c_1535, plain, (c2_1(a1879))). % 34.52/12.97 tff(c_1534, plain, (c5_1(a1950))). % 34.52/12.97 tff(c_1531, plain, (c1_1(a1979))). % 34.52/12.97 tff(c_1530, plain, (c1_1(a1845))). % 34.52/12.97 tff(c_1529, plain, (ndr1_1(a1910))). % 34.52/12.97 tff(c_1528, plain, (c10_1(a1939))). % 34.52/12.97 tff(c_1527, plain, (ndr1_1(a1971))). % 34.52/12.97 tff(c_1525, plain, (c8_1(a1946))). % 34.52/12.97 tff(c_1524, plain, (c6_1(a1875))). % 34.52/12.97 tff(c_1523, plain, (~c10_1(a1907))). % 34.52/12.97 tff(c_1519, plain, (c6_1(a1854))). % 34.52/12.97 tff(c_1518, plain, (~ssSkC28)). % 34.52/12.97 tff(c_1517, plain, (c2_1(a1839))). % 34.52/12.97 tff(c_1516, plain, (c3_1(a1903))). % 34.52/12.97 tff(c_1515, plain, (c8_1(a2017))). % 34.52/12.97 tff(c_1512, plain, (~c1_1(a1976))). % 34.52/12.97 tff(c_1511, plain, (c3_1(a2017))). % 34.52/12.97 tff(c_1507, plain, (c2_1(a2014))). % 34.52/12.97 tff(c_1503, plain, (ndr1_1(a1998))). % 34.52/12.97 tff(c_1499, plain, (c3_1(a1854))). % 34.52/12.97 tff(c_1498, plain, (~c8_0)). % 34.52/12.97 tff(c_1495, plain, (~c2_1(a1848))). % 34.52/12.97 tff(c_1492, plain, (~c7_1(a1943))). % 34.52/12.97 tff(c_1490, plain, (c8_1(a1907))). % 34.52/12.97 tff(c_1481, plain, (~c4_1(a1919))). % 34.52/12.97 tff(c_1480, plain, (ndr1_1(a1871))). % 34.52/12.97 tff(c_1479, plain, (~ssSkC12)). % 34.52/12.97 tff(c_1478, plain, (ndr1_1(a1879))). % 34.52/12.97 tff(c_1477, plain, (~c6_0)). % 34.52/12.97 tff(c_1475, plain, (~c8_1(a1892))). % 34.52/12.97 tff(c_1474, plain, (~c6_1(a2030))). % 34.52/12.97 tff(c_1473, plain, (c5_1(a1907))). % 34.52/12.97 tff(c_1471, plain, (~c4_1(a1943))). % 34.52/12.97 tff(c_1469, plain, (~c1_1(a1946))). % 34.52/12.97 tff(c_1468, plain, (~c7_1(a2030))). % 34.52/12.97 tff(c_1467, plain, (~c9_1(a1919))). % 34.52/12.97 tff(c_1466, plain, (~c10_1(a1875))). % 34.52/12.97 tff(c_1465, plain, (~c10_1(a1839))). % 34.52/12.97 tff(c_1464, plain, (~c10_1(a1845))). % 34.52/12.97 tff(c_1463, plain, (~c6_1(a2027))). % 34.52/12.97 tff(c_1462, plain, (~c4_1(a2027))). % 34.52/12.97 tff(c_1461, plain, (~c2_1(a1913))). % 34.52/12.97 tff(c_1459, plain, (~c7_1(a1884))). % 34.52/12.97 tff(c_1458, plain, (~c1_1(a1950))). % 34.52/12.97 tff(c_1457, plain, (~c5_1(a1998))). % 34.52/12.97 tff(c_1456, plain, (~c7_1(a2014))). % 34.52/12.97 tff(c_1455, plain, (~c9_1(a1976))). % 34.52/12.97 tff(c_1454, plain, (~c3_1(a1971))). % 34.52/12.97 tff(c_1453, plain, (~c2_1(a1939))). % 34.52/12.97 tff(c_1452, plain, (~c5_1(a1924))). % 34.52/12.97 tff(c_1451, plain, (~c3_0)). % 34.52/12.97 tff(c_1423, plain, (c9_0)). % 34.52/12.97 tff(c_1415, plain, (~c10_0)). % 34.52/12.97 tff(c_1413, plain, (c5_0)). % 34.52/12.97 tff(c_1412, plain, (~c1_0)). % 34.52/12.97 tff(c_1404, plain, (ndr1_0)). % 34.52/12.97 tff(c_1403, plain, (~ssSkC39)). % 34.52/12.97 tff(c_1402, plain, (~c4_0)). % 34.52/12.97 tff(c_1401, plain, (~c2_0)). % 34.52/12.97 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.52/12.97 %------------------------------------------------------------------------------