%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL676+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/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:08:04 PM UTC 2026
% Result : Theorem 22.32s 5.22s
% Output : CNFRefutation 22.32s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f62ERROR: Could not build tree for root c_43698ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X1,X2)
& r1(X0,X1) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity) ).
fof(f8,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f9,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(flattening,[],[f8]) ).
fof(f63,plain,
! [X0] :
( ~ sP49(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p2(X4)
& r1(X0,X4) ) ) ),
inference(nnf_transformation,[],[f61]) ).
fof(f64,plain,
! [X0] :
( ~ sP49(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,[],[f63]) ).
fof(f65,plain,
! [X0] :
( ~ sP49(X0)
| ( ! [X2] :
( ( p2(sK51(X2))
& ~ p2(sK52(X2))
& r1(sK51(X2),sK52(X2))
& r1(X2,sK51(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK50(X0))
& r1(X0,sK50(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50,sK51,sK52]),skolemize(X1,sK50(X0)),skolemize(X3,sK51(X2)),skolemize(X4,sK52(X2))],[f64]) ).
fof(f66,plain,
! [X0] :
( ~ sP48(X0)
| ( ! [X15] :
( ? [X16] :
( p2(X16)
& ? [X17] :
( ~ p2(X17)
& r1(X16,X17) )
& r1(X15,X16) )
| p2(X15)
| ~ r1(X0,X15) )
& ? [X14] :
( ~ p2(X14)
& r1(X0,X14) ) ) ),
inference(nnf_transformation,[],[f60]) ).
fof(f67,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,[],[f66]) ).
fof(f68,plain,
! [X0] :
( ~ sP48(X0)
| ( ! [X2] :
( ( p2(sK54(X2))
& ~ p2(sK55(X2))
& r1(sK54(X2),sK55(X2))
& r1(X2,sK54(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK53(X0))
& r1(X0,sK53(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53,sK54,sK55]),skolemize(X1,sK53(X0)),skolemize(X3,sK54(X2)),skolemize(X4,sK55(X2))],[f67]) ).
fof(f209,plain,
? [X0] :
( ! [X78] :
( ? [X79] :
( ! [X80] :
( ~ p2(X80)
| ! [X81] :
( p2(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
& ~ p2(X79)
& r1(X78,X79) )
| p2(X78)
| ~ r1(X0,X78) )
& ( ? [X72] :
( ! [X74] :
( ( ? [X77] : r1(X74,X77)
& ~ p1(X74) )
| ! [X75] :
( ! [X76] : ~ r1(X75,X76)
| p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X72,X74) )
& ? [X73] : r1(X72,X73)
& ~ p1(X72)
& r1(X0,X72) )
| ! [X71] : ~ r1(X0,X71)
| p1(X0) )
& ( ? [X65] :
( ! [X67] :
( ( ? [X70] : r1(X67,X70)
& ~ p1(X67)
& ~ p2(X67) )
| ! [X68] :
( ! [X69] : ~ r1(X68,X69)
| p1(X68)
| p2(X68)
| ~ r1(X67,X68) )
| ~ r1(X65,X67) )
& ? [X66] : r1(X65,X66)
& ~ p1(X65)
& ~ p2(X65)
& r1(X0,X65) )
| ! [X64] : ~ r1(X0,X64)
| p1(X0)
| p2(X0) )
& ( ? [X62] :
( sP0(X62)
& ? [X63] : r1(X62,X63)
& ~ p1(X62)
& ~ p2(X62)
& ~ p3(X62)
& r1(X0,X62) )
| ! [X61] : ~ r1(X0,X61)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X59] :
( sP1(X59)
& ? [X60] : r1(X59,X60)
& ~ p1(X59)
& ~ p2(X59)
& ~ p3(X59)
& ~ p4(X59)
& r1(X0,X59) )
| ! [X58] : ~ r1(X0,X58)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X57] :
( sP2(X57)
& sP3(X57)
& ~ p1(X57)
& r1(X0,X57) )
| ! [X55] :
( ! [X56] : ~ r1(X55,X56)
| p1(X55)
| p2(X55)
| p3(X55)
| p4(X55)
| ~ r1(X0,X55) )
| p1(X0) )
& ( ? [X54] :
( sP4(X54)
& sP5(X54)
& ~ p1(X54)
& ~ p2(X54)
& r1(X0,X54) )
| ! [X52] :
( ! [X53] : ~ r1(X52,X53)
| p1(X52)
| p2(X52)
| p3(X52)
| p4(X52)
| ~ r1(X0,X52) )
| p1(X0)
| p2(X0) )
& ( ? [X51] :
( sP8(X51)
& sP7(X51)
& ~ p1(X51)
& ~ p2(X51)
& ~ p3(X51)
& r1(X0,X51) )
| ! [X49] :
( ! [X50] : ~ r1(X49,X50)
| p1(X49)
| p2(X49)
| p3(X49)
| p4(X49)
| ~ r1(X0,X49) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X48] :
( sP11(X48)
& sP10(X48)
& ~ p1(X48)
& ~ p2(X48)
& ~ p3(X48)
& ~ p4(X48)
& r1(X0,X48) )
| ! [X46] :
( ! [X47] : ~ r1(X46,X47)
| p1(X46)
| p2(X46)
| p3(X46)
| p4(X46)
| ~ r1(X0,X46) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X45] :
( sP14(X45)
& sP15(X45)
& ~ p1(X45)
& r1(X0,X45) )
| ! [X42] :
( ! [X43] :
( ! [X44] : ~ r1(X43,X44)
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43)
| ~ r1(X42,X43) )
| p1(X42)
| p2(X42)
| p3(X42)
| p4(X42)
| ~ r1(X0,X42) )
| p1(X0) )
& ( ? [X41] :
( sP18(X41)
& sP19(X41)
& ~ p1(X41)
& ~ p2(X41)
& r1(X0,X41) )
| ! [X38] :
( ! [X39] :
( ! [X40] : ~ r1(X39,X40)
| p1(X39)
| p2(X39)
| p3(X39)
| p4(X39)
| ~ r1(X38,X39) )
| p1(X38)
| p2(X38)
| p3(X38)
| p4(X38)
| ~ r1(X0,X38) )
| p1(X0)
| p2(X0) )
& ( ? [X37] :
( sP24(X37)
& sP23(X37)
& ~ p1(X37)
& ~ p2(X37)
& ~ p3(X37)
& r1(X0,X37) )
| ! [X34] :
( ! [X35] :
( ! [X36] : ~ r1(X35,X36)
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X34,X35) )
| p1(X34)
| p2(X34)
| p3(X34)
| p4(X34)
| ~ r1(X0,X34) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X33] :
( sP29(X33)
& sP28(X33)
& ~ p1(X33)
& ~ p2(X33)
& ~ p3(X33)
& ~ p4(X33)
& r1(X0,X33) )
| ! [X30] :
( ! [X31] :
( ! [X32] : ~ r1(X31,X32)
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(X30,X31) )
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(X0,X30) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X29] :
( sP34(X29)
& sP35(X29)
& ~ p1(X29)
& r1(X0,X29) )
| ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] : ~ r1(X27,X28)
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(X26,X27) )
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(X25,X26) )
| p1(X25)
| p2(X25)
| p3(X25)
| p4(X25)
| ~ r1(X0,X25) )
| p1(X0) )
& ( ? [X24] :
( sP40(X24)
& sP41(X24)
& ~ p1(X24)
& ~ p2(X24)
& r1(X0,X24) )
| ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] : ~ r1(X22,X23)
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X21,X22) )
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21) )
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(X0,X20) )
| p1(X0)
| p2(X0) )
& ( ? [X14] :
( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP43(X17)
| sP44(X17)
| ~ r1(X14,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
& ~ p2(X14) )
| sP45(X14) )
& r1(X0,X14) )
| sP47(X0) )
& ! [X11] :
( ? [X12] :
( p1(X12)
& ? [X13] :
( ~ p1(X13)
& r1(X12,X13) )
& r1(X11,X12) )
| p1(X11)
| ~ r1(X0,X11) )
& ? [X10] :
( ~ p1(X10)
& r1(X0,X10) )
& ( sP48(X0)
| ! [X8] :
( ? [X9] :
( p5(X9)
& r1(X8,X9) )
| ~ r1(X0,X8) ) )
& ! [X5] :
( ? [X6] :
( p3(X6)
& ? [X7] :
( ~ p3(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p3(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p3(X4)
& r1(X0,X4) )
& ( sP49(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p5(X3)
| ~ r1(X2,X3) )
& r1(X1,X2) )
& ~ p1(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f62]) ).
fof(f210,plain,
( ! [X78] :
( ( ! [X80] :
( ~ p2(X80)
| ! [X81] :
( p2(X81)
| ~ r1(X80,X81) )
| ~ r1(sK163(X78),X80) )
& ~ p2(sK163(X78))
& r1(X78,sK163(X78)) )
| p2(X78)
| ~ r1(sK132,X78) )
& ( ( ! [X74] :
( ( r1(X74,sK162(X74))
& ~ p1(X74) )
| ! [X75] :
( ! [X76] : ~ r1(X75,X76)
| p1(X75)
| ~ r1(X74,X75) )
| ~ r1(sK160,X74) )
& r1(sK160,sK161)
& ~ p1(sK160)
& r1(sK132,sK160) )
| ! [X71] : ~ r1(sK132,X71)
| p1(sK132) )
& ( ( ! [X67] :
( ( r1(X67,sK159(X67))
& ~ p1(X67)
& ~ p2(X67) )
| ! [X68] :
( ! [X69] : ~ r1(X68,X69)
| p1(X68)
| p2(X68)
| ~ r1(X67,X68) )
| ~ r1(sK157,X67) )
& r1(sK157,sK158)
& ~ p1(sK157)
& ~ p2(sK157)
& r1(sK132,sK157) )
| ! [X64] : ~ r1(sK132,X64)
| p1(sK132)
| p2(sK132) )
& ( ( sP0(sK155)
& r1(sK155,sK156)
& ~ p1(sK155)
& ~ p2(sK155)
& ~ p3(sK155)
& r1(sK132,sK155) )
| ! [X61] : ~ r1(sK132,X61)
| p1(sK132)
| p2(sK132)
| p3(sK132) )
& ( ( sP1(sK153)
& r1(sK153,sK154)
& ~ p1(sK153)
& ~ p2(sK153)
& ~ p3(sK153)
& ~ p4(sK153)
& r1(sK132,sK153) )
| ! [X58] : ~ r1(sK132,X58)
| p1(sK132)
| p2(sK132)
| p3(sK132)
| p4(sK132) )
& ( ( sP2(sK152)
& sP3(sK152)
& ~ p1(sK152)
& r1(sK132,sK152) )
| ! [X55] :
( ! [X56] : ~ r1(X55,X56)
| p1(X55)
| p2(X55)
| p3(X55)
| p4(X55)
| ~ r1(sK132,X55) )
| p1(sK132) )
& ( ( sP4(sK151)
& sP5(sK151)
& ~ p1(sK151)
& ~ p2(sK151)
& r1(sK132,sK151) )
| ! [X52] :
( ! [X53] : ~ r1(X52,X53)
| p1(X52)
| p2(X52)
| p3(X52)
| p4(X52)
| ~ r1(sK132,X52) )
| p1(sK132)
| p2(sK132) )
& ( ( sP8(sK150)
& sP7(sK150)
& ~ p1(sK150)
& ~ p2(sK150)
& ~ p3(sK150)
& r1(sK132,sK150) )
| ! [X49] :
( ! [X50] : ~ r1(X49,X50)
| p1(X49)
| p2(X49)
| p3(X49)
| p4(X49)
| ~ r1(sK132,X49) )
| p1(sK132)
| p2(sK132)
| p3(sK132) )
& ( ( sP11(sK149)
& sP10(sK149)
& ~ p1(sK149)
& ~ p2(sK149)
& ~ p3(sK149)
& ~ p4(sK149)
& r1(sK132,sK149) )
| ! [X46] :
( ! [X47] : ~ r1(X46,X47)
| p1(X46)
| p2(X46)
| p3(X46)
| p4(X46)
| ~ r1(sK132,X46) )
| p1(sK132)
| p2(sK132)
| p3(sK132)
| p4(sK132) )
& ( ( sP14(sK148)
& sP15(sK148)
& ~ p1(sK148)
& r1(sK132,sK148) )
| ! [X42] :
( ! [X43] :
( ! [X44] : ~ r1(X43,X44)
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43)
| ~ r1(X42,X43) )
| p1(X42)
| p2(X42)
| p3(X42)
| p4(X42)
| ~ r1(sK132,X42) )
| p1(sK132) )
& ( ( sP18(sK147)
& sP19(sK147)
& ~ p1(sK147)
& ~ p2(sK147)
& r1(sK132,sK147) )
| ! [X38] :
( ! [X39] :
( ! [X40] : ~ r1(X39,X40)
| p1(X39)
| p2(X39)
| p3(X39)
| p4(X39)
| ~ r1(X38,X39) )
| p1(X38)
| p2(X38)
| p3(X38)
| p4(X38)
| ~ r1(sK132,X38) )
| p1(sK132)
| p2(sK132) )
& ( ( sP24(sK146)
& sP23(sK146)
& ~ p1(sK146)
& ~ p2(sK146)
& ~ p3(sK146)
& r1(sK132,sK146) )
| ! [X34] :
( ! [X35] :
( ! [X36] : ~ r1(X35,X36)
| p1(X35)
| p2(X35)
| p3(X35)
| p4(X35)
| ~ r1(X34,X35) )
| p1(X34)
| p2(X34)
| p3(X34)
| p4(X34)
| ~ r1(sK132,X34) )
| p1(sK132)
| p2(sK132)
| p3(sK132) )
& ( ( sP29(sK145)
& sP28(sK145)
& ~ p1(sK145)
& ~ p2(sK145)
& ~ p3(sK145)
& ~ p4(sK145)
& r1(sK132,sK145) )
| ! [X30] :
( ! [X31] :
( ! [X32] : ~ r1(X31,X32)
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(X30,X31) )
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(sK132,X30) )
| p1(sK132)
| p2(sK132)
| p3(sK132)
| p4(sK132) )
& ( ( sP34(sK144)
& sP35(sK144)
& ~ p1(sK144)
& r1(sK132,sK144) )
| ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] : ~ r1(X27,X28)
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(X26,X27) )
| p1(X26)
| p2(X26)
| p3(X26)
| p4(X26)
| ~ r1(X25,X26) )
| p1(X25)
| p2(X25)
| p3(X25)
| p4(X25)
| ~ r1(sK132,X25) )
| p1(sK132) )
& ( ( sP40(sK143)
& sP41(sK143)
& ~ p1(sK143)
& ~ p2(sK143)
& r1(sK132,sK143) )
| ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] : ~ r1(X22,X23)
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X21,X22) )
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21) )
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(sK132,X20) )
| p1(sK132)
| p2(sK132) )
& ( ( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP43(X17)
| sP44(X17)
| ~ r1(sK142,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(sK142,X15) )
& ~ p2(sK142) )
| sP45(sK142) )
& r1(sK132,sK142) )
| sP47(sK132) )
& ! [X11] :
( ( p1(sK140(X11))
& ~ p1(sK141(X11))
& r1(sK140(X11),sK141(X11))
& r1(X11,sK140(X11)) )
| p1(X11)
| ~ r1(sK132,X11) )
& ~ p1(sK139)
& r1(sK132,sK139)
& ( sP48(sK132)
| ! [X8] :
( ( p5(sK138(X8))
& r1(X8,sK138(X8)) )
| ~ r1(sK132,X8) ) )
& ! [X5] :
( ( p3(sK136(X5))
& ~ p3(sK137(X5))
& r1(sK136(X5),sK137(X5))
& r1(X5,sK136(X5)) )
| p3(X5)
| ~ r1(sK132,X5) )
& ~ p3(sK135)
& r1(sK132,sK135)
& ( sP49(sK132)
| ( ! [X3] :
( ~ p5(X3)
| ~ r1(sK134,X3) )
& r1(sK133,sK134)
& ~ p1(sK133)
& r1(sK132,sK133) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[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,sK161,sK162,sK163]),skolemize(X0,sK132),skolemize(X1,sK133),skolemize(X2,sK134),skolemize(X4,sK135),skolemize(X6,sK136(X5)),skolemize(X7,sK137(X5)),skolemize(X9,sK138(X8)),skolemize(X10,sK139),skolemize(X12,sK140(X11)),skolemize(X13,sK141(X11)),skolemize(X14,sK142),skolemize(X24,sK143),skolemize(X29,sK144),skolemize(X33,sK145),skolemize(X37,sK146),skolemize(X41,sK147),skolemize(X45,sK148),skolemize(X48,sK149),skolemize(X51,sK150),skolemize(X54,sK151),skolemize(X57,sK152),skolemize(X59,sK153),skolemize(X60,sK154),skolemize(X62,sK155),skolemize(X63,sK156),skolemize(X65,sK157),skolemize(X66,sK158),skolemize(X70,sK159(X67)),skolemize(X72,sK160),skolemize(X73,sK161),skolemize(X77,sK162(X74)),skolemize(X79,sK163(X78))],[f209]) ).
fof(f212,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f213,plain,
! [X2,X0] :
( ~ sP49(X0)
| p2(sK51(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f65]) ).
fof(f214,plain,
! [X2,X0] :
( ~ sP49(X0)
| ~ p2(sK52(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f65]) ).
fof(f215,plain,
! [X2,X0] :
( ~ sP49(X0)
| r1(sK51(X2),sK52(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f65]) ).
fof(f216,plain,
! [X2,X0] :
( ~ sP49(X0)
| r1(X2,sK51(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f65]) ).
fof(f217,plain,
! [X0] :
( ~ sP49(X0)
| ~ p2(sK50(X0)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f218,plain,
! [X0] :
( ~ sP49(X0)
| r1(X0,sK50(X0)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f219,plain,
! [X2,X0] :
( ~ sP48(X0)
| p2(sK54(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f220,plain,
! [X2,X0] :
( ~ sP48(X0)
| ~ p2(sK55(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f221,plain,
! [X2,X0] :
( ~ sP48(X0)
| r1(sK54(X2),sK55(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f222,plain,
! [X2,X0] :
( ~ sP48(X0)
| r1(X2,sK54(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f223,plain,
! [X0] :
( ~ sP48(X0)
| ~ p2(sK53(X0)) ),
inference(cnf_transformation,[],[f68]) ).
fof(f224,plain,
! [X0] :
( ~ sP48(X0)
| r1(X0,sK53(X0)) ),
inference(cnf_transformation,[],[f68]) ).
fof(f515,plain,
! [X80,X78,X81] :
( ~ p2(X80)
| p2(X81)
| ~ r1(X80,X81)
| ~ r1(sK163(X78),X80)
| p2(X78)
| ~ r1(sK132,X78) ),
inference(cnf_transformation,[],[f210]) ).
fof(f516,plain,
! [X78] :
( ~ p2(sK163(X78))
| p2(X78)
| ~ r1(sK132,X78) ),
inference(cnf_transformation,[],[f210]) ).
fof(f517,plain,
! [X78] :
( r1(X78,sK163(X78))
| p2(X78)
| ~ r1(sK132,X78) ),
inference(cnf_transformation,[],[f210]) ).
fof(f606,plain,
r1(sK132,sK139),
inference(cnf_transformation,[],[f210]) ).
fof(f607,plain,
! [X8] :
( sP48(sK132)
| p5(sK138(X8))
| ~ r1(sK132,X8) ),
inference(cnf_transformation,[],[f210]) ).
fof(f608,plain,
! [X8] :
( sP48(sK132)
| r1(X8,sK138(X8))
| ~ r1(sK132,X8) ),
inference(cnf_transformation,[],[f210]) ).
fof(f615,plain,
! [X3] :
( sP49(sK132)
| ~ p5(X3)
| ~ r1(sK134,X3) ),
inference(cnf_transformation,[],[f210]) ).
fof(f616,plain,
( sP49(sK132)
| r1(sK133,sK134) ),
inference(cnf_transformation,[],[f210]) ).
fof(f618,plain,
( sP49(sK132)
| r1(sK132,sK133) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_51,plain,
! [X0: $i] :
( r1(X0,sK50(X0))
| ~ sP49(X0) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( ~ sP49(X0)
| ~ p2(sK50(X0)) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK51(X1))
| ~ sP49(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK51(X1),sK52(X1))
| ~ sP49(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP49(X0)
| ~ p2(sK52(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK51(X1))
| ~ sP49(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_57,plain,
! [X0: $i] :
( r1(X0,sK53(X0))
| ~ sP48(X0) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_58,negated_conjecture,
! [X0: $i] :
( ~ sP48(X0)
| ~ p2(sK53(X0)) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK54(X1))
| ~ sP48(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK54(X1),sK55(X1))
| ~ sP48(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP48(X0)
| ~ p2(sK55(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK54(X1))
| ~ sP48(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_353,negated_conjecture,
( sP49(sK132)
| r1(sK132,sK133) ),
inference(cnf_transformation,[],[f618]) ).
tcf(c_355,negated_conjecture,
( sP49(sK132)
| r1(sK133,sK134) ),
inference(cnf_transformation,[],[f616]) ).
tcf(c_356,negated_conjecture,
! [X0: $i] :
( sP49(sK132)
| ~ p5(X0)
| ~ r1(sK134,X0) ),
inference(cnf_transformation,[],[f615]) ).
tcf(c_363,negated_conjecture,
! [X0: $i] :
( sP48(sK132)
| r1(X0,sK138(X0))
| ~ r1(sK132,X0) ),
inference(cnf_transformation,[],[f608]) ).
tcf(c_364,negated_conjecture,
! [X0: $i] :
( sP48(sK132)
| p5(sK138(X0))
| ~ r1(sK132,X0) ),
inference(cnf_transformation,[],[f607]) ).
tcf(c_365,negated_conjecture,
r1(sK132,sK139),
inference(cnf_transformation,[],[f606]) ).
tcf(c_454,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK163(X0))
| ~ r1(sK132,X0) ),
inference(cnf_transformation,[],[f517]) ).
tcf(c_455,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK163(X0))
| ~ r1(sK132,X0) ),
inference(cnf_transformation,[],[f516]) ).
tcf(c_456,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK132,X0)
| ~ r1(X1,X2)
| ~ r1(sK163(X0),X1) ),
inference(cnf_transformation,[],[f515]) ).
tcf(c_592,plain,
( ~ sP48(sK132)
| ~ p2(sK53(sK132)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_593,plain,
( ~ sP49(sK132)
| ~ p2(sK50(sK132)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_626,plain,
( r1(sK132,sK53(sK132))
| ~ sP48(sK132) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_627,plain,
( r1(sK132,sK50(sK132))
| ~ sP49(sK132) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_899,plain,
! [X0: $i] :
( p2(sK53(X0))
| r1(sK53(X0),sK163(sK53(X0)))
| ~ r1(sK132,sK53(X0)) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_900,plain,
( p2(sK53(sK132))
| r1(sK53(sK132),sK163(sK53(sK132)))
| ~ r1(sK132,sK53(sK132)) ),
inference(instantiation,[status(thm)],[c_899]) ).
tcf(c_926,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| p2(sK54(sK163(X1)))
| ~ sP48(X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_936,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| r1(sK163(X1),sK54(sK163(X1)))
| ~ sP48(X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_944,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| r1(sK54(sK163(X1)),sK55(sK163(X1)))
| ~ sP48(X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_991,plain,
( sP48(sK132)
| sP49(sK132)
| p5(sK138(sK133)) ),
inference(superposition,[status(thm)],[c_353,c_364]) ).
tcf(c_998,plain,
! [X0: $i,X1: $i] :
( r1(sK132,sK163(X1))
| ~ r1(sK132,X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_1025,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ r1(sK132,X0)
| ~ p2(sK54(sK163(X0)))
| ~ r1(sK54(sK163(X0)),X1)
| ~ r1(sK163(X0),sK54(sK163(X0))) ),
inference(instantiation,[status(thm)],[c_456]) ).
tcf(c_1100,plain,
( sP48(sK132)
| sP49(sK132)
| ~ p5(sK138(sK134))
| ~ r1(sK132,sK134) ),
inference(superposition,[status(thm)],[c_363,c_356]) ).
tcf(c_1117,plain,
! [X0: $i] :
( r1(sK132,sK163(sK53(X0)))
| ~ r1(sK132,sK53(X0))
| ~ r1(sK53(X0),sK163(sK53(X0))) ),
inference(instantiation,[status(thm)],[c_998]) ).
tcf(c_1118,plain,
( r1(sK132,sK163(sK53(sK132)))
| ~ r1(sK132,sK53(sK132))
| ~ r1(sK53(sK132),sK163(sK53(sK132))) ),
inference(instantiation,[status(thm)],[c_1117]) ).
tcf(c_1202,plain,
( p2(sK50(sK132))
| ~ sP49(sK132)
| ~ p2(sK163(sK50(sK132))) ),
inference(superposition,[status(thm)],[c_51,c_455]) ).
tcf(c_1203,plain,
( p2(sK53(sK132))
| ~ sP48(sK132)
| ~ p2(sK163(sK53(sK132))) ),
inference(superposition,[status(thm)],[c_57,c_455]) ).
tcf(c_1367,plain,
! [X0: $i] :
( p2(sK50(X0))
| r1(sK50(X0),sK163(sK50(X0)))
| ~ r1(sK132,sK50(X0)) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_1368,plain,
( p2(sK50(sK132))
| r1(sK50(sK132),sK163(sK50(sK132)))
| ~ r1(sK132,sK50(sK132)) ),
inference(instantiation,[status(thm)],[c_1367]) ).
tcf(c_1628,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| p2(sK51(sK163(X1)))
| ~ sP49(X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_2014,plain,
! [X0: $i] :
( sP49(sK132)
| r1(X0,sK134)
| ~ r1(X0,sK133) ),
inference(resolution,[status(thm)],[c_50,c_355]) ).
tcf(c_2015,plain,
( sP49(sK132)
| r1(sK132,sK134)
| ~ r1(sK132,sK133) ),
inference(instantiation,[status(thm)],[c_2014]) ).
tcf(c_2042,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| r1(sK163(X1),sK51(sK163(X1)))
| ~ sP49(X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_2091,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| ~ sP49(X0)
| ~ p2(sK52(sK163(X1)))
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_2101,plain,
! [X0: $i,X1: $i] :
( p2(sK163(X1))
| r1(sK51(sK163(X1)),sK52(sK163(X1)))
| ~ sP49(X0)
| ~ r1(X0,sK163(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_2228,plain,
! [X0: $i] :
( r1(sK132,sK163(sK50(X0)))
| ~ r1(sK132,sK50(X0))
| ~ r1(sK50(X0),sK163(sK50(X0))) ),
inference(instantiation,[status(thm)],[c_998]) ).
tcf(c_2231,plain,
( r1(sK132,sK163(sK50(sK132)))
| ~ r1(sK132,sK50(sK132))
| ~ r1(sK50(sK132),sK163(sK50(sK132))) ),
inference(instantiation,[status(thm)],[c_2228]) ).
tcf(c_2337,plain,
( sP48(sK132)
| sP49(sK132)
| p5(sK138(sK134))
| ~ r1(sK132,sK133) ),
inference(resolution,[status(thm)],[c_2014,c_364]) ).
tcf(c_2347,plain,
( sP48(sK132)
| sP49(sK132) ),
inference(global_subsumption_just,[status(thm)],[c_991,c_353,c_1100,c_2015,c_2337]) ).
tcf(c_3070,plain,
! [X0: $i] :
( p2(sK163(sK50(X0)))
| r1(sK51(sK163(sK50(X0))),sK52(sK163(sK50(X0))))
| ~ sP49(sK132)
| ~ r1(sK132,sK163(sK50(X0))) ),
inference(instantiation,[status(thm)],[c_2101]) ).
tcf(c_3071,plain,
! [X0: $i] :
( p2(sK163(sK50(X0)))
| r1(sK163(sK50(X0)),sK51(sK163(sK50(X0))))
| ~ sP49(sK132)
| ~ r1(sK132,sK163(sK50(X0))) ),
inference(instantiation,[status(thm)],[c_2042]) ).
tcf(c_3072,plain,
! [X0: $i] :
( p2(sK163(sK50(X0)))
| ~ sP49(sK132)
| ~ p2(sK52(sK163(sK50(X0))))
| ~ r1(sK132,sK163(sK50(X0))) ),
inference(instantiation,[status(thm)],[c_2091]) ).
tcf(c_3073,plain,
! [X0: $i] :
( p2(sK163(sK50(X0)))
| p2(sK51(sK163(sK50(X0))))
| ~ sP49(sK132)
| ~ r1(sK132,sK163(sK50(X0))) ),
inference(instantiation,[status(thm)],[c_1628]) ).
tcf(c_3086,plain,
( p2(sK163(sK50(sK132)))
| p2(sK51(sK163(sK50(sK132))))
| ~ sP49(sK132)
| ~ r1(sK132,sK163(sK50(sK132))) ),
inference(instantiation,[status(thm)],[c_3073]) ).
tcf(c_3087,plain,
( p2(sK163(sK50(sK132)))
| ~ sP49(sK132)
| ~ p2(sK52(sK163(sK50(sK132))))
| ~ r1(sK132,sK163(sK50(sK132))) ),
inference(instantiation,[status(thm)],[c_3072]) ).
tcf(c_3088,plain,
( p2(sK163(sK50(sK132)))
| r1(sK163(sK50(sK132)),sK51(sK163(sK50(sK132))))
| ~ sP49(sK132)
| ~ r1(sK132,sK163(sK50(sK132))) ),
inference(instantiation,[status(thm)],[c_3071]) ).
tcf(c_3089,plain,
( p2(sK163(sK50(sK132)))
| r1(sK51(sK163(sK50(sK132))),sK52(sK163(sK50(sK132))))
| ~ sP49(sK132)
| ~ r1(sK132,sK163(sK50(sK132))) ),
inference(instantiation,[status(thm)],[c_3070]) ).
tcf(c_4955,plain,
! [X0: $i] :
( p2(sK163(sK53(X0)))
| r1(sK54(sK163(sK53(X0))),sK55(sK163(sK53(X0))))
| ~ sP48(sK132)
| ~ r1(sK132,sK163(sK53(X0))) ),
inference(instantiation,[status(thm)],[c_944]) ).
tcf(c_4966,plain,
! [X0: $i] :
( p2(sK163(sK53(X0)))
| r1(sK163(sK53(X0)),sK54(sK163(sK53(X0))))
| ~ sP48(sK132)
| ~ r1(sK132,sK163(sK53(X0))) ),
inference(instantiation,[status(thm)],[c_936]) ).
tcf(c_4967,plain,
( p2(sK163(sK53(sK132)))
| r1(sK163(sK53(sK132)),sK54(sK163(sK53(sK132))))
| ~ sP48(sK132)
| ~ r1(sK132,sK163(sK53(sK132))) ),
inference(instantiation,[status(thm)],[c_4966]) ).
tcf(c_4976,plain,
( p2(sK163(sK53(sK132)))
| r1(sK54(sK163(sK53(sK132))),sK55(sK163(sK53(sK132))))
| ~ sP48(sK132)
| ~ r1(sK132,sK163(sK53(sK132))) ),
inference(instantiation,[status(thm)],[c_4955]) ).
tcf(c_7633,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK53(X0))
| ~ r1(sK132,sK53(X0))
| ~ p2(sK54(sK163(sK53(X0))))
| ~ r1(sK54(sK163(sK53(X0))),X1)
| ~ r1(sK163(sK53(X0)),sK54(sK163(sK53(X0)))) ),
inference(instantiation,[status(thm)],[c_1025]) ).
tcf(c_10829,plain,
! [X0: $i] :
( p2(sK53(X0))
| p2(sK55(sK163(sK53(X0))))
| ~ r1(sK132,sK53(X0))
| ~ p2(sK54(sK163(sK53(X0))))
| ~ r1(sK163(sK53(X0)),sK54(sK163(sK53(X0))))
| ~ r1(sK54(sK163(sK53(X0))),sK55(sK163(sK53(X0)))) ),
inference(instantiation,[status(thm)],[c_7633]) ).
tcf(c_10830,plain,
( p2(sK53(sK132))
| p2(sK55(sK163(sK53(sK132))))
| ~ r1(sK132,sK53(sK132))
| ~ p2(sK54(sK163(sK53(sK132))))
| ~ r1(sK163(sK53(sK132)),sK54(sK163(sK53(sK132))))
| ~ r1(sK54(sK163(sK53(sK132))),sK55(sK163(sK53(sK132)))) ),
inference(instantiation,[status(thm)],[c_10829]) ).
tcf(c_20732,plain,
! [X0: $i] :
( p2(sK163(sK53(X0)))
| p2(sK54(sK163(sK53(X0))))
| ~ sP48(sK132)
| ~ r1(sK132,sK163(sK53(X0))) ),
inference(instantiation,[status(thm)],[c_926]) ).
tcf(c_20733,plain,
( p2(sK163(sK53(sK132)))
| p2(sK54(sK163(sK53(sK132))))
| ~ sP48(sK132)
| ~ r1(sK132,sK163(sK53(sK132))) ),
inference(instantiation,[status(thm)],[c_20732]) ).
tcf(c_32443,plain,
! [X0: $i] :
( r1(sK132,X0)
| ~ r1(sK139,X0) ),
inference(superposition,[status(thm)],[c_365,c_50]) ).
tcf(c_32677,plain,
( p2(sK139)
| r1(sK139,sK54(sK139))
| ~ sP48(sK132) ),
inference(superposition,[status(thm)],[c_365,c_59]) ).
tcf(c_33277,plain,
( p2(sK139)
| r1(sK132,sK54(sK139))
| ~ sP48(sK132) ),
inference(superposition,[status(thm)],[c_32677,c_32443]) ).
tcf(c_35700,plain,
! [X0: $i,X1: $i] :
( p2(sK163(sK53(X1)))
| ~ sP48(X0)
| ~ p2(sK55(sK163(sK53(X1))))
| ~ r1(X0,sK163(sK53(X1))) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_35701,plain,
( p2(sK163(sK53(sK132)))
| ~ sP48(sK132)
| ~ p2(sK55(sK163(sK53(sK132))))
| ~ r1(sK132,sK163(sK53(sK132))) ),
inference(instantiation,[status(thm)],[c_35700]) ).
tcf(c_36549,plain,
~ sP48(sK132),
inference(global_subsumption_just,[status(thm)],[c_33277,c_592,c_626,c_900,c_1118,c_1203,c_4967,c_4976,c_10830,c_20733,c_35701]) ).
tcf(c_41835,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK52(sK163(X1)))
| ~ p2(X0)
| ~ r1(sK132,X2)
| ~ r1(sK163(X2),X0)
| ~ r1(X0,sK52(sK163(X1))) ),
inference(instantiation,[status(thm)],[c_456]) ).
tcf(c_42419,plain,
! [X0: $i,X1: $i] :
( p2(X0)
| p2(sK52(sK163(X1)))
| ~ r1(sK132,X0)
| ~ p2(sK51(sK163(X0)))
| ~ r1(sK163(X0),sK51(sK163(X0)))
| ~ r1(sK51(sK163(X0)),sK52(sK163(X1))) ),
inference(instantiation,[status(thm)],[c_41835]) ).
tcf(c_43199,plain,
! [X0: $i,X1: $i] :
( p2(sK50(X0))
| p2(sK52(sK163(X1)))
| ~ r1(sK132,sK50(X0))
| ~ p2(sK51(sK163(sK50(X0))))
| ~ r1(sK163(sK50(X0)),sK51(sK163(sK50(X0))))
| ~ r1(sK51(sK163(sK50(X0))),sK52(sK163(X1))) ),
inference(instantiation,[status(thm)],[c_42419]) ).
tcf(c_43695,plain,
! [X0: $i] :
( p2(sK50(X0))
| p2(sK52(sK163(sK50(X0))))
| ~ r1(sK132,sK50(X0))
| ~ p2(sK51(sK163(sK50(X0))))
| ~ r1(sK163(sK50(X0)),sK51(sK163(sK50(X0))))
| ~ r1(sK51(sK163(sK50(X0))),sK52(sK163(sK50(X0)))) ),
inference(instantiation,[status(thm)],[c_43199]) ).
tcf(c_43697,plain,
( p2(sK50(sK132))
| p2(sK52(sK163(sK50(sK132))))
| ~ r1(sK132,sK50(sK132))
| ~ p2(sK51(sK163(sK50(sK132))))
| ~ r1(sK163(sK50(sK132)),sK51(sK163(sK50(sK132))))
| ~ r1(sK51(sK163(sK50(sK132))),sK52(sK163(sK50(sK132)))) ),
inference(instantiation,[status(thm)],[c_43695]) ).
tcf(c_43698,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_43697,c_36549,c_3089,c_3088,c_3087,c_3086,c_2347,c_2231,c_1368,c_1202,c_627,c_593]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL676+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n013.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 00:13:26 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.41
% 0.11/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.41
% 0.11/0.41 % Detected problem language: tptp
% 0.11/0.42 % Proving...
% 22.32/5.22 % SZS status Started for theBenchmark.p
% 22.32/5.22 % SZS status Theorem for theBenchmark.p
% 22.32/5.22
% 22.32/5.22 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 22.32/5.22
% 22.32/5.22 % ------ iProver source info
% 22.32/5.22
% 22.32/5.22 % git: date: 2026-07-19 20:42:38 +0200
% 22.32/5.22 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 22.32/5.22 % git: non_committed_changes: false
% 22.32/5.22
% 22.32/5.22 % ------ Parsing...
% 22.32/5.22 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 22.32/5.22
% 22.32/5.22 % ------ Preprocessing... sf_s rm: 327 0s sf_e sf_s rm: 0 0s sf_e %
% 22.32/5.22
% 22.32/5.22 % ------ Preprocessing...
% 22.32/5.22 % ------ Proving...
% 22.32/5.22 % ------ Problem Properties
% 22.32/5.22
% 22.32/5.22 %
% 22.32/5.22 % clauses 81
% 22.32/5.22 % conjectures 33
% 22.32/5.22 % EPR 20
% 22.32/5.22 % Horn 33
% 22.32/5.22 % unary 5
% 22.32/5.22 % binary 16
% 22.32/5.22 % lits 280
% 22.32/5.22 % lits eq 0
% 22.32/5.22 % fd_pure 0
% 22.32/5.22 % fd_pseudo 0
% 22.32/5.22 % fd_cond 0
% 22.32/5.22 % fd_pseudo_cond 0
% 22.32/5.22 % AC symbols 0
% 22.32/5.22
% 22.32/5.22 % ------ Input Options Time Limit: Unbounded
% 22.32/5.22
% 22.32/5.22
% 22.32/5.22 % ------
% 22.32/5.22 % Current options:
% 22.32/5.22 % ------
% 22.32/5.22
% 22.32/5.22
% 22.32/5.22 %
% 22.32/5.22
% 22.32/5.22 % ------ Proving...
% 22.32/5.22 %
% 22.32/5.22
% 22.32/5.22 % SZS status Theorem for theBenchmark.p
% 22.32/5.22
% 22.32/5.22 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 22.32/5.23
% 22.32/5.23
%------------------------------------------------------------------------------