%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN441+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:08:23 PM UTC 2026
% Result : CounterSatisfiable 0.30s 0.31s
% Output : FiniteModel 0.30s
% 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('declare_$i3',type,
'fmb_$i_3': $i ).
tff('declare_$i4',type,
'fmb_$i_4': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' )
| ( X = 'fmb_$i_3' )
| ( X = 'fmb_$i_4' ) ) ).
tff('distinct_domain_$i',axiom,
( ( 'fmb_$i_1' != 'fmb_$i_2' )
& ( 'fmb_$i_1' != 'fmb_$i_3' )
& ( 'fmb_$i_1' != 'fmb_$i_4' )
& ( 'fmb_$i_2' != 'fmb_$i_3' )
& ( 'fmb_$i_2' != 'fmb_$i_4' )
& ( 'fmb_$i_3' != 'fmb_$i_4' ) ) ).
tff(declare_a1818,type,
a1818: $i ).
tff(a1818_definition,axiom,
a1818 = 'fmb_$i_1' ).
tff(declare_a1824,type,
a1824: $i ).
tff(a1824_definition,axiom,
a1824 = 'fmb_$i_2' ).
tff(declare_a1826,type,
a1826: $i ).
tff(a1826_definition,axiom,
a1826 = 'fmb_$i_3' ).
tff(declare_a1828,type,
a1828: $i ).
tff(a1828_definition,axiom,
a1828 = 'fmb_$i_4' ).
tff(declare_a1829,type,
a1829: $i ).
tff(a1829_definition,axiom,
a1829 = 'fmb_$i_4' ).
tff(declare_a1831,type,
a1831: $i ).
tff(a1831_definition,axiom,
a1831 = 'fmb_$i_1' ).
tff(declare_a1832,type,
a1832: $i ).
tff(a1832_definition,axiom,
a1832 = 'fmb_$i_1' ).
tff(declare_a1833,type,
a1833: $i ).
tff(a1833_definition,axiom,
a1833 = 'fmb_$i_3' ).
tff(declare_a1837,type,
a1837: $i ).
tff(a1837_definition,axiom,
a1837 = 'fmb_$i_4' ).
tff(declare_a1840,type,
a1840: $i ).
tff(a1840_definition,axiom,
a1840 = 'fmb_$i_4' ).
tff(declare_a1841,type,
a1841: $i ).
tff(a1841_definition,axiom,
a1841 = 'fmb_$i_4' ).
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_4' ).
tff(declare_a1846,type,
a1846: $i ).
tff(a1846_definition,axiom,
a1846 = 'fmb_$i_4' ).
tff(declare_a1847,type,
a1847: $i ).
tff(a1847_definition,axiom,
a1847 = 'fmb_$i_2' ).
tff(declare_a1850,type,
a1850: $i ).
tff(a1850_definition,axiom,
a1850 = 'fmb_$i_1' ).
tff(declare_a1851,type,
a1851: $i ).
tff(a1851_definition,axiom,
a1851 = 'fmb_$i_3' ).
tff(declare_a1853,type,
a1853: $i ).
tff(a1853_definition,axiom,
a1853 = 'fmb_$i_3' ).
tff(declare_a1854,type,
a1854: $i ).
tff(a1854_definition,axiom,
a1854 = 'fmb_$i_3' ).
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_4' ).
tff(declare_a1857,type,
a1857: $i ).
tff(a1857_definition,axiom,
a1857 = 'fmb_$i_1' ).
tff(declare_a1858,type,
a1858: $i ).
tff(a1858_definition,axiom,
a1858 = 'fmb_$i_4' ).
tff(declare_a1859,type,
a1859: $i ).
tff(a1859_definition,axiom,
a1859 = 'fmb_$i_4' ).
tff(declare_a1862,type,
a1862: $i ).
tff(a1862_definition,axiom,
a1862 = 'fmb_$i_3' ).
tff(declare_a1864,type,
a1864: $i ).
tff(a1864_definition,axiom,
a1864 = 'fmb_$i_4' ).
tff(declare_a1866,type,
a1866: $i ).
tff(a1866_definition,axiom,
a1866 = 'fmb_$i_1' ).
tff(declare_a1869,type,
a1869: $i ).
tff(a1869_definition,axiom,
a1869 = 'fmb_$i_3' ).
tff(declare_a1870,type,
a1870: $i ).
tff(a1870_definition,axiom,
a1870 = 'fmb_$i_4' ).
tff(declare_a1872,type,
a1872: $i ).
tff(a1872_definition,axiom,
a1872 = 'fmb_$i_1' ).
tff(declare_a1873,type,
a1873: $i ).
tff(a1873_definition,axiom,
a1873 = 'fmb_$i_1' ).
tff(declare_a1875,type,
a1875: $i ).
tff(a1875_definition,axiom,
a1875 = 'fmb_$i_1' ).
tff(declare_a1876,type,
a1876: $i ).
tff(a1876_definition,axiom,
a1876 = 'fmb_$i_1' ).
tff(declare_a1881,type,
a1881: $i ).
tff(a1881_definition,axiom,
a1881 = 'fmb_$i_1' ).
tff(declare_a1882,type,
a1882: $i ).
tff(a1882_definition,axiom,
a1882 = 'fmb_$i_3' ).
tff(declare_a1890,type,
a1890: $i ).
tff(a1890_definition,axiom,
a1890 = 'fmb_$i_4' ).
tff(declare_a1891,type,
a1891: $i ).
tff(a1891_definition,axiom,
a1891 = 'fmb_$i_1' ).
tff(declare_a1892,type,
a1892: $i ).
tff(a1892_definition,axiom,
a1892 = 'fmb_$i_1' ).
tff(declare_a1895,type,
a1895: $i ).
tff(a1895_definition,axiom,
a1895 = 'fmb_$i_1' ).
tff(declare_a1896,type,
a1896: $i ).
tff(a1896_definition,axiom,
a1896 = 'fmb_$i_1' ).
tff(declare_a1900,type,
a1900: $i ).
tff(a1900_definition,axiom,
a1900 = 'fmb_$i_1' ).
tff(declare_a1901,type,
a1901: $i ).
tff(a1901_definition,axiom,
a1901 = 'fmb_$i_4' ).
tff(declare_a1819,type,
a1819: $i ).
tff(a1819_definition,axiom,
a1819 = 'fmb_$i_4' ).
tff(declare_a1820,type,
a1820: $i ).
tff(a1820_definition,axiom,
a1820 = 'fmb_$i_1' ).
tff(declare_a1821,type,
a1821: $i ).
tff(a1821_definition,axiom,
a1821 = 'fmb_$i_3' ).
tff(declare_a1822,type,
a1822: $i ).
tff(a1822_definition,axiom,
a1822 = 'fmb_$i_1' ).
tff(declare_a1823,type,
a1823: $i ).
tff(a1823_definition,axiom,
a1823 = 'fmb_$i_1' ).
tff(declare_a1825,type,
a1825: $i ).
tff(a1825_definition,axiom,
a1825 = 'fmb_$i_1' ).
tff(declare_a1827,type,
a1827: $i ).
tff(a1827_definition,axiom,
a1827 = 'fmb_$i_1' ).
tff(declare_a1830,type,
a1830: $i ).
tff(a1830_definition,axiom,
a1830 = 'fmb_$i_3' ).
tff(declare_a1834,type,
a1834: $i ).
tff(a1834_definition,axiom,
a1834 = 'fmb_$i_4' ).
tff(declare_a1835,type,
a1835: $i ).
tff(a1835_definition,axiom,
a1835 = 'fmb_$i_1' ).
tff(declare_a1836,type,
a1836: $i ).
tff(a1836_definition,axiom,
a1836 = 'fmb_$i_1' ).
tff(declare_a1838,type,
a1838: $i ).
tff(a1838_definition,axiom,
a1838 = 'fmb_$i_1' ).
tff(declare_a1839,type,
a1839: $i ).
tff(a1839_definition,axiom,
a1839 = 'fmb_$i_1' ).
tff(declare_a1842,type,
a1842: $i ).
tff(a1842_definition,axiom,
a1842 = 'fmb_$i_4' ).
tff(declare_a1845,type,
a1845: $i ).
tff(a1845_definition,axiom,
a1845 = 'fmb_$i_4' ).
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_1' ).
tff(declare_a1852,type,
a1852: $i ).
tff(a1852_definition,axiom,
a1852 = 'fmb_$i_1' ).
tff(declare_a1860,type,
a1860: $i ).
tff(a1860_definition,axiom,
a1860 = 'fmb_$i_4' ).
tff(declare_a1863,type,
a1863: $i ).
tff(a1863_definition,axiom,
a1863 = 'fmb_$i_1' ).
tff(declare_a1867,type,
a1867: $i ).
tff(a1867_definition,axiom,
a1867 = 'fmb_$i_1' ).
tff(declare_a1868,type,
a1868: $i ).
tff(a1868_definition,axiom,
a1868 = 'fmb_$i_2' ).
tff(declare_a1874,type,
a1874: $i ).
tff(a1874_definition,axiom,
a1874 = 'fmb_$i_4' ).
tff(declare_a1878,type,
a1878: $i ).
tff(a1878_definition,axiom,
a1878 = 'fmb_$i_1' ).
tff(declare_a1879,type,
a1879: $i ).
tff(a1879_definition,axiom,
a1879 = 'fmb_$i_2' ).
tff(declare_a1885,type,
a1885: $i ).
tff(a1885_definition,axiom,
a1885 = 'fmb_$i_1' ).
tff(declare_a1886,type,
a1886: $i ).
tff(a1886_definition,axiom,
a1886 = 'fmb_$i_1' ).
tff(declare_a1887,type,
a1887: $i ).
tff(a1887_definition,axiom,
a1887 = 'fmb_$i_1' ).
tff(declare_a1889,type,
a1889: $i ).
tff(a1889_definition,axiom,
a1889 = 'fmb_$i_4' ).
tff(declare_a1894,type,
a1894: $i ).
tff(a1894_definition,axiom,
a1894 = 'fmb_$i_3' ).
tff(declare_a1897,type,
a1897: $i ).
tff(a1897_definition,axiom,
a1897 = 'fmb_$i_1' ).
tff(declare_a1898,type,
a1898: $i ).
tff(a1898_definition,axiom,
a1898 = 'fmb_$i_1' ).
tff(declare_a1899,type,
a1899: $i ).
tff(a1899_definition,axiom,
a1899 = 'fmb_$i_1' ).
tff(declare_a1902,type,
a1902: $i ).
tff(a1902_definition,axiom,
a1902 = 'fmb_$i_1' ).
tff(declare_hskp0,type,
hskp0: $o ).
tff(hskp0_definition,axiom,
~ hskp0 ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_hskp1,type,
hskp1: $o ).
tff(hskp1_definition,axiom,
~ hskp1 ).
tff(declare_hskp2,type,
hskp2: $o ).
tff(hskp2_definition,axiom,
hskp2 ).
tff(declare_hskp3,type,
hskp3: $o ).
tff(hskp3_definition,axiom,
~ hskp3 ).
tff(declare_hskp4,type,
hskp4: $o ).
tff(hskp4_definition,axiom,
hskp4 ).
tff(declare_hskp5,type,
hskp5: $o ).
tff(hskp5_definition,axiom,
~ hskp5 ).
tff(declare_hskp6,type,
hskp6: $o ).
tff(hskp6_definition,axiom,
~ hskp6 ).
tff(declare_hskp7,type,
hskp7: $o ).
tff(hskp7_definition,axiom,
hskp7 ).
tff(declare_hskp8,type,
hskp8: $o ).
tff(hskp8_definition,axiom,
~ hskp8 ).
tff(declare_hskp9,type,
hskp9: $o ).
tff(hskp9_definition,axiom,
~ hskp9 ).
tff(declare_hskp10,type,
hskp10: $o ).
tff(hskp10_definition,axiom,
~ hskp10 ).
tff(declare_hskp11,type,
hskp11: $o ).
tff(hskp11_definition,axiom,
hskp11 ).
tff(declare_hskp12,type,
hskp12: $o ).
tff(hskp12_definition,axiom,
~ hskp12 ).
tff(declare_hskp13,type,
hskp13: $o ).
tff(hskp13_definition,axiom,
~ hskp13 ).
tff(declare_hskp14,type,
hskp14: $o ).
tff(hskp14_definition,axiom,
hskp14 ).
tff(declare_hskp15,type,
hskp15: $o ).
tff(hskp15_definition,axiom,
~ hskp15 ).
tff(declare_hskp16,type,
hskp16: $o ).
tff(hskp16_definition,axiom,
~ hskp16 ).
tff(declare_hskp17,type,
hskp17: $o ).
tff(hskp17_definition,axiom,
~ hskp17 ).
tff(declare_hskp18,type,
hskp18: $o ).
tff(hskp18_definition,axiom,
~ hskp18 ).
tff(declare_hskp19,type,
hskp19: $o ).
tff(hskp19_definition,axiom,
hskp19 ).
tff(declare_hskp20,type,
hskp20: $o ).
tff(hskp20_definition,axiom,
~ hskp20 ).
tff(declare_hskp21,type,
hskp21: $o ).
tff(hskp21_definition,axiom,
~ hskp21 ).
tff(declare_hskp22,type,
hskp22: $o ).
tff(hskp22_definition,axiom,
hskp22 ).
tff(declare_hskp23,type,
hskp23: $o ).
tff(hskp23_definition,axiom,
hskp23 ).
tff(declare_hskp24,type,
hskp24: $o ).
tff(hskp24_definition,axiom,
hskp24 ).
tff(declare_hskp25,type,
hskp25: $o ).
tff(hskp25_definition,axiom,
~ hskp25 ).
tff(declare_hskp26,type,
hskp26: $o ).
tff(hskp26_definition,axiom,
~ hskp26 ).
tff(declare_hskp27,type,
hskp27: $o ).
tff(hskp27_definition,axiom,
hskp27 ).
tff(declare_hskp28,type,
hskp28: $o ).
tff(hskp28_definition,axiom,
~ hskp28 ).
tff(declare_hskp29,type,
hskp29: $o ).
tff(hskp29_definition,axiom,
~ hskp29 ).
tff(declare_hskp30,type,
hskp30: $o ).
tff(hskp30_definition,axiom,
~ hskp30 ).
tff(declare_hskp31,type,
hskp31: $o ).
tff(hskp31_definition,axiom,
~ hskp31 ).
tff(declare_hskp32,type,
hskp32: $o ).
tff(hskp32_definition,axiom,
~ hskp32 ).
tff(declare_hskp33,type,
hskp33: $o ).
tff(hskp33_definition,axiom,
~ hskp33 ).
tff(declare_hskp34,type,
hskp34: $o ).
tff(hskp34_definition,axiom,
~ hskp34 ).
tff(declare_hskp35,type,
hskp35: $o ).
tff(hskp35_definition,axiom,
~ hskp35 ).
tff(declare_hskp36,type,
hskp36: $o ).
tff(hskp36_definition,axiom,
~ hskp36 ).
tff(declare_hskp37,type,
hskp37: $o ).
tff(hskp37_definition,axiom,
~ hskp37 ).
tff(declare_hskp38,type,
hskp38: $o ).
tff(hskp38_definition,axiom,
~ hskp38 ).
tff(declare_hskp39,type,
hskp39: $o ).
tff(hskp39_definition,axiom,
~ hskp39 ).
tff(declare_hskp40,type,
hskp40: $o ).
tff(hskp40_definition,axiom,
~ hskp40 ).
tff(declare_hskp41,type,
hskp41: $o ).
tff(hskp41_definition,axiom,
hskp41 ).
tff(declare_hskp42,type,
hskp42: $o ).
tff(hskp42_definition,axiom,
~ hskp42 ).
tff(declare_hskp43,type,
hskp43: $o ).
tff(hskp43_definition,axiom,
~ hskp43 ).
tff(declare_hskp44,type,
hskp44: $o ).
tff(hskp44_definition,axiom,
hskp44 ).
tff(declare_hskp45,type,
hskp45: $o ).
tff(hskp45_definition,axiom,
~ hskp45 ).
tff(declare_hskp46,type,
hskp46: $o ).
tff(hskp46_definition,axiom,
hskp46 ).
tff(declare_hskp47,type,
hskp47: $o ).
tff(hskp47_definition,axiom,
~ hskp47 ).
tff(declare_hskp48,type,
hskp48: $o ).
tff(hskp48_definition,axiom,
~ hskp48 ).
tff(declare_hskp49,type,
hskp49: $o ).
tff(hskp49_definition,axiom,
~ hskp49 ).
tff(declare_hskp50,type,
hskp50: $o ).
tff(hskp50_definition,axiom,
~ hskp50 ).
tff(declare_hskp51,type,
hskp51: $o ).
tff(hskp51_definition,axiom,
~ hskp51 ).
tff(declare_hskp52,type,
hskp52: $o ).
tff(hskp52_definition,axiom,
~ hskp52 ).
tff(declare_hskp53,type,
hskp53: $o ).
tff(hskp53_definition,axiom,
~ hskp53 ).
tff(declare_hskp54,type,
hskp54: $o ).
tff(hskp54_definition,axiom,
~ hskp54 ).
tff(declare_hskp55,type,
hskp55: $o ).
tff(hskp55_definition,axiom,
~ hskp55 ).
tff(declare_hskp56,type,
hskp56: $o ).
tff(hskp56_definition,axiom,
hskp56 ).
tff(declare_hskp57,type,
hskp57: $o ).
tff(hskp57_definition,axiom,
~ hskp57 ).
tff(declare_hskp58,type,
hskp58: $o ).
tff(hskp58_definition,axiom,
~ hskp58 ).
tff(declare_hskp59,type,
hskp59: $o ).
tff(hskp59_definition,axiom,
~ hskp59 ).
tff(declare_hskp60,type,
hskp60: $o ).
tff(hskp60_definition,axiom,
~ hskp60 ).
tff(declare_hskp61,type,
hskp61: $o ).
tff(hskp61_definition,axiom,
~ hskp61 ).
tff(declare_hskp62,type,
hskp62: $o ).
tff(hskp62_definition,axiom,
~ hskp62 ).
tff(declare_hskp63,type,
hskp63: $o ).
tff(hskp63_definition,axiom,
hskp63 ).
tff(declare_hskp64,type,
hskp64: $o ).
tff(hskp64_definition,axiom,
~ hskp64 ).
tff(declare_hskp65,type,
hskp65: $o ).
tff(hskp65_definition,axiom,
~ hskp65 ).
tff(declare_hskp66,type,
hskp66: $o ).
tff(hskp66_definition,axiom,
hskp66 ).
tff(declare_hskp67,type,
hskp67: $o ).
tff(hskp67_definition,axiom,
hskp67 ).
tff(declare_hskp68,type,
hskp68: $o ).
tff(hskp68_definition,axiom,
~ hskp68 ).
tff(declare_hskp69,type,
hskp69: $o ).
tff(hskp69_definition,axiom,
~ hskp69 ).
tff(declare_hskp70,type,
hskp70: $o ).
tff(hskp70_definition,axiom,
~ hskp70 ).
tff(declare_hskp71,type,
hskp71: $o ).
tff(hskp71_definition,axiom,
hskp71 ).
tff(declare_hskp72,type,
hskp72: $o ).
tff(hskp72_definition,axiom,
hskp72 ).
tff(declare_hskp73,type,
hskp73: $o ).
tff(hskp73_definition,axiom,
~ hskp73 ).
tff(declare_hskp74,type,
hskp74: $o ).
tff(hskp74_definition,axiom,
~ hskp74 ).
tff(declare_hskp75,type,
hskp75: $o ).
tff(hskp75_definition,axiom,
~ hskp75 ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
( ~ c1_1('fmb_$i_1')
& c1_1('fmb_$i_2')
& ~ c1_1('fmb_$i_3')
& ~ c1_1('fmb_$i_4') ) ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
( c2_1('fmb_$i_1')
& ~ c2_1('fmb_$i_2')
& ~ c2_1('fmb_$i_3')
& ~ c2_1('fmb_$i_4') ) ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
( c3_1('fmb_$i_1')
& c3_1('fmb_$i_2')
& c3_1('fmb_$i_3')
& ~ c3_1('fmb_$i_4') ) ).
tff(declare_c0_1,type,
c0_1: $i > $o ).
tff(predicate_c0_1,axiom,
( ~ c0_1('fmb_$i_1')
& ~ c0_1('fmb_$i_2')
& c0_1('fmb_$i_3')
& c0_1('fmb_$i_4') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN441+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n001.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 16:07:04 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 Running first-order model finding
% 0.10/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.31 % (460232)Will run a generic schedule for satisfiability detection.
% 0.30/0.31 % (460237)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1467175598_2999 on theBenchmark for (2999ds/0Mi)
% 0.30/0.31 % (460238)% WARNING: option uhcvi not known.
% 0.30/0.31 % Detected minimum model sizes of [1]
% 0.30/0.31 % Detected maximum model sizes of [76]
% 0.30/0.31 % TRYING [1]
% 0.30/0.31 % TRYING [2]
% 0.30/0.31 % (460240)dis+10_1_sil=32000:sp=arity:random_seed=3341667148:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.30/0.31 % (460238)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3887904782:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.30/0.31 % (460242)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1842829010:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.30/0.31 % (460239)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3776725692:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.30/0.31 % (460241)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3501435588:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.30/0.31 % (460243)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=458994352:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.30/0.31 % TRYING [3]
% 0.30/0.31 % TRYING [4]
% 0.30/0.31 % Finite Model Found!
% 0.30/0.31 % SZS status CounterSatisfiable for theBenchmark
% 0.30/0.31 % (460237) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-460232-460237"...
% 0.30/0.31 % (460237)...printing done.
% 0.30/0.31 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.30/0.31 % (460237)------------------------------
% 0.30/0.31 % (460237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.30/0.31 % (460237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/0.31 % (460237)CaDiCaL version: 2.1.3
% 0.30/0.31 % (460237)Termination reason: Satisfiable
% 0.30/0.31 % (460237)Time elapsed: 0.042 s
% 0.30/0.31 % (460237)Peak memory usage: 12 MB
% 0.30/0.31 % (460237)Instructions burned: 132 (million)
% 0.30/0.31 % (460232)Success in time 0.072 s
% 0.30/0.31 % Vampire exiting
%------------------------------------------------------------------------------