%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL660+1.015 : 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 : n013.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 6.42s 2.71s
% Output : CNFRefutation 6.42s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f56ERROR: Could not build tree for root c_47138ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f59,plain,
! [X0] :
( ~ sP48(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,[],[f57]) ).
fof(f60,plain,
! [X0] :
( ~ sP48(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,[],[f59]) ).
fof(f61,plain,
! [X0] :
( ~ sP48(X0)
| ( ! [X2] :
( ( p2(sK50(X2))
& ~ p2(sK51(X2))
& r1(sK50(X2),sK51(X2))
& r1(X2,sK50(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK49(X0))
& r1(X0,sK49(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49,sK50,sK51]),skolemize(X1,sK49(X0)),skolemize(X3,sK50(X2)),skolemize(X4,sK51(X2))],[f60]) ).
fof(f62,plain,
! [X0] :
( ~ sP47(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) )
| sP46(X0) ) ) ),
inference(nnf_transformation,[],[f56]) ).
fof(f63,plain,
! [X0] :
( ~ sP47(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) )
| sP46(X0) ) ) ),
inference(rectify,[],[f62]) ).
fof(f64,plain,
! [X0] :
( ~ sP47(X0)
| ( ( ( p2(sK53(X0))
& ~ p2(sK54(X0))
& r1(sK53(X0),sK54(X0))
& r1(X0,sK53(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK52(X0),X2) )
& ~ p2(sK52(X0))
& r1(X0,sK52(X0)) )
| sP46(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53,sK54]),skolemize(X1,sK52(X0)),skolemize(X4,sK53(X0)),skolemize(X5,sK54(X0))],[f63]) ).
fof(f65,plain,
! [X0] :
( ~ sP46(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,[],[f55]) ).
fof(f66,plain,
! [X0] :
( ~ sP46(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,[],[f65]) ).
fof(f67,plain,
! [X0] :
( ~ sP46(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK55(X2))
& ~ p2(sK56(X2))
& r1(sK55(X2),sK56(X2))
& r1(X2,sK55(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56]),skolemize(X3,sK55(X2)),skolemize(X4,sK56(X2))],[f66]) ).
fof(f68,plain,
! [X29] :
( ~ sP45(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,[],[f54]) ).
fof(f69,plain,
! [X0] :
( ~ sP45(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,[],[f68]) ).
fof(f70,plain,
! [X0] :
( ~ sP45(X0)
| ( ! [X5] :
( ( p2(sK59(X5))
& ~ p2(sK60(X5))
& r1(sK59(X5),sK60(X5))
& r1(X5,sK59(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK58(X0),X3) )
& ~ p2(sK58(X0))
& r1(sK57(X0),sK58(X0))
& r1(X0,sK57(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57,sK58,sK59,sK60]),skolemize(X1,sK57(X0)),skolemize(X2,sK58(X0)),skolemize(X6,sK59(X5)),skolemize(X7,sK60(X5))],[f69]) ).
fof(f71,plain,
! [X39] :
( ~ sP44(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) )
| sP42(X40) ) )
| ~ r1(X39,X40) ) ),
inference(nnf_transformation,[],[f53]) ).
fof(f72,plain,
! [X0] :
( ~ sP44(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) )
| sP42(X1) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f71]) ).
fof(f73,plain,
! [X0] :
( ~ sP44(X0)
| ! [X1] :
( ( ( ( p2(sK62(X1))
& ~ p2(sK63(X1))
& r1(sK62(X1),sK63(X1))
& r1(X1,sK62(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK61(X1),X3) )
& ~ p2(sK61(X1))
& r1(X1,sK61(X1)) )
| sP42(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61,sK62,sK63]),skolemize(X2,sK61(X1)),skolemize(X5,sK62(X1)),skolemize(X6,sK63(X1))],[f72]) ).
fof(f74,plain,
! [X39] :
( ~ sP43(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,[],[f52]) ).
fof(f75,plain,
! [X0] :
( ~ sP43(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,[],[f74]) ).
fof(f76,plain,
! [X0] :
( ~ sP43(X0)
| ( ! [X5] :
( ( p2(sK66(X5))
& ~ p2(sK67(X5))
& r1(sK66(X5),sK67(X5))
& r1(X5,sK66(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK65(X0),X3) )
& ~ p2(sK65(X0))
& r1(sK64(X0),sK65(X0))
& r1(X0,sK64(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66,sK67]),skolemize(X1,sK64(X0)),skolemize(X2,sK65(X0)),skolemize(X6,sK66(X5)),skolemize(X7,sK67(X5))],[f75]) ).
fof(f202,plain,
? [X0] :
( ! [X80] :
( ? [X81] :
( ! [X82] :
( ~ p2(X82)
| ! [X83] :
( p2(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
& ~ p2(X81)
& r1(X80,X81) )
| p2(X80)
| ~ r1(X0,X80) )
& ( ? [X74] :
( ! [X76] :
( ( ? [X79] : r1(X76,X79)
& ~ p1(X76) )
| ! [X77] :
( ! [X78] : ~ r1(X77,X78)
| p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X74,X76) )
& ? [X75] : r1(X74,X75)
& ~ p1(X74)
& r1(X0,X74) )
| ! [X73] : ~ r1(X0,X73)
| p1(X0) )
& ( ? [X67] :
( ! [X69] :
( ( ? [X72] : r1(X69,X72)
& ~ p1(X69)
& ~ p2(X69) )
| ! [X70] :
( ! [X71] : ~ r1(X70,X71)
| p1(X70)
| p2(X70)
| ~ r1(X69,X70) )
| ~ r1(X67,X69) )
& ? [X68] : r1(X67,X68)
& ~ p1(X67)
& ~ p2(X67)
& r1(X0,X67) )
| ! [X66] : ~ r1(X0,X66)
| p1(X0)
| p2(X0) )
& ( ? [X64] :
( sP0(X64)
& ? [X65] : r1(X64,X65)
& ~ p1(X64)
& ~ p2(X64)
& ~ p3(X64)
& r1(X0,X64) )
| ! [X63] : ~ r1(X0,X63)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X61] :
( sP1(X61)
& ? [X62] : r1(X61,X62)
& ~ p1(X61)
& ~ p2(X61)
& ~ p3(X61)
& ~ p4(X61)
& r1(X0,X61) )
| ! [X60] : ~ r1(X0,X60)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X59] :
( sP2(X59)
& sP3(X59)
& ~ p1(X59)
& r1(X0,X59) )
| ! [X57] :
( ! [X58] : ~ r1(X57,X58)
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(X0,X57) )
| p1(X0) )
& ( ? [X56] :
( sP4(X56)
& sP5(X56)
& ~ p1(X56)
& ~ p2(X56)
& r1(X0,X56) )
| ! [X54] :
( ! [X55] : ~ r1(X54,X55)
| p1(X54)
| p2(X54)
| p3(X54)
| p4(X54)
| ~ r1(X0,X54) )
| p1(X0)
| p2(X0) )
& ( ? [X53] :
( sP8(X53)
& sP7(X53)
& ~ p1(X53)
& ~ p2(X53)
& ~ p3(X53)
& r1(X0,X53) )
| ! [X51] :
( ! [X52] : ~ r1(X51,X52)
| p1(X51)
| p2(X51)
| p3(X51)
| p4(X51)
| ~ r1(X0,X51) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X50] :
( sP11(X50)
& sP10(X50)
& ~ p1(X50)
& ~ p2(X50)
& ~ p3(X50)
& ~ p4(X50)
& r1(X0,X50) )
| ! [X48] :
( ! [X49] : ~ r1(X48,X49)
| p1(X48)
| p2(X48)
| p3(X48)
| p4(X48)
| ~ r1(X0,X48) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X47] :
( sP14(X47)
& sP15(X47)
& ~ p1(X47)
& r1(X0,X47) )
| ! [X44] :
( ! [X45] :
( ! [X46] : ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(X44,X45) )
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(X0,X44) )
| p1(X0) )
& ( ? [X43] :
( sP18(X43)
& sP19(X43)
& ~ p1(X43)
& ~ p2(X43)
& r1(X0,X43) )
| ! [X40] :
( ! [X41] :
( ! [X42] : ~ r1(X41,X42)
| p1(X41)
| p2(X41)
| p3(X41)
| p4(X41)
| ~ r1(X40,X41) )
| p1(X40)
| p2(X40)
| p3(X40)
| p4(X40)
| ~ r1(X0,X40) )
| p1(X0)
| p2(X0) )
& ( ? [X39] :
( sP24(X39)
& sP23(X39)
& ~ p1(X39)
& ~ p2(X39)
& ~ p3(X39)
& r1(X0,X39) )
| ! [X36] :
( ! [X37] :
( ! [X38] : ~ r1(X37,X38)
| p1(X37)
| p2(X37)
| p3(X37)
| p4(X37)
| ~ r1(X36,X37) )
| p1(X36)
| p2(X36)
| p3(X36)
| p4(X36)
| ~ r1(X0,X36) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X35] :
( sP29(X35)
& sP28(X35)
& ~ p1(X35)
& ~ p2(X35)
& ~ p3(X35)
& ~ p4(X35)
& r1(X0,X35) )
| ! [X32] :
( ! [X33] :
( ! [X34] : ~ r1(X33,X34)
| p1(X33)
| p2(X33)
| p3(X33)
| p4(X33)
| ~ r1(X32,X33) )
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(X0,X32) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X31] :
( sP34(X31)
& sP35(X31)
& ~ p1(X31)
& r1(X0,X31) )
| ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29) )
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(X27,X28) )
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(X0,X27) )
| p1(X0) )
& ( ? [X26] :
( sP40(X26)
& sP41(X26)
& ~ p1(X26)
& ~ p2(X26)
& r1(X0,X26) )
| ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] : ~ r1(X24,X25)
| p1(X24)
| p2(X24)
| p3(X24)
| p4(X24)
| ~ r1(X23,X24) )
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X0,X22) )
| p1(X0)
| p2(X0) )
& ( ? [X16] :
( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP43(X19)
| sP44(X19)
| ~ r1(X16,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP45(X16) )
& r1(X0,X16) )
| sP47(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) )
& ( sP48(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,[],[f58]) ).
fof(f203,plain,
( ! [X80] :
( ( ! [X82] :
( ~ p2(X82)
| ! [X83] :
( p2(X83)
| ~ r1(X82,X83) )
| ~ r1(sK160(X80),X82) )
& ~ p2(sK160(X80))
& r1(X80,sK160(X80)) )
| p2(X80)
| ~ r1(sK128,X80) )
& ( ( ! [X76] :
( ( r1(X76,sK159(X76))
& ~ p1(X76) )
| ! [X77] :
( ! [X78] : ~ r1(X77,X78)
| p1(X77)
| ~ r1(X76,X77) )
| ~ r1(sK157,X76) )
& r1(sK157,sK158)
& ~ p1(sK157)
& r1(sK128,sK157) )
| ! [X73] : ~ r1(sK128,X73)
| p1(sK128) )
& ( ( ! [X69] :
( ( r1(X69,sK156(X69))
& ~ p1(X69)
& ~ p2(X69) )
| ! [X70] :
( ! [X71] : ~ r1(X70,X71)
| p1(X70)
| p2(X70)
| ~ r1(X69,X70) )
| ~ r1(sK154,X69) )
& r1(sK154,sK155)
& ~ p1(sK154)
& ~ p2(sK154)
& r1(sK128,sK154) )
| ! [X66] : ~ r1(sK128,X66)
| p1(sK128)
| p2(sK128) )
& ( ( sP0(sK152)
& r1(sK152,sK153)
& ~ p1(sK152)
& ~ p2(sK152)
& ~ p3(sK152)
& r1(sK128,sK152) )
| ! [X63] : ~ r1(sK128,X63)
| p1(sK128)
| p2(sK128)
| p3(sK128) )
& ( ( sP1(sK150)
& r1(sK150,sK151)
& ~ p1(sK150)
& ~ p2(sK150)
& ~ p3(sK150)
& ~ p4(sK150)
& r1(sK128,sK150) )
| ! [X60] : ~ r1(sK128,X60)
| p1(sK128)
| p2(sK128)
| p3(sK128)
| p4(sK128) )
& ( ( sP2(sK149)
& sP3(sK149)
& ~ p1(sK149)
& r1(sK128,sK149) )
| ! [X57] :
( ! [X58] : ~ r1(X57,X58)
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(sK128,X57) )
| p1(sK128) )
& ( ( sP4(sK148)
& sP5(sK148)
& ~ p1(sK148)
& ~ p2(sK148)
& r1(sK128,sK148) )
| ! [X54] :
( ! [X55] : ~ r1(X54,X55)
| p1(X54)
| p2(X54)
| p3(X54)
| p4(X54)
| ~ r1(sK128,X54) )
| p1(sK128)
| p2(sK128) )
& ( ( sP8(sK147)
& sP7(sK147)
& ~ p1(sK147)
& ~ p2(sK147)
& ~ p3(sK147)
& r1(sK128,sK147) )
| ! [X51] :
( ! [X52] : ~ r1(X51,X52)
| p1(X51)
| p2(X51)
| p3(X51)
| p4(X51)
| ~ r1(sK128,X51) )
| p1(sK128)
| p2(sK128)
| p3(sK128) )
& ( ( sP11(sK146)
& sP10(sK146)
& ~ p1(sK146)
& ~ p2(sK146)
& ~ p3(sK146)
& ~ p4(sK146)
& r1(sK128,sK146) )
| ! [X48] :
( ! [X49] : ~ r1(X48,X49)
| p1(X48)
| p2(X48)
| p3(X48)
| p4(X48)
| ~ r1(sK128,X48) )
| p1(sK128)
| p2(sK128)
| p3(sK128)
| p4(sK128) )
& ( ( sP14(sK145)
& sP15(sK145)
& ~ p1(sK145)
& r1(sK128,sK145) )
| ! [X44] :
( ! [X45] :
( ! [X46] : ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(X44,X45) )
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(sK128,X44) )
| p1(sK128) )
& ( ( sP18(sK144)
& sP19(sK144)
& ~ p1(sK144)
& ~ p2(sK144)
& r1(sK128,sK144) )
| ! [X40] :
( ! [X41] :
( ! [X42] : ~ r1(X41,X42)
| p1(X41)
| p2(X41)
| p3(X41)
| p4(X41)
| ~ r1(X40,X41) )
| p1(X40)
| p2(X40)
| p3(X40)
| p4(X40)
| ~ r1(sK128,X40) )
| p1(sK128)
| p2(sK128) )
& ( ( sP24(sK143)
& sP23(sK143)
& ~ p1(sK143)
& ~ p2(sK143)
& ~ p3(sK143)
& r1(sK128,sK143) )
| ! [X36] :
( ! [X37] :
( ! [X38] : ~ r1(X37,X38)
| p1(X37)
| p2(X37)
| p3(X37)
| p4(X37)
| ~ r1(X36,X37) )
| p1(X36)
| p2(X36)
| p3(X36)
| p4(X36)
| ~ r1(sK128,X36) )
| p1(sK128)
| p2(sK128)
| p3(sK128) )
& ( ( sP29(sK142)
& sP28(sK142)
& ~ p1(sK142)
& ~ p2(sK142)
& ~ p3(sK142)
& ~ p4(sK142)
& r1(sK128,sK142) )
| ! [X32] :
( ! [X33] :
( ! [X34] : ~ r1(X33,X34)
| p1(X33)
| p2(X33)
| p3(X33)
| p4(X33)
| ~ r1(X32,X33) )
| p1(X32)
| p2(X32)
| p3(X32)
| p4(X32)
| ~ r1(sK128,X32) )
| p1(sK128)
| p2(sK128)
| p3(sK128)
| p4(sK128) )
& ( ( sP34(sK141)
& sP35(sK141)
& ~ p1(sK141)
& r1(sK128,sK141) )
| ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29) )
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(X27,X28) )
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(sK128,X27) )
| p1(sK128) )
& ( ( sP40(sK140)
& sP41(sK140)
& ~ p1(sK140)
& ~ p2(sK140)
& r1(sK128,sK140) )
| ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] : ~ r1(X24,X25)
| p1(X24)
| p2(X24)
| p3(X24)
| p4(X24)
| ~ r1(X23,X24) )
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23) )
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(sK128,X22) )
| p1(sK128)
| p2(sK128) )
& ( ( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP43(X19)
| sP44(X19)
| ~ r1(sK139,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(sK139,X17) )
& ~ p2(sK139) )
| sP45(sK139) )
& r1(sK128,sK139) )
| sP47(sK128) )
& ! [X13] :
( ( p1(sK137(X13))
& ~ p1(sK138(X13))
& r1(sK137(X13),sK138(X13))
& r1(X13,sK137(X13)) )
| p1(X13)
| ~ r1(sK128,X13) )
& ~ p1(sK136)
& r1(sK128,sK136)
& ( sP48(sK128)
| ! [X10] :
( ( p5(sK135(X10))
& r1(X10,sK135(X10)) )
| ~ r1(sK128,X10) ) )
& ! [X7] :
( ( p3(sK133(X7))
& ~ p3(sK134(X7))
& r1(sK133(X7),sK134(X7))
& r1(X7,sK133(X7)) )
| p3(X7)
| ~ r1(sK128,X7) )
& ~ p3(sK132)
& r1(sK128,sK132)
& ( ( ! [X3] :
( ( p2(sK130(X3))
& ~ p2(sK131(X3))
& r1(sK130(X3),sK131(X3))
& r1(X3,sK130(X3)) )
| p2(X3)
| ~ r1(sK128,X3) )
& ~ p2(sK129)
& r1(sK128,sK129) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(sK128,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK128,sK129,sK130,sK131,sK132,sK133,sK134,sK135,sK136,sK137,sK138,sK139,sK140,sK141,sK142,sK143,sK144,sK145,sK146,sK147,sK148,sK149,sK150,sK151,sK152,sK153,sK154,sK155,sK156,sK157,sK158,sK159,sK160]),skolemize(X0,sK128),skolemize(X2,sK129),skolemize(X4,sK130(X3)),skolemize(X5,sK131(X3)),skolemize(X6,sK132),skolemize(X8,sK133(X7)),skolemize(X9,sK134(X7)),skolemize(X11,sK135(X10)),skolemize(X12,sK136),skolemize(X14,sK137(X13)),skolemize(X15,sK138(X13)),skolemize(X16,sK139),skolemize(X26,sK140),skolemize(X31,sK141),skolemize(X35,sK142),skolemize(X39,sK143),skolemize(X43,sK144),skolemize(X47,sK145),skolemize(X50,sK146),skolemize(X53,sK147),skolemize(X56,sK148),skolemize(X59,sK149),skolemize(X61,sK150),skolemize(X62,sK151),skolemize(X64,sK152),skolemize(X65,sK153),skolemize(X67,sK154),skolemize(X68,sK155),skolemize(X72,sK156(X69)),skolemize(X74,sK157),skolemize(X75,sK158),skolemize(X79,sK159(X76)),skolemize(X81,sK160(X80))],[f202]) ).
fof(f204,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f205,plain,
! [X2,X0] :
( ~ sP48(X0)
| p2(sK50(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f206,plain,
! [X2,X0] :
( ~ sP48(X0)
| ~ p2(sK51(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f207,plain,
! [X2,X0] :
( ~ sP48(X0)
| r1(sK50(X2),sK51(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f208,plain,
! [X2,X0] :
( ~ sP48(X0)
| r1(X2,sK50(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f209,plain,
! [X0] :
( ~ sP48(X0)
| ~ p2(sK49(X0)) ),
inference(cnf_transformation,[],[f61]) ).
fof(f210,plain,
! [X0] :
( ~ sP48(X0)
| r1(X0,sK49(X0)) ),
inference(cnf_transformation,[],[f61]) ).
fof(f215,plain,
! [X2,X3,X0] :
( ~ sP47(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK52(X0),X2)
| sP46(X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f216,plain,
! [X0] :
( ~ sP47(X0)
| ~ p2(sK52(X0))
| sP46(X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f217,plain,
! [X0] :
( ~ sP47(X0)
| r1(X0,sK52(X0))
| sP46(X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f218,plain,
! [X2,X0,X1] :
( ~ sP46(X0)
| p2(sK55(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ sP46(X0)
| ~ p2(sK56(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f220,plain,
! [X2,X0,X1] :
( ~ sP46(X0)
| r1(sK55(X2),sK56(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ sP46(X0)
| r1(X2,sK55(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f222,plain,
! [X0,X5] :
( ~ sP45(X0)
| p2(sK59(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f70]) ).
fof(f223,plain,
! [X0,X5] :
( ~ sP45(X0)
| ~ p2(sK60(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f70]) ).
fof(f224,plain,
! [X0,X5] :
( ~ sP45(X0)
| r1(sK59(X5),sK60(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f70]) ).
fof(f225,plain,
! [X0,X5] :
( ~ sP45(X0)
| r1(X5,sK59(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f70]) ).
fof(f226,plain,
! [X3,X0,X4] :
( ~ sP45(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK58(X0),X3) ),
inference(cnf_transformation,[],[f70]) ).
fof(f227,plain,
! [X0] :
( ~ sP45(X0)
| ~ p2(sK58(X0)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f228,plain,
! [X0] :
( ~ sP45(X0)
| r1(sK57(X0),sK58(X0)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f229,plain,
! [X0] :
( ~ sP45(X0)
| r1(X0,sK57(X0)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f230,plain,
! [X0,X1] :
( ~ sP44(X0)
| p2(sK62(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f73]) ).
fof(f231,plain,
! [X0,X1] :
( ~ sP44(X0)
| ~ p2(sK63(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f73]) ).
fof(f232,plain,
! [X0,X1] :
( ~ sP44(X0)
| r1(sK62(X1),sK63(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f73]) ).
fof(f233,plain,
! [X0,X1] :
( ~ sP44(X0)
| r1(X1,sK62(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f73]) ).
fof(f237,plain,
! [X0,X5] :
( ~ sP43(X0)
| p2(sK66(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f76]) ).
fof(f238,plain,
! [X0,X5] :
( ~ sP43(X0)
| ~ p2(sK67(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f76]) ).
fof(f239,plain,
! [X0,X5] :
( ~ sP43(X0)
| r1(sK66(X5),sK67(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f76]) ).
fof(f240,plain,
! [X0,X5] :
( ~ sP43(X0)
| r1(X5,sK66(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f76]) ).
fof(f501,plain,
! [X82,X83,X80] :
( ~ p2(X82)
| p2(X83)
| ~ r1(X82,X83)
| ~ r1(sK160(X80),X82)
| p2(X80)
| ~ r1(sK128,X80) ),
inference(cnf_transformation,[],[f203]) ).
fof(f502,plain,
! [X80] :
( ~ p2(sK160(X80))
| p2(X80)
| ~ r1(sK128,X80) ),
inference(cnf_transformation,[],[f203]) ).
fof(f503,plain,
! [X80] :
( r1(X80,sK160(X80))
| p2(X80)
| ~ r1(sK128,X80) ),
inference(cnf_transformation,[],[f203]) ).
fof(f582,plain,
! [X21,X19,X20] :
( ~ p2(X20)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| sP43(X19)
| sP44(X19)
| ~ r1(sK139,X19)
| sP47(sK128) ),
inference(cnf_transformation,[],[f203]) ).
fof(f583,plain,
! [X19] :
( ~ p2(X19)
| sP43(X19)
| sP44(X19)
| ~ r1(sK139,X19)
| sP47(sK128) ),
inference(cnf_transformation,[],[f203]) ).
fof(f584,plain,
! [X18,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(sK139,X17)
| sP45(sK139)
| sP47(sK128) ),
inference(cnf_transformation,[],[f203]) ).
fof(f585,plain,
( ~ p2(sK139)
| sP45(sK139)
| sP47(sK128) ),
inference(cnf_transformation,[],[f203]) ).
fof(f586,plain,
( r1(sK128,sK139)
| sP47(sK128) ),
inference(cnf_transformation,[],[f203]) ).
fof(f593,plain,
! [X10] :
( sP48(sK128)
| p5(sK135(X10))
| ~ r1(sK128,X10) ),
inference(cnf_transformation,[],[f203]) ).
fof(f594,plain,
! [X10] :
( sP48(sK128)
| r1(X10,sK135(X10))
| ~ r1(sK128,X10) ),
inference(cnf_transformation,[],[f203]) ).
fof(f598,plain,
! [X7] :
( r1(X7,sK133(X7))
| p3(X7)
| ~ r1(sK128,X7) ),
inference(cnf_transformation,[],[f203]) ).
fof(f601,plain,
! [X3,X1] :
( p2(sK130(X3))
| p2(X3)
| ~ r1(sK128,X3)
| ~ p5(X1)
| ~ r1(sK128,X1) ),
inference(cnf_transformation,[],[f203]) ).
fof(f602,plain,
! [X3,X1] :
( ~ p2(sK131(X3))
| p2(X3)
| ~ r1(sK128,X3)
| ~ p5(X1)
| ~ r1(sK128,X1) ),
inference(cnf_transformation,[],[f203]) ).
fof(f603,plain,
! [X3,X1] :
( r1(sK130(X3),sK131(X3))
| p2(X3)
| ~ r1(sK128,X3)
| ~ p5(X1)
| ~ r1(sK128,X1) ),
inference(cnf_transformation,[],[f203]) ).
fof(f604,plain,
! [X3,X1] :
( r1(X3,sK130(X3))
| p2(X3)
| ~ r1(sK128,X3)
| ~ p5(X1)
| ~ r1(sK128,X1) ),
inference(cnf_transformation,[],[f203]) ).
fof(f605,plain,
! [X1] :
( ~ p2(sK129)
| ~ p5(X1)
| ~ r1(sK128,X1) ),
inference(cnf_transformation,[],[f203]) ).
fof(f606,plain,
! [X1] :
( r1(sK128,sK129)
| ~ p5(X1)
| ~ r1(sK128,X1) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f204]) ).
tcf(c_50,plain,
! [X0: $i] :
( r1(X0,sK49(X0))
| ~ sP48(X0) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_51,plain,
! [X0: $i] :
( ~ sP48(X0)
| ~ p2(sK49(X0)) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK50(X1))
| ~ sP48(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK50(X1),sK51(X1))
| ~ sP48(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP48(X0)
| ~ p2(sK51(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK50(X1))
| ~ sP48(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_56,plain,
! [X0: $i] :
( sP46(X0)
| r1(X0,sK52(X0))
| ~ sP47(X0) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_57,plain,
! [X0: $i] :
( sP46(X0)
| ~ sP47(X0)
| ~ p2(sK52(X0)) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP46(X0)
| p2(X2)
| ~ sP47(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK52(X0),X1) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK55(X2))
| ~ sP46(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK55(X2),sK56(X2))
| ~ sP46(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP46(X0)
| ~ p2(sK56(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK55(X2))
| ~ sP46(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_67,plain,
! [X0: $i] :
( r1(X0,sK57(X0))
| ~ sP45(X0) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_68,plain,
! [X0: $i] :
( r1(sK57(X0),sK58(X0))
| ~ sP45(X0) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_69,plain,
! [X0: $i] :
( ~ sP45(X0)
| ~ p2(sK58(X0)) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP45(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK58(X0),X1) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK59(X1))
| ~ sP45(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK59(X1),sK60(X1))
| ~ sP45(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP45(X0)
| ~ p2(sK60(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK59(X1))
| ~ sP45(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK62(X1))
| ~ sP44(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK62(X1),sK63(X1))
| ~ sP44(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP44(X0)
| ~ p2(sK63(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK62(X1))
| ~ sP44(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK66(X1))
| ~ sP43(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK66(X1),sK67(X1))
| ~ sP43(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP43(X0)
| ~ p2(sK67(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK66(X1))
| ~ sP43(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_346,negated_conjecture,
! [X0: $i] :
( r1(sK128,sK129)
| ~ p5(X0)
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f606]) ).
tcf(c_347,negated_conjecture,
! [X0: $i] :
( ~ p2(sK129)
| ~ p5(X0)
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f605]) ).
tcf(c_348,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(X0,sK130(X0))
| ~ p5(X1)
| ~ r1(sK128,X1)
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f604]) ).
tcf(c_349,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(sK130(X0),sK131(X0))
| ~ p5(X1)
| ~ r1(sK128,X1)
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f603]) ).
tcf(c_350,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| ~ p5(X1)
| ~ p2(sK131(X0))
| ~ r1(sK128,X1)
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f602]) ).
tcf(c_351,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| p2(sK130(X0))
| ~ p5(X1)
| ~ r1(sK128,X1)
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f601]) ).
tcf(c_354,negated_conjecture,
! [X0: $i] :
( p3(X0)
| r1(X0,sK133(X0))
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f598]) ).
tcf(c_358,negated_conjecture,
! [X0: $i] :
( sP48(sK128)
| r1(X0,sK135(X0))
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f594]) ).
tcf(c_359,negated_conjecture,
! [X0: $i] :
( sP48(sK128)
| p5(sK135(X0))
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f593]) ).
tcf(c_366,negated_conjecture,
( sP47(sK128)
| r1(sK128,sK139) ),
inference(cnf_transformation,[],[f586]) ).
tcf(c_367,negated_conjecture,
( sP45(sK139)
| sP47(sK128)
| ~ p2(sK139) ),
inference(cnf_transformation,[],[f585]) ).
tcf(c_368,negated_conjecture,
! [X0: $i,X1: $i] :
( sP45(sK139)
| sP47(sK128)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK139,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f584]) ).
tcf(c_369,negated_conjecture,
! [X0: $i] :
( sP47(sK128)
| sP43(X0)
| sP44(X0)
| ~ p2(X0)
| ~ r1(sK139,X0) ),
inference(cnf_transformation,[],[f583]) ).
tcf(c_370,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP47(sK128)
| sP43(X0)
| sP44(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK139,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f582]) ).
tcf(c_449,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK160(X0))
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f503]) ).
tcf(c_450,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK160(X0))
| ~ r1(sK128,X0) ),
inference(cnf_transformation,[],[f502]) ).
tcf(c_451,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK128,X0)
| ~ r1(X1,X2)
| ~ r1(sK160(X0),X1) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_452,plain,
r1(sK128,sK128),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_619,plain,
( ~ sP48(sK128)
| ~ p2(sK49(sK128)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_620,plain,
( r1(sK128,sK49(sK128))
| ~ sP48(sK128) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_650,plain,
( sP46(sK128)
| ~ sP47(sK128)
| ~ p2(sK52(sK128)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_656,plain,
( sP48(sK128)
| r1(sK128,sK135(sK128))
| ~ r1(sK128,sK128) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_5757,plain,
! [X0: $i] :
( sP48(sK128)
| ~ p2(sK129)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK135(X0)) ),
inference(resolution,[status(thm)],[c_347,c_359]) ).
tcf(c_5758,plain,
( sP48(sK128)
| ~ p2(sK129)
| ~ r1(sK128,sK128)
| ~ r1(sK128,sK135(sK128)) ),
inference(instantiation,[status(thm)],[c_5757]) ).
tcf(c_5759,plain,
( sP48(sK128)
| ~ p2(sK129) ),
inference(global_subsumption_just,[status(thm)],[c_5757,c_452,c_656,c_5758]) ).
tcf(c_5767,plain,
! [X0: $i] :
( sP48(sK128)
| r1(sK128,sK129)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK135(X0)) ),
inference(resolution,[status(thm)],[c_346,c_359]) ).
tcf(c_5768,plain,
( sP48(sK128)
| r1(sK128,sK129)
| ~ r1(sK128,sK128)
| ~ r1(sK128,sK135(sK128)) ),
inference(instantiation,[status(thm)],[c_5767]) ).
tcf(c_5769,plain,
( sP48(sK128)
| r1(sK128,sK129) ),
inference(global_subsumption_just,[status(thm)],[c_5767,c_452,c_656,c_5768]) ).
tcf(c_5777,plain,
! [X0: $i,X1: $i] :
( sP48(sK128)
| p2(X1)
| p2(sK130(X1))
| ~ r1(sK128,X1)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK135(X0)) ),
inference(resolution,[status(thm)],[c_351,c_359]) ).
tcf(c_5797,plain,
! [X0: $i,X1: $i] :
( sP48(sK128)
| p2(X1)
| ~ p2(sK131(X1))
| ~ r1(sK128,X1)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK135(X0)) ),
inference(resolution,[status(thm)],[c_350,c_359]) ).
tcf(c_5817,plain,
! [X0: $i,X1: $i] :
( sP48(sK128)
| p2(X1)
| r1(sK130(X1),sK131(X1))
| ~ r1(sK128,X1)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK135(X0)) ),
inference(resolution,[status(thm)],[c_349,c_359]) ).
tcf(c_5837,plain,
! [X0: $i,X1: $i] :
( sP48(sK128)
| p2(X1)
| r1(X1,sK130(X1))
| ~ r1(sK128,X1)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK135(X0)) ),
inference(resolution,[status(thm)],[c_348,c_359]) ).
tcf(c_6475,plain,
( sP47(sK128)
| ~ p2(sK139)
| ~ p2(sK58(sK139)) ),
inference(resolution,[status(thm)],[c_69,c_367]) ).
tcf(c_6504,plain,
( sP47(sK128)
| r1(sK57(sK139),sK58(sK139))
| ~ p2(sK139) ),
inference(resolution,[status(thm)],[c_68,c_367]) ).
tcf(c_6533,plain,
( sP47(sK128)
| r1(sK139,sK57(sK139))
| ~ p2(sK139) ),
inference(resolution,[status(thm)],[c_67,c_367]) ).
tcf(c_14588,plain,
! [X0: $i] :
( ~ iPr_def_10
| p2(X0)
| ~ r1(sK128,X0)
| r1(X0,sK130(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_5837]) ).
tcf(c_14589,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ r1(sK128,sK135(X0))
| ~ r1(sK128,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_5837]) ).
tcf(c_14590,plain,
( iPr_def_11
| iPr_def_10
| sP48(sK128) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_5837]) ).
tcf(c_14591,plain,
! [X0: $i] :
( ~ iPr_def_12
| p2(X0)
| ~ r1(sK128,X0)
| r1(sK130(X0),sK131(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_5817]) ).
tcf(c_14592,plain,
( iPr_def_12
| iPr_def_11
| sP48(sK128) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_5817]) ).
tcf(c_14593,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p2(sK131(X0))
| p2(X0)
| ~ r1(sK128,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_5797]) ).
tcf(c_14594,plain,
( iPr_def_13
| iPr_def_11
| sP48(sK128) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_5797]) ).
tcf(c_14595,plain,
! [X0: $i] :
( ~ iPr_def_14
| p2(sK130(X0))
| p2(X0)
| ~ r1(sK128,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_5777]) ).
tcf(c_14596,plain,
( iPr_def_14
| iPr_def_11
| sP48(sK128) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_5777]) ).
tcf(c_14597,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_15
| p2(X1)
| ~ p2(X0)
| ~ r1(sK139,X0)
| ~ r1(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_368]) ).
tcf(c_14598,negated_conjecture,
( iPr_def_15
| sP45(sK139)
| sP47(sK128) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_368]) ).
tcf(c_14599,plain,
( ~ iPr_def_11
| ~ r1(sK128,sK128)
| ~ r1(sK128,sK135(sK128)) ),
inference(instantiation,[status(thm)],[c_14589]) ).
tcf(c_14645,plain,
! [X0: $i] :
( p2(sK49(X0))
| r1(sK49(X0),sK160(sK49(X0)))
| ~ r1(sK128,sK49(X0)) ),
inference(instantiation,[status(thm)],[c_449]) ).
tcf(c_14646,plain,
( p2(sK49(sK128))
| r1(sK49(sK128),sK160(sK49(sK128)))
| ~ r1(sK128,sK49(sK128)) ),
inference(instantiation,[status(thm)],[c_14645]) ).
tcf(c_14660,plain,
( p2(sK129)
| r1(sK129,sK160(sK129))
| ~ r1(sK128,sK129) ),
inference(instantiation,[status(thm)],[c_449]) ).
tcf(c_14733,plain,
! [X0: $i,X1: $i] :
( sP47(sK128)
| p2(X1)
| sP43(sK57(sK139))
| sP44(sK57(sK139))
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK139,sK57(sK139))
| ~ r1(sK57(sK139),X0) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_14854,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK129))
| r1(sK55(sK160(sK129)),sK56(sK160(sK129)))
| ~ sP46(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_14859,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK129))
| ~ sP46(X1)
| ~ r1(X1,X0)
| ~ p2(sK56(sK160(sK129)))
| ~ r1(X0,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_14860,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK129))
| r1(sK160(sK129),sK55(sK160(sK129)))
| ~ sP46(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_14862,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK129))
| p2(sK55(sK160(sK129)))
| ~ sP46(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_14888,plain,
! [X0: $i] :
( p2(sK58(sK139))
| r1(sK66(sK58(sK139)),sK67(sK58(sK139)))
| ~ sP43(X0)
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_14889,plain,
! [X0: $i] :
( p2(sK58(sK139))
| r1(sK62(sK58(sK139)),sK63(sK58(sK139)))
| ~ sP44(X0)
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_14892,plain,
! [X0: $i] :
( p2(sK58(sK139))
| ~ sP43(X0)
| ~ p2(sK67(sK58(sK139)))
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_14893,plain,
! [X0: $i] :
( p2(sK58(sK139))
| r1(sK58(sK139),sK66(sK58(sK139)))
| ~ sP43(X0)
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_14894,plain,
! [X0: $i] :
( p2(sK58(sK139))
| ~ sP44(X0)
| ~ p2(sK63(sK58(sK139)))
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_14895,plain,
! [X0: $i] :
( p2(sK58(sK139))
| r1(sK58(sK139),sK62(sK58(sK139)))
| ~ sP44(X0)
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_14900,plain,
! [X0: $i] :
( p2(sK58(sK139))
| p2(sK66(sK58(sK139)))
| ~ sP43(X0)
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_14901,plain,
! [X0: $i] :
( p2(sK58(sK139))
| p2(sK62(sK58(sK139)))
| ~ sP44(X0)
| ~ r1(X0,sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_15019,plain,
! [X0: $i] :
( p2(sK52(X0))
| p2(sK130(sK52(X0)))
| ~ iPr_def_14
| ~ r1(sK128,sK52(X0)) ),
inference(instantiation,[status(thm)],[c_14595]) ).
tcf(c_15020,plain,
! [X0: $i] :
( p2(sK52(X0))
| ~ iPr_def_13
| ~ p2(sK131(sK52(X0)))
| ~ r1(sK128,sK52(X0)) ),
inference(instantiation,[status(thm)],[c_14593]) ).
tcf(c_15102,plain,
! [X0: $i] :
( p2(sK160(sK129))
| ~ sP46(X0)
| ~ r1(X0,sK129)
| ~ p2(sK56(sK160(sK129)))
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_14859]) ).
tcf(c_15103,plain,
( p2(sK160(sK129))
| ~ sP46(sK128)
| ~ r1(sK128,sK129)
| ~ p2(sK56(sK160(sK129)))
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_15102]) ).
tcf(c_15205,plain,
( sP48(sK128)
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_14590,c_452,c_656,c_14590,c_14599]) ).
tcf(c_15206,plain,
( iPr_def_10
| sP48(sK128) ),
inference(renaming,[status(thm)],[c_15205]) ).
tcf(c_15207,plain,
( iPr_def_12
| sP48(sK128) ),
inference(global_subsumption_just,[status(thm)],[c_14592,c_452,c_656,c_14592,c_14599]) ).
tcf(c_15209,plain,
( iPr_def_13
| sP48(sK128) ),
inference(global_subsumption_just,[status(thm)],[c_14594,c_452,c_656,c_14594,c_14599]) ).
tcf(c_15211,plain,
( iPr_def_14
| sP48(sK128) ),
inference(global_subsumption_just,[status(thm)],[c_14596,c_452,c_656,c_14596,c_14599]) ).
tcf(c_15220,plain,
! [X0: $i] :
( p2(sK160(sK129))
| r1(sK55(sK160(sK129)),sK56(sK160(sK129)))
| ~ sP46(X0)
| ~ r1(X0,sK129)
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_14854]) ).
tcf(c_15221,plain,
( p2(sK160(sK129))
| r1(sK55(sK160(sK129)),sK56(sK160(sK129)))
| ~ sP46(sK128)
| ~ r1(sK128,sK129)
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_15220]) ).
tcf(c_15231,plain,
! [X0: $i] :
( p2(sK160(sK129))
| r1(sK160(sK129),sK55(sK160(sK129)))
| ~ sP46(X0)
| ~ r1(X0,sK129)
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_14860]) ).
tcf(c_15232,plain,
( p2(sK160(sK129))
| r1(sK160(sK129),sK55(sK160(sK129)))
| ~ sP46(sK128)
| ~ r1(sK128,sK129)
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_15231]) ).
tcf(c_15235,plain,
! [X0: $i] :
( p2(sK160(sK129))
| p2(sK55(sK160(sK129)))
| ~ sP46(X0)
| ~ r1(X0,sK129)
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_14862]) ).
tcf(c_15236,plain,
( p2(sK160(sK129))
| p2(sK55(sK160(sK129)))
| ~ sP46(sK128)
| ~ r1(sK128,sK129)
| ~ r1(sK129,sK160(sK129)) ),
inference(instantiation,[status(thm)],[c_15235]) ).
tcf(c_15257,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK56(sK160(sK129)))
| ~ p2(X0)
| ~ r1(sK128,X1)
| ~ r1(sK160(X1),X0)
| ~ r1(X0,sK56(sK160(sK129))) ),
inference(instantiation,[status(thm)],[c_451]) ).
tcf(c_15380,plain,
( p2(sK49(sK128))
| ~ sP48(sK128)
| ~ p2(sK160(sK49(sK128))) ),
inference(superposition,[status(thm)],[c_50,c_450]) ).
tcf(c_15383,plain,
( p2(sK129)
| sP48(sK128)
| ~ p2(sK160(sK129)) ),
inference(superposition,[status(thm)],[c_5769,c_450]) ).
tcf(c_15539,plain,
( p2(sK129)
| p2(sK56(sK160(sK129)))
| ~ r1(sK128,sK129)
| ~ p2(sK55(sK160(sK129)))
| ~ r1(sK160(sK129),sK55(sK160(sK129)))
| ~ r1(sK55(sK160(sK129)),sK56(sK160(sK129))) ),
inference(instantiation,[status(thm)],[c_15257]) ).
tcf(c_16256,plain,
( sP47(sK128)
| p2(sK139)
| p2(sK130(sK139))
| ~ iPr_def_14 ),
inference(resolution,[status(thm)],[c_14595,c_366]) ).
tcf(c_16731,plain,
( p2(sK129)
| sP48(sK128)
| ~ p2(sK160(sK129)) ),
inference(superposition,[status(thm)],[c_5769,c_450]) ).
tcf(c_16736,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| p2(sK50(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(superposition,[status(thm)],[c_56,c_55]) ).
tcf(c_16751,plain,
( sP47(sK128)
| p2(sK139)
| p2(sK50(sK139))
| ~ sP48(sK128) ),
inference(superposition,[status(thm)],[c_366,c_55]) ).
tcf(c_16833,plain,
( sP47(sK128)
| sP43(sK57(sK139))
| sP44(sK57(sK139))
| ~ sP45(sK139)
| ~ p2(sK57(sK139)) ),
inference(resolution,[status(thm)],[c_369,c_67]) ).
tcf(c_16970,plain,
! [X0: $i] :
( p2(X0)
| p2(sK160(X0))
| p2(sK59(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(superposition,[status(thm)],[c_449,c_74]) ).
tcf(c_17036,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK160(sK49(X1)))
| r1(sK55(sK160(sK49(X1))),sK56(sK160(sK49(X1))))
| ~ sP46(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK160(sK49(X1))) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_17041,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK160(sK49(X1)))
| ~ sP46(X2)
| ~ r1(X2,X0)
| ~ p2(sK56(sK160(sK49(X1))))
| ~ r1(X0,sK160(sK49(X1))) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_17042,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK160(sK49(X1)))
| r1(sK160(sK49(X1)),sK55(sK160(sK49(X1))))
| ~ sP46(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK160(sK49(X1))) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_17044,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK160(sK49(X1)))
| p2(sK55(sK160(sK49(X1))))
| ~ sP46(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK160(sK49(X1))) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_17588,plain,
! [X0: $i] :
( p2(sK139)
| p2(X0)
| ~ iPr_def_15
| ~ iPr_def_10
| ~ p2(sK130(sK139))
| ~ r1(sK128,sK139)
| ~ r1(sK130(sK139),X0) ),
inference(resolution,[status(thm)],[c_14588,c_14597]) ).
tcf(c_17873,plain,
( ~ p2(sK160(sK129))
| sP48(sK128) ),
inference(global_subsumption_just,[status(thm)],[c_16731,c_5759,c_15383]) ).
tcf(c_17874,plain,
( sP48(sK128)
| ~ p2(sK160(sK129)) ),
inference(renaming,[status(thm)],[c_17873]) ).
tcf(c_17877,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| r1(sK52(X0),sK50(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(superposition,[status(thm)],[c_56,c_52]) ).
tcf(c_17995,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK49(X0)))
| ~ sP46(X1)
| ~ r1(X1,sK49(X0))
| ~ p2(sK56(sK160(sK49(X0))))
| ~ r1(sK49(X0),sK160(sK49(X0))) ),
inference(instantiation,[status(thm)],[c_17041]) ).
tcf(c_17996,plain,
( p2(sK160(sK49(sK128)))
| ~ sP46(sK128)
| ~ r1(sK128,sK49(sK128))
| ~ p2(sK56(sK160(sK49(sK128))))
| ~ r1(sK49(sK128),sK160(sK49(sK128))) ),
inference(instantiation,[status(thm)],[c_17995]) ).
tcf(c_18139,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| ~ sP47(X0)
| ~ sP48(X0)
| ~ p2(sK51(sK52(X0))) ),
inference(superposition,[status(thm)],[c_56,c_54]) ).
tcf(c_18154,plain,
( sP47(sK128)
| p2(sK139)
| ~ sP48(sK128)
| ~ p2(sK51(sK139)) ),
inference(superposition,[status(thm)],[c_366,c_54]) ).
tcf(c_18165,plain,
( sP46(sK128)
| p2(sK52(sK128))
| ~ sP47(sK128)
| ~ sP48(sK128)
| ~ p2(sK51(sK52(sK128))) ),
inference(instantiation,[status(thm)],[c_18139]) ).
tcf(c_18391,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK49(X0)))
| p2(sK55(sK160(sK49(X0))))
| ~ sP46(X1)
| ~ r1(X1,sK49(X0))
| ~ r1(sK49(X0),sK160(sK49(X0))) ),
inference(instantiation,[status(thm)],[c_17044]) ).
tcf(c_18392,plain,
( p2(sK160(sK49(sK128)))
| p2(sK55(sK160(sK49(sK128))))
| ~ sP46(sK128)
| ~ r1(sK128,sK49(sK128))
| ~ r1(sK49(sK128),sK160(sK49(sK128))) ),
inference(instantiation,[status(thm)],[c_18391]) ).
tcf(c_18419,plain,
! [X0: $i] :
( p2(X0)
| p2(sK160(X0))
| r1(sK160(X0),sK59(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(superposition,[status(thm)],[c_449,c_71]) ).
tcf(c_18438,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK49(X0)))
| r1(sK55(sK160(sK49(X0))),sK56(sK160(sK49(X0))))
| ~ sP46(X1)
| ~ r1(X1,sK49(X0))
| ~ r1(sK49(X0),sK160(sK49(X0))) ),
inference(instantiation,[status(thm)],[c_17036]) ).
tcf(c_18439,plain,
( p2(sK160(sK49(sK128)))
| r1(sK55(sK160(sK49(sK128))),sK56(sK160(sK49(sK128))))
| ~ sP46(sK128)
| ~ r1(sK128,sK49(sK128))
| ~ r1(sK49(sK128),sK160(sK49(sK128))) ),
inference(instantiation,[status(thm)],[c_18438]) ).
tcf(c_18442,plain,
! [X0: $i,X1: $i] :
( p2(sK160(sK49(X0)))
| r1(sK160(sK49(X0)),sK55(sK160(sK49(X0))))
| ~ sP46(X1)
| ~ r1(X1,sK49(X0))
| ~ r1(sK49(X0),sK160(sK49(X0))) ),
inference(instantiation,[status(thm)],[c_17042]) ).
tcf(c_18443,plain,
( p2(sK160(sK49(sK128)))
| r1(sK160(sK49(sK128)),sK55(sK160(sK49(sK128))))
| ~ sP46(sK128)
| ~ r1(sK128,sK49(sK128))
| ~ r1(sK49(sK128),sK160(sK49(sK128))) ),
inference(instantiation,[status(thm)],[c_18442]) ).
tcf(c_18630,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK56(sK160(sK49(X1))))
| ~ p2(X0)
| ~ r1(sK128,X2)
| ~ r1(sK160(X2),X0)
| ~ r1(X0,sK56(sK160(sK49(X1)))) ),
inference(instantiation,[status(thm)],[c_451]) ).
tcf(c_18877,plain,
( sP47(sK128)
| p2(sK139)
| r1(sK139,sK50(sK139))
| ~ sP48(sK128) ),
inference(resolution,[status(thm)],[c_52,c_366]) ).
tcf(c_19224,plain,
! [X0: $i] :
( p2(X0)
| p2(sK160(X0))
| ~ sP45(X0)
| ~ r1(sK128,X0)
| ~ p2(sK60(sK160(X0))) ),
inference(superposition,[status(thm)],[c_449,c_73]) ).
tcf(c_19418,plain,
! [X0: $i] :
( p2(X0)
| p2(sK160(X0))
| r1(sK160(X0),sK59(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(resolution,[status(thm)],[c_71,c_449]) ).
tcf(c_19613,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK56(sK160(sK49(X0))))
| ~ r1(sK128,X1)
| ~ p2(sK55(sK160(sK49(X0))))
| ~ r1(sK160(X1),sK55(sK160(sK49(X0))))
| ~ r1(sK55(sK160(sK49(X0))),sK56(sK160(sK49(X0)))) ),
inference(instantiation,[status(thm)],[c_18630]) ).
tcf(c_20104,plain,
! [X0: $i] :
( sP47(sK128)
| p2(sK139)
| p2(X0)
| ~ iPr_def_15
| ~ sP48(sK128)
| ~ p2(sK50(sK139))
| ~ r1(sK50(sK139),X0) ),
inference(resolution,[status(thm)],[c_18877,c_14597]) ).
tcf(c_21412,plain,
! [X0: $i] :
( p2(sK49(X0))
| p2(sK56(sK160(sK49(X0))))
| ~ r1(sK128,sK49(X0))
| ~ p2(sK55(sK160(sK49(X0))))
| ~ r1(sK160(sK49(X0)),sK55(sK160(sK49(X0))))
| ~ r1(sK55(sK160(sK49(X0))),sK56(sK160(sK49(X0)))) ),
inference(instantiation,[status(thm)],[c_19613]) ).
tcf(c_21413,plain,
( p2(sK49(sK128))
| p2(sK56(sK160(sK49(sK128))))
| ~ r1(sK128,sK49(sK128))
| ~ p2(sK55(sK160(sK49(sK128))))
| ~ r1(sK160(sK49(sK128)),sK55(sK160(sK49(sK128))))
| ~ r1(sK55(sK160(sK49(sK128))),sK56(sK160(sK49(sK128)))) ),
inference(instantiation,[status(thm)],[c_21412]) ).
tcf(c_21776,plain,
! [X0: $i] :
( p2(sK57(sK139))
| r1(sK59(sK57(sK139)),sK60(sK57(sK139)))
| ~ sP45(X0)
| ~ r1(X0,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_21782,plain,
! [X0: $i] :
( p2(sK57(sK139))
| ~ sP45(X0)
| ~ p2(sK60(sK57(sK139)))
| ~ r1(X0,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_21783,plain,
! [X0: $i] :
( p2(sK57(sK139))
| r1(sK57(sK139),sK59(sK57(sK139)))
| ~ sP45(X0)
| ~ r1(X0,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_21788,plain,
! [X0: $i] :
( p2(sK57(sK139))
| p2(sK59(sK57(sK139)))
| ~ sP45(X0)
| ~ r1(X0,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_22145,plain,
( sP47(sK128)
| p2(sK139)
| r1(sK50(sK139),sK51(sK139))
| ~ sP48(sK128) ),
inference(resolution,[status(thm)],[c_53,c_366]) ).
tcf(c_22185,plain,
( p2(sK57(sK139))
| ~ sP45(sK139)
| ~ p2(sK60(sK57(sK139)))
| ~ r1(sK139,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_21782]) ).
tcf(c_22436,plain,
( p2(sK57(sK139))
| r1(sK59(sK57(sK139)),sK60(sK57(sK139)))
| ~ sP45(sK139)
| ~ r1(sK139,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_21776]) ).
tcf(c_22445,plain,
( p2(sK57(sK139))
| r1(sK57(sK139),sK59(sK57(sK139)))
| ~ sP45(sK139)
| ~ r1(sK139,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_21783]) ).
tcf(c_22454,plain,
( p2(sK57(sK139))
| p2(sK59(sK57(sK139)))
| ~ sP45(sK139)
| ~ r1(sK139,sK57(sK139)) ),
inference(instantiation,[status(thm)],[c_21788]) ).
tcf(c_23161,plain,
( p2(sK49(sK128))
| ~ sP48(sK128)
| ~ p2(sK160(sK49(sK128))) ),
inference(superposition,[status(thm)],[c_50,c_450]) ).
tcf(c_23846,plain,
! [X0: $i] :
( p2(X0)
| p2(sK160(X0))
| r1(sK59(sK160(X0)),sK60(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(resolution,[status(thm)],[c_72,c_449]) ).
tcf(c_23873,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| r1(sK50(sK52(X0)),sK51(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(superposition,[status(thm)],[c_56,c_53]) ).
tcf(c_24158,plain,
( p2(sK58(sK139))
| p2(sK62(sK58(sK139)))
| ~ sP44(sK57(sK139))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14901]) ).
tcf(c_24159,plain,
( p2(sK58(sK139))
| r1(sK58(sK139),sK62(sK58(sK139)))
| ~ sP44(sK57(sK139))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14895]) ).
tcf(c_24160,plain,
( p2(sK58(sK139))
| r1(sK62(sK58(sK139)),sK63(sK58(sK139)))
| ~ sP44(sK57(sK139))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14889]) ).
tcf(c_24167,plain,
( p2(sK58(sK139))
| ~ sP44(sK57(sK139))
| ~ p2(sK63(sK58(sK139)))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14894]) ).
tcf(c_24711,plain,
! [X0: $i,X1: $i] :
( p2(sK63(sK58(sK139)))
| ~ sP45(X1)
| ~ p2(X0)
| ~ r1(sK58(X1),X0)
| ~ r1(X0,sK63(sK58(sK139))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_26921,plain,
! [X0: $i] :
( p2(sK63(sK58(sK139)))
| ~ sP45(X0)
| ~ p2(sK62(sK58(sK139)))
| ~ r1(sK58(X0),sK62(sK58(sK139)))
| ~ r1(sK62(sK58(sK139)),sK63(sK58(sK139))) ),
inference(instantiation,[status(thm)],[c_24711]) ).
tcf(c_27268,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK128,X0)
| ~ sP45(X0)
| r1(sK160(X0),sK59(sK160(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_19418,c_450,c_18419]) ).
tcf(c_27269,plain,
! [X0: $i] :
( p2(X0)
| r1(sK160(X0),sK59(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(renaming,[status(thm)],[c_27268]) ).
tcf(c_27305,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP45(X0)
| ~ r1(sK128,X0)
| ~ p2(sK59(sK160(X0)))
| ~ r1(sK59(sK160(X0)),X1) ),
inference(resolution,[status(thm)],[c_27269,c_451]) ).
tcf(c_28571,plain,
( p2(sK63(sK58(sK139)))
| ~ sP45(sK139)
| ~ p2(sK62(sK58(sK139)))
| ~ r1(sK58(sK139),sK62(sK58(sK139)))
| ~ r1(sK62(sK58(sK139)),sK63(sK58(sK139))) ),
inference(instantiation,[status(thm)],[c_26921]) ).
tcf(c_29272,plain,
! [X0: $i] :
( sP47(sK128)
| p2(X0)
| sP43(sK57(sK139))
| sP44(sK57(sK139))
| ~ p2(sK59(sK57(sK139)))
| ~ r1(sK139,sK57(sK139))
| ~ r1(sK59(sK57(sK139)),X0)
| ~ r1(sK57(sK139),sK59(sK57(sK139))) ),
inference(instantiation,[status(thm)],[c_14733]) ).
tcf(c_30398,plain,
( sP47(sK128)
| sP43(sK57(sK139))
| sP44(sK57(sK139))
| p2(sK60(sK57(sK139)))
| ~ p2(sK59(sK57(sK139)))
| ~ r1(sK139,sK57(sK139))
| ~ r1(sK57(sK139),sK59(sK57(sK139)))
| ~ r1(sK59(sK57(sK139)),sK60(sK57(sK139))) ),
inference(instantiation,[status(thm)],[c_29272]) ).
tcf(c_30596,plain,
( p2(sK139)
| ~ iPr_def_13
| ~ p2(sK131(sK139))
| ~ r1(sK128,sK139) ),
inference(instantiation,[status(thm)],[c_14593]) ).
tcf(c_30892,plain,
( p2(sK58(sK139))
| p2(sK66(sK58(sK139)))
| ~ sP43(sK57(sK139))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14900]) ).
tcf(c_30893,plain,
( p2(sK58(sK139))
| r1(sK58(sK139),sK66(sK58(sK139)))
| ~ sP43(sK57(sK139))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14893]) ).
tcf(c_30894,plain,
( p2(sK58(sK139))
| r1(sK66(sK58(sK139)),sK67(sK58(sK139)))
| ~ sP43(sK57(sK139))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14888]) ).
tcf(c_30903,plain,
( p2(sK58(sK139))
| ~ sP43(sK57(sK139))
| ~ p2(sK67(sK58(sK139)))
| ~ r1(sK57(sK139),sK58(sK139)) ),
inference(instantiation,[status(thm)],[c_14892]) ).
tcf(c_31170,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK128,X0)
| ~ sP45(X0)
| r1(sK59(sK160(X0)),sK60(sK160(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_23846,c_450,c_23846]) ).
tcf(c_31171,plain,
! [X0: $i] :
( p2(X0)
| r1(sK59(sK160(X0)),sK60(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(renaming,[status(thm)],[c_31170]) ).
tcf(c_32053,plain,
! [X0: $i,X1: $i] :
( p2(sK67(sK58(sK139)))
| ~ sP45(X1)
| ~ p2(X0)
| ~ r1(sK58(X1),X0)
| ~ r1(X0,sK67(sK58(sK139))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_32264,plain,
( ~ p2(sK160(sK49(sK128)))
| ~ sP48(sK128) ),
inference(global_subsumption_just,[status(thm)],[c_23161,c_619,c_15380]) ).
tcf(c_32265,plain,
( ~ sP48(sK128)
| ~ p2(sK160(sK49(sK128))) ),
inference(renaming,[status(thm)],[c_32264]) ).
tcf(c_34722,plain,
! [X0: $i] :
( p2(sK67(sK58(sK139)))
| ~ sP45(X0)
| ~ p2(sK66(sK58(sK139)))
| ~ r1(sK58(X0),sK66(sK58(sK139)))
| ~ r1(sK66(sK58(sK139)),sK67(sK58(sK139))) ),
inference(instantiation,[status(thm)],[c_32053]) ).
tcf(c_34842,plain,
! [X0: $i] :
( sP47(sK128)
| p2(sK139)
| p2(X0)
| ~ iPr_def_15
| ~ sP48(sK128)
| ~ r1(sK50(sK139),X0) ),
inference(global_subsumption_just,[status(thm)],[c_20104,c_16751,c_20104]) ).
tcf(c_34874,plain,
( sP47(sK128)
| p2(sK139)
| p3(sK50(sK139))
| p2(sK133(sK50(sK139)))
| ~ iPr_def_15
| ~ sP48(sK128)
| ~ r1(sK128,sK50(sK139)) ),
inference(resolution,[status(thm)],[c_34842,c_354]) ).
tcf(c_34882,plain,
( sP47(sK128)
| p2(sK139)
| p2(sK51(sK139))
| ~ iPr_def_15
| ~ sP48(sK128) ),
inference(resolution,[status(thm)],[c_34842,c_22145]) ).
tcf(c_35269,plain,
( p2(sK139)
| p2(sK131(sK139))
| ~ iPr_def_15
| ~ iPr_def_12
| ~ iPr_def_10
| ~ p2(sK130(sK139))
| ~ r1(sK128,sK139) ),
inference(resolution,[status(thm)],[c_17588,c_14591]) ).
tcf(c_35317,plain,
( sP47(sK128)
| p2(sK139)
| ~ iPr_def_15
| ~ sP48(sK128) ),
inference(global_subsumption_just,[status(thm)],[c_34874,c_18154,c_34882]) ).
tcf(c_35319,plain,
( sP47(sK128)
| p2(sK139)
| ~ iPr_def_15 ),
inference(global_subsumption_just,[status(thm)],[c_35317,c_452,c_366,c_656,c_14590,c_14599,c_15207,c_15209,c_15211,c_16256,c_30596,c_35269,c_35317]) ).
tcf(c_35347,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| p2(sK50(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(resolution,[status(thm)],[c_56,c_55]) ).
tcf(c_35349,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| r1(sK52(X0),sK50(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(resolution,[status(thm)],[c_56,c_52]) ).
tcf(c_35353,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| r1(sK50(sK52(X0)),sK51(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(resolution,[status(thm)],[c_56,c_53]) ).
tcf(c_36206,plain,
! [X0: $i,X1: $i] :
( sP46(X0)
| p2(X1)
| p2(sK52(X0))
| ~ iPr_def_10
| ~ sP47(X0)
| ~ p2(sK130(sK52(X0)))
| ~ r1(sK128,sK52(X0))
| ~ r1(sK130(sK52(X0)),X1) ),
inference(resolution,[status(thm)],[c_58,c_14588]) ).
tcf(c_36773,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP45(X0)
| ~ r1(sK128,X0)
| ~ r1(sK59(sK160(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_27305,c_450,c_16970,c_27305]) ).
tcf(c_37149,plain,
( p2(sK67(sK58(sK139)))
| ~ sP45(sK139)
| ~ p2(sK66(sK58(sK139)))
| ~ r1(sK58(sK139),sK66(sK58(sK139)))
| ~ r1(sK66(sK58(sK139)),sK67(sK58(sK139))) ),
inference(instantiation,[status(thm)],[c_34722]) ).
tcf(c_37183,plain,
! [X0: $i] :
( sP48(sK128)
| p2(X0)
| p2(sK135(sK59(sK160(X0))))
| ~ sP45(X0)
| ~ r1(sK128,X0)
| ~ r1(sK128,sK59(sK160(X0))) ),
inference(resolution,[status(thm)],[c_36773,c_358]) ).
tcf(c_37193,plain,
! [X0: $i] :
( p2(X0)
| p2(sK60(sK160(X0)))
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(resolution,[status(thm)],[c_36773,c_31171]) ).
tcf(c_37991,plain,
! [X0: $i] :
( ~ sP45(X0)
| ~ r1(sK128,X0)
| p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_37183,c_450,c_19224,c_37193]) ).
tcf(c_37992,plain,
! [X0: $i] :
( p2(X0)
| ~ sP45(X0)
| ~ r1(sK128,X0) ),
inference(renaming,[status(thm)],[c_37991]) ).
tcf(c_38019,plain,
( sP47(sK128)
| p2(sK139)
| ~ sP45(sK139) ),
inference(resolution,[status(thm)],[c_37992,c_366]) ).
tcf(c_38104,plain,
( sP47(sK128)
| p2(sK139) ),
inference(global_subsumption_just,[status(thm)],[c_38019,c_14598,c_35319,c_38019]) ).
tcf(c_38113,plain,
( sP45(sK139)
| sP47(sK128) ),
inference(backward_subsumption_resolution,[status(thm)],[c_367,c_38104]) ).
tcf(c_38123,plain,
( sP47(sK128)
| sP43(sK57(sK139))
| sP44(sK57(sK139))
| ~ p2(sK57(sK139)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_16833,c_38113]) ).
tcf(c_38481,plain,
! [X0: $i] :
( sP46(X0)
| ~ sP48(X0)
| ~ sP47(X0)
| p2(sK50(sK52(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_35347,c_57,c_16736]) ).
tcf(c_38482,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK50(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(renaming,[status(thm)],[c_38481]) ).
tcf(c_40619,plain,
! [X0: $i] :
( sP46(X0)
| ~ sP48(X0)
| ~ sP47(X0)
| r1(sK52(X0),sK50(sK52(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_35349,c_57,c_17877]) ).
tcf(c_40620,plain,
! [X0: $i] :
( sP46(X0)
| r1(sK52(X0),sK50(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(renaming,[status(thm)],[c_40619]) ).
tcf(c_40756,plain,
! [X0: $i] :
( sP46(X0)
| ~ sP48(X0)
| ~ sP47(X0)
| r1(sK50(sK52(X0)),sK51(sK52(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_35353,c_57,c_23873]) ).
tcf(c_40757,plain,
! [X0: $i] :
( sP46(X0)
| r1(sK50(sK52(X0)),sK51(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(renaming,[status(thm)],[c_40756]) ).
tcf(c_40823,plain,
( sP47(sK128)
| sP43(sK57(sK139))
| sP44(sK57(sK139)) ),
inference(global_subsumption_just,[status(thm)],[c_38123,c_6533,c_22185,c_22436,c_22445,c_22454,c_30398,c_38104,c_38113,c_38123]) ).
tcf(c_40825,plain,
( sP47(sK128)
| sP43(sK57(sK139)) ),
inference(global_subsumption_just,[status(thm)],[c_40823,c_6475,c_6504,c_24167,c_24160,c_24159,c_24158,c_28571,c_38104,c_38113,c_40823]) ).
tcf(c_40827,plain,
sP47(sK128),
inference(global_subsumption_just,[status(thm)],[c_40825,c_6475,c_6504,c_30903,c_30894,c_30893,c_30892,c_37149,c_38104,c_38113,c_40825]) ).
tcf(c_41842,plain,
! [X0: $i,X1: $i] :
( sP46(X0)
| p2(X1)
| ~ sP47(X0)
| ~ sP48(X0)
| ~ p2(sK50(sK52(X0)))
| ~ r1(sK50(sK52(X0)),X1) ),
inference(resolution,[status(thm)],[c_40620,c_58]) ).
tcf(c_43350,plain,
! [X0: $i,X1: $i] :
( sP46(X0)
| p2(X1)
| ~ r1(sK130(sK52(X0)),X1)
| ~ r1(sK128,sK52(X0))
| ~ p2(sK130(sK52(X0)))
| ~ sP47(X0)
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_36206,c_57,c_36206]) ).
tcf(c_43351,plain,
! [X0: $i,X1: $i] :
( sP46(X0)
| p2(X1)
| ~ iPr_def_10
| ~ sP47(X0)
| ~ p2(sK130(sK52(X0)))
| ~ r1(sK128,sK52(X0))
| ~ r1(sK130(sK52(X0)),X1) ),
inference(renaming,[status(thm)],[c_43350]) ).
tcf(c_45455,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK52(X0))
| p2(sK131(sK52(X0)))
| ~ iPr_def_12
| ~ iPr_def_10
| ~ sP47(X0)
| ~ p2(sK130(sK52(X0)))
| ~ r1(sK128,sK52(X0)) ),
inference(resolution,[status(thm)],[c_43351,c_14591]) ).
tcf(c_45459,plain,
! [X0: $i] :
( sP48(sK128)
| sP46(X0)
| p2(sK135(sK130(sK52(X0))))
| ~ iPr_def_10
| ~ sP47(X0)
| ~ p2(sK130(sK52(X0)))
| ~ r1(sK128,sK52(X0))
| ~ r1(sK128,sK130(sK52(X0))) ),
inference(resolution,[status(thm)],[c_43351,c_358]) ).
tcf(c_45467,plain,
! [X0: $i] :
( sP48(sK128)
| sP46(X0)
| ~ sP47(X0)
| ~ r1(sK128,sK52(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_45459,c_57,c_15020,c_15019,c_15206,c_15207,c_15209,c_15211,c_45455]) ).
tcf(c_45486,plain,
( sP46(sK128)
| sP48(sK128)
| ~ sP47(sK128) ),
inference(resolution,[status(thm)],[c_45467,c_56]) ).
tcf(c_45519,plain,
sP48(sK128),
inference(global_subsumption_just,[status(thm)],[c_45486,c_5759,c_5769,c_14660,c_15103,c_15221,c_15232,c_15236,c_15539,c_17874,c_40827,c_45486]) ).
tcf(c_47092,plain,
! [X0: $i,X1: $i] :
( sP46(X0)
| p2(X1)
| ~ sP47(X0)
| ~ sP48(X0)
| ~ r1(sK50(sK52(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_41842,c_38482,c_41842]) ).
tcf(c_47136,plain,
! [X0: $i] :
( sP46(X0)
| p2(sK51(sK52(X0)))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(resolution,[status(thm)],[c_47092,c_40757]) ).
tcf(c_47137,plain,
( sP46(sK128)
| p2(sK51(sK52(sK128)))
| ~ sP47(sK128)
| ~ sP48(sK128) ),
inference(instantiation,[status(thm)],[c_47136]) ).
tcf(c_47138,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_47137,c_45519,c_40827,c_32265,c_21413,c_18443,c_18439,c_18392,c_18165,c_17996,c_14646,c_650,c_620,c_619]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL660+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 00:04:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 6.42/2.71 % SZS status Started for theBenchmark.p
% 6.42/2.71 % SZS status Theorem for theBenchmark.p
% 6.42/2.71
% 6.42/2.71 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.42/2.71
% 6.42/2.71 % ------ iProver source info
% 6.42/2.71
% 6.42/2.71 % git: date: 2026-07-19 20:42:38 +0200
% 6.42/2.71 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.42/2.71 % git: non_committed_changes: false
% 6.42/2.71
% 6.42/2.71 % ------ Parsing...
% 6.42/2.71 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.42/2.71
% 6.42/2.71 % ------ Preprocessing... sf_s rm: 329 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.42/2.71
% 6.42/2.71 % ------ Preprocessing... gs_s sp: 9 0s gs_e snvd_s sp: 0 0s snvd_e
% 6.42/2.71 % ------ Proving...
% 6.42/2.71 % ------ Problem Properties
% 6.42/2.71
% 6.42/2.71 %
% 6.42/2.71 % clauses 79
% 6.42/2.71 % conjectures 23
% 6.42/2.71 % EPR 20
% 6.42/2.71 % Horn 31
% 6.42/2.71 % unary 5
% 6.42/2.71 % binary 12
% 6.42/2.71 % lits 277
% 6.42/2.71 % lits eq 0
% 6.42/2.71 % fd_pure 0
% 6.42/2.71 % fd_pseudo 0
% 6.42/2.71 % fd_cond 0
% 6.42/2.71 % fd_pseudo_cond 0
% 6.42/2.71 % AC symbols 0
% 6.42/2.71
% 6.42/2.71 % ------ Input Options Time Limit: Unbounded
% 6.42/2.71
% 6.42/2.71
% 6.42/2.71 % ------
% 6.42/2.71 % Current options:
% 6.42/2.71 % ------
% 6.42/2.71
% 6.42/2.71
% 6.42/2.71 %
% 6.42/2.71
% 6.42/2.71 % ------ Proving...
% 6.42/2.71 %
% 6.42/2.71
% 6.42/2.71 % SZS status Theorem for theBenchmark.p
% 6.42/2.71
% 6.42/2.71 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.42/2.72
% 6.42/2.72
%------------------------------------------------------------------------------