%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN427+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 7.75s 2.02s
% Output : Saturation 7.75s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1401,negated_conjecture,
c9_0 ).
cnf(u1481,negated_conjecture,
ndr1_0 ).
cnf(u1450,negated_conjecture,
c2_0 ).
cnf(u3695,negated_conjecture,
~ sP0 ).
cnf(u2267,negated_conjecture,
c3_0 ).
cnf(u1490,negated_conjecture,
c10_0 ).
cnf(u3720,negated_conjecture,
~ sP1 ).
cnf(u1493,negated_conjecture,
~ c4_1(a1824) ).
cnf(u1497,negated_conjecture,
c5_2(a1824,a1825) ).
cnf(u1501,negated_conjecture,
c8_2(a1824,a1825) ).
cnf(u1505,negated_conjecture,
~ c9_2(a1824,a1825) ).
cnf(u5656,negated_conjecture,
~ ndr1_1(a1824) ).
cnf(u1513,negated_conjecture,
c8_1(a1824) ).
cnf(u1518,negated_conjecture,
sP3 ).
cnf(u1521,negated_conjecture,
c8_2(a1820,a1821) ).
cnf(u3746,negated_conjecture,
~ sP2 ).
cnf(u1528,negated_conjecture,
~ c9_2(a1820,a1821) ).
cnf(u1532,negated_conjecture,
~ c1_2(a1820,a1821) ).
cnf(u1542,negated_conjecture,
~ ndr1_1(a1820) ).
cnf(u1540,negated_conjecture,
~ c7_1(a1820) ).
cnf(u1545,negated_conjecture,
( ~ c10_2(a1820,X188)
| c5_2(a1820,X188)
| c9_2(a1820,X188) ) ).
cnf(u1571,negated_conjecture,
~ c8_0 ).
cnf(u1557,negated_conjecture,
~ c6_0 ).
cnf(u1680,negated_conjecture,
~ c4_0 ).
cnf(u1600,negated_conjecture,
~ c5_1(a1813) ).
cnf(u3807,negated_conjecture,
~ sP4 ).
cnf(u1610,negated_conjecture,
~ ndr1_1(a1813) ).
cnf(u1617,negated_conjecture,
~ c4_1(a1813) ).
cnf(u3829,negated_conjecture,
~ sP5 ).
cnf(u1649,negated_conjecture,
~ c1_0 ).
cnf(u1678,negated_conjecture,
( ~ c5_1(X181)
| c10_2(X181,X182)
| ~ c9_2(X181,X183)
| c2_2(X181,X183)
| ~ ndr1_1(X181)
| c5_2(X181,X182)
| ~ c7_2(X181,X182) ) ).
cnf(u1684,negated_conjecture,
~ c7_2(a1802,a1804) ).
cnf(u3855,negated_conjecture,
~ sP6 ).
cnf(u1691,negated_conjecture,
c6_2(a1802,a1804) ).
cnf(u1695,negated_conjecture,
c5_2(a1802,a1804) ).
cnf(u1699,negated_conjecture,
ndr1_1(a1802) ).
cnf(u1703,negated_conjecture,
c7_2(a1802,a1803) ).
cnf(u1707,negated_conjecture,
c4_2(a1802,a1803) ).
cnf(u1711,negated_conjecture,
c9_2(a1802,a1803) ).
cnf(u1716,negated_conjecture,
c7_1(a1802) ).
cnf(u1721,negated_conjecture,
~ c6_1(a1798) ).
cnf(u1724,negated_conjecture,
sP7 ).
cnf(u1728,negated_conjecture,
~ c9_2(a1798,a1799) ).
cnf(u1732,negated_conjecture,
c10_2(a1798,a1799) ).
cnf(u1736,negated_conjecture,
c5_2(a1798,a1799) ).
cnf(u1744,negated_conjecture,
~ c1_1(a1798) ).
cnf(u3919,negated_conjecture,
~ sP8 ).
cnf(u1752,negated_conjecture,
( ~ c7_2(X179,X180)
| ~ ndr1_1(X179)
| c4_2(X179,a1792)
| ~ c8_2(X179,X180)
| ~ c4_2(X179,X180) ) ).
cnf(u1756,negated_conjecture,
( ~ c1_2(X179,a1792)
| ~ ndr1_1(X179)
| ~ c7_2(X179,X180)
| ~ c8_2(X179,X180)
| ~ c4_2(X179,X180) ) ).
cnf(u1760,negated_conjecture,
( ~ c7_2(X179,X180)
| ~ ndr1_1(X179)
| c5_2(X179,a1792)
| ~ c8_2(X179,X180)
| ~ c4_2(X179,X180) ) ).
cnf(u1764,negated_conjecture,
( ~ c8_1(X176)
| ~ c4_2(X176,X178)
| ~ c8_2(X176,X178)
| c5_2(X176,X178)
| ~ c3_2(X176,X177)
| ~ ndr1_1(X176)
| c5_2(X176,X177)
| ~ c2_2(X176,X177) ) ).
cnf(u3957,negated_conjecture,
~ sP9 ).
cnf(u3992,negated_conjecture,
~ sP10 ).
cnf(u1798,negated_conjecture,
~ c10_1(a1784) ).
cnf(u1802,negated_conjecture,
~ ndr1_1(a1784) ).
cnf(u1809,negated_conjecture,
~ c2_1(a1784) ).
cnf(u1830,negated_conjecture,
( ~ c6_1(X169)
| ~ ndr1_1(X169)
| c1_2(X169,X170)
| c2_2(X169,X170)
| c10_2(X169,X170)
| c7_1(X169) ) ).
cnf(u1861,negated_conjecture,
( ~ c4_1(X164)
| ~ c2_2(X164,X165)
| c3_2(X164,a1780)
| ~ ndr1_1(X164)
| c9_2(X164,X165)
| ~ c3_2(X164,X165) ) ).
cnf(u1865,negated_conjecture,
( ~ c4_1(X164)
| ~ c2_2(X164,X165)
| c7_2(X164,a1780)
| ~ ndr1_1(X164)
| c9_2(X164,X165)
| ~ c3_2(X164,X165) ) ).
cnf(u1869,negated_conjecture,
( ~ c4_1(X164)
| ~ c2_2(X164,X165)
| c6_2(X164,a1780)
| ~ ndr1_1(X164)
| c9_2(X164,X165)
| ~ c3_2(X164,X165) ) ).
cnf(u4019,negated_conjecture,
~ sP11 ).
cnf(u4060,negated_conjecture,
~ sP12 ).
cnf(u1936,negated_conjecture,
( ~ c6_2(X158,a1772)
| ~ c8_2(X158,X160)
| ~ c1_2(X158,X160)
| c10_2(X158,X159)
| ~ ndr1_1(X158)
| c9_2(X158,X159)
| ~ c2_2(X158,X159) ) ).
cnf(u1940,negated_conjecture,
( ~ c2_2(X158,a1772)
| ~ c8_2(X158,X160)
| ~ c1_2(X158,X160)
| c10_2(X158,X159)
| ~ ndr1_1(X158)
| c9_2(X158,X159)
| ~ c2_2(X158,X159) ) ).
cnf(u1944,negated_conjecture,
( ~ ndr1_1(X158)
| ~ c8_2(X158,X160)
| ~ c1_2(X158,X160)
| c3_2(X158,a1772)
| c10_2(X158,X159)
| c9_2(X158,X159)
| ~ c2_2(X158,X159) ) ).
cnf(u1974,negated_conjecture,
c5_0 ).
cnf(u1993,negated_conjecture,
( c7_1(X155)
| c3_1(X155)
| c10_1(X155) ) ).
cnf(u2012,negated_conjecture,
( ~ c9_1(X153)
| c8_1(X153)
| ~ c5_1(X153) ) ).
cnf(u2020,negated_conjecture,
( ~ c9_2(X145,a1765)
| ~ c6_2(X145,X146)
| c9_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2025,negated_conjecture,
( ~ c4_2(X145,a1765)
| ~ c6_2(X145,X146)
| c9_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2029,negated_conjecture,
( ~ c3_2(X145,a1765)
| ~ c6_2(X145,X146)
| c9_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2033,negated_conjecture,
( ~ c9_2(X145,a1765)
| ~ c6_2(X145,X146)
| c2_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2037,negated_conjecture,
( ~ c4_2(X145,a1765)
| ~ c6_2(X145,X146)
| c2_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2041,negated_conjecture,
( ~ c3_2(X145,a1765)
| ~ c6_2(X145,X146)
| c2_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2045,negated_conjecture,
( ~ c9_2(X145,a1765)
| ~ c6_2(X145,X146)
| c4_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2049,negated_conjecture,
( ~ c4_2(X145,a1765)
| ~ c6_2(X145,X146)
| c4_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2053,negated_conjecture,
( ~ c3_2(X145,a1765)
| ~ c6_2(X145,X146)
| c4_2(X145,a1764)
| ~ ndr1_1(X145)
| c1_2(X145,X146)
| ~ c3_2(X145,X146) ) ).
cnf(u2057,negated_conjecture,
( c7_1(X144)
| ~ c1_1(X144)
| c4_1(X144) ) ).
cnf(u4097,negated_conjecture,
~ sP13 ).
cnf(u4138,negated_conjecture,
~ sP14 ).
cnf(u2121,negated_conjecture,
( ~ c9_1(X139)
| ~ c10_1(X139)
| ~ c1_1(X139) ) ).
cnf(u4165,negated_conjecture,
~ sP15 ).
cnf(u2139,negated_conjecture,
~ c9_1(a1752) ).
cnf(u2143,negated_conjecture,
~ c8_1(a1752) ).
cnf(u2150,negated_conjecture,
( ~ c1_2(a1752,X136)
| ~ c6_2(a1752,X136)
| c2_2(a1752,X136) ) ).
cnf(u2167,negated_conjecture,
~ ndr1_1(a1750) ).
cnf(u2181,negated_conjecture,
c6_1(a1750) ).
cnf(u4206,negated_conjecture,
~ sP16 ).
cnf(u2245,negated_conjecture,
ndr1_1(a1743) ).
cnf(u2227,negated_conjecture,
( c4_2(a1743,X127)
| c2_2(a1743,X127)
| ~ c3_2(a1743,X127) ) ).
cnf(u2231,negated_conjecture,
( ~ c5_2(a1743,X126)
| ~ c1_2(a1743,X126)
| c8_2(a1743,X126) ) ).
cnf(u2235,negated_conjecture,
c8_2(a1743,a1744) ).
cnf(u2239,negated_conjecture,
c2_2(a1743,a1744) ).
cnf(u2243,negated_conjecture,
~ c1_2(a1743,a1744) ).
cnf(u2250,negated_conjecture,
( ~ c10_1(X125)
| ~ c4_1(X125)
| c8_2(X125,a1742) ) ).
cnf(u4233,negated_conjecture,
~ sP17 ).
cnf(u2257,negated_conjecture,
( ~ c10_1(X125)
| ~ c4_1(X125)
| c2_2(X125,a1742) ) ).
cnf(u2261,negated_conjecture,
( ~ c10_1(X125)
| ~ c4_1(X125)
| c7_2(X125,a1742) ) ).
cnf(u2265,negated_conjecture,
( ~ c4_1(X125)
| ndr1_1(X125)
| ~ c10_1(X125) ) ).
cnf(u4258,negated_conjecture,
~ sP18 ).
cnf(u2288,negated_conjecture,
~ c8_1(a1736) ).
cnf(u4284,negated_conjecture,
~ sP19 ).
cnf(u2295,negated_conjecture,
~ c1_1(a1736) ).
cnf(u2299,negated_conjecture,
c6_1(a1736) ).
cnf(u4319,negated_conjecture,
~ sP20 ).
cnf(u2321,negated_conjecture,
( ~ c7_2(X119,X120)
| ~ ndr1_1(X119)
| c1_2(X119,X120)
| c5_2(X119,a1728)
| c2_2(X119,X120)
| c1_1(X119) ) ).
cnf(u2325,negated_conjecture,
c3_1(a1729) ).
cnf(u2329,negated_conjecture,
c5_1(a1729) ).
cnf(u2333,negated_conjecture,
( ~ c9_2(X119,a1728)
| ~ ndr1_1(X119)
| c1_2(X119,X120)
| ~ c7_2(X119,X120)
| c2_2(X119,X120)
| c1_1(X119) ) ).
cnf(u2339,negated_conjecture,
( ~ c3_2(X119,a1728)
| ~ ndr1_1(X119)
| c1_2(X119,X120)
| ~ c7_2(X119,X120)
| c2_2(X119,X120)
| c1_1(X119) ) ).
cnf(u2352,negated_conjecture,
( ~ c5_1(X117)
| ~ c6_1(X117)
| c9_1(X117) ) ).
cnf(u2374,negated_conjecture,
( ~ c9_1(X116)
| c3_1(X116)
| ~ c10_1(X116) ) ).
cnf(u2389,negated_conjecture,
sP21 ).
cnf(u4371,negated_conjecture,
~ sP22 ).
cnf(u2429,negated_conjecture,
( ~ c10_2(X112,a1717)
| ~ ndr1_1(X112)
| c3_2(X112,X113)
| ~ c10_2(X112,X113)
| c6_2(X112,X113)
| ~ c8_1(X112) ) ).
cnf(u2436,negated_conjecture,
( ~ c9_2(X112,a1717)
| ~ ndr1_1(X112)
| c3_2(X112,X113)
| ~ c10_2(X112,X113)
| c6_2(X112,X113)
| ~ c8_1(X112) ) ).
cnf(u2465,negated_conjecture,
( ~ c5_1(X106)
| ~ c10_1(X106)
| c2_2(X106,a1714) ) ).
cnf(u4397,negated_conjecture,
~ sP23 ).
cnf(u2472,negated_conjecture,
( c3_2(X106,a1714)
| ~ c5_1(X106)
| ~ c10_1(X106) ) ).
cnf(u2476,negated_conjecture,
( c4_2(X106,a1714)
| ~ c5_1(X106)
| ~ c10_1(X106) ) ).
cnf(u4423,negated_conjecture,
~ sP24 ).
cnf(u2494,negated_conjecture,
( c3_2(X101,a1710)
| c2_1(X101)
| c8_1(X101) ) ).
cnf(u2501,negated_conjecture,
( c1_2(X101,a1710)
| c2_1(X101)
| c8_1(X101) ) ).
cnf(u2505,negated_conjecture,
( c2_1(X101)
| c8_1(X101)
| ndr1_1(X101) ) ).
cnf(u2529,negated_conjecture,
~ ndr1_1(a1708) ).
cnf(u4439,negated_conjecture,
~ sP25 ).
cnf(u2548,negated_conjecture,
~ c1_1(a1705) ).
cnf(u2552,negated_conjecture,
~ c9_1(a1705) ).
cnf(u2556,negated_conjecture,
~ c3_1(a1705) ).
cnf(u2562,negated_conjecture,
c1_1(a1704) ).
cnf(u2566,negated_conjecture,
~ ndr1_1(a1704) ).
cnf(u2582,negated_conjecture,
~ c7_1(a1700) ).
cnf(u2603,negated_conjecture,
ndr1_1(a1700) ).
cnf(u2589,negated_conjecture,
( ~ c10_2(a1700,X92)
| c6_2(a1700,X92)
| ~ c3_2(a1700,X92) ) ).
cnf(u2593,negated_conjecture,
~ c7_2(a1700,a1701) ).
cnf(u2597,negated_conjecture,
c9_2(a1700,a1701) ).
cnf(u2601,negated_conjecture,
c4_2(a1700,a1701) ).
cnf(u2611,negated_conjecture,
~ c3_1(a1698) ).
cnf(u2630,negated_conjecture,
~ c6_1(a1698) ).
cnf(u2637,negated_conjecture,
( ~ c3_1(X88)
| c8_1(X88)
| c10_1(X88) ) ).
cnf(u4466,negated_conjecture,
~ sP26 ).
cnf(u2644,negated_conjecture,
~ ndr1_1(a1694) ).
cnf(u4501,negated_conjecture,
~ sP27 ).
cnf(u2654,negated_conjecture,
~ c6_1(a1694) ).
cnf(u2658,negated_conjecture,
c9_1(a1694) ).
cnf(u2663,negated_conjecture,
~ c1_1(a1691) ).
cnf(u2670,negated_conjecture,
~ c6_1(a1691) ).
cnf(u2674,negated_conjecture,
~ ndr1_1(a1691) ).
cnf(u2681,negated_conjecture,
( ~ c5_1(X82)
| ~ ndr1_1(X82)
| ~ c10_2(X82,X83)
| c2_2(X82,X83)
| c1_2(X82,X83) ) ).
cnf(u2687,negated_conjecture,
( c6_2(X80,a1690)
| c1_2(X80,a1689) ) ).
cnf(u2691,negated_conjecture,
( c7_2(X80,a1690)
| c1_2(X80,a1689) ) ).
cnf(u2699,negated_conjecture,
( ~ c9_2(X80,a1689)
| c6_2(X80,a1690) ) ).
cnf(u2703,negated_conjecture,
( ~ c9_2(X80,a1689)
| c7_2(X80,a1690) ) ).
cnf(u2707,negated_conjecture,
( ~ c9_2(X80,a1689)
| ~ c2_2(X80,a1690) ) ).
cnf(u2711,negated_conjecture,
( ~ c3_2(X80,a1689)
| c6_2(X80,a1690) ) ).
cnf(u2715,negated_conjecture,
( ~ c3_2(X80,a1689)
| c7_2(X80,a1690) ) ).
cnf(u2719,negated_conjecture,
( ~ c3_2(X80,a1689)
| ~ c2_2(X80,a1690) ) ).
cnf(u2727,negated_conjecture,
( ~ c5_1(X78)
| ~ ndr1_1(X78)
| ~ c9_2(X78,X79)
| ~ c7_2(X78,X79)
| ~ c3_2(X78,X79)
| c1_1(X78) ) ).
cnf(u2756,negated_conjecture,
( ~ c5_1(X68)
| ~ c1_2(X68,X69)
| c7_1(X68)
| ~ ndr1_1(X68)
| c2_2(X68,X69)
| ~ c6_2(X68,X69) ) ).
cnf(u2786,negated_conjecture,
~ c2_1(a1683) ).
cnf(u2790,negated_conjecture,
~ c8_2(a1683,a1684) ).
cnf(u2794,negated_conjecture,
c5_2(a1683,a1684) ).
cnf(u2798,negated_conjecture,
~ c6_2(a1683,a1684) ).
cnf(u2802,negated_conjecture,
ndr1_1(a1683) ).
cnf(u2806,negated_conjecture,
c8_1(a1683) ).
cnf(u2811,negated_conjecture,
( c4_2(X65,X66)
| ~ c7_1(X65)
| ~ ndr1_1(X65)
| c3_2(X65,X66)
| c9_2(X65,a1682)
| c1_2(X65,X66) ) ).
cnf(u2818,negated_conjecture,
( ~ c8_2(X65,a1682)
| ~ c7_1(X65)
| ~ ndr1_1(X65)
| c3_2(X65,X66)
| c4_2(X65,X66)
| c1_2(X65,X66) ) ).
cnf(u2822,negated_conjecture,
( ~ c1_2(X65,a1682)
| ~ c7_1(X65)
| ~ ndr1_1(X65)
| c3_2(X65,X66)
| c4_2(X65,X66)
| c1_2(X65,X66) ) ).
cnf(u2826,negated_conjecture,
c3_1(a1681) ).
cnf(u2830,negated_conjecture,
c8_1(a1681) ).
cnf(u2834,negated_conjecture,
~ ndr1_1(a1681) ).
cnf(u4528,negated_conjecture,
~ sP28 ).
cnf(u4549,negated_conjecture,
~ sP29 ).
cnf(u2938,negated_conjecture,
~ ndr1_1(a1668) ).
cnf(u2945,negated_conjecture,
~ c6_1(a1668) ).
cnf(u2950,negated_conjecture,
~ ndr1_1(a1667) ).
cnf(u2960,negated_conjecture,
c4_1(a1667) ).
cnf(u2964,negated_conjecture,
~ c9_1(a1667) ).
cnf(u2981,negated_conjecture,
( ~ c8_2(X52,a1665)
| c3_1(X52)
| c8_1(X52) ) ).
cnf(u4579,negated_conjecture,
~ sP30 ).
cnf(u2988,negated_conjecture,
( ~ c7_2(X52,a1665)
| c3_1(X52)
| c8_1(X52) ) ).
cnf(u2992,negated_conjecture,
( ~ c9_2(X52,a1665)
| c3_1(X52)
| c8_1(X52) ) ).
cnf(u2996,negated_conjecture,
( c3_1(X52)
| c8_1(X52)
| ndr1_1(X52) ) ).
cnf(u3000,negated_conjecture,
sP31 ).
cnf(u3003,negated_conjecture,
( ~ c7_2(X50,a1658)
| c9_1(X50)
| c9_2(X50,X51)
| ~ ndr1_1(X50)
| c8_2(X50,X51) ) ).
cnf(u3011,negated_conjecture,
( ~ c9_2(X50,a1658)
| c9_1(X50)
| c9_2(X50,X51)
| ~ ndr1_1(X50)
| c8_2(X50,X51) ) ).
cnf(u3015,negated_conjecture,
( ~ c1_1(X49)
| c6_1(X49) ) ).
cnf(u3033,negated_conjecture,
~ ndr1_1(a1655) ).
cnf(u3036,negated_conjecture,
( ~ c10_2(a1655,X44)
| c1_2(a1655,X44)
| ~ c7_2(a1655,X44) ) ).
cnf(u3040,negated_conjecture,
c6_1(a1655) ).
cnf(u3044,negated_conjecture,
c2_2(a1655,a1656) ).
cnf(u3048,negated_conjecture,
~ c7_2(a1655,a1656) ).
cnf(u3058,negated_conjecture,
( ~ c1_2(X42,X43)
| ~ ndr1_1(X42)
| ~ c9_2(X42,X43)
| ~ c3_2(X42,X43)
| c5_1(X42)
| c10_1(X42) ) ).
cnf(u3070,negated_conjecture,
( ~ c3_1(X41)
| c6_2(X41,a1653)
| ~ c2_1(X41) ) ).
cnf(u3074,negated_conjecture,
( ~ c3_1(X41)
| ~ c4_2(X41,a1653)
| ~ c2_1(X41) ) ).
cnf(u3078,negated_conjecture,
( ~ c3_1(X41)
| ndr1_1(X41)
| ~ c2_1(X41) ) ).
cnf(u4647,negated_conjecture,
~ sP32 ).
cnf(u3109,negated_conjecture,
~ ndr1_1(a1647) ).
cnf(u3124,negated_conjecture,
~ c4_1(a1647) ).
cnf(u3130,negated_conjecture,
~ c2_1(a1647) ).
cnf(u4685,negated_conjecture,
~ sP33 ).
cnf(u3139,negated_conjecture,
~ c9_1(a1644) ).
cnf(u3146,negated_conjecture,
~ c6_1(a1644) ).
cnf(u3150,negated_conjecture,
~ ndr1_1(a1644) ).
cnf(u3175,negated_conjecture,
( ~ c6_1(X33)
| ~ c3_1(X33)
| ~ c1_1(X33) ) ).
cnf(u4710,negated_conjecture,
~ sP34 ).
cnf(u3228,negated_conjecture,
( c9_1(X32)
| c6_1(X32)
| ~ c5_1(X32) ) ).
cnf(u4750,negated_conjecture,
~ sP35 ).
cnf(u3249,negated_conjecture,
( c4_1(X29)
| c2_1(X29)
| ~ c6_1(X29) ) ).
cnf(u3311,negated_conjecture,
c9_1(a1626) ).
cnf(u4784,negated_conjecture,
~ sP36 ).
cnf(u3321,negated_conjecture,
c3_1(a1626) ).
cnf(u3325,negated_conjecture,
c5_1(a1626) ).
cnf(u3344,negated_conjecture,
( ~ c2_2(X21,X23)
| c7_2(X21,X23)
| c4_1(X21)
| c1_2(X21,X23)
| ~ ndr1_1(X21)
| ~ c10_2(X21,X22)
| c6_2(X21,X22)
| ~ c7_2(X21,X22) ) ).
cnf(u4810,negated_conjecture,
~ sP37 ).
cnf(u3380,negated_conjecture,
ndr1_1(a1618) ).
cnf(u3362,negated_conjecture,
( ~ c9_2(a1618,X20)
| ~ c8_2(a1618,X20)
| c3_2(a1618,X20) ) ).
cnf(u3366,negated_conjecture,
c5_1(a1618) ).
cnf(u3370,negated_conjecture,
c9_2(a1618,a1619) ).
cnf(u3374,negated_conjecture,
c8_2(a1618,a1619) ).
cnf(u3378,negated_conjecture,
~ c6_2(a1618,a1619) ).
cnf(u4837,negated_conjecture,
~ sP38 ).
cnf(u3469,negated_conjecture,
~ ndr1_1(a1610) ).
cnf(u3476,negated_conjecture,
c7_1(a1610) ).
cnf(u3481,negated_conjecture,
sP39 ).
cnf(u3487,negated_conjecture,
( ~ c5_1(X12)
| c6_1(X12)
| ~ c8_2(X12,a1607) ) ).
cnf(u3495,negated_conjecture,
( ~ c10_2(X13,a1608)
| ~ c10_2(X13,X15)
| c3_2(X13,X15)
| c6_2(X13,X15)
| ~ c7_2(X13,X14)
| ~ ndr1_1(X13)
| c5_2(X13,X14)
| ~ c8_2(X13,X14) ) ).
cnf(u3499,negated_conjecture,
( ~ c5_1(X12)
| c6_1(X12)
| ~ c6_2(X12,a1607) ) ).
cnf(u3511,negated_conjecture,
( ~ c5_1(X12)
| c6_1(X12)
| ndr1_1(X12) ) ).
cnf(u4876,negated_conjecture,
~ sP40 ).
cnf(u3523,negated_conjecture,
( ~ c8_1(X8)
| ~ ndr1_1(X8)
| ~ c7_2(X8,X9)
| ~ c8_2(X8,X9)
| c3_2(X8,X9)
| c2_2(X8,a1602) ) ).
cnf(u3527,negated_conjecture,
( ~ c8_1(X8)
| ~ ndr1_1(X8)
| ~ c7_2(X8,X9)
| ~ c8_2(X8,X9)
| c3_2(X8,X9)
| ~ c4_2(X8,a1602) ) ).
cnf(u3531,negated_conjecture,
c9_1(a1601) ).
cnf(u4915,negated_conjecture,
~ sP41 ).
cnf(u3541,negated_conjecture,
c1_1(a1601) ).
cnf(u4928,negated_conjecture,
~ sP42 ).
cnf(u3588,negated_conjecture,
~ c6_1(a1593) ).
cnf(u3592,negated_conjecture,
~ c3_2(a1593,a1594) ).
cnf(u3596,negated_conjecture,
~ c8_2(a1593,a1594) ).
cnf(u3600,negated_conjecture,
~ c10_2(a1593,a1594) ).
cnf(u3604,negated_conjecture,
ndr1_1(a1593) ).
cnf(u3608,negated_conjecture,
c9_1(a1593) ).
cnf(u4957,negated_conjecture,
~ sP43 ).
cnf(u3615,negated_conjecture,
~ c3_1(a1587) ).
cnf(u3622,negated_conjecture,
~ ndr1_1(a1587) ).
cnf(u3629,negated_conjecture,
c2_1(a1587) ).
cnf(u4991,negated_conjecture,
~ sP44 ).
cnf(u3784,axiom,
c5_2(a1822,a1823) ).
cnf(u3788,axiom,
~ c7_2(a1822,a1823) ).
cnf(u3792,axiom,
~ c9_2(a1822,a1823) ).
cnf(u3796,axiom,
ndr1_1(a1822) ).
cnf(u3800,axiom,
c10_1(a1822) ).
cnf(u3804,axiom,
~ c4_1(a1822) ).
cnf(u3887,axiom,
~ c2_1(a1795) ).
cnf(u3891,axiom,
~ c2_2(a1795,a1797) ).
cnf(u3895,axiom,
c10_2(a1795,a1797) ).
cnf(u3899,axiom,
~ c8_2(a1795,a1797) ).
cnf(u3903,axiom,
ndr1_1(a1795) ).
cnf(u3907,axiom,
c6_2(a1795,a1796) ).
cnf(u3911,axiom,
~ c5_2(a1795,a1796) ).
cnf(u3915,axiom,
~ c10_2(a1795,a1796) ).
cnf(u4348,axiom,
c7_2(a1723,a1724) ).
cnf(u4352,axiom,
c5_2(a1723,a1724) ).
cnf(u4356,axiom,
c9_2(a1723,a1724) ).
cnf(u4360,axiom,
ndr1_1(a1723) ).
cnf(u4365,axiom,
( c6_2(a1723,X0)
| c9_2(a1723,X0)
| ~ c3_2(a1723,X0) ) ).
cnf(u4369,axiom,
~ c5_1(a1723) ).
cnf(u4616,axiom,
~ c5_1(a1659) ).
cnf(u4620,axiom,
c9_2(a1659,a1661) ).
cnf(u4624,axiom,
~ c1_2(a1659,a1661) ).
cnf(u4628,axiom,
c4_2(a1659,a1661) ).
cnf(u4632,axiom,
ndr1_1(a1659) ).
cnf(u4636,axiom,
c3_2(a1659,a1660) ).
cnf(u4640,axiom,
c5_2(a1659,a1660) ).
cnf(u4644,axiom,
c4_2(a1659,a1660) ).
cnf(u4866,axiom,
c3_1(a1609) ).
cnf(u4870,axiom,
~ c2_1(a1609) ).
cnf(u4874,axiom,
c10_1(a1609) ).
cnf(u5019,negated_conjecture,
( ~ ndr1_1(X123)
| ~ c8_1(X123)
| c10_2(X123,X124)
| c7_2(X123,X124)
| ~ c6_2(X123,X124)
| ~ c2_1(X123) ) ).
cnf(u5082,negated_conjecture,
( ~ c2_2(a1824,X1)
| ~ c3_2(a1824,X1)
| c5_2(a1824,X1) ) ).
cnf(u5183,negated_conjecture,
~ c8_1(a1593) ).
cnf(u5599,negated_conjecture,
~ c1_1(a1593) ).
cnf(u5221,negated_conjecture,
c3_2(a1593,a1772) ).
cnf(u5234,negated_conjecture,
~ c2_1(a1820) ).
cnf(u6666,negated_conjecture,
c8_1(a1820) ).
cnf(u5276,negated_conjecture,
~ c5_1(a1694) ).
cnf(u5379,negated_conjecture,
c3_2(a1795,a1772) ).
cnf(u5388,negated_conjecture,
~ c2_1(a1723) ).
cnf(u5401,negated_conjecture,
c3_2(a1723,a1772) ).
cnf(u5404,negated_conjecture,
( ~ c8_2(a1723,X0)
| ~ c1_2(a1723,X0) ) ).
cnf(u5410,negated_conjecture,
~ c2_1(a1700) ).
cnf(u5423,negated_conjecture,
c3_2(a1700,a1772) ).
cnf(u5433,negated_conjecture,
~ c2_1(a1822) ).
cnf(u5443,negated_conjecture,
( ~ c2_2(a1822,X1)
| c10_2(a1822,X1)
| c9_2(a1822,X1) ) ).
cnf(u5457,negated_conjecture,
( c2_2(a1736,X0)
| c10_2(a1736,X0)
| c1_2(a1736,X0) ) ).
cnf(u5470,negated_conjecture,
( ~ c10_2(a1743,X0)
| ~ c7_2(a1743,X0)
| c6_2(a1743,X0) ) ).
cnf(u5480,negated_conjecture,
( ~ c10_2(a1655,X0)
| ~ c7_2(a1655,X0)
| c6_2(a1655,X0) ) ).
cnf(u5491,negated_conjecture,
~ c10_1(a1694) ).
cnf(u5501,negated_conjecture,
~ c4_2(a1723,a1724) ).
cnf(u5515,negated_conjecture,
~ c8_2(a1802,a1803) ).
cnf(u5525,negated_conjecture,
~ c2_1(a1659) ).
cnf(u5535,negated_conjecture,
( ~ c2_2(a1659,X1)
| c10_2(a1659,X1)
| c9_2(a1659,X1) ) ).
cnf(u5547,negated_conjecture,
~ c2_1(a1655) ).
cnf(u5563,negated_conjecture,
( ~ c8_2(a1655,X0)
| ~ c1_2(a1655,X0) ) ).
cnf(u5569,negated_conjecture,
~ c2_1(a1743) ).
cnf(u5579,negated_conjecture,
( ~ c2_2(a1743,X1)
| c10_2(a1743,X1)
| c9_2(a1743,X1) ) ).
cnf(u5594,negated_conjecture,
~ c10_1(a1593) ).
cnf(u5605,negated_conjecture,
~ c2_1(a1618) ).
cnf(u5914,negated_conjecture,
c8_1(a1618) ).
cnf(u5621,negated_conjecture,
( ~ c8_2(a1618,X0)
| ~ c1_2(a1618,X0) ) ).
cnf(u5633,negated_conjecture,
( c2_2(a1655,X0)
| c10_2(a1655,X0)
| c1_2(a1655,X0) ) ).
cnf(u5641,negated_conjecture,
c1_2(a1655,a1689) ).
cnf(u5684,negated_conjecture,
c9_2(a1618,a1607) ).
cnf(u5687,negated_conjecture,
c6_1(a1618) ).
cnf(u5691,negated_conjecture,
~ c6_2(a1618,a1607) ).
cnf(u5695,negated_conjecture,
~ c8_2(a1618,a1607) ).
cnf(u5706,negated_conjecture,
( ~ c6_2(a1618,X0)
| ~ c1_2(a1618,X0)
| c2_2(a1618,X0) ) ).
cnf(u5710,negated_conjecture,
c1_1(a1618) ).
cnf(u5717,negated_conjecture,
( ~ c9_2(a1618,X1)
| c2_2(a1618,X1) ) ).
cnf(u5734,negated_conjecture,
~ c1_2(a1618,a1690) ).
cnf(u5752,negated_conjecture,
c7_2(a1618,a1607) ).
cnf(u5766,negated_conjecture,
( ~ c8_2(a1683,X0)
| ~ c1_2(a1683,X0) ) ).
cnf(u5778,negated_conjecture,
~ c3_2(a1655,a1689) ).
cnf(u5792,negated_conjecture,
~ c1_1(a1767) ).
cnf(u5799,negated_conjecture,
c3_1(a1767) ).
cnf(u5808,negated_conjecture,
~ c2_1(a1802) ).
cnf(u5821,negated_conjecture,
c3_2(a1802,a1772) ).
cnf(u5829,negated_conjecture,
c9_2(a1743,a1744) ).
cnf(u5848,negated_conjecture,
( ~ c2_2(a1683,X1)
| ~ c3_2(a1683,X1)
| c5_2(a1683,X1) ) ).
cnf(u5855,negated_conjecture,
c2_2(a1683,a1602) ).
cnf(u5862,negated_conjecture,
~ c4_2(a1683,a1602) ).
cnf(u5872,negated_conjecture,
~ c3_2(a1683,a1602) ).
cnf(u5876,negated_conjecture,
( ~ c10_2(a1683,X0)
| ~ c7_2(a1683,X0)
| c6_2(a1683,X0) ) ).
cnf(u5895,negated_conjecture,
( c2_2(a1618,X0)
| c1_2(a1618,X0) ) ).
cnf(u5905,negated_conjecture,
( c7_2(a1618,X0)
| c1_2(a1618,X0) ) ).
cnf(u5926,negated_conjecture,
( ~ c8_2(a1618,X0)
| ~ c4_2(a1618,X0) ) ).
cnf(u5945,negated_conjecture,
~ c2_1(a1681) ).
cnf(u5967,negated_conjecture,
~ c2_1(a1767) ).
cnf(u6310,negated_conjecture,
~ ndr1_1(a1767) ).
cnf(u5978,negated_conjecture,
c8_1(a1767) ).
cnf(u5990,negated_conjecture,
~ c5_1(a1601) ).
cnf(u5997,negated_conjecture,
~ c10_1(a1601) ).
cnf(u6011,negated_conjecture,
c9_2(a1723,a1682) ).
cnf(u6448,negated_conjecture,
c7_1(a1723) ).
cnf(u6041,negated_conjecture,
~ c4_1(a1700) ).
cnf(u6026,negated_conjecture,
~ c1_1(a1700) ).
cnf(u6030,negated_conjecture,
c10_1(a1700) ).
cnf(u6068,negated_conjecture,
~ c6_2(a1752,a1710) ).
cnf(u6081,negated_conjecture,
c9_2(a1802,a1682) ).
cnf(u6096,negated_conjecture,
~ c2_1(a1729) ).
cnf(u6373,negated_conjecture,
~ ndr1_1(a1729) ).
cnf(u6800,negated_conjecture,
~ c10_1(a1729) ).
cnf(u6110,negated_conjecture,
c8_1(a1729) ).
cnf(u6150,negated_conjecture,
~ c10_1(a1618) ).
cnf(u6220,negated_conjecture,
c1_1(a1723) ).
cnf(u6691,negated_conjecture,
~ c1_1(a1683) ).
cnf(u6283,negated_conjecture,
( ~ c8_2(a1618,X0)
| c3_2(a1618,X0)
| ~ c7_2(a1618,X0) ) ).
cnf(u6297,negated_conjecture,
~ c7_1(a1683) ).
cnf(u6302,negated_conjecture,
~ c6_1(a1813) ).
cnf(u6359,negated_conjecture,
c6_1(a1729) ).
cnf(u6414,negated_conjecture,
c5_2(a1802,a1728) ).
cnf(u6433,negated_conjecture,
~ c1_2(a1743,a1728) ).
cnf(u6468,negated_conjecture,
( ~ c8_2(a1736,X0)
| ~ c1_2(a1736,X0) ) ).
cnf(u6474,negated_conjecture,
c10_2(a1736,a1772) ).
cnf(u6478,negated_conjecture,
( ~ c10_2(a1736,X1)
| ~ c7_2(a1736,X1)
| c6_2(a1736,X1) ) ).
cnf(u6492,negated_conjecture,
~ c7_2(a1736,a1772) ).
cnf(u6512,negated_conjecture,
~ c2_1(a1626) ).
cnf(u6519,negated_conjecture,
ndr1_1(a1626) ).
cnf(u6584,negated_conjecture,
~ c10_1(a1626) ).
cnf(u6526,negated_conjecture,
c8_1(a1626) ).
cnf(u6538,negated_conjecture,
( ~ c2_2(a1626,X1)
| ~ c3_2(a1626,X1)
| c5_2(a1626,X1) ) ).
cnf(u6548,negated_conjecture,
( ~ c8_2(a1626,X0)
| c3_2(a1626,X0)
| ~ c7_2(a1626,X0) ) ).
cnf(u6575,negated_conjecture,
~ c6_2(a1626,a1607) ).
cnf(u6579,negated_conjecture,
~ c8_2(a1626,a1607) ).
cnf(u6596,negated_conjecture,
( ~ c1_2(a1626,X0)
| ~ c6_2(a1626,X0)
| c2_2(a1626,X0) ) ).
cnf(u6601,negated_conjecture,
( ~ c9_2(a1626,X1)
| c2_2(a1626,X1) ) ).
cnf(u6619,negated_conjecture,
~ c4_1(a1609) ).
cnf(u6640,negated_conjecture,
( ~ c8_2(a1626,X0)
| ~ c1_2(a1626,X0) ) ).
cnf(u6650,negated_conjecture,
~ c1_1(a1820) ).
cnf(u6654,negated_conjecture,
c3_1(a1820) ).
cnf(u6679,negated_conjecture,
~ c6_1(a1824) ).
cnf(u6698,negated_conjecture,
c3_1(a1683) ).
cnf(u6714,negated_conjecture,
~ ndr1_1(a1601) ).
cnf(u6751,negated_conjecture,
~ c3_2(a1795,a1796) ).
cnf(u6834,negated_conjecture,
c1_2(a1618,a1765) ).
cnf(u6854,negated_conjecture,
( ~ c3_2(a1618,X0)
| ~ c2_2(a1618,X0)
| c9_2(a1618,X0) ) ).
cnf(u6877,negated_conjecture,
( ~ c2_2(a1752,X1)
| c10_2(a1752,X1)
| c9_2(a1752,X1) ) ).
cnf(u6899,negated_conjecture,
c2_1(a1736) ).
cnf(u6912,negated_conjecture,
( ~ c2_2(a1723,X0)
| c9_2(a1723,X0)
| ~ c3_2(a1723,X0) ) ).
cnf(u6922,negated_conjecture,
c6_2(a1655,a1780) ).
cnf(u6948,negated_conjecture,
~ c3_2(a1655,a1780) ).
cnf(u5783,negated_conjecture,
( ~ c6_1(X0)
| c6_2(X0,a1780)
| ~ ndr1_1(X0)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u5093,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u5623,negated_conjecture,
( ~ c8_2(X0,a1690)
| c5_2(X0,a1792)
| ~ ndr1_1(X0)
| ~ c4_2(X0,a1690)
| c1_2(X0,a1689) ) ).
cnf(u6138,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_2(X0,a1764)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c3_1(X0)
| c10_1(X0) ) ).
cnf(u5670,negated_conjecture,
( ~ c7_1(X0)
| c4_2(X0,a1764)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c9_2(X0,a1682)
| c1_2(X0,a1765) ) ).
cnf(u6783,negated_conjecture,
~ c6_1(a1609) ).
cnf(u6070,negated_conjecture,
c6_1(a1601) ).
cnf(u5699,negated_conjecture,
( ~ c10_2(a1618,X0)
| c2_2(a1618,X0)
| c1_2(a1618,X0) ) ).
cnf(u5661,negated_conjecture,
( ~ c7_1(X0)
| c9_2(X0,a1764)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c9_2(X0,a1682)
| c1_2(X0,a1765) ) ).
cnf(u5834,negated_conjecture,
( ~ c6_1(X0)
| c7_2(X0,a1780)
| ~ ndr1_1(X0)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u6055,negated_conjecture,
ndr1_1(a1752) ).
cnf(u6505,negated_conjecture,
~ c1_1(a1626) ).
cnf(u5165,negated_conjecture,
c6_1(a1704) ).
cnf(u5091,negated_conjecture,
( c10_1(X0)
| ndr1_1(X0)
| c8_1(X0) ) ).
cnf(u6776,negated_conjecture,
( c4_2(X0,a1764)
| c1_2(X0,a1690)
| ~ c3_2(X0,a1690)
| ~ ndr1_1(X0)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c3_1(X0)
| c10_1(X0)
| c1_2(X0,a1689) ) ).
cnf(u5738,negated_conjecture,
( ~ c9_2(X0,a1710)
| c5_1(X0)
| c10_1(X0)
| c2_1(X0)
| c8_1(X0) ) ).
cnf(u5839,negated_conjecture,
~ c6_1(a1822) ).
cnf(u6071,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| c4_2(X0,a1764)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c3_1(X0)
| c10_1(X0) ) ).
cnf(u6445,negated_conjecture,
c6_1(a1723) ).
cnf(u5723,negated_conjecture,
c2_2(a1618,a1607) ).
cnf(u6139,negated_conjecture,
( ~ c1_1(X0)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c2_2(X0,a1764)
| c4_1(X0) ) ).
cnf(u5496,negated_conjecture,
( ~ c8_2(X0,a1690)
| c4_2(X0,a1792)
| ~ ndr1_1(X0)
| ~ c4_2(X0,a1690)
| c1_2(X0,a1689) ) ).
cnf(u6598,negated_conjecture,
( ~ c9_2(a1626,X0)
| ~ c7_2(a1626,X0)
| ~ c3_2(a1626,X0) ) ).
cnf(u5282,negated_conjecture,
c3_2(a1618,a1619) ).
cnf(u5428,negated_conjecture,
( ~ c10_1(X0)
| ndr1_1(X0)
| c2_1(X0)
| ~ c6_1(X0) ) ).
cnf(u6774,negated_conjecture,
~ c6_1(a1700) ).
cnf(u5666,negated_conjecture,
( ~ c7_1(X0)
| c2_2(X0,a1764)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c9_2(X0,a1682)
| c1_2(X0,a1765) ) ).
cnf(u709,negated_conjecture,
~ c5_1(a1767) ).
cnf(u6589,negated_conjecture,
( ~ c10_2(a1626,X0)
| c2_2(a1626,X0)
| c1_2(a1626,X0) ) ).
cnf(u6143,negated_conjecture,
~ c6_1(a1647) ).
cnf(u5836,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,a1780)
| ~ ndr1_1(X0)
| c9_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u6134,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| c9_2(X0,a1764)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c3_1(X0)
| c10_1(X0) ) ).
cnf(u699,negated_conjecture,
c7_0 ).
cnf(u5067,negated_conjecture,
( ~ c5_1(X32)
| c9_1(X32) ) ).
cnf(u5681,negated_conjecture,
c9_1(a1618) ).
cnf(u5726,negated_conjecture,
~ c10_1(a1667) ).
cnf(u5722,negated_conjecture,
c2_2(a1618,a1619) ).
cnf(u5092,negated_conjecture,
( c6_2(X0,a1653)
| ndr1_1(X0)
| c8_1(X0) ) ).
cnf(u710,negated_conjecture,
~ c7_1(a1767) ).
cnf(u5591,negated_conjecture,
~ c5_1(a1593) ).
cnf(u6730,negated_conjecture,
( ~ c3_2(X0,a1690)
| c1_2(X0,a1690)
| ~ ndr1_1(X0)
| c2_2(X0,a1764)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c3_1(X0)
| c10_1(X0)
| c1_2(X0,a1689) ) ).
cnf(u6090,negated_conjecture,
~ c1_1(a1729) ).
cnf(u5226,negated_conjecture,
( ~ c3_1(X33)
| ~ c1_1(X33) ) ).
cnf(u5939,negated_conjecture,
~ c1_1(a1681) ).
cnf(u5935,negated_conjecture,
~ c4_2(a1618,a1619) ).
cnf(u6764,negated_conjecture,
( ~ c3_2(X0,a1690)
| c1_2(X0,a1690)
| ~ ndr1_1(X0)
| c9_2(X0,a1764)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c3_1(X0)
| c10_1(X0)
| c1_2(X0,a1689) ) ).
cnf(u6072,negated_conjecture,
( ~ c1_1(X0)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c4_2(X0,a1764)
| c4_1(X0) ) ).
cnf(u6606,negated_conjecture,
~ c1_1(a1609) ).
cnf(u6354,negated_conjecture,
c9_1(a1729) ).
cnf(u6135,negated_conjecture,
( ~ c1_1(X0)
| ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c9_2(X0,a1682)
| c1_2(X0,a1765)
| c9_2(X0,a1764)
| c4_1(X0) ) ).
cnf(u6454,negated_conjecture,
ndr1_1(a1736) ).
cnf(u5937,negated_conjecture,
~ c1_2(a1618,a1619) ).
cnf(u6401,negated_conjecture,
( c5_2(X0,a1728)
| c1_2(X0,a1690)
| ~ ndr1_1(X0)
| c2_2(X0,a1690)
| c1_1(X0)
| c1_2(X0,a1689) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN427+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 15:58:57 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.75/2.02 % (3979130)Detected formulas, will run a generic FOF schedule.
% 7.75/2.02 % (3979135)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=4292553279:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.75/2.02 % (3979139)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2491861587:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.75/2.02 % (3979140)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=553165184:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.75/2.02 % (3979141)dis-21_1_sil=8000:lcm=predicate:random_seed=1999433661: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)
% 7.75/2.02 % (3979138)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2803952411:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.75/2.02 % (3979136)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=3078312203:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.75/2.02 % (3979137)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=596829203:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.75/2.02 % (3979140)Refutation not found, incomplete strategy
% 7.75/2.02 % (3979140)------------------------------
% 7.75/2.02 % (3979140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979140)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979140)Termination reason: Refutation not found, incomplete strategy
% 7.75/2.02 % (3979140)Time elapsed: 0.051 s
% 7.75/2.02 % (3979140)Peak memory usage: 92 MB
% 7.75/2.02 % (3979140)Instructions burned: 86 (million)
% 7.75/2.02 % (3979138)Instruction limit reached!
% 7.75/2.02 % (3979138)------------------------------
% 7.75/2.02 % (3979138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979138)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979138)Termination reason: Instruction limit
% 7.75/2.02 % (3979138)Termination phase: Saturation
% 7.75/2.02 % (3979138)Time elapsed: 0.061 s
% 7.75/2.02 % (3979138)Peak memory usage: 91 MB
% 7.75/2.02 % (3979138)Instructions burned: 110 (million)
% 7.75/2.02 % (3979139)Instruction limit reached!
% 7.75/2.02 % (3979139)------------------------------
% 7.75/2.02 % (3979139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979139)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979139)Termination reason: Instruction limit
% 7.75/2.02 % (3979139)Termination phase: Saturation
% 7.75/2.02 % (3979139)Time elapsed: 0.064 s
% 7.75/2.02 % (3979139)Peak memory usage: 89 MB
% 7.75/2.02 % (3979139)Instructions burned: 119 (million)
% 7.75/2.02 % (3979141)Instruction limit reached!
% 7.75/2.02 % (3979141)------------------------------
% 7.75/2.02 % (3979141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979141)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979141)Termination reason: Instruction limit
% 7.75/2.02 % (3979141)Termination phase: Saturation
% 7.75/2.02 % (3979141)Time elapsed: 0.071 s
% 7.75/2.02 % (3979141)Peak memory usage: 91 MB
% 7.75/2.02 % (3979141)Instructions burned: 130 (million)
% 7.75/2.02 % (3979150)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3867251512:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.75/2.02 % (3979149)lrs+10_1_sil=8000:sp=occurrence:random_seed=694822665:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.75/2.02 % (3979151)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3003455530:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.75/2.02 % (3979150)Refutation not found, incomplete strategy
% 7.75/2.02 % (3979150)------------------------------
% 7.75/2.02 % (3979150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979150)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979150)Termination reason: Refutation not found, incomplete strategy
% 7.75/2.02 % (3979150)Time elapsed: 0.038 s
% 7.75/2.02 % (3979150)Peak memory usage: 92 MB
% 7.75/2.02 % (3979150)Instructions burned: 63 (million)
% 7.75/2.02 % (3979151)Refutation not found, incomplete strategy
% 7.75/2.02 % (3979151)------------------------------
% 7.75/2.02 % (3979151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979151)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979151)Termination reason: Refutation not found, incomplete strategy
% 7.75/2.02 % (3979151)Time elapsed: 0.064 s
% 7.75/2.02 % (3979151)Peak memory usage: 92 MB
% 7.75/2.02 % (3979151)Instructions burned: 109 (million)
% 7.75/2.02 % (3979140)------------------------------
% 7.75/2.02 % (3979140)------------------------------
% 7.75/2.02 % (3979149)Instruction limit reached!
% 7.75/2.02 % (3979149)------------------------------
% 7.75/2.02 % (3979149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979149)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979149)Termination reason: Instruction limit
% 7.75/2.02 % (3979149)Termination phase: Saturation
% 7.75/2.02 % (3979149)Time elapsed: 0.156 s
% 7.75/2.02 % (3979149)Peak memory usage: 94 MB
% 7.75/2.02 % (3979149)Instructions burned: 286 (million)
% 7.75/2.02 % (3979155)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=2019800716:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 7.75/2.02 % (3979150)------------------------------
% 7.75/2.02 % (3979150)------------------------------
% 7.75/2.02 % (3979155)Refutation not found, incomplete strategy
% 7.75/2.02 % (3979155)------------------------------
% 7.75/2.02 % (3979155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979155)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979155)Termination reason: Refutation not found, incomplete strategy
% 7.75/2.02 % (3979155)Time elapsed: 0.048 s
% 7.75/2.02 % (3979155)Peak memory usage: 92 MB
% 7.75/2.02 % (3979155)Instructions burned: 80 (million)
% 7.75/2.02 % (3979156)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=676832758:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 7.75/2.02 % (3979151)------------------------------
% 7.75/2.02 % (3979151)------------------------------
% 7.75/2.02 % (3979158)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3541464959:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 7.75/2.02 % (3979156)Instruction limit reached!
% 7.75/2.02 % (3979156)------------------------------
% 7.75/2.02 % (3979156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979156)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979156)Termination reason: Instruction limit
% 7.75/2.02 % (3979156)Termination phase: Saturation
% 7.75/2.02 % (3979156)Time elapsed: 0.168 s
% 7.75/2.02 % (3979156)Peak memory usage: 93 MB
% 7.75/2.02 % (3979156)Instructions burned: 295 (million)
% 7.75/2.02 % (3979160)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3860639710:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 7.75/2.02 % (3979155)------------------------------
% 7.75/2.02 % (3979155)------------------------------
% 7.75/2.02 % (3979160)Instruction limit reached!
% 7.75/2.02 % (3979160)------------------------------
% 7.75/2.02 % (3979160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979160)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979160)Termination reason: Instruction limit
% 7.75/2.02 % (3979160)Termination phase: Saturation
% 7.75/2.02 % (3979160)Time elapsed: 0.066 s
% 7.75/2.02 % (3979160)Peak memory usage: 92 MB
% 7.75/2.02 % (3979160)Instructions burned: 114 (million)
% 7.75/2.02 % (3979163)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1409296762:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 7.75/2.02 % (3979163)Instruction limit reached!
% 7.75/2.02 % (3979163)------------------------------
% 7.75/2.02 % (3979163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979163)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979163)Termination reason: Instruction limit
% 7.75/2.02 % (3979163)Termination phase: Saturation
% 7.75/2.02 % (3979163)Time elapsed: 0.067 s
% 7.75/2.02 % (3979163)Peak memory usage: 90 MB
% 7.75/2.02 % (3979163)Instructions burned: 128 (million)
% 7.75/2.02 % (3979164)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3812118803:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 7.75/2.02 % (3979165)lrs+10_1_sil=8000:sp=occurrence:random_seed=1436071737:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 7.75/2.02 % (3979164)Instruction limit reached!
% 7.75/2.02 % (3979164)------------------------------
% 7.75/2.02 % (3979164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3979164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3979164)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3979164)Termination reason: Instruction limit
% 7.75/2.02 % (3979164)Termination phase: Saturation
% 7.75/2.02 % (3979164)Time elapsed: 0.051 s
% 7.75/2.02 % (3979164)Peak memory usage: 90 MB
% 7.75/2.02 % (3979164)Instructions burned: 115 (million)
% 7.75/2.02 % (3979136)First to succeed.
% 7.75/2.02 % (3979136)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3979130"
% 7.75/2.02 % (3979167)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1304944995:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 7.75/2.02 % (3979170)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2672005018:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 7.75/2.02 % SZS status CounterSatisfiable for theBenchmark
% 7.75/2.02 % SZS output start Saturation.
% See solution above
% 7.75/2.03 % SZS output start Definitions and Model Updates.
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_1(X0) | c8_2(X0,a1754) | ndr1_1(X0) | ~ndr1_0 | ~sP15 is false, set c8_2(X0,a1754) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c8_2(X0,a1649) | ~ndr1_0 | ~sP32 is false, set c8_2(X0,a1649) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_1(X0) | c8_2(X0,a1737) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set c8_2(X0,a1737) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X161) | c2_1(X161) | ~c3_2(X161,a1778) | ~ndr1_0 | ~c4_0 | ~c6_1(X162) | c7_1(X162) | ~c4_2(X162,X163) | ~c8_2(X162,X163) | c1_2(X162,X163) | ~ndr1_1(X162) | ~ndr1_0 is false, set ~c3_2(X161,a1778) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X80,a1689) | ndr1_1(X80) | ~ndr1_0 | c8_0 | c10_0 is false, set ~c3_2(X80,a1689) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c6_1(X0) | ~c3_2(X0,a1776) | ~ndr1_0 | ~sP11 is false, set ~c3_2(X0,a1776) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_0 | ndr1_1(X28) | ~c3_2(X28,a1628) | ~c9_1(X28) | ~ndr1_0 is false, set ~c3_2(X28,a1628) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_1(X17) | c8_1(X17) | c10_1(X17) | ~ndr1_0 | c3_1(X18) | ndr1_1(X18) | ~c3_2(X18,a1614) | ~ndr1_0 is false, set ~c3_2(X18,a1614) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c1_2(X0,a1649) | ~ndr1_0 | ~sP32 is false, set ~c1_2(X0,a1649) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_0 | ~c1_2(X28,a1627) | ndr1_1(X28) | ~c9_1(X28) | ~ndr1_0 is false, set ~c1_2(X28,a1627) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_1(X17) | c8_1(X17) | c10_1(X17) | ~ndr1_0 | c3_1(X18) | ~c1_2(X18,a1613) | ndr1_1(X18) | ~ndr1_0 is false, set ~c1_2(X18,a1613) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X161) | c2_1(X161) | ~c5_2(X161,a1778) | ~ndr1_0 | ~c4_0 | ~c6_1(X162) | c7_1(X162) | ~c4_2(X162,X163) | ~c8_2(X162,X163) | c1_2(X162,X163) | ~ndr1_1(X162) | ~ndr1_0 is false, set ~c5_2(X161,a1778) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c5_2(X0,a1793) | c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~c5_2(X0,a1793) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c3_2(X161,a1777) | c2_1(X161) | ndr1_1(X161) | ~ndr1_0 | ~c4_0 | ~c6_1(X162) | c7_1(X162) | ~c4_2(X162,X163) | ~c8_2(X162,X163) | c1_2(X162,X163) | ~ndr1_1(X162) | ~ndr1_0 is false, set c3_2(X161,a1777) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c3_2(X0,a1648) | ndr1_1(X0) | ~ndr1_0 | ~sP32 is false, set c3_2(X0,a1648) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c3_2(X0,a1596) | c7_1(X0) | ~ndr1_0 | ~sP42 is false, set c3_2(X0,a1596) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c3_2(X0,a1762) | ~c10_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set c3_2(X0,a1762) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c3_2(X0,a1595) | ndr1_1(X0) | c7_1(X0) | ~ndr1_0 | ~sP42 is false, set c3_2(X0,a1595) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c2_2(X0,a1762) | ~c10_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set ~c2_2(X0,a1762) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c2_2(X161,a1777) | c2_1(X161) | ndr1_1(X161) | ~ndr1_0 | ~c4_0 | ~c6_1(X162) | c7_1(X162) | ~c4_2(X162,X163) | ~c8_2(X162,X163) | c1_2(X162,X163) | ~ndr1_1(X162) | ~ndr1_0 is false, set ~c2_2(X161,a1777) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X80) | ~c2_2(X80,a1690) | ~ndr1_0 | c8_0 | c10_0 is false, set ~c2_2(X80,a1690) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c2_2(X0,a1623) | ndr1_1(X0) | ~c9_1(X0) | ~ndr1_0 | ~sP36 is false, set ~c2_2(X0,a1623) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_1(X0) | ndr1_1(X0) | ~c2_2(X0,a1738) | ~ndr1_0 | ~sP18 is false, set ~c2_2(X0,a1738) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X80) | c7_2(X80,a1690) | ~ndr1_0 | c8_0 | c10_0 is false, set c7_2(X80,a1690) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c7_2(X0,a1649) | ~ndr1_0 | ~sP32 is false, set c7_2(X0,a1649) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c7_2(X193,a1832) | ndr1_1(X193) | c6_1(X193) | ~ndr1_0 | c9_0 | ~c5_2(X194,X195) | c8_2(X194,X195) | c2_2(X194,X195) | ~ndr1_1(X194) | c7_1(X194) | ~c4_1(X194) | ~ndr1_0 is false, set c7_2(X193,a1832) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c10_2(X0,a1648) | ndr1_1(X0) | ~ndr1_0 | ~sP32 is false, set c10_2(X0,a1648) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_1(X0) | ndr1_1(X0) | c10_2(X0,a1755) | ~ndr1_0 | ~sP15 is false, set c10_2(X0,a1755) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_0 | ndr1_1(X28) | c10_2(X28,a1628) | ~c9_1(X28) | ~ndr1_0 is false, set c10_2(X28,a1628) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c4_2(X0,a1624) | ~c9_1(X0) | ~ndr1_0 | ~sP36 is false, set c4_2(X0,a1624) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_1(X0) | c4_2(X0,a1754) | ndr1_1(X0) | ~ndr1_0 | ~sP15 is false, set c4_2(X0,a1754) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c4_2(X0,a1595) | ndr1_1(X0) | c7_1(X0) | ~ndr1_0 | ~sP42 is false, set c4_2(X0,a1595) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_1(X17) | c8_1(X17) | c10_1(X17) | ~ndr1_0 | c3_1(X18) | ndr1_1(X18) | c4_2(X18,a1614) | ~ndr1_0 is false, set c4_2(X18,a1614) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_1(X0) | ndr1_1(X0) | c9_2(X0,a1738) | ~ndr1_0 | ~sP18 is false, set c9_2(X0,a1738) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X193) | c9_2(X193,a1833) | c6_1(X193) | ~ndr1_0 | c9_0 | ~c5_2(X194,X195) | c8_2(X194,X195) | c2_2(X194,X195) | ~ndr1_1(X194) | c7_1(X194) | ~c4_1(X194) | ~ndr1_0 is false, set c9_2(X193,a1833) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_0 | ndr1_1(X28) | c9_2(X28,a1628) | ~c9_1(X28) | ~ndr1_0 is false, set c9_2(X28,a1628) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c6_2(X0,a1623) | ndr1_1(X0) | ~c9_1(X0) | ~ndr1_0 | ~sP36 is false, set ~c6_2(X0,a1623) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c6_2(X0,a1595) | ndr1_1(X0) | c7_1(X0) | ~ndr1_0 | ~sP42 is false, set c6_2(X0,a1595) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c10_1(X0) | c6_2(X0,a1763) | ~ndr1_0 | ~sP13 is false, set c6_2(X0,a1763) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c5_1(X0) | c6_2(X0,a1801) | ~ndr1_0 | ~sP6 is false, set c6_2(X0,a1801) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X80) | c6_2(X80,a1690) | ~ndr1_0 | c8_0 | c10_0 is false, set c6_2(X80,a1690) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X193) | c6_2(X193,a1833) | c6_1(X193) | ~ndr1_0 | c9_0 | ~c5_2(X194,X195) | c8_2(X194,X195) | c2_2(X194,X195) | ~ndr1_1(X194) | c7_1(X194) | ~c4_1(X194) | ~ndr1_0 is false, set c6_2(X193,a1833) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c6_1(X0) | ~c9_2(X0,a1776) | ~ndr1_0 | ~sP11 is false, set ~c9_2(X0,a1776) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c9_2(X0,a1775) | ~c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c9_2(X0,a1775) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_1(X17) | c8_1(X17) | c10_1(X17) | ~ndr1_0 | c3_1(X18) | ~c9_2(X18,a1613) | ndr1_1(X18) | ~ndr1_0 is false, set ~c9_2(X18,a1613) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_1(X17) | c8_1(X17) | c10_1(X17) | ~ndr1_0 | c3_1(X18) | ndr1_1(X18) | ~c9_2(X18,a1614) | ~ndr1_0 is false, set ~c9_2(X18,a1614) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c9_2(X80,a1689) | ndr1_1(X80) | ~ndr1_0 | c8_0 | c10_0 is false, set ~c9_2(X80,a1689) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_2(X0,a1623) | ndr1_1(X0) | ~c9_1(X0) | ~ndr1_0 | ~sP36 is false, set ~c10_2(X0,a1623) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_1(X0) | ~c10_2(X0,a1737) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~c10_2(X0,a1737) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_2(X0,a1762) | ~c10_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP13 is false, set ~c10_2(X0,a1762) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c6_1(X0) | ~c10_2(X0,a1794) | ~ndr1_0 | ~sP8 is false, set ~c10_2(X0,a1794) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_2(X0,a1800) | c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c10_2(X0,a1800) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c5_1(X0) | ~c10_2(X0,a1801) | ~ndr1_0 | ~sP6 is false, set ~c10_2(X0,a1801) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_0 | ~c10_2(X28,a1627) | ndr1_1(X28) | ~c9_1(X28) | ~ndr1_0 is false, set ~c10_2(X28,a1627) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_1(X0) | ndr1_1(X0) | c1_2(X0,a1755) | ~ndr1_0 | ~sP15 is false, set c1_2(X0,a1755) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c1_2(X80,a1689) | ndr1_1(X80) | ~ndr1_0 | c8_0 | c10_0 is false, set c1_2(X80,a1689) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c1_2(X193,a1832) | ndr1_1(X193) | c6_1(X193) | ~ndr1_0 | c9_0 | ~c5_2(X194,X195) | c8_2(X194,X195) | c2_2(X194,X195) | ~ndr1_1(X194) | c7_1(X194) | ~c4_1(X194) | ~ndr1_0 is false, set c1_2(X193,a1832) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c1_2(X0,a1624) | ~c9_1(X0) | ~ndr1_0 | ~sP36 is false, set c1_2(X0,a1624) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_1(X0) | ndr1_1(X0) | ~c4_2(X0,a1738) | ~ndr1_0 | ~sP18 is false, set ~c4_2(X0,a1738) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c4_2(X193,a1832) | ndr1_1(X193) | c6_1(X193) | ~ndr1_0 | c9_0 | ~c5_2(X194,X195) | c8_2(X194,X195) | c2_2(X194,X195) | ~ndr1_1(X194) | c7_1(X194) | ~c4_1(X194) | ~ndr1_0 is false, set ~c4_2(X193,a1832) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c10_1(X0) | ~c4_2(X0,a1763) | ~ndr1_0 | ~sP13 is false, set ~c4_2(X0,a1763) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c6_1(X0) | ~c4_2(X0,a1794) | ~ndr1_0 | ~sP8 is false, set ~c4_2(X0,a1794) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c5_1(X0) | ~c4_2(X0,a1801) | ~ndr1_0 | ~sP6 is false, set ~c4_2(X0,a1801) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_2(X0,a1775) | ~c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c8_2(X0,a1775) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_2(X0,a1793) | c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~c8_2(X0,a1793) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_2(X161,a1777) | c2_1(X161) | ndr1_1(X161) | ~ndr1_0 | ~c4_0 | ~c6_1(X162) | c7_1(X162) | ~c4_2(X162,X163) | ~c8_2(X162,X163) | c1_2(X162,X163) | ~ndr1_1(X162) | ~ndr1_0 is false, set ~c8_2(X161,a1777) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c2_2(X0,a1648) | ndr1_1(X0) | ~ndr1_0 | ~sP32 is false, set c2_2(X0,a1648) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_1(X0) | ndr1_1(X0) | c2_2(X0,a1755) | ~ndr1_0 | ~sP15 is false, set c2_2(X0,a1755) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_1(X0) | c2_2(X0,a1754) | ndr1_1(X0) | ~ndr1_0 | ~sP15 is false, set c2_2(X0,a1754) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c2_2(X0,a1800) | c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c2_2(X0,a1800) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X193) | c2_2(X193,a1833) | c6_1(X193) | ~ndr1_0 | c9_0 | ~c5_2(X194,X195) | c8_2(X194,X195) | c2_2(X194,X195) | ~ndr1_1(X194) | c7_1(X194) | ~c4_1(X194) | ~ndr1_0 is false, set c2_2(X193,a1833) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X53) | ~c8_1(X53) | c6_1(X53) | ~ndr1_0 | ~c9_0 | ndr1_0 is false, set ~c9_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c3_2(X53,a1666) | ~c8_1(X53) | c6_1(X53) | ~ndr1_0 | ~c9_0 | ndr1_0 is false, set ~c9_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_2(X53,a1666) | ~c8_1(X53) | c6_1(X53) | ~ndr1_0 | ~c9_0 | ndr1_0 is false, set ~c9_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c2_2(X0,a1793) | c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set c2_2(X0,a1793) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c8_0 | ~c7_2(X28,a1627) | ndr1_1(X28) | ~c9_1(X28) | ~ndr1_0 is false, set ~c7_2(X28,a1627) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_2(X0,a1775) | ~c6_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP11 is false, set ~c7_2(X0,a1775) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X161) | c2_1(X161) | ~c7_2(X161,a1778) | ~ndr1_0 | ~c4_0 | ~c6_1(X162) | c7_1(X162) | ~c4_2(X162,X163) | ~c8_2(X162,X163) | c1_2(X162,X163) | ~ndr1_1(X162) | ~ndr1_0 is false, set ~c7_2(X161,a1778) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c10_1(X0) | ~c7_2(X0,a1763) | ~ndr1_0 | ~sP13 is false, set ~c7_2(X0,a1763) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c5_2(X0,a1596) | c7_1(X0) | ~ndr1_0 | ~sP42 is false, set c5_2(X0,a1596) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | c6_1(X0) | c5_2(X0,a1794) | ~ndr1_0 | ~sP8 is false, set c5_2(X0,a1794) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X0) | ~c6_1(X0) | c5_2(X0,a1776) | ~ndr1_0 | ~sP11 is false, set c5_2(X0,a1776) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_1(X17) | c8_1(X17) | c10_1(X17) | ~ndr1_0 | c3_1(X18) | c5_2(X18,a1613) | ndr1_1(X18) | ~ndr1_0 is false, set c5_2(X18,a1613) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | ~c9_0 | ~c3_2(X176,X177) | ~c2_2(X176,X177) | c5_2(X176,X177) | ~ndr1_1(X176) | ~c8_1(X176) | c5_2(X176,X178) | ~c8_2(X176,X178) | ~c4_2(X176,X178) | ~ndr1_1(X176) | ~ndr1_0 is false, set c5_2(X176,X177) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X45) | ~c9_1(X45) | c3_2(X45,X46) | ~c8_2(X45,X46) | c6_2(X45,X46) | ~ndr1_1(X45) | ~ndr1_0 | ~c9_2(X47,X48) | c3_2(X47,X48) | ~c7_2(X47,X48) | ~ndr1_1(X47) | c3_1(X47) | ~c8_1(X47) | ~ndr1_0 | ~c1_1(X49) | c6_1(X49) | ~ndr1_0 is false, set ~c1_1(X49) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c3_0 | ~c10_1(X107) | ~c9_1(X107) | ~ndr1_0 | ndr1_1(X108) | ~c1_2(X108,X109) | ~c4_2(X108,X109) | ~c3_2(X108,X109) | ~ndr1_1(X108) | c9_1(X108) | ~ndr1_0 is false, set ~c10_1(X107) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | c3_1(X116) | ~c10_1(X116) | ~c9_1(X116) | ~ndr1_0 is false, set ~c10_1(X116) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c7_1(X89) | c9_1(X89) | c7_2(X89,X90) | c10_2(X89,X90) | c3_2(X89,X90) | ~ndr1_1(X89) | ~ndr1_0 | ndr1_0 | ndr1_1(X91) | ~c8_1(X91) | ~c10_1(X91) | ~ndr1_0 is false, set c7_1(X89) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c7_1(X89) | c9_1(X89) | c7_2(X89,X90) | c10_2(X89,X90) | c3_2(X89,X90) | ~ndr1_1(X89) | ~ndr1_0 | ndr1_0 | ~c8_2(X91,a1699) | ~c8_1(X91) | ~c10_1(X91) | ~ndr1_0 is false, set c7_1(X89) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c7_1(X89) | c9_1(X89) | c7_2(X89,X90) | c10_2(X89,X90) | c3_2(X89,X90) | ~ndr1_1(X89) | ~ndr1_0 | ndr1_0 | ~c4_2(X91,a1699) | ~c8_1(X91) | ~c10_1(X91) | ~ndr1_0 is false, set c7_1(X89) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c7_1(X89) | c9_1(X89) | c7_2(X89,X90) | c10_2(X89,X90) | c3_2(X89,X90) | ~ndr1_1(X89) | ~ndr1_0 | ndr1_0 | ~c9_2(X91,a1699) | ~c8_1(X91) | ~c10_1(X91) | ~ndr1_0 is false, set c7_1(X89) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X110,X111) | c1_2(X110,X111) | ~ndr1_1(X110) | c8_2(X110,a1716) | ~c7_1(X110) | ~ndr1_0 | ~c2_0 | ~c8_1(X112) | ndr1_1(X112) | c6_2(X112,X113) | ~c10_2(X112,X113) | c3_2(X112,X113) | ~ndr1_1(X112) | ~ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X110,X111) | c1_2(X110,X111) | ~ndr1_1(X110) | c7_2(X110,a1716) | ~c7_1(X110) | ~ndr1_0 | ~c2_0 | ~c8_1(X112) | ndr1_1(X112) | c6_2(X112,X113) | ~c10_2(X112,X113) | c3_2(X112,X113) | ~ndr1_1(X112) | ~ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c2_0 | c5_1(X42) | c10_1(X42) | ~c1_2(X42,X43) | ~c3_2(X42,X43) | ~c9_2(X42,X43) | ~ndr1_1(X42) | ~ndr1_0 | ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X110,X111) | c1_2(X110,X111) | ~ndr1_1(X110) | ndr1_1(X110) | ~c7_1(X110) | ~ndr1_0 | ~c2_0 | ~c8_1(X112) | ndr1_1(X112) | c6_2(X112,X113) | ~c10_2(X112,X113) | c3_2(X112,X113) | ~ndr1_1(X112) | ~ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X110,X111) | c1_2(X110,X111) | ~ndr1_1(X110) | ndr1_1(X110) | ~c7_1(X110) | ~ndr1_0 | ~c2_0 | ~c8_1(X112) | ~c9_2(X112,a1717) | c6_2(X112,X113) | ~c10_2(X112,X113) | c3_2(X112,X113) | ~ndr1_1(X112) | ~ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X110,X111) | c1_2(X110,X111) | ~ndr1_1(X110) | ndr1_1(X110) | ~c7_1(X110) | ~ndr1_0 | ~c2_0 | ~c8_1(X112) | ~c10_2(X112,a1717) | c6_2(X112,X113) | ~c10_2(X112,X113) | c3_2(X112,X113) | ~ndr1_1(X112) | ~ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c3_2(X110,X111) | c1_2(X110,X111) | ~ndr1_1(X110) | c10_2(X110,a1716) | ~c7_1(X110) | ~ndr1_0 | ~c2_0 | ~c8_1(X112) | ndr1_1(X112) | c6_2(X112,X113) | ~c10_2(X112,X113) | c3_2(X112,X113) | ~ndr1_1(X112) | ~ndr1_0 is false, set ~c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c6_1(X117) | c9_1(X117) | ~c5_1(X117) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X117) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c4_0 | c7_2(X84,X85) | ~c4_2(X84,X85) | ~c8_2(X84,X85) | ~ndr1_1(X84) | c8_1(X84) | ~ndr1_0 | ndr1_0 is false, set c4_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_0 | ~c1_0 | ~c3_1(X134) | c4_2(X134,X135) | c2_2(X134,X135) | c5_2(X134,X135) | ~ndr1_1(X134) | ndr1_1(X134) | ~ndr1_0 is false, set ~c1_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c1_0 | ~c1_1(X0) | ~c1_2(X0,X1) | c5_2(X0,X1) | c7_2(X0,X1) | ~ndr1_1(X0) | c10_1(X0) | ~ndr1_0 | ndr1_0 is false, set ~c1_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c2_2(X164,X165) | ~c3_2(X164,X165) | c9_2(X164,X165) | ~ndr1_1(X164) | ndr1_1(X164) | ~c4_1(X164) | ~ndr1_0 | ~c10_0 is false, set ~c4_1(X164) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c2_0 | c10_0 | ~c10_2(X121,X122) | c3_2(X121,X122) | ~c6_2(X121,X122) | ~ndr1_1(X121) | ~c10_1(X121) | ndr1_1(X121) | ~ndr1_0 is false, set c2_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c10_0 | c4_1(X29) | ~c6_1(X29) | c2_1(X29) | ~ndr1_0 | ndr1_0 is false, set c2_1(X29) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X130) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | ~c9_2(a1750,X133) | ~c3_2(a1750,X133) | ~c7_2(a1750,X133) | ~ndr1_1(a1750) | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X130) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | c2_2(a1750,X132) | ~c10_2(a1750,X132) | ~c8_2(a1750,X132) | ~ndr1_1(a1750) | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c8_2(X130,a1749) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | ndr1_0 | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X130) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | c6_1(a1750) | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c5_2(X130,a1749) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | ndr1_0 | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c7_2(X130,a1749) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | ndr1_0 | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X130) | c2_1(X130) | ~c1_2(X130,X131) | ~c8_2(X130,X131) | ~ndr1_1(X130) | ~ndr1_0 | ndr1_0 | ~c10_0 is false, set c2_1(X130) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c2_1(X166) | ~c7_2(X166,X167) | ~c6_2(X166,X167) | c1_2(X166,X167) | ~ndr1_1(X166) | ~ndr1_0 | ndr1_0 | ~c6_1(X169) | c7_1(X169) | c10_2(X169,X170) | c2_2(X169,X170) | c1_2(X169,X170) | ~ndr1_1(X169) | ~ndr1_0 is false, set c2_1(X166) to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c4_1(X21) | ~c7_2(X21,X22) | c6_2(X21,X22) | ~c10_2(X21,X22) | ~ndr1_1(X21) | c1_2(X21,X23) | ~c2_2(X21,X23) | c7_2(X21,X23) | ~ndr1_1(X21) | ~ndr1_0 | c6_1(X24) | ndr1_1(X24) | c2_2(X24,X25) | ~c4_2(X24,X25) | c5_2(X24,X25) | ~ndr1_1(X24) | ~ndr1_0 | c1_0 is false, set c1_0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_1(X179) | ~c4_2(X179,X180) | ~c8_2(X179,X180) | ~c7_2(X179,X180) | ~ndr1_1(X179) | ~ndr1_0 | ~c9_0 | sP8 is false, set sP8 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c6_2(X141,X142) | c9_2(X141,X142) | c4_2(X141,X142) | ~ndr1_1(X141) | ndr1_1(X141) | c10_2(X141,X143) | ~c3_2(X141,X143) | ~ndr1_1(X141) | ~ndr1_0 | sP13 | c7_1(X144) | c4_1(X144) | ~c1_1(X144) | ~ndr1_0 is false, set sP13 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c10_2(X158,X159) | ~c2_2(X158,X159) | c9_2(X158,X159) | ~ndr1_1(X158) | ndr1_1(X158) | ~c1_2(X158,X160) | ~c8_2(X158,X160) | ~ndr1_1(X158) | ~ndr1_0 | sP12 | sP11 is false, set sP11 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c9_1(X137) | ndr1_1(X137) | ~c7_2(X137,X138) | ~c3_2(X137,X138) | ~c6_2(X137,X138) | ~ndr1_1(X137) | ~ndr1_0 | sP15 | ~c10_1(X139) | ~c1_1(X139) | ~c9_1(X139) | ~ndr1_0 is false, set sP15 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | sP32 | ~c6_1(a1650) is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | sP32 | c2_1(a1650) is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | sP32 | ~c9_1(a1650) is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c4_1(a1647) | sP32 | ndr1_0 is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | sP32 | ndr1_0 is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ~c2_1(a1647) | sP32 | ndr1_0 is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever c9_2(a1647,X40) | c4_2(a1647,X40) | ~ndr1_1(a1647) | sP32 | ndr1_0 is false, set sP32 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | ~sP20 is false, set ~sP20 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | ~sP39 is false, set ~sP39 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever ndr1_0 | ~sP43 is false, set ~sP43 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever sP0 | c2_0 | ndr1_1(X191) | c4_2(X191,X192) | c1_2(X191,X192) | ~c7_2(X191,X192) | ~ndr1_1(X191) | ~c10_1(X191) | ~ndr1_0 is false, set sP0 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever sP19 | ndr1_0 | sP18 is false, set sP18 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | ndr1_1(X26) | ~ndr1_0 | c5_1(a1626) is false, set sP36 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | ndr1_1(X26) | ~ndr1_0 | c3_1(a1626) is false, set sP36 to true
% 7.75/2.03 for all groundings,
% 7.75/2.03 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | ndr1_1(X26) | ~ndr1_0 | ndr1_0 is false, set sP36 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | ~c5_2(X26,a1625) | ~ndr1_0 | ndr1_0 is false, set sP36 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | c9_2(X26,a1625) | ~ndr1_0 | ndr1_0 is false, set sP36 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | c6_2(X26,a1625) | ~ndr1_0 | ndr1_0 is false, set sP36 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c8_1(X8) | ndr1_1(X8) | c3_2(X8,X9) | ~c8_2(X8,X9) | ~c7_2(X8,X9) | ~ndr1_1(X8) | ~ndr1_0 | sP40 | c10_1(X10) | ~c6_2(X10,X11) | c3_2(X10,X11) | ~ndr1_1(X10) | c9_1(X10) | ~ndr1_0 is false, set sP40 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | sP42 | ~c10_0 is false, set sP42 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever sP6 | c8_0 | ndr1_0 is false, set sP6 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP4 is false, set ~sP4 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever sP36 | c10_2(X26,X27) | c3_2(X26,X27) | ~c6_2(X26,X27) | ~ndr1_1(X26) | c9_1(X26) | ndr1_1(X26) | ~ndr1_0 | c9_1(a1626) is false, set sP36 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP33 is false, set ~sP33 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c5_2(X0,X1) | ~c7_2(X0,X1) | ~c8_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP41 is false, set ~sP41 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c8_2(X5,a1586) | ~c10_1(X5) | c8_1(X5) | ~ndr1_0 | ndr1_0 | sP43 is false, set sP43 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c9_2(X5,a1586) | ~c10_1(X5) | c8_1(X5) | ~ndr1_0 | ndr1_0 | sP43 is false, set sP43 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X5) | ~c10_1(X5) | c8_1(X5) | ~ndr1_0 | ndr1_0 | sP43 is false, set sP43 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c10_2(X5,a1586) | ~c10_1(X5) | c8_1(X5) | ~ndr1_0 | ndr1_0 | sP43 is false, set sP43 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c9_2(X50,X51) | c8_2(X50,X51) | ~ndr1_1(X50) | ndr1_1(X50) | c9_1(X50) | ~ndr1_0 | sP31 is false, set sP31 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X119) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | c5_1(a1729) | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X119) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | ~c9_1(a1729) | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_2(X119,a1728) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | ndr1_0 | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X119) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | c3_1(a1729) | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X119) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | ndr1_0 | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c9_2(X119,a1728) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | ndr1_0 | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c5_2(X119,a1728) | c1_1(X119) | c2_2(X119,X120) | ~c7_2(X119,X120) | c1_2(X119,X120) | ~ndr1_1(X119) | ~ndr1_0 | ndr1_0 | sP20 is false, set sP20 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c9_1(X114) | ndr1_1(X114) | c8_2(X114,X115) | c4_2(X114,X115) | c10_2(X114,X115) | ~ndr1_1(X114) | ~ndr1_0 | sP22 | sP21 is false, set sP22 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c6_1(X38) | c3_1(X38) | c3_2(X38,a1643) | ~ndr1_0 | ndr1_0 | sP33 is false, set sP33 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c6_1(X38) | c3_1(X38) | ndr1_1(X38) | ~ndr1_0 | ndr1_0 | sP33 is false, set sP33 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c6_1(X38) | c3_1(X38) | ~c9_2(X38,a1643) | ~ndr1_0 | ndr1_0 | sP33 is false, set sP33 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c5_0 | ~c5_2(X63,X64) | c1_2(X63,X64) | ~ndr1_1(X63) | c7_1(X63) | ~ndr1_0 | ndr1_1(X65) | c1_2(X65,X66) | c4_2(X65,X66) | c3_2(X65,X66) | ~ndr1_1(X65) | ~c7_1(X65) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | ndr1_1(X145) | ndr1_1(X145) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | ndr1_1(X145) | ~c4_2(X145,a1765) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | ndr1_1(X145) | ~c3_2(X145,a1765) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c8_1(X185) | ~c1_1(X185) | ndr1_1(X185) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | c4_2(X145,a1764) | ndr1_1(X145) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | c2_2(X145,a1764) | ndr1_1(X145) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | ndr1_1(X145) | ~c9_2(X145,a1765) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c3_0 | ~c5_0 | ~c6_2(X145,X146) | ~c3_2(X145,X146) | c1_2(X145,X146) | ~ndr1_1(X145) | c9_2(X145,a1764) | ndr1_1(X145) | ~ndr1_0 is false, set ~c5_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c8_1(X185) | ~c1_1(X185) | ~c7_2(X185,a1810) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c8_1(X185) | ~c1_1(X185) | c2_2(X185,a1810) | ~ndr1_0 | sP4 | ndr1_0 is false, set sP4 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c6_0 | ~c1_2(X128,a1747) | c5_1(X128) | ~c2_1(X128) | ~ndr1_0 | ndr1_0 is false, set ~c6_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c6_0 | ndr1_1(X128) | c5_1(X128) | ~c2_1(X128) | ~ndr1_0 | ndr1_0 is false, set ~c6_0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c9_2(X12,a1607) | ~c5_1(X12) | c6_1(X12) | ~ndr1_0 | ~c7_2(X13,X14) | ~c8_2(X13,X14) | c5_2(X13,X14) | ~ndr1_1(X13) | ndr1_1(X13) | c6_2(X13,X15) | c3_2(X13,X15) | ~c10_2(X13,X15) | ~ndr1_1(X13) | ~ndr1_0 | sP39 is false, set sP39 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c6_2(X12,a1607) | ~c5_1(X12) | c6_1(X12) | ~ndr1_0 | ~c7_2(X13,X14) | ~c8_2(X13,X14) | c5_2(X13,X14) | ~ndr1_1(X13) | ndr1_1(X13) | c6_2(X13,X15) | c3_2(X13,X15) | ~c10_2(X13,X15) | ~ndr1_1(X13) | ~ndr1_0 | sP39 is false, set sP39 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c8_2(X12,a1607) | ~c5_1(X12) | c6_1(X12) | ~ndr1_0 | ~c7_2(X13,X14) | ~c8_2(X13,X14) | c5_2(X13,X14) | ~ndr1_1(X13) | ndr1_1(X13) | c6_2(X13,X15) | c3_2(X13,X15) | ~c10_2(X13,X15) | ~ndr1_1(X13) | ~ndr1_0 | sP39 is false, set sP39 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X12) | ~c5_1(X12) | c6_1(X12) | ~ndr1_0 | ~c7_2(X13,X14) | ~c8_2(X13,X14) | c5_2(X13,X14) | ~ndr1_1(X13) | ndr1_1(X13) | c6_2(X13,X15) | c3_2(X13,X15) | ~c10_2(X13,X15) | ~ndr1_1(X13) | ~ndr1_0 | sP39 is false, set sP39 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c1_1(X7) | ~c1_2(X7,a1599) | c3_1(X7) | ~ndr1_0 | sP41 | ndr1_0 is false, set sP41 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c1_1(X7) | c9_2(X7,a1599) | c3_1(X7) | ~ndr1_0 | sP41 | ndr1_0 is false, set sP41 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c1_1(X7) | ndr1_1(X7) | c3_1(X7) | ~ndr1_0 | sP41 | ndr1_0 is false, set sP41 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c4_2(X0,a1829) | ndr1_1(X0) | ~c9_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c5_2(X0,a1829) | ndr1_1(X0) | ~c9_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | c2_2(X0,a1774) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | ndr1_1(X0) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c5_2(X0,a1773) | ndr1_1(X0) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | c7_2(X0,a1774) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c4_2(X0,a1773) | ndr1_1(X0) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | ~c3_2(X0,a1774) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c2_2(X0,a1773) | ndr1_1(X0) | ~c3_2(X0,X1) | c6_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~sP12 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ~c2_2(X0,a1829) | ndr1_1(X0) | ~c9_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP17 is false, set ~sP17 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | ~c1_2(X0,a1830) | ~c9_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | ~c7_2(X0,a1830) | ~c9_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_1(X0) | ndr1_1(X0) | ~c9_2(X0,X1) | c5_2(X0,X1) | ~ndr1_1(X0) | ~ndr1_0 | ~sP0 is false, set ~sP0 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP23 is false, set ~sP23 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP29 is false, set ~sP29 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP30 is false, set ~sP30 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever c1_1(X7) | ~c10_2(X7,a1599) | c3_1(X7) | ~ndr1_0 | sP41 | ndr1_0 is false, set sP41 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP31 is false, set ~sP31 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP22 is false, set ~sP22 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP28 is false, set ~sP28 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP40 is false, set ~sP40 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP35 is false, set ~sP35 to true
% 10.12/2.21 for all groundings,
% 10.12/2.21 whenever ndr1_0 | ~sP21 is false, set ~sP21 to true
% 10.12/2.21 % SZS output end Definitions and Model Updates.
% 10.12/2.21 % (3979136)------------------------------
% 10.12/2.21 % (3979136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.12/2.21 % (3979136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.12/2.21 % (3979136)CaDiCaL version: 2.1.3
% 10.12/2.21 % (3979136)Termination reason: Satisfiable
% 10.12/2.21 % (3979136)Time elapsed: 0.926 s
% 10.12/2.21 % (3979136)Peak memory usage: 138 MB
% 10.12/2.21 % (3979136)Instructions burned: 1430 (million)
% 10.12/2.21 % (3979136)------------------------------
% 10.12/2.21 % (3979136)------------------------------
% 10.12/2.21 % (3979130)Success in time 1.344 s
% 10.12/2.21 % Vampire exiting
%------------------------------------------------------------------------------