%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN426+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:50:36 PM UTC 2026
% Result : CounterSatisfiable 8.18s 2.04s
% Output : Saturation 8.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u3556,negated_conjecture,
~ sP0 ).
cnf(u1262,negated_conjecture,
~ c7_2(a427,a428) ).
cnf(u1266,negated_conjecture,
~ c10_2(a427,a428) ).
cnf(u1270,negated_conjecture,
c9_2(a427,a428) ).
cnf(u1274,negated_conjecture,
ndr1_1(a427) ).
cnf(u1278,negated_conjecture,
c10_1(a427) ).
cnf(u1282,negated_conjecture,
ndr1_0 ).
cnf(u3582,negated_conjecture,
~ sP1 ).
cnf(u5349,negated_conjecture,
ndr1_1(a424) ).
cnf(u1292,negated_conjecture,
( ~ c3_2(a424,X194)
| ~ c8_2(a424,X194)
| ~ c6_2(a424,X194) ) ).
cnf(u1295,negated_conjecture,
~ c6_1(a423) ).
cnf(u1299,negated_conjecture,
( ~ c5_2(a424,X193)
| ~ c1_2(a424,X193)
| ~ c2_2(a424,X193) ) ).
cnf(u1307,negated_conjecture,
~ c5_1(a423) ).
cnf(u1313,negated_conjecture,
c10_1(a423) ).
cnf(u1320,negated_conjecture,
~ ndr1_1(a422) ).
cnf(u3604,negated_conjecture,
~ sP2 ).
cnf(u1334,negated_conjecture,
~ c10_1(a422) ).
cnf(u1338,negated_conjecture,
~ c1_1(a422) ).
cnf(u3625,negated_conjecture,
~ sP3 ).
cnf(u1345,negated_conjecture,
c5_1(a417) ).
cnf(u1348,negated_conjecture,
( ~ c6_2(X189,a416)
| ~ c1_1(X189)
| ~ c5_1(X189) ) ).
cnf(u1352,negated_conjecture,
c3_1(a417) ).
cnf(u1360,negated_conjecture,
( ~ c5_1(X189)
| c9_2(X189,a416)
| ~ c1_1(X189) ) ).
cnf(u1366,negated_conjecture,
( ~ c1_1(X189)
| ndr1_1(X189)
| ~ c5_1(X189) ) ).
cnf(u1375,negated_conjecture,
( ~ c8_1(X188)
| ~ c1_1(X188)
| ~ c5_1(X188) ) ).
cnf(u3650,negated_conjecture,
~ sP4 ).
cnf(u1402,negated_conjecture,
( ~ c8_1(X187)
| ~ c3_1(X187)
| ~ c7_1(X187) ) ).
cnf(u3681,negated_conjecture,
~ sP5 ).
cnf(u3707,negated_conjecture,
~ sP6 ).
cnf(u1423,negated_conjecture,
( ~ c2_1(X184)
| ~ c5_2(X184,a405)
| c9_1(X184) ) ).
cnf(u1427,negated_conjecture,
( ~ c2_1(X184)
| c4_2(X184,a405)
| c9_1(X184) ) ).
cnf(u1431,negated_conjecture,
( ~ c2_1(X184)
| ndr1_1(X184)
| c9_1(X184) ) ).
cnf(u1435,negated_conjecture,
sP7 ).
cnf(u1438,negated_conjecture,
( ~ c3_2(X183,a402)
| c8_1(X183) ) ).
cnf(u1442,negated_conjecture,
( ~ c1_2(X183,a402)
| c8_1(X183) ) ).
cnf(u1446,negated_conjecture,
( c2_2(X183,a402)
| c8_1(X183) ) ).
cnf(u1454,negated_conjecture,
~ ndr1_1(a401) ).
cnf(u3757,negated_conjecture,
~ sP8 ).
cnf(u1493,negated_conjecture,
( ~ c8_1(X175)
| ~ c8_2(X175,a396)
| ~ ndr1_1(X175)
| ~ c7_2(X175,X176)
| c6_2(X175,X176) ) ).
cnf(u1500,negated_conjecture,
( ~ c8_1(X175)
| c6_2(X175,a396)
| ~ ndr1_1(X175)
| ~ c7_2(X175,X176)
| c6_2(X175,X176) ) ).
cnf(u1504,negated_conjecture,
( ~ c8_1(X175)
| c2_2(X175,a396)
| ~ ndr1_1(X175)
| ~ c7_2(X175,X176)
| c6_2(X175,X176) ) ).
cnf(u3791,negated_conjecture,
~ sP9 ).
cnf(u1529,negated_conjecture,
( ~ c9_2(X172,a392)
| ~ c7_1(X172)
| ~ ndr1_1(X172)
| ~ c6_2(X172,X173)
| c7_2(X172,X173)
| c2_2(X172,X173) ) ).
cnf(u1532,negated_conjecture,
( ~ c6_2(X171,a391)
| c5_1(X171)
| ~ c1_1(X171) ) ).
cnf(u1544,negated_conjecture,
( c7_2(X171,a391)
| c5_1(X171)
| ~ c1_1(X171) ) ).
cnf(u1550,negated_conjecture,
( c5_2(X171,a391)
| c5_1(X171)
| ~ c1_1(X171) ) ).
cnf(u1556,negated_conjecture,
( c5_1(X171)
| ndr1_1(X171)
| ~ c1_1(X171) ) ).
cnf(u1568,negated_conjecture,
( ~ c3_1(X167)
| c4_1(X167)
| ~ c10_1(X167) ) ).
cnf(u3820,negated_conjecture,
~ sP10 ).
cnf(u1595,negated_conjecture,
( ~ c8_2(X163,a386)
| c3_1(X163)
| c7_1(X163) ) ).
cnf(u1599,negated_conjecture,
( ~ c7_2(X163,a386)
| c3_1(X163)
| c7_1(X163) ) ).
cnf(u1603,negated_conjecture,
( c6_2(X163,a386)
| c3_1(X163)
| c7_1(X163) ) ).
cnf(u1607,negated_conjecture,
( c3_1(X163)
| ndr1_1(X163)
| c7_1(X163) ) ).
cnf(u1611,negated_conjecture,
~ c5_2(a383,a385) ).
cnf(u3842,negated_conjecture,
~ sP11 ).
cnf(u1621,negated_conjecture,
~ c3_2(a383,a385) ).
cnf(u1625,negated_conjecture,
~ c10_2(a383,a385) ).
cnf(u1629,negated_conjecture,
ndr1_1(a383) ).
cnf(u1633,negated_conjecture,
~ c6_2(a383,a384) ).
cnf(u1637,negated_conjecture,
~ c1_2(a383,a384) ).
cnf(u3872,negated_conjecture,
~ sP12 ).
cnf(u1645,negated_conjecture,
( ~ c9_1(X159)
| ~ ndr1_1(X159)
| ~ c9_2(X159,X160)
| ~ c2_2(X159,X160)
| c7_1(X159) ) ).
cnf(u1670,negated_conjecture,
( ~ c6_1(X150)
| ~ ndr1_1(X150)
| ~ c2_2(X150,X151)
| c6_2(X150,X151)
| c10_2(X150,X151)
| c10_1(X150) ) ).
cnf(u3913,negated_conjecture,
~ sP13 ).
cnf(u1683,negated_conjecture,
( ~ c8_2(X148,a373)
| c1_1(X148)
| ~ c8_1(X148) ) ).
cnf(u1691,negated_conjecture,
c8_1(a376) ).
cnf(u1695,negated_conjecture,
( ~ c1_2(X148,a373)
| c1_1(X148)
| ~ c8_1(X148) ) ).
cnf(u1701,negated_conjecture,
( ~ c8_1(X148)
| c3_2(X148,a373)
| c1_1(X148) ) ).
cnf(u1707,negated_conjecture,
( c1_1(X148)
| ndr1_1(X148)
| ~ c8_1(X148) ) ).
cnf(u3938,negated_conjecture,
~ sP14 ).
cnf(u1719,negated_conjecture,
~ c9_0 ).
cnf(u1797,negated_conjecture,
( ~ c2_1(X147)
| ndr1_1(X147) ) ).
cnf(u1879,negated_conjecture,
( ~ c6_2(X137,a359)
| c8_1(X137)
| ~ ndr1_1(X137)
| ~ c5_2(X137,X138)
| ~ c2_2(X137,X138)
| c3_2(X137,X138) ) ).
cnf(u2476,negated_conjecture,
c8_0 ).
cnf(u1889,negated_conjecture,
( ~ c2_2(X137,a359)
| c8_1(X137)
| ~ ndr1_1(X137)
| ~ c5_2(X137,X138)
| ~ c2_2(X137,X138)
| c3_2(X137,X138) ) ).
cnf(u1893,negated_conjecture,
( ~ c10_2(X137,a359)
| c8_1(X137)
| ~ ndr1_1(X137)
| ~ c5_2(X137,X138)
| ~ c2_2(X137,X138)
| c3_2(X137,X138) ) ).
cnf(u1915,negated_conjecture,
~ ndr1_1(a357) ).
cnf(u3975,negated_conjecture,
~ sP15 ).
cnf(u1924,negated_conjecture,
~ c7_0 ).
cnf(u1932,negated_conjecture,
c9_1(a357) ).
cnf(u1937,negated_conjecture,
( ~ c2_2(X133,a354)
| c8_1(X133)
| ~ c9_1(X133) ) ).
cnf(u1941,negated_conjecture,
( c10_2(X133,a354)
| c8_1(X133)
| ~ c9_1(X133) ) ).
cnf(u1945,negated_conjecture,
( c1_2(X133,a354)
| c8_1(X133)
| ~ c9_1(X133) ) ).
cnf(u1956,negated_conjecture,
( ~ c8_1(X130)
| ~ ndr1_1(X130)
| ~ c1_2(X130,X131)
| c5_2(X130,X131)
| c3_2(X130,X131)
| c4_1(X130) ) ).
cnf(u1963,negated_conjecture,
( ~ c4_1(X127)
| ~ c5_1(X127)
| c3_1(X127) ) ).
cnf(u1975,negated_conjecture,
( ~ c8_1(X125)
| ~ ndr1_1(X125)
| ~ c7_2(X125,X126)
| c2_2(X125,X126)
| c1_2(X125,X126)
| c3_1(X125) ) ).
cnf(u1982,negated_conjecture,
~ c6_0 ).
cnf(u1986,negated_conjecture,
~ c5_2(a350,a352) ).
cnf(u4002,negated_conjecture,
~ sP16 ).
cnf(u1992,negated_conjecture,
~ c4_0 ).
cnf(u1996,negated_conjecture,
~ c4_2(a350,a352) ).
cnf(u2000,negated_conjecture,
c7_2(a350,a352) ).
cnf(u2004,negated_conjecture,
ndr1_1(a350) ).
cnf(u2008,negated_conjecture,
~ c6_2(a350,a351) ).
cnf(u2012,negated_conjecture,
c5_2(a350,a351) ).
cnf(u2018,negated_conjecture,
( ~ c1_2(a350,X123)
| ~ c5_2(a350,X123)
| c8_2(a350,X123) ) ).
cnf(u2022,negated_conjecture,
( ~ c7_2(X122,a347)
| c1_1(X122)
| c7_1(X122) ) ).
cnf(u2026,negated_conjecture,
( c8_2(X122,a347)
| c1_1(X122)
| c7_1(X122) ) ).
cnf(u2030,negated_conjecture,
( c2_2(X122,a347)
| c1_1(X122)
| c7_1(X122) ) ).
cnf(u2041,negated_conjecture,
( ~ c3_2(a346,X121)
| ~ c7_2(a346,X121)
| ~ c6_2(a346,X121) ) ).
cnf(u3206,negated_conjecture,
c3_0 ).
cnf(u2051,negated_conjecture,
c5_1(a346) ).
cnf(u2055,negated_conjecture,
( ~ c9_2(X116,a345)
| c7_1(X116)
| c9_1(X116) ) ).
cnf(u2062,negated_conjecture,
( c7_2(X116,a345)
| c7_1(X116)
| c9_1(X116) ) ).
cnf(u2066,negated_conjecture,
( c3_2(X116,a345)
| c7_1(X116)
| c9_1(X116) ) ).
cnf(u2070,negated_conjecture,
( c7_1(X116)
| ndr1_1(X116)
| c9_1(X116) ) ).
cnf(u2095,negated_conjecture,
( ~ c4_2(X112,a343)
| c1_2(X112,X113)
| ~ c3_2(X112,X114)
| ~ c2_2(X112,X114)
| c6_2(X112,X114)
| ~ ndr1_1(X112)
| ~ c9_2(X112,X113)
| ~ c4_2(X112,X113) ) ).
cnf(u2102,negated_conjecture,
( ~ c3_2(X112,a343)
| c1_2(X112,X113)
| ~ c3_2(X112,X114)
| ~ c2_2(X112,X114)
| c6_2(X112,X114)
| ~ ndr1_1(X112)
| ~ c9_2(X112,X113)
| ~ c4_2(X112,X113) ) ).
cnf(u2106,negated_conjecture,
( ~ c3_2(X112,X114)
| c9_2(X112,a343)
| c1_2(X112,X113)
| ~ c2_2(X112,X114)
| c6_2(X112,X114)
| ~ ndr1_1(X112)
| ~ c9_2(X112,X113)
| ~ c4_2(X112,X113) ) ).
cnf(u2110,negated_conjecture,
~ ndr1_1(a342) ).
cnf(u2117,negated_conjecture,
~ c3_1(a342) ).
cnf(u2121,negated_conjecture,
~ c2_1(a342) ).
cnf(u4043,negated_conjecture,
~ sP17 ).
cnf(u2129,negated_conjecture,
~ c6_1(a339) ).
cnf(u3271,negated_conjecture,
c2_0 ).
cnf(u2136,negated_conjecture,
c3_1(a339) ).
cnf(u2145,negated_conjecture,
( ~ c7_2(X104,a338)
| c8_1(X104)
| ~ ndr1_1(X104)
| ~ c9_2(X104,X105)
| ~ c8_2(X104,X105)
| c10_2(X104,X105) ) ).
cnf(u2149,negated_conjecture,
( ~ c9_2(X104,X105)
| c2_2(X104,a338)
| ~ ndr1_1(X104)
| c8_1(X104)
| ~ c8_2(X104,X105)
| c10_2(X104,X105) ) ).
cnf(u2153,negated_conjecture,
( ~ c9_2(X104,X105)
| c10_2(X104,a338)
| ~ ndr1_1(X104)
| c8_1(X104)
| ~ c8_2(X104,X105)
| c10_2(X104,X105) ) ).
cnf(u4065,negated_conjecture,
~ sP18 ).
cnf(u2166,negated_conjecture,
~ c10_0 ).
cnf(u2170,negated_conjecture,
~ c9_1(a337) ).
cnf(u2174,negated_conjecture,
~ c5_1(a337) ).
cnf(u2206,negated_conjecture,
~ ndr1_1(a332) ).
cnf(u2213,negated_conjecture,
~ c4_1(a332) ).
cnf(u2217,negated_conjecture,
~ c1_1(a332) ).
cnf(u2226,negated_conjecture,
( ~ c7_2(X98,a331)
| c5_1(X98) ) ).
cnf(u2230,negated_conjecture,
( c8_2(X98,a331)
| c5_1(X98) ) ).
cnf(u2234,negated_conjecture,
( c6_2(X98,a331)
| c5_1(X98) ) ).
cnf(u2238,negated_conjecture,
( c5_1(X98)
| ndr1_1(X98) ) ).
cnf(u2242,negated_conjecture,
~ c9_1(a330) ).
cnf(u4091,negated_conjecture,
~ sP19 ).
cnf(u2248,negated_conjecture,
~ c1_0 ).
cnf(u2252,negated_conjecture,
~ c8_1(a330) ).
cnf(u2256,negated_conjecture,
~ c10_1(a330) ).
cnf(u2265,negated_conjecture,
c6_1(a327) ).
cnf(u2269,negated_conjecture,
c10_1(a327) ).
cnf(u2274,negated_conjecture,
~ ndr1_1(a326) ).
cnf(u2321,negated_conjecture,
( ~ c2_1(X90)
| ~ c9_2(X90,a322) ) ).
cnf(u2325,negated_conjecture,
( ~ c2_1(X90)
| ~ c10_2(X90,a322) ) ).
cnf(u2329,negated_conjecture,
( ~ c2_1(X90)
| c4_2(X90,a322) ) ).
cnf(u2334,negated_conjecture,
~ c2_2(a319,a321) ).
cnf(u2338,negated_conjecture,
ndr1_1(a319) ).
cnf(u2342,negated_conjecture,
c6_2(a319,a320) ).
cnf(u2346,negated_conjecture,
c5_2(a319,a320) ).
cnf(u2350,negated_conjecture,
c4_2(a319,a320) ).
cnf(u2355,negated_conjecture,
~ c8_1(a319) ).
cnf(u2363,negated_conjecture,
( ~ c7_2(a318,X89)
| ~ c10_2(a318,X89)
| ~ c4_2(a318,X89) ) ).
cnf(u4118,negated_conjecture,
~ sP20 ).
cnf(u2371,negated_conjecture,
~ c8_1(a318) ).
cnf(u2375,negated_conjecture,
~ c10_1(a318) ).
cnf(u2380,negated_conjecture,
sP21 ).
cnf(u2383,negated_conjecture,
( ~ c9_2(X88,a313)
| ~ c5_1(X88)
| ~ c6_1(X88) ) ).
cnf(u2387,negated_conjecture,
( ~ c5_1(X88)
| c3_2(X88,a313)
| ~ c6_1(X88) ) ).
cnf(u2395,negated_conjecture,
( ~ c9_2(X87,a311)
| ~ c6_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2399,negated_conjecture,
( ~ c9_2(X87,a311)
| c9_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2403,negated_conjecture,
( ~ c9_2(X87,a311)
| c8_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2407,negated_conjecture,
( ~ c2_2(X87,a311)
| ~ c6_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2411,negated_conjecture,
( ~ c2_2(X87,a311)
| c9_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2415,negated_conjecture,
( c8_2(X87,a312)
| c9_1(X87)
| ~ c2_2(X87,a311) ) ).
cnf(u2419,negated_conjecture,
( c4_2(X87,a311)
| ~ c6_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2423,negated_conjecture,
( c4_2(X87,a311)
| c9_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2427,negated_conjecture,
( c4_2(X87,a311)
| c8_2(X87,a312)
| c9_1(X87) ) ).
cnf(u2431,negated_conjecture,
( c9_1(X87)
| ndr1_1(X87) ) ).
cnf(u2452,negated_conjecture,
~ ndr1_1(a309) ).
cnf(u2468,negated_conjecture,
( c6_1(X83)
| ~ c8_1(X83)
| c1_1(X83) ) ).
cnf(u4171,negated_conjecture,
~ sP22 ).
cnf(u4209,negated_conjecture,
~ sP23 ).
cnf(u2557,negated_conjecture,
( ~ c8_1(X78)
| ndr1_1(X78) ) ).
cnf(u4247,negated_conjecture,
~ sP24 ).
cnf(u2621,negated_conjecture,
~ c1_1(a293) ).
cnf(u2629,negated_conjecture,
c9_1(a293) ).
cnf(u2633,negated_conjecture,
c7_1(a293) ).
cnf(u2731,negated_conjecture,
( ~ c4_2(X66,a286)
| c10_2(X66,X67)
| ~ c1_2(X66,X68)
| c9_2(X66,X68)
| c6_2(X66,X68)
| ~ ndr1_1(X66)
| ~ c3_2(X66,X67)
| c8_2(X66,X67) ) ).
cnf(u2735,negated_conjecture,
( ~ c1_2(X66,a286)
| c10_2(X66,X67)
| ~ c1_2(X66,X68)
| c9_2(X66,X68)
| c6_2(X66,X68)
| ~ ndr1_1(X66)
| ~ c3_2(X66,X67)
| c8_2(X66,X67) ) ).
cnf(u2739,negated_conjecture,
( ~ c1_2(X66,X68)
| c2_2(X66,a286)
| c10_2(X66,X67)
| c9_2(X66,X68)
| c6_2(X66,X68)
| ~ ndr1_1(X66)
| ~ c3_2(X66,X67)
| c8_2(X66,X67) ) ).
cnf(u2778,negated_conjecture,
~ c4_2(a281,a282) ).
cnf(u2783,negated_conjecture,
c8_2(a281,a282) ).
cnf(u2787,negated_conjecture,
ndr1_1(a281) ).
cnf(u2792,negated_conjecture,
( ~ c3_2(a281,X65)
| c7_2(a281,X65)
| ~ c2_2(a281,X65) ) ).
cnf(u2796,negated_conjecture,
~ c5_1(a281) ).
cnf(u2801,negated_conjecture,
( ~ c9_2(X63,a279)
| ~ c5_2(X63,a280)
| c3_2(X63,X64)
| ~ ndr1_1(X63)
| ~ c7_2(X63,X64) ) ).
cnf(u4284,negated_conjecture,
~ sP25 ).
cnf(u2808,negated_conjecture,
( ~ c4_2(X63,a280)
| c3_2(X63,X64)
| ~ c9_2(X63,a279)
| ~ ndr1_1(X63)
| ~ c7_2(X63,X64) ) ).
cnf(u2812,negated_conjecture,
( ~ c8_2(X63,a279)
| ~ c5_2(X63,a280)
| c3_2(X63,X64)
| ~ ndr1_1(X63)
| ~ c7_2(X63,X64) ) ).
cnf(u2816,negated_conjecture,
( ~ c4_2(X63,a280)
| c3_2(X63,X64)
| ~ c8_2(X63,a279)
| ~ ndr1_1(X63)
| ~ c7_2(X63,X64) ) ).
cnf(u2820,negated_conjecture,
( ~ c2_2(X63,a279)
| ~ c5_2(X63,a280)
| c3_2(X63,X64)
| ~ ndr1_1(X63)
| ~ c7_2(X63,X64) ) ).
cnf(u2824,negated_conjecture,
( ~ c4_2(X63,a280)
| c3_2(X63,X64)
| ~ c2_2(X63,a279)
| ~ ndr1_1(X63)
| ~ c7_2(X63,X64) ) ).
cnf(u4322,negated_conjecture,
~ sP26 ).
cnf(u2831,negated_conjecture,
( ~ c4_1(X62)
| ~ c4_2(X62,a274)
| c3_1(X62) ) ).
cnf(u2835,negated_conjecture,
( ~ c4_1(X62)
| c3_2(X62,a274)
| c3_1(X62) ) ).
cnf(u2839,negated_conjecture,
( ~ c4_1(X62)
| c2_2(X62,a274)
| c3_1(X62) ) ).
cnf(u2843,negated_conjecture,
( ~ c4_1(X62)
| ndr1_1(X62)
| c3_1(X62) ) ).
cnf(u2847,negated_conjecture,
( ~ c2_1(X61)
| c6_2(X61,a273)
| c3_1(X61) ) ).
cnf(u2851,negated_conjecture,
( ~ c2_1(X61)
| c5_2(X61,a273)
| c3_1(X61) ) ).
cnf(u2855,negated_conjecture,
( ~ c2_1(X61)
| c2_2(X61,a273)
| c3_1(X61) ) ).
cnf(u2859,negated_conjecture,
( c3_1(X61)
| ndr1_1(X61)
| ~ c2_1(X61) ) ).
cnf(u2863,negated_conjecture,
sP27 ).
cnf(u2866,negated_conjecture,
( ~ c10_2(X59,a270)
| c10_1(X59)
| ~ ndr1_1(X59)
| ~ c7_2(X59,X60)
| ~ c6_2(X59,X60)
| c8_2(X59,X60) ) ).
cnf(u2874,negated_conjecture,
( ~ c7_2(X59,X60)
| c1_2(X59,a270)
| ~ ndr1_1(X59)
| c10_1(X59)
| ~ c6_2(X59,X60)
| c8_2(X59,X60) ) ).
cnf(u2885,negated_conjecture,
( ~ c9_2(a269,X55)
| c5_2(a269,X55)
| c6_2(a269,X55) ) ).
cnf(u2892,negated_conjecture,
c5_1(a269) ).
cnf(u2911,negated_conjecture,
( ~ c2_1(X52)
| ~ ndr1_1(X52)
| ~ c6_2(X52,X53)
| c9_2(X52,X53)
| c10_2(X52,X53)
| ~ c3_1(X52) ) ).
cnf(u2915,negated_conjecture,
( ~ c9_2(X51,a267)
| ~ c1_1(X51) ) ).
cnf(u2922,negated_conjecture,
( ~ c3_2(X51,a267)
| ~ c1_1(X51) ) ).
cnf(u2926,negated_conjecture,
( c8_2(X51,a267)
| ~ c1_1(X51) ) ).
cnf(u2930,negated_conjecture,
( ~ c1_1(X51)
| ndr1_1(X51) ) ).
cnf(u2976,negated_conjecture,
( ~ c4_2(X44,a263)
| c7_1(X44)
| ~ ndr1_1(X44)
| ~ c7_2(X44,X45)
| ~ c5_2(X44,X45)
| c10_2(X44,X45) ) ).
cnf(u2980,negated_conjecture,
( c10_2(X44,X45)
| c8_2(X44,a263)
| ~ ndr1_1(X44)
| ~ c7_2(X44,X45)
| ~ c5_2(X44,X45)
| c7_1(X44) ) ).
cnf(u2984,negated_conjecture,
( c10_2(X44,X45)
| c3_2(X44,a263)
| ~ ndr1_1(X44)
| ~ c7_2(X44,X45)
| ~ c5_2(X44,X45)
| c7_1(X44) ) ).
cnf(u2992,negated_conjecture,
( c5_2(a262,X43)
| ~ c4_2(a262,X43) ) ).
cnf(u2996,negated_conjecture,
~ c6_1(a262) ).
cnf(u3000,negated_conjecture,
c1_1(a262) ).
cnf(u3005,negated_conjecture,
( ~ c4_2(X42,a261)
| c5_1(X42)
| ~ c3_2(X42,a260) ) ).
cnf(u3009,negated_conjecture,
( ~ c1_2(X42,a261)
| c5_1(X42)
| ~ c3_2(X42,a260) ) ).
cnf(u3013,negated_conjecture,
( c7_2(X42,a261)
| c5_1(X42)
| ~ c3_2(X42,a260) ) ).
cnf(u3017,negated_conjecture,
( ~ c4_2(X42,a261)
| c5_1(X42)
| c4_2(X42,a260) ) ).
cnf(u3021,negated_conjecture,
( c4_2(X42,a260)
| ~ c1_2(X42,a261)
| c5_1(X42) ) ).
cnf(u3025,negated_conjecture,
( c4_2(X42,a260)
| c7_2(X42,a261)
| c5_1(X42) ) ).
cnf(u3029,negated_conjecture,
( ~ c4_2(X42,a261)
| c5_1(X42)
| c10_2(X42,a260) ) ).
cnf(u3033,negated_conjecture,
( ~ c1_2(X42,a261)
| c5_1(X42)
| c10_2(X42,a260) ) ).
cnf(u3037,negated_conjecture,
( c10_2(X42,a260)
| c7_2(X42,a261)
| c5_1(X42) ) ).
cnf(u3042,negated_conjecture,
~ c5_1(a259) ).
cnf(u3046,negated_conjecture,
~ c4_1(a259) ).
cnf(u3051,negated_conjecture,
( ~ c3_2(X39,a258)
| c8_2(X39,X40)
| ~ c9_2(X39,X41)
| ~ c7_2(X39,X41)
| ~ c1_2(X39,X41)
| ~ ndr1_1(X39)
| c9_2(X39,X40) ) ).
cnf(u3056,negated_conjecture,
( ~ c2_2(X39,a258)
| c8_2(X39,X40)
| ~ c9_2(X39,X41)
| ~ c7_2(X39,X41)
| ~ c1_2(X39,X41)
| ~ ndr1_1(X39)
| c9_2(X39,X40) ) ).
cnf(u3060,negated_conjecture,
( ~ c1_2(X39,X41)
| c4_2(X39,a258)
| ~ c9_2(X39,X41)
| ~ c7_2(X39,X41)
| c8_2(X39,X40)
| ~ ndr1_1(X39)
| c9_2(X39,X40) ) ).
cnf(u3064,negated_conjecture,
( ~ c3_2(X37,X38)
| ~ ndr1_1(X37)
| ~ c8_2(X37,X38)
| c5_1(X37)
| c2_2(X37,X38)
| c8_1(X37) ) ).
cnf(u3068,negated_conjecture,
c5_1(a257) ).
cnf(u3075,negated_conjecture,
c4_1(a257) ).
cnf(u3079,negated_conjecture,
c3_1(a257) ).
cnf(u3099,negated_conjecture,
( ~ c8_2(X31,a255)
| ~ c2_2(X31,X32)
| ~ c3_2(X31,a254)
| ~ ndr1_1(X31)
| ~ c3_2(X31,X32) ) ).
cnf(u3103,negated_conjecture,
( ~ c3_2(X31,a254)
| ~ c5_2(X31,a255)
| ~ c2_2(X31,X32)
| ~ ndr1_1(X31)
| ~ c3_2(X31,X32) ) ).
cnf(u3107,negated_conjecture,
( ~ c8_2(X31,a255)
| ~ c2_2(X31,X32)
| c2_2(X31,a254)
| ~ ndr1_1(X31)
| ~ c3_2(X31,X32) ) ).
cnf(u3111,negated_conjecture,
( ~ c5_2(X31,a255)
| ~ c2_2(X31,X32)
| c2_2(X31,a254)
| ~ ndr1_1(X31)
| ~ c3_2(X31,X32) ) ).
cnf(u3115,negated_conjecture,
( ~ c8_2(X31,a255)
| ~ c2_2(X31,X32)
| c1_2(X31,a254)
| ~ ndr1_1(X31)
| ~ c3_2(X31,X32) ) ).
cnf(u3119,negated_conjecture,
( ~ c5_2(X31,a255)
| ~ c2_2(X31,X32)
| c1_2(X31,a254)
| ~ ndr1_1(X31)
| ~ c3_2(X31,X32) ) ).
cnf(u3164,negated_conjecture,
~ c7_1(a250) ).
cnf(u3170,negated_conjecture,
~ c10_2(a247,a249) ).
cnf(u3174,negated_conjecture,
c9_2(a247,a249) ).
cnf(u3178,negated_conjecture,
c2_2(a247,a249) ).
cnf(u3182,negated_conjecture,
ndr1_1(a247) ).
cnf(u3186,negated_conjecture,
~ c1_2(a247,a248) ).
cnf(u3190,negated_conjecture,
c9_2(a247,a248) ).
cnf(u3194,negated_conjecture,
c10_2(a247,a248) ).
cnf(u3200,negated_conjecture,
( ~ c3_2(a247,X29)
| ~ c6_2(a247,X29)
| c9_2(a247,X29) ) ).
cnf(u4389,negated_conjecture,
~ sP29 ).
cnf(u3439,negated_conjecture,
( ~ c7_2(X7,a228)
| ~ c8_1(X7)
| ~ ndr1_1(X7)
| ~ c8_2(X7,X8)
| c6_2(X7,X8) ) ).
cnf(u3444,negated_conjecture,
( ~ c8_1(X7)
| c4_2(X7,a228)
| ~ ndr1_1(X7)
| ~ c8_2(X7,X8)
| c6_2(X7,X8) ) ).
cnf(u3448,negated_conjecture,
( ~ c8_1(X7)
| c3_2(X7,a228)
| ~ ndr1_1(X7)
| ~ c8_2(X7,X8)
| c6_2(X7,X8) ) ).
cnf(u3452,negated_conjecture,
~ c10_1(a227) ).
cnf(u4415,negated_conjecture,
~ sP30 ).
cnf(u3459,negated_conjecture,
~ c1_1(a227) ).
cnf(u3463,negated_conjecture,
c9_1(a227) ).
cnf(u3470,negated_conjecture,
( c1_1(X5)
| ~ c7_1(X5)
| c9_1(X5) ) ).
cnf(u3495,negated_conjecture,
~ ndr1_1(a222) ).
cnf(u3502,negated_conjecture,
~ c7_1(a222) ).
cnf(u3506,negated_conjecture,
~ c1_1(a222) ).
cnf(u3735,axiom,
c8_2(a403,a404) ).
cnf(u3739,axiom,
c5_2(a403,a404) ).
cnf(u3743,axiom,
c10_2(a403,a404) ).
cnf(u3747,axiom,
ndr1_1(a403) ).
cnf(u3751,axiom,
~ c4_1(a403) ).
cnf(u3755,axiom,
c2_1(a403) ).
cnf(u4148,axiom,
~ c5_2(a314,a315) ).
cnf(u4152,axiom,
c7_2(a314,a315) ).
cnf(u4156,axiom,
c4_2(a314,a315) ).
cnf(u4160,axiom,
ndr1_1(a314) ).
cnf(u4165,axiom,
( ~ c4_2(a314,X0)
| ~ c8_2(a314,X0)
| c7_2(a314,X0) ) ).
cnf(u4169,axiom,
~ c4_1(a314) ).
cnf(u4349,axiom,
( c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u4354,axiom,
( ~ c2_2(X0,a272)
| c6_1(X0)
| ~ c10_2(X0,a271) ) ).
cnf(u4358,axiom,
( ~ c10_2(X0,a271)
| c8_2(X0,a272)
| c6_1(X0) ) ).
cnf(u4362,axiom,
( ~ c10_2(X0,a271)
| c6_2(X0,a272)
| c6_1(X0) ) ).
cnf(u4366,axiom,
( c8_2(X0,a271)
| ~ c2_2(X0,a272)
| c6_1(X0) ) ).
cnf(u4370,axiom,
( c8_2(X0,a272)
| c6_1(X0)
| c8_2(X0,a271) ) ).
cnf(u4374,axiom,
( c8_2(X0,a271)
| c6_2(X0,a272)
| c6_1(X0) ) ).
cnf(u4378,axiom,
( ~ c2_2(X0,a272)
| c6_1(X0)
| c3_2(X0,a271) ) ).
cnf(u4382,axiom,
( c8_2(X0,a272)
| c6_1(X0)
| c3_2(X0,a271) ) ).
cnf(u4386,axiom,
( c6_2(X0,a272)
| c6_1(X0)
| c3_2(X0,a271) ) ).
cnf(u4492,negated_conjecture,
ndr1_1(a327) ).
cnf(u4517,negated_conjecture,
~ c6_2(a247,a345) ).
cnf(u4780,negated_conjecture,
~ c9_1(a350) ).
cnf(u4565,negated_conjecture,
~ ndr1_1(a227) ).
cnf(u4613,negated_conjecture,
~ c10_1(a339) ).
cnf(u4632,negated_conjecture,
~ c6_2(a350,a352) ).
cnf(u4729,negated_conjecture,
~ c7_1(a376) ).
cnf(u5220,negated_conjecture,
c3_1(a376) ).
cnf(u4739,negated_conjecture,
~ c1_1(a376) ).
cnf(u4750,negated_conjecture,
~ c6_1(a424) ).
cnf(u4762,negated_conjecture,
~ c7_1(a332) ).
cnf(u4768,negated_conjecture,
~ c6_1(a269) ).
cnf(u4801,negated_conjecture,
~ c8_2(a247,a249) ).
cnf(u4811,negated_conjecture,
~ c8_2(a427,a428) ).
cnf(u4829,negated_conjecture,
~ c8_1(a339) ).
cnf(u4854,negated_conjecture,
~ c6_2(a424,a345) ).
cnf(u4865,negated_conjecture,
~ c8_1(a423) ).
cnf(u4874,negated_conjecture,
~ c8_1(a309) ).
cnf(u4913,negated_conjecture,
~ c2_2(a424,a391) ).
cnf(u4935,negated_conjecture,
~ c1_1(a318) ).
cnf(u5475,negated_conjecture,
~ c7_1(a318) ).
cnf(u4957,negated_conjecture,
~ c10_2(a318,a345) ).
cnf(u4990,negated_conjecture,
~ c1_1(a269) ).
cnf(u5007,negated_conjecture,
~ c10_1(a417) ).
cnf(u5017,negated_conjecture,
~ c6_1(a346) ).
cnf(u5024,negated_conjecture,
~ c1_1(a346) ).
cnf(u5041,negated_conjecture,
~ c6_1(a257) ).
cnf(u5048,negated_conjecture,
~ c1_1(a257) ).
cnf(u5122,negated_conjecture,
~ c6_2(a314,a315) ).
cnf(u5165,negated_conjecture,
~ c3_1(a403) ).
cnf(u5173,negated_conjecture,
c2_2(a403,a273) ).
cnf(u5177,negated_conjecture,
c5_2(a403,a273) ).
cnf(u5181,negated_conjecture,
c6_2(a403,a273) ).
cnf(u5188,negated_conjecture,
c4_2(a403,a405) ).
cnf(u5192,negated_conjecture,
~ c5_2(a403,a405) ).
cnf(u5398,negated_conjecture,
~ c7_1(a346) ).
cnf(u5204,negated_conjecture,
~ c6_2(a346,a345) ).
cnf(u5214,negated_conjecture,
c3_2(a376,a228) ).
cnf(u5218,negated_conjecture,
c4_2(a376,a228) ).
cnf(u5223,negated_conjecture,
( ~ c7_2(a376,X0)
| c1_2(a376,X0)
| c2_2(a376,X0) ) ).
cnf(u5227,negated_conjecture,
( ~ c7_2(a376,X0)
| c6_2(a376,X0) ) ).
cnf(u5245,negated_conjecture,
~ c2_2(a376,a373) ).
cnf(u5267,negated_conjecture,
c4_1(a376) ).
cnf(u5279,negated_conjecture,
~ c3_2(a376,a260) ).
cnf(u5291,negated_conjecture,
c6_2(a376,a345) ).
cnf(u5302,negated_conjecture,
~ c4_2(a262,a255) ).
cnf(u5318,negated_conjecture,
c2_2(a376,a345) ).
cnf(u5334,negated_conjecture,
~ c2_2(a376,a228) ).
cnf(u5368,negated_conjecture,
~ c8_2(a314,a260) ).
cnf(u5385,negated_conjecture,
~ c8_2(a314,a311) ).
cnf(u5404,negated_conjecture,
~ c6_1(a417) ).
cnf(u5411,negated_conjecture,
~ c1_1(a417) ).
cnf(u5420,negated_conjecture,
~ c5_2(a318,a345) ).
cnf(u5459,negated_conjecture,
c8_2(a376,a345) ).
cnf(u5472,negated_conjecture,
~ c8_1(a424) ).
cnf(u5483,negated_conjecture,
~ c7_1(a422) ).
cnf(u5498,negated_conjecture,
( ~ c2_2(a376,X0)
| c6_2(a376,X0)
| c10_2(a376,X0) ) ).
cnf(u5507,negated_conjecture,
c10_2(a376,a347) ).
cnf(u5518,negated_conjecture,
~ c7_1(a269) ).
cnf(u5540,negated_conjecture,
~ ndr1_1(a293) ).
cnf(u5569,negated_conjecture,
~ c7_1(a257) ).
cnf(u5575,negated_conjecture,
~ c7_1(a417) ).
cnf(u5586,negated_conjecture,
~ c5_2(a403,a322) ).
cnf(u5605,negated_conjecture,
~ c5_2(a247,a249) ).
cnf(u4607,negated_conjecture,
( ~ c7_2(X0,a270)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c6_2(X0,X1)
| c8_2(X0,X1)
| c8_2(X0,a263)
| c10_1(X0)
| ~ c5_2(X0,a270)
| c7_1(X0) ) ).
cnf(u5255,negated_conjecture,
( ~ c7_2(X0,a359)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c2_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a263)
| c8_1(X0)
| ~ c5_2(X0,a359)
| c7_1(X0) ) ).
cnf(u5146,negated_conjecture,
ndr1_1(a346) ).
cnf(u4620,negated_conjecture,
ndr1_1(a330) ).
cnf(u5561,negated_conjecture,
~ c8_1(a417) ).
cnf(u5488,negated_conjecture,
~ c8_1(a269) ).
cnf(u4571,negated_conjecture,
( ~ c9_1(X0)
| c10_2(X0,X1)
| c9_2(X0,a354)
| c6_2(X0,a354)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| c8_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a286) ) ).
cnf(u4547,negated_conjecture,
( ~ c10_1(X0)
| c4_1(X0)
| ndr1_1(X0)
| c7_1(X0) ) ).
cnf(u5556,negated_conjecture,
~ c8_1(a257) ).
cnf(u4822,negated_conjecture,
ndr1_1(a259) ).
cnf(u5206,negated_conjecture,
ndr1_1(a376) ).
cnf(u5157,negated_conjecture,
~ c10_2(a403,a322) ).
cnf(u4867,negated_conjecture,
( ~ c8_2(X0,a345)
| c5_1(X0)
| c2_2(X0,a345)
| c8_1(X0)
| c7_1(X0)
| c9_1(X0) ) ).
cnf(u5114,negated_conjecture,
( c3_2(X0,a313)
| ndr1_1(X0) ) ).
cnf(u5137,negated_conjecture,
( ~ c8_1(X0)
| c6_2(X0,X1)
| c10_2(X0,X1)
| c10_1(X0)
| ~ c2_2(X0,X1)
| c1_1(X0) ) ).
cnf(u5088,negated_conjecture,
c7_1(a342) ).
cnf(u5559,negated_conjecture,
ndr1_1(a417) ).
cnf(u4506,negated_conjecture,
( ~ c3_2(X37,X38)
| ~ c8_2(X37,X38)
| c5_1(X37)
| c2_2(X37,X38)
| c8_1(X37) ) ).
cnf(u5029,negated_conjecture,
ndr1_1(a423) ).
cnf(u5080,negated_conjecture,
c3_2(a376,a373) ).
cnf(u4876,negated_conjecture,
ndr1_1(a337) ).
cnf(u4606,negated_conjecture,
( ~ c7_2(X0,a270)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c6_2(X0,X1)
| c8_2(X0,X1)
| c3_2(X0,a263)
| c10_1(X0)
| ~ c5_2(X0,a270)
| c7_1(X0) ) ).
cnf(u5073,negated_conjecture,
~ c8_1(a346) ).
cnf(u114,axiom,
( ~ sP28(X0)
| ~ c10_2(X0,a233) ) ).
cnf(u113,axiom,
( ~ sP28(X0)
| ~ c8_2(X0,a233) ) ).
cnf(u5554,negated_conjecture,
ndr1_1(a257) ).
cnf(u5145,negated_conjecture,
ndr1_1(a339) ).
cnf(u5156,negated_conjecture,
~ c9_2(a403,a322) ).
cnf(u5139,negated_conjecture,
ndr1_1(a262) ).
cnf(u5486,negated_conjecture,
ndr1_1(a269) ).
cnf(u5256,negated_conjecture,
( ~ c7_2(X0,a359)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c2_2(X0,X1)
| c3_2(X0,X1)
| c8_2(X0,a263)
| c8_1(X0)
| ~ c5_2(X0,a359)
| c7_1(X0) ) ).
cnf(u116,axiom,
( ~ sP28(X0)
| ndr1_1(X0) ) ).
cnf(u4640,negated_conjecture,
( ~ c7_2(X0,a271)
| c6_1(X0)
| c8_2(X0,a263)
| ~ ndr1_1(X0)
| c8_2(X0,a272)
| ~ c5_2(X0,a271)
| c7_1(X0) ) ).
cnf(u4531,negated_conjecture,
( ~ c2_2(X0,a345)
| c1_2(X0,X1)
| c9_2(X0,a343)
| c6_2(X0,a345)
| ~ c9_2(X0,X1)
| ~ c4_2(X0,X1)
| c7_1(X0)
| c9_1(X0) ) ).
cnf(u4625,negated_conjecture,
( ~ c6_2(X0,a345)
| c10_1(X0)
| c1_2(X0,a270)
| c8_2(X0,a345)
| c7_1(X0)
| c9_1(X0) ) ).
cnf(u4641,negated_conjecture,
( ~ c7_2(X0,a271)
| c6_1(X0)
| c3_2(X0,a263)
| ~ ndr1_1(X0)
| c8_2(X0,a272)
| ~ c5_2(X0,a271)
| c7_1(X0) ) ).
cnf(u5158,negated_conjecture,
c4_2(a403,a322) ).
cnf(u4623,negated_conjecture,
( ~ c6_2(X0,a261)
| ~ ndr1_1(X0)
| c10_1(X0)
| c1_2(X0,a270)
| c8_2(X0,a261)
| c5_1(X0)
| ~ c3_2(X0,a260) ) ).
cnf(u4600,negated_conjecture,
( ~ c7_2(X0,a271)
| c6_1(X0)
| c8_2(X0,a263)
| ~ ndr1_1(X0)
| c6_2(X0,a272)
| ~ c5_2(X0,a271)
| c7_1(X0) ) ).
cnf(u4463,negated_conjecture,
( ~ c2_1(X52)
| ~ c6_2(X52,X53)
| c9_2(X52,X53)
| c10_2(X52,X53)
| ~ c3_1(X52) ) ).
cnf(u4551,negated_conjecture,
( ~ c9_2(X0,a354)
| ~ c9_1(X0)
| c4_2(X0,a258)
| c8_1(X0)
| ~ c7_2(X0,a354)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| c9_2(X0,X1) ) ).
cnf(u4601,negated_conjecture,
( ~ c7_2(X0,a271)
| c6_1(X0)
| c3_2(X0,a263)
| ~ ndr1_1(X0)
| c6_2(X0,a272)
| ~ c5_2(X0,a271)
| c7_1(X0) ) ).
cnf(u115,axiom,
( ~ sP28(X0)
| c6_2(X0,a233) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN426+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.16 % Computer : n014.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Mon Sep 28 15:56:00 UTC 2026
% 0.10/0.16 % CPUTime :
% 0.10/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running first-order theorem proving
% 0.10/0.21 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.69/2.04 % (1895646)Detected formulas, will run a generic FOF schedule.
% 7.69/2.04 % (1895655)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2640776847:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.69/2.04 % (1895655)Instruction limit reached!
% 7.69/2.04 % (1895655)------------------------------
% 7.69/2.04 % (1895655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.69/2.04 % (1895655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/2.04 % (1895655)CaDiCaL version: 2.1.3
% 7.69/2.04 % (1895655)Termination reason: Instruction limit
% 7.69/2.04 % (1895655)Termination phase: Saturation
% 7.69/2.04 % (1895655)Time elapsed: 0.036 s
% 7.69/2.04 % (1895655)Peak memory usage: 89 MB
% 7.69/2.04 % (1895655)Instructions burned: 121 (million)
% 7.69/2.04 % (1895651)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=2159595377:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.69/2.04 % (1895657)dis-21_1_sil=8000:lcm=predicate:random_seed=3882881133: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.69/2.04 % (1895656)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4076952144:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.69/2.04 % (1895654)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=365362476:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.69/2.04 % (1895652)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=1161779766:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.69/2.04 % (1895653)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=320578539:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.69/2.04 % (1895654)Instruction limit reached!
% 7.69/2.04 % (1895654)------------------------------
% 7.69/2.04 % (1895654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.69/2.04 % (1895654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/2.04 % (1895654)CaDiCaL version: 2.1.3
% 7.69/2.04 % (1895654)Termination reason: Instruction limit
% 7.69/2.04 % (1895654)Termination phase: Saturation
% 7.69/2.04 % (1895654)Time elapsed: 0.060 s
% 7.69/2.04 % (1895654)Peak memory usage: 91 MB
% 7.69/2.04 % (1895654)Instructions burned: 109 (million)
% 7.69/2.04 % (1895657)Instruction limit reached!
% 7.69/2.04 % (1895657)------------------------------
% 7.69/2.04 % (1895657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.69/2.04 % (1895657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/2.04 % (1895657)CaDiCaL version: 2.1.3
% 7.69/2.04 % (1895657)Termination reason: Instruction limit
% 7.69/2.04 % (1895657)Termination phase: Saturation
% 7.69/2.04 % (1895657)Time elapsed: 0.071 s
% 7.69/2.04 % (1895657)Peak memory usage: 92 MB
% 7.69/2.04 % (1895657)Instructions burned: 130 (million)
% 7.69/2.04 % (1895656)Instruction limit reached!
% 7.69/2.04 % (1895656)------------------------------
% 7.69/2.04 % (1895656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.69/2.04 % (1895656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/2.04 % (1895656)CaDiCaL version: 2.1.3
% 7.69/2.04 % (1895656)Termination reason: Instruction limit
% 7.69/2.04 % (1895656)Termination phase: Saturation
% 7.69/2.04 % (1895656)Time elapsed: 0.078 s
% 7.69/2.04 % (1895656)Peak memory usage: 92 MB
% 7.69/2.04 % (1895656)Instructions burned: 140 (million)
% 7.69/2.04 % (1895665)lrs+10_1_sil=8000:sp=occurrence:random_seed=263877698:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 7.69/2.04 % (1895668)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=2018530807:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 7.69/2.04 % (1895666)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1603401791:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.69/2.04 % (1895668)Refutation not found, incomplete strategy
% 7.69/2.04 % (1895668)------------------------------
% 7.69/2.04 % (1895668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.69/2.04 % (1895668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/2.04 % (1895668)CaDiCaL version: 2.1.3
% 7.69/2.04 % (1895668)Termination reason: Refutation not found, incomplete strategy
% 7.69/2.04 % (1895668)Time elapsed: 0.034 s
% 7.69/2.04 % (1895668)Peak memory usage: 92 MB
% 7.69/2.04 % (1895668)Instructions burned: 103 (million)
% 7.69/2.04 % (1895667)lrs+1011_1_sil=32000:sp=occurrence:random_seed=462646270:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.69/2.04 % (1895666)Refutation not found, incomplete strategy
% 7.69/2.04 % (1895666)------------------------------
% 7.69/2.04 % (1895666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.69/2.04 % (1895666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.69/2.04 % (1895666)CaDiCaL version: 2.1.3
% 7.69/2.04 % (1895666)Termination reason: Refutation not found, incomplete strategy
% 7.69/2.04 % (1895666)Time elapsed: 0.037 s
% 7.69/2.04 % (1895666)Peak memory usage: 91 MB
% 7.69/2.04 % (1895666)Instructions burned: 60 (million)
% 7.69/2.04 % (1895665)Instruction limit reached!
% 8.18/2.04 % (1895665)------------------------------
% 8.18/2.04 % (1895665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.04 % (1895665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.04 % (1895665)CaDiCaL version: 2.1.3
% 8.18/2.04 % (1895665)Termination reason: Instruction limit
% 8.18/2.04 % (1895665)Termination phase: Saturation
% 8.18/2.04 % (1895665)Time elapsed: 0.163 s
% 8.18/2.04 % (1895665)Peak memory usage: 94 MB
% 8.18/2.04 % (1895665)Instructions burned: 286 (million)
% 8.18/2.04 % (1895667)Refutation not found, incomplete strategy
% 8.18/2.04 % (1895667)------------------------------
% 8.18/2.04 % (1895667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.04 % (1895667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.04 % (1895667)CaDiCaL version: 2.1.3
% 8.18/2.04 % (1895667)Termination reason: Refutation not found, incomplete strategy
% 8.18/2.04 % (1895667)Time elapsed: 0.119 s
% 8.18/2.04 % (1895667)Peak memory usage: 93 MB
% 8.18/2.04 % (1895667)Instructions burned: 208 (million)
% 8.18/2.04 % (1895668)------------------------------
% 8.18/2.04 % (1895668)------------------------------
% 8.18/2.04 % (1895666)------------------------------
% 8.18/2.04 % (1895666)------------------------------
% 8.18/2.04 % (1895673)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3900010360:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 8.18/2.04 % (1895674)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=380126520:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.18/2.04 % (1895667)------------------------------
% 8.18/2.04 % (1895667)------------------------------
% 8.18/2.04 % (1895675)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3423720936:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.18/2.04 % (1895673)Instruction limit reached!
% 8.18/2.04 % (1895673)------------------------------
% 8.18/2.04 % (1895673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.04 % (1895673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.04 % (1895673)CaDiCaL version: 2.1.3
% 8.18/2.04 % (1895673)Termination reason: Instruction limit
% 8.18/2.04 % (1895673)Termination phase: Saturation
% 8.18/2.04 % (1895673)Time elapsed: 0.160 s
% 8.18/2.04 % (1895673)Peak memory usage: 94 MB
% 8.18/2.04 % (1895673)Instructions burned: 294 (million)
% 8.18/2.04 % (1895675)Instruction limit reached!
% 8.18/2.04 % (1895675)------------------------------
% 8.18/2.04 % (1895675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.04 % (1895675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.04 % (1895675)CaDiCaL version: 2.1.3
% 8.18/2.04 % (1895675)Termination reason: Instruction limit
% 8.18/2.04 % (1895675)Termination phase: Saturation
% 8.18/2.04 % (1895675)Time elapsed: 0.065 s
% 8.18/2.04 % (1895675)Peak memory usage: 92 MB
% 8.18/2.04 % (1895675)Instructions burned: 114 (million)
% 8.18/2.04 % (1895678)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1596870694:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 8.18/2.04 % (1895680)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3670257916:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.18/2.04 % (1895678)Instruction limit reached!
% 8.18/2.04 % (1895678)------------------------------
% 8.18/2.04 % (1895678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.04 % (1895678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.04 % (1895678)CaDiCaL version: 2.1.3
% 8.18/2.04 % (1895678)Termination reason: Instruction limit
% 8.18/2.04 % (1895678)Termination phase: Saturation
% 8.18/2.04 % (1895678)Time elapsed: 0.067 s
% 8.18/2.04 % (1895678)Peak memory usage: 90 MB
% 8.18/2.04 % (1895678)Instructions burned: 129 (million)
% 8.18/2.04 % (1895680)Instruction limit reached!
% 8.18/2.04 % (1895680)------------------------------
% 8.18/2.04 % (1895680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.04 % (1895680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.04 % (1895680)CaDiCaL version: 2.1.3
% 8.18/2.04 % (1895680)Termination reason: Instruction limit
% 8.18/2.04 % (1895680)Termination phase: Saturation
% 8.18/2.04 % (1895680)Time elapsed: 0.058 s
% 8.18/2.04 % (1895680)Peak memory usage: 90 MB
% 8.18/2.04 % (1895680)Instructions burned: 114 (million)
% 8.18/2.04 % (1895681)lrs+10_1_sil=8000:sp=occurrence:random_seed=1733102848:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 8.18/2.04 % (1895652)First to succeed.
% 8.18/2.04 % (1895652)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1895646"
% 8.18/2.04 % (1895684)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1861851664:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 8.18/2.04 % (1895686)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=643821517:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.18/2.04 % SZS status CounterSatisfiable for theBenchmark
% 8.18/2.04 % SZS output start Saturation.
% See solution above
% 8.18/2.04 % SZS output start Definitions and Model Updates.
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c5_1(X42) | ~c3_2(X42,a260) | ndr1_1(X42) | ~ndr1_0 is false, set ~c3_2(X42,a260) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X0) | ~c3_2(X0,a300) | ndr1_1(X0) | ~ndr1_0 | ~sP23 is false, set ~c3_2(X0,a300) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_1(X0) | ~c3_2(X0,a393) | ndr1_1(X0) | ~ndr1_0 | ~sP9 is false, set ~c3_2(X0,a393) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(X0) | ~c3_2(X0,a225) | ndr1_1(X0) | ~ndr1_0 | ~sP30 is false, set ~c3_2(X0,a225) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X147) | ~c3_2(X147,a365) | ndr1_1(X147) | ~ndr1_0 is false, set ~c3_2(X147,a365) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_1(X0) | ~c3_2(X0,a348) | ndr1_1(X0) | ~ndr1_0 | ~sP16 is false, set ~c3_2(X0,a348) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ndr1_1(X0) | ~c2_2(X0,a272) | ~ndr1_0 | ~sP27 is false, set ~c2_2(X0,a272) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c3_0 | ndr1_1(X10) | ~c2_2(X10,a232) | sP28(X10) | ~ndr1_0 is false, set ~c2_2(X10,a232) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c9_0 | ~c7_0 | c9_1(X87) | ~c2_2(X87,a311) | ndr1_1(X87) | ~ndr1_0 is false, set ~c2_2(X87,a311) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_1(X0) | ndr1_1(X0) | ~c2_2(X0,a349) | ~ndr1_0 | ~sP16 is false, set ~c2_2(X0,a349) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_1(X0) | c9_2(X0,a277) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set c9_2(X0,a277) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c8_0 | sP23 | ~c8_1(X78) | c9_2(X78,a302) | ndr1_1(X78) | ~ndr1_0 is false, set c9_2(X78,a302) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_1(X0) | c9_2(X0,a348) | ndr1_1(X0) | ~ndr1_0 | ~sP16 is false, set c9_2(X0,a348) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c9_0 | ~c7_0 | c9_1(X87) | ndr1_1(X87) | c9_2(X87,a312) | ~ndr1_0 is false, set c9_2(X87,a312) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ndr1_0 | c10_2(a242,X21) | c9_2(a242,X21) | ~c2_2(a242,X21) | ~ndr1_1(a242) is false, set c9_2(a242,X21) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_1(X0) | c1_2(X0,a277) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set c1_2(X0,a277) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_1(X0) | c1_2(X0,a393) | ndr1_1(X0) | ~ndr1_0 | ~sP9 is false, set c1_2(X0,a393) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c4_0 | c5_1(X71) | c1_2(X71,a290) | ndr1_1(X71) | ~ndr1_0 is false, set c1_2(X71,a290) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_1(X0) | ndr1_1(X0) | c1_2(X0,a394) | ~ndr1_0 | ~sP9 is false, set c1_2(X0,a394) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(X0) | c6_2(X0,a225) | ndr1_1(X0) | ~ndr1_0 | ~sP30 is false, set c6_2(X0,a225) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(X0) | ndr1_1(X0) | c6_2(X0,a226) | ~ndr1_0 | ~sP30 is false, set c6_2(X0,a226) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ndr1_1(X0) | c6_2(X0,a272) | ~ndr1_0 | ~sP27 is false, set c6_2(X0,a272) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_2(X0,a307) | ndr1_1(X0) | ~ndr1_0 | ~sP22 is false, set c6_2(X0,a307) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c1_2(X0,a307) | ndr1_1(X0) | ~ndr1_0 | ~sP22 is false, set c1_2(X0,a307) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(X0) | ndr1_1(X0) | ~c7_2(X0,a226) | ~ndr1_0 | ~sP30 is false, set ~c7_2(X0,a226) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X147) | ndr1_1(X147) | ~c7_2(X147,a366) | ~ndr1_0 is false, set ~c7_2(X147,a366) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_1(X0) | c2_2(X0,a378) | ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set c2_2(X0,a378) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_1(X0) | ndr1_1(X0) | c7_2(X0,a278) | ~ndr1_0 | ~sP25 is false, set c7_2(X0,a278) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | c7_2(X0,a275) | ndr1_1(X0) | ~ndr1_0 | ~sP26 is false, set c7_2(X0,a275) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ndr1_1(X0) | c7_2(X0,a308) | ~ndr1_0 | ~sP22 is false, set c7_2(X0,a308) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_1(X0) | c7_2(X0,a378) | ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set c7_2(X0,a378) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c4_0 | c5_1(X71) | c7_2(X71,a290) | ndr1_1(X71) | ~ndr1_0 is false, set c7_2(X71,a290) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X147) | c2_2(X147,a365) | ndr1_1(X147) | ~ndr1_0 is false, set c2_2(X147,a365) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | c2_2(X0,a275) | ndr1_1(X0) | ~ndr1_0 | ~sP26 is false, set c2_2(X0,a275) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X0) | c2_2(X0,a300) | ndr1_1(X0) | ~ndr1_0 | ~sP23 is false, set c2_2(X0,a300) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c5_1(X42) | ndr1_1(X42) | c7_2(X42,a261) | ~ndr1_0 is false, set c7_2(X42,a261) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_1(X0) | c7_2(X0,a393) | ndr1_1(X0) | ~ndr1_0 | ~sP9 is false, set c7_2(X0,a393) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(X0) | c7_2(X0,a225) | ndr1_1(X0) | ~ndr1_0 | ~sP30 is false, set c7_2(X0,a225) to true
% 8.18/2.04 for all groundings, until fixed point,
% 8.18/2.04 whenever ndr1_1(X54) | ~ndr1_0 | ndr1_0 is false, set ~ndr1_0 to true
% 8.18/2.04 for all groundings, until fixed point,
% 8.18/2.04 whenever ~c2_2(X54,a268) | ~ndr1_0 | ndr1_0 is false, set ~ndr1_0 to true
% 8.18/2.04 for all groundings, until fixed point,
% 8.18/2.04 whenever ~c3_2(X54,a268) | ~ndr1_0 | ndr1_0 is false, set ~ndr1_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | c3_2(X0,a271) | ndr1_1(X0) | ~ndr1_0 | ~sP27 is false, set c3_2(X0,a271) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_1(X0) | ~c8_2(X0,a378) | ndr1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~c8_2(X0,a378) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c8_0 | sP23 | ~c8_1(X78) | ndr1_1(X78) | ~c8_2(X78,a303) | ~ndr1_0 is false, set ~c8_2(X78,a303) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c8_0 | sP23 | ~c8_1(X78) | ~c8_2(X78,a302) | ndr1_1(X78) | ~ndr1_0 is false, set ~c8_2(X78,a302) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ndr1_0 | ~c3_2(a424,X194) | ~c6_2(a424,X194) | ~c8_2(a424,X194) | ~ndr1_1(a424) | sP1 is false, set ~c8_2(a424,X194) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_1(X0) | ndr1_1(X0) | c3_2(X0,a379) | ~ndr1_0 | ~sP12 is false, set c3_2(X0,a379) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c3_0 | ndr1_1(X10) | c4_2(X10,a232) | sP28(X10) | ~ndr1_0 is false, set c4_2(X10,a232) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c5_1(X42) | c4_2(X42,a260) | ndr1_1(X42) | ~ndr1_0 is false, set c4_2(X42,a260) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_2(X54,a268) | ~ndr1_0 | ndr1_0 is false, set c4_2(X54,a268) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c9_0 | ~c7_0 | c9_1(X87) | c4_2(X87,a311) | ndr1_1(X87) | ~ndr1_0 is false, set c4_2(X87,a311) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X147) | c4_2(X147,a365) | ndr1_1(X147) | ~ndr1_0 is false, set c4_2(X147,a365) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X0) | c4_2(X0,a300) | ndr1_1(X0) | ~ndr1_0 | ~sP23 is false, set c4_2(X0,a300) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ndr1_1(X0) | c5_2(X0,a276) | ~ndr1_0 | ~sP26 is false, set c5_2(X0,a276) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c8_0 | sP23 | ~c8_1(X78) | ndr1_1(X78) | c5_2(X78,a303) | ~ndr1_0 is false, set c5_2(X78,a303) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c8_0 | sP23 | ~c8_1(X78) | c5_2(X78,a302) | ndr1_1(X78) | ~ndr1_0 is false, set c5_2(X78,a302) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c4_0 | c5_1(X71) | c5_2(X71,a290) | ndr1_1(X71) | ~ndr1_0 is false, set c5_2(X71,a290) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c4_0 | c5_1(X71) | ndr1_1(X71) | ~c6_2(X71,a291) | ~ndr1_0 is false, set ~c6_2(X71,a291) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c9_0 | ~c7_0 | c9_1(X87) | ndr1_1(X87) | ~c6_2(X87,a312) | ~ndr1_0 is false, set ~c6_2(X87,a312) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c9_0 | ~c7_0 | c9_1(X87) | ndr1_1(X87) | c8_2(X87,a312) | ~ndr1_0 is false, set c8_2(X87,a312) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | c8_2(X0,a271) | ndr1_1(X0) | ~ndr1_0 | ~sP27 is false, set c8_2(X0,a271) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c3_0 | c8_2(X10,a231) | ndr1_1(X10) | sP28(X10) | ~ndr1_0 is false, set c8_2(X10,a231) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c3_0 | ndr1_1(X10) | c8_2(X10,a232) | sP28(X10) | ~ndr1_0 is false, set c8_2(X10,a232) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_1(X0) | ndr1_1(X0) | c8_2(X0,a278) | ~ndr1_0 | ~sP25 is false, set c8_2(X0,a278) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ndr1_1(X0) | c8_2(X0,a272) | ~ndr1_0 | ~sP27 is false, set c8_2(X0,a272) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(a423) | ndr1_0 | sP1 is false, set ~c5_1(a423) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ndr1_0 | c5_1(a424) | sP1 is false, set c5_1(a424) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X0) | ndr1_1(X0) | ~c1_2(X0,a301) | ~ndr1_0 | ~sP23 is false, set ~c1_2(X0,a301) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_1(X0) | ndr1_1(X0) | ~c1_2(X0,a349) | ~ndr1_0 | ~sP16 is false, set ~c1_2(X0,a349) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_1(X0) | ndr1_1(X0) | ~c1_2(X0,a379) | ~ndr1_0 | ~sP12 is false, set ~c1_2(X0,a379) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ndr1_0 | c10_2(a242,X22) | ~c1_2(a242,X22) | ~c2_2(a242,X22) | ~ndr1_1(a242) is false, set ~c1_2(a242,X22) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c5_1(X42) | ndr1_1(X42) | ~c1_2(X42,a261) | ~ndr1_0 is false, set ~c1_2(X42,a261) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X147) | ndr1_1(X147) | ~c1_2(X147,a366) | ~ndr1_0 is false, set ~c1_2(X147,a366) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c9_1(a241) | ndr1_0 is false, set ~c9_1(a241) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c3_0 | c10_2(X10,a231) | ndr1_1(X10) | sP28(X10) | ~ndr1_0 is false, set c10_2(X10,a231) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c5_1(X42) | c10_2(X42,a260) | ndr1_1(X42) | ~ndr1_0 is false, set c10_2(X42,a260) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ~c10_2(X0,a271) | ndr1_1(X0) | ~ndr1_0 | ~sP27 is false, set ~c10_2(X0,a271) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ndr1_1(X0) | ~c10_2(X0,a276) | ~ndr1_0 | ~sP26 is false, set ~c10_2(X0,a276) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_1(X0) | ~c10_2(X0,a277) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~c10_2(X0,a277) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_1(X0) | ndr1_1(X0) | ~c10_2(X0,a379) | ~ndr1_0 | ~sP12 is false, set ~c10_2(X0,a379) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_1(X0) | ndr1_1(X0) | ~c9_2(X0,a278) | ~ndr1_0 | ~sP25 is false, set ~c9_2(X0,a278) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X0) | ndr1_1(X0) | ~c9_2(X0,a301) | ~ndr1_0 | ~sP23 is false, set ~c9_2(X0,a301) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_2(X0,a307) | ndr1_1(X0) | ~ndr1_0 | ~sP22 is false, set ~c9_2(X0,a307) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_1(X0) | ndr1_1(X0) | ~c9_2(X0,a394) | ~ndr1_0 | ~sP9 is false, set ~c9_2(X0,a394) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c3_0 | ~c9_2(X10,a231) | ndr1_1(X10) | sP28(X10) | ~ndr1_0 is false, set ~c9_2(X10,a231) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c4_0 | c5_1(X71) | ndr1_1(X71) | ~c9_2(X71,a291) | ~ndr1_0 is false, set ~c9_2(X71,a291) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c9_0 | ~c7_0 | c9_1(X87) | ~c9_2(X87,a311) | ndr1_1(X87) | ~ndr1_0 is false, set ~c9_2(X87,a311) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X147) | ndr1_1(X147) | ~c9_2(X147,a366) | ~ndr1_0 is false, set ~c9_2(X147,a366) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c5_1(X0) | ndr1_1(X0) | ~c4_2(X0,a226) | ~ndr1_0 | ~sP30 is false, set ~c4_2(X0,a226) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X0) | ndr1_1(X0) | ~c4_2(X0,a276) | ~ndr1_0 | ~sP26 is false, set ~c4_2(X0,a276) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X0) | ndr1_1(X0) | ~c4_2(X0,a301) | ~ndr1_0 | ~sP23 is false, set ~c4_2(X0,a301) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ndr1_1(X0) | ~c4_2(X0,a308) | ~ndr1_0 | ~sP22 is false, set ~c4_2(X0,a308) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c5_1(X42) | ndr1_1(X42) | ~c4_2(X42,a261) | ~ndr1_0 is false, set ~c4_2(X42,a261) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_1(X0) | ~c4_2(X0,a348) | ndr1_1(X0) | ~ndr1_0 | ~sP16 is false, set ~c4_2(X0,a348) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ndr1_1(X0) | ~c5_2(X0,a308) | ~ndr1_0 | ~sP22 is false, set ~c5_2(X0,a308) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_1(X0) | ndr1_1(X0) | ~c5_2(X0,a349) | ~ndr1_0 | ~sP16 is false, set ~c5_2(X0,a349) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ndr1_0 | c8_2(a242,X23) | ~c1_2(a242,X23) | ~c5_2(a242,X23) | ~ndr1_1(a242) is false, set ~c5_2(a242,X23) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c4_0 | c5_1(X71) | ndr1_1(X71) | ~c5_2(X71,a291) | ~ndr1_0 is false, set ~c5_2(X71,a291) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ndr1_0 | ~c1_2(a424,X193) | ~c2_2(a424,X193) | ~c5_2(a424,X193) | ~ndr1_1(a424) | sP1 is false, set ~c5_2(a424,X193) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | c7_1(a241) | ndr1_0 is false, set c7_1(a241) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c6_1(a423) | ndr1_0 | sP1 is false, set ~c6_1(a423) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c2_0 | ~c8_0 | c8_1(X104) | c10_2(X104,X105) | ~c8_2(X104,X105) | ~c9_2(X104,X105) | ~ndr1_1(X104) | ndr1_1(X104) | ~ndr1_0 is false, set ~c2_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c10_0 | c1_1(X5) | c9_1(X5) | ~c7_1(X5) | ~ndr1_0 | ndr1_0 is false, set c1_1(X5) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c5_1(X72) | ~c6_1(X72) | ndr1_1(X72) | ~ndr1_0 | ndr1_0 is false, set c7_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c5_1(X72) | ~c6_1(X72) | c7_2(X72,a292) | ~ndr1_0 | ndr1_0 is false, set c7_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c5_1(X72) | ~c6_1(X72) | ~c9_2(X72,a292) | ~ndr1_0 | ndr1_0 is false, set c7_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | ~c5_1(X72) | ~c6_1(X72) | ~c1_2(X72,a292) | ~ndr1_0 | ndr1_0 is false, set c7_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c7_0 | c9_0 | c10_2(X66,X67) | c8_2(X66,X67) | ~c3_2(X66,X67) | ~ndr1_1(X66) | c6_2(X66,X68) | c9_2(X66,X68) | ~c1_2(X66,X68) | ~ndr1_1(X66) | ndr1_1(X66) | ~ndr1_0 is false, set c7_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c1_1(X188) | ~c5_1(X188) | ~c8_1(X188) | ~ndr1_0 | ndr1_0 is false, set ~c8_1(X188) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c3_0 | c7_0 | ndr1_0 is false, set c3_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c7_0 | c3_1(X127) | ~c4_1(X127) | ~c5_1(X127) | ~ndr1_0 | ~c7_1(X128) | c1_2(X128,X129) | c2_2(X128,X129) | c3_2(X128,X129) | ~ndr1_1(X128) | ndr1_1(X128) | ~ndr1_0 is false, set c3_1(X127) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c8_0 | c3_1(X136) | c9_1(X136) | ndr1_1(X136) | ~ndr1_0 | c8_1(X137) | c3_2(X137,X138) | ~c2_2(X137,X138) | ~c5_2(X137,X138) | ~ndr1_1(X137) | ndr1_1(X137) | ~ndr1_0 is false, set c3_1(X136) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c8_0 | c3_1(X136) | c9_1(X136) | c1_2(X136,a358) | ~ndr1_0 | c8_1(X137) | c3_2(X137,X138) | ~c2_2(X137,X138) | ~c5_2(X137,X138) | ~ndr1_1(X137) | ndr1_1(X137) | ~ndr1_0 is false, set c3_1(X136) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c8_0 | c3_1(X136) | c9_1(X136) | ~c3_2(X136,a358) | ~ndr1_0 | c8_1(X137) | c3_2(X137,X138) | ~c2_2(X137,X138) | ~c5_2(X137,X138) | ~ndr1_1(X137) | ndr1_1(X137) | ~ndr1_0 is false, set c3_1(X136) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c8_0 | c3_1(X136) | c9_1(X136) | c8_2(X136,a358) | ~ndr1_0 | c8_1(X137) | c3_2(X137,X138) | ~c2_2(X137,X138) | ~c5_2(X137,X138) | ~ndr1_1(X137) | ndr1_1(X137) | ~ndr1_0 is false, set c3_1(X136) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | c3_1(X142) | ~c5_1(X142) | ~c7_1(X142) | ~ndr1_0 | ndr1_0 is false, set c3_1(X142) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | ~c7_0 | ~c2_2(X31,X32) | ~c3_2(X31,X32) | ~ndr1_1(X31) | ndr1_1(X31) | ~c5_2(X31,a255) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | ~c7_0 | ~c2_2(X31,X32) | ~c3_2(X31,X32) | ~ndr1_1(X31) | ndr1_1(X31) | ndr1_1(X31) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | ~c7_0 | ~c2_2(X31,X32) | ~c3_2(X31,X32) | ~ndr1_1(X31) | c1_2(X31,a254) | ndr1_1(X31) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | ~c7_0 | ~c2_2(X31,X32) | ~c3_2(X31,X32) | ~ndr1_1(X31) | ndr1_1(X31) | ~c8_2(X31,a255) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | ~c7_0 | ~c2_2(X31,X32) | ~c3_2(X31,X32) | ~ndr1_1(X31) | ~c3_2(X31,a254) | ndr1_1(X31) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | c8_2(X39,X40) | c9_2(X39,X40) | ~ndr1_1(X39) | ~c1_2(X39,X41) | ~c7_2(X39,X41) | ~c9_2(X39,X41) | ~ndr1_1(X39) | ndr1_1(X39) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | ~c7_0 | ~c2_2(X31,X32) | ~c3_2(X31,X32) | ~ndr1_1(X31) | c2_2(X31,a254) | ndr1_1(X31) | ~ndr1_0 is false, set c4_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | ndr1_0 | c5_2(a401,X180) | ~c8_2(a401,X180) | ~ndr1_1(a401) is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | ndr1_0 | ndr1_0 is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | ndr1_0 | ~c1_2(a401,X182) | ~c10_2(a401,X182) | ~c2_2(a401,X182) | ~ndr1_1(a401) is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | ~c3_1(a400) | ndr1_0 is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | ndr1_0 | c8_2(a401,X181) | ~c2_2(a401,X181) | ~c4_2(a401,X181) | ~ndr1_1(a401) is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | c1_2(a400,X178) | c10_2(a400,X178) | ~c3_2(a400,X178) | ~ndr1_1(a400) | ndr1_0 is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c6_1(X177) | c8_1(X177) | ~c4_1(X177) | ~ndr1_0 | ~c1_2(a400,X179) | ~c7_2(a400,X179) | ~c9_2(a400,X179) | ~ndr1_1(a400) | ndr1_0 is false, set c6_1(X177) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_0 | c10_1(X34) | c2_2(X34,X35) | c3_2(X34,X35) | c4_2(X34,X35) | ~ndr1_1(X34) | c2_2(X34,X36) | c4_2(X34,X36) | c8_2(X34,X36) | ~ndr1_1(X34) | ~ndr1_0 | ndr1_0 is false, set c10_1(X34) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c10_1(a423) | ndr1_0 | sP1 is false, set c10_1(a423) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | ~c2_1(X143) | ~c5_1(X143) | ~c4_2(X143,X144) | ~c5_2(X143,X144) | ~ndr1_1(X143) | ~ndr1_0 | ndr1_0 is false, set ~c2_1(X143) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_0 | c10_1(X110) | c2_1(X110) | c6_2(X110,X111) | c8_2(X110,X111) | ~c3_2(X110,X111) | ~ndr1_1(X110) | ~ndr1_0 | c1_2(X112,X113) | ~c4_2(X112,X113) | ~c9_2(X112,X113) | ~ndr1_1(X112) | c6_2(X112,X114) | ~c2_2(X112,X114) | ~c3_2(X112,X114) | ~ndr1_1(X112) | ndr1_1(X112) | ~ndr1_0 is false, set ~c3_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c3_0 | c10_2(X117,X118) | c8_2(X117,X118) | ~c6_2(X117,X118) | ~ndr1_1(X117) | c10_2(X117,X119) | ~c3_2(X117,X119) | ~c8_2(X117,X119) | ~ndr1_1(X117) | c4_2(X117,X120) | ~c3_2(X117,X120) | ~c7_2(X117,X120) | ~ndr1_1(X117) | ~ndr1_0 | ndr1_0 is false, set ~c3_0 to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c2_0 | ~c10_1(a241) | ndr1_0 is false, set ~c10_1(a241) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | c1_1(X139) | ~c10_1(X139) | ~c10_2(X139,a360) | ~ndr1_0 | ~c9_1(X140) | c2_2(X140,X141) | ~c4_2(X140,X141) | ~c6_2(X140,X141) | ~ndr1_1(X140) | ndr1_1(X140) | ~ndr1_0 is false, set ~c10_1(X139) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | c1_1(X139) | ~c10_1(X139) | ndr1_1(X139) | ~ndr1_0 | ~c9_1(X140) | c2_2(X140,X141) | ~c4_2(X140,X141) | ~c6_2(X140,X141) | ~ndr1_1(X140) | ndr1_1(X140) | ~ndr1_0 is false, set ~c10_1(X139) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | c1_1(X139) | ~c10_1(X139) | c6_2(X139,a360) | ~ndr1_0 | ~c9_1(X140) | c2_2(X140,X141) | ~c4_2(X140,X141) | ~c6_2(X140,X141) | ~ndr1_1(X140) | ndr1_1(X140) | ~ndr1_0 is false, set ~c10_1(X139) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c8_0 | ~c10_1(X79) | ~c3_1(X79) | ~ndr1_0 | ndr1_0 is false, set ~c10_1(X79) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever c4_1(X167) | ~c10_1(X167) | ~c3_1(X167) | ~ndr1_0 | c6_1(X168) | c9_1(X168) | c6_2(X168,X169) | c8_2(X168,X169) | ~c5_2(X168,X169) | ~ndr1_1(X168) | ~ndr1_0 | ndr1_0 is false, set ~c10_1(X167) to true
% 8.18/2.04 for all groundings,
% 8.18/2.04 whenever ~c9_0 | c1_1(X139) | ~c10_1(X139) | c9_2(X139,a360) | ~ndr1_0 | ~c9_1(X140) | c2_2(X140,X141) | ~c4_2(X140,X141) | ~c6_2(X140,X141) | ~ndr1_1(X140) | ndr1_1(X140) | ~ndr1_0 is false, set ~c10_1(X139) to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c10_0 | c7_1(X44) | c10_2(X44,X45) | ~c5_2(X44,X45) | ~c7_2(X44,X45) | ~ndr1_1(X44) | ndr1_1(X44) | ~ndr1_0 is false, set ~c10_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c10_0 | c5_1(X101) | ~c7_1(X101) | c8_2(X101,X102) | c9_2(X101,X102) | ~c2_2(X101,X102) | ~ndr1_1(X101) | ~ndr1_0 | ndr1_0 is false, set ~c10_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c9_0 | sP14 | ndr1_0 is false, set sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c4_0 | sP16 | ndr1_0 is false, set sP16 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | c5_2(X81,a305) | ndr1_1(X81) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | ndr1_1(X81) | ~c9_2(X81,a306) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | ndr1_1(X81) | ~c4_2(X81,a306) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | c6_2(X81,a305) | ndr1_1(X81) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | c8_2(X81,a305) | ndr1_1(X81) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | ndr1_1(X81) | c5_2(X81,a306) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c8_0 | c1_2(X81,X82) | ~c10_2(X81,X82) | ~c7_2(X81,X82) | ~ndr1_1(X81) | ndr1_1(X81) | ndr1_1(X81) | ~ndr1_0 | sP22 is false, set sP22 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c10_0 | sP30 | ndr1_0 is false, set sP30 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP8 is false, set ~sP8 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP13 is false, set ~sP13 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_0 | ~c2_1(X94) | c10_2(X94,X95) | ~c1_2(X94,X95) | ~c5_2(X94,X95) | ~ndr1_1(X94) | c4_2(X94,a325) | ~ndr1_0 | ndr1_0 is false, set ~c1_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_0 | c1_1(X91) | c4_1(X91) | c1_2(X91,X92) | c2_2(X91,X92) | ~c6_2(X91,X92) | ~ndr1_1(X91) | ~ndr1_0 | ndr1_0 is false, set ~c1_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_0 | ~c2_1(X94) | c10_2(X94,X95) | ~c1_2(X94,X95) | ~c5_2(X94,X95) | ~ndr1_1(X94) | ndr1_1(X94) | ~ndr1_0 | ndr1_0 is false, set ~c1_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_0 | ~c2_1(X94) | c10_2(X94,X95) | ~c1_2(X94,X95) | ~c5_2(X94,X95) | ~ndr1_1(X94) | ndr1_1(X94) | ~ndr1_0 | c4_2(a326,X96) | c6_2(a326,X96) | ~c7_2(a326,X96) | ~ndr1_1(a326) is false, set ~c1_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_0 | ~c2_1(X94) | c10_2(X94,X95) | ~c1_2(X94,X95) | ~c5_2(X94,X95) | ~ndr1_1(X94) | ndr1_1(X94) | ~ndr1_0 | ~c10_2(a326,X97) | ~c5_2(a326,X97) | ~c9_2(a326,X97) | ~ndr1_1(a326) is false, set ~c1_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_0 | ~c2_1(X94) | c10_2(X94,X95) | ~c1_2(X94,X95) | ~c5_2(X94,X95) | ~ndr1_1(X94) | c3_2(X94,a325) | ~ndr1_0 | ndr1_0 is false, set ~c1_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ~c1_2(X0,a367) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c5_2(X0,a368) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c4_2(X0,a368) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ~c2_2(X0,a367) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ~c6_2(X0,a367) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c1_2(X0,a368) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c7_2(X0,X1) | ~c4_2(X0,X1) | ~c6_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set ~sP14 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | c10_1(X59) | c8_2(X59,X60) | ~c6_2(X59,X60) | ~c7_2(X59,X60) | ~ndr1_1(X59) | ndr1_1(X59) | ~ndr1_0 | sP27 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | sP25 | c3_2(X63,X64) | ~c7_2(X63,X64) | ~ndr1_1(X63) | ~c2_2(X63,a279) | ndr1_1(X63) | ~ndr1_0 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | sP25 | c3_2(X63,X64) | ~c7_2(X63,X64) | ~ndr1_1(X63) | ~c8_2(X63,a279) | ndr1_1(X63) | ~ndr1_0 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | sP25 | c3_2(X63,X64) | ~c7_2(X63,X64) | ~ndr1_1(X63) | ndr1_1(X63) | ~c5_2(X63,a280) | ~ndr1_0 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | sP25 | c3_2(X63,X64) | ~c7_2(X63,X64) | ~ndr1_1(X63) | ~c9_2(X63,a279) | ndr1_1(X63) | ~ndr1_0 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | sP25 | c3_2(X63,X64) | ~c7_2(X63,X64) | ~ndr1_1(X63) | ndr1_1(X63) | ~c4_2(X63,a280) | ~ndr1_0 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c6_0 | sP25 | c3_2(X63,X64) | ~c7_2(X63,X64) | ~ndr1_1(X63) | ndr1_1(X63) | ndr1_1(X63) | ~ndr1_0 is false, set c6_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X171) | ~c1_1(X171) | ndr1_1(X171) | ~ndr1_0 | ~c7_1(X172) | c2_2(X172,X173) | c7_2(X172,X173) | ~c6_2(X172,X173) | ~ndr1_1(X172) | ndr1_1(X172) | ~ndr1_0 | sP9 is false, set sP9 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X171) | ~c1_1(X171) | c5_2(X171,a391) | ~ndr1_0 | ~c7_1(X172) | c2_2(X172,X173) | c7_2(X172,X173) | ~c6_2(X172,X173) | ~ndr1_1(X172) | ndr1_1(X172) | ~ndr1_0 | sP9 is false, set sP9 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X171) | ~c1_1(X171) | c7_2(X171,a391) | ~ndr1_0 | ~c7_1(X172) | c2_2(X172,X173) | c7_2(X172,X173) | ~c6_2(X172,X173) | ~ndr1_1(X172) | ndr1_1(X172) | ~ndr1_0 | sP9 is false, set sP9 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP3 is false, set ~sP3 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X171) | ~c1_1(X171) | ~c6_2(X171,a391) | ~ndr1_0 | ~c7_1(X172) | c2_2(X172,X173) | c7_2(X172,X173) | ~c6_2(X172,X173) | ~ndr1_1(X172) | ndr1_1(X172) | ~ndr1_0 | sP9 is false, set sP9 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X174) | ~c9_1(X174) | ndr1_1(X174) | ~ndr1_0 | ~c8_1(X175) | c6_2(X175,X176) | ~c7_2(X175,X176) | ~ndr1_1(X175) | ndr1_1(X175) | ~ndr1_0 | sP8 is false, set sP8 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X174) | ~c9_1(X174) | c10_2(X174,a395) | ~ndr1_0 | ~c8_1(X175) | c6_2(X175,X176) | ~c7_2(X175,X176) | ~ndr1_1(X175) | ndr1_1(X175) | ~ndr1_0 | sP8 is false, set sP8 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X174) | ~c9_1(X174) | c3_2(X174,a395) | ~ndr1_0 | ~c8_1(X175) | c6_2(X175,X176) | ~c7_2(X175,X176) | ~ndr1_1(X175) | ndr1_1(X175) | ~ndr1_0 | sP8 is false, set sP8 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c5_1(X174) | ~c9_1(X174) | ~c9_2(X174,a395) | ~ndr1_0 | ~c8_1(X175) | c6_2(X175,X176) | ~c7_2(X175,X176) | ~ndr1_1(X175) | ndr1_1(X175) | ~ndr1_0 | sP8 is false, set sP8 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c9_1(X185) | c3_2(X185,X186) | c6_2(X185,X186) | ~ndr1_1(X185) | ndr1_1(X185) | ~ndr1_0 | ~c3_1(X187) | ~c7_1(X187) | ~c8_1(X187) | ~ndr1_0 | sP4 is false, set sP4 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c2_1(X161) | ~c7_1(X161) | c9_2(X161,X162) | ~c3_2(X161,X162) | ~c8_2(X161,X162) | ~ndr1_1(X161) | ~ndr1_0 | sP11 | ndr1_0 is false, set sP11 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c2_0 | c6_1(X11) | c7_1(X11) | c7_2(X11,X12) | ~c3_2(X11,X12) | ~c8_2(X11,X12) | ~ndr1_1(X11) | ~ndr1_0 | ndr1_0 is false, set c2_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c2_0 | c2_2(X18,X19) | c7_2(X18,X19) | ~c8_2(X18,X19) | ~ndr1_1(X18) | c2_2(X18,X20) | c8_2(X18,X20) | ~c5_2(X18,X20) | ~ndr1_1(X18) | ~ndr1_0 | ndr1_0 is false, set c2_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c2_0 | ~c5_1(X15) | c3_2(X15,X16) | c5_2(X15,X16) | ~c10_2(X15,X16) | ~ndr1_1(X15) | c3_2(X15,X17) | c7_2(X15,X17) | ~c9_2(X15,X17) | ~ndr1_1(X15) | ~ndr1_0 | ndr1_0 is false, set c2_0 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP11 is false, set ~sP11 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_1(X189) | ~c5_1(X189) | ndr1_1(X189) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_1(X189) | ~c5_1(X189) | c9_2(X189,a416) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c1_1(X189) | ~c5_1(X189) | ~c6_2(X189,a416) | ~ndr1_0 | ndr1_0 | sP3 is false, set sP3 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c1_1(X148) | ~c8_1(X148) | ~c1_2(X148,a373) | ~ndr1_0 | sP13 | ndr1_0 is false, set sP13 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c1_1(X148) | ~c8_1(X148) | c3_2(X148,a373) | ~ndr1_0 | sP13 | ndr1_0 is false, set sP13 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c1_1(X148) | ~c8_1(X148) | ~c8_2(X148,a373) | ~ndr1_0 | sP13 | ndr1_0 is false, set sP13 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c1_1(X148) | ~c8_1(X148) | ndr1_1(X148) | ~ndr1_0 | sP13 | ndr1_0 is false, set sP13 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c10_0 | ~c8_1(X7) | c6_2(X7,X8) | ~c8_2(X7,X8) | ~ndr1_1(X7) | ndr1_1(X7) | ~ndr1_0 | sP29 is false, set sP29 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c2_1(X190) | ~c6_1(X190) | c1_2(X190,X191) | c4_2(X190,X191) | c5_2(X190,X191) | ~ndr1_1(X190) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP4 is false, set ~sP4 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP2 is false, set ~sP2 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP7 is false, set ~sP7 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP10 is false, set ~sP10 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ~c1_2(X0,a298) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c8_2(X0,a299) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c4_2(X0,a299) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ~c5_2(X0,a298) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ~c9_2(X0,a298) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~c3_2(X0,a299) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever c3_2(X0,X1) | ~c1_2(X0,X1) | ~c7_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP24 is false, set ~sP24 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP29 is false, set ~sP29 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP6 is false, set ~sP6 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP21 is false, set ~sP21 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ndr1_0 | ~sP5 is false, set ~sP5 to true
% 10.10/2.24 for all groundings,
% 10.10/2.24 whenever ~c5_0 is false, set ~c5_0 to true
% 10.10/2.24 % SZS output end Definitions and Model Updates.
% 10.10/2.24 % (1895652)------------------------------
% 10.10/2.24 % (1895652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.10/2.24 % (1895652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/2.24 % (1895652)CaDiCaL version: 2.1.3
% 10.10/2.24 % (1895652)Termination reason: Satisfiable
% 10.10/2.24 % (1895652)Time elapsed: 0.900 s
% 10.10/2.24 % (1895652)Peak memory usage: 138 MB
% 10.10/2.24 % (1895652)Instructions burned: 1392 (million)
% 10.10/2.24 % (1895652)------------------------------
% 10.10/2.24 % (1895652)------------------------------
% 10.10/2.24 % (1895646)Success in time 1.344 s
% 10.10/2.24 % Vampire exiting
%------------------------------------------------------------------------------