%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL642+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 : n001.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:02 PM UTC 2026
% Result : Theorem 6.05s 2.27s
% Output : CNFRefutation 6.05s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f93ERROR: Could not build tree for root c_16173ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f96,plain,
! [X0] :
( ~ sP86(X0)
| ( ( ? [X20] :
( p2(X20)
& ? [X21] :
( ~ p2(X21)
& r1(X20,X21) )
& r1(X0,X20) )
| p2(X0) )
& ( ? [X17] :
( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17)
& r1(X0,X17) )
| sP85(X0) ) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f97,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,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ~ sP86(X0)
| ( ( ( p2(sK88(X0))
& ~ p2(sK89(X0))
& r1(sK88(X0),sK89(X0))
& r1(X0,sK88(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK87(X0),X2) )
& ~ p2(sK87(X0))
& r1(X0,sK87(X0)) )
| sP85(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88,sK89]),skolemize(X1,sK87(X0)),skolemize(X4,sK88(X0)),skolemize(X5,sK89(X0))],[f97]) ).
fof(f99,plain,
! [X0] :
( ~ sP85(X0)
| ! [X13] :
( ! [X14] :
( ? [X15] :
( p2(X15)
& ? [X16] :
( ~ p2(X16)
& r1(X15,X16) )
& r1(X14,X15) )
| p2(X14)
| ~ r1(X13,X14) )
| ~ r1(X0,X13) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f100,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,[],[f99]) ).
fof(f101,plain,
! [X0] :
( ~ sP85(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK90(X2))
& ~ p2(sK91(X2))
& r1(sK90(X2),sK91(X2))
& r1(X2,sK90(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK90,sK91]),skolemize(X3,sK90(X2)),skolemize(X4,sK91(X2))],[f100]) ).
fof(f102,plain,
! [X22] :
( ~ sP84(X22)
| ( ! [X27] :
( ? [X28] :
( p2(X28)
& ? [X29] :
( ~ p2(X29)
& r1(X28,X29) )
& r1(X27,X28) )
| p2(X27)
| ~ r1(X22,X27) )
& ? [X23] :
( ? [X24] :
( ! [X25] :
( ~ p2(X25)
| ! [X26] :
( p2(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
& ~ p2(X24)
& r1(X23,X24) )
& r1(X22,X23) ) ) ),
inference(nnf_transformation,[],[f92]) ).
fof(f103,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,[],[f102]) ).
fof(f104,plain,
! [X0] :
( ~ sP84(X0)
| ( ! [X5] :
( ( p2(sK94(X5))
& ~ p2(sK95(X5))
& r1(sK94(X5),sK95(X5))
& r1(X5,sK94(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK93(X0),X3) )
& ~ p2(sK93(X0))
& r1(sK92(X0),sK93(X0))
& r1(X0,sK92(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92,sK93,sK94,sK95]),skolemize(X1,sK92(X0)),skolemize(X2,sK93(X0)),skolemize(X6,sK94(X5)),skolemize(X7,sK95(X5))],[f103]) ).
fof(f105,plain,
! [X32] :
( ~ sP83(X32)
| ! [X33] :
( ( ( ? [X41] :
( p2(X41)
& ? [X42] :
( ~ p2(X42)
& r1(X41,X42) )
& r1(X33,X41) )
| p2(X33) )
& ( ? [X38] :
( ! [X39] :
( ~ p2(X39)
| ! [X40] :
( p2(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
& ~ p2(X38)
& r1(X33,X38) )
| sP81(X33) ) )
| ~ r1(X32,X33) ) ),
inference(nnf_transformation,[],[f91]) ).
fof(f106,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,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ~ sP83(X0)
| ! [X1] :
( ( ( ( p2(sK97(X1))
& ~ p2(sK98(X1))
& r1(sK97(X1),sK98(X1))
& r1(X1,sK97(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK96(X1),X3) )
& ~ p2(sK96(X1))
& r1(X1,sK96(X1)) )
| sP81(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96,sK97,sK98]),skolemize(X2,sK96(X1)),skolemize(X5,sK97(X1)),skolemize(X6,sK98(X1))],[f106]) ).
fof(f108,plain,
! [X32] :
( ~ sP82(X32)
| ( ! [X47] :
( ? [X48] :
( p2(X48)
& ? [X49] :
( ~ p2(X49)
& r1(X48,X49) )
& r1(X47,X48) )
| p2(X47)
| ~ r1(X32,X47) )
& ? [X43] :
( ? [X44] :
( ! [X45] :
( ~ p2(X45)
| ! [X46] :
( p2(X46)
| ~ r1(X45,X46) )
| ~ r1(X44,X45) )
& ~ p2(X44)
& r1(X43,X44) )
& r1(X32,X43) ) ) ),
inference(nnf_transformation,[],[f90]) ).
fof(f109,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,[],[f108]) ).
fof(f110,plain,
! [X0] :
( ~ sP82(X0)
| ( ! [X5] :
( ( p2(sK101(X5))
& ~ p2(sK102(X5))
& r1(sK101(X5),sK102(X5))
& r1(X5,sK101(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK100(X0),X3) )
& ~ p2(sK100(X0))
& r1(sK99(X0),sK100(X0))
& r1(X0,sK99(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK99,sK100,sK101,sK102]),skolemize(X1,sK99(X0)),skolemize(X2,sK100(X0)),skolemize(X6,sK101(X5)),skolemize(X7,sK102(X5))],[f109]) ).
fof(f350,plain,
? [X0] :
( ! [X105] :
( ? [X106] :
( ! [X107] :
( ~ p2(X107)
| ! [X108] :
( p2(X108)
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
& ~ p2(X106)
& r1(X105,X106) )
| p2(X105)
| ~ r1(X0,X105) )
& ( ? [X99] :
( ! [X101] :
( ( ? [X104] : r1(X101,X104)
& ~ p1(X101) )
| ! [X102] :
( ! [X103] : ~ r1(X102,X103)
| p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X99,X101) )
& ? [X100] : r1(X99,X100)
& ~ p1(X99)
& r1(X0,X99) )
| ! [X98] : ~ r1(X0,X98)
| p1(X0) )
& ( ? [X92] :
( ! [X94] :
( ( ? [X97] : r1(X94,X97)
& ~ p1(X94)
& ~ p2(X94) )
| ! [X95] :
( ! [X96] : ~ r1(X95,X96)
| p1(X95)
| p2(X95)
| ~ r1(X94,X95) )
| ~ r1(X92,X94) )
& ? [X93] : r1(X92,X93)
& ~ p1(X92)
& ~ p2(X92)
& r1(X0,X92) )
| ! [X91] : ~ r1(X0,X91)
| p1(X0)
| p2(X0) )
& ( ? [X89] :
( sP0(X89)
& ? [X90] : r1(X89,X90)
& ~ p1(X89)
& ~ p2(X89)
& ~ p3(X89)
& r1(X0,X89) )
| ! [X88] : ~ r1(X0,X88)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X86] :
( sP1(X86)
& ? [X87] : r1(X86,X87)
& ~ p1(X86)
& ~ p2(X86)
& ~ p3(X86)
& ~ p4(X86)
& r1(X0,X86) )
| ! [X85] : ~ r1(X0,X85)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X84] :
( sP2(X84)
& sP3(X84)
& ~ p1(X84)
& r1(X0,X84) )
| ! [X82] :
( ! [X83] : ~ r1(X82,X83)
| p1(X82)
| p2(X82)
| p3(X82)
| p4(X82)
| ~ r1(X0,X82) )
| p1(X0) )
& ( ? [X81] :
( sP4(X81)
& sP5(X81)
& ~ p1(X81)
& ~ p2(X81)
& r1(X0,X81) )
| ! [X79] :
( ! [X80] : ~ r1(X79,X80)
| p1(X79)
| p2(X79)
| p3(X79)
| p4(X79)
| ~ r1(X0,X79) )
| p1(X0)
| p2(X0) )
& ( ? [X78] :
( sP8(X78)
& sP7(X78)
& ~ p1(X78)
& ~ p2(X78)
& ~ p3(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) )
& ( ? [X75] :
( sP11(X75)
& sP10(X75)
& ~ p1(X75)
& ~ p2(X75)
& ~ p3(X75)
& ~ p4(X75)
& r1(X0,X75) )
| ! [X73] :
( ! [X74] : ~ r1(X73,X74)
| p1(X73)
| p2(X73)
| p3(X73)
| p4(X73)
| ~ r1(X0,X73) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X72] :
( sP14(X72)
& sP15(X72)
& ~ p1(X72)
& r1(X0,X72) )
| ! [X69] :
( ! [X70] :
( ! [X71] : ~ r1(X70,X71)
| p1(X70)
| p2(X70)
| p3(X70)
| p4(X70)
| ~ r1(X69,X70) )
| p1(X69)
| p2(X69)
| p3(X69)
| p4(X69)
| ~ r1(X0,X69) )
| p1(X0) )
& ( ? [X68] :
( sP18(X68)
& sP19(X68)
& ~ p1(X68)
& ~ p2(X68)
& r1(X0,X68) )
| ! [X65] :
( ! [X66] :
( ! [X67] : ~ r1(X66,X67)
| p1(X66)
| p2(X66)
| p3(X66)
| p4(X66)
| ~ r1(X65,X66) )
| p1(X65)
| p2(X65)
| p3(X65)
| p4(X65)
| ~ r1(X0,X65) )
| p1(X0)
| p2(X0) )
& ( ? [X64] :
( sP24(X64)
& sP23(X64)
& ~ p1(X64)
& ~ p2(X64)
& ~ p3(X64)
& r1(X0,X64) )
| ! [X61] :
( ! [X62] :
( ! [X63] : ~ r1(X62,X63)
| p1(X62)
| p2(X62)
| p3(X62)
| p4(X62)
| ~ r1(X61,X62) )
| p1(X61)
| p2(X61)
| p3(X61)
| p4(X61)
| ~ r1(X0,X61) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X60] :
( sP29(X60)
& sP28(X60)
& ~ p1(X60)
& ~ p2(X60)
& ~ p3(X60)
& ~ p4(X60)
& r1(X0,X60) )
| ! [X57] :
( ! [X58] :
( ! [X59] : ~ r1(X58,X59)
| p1(X58)
| p2(X58)
| p3(X58)
| p4(X58)
| ~ r1(X57,X58) )
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(X0,X57) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X56] :
( sP34(X56)
& sP35(X56)
& ~ p1(X56)
& r1(X0,X56) )
| ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] : ~ r1(X54,X55)
| p1(X54)
| p2(X54)
| p3(X54)
| p4(X54)
| ~ r1(X53,X54) )
| p1(X53)
| p2(X53)
| p3(X53)
| p4(X53)
| ~ r1(X52,X53) )
| p1(X52)
| p2(X52)
| p3(X52)
| p4(X52)
| ~ r1(X0,X52) )
| p1(X0) )
& ( ? [X51] :
( sP40(X51)
& sP41(X51)
& ~ p1(X51)
& ~ p2(X51)
& r1(X0,X51) )
| ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] : ~ r1(X49,X50)
| p1(X49)
| p2(X49)
| p3(X49)
| p4(X49)
| ~ r1(X48,X49) )
| p1(X48)
| p2(X48)
| p3(X48)
| p4(X48)
| ~ r1(X47,X48) )
| p1(X47)
| p2(X47)
| p3(X47)
| p4(X47)
| ~ r1(X0,X47) )
| p1(X0)
| p2(X0) )
& ( ? [X46] :
( sP48(X46)
& sP47(X46)
& ~ p1(X46)
& ~ p2(X46)
& ~ p3(X46)
& r1(X0,X46) )
| ! [X42] :
( ! [X43] :
( ! [X44] :
( ! [X45] : ~ r1(X44,X45)
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(X43,X44) )
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43)
| ~ r1(X42,X43) )
| p1(X42)
| p2(X42)
| p3(X42)
| p4(X42)
| ~ r1(X0,X42) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X41] :
( sP55(X41)
& sP54(X41)
& ~ p1(X41)
& ~ p2(X41)
& ~ p3(X41)
& ~ p4(X41)
& r1(X0,X41) )
| ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] : ~ r1(X39,X40)
| p1(X39)
| p2(X39)
| p3(X39)
| p4(X39)
| ~ r1(X38,X39) )
| p1(X38)
| p2(X38)
| p3(X38)
| p4(X38)
| ~ r1(X37,X38) )
| p1(X37)
| p2(X37)
| p3(X37)
| p4(X37)
| ~ r1(X0,X37) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X36] :
( sP62(X36)
& sP63(X36)
& ~ p1(X36)
& r1(X0,X36) )
| ! [X31] :
( ! [X32] :
( ! [X33] :
( ! [X34] :
( ! [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(X31,X32) )
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(X0,X31) )
| p1(X0) )
& ( ? [X30] :
( sP70(X30)
& sP71(X30)
& ~ p1(X30)
& ~ p2(X30)
& r1(X0,X30) )
| ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [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(X25,X26) )
| p1(X25)
| p2(X25)
| p3(X25)
| p4(X25)
| ~ r1(X0,X25) )
| p1(X0)
| p2(X0) )
& ( ? [X24] :
( sP80(X24)
& sP79(X24)
& ~ p1(X24)
& ~ p2(X24)
& ~ p3(X24)
& r1(X0,X24) )
| ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [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(X19,X20) )
| p1(X19)
| p2(X19)
| p3(X19)
| p4(X19)
| ~ r1(X0,X19) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X13] :
( ! [X16] :
( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP82(X16)
| sP83(X16)
| ~ r1(X13,X16) )
& ( ( ! [X14] :
( ~ p2(X14)
| ! [X15] :
( p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
& ~ p2(X13) )
| sP84(X13) )
& r1(X0,X13) )
| sP86(X0) )
& ! [X10] :
( ? [X11] :
( p1(X11)
& ? [X12] :
( ~ p1(X12)
& r1(X11,X12) )
& r1(X10,X11) )
| p1(X10)
| ~ r1(X0,X10) )
& ? [X9] :
( ~ p1(X9)
& r1(X0,X9) )
& ! [X6] :
( ? [X7] :
( p2(X7)
& ? [X8] :
( ~ p2(X8)
& r1(X7,X8) )
& r1(X6,X7) )
| p2(X6)
| ~ r1(X0,X6) )
& ? [X5] :
( ~ p2(X5)
& r1(X0,X5) )
& ! [X2] :
( ? [X3] :
( p3(X3)
& ? [X4] :
( ~ p3(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p3(X2)
| ~ r1(X0,X2) )
& ? [X1] :
( ~ p3(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f95]) ).
fof(f351,plain,
( ! [X105] :
( ( ! [X107] :
( ~ p2(X107)
| ! [X108] :
( p2(X108)
| ~ r1(X107,X108) )
| ~ r1(sK245(X105),X107) )
& ~ p2(sK245(X105))
& r1(X105,sK245(X105)) )
| p2(X105)
| ~ r1(sK209,X105) )
& ( ( ! [X101] :
( ( r1(X101,sK244(X101))
& ~ p1(X101) )
| ! [X102] :
( ! [X103] : ~ r1(X102,X103)
| p1(X102)
| ~ r1(X101,X102) )
| ~ r1(sK242,X101) )
& r1(sK242,sK243)
& ~ p1(sK242)
& r1(sK209,sK242) )
| ! [X98] : ~ r1(sK209,X98)
| p1(sK209) )
& ( ( ! [X94] :
( ( r1(X94,sK241(X94))
& ~ p1(X94)
& ~ p2(X94) )
| ! [X95] :
( ! [X96] : ~ r1(X95,X96)
| p1(X95)
| p2(X95)
| ~ r1(X94,X95) )
| ~ r1(sK239,X94) )
& r1(sK239,sK240)
& ~ p1(sK239)
& ~ p2(sK239)
& r1(sK209,sK239) )
| ! [X91] : ~ r1(sK209,X91)
| p1(sK209)
| p2(sK209) )
& ( ( sP0(sK237)
& r1(sK237,sK238)
& ~ p1(sK237)
& ~ p2(sK237)
& ~ p3(sK237)
& r1(sK209,sK237) )
| ! [X88] : ~ r1(sK209,X88)
| p1(sK209)
| p2(sK209)
| p3(sK209) )
& ( ( sP1(sK235)
& r1(sK235,sK236)
& ~ p1(sK235)
& ~ p2(sK235)
& ~ p3(sK235)
& ~ p4(sK235)
& r1(sK209,sK235) )
| ! [X85] : ~ r1(sK209,X85)
| p1(sK209)
| p2(sK209)
| p3(sK209)
| p4(sK209) )
& ( ( sP2(sK234)
& sP3(sK234)
& ~ p1(sK234)
& r1(sK209,sK234) )
| ! [X82] :
( ! [X83] : ~ r1(X82,X83)
| p1(X82)
| p2(X82)
| p3(X82)
| p4(X82)
| ~ r1(sK209,X82) )
| p1(sK209) )
& ( ( sP4(sK233)
& sP5(sK233)
& ~ p1(sK233)
& ~ p2(sK233)
& r1(sK209,sK233) )
| ! [X79] :
( ! [X80] : ~ r1(X79,X80)
| p1(X79)
| p2(X79)
| p3(X79)
| p4(X79)
| ~ r1(sK209,X79) )
| p1(sK209)
| p2(sK209) )
& ( ( sP8(sK232)
& sP7(sK232)
& ~ p1(sK232)
& ~ p2(sK232)
& ~ p3(sK232)
& r1(sK209,sK232) )
| ! [X76] :
( ! [X77] : ~ r1(X76,X77)
| p1(X76)
| p2(X76)
| p3(X76)
| p4(X76)
| ~ r1(sK209,X76) )
| p1(sK209)
| p2(sK209)
| p3(sK209) )
& ( ( sP11(sK231)
& sP10(sK231)
& ~ p1(sK231)
& ~ p2(sK231)
& ~ p3(sK231)
& ~ p4(sK231)
& r1(sK209,sK231) )
| ! [X73] :
( ! [X74] : ~ r1(X73,X74)
| p1(X73)
| p2(X73)
| p3(X73)
| p4(X73)
| ~ r1(sK209,X73) )
| p1(sK209)
| p2(sK209)
| p3(sK209)
| p4(sK209) )
& ( ( sP14(sK230)
& sP15(sK230)
& ~ p1(sK230)
& r1(sK209,sK230) )
| ! [X69] :
( ! [X70] :
( ! [X71] : ~ r1(X70,X71)
| p1(X70)
| p2(X70)
| p3(X70)
| p4(X70)
| ~ r1(X69,X70) )
| p1(X69)
| p2(X69)
| p3(X69)
| p4(X69)
| ~ r1(sK209,X69) )
| p1(sK209) )
& ( ( sP18(sK229)
& sP19(sK229)
& ~ p1(sK229)
& ~ p2(sK229)
& r1(sK209,sK229) )
| ! [X65] :
( ! [X66] :
( ! [X67] : ~ r1(X66,X67)
| p1(X66)
| p2(X66)
| p3(X66)
| p4(X66)
| ~ r1(X65,X66) )
| p1(X65)
| p2(X65)
| p3(X65)
| p4(X65)
| ~ r1(sK209,X65) )
| p1(sK209)
| p2(sK209) )
& ( ( sP24(sK228)
& sP23(sK228)
& ~ p1(sK228)
& ~ p2(sK228)
& ~ p3(sK228)
& r1(sK209,sK228) )
| ! [X61] :
( ! [X62] :
( ! [X63] : ~ r1(X62,X63)
| p1(X62)
| p2(X62)
| p3(X62)
| p4(X62)
| ~ r1(X61,X62) )
| p1(X61)
| p2(X61)
| p3(X61)
| p4(X61)
| ~ r1(sK209,X61) )
| p1(sK209)
| p2(sK209)
| p3(sK209) )
& ( ( sP29(sK227)
& sP28(sK227)
& ~ p1(sK227)
& ~ p2(sK227)
& ~ p3(sK227)
& ~ p4(sK227)
& r1(sK209,sK227) )
| ! [X57] :
( ! [X58] :
( ! [X59] : ~ r1(X58,X59)
| p1(X58)
| p2(X58)
| p3(X58)
| p4(X58)
| ~ r1(X57,X58) )
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(sK209,X57) )
| p1(sK209)
| p2(sK209)
| p3(sK209)
| p4(sK209) )
& ( ( sP34(sK226)
& sP35(sK226)
& ~ p1(sK226)
& r1(sK209,sK226) )
| ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] : ~ r1(X54,X55)
| p1(X54)
| p2(X54)
| p3(X54)
| p4(X54)
| ~ r1(X53,X54) )
| p1(X53)
| p2(X53)
| p3(X53)
| p4(X53)
| ~ r1(X52,X53) )
| p1(X52)
| p2(X52)
| p3(X52)
| p4(X52)
| ~ r1(sK209,X52) )
| p1(sK209) )
& ( ( sP40(sK225)
& sP41(sK225)
& ~ p1(sK225)
& ~ p2(sK225)
& r1(sK209,sK225) )
| ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] : ~ r1(X49,X50)
| p1(X49)
| p2(X49)
| p3(X49)
| p4(X49)
| ~ r1(X48,X49) )
| p1(X48)
| p2(X48)
| p3(X48)
| p4(X48)
| ~ r1(X47,X48) )
| p1(X47)
| p2(X47)
| p3(X47)
| p4(X47)
| ~ r1(sK209,X47) )
| p1(sK209)
| p2(sK209) )
& ( ( sP48(sK224)
& sP47(sK224)
& ~ p1(sK224)
& ~ p2(sK224)
& ~ p3(sK224)
& r1(sK209,sK224) )
| ! [X42] :
( ! [X43] :
( ! [X44] :
( ! [X45] : ~ r1(X44,X45)
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(X43,X44) )
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43)
| ~ r1(X42,X43) )
| p1(X42)
| p2(X42)
| p3(X42)
| p4(X42)
| ~ r1(sK209,X42) )
| p1(sK209)
| p2(sK209)
| p3(sK209) )
& ( ( sP55(sK223)
& sP54(sK223)
& ~ p1(sK223)
& ~ p2(sK223)
& ~ p3(sK223)
& ~ p4(sK223)
& r1(sK209,sK223) )
| ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] : ~ r1(X39,X40)
| p1(X39)
| p2(X39)
| p3(X39)
| p4(X39)
| ~ r1(X38,X39) )
| p1(X38)
| p2(X38)
| p3(X38)
| p4(X38)
| ~ r1(X37,X38) )
| p1(X37)
| p2(X37)
| p3(X37)
| p4(X37)
| ~ r1(sK209,X37) )
| p1(sK209)
| p2(sK209)
| p3(sK209)
| p4(sK209) )
& ( ( sP62(sK222)
& sP63(sK222)
& ~ p1(sK222)
& r1(sK209,sK222) )
| ! [X31] :
( ! [X32] :
( ! [X33] :
( ! [X34] :
( ! [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(X31,X32) )
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(sK209,X31) )
| p1(sK209) )
& ( ( sP70(sK221)
& sP71(sK221)
& ~ p1(sK221)
& ~ p2(sK221)
& r1(sK209,sK221) )
| ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [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(X25,X26) )
| p1(X25)
| p2(X25)
| p3(X25)
| p4(X25)
| ~ r1(sK209,X25) )
| p1(sK209)
| p2(sK209) )
& ( ( sP80(sK220)
& sP79(sK220)
& ~ p1(sK220)
& ~ p2(sK220)
& ~ p3(sK220)
& r1(sK209,sK220) )
| ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [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(X19,X20) )
| p1(X19)
| p2(X19)
| p3(X19)
| p4(X19)
| ~ r1(sK209,X19) )
| p1(sK209)
| p2(sK209)
| p3(sK209) )
& ( ( ! [X16] :
( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP82(X16)
| sP83(X16)
| ~ r1(sK219,X16) )
& ( ( ! [X14] :
( ~ p2(X14)
| ! [X15] :
( p2(X15)
| ~ r1(X14,X15) )
| ~ r1(sK219,X14) )
& ~ p2(sK219) )
| sP84(sK219) )
& r1(sK209,sK219) )
| sP86(sK209) )
& ! [X10] :
( ( p1(sK217(X10))
& ~ p1(sK218(X10))
& r1(sK217(X10),sK218(X10))
& r1(X10,sK217(X10)) )
| p1(X10)
| ~ r1(sK209,X10) )
& ~ p1(sK216)
& r1(sK209,sK216)
& ! [X6] :
( ( p2(sK214(X6))
& ~ p2(sK215(X6))
& r1(sK214(X6),sK215(X6))
& r1(X6,sK214(X6)) )
| p2(X6)
| ~ r1(sK209,X6) )
& ~ p2(sK213)
& r1(sK209,sK213)
& ! [X2] :
( ( p3(sK211(X2))
& ~ p3(sK212(X2))
& r1(sK211(X2),sK212(X2))
& r1(X2,sK211(X2)) )
| p3(X2)
| ~ r1(sK209,X2) )
& ~ p3(sK210)
& r1(sK209,sK210) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK209,sK210,sK211,sK212,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]),skolemize(X0,sK209),skolemize(X1,sK210),skolemize(X3,sK211(X2)),skolemize(X4,sK212(X2)),skolemize(X5,sK213),skolemize(X7,sK214(X6)),skolemize(X8,sK215(X6)),skolemize(X9,sK216),skolemize(X11,sK217(X10)),skolemize(X12,sK218(X10)),skolemize(X13,sK219),skolemize(X24,sK220),skolemize(X30,sK221),skolemize(X36,sK222),skolemize(X41,sK223),skolemize(X46,sK224),skolemize(X51,sK225),skolemize(X56,sK226),skolemize(X60,sK227),skolemize(X64,sK228),skolemize(X68,sK229),skolemize(X72,sK230),skolemize(X75,sK231),skolemize(X78,sK232),skolemize(X81,sK233),skolemize(X84,sK234),skolemize(X86,sK235),skolemize(X87,sK236),skolemize(X89,sK237),skolemize(X90,sK238),skolemize(X92,sK239),skolemize(X93,sK240),skolemize(X97,sK241(X94)),skolemize(X99,sK242),skolemize(X100,sK243),skolemize(X104,sK244(X101)),skolemize(X106,sK245(X105))],[f350]) ).
fof(f356,plain,
! [X2,X3,X0] :
( ~ sP86(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK87(X0),X2)
| sP85(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f357,plain,
! [X0] :
( ~ sP86(X0)
| ~ p2(sK87(X0))
| sP85(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f358,plain,
! [X0] :
( ~ sP86(X0)
| r1(X0,sK87(X0))
| sP85(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f359,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| p2(sK90(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f360,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| ~ p2(sK91(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f361,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| r1(sK90(X2),sK91(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f362,plain,
! [X2,X0,X1] :
( ~ sP85(X0)
| r1(X2,sK90(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f363,plain,
! [X0,X5] :
( ~ sP84(X0)
| p2(sK94(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f104]) ).
fof(f364,plain,
! [X0,X5] :
( ~ sP84(X0)
| ~ p2(sK95(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f104]) ).
fof(f365,plain,
! [X0,X5] :
( ~ sP84(X0)
| r1(sK94(X5),sK95(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f104]) ).
fof(f366,plain,
! [X0,X5] :
( ~ sP84(X0)
| r1(X5,sK94(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f104]) ).
fof(f367,plain,
! [X3,X0,X4] :
( ~ sP84(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK93(X0),X3) ),
inference(cnf_transformation,[],[f104]) ).
fof(f368,plain,
! [X0] :
( ~ sP84(X0)
| ~ p2(sK93(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f369,plain,
! [X0] :
( ~ sP84(X0)
| r1(sK92(X0),sK93(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f370,plain,
! [X0] :
( ~ sP84(X0)
| r1(X0,sK92(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f371,plain,
! [X0,X1] :
( ~ sP83(X0)
| p2(sK97(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f372,plain,
! [X0,X1] :
( ~ sP83(X0)
| ~ p2(sK98(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f373,plain,
! [X0,X1] :
( ~ sP83(X0)
| r1(sK97(X1),sK98(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f374,plain,
! [X0,X1] :
( ~ sP83(X0)
| r1(X1,sK97(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f378,plain,
! [X0,X5] :
( ~ sP82(X0)
| p2(sK101(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f110]) ).
fof(f379,plain,
! [X0,X5] :
( ~ sP82(X0)
| ~ p2(sK102(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f110]) ).
fof(f380,plain,
! [X0,X5] :
( ~ sP82(X0)
| r1(sK101(X5),sK102(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f110]) ).
fof(f381,plain,
! [X0,X5] :
( ~ sP82(X0)
| r1(X5,sK101(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f110]) ).
fof(f874,plain,
! [X108,X107,X105] :
( ~ p2(X107)
| p2(X108)
| ~ r1(X107,X108)
| ~ r1(sK245(X105),X107)
| p2(X105)
| ~ r1(sK209,X105) ),
inference(cnf_transformation,[],[f351]) ).
fof(f875,plain,
! [X105] :
( ~ p2(sK245(X105))
| p2(X105)
| ~ r1(sK209,X105) ),
inference(cnf_transformation,[],[f351]) ).
fof(f876,plain,
! [X105] :
( r1(X105,sK245(X105))
| p2(X105)
| ~ r1(sK209,X105) ),
inference(cnf_transformation,[],[f351]) ).
fof(f983,plain,
! [X18,X16,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP82(X16)
| sP83(X16)
| ~ r1(sK219,X16)
| sP86(sK209) ),
inference(cnf_transformation,[],[f351]) ).
fof(f984,plain,
! [X16] :
( ~ p2(X16)
| sP82(X16)
| sP83(X16)
| ~ r1(sK219,X16)
| sP86(sK209) ),
inference(cnf_transformation,[],[f351]) ).
fof(f985,plain,
! [X14,X15] :
( ~ p2(X14)
| p2(X15)
| ~ r1(X14,X15)
| ~ r1(sK219,X14)
| sP84(sK219)
| sP86(sK209) ),
inference(cnf_transformation,[],[f351]) ).
fof(f986,plain,
( ~ p2(sK219)
| sP84(sK219)
| sP86(sK209) ),
inference(cnf_transformation,[],[f351]) ).
fof(f987,plain,
( r1(sK209,sK219)
| sP86(sK209) ),
inference(cnf_transformation,[],[f351]) ).
fof(f994,plain,
! [X6] :
( p2(sK214(X6))
| p2(X6)
| ~ r1(sK209,X6) ),
inference(cnf_transformation,[],[f351]) ).
fof(f995,plain,
! [X6] :
( ~ p2(sK215(X6))
| p2(X6)
| ~ r1(sK209,X6) ),
inference(cnf_transformation,[],[f351]) ).
fof(f996,plain,
! [X6] :
( r1(sK214(X6),sK215(X6))
| p2(X6)
| ~ r1(sK209,X6) ),
inference(cnf_transformation,[],[f351]) ).
fof(f997,plain,
! [X6] :
( r1(X6,sK214(X6))
| p2(X6)
| ~ r1(sK209,X6) ),
inference(cnf_transformation,[],[f351]) ).
fof(f998,plain,
~ p2(sK213),
inference(cnf_transformation,[],[f351]) ).
fof(f999,plain,
r1(sK209,sK213),
inference(cnf_transformation,[],[f351]) ).
tcf(c_49,plain,
! [X0: $i] :
( sP85(X0)
| r1(X0,sK87(X0))
| ~ sP86(X0) ),
inference(cnf_transformation,[],[f358]) ).
tcf(c_50,plain,
! [X0: $i] :
( sP85(X0)
| ~ sP86(X0)
| ~ p2(sK87(X0)) ),
inference(cnf_transformation,[],[f357]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| sP85(X0)
| ~ p2(X1)
| ~ sP86(X0)
| ~ r1(X1,X2)
| ~ r1(sK87(X0),X1) ),
inference(cnf_transformation,[],[f356]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK90(X2))
| ~ sP85(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK90(X2),sK91(X2))
| ~ sP85(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP85(X0)
| ~ p2(sK91(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK90(X2))
| ~ sP85(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f359]) ).
tcf(c_60,plain,
! [X0: $i] :
( r1(X0,sK92(X0))
| ~ sP84(X0) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_61,plain,
! [X0: $i] :
( r1(sK92(X0),sK93(X0))
| ~ sP84(X0) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_62,plain,
! [X0: $i] :
( ~ sP84(X0)
| ~ p2(sK93(X0)) ),
inference(cnf_transformation,[],[f368]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP84(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK93(X0),X1) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK94(X1))
| ~ sP84(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f366]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK94(X1),sK95(X1))
| ~ sP84(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f365]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP84(X0)
| ~ p2(sK95(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f364]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK94(X1))
| ~ sP84(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK97(X1))
| ~ sP83(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK97(X1),sK98(X1))
| ~ sP83(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f373]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP83(X0)
| ~ p2(sK98(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK97(X1))
| ~ sP83(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK101(X1))
| ~ sP82(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f381]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK101(X1),sK102(X1))
| ~ sP82(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f380]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP82(X0)
| ~ p2(sK102(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f379]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK101(X1))
| ~ sP82(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_577,negated_conjecture,
r1(sK209,sK213),
inference(cnf_transformation,[],[f999]) ).
tcf(c_578,negated_conjecture,
~ p2(sK213),
inference(cnf_transformation,[],[f998]) ).
tcf(c_579,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK214(X0))
| ~ r1(sK209,X0) ),
inference(cnf_transformation,[],[f997]) ).
tcf(c_580,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(sK214(X0),sK215(X0))
| ~ r1(sK209,X0) ),
inference(cnf_transformation,[],[f996]) ).
tcf(c_581,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK215(X0))
| ~ r1(sK209,X0) ),
inference(cnf_transformation,[],[f995]) ).
tcf(c_582,negated_conjecture,
! [X0: $i] :
( p2(X0)
| p2(sK214(X0))
| ~ r1(sK209,X0) ),
inference(cnf_transformation,[],[f994]) ).
tcf(c_589,negated_conjecture,
( sP86(sK209)
| r1(sK209,sK219) ),
inference(cnf_transformation,[],[f987]) ).
tcf(c_590,negated_conjecture,
( sP84(sK219)
| sP86(sK209)
| ~ p2(sK219) ),
inference(cnf_transformation,[],[f986]) ).
tcf(c_591,negated_conjecture,
! [X0: $i,X1: $i] :
( sP84(sK219)
| sP86(sK209)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK219,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f985]) ).
tcf(c_592,negated_conjecture,
! [X0: $i] :
( sP86(sK209)
| sP82(X0)
| sP83(X0)
| ~ p2(X0)
| ~ r1(sK219,X0) ),
inference(cnf_transformation,[],[f984]) ).
tcf(c_593,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP86(sK209)
| sP82(X0)
| sP83(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK219,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f983]) ).
tcf(c_700,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK245(X0))
| ~ r1(sK209,X0) ),
inference(cnf_transformation,[],[f876]) ).
tcf(c_701,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK245(X0))
| ~ r1(sK209,X0) ),
inference(cnf_transformation,[],[f875]) ).
tcf(c_702,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK209,X0)
| ~ r1(X1,X2)
| ~ r1(sK245(X0),X1) ),
inference(cnf_transformation,[],[f874]) ).
tcf(c_1102,plain,
( sP85(sK209)
| ~ sP86(sK209)
| ~ p2(sK87(sK209)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_1103,plain,
( sP85(sK209)
| r1(sK209,sK87(sK209))
| ~ sP86(sK209) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_12962,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| p2(X1)
| ~ p2(X0)
| ~ r1(sK219,X0)
| ~ r1(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_591]) ).
tcf(c_12963,negated_conjecture,
( iPr_def_10
| sP84(sK219)
| sP86(sK209) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_591]) ).
tcf(c_12972,plain,
( p2(sK213)
| r1(sK213,sK245(sK213))
| ~ r1(sK209,sK213) ),
inference(instantiation,[status(thm)],[c_700]) ).
tcf(c_12991,plain,
( p2(sK219)
| p2(sK214(sK219))
| ~ r1(sK209,sK219) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_13101,plain,
( p2(sK87(sK209))
| r1(sK87(sK209),sK214(sK87(sK209)))
| ~ r1(sK209,sK87(sK209)) ),
inference(instantiation,[status(thm)],[c_579]) ).
tcf(c_13115,plain,
! [X0: $i] :
( p2(X0)
| p2(sK94(X0))
| ~ sP84(sK219)
| ~ r1(sK219,X0) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_13117,plain,
! [X0: $i] :
( p2(X0)
| r1(sK94(X0),sK95(X0))
| ~ sP84(sK219)
| ~ r1(sK219,X0) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_13118,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK94(X0))
| ~ sP84(sK219)
| ~ r1(sK219,X0) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_13120,plain,
( ~ sP84(sK219)
| ~ p2(sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_13121,plain,
( r1(sK92(sK219),sK93(sK219))
| ~ sP84(sK219) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_13122,plain,
( r1(sK219,sK92(sK219))
| ~ sP84(sK219) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_13129,plain,
( p2(sK213)
| ~ p2(sK245(sK213))
| ~ r1(sK209,sK213) ),
inference(instantiation,[status(thm)],[c_701]) ).
tcf(c_13149,plain,
( p2(sK92(sK219))
| r1(sK92(sK219),sK94(sK92(sK219)))
| ~ sP84(sK219)
| ~ r1(sK219,sK92(sK219)) ),
inference(instantiation,[status(thm)],[c_13118]) ).
tcf(c_13150,plain,
( p2(sK92(sK219))
| r1(sK94(sK92(sK219)),sK95(sK92(sK219)))
| ~ sP84(sK219)
| ~ r1(sK219,sK92(sK219)) ),
inference(instantiation,[status(thm)],[c_13117]) ).
tcf(c_13151,plain,
( p2(sK92(sK219))
| p2(sK94(sK92(sK219)))
| ~ sP84(sK219)
| ~ r1(sK219,sK92(sK219)) ),
inference(instantiation,[status(thm)],[c_13115]) ).
tcf(c_13170,plain,
! [X0: $i] :
( p2(X0)
| p2(sK101(X0))
| ~ sP82(sK92(sK219))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_13172,plain,
! [X0: $i] :
( p2(X0)
| r1(sK101(X0),sK102(X0))
| ~ sP82(sK92(sK219))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_13173,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK101(X0))
| ~ sP82(sK92(sK219))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_13184,plain,
( p2(sK93(sK219))
| p2(sK101(sK93(sK219)))
| ~ sP82(sK92(sK219))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13170]) ).
tcf(c_13186,plain,
( p2(sK93(sK219))
| r1(sK101(sK93(sK219)),sK102(sK93(sK219)))
| ~ sP82(sK92(sK219))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13172]) ).
tcf(c_13188,plain,
( p2(sK93(sK219))
| r1(sK93(sK219),sK101(sK93(sK219)))
| ~ sP82(sK92(sK219))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13173]) ).
tcf(c_13191,plain,
! [X0: $i] :
( p2(X0)
| p2(sK97(X0))
| ~ sP83(sK92(sK219))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_13193,plain,
! [X0: $i] :
( p2(X0)
| r1(sK97(X0),sK98(X0))
| ~ sP83(sK92(sK219))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_13194,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK97(X0))
| ~ sP83(sK92(sK219))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_13205,plain,
( p2(sK93(sK219))
| p2(sK97(sK93(sK219)))
| ~ sP83(sK92(sK219))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13191]) ).
tcf(c_13207,plain,
( p2(sK93(sK219))
| r1(sK97(sK93(sK219)),sK98(sK93(sK219)))
| ~ sP83(sK92(sK219))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13193]) ).
tcf(c_13209,plain,
( p2(sK93(sK219))
| r1(sK93(sK219),sK97(sK93(sK219)))
| ~ sP83(sK92(sK219))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13194]) ).
tcf(c_13214,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| sP85(X0)
| ~ sP86(X0)
| ~ p2(sK214(X1))
| ~ r1(sK214(X1),X2)
| ~ r1(sK87(X0),sK214(X1)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_13236,plain,
! [X0: $i] :
( p2(X0)
| ~ sP84(sK219)
| ~ p2(sK95(X0))
| ~ r1(sK219,X0) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_13239,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP84(sK219)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK93(sK219),X0) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_13303,plain,
! [X0: $i,X1: $i] :
( sP86(sK209)
| sP82(X1)
| sP83(X1)
| p2(X0)
| ~ r1(sK219,X1)
| ~ p2(sK94(sK92(sK219)))
| ~ r1(X1,sK94(sK92(sK219)))
| ~ r1(sK94(sK92(sK219)),X0) ),
inference(instantiation,[status(thm)],[c_593]) ).
tcf(c_13333,plain,
! [X0: $i] :
( sP86(sK209)
| p2(X0)
| sP82(sK92(sK219))
| sP83(sK92(sK219))
| ~ p2(sK94(sK92(sK219)))
| ~ r1(sK219,sK92(sK219))
| ~ r1(sK94(sK92(sK219)),X0)
| ~ r1(sK92(sK219),sK94(sK92(sK219))) ),
inference(instantiation,[status(thm)],[c_13303]) ).
tcf(c_13368,plain,
( sP86(sK209)
| sP82(sK92(sK219))
| sP83(sK92(sK219))
| p2(sK95(sK92(sK219)))
| ~ p2(sK94(sK92(sK219)))
| ~ r1(sK219,sK92(sK219))
| ~ r1(sK92(sK219),sK94(sK92(sK219)))
| ~ r1(sK94(sK92(sK219)),sK95(sK92(sK219))) ),
inference(instantiation,[status(thm)],[c_13333]) ).
tcf(c_13402,plain,
( p2(sK92(sK219))
| ~ sP84(sK219)
| ~ p2(sK95(sK92(sK219)))
| ~ r1(sK219,sK92(sK219)) ),
inference(instantiation,[status(thm)],[c_13236]) ).
tcf(c_13445,plain,
! [X0: $i] :
( p2(X0)
| ~ sP82(sK92(sK219))
| ~ p2(sK102(X0))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_13523,plain,
! [X0: $i] :
( p2(X0)
| ~ sP84(sK219)
| ~ p2(sK101(sK93(sK219)))
| ~ r1(sK101(sK93(sK219)),X0)
| ~ r1(sK93(sK219),sK101(sK93(sK219))) ),
inference(instantiation,[status(thm)],[c_13239]) ).
tcf(c_13553,plain,
( p2(sK102(sK93(sK219)))
| ~ sP84(sK219)
| ~ p2(sK101(sK93(sK219)))
| ~ r1(sK93(sK219),sK101(sK93(sK219)))
| ~ r1(sK101(sK93(sK219)),sK102(sK93(sK219))) ),
inference(instantiation,[status(thm)],[c_13523]) ).
tcf(c_13563,plain,
( p2(sK93(sK219))
| ~ sP82(sK92(sK219))
| ~ p2(sK102(sK93(sK219)))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13445]) ).
tcf(c_13576,plain,
! [X0: $i] :
( p2(X0)
| ~ sP83(sK92(sK219))
| ~ p2(sK98(X0))
| ~ r1(sK92(sK219),X0) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_13657,plain,
! [X0: $i] :
( p2(X0)
| ~ sP84(sK219)
| ~ p2(sK97(sK93(sK219)))
| ~ r1(sK97(sK93(sK219)),X0)
| ~ r1(sK93(sK219),sK97(sK93(sK219))) ),
inference(instantiation,[status(thm)],[c_13239]) ).
tcf(c_13666,plain,
( sP85(sK209)
| p2(sK87(sK209))
| ~ sP86(sK209)
| ~ p2(sK215(sK87(sK209))) ),
inference(superposition,[status(thm)],[c_49,c_581]) ).
tcf(c_13668,plain,
( sP85(sK209)
| p2(sK87(sK209))
| p2(sK214(sK87(sK209)))
| ~ sP86(sK209) ),
inference(superposition,[status(thm)],[c_49,c_582]) ).
tcf(c_13677,plain,
( p2(sK98(sK93(sK219)))
| ~ sP84(sK219)
| ~ p2(sK97(sK93(sK219)))
| ~ r1(sK93(sK219),sK97(sK93(sK219)))
| ~ r1(sK97(sK93(sK219)),sK98(sK93(sK219))) ),
inference(instantiation,[status(thm)],[c_13657]) ).
tcf(c_13692,plain,
( p2(sK93(sK219))
| ~ sP83(sK92(sK219))
| ~ p2(sK98(sK93(sK219)))
| ~ r1(sK92(sK219),sK93(sK219)) ),
inference(instantiation,[status(thm)],[c_13576]) ).
tcf(c_13731,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| sP85(X0)
| ~ sP86(X0)
| ~ p2(sK214(sK87(X0)))
| ~ r1(sK214(sK87(X0)),X1)
| ~ r1(sK87(X0),sK214(sK87(X0))) ),
inference(instantiation,[status(thm)],[c_13214]) ).
tcf(c_13745,plain,
! [X0: $i] :
( sP85(X0)
| p2(sK215(sK87(X0)))
| ~ sP86(X0)
| ~ p2(sK214(sK87(X0)))
| ~ r1(sK87(X0),sK214(sK87(X0)))
| ~ r1(sK214(sK87(X0)),sK215(sK87(X0))) ),
inference(instantiation,[status(thm)],[c_13731]) ).
tcf(c_13746,plain,
( sP85(sK209)
| p2(sK215(sK87(sK209)))
| ~ sP86(sK209)
| ~ p2(sK214(sK87(sK209)))
| ~ r1(sK87(sK209),sK214(sK87(sK209)))
| ~ r1(sK214(sK87(sK209)),sK215(sK87(sK209))) ),
inference(instantiation,[status(thm)],[c_13745]) ).
tcf(c_13764,plain,
! [X0: $i] :
( p2(sK87(X0))
| r1(sK214(sK87(X0)),sK215(sK87(X0)))
| ~ r1(sK209,sK87(X0)) ),
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_13765,plain,
( p2(sK87(sK209))
| r1(sK214(sK87(sK209)),sK215(sK87(sK209)))
| ~ r1(sK209,sK87(sK209)) ),
inference(instantiation,[status(thm)],[c_13764]) ).
tcf(c_13787,plain,
! [X0: $i,X1: $i] :
( p2(sK245(X0))
| r1(sK245(X0),sK90(sK245(X0)))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK245(X0)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_13821,plain,
( sP86(sK209)
| sP82(sK92(sK219))
| sP83(sK92(sK219))
| ~ sP84(sK219)
| ~ p2(sK92(sK219)) ),
inference(superposition,[status(thm)],[c_60,c_592]) ).
tcf(c_13876,plain,
! [X0: $i,X1: $i] :
( p2(sK245(X0))
| r1(sK90(sK245(X0)),sK91(sK245(X0)))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK245(X0)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_14231,plain,
( sP86(sK209)
| sP82(sK92(sK219))
| sP83(sK92(sK219))
| ~ sP84(sK219)
| ~ p2(sK92(sK219)) ),
inference(resolution,[status(thm)],[c_592,c_60]) ).
tcf(c_14248,plain,
! [X0: $i,X1: $i] :
( p2(sK245(X0))
| p2(sK90(sK245(X0)))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK245(X0)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_14364,plain,
! [X0: $i] :
( p2(sK219)
| p2(X0)
| ~ iPr_def_10
| ~ p2(sK214(sK219))
| ~ r1(sK209,sK219)
| ~ r1(sK214(sK219),X0) ),
inference(resolution,[status(thm)],[c_12962,c_579]) ).
tcf(c_14374,plain,
! [X0: $i] :
( p2(sK245(sK213))
| r1(sK245(sK213),sK90(sK245(sK213)))
| ~ sP85(X0)
| ~ r1(X0,sK213)
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_13787]) ).
tcf(c_14375,plain,
( p2(sK245(sK213))
| r1(sK245(sK213),sK90(sK245(sK213)))
| ~ sP85(sK209)
| ~ r1(sK209,sK213)
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_14374]) ).
tcf(c_14742,plain,
( sP86(sK209)
| sP82(sK92(sK219))
| sP83(sK92(sK219))
| ~ sP84(sK219) ),
inference(global_subsumption_just,[status(thm)],[c_14231,c_13122,c_13121,c_13120,c_13151,c_13150,c_13149,c_13184,c_13186,c_13188,c_13205,c_13207,c_13209,c_13368,c_13402,c_13553,c_13563,c_13677,c_13692,c_13821]) ).
tcf(c_14744,plain,
( sP86(sK209)
| sP82(sK92(sK219))
| ~ sP84(sK219) ),
inference(global_subsumption_just,[status(thm)],[c_14742,c_13121,c_13120,c_13184,c_13186,c_13188,c_13205,c_13207,c_13209,c_13553,c_13563,c_13677,c_13692,c_14742]) ).
tcf(c_14746,plain,
( sP86(sK209)
| ~ sP84(sK219) ),
inference(global_subsumption_just,[status(thm)],[c_14744,c_13121,c_13120,c_13184,c_13186,c_13188,c_13553,c_13563,c_14744]) ).
tcf(c_14755,plain,
( iPr_def_10
| sP86(sK209) ),
inference(backward_subsumption_resolution,[status(thm)],[c_12963,c_14746]) ).
tcf(c_14756,plain,
( sP86(sK209)
| ~ p2(sK219) ),
inference(backward_subsumption_resolution,[status(thm)],[c_590,c_14746]) ).
tcf(c_14793,plain,
( sP85(sK209)
| p2(sK87(sK209))
| p2(sK214(sK87(sK209)))
| ~ sP86(sK209) ),
inference(resolution,[status(thm)],[c_49,c_582]) ).
tcf(c_14910,plain,
( sP85(sK209)
| ~ sP86(sK209) ),
inference(global_subsumption_just,[status(thm)],[c_14793,c_1102,c_1103,c_13101,c_13668,c_13666,c_13746,c_13765]) ).
tcf(c_15093,plain,
! [X0: $i] :
( p2(sK219)
| p2(X0)
| ~ iPr_def_10
| ~ r1(sK214(sK219),X0)
| ~ r1(sK209,sK219) ),
inference(global_subsumption_just,[status(thm)],[c_14364,c_12991,c_14364]) ).
tcf(c_15094,plain,
! [X0: $i] :
( p2(sK219)
| p2(X0)
| ~ iPr_def_10
| ~ r1(sK209,sK219)
| ~ r1(sK214(sK219),X0) ),
inference(renaming,[status(thm)],[c_15093]) ).
tcf(c_15121,plain,
( p2(sK219)
| p2(sK215(sK219))
| ~ iPr_def_10
| ~ r1(sK209,sK219) ),
inference(resolution,[status(thm)],[c_15094,c_580]) ).
tcf(c_15134,plain,
! [X0: $i] :
( p2(sK245(sK213))
| r1(sK90(sK245(sK213)),sK91(sK245(sK213)))
| ~ sP85(X0)
| ~ r1(X0,sK213)
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_13876]) ).
tcf(c_15135,plain,
( p2(sK245(sK213))
| r1(sK90(sK245(sK213)),sK91(sK245(sK213)))
| ~ sP85(sK209)
| ~ r1(sK209,sK213)
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_15134]) ).
tcf(c_15154,plain,
( p2(sK219)
| ~ iPr_def_10
| ~ r1(sK209,sK219) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15121,c_581]) ).
tcf(c_15165,plain,
( p2(sK219)
| sP86(sK209)
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_15154,c_589]) ).
tcf(c_15166,plain,
sP86(sK209),
inference(global_subsumption_just,[status(thm)],[c_15165,c_14756,c_14755,c_15165]) ).
tcf(c_15561,plain,
! [X0: $i] :
( p2(sK245(sK213))
| p2(sK90(sK245(sK213)))
| ~ sP85(X0)
| ~ r1(X0,sK213)
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_14248]) ).
tcf(c_15562,plain,
( p2(sK245(sK213))
| p2(sK90(sK245(sK213)))
| ~ sP85(sK209)
| ~ r1(sK209,sK213)
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_15561]) ).
tcf(c_15634,plain,
! [X0: $i] :
( p2(sK213)
| p2(X0)
| ~ r1(sK209,sK213)
| ~ p2(sK90(sK245(sK213)))
| ~ r1(sK90(sK245(sK213)),X0)
| ~ r1(sK245(sK213),sK90(sK245(sK213))) ),
inference(instantiation,[status(thm)],[c_702]) ).
tcf(c_16012,plain,
( p2(sK213)
| p2(sK91(sK245(sK213)))
| ~ r1(sK209,sK213)
| ~ p2(sK90(sK245(sK213)))
| ~ r1(sK245(sK213),sK90(sK245(sK213)))
| ~ r1(sK90(sK245(sK213)),sK91(sK245(sK213))) ),
inference(instantiation,[status(thm)],[c_15634]) ).
tcf(c_16039,plain,
! [X0: $i,X1: $i] :
( p2(sK245(sK213))
| ~ sP85(X1)
| ~ r1(X1,X0)
| ~ p2(sK91(sK245(sK213)))
| ~ r1(X0,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_16171,plain,
! [X0: $i] :
( p2(sK245(sK213))
| ~ sP85(X0)
| ~ r1(X0,sK213)
| ~ p2(sK91(sK245(sK213)))
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_16039]) ).
tcf(c_16172,plain,
( p2(sK245(sK213))
| ~ sP85(sK209)
| ~ r1(sK209,sK213)
| ~ p2(sK91(sK245(sK213)))
| ~ r1(sK213,sK245(sK213)) ),
inference(instantiation,[status(thm)],[c_16171]) ).
tcf(c_16173,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_16172,c_16012,c_15562,c_15166,c_15135,c_14910,c_14375,c_13129,c_12972,c_577,c_578]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL642+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.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 23:58:37 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 6.05/2.27 % SZS status Started for theBenchmark.p
% 6.05/2.27 % SZS status Theorem for theBenchmark.p
% 6.05/2.27
% 6.05/2.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.05/2.27
% 6.05/2.27 % ------ iProver source info
% 6.05/2.27
% 6.05/2.27 % git: date: 2026-07-19 20:42:38 +0200
% 6.05/2.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.05/2.27 % git: non_committed_changes: false
% 6.05/2.27
% 6.05/2.27 % ------ Parsing...
% 6.05/2.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.05/2.27
% 6.05/2.27 % ------ Preprocessing... sf_s rm: 592 0s sf_e pe_s pe_e %
% 6.05/2.27
% 6.05/2.27 % ------ Preprocessing... gs_s sp: 1 0s gs_e snvd_s sp: 0 0s snvd_e
% 6.05/2.27 % ------ Proving...
% 6.05/2.27 % ------ Problem Properties
% 6.05/2.27
% 6.05/2.27 %
% 6.05/2.27 % clauses 63
% 6.05/2.27 % conjectures 25
% 6.05/2.27 % EPR 12
% 6.05/2.27 % Horn 27
% 6.05/2.27 % unary 6
% 6.05/2.27 % binary 7
% 6.05/2.27 % lits 223
% 6.05/2.27 % lits eq 0
% 6.05/2.27 % fd_pure 0
% 6.05/2.27 % fd_pseudo 0
% 6.05/2.27 % fd_cond 0
% 6.05/2.27 % fd_pseudo_cond 0
% 6.05/2.27 % AC symbols 0
% 6.05/2.27
% 6.05/2.27 % ------ Input Options Time Limit: Unbounded
% 6.05/2.27
% 6.05/2.27
% 6.05/2.27 % ------
% 6.05/2.27 % Current options:
% 6.05/2.27 % ------
% 6.05/2.27
% 6.05/2.27
% 6.05/2.27 %
% 6.05/2.27
% 6.05/2.27 % ------ Proving...
% 6.05/2.27 %
% 6.05/2.27
% 6.05/2.27 % SZS status Theorem for theBenchmark.p
% 6.05/2.27
% 6.05/2.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.05/2.28
% 6.05/2.28
%------------------------------------------------------------------------------