%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL645+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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.17s 0.50s
% Output : Saturation 0.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u788,negated_conjecture,
( ~ p1(X424)
| ~ r1(sK105,X421)
| ~ r1(X421,X424)
| ~ p1(X423)
| ~ r1(sK282(X421),X423)
| p2(X421) ) ).
cnf(u791,negated_conjecture,
( ~ p2(sK281(X418))
| ~ p2(X418)
| ~ r1(sK105,X418)
| p1(sK280(X418)) ) ).
cnf(u795,negated_conjecture,
( ~ p1(X424)
| ~ r1(sK105,X421)
| ~ r1(X421,X424)
| r1(X421,sK282(X421))
| p2(X421) ) ).
cnf(u804,negated_conjecture,
( ~ p2(sK281(X418))
| ~ p2(X418)
| ~ r1(sK105,X418)
| r1(X418,sK280(X418)) ) ).
cnf(u817,negated_conjecture,
( ~ p1(X413)
| ~ p2(X413)
| ~ p2(sK278(X413))
| ~ r1(sK105,X413)
| p2(X414)
| ~ r1(X413,X414) ) ).
cnf(u821,negated_conjecture,
( ~ p2(sK279(X416))
| ~ r1(sK105,X416)
| sP0(X416)
| p2(X416) ) ).
cnf(u825,negated_conjecture,
( ~ r1(sK105,X416)
| r1(X416,sK279(X416))
| sP0(X416)
| p2(X416) ) ).
cnf(u829,negated_conjecture,
( ~ p1(X413)
| ~ p2(X413)
| r1(X413,sK278(X413))
| ~ r1(sK105,X413)
| p2(X414)
| ~ r1(X413,X414) ) ).
cnf(u835,negated_conjecture,
( ~ p2(X412)
| ~ r1(sK105,X409)
| ~ r1(X409,X412)
| ~ p2(X411)
| ~ r1(sK277(X409),X411)
| p3(X409) ) ).
cnf(u842,negated_conjecture,
( ~ p2(X412)
| ~ r1(sK105,X409)
| ~ r1(X409,X412)
| r1(X409,sK277(X409))
| p3(X409) ) ).
cnf(u861,negated_conjecture,
( ~ r1(sK105,X404)
| p2(X404)
| sP1(X404)
| p3(X404) ) ).
cnf(u864,negated_conjecture,
( ~ p2(X401)
| ~ p3(X401)
| ~ p3(sK273(X401))
| ~ r1(sK105,X401)
| p3(X402)
| ~ r1(X401,X402) ) ).
cnf(u868,negated_conjecture,
( ~ p3(sK274(X404))
| ~ r1(sK105,X404)
| sP1(X404)
| p3(X404) ) ).
cnf(u872,negated_conjecture,
( ~ r1(sK105,X404)
| r1(X404,sK274(X404))
| sP1(X404)
| p3(X404) ) ).
cnf(u882,negated_conjecture,
( ~ p3(X400)
| ~ r1(sK105,X397)
| ~ r1(X397,X400)
| ~ p3(X399)
| ~ r1(sK272(X397),X399)
| p4(X397) ) ).
cnf(u889,negated_conjecture,
( ~ p3(X400)
| ~ r1(sK105,X397)
| ~ r1(X397,X400)
| r1(X397,sK272(X397))
| p4(X397) ) ).
cnf(u908,negated_conjecture,
( ~ r1(sK105,X392)
| p3(X392)
| sP2(X392)
| p4(X392) ) ).
cnf(u911,negated_conjecture,
( ~ p3(X389)
| ~ p4(X389)
| ~ p4(sK268(X389))
| ~ r1(sK105,X389)
| p4(X390)
| ~ r1(X389,X390) ) ).
cnf(u915,negated_conjecture,
( ~ p4(sK269(X392))
| ~ r1(sK105,X392)
| sP2(X392)
| p4(X392) ) ).
cnf(u919,negated_conjecture,
( ~ r1(sK105,X392)
| r1(X392,sK269(X392))
| sP2(X392)
| p4(X392) ) ).
cnf(u929,negated_conjecture,
( ~ p4(X388)
| ~ r1(sK105,X385)
| ~ r1(X385,X388)
| ~ p4(X387)
| ~ r1(sK267(X385),X387)
| p5(X385) ) ).
cnf(u936,negated_conjecture,
( ~ p4(X388)
| ~ r1(sK105,X385)
| ~ r1(X385,X388)
| r1(X385,sK267(X385))
| p5(X385) ) ).
cnf(u955,negated_conjecture,
( ~ r1(sK105,X380)
| p4(X380)
| sP3(X380)
| p5(X380) ) ).
cnf(u958,negated_conjecture,
( ~ p4(X377)
| ~ p5(X377)
| ~ p5(sK263(X377))
| ~ r1(sK105,X377)
| p5(X378)
| ~ r1(X377,X378) ) ).
cnf(u962,negated_conjecture,
( ~ p5(sK264(X380))
| ~ r1(sK105,X380)
| sP3(X380)
| p5(X380) ) ).
cnf(u966,negated_conjecture,
( ~ r1(sK105,X380)
| r1(X380,sK264(X380))
| sP3(X380)
| p5(X380) ) ).
cnf(u976,negated_conjecture,
( ~ p5(X376)
| ~ r1(sK105,X373)
| ~ r1(X373,X376)
| ~ p5(X375)
| ~ r1(sK262(X373),X375)
| p6(X373) ) ).
cnf(u983,negated_conjecture,
( ~ p5(X376)
| ~ r1(sK105,X373)
| ~ r1(X373,X376)
| r1(X373,sK262(X373))
| p6(X373) ) ).
cnf(u1002,negated_conjecture,
( ~ r1(sK105,X368)
| p5(X368)
| sP4(X368)
| p6(X368) ) ).
cnf(u1005,negated_conjecture,
( ~ p5(X365)
| ~ p6(X365)
| ~ p6(sK258(X365))
| ~ r1(sK105,X365)
| p6(X366)
| ~ r1(X365,X366) ) ).
cnf(u1009,negated_conjecture,
( ~ p6(sK259(X368))
| ~ r1(sK105,X368)
| sP4(X368)
| p6(X368) ) ).
cnf(u1013,negated_conjecture,
( ~ r1(sK105,X368)
| r1(X368,sK259(X368))
| sP4(X368)
| p6(X368) ) ).
cnf(u1023,negated_conjecture,
( ~ p6(X364)
| ~ r1(sK105,X361)
| ~ r1(X361,X364)
| ~ p6(X363)
| ~ r1(sK257(X361),X363)
| p7(X361) ) ).
cnf(u1030,negated_conjecture,
( ~ p6(X364)
| ~ r1(sK105,X361)
| ~ r1(X361,X364)
| r1(X361,sK257(X361))
| p7(X361) ) ).
cnf(u1049,negated_conjecture,
( ~ r1(sK105,X356)
| p6(X356)
| sP5(X356)
| p7(X356) ) ).
cnf(u1052,negated_conjecture,
( ~ p6(X353)
| ~ p7(X353)
| ~ p7(sK253(X353))
| ~ r1(sK105,X353)
| p7(X354)
| ~ r1(X353,X354) ) ).
cnf(u1056,negated_conjecture,
( ~ p7(sK254(X356))
| ~ r1(sK105,X356)
| sP5(X356)
| p7(X356) ) ).
cnf(u1060,negated_conjecture,
( ~ r1(sK105,X356)
| r1(X356,sK254(X356))
| sP5(X356)
| p7(X356) ) ).
cnf(u1070,negated_conjecture,
( ~ p7(X352)
| ~ r1(sK105,X349)
| ~ r1(X349,X352)
| ~ p7(X351)
| ~ r1(sK252(X349),X351)
| p8(X349) ) ).
cnf(u1077,negated_conjecture,
( ~ p7(X352)
| ~ r1(sK105,X349)
| ~ r1(X349,X352)
| r1(X349,sK252(X349))
| p8(X349) ) ).
cnf(u1096,negated_conjecture,
( ~ r1(sK105,X344)
| p7(X344)
| sP6(X344)
| p8(X344) ) ).
cnf(u1099,negated_conjecture,
( ~ p7(X341)
| ~ p8(X341)
| ~ p8(sK248(X341))
| ~ r1(sK105,X341)
| p8(X342)
| ~ r1(X341,X342) ) ).
cnf(u1103,negated_conjecture,
( ~ p8(sK249(X344))
| ~ r1(sK105,X344)
| sP6(X344)
| p8(X344) ) ).
cnf(u1107,negated_conjecture,
( ~ r1(sK105,X344)
| r1(X344,sK249(X344))
| sP6(X344)
| p8(X344) ) ).
cnf(u1117,negated_conjecture,
( ~ p8(X340)
| ~ r1(sK105,X337)
| ~ r1(X337,X340)
| ~ p8(X339)
| ~ r1(sK247(X337),X339)
| p9(X337) ) ).
cnf(u1124,negated_conjecture,
( ~ p8(X340)
| ~ r1(sK105,X337)
| ~ r1(X337,X340)
| r1(X337,sK247(X337))
| p9(X337) ) ).
cnf(u1146,negated_conjecture,
( ~ p8(X329)
| ~ p9(X329)
| ~ p9(sK243(X329))
| ~ r1(sK105,X329)
| p9(X330)
| ~ r1(X329,X330) ) ).
cnf(u1150,negated_conjecture,
( ~ p9(sK244(X332))
| ~ r1(sK105,X332)
| sP7(X332)
| p9(X332) ) ).
cnf(u1158,negated_conjecture,
( ~ p8(X329)
| ~ p9(X329)
| r1(X329,sK243(X329))
| ~ r1(sK105,X329)
| p9(X330)
| ~ r1(X329,X330) ) ).
cnf(u1164,negated_conjecture,
( ~ p9(X328)
| ~ r1(sK105,X325)
| ~ r1(X325,X328)
| ~ p9(X327)
| ~ r1(sK242(X325),X327)
| p10(X325) ) ).
cnf(u1171,negated_conjecture,
( ~ p9(X328)
| ~ r1(sK105,X325)
| ~ r1(X325,X328)
| r1(X325,sK242(X325))
| p10(X325) ) ).
cnf(u1193,negated_conjecture,
( ~ p9(X317)
| ~ p10(X317)
| ~ p10(sK238(X317))
| ~ r1(sK105,X317)
| p10(X318)
| ~ r1(X317,X318) ) ).
cnf(u1197,negated_conjecture,
( ~ p10(sK239(X320))
| ~ r1(sK105,X320)
| sP8(X320)
| p10(X320) ) ).
cnf(u1205,negated_conjecture,
( ~ p9(X317)
| ~ p10(X317)
| r1(X317,sK238(X317))
| ~ r1(sK105,X317)
| p10(X318)
| ~ r1(X317,X318) ) ).
cnf(u1211,negated_conjecture,
( ~ p10(X316)
| ~ r1(sK105,X313)
| ~ r1(X313,X316)
| ~ p10(X315)
| ~ r1(sK237(X313),X315)
| p11(X313) ) ).
cnf(u1218,negated_conjecture,
( ~ p10(X316)
| ~ r1(sK105,X313)
| ~ r1(X313,X316)
| r1(X313,sK237(X313))
| p11(X313) ) ).
cnf(u1240,negated_conjecture,
( ~ p11(sK233(X305))
| ~ p11(X305)
| ~ r1(sK105,X305)
| ~ p10(X305)
| p11(X306)
| ~ r1(X305,X306) ) ).
cnf(u1244,negated_conjecture,
( ~ p11(sK234(X308))
| ~ r1(sK105,X308)
| sP9(X308)
| p11(X308) ) ).
cnf(u1252,negated_conjecture,
( ~ p11(X305)
| ~ r1(sK105,X305)
| r1(X305,sK233(X305))
| ~ p10(X305)
| p11(X306)
| ~ r1(X305,X306) ) ).
cnf(u1258,negated_conjecture,
( ~ p11(X304)
| ~ r1(sK105,X301)
| ~ r1(X301,X304)
| ~ p11(X303)
| ~ r1(sK232(X301),X303)
| p12(X301) ) ).
cnf(u1265,negated_conjecture,
( ~ p11(X304)
| ~ r1(sK105,X301)
| ~ r1(X301,X304)
| r1(X301,sK232(X301))
| p12(X301) ) ).
cnf(u1287,negated_conjecture,
( ~ p11(X293)
| ~ p12(X293)
| ~ p12(sK228(X293))
| ~ r1(sK105,X293)
| p12(X294)
| ~ r1(X293,X294) ) ).
cnf(u1291,negated_conjecture,
( ~ p12(sK229(X296))
| ~ r1(sK105,X296)
| sP10(X296)
| p12(X296) ) ).
cnf(u1299,negated_conjecture,
( ~ p11(X293)
| ~ p12(X293)
| r1(X293,sK228(X293))
| ~ r1(sK105,X293)
| p12(X294)
| ~ r1(X293,X294) ) ).
cnf(u1305,negated_conjecture,
( ~ p12(X292)
| ~ r1(sK105,X289)
| ~ r1(X289,X292)
| ~ p12(X291)
| ~ r1(sK227(X289),X291)
| p13(X289) ) ).
cnf(u1312,negated_conjecture,
( ~ p12(X292)
| ~ r1(sK105,X289)
| ~ r1(X289,X292)
| r1(X289,sK227(X289))
| p13(X289) ) ).
cnf(u1334,negated_conjecture,
( ~ p12(X281)
| ~ p13(X281)
| ~ p13(sK223(X281))
| ~ r1(sK105,X281)
| p13(X282)
| ~ r1(X281,X282) ) ).
cnf(u1338,negated_conjecture,
( ~ p13(sK224(X284))
| ~ r1(sK105,X284)
| sP11(X284)
| p13(X284) ) ).
cnf(u1346,negated_conjecture,
( ~ p12(X281)
| ~ p13(X281)
| r1(X281,sK223(X281))
| ~ r1(sK105,X281)
| p13(X282)
| ~ r1(X281,X282) ) ).
cnf(u1352,negated_conjecture,
( ~ p13(X280)
| ~ r1(sK105,X277)
| ~ r1(X277,X280)
| ~ p13(X279)
| ~ r1(sK222(X277),X279)
| p14(X277) ) ).
cnf(u1359,negated_conjecture,
( ~ p13(X280)
| ~ r1(sK105,X277)
| ~ r1(X277,X280)
| r1(X277,sK222(X277))
| p14(X277) ) ).
cnf(u1381,negated_conjecture,
( ~ p13(X269)
| ~ p14(X269)
| ~ p14(sK218(X269))
| ~ r1(sK105,X269)
| p14(X270)
| ~ r1(X269,X270) ) ).
cnf(u1385,negated_conjecture,
( ~ p14(sK219(X272))
| ~ r1(sK105,X272)
| sP12(X272)
| p14(X272) ) ).
cnf(u1393,negated_conjecture,
( ~ p13(X269)
| ~ p14(X269)
| r1(X269,sK218(X269))
| ~ r1(sK105,X269)
| p14(X270)
| ~ r1(X269,X270) ) ).
cnf(u1399,negated_conjecture,
( ~ p14(X268)
| ~ r1(sK105,X265)
| ~ r1(X265,X268)
| ~ p14(X267)
| ~ r1(sK217(X265),X267)
| p15(X265) ) ).
cnf(u1406,negated_conjecture,
( ~ p14(X268)
| ~ r1(sK105,X265)
| ~ r1(X265,X268)
| r1(X265,sK217(X265))
| p15(X265) ) ).
cnf(u1428,negated_conjecture,
( ~ p14(X257)
| ~ p15(X257)
| ~ p15(sK213(X257))
| ~ r1(sK105,X257)
| p15(X258)
| ~ r1(X257,X258) ) ).
cnf(u1432,negated_conjecture,
( ~ p15(sK214(X260))
| ~ r1(sK105,X260)
| sP13(X260)
| p15(X260) ) ).
cnf(u1440,negated_conjecture,
( ~ p14(X257)
| ~ p15(X257)
| r1(X257,sK213(X257))
| ~ r1(sK105,X257)
| p15(X258)
| ~ r1(X257,X258) ) ).
cnf(u1446,negated_conjecture,
( ~ p15(X256)
| ~ r1(sK105,X253)
| ~ r1(X253,X256)
| ~ p15(X255)
| ~ r1(sK212(X253),X255)
| p16(X253) ) ).
cnf(u1453,negated_conjecture,
( ~ p15(X256)
| ~ r1(sK105,X253)
| ~ r1(X253,X256)
| r1(X253,sK212(X253))
| p16(X253) ) ).
cnf(u1475,negated_conjecture,
( ~ p15(X245)
| ~ p16(X245)
| ~ p16(sK208(X245))
| ~ r1(sK105,X245)
| p16(X246)
| ~ r1(X245,X246) ) ).
cnf(u1479,negated_conjecture,
( ~ p16(sK209(X248))
| ~ r1(sK105,X248)
| sP14(X248)
| p16(X248) ) ).
cnf(u1487,negated_conjecture,
( ~ p15(X245)
| ~ p16(X245)
| r1(X245,sK208(X245))
| ~ r1(sK105,X245)
| p16(X246)
| ~ r1(X245,X246) ) ).
cnf(u1493,negated_conjecture,
( ~ p16(X244)
| ~ r1(sK105,X241)
| ~ r1(X241,X244)
| ~ p16(X243)
| ~ r1(sK207(X241),X243)
| p17(X241) ) ).
cnf(u1500,negated_conjecture,
( ~ p16(X244)
| ~ r1(sK105,X241)
| ~ r1(X241,X244)
| r1(X241,sK207(X241))
| p17(X241) ) ).
cnf(u1522,negated_conjecture,
( ~ p16(X233)
| ~ p17(X233)
| ~ p17(sK203(X233))
| ~ r1(sK105,X233)
| p17(X234)
| ~ r1(X233,X234) ) ).
cnf(u1526,negated_conjecture,
( ~ p17(sK204(X236))
| ~ r1(sK105,X236)
| sP15(X236)
| p17(X236) ) ).
cnf(u1534,negated_conjecture,
( ~ p16(X233)
| ~ p17(X233)
| r1(X233,sK203(X233))
| ~ r1(sK105,X233)
| p17(X234)
| ~ r1(X233,X234) ) ).
cnf(u1540,negated_conjecture,
( ~ p17(X232)
| ~ r1(sK105,X229)
| ~ r1(X229,X232)
| ~ p17(X231)
| ~ r1(sK202(X229),X231)
| p18(X229) ) ).
cnf(u1547,negated_conjecture,
( ~ p17(X232)
| ~ r1(sK105,X229)
| ~ r1(X229,X232)
| r1(X229,sK202(X229))
| p18(X229) ) ).
cnf(u1569,negated_conjecture,
( ~ p17(X221)
| ~ p18(X221)
| ~ p18(sK198(X221))
| ~ r1(sK105,X221)
| p18(X222)
| ~ r1(X221,X222) ) ).
cnf(u1573,negated_conjecture,
( ~ p18(sK199(X224))
| ~ r1(sK105,X224)
| sP16(X224)
| p18(X224) ) ).
cnf(u1581,negated_conjecture,
( ~ p17(X221)
| ~ p18(X221)
| r1(X221,sK198(X221))
| ~ r1(sK105,X221)
| p18(X222)
| ~ r1(X221,X222) ) ).
cnf(u1587,negated_conjecture,
( ~ p18(X220)
| ~ r1(sK105,X217)
| ~ r1(X217,X220)
| ~ p18(X219)
| ~ r1(sK197(X217),X219)
| p19(X217) ) ).
cnf(u1594,negated_conjecture,
( ~ p18(X220)
| ~ r1(sK105,X217)
| ~ r1(X217,X220)
| r1(X217,sK197(X217))
| p19(X217) ) ).
cnf(u1616,negated_conjecture,
( ~ p18(X209)
| ~ p19(X209)
| ~ p19(sK193(X209))
| ~ r1(sK105,X209)
| p19(X210)
| ~ r1(X209,X210) ) ).
cnf(u1620,negated_conjecture,
( ~ p19(sK194(X212))
| ~ r1(sK105,X212)
| sP17(X212)
| p19(X212) ) ).
cnf(u1628,negated_conjecture,
( ~ p18(X209)
| ~ p19(X209)
| r1(X209,sK193(X209))
| ~ r1(sK105,X209)
| p19(X210)
| ~ r1(X209,X210) ) ).
cnf(u1634,negated_conjecture,
( ~ p20(X204)
| ~ r1(sK105,X201)
| ~ r1(X201,X204)
| ~ p20(X203)
| ~ r1(sK190(X201),X203)
| p21(X201) ) ).
cnf(u1641,negated_conjecture,
( ~ p20(X204)
| ~ r1(sK105,X201)
| ~ r1(X201,X204)
| r1(X201,sK190(X201))
| p21(X201) ) ).
cnf(u1663,negated_conjecture,
( ~ p20(X193)
| ~ p21(X193)
| ~ p21(sK186(X193))
| ~ r1(sK105,X193)
| p21(X194)
| ~ r1(X193,X194) ) ).
cnf(u1667,negated_conjecture,
( ~ p21(sK187(X196))
| ~ r1(sK105,X196)
| sP18(X196)
| p21(X196) ) ).
cnf(u1675,negated_conjecture,
( ~ p20(X193)
| ~ p21(X193)
| r1(X193,sK186(X193))
| ~ r1(sK105,X193)
| p21(X194)
| ~ r1(X193,X194) ) ).
cnf(u1681,negated_conjecture,
( ~ p21(X192)
| ~ r1(sK105,X189)
| ~ r1(X189,X192)
| ~ p21(X191)
| ~ r1(sK185(X189),X191)
| p22(X189) ) ).
cnf(u1688,negated_conjecture,
( ~ p21(X192)
| ~ r1(sK105,X189)
| ~ r1(X189,X192)
| r1(X189,sK185(X189))
| p22(X189) ) ).
cnf(u1710,negated_conjecture,
( ~ p21(X181)
| ~ p22(X181)
| ~ p22(sK181(X181))
| ~ r1(sK105,X181)
| p22(X182)
| ~ r1(X181,X182) ) ).
cnf(u1714,negated_conjecture,
( ~ p22(sK182(X184))
| ~ r1(sK105,X184)
| sP19(X184)
| p22(X184) ) ).
cnf(u1722,negated_conjecture,
( ~ p21(X181)
| ~ p22(X181)
| r1(X181,sK181(X181))
| ~ r1(sK105,X181)
| p22(X182)
| ~ r1(X181,X182) ) ).
cnf(u1728,negated_conjecture,
( ~ p22(X180)
| ~ r1(sK105,X177)
| ~ r1(X177,X180)
| ~ p22(X179)
| ~ r1(sK180(X177),X179)
| p23(X177) ) ).
cnf(u1735,negated_conjecture,
( ~ p22(X180)
| ~ r1(sK105,X177)
| ~ r1(X177,X180)
| r1(X177,sK180(X177))
| p23(X177) ) ).
cnf(u1757,negated_conjecture,
( ~ p22(X169)
| ~ p23(X169)
| ~ p23(sK176(X169))
| ~ r1(sK105,X169)
| p23(X170)
| ~ r1(X169,X170) ) ).
cnf(u1761,negated_conjecture,
( ~ p23(sK177(X172))
| ~ r1(sK105,X172)
| sP20(X172)
| p23(X172) ) ).
cnf(u1769,negated_conjecture,
( ~ p22(X169)
| ~ p23(X169)
| r1(X169,sK176(X169))
| ~ r1(sK105,X169)
| p23(X170)
| ~ r1(X169,X170) ) ).
cnf(u1775,negated_conjecture,
( ~ p23(X168)
| ~ r1(sK105,X165)
| ~ r1(X165,X168)
| ~ p23(X167)
| ~ r1(sK175(X165),X167)
| p24(X165) ) ).
cnf(u1782,negated_conjecture,
( ~ p23(X168)
| ~ r1(sK105,X165)
| ~ r1(X165,X168)
| r1(X165,sK175(X165))
| p24(X165) ) ).
cnf(u1804,negated_conjecture,
( ~ p23(X157)
| ~ p24(X157)
| ~ p24(sK171(X157))
| ~ r1(sK105,X157)
| p24(X158)
| ~ r1(X157,X158) ) ).
cnf(u1808,negated_conjecture,
( ~ p24(sK172(X160))
| ~ r1(sK105,X160)
| sP21(X160)
| p24(X160) ) ).
cnf(u1816,negated_conjecture,
( ~ p23(X157)
| ~ p24(X157)
| r1(X157,sK171(X157))
| ~ r1(sK105,X157)
| p24(X158)
| ~ r1(X157,X158) ) ).
cnf(u1822,negated_conjecture,
( ~ p24(X156)
| ~ r1(sK105,X153)
| ~ r1(X153,X156)
| ~ p24(X155)
| ~ r1(sK170(X153),X155)
| p25(X153) ) ).
cnf(u1829,negated_conjecture,
( ~ p24(X156)
| ~ r1(sK105,X153)
| ~ r1(X153,X156)
| r1(X153,sK170(X153))
| p25(X153) ) ).
cnf(u1851,negated_conjecture,
( ~ p24(X145)
| ~ p25(X145)
| ~ p25(sK166(X145))
| ~ r1(sK105,X145)
| p25(X146)
| ~ r1(X145,X146) ) ).
cnf(u1855,negated_conjecture,
( ~ p25(sK167(X148))
| ~ r1(sK105,X148)
| sP22(X148)
| p25(X148) ) ).
cnf(u1863,negated_conjecture,
( ~ p24(X145)
| ~ p25(X145)
| r1(X145,sK166(X145))
| ~ r1(sK105,X145)
| p25(X146)
| ~ r1(X145,X146) ) ).
cnf(u1869,negated_conjecture,
( ~ p25(X144)
| ~ r1(sK105,X141)
| ~ r1(X141,X144)
| ~ p25(X143)
| ~ r1(sK165(X141),X143)
| p26(X141) ) ).
cnf(u1876,negated_conjecture,
( ~ p25(X144)
| ~ r1(sK105,X141)
| ~ r1(X141,X144)
| r1(X141,sK165(X141))
| p26(X141) ) ).
cnf(u1898,negated_conjecture,
( ~ p25(X133)
| ~ p26(X133)
| ~ p26(sK161(X133))
| ~ r1(sK105,X133)
| p26(X134)
| ~ r1(X133,X134) ) ).
cnf(u1902,negated_conjecture,
( ~ p26(sK162(X136))
| ~ r1(sK105,X136)
| sP23(X136)
| p26(X136) ) ).
cnf(u1910,negated_conjecture,
( ~ p25(X133)
| ~ p26(X133)
| r1(X133,sK161(X133))
| ~ r1(sK105,X133)
| p26(X134)
| ~ r1(X133,X134) ) ).
cnf(u1916,negated_conjecture,
( ~ p26(X132)
| ~ r1(sK105,X129)
| ~ r1(X129,X132)
| ~ p26(X131)
| ~ r1(sK160(X129),X131)
| p27(X129) ) ).
cnf(u1923,negated_conjecture,
( ~ p26(X132)
| ~ r1(sK105,X129)
| ~ r1(X129,X132)
| r1(X129,sK160(X129))
| p27(X129) ) ).
cnf(u1945,negated_conjecture,
( ~ p26(X121)
| ~ p27(X121)
| ~ p27(sK156(X121))
| ~ r1(sK105,X121)
| p27(X122)
| ~ r1(X121,X122) ) ).
cnf(u1949,negated_conjecture,
( ~ p27(sK157(X124))
| ~ r1(sK105,X124)
| sP24(X124)
| p27(X124) ) ).
cnf(u1957,negated_conjecture,
( ~ p26(X121)
| ~ p27(X121)
| r1(X121,sK156(X121))
| ~ r1(sK105,X121)
| p27(X122)
| ~ r1(X121,X122) ) ).
cnf(u1963,negated_conjecture,
( ~ p27(X120)
| ~ r1(sK105,X117)
| ~ r1(X117,X120)
| ~ p27(X119)
| ~ r1(sK155(X117),X119)
| p28(X117) ) ).
cnf(u1970,negated_conjecture,
( ~ p27(X120)
| ~ r1(sK105,X117)
| ~ r1(X117,X120)
| r1(X117,sK155(X117))
| p28(X117) ) ).
cnf(u1992,negated_conjecture,
( ~ p27(X109)
| ~ p28(X109)
| ~ p28(sK151(X109))
| ~ r1(sK105,X109)
| p28(X110)
| ~ r1(X109,X110) ) ).
cnf(u1996,negated_conjecture,
( ~ p28(sK152(X112))
| ~ r1(sK105,X112)
| sP25(X112)
| p28(X112) ) ).
cnf(u2004,negated_conjecture,
( ~ p27(X109)
| ~ p28(X109)
| r1(X109,sK151(X109))
| ~ r1(sK105,X109)
| p28(X110)
| ~ r1(X109,X110) ) ).
cnf(u2010,negated_conjecture,
( ~ p28(X108)
| ~ r1(sK105,X105)
| ~ r1(X105,X108)
| ~ p28(X107)
| ~ r1(sK150(X105),X107)
| p29(X105) ) ).
cnf(u2017,negated_conjecture,
( ~ p28(X108)
| ~ r1(sK105,X105)
| ~ r1(X105,X108)
| r1(X105,sK150(X105))
| p29(X105) ) ).
cnf(u2039,negated_conjecture,
( ~ p28(X97)
| ~ p29(X97)
| ~ p29(sK146(X97))
| ~ r1(sK105,X97)
| p29(X98)
| ~ r1(X97,X98) ) ).
cnf(u2043,negated_conjecture,
( ~ p29(sK147(X100))
| ~ r1(sK105,X100)
| sP26(X100)
| p29(X100) ) ).
cnf(u2051,negated_conjecture,
( ~ p28(X97)
| ~ p29(X97)
| r1(X97,sK146(X97))
| ~ r1(sK105,X97)
| p29(X98)
| ~ r1(X97,X98) ) ).
cnf(u2057,negated_conjecture,
( ~ p29(X96)
| ~ r1(sK105,X93)
| ~ r1(X93,X96)
| ~ p29(X95)
| ~ r1(sK145(X93),X95)
| p30(X93) ) ).
cnf(u2064,negated_conjecture,
( ~ p29(X96)
| ~ r1(sK105,X93)
| ~ r1(X93,X96)
| r1(X93,sK145(X93))
| p30(X93) ) ).
cnf(u2086,negated_conjecture,
( ~ p29(X85)
| ~ p30(X85)
| ~ p30(sK141(X85))
| ~ r1(sK105,X85)
| p30(X86)
| ~ r1(X85,X86) ) ).
cnf(u2090,negated_conjecture,
( ~ p30(sK142(X88))
| ~ r1(sK105,X88)
| sP27(X88)
| p30(X88) ) ).
cnf(u2098,negated_conjecture,
( ~ p29(X85)
| ~ p30(X85)
| r1(X85,sK141(X85))
| ~ r1(sK105,X85)
| p30(X86)
| ~ r1(X85,X86) ) ).
cnf(u2104,negated_conjecture,
( ~ p30(X84)
| ~ r1(sK105,X81)
| ~ r1(X81,X84)
| ~ p30(X83)
| ~ r1(sK140(X81),X83)
| p31(X81) ) ).
cnf(u2111,negated_conjecture,
( ~ p30(X84)
| ~ r1(sK105,X81)
| ~ r1(X81,X84)
| r1(X81,sK140(X81))
| p31(X81) ) ).
cnf(u2133,negated_conjecture,
( ~ p30(X73)
| ~ p31(X73)
| ~ p31(sK136(X73))
| ~ r1(sK105,X73)
| p31(X74)
| ~ r1(X73,X74) ) ).
cnf(u2137,negated_conjecture,
( ~ p31(sK137(X76))
| ~ r1(sK105,X76)
| sP28(X76)
| p31(X76) ) ).
cnf(u2145,negated_conjecture,
( ~ p30(X73)
| ~ p31(X73)
| r1(X73,sK136(X73))
| ~ r1(sK105,X73)
| p31(X74)
| ~ r1(X73,X74) ) ).
cnf(u2151,negated_conjecture,
( ~ p31(X72)
| ~ r1(sK105,X69)
| ~ r1(X69,X72)
| ~ p31(X71)
| ~ r1(sK135(X69),X71)
| p32(X69) ) ).
cnf(u2158,negated_conjecture,
( ~ p31(X72)
| ~ r1(sK105,X69)
| ~ r1(X69,X72)
| r1(X69,sK135(X69))
| p32(X69) ) ).
cnf(u2180,negated_conjecture,
( ~ p31(X61)
| ~ p32(X61)
| ~ p32(sK131(X61))
| ~ r1(sK105,X61)
| p32(X62)
| ~ r1(X61,X62) ) ).
cnf(u2184,negated_conjecture,
( ~ p32(sK132(X64))
| ~ r1(sK105,X64)
| sP29(X64)
| p32(X64) ) ).
cnf(u2192,negated_conjecture,
( ~ p31(X61)
| ~ p32(X61)
| r1(X61,sK131(X61))
| ~ r1(sK105,X61)
| p32(X62)
| ~ r1(X61,X62) ) ).
cnf(u2198,negated_conjecture,
( ~ p32(X60)
| ~ r1(sK105,X57)
| ~ r1(X57,X60)
| ~ p32(X59)
| ~ r1(sK130(X57),X59)
| p33(X57) ) ).
cnf(u2205,negated_conjecture,
( ~ p32(X60)
| ~ r1(sK105,X57)
| ~ r1(X57,X60)
| r1(X57,sK130(X57))
| p33(X57) ) ).
cnf(u2227,negated_conjecture,
( ~ p32(X49)
| ~ p33(X49)
| ~ p33(sK126(X49))
| ~ r1(sK105,X49)
| p33(X50)
| ~ r1(X49,X50) ) ).
cnf(u2231,negated_conjecture,
( ~ p33(sK127(X52))
| ~ r1(sK105,X52)
| sP30(X52)
| p33(X52) ) ).
cnf(u2239,negated_conjecture,
( ~ p32(X49)
| ~ p33(X49)
| r1(X49,sK126(X49))
| ~ r1(sK105,X49)
| p33(X50)
| ~ r1(X49,X50) ) ).
cnf(u2245,negated_conjecture,
( ~ p33(X48)
| ~ r1(sK105,X45)
| ~ r1(X45,X48)
| ~ p33(X47)
| ~ r1(sK125(X45),X47)
| p34(X45) ) ).
cnf(u2252,negated_conjecture,
( ~ p33(X48)
| ~ r1(sK105,X45)
| ~ r1(X45,X48)
| r1(X45,sK125(X45))
| p34(X45) ) ).
cnf(u2274,negated_conjecture,
( ~ p33(X37)
| ~ p34(X37)
| ~ p34(sK121(X37))
| ~ r1(sK105,X37)
| p34(X38)
| ~ r1(X37,X38) ) ).
cnf(u2278,negated_conjecture,
( ~ p34(sK122(X40))
| ~ r1(sK105,X40)
| sP31(X40)
| p34(X40) ) ).
cnf(u2286,negated_conjecture,
( ~ p33(X37)
| ~ p34(X37)
| r1(X37,sK121(X37))
| ~ r1(sK105,X37)
| p34(X38)
| ~ r1(X37,X38) ) ).
cnf(u2292,negated_conjecture,
( ~ p34(X36)
| ~ r1(sK105,X33)
| ~ r1(X33,X36)
| ~ p34(X35)
| ~ r1(sK120(X33),X35)
| p35(X33) ) ).
cnf(u2299,negated_conjecture,
( ~ p34(X36)
| ~ r1(sK105,X33)
| ~ r1(X33,X36)
| r1(X33,sK120(X33))
| p35(X33) ) ).
cnf(u2321,negated_conjecture,
( ~ p34(X25)
| ~ p35(X25)
| ~ p35(sK116(X25))
| ~ r1(sK105,X25)
| p35(X26)
| ~ r1(X25,X26) ) ).
cnf(u2325,negated_conjecture,
( ~ p35(sK117(X28))
| ~ r1(sK105,X28)
| sP32(X28)
| p35(X28) ) ).
cnf(u2333,negated_conjecture,
( ~ p34(X25)
| ~ p35(X25)
| r1(X25,sK116(X25))
| ~ r1(sK105,X25)
| p35(X26)
| ~ r1(X25,X26) ) ).
cnf(u2339,negated_conjecture,
( ~ p35(X24)
| ~ r1(sK105,X21)
| ~ r1(X21,X24)
| ~ p35(X23)
| ~ r1(sK115(X21),X23)
| p36(X21) ) ).
cnf(u2346,negated_conjecture,
( ~ p35(X24)
| ~ r1(sK105,X21)
| ~ r1(X21,X24)
| r1(X21,sK115(X21))
| p36(X21) ) ).
cnf(u2368,negated_conjecture,
( ~ p35(X13)
| ~ p36(X13)
| ~ p36(sK111(X13))
| ~ r1(sK105,X13)
| p36(X14)
| ~ r1(X13,X14) ) ).
cnf(u2372,negated_conjecture,
( ~ p36(sK112(X16))
| ~ r1(sK105,X16)
| sP33(X16)
| p36(X16) ) ).
cnf(u2380,negated_conjecture,
( ~ p35(X13)
| ~ p36(X13)
| r1(X13,sK111(X13))
| ~ r1(sK105,X13)
| p36(X14)
| ~ r1(X13,X14) ) ).
cnf(u2386,negated_conjecture,
( ~ p36(X12)
| ~ r1(sK105,X9)
| ~ r1(X9,X12)
| ~ p36(X11)
| ~ r1(sK110(X9),X11)
| p37(X9) ) ).
cnf(u2393,negated_conjecture,
( ~ p36(X12)
| ~ r1(sK105,X9)
| ~ r1(X9,X12)
| r1(X9,sK110(X9))
| p37(X9) ) ).
cnf(u2415,negated_conjecture,
( ~ p36(X1)
| ~ p37(X1)
| ~ p37(sK106(X1))
| ~ r1(sK105,X1)
| p37(X2)
| ~ r1(X1,X2) ) ).
cnf(u2419,negated_conjecture,
( ~ p37(sK107(X4))
| ~ r1(sK105,X4)
| sP34(X4)
| p37(X4) ) ).
cnf(u2427,negated_conjecture,
( ~ p36(X1)
| ~ p37(X1)
| r1(X1,sK106(X1))
| ~ r1(sK105,X1)
| p37(X2)
| ~ r1(X1,X2) ) ).
cnf(u2436,negated_conjecture,
p2(sK191) ).
cnf(u2439,negated_conjecture,
~ sP0(sK191) ).
cnf(u2449,negated_conjecture,
p2(sK192) ).
cnf(u2452,negated_conjecture,
~ sP0(sK192) ).
cnf(u2464,negated_conjecture,
p3(sK191) ).
cnf(u2473,negated_conjecture,
p3(sK192) ).
cnf(u2484,negated_conjecture,
p4(sK191) ).
cnf(u2493,negated_conjecture,
p4(sK192) ).
cnf(u2504,negated_conjecture,
p5(sK191) ).
cnf(u2513,negated_conjecture,
p5(sK192) ).
cnf(u2524,negated_conjecture,
p6(sK191) ).
cnf(u2533,negated_conjecture,
p6(sK192) ).
cnf(u2544,negated_conjecture,
p7(sK191) ).
cnf(u2553,negated_conjecture,
p7(sK192) ).
cnf(u2564,negated_conjecture,
p8(sK191) ).
cnf(u2573,negated_conjecture,
p8(sK192) ).
cnf(u2583,negated_conjecture,
~ p9(sK191) ).
cnf(u2592,negated_conjecture,
~ p9(sK192) ).
cnf(u3628,negated_conjecture,
~ r1(sK191,sK191) ).
cnf(u3637,negated_conjecture,
~ r1(sK192,sK191) ).
cnf(u3644,negated_conjecture,
~ r1(sK191,sK192) ).
cnf(u3649,negated_conjecture,
~ r1(sK192,sK192) ).
cnf(u3663,negated_conjecture,
~ p4(sK268(sK192)) ).
cnf(u3671,negated_conjecture,
~ p4(sK268(sK191)) ).
cnf(u3685,negated_conjecture,
~ p5(sK263(sK192)) ).
cnf(u3693,negated_conjecture,
~ p5(sK263(sK191)) ).
cnf(u3707,negated_conjecture,
~ p6(sK258(sK192)) ).
cnf(u3715,negated_conjecture,
~ p6(sK258(sK191)) ).
cnf(u3729,negated_conjecture,
~ p7(sK253(sK192)) ).
cnf(u3737,negated_conjecture,
~ p7(sK253(sK191)) ).
cnf(u3751,negated_conjecture,
~ p8(sK248(sK192)) ).
cnf(u3759,negated_conjecture,
~ p8(sK248(sK191)) ).
cnf(u3969,negated_conjecture,
~ r1(sK105,sK103(sK191)) ).
cnf(u3992,negated_conjecture,
~ r1(sK105,sK103(sK192)) ).
cnf(u4054,negated_conjecture,
~ p3(sK273(sK191)) ).
cnf(u4093,negated_conjecture,
~ p3(sK273(sK192)) ).
cnf(u263,axiom,
( ~ sP6(X0)
| ~ p8(sK92(X0)) ) ).
cnf(u180,axiom,
( ~ sP27(X0)
| r1(sK49(X0),sK50(X0)) ) ).
cnf(u3588,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK272(X0))
| p4(X0) ) ).
cnf(u240,axiom,
( ~ sP12(X0)
| r1(sK79(X0),sK80(X0)) ) ).
cnf(u3951,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK247(X0),sK191)
| p9(X0) ) ).
cnf(u285,axiom,
( ~ sP1(X0)
| r1(X0,sK101(X0)) ) ).
cnf(u3915,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK262(X0),sK191)
| p6(X0) ) ).
cnf(u3825,negated_conjecture,
( ~ p5(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK262(X0),X1)
| p6(X0) ) ).
cnf(u3903,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK267(X0),sK191)
| p5(X0) ) ).
cnf(u3934,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK252(X0),sK192)
| p8(X0) ) ).
cnf(u546,negated_conjecture,
~ p10(sK191) ).
cnf(u265,axiom,
( ~ sP6(X0)
| r1(X0,sK91(X0)) ) ).
cnf(u250,axiom,
( ~ sP9(X0)
| p10(sK85(X0)) ) ).
cnf(u3601,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK252(X0))
| p8(X0) ) ).
cnf(u259,axiom,
( ~ sP7(X0)
| ~ p9(sK90(X0)) ) ).
cnf(u249,axiom,
( ~ sP10(X0)
| r1(X0,sK83(X0)) ) ).
cnf(u3849,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK272(X0),sK191)
| p4(X0) ) ).
cnf(u252,axiom,
( ~ sP9(X0)
| r1(sK85(X0),sK86(X0)) ) ).
cnf(u284,axiom,
( ~ sP1(X0)
| r1(sK101(X0),sK102(X0)) ) ).
cnf(u243,axiom,
( ~ sP11(X0)
| ~ p13(sK82(X0)) ) ).
cnf(u197,axiom,
( ~ sP23(X0)
| r1(X0,sK57(X0)) ) ).
cnf(u246,axiom,
( ~ sP10(X0)
| p11(sK83(X0)) ) ).
cnf(u3784,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK272(X0),sK192)
| p4(X0) ) ).
cnf(u278,axiom,
( ~ sP2(X0)
| p3(sK99(X0)) ) ).
cnf(u4103,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK277(X0),sK191)
| p3(X0) ) ).
cnf(u173,axiom,
( ~ sP29(X0)
| r1(X0,sK45(X0)) ) ).
cnf(u212,axiom,
( ~ sP19(X0)
| r1(sK65(X0),sK66(X0)) ) ).
cnf(u232,axiom,
( ~ sP14(X0)
| r1(sK75(X0),sK76(X0)) ) ).
cnf(u264,axiom,
( ~ sP6(X0)
| r1(sK91(X0),sK92(X0)) ) ).
cnf(u239,axiom,
( ~ sP12(X0)
| ~ p14(sK80(X0)) ) ).
cnf(u258,axiom,
( ~ sP7(X0)
| p8(sK89(X0)) ) ).
cnf(u225,axiom,
( ~ sP16(X0)
| r1(X0,sK71(X0)) ) ).
cnf(u228,axiom,
( ~ sP15(X0)
| r1(sK73(X0),sK74(X0)) ) ).
cnf(u260,axiom,
( ~ sP7(X0)
| r1(sK89(X0),sK90(X0)) ) ).
cnf(u219,axiom,
( ~ sP17(X0)
| ~ p19(sK70(X0)) ) ).
cnf(u191,axiom,
( ~ sP24(X0)
| ~ p27(sK56(X0)) ) ).
cnf(u178,axiom,
( ~ sP27(X0)
| p29(sK49(X0)) ) ).
cnf(u3952,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK247(X0),sK192)
| p9(X0) ) ).
cnf(u177,axiom,
( ~ sP28(X0)
| r1(X0,sK47(X0)) ) ).
cnf(u3847,negated_conjecture,
( ~ p6(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK257(X0),X1)
| p7(X0) ) ).
cnf(u181,axiom,
( ~ sP27(X0)
| r1(X0,sK49(X0)) ) ).
cnf(u4082,negated_conjecture,
( ~ p2(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK277(X0),X1)
| p3(X0) ) ).
cnf(u3782,negated_conjecture,
( ~ p3(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK272(X0),X1)
| p4(X0) ) ).
cnf(u281,axiom,
( ~ sP2(X0)
| r1(X0,sK99(X0)) ) ).
cnf(u3939,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK252(X0),sK191)
| p8(X0) ) ).
cnf(u275,axiom,
( ~ sP3(X0)
| ~ p5(sK98(X0)) ) ).
cnf(u277,axiom,
( ~ sP3(X0)
| r1(X0,sK97(X0)) ) ).
cnf(u253,axiom,
( ~ sP9(X0)
| r1(X0,sK85(X0)) ) ).
cnf(u3891,negated_conjecture,
( ~ p8(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK247(X0),X1)
| p9(X0) ) ).
cnf(u3826,negated_conjecture,
( ~ p5(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK262(X0),X1)
| p6(X0) ) ).
cnf(u222,axiom,
( ~ sP16(X0)
| p17(sK71(X0)) ) ).
cnf(u221,axiom,
( ~ sP17(X0)
| r1(X0,sK69(X0)) ) ).
cnf(u208,axiom,
( ~ sP20(X0)
| r1(sK63(X0),sK64(X0)) ) ).
cnf(u241,axiom,
( ~ sP12(X0)
| r1(X0,sK79(X0)) ) ).
cnf(u215,axiom,
( ~ sP18(X0)
| ~ p21(sK68(X0)) ) ).
cnf(u202,axiom,
( ~ sP21(X0)
| p23(sK61(X0)) ) ).
cnf(u171,axiom,
( ~ sP29(X0)
| ~ p32(sK46(X0)) ) ).
cnf(u230,axiom,
( ~ sP14(X0)
| p15(sK75(X0)) ) ).
cnf(u174,axiom,
( ~ sP28(X0)
| p30(sK47(X0)) ) ).
cnf(u192,axiom,
( ~ sP24(X0)
| r1(sK55(X0),sK56(X0)) ) ).
cnf(u204,axiom,
( ~ sP21(X0)
| r1(sK61(X0),sK62(X0)) ) ).
cnf(u195,axiom,
( ~ sP23(X0)
| ~ p26(sK58(X0)) ) ).
cnf(u160,axiom,
( ~ sP32(X0)
| r1(sK39(X0),sK40(X0)) ) ).
cnf(u3602,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK252(X0))
| p8(X0) ) ).
cnf(u198,axiom,
( ~ sP22(X0)
| p24(sK59(X0)) ) ).
cnf(u167,axiom,
( ~ sP30(X0)
| ~ p33(sK44(X0)) ) ).
cnf(u3909,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK262(X0),sK191)
| p6(X0) ) ).
cnf(u154,axiom,
( ~ sP33(X0)
| p35(sK37(X0)) ) ).
cnf(u156,axiom,
( ~ sP33(X0)
| r1(sK37(X0),sK38(X0)) ) ).
cnf(u150,axiom,
( ~ sP34(X0)
| p36(sK35(X0)) ) ).
cnf(u3848,negated_conjecture,
( ~ p6(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK257(X0),X1)
| p7(X0) ) ).
cnf(u271,axiom,
( ~ sP4(X0)
| ~ p6(sK96(X0)) ) ).
cnf(u4098,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK277(X0),sK192)
| p3(X0) ) ).
cnf(u257,axiom,
( ~ sP8(X0)
| r1(X0,sK87(X0)) ) ).
cnf(u182,axiom,
( ~ sP26(X0)
| p28(sK51(X0)) ) ).
cnf(u261,axiom,
( ~ sP7(X0)
| r1(X0,sK89(X0)) ) ).
cnf(u3587,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK272(X0))
| p4(X0) ) ).
cnf(u286,axiom,
( ~ sP0(X0)
| p1(sK103(X0)) ) ).
cnf(u3927,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK257(X0),sK191)
| p7(X0) ) ).
cnf(u3869,negated_conjecture,
( ~ p7(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK252(X0),X1)
| p8(X0) ) ).
cnf(u4034,negated_conjecture,
( ~ p2(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK277(X0),X1)
| p3(X0) ) ).
cnf(u4097,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK277(X0),sK191)
| p3(X0) ) ).
cnf(u3804,negated_conjecture,
( ~ p4(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK267(X0),X1)
| p5(X0) ) ).
cnf(u3781,negated_conjecture,
( ~ p3(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK272(X0),X1)
| p4(X0) ) ).
cnf(u251,axiom,
( ~ sP9(X0)
| ~ p11(sK86(X0)) ) ).
cnf(u254,axiom,
( ~ sP8(X0)
| p9(sK87(X0)) ) ).
cnf(u3946,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK247(X0),sK192)
| p9(X0) ) ).
cnf(u3870,negated_conjecture,
( ~ p7(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK252(X0),X1)
| p8(X0) ) ).
cnf(u276,axiom,
( ~ sP3(X0)
| r1(sK97(X0),sK98(X0)) ) ).
cnf(u272,axiom,
( ~ sP4(X0)
| r1(sK95(X0),sK96(X0)) ) ).
cnf(u247,axiom,
( ~ sP10(X0)
| ~ p12(sK84(X0)) ) ).
cnf(u248,axiom,
( ~ sP10(X0)
| r1(sK83(X0),sK84(X0)) ) ).
cnf(u234,axiom,
( ~ sP13(X0)
| p14(sK77(X0)) ) ).
cnf(u266,axiom,
( ~ sP5(X0)
| p6(sK93(X0)) ) ).
cnf(u233,axiom,
( ~ sP14(X0)
| r1(X0,sK75(X0)) ) ).
cnf(u236,axiom,
( ~ sP13(X0)
| r1(sK77(X0),sK78(X0)) ) ).
cnf(u3898,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK267(X0),sK192)
| p5(X0) ) ).
cnf(u268,axiom,
( ~ sP5(X0)
| r1(sK93(X0),sK94(X0)) ) ).
cnf(u227,axiom,
( ~ sP15(X0)
| ~ p17(sK74(X0)) ) ).
cnf(u4084,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK277(X0))
| p3(X0) ) ).
cnf(u244,axiom,
( ~ sP11(X0)
| r1(sK81(X0),sK82(X0)) ) ).
cnf(u262,axiom,
( ~ sP6(X0)
| p7(sK91(X0)) ) ).
cnf(u229,axiom,
( ~ sP15(X0)
| r1(X0,sK73(X0)) ) ).
cnf(u3928,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK257(X0),sK192)
| p7(X0) ) ).
cnf(u216,axiom,
( ~ sP18(X0)
| r1(sK67(X0),sK68(X0)) ) ).
cnf(u185,axiom,
( ~ sP26(X0)
| r1(X0,sK51(X0)) ) ).
cnf(u223,axiom,
( ~ sP16(X0)
| ~ p18(sK72(X0)) ) ).
cnf(u3904,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK267(X0),sK192)
| p5(X0) ) ).
cnf(u188,axiom,
( ~ sP25(X0)
| r1(sK53(X0),sK54(X0)) ) ).
cnf(u210,axiom,
( ~ sP19(X0)
| p21(sK65(X0)) ) ).
cnf(u179,axiom,
( ~ sP27(X0)
| ~ p30(sK50(X0)) ) ).
cnf(u157,axiom,
( ~ sP33(X0)
| r1(X0,sK37(X0)) ) ).
cnf(u209,axiom,
( ~ sP20(X0)
| r1(X0,sK63(X0)) ) ).
cnf(u3606,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK247(X0))
| p9(X0) ) ).
cnf(u203,axiom,
( ~ sP21(X0)
| ~ p24(sK62(X0)) ) ).
cnf(u168,axiom,
( ~ sP30(X0)
| r1(sK43(X0),sK44(X0)) ) ).
cnf(u183,axiom,
( ~ sP26(X0)
| ~ p29(sK52(X0)) ) ).
cnf(u175,axiom,
( ~ sP28(X0)
| ~ p31(sK48(X0)) ) ).
cnf(u162,axiom,
( ~ sP31(X0)
| p33(sK41(X0)) ) ).
cnf(u289,axiom,
( ~ sP0(X0)
| r1(X0,sK103(X0)) ) ).
cnf(u161,axiom,
( ~ sP32(X0)
| r1(X0,sK39(X0)) ) ).
cnf(u164,axiom,
( ~ sP31(X0)
| r1(sK41(X0),sK42(X0)) ) ).
cnf(u283,axiom,
( ~ sP1(X0)
| ~ p3(sK102(X0)) ) ).
cnf(u172,axiom,
( ~ sP29(X0)
| r1(sK45(X0),sK46(X0)) ) ).
cnf(u279,axiom,
( ~ sP2(X0)
| ~ p4(sK100(X0)) ) ).
cnf(u545,negated_conjecture,
( ~ r1(sK191,X206)
| p10(X206) ) ).
cnf(u542,negated_conjecture,
( ~ r1(sK192,X208)
| p10(X208) ) ).
cnf(u256,axiom,
( ~ sP8(X0)
| r1(sK87(X0),sK88(X0)) ) ).
cnf(u245,axiom,
( ~ sP11(X0)
| r1(X0,sK81(X0)) ) ).
cnf(u3589,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK267(X0))
| p5(X0) ) ).
cnf(u206,axiom,
( ~ sP20(X0)
| p22(sK63(X0)) ) ).
cnf(u205,axiom,
( ~ sP21(X0)
| r1(X0,sK61(X0)) ) ).
cnf(u199,axiom,
( ~ sP22(X0)
| ~ p25(sK60(X0)) ) ).
cnf(u547,negated_conjecture,
r1(sK105,sK191) ).
cnf(u155,axiom,
( ~ sP33(X0)
| ~ p36(sK38(X0)) ) ).
cnf(u217,axiom,
( ~ sP18(X0)
| r1(X0,sK67(X0)) ) ).
cnf(u158,axiom,
( ~ sP32(X0)
| p34(sK39(X0)) ) ).
cnf(u3850,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK272(X0),sK192)
| p4(X0) ) ).
cnf(u543,negated_conjecture,
~ p10(sK192) ).
cnf(u4036,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK277(X0))
| p3(X0) ) ).
cnf(u151,axiom,
( ~ sP34(X0)
| ~ p37(sK36(X0)) ) ).
cnf(u190,axiom,
( ~ sP24(X0)
| p26(sK55(X0)) ) ).
cnf(u207,axiom,
( ~ sP20(X0)
| ~ p23(sK64(X0)) ) ).
cnf(u3597,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK257(X0))
| p7(X0) ) ).
cnf(u3921,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK257(X0),sK191)
| p7(X0) ) ).
cnf(u280,axiom,
( ~ sP2(X0)
| r1(sK99(X0),sK100(X0)) ) ).
cnf(u255,axiom,
( ~ sP8(X0)
| ~ p10(sK88(X0)) ) ).
cnf(u3594,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK262(X0))
| p6(X0) ) ).
cnf(u242,axiom,
( ~ sP11(X0)
| p12(sK81(X0)) ) ).
cnf(u3916,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK262(X0),sK192)
| p6(X0) ) ).
cnf(u274,axiom,
( ~ sP3(X0)
| p4(sK97(X0)) ) ).
cnf(u3940,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK252(X0),sK192)
| p8(X0) ) ).
cnf(u3803,negated_conjecture,
( ~ p4(X1)
| ~ r1(X0,sK191)
| ~ r1(sK105,X0)
| ~ r1(sK267(X0),X1)
| p5(X0) ) ).
cnf(u3605,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK247(X0))
| p9(X0) ) ).
cnf(u270,axiom,
( ~ sP4(X0)
| p5(sK95(X0)) ) ).
cnf(u3783,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK272(X0),sK191)
| p4(X0) ) ).
cnf(u3892,negated_conjecture,
( ~ p8(X1)
| ~ r1(X0,sK192)
| ~ r1(sK105,X0)
| ~ r1(sK247(X0),X1)
| p9(X0) ) ).
cnf(u152,axiom,
( ~ sP34(X0)
| r1(sK35(X0),sK36(X0)) ) ).
cnf(u288,axiom,
( ~ sP0(X0)
| r1(sK103(X0),sK104(X0)) ) ).
cnf(u282,axiom,
( ~ sP1(X0)
| p2(sK101(X0)) ) ).
cnf(u3922,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK257(X0),sK192)
| p7(X0) ) ).
cnf(u235,axiom,
( ~ sP13(X0)
| ~ p15(sK78(X0)) ) ).
cnf(u153,axiom,
( ~ sP34(X0)
| r1(X0,sK35(X0)) ) ).
cnf(u238,axiom,
( ~ sP12(X0)
| p13(sK79(X0)) ) ).
cnf(u237,axiom,
( ~ sP13(X0)
| r1(X0,sK77(X0)) ) ).
cnf(u224,axiom,
( ~ sP16(X0)
| r1(sK71(X0),sK72(X0)) ) ).
cnf(u231,axiom,
( ~ sP14(X0)
| ~ p16(sK76(X0)) ) ).
cnf(u273,axiom,
( ~ sP4(X0)
| r1(X0,sK95(X0)) ) ).
cnf(u218,axiom,
( ~ sP17(X0)
| p18(sK69(X0)) ) ).
cnf(u187,axiom,
( ~ sP25(X0)
| ~ p28(sK54(X0)) ) ).
cnf(u3910,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK262(X0),sK192)
| p6(X0) ) ).
cnf(u201,axiom,
( ~ sP22(X0)
| r1(X0,sK59(X0)) ) ).
cnf(u3945,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK247(X0),sK191)
| p9(X0) ) ).
cnf(u220,axiom,
( ~ sP17(X0)
| r1(sK69(X0),sK70(X0)) ) ).
cnf(u189,axiom,
( ~ sP25(X0)
| r1(X0,sK53(X0)) ) ).
cnf(u211,axiom,
( ~ sP19(X0)
| ~ p22(sK66(X0)) ) ).
cnf(u176,axiom,
( ~ sP28(X0)
| r1(sK47(X0),sK48(X0)) ) ).
cnf(u214,axiom,
( ~ sP18(X0)
| p20(sK67(X0)) ) ).
cnf(u213,axiom,
( ~ sP19(X0)
| r1(X0,sK65(X0)) ) ).
cnf(u170,axiom,
( ~ sP29(X0)
| p31(sK45(X0)) ) ).
cnf(u226,axiom,
( ~ sP15(X0)
| p16(sK73(X0)) ) ).
cnf(u200,axiom,
( ~ sP22(X0)
| r1(sK59(X0),sK60(X0)) ) ).
cnf(u169,axiom,
( ~ sP30(X0)
| r1(X0,sK43(X0)) ) ).
cnf(u3897,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK267(X0),sK191)
| p5(X0) ) ).
cnf(u3598,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK257(X0))
| p7(X0) ) ).
cnf(u194,axiom,
( ~ sP23(X0)
| p25(sK57(X0)) ) ).
cnf(u163,axiom,
( ~ sP31(X0)
| ~ p34(sK42(X0)) ) ).
cnf(u193,axiom,
( ~ sP24(X0)
| r1(X0,sK55(X0)) ) ).
cnf(u166,axiom,
( ~ sP30(X0)
| p32(sK43(X0)) ) ).
cnf(u196,axiom,
( ~ sP23(X0)
| r1(sK57(X0),sK58(X0)) ) ).
cnf(u544,negated_conjecture,
r1(sK105,sK192) ).
cnf(u165,axiom,
( ~ sP31(X0)
| r1(X0,sK41(X0)) ) ).
cnf(u287,axiom,
( ~ sP0(X0)
| ~ p2(sK104(X0)) ) ).
cnf(u159,axiom,
( ~ sP32(X0)
| ~ p35(sK40(X0)) ) ).
cnf(u3593,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| r1(X0,sK262(X0))
| p6(X0) ) ).
cnf(u3590,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| r1(X0,sK267(X0))
| p5(X0) ) ).
cnf(u4104,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK192)
| ~ r1(sK277(X0),sK192)
| p3(X0) ) ).
cnf(u3933,negated_conjecture,
( ~ r1(sK105,X0)
| ~ r1(X0,sK191)
| ~ r1(sK252(X0),sK191)
| p8(X0) ) ).
cnf(u267,axiom,
( ~ sP5(X0)
| ~ p7(sK94(X0)) ) ).
cnf(u186,axiom,
( ~ sP25(X0)
| p27(sK53(X0)) ) ).
cnf(u184,axiom,
( ~ sP26(X0)
| r1(sK51(X0),sK52(X0)) ) ).
cnf(u269,axiom,
( ~ sP5(X0)
| r1(X0,sK93(X0)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL645+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n018.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 16:15:23 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.50 % (2554671)Will run a generic schedule for satisfiability detection.
% 0.17/0.50 % (2554681)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=968944589:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.50 % (2554677)% WARNING: option uhcvi not known.
% 0.17/0.50 % (2554676)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1326294669_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.50 % (2554677)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3490234610:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.50 % (2554678)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2139621101:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.50 % (2554679)dis+10_1_sil=32000:sp=arity:random_seed=2237741870:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.50 % (2554680)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1429099685:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.50 % (2554682)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1921028283:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.50 % (2554681) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2554671-2554681"...
% 0.17/0.50 % (2554681)...printing done.
% 0.17/0.50 % SZS status CounterSatisfiable for theBenchmark
% 0.17/0.50 % SZS output start Saturation.
% See solution above
% 0.17/0.51 % SZS output start Definitions and Model Updates.
% 0.17/0.51 % SZS output end Definitions and Model Updates.
% 0.17/0.51 % (2554681)------------------------------
% 0.17/0.51 % (2554681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.51 % (2554681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.51 % (2554681)CaDiCaL version: 2.1.3
% 0.17/0.51 % (2554681)Termination reason: Satisfiable
% 0.17/0.51 % (2554681)Time elapsed: 0.029 s
% 0.17/0.51 % (2554681)Peak memory usage: 15 MB
% 0.17/0.51 % (2554681)Instructions burned: 95 (million)
% 0.17/0.51 % (2554671)Success in time 0.068 s
% 0.17/0.51 % Vampire exiting
%------------------------------------------------------------------------------