%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL676+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 02:08:05 PM UTC 2026
% Result : Theorem 40.89s 7.32s
% Output : CNFRefutation 40.89s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f101ERROR: Could not build tree for root c_33243ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X1,X2)
& r1(X0,X1) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
fof(f8,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f9,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(flattening,[],[f8]) ).
fof(f102,plain,
! [X0] :
( ~ sP88(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p2(X4)
& r1(X0,X4) ) ) ),
inference(nnf_transformation,[],[f100]) ).
fof(f103,plain,
! [X0] :
( ~ sP88(X0)
| ( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] :
( ~ p2(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p2(X2)
| ~ r1(X0,X2) )
& ? [X1] :
( ~ p2(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f102]) ).
fof(f104,plain,
! [X0] :
( ~ sP88(X0)
| ( ! [X2] :
( ( p2(sK90(X2))
& ~ p2(sK91(X2))
& r1(sK90(X2),sK91(X2))
& r1(X2,sK90(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK89(X0))
& r1(X0,sK89(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK89,sK90,sK91]),skolemize(X1,sK89(X0)),skolemize(X3,sK90(X2)),skolemize(X4,sK91(X2))],[f103]) ).
fof(f105,plain,
! [X0] :
( ~ sP87(X0)
| ( ! [X15] :
( ? [X16] :
( p2(X16)
& ? [X17] :
( ~ p2(X17)
& r1(X16,X17) )
& r1(X15,X16) )
| p2(X15)
| ~ r1(X0,X15) )
& ? [X14] :
( ~ p2(X14)
& r1(X0,X14) ) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f106,plain,
! [X0] :
( ~ sP87(X0)
| ( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] :
( ~ p2(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p2(X2)
| ~ r1(X0,X2) )
& ? [X1] :
( ~ p2(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ~ sP87(X0)
| ( ! [X2] :
( ( p2(sK93(X2))
& ~ p2(sK94(X2))
& r1(sK93(X2),sK94(X2))
& r1(X2,sK93(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK92(X0))
& r1(X0,sK92(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92,sK93,sK94]),skolemize(X1,sK92(X0)),skolemize(X3,sK93(X2)),skolemize(X4,sK94(X2))],[f106]) ).
fof(f362,plain,
? [X0] :
( ! [X106] :
( ? [X107] :
( ! [X108] :
( ~ p2(X108)
| ! [X109] :
( p2(X109)
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
& ~ p2(X107)
& r1(X106,X107) )
| p2(X106)
| ~ r1(X0,X106) )
& ( ? [X100] :
( ! [X102] :
( ( ? [X105] : r1(X102,X105)
& ~ p1(X102) )
| ! [X103] :
( ! [X104] : ~ r1(X103,X104)
| p1(X103)
| ~ r1(X102,X103) )
| ~ r1(X100,X102) )
& ? [X101] : r1(X100,X101)
& ~ p1(X100)
& r1(X0,X100) )
| ! [X99] : ~ r1(X0,X99)
| p1(X0) )
& ( ? [X93] :
( ! [X95] :
( ( ? [X98] : r1(X95,X98)
& ~ p1(X95)
& ~ p2(X95) )
| ! [X96] :
( ! [X97] : ~ r1(X96,X97)
| p1(X96)
| p2(X96)
| ~ r1(X95,X96) )
| ~ r1(X93,X95) )
& ? [X94] : r1(X93,X94)
& ~ p1(X93)
& ~ p2(X93)
& r1(X0,X93) )
| ! [X92] : ~ r1(X0,X92)
| p1(X0)
| p2(X0) )
& ( ? [X90] :
( sP0(X90)
& ? [X91] : r1(X90,X91)
& ~ p1(X90)
& ~ p2(X90)
& ~ p3(X90)
& r1(X0,X90) )
| ! [X89] : ~ r1(X0,X89)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X87] :
( sP1(X87)
& ? [X88] : r1(X87,X88)
& ~ p1(X87)
& ~ p2(X87)
& ~ p3(X87)
& ~ p4(X87)
& r1(X0,X87) )
| ! [X86] : ~ r1(X0,X86)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X85] :
( sP2(X85)
& sP3(X85)
& ~ p1(X85)
& r1(X0,X85) )
| ! [X83] :
( ! [X84] : ~ r1(X83,X84)
| p1(X83)
| p2(X83)
| p3(X83)
| p4(X83)
| ~ r1(X0,X83) )
| p1(X0) )
& ( ? [X82] :
( sP4(X82)
& sP5(X82)
& ~ p1(X82)
& ~ p2(X82)
& r1(X0,X82) )
| ! [X80] :
( ! [X81] : ~ r1(X80,X81)
| p1(X80)
| p2(X80)
| p3(X80)
| p4(X80)
| ~ r1(X0,X80) )
| p1(X0)
| p2(X0) )
& ( ? [X79] :
( sP8(X79)
& sP7(X79)
& ~ p1(X79)
& ~ p2(X79)
& ~ p3(X79)
& r1(X0,X79) )
| ! [X77] :
( ! [X78] : ~ r1(X77,X78)
| p1(X77)
| p2(X77)
| p3(X77)
| p4(X77)
| ~ r1(X0,X77) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X76] :
( sP11(X76)
& sP10(X76)
& ~ p1(X76)
& ~ p2(X76)
& ~ p3(X76)
& ~ p4(X76)
& r1(X0,X76) )
| ! [X74] :
( ! [X75] : ~ r1(X74,X75)
| p1(X74)
| p2(X74)
| p3(X74)
| p4(X74)
| ~ r1(X0,X74) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X73] :
( sP14(X73)
& sP15(X73)
& ~ p1(X73)
& r1(X0,X73) )
| ! [X70] :
( ! [X71] :
( ! [X72] : ~ r1(X71,X72)
| p1(X71)
| p2(X71)
| p3(X71)
| p4(X71)
| ~ r1(X70,X71) )
| p1(X70)
| p2(X70)
| p3(X70)
| p4(X70)
| ~ r1(X0,X70) )
| p1(X0) )
& ( ? [X69] :
( sP18(X69)
& sP19(X69)
& ~ p1(X69)
& ~ p2(X69)
& r1(X0,X69) )
| ! [X66] :
( ! [X67] :
( ! [X68] : ~ r1(X67,X68)
| p1(X67)
| p2(X67)
| p3(X67)
| p4(X67)
| ~ r1(X66,X67) )
| p1(X66)
| p2(X66)
| p3(X66)
| p4(X66)
| ~ r1(X0,X66) )
| p1(X0)
| p2(X0) )
& ( ? [X65] :
( sP24(X65)
& sP23(X65)
& ~ p1(X65)
& ~ p2(X65)
& ~ p3(X65)
& r1(X0,X65) )
| ! [X62] :
( ! [X63] :
( ! [X64] : ~ r1(X63,X64)
| p1(X63)
| p2(X63)
| p3(X63)
| p4(X63)
| ~ r1(X62,X63) )
| p1(X62)
| p2(X62)
| p3(X62)
| p4(X62)
| ~ r1(X0,X62) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X61] :
( sP29(X61)
& sP28(X61)
& ~ p1(X61)
& ~ p2(X61)
& ~ p3(X61)
& ~ p4(X61)
& r1(X0,X61) )
| ! [X58] :
( ! [X59] :
( ! [X60] : ~ r1(X59,X60)
| p1(X59)
| p2(X59)
| p3(X59)
| p4(X59)
| ~ r1(X58,X59) )
| p1(X58)
| p2(X58)
| p3(X58)
| p4(X58)
| ~ r1(X0,X58) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X57] :
( sP34(X57)
& sP35(X57)
& ~ p1(X57)
& r1(X0,X57) )
| ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] : ~ r1(X55,X56)
| p1(X55)
| p2(X55)
| p3(X55)
| p4(X55)
| ~ r1(X54,X55) )
| p1(X54)
| p2(X54)
| p3(X54)
| p4(X54)
| ~ r1(X53,X54) )
| p1(X53)
| p2(X53)
| p3(X53)
| p4(X53)
| ~ r1(X0,X53) )
| p1(X0) )
& ( ? [X52] :
( sP40(X52)
& sP41(X52)
& ~ p1(X52)
& ~ p2(X52)
& r1(X0,X52) )
| ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] : ~ r1(X50,X51)
| p1(X50)
| p2(X50)
| p3(X50)
| p4(X50)
| ~ r1(X49,X50) )
| p1(X49)
| p2(X49)
| p3(X49)
| p4(X49)
| ~ r1(X48,X49) )
| p1(X48)
| p2(X48)
| p3(X48)
| p4(X48)
| ~ r1(X0,X48) )
| p1(X0)
| p2(X0) )
& ( ? [X47] :
( sP48(X47)
& sP47(X47)
& ~ p1(X47)
& ~ p2(X47)
& ~ p3(X47)
& r1(X0,X47) )
| ! [X43] :
( ! [X44] :
( ! [X45] :
( ! [X46] : ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(X44,X45) )
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(X43,X44) )
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43)
| ~ r1(X0,X43) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X42] :
( sP55(X42)
& sP54(X42)
& ~ p1(X42)
& ~ p2(X42)
& ~ p3(X42)
& ~ p4(X42)
& r1(X0,X42) )
| ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] : ~ r1(X40,X41)
| p1(X40)
| p2(X40)
| p3(X40)
| p4(X40)
| ~ r1(X39,X40) )
| p1(X39)
| p2(X39)
| p3(X39)
| p4(X39)
| ~ r1(X38,X39) )
| p1(X38)
| p2(X38)
| p3(X38)
| p4(X38)
| ~ r1(X0,X38) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X37] :
( sP62(X37)
& sP63(X37)
& ~ p1(X37)
& r1(X0,X37) )
| ! [X32] :
( ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] : ~ r1(X35,X36)
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X34,X35) )
| p1(X34)
| p2(X34)
| p3(X34)
| p4(X34)
| ~ r1(X33,X34) )
| p1(X33)
| p2(X33)
| p3(X33)
| p4(X33)
| ~ r1(X32,X33) )
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(X0,X32) )
| p1(X0) )
& ( ? [X31] :
( sP70(X31)
& sP71(X31)
& ~ p1(X31)
& ~ p2(X31)
& r1(X0,X31) )
| ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29) )
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(X27,X28) )
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(X26,X27) )
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(X0,X26) )
| p1(X0)
| p2(X0) )
& ( ? [X25] :
( sP80(X25)
& sP79(X25)
& ~ p1(X25)
& ~ p2(X25)
& ~ p3(X25)
& r1(X0,X25) )
| ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] : ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X21,X22) )
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21) )
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(X0,X20) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X14] :
( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP82(X17)
| sP83(X17)
| ~ r1(X14,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
& ~ p2(X14) )
| sP84(X14) )
& r1(X0,X14) )
| sP86(X0) )
& ! [X11] :
( ? [X12] :
( p1(X12)
& ? [X13] :
( ~ p1(X13)
& r1(X12,X13) )
& r1(X11,X12) )
| p1(X11)
| ~ r1(X0,X11) )
& ? [X10] :
( ~ p1(X10)
& r1(X0,X10) )
& ( sP87(X0)
| ! [X8] :
( ? [X9] :
( p5(X9)
& r1(X8,X9) )
| ~ r1(X0,X8) ) )
& ! [X5] :
( ? [X6] :
( p3(X6)
& ? [X7] :
( ~ p3(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p3(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p3(X4)
& r1(X0,X4) )
& ( sP88(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p5(X3)
| ~ r1(X2,X3) )
& r1(X1,X2) )
& ~ p1(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f101]) ).
fof(f363,plain,
( ! [X106] :
( ( ! [X108] :
( ~ p2(X108)
| ! [X109] :
( p2(X109)
| ~ r1(X108,X109) )
| ~ r1(sK253(X106),X108) )
& ~ p2(sK253(X106))
& r1(X106,sK253(X106)) )
| p2(X106)
| ~ r1(sK217,X106) )
& ( ( ! [X102] :
( ( r1(X102,sK252(X102))
& ~ p1(X102) )
| ! [X103] :
( ! [X104] : ~ r1(X103,X104)
| p1(X103)
| ~ r1(X102,X103) )
| ~ r1(sK250,X102) )
& r1(sK250,sK251)
& ~ p1(sK250)
& r1(sK217,sK250) )
| ! [X99] : ~ r1(sK217,X99)
| p1(sK217) )
& ( ( ! [X95] :
( ( r1(X95,sK249(X95))
& ~ p1(X95)
& ~ p2(X95) )
| ! [X96] :
( ! [X97] : ~ r1(X96,X97)
| p1(X96)
| p2(X96)
| ~ r1(X95,X96) )
| ~ r1(sK247,X95) )
& r1(sK247,sK248)
& ~ p1(sK247)
& ~ p2(sK247)
& r1(sK217,sK247) )
| ! [X92] : ~ r1(sK217,X92)
| p1(sK217)
| p2(sK217) )
& ( ( sP0(sK245)
& r1(sK245,sK246)
& ~ p1(sK245)
& ~ p2(sK245)
& ~ p3(sK245)
& r1(sK217,sK245) )
| ! [X89] : ~ r1(sK217,X89)
| p1(sK217)
| p2(sK217)
| p3(sK217) )
& ( ( sP1(sK243)
& r1(sK243,sK244)
& ~ p1(sK243)
& ~ p2(sK243)
& ~ p3(sK243)
& ~ p4(sK243)
& r1(sK217,sK243) )
| ! [X86] : ~ r1(sK217,X86)
| p1(sK217)
| p2(sK217)
| p3(sK217)
| p4(sK217) )
& ( ( sP2(sK242)
& sP3(sK242)
& ~ p1(sK242)
& r1(sK217,sK242) )
| ! [X83] :
( ! [X84] : ~ r1(X83,X84)
| p1(X83)
| p2(X83)
| p3(X83)
| p4(X83)
| ~ r1(sK217,X83) )
| p1(sK217) )
& ( ( sP4(sK241)
& sP5(sK241)
& ~ p1(sK241)
& ~ p2(sK241)
& r1(sK217,sK241) )
| ! [X80] :
( ! [X81] : ~ r1(X80,X81)
| p1(X80)
| p2(X80)
| p3(X80)
| p4(X80)
| ~ r1(sK217,X80) )
| p1(sK217)
| p2(sK217) )
& ( ( sP8(sK240)
& sP7(sK240)
& ~ p1(sK240)
& ~ p2(sK240)
& ~ p3(sK240)
& r1(sK217,sK240) )
| ! [X77] :
( ! [X78] : ~ r1(X77,X78)
| p1(X77)
| p2(X77)
| p3(X77)
| p4(X77)
| ~ r1(sK217,X77) )
| p1(sK217)
| p2(sK217)
| p3(sK217) )
& ( ( sP11(sK239)
& sP10(sK239)
& ~ p1(sK239)
& ~ p2(sK239)
& ~ p3(sK239)
& ~ p4(sK239)
& r1(sK217,sK239) )
| ! [X74] :
( ! [X75] : ~ r1(X74,X75)
| p1(X74)
| p2(X74)
| p3(X74)
| p4(X74)
| ~ r1(sK217,X74) )
| p1(sK217)
| p2(sK217)
| p3(sK217)
| p4(sK217) )
& ( ( sP14(sK238)
& sP15(sK238)
& ~ p1(sK238)
& r1(sK217,sK238) )
| ! [X70] :
( ! [X71] :
( ! [X72] : ~ r1(X71,X72)
| p1(X71)
| p2(X71)
| p3(X71)
| p4(X71)
| ~ r1(X70,X71) )
| p1(X70)
| p2(X70)
| p3(X70)
| p4(X70)
| ~ r1(sK217,X70) )
| p1(sK217) )
& ( ( sP18(sK237)
& sP19(sK237)
& ~ p1(sK237)
& ~ p2(sK237)
& r1(sK217,sK237) )
| ! [X66] :
( ! [X67] :
( ! [X68] : ~ r1(X67,X68)
| p1(X67)
| p2(X67)
| p3(X67)
| p4(X67)
| ~ r1(X66,X67) )
| p1(X66)
| p2(X66)
| p3(X66)
| p4(X66)
| ~ r1(sK217,X66) )
| p1(sK217)
| p2(sK217) )
& ( ( sP24(sK236)
& sP23(sK236)
& ~ p1(sK236)
& ~ p2(sK236)
& ~ p3(sK236)
& r1(sK217,sK236) )
| ! [X62] :
( ! [X63] :
( ! [X64] : ~ r1(X63,X64)
| p1(X63)
| p2(X63)
| p3(X63)
| p4(X63)
| ~ r1(X62,X63) )
| p1(X62)
| p2(X62)
| p3(X62)
| p4(X62)
| ~ r1(sK217,X62) )
| p1(sK217)
| p2(sK217)
| p3(sK217) )
& ( ( sP29(sK235)
& sP28(sK235)
& ~ p1(sK235)
& ~ p2(sK235)
& ~ p3(sK235)
& ~ p4(sK235)
& r1(sK217,sK235) )
| ! [X58] :
( ! [X59] :
( ! [X60] : ~ r1(X59,X60)
| p1(X59)
| p2(X59)
| p3(X59)
| p4(X59)
| ~ r1(X58,X59) )
| p1(X58)
| p2(X58)
| p3(X58)
| p4(X58)
| ~ r1(sK217,X58) )
| p1(sK217)
| p2(sK217)
| p3(sK217)
| p4(sK217) )
& ( ( sP34(sK234)
& sP35(sK234)
& ~ p1(sK234)
& r1(sK217,sK234) )
| ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] : ~ r1(X55,X56)
| p1(X55)
| p2(X55)
| p3(X55)
| p4(X55)
| ~ r1(X54,X55) )
| p1(X54)
| p2(X54)
| p3(X54)
| p4(X54)
| ~ r1(X53,X54) )
| p1(X53)
| p2(X53)
| p3(X53)
| p4(X53)
| ~ r1(sK217,X53) )
| p1(sK217) )
& ( ( sP40(sK233)
& sP41(sK233)
& ~ p1(sK233)
& ~ p2(sK233)
& r1(sK217,sK233) )
| ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] : ~ r1(X50,X51)
| p1(X50)
| p2(X50)
| p3(X50)
| p4(X50)
| ~ r1(X49,X50) )
| p1(X49)
| p2(X49)
| p3(X49)
| p4(X49)
| ~ r1(X48,X49) )
| p1(X48)
| p2(X48)
| p3(X48)
| p4(X48)
| ~ r1(sK217,X48) )
| p1(sK217)
| p2(sK217) )
& ( ( sP48(sK232)
& sP47(sK232)
& ~ p1(sK232)
& ~ p2(sK232)
& ~ p3(sK232)
& r1(sK217,sK232) )
| ! [X43] :
( ! [X44] :
( ! [X45] :
( ! [X46] : ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(X44,X45) )
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(X43,X44) )
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43)
| ~ r1(sK217,X43) )
| p1(sK217)
| p2(sK217)
| p3(sK217) )
& ( ( sP55(sK231)
& sP54(sK231)
& ~ p1(sK231)
& ~ p2(sK231)
& ~ p3(sK231)
& ~ p4(sK231)
& r1(sK217,sK231) )
| ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] : ~ r1(X40,X41)
| p1(X40)
| p2(X40)
| p3(X40)
| p4(X40)
| ~ r1(X39,X40) )
| p1(X39)
| p2(X39)
| p3(X39)
| p4(X39)
| ~ r1(X38,X39) )
| p1(X38)
| p2(X38)
| p3(X38)
| p4(X38)
| ~ r1(sK217,X38) )
| p1(sK217)
| p2(sK217)
| p3(sK217)
| p4(sK217) )
& ( ( sP62(sK230)
& sP63(sK230)
& ~ p1(sK230)
& r1(sK217,sK230) )
| ! [X32] :
( ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] : ~ r1(X35,X36)
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X34,X35) )
| p1(X34)
| p2(X34)
| p3(X34)
| p4(X34)
| ~ r1(X33,X34) )
| p1(X33)
| p2(X33)
| p3(X33)
| p4(X33)
| ~ r1(X32,X33) )
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(sK217,X32) )
| p1(sK217) )
& ( ( sP70(sK229)
& sP71(sK229)
& ~ p1(sK229)
& ~ p2(sK229)
& r1(sK217,sK229) )
| ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29) )
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(X27,X28) )
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(X26,X27) )
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(sK217,X26) )
| p1(sK217)
| p2(sK217) )
& ( ( sP80(sK228)
& sP79(sK228)
& ~ p1(sK228)
& ~ p2(sK228)
& ~ p3(sK228)
& r1(sK217,sK228) )
| ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] : ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X21,X22) )
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21) )
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(sK217,X20) )
| p1(sK217)
| p2(sK217)
| p3(sK217) )
& ( ( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP82(X17)
| sP83(X17)
| ~ r1(sK227,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(sK227,X15) )
& ~ p2(sK227) )
| sP84(sK227) )
& r1(sK217,sK227) )
| sP86(sK217) )
& ! [X11] :
( ( p1(sK225(X11))
& ~ p1(sK226(X11))
& r1(sK225(X11),sK226(X11))
& r1(X11,sK225(X11)) )
| p1(X11)
| ~ r1(sK217,X11) )
& ~ p1(sK224)
& r1(sK217,sK224)
& ( sP87(sK217)
| ! [X8] :
( ( p5(sK223(X8))
& r1(X8,sK223(X8)) )
| ~ r1(sK217,X8) ) )
& ! [X5] :
( ( p3(sK221(X5))
& ~ p3(sK222(X5))
& r1(sK221(X5),sK222(X5))
& r1(X5,sK221(X5)) )
| p3(X5)
| ~ r1(sK217,X5) )
& ~ p3(sK220)
& r1(sK217,sK220)
& ( sP88(sK217)
| ( ! [X3] :
( ~ p5(X3)
| ~ r1(sK219,X3) )
& r1(sK218,sK219)
& ~ p1(sK218)
& r1(sK217,sK218) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK217,sK218,sK219,sK220,sK221,sK222,sK223,sK224,sK225,sK226,sK227,sK228,sK229,sK230,sK231,sK232,sK233,sK234,sK235,sK236,sK237,sK238,sK239,sK240,sK241,sK242,sK243,sK244,sK245,sK246,sK247,sK248,sK249,sK250,sK251,sK252,sK253]),skolemize(X0,sK217),skolemize(X1,sK218),skolemize(X2,sK219),skolemize(X4,sK220),skolemize(X6,sK221(X5)),skolemize(X7,sK222(X5)),skolemize(X9,sK223(X8)),skolemize(X10,sK224),skolemize(X12,sK225(X11)),skolemize(X13,sK226(X11)),skolemize(X14,sK227),skolemize(X25,sK228),skolemize(X31,sK229),skolemize(X37,sK230),skolemize(X42,sK231),skolemize(X47,sK232),skolemize(X52,sK233),skolemize(X57,sK234),skolemize(X61,sK235),skolemize(X65,sK236),skolemize(X69,sK237),skolemize(X73,sK238),skolemize(X76,sK239),skolemize(X79,sK240),skolemize(X82,sK241),skolemize(X85,sK242),skolemize(X87,sK243),skolemize(X88,sK244),skolemize(X90,sK245),skolemize(X91,sK246),skolemize(X93,sK247),skolemize(X94,sK248),skolemize(X98,sK249(X95)),skolemize(X100,sK250),skolemize(X101,sK251),skolemize(X105,sK252(X102)),skolemize(X107,sK253(X106))],[f362]) ).
fof(f365,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f366,plain,
! [X2,X0] :
( ~ sP88(X0)
| p2(sK90(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f104]) ).
fof(f367,plain,
! [X2,X0] :
( ~ sP88(X0)
| ~ p2(sK91(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f104]) ).
fof(f368,plain,
! [X2,X0] :
( ~ sP88(X0)
| r1(sK90(X2),sK91(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f104]) ).
fof(f369,plain,
! [X2,X0] :
( ~ sP88(X0)
| r1(X2,sK90(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f104]) ).
fof(f370,plain,
! [X0] :
( ~ sP88(X0)
| ~ p2(sK89(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f371,plain,
! [X0] :
( ~ sP88(X0)
| r1(X0,sK89(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f372,plain,
! [X2,X0] :
( ~ sP87(X0)
| p2(sK93(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f373,plain,
! [X2,X0] :
( ~ sP87(X0)
| ~ p2(sK94(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f374,plain,
! [X2,X0] :
( ~ sP87(X0)
| r1(sK93(X2),sK94(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f375,plain,
! [X2,X0] :
( ~ sP87(X0)
| r1(X2,sK93(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f376,plain,
! [X0] :
( ~ sP87(X0)
| ~ p2(sK92(X0)) ),
inference(cnf_transformation,[],[f107]) ).
fof(f377,plain,
! [X0] :
( ~ sP87(X0)
| r1(X0,sK92(X0)) ),
inference(cnf_transformation,[],[f107]) ).
fof(f900,plain,
! [X108,X109,X106] :
( ~ p2(X108)
| p2(X109)
| ~ r1(X108,X109)
| ~ r1(sK253(X106),X108)
| p2(X106)
| ~ r1(sK217,X106) ),
inference(cnf_transformation,[],[f363]) ).
fof(f901,plain,
! [X106] :
( ~ p2(sK253(X106))
| p2(X106)
| ~ r1(sK217,X106) ),
inference(cnf_transformation,[],[f363]) ).
fof(f902,plain,
! [X106] :
( r1(X106,sK253(X106))
| p2(X106)
| ~ r1(sK217,X106) ),
inference(cnf_transformation,[],[f363]) ).
fof(f1020,plain,
! [X8] :
( sP87(sK217)
| p5(sK223(X8))
| ~ r1(sK217,X8) ),
inference(cnf_transformation,[],[f363]) ).
fof(f1021,plain,
! [X8] :
( sP87(sK217)
| r1(X8,sK223(X8))
| ~ r1(sK217,X8) ),
inference(cnf_transformation,[],[f363]) ).
fof(f1027,plain,
r1(sK217,sK220),
inference(cnf_transformation,[],[f363]) ).
fof(f1028,plain,
! [X3] :
( sP88(sK217)
| ~ p5(X3)
| ~ r1(sK219,X3) ),
inference(cnf_transformation,[],[f363]) ).
fof(f1029,plain,
( sP88(sK217)
| r1(sK218,sK219) ),
inference(cnf_transformation,[],[f363]) ).
fof(f1031,plain,
( sP88(sK217)
| r1(sK217,sK218) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f365]) ).
tcf(c_51,plain,
! [X0: $i] :
( r1(X0,sK89(X0))
| ~ sP88(X0) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ sP88(X0)
| ~ p2(sK89(X0)) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK90(X1))
| ~ sP88(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK90(X1),sK91(X1))
| ~ sP88(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f368]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP88(X0)
| ~ p2(sK91(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK90(X1))
| ~ sP88(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f366]) ).
tcf(c_57,plain,
! [X0: $i] :
( r1(X0,sK92(X0))
| ~ sP87(X0) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_58,plain,
! [X0: $i] :
( ~ sP87(X0)
| ~ p2(sK92(X0)) ),
inference(cnf_transformation,[],[f376]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK93(X1))
| ~ sP87(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK93(X1),sK94(X1))
| ~ sP87(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP87(X0)
| ~ p2(sK94(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f373]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK93(X1))
| ~ sP87(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_585,negated_conjecture,
( sP88(sK217)
| r1(sK217,sK218) ),
inference(cnf_transformation,[],[f1031]) ).
tcf(c_587,negated_conjecture,
( sP88(sK217)
| r1(sK218,sK219) ),
inference(cnf_transformation,[],[f1029]) ).
tcf(c_588,negated_conjecture,
! [X0: $i] :
( sP88(sK217)
| ~ p5(X0)
| ~ r1(sK219,X0) ),
inference(cnf_transformation,[],[f1028]) ).
tcf(c_589,negated_conjecture,
r1(sK217,sK220),
inference(cnf_transformation,[],[f1027]) ).
tcf(c_595,negated_conjecture,
! [X0: $i] :
( sP87(sK217)
| r1(X0,sK223(X0))
| ~ r1(sK217,X0) ),
inference(cnf_transformation,[],[f1021]) ).
tcf(c_596,negated_conjecture,
! [X0: $i] :
( sP87(sK217)
| p5(sK223(X0))
| ~ r1(sK217,X0) ),
inference(cnf_transformation,[],[f1020]) ).
tcf(c_714,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK253(X0))
| ~ r1(sK217,X0) ),
inference(cnf_transformation,[],[f902]) ).
tcf(c_715,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK253(X0))
| ~ r1(sK217,X0) ),
inference(cnf_transformation,[],[f901]) ).
tcf(c_716,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK217,X0)
| ~ r1(X1,X2)
| ~ r1(sK253(X0),X1) ),
inference(cnf_transformation,[],[f900]) ).
tcf(c_1078,plain,
( ~ sP87(sK217)
| ~ p2(sK92(sK217)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_1079,plain,
( r1(sK217,sK92(sK217))
| ~ sP87(sK217) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_1080,plain,
( ~ sP88(sK217)
| ~ p2(sK89(sK217)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_1081,plain,
( r1(sK217,sK89(sK217))
| ~ sP88(sK217) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_9590,plain,
! [X0: $i] :
( sP87(sK217)
| sP88(sK217)
| ~ r1(sK217,X0)
| ~ r1(sK219,sK223(X0)) ),
inference(resolution,[status(thm)],[c_588,c_596]) ).
tcf(c_13342,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ r1(sK217,X0)
| ~ r1(sK219,sK223(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_9590]) ).
tcf(c_13343,plain,
( iPr_def_10
| sP87(sK217)
| sP88(sK217) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_9590]) ).
tcf(c_13367,plain,
! [X0: $i] :
( p2(sK92(X0))
| r1(sK92(X0),sK253(sK92(X0)))
| ~ r1(sK217,sK92(X0)) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_13370,plain,
( p2(sK92(sK217))
| r1(sK92(sK217),sK253(sK92(sK217)))
| ~ r1(sK217,sK92(sK217)) ),
inference(instantiation,[status(thm)],[c_13367]) ).
tcf(c_13387,plain,
! [X0: $i] :
( p2(sK89(X0))
| r1(sK89(X0),sK253(sK89(X0)))
| ~ r1(sK217,sK89(X0)) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_13390,plain,
( p2(sK89(sK217))
| r1(sK89(sK217),sK253(sK89(sK217)))
| ~ r1(sK217,sK89(sK217)) ),
inference(instantiation,[status(thm)],[c_13387]) ).
tcf(c_13399,plain,
( ~ iPr_def_10
| ~ r1(sK217,sK219)
| ~ r1(sK219,sK223(sK219)) ),
inference(instantiation,[status(thm)],[c_13342]) ).
tcf(c_13406,plain,
! [X0: $i] :
( r1(sK217,sK219)
| ~ r1(sK217,X0)
| ~ r1(X0,sK219) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_13428,plain,
( sP87(sK217)
| r1(sK219,sK223(sK219))
| ~ r1(sK217,sK219) ),
inference(instantiation,[status(thm)],[c_595]) ).
tcf(c_13431,plain,
( r1(sK217,sK219)
| ~ r1(sK218,sK219)
| ~ r1(sK217,sK218) ),
inference(instantiation,[status(thm)],[c_13406]) ).
tcf(c_13473,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK92(X1)))
| r1(sK93(sK253(sK92(X1))),sK94(sK253(sK92(X1))))
| ~ sP87(X0)
| ~ r1(X0,sK253(sK92(X1))) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_13474,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK92(X1)))
| r1(sK253(sK92(X1)),sK93(sK253(sK92(X1))))
| ~ sP87(X0)
| ~ r1(X0,sK253(sK92(X1))) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_13475,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK92(X1)))
| p2(sK93(sK253(sK92(X1))))
| ~ sP87(X0)
| ~ r1(X0,sK253(sK92(X1))) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_13476,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK92(X1)))
| ~ sP87(X0)
| ~ p2(sK94(sK253(sK92(X1))))
| ~ r1(X0,sK253(sK92(X1))) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_13479,plain,
( p2(sK253(sK92(sK217)))
| ~ sP87(sK217)
| ~ p2(sK94(sK253(sK92(sK217))))
| ~ r1(sK217,sK253(sK92(sK217))) ),
inference(instantiation,[status(thm)],[c_13476]) ).
tcf(c_13480,plain,
( p2(sK253(sK92(sK217)))
| p2(sK93(sK253(sK92(sK217))))
| ~ sP87(sK217)
| ~ r1(sK217,sK253(sK92(sK217))) ),
inference(instantiation,[status(thm)],[c_13475]) ).
tcf(c_13481,plain,
( p2(sK253(sK92(sK217)))
| r1(sK253(sK92(sK217)),sK93(sK253(sK92(sK217))))
| ~ sP87(sK217)
| ~ r1(sK217,sK253(sK92(sK217))) ),
inference(instantiation,[status(thm)],[c_13474]) ).
tcf(c_13482,plain,
( p2(sK253(sK92(sK217)))
| r1(sK93(sK253(sK92(sK217))),sK94(sK253(sK92(sK217))))
| ~ sP87(sK217)
| ~ r1(sK217,sK253(sK92(sK217))) ),
inference(instantiation,[status(thm)],[c_13473]) ).
tcf(c_13685,plain,
! [X0: $i,X1: $i] :
( r1(sK217,sK253(sK92(X1)))
| ~ r1(sK217,X0)
| ~ r1(X0,sK253(sK92(X1))) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_13942,plain,
! [X0: $i] :
( r1(sK217,sK253(sK92(X0)))
| ~ r1(sK217,sK92(X0))
| ~ r1(sK92(X0),sK253(sK92(X0))) ),
inference(instantiation,[status(thm)],[c_13685]) ).
tcf(c_13943,plain,
( r1(sK217,sK253(sK92(sK217)))
| ~ r1(sK217,sK92(sK217))
| ~ r1(sK92(sK217),sK253(sK92(sK217))) ),
inference(instantiation,[status(thm)],[c_13942]) ).
tcf(c_14014,plain,
( sP88(sK217)
| sP87(sK217) ),
inference(global_subsumption_just,[status(thm)],[c_13343,c_587,c_585,c_13343,c_13399,c_13428,c_13431]) ).
tcf(c_14015,plain,
( sP87(sK217)
| sP88(sK217) ),
inference(renaming,[status(thm)],[c_14014]) ).
tcf(c_14230,plain,
( p2(sK89(sK217))
| ~ sP88(sK217)
| ~ p2(sK253(sK89(sK217))) ),
inference(superposition,[status(thm)],[c_51,c_715]) ).
tcf(c_14231,plain,
( p2(sK92(sK217))
| ~ sP87(sK217)
| ~ p2(sK253(sK92(sK217))) ),
inference(superposition,[status(thm)],[c_57,c_715]) ).
tcf(c_15758,plain,
( p2(sK220)
| p2(sK93(sK220))
| ~ sP87(sK217) ),
inference(resolution,[status(thm)],[c_62,c_589]) ).
tcf(c_16187,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK94(sK253(sK92(X1))))
| ~ p2(X0)
| ~ r1(sK217,X2)
| ~ r1(sK253(X2),X0)
| ~ r1(X0,sK94(sK253(sK92(X1)))) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_16411,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK94(sK253(sK92(X0))))
| ~ r1(sK217,X1)
| ~ p2(sK93(sK253(sK92(X0))))
| ~ r1(sK253(X1),sK93(sK253(sK92(X0))))
| ~ r1(sK93(sK253(sK92(X0))),sK94(sK253(sK92(X0)))) ),
inference(instantiation,[status(thm)],[c_16187]) ).
tcf(c_18143,plain,
! [X0: $i] :
( p2(sK92(X0))
| p2(sK94(sK253(sK92(X0))))
| ~ r1(sK217,sK92(X0))
| ~ p2(sK93(sK253(sK92(X0))))
| ~ r1(sK253(sK92(X0)),sK93(sK253(sK92(X0))))
| ~ r1(sK93(sK253(sK92(X0))),sK94(sK253(sK92(X0)))) ),
inference(instantiation,[status(thm)],[c_16411]) ).
tcf(c_18144,plain,
( p2(sK92(sK217))
| p2(sK94(sK253(sK92(sK217))))
| ~ r1(sK217,sK92(sK217))
| ~ p2(sK93(sK253(sK92(sK217))))
| ~ r1(sK253(sK92(sK217)),sK93(sK253(sK92(sK217))))
| ~ r1(sK93(sK253(sK92(sK217))),sK94(sK253(sK92(sK217)))) ),
inference(instantiation,[status(thm)],[c_18143]) ).
tcf(c_18254,plain,
~ sP87(sK217),
inference(global_subsumption_just,[status(thm)],[c_15758,c_1078,c_1079,c_13370,c_13479,c_13480,c_13481,c_13482,c_13943,c_14231,c_18144]) ).
tcf(c_19654,plain,
! [X0: $i,X1: $i] :
( r1(sK217,sK253(X1))
| ~ r1(sK217,X0)
| ~ r1(X0,sK253(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_19660,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK89(X1)))
| r1(sK90(sK253(sK89(X1))),sK91(sK253(sK89(X1))))
| ~ sP88(X0)
| ~ r1(X0,sK253(sK89(X1))) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_19661,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK89(X1)))
| r1(sK253(sK89(X1)),sK90(sK253(sK89(X1))))
| ~ sP88(X0)
| ~ r1(X0,sK253(sK89(X1))) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_19662,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK89(X1)))
| p2(sK90(sK253(sK89(X1))))
| ~ sP88(X0)
| ~ r1(X0,sK253(sK89(X1))) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_19663,plain,
! [X0: $i,X1: $i] :
( p2(sK253(sK89(X1)))
| ~ sP88(X0)
| ~ p2(sK91(sK253(sK89(X1))))
| ~ r1(X0,sK253(sK89(X1))) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_19678,plain,
( p2(sK253(sK89(sK217)))
| ~ sP88(sK217)
| ~ p2(sK91(sK253(sK89(sK217))))
| ~ r1(sK217,sK253(sK89(sK217))) ),
inference(instantiation,[status(thm)],[c_19663]) ).
tcf(c_19679,plain,
( p2(sK253(sK89(sK217)))
| p2(sK90(sK253(sK89(sK217))))
| ~ sP88(sK217)
| ~ r1(sK217,sK253(sK89(sK217))) ),
inference(instantiation,[status(thm)],[c_19662]) ).
tcf(c_19680,plain,
( p2(sK253(sK89(sK217)))
| r1(sK253(sK89(sK217)),sK90(sK253(sK89(sK217))))
| ~ sP88(sK217)
| ~ r1(sK217,sK253(sK89(sK217))) ),
inference(instantiation,[status(thm)],[c_19661]) ).
tcf(c_19681,plain,
( p2(sK253(sK89(sK217)))
| r1(sK90(sK253(sK89(sK217))),sK91(sK253(sK89(sK217))))
| ~ sP88(sK217)
| ~ r1(sK217,sK253(sK89(sK217))) ),
inference(instantiation,[status(thm)],[c_19660]) ).
tcf(c_26740,plain,
! [X0: $i] :
( r1(sK217,sK253(sK89(X0)))
| ~ r1(sK217,sK89(X0))
| ~ r1(sK89(X0),sK253(sK89(X0))) ),
inference(instantiation,[status(thm)],[c_19654]) ).
tcf(c_26741,plain,
( r1(sK217,sK253(sK89(sK217)))
| ~ r1(sK217,sK89(sK217))
| ~ r1(sK89(sK217),sK253(sK89(sK217))) ),
inference(instantiation,[status(thm)],[c_26740]) ).
tcf(c_32418,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK91(sK253(sK89(X1))))
| ~ p2(X0)
| ~ r1(sK217,X2)
| ~ r1(sK253(X2),X0)
| ~ r1(X0,sK91(sK253(sK89(X1)))) ),
inference(instantiation,[status(thm)],[c_716]) ).
tcf(c_32639,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK91(sK253(sK89(X0))))
| ~ r1(sK217,X1)
| ~ p2(sK90(sK253(sK89(X0))))
| ~ r1(sK253(X1),sK90(sK253(sK89(X0))))
| ~ r1(sK90(sK253(sK89(X0))),sK91(sK253(sK89(X0)))) ),
inference(instantiation,[status(thm)],[c_32418]) ).
tcf(c_33241,plain,
! [X0: $i] :
( p2(sK89(X0))
| p2(sK91(sK253(sK89(X0))))
| ~ r1(sK217,sK89(X0))
| ~ p2(sK90(sK253(sK89(X0))))
| ~ r1(sK253(sK89(X0)),sK90(sK253(sK89(X0))))
| ~ r1(sK90(sK253(sK89(X0))),sK91(sK253(sK89(X0)))) ),
inference(instantiation,[status(thm)],[c_32639]) ).
tcf(c_33242,plain,
( p2(sK89(sK217))
| p2(sK91(sK253(sK89(sK217))))
| ~ r1(sK217,sK89(sK217))
| ~ p2(sK90(sK253(sK89(sK217))))
| ~ r1(sK253(sK89(sK217)),sK90(sK253(sK89(sK217))))
| ~ r1(sK90(sK253(sK89(sK217))),sK91(sK253(sK89(sK217)))) ),
inference(instantiation,[status(thm)],[c_33241]) ).
tcf(c_33243,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_33242,c_26741,c_19681,c_19680,c_19679,c_19678,c_18254,c_14230,c_14015,c_13390,c_1081,c_1080]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL676+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.33 % Computer : n003.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Thu Sep 24 00:16:20 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.37 Running first-order theorem proving
% 0.13/0.37 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.38
% 0.13/0.38 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.38
% 0.13/0.38 % Detected problem language: tptp
% 0.13/0.39 % Proving...
% 40.89/7.32 % SZS status Started for theBenchmark.p
% 40.89/7.32 % SZS status Theorem for theBenchmark.p
% 40.89/7.32
% 40.89/7.32 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 40.89/7.32
% 40.89/7.32 % ------ iProver source info
% 40.89/7.32
% 40.89/7.32 % git: date: 2026-07-19 20:42:38 +0200
% 40.89/7.32 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 40.89/7.32 % git: non_committed_changes: false
% 40.89/7.32
% 40.89/7.32 % ------ Parsing...
% 40.89/7.32 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 40.89/7.32
% 40.89/7.32 % ------ Preprocessing... sf_s rm: 590 0s sf_e pe_s pe:1:0s pe_e %
% 40.89/7.32
% 40.89/7.32 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e
% 40.89/7.32 % ------ Proving...
% 40.89/7.32 % ------ Problem Properties
% 40.89/7.32
% 40.89/7.32 %
% 40.89/7.32 % clauses 79
% 40.89/7.32 % conjectures 25
% 40.89/7.32 % EPR 18
% 40.89/7.32 % Horn 34
% 40.89/7.32 % unary 5
% 40.89/7.32 % binary 14
% 40.89/7.32 % lits 275
% 40.89/7.32 % lits eq 0
% 40.89/7.32 % fd_pure 0
% 40.89/7.32 % fd_pseudo 0
% 40.89/7.32 % fd_cond 0
% 40.89/7.32 % fd_pseudo_cond 0
% 40.89/7.32 % AC symbols 0
% 40.89/7.32
% 40.89/7.32 % ------ Input Options Time Limit: Unbounded
% 40.89/7.32
% 40.89/7.32
% 40.89/7.32 % ------
% 40.89/7.32 % Current options:
% 40.89/7.32 % ------
% 40.89/7.32
% 40.89/7.32
% 40.89/7.32 %
% 40.89/7.32
% 40.89/7.32 % ------ Proving...
% 40.89/7.32 %
% 40.89/7.32
% 40.89/7.32 % SZS status Theorem for theBenchmark.p
% 40.89/7.32
% 40.89/7.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 40.89/7.33
% 40.89/7.33
%------------------------------------------------------------------------------