%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN428+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:07:51 PM UTC 2026
% Result : CounterSatisfiable 0.54s 0.38s
% Output : FiniteModel 0.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_a1834,type,
a1834: $i ).
tff(a1834_definition,axiom,
a1834 = 'fmb_$i_1' ).
tff(declare_a1835,type,
a1835: $i ).
tff(a1835_definition,axiom,
a1835 = 'fmb_$i_2' ).
tff(declare_a1836,type,
a1836: $i ).
tff(a1836_definition,axiom,
a1836 = 'fmb_$i_2' ).
tff(declare_a1837,type,
a1837: $i ).
tff(a1837_definition,axiom,
a1837 = 'fmb_$i_2' ).
tff(declare_a1838,type,
a1838: $i ).
tff(a1838_definition,axiom,
a1838 = 'fmb_$i_2' ).
tff(declare_a1839,type,
a1839: $i ).
tff(a1839_definition,axiom,
a1839 = 'fmb_$i_1' ).
tff(declare_a1840,type,
a1840: $i ).
tff(a1840_definition,axiom,
a1840 = 'fmb_$i_2' ).
tff(declare_a1841,type,
a1841: $i ).
tff(a1841_definition,axiom,
a1841 = 'fmb_$i_2' ).
tff(declare_a1842,type,
a1842: $i ).
tff(a1842_definition,axiom,
a1842 = 'fmb_$i_2' ).
tff(declare_a1843,type,
a1843: $i ).
tff(a1843_definition,axiom,
a1843 = 'fmb_$i_2' ).
tff(declare_a1844,type,
a1844: $i ).
tff(a1844_definition,axiom,
a1844 = 'fmb_$i_2' ).
tff(declare_a1845,type,
a1845: $i ).
tff(a1845_definition,axiom,
a1845 = 'fmb_$i_2' ).
tff(declare_a1846,type,
a1846: $i ).
tff(a1846_definition,axiom,
a1846 = 'fmb_$i_2' ).
tff(declare_a1847,type,
a1847: $i ).
tff(a1847_definition,axiom,
a1847 = 'fmb_$i_2' ).
tff(declare_a1848,type,
a1848: $i ).
tff(a1848_definition,axiom,
a1848 = 'fmb_$i_2' ).
tff(declare_a1849,type,
a1849: $i ).
tff(a1849_definition,axiom,
a1849 = 'fmb_$i_2' ).
tff(declare_a1850,type,
a1850: $i ).
tff(a1850_definition,axiom,
a1850 = 'fmb_$i_2' ).
tff(declare_a1851,type,
a1851: $i ).
tff(a1851_definition,axiom,
a1851 = 'fmb_$i_2' ).
tff(declare_a1852,type,
a1852: $i ).
tff(a1852_definition,axiom,
a1852 = 'fmb_$i_2' ).
tff(declare_a1853,type,
a1853: $i ).
tff(a1853_definition,axiom,
a1853 = 'fmb_$i_2' ).
tff(declare_a1854,type,
a1854: $i ).
tff(a1854_definition,axiom,
a1854 = 'fmb_$i_2' ).
tff(declare_a1855,type,
a1855: $i ).
tff(a1855_definition,axiom,
a1855 = 'fmb_$i_2' ).
tff(declare_a1856,type,
a1856: $i ).
tff(a1856_definition,axiom,
a1856 = 'fmb_$i_2' ).
tff(declare_a1857,type,
a1857: $i ).
tff(a1857_definition,axiom,
a1857 = 'fmb_$i_2' ).
tff(declare_a1858,type,
a1858: $i ).
tff(a1858_definition,axiom,
a1858 = 'fmb_$i_2' ).
tff(declare_a1859,type,
a1859: $i ).
tff(a1859_definition,axiom,
a1859 = 'fmb_$i_2' ).
tff(declare_a1860,type,
a1860: $i ).
tff(a1860_definition,axiom,
a1860 = 'fmb_$i_2' ).
tff(declare_a1861,type,
a1861: $i ).
tff(a1861_definition,axiom,
a1861 = 'fmb_$i_2' ).
tff(declare_a1862,type,
a1862: $i ).
tff(a1862_definition,axiom,
a1862 = 'fmb_$i_2' ).
tff(declare_a1863,type,
a1863: $i ).
tff(a1863_definition,axiom,
a1863 = 'fmb_$i_2' ).
tff(declare_a1864,type,
a1864: $i ).
tff(a1864_definition,axiom,
a1864 = 'fmb_$i_2' ).
tff(declare_a1865,type,
a1865: $i ).
tff(a1865_definition,axiom,
a1865 = 'fmb_$i_2' ).
tff(declare_a1866,type,
a1866: $i ).
tff(a1866_definition,axiom,
a1866 = 'fmb_$i_2' ).
tff(declare_a1867,type,
a1867: $i ).
tff(a1867_definition,axiom,
a1867 = 'fmb_$i_2' ).
tff(declare_a1868,type,
a1868: $i ).
tff(a1868_definition,axiom,
a1868 = 'fmb_$i_2' ).
tff(declare_a1869,type,
a1869: $i ).
tff(a1869_definition,axiom,
a1869 = 'fmb_$i_2' ).
tff(declare_a1870,type,
a1870: $i ).
tff(a1870_definition,axiom,
a1870 = 'fmb_$i_2' ).
tff(declare_a1871,type,
a1871: $i ).
tff(a1871_definition,axiom,
a1871 = 'fmb_$i_2' ).
tff(declare_a1872,type,
a1872: $i ).
tff(a1872_definition,axiom,
a1872 = 'fmb_$i_2' ).
tff(declare_a1873,type,
a1873: $i ).
tff(a1873_definition,axiom,
a1873 = 'fmb_$i_2' ).
tff(declare_a1874,type,
a1874: $i ).
tff(a1874_definition,axiom,
a1874 = 'fmb_$i_2' ).
tff(declare_a1875,type,
a1875: $i ).
tff(a1875_definition,axiom,
a1875 = 'fmb_$i_2' ).
tff(declare_a1876,type,
a1876: $i ).
tff(a1876_definition,axiom,
a1876 = 'fmb_$i_2' ).
tff(declare_a1877,type,
a1877: $i ).
tff(a1877_definition,axiom,
a1877 = 'fmb_$i_2' ).
tff(declare_a1878,type,
a1878: $i ).
tff(a1878_definition,axiom,
a1878 = 'fmb_$i_2' ).
tff(declare_a1879,type,
a1879: $i ).
tff(a1879_definition,axiom,
a1879 = 'fmb_$i_2' ).
tff(declare_a1880,type,
a1880: $i ).
tff(a1880_definition,axiom,
a1880 = 'fmb_$i_2' ).
tff(declare_a1881,type,
a1881: $i ).
tff(a1881_definition,axiom,
a1881 = 'fmb_$i_2' ).
tff(declare_a1882,type,
a1882: $i ).
tff(a1882_definition,axiom,
a1882 = 'fmb_$i_2' ).
tff(declare_a1883,type,
a1883: $i ).
tff(a1883_definition,axiom,
a1883 = 'fmb_$i_2' ).
tff(declare_a1884,type,
a1884: $i ).
tff(a1884_definition,axiom,
a1884 = 'fmb_$i_2' ).
tff(declare_a1885,type,
a1885: $i ).
tff(a1885_definition,axiom,
a1885 = 'fmb_$i_2' ).
tff(declare_a1886,type,
a1886: $i ).
tff(a1886_definition,axiom,
a1886 = 'fmb_$i_2' ).
tff(declare_a1887,type,
a1887: $i ).
tff(a1887_definition,axiom,
a1887 = 'fmb_$i_2' ).
tff(declare_a1888,type,
a1888: $i ).
tff(a1888_definition,axiom,
a1888 = 'fmb_$i_2' ).
tff(declare_a1889,type,
a1889: $i ).
tff(a1889_definition,axiom,
a1889 = 'fmb_$i_2' ).
tff(declare_a1890,type,
a1890: $i ).
tff(a1890_definition,axiom,
a1890 = 'fmb_$i_2' ).
tff(declare_a1891,type,
a1891: $i ).
tff(a1891_definition,axiom,
a1891 = 'fmb_$i_2' ).
tff(declare_a1892,type,
a1892: $i ).
tff(a1892_definition,axiom,
a1892 = 'fmb_$i_2' ).
tff(declare_a1893,type,
a1893: $i ).
tff(a1893_definition,axiom,
a1893 = 'fmb_$i_2' ).
tff(declare_a1894,type,
a1894: $i ).
tff(a1894_definition,axiom,
a1894 = 'fmb_$i_2' ).
tff(declare_a1895,type,
a1895: $i ).
tff(a1895_definition,axiom,
a1895 = 'fmb_$i_2' ).
tff(declare_a1896,type,
a1896: $i ).
tff(a1896_definition,axiom,
a1896 = 'fmb_$i_2' ).
tff(declare_a1897,type,
a1897: $i ).
tff(a1897_definition,axiom,
a1897 = 'fmb_$i_2' ).
tff(declare_a1898,type,
a1898: $i ).
tff(a1898_definition,axiom,
a1898 = 'fmb_$i_2' ).
tff(declare_a1899,type,
a1899: $i ).
tff(a1899_definition,axiom,
a1899 = 'fmb_$i_2' ).
tff(declare_a1900,type,
a1900: $i ).
tff(a1900_definition,axiom,
a1900 = 'fmb_$i_2' ).
tff(declare_a1901,type,
a1901: $i ).
tff(a1901_definition,axiom,
a1901 = 'fmb_$i_2' ).
tff(declare_a1902,type,
a1902: $i ).
tff(a1902_definition,axiom,
a1902 = 'fmb_$i_2' ).
tff(declare_a1903,type,
a1903: $i ).
tff(a1903_definition,axiom,
a1903 = 'fmb_$i_2' ).
tff(declare_a1904,type,
a1904: $i ).
tff(a1904_definition,axiom,
a1904 = 'fmb_$i_2' ).
tff(declare_a1905,type,
a1905: $i ).
tff(a1905_definition,axiom,
a1905 = 'fmb_$i_2' ).
tff(declare_a1906,type,
a1906: $i ).
tff(a1906_definition,axiom,
a1906 = 'fmb_$i_2' ).
tff(declare_a1907,type,
a1907: $i ).
tff(a1907_definition,axiom,
a1907 = 'fmb_$i_2' ).
tff(declare_a1908,type,
a1908: $i ).
tff(a1908_definition,axiom,
a1908 = 'fmb_$i_2' ).
tff(declare_a1909,type,
a1909: $i ).
tff(a1909_definition,axiom,
a1909 = 'fmb_$i_2' ).
tff(declare_a1910,type,
a1910: $i ).
tff(a1910_definition,axiom,
a1910 = 'fmb_$i_2' ).
tff(declare_a1911,type,
a1911: $i ).
tff(a1911_definition,axiom,
a1911 = 'fmb_$i_2' ).
tff(declare_a1912,type,
a1912: $i ).
tff(a1912_definition,axiom,
a1912 = 'fmb_$i_2' ).
tff(declare_a1913,type,
a1913: $i ).
tff(a1913_definition,axiom,
a1913 = 'fmb_$i_2' ).
tff(declare_a1914,type,
a1914: $i ).
tff(a1914_definition,axiom,
a1914 = 'fmb_$i_2' ).
tff(declare_a1915,type,
a1915: $i ).
tff(a1915_definition,axiom,
a1915 = 'fmb_$i_1' ).
tff(declare_a1916,type,
a1916: $i ).
tff(a1916_definition,axiom,
a1916 = 'fmb_$i_2' ).
tff(declare_a1917,type,
a1917: $i ).
tff(a1917_definition,axiom,
a1917 = 'fmb_$i_2' ).
tff(declare_a1918,type,
a1918: $i ).
tff(a1918_definition,axiom,
a1918 = 'fmb_$i_2' ).
tff(declare_a1919,type,
a1919: $i ).
tff(a1919_definition,axiom,
a1919 = 'fmb_$i_2' ).
tff(declare_a1920,type,
a1920: $i ).
tff(a1920_definition,axiom,
a1920 = 'fmb_$i_2' ).
tff(declare_a1921,type,
a1921: $i ).
tff(a1921_definition,axiom,
a1921 = 'fmb_$i_2' ).
tff(declare_a1922,type,
a1922: $i ).
tff(a1922_definition,axiom,
a1922 = 'fmb_$i_2' ).
tff(declare_a1923,type,
a1923: $i ).
tff(a1923_definition,axiom,
a1923 = 'fmb_$i_2' ).
tff(declare_a1924,type,
a1924: $i ).
tff(a1924_definition,axiom,
a1924 = 'fmb_$i_2' ).
tff(declare_a1925,type,
a1925: $i ).
tff(a1925_definition,axiom,
a1925 = 'fmb_$i_2' ).
tff(declare_a1926,type,
a1926: $i ).
tff(a1926_definition,axiom,
a1926 = 'fmb_$i_2' ).
tff(declare_a1927,type,
a1927: $i ).
tff(a1927_definition,axiom,
a1927 = 'fmb_$i_1' ).
tff(declare_a1928,type,
a1928: $i ).
tff(a1928_definition,axiom,
a1928 = 'fmb_$i_2' ).
tff(declare_a1929,type,
a1929: $i ).
tff(a1929_definition,axiom,
a1929 = 'fmb_$i_2' ).
tff(declare_a1930,type,
a1930: $i ).
tff(a1930_definition,axiom,
a1930 = 'fmb_$i_2' ).
tff(declare_a1931,type,
a1931: $i ).
tff(a1931_definition,axiom,
a1931 = 'fmb_$i_2' ).
tff(declare_a1932,type,
a1932: $i ).
tff(a1932_definition,axiom,
a1932 = 'fmb_$i_2' ).
tff(declare_a1933,type,
a1933: $i ).
tff(a1933_definition,axiom,
a1933 = 'fmb_$i_2' ).
tff(declare_a1934,type,
a1934: $i ).
tff(a1934_definition,axiom,
a1934 = 'fmb_$i_2' ).
tff(declare_a1935,type,
a1935: $i ).
tff(a1935_definition,axiom,
a1935 = 'fmb_$i_2' ).
tff(declare_a1936,type,
a1936: $i ).
tff(a1936_definition,axiom,
a1936 = 'fmb_$i_2' ).
tff(declare_a1937,type,
a1937: $i ).
tff(a1937_definition,axiom,
a1937 = 'fmb_$i_2' ).
tff(declare_a1938,type,
a1938: $i ).
tff(a1938_definition,axiom,
a1938 = 'fmb_$i_2' ).
tff(declare_a1939,type,
a1939: $i ).
tff(a1939_definition,axiom,
a1939 = 'fmb_$i_2' ).
tff(declare_a1940,type,
a1940: $i ).
tff(a1940_definition,axiom,
a1940 = 'fmb_$i_2' ).
tff(declare_a1941,type,
a1941: $i ).
tff(a1941_definition,axiom,
a1941 = 'fmb_$i_2' ).
tff(declare_a1942,type,
a1942: $i ).
tff(a1942_definition,axiom,
a1942 = 'fmb_$i_2' ).
tff(declare_a1943,type,
a1943: $i ).
tff(a1943_definition,axiom,
a1943 = 'fmb_$i_2' ).
tff(declare_a1944,type,
a1944: $i ).
tff(a1944_definition,axiom,
a1944 = 'fmb_$i_2' ).
tff(declare_a1945,type,
a1945: $i ).
tff(a1945_definition,axiom,
a1945 = 'fmb_$i_2' ).
tff(declare_a1946,type,
a1946: $i ).
tff(a1946_definition,axiom,
a1946 = 'fmb_$i_2' ).
tff(declare_a1947,type,
a1947: $i ).
tff(a1947_definition,axiom,
a1947 = 'fmb_$i_2' ).
tff(declare_a1948,type,
a1948: $i ).
tff(a1948_definition,axiom,
a1948 = 'fmb_$i_2' ).
tff(declare_a1949,type,
a1949: $i ).
tff(a1949_definition,axiom,
a1949 = 'fmb_$i_2' ).
tff(declare_a1950,type,
a1950: $i ).
tff(a1950_definition,axiom,
a1950 = 'fmb_$i_2' ).
tff(declare_a1951,type,
a1951: $i ).
tff(a1951_definition,axiom,
a1951 = 'fmb_$i_1' ).
tff(declare_a1952,type,
a1952: $i ).
tff(a1952_definition,axiom,
a1952 = 'fmb_$i_2' ).
tff(declare_a1953,type,
a1953: $i ).
tff(a1953_definition,axiom,
a1953 = 'fmb_$i_2' ).
tff(declare_a1954,type,
a1954: $i ).
tff(a1954_definition,axiom,
a1954 = 'fmb_$i_2' ).
tff(declare_a1955,type,
a1955: $i ).
tff(a1955_definition,axiom,
a1955 = 'fmb_$i_2' ).
tff(declare_a1956,type,
a1956: $i ).
tff(a1956_definition,axiom,
a1956 = 'fmb_$i_2' ).
tff(declare_a1957,type,
a1957: $i ).
tff(a1957_definition,axiom,
a1957 = 'fmb_$i_2' ).
tff(declare_a1958,type,
a1958: $i ).
tff(a1958_definition,axiom,
a1958 = 'fmb_$i_2' ).
tff(declare_a1959,type,
a1959: $i ).
tff(a1959_definition,axiom,
a1959 = 'fmb_$i_2' ).
tff(declare_a1960,type,
a1960: $i ).
tff(a1960_definition,axiom,
a1960 = 'fmb_$i_2' ).
tff(declare_a1961,type,
a1961: $i ).
tff(a1961_definition,axiom,
a1961 = 'fmb_$i_2' ).
tff(declare_a1962,type,
a1962: $i ).
tff(a1962_definition,axiom,
a1962 = 'fmb_$i_2' ).
tff(declare_a1963,type,
a1963: $i ).
tff(a1963_definition,axiom,
a1963 = 'fmb_$i_2' ).
tff(declare_a1964,type,
a1964: $i ).
tff(a1964_definition,axiom,
a1964 = 'fmb_$i_2' ).
tff(declare_a1965,type,
a1965: $i ).
tff(a1965_definition,axiom,
a1965 = 'fmb_$i_2' ).
tff(declare_a1966,type,
a1966: $i ).
tff(a1966_definition,axiom,
a1966 = 'fmb_$i_2' ).
tff(declare_a1967,type,
a1967: $i ).
tff(a1967_definition,axiom,
a1967 = 'fmb_$i_2' ).
tff(declare_a1968,type,
a1968: $i ).
tff(a1968_definition,axiom,
a1968 = 'fmb_$i_2' ).
tff(declare_a1969,type,
a1969: $i ).
tff(a1969_definition,axiom,
a1969 = 'fmb_$i_2' ).
tff(declare_a1970,type,
a1970: $i ).
tff(a1970_definition,axiom,
a1970 = 'fmb_$i_2' ).
tff(declare_a1971,type,
a1971: $i ).
tff(a1971_definition,axiom,
a1971 = 'fmb_$i_2' ).
tff(declare_a1972,type,
a1972: $i ).
tff(a1972_definition,axiom,
a1972 = 'fmb_$i_2' ).
tff(declare_a1973,type,
a1973: $i ).
tff(a1973_definition,axiom,
a1973 = 'fmb_$i_2' ).
tff(declare_a1974,type,
a1974: $i ).
tff(a1974_definition,axiom,
a1974 = 'fmb_$i_2' ).
tff(declare_a1975,type,
a1975: $i ).
tff(a1975_definition,axiom,
a1975 = 'fmb_$i_2' ).
tff(declare_a1976,type,
a1976: $i ).
tff(a1976_definition,axiom,
a1976 = 'fmb_$i_2' ).
tff(declare_a1977,type,
a1977: $i ).
tff(a1977_definition,axiom,
a1977 = 'fmb_$i_2' ).
tff(declare_a1978,type,
a1978: $i ).
tff(a1978_definition,axiom,
a1978 = 'fmb_$i_2' ).
tff(declare_a1979,type,
a1979: $i ).
tff(a1979_definition,axiom,
a1979 = 'fmb_$i_2' ).
tff(declare_a1980,type,
a1980: $i ).
tff(a1980_definition,axiom,
a1980 = 'fmb_$i_2' ).
tff(declare_a1981,type,
a1981: $i ).
tff(a1981_definition,axiom,
a1981 = 'fmb_$i_2' ).
tff(declare_a1982,type,
a1982: $i ).
tff(a1982_definition,axiom,
a1982 = 'fmb_$i_2' ).
tff(declare_a1983,type,
a1983: $i ).
tff(a1983_definition,axiom,
a1983 = 'fmb_$i_2' ).
tff(declare_a1984,type,
a1984: $i ).
tff(a1984_definition,axiom,
a1984 = 'fmb_$i_2' ).
tff(declare_a1985,type,
a1985: $i ).
tff(a1985_definition,axiom,
a1985 = 'fmb_$i_2' ).
tff(declare_a1986,type,
a1986: $i ).
tff(a1986_definition,axiom,
a1986 = 'fmb_$i_2' ).
tff(declare_a1987,type,
a1987: $i ).
tff(a1987_definition,axiom,
a1987 = 'fmb_$i_2' ).
tff(declare_a1988,type,
a1988: $i ).
tff(a1988_definition,axiom,
a1988 = 'fmb_$i_2' ).
tff(declare_a1989,type,
a1989: $i ).
tff(a1989_definition,axiom,
a1989 = 'fmb_$i_2' ).
tff(declare_a1990,type,
a1990: $i ).
tff(a1990_definition,axiom,
a1990 = 'fmb_$i_2' ).
tff(declare_a1991,type,
a1991: $i ).
tff(a1991_definition,axiom,
a1991 = 'fmb_$i_2' ).
tff(declare_a1992,type,
a1992: $i ).
tff(a1992_definition,axiom,
a1992 = 'fmb_$i_2' ).
tff(declare_a1993,type,
a1993: $i ).
tff(a1993_definition,axiom,
a1993 = 'fmb_$i_2' ).
tff(declare_a1994,type,
a1994: $i ).
tff(a1994_definition,axiom,
a1994 = 'fmb_$i_2' ).
tff(declare_a1995,type,
a1995: $i ).
tff(a1995_definition,axiom,
a1995 = 'fmb_$i_2' ).
tff(declare_a1996,type,
a1996: $i ).
tff(a1996_definition,axiom,
a1996 = 'fmb_$i_2' ).
tff(declare_a1997,type,
a1997: $i ).
tff(a1997_definition,axiom,
a1997 = 'fmb_$i_2' ).
tff(declare_a1998,type,
a1998: $i ).
tff(a1998_definition,axiom,
a1998 = 'fmb_$i_2' ).
tff(declare_a1999,type,
a1999: $i ).
tff(a1999_definition,axiom,
a1999 = 'fmb_$i_2' ).
tff(declare_a2000,type,
a2000: $i ).
tff(a2000_definition,axiom,
a2000 = 'fmb_$i_2' ).
tff(declare_a2001,type,
a2001: $i ).
tff(a2001_definition,axiom,
a2001 = 'fmb_$i_2' ).
tff(declare_a2002,type,
a2002: $i ).
tff(a2002_definition,axiom,
a2002 = 'fmb_$i_2' ).
tff(declare_a2003,type,
a2003: $i ).
tff(a2003_definition,axiom,
a2003 = 'fmb_$i_2' ).
tff(declare_a2004,type,
a2004: $i ).
tff(a2004_definition,axiom,
a2004 = 'fmb_$i_2' ).
tff(declare_a2005,type,
a2005: $i ).
tff(a2005_definition,axiom,
a2005 = 'fmb_$i_2' ).
tff(declare_a2006,type,
a2006: $i ).
tff(a2006_definition,axiom,
a2006 = 'fmb_$i_2' ).
tff(declare_a2007,type,
a2007: $i ).
tff(a2007_definition,axiom,
a2007 = 'fmb_$i_2' ).
tff(declare_a2008,type,
a2008: $i ).
tff(a2008_definition,axiom,
a2008 = 'fmb_$i_2' ).
tff(declare_a2009,type,
a2009: $i ).
tff(a2009_definition,axiom,
a2009 = 'fmb_$i_2' ).
tff(declare_a2010,type,
a2010: $i ).
tff(a2010_definition,axiom,
a2010 = 'fmb_$i_2' ).
tff(declare_a2011,type,
a2011: $i ).
tff(a2011_definition,axiom,
a2011 = 'fmb_$i_2' ).
tff(declare_a2012,type,
a2012: $i ).
tff(a2012_definition,axiom,
a2012 = 'fmb_$i_2' ).
tff(declare_a2013,type,
a2013: $i ).
tff(a2013_definition,axiom,
a2013 = 'fmb_$i_2' ).
tff(declare_a2014,type,
a2014: $i ).
tff(a2014_definition,axiom,
a2014 = 'fmb_$i_2' ).
tff(declare_a2015,type,
a2015: $i ).
tff(a2015_definition,axiom,
a2015 = 'fmb_$i_2' ).
tff(declare_a2016,type,
a2016: $i ).
tff(a2016_definition,axiom,
a2016 = 'fmb_$i_1' ).
tff(declare_a2017,type,
a2017: $i ).
tff(a2017_definition,axiom,
a2017 = 'fmb_$i_2' ).
tff(declare_a2018,type,
a2018: $i ).
tff(a2018_definition,axiom,
a2018 = 'fmb_$i_2' ).
tff(declare_a2019,type,
a2019: $i ).
tff(a2019_definition,axiom,
a2019 = 'fmb_$i_2' ).
tff(declare_a2020,type,
a2020: $i ).
tff(a2020_definition,axiom,
a2020 = 'fmb_$i_2' ).
tff(declare_a2021,type,
a2021: $i ).
tff(a2021_definition,axiom,
a2021 = 'fmb_$i_1' ).
tff(declare_a2022,type,
a2022: $i ).
tff(a2022_definition,axiom,
a2022 = 'fmb_$i_2' ).
tff(declare_a2023,type,
a2023: $i ).
tff(a2023_definition,axiom,
a2023 = 'fmb_$i_2' ).
tff(declare_a2024,type,
a2024: $i ).
tff(a2024_definition,axiom,
a2024 = 'fmb_$i_2' ).
tff(declare_a2025,type,
a2025: $i ).
tff(a2025_definition,axiom,
a2025 = 'fmb_$i_2' ).
tff(declare_a2026,type,
a2026: $i ).
tff(a2026_definition,axiom,
a2026 = 'fmb_$i_2' ).
tff(declare_a2027,type,
a2027: $i ).
tff(a2027_definition,axiom,
a2027 = 'fmb_$i_2' ).
tff(declare_a2028,type,
a2028: $i ).
tff(a2028_definition,axiom,
a2028 = 'fmb_$i_2' ).
tff(declare_a2029,type,
a2029: $i ).
tff(a2029_definition,axiom,
a2029 = 'fmb_$i_1' ).
tff(declare_a2030,type,
a2030: $i ).
tff(a2030_definition,axiom,
a2030 = 'fmb_$i_2' ).
tff(declare_a2031,type,
a2031: $i ).
tff(a2031_definition,axiom,
a2031 = 'fmb_$i_2' ).
tff(declare_a2032,type,
a2032: $i ).
tff(a2032_definition,axiom,
a2032 = 'fmb_$i_2' ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_c4_0,type,
c4_0: $o ).
tff(c4_0_definition,axiom,
~ c4_0 ).
tff(declare_c6_0,type,
c6_0: $o ).
tff(c6_0_definition,axiom,
~ c6_0 ).
tff(declare_c7_0,type,
c7_0: $o ).
tff(c7_0_definition,axiom,
c7_0 ).
tff(declare_c8_0,type,
c8_0: $o ).
tff(c8_0_definition,axiom,
c8_0 ).
tff(declare_c5_0,type,
c5_0: $o ).
tff(c5_0_definition,axiom,
~ c5_0 ).
tff(declare_c9_0,type,
c9_0: $o ).
tff(c9_0_definition,axiom,
c9_0 ).
tff(declare_c10_0,type,
c10_0: $o ).
tff(c10_0_definition,axiom,
~ c10_0 ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
~ c1_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
c3_0 ).
tff(declare_c2_0,type,
c2_0: $o ).
tff(c2_0_definition,axiom,
~ c2_0 ).
tff(declare_ndr1_1,type,
ndr1_1: $i > $o ).
tff(predicate_ndr1_1,axiom,
( ndr1_1('fmb_$i_1')
& ndr1_1('fmb_$i_2') ) ).
tff(declare_c9_2,type,
c9_2: ( $i * $i ) > $o ).
tff(predicate_c9_2,axiom,
( ~ c9_2('fmb_$i_1','fmb_$i_1')
& ~ c9_2('fmb_$i_1','fmb_$i_2')
& ~ c9_2('fmb_$i_2','fmb_$i_1')
& ~ c9_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c3_2,type,
c3_2: ( $i * $i ) > $o ).
tff(predicate_c3_2,axiom,
( ~ c3_2('fmb_$i_1','fmb_$i_1')
& ~ c3_2('fmb_$i_1','fmb_$i_2')
& ~ c3_2('fmb_$i_2','fmb_$i_1')
& c3_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c7_2,type,
c7_2: ( $i * $i ) > $o ).
tff(predicate_c7_2,axiom,
( c7_2('fmb_$i_1','fmb_$i_1')
& c7_2('fmb_$i_1','fmb_$i_2')
& c7_2('fmb_$i_2','fmb_$i_1')
& c7_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c5_2,type,
c5_2: ( $i * $i ) > $o ).
tff(predicate_c5_2,axiom,
( ~ c5_2('fmb_$i_1','fmb_$i_1')
& c5_2('fmb_$i_1','fmb_$i_2')
& ~ c5_2('fmb_$i_2','fmb_$i_1')
& c5_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c1_2,type,
c1_2: ( $i * $i ) > $o ).
tff(predicate_c1_2,axiom,
( c1_2('fmb_$i_1','fmb_$i_1')
& c1_2('fmb_$i_1','fmb_$i_2')
& c1_2('fmb_$i_2','fmb_$i_1')
& ~ c1_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c4_2,type,
c4_2: ( $i * $i ) > $o ).
tff(predicate_c4_2,axiom,
( ~ c4_2('fmb_$i_1','fmb_$i_1')
& c4_2('fmb_$i_1','fmb_$i_2')
& ~ c4_2('fmb_$i_2','fmb_$i_1')
& ~ c4_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c6_2,type,
c6_2: ( $i * $i ) > $o ).
tff(predicate_c6_2,axiom,
( ~ c6_2('fmb_$i_1','fmb_$i_1')
& ~ c6_2('fmb_$i_1','fmb_$i_2')
& c6_2('fmb_$i_2','fmb_$i_1')
& c6_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c6_1,type,
c6_1: $i > $o ).
tff(predicate_c6_1,axiom,
( ~ c6_1('fmb_$i_1')
& ~ c6_1('fmb_$i_2') ) ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
( c4_1('fmb_$i_1')
& c4_1('fmb_$i_2') ) ).
tff(declare_c10_2,type,
c10_2: ( $i * $i ) > $o ).
tff(predicate_c10_2,axiom,
( c10_2('fmb_$i_1','fmb_$i_1')
& c10_2('fmb_$i_1','fmb_$i_2')
& ~ c10_2('fmb_$i_2','fmb_$i_1')
& ~ c10_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c10_1,type,
c10_1: $i > $o ).
tff(predicate_c10_1,axiom,
( c10_1('fmb_$i_1')
& c10_1('fmb_$i_2') ) ).
tff(declare_c8_2,type,
c8_2: ( $i * $i ) > $o ).
tff(predicate_c8_2,axiom,
( c8_2('fmb_$i_1','fmb_$i_1')
& c8_2('fmb_$i_1','fmb_$i_2')
& ~ c8_2('fmb_$i_2','fmb_$i_1')
& c8_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c2_2,type,
c2_2: ( $i * $i ) > $o ).
tff(predicate_c2_2,axiom,
( c2_2('fmb_$i_1','fmb_$i_1')
& c2_2('fmb_$i_1','fmb_$i_2')
& c2_2('fmb_$i_2','fmb_$i_1')
& ~ c2_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
( ~ c2_1('fmb_$i_1')
& ~ c2_1('fmb_$i_2') ) ).
tff(declare_c9_1,type,
c9_1: $i > $o ).
tff(predicate_c9_1,axiom,
( ~ c9_1('fmb_$i_1')
& c9_1('fmb_$i_2') ) ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
( ~ c3_1('fmb_$i_1')
& c3_1('fmb_$i_2') ) ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
( ~ c1_1('fmb_$i_1')
& c1_1('fmb_$i_2') ) ).
tff(declare_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
( c5_1('fmb_$i_1')
& ~ c5_1('fmb_$i_2') ) ).
tff(declare_c7_1,type,
c7_1: $i > $o ).
tff(predicate_c7_1,axiom,
( ~ c7_1('fmb_$i_1')
& ~ c7_1('fmb_$i_2') ) ).
tff(declare_c8_1,type,
c8_1: $i > $o ).
tff(predicate_c8_1,axiom,
( ~ c8_1('fmb_$i_1')
& c8_1('fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN428+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.25 % Computer : n013.cluster.edu
% 0.09/0.25 % Model : x86_64 x86_64
% 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.25 % Memory : 8046.5625MB
% 0.09/0.25 % OS : Linux 6.8.0-71-generic
% 0.09/0.25 % CPULimit : 300
% 0.09/0.25 % WCLimit : 300
% 0.09/0.25 % DateTime : Mon Sep 28 15:58:36 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.23/0.28 Running first-order model finding
% 0.23/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.54/0.38 % (1298406)Will run a generic schedule for satisfiability detection.
% 0.54/0.38 % (1298416)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2589102348:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.54/0.38 % (1298412)% WARNING: option uhcvi not known.
% 0.54/0.38 % (1298411)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=349861533_2999 on theBenchmark for (2999ds/0Mi)
% 0.54/0.38 % (1298413)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2057088279:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.54/0.38 % (1298414)dis+10_1_sil=32000:sp=arity:random_seed=663744875:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.54/0.38 % (1298412)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=497478810:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.54/0.38 % (1298417)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3737097216:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.54/0.38 % (1298415)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1840134046:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.54/0.38 % (1298416)Instruction limit reached!
% 0.54/0.38 % (1298416)------------------------------
% 0.54/0.38 % (1298416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.38 % (1298416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.38 % (1298416)CaDiCaL version: 2.1.3
% 0.54/0.38 % (1298416)Termination reason: Instruction limit
% 0.54/0.38 % (1298416)Termination phase: Saturation
% 0.54/0.38 % (1298416)Time elapsed: 0.041 s
% 0.54/0.38 % (1298416)Peak memory usage: 16 MB
% 0.54/0.38 % (1298416)Instructions burned: 134 (million)
% 0.54/0.38 % Detected minimum model sizes of [1]
% 0.54/0.38 % Detected maximum model sizes of [199]
% 0.54/0.38 % TRYING [1]
% 0.54/0.38 % TRYING [2]
% 0.54/0.38 % (1298425)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3838329619:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.54/0.38 % Finite Model Found!
% 0.54/0.38 % SZS status CounterSatisfiable for theBenchmark
% 0.54/0.38 % (1298411) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1298406-1298411"...
% 0.54/0.38 % (1298411)...printing done.
% 0.54/0.38 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.54/0.39 % (1298411)------------------------------
% 0.54/0.39 % (1298411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.39 % (1298411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.39 % (1298411)CaDiCaL version: 2.1.3
% 0.54/0.39 % (1298411)Termination reason: Satisfiable
% 0.54/0.39 % (1298411)Time elapsed: 0.052 s
% 0.54/0.39 % (1298411)Peak memory usage: 14 MB
% 0.54/0.39 % (1298411)Instructions burned: 107 (million)
% 0.54/0.39 % (1298406)Success in time 0.093 s
% 0.54/0.39 % Vampire exiting
%------------------------------------------------------------------------------