%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN520+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:00:48 PM UTC 2026
% Result : CounterSatisfiable 5.80s 1.58s
% Output : Saturation 5.80s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1052,negated_conjecture,
( ~ c5_1(X166)
| ~ c2_1(X166)
| ~ ndr1_1(X166)
| ~ c3_2(X166,X167)
| ~ c5_2(X166,X167)
| ~ c1_2(X166,X167) ) ).
cnf(u1186,negated_conjecture,
ndr1_0 ).
cnf(u1062,negated_conjecture,
( ~ c4_1(X164)
| ~ c1_1(X164)
| c2_1(X164) ) ).
cnf(u1065,negated_conjecture,
( ~ c2_2(X163,a1526)
| ~ c1_1(X163)
| c4_1(X163) ) ).
cnf(u1113,negated_conjecture,
~ c2_0 ).
cnf(u1084,negated_conjecture,
c5_2(a1524,a1525) ).
cnf(u1129,negated_conjecture,
~ c1_0 ).
cnf(u1094,negated_conjecture,
ndr1_1(a1524) ).
cnf(u1099,negated_conjecture,
( c1_2(a1524,X162)
| ~ c4_2(a1524,X162) ) ).
cnf(u2438,negated_conjecture,
~ sP0 ).
cnf(u1136,negated_conjecture,
~ c4_0 ).
cnf(u1172,negated_conjecture,
~ c2_1(a1516) ).
cnf(u1179,negated_conjecture,
c5_1(a1516) ).
cnf(u1219,negated_conjecture,
( ~ c1_1(X154)
| ~ c3_1(X154)
| c5_1(X154) ) ).
cnf(u1222,negated_conjecture,
~ c5_2(a1510,a1511) ).
cnf(u1226,negated_conjecture,
~ c1_2(a1510,a1511) ).
cnf(u1230,negated_conjecture,
~ c2_2(a1510,a1511) ).
cnf(u1234,negated_conjecture,
ndr1_1(a1510) ).
cnf(u1289,negated_conjecture,
( ~ ndr1_1(X148)
| c3_2(X148,a1505)
| ~ c2_2(X148,X149)
| ~ c1_2(X148,X149)
| ~ c5_2(X148,X149) ) ).
cnf(u1293,negated_conjecture,
( ~ c4_2(X148,a1505)
| ~ ndr1_1(X148)
| ~ c2_2(X148,X149)
| ~ c1_2(X148,X149)
| ~ c5_2(X148,X149) ) ).
cnf(u1297,negated_conjecture,
( ~ ndr1_1(X148)
| c2_2(X148,a1505)
| ~ c2_2(X148,X149)
| ~ c1_2(X148,X149)
| ~ c5_2(X148,X149) ) ).
cnf(u1304,negated_conjecture,
( ~ c4_2(a1504,X147)
| ~ c3_2(a1504,X147)
| c5_2(a1504,X147) ) ).
cnf(u1311,negated_conjecture,
~ c4_1(a1504) ).
cnf(u1315,negated_conjecture,
~ c1_1(a1504) ).
cnf(u1319,negated_conjecture,
~ c3_1(a1503) ).
cnf(u2464,negated_conjecture,
~ sP2 ).
cnf(u1332,negated_conjecture,
~ ndr1_1(a1503) ).
cnf(u1339,negated_conjecture,
~ c5_1(a1503) ).
cnf(u1356,negated_conjecture,
~ ndr1_1(a1498) ).
cnf(u1363,negated_conjecture,
~ c5_1(a1498) ).
cnf(u1378,negated_conjecture,
sP3 ).
cnf(u1394,negated_conjecture,
~ ndr1_1(a1494) ).
cnf(u1406,negated_conjecture,
~ c2_1(a1493) ).
cnf(u1416,negated_conjecture,
( c2_2(a1493,X135)
| c1_2(a1493,X135) ) ).
cnf(u1436,negated_conjecture,
~ ndr1_1(a1490) ).
cnf(u1457,negated_conjecture,
( ~ ndr1_1(X126)
| c4_1(X126)
| c3_2(X126,a1489)
| c4_2(X126,X127)
| ~ c5_2(X126,X127) ) ).
cnf(u1461,negated_conjecture,
( ~ c1_2(X126,a1489)
| c4_1(X126)
| ~ ndr1_1(X126)
| c4_2(X126,X127)
| ~ c5_2(X126,X127) ) ).
cnf(u2556,negated_conjecture,
~ sP5 ).
cnf(u2521,negated_conjecture,
~ sP4 ).
cnf(u1472,negated_conjecture,
c1_1(a1483) ).
cnf(u1476,negated_conjecture,
~ c3_1(a1483) ).
cnf(u1480,negated_conjecture,
~ ndr1_1(a1483) ).
cnf(u1488,negated_conjecture,
~ ndr1_1(a1482) ).
cnf(u2582,negated_conjecture,
~ sP6 ).
cnf(u1498,negated_conjecture,
~ c5_1(a1482) ).
cnf(u2611,negated_conjecture,
~ sP7 ).
cnf(u1533,negated_conjecture,
~ c5_1(a1475) ).
cnf(u1537,negated_conjecture,
c4_1(a1475) ).
cnf(u1541,negated_conjecture,
~ ndr1_1(a1475) ).
cnf(u2637,negated_conjecture,
~ sP8 ).
cnf(u1618,negated_conjecture,
( ~ c1_2(X112,a1459)
| c1_1(X112)
| ~ ndr1_1(X112)
| ~ c3_2(X112,X113)
| c4_2(X112,X113)
| ~ c2_2(X112,X113) ) ).
cnf(u1622,negated_conjecture,
( ~ c3_2(X112,a1459)
| c1_1(X112)
| ~ ndr1_1(X112)
| ~ c3_2(X112,X113)
| c4_2(X112,X113)
| ~ c2_2(X112,X113) ) ).
cnf(u1626,negated_conjecture,
( ~ ndr1_1(X112)
| c4_2(X112,a1459)
| c1_1(X112)
| ~ c3_2(X112,X113)
| c4_2(X112,X113)
| ~ c2_2(X112,X113) ) ).
cnf(u1630,negated_conjecture,
~ ndr1_1(a1458) ).
cnf(u2663,negated_conjecture,
~ sP9 ).
cnf(u1644,negated_conjecture,
c2_1(a1454) ).
cnf(u1648,negated_conjecture,
~ c5_1(a1454) ).
cnf(u2698,negated_conjecture,
~ sP10 ).
cnf(u1670,negated_conjecture,
~ ndr1_1(a1446) ).
cnf(u1677,negated_conjecture,
~ c3_1(a1446) ).
cnf(u1681,negated_conjecture,
~ c5_1(a1446) ).
cnf(u1689,negated_conjecture,
~ c3_1(a1443) ).
cnf(u1692,negated_conjecture,
( ~ c1_1(X106)
| c2_2(X106,X107)
| ~ c4_2(X106,X108)
| c2_2(X106,X108)
| ~ c1_2(X106,X108)
| ~ ndr1_1(X106)
| ~ c4_2(X106,X107)
| c5_2(X106,X107) ) ).
cnf(u1696,negated_conjecture,
~ c4_2(a1443,a1444) ).
cnf(u1700,negated_conjecture,
c1_2(a1443,a1444) ).
cnf(u1704,negated_conjecture,
c3_2(a1443,a1444) ).
cnf(u1726,negated_conjecture,
( ~ ndr1_1(X100)
| c2_2(X100,a1435)
| c3_2(X100,X101)
| c5_2(X100,X101)
| ~ c4_2(X100,X101)
| c2_1(X100) ) ).
cnf(u1729,negated_conjecture,
~ ndr1_1(a1434) ).
cnf(u1736,negated_conjecture,
( ~ c4_2(X100,a1435)
| ~ ndr1_1(X100)
| c3_2(X100,X101)
| c5_2(X100,X101)
| ~ c4_2(X100,X101)
| c2_1(X100) ) ).
cnf(u1753,negated_conjecture,
sP12 ).
cnf(u2800,negated_conjecture,
~ sP13 ).
cnf(u1764,negated_conjecture,
( ~ c3_2(X97,a1433)
| c3_1(X97) ) ).
cnf(u1811,negated_conjecture,
c4_1(a1424) ).
cnf(u1818,negated_conjecture,
( ~ c4_2(a1424,X94)
| c3_2(a1424,X94)
| c1_2(a1424,X94) ) ).
cnf(u1822,negated_conjecture,
~ c1_1(a1424) ).
cnf(u1844,negated_conjecture,
( c5_2(X89,a1414)
| c2_1(X89)
| c3_1(X89) ) ).
cnf(u1851,negated_conjecture,
( c4_2(X89,a1414)
| c2_1(X89)
| c3_1(X89) ) ).
cnf(u1855,negated_conjecture,
( c2_2(X89,a1414)
| c2_1(X89)
| c3_1(X89) ) ).
cnf(u1859,negated_conjecture,
( ndr1_1(X89)
| c2_1(X89)
| c3_1(X89) ) ).
cnf(u1870,negated_conjecture,
( ~ ndr1_1(X87)
| ~ c2_2(X87,a1413)
| ~ c4_2(X87,X88)
| c5_2(X87,X88)
| ~ c1_2(X87,X88)
| c3_1(X87) ) ).
cnf(u1877,negated_conjecture,
( ~ c1_2(X83,a1410)
| ~ c4_1(X83)
| c2_1(X83) ) ).
cnf(u1881,negated_conjecture,
( ~ c4_1(X83)
| c5_2(X83,a1410)
| c2_1(X83) ) ).
cnf(u1885,negated_conjecture,
( ~ c4_1(X83)
| ndr1_1(X83)
| c2_1(X83) ) ).
cnf(u1889,negated_conjecture,
~ ndr1_1(a1409) ).
cnf(u1900,negated_conjecture,
~ c3_1(a1409) ).
cnf(u2886,negated_conjecture,
~ sP16 ).
cnf(u1969,negated_conjecture,
( ndr1_1(X78)
| c1_1(X78) ) ).
cnf(u1988,negated_conjecture,
( ~ c5_1(X73)
| ~ c3_2(X73,X75)
| ~ c5_2(X73,X75)
| ~ ndr1_1(X73)
| ~ c1_2(X73,X74)
| ~ c2_2(X73,X74)
| ~ c4_2(X73,X74) ) ).
cnf(u1994,negated_conjecture,
( ~ c5_2(X70,a1396)
| ~ ndr1_1(X70)
| ~ c3_2(X70,X71)
| ~ c4_2(X70,X71)
| ~ c1_1(X70) ) ).
cnf(u1998,negated_conjecture,
( ~ ndr1_1(X70)
| ~ c2_2(X70,a1396)
| ~ c3_2(X70,X71)
| ~ c4_2(X70,X71)
| ~ c1_1(X70) ) ).
cnf(u2006,negated_conjecture,
( ~ c3_1(X68)
| c2_2(X68,a1395)
| ~ ndr1_1(X68)
| c5_2(X68,X69)
| c3_2(X68,X69) ) ).
cnf(u2016,negated_conjecture,
( ~ c3_1(X68)
| c3_2(X68,a1395)
| ~ ndr1_1(X68)
| c5_2(X68,X69)
| c3_2(X68,X69) ) ).
cnf(u2064,negated_conjecture,
( ~ c5_1(X56)
| ~ ndr1_1(X56)
| c5_2(X56,X57)
| c3_2(X56,X57)
| c2_2(X56,X57)
| ~ c2_1(X56) ) ).
cnf(u2094,negated_conjecture,
( c2_2(X50,a1379)
| c2_1(X50)
| ~ ndr1_1(X50)
| c3_2(X50,X51)
| c5_2(X50,X51)
| c4_2(X50,X51) ) ).
cnf(u2101,negated_conjecture,
( ~ c5_2(X50,a1379)
| c2_1(X50)
| ~ ndr1_1(X50)
| c3_2(X50,X51)
| c5_2(X50,X51)
| c4_2(X50,X51) ) ).
cnf(u2105,negated_conjecture,
( ~ c1_2(X50,a1379)
| c2_1(X50)
| ~ ndr1_1(X50)
| c3_2(X50,X51)
| c5_2(X50,X51)
| c4_2(X50,X51) ) ).
cnf(u2109,negated_conjecture,
~ c3_1(a1378) ).
cnf(u2911,negated_conjecture,
~ sP18 ).
cnf(u2116,negated_conjecture,
~ ndr1_1(a1378) ).
cnf(u2133,negated_conjecture,
( ~ ndr1_1(X39)
| c4_1(X39)
| ~ c5_2(X39,X40)
| c2_2(X39,X40)
| ~ c4_2(X39,X40) ) ).
cnf(u2185,negated_conjecture,
~ c5_1(a1361) ).
cnf(u2977,negated_conjecture,
~ sP20 ).
cnf(u2192,negated_conjecture,
~ c1_1(a1361) ).
cnf(u2201,negated_conjecture,
( c1_2(X29,a1358)
| c1_1(X29)
| c1_2(X29,a1357) ) ).
cnf(u2205,negated_conjecture,
( c2_2(X29,a1358)
| c1_1(X29)
| c1_2(X29,a1357) ) ).
cnf(u2209,negated_conjecture,
( c3_2(X29,a1358)
| c1_1(X29)
| c1_2(X29,a1357) ) ).
cnf(u2213,negated_conjecture,
( c5_2(X29,a1357)
| c1_1(X29)
| c1_2(X29,a1358) ) ).
cnf(u2217,negated_conjecture,
( c2_2(X29,a1358)
| c1_1(X29)
| c5_2(X29,a1357) ) ).
cnf(u2221,negated_conjecture,
( c3_2(X29,a1358)
| c1_1(X29)
| c5_2(X29,a1357) ) ).
cnf(u2225,negated_conjecture,
( ~ c4_2(X29,a1357)
| c1_1(X29)
| c1_2(X29,a1358) ) ).
cnf(u2229,negated_conjecture,
( ~ c4_2(X29,a1357)
| c1_1(X29)
| c2_2(X29,a1358) ) ).
cnf(u2233,negated_conjecture,
( ~ c4_2(X29,a1357)
| c1_1(X29)
| c3_2(X29,a1358) ) ).
cnf(u3004,negated_conjecture,
~ sP21 ).
cnf(u2273,negated_conjecture,
~ c2_1(a1350) ).
cnf(u2277,negated_conjecture,
c5_1(a1350) ).
cnf(u2313,negated_conjecture,
c2_1(a1346) ).
cnf(u2317,negated_conjecture,
~ c4_1(a1346) ).
cnf(u2321,negated_conjecture,
c3_1(a1346) ).
cnf(u2407,negated_conjecture,
~ c4_1(a1325) ).
cnf(u2410,negated_conjecture,
( c5_2(X4,a1324)
| c3_1(X4)
| ~ c4_1(X4) ) ).
cnf(u2414,negated_conjecture,
c2_1(a1325) ).
cnf(u2418,negated_conjecture,
~ c1_1(a1325) ).
cnf(u2428,negated_conjecture,
( c3_2(X4,a1324)
| c3_1(X4)
| ~ c4_1(X4) ) ).
cnf(u2498,axiom,
c2_1(a1495) ).
cnf(u2502,axiom,
c2_2(a1495,a1496) ).
cnf(u2506,axiom,
~ c5_2(a1495,a1496) ).
cnf(u2510,axiom,
c1_2(a1495,a1496) ).
cnf(u2514,axiom,
ndr1_1(a1495) ).
cnf(u2519,axiom,
( ~ c5_2(a1495,X0)
| c1_2(a1495,X0) ) ).
cnf(u2735,axiom,
~ sP11 ).
cnf(u7118,axiom,
~ c3_1(a1439) ).
cnf(u2742,axiom,
c3_2(a1439,a1441) ).
cnf(u2746,axiom,
c5_2(a1439,a1441) ).
cnf(u2750,axiom,
c1_2(a1439,a1441) ).
cnf(u2754,axiom,
ndr1_1(a1439) ).
cnf(u2758,axiom,
~ c3_2(a1439,a1440) ).
cnf(u2762,axiom,
~ c4_2(a1439,a1440) ).
cnf(u2769,axiom,
~ c2_2(a1430,a1432) ).
cnf(u2773,axiom,
~ c4_2(a1430,a1432) ).
cnf(u2777,axiom,
~ c1_2(a1430,a1432) ).
cnf(u2781,axiom,
ndr1_1(a1430) ).
cnf(u2785,axiom,
c2_1(a1430) ).
cnf(u2789,axiom,
c5_2(a1430,a1431) ).
cnf(u2793,axiom,
c2_2(a1430,a1431) ).
cnf(u2797,axiom,
c1_2(a1430,a1431) ).
cnf(u2820,axiom,
ndr1_1(a1428) ).
cnf(u2806,axiom,
( c2_2(a1428,X0)
| ~ c1_2(a1428,X0) ) ).
cnf(u2810,axiom,
c2_2(a1428,a1429) ).
cnf(u2814,axiom,
~ c3_2(a1428,a1429) ).
cnf(u2818,axiom,
c4_2(a1428,a1429) ).
cnf(u3822,axiom,
~ c2_1(a1428) ).
cnf(u2828,axiom,
~ sP14 ).
cnf(u2852,axiom,
~ sP15 ).
cnf(u2939,axiom,
~ sP19 ).
cnf(u3032,axiom,
~ sP22 ).
cnf(u3069,axiom,
~ sP23 ).
cnf(u3098,axiom,
~ sP25 ).
cnf(u3129,negated_conjecture,
( ~ c5_1(X114)
| ~ ndr1_1(X114)
| c3_2(X114,X115)
| ~ c2_2(X114,X115)
| c4_2(X114,X115)
| c1_1(X114) ) ).
cnf(u3192,negated_conjecture,
~ c1_2(a1452,a1453) ).
cnf(u3196,negated_conjecture,
c2_2(a1452,a1453) ).
cnf(u3200,negated_conjecture,
ndr1_1(a1452) ).
cnf(u3204,negated_conjecture,
~ c5_1(a1452) ).
cnf(u3218,negated_conjecture,
~ ndr1_1(a1442) ).
cnf(u3221,negated_conjecture,
( c3_2(a1442,X105)
| ~ c2_2(a1442,X105)
| c4_2(a1442,X105) ) ).
cnf(u3226,negated_conjecture,
c1_1(a1438) ).
cnf(u3230,negated_conjecture,
~ ndr1_1(a1438) ).
cnf(u3255,negated_conjecture,
ndr1_1(a1436) ).
cnf(u3241,negated_conjecture,
( c3_2(a1436,X103)
| c5_2(a1436,X103)
| ~ c2_2(a1436,X103) ) ).
cnf(u3245,negated_conjecture,
c1_2(a1436,a1437) ).
cnf(u3249,negated_conjecture,
~ c2_2(a1436,a1437) ).
cnf(u3253,negated_conjecture,
~ c4_2(a1436,a1437) ).
cnf(u3259,negated_conjecture,
( ~ c2_2(a1436,X102)
| c4_2(a1436,X102)
| c1_2(a1436,X102) ) ).
cnf(u3278,negated_conjecture,
( ~ c5_1(X62)
| ~ c1_1(X62)
| ~ c5_2(X62,X63)
| ~ ndr1_1(X62)
| c3_2(X62,X63)
| ~ c2_2(X62,X63) ) ).
cnf(u3336,negated_conjecture,
( c2_2(X47,a1373)
| c1_1(X47)
| ~ c5_2(X47,a1374) ) ).
cnf(u3340,negated_conjecture,
( c2_2(X47,a1373)
| c1_1(X47)
| c4_2(X47,a1374) ) ).
cnf(u3344,negated_conjecture,
( c2_2(X47,a1373)
| c1_1(X47)
| ~ c1_2(X47,a1374) ) ).
cnf(u3348,negated_conjecture,
( ~ c5_2(X47,a1374)
| c1_1(X47)
| c3_2(X47,a1373) ) ).
cnf(u3352,negated_conjecture,
( c3_2(X47,a1373)
| c1_1(X47)
| c4_2(X47,a1374) ) ).
cnf(u3356,negated_conjecture,
( c3_2(X47,a1373)
| c1_1(X47)
| ~ c1_2(X47,a1374) ) ).
cnf(u3360,negated_conjecture,
( ~ c5_2(X47,a1374)
| c1_1(X47)
| ~ c1_2(X47,a1373) ) ).
cnf(u3364,negated_conjecture,
( ~ c1_2(X47,a1373)
| c1_1(X47)
| c4_2(X47,a1374) ) ).
cnf(u3368,negated_conjecture,
( ~ c1_2(X47,a1374)
| c1_1(X47)
| ~ c1_2(X47,a1373) ) ).
cnf(u3374,negated_conjecture,
~ c2_1(a1363) ).
cnf(u3378,negated_conjecture,
c1_2(a1363,a1364) ).
cnf(u3382,negated_conjecture,
c5_2(a1363,a1364) ).
cnf(u3386,negated_conjecture,
~ c2_2(a1363,a1364) ).
cnf(u3390,negated_conjecture,
ndr1_1(a1363) ).
cnf(u3395,negated_conjecture,
( ~ c3_2(a1363,X34)
| c2_2(a1363,X34) ) ).
cnf(u3403,negated_conjecture,
( ~ c5_1(X19)
| ~ c4_1(X19)
| c3_1(X19) ) ).
cnf(u3419,negated_conjecture,
( ~ c4_2(X12,a1341)
| c2_1(X12)
| ~ c2_2(X12,a1340) ) ).
cnf(u3423,negated_conjecture,
( ~ c2_2(X12,a1340)
| c5_2(X12,a1341)
| c2_1(X12) ) ).
cnf(u3427,negated_conjecture,
( ~ c4_2(X12,a1341)
| c2_1(X12)
| ~ c4_2(X12,a1340) ) ).
cnf(u3431,negated_conjecture,
( ~ c4_2(X12,a1340)
| c5_2(X12,a1341)
| c2_1(X12) ) ).
cnf(u3435,negated_conjecture,
( c2_1(X12)
| ndr1_1(X12) ) ).
cnf(u3439,negated_conjecture,
~ c4_1(a1337) ).
cnf(u3444,negated_conjecture,
~ c5_1(a1337) ).
cnf(u3466,negated_conjecture,
( ~ c1_2(a1516,X1)
| ~ c4_2(a1516,X1)
| ~ c2_2(a1516,X1) ) ).
cnf(u3477,negated_conjecture,
( ~ c1_2(a1350,X1)
| ~ c4_2(a1350,X1)
| ~ c2_2(a1350,X1) ) ).
cnf(u3489,negated_conjecture,
c2_1(a1424) ).
cnf(u3492,negated_conjecture,
c5_2(a1424,a1410) ).
cnf(u6405,negated_conjecture,
~ c3_1(a1464) ).
cnf(u3513,negated_conjecture,
c2_1(a1475) ).
cnf(u5132,negated_conjecture,
c1_1(a1475) ).
cnf(u3526,negated_conjecture,
~ c4_2(a1524,a1373) ).
cnf(u3532,negated_conjecture,
c1_1(a1524) ).
cnf(u3542,negated_conjecture,
c2_2(a1363,a1379) ).
cnf(u3559,negated_conjecture,
( ~ c5_2(a1439,X0)
| ~ c4_2(a1439,X0)
| c2_2(a1439,X0) ) ).
cnf(u3567,negated_conjecture,
~ c4_1(a1439) ).
cnf(u3566,negated_conjecture,
( ~ c4_2(a1439,X0)
| ~ c3_2(a1439,X0) ) ).
cnf(u3571,negated_conjecture,
( ~ c1_2(a1439,X0)
| ~ c5_2(a1439,X0)
| ~ c2_2(a1439,X0) ) ).
cnf(u3574,negated_conjecture,
c2_2(a1439,a1505) ).
cnf(u3588,negated_conjecture,
c3_1(a1350) ).
cnf(u3591,negated_conjecture,
~ c4_1(a1350) ).
cnf(u3595,negated_conjecture,
c3_1(a1516) ).
cnf(u3598,negated_conjecture,
~ c4_1(a1516) ).
cnf(u3617,negated_conjecture,
~ c4_2(a1524,a1410) ).
cnf(u3620,negated_conjecture,
c2_1(a1524) ).
cnf(u3854,negated_conjecture,
c4_1(a1524) ).
cnf(u3639,negated_conjecture,
~ c4_1(a1464) ).
cnf(u3665,negated_conjecture,
c1_1(a1436) ).
cnf(u3668,negated_conjecture,
~ c2_2(a1436,a1459) ).
cnf(u3686,negated_conjecture,
~ c4_2(a1524,a1379) ).
cnf(u4906,negated_conjecture,
~ c3_1(a1436) ).
cnf(u4622,negated_conjecture,
~ c4_2(a1436,a1433) ).
cnf(u5030,negated_conjecture,
~ c3_1(a1428) ).
cnf(u3751,negated_conjecture,
c5_2(a1363,a1340) ).
cnf(u3765,negated_conjecture,
( ~ c4_2(a1430,X0)
| ~ c3_2(a1430,X0) ) ).
cnf(u3773,negated_conjecture,
c4_1(a1430) ).
cnf(u3788,negated_conjecture,
c2_2(a1430,a1505) ).
cnf(u3792,negated_conjecture,
( c3_2(a1430,X1)
| ~ c2_2(a1430,X1)
| c1_2(a1430,X1) ) ).
cnf(u3809,negated_conjecture,
~ c4_1(a1428) ).
cnf(u3813,negated_conjecture,
( c2_2(a1428,X0)
| ~ c4_2(a1428,X0)
| ~ c5_2(a1428,X0) ) ).
cnf(u3826,negated_conjecture,
( c3_2(a1428,X0)
| ~ c4_2(a1428,X0)
| c5_2(a1428,X0) ) ).
cnf(u3833,negated_conjecture,
( ~ c5_2(a1428,X0)
| c4_2(a1428,X0) ) ).
cnf(u3844,negated_conjecture,
c2_2(a1428,a1505) ).
cnf(u3850,negated_conjecture,
~ c4_2(a1524,a1489) ).
cnf(u3862,negated_conjecture,
~ c3_1(a1438) ).
cnf(u3878,negated_conjecture,
c3_2(a1428,a1505) ).
cnf(u3884,negated_conjecture,
( c3_2(a1346,X0)
| ~ c2_2(a1346,X0)
| ~ c5_2(a1346,X0) ) ).
cnf(u3907,negated_conjecture,
c1_1(a1516) ).
cnf(u3910,negated_conjecture,
( c3_2(a1516,X0)
| c4_2(a1516,X0)
| ~ c2_2(a1516,X0) ) ).
cnf(u3914,negated_conjecture,
c1_1(a1464) ).
cnf(u3921,negated_conjecture,
c1_1(a1350) ).
cnf(u3940,negated_conjecture,
~ c3_1(a1333) ).
cnf(u3943,negated_conjecture,
~ c2_1(a1333) ).
cnf(u3951,negated_conjecture,
( ~ c1_2(a1333,X1)
| ~ c4_2(a1333,X1)
| c2_2(a1333,X1) ) ).
cnf(u3964,negated_conjecture,
c4_2(a1430,a1374) ).
cnf(u5269,negated_conjecture,
~ c1_1(a1430) ).
cnf(u3970,negated_conjecture,
c4_2(a1430,a1373) ).
cnf(u3978,negated_conjecture,
~ c3_1(a1524) ).
cnf(u3991,negated_conjecture,
( c2_2(a1524,X0)
| c5_2(a1524,X0)
| ~ c4_2(a1524,X0) ) ).
cnf(u4005,negated_conjecture,
~ c2_2(a1464,a1433) ).
cnf(u4013,negated_conjecture,
~ c4_1(a1363) ).
cnf(u5003,negated_conjecture,
~ c3_1(a1363) ).
cnf(u4042,negated_conjecture,
~ c3_1(a1494) ).
cnf(u4030,negated_conjecture,
~ c4_1(a1494) ).
cnf(u4034,negated_conjecture,
c1_1(a1494) ).
cnf(u4061,negated_conjecture,
( ~ c1_2(a1363,X0)
| ~ c5_2(a1363,X0)
| ~ c2_2(a1363,X0) ) ).
cnf(u4064,negated_conjecture,
c2_2(a1363,a1505) ).
cnf(u4068,negated_conjecture,
c3_2(a1363,a1505) ).
cnf(u4075,negated_conjecture,
c2_2(a1363,a1435) ).
cnf(u4079,negated_conjecture,
( ~ c3_2(a1363,X0)
| c4_2(a1363,X0) ) ).
cnf(u4082,negated_conjecture,
c1_1(a1363) ).
cnf(u4092,negated_conjecture,
c3_2(a1363,a1489) ).
cnf(u4139,negated_conjecture,
( ~ c1_2(a1464,X0)
| ~ c5_2(a1464,X0)
| ~ c2_2(a1464,X0) ) ).
cnf(u4150,negated_conjecture,
( c3_2(a1464,X1)
| ~ c2_2(a1464,X1)
| c1_2(a1464,X1) ) ).
cnf(u4160,negated_conjecture,
c3_2(a1464,a1489) ).
cnf(u4170,negated_conjecture,
c5_2(a1439,a1440) ).
cnf(u4173,negated_conjecture,
c2_2(a1439,a1379) ).
cnf(u6619,negated_conjecture,
~ c2_1(a1439) ).
cnf(u4188,negated_conjecture,
( ~ c4_2(a1436,X0)
| ~ c3_2(a1436,X0) ) ).
cnf(u4196,negated_conjecture,
c4_1(a1436) ).
cnf(u4203,negated_conjecture,
( c1_2(a1436,X0)
| c4_2(a1436,X0) ) ).
cnf(u4208,negated_conjecture,
c2_1(a1436) ).
cnf(u4211,negated_conjecture,
( c3_2(a1436,X0)
| ~ c4_2(a1436,X0)
| c5_2(a1436,X0) ) ).
cnf(u4225,negated_conjecture,
( ~ c1_2(a1436,X0)
| ~ c5_2(a1436,X0)
| ~ c2_2(a1436,X0) ) ).
cnf(u4239,negated_conjecture,
c4_2(a1363,a1358) ).
cnf(u4274,negated_conjecture,
( c2_2(a1452,X0)
| ~ c4_2(a1452,X0)
| ~ c5_2(a1452,X0) ) ).
cnf(u4514,negated_conjecture,
~ c4_1(a1452) ).
cnf(u4287,negated_conjecture,
~ c2_1(a1452) ).
cnf(u4295,negated_conjecture,
c2_2(a1452,a1435) ).
cnf(u4302,negated_conjecture,
c3_2(a1452,a1489) ).
cnf(u4309,negated_conjecture,
c2_2(a1452,a1505) ).
cnf(u4313,negated_conjecture,
c3_2(a1452,a1505) ).
cnf(u4327,negated_conjecture,
c1_1(a1452) ).
cnf(u4330,negated_conjecture,
c4_2(a1452,a1373) ).
cnf(u4354,negated_conjecture,
c5_2(a1363,a1373) ).
cnf(u4368,negated_conjecture,
( c2_2(a1333,X0)
| ~ c4_2(a1333,X0)
| ~ c5_2(a1333,X0) ) ).
cnf(u7131,negated_conjecture,
~ c4_1(a1333) ).
cnf(u4383,negated_conjecture,
( c3_2(a1333,X0)
| ~ c4_2(a1333,X0)
| c5_2(a1333,X0) ) ).
cnf(u4390,negated_conjecture,
( ~ c5_2(a1333,X0)
| c4_2(a1333,X0) ) ).
cnf(u4400,negated_conjecture,
c2_2(a1333,a1505) ).
cnf(u4404,negated_conjecture,
c3_2(a1333,a1505) ).
cnf(u4419,negated_conjecture,
~ c1_2(a1428,a1340) ).
cnf(u4430,negated_conjecture,
c2_1(a1337) ).
cnf(u4443,negated_conjecture,
~ c4_2(a1464,a1433) ).
cnf(u4456,negated_conjecture,
( ~ c1_2(a1464,X1)
| ~ c4_2(a1464,X1)
| c2_2(a1464,X1) ) ).
cnf(u4482,negated_conjecture,
c3_2(a1430,a1505) ).
cnf(u4493,negated_conjecture,
c1_1(a1482) ).
cnf(u4537,negated_conjecture,
( c3_2(a1524,X0)
| ~ c4_2(a1524,X0)
| c5_2(a1524,X0) ) ).
cnf(u4551,negated_conjecture,
c2_2(a1524,a1505) ).
cnf(u4555,negated_conjecture,
c3_2(a1524,a1505) ).
cnf(u4560,negated_conjecture,
( c3_2(a1524,X1)
| ~ c2_2(a1524,X1)
| c1_2(a1524,X1) ) ).
cnf(u4587,negated_conjecture,
~ c2_2(a1430,a1433) ).
cnf(u4595,negated_conjecture,
~ c2_2(a1430,a1459) ).
cnf(u4951,negated_conjecture,
~ c4_2(a1428,a1433) ).
cnf(u4608,negated_conjecture,
c1_2(a1428,a1358) ).
cnf(u4611,negated_conjecture,
c1_1(a1428) ).
cnf(u4615,negated_conjecture,
~ c2_2(a1436,a1433) ).
cnf(u4631,negated_conjecture,
~ c4_2(a1333,a1433) ).
cnf(u4638,negated_conjecture,
~ c4_2(a1524,a1433) ).
cnf(u4665,negated_conjecture,
~ c2_2(a1524,a1433) ).
cnf(u4681,negated_conjecture,
c1_1(a1439) ).
cnf(u4684,negated_conjecture,
~ c2_2(a1439,a1441) ).
cnf(u4730,negated_conjecture,
c4_2(a1452,a1459) ).
cnf(u4737,negated_conjecture,
c4_2(a1430,a1459) ).
cnf(u4825,negated_conjecture,
c1_1(a1503) ).
cnf(u4891,negated_conjecture,
( ~ c1_2(a1452,X1)
| ~ c4_2(a1452,X1)
| c2_2(a1452,X1) ) ).
cnf(u4913,negated_conjecture,
( ~ c4_2(a1436,X0)
| c5_2(a1436,X0)
| c2_2(a1436,X0) ) ).
cnf(u4939,negated_conjecture,
c1_1(a1446) ).
cnf(u5008,negated_conjecture,
( c2_2(a1363,X1)
| ~ c1_2(a1363,X1)
| ~ c4_2(a1363,X1) ) ).
cnf(u5048,negated_conjecture,
c1_1(a1498) ).
cnf(u5055,negated_conjecture,
~ c3_1(a1498) ).
cnf(u5083,negated_conjecture,
c3_2(a1439,a1489) ).
cnf(u5089,negated_conjecture,
~ c2_2(a1439,a1489) ).
cnf(u5138,negated_conjecture,
( c1_2(a1475,X0)
| c4_2(a1475,X0) ) ).
cnf(u5142,negated_conjecture,
c1_1(a1458) ).
cnf(u5152,negated_conjecture,
c1_1(a1454) ).
cnf(u5162,negated_conjecture,
c1_1(a1442) ).
cnf(u5168,negated_conjecture,
( c1_2(a1442,X0)
| c4_2(a1442,X0) ) ).
cnf(u5186,negated_conjecture,
( c1_2(a1346,X0)
| c4_2(a1346,X0) ) ).
cnf(u5190,negated_conjecture,
( c3_2(a1337,X1)
| ~ c2_2(a1337,X1)
| c1_2(a1337,X1) ) ).
cnf(u5214,negated_conjecture,
c4_2(a1442,a1374) ).
cnf(u5224,negated_conjecture,
( ~ c5_2(a1442,X0)
| c4_2(a1442,X0)
| ~ c2_2(a1442,X0) ) ).
cnf(u5472,negated_conjecture,
~ c4_2(a1363,a1396) ).
cnf(u5282,negated_conjecture,
~ c2_2(a1524,a1396) ).
cnf(u5289,negated_conjecture,
~ c2_2(a1464,a1396) ).
cnf(u5296,negated_conjecture,
~ c2_2(a1452,a1396) ).
cnf(u5300,negated_conjecture,
~ c2_2(a1436,a1396) ).
cnf(u5304,negated_conjecture,
~ c2_2(a1428,a1396) ).
cnf(u5312,negated_conjecture,
~ c2_2(a1333,a1396) ).
cnf(u5316,negated_conjecture,
~ c2_2(a1363,a1396) ).
cnf(u5336,negated_conjecture,
c1_2(a1524,a1396) ).
cnf(u5340,negated_conjecture,
c1_2(a1464,a1396) ).
cnf(u5344,negated_conjecture,
c1_2(a1452,a1396) ).
cnf(u5348,negated_conjecture,
c1_2(a1436,a1396) ).
cnf(u5357,negated_conjecture,
c1_2(a1333,a1396) ).
cnf(u5361,negated_conjecture,
c1_2(a1363,a1396) ).
cnf(u5373,negated_conjecture,
~ c3_2(a1333,a1396) ).
cnf(u5392,negated_conjecture,
~ c5_2(a1442,a1374) ).
cnf(u5412,negated_conjecture,
c4_2(a1475,a1374) ).
cnf(u5670,negated_conjecture,
~ c2_2(a1475,a1505) ).
cnf(u5422,negated_conjecture,
( ~ c5_2(a1475,X0)
| c4_2(a1475,X0)
| ~ c2_2(a1475,X0) ) ).
cnf(u5426,negated_conjecture,
c3_2(a1475,a1505) ).
cnf(u5475,negated_conjecture,
~ c5_2(a1363,a1396) ).
cnf(u5507,negated_conjecture,
~ c2_2(a1442,a1357) ).
cnf(u5526,negated_conjecture,
c4_2(a1337,a1459) ).
cnf(u5540,negated_conjecture,
~ c2_2(a1337,a1433) ).
cnf(u5548,negated_conjecture,
~ c2_2(a1337,a1459) ).
cnf(u5555,negated_conjecture,
~ c5_2(a1337,a1459) ).
cnf(u5586,negated_conjecture,
c4_2(a1346,a1374) ).
cnf(u5596,negated_conjecture,
( ~ c5_2(a1346,X0)
| c4_2(a1346,X0)
| ~ c2_2(a1346,X0) ) ).
cnf(u5607,negated_conjecture,
c4_2(a1346,a1489) ).
cnf(u5616,negated_conjecture,
~ c5_2(a1346,a1374) ).
cnf(u5625,negated_conjecture,
~ c5_2(a1346,a1489) ).
cnf(u5640,negated_conjecture,
~ ndr1_1(a1454) ).
cnf(u5657,negated_conjecture,
~ c4_2(a1452,a1396) ).
cnf(u5675,negated_conjecture,
~ c4_2(a1524,a1396) ).
cnf(u5686,negated_conjecture,
( ~ c1_2(a1516,X1)
| ~ c4_2(a1516,X1)
| c2_2(a1516,X1) ) ).
cnf(u5695,negated_conjecture,
( c3_2(a1516,X0)
| ~ c2_2(a1516,X0)
| ~ c5_2(a1516,X0) ) ).
cnf(u5705,negated_conjecture,
~ c2_2(a1516,a1433) ).
cnf(u5771,negated_conjecture,
~ c4_2(a1516,a1433) ).
cnf(u5712,negated_conjecture,
c4_2(a1516,a1459) ).
cnf(u7610,negated_conjecture,
~ c2_2(a1516,a1459) ).
cnf(u5725,negated_conjecture,
~ c5_2(a1516,a1459) ).
cnf(u5744,negated_conjecture,
c2_2(a1516,a1505) ).
cnf(u5748,negated_conjecture,
c3_2(a1516,a1505) ).
cnf(u5752,negated_conjecture,
( c3_2(a1516,X0)
| ~ c4_2(a1516,X0)
| c5_2(a1516,X0) ) ).
cnf(u5762,negated_conjecture,
c3_2(a1516,a1489) ).
cnf(u5794,negated_conjecture,
~ c2_2(a1516,a1396) ).
cnf(u5803,negated_conjecture,
~ c3_2(a1516,a1414) ).
cnf(u5830,negated_conjecture,
~ c2_2(a1516,a1414) ).
cnf(u5838,negated_conjecture,
~ c4_2(a1516,a1414) ).
cnf(u5844,negated_conjecture,
c2_2(a1516,a1379) ).
cnf(u5866,negated_conjecture,
~ c2_2(a1346,a1357) ).
cnf(u5886,negated_conjecture,
~ c5_2(a1346,a1459) ).
cnf(u5910,negated_conjecture,
( ~ c1_2(a1516,X0)
| ~ c4_2(a1516,X0)
| c5_2(a1516,X0) ) ).
cnf(u5920,negated_conjecture,
( ~ c1_2(a1430,X0)
| ~ c4_2(a1430,X0)
| c5_2(a1430,X0) ) ).
cnf(u5930,negated_conjecture,
( ~ c4_2(a1464,X0)
| ~ c1_2(a1464,X0)
| c5_2(a1464,X0) ) ).
cnf(u5944,negated_conjecture,
( ~ c4_2(a1436,X0)
| ~ c1_2(a1436,X0)
| c5_2(a1436,X0) ) ).
cnf(u5951,negated_conjecture,
( ~ c1_2(a1363,X0)
| ~ c4_2(a1363,X0)
| c5_2(a1363,X0) ) ).
cnf(u5958,negated_conjecture,
( ~ c1_2(a1333,X0)
| ~ c4_2(a1333,X0)
| c5_2(a1333,X0) ) ).
cnf(u5968,negated_conjecture,
c5_2(a1524,a1413) ).
cnf(u5991,negated_conjecture,
~ c2_2(a1452,a1413) ).
cnf(u5996,negated_conjecture,
~ c2_2(a1524,a1413) ).
cnf(u6010,negated_conjecture,
c4_2(a1452,a1413) ).
cnf(u6015,negated_conjecture,
c4_2(a1524,a1413) ).
cnf(u6031,negated_conjecture,
c3_1(a1510) ).
cnf(u6034,negated_conjecture,
~ c4_1(a1510) ).
cnf(u6055,negated_conjecture,
~ c1_1(a1510) ).
cnf(u6047,negated_conjecture,
~ c2_1(a1510) ).
cnf(u6128,negated_conjecture,
( ~ c1_2(a1510,X0)
| ~ c5_2(a1510,X0)
| ~ c2_2(a1510,X0) ) ).
cnf(u6131,negated_conjecture,
c2_2(a1510,a1505) ).
cnf(u6135,negated_conjecture,
c3_2(a1510,a1505) ).
cnf(u6142,negated_conjecture,
c2_2(a1510,a1435) ).
cnf(u6149,negated_conjecture,
c3_2(a1510,a1489) ).
cnf(u6160,negated_conjecture,
c4_2(a1510,a1358) ).
cnf(u6174,negated_conjecture,
c1_1(a1495) ).
cnf(u6177,negated_conjecture,
( c3_2(a1495,X1)
| ~ c2_2(a1495,X1)
| c1_2(a1495,X1) ) ).
cnf(u6198,negated_conjecture,
c4_1(a1495) ).
cnf(u6205,negated_conjecture,
c3_1(a1495) ).
cnf(u6219,negated_conjecture,
( ~ c5_2(a1495,X0)
| c4_2(a1495,X0) ) ).
cnf(u6229,negated_conjecture,
( ~ c4_2(a1495,X0)
| ~ c3_2(a1495,X0) ) ).
cnf(u6243,negated_conjecture,
c2_2(a1495,a1505) ).
cnf(u6247,negated_conjecture,
c3_2(a1495,a1505) ).
cnf(u6266,negated_conjecture,
c2_2(a1510,a1379) ).
cnf(u6269,negated_conjecture,
c4_2(a1510,a1505) ).
cnf(u6287,negated_conjecture,
~ c2_2(a1510,a1489) ).
cnf(u6318,negated_conjecture,
~ c2_2(a1510,a1357) ).
cnf(u6325,negated_conjecture,
~ c5_2(a1510,a1358) ).
cnf(u6339,negated_conjecture,
c4_2(a1510,a1374) ).
cnf(u6345,negated_conjecture,
~ c5_2(a1510,a1459) ).
cnf(u6357,negated_conjecture,
~ c4_2(a1430,a1358) ).
cnf(u6393,negated_conjecture,
( ~ c4_2(a1495,X1)
| ~ c1_2(a1495,X1)
| c2_2(a1495,X1) ) ).
cnf(u6487,negated_conjecture,
( ~ c1_2(a1350,X1)
| ~ c4_2(a1350,X1)
| c2_2(a1350,X1) ) ).
cnf(u6501,negated_conjecture,
~ c2_2(a1350,a1433) ).
cnf(u6525,negated_conjecture,
~ c2_2(a1350,a1413) ).
cnf(u6538,negated_conjecture,
c2_2(a1350,a1505) ).
cnf(u6542,negated_conjecture,
c3_2(a1350,a1505) ).
cnf(u6549,negated_conjecture,
c1_2(a1350,a1396) ).
cnf(u6553,negated_conjecture,
~ c2_2(a1350,a1396) ).
cnf(u6557,negated_conjecture,
( c3_2(a1350,X0)
| ~ c4_2(a1350,X0)
| c5_2(a1350,X0) ) ).
cnf(u6564,negated_conjecture,
( ~ c5_2(a1350,X0)
| c4_2(a1350,X0) ) ).
cnf(u6575,negated_conjecture,
~ c4_2(a1350,a1433) ).
cnf(u6632,negated_conjecture,
( ~ c4_2(a1439,X0)
| c3_2(a1439,X0)
| c5_2(a1439,X0) ) ).
cnf(u6654,negated_conjecture,
~ c2_2(a1439,a1357) ).
cnf(u6661,negated_conjecture,
~ c5_2(a1439,a1358) ).
cnf(u6672,negated_conjecture,
c3_2(a1439,a1459) ).
cnf(u6681,negated_conjecture,
~ c2_2(a1439,a1459) ).
cnf(u6827,negated_conjecture,
~ c3_2(a1333,a1526) ).
cnf(u6832,negated_conjecture,
~ c4_2(a1333,a1526) ).
cnf(u6839,negated_conjecture,
~ c4_2(a1516,a1526) ).
cnf(u6848,negated_conjecture,
~ c4_2(a1363,a1526) ).
cnf(u6894,negated_conjecture,
c2_2(a1346,a1395) ).
cnf(u6901,negated_conjecture,
c2_2(a1516,a1395) ).
cnf(u6905,negated_conjecture,
( c3_2(a1510,X0)
| c5_2(a1510,X0) ) ).
cnf(u6908,negated_conjecture,
c2_2(a1510,a1395) ).
cnf(u6915,negated_conjecture,
c2_2(a1495,a1395) ).
cnf(u6919,negated_conjecture,
( c3_2(a1439,X0)
| c5_2(a1439,X0) ) ).
cnf(u6980,negated_conjecture,
( ~ c2_2(a1510,X0)
| c5_2(a1510,X0)
| c4_2(a1510,X0) ) ).
cnf(u7004,negated_conjecture,
~ c5_2(a1346,a1433) ).
cnf(u7054,negated_conjecture,
c3_2(a1346,a1395) ).
cnf(u7058,negated_conjecture,
c3_2(a1516,a1395) ).
cnf(u7066,negated_conjecture,
c3_2(a1495,a1395) ).
cnf(u7104,negated_conjecture,
( ~ c4_2(a1439,X0)
| c5_2(a1439,X0)
| c2_2(a1439,X0) ) ).
cnf(u7112,negated_conjecture,
~ c2_2(a1439,a1413) ).
cnf(u7116,negated_conjecture,
c5_2(a1439,a1433) ).
cnf(u7143,negated_conjecture,
~ c2_2(a1436,a1324) ).
cnf(u7165,negated_conjecture,
~ c4_2(a1464,a1526) ).
cnf(u7175,negated_conjecture,
~ c4_2(a1452,a1526) ).
cnf(u7191,negated_conjecture,
c4_2(a1510,a1395) ).
cnf(u7222,negated_conjecture,
c4_2(a1510,a1435) ).
cnf(u7236,negated_conjecture,
c5_2(a1510,a1379) ).
cnf(u7240,negated_conjecture,
c5_2(a1510,a1373) ).
cnf(u7244,negated_conjecture,
~ c5_2(a1510,a1374) ).
cnf(u7248,negated_conjecture,
~ c1_2(a1510,a1374) ).
cnf(u7300,negated_conjecture,
c4_2(a1346,a1395) ).
cnf(u7384,negated_conjecture,
~ c5_2(a1504,a1459) ).
cnf(u7342,negated_conjecture,
~ c3_2(a1504,a1459) ).
cnf(u7348,negated_conjecture,
c4_2(a1504,a1459) ).
cnf(u7351,negated_conjecture,
c2_2(a1504,a1379) ).
cnf(u7360,negated_conjecture,
c2_2(a1504,a1435) ).
cnf(u7400,negated_conjecture,
c4_1(a1493) ).
cnf(u7403,negated_conjecture,
~ c1_1(a1493) ).
cnf(u7413,negated_conjecture,
c4_2(a1493,a1459) ).
cnf(u7434,negated_conjecture,
( ~ c4_2(a1493,X0)
| ~ c1_2(a1493,X0)
| c5_2(a1493,X0) ) ).
cnf(u7446,negated_conjecture,
c1_2(a1493,a1340) ).
cnf(u7461,negated_conjecture,
~ c5_2(a1493,a1340) ).
cnf(u7480,negated_conjecture,
~ c5_2(a1493,a1459) ).
cnf(u7511,negated_conjecture,
( ~ c1_2(a1493,X0)
| ~ c5_2(a1493,X0)
| ~ c2_2(a1493,X0) ) ).
cnf(u7519,negated_conjecture,
c2_2(a1493,a1435) ).
cnf(u7537,negated_conjecture,
~ c4_2(a1493,a1433) ).
cnf(u7602,negated_conjecture,
~ c5_2(a1493,a1358) ).
cnf(u7655,negated_conjecture,
~ c5_2(a1443,a1444) ).
cnf(u7661,negated_conjecture,
~ c2_2(a1443,a1444) ).
cnf(u7804,negated_conjecture,
~ c2_2(a1350,a1414) ).
cnf(u7807,negated_conjecture,
~ c5_2(a1350,a1414) ).
cnf(u7815,negated_conjecture,
c4_2(a1350,a1414) ).
cnf(u7818,negated_conjecture,
c2_2(a1350,a1379) ).
cnf(u7824,negated_conjecture,
~ c4_2(a1516,a1396) ).
cnf(u7840,negated_conjecture,
~ c1_2(a1350,a1414) ).
cnf(u7856,negated_conjecture,
( c3_2(a1350,X0)
| c5_2(a1350,X0) ) ).
cnf(u7879,negated_conjecture,
~ c2_2(a1475,a1357) ).
cnf(u7896,negated_conjecture,
~ c3_1(a1490) ).
cnf(u8038,negated_conjecture,
~ c3_1(a1458) ).
cnf(u8065,negated_conjecture,
~ c2_2(a1428,a1413) ).
cnf(u8086,negated_conjecture,
~ c2_2(a1475,a1324) ).
cnf(u8106,negated_conjecture,
c2_2(a1424,a1395) ).
cnf(u8118,negated_conjecture,
c4_2(a1424,a1374) ).
cnf(u8127,negated_conjecture,
c3_2(a1424,a1459) ).
cnf(u8137,negated_conjecture,
( ~ c3_2(a1424,X0)
| ~ c2_2(a1424,X0)
| c4_2(a1424,X0) ) ).
cnf(u8176,negated_conjecture,
~ c2_2(a1424,a1459) ).
cnf(u8210,negated_conjecture,
~ c1_2(a1424,a1374) ).
cnf(u8214,negated_conjecture,
c5_2(a1424,a1357) ).
cnf(u8221,negated_conjecture,
c1_2(a1424,a1357) ).
cnf(u8240,negated_conjecture,
~ c2_2(a1424,a1357) ).
cnf(u8308,negated_conjecture,
c4_2(a1325,a1373) ).
cnf(u8315,negated_conjecture,
( ~ c5_2(a1325,X0)
| c4_2(a1325,X0)
| ~ c2_2(a1325,X0) ) ).
cnf(u8342,negated_conjecture,
~ c2_2(a1424,a1324) ).
cnf(u8362,negated_conjecture,
~ c5_2(a1325,a1373) ).
cnf(u8379,negated_conjecture,
~ c2_2(a1325,a1357) ).
cnf(u8416,negated_conjecture,
~ c3_1(a1434) ).
cnf(u8433,negated_conjecture,
c4_2(a1442,a1489) ).
cnf(u8438,negated_conjecture,
( c3_2(a1442,X0)
| c5_2(a1442,X0) ) ).
cnf(u8482,negated_conjecture,
~ c1_2(a1442,a1374) ).
cnf(u8704,negated_conjecture,
~ c2_2(a1430,a1373) ).
cnf(u8226,negated_conjecture,
c3_2(a1424,a1374) ).
cnf(u3506,negated_conjecture,
( ~ c5_2(X50,a1379)
| c2_1(X50)
| c3_2(X50,X51)
| c5_2(X50,X51)
| c4_2(X50,X51) ) ).
cnf(u3872,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c2_2(X0,X1)
| c3_2(X0,a1505)
| ~ c5_2(X0,X1)
| c1_1(X0) ) ).
cnf(u3505,negated_conjecture,
( c3_2(X50,X51)
| c2_1(X50)
| c2_2(X50,a1379)
| c5_2(X50,X51)
| c4_2(X50,X51) ) ).
cnf(u5519,negated_conjecture,
~ c5_2(a1428,a1396) ).
cnf(u8680,negated_conjecture,
( ~ c2_2(X0,a1489)
| c4_1(X0)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,a1358)
| c4_2(X0,a1489)
| c4_2(X0,a1357) ) ).
cnf(u5370,negated_conjecture,
~ c4_2(a1333,a1396) ).
cnf(u3550,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c2_2(X0,X1)
| c2_2(X0,a1505)
| ~ c5_2(X0,X1)
| c1_1(X0) ) ).
cnf(u6517,negated_conjecture,
( ~ c4_2(a1350,X0)
| c2_2(a1350,X0)
| ~ c5_2(a1350,X0) ) ).
cnf(u4744,negated_conjecture,
( c1_2(X0,a1357)
| c4_2(X0,a1459)
| c4_2(X0,a1358)
| c1_1(X0) ) ).
cnf(u87,axiom,
( ~ sP24(X0)
| c3_2(X0,a1330) ) ).
cnf(u5979,negated_conjecture,
( ~ c2_2(X0,a1413)
| ~ c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_2(X0,X1)
| c3_1(X0)
| c1_1(X0) ) ).
cnf(u7967,negated_conjecture,
( ~ c5_2(X0,a1374)
| c2_1(X0)
| c1_1(X0)
| c4_2(X0,a1373)
| c2_2(X0,a1435)
| c5_2(X0,a1459) ) ).
cnf(u8716,negated_conjecture,
~ c2_2(a1430,a1374) ).
cnf(u8707,negated_conjecture,
~ c3_2(a1430,a1374) ).
cnf(u6876,negated_conjecture,
~ c5_2(a1428,a1526) ).
cnf(u7526,negated_conjecture,
c5_2(a1493,a1410) ).
cnf(u4859,negated_conjecture,
( c3_2(X0,a1505)
| ~ c2_2(X0,a1357)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,a1358) ) ).
cnf(u540,negated_conjecture,
~ c5_0 ).
cnf(u4723,negated_conjecture,
( ~ c2_2(X0,X1)
| c4_2(X0,a1459)
| c4_2(X0,X1)
| c1_1(X0)
| c2_1(X0)
| c2_2(X0,a1379)
| c5_2(X0,X1) ) ).
cnf(u290,axiom,
( ~ sP1(X0)
| ndr1_1(X0) ) ).
cnf(u502,negated_conjecture,
c2_1(a1464) ).
cnf(u3448,negated_conjecture,
c5_2(a1333,a1334) ).
cnf(u4983,negated_conjecture,
( ~ c5_2(X0,a1459)
| c2_2(X0,a1459)
| c4_1(X0)
| c1_1(X0)
| c4_2(X0,a1373)
| c4_2(X0,a1374) ) ).
cnf(u8698,negated_conjecture,
~ c1_2(a1430,a1374) ).
cnf(u8591,negated_conjecture,
~ c3_2(a1430,a1459) ).
cnf(u288,axiom,
( ~ sP1(X0)
| ~ c1_2(X0,a1513) ) ).
cnf(u3601,negated_conjecture,
( c3_2(X0,X1)
| c2_2(X0,a1435)
| c5_2(X0,X1)
| ~ c4_2(X0,X1)
| c2_1(X0)
| c1_1(X0) ) ).
cnf(u8068,negated_conjecture,
~ c1_2(a1428,a1413) ).
cnf(u6112,negated_conjecture,
( ~ c4_2(a1510,X0)
| c2_2(a1510,X0)
| ~ c5_2(a1510,X0) ) ).
cnf(u5077,negated_conjecture,
( c3_2(X0,a1489)
| c4_2(X0,a1357)
| c4_1(X0)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,a1358) ) ).
cnf(u3630,negated_conjecture,
( ~ c5_2(X0,X1)
| c3_2(X0,a1489)
| c4_2(X0,X1)
| c4_1(X0)
| c1_1(X0) ) ).
cnf(u4678,negated_conjecture,
( c2_2(X0,a1505)
| ~ c5_2(X0,a1358)
| c1_1(X0)
| c1_2(X0,a1357) ) ).
cnf(u4742,negated_conjecture,
( ~ c1_2(X0,a1374)
| c4_2(X0,a1459)
| c4_2(X0,a1373)
| c1_1(X0) ) ).
cnf(u505,negated_conjecture,
~ c5_2(a1464,a1465) ).
cnf(u7388,negated_conjecture,
ndr1_1(a1493) ).
cnf(u1711,negated_conjecture,
c3_1(a1442) ).
cnf(u7969,negated_conjecture,
( c2_2(X0,a1435)
| c2_1(X0)
| c1_1(X0)
| c4_2(X0,a1358)
| c5_2(X0,a1459)
| c5_2(X0,a1357) ) ).
cnf(u499,negated_conjecture,
~ c5_2(a1464,a1466) ).
cnf(u7968,negated_conjecture,
( c2_2(X0,a1435)
| c2_1(X0)
| c1_1(X0)
| c4_2(X0,a1373)
| c5_2(X0,a1459)
| ~ c1_2(X0,a1374) ) ).
cnf(u6983,negated_conjecture,
( ~ c3_2(a1510,X0)
| c4_2(a1510,X0)
| ~ c2_2(a1510,X0) ) ).
cnf(u501,negated_conjecture,
ndr1_1(a1464) ).
cnf(u8179,negated_conjecture,
c5_2(a1439,a1414) ).
cnf(u7965,negated_conjecture,
( ~ c3_2(X0,a1379)
| c2_1(X0)
| c1_1(X0)
| c5_2(X0,a1459)
| c4_2(X0,a1379)
| c2_2(X0,a1435)
| c5_2(X0,a1433)
| c3_1(X0) ) ).
cnf(u5632,negated_conjecture,
c2_2(a1333,a1379) ).
cnf(u8153,negated_conjecture,
~ c3_2(a1439,a1414) ).
cnf(u4960,negated_conjecture,
( ~ c2_2(X0,a1357)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,a1358)
| c4_2(X0,a1505) ) ).
cnf(u8590,negated_conjecture,
~ c3_2(a1430,a1373) ).
cnf(u4887,negated_conjecture,
~ c3_1(a1452) ).
cnf(u3449,negated_conjecture,
~ c1_2(a1333,a1334) ).
cnf(u153,axiom,
( ~ sP17(X0)
| ndr1_1(X0) ) ).
cnf(u4676,negated_conjecture,
( ~ c5_2(X0,a1358)
| c2_2(X0,a1505)
| ~ c2_2(X0,a1358)
| c1_1(X0)
| c1_2(X0,a1357) ) ).
cnf(u150,axiom,
( ~ sP17(X0)
| ~ c2_2(X0,a1377) ) ).
cnf(u4722,negated_conjecture,
( ~ c2_2(X0,a1358)
| c4_2(X0,a1459)
| c4_2(X0,a1358)
| c1_1(X0)
| c1_2(X0,a1357) ) ).
cnf(u7832,negated_conjecture,
( ~ c4_2(a1350,X1)
| ~ c1_2(a1350,X1) ) ).
cnf(u7486,negated_conjecture,
~ c1_2(a1493,a1459) ).
cnf(u88,axiom,
( ~ sP24(X0)
| ~ c2_2(X0,a1330) ) ).
cnf(u7888,negated_conjecture,
c1_1(a1490) ).
cnf(u4689,negated_conjecture,
( ~ c4_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,a1324)
| ~ c2_2(X0,a1324)
| c3_1(X0)
| c1_1(X0) ) ).
cnf(u4858,negated_conjecture,
( ~ c5_2(X0,a1358)
| c3_2(X0,a1505)
| ~ c2_2(X0,a1358)
| c1_1(X0)
| c1_2(X0,a1357) ) ).
cnf(u6426,negated_conjecture,
( c3_2(a1495,X0)
| c5_2(a1495,X0)
| c2_2(a1495,X0) ) ).
cnf(u4055,negated_conjecture,
( c2_2(a1363,X0)
| ~ c5_2(a1363,X0)
| ~ c4_2(a1363,X0) ) ).
cnf(u5680,negated_conjecture,
ndr1_1(a1516) ).
cnf(u7970,negated_conjecture,
( c2_2(X0,a1435)
| c2_1(X0)
| c1_1(X0)
| c4_2(X0,a1358)
| c5_2(X0,a1459)
| c1_2(X0,a1357) ) ).
cnf(u4832,negated_conjecture,
c1_1(a1409) ).
cnf(u8069,negated_conjecture,
~ c5_2(a1428,a1413) ).
cnf(u3507,negated_conjecture,
( ~ c1_2(X50,a1379)
| c2_1(X50)
| c3_2(X50,X51)
| c5_2(X50,X51)
| c4_2(X50,X51) ) ).
cnf(u4741,negated_conjecture,
( c4_2(X0,a1459)
| c1_1(X0)
| c4_2(X0,a1373)
| c4_2(X0,a1374) ) ).
cnf(u5649,negated_conjecture,
~ c3_1(a1454) ).
cnf(u8405,negated_conjecture,
c1_1(a1378) ).
cnf(u4263,negated_conjecture,
c4_2(a1363,a1505) ).
cnf(u5896,negated_conjecture,
c4_2(a1333,a1414) ).
cnf(u414,negated_conjecture,
c5_1(a1494) ).
cnf(u6466,negated_conjecture,
( ~ c2_2(X0,a1489)
| c1_1(X0)
| c1_2(X0,a1358)
| c4_2(X0,a1459)
| c4_2(X0,a1489)
| c4_1(X0) ) ).
cnf(u503,negated_conjecture,
c2_2(a1464,a1465) ).
cnf(u4436,negated_conjecture,
( ~ c5_2(a1436,X0)
| ~ c2_2(a1436,X0)
| c4_2(a1436,X0) ) ).
cnf(u8661,negated_conjecture,
c5_1(a1442) ).
cnf(u289,axiom,
( ~ sP1(X0)
| c4_2(X0,a1513) ) ).
cnf(u6480,negated_conjecture,
ndr1_1(a1350) ).
cnf(u4134,negated_conjecture,
( c2_2(a1464,X0)
| ~ c5_2(a1464,X0)
| ~ c4_2(a1464,X0) ) ).
cnf(u4721,negated_conjecture,
( ~ c2_2(X0,a1358)
| c4_2(X0,a1459)
| c4_2(X0,a1358)
| c1_1(X0)
| c5_2(X0,a1357) ) ).
cnf(u7780,negated_conjecture,
( ~ c1_2(a1516,X1)
| ~ c4_2(a1516,X1) ) ).
cnf(u3452,negated_conjecture,
c1_1(a1333) ).
cnf(u3458,negated_conjecture,
( ~ c1_2(a1333,X7)
| c4_2(a1333,X7)
| ~ c3_2(a1333,X7) ) ).
cnf(u3450,negated_conjecture,
ndr1_1(a1333) ).
cnf(u3604,negated_conjecture,
( ~ c3_2(X0,X1)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u5085,negated_conjecture,
( c3_2(X0,a1489)
| c4_1(X0)
| c1_1(X0)
| c1_2(X0,a1358) ) ).
cnf(u5400,negated_conjecture,
~ c4_2(a1464,a1396) ).
cnf(u152,axiom,
( ~ sP17(X0)
| ~ c3_2(X0,a1377) ) ).
cnf(u4333,negated_conjecture,
c4_2(a1363,a1489) ).
cnf(u8712,negated_conjecture,
~ c5_2(a1430,a1374) ).
cnf(u3459,negated_conjecture,
( ~ c5_1(X114)
| c3_2(X114,X115)
| ~ c2_2(X114,X115)
| c4_2(X114,X115)
| c1_1(X114) ) ).
cnf(u3447,negated_conjecture,
c4_2(a1333,a1334) ).
cnf(u504,negated_conjecture,
c3_2(a1464,a1465) ).
cnf(u7966,negated_conjecture,
( c2_2(X0,a1435)
| c2_1(X0)
| c1_1(X0)
| c4_2(X0,a1373)
| c5_2(X0,a1459)
| c4_2(X0,a1374) ) ).
cnf(u5851,negated_conjecture,
~ c4_2(a1363,a1364) ).
cnf(u1710,negated_conjecture,
c2_1(a1442) ).
cnf(u151,axiom,
( ~ sP17(X0)
| c5_2(X0,a1377) ) ).
cnf(u6374,negated_conjecture,
~ c5_2(a1452,a1413) ).
cnf(u500,negated_conjecture,
c2_2(a1464,a1466) ).
cnf(u5897,negated_conjecture,
c4_2(a1428,a1414) ).
cnf(u3535,negated_conjecture,
( c2_2(X0,a1379)
| c2_1(X0)
| c5_2(X0,a1433)
| c4_2(X0,a1433)
| c3_1(X0) ) ).
cnf(u4805,negated_conjecture,
( ~ c5_2(X0,a1374)
| c4_2(X0,a1373)
| c1_1(X0)
| c2_1(X0)
| c2_2(X0,a1379)
| c5_2(X0,a1373)
| c4_2(X0,a1459) ) ).
cnf(u5063,negated_conjecture,
( c3_2(X0,a1489)
| c4_2(X0,a1414)
| c4_1(X0)
| c1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ).
cnf(u90,axiom,
( ~ sP24(X0)
| ndr1_1(X0) ) ).
cnf(u89,axiom,
( ~ sP24(X0)
| c1_2(X0,a1330) ) ).
cnf(u7162,negated_conjecture,
~ c1_2(a1428,a1526) ).
cnf(u5736,negated_conjecture,
( c2_2(a1516,X0)
| ~ c5_2(a1516,X0)
| ~ c4_2(a1516,X0) ) ).
cnf(u6427,negated_conjecture,
( c3_2(a1495,X0)
| ~ c5_2(a1495,X0)
| ~ c2_2(a1495,X0) ) ).
cnf(u518,negated_conjecture,
c2_1(a1458) ).
cnf(u5202,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a1459)
| c2_1(X0)
| c1_1(X0)
| ~ c3_2(X0,X1)
| c4_2(X0,X1)
| c2_2(X0,a1435) ) ).
cnf(u4862,negated_conjecture,
( ~ c4_2(X0,a1433)
| c5_2(X0,a1433)
| c2_2(X0,a1435)
| c2_1(X0)
| c1_1(X0)
| c3_1(X0) ) ).
cnf(u4953,negated_conjecture,
c5_2(a1428,a1429) ).
cnf(u5518,negated_conjecture,
~ c1_2(a1428,a1396) ).
cnf(u458,negated_conjecture,
c3_0 ).
cnf(u3496,negated_conjecture,
( ~ c4_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,X1)
| c4_1(X0)
| c1_1(X0) ) ).
cnf(u4860,negated_conjecture,
( ~ c5_2(X0,a1358)
| c3_2(X0,a1505)
| c1_1(X0)
| c1_2(X0,a1357) ) ).
cnf(u4743,negated_conjecture,
( c5_2(X0,a1357)
| c4_2(X0,a1459)
| c4_2(X0,a1358)
| c1_1(X0) ) ).
cnf(u8019,negated_conjecture,
( c2_2(X0,a1379)
| c1_1(X0)
| c5_2(X0,a1459)
| c4_2(X0,a1379)
| c2_2(X0,a1435)
| c5_2(X0,a1433)
| c3_1(X0)
| c2_1(X0)
| c5_2(X0,a1379) ) ).
cnf(u7674,negated_conjecture,
~ c3_1(a1482) ).
cnf(u8588,negated_conjecture,
( ~ c5_2(X0,a1358)
| c1_1(X0)
| c1_2(X0,a1357)
| c5_2(X0,a1459)
| c2_1(X0)
| c4_2(X0,a1505)
| c2_2(X0,a1435) ) ).
cnf(u8408,negated_conjecture,
c1_1(a1434) ).
cnf(u6492,negated_conjecture,
( c3_2(a1350,X0)
| ~ c5_2(a1350,X0)
| ~ c2_2(a1350,X0) ) ).
cnf(u6429,negated_conjecture,
( ~ c5_2(a1495,X0)
| ~ c3_2(a1495,X0) ) ).
cnf(u8150,negated_conjecture,
( ~ c4_2(a1439,X0)
| c2_2(a1439,X0) ) ).
cnf(u8080,negated_conjecture,
~ c3_1(a1475) ).
cnf(u6387,negated_conjecture,
c5_1(a1495) ).
cnf(u4334,negated_conjecture,
c2_2(a1363,a1489) ).
cnf(u6580,negated_conjecture,
~ c4_2(a1350,a1396) ).
cnf(u287,axiom,
( ~ sP1(X0)
| c2_2(X0,a1513) ) ).
cnf(u8586,negated_conjecture,
( ~ c5_2(X0,a1358)
| c1_1(X0)
| c1_2(X0,a1357)
| c4_2(X0,a1459)
| c4_2(X0,a1505)
| c2_1(X0)
| c2_2(X0,a1379)
| c5_2(X0,a1505) ) ).
cnf(u4769,negated_conjecture,
( c2_2(X0,a1505)
| c4_2(X0,a1358)
| c1_1(X0)
| ~ c2_2(X0,a1357)
| c4_2(X0,a1459) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN520+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n010.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:25:33 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.80/1.58 % (2052400)Detected formulas, will run a generic FOF schedule.
% 5.80/1.58 % (2052406)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=105171511:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.80/1.58 % (2052407)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=1438412521:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.80/1.58 % (2052405)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=657048727:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.80/1.58 % (2052410)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2012851121:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.80/1.58 % (2052409)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2352564251:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.80/1.58 % (2052408)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1154671000:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.80/1.58 % (2052411)dis-21_1_sil=8000:lcm=predicate:random_seed=1558308711: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)
% 5.80/1.58 % (2052408)Instruction limit reached!
% 5.80/1.58 % (2052408)------------------------------
% 5.80/1.58 % (2052408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052408)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052408)Termination reason: Instruction limit
% 5.80/1.58 % (2052408)Termination phase: Saturation
% 5.80/1.58 % (2052408)Time elapsed: 0.062 s
% 5.80/1.58 % (2052408)Peak memory usage: 91 MB
% 5.80/1.58 % (2052408)Instructions burned: 109 (million)
% 5.80/1.58 % (2052409)Instruction limit reached!
% 5.80/1.58 % (2052409)------------------------------
% 5.80/1.58 % (2052409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052409)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052409)Termination reason: Instruction limit
% 5.80/1.58 % (2052409)Termination phase: Saturation
% 5.80/1.58 % (2052409)Time elapsed: 0.064 s
% 5.80/1.58 % (2052409)Peak memory usage: 89 MB
% 5.80/1.58 % (2052409)Instructions burned: 120 (million)
% 5.80/1.58 % (2052411)Instruction limit reached!
% 5.80/1.58 % (2052411)------------------------------
% 5.80/1.58 % (2052411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052411)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052411)Termination reason: Instruction limit
% 5.80/1.58 % (2052411)Termination phase: Saturation
% 5.80/1.58 % (2052411)Time elapsed: 0.073 s
% 5.80/1.58 % (2052411)Peak memory usage: 92 MB
% 5.80/1.58 % (2052411)Instructions burned: 129 (million)
% 5.80/1.58 % (2052410)Instruction limit reached!
% 5.80/1.58 % (2052410)------------------------------
% 5.80/1.58 % (2052410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052410)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052410)Termination reason: Instruction limit
% 5.80/1.58 % (2052410)Termination phase: Saturation
% 5.80/1.58 % (2052410)Time elapsed: 0.079 s
% 5.80/1.58 % (2052410)Peak memory usage: 92 MB
% 5.80/1.58 % (2052410)Instructions burned: 139 (million)
% 5.80/1.58 % (2052419)lrs+10_1_sil=8000:sp=occurrence:random_seed=3728576233:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.80/1.58 % (2052420)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4097289163:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.80/1.58 % (2052421)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1050603354:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.80/1.58 % (2052422)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=2925203435:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.80/1.58 % (2052420)Refutation not found, incomplete strategy
% 5.80/1.58 % (2052420)------------------------------
% 5.80/1.58 % (2052420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052420)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052420)Termination reason: Refutation not found, incomplete strategy
% 5.80/1.58 % (2052420)Time elapsed: 0.032 s
% 5.80/1.58 % (2052420)Peak memory usage: 91 MB
% 5.80/1.58 % (2052420)Instructions burned: 52 (million)
% 5.80/1.58 % (2052422)Refutation not found, incomplete strategy
% 5.80/1.58 % (2052422)------------------------------
% 5.80/1.58 % (2052422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052422)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052422)Termination reason: Refutation not found, incomplete strategy
% 5.80/1.58 % (2052422)Time elapsed: 0.036 s
% 5.80/1.58 % (2052422)Peak memory usage: 91 MB
% 5.80/1.58 % (2052422)Instructions burned: 59 (million)
% 5.80/1.58 % (2052421)Refutation not found, incomplete strategy
% 5.80/1.58 % (2052421)------------------------------
% 5.80/1.58 % (2052421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052421)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052421)Termination reason: Refutation not found, incomplete strategy
% 5.80/1.58 % (2052421)Time elapsed: 0.116 s
% 5.80/1.58 % (2052421)Peak memory usage: 93 MB
% 5.80/1.58 % (2052421)Instructions burned: 197 (million)
% 5.80/1.58 % (2052419)Instruction limit reached!
% 5.80/1.58 % (2052419)------------------------------
% 5.80/1.58 % (2052419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052419)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052419)Termination reason: Instruction limit
% 5.80/1.58 % (2052419)Termination phase: Saturation
% 5.80/1.58 % (2052419)Time elapsed: 0.161 s
% 5.80/1.58 % (2052419)Peak memory usage: 93 MB
% 5.80/1.58 % (2052419)Instructions burned: 287 (million)
% 5.80/1.58 % (2052420)------------------------------
% 5.80/1.58 % (2052420)------------------------------
% 5.80/1.58 % (2052427)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=176332617:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 5.80/1.58 % (2052422)------------------------------
% 5.80/1.58 % (2052422)------------------------------
% 5.80/1.58 % (2052421)------------------------------
% 5.80/1.58 % (2052421)------------------------------
% 5.80/1.58 % (2052428)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3415127987:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 5.80/1.58 % (2052406)First to succeed.
% 5.80/1.58 % (2052406)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2052400"
% 5.80/1.58 % (2052430)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1263257016:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 5.80/1.58 % (2052427)Instruction limit reached!
% 5.80/1.58 % (2052427)------------------------------
% 5.80/1.58 % (2052427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052427)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052427)Termination reason: Instruction limit
% 5.80/1.58 % (2052427)Termination phase: Saturation
% 5.80/1.58 % (2052427)Time elapsed: 0.170 s
% 5.80/1.58 % (2052427)Peak memory usage: 93 MB
% 5.80/1.58 % (2052427)Instructions burned: 294 (million)
% 5.80/1.58 % (2052430)Instruction limit reached!
% 5.80/1.58 % (2052430)------------------------------
% 5.80/1.58 % (2052430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.80/1.58 % (2052430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.80/1.58 % (2052430)CaDiCaL version: 2.1.3
% 5.80/1.58 % (2052430)Termination reason: Instruction limit
% 5.80/1.58 % (2052430)Termination phase: Saturation
% 5.80/1.58 % (2052430)Time elapsed: 0.069 s
% 5.80/1.58 % (2052430)Peak memory usage: 92 MB
% 5.80/1.58 % (2052430)Instructions burned: 113 (million)
% 5.80/1.58 % (2052431)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3404035934:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 5.80/1.58 % SZS status CounterSatisfiable for theBenchmark
% 5.80/1.58 % SZS output start Saturation.
% See solution above
% 5.80/1.59 % SZS output start Definitions and Model Updates.
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_0 | ~c5_2(X155,a1512) | sP1(X155) | ndr1_1(X155) | ~ndr1_0 | c4_0 is false, set ~c5_2(X155,a1512) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_0 | c1_0 | ndr1_1(X47) | ~c5_2(X47,a1374) | c1_1(X47) | ~ndr1_0 is false, set ~c5_2(X47,a1374) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c5_2(X0,a1480) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c5_2(X0,a1480) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_2(X53,a1381) | ndr1_1(X53) | c2_1(X53) | ~ndr1_0 | ~c3_0 | ~c5_0 is false, set c4_2(X53,a1381) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_1(X0) | c4_2(X0,a1462) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set c4_2(X0,a1462) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_0 | c1_0 | ndr1_1(X47) | c4_2(X47,a1374) | c1_1(X47) | ~ndr1_0 is false, set c4_2(X47,a1374) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_1(X0) | ndr1_1(X0) | c4_2(X0,a1463) | ~ndr1_0 | ~sP8 is false, set c4_2(X0,a1463) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_2(X0,a1480) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set c4_2(X0,a1480) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_1(X0) | ~c3_2(X0,a1462) | ndr1_1(X0) | ~ndr1_0 | ~sP8 is false, set ~c3_2(X0,a1462) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_1(X0) | ndr1_1(X0) | ~c3_2(X0,a1463) | ~ndr1_0 | ~sP8 is false, set ~c3_2(X0,a1463) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c3_2(X0,a1480) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c3_2(X0,a1480) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X53) | ~c3_2(X53,a1382) | c2_1(X53) | ~ndr1_0 | ~c3_0 | ~c5_0 is false, set ~c3_2(X53,a1382) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_2(X0,a1329) | sP24(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~c1_2(X0,a1329) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_0 | ~c1_2(X155,a1512) | sP1(X155) | ndr1_1(X155) | ~ndr1_0 | c4_0 is false, set ~c1_2(X155,a1512) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_0 | c1_0 | ndr1_1(X47) | ~c1_2(X47,a1374) | c1_1(X47) | ~ndr1_0 is false, set ~c1_2(X47,a1374) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_0 | c1_0 | ~c1_2(X47,a1373) | ndr1_1(X47) | c1_1(X47) | ~ndr1_0 is false, set ~c1_2(X47,a1373) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_2(X0,a1371) | c3_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set ~c1_2(X0,a1371) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | ~c2_2(X0,a1376) | sP17(X0) | ~ndr1_0 | ~sP18 is false, set ~c2_2(X0,a1376) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_1(X0) | ndr1_1(X0) | ~c2_2(X0,a1463) | ~ndr1_0 | ~sP8 is false, set ~c2_2(X0,a1463) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | ~c2_2(X0,a1481) | ~ndr1_0 | ~sP6 is false, set ~c2_2(X0,a1481) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c2_1(X12) | ~c2_2(X12,a1340) | ndr1_1(X12) | ~ndr1_0 | ~c3_0 | c4_0 is false, set ~c2_2(X12,a1340) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | c3_1(X0) | ~c2_2(X0,a1372) | ~ndr1_0 | ~sP19 is false, set ~c2_2(X0,a1372) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c2_2(X0,a1371) | c3_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set ~c2_2(X0,a1371) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_0 | ~c2_2(X155,a1512) | sP1(X155) | ndr1_1(X155) | ~ndr1_0 | c4_0 is false, set ~c2_2(X155,a1512) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c2_2(X0,a1375) | ndr1_1(X0) | sP17(X0) | ~ndr1_0 | ~sP18 is false, set ~c2_2(X0,a1375) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c2_2(X0,a1329) | sP24(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set c2_2(X0,a1329) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | sP24(X0) | c2_2(X0,a1331) | ~ndr1_0 | ~sP25 is false, set c2_2(X0,a1331) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X53) | c2_2(X53,a1382) | c2_1(X53) | ~ndr1_0 | ~c3_0 | ~c5_0 is false, set c2_2(X53,a1382) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_0 | c1_0 | c2_2(X47,a1373) | ndr1_1(X47) | c1_1(X47) | ~ndr1_0 is false, set c2_2(X47,a1373) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X29) | c2_2(X29,a1358) | c1_1(X29) | ~ndr1_0 | c4_0 | ~c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ~c4_1(X30) | ~ndr1_0 is false, set c2_2(X29,a1358) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_0 | ndr1_1(X155) | sP1(X155) | c2_2(X155,a1514) | ~ndr1_0 | c4_0 is false, set c2_2(X155,a1514) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c4_2(X0,a1329) | sP24(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP25 is false, set ~c4_2(X0,a1329) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c2_1(X12) | ~c4_2(X12,a1340) | ndr1_1(X12) | ~ndr1_0 | ~c3_0 | c4_0 is false, set ~c4_2(X12,a1340) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c2_1(X12) | ndr1_1(X12) | ~c4_2(X12,a1341) | ~ndr1_0 | ~c3_0 | c4_0 is false, set ~c4_2(X12,a1341) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c4_2(X29,a1357) | ndr1_1(X29) | c1_1(X29) | ~ndr1_0 | c4_0 | ~c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ~c4_1(X30) | ~ndr1_0 is false, set ~c4_2(X29,a1357) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X53) | ~c4_2(X53,a1382) | c2_1(X53) | ~ndr1_0 | ~c3_0 | ~c5_0 is false, set ~c4_2(X53,a1382) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | c3_1(X0) | c1_2(X0,a1372) | ~ndr1_0 | ~sP19 is false, set c1_2(X0,a1372) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c1_2(X0,a1375) | ndr1_1(X0) | sP17(X0) | ~ndr1_0 | ~sP18 is false, set c1_2(X0,a1375) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | c1_2(X0,a1481) | ~ndr1_0 | ~sP6 is false, set c1_2(X0,a1481) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X29) | c1_2(X29,a1358) | c1_1(X29) | ~ndr1_0 | c4_0 | ~c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ~c4_1(X30) | ~ndr1_0 is false, set c1_2(X29,a1358) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c1_2(X29,a1357) | ndr1_1(X29) | c1_1(X29) | ~ndr1_0 | c4_0 | ~c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ~c4_1(X30) | ~ndr1_0 is false, set c1_2(X29,a1357) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c1_2(X53,a1381) | ndr1_1(X53) | c2_1(X53) | ~ndr1_0 | ~c3_0 | ~c5_0 is false, set c1_2(X53,a1381) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | c5_2(X0,a1376) | sP17(X0) | ~ndr1_0 | ~sP18 is false, set c5_2(X0,a1376) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | c3_1(X0) | c5_2(X0,a1372) | ~ndr1_0 | ~sP19 is false, set c5_2(X0,a1372) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_2(X29,a1357) | ndr1_1(X29) | c1_1(X29) | ~ndr1_0 | c4_0 | ~c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ~c4_1(X30) | ~ndr1_0 is false, set c5_2(X29,a1357) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | sP2 | c5_2(a1503,X144) | ~c2_2(a1503,X144) | ~c1_2(a1503,X144) | ~ndr1_1(a1503) is false, set c5_2(a1503,X144) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_2(a1499,X143) | c5_2(a1499,X143) | ~ndr1_1(a1499) | sP2 | ndr1_0 is false, set c5_2(a1499,X143) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c2_1(X12) | ndr1_1(X12) | c5_2(X12,a1341) | ~ndr1_0 | ~c3_0 | c4_0 is false, set c5_2(X12,a1341) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | sP24(X0) | c3_2(X0,a1331) | ~ndr1_0 | ~sP25 is false, set c3_2(X0,a1331) to true
% 5.80/1.59 for all groundings, until fixed point,
% 5.80/1.59 whenever ndr1_1(X29) | c3_2(X29,a1358) | c1_1(X29) | ~ndr1_0 | c4_0 | ~c3_2(X30,X31) | ~c4_2(X30,X31) | ~ndr1_1(X30) | ~c4_1(X30) | ~ndr1_0 is false, set c3_2(X29,a1358) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_2(X53,a1381) | ndr1_1(X53) | c2_1(X53) | ~ndr1_0 | ~c3_0 | ~c5_0 is false, set c3_2(X53,a1381) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_0 | ndr1_1(X155) | sP1(X155) | c3_2(X155,a1514) | ~ndr1_0 | c4_0 is false, set c3_2(X155,a1514) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_2(X0,a1375) | ndr1_1(X0) | sP17(X0) | ~ndr1_0 | ~sP18 is false, set c3_2(X0,a1375) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_2(X0,a1371) | c3_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP19 is false, set c3_2(X0,a1371) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_0 | c1_0 | c3_2(X47,a1373) | ndr1_1(X47) | c1_1(X47) | ~ndr1_0 is false, set c3_2(X47,a1373) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c4_0 | ~c2_1(a1389) is false, set ~c2_1(a1389) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c2_1(a1516) | c2_0 is false, set ~c2_1(a1516) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_1(a1388) | ~c4_0 | ndr1_0 is false, set ~c1_1(a1388) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c4_0 | ndr1_0 | ~c1_1(a1366) is false, set ~c1_1(a1366) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c4_0 | ndr1_0 | ~c3_1(a1366) is false, set ~c3_1(a1366) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c1_1(X64) | ~ndr1_0 | ~c2_2(X65,X66) | c3_2(X65,X66) | c1_2(X65,X66) | ~ndr1_1(X65) | c1_2(X65,X67) | c4_2(X65,X67) | ~ndr1_1(X65) | ~c2_1(X65) | ~ndr1_0 | ndr1_1(X68) | c3_2(X68,X69) | c5_2(X68,X69) | ~ndr1_1(X68) | ~c3_1(X68) | ~ndr1_0 is false, set ~c3_1(X68) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ndr1_1(X130) | ~c2_1(X130) | ~ndr1_0 | ~c3_1(X131) | c4_2(X131,X132) | c5_2(X131,X132) | c3_2(X131,X132) | ~ndr1_1(X131) | ~ndr1_0 is false, set ~c3_1(X131) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c1_2(X130,a1491) | ~c2_1(X130) | ~ndr1_0 | ~c3_1(X131) | c4_2(X131,X132) | c5_2(X131,X132) | c3_2(X131,X132) | ~ndr1_1(X131) | ~ndr1_0 is false, set ~c3_1(X131) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c5_2(X130,a1491) | ~c2_1(X130) | ~ndr1_0 | ~c3_1(X131) | c4_2(X131,X132) | c5_2(X131,X132) | c3_2(X131,X132) | ~ndr1_1(X131) | ~ndr1_0 is false, set ~c3_1(X131) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c3_1(a1499) | sP2 | ndr1_0 is false, set ~c3_1(a1499) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | sP2 | ~c3_1(a1503) is false, set ~c3_1(a1503) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X126) | ~c5_2(X126,X127) | c4_2(X126,X127) | ~ndr1_1(X126) | c4_1(X126) | ~ndr1_0 is false, set c4_1(X126) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c1_1(a1515) | ndr1_0 | c2_0 is false, set c1_1(a1515) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c1_1(X112) | ~c2_2(X112,X113) | c4_2(X112,X113) | ~c3_2(X112,X113) | ~ndr1_1(X112) | ndr1_1(X112) | ~ndr1_0 | c4_0 is false, set c1_1(X112) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c3_1(X154) | c5_1(X154) | ~c1_1(X154) | ~ndr1_0 is false, set c5_1(X154) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c2_0 | ~c5_2(X32,X33) | c2_2(X32,X33) | ~c4_2(X32,X33) | ~ndr1_1(X32) | ndr1_1(X32) | c1_1(X32) | ~ndr1_0 is false, set ~c2_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | ~c1_2(X84,a1411) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | ndr1_1(X84) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | ndr1_1(X84) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | c1_2(a1412,X86) | c5_2(a1412,X86) | ~c3_2(a1412,X86) | ~ndr1_1(a1412) is false, set c3_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | ndr1_1(X84) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | c4_1(a1412) is false, set c3_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | c2_2(X84,a1411) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | ~c4_2(X84,a1411) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | c1_1(X151) | c5_1(X151) | ~ndr1_0 | ~c1_0 is false, set c5_1(X151) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | c5_1(a1516) | c2_0 is false, set c5_1(a1516) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_2(X76,X77) | ~c2_2(X76,X77) | c4_2(X76,X77) | ~ndr1_1(X76) | ~c2_1(X76) | ndr1_1(X76) | ~ndr1_0 | ~c4_0 | c1_1(X78) | ~c1_2(X78,a1398) | ~ndr1_0 is false, set ~c4_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_2(X76,X77) | ~c2_2(X76,X77) | c4_2(X76,X77) | ~ndr1_1(X76) | ~c2_1(X76) | ndr1_1(X76) | ~ndr1_0 | ~c4_0 | c1_1(X78) | ndr1_1(X78) | ~ndr1_0 is false, set ~c4_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_2(X76,X77) | ~c2_2(X76,X77) | c4_2(X76,X77) | ~ndr1_1(X76) | ~c2_1(X76) | ndr1_1(X76) | ~ndr1_0 | ~c4_0 | c1_1(X78) | ~c5_2(X78,a1398) | ~ndr1_0 is false, set ~c4_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c5_2(X76,X77) | ~c2_2(X76,X77) | c4_2(X76,X77) | ~ndr1_1(X76) | ~c2_1(X76) | ndr1_1(X76) | ~ndr1_0 | ~c4_0 | c1_1(X78) | ~c4_2(X78,a1398) | ~ndr1_0 is false, set ~c4_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c3_1(X121) | c5_2(X121,X122) | c3_2(X121,X122) | ~ndr1_1(X121) | ndr1_1(X121) | ~ndr1_0 | ~c4_0 is false, set ~c4_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_0 | ~c4_0 | ndr1_1(X58) | ~c5_2(X58,X59) | c3_2(X58,X59) | ~ndr1_1(X58) | c4_2(X58,X60) | c1_2(X58,X60) | ~ndr1_1(X58) | ~ndr1_0 is false, set ~c4_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c3_1(a1515) | ndr1_0 | c2_0 is false, set c3_1(a1515) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c4_0 | c3_1(a1365) | ndr1_0 is false, set c3_1(a1365) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ndr1_1(X100) | c2_1(X100) | ~c4_2(X100,X101) | c5_2(X100,X101) | c3_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c1_2(a1434,X99) | c3_2(a1434,X99) | c5_2(a1434,X99) | ~ndr1_1(a1434) | ndr1_1(X100) | c2_1(X100) | ~c4_2(X100,X101) | c5_2(X100,X101) | c3_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | c2_1(X21) | ~c3_1(X21) | ~ndr1_0 | ~c4_0 is false, set c2_1(X21) to true
% 5.80/1.59 for all groundings, until fixed point,
% 5.80/1.59 whenever ~c2_1(X49) | c5_1(X49) | c3_1(X49) | ~ndr1_0 | ndr1_1(X50) | c4_2(X50,X51) | c5_2(X50,X51) | c3_2(X50,X51) | ~ndr1_1(X50) | c2_1(X50) | ~ndr1_0 | c4_0 is false, set c2_1(X50) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c4_2(a1434,X98) | c1_2(a1434,X98) | ~ndr1_1(a1434) | ndr1_1(X100) | c2_1(X100) | ~c4_2(X100,X101) | c5_2(X100,X101) | c3_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever c2_1(a1434) | ndr1_1(X100) | c2_1(X100) | ~c4_2(X100,X101) | c5_2(X100,X101) | c3_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | c2_2(X100,a1435) | c2_1(X100) | ~c4_2(X100,X101) | c5_2(X100,X101) | c3_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c4_2(X100,a1435) | c2_1(X100) | ~c4_2(X100,X101) | c5_2(X100,X101) | c3_2(X100,X101) | ~ndr1_1(X100) | ~ndr1_0 is false, set c2_1(X100) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_1(X0) | ~c1_2(X0,X1) | ~c2_2(X0,X1) | ~ndr1_1(X0) | c4_2(X0,X2) | ~c3_2(X0,X2) | ~ndr1_1(X0) | ~ndr1_0 | ~c5_0 | c2_1(X3) | ~ndr1_0 is false, set ~c5_0 to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ~c5_1(X56) | ~c2_1(X56) | c2_2(X56,X57) | c3_2(X56,X57) | c5_2(X56,X57) | ~ndr1_1(X56) | ~ndr1_0 | ndr1_0 is false, set ~c5_1(X56) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c4_0 | ~c5_1(a1389) is false, set ~c5_1(a1389) to true
% 5.80/1.59 for all groundings,
% 5.80/1.59 whenever ndr1_0 | ~c5_2(X62,X63) | ~c2_2(X62,X63) | c3_2(X62,X63) | ~ndr1_1(X62) | ~c5_1(X62) | ~c1_1(X62) | ~ndr1_0 | c5_0 is false, set ~c5_1(X62) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c3_0 | ndr1_1(X84) | c1_2(X84,X85) | c3_2(X84,X85) | ~ndr1_1(X84) | ~ndr1_0 | ~c5_1(a1412) is false, set ~c5_1(a1412) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | sP2 | ~c5_1(a1503) is false, set ~c5_1(a1503) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c5_1(a1499) | sP2 | ndr1_0 is false, set ~c5_1(a1499) to true
% 7.09/1.77 for all groundings, until fixed point,
% 7.09/1.77 whenever ndr1_1(X70) | ~c1_1(X70) | ~c4_2(X70,X71) | ~c3_2(X70,X71) | ~ndr1_1(X70) | ~ndr1_0 | c1_1(X72) | c2_1(X72) | c5_1(X72) | ~ndr1_0 | ~c5_1(X73) | ~c4_2(X73,X74) | ~c2_2(X73,X74) | ~c1_2(X73,X74) | ~ndr1_1(X73) | ~c5_2(X73,X75) | ~c3_2(X73,X75) | ~ndr1_1(X73) | ~ndr1_0 is false, set ~c5_1(X73) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X87) | c3_1(X87) | ~c1_2(X87,X88) | c5_2(X87,X88) | ~c4_2(X87,X88) | ~ndr1_1(X87) | ~ndr1_0 | c5_2(X89,a1414) | c3_1(X89) | c2_1(X89) | ~ndr1_0 | c2_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X87) | c3_1(X87) | ~c1_2(X87,X88) | c5_2(X87,X88) | ~c4_2(X87,X88) | ~ndr1_1(X87) | ~ndr1_0 | c4_2(X89,a1414) | c3_1(X89) | c2_1(X89) | ~ndr1_0 | c2_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c2_2(X106,X107) | c5_2(X106,X107) | ~c4_2(X106,X107) | ~ndr1_1(X106) | ~c1_2(X106,X108) | c2_2(X106,X108) | ~c4_2(X106,X108) | ~ndr1_1(X106) | ~c1_1(X106) | ~ndr1_0 | c2_0 | ndr1_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X87) | c3_1(X87) | ~c1_2(X87,X88) | c5_2(X87,X88) | ~c4_2(X87,X88) | ~ndr1_1(X87) | ~ndr1_0 | c2_2(X89,a1414) | c3_1(X89) | c2_1(X89) | ~ndr1_0 | c2_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c2_0 | ndr1_1(X148) | ~c5_2(X148,X149) | ~c1_2(X148,X149) | ~c2_2(X148,X149) | ~ndr1_1(X148) | ~ndr1_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c2_0 | ndr1_0 | ~c5_1(X15) | c4_1(X15) | c4_2(X15,X16) | ~c3_2(X15,X16) | ~ndr1_1(X15) | ~ndr1_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X133) | c5_2(X133,X134) | c1_2(X133,X134) | c2_2(X133,X134) | ~ndr1_1(X133) | c1_1(X133) | ~ndr1_0 | c1_0 | c2_2(a1493,X135) | c1_2(a1493,X135) | ~ndr1_1(a1493) is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X133) | c5_2(X133,X134) | c1_2(X133,X134) | c2_2(X133,X134) | ~ndr1_1(X133) | c1_1(X133) | ~ndr1_0 | c1_0 | ~c2_1(a1493) is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X133) | c5_2(X133,X134) | c1_2(X133,X134) | c2_2(X133,X134) | ~ndr1_1(X133) | c1_1(X133) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c3_2(X133,a1492) | c5_2(X133,X134) | c1_2(X133,X134) | c2_2(X133,X134) | ~ndr1_1(X133) | c1_1(X133) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c4_2(X133,a1492) | c5_2(X133,X134) | c1_2(X133,X134) | c2_2(X133,X134) | ~ndr1_1(X133) | c1_1(X133) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_2(X145,X146) | ~c4_2(X145,X146) | c3_2(X145,X146) | ~ndr1_1(X145) | c2_1(X145) | ~c3_1(X145) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | ~c3_2(X156,a1517) | ndr1_1(X156) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | ndr1_1(X156) | c5_2(X156,a1518) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ~c2_2(X160,a1523) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | c1_0 | c5_2(a1524,a1525) is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X87) | c3_1(X87) | ~c1_2(X87,X88) | c5_2(X87,X88) | ~c4_2(X87,X88) | ~ndr1_1(X87) | ~ndr1_0 | ndr1_1(X89) | c3_1(X89) | c2_1(X89) | ~ndr1_0 | c2_0 is false, set c2_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c5_2(X133,a1492) | c5_2(X133,X134) | c1_2(X133,X134) | c2_2(X133,X134) | ~ndr1_1(X133) | c1_1(X133) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | ndr1_1(X156) | ndr1_1(X156) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | ndr1_1(X156) | c1_2(X156,a1518) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | ndr1_1(X156) | ~c4_2(X156,a1518) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | ~c4_2(X156,a1517) | ndr1_1(X156) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | ~c4_0 | c1_2(X156,X157) | ~c4_2(X156,X157) | ~ndr1_1(X156) | c1_2(X156,a1517) | ndr1_1(X156) | ~ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | c1_0 | ndr1_1(a1524) is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ndr1_1(X160) | ~ndr1_0 | c1_0 | ~c4_2(a1524,X162) | c1_2(a1524,X162) | ~ndr1_1(a1524) is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ~c5_2(X160,a1523) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_1(X160) | c4_2(X160,X161) | c1_2(X160,X161) | c2_2(X160,X161) | ~ndr1_1(X160) | ~c4_2(X160,a1523) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c5_1(X114) | c1_1(X114) | c4_2(X114,X115) | ~c2_2(X114,X115) | c3_2(X114,X115) | ~ndr1_1(X114) | ~ndr1_0 | ndr1_0 | ~c3_0 is false, set ~c3_0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c4_2(X4,a1324) | ~c4_1(X4) | c3_1(X4) | ~ndr1_0 | ndr1_0 is false, set ~c4_1(X4) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c5_2(X4,a1324) | ~c4_1(X4) | c3_1(X4) | ~ndr1_0 | ndr1_0 is false, set ~c4_1(X4) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c3_2(X4,a1324) | ~c4_1(X4) | c3_1(X4) | ~ndr1_0 | ndr1_0 is false, set ~c4_1(X4) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~c3_1(X22) | c5_1(X22) | ~c4_1(X22) | ~ndr1_0 | c3_0 is false, set ~c4_1(X22) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c4_2(X17,X18) | c2_2(X17,X18) | ~c5_2(X17,X18) | ~ndr1_1(X17) | ndr1_1(X17) | c1_1(X17) | ~ndr1_0 | ~c5_1(X19) | c3_1(X19) | ~c4_1(X19) | ~ndr1_0 | c5_0 is false, set ~c4_1(X19) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_1(X4) | ~c4_1(X4) | c3_1(X4) | ~ndr1_0 | ndr1_0 is false, set ~c4_1(X4) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c5_0 | ~c4_1(X27) | c3_2(X27,X28) | c4_2(X27,X28) | ~ndr1_1(X27) | ndr1_1(X27) | ~ndr1_0 | c2_0 is false, set ~c4_1(X27) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | ndr1_1(X116) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | c2_2(X118,a1474) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | ndr1_1(X116) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | ndr1_1(X118) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~c4_0 | ~c4_1(a1389) is false, set ~c4_1(a1389) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | ~c5_2(X116,a1473) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | ndr1_1(X118) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | c3_2(X116,a1473) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | ndr1_1(X118) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | c2_2(X116,a1473) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | ndr1_1(X118) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | ndr1_1(X116) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | c4_2(X118,a1474) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c2_0 | ndr1_1(X116) | ~c4_1(X116) | ~c1_2(X116,X117) | ~c2_2(X116,X117) | ~ndr1_1(X116) | ~ndr1_0 | ~c3_2(X118,X119) | c5_2(X118,X119) | ~ndr1_1(X118) | c5_2(X118,a1474) | c5_1(X118) | ~ndr1_0 is false, set ~c4_1(X116) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c4_0 | ~c1_1(X24) | ~c5_1(X24) | ~c4_1(X24) | ~ndr1_0 | c2_2(X25,X26) | ~ndr1_1(X25) | ndr1_1(X25) | ~c5_1(X25) | ~ndr1_0 is false, set ~c4_1(X24) to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | sP19 | ~c5_0 is false, set sP19 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever c1_0 | sP6 | ndr1_0 is false, set sP6 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c4_0 | ndr1_0 | sP8 is false, set sP8 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever sP18 | c2_0 | ndr1_0 is false, set sP18 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | sP25 | ~c5_0 is false, set sP25 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ~c1_2(X158,X159) | c3_2(X158,X159) | ~ndr1_1(X158) | ndr1_1(X158) | ~ndr1_0 | sP0 | ~c2_0 is false, set sP0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP3 is false, set ~sP3 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP0 is false, set ~sP0 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP7 is false, set ~sP7 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP12 is false, set ~sP12 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP13 is false, set ~sP13 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP14 is false, set ~sP14 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP21 is false, set ~sP21 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP16 is false, set ~sP16 to true
% 7.09/1.77 for all groundings,
% 7.09/1.77 whenever ndr1_0 | ~sP15 is false, set ~sP15 to true
% 7.09/1.77 % SZS output end Definitions and Model Updates.
% 7.09/1.77 % (2052406)------------------------------
% 7.09/1.77 % (2052406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.09/1.77 % (2052406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.09/1.77 % (2052406)CaDiCaL version: 2.1.3
% 7.09/1.77 % (2052406)Termination reason: Satisfiable
% 7.09/1.77 % (2052406)Time elapsed: 0.655 s
% 7.09/1.77 % (2052406)Peak memory usage: 138 MB
% 7.09/1.77 % (2052406)Instructions burned: 1728 (million)
% 7.09/1.77 % (2052406)------------------------------
% 7.09/1.77 % (2052406)------------------------------
% 7.09/1.77 % (2052400)Success in time 0.925 s
% 7.09/1.77 % Vampire exiting
%------------------------------------------------------------------------------