%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL660+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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:07:48 PM UTC 2026
% Result : Theorem 11.77s 3.87s
% Output : CNFRefutation 11.77s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f30ERROR: Could not build tree for root c_48627ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f33,plain,
! [X0] :
( ~ sP22(X0)
| ( ! [X13] :
( ? [X14] :
( p2(X14)
& ? [X15] :
( ~ p2(X15)
& r1(X14,X15) )
& r1(X13,X14) )
| p2(X13)
| ~ r1(X0,X13) )
& ? [X12] :
( ~ p2(X12)
& r1(X0,X12) ) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f34,plain,
! [X0] :
( ~ sP22(X0)
| ( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] :
( ~ p2(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p2(X2)
| ~ r1(X0,X2) )
& ? [X1] :
( ~ p2(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f33]) ).
fof(f35,plain,
! [X0] :
( ~ sP22(X0)
| ( ! [X2] :
( ( p2(sK24(X2))
& ~ p2(sK25(X2))
& r1(sK24(X2),sK25(X2))
& r1(X2,sK24(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK23(X0))
& r1(X0,sK23(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24,sK25]),skolemize(X1,sK23(X0)),skolemize(X3,sK24(X2)),skolemize(X4,sK25(X2))],[f34]) ).
fof(f36,plain,
! [X0] :
( ~ sP21(X0)
| ( ( ? [X27] :
( p2(X27)
& ? [X28] :
( ~ p2(X28)
& r1(X27,X28) )
& r1(X0,X27) )
| p2(X0) )
& ( ? [X24] :
( ! [X25] :
( ~ p2(X25)
| ! [X26] :
( p2(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
& ~ p2(X24)
& r1(X0,X24) )
| sP20(X0) ) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f37,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,[],[f36]) ).
fof(f38,plain,
! [X0] :
( ~ sP21(X0)
| ( ( ( p2(sK27(X0))
& ~ p2(sK28(X0))
& r1(sK27(X0),sK28(X0))
& r1(X0,sK27(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK26(X0),X2) )
& ~ p2(sK26(X0))
& r1(X0,sK26(X0)) )
| sP20(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27,sK28]),skolemize(X1,sK26(X0)),skolemize(X4,sK27(X0)),skolemize(X5,sK28(X0))],[f37]) ).
fof(f39,plain,
! [X0] :
( ~ sP20(X0)
| ! [X20] :
( ! [X21] :
( ? [X22] :
( p2(X22)
& ? [X23] :
( ~ p2(X23)
& r1(X22,X23) )
& r1(X21,X22) )
| p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X0,X20) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f40,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,[],[f39]) ).
fof(f41,plain,
! [X0] :
( ~ sP20(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK29(X2))
& ~ p2(sK30(X2))
& r1(sK29(X2),sK30(X2))
& r1(X2,sK29(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29,sK30]),skolemize(X3,sK29(X2)),skolemize(X4,sK30(X2))],[f40]) ).
fof(f42,plain,
! [X29] :
( ~ sP19(X29)
| ( ! [X34] :
( ? [X35] :
( p2(X35)
& ? [X36] :
( ~ p2(X36)
& r1(X35,X36) )
& r1(X34,X35) )
| p2(X34)
| ~ r1(X29,X34) )
& ? [X30] :
( ? [X31] :
( ! [X32] :
( ~ p2(X32)
| ! [X33] :
( p2(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
& ~ p2(X31)
& r1(X30,X31) )
& r1(X29,X30) ) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f43,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,[],[f42]) ).
fof(f44,plain,
! [X0] :
( ~ sP19(X0)
| ( ! [X5] :
( ( p2(sK33(X5))
& ~ p2(sK34(X5))
& r1(sK33(X5),sK34(X5))
& r1(X5,sK33(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK32(X0),X3) )
& ~ p2(sK32(X0))
& r1(sK31(X0),sK32(X0))
& r1(X0,sK31(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33,sK34]),skolemize(X1,sK31(X0)),skolemize(X2,sK32(X0)),skolemize(X6,sK33(X5)),skolemize(X7,sK34(X5))],[f43]) ).
fof(f45,plain,
! [X39] :
( ~ sP18(X39)
| ! [X40] :
( ( ( ? [X48] :
( p2(X48)
& ? [X49] :
( ~ p2(X49)
& r1(X48,X49) )
& r1(X40,X48) )
| p2(X40) )
& ( ? [X45] :
( ! [X46] :
( ~ p2(X46)
| ! [X47] :
( p2(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p2(X45)
& r1(X40,X45) )
| sP16(X40) ) )
| ~ r1(X39,X40) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f46,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,[],[f45]) ).
fof(f47,plain,
! [X0] :
( ~ sP18(X0)
| ! [X1] :
( ( ( ( p2(sK36(X1))
& ~ p2(sK37(X1))
& r1(sK36(X1),sK37(X1))
& r1(X1,sK36(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK35(X1),X3) )
& ~ p2(sK35(X1))
& r1(X1,sK35(X1)) )
| sP16(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36,sK37]),skolemize(X2,sK35(X1)),skolemize(X5,sK36(X1)),skolemize(X6,sK37(X1))],[f46]) ).
fof(f48,plain,
! [X39] :
( ~ sP17(X39)
| ( ! [X54] :
( ? [X55] :
( p2(X55)
& ? [X56] :
( ~ p2(X56)
& r1(X55,X56) )
& r1(X54,X55) )
| p2(X54)
| ~ r1(X39,X54) )
& ? [X50] :
( ? [X51] :
( ! [X52] :
( ~ p2(X52)
| ! [X53] :
( p2(X53)
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
& ~ p2(X51)
& r1(X50,X51) )
& r1(X39,X50) ) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f49,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,[],[f48]) ).
fof(f50,plain,
! [X0] :
( ~ sP17(X0)
| ( ! [X5] :
( ( p2(sK40(X5))
& ~ p2(sK41(X5))
& r1(sK40(X5),sK41(X5))
& r1(X5,sK40(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK39(X0),X3) )
& ~ p2(sK39(X0))
& r1(sK38(X0),sK39(X0))
& r1(X0,sK38(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38,sK39,sK40,sK41]),skolemize(X1,sK38(X0)),skolemize(X2,sK39(X0)),skolemize(X6,sK40(X5)),skolemize(X7,sK41(X5))],[f49]) ).
fof(f100,plain,
? [X0] :
( ! [X58] :
( ? [X59] :
( ! [X60] :
( ~ p2(X60)
| ! [X61] :
( p2(X61)
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
& ~ p2(X59)
& r1(X58,X59) )
| p2(X58)
| ~ r1(X0,X58) )
& ( ? [X52] :
( ! [X54] :
( ( ? [X57] : r1(X54,X57)
& ~ p1(X54) )
| ! [X55] :
( ! [X56] : ~ r1(X55,X56)
| p1(X55)
| ~ r1(X54,X55) )
| ~ r1(X52,X54) )
& ? [X53] : r1(X52,X53)
& ~ p1(X52)
& r1(X0,X52) )
| ! [X51] : ~ r1(X0,X51)
| p1(X0) )
& ( ? [X45] :
( ! [X47] :
( ( ? [X50] : r1(X47,X50)
& ~ p1(X47)
& ~ p2(X47) )
| ! [X48] :
( ! [X49] : ~ r1(X48,X49)
| p1(X48)
| p2(X48)
| ~ r1(X47,X48) )
| ~ r1(X45,X47) )
& ? [X46] : r1(X45,X46)
& ~ p1(X45)
& ~ p2(X45)
& r1(X0,X45) )
| ! [X44] : ~ r1(X0,X44)
| p1(X0)
| p2(X0) )
& ( ? [X42] :
( sP0(X42)
& ? [X43] : r1(X42,X43)
& ~ p1(X42)
& ~ p2(X42)
& ~ p3(X42)
& r1(X0,X42) )
| ! [X41] : ~ r1(X0,X41)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X39] :
( sP1(X39)
& ? [X40] : r1(X39,X40)
& ~ p1(X39)
& ~ p2(X39)
& ~ p3(X39)
& ~ p4(X39)
& r1(X0,X39) )
| ! [X38] : ~ r1(X0,X38)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X37] :
( sP2(X37)
& sP3(X37)
& ~ p1(X37)
& r1(X0,X37) )
| ! [X35] :
( ! [X36] : ~ r1(X35,X36)
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X0,X35) )
| p1(X0) )
& ( ? [X34] :
( sP4(X34)
& sP5(X34)
& ~ p1(X34)
& ~ p2(X34)
& r1(X0,X34) )
| ! [X32] :
( ! [X33] : ~ r1(X32,X33)
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(X0,X32) )
| p1(X0)
| p2(X0) )
& ( ? [X31] :
( sP8(X31)
& sP7(X31)
& ~ p1(X31)
& ~ p2(X31)
& ~ p3(X31)
& r1(X0,X31) )
| ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X0,X29) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X28] :
( sP11(X28)
& sP10(X28)
& ~ p1(X28)
& ~ p2(X28)
& ~ p3(X28)
& ~ p4(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)
| p4(X0) )
& ( ? [X25] :
( sP14(X25)
& sP15(X25)
& ~ p1(X25)
& r1(X0,X25) )
| ! [X22] :
( ! [X23] :
( ! [X24] : ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X0,X22) )
| p1(X0) )
& ( ? [X16] :
( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP17(X19)
| sP18(X19)
| ~ r1(X16,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP19(X16) )
& r1(X0,X16) )
| sP21(X0) )
& ! [X13] :
( ? [X14] :
( p1(X14)
& ? [X15] :
( ~ p1(X15)
& r1(X14,X15) )
& r1(X13,X14) )
| p1(X13)
| ~ r1(X0,X13) )
& ? [X12] :
( ~ p1(X12)
& r1(X0,X12) )
& ( sP22(X0)
| ! [X10] :
( ? [X11] :
( p5(X11)
& r1(X10,X11) )
| ~ r1(X0,X10) ) )
& ! [X7] :
( ? [X8] :
( p3(X8)
& ? [X9] :
( ~ p3(X9)
& r1(X8,X9) )
& r1(X7,X8) )
| p3(X7)
| ~ r1(X0,X7) )
& ? [X6] :
( ~ p3(X6)
& r1(X0,X6) )
& ( ( ! [X3] :
( ? [X4] :
( p2(X4)
& ? [X5] :
( ~ p2(X5)
& r1(X4,X5) )
& r1(X3,X4) )
| p2(X3)
| ~ r1(X0,X3) )
& ? [X2] :
( ~ p2(X2)
& r1(X0,X2) ) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(X0,X1) ) ) ),
inference(rectify,[],[f32]) ).
fof(f101,plain,
( ! [X58] :
( ( ! [X60] :
( ~ p2(X60)
| ! [X61] :
( p2(X61)
| ~ r1(X60,X61) )
| ~ r1(sK95(X58),X60) )
& ~ p2(sK95(X58))
& r1(X58,sK95(X58)) )
| p2(X58)
| ~ r1(sK68,X58) )
& ( ( ! [X54] :
( ( r1(X54,sK94(X54))
& ~ p1(X54) )
| ! [X55] :
( ! [X56] : ~ r1(X55,X56)
| p1(X55)
| ~ r1(X54,X55) )
| ~ r1(sK92,X54) )
& r1(sK92,sK93)
& ~ p1(sK92)
& r1(sK68,sK92) )
| ! [X51] : ~ r1(sK68,X51)
| p1(sK68) )
& ( ( ! [X47] :
( ( r1(X47,sK91(X47))
& ~ p1(X47)
& ~ p2(X47) )
| ! [X48] :
( ! [X49] : ~ r1(X48,X49)
| p1(X48)
| p2(X48)
| ~ r1(X47,X48) )
| ~ r1(sK89,X47) )
& r1(sK89,sK90)
& ~ p1(sK89)
& ~ p2(sK89)
& r1(sK68,sK89) )
| ! [X44] : ~ r1(sK68,X44)
| p1(sK68)
| p2(sK68) )
& ( ( sP0(sK87)
& r1(sK87,sK88)
& ~ p1(sK87)
& ~ p2(sK87)
& ~ p3(sK87)
& r1(sK68,sK87) )
| ! [X41] : ~ r1(sK68,X41)
| p1(sK68)
| p2(sK68)
| p3(sK68) )
& ( ( sP1(sK85)
& r1(sK85,sK86)
& ~ p1(sK85)
& ~ p2(sK85)
& ~ p3(sK85)
& ~ p4(sK85)
& r1(sK68,sK85) )
| ! [X38] : ~ r1(sK68,X38)
| p1(sK68)
| p2(sK68)
| p3(sK68)
| p4(sK68) )
& ( ( sP2(sK84)
& sP3(sK84)
& ~ p1(sK84)
& r1(sK68,sK84) )
| ! [X35] :
( ! [X36] : ~ r1(X35,X36)
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(sK68,X35) )
| p1(sK68) )
& ( ( sP4(sK83)
& sP5(sK83)
& ~ p1(sK83)
& ~ p2(sK83)
& r1(sK68,sK83) )
| ! [X32] :
( ! [X33] : ~ r1(X32,X33)
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(sK68,X32) )
| p1(sK68)
| p2(sK68) )
& ( ( sP8(sK82)
& sP7(sK82)
& ~ p1(sK82)
& ~ p2(sK82)
& ~ p3(sK82)
& r1(sK68,sK82) )
| ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(sK68,X29) )
| p1(sK68)
| p2(sK68)
| p3(sK68) )
& ( ( sP11(sK81)
& sP10(sK81)
& ~ p1(sK81)
& ~ p2(sK81)
& ~ p3(sK81)
& ~ p4(sK81)
& r1(sK68,sK81) )
| ! [X26] :
( ! [X27] : ~ r1(X26,X27)
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(sK68,X26) )
| p1(sK68)
| p2(sK68)
| p3(sK68)
| p4(sK68) )
& ( ( sP14(sK80)
& sP15(sK80)
& ~ p1(sK80)
& r1(sK68,sK80) )
| ! [X22] :
( ! [X23] :
( ! [X24] : ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(sK68,X22) )
| p1(sK68) )
& ( ( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP17(X19)
| sP18(X19)
| ~ r1(sK79,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(sK79,X17) )
& ~ p2(sK79) )
| sP19(sK79) )
& r1(sK68,sK79) )
| sP21(sK68) )
& ! [X13] :
( ( p1(sK77(X13))
& ~ p1(sK78(X13))
& r1(sK77(X13),sK78(X13))
& r1(X13,sK77(X13)) )
| p1(X13)
| ~ r1(sK68,X13) )
& ~ p1(sK76)
& r1(sK68,sK76)
& ( sP22(sK68)
| ! [X10] :
( ( p5(sK75(X10))
& r1(X10,sK75(X10)) )
| ~ r1(sK68,X10) ) )
& ! [X7] :
( ( p3(sK73(X7))
& ~ p3(sK74(X7))
& r1(sK73(X7),sK74(X7))
& r1(X7,sK73(X7)) )
| p3(X7)
| ~ r1(sK68,X7) )
& ~ p3(sK72)
& r1(sK68,sK72)
& ( ( ! [X3] :
( ( p2(sK70(X3))
& ~ p2(sK71(X3))
& r1(sK70(X3),sK71(X3))
& r1(X3,sK70(X3)) )
| p2(X3)
| ~ r1(sK68,X3) )
& ~ p2(sK69)
& r1(sK68,sK69) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(sK68,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68,sK69,sK70,sK71,sK72,sK73,sK74,sK75,sK76,sK77,sK78,sK79,sK80,sK81,sK82,sK83,sK84,sK85,sK86,sK87,sK88,sK89,sK90,sK91,sK92,sK93,sK94,sK95]),skolemize(X0,sK68),skolemize(X2,sK69),skolemize(X4,sK70(X3)),skolemize(X5,sK71(X3)),skolemize(X6,sK72),skolemize(X8,sK73(X7)),skolemize(X9,sK74(X7)),skolemize(X11,sK75(X10)),skolemize(X12,sK76),skolemize(X14,sK77(X13)),skolemize(X15,sK78(X13)),skolemize(X16,sK79),skolemize(X25,sK80),skolemize(X28,sK81),skolemize(X31,sK82),skolemize(X34,sK83),skolemize(X37,sK84),skolemize(X39,sK85),skolemize(X40,sK86),skolemize(X42,sK87),skolemize(X43,sK88),skolemize(X45,sK89),skolemize(X46,sK90),skolemize(X50,sK91(X47)),skolemize(X52,sK92),skolemize(X53,sK93),skolemize(X57,sK94(X54)),skolemize(X59,sK95(X58))],[f100]) ).
fof(f102,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f103,plain,
! [X2,X0] :
( ~ sP22(X0)
| p2(sK24(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f104,plain,
! [X2,X0] :
( ~ sP22(X0)
| ~ p2(sK25(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f105,plain,
! [X2,X0] :
( ~ sP22(X0)
| r1(sK24(X2),sK25(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f106,plain,
! [X2,X0] :
( ~ sP22(X0)
| r1(X2,sK24(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f107,plain,
! [X0] :
( ~ sP22(X0)
| ~ p2(sK23(X0)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f108,plain,
! [X0] :
( ~ sP22(X0)
| r1(X0,sK23(X0)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f113,plain,
! [X2,X3,X0] :
( ~ sP21(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK26(X0),X2)
| sP20(X0) ),
inference(cnf_transformation,[],[f38]) ).
fof(f114,plain,
! [X0] :
( ~ sP21(X0)
| ~ p2(sK26(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f38]) ).
fof(f115,plain,
! [X0] :
( ~ sP21(X0)
| r1(X0,sK26(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f38]) ).
fof(f116,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| p2(sK29(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f117,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ p2(sK30(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f118,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| r1(sK29(X2),sK30(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f119,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| r1(X2,sK29(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f120,plain,
! [X0,X5] :
( ~ sP19(X0)
| p2(sK33(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f44]) ).
fof(f121,plain,
! [X0,X5] :
( ~ sP19(X0)
| ~ p2(sK34(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f44]) ).
fof(f122,plain,
! [X0,X5] :
( ~ sP19(X0)
| r1(sK33(X5),sK34(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f44]) ).
fof(f123,plain,
! [X0,X5] :
( ~ sP19(X0)
| r1(X5,sK33(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f44]) ).
fof(f124,plain,
! [X3,X0,X4] :
( ~ sP19(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK32(X0),X3) ),
inference(cnf_transformation,[],[f44]) ).
fof(f125,plain,
! [X0] :
( ~ sP19(X0)
| ~ p2(sK32(X0)) ),
inference(cnf_transformation,[],[f44]) ).
fof(f126,plain,
! [X0] :
( ~ sP19(X0)
| r1(sK31(X0),sK32(X0)) ),
inference(cnf_transformation,[],[f44]) ).
fof(f127,plain,
! [X0] :
( ~ sP19(X0)
| r1(X0,sK31(X0)) ),
inference(cnf_transformation,[],[f44]) ).
fof(f128,plain,
! [X0,X1] :
( ~ sP18(X0)
| p2(sK36(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f129,plain,
! [X0,X1] :
( ~ sP18(X0)
| ~ p2(sK37(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f130,plain,
! [X0,X1] :
( ~ sP18(X0)
| r1(sK36(X1),sK37(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f131,plain,
! [X0,X1] :
( ~ sP18(X0)
| r1(X1,sK36(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f135,plain,
! [X0,X5] :
( ~ sP17(X0)
| p2(sK40(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f50]) ).
fof(f136,plain,
! [X0,X5] :
( ~ sP17(X0)
| ~ p2(sK41(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f50]) ).
fof(f137,plain,
! [X0,X5] :
( ~ sP17(X0)
| r1(sK40(X5),sK41(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f50]) ).
fof(f138,plain,
! [X0,X5] :
( ~ sP17(X0)
| r1(X5,sK40(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f50]) ).
fof(f241,plain,
! [X58,X60,X61] :
( ~ p2(X60)
| p2(X61)
| ~ r1(X60,X61)
| ~ r1(sK95(X58),X60)
| p2(X58)
| ~ r1(sK68,X58) ),
inference(cnf_transformation,[],[f101]) ).
fof(f242,plain,
! [X58] :
( ~ p2(sK95(X58))
| p2(X58)
| ~ r1(sK68,X58) ),
inference(cnf_transformation,[],[f101]) ).
fof(f243,plain,
! [X58] :
( r1(X58,sK95(X58))
| p2(X58)
| ~ r1(sK68,X58) ),
inference(cnf_transformation,[],[f101]) ).
fof(f295,plain,
! [X21,X19,X20] :
( ~ p2(X20)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| sP17(X19)
| sP18(X19)
| ~ r1(sK79,X19)
| sP21(sK68) ),
inference(cnf_transformation,[],[f101]) ).
fof(f296,plain,
! [X19] :
( ~ p2(X19)
| sP17(X19)
| sP18(X19)
| ~ r1(sK79,X19)
| sP21(sK68) ),
inference(cnf_transformation,[],[f101]) ).
fof(f297,plain,
! [X18,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(sK79,X17)
| sP19(sK79)
| sP21(sK68) ),
inference(cnf_transformation,[],[f101]) ).
fof(f298,plain,
( ~ p2(sK79)
| sP19(sK79)
| sP21(sK68) ),
inference(cnf_transformation,[],[f101]) ).
fof(f299,plain,
( r1(sK68,sK79)
| sP21(sK68) ),
inference(cnf_transformation,[],[f101]) ).
fof(f306,plain,
! [X10] :
( sP22(sK68)
| p5(sK75(X10))
| ~ r1(sK68,X10) ),
inference(cnf_transformation,[],[f101]) ).
fof(f307,plain,
! [X10] :
( sP22(sK68)
| r1(X10,sK75(X10))
| ~ r1(sK68,X10) ),
inference(cnf_transformation,[],[f101]) ).
fof(f314,plain,
! [X3,X1] :
( p2(sK70(X3))
| p2(X3)
| ~ r1(sK68,X3)
| ~ p5(X1)
| ~ r1(sK68,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f315,plain,
! [X3,X1] :
( ~ p2(sK71(X3))
| p2(X3)
| ~ r1(sK68,X3)
| ~ p5(X1)
| ~ r1(sK68,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f316,plain,
! [X3,X1] :
( r1(sK70(X3),sK71(X3))
| p2(X3)
| ~ r1(sK68,X3)
| ~ p5(X1)
| ~ r1(sK68,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f317,plain,
! [X3,X1] :
( r1(X3,sK70(X3))
| p2(X3)
| ~ r1(sK68,X3)
| ~ p5(X1)
| ~ r1(sK68,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f318,plain,
! [X1] :
( ~ p2(sK69)
| ~ p5(X1)
| ~ r1(sK68,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f319,plain,
! [X1] :
( r1(sK68,sK69)
| ~ p5(X1)
| ~ r1(sK68,X1) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f102]) ).
tcf(c_50,plain,
! [X0: $i] :
( r1(X0,sK23(X0))
| ~ sP22(X0) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_51,plain,
! [X0: $i] :
( ~ sP22(X0)
| ~ p2(sK23(X0)) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK24(X1))
| ~ sP22(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK24(X1),sK25(X1))
| ~ sP22(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP22(X0)
| ~ p2(sK25(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK24(X1))
| ~ sP22(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_56,plain,
! [X0: $i] :
( sP20(X0)
| r1(X0,sK26(X0))
| ~ sP21(X0) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_57,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP21(X0)
| ~ p2(sK26(X0)) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP20(X0)
| p2(X2)
| ~ sP21(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK26(X0),X1) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK29(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK29(X2),sK30(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP20(X0)
| ~ p2(sK30(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK29(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_67,plain,
! [X0: $i] :
( r1(X0,sK31(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_68,plain,
! [X0: $i] :
( r1(sK31(X0),sK32(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_69,plain,
! [X0: $i] :
( ~ sP19(X0)
| ~ p2(sK32(X0)) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP19(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK32(X0),X1) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK33(X1))
| ~ sP19(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK33(X1),sK34(X1))
| ~ sP19(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP19(X0)
| ~ p2(sK34(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK33(X1))
| ~ sP19(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK36(X1))
| ~ sP18(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK36(X1),sK37(X1))
| ~ sP18(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP18(X0)
| ~ p2(sK37(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK36(X1))
| ~ sP18(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK40(X1))
| ~ sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK40(X1),sK41(X1))
| ~ sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP17(X0)
| ~ p2(sK41(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK40(X1))
| ~ sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_188,negated_conjecture,
! [X0: $i] :
( r1(sK68,sK69)
| ~ p5(X0)
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_189,negated_conjecture,
! [X0: $i] :
( ~ p2(sK69)
| ~ p5(X0)
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_190,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(X0,sK70(X0))
| ~ p5(X1)
| ~ r1(sK68,X1)
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_191,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(sK70(X0),sK71(X0))
| ~ p5(X1)
| ~ r1(sK68,X1)
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_192,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| ~ p5(X1)
| ~ p2(sK71(X0))
| ~ r1(sK68,X1)
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_193,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| p2(sK70(X0))
| ~ p5(X1)
| ~ r1(sK68,X1)
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_200,negated_conjecture,
! [X0: $i] :
( sP22(sK68)
| r1(X0,sK75(X0))
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_201,negated_conjecture,
! [X0: $i] :
( sP22(sK68)
| p5(sK75(X0))
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_208,negated_conjecture,
( sP21(sK68)
| r1(sK68,sK79) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_209,negated_conjecture,
( sP19(sK79)
| sP21(sK68)
| ~ p2(sK79) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_210,negated_conjecture,
! [X0: $i,X1: $i] :
( sP19(sK79)
| sP21(sK68)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK79,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_211,negated_conjecture,
! [X0: $i] :
( sP21(sK68)
| sP17(X0)
| sP18(X0)
| ~ p2(X0)
| ~ r1(sK79,X0) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_212,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP21(sK68)
| sP17(X0)
| sP18(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK79,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_264,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK95(X0))
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_265,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK95(X0))
| ~ r1(sK68,X0) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_266,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK68,X0)
| ~ r1(X1,X2)
| ~ r1(sK95(X0),X1) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_267,plain,
r1(sK68,sK68),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_318,plain,
( ~ sP22(sK68)
| ~ p2(sK23(sK68)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_319,plain,
( r1(sK68,sK23(sK68))
| ~ sP22(sK68) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_339,plain,
( sP20(sK68)
| ~ sP21(sK68)
| ~ p2(sK26(sK68)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_340,plain,
( sP20(sK68)
| r1(sK68,sK26(sK68))
| ~ sP21(sK68) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_345,plain,
( sP22(sK68)
| r1(sK68,sK75(sK68))
| ~ r1(sK68,sK68) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_2905,plain,
! [X0: $i] :
( sP22(sK68)
| ~ p2(sK69)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK75(X0)) ),
inference(resolution,[status(thm)],[c_189,c_201]) ).
tcf(c_2906,plain,
( sP22(sK68)
| ~ p2(sK69)
| ~ r1(sK68,sK68)
| ~ r1(sK68,sK75(sK68)) ),
inference(instantiation,[status(thm)],[c_2905]) ).
tcf(c_2907,plain,
( sP22(sK68)
| ~ p2(sK69) ),
inference(global_subsumption_just,[status(thm)],[c_2905,c_267,c_345,c_2906]) ).
tcf(c_2915,plain,
! [X0: $i] :
( sP22(sK68)
| r1(sK68,sK69)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK75(X0)) ),
inference(resolution,[status(thm)],[c_188,c_201]) ).
tcf(c_2916,plain,
( sP22(sK68)
| r1(sK68,sK69)
| ~ r1(sK68,sK68)
| ~ r1(sK68,sK75(sK68)) ),
inference(instantiation,[status(thm)],[c_2915]) ).
tcf(c_2917,plain,
( sP22(sK68)
| r1(sK68,sK69) ),
inference(global_subsumption_just,[status(thm)],[c_2915,c_267,c_345,c_2916]) ).
tcf(c_2925,plain,
! [X0: $i,X1: $i] :
( sP22(sK68)
| p2(X1)
| p2(sK70(X1))
| ~ r1(sK68,X1)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK75(X0)) ),
inference(resolution,[status(thm)],[c_193,c_201]) ).
tcf(c_2945,plain,
! [X0: $i,X1: $i] :
( sP22(sK68)
| p2(X1)
| ~ p2(sK71(X1))
| ~ r1(sK68,X1)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK75(X0)) ),
inference(resolution,[status(thm)],[c_192,c_201]) ).
tcf(c_2965,plain,
! [X0: $i,X1: $i] :
( sP22(sK68)
| p2(X1)
| r1(sK70(X1),sK71(X1))
| ~ r1(sK68,X1)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK75(X0)) ),
inference(resolution,[status(thm)],[c_191,c_201]) ).
tcf(c_2985,plain,
! [X0: $i,X1: $i] :
( sP22(sK68)
| p2(X1)
| r1(X1,sK70(X1))
| ~ r1(sK68,X1)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK75(X0)) ),
inference(resolution,[status(thm)],[c_190,c_201]) ).
tcf(c_3623,plain,
( sP21(sK68)
| ~ p2(sK79)
| ~ p2(sK32(sK79)) ),
inference(resolution,[status(thm)],[c_69,c_209]) ).
tcf(c_3652,plain,
( sP21(sK68)
| r1(sK31(sK79),sK32(sK79))
| ~ p2(sK79) ),
inference(resolution,[status(thm)],[c_68,c_209]) ).
tcf(c_3681,plain,
( sP21(sK68)
| r1(sK79,sK31(sK79))
| ~ p2(sK79) ),
inference(resolution,[status(thm)],[c_67,c_209]) ).
tcf(c_11726,plain,
! [X0: $i] :
( ~ iPr_def_10
| p2(X0)
| ~ r1(sK68,X0)
| r1(X0,sK70(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_2985]) ).
tcf(c_11727,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ r1(sK68,sK75(X0))
| ~ r1(sK68,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_2985]) ).
tcf(c_11728,plain,
( iPr_def_11
| iPr_def_10
| sP22(sK68) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2985]) ).
tcf(c_11729,plain,
! [X0: $i] :
( ~ iPr_def_12
| p2(X0)
| ~ r1(sK68,X0)
| r1(sK70(X0),sK71(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_2965]) ).
tcf(c_11730,plain,
( iPr_def_12
| iPr_def_11
| sP22(sK68) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2965]) ).
tcf(c_11731,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p2(sK71(X0))
| p2(X0)
| ~ r1(sK68,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_2945]) ).
tcf(c_11732,plain,
( iPr_def_13
| iPr_def_11
| sP22(sK68) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2945]) ).
tcf(c_11733,plain,
! [X0: $i] :
( ~ iPr_def_14
| p2(sK70(X0))
| p2(X0)
| ~ r1(sK68,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_2925]) ).
tcf(c_11734,plain,
( iPr_def_14
| iPr_def_11
| sP22(sK68) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2925]) ).
tcf(c_11735,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_15
| p2(X1)
| ~ p2(X0)
| ~ r1(sK79,X0)
| ~ r1(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_210]) ).
tcf(c_11736,negated_conjecture,
( iPr_def_15
| sP19(sK79)
| sP21(sK68) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_210]) ).
tcf(c_11737,plain,
( ~ iPr_def_11
| ~ r1(sK68,sK68)
| ~ r1(sK68,sK75(sK68)) ),
inference(instantiation,[status(thm)],[c_11727]) ).
tcf(c_11783,plain,
! [X0: $i] :
( p2(sK23(X0))
| r1(sK23(X0),sK95(sK23(X0)))
| ~ r1(sK68,sK23(X0)) ),
inference(instantiation,[status(thm)],[c_264]) ).
tcf(c_11784,plain,
( p2(sK23(sK68))
| r1(sK23(sK68),sK95(sK23(sK68)))
| ~ r1(sK68,sK23(sK68)) ),
inference(instantiation,[status(thm)],[c_11783]) ).
tcf(c_11923,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK95(sK23(X1)))
| r1(sK29(sK95(sK23(X1))),sK30(sK95(sK23(X1))))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK95(sK23(X1))) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_11928,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK95(sK23(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ p2(sK30(sK95(sK23(X1))))
| ~ r1(X0,sK95(sK23(X1))) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_11929,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK95(sK23(X1)))
| r1(sK95(sK23(X1)),sK29(sK95(sK23(X1))))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK95(sK23(X1))) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_11931,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK95(sK23(X1)))
| p2(sK29(sK95(sK23(X1))))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK95(sK23(X1))) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_12092,plain,
( p2(sK69)
| r1(sK69,sK95(sK69))
| ~ r1(sK68,sK69) ),
inference(instantiation,[status(thm)],[c_264]) ).
tcf(c_12331,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK69))
| r1(sK29(sK95(sK69)),sK30(sK95(sK69)))
| ~ sP20(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_12336,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK69))
| ~ sP20(X1)
| ~ r1(X1,X0)
| ~ p2(sK30(sK95(sK69)))
| ~ r1(X0,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_12337,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK69))
| r1(sK95(sK69),sK29(sK95(sK69)))
| ~ sP20(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_12339,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK69))
| p2(sK29(sK95(sK69)))
| ~ sP20(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_12357,plain,
( sP22(sK68)
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_11728,c_267,c_345,c_11728,c_11737]) ).
tcf(c_12358,plain,
( iPr_def_10
| sP22(sK68) ),
inference(renaming,[status(thm)],[c_12357]) ).
tcf(c_12359,plain,
( iPr_def_12
| sP22(sK68) ),
inference(global_subsumption_just,[status(thm)],[c_11730,c_267,c_345,c_11730,c_11737]) ).
tcf(c_12361,plain,
( iPr_def_13
| sP22(sK68) ),
inference(global_subsumption_just,[status(thm)],[c_11732,c_267,c_345,c_11732,c_11737]) ).
tcf(c_12363,plain,
( iPr_def_14
| sP22(sK68) ),
inference(global_subsumption_just,[status(thm)],[c_11734,c_267,c_345,c_11734,c_11737]) ).
tcf(c_12380,plain,
! [X0: $i] :
( p2(sK26(X0))
| p2(sK70(sK26(X0)))
| ~ iPr_def_14
| ~ r1(sK68,sK26(X0)) ),
inference(instantiation,[status(thm)],[c_11733]) ).
tcf(c_12381,plain,
! [X0: $i] :
( p2(sK26(X0))
| ~ iPr_def_13
| ~ p2(sK71(sK26(X0)))
| ~ r1(sK68,sK26(X0)) ),
inference(instantiation,[status(thm)],[c_11731]) ).
tcf(c_12401,plain,
! [X0: $i,X1: $i] :
( p2(sK26(X1))
| ~ sP22(X0)
| ~ p2(sK25(sK26(X1)))
| ~ r1(X0,sK26(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_12412,plain,
( p2(sK26(sK68))
| ~ sP22(sK68)
| ~ p2(sK25(sK26(sK68)))
| ~ r1(sK68,sK26(sK68)) ),
inference(instantiation,[status(thm)],[c_12401]) ).
tcf(c_12555,plain,
( p2(sK23(sK68))
| ~ sP22(sK68)
| ~ p2(sK95(sK23(sK68))) ),
inference(superposition,[status(thm)],[c_50,c_265]) ).
tcf(c_12636,plain,
( p2(sK69)
| sP22(sK68)
| ~ p2(sK95(sK69)) ),
inference(superposition,[status(thm)],[c_2917,c_265]) ).
tcf(c_12649,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK23(X0)))
| ~ sP20(X1)
| ~ r1(X1,sK23(X0))
| ~ p2(sK30(sK95(sK23(X0))))
| ~ r1(sK23(X0),sK95(sK23(X0))) ),
inference(instantiation,[status(thm)],[c_11928]) ).
tcf(c_12650,plain,
( p2(sK95(sK23(sK68)))
| ~ sP20(sK68)
| ~ r1(sK68,sK23(sK68))
| ~ p2(sK30(sK95(sK23(sK68))))
| ~ r1(sK23(sK68),sK95(sK23(sK68))) ),
inference(instantiation,[status(thm)],[c_12649]) ).
tcf(c_12658,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK23(X0)))
| r1(sK29(sK95(sK23(X0))),sK30(sK95(sK23(X0))))
| ~ sP20(X1)
| ~ r1(X1,sK23(X0))
| ~ r1(sK23(X0),sK95(sK23(X0))) ),
inference(instantiation,[status(thm)],[c_11923]) ).
tcf(c_12659,plain,
( p2(sK95(sK23(sK68)))
| r1(sK29(sK95(sK23(sK68))),sK30(sK95(sK23(sK68))))
| ~ sP20(sK68)
| ~ r1(sK68,sK23(sK68))
| ~ r1(sK23(sK68),sK95(sK23(sK68))) ),
inference(instantiation,[status(thm)],[c_12658]) ).
tcf(c_12663,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK23(X0)))
| r1(sK95(sK23(X0)),sK29(sK95(sK23(X0))))
| ~ sP20(X1)
| ~ r1(X1,sK23(X0))
| ~ r1(sK23(X0),sK95(sK23(X0))) ),
inference(instantiation,[status(thm)],[c_11929]) ).
tcf(c_12664,plain,
( p2(sK95(sK23(sK68)))
| r1(sK95(sK23(sK68)),sK29(sK95(sK23(sK68))))
| ~ sP20(sK68)
| ~ r1(sK68,sK23(sK68))
| ~ r1(sK23(sK68),sK95(sK23(sK68))) ),
inference(instantiation,[status(thm)],[c_12663]) ).
tcf(c_12668,plain,
! [X0: $i,X1: $i] :
( p2(sK95(sK23(X0)))
| p2(sK29(sK95(sK23(X0))))
| ~ sP20(X1)
| ~ r1(X1,sK23(X0))
| ~ r1(sK23(X0),sK95(sK23(X0))) ),
inference(instantiation,[status(thm)],[c_11931]) ).
tcf(c_12669,plain,
( p2(sK95(sK23(sK68)))
| p2(sK29(sK95(sK23(sK68))))
| ~ sP20(sK68)
| ~ r1(sK68,sK23(sK68))
| ~ r1(sK23(sK68),sK95(sK23(sK68))) ),
inference(instantiation,[status(thm)],[c_12668]) ).
tcf(c_12705,plain,
! [X0: $i] :
( p2(sK95(sK69))
| ~ sP20(X0)
| ~ r1(X0,sK69)
| ~ p2(sK30(sK95(sK69)))
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12336]) ).
tcf(c_12706,plain,
( p2(sK95(sK69))
| ~ sP20(sK68)
| ~ r1(sK68,sK69)
| ~ p2(sK30(sK95(sK69)))
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12705]) ).
tcf(c_12748,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK30(sK95(sK23(X1))))
| ~ p2(X0)
| ~ r1(sK68,X2)
| ~ r1(sK95(X2),X0)
| ~ r1(X0,sK30(sK95(sK23(X1)))) ),
inference(instantiation,[status(thm)],[c_266]) ).
tcf(c_12868,plain,
! [X0: $i] :
( p2(sK95(sK69))
| r1(sK29(sK95(sK69)),sK30(sK95(sK69)))
| ~ sP20(X0)
| ~ r1(X0,sK69)
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12331]) ).
tcf(c_12869,plain,
( p2(sK95(sK69))
| r1(sK29(sK95(sK69)),sK30(sK95(sK69)))
| ~ sP20(sK68)
| ~ r1(sK68,sK69)
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12868]) ).
tcf(c_12873,plain,
! [X0: $i] :
( p2(sK95(sK69))
| r1(sK95(sK69),sK29(sK95(sK69)))
| ~ sP20(X0)
| ~ r1(X0,sK69)
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12337]) ).
tcf(c_12874,plain,
( p2(sK95(sK69))
| r1(sK95(sK69),sK29(sK95(sK69)))
| ~ sP20(sK68)
| ~ r1(sK68,sK69)
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12873]) ).
tcf(c_12878,plain,
! [X0: $i] :
( p2(sK95(sK69))
| p2(sK29(sK95(sK69)))
| ~ sP20(X0)
| ~ r1(X0,sK69)
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12339]) ).
tcf(c_12879,plain,
( p2(sK95(sK69))
| p2(sK29(sK95(sK69)))
| ~ sP20(sK68)
| ~ r1(sK68,sK69)
| ~ r1(sK69,sK95(sK69)) ),
inference(instantiation,[status(thm)],[c_12878]) ).
tcf(c_13246,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK30(sK95(sK69)))
| ~ p2(X0)
| ~ r1(sK68,X1)
| ~ r1(sK95(X1),X0)
| ~ r1(X0,sK30(sK95(sK69))) ),
inference(instantiation,[status(thm)],[c_266]) ).
tcf(c_13430,plain,
( sP21(sK68)
| p2(sK79)
| p2(sK70(sK79))
| ~ iPr_def_14 ),
inference(resolution,[status(thm)],[c_11733,c_208]) ).
tcf(c_13583,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| p2(sK24(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(superposition,[status(thm)],[c_56,c_55]) ).
tcf(c_13598,plain,
( sP21(sK68)
| p2(sK79)
| p2(sK24(sK79))
| ~ sP22(sK68) ),
inference(superposition,[status(thm)],[c_208,c_55]) ).
tcf(c_13622,plain,
! [X0: $i,X1: $i] :
( p2(sK23(X0))
| p2(sK30(sK95(sK23(X1))))
| ~ r1(sK68,sK23(X0))
| ~ p2(sK29(sK95(sK23(X0))))
| ~ r1(sK95(sK23(X0)),sK29(sK95(sK23(X0))))
| ~ r1(sK29(sK95(sK23(X0))),sK30(sK95(sK23(X1)))) ),
inference(instantiation,[status(thm)],[c_12748]) ).
tcf(c_13623,plain,
( p2(sK23(sK68))
| p2(sK30(sK95(sK23(sK68))))
| ~ r1(sK68,sK23(sK68))
| ~ p2(sK29(sK95(sK23(sK68))))
| ~ r1(sK95(sK23(sK68)),sK29(sK95(sK23(sK68))))
| ~ r1(sK29(sK95(sK23(sK68))),sK30(sK95(sK23(sK68)))) ),
inference(instantiation,[status(thm)],[c_13622]) ).
tcf(c_13667,plain,
( sP21(sK68)
| sP17(sK31(sK79))
| sP18(sK31(sK79))
| ~ sP19(sK79)
| ~ p2(sK31(sK79)) ),
inference(resolution,[status(thm)],[c_211,c_67]) ).
tcf(c_13785,plain,
! [X0: $i] :
( p2(X0)
| p2(sK95(X0))
| p2(sK33(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(superposition,[status(thm)],[c_264,c_74]) ).
tcf(c_14370,plain,
! [X0: $i,X1: $i] :
( sP21(sK68)
| p2(X1)
| sP17(sK31(sK79))
| sP18(sK31(sK79))
| ~ sP19(sK79)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK31(sK79),X0) ),
inference(resolution,[status(thm)],[c_212,c_67]) ).
tcf(c_14427,plain,
! [X0: $i] :
( p2(X0)
| p2(sK30(sK95(sK69)))
| ~ r1(sK68,X0)
| ~ p2(sK29(sK95(sK69)))
| ~ r1(sK95(X0),sK29(sK95(sK69)))
| ~ r1(sK29(sK95(sK69)),sK30(sK95(sK69))) ),
inference(instantiation,[status(thm)],[c_13246]) ).
tcf(c_15030,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| r1(sK26(X0),sK24(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(superposition,[status(thm)],[c_56,c_52]) ).
tcf(c_15509,plain,
( sP21(sK68)
| p2(sK79)
| ~ sP22(sK68)
| ~ p2(sK25(sK79)) ),
inference(superposition,[status(thm)],[c_208,c_54]) ).
tcf(c_16094,plain,
! [X0: $i] :
( p2(X0)
| p2(sK95(X0))
| r1(sK95(X0),sK33(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(superposition,[status(thm)],[c_264,c_71]) ).
tcf(c_16929,plain,
( sP21(sK68)
| p2(sK79)
| r1(sK79,sK24(sK79))
| ~ sP22(sK68) ),
inference(resolution,[status(thm)],[c_52,c_208]) ).
tcf(c_17292,plain,
! [X0: $i] :
( p2(X0)
| p2(sK95(X0))
| ~ sP19(X0)
| ~ r1(sK68,X0)
| ~ p2(sK34(sK95(X0))) ),
inference(superposition,[status(thm)],[c_264,c_73]) ).
tcf(c_17328,plain,
( p2(sK69)
| p2(sK30(sK95(sK69)))
| ~ r1(sK68,sK69)
| ~ p2(sK29(sK95(sK69)))
| ~ r1(sK95(sK69),sK29(sK95(sK69)))
| ~ r1(sK29(sK95(sK69)),sK30(sK95(sK69))) ),
inference(instantiation,[status(thm)],[c_14427]) ).
tcf(c_17516,plain,
! [X0: $i] :
( p2(sK31(X0))
| r1(sK31(X0),sK33(sK31(X0)))
| ~ sP19(X0) ),
inference(resolution,[status(thm)],[c_71,c_67]) ).
tcf(c_17532,plain,
! [X0: $i] :
( p2(X0)
| p2(sK95(X0))
| r1(sK95(X0),sK33(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(resolution,[status(thm)],[c_71,c_264]) ).
tcf(c_17670,plain,
! [X0: $i] :
( p2(sK32(sK79))
| r1(sK40(sK32(sK79)),sK41(sK32(sK79)))
| ~ sP17(X0)
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_17671,plain,
! [X0: $i] :
( p2(sK32(sK79))
| r1(sK36(sK32(sK79)),sK37(sK32(sK79)))
| ~ sP18(X0)
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_17674,plain,
! [X0: $i] :
( p2(sK32(sK79))
| ~ sP17(X0)
| ~ p2(sK41(sK32(sK79)))
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_17675,plain,
! [X0: $i] :
( p2(sK32(sK79))
| r1(sK32(sK79),sK40(sK32(sK79)))
| ~ sP17(X0)
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_17676,plain,
! [X0: $i] :
( p2(sK32(sK79))
| ~ sP18(X0)
| ~ p2(sK37(sK32(sK79)))
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_17677,plain,
! [X0: $i] :
( p2(sK32(sK79))
| r1(sK32(sK79),sK36(sK32(sK79)))
| ~ sP18(X0)
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_17682,plain,
! [X0: $i] :
( p2(sK32(sK79))
| p2(sK40(sK32(sK79)))
| ~ sP17(X0)
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_17683,plain,
! [X0: $i] :
( p2(sK32(sK79))
| p2(sK36(sK32(sK79)))
| ~ sP18(X0)
| ~ r1(X0,sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_17997,plain,
! [X0: $i] :
( p2(sK31(sK79))
| ~ sP19(X0)
| ~ p2(sK34(sK31(sK79)))
| ~ r1(X0,sK31(sK79)) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_18003,plain,
! [X0: $i] :
( p2(sK31(sK79))
| p2(sK33(sK31(sK79)))
| ~ sP19(X0)
| ~ r1(X0,sK31(sK79)) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_18154,plain,
! [X0: $i] :
( sP21(sK68)
| p2(sK79)
| p2(X0)
| ~ iPr_def_15
| ~ sP22(sK68)
| ~ p2(sK24(sK79))
| ~ r1(sK24(sK79),X0) ),
inference(resolution,[status(thm)],[c_16929,c_11735]) ).
tcf(c_18821,plain,
( p2(sK32(sK79))
| ~ sP17(sK31(sK79))
| ~ p2(sK41(sK32(sK79)))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17674]) ).
tcf(c_18862,plain,
( p2(sK31(sK79))
| ~ sP19(sK79)
| ~ p2(sK34(sK31(sK79)))
| ~ r1(sK79,sK31(sK79)) ),
inference(instantiation,[status(thm)],[c_17997]) ).
tcf(c_19022,plain,
( p2(sK32(sK79))
| r1(sK40(sK32(sK79)),sK41(sK32(sK79)))
| ~ sP17(sK31(sK79))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17670]) ).
tcf(c_19026,plain,
( p2(sK32(sK79))
| r1(sK32(sK79),sK40(sK32(sK79)))
| ~ sP17(sK31(sK79))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17675]) ).
tcf(c_19030,plain,
( p2(sK32(sK79))
| p2(sK40(sK32(sK79)))
| ~ sP17(sK31(sK79))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17682]) ).
tcf(c_19058,plain,
( p2(sK31(sK79))
| p2(sK33(sK31(sK79)))
| ~ sP19(sK79)
| ~ r1(sK79,sK31(sK79)) ),
inference(instantiation,[status(thm)],[c_18003]) ).
tcf(c_19484,plain,
! [X0: $i,X1: $i] :
( p2(sK37(sK32(sK79)))
| ~ sP19(X1)
| ~ p2(X0)
| ~ r1(sK32(X1),X0)
| ~ r1(X0,sK37(sK32(sK79))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_19798,plain,
( p2(sK32(sK79))
| p2(sK36(sK32(sK79)))
| ~ sP18(sK31(sK79))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17683]) ).
tcf(c_19799,plain,
( p2(sK32(sK79))
| r1(sK32(sK79),sK36(sK32(sK79)))
| ~ sP18(sK31(sK79))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17677]) ).
tcf(c_19800,plain,
( p2(sK32(sK79))
| r1(sK36(sK32(sK79)),sK37(sK32(sK79)))
| ~ sP18(sK31(sK79))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17671]) ).
tcf(c_19804,plain,
( p2(sK32(sK79))
| ~ sP18(sK31(sK79))
| ~ p2(sK37(sK32(sK79)))
| ~ r1(sK31(sK79),sK32(sK79)) ),
inference(instantiation,[status(thm)],[c_17676]) ).
tcf(c_20098,plain,
( p2(sK79)
| ~ iPr_def_13
| ~ p2(sK71(sK79))
| ~ r1(sK68,sK79) ),
inference(instantiation,[status(thm)],[c_11731]) ).
tcf(c_20100,plain,
( p2(sK79)
| r1(sK70(sK79),sK71(sK79))
| ~ iPr_def_12
| ~ r1(sK68,sK79) ),
inference(instantiation,[status(thm)],[c_11729]) ).
tcf(c_20101,plain,
( p2(sK79)
| r1(sK79,sK70(sK79))
| ~ iPr_def_10
| ~ r1(sK68,sK79) ),
inference(instantiation,[status(thm)],[c_11726]) ).
tcf(c_20198,plain,
( sP21(sK68)
| p2(sK79)
| r1(sK24(sK79),sK25(sK79))
| ~ sP22(sK68) ),
inference(resolution,[status(thm)],[c_53,c_208]) ).
tcf(c_20406,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| r1(sK24(sK26(X0)),sK25(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(superposition,[status(thm)],[c_56,c_53]) ).
tcf(c_20521,plain,
! [X0: $i] :
( p2(sK71(sK79))
| ~ iPr_def_15
| ~ p2(X0)
| ~ r1(sK79,X0)
| ~ r1(X0,sK71(sK79)) ),
inference(instantiation,[status(thm)],[c_11735]) ).
tcf(c_20725,plain,
( p2(sK23(sK68))
| ~ sP22(sK68)
| ~ p2(sK95(sK23(sK68))) ),
inference(superposition,[status(thm)],[c_50,c_265]) ).
tcf(c_21721,plain,
( p2(sK71(sK79))
| ~ iPr_def_15
| ~ p2(sK70(sK79))
| ~ r1(sK79,sK70(sK79))
| ~ r1(sK70(sK79),sK71(sK79)) ),
inference(instantiation,[status(thm)],[c_20521]) ).
tcf(c_21800,plain,
! [X0: $i] :
( p2(sK31(X0))
| r1(sK33(sK31(X0)),sK34(sK31(X0)))
| ~ sP19(X0) ),
inference(resolution,[status(thm)],[c_72,c_67]) ).
tcf(c_21827,plain,
! [X0: $i] :
( p2(X0)
| p2(sK95(X0))
| r1(sK33(sK95(X0)),sK34(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(resolution,[status(thm)],[c_72,c_264]) ).
tcf(c_22825,plain,
! [X0: $i] :
( p2(sK37(sK32(sK79)))
| ~ sP19(sK79)
| ~ p2(X0)
| ~ r1(sK32(sK79),X0)
| ~ r1(X0,sK37(sK32(sK79))) ),
inference(instantiation,[status(thm)],[c_19484]) ).
tcf(c_23522,plain,
! [X0: $i,X1: $i] :
( p2(sK41(sK32(sK79)))
| ~ sP19(X1)
| ~ p2(X0)
| ~ r1(sK32(X1),X0)
| ~ r1(X0,sK41(sK32(sK79))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_23995,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK68,X0)
| ~ sP19(X0)
| r1(sK95(X0),sK33(sK95(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_17532,c_265,c_16094]) ).
tcf(c_23996,plain,
! [X0: $i] :
( p2(X0)
| r1(sK95(X0),sK33(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(renaming,[status(thm)],[c_23995]) ).
tcf(c_24032,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP19(X0)
| ~ r1(sK68,X0)
| ~ p2(sK33(sK95(X0)))
| ~ r1(sK33(sK95(X0)),X1) ),
inference(resolution,[status(thm)],[c_23996,c_266]) ).
tcf(c_26823,plain,
( ~ p2(sK95(sK23(sK68)))
| ~ sP22(sK68) ),
inference(global_subsumption_just,[status(thm)],[c_20725,c_318,c_12555]) ).
tcf(c_26824,plain,
( ~ sP22(sK68)
| ~ p2(sK95(sK23(sK68))) ),
inference(renaming,[status(thm)],[c_26823]) ).
tcf(c_26852,plain,
! [X0: $i] :
( p2(sK41(sK32(sK79)))
| ~ sP19(sK79)
| ~ p2(X0)
| ~ r1(sK32(sK79),X0)
| ~ r1(X0,sK41(sK32(sK79))) ),
inference(instantiation,[status(thm)],[c_23522]) ).
tcf(c_26908,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK68,X0)
| ~ sP19(X0)
| r1(sK33(sK95(X0)),sK34(sK95(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_21827,c_265,c_21827]) ).
tcf(c_26909,plain,
! [X0: $i] :
( p2(X0)
| r1(sK33(sK95(X0)),sK34(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(renaming,[status(thm)],[c_26908]) ).
tcf(c_30397,plain,
! [X0: $i] :
( sP21(sK68)
| p2(sK79)
| p2(X0)
| ~ iPr_def_15
| ~ sP22(sK68)
| ~ r1(sK24(sK79),X0) ),
inference(global_subsumption_just,[status(thm)],[c_18154,c_13598,c_18154]) ).
tcf(c_30400,plain,
! [X0: $i] :
( sP21(sK68)
| p2(sK79)
| p2(X0)
| ~ iPr_def_15
| ~ r1(sK24(sK79),X0) ),
inference(global_subsumption_just,[status(thm)],[c_30397,c_208,c_12358,c_12359,c_12361,c_12363,c_13430,c_20101,c_20100,c_20098,c_21721,c_30397]) ).
tcf(c_30429,plain,
( sP21(sK68)
| p2(sK79)
| sP22(sK68)
| p2(sK75(sK24(sK79)))
| ~ iPr_def_15
| ~ r1(sK68,sK24(sK79)) ),
inference(resolution,[status(thm)],[c_30400,c_200]) ).
tcf(c_30436,plain,
( sP21(sK68)
| p2(sK79)
| p2(sK25(sK79))
| ~ iPr_def_15
| ~ sP22(sK68) ),
inference(resolution,[status(thm)],[c_30400,c_20198]) ).
tcf(c_30733,plain,
( sP21(sK68)
| p2(sK79)
| sP22(sK68)
| ~ iPr_def_15 ),
inference(global_subsumption_just,[status(thm)],[c_30429,c_208,c_12358,c_12359,c_12361,c_12363,c_13430,c_20101,c_20100,c_20098,c_21721]) ).
tcf(c_30735,plain,
( sP21(sK68)
| p2(sK79)
| ~ iPr_def_15 ),
inference(global_subsumption_just,[status(thm)],[c_30733,c_15509,c_30436,c_30733]) ).
tcf(c_30791,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| p2(sK24(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(resolution,[status(thm)],[c_56,c_55]) ).
tcf(c_30793,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| r1(sK26(X0),sK24(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(resolution,[status(thm)],[c_56,c_52]) ).
tcf(c_30797,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| r1(sK24(sK26(X0)),sK25(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(resolution,[status(thm)],[c_56,c_53]) ).
tcf(c_31193,plain,
( p2(sK41(sK32(sK79)))
| ~ sP19(sK79)
| ~ p2(sK40(sK32(sK79)))
| ~ r1(sK32(sK79),sK40(sK32(sK79)))
| ~ r1(sK40(sK32(sK79)),sK41(sK32(sK79))) ),
inference(instantiation,[status(thm)],[c_26852]) ).
tcf(c_31410,plain,
! [X0: $i,X1: $i] :
( sP20(X0)
| p2(X1)
| p2(sK26(X0))
| ~ iPr_def_10
| ~ sP21(X0)
| ~ p2(sK70(sK26(X0)))
| ~ r1(sK68,sK26(X0))
| ~ r1(sK70(sK26(X0)),X1) ),
inference(resolution,[status(thm)],[c_58,c_11726]) ).
tcf(c_32748,plain,
( p2(sK37(sK32(sK79)))
| ~ sP19(sK79)
| ~ p2(sK36(sK32(sK79)))
| ~ r1(sK32(sK79),sK36(sK32(sK79)))
| ~ r1(sK36(sK32(sK79)),sK37(sK32(sK79))) ),
inference(instantiation,[status(thm)],[c_22825]) ).
tcf(c_33740,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP19(X0)
| ~ r1(sK68,X0)
| ~ r1(sK33(sK95(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_24032,c_265,c_13785,c_24032]) ).
tcf(c_33778,plain,
! [X0: $i] :
( sP22(sK68)
| p2(X0)
| p2(sK75(sK33(sK95(X0))))
| ~ sP19(X0)
| ~ r1(sK68,X0)
| ~ r1(sK68,sK33(sK95(X0))) ),
inference(resolution,[status(thm)],[c_33740,c_200]) ).
tcf(c_33788,plain,
! [X0: $i] :
( p2(X0)
| p2(sK34(sK95(X0)))
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(resolution,[status(thm)],[c_33740,c_26909]) ).
tcf(c_34990,plain,
! [X0: $i] :
( ~ sP19(X0)
| ~ r1(sK68,X0)
| p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_33778,c_265,c_17292,c_33788]) ).
tcf(c_34991,plain,
! [X0: $i] :
( p2(X0)
| ~ sP19(X0)
| ~ r1(sK68,X0) ),
inference(renaming,[status(thm)],[c_34990]) ).
tcf(c_35018,plain,
( sP21(sK68)
| p2(sK79)
| ~ sP19(sK79) ),
inference(resolution,[status(thm)],[c_34991,c_208]) ).
tcf(c_35031,plain,
( sP21(sK68)
| p2(sK79) ),
inference(global_subsumption_just,[status(thm)],[c_35018,c_11736,c_30735,c_35018]) ).
tcf(c_35040,plain,
( sP19(sK79)
| sP21(sK68) ),
inference(backward_subsumption_resolution,[status(thm)],[c_209,c_35031]) ).
tcf(c_35049,plain,
! [X0: $i,X1: $i] :
( sP21(sK68)
| p2(X1)
| sP17(sK31(sK79))
| sP18(sK31(sK79))
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK31(sK79),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_14370,c_35040]) ).
tcf(c_35050,plain,
( sP21(sK68)
| sP17(sK31(sK79))
| sP18(sK31(sK79))
| ~ p2(sK31(sK79)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_13667,c_35040]) ).
tcf(c_35584,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP22(X0)
| ~ sP21(X0)
| p2(sK24(sK26(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_30791,c_57,c_13583]) ).
tcf(c_35585,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK24(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(renaming,[status(thm)],[c_35584]) ).
tcf(c_36920,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP22(X0)
| ~ sP21(X0)
| r1(sK26(X0),sK24(sK26(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_30793,c_57,c_15030]) ).
tcf(c_36921,plain,
! [X0: $i] :
( sP20(X0)
| r1(sK26(X0),sK24(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(renaming,[status(thm)],[c_36920]) ).
tcf(c_37100,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP22(X0)
| ~ sP21(X0)
| r1(sK24(sK26(X0)),sK25(sK26(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_30797,c_57,c_20406]) ).
tcf(c_37101,plain,
! [X0: $i] :
( sP20(X0)
| r1(sK24(sK26(X0)),sK25(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(renaming,[status(thm)],[c_37100]) ).
tcf(c_37137,plain,
( sP21(sK68)
| sP17(sK31(sK79))
| ~ p2(sK31(sK79)) ),
inference(global_subsumption_just,[status(thm)],[c_35050,c_3623,c_3652,c_19804,c_19800,c_19799,c_19798,c_32748,c_35031,c_35040,c_35050]) ).
tcf(c_37139,plain,
( sP21(sK68)
| ~ p2(sK31(sK79)) ),
inference(global_subsumption_just,[status(thm)],[c_37137,c_3623,c_3652,c_18821,c_19022,c_19026,c_19030,c_31193,c_35031,c_35040,c_37137]) ).
tcf(c_38739,plain,
! [X0: $i,X1: $i] :
( sP21(sK68)
| p2(X1)
| sP17(sK31(sK79))
| ~ r1(sK31(sK79),X0)
| ~ r1(X0,X1)
| ~ p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_35049,c_3623,c_3652,c_19804,c_19800,c_19799,c_19798,c_32748,c_35031,c_35040,c_35049]) ).
tcf(c_38740,plain,
! [X0: $i,X1: $i] :
( sP21(sK68)
| p2(X1)
| sP17(sK31(sK79))
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK31(sK79),X0) ),
inference(renaming,[status(thm)],[c_38739]) ).
tcf(c_38741,plain,
! [X0: $i,X1: $i] :
( sP21(sK68)
| p2(X1)
| ~ r1(sK31(sK79),X0)
| ~ r1(X0,X1)
| ~ p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_38740,c_3623,c_3652,c_18821,c_19022,c_19026,c_19030,c_31193,c_35031,c_35040,c_38740]) ).
tcf(c_38742,plain,
! [X0: $i,X1: $i] :
( sP21(sK68)
| p2(X1)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK31(sK79),X0) ),
inference(renaming,[status(thm)],[c_38741]) ).
tcf(c_38778,plain,
! [X0: $i] :
( sP21(sK68)
| p2(X0)
| p2(sK31(sK79))
| ~ sP19(sK79)
| ~ p2(sK33(sK31(sK79)))
| ~ r1(sK33(sK31(sK79)),X0) ),
inference(resolution,[status(thm)],[c_38742,c_17516]) ).
tcf(c_39084,plain,
! [X0: $i,X1: $i] :
( sP20(X0)
| p2(X1)
| ~ sP21(X0)
| ~ sP22(X0)
| ~ p2(sK24(sK26(X0)))
| ~ r1(sK24(sK26(X0)),X1) ),
inference(resolution,[status(thm)],[c_36921,c_58]) ).
tcf(c_41108,plain,
! [X0: $i,X1: $i] :
( sP20(X0)
| p2(X1)
| ~ r1(sK70(sK26(X0)),X1)
| ~ r1(sK68,sK26(X0))
| ~ p2(sK70(sK26(X0)))
| ~ sP21(X0)
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_31410,c_57,c_31410]) ).
tcf(c_41109,plain,
! [X0: $i,X1: $i] :
( sP20(X0)
| p2(X1)
| ~ iPr_def_10
| ~ sP21(X0)
| ~ p2(sK70(sK26(X0)))
| ~ r1(sK68,sK26(X0))
| ~ r1(sK70(sK26(X0)),X1) ),
inference(renaming,[status(thm)],[c_41108]) ).
tcf(c_41149,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(X0))
| p2(sK71(sK26(X0)))
| ~ iPr_def_12
| ~ iPr_def_10
| ~ sP21(X0)
| ~ p2(sK70(sK26(X0)))
| ~ r1(sK68,sK26(X0)) ),
inference(resolution,[status(thm)],[c_41109,c_11729]) ).
tcf(c_41153,plain,
! [X0: $i] :
( sP22(sK68)
| sP20(X0)
| p2(sK75(sK70(sK26(X0))))
| ~ iPr_def_10
| ~ sP21(X0)
| ~ p2(sK70(sK26(X0)))
| ~ r1(sK68,sK26(X0))
| ~ r1(sK68,sK70(sK26(X0))) ),
inference(resolution,[status(thm)],[c_41109,c_200]) ).
tcf(c_41161,plain,
! [X0: $i] :
( sP22(sK68)
| sP20(X0)
| ~ sP21(X0)
| ~ r1(sK68,sK26(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_41153,c_57,c_12358,c_12359,c_12361,c_12363,c_12381,c_12380,c_41149]) ).
tcf(c_41180,plain,
( sP20(sK68)
| sP22(sK68)
| ~ sP21(sK68) ),
inference(resolution,[status(thm)],[c_41161,c_56]) ).
tcf(c_41223,plain,
( ~ sP21(sK68)
| sP22(sK68) ),
inference(global_subsumption_just,[status(thm)],[c_41180,c_2907,c_2917,c_12092,c_12636,c_12706,c_12869,c_12874,c_12879,c_17328,c_41180]) ).
tcf(c_41224,plain,
( sP22(sK68)
| ~ sP21(sK68) ),
inference(renaming,[status(thm)],[c_41223]) ).
tcf(c_46735,plain,
! [X0: $i] :
( sP21(sK68)
| p2(X0)
| ~ r1(sK33(sK31(sK79)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_38778,c_3681,c_19058,c_35031,c_35040,c_37139,c_38778]) ).
tcf(c_46757,plain,
( sP21(sK68)
| sP22(sK68)
| p2(sK75(sK33(sK31(sK79))))
| ~ r1(sK68,sK33(sK31(sK79))) ),
inference(resolution,[status(thm)],[c_46735,c_200]) ).
tcf(c_46764,plain,
( sP21(sK68)
| p2(sK31(sK79))
| p2(sK34(sK31(sK79)))
| ~ sP19(sK79) ),
inference(resolution,[status(thm)],[c_46735,c_21800]) ).
tcf(c_46765,plain,
sP21(sK68),
inference(global_subsumption_just,[status(thm)],[c_46757,c_3681,c_18862,c_35031,c_35040,c_37139,c_46764]) ).
tcf(c_48582,plain,
! [X0: $i,X1: $i] :
( sP20(X0)
| p2(X1)
| ~ sP21(X0)
| ~ sP22(X0)
| ~ r1(sK24(sK26(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_39084,c_35585,c_39084]) ).
tcf(c_48625,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK25(sK26(X0)))
| ~ sP21(X0)
| ~ sP22(X0) ),
inference(resolution,[status(thm)],[c_48582,c_37101]) ).
tcf(c_48626,plain,
( sP20(sK68)
| p2(sK25(sK26(sK68)))
| ~ sP21(sK68)
| ~ sP22(sK68) ),
inference(instantiation,[status(thm)],[c_48625]) ).
tcf(c_48627,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_48626,c_46765,c_41224,c_26824,c_13623,c_12669,c_12664,c_12659,c_12650,c_12412,c_11784,c_340,c_339,c_319,c_318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL660+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.37 % Computer : n018.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Thu Sep 24 00:07:05 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/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.13/0.43
% 0.13/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.43
% 0.13/0.43 % Detected problem language: tptp
% 0.13/0.44 % Proving...
% 11.77/3.87 % SZS status Started for theBenchmark.p
% 11.77/3.87 % SZS status Theorem for theBenchmark.p
% 11.77/3.87
% 11.77/3.87 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 11.77/3.87
% 11.77/3.87 % ------ iProver source info
% 11.77/3.87
% 11.77/3.87 % git: date: 2026-07-19 20:42:38 +0200
% 11.77/3.87 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 11.77/3.87 % git: non_committed_changes: false
% 11.77/3.87
% 11.77/3.87 % ------ Parsing...
% 11.77/3.87 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 11.77/3.87
% 11.77/3.87 % ------ Preprocessing... sf_s rm: 146 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 11.77/3.87
% 11.77/3.87 % ------ Preprocessing... gs_s sp: 9 0s gs_e snvd_s sp: 0 0s snvd_e
% 11.77/3.87 % ------ Proving...
% 11.77/3.87 % ------ Problem Properties
% 11.77/3.87
% 11.77/3.87 %
% 11.77/3.87 % clauses 77
% 11.77/3.87 % conjectures 21
% 11.77/3.87 % EPR 18
% 11.77/3.87 % Horn 31
% 11.77/3.87 % unary 5
% 11.77/3.87 % binary 11
% 11.77/3.87 % lits 272
% 11.77/3.87 % lits eq 0
% 11.77/3.87 % fd_pure 0
% 11.77/3.87 % fd_pseudo 0
% 11.77/3.87 % fd_cond 0
% 11.77/3.87 % fd_pseudo_cond 0
% 11.77/3.87 % AC symbols 0
% 11.77/3.87
% 11.77/3.87 % ------ Input Options Time Limit: Unbounded
% 11.77/3.87
% 11.77/3.87
% 11.77/3.87 % ------
% 11.77/3.87 % Current options:
% 11.77/3.87 % ------
% 11.77/3.87
% 11.77/3.87
% 11.77/3.87 %
% 11.77/3.87
% 11.77/3.87 % ------ Proving...
% 11.77/3.87 %
% 11.77/3.87
% 11.77/3.87 % SZS status Theorem for theBenchmark.p
% 11.77/3.87
% 11.77/3.87 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 11.77/3.87
% 11.77/3.87
%------------------------------------------------------------------------------