%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n003.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 01:50:36 PM UTC 2026
% Result : CounterSatisfiable 8.28s 2.05s
% Output : Saturation 8.28s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u3421,negated_conjecture,
~ sP0 ).
cnf(u1217,negated_conjecture,
~ c6_1(a2030) ).
cnf(u1376,negated_conjecture,
~ c3_0 ).
cnf(u1224,negated_conjecture,
~ c7_1(a2030) ).
cnf(u1641,negated_conjecture,
~ c4_0 ).
cnf(u1231,negated_conjecture,
~ ndr1_1(a2029) ).
cnf(u1242,negated_conjecture,
c10_1(a2029) ).
cnf(u1246,negated_conjecture,
ndr1_0 ).
cnf(u1593,negated_conjecture,
~ c8_0 ).
cnf(u1257,negated_conjecture,
~ c6_1(a2027) ).
cnf(u1273,negated_conjecture,
~ c4_1(a2027) ).
cnf(u1280,negated_conjecture,
c3_1(a2027) ).
cnf(u1393,negated_conjecture,
~ c6_0 ).
cnf(u1341,negated_conjecture,
c7_0 ).
cnf(u1293,negated_conjecture,
( ~ c5_1(X187)
| c3_2(X187,a2026)
| c4_1(X187) ) ).
cnf(u1297,negated_conjecture,
( ~ c5_1(X187)
| c4_2(X187,a2026)
| c4_1(X187) ) ).
cnf(u1301,negated_conjecture,
( ~ c5_1(X187)
| ~ c10_2(X187,a2026)
| c4_1(X187) ) ).
cnf(u1305,negated_conjecture,
( ~ c5_1(X187)
| ndr1_1(X187)
| c4_1(X187) ) ).
cnf(u1309,negated_conjecture,
( ~ c8_2(X185,X186)
| c3_2(X185,a2025)
| ~ ndr1_1(X185)
| c3_2(X185,X186)
| c2_2(X185,X186)
| c10_1(X185) ) ).
cnf(u1316,negated_conjecture,
( ~ c6_2(X185,a2025)
| c10_1(X185)
| ~ ndr1_1(X185)
| c3_2(X185,X186)
| c2_2(X185,X186)
| ~ c8_2(X185,X186) ) ).
cnf(u1320,negated_conjecture,
( ~ c5_2(X185,a2025)
| c10_1(X185)
| ~ ndr1_1(X185)
| c3_2(X185,X186)
| c2_2(X185,X186)
| ~ c8_2(X185,X186) ) ).
cnf(u1336,negated_conjecture,
~ c1_0 ).
cnf(u1340,negated_conjecture,
c9_0 ).
cnf(u1345,negated_conjecture,
( ~ c7_1(X181)
| ~ c5_1(X181)
| ~ ndr1_1(X181)
| c4_2(X181,X182)
| c3_2(X181,X182)
| c5_2(X181,X182) ) ).
cnf(u1369,negated_conjecture,
~ c10_0 ).
cnf(u1379,negated_conjecture,
~ c1_1(a2021) ).
cnf(u1387,negated_conjecture,
~ c3_1(a2021) ).
cnf(u1397,negated_conjecture,
( ~ c9_1(X177)
| ~ c3_1(X177)
| ~ c10_1(X177) ) ).
cnf(u1424,negated_conjecture,
~ c2_0 ).
cnf(u1428,negated_conjecture,
( ~ c4_2(X173,a2018)
| c10_1(X173)
| c8_1(X173) ) ).
cnf(u1433,negated_conjecture,
( ~ c10_2(X173,a2018)
| c10_1(X173)
| c8_1(X173) ) ).
cnf(u1437,negated_conjecture,
( c6_2(X173,a2018)
| c10_1(X173)
| c8_1(X173) ) ).
cnf(u1441,negated_conjecture,
( c8_1(X173)
| c10_1(X173)
| ndr1_1(X173) ) ).
cnf(u1445,negated_conjecture,
~ ndr1_1(a2017) ).
cnf(u1452,negated_conjecture,
c3_1(a2017) ).
cnf(u1456,negated_conjecture,
c8_1(a2017) ).
cnf(u3450,negated_conjecture,
~ sP1 ).
cnf(u1465,negated_conjecture,
~ ndr1_1(a2014) ).
cnf(u1472,negated_conjecture,
c2_1(a2014) ).
cnf(u1476,negated_conjecture,
~ c7_1(a2014) ).
cnf(u3469,negated_conjecture,
~ sP2 ).
cnf(u1569,negated_conjecture,
ndr1_1(a2006) ).
cnf(u1551,negated_conjecture,
( c9_2(a2006,X158)
| c7_2(a2006,X158) ) ).
cnf(u1555,negated_conjecture,
c4_1(a2006) ).
cnf(u1559,negated_conjecture,
~ c2_2(a2006,a2007) ).
cnf(u1563,negated_conjecture,
c7_2(a2006,a2007) ).
cnf(u1567,negated_conjecture,
c4_2(a2006,a2007) ).
cnf(u1596,negated_conjecture,
c3_1(a2003) ).
cnf(u1600,negated_conjecture,
~ ndr1_1(a2003) ).
cnf(u1612,negated_conjecture,
~ c5_0 ).
cnf(u3510,negated_conjecture,
~ sP3 ).
cnf(u3545,negated_conjecture,
~ sP4 ).
cnf(u1656,negated_conjecture,
( ~ c10_1(X154)
| c9_2(X154,a1994)
| c4_1(X154) ) ).
cnf(u1660,negated_conjecture,
( ~ c10_2(X154,a1994)
| ~ c10_1(X154)
| c4_1(X154) ) ).
cnf(u1664,negated_conjecture,
( ~ c10_1(X154)
| ndr1_1(X154)
| c4_1(X154) ) ).
cnf(u3571,negated_conjecture,
~ sP5 ).
cnf(u1715,negated_conjecture,
( c5_2(X150,X151)
| ~ ndr1_1(X150)
| c10_2(X150,X151)
| c9_1(X150)
| ~ c8_2(X150,X151)
| ~ c8_1(X150) ) ).
cnf(u3647,negated_conjecture,
~ sP7 ).
cnf(u3609,negated_conjecture,
~ sP6 ).
cnf(u1752,negated_conjecture,
( ~ c5_1(X146)
| c1_2(X146,a1983)
| ~ c2_1(X146) ) ).
cnf(u1756,negated_conjecture,
( c8_2(X146,a1983)
| ~ c2_1(X146)
| ~ c5_1(X146) ) ).
cnf(u1760,negated_conjecture,
( ~ c5_1(X146)
| ~ c5_2(X146,a1983)
| ~ c2_1(X146) ) ).
cnf(u1764,negated_conjecture,
( ~ c5_1(X146)
| ndr1_1(X146)
| ~ c2_1(X146) ) ).
cnf(u3672,negated_conjecture,
~ sP8 ).
cnf(u1789,negated_conjecture,
~ ndr1_1(a1979) ).
cnf(u1796,negated_conjecture,
c9_1(a1979) ).
cnf(u1800,negated_conjecture,
c1_1(a1979) ).
cnf(u1807,negated_conjecture,
( ~ c2_2(X139,X140)
| ~ c8_2(X139,X141)
| ~ c7_2(X139,X141)
| ~ c3_2(X139,X141)
| c3_1(X139)
| ~ ndr1_1(X139)
| ~ c3_2(X139,X140)
| ~ c1_2(X139,X140) ) ).
cnf(u3713,negated_conjecture,
~ sP9 ).
cnf(u1840,negated_conjecture,
( ~ c10_1(X133)
| ~ c7_2(X133,a1974)
| ~ c6_1(X133) ) ).
cnf(u3738,negated_conjecture,
~ sP10 ).
cnf(u1847,negated_conjecture,
( ~ c2_2(X133,a1974)
| ~ c10_1(X133)
| ~ c6_1(X133) ) ).
cnf(u1851,negated_conjecture,
( ~ c10_1(X133)
| ~ c1_2(X133,a1974)
| ~ c6_1(X133) ) ).
cnf(u1855,negated_conjecture,
( ~ c6_1(X133)
| ~ c10_1(X133)
| ndr1_1(X133) ) ).
cnf(u1875,negated_conjecture,
( ~ c6_2(X130,X131)
| ~ ndr1_1(X130)
| ~ c3_2(X130,X131)
| c7_1(X130) ) ).
cnf(u1912,negated_conjecture,
~ ndr1_1(a1967) ).
cnf(u1961,negated_conjecture,
~ ndr1_1(a1963) ).
cnf(u1975,negated_conjecture,
c5_1(a1963) ).
cnf(u1997,negated_conjecture,
( ~ c6_1(X117)
| c1_1(X117)
| ~ ndr1_1(X117)
| c8_2(X117,X118)
| c1_2(X117,X118)
| c9_2(X117,X118) ) ).
cnf(u2020,negated_conjecture,
~ c5_1(a1958) ).
cnf(u2024,negated_conjecture,
~ c9_1(a1958) ).
cnf(u2028,negated_conjecture,
c8_2(a1958,a1959) ).
cnf(u2032,negated_conjecture,
~ c7_2(a1958,a1959) ).
cnf(u2036,negated_conjecture,
c4_2(a1958,a1959) ).
cnf(u2040,negated_conjecture,
ndr1_1(a1958) ).
cnf(u3768,negated_conjecture,
~ sP11 ).
cnf(u2048,negated_conjecture,
( ~ c1_2(X116,a1955)
| ~ c7_1(X116)
| ~ c10_1(X116) ) ).
cnf(u2052,negated_conjecture,
( c3_2(X116,a1955)
| ~ c7_1(X116)
| ~ c10_1(X116) ) ).
cnf(u2056,negated_conjecture,
( ~ c7_1(X116)
| ~ c10_1(X116)
| c5_2(X116,a1955) ) ).
cnf(u2060,negated_conjecture,
( ~ c7_1(X116)
| ~ c10_1(X116)
| ndr1_1(X116) ) ).
cnf(u2064,negated_conjecture,
( ~ c6_2(X114,a1953)
| c5_2(X114,a1954)
| c1_2(X114,X115)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| ~ c5_2(X114,X115) ) ).
cnf(u2068,negated_conjecture,
( ~ c6_2(X114,a1953)
| c10_2(X114,a1954)
| c1_2(X114,X115)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| ~ c5_2(X114,X115) ) ).
cnf(u2072,negated_conjecture,
( ~ c6_2(X114,a1953)
| c3_2(X114,a1954)
| c1_2(X114,X115)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| ~ c5_2(X114,X115) ) ).
cnf(u2076,negated_conjecture,
( ~ c5_2(X114,X115)
| c5_2(X114,a1954)
| c10_2(X114,a1953)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| c1_2(X114,X115) ) ).
cnf(u2080,negated_conjecture,
( ~ c5_2(X114,X115)
| c10_2(X114,a1954)
| c10_2(X114,a1953)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| c1_2(X114,X115) ) ).
cnf(u2084,negated_conjecture,
( ~ c5_2(X114,X115)
| c3_2(X114,a1954)
| c10_2(X114,a1953)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| c1_2(X114,X115) ) ).
cnf(u2088,negated_conjecture,
( ~ c5_2(X114,X115)
| c5_2(X114,a1954)
| c4_2(X114,a1953)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| c1_2(X114,X115) ) ).
cnf(u2092,negated_conjecture,
( ~ c5_2(X114,X115)
| c10_2(X114,a1954)
| c4_2(X114,a1953)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| c1_2(X114,X115) ) ).
cnf(u2096,negated_conjecture,
( ~ c5_2(X114,X115)
| c3_2(X114,a1954)
| c4_2(X114,a1953)
| ~ ndr1_1(X114)
| ~ c7_2(X114,X115)
| c1_2(X114,X115) ) ).
cnf(u2118,negated_conjecture,
c5_1(a1951) ).
cnf(u3809,negated_conjecture,
~ sP12 ).
cnf(u2128,negated_conjecture,
~ c3_1(a1951) ).
cnf(u3825,negated_conjecture,
~ sP13 ).
cnf(u2161,negated_conjecture,
~ c4_1(a1945) ).
cnf(u3863,negated_conjecture,
~ sP14 ).
cnf(u2168,negated_conjecture,
~ ndr1_1(a1945) ).
cnf(u2179,negated_conjecture,
( ~ c9_1(X100)
| ~ c9_2(X100,X101)
| ~ c1_2(X100,X102)
| c10_2(X100,X102)
| ~ ndr1_1(X100)
| c2_2(X100,X101)
| c8_2(X100,X101) ) ).
cnf(u2183,negated_conjecture,
( ~ c10_1(X99)
| c2_1(X99)
| ~ c3_1(X99) ) ).
cnf(u2202,negated_conjecture,
~ c9_1(a1941) ).
cnf(u2206,negated_conjecture,
~ c1_1(a1941) ).
cnf(u2211,negated_conjecture,
( ~ c6_1(X97)
| c8_2(X97,a1940)
| c3_1(X97) ) ).
cnf(u2221,negated_conjecture,
( ~ c6_1(X97)
| ~ c6_2(X97,a1940)
| c3_1(X97) ) ).
cnf(u2225,negated_conjecture,
( ~ c6_1(X97)
| ndr1_1(X97)
| c3_1(X97) ) ).
cnf(u2241,negated_conjecture,
~ c10_1(a1937) ).
cnf(u2245,negated_conjecture,
~ c6_2(a1937,a1938) ).
cnf(u2249,negated_conjecture,
~ c7_2(a1937,a1938) ).
cnf(u2253,negated_conjecture,
ndr1_1(a1937) ).
cnf(u2257,negated_conjecture,
c2_1(a1937) ).
cnf(u2262,negated_conjecture,
( ~ c6_1(X95)
| ~ c10_1(X95) ) ).
cnf(u2311,negated_conjecture,
( ~ c4_1(X92)
| c9_1(X92)
| ~ ndr1_1(X92)
| ~ c8_2(X92,X93)
| c10_2(X92,X93)
| ~ c1_2(X92,X93) ) ).
cnf(u3888,negated_conjecture,
~ sP15 ).
cnf(u2324,negated_conjecture,
( c7_2(X87,a1930)
| c10_1(X87)
| c3_1(X87) ) ).
cnf(u2327,negated_conjecture,
( ~ c5_1(X86)
| ~ c2_1(X86)
| ~ c3_2(X86,a1929) ) ).
cnf(u2331,negated_conjecture,
( c8_2(X87,a1930)
| c10_1(X87)
| c3_1(X87) ) ).
cnf(u2335,negated_conjecture,
( ~ c6_2(X87,a1930)
| c10_1(X87)
| c3_1(X87) ) ).
cnf(u2343,negated_conjecture,
( c8_2(X86,a1929)
| ~ c2_1(X86)
| ~ c5_1(X86) ) ).
cnf(u2350,negated_conjecture,
( ~ c5_1(X86)
| ~ c2_1(X86)
| ~ c9_2(X86,a1929) ) ).
cnf(u2364,negated_conjecture,
~ ndr1_1(a1928) ).
cnf(u2375,negated_conjecture,
( ~ c9_2(X82,a1927)
| c2_1(X82)
| ~ c1_1(X82) ) ).
cnf(u2379,negated_conjecture,
( ~ c1_1(X82)
| c2_1(X82)
| c1_2(X82,a1927) ) ).
cnf(u2383,negated_conjecture,
( ~ c1_1(X82)
| c2_1(X82)
| ndr1_1(X82) ) ).
cnf(u2407,negated_conjecture,
~ ndr1_1(a1924) ).
cnf(u2426,negated_conjecture,
~ c5_1(a1924) ).
cnf(u2440,negated_conjecture,
~ c7_2(a1922,a1923) ).
cnf(u2444,negated_conjecture,
c8_2(a1922,a1923) ).
cnf(u2448,negated_conjecture,
~ c3_2(a1922,a1923) ).
cnf(u2452,negated_conjecture,
ndr1_1(a1922) ).
cnf(u2456,negated_conjecture,
c8_1(a1922) ).
cnf(u2461,negated_conjecture,
( ~ c2_2(a1922,X75)
| ~ c5_2(a1922,X75)
| ~ c10_2(a1922,X75) ) ).
cnf(u3914,negated_conjecture,
~ sP16 ).
cnf(u2510,negated_conjecture,
( ~ c10_2(X69,X71)
| ~ c7_2(X69,X71)
| c2_2(X69,X71)
| c9_2(X69,X70)
| c8_1(X69)
| ~ ndr1_1(X69)
| c10_2(X69,X70)
| ~ c1_2(X69,X70) ) ).
cnf(u2527,negated_conjecture,
ndr1_1(a1915) ).
cnf(u2517,negated_conjecture,
( c7_2(a1915,X68)
| c1_2(a1915,X68) ) ).
cnf(u2521,negated_conjecture,
~ c9_2(a1915,a1916) ).
cnf(u2525,negated_conjecture,
c5_2(a1915,a1916) ).
cnf(u2531,negated_conjecture,
c5_1(a1915) ).
cnf(u2539,negated_conjecture,
~ ndr1_1(a1913) ).
cnf(u2554,negated_conjecture,
~ c2_1(a1913) ).
cnf(u2562,negated_conjecture,
c3_1(a1912) ).
cnf(u3940,negated_conjecture,
~ sP17 ).
cnf(u2569,negated_conjecture,
~ ndr1_1(a1912) ).
cnf(u2576,negated_conjecture,
~ c5_1(a1912) ).
cnf(u2582,negated_conjecture,
( ~ c8_2(X64,a1909)
| ~ c8_1(X64)
| ~ ndr1_1(X64)
| c10_2(X64,X65)
| c3_2(X64,X65)
| c4_2(X64,X65) ) ).
cnf(u2585,negated_conjecture,
( c3_2(X63,a1908)
| c10_1(X63)
| c7_1(X63) ) ).
cnf(u2597,negated_conjecture,
( c1_2(X63,a1908)
| c10_1(X63)
| c7_1(X63) ) ).
cnf(u2603,negated_conjecture,
( c9_2(X63,a1908)
| c10_1(X63)
| c7_1(X63) ) ).
cnf(u2609,negated_conjecture,
( c7_1(X63)
| ndr1_1(X63)
| c10_1(X63) ) ).
cnf(u2646,negated_conjecture,
~ ndr1_1(a1906) ).
cnf(u3963,negated_conjecture,
~ sP18 ).
cnf(u2662,negated_conjecture,
c4_1(a1906) ).
cnf(u2682,negated_conjecture,
~ c6_1(a1900) ).
cnf(u2686,negated_conjecture,
c2_2(a1900,a1902) ).
cnf(u2690,negated_conjecture,
c9_2(a1900,a1902) ).
cnf(u2694,negated_conjecture,
~ c10_2(a1900,a1902) ).
cnf(u2698,negated_conjecture,
ndr1_1(a1900) ).
cnf(u2702,negated_conjecture,
~ c2_2(a1900,a1901) ).
cnf(u2706,negated_conjecture,
~ c10_2(a1900,a1901) ).
cnf(u2710,negated_conjecture,
~ c4_2(a1900,a1901) ).
cnf(u2717,negated_conjecture,
~ ndr1_1(a1899) ).
cnf(u2727,negated_conjecture,
~ c1_1(a1899) ).
cnf(u2731,negated_conjecture,
~ c9_1(a1899) ).
cnf(u2750,negated_conjecture,
( ~ c9_1(X44)
| ~ ndr1_1(X44)
| c2_2(X44,X45)
| c8_2(X44,X45)
| c1_1(X44) ) ).
cnf(u4004,negated_conjecture,
~ sP19 ).
cnf(u4030,negated_conjecture,
~ sP20 ).
cnf(u4071,negated_conjecture,
~ sP21 ).
cnf(u2972,negated_conjecture,
~ c5_1(a1876) ).
cnf(u2979,negated_conjecture,
~ c2_1(a1876) ).
cnf(u2997,negated_conjecture,
( c1_2(X25,a1874)
| c2_1(X25)
| c6_1(X25) ) ).
cnf(u4097,negated_conjecture,
~ sP22 ).
cnf(u3007,negated_conjecture,
( c10_2(X25,a1874)
| c2_1(X25)
| c6_1(X25) ) ).
cnf(u3011,negated_conjecture,
( ~ c2_2(X25,a1874)
| c2_1(X25)
| c6_1(X25) ) ).
cnf(u3015,negated_conjecture,
( c2_1(X25)
| ndr1_1(X25)
| c6_1(X25) ) ).
cnf(u3040,negated_conjecture,
( c4_2(X22,X23)
| ~ ndr1_1(X22)
| c10_1(X22)
| c10_2(X22,X23)
| c1_2(X22,X23)
| c4_1(X22) ) ).
cnf(u3065,negated_conjecture,
~ c6_2(a1865,a1868) ).
cnf(u4115,negated_conjecture,
~ sP23 ).
cnf(u3072,negated_conjecture,
~ c7_2(a1865,a1868) ).
cnf(u3076,negated_conjecture,
c2_2(a1865,a1868) ).
cnf(u3080,negated_conjecture,
ndr1_1(a1865) ).
cnf(u3084,negated_conjecture,
~ c5_2(a1865,a1867) ).
cnf(u3088,negated_conjecture,
~ c9_2(a1865,a1867) ).
cnf(u3092,negated_conjecture,
c3_2(a1865,a1867) ).
cnf(u3097,negated_conjecture,
~ c4_2(a1865,a1866) ).
cnf(u3101,negated_conjecture,
c8_2(a1865,a1866) ).
cnf(u3105,negated_conjecture,
~ c7_2(a1865,a1866) ).
cnf(u3148,negated_conjecture,
( ~ c7_1(X19)
| ~ ndr1_1(X19)
| c3_2(X19,X20)
| ~ c7_2(X19,X20)
| c9_2(X19,X20)
| c8_1(X19) ) ).
cnf(u4153,negated_conjecture,
~ sP24 ).
cnf(u3202,negated_conjecture,
c1_1(a1853) ).
cnf(u3209,negated_conjecture,
( c6_2(a1853,X17)
| c10_2(a1853,X17)
| c3_2(a1853,X17) ) ).
cnf(u3213,negated_conjecture,
~ c2_1(a1853) ).
cnf(u3237,negated_conjecture,
ndr1_1(a1851) ).
cnf(u3223,negated_conjecture,
( c5_2(a1851,X16)
| ~ c8_2(a1851,X16)
| c4_2(a1851,X16) ) ).
cnf(u3227,negated_conjecture,
c3_2(a1851,a1852) ).
cnf(u3231,negated_conjecture,
~ c2_2(a1851,a1852) ).
cnf(u3235,negated_conjecture,
~ c4_2(a1851,a1852) ).
cnf(u3241,negated_conjecture,
( ~ c4_2(a1851,X15)
| ~ c7_2(a1851,X15) ) ).
cnf(u4191,negated_conjecture,
~ sP25 ).
cnf(u4217,negated_conjecture,
~ sP26 ).
cnf(u3272,negated_conjecture,
~ ndr1_1(a1845) ).
cnf(u3279,negated_conjecture,
~ c10_1(a1845) ).
cnf(u3283,negated_conjecture,
c1_1(a1845) ).
cnf(u3288,negated_conjecture,
( ~ c9_1(X9)
| ~ ndr1_1(X9)
| ~ c1_2(X9,X10)
| c2_2(X9,X10)
| ~ c4_2(X9,X10)
| ~ c3_1(X9) ) ).
cnf(u3327,negated_conjecture,
c2_2(a1841,a1842) ).
cnf(u4244,negated_conjecture,
~ sP27 ).
cnf(u3334,negated_conjecture,
c4_2(a1841,a1842) ).
cnf(u3338,negated_conjecture,
ndr1_1(a1841) ).
cnf(u3343,negated_conjecture,
( ~ c2_2(a1841,X6)
| ~ c7_2(a1841,X6) ) ).
cnf(u3348,negated_conjecture,
( ~ c1_2(X4,X5)
| ~ c10_1(X4)
| ~ c6_1(X4)
| ~ ndr1_1(X4)
| ~ c7_2(X4,X5) ) ).
cnf(u4307,negated_conjecture,
~ c1_2(a1900,a1902) ).
cnf(u5100,negated_conjecture,
~ c3_1(a1900) ).
cnf(u4323,negated_conjecture,
~ c1_2(a1841,a1842) ).
cnf(u4923,negated_conjecture,
~ c3_1(a1841) ).
cnf(u4342,negated_conjecture,
c10_1(a1958) ).
cnf(u5316,negated_conjecture,
~ c10_1(a1922) ).
cnf(u4359,negated_conjecture,
c2_2(a1922,a1923) ).
cnf(u4368,negated_conjecture,
c10_1(a1865) ).
cnf(u4386,negated_conjecture,
~ c3_1(a2029) ).
cnf(u4393,negated_conjecture,
~ c6_1(a2029) ).
cnf(u4400,negated_conjecture,
c4_1(a2029) ).
cnf(u4430,negated_conjecture,
c4_2(a1851,a1953) ).
cnf(u4437,negated_conjecture,
c1_2(a1915,a1916) ).
cnf(u4458,negated_conjecture,
c10_1(a1853) ).
cnf(u4480,negated_conjecture,
c10_2(a1851,a1953) ).
cnf(u4489,negated_conjecture,
c2_1(a1979) ).
cnf(u4501,negated_conjecture,
c4_1(a1851) ).
cnf(u4516,negated_conjecture,
ndr1_1(a2030) ).
cnf(u4523,negated_conjecture,
~ ndr1_1(a2027) ).
cnf(u4536,negated_conjecture,
~ c10_1(a1979) ).
cnf(u4548,negated_conjecture,
c2_1(a1845) ).
cnf(u4568,negated_conjecture,
~ c2_1(a1915) ).
cnf(u4584,negated_conjecture,
c4_1(a1915) ).
cnf(u4604,negated_conjecture,
~ c1_1(a2006) ).
cnf(u4623,negated_conjecture,
~ c2_1(a1963) ).
cnf(u4641,negated_conjecture,
c4_1(a1963) ).
cnf(u4665,negated_conjecture,
~ c8_2(a1851,a2025) ).
cnf(u4675,negated_conjecture,
~ c1_2(a1865,a1868) ).
cnf(u5057,negated_conjecture,
~ c3_1(a1865) ).
cnf(u4700,negated_conjecture,
~ c2_1(a1951) ).
cnf(u4708,negated_conjecture,
ndr1_1(a1951) ).
cnf(u4720,negated_conjecture,
c4_1(a1951) ).
cnf(u4741,negated_conjecture,
c9_1(a1951) ).
cnf(u4768,negated_conjecture,
~ c6_1(a1853) ).
cnf(u4775,negated_conjecture,
c4_1(a1853) ).
cnf(u4796,negated_conjecture,
c9_1(a1915) ).
cnf(u4805,negated_conjecture,
~ c10_2(a1922,a1923) ).
cnf(u4821,negated_conjecture,
c10_1(a1900) ).
cnf(u4830,negated_conjecture,
( ~ c1_2(a1851,X0)
| ~ c8_2(a1851,X0)
| c10_2(a1851,X0) ) ).
cnf(u4845,negated_conjecture,
~ c8_2(a1851,a1908) ).
cnf(u4852,negated_conjecture,
( ~ c1_2(a2006,X0)
| ~ c8_2(a2006,X0)
| c10_2(a2006,X0) ) ).
cnf(u4870,negated_conjecture,
~ c8_2(a2006,a1908) ).
cnf(u4878,negated_conjecture,
ndr1_1(a1876) ).
cnf(u4896,negated_conjecture,
~ c10_2(a1922,a1930) ).
cnf(u4902,negated_conjecture,
c3_1(a1922) ).
cnf(u4910,negated_conjecture,
c10_1(a1841) ).
cnf(u4930,negated_conjecture,
~ c6_1(a1841) ).
cnf(u4940,negated_conjecture,
c9_2(a1841,a1994) ).
cnf(u4967,negated_conjecture,
~ c10_1(a1915) ).
cnf(u4970,negated_conjecture,
~ c3_1(a1915) ).
cnf(u4976,negated_conjecture,
c1_1(a1915) ).
cnf(u4983,negated_conjecture,
( c10_2(a1915,X1)
| ~ c1_2(a1915,X1) ) ).
cnf(u4997,negated_conjecture,
~ c1_2(a1915,a2018) ).
cnf(u5008,negated_conjecture,
( ~ c8_2(a1853,X0)
| ~ c1_2(a1853,X0)
| c10_2(a1853,X0) ) ).
cnf(u5023,negated_conjecture,
~ c3_1(a1958) ).
cnf(u5030,negated_conjecture,
~ c6_1(a1958) ).
cnf(u5037,negated_conjecture,
c4_1(a1958) ).
cnf(u5064,negated_conjecture,
~ c6_1(a1865) ).
cnf(u5071,negated_conjecture,
c4_1(a1865) ).
cnf(u5084,negated_conjecture,
( ~ c1_2(a1865,X0)
| ~ c8_2(a1865,X0)
| c10_2(a1865,X0) ) ).
cnf(u5107,negated_conjecture,
c9_2(a1900,a1994) ).
cnf(u5133,negated_conjecture,
c3_1(a1963) ).
cnf(u5162,negated_conjecture,
~ c8_1(a1865) ).
cnf(u5180,negated_conjecture,
~ c6_1(a2014) ).
cnf(u5187,negated_conjecture,
c4_1(a2014) ).
cnf(u5217,negated_conjecture,
c1_1(a1951) ).
cnf(u5224,negated_conjecture,
( c10_2(a1951,X1)
| ~ c1_2(a1951,X1) ) ).
cnf(u5240,negated_conjecture,
~ c1_2(a1951,a2018) ).
cnf(u5257,negated_conjecture,
c3_1(a1913) ).
cnf(u5278,negated_conjecture,
c3_2(a1922,a1954) ).
cnf(u5287,negated_conjecture,
c10_2(a1922,a1953) ).
cnf(u5299,negated_conjecture,
c10_2(a1922,a1954) ).
cnf(u5354,negated_conjecture,
~ c6_1(a1922) ).
cnf(u5385,negated_conjecture,
c10_2(a1922,a1908) ).
cnf(u5468,negated_conjecture,
c4_2(a1922,a1953) ).
cnf(u4420,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,a1953)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| c9_1(X0)
| ~ c8_2(X0,X1)
| c3_2(X0,a1954) ) ).
cnf(u4469,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,a1953)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| c9_1(X0)
| ~ c8_2(X0,X1)
| c10_2(X0,a1954) ) ).
cnf(u84,axiom,
( ~ sP28(X0)
| c6_2(X0,a1836) ) ).
cnf(u5251,negated_conjecture,
~ c10_1(a1913) ).
cnf(u4765,negated_conjecture,
~ c3_1(a1853) ).
cnf(u5123,negated_conjecture,
c6_1(a1963) ).
cnf(u4746,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a2025)
| c2_2(X0,a1929)
| c10_1(X0) ) ).
cnf(u4750,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,a1953)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| c9_1(X0)
| ~ c8_2(X0,X1)
| c5_2(X0,a1954) ) ).
cnf(u4416,negated_conjecture,
( ~ c7_2(X0,a1874)
| c9_2(X0,X1)
| c8_1(X0)
| c10_2(X0,X1)
| ~ c1_2(X0,X1)
| c2_1(X0)
| c6_1(X0) ) ).
cnf(u5001,negated_conjecture,
c1_2(a1915,a1927) ).
cnf(u4881,negated_conjecture,
~ c7_2(a1851,a1953) ).
cnf(u5247,negated_conjecture,
c6_1(a1913) ).
cnf(u5172,negated_conjecture,
c10_1(a2014) ).
cnf(u4302,negated_conjecture,
( ~ c3_2(X0,a2018)
| c7_1(X0)
| c10_1(X0)
| c8_1(X0) ) ).
cnf(u4318,negated_conjecture,
~ c7_2(a1841,a1842) ).
cnf(u5048,negated_conjecture,
( ~ c1_2(a1958,X0)
| c10_2(a1958,X0)
| ~ c8_2(a1958,X0) ) ).
cnf(u4755,negated_conjecture,
( ~ c8_1(X0)
| c10_2(X0,a1953)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| c9_1(X0)
| ~ c8_2(X0,X1)
| c5_2(X0,a1954) ) ).
cnf(u86,axiom,
( ~ sP28(X0)
| c1_2(X0,a1836) ) ).
cnf(u4658,negated_conjecture,
( ~ c8_2(X0,a2025)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c8_2(X0,X1)
| c10_2(X0,a2025)
| c9_1(X0)
| c10_1(X0)
| ~ c8_1(X0) ) ).
cnf(u5245,negated_conjecture,
c1_2(a1951,a1927) ).
cnf(u4509,negated_conjecture,
( c1_2(X0,a2018)
| c10_1(X0)
| c4_1(X0)
| c8_1(X0) ) ).
cnf(u4337,negated_conjecture,
( c2_2(X0,a1930)
| ~ ndr1_1(X0)
| c3_2(X0,a1930)
| c3_2(X0,a2025)
| c10_1(X0)
| c3_1(X0) ) ).
cnf(u4448,negated_conjecture,
ndr1_1(a1853) ).
cnf(u4825,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a2025)
| c3_2(X0,a1983)
| c2_2(X0,a1983)
| c10_1(X0) ) ).
cnf(u4474,negated_conjecture,
( ~ c8_1(X0)
| c10_2(X0,a1953)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| c9_1(X0)
| ~ c8_2(X0,X1)
| c3_2(X0,a1954) ) ).
cnf(u4447,negated_conjecture,
c1_2(a1853,a1927) ).
cnf(u4531,negated_conjecture,
( ~ c8_1(X0)
| c10_2(X0,a1953)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| c9_1(X0)
| ~ c8_2(X0,X1)
| c10_2(X0,a1954) ) ).
cnf(u85,axiom,
( ~ sP28(X0)
| ~ c4_2(X0,a1836) ) ).
cnf(u87,axiom,
( ~ sP28(X0)
| ndr1_1(X0) ) ).
cnf(u5127,negated_conjecture,
~ c10_1(a1963) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN428+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 % Computer : n003.cluster.edu
% 0.08/0.25 % Model : x86_64 x86_64
% 0.08/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.25 % Memory : 8046.5625MB
% 0.08/0.25 % OS : Linux 6.8.0-71-generic
% 0.08/0.25 % CPULimit : 300
% 0.08/0.25 % WCLimit : 300
% 0.08/0.25 % DateTime : Mon Sep 28 16:00:57 UTC 2026
% 0.08/0.25 % CPUTime :
% 0.08/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.28 Running first-order theorem proving
% 0.17/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.28/2.05 % (1720496)Detected formulas, will run a generic FOF schedule.
% 8.28/2.05 % (1720507)dis-21_1_sil=8000:lcm=predicate:random_seed=50756019:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.28/2.05 % (1720507)Instruction limit reached!
% 8.28/2.05 % (1720507)------------------------------
% 8.28/2.05 % (1720507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720507)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720507)Termination reason: Instruction limit
% 8.28/2.05 % (1720507)Termination phase: Saturation
% 8.28/2.05 % (1720507)Time elapsed: 0.041 s
% 8.28/2.05 % (1720507)Peak memory usage: 92 MB
% 8.28/2.05 % (1720507)Instructions burned: 131 (million)
% 8.28/2.05 % (1720501)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=293308696:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.28/2.05 % (1720502)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4122390578:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.28/2.05 % (1720504)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=562879421:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.28/2.05 % (1720505)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1633541900:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.28/2.05 % (1720503)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1805242933:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.28/2.05 % (1720506)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1314472092:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.28/2.05 % (1720506)Refutation not found, incomplete strategy
% 8.28/2.05 % (1720506)------------------------------
% 8.28/2.05 % (1720506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720506)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720506)Termination reason: Refutation not found, incomplete strategy
% 8.28/2.05 % (1720506)Time elapsed: 0.031 s
% 8.28/2.05 % (1720506)Peak memory usage: 91 MB
% 8.28/2.05 % (1720506)Instructions burned: 48 (million)
% 8.28/2.05 % (1720504)Instruction limit reached!
% 8.28/2.05 % (1720504)------------------------------
% 8.28/2.05 % (1720504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720504)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720504)Termination reason: Instruction limit
% 8.28/2.05 % (1720504)Termination phase: Saturation
% 8.28/2.05 % (1720504)Time elapsed: 0.064 s
% 8.28/2.05 % (1720504)Peak memory usage: 91 MB
% 8.28/2.05 % (1720504)Instructions burned: 109 (million)
% 8.28/2.05 % (1720505)Instruction limit reached!
% 8.28/2.05 % (1720505)------------------------------
% 8.28/2.05 % (1720505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720505)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720505)Termination reason: Instruction limit
% 8.28/2.05 % (1720505)Termination phase: Saturation
% 8.28/2.05 % (1720505)Time elapsed: 0.065 s
% 8.28/2.05 % (1720505)Peak memory usage: 89 MB
% 8.28/2.05 % (1720505)Instructions burned: 119 (million)
% 8.28/2.05 % (1720515)lrs+10_1_sil=8000:sp=occurrence:random_seed=2236037560:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.28/2.05 % (1720515)Instruction limit reached!
% 8.28/2.05 % (1720515)------------------------------
% 8.28/2.05 % (1720515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720515)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720515)Termination reason: Instruction limit
% 8.28/2.05 % (1720515)Termination phase: Saturation
% 8.28/2.05 % (1720515)Time elapsed: 0.084 s
% 8.28/2.05 % (1720515)Peak memory usage: 94 MB
% 8.28/2.05 % (1720515)Instructions burned: 288 (million)
% 8.28/2.05 % (1720517)lrs+1011_1_sil=32000:sp=occurrence:random_seed=340916497:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.28/2.05 % (1720516)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3373814904:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.28/2.05 % (1720517)Refutation not found, incomplete strategy
% 8.28/2.05 % (1720517)------------------------------
% 8.28/2.05 % (1720517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720517)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720517)Termination reason: Refutation not found, incomplete strategy
% 8.28/2.05 % (1720517)Time elapsed: 0.033 s
% 8.28/2.05 % (1720517)Peak memory usage: 91 MB
% 8.28/2.05 % (1720517)Instructions burned: 51 (million)
% 8.28/2.05 % (1720516)Refutation not found, incomplete strategy
% 8.28/2.05 % (1720516)------------------------------
% 8.28/2.05 % (1720516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720516)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720516)Termination reason: Refutation not found, incomplete strategy
% 8.28/2.05 % (1720516)Time elapsed: 0.036 s
% 8.28/2.05 % (1720516)Peak memory usage: 91 MB
% 8.28/2.05 % (1720516)Instructions burned: 58 (million)
% 8.28/2.05 % (1720506)------------------------------
% 8.28/2.05 % (1720506)------------------------------
% 8.28/2.05 % (1720519)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1544883154:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 8.28/2.05 % (1720519)Refutation not found, incomplete strategy
% 8.28/2.05 % (1720519)------------------------------
% 8.28/2.05 % (1720519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720519)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720519)Termination reason: Refutation not found, incomplete strategy
% 8.28/2.05 % (1720519)Time elapsed: 0.016 s
% 8.28/2.05 % (1720519)Peak memory usage: 91 MB
% 8.28/2.05 % (1720519)Instructions burned: 47 (million)
% 8.28/2.05 % (1720522)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2429010022:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.28/2.05 % (1720516)------------------------------
% 8.28/2.05 % (1720516)------------------------------
% 8.28/2.05 % (1720517)------------------------------
% 8.28/2.05 % (1720517)------------------------------
% 8.28/2.05 % (1720519)------------------------------
% 8.28/2.05 % (1720519)------------------------------
% 8.28/2.05 % (1720522)Instruction limit reached!
% 8.28/2.05 % (1720522)------------------------------
% 8.28/2.05 % (1720522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720522)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720522)Termination reason: Instruction limit
% 8.28/2.05 % (1720522)Termination phase: Saturation
% 8.28/2.05 % (1720522)Time elapsed: 0.169 s
% 8.28/2.05 % (1720522)Peak memory usage: 93 MB
% 8.28/2.05 % (1720522)Instructions burned: 295 (million)
% 8.28/2.05 % (1720525)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=275202064:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.28/2.05 % (1720527)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=488944090:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 8.28/2.05 % (1720526)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3543156846:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.28/2.05 % (1720527)Instruction limit reached!
% 8.28/2.05 % (1720527)------------------------------
% 8.28/2.05 % (1720527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720527)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720527)Termination reason: Instruction limit
% 8.28/2.05 % (1720527)Termination phase: Saturation
% 8.28/2.05 % (1720527)Time elapsed: 0.064 s
% 8.28/2.05 % (1720527)Peak memory usage: 90 MB
% 8.28/2.05 % (1720527)Instructions burned: 129 (million)
% 8.28/2.05 % (1720526)Instruction limit reached!
% 8.28/2.05 % (1720526)------------------------------
% 8.28/2.05 % (1720526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720526)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720526)Termination reason: Instruction limit
% 8.28/2.05 % (1720526)Termination phase: Saturation
% 8.28/2.05 % (1720526)Time elapsed: 0.066 s
% 8.28/2.05 % (1720526)Peak memory usage: 92 MB
% 8.28/2.05 % (1720526)Instructions burned: 113 (million)
% 8.28/2.05 % (1720529)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2139886542:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.28/2.05 % (1720529)Instruction limit reached!
% 8.28/2.05 % (1720529)------------------------------
% 8.28/2.05 % (1720529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720529)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720529)Termination reason: Instruction limit
% 8.28/2.05 % (1720529)Termination phase: Saturation
% 8.28/2.05 % (1720529)Time elapsed: 0.058 s
% 8.28/2.05 % (1720529)Peak memory usage: 90 MB
% 8.28/2.05 % (1720529)Instructions burned: 115 (million)
% 8.28/2.05 % (1720502)First to succeed.
% 8.28/2.05 % (1720502)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1720496"
% 8.28/2.05 % (1720533)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=111377114:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.28/2.05 % (1720532)lrs+10_1_sil=8000:sp=occurrence:random_seed=3649093396:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 8.28/2.05 % (1720535)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2178672462:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.28/2.05 % (1720501)Also succeeded, but the first one will report.
% 8.28/2.05 % (1720533)Instruction limit reached!
% 8.28/2.05 % (1720533)------------------------------
% 8.28/2.05 % (1720533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/2.05 % (1720533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/2.05 % (1720533)CaDiCaL version: 2.1.3
% 8.28/2.05 % (1720533)Termination reason: Instruction limit
% 8.28/2.05 % (1720533)Termination phase: Saturation
% 8.28/2.05 % (1720533)Time elapsed: 0.230 s
% 8.28/2.05 % (1720533)Peak memory usage: 94 MB
% 8.28/2.05 % (1720533)Instructions burned: 439 (million)
% 8.28/2.05 % SZS status CounterSatisfiable for theBenchmark
% 8.28/2.05 % SZS output start Saturation.
% See solution above
% 8.28/2.06 % SZS output start Definitions and Model Updates.
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_2(X0,a1984) | c1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c10_2(X0,a1984) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c6_1(X0) | ~c10_2(X0,a1905) | ~ndr1_0 | ~sP18 is false, set ~c10_2(X0,a1905) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(X0) | ndr1_1(X0) | ~c10_2(X0,a1948) | ~ndr1_0 | ~sP13 is false, set ~c10_2(X0,a1948) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(a1875) | c1_0 | ndr1_0 is false, set ~c10_1(a1875) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c1_2(X0,a1889) | ~c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c1_2(X0,a1889) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c1_2(X0,a2032) | c1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~c1_2(X0,a2032) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c4_1(X3) | ndr1_1(X3) | ~c1_2(X3,a1838) | ~ndr1_0 | ~c7_0 | ~c1_2(X4,X5) | ~c7_2(X4,X5) | ~ndr1_1(X4) | ~c6_1(X4) | ~c10_1(X4) | ~ndr1_0 is false, set ~c1_2(X3,a1838) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c8_1(X0) | ~c1_2(X0,a1864) | ~ndr1_0 | ~sP23 is false, set ~c1_2(X0,a1864) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c1_2(X0,a1863) | ~c8_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP23 is false, set ~c1_2(X0,a1863) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c3_2(X0,a1834) | ndr1_1(X0) | sP28(X0) | ~ndr1_0 | c4_0 | ~c6_0 is false, set ~c3_2(X0,a1834) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c7_2(X0,a1888) | ndr1_1(X0) | ~c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c7_2(X0,a1888) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c7_2(X0,a1904) | c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~c7_2(X0,a1904) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c4_1(X3) | ~c3_2(X3,a1837) | ndr1_1(X3) | ~ndr1_0 | ~c7_0 | ~c1_2(X4,X5) | ~c7_2(X4,X5) | ~ndr1_1(X4) | ~c6_1(X4) | ~c10_1(X4) | ~ndr1_0 is false, set ~c3_2(X3,a1837) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c7_2(X0,a1889) | ~c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c7_2(X0,a1889) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c7_2(X0,a1957) | ~c8_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c7_2(X0,a1957) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c3_2(X0,a1863) | ~c8_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP23 is false, set ~c3_2(X0,a1863) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(a1884) | ndr1_0 | ~c1_0 is false, set c10_1(a1884) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X153) | ~c10_1(X153) | c1_2(X153,a1991) | ~ndr1_0 | sP5 | ~c6_0 is false, set c1_2(X153,a1991) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c8_2(X0,a1904) | c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~c8_2(X0,a1904) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c1_2(X0,a1855) | ndr1_1(X0) | c10_1(X0) | ~ndr1_0 | ~sP24 is false, set c1_2(X0,a1855) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c1_2(X0,a1956) | ndr1_1(X0) | ~c8_1(X0) | ~ndr1_0 | ~sP11 is false, set c1_2(X0,a1956) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c8_2(X0,a1957) | ~c8_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c8_2(X0,a1957) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c1_2(X0,a1856) | c10_1(X0) | ~ndr1_0 | ~sP24 is false, set c1_2(X0,a1856) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X0) | c1_2(X0,a1980) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set c1_2(X0,a1980) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c6_1(a1875) | c1_0 | ndr1_0 is false, set c6_1(a1875) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c1_1(X0) | c6_2(X0,a1985) | ~ndr1_0 | ~sP6 is false, set c6_2(X0,a1985) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_1(X0) | ndr1_1(X0) | c6_2(X0,a2009) | ~ndr1_0 | ~sP2 is false, set c6_2(X0,a2009) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c4_1(X3) | ndr1_1(X3) | c6_2(X3,a1838) | ~ndr1_0 | ~c7_0 | ~c1_2(X4,X5) | ~c7_2(X4,X5) | ~ndr1_1(X4) | ~c6_1(X4) | ~c10_1(X4) | ~ndr1_0 is false, set c6_2(X3,a1838) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c6_2(X0,a1957) | ~c8_1(X0) | ~ndr1_0 | ~sP11 is false, set c6_2(X0,a1957) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c5_2(X0,a1856) | c10_1(X0) | ~ndr1_0 | ~sP24 is false, set ~c5_2(X0,a1856) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c6_2(X0,a1855) | ndr1_1(X0) | c10_1(X0) | ~ndr1_0 | ~sP24 is false, set c6_2(X0,a1855) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c6_2(X0,a1889) | ~c6_1(X0) | ~ndr1_0 | ~sP20 is false, set c6_2(X0,a1889) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c4_1(X3) | c6_2(X3,a1837) | ndr1_1(X3) | ~ndr1_0 | ~c7_0 | ~c1_2(X4,X5) | ~c7_2(X4,X5) | ~ndr1_1(X4) | ~c6_1(X4) | ~c10_1(X4) | ~ndr1_0 is false, set c6_2(X3,a1837) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_1(X0) | ~c5_2(X0,a2008) | ndr1_1(X0) | ~ndr1_0 | ~sP2 is false, set ~c5_2(X0,a2008) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c5_2(X0,a1888) | ndr1_1(X0) | ~c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c5_2(X0,a1888) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X0) | ndr1_1(X0) | ~c5_2(X0,a1981) | ~ndr1_0 | ~sP8 is false, set ~c5_2(X0,a1981) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c5_2(X153,a1990) | ~c10_1(X153) | ndr1_1(X153) | ~ndr1_0 | sP5 | ~c6_0 is false, set ~c5_2(X153,a1990) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c5_2(X0,a2031) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~c5_2(X0,a2031) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c8_2(X0,a1863) | ~c8_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP23 is false, set c8_2(X0,a1863) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c8_2(X0,a1956) | ndr1_1(X0) | ~c8_1(X0) | ~ndr1_0 | ~sP11 is false, set c8_2(X0,a1956) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c8_2(X0,a2031) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP0 is false, set c8_2(X0,a2031) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c8_1(X0) | c8_2(X0,a1864) | ~ndr1_0 | ~sP23 is false, set c8_2(X0,a1864) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c8_2(X0,a1984) | c1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c8_2(X0,a1984) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c1_1(X0) | c8_2(X0,a1985) | ~ndr1_0 | ~sP6 is false, set c8_2(X0,a1985) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c8_2(X0,a1992) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP5 is false, set c8_2(X0,a1992) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c8_2(X0,a1993) | c1_1(X0) | ~ndr1_0 | ~sP5 is false, set c8_2(X0,a1993) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_1(X0) | ndr1_1(X0) | ~c4_2(X0,a2009) | ~ndr1_0 | ~sP2 is false, set ~c4_2(X0,a2009) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_2(a1875,X26) | ~c10_2(a1875,X26) | ~c8_2(a1875,X26) | ~ndr1_1(a1875) | c1_0 | ndr1_0 is false, set ~c4_2(a1875,X26) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X153) | ~c10_1(X153) | ~c4_2(X153,a1991) | ~ndr1_0 | sP5 | ~c6_0 is false, set ~c4_2(X153,a1991) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c6_1(X0) | ~c4_2(X0,a1905) | ~ndr1_0 | ~sP18 is false, set ~c4_2(X0,a1905) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X0) | ndr1_1(X0) | ~c2_2(X0,a1981) | ~ndr1_0 | ~sP8 is false, set ~c2_2(X0,a1981) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c2_2(X0,a1992) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c2_2(X0,a1992) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_1(X0) | ~c2_2(X0,a2008) | ndr1_1(X0) | ~ndr1_0 | ~sP2 is false, set ~c2_2(X0,a2008) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c8_2(a1885,X34) | ~c2_2(a1885,X34) | ~c3_2(a1885,X34) | ~ndr1_1(a1885) | ~c1_0 is false, set ~c2_2(a1885,X34) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c2_2(X153,a1990) | ~c10_1(X153) | ndr1_1(X153) | ~ndr1_0 | sP5 | ~c6_0 is false, set ~c2_2(X153,a1990) to true
% 8.28/2.06 for all groundings, until fixed point,
% 8.28/2.06 whenever c4_1(X3) | c7_2(X3,a1837) | ndr1_1(X3) | ~ndr1_0 | ~c7_0 | ~c1_2(X4,X5) | ~c7_2(X4,X5) | ~ndr1_1(X4) | ~c6_1(X4) | ~c10_1(X4) | ~ndr1_0 is false, set c7_2(X3,a1837) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c8_1(X0) | c7_2(X0,a1864) | ~ndr1_0 | ~sP23 is false, set c7_2(X0,a1864) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(X0) | c7_2(X0,a1947) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c7_2(X0,a1947) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X0) | ndr1_1(X0) | c7_2(X0,a1981) | ~ndr1_0 | ~sP8 is false, set c7_2(X0,a1981) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X0) | c7_2(X0,a1980) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set c7_2(X0,a1980) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_1(X0) | ndr1_1(X0) | c7_2(X0,a2009) | ~ndr1_0 | ~sP2 is false, set c7_2(X0,a2009) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c7_2(X0,a2032) | c1_1(X0) | ~ndr1_0 | ~sP0 is false, set c7_2(X0,a2032) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c7_2(X0,a1834) | ndr1_1(X0) | sP28(X0) | ~ndr1_0 | c4_0 | ~c6_0 is false, set c7_2(X0,a1834) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(X0) | ndr1_1(X0) | c7_2(X0,a1948) | ~ndr1_0 | ~sP13 is false, set c7_2(X0,a1948) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X0) | c4_2(X0,a1980) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set c4_2(X0,a1980) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_1(X0) | c3_2(X0,a2008) | ndr1_1(X0) | ~ndr1_0 | ~sP2 is false, set c3_2(X0,a2008) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c1_1(X0) | c3_2(X0,a1985) | ~ndr1_0 | ~sP6 is false, set c3_2(X0,a1985) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c3_2(X0,a1835) | sP28(X0) | ~ndr1_0 | c4_0 | ~c6_0 is false, set c3_2(X0,a1835) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c9_2(X0,a1984) | c1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c9_2(X0,a1984) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(X0) | c9_2(X0,a1947) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c9_2(X0,a1947) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c9_2(a1884,X33) | ~c1_2(a1884,X33) | c7_2(a1884,X33) | ~ndr1_1(a1884) | ndr1_0 | ~c1_0 is false, set c9_2(a1884,X33) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c9_2(a1913,X67) | c7_2(a1913,X67) | c3_2(a1913,X67) | ~ndr1_1(a1913) | c1_0 | ndr1_0 is false, set c9_2(a1913,X67) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | ~c2_1(a1885) | ~c1_0 is false, set ~c2_1(a1885) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c2_1(a1913) | c1_0 | ndr1_0 is false, set ~c2_1(a1913) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c1_0 | ~c2_1(a1876) is false, set ~c2_1(a1876) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c10_2(X0,a1856) | c10_1(X0) | ~ndr1_0 | ~sP24 is false, set c10_2(X0,a1856) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_2(X0,a1855) | ndr1_1(X0) | c10_1(X0) | ~ndr1_0 | ~sP24 is false, set c10_2(X0,a1855) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_2(X0,a1904) | c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set c10_2(X0,a1904) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c10_2(X0,a1993) | c1_1(X0) | ~ndr1_0 | ~sP5 is false, set c10_2(X0,a1993) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c4_1(X3) | ndr1_1(X3) | c10_2(X3,a1838) | ~ndr1_0 | ~c7_0 | ~c1_2(X4,X5) | ~c7_2(X4,X5) | ~ndr1_1(X4) | ~c6_1(X4) | ~c10_1(X4) | ~ndr1_0 is false, set c10_2(X3,a1838) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_2(X153,a1990) | ~c10_1(X153) | ndr1_1(X153) | ~ndr1_0 | sP5 | ~c6_0 is false, set c10_2(X153,a1990) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_2(X0,a1992) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP5 is false, set c10_2(X0,a1992) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(X0) | c2_2(X0,a1947) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c2_2(X0,a1947) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c2_2(X0,a2032) | c1_1(X0) | ~ndr1_0 | ~sP0 is false, set c2_2(X0,a2032) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c1_0 | c9_1(a1914) is false, set c9_1(a1914) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c1_1(X119) | c8_1(X119) | ndr1_1(X119) | ~ndr1_0 | ndr1_0 is false, set c8_1(X119) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c1_1(X119) | c8_1(X119) | c3_2(X119,a1962) | ~ndr1_0 | ndr1_0 is false, set c8_1(X119) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c1_1(X119) | c8_1(X119) | c6_2(X119,a1962) | ~ndr1_0 | ndr1_0 is false, set c8_1(X119) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c6_1(X0) | c5_2(X0,a1905) | ~ndr1_0 | ~sP18 is false, set c5_2(X0,a1905) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | c5_2(X0,a1835) | sP28(X0) | ~ndr1_0 | c4_0 | ~c6_0 is false, set c5_2(X0,a1835) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X0) | ~c9_2(X0,a1993) | c1_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c9_2(X0,a1993) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c9_2(X0,a1834) | ndr1_1(X0) | sP28(X0) | ~ndr1_0 | c4_0 | ~c6_0 is false, set ~c9_2(X0,a1834) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c1_1(X119) | c8_1(X119) | ~c9_2(X119,a1962) | ~ndr1_0 | ndr1_0 is false, set ~c9_2(X119,a1962) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X153) | ~c10_1(X153) | ~c9_2(X153,a1991) | ~ndr1_0 | sP5 | ~c6_0 is false, set ~c9_2(X153,a1991) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c1_0 | ~c5_1(a1876) is false, set ~c5_1(a1876) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c10_1(X0) | ndr1_1(X0) | ~c6_2(X0,a1948) | ~ndr1_0 | ~sP13 is false, set ~c6_2(X0,a1948) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c6_2(X0,a1956) | ndr1_1(X0) | ~c8_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c6_2(X0,a1956) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c6_2(X0,a1888) | ndr1_1(X0) | ~c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c6_2(X0,a1888) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c1_0 | ~c3_1(a1914) is false, set ~c3_1(a1914) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | ~c6_2(X97,a1940) | c3_1(X97) | ~c6_1(X97) | ~ndr1_0 is false, set c3_1(X97) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | ndr1_1(X97) | c3_1(X97) | ~c6_1(X97) | ~ndr1_0 is false, set c3_1(X97) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c8_2(X97,a1940) | c3_1(X97) | ~c6_1(X97) | ~ndr1_0 is false, set c3_1(X97) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | ~c8_1(a1885) | ~c1_0 is false, set ~c8_1(a1885) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X63) | c7_1(X63) | ndr1_1(X63) | ~ndr1_0 | c1_0 | ~c8_1(X64) | c4_2(X64,X65) | c3_2(X64,X65) | c10_2(X64,X65) | ~ndr1_1(X64) | ndr1_1(X64) | ~ndr1_0 is false, set c7_1(X63) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X63) | c7_1(X63) | c9_2(X63,a1908) | ~ndr1_0 | c1_0 | ~c8_1(X64) | c4_2(X64,X65) | c3_2(X64,X65) | c10_2(X64,X65) | ~ndr1_1(X64) | ndr1_1(X64) | ~ndr1_0 is false, set c7_1(X63) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X63) | c7_1(X63) | c1_2(X63,a1908) | ~ndr1_0 | c1_0 | ~c8_1(X64) | c4_2(X64,X65) | c3_2(X64,X65) | c10_2(X64,X65) | ~ndr1_1(X64) | ndr1_1(X64) | ~ndr1_0 is false, set c7_1(X63) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c10_1(X63) | c7_1(X63) | c3_2(X63,a1908) | ~ndr1_0 | c1_0 | ~c8_1(X64) | c4_2(X64,X65) | c3_2(X64,X65) | c10_2(X64,X65) | ~ndr1_1(X64) | ndr1_1(X64) | ~ndr1_0 is false, set c7_1(X63) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X46) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | ndr1_0 is false, set c2_1(X46) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X46) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | ~c1_1(a1899) is false, set c2_1(X46) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_1(X46) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | c1_2(a1899,X48) | ~c9_2(a1899,X48) | c2_2(a1899,X48) | ~ndr1_1(a1899) is false, set c2_1(X46) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c6_2(X46,a1898) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | ndr1_0 is false, set c2_1(X46) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c2_2(X46,a1898) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | ndr1_0 is false, set c2_1(X46) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c1_2(X46,a1898) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | ndr1_0 is false, set c2_1(X46) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c1_0 | c5_1(a1914) is false, set c5_1(a1914) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c5_0 | c5_1(X85) | ~c6_1(X85) | ~ndr1_0 is false, set c5_1(X85) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | ndr1_1(X183) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | ~c6_2(X185,a2025) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | c3_2(X183,a2024) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | ndr1_1(X183) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | c3_2(X185,a2025) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | ndr1_1(X183) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | ~c5_2(X185,a2025) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | c10_2(X183,a2024) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | ~c6_2(X183,a2024) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c4_1(X183) | c7_2(X183,X184) | ~c10_2(X183,X184) | c4_2(X183,X184) | ~ndr1_1(X183) | ndr1_1(X183) | ~ndr1_0 | ~c7_0 | c10_1(X185) | ~c8_2(X185,X186) | c2_2(X185,X186) | c3_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 is false, set ~c7_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c2_0 | ndr1_0 | ~c10_1(X95) | ~c6_1(X95) | ~ndr1_0 is false, set c2_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | ndr1_1(X114) | ndr1_1(X114) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | ndr1_1(X114) | c10_2(X114,a1954) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | c4_2(X114,a1953) | ndr1_1(X114) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | c10_2(X114,a1953) | ndr1_1(X114) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | ~c6_2(X114,a1953) | ndr1_1(X114) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | ndr1_1(X114) | c3_2(X114,a1954) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c3_0 | c1_2(X114,X115) | ~c5_2(X114,X115) | ~c7_2(X114,X115) | ~ndr1_1(X114) | ndr1_1(X114) | c5_2(X114,a1954) | ~ndr1_0 is false, set c3_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c1_0 | ndr1_0 | ndr1_1(X78) | c6_1(X78) | ~c7_1(X78) | ~ndr1_0 is false, set ~c7_1(X78) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c1_0 | ndr1_0 | c10_2(X78,a1925) | c6_1(X78) | ~c7_1(X78) | ~ndr1_0 is false, set ~c7_1(X78) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c7_1(a1884) | ndr1_0 | ~c1_0 is false, set ~c7_1(a1884) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c1_0 | ndr1_0 | c5_2(X78,a1925) | c6_1(X78) | ~c7_1(X78) | ~ndr1_0 is false, set ~c7_1(X78) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c1_0 | ndr1_0 | c7_2(X78,a1925) | c6_1(X78) | ~c7_1(X78) | ~ndr1_0 is false, set ~c7_1(X78) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c5_1(X123) | ~c10_2(X123,X124) | ~c4_2(X123,X124) | c6_2(X123,X124) | ~ndr1_1(X123) | ~c7_1(X123) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X123) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c7_0 | ~c7_1(X19) | c8_1(X19) | c9_2(X19,X20) | ~c7_2(X19,X20) | c3_2(X19,X20) | ~ndr1_1(X19) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X19) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ~c7_0 | c10_1(X22) | c4_1(X22) | c1_2(X22,X23) | c10_2(X22,X23) | c4_2(X22,X23) | ~ndr1_1(X22) | ~ndr1_0 | ndr1_0 is false, set c4_1(X22) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c4_1(X147) | ~c1_2(X147,X148) | c3_2(X147,X148) | ~c8_2(X147,X148) | ~ndr1_1(X147) | c5_1(X147) | ~ndr1_0 | ndr1_0 | c9_1(X150) | ~c8_1(X150) | ~c8_2(X150,X151) | c5_2(X150,X151) | c10_2(X150,X151) | ~ndr1_1(X150) | ~ndr1_0 is false, set c4_1(X147) to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever c8_0 | ndr1_0 | ~c6_1(X117) | c9_2(X117,X118) | c1_2(X117,X118) | c8_2(X117,X118) | ~ndr1_1(X117) | c1_1(X117) | ~ndr1_0 is false, set c8_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c8_0 | ~c8_2(X188,a2028) | c2_1(X188) | ~c6_1(X188) | ~ndr1_0 is false, set c8_0 to true
% 8.28/2.06 for all groundings,
% 8.28/2.06 whenever ndr1_0 | c8_0 | c2_2(X188,a2028) | c2_1(X188) | ~c6_1(X188) | ~ndr1_0 is false, set c8_0 to true
% 8.28/2.06 for all groundings,
% 9.89/2.25 whenever ndr1_0 | c8_0 | ndr1_1(X188) | c2_1(X188) | ~c6_1(X188) | ~ndr1_0 is false, set c8_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | c8_0 | c4_2(X188,a2028) | c2_1(X188) | ~c6_1(X188) | ~ndr1_0 is false, set c8_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c5_1(X72) | ~c3_2(X72,X73) | ~c1_2(X72,X73) | ~c6_2(X72,X73) | ~ndr1_1(X72) | c2_1(X72) | ~ndr1_0 | ndr1_0 | ~c5_0 is false, set ~c5_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c7_2(X111,X112) | ~c6_2(X111,X112) | ~c3_2(X111,X112) | ~ndr1_1(X111) | c6_1(X111) | ~ndr1_0 | ~c5_0 | ndr1_0 is false, set ~c5_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | ndr1_1(X167) | ~ndr1_0 | c1_2(X169,a2013) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | c8_2(X167,a2012) | ~ndr1_0 | ndr1_1(X169) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | ndr1_1(X167) | ~ndr1_0 | c7_2(X169,a2013) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | ndr1_1(X167) | ~ndr1_0 | ndr1_1(X169) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | ndr1_1(X167) | ~ndr1_0 | ~c4_2(X169,a2013) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | c2_2(X167,a2012) | ~ndr1_0 | ndr1_1(X169) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c2_0 | c1_2(X167,X168) | ~c6_2(X167,X168) | ~ndr1_1(X167) | c5_1(X167) | ~c7_2(X167,a2012) | ~ndr1_0 | ndr1_1(X169) | c10_1(X169) | ~c8_2(X169,X170) | c4_2(X169,X170) | c10_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set ~c2_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | ndr1_1(X7) | ndr1_1(X7) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | ndr1_1(X7) | c10_2(X7,a1844) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | c9_2(X7,a1843) | ndr1_1(X7) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | ndr1_1(X7) | c6_2(X7,a1844) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | ndr1_1(X7) | c7_2(X7,a1844) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | c7_2(X7,a1843) | ndr1_1(X7) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c8_0 | ~c3_2(X7,a1843) | ndr1_1(X7) | c5_2(X7,X8) | ~c6_2(X7,X8) | ~c4_2(X7,X8) | ~ndr1_1(X7) | ~ndr1_0 | ~c9_1(X9) | ~c3_1(X9) | ~c4_2(X9,X10) | c2_2(X9,X10) | ~c1_2(X9,X10) | ~ndr1_1(X9) | ~ndr1_0 is false, set ~c9_1(X9) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c5_2(X41,X42) | c10_2(X41,X42) | ~c9_2(X41,X42) | ~ndr1_1(X41) | c10_1(X41) | c4_2(X41,X43) | c10_2(X41,X43) | ~c9_2(X41,X43) | ~ndr1_1(X41) | ~ndr1_0 | ~c9_1(X44) | c1_1(X44) | c8_2(X44,X45) | c2_2(X44,X45) | ~ndr1_1(X44) | ~ndr1_0 | ndr1_0 is false, set ~c9_1(X44) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_1(X46) | c2_1(X46) | c8_2(X46,X47) | c5_2(X46,X47) | ~c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 | ~c9_1(a1899) is false, set ~c9_1(a1899) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~c6_1(X175) | ndr1_1(X175) | ~c3_2(X175,X176) | c2_2(X175,X176) | c1_2(X175,X176) | ~ndr1_1(X175) | ~ndr1_0 | ~c3_1(X177) | ~c10_1(X177) | ~c9_1(X177) | ~ndr1_0 is false, set ~c9_1(X177) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~c6_1(X175) | c5_2(X175,a2020) | ~c3_2(X175,X176) | c2_2(X175,X176) | c1_2(X175,X176) | ~ndr1_1(X175) | ~ndr1_0 | ~c3_1(X177) | ~c10_1(X177) | ~c9_1(X177) | ~ndr1_0 is false, set ~c9_1(X177) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~c6_1(X175) | ~c9_2(X175,a2020) | ~c3_2(X175,X176) | c2_2(X175,X176) | c1_2(X175,X176) | ~ndr1_1(X175) | ~ndr1_0 | ~c3_1(X177) | ~c10_1(X177) | ~c9_1(X177) | ~ndr1_0 is false, set ~c9_1(X177) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c2_2(a2019,X174) | ~c6_2(a2019,X174) | ~c3_2(a2019,X174) | ~ndr1_1(a2019) | ~c6_1(X175) | ndr1_1(X175) | ~c3_2(X175,X176) | c2_2(X175,X176) | c1_2(X175,X176) | ~ndr1_1(X175) | ~ndr1_0 | ~c3_1(X177) | ~c10_1(X177) | ~c9_1(X177) | ~ndr1_0 is false, set ~c9_1(X177) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c3_1(a2019) | ~c6_1(X175) | ndr1_1(X175) | ~c3_2(X175,X176) | c2_2(X175,X176) | c1_2(X175,X176) | ~ndr1_1(X175) | ~ndr1_0 | ~c3_1(X177) | ~c10_1(X177) | ~c9_1(X177) | ~ndr1_0 is false, set ~c9_1(X177) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c4_1(a2019) | ~c6_1(X175) | ndr1_1(X175) | ~c3_2(X175,X176) | c2_2(X175,X176) | c1_2(X175,X176) | ~ndr1_1(X175) | ~ndr1_0 | ~c3_1(X177) | ~c10_1(X177) | ~c9_1(X177) | ~ndr1_0 is false, set ~c9_1(X177) to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c1_2(X37,X38) | c7_2(X37,X38) | ~c3_2(X37,X38) | ~ndr1_1(X37) | c9_1(X37) | c8_2(X37,X39) | c10_2(X37,X39) | ~ndr1_1(X37) | ~ndr1_0 | ~c10_0 | ndr1_0 is false, set ~c10_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | sP2 | c4_0 is false, set sP2 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | c3_0 | sP8 is false, set sP8 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | c9_0 | sP13 is false, set sP13 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | sP18 | ~c3_2(a1906,X51) | ~c2_2(a1906,X51) | ~c1_2(a1906,X51) | ~ndr1_1(a1906) is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | sP18 | ndr1_0 is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | sP18 | c9_2(a1906,X52) | ~c2_2(a1906,X52) | ~c1_2(a1906,X52) | ~ndr1_1(a1906) is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c7_2(a1903,X49) | ~c9_2(a1903,X49) | ~c8_2(a1903,X49) | ~ndr1_1(a1903) | sP18 | ndr1_0 is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | sP18 | c4_1(a1906) is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c3_1(a1903) | sP18 | ndr1_0 is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c4_2(a1903,X50) | c7_2(a1903,X50) | c5_2(a1903,X50) | ~ndr1_1(a1903) | sP18 | ndr1_0 is false, set sP18 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever sP20 | ndr1_0 | ~c1_0 is false, set sP20 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever sP23 | ndr1_0 is false, set sP23 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP15 is false, set ~sP15 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP22 is false, set ~sP22 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ~c6_0 | ndr1_0 | sP24 is false, set sP24 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c3_0 | ndr1_0 | sP0 is false, set sP0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP12 is false, set ~sP12 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_1(X160) | c2_1(X160) | c7_2(X160,X161) | ~c4_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ~ndr1_0 | ~c6_0 | ~c1_0 is false, set ~c6_0 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever sP9 | ~c2_2(X139,X140) | ~c1_2(X139,X140) | ~c3_2(X139,X140) | ~ndr1_1(X139) | c3_1(X139) | ~c3_2(X139,X141) | ~c7_2(X139,X141) | ~c8_2(X139,X141) | ~ndr1_1(X139) | ~ndr1_0 | c7_1(X142) | ndr1_1(X142) | ~c2_2(X142,X143) | c5_2(X142,X143) | c7_2(X142,X143) | ~ndr1_1(X142) | ~ndr1_0 is false, set sP9 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever sP14 | ndr1_0 | ~c3_2(X105,X106) | ~c8_2(X105,X106) | c1_2(X105,X106) | ~ndr1_1(X105) | ~c6_2(X105,X107) | ~c8_2(X105,X107) | c3_2(X105,X107) | ~ndr1_1(X105) | ~ndr1_0 is false, set sP14 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c8_1(X108) | c1_1(X108) | c7_2(X108,a1949) | ~ndr1_0 | sP12 | ndr1_0 is false, set sP12 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c8_1(X108) | c1_1(X108) | c10_2(X108,a1949) | ~ndr1_0 | sP12 | ndr1_0 is false, set sP12 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c8_1(X108) | c1_1(X108) | c9_2(X108,a1949) | ~ndr1_0 | sP12 | ndr1_0 is false, set sP12 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever c8_1(X108) | c1_1(X108) | ndr1_1(X108) | ~ndr1_0 | sP12 | ndr1_0 is false, set sP12 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP7 is false, set ~sP7 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP10 is false, set ~sP10 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP14 is false, set ~sP14 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP4 is false, set ~sP4 to true
% 9.89/2.25 for all groundings,
% 9.89/2.25 whenever ndr1_0 | ~sP9 is false, set ~sP9 to true
% 9.89/2.25 % SZS output end Definitions and Model Updates.
% 9.89/2.25 % (1720502)------------------------------
% 9.89/2.25 % (1720502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.89/2.25 % (1720502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.89/2.25 % (1720502)CaDiCaL version: 2.1.3
% 9.89/2.25 % (1720502)Termination reason: Satisfiable
% 9.89/2.25 % (1720502)Time elapsed: 0.881 s
% 9.89/2.25 % (1720502)Peak memory usage: 135 MB
% 9.89/2.25 % (1720502)Instructions burned: 1345 (million)
% 9.89/2.25 % (1720502)------------------------------
% 9.89/2.25 % (1720502)------------------------------
% 9.89/2.25 % (1720496)Success in time 1.331 s
% 9.89/2.25 % Vampire exiting
%------------------------------------------------------------------------------