%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN425-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 : n001.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 : Satisfiable 4.92s 1.53s
% Output : Saturation 6.63s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u535,negated_conjecture,
c2_0 ).
cnf(u538,negated_conjecture,
( ~ c4_2(X2,X3)
| c4_1(X2)
| c4_2(X2,X4)
| c9_2(X2,X4)
| c2_2(X2,X3)
| ~ c1_2(X2,X4)
| ~ ndr1_1(X2)
| ~ c7_2(X2,X3) ) ).
cnf(u541,negated_conjecture,
ndr1_0 ).
cnf(u549,negated_conjecture,
c1_0 ).
cnf(u556,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,X4)
| c2_2(X0,X4)
| c10_2(X0,X4)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c10_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u569,negated_conjecture,
~ c6_0 ).
cnf(u579,negated_conjecture,
( ~ c6_2(X2,X3)
| c9_1(X2)
| ~ ndr1_1(X2)
| ~ c9_2(X2,X3)
| ~ c5_2(X2,X3) ) ).
cnf(u593,negated_conjecture,
( ~ c3_2(X0,X1)
| c7_2(X0,X3)
| c5_2(X0,X3)
| c3_2(X0,X3)
| c7_2(X0,X1)
| c10_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u596,negated_conjecture,
ssSkC11 ).
cnf(u601,negated_conjecture,
~ c7_0 ).
cnf(u608,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c10_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u616,negated_conjecture,
( ~ c4_2(X0,X2)
| c4_2(X0,X3)
| c3_2(X0,X3)
| c8_2(X0,X2)
| c2_2(X0,X1)
| c8_2(X0,X1)
| ~ c5_2(X0,X3)
| ~ c1_2(X0,X2)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u650,negated_conjecture,
~ c8_0 ).
cnf(u681,negated_conjecture,
c4_0 ).
cnf(u688,negated_conjecture,
( ~ c6_2(X0,X1)
| c7_1(X0)
| c3_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u708,negated_conjecture,
~ ssSkC19 ).
cnf(u712,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,X2)
| c1_2(X0,X2)
| c9_2(X0,X2)
| ~ c10_2(X0,a1292)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u716,negated_conjecture,
( ~ c6_2(X0,a1292)
| c6_2(X0,X1)
| c3_2(X0,X2)
| c1_2(X0,X2)
| c9_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u720,negated_conjecture,
( ~ c7_2(X0,X1)
| c7_1(X0)
| c10_2(X0,X2)
| c6_2(X0,X2)
| c3_2(X0,X1)
| ~ c9_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u729,negated_conjecture,
( ~ c2_1(X1)
| c7_1(X1)
| c3_1(X1) ) ).
cnf(u732,negated_conjecture,
ssSkC25 ).
cnf(u740,negated_conjecture,
( ~ c2_1(X1)
| c7_1(X1)
| c8_2(X1,X2)
| c6_2(X1,X2)
| c3_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u743,negated_conjecture,
ssSkC26 ).
cnf(u755,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_2(X0,a1292)
| c6_2(X0,X1)
| c3_2(X0,X2)
| c1_2(X0,X2)
| c9_2(X0,X2)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u766,negated_conjecture,
( ~ c8_1(X0)
| ~ c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u782,negated_conjecture,
( ~ c1_2(X0,X1)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ c4_2(X0,a1312)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u786,negated_conjecture,
( ~ c1_2(X0,X1)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ c3_2(X0,a1312)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u790,negated_conjecture,
~ c3_0 ).
cnf(u794,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_1(X0)
| ~ c9_2(X0,a1340)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u798,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_1(X0)
| ~ c2_2(X0,a1340)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u825,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,a1312)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u829,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_1(X0)
| c6_2(X0,a1340)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u833,negated_conjecture,
~ c10_0 ).
cnf(u848,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| c4_1(X0) ) ).
cnf(u852,negated_conjecture,
( ~ c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u886,negated_conjecture,
( ~ c3_2(X0,X1)
| c9_2(X0,X1)
| ~ c5_1(X0)
| ~ c7_2(X0,a1231)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u889,negated_conjecture,
ssSkC6 ).
cnf(u930,negated_conjecture,
~ ssSkC21 ).
cnf(u934,negated_conjecture,
( ~ c6_2(X0,a1301)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u938,negated_conjecture,
( ~ c9_2(X0,X1)
| ~ c10_2(X0,a1301)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u946,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_1(X0)
| c4_2(X0,X1)
| c9_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u955,negated_conjecture,
( ~ c3_2(X0,X1)
| c6_2(X0,a1231)
| c9_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u959,negated_conjecture,
( ~ c3_2(X0,X1)
| c9_2(X0,a1231)
| c9_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u973,negated_conjecture,
ssSkC30 ).
cnf(u976,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ c8_2(X0,a1348)
| ~ ndr1_1(X0) ) ).
cnf(u980,negated_conjecture,
( ~ c9_2(X0,X1)
| c8_2(X0,a1301)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u988,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_1(X0)
| c4_2(X0,a1348)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u992,negated_conjecture,
ndr1_1(a1327) ).
cnf(u996,negated_conjecture,
( ~ c3_2(a1327,X0)
| ~ c10_2(a1327,X0)
| ~ c2_2(a1327,X0) ) ).
cnf(u1003,negated_conjecture,
( ~ c1_1(X0)
| c10_1(X0)
| c6_1(X0) ) ).
cnf(u1006,negated_conjecture,
ssSkC1 ).
cnf(u1015,negated_conjecture,
~ c5_0 ).
cnf(u1019,negated_conjecture,
ndr1_1(a1247) ).
cnf(u1023,negated_conjecture,
( ~ c10_2(a1247,X0)
| c5_2(a1247,X0)
| ~ c2_2(a1247,X0) ) ).
cnf(u1035,negated_conjecture,
ndr1_1(a1307) ).
cnf(u1039,negated_conjecture,
( ~ c4_2(a1307,X0)
| ~ c5_2(a1307,X0)
| ~ c6_2(a1307,X0) ) ).
cnf(u1042,negated_conjecture,
ssSkC22 ).
cnf(u1054,negated_conjecture,
ssSkC34 ).
cnf(u1068,negated_conjecture,
ssSkC18 ).
cnf(u1080,negated_conjecture,
ssSkC24 ).
cnf(u1091,negated_conjecture,
~ ssSkC27 ).
cnf(u1095,negated_conjecture,
ndr1_1(a1333) ).
cnf(u1099,negated_conjecture,
( ~ c4_2(a1333,X0)
| ~ c9_2(a1333,X0)
| ~ c10_2(a1333,X0) ) ).
cnf(u1104,negated_conjecture,
ssSkC31 ).
cnf(u1119,negated_conjecture,
ndr1_1(a1210) ).
cnf(u1123,negated_conjecture,
( ~ c1_2(a1210,X0)
| c5_2(a1210,X0)
| c2_2(a1210,X0) ) ).
cnf(u1135,negated_conjecture,
~ ssSkC5 ).
cnf(u1146,negated_conjecture,
ssSkC7 ).
cnf(u1158,negated_conjecture,
ssSkC8 ).
cnf(u1163,negated_conjecture,
ndr1_1(a1252) ).
cnf(u1167,negated_conjecture,
( ~ c4_2(a1252,X0)
| c8_2(a1252,X0)
| ~ c3_2(a1252,X0) ) ).
cnf(u1192,negated_conjecture,
( ~ c3_2(a1307,X0)
| c5_2(a1307,X0)
| ~ c9_2(a1307,X0) ) ).
cnf(u1204,negated_conjecture,
ndr1_1(a1346) ).
cnf(u1208,negated_conjecture,
( ~ c5_2(a1346,X0)
| c9_2(a1346,X0)
| ~ c10_2(a1346,X0) ) ).
cnf(u1212,negated_conjecture,
( ~ c6_2(a1346,X0)
| c8_2(a1346,X0)
| ~ c10_2(a1346,X0) ) ).
cnf(u1224,negated_conjecture,
~ ssSkC33 ).
cnf(u1229,negated_conjecture,
ssSkC3 ).
cnf(u1241,negated_conjecture,
ssSkC4 ).
cnf(u1253,negated_conjecture,
ssSkC15 ).
cnf(u1269,negated_conjecture,
ssSkC29 ).
cnf(u1280,negated_conjecture,
( ~ c9_1(X1)
| c8_1(X1)
| ndr1_1(X1) ) ).
cnf(u1284,negated_conjecture,
ndr1_1(a1211) ).
cnf(u1288,negated_conjecture,
( ~ c7_2(a1211,X0)
| c2_2(a1211,X0)
| c1_2(a1211,X0) ) ).
cnf(u1292,negated_conjecture,
ndr1_1(a1288) ).
cnf(u1296,negated_conjecture,
( ~ c2_2(a1288,X0)
| c3_2(a1288,X0)
| c1_2(a1288,X0) ) ).
cnf(u1300,negated_conjecture,
( ~ c8_2(a1288,X0)
| c5_2(a1288,X0)
| c4_2(a1288,X0) ) ).
cnf(u1304,negated_conjecture,
( ~ c1_2(a1288,X0)
| c8_2(a1288,X0)
| c3_2(a1288,X0) ) ).
cnf(u1338,negated_conjecture,
ndr1_1(a1240) ).
cnf(u1346,negated_conjecture,
ndr1_1(a1208) ).
cnf(u1350,negated_conjecture,
( ~ c4_2(a1208,X0)
| ~ c10_2(a1208,X0) ) ).
cnf(u1380,negated_conjecture,
( ~ c8_2(X0,a1224)
| c7_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1384,negated_conjecture,
( ~ c1_2(X0,a1224)
| c7_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1406,negated_conjecture,
( ~ c5_2(X0,a1314)
| ~ c7_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1410,negated_conjecture,
( c7_2(a1350,X0)
| c6_2(a1350,X0)
| c1_2(a1350,X0) ) ).
cnf(u1413,negated_conjecture,
ndr1_1(a1350) ).
cnf(u1418,negated_conjecture,
ndr1_1(a1363) ).
cnf(u1422,negated_conjecture,
( ~ c10_2(a1363,X0)
| c3_2(a1363,X0)
| c1_2(a1363,X0) ) ).
cnf(u1446,negated_conjecture,
~ ssSkC32 ).
cnf(u1450,negated_conjecture,
( c2_2(a1353,X0)
| c5_2(a1353,X0)
| c3_2(a1353,X0) ) ).
cnf(u1453,negated_conjecture,
ndr1_1(a1353) ).
cnf(u1458,negated_conjecture,
c9_0 ).
cnf(u1462,negated_conjecture,
ndr1_1(a1214) ).
cnf(u1466,negated_conjecture,
( ~ c5_2(a1214,X0)
| c7_2(a1214,X0) ) ).
cnf(u1500,negated_conjecture,
( ~ c3_2(X0,a1300)
| ~ c2_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1503,negated_conjecture,
ssSkC20 ).
cnf(u1508,negated_conjecture,
( ~ c7_1(X0)
| c10_2(X0,a1314)
| ~ ssSkP5(X0) ) ).
cnf(u1512,negated_conjecture,
( ~ c7_1(X0)
| c4_2(X0,a1314)
| ~ ssSkP5(X0) ) ).
cnf(u1520,negated_conjecture,
~ ssSkC14 ).
cnf(u1524,negated_conjecture,
( ~ c9_2(X0,a1268)
| c8_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1528,negated_conjecture,
( ~ c8_2(X0,a1268)
| c8_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1532,negated_conjecture,
~ ssSkC23 ).
cnf(u1536,negated_conjecture,
( ~ c2_2(X0,a1310)
| c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1540,negated_conjecture,
( ~ c3_2(X0,a1310)
| c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1544,negated_conjecture,
( c2_2(a1200,X0)
| c4_2(a1200,X0) ) ).
cnf(u1547,negated_conjecture,
ndr1_1(a1200) ).
cnf(u1556,negated_conjecture,
( ~ c3_1(X0)
| c8_1(X0) ) ).
cnf(u1569,negated_conjecture,
( ~ c2_1(X0)
| c6_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1579,negated_conjecture,
( ~ c1_1(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u1587,negated_conjecture,
( ~ c10_1(X0)
| c1_2(X0,a1300)
| ~ c2_1(X0) ) ).
cnf(u1591,negated_conjecture,
( ~ c10_1(X0)
| c5_2(X0,a1300)
| ~ c2_1(X0) ) ).
cnf(u1603,negated_conjecture,
( ~ ssSkP5(X0)
| ndr1_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1607,negated_conjecture,
ssSkC28 ).
cnf(u1611,negated_conjecture,
( ~ c4_2(X0,a1345)
| c3_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1615,negated_conjecture,
( ~ c4_2(X0,a1222)
| c6_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u1627,negated_conjecture,
( ~ c9_1(X0)
| c8_1(X0)
| c7_2(X0,a1268) ) ).
cnf(u1631,negated_conjecture,
~ ssSkC16 ).
cnf(u1635,negated_conjecture,
( ~ c5_2(X0,a1280)
| c1_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u1639,negated_conjecture,
( ~ c3_1(X0)
| c8_1(X0)
| c1_2(X0,a1310) ) ).
cnf(u1643,negated_conjecture,
( ~ c10_1(X0)
| ndr1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1647,negated_conjecture,
( ~ c4_2(X0,a1356)
| c8_1(X0)
| ~ ssSkP10(X0) ) ).
cnf(u1651,negated_conjecture,
( ~ c5_2(X0,a1356)
| c8_1(X0)
| ~ ssSkP10(X0) ) ).
cnf(u1655,negated_conjecture,
( ~ c10_2(X0,a1360)
| c8_1(X0)
| ~ ssSkP11(X0) ) ).
cnf(u1687,negated_conjecture,
ndr1_1(a1311) ).
cnf(u1692,negated_conjecture,
( ~ c5_1(X0)
| c4_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1697,negated_conjecture,
( ~ ssSkP8(X0)
| c3_1(X0)
| c5_2(X0,a1345) ) ).
cnf(u1701,negated_conjecture,
( ~ ssSkP1(X0)
| c6_1(X0)
| c5_2(X0,a1222) ) ).
cnf(u1705,negated_conjecture,
( ~ ssSkP1(X0)
| c6_1(X0)
| c2_2(X0,a1222) ) ).
cnf(u1714,negated_conjecture,
( ~ ssSkP4(X0)
| c1_1(X0)
| c4_2(X0,a1280) ) ).
cnf(u1718,negated_conjecture,
( ~ c3_1(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u1722,negated_conjecture,
( ~ ssSkP10(X0)
| c8_1(X0)
| c1_2(X0,a1356) ) ).
cnf(u1730,negated_conjecture,
( ~ ssSkP11(X0)
| c8_1(X0)
| c6_2(X0,a1360) ) ).
cnf(u1743,negated_conjecture,
( ~ c9_2(X0,a1246)
| c7_1(X0) ) ).
cnf(u1746,negated_conjecture,
ssSkC10 ).
cnf(u1750,negated_conjecture,
ssSkC9 ).
cnf(u1755,negated_conjecture,
( ~ c1_2(X0,a1246)
| c7_1(X0) ) ).
cnf(u1763,negated_conjecture,
( ~ ssSkP8(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1767,negated_conjecture,
( ~ c2_2(X0,a1352)
| c2_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u1771,negated_conjecture,
( ~ c8_2(X0,a1352)
| c2_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u1775,negated_conjecture,
( ~ ssSkP1(X0)
| c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u1779,negated_conjecture,
( ~ ssSkP4(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u1783,negated_conjecture,
( ~ ssSkP10(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u1787,negated_conjecture,
( ~ ssSkP11(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u1791,negated_conjecture,
( c7_1(X0)
| c5_2(X0,a1246) ) ).
cnf(u1795,negated_conjecture,
( c6_1(X0)
| c9_1(X0)
| c7_1(X0) ) ).
cnf(u1799,negated_conjecture,
( ~ ssSkP9(X0)
| c2_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u1804,negated_conjecture,
~ c6_2(a1226,a1227) ).
cnf(u1809,negated_conjecture,
~ c5_2(a1226,a1227) ).
cnf(u1814,negated_conjecture,
~ c8_2(a1226,a1227) ).
cnf(u1818,negated_conjecture,
( c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u1843,negated_conjecture,
~ c3_2(a1327,a1328) ).
cnf(u1847,negated_conjecture,
( ~ ssSkP9(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u1853,negated_conjecture,
~ c6_1(a1200) ).
cnf(u1858,negated_conjecture,
~ c9_1(a1210) ).
cnf(u1863,negated_conjecture,
~ c2_2(a1211,a1212) ).
cnf(u1868,negated_conjecture,
~ c8_2(a1211,a1212) ).
cnf(u1873,negated_conjecture,
~ c6_1(a1220) ).
cnf(u1878,negated_conjecture,
~ c9_1(a1226) ).
cnf(u1898,negated_conjecture,
~ c6_2(a1252,a1253) ).
cnf(u1903,negated_conjecture,
~ c2_2(a1252,a1253) ).
cnf(u1908,negated_conjecture,
~ c10_2(a1252,a1254) ).
cnf(u1961,negated_conjecture,
ssSkC17 ).
cnf(u1967,negated_conjecture,
~ c4_2(a1307,a1308) ).
cnf(u1972,negated_conjecture,
~ c5_1(a1316) ).
cnf(u1977,negated_conjecture,
~ c8_1(a1316) ).
cnf(u1982,negated_conjecture,
c8_2(a1327,a1328) ).
cnf(u1997,negated_conjecture,
~ c2_2(a1346,a1347) ).
cnf(u2002,negated_conjecture,
~ c4_2(a1346,a1347) ).
cnf(u2047,negated_conjecture,
~ c9_2(a1333,a1334) ).
cnf(u2052,negated_conjecture,
~ c3_2(a1333,a1334) ).
cnf(u2064,negated_conjecture,
c9_1(a1208) ).
cnf(u2069,negated_conjecture,
c10_1(a1208) ).
cnf(u2074,negated_conjecture,
c10_1(a1210) ).
cnf(u2079,negated_conjecture,
~ c10_1(a1211) ).
cnf(u2084,negated_conjecture,
c10_2(a1211,a1212) ).
cnf(u2089,negated_conjecture,
c3_1(a1214) ).
cnf(u2094,negated_conjecture,
c1_1(a1214) ).
cnf(u2099,negated_conjecture,
c10_1(a1220) ).
cnf(u2104,negated_conjecture,
c2_1(a1220) ).
cnf(u2114,negated_conjecture,
c7_1(a1226) ).
cnf(u2119,negated_conjecture,
ndr1_1(a1226) ).
cnf(u2129,negated_conjecture,
c9_1(a1247) ).
cnf(u2134,negated_conjecture,
c6_1(a1247) ).
cnf(u2139,negated_conjecture,
c5_2(a1252,a1253) ).
cnf(u2144,negated_conjecture,
c5_2(a1252,a1254) ).
cnf(u2149,negated_conjecture,
c2_2(a1252,a1254) ).
cnf(u2221,negated_conjecture,
c7_2(a1307,a1308) ).
cnf(u2226,negated_conjecture,
c5_2(a1307,a1308) ).
cnf(u2231,negated_conjecture,
~ c5_1(a1311) ).
cnf(u2236,negated_conjecture,
~ c4_1(a1311) ).
cnf(u2241,negated_conjecture,
c10_1(a1327) ).
cnf(u2277,negated_conjecture,
c6_2(a1346,a1347) ).
cnf(u2282,negated_conjecture,
~ c10_1(a1350) ).
cnf(u2312,negated_conjecture,
~ c1_2(a1363,a1364) ).
cnf(u2317,negated_conjecture,
~ c7_2(a1363,a1364) ).
cnf(u2357,negated_conjecture,
~ c7_1(a1240) ).
cnf(u2442,negated_conjecture,
c6_2(a1333,a1334) ).
cnf(u2457,negated_conjecture,
~ c3_1(a1353) ).
cnf(u2462,negated_conjecture,
~ c5_1(a1353) ).
cnf(u2547,negated_conjecture,
~ c6_1(a1363) ).
cnf(u2552,negated_conjecture,
c2_2(a1363,a1364) ).
cnf(u2650,negated_conjecture,
c3_1(a1333) ).
cnf(u2776,negated_conjecture,
~ c7_1(a1333) ).
cnf(u2780,negated_conjecture,
~ c10_1(a1333) ).
cnf(u2789,negated_conjecture,
~ c10_1(a1214) ).
cnf(u2842,negated_conjecture,
c9_1(a1200) ).
cnf(u2849,negated_conjecture,
c7_1(a1220) ).
cnf(u2863,negated_conjecture,
~ c4_1(a1220) ).
cnf(u2868,negated_conjecture,
c5_1(a1220) ).
cnf(u2878,negated_conjecture,
c7_1(a1363) ).
cnf(u2896,negated_conjecture,
c4_2(a1200,a1279) ).
cnf(u2900,negated_conjecture,
~ ssSkP5(a1200) ).
cnf(u2905,negated_conjecture,
c4_2(a1200,a1313) ).
cnf(u2915,negated_conjecture,
~ ssSkP5(a1220) ).
cnf(u2924,negated_conjecture,
~ ssSkP5(a1226) ).
cnf(u2933,negated_conjecture,
~ ssSkP5(a1363) ).
cnf(u2957,negated_conjecture,
~ c2_1(a1208) ).
cnf(u2966,negated_conjecture,
~ c2_1(a1210) ).
cnf(u2976,negated_conjecture,
~ c2_1(a1327) ).
cnf(u2996,negated_conjecture,
c7_2(a1200,a1268) ).
cnf(u3005,negated_conjecture,
c7_2(a1208,a1268) ).
cnf(u3014,negated_conjecture,
c7_2(a1247,a1268) ).
cnf(u3048,negated_conjecture,
~ ssSkP9(a1200) ).
cnf(u3087,negated_conjecture,
c5_2(a1353,a1345) ).
cnf(u3099,negated_conjecture,
c4_2(a1363,a1221) ).
cnf(u3103,negated_conjecture,
c5_2(a1363,a1222) ).
cnf(u3108,negated_conjecture,
c4_2(a1220,a1221) ).
cnf(u3117,negated_conjecture,
c4_2(a1200,a1221) ).
cnf(u3134,negated_conjecture,
c10_2(a1220,a1221) ).
cnf(u3139,negated_conjecture,
c10_2(a1200,a1221) ).
cnf(u3150,negated_conjecture,
c2_2(a1363,a1222) ).
cnf(u3157,negated_conjecture,
c6_2(a1316,a1355) ).
cnf(u3168,negated_conjecture,
c9_2(a1316,a1355) ).
cnf(u3175,negated_conjecture,
c7_2(a1316,a1359) ).
cnf(u3179,negated_conjecture,
c9_2(a1316,a1360) ).
cnf(u3195,negated_conjecture,
c6_2(a1316,a1360) ).
cnf(u3206,negated_conjecture,
c3_2(a1208,a1351) ).
cnf(u3210,negated_conjecture,
c10_2(a1208,a1352) ).
cnf(u3215,negated_conjecture,
c3_2(a1210,a1351) ).
cnf(u3219,negated_conjecture,
c10_2(a1210,a1352) ).
cnf(u3224,negated_conjecture,
c3_2(a1327,a1351) ).
cnf(u3228,negated_conjecture,
c10_2(a1327,a1352) ).
cnf(u3234,negated_conjecture,
~ c2_2(a1327,a1351) ).
cnf(u3254,negated_conjecture,
c8_2(a1210,a1351) ).
cnf(u3277,negated_conjecture,
c5_2(a1316,a1345) ).
cnf(u3291,negated_conjecture,
~ c10_2(a1346,a1347) ).
cnf(u3294,negated_conjecture,
~ c8_2(a1346,a1347) ).
cnf(u3303,negated_conjecture,
~ ssSkP9(a1353) ).
cnf(u3306,negated_conjecture,
~ c2_1(a1353) ).
cnf(u3321,negated_conjecture,
~ ssSkP4(a1353) ).
cnf(u3326,negated_conjecture,
c3_2(a1353,a1279) ).
cnf(u3331,negated_conjecture,
ssSkP5(a1353) ).
cnf(u3357,negated_conjecture,
c5_2(a1353,a1246) ).
cnf(u3373,negated_conjecture,
~ c2_2(a1247,a1314) ).
cnf(u3395,negated_conjecture,
~ c8_2(a1288,a1313) ).
cnf(u3400,negated_conjecture,
c4_2(a1288,a1314) ).
cnf(u3408,negated_conjecture,
~ c2_2(a1210,a1313) ).
cnf(u3417,negated_conjecture,
c4_2(a1210,a1314) ).
cnf(u3421,negated_conjecture,
c5_2(a1210,a1246) ).
cnf(u3455,negated_conjecture,
~ c10_1(a1226) ).
cnf(u3464,negated_conjecture,
c1_2(a1363,a1356) ).
cnf(u3468,negated_conjecture,
~ c10_1(a1363) ).
cnf(u3477,negated_conjecture,
c1_2(a1220,a1356) ).
cnf(u3497,negated_conjecture,
c9_2(a1220,a1360) ).
cnf(u3501,negated_conjecture,
c7_2(a1220,a1359) ).
cnf(u3520,negated_conjecture,
~ c5_2(a1346,a1347) ).
cnf(u3533,negated_conjecture,
~ c5_2(a1316,a1360) ).
cnf(u3536,negated_conjecture,
~ c9_1(a1316) ).
cnf(u3542,negated_conjecture,
~ c5_2(a1316,a1355) ).
cnf(u3553,negated_conjecture,
c6_2(a1220,a1360) ).
cnf(u3563,negated_conjecture,
~ c1_2(a1220,a1359) ).
cnf(u3572,negated_conjecture,
~ c5_2(a1220,a1360) ).
cnf(u3582,negated_conjecture,
c4_1(a1316) ).
cnf(u3590,negated_conjecture,
c3_2(a1316,a1351) ).
cnf(u3596,negated_conjecture,
c10_2(a1311,a1352) ).
cnf(u3614,negated_conjecture,
c8_2(a1316,a1351) ).
cnf(u3627,negated_conjecture,
c10_2(a1316,a1351) ).
cnf(u3645,negated_conjecture,
c4_2(a1220,a1344) ).
cnf(u3649,negated_conjecture,
c5_2(a1220,a1345) ).
cnf(u3659,negated_conjecture,
~ c9_2(a1220,a1344) ).
cnf(u3671,negated_conjecture,
c1_2(a1220,a1344) ).
cnf(u3678,negated_conjecture,
c3_2(a1214,a1351) ).
cnf(u3682,negated_conjecture,
c4_1(a1214) ).
cnf(u3704,negated_conjecture,
c8_1(a1240) ).
cnf(u3712,negated_conjecture,
c3_2(a1240,a1351) ).
cnf(u3760,negated_conjecture,
c5_2(a1208,a1246) ).
cnf(u3768,negated_conjecture,
c6_2(a1208,a1355) ).
cnf(u3777,negated_conjecture,
c6_2(a1210,a1355) ).
cnf(u3782,negated_conjecture,
c5_2(a1327,a1246) ).
cnf(u3799,negated_conjecture,
~ c5_2(a1210,a1355) ).
cnf(u3802,negated_conjecture,
c9_2(a1210,a1355) ).
cnf(u3812,negated_conjecture,
c9_2(a1208,a1355) ).
cnf(u3826,negated_conjecture,
c7_2(a1208,a1359) ).
cnf(u3834,negated_conjecture,
~ c1_2(a1208,a1359) ).
cnf(u3869,negated_conjecture,
~ c8_2(a1208,a1355) ).
cnf(u3877,negated_conjecture,
~ c3_1(a1208) ).
cnf(u3880,negated_conjecture,
~ c1_2(a1208,a1355) ).
cnf(u3886,negated_conjecture,
~ c8_2(a1210,a1355) ).
cnf(u3890,negated_conjecture,
~ c4_1(a1210) ).
cnf(u3917,negated_conjecture,
~ c8_2(a1316,a1360) ).
cnf(u3921,negated_conjecture,
~ c3_1(a1316) ).
cnf(u3933,negated_conjecture,
~ c1_2(a1316,a1355) ).
cnf(u3943,negated_conjecture,
~ c4_1(a1333) ).
cnf(u3970,negated_conjecture,
c5_2(a1208,a1345) ).
cnf(u4023,negated_conjecture,
~ c8_2(a1220,a1360) ).
cnf(u4027,negated_conjecture,
~ c10_2(a1220,a1301) ).
cnf(u4032,negated_conjecture,
~ c10_2(a1316,a1301) ).
cnf(u4037,negated_conjecture,
c8_2(a1220,a1344) ).
cnf(u4073,negated_conjecture,
~ c8_2(a1226,a1348) ).
cnf(u4077,negated_conjecture,
c4_2(a1226,a1313) ).
cnf(u4090,negated_conjecture,
~ c8_2(a1363,a1348) ).
cnf(u4097,negated_conjecture,
~ c3_2(a1363,a1313) ).
cnf(u4137,negated_conjecture,
c6_2(a1350,a1279) ).
cnf(u4145,negated_conjecture,
~ c8_2(a1350,a1279) ).
cnf(u4162,negated_conjecture,
~ c9_2(a1350,a1279) ).
cnf(u4180,negated_conjecture,
c4_2(a1363,a1348) ).
cnf(u4194,negated_conjecture,
~ c2_2(a1316,a1359) ).
cnf(u4207,negated_conjecture,
~ c2_2(a1208,a1340) ).
cnf(u4211,negated_conjecture,
c6_1(a1208) ).
cnf(u4216,negated_conjecture,
~ c2_2(a1208,a1268) ).
cnf(u4226,negated_conjecture,
~ c2_2(a1307,a1308) ).
cnf(u4247,negated_conjecture,
~ c1_2(a1200,a1268) ).
cnf(u4251,negated_conjecture,
~ c2_2(a1200,a1340) ).
cnf(u4260,negated_conjecture,
~ c2_2(a1220,a1340) ).
cnf(u4274,negated_conjecture,
~ c10_2(a1200,a1313) ).
cnf(u4295,negated_conjecture,
~ c4_1(a1226) ).
cnf(u4312,negated_conjecture,
~ c4_1(a1363) ).
cnf(u4389,negated_conjecture,
~ c10_1(a1316) ).
cnf(u4407,negated_conjecture,
~ c10_1(a1240) ).
cnf(u4424,negated_conjecture,
~ c10_1(a1353) ).
cnf(u4450,negated_conjecture,
~ c10_1(a1252) ).
cnf(u4507,negated_conjecture,
c7_2(a1210,a1246) ).
cnf(u4511,negated_conjecture,
c3_2(a1210,a1246) ).
cnf(u4525,negated_conjecture,
c3_2(a1327,a1246) ).
cnf(u4534,negated_conjecture,
c7_2(a1220,a1300) ).
cnf(u4537,negated_conjecture,
~ c3_2(a1220,a1300) ).
cnf(u4551,negated_conjecture,
~ c2_2(a1220,a1300) ).
cnf(u4558,negated_conjecture,
~ c2_2(a1210,a1246) ).
cnf(u4562,negated_conjecture,
~ c1_2(a1210,a1246) ).
cnf(u4577,negated_conjecture,
~ c2_2(a1327,a1246) ).
cnf(u4618,negated_conjecture,
~ c9_1(a1333) ).
cnf(u4644,negated_conjecture,
~ c8_1(a1220) ).
cnf(u4679,negated_conjecture,
~ c8_1(a1363) ).
cnf(u4720,negated_conjecture,
c5_2(a1363,a1345) ).
cnf(u4739,negated_conjecture,
c1_2(a1363,a1359) ).
cnf(u4748,negated_conjecture,
c7_2(a1363,a1359) ).
cnf(u4780,negated_conjecture,
~ c2_2(a1363,a1359) ).
cnf(u4814,negated_conjecture,
~ c7_2(a1200,a1231) ).
cnf(u4818,negated_conjecture,
~ c5_1(a1200) ).
cnf(u4827,negated_conjecture,
~ c5_2(a1208,a1351) ).
cnf(u4844,negated_conjecture,
~ c5_2(a1210,a1351) ).
cnf(u4852,negated_conjecture,
~ c5_1(a1210) ).
cnf(u4861,negated_conjecture,
~ c5_2(a1214,a1351) ).
cnf(u4882,negated_conjecture,
~ c7_2(a1327,a1231) ).
cnf(u4886,negated_conjecture,
~ c5_1(a1327) ).
cnf(u5056,negated_conjecture,
c10_2(a1333,a1352) ).
cnf(u5074,negated_conjecture,
~ c5_2(a1240,a1351) ).
cnf(u5126,negated_conjecture,
c8_2(a1240,a1351) ).
cnf(u5170,negated_conjecture,
c10_2(a1240,a1351) ).
cnf(u5197,negated_conjecture,
c4_2(a1316,a1348) ).
cnf(u5202,negated_conjecture,
c4_2(a1311,a1314) ).
cnf(u5276,negated_conjecture,
~ c2_2(a1247,a1352) ).
cnf(u5325,negated_conjecture,
~ c7_2(a1288,a1314) ).
cnf(u5342,negated_conjecture,
~ c7_2(a1200,a1279) ).
cnf(u5354,negated_conjecture,
~ c7_2(a1200,a1221) ).
cnf(u5363,negated_conjecture,
~ c7_2(a1200,a1313) ).
cnf(u5372,negated_conjecture,
~ c7_2(a1210,a1314) ).
cnf(u5390,negated_conjecture,
~ c7_2(a1200,a1340) ).
cnf(u5395,negated_conjecture,
~ c7_2(a1220,a1344) ).
cnf(u5407,negated_conjecture,
~ c7_2(a1220,a1221) ).
cnf(u5416,negated_conjecture,
~ c7_2(a1226,a1313) ).
cnf(u5428,negated_conjecture,
~ c7_2(a1311,a1314) ).
cnf(u5440,negated_conjecture,
~ c7_2(a1363,a1348) ).
cnf(u5452,negated_conjecture,
~ c7_2(a1363,a1221) ).
cnf(u5487,negated_conjecture,
~ c10_1(a1307) ).
cnf(u5502,negated_conjecture,
( c7_2(a1208,X0)
| c10_2(a1208,X0)
| c2_2(a1208,X0) ) ).
cnf(u5536,negated_conjecture,
~ c10_2(a1210,a1246) ).
cnf(u5550,negated_conjecture,
~ c8_1(a1210) ).
cnf(u5556,negated_conjecture,
~ c1_1(a1210) ).
cnf(u5596,negated_conjecture,
c5_2(a1210,a1345) ).
cnf(u5611,negated_conjecture,
c6_2(a1210,a1360) ).
cnf(u5696,negated_conjecture,
c3_2(a1210,a1345) ).
cnf(u5720,negated_conjecture,
~ c5_2(a1210,a1360) ).
cnf(u5736,negated_conjecture,
c10_2(a1208,a1279) ).
cnf(u5767,negated_conjecture,
c2_1(a1214) ).
cnf(u5772,negated_conjecture,
c10_2(a1214,a1351) ).
cnf(u5798,negated_conjecture,
( c6_2(a1214,X0)
| c3_2(a1214,X0)
| c8_2(a1214,X0) ) ).
cnf(u5812,negated_conjecture,
( ~ c9_2(a1214,X0)
| ~ c5_2(a1214,X0)
| c3_2(a1214,X0)
| c8_2(a1214,X0) ) ).
cnf(u5840,negated_conjecture,
~ c10_2(a1200,a1268) ).
cnf(u5856,negated_conjecture,
~ c10_2(a1316,a1359) ).
cnf(u5860,negated_conjecture,
~ c10_2(a1316,a1292) ).
cnf(u5872,negated_conjecture,
~ c10_2(a1208,a1359) ).
cnf(u5876,negated_conjecture,
~ c10_2(a1208,a1292) ).
cnf(u5888,negated_conjecture,
~ c10_2(a1208,a1268) ).
cnf(u5897,negated_conjecture,
~ c10_2(a1220,a1300) ).
cnf(u5901,negated_conjecture,
~ c10_2(a1220,a1292) ).
cnf(u5913,negated_conjecture,
~ c10_2(a1220,a1359) ).
cnf(u5922,negated_conjecture,
~ c10_2(a1247,a1268) ).
cnf(u5938,negated_conjecture,
~ c10_2(a1350,a1292) ).
cnf(u5949,negated_conjecture,
~ c10_2(a1307,a1308) ).
cnf(u5953,negated_conjecture,
~ c10_2(a1307,a1292) ).
cnf(u5965,negated_conjecture,
~ c10_2(a1363,a1359) ).
cnf(u6019,negated_conjecture,
c8_2(a1350,a1292) ).
cnf(u6075,negated_conjecture,
~ c1_2(a1288,a1314) ).
cnf(u6094,negated_conjecture,
~ c1_2(a1316,a1348) ).
cnf(u6109,negated_conjecture,
~ c1_2(a1210,a1314) ).
cnf(u6125,negated_conjecture,
~ c1_2(a1220,a1221) ).
cnf(u6141,negated_conjecture,
~ c1_2(a1311,a1314) ).
cnf(u6157,negated_conjecture,
~ c1_2(a1363,a1221) ).
cnf(u6182,negated_conjecture,
( ~ c5_2(a1200,X0)
| c4_2(a1200,X0)
| c3_2(a1200,X0) ) ).
cnf(u6206,negated_conjecture,
( ~ c4_2(a1226,X1)
| c2_2(a1226,X1)
| c8_2(a1226,X1) ) ).
cnf(u6210,negated_conjecture,
c8_2(a1226,a1313) ).
cnf(u6218,negated_conjecture,
~ c1_2(a1363,a1348) ).
cnf(u6240,negated_conjecture,
c1_2(a1220,a1345) ).
cnf(u6248,negated_conjecture,
c7_2(a1220,a1345) ).
cnf(u6264,negated_conjecture,
~ c10_2(a1220,a1345) ).
cnf(u6273,negated_conjecture,
~ c2_2(a1220,a1345) ).
cnf(u2826,negated_conjecture,
( ~ c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u2740,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0) ) ).
cnf(clause56,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(u3028,negated_conjecture,
( c6_1(X0)
| c2_2(X0,a1222)
| c10_2(X0,a1221) ) ).
cnf(u2945,negated_conjecture,
( ~ ssSkP5(X0)
| c4_2(X0,a1314)
| c5_2(X0,a1246) ) ).
cnf(u2822,negated_conjecture,
( ~ c9_2(X0,a1340)
| c6_1(X0)
| ~ c1_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(clause94,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u3197,negated_conjecture,
( ~ c4_1(X0)
| c3_2(X0,a1351)
| c6_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u5046,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c10_2(X0,a1314)
| c8_2(X0,a1351)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u4262,negated_conjecture,
c4_2(a1200,a1340) ).
cnf(u3982,negated_conjecture,
( c8_1(X0)
| c10_2(X0,a1352)
| c10_2(X0,a1314)
| c3_2(X0,a1351)
| c1_2(X0,a1313) ) ).
cnf(u5150,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c7_2(X0,a1359)
| c8_2(X0,X1)
| c6_2(X0,a1360) ) ).
cnf(u5146,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c6_2(X0,a1355)
| c8_2(X0,X1)
| c1_2(X0,a1356) ) ).
cnf(u5233,negated_conjecture,
( c10_2(X0,a1314)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c6_2(X0,X1)
| c8_2(X0,X1)
| c1_2(X0,a1313) ) ).
cnf(u2762,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_1(X0)
| c4_2(X0,a1348)
| c3_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(clause142,negated_conjecture,
( ssSkP9(X0)
| c3_2(X0,a1351) ) ).
cnf(clause141,negated_conjecture,
( ssSkP9(X0)
| c8_2(X0,a1351) ) ).
cnf(u3198,negated_conjecture,
( c5_1(X0)
| c3_2(X0,a1351)
| c10_2(X0,a1352)
| c4_1(X0) ) ).
cnf(u3090,negated_conjecture,
( c8_1(X0)
| c9_2(X0,a1344)
| c5_2(X0,a1345) ) ).
cnf(clause250,negated_conjecture,
( ~ c1_2(X0,a1325)
| ssSkP7(X0) ) ).
cnf(u5236,negated_conjecture,
( c10_2(X0,a1352)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c8_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,X1)
| c1_2(X0,a1313) ) ).
cnf(u3076,negated_conjecture,
( c1_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314) ) ).
cnf(clause80,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause246,negated_conjecture,
( ~ c4_2(X0,a1355)
| ssSkP10(X0) ) ).
cnf(clause245,negated_conjecture,
( ~ c4_2(X0,a1359)
| ssSkP11(X0) ) ).
cnf(u3620,negated_conjecture,
( ~ c1_1(X0)
| c10_2(X0,a1352)
| c4_1(X0)
| c8_2(X0,a1351) ) ).
cnf(clause73,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u3622,negated_conjecture,
( c7_1(X0)
| c8_2(X0,a1351)
| c10_2(X0,a1352)
| c8_1(X0) ) ).
cnf(clause67,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u3578,negated_conjecture,
( ~ c1_1(X0)
| c10_2(X0,a1352)
| c4_1(X0)
| c3_2(X0,a1351) ) ).
cnf(clause260,negated_conjecture,
( ~ c5_2(X0,a1279)
| ssSkP4(X0) ) ).
cnf(u5109,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c9_2(X0,a1344) ) ).
cnf(u4264,negated_conjecture,
( ~ c10_2(X0,a1313)
| c9_2(X0,a1313)
| ~ c4_1(X0)
| c6_2(X0,a1312)
| c5_2(X0,a1246)
| c4_2(X0,a1314) ) ).
cnf(clause180,negated_conjecture,
( ssSkP1(X0)
| c4_2(X0,a1221) ) ).
cnf(u2885,negated_conjecture,
~ c1_1(a1220) ).
cnf(u3025,negated_conjecture,
( c6_1(X0)
| c5_2(X0,a1222)
| c10_2(X0,a1221) ) ).
cnf(u5162,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c10_2(X0,a1314)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u3633,negated_conjecture,
( ~ c1_1(X0)
| c10_2(X0,a1352)
| c4_1(X0)
| c10_2(X0,a1351) ) ).
cnf(u5032,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c7_2(X0,a1359)
| c8_2(X0,X1)
| c6_2(X0,a1360) ) ).
cnf(u3691,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1352)
| c8_1(X0)
| c4_2(X0,a1314)
| c3_2(X0,a1351) ) ).
cnf(clause136,negated_conjecture,
( ssSkP10(X0)
| c9_2(X0,a1355) ) ).
cnf(u3021,negated_conjecture,
( c3_1(X0)
| c5_2(X0,a1345)
| c9_2(X0,a1344) ) ).
cnf(u3060,negated_conjecture,
( c2_1(X0)
| c10_2(X0,a1352)
| c10_2(X0,a1351) ) ).
cnf(u3152,negated_conjecture,
( ~ c7_1(X0)
| c6_2(X0,a1355)
| ~ c10_1(X0)
| c1_2(X0,a1356) ) ).
cnf(u5227,negated_conjecture,
( c10_2(X0,a1314)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c6_2(X0,X1)
| c8_2(X0,X1)
| c1_2(X0,a1313) ) ).
cnf(u5028,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c6_2(X0,a1355)
| c8_2(X0,X1)
| c1_2(X0,a1356) ) ).
cnf(u5153,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c9_2(X0,a1344) ) ).
cnf(u3272,negated_conjecture,
( ~ c7_1(X0)
| c5_2(X0,a1345)
| ~ c10_1(X0)
| c4_2(X0,a1344) ) ).
cnf(u3241,negated_conjecture,
( c5_1(X0)
| c8_2(X0,a1351)
| c10_2(X0,a1352)
| c4_1(X0) ) ).
cnf(u3079,negated_conjecture,
( c8_1(X0)
| c4_2(X0,a1344)
| c5_2(X0,a1345) ) ).
cnf(u5044,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c10_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u3263,negated_conjecture,
( c3_1(X0)
| c10_2(X0,a1351)
| c7_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u5154,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c1_2(X0,a1344) ) ).
cnf(u5107,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c1_2(X0,a1359)
| c8_2(X0,X1)
| c6_2(X0,a1360) ) ).
cnf(u4627,negated_conjecture,
( c7_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351) ) ).
cnf(u5048,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c10_2(X0,a1314)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u2791,negated_conjecture,
c5_2(a1333,a1246) ).
cnf(clause174,negated_conjecture,
( ssSkP2(X0)
| c9_2(X0,a1233) ) ).
cnf(u3985,negated_conjecture,
( c8_1(X0)
| c10_2(X0,a1352)
| c4_2(X0,a1314)
| c3_2(X0,a1351)
| c1_2(X0,a1313) ) ).
cnf(u3022,negated_conjecture,
( c3_1(X0)
| c5_2(X0,a1345)
| c1_2(X0,a1344) ) ).
cnf(clause150,negated_conjecture,
( ssSkP6(X0)
| c7_2(X0,a1318) ) ).
cnf(u4169,negated_conjecture,
( c5_1(X0)
| c4_2(X0,a1348)
| c3_2(X0,a1313)
| c4_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314) ) ).
cnf(u3727,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1352)
| c8_1(X0)
| c10_2(X0,a1314)
| c8_2(X0,a1351) ) ).
cnf(u2907,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1314)
| c5_2(X0,a1246) ) ).
cnf(clause143,negated_conjecture,
( ssSkP8(X0)
| c1_2(X0,a1344) ) ).
cnf(u4354,negated_conjecture,
( ~ c7_1(X0)
| c4_2(X0,a1314)
| c8_2(X0,a1351)
| c1_2(X0,a1313)
| ~ c10_1(X0)
| c10_2(X0,a1352) ) ).
cnf(clause257,negated_conjecture,
( ~ c3_2(X0,a1313)
| ssSkP5(X0) ) ).
cnf(u2741,negated_conjecture,
( c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u2819,negated_conjecture,
( ~ c9_2(X0,X2)
| c7_1(X0)
| c10_2(X0,X2)
| c6_2(X0,X2)
| c3_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u2739,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(clause58,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(clause57,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u5110,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c1_2(X0,a1344) ) ).
cnf(u3188,negated_conjecture,
( ~ c7_1(X0)
| c7_2(X0,a1359)
| ~ c10_1(X0)
| c6_2(X0,a1360) ) ).
cnf(clause175,negated_conjecture,
( ssSkP2(X0)
| c10_2(X0,a1233) ) ).
cnf(u5029,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c9_2(X0,a1355)
| c8_2(X0,X1)
| c1_2(X0,a1356) ) ).
cnf(u2825,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_1(X0)
| c6_2(X0,a1340)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u5120,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c10_2(X0,a1314)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u2760,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ c8_2(X0,a1348) ) ).
cnf(u3483,negated_conjecture,
( ~ c10_1(X0)
| c9_2(X0,a1355)
| c1_2(X0,a1356)
| c5_2(X0,a1246) ) ).
cnf(u3020,negated_conjecture,
( c3_1(X0)
| c5_2(X0,a1345)
| c4_2(X0,a1344) ) ).
cnf(u4941,negated_conjecture,
( c3_1(X0)
| c9_2(X0,a1313)
| c4_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314)
| c6_2(X0,a1360)
| c7_2(X0,a1359) ) ).
cnf(u5033,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c1_2(X0,a1359)
| c8_2(X0,X1)
| c6_2(X0,a1360) ) ).
cnf(u2742,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u3024,negated_conjecture,
( c6_1(X0)
| c5_2(X0,a1222)
| c4_2(X0,a1221) ) ).
cnf(u3027,negated_conjecture,
( c6_1(X0)
| c2_2(X0,a1222)
| c4_2(X0,a1221) ) ).
cnf(u3555,negated_conjecture,
( ~ c10_1(X0)
| c1_2(X0,a1359)
| c6_2(X0,a1360)
| c5_2(X0,a1246) ) ).
cnf(u2972,negated_conjecture,
c1_2(a1220,a1300) ).
cnf(u2768,negated_conjecture,
c5_2(a1240,a1246) ).
cnf(u5100,negated_conjecture,
( ~ ssSkP5(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c10_2(X0,a1314)
| c8_2(X0,X1) ) ).
cnf(clause251,negated_conjecture,
( ~ c10_2(X0,a1325)
| ssSkP7(X0) ) ).
cnf(u5035,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c9_2(X0,a1344) ) ).
cnf(u3055,negated_conjecture,
c8_2(a1200,a1351) ).
cnf(u2823,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_1(X0)
| ~ c2_2(X0,a1340)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u3074,negated_conjecture,
c1_2(a1200,a1313) ).
cnf(u5152,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c4_2(X0,a1344) ) ).
cnf(clause266,negated_conjecture,
( ~ c8_2(X0,a1221)
| ssSkP1(X0) ) ).
cnf(u3058,negated_conjecture,
( c2_1(X0)
| c10_2(X0,a1352)
| c3_2(X0,a1351) ) ).
cnf(u4942,negated_conjecture,
( c3_1(X0)
| c9_2(X0,a1313)
| c4_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314)
| c6_2(X0,a1360)
| c1_2(X0,a1359) ) ).
cnf(u3662,negated_conjecture,
( ~ c10_1(X0)
| c5_2(X0,a1345)
| c1_2(X0,a1344)
| c5_2(X0,a1246) ) ).
cnf(clause71,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause262,negated_conjecture,
( ~ c7_2(X0,a1279)
| ssSkP4(X0) ) ).
cnf(u3054,negated_conjecture,
c3_2(a1200,a1351) ).
cnf(u5172,negated_conjecture,
( ~ c1_1(X0)
| c3_2(X0,a1313)
| c4_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314)
| c4_1(X0)
| c4_2(X0,a1348) ) ).
cnf(clause179,negated_conjecture,
( ssSkP1(X0)
| c10_2(X0,a1221) ) ).
cnf(u2745,negated_conjecture,
ndr1_1(X0) ).
cnf(u3994,negated_conjecture,
( c8_1(X0)
| c10_2(X0,a1352)
| c10_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313) ) ).
cnf(u2939,negated_conjecture,
c1_2(a1226,a1313) ).
cnf(u3609,negated_conjecture,
( c7_1(X0)
| c3_2(X0,a1351)
| c10_2(X0,a1352)
| c8_1(X0) ) ).
cnf(u3062,negated_conjecture,
( c10_2(X0,a1314)
| c5_2(X0,a1246)
| c1_2(X0,a1313) ) ).
cnf(u4063,negated_conjecture,
( ~ c8_2(X0,a1348)
| c3_2(X0,a1313)
| c4_2(X0,a1313)
| c5_1(X0)
| c5_2(X0,a1246)
| c4_2(X0,a1314) ) ).
cnf(clause137,negated_conjecture,
( ssSkP10(X0)
| c6_2(X0,a1355) ) ).
cnf(u4937,negated_conjecture,
( c3_1(X0)
| c9_2(X0,a1313)
| c4_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314)
| c1_2(X0,a1356)
| c6_2(X0,a1355) ) ).
cnf(u5045,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,a1351)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u3338,negated_conjecture,
c8_2(a1353,a1351) ).
cnf(u3261,negated_conjecture,
( ~ c4_1(X0)
| c10_2(X0,a1351)
| c6_1(X0)
| c10_2(X0,a1352) ) ).
cnf(clause265,negated_conjecture,
( ~ c3_2(X0,a1233)
| ssSkP2(X0) ) ).
cnf(u5147,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c9_2(X0,a1355)
| c8_2(X0,X1)
| c1_2(X0,a1356) ) ).
cnf(clause261,negated_conjecture,
( ~ c2_2(X0,a1279)
| ssSkP4(X0) ) ).
cnf(u3635,negated_conjecture,
( c7_1(X0)
| c10_2(X0,a1351)
| c10_2(X0,a1352)
| c8_1(X0) ) ).
cnf(u3056,negated_conjecture,
c10_2(a1200,a1351) ).
cnf(u2824,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,a1312)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u4348,negated_conjecture,
( ~ c7_1(X0)
| c10_2(X0,a1314)
| c3_2(X0,a1351)
| c1_2(X0,a1313)
| ~ c10_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u5145,negated_conjecture,
( ~ ssSkP5(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,X1) ) ).
cnf(u5151,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c1_2(X0,a1359)
| c8_2(X0,X1)
| c6_2(X0,a1360) ) ).
cnf(u5144,negated_conjecture,
( ~ ssSkP5(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c10_2(X0,a1314)
| c8_2(X0,X1) ) ).
cnf(u5047,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c4_2(X0,a1314)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u2820,negated_conjecture,
( ~ c4_2(X0,a1312)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ c1_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u3190,negated_conjecture,
( ~ c7_1(X0)
| c1_2(X0,a1359)
| ~ c10_1(X0)
| c6_2(X0,a1360) ) ).
cnf(u3339,negated_conjecture,
c10_2(a1353,a1351) ).
cnf(u5161,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c4_2(X0,a1314)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u3059,negated_conjecture,
( c2_1(X0)
| c10_2(X0,a1352)
| c8_2(X0,a1351) ) ).
cnf(u3199,negated_conjecture,
( c3_1(X0)
| c3_2(X0,a1351)
| c7_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u4350,negated_conjecture,
( ~ c7_1(X0)
| c4_2(X0,a1314)
| c3_2(X0,a1351)
| c1_2(X0,a1313)
| ~ c10_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u5230,negated_conjecture,
( c10_2(X0,a1352)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,X1)
| c1_2(X0,a1313) ) ).
cnf(u3742,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1352)
| c8_1(X0)
| c10_2(X0,a1314)
| c10_2(X0,a1351) ) ).
cnf(u5106,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c7_2(X0,a1359)
| c8_2(X0,X1)
| c6_2(X0,a1360) ) ).
cnf(u5043,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c4_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(clause144,negated_conjecture,
( ssSkP8(X0)
| c9_2(X0,a1344) ) ).
cnf(u2796,negated_conjecture,
c6_1(a1214) ).
cnf(clause135,negated_conjecture,
( ssSkP11(X0)
| c7_2(X0,a1359) ) ).
cnf(clause151,negated_conjecture,
( ssSkP6(X0)
| c3_2(X0,a1318) ) ).
cnf(u5118,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c10_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u3997,negated_conjecture,
( c8_1(X0)
| c10_2(X0,a1352)
| c4_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313) ) ).
cnf(u5102,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c6_2(X0,a1355)
| c8_2(X0,X1)
| c1_2(X0,a1356) ) ).
cnf(u5242,negated_conjecture,
( c10_2(X0,a1352)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c10_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,X1)
| c1_2(X0,a1313) ) ).
cnf(clause140,negated_conjecture,
( ssSkP9(X0)
| c10_2(X0,a1351) ) ).
cnf(u3988,negated_conjecture,
( c8_1(X0)
| c10_2(X0,a1352)
| c10_2(X0,a1314)
| c8_2(X0,a1351)
| c1_2(X0,a1313) ) ).
cnf(clause134,negated_conjecture,
( ssSkP11(X0)
| c1_2(X0,a1359) ) ).
cnf(u3031,negated_conjecture,
( c8_1(X0)
| c1_2(X0,a1356)
| c6_2(X0,a1355) ) ).
cnf(u4640,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,a1313)
| c9_2(X0,a1313)
| c3_1(X0)
| c5_2(X0,a1246)
| c4_2(X0,a1314) ) ).
cnf(clause255,negated_conjecture,
( ~ c8_2(X0,a1318)
| ssSkP6(X0) ) ).
cnf(clause92,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(clause61,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u5034,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c4_2(X0,a1344) ) ).
cnf(u4358,negated_conjecture,
( ~ c7_1(X0)
| c4_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313)
| ~ c10_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u3544,negated_conjecture,
( ~ c10_1(X0)
| c7_2(X0,a1359)
| c6_2(X0,a1360)
| c5_2(X0,a1246) ) ).
cnf(u2764,negated_conjecture,
c8_1(a1333) ).
cnf(u4626,negated_conjecture,
( c7_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351) ) ).
cnf(u4625,negated_conjecture,
( c7_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351) ) ).
cnf(u3163,negated_conjecture,
( ~ c7_1(X0)
| c9_2(X0,a1355)
| ~ c10_1(X0)
| c1_2(X0,a1356) ) ).
cnf(u3262,negated_conjecture,
( c5_1(X0)
| c10_2(X0,a1351)
| c10_2(X0,a1352)
| c4_1(X0) ) ).
cnf(u5108,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c4_2(X0,a1344) ) ).
cnf(u3283,negated_conjecture,
( ~ c7_1(X0)
| c5_2(X0,a1345)
| ~ c10_1(X0)
| c9_2(X0,a1344) ) ).
cnf(u3037,negated_conjecture,
( c8_1(X0)
| c6_2(X0,a1360)
| c7_2(X0,a1359) ) ).
cnf(u3092,negated_conjecture,
( c8_1(X0)
| c1_2(X0,a1344)
| c5_2(X0,a1345) ) ).
cnf(u3285,negated_conjecture,
( ~ c7_1(X0)
| c5_2(X0,a1345)
| ~ c10_1(X0)
| c1_2(X0,a1344) ) ).
cnf(u5117,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c4_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u5239,negated_conjecture,
( c10_2(X0,a1314)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c10_2(X0,a1351)
| c6_2(X0,X1)
| c8_2(X0,X1)
| c1_2(X0,a1313) ) ).
cnf(u3636,negated_conjecture,
( ~ c10_1(X0)
| c5_2(X0,a1345)
| c4_2(X0,a1344)
| c5_2(X0,a1246) ) ).
cnf(u5027,negated_conjecture,
( ~ ssSkP5(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,X1) ) ).
cnf(u3242,negated_conjecture,
( c3_1(X0)
| c8_2(X0,a1351)
| c7_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u5101,negated_conjecture,
( ~ ssSkP5(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c4_2(X0,a1314)
| c8_2(X0,X1) ) ).
cnf(u3442,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,a1355)
| c1_2(X0,a1356)
| c5_2(X0,a1246) ) ).
cnf(u2763,negated_conjecture,
c8_1(a1214) ).
cnf(u3240,negated_conjecture,
( ~ c4_1(X0)
| c8_2(X0,a1351)
| c6_1(X0)
| c10_2(X0,a1352) ) ).
cnf(clause252,negated_conjecture,
( ~ c8_2(X0,a1325)
| ssSkP7(X0) ) ).
cnf(u2941,negated_conjecture,
c1_2(a1220,a1313) ).
cnf(u5119,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c4_2(X0,a1314)
| c1_2(X0,a1313)
| c8_2(X0,X1) ) ).
cnf(u3032,negated_conjecture,
( c8_1(X0)
| c1_2(X0,a1356)
| c9_2(X0,a1355) ) ).
cnf(u5103,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c8_2(X0,a1351)
| c9_2(X0,a1355)
| c8_2(X0,X1)
| c1_2(X0,a1356) ) ).
cnf(u5036,negated_conjecture,
( ~ c10_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c5_2(X0,a1345)
| c8_2(X0,X1)
| c1_2(X0,a1344) ) ).
cnf(clause256,negated_conjecture,
( ~ c2_2(X0,a1313)
| ssSkP5(X0) ) ).
cnf(u4352,negated_conjecture,
( ~ c7_1(X0)
| c10_2(X0,a1314)
| c8_2(X0,a1351)
| c1_2(X0,a1313)
| ~ c10_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u2821,negated_conjecture,
( ~ c3_2(X0,a1312)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ c1_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u3337,negated_conjecture,
c3_2(a1353,a1351) ).
cnf(u2989,negated_conjecture,
c5_2(a1220,a1300) ).
cnf(u3690,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1352)
| c8_1(X0)
| c10_2(X0,a1314)
| c3_2(X0,a1351) ) ).
cnf(u3038,negated_conjecture,
( c8_1(X0)
| c6_2(X0,a1360)
| c1_2(X0,a1359) ) ).
cnf(u5026,negated_conjecture,
( ~ ssSkP5(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a1352)
| c3_2(X0,a1351)
| c10_2(X0,a1314)
| c8_2(X0,X1) ) ).
cnf(u2943,negated_conjecture,
c1_2(a1363,a1313) ).
cnf(u3728,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1352)
| c8_1(X0)
| c4_2(X0,a1314)
| c8_2(X0,a1351) ) ).
cnf(clause152,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a1313) ) ).
cnf(u4356,negated_conjecture,
( ~ c7_1(X0)
| c10_2(X0,a1314)
| c10_2(X0,a1351)
| c1_2(X0,a1313)
| ~ c10_1(X0)
| c10_2(X0,a1352) ) ).
cnf(u3743,negated_conjecture,
( ~ ssSkP5(X0)
| c10_2(X0,a1352)
| c8_1(X0)
| c4_2(X0,a1314)
| c10_2(X0,a1351) ) ).
cnf(u3651,negated_conjecture,
( ~ c10_1(X0)
| c5_2(X0,a1345)
| c9_2(X0,a1344)
| c5_2(X0,a1246) ) ).
cnf(u3991,negated_conjecture,
( c8_1(X0)
| c10_2(X0,a1352)
| c4_2(X0,a1314)
| c8_2(X0,a1351)
| c1_2(X0,a1313) ) ).
cnf(clause145,negated_conjecture,
( ssSkP8(X0)
| c4_2(X0,a1344) ) ).
cnf(u4938,negated_conjecture,
( c3_1(X0)
| c9_2(X0,a1313)
| c4_2(X0,a1313)
| c5_2(X0,a1246)
| c4_2(X0,a1314)
| c1_2(X0,a1356)
| c9_2(X0,a1355) ) ).
cnf(u2744,negated_conjecture,
( c2_1(X0)
| ndr1_1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN425-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n001.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 16:02:18 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 4.92/1.53 % (458531)Input is clausal, will run a generic CNF schedule.
% 4.92/1.53 % (458538)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=273186758:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.92/1.53 % (458539)lrs+10_1_sil=8000:sp=occurrence:random_seed=1811439107:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.92/1.53 % (458536)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=3032921918:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.92/1.53 % (458541)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3378786261:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.92/1.53 % (458537)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4115225195:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.92/1.53 % (458540)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2478681943:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.92/1.53 % (458542)dis-21_1_sil=8000:lcm=predicate:random_seed=2163700659:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 4.92/1.53 % (458541)Refutation not found, incomplete strategy
% 4.92/1.53 % (458541)------------------------------
% 4.92/1.53 % (458541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458541)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458541)Termination reason: Refutation not found, incomplete strategy
% 4.92/1.53 % (458541)Time elapsed: 0.036 s
% 4.92/1.53 % (458541)Peak memory usage: 90 MB
% 4.92/1.53 % (458541)Instructions burned: 59 (million)
% 4.92/1.53 % (458539)Instruction limit reached!
% 4.92/1.53 % (458539)------------------------------
% 4.92/1.53 % (458539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458539)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458539)Termination reason: Instruction limit
% 4.92/1.53 % (458539)Termination phase: Saturation
% 4.92/1.53 % (458539)Time elapsed: 0.060 s
% 4.92/1.53 % (458539)Peak memory usage: 90 MB
% 4.92/1.53 % (458539)Instructions burned: 107 (million)
% 4.92/1.53 % (458540)Instruction limit reached!
% 4.92/1.53 % (458540)------------------------------
% 4.92/1.53 % (458540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458540)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458540)Termination reason: Instruction limit
% 4.92/1.53 % (458540)Termination phase: Saturation
% 4.92/1.53 % (458540)Time elapsed: 0.066 s
% 4.92/1.53 % (458540)Peak memory usage: 90 MB
% 4.92/1.53 % (458540)Instructions burned: 115 (million)
% 4.92/1.53 % (458542)Instruction limit reached!
% 4.92/1.53 % (458542)------------------------------
% 4.92/1.53 % (458542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458542)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458542)Termination reason: Instruction limit
% 4.92/1.53 % (458542)Termination phase: Saturation
% 4.92/1.53 % (458542)Time elapsed: 0.067 s
% 4.92/1.53 % (458542)Peak memory usage: 90 MB
% 4.92/1.53 % (458542)Instructions burned: 118 (million)
% 4.92/1.53 % (458550)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=205915357:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.92/1.53 % (458552)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3593915041:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.92/1.53 % (458551)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1550394204:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.92/1.53 % (458551)Refutation not found, incomplete strategy
% 4.92/1.53 % (458551)------------------------------
% 4.92/1.53 % (458551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458551)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458551)Termination reason: Refutation not found, incomplete strategy
% 4.92/1.53 % (458551)Time elapsed: 0.033 s
% 4.92/1.53 % (458551)Peak memory usage: 90 MB
% 4.92/1.53 % (458551)Instructions burned: 58 (million)
% 4.92/1.53 % (458550)Instruction limit reached!
% 4.92/1.53 % (458550)------------------------------
% 4.92/1.53 % (458550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458550)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458550)Termination reason: Instruction limit
% 4.92/1.53 % (458550)Termination phase: Saturation
% 4.92/1.53 % (458550)Time elapsed: 0.078 s
% 4.92/1.53 % (458550)Peak memory usage: 91 MB
% 4.92/1.53 % (458550)Instructions burned: 144 (million)
% 4.92/1.53 % (458541)------------------------------
% 4.92/1.53 % (458541)------------------------------
% 4.92/1.53 % (458552)Instruction limit reached!
% 4.92/1.53 % (458552)------------------------------
% 4.92/1.53 % (458552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458552)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458552)Termination reason: Instruction limit
% 4.92/1.53 % (458552)Termination phase: Saturation
% 4.92/1.53 % (458552)Time elapsed: 0.120 s
% 4.92/1.53 % (458552)Peak memory usage: 92 MB
% 4.92/1.53 % (458552)Instructions burned: 219 (million)
% 4.92/1.53 % (458556)lrs+10_64_to=lpo:sil=8000:random_seed=3277451204:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 4.92/1.53 % (458557)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3956018745:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 4.92/1.53 % (458557)Refutation not found, incomplete strategy
% 4.92/1.53 % (458557)------------------------------
% 4.92/1.53 % (458557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458557)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458557)Termination reason: Refutation not found, incomplete strategy
% 4.92/1.53 % (458557)Time elapsed: 0.028 s
% 4.92/1.53 % (458557)Peak memory usage: 90 MB
% 4.92/1.53 % (458557)Instructions burned: 45 (million)
% 4.92/1.53 % (458556)First to succeed.
% 4.92/1.53 % (458556)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-458531"
% 4.92/1.53 % (458558)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=297385316:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 4.92/1.53 % (458551)------------------------------
% 4.92/1.53 % (458551)------------------------------
% 4.92/1.53 % (458558)Also succeeded, but the first one will report.
% 4.92/1.53 % (458562)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3455084554:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 4.92/1.53 % (458557)------------------------------
% 4.92/1.53 % (458557)------------------------------
% 4.92/1.53 % (458537)Refutation not found, incomplete strategy
% 4.92/1.53 % (458537)------------------------------
% 4.92/1.53 % (458537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.53 % (458537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.53 % (458537)CaDiCaL version: 2.1.3
% 4.92/1.53 % (458537)Termination reason: Refutation not found, incomplete strategy
% 4.92/1.53 % (458537)Time elapsed: 0.679 s
% 4.92/1.53 % (458537)Peak memory usage: 133 MB
% 4.92/1.53 % (458537)Instructions burned: 1049 (million)
% 4.92/1.53 % SZS status Satisfiable for theBenchmark
% 4.92/1.53 % SZS output start Saturation.
% See solution above
% 6.63/1.73 % SZS output start Definitions and Model Updates.
% 6.63/1.73 for all inputs,
% 6.63/1.73 define ssSkC13 := $true
% 6.63/1.73 for all inputs,
% 6.63/1.73 define ssSkC12 := $true
% 6.63/1.73 for all inputs,
% 6.63/1.73 define ssSkC0 := $true
% 6.63/1.73 for all inputs,
% 6.63/1.73 define ssSkP3(X0) := $true
% 6.63/1.73 for all inputs,
% 6.63/1.73 define ssSkP0(X0) := $true
% 6.63/1.73 for all inputs,
% 6.63/1.73 define ssSkC2 := $true
% 6.63/1.73 % SZS output end Definitions and Model Updates.
% 6.63/1.73 % (458556)------------------------------
% 6.63/1.73 % (458556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.63/1.73 % (458556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.63/1.73 % (458556)CaDiCaL version: 2.1.3
% 6.63/1.73 % (458556)Termination reason: Satisfiable
% 6.63/1.73 % (458556)Time elapsed: 0.062 s
% 6.63/1.73 % (458556)Peak memory usage: 91 MB
% 6.63/1.73 % (458556)Instructions burned: 106 (million)
% 6.63/1.73 % (458556)------------------------------
% 6.63/1.73 % (458556)------------------------------
% 6.63/1.73 % (458531)Success in time 0.856 s
% 6.63/1.73 % Vampire exiting
%------------------------------------------------------------------------------