%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL642+1.010 : 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 : n010.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.14s 1.77s
% Output : CNFRefutation 6.14s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f29ERROR: Could not build tree for root c_11416ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f31,plain,
! [X0] :
( ~ sP21(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) )
| sP20(X0) ) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f32,plain,
! [X0] :
( ~ sP21(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) )
| sP20(X0) ) ) ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
! [X0] :
( ~ sP21(X0)
| ( ( ( p2(sK23(X0))
& ~ p2(sK24(X0))
& r1(sK23(X0),sK24(X0))
& r1(X0,sK23(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK22(X0),X2) )
& ~ p2(sK22(X0))
& r1(X0,sK22(X0)) )
| sP20(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24]),skolemize(X1,sK22(X0)),skolemize(X4,sK23(X0)),skolemize(X5,sK24(X0))],[f32]) ).
fof(f34,plain,
! [X0] :
( ~ sP20(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,[],[f28]) ).
fof(f35,plain,
! [X0] :
( ~ sP20(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,[],[f34]) ).
fof(f36,plain,
! [X0] :
( ~ sP20(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK25(X2))
& ~ p2(sK26(X2))
& r1(sK25(X2),sK26(X2))
& r1(X2,sK25(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26]),skolemize(X3,sK25(X2)),skolemize(X4,sK26(X2))],[f35]) ).
fof(f37,plain,
! [X22] :
( ~ sP19(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,[],[f27]) ).
fof(f38,plain,
! [X0] :
( ~ sP19(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,[],[f37]) ).
fof(f39,plain,
! [X0] :
( ~ sP19(X0)
| ( ! [X5] :
( ( p2(sK29(X5))
& ~ p2(sK30(X5))
& r1(sK29(X5),sK30(X5))
& r1(X5,sK29(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK28(X0),X3) )
& ~ p2(sK28(X0))
& r1(sK27(X0),sK28(X0))
& r1(X0,sK27(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30]),skolemize(X1,sK27(X0)),skolemize(X2,sK28(X0)),skolemize(X6,sK29(X5)),skolemize(X7,sK30(X5))],[f38]) ).
fof(f40,plain,
! [X32] :
( ~ sP18(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) )
| sP16(X33) ) )
| ~ r1(X32,X33) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f41,plain,
! [X0] :
( ~ sP18(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) )
| sP16(X1) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f40]) ).
fof(f42,plain,
! [X0] :
( ~ sP18(X0)
| ! [X1] :
( ( ( ( p2(sK32(X1))
& ~ p2(sK33(X1))
& r1(sK32(X1),sK33(X1))
& r1(X1,sK32(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK31(X1),X3) )
& ~ p2(sK31(X1))
& r1(X1,sK31(X1)) )
| sP16(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33]),skolemize(X2,sK31(X1)),skolemize(X5,sK32(X1)),skolemize(X6,sK33(X1))],[f41]) ).
fof(f43,plain,
! [X32] :
( ~ sP17(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,[],[f25]) ).
fof(f44,plain,
! [X0] :
( ~ sP17(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,[],[f43]) ).
fof(f45,plain,
! [X0] :
( ~ sP17(X0)
| ( ! [X5] :
( ( p2(sK36(X5))
& ~ p2(sK37(X5))
& r1(sK36(X5),sK37(X5))
& r1(X5,sK36(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK35(X0),X3) )
& ~ p2(sK35(X0))
& r1(sK34(X0),sK35(X0))
& r1(X0,sK34(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35,sK36,sK37]),skolemize(X1,sK34(X0)),skolemize(X2,sK35(X0)),skolemize(X6,sK36(X5)),skolemize(X7,sK37(X5))],[f44]) ).
fof(f95,plain,
? [X0] :
( ! [X55] :
( ? [X56] :
( ! [X57] :
( ~ p2(X57)
| ! [X58] :
( p2(X58)
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
& ~ p2(X56)
& r1(X55,X56) )
| p2(X55)
| ~ r1(X0,X55) )
& ( ? [X49] :
( ! [X51] :
( ( ? [X54] : r1(X51,X54)
& ~ p1(X51) )
| ! [X52] :
( ! [X53] : ~ r1(X52,X53)
| p1(X52)
| ~ r1(X51,X52) )
| ~ r1(X49,X51) )
& ? [X50] : r1(X49,X50)
& ~ p1(X49)
& r1(X0,X49) )
| ! [X48] : ~ r1(X0,X48)
| p1(X0) )
& ( ? [X42] :
( ! [X44] :
( ( ? [X47] : r1(X44,X47)
& ~ p1(X44)
& ~ p2(X44) )
| ! [X45] :
( ! [X46] : ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| ~ r1(X44,X45) )
| ~ r1(X42,X44) )
& ? [X43] : r1(X42,X43)
& ~ p1(X42)
& ~ p2(X42)
& r1(X0,X42) )
| ! [X41] : ~ r1(X0,X41)
| p1(X0)
| p2(X0) )
& ( ? [X39] :
( sP0(X39)
& ? [X40] : r1(X39,X40)
& ~ p1(X39)
& ~ p2(X39)
& ~ p3(X39)
& r1(X0,X39) )
| ! [X38] : ~ r1(X0,X38)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X36] :
( sP1(X36)
& ? [X37] : r1(X36,X37)
& ~ p1(X36)
& ~ p2(X36)
& ~ p3(X36)
& ~ p4(X36)
& r1(X0,X36) )
| ! [X35] : ~ r1(X0,X35)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X34] :
( sP2(X34)
& sP3(X34)
& ~ p1(X34)
& r1(X0,X34) )
| ! [X32] :
( ! [X33] : ~ r1(X32,X33)
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(X0,X32) )
| p1(X0) )
& ( ? [X31] :
( sP4(X31)
& sP5(X31)
& ~ p1(X31)
& ~ p2(X31)
& r1(X0,X31) )
| ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X0,X29) )
| p1(X0)
| p2(X0) )
& ( ? [X28] :
( sP8(X28)
& sP7(X28)
& ~ p1(X28)
& ~ p2(X28)
& ~ p3(X28)
& r1(X0,X28) )
| ! [X26] :
( ! [X27] : ~ r1(X26,X27)
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(X0,X26) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X25] :
( sP11(X25)
& sP10(X25)
& ~ p1(X25)
& ~ p2(X25)
& ~ p3(X25)
& ~ p4(X25)
& r1(X0,X25) )
| ! [X23] :
( ! [X24] : ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X0,X23) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X22] :
( sP14(X22)
& sP15(X22)
& ~ p1(X22)
& r1(X0,X22) )
| ! [X19] :
( ! [X20] :
( ! [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) )
& ( ? [X13] :
( ! [X16] :
( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP17(X16)
| sP18(X16)
| ~ r1(X13,X16) )
& ( ( ! [X14] :
( ~ p2(X14)
| ! [X15] :
( p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
& ~ p2(X13) )
| sP19(X13) )
& r1(X0,X13) )
| sP21(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,[],[f30]) ).
fof(f96,plain,
( ! [X55] :
( ( ! [X57] :
( ~ p2(X57)
| ! [X58] :
( p2(X58)
| ~ r1(X57,X58) )
| ~ r1(sK90(X55),X57) )
& ~ p2(sK90(X55))
& r1(X55,sK90(X55)) )
| p2(X55)
| ~ r1(sK64,X55) )
& ( ( ! [X51] :
( ( r1(X51,sK89(X51))
& ~ p1(X51) )
| ! [X52] :
( ! [X53] : ~ r1(X52,X53)
| p1(X52)
| ~ r1(X51,X52) )
| ~ r1(sK87,X51) )
& r1(sK87,sK88)
& ~ p1(sK87)
& r1(sK64,sK87) )
| ! [X48] : ~ r1(sK64,X48)
| p1(sK64) )
& ( ( ! [X44] :
( ( r1(X44,sK86(X44))
& ~ p1(X44)
& ~ p2(X44) )
| ! [X45] :
( ! [X46] : ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| ~ r1(X44,X45) )
| ~ r1(sK84,X44) )
& r1(sK84,sK85)
& ~ p1(sK84)
& ~ p2(sK84)
& r1(sK64,sK84) )
| ! [X41] : ~ r1(sK64,X41)
| p1(sK64)
| p2(sK64) )
& ( ( sP0(sK82)
& r1(sK82,sK83)
& ~ p1(sK82)
& ~ p2(sK82)
& ~ p3(sK82)
& r1(sK64,sK82) )
| ! [X38] : ~ r1(sK64,X38)
| p1(sK64)
| p2(sK64)
| p3(sK64) )
& ( ( sP1(sK80)
& r1(sK80,sK81)
& ~ p1(sK80)
& ~ p2(sK80)
& ~ p3(sK80)
& ~ p4(sK80)
& r1(sK64,sK80) )
| ! [X35] : ~ r1(sK64,X35)
| p1(sK64)
| p2(sK64)
| p3(sK64)
| p4(sK64) )
& ( ( sP2(sK79)
& sP3(sK79)
& ~ p1(sK79)
& r1(sK64,sK79) )
| ! [X32] :
( ! [X33] : ~ r1(X32,X33)
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(sK64,X32) )
| p1(sK64) )
& ( ( sP4(sK78)
& sP5(sK78)
& ~ p1(sK78)
& ~ p2(sK78)
& r1(sK64,sK78) )
| ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(sK64,X29) )
| p1(sK64)
| p2(sK64) )
& ( ( sP8(sK77)
& sP7(sK77)
& ~ p1(sK77)
& ~ p2(sK77)
& ~ p3(sK77)
& r1(sK64,sK77) )
| ! [X26] :
( ! [X27] : ~ r1(X26,X27)
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(sK64,X26) )
| p1(sK64)
| p2(sK64)
| p3(sK64) )
& ( ( sP11(sK76)
& sP10(sK76)
& ~ p1(sK76)
& ~ p2(sK76)
& ~ p3(sK76)
& ~ p4(sK76)
& r1(sK64,sK76) )
| ! [X23] :
( ! [X24] : ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(sK64,X23) )
| p1(sK64)
| p2(sK64)
| p3(sK64)
| p4(sK64) )
& ( ( sP14(sK75)
& sP15(sK75)
& ~ p1(sK75)
& r1(sK64,sK75) )
| ! [X19] :
( ! [X20] :
( ! [X21] : ~ r1(X20,X21)
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(X19,X20) )
| p1(X19)
| p2(X19)
| p3(X19)
| p4(X19)
| ~ r1(sK64,X19) )
| p1(sK64) )
& ( ( ! [X16] :
( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP17(X16)
| sP18(X16)
| ~ r1(sK74,X16) )
& ( ( ! [X14] :
( ~ p2(X14)
| ! [X15] :
( p2(X15)
| ~ r1(X14,X15) )
| ~ r1(sK74,X14) )
& ~ p2(sK74) )
| sP19(sK74) )
& r1(sK64,sK74) )
| sP21(sK64) )
& ! [X10] :
( ( p1(sK72(X10))
& ~ p1(sK73(X10))
& r1(sK72(X10),sK73(X10))
& r1(X10,sK72(X10)) )
| p1(X10)
| ~ r1(sK64,X10) )
& ~ p1(sK71)
& r1(sK64,sK71)
& ! [X6] :
( ( p2(sK69(X6))
& ~ p2(sK70(X6))
& r1(sK69(X6),sK70(X6))
& r1(X6,sK69(X6)) )
| p2(X6)
| ~ r1(sK64,X6) )
& ~ p2(sK68)
& r1(sK64,sK68)
& ! [X2] :
( ( p3(sK66(X2))
& ~ p3(sK67(X2))
& r1(sK66(X2),sK67(X2))
& r1(X2,sK66(X2)) )
| p3(X2)
| ~ r1(sK64,X2) )
& ~ p3(sK65)
& r1(sK64,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66,sK67,sK68,sK69,sK70,sK71,sK72,sK73,sK74,sK75,sK76,sK77,sK78,sK79,sK80,sK81,sK82,sK83,sK84,sK85,sK86,sK87,sK88,sK89,sK90]),skolemize(X0,sK64),skolemize(X1,sK65),skolemize(X3,sK66(X2)),skolemize(X4,sK67(X2)),skolemize(X5,sK68),skolemize(X7,sK69(X6)),skolemize(X8,sK70(X6)),skolemize(X9,sK71),skolemize(X11,sK72(X10)),skolemize(X12,sK73(X10)),skolemize(X13,sK74),skolemize(X22,sK75),skolemize(X25,sK76),skolemize(X28,sK77),skolemize(X31,sK78),skolemize(X34,sK79),skolemize(X36,sK80),skolemize(X37,sK81),skolemize(X39,sK82),skolemize(X40,sK83),skolemize(X42,sK84),skolemize(X43,sK85),skolemize(X47,sK86(X44)),skolemize(X49,sK87),skolemize(X50,sK88),skolemize(X54,sK89(X51)),skolemize(X56,sK90(X55))],[f95]) ).
fof(f101,plain,
! [X2,X3,X0] :
( ~ sP21(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK22(X0),X2)
| sP20(X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f102,plain,
! [X0] :
( ~ sP21(X0)
| ~ p2(sK22(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f103,plain,
! [X0] :
( ~ sP21(X0)
| r1(X0,sK22(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f104,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| p2(sK25(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f105,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ p2(sK26(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f106,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| r1(sK25(X2),sK26(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f107,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| r1(X2,sK25(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f108,plain,
! [X0,X5] :
( ~ sP19(X0)
| p2(sK29(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f109,plain,
! [X0,X5] :
( ~ sP19(X0)
| ~ p2(sK30(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f110,plain,
! [X0,X5] :
( ~ sP19(X0)
| r1(sK29(X5),sK30(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f111,plain,
! [X0,X5] :
( ~ sP19(X0)
| r1(X5,sK29(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f112,plain,
! [X3,X0,X4] :
( ~ sP19(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK28(X0),X3) ),
inference(cnf_transformation,[],[f39]) ).
fof(f113,plain,
! [X0] :
( ~ sP19(X0)
| ~ p2(sK28(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f114,plain,
! [X0] :
( ~ sP19(X0)
| r1(sK27(X0),sK28(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f115,plain,
! [X0] :
( ~ sP19(X0)
| r1(X0,sK27(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f116,plain,
! [X0,X1] :
( ~ sP18(X0)
| p2(sK32(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f117,plain,
! [X0,X1] :
( ~ sP18(X0)
| ~ p2(sK33(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f118,plain,
! [X0,X1] :
( ~ sP18(X0)
| r1(sK32(X1),sK33(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f119,plain,
! [X0,X1] :
( ~ sP18(X0)
| r1(X1,sK32(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f123,plain,
! [X0,X5] :
( ~ sP17(X0)
| p2(sK36(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f124,plain,
! [X0,X5] :
( ~ sP17(X0)
| ~ p2(sK37(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f125,plain,
! [X0,X5] :
( ~ sP17(X0)
| r1(sK36(X5),sK37(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f126,plain,
! [X0,X5] :
( ~ sP17(X0)
| r1(X5,sK36(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f229,plain,
! [X58,X57,X55] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(sK90(X55),X57)
| p2(X55)
| ~ r1(sK64,X55) ),
inference(cnf_transformation,[],[f96]) ).
fof(f230,plain,
! [X55] :
( ~ p2(sK90(X55))
| p2(X55)
| ~ r1(sK64,X55) ),
inference(cnf_transformation,[],[f96]) ).
fof(f231,plain,
! [X55] :
( r1(X55,sK90(X55))
| p2(X55)
| ~ r1(sK64,X55) ),
inference(cnf_transformation,[],[f96]) ).
fof(f283,plain,
! [X18,X16,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP17(X16)
| sP18(X16)
| ~ r1(sK74,X16)
| sP21(sK64) ),
inference(cnf_transformation,[],[f96]) ).
fof(f284,plain,
! [X16] :
( ~ p2(X16)
| sP17(X16)
| sP18(X16)
| ~ r1(sK74,X16)
| sP21(sK64) ),
inference(cnf_transformation,[],[f96]) ).
fof(f285,plain,
! [X14,X15] :
( ~ p2(X14)
| p2(X15)
| ~ r1(X14,X15)
| ~ r1(sK74,X14)
| sP19(sK74)
| sP21(sK64) ),
inference(cnf_transformation,[],[f96]) ).
fof(f286,plain,
( ~ p2(sK74)
| sP19(sK74)
| sP21(sK64) ),
inference(cnf_transformation,[],[f96]) ).
fof(f287,plain,
( r1(sK64,sK74)
| sP21(sK64) ),
inference(cnf_transformation,[],[f96]) ).
fof(f294,plain,
! [X6] :
( p2(sK69(X6))
| p2(X6)
| ~ r1(sK64,X6) ),
inference(cnf_transformation,[],[f96]) ).
fof(f295,plain,
! [X6] :
( ~ p2(sK70(X6))
| p2(X6)
| ~ r1(sK64,X6) ),
inference(cnf_transformation,[],[f96]) ).
fof(f296,plain,
! [X6] :
( r1(sK69(X6),sK70(X6))
| p2(X6)
| ~ r1(sK64,X6) ),
inference(cnf_transformation,[],[f96]) ).
fof(f297,plain,
! [X6] :
( r1(X6,sK69(X6))
| p2(X6)
| ~ r1(sK64,X6) ),
inference(cnf_transformation,[],[f96]) ).
fof(f298,plain,
~ p2(sK68),
inference(cnf_transformation,[],[f96]) ).
fof(f299,plain,
r1(sK64,sK68),
inference(cnf_transformation,[],[f96]) ).
tcf(c_49,plain,
! [X0: $i] :
( sP20(X0)
| r1(X0,sK22(X0))
| ~ sP21(X0) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_50,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP21(X0)
| ~ p2(sK22(X0)) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| sP20(X0)
| ~ p2(X1)
| ~ sP21(X0)
| ~ r1(X1,X2)
| ~ r1(sK22(X0),X1) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK25(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK25(X2),sK26(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP20(X0)
| ~ p2(sK26(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK25(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_60,plain,
! [X0: $i] :
( r1(X0,sK27(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_61,plain,
! [X0: $i] :
( r1(sK27(X0),sK28(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_62,plain,
! [X0: $i] :
( ~ sP19(X0)
| ~ p2(sK28(X0)) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP19(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK28(X0),X1) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK29(X1))
| ~ sP19(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK29(X1),sK30(X1))
| ~ sP19(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP19(X0)
| ~ p2(sK30(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK29(X1))
| ~ sP19(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK32(X1))
| ~ sP18(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK32(X1),sK33(X1))
| ~ sP18(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP18(X0)
| ~ p2(sK33(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK32(X1))
| ~ sP18(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK36(X1))
| ~ sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK36(X1),sK37(X1))
| ~ sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP17(X0)
| ~ p2(sK37(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK36(X1))
| ~ sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_187,negated_conjecture,
r1(sK64,sK68),
inference(cnf_transformation,[],[f299]) ).
tcf(c_188,negated_conjecture,
~ p2(sK68),
inference(cnf_transformation,[],[f298]) ).
tcf(c_189,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK69(X0))
| ~ r1(sK64,X0) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_190,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(sK69(X0),sK70(X0))
| ~ r1(sK64,X0) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_191,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK70(X0))
| ~ r1(sK64,X0) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_192,negated_conjecture,
! [X0: $i] :
( p2(X0)
| p2(sK69(X0))
| ~ r1(sK64,X0) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_199,negated_conjecture,
( sP21(sK64)
| r1(sK64,sK74) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_200,negated_conjecture,
( sP19(sK74)
| sP21(sK64)
| ~ p2(sK74) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_201,negated_conjecture,
! [X0: $i,X1: $i] :
( sP19(sK74)
| sP21(sK64)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK74,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_202,negated_conjecture,
! [X0: $i] :
( sP21(sK64)
| sP17(X0)
| sP18(X0)
| ~ p2(X0)
| ~ r1(sK74,X0) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_203,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP21(sK64)
| sP17(X0)
| sP18(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK74,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_255,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK90(X0))
| ~ r1(sK64,X0) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_256,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK90(X0))
| ~ r1(sK64,X0) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_257,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK64,X0)
| ~ r1(X1,X2)
| ~ r1(sK90(X0),X1) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_327,plain,
( sP20(sK64)
| ~ sP21(sK64)
| ~ p2(sK22(sK64)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_328,plain,
( sP20(sK64)
| r1(sK64,sK22(sK64))
| ~ sP21(sK64) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_5945,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| p2(X1)
| ~ p2(X0)
| ~ r1(sK74,X0)
| ~ r1(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_201]) ).
tcf(c_5946,negated_conjecture,
( iPr_def_10
| sP19(sK74)
| sP21(sK64) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_201]) ).
tcf(c_6058,plain,
( ~ p2(sK90(sK68))
| ~ r1(sK64,sK68) ),
inference(resolution,[status(thm)],[c_256,c_188]) ).
tcf(c_6059,plain,
~ p2(sK90(sK68)),
inference(global_subsumption_just,[status(thm)],[c_6058,c_187,c_6058]) ).
tcf(c_6088,plain,
( p2(sK74)
| p2(sK69(sK74))
| ~ r1(sK64,sK74) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_6172,plain,
( p2(sK74)
| r1(sK74,sK69(sK74))
| ~ r1(sK64,sK74) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_6232,plain,
( p2(sK74)
| r1(sK69(sK74),sK70(sK74))
| ~ r1(sK64,sK74) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_6298,plain,
( p2(sK68)
| r1(sK68,sK90(sK68))
| ~ r1(sK64,sK68) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_6301,plain,
( r1(sK74,sK27(sK74))
| ~ sP19(sK74) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_6320,plain,
( r1(sK27(sK74),sK28(sK74))
| ~ sP19(sK74) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_6359,plain,
! [X0: $i] :
( p2(X0)
| p2(sK29(X0))
| ~ sP19(sK74)
| ~ r1(sK74,X0) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_6361,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK29(X0))
| ~ sP19(sK74)
| ~ r1(sK74,X0) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_6363,plain,
! [X0: $i] :
( p2(X0)
| r1(sK29(X0),sK30(X0))
| ~ sP19(sK74)
| ~ r1(sK74,X0) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_6466,plain,
( p2(sK74)
| sP21(sK64)
| ~ p2(sK70(sK74)) ),
inference(superposition,[status(thm)],[c_199,c_191]) ).
tcf(c_6734,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK90(X1))
| p2(sK25(sK90(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK90(X1)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_6770,plain,
! [X0: $i,X1: $i] :
( ~ sP20(X1)
| ~ r1(X1,X0)
| ~ p2(sK26(sK90(sK68)))
| ~ r1(X0,sK90(sK68)) ),
inference(resolution,[status(thm)],[c_58,c_6059]) ).
tcf(c_6800,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK90(X1))
| r1(sK90(X1),sK25(sK90(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK90(X1)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_6803,plain,
( sP20(sK64)
| p2(sK22(sK64))
| ~ sP21(sK64)
| ~ p2(sK70(sK22(sK64))) ),
inference(superposition,[status(thm)],[c_49,c_191]) ).
tcf(c_6805,plain,
( sP20(sK64)
| p2(sK22(sK64))
| p2(sK69(sK22(sK64)))
| ~ sP21(sK64) ),
inference(superposition,[status(thm)],[c_49,c_192]) ).
tcf(c_6872,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK90(X1))
| r1(sK25(sK90(X1)),sK26(sK90(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK90(X1)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_6894,plain,
! [X0: $i] :
( p2(sK90(sK68))
| r1(sK90(sK68),sK25(sK90(sK68)))
| ~ sP20(X0)
| ~ r1(X0,sK68)
| ~ r1(sK68,sK90(sK68)) ),
inference(instantiation,[status(thm)],[c_6800]) ).
tcf(c_6895,plain,
( p2(sK90(sK68))
| r1(sK90(sK68),sK25(sK90(sK68)))
| ~ sP20(sK64)
| ~ r1(sK64,sK68)
| ~ r1(sK68,sK90(sK68)) ),
inference(instantiation,[status(thm)],[c_6894]) ).
tcf(c_6896,plain,
! [X0: $i] :
( p2(sK68)
| p2(X0)
| ~ r1(sK64,sK68)
| ~ p2(sK25(sK90(sK68)))
| ~ r1(sK25(sK90(sK68)),X0)
| ~ r1(sK90(sK68),sK25(sK90(sK68))) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_6900,plain,
! [X0: $i] :
( p2(sK68)
| p2(sK26(X0))
| ~ r1(sK64,sK68)
| ~ p2(sK25(sK90(sK68)))
| ~ r1(sK90(sK68),sK25(sK90(sK68)))
| ~ r1(sK25(sK90(sK68)),sK26(X0)) ),
inference(instantiation,[status(thm)],[c_6896]) ).
tcf(c_7009,plain,
( p2(sK22(sK64))
| r1(sK69(sK22(sK64)),sK70(sK22(sK64)))
| ~ r1(sK64,sK22(sK64)) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_7010,plain,
( p2(sK22(sK64))
| r1(sK22(sK64),sK69(sK22(sK64)))
| ~ r1(sK64,sK22(sK64)) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_7025,plain,
( sP21(sK64)
| sP17(sK27(sK74))
| sP18(sK27(sK74))
| ~ sP19(sK74)
| ~ p2(sK27(sK74)) ),
inference(superposition,[status(thm)],[c_60,c_202]) ).
tcf(c_7177,plain,
! [X0: $i] :
( sP20(sK64)
| p2(X0)
| ~ sP21(sK64)
| ~ p2(sK69(sK22(sK64)))
| ~ r1(sK69(sK22(sK64)),X0)
| ~ r1(sK22(sK64),sK69(sK22(sK64))) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_7216,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP19(sK74)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK28(sK74),X0) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_7236,plain,
! [X0: $i,X1: $i] :
( sP21(sK64)
| p2(X1)
| sP17(sK27(sK74))
| sP18(sK27(sK74))
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK74,sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_7277,plain,
( ~ sP20(sK64)
| ~ p2(sK26(sK90(sK68)))
| ~ r1(sK68,sK90(sK68)) ),
inference(resolution,[status(thm)],[c_6770,c_187]) ).
tcf(c_7298,plain,
( p2(sK27(sK74))
| p2(sK29(sK27(sK74)))
| ~ sP19(sK74)
| ~ r1(sK74,sK27(sK74)) ),
inference(instantiation,[status(thm)],[c_6359]) ).
tcf(c_7299,plain,
( p2(sK27(sK74))
| r1(sK27(sK74),sK29(sK27(sK74)))
| ~ sP19(sK74)
| ~ r1(sK74,sK27(sK74)) ),
inference(instantiation,[status(thm)],[c_6361]) ).
tcf(c_7300,plain,
( p2(sK27(sK74))
| r1(sK29(sK27(sK74)),sK30(sK27(sK74)))
| ~ sP19(sK74)
| ~ r1(sK74,sK27(sK74)) ),
inference(instantiation,[status(thm)],[c_6363]) ).
tcf(c_7351,plain,
! [X0: $i,X1: $i] :
( sP21(sK64)
| sP17(sK27(sK74))
| sP18(sK27(sK74))
| p2(sK30(X1))
| ~ p2(X0)
| ~ r1(sK74,sK27(sK74))
| ~ r1(sK27(sK74),X0)
| ~ r1(X0,sK30(X1)) ),
inference(instantiation,[status(thm)],[c_7236]) ).
tcf(c_7454,plain,
! [X0: $i] :
( p2(X0)
| ~ iPr_def_10
| ~ p2(sK69(sK74))
| ~ r1(sK74,sK69(sK74))
| ~ r1(sK69(sK74),X0) ),
inference(instantiation,[status(thm)],[c_5945]) ).
tcf(c_7769,plain,
( p2(sK70(sK74))
| ~ iPr_def_10
| ~ p2(sK69(sK74))
| ~ r1(sK74,sK69(sK74))
| ~ r1(sK69(sK74),sK70(sK74)) ),
inference(instantiation,[status(thm)],[c_7454]) ).
tcf(c_8008,plain,
! [X0: $i] :
( p2(X0)
| r1(sK32(X0),sK33(X0))
| ~ sP18(sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_8009,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK32(X0))
| ~ sP18(sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_8011,plain,
! [X0: $i] :
( p2(X0)
| p2(sK32(X0))
| ~ sP18(sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_8012,plain,
! [X0: $i] :
( p2(X0)
| ~ sP18(sK27(sK74))
| ~ p2(sK33(X0))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_8501,plain,
( p2(sK28(sK74))
| p2(sK32(sK28(sK74)))
| ~ sP18(sK27(sK74))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8011]) ).
tcf(c_8502,plain,
( p2(sK28(sK74))
| ~ sP18(sK27(sK74))
| ~ p2(sK33(sK28(sK74)))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8012]) ).
tcf(c_8505,plain,
( p2(sK28(sK74))
| r1(sK32(sK28(sK74)),sK33(sK28(sK74)))
| ~ sP18(sK27(sK74))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8008]) ).
tcf(c_8506,plain,
( p2(sK28(sK74))
| r1(sK28(sK74),sK32(sK28(sK74)))
| ~ sP18(sK27(sK74))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8009]) ).
tcf(c_8628,plain,
! [X0: $i] :
( p2(X0)
| ~ sP19(sK74)
| ~ p2(sK32(sK28(sK74)))
| ~ r1(sK32(sK28(sK74)),X0)
| ~ r1(sK28(sK74),sK32(sK28(sK74))) ),
inference(instantiation,[status(thm)],[c_7216]) ).
tcf(c_8636,plain,
( p2(sK33(sK28(sK74)))
| ~ sP19(sK74)
| ~ p2(sK32(sK28(sK74)))
| ~ r1(sK28(sK74),sK32(sK28(sK74)))
| ~ r1(sK32(sK28(sK74)),sK33(sK28(sK74))) ),
inference(instantiation,[status(thm)],[c_8628]) ).
tcf(c_8793,plain,
( ~ sP19(sK74)
| ~ p2(sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_8840,plain,
! [X0: $i] :
( p2(X0)
| r1(sK36(X0),sK37(X0))
| ~ sP17(sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_8841,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK36(X0))
| ~ sP17(sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_8842,plain,
! [X0: $i] :
( p2(X0)
| p2(sK36(X0))
| ~ sP17(sK27(sK74))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_8843,plain,
! [X0: $i] :
( p2(X0)
| ~ sP17(sK27(sK74))
| ~ p2(sK37(X0))
| ~ r1(sK27(sK74),X0) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_8851,plain,
( sP21(sK64)
| sP19(sK74) ),
inference(global_subsumption_just,[status(thm)],[c_5946,c_199,c_200,c_5946,c_6088,c_6172,c_6232,c_6466,c_7769]) ).
tcf(c_8852,negated_conjecture,
( sP19(sK74)
| sP21(sK64) ),
inference(renaming,[status(thm)],[c_8851]) ).
tcf(c_9247,plain,
( p2(sK28(sK74))
| p2(sK36(sK28(sK74)))
| ~ sP17(sK27(sK74))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8842]) ).
tcf(c_9249,plain,
( p2(sK28(sK74))
| ~ sP17(sK27(sK74))
| ~ p2(sK37(sK28(sK74)))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8843]) ).
tcf(c_9251,plain,
( p2(sK28(sK74))
| r1(sK36(sK28(sK74)),sK37(sK28(sK74)))
| ~ sP17(sK27(sK74))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8840]) ).
tcf(c_9379,plain,
( p2(sK28(sK74))
| r1(sK28(sK74),sK36(sK28(sK74)))
| ~ sP17(sK27(sK74))
| ~ r1(sK27(sK74),sK28(sK74)) ),
inference(instantiation,[status(thm)],[c_8841]) ).
tcf(c_9413,plain,
! [X0: $i] :
( p2(X0)
| ~ sP19(sK74)
| ~ p2(sK36(sK28(sK74)))
| ~ r1(sK36(sK28(sK74)),X0)
| ~ r1(sK28(sK74),sK36(sK28(sK74))) ),
inference(instantiation,[status(thm)],[c_7216]) ).
tcf(c_9606,plain,
( p2(sK37(sK28(sK74)))
| ~ sP19(sK74)
| ~ p2(sK36(sK28(sK74)))
| ~ r1(sK28(sK74),sK36(sK28(sK74)))
| ~ r1(sK36(sK28(sK74)),sK37(sK28(sK74))) ),
inference(instantiation,[status(thm)],[c_9413]) ).
tcf(c_10336,plain,
! [X0: $i] :
( sP21(sK64)
| sP17(sK27(sK74))
| sP18(sK27(sK74))
| p2(sK30(X0))
| ~ p2(sK29(sK27(sK74)))
| ~ r1(sK74,sK27(sK74))
| ~ r1(sK27(sK74),sK29(sK27(sK74)))
| ~ r1(sK29(sK27(sK74)),sK30(X0)) ),
inference(instantiation,[status(thm)],[c_7351]) ).
tcf(c_10508,plain,
( sP21(sK64)
| sP17(sK27(sK74))
| sP18(sK27(sK74))
| p2(sK30(sK27(sK74)))
| ~ p2(sK29(sK27(sK74)))
| ~ r1(sK74,sK27(sK74))
| ~ r1(sK27(sK74),sK29(sK27(sK74)))
| ~ r1(sK29(sK27(sK74)),sK30(sK27(sK74))) ),
inference(instantiation,[status(thm)],[c_10336]) ).
tcf(c_10524,plain,
! [X0: $i] :
( p2(sK27(sK74))
| ~ sP19(X0)
| ~ p2(sK30(sK27(sK74)))
| ~ r1(X0,sK27(sK74)) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_10526,plain,
( p2(sK27(sK74))
| ~ sP19(sK74)
| ~ p2(sK30(sK27(sK74)))
| ~ r1(sK74,sK27(sK74)) ),
inference(instantiation,[status(thm)],[c_10524]) ).
tcf(c_10547,plain,
! [X0: $i] :
( p2(sK90(sK68))
| r1(sK25(sK90(sK68)),sK26(sK90(sK68)))
| ~ sP20(X0)
| ~ r1(X0,sK68)
| ~ r1(sK68,sK90(sK68)) ),
inference(instantiation,[status(thm)],[c_6872]) ).
tcf(c_10548,plain,
( p2(sK90(sK68))
| r1(sK25(sK90(sK68)),sK26(sK90(sK68)))
| ~ sP20(sK64)
| ~ r1(sK64,sK68)
| ~ r1(sK68,sK90(sK68)) ),
inference(instantiation,[status(thm)],[c_10547]) ).
tcf(c_10773,plain,
( p2(sK68)
| p2(sK26(sK90(sK68)))
| ~ r1(sK64,sK68)
| ~ p2(sK25(sK90(sK68)))
| ~ r1(sK90(sK68),sK25(sK90(sK68)))
| ~ r1(sK25(sK90(sK68)),sK26(sK90(sK68))) ),
inference(instantiation,[status(thm)],[c_6900]) ).
tcf(c_11172,plain,
! [X0: $i] :
( p2(sK90(sK68))
| p2(sK25(sK90(sK68)))
| ~ sP20(X0)
| ~ r1(X0,sK68)
| ~ r1(sK68,sK90(sK68)) ),
inference(instantiation,[status(thm)],[c_6734]) ).
tcf(c_11173,plain,
( p2(sK90(sK68))
| p2(sK25(sK90(sK68)))
| ~ sP20(sK64)
| ~ r1(sK64,sK68)
| ~ r1(sK68,sK90(sK68)) ),
inference(instantiation,[status(thm)],[c_11172]) ).
tcf(c_11211,plain,
( sP20(sK64)
| p2(sK70(sK22(sK64)))
| ~ sP21(sK64)
| ~ p2(sK69(sK22(sK64)))
| ~ r1(sK22(sK64),sK69(sK22(sK64)))
| ~ r1(sK69(sK22(sK64)),sK70(sK22(sK64))) ),
inference(instantiation,[status(thm)],[c_7177]) ).
tcf(c_11416,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_11211,c_11173,c_10773,c_10548,c_10526,c_10508,c_9606,c_9379,c_9251,c_9249,c_9247,c_8852,c_8793,c_8636,c_8506,c_8505,c_8502,c_8501,c_7300,c_7299,c_7298,c_7277,c_7025,c_7009,c_7010,c_6895,c_6803,c_6805,c_6320,c_6301,c_6298,c_6058,c_328,c_327,c_187,c_188]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL642+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n010.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 23:53:13 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 6.14/1.77 % SZS status Started for theBenchmark.p
% 6.14/1.77 % SZS status Theorem for theBenchmark.p
% 6.14/1.77
% 6.14/1.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.14/1.77
% 6.14/1.77 % ------ iProver source info
% 6.14/1.77
% 6.14/1.77 % git: date: 2026-07-19 20:42:38 +0200
% 6.14/1.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.14/1.77 % git: non_committed_changes: false
% 6.14/1.77
% 6.14/1.77 % ------ Parsing...
% 6.14/1.77 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.14/1.77
% 6.14/1.77 % ------ Preprocessing... sf_s rm: 147 0s sf_e pe_s pe_e %
% 6.14/1.77
% 6.14/1.77 % ------ Preprocessing... gs_s sp: 1 0s gs_e snvd_s sp: 0 0s snvd_e
% 6.14/1.77 % ------ Proving...
% 6.14/1.77 % ------ Problem Properties
% 6.14/1.77
% 6.14/1.77 %
% 6.14/1.77 % clauses 63
% 6.14/1.77 % conjectures 25
% 6.14/1.77 % EPR 12
% 6.14/1.77 % Horn 27
% 6.14/1.77 % unary 6
% 6.14/1.77 % binary 7
% 6.14/1.77 % lits 223
% 6.14/1.77 % lits eq 0
% 6.14/1.77 % fd_pure 0
% 6.14/1.77 % fd_pseudo 0
% 6.14/1.77 % fd_cond 0
% 6.14/1.77 % fd_pseudo_cond 0
% 6.14/1.77 % AC symbols 0
% 6.14/1.77
% 6.14/1.77 % ------ Input Options Time Limit: Unbounded
% 6.14/1.77
% 6.14/1.77
% 6.14/1.77 % ------
% 6.14/1.77 % Current options:
% 6.14/1.77 % ------
% 6.14/1.77
% 6.14/1.77
% 6.14/1.77 %
% 6.14/1.77
% 6.14/1.77 % ------ Proving...
% 6.14/1.77 %
% 6.14/1.77
% 6.14/1.77 % SZS status Theorem for theBenchmark.p
% 6.14/1.77
% 6.14/1.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.14/1.78
% 6.14/1.78
%------------------------------------------------------------------------------