%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL663+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 : n006.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:33 AM UTC 2026
% Result : CounterSatisfiable 0.19s 0.48s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u121,negated_conjecture,
( ~ p1(X459)
| r1(sK0,X449)
| r1(sK2(X449),X451)
| r1(X451,X452)
| r1(X452,X453)
| r1(X453,X454)
| r1(X454,X455)
| r1(X455,X456)
| r1(X456,X457)
| r1(X457,X458)
| r1(X458,X459) ) ).
cnf(u124,negated_conjecture,
~ p1(sK0) ).
cnf(u129,negated_conjecture,
( ~ r1(X449,sK2(X449))
| r1(sK0,X449) ) ).
cnf(u100,negated_conjecture,
( ~ r1(X284,sK32(X284))
| r1(X283,X284)
| r1(X282,X283)
| r1(X281,X282)
| r1(X280,X281)
| r1(X279,X280)
| r1(X278,X279)
| r1(X277,X278)
| r1(sK27(X275),X277)
| r1(X274,X275)
| r1(X273,X274)
| r1(X272,X273)
| r1(X271,X272)
| r1(X270,X271)
| r1(X269,X270)
| r1(X268,X269)
| r1(sK21(X266),X268)
| r1(X265,X266)
| r1(X264,X265)
| r1(X263,X264)
| r1(X262,X263)
| r1(X261,X262)
| r1(X260,X261)
| r1(X259,X260)
| r1(sK14(X257),X259)
| r1(X256,X257)
| r1(X255,X256)
| r1(X254,X255)
| r1(X253,X254)
| r1(X252,X253)
| r1(X251,X252)
| r1(X250,X251)
| r1(sK6(X248),X250)
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u82,negated_conjecture,
( ~ r1(X17,sK17(X17))
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u92,negated_conjecture,
( ~ r1(X386,sK25(X386))
| p1(X385)
| r1(X385,X386)
| r1(X384,X385)
| r1(X383,X384)
| r1(X382,X383)
| r1(X381,X382)
| r1(X380,X381)
| r1(X379,X380)
| r1(X378,X379)
| r1(sK19(X376),X378)
| r1(X375,X376)
| r1(X374,X375)
| r1(X373,X374)
| r1(X372,X373)
| r1(X371,X372)
| r1(X370,X371)
| r1(X369,X370)
| r1(sK12(X367),X369)
| r1(X366,X367)
| r1(X365,X366)
| r1(X364,X365)
| r1(X363,X364)
| r1(X362,X363)
| r1(X361,X362)
| r1(X360,X361)
| r1(sK4(X358),X360)
| r1(X357,X358)
| r1(X356,X357)
| r1(sK0,X356) ) ).
cnf(u94,negated_conjecture,
( ~ r1(X275,sK27(X275))
| r1(X274,X275)
| r1(X273,X274)
| r1(X272,X273)
| r1(X271,X272)
| r1(X270,X271)
| r1(X269,X270)
| r1(X268,X269)
| r1(sK21(X266),X268)
| r1(X265,X266)
| r1(X264,X265)
| r1(X263,X264)
| r1(X262,X263)
| r1(X261,X262)
| r1(X260,X261)
| r1(X259,X260)
| r1(sK14(X257),X259)
| r1(X256,X257)
| r1(X255,X256)
| r1(X254,X255)
| r1(X253,X254)
| r1(X252,X253)
| r1(X251,X252)
| r1(X250,X251)
| r1(sK6(X248),X250)
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u86,negated_conjecture,
( ~ r1(X326,sK20(X326))
| r1(X325,X326)
| r1(X324,X325)
| r1(X323,X324)
| r1(X322,X323)
| r1(X321,X322)
| r1(X320,X321)
| r1(X319,X320)
| r1(sK13(X317),X319)
| r1(X316,X317)
| r1(X315,X316)
| r1(X314,X315)
| r1(X313,X314)
| r1(X312,X313)
| r1(X311,X312)
| r1(X310,X311)
| r1(sK5(X308),X310)
| r1(X307,X308)
| r1(X306,X307)
| r1(X305,X306)
| r1(sK0,X305) ) ).
cnf(u80,negated_conjecture,
( ~ r1(X187,sK15(X187))
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u72,negated_conjecture,
( ~ r1(X98,sK8(X98))
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u113,negated_conjecture,
( ~ p1(X243)
| p1(X232)
| r1(X242,X243)
| r1(X241,X242)
| r1(X240,X241)
| r1(X239,X240)
| r1(X238,X239)
| r1(X237,X238)
| r1(X236,X237)
| r1(X235,X236)
| r1(sK40(X233),X235)
| r1(X232,X233)
| r1(X231,X232)
| r1(X230,X231)
| r1(X229,X230)
| r1(X228,X229)
| r1(X227,X228)
| r1(X226,X227)
| r1(X225,X226)
| r1(sK37(X223),X225)
| r1(X222,X223)
| r1(X221,X222)
| r1(X220,X221)
| r1(X219,X220)
| r1(X218,X219)
| r1(X217,X218)
| r1(X216,X217)
| r1(sK33(X214),X216)
| r1(X213,X214)
| r1(X212,X213)
| r1(X211,X212)
| r1(X210,X211)
| r1(X209,X210)
| r1(X208,X209)
| r1(X207,X208)
| r1(sK28(X205),X207)
| r1(X204,X205)
| r1(X203,X204)
| r1(X202,X203)
| r1(X201,X202)
| r1(X200,X201)
| r1(X199,X200)
| r1(X198,X199)
| r1(sK22(X196),X198)
| r1(X195,X196)
| r1(X194,X195)
| r1(X193,X194)
| r1(X192,X193)
| r1(X191,X192)
| r1(X190,X191)
| r1(X189,X190)
| r1(sK15(X187),X189)
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u115,negated_conjecture,
( ~ r1(X71,sK44(X71))
| r1(X70,X71)
| r1(X69,X70)
| r1(X68,X69)
| r1(X67,X68)
| r1(X66,X67)
| r1(X65,X66)
| r1(X64,X65)
| r1(sK42(X62),X64)
| r1(X61,X62)
| r1(X60,X61)
| r1(X59,X60)
| r1(X58,X59)
| r1(X57,X58)
| r1(X56,X57)
| r1(X55,X56)
| r1(sK39(X53),X55)
| r1(X52,X53)
| r1(X51,X52)
| r1(X50,X51)
| r1(X49,X50)
| r1(X48,X49)
| r1(X47,X48)
| r1(X46,X47)
| r1(sK35(X44),X46)
| r1(X43,X44)
| r1(X42,X43)
| r1(X41,X42)
| r1(X40,X41)
| r1(X39,X40)
| r1(X38,X39)
| r1(X37,X38)
| r1(sK30(X35),X37)
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u84,negated_conjecture,
( ~ r1(X417,sK18(X417))
| p1(X416)
| r1(X416,X417)
| r1(X415,X416)
| r1(X414,X415)
| r1(X413,X414)
| r1(X412,X413)
| r1(X411,X412)
| r1(X410,X411)
| r1(X409,X410)
| r1(sK11(X407),X409)
| r1(X406,X407)
| r1(X405,X406)
| r1(X404,X405)
| r1(X403,X404)
| r1(X402,X403)
| r1(X401,X402)
| r1(X400,X401)
| r1(sK3(X398),X400)
| r1(X397,X398)
| r1(sK0,X397) ) ).
cnf(u76,negated_conjecture,
( ~ r1(X407,sK11(X407))
| r1(X406,X407)
| r1(X405,X406)
| r1(X404,X405)
| r1(X403,X404)
| r1(X402,X403)
| r1(X401,X402)
| r1(X400,X401)
| r1(sK3(X398),X400)
| r1(X397,X398)
| r1(sK0,X397) ) ).
cnf(u117,negated_conjecture,
( ~ r1(X81,sK45(X81))
| p1(X80)
| r1(X80,X81)
| r1(X79,X80)
| r1(X78,X79)
| r1(X77,X78)
| r1(X76,X77)
| r1(X75,X76)
| r1(X74,X75)
| r1(X73,X74)
| r1(sK44(X71),X73)
| r1(X70,X71)
| r1(X69,X70)
| r1(X68,X69)
| r1(X67,X68)
| r1(X66,X67)
| r1(X65,X66)
| r1(X64,X65)
| r1(sK42(X62),X64)
| r1(X61,X62)
| r1(X60,X61)
| r1(X59,X60)
| r1(X58,X59)
| r1(X57,X58)
| r1(X56,X57)
| r1(X55,X56)
| r1(sK39(X53),X55)
| r1(X52,X53)
| r1(X51,X52)
| r1(X50,X51)
| r1(X49,X50)
| r1(X48,X49)
| r1(X47,X48)
| r1(X46,X47)
| r1(sK35(X44),X46)
| r1(X43,X44)
| r1(X42,X43)
| r1(X41,X42)
| r1(X40,X41)
| r1(X39,X40)
| r1(X38,X39)
| r1(X37,X38)
| r1(sK30(X35),X37)
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u78,negated_conjecture,
( ~ r1(X317,sK13(X317))
| r1(X316,X317)
| r1(X315,X316)
| r1(X314,X315)
| r1(X313,X314)
| r1(X312,X313)
| r1(X311,X312)
| r1(X310,X311)
| r1(sK5(X308),X310)
| r1(X307,X308)
| r1(X306,X307)
| r1(X305,X306)
| r1(sK0,X305) ) ).
cnf(u68,negated_conjecture,
( ~ r1(X358,sK4(X358))
| r1(X357,X358)
| r1(X356,X357)
| r1(sK0,X356) ) ).
cnf(u70,negated_conjecture,
( ~ r1(X248,sK6(X248))
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u111,negated_conjecture,
( ~ r1(X152,sK41(X152))
| r1(X151,X152)
| r1(X150,X151)
| r1(X149,X150)
| r1(X148,X149)
| r1(X147,X148)
| r1(X146,X147)
| r1(X145,X146)
| r1(sK38(X143),X145)
| r1(X142,X143)
| r1(X141,X142)
| r1(X140,X141)
| r1(X139,X140)
| r1(X138,X139)
| r1(X137,X138)
| r1(X136,X137)
| r1(sK34(X134),X136)
| r1(X133,X134)
| r1(X132,X133)
| r1(X131,X132)
| r1(X130,X131)
| r1(X129,X130)
| r1(X128,X129)
| r1(X127,X128)
| r1(sK29(X125),X127)
| r1(X124,X125)
| r1(X123,X124)
| r1(X122,X123)
| r1(X121,X122)
| r1(X120,X121)
| r1(X119,X120)
| r1(X118,X119)
| r1(sK23(X116),X118)
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u64,axiom,
~ r1(X0,X0) ).
cnf(u105,negated_conjecture,
( ~ r1(X294,sK36(X294))
| p1(X293)
| r1(X293,X294)
| r1(X292,X293)
| r1(X291,X292)
| r1(X290,X291)
| r1(X289,X290)
| r1(X288,X289)
| r1(X287,X288)
| r1(X286,X287)
| r1(sK32(X284),X286)
| r1(X283,X284)
| r1(X282,X283)
| r1(X281,X282)
| r1(X280,X281)
| r1(X279,X280)
| r1(X278,X279)
| r1(X277,X278)
| r1(sK27(X275),X277)
| r1(X274,X275)
| r1(X273,X274)
| r1(X272,X273)
| r1(X271,X272)
| r1(X270,X271)
| r1(X269,X270)
| r1(X268,X269)
| r1(sK21(X266),X268)
| r1(X265,X266)
| r1(X264,X265)
| r1(X263,X264)
| r1(X262,X263)
| r1(X261,X262)
| r1(X260,X261)
| r1(X259,X260)
| r1(sK14(X257),X259)
| r1(X256,X257)
| r1(X255,X256)
| r1(X254,X255)
| r1(X253,X254)
| r1(X252,X253)
| r1(X251,X252)
| r1(X250,X251)
| r1(sK6(X248),X250)
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u107,negated_conjecture,
( ~ r1(X143,sK38(X143))
| r1(X142,X143)
| r1(X141,X142)
| r1(X140,X141)
| r1(X139,X140)
| r1(X138,X139)
| r1(X137,X138)
| r1(X136,X137)
| r1(sK34(X134),X136)
| r1(X133,X134)
| r1(X132,X133)
| r1(X131,X132)
| r1(X130,X131)
| r1(X129,X130)
| r1(X128,X129)
| r1(X127,X128)
| r1(sK29(X125),X127)
| r1(X124,X125)
| r1(X123,X124)
| r1(X122,X123)
| r1(X121,X122)
| r1(X120,X121)
| r1(X119,X120)
| r1(X118,X119)
| r1(sK23(X116),X118)
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u97,negated_conjecture,
( ~ r1(X35,sK30(X35))
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u99,negated_conjecture,
( ~ r1(X345,sK31(X345))
| p1(X344)
| r1(X344,X345)
| r1(X343,X344)
| r1(X342,X343)
| r1(X341,X342)
| r1(X340,X341)
| r1(X339,X340)
| r1(X338,X339)
| r1(X337,X338)
| r1(sK26(X335),X337)
| r1(X334,X335)
| r1(X333,X334)
| r1(X332,X333)
| r1(X331,X332)
| r1(X330,X331)
| r1(X329,X330)
| r1(X328,X329)
| r1(sK20(X326),X328)
| r1(X325,X326)
| r1(X324,X325)
| r1(X323,X324)
| r1(X322,X323)
| r1(X321,X322)
| r1(X320,X321)
| r1(X319,X320)
| r1(sK13(X317),X319)
| r1(X316,X317)
| r1(X315,X316)
| r1(X314,X315)
| r1(X313,X314)
| r1(X312,X313)
| r1(X311,X312)
| r1(X310,X311)
| r1(sK5(X308),X310)
| r1(X307,X308)
| r1(X306,X307)
| r1(X305,X306)
| r1(sK0,X305) ) ).
cnf(u109,negated_conjecture,
( ~ p1(X304)
| p1(X293)
| r1(X303,X304)
| r1(X302,X303)
| r1(X301,X302)
| r1(X300,X301)
| r1(X299,X300)
| r1(X298,X299)
| r1(X297,X298)
| r1(X296,X297)
| r1(sK36(X294),X296)
| r1(X293,X294)
| r1(X292,X293)
| r1(X291,X292)
| r1(X290,X291)
| r1(X289,X290)
| r1(X288,X289)
| r1(X287,X288)
| r1(X286,X287)
| r1(sK32(X284),X286)
| r1(X283,X284)
| r1(X282,X283)
| r1(X281,X282)
| r1(X280,X281)
| r1(X279,X280)
| r1(X278,X279)
| r1(X277,X278)
| r1(sK27(X275),X277)
| r1(X274,X275)
| r1(X273,X274)
| r1(X272,X273)
| r1(X271,X272)
| r1(X270,X271)
| r1(X269,X270)
| r1(X268,X269)
| r1(sK21(X266),X268)
| r1(X265,X266)
| r1(X264,X265)
| r1(X263,X264)
| r1(X262,X263)
| r1(X261,X262)
| r1(X260,X261)
| r1(X259,X260)
| r1(sK14(X257),X259)
| r1(X256,X257)
| r1(X255,X256)
| r1(X254,X255)
| r1(X253,X254)
| r1(X252,X253)
| r1(X251,X252)
| r1(X250,X251)
| r1(sK6(X248),X250)
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u101,negated_conjecture,
( ~ r1(X214,sK33(X214))
| r1(X213,X214)
| r1(X212,X213)
| r1(X211,X212)
| r1(X210,X211)
| r1(X209,X210)
| r1(X208,X209)
| r1(X207,X208)
| r1(sK28(X205),X207)
| r1(X204,X205)
| r1(X203,X204)
| r1(X202,X203)
| r1(X201,X202)
| r1(X200,X201)
| r1(X199,X200)
| r1(X198,X199)
| r1(sK22(X196),X198)
| r1(X195,X196)
| r1(X194,X195)
| r1(X193,X194)
| r1(X192,X193)
| r1(X191,X192)
| r1(X190,X191)
| r1(X189,X190)
| r1(sK15(X187),X189)
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u103,negated_conjecture,
( ~ r1(X44,sK35(X44))
| r1(X43,X44)
| r1(X42,X43)
| r1(X41,X42)
| r1(X40,X41)
| r1(X39,X40)
| r1(X38,X39)
| r1(X37,X38)
| r1(sK30(X35),X37)
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u89,negated_conjecture,
( ~ r1(X116,sK23(X116))
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u91,negated_conjecture,
( ~ p1(X427)
| p1(X416)
| r1(X426,X427)
| r1(X425,X426)
| r1(X424,X425)
| r1(X423,X424)
| r1(X422,X423)
| r1(X421,X422)
| r1(X420,X421)
| r1(X419,X420)
| r1(sK18(X417),X419)
| r1(X416,X417)
| r1(X415,X416)
| r1(X414,X415)
| r1(X413,X414)
| r1(X412,X413)
| r1(X411,X412)
| r1(X410,X411)
| r1(X409,X410)
| r1(sK11(X407),X409)
| r1(X406,X407)
| r1(X405,X406)
| r1(X404,X405)
| r1(X403,X404)
| r1(X402,X403)
| r1(X401,X402)
| r1(X400,X401)
| r1(sK3(X398),X400)
| r1(X397,X398)
| r1(sK0,X397) ) ).
cnf(u81,negated_conjecture,
( ~ r1(X107,sK16(X107))
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u83,negated_conjecture,
( ~ p1(X448)
| p1(X437)
| r1(X447,X448)
| r1(X446,X447)
| r1(X445,X446)
| r1(X444,X445)
| r1(X443,X444)
| r1(X442,X443)
| r1(X441,X442)
| r1(X440,X441)
| r1(sK10(X438),X440)
| r1(X437,X438)
| r1(X436,X437)
| r1(X435,X436)
| r1(X434,X435)
| r1(X433,X434)
| r1(X432,X433)
| r1(X431,X432)
| r1(X430,X431)
| r1(sK1(X428),X430)
| r1(sK0,X428) ) ).
cnf(u93,negated_conjecture,
( ~ r1(X335,sK26(X335))
| r1(X334,X335)
| r1(X333,X334)
| r1(X332,X333)
| r1(X331,X332)
| r1(X330,X331)
| r1(X329,X330)
| r1(X328,X329)
| r1(sK20(X326),X328)
| r1(X325,X326)
| r1(X324,X325)
| r1(X323,X324)
| r1(X322,X323)
| r1(X321,X322)
| r1(X320,X321)
| r1(X319,X320)
| r1(sK13(X317),X319)
| r1(X316,X317)
| r1(X315,X316)
| r1(X314,X315)
| r1(X313,X314)
| r1(X312,X313)
| r1(X311,X312)
| r1(X310,X311)
| r1(sK5(X308),X310)
| r1(X307,X308)
| r1(X306,X307)
| r1(X305,X306)
| r1(sK0,X305) ) ).
cnf(u85,negated_conjecture,
( ~ r1(X376,sK19(X376))
| r1(X375,X376)
| r1(X374,X375)
| r1(X373,X374)
| r1(X372,X373)
| r1(X371,X372)
| r1(X370,X371)
| r1(X369,X370)
| r1(sK12(X367),X369)
| r1(X366,X367)
| r1(X365,X366)
| r1(X364,X365)
| r1(X363,X364)
| r1(X362,X363)
| r1(X361,X362)
| r1(X360,X361)
| r1(sK4(X358),X360)
| r1(X357,X358)
| r1(X356,X357)
| r1(sK0,X356) ) ).
cnf(u114,negated_conjecture,
( ~ r1(X162,sK43(X162))
| p1(X161)
| r1(X161,X162)
| r1(X160,X161)
| r1(X159,X160)
| r1(X158,X159)
| r1(X157,X158)
| r1(X156,X157)
| r1(X155,X156)
| r1(X154,X155)
| r1(sK41(X152),X154)
| r1(X151,X152)
| r1(X150,X151)
| r1(X149,X150)
| r1(X148,X149)
| r1(X147,X148)
| r1(X146,X147)
| r1(X145,X146)
| r1(sK38(X143),X145)
| r1(X142,X143)
| r1(X141,X142)
| r1(X140,X141)
| r1(X139,X140)
| r1(X138,X139)
| r1(X137,X138)
| r1(X136,X137)
| r1(sK34(X134),X136)
| r1(X133,X134)
| r1(X132,X133)
| r1(X131,X132)
| r1(X130,X131)
| r1(X129,X130)
| r1(X128,X129)
| r1(X127,X128)
| r1(sK29(X125),X127)
| r1(X124,X125)
| r1(X123,X124)
| r1(X122,X123)
| r1(X121,X122)
| r1(X120,X121)
| r1(X119,X120)
| r1(X118,X119)
| r1(sK23(X116),X118)
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u87,negated_conjecture,
( ~ r1(X266,sK21(X266))
| r1(X265,X266)
| r1(X264,X265)
| r1(X263,X264)
| r1(X262,X263)
| r1(X261,X262)
| r1(X260,X261)
| r1(X259,X260)
| r1(sK14(X257),X259)
| r1(X256,X257)
| r1(X255,X256)
| r1(X254,X255)
| r1(X253,X254)
| r1(X252,X253)
| r1(X251,X252)
| r1(X250,X251)
| r1(sK6(X248),X250)
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u79,negated_conjecture,
( ~ r1(X257,sK14(X257))
| r1(X256,X257)
| r1(X255,X256)
| r1(X254,X255)
| r1(X253,X254)
| r1(X252,X253)
| r1(X251,X252)
| r1(X250,X251)
| r1(sK6(X248),X250)
| r1(X247,X248)
| r1(X246,X247)
| r1(X245,X246)
| r1(X244,X245)
| r1(sK0,X244) ) ).
cnf(u73,negated_conjecture,
( ~ r1(X8,sK9(X8))
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u118,negated_conjecture,
( ~ p1(X91)
| p1(X80)
| r1(X90,X91)
| r1(X89,X90)
| r1(X88,X89)
| r1(X87,X88)
| r1(X86,X87)
| r1(X85,X86)
| r1(X84,X85)
| r1(X83,X84)
| r1(sK45(X81),X83)
| r1(X80,X81)
| r1(X79,X80)
| r1(X78,X79)
| r1(X77,X78)
| r1(X76,X77)
| r1(X75,X76)
| r1(X74,X75)
| r1(X73,X74)
| r1(sK44(X71),X73)
| r1(X70,X71)
| r1(X69,X70)
| r1(X68,X69)
| r1(X67,X68)
| r1(X66,X67)
| r1(X65,X66)
| r1(X64,X65)
| r1(sK42(X62),X64)
| r1(X61,X62)
| r1(X60,X61)
| r1(X59,X60)
| r1(X58,X59)
| r1(X57,X58)
| r1(X56,X57)
| r1(X55,X56)
| r1(sK39(X53),X55)
| r1(X52,X53)
| r1(X51,X52)
| r1(X50,X51)
| r1(X49,X50)
| r1(X48,X49)
| r1(X47,X48)
| r1(X46,X47)
| r1(sK35(X44),X46)
| r1(X43,X44)
| r1(X42,X43)
| r1(X41,X42)
| r1(X40,X41)
| r1(X39,X40)
| r1(X38,X39)
| r1(X37,X38)
| r1(sK30(X35),X37)
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u75,negated_conjecture,
( ~ r1(X438,sK10(X438))
| p1(X437)
| r1(X437,X438)
| r1(X436,X437)
| r1(X435,X436)
| r1(X434,X435)
| r1(X433,X434)
| r1(X432,X433)
| r1(X431,X432)
| r1(X430,X431)
| r1(sK1(X428),X430)
| r1(sK0,X428) ) ).
cnf(u65,negated_conjecture,
( ~ r1(X428,sK1(X428))
| r1(sK0,X428) ) ).
cnf(u95,negated_conjecture,
( ~ r1(X205,sK28(X205))
| r1(X204,X205)
| r1(X203,X204)
| r1(X202,X203)
| r1(X201,X202)
| r1(X200,X201)
| r1(X199,X200)
| r1(X198,X199)
| r1(sK22(X196),X198)
| r1(X195,X196)
| r1(X194,X195)
| r1(X193,X194)
| r1(X192,X193)
| r1(X191,X192)
| r1(X190,X191)
| r1(X189,X190)
| r1(sK15(X187),X189)
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u67,negated_conjecture,
( ~ r1(X398,sK3(X398))
| r1(X397,X398)
| r1(sK0,X397) ) ).
cnf(u104,negated_conjecture,
( ~ p1(X355)
| p1(X344)
| r1(X354,X355)
| r1(X353,X354)
| r1(X352,X353)
| r1(X351,X352)
| r1(X350,X351)
| r1(X349,X350)
| r1(X348,X349)
| r1(X347,X348)
| r1(sK31(X345),X347)
| r1(X344,X345)
| r1(X343,X344)
| r1(X342,X343)
| r1(X341,X342)
| r1(X340,X341)
| r1(X339,X340)
| r1(X338,X339)
| r1(X337,X338)
| r1(sK26(X335),X337)
| r1(X334,X335)
| r1(X333,X334)
| r1(X332,X333)
| r1(X331,X332)
| r1(X330,X331)
| r1(X329,X330)
| r1(X328,X329)
| r1(sK20(X326),X328)
| r1(X325,X326)
| r1(X324,X325)
| r1(X323,X324)
| r1(X322,X323)
| r1(X321,X322)
| r1(X320,X321)
| r1(X319,X320)
| r1(sK13(X317),X319)
| r1(X316,X317)
| r1(X315,X316)
| r1(X314,X315)
| r1(X313,X314)
| r1(X312,X313)
| r1(X311,X312)
| r1(X310,X311)
| r1(sK5(X308),X310)
| r1(X307,X308)
| r1(X306,X307)
| r1(X305,X306)
| r1(sK0,X305) ) ).
cnf(u77,negated_conjecture,
( ~ r1(X367,sK12(X367))
| r1(X366,X367)
| r1(X365,X366)
| r1(X364,X365)
| r1(X363,X364)
| r1(X362,X363)
| r1(X361,X362)
| r1(X360,X361)
| r1(sK4(X358),X360)
| r1(X357,X358)
| r1(X356,X357)
| r1(sK0,X356) ) ).
cnf(u106,negated_conjecture,
( ~ r1(X223,sK37(X223))
| r1(X222,X223)
| r1(X221,X222)
| r1(X220,X221)
| r1(X219,X220)
| r1(X218,X219)
| r1(X217,X218)
| r1(X216,X217)
| r1(sK33(X214),X216)
| r1(X213,X214)
| r1(X212,X213)
| r1(X211,X212)
| r1(X210,X211)
| r1(X209,X210)
| r1(X208,X209)
| r1(X207,X208)
| r1(sK28(X205),X207)
| r1(X204,X205)
| r1(X203,X204)
| r1(X202,X203)
| r1(X201,X202)
| r1(X200,X201)
| r1(X199,X200)
| r1(X198,X199)
| r1(sK22(X196),X198)
| r1(X195,X196)
| r1(X194,X195)
| r1(X193,X194)
| r1(X192,X193)
| r1(X191,X192)
| r1(X190,X191)
| r1(X189,X190)
| r1(sK15(X187),X189)
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u69,negated_conjecture,
( ~ r1(X308,sK5(X308))
| r1(X307,X308)
| r1(X306,X307)
| r1(X305,X306)
| r1(sK0,X305) ) ).
cnf(u116,negated_conjecture,
( ~ p1(X172)
| p1(X161)
| r1(X171,X172)
| r1(X170,X171)
| r1(X169,X170)
| r1(X168,X169)
| r1(X167,X168)
| r1(X166,X167)
| r1(X165,X166)
| r1(X164,X165)
| r1(sK43(X162),X164)
| r1(X161,X162)
| r1(X160,X161)
| r1(X159,X160)
| r1(X158,X159)
| r1(X157,X158)
| r1(X156,X157)
| r1(X155,X156)
| r1(X154,X155)
| r1(sK41(X152),X154)
| r1(X151,X152)
| r1(X150,X151)
| r1(X149,X150)
| r1(X148,X149)
| r1(X147,X148)
| r1(X146,X147)
| r1(X145,X146)
| r1(sK38(X143),X145)
| r1(X142,X143)
| r1(X141,X142)
| r1(X140,X141)
| r1(X139,X140)
| r1(X138,X139)
| r1(X137,X138)
| r1(X136,X137)
| r1(sK34(X134),X136)
| r1(X133,X134)
| r1(X132,X133)
| r1(X131,X132)
| r1(X130,X131)
| r1(X129,X130)
| r1(X128,X129)
| r1(X127,X128)
| r1(sK29(X125),X127)
| r1(X124,X125)
| r1(X123,X124)
| r1(X122,X123)
| r1(X121,X122)
| r1(X120,X121)
| r1(X119,X120)
| r1(X118,X119)
| r1(sK23(X116),X118)
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u98,negated_conjecture,
( ~ p1(X396)
| p1(X385)
| r1(X395,X396)
| r1(X394,X395)
| r1(X393,X394)
| r1(X392,X393)
| r1(X391,X392)
| r1(X390,X391)
| r1(X389,X390)
| r1(X388,X389)
| r1(sK25(X386),X388)
| r1(X385,X386)
| r1(X384,X385)
| r1(X383,X384)
| r1(X382,X383)
| r1(X381,X382)
| r1(X380,X381)
| r1(X379,X380)
| r1(X378,X379)
| r1(sK19(X376),X378)
| r1(X375,X376)
| r1(X374,X375)
| r1(X373,X374)
| r1(X372,X373)
| r1(X371,X372)
| r1(X370,X371)
| r1(X369,X370)
| r1(sK12(X367),X369)
| r1(X366,X367)
| r1(X365,X366)
| r1(X364,X365)
| r1(X363,X364)
| r1(X362,X363)
| r1(X361,X362)
| r1(X360,X361)
| r1(sK4(X358),X360)
| r1(X357,X358)
| r1(X356,X357)
| r1(sK0,X356) ) ).
cnf(u71,negated_conjecture,
( ~ r1(X178,sK7(X178))
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u108,negated_conjecture,
( ~ r1(X53,sK39(X53))
| r1(X52,X53)
| r1(X51,X52)
| r1(X50,X51)
| r1(X49,X50)
| r1(X48,X49)
| r1(X47,X48)
| r1(X46,X47)
| r1(sK35(X44),X46)
| r1(X43,X44)
| r1(X42,X43)
| r1(X41,X42)
| r1(X40,X41)
| r1(X39,X40)
| r1(X38,X39)
| r1(X37,X38)
| r1(sK30(X35),X37)
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u112,negated_conjecture,
( ~ r1(X62,sK42(X62))
| r1(X61,X62)
| r1(X60,X61)
| r1(X59,X60)
| r1(X58,X59)
| r1(X57,X58)
| r1(X56,X57)
| r1(X55,X56)
| r1(sK39(X53),X55)
| r1(X52,X53)
| r1(X51,X52)
| r1(X50,X51)
| r1(X49,X50)
| r1(X48,X49)
| r1(X47,X48)
| r1(X46,X47)
| r1(sK35(X44),X46)
| r1(X43,X44)
| r1(X42,X43)
| r1(X41,X42)
| r1(X40,X41)
| r1(X39,X40)
| r1(X38,X39)
| r1(X37,X38)
| r1(sK30(X35),X37)
| r1(X34,X35)
| r1(X33,X34)
| r1(X32,X33)
| r1(X31,X32)
| r1(X30,X31)
| r1(X29,X30)
| r1(X28,X29)
| r1(sK24(X26),X28)
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
cnf(u110,negated_conjecture,
( ~ r1(X233,sK40(X233))
| p1(X232)
| r1(X232,X233)
| r1(X231,X232)
| r1(X230,X231)
| r1(X229,X230)
| r1(X228,X229)
| r1(X227,X228)
| r1(X226,X227)
| r1(X225,X226)
| r1(sK37(X223),X225)
| r1(X222,X223)
| r1(X221,X222)
| r1(X220,X221)
| r1(X219,X220)
| r1(X218,X219)
| r1(X217,X218)
| r1(X216,X217)
| r1(sK33(X214),X216)
| r1(X213,X214)
| r1(X212,X213)
| r1(X211,X212)
| r1(X210,X211)
| r1(X209,X210)
| r1(X208,X209)
| r1(X207,X208)
| r1(sK28(X205),X207)
| r1(X204,X205)
| r1(X203,X204)
| r1(X202,X203)
| r1(X201,X202)
| r1(X200,X201)
| r1(X199,X200)
| r1(X198,X199)
| r1(sK22(X196),X198)
| r1(X195,X196)
| r1(X194,X195)
| r1(X193,X194)
| r1(X192,X193)
| r1(X191,X192)
| r1(X190,X191)
| r1(X189,X190)
| r1(sK15(X187),X189)
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u102,negated_conjecture,
( ~ r1(X134,sK34(X134))
| r1(X133,X134)
| r1(X132,X133)
| r1(X131,X132)
| r1(X130,X131)
| r1(X129,X130)
| r1(X128,X129)
| r1(X127,X128)
| r1(sK29(X125),X127)
| r1(X124,X125)
| r1(X123,X124)
| r1(X122,X123)
| r1(X121,X122)
| r1(X120,X121)
| r1(X119,X120)
| r1(X118,X119)
| r1(sK23(X116),X118)
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u96,negated_conjecture,
( ~ r1(X125,sK29(X125))
| r1(X124,X125)
| r1(X123,X124)
| r1(X122,X123)
| r1(X121,X122)
| r1(X120,X121)
| r1(X119,X120)
| r1(X118,X119)
| r1(sK23(X116),X118)
| r1(X115,X116)
| r1(X114,X115)
| r1(X113,X114)
| r1(X112,X113)
| r1(X111,X112)
| r1(X110,X111)
| r1(X109,X110)
| r1(sK16(X107),X109)
| r1(X106,X107)
| r1(X105,X106)
| r1(X104,X105)
| r1(X103,X104)
| r1(X102,X103)
| r1(X101,X102)
| r1(X100,X101)
| r1(sK8(X98),X100)
| r1(X97,X98)
| r1(X96,X97)
| r1(X95,X96)
| r1(X94,X95)
| r1(X93,X94)
| r1(X92,X93)
| r1(sK0,X92) ) ).
cnf(u88,negated_conjecture,
( ~ r1(X196,sK22(X196))
| r1(X195,X196)
| r1(X194,X195)
| r1(X193,X194)
| r1(X192,X193)
| r1(X191,X192)
| r1(X190,X191)
| r1(X189,X190)
| r1(sK15(X187),X189)
| r1(X186,X187)
| r1(X185,X186)
| r1(X184,X185)
| r1(X183,X184)
| r1(X182,X183)
| r1(X181,X182)
| r1(X180,X181)
| r1(sK7(X178),X180)
| r1(X177,X178)
| r1(X176,X177)
| r1(X175,X176)
| r1(X174,X175)
| r1(X173,X174)
| r1(sK0,X173) ) ).
cnf(u90,negated_conjecture,
( ~ r1(X26,sK24(X26))
| r1(X25,X26)
| r1(X24,X25)
| r1(X23,X24)
| r1(X22,X23)
| r1(X21,X22)
| r1(X20,X21)
| r1(X19,X20)
| r1(sK17(X17),X19)
| r1(X16,X17)
| r1(X15,X16)
| r1(X14,X15)
| r1(X13,X14)
| r1(X12,X13)
| r1(X11,X12)
| r1(X10,X11)
| r1(sK9(X8),X10)
| r1(X7,X8)
| r1(X6,X7)
| r1(X5,X6)
| r1(X4,X5)
| r1(X3,X4)
| r1(X2,X3)
| r1(X1,X2)
| r1(sK0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL663+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n006.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 16:25:11 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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.19/0.48 % (3150184)Will run a generic schedule for satisfiability detection.
% 0.19/0.48 % (3150190)% WARNING: option uhcvi not known.
% 0.19/0.48 % (3150190)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=832795987:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.48 % (3150189)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1865265251_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.48 % (3150192)dis+10_1_sil=32000:sp=arity:random_seed=2727255320:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.48 % (3150191)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4009932600:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.48 % (3150194)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2688386486:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.48 % (3150193)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=278323557:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.48 % (3150195)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=863961764:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.48 % (3150190) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3150184-3150190"...
% 0.19/0.48 % (3150190)...printing done.
% 0.19/0.48 % SZS status CounterSatisfiable for theBenchmark
% 0.19/0.48 % SZS output start Saturation.
% See solution above
% 0.19/0.48 % SZS output start Definitions and Model Updates.
% 0.19/0.48 globally flip the polarity of every occurrence of predicate "r1"
% 0.19/0.48 % SZS output end Definitions and Model Updates.
% 0.19/0.48 % (3150190)------------------------------
% 0.19/0.48 % (3150190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.48 % (3150190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.48 % (3150190)CaDiCaL version: 2.1.3
% 0.19/0.48 % (3150190)Termination reason: Satisfiable
% 0.19/0.48 % (3150190)Time elapsed: 0.021 s
% 0.19/0.48 % (3150190)Peak memory usage: 12 MB
% 0.19/0.48 % (3150190)Instructions burned: 79 (million)
% 0.19/0.48 % (3150184)Success in time 0.054 s
% 0.19/0.48 % Vampire exiting
%------------------------------------------------------------------------------