%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN423+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 : n007.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:35 PM UTC 2026
% Result : CounterSatisfiable 9.61s 2.09s
% Output : Saturation 9.61s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1045,negated_conjecture,
~ ndr1_1(a619) ).
cnf(u3060,negated_conjecture,
~ sP0 ).
cnf(u1061,negated_conjecture,
~ c3_1(a619) ).
cnf(u1065,negated_conjecture,
c8_1(a619) ).
cnf(u1081,negated_conjecture,
ndr1_0 ).
cnf(u1085,negated_conjecture,
~ ndr1_1(a615) ).
cnf(u3087,negated_conjecture,
~ sP1 ).
cnf(u1095,negated_conjecture,
~ c1_1(a615) ).
cnf(u1099,negated_conjecture,
c7_1(a615) ).
cnf(u1107,negated_conjecture,
c1_1(a610) ).
cnf(u1135,negated_conjecture,
sP2 ).
cnf(u3170,negated_conjecture,
~ sP4 ).
cnf(u1166,negated_conjecture,
~ c8_1(a603) ).
cnf(u3129,negated_conjecture,
~ sP3 ).
cnf(u1173,negated_conjecture,
~ c6_1(a603) ).
cnf(u1177,negated_conjecture,
~ c10_1(a603) ).
cnf(u1187,negated_conjecture,
( ~ c9_2(X155,X158)
| c10_2(X155,X156)
| ~ c8_2(X155,X158)
| ~ c5_2(X155,X158)
| ~ c8_2(X155,X157)
| ~ c4_2(X155,X157)
| c9_2(X155,X157)
| ~ ndr1_1(X155)
| ~ c6_2(X155,X156)
| ~ c3_2(X155,X156) ) ).
cnf(u3205,negated_conjecture,
~ sP5 ).
cnf(u1198,negated_conjecture,
( ~ c5_2(X154,a597)
| ~ c7_1(X154) ) ).
cnf(u1201,negated_conjecture,
( ~ c5_2(X153,a596)
| c5_1(X153)
| c8_1(X153) ) ).
cnf(u1205,negated_conjecture,
( ~ c3_2(X154,a597)
| ~ c7_1(X154) ) ).
cnf(u1209,negated_conjecture,
( c10_2(X154,a597)
| ~ c7_1(X154) ) ).
cnf(u1217,negated_conjecture,
( ~ c2_2(X153,a596)
| c5_1(X153)
| c8_1(X153) ) ).
cnf(u1224,negated_conjecture,
( c5_1(X153)
| ndr1_1(X153)
| c8_1(X153) ) ).
cnf(u1231,negated_conjecture,
~ ndr1_1(a595) ).
cnf(u3243,negated_conjecture,
~ sP6 ).
cnf(u1244,negated_conjecture,
~ c9_1(a595) ).
cnf(u1248,negated_conjecture,
~ c3_1(a595) ).
cnf(u3272,negated_conjecture,
~ sP7 ).
cnf(u1255,negated_conjecture,
( ~ c9_2(X148,a590)
| c3_1(X148)
| ~ ndr1_1(X148)
| ~ c9_2(X148,X149)
| ~ c5_2(X148,X149)
| c3_2(X148,X149) ) ).
cnf(u1259,negated_conjecture,
( ~ c10_2(X148,a590)
| c3_1(X148)
| ~ ndr1_1(X148)
| ~ c9_2(X148,X149)
| ~ c5_2(X148,X149)
| c3_2(X148,X149) ) ).
cnf(u3297,negated_conjecture,
~ sP8 ).
cnf(u1269,negated_conjecture,
( c3_1(X147)
| ~ c2_1(X147)
| ~ c1_1(X147) ) ).
cnf(u3322,negated_conjecture,
~ sP9 ).
cnf(u1296,negated_conjecture,
( ~ c3_1(X145)
| ~ c6_2(X145,a583)
| ~ ndr1_1(X145)
| ~ c7_2(X145,X146)
| c6_2(X145,X146)
| c5_2(X145,X146) ) ).
cnf(u1303,negated_conjecture,
( ~ c3_1(X145)
| c4_2(X145,a583)
| ~ ndr1_1(X145)
| ~ c7_2(X145,X146)
| c6_2(X145,X146)
| c5_2(X145,X146) ) ).
cnf(u1307,negated_conjecture,
( ~ c3_1(X145)
| c10_2(X145,a583)
| ~ ndr1_1(X145)
| ~ c7_2(X145,X146)
| c6_2(X145,X146)
| c5_2(X145,X146) ) ).
cnf(u3348,negated_conjecture,
~ sP10 ).
cnf(u1317,negated_conjecture,
( ~ c5_1(X141)
| c10_1(X141)
| ~ c3_1(X141) ) ).
cnf(u1338,negated_conjecture,
( ~ c4_1(X138)
| ~ c8_2(X138,X140)
| ~ c6_2(X138,X140)
| ~ c5_2(X138,X140)
| ~ ndr1_1(X138)
| ~ c4_2(X138,X139)
| ~ c10_2(X138,X139)
| c8_2(X138,X139) ) ).
cnf(u1360,negated_conjecture,
( ~ c8_2(X131,a577)
| c9_2(X131,X132)
| ~ c9_2(X131,X133)
| ~ c8_2(X131,X133)
| ~ c4_2(X131,X133)
| ~ ndr1_1(X131)
| ~ c3_2(X131,X132)
| ~ c1_2(X131,X132) ) ).
cnf(u1370,negated_conjecture,
( ~ c4_2(X131,X133)
| c9_2(X131,a577)
| ~ c9_2(X131,X133)
| ~ c8_2(X131,X133)
| c9_2(X131,X132)
| ~ ndr1_1(X131)
| ~ c3_2(X131,X132)
| ~ c1_2(X131,X132) ) ).
cnf(u1374,negated_conjecture,
( ~ c4_2(X131,X133)
| c3_2(X131,a577)
| ~ c9_2(X131,X133)
| ~ c8_2(X131,X133)
| c9_2(X131,X132)
| ~ ndr1_1(X131)
| ~ c3_2(X131,X132)
| ~ c1_2(X131,X132) ) ).
cnf(u1402,negated_conjecture,
~ c9_0 ).
cnf(u1415,negated_conjecture,
~ c3_1(a574) ).
cnf(u1418,negated_conjecture,
~ c7_0 ).
cnf(u1422,negated_conjecture,
~ c10_1(a574) ).
cnf(u1426,negated_conjecture,
c1_1(a574) ).
cnf(u3373,negated_conjecture,
~ sP11 ).
cnf(u1434,negated_conjecture,
c7_1(a571) ).
cnf(u1438,negated_conjecture,
c6_1(a571) ).
cnf(u1442,negated_conjecture,
c1_1(a571) ).
cnf(u1447,negated_conjecture,
sP12 ).
cnf(u1450,negated_conjecture,
~ c7_2(a566,a567) ).
cnf(u1453,negated_conjecture,
~ c5_0 ).
cnf(u1457,negated_conjecture,
c8_2(a566,a567) ).
cnf(u1461,negated_conjecture,
ndr1_1(a566) ).
cnf(u1466,negated_conjecture,
( ~ c6_2(a566,X125)
| ~ c8_2(a566,X125)
| ~ c10_2(a566,X125) ) ).
cnf(u1475,negated_conjecture,
c4_2(a564,a565) ).
cnf(u1479,negated_conjecture,
c10_2(a564,a565) ).
cnf(u1483,negated_conjecture,
ndr1_1(a564) ).
cnf(u1487,negated_conjecture,
~ c1_1(a564) ).
cnf(u1491,negated_conjecture,
c10_1(a564) ).
cnf(u1502,negated_conjecture,
( ~ c5_1(X121)
| ~ c4_2(X121,X123)
| c5_2(X121,X123)
| ~ ndr1_1(X121)
| ~ c6_2(X121,X122)
| ~ c5_2(X121,X122)
| c10_2(X121,X122) ) ).
cnf(u1520,negated_conjecture,
( ~ c3_1(X118)
| ~ ndr1_1(X118)
| c8_2(X118,X119)
| c6_2(X118,X119)
| c4_2(X118,X119)
| c8_1(X118) ) ).
cnf(u3435,negated_conjecture,
~ sP13 ).
cnf(u1535,negated_conjecture,
( ~ c2_2(X116,a559)
| c7_1(X116)
| ~ ndr1_1(X116)
| ~ c5_2(X116,X117)
| c10_2(X116,X117) ) ).
cnf(u1539,negated_conjecture,
( c10_2(X116,X117)
| c8_2(X116,a559)
| ~ ndr1_1(X116)
| ~ c5_2(X116,X117)
| c7_1(X116) ) ).
cnf(u1550,negated_conjecture,
( ~ c3_2(a558,X115)
| c4_2(a558,X115)
| c9_2(a558,X115) ) ).
cnf(u1557,negated_conjecture,
~ c9_1(a558) ).
cnf(u1561,negated_conjecture,
c4_1(a558) ).
cnf(u1586,negated_conjecture,
( ~ c8_2(a556,X113)
| c10_2(a556,X113)
| ~ c6_2(a556,X113) ) ).
cnf(u1593,negated_conjecture,
( ~ c6_2(a556,X112)
| c1_2(a556,X112)
| c5_2(a556,X112) ) ).
cnf(u1641,negated_conjecture,
( ~ c7_2(X108,a551)
| ~ c4_2(X108,a552)
| c5_2(X108,X109)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1645,negated_conjecture,
( ~ c7_2(X108,a551)
| ~ c10_2(X108,a552)
| c5_2(X108,X109)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1649,negated_conjecture,
( ~ c7_2(X108,a551)
| c3_2(X108,a552)
| c5_2(X108,X109)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1653,negated_conjecture,
( ~ c4_2(X108,a552)
| c5_2(X108,X109)
| c2_2(X108,a551)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1657,negated_conjecture,
( ~ c10_2(X108,a552)
| c5_2(X108,X109)
| c2_2(X108,a551)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1661,negated_conjecture,
( ~ c2_2(X108,X109)
| c3_2(X108,a552)
| c2_2(X108,a551)
| ~ ndr1_1(X108)
| c5_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1665,negated_conjecture,
( ~ c4_2(X108,a552)
| c5_2(X108,X109)
| c1_2(X108,a551)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1669,negated_conjecture,
( ~ c10_2(X108,a552)
| c5_2(X108,X109)
| c1_2(X108,a551)
| ~ ndr1_1(X108)
| ~ c2_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1673,negated_conjecture,
( ~ c2_2(X108,X109)
| c3_2(X108,a552)
| c1_2(X108,a551)
| ~ ndr1_1(X108)
| c5_2(X108,X109)
| c9_2(X108,X109) ) ).
cnf(u1677,negated_conjecture,
( ~ c2_2(X105,X107)
| ~ c8_2(X105,X107)
| ~ c8_1(X105)
| ~ c1_2(X105,X107)
| ~ ndr1_1(X105)
| ~ c6_2(X105,X106)
| c9_2(X105,X106) ) ).
cnf(u2551,negated_conjecture,
c4_0 ).
cnf(u1687,negated_conjecture,
( ~ c7_2(X101,a550)
| c3_1(X101)
| ~ ndr1_1(X101)
| ~ c9_2(X101,X102)
| ~ c10_2(X101,X102)
| c5_2(X101,X102) ) ).
cnf(u1691,negated_conjecture,
( ~ c5_2(X101,a550)
| c3_1(X101)
| ~ ndr1_1(X101)
| ~ c9_2(X101,X102)
| ~ c10_2(X101,X102)
| c5_2(X101,X102) ) ).
cnf(u1695,negated_conjecture,
( ~ c10_2(X101,a550)
| c3_1(X101)
| ~ ndr1_1(X101)
| ~ c9_2(X101,X102)
| ~ c10_2(X101,X102)
| c5_2(X101,X102) ) ).
cnf(u3473,negated_conjecture,
~ sP14 ).
cnf(u1707,negated_conjecture,
~ c8_1(a547) ).
cnf(u1710,negated_conjecture,
~ c3_0 ).
cnf(u1714,negated_conjecture,
~ c1_1(a547) ).
cnf(u1733,negated_conjecture,
c3_1(a546) ).
cnf(u1749,negated_conjecture,
( ~ c4_2(X94,X95)
| ~ ndr1_1(X94)
| ~ c9_2(X94,X95)
| c10_1(X94)
| c6_2(X94,X95)
| c3_1(X94) ) ).
cnf(u1756,negated_conjecture,
~ c1_1(a544) ).
cnf(u1759,negated_conjecture,
~ ndr1_1(a543) ).
cnf(u1765,negated_conjecture,
~ c2_0 ).
cnf(u1769,negated_conjecture,
c6_1(a544) ).
cnf(u1773,negated_conjecture,
c2_1(a544) ).
cnf(u1790,negated_conjecture,
~ ndr1_1(a542) ).
cnf(u1800,negated_conjecture,
~ c10_1(a542) ).
cnf(u1804,negated_conjecture,
( c10_2(X87,X88)
| ~ ndr1_1(X87)
| ~ c2_2(X87,X88)
| ~ c1_2(X87,X88)
| c3_1(X87) ) ).
cnf(u1811,negated_conjecture,
( c1_2(a541,X86)
| c9_2(a541,X86)
| c3_2(a541,X86) ) ).
cnf(u2743,negated_conjecture,
c10_0 ).
cnf(u1824,negated_conjecture,
~ c8_1(a541) ).
cnf(u1828,negated_conjecture,
~ c5_1(a541) ).
cnf(u1832,negated_conjecture,
~ c8_1(a540) ).
cnf(u1838,negated_conjecture,
~ c2_1(a540) ).
cnf(u1845,negated_conjecture,
~ c9_1(a539) ).
cnf(u1852,negated_conjecture,
c3_1(a539) ).
cnf(u1871,negated_conjecture,
( c9_1(X82)
| ~ ndr1_1(X82)
| ~ c7_2(X82,X83)
| ~ c1_2(X82,X83)
| c10_2(X82,X83)
| ~ c3_1(X82) ) ).
cnf(u1878,negated_conjecture,
~ c7_2(a536,a537) ).
cnf(u1882,negated_conjecture,
c2_2(a536,a537) ).
cnf(u1886,negated_conjecture,
c1_2(a536,a537) ).
cnf(u4698,negated_conjecture,
~ ndr1_1(a536) ).
cnf(u1894,negated_conjecture,
~ c6_1(a536) ).
cnf(u1898,negated_conjecture,
c10_1(a536) ).
cnf(u1903,negated_conjecture,
( ~ c9_2(X79,a535)
| c5_2(X79,X80)
| ~ c5_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1907,negated_conjecture,
( ~ c8_2(X79,a535)
| c5_2(X79,X80)
| ~ c5_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1911,negated_conjecture,
( ~ c5_2(X79,a534)
| ~ c4_2(X79,a535)
| c5_2(X79,X80)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1915,negated_conjecture,
( ~ c9_2(X79,a535)
| c5_2(X79,X80)
| ~ c4_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1919,negated_conjecture,
( ~ c8_2(X79,a535)
| c5_2(X79,X80)
| ~ c4_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1923,negated_conjecture,
( ~ c4_2(X79,a535)
| c5_2(X79,X80)
| ~ c4_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1927,negated_conjecture,
( ~ c9_2(X79,a535)
| c5_2(X79,X80)
| c8_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1931,negated_conjecture,
( ~ c8_2(X79,a535)
| c5_2(X79,X80)
| c8_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1935,negated_conjecture,
( ~ c4_2(X79,a535)
| c5_2(X79,X80)
| c8_2(X79,a534)
| ~ ndr1_1(X79)
| ~ c3_2(X79,X80) ) ).
cnf(u1939,negated_conjecture,
( c8_2(X78,a533)
| c7_1(X78) ) ).
cnf(u1943,negated_conjecture,
( c5_2(X78,a533)
| c7_1(X78) ) ).
cnf(u1947,negated_conjecture,
( c10_2(X78,a533)
| c7_1(X78) ) ).
cnf(u1951,negated_conjecture,
( c7_1(X78)
| ndr1_1(X78) ) ).
cnf(u3500,negated_conjecture,
~ sP15 ).
cnf(u1958,negated_conjecture,
( ~ c10_1(X77)
| ~ c10_2(X77,a530)
| ~ c1_1(X77) ) ).
cnf(u1961,negated_conjecture,
~ c1_0 ).
cnf(u1965,negated_conjecture,
( c8_2(X77,a530)
| ~ c1_1(X77)
| ~ c10_1(X77) ) ).
cnf(u1969,negated_conjecture,
( ~ c10_1(X77)
| ndr1_1(X77)
| ~ c1_1(X77) ) ).
cnf(u1973,negated_conjecture,
c9_2(a528,a529) ).
cnf(u1977,negated_conjecture,
c7_2(a528,a529) ).
cnf(u1981,negated_conjecture,
c4_2(a528,a529) ).
cnf(u1985,negated_conjecture,
ndr1_1(a528) ).
cnf(u1989,negated_conjecture,
c5_1(a528) ).
cnf(u1993,negated_conjecture,
c10_1(a528) ).
cnf(u1998,negated_conjecture,
~ c1_2(a526,a527) ).
cnf(u2002,negated_conjecture,
c9_2(a526,a527) ).
cnf(u2006,negated_conjecture,
ndr1_1(a526) ).
cnf(u2011,negated_conjecture,
( ~ c4_2(a526,X76)
| c9_2(a526,X76)
| ~ c2_2(a526,X76) ) ).
cnf(u2015,negated_conjecture,
( ~ c7_2(a526,X75)
| ~ c9_2(a526,X75)
| c8_2(a526,X75) ) ).
cnf(u2020,negated_conjecture,
sP16 ).
cnf(u2023,negated_conjecture,
( ~ c10_1(X74)
| ~ c2_2(X74,a523) ) ).
cnf(u2028,negated_conjecture,
( ~ c10_1(X74)
| ~ c10_2(X74,a523) ) ).
cnf(u2032,negated_conjecture,
( ~ c10_1(X74)
| c9_2(X74,a523) ) ).
cnf(u3546,negated_conjecture,
~ sP17 ).
cnf(u2043,negated_conjecture,
( ~ c2_2(X72,a520)
| ~ c1_1(X72)
| ~ ndr1_1(X72)
| ~ c3_2(X72,X73)
| c4_2(X72,X73)
| c1_2(X72,X73) ) ).
cnf(u2047,negated_conjecture,
( ~ c3_2(X72,X73)
| c8_2(X72,a520)
| ~ ndr1_1(X72)
| ~ c1_1(X72)
| c4_2(X72,X73)
| c1_2(X72,X73) ) ).
cnf(u2051,negated_conjecture,
( ~ c3_2(X71,a519)
| c9_1(X71)
| ~ c1_1(X71) ) ).
cnf(u2055,negated_conjecture,
( ~ c1_2(X71,a519)
| c9_1(X71)
| ~ c1_1(X71) ) ).
cnf(u2059,negated_conjecture,
( c2_2(X71,a519)
| c9_1(X71)
| ~ c1_1(X71) ) ).
cnf(u2067,negated_conjecture,
( ~ c9_1(X70)
| ~ c8_2(X70,a518)
| ~ c1_1(X70) ) ).
cnf(u2071,negated_conjecture,
( ~ c9_1(X70)
| c4_2(X70,a518)
| ~ c1_1(X70) ) ).
cnf(u2075,negated_conjecture,
( ~ c9_1(X70)
| c1_2(X70,a518)
| ~ c1_1(X70) ) ).
cnf(u2079,negated_conjecture,
( ~ c9_1(X70)
| ndr1_1(X70)
| ~ c1_1(X70) ) ).
cnf(u2083,negated_conjecture,
~ ndr1_1(a517) ).
cnf(u2095,negated_conjecture,
~ c4_1(a516) ).
cnf(u2102,negated_conjecture,
c7_1(a516) ).
cnf(u2106,negated_conjecture,
c2_1(a516) ).
cnf(u2122,negated_conjecture,
~ c8_1(a514) ).
cnf(u2129,negated_conjecture,
c10_1(a514) ).
cnf(u2133,negated_conjecture,
( ~ c9_1(X65)
| ~ c3_1(X65) ) ).
cnf(u2140,negated_conjecture,
( ~ c2_2(a513,X64)
| ~ c5_2(a513,X64)
| c8_2(a513,X64) ) ).
cnf(u2147,negated_conjecture,
c3_1(a513) ).
cnf(u2151,negated_conjecture,
c10_1(a513) ).
cnf(u2167,negated_conjecture,
( ~ c8_2(X60,a511)
| ~ c2_1(X60)
| ~ ndr1_1(X60)
| ~ c9_2(X60,X61)
| ~ c2_2(X60,X61)
| c8_2(X60,X61) ) ).
cnf(u2171,negated_conjecture,
( ~ c2_2(X60,X61)
| c4_2(X60,a511)
| ~ ndr1_1(X60)
| ~ c9_2(X60,X61)
| ~ c2_1(X60)
| c8_2(X60,X61) ) ).
cnf(u2175,negated_conjecture,
( ~ c2_2(X60,X61)
| c1_2(X60,a511)
| ~ ndr1_1(X60)
| ~ c9_2(X60,X61)
| ~ c2_1(X60)
| c8_2(X60,X61) ) ).
cnf(u2182,negated_conjecture,
( ~ c8_1(X58)
| ~ ndr1_1(X58)
| ~ c2_2(X58,X59)
| c4_2(X58,X59)
| c3_2(X58,X59)
| ~ c2_1(X58) ) ).
cnf(u3572,negated_conjecture,
~ sP18 ).
cnf(u2197,negated_conjecture,
( ~ c4_1(X57)
| ~ c5_2(X57,a507)
| c9_1(X57) ) ).
cnf(u2201,negated_conjecture,
( ~ c4_1(X57)
| ~ c2_2(X57,a507)
| c9_1(X57) ) ).
cnf(u2205,negated_conjecture,
( ~ c4_1(X57)
| c1_2(X57,a507)
| c9_1(X57) ) ).
cnf(u2209,negated_conjecture,
( ~ c4_1(X57)
| ndr1_1(X57)
| c9_1(X57) ) ).
cnf(u2213,negated_conjecture,
( ~ c8_2(X54,a506)
| c1_2(X54,X55)
| ~ c6_2(X54,X56)
| c3_2(X54,X56)
| c2_2(X54,X56)
| ~ ndr1_1(X54)
| ~ c7_2(X54,X55)
| c3_2(X54,X55) ) ).
cnf(u2220,negated_conjecture,
( ~ c1_2(X54,a506)
| c1_2(X54,X55)
| ~ c6_2(X54,X56)
| c3_2(X54,X56)
| c2_2(X54,X56)
| ~ ndr1_1(X54)
| ~ c7_2(X54,X55)
| c3_2(X54,X55) ) ).
cnf(u2224,negated_conjecture,
( ~ c6_2(X54,X56)
| c6_2(X54,a506)
| c1_2(X54,X55)
| c3_2(X54,X56)
| c2_2(X54,X56)
| ~ ndr1_1(X54)
| ~ c7_2(X54,X55)
| c3_2(X54,X55) ) ).
cnf(u2234,negated_conjecture,
( ~ c3_1(X51)
| c3_2(X51,a504)
| c2_1(X51) ) ).
cnf(u2238,negated_conjecture,
( ~ c3_1(X51)
| c2_2(X51,a504)
| c2_1(X51) ) ).
cnf(u2242,negated_conjecture,
( ~ c3_1(X51)
| ndr1_1(X51)
| c2_1(X51) ) ).
cnf(u2250,negated_conjecture,
( ~ c1_2(a503,X50)
| c8_2(a503,X50)
| c9_2(a503,X50) ) ).
cnf(u2254,negated_conjecture,
( ~ c7_2(a503,X49)
| c4_2(a503,X49)
| c9_2(a503,X49) ) ).
cnf(u2258,negated_conjecture,
~ c6_1(a503) ).
cnf(u2264,negated_conjecture,
~ c2_2(a501,a502) ).
cnf(u2269,negated_conjecture,
c9_2(a501,a502) ).
cnf(u2273,negated_conjecture,
c3_2(a501,a502) ).
cnf(u2277,negated_conjecture,
ndr1_1(a501) ).
cnf(u2282,negated_conjecture,
( ~ c7_2(a501,X48)
| c6_2(a501,X48)
| c9_2(a501,X48) ) ).
cnf(u2286,negated_conjecture,
( ~ c6_2(a501,X47)
| c3_2(a501,X47)
| ~ c1_2(a501,X47) ) ).
cnf(u2294,negated_conjecture,
~ c2_1(a499) ).
cnf(u2298,negated_conjecture,
c10_1(a500) ).
cnf(u2302,negated_conjecture,
c1_1(a499) ).
cnf(u2308,negated_conjecture,
~ c6_1(a498) ).
cnf(u3594,negated_conjecture,
~ sP19 ).
cnf(u2315,negated_conjecture,
~ c2_1(a498) ).
cnf(u2322,negated_conjecture,
( ~ c10_1(X44)
| ~ c1_1(X44) ) ).
cnf(u2361,negated_conjecture,
( ~ c5_2(a493,X43)
| c10_2(a493,X43)
| c3_2(a493,X43) ) ).
cnf(u2365,negated_conjecture,
c2_1(a493) ).
cnf(u3632,negated_conjecture,
~ sP20 ).
cnf(u2374,negated_conjecture,
~ c9_1(a490) ).
cnf(u2379,negated_conjecture,
c8_1(a490) ).
cnf(u2383,negated_conjecture,
c6_1(a490) ).
cnf(u2388,negated_conjecture,
~ ndr1_1(a489) ).
cnf(u2394,negated_conjecture,
( ~ c3_1(X41)
| c5_2(X41,a488)
| ~ c7_1(X41) ) ).
cnf(u2406,negated_conjecture,
( ~ c3_1(X41)
| c4_2(X41,a488)
| ~ c7_1(X41) ) ).
cnf(u2412,negated_conjecture,
( ~ c3_1(X41)
| c1_2(X41,a488)
| ~ c7_1(X41) ) ).
cnf(u2418,negated_conjecture,
( ~ c3_1(X41)
| ndr1_1(X41)
| ~ c7_1(X41) ) ).
cnf(u2424,negated_conjecture,
sP21 ).
cnf(u2427,negated_conjecture,
( c9_2(X40,a484)
| c2_1(X40) ) ).
cnf(u2443,negated_conjecture,
~ c3_1(a483) ).
cnf(u2452,negated_conjecture,
~ c5_1(a482) ).
cnf(u2456,negated_conjecture,
c2_1(a482) ).
cnf(u2461,negated_conjecture,
~ c4_2(a479,a481) ).
cnf(u2465,negated_conjecture,
c8_2(a479,a481) ).
cnf(u2469,negated_conjecture,
c5_2(a479,a481) ).
cnf(u2473,negated_conjecture,
ndr1_1(a479) ).
cnf(u2477,negated_conjecture,
c9_2(a479,a480) ).
cnf(u2481,negated_conjecture,
c10_2(a479,a480) ).
cnf(u2487,negated_conjecture,
( ~ c7_2(X39,a478)
| c10_1(X39)
| c2_1(X39) ) ).
cnf(u2491,negated_conjecture,
( ~ c4_2(X39,a478)
| c10_1(X39)
| c2_1(X39) ) ).
cnf(u2503,negated_conjecture,
~ c3_1(a477) ).
cnf(u2507,negated_conjecture,
~ c10_1(a477) ).
cnf(u2516,negated_conjecture,
( ~ c7_2(X38,a475)
| ~ c4_2(X38,a476)
| ~ c2_1(X38) ) ).
cnf(u2520,negated_conjecture,
( ~ c7_2(X38,a475)
| ~ c10_2(X38,a476)
| ~ c2_1(X38) ) ).
cnf(u2524,negated_conjecture,
( ~ c7_2(X38,a475)
| c2_2(X38,a476)
| ~ c2_1(X38) ) ).
cnf(u2528,negated_conjecture,
( ~ c4_2(X38,a476)
| ~ c2_1(X38)
| c1_2(X38,a475) ) ).
cnf(u2532,negated_conjecture,
( ~ c10_2(X38,a476)
| ~ c2_1(X38)
| c1_2(X38,a475) ) ).
cnf(u2536,negated_conjecture,
( c1_2(X38,a475)
| c2_2(X38,a476)
| ~ c2_1(X38) ) ).
cnf(u2540,negated_conjecture,
( ~ c2_1(X38)
| ndr1_1(X38) ) ).
cnf(u2547,negated_conjecture,
( ~ c3_2(a474,X37)
| c10_2(a474,X37)
| c4_2(a474,X37) ) ).
cnf(u3692,negated_conjecture,
~ sP22 ).
cnf(u2555,negated_conjecture,
~ c8_1(a474) ).
cnf(u2559,negated_conjecture,
c10_1(a474) ).
cnf(u2563,negated_conjecture,
( ~ c4_2(X34,X36)
| c6_1(X34)
| c8_2(X34,X36)
| c6_2(X34,X36)
| ~ ndr1_1(X34)
| c9_2(X34,X35)
| c5_2(X34,X35)
| c4_2(X34,X35) ) ).
cnf(u2571,negated_conjecture,
c8_2(a470,a471) ).
cnf(u2575,negated_conjecture,
c7_2(a470,a471) ).
cnf(u2579,negated_conjecture,
ndr1_1(a470) ).
cnf(u2584,negated_conjecture,
( ~ c4_2(a470,X31)
| c3_2(a470,X31)
| c7_2(a470,X31) ) ).
cnf(u2588,negated_conjecture,
c8_1(a470) ).
cnf(u2622,negated_conjecture,
( ~ c3_2(X28,X29)
| ~ ndr1_1(X28)
| ~ c7_1(X28)
| c5_2(X28,X29)
| ~ c8_1(X28) ) ).
cnf(u2635,negated_conjecture,
~ c1_2(a465,a466) ).
cnf(u2639,negated_conjecture,
c6_2(a465,a466) ).
cnf(u2643,negated_conjecture,
c2_2(a465,a466) ).
cnf(u2647,negated_conjecture,
ndr1_1(a465) ).
cnf(u2652,negated_conjecture,
( ~ c3_2(a465,X27)
| ~ c4_2(a465,X27)
| c8_2(a465,X27) ) ).
cnf(u2656,negated_conjecture,
~ c10_1(a465) ).
cnf(u2662,negated_conjecture,
( ~ c6_2(X25,a464)
| c6_1(X25)
| ~ ndr1_1(X25)
| ~ c6_2(X25,X26)
| ~ c3_2(X25,X26)
| c8_2(X25,X26) ) ).
cnf(u2666,negated_conjecture,
( ~ c6_2(X25,X26)
| c7_2(X25,a464)
| ~ ndr1_1(X25)
| c6_1(X25)
| ~ c3_2(X25,X26)
| c8_2(X25,X26) ) ).
cnf(u2670,negated_conjecture,
( ~ c6_2(X25,X26)
| c3_2(X25,a464)
| ~ ndr1_1(X25)
| c6_1(X25)
| ~ c3_2(X25,X26)
| c8_2(X25,X26) ) ).
cnf(u2682,negated_conjecture,
( ~ c5_2(X19,a463)
| c4_1(X19)
| ~ ndr1_1(X19)
| ~ c3_2(X19,X20)
| ~ c1_2(X19,X20)
| c9_2(X19,X20) ) ).
cnf(u2686,negated_conjecture,
( ~ c2_2(X19,a463)
| c4_1(X19)
| ~ ndr1_1(X19)
| ~ c3_2(X19,X20)
| ~ c1_2(X19,X20)
| c9_2(X19,X20) ) ).
cnf(u2690,negated_conjecture,
( ~ c3_2(X19,X20)
| c7_2(X19,a463)
| ~ ndr1_1(X19)
| c4_1(X19)
| ~ c1_2(X19,X20)
| c9_2(X19,X20) ) ).
cnf(u2729,negated_conjecture,
~ c5_1(a460) ).
cnf(u2733,negated_conjecture,
c2_1(a460) ).
cnf(u2737,negated_conjecture,
c1_1(a460) ).
cnf(u2742,negated_conjecture,
~ c4_2(a457,a459) ).
cnf(u2747,negated_conjecture,
~ c2_2(a457,a459) ).
cnf(u2751,negated_conjecture,
c10_2(a457,a459) ).
cnf(u2755,negated_conjecture,
ndr1_1(a457) ).
cnf(u2759,negated_conjecture,
~ c8_2(a457,a458) ).
cnf(u2763,negated_conjecture,
c1_2(a457,a458) ).
cnf(u2769,negated_conjecture,
~ c4_2(a455,a456) ).
cnf(u2773,negated_conjecture,
~ c2_2(a455,a456) ).
cnf(u2777,negated_conjecture,
c8_2(a455,a456) ).
cnf(u2781,negated_conjecture,
ndr1_1(a455) ).
cnf(u2786,negated_conjecture,
( ~ c1_2(a455,X15)
| c3_2(a455,X15)
| c9_2(a455,X15) ) ).
cnf(u2790,negated_conjecture,
( ~ c1_2(a455,X14)
| c3_2(a455,X14)
| c8_2(a455,X14) ) ).
cnf(u2795,negated_conjecture,
~ c5_2(a453,a454) ).
cnf(u2799,negated_conjecture,
~ c2_2(a453,a454) ).
cnf(u2803,negated_conjecture,
c7_2(a453,a454) ).
cnf(u2807,negated_conjecture,
ndr1_1(a453) ).
cnf(u2812,negated_conjecture,
( ~ c5_2(a453,X13)
| ~ c10_2(a453,X13)
| ~ c4_2(a453,X13) ) ).
cnf(u2816,negated_conjecture,
c8_1(a453) ).
cnf(u2821,negated_conjecture,
~ c9_2(a451,a452) ).
cnf(u3730,negated_conjecture,
~ sP23 ).
cnf(u2828,negated_conjecture,
~ c6_2(a451,a452) ).
cnf(u2832,negated_conjecture,
c5_2(a451,a452) ).
cnf(u2836,negated_conjecture,
ndr1_1(a451) ).
cnf(u2840,negated_conjecture,
~ c6_1(a451) ).
cnf(u2845,negated_conjecture,
( c2_1(X12)
| ~ c3_1(X12)
| c9_1(X12) ) ).
cnf(u2849,negated_conjecture,
~ ndr1_1(a448) ).
cnf(u3757,negated_conjecture,
~ sP24 ).
cnf(u2863,negated_conjecture,
~ c9_1(a448) ).
cnf(u2867,negated_conjecture,
( ~ c9_1(X8)
| ~ ndr1_1(X8)
| c9_2(X8,X9)
| c4_2(X8,X9)
| c2_2(X8,X9)
| c1_1(X8) ) ).
cnf(u2871,negated_conjecture,
~ c8_2(a443,a445) ).
cnf(u2875,negated_conjecture,
~ c10_2(a443,a445) ).
cnf(u6402,negated_conjecture,
~ c5_2(a443,a445) ).
cnf(u2883,negated_conjecture,
ndr1_1(a443) ).
cnf(u2887,negated_conjecture,
~ c4_2(a443,a444) ).
cnf(u2891,negated_conjecture,
c1_2(a443,a444) ).
cnf(u2901,negated_conjecture,
( ~ c7_2(X7,a442)
| ~ c5_1(X7) ) ).
cnf(u2905,negated_conjecture,
( ~ c5_1(X7)
| c5_2(X7,a442) ) ).
cnf(u2909,negated_conjecture,
( c10_2(X7,a442)
| ~ c5_1(X7) ) ).
cnf(u2913,negated_conjecture,
( ~ c5_1(X7)
| ndr1_1(X7) ) ).
cnf(u2987,negated_conjecture,
~ c9_1(a436) ).
cnf(u3798,negated_conjecture,
~ sP25 ).
cnf(u2995,negated_conjecture,
~ c3_1(a436) ).
cnf(u2999,negated_conjecture,
c7_1(a436) ).
cnf(u3025,negated_conjecture,
( ~ c10_2(X0,a431)
| c5_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3029,negated_conjecture,
( ~ c10_2(X0,a431)
| c4_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3033,negated_conjecture,
( c10_2(X0,a432)
| ~ c2_1(X0)
| ~ c10_2(X0,a431) ) ).
cnf(u3037,negated_conjecture,
( c6_2(X0,a431)
| c5_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3041,negated_conjecture,
( c6_2(X0,a431)
| c4_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3045,negated_conjecture,
( c6_2(X0,a431)
| c10_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3049,negated_conjecture,
( c1_2(X0,a431)
| c5_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3053,negated_conjecture,
( c1_2(X0,a431)
| c4_2(X0,a432)
| ~ c2_1(X0) ) ).
cnf(u3057,negated_conjecture,
( c10_2(X0,a432)
| ~ c2_1(X0)
| c1_2(X0,a431) ) ).
cnf(u3116,axiom,
~ ndr1_1(a609) ).
cnf(u3127,axiom,
~ c3_1(a609) ).
cnf(u3403,axiom,
~ c7_2(a568,a570) ).
cnf(u3407,axiom,
c8_2(a568,a570) ).
cnf(u3411,axiom,
c5_2(a568,a570) ).
cnf(u3415,axiom,
ndr1_1(a568) ).
cnf(u3419,axiom,
c9_2(a568,a569) ).
cnf(u3423,axiom,
c3_2(a568,a569) ).
cnf(u3427,axiom,
c10_2(a568,a569) ).
cnf(u3432,axiom,
~ c7_1(a568) ).
cnf(u3528,axiom,
~ c4_2(a524,a525) ).
cnf(u3532,axiom,
c7_2(a524,a525) ).
cnf(u3536,axiom,
c3_2(a524,a525) ).
cnf(u3540,axiom,
ndr1_1(a524) ).
cnf(u3544,axiom,
c3_1(a524) ).
cnf(u3661,axiom,
~ c8_2(a485,a487) ).
cnf(u3665,axiom,
~ c3_2(a485,a487) ).
cnf(u3669,axiom,
~ c2_2(a485,a487) ).
cnf(u3673,axiom,
ndr1_1(a485) ).
cnf(u3677,axiom,
~ c6_2(a485,a486) ).
cnf(u3681,axiom,
c7_2(a485,a486) ).
cnf(u3685,axiom,
c5_2(a485,a486) ).
cnf(u3690,axiom,
c1_1(a485) ).
cnf(u3834,negated_conjecture,
~ c5_2(a479,a480) ).
cnf(u3852,negated_conjecture,
~ c5_2(a528,a529) ).
cnf(u3855,negated_conjecture,
~ c8_2(a528,a529) ).
cnf(u3869,negated_conjecture,
~ c2_1(a455) ).
cnf(u3898,negated_conjecture,
~ c1_1(a528) ).
cnf(u3971,negated_conjecture,
c2_1(a436) ).
cnf(u5651,negated_conjecture,
~ c2_1(a566) ).
cnf(u3986,negated_conjecture,
~ c10_2(a566,a478) ).
cnf(u3998,negated_conjecture,
~ c5_2(a501,a502) ).
cnf(u4014,negated_conjecture,
~ c2_1(a503) ).
cnf(u4029,negated_conjecture,
~ c8_1(a501) ).
cnf(u4042,negated_conjecture,
~ c1_1(a474) ).
cnf(u4056,negated_conjecture,
c5_2(a556,a478) ).
cnf(u4068,negated_conjecture,
~ c1_1(a541) ).
cnf(u5389,negated_conjecture,
~ c2_1(a501) ).
cnf(u4095,negated_conjecture,
~ c1_2(a501,a478) ).
cnf(u4109,negated_conjecture,
~ c2_1(a470) ).
cnf(u4116,negated_conjecture,
~ c2_1(a453) ).
cnf(u4123,negated_conjecture,
~ c2_1(a490) ).
cnf(u4154,negated_conjecture,
~ c5_2(a568,a569) ).
cnf(u4170,negated_conjecture,
~ c5_2(a526,a527) ).
cnf(u4191,negated_conjecture,
( ~ c6_2(a541,X1)
| c2_2(a541,X1)
| c3_2(a541,X1) ) ).
cnf(u4208,negated_conjecture,
~ c1_1(a568) ).
cnf(u4221,negated_conjecture,
~ c1_1(a501) ).
cnf(u4236,negated_conjecture,
~ c1_1(a477) ).
cnf(u4273,negated_conjecture,
( ~ c5_2(a528,X1)
| c10_2(a528,X1)
| ~ c6_2(a528,X1) ) ).
cnf(u4291,negated_conjecture,
~ c2_1(a536) ).
cnf(u5046,negated_conjecture,
~ c8_2(a465,a466) ).
cnf(u4304,negated_conjecture,
~ c2_1(a465) ).
cnf(u4684,negated_conjecture,
c9_2(a465,a466) ).
cnf(u4336,negated_conjecture,
~ c8_1(a477) ).
cnf(u4387,negated_conjecture,
c3_2(a470,a484) ).
cnf(u4423,negated_conjecture,
~ c5_2(a514,a523) ).
cnf(u4438,negated_conjecture,
~ c5_2(a474,a523) ).
cnf(u4501,negated_conjecture,
~ c5_2(a564,a523) ).
cnf(u4516,negated_conjecture,
~ c1_1(a609) ).
cnf(u4528,negated_conjecture,
~ c5_2(a500,a523) ).
cnf(u5380,negated_conjecture,
~ c2_1(a541) ).
cnf(u4545,negated_conjecture,
c3_2(a541,a478) ).
cnf(u4584,negated_conjecture,
c1_2(a465,a551) ).
cnf(u4650,negated_conjecture,
~ c1_2(a541,a478) ).
cnf(u4666,negated_conjecture,
c2_2(a536,a551) ).
cnf(u4671,negated_conjecture,
c2_2(a465,a551) ).
cnf(u4710,negated_conjecture,
~ c1_2(a524,a525) ).
cnf(u4721,negated_conjecture,
~ c1_1(a524) ).
cnf(u4731,negated_conjecture,
~ c4_2(a453,a533) ).
cnf(u4744,negated_conjecture,
c2_1(a524) ).
cnf(u4766,negated_conjecture,
( ~ c4_2(a558,X1)
| c8_2(a558,X1)
| ~ c10_2(a558,X1) ) ).
cnf(u4785,negated_conjecture,
~ c9_2(a564,a565) ).
cnf(u5817,negated_conjecture,
~ c7_1(a485) ).
cnf(u6262,negated_conjecture,
~ c7_1(a479) ).
cnf(u4883,negated_conjecture,
~ c8_1(a524) ).
cnf(u4889,negated_conjecture,
~ c7_1(a524) ).
cnf(u4896,negated_conjecture,
~ c3_2(a465,a466) ).
cnf(u4932,negated_conjecture,
c6_2(a564,a565) ).
cnf(u4944,negated_conjecture,
c6_2(a528,a529) ).
cnf(u5115,negated_conjecture,
~ c10_2(a558,a484) ).
cnf(u5141,negated_conjecture,
~ c3_2(a528,a529) ).
cnf(u5134,negated_conjecture,
( ~ c7_2(a528,X0)
| c3_2(a528,X0)
| c1_2(a528,X0) ) ).
cnf(u5171,negated_conjecture,
~ c3_2(a564,a565) ).
cnf(u5166,negated_conjecture,
( ~ c7_2(a564,X0)
| c3_2(a564,X0)
| c1_2(a564,X0) ) ).
cnf(u5210,negated_conjecture,
c6_1(a524) ).
cnf(u5223,negated_conjecture,
c6_2(a524,a506) ).
cnf(u5256,negated_conjecture,
( ~ c7_2(a539,X0)
| c10_2(a539,X0)
| ~ c1_2(a539,X0) ) ).
cnf(u5260,negated_conjecture,
~ c7_1(a539) ).
cnf(u5276,negated_conjecture,
c8_1(a539) ).
cnf(u5285,negated_conjecture,
~ c5_2(a528,a523) ).
cnf(u5303,negated_conjecture,
~ c6_2(a528,a484) ).
cnf(u5311,negated_conjecture,
~ c1_1(a483) ).
cnf(u5335,negated_conjecture,
~ c8_2(a465,a551) ).
cnf(u6319,negated_conjecture,
~ c9_2(a465,a551) ).
cnf(u5359,negated_conjecture,
~ c1_1(a539) ).
cnf(u5427,negated_conjecture,
~ c7_1(a546) ).
cnf(u5443,negated_conjecture,
c8_1(a546) ).
cnf(u5467,negated_conjecture,
~ c1_1(a546) ).
cnf(u5548,negated_conjecture,
c3_2(a485,a552) ).
cnf(u6756,negated_conjecture,
~ c9_2(a485,a519) ).
cnf(u5557,negated_conjecture,
c5_2(a485,a519) ).
cnf(u5576,negated_conjecture,
c2_2(a460,a551) ).
cnf(u5621,negated_conjecture,
c2_2(a566,a478) ).
cnf(u5629,negated_conjecture,
~ c1_2(a566,a478) ).
cnf(u5637,negated_conjecture,
~ c5_2(a566,a478) ).
cnf(u5665,negated_conjecture,
c9_2(a566,a478) ).
cnf(u5695,negated_conjecture,
~ c1_1(a595) ).
cnf(u5716,negated_conjecture,
~ c7_1(a513) ).
cnf(u5734,negated_conjecture,
~ c5_2(a513,a523) ).
cnf(u5746,negated_conjecture,
c8_1(a513) ).
cnf(u5760,negated_conjecture,
~ c6_2(a528,a442) ).
cnf(u5773,negated_conjecture,
~ ndr1_1(a610) ).
cnf(u5777,negated_conjecture,
~ ndr1_1(a574) ).
cnf(u5781,negated_conjecture,
~ ndr1_1(a571) ).
cnf(u5785,negated_conjecture,
~ ndr1_1(a499) ).
cnf(u5803,negated_conjecture,
~ c1_2(a485,a552) ).
cnf(u5825,negated_conjecture,
c8_2(a485,a520) ).
cnf(u5852,negated_conjecture,
~ c9_2(a460,a518) ).
cnf(u5859,negated_conjecture,
c6_1(a460) ).
cnf(u6098,negated_conjecture,
~ c3_2(a556,a478) ).
cnf(u5949,negated_conjecture,
~ c9_2(a556,a478) ).
cnf(u5973,negated_conjecture,
~ c9_2(a568,a570) ).
cnf(u5992,negated_conjecture,
~ c9_2(a485,a486) ).
cnf(u6008,negated_conjecture,
c3_1(a479) ).
cnf(u6011,negated_conjecture,
~ c9_2(a479,a481) ).
cnf(u6015,negated_conjecture,
c10_1(a443) ).
cnf(u6030,negated_conjecture,
~ c9_2(a443,a445) ).
cnf(u6044,negated_conjecture,
~ c1_1(a503) ).
cnf(u6068,negated_conjecture,
~ c1_1(a455) ).
cnf(u6143,negated_conjecture,
~ c9_2(a457,a459) ).
cnf(u6149,negated_conjecture,
c2_2(a568,a550) ).
cnf(u6200,negated_conjecture,
~ c9_2(a568,a550) ).
cnf(u6191,negated_conjecture,
c1_2(a568,a551) ).
cnf(u6195,negated_conjecture,
c2_2(a568,a551) ).
cnf(u6199,negated_conjecture,
~ c2_1(a568) ).
cnf(u6214,negated_conjecture,
~ c1_2(a568,a550) ).
cnf(u6217,negated_conjecture,
~ c8_1(a568) ).
cnf(u6278,negated_conjecture,
c8_1(a479) ).
cnf(u6290,negated_conjecture,
~ c1_1(a479) ).
cnf(u6328,negated_conjecture,
c7_2(a541,a464) ).
cnf(u6353,negated_conjecture,
~ c2_1(a610) ).
cnf(u6360,negated_conjecture,
~ c2_1(a571) ).
cnf(u6367,negated_conjecture,
~ c2_1(a485) ).
cnf(u6393,negated_conjecture,
~ c2_2(a443,a445) ).
cnf(u6417,negated_conjecture,
~ c5_2(a443,a523) ).
cnf(u6438,negated_conjecture,
( c6_2(a460,X0)
| c8_2(a460,X0)
| c4_2(a460,X0) ) ).
cnf(u6449,negated_conjecture,
( ~ c7_2(a460,X1)
| c3_2(a460,X1)
| c1_2(a460,X1) ) ).
cnf(u6460,negated_conjecture,
~ c1_1(a619) ).
cnf(u6565,negated_conjecture,
c3_2(a503,a484) ).
cnf(u6577,negated_conjecture,
c2_2(a455,a552) ).
cnf(u6589,negated_conjecture,
c3_2(a455,a484) ).
cnf(u6616,negated_conjecture,
~ c1_2(a455,a552) ).
cnf(u6625,negated_conjecture,
c5_2(a455,a552) ).
cnf(u6631,negated_conjecture,
~ c9_2(a455,a552) ).
cnf(u6638,negated_conjecture,
~ c8_1(a455) ).
cnf(u6652,negated_conjecture,
( ~ c2_2(a455,X0)
| c5_2(a455,X0)
| c9_2(a455,X0) ) ).
cnf(u6693,negated_conjecture,
~ c1_2(a503,a484) ).
cnf(u6709,negated_conjecture,
~ c7_1(a503) ).
cnf(u6721,negated_conjecture,
~ c1_2(a455,a484) ).
cnf(u6858,negated_conjecture,
c2_2(a526,a527) ).
cnf(u6877,negated_conjecture,
c2_2(a501,a550) ).
cnf(u6907,negated_conjecture,
c9_2(a501,a550) ).
cnf(u6983,negated_conjecture,
~ c5_2(a501,a550) ).
cnf(u6926,negated_conjecture,
~ c1_2(a501,a550) ).
cnf(u6964,negated_conjecture,
~ c2_1(a526) ).
cnf(u7008,negated_conjecture,
~ c1_2(a470,a484) ).
cnf(u7000,negated_conjecture,
~ c1_1(a470) ).
cnf(u7022,negated_conjecture,
~ c7_1(a470) ).
cnf(u7049,negated_conjecture,
~ c2_2(a453,a484) ).
cnf(u7066,negated_conjecture,
~ c4_2(a453,a484) ).
cnf(u7097,negated_conjecture,
~ c1_1(a516) ).
cnf(u7257,negated_conjecture,
( ~ c7_2(a546,X0)
| c5_2(a546,X0)
| c6_2(a546,X0) ) ).
cnf(u7264,negated_conjecture,
( ~ c7_2(a539,X0)
| c5_2(a539,X0)
| c6_2(a539,X0) ) ).
cnf(u7271,negated_conjecture,
( ~ c7_2(a524,X0)
| c5_2(a524,X0)
| c6_2(a524,X0) ) ).
cnf(u7278,negated_conjecture,
( ~ c7_2(a513,X0)
| c5_2(a513,X0)
| c6_2(a513,X0) ) ).
cnf(u7285,negated_conjecture,
( ~ c7_2(a479,X0)
| c5_2(a479,X0)
| c6_2(a479,X0) ) ).
cnf(u7293,negated_conjecture,
c6_2(a524,a525) ).
cnf(u7316,negated_conjecture,
~ c1_1(a493) ).
cnf(u7331,negated_conjecture,
c4_2(a460,a583) ).
cnf(u7349,negated_conjecture,
~ c9_2(a460,a583) ).
cnf(u7371,negated_conjecture,
c10_2(a460,a583) ).
cnf(u7414,negated_conjecture,
c1_2(a460,a551) ).
cnf(u7406,negated_conjecture,
~ c8_2(a460,a551) ).
cnf(u7417,negated_conjecture,
~ c9_2(a460,a551) ).
cnf(u7435,negated_conjecture,
~ c1_2(a558,a484) ).
cnf(u7445,negated_conjecture,
~ c5_2(a558,a484) ).
cnf(u6258,negated_conjecture,
c2_1(a479) ).
cnf(u4278,negated_conjecture,
( ~ c8_2(X0,a484)
| c10_2(X0,X1)
| c2_1(X0)
| ~ c5_2(X0,a484)
| ~ c8_2(X0,X2)
| ~ c4_2(X0,X2)
| c9_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5457,negated_conjecture,
( ~ c3_2(X0,a431)
| ~ c2_1(X0)
| c7_2(X0,a464)
| c6_1(X0)
| c5_2(X0,a432)
| c8_2(X0,a431) ) ).
cnf(u7245,negated_conjecture,
( ~ c3_1(X145)
| c4_2(X145,a583)
| ~ c7_2(X145,X146)
| c6_2(X145,X146)
| c5_2(X145,X146) ) ).
cnf(u4413,negated_conjecture,
~ c1_1(a500) ).
cnf(u5184,negated_conjecture,
( ~ c2_2(X0,a552)
| c2_2(X0,a551)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c9_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_2(X0,a552)
| c3_1(X0) ) ).
cnf(u5348,negated_conjecture,
c9_2(a513,a523) ).
cnf(u5402,negated_conjecture,
( ~ c3_2(X0,a431)
| ~ c2_1(X0)
| c7_2(X0,a464)
| c6_1(X0)
| c10_2(X0,a432)
| c8_2(X0,a431) ) ).
cnf(u4362,negated_conjecture,
~ c10_2(a514,a523) ).
cnf(u5349,negated_conjecture,
~ c1_1(a513) ).
cnf(u5316,negated_conjecture,
ndr1_1(a603) ).
cnf(u7025,negated_conjecture,
ndr1_1(a474) ).
cnf(u5193,negated_conjecture,
( ~ c5_2(X0,a552)
| c1_2(X0,a551)
| ~ c2_2(X0,X1)
| c9_2(X0,X1)
| c8_2(X0,a559)
| c5_2(X0,X1)
| c7_1(X0) ) ).
cnf(u7244,negated_conjecture,
( ~ c6_2(X145,a583)
| ~ c3_1(X145)
| ~ c7_2(X145,X146)
| c6_2(X145,X146)
| c5_2(X145,X146) ) ).
cnf(u5346,negated_conjecture,
~ c2_2(a513,a523) ).
cnf(u4374,negated_conjecture,
( ~ c2_2(X0,a550)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c10_2(X0,X1)
| c5_2(X0,X1)
| c3_1(X0)
| ~ c1_2(X0,a550) ) ).
cnf(u7321,negated_conjecture,
ndr1_1(a514) ).
cnf(u7249,negated_conjecture,
( ~ c1_1(X0)
| ~ c7_2(X0,X1)
| c6_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_1(X0)
| c4_2(X0,a583) ) ).
cnf(u6261,negated_conjecture,
( ~ c7_2(a479,X0)
| ~ c1_2(a479,X0)
| c10_2(a479,X0) ) ).
cnf(u6380,negated_conjecture,
( ~ c2_2(X0,a431)
| ~ c2_1(X0)
| c5_2(X0,a432)
| c3_1(X0) ) ).
cnf(u6409,negated_conjecture,
~ c1_1(a443) ).
cnf(u4911,negated_conjecture,
( c6_2(a524,X0)
| c8_2(a524,X0)
| c4_2(a524,X0) ) ).
cnf(u6407,negated_conjecture,
~ c10_2(a443,a523) ).
cnf(u4633,negated_conjecture,
( ~ c5_2(X0,a590)
| ~ ndr1_1(X0)
| c8_2(X0,a559)
| c7_1(X0)
| c3_1(X0)
| ~ c9_2(X0,X1)
| ~ c5_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u4910,negated_conjecture,
( ~ c1_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c8_2(X0,X1) ) ).
cnf(u4363,negated_conjecture,
c9_2(a514,a523) ).
cnf(u4404,negated_conjecture,
c9_2(a536,a523) ).
cnf(u4673,negated_conjecture,
( c1_2(X0,a551)
| c3_2(X0,a552)
| ~ ndr1_1(X0)
| c5_2(X0,a519)
| c9_2(X0,a519)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u5318,negated_conjecture,
~ c1_1(a436) ).
cnf(u4593,negated_conjecture,
( ~ c9_2(X0,a519)
| c4_2(X0,a511)
| ~ c2_1(X0)
| c8_2(X0,a519)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u7246,negated_conjecture,
( ~ c3_1(X145)
| c10_2(X145,a583)
| ~ c7_2(X145,X146)
| c6_2(X145,X146)
| c5_2(X145,X146) ) ).
cnf(u6465,negated_conjecture,
ndr1_1(a477) ).
cnf(u5372,negated_conjecture,
( ~ c3_2(X0,a431)
| ~ c2_1(X0)
| c7_2(X0,a464)
| c6_1(X0)
| c4_2(X0,a432)
| c8_2(X0,a431) ) ).
cnf(u5462,negated_conjecture,
( ~ c2_2(a546,X0)
| c4_2(a546,X0)
| c3_2(a546,X0) ) ).
cnf(u4920,negated_conjecture,
( ~ c7_2(a524,X0)
| ~ c1_2(a524,X0)
| c10_2(a524,X0) ) ).
cnf(u3826,negated_conjecture,
( ~ c3_1(X12)
| c2_1(X12) ) ).
cnf(u5191,negated_conjecture,
( ~ c2_2(X0,a552)
| c1_2(X0,a551)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c9_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_2(X0,a552)
| c3_1(X0) ) ).
cnf(u5107,negated_conjecture,
( ~ c7_1(X0)
| c4_2(X0,a488)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u6285,negated_conjecture,
( ~ c2_2(a479,X0)
| c4_2(a479,X0)
| c3_2(a479,X0) ) ).
cnf(u4627,negated_conjecture,
ndr1_1(a544) ).
cnf(u4598,negated_conjecture,
( ~ c1_2(X0,a476)
| c1_2(X0,a475)
| ~ c2_1(X0)
| c3_1(X0) ) ).
cnf(u4622,negated_conjecture,
ndr1_1(a436) ).
cnf(u6372,negated_conjecture,
( ~ c7_2(a460,X0)
| c10_2(a460,X0)
| ~ c1_2(a460,X0) ) ).
cnf(u4322,negated_conjecture,
( ~ c2_2(X0,a590)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c5_2(X0,X1)
| c3_2(X0,X1)
| c3_1(X0)
| ~ c1_2(X0,a590) ) ).
cnf(u5347,negated_conjecture,
~ c10_2(a513,a523) ).
cnf(u4595,negated_conjecture,
( ~ c9_2(X0,a519)
| c1_2(X0,a511)
| ~ c2_1(X0)
| c8_2(X0,a519)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u4634,negated_conjecture,
( ~ c5_2(X0,a476)
| c8_2(X0,a559)
| c7_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a475) ) ).
cnf(u4395,negated_conjecture,
c1_2(a558,a507) ).
cnf(u3879,negated_conjecture,
c9_2(a528,a523) ).
cnf(u5353,negated_conjecture,
( ~ c2_2(a539,X0)
| c4_2(a539,X0)
| c3_2(a539,X0) ) ).
cnf(u5401,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c2_1(X0)
| c6_2(X0,a506)
| c1_2(X0,X1)
| c3_2(X0,a431)
| c2_2(X0,a431)
| c10_2(X0,a432)
| c3_2(X0,X1) ) ).
cnf(u4921,negated_conjecture,
( ~ c1_1(X0)
| ~ c1_2(X0,X1)
| c10_2(X0,X1)
| ~ c2_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u6408,negated_conjecture,
c9_2(a443,a523) ).
cnf(u3844,negated_conjecture,
c5_2(a528,a442) ).
cnf(u5292,negated_conjecture,
ndr1_1(a539) ).
cnf(u5708,negated_conjecture,
c2_1(a513) ).
cnf(u4658,negated_conjecture,
( ~ c1_1(X0)
| c2_2(X0,a551)
| ~ ndr1_1(X0)
| c5_2(X0,a519)
| c9_2(X0,a519)
| c9_1(X0)
| c3_2(X0,a552) ) ).
cnf(u5373,negated_conjecture,
( ~ c3_2(X0,a431)
| ~ c2_1(X0)
| c3_2(X0,a464)
| c6_1(X0)
| c4_2(X0,a432)
| c8_2(X0,a431) ) ).
cnf(u4037,negated_conjecture,
c9_2(a474,a523) ).
cnf(u4696,negated_conjecture,
( ~ c3_1(X41)
| ndr1_1(X41) ) ).
cnf(u4034,negated_conjecture,
~ c10_2(a474,a523) ).
cnf(u4365,negated_conjecture,
~ c1_1(a514) ).
cnf(u5710,negated_conjecture,
ndr1_1(a513) ).
cnf(u3965,negated_conjecture,
~ c2_2(a564,a523) ).
cnf(u4361,negated_conjecture,
~ c2_2(a514,a523) ).
cnf(u4624,negated_conjecture,
ndr1_1(a482) ).
cnf(u4411,negated_conjecture,
c9_2(a500,a523) ).
cnf(u4803,negated_conjecture,
ndr1_1(a547) ).
cnf(u4406,negated_conjecture,
~ c1_1(a536) ).
cnf(u5424,negated_conjecture,
( ~ c7_2(a546,X0)
| ~ c1_2(a546,X0)
| c10_2(a546,X0) ) ).
cnf(u6379,negated_conjecture,
( ~ c5_2(X0,a431)
| ~ c2_1(X0)
| c8_2(X0,a559)
| c5_2(X0,a432)
| c7_1(X0) ) ).
cnf(u4403,negated_conjecture,
~ c10_2(a536,a523) ).
cnf(u4912,negated_conjecture,
( c5_2(X0,a488)
| ~ c7_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u3842,negated_conjecture,
~ c2_2(a528,a523) ).
cnf(u5421,negated_conjecture,
c2_1(a546) ).
cnf(u5403,negated_conjecture,
( ~ c3_2(X0,a431)
| ~ c2_1(X0)
| c3_2(X0,a464)
| c6_1(X0)
| c10_2(X0,a432)
| c8_2(X0,a431) ) ).
cnf(u5186,negated_conjecture,
( ~ c5_2(X0,a552)
| c2_2(X0,a551)
| ~ c2_2(X0,X1)
| c9_2(X0,X1)
| c8_2(X0,a559)
| c5_2(X0,X1)
| c7_1(X0) ) ).
cnf(u3913,negated_conjecture,
( ~ c5_1(X121)
| ~ c4_2(X121,X123)
| c5_2(X121,X123)
| ~ c6_2(X121,X122)
| ~ c5_2(X121,X122)
| c10_2(X121,X122) ) ).
cnf(u5151,negated_conjecture,
c1_2(a528,a529) ).
cnf(u6406,negated_conjecture,
~ c2_2(a443,a523) ).
cnf(u7026,negated_conjecture,
ndr1_1(a541) ).
cnf(u3960,negated_conjecture,
~ c10_2(a564,a523) ).
cnf(u5423,negated_conjecture,
ndr1_1(a546) ).
cnf(u4402,negated_conjecture,
~ c2_2(a536,a523) ).
cnf(u4693,negated_conjecture,
( c8_1(X153)
| ndr1_1(X153) ) ).
cnf(u5371,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c2_1(X0)
| c6_2(X0,a506)
| c1_2(X0,X1)
| c3_2(X0,a431)
| c2_2(X0,a431)
| c4_2(X0,a432)
| c3_2(X0,X1) ) ).
cnf(u5683,negated_conjecture,
( ~ c5_2(X0,a431)
| ~ c2_1(X0)
| c8_2(X0,a559)
| c4_2(X0,a432)
| c7_1(X0) ) ).
cnf(u7105,negated_conjecture,
ndr1_1(a540) ).
cnf(u4626,negated_conjecture,
ndr1_1(a516) ).
cnf(u5105,negated_conjecture,
( c1_2(X0,a488)
| ~ c7_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u4625,negated_conjecture,
ndr1_1(a493) ).
cnf(u5458,negated_conjecture,
( ~ c3_2(X0,a431)
| ~ c2_1(X0)
| c3_2(X0,a464)
| c6_1(X0)
| c5_2(X0,a432)
| c8_2(X0,a431) ) ).
cnf(u4039,negated_conjecture,
~ c2_2(a474,a523) ).
cnf(u3963,negated_conjecture,
c9_2(a564,a523) ).
cnf(u7298,negated_conjecture,
( ~ c1_1(X0)
| ~ c7_2(X0,X1)
| c6_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_1(X0)
| c10_2(X0,a583) ) ).
cnf(u5684,negated_conjecture,
( ~ c2_2(X0,a431)
| ~ c2_1(X0)
| c4_2(X0,a432)
| c3_1(X0) ) ).
cnf(u7458,negated_conjecture,
ndr1_1(a503) ).
cnf(u5456,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c2_1(X0)
| c6_2(X0,a506)
| c1_2(X0,X1)
| c3_2(X0,a431)
| c2_2(X0,a431)
| c5_2(X0,a432)
| c3_2(X0,X1) ) ).
cnf(u4623,negated_conjecture,
ndr1_1(a460) ).
cnf(u4409,negated_conjecture,
~ c2_2(a500,a523) ).
cnf(u5742,negated_conjecture,
( ~ c7_2(a513,X0)
| ~ c1_2(a513,X0)
| c10_2(a513,X0) ) ).
cnf(u4410,negated_conjecture,
~ c10_2(a500,a523) ).
cnf(u4396,negated_conjecture,
~ c2_2(a558,a507) ).
cnf(u3904,negated_conjecture,
~ c10_2(a528,a523) ).
cnf(u5754,negated_conjecture,
( ~ c2_2(a513,X0)
| c4_2(a513,X0)
| c3_2(a513,X0) ) ).
cnf(u4179,negated_conjecture,
~ c2_1(a574) ).
cnf(u3933,negated_conjecture,
( ~ c3_1(X82)
| ~ c7_2(X82,X83)
| ~ c1_2(X82,X83)
| c10_2(X82,X83)
| ~ ndr1_1(X82) ) ).
cnf(u4597,negated_conjecture,
ndr1_1(a558) ).
cnf(u5249,negated_conjecture,
c2_1(a539) ).
cnf(u4397,negated_conjecture,
~ c5_2(a558,a507) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN423+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.09/0.18 % Computer : n007.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:53:41 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 9.61/2.09 % (2522523)Detected formulas, will run a generic FOF schedule.
% 9.61/2.09 % (2522531)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3513933125:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.61/2.09 % (2522531)Instruction limit reached!
% 9.61/2.09 % (2522531)------------------------------
% 9.61/2.09 % (2522531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522531)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522531)Termination reason: Instruction limit
% 9.61/2.09 % (2522531)Termination phase: Saturation
% 9.61/2.09 % (2522531)Time elapsed: 0.036 s
% 9.61/2.09 % (2522531)Peak memory usage: 91 MB
% 9.61/2.09 % (2522531)Instructions burned: 110 (million)
% 9.61/2.09 % (2522533)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3708688842:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.61/2.09 % (2522534)dis-21_1_sil=8000:lcm=predicate:random_seed=1464270499: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)
% 9.61/2.09 % (2522532)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=61908601:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.61/2.09 % (2522528)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=3440561566:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.61/2.09 % (2522529)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=2798716421:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.61/2.09 % (2522530)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=2650774650:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.61/2.09 % (2522533)Refutation not found, incomplete strategy
% 9.61/2.09 % (2522533)------------------------------
% 9.61/2.09 % (2522533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522533)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522533)Termination reason: Refutation not found, incomplete strategy
% 9.61/2.09 % (2522533)Time elapsed: 0.032 s
% 9.61/2.09 % (2522533)Peak memory usage: 91 MB
% 9.61/2.09 % (2522533)Instructions burned: 50 (million)
% 9.61/2.09 % (2522532)Instruction limit reached!
% 9.61/2.09 % (2522532)------------------------------
% 9.61/2.09 % (2522532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522532)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522532)Termination reason: Instruction limit
% 9.61/2.09 % (2522532)Termination phase: Saturation
% 9.61/2.09 % (2522532)Time elapsed: 0.066 s
% 9.61/2.09 % (2522532)Peak memory usage: 89 MB
% 9.61/2.09 % (2522532)Instructions burned: 120 (million)
% 9.61/2.09 % (2522534)Instruction limit reached!
% 9.61/2.09 % (2522534)------------------------------
% 9.61/2.09 % (2522534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522534)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522534)Termination reason: Instruction limit
% 9.61/2.09 % (2522534)Termination phase: Saturation
% 9.61/2.09 % (2522534)Time elapsed: 0.074 s
% 9.61/2.09 % (2522534)Peak memory usage: 92 MB
% 9.61/2.09 % (2522534)Instructions burned: 130 (million)
% 9.61/2.09 % (2522536)lrs+10_1_sil=8000:sp=occurrence:random_seed=1513105215:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.61/2.09 % (2522536)Instruction limit reached!
% 9.61/2.09 % (2522536)------------------------------
% 9.61/2.09 % (2522536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522536)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522536)Termination reason: Instruction limit
% 9.61/2.09 % (2522536)Termination phase: Saturation
% 9.61/2.09 % (2522536)Time elapsed: 0.080 s
% 9.61/2.09 % (2522536)Peak memory usage: 93 MB
% 9.61/2.09 % (2522536)Instructions burned: 288 (million)
% 9.61/2.09 % (2522543)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3252992234:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.61/2.09 % (2522545)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1292795150:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.61/2.09 % (2522545)Refutation not found, incomplete strategy
% 9.61/2.09 % (2522545)------------------------------
% 9.61/2.09 % (2522545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522545)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522545)Termination reason: Refutation not found, incomplete strategy
% 9.61/2.09 % (2522545)Time elapsed: 0.026 s
% 9.61/2.09 % (2522545)Peak memory usage: 91 MB
% 9.61/2.09 % (2522545)Instructions burned: 42 (million)
% 9.61/2.09 % (2522543)Refutation not found, incomplete strategy
% 9.61/2.09 % (2522543)------------------------------
% 9.61/2.09 % (2522543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522543)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522543)Termination reason: Refutation not found, incomplete strategy
% 9.61/2.09 % (2522543)Time elapsed: 0.027 s
% 9.61/2.09 % (2522543)Peak memory usage: 91 MB
% 9.61/2.09 % (2522543)Instructions burned: 44 (million)
% 9.61/2.09 % (2522546)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=4268658473:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 9.61/2.09 % (2522533)------------------------------
% 9.61/2.09 % (2522533)------------------------------
% 9.61/2.09 % (2522546)Refutation not found, incomplete strategy
% 9.61/2.09 % (2522546)------------------------------
% 9.61/2.09 % (2522546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522546)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522546)Termination reason: Refutation not found, incomplete strategy
% 9.61/2.09 % (2522546)Time elapsed: 0.017 s
% 9.61/2.09 % (2522546)Peak memory usage: 91 MB
% 9.61/2.09 % (2522546)Instructions burned: 49 (million)
% 9.61/2.09 % (2522550)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1752286518:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.61/2.09 % (2522546)------------------------------
% 9.61/2.09 % (2522546)------------------------------
% 9.61/2.09 % (2522545)------------------------------
% 9.61/2.09 % (2522545)------------------------------
% 9.61/2.09 % (2522543)------------------------------
% 9.61/2.09 % (2522543)------------------------------
% 9.61/2.09 % (2522552)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1450970151:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.61/2.09 % (2522550)Instruction limit reached!
% 9.61/2.09 % (2522550)------------------------------
% 9.61/2.09 % (2522550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522550)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522550)Termination reason: Instruction limit
% 9.61/2.09 % (2522550)Termination phase: Saturation
% 9.61/2.09 % (2522550)Time elapsed: 0.165 s
% 9.61/2.09 % (2522550)Peak memory usage: 93 MB
% 9.61/2.09 % (2522550)Instructions burned: 294 (million)
% 9.61/2.09 % (2522554)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=397730242:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 9.61/2.09 % (2522553)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=907265911:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 9.61/2.09 % (2522554)Instruction limit reached!
% 9.61/2.09 % (2522554)------------------------------
% 9.61/2.09 % (2522554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522554)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522554)Termination reason: Instruction limit
% 9.61/2.09 % (2522554)Termination phase: Saturation
% 9.61/2.09 % (2522554)Time elapsed: 0.067 s
% 9.61/2.09 % (2522554)Peak memory usage: 90 MB
% 9.61/2.09 % (2522554)Instructions burned: 128 (million)
% 9.61/2.09 % (2522553)Instruction limit reached!
% 9.61/2.09 % (2522553)------------------------------
% 9.61/2.09 % (2522553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522553)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522553)Termination reason: Instruction limit
% 9.61/2.09 % (2522553)Termination phase: Saturation
% 9.61/2.09 % (2522553)Time elapsed: 0.067 s
% 9.61/2.09 % (2522553)Peak memory usage: 92 MB
% 9.61/2.09 % (2522553)Instructions burned: 114 (million)
% 9.61/2.09 % (2522556)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=347289957:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 9.61/2.09 % (2522556)Instruction limit reached!
% 9.61/2.09 % (2522556)------------------------------
% 9.61/2.09 % (2522556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522556)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522556)Termination reason: Instruction limit
% 9.61/2.09 % (2522556)Termination phase: Saturation
% 9.61/2.09 % (2522556)Time elapsed: 0.058 s
% 9.61/2.09 % (2522556)Peak memory usage: 90 MB
% 9.61/2.09 % (2522556)Instructions burned: 115 (million)
% 9.61/2.09 % (2522559)lrs+10_1_sil=8000:sp=occurrence:random_seed=3132319665:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 9.61/2.09 % (2522560)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1963922576:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 9.61/2.09 % (2522562)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=596561217:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 9.61/2.09 % (2522529)First to succeed.
% 9.61/2.09 % (2522529)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2522523"
% 9.61/2.09 % (2522560)Instruction limit reached!
% 9.61/2.09 % (2522560)------------------------------
% 9.61/2.09 % (2522560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522560)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522560)Termination reason: Instruction limit
% 9.61/2.09 % (2522560)Termination phase: Saturation
% 9.61/2.09 % (2522560)Time elapsed: 0.225 s
% 9.61/2.09 % (2522560)Peak memory usage: 95 MB
% 9.61/2.09 % (2522560)Instructions burned: 438 (million)
% 9.61/2.09 % (2522566)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4067309279:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 9.61/2.09 % (2522559)Instruction limit reached!
% 9.61/2.09 % (2522559)------------------------------
% 9.61/2.09 % (2522559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522559)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522559)Termination reason: Instruction limit
% 9.61/2.09 % (2522559)Termination phase: Saturation
% 9.61/2.09 % (2522559)Time elapsed: 0.420 s
% 9.61/2.09 % (2522559)Peak memory usage: 98 MB
% 9.61/2.09 % (2522559)Instructions burned: 907 (million)
% 9.61/2.09 % (2522566)Refutation not found, incomplete strategy
% 9.61/2.09 % (2522566)------------------------------
% 9.61/2.09 % (2522566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.09 % (2522566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.09 % (2522566)CaDiCaL version: 2.1.3
% 9.61/2.09 % (2522566)Termination reason: Refutation not found, incomplete strategy
% 9.61/2.09 % (2522566)Time elapsed: 0.057 s
% 9.61/2.09 % (2522566)Peak memory usage: 91 MB
% 9.61/2.09 % (2522566)Instructions burned: 99 (million)
% 9.61/2.09 % SZS status CounterSatisfiable for theBenchmark
% 9.61/2.09 % SZS output start Saturation.
% See solution above
% 9.61/2.10 % SZS output start Definitions and Model Updates.
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_1(X0) | ~c9_2(X0,a446) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set ~c9_2(X0,a446) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ndr1_1(X0) | ~c9_2(X0,a561) | ~ndr1_0 | ~sP13 is false, set ~c9_2(X0,a561) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_0 | c5_0 | ~c2_1(X0) | ndr1_1(X0) | c4_2(X0,a432) | ~ndr1_0 is false, set c4_2(X0,a432) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | c4_2(X0,a496) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set c4_2(X0,a496) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | c9_2(X0,a472) | ndr1_1(X0) | ~ndr1_0 | ~sP22 is false, set c9_2(X0,a472) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | c9_2(X0,a496) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set c9_2(X0,a496) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ndr1_1(X0) | c9_2(X0,a473) | ~ndr1_0 | ~sP22 is false, set c9_2(X0,a473) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c4_1(X0) | ndr1_1(X0) | c9_2(X0,a594) | ~ndr1_0 | ~sP6 is false, set c9_2(X0,a594) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ndr1_1(X0) | c9_2(X0,a602) | ~ndr1_0 | ~sP3 is false, set c9_2(X0,a602) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_1(X0) | c2_2(X0,a598) | ndr1_1(X0) | ~ndr1_0 | ~sP5 is false, set c2_2(X0,a598) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c5_0 | ~c2_1(X38) | ndr1_1(X38) | c2_2(X38,a476) | ~ndr1_0 is false, set c2_2(X38,a476) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | c2_2(X0,a560) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c2_2(X0,a560) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | c2_2(X0,a472) | ndr1_1(X0) | ~ndr1_0 | ~sP22 is false, set c2_2(X0,a472) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_0 | c5_0 | ~c2_1(X0) | ndr1_1(X0) | c10_2(X0,a432) | ~ndr1_0 is false, set c10_2(X0,a432) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_0 | c10_2(a543,X91) | c3_2(a543,X91) | ~c9_2(a543,X91) | ~ndr1_1(a543) | ndr1_0 is false, set c10_2(a543,X91) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ndr1_1(X0) | c8_2(X0,a473) | ~ndr1_0 | ~sP22 is false, set c8_2(X0,a473) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_0 | c8_2(a543,X92) | c9_2(a543,X92) | ~c5_2(a543,X92) | ~ndr1_1(a543) | ndr1_0 is false, set c8_2(a543,X92) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ndr1_1(X0) | c7_2(X0,a602) | ~ndr1_0 | ~sP3 is false, set c7_2(X0,a602) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ndr1_1(X0) | ~c1_2(X0,a561) | ~ndr1_0 | ~sP13 is false, set ~c1_2(X0,a561) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_1(X0) | ndr1_1(X0) | ~c1_2(X0,a599) | ~ndr1_0 | ~sP5 is false, set ~c1_2(X0,a599) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_1(X0) | ndr1_1(X0) | ~c3_2(X0,a447) | ~ndr1_0 | ~sP24 is false, set ~c3_2(X0,a447) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ~c3_2(X0,a472) | ndr1_1(X0) | ~ndr1_0 | ~sP22 is false, set ~c3_2(X0,a472) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_1(X0) | ndr1_1(X0) | ~c2_2(X0,a447) | ~ndr1_0 | ~sP24 is false, set ~c2_2(X0,a447) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ndr1_1(X0) | ~c2_2(X0,a497) | ~ndr1_0 | ~sP19 is false, set ~c2_2(X0,a497) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ~c2_2(X0,a601) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c2_2(X0,a601) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_1(X0) | ndr1_1(X0) | c6_2(X0,a599) | ~ndr1_0 | ~sP5 is false, set c6_2(X0,a599) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | c6_2(X0,a560) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c6_2(X0,a560) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ndr1_1(X0) | c6_2(X0,a602) | ~ndr1_0 | ~sP3 is false, set c6_2(X0,a602) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_0 | c5_0 | ~c2_1(X0) | c6_2(X0,a431) | ndr1_1(X0) | ~ndr1_0 is false, set c6_2(X0,a431) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | c2_1(a516) is false, set c2_1(a516) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_0 | ndr1_0 | c2_1(a544) is false, set c2_1(a544) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ndr1_1(X0) | ~c8_2(X0,a561) | ~ndr1_0 | ~sP13 is false, set ~c8_2(X0,a561) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c1_1(a616) | sP0 | ndr1_0 is false, set ~c1_1(a616) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_0 | ndr1_0 | ~c1_1(a544) is false, set ~c1_1(a544) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | c7_1(a516) is false, set c7_1(a516) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c7_0 | c1_1(a499) | ndr1_0 is false, set c1_1(a499) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_0 | c1_1(a543) | ndr1_0 is false, set c1_1(a543) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(a515) | ndr1_0 is false, set c1_1(a515) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(a610) | ndr1_0 is false, set c1_1(a610) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ndr1_0 | c1_2(a541,X86) | c3_2(a541,X86) | c9_2(a541,X86) | ~ndr1_1(a541) is false, set c1_2(a541,X86) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c5_0 | ~c2_1(X38) | c1_2(X38,a475) | ndr1_1(X38) | ~ndr1_0 is false, set c1_2(X38,a475) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | sP0 | c8_1(a619) is false, set c8_1(a619) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c8_1(a515) | ndr1_0 is false, set c8_1(a515) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_1(X0) | c1_2(X0,a446) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set c1_2(X0,a446) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_0 | c5_0 | ~c2_1(X0) | c1_2(X0,a431) | ndr1_1(X0) | ~ndr1_0 is false, set c1_2(X0,a431) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | c1_2(X0,a601) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set c1_2(X0,a601) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | c1_2(a611,a612) is false, set c1_2(a611,a612) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_1(X0) | ~c6_2(X0,a446) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set ~c6_2(X0,a446) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | c5_2(a611,X163) | ~c6_2(a611,X163) | ~c9_2(a611,X163) | ~ndr1_1(a611) is false, set ~c6_2(a611,X163) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_2(a616,X165) | c3_2(a616,X165) | ~c6_2(a616,X165) | ~ndr1_1(a616) | sP0 | ndr1_0 is false, set ~c6_2(a616,X165) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c4_1(X0) | ~c6_2(X0,a593) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c6_2(X0,a593) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_1(X0) | ~c6_2(X0,a598) | ndr1_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c6_2(X0,a598) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ~c4_2(X0,a601) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c4_2(X0,a601) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c5_0 | ~c2_1(X38) | ndr1_1(X38) | ~c4_2(X38,a476) | ~ndr1_0 is false, set ~c4_2(X38,a476) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c10_1(X0) | ndr1_1(X0) | ~c10_2(X0,a447) | ~ndr1_0 | ~sP24 is false, set ~c10_2(X0,a447) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c4_1(X0) | ndr1_1(X0) | ~c10_2(X0,a594) | ~ndr1_0 | ~sP6 is false, set ~c10_2(X0,a594) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_1(X0) | ndr1_1(X0) | ~c10_2(X0,a599) | ~ndr1_0 | ~sP5 is false, set ~c10_2(X0,a599) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_1(X0) | ~c10_2(X0,a598) | ndr1_1(X0) | ~ndr1_0 | ~sP5 is false, set ~c10_2(X0,a598) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_0 | c5_0 | ~c2_1(X0) | ~c10_2(X0,a431) | ndr1_1(X0) | ~ndr1_0 is false, set ~c10_2(X0,a431) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c5_0 | ~c2_1(X38) | ndr1_1(X38) | ~c10_2(X38,a476) | ~ndr1_0 is false, set ~c10_2(X38,a476) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | ndr1_1(X79) | ndr1_1(X79) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | c8_2(X79,a534) | ndr1_1(X79) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ndr1_1(X0) | c5_2(X0,a497) | ~ndr1_0 | ~sP19 is false, set c5_2(X0,a497) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | ndr1_1(X0) | c5_2(X0,a473) | ~ndr1_0 | ~sP22 is false, set c5_2(X0,a473) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c4_1(X0) | c5_2(X0,a593) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c5_2(X0,a593) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_1(X0) | c5_2(X0,a560) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c5_2(X0,a560) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_0 | c5_0 | ~c2_1(X0) | ndr1_1(X0) | c5_2(X0,a432) | ~ndr1_0 is false, set c5_2(X0,a432) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | ndr1_1(X79) | ~c4_2(X79,a535) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | ndr1_1(X79) | ~c8_2(X79,a535) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | ndr1_1(X79) | ~c9_2(X79,a535) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | ~c4_2(X79,a534) | ndr1_1(X79) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | c5_2(a540,X85) | c8_2(a540,X85) | ~c6_2(a540,X85) | ~ndr1_1(a540) | ndr1_0 is false, set c5_2(a540,X85) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | ndr1_1(X108) | ~c10_2(X108,a552) | ~ndr1_0 is false, set c5_2(X108,X109) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | ndr1_1(X108) | c3_2(X108,a552) | ~ndr1_0 is false, set c5_2(X108,X109) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | c1_2(X108,a551) | ndr1_1(X108) | ~ndr1_0 is false, set c5_2(X108,X109) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | ndr1_1(X108) | ~c4_2(X108,a552) | ~ndr1_0 is false, set c5_2(X108,X109) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | ndr1_1(X108) | ndr1_1(X108) | ~ndr1_0 is false, set c5_2(X108,X109) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | c2_2(X108,a551) | ndr1_1(X108) | ~ndr1_0 is false, set c5_2(X108,X109) to true
% 9.61/2.10 for all groundings, until fixed point,
% 9.61/2.10 whenever ~c10_0 | ~c5_0 | c5_2(X79,X80) | ~c3_2(X79,X80) | ~ndr1_1(X79) | ~c5_2(X79,a534) | ndr1_1(X79) | ~ndr1_0 is false, set c5_2(X79,X80) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c7_0 | ~c2_1(a499) | ndr1_0 is false, set ~c2_1(a499) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X60) | c8_2(X60,X61) | ~c2_2(X60,X61) | ~c9_2(X60,X61) | ~ndr1_1(X60) | ndr1_1(X60) | ~ndr1_0 is false, set ~c2_1(X60) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c2_1(a540) | ndr1_0 is false, set ~c2_1(a540) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c8_1(X118) | ~c3_1(X118) | c4_2(X118,X119) | c6_2(X118,X119) | c8_2(X118,X119) | ~ndr1_1(X118) | ~ndr1_0 | ndr1_0 is false, set ~c3_1(X118) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | sP0 | ~c3_1(a619) is false, set ~c3_1(a619) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c7_0 | ndr1_0 | c10_1(a500) is false, set c10_1(a500) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X58) | ~c8_1(X58) | c3_2(X58,X59) | c4_2(X58,X59) | ~c2_2(X58,X59) | ~ndr1_1(X58) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X58) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c8_1(X66) | c10_2(X66,X67) | c2_2(X66,X67) | c7_2(X66,X67) | ~ndr1_1(X66) | c3_2(X66,X68) | c8_2(X66,X68) | c9_2(X66,X68) | ~ndr1_1(X66) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X66) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | c3_1(X84) | ~c8_1(X84) | c2_2(X84,a538) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X84) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | c3_1(X84) | ~c8_1(X84) | c5_2(X84,a538) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X84) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | c3_1(X84) | ~c8_1(X84) | ndr1_1(X84) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X84) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ~c8_1(a540) | ndr1_0 is false, set ~c8_1(a540) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | ndr1_0 | ~c8_1(a541) is false, set ~c8_1(a541) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c2_1(X114) | ~c8_1(X114) | ndr1_1(X114) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X114) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c10_0 | c3_1(X84) | ~c8_1(X84) | ~c1_2(X84,a538) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X84) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c2_1(X114) | ~c8_1(X114) | c10_2(X114,a557) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X114) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c2_1(X114) | ~c8_1(X114) | c5_2(X114,a557) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X114) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c2_1(X114) | ~c8_1(X114) | ~c4_2(X114,a557) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X114) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c7_0 | ndr1_0 | c4_1(a500) is false, set c4_1(a500) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c4_1(X0) | ndr1_1(X0) | ~c7_2(X0,a497) | ~ndr1_0 | ~sP19 is false, set ~c7_2(X0,a497) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(X52) | c2_2(X52,X53) | ~c10_2(X52,X53) | ~c9_2(X52,X53) | ~ndr1_1(X52) | ndr1_1(X52) | ~ndr1_0 | c1_2(X54,X55) | c3_2(X54,X55) | ~c7_2(X54,X55) | ~ndr1_1(X54) | c2_2(X54,X56) | c3_2(X54,X56) | ~c6_2(X54,X56) | ~ndr1_1(X54) | ndr1_1(X54) | ~ndr1_0 is false, set ~c7_2(X54,X55) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(X52) | c2_2(X52,X53) | ~c10_2(X52,X53) | ~c9_2(X52,X53) | ~ndr1_1(X52) | ndr1_1(X52) | ~ndr1_0 | c1_2(X54,X55) | c3_2(X54,X55) | ~c7_2(X54,X55) | ~ndr1_1(X54) | c2_2(X54,X56) | c3_2(X54,X56) | ~c6_2(X54,X56) | ~ndr1_1(X54) | ~c1_2(X54,a506) | ~ndr1_0 is false, set ~c7_2(X54,X55) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(X52) | c2_2(X52,X53) | ~c10_2(X52,X53) | ~c9_2(X52,X53) | ~ndr1_1(X52) | ndr1_1(X52) | ~ndr1_0 | c1_2(X54,X55) | c3_2(X54,X55) | ~c7_2(X54,X55) | ~ndr1_1(X54) | c2_2(X54,X56) | c3_2(X54,X56) | ~c6_2(X54,X56) | ~ndr1_1(X54) | c6_2(X54,a506) | ~ndr1_0 is false, set ~c7_2(X54,X55) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(X52) | c2_2(X52,X53) | ~c10_2(X52,X53) | ~c9_2(X52,X53) | ~ndr1_1(X52) | ~c3_2(X52,a505) | ~ndr1_0 | c1_2(X54,X55) | c3_2(X54,X55) | ~c7_2(X54,X55) | ~ndr1_1(X54) | c2_2(X54,X56) | c3_2(X54,X56) | ~c6_2(X54,X56) | ~ndr1_1(X54) | ndr1_1(X54) | ~ndr1_0 is false, set ~c7_2(X54,X55) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(X52) | c2_2(X52,X53) | ~c10_2(X52,X53) | ~c9_2(X52,X53) | ~ndr1_1(X52) | c6_2(X52,a505) | ~ndr1_0 | c1_2(X54,X55) | c3_2(X54,X55) | ~c7_2(X54,X55) | ~ndr1_1(X54) | c2_2(X54,X56) | c3_2(X54,X56) | ~c6_2(X54,X56) | ~ndr1_1(X54) | ndr1_1(X54) | ~ndr1_0 is false, set ~c7_2(X54,X55) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | ndr1_1(X62) | ~ndr1_0 | c3_1(a513) is false, set ~c7_2(X62,X63) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | ndr1_1(X62) | ~ndr1_0 | c10_1(a513) is false, set ~c7_2(X62,X63) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | ndr1_1(X62) | ~ndr1_0 | ndr1_0 is false, set ~c7_2(X62,X63) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | c1_2(X62,a512) | ~ndr1_0 | ndr1_0 is false, set ~c7_2(X62,X63) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | ndr1_1(X62) | ~ndr1_0 | c8_2(a513,X64) | ~c2_2(a513,X64) | ~c5_2(a513,X64) | ~ndr1_1(a513) is false, set ~c7_2(X62,X63) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever c1_1(X52) | c2_2(X52,X53) | ~c10_2(X52,X53) | ~c9_2(X52,X53) | ~ndr1_1(X52) | ndr1_1(X52) | ~ndr1_0 | c1_2(X54,X55) | c3_2(X54,X55) | ~c7_2(X54,X55) | ~ndr1_1(X54) | c2_2(X54,X56) | c3_2(X54,X56) | ~c6_2(X54,X56) | ~ndr1_1(X54) | ~c8_2(X54,a506) | ~ndr1_0 is false, set ~c7_2(X54,X55) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | ~c4_2(X62,a512) | ~ndr1_0 | ndr1_0 is false, set ~c7_2(X62,X63) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ~c5_0 | c5_2(X108,X109) | c9_2(X108,X109) | ~c2_2(X108,X109) | ~ndr1_1(X108) | ~c7_2(X108,a551) | ndr1_1(X108) | ~ndr1_0 is false, set ~c7_2(X108,a551) to true
% 9.61/2.10 for all groundings,
% 9.61/2.10 whenever ndr1_0 | ~c7_2(a611,a612) is false, set ~c7_2(a611,a612) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c2_1(X62) | ~c4_2(X62,X63) | ~c7_2(X62,X63) | ~c9_2(X62,X63) | ~ndr1_1(X62) | ~c3_2(X62,a512) | ~ndr1_0 | ndr1_0 is false, set ~c7_2(X62,X63) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | sP0 | c3_2(a619,X166) | ~c4_2(a619,X166) | ~c7_2(a619,X166) | ~ndr1_1(a619) is false, set ~c7_2(a619,X166) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c4_1(X0) | ~c7_2(X0,a496) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set ~c7_2(X0,a496) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c4_1(X0) | ~c7_2(X0,a593) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c7_2(X0,a593) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c5_0 | ~c2_1(X38) | ~c7_2(X38,a475) | ndr1_1(X38) | ~ndr1_0 is false, set ~c7_2(X38,a475) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~c4_1(a516) is false, set ~c4_1(a516) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | c2_2(X45,a494) | ndr1_1(X45) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | ndr1_1(X45) | ~c3_2(X45,a495) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | c8_2(X45,a494) | ndr1_1(X45) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | ndr1_1(X45) | ~c4_2(X45,a495) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | ndr1_1(X45) | ndr1_1(X45) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | ndr1_1(X45) | ~c1_2(X45,a495) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | ~c1_1(X44) | ~c10_1(X44) | ~ndr1_0 | c6_2(X45,X46) | c7_2(X45,X46) | ~c3_2(X45,X46) | ~ndr1_1(X45) | c5_2(X45,a494) | ndr1_1(X45) | ~ndr1_0 is false, set c7_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | ndr1_1(X96) | ~ndr1_0 | ndr1_0 is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | c4_2(X96,a545) | ~ndr1_0 | ndr1_0 is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | ndr1_1(X96) | ~ndr1_0 | ~c2_2(a546,X99) | ~c3_2(a546,X99) | ~ndr1_1(a546) is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | ndr1_1(X96) | ~ndr1_0 | c1_2(a546,X98) | c3_2(a546,X98) | c7_2(a546,X98) | ~ndr1_1(a546) is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | c6_2(X96,a545) | ~ndr1_0 | ndr1_0 is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | ndr1_1(X96) | ~ndr1_0 | c3_1(a546) is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c3_0 | ~c10_2(X96,X97) | ~c2_2(X96,X97) | ~c8_2(X96,X97) | ~ndr1_1(X96) | ~c8_2(X96,a545) | ~ndr1_0 | ndr1_0 is false, set ~c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c3_0 | c7_0 | c4_1(X19) | c9_2(X19,X20) | ~c1_2(X19,X20) | ~c3_2(X19,X20) | ~ndr1_1(X19) | ndr1_1(X19) | ~ndr1_0 is false, set c3_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c4_0 | c3_1(X101) | c5_2(X101,X102) | ~c10_2(X101,X102) | ~c9_2(X101,X102) | ~ndr1_1(X101) | ndr1_1(X101) | ~ndr1_0 is false, set ~c4_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c5_0 | ~c3_1(X41) | ~c7_1(X41) | ndr1_1(X41) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X41) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c5_0 | ~c3_1(X41) | ~c7_1(X41) | c4_2(X41,a488) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X41) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c5_0 | ~c3_1(X41) | ~c7_1(X41) | c1_2(X41,a488) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X41) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c7_1(a515) | ndr1_0 is false, set ~c7_1(a515) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c5_0 | c1_1(X111) | ~c7_1(X111) | c1_2(X111,a555) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X111) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c5_0 | c1_1(X111) | ~c7_1(X111) | ~c2_2(X111,a555) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X111) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c5_0 | c1_1(X111) | ~c7_1(X111) | ndr1_1(X111) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X111) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c5_0 | ~c3_1(X41) | ~c7_1(X41) | c5_2(X41,a488) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X41) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c3_0 | ~c7_1(X28) | ~c8_1(X28) | c5_2(X28,X29) | ~c3_2(X28,X29) | ~ndr1_1(X28) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X28) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c1_1(X129) | c2_1(X129) | ~c7_1(X129) | ~ndr1_0 | c8_1(X130) | ~c1_1(X130) | ndr1_1(X130) | ~ndr1_0 | c9_2(X131,X132) | ~c1_2(X131,X132) | ~c3_2(X131,X132) | ~ndr1_1(X131) | ~c4_2(X131,X133) | ~c8_2(X131,X133) | ~c9_2(X131,X133) | ~ndr1_1(X131) | ndr1_1(X131) | ~ndr1_0 is false, set ~c7_1(X129) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c1_1(X129) | c2_1(X129) | ~c7_1(X129) | ~ndr1_0 | c8_1(X130) | ~c1_1(X130) | ~c6_2(X130,a576) | ~ndr1_0 | c9_2(X131,X132) | ~c1_2(X131,X132) | ~c3_2(X131,X132) | ~ndr1_1(X131) | ~c4_2(X131,X133) | ~c8_2(X131,X133) | ~c9_2(X131,X133) | ~ndr1_1(X131) | ndr1_1(X131) | ~ndr1_0 is false, set ~c7_1(X129) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c1_1(X129) | c2_1(X129) | ~c7_1(X129) | ~ndr1_0 | c8_1(X130) | ~c1_1(X130) | c5_2(X130,a576) | ~ndr1_0 | c9_2(X131,X132) | ~c1_2(X131,X132) | ~c3_2(X131,X132) | ~ndr1_1(X131) | ~c4_2(X131,X133) | ~c8_2(X131,X133) | ~c9_2(X131,X133) | ~ndr1_1(X131) | ndr1_1(X131) | ~ndr1_0 is false, set ~c7_1(X129) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c1_1(X129) | c2_1(X129) | ~c7_1(X129) | ~ndr1_0 | c8_1(X130) | ~c1_1(X130) | ~c7_2(X130,a576) | ~ndr1_0 | c9_2(X131,X132) | ~c1_2(X131,X132) | ~c3_2(X131,X132) | ~ndr1_1(X131) | ~c4_2(X131,X133) | ~c8_2(X131,X133) | ~c9_2(X131,X133) | ~ndr1_1(X131) | ndr1_1(X131) | ~ndr1_0 is false, set ~c7_1(X129) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c5_0 | c1_1(X111) | ~c7_1(X111) | ~c6_2(X111,a555) | ~ndr1_0 | ndr1_0 is false, set ~c7_1(X111) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c10_0 | ndr1_0 | ~c5_1(a541) is false, set ~c5_1(a541) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c5_0 | ~c5_1(X121) | c10_2(X121,X122) | ~c5_2(X121,X122) | ~c6_2(X121,X122) | ~ndr1_1(X121) | c5_2(X121,X123) | ~c4_2(X121,X123) | ~ndr1_1(X121) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X121) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever sP3 | ndr1_0 | sP4 is false, set sP3 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever sP5 | c10_2(X155,X156) | ~c3_2(X155,X156) | ~c6_2(X155,X156) | ~ndr1_1(X155) | c9_2(X155,X157) | ~c4_2(X155,X157) | ~c8_2(X155,X157) | ~ndr1_1(X155) | ~c5_2(X155,X158) | ~c8_2(X155,X158) | ~c9_2(X155,X158) | ~ndr1_1(X155) | ~ndr1_0 | ndr1_0 is false, set sP5 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c5_0 | c7_1(X116) | c10_2(X116,X117) | ~c5_2(X116,X117) | ~ndr1_1(X116) | ndr1_1(X116) | ~ndr1_0 | sP13 is false, set sP13 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c7_0 | sP19 | ndr1_0 is false, set sP19 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c4_0 | sP22 | ndr1_0 is false, set sP22 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c10_0 | sP24 | ndr1_0 is false, set sP24 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c2_0 | c3_1(X89) | c5_1(X89) | c7_1(X89) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c2_0 | ndr1_0 | c6_1(a544) is false, set c6_1(a544) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | c6_1(a611) is false, set c6_1(a611) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c6_1(a616) | sP0 | ndr1_0 is false, set c6_1(a616) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c3_0 | ~c10_0 | c6_1(X25) | c8_2(X25,X26) | ~c3_2(X25,X26) | ~c6_2(X25,X26) | ~ndr1_1(X25) | ndr1_1(X25) | ~ndr1_0 is false, set c6_1(X25) to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever sP6 | ~c5_1(X150) | ~c8_1(X150) | c1_2(X150,X151) | ~c8_2(X150,X151) | ~ndr1_1(X150) | ~ndr1_0 | ndr1_0 is false, set sP6 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP2 is false, set ~sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c3_1(X147) | ~c1_1(X147) | ~c2_1(X147) | ~ndr1_0 | ndr1_0 | sP8 is false, set sP8 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c10_1(X141) | ~c3_1(X141) | ~c5_1(X141) | ~ndr1_0 | sP10 | ndr1_0 is false, set sP10 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c10_1(X143) | c10_2(X143,X144) | c2_2(X143,X144) | c8_2(X143,X144) | ~ndr1_1(X143) | ~ndr1_0 | ~c3_1(X145) | c5_2(X145,X146) | c6_2(X145,X146) | ~c7_2(X145,X146) | ~ndr1_1(X145) | ndr1_1(X145) | ~ndr1_0 | sP9 is false, set sP9 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c9_0 | ~c1_1(X72) | c1_2(X72,X73) | c4_2(X72,X73) | ~c3_2(X72,X73) | ~ndr1_1(X72) | ndr1_1(X72) | ~ndr1_0 | sP17 is false, set sP17 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c3_1(X148) | c3_2(X148,X149) | ~c5_2(X148,X149) | ~c9_2(X148,X149) | ~ndr1_1(X148) | ndr1_1(X148) | ~ndr1_0 | sP7 is false, set sP7 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP8 is false, set ~sP8 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP10 is false, set ~sP10 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c9_1(X160) | c2_2(X160,X161) | c4_2(X160,X161) | c9_2(X160,X161) | ~ndr1_1(X160) | ~c4_2(X160,a607) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c9_1(X160) | c2_2(X160,X161) | c4_2(X160,X161) | c9_2(X160,X161) | ~ndr1_1(X160) | ~c3_2(X160,a607) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c9_1(X160) | c2_2(X160,X161) | c4_2(X160,X161) | c9_2(X160,X161) | ~ndr1_1(X160) | ~c2_2(X160,a607) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c9_1(X160) | c2_2(X160,X161) | c4_2(X160,X161) | c9_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | c2_2(a608,X162) | ~c10_2(a608,X162) | ~c7_2(a608,X162) | ~ndr1_1(a608) | sP2 is false, set sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c9_1(X160) | c2_2(X160,X161) | c4_2(X160,X161) | c9_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | c4_1(a608) | sP2 is false, set sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c9_1(X160) | c2_2(X160,X161) | c4_2(X160,X161) | c9_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | ndr1_0 | sP2 is false, set sP2 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP9 is false, set ~sP9 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP16 is false, set ~sP16 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP18 is false, set ~sP18 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP21 is false, set ~sP21 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP17 is false, set ~sP17 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP15 is false, set ~sP15 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ndr1_0 | ~sP7 is false, set ~sP7 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever c6_0 is false, set c6_0 to true
% 10.64/2.18 for all groundings,
% 10.64/2.18 whenever ~c8_0 is false, set ~c8_0 to true
% 10.64/2.18 % SZS output end Definitions and Model Updates.
% 10.64/2.18 % (2522529)------------------------------
% 10.64/2.18 % (2522529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.18 % (2522529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.18 % (2522529)CaDiCaL version: 2.1.3
% 10.64/2.18 % (2522529)Termination reason: Satisfiable
% 10.64/2.18 % (2522529)Time elapsed: 1.027 s
% 10.64/2.18 % (2522529)Peak memory usage: 138 MB
% 10.64/2.18 % (2522529)Instructions burned: 1569 (million)
% 10.64/2.18 % (2522529)------------------------------
% 10.64/2.18 % (2522529)------------------------------
% 10.64/2.18 % (2522523)Success in time 1.442 s
% 10.64/2.18 % Vampire exiting
%------------------------------------------------------------------------------