%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 : Satisfiable 7.04s 1.43s
% Output : Saturation 8.04s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u537,negated_conjecture,
ndr1_0 ).
cnf(u541,negated_conjecture,
( ~ c4_2(X0,X2)
| ~ c5_1(X0)
| ~ c1_2(X0,X2)
| ~ c2_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u559,negated_conjecture,
( ~ c2_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,X1)
| c4_2(X0,X4)
| c1_2(X0,X4)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u567,negated_conjecture,
~ c1_0 ).
cnf(u571,negated_conjecture,
ndr1_1(a1504) ).
cnf(u575,negated_conjecture,
( ~ c4_2(a1504,X2)
| c5_2(a1504,X2)
| ~ c3_2(a1504,X2) ) ).
cnf(u578,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u582,negated_conjecture,
~ c2_0 ).
cnf(u590,negated_conjecture,
( ~ c4_2(X0,X2)
| c5_2(X0,X2)
| c2_2(X0,X2)
| c2_2(X0,X1)
| ~ c1_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u597,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c2_1(X0)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u616,negated_conjecture,
~ c5_0 ).
cnf(u623,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ~ c5_1(X0) ) ).
cnf(u644,negated_conjecture,
( ~ c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u659,negated_conjecture,
~ c4_0 ).
cnf(u669,negated_conjecture,
( ~ ndr1_1(X1)
| c2_1(X1)
| c3_2(X1,X2)
| c5_2(X1,X2)
| c4_2(X1,X2)
| ~ c5_2(X1,a1379) ) ).
cnf(u676,negated_conjecture,
( ~ ndr1_1(X1)
| c2_1(X1)
| c3_2(X1,X2)
| c5_2(X1,X2)
| c4_2(X1,X2)
| ~ c1_2(X1,a1379) ) ).
cnf(u700,negated_conjecture,
c3_0 ).
cnf(u708,negated_conjecture,
( ~ c2_2(X0,X1)
| c1_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u715,negated_conjecture,
( ~ c5_2(X0,X1)
| c5_1(X0)
| c3_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u718,negated_conjecture,
ssSkC30 ).
cnf(u735,negated_conjecture,
( ~ ndr1_1(X1)
| c2_1(X1)
| c2_2(X1,a1379)
| c3_2(X1,X2)
| c5_2(X1,X2)
| c4_2(X1,X2) ) ).
cnf(u780,negated_conjecture,
~ ssSkC28 ).
cnf(u791,negated_conjecture,
( ~ ssSkP3(X0)
| c1_1(X0)
| c1_2(X0,a1358) ) ).
cnf(u795,negated_conjecture,
( ~ ssSkP3(X0)
| c1_1(X0)
| c2_2(X0,a1358) ) ).
cnf(u799,negated_conjecture,
( ~ ssSkP3(X0)
| c1_1(X0)
| c3_2(X0,a1358) ) ).
cnf(u807,negated_conjecture,
( ~ c2_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u817,negated_conjecture,
~ c4_1(a1504) ).
cnf(u821,negated_conjecture,
c1_1(a1504) ).
cnf(u827,negated_conjecture,
ssSkC10 ).
cnf(u839,negated_conjecture,
ssSkC14 ).
cnf(u850,negated_conjecture,
( ~ ssSkP3(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u876,negated_conjecture,
( ~ c1_2(X0,a1459)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u880,negated_conjecture,
( ~ c3_2(X0,a1459)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u888,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_1(X0)
| c4_2(X0,a1413)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u892,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_1(X0)
| c5_2(X0,a1413)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u897,negated_conjecture,
ssSkC23 ).
cnf(u904,negated_conjecture,
~ ssSkC35 ).
cnf(u908,negated_conjecture,
( ~ c4_2(X0,a1523)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u912,negated_conjecture,
( ~ c5_2(X0,a1523)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u916,negated_conjecture,
( ~ c2_2(X0,a1523)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u924,negated_conjecture,
( ~ c4_2(X0,a1505)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u929,negated_conjecture,
~ c4_1(a1346) ).
cnf(u950,negated_conjecture,
~ ssSkC18 ).
cnf(u954,negated_conjecture,
( ~ c3_2(X0,X1)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u971,negated_conjecture,
ssSkC29 ).
cnf(u978,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,a1505)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u982,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_2(X0,a1505)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u989,negated_conjecture,
( ~ c1_1(X0)
| c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u994,negated_conjecture,
c2_1(a1346) ).
cnf(u999,negated_conjecture,
c3_1(a1346) ).
cnf(u1039,negated_conjecture,
( ~ ndr1_1(X0)
| c1_1(X0)
| c3_2(X0,a1492)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u1043,negated_conjecture,
( ~ ndr1_1(X0)
| c1_1(X0)
| c5_2(X0,a1492)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u1047,negated_conjecture,
( ~ c4_2(X0,X1)
| c4_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1059,negated_conjecture,
ndr1_1(a1333) ).
cnf(u1063,negated_conjecture,
( ~ c1_2(a1333,X0)
| c4_2(a1333,X0)
| ~ c3_2(a1333,X0) ) ).
cnf(u1080,negated_conjecture,
ssSkC34 ).
cnf(u1099,negated_conjecture,
ndr1_1(a1409) ).
cnf(u1103,negated_conjecture,
( ~ c4_2(a1409,X0)
| ~ c5_2(a1409,X0)
| ~ c1_2(a1409,X0) ) ).
cnf(u1122,negated_conjecture,
ssSkC24 ).
cnf(u1131,negated_conjecture,
ndr1_1(a1482) ).
cnf(u1135,negated_conjecture,
( ~ c1_2(a1482,X0)
| c3_2(a1482,X0)
| ~ c5_2(a1482,X0) ) ).
cnf(u1138,negated_conjecture,
ssSkC25 ).
cnf(u1143,negated_conjecture,
( ~ c1_2(X0,a1489)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1147,negated_conjecture,
ndr1_1(a1503) ).
cnf(u1151,negated_conjecture,
( ~ c1_2(a1503,X0)
| c5_2(a1503,X0)
| ~ c2_2(a1503,X0) ) ).
cnf(u1154,negated_conjecture,
ssSkC32 ).
cnf(u1158,negated_conjecture,
ssSkC31 ).
cnf(u1172,negated_conjecture,
ssSkC19 ).
cnf(u1190,negated_conjecture,
ssSkC4 ).
cnf(u1199,negated_conjecture,
ndr1_1(a1436) ).
cnf(u1203,negated_conjecture,
( ~ c2_2(a1436,X0)
| c5_2(a1436,X0)
| c3_2(a1436,X0) ) ).
cnf(u1207,negated_conjecture,
( ~ c2_2(a1436,X0)
| c4_2(a1436,X0)
| c1_2(a1436,X0) ) ).
cnf(u1211,negated_conjecture,
ndr1_1(a1442) ).
cnf(u1215,negated_conjecture,
( ~ c2_2(a1442,X0)
| c4_2(a1442,X0)
| c3_2(a1442,X0) ) ).
cnf(u1220,negated_conjecture,
~ ndr1_1(a1446) ).
cnf(u1223,negated_conjecture,
( ~ c1_2(a1446,X0)
| c3_2(a1446,X0)
| ~ c5_2(a1446,X0) ) ).
cnf(u1227,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c3_2(X0,a1489)
| c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1239,negated_conjecture,
~ ssSkC5 ).
cnf(u1243,negated_conjecture,
ndr1_1(a1359) ).
cnf(u1247,negated_conjecture,
( ~ c3_2(a1359,X0)
| c5_2(a1359,X0)
| c1_2(a1359,X0) ) ).
cnf(u1252,negated_conjecture,
ssSkC6 ).
cnf(u1267,negated_conjecture,
~ ssSkC26 ).
cnf(u1272,negated_conjecture,
~ ndr1_1(a1483) ).
cnf(u1280,negated_conjecture,
~ ndr1_1(a1490) ).
cnf(u1299,negated_conjecture,
( ~ c4_2(a1409,X0)
| c2_2(a1409,X0)
| c1_2(a1409,X0) ) ).
cnf(u1303,negated_conjecture,
ndr1_1(a1424) ).
cnf(u1307,negated_conjecture,
( ~ c4_2(a1424,X0)
| c3_2(a1424,X0)
| c1_2(a1424,X0) ) ).
cnf(u1311,negated_conjecture,
( c1_2(a1498,X0)
| c5_2(a1498,X0)
| c4_2(a1498,X0) ) ).
cnf(u1314,negated_conjecture,
ndr1_1(a1498) ).
cnf(u1328,negated_conjecture,
~ c5_2(a1510,a1511) ).
cnf(u1336,negated_conjecture,
~ c1_2(a1510,a1511) ).
cnf(u1341,negated_conjecture,
~ c2_2(a1510,a1511) ).
cnf(u1346,negated_conjecture,
ssSkC11 ).
cnf(u1357,negated_conjecture,
~ ndr1_1(a1434) ).
cnf(u1361,negated_conjecture,
ndr1_1(a1363) ).
cnf(u1365,negated_conjecture,
( ~ c3_2(a1363,X0)
| c2_2(a1363,X0) ) ).
cnf(u1370,negated_conjecture,
ssSkC9 ).
cnf(u1373,negated_conjecture,
ndr1_1(a1388) ).
cnf(u1389,negated_conjecture,
( ~ c4_2(X0,a1341)
| c2_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u1397,negated_conjecture,
ssSkC22 ).
cnf(u1409,negated_conjecture,
ndr1_1(a1494) ).
cnf(u1413,negated_conjecture,
( ~ c5_2(a1494,X0)
| c1_2(a1494,X0)
| c3_2(a1494,X0) ) ).
cnf(u1417,negated_conjecture,
( ~ c2_2(a1494,X0)
| c3_2(a1494,X0)
| c1_2(a1494,X0) ) ).
cnf(u1433,negated_conjecture,
( ~ c4_2(a1498,X0)
| c5_2(a1498,X0) ) ).
cnf(u1450,negated_conjecture,
ssSkC2 ).
cnf(u1461,negated_conjecture,
~ ssSkC16 ).
cnf(u1465,negated_conjecture,
ndr1_1(a1428) ).
cnf(u1469,negated_conjecture,
( ~ c1_2(a1428,X0)
| c2_2(a1428,X0) ) ).
cnf(u1481,negated_conjecture,
ndr1_1(a1499) ).
cnf(u1497,negated_conjecture,
( ~ ssSkP2(X0)
| c2_1(X0)
| c5_2(X0,a1341) ) ).
cnf(u1501,negated_conjecture,
( ~ c5_2(X0,a1374)
| c1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1505,negated_conjecture,
( ~ c1_2(X0,a1374)
| c1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1509,negated_conjecture,
( ~ c1_2(X0,a1410)
| c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1518,negated_conjecture,
c5_1(a1510) ).
cnf(u1523,negated_conjecture,
ndr1_1(a1510) ).
cnf(u1536,negated_conjecture,
ssSkC0 ).
cnf(u1547,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| c3_2(X0,a1324) ) ).
cnf(u1552,negated_conjecture,
ssSkC8 ).
cnf(u1555,negated_conjecture,
( ~ c2_2(X0,a1377)
| ~ ssSkP6(X0)
| ~ ssSkP7(X0) ) ).
cnf(u1559,negated_conjecture,
( ~ c3_2(X0,a1377)
| ~ ssSkP6(X0)
| ~ ssSkP7(X0) ) ).
cnf(u1571,negated_conjecture,
( c1_2(a1378,X0)
| c5_2(a1378,X0) ) ).
cnf(u1574,negated_conjecture,
ndr1_1(a1378) ).
cnf(u1591,negated_conjecture,
( c1_2(a1493,X0)
| c2_2(a1493,X0) ) ).
cnf(u1594,negated_conjecture,
ndr1_1(a1493) ).
cnf(u1615,negated_conjecture,
( ~ ssSkP2(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u1619,negated_conjecture,
( ~ ssSkP5(X0)
| c1_1(X0)
| c4_2(X0,a1374) ) ).
cnf(u1623,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| c5_2(X0,a1410) ) ).
cnf(u1627,negated_conjecture,
( c3_1(X0)
| c2_1(X0)
| c5_2(X0,a1414) ) ).
cnf(u1631,negated_conjecture,
( c3_1(X0)
| c2_1(X0)
| c4_2(X0,a1414) ) ).
cnf(u1635,negated_conjecture,
( c3_1(X0)
| c2_1(X0)
| c2_2(X0,a1414) ) ).
cnf(u1647,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1651,negated_conjecture,
( ~ ssSkP6(X0)
| c5_2(X0,a1377)
| ~ ssSkP7(X0) ) ).
cnf(u1666,negated_conjecture,
ssSkC17 ).
cnf(u1671,negated_conjecture,
ndr1_1(a1458) ).
cnf(u1675,negated_conjecture,
( ~ c4_2(a1458,X0)
| c1_2(a1458,X0) ) ).
cnf(u1679,negated_conjecture,
( c5_2(a1475,X0)
| c2_2(a1475,X0) ) ).
cnf(u1682,negated_conjecture,
ndr1_1(a1475) ).
cnf(u1691,negated_conjecture,
( ~ ssSkP5(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u1695,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u1699,negated_conjecture,
( ndr1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ).
cnf(u1719,negated_conjecture,
( c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u1731,negated_conjecture,
( c3_2(a1458,X0)
| c2_2(a1458,X0) ) ).
cnf(u1750,negated_conjecture,
~ c1_2(a1333,a1334) ).
cnf(u1755,negated_conjecture,
~ c2_2(a1363,a1364) ).
cnf(u1825,negated_conjecture,
~ c3_2(a1439,a1440) ).
cnf(u1830,negated_conjecture,
~ c4_2(a1439,a1440) ).
cnf(u1848,negated_conjecture,
ssSkC20 ).
cnf(u1854,negated_conjecture,
~ c1_2(a1452,a1453) ).
cnf(u1913,negated_conjecture,
c4_2(a1333,a1334) ).
cnf(u1918,negated_conjecture,
c5_2(a1333,a1334) ).
cnf(u1923,negated_conjecture,
~ c4_1(a1337) ).
cnf(u1928,negated_conjecture,
~ c5_1(a1337) ).
cnf(u1933,negated_conjecture,
~ c2_1(a1363) ).
cnf(u1938,negated_conjecture,
c1_2(a1363,a1364) ).
cnf(u1943,negated_conjecture,
c5_2(a1363,a1364) ).
cnf(u2013,negated_conjecture,
~ c2_2(a1436,a1437) ).
cnf(u2018,negated_conjecture,
~ c4_2(a1436,a1437) ).
cnf(u2023,negated_conjecture,
c3_2(a1439,a1441) ).
cnf(u2028,negated_conjecture,
c5_2(a1439,a1441) ).
cnf(u2033,negated_conjecture,
c1_2(a1439,a1441) ).
cnf(u2038,negated_conjecture,
~ c5_1(a1452) ).
cnf(u2043,negated_conjecture,
c2_2(a1452,a1453) ).
cnf(u2048,negated_conjecture,
~ c4_2(a1455,a1456) ).
cnf(u2051,negated_conjecture,
ssSkC21 ).
cnf(u2057,negated_conjecture,
~ c3_2(a1455,a1456) ).
cnf(u2062,negated_conjecture,
~ c2_2(a1455,a1457) ).
cnf(u2117,negated_conjecture,
~ c3_2(a1359,a1360) ).
cnf(u2122,negated_conjecture,
~ c1_2(a1359,a1360) ).
cnf(u2127,negated_conjecture,
~ c2_2(a1359,a1360) ).
cnf(u2132,negated_conjecture,
~ c3_2(a1428,a1429) ).
cnf(u2182,negated_conjecture,
ssSkC27 ).
cnf(u2223,negated_conjecture,
c1_1(a1333) ).
cnf(u2245,negated_conjecture,
~ c3_1(a1378) ).
cnf(u2296,negated_conjecture,
c1_2(a1436,a1437) ).
cnf(u2301,negated_conjecture,
c3_1(a1439) ).
cnf(u2306,negated_conjecture,
ndr1_1(a1439) ).
cnf(u2316,negated_conjecture,
ndr1_1(a1452) ).
cnf(u2321,negated_conjecture,
c2_2(a1455,a1456) ).
cnf(u2326,negated_conjecture,
c3_2(a1455,a1457) ).
cnf(u2331,negated_conjecture,
c5_2(a1455,a1457) ).
cnf(u2337,negated_conjecture,
~ c5_1(a1482) ).
cnf(u2342,negated_conjecture,
c5_2(a1487,a1488) ).
cnf(u2347,negated_conjecture,
c4_2(a1487,a1488) ).
cnf(u2352,negated_conjecture,
c2_2(a1487,a1488) ).
cnf(u2357,negated_conjecture,
~ c2_1(a1493) ).
cnf(u2362,negated_conjecture,
~ c5_1(a1498) ).
cnf(u2367,negated_conjecture,
~ c3_1(a1503) ).
cnf(u2372,negated_conjecture,
~ c5_1(a1503) ).
cnf(u2386,negated_conjecture,
c2_1(a1516) ).
cnf(u2391,negated_conjecture,
~ ssSkC33 ).
cnf(u2430,negated_conjecture,
c1_1(a1388) ).
cnf(u2436,negated_conjecture,
c2_2(a1428,a1429) ).
cnf(u2441,negated_conjecture,
c4_2(a1428,a1429) ).
cnf(u2481,negated_conjecture,
~ c3_1(a1483) ).
cnf(u2521,negated_conjecture,
~ c5_1(a1499) ).
cnf(u2526,negated_conjecture,
~ c3_1(a1499) ).
cnf(u2551,negated_conjecture,
~ c4_1(a1325) ).
cnf(u2556,negated_conjecture,
~ c1_1(a1325) ).
cnf(u2566,negated_conjecture,
~ c2_1(a1350) ).
cnf(u2571,negated_conjecture,
~ c5_1(a1361) ).
cnf(u2575,negated_conjecture,
c1_1(a1361) ).
cnf(u2581,negated_conjecture,
~ c3_1(a1409) ).
cnf(u2586,negated_conjecture,
~ c1_1(a1424) ).
cnf(u2592,negated_conjecture,
c2_1(a1442) ).
cnf(u2597,negated_conjecture,
c3_1(a1442) ).
cnf(u2602,negated_conjecture,
~ c3_1(a1446) ).
cnf(u2607,negated_conjecture,
~ c5_1(a1446) ).
cnf(u2612,negated_conjecture,
c1_1(a1455) ).
cnf(u2617,negated_conjecture,
ndr1_1(a1455) ).
cnf(u2622,negated_conjecture,
~ c5_1(a1475) ).
cnf(u2627,negated_conjecture,
c1_1(a1487) ).
cnf(u2631,negated_conjecture,
~ c3_1(a1487) ).
cnf(u2637,negated_conjecture,
ndr1_1(a1487) ).
cnf(u2648,negated_conjecture,
c5_1(a1516) ).
cnf(u2656,negated_conjecture,
c2_1(a1359) ).
cnf(u2667,negated_conjecture,
c2_1(a1428) ).
cnf(u2683,negated_conjecture,
c2_1(a1434) ).
cnf(u2718,negated_conjecture,
c1_1(a1483) ).
cnf(u2739,negated_conjecture,
c1_1(a1515) ).
cnf(u2744,negated_conjecture,
c3_1(a1515) ).
cnf(u2751,negated_conjecture,
c2_1(a1325) ).
cnf(u2756,negated_conjecture,
c5_1(a1350) ).
cnf(u2761,negated_conjecture,
c4_1(a1424) ).
cnf(u2766,negated_conjecture,
c4_1(a1475) ).
cnf(u3114,negated_conjecture,
~ c3_1(a1333) ).
cnf(u3118,negated_conjecture,
~ c2_1(a1333) ).
cnf(u3123,negated_conjecture,
~ c3_1(a1455) ).
cnf(u3127,negated_conjecture,
~ c2_1(a1455) ).
cnf(u3139,negated_conjecture,
~ c5_1(a1424) ).
cnf(u3143,negated_conjecture,
c3_1(a1424) ).
cnf(u3154,negated_conjecture,
~ c5_1(a1464) ).
cnf(u3171,negated_conjecture,
~ c4_1(a1333) ).
cnf(u3176,negated_conjecture,
~ c4_1(a1455) ).
cnf(u3180,negated_conjecture,
c4_1(a1487) ).
cnf(u3185,negated_conjecture,
c2_1(a1487) ).
cnf(u3194,negated_conjecture,
~ c5_1(a1333) ).
cnf(u3199,negated_conjecture,
~ c5_1(a1455) ).
cnf(u3210,negated_conjecture,
~ ssSkP5(a1378) ).
cnf(u3215,negated_conjecture,
c5_2(a1378,a1373) ).
cnf(u3221,negated_conjecture,
ssSkP12(a1378) ).
cnf(u3253,negated_conjecture,
ssSkP10(a1475) ).
cnf(u3270,negated_conjecture,
c3_1(a1475) ).
cnf(u3296,negated_conjecture,
ssSkP9(a1458) ).
cnf(u3305,negated_conjecture,
ssSkP10(a1458) ).
cnf(u3314,negated_conjecture,
ssSkP13(a1458) ).
cnf(u3318,negated_conjecture,
c2_2(a1458,a1517) ).
cnf(u3329,negated_conjecture,
~ ssSkP5(a1475) ).
cnf(u3332,negated_conjecture,
~ c1_1(a1475) ).
cnf(u3340,negated_conjecture,
c5_2(a1378,a1374) ).
cnf(u3343,negated_conjecture,
~ c1_1(a1378) ).
cnf(u3357,negated_conjecture,
c5_2(a1424,a1324) ).
cnf(u3363,negated_conjecture,
~ c4_2(a1424,a1324) ).
cnf(u3371,negated_conjecture,
c3_2(a1424,a1324) ).
cnf(u3380,negated_conjecture,
~ ssSkP7(a1458) ).
cnf(u3392,negated_conjecture,
~ c4_2(a1378,a1374) ).
cnf(u3400,negated_conjecture,
c5_2(a1475,a1410) ).
cnf(u3404,negated_conjecture,
c2_1(a1475) ).
cnf(u3409,negated_conjecture,
c5_2(a1424,a1410) ).
cnf(u3413,negated_conjecture,
c2_1(a1424) ).
cnf(u3443,negated_conjecture,
ssSkP11(a1498) ).
cnf(u3452,negated_conjecture,
ssSkP5(a1498) ).
cnf(u3466,negated_conjecture,
c1_1(a1498) ).
cnf(u3477,negated_conjecture,
~ c4_1(a1498) ).
cnf(u3480,negated_conjecture,
~ c2_1(a1498) ).
cnf(u3495,negated_conjecture,
~ c5_1(a1439) ).
cnf(u3498,negated_conjecture,
~ c4_2(a1439,a1441) ).
cnf(u3502,negated_conjecture,
~ c4_1(a1439) ).
cnf(u3509,negated_conjecture,
~ c5_1(a1458) ).
cnf(u3521,negated_conjecture,
c4_2(a1464,a1465) ).
cnf(u3524,negated_conjecture,
~ c4_1(a1464) ).
cnf(u3529,negated_conjecture,
~ c4_2(a1455,a1457) ).
cnf(u3559,negated_conjecture,
c5_2(a1378,a1489) ).
cnf(u3565,negated_conjecture,
~ c4_1(a1378) ).
cnf(u3576,negated_conjecture,
( ~ c5_2(a1498,X0)
| c4_2(a1498,X0) ) ).
cnf(u3591,negated_conjecture,
c4_2(a1363,a1364) ).
cnf(u3599,negated_conjecture,
c4_1(a1363) ).
cnf(u3604,negated_conjecture,
c3_2(a1439,a1489) ).
cnf(u3622,negated_conjecture,
~ c2_1(a1439) ).
cnf(u3636,negated_conjecture,
~ c2_2(a1439,a1441) ).
cnf(u3667,negated_conjecture,
( c1_2(a1439,X0)
| c5_2(a1439,X0)
| c2_2(a1439,X0) ) ).
cnf(u3687,negated_conjecture,
c3_2(a1361,a1492) ).
cnf(u3695,negated_conjecture,
c3_2(a1424,a1492) ).
cnf(u3703,negated_conjecture,
~ c3_1(a1504) ).
cnf(u3706,negated_conjecture,
~ c5_1(a1504) ).
cnf(u3714,negated_conjecture,
~ c4_1(a1388) ).
cnf(u3717,negated_conjecture,
~ c2_1(a1388) ).
cnf(u3723,negated_conjecture,
~ c3_1(a1388) ).
cnf(u3726,negated_conjecture,
~ c5_1(a1388) ).
cnf(u3740,negated_conjecture,
~ c1_2(a1487,a1488) ).
cnf(u3745,negated_conjecture,
c3_2(a1487,a1488) ).
cnf(u3756,negated_conjecture,
c5_2(a1424,a1492) ).
cnf(u3773,negated_conjecture,
c2_1(a1378) ).
cnf(u3784,negated_conjecture,
( c4_2(a1498,X0)
| c3_2(a1498,X0) ) ).
cnf(u3796,negated_conjecture,
( c4_2(a1363,X0)
| c3_2(a1363,X0)
| c5_2(a1363,X0) ) ).
cnf(u3808,negated_conjecture,
c2_2(a1493,a1379) ).
cnf(u3824,negated_conjecture,
c2_2(a1350,a1379) ).
cnf(u3840,negated_conjecture,
~ c5_2(a1436,a1437) ).
cnf(u3848,negated_conjecture,
~ c5_1(a1436) ).
cnf(u3871,negated_conjecture,
c3_2(a1333,a1334) ).
cnf(u3888,negated_conjecture,
~ c5_1(a1409) ).
cnf(u3892,negated_conjecture,
c4_2(a1409,a1433) ).
cnf(u3895,negated_conjecture,
~ c1_1(a1409) ).
cnf(u3917,negated_conjecture,
~ c5_1(a1378) ).
cnf(u3925,negated_conjecture,
~ c5_1(a1442) ).
cnf(u3933,negated_conjecture,
~ c5_1(a1428) ).
cnf(u3946,negated_conjecture,
~ c1_2(a1428,a1429) ).
cnf(u3950,negated_conjecture,
~ c2_2(a1428,a1413) ).
cnf(u3954,negated_conjecture,
c5_2(a1428,a1429) ).
cnf(u3957,negated_conjecture,
~ c3_1(a1428) ).
cnf(u3966,negated_conjecture,
c5_2(a1378,a1459) ).
cnf(u3983,negated_conjecture,
c1_1(a1458) ).
cnf(u4079,negated_conjecture,
~ c2_1(a1452) ).
cnf(u4091,negated_conjecture,
~ c2_1(a1503) ).
cnf(u4103,negated_conjecture,
~ c2_1(a1499) ).
cnf(u4115,negated_conjecture,
~ c2_1(a1409) ).
cnf(u4121,negated_conjecture,
~ c1_2(a1409,a1433) ).
cnf(u4126,negated_conjecture,
c2_1(a1446) ).
cnf(u4133,negated_conjecture,
~ c1_2(a1446,a1433) ).
cnf(u4150,negated_conjecture,
~ c3_2(a1464,a1466) ).
cnf(u4155,negated_conjecture,
c1_2(a1464,a1466) ).
cnf(u4163,negated_conjecture,
c1_2(a1378,a1433) ).
cnf(u4172,negated_conjecture,
( c4_2(a1455,X0)
| c3_2(a1455,X0)
| c5_2(a1455,X0) ) ).
cnf(u4190,negated_conjecture,
c2_2(a1452,a1379) ).
cnf(u4202,negated_conjecture,
c4_2(a1446,a1433) ).
cnf(u4209,negated_conjecture,
~ c4_1(a1446) ).
cnf(u4221,negated_conjecture,
c2_2(a1503,a1379) ).
cnf(u4231,negated_conjecture,
c3_2(a1409,a1489) ).
cnf(u4235,negated_conjecture,
c4_1(a1409) ).
cnf(u4249,negated_conjecture,
c3_2(a1499,a1489) ).
cnf(u4252,negated_conjecture,
~ c4_1(a1499) ).
cnf(u4282,negated_conjecture,
c2_2(a1499,a1379) ).
cnf(u4292,negated_conjecture,
c4_2(a1503,a1433) ).
cnf(u4307,negated_conjecture,
( c4_2(a1409,X0)
| c3_2(a1409,X0)
| c5_2(a1409,X0) ) ).
cnf(u4325,negated_conjecture,
c3_2(a1378,a1489) ).
cnf(u4353,negated_conjecture,
c3_2(a1458,a1517) ).
cnf(u4364,negated_conjecture,
( c4_2(a1446,X0)
| c3_2(a1446,X0)
| c5_2(a1446,X0) ) ).
cnf(u4421,negated_conjecture,
c3_2(a1409,a1492) ).
cnf(u4426,negated_conjecture,
c5_2(a1409,a1492) ).
cnf(u4470,negated_conjecture,
~ c2_2(a1424,a1324) ).
cnf(u4474,negated_conjecture,
c4_2(a1424,a1459) ).
cnf(u4485,negated_conjecture,
~ c2_2(a1475,a1410) ).
cnf(u4500,negated_conjecture,
~ c2_2(a1424,a1410) ).
cnf(u4528,negated_conjecture,
~ c1_2(a1464,a1465) ).
cnf(u4587,negated_conjecture,
c3_2(a1363,a1324) ).
cnf(u4590,negated_conjecture,
~ c3_1(a1363) ).
cnf(u4606,negated_conjecture,
~ c5_1(a1363) ).
cnf(u4615,negated_conjecture,
~ c2_2(a1439,a1489) ).
cnf(u4618,negated_conjecture,
~ c4_2(a1439,a1489) ).
cnf(u4631,negated_conjecture,
( c1_2(a1363,X0)
| c5_2(a1363,X0)
| c2_2(a1363,X0) ) ).
cnf(u4660,negated_conjecture,
~ c2_2(a1424,a1492) ).
cnf(u4705,negated_conjecture,
c4_2(a1333,a1433) ).
cnf(u4709,negated_conjecture,
c3_2(a1333,a1489) ).
cnf(u4722,negated_conjecture,
~ c1_2(a1333,a1433) ).
cnf(u4731,negated_conjecture,
( c4_2(a1333,X0)
| c3_2(a1333,X0)
| c5_2(a1333,X0) ) ).
cnf(u4761,negated_conjecture,
~ ssSkP2(a1498) ).
cnf(u4765,negated_conjecture,
c3_2(a1498,a1341) ).
cnf(u4770,negated_conjecture,
c3_2(a1498,a1340) ).
cnf(u4779,negated_conjecture,
c3_2(a1498,a1357) ).
cnf(u4792,negated_conjecture,
( c1_2(a1498,X0)
| c4_2(a1498,X0)
| c2_2(a1498,X0) ) ).
cnf(u4897,negated_conjecture,
c4_2(a1428,a1512) ).
cnf(u4902,negated_conjecture,
ssSkP5(a1428) ).
cnf(u4906,negated_conjecture,
c4_2(a1428,a1373) ).
cnf(u4912,negated_conjecture,
( ~ c5_2(a1428,X0)
| c4_2(a1428,X0) ) ).
cnf(u4916,negated_conjecture,
c4_1(a1428) ).
cnf(u4941,negated_conjecture,
c4_2(a1428,a1413) ).
cnf(u4992,negated_conjecture,
c2_2(a1363,a1373) ).
cnf(u4996,negated_conjecture,
c4_2(a1363,a1374) ).
cnf(u5001,negated_conjecture,
c2_2(a1439,a1373) ).
cnf(u5004,negated_conjecture,
~ c4_2(a1439,a1374) ).
cnf(u5009,negated_conjecture,
~ c2_2(a1361,a1373) ).
cnf(u5014,negated_conjecture,
c4_2(a1361,a1374) ).
cnf(u5023,negated_conjecture,
c4_2(a1428,a1374) ).
cnf(u5028,negated_conjecture,
c2_2(a1424,a1373) ).
cnf(u5032,negated_conjecture,
c4_2(a1424,a1374) ).
cnf(u5048,negated_conjecture,
c3_2(a1363,a1373) ).
cnf(u5053,negated_conjecture,
c3_2(a1439,a1373) ).
cnf(u5183,negated_conjecture,
~ c3_1(a1490) ).
cnf(u5214,negated_conjecture,
( ~ c5_2(a1361,X0)
| c4_2(a1361,X0) ) ).
cnf(u5217,negated_conjecture,
~ c4_1(a1361) ).
cnf(u5221,negated_conjecture,
~ c2_2(a1361,a1489) ).
cnf(u5232,negated_conjecture,
( ~ c3_2(a1361,X0)
| c4_2(a1361,X0)
| ~ c2_2(a1361,X0) ) ).
cnf(u5244,negated_conjecture,
ssSkP5(a1361) ).
cnf(u5261,negated_conjecture,
c5_2(a1361,a1410) ).
cnf(u5265,negated_conjecture,
c2_1(a1361) ).
cnf(u5274,negated_conjecture,
c3_1(a1361) ).
cnf(u5313,negated_conjecture,
ssSkP2(a1363) ).
cnf(u5331,negated_conjecture,
ssSkP13(a1363) ).
cnf(u5353,negated_conjecture,
( c3_2(a1363,X0)
| c5_2(a1363,X0) ) ).
cnf(u5468,negated_conjecture,
~ c5_1(a1493) ).
cnf(u5562,negated_conjecture,
ssSkP13(a1516) ).
cnf(u5566,negated_conjecture,
c5_2(a1516,a1517) ).
cnf(u5597,negated_conjecture,
c1_1(a1516) ).
cnf(u5604,negated_conjecture,
( c3_2(a1516,X0)
| c2_2(a1516,X0)
| c5_2(a1516,X0) ) ).
cnf(u5644,negated_conjecture,
ndr1_1(a1516) ).
cnf(u5652,negated_conjecture,
~ c4_1(a1515) ).
cnf(u5764,negated_conjecture,
c1_1(a1350) ).
cnf(u5831,negated_conjecture,
c5_2(a1361,a1492) ).
cnf(u5840,negated_conjecture,
~ c2_2(a1361,a1492) ).
cnf(u5844,negated_conjecture,
c4_2(a1361,a1492) ).
cnf(u5862,negated_conjecture,
c3_2(a1361,a1489) ).
cnf(u5931,negated_conjecture,
c1_1(a1442) ).
cnf(u6038,negated_conjecture,
c2_2(a1388,a1379) ).
cnf(u6066,negated_conjecture,
( c3_2(a1487,X0)
| c5_2(a1487,X0)
| c2_2(a1487,X0) ) ).
cnf(u6070,negated_conjecture,
( c4_2(a1494,X1)
| c3_2(a1494,X1)
| c5_2(a1494,X1) ) ).
cnf(u6077,negated_conjecture,
( c3_2(a1494,X0)
| c5_2(a1494,X0)
| c2_2(a1494,X0) ) ).
cnf(u6094,negated_conjecture,
c2_2(a1442,a1373) ).
cnf(u6103,negated_conjecture,
c3_2(a1442,a1373) ).
cnf(u6128,negated_conjecture,
~ c4_2(a1458,a1376) ).
cnf(u6133,negated_conjecture,
c3_2(a1458,a1489) ).
cnf(u6157,negated_conjecture,
c2_1(a1504) ).
cnf(u6161,negated_conjecture,
( c1_2(a1504,X0)
| c4_2(a1504,X0) ) ).
cnf(u6180,negated_conjecture,
c2_2(a1475,a1379) ).
cnf(u6212,negated_conjecture,
c3_2(a1475,a1379) ).
cnf(u6288,negated_conjecture,
c5_2(a1409,a1433) ).
cnf(u6299,negated_conjecture,
c5_2(a1409,a1413) ).
cnf(u6304,negated_conjecture,
c4_2(a1409,a1413) ).
cnf(u6308,negated_conjecture,
c2_2(a1409,a1413) ).
cnf(u6338,negated_conjecture,
c2_2(a1446,a1435) ).
cnf(u6346,negated_conjecture,
~ c2_2(a1499,a1489) ).
cnf(u6354,negated_conjecture,
c4_2(a1499,a1459) ).
cnf(u6358,negated_conjecture,
c1_1(a1499) ).
cnf(u6381,negated_conjecture,
c5_2(a1503,a1433) ).
cnf(u6435,negated_conjecture,
c4_2(a1378,a1373) ).
cnf(u6440,negated_conjecture,
c4_2(a1378,a1489) ).
cnf(u6444,negated_conjecture,
~ c4_2(a1378,a1459) ).
cnf(u6508,negated_conjecture,
~ c2_2(a1363,a1410) ).
cnf(u6511,negated_conjecture,
~ c3_2(a1363,a1410) ).
cnf(u6574,negated_conjecture,
c1_2(a1424,a1374) ).
cnf(u6577,negated_conjecture,
~ c3_2(a1424,a1374) ).
cnf(u6584,negated_conjecture,
~ c5_2(a1424,a1374) ).
cnf(u6596,negated_conjecture,
~ c4_2(a1475,a1373) ).
cnf(u6601,negated_conjecture,
c4_2(a1475,a1459) ).
cnf(u6642,negated_conjecture,
c1_2(a1363,a1357) ).
cnf(u6660,negated_conjecture,
c1_2(a1361,a1357) ).
cnf(u6669,negated_conjecture,
c1_2(a1442,a1357) ).
cnf(u6677,negated_conjecture,
~ c1_2(a1428,a1357) ).
cnf(u6687,negated_conjecture,
c1_2(a1424,a1357) ).
cnf(u6691,negated_conjecture,
c1_2(a1424,a1358) ).
cnf(u6696,negated_conjecture,
c1_2(a1475,a1357) ).
cnf(u6734,negated_conjecture,
c2_2(a1363,a1358) ).
cnf(u6739,negated_conjecture,
c2_2(a1439,a1358) ).
cnf(u6748,negated_conjecture,
~ c2_2(a1442,a1358) ).
cnf(u6759,negated_conjecture,
c2_2(a1424,a1358) ).
cnf(u6780,negated_conjecture,
c5_2(a1361,a1357) ).
cnf(u6784,negated_conjecture,
~ c5_2(a1442,a1357) ).
cnf(u6795,negated_conjecture,
c5_2(a1475,a1357) ).
cnf(u6843,negated_conjecture,
~ c3_2(a1428,a1413) ).
cnf(u6895,negated_conjecture,
c3_2(a1363,a1358) ).
cnf(u6905,negated_conjecture,
c3_2(a1424,a1358) ).
cnf(u6910,negated_conjecture,
~ c3_1(a1498) ).
cnf(u6920,negated_conjecture,
c2_2(a1510,a1379) ).
cnf(u6947,negated_conjecture,
~ c1_2(a1428,a1512) ).
cnf(u6966,negated_conjecture,
~ c5_2(a1424,a1357) ).
cnf(u6986,negated_conjecture,
~ c1_2(a1428,a1373) ).
cnf(u7074,negated_conjecture,
~ c2_2(a1361,a1357) ).
cnf(u7114,negated_conjecture,
~ c2_2(a1475,a1357) ).
cnf(u7154,negated_conjecture,
c3_2(a1424,a1459) ).
cnf(u7160,negated_conjecture,
~ c5_2(a1424,a1459) ).
cnf(u7218,negated_conjecture,
c3_2(a1510,a1379) ).
cnf(u7221,negated_conjecture,
~ c1_2(a1510,a1379) ).
cnf(u7227,negated_conjecture,
c4_2(a1510,a1379) ).
cnf(u7259,negated_conjecture,
~ c5_2(a1333,a1433) ).
cnf(u7314,negated_conjecture,
~ c5_2(a1378,a1433) ).
cnf(u7329,negated_conjecture,
ssSkP9(a1498) ).
cnf(u7332,negated_conjecture,
~ c5_2(a1498,a1462) ).
cnf(u7357,negated_conjecture,
~ ssSkP6(a1498) ).
cnf(u7382,negated_conjecture,
ssSkP3(a1428) ).
cnf(u7395,negated_conjecture,
c2_2(a1428,a1517) ).
cnf(u7426,negated_conjecture,
~ ndr1_1(a1361) ).
cnf(u7440,negated_conjecture,
~ c5_1(a1359) ).
cnf(u7460,negated_conjecture,
c1_1(a1428) ).
cnf(u7506,negated_conjecture,
ssSkP9(a1363) ).
cnf(u7524,negated_conjecture,
c5_2(a1363,a1459) ).
cnf(u7529,negated_conjecture,
c4_2(a1363,a1459) ).
cnf(u7563,negated_conjecture,
ssSkP2(a1455) ).
cnf(u7584,negated_conjecture,
ssSkP13(a1455) ).
cnf(u7602,negated_conjecture,
( ~ c1_2(a1455,X0)
| c3_2(a1455,X0)
| c5_2(a1455,X0) ) ).
cnf(u7616,negated_conjecture,
( ~ c4_2(a1455,X1)
| c2_2(a1455,X1)
| ~ c1_2(a1455,X1) ) ).
cnf(u7623,negated_conjecture,
( c1_2(a1455,X0)
| c4_2(a1455,X0)
| c2_2(a1455,X0) ) ).
cnf(u7635,negated_conjecture,
c5_2(a1455,a1435) ).
cnf(u7687,negated_conjecture,
ssSkP2(a1452) ).
cnf(u7708,negated_conjecture,
ssSkP13(a1452) ).
cnf(u7717,negated_conjecture,
~ c3_1(a1452) ).
cnf(u7728,negated_conjecture,
( ~ c1_2(a1452,X0)
| c3_2(a1452,X0)
| c5_2(a1452,X0) ) ).
cnf(u7742,negated_conjecture,
c1_1(a1452) ).
cnf(u7746,negated_conjecture,
( ~ c4_2(a1452,X1)
| c2_2(a1452,X1)
| ~ c1_2(a1452,X1) ) ).
cnf(u7762,negated_conjecture,
( c3_2(a1452,X0)
| c5_2(a1452,X0) ) ).
cnf(u7806,negated_conjecture,
c3_2(a1333,a1340) ).
cnf(u7818,negated_conjecture,
ssSkP13(a1333) ).
cnf(u7832,negated_conjecture,
( ~ c1_2(a1333,X0)
| c3_2(a1333,X0)
| c5_2(a1333,X0) ) ).
cnf(u7838,negated_conjecture,
( ~ c4_2(a1333,X1)
| c2_2(a1333,X1)
| ~ c1_2(a1333,X1) ) ).
cnf(u7849,negated_conjecture,
c3_2(a1333,a1523) ).
cnf(u7861,negated_conjecture,
c3_2(a1333,a1435) ).
cnf(u7879,negated_conjecture,
c2_2(a1333,a1433) ).
cnf(u7917,negated_conjecture,
~ c2_2(a1503,a1375) ).
cnf(u7938,negated_conjecture,
c5_2(a1428,a1376) ).
cnf(u7950,negated_conjecture,
c4_2(a1333,a1375) ).
cnf(u7954,negated_conjecture,
c5_2(a1333,a1376) ).
cnf(u7968,negated_conjecture,
c2_2(a1363,a1375) ).
cnf(u7976,negated_conjecture,
c5_2(a1363,a1377) ).
cnf(u8070,negated_conjecture,
ssSkP9(a1516) ).
cnf(u8083,negated_conjecture,
~ c2_2(a1516,a1517) ).
cnf(u8102,negated_conjecture,
ssSkP10(a1516) ).
cnf(u8111,negated_conjecture,
~ c4_1(a1516) ).
cnf(u8144,negated_conjecture,
ssSkP2(a1487) ).
cnf(u8148,negated_conjecture,
c5_2(a1487,a1340) ).
cnf(u8163,negated_conjecture,
ssSkP13(a1487) ).
cnf(u8167,negated_conjecture,
c5_2(a1487,a1517) ).
cnf(u8171,negated_conjecture,
( c1_2(a1487,X0)
| c3_2(a1487,X0)
| c5_2(a1487,X0) ) ).
cnf(u8180,negated_conjecture,
~ c5_1(a1487) ).
cnf(u8204,negated_conjecture,
( c1_2(a1487,X0)
| c4_2(a1487,X0)
| c2_2(a1487,X0) ) ).
cnf(u8225,negated_conjecture,
c2_2(a1487,a1462) ).
cnf(u8228,negated_conjecture,
~ c5_2(a1487,a1462) ).
cnf(u8235,negated_conjecture,
ssSkP10(a1487) ).
cnf(u8270,negated_conjecture,
~ c5_2(a1494,a1340) ).
cnf(u8275,negated_conjecture,
c3_2(a1494,a1340) ).
cnf(u8289,negated_conjecture,
ssSkP13(a1494) ).
cnf(u8297,negated_conjecture,
c3_1(a1494) ).
cnf(u8302,negated_conjecture,
c2_1(a1494) ).
cnf(u8327,negated_conjecture,
c1_1(a1494) ).
cnf(u8331,negated_conjecture,
( ~ c4_2(a1494,X1)
| c2_2(a1494,X1)
| ~ c1_2(a1494,X1) ) ).
cnf(u8340,negated_conjecture,
c3_2(a1494,a1523) ).
cnf(u8357,negated_conjecture,
( ~ c5_2(a1494,X1)
| ~ c3_2(a1494,X1) ) ).
cnf(u8374,negated_conjecture,
ssSkP9(a1494) ).
cnf(u8377,negated_conjecture,
~ c2_2(a1494,a1462) ).
cnf(u8381,negated_conjecture,
~ c5_2(a1494,a1462) ).
cnf(u8393,negated_conjecture,
( ~ c3_2(a1494,X0)
| c4_2(a1494,X0)
| ~ c2_2(a1494,X0) ) ).
cnf(u8406,negated_conjecture,
ssSkP10(a1494) ).
cnf(u8409,negated_conjecture,
~ c2_2(a1494,a1480) ).
cnf(u8415,negated_conjecture,
~ c4_1(a1494) ).
cnf(u8588,negated_conjecture,
~ c3_2(a1504,a1373) ).
cnf(u8665,negated_conjecture,
( ~ c5_2(a1504,X0)
| c4_2(a1504,X0) ) ).
cnf(u8672,negated_conjecture,
~ c5_2(a1504,a1489) ).
cnf(u8719,negated_conjecture,
~ c1_2(a1439,a1373) ).
cnf(u8731,negated_conjecture,
c2_2(a1439,a1379) ).
cnf(u8795,negated_conjecture,
~ c1_2(a1428,a1374) ).
cnf(u8818,negated_conjecture,
~ c2_2(a1363,a1341) ).
cnf(u8821,negated_conjecture,
~ c3_2(a1363,a1341) ).
cnf(u8877,negated_conjecture,
c1_2(a1378,a1374) ).
cnf(u8892,negated_conjecture,
~ c2_2(a1378,a1374) ).
cnf(u8911,negated_conjecture,
c5_2(a1378,a1357) ).
cnf(u8920,negated_conjecture,
c1_2(a1378,a1357) ).
cnf(u8937,negated_conjecture,
~ c4_2(a1378,a1357) ).
cnf(u8953,negated_conjecture,
~ c2_2(a1378,a1357) ).
cnf(u9076,negated_conjecture,
c5_2(a1325,a1357) ).
cnf(u9085,negated_conjecture,
c1_2(a1325,a1357) ).
cnf(u9096,negated_conjecture,
c3_2(a1325,a1373) ).
cnf(u9105,negated_conjecture,
c2_2(a1325,a1373) ).
cnf(u9113,negated_conjecture,
c5_2(a1325,a1492) ).
cnf(u9118,negated_conjecture,
c3_2(a1325,a1492) ).
cnf(u9125,negated_conjecture,
~ c5_1(a1325) ).
cnf(u9159,negated_conjecture,
~ c5_2(a1325,a1459) ).
cnf(u9191,negated_conjecture,
c4_2(a1325,a1492) ).
cnf(u9195,negated_conjecture,
c3_2(a1325,a1489) ).
cnf(u9208,negated_conjecture,
~ c4_2(a1325,a1357) ).
cnf(u9214,negated_conjecture,
~ c2_2(a1325,a1357) ).
cnf(u9217,negated_conjecture,
c3_1(a1325) ).
cnf(u9256,negated_conjecture,
c4_2(a1325,a1459) ).
cnf(u9292,negated_conjecture,
~ ssSkP5(a1493) ).
cnf(u9302,negated_conjecture,
( ~ c3_2(a1493,X0)
| c4_2(a1493,X0)
| ~ c2_2(a1493,X0) ) ).
cnf(u9313,negated_conjecture,
~ c4_1(a1493) ).
cnf(u9318,negated_conjecture,
c2_2(a1493,a1489) ).
cnf(u9348,negated_conjecture,
~ c2_2(a1493,a1375) ).
cnf(u9410,negated_conjecture,
~ c3_2(a1378,a1459) ).
cnf(u9432,negated_conjecture,
( c1_2(a1424,X0)
| c4_2(a1424,X0) ) ).
cnf(u9436,negated_conjecture,
c3_2(a1424,a1373) ).
cnf(u9439,negated_conjecture,
~ c1_2(a1424,a1373) ).
cnf(u9522,negated_conjecture,
~ c4_1(a1510) ).
cnf(u9612,negated_conjecture,
~ c2_2(a1363,a1459) ).
cnf(u9615,negated_conjecture,
~ c3_2(a1363,a1459) ).
cnf(u9634,negated_conjecture,
~ c1_2(a1363,a1459) ).
cnf(u9672,negated_conjecture,
~ c1_2(a1333,a1375) ).
cnf(u9677,negated_conjecture,
c3_2(a1333,a1375) ).
cnf(u9682,negated_conjecture,
~ c5_2(a1333,a1375) ).
cnf(u9695,negated_conjecture,
ssSkP7(a1363) ).
cnf(u9707,negated_conjecture,
~ c3_2(a1516,a1517) ).
cnf(u9727,negated_conjecture,
~ c4_2(a1516,a1517) ).
cnf(u9732,negated_conjecture,
c3_2(a1516,a1489) ).
cnf(u9743,negated_conjecture,
~ c2_2(a1363,a1377) ).
cnf(u9746,negated_conjecture,
~ c3_2(a1363,a1377) ).
cnf(u9777,negated_conjecture,
c4_2(a1487,a1340) ).
cnf(u9781,negated_conjecture,
c3_2(a1487,a1489) ).
cnf(u9786,negated_conjecture,
c2_2(a1487,a1340) ).
cnf(u9798,negated_conjecture,
~ c2_2(a1487,a1517) ).
cnf(u9801,negated_conjecture,
~ c3_2(a1487,a1517) ).
cnf(u9809,negated_conjecture,
( c1_2(a1487,X0)
| c4_2(a1487,X0) ) ).
cnf(u9817,negated_conjecture,
c1_2(a1487,a1462) ).
cnf(u9843,negated_conjecture,
c3_2(a1494,a1462) ).
cnf(u9932,negated_conjecture,
~ c1_2(a1325,a1459) ).
cnf(u10025,negated_conjecture,
~ c1_2(a1363,a1374) ).
cnf(u10107,negated_conjecture,
~ c5_2(a1424,a1358) ).
cnf(u10120,negated_conjecture,
c5_2(a1363,a1357) ).
cnf(u10140,negated_conjecture,
~ c2_2(a1363,a1357) ).
cnf(u10249,negated_conjecture,
ssSkP5(a1504) ).
cnf(u10253,negated_conjecture,
c4_2(a1504,a1373) ).
cnf(u10270,negated_conjecture,
~ ssSkP5(a1363) ).
cnf(u10292,negated_conjecture,
c5_2(a1452,a1462) ).
cnf(u10344,negated_conjecture,
~ c5_1(a1346) ).
cnf(u10402,negated_conjecture,
ssSkP11(a1424) ).
cnf(u10412,negated_conjecture,
( ~ c5_2(a1424,X0)
| c4_2(a1424,X0)
| ~ c2_2(a1424,X0) ) ).
cnf(u10435,negated_conjecture,
( ~ c3_2(a1439,X0)
| c4_2(a1439,X0)
| ~ c2_2(a1439,X0) ) ).
cnf(u10448,negated_conjecture,
~ ssSkP5(a1439) ).
cnf(u10466,negated_conjecture,
c4_2(a1439,a1373) ).
cnf(u10597,negated_conjecture,
c5_2(a1499,a1340) ).
cnf(u10612,negated_conjecture,
ssSkP13(a1499) ).
cnf(u10623,negated_conjecture,
( ~ c4_2(a1499,X1)
| c2_2(a1499,X1)
| ~ c1_2(a1499,X1) ) ).
cnf(u10642,negated_conjecture,
( ~ c1_2(a1499,X0)
| c3_2(a1499,X0)
| c5_2(a1499,X0) ) ).
cnf(u10673,negated_conjecture,
c2_2(a1499,a1358) ).
cnf(u10683,negated_conjecture,
c1_2(a1499,a1358) ).
cnf(u10689,negated_conjecture,
c3_2(a1499,a1358) ).
cnf(u10699,negated_conjecture,
c4_2(a1499,a1374) ).
cnf(u10747,negated_conjecture,
c5_2(a1409,a1340) ).
cnf(u10766,negated_conjecture,
c5_2(a1409,a1517) ).
cnf(u10775,negated_conjecture,
( ~ c1_2(a1409,X0)
| c3_2(a1409,X0)
| c5_2(a1409,X0) ) ).
cnf(u10786,negated_conjecture,
( c3_2(a1409,X0)
| c2_2(a1409,X0)
| c5_2(a1409,X0) ) ).
cnf(u10794,negated_conjecture,
c3_2(a1409,a1523) ).
cnf(u10815,negated_conjecture,
ssSkP11(a1409) ).
cnf(u10819,negated_conjecture,
c4_2(a1409,a1512) ).
cnf(u10824,negated_conjecture,
ssSkP5(a1409) ).
cnf(u10827,negated_conjecture,
~ c4_2(a1409,a1373) ).
cnf(u10839,negated_conjecture,
( ~ c5_2(a1409,X0)
| c4_2(a1409,X0)
| ~ c2_2(a1409,X0) ) ).
cnf(u10902,negated_conjecture,
~ c1_2(a1409,a1512) ).
cnf(u10905,negated_conjecture,
c5_2(a1409,a1512) ).
cnf(u10911,negated_conjecture,
c2_2(a1409,a1512) ).
cnf(u10946,negated_conjecture,
c5_2(a1409,a1373) ).
cnf(u10951,negated_conjecture,
~ c2_2(a1409,a1373) ).
cnf(u11059,negated_conjecture,
ssSkP2(a1446) ).
cnf(u11078,negated_conjecture,
ssSkP13(a1446) ).
cnf(u11089,negated_conjecture,
c1_1(a1446) ).
cnf(u11096,negated_conjecture,
( c3_2(a1446,X0)
| c2_2(a1446,X0)
| c5_2(a1446,X0) ) ).
cnf(u11104,negated_conjecture,
c3_2(a1446,a1523) ).
cnf(u11112,negated_conjecture,
c5_2(a1446,a1413) ).
cnf(u11120,negated_conjecture,
c4_2(a1446,a1413) ).
cnf(u11125,negated_conjecture,
~ c2_2(a1446,a1413) ).
cnf(u11230,negated_conjecture,
c2_2(a1455,a1489) ).
cnf(u11240,negated_conjecture,
ssSkP11(a1455) ).
cnf(u11424,negated_conjecture,
c3_2(a1487,a1513) ).
cnf(u11429,negated_conjecture,
ssSkP11(a1487) ).
cnf(u11451,negated_conjecture,
( ~ c5_2(a1487,X0)
| c4_2(a1487,X0) ) ).
cnf(u11541,negated_conjecture,
~ c2_2(a1494,a1375) ).
cnf(u11550,negated_conjecture,
~ c2_2(a1494,a1523) ).
cnf(u11559,negated_conjecture,
~ c2_2(a1494,a1340) ).
cnf(u11734,negated_conjecture,
~ c4_2(a1333,a1376) ).
cnf(u11761,negated_conjecture,
~ ssSkP7(a1333) ).
cnf(u11877,negated_conjecture,
~ c5_2(a1504,a1373) ).
cnf(u11889,negated_conjecture,
~ c1_2(a1504,a1373) ).
cnf(u11907,negated_conjecture,
( ~ c4_2(a1504,X0)
| c2_2(a1504,X0)
| ~ c1_2(a1504,X0) ) ).
cnf(u11949,negated_conjecture,
~ c5_2(a1499,a1358) ).
cnf(u11983,negated_conjecture,
~ c5_2(a1499,a1459) ).
cnf(u11995,negated_conjecture,
~ c1_2(a1499,a1459) ).
cnf(u12013,negated_conjecture,
~ c5_2(a1499,a1374) ).
cnf(u12025,negated_conjecture,
~ c1_2(a1499,a1374) ).
cnf(u12037,negated_conjecture,
~ c2_2(a1409,a1340) ).
cnf(u12040,negated_conjecture,
~ c4_2(a1409,a1340) ).
cnf(u12053,negated_conjecture,
~ c2_2(a1409,a1517) ).
cnf(u12056,negated_conjecture,
~ c4_2(a1409,a1517) ).
cnf(u12221,negated_conjecture,
~ c2_2(a1409,a1489) ).
cnf(u12276,negated_conjecture,
c2_2(a1503,a1433) ).
cnf(u12303,negated_conjecture,
~ c1_2(a1487,a1340) ).
cnf(u12313,negated_conjecture,
c1_2(a1487,a1517) ).
cnf(u12346,negated_conjecture,
~ c2_2(a1424,a1375) ).
cnf(u12370,negated_conjecture,
~ c2_2(a1439,a1375) ).
cnf(u12459,negated_conjecture,
ssSkP9(a1409) ).
cnf(u12462,negated_conjecture,
~ c5_2(a1409,a1462) ).
cnf(u12466,negated_conjecture,
~ c2_2(a1409,a1462) ).
cnf(u12477,negated_conjecture,
c2_2(a1409,a1480) ).
cnf(u12500,negated_conjecture,
ssSkP11(a1504) ).
cnf(u12613,negated_conjecture,
ssSkP5(a1487) ).
cnf(u12671,negated_conjecture,
c4_2(a1409,a1462) ).
cnf(u12725,negated_conjecture,
~ c2_2(a1409,a1523) ).
cnf(u12733,negated_conjecture,
( ~ c3_2(a1409,X0)
| c4_2(a1409,X0)
| ~ c2_2(a1409,X0) ) ).
cnf(u12762,negated_conjecture,
c5_2(a1409,a1357) ).
cnf(u12771,negated_conjecture,
c1_2(a1409,a1357) ).
cnf(u12817,negated_conjecture,
~ c2_2(a1409,a1324) ).
cnf(u12830,negated_conjecture,
~ c2_2(a1409,a1410) ).
cnf(u12833,negated_conjecture,
~ c4_2(a1409,a1410) ).
cnf(u12842,negated_conjecture,
~ c2_2(a1409,a1492) ).
cnf(u12859,negated_conjecture,
~ c2_2(a1409,a1357) ).
cnf(u12862,negated_conjecture,
~ c4_2(a1409,a1357) ).
cnf(u13192,negated_conjecture,
~ c2_2(a1409,a1375) ).
cnf(u2831,negated_conjecture,
ssSkP11(a1490) ).
cnf(clause21,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(u12950,negated_conjecture,
c5_2(a1333,a1414) ).
cnf(clause51,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u7472,negated_conjecture,
ssSkP7(a1361) ).
cnf(u12943,negated_conjecture,
c5_2(a1409,a1414) ).
cnf(u12167,negated_conjecture,
~ c3_2(a1446,a1377) ).
cnf(clause189,negated_conjecture,
( ~ c1_2(X0,a1513)
| ssSkP12(X0) ) ).
cnf(u10295,negated_conjecture,
~ c1_2(a1363,a1373) ).
cnf(u3259,negated_conjecture,
ssSkP11(a1475) ).
cnf(u13016,negated_conjecture,
c2_2(a1388,a1414) ).
cnf(u12983,negated_conjecture,
c4_2(a1363,a1414) ).
cnf(u10171,negated_conjecture,
( ~ c3_2(a1424,X0)
| ~ c2_2(a1424,X0)
| c4_2(a1424,X0) ) ).
cnf(u12880,negated_conjecture,
c2_2(a1409,a1374) ).
cnf(u7476,negated_conjecture,
ssSkP2(a1361) ).
cnf(u11472,negated_conjecture,
ssSkP5(a1483) ).
cnf(clause91,negated_conjecture,
( ssSkP12(X0)
| c4_2(X0,a1513) ) ).
cnf(u6885,negated_conjecture,
( ~ c4_1(X0)
| c1_2(X0,a1357)
| c2_1(X0)
| c3_2(X0,a1358) ) ).
cnf(u7480,negated_conjecture,
c5_2(a1361,a1377) ).
cnf(u3423,negated_conjecture,
c2_2(a1475,a1373) ).
cnf(u4573,negated_conjecture,
~ c1_2(a1363,a1410) ).
cnf(u4979,negated_conjecture,
~ c1_2(a1428,a1413) ).
cnf(u11211,negated_conjecture,
c1_2(a1455,a1457) ).
cnf(u11688,negated_conjecture,
~ c4_2(a1498,a1462) ).
cnf(clause190,negated_conjecture,
( ~ c2_2(X0,a1512)
| ssSkP11(X0) ) ).
cnf(u6625,negated_conjecture,
( c1_1(X0)
| c3_2(X0,a1358)
| c5_2(X0,a1357) ) ).
cnf(u2822,negated_conjecture,
ssSkP11(a1446) ).
cnf(u7890,negated_conjecture,
~ c4_2(a1452,a1341) ).
cnf(clause217,negated_conjecture,
( ~ c2_2(X0,a1376)
| ssSkP7(X0) ) ).
cnf(u2936,negated_conjecture,
ssSkP2(a1490) ).
cnf(u12979,negated_conjecture,
c4_2(a1388,a1414) ).
cnf(u8805,negated_conjecture,
c4_2(a1361,a1410) ).
cnf(clause106,negated_conjecture,
( ssSkP10(X0)
| c4_2(X0,a1480) ) ).
cnf(u13013,negated_conjecture,
c2_2(a1455,a1414) ).
cnf(u7173,negated_conjecture,
ssSkP2(a1434) ).
cnf(u7960,negated_conjecture,
( ~ c5_2(X0,a1375)
| c5_2(X0,a1376)
| ~ c2_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a1377) ) ).
cnf(u12984,negated_conjecture,
c4_2(a1333,a1414) ).
cnf(u7378,negated_conjecture,
ssSkP2(a1428) ).
cnf(u12980,negated_conjecture,
c4_2(a1503,a1414) ).
cnf(u11478,negated_conjecture,
c5_2(a1483,a1377) ).
cnf(u7177,negated_conjecture,
c5_2(a1434,a1377) ).
cnf(u11471,negated_conjecture,
ssSkP6(a1483) ).
cnf(clause232,negated_conjecture,
( ~ c2_2(X0,a1340)
| ssSkP2(X0) ) ).
cnf(clause5,negated_conjecture,
c2_1(a1464) ).
cnf(u13014,negated_conjecture,
c2_2(a1409,a1414) ).
cnf(u7171,negated_conjecture,
ssSkP5(a1434) ).
cnf(u10091,negated_conjecture,
( ~ c4_1(X0)
| c1_2(X0,a1357)
| c2_1(X0)
| c1_2(X0,a1358) ) ).
cnf(u2846,negated_conjecture,
ssSkP10(a1490) ).
cnf(clause45,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u12743,negated_conjecture,
~ c5_2(a1409,a1374) ).
cnf(u4389,negated_conjecture,
~ c1_2(a1409,a1410) ).
cnf(u11476,negated_conjecture,
c2_1(a1483) ).
cnf(u10385,negated_conjecture,
c1_2(a1424,a1324) ).
cnf(u7475,negated_conjecture,
ssSkP3(a1361) ).
cnf(u9261,negated_conjecture,
c2_2(a1325,a1492) ).
cnf(u10415,negated_conjecture,
c5_2(a1439,a1489) ).
cnf(u12977,negated_conjecture,
c4_2(a1409,a1414) ).
cnf(u6624,negated_conjecture,
( c1_1(X0)
| c3_2(X0,a1358)
| c1_2(X0,a1357) ) ).
cnf(u2816,negated_conjecture,
ssSkP12(a1490) ).
cnf(clause90,negated_conjecture,
( ssSkP13(X0)
| c1_2(X0,a1517) ) ).
cnf(clause188,negated_conjecture,
( ~ c4_2(X0,a1517)
| ssSkP13(X0) ) ).
cnf(u7655,negated_conjecture,
c5_2(a1455,a1341) ).
cnf(u7183,negated_conjecture,
~ c2_2(a1434,a1377) ).
cnf(u5060,negated_conjecture,
( c1_2(X0,a1375)
| c5_2(X0,a1377)
| c5_2(X0,a1376) ) ).
cnf(clause201,negated_conjecture,
( ~ c3_2(X0,a1462)
| ssSkP9(X0) ) ).
cnf(u11469,negated_conjecture,
ssSkP9(a1483) ).
cnf(u3418,negated_conjecture,
( ndr1_1(X0)
| c5_2(X0,a1377) ) ).
cnf(u9689,negated_conjecture,
ssSkP6(a1363) ).
cnf(u2882,negated_conjecture,
ssSkP6(a1446) ).
cnf(u3428,negated_conjecture,
~ c2_2(a1458,a1376) ).
cnf(clause218,negated_conjecture,
( ~ c2_2(X0,a1375)
| ssSkP6(X0) ) ).
cnf(u11465,negated_conjecture,
ssSkP13(a1483) ).
cnf(u4574,negated_conjecture,
c5_2(a1363,a1410) ).
cnf(u9064,negated_conjecture,
ndr1_1(a1325) ).
cnf(u8055,negated_conjecture,
~ c4_1(a1452) ).
cnf(u7945,negated_conjecture,
( ~ c5_2(X0,a1375)
| c5_2(X0,a1376)
| c2_2(X0,a1505)
| ~ c2_2(X0,a1375)
| c5_2(X0,a1377) ) ).
cnf(u11397,negated_conjecture,
~ c1_2(a1452,a1489) ).
cnf(u9299,negated_conjecture,
ssSkP11(a1493) ).
cnf(u7405,negated_conjecture,
c1_2(a1498,a1375) ).
cnf(u12948,negated_conjecture,
c5_2(a1452,a1414) ).
cnf(u4860,negated_conjecture,
~ c4_2(a1498,a1340) ).
cnf(u10450,negated_conjecture,
ssSkP11(a1439) ).
cnf(u7182,negated_conjecture,
~ c3_2(a1434,a1377) ).
cnf(clause6,negated_conjecture,
c2_1(a1458) ).
cnf(u11511,negated_conjecture,
~ c2_2(a1483,a1377) ).
cnf(u7168,negated_conjecture,
ssSkP9(a1434) ).
cnf(u7335,negated_conjecture,
ssSkP10(a1498) ).
cnf(u3607,negated_conjecture,
c3_2(a1455,a1489) ).
cnf(u10066,negated_conjecture,
( c1_1(X0)
| c1_2(X0,a1358)
| c5_2(X0,a1357) ) ).
cnf(clause17,negated_conjecture,
( ssSkP13(X0)
| ndr1_1(X0) ) ).
cnf(u12178,negated_conjecture,
~ c1_2(a1446,a1377) ).
cnf(clause44,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u5174,negated_conjecture,
~ c2_2(a1490,a1377) ).
cnf(u5169,negated_conjecture,
c5_2(a1490,a1377) ).
cnf(u4392,negated_conjecture,
c3_2(a1409,a1324) ).
cnf(u9019,negated_conjecture,
c4_2(a1428,a1357) ).
cnf(clause187,negated_conjecture,
( ~ c3_2(X0,a1517)
| ssSkP13(X0) ) ).
cnf(u10181,negated_conjecture,
~ c1_2(a1516,a1489) ).
cnf(u5038,negated_conjecture,
( ~ c4_1(X0)
| c3_2(X0,a1373)
| c2_1(X0)
| c4_2(X0,a1374) ) ).
cnf(u4781,negated_conjecture,
ssSkP13(a1498) ).
cnf(u3650,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c5_2(X0,X1)
| c2_1(X0)
| c3_2(X0,a1492) ) ).
cnf(u7468,negated_conjecture,
ssSkP12(a1361) ).
cnf(u12946,negated_conjecture,
c5_2(a1503,a1414) ).
cnf(clause191,negated_conjecture,
( ~ c1_2(X0,a1512)
| ssSkP11(X0) ) ).
cnf(u13098,negated_conjecture,
~ c1_2(a1409,a1414) ).
cnf(u11474,negated_conjecture,
ssSkP2(a1483) ).
cnf(u7492,negated_conjecture,
( c5_2(a1363,X0)
| c2_2(a1363,X0) ) ).
cnf(u3161,negated_conjecture,
( ~ c5_2(X1,a1379)
| c3_2(X1,X2)
| c5_2(X1,X2)
| c4_2(X1,X2)
| c2_1(X1) ) ).
cnf(u3416,negated_conjecture,
( ~ ssSkP7(X0)
| c5_2(X0,a1377)
| c3_2(X0,a1375) ) ).
cnf(u2897,negated_conjecture,
ssSkP5(a1446) ).
cnf(clause200,negated_conjecture,
( ~ c5_2(X0,a1480)
| ssSkP10(X0) ) ).
cnf(u13017,negated_conjecture,
c2_2(a1503,a1414) ).
cnf(u3162,negated_conjecture,
( ~ c1_2(X1,a1379)
| c3_2(X1,X2)
| c5_2(X1,X2)
| c4_2(X1,X2)
| c2_1(X1) ) ).
cnf(u12641,negated_conjecture,
c3_2(a1487,a1324) ).
cnf(u8775,negated_conjecture,
~ c3_2(a1361,a1377) ).
cnf(u11687,negated_conjecture,
c3_2(a1498,a1462) ).
cnf(u11724,negated_conjecture,
ssSkP6(a1333) ).
cnf(u3544,negated_conjecture,
c2_2(a1333,a1334) ).
cnf(clause231,negated_conjecture,
( ~ c4_2(X0,a1340)
| ssSkP2(X0) ) ).
cnf(u10266,negated_conjecture,
ssSkP11(a1363) ).
cnf(u5190,negated_conjecture,
~ c4_1(a1490) ).
cnf(u5066,negated_conjecture,
( c3_2(X0,a1375)
| c5_2(X0,a1377)
| c5_2(X0,a1376) ) ).
cnf(u11473,negated_conjecture,
ssSkP3(a1483) ).
cnf(u10065,negated_conjecture,
( c1_1(X0)
| c1_2(X0,a1358)
| c1_2(X0,a1357) ) ).
cnf(u10079,negated_conjecture,
( c1_1(X0)
| c2_2(X0,a1358)
| c5_2(X0,a1357) ) ).
cnf(u3079,negated_conjecture,
( c1_1(X0)
| c5_2(X0,a1492)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u6119,negated_conjecture,
c3_2(a1458,a1376) ).
cnf(clause219,negated_conjecture,
( ~ c1_2(X0,a1373)
| ssSkP5(X0) ) ).
cnf(u6192,negated_conjecture,
( ~ ndr1_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c3_2(X0,X2)
| c2_2(X0,X2)
| c2_2(X0,a1379)
| ~ c5_1(X0) ) ).
cnf(clause3,negated_conjecture,
c5_1(a1494) ).
cnf(clause43,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u2951,negated_conjecture,
c1_1(a1490) ).
cnf(u12711,negated_conjecture,
c4_2(a1409,a1374) ).
cnf(u11479,negated_conjecture,
~ c4_1(a1483) ).
cnf(clause28,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u12168,negated_conjecture,
~ c2_2(a1446,a1377) ).
cnf(u5970,negated_conjecture,
~ c4_2(a1363,a1341) ).
cnf(u7467,negated_conjecture,
ssSkP13(a1361) ).
cnf(clause129,negated_conjecture,
( ssSkP3(X0)
| c5_2(X0,a1357) ) ).
cnf(u10163,negated_conjecture,
c4_2(a1424,a1373) ).
cnf(u2867,negated_conjecture,
ssSkP7(a1446) ).
cnf(u7979,negated_conjecture,
( ~ c2_2(X0,a1375)
| c5_2(X0,a1376)
| c1_1(X0)
| c4_2(X0,a1459)
| c4_2(X0,a1375)
| c5_2(X0,a1377) ) ).
cnf(u13200,negated_conjecture,
~ c1_2(a1333,a1489) ).
cnf(u3217,negated_conjecture,
ssSkP11(a1378) ).
cnf(u3386,negated_conjecture,
( c1_1(X0)
| c4_2(X0,a1374)
| c2_2(X0,a1373) ) ).
cnf(u12947,negated_conjecture,
c5_2(a1498,a1414) ).
cnf(u7170,negated_conjecture,
ssSkP6(a1434) ).
cnf(u11766,negated_conjecture,
~ c2_2(a1333,a1376) ).
cnf(u3078,negated_conjecture,
( c1_1(X0)
| c3_2(X0,a1492)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u2876,negated_conjecture,
ssSkP7(a1490) ).
cnf(u9899,negated_conjecture,
~ c1_2(a1378,a1489) ).
cnf(u10124,negated_conjecture,
( ~ c4_1(X0)
| c1_2(X0,a1357)
| c2_1(X0)
| c2_2(X0,a1358) ) ).
cnf(u10164,negated_conjecture,
c4_2(a1424,a1358) ).
cnf(u3424,negated_conjecture,
c3_2(a1475,a1373) ).
cnf(u7470,negated_conjecture,
ssSkP10(a1361) ).
cnf(u3387,negated_conjecture,
( c1_1(X0)
| c4_2(X0,a1374)
| c3_2(X0,a1373) ) ).
cnf(u5969,negated_conjecture,
c5_2(a1363,a1341) ).
cnf(u8965,negated_conjecture,
~ c1_2(a1475,a1459) ).
cnf(u7406,negated_conjecture,
c3_2(a1498,a1375) ).
cnf(clause125,negated_conjecture,
( ssSkP5(X0)
| c3_2(X0,a1373) ) ).
cnf(u9329,negated_conjecture,
c2_2(a1493,a1373) ).
cnf(u3060,negated_conjecture,
c2_1(a1490) ).
cnf(u7166,negated_conjecture,
ssSkP11(a1434) ).
cnf(u12945,negated_conjecture,
c5_2(a1388,a1414) ).
cnf(u4737,negated_conjecture,
( c3_2(a1498,X0)
| c5_2(a1498,X0) ) ).
cnf(u7944,negated_conjecture,
( ~ c5_2(X0,a1375)
| c5_2(X0,a1376)
| c3_2(X0,a1505)
| ~ c2_2(X0,a1375)
| c5_2(X0,a1377) ) ).
cnf(u4876,negated_conjecture,
( c4_2(a1428,X0)
| c2_2(a1428,X0) ) ).
cnf(u4381,negated_conjecture,
c2_2(a1378,a1373) ).
cnf(u12944,negated_conjecture,
c5_2(a1499,a1414) ).
cnf(u7165,negated_conjecture,
ssSkP12(a1434) ).
cnf(clause27,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u9654,negated_conjecture,
c4_2(a1428,a1376) ).
cnf(u3066,negated_conjecture,
ndr1_1(a1350) ).
cnf(u3204,negated_conjecture,
~ c3_2(a1363,a1364) ).
cnf(u10153,negated_conjecture,
( ~ c4_1(X0)
| c5_2(X0,a1357)
| c2_1(X0)
| c2_2(X0,a1358) ) ).
cnf(u4393,negated_conjecture,
c5_2(a1409,a1410) ).
cnf(clause130,negated_conjecture,
( ssSkP3(X0)
| c1_2(X0,a1357) ) ).
cnf(u10294,negated_conjecture,
ssSkP10(a1452) ).
cnf(u9356,negated_conjecture,
c4_2(a1493,a1373) ).
cnf(u12927,negated_conjecture,
~ c1_2(a1409,a1413) ).
cnf(u4377,negated_conjecture,
~ c1_2(a1378,a1373) ).
cnf(u12949,negated_conjecture,
c5_2(a1363,a1414) ).
cnf(u2777,negated_conjecture,
( c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u7656,negated_conjecture,
~ c4_2(a1455,a1341) ).
cnf(u4798,negated_conjecture,
( c3_2(a1498,X0)
| c2_2(a1498,X0) ) ).
cnf(u10382,negated_conjecture,
~ c5_2(a1494,a1523) ).
cnf(u12197,negated_conjecture,
c1_2(a1498,a1462) ).
cnf(u10078,negated_conjecture,
( c1_1(X0)
| c2_2(X0,a1358)
| c1_2(X0,a1357) ) ).
cnf(clause69,negated_conjecture,
~ c5_2(a1464,a1465) ).
cnf(clause199,negated_conjecture,
( ~ c3_2(X0,a1480)
| ssSkP10(X0) ) ).
cnf(u7235,negated_conjecture,
ssSkP3(a1424) ).
cnf(u11354,negated_conjecture,
c3_2(a1452,a1489) ).
cnf(u7471,negated_conjecture,
ssSkP9(a1361) ).
cnf(u2921,negated_conjecture,
ssSkP3(a1490) ).
cnf(u13170,negated_conjecture,
c3_2(a1409,a1462) ).
cnf(u13015,negated_conjecture,
c2_2(a1499,a1414) ).
cnf(u4572,negated_conjecture,
~ c1_1(a1363) ).
cnf(clause126,negated_conjecture,
( ssSkP5(X0)
| c2_2(X0,a1373) ) ).
cnf(u9325,negated_conjecture,
~ c1_2(a1493,a1373) ).
cnf(u9330,negated_conjecture,
c3_2(a1493,a1373) ).
cnf(u7172,negated_conjecture,
ssSkP3(a1434) ).
cnf(u4982,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,a1373)
| c2_1(X0)
| c4_2(X0,a1374) ) ).
cnf(u8693,negated_conjecture,
~ c5_2(a1498,a1340) ).
cnf(u3697,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1)
| ~ c3_1(X0) ) ).
cnf(clause124,negated_conjecture,
( ssSkP6(X0)
| c1_2(X0,a1375) ) ).
cnf(u7534,negated_conjecture,
c5_2(a1455,a1456) ).
cnf(u6316,negated_conjecture,
c2_2(a1409,a1433) ).
cnf(clause11,negated_conjecture,
c2_2(a1464,a1465) ).
cnf(clause225,negated_conjecture,
( ~ c4_2(X0,a1357)
| ssSkP3(X0) ) ).
cnf(u2837,negated_conjecture,
ssSkP10(a1446) ).
cnf(clause9,negated_conjecture,
c2_2(a1464,a1466) ).
cnf(u13019,negated_conjecture,
c2_2(a1452,a1414) ).
cnf(u7169,negated_conjecture,
ssSkP7(a1434) ).
cnf(u10111,negated_conjecture,
( ~ c4_1(X0)
| c5_2(X0,a1357)
| c2_1(X0)
| c1_2(X0,a1358) ) ).
cnf(u11033,negated_conjecture,
c4_2(a1361,a1377) ).
cnf(u2861,negated_conjecture,
ssSkP9(a1490) ).
cnf(u4859,negated_conjecture,
~ c2_2(a1498,a1340) ).
cnf(u13021,negated_conjecture,
c2_2(a1333,a1414) ).
cnf(u4382,negated_conjecture,
c3_2(a1378,a1373) ).
cnf(u6225,negated_conjecture,
( ~ c5_1(X0)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c3_2(X0,X2)
| c2_2(X0,X2)
| c2_2(X0,a1379)
| c3_2(X0,X1)
| c5_2(X0,a1377) ) ).
cnf(u2852,negated_conjecture,
ssSkP9(a1446) ).
cnf(u9490,negated_conjecture,
~ ssSkP5(a1424) ).
cnf(u11510,negated_conjecture,
~ c3_2(a1483,a1377) ).
cnf(u3748,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c5_2(X0,X1)
| c2_1(X0)
| c5_2(X0,a1492) ) ).
cnf(u7167,negated_conjecture,
ssSkP10(a1434) ).
cnf(u7401,negated_conjecture,
~ c2_2(a1498,a1375) ).
cnf(u4165,negated_conjecture,
( c1_2(a1428,X0)
| c4_2(a1428,X0) ) ).
cnf(clause192,negated_conjecture,
( ~ c5_2(X0,a1512)
| ssSkP11(X0) ) ).
cnf(u11466,negated_conjecture,
ssSkP12(a1483) ).
cnf(u12976,negated_conjecture,
c4_2(a1455,a1414) ).
cnf(u3163,negated_conjecture,
( c2_1(X1)
| c2_2(X1,a1379)
| c3_2(X1,X2)
| c5_2(X1,X2)
| c4_2(X1,X2) ) ).
cnf(u9950,negated_conjecture,
c1_2(a1493,a1375) ).
cnf(clause68,negated_conjecture,
~ c5_2(a1464,a1466) ).
cnf(u11842,negated_conjecture,
~ c3_2(a1363,a1357) ).
cnf(u8776,negated_conjecture,
~ c2_2(a1361,a1377) ).
cnf(u2891,negated_conjecture,
ssSkP6(a1490) ).
cnf(u3431,negated_conjecture,
c5_2(a1458,a1376) ).
cnf(u9039,negated_conjecture,
ssSkP3(a1442) ).
cnf(u2906,negated_conjecture,
ssSkP5(a1490) ).
cnf(u2912,negated_conjecture,
ssSkP3(a1446) ).
cnf(u7512,negated_conjecture,
ssSkP10(a1363) ).
cnf(clause123,negated_conjecture,
( ssSkP6(X0)
| c3_2(X0,a1375) ) ).
cnf(u7889,negated_conjecture,
c5_2(a1452,a1341) ).
cnf(u12744,negated_conjecture,
~ c1_2(a1409,a1374) ).
cnf(clause20,negated_conjecture,
( ssSkP12(X0)
| ndr1_1(X0) ) ).
cnf(u8966,negated_conjecture,
~ c3_2(a1475,a1459) ).
cnf(u2807,negated_conjecture,
ssSkP12(a1446) ).
cnf(clause10,negated_conjecture,
c3_2(a1464,a1465) ).
cnf(u7036,negated_conjecture,
c2_2(a1378,a1489) ).
cnf(u7174,negated_conjecture,
c1_1(a1434) ).
cnf(u12163,negated_conjecture,
c5_2(a1446,a1377) ).
cnf(u7164,negated_conjecture,
ssSkP13(a1434) ).
cnf(u12982,negated_conjecture,
c4_2(a1452,a1414) ).
cnf(u6953,negated_conjecture,
( ~ c4_1(X0)
| c5_2(X0,a1357)
| c2_1(X0)
| c3_2(X0,a1358) ) ).
cnf(u12981,negated_conjecture,
c4_2(a1498,a1414) ).
cnf(u11470,negated_conjecture,
ssSkP7(a1483) ).
cnf(u12487,negated_conjecture,
c5_2(a1475,a1459) ).
cnf(u4649,negated_conjecture,
~ c1_2(a1439,a1489) ).
cnf(u7469,negated_conjecture,
ssSkP11(a1361) ).
cnf(u11467,negated_conjecture,
ssSkP11(a1483) ).
cnf(clause54,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u9910,negated_conjecture,
~ c1_2(a1325,a1489) ).
cnf(clause92,negated_conjecture,
( ssSkP12(X0)
| c2_2(X0,a1513) ) ).
cnf(u7473,negated_conjecture,
ssSkP6(a1361) ).
cnf(u5173,negated_conjecture,
~ c3_2(a1490,a1377) ).
cnf(u11468,negated_conjecture,
ssSkP10(a1483) ).
cnf(u4545,negated_conjecture,
~ c1_2(a1455,a1489) ).
cnf(u3415,negated_conjecture,
( ~ ssSkP7(X0)
| c5_2(X0,a1377)
| c1_2(X0,a1375) ) ).
cnf(u6852,negated_conjecture,
c3_2(a1428,a1324) ).
cnf(u13018,negated_conjecture,
c2_2(a1498,a1414) ).
cnf(u3419,negated_conjecture,
~ c1_2(a1475,a1373) ).
cnf(u12232,negated_conjecture,
c4_2(a1487,a1517) ).
cnf(u6081,negated_conjecture,
~ c4_1(a1350) ).
cnf(clause107,negated_conjecture,
( ssSkP9(X0)
| c4_2(X0,a1462) ) ).
cnf(u13020,negated_conjecture,
c2_2(a1363,a1414) ).
cnf(u12978,negated_conjecture,
c4_2(a1499,a1414) ).
cnf(u11606,negated_conjecture,
~ c2_2(a1475,a1459) ).
cnf(u12890,negated_conjecture,
c1_2(a1409,a1462) ).
cnf(u10088,negated_conjecture,
c2_2(a1363,a1324) ).
cnf(clause4,negated_conjecture,
ndr1_1(a1464) ).
cnf(u8691,negated_conjecture,
c1_2(a1498,a1340) ).
cnf(clause122,negated_conjecture,
( ssSkP7(X0)
| c5_2(X0,a1376) ) ).
cnf(u2801,negated_conjecture,
ssSkP13(a1490) ).
cnf(u7413,negated_conjecture,
c4_2(a1361,a1357) ).
cnf(u12942,negated_conjecture,
c5_2(a1455,a1414) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN520-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 16:24:49 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.12 Running first-order theorem proving
% 0.10/0.12 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.94/1.25 % (3495113)Input is clausal, will run a generic CNF schedule.
% 5.94/1.25 % (3495121)lrs+10_1_sil=8000:sp=occurrence:random_seed=2173709418:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.94/1.25 % (3495123)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=865476277:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.94/1.25 % (3495124)dis-21_1_sil=8000:lcm=predicate:random_seed=1539601050: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)
% 5.94/1.25 % (3495119)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1241287261:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.94/1.25 % (3495118)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=2733652662:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.94/1.25 % (3495120)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=534274610:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.94/1.25 % (3495122)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=327747118:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.94/1.25 % (3495121)Instruction limit reached!
% 5.94/1.25 % (3495121)------------------------------
% 5.94/1.25 % (3495121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.94/1.25 % (3495121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.25 % (3495121)CaDiCaL version: 2.1.3
% 5.94/1.25 % (3495121)Termination reason: Instruction limit
% 5.94/1.25 % (3495121)Termination phase: Saturation
% 5.94/1.25 % (3495121)Time elapsed: 0.034 s
% 5.94/1.25 % (3495121)Peak memory usage: 90 MB
% 5.94/1.25 % (3495121)Instructions burned: 107 (million)
% 5.94/1.25 % (3495123)Refutation not found, incomplete strategy
% 5.94/1.25 % (3495123)------------------------------
% 5.94/1.25 % (3495123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.94/1.25 % (3495123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.25 % (3495123)CaDiCaL version: 2.1.3
% 5.94/1.25 % (3495123)Termination reason: Refutation not found, incomplete strategy
% 5.94/1.25 % (3495123)Time elapsed: 0.035 s
% 5.94/1.25 % (3495123)Peak memory usage: 91 MB
% 5.94/1.25 % (3495123)Instructions burned: 111 (million)
% 5.94/1.25 % (3495124)Instruction limit reached!
% 5.94/1.25 % (3495124)------------------------------
% 5.94/1.25 % (3495124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.94/1.25 % (3495124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.25 % (3495124)CaDiCaL version: 2.1.3
% 5.94/1.25 % (3495124)Termination reason: Instruction limit
% 5.94/1.25 % (3495124)Termination phase: Saturation
% 5.94/1.25 % (3495124)Time elapsed: 0.035 s
% 5.94/1.25 % (3495124)Peak memory usage: 90 MB
% 5.94/1.25 % (3495124)Instructions burned: 117 (million)
% 5.94/1.25 % (3495122)Instruction limit reached!
% 5.94/1.25 % (3495122)------------------------------
% 5.94/1.25 % (3495122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.94/1.25 % (3495122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.25 % (3495122)CaDiCaL version: 2.1.3
% 5.94/1.25 % (3495122)Termination reason: Instruction limit
% 5.94/1.25 % (3495122)Termination phase: Saturation
% 5.94/1.25 % (3495122)Time elapsed: 0.035 s
% 5.94/1.25 % (3495122)Peak memory usage: 90 MB
% 5.94/1.25 % (3495122)Instructions burned: 114 (million)
% 5.94/1.25 % (3495133)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3649024405:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 5.94/1.25 % (3495132)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=3301089798:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.94/1.25 % (3495134)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3635088375:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 5.94/1.25 % (3495133)Refutation not found, incomplete strategy
% 5.94/1.25 % (3495133)------------------------------
% 5.94/1.25 % (3495133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495133)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495133)Termination reason: Refutation not found, incomplete strategy
% 7.04/1.43 % (3495133)Time elapsed: 0.019 s
% 7.04/1.43 % (3495133)Peak memory usage: 90 MB
% 7.04/1.43 % (3495133)Instructions burned: 64 (million)
% 7.04/1.43 % (3495123)------------------------------
% 7.04/1.43 % (3495123)------------------------------
% 7.04/1.43 % (3495132)Instruction limit reached!
% 7.04/1.43 % (3495132)------------------------------
% 7.04/1.43 % (3495132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495132)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495132)Termination reason: Instruction limit
% 7.04/1.43 % (3495132)Termination phase: Saturation
% 7.04/1.43 % (3495132)Time elapsed: 0.046 s
% 7.04/1.43 % (3495132)Peak memory usage: 91 MB
% 7.04/1.43 % (3495132)Instructions burned: 144 (million)
% 7.04/1.43 % (3495134)Instruction limit reached!
% 7.04/1.43 % (3495134)------------------------------
% 7.04/1.43 % (3495134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495134)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495134)Termination reason: Instruction limit
% 7.04/1.43 % (3495134)Termination phase: Saturation
% 7.04/1.43 % (3495134)Time elapsed: 0.070 s
% 7.04/1.43 % (3495134)Peak memory usage: 91 MB
% 7.04/1.43 % (3495134)Instructions burned: 221 (million)
% 7.04/1.43 % (3495139)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=836031404:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 7.04/1.43 % (3495138)lrs+10_64_to=lpo:sil=8000:random_seed=1676187426:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.04/1.43 % (3495140)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4276035146:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 7.04/1.43 % (3495133)------------------------------
% 7.04/1.43 % (3495133)------------------------------
% 7.04/1.43 % (3495138)Instruction limit reached!
% 7.04/1.43 % (3495138)------------------------------
% 7.04/1.43 % (3495138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495138)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495138)Termination reason: Instruction limit
% 7.04/1.43 % (3495138)Termination phase: Saturation
% 7.04/1.43 % (3495138)Time elapsed: 0.041 s
% 7.04/1.43 % (3495138)Peak memory usage: 90 MB
% 7.04/1.43 % (3495138)Instructions burned: 128 (million)
% 7.04/1.43 % (3495139)Instruction limit reached!
% 7.04/1.43 % (3495139)------------------------------
% 7.04/1.43 % (3495139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495139)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495139)Termination reason: Instruction limit
% 7.04/1.43 % (3495139)Termination phase: Saturation
% 7.04/1.43 % (3495139)Time elapsed: 0.063 s
% 7.04/1.43 % (3495139)Peak memory usage: 91 MB
% 7.04/1.43 % (3495139)Instructions burned: 196 (million)
% 7.04/1.43 % (3495140)Instruction limit reached!
% 7.04/1.43 % (3495140)------------------------------
% 7.04/1.43 % (3495140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495140)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495140)Termination reason: Instruction limit
% 7.04/1.43 % (3495140)Termination phase: Saturation
% 7.04/1.43 % (3495140)Time elapsed: 0.054 s
% 7.04/1.43 % (3495140)Peak memory usage: 92 MB
% 7.04/1.43 % (3495140)Instructions burned: 157 (million)
% 7.04/1.43 % (3495119)Refutation not found, incomplete strategy
% 7.04/1.43 % (3495119)------------------------------
% 7.04/1.43 % (3495119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495119)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495119)Termination reason: Refutation not found, incomplete strategy
% 7.04/1.43 % (3495119)Time elapsed: 0.392 s
% 7.04/1.43 % (3495119)Peak memory usage: 132 MB
% 7.04/1.43 % (3495119)Instructions burned: 1067 (million)
% 7.04/1.43 % (3495144)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1809165419:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 7.04/1.43 % (3495145)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=490767207:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 7.04/1.43 % (3495146)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1676175814:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 7.04/1.43 % (3495145)Refutation not found, incomplete strategy
% 7.04/1.43 % (3495145)------------------------------
% 7.04/1.43 % (3495145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495145)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495145)Termination reason: Refutation not found, incomplete strategy
% 7.04/1.43 % (3495145)Time elapsed: 0.015 s
% 7.04/1.43 % (3495145)Peak memory usage: 90 MB
% 7.04/1.43 % (3495145)Instructions burned: 45 (million)
% 7.04/1.43 % (3495146)Instruction limit reached!
% 7.04/1.43 % (3495146)------------------------------
% 7.04/1.43 % (3495146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495146)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495146)Termination reason: Instruction limit
% 7.04/1.43 % (3495146)Termination phase: Saturation
% 7.04/1.43 % (3495146)Time elapsed: 0.034 s
% 7.04/1.43 % (3495146)Peak memory usage: 90 MB
% 7.04/1.43 % (3495146)Instructions burned: 107 (million)
% 7.04/1.43 % (3495147)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=867044787:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2995 on theBenchmark for (2995ds/242Mi)
% 7.04/1.43 % (3495147)Refutation not found, incomplete strategy
% 7.04/1.43 % (3495147)------------------------------
% 7.04/1.43 % (3495147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495147)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495147)Termination reason: Refutation not found, incomplete strategy
% 7.04/1.43 % (3495147)Time elapsed: 0.042 s
% 7.04/1.43 % (3495147)Peak memory usage: 89 MB
% 7.04/1.43 % (3495147)Instructions burned: 136 (million)
% 7.04/1.43 % (3495119)------------------------------
% 7.04/1.43 % (3495119)------------------------------
% 7.04/1.43 % (3495151)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3444953902:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 7.04/1.43 % (3495145)------------------------------
% 7.04/1.43 % (3495145)------------------------------
% 7.04/1.43 % (3495154)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3987622485:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 7.04/1.43 % (3495147)------------------------------
% 7.04/1.43 % (3495147)------------------------------
% 7.04/1.43 % (3495154)Instruction limit reached!
% 7.04/1.43 % (3495154)------------------------------
% 7.04/1.43 % (3495154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495154)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495154)Termination reason: Instruction limit
% 7.04/1.43 % (3495154)Termination phase: Saturation
% 7.04/1.43 % (3495154)Time elapsed: 0.042 s
% 7.04/1.43 % (3495154)Peak memory usage: 91 MB
% 7.04/1.43 % (3495154)Instructions burned: 135 (million)
% 7.04/1.43 % (3495155)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3199424029:i=499:bd=all_2993 on theBenchmark for (2993ds/499Mi)
% 7.04/1.43 % (3495157)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3591458792:i=191:fgj=on:bd=all_2992 on theBenchmark for (2992ds/191Mi)
% 7.04/1.43 % (3495159)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2024887614:i=264:kws=precedence:fsr=off_2992 on theBenchmark for (2992ds/264Mi)
% 7.04/1.43 % (3495157)Instruction limit reached!
% 7.04/1.43 % (3495157)------------------------------
% 7.04/1.43 % (3495157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495157)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495157)Termination reason: Instruction limit
% 7.04/1.43 % (3495157)Termination phase: Saturation
% 7.04/1.43 % (3495157)Time elapsed: 0.061 s
% 7.04/1.43 % (3495157)Peak memory usage: 92 MB
% 7.04/1.43 % (3495157)Instructions burned: 192 (million)
% 7.04/1.43 % (3495155)First to succeed.
% 7.04/1.43 % (3495155)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3495113"
% 7.04/1.43 % (3495159)Instruction limit reached!
% 7.04/1.43 % (3495159)------------------------------
% 7.04/1.43 % (3495159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495159)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495159)Termination reason: Instruction limit
% 7.04/1.43 % (3495159)Termination phase: Saturation
% 7.04/1.43 % (3495159)Time elapsed: 0.068 s
% 7.04/1.43 % (3495159)Peak memory usage: 91 MB
% 7.04/1.43 % (3495159)Instructions burned: 264 (million)
% 7.04/1.43 % (3495162)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1945356089:cond=on:i=156:bs=on:gtg=exists_all:er=known_2990 on theBenchmark for (2990ds/156Mi)
% 7.04/1.43 % (3495163)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1534154185:i=3256:kws=precedence:bd=preordered:av=off_2990 on theBenchmark for (2990ds/3256Mi)
% 7.04/1.43 % (3495162)Instruction limit reached!
% 7.04/1.43 % (3495162)------------------------------
% 7.04/1.43 % (3495162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.43 % (3495162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.43 % (3495162)CaDiCaL version: 2.1.3
% 7.04/1.43 % (3495162)Termination reason: Instruction limit
% 7.04/1.43 % (3495162)Termination phase: Saturation
% 7.04/1.43 % (3495162)Time elapsed: 0.048 s
% 7.04/1.43 % (3495162)Peak memory usage: 92 MB
% 7.04/1.43 % (3495162)Instructions burned: 156 (million)
% 7.04/1.43 % SZS status Satisfiable for theBenchmark
% 7.04/1.43 % SZS output start Saturation.
% See solution above
% 8.04/1.52 % SZS output start Definitions and Model Updates.
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkC12 := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkP8(X0) := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkP4(X0) := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkC7 := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkC3 := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkP1(X0) := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkP0(X0) := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkC1 := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkC15 := $true
% 8.04/1.52 for all inputs,
% 8.04/1.52 define ssSkC13 := $true
% 8.04/1.52 % SZS output end Definitions and Model Updates.
% 8.04/1.52 % (3495155)------------------------------
% 8.04/1.52 % (3495155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.04/1.52 % (3495155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.04/1.52 % (3495155)CaDiCaL version: 2.1.3
% 8.04/1.52 % (3495155)Termination reason: Satisfiable
% 8.04/1.52 % (3495155)Time elapsed: 0.153 s
% 8.04/1.52 % (3495155)Peak memory usage: 95 MB
% 8.04/1.52 % (3495155)Instructions burned: 474 (million)
% 8.04/1.52 % (3495155)------------------------------
% 8.04/1.52 % (3495155)------------------------------
% 8.04/1.52 % (3495113)Success in time 1.117 s
% 8.04/1.52 % Vampire exiting
%------------------------------------------------------------------------------