%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL636+1.005 : 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:06:58 PM UTC 2026
% Result : Theorem 31.97s 5.34s
% Output : CNFRefutation 31.97s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f27ERROR: Could not build tree for root c_39798ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f69,plain,
! [X10] :
( ~ sP59(X10)
| ( ( ~ p101(X10)
| p100(X10) )
& ( ~ p102(X10)
| p101(X10) )
& ( ~ p103(X10)
| p102(X10) )
& ( ~ p104(X10)
| p103(X10) )
& ( ~ p105(X10)
| p104(X10) )
& sP53(X10)
& sP54(X10)
& sP55(X10)
& sP56(X10)
& sP57(X10)
& sP58(X10)
& sP48(X10)
& sP49(X10)
& sP50(X10)
& sP51(X10)
& sP52(X10) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f70,plain,
! [X0] :
( ~ sP59(X0)
| ( ( ~ p101(X0)
| p100(X0) )
& ( ~ p102(X0)
| p101(X0) )
& ( ~ p103(X0)
| p102(X0) )
& ( ~ p104(X0)
| p103(X0) )
& ( ~ p105(X0)
| p104(X0) )
& sP53(X0)
& sP54(X0)
& sP55(X0)
& sP56(X0)
& sP57(X0)
& sP58(X0)
& sP48(X0)
& sP49(X0)
& sP50(X0)
& sP51(X0)
& sP52(X0) ) ),
inference(rectify,[],[f69]) ).
fof(f98,plain,
! [X36] :
( ~ sP47(X36)
| ( ( ~ p101(X36)
| p100(X36) )
& ( ~ p102(X36)
| p101(X36) )
& ( ~ p103(X36)
| p102(X36) )
& ( ~ p104(X36)
| p103(X36) )
& ( ~ p105(X36)
| p104(X36) )
& sP41(X36)
& sP42(X36)
& sP43(X36)
& sP44(X36)
& sP45(X36)
& sP46(X36)
& sP36(X36)
& sP37(X36)
& sP38(X36)
& sP39(X36)
& sP40(X36) ) ),
inference(nnf_transformation,[],[f55]) ).
fof(f99,plain,
! [X0] :
( ~ sP47(X0)
| ( ( ~ p101(X0)
| p100(X0) )
& ( ~ p102(X0)
| p101(X0) )
& ( ~ p103(X0)
| p102(X0) )
& ( ~ p104(X0)
| p103(X0) )
& ( ~ p105(X0)
| p104(X0) )
& sP41(X0)
& sP42(X0)
& sP43(X0)
& sP44(X0)
& sP45(X0)
& sP46(X0)
& sP36(X0)
& sP37(X0)
& sP38(X0)
& sP39(X0)
& sP40(X0) ) ),
inference(rectify,[],[f98]) ).
fof(f106,plain,
! [X36] :
( ~ sP43(X36)
| ~ p102(X36)
| ( ( ~ p3(X36)
| ! [X54] :
( ~ p102(X54)
| p3(X54)
| ~ r1(X36,X54) ) )
& ( p3(X36)
| ! [X53] :
( ~ p102(X53)
| ~ p3(X53)
| ~ r1(X36,X53) ) ) ) ),
inference(nnf_transformation,[],[f51]) ).
fof(f107,plain,
! [X0] :
( ~ sP43(X0)
| ~ p102(X0)
| ( ( ~ p3(X0)
| ! [X2] :
( ~ p102(X2)
| p3(X2)
| ~ r1(X0,X2) ) )
& ( p3(X0)
| ! [X1] :
( ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1) ) ) ) ),
inference(rectify,[],[f106]) ).
fof(f112,plain,
! [X36] :
( ~ sP40(X36)
| ~ p104(X36)
| p105(X36)
| ( ? [X38] :
( p105(X38)
& p6(X38)
& r1(X36,X38) )
& ? [X37] :
( p105(X37)
& ~ p6(X37)
& r1(X36,X37) ) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f113,plain,
! [X0] :
( ~ sP40(X0)
| ~ p104(X0)
| p105(X0)
| ( ? [X2] :
( p105(X2)
& p6(X2)
& r1(X0,X2) )
& ? [X1] :
( p105(X1)
& ~ p6(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ~ sP40(X0)
| ~ p104(X0)
| p105(X0)
| ( p105(sK71(X0))
& p6(sK71(X0))
& r1(X0,sK71(X0))
& p105(sK70(X0))
& ~ p6(sK70(X0))
& r1(X0,sK70(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70,sK71]),skolemize(X1,sK70(X0)),skolemize(X2,sK71(X0))],[f113]) ).
fof(f127,plain,
! [X61] :
( ~ sP35(X61)
| ( ( ~ p101(X61)
| p100(X61) )
& ( ~ p102(X61)
| p101(X61) )
& ( ~ p103(X61)
| p102(X61) )
& ( ~ p104(X61)
| p103(X61) )
& ( ~ p105(X61)
| p104(X61) )
& sP29(X61)
& sP30(X61)
& sP31(X61)
& sP32(X61)
& sP33(X61)
& sP34(X61)
& sP24(X61)
& sP25(X61)
& sP26(X61)
& sP27(X61)
& sP28(X61) ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f128,plain,
! [X0] :
( ~ sP35(X0)
| ( ( ~ p101(X0)
| p100(X0) )
& ( ~ p102(X0)
| p101(X0) )
& ( ~ p103(X0)
| p102(X0) )
& ( ~ p104(X0)
| p103(X0) )
& ( ~ p105(X0)
| p104(X0) )
& sP29(X0)
& sP30(X0)
& sP31(X0)
& sP32(X0)
& sP33(X0)
& sP34(X0)
& sP24(X0)
& sP25(X0)
& sP26(X0)
& sP27(X0)
& sP28(X0) ) ),
inference(rectify,[],[f127]) ).
fof(f135,plain,
! [X61] :
( ~ sP31(X61)
| ~ p102(X61)
| ( ( ~ p3(X61)
| ! [X79] :
( ~ p102(X79)
| p3(X79)
| ~ r1(X61,X79) ) )
& ( p3(X61)
| ! [X78] :
( ~ p102(X78)
| ~ p3(X78)
| ~ r1(X61,X78) ) ) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f136,plain,
! [X0] :
( ~ sP31(X0)
| ~ p102(X0)
| ( ( ~ p3(X0)
| ! [X2] :
( ~ p102(X2)
| p3(X2)
| ~ r1(X0,X2) ) )
& ( p3(X0)
| ! [X1] :
( ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1) ) ) ) ),
inference(rectify,[],[f135]) ).
fof(f144,plain,
! [X61] :
( ~ sP27(X61)
| ~ p103(X61)
| p104(X61)
| ( ? [X65] :
( p104(X65)
& ~ p105(X65)
& p5(X65)
& r1(X61,X65) )
& ? [X64] :
( p104(X64)
& ~ p105(X64)
& ~ p5(X64)
& r1(X61,X64) ) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f145,plain,
! [X0] :
( ~ sP27(X0)
| ~ p103(X0)
| p104(X0)
| ( ? [X2] :
( p104(X2)
& ~ p105(X2)
& p5(X2)
& r1(X0,X2) )
& ? [X1] :
( p104(X1)
& ~ p105(X1)
& ~ p5(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f144]) ).
fof(f146,plain,
! [X0] :
( ~ sP27(X0)
| ~ p103(X0)
| p104(X0)
| ( p104(sK83(X0))
& ~ p105(sK83(X0))
& p5(sK83(X0))
& r1(X0,sK83(X0))
& p104(sK82(X0))
& ~ p105(sK82(X0))
& ~ p5(sK82(X0))
& r1(X0,sK82(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK82,sK83]),skolemize(X1,sK82(X0)),skolemize(X2,sK83(X0))],[f145]) ).
fof(f156,plain,
! [X85] :
( ~ sP23(X85)
| ( ( ~ p101(X85)
| p100(X85) )
& ( ~ p102(X85)
| p101(X85) )
& ( ~ p103(X85)
| p102(X85) )
& ( ~ p104(X85)
| p103(X85) )
& ( ~ p105(X85)
| p104(X85) )
& sP17(X85)
& sP18(X85)
& sP19(X85)
& sP20(X85)
& sP21(X85)
& sP22(X85)
& sP12(X85)
& sP13(X85)
& sP14(X85)
& sP15(X85)
& sP16(X85) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f157,plain,
! [X0] :
( ~ sP23(X0)
| ( ( ~ p101(X0)
| p100(X0) )
& ( ~ p102(X0)
| p101(X0) )
& ( ~ p103(X0)
| p102(X0) )
& ( ~ p104(X0)
| p103(X0) )
& ( ~ p105(X0)
| p104(X0) )
& sP17(X0)
& sP18(X0)
& sP19(X0)
& sP20(X0)
& sP21(X0)
& sP22(X0)
& sP12(X0)
& sP13(X0)
& sP14(X0)
& sP15(X0)
& sP16(X0) ) ),
inference(rectify,[],[f156]) ).
fof(f164,plain,
! [X85] :
( ~ sP19(X85)
| ~ p102(X85)
| ( ( ~ p3(X85)
| ! [X103] :
( ~ p102(X103)
| p3(X103)
| ~ r1(X85,X103) ) )
& ( p3(X85)
| ! [X102] :
( ~ p102(X102)
| ~ p3(X102)
| ~ r1(X85,X102) ) ) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f165,plain,
! [X0] :
( ~ sP19(X0)
| ~ p102(X0)
| ( ( ~ p3(X0)
| ! [X2] :
( ~ p102(X2)
| p3(X2)
| ~ r1(X0,X2) ) )
& ( p3(X0)
| ! [X1] :
( ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1) ) ) ) ),
inference(rectify,[],[f164]) ).
fof(f176,plain,
! [X85] :
( ~ sP14(X85)
| ~ p102(X85)
| p103(X85)
| ( ? [X91] :
( p103(X91)
& ~ p104(X91)
& p4(X91)
& r1(X85,X91) )
& ? [X90] :
( p103(X90)
& ~ p104(X90)
& ~ p4(X90)
& r1(X85,X90) ) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f177,plain,
! [X0] :
( ~ sP14(X0)
| ~ p102(X0)
| p103(X0)
| ( ? [X2] :
( p103(X2)
& ~ p104(X2)
& p4(X2)
& r1(X0,X2) )
& ? [X1] :
( p103(X1)
& ~ p104(X1)
& ~ p4(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f176]) ).
fof(f178,plain,
! [X0] :
( ~ sP14(X0)
| ~ p102(X0)
| p103(X0)
| ( p103(sK95(X0))
& ~ p104(sK95(X0))
& p4(sK95(X0))
& r1(X0,sK95(X0))
& p103(sK94(X0))
& ~ p104(sK94(X0))
& ~ p4(sK94(X0))
& r1(X0,sK94(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94,sK95]),skolemize(X1,sK94(X0)),skolemize(X2,sK95(X0))],[f177]) ).
fof(f185,plain,
! [X108] :
( ~ sP11(X108)
| ( ( ~ p101(X108)
| p100(X108) )
& ( ~ p102(X108)
| p101(X108) )
& ( ~ p103(X108)
| p102(X108) )
& ( ~ p104(X108)
| p103(X108) )
& ( ~ p105(X108)
| p104(X108) )
& sP5(X108)
& sP6(X108)
& sP7(X108)
& sP8(X108)
& sP9(X108)
& sP10(X108)
& sP0(X108)
& sP1(X108)
& sP2(X108)
& sP3(X108)
& sP4(X108) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f186,plain,
! [X0] :
( ~ sP11(X0)
| ( ( ~ p101(X0)
| p100(X0) )
& ( ~ p102(X0)
| p101(X0) )
& ( ~ p103(X0)
| p102(X0) )
& ( ~ p104(X0)
| p103(X0) )
& ( ~ p105(X0)
| p104(X0) )
& sP5(X0)
& sP6(X0)
& sP7(X0)
& sP8(X0)
& sP9(X0)
& sP10(X0)
& sP0(X0)
& sP1(X0)
& sP2(X0)
& sP3(X0)
& sP4(X0) ) ),
inference(rectify,[],[f185]) ).
fof(f208,plain,
! [X108] :
( ~ sP1(X108)
| ~ p101(X108)
| p102(X108)
| ( ? [X116] :
( p102(X116)
& ~ p103(X116)
& p3(X116)
& r1(X108,X116) )
& ? [X115] :
( p102(X115)
& ~ p103(X115)
& ~ p3(X115)
& r1(X108,X115) ) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f209,plain,
! [X0] :
( ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| ( ? [X2] :
( p102(X2)
& ~ p103(X2)
& p3(X2)
& r1(X0,X2) )
& ? [X1] :
( p102(X1)
& ~ p103(X1)
& ~ p3(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f208]) ).
fof(f210,plain,
! [X0] :
( ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| ( p102(sK107(X0))
& ~ p103(sK107(X0))
& p3(sK107(X0))
& r1(X0,sK107(X0))
& p102(sK106(X0))
& ~ p103(sK106(X0))
& ~ p3(sK106(X0))
& r1(X0,sK106(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK106,sK107]),skolemize(X1,sK106(X0)),skolemize(X2,sK107(X0))],[f209]) ).
fof(f214,plain,
? [X0] :
( p100(X0)
& ~ p101(X0)
& ( ~ p101(X0)
| p100(X0) )
& ( ~ p102(X0)
| p101(X0) )
& ( ~ p103(X0)
| p102(X0) )
& ( ~ p104(X0)
| p103(X0) )
& ( ~ p105(X0)
| p104(X0) )
& ( ~ p100(X0)
| ( ( ~ p1(X0)
| ! [X42] :
( ~ p100(X42)
| p1(X42)
| ~ r1(X0,X42) ) )
& ( p1(X0)
| ! [X41] :
( ~ p100(X41)
| ~ p1(X41)
| ~ r1(X0,X41) ) ) ) )
& ( ~ p101(X0)
| ( ( ~ p2(X0)
| ! [X40] :
( ~ p101(X40)
| p2(X40)
| ~ r1(X0,X40) ) )
& ( p2(X0)
| ! [X39] :
( ~ p101(X39)
| ~ p2(X39)
| ~ r1(X0,X39) ) ) ) )
& ( ~ p102(X0)
| ( ( ~ p3(X0)
| ! [X38] :
( ~ p102(X38)
| p3(X38)
| ~ r1(X0,X38) ) )
& ( p3(X0)
| ! [X37] :
( ~ p102(X37)
| ~ p3(X37)
| ~ r1(X0,X37) ) ) ) )
& ( ~ p103(X0)
| ( ( ~ p4(X0)
| ! [X36] :
( ~ p103(X36)
| p4(X36)
| ~ r1(X0,X36) ) )
& ( p4(X0)
| ! [X35] :
( ~ p103(X35)
| ~ p4(X35)
| ~ r1(X0,X35) ) ) ) )
& ( ~ p104(X0)
| ( ( ~ p5(X0)
| ! [X34] :
( ~ p104(X34)
| p5(X34)
| ~ r1(X0,X34) ) )
& ( p5(X0)
| ! [X33] :
( ~ p104(X33)
| ~ p5(X33)
| ~ r1(X0,X33) ) ) ) )
& ( ~ p105(X0)
| ( ( ~ p6(X0)
| ! [X32] :
( ~ p105(X32)
| p6(X32)
| ~ r1(X0,X32) ) )
& ( p6(X0)
| ! [X31] :
( ~ p105(X31)
| ~ p6(X31)
| ~ r1(X0,X31) ) ) ) )
& ( ~ p100(X0)
| p101(X0)
| ( ? [X30] :
( p101(X30)
& ~ p102(X30)
& p2(X30)
& r1(X0,X30) )
& ? [X29] :
( p101(X29)
& ~ p102(X29)
& ~ p2(X29)
& r1(X0,X29) ) ) )
& ( ~ p101(X0)
| p102(X0)
| ( ? [X28] :
( p102(X28)
& ~ p103(X28)
& p3(X28)
& r1(X0,X28) )
& ? [X27] :
( p102(X27)
& ~ p103(X27)
& ~ p3(X27)
& r1(X0,X27) ) ) )
& ( ~ p102(X0)
| p103(X0)
| ( ? [X26] :
( p103(X26)
& ~ p104(X26)
& p4(X26)
& r1(X0,X26) )
& ? [X25] :
( p103(X25)
& ~ p104(X25)
& ~ p4(X25)
& r1(X0,X25) ) ) )
& ( ~ p103(X0)
| p104(X0)
| ( ? [X24] :
( p104(X24)
& ~ p105(X24)
& p5(X24)
& r1(X0,X24) )
& ? [X23] :
( p104(X23)
& ~ p105(X23)
& ~ p5(X23)
& r1(X0,X23) ) ) )
& ( ~ p104(X0)
| p105(X0)
| ( ? [X22] :
( p105(X22)
& p6(X22)
& r1(X0,X22) )
& ? [X21] :
( p105(X21)
& ~ p6(X21)
& r1(X0,X21) ) ) )
& ! [X20] :
( sP11(X20)
| ~ r1(X0,X20) )
& ! [X18] :
( ! [X19] :
( sP23(X19)
| ~ r1(X18,X19) )
| ~ r1(X0,X18) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( sP35(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X0,X15) )
& ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X14] :
( sP47(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X0,X11) )
& ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ! [X10] :
( sP59(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X0,X6) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( p3(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f68]) ).
fof(f215,plain,
( p100(sK110)
& ~ p101(sK110)
& ( ~ p101(sK110)
| p100(sK110) )
& ( ~ p102(sK110)
| p101(sK110) )
& ( ~ p103(sK110)
| p102(sK110) )
& ( ~ p104(sK110)
| p103(sK110) )
& ( ~ p105(sK110)
| p104(sK110) )
& ( ~ p100(sK110)
| ( ( ~ p1(sK110)
| ! [X42] :
( ~ p100(X42)
| p1(X42)
| ~ r1(sK110,X42) ) )
& ( p1(sK110)
| ! [X41] :
( ~ p100(X41)
| ~ p1(X41)
| ~ r1(sK110,X41) ) ) ) )
& ( ~ p101(sK110)
| ( ( ~ p2(sK110)
| ! [X40] :
( ~ p101(X40)
| p2(X40)
| ~ r1(sK110,X40) ) )
& ( p2(sK110)
| ! [X39] :
( ~ p101(X39)
| ~ p2(X39)
| ~ r1(sK110,X39) ) ) ) )
& ( ~ p102(sK110)
| ( ( ~ p3(sK110)
| ! [X38] :
( ~ p102(X38)
| p3(X38)
| ~ r1(sK110,X38) ) )
& ( p3(sK110)
| ! [X37] :
( ~ p102(X37)
| ~ p3(X37)
| ~ r1(sK110,X37) ) ) ) )
& ( ~ p103(sK110)
| ( ( ~ p4(sK110)
| ! [X36] :
( ~ p103(X36)
| p4(X36)
| ~ r1(sK110,X36) ) )
& ( p4(sK110)
| ! [X35] :
( ~ p103(X35)
| ~ p4(X35)
| ~ r1(sK110,X35) ) ) ) )
& ( ~ p104(sK110)
| ( ( ~ p5(sK110)
| ! [X34] :
( ~ p104(X34)
| p5(X34)
| ~ r1(sK110,X34) ) )
& ( p5(sK110)
| ! [X33] :
( ~ p104(X33)
| ~ p5(X33)
| ~ r1(sK110,X33) ) ) ) )
& ( ~ p105(sK110)
| ( ( ~ p6(sK110)
| ! [X32] :
( ~ p105(X32)
| p6(X32)
| ~ r1(sK110,X32) ) )
& ( p6(sK110)
| ! [X31] :
( ~ p105(X31)
| ~ p6(X31)
| ~ r1(sK110,X31) ) ) ) )
& ( ~ p100(sK110)
| p101(sK110)
| ( p101(sK120)
& ~ p102(sK120)
& p2(sK120)
& r1(sK110,sK120)
& p101(sK119)
& ~ p102(sK119)
& ~ p2(sK119)
& r1(sK110,sK119) ) )
& ( ~ p101(sK110)
| p102(sK110)
| ( p102(sK118)
& ~ p103(sK118)
& p3(sK118)
& r1(sK110,sK118)
& p102(sK117)
& ~ p103(sK117)
& ~ p3(sK117)
& r1(sK110,sK117) ) )
& ( ~ p102(sK110)
| p103(sK110)
| ( p103(sK116)
& ~ p104(sK116)
& p4(sK116)
& r1(sK110,sK116)
& p103(sK115)
& ~ p104(sK115)
& ~ p4(sK115)
& r1(sK110,sK115) ) )
& ( ~ p103(sK110)
| p104(sK110)
| ( p104(sK114)
& ~ p105(sK114)
& p5(sK114)
& r1(sK110,sK114)
& p104(sK113)
& ~ p105(sK113)
& ~ p5(sK113)
& r1(sK110,sK113) ) )
& ( ~ p104(sK110)
| p105(sK110)
| ( p105(sK112)
& p6(sK112)
& r1(sK110,sK112)
& p105(sK111)
& ~ p6(sK111)
& r1(sK110,sK111) ) )
& ! [X20] :
( sP11(X20)
| ~ r1(sK110,X20) )
& ! [X18] :
( ! [X19] :
( sP23(X19)
| ~ r1(X18,X19) )
| ~ r1(sK110,X18) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( sP35(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(sK110,X15) )
& ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X14] :
( sP47(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(sK110,X11) )
& ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ! [X10] :
( sP59(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(sK110,X6) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( p3(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(sK110,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110,sK111,sK112,sK113,sK114,sK115,sK116,sK117,sK118,sK119,sK120]),skolemize(X0,sK110),skolemize(X21,sK111),skolemize(X22,sK112),skolemize(X23,sK113),skolemize(X24,sK114),skolemize(X25,sK115),skolemize(X26,sK116),skolemize(X27,sK117),skolemize(X28,sK118),skolemize(X29,sK119),skolemize(X30,sK120)],[f214]) ).
fof(f218,plain,
! [X0] :
( ~ sP59(X0)
| ~ p103(X0)
| p102(X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f219,plain,
! [X0] :
( ~ sP59(X0)
| ~ p104(X0)
| p103(X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f220,plain,
! [X0] :
( ~ sP59(X0)
| ~ p105(X0)
| p104(X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f284,plain,
! [X0] :
( ~ sP47(X0)
| ~ p103(X0)
| p102(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f285,plain,
! [X0] :
( ~ sP47(X0)
| ~ p104(X0)
| p103(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f289,plain,
! [X0] :
( ~ sP47(X0)
| sP43(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f297,plain,
! [X0] :
( ~ sP47(X0)
| sP40(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f305,plain,
! [X0,X1] :
( ~ sP43(X0)
| ~ p102(X0)
| p3(X0)
| ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f310,plain,
! [X0] :
( ~ sP40(X0)
| ~ p104(X0)
| p105(X0)
| p105(sK71(X0)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f312,plain,
! [X0] :
( ~ sP40(X0)
| ~ p104(X0)
| p105(X0)
| r1(X0,sK71(X0)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f350,plain,
! [X0] :
( ~ sP35(X0)
| ~ p103(X0)
| p102(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f355,plain,
! [X0] :
( ~ sP35(X0)
| sP31(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f362,plain,
! [X0] :
( ~ sP35(X0)
| sP27(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f371,plain,
! [X0,X1] :
( ~ sP31(X0)
| ~ p102(X0)
| p3(X0)
| ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f136]) ).
fof(f382,plain,
! [X0] :
( ~ sP27(X0)
| ~ p103(X0)
| p104(X0)
| p104(sK83(X0)) ),
inference(cnf_transformation,[],[f146]) ).
fof(f383,plain,
! [X0] :
( ~ sP27(X0)
| ~ p103(X0)
| p104(X0)
| ~ p105(sK83(X0)) ),
inference(cnf_transformation,[],[f146]) ).
fof(f385,plain,
! [X0] :
( ~ sP27(X0)
| ~ p103(X0)
| p104(X0)
| r1(X0,sK83(X0)) ),
inference(cnf_transformation,[],[f146]) ).
fof(f421,plain,
! [X0] :
( ~ sP23(X0)
| sP19(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f427,plain,
! [X0] :
( ~ sP23(X0)
| sP14(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f437,plain,
! [X0,X1] :
( ~ sP19(X0)
| ~ p102(X0)
| p3(X0)
| ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f165]) ).
fof(f456,plain,
! [X0] :
( ~ sP14(X0)
| ~ p102(X0)
| p103(X0)
| p103(sK95(X0)) ),
inference(cnf_transformation,[],[f178]) ).
fof(f457,plain,
! [X0] :
( ~ sP14(X0)
| ~ p102(X0)
| p103(X0)
| ~ p104(sK95(X0)) ),
inference(cnf_transformation,[],[f178]) ).
fof(f459,plain,
! [X0] :
( ~ sP14(X0)
| ~ p102(X0)
| p103(X0)
| r1(X0,sK95(X0)) ),
inference(cnf_transformation,[],[f178]) ).
fof(f492,plain,
! [X0] :
( ~ sP11(X0)
| sP1(X0) ),
inference(cnf_transformation,[],[f186]) ).
fof(f534,plain,
! [X0] :
( ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| p102(sK106(X0)) ),
inference(cnf_transformation,[],[f210]) ).
fof(f535,plain,
! [X0] :
( ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| ~ p103(sK106(X0)) ),
inference(cnf_transformation,[],[f210]) ).
fof(f536,plain,
! [X0] :
( ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| ~ p3(sK106(X0)) ),
inference(cnf_transformation,[],[f210]) ).
fof(f537,plain,
! [X0] :
( ~ sP1(X0)
| ~ p101(X0)
| p102(X0)
| r1(X0,sK106(X0)) ),
inference(cnf_transformation,[],[f210]) ).
fof(f546,plain,
p100(sK110),
inference(cnf_transformation,[],[f215]) ).
fof(f547,plain,
~ p101(sK110),
inference(cnf_transformation,[],[f215]) ).
fof(f569,plain,
( ~ p100(sK110)
| p101(sK110)
| p101(sK119) ),
inference(cnf_transformation,[],[f215]) ).
fof(f570,plain,
( ~ p100(sK110)
| p101(sK110)
| ~ p102(sK119) ),
inference(cnf_transformation,[],[f215]) ).
fof(f572,plain,
( ~ p100(sK110)
| p101(sK110)
| r1(sK110,sK119) ),
inference(cnf_transformation,[],[f215]) ).
fof(f603,plain,
! [X20] :
( sP11(X20)
| ~ r1(sK110,X20) ),
inference(cnf_transformation,[],[f215]) ).
fof(f604,plain,
! [X18,X19] :
( sP23(X19)
| ~ r1(X18,X19)
| ~ r1(sK110,X18) ),
inference(cnf_transformation,[],[f215]) ).
fof(f605,plain,
! [X16,X17,X15] :
( sP35(X17)
| ~ r1(X16,X17)
| ~ r1(X15,X16)
| ~ r1(sK110,X15) ),
inference(cnf_transformation,[],[f215]) ).
fof(f606,plain,
! [X11,X14,X12,X13] :
( sP47(X14)
| ~ r1(X13,X14)
| ~ r1(X12,X13)
| ~ r1(X11,X12)
| ~ r1(sK110,X11) ),
inference(cnf_transformation,[],[f215]) ).
fof(f607,plain,
! [X10,X8,X6,X9,X7] :
( sP59(X10)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(sK110,X6) ),
inference(cnf_transformation,[],[f215]) ).
fof(f608,plain,
! [X2,X3,X1,X4,X5] :
( p3(X5)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK110,X1) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_60,plain,
! [X0: $i] :
( p104(X0)
| ~ p105(X0)
| ~ sP59(X0) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_61,plain,
! [X0: $i] :
( p103(X0)
| ~ p104(X0)
| ~ sP59(X0) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_62,plain,
! [X0: $i] :
( p102(X0)
| ~ p103(X0)
| ~ sP59(X0) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_115,plain,
! [X0: $i] :
( sP40(X0)
| ~ sP47(X0) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_123,plain,
! [X0: $i] :
( sP43(X0)
| ~ sP47(X0) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_127,plain,
! [X0: $i] :
( p103(X0)
| ~ sP47(X0)
| ~ p104(X0) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_128,plain,
! [X0: $i] :
( p102(X0)
| ~ sP47(X0)
| ~ p103(X0) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i] :
( p3(X0)
| ~ sP43(X0)
| ~ p3(X1)
| ~ p102(X1)
| ~ p102(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_146,plain,
! [X0: $i] :
( p105(X0)
| r1(X0,sK71(X0))
| ~ sP40(X0)
| ~ p104(X0) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_148,plain,
! [X0: $i] :
( p105(X0)
| p105(sK71(X0))
| ~ sP40(X0)
| ~ p104(X0) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_182,plain,
! [X0: $i] :
( sP27(X0)
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_189,plain,
! [X0: $i] :
( sP31(X0)
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f355]) ).
tcf(c_194,plain,
! [X0: $i] :
( p102(X0)
| ~ sP35(X0)
| ~ p103(X0) ),
inference(cnf_transformation,[],[f350]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i] :
( p3(X0)
| ~ sP31(X0)
| ~ p3(X1)
| ~ p102(X1)
| ~ p102(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_219,plain,
! [X0: $i] :
( p104(X0)
| r1(X0,sK83(X0))
| ~ sP27(X0)
| ~ p103(X0) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_221,plain,
! [X0: $i] :
( p104(X0)
| ~ sP27(X0)
| ~ p103(X0)
| ~ p105(sK83(X0)) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_222,plain,
! [X0: $i] :
( p104(X0)
| p104(sK83(X0))
| ~ sP27(X0)
| ~ p103(X0) ),
inference(cnf_transformation,[],[f382]) ).
tcf(c_249,plain,
! [X0: $i] :
( sP14(X0)
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f427]) ).
tcf(c_255,plain,
! [X0: $i] :
( sP19(X0)
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f421]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i] :
( p3(X0)
| ~ sP19(X0)
| ~ p3(X1)
| ~ p102(X1)
| ~ p102(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f437]) ).
tcf(c_293,plain,
! [X0: $i] :
( p103(X0)
| r1(X0,sK95(X0))
| ~ sP14(X0)
| ~ p102(X0) ),
inference(cnf_transformation,[],[f459]) ).
tcf(c_295,plain,
! [X0: $i] :
( p103(X0)
| ~ sP14(X0)
| ~ p102(X0)
| ~ p104(sK95(X0)) ),
inference(cnf_transformation,[],[f457]) ).
tcf(c_296,plain,
! [X0: $i] :
( p103(X0)
| p103(sK95(X0))
| ~ sP14(X0)
| ~ p102(X0) ),
inference(cnf_transformation,[],[f456]) ).
tcf(c_316,plain,
! [X0: $i] :
( sP1(X0)
| ~ sP11(X0) ),
inference(cnf_transformation,[],[f492]) ).
tcf(c_363,plain,
! [X0: $i] :
( p102(X0)
| r1(X0,sK106(X0))
| ~ sP1(X0)
| ~ p101(X0) ),
inference(cnf_transformation,[],[f537]) ).
tcf(c_364,plain,
! [X0: $i] :
( p102(X0)
| ~ sP1(X0)
| ~ p101(X0)
| ~ p3(sK106(X0)) ),
inference(cnf_transformation,[],[f536]) ).
tcf(c_365,plain,
! [X0: $i] :
( p102(X0)
| ~ sP1(X0)
| ~ p101(X0)
| ~ p103(sK106(X0)) ),
inference(cnf_transformation,[],[f535]) ).
tcf(c_366,plain,
! [X0: $i] :
( p102(X0)
| p102(sK106(X0))
| ~ sP1(X0)
| ~ p101(X0) ),
inference(cnf_transformation,[],[f534]) ).
tcf(c_379,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p3(X4)
| ~ r1(sK110,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f608]) ).
tcf(c_380,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP59(X4)
| ~ r1(sK110,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f607]) ).
tcf(c_381,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP47(X3)
| ~ r1(sK110,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f606]) ).
tcf(c_382,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP35(X2)
| ~ r1(sK110,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f605]) ).
tcf(c_383,negated_conjecture,
! [X0: $i,X1: $i] :
( sP23(X1)
| ~ r1(sK110,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f604]) ).
tcf(c_384,negated_conjecture,
! [X0: $i] :
( sP11(X0)
| ~ r1(sK110,X0) ),
inference(cnf_transformation,[],[f603]) ).
tcf(c_415,negated_conjecture,
( p101(sK110)
| r1(sK110,sK119)
| ~ p100(sK110) ),
inference(cnf_transformation,[],[f572]) ).
tcf(c_417,negated_conjecture,
( p101(sK110)
| ~ p100(sK110)
| ~ p102(sK119) ),
inference(cnf_transformation,[],[f570]) ).
tcf(c_418,negated_conjecture,
( p101(sK119)
| p101(sK110)
| ~ p100(sK110) ),
inference(cnf_transformation,[],[f569]) ).
tcf(c_440,negated_conjecture,
~ p101(sK110),
inference(cnf_transformation,[],[f547]) ).
tcf(c_441,negated_conjecture,
p100(sK110),
inference(cnf_transformation,[],[f546]) ).
tcf(c_763,plain,
( sP11(sK119)
| ~ r1(sK110,sK119) ),
inference(instantiation,[status(thm)],[c_384]) ).
tcf(c_765,plain,
! [X0: $i] :
( sP23(X0)
| ~ r1(sK110,sK119)
| ~ r1(sK119,X0) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i] :
( sP35(X1)
| ~ r1(sK110,sK119)
| ~ r1(sK119,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_382]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP47(X2)
| ~ r1(sK110,sK119)
| ~ r1(sK119,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_773,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p3(X3)
| ~ r1(sK110,sK119)
| ~ r1(sK119,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_775,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP59(X3)
| ~ r1(sK110,sK119)
| ~ r1(sK119,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_380]) ).
tcf(c_787,plain,
( sP1(sK119)
| ~ sP11(sK119) ),
inference(instantiation,[status(thm)],[c_316]) ).
tcf(c_824,plain,
( p102(sK119)
| r1(sK119,sK106(sK119))
| ~ sP1(sK119)
| ~ p101(sK119) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_828,plain,
( p102(sK119)
| p102(sK106(sK119))
| ~ sP1(sK119)
| ~ p101(sK119) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_829,plain,
( p102(sK119)
| ~ sP1(sK119)
| ~ p101(sK119)
| ~ p103(sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_365]) ).
tcf(c_830,plain,
( p102(sK119)
| ~ sP1(sK119)
| ~ p101(sK119)
| ~ p3(sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_364]) ).
tcf(c_907,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP59(X2)
| ~ r1(sK110,sK119)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),X0) ),
inference(instantiation,[status(thm)],[c_775]) ).
tcf(c_908,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2)
| ~ r1(sK110,sK119)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),X0) ),
inference(instantiation,[status(thm)],[c_773]) ).
tcf(c_909,plain,
! [X0: $i,X1: $i] :
( sP47(X1)
| ~ r1(sK110,sK119)
| ~ r1(X0,X1)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),X0) ),
inference(instantiation,[status(thm)],[c_771]) ).
tcf(c_910,plain,
! [X0: $i] :
( sP35(X0)
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),X0) ),
inference(instantiation,[status(thm)],[c_769]) ).
tcf(c_911,plain,
( sP23(sK106(sK119))
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_765]) ).
tcf(c_987,plain,
( sP19(sK106(sK119))
| ~ sP23(sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_255]) ).
tcf(c_993,plain,
( sP14(sK106(sK119))
| ~ sP23(sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_1168,plain,
( p103(sK106(sK119))
| r1(sK106(sK119),sK95(sK106(sK119)))
| ~ sP14(sK106(sK119))
| ~ p102(sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_293]) ).
tcf(c_1170,plain,
( p103(sK106(sK119))
| p103(sK95(sK106(sK119)))
| ~ sP14(sK106(sK119))
| ~ p102(sK106(sK119)) ),
inference(instantiation,[status(thm)],[c_296]) ).
tcf(c_1171,plain,
( p103(sK106(sK119))
| ~ sP14(sK106(sK119))
| ~ p102(sK106(sK119))
| ~ p104(sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_1542,plain,
! [X0: $i,X1: $i] :
( p3(X1)
| ~ r1(sK110,sK119)
| ~ r1(X0,X1)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK95(sK106(sK119)),X0)
| ~ r1(sK106(sK119),sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_908]) ).
tcf(c_1543,plain,
! [X0: $i,X1: $i] :
( sP59(X1)
| ~ r1(sK110,sK119)
| ~ r1(X0,X1)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK95(sK106(sK119)),X0)
| ~ r1(sK106(sK119),sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_1544,plain,
! [X0: $i] :
( sP47(X0)
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK95(sK106(sK119)),X0)
| ~ r1(sK106(sK119),sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_909]) ).
tcf(c_1545,plain,
( sP35(sK95(sK106(sK119)))
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_910]) ).
tcf(c_1901,plain,
( p102(sK95(sK106(sK119)))
| ~ sP35(sK95(sK106(sK119)))
| ~ p103(sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_1905,plain,
( sP31(sK95(sK106(sK119)))
| ~ sP35(sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_1912,plain,
( sP27(sK95(sK106(sK119)))
| ~ sP35(sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_182]) ).
tcf(c_5479,plain,
! [X0: $i] :
( p3(sK95(sK106(sK119)))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP31(sK95(sK106(sK119)))
| ~ p102(sK95(sK106(sK119)))
| ~ r1(sK95(sK106(sK119)),X0) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_5607,plain,
( p104(sK95(sK106(sK119)))
| r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119))))
| ~ sP27(sK95(sK106(sK119)))
| ~ p103(sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_5609,plain,
( p104(sK95(sK106(sK119)))
| p104(sK83(sK95(sK106(sK119))))
| ~ sP27(sK95(sK106(sK119)))
| ~ p103(sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_222]) ).
tcf(c_5610,plain,
( p104(sK95(sK106(sK119)))
| ~ sP27(sK95(sK106(sK119)))
| ~ p103(sK95(sK106(sK119)))
| ~ p105(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_221]) ).
tcf(c_7668,plain,
! [X0: $i] :
( sP59(X0)
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),sK95(sK106(sK119)))
| ~ r1(sK83(sK95(sK106(sK119))),X0)
| ~ r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_1543]) ).
tcf(c_7669,plain,
! [X0: $i] :
( p3(X0)
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),sK95(sK106(sK119)))
| ~ r1(sK83(sK95(sK106(sK119))),X0)
| ~ r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_1542]) ).
tcf(c_7670,plain,
( sP47(sK83(sK95(sK106(sK119))))
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),sK95(sK106(sK119)))
| ~ r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_1544]) ).
tcf(c_8863,plain,
( p3(sK95(sK106(sK119)))
| ~ sP31(sK95(sK106(sK119)))
| ~ p102(sK95(sK106(sK119)))
| ~ p3(sK83(sK95(sK106(sK119))))
| ~ p102(sK83(sK95(sK106(sK119))))
| ~ r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_5479]) ).
tcf(c_9171,plain,
( p102(sK83(sK95(sK106(sK119))))
| ~ sP47(sK83(sK95(sK106(sK119))))
| ~ p103(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_9172,plain,
( p103(sK83(sK95(sK106(sK119))))
| ~ sP47(sK83(sK95(sK106(sK119))))
| ~ p104(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_9175,plain,
( sP43(sK83(sK95(sK106(sK119))))
| ~ sP47(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_9183,plain,
( sP40(sK83(sK95(sK106(sK119))))
| ~ sP47(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_12053,plain,
! [X0: $i] :
( p3(sK83(sK95(sK106(sK119))))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP43(sK83(sK95(sK106(sK119))))
| ~ p102(sK83(sK95(sK106(sK119))))
| ~ r1(sK83(sK95(sK106(sK119))),X0) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_12244,plain,
( p105(sK83(sK95(sK106(sK119))))
| r1(sK83(sK95(sK106(sK119))),sK71(sK83(sK95(sK106(sK119)))))
| ~ sP40(sK83(sK95(sK106(sK119))))
| ~ p104(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_12246,plain,
( p105(sK83(sK95(sK106(sK119))))
| p105(sK71(sK83(sK95(sK106(sK119)))))
| ~ sP40(sK83(sK95(sK106(sK119))))
| ~ p104(sK83(sK95(sK106(sK119)))) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_15528,plain,
( p3(sK71(sK83(sK95(sK106(sK119)))))
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),sK95(sK106(sK119)))
| ~ r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119))))
| ~ r1(sK83(sK95(sK106(sK119))),sK71(sK83(sK95(sK106(sK119))))) ),
inference(instantiation,[status(thm)],[c_7669]) ).
tcf(c_15529,plain,
( sP59(sK71(sK83(sK95(sK106(sK119)))))
| ~ r1(sK110,sK119)
| ~ r1(sK119,sK106(sK119))
| ~ r1(sK106(sK119),sK95(sK106(sK119)))
| ~ r1(sK95(sK106(sK119)),sK83(sK95(sK106(sK119))))
| ~ r1(sK83(sK95(sK106(sK119))),sK71(sK83(sK95(sK106(sK119))))) ),
inference(instantiation,[status(thm)],[c_7668]) ).
tcf(c_15532,plain,
( p104(sK71(sK83(sK95(sK106(sK119)))))
| ~ p105(sK71(sK83(sK95(sK106(sK119)))))
| ~ sP59(sK71(sK83(sK95(sK106(sK119))))) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_17295,plain,
( p3(sK83(sK95(sK106(sK119))))
| ~ sP43(sK83(sK95(sK106(sK119))))
| ~ p102(sK83(sK95(sK106(sK119))))
| ~ p3(sK71(sK83(sK95(sK106(sK119)))))
| ~ p102(sK71(sK83(sK95(sK106(sK119)))))
| ~ r1(sK83(sK95(sK106(sK119))),sK71(sK83(sK95(sK106(sK119))))) ),
inference(instantiation,[status(thm)],[c_12053]) ).
tcf(c_25191,plain,
( p103(sK71(sK83(sK95(sK106(sK119)))))
| ~ p104(sK71(sK83(sK95(sK106(sK119)))))
| ~ sP59(sK71(sK83(sK95(sK106(sK119))))) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_35173,plain,
( p102(sK71(sK83(sK95(sK106(sK119)))))
| ~ p103(sK71(sK83(sK95(sK106(sK119)))))
| ~ sP59(sK71(sK83(sK95(sK106(sK119))))) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_37271,plain,
! [X0: $i] :
( p3(sK106(sK119))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP19(sK106(sK119))
| ~ p102(sK106(sK119))
| ~ r1(sK106(sK119),X0) ),
inference(instantiation,[status(thm)],[c_269]) ).
tcf(c_39795,plain,
( p3(sK106(sK119))
| ~ sP19(sK106(sK119))
| ~ p102(sK106(sK119))
| ~ p3(sK95(sK106(sK119)))
| ~ p102(sK95(sK106(sK119)))
| ~ r1(sK106(sK119),sK95(sK106(sK119))) ),
inference(instantiation,[status(thm)],[c_37271]) ).
tcf(c_39798,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_39795,c_35173,c_25191,c_17295,c_15532,c_15528,c_15529,c_12244,c_12246,c_9171,c_9172,c_9175,c_9183,c_8863,c_7670,c_5607,c_5609,c_5610,c_1901,c_1905,c_1912,c_1545,c_1168,c_1170,c_1171,c_987,c_993,c_911,c_824,c_828,c_829,c_830,c_787,c_763,c_415,c_417,c_418,c_440,c_441]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.37 % Computer : n010.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Wed Sep 23 23:50:27 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/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.14/0.42
% 0.14/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.42
% 0.14/0.42 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 31.97/5.34 % SZS status Started for theBenchmark.p
% 31.97/5.34 % SZS status Theorem for theBenchmark.p
% 31.97/5.34
% 31.97/5.34 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 31.97/5.34
% 31.97/5.34 % ------ iProver source info
% 31.97/5.34
% 31.97/5.34 % git: date: 2026-07-19 20:42:38 +0200
% 31.97/5.34 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 31.97/5.34 % git: non_committed_changes: false
% 31.97/5.34
% 31.97/5.34 % ------ Parsing...
% 31.97/5.34 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 31.97/5.34
% 31.97/5.34 % ------ Preprocessing... sf_s rm: 17 0s sf_e sf_s rm: 0 0s sf_e %
% 31.97/5.34
% 31.97/5.34 % ------ Preprocessing...
% 31.97/5.34 % ------ Proving...
% 31.97/5.34 % ------ Problem Properties
% 31.97/5.34
% 31.97/5.34 %
% 31.97/5.34 % clauses 335
% 31.97/5.34 % conjectures 20
% 31.97/5.34 % EPR 145
% 31.97/5.34 % Horn 210
% 31.97/5.34 % unary 14
% 31.97/5.34 % binary 51
% 31.97/5.34 % lits 1275
% 31.97/5.34 % lits eq 0
% 31.97/5.34 % fd_pure 0
% 31.97/5.34 % fd_pseudo 0
% 31.97/5.34 % fd_cond 0
% 31.97/5.34 % fd_pseudo_cond 0
% 31.97/5.34 % AC symbols 0
% 31.97/5.34
% 31.97/5.34 % ------ Input Options Time Limit: Unbounded
% 31.97/5.34
% 31.97/5.34
% 31.97/5.34 % ------
% 31.97/5.34 % Current options:
% 31.97/5.34 % ------
% 31.97/5.34
% 31.97/5.34
% 31.97/5.34 %
% 31.97/5.34
% 31.97/5.34 % ------ Proving...
% 31.97/5.34 %
% 31.97/5.34
% 31.97/5.34 % SZS status Theorem for theBenchmark.p
% 31.97/5.34
% 31.97/5.34 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 31.97/5.34
% 31.97/5.34
%------------------------------------------------------------------------------