%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL645+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 11:59:11 AM UTC 2026
% Result : CounterSatisfiable 0.07s 0.40s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1228,axiom,
~ p57(sK56(X0)) ).
cnf(u1231,axiom,
~ sP54(X0) ).
cnf(u1234,axiom,
~ p56(sK58(X0)) ).
cnf(u1237,axiom,
~ sP53(X0) ).
cnf(u1240,axiom,
~ p55(sK60(X0)) ).
cnf(u1243,axiom,
~ sP52(X0) ).
cnf(u1246,axiom,
~ p54(sK62(X0)) ).
cnf(u1249,axiom,
~ sP51(X0) ).
cnf(u1252,axiom,
~ p53(sK64(X0)) ).
cnf(u1255,axiom,
~ sP50(X0) ).
cnf(u1258,axiom,
~ p52(sK66(X0)) ).
cnf(u1261,axiom,
~ sP49(X0) ).
cnf(u1264,axiom,
~ p51(sK68(X0)) ).
cnf(u1267,axiom,
~ sP48(X0) ).
cnf(u1270,axiom,
~ p50(sK70(X0)) ).
cnf(u1273,axiom,
~ sP47(X0) ).
cnf(u1276,axiom,
~ p49(sK72(X0)) ).
cnf(u1279,axiom,
~ sP46(X0) ).
cnf(u1282,axiom,
~ p48(sK74(X0)) ).
cnf(u1285,axiom,
~ sP45(X0) ).
cnf(u1288,axiom,
~ p47(sK76(X0)) ).
cnf(u1291,axiom,
~ sP44(X0) ).
cnf(u1294,axiom,
~ p46(sK78(X0)) ).
cnf(u1297,axiom,
~ sP43(X0) ).
cnf(u1300,axiom,
~ p45(sK80(X0)) ).
cnf(u1303,axiom,
~ sP42(X0) ).
cnf(u1306,axiom,
~ p44(sK82(X0)) ).
cnf(u1309,axiom,
~ sP41(X0) ).
cnf(u1312,axiom,
~ p43(sK84(X0)) ).
cnf(u1315,axiom,
~ sP40(X0) ).
cnf(u1318,axiom,
~ p42(sK86(X0)) ).
cnf(u1321,axiom,
~ sP39(X0) ).
cnf(u1324,axiom,
~ p41(sK88(X0)) ).
cnf(u1327,axiom,
~ sP38(X0) ).
cnf(u1330,axiom,
~ p40(sK90(X0)) ).
cnf(u1333,axiom,
~ sP37(X0) ).
cnf(u1336,axiom,
~ p39(sK92(X0)) ).
cnf(u1339,axiom,
~ sP36(X0) ).
cnf(u1342,axiom,
~ p38(sK94(X0)) ).
cnf(u1345,axiom,
~ sP35(X0) ).
cnf(u1348,axiom,
~ p37(sK96(X0)) ).
cnf(u1351,axiom,
~ sP34(X0) ).
cnf(u1354,axiom,
~ p36(sK98(X0)) ).
cnf(u1357,axiom,
~ sP33(X0) ).
cnf(u1360,axiom,
~ p35(sK100(X0)) ).
cnf(u1363,axiom,
~ sP32(X0) ).
cnf(u1366,axiom,
~ p34(sK102(X0)) ).
cnf(u1369,axiom,
~ sP31(X0) ).
cnf(u1372,axiom,
~ p33(sK104(X0)) ).
cnf(u1375,axiom,
~ sP30(X0) ).
cnf(u1378,axiom,
~ p32(sK106(X0)) ).
cnf(u1381,axiom,
~ sP29(X0) ).
cnf(u1384,axiom,
~ p31(sK108(X0)) ).
cnf(u1387,axiom,
~ sP28(X0) ).
cnf(u1390,axiom,
~ p29(sK110(X0)) ).
cnf(u1393,axiom,
~ sP27(X0) ).
cnf(u1396,axiom,
~ p28(sK112(X0)) ).
cnf(u1399,axiom,
~ sP26(X0) ).
cnf(u1402,axiom,
~ p27(sK114(X0)) ).
cnf(u1405,axiom,
~ sP25(X0) ).
cnf(u1408,axiom,
~ p26(sK116(X0)) ).
cnf(u1411,axiom,
~ sP24(X0) ).
cnf(u1414,axiom,
~ p25(sK118(X0)) ).
cnf(u1417,axiom,
~ sP23(X0) ).
cnf(u1420,axiom,
~ p24(sK120(X0)) ).
cnf(u1423,axiom,
~ sP22(X0) ).
cnf(u1426,axiom,
~ p23(sK122(X0)) ).
cnf(u1429,axiom,
~ sP21(X0) ).
cnf(u1432,axiom,
~ p22(sK124(X0)) ).
cnf(u1435,axiom,
~ sP20(X0) ).
cnf(u1438,axiom,
~ p21(sK126(X0)) ).
cnf(u1441,axiom,
~ sP19(X0) ).
cnf(u1444,axiom,
~ p20(sK128(X0)) ).
cnf(u1447,axiom,
~ sP18(X0) ).
cnf(u1450,axiom,
~ p19(sK130(X0)) ).
cnf(u1453,axiom,
~ sP17(X0) ).
cnf(u1456,axiom,
~ p18(sK132(X0)) ).
cnf(u1459,axiom,
~ sP16(X0) ).
cnf(u1462,axiom,
~ p17(sK134(X0)) ).
cnf(u1465,axiom,
~ sP15(X0) ).
cnf(u1468,axiom,
~ p16(sK136(X0)) ).
cnf(u1471,axiom,
~ sP14(X0) ).
cnf(u1474,axiom,
~ p15(sK138(X0)) ).
cnf(u1477,axiom,
~ sP13(X0) ).
cnf(u1480,axiom,
~ p14(sK140(X0)) ).
cnf(u1483,axiom,
~ sP12(X0) ).
cnf(u1486,axiom,
~ p13(sK142(X0)) ).
cnf(u1489,axiom,
~ sP11(X0) ).
cnf(u1492,axiom,
~ p12(sK144(X0)) ).
cnf(u1495,axiom,
~ sP10(X0) ).
cnf(u1498,axiom,
~ p11(sK146(X0)) ).
cnf(u1501,axiom,
~ sP9(X0) ).
cnf(u1504,axiom,
~ p10(sK148(X0)) ).
cnf(u1507,axiom,
~ sP8(X0) ).
cnf(u1510,negated_conjecture,
~ r1(sK302,X328) ).
cnf(u1516,axiom,
~ p9(sK150(X0)) ).
cnf(u1519,axiom,
~ sP7(X0) ).
cnf(u1522,axiom,
~ p8(sK152(X0)) ).
cnf(u1525,axiom,
~ sP6(X0) ).
cnf(u1535,axiom,
~ p7(sK154(X0)) ).
cnf(u1538,axiom,
~ sP5(X0) ).
cnf(u1541,axiom,
~ p6(sK156(X0)) ).
cnf(u1544,axiom,
~ sP4(X0) ).
cnf(u1547,axiom,
~ p5(sK158(X0)) ).
cnf(u1550,axiom,
~ sP3(X0) ).
cnf(u1553,axiom,
~ p4(sK160(X0)) ).
cnf(u1556,axiom,
~ sP2(X0) ).
cnf(u1559,axiom,
~ p3(sK162(X0)) ).
cnf(u1562,axiom,
~ sP1(X0) ).
cnf(u1565,axiom,
~ p2(sK164(X0)) ).
cnf(u1568,axiom,
~ sP0(X0) ).
cnf(u1571,negated_conjecture,
~ r1(sK301,X326) ).
cnf(u1590,negated_conjecture,
~ p1(X653) ).
cnf(u1593,negated_conjecture,
~ p2(sK438(X653)) ).
cnf(u1596,negated_conjecture,
~ p2(X653) ).
cnf(u1599,negated_conjecture,
( ~ r1(sK165,X653)
| ~ p2(X653)
| ~ p2(sK438(X653))
| ~ p1(X653)
| p2(X654)
| ~ r1(X653,X654) ) ).
cnf(u1628,negated_conjecture,
~ p3(X629) ).
cnf(u1631,negated_conjecture,
~ p4(sK428(X629)) ).
cnf(u1634,negated_conjecture,
~ p4(X629) ).
cnf(u1637,negated_conjecture,
( ~ r1(sK165,X629)
| ~ p4(X629)
| ~ p4(sK428(X629))
| ~ p3(X629)
| p4(X630)
| ~ r1(X629,X630) ) ).
cnf(u1658,negated_conjecture,
~ p5(X605) ).
cnf(u1661,negated_conjecture,
~ p6(sK418(X605)) ).
cnf(u1664,negated_conjecture,
~ p6(X605) ).
cnf(u1667,negated_conjecture,
( ~ r1(sK165,X605)
| ~ p6(X605)
| ~ p6(sK418(X605))
| ~ p5(X605)
| p6(X606)
| ~ r1(X605,X606) ) ).
cnf(u1688,negated_conjecture,
~ p7(X581) ).
cnf(u1691,negated_conjecture,
~ p8(sK408(X581)) ).
cnf(u1694,negated_conjecture,
~ p8(X581) ).
cnf(u1697,negated_conjecture,
( ~ r1(sK165,X581)
| ~ p8(X581)
| ~ p8(sK408(X581))
| ~ p7(X581)
| p8(X582)
| ~ r1(X581,X582) ) ).
cnf(u1718,negated_conjecture,
~ p9(X557) ).
cnf(u1721,negated_conjecture,
~ p10(sK398(X557)) ).
cnf(u1724,negated_conjecture,
~ p10(X557) ).
cnf(u1727,negated_conjecture,
( ~ r1(sK165,X557)
| ~ p10(X557)
| ~ p10(sK398(X557))
| ~ p9(X557)
| p10(X558)
| ~ r1(X557,X558) ) ).
cnf(u1748,negated_conjecture,
~ p11(X533) ).
cnf(u1751,negated_conjecture,
~ p12(sK388(X533)) ).
cnf(u1754,negated_conjecture,
~ p12(X533) ).
cnf(u1757,negated_conjecture,
( ~ r1(sK165,X533)
| ~ p12(X533)
| ~ p12(sK388(X533))
| ~ p11(X533)
| p12(X534)
| ~ r1(X533,X534) ) ).
cnf(u1778,negated_conjecture,
~ p13(X509) ).
cnf(u1781,negated_conjecture,
~ p14(sK378(X509)) ).
cnf(u1784,negated_conjecture,
~ p14(X509) ).
cnf(u1787,negated_conjecture,
( ~ r1(sK165,X509)
| ~ p14(X509)
| ~ p14(sK378(X509))
| ~ p13(X509)
| p14(X510)
| ~ r1(X509,X510) ) ).
cnf(u1805,negated_conjecture,
~ p15(X485) ).
cnf(u1808,negated_conjecture,
~ p16(sK368(X485)) ).
cnf(u1811,negated_conjecture,
~ p16(X485) ).
cnf(u1814,negated_conjecture,
( ~ r1(sK165,X485)
| ~ p16(X485)
| ~ p16(sK368(X485))
| ~ p15(X485)
| p16(X486)
| ~ r1(X485,X486) ) ).
cnf(u1833,negated_conjecture,
~ p17(X461) ).
cnf(u1836,negated_conjecture,
~ p18(sK358(X461)) ).
cnf(u1839,negated_conjecture,
~ p18(X461) ).
cnf(u1842,negated_conjecture,
( ~ r1(sK165,X461)
| ~ p18(X461)
| ~ p18(sK358(X461))
| ~ p17(X461)
| p18(X462)
| ~ r1(X461,X462) ) ).
cnf(u1863,negated_conjecture,
~ p19(X437) ).
cnf(u1866,negated_conjecture,
~ p20(sK348(X437)) ).
cnf(u1869,negated_conjecture,
~ p20(X437) ).
cnf(u1872,negated_conjecture,
( ~ r1(sK165,X437)
| ~ p20(X437)
| ~ p20(sK348(X437))
| ~ p19(X437)
| p20(X438)
| ~ r1(X437,X438) ) ).
cnf(u1893,negated_conjecture,
~ p21(X413) ).
cnf(u1896,negated_conjecture,
~ p22(sK338(X413)) ).
cnf(u1899,negated_conjecture,
~ p22(X413) ).
cnf(u1902,negated_conjecture,
( ~ r1(sK165,X413)
| ~ p22(X413)
| ~ p22(sK338(X413))
| ~ p21(X413)
| p22(X414)
| ~ r1(X413,X414) ) ).
cnf(u1923,negated_conjecture,
~ p23(X389) ).
cnf(u1926,negated_conjecture,
~ p24(sK328(X389)) ).
cnf(u1929,negated_conjecture,
~ p24(X389) ).
cnf(u1932,negated_conjecture,
( ~ r1(sK165,X389)
| ~ p24(X389)
| ~ p24(sK328(X389))
| ~ p23(X389)
| p24(X390)
| ~ r1(X389,X390) ) ).
cnf(u1953,negated_conjecture,
~ p25(X365) ).
cnf(u1956,negated_conjecture,
~ p26(sK318(X365)) ).
cnf(u1959,negated_conjecture,
~ p26(X365) ).
cnf(u1962,negated_conjecture,
( ~ r1(sK165,X365)
| ~ p26(X365)
| ~ p26(sK318(X365))
| ~ p25(X365)
| p26(X366)
| ~ r1(X365,X366) ) ).
cnf(u1983,negated_conjecture,
~ p27(X341) ).
cnf(u1986,negated_conjecture,
~ p28(sK308(X341)) ).
cnf(u1989,negated_conjecture,
~ p28(X341) ).
cnf(u1992,negated_conjecture,
( ~ r1(sK165,X341)
| ~ p28(X341)
| ~ p28(sK308(X341))
| ~ p27(X341)
| p28(X342)
| ~ r1(X341,X342) ) ).
cnf(u2013,negated_conjecture,
~ p30(X313) ).
cnf(u2016,negated_conjecture,
~ p31(sK296(X313)) ).
cnf(u2019,negated_conjecture,
~ p31(X313) ).
cnf(u2022,negated_conjecture,
( ~ r1(sK165,X313)
| ~ p31(X313)
| ~ p31(sK296(X313))
| ~ p30(X313)
| p31(X314)
| ~ r1(X313,X314) ) ).
cnf(u2043,negated_conjecture,
~ p32(X289) ).
cnf(u2046,negated_conjecture,
~ p33(sK286(X289)) ).
cnf(u2049,negated_conjecture,
~ p33(X289) ).
cnf(u2052,negated_conjecture,
( ~ r1(sK165,X289)
| ~ p33(X289)
| ~ p33(sK286(X289))
| ~ p32(X289)
| p33(X290)
| ~ r1(X289,X290) ) ).
cnf(u2073,negated_conjecture,
~ p34(X265) ).
cnf(u2076,negated_conjecture,
~ p35(sK276(X265)) ).
cnf(u2079,negated_conjecture,
~ p35(X265) ).
cnf(u2082,negated_conjecture,
( ~ r1(sK165,X265)
| ~ p35(X265)
| ~ p35(sK276(X265))
| ~ p34(X265)
| p35(X266)
| ~ r1(X265,X266) ) ).
cnf(u2103,negated_conjecture,
~ p36(X241) ).
cnf(u2106,negated_conjecture,
~ p37(sK266(X241)) ).
cnf(u2109,negated_conjecture,
~ p37(X241) ).
cnf(u2112,negated_conjecture,
( ~ r1(sK165,X241)
| ~ p37(X241)
| ~ p37(sK266(X241))
| ~ p36(X241)
| p37(X242)
| ~ r1(X241,X242) ) ).
cnf(u2133,negated_conjecture,
~ p38(X217) ).
cnf(u2136,negated_conjecture,
~ p39(sK256(X217)) ).
cnf(u2139,negated_conjecture,
~ p39(X217) ).
cnf(u2142,negated_conjecture,
( ~ r1(sK165,X217)
| ~ p39(X217)
| ~ p39(sK256(X217))
| ~ p38(X217)
| p39(X218)
| ~ r1(X217,X218) ) ).
cnf(u2163,negated_conjecture,
~ p40(X193) ).
cnf(u2166,negated_conjecture,
~ p41(sK246(X193)) ).
cnf(u2169,negated_conjecture,
~ p41(X193) ).
cnf(u2172,negated_conjecture,
( ~ r1(sK165,X193)
| ~ p41(X193)
| ~ p41(sK246(X193))
| ~ p40(X193)
| p41(X194)
| ~ r1(X193,X194) ) ).
cnf(u2193,negated_conjecture,
~ p42(X169) ).
cnf(u2196,negated_conjecture,
~ p43(sK236(X169)) ).
cnf(u2199,negated_conjecture,
~ p43(X169) ).
cnf(u2202,negated_conjecture,
( ~ r1(sK165,X169)
| ~ p43(X169)
| ~ p43(sK236(X169))
| ~ p42(X169)
| p43(X170)
| ~ r1(X169,X170) ) ).
cnf(u2223,negated_conjecture,
~ p44(X145) ).
cnf(u2226,negated_conjecture,
~ p45(sK226(X145)) ).
cnf(u2229,negated_conjecture,
~ p45(X145) ).
cnf(u2232,negated_conjecture,
( ~ r1(sK165,X145)
| ~ p45(X145)
| ~ p45(sK226(X145))
| ~ p44(X145)
| p45(X146)
| ~ r1(X145,X146) ) ).
cnf(u2253,negated_conjecture,
~ p46(X121) ).
cnf(u2256,negated_conjecture,
~ p47(sK216(X121)) ).
cnf(u2259,negated_conjecture,
~ p47(X121) ).
cnf(u2262,negated_conjecture,
( ~ r1(sK165,X121)
| ~ p47(X121)
| ~ p47(sK216(X121))
| ~ p46(X121)
| p47(X122)
| ~ r1(X121,X122) ) ).
cnf(u2283,negated_conjecture,
~ p48(X97) ).
cnf(u2286,negated_conjecture,
~ p49(sK206(X97)) ).
cnf(u2289,negated_conjecture,
~ p49(X97) ).
cnf(u2292,negated_conjecture,
( ~ r1(sK165,X97)
| ~ p49(X97)
| ~ p49(sK206(X97))
| ~ p48(X97)
| p49(X98)
| ~ r1(X97,X98) ) ).
cnf(u2313,negated_conjecture,
~ p50(X73) ).
cnf(u2316,negated_conjecture,
~ p51(sK196(X73)) ).
cnf(u2319,negated_conjecture,
~ p51(X73) ).
cnf(u2322,negated_conjecture,
( ~ r1(sK165,X73)
| ~ p51(X73)
| ~ p51(sK196(X73))
| ~ p50(X73)
| p51(X74)
| ~ r1(X73,X74) ) ).
cnf(u2343,negated_conjecture,
~ p52(X49) ).
cnf(u2346,negated_conjecture,
~ p53(sK186(X49)) ).
cnf(u2349,negated_conjecture,
~ p53(X49) ).
cnf(u2352,negated_conjecture,
( ~ r1(sK165,X49)
| ~ p53(X49)
| ~ p53(sK186(X49))
| ~ p52(X49)
| p53(X50)
| ~ r1(X49,X50) ) ).
cnf(u2373,negated_conjecture,
~ p54(X25) ).
cnf(u2376,negated_conjecture,
~ p55(sK176(X25)) ).
cnf(u2379,negated_conjecture,
~ p55(X25) ).
cnf(u2382,negated_conjecture,
( ~ r1(sK165,X25)
| ~ p55(X25)
| ~ p55(sK176(X25))
| ~ p54(X25)
| p55(X26)
| ~ r1(X25,X26) ) ).
cnf(u2403,negated_conjecture,
~ p56(X1) ).
cnf(u2406,negated_conjecture,
~ p57(sK166(X1)) ).
cnf(u2409,negated_conjecture,
~ p57(X1) ).
cnf(u2412,negated_conjecture,
( ~ r1(sK165,X1)
| ~ p57(X1)
| ~ p57(sK166(X1))
| ~ p56(X1)
| p57(X2)
| ~ r1(X1,X2) ) ).
cnf(u295,axiom,
( ~ p41(sK88(X0))
| ~ sP38(X0) ) ).
cnf(u339,axiom,
( ~ p29(sK110(X0))
| ~ sP27(X0) ) ).
cnf(u367,axiom,
( ~ p22(sK124(X0))
| ~ sP20(X0) ) ).
cnf(u411,axiom,
( ~ p11(sK146(X0))
| ~ sP9(X0) ) ).
cnf(u327,axiom,
( ~ p33(sK104(X0))
| ~ sP30(X0) ) ).
cnf(u283,axiom,
( ~ p44(sK82(X0))
| ~ sP41(X0) ) ).
cnf(u343,axiom,
( ~ p28(sK112(X0))
| ~ sP26(X0) ) ).
cnf(u387,axiom,
( ~ p17(sK134(X0))
| ~ sP15(X0) ) ).
cnf(u415,axiom,
( ~ p10(sK148(X0))
| ~ sP8(X0) ) ).
cnf(u239,axiom,
( ~ p55(sK60(X0))
| ~ sP52(X0) ) ).
cnf(u251,axiom,
( ~ p52(sK66(X0))
| ~ sP49(X0) ) ).
cnf(u259,axiom,
( ~ p50(sK70(X0))
| ~ sP47(X0) ) ).
cnf(u287,axiom,
( ~ p43(sK84(X0))
| ~ sP40(X0) ) ).
cnf(u331,axiom,
( ~ p32(sK106(X0))
| ~ sP29(X0) ) ).
cnf(u391,axiom,
( ~ p16(sK136(X0))
| ~ sP14(X0) ) ).
cnf(u843,negated_conjecture,
~ p15(sK302) ).
cnf(u271,axiom,
( ~ p47(sK76(X0))
| ~ sP44(X0) ) ).
cnf(u263,axiom,
( ~ p49(sK72(X0))
| ~ sP46(X0) ) ).
cnf(u435,axiom,
( ~ p5(sK158(X0))
| ~ sP3(X0) ) ).
cnf(u335,axiom,
( ~ p31(sK108(X0))
| ~ sP28(X0) ) ).
cnf(u351,axiom,
( ~ p26(sK116(X0))
| ~ sP24(X0) ) ).
cnf(u847,negated_conjecture,
r1(sK165,sK301) ).
cnf(u231,axiom,
( ~ p57(sK56(X0))
| ~ sP54(X0) ) ).
cnf(u319,axiom,
( ~ p35(sK100(X0))
| ~ sP32(X0) ) ).
cnf(u307,axiom,
( ~ p38(sK94(X0))
| ~ sP35(X0) ) ).
cnf(u379,axiom,
( ~ p19(sK130(X0))
| ~ sP17(X0) ) ).
cnf(u439,axiom,
( ~ p4(sK160(X0))
| ~ sP2(X0) ) ).
cnf(u235,axiom,
( ~ p56(sK58(X0))
| ~ sP53(X0) ) ).
cnf(u311,axiom,
( ~ p37(sK96(X0))
| ~ sP34(X0) ) ).
cnf(u355,axiom,
( ~ p25(sK118(X0))
| ~ sP23(X0) ) ).
cnf(u383,axiom,
( ~ p18(sK132(X0))
| ~ sP16(X0) ) ).
cnf(u427,axiom,
( ~ p7(sK154(X0))
| ~ sP5(X0) ) ).
cnf(u299,axiom,
( ~ p40(sK90(X0))
| ~ sP37(X0) ) ).
cnf(u359,axiom,
( ~ p24(sK120(X0))
| ~ sP22(X0) ) ).
cnf(u403,axiom,
( ~ p13(sK142(X0))
| ~ sP11(X0) ) ).
cnf(u431,axiom,
( ~ p6(sK156(X0))
| ~ sP4(X0) ) ).
cnf(u275,axiom,
( ~ p46(sK78(X0))
| ~ sP43(X0) ) ).
cnf(u303,axiom,
( ~ p39(sK92(X0))
| ~ sP36(X0) ) ).
cnf(u347,axiom,
( ~ p27(sK114(X0))
| ~ sP25(X0) ) ).
cnf(u407,axiom,
( ~ p12(sK144(X0))
| ~ sP10(X0) ) ).
cnf(u243,axiom,
( ~ p54(sK62(X0))
| ~ sP51(X0) ) ).
cnf(u279,axiom,
( ~ p45(sK80(X0))
| ~ sP42(X0) ) ).
cnf(u323,axiom,
( ~ p34(sK102(X0))
| ~ sP31(X0) ) ).
cnf(u395,axiom,
( ~ p15(sK138(X0))
| ~ sP13(X0) ) ).
cnf(u247,axiom,
( ~ p53(sK64(X0))
| ~ sP50(X0) ) ).
cnf(u267,axiom,
( ~ p48(sK74(X0))
| ~ sP45(X0) ) ).
cnf(u844,negated_conjecture,
r1(sK165,sK302) ).
cnf(u399,axiom,
( ~ p14(sK140(X0))
| ~ sP12(X0) ) ).
cnf(u842,negated_conjecture,
( ~ r1(sK302,X328)
| p15(X328) ) ).
cnf(u845,negated_conjecture,
( ~ r1(sK301,X326)
| p15(X326) ) ).
cnf(u371,axiom,
( ~ p21(sK126(X0))
| ~ sP19(X0) ) ).
cnf(u443,axiom,
( ~ p3(sK162(X0))
| ~ sP1(X0) ) ).
cnf(u846,negated_conjecture,
~ p15(sK301) ).
cnf(u315,axiom,
( ~ p36(sK98(X0))
| ~ sP33(X0) ) ).
cnf(u375,axiom,
( ~ p20(sK128(X0))
| ~ sP18(X0) ) ).
cnf(u419,axiom,
( ~ p9(sK150(X0))
| ~ sP7(X0) ) ).
cnf(u447,axiom,
( ~ p2(sK164(X0))
| ~ sP0(X0) ) ).
cnf(u291,axiom,
( ~ p42(sK86(X0))
| ~ sP39(X0) ) ).
cnf(u363,axiom,
( ~ p23(sK122(X0))
| ~ sP21(X0) ) ).
cnf(u423,axiom,
( ~ p8(sK152(X0))
| ~ sP6(X0) ) ).
cnf(u255,axiom,
( ~ p51(sK68(X0))
| ~ sP48(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL645+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 16:12:35 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.40 % (2559756)Will run a generic schedule for satisfiability detection.
% 0.07/0.40 % (2559762)% WARNING: option uhcvi not known.
% 0.07/0.40 % (2559765)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=766946978:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.07/0.40 % (2559767)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1204601365:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.07/0.40 % (2559761)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3188998198_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.40 % (2559763)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3627362972:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.07/0.40 % (2559762)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3456829498:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.07/0.40 % (2559764)dis+10_1_sil=32000:sp=arity:random_seed=1036352190:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.07/0.40 % (2559766)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=472476230:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.07/0.40 % (2559763) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2559756-2559763"...
% 0.07/0.40 % (2559763)...printing done.
% 0.07/0.40 % (2559764)Instruction limit reached!
% 0.07/0.40 % (2559764)------------------------------
% 0.07/0.40 % (2559764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.40 % (2559764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.40 % (2559764)CaDiCaL version: 2.1.3
% 0.07/0.40 % (2559764)Termination reason: Instruction limit
% 0.07/0.40 % (2559764)Termination phase: Saturation
% 0.07/0.40 % (2559764)Time elapsed: 0.031 s
% 0.07/0.40 % (2559764)Peak memory usage: 15 MB
% 0.07/0.40 % (2559764)Instructions burned: 105 (million)
% 0.07/0.40 % SZS status CounterSatisfiable for theBenchmark
% 0.07/0.40 % SZS output start Saturation.
% See solution above
% 0.07/0.40 % SZS output start Definitions and Model Updates.
% 0.07/0.40 % SZS output end Definitions and Model Updates.
% 0.07/0.40 % (2559763)------------------------------
% 0.07/0.40 % (2559763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.40 % (2559763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.40 % (2559763)CaDiCaL version: 2.1.3
% 0.07/0.40 % (2559763)Termination reason: Satisfiable
% 0.07/0.40 % (2559763)Time elapsed: 0.029 s
% 0.07/0.40 % (2559763)Peak memory usage: 15 MB
% 0.07/0.40 % (2559763)Instructions burned: 97 (million)
% 0.07/0.40 % (2559756)Success in time 0.066 s
% 0.07/0.40 % Vampire exiting
%------------------------------------------------------------------------------