%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL660+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 : 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 : Fri Sep 25 02:07:48 PM UTC 2026
% Result : Theorem 20.13s 14.25s
% Output : CNFRefutation 20.13s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f95ERROR: Could not build tree for root c_45452ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f98,plain,
! [X0] :
( ~ sP87(X0)
| ( ! [X13] :
( ? [X14] :
( p2(X14)
& ? [X15] :
( ~ p2(X15)
& r1(X14,X15) )
& r1(X13,X14) )
| p2(X13)
| ~ r1(X0,X13) )
& ? [X12] :
( ~ p2(X12)
& r1(X0,X12) ) ) ),
inference(nnf_transformation,[],[f96]) ).
fof(f99,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,[],[f98]) ).
fof(f100,plain,
! [X0] :
( ~ sP87(X0)
| ( ! [X2] :
( ( p2(sK89(X2))
& ~ p2(sK90(X2))
& r1(sK89(X2),sK90(X2))
& r1(X2,sK89(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK88(X0))
& r1(X0,sK88(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK88,sK89,sK90]),skolemize(X1,sK88(X0)),skolemize(X3,sK89(X2)),skolemize(X4,sK90(X2))],[f99]) ).
fof(f101,plain,
! [X0] :
( ~ sP86(X0)
| ( ( ? [X27] :
( p2(X27)
& ? [X28] :
( ~ p2(X28)
& r1(X27,X28) )
& r1(X0,X27) )
| p2(X0) )
& ( ? [X24] :
( ! [X25] :
( ~ p2(X25)
| ! [X26] :
( p2(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
& ~ p2(X24)
& r1(X0,X24) )
| sP85(X0) ) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f102,plain,
! [X0] :
( ~ sP86(X0)
| ( ( ? [X4] :
( p2(X4)
& ? [X5] :
( ~ p2(X5)
& r1(X4,X5) )
& r1(X0,X4) )
| p2(X0) )
& ( ? [X1] :
( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
& ~ p2(X1)
& r1(X0,X1) )
| sP85(X0) ) ) ),
inference(rectify,[],[f101]) ).
fof(f103,plain,
! [X0] :
( ~ sP86(X0)
| ( ( ( p2(sK92(X0))
& ~ p2(sK93(X0))
& r1(sK92(X0),sK93(X0))
& r1(X0,sK92(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK91(X0),X2) )
& ~ p2(sK91(X0))
& r1(X0,sK91(X0)) )
| sP85(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91,sK92,sK93]),skolemize(X1,sK91(X0)),skolemize(X4,sK92(X0)),skolemize(X5,sK93(X0))],[f102]) ).
fof(f104,plain,
! [X0] :
( ~ sP85(X0)
| ! [X20] :
( ! [X21] :
( ? [X22] :
( p2(X22)
& ? [X23] :
( ~ p2(X23)
& r1(X22,X23) )
& r1(X21,X22) )
| p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X0,X20) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f105,plain,
! [X0] :
( ~ sP85(X0)
| ! [X1] :
( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] :
( ~ p2(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f104]) ).
fof(f106,plain,
! [X0] :
( ~ sP85(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK94(X2))
& ~ p2(sK95(X2))
& r1(sK94(X2),sK95(X2))
& r1(X2,sK94(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94,sK95]),skolemize(X3,sK94(X2)),skolemize(X4,sK95(X2))],[f105]) ).
fof(f107,plain,
! [X29] :
( ~ sP84(X29)
| ( ! [X34] :
( ? [X35] :
( p2(X35)
& ? [X36] :
( ~ p2(X36)
& r1(X35,X36) )
& r1(X34,X35) )
| p2(X34)
| ~ r1(X29,X34) )
& ? [X30] :
( ? [X31] :
( ! [X32] :
( ~ p2(X32)
| ! [X33] :
( p2(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
& ~ p2(X31)
& r1(X30,X31) )
& r1(X29,X30) ) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f108,plain,
! [X0] :
( ~ sP84(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
& ~ p2(X2)
& r1(X1,X2) )
& r1(X0,X1) ) ) ),
inference(rectify,[],[f107]) ).
fof(f109,plain,
! [X0] :
( ~ sP84(X0)
| ( ! [X5] :
( ( p2(sK98(X5))
& ~ p2(sK99(X5))
& r1(sK98(X5),sK99(X5))
& r1(X5,sK98(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK97(X0),X3) )
& ~ p2(sK97(X0))
& r1(sK96(X0),sK97(X0))
& r1(X0,sK96(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96,sK97,sK98,sK99]),skolemize(X1,sK96(X0)),skolemize(X2,sK97(X0)),skolemize(X6,sK98(X5)),skolemize(X7,sK99(X5))],[f108]) ).
fof(f110,plain,
! [X39] :
( ~ sP83(X39)
| ! [X40] :
( ( ( ? [X48] :
( p2(X48)
& ? [X49] :
( ~ p2(X49)
& r1(X48,X49) )
& r1(X40,X48) )
| p2(X40) )
& ( ? [X45] :
( ! [X46] :
( ~ p2(X46)
| ! [X47] :
( p2(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p2(X45)
& r1(X40,X45) )
| sP81(X40) ) )
| ~ r1(X39,X40) ) ),
inference(nnf_transformation,[],[f92]) ).
fof(f111,plain,
! [X0] :
( ~ sP83(X0)
| ! [X1] :
( ( ( ? [X5] :
( p2(X5)
& ? [X6] :
( ~ p2(X6)
& r1(X5,X6) )
& r1(X1,X5) )
| p2(X1) )
& ( ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
& ~ p2(X2)
& r1(X1,X2) )
| sP81(X1) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f110]) ).
fof(f112,plain,
! [X0] :
( ~ sP83(X0)
| ! [X1] :
( ( ( ( p2(sK101(X1))
& ~ p2(sK102(X1))
& r1(sK101(X1),sK102(X1))
& r1(X1,sK101(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK100(X1),X3) )
& ~ p2(sK100(X1))
& r1(X1,sK100(X1)) )
| sP81(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK100,sK101,sK102]),skolemize(X2,sK100(X1)),skolemize(X5,sK101(X1)),skolemize(X6,sK102(X1))],[f111]) ).
fof(f113,plain,
! [X39] :
( ~ sP82(X39)
| ( ! [X54] :
( ? [X55] :
( p2(X55)
& ? [X56] :
( ~ p2(X56)
& r1(X55,X56) )
& r1(X54,X55) )
| p2(X54)
| ~ r1(X39,X54) )
& ? [X50] :
( ? [X51] :
( ! [X52] :
( ~ p2(X52)
| ! [X53] :
( p2(X53)
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
& ~ p2(X51)
& r1(X50,X51) )
& r1(X39,X50) ) ) ),
inference(nnf_transformation,[],[f91]) ).
fof(f114,plain,
! [X0] :
( ~ sP82(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
& ~ p2(X2)
& r1(X1,X2) )
& r1(X0,X1) ) ) ),
inference(rectify,[],[f113]) ).
fof(f115,plain,
! [X0] :
( ~ sP82(X0)
| ( ! [X5] :
( ( p2(sK105(X5))
& ~ p2(sK106(X5))
& r1(sK105(X5),sK106(X5))
& r1(X5,sK105(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK104(X0),X3) )
& ~ p2(sK104(X0))
& r1(sK103(X0),sK104(X0))
& r1(X0,sK103(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103,sK104,sK105,sK106]),skolemize(X1,sK103(X0)),skolemize(X2,sK104(X0)),skolemize(X6,sK105(X5)),skolemize(X7,sK106(X5))],[f114]) ).
fof(f355,plain,
? [X0] :
( ! [X108] :
( ? [X109] :
( ! [X110] :
( ~ p2(X110)
| ! [X111] :
( p2(X111)
| ~ r1(X110,X111) )
| ~ r1(X109,X110) )
& ~ p2(X109)
& r1(X108,X109) )
| p2(X108)
| ~ r1(X0,X108) )
& ( ? [X102] :
( ! [X104] :
( ( ? [X107] : r1(X104,X107)
& ~ p1(X104) )
| ! [X105] :
( ! [X106] : ~ r1(X105,X106)
| p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X102,X104) )
& ? [X103] : r1(X102,X103)
& ~ p1(X102)
& r1(X0,X102) )
| ! [X101] : ~ r1(X0,X101)
| p1(X0) )
& ( ? [X95] :
( ! [X97] :
( ( ? [X100] : r1(X97,X100)
& ~ p1(X97)
& ~ p2(X97) )
| ! [X98] :
( ! [X99] : ~ r1(X98,X99)
| p1(X98)
| p2(X98)
| ~ r1(X97,X98) )
| ~ r1(X95,X97) )
& ? [X96] : r1(X95,X96)
& ~ p1(X95)
& ~ p2(X95)
& r1(X0,X95) )
| ! [X94] : ~ r1(X0,X94)
| p1(X0)
| p2(X0) )
& ( ? [X92] :
( sP0(X92)
& ? [X93] : r1(X92,X93)
& ~ p1(X92)
& ~ p2(X92)
& ~ p3(X92)
& r1(X0,X92) )
| ! [X91] : ~ r1(X0,X91)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X89] :
( sP1(X89)
& ? [X90] : r1(X89,X90)
& ~ p1(X89)
& ~ p2(X89)
& ~ p3(X89)
& ~ p4(X89)
& r1(X0,X89) )
| ! [X88] : ~ r1(X0,X88)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X87] :
( sP2(X87)
& sP3(X87)
& ~ p1(X87)
& r1(X0,X87) )
| ! [X85] :
( ! [X86] : ~ r1(X85,X86)
| p1(X85)
| p2(X85)
| p3(X85)
| p4(X85)
| ~ r1(X0,X85) )
| p1(X0) )
& ( ? [X84] :
( sP4(X84)
& sP5(X84)
& ~ p1(X84)
& ~ p2(X84)
& r1(X0,X84) )
| ! [X82] :
( ! [X83] : ~ r1(X82,X83)
| p1(X82)
| p2(X82)
| p3(X82)
| p4(X82)
| ~ r1(X0,X82) )
| p1(X0)
| p2(X0) )
& ( ? [X81] :
( sP8(X81)
& sP7(X81)
& ~ p1(X81)
& ~ p2(X81)
& ~ p3(X81)
& r1(X0,X81) )
| ! [X79] :
( ! [X80] : ~ r1(X79,X80)
| p1(X79)
| p2(X79)
| p3(X79)
| p4(X79)
| ~ r1(X0,X79) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X78] :
( sP11(X78)
& sP10(X78)
& ~ p1(X78)
& ~ p2(X78)
& ~ p3(X78)
& ~ p4(X78)
& r1(X0,X78) )
| ! [X76] :
( ! [X77] : ~ r1(X76,X77)
| p1(X76)
| p2(X76)
| p3(X76)
| p4(X76)
| ~ r1(X0,X76) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X75] :
( sP14(X75)
& sP15(X75)
& ~ p1(X75)
& r1(X0,X75) )
| ! [X72] :
( ! [X73] :
( ! [X74] : ~ r1(X73,X74)
| p1(X73)
| p2(X73)
| p3(X73)
| p4(X73)
| ~ r1(X72,X73) )
| p1(X72)
| p2(X72)
| p3(X72)
| p4(X72)
| ~ r1(X0,X72) )
| p1(X0) )
& ( ? [X71] :
( sP18(X71)
& sP19(X71)
& ~ p1(X71)
& ~ p2(X71)
& r1(X0,X71) )
| ! [X68] :
( ! [X69] :
( ! [X70] : ~ r1(X69,X70)
| p1(X69)
| p2(X69)
| p3(X69)
| p4(X69)
| ~ r1(X68,X69) )
| p1(X68)
| p2(X68)
| p3(X68)
| p4(X68)
| ~ r1(X0,X68) )
| p1(X0)
| p2(X0) )
& ( ? [X67] :
( sP24(X67)
& sP23(X67)
& ~ p1(X67)
& ~ p2(X67)
& ~ p3(X67)
& r1(X0,X67) )
| ! [X64] :
( ! [X65] :
( ! [X66] : ~ r1(X65,X66)
| p1(X65)
| p2(X65)
| p3(X65)
| p4(X65)
| ~ r1(X64,X65) )
| p1(X64)
| p2(X64)
| p3(X64)
| p4(X64)
| ~ r1(X0,X64) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X63] :
( sP29(X63)
& sP28(X63)
& ~ p1(X63)
& ~ p2(X63)
& ~ p3(X63)
& ~ p4(X63)
& r1(X0,X63) )
| ! [X60] :
( ! [X61] :
( ! [X62] : ~ r1(X61,X62)
| p1(X61)
| p2(X61)
| p3(X61)
| p4(X61)
| ~ r1(X60,X61) )
| p1(X60)
| p2(X60)
| p3(X60)
| p4(X60)
| ~ r1(X0,X60) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X59] :
( sP34(X59)
& sP35(X59)
& ~ p1(X59)
& r1(X0,X59) )
| ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] : ~ r1(X57,X58)
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(X56,X57) )
| p1(X56)
| p2(X56)
| p3(X56)
| p4(X56)
| ~ r1(X55,X56) )
| p1(X55)
| p2(X55)
| p3(X55)
| p4(X55)
| ~ r1(X0,X55) )
| p1(X0) )
& ( ? [X54] :
( sP40(X54)
& sP41(X54)
& ~ p1(X54)
& ~ p2(X54)
& r1(X0,X54) )
| ! [X50] :
( ! [X51] :
( ! [X52] :
( ! [X53] : ~ r1(X52,X53)
| p1(X52)
| p2(X52)
| p3(X52)
| p4(X52)
| ~ r1(X51,X52) )
| p1(X51)
| p2(X51)
| p3(X51)
| p4(X51)
| ~ r1(X50,X51) )
| p1(X50)
| p2(X50)
| p3(X50)
| p4(X50)
| ~ r1(X0,X50) )
| p1(X0)
| p2(X0) )
& ( ? [X49] :
( sP48(X49)
& sP47(X49)
& ~ p1(X49)
& ~ p2(X49)
& ~ p3(X49)
& r1(X0,X49) )
| ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] : ~ r1(X47,X48)
| p1(X47)
| p2(X47)
| p3(X47)
| p4(X47)
| ~ r1(X46,X47) )
| p1(X46)
| p2(X46)
| p3(X46)
| p4(X46)
| ~ r1(X45,X46) )
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(X0,X45) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X44] :
( sP55(X44)
& sP54(X44)
& ~ p1(X44)
& ~ p2(X44)
& ~ p3(X44)
& ~ p4(X44)
& r1(X0,X44) )
| ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] : ~ r1(X42,X43)
| p1(X42)
| p2(X42)
| p3(X42)
| p4(X42)
| ~ r1(X41,X42) )
| p1(X41)
| p2(X41)
| p3(X41)
| p4(X41)
| ~ r1(X40,X41) )
| p1(X40)
| p2(X40)
| p3(X40)
| p4(X40)
| ~ r1(X0,X40) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X39] :
( sP62(X39)
& sP63(X39)
& ~ p1(X39)
& r1(X0,X39) )
| ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] : ~ r1(X37,X38)
| p1(X37)
| p2(X37)
| p3(X37)
| p4(X37)
| ~ r1(X36,X37) )
| p1(X36)
| p2(X36)
| p3(X36)
| p4(X36)
| ~ r1(X35,X36) )
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X34,X35) )
| p1(X34)
| p2(X34)
| p3(X34)
| p4(X34)
| ~ r1(X0,X34) )
| p1(X0) )
& ( ? [X33] :
( sP70(X33)
& sP71(X33)
& ~ p1(X33)
& ~ p2(X33)
& r1(X0,X33) )
| ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ! [X32] : ~ r1(X31,X32)
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(X30,X31) )
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(X29,X30) )
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29) )
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(X0,X28) )
| p1(X0)
| p2(X0) )
& ( ? [X27] :
( sP80(X27)
& sP79(X27)
& ~ p1(X27)
& ~ p2(X27)
& ~ p3(X27)
& r1(X0,X27) )
| ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] : ~ r1(X25,X26)
| p1(X25)
| p2(X25)
| p3(X25)
| p4(X25)
| ~ r1(X24,X25) )
| p1(X24)
| p2(X24)
| p3(X24)
| p4(X24)
| ~ r1(X23,X24) )
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X0,X22) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X16] :
( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP82(X19)
| sP83(X19)
| ~ r1(X16,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP84(X16) )
& r1(X0,X16) )
| sP86(X0) )
& ! [X13] :
( ? [X14] :
( p1(X14)
& ? [X15] :
( ~ p1(X15)
& r1(X14,X15) )
& r1(X13,X14) )
| p1(X13)
| ~ r1(X0,X13) )
& ? [X12] :
( ~ p1(X12)
& r1(X0,X12) )
& ( sP87(X0)
| ! [X10] :
( ? [X11] :
( p5(X11)
& r1(X10,X11) )
| ~ r1(X0,X10) ) )
& ! [X7] :
( ? [X8] :
( p3(X8)
& ? [X9] :
( ~ p3(X9)
& r1(X8,X9) )
& r1(X7,X8) )
| p3(X7)
| ~ r1(X0,X7) )
& ? [X6] :
( ~ p3(X6)
& r1(X0,X6) )
& ( ( ! [X3] :
( ? [X4] :
( p2(X4)
& ? [X5] :
( ~ p2(X5)
& r1(X4,X5) )
& r1(X3,X4) )
| p2(X3)
| ~ r1(X0,X3) )
& ? [X2] :
( ~ p2(X2)
& r1(X0,X2) ) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(X0,X1) ) ) ),
inference(rectify,[],[f97]) ).
fof(f356,plain,
( ! [X108] :
( ( ! [X110] :
( ~ p2(X110)
| ! [X111] :
( p2(X111)
| ~ r1(X110,X111) )
| ~ r1(sK250(X108),X110) )
& ~ p2(sK250(X108))
& r1(X108,sK250(X108)) )
| p2(X108)
| ~ r1(sK213,X108) )
& ( ( ! [X104] :
( ( r1(X104,sK249(X104))
& ~ p1(X104) )
| ! [X105] :
( ! [X106] : ~ r1(X105,X106)
| p1(X105)
| ~ r1(X104,X105) )
| ~ r1(sK247,X104) )
& r1(sK247,sK248)
& ~ p1(sK247)
& r1(sK213,sK247) )
| ! [X101] : ~ r1(sK213,X101)
| p1(sK213) )
& ( ( ! [X97] :
( ( r1(X97,sK246(X97))
& ~ p1(X97)
& ~ p2(X97) )
| ! [X98] :
( ! [X99] : ~ r1(X98,X99)
| p1(X98)
| p2(X98)
| ~ r1(X97,X98) )
| ~ r1(sK244,X97) )
& r1(sK244,sK245)
& ~ p1(sK244)
& ~ p2(sK244)
& r1(sK213,sK244) )
| ! [X94] : ~ r1(sK213,X94)
| p1(sK213)
| p2(sK213) )
& ( ( sP0(sK242)
& r1(sK242,sK243)
& ~ p1(sK242)
& ~ p2(sK242)
& ~ p3(sK242)
& r1(sK213,sK242) )
| ! [X91] : ~ r1(sK213,X91)
| p1(sK213)
| p2(sK213)
| p3(sK213) )
& ( ( sP1(sK240)
& r1(sK240,sK241)
& ~ p1(sK240)
& ~ p2(sK240)
& ~ p3(sK240)
& ~ p4(sK240)
& r1(sK213,sK240) )
| ! [X88] : ~ r1(sK213,X88)
| p1(sK213)
| p2(sK213)
| p3(sK213)
| p4(sK213) )
& ( ( sP2(sK239)
& sP3(sK239)
& ~ p1(sK239)
& r1(sK213,sK239) )
| ! [X85] :
( ! [X86] : ~ r1(X85,X86)
| p1(X85)
| p2(X85)
| p3(X85)
| p4(X85)
| ~ r1(sK213,X85) )
| p1(sK213) )
& ( ( sP4(sK238)
& sP5(sK238)
& ~ p1(sK238)
& ~ p2(sK238)
& r1(sK213,sK238) )
| ! [X82] :
( ! [X83] : ~ r1(X82,X83)
| p1(X82)
| p2(X82)
| p3(X82)
| p4(X82)
| ~ r1(sK213,X82) )
| p1(sK213)
| p2(sK213) )
& ( ( sP8(sK237)
& sP7(sK237)
& ~ p1(sK237)
& ~ p2(sK237)
& ~ p3(sK237)
& r1(sK213,sK237) )
| ! [X79] :
( ! [X80] : ~ r1(X79,X80)
| p1(X79)
| p2(X79)
| p3(X79)
| p4(X79)
| ~ r1(sK213,X79) )
| p1(sK213)
| p2(sK213)
| p3(sK213) )
& ( ( sP11(sK236)
& sP10(sK236)
& ~ p1(sK236)
& ~ p2(sK236)
& ~ p3(sK236)
& ~ p4(sK236)
& r1(sK213,sK236) )
| ! [X76] :
( ! [X77] : ~ r1(X76,X77)
| p1(X76)
| p2(X76)
| p3(X76)
| p4(X76)
| ~ r1(sK213,X76) )
| p1(sK213)
| p2(sK213)
| p3(sK213)
| p4(sK213) )
& ( ( sP14(sK235)
& sP15(sK235)
& ~ p1(sK235)
& r1(sK213,sK235) )
| ! [X72] :
( ! [X73] :
( ! [X74] : ~ r1(X73,X74)
| p1(X73)
| p2(X73)
| p3(X73)
| p4(X73)
| ~ r1(X72,X73) )
| p1(X72)
| p2(X72)
| p3(X72)
| p4(X72)
| ~ r1(sK213,X72) )
| p1(sK213) )
& ( ( sP18(sK234)
& sP19(sK234)
& ~ p1(sK234)
& ~ p2(sK234)
& r1(sK213,sK234) )
| ! [X68] :
( ! [X69] :
( ! [X70] : ~ r1(X69,X70)
| p1(X69)
| p2(X69)
| p3(X69)
| p4(X69)
| ~ r1(X68,X69) )
| p1(X68)
| p2(X68)
| p3(X68)
| p4(X68)
| ~ r1(sK213,X68) )
| p1(sK213)
| p2(sK213) )
& ( ( sP24(sK233)
& sP23(sK233)
& ~ p1(sK233)
& ~ p2(sK233)
& ~ p3(sK233)
& r1(sK213,sK233) )
| ! [X64] :
( ! [X65] :
( ! [X66] : ~ r1(X65,X66)
| p1(X65)
| p2(X65)
| p3(X65)
| p4(X65)
| ~ r1(X64,X65) )
| p1(X64)
| p2(X64)
| p3(X64)
| p4(X64)
| ~ r1(sK213,X64) )
| p1(sK213)
| p2(sK213)
| p3(sK213) )
& ( ( sP29(sK232)
& sP28(sK232)
& ~ p1(sK232)
& ~ p2(sK232)
& ~ p3(sK232)
& ~ p4(sK232)
& r1(sK213,sK232) )
| ! [X60] :
( ! [X61] :
( ! [X62] : ~ r1(X61,X62)
| p1(X61)
| p2(X61)
| p3(X61)
| p4(X61)
| ~ r1(X60,X61) )
| p1(X60)
| p2(X60)
| p3(X60)
| p4(X60)
| ~ r1(sK213,X60) )
| p1(sK213)
| p2(sK213)
| p3(sK213)
| p4(sK213) )
& ( ( sP34(sK231)
& sP35(sK231)
& ~ p1(sK231)
& r1(sK213,sK231) )
| ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] : ~ r1(X57,X58)
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(X56,X57) )
| p1(X56)
| p2(X56)
| p3(X56)
| p4(X56)
| ~ r1(X55,X56) )
| p1(X55)
| p2(X55)
| p3(X55)
| p4(X55)
| ~ r1(sK213,X55) )
| p1(sK213) )
& ( ( sP40(sK230)
& sP41(sK230)
& ~ p1(sK230)
& ~ p2(sK230)
& r1(sK213,sK230) )
| ! [X50] :
( ! [X51] :
( ! [X52] :
( ! [X53] : ~ r1(X52,X53)
| p1(X52)
| p2(X52)
| p3(X52)
| p4(X52)
| ~ r1(X51,X52) )
| p1(X51)
| p2(X51)
| p3(X51)
| p4(X51)
| ~ r1(X50,X51) )
| p1(X50)
| p2(X50)
| p3(X50)
| p4(X50)
| ~ r1(sK213,X50) )
| p1(sK213)
| p2(sK213) )
& ( ( sP48(sK229)
& sP47(sK229)
& ~ p1(sK229)
& ~ p2(sK229)
& ~ p3(sK229)
& r1(sK213,sK229) )
| ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] : ~ r1(X47,X48)
| p1(X47)
| p2(X47)
| p3(X47)
| p4(X47)
| ~ r1(X46,X47) )
| p1(X46)
| p2(X46)
| p3(X46)
| p4(X46)
| ~ r1(X45,X46) )
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(sK213,X45) )
| p1(sK213)
| p2(sK213)
| p3(sK213) )
& ( ( sP55(sK228)
& sP54(sK228)
& ~ p1(sK228)
& ~ p2(sK228)
& ~ p3(sK228)
& ~ p4(sK228)
& r1(sK213,sK228) )
| ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] : ~ r1(X42,X43)
| p1(X42)
| p2(X42)
| p3(X42)
| p4(X42)
| ~ r1(X41,X42) )
| p1(X41)
| p2(X41)
| p3(X41)
| p4(X41)
| ~ r1(X40,X41) )
| p1(X40)
| p2(X40)
| p3(X40)
| p4(X40)
| ~ r1(sK213,X40) )
| p1(sK213)
| p2(sK213)
| p3(sK213)
| p4(sK213) )
& ( ( sP62(sK227)
& sP63(sK227)
& ~ p1(sK227)
& r1(sK213,sK227) )
| ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] : ~ r1(X37,X38)
| p1(X37)
| p2(X37)
| p3(X37)
| p4(X37)
| ~ r1(X36,X37) )
| p1(X36)
| p2(X36)
| p3(X36)
| p4(X36)
| ~ r1(X35,X36) )
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X34,X35) )
| p1(X34)
| p2(X34)
| p3(X34)
| p4(X34)
| ~ r1(sK213,X34) )
| p1(sK213) )
& ( ( sP70(sK226)
& sP71(sK226)
& ~ p1(sK226)
& ~ p2(sK226)
& r1(sK213,sK226) )
| ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ! [X32] : ~ r1(X31,X32)
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(X30,X31) )
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(X29,X30) )
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29) )
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(sK213,X28) )
| p1(sK213)
| p2(sK213) )
& ( ( sP80(sK225)
& sP79(sK225)
& ~ p1(sK225)
& ~ p2(sK225)
& ~ p3(sK225)
& r1(sK213,sK225) )
| ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] : ~ r1(X25,X26)
| p1(X25)
| p2(X25)
| p3(X25)
| p4(X25)
| ~ r1(X24,X25) )
| p1(X24)
| p2(X24)
| p3(X24)
| p4(X24)
| ~ r1(X23,X24) )
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(sK213,X22) )
| p1(sK213)
| p2(sK213)
| p3(sK213) )
& ( ( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP82(X19)
| sP83(X19)
| ~ r1(sK224,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(sK224,X17) )
& ~ p2(sK224) )
| sP84(sK224) )
& r1(sK213,sK224) )
| sP86(sK213) )
& ! [X13] :
( ( p1(sK222(X13))
& ~ p1(sK223(X13))
& r1(sK222(X13),sK223(X13))
& r1(X13,sK222(X13)) )
| p1(X13)
| ~ r1(sK213,X13) )
& ~ p1(sK221)
& r1(sK213,sK221)
& ( sP87(sK213)
| ! [X10] :
( ( p5(sK220(X10))
& r1(X10,sK220(X10)) )
| ~ r1(sK213,X10) ) )
& ! [X7] :
( ( p3(sK218(X7))
& ~ p3(sK219(X7))
& r1(sK218(X7),sK219(X7))
& r1(X7,sK218(X7)) )
| p3(X7)
| ~ r1(sK213,X7) )
& ~ p3(sK217)
& r1(sK213,sK217)
& ( ( ! [X3] :
( ( p2(sK215(X3))
& ~ p2(sK216(X3))
& r1(sK215(X3),sK216(X3))
& r1(X3,sK215(X3)) )
| p2(X3)
| ~ r1(sK213,X3) )
& ~ p2(sK214)
& r1(sK213,sK214) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(sK213,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK213,sK214,sK215,sK216,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]),skolemize(X0,sK213),skolemize(X2,sK214),skolemize(X4,sK215(X3)),skolemize(X5,sK216(X3)),skolemize(X6,sK217),skolemize(X8,sK218(X7)),skolemize(X9,sK219(X7)),skolemize(X11,sK220(X10)),skolemize(X12,sK221),skolemize(X14,sK222(X13)),skolemize(X15,sK223(X13)),skolemize(X16,sK224),skolemize(X27,sK225),skolemize(X33,sK226),skolemize(X39,sK227),skolemize(X44,sK228),skolemize(X49,sK229),skolemize(X54,sK230),skolemize(X59,sK231),skolemize(X63,sK232),skolemize(X67,sK233),skolemize(X71,sK234),skolemize(X75,sK235),skolemize(X78,sK236),skolemize(X81,sK237),skolemize(X84,sK238),skolemize(X87,sK239),skolemize(X89,sK240),skolemize(X90,sK241),skolemize(X92,sK242),skolemize(X93,sK243),skolemize(X95,sK244),skolemize(X96,sK245),skolemize(X100,sK246(X97)),skolemize(X102,sK247),skolemize(X103,sK248),skolemize(X107,sK249(X104)),skolemize(X109,sK250(X108))],[f355]) ).
fof(f357,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f358,plain,
! [X2,X0] :
( ~ sP87(X0)
| p2(sK89(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f359,plain,
! [X2,X0] :
( ~ sP87(X0)
| ~ p2(sK90(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f360,plain,
! [X2,X0] :
( ~ sP87(X0)
| r1(sK89(X2),sK90(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f361,plain,
! [X2,X0] :
( ~ sP87(X0)
| r1(X2,sK89(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f362,plain,
! [X0] :
( ~ sP87(X0)
| ~ p2(sK88(X0)) ),
inference(cnf_transformation,[],[f100]) ).
fof(f363,plain,
! [X0] :
( ~ sP87(X0)
| r1(X0,sK88(X0)) ),
inference(cnf_transformation,[],[f100]) ).
fof(f368,plain,
! [X2,X3,X0] :
( ~ sP86(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK91(X0),X2)
| sP85(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f369,plain,
! [X0] :
( ~ sP86(X0)
| ~ p2(sK91(X0))
| sP85(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f370,plain,
! [X0] :
( ~ sP86(X0)
| r1(X0,sK91(X0))
| sP85(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f371,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| p2(sK94(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f372,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| ~ p2(sK95(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f373,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| r1(sK94(X2),sK95(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f374,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| r1(X2,sK94(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f375,plain,
! [X0,X5] :
( ~ sP84(X0)
| p2(sK98(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f376,plain,
! [X0,X5] :
( ~ sP84(X0)
| ~ p2(sK99(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f377,plain,
! [X0,X5] :
( ~ sP84(X0)
| r1(sK98(X5),sK99(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f378,plain,
! [X0,X5] :
( ~ sP84(X0)
| r1(X5,sK98(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f379,plain,
! [X3,X0,X4] :
( ~ sP84(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK97(X0),X3) ),
inference(cnf_transformation,[],[f109]) ).
fof(f380,plain,
! [X0] :
( ~ sP84(X0)
| ~ p2(sK97(X0)) ),
inference(cnf_transformation,[],[f109]) ).
fof(f381,plain,
! [X0] :
( ~ sP84(X0)
| r1(sK96(X0),sK97(X0)) ),
inference(cnf_transformation,[],[f109]) ).
fof(f382,plain,
! [X0] :
( ~ sP84(X0)
| r1(X0,sK96(X0)) ),
inference(cnf_transformation,[],[f109]) ).
fof(f383,plain,
! [X0,X1] :
( ~ sP83(X0)
| p2(sK101(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f384,plain,
! [X0,X1] :
( ~ sP83(X0)
| ~ p2(sK102(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f385,plain,
! [X0,X1] :
( ~ sP83(X0)
| r1(sK101(X1),sK102(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sP83(X0)
| r1(X1,sK101(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f390,plain,
! [X0,X5] :
( ~ sP82(X0)
| p2(sK105(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f115]) ).
fof(f391,plain,
! [X0,X5] :
( ~ sP82(X0)
| ~ p2(sK106(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f115]) ).
fof(f392,plain,
! [X0,X5] :
( ~ sP82(X0)
| r1(sK105(X5),sK106(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f115]) ).
fof(f393,plain,
! [X0,X5] :
( ~ sP82(X0)
| r1(X5,sK105(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f115]) ).
fof(f886,plain,
! [X111,X108,X110] :
( ~ p2(X110)
| p2(X111)
| ~ r1(X110,X111)
| ~ r1(sK250(X108),X110)
| p2(X108)
| ~ r1(sK213,X108) ),
inference(cnf_transformation,[],[f356]) ).
fof(f887,plain,
! [X108] :
( ~ p2(sK250(X108))
| p2(X108)
| ~ r1(sK213,X108) ),
inference(cnf_transformation,[],[f356]) ).
fof(f888,plain,
! [X108] :
( r1(X108,sK250(X108))
| p2(X108)
| ~ r1(sK213,X108) ),
inference(cnf_transformation,[],[f356]) ).
fof(f995,plain,
! [X21,X19,X20] :
( ~ p2(X20)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| sP82(X19)
| sP83(X19)
| ~ r1(sK224,X19)
| sP86(sK213) ),
inference(cnf_transformation,[],[f356]) ).
fof(f996,plain,
! [X19] :
( ~ p2(X19)
| sP82(X19)
| sP83(X19)
| ~ r1(sK224,X19)
| sP86(sK213) ),
inference(cnf_transformation,[],[f356]) ).
fof(f997,plain,
! [X18,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(sK224,X17)
| sP84(sK224)
| sP86(sK213) ),
inference(cnf_transformation,[],[f356]) ).
fof(f998,plain,
( ~ p2(sK224)
| sP84(sK224)
| sP86(sK213) ),
inference(cnf_transformation,[],[f356]) ).
fof(f999,plain,
( r1(sK213,sK224)
| sP86(sK213) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1006,plain,
! [X10] :
( sP87(sK213)
| p5(sK220(X10))
| ~ r1(sK213,X10) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1007,plain,
! [X10] :
( sP87(sK213)
| r1(X10,sK220(X10))
| ~ r1(sK213,X10) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1011,plain,
! [X7] :
( r1(X7,sK218(X7))
| p3(X7)
| ~ r1(sK213,X7) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1013,plain,
r1(sK213,sK217),
inference(cnf_transformation,[],[f356]) ).
fof(f1014,plain,
! [X3,X1] :
( p2(sK215(X3))
| p2(X3)
| ~ r1(sK213,X3)
| ~ p5(X1)
| ~ r1(sK213,X1) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1015,plain,
! [X3,X1] :
( ~ p2(sK216(X3))
| p2(X3)
| ~ r1(sK213,X3)
| ~ p5(X1)
| ~ r1(sK213,X1) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1016,plain,
! [X3,X1] :
( r1(sK215(X3),sK216(X3))
| p2(X3)
| ~ r1(sK213,X3)
| ~ p5(X1)
| ~ r1(sK213,X1) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1017,plain,
! [X3,X1] :
( r1(X3,sK215(X3))
| p2(X3)
| ~ r1(sK213,X3)
| ~ p5(X1)
| ~ r1(sK213,X1) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1018,plain,
! [X1] :
( ~ p2(sK214)
| ~ p5(X1)
| ~ r1(sK213,X1) ),
inference(cnf_transformation,[],[f356]) ).
fof(f1019,plain,
! [X1] :
( r1(sK213,sK214)
| ~ p5(X1)
| ~ r1(sK213,X1) ),
inference(cnf_transformation,[],[f356]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f357]) ).
tcf(c_50,plain,
! [X0: $i] :
( r1(X0,sK88(X0))
| ~ sP87(X0) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_51,plain,
! [X0: $i] :
( ~ sP87(X0)
| ~ p2(sK88(X0)) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK89(X1))
| ~ sP87(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK89(X1),sK90(X1))
| ~ sP87(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP87(X0)
| ~ p2(sK90(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f359]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK89(X1))
| ~ sP87(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f358]) ).
tcf(c_56,plain,
! [X0: $i] :
( sP85(X0)
| r1(X0,sK91(X0))
| ~ sP86(X0) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_57,plain,
! [X0: $i] :
( sP85(X0)
| ~ sP86(X0)
| ~ p2(sK91(X0)) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP85(X0)
| p2(X2)
| ~ sP86(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK91(X0),X1) ),
inference(cnf_transformation,[],[f368]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK94(X2))
| ~ sP85(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK94(X2),sK95(X2))
| ~ sP85(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f373]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP85(X0)
| ~ p2(sK95(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK94(X2))
| ~ sP85(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_67,plain,
! [X0: $i] :
( r1(X0,sK96(X0))
| ~ sP84(X0) ),
inference(cnf_transformation,[],[f382]) ).
tcf(c_68,plain,
! [X0: $i] :
( r1(sK96(X0),sK97(X0))
| ~ sP84(X0) ),
inference(cnf_transformation,[],[f381]) ).
tcf(c_69,plain,
! [X0: $i] :
( ~ sP84(X0)
| ~ p2(sK97(X0)) ),
inference(cnf_transformation,[],[f380]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP84(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK97(X0),X1) ),
inference(cnf_transformation,[],[f379]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK98(X1))
| ~ sP84(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK98(X1),sK99(X1))
| ~ sP84(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP84(X0)
| ~ p2(sK99(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f376]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK98(X1))
| ~ sP84(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK101(X1))
| ~ sP83(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f386]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK101(X1),sK102(X1))
| ~ sP83(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP83(X0)
| ~ p2(sK102(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f384]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK101(X1))
| ~ sP83(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK105(X1))
| ~ sP82(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f393]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK105(X1),sK106(X1))
| ~ sP82(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f392]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP82(X0)
| ~ p2(sK106(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f391]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK105(X1))
| ~ sP82(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f390]) ).
tcf(c_578,negated_conjecture,
! [X0: $i] :
( r1(sK213,sK214)
| ~ p5(X0)
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1019]) ).
tcf(c_579,negated_conjecture,
! [X0: $i] :
( ~ p2(sK214)
| ~ p5(X0)
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1018]) ).
tcf(c_580,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(X0,sK215(X0))
| ~ p5(X1)
| ~ r1(sK213,X1)
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1017]) ).
tcf(c_581,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(sK215(X0),sK216(X0))
| ~ p5(X1)
| ~ r1(sK213,X1)
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1016]) ).
tcf(c_582,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| ~ p5(X1)
| ~ p2(sK216(X0))
| ~ r1(sK213,X1)
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1015]) ).
tcf(c_583,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| p2(sK215(X0))
| ~ p5(X1)
| ~ r1(sK213,X1)
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1014]) ).
tcf(c_584,negated_conjecture,
r1(sK213,sK217),
inference(cnf_transformation,[],[f1013]) ).
tcf(c_586,negated_conjecture,
! [X0: $i] :
( p3(X0)
| r1(X0,sK218(X0))
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1011]) ).
tcf(c_590,negated_conjecture,
! [X0: $i] :
( sP87(sK213)
| r1(X0,sK220(X0))
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1007]) ).
tcf(c_591,negated_conjecture,
! [X0: $i] :
( sP87(sK213)
| p5(sK220(X0))
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f1006]) ).
tcf(c_598,negated_conjecture,
( sP86(sK213)
| r1(sK213,sK224) ),
inference(cnf_transformation,[],[f999]) ).
tcf(c_599,negated_conjecture,
( sP84(sK224)
| sP86(sK213)
| ~ p2(sK224) ),
inference(cnf_transformation,[],[f998]) ).
tcf(c_600,negated_conjecture,
! [X0: $i,X1: $i] :
( sP84(sK224)
| sP86(sK213)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK224,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f997]) ).
tcf(c_601,negated_conjecture,
! [X0: $i] :
( sP86(sK213)
| sP82(X0)
| sP83(X0)
| ~ p2(X0)
| ~ r1(sK224,X0) ),
inference(cnf_transformation,[],[f996]) ).
tcf(c_602,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP86(sK213)
| sP82(X0)
| sP83(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK224,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f995]) ).
tcf(c_709,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK250(X0))
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f888]) ).
tcf(c_710,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK250(X0))
| ~ r1(sK213,X0) ),
inference(cnf_transformation,[],[f887]) ).
tcf(c_711,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK213,X0)
| ~ r1(X1,X2)
| ~ r1(sK250(X0),X1) ),
inference(cnf_transformation,[],[f886]) ).
tcf(c_712,plain,
r1(sK213,sK213),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1073,plain,
( ~ sP87(sK213)
| ~ p2(sK88(sK213)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_1074,plain,
( r1(sK213,sK88(sK213))
| ~ sP87(sK213) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_1114,plain,
( sP85(sK213)
| ~ sP86(sK213)
| ~ p2(sK91(sK213)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_1115,plain,
( sP85(sK213)
| r1(sK213,sK91(sK213))
| ~ sP86(sK213) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_1120,plain,
( sP87(sK213)
| r1(sK213,sK220(sK213))
| ~ r1(sK213,sK213) ),
inference(instantiation,[status(thm)],[c_590]) ).
tcf(c_9572,plain,
! [X0: $i] :
( sP87(sK213)
| ~ p2(sK214)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK220(X0)) ),
inference(resolution,[status(thm)],[c_579,c_591]) ).
tcf(c_9573,plain,
( sP87(sK213)
| ~ p2(sK214)
| ~ r1(sK213,sK213)
| ~ r1(sK213,sK220(sK213)) ),
inference(instantiation,[status(thm)],[c_9572]) ).
tcf(c_9574,plain,
( sP87(sK213)
| ~ p2(sK214) ),
inference(global_subsumption_just,[status(thm)],[c_9572,c_712,c_1120,c_9573]) ).
tcf(c_9582,plain,
! [X0: $i] :
( sP87(sK213)
| r1(sK213,sK214)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK220(X0)) ),
inference(resolution,[status(thm)],[c_578,c_591]) ).
tcf(c_9583,plain,
( sP87(sK213)
| r1(sK213,sK214)
| ~ r1(sK213,sK213)
| ~ r1(sK213,sK220(sK213)) ),
inference(instantiation,[status(thm)],[c_9582]) ).
tcf(c_9584,plain,
( sP87(sK213)
| r1(sK213,sK214) ),
inference(global_subsumption_just,[status(thm)],[c_9582,c_712,c_1120,c_9583]) ).
tcf(c_9592,plain,
! [X0: $i,X1: $i] :
( sP87(sK213)
| p2(X1)
| p2(sK215(X1))
| ~ r1(sK213,X1)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK220(X0)) ),
inference(resolution,[status(thm)],[c_583,c_591]) ).
tcf(c_9612,plain,
! [X0: $i,X1: $i] :
( sP87(sK213)
| p2(X1)
| ~ p2(sK216(X1))
| ~ r1(sK213,X1)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK220(X0)) ),
inference(resolution,[status(thm)],[c_582,c_591]) ).
tcf(c_9632,plain,
! [X0: $i,X1: $i] :
( sP87(sK213)
| p2(X1)
| r1(sK215(X1),sK216(X1))
| ~ r1(sK213,X1)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK220(X0)) ),
inference(resolution,[status(thm)],[c_581,c_591]) ).
tcf(c_9652,plain,
! [X0: $i,X1: $i] :
( sP87(sK213)
| p2(X1)
| r1(X1,sK215(X1))
| ~ r1(sK213,X1)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK220(X0)) ),
inference(resolution,[status(thm)],[c_580,c_591]) ).
tcf(c_13816,plain,
! [X0: $i] :
( ~ iPr_def_10
| p2(X0)
| ~ r1(sK213,X0)
| r1(X0,sK215(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_9652]) ).
tcf(c_13817,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ r1(sK213,sK220(X0))
| ~ r1(sK213,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_9652]) ).
tcf(c_13818,plain,
( iPr_def_11
| iPr_def_10
| sP87(sK213) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_9652]) ).
tcf(c_13819,plain,
! [X0: $i] :
( ~ iPr_def_12
| p2(X0)
| ~ r1(sK213,X0)
| r1(sK215(X0),sK216(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_9632]) ).
tcf(c_13820,plain,
( iPr_def_12
| iPr_def_11
| sP87(sK213) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_9632]) ).
tcf(c_13821,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p2(sK216(X0))
| p2(X0)
| ~ r1(sK213,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_9612]) ).
tcf(c_13822,plain,
( iPr_def_13
| iPr_def_11
| sP87(sK213) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_9612]) ).
tcf(c_13823,plain,
! [X0: $i] :
( ~ iPr_def_14
| p2(sK215(X0))
| p2(X0)
| ~ r1(sK213,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_9592]) ).
tcf(c_13824,plain,
( iPr_def_14
| iPr_def_11
| sP87(sK213) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_9592]) ).
tcf(c_13825,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_15
| p2(X1)
| ~ p2(X0)
| ~ r1(sK224,X0)
| ~ r1(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_600]) ).
tcf(c_13826,negated_conjecture,
( iPr_def_15
| sP84(sK224)
| sP86(sK213) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_600]) ).
tcf(c_13827,plain,
( ~ iPr_def_11
| ~ r1(sK213,sK213)
| ~ r1(sK213,sK220(sK213)) ),
inference(instantiation,[status(thm)],[c_13817]) ).
tcf(c_13873,plain,
! [X0: $i] :
( p2(sK88(X0))
| r1(sK88(X0),sK250(sK88(X0)))
| ~ r1(sK213,sK88(X0)) ),
inference(instantiation,[status(thm)],[c_709]) ).
tcf(c_13874,plain,
( p2(sK88(sK213))
| r1(sK88(sK213),sK250(sK88(sK213)))
| ~ r1(sK213,sK88(sK213)) ),
inference(instantiation,[status(thm)],[c_13873]) ).
tcf(c_13886,plain,
( ~ sP84(sK224)
| ~ p2(sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_13986,plain,
! [X0: $i] :
( p2(sK97(sK224))
| r1(sK105(sK97(sK224)),sK106(sK97(sK224)))
| ~ sP82(X0)
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_13987,plain,
! [X0: $i] :
( p2(sK97(sK224))
| r1(sK101(sK97(sK224)),sK102(sK97(sK224)))
| ~ sP83(X0)
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_13990,plain,
! [X0: $i] :
( p2(sK97(sK224))
| ~ sP82(X0)
| ~ p2(sK106(sK97(sK224)))
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_13991,plain,
! [X0: $i] :
( p2(sK97(sK224))
| r1(sK97(sK224),sK105(sK97(sK224)))
| ~ sP82(X0)
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_13992,plain,
! [X0: $i] :
( p2(sK97(sK224))
| ~ sP83(X0)
| ~ p2(sK102(sK97(sK224)))
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_13993,plain,
! [X0: $i] :
( p2(sK97(sK224))
| r1(sK97(sK224),sK101(sK97(sK224)))
| ~ sP83(X0)
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_13998,plain,
! [X0: $i] :
( p2(sK97(sK224))
| p2(sK105(sK97(sK224)))
| ~ sP82(X0)
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_13999,plain,
! [X0: $i] :
( p2(sK97(sK224))
| p2(sK101(sK97(sK224)))
| ~ sP83(X0)
| ~ r1(X0,sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_14097,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK250(sK88(X1)))
| r1(sK94(sK250(sK88(X1))),sK95(sK250(sK88(X1))))
| ~ sP85(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK250(sK88(X1))) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_14102,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK250(sK88(X1)))
| ~ sP85(X2)
| ~ r1(X2,X0)
| ~ p2(sK95(sK250(sK88(X1))))
| ~ r1(X0,sK250(sK88(X1))) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_14103,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK250(sK88(X1)))
| r1(sK250(sK88(X1)),sK94(sK250(sK88(X1))))
| ~ sP85(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK250(sK88(X1))) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_14105,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK250(sK88(X1)))
| p2(sK94(sK250(sK88(X1))))
| ~ sP85(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK250(sK88(X1))) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_14233,plain,
( r1(sK224,sK96(sK224))
| ~ sP84(sK224) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_14313,plain,
( p2(sK214)
| r1(sK214,sK250(sK214))
| ~ r1(sK213,sK214) ),
inference(instantiation,[status(thm)],[c_709]) ).
tcf(c_14517,plain,
( sP87(sK213)
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_13818,c_712,c_1120,c_13818,c_13827]) ).
tcf(c_14518,plain,
( iPr_def_10
| sP87(sK213) ),
inference(renaming,[status(thm)],[c_14517]) ).
tcf(c_14519,plain,
( iPr_def_12
| sP87(sK213) ),
inference(global_subsumption_just,[status(thm)],[c_13820,c_712,c_1120,c_13820,c_13827]) ).
tcf(c_14521,plain,
( iPr_def_13
| sP87(sK213) ),
inference(global_subsumption_just,[status(thm)],[c_13822,c_712,c_1120,c_13822,c_13827]) ).
tcf(c_14523,plain,
( iPr_def_14
| sP87(sK213) ),
inference(global_subsumption_just,[status(thm)],[c_13824,c_712,c_1120,c_13824,c_13827]) ).
tcf(c_14578,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK214))
| r1(sK94(sK250(sK214)),sK95(sK250(sK214)))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_14583,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK214))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ p2(sK95(sK250(sK214)))
| ~ r1(X0,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_14584,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK214))
| r1(sK250(sK214),sK94(sK250(sK214)))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_14586,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK214))
| p2(sK94(sK250(sK214)))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_14625,plain,
! [X0: $i] :
( p2(sK91(X0))
| p2(sK215(sK91(X0)))
| ~ iPr_def_14
| ~ r1(sK213,sK91(X0)) ),
inference(instantiation,[status(thm)],[c_13823]) ).
tcf(c_14626,plain,
! [X0: $i] :
( p2(sK91(X0))
| ~ iPr_def_13
| ~ p2(sK216(sK91(X0)))
| ~ r1(sK213,sK91(X0)) ),
inference(instantiation,[status(thm)],[c_13821]) ).
tcf(c_14646,plain,
! [X0: $i,X1: $i] :
( p2(sK91(X1))
| ~ sP87(X0)
| ~ p2(sK90(sK91(X1)))
| ~ r1(X0,sK91(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_14657,plain,
( p2(sK91(sK213))
| ~ sP87(sK213)
| ~ p2(sK90(sK91(sK213)))
| ~ r1(sK213,sK91(sK213)) ),
inference(instantiation,[status(thm)],[c_14646]) ).
tcf(c_14701,plain,
( p2(sK88(sK213))
| ~ sP87(sK213)
| ~ p2(sK250(sK88(sK213))) ),
inference(superposition,[status(thm)],[c_50,c_710]) ).
tcf(c_14800,plain,
( p2(sK214)
| sP87(sK213)
| ~ p2(sK250(sK214)) ),
inference(superposition,[status(thm)],[c_9584,c_710]) ).
tcf(c_14807,plain,
( sP86(sK213)
| sP82(sK96(sK224))
| sP83(sK96(sK224))
| ~ sP84(sK224)
| ~ p2(sK96(sK224)) ),
inference(superposition,[status(thm)],[c_67,c_601]) ).
tcf(c_14925,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK88(X0)))
| ~ sP85(X1)
| ~ r1(X1,sK88(X0))
| ~ p2(sK95(sK250(sK88(X0))))
| ~ r1(sK88(X0),sK250(sK88(X0))) ),
inference(instantiation,[status(thm)],[c_14102]) ).
tcf(c_14926,plain,
( p2(sK250(sK88(sK213)))
| ~ sP85(sK213)
| ~ r1(sK213,sK88(sK213))
| ~ p2(sK95(sK250(sK88(sK213))))
| ~ r1(sK88(sK213),sK250(sK88(sK213))) ),
inference(instantiation,[status(thm)],[c_14925]) ).
tcf(c_14946,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK88(X0)))
| r1(sK94(sK250(sK88(X0))),sK95(sK250(sK88(X0))))
| ~ sP85(X1)
| ~ r1(X1,sK88(X0))
| ~ r1(sK88(X0),sK250(sK88(X0))) ),
inference(instantiation,[status(thm)],[c_14097]) ).
tcf(c_14947,plain,
( p2(sK250(sK88(sK213)))
| r1(sK94(sK250(sK88(sK213))),sK95(sK250(sK88(sK213))))
| ~ sP85(sK213)
| ~ r1(sK213,sK88(sK213))
| ~ r1(sK88(sK213),sK250(sK88(sK213))) ),
inference(instantiation,[status(thm)],[c_14946]) ).
tcf(c_14951,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK88(X0)))
| r1(sK250(sK88(X0)),sK94(sK250(sK88(X0))))
| ~ sP85(X1)
| ~ r1(X1,sK88(X0))
| ~ r1(sK88(X0),sK250(sK88(X0))) ),
inference(instantiation,[status(thm)],[c_14103]) ).
tcf(c_14952,plain,
( p2(sK250(sK88(sK213)))
| r1(sK250(sK88(sK213)),sK94(sK250(sK88(sK213))))
| ~ sP85(sK213)
| ~ r1(sK213,sK88(sK213))
| ~ r1(sK88(sK213),sK250(sK88(sK213))) ),
inference(instantiation,[status(thm)],[c_14951]) ).
tcf(c_14956,plain,
! [X0: $i,X1: $i] :
( p2(sK250(sK88(X0)))
| p2(sK94(sK250(sK88(X0))))
| ~ sP85(X1)
| ~ r1(X1,sK88(X0))
| ~ r1(sK88(X0),sK250(sK88(X0))) ),
inference(instantiation,[status(thm)],[c_14105]) ).
tcf(c_14957,plain,
( p2(sK250(sK88(sK213)))
| p2(sK94(sK250(sK88(sK213))))
| ~ sP85(sK213)
| ~ r1(sK213,sK88(sK213))
| ~ r1(sK88(sK213),sK250(sK88(sK213))) ),
inference(instantiation,[status(thm)],[c_14956]) ).
tcf(c_15021,plain,
! [X0: $i] :
( p2(sK250(sK214))
| ~ sP85(X0)
| ~ r1(X0,sK214)
| ~ p2(sK95(sK250(sK214)))
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_14583]) ).
tcf(c_15022,plain,
( p2(sK250(sK214))
| ~ sP85(sK213)
| ~ r1(sK213,sK214)
| ~ p2(sK95(sK250(sK214)))
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_15021]) ).
tcf(c_15038,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK95(sK250(sK88(X1))))
| ~ p2(X0)
| ~ r1(sK213,X2)
| ~ r1(sK250(X2),X0)
| ~ r1(X0,sK95(sK250(sK88(X1)))) ),
inference(instantiation,[status(thm)],[c_711]) ).
tcf(c_15462,plain,
( sP86(sK213)
| p2(sK224)
| p2(sK215(sK224))
| ~ iPr_def_14 ),
inference(resolution,[status(thm)],[c_13823,c_598]) ).
tcf(c_15501,plain,
! [X0: $i] :
( p2(sK250(sK214))
| r1(sK94(sK250(sK214)),sK95(sK250(sK214)))
| ~ sP85(X0)
| ~ r1(X0,sK214)
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_14578]) ).
tcf(c_15502,plain,
( p2(sK250(sK214))
| r1(sK94(sK250(sK214)),sK95(sK250(sK214)))
| ~ sP85(sK213)
| ~ r1(sK213,sK214)
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_15501]) ).
tcf(c_15506,plain,
! [X0: $i] :
( p2(sK250(sK214))
| r1(sK250(sK214),sK94(sK250(sK214)))
| ~ sP85(X0)
| ~ r1(X0,sK214)
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_14584]) ).
tcf(c_15507,plain,
( p2(sK250(sK214))
| r1(sK250(sK214),sK94(sK250(sK214)))
| ~ sP85(sK213)
| ~ r1(sK213,sK214)
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_15506]) ).
tcf(c_15511,plain,
! [X0: $i] :
( p2(sK250(sK214))
| p2(sK94(sK250(sK214)))
| ~ sP85(X0)
| ~ r1(X0,sK214)
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_14586]) ).
tcf(c_15512,plain,
( p2(sK250(sK214))
| p2(sK94(sK250(sK214)))
| ~ sP85(sK213)
| ~ r1(sK213,sK214)
| ~ r1(sK214,sK250(sK214)) ),
inference(instantiation,[status(thm)],[c_15511]) ).
tcf(c_15558,plain,
( p2(sK214)
| sP87(sK213)
| ~ p2(sK250(sK214)) ),
inference(superposition,[status(thm)],[c_9584,c_710]) ).
tcf(c_15591,plain,
( ~ p2(sK250(sK214))
| sP87(sK213) ),
inference(global_subsumption_just,[status(thm)],[c_15558,c_9574,c_14800]) ).
tcf(c_15592,plain,
( sP87(sK213)
| ~ p2(sK250(sK214)) ),
inference(renaming,[status(thm)],[c_15591]) ).
tcf(c_15595,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| p2(sK89(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(superposition,[status(thm)],[c_56,c_55]) ).
tcf(c_15610,plain,
( sP86(sK213)
| p2(sK224)
| p2(sK89(sK224))
| ~ sP87(sK213) ),
inference(superposition,[status(thm)],[c_598,c_55]) ).
tcf(c_15812,plain,
! [X0: $i] :
( p2(X0)
| p2(sK250(X0))
| p2(sK98(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(superposition,[status(thm)],[c_709,c_74]) ).
tcf(c_15861,plain,
! [X0: $i] :
( p2(sK96(sK224))
| r1(sK98(sK96(sK224)),sK99(sK96(sK224)))
| ~ sP84(X0)
| ~ r1(X0,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_15867,plain,
! [X0: $i] :
( p2(sK96(sK224))
| ~ sP84(X0)
| ~ p2(sK99(sK96(sK224)))
| ~ r1(X0,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_15868,plain,
! [X0: $i] :
( p2(sK96(sK224))
| r1(sK96(sK224),sK98(sK96(sK224)))
| ~ sP84(X0)
| ~ r1(X0,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_15873,plain,
! [X0: $i] :
( p2(sK96(sK224))
| p2(sK98(sK96(sK224)))
| ~ sP84(X0)
| ~ r1(X0,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_16195,plain,
! [X0: $i,X1: $i] :
( sP86(sK213)
| p2(X1)
| sP82(sK96(sK224))
| sP83(sK96(sK224))
| ~ sP84(sK224)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK96(sK224),X0) ),
inference(resolution,[status(thm)],[c_602,c_67]) ).
tcf(c_16335,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK95(sK250(sK214)))
| ~ p2(X0)
| ~ r1(sK213,X1)
| ~ r1(sK250(X1),X0)
| ~ r1(X0,sK95(sK250(sK214))) ),
inference(instantiation,[status(thm)],[c_711]) ).
tcf(c_16443,plain,
! [X0: $i] :
( p2(sK224)
| p2(X0)
| ~ iPr_def_15
| ~ iPr_def_10
| ~ p2(sK215(sK224))
| ~ r1(sK213,sK224)
| ~ r1(sK215(sK224),X0) ),
inference(resolution,[status(thm)],[c_13816,c_13825]) ).
tcf(c_16660,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| r1(sK91(X0),sK89(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(superposition,[status(thm)],[c_56,c_52]) ).
tcf(c_16714,plain,
( p2(sK96(sK224))
| ~ sP84(sK224)
| ~ p2(sK99(sK96(sK224)))
| ~ r1(sK224,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_16814,plain,
( sP86(sK213)
| p2(sK224)
| ~ sP87(sK213)
| ~ p2(sK90(sK224)) ),
inference(superposition,[status(thm)],[c_598,c_54]) ).
tcf(c_17031,plain,
! [X0: $i] :
( p2(X0)
| p2(sK250(X0))
| r1(sK250(X0),sK98(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(superposition,[status(thm)],[c_709,c_71]) ).
tcf(c_17091,plain,
! [X0: $i,X1: $i] :
( p2(sK88(X0))
| p2(sK95(sK250(sK88(X1))))
| ~ r1(sK213,sK88(X0))
| ~ p2(sK94(sK250(sK88(X0))))
| ~ r1(sK250(sK88(X0)),sK94(sK250(sK88(X0))))
| ~ r1(sK94(sK250(sK88(X0))),sK95(sK250(sK88(X1)))) ),
inference(instantiation,[status(thm)],[c_15038]) ).
tcf(c_17092,plain,
( p2(sK88(sK213))
| p2(sK95(sK250(sK88(sK213))))
| ~ r1(sK213,sK88(sK213))
| ~ p2(sK94(sK250(sK88(sK213))))
| ~ r1(sK250(sK88(sK213)),sK94(sK250(sK88(sK213))))
| ~ r1(sK94(sK250(sK88(sK213))),sK95(sK250(sK88(sK213)))) ),
inference(instantiation,[status(thm)],[c_17091]) ).
tcf(c_17122,plain,
( p2(sK96(sK224))
| r1(sK98(sK96(sK224)),sK99(sK96(sK224)))
| ~ sP84(sK224)
| ~ r1(sK224,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_15861]) ).
tcf(c_17130,plain,
( p2(sK96(sK224))
| r1(sK96(sK224),sK98(sK96(sK224)))
| ~ sP84(sK224)
| ~ r1(sK224,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_15868]) ).
tcf(c_17136,plain,
( p2(sK96(sK224))
| p2(sK98(sK96(sK224)))
| ~ sP84(sK224)
| ~ r1(sK224,sK96(sK224)) ),
inference(instantiation,[status(thm)],[c_15873]) ).
tcf(c_17316,plain,
( sP86(sK213)
| p2(sK224)
| r1(sK224,sK89(sK224))
| ~ sP87(sK213) ),
inference(resolution,[status(thm)],[c_52,c_598]) ).
tcf(c_17361,plain,
! [X0: $i] :
( p2(X0)
| p2(sK250(X0))
| ~ sP84(X0)
| ~ r1(sK213,X0)
| ~ p2(sK99(sK250(X0))) ),
inference(superposition,[status(thm)],[c_709,c_73]) ).
tcf(c_17878,plain,
( r1(sK96(sK224),sK97(sK224))
| ~ sP84(sK224) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_17962,plain,
! [X0: $i] :
( p2(X0)
| p2(sK250(X0))
| r1(sK250(X0),sK98(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(resolution,[status(thm)],[c_71,c_709]) ).
tcf(c_18326,plain,
( p2(sK97(sK224))
| p2(sK101(sK97(sK224)))
| ~ sP83(sK96(sK224))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13999]) ).
tcf(c_18327,plain,
( p2(sK97(sK224))
| r1(sK97(sK224),sK101(sK97(sK224)))
| ~ sP83(sK96(sK224))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13993]) ).
tcf(c_18328,plain,
( p2(sK97(sK224))
| r1(sK101(sK97(sK224)),sK102(sK97(sK224)))
| ~ sP83(sK96(sK224))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13987]) ).
tcf(c_18334,plain,
( p2(sK97(sK224))
| ~ sP83(sK96(sK224))
| ~ p2(sK102(sK97(sK224)))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13992]) ).
tcf(c_18666,plain,
! [X0: $i] :
( sP86(sK213)
| p2(sK224)
| p2(X0)
| ~ iPr_def_15
| ~ sP87(sK213)
| ~ p2(sK89(sK224))
| ~ r1(sK89(sK224),X0) ),
inference(resolution,[status(thm)],[c_17316,c_13825]) ).
tcf(c_18943,plain,
! [X0: $i,X1: $i] :
( p2(sK102(sK97(sK224)))
| ~ sP84(X1)
| ~ p2(X0)
| ~ r1(sK97(X1),X0)
| ~ r1(X0,sK102(sK97(sK224))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_19384,plain,
! [X0: $i,X1: $i] :
( sP86(sK213)
| sP82(X1)
| sP83(X1)
| p2(sK99(sK96(sK224)))
| ~ p2(X0)
| ~ r1(sK224,X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK99(sK96(sK224))) ),
inference(instantiation,[status(thm)],[c_602]) ).
tcf(c_20085,plain,
( sP86(sK213)
| p2(sK224)
| r1(sK89(sK224),sK90(sK224))
| ~ sP87(sK213) ),
inference(resolution,[status(thm)],[c_53,c_598]) ).
tcf(c_20681,plain,
! [X0: $i] :
( p2(X0)
| p2(sK250(X0))
| r1(sK98(sK250(X0)),sK99(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(resolution,[status(thm)],[c_72,c_709]) ).
tcf(c_21077,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| r1(sK89(sK91(X0)),sK90(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(superposition,[status(thm)],[c_56,c_53]) ).
tcf(c_21362,plain,
( p2(sK88(sK213))
| ~ sP87(sK213)
| ~ p2(sK250(sK88(sK213))) ),
inference(superposition,[status(thm)],[c_50,c_710]) ).
tcf(c_22001,plain,
! [X0: $i] :
( sP86(sK213)
| sP82(X0)
| sP83(X0)
| p2(sK99(sK96(sK224)))
| ~ r1(sK224,X0)
| ~ p2(sK98(sK96(sK224)))
| ~ r1(X0,sK98(sK96(sK224)))
| ~ r1(sK98(sK96(sK224)),sK99(sK96(sK224))) ),
inference(instantiation,[status(thm)],[c_19384]) ).
tcf(c_23497,plain,
( sP86(sK213)
| sP82(sK96(sK224))
| sP83(sK96(sK224))
| p2(sK99(sK96(sK224)))
| ~ p2(sK98(sK96(sK224)))
| ~ r1(sK224,sK96(sK224))
| ~ r1(sK96(sK224),sK98(sK96(sK224)))
| ~ r1(sK98(sK96(sK224)),sK99(sK96(sK224))) ),
inference(instantiation,[status(thm)],[c_22001]) ).
tcf(c_24167,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK213,X0)
| ~ sP84(X0)
| r1(sK250(X0),sK98(sK250(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_17962,c_710,c_17031]) ).
tcf(c_24168,plain,
! [X0: $i] :
( p2(X0)
| r1(sK250(X0),sK98(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(renaming,[status(thm)],[c_24167]) ).
tcf(c_24204,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP84(X0)
| ~ r1(sK213,X0)
| ~ p2(sK98(sK250(X0)))
| ~ r1(sK98(sK250(X0)),X1) ),
inference(resolution,[status(thm)],[c_24168,c_711]) ).
tcf(c_25388,plain,
( p2(sK97(sK224))
| p2(sK105(sK97(sK224)))
| ~ sP82(sK96(sK224))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13998]) ).
tcf(c_25389,plain,
( p2(sK97(sK224))
| r1(sK97(sK224),sK105(sK97(sK224)))
| ~ sP82(sK96(sK224))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13991]) ).
tcf(c_25390,plain,
( p2(sK97(sK224))
| r1(sK105(sK97(sK224)),sK106(sK97(sK224)))
| ~ sP82(sK96(sK224))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13986]) ).
tcf(c_25398,plain,
( p2(sK97(sK224))
| ~ sP82(sK96(sK224))
| ~ p2(sK106(sK97(sK224)))
| ~ r1(sK96(sK224),sK97(sK224)) ),
inference(instantiation,[status(thm)],[c_13990]) ).
tcf(c_26202,plain,
! [X0: $i,X1: $i] :
( p2(sK106(sK97(sK224)))
| ~ sP84(X1)
| ~ p2(X0)
| ~ r1(sK97(X1),X0)
| ~ r1(X0,sK106(sK97(sK224))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_27340,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK213,X0)
| ~ sP84(X0)
| r1(sK98(sK250(X0)),sK99(sK250(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_20681,c_710,c_20681]) ).
tcf(c_27341,plain,
! [X0: $i] :
( p2(X0)
| r1(sK98(sK250(X0)),sK99(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(renaming,[status(thm)],[c_27340]) ).
tcf(c_28191,plain,
( ~ p2(sK250(sK88(sK213)))
| ~ sP87(sK213) ),
inference(global_subsumption_just,[status(thm)],[c_21362,c_1073,c_14701]) ).
tcf(c_28192,plain,
( ~ sP87(sK213)
| ~ p2(sK250(sK88(sK213))) ),
inference(renaming,[status(thm)],[c_28191]) ).
tcf(c_28623,plain,
! [X0: $i] :
( p2(sK106(sK97(sK224)))
| ~ sP84(X0)
| ~ p2(sK105(sK97(sK224)))
| ~ r1(sK97(X0),sK105(sK97(sK224)))
| ~ r1(sK105(sK97(sK224)),sK106(sK97(sK224))) ),
inference(instantiation,[status(thm)],[c_26202]) ).
tcf(c_28791,plain,
! [X0: $i] :
( sP86(sK213)
| p2(sK224)
| p2(X0)
| ~ iPr_def_15
| ~ sP87(sK213)
| ~ r1(sK89(sK224),X0) ),
inference(global_subsumption_just,[status(thm)],[c_18666,c_15610,c_18666]) ).
tcf(c_28823,plain,
( sP86(sK213)
| p2(sK224)
| p3(sK89(sK224))
| p2(sK218(sK89(sK224)))
| ~ iPr_def_15
| ~ sP87(sK213)
| ~ r1(sK213,sK89(sK224)) ),
inference(resolution,[status(thm)],[c_28791,c_586]) ).
tcf(c_28827,plain,
( sP86(sK213)
| p2(sK224)
| p2(sK90(sK224))
| ~ iPr_def_15
| ~ sP87(sK213) ),
inference(resolution,[status(thm)],[c_28791,c_20085]) ).
tcf(c_29801,plain,
( p2(sK106(sK97(sK224)))
| ~ sP84(sK224)
| ~ p2(sK105(sK97(sK224)))
| ~ r1(sK97(sK224),sK105(sK97(sK224)))
| ~ r1(sK105(sK97(sK224)),sK106(sK97(sK224))) ),
inference(instantiation,[status(thm)],[c_28623]) ).
tcf(c_30038,plain,
( p2(sK224)
| p2(sK216(sK224))
| ~ iPr_def_15
| ~ iPr_def_12
| ~ iPr_def_10
| ~ p2(sK215(sK224))
| ~ r1(sK213,sK224) ),
inference(resolution,[status(thm)],[c_16443,c_13819]) ).
tcf(c_31598,plain,
( sP86(sK213)
| p2(sK224)
| ~ iPr_def_15
| ~ sP87(sK213) ),
inference(global_subsumption_just,[status(thm)],[c_28823,c_16814,c_28827]) ).
tcf(c_31628,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| p2(sK89(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(resolution,[status(thm)],[c_56,c_55]) ).
tcf(c_31630,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| r1(sK91(X0),sK89(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(resolution,[status(thm)],[c_56,c_52]) ).
tcf(c_31634,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| r1(sK89(sK91(X0)),sK90(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(resolution,[status(thm)],[c_56,c_53]) ).
tcf(c_32220,plain,
! [X0: $i,X1: $i] :
( sP85(X0)
| p2(X1)
| p2(sK91(X0))
| ~ iPr_def_10
| ~ sP86(X0)
| ~ p2(sK215(sK91(X0)))
| ~ r1(sK213,sK91(X0))
| ~ r1(sK215(sK91(X0)),X1) ),
inference(resolution,[status(thm)],[c_58,c_13816]) ).
tcf(c_32475,plain,
( p2(sK102(sK97(sK224)))
| ~ sP84(sK224)
| ~ p2(sK101(sK97(sK224)))
| ~ r1(sK97(sK224),sK101(sK97(sK224)))
| ~ r1(sK101(sK97(sK224)),sK102(sK97(sK224))) ),
inference(instantiation,[status(thm)],[c_18943]) ).
tcf(c_32866,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP84(X0)
| ~ r1(sK213,X0)
| ~ r1(sK98(sK250(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_24204,c_710,c_15812,c_24204]) ).
tcf(c_32903,plain,
! [X0: $i] :
( sP87(sK213)
| p2(X0)
| p2(sK220(sK98(sK250(X0))))
| ~ sP84(X0)
| ~ r1(sK213,X0)
| ~ r1(sK213,sK98(sK250(X0))) ),
inference(resolution,[status(thm)],[c_32866,c_590]) ).
tcf(c_32911,plain,
! [X0: $i] :
( p2(X0)
| p2(sK99(sK250(X0)))
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(resolution,[status(thm)],[c_32866,c_27341]) ).
tcf(c_33408,plain,
! [X0: $i] :
( p2(X0)
| p2(sK95(sK250(sK214)))
| ~ r1(sK213,X0)
| ~ p2(sK94(sK250(sK214)))
| ~ r1(sK250(X0),sK94(sK250(sK214)))
| ~ r1(sK94(sK250(sK214)),sK95(sK250(sK214))) ),
inference(instantiation,[status(thm)],[c_16335]) ).
tcf(c_33613,plain,
! [X0: $i] :
( ~ sP84(X0)
| ~ r1(sK213,X0)
| p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_32903,c_710,c_17361,c_32911]) ).
tcf(c_33614,plain,
! [X0: $i] :
( p2(X0)
| ~ sP84(X0)
| ~ r1(sK213,X0) ),
inference(renaming,[status(thm)],[c_33613]) ).
tcf(c_33641,plain,
( sP86(sK213)
| p2(sK224)
| ~ sP84(sK224) ),
inference(resolution,[status(thm)],[c_33614,c_598]) ).
tcf(c_33660,plain,
( iPr_def_15
| sP86(sK213)
| p2(sK224) ),
inference(resolution,[status(thm)],[c_33641,c_13826]) ).
tcf(c_33667,plain,
( sP86(sK213)
| p2(sK224)
| ~ sP87(sK213) ),
inference(backward_subsumption_resolution,[status(thm)],[c_31598,c_33660]) ).
tcf(c_34263,plain,
( sP86(sK213)
| ~ sP84(sK224)
| sP83(sK96(sK224))
| sP82(sK96(sK224)) ),
inference(global_subsumption_just,[status(thm)],[c_16195,c_14233,c_14807,c_16714,c_17122,c_17130,c_17136,c_23497]) ).
tcf(c_34264,plain,
( sP86(sK213)
| sP82(sK96(sK224))
| sP83(sK96(sK224))
| ~ sP84(sK224) ),
inference(renaming,[status(thm)],[c_34263]) ).
tcf(c_34265,plain,
( sP86(sK213)
| sP82(sK96(sK224))
| ~ sP84(sK224) ),
inference(global_subsumption_just,[status(thm)],[c_34264,c_13886,c_17878,c_18334,c_18328,c_18327,c_18326,c_25398,c_25390,c_25389,c_25388,c_29801,c_32475,c_34264]) ).
tcf(c_34267,plain,
( sP86(sK213)
| ~ sP84(sK224) ),
inference(global_subsumption_just,[status(thm)],[c_34265,c_13886,c_17878,c_25398,c_25390,c_25389,c_25388,c_29801,c_34265]) ).
tcf(c_34276,plain,
( iPr_def_15
| sP86(sK213) ),
inference(backward_subsumption_resolution,[status(thm)],[c_13826,c_34267]) ).
tcf(c_34277,plain,
( sP86(sK213)
| ~ p2(sK224) ),
inference(backward_subsumption_resolution,[status(thm)],[c_599,c_34267]) ).
tcf(c_34297,plain,
( sP86(sK213)
| ~ sP87(sK213) ),
inference(backward_subsumption_resolution,[status(thm)],[c_33667,c_34277]) ).
tcf(c_34301,plain,
( sP86(sK213)
| p2(sK215(sK224))
| ~ iPr_def_14 ),
inference(backward_subsumption_resolution,[status(thm)],[c_15462,c_34277]) ).
tcf(c_34645,plain,
! [X0: $i] :
( sP85(X0)
| ~ sP87(X0)
| ~ sP86(X0)
| p2(sK89(sK91(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_31628,c_57,c_15595]) ).
tcf(c_34646,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK89(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(renaming,[status(thm)],[c_34645]) ).
tcf(c_35854,plain,
( sP86(sK213)
| p2(sK215(sK224)) ),
inference(global_subsumption_just,[status(thm)],[c_34301,c_14523,c_15462,c_34277,c_34297]) ).
tcf(c_36047,plain,
! [X0: $i] :
( sP85(X0)
| ~ sP87(X0)
| ~ sP86(X0)
| r1(sK91(X0),sK89(sK91(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_31630,c_57,c_16660]) ).
tcf(c_36048,plain,
! [X0: $i] :
( sP85(X0)
| r1(sK91(X0),sK89(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(renaming,[status(thm)],[c_36047]) ).
tcf(c_36264,plain,
! [X0: $i] :
( sP85(X0)
| ~ sP87(X0)
| ~ sP86(X0)
| r1(sK89(sK91(X0)),sK90(sK91(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_31634,c_57,c_21077]) ).
tcf(c_36265,plain,
! [X0: $i] :
( sP85(X0)
| r1(sK89(sK91(X0)),sK90(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(renaming,[status(thm)],[c_36264]) ).
tcf(c_37251,plain,
( sP86(sK213)
| p2(sK224)
| p2(sK216(sK224))
| ~ iPr_def_15
| ~ iPr_def_12
| ~ iPr_def_10
| ~ p2(sK215(sK224)) ),
inference(resolution,[status(thm)],[c_30038,c_598]) ).
tcf(c_37252,plain,
( sP86(sK213)
| p2(sK216(sK224)) ),
inference(global_subsumption_just,[status(thm)],[c_37251,c_14518,c_14519,c_34277,c_34276,c_34297,c_35854,c_37251]) ).
tcf(c_37283,plain,
( sP86(sK213)
| p2(sK224)
| ~ iPr_def_13
| ~ p2(sK216(sK224)) ),
inference(resolution,[status(thm)],[c_13821,c_598]) ).
tcf(c_37300,plain,
sP86(sK213),
inference(global_subsumption_just,[status(thm)],[c_37283,c_14521,c_34277,c_34297,c_37252,c_37283]) ).
tcf(c_37547,plain,
! [X0: $i,X1: $i] :
( sP85(X0)
| p2(X1)
| ~ sP86(X0)
| ~ sP87(X0)
| ~ p2(sK89(sK91(X0)))
| ~ r1(sK89(sK91(X0)),X1) ),
inference(resolution,[status(thm)],[c_36048,c_58]) ).
tcf(c_39092,plain,
! [X0: $i,X1: $i] :
( sP85(X0)
| p2(X1)
| ~ r1(sK215(sK91(X0)),X1)
| ~ r1(sK213,sK91(X0))
| ~ p2(sK215(sK91(X0)))
| ~ sP86(X0)
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_32220,c_57,c_32220]) ).
tcf(c_39093,plain,
! [X0: $i,X1: $i] :
( sP85(X0)
| p2(X1)
| ~ iPr_def_10
| ~ sP86(X0)
| ~ p2(sK215(sK91(X0)))
| ~ r1(sK213,sK91(X0))
| ~ r1(sK215(sK91(X0)),X1) ),
inference(renaming,[status(thm)],[c_39092]) ).
tcf(c_39133,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK91(X0))
| p2(sK216(sK91(X0)))
| ~ iPr_def_12
| ~ iPr_def_10
| ~ sP86(X0)
| ~ p2(sK215(sK91(X0)))
| ~ r1(sK213,sK91(X0)) ),
inference(resolution,[status(thm)],[c_39093,c_13819]) ).
tcf(c_39137,plain,
! [X0: $i] :
( sP87(sK213)
| sP85(X0)
| p2(sK220(sK215(sK91(X0))))
| ~ iPr_def_10
| ~ sP86(X0)
| ~ p2(sK215(sK91(X0)))
| ~ r1(sK213,sK91(X0))
| ~ r1(sK213,sK215(sK91(X0))) ),
inference(resolution,[status(thm)],[c_39093,c_590]) ).
tcf(c_39145,plain,
! [X0: $i] :
( sP87(sK213)
| sP85(X0)
| ~ sP86(X0)
| ~ r1(sK213,sK91(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_39137,c_57,c_14518,c_14519,c_14521,c_14523,c_14626,c_14625,c_39133]) ).
tcf(c_39164,plain,
( sP85(sK213)
| sP87(sK213)
| ~ sP86(sK213) ),
inference(resolution,[status(thm)],[c_39145,c_56]) ).
tcf(c_39249,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK94(X1))
| ~ sP85(X0)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_66,c_49]) ).
tcf(c_39372,plain,
! [X0: $i] :
( p2(sK217)
| r1(sK217,sK94(sK217))
| ~ sP85(X0)
| ~ r1(X0,sK213) ),
inference(resolution,[status(thm)],[c_63,c_584]) ).
tcf(c_39895,plain,
! [X0: $i] :
( sP87(sK213)
| p2(sK220(X0))
| p2(sK94(sK220(X0)))
| ~ sP85(X0)
| ~ r1(sK213,X0) ),
inference(resolution,[status(thm)],[c_39249,c_590]) ).
tcf(c_40421,plain,
( p2(sK214)
| p2(sK95(sK250(sK214)))
| ~ r1(sK213,sK214)
| ~ p2(sK94(sK250(sK214)))
| ~ r1(sK250(sK214),sK94(sK250(sK214)))
| ~ r1(sK94(sK250(sK214)),sK95(sK250(sK214))) ),
inference(instantiation,[status(thm)],[c_33408]) ).
tcf(c_41183,plain,
( p2(sK217)
| r1(sK217,sK94(sK217))
| ~ sP85(sK213) ),
inference(resolution,[status(thm)],[c_39372,c_49]) ).
tcf(c_41324,plain,
sP87(sK213),
inference(global_subsumption_just,[status(thm)],[c_39895,c_9574,c_9584,c_14313,c_15022,c_15502,c_15507,c_15512,c_15592,c_37300,c_39164,c_40421]) ).
tcf(c_41869,plain,
~ sP85(sK213),
inference(global_subsumption_just,[status(thm)],[c_41183,c_1073,c_1074,c_13874,c_14926,c_14947,c_14952,c_14957,c_17092,c_28192,c_41324]) ).
tcf(c_45407,plain,
! [X0: $i,X1: $i] :
( sP85(X0)
| p2(X1)
| ~ sP86(X0)
| ~ sP87(X0)
| ~ r1(sK89(sK91(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_37547,c_34646,c_37547]) ).
tcf(c_45450,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK90(sK91(X0)))
| ~ sP86(X0)
| ~ sP87(X0) ),
inference(resolution,[status(thm)],[c_45407,c_36265]) ).
tcf(c_45451,plain,
( sP85(sK213)
| p2(sK90(sK91(sK213)))
| ~ sP86(sK213)
| ~ sP87(sK213) ),
inference(instantiation,[status(thm)],[c_45450]) ).
tcf(c_45452,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_45451,c_41869,c_41324,c_37300,c_14657,c_1115,c_1114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL660+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/10.39 % Computer : n006.cluster.edu
% 0.12/10.39 % Model : x86_64 x86_64
% 0.12/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.39 % Memory : 8046.5625MB
% 0.12/10.39 % OS : Linux 6.8.0-71-generic
% 0.12/10.39 % CPULimit : 300
% 0.12/10.39 % WCLimit : 300
% 0.12/10.39 % DateTime : Thu Sep 24 00:04:38 UTC 2026
% 0.12/10.39 % CPUTime :
% 0.12/10.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/10.43 Running first-order theorem proving
% 0.16/10.43 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.16/10.44
% 0.16/10.44 % ======== iProver multi-core TPTP/SMT =========
% 0.16/10.44
% 0.16/10.45 % Detected problem language: tptp
% 0.16/10.46 % Proving...
% 20.13/14.25 % SZS status Started for theBenchmark.p
% 20.13/14.25 % SZS status Theorem for theBenchmark.p
% 20.13/14.25
% 20.13/14.25 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 20.13/14.25
% 20.13/14.25 % ------ iProver source info
% 20.13/14.25
% 20.13/14.25 % git: date: 2026-07-19 20:42:38 +0200
% 20.13/14.25 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 20.13/14.25 % git: non_committed_changes: false
% 20.13/14.25
% 20.13/14.25 % ------ Parsing...
% 20.13/14.25 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 20.13/14.25
% 20.13/14.25 % ------ Preprocessing... sf_s rm: 592 0s sf_e pe_s pe:1:0s pe_e %
% 20.13/14.25
% 20.13/14.25 % ------ Preprocessing... gs_s sp: 9 0s gs_e snvd_s sp: 0 0s snvd_e
% 20.13/14.25 % ------ Proving...
% 20.13/14.25 % ------ Problem Properties
% 20.13/14.25
% 20.13/14.25 %
% 20.13/14.25 % clauses 76
% 20.13/14.25 % conjectures 20
% 20.13/14.25 % EPR 17
% 20.13/14.25 % Horn 31
% 20.13/14.25 % unary 5
% 20.13/14.25 % binary 11
% 20.13/14.25 % lits 268
% 20.13/14.25 % lits eq 0
% 20.13/14.25 % fd_pure 0
% 20.13/14.25 % fd_pseudo 0
% 20.13/14.25 % fd_cond 0
% 20.13/14.25 % fd_pseudo_cond 0
% 20.13/14.25 % AC symbols 0
% 20.13/14.25
% 20.13/14.25 % ------ Input Options Time Limit: Unbounded
% 20.13/14.25
% 20.13/14.25
% 20.13/14.25 % ------
% 20.13/14.25 % Current options:
% 20.13/14.25 % ------
% 20.13/14.25
% 20.13/14.25
% 20.13/14.25 %
% 20.13/14.25
% 20.13/14.25 % ------ Proving...
% 20.13/14.25 %
% 20.13/14.25
% 20.13/14.25 % SZS status Theorem for theBenchmark.p
% 20.13/14.25
% 20.13/14.25 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 20.13/14.26
%------------------------------------------------------------------------------