%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL644+1.020 : 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 : n015.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:03 PM UTC 2026
% Result : Theorem 3.25s 1.43s
% Output : CNFRefutation 3.25s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f107ERROR: Could not build tree for root c_697ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f408,plain,
? [X0] :
( ( sP2(X0)
| sP4(X0)
| sP3(X0)
| ! [X83] :
( ~ p1(X83)
| ? [X84] :
( ~ p1(X84)
& r1(X83,X84) )
| ~ p1(X83)
| p2(X83)
| ~ r1(X0,X83) )
| ! [X81] :
( p1(X81)
| ? [X82] :
( ~ p2(X82)
& r1(X81,X82) )
| ~ p2(X81)
| ~ r1(X0,X81) ) )
& ( sP7(X0)
| sP9(X0)
| sP8(X0)
| ! [X79] :
( ~ p2(X79)
| ? [X80] :
( ~ p2(X80)
& r1(X79,X80) )
| ~ p2(X79)
| p3(X79)
| ~ r1(X0,X79) )
| ! [X77] :
( p2(X77)
| ? [X78] :
( ~ p3(X78)
& r1(X77,X78) )
| ~ p3(X77)
| ~ r1(X0,X77) ) )
& ( sP12(X0)
| sP14(X0)
| sP13(X0)
| ! [X75] :
( ~ p3(X75)
| ? [X76] :
( ~ p3(X76)
& r1(X75,X76) )
| ~ p3(X75)
| p4(X75)
| ~ r1(X0,X75) )
| ! [X73] :
( p3(X73)
| ? [X74] :
( ~ p4(X74)
& r1(X73,X74) )
| ~ p4(X73)
| ~ r1(X0,X73) ) )
& ( sP17(X0)
| sP19(X0)
| sP18(X0)
| ! [X71] :
( ~ p4(X71)
| ? [X72] :
( ~ p4(X72)
& r1(X71,X72) )
| ~ p4(X71)
| p5(X71)
| ~ r1(X0,X71) )
| ! [X69] :
( p4(X69)
| ? [X70] :
( ~ p5(X70)
& r1(X69,X70) )
| ~ p5(X69)
| ~ r1(X0,X69) ) )
& ( sP22(X0)
| sP24(X0)
| sP23(X0)
| ! [X67] :
( ~ p5(X67)
| ? [X68] :
( ~ p5(X68)
& r1(X67,X68) )
| ~ p5(X67)
| p6(X67)
| ~ r1(X0,X67) )
| ! [X65] :
( p5(X65)
| ? [X66] :
( ~ p6(X66)
& r1(X65,X66) )
| ~ p6(X65)
| ~ r1(X0,X65) ) )
& ( sP27(X0)
| sP29(X0)
| sP28(X0)
| ! [X63] :
( ~ p6(X63)
| ? [X64] :
( ~ p6(X64)
& r1(X63,X64) )
| ~ p6(X63)
| p7(X63)
| ~ r1(X0,X63) )
| ! [X61] :
( p6(X61)
| ? [X62] :
( ~ p7(X62)
& r1(X61,X62) )
| ~ p7(X61)
| ~ r1(X0,X61) ) )
& ? [X59] :
( p20(X59)
& ! [X60] :
( p20(X60)
| ~ r1(X59,X60) )
& ~ p20(X59)
& r1(X0,X59) )
& ? [X57] :
( p20(X57)
& ! [X58] :
( p20(X58)
| ~ r1(X57,X58) )
& ~ p20(X57)
& r1(X0,X57) )
& ( sP32(X0)
| sP34(X0)
| sP33(X0)
| ! [X55] :
( ~ p7(X55)
| ? [X56] :
( ~ p7(X56)
& r1(X55,X56) )
| ~ p7(X55)
| p8(X55)
| ~ r1(X0,X55) )
| ! [X53] :
( p7(X53)
| ? [X54] :
( ~ p8(X54)
& r1(X53,X54) )
| ~ p8(X53)
| ~ r1(X0,X53) ) )
& ( sP37(X0)
| sP39(X0)
| sP38(X0)
| ! [X51] :
( ~ p8(X51)
| ? [X52] :
( ~ p8(X52)
& r1(X51,X52) )
| ~ p8(X51)
| p9(X51)
| ~ r1(X0,X51) )
| ! [X49] :
( p8(X49)
| ? [X50] :
( ~ p9(X50)
& r1(X49,X50) )
| ~ p9(X49)
| ~ r1(X0,X49) ) )
& ( sP42(X0)
| sP44(X0)
| sP43(X0)
| ! [X47] :
( ~ p9(X47)
| ? [X48] :
( ~ p9(X48)
& r1(X47,X48) )
| ~ p9(X47)
| p10(X47)
| ~ r1(X0,X47) )
| ! [X45] :
( p9(X45)
| ? [X46] :
( ~ p10(X46)
& r1(X45,X46) )
| ~ p10(X45)
| ~ r1(X0,X45) ) )
& ( sP47(X0)
| sP49(X0)
| sP48(X0)
| ! [X43] :
( ~ p10(X43)
| ? [X44] :
( ~ p10(X44)
& r1(X43,X44) )
| ~ p10(X43)
| p11(X43)
| ~ r1(X0,X43) )
| ! [X41] :
( p10(X41)
| ? [X42] :
( ~ p11(X42)
& r1(X41,X42) )
| ~ p11(X41)
| ~ r1(X0,X41) ) )
& ( sP52(X0)
| sP54(X0)
| sP53(X0)
| ! [X39] :
( ~ p11(X39)
| ? [X40] :
( ~ p11(X40)
& r1(X39,X40) )
| ~ p11(X39)
| p12(X39)
| ~ r1(X0,X39) )
| ! [X37] :
( p11(X37)
| ? [X38] :
( ~ p12(X38)
& r1(X37,X38) )
| ~ p12(X37)
| ~ r1(X0,X37) ) )
& ( sP57(X0)
| sP59(X0)
| sP58(X0)
| ! [X35] :
( ~ p12(X35)
| ? [X36] :
( ~ p12(X36)
& r1(X35,X36) )
| ~ p12(X35)
| p13(X35)
| ~ r1(X0,X35) )
| ! [X33] :
( p12(X33)
| ? [X34] :
( ~ p13(X34)
& r1(X33,X34) )
| ~ p13(X33)
| ~ r1(X0,X33) ) )
& ( sP62(X0)
| sP64(X0)
| sP63(X0)
| ! [X31] :
( ~ p13(X31)
| ? [X32] :
( ~ p13(X32)
& r1(X31,X32) )
| ~ p13(X31)
| p14(X31)
| ~ r1(X0,X31) )
| ! [X29] :
( p13(X29)
| ? [X30] :
( ~ p14(X30)
& r1(X29,X30) )
| ~ p14(X29)
| ~ r1(X0,X29) ) )
& ( sP67(X0)
| sP69(X0)
| sP68(X0)
| ! [X27] :
( ~ p14(X27)
| ? [X28] :
( ~ p14(X28)
& r1(X27,X28) )
| ~ p14(X27)
| p15(X27)
| ~ r1(X0,X27) )
| ! [X25] :
( p14(X25)
| ? [X26] :
( ~ p15(X26)
& r1(X25,X26) )
| ~ p15(X25)
| ~ r1(X0,X25) ) )
& ( sP72(X0)
| sP74(X0)
| sP73(X0)
| ! [X23] :
( ~ p15(X23)
| ? [X24] :
( ~ p15(X24)
& r1(X23,X24) )
| ~ p15(X23)
| p16(X23)
| ~ r1(X0,X23) )
| ! [X21] :
( p15(X21)
| ? [X22] :
( ~ p16(X22)
& r1(X21,X22) )
| ~ p16(X21)
| ~ r1(X0,X21) ) )
& ( sP77(X0)
| sP79(X0)
| sP78(X0)
| ! [X19] :
( ~ p16(X19)
| ? [X20] :
( ~ p16(X20)
& r1(X19,X20) )
| ~ p16(X19)
| p17(X19)
| ~ r1(X0,X19) )
| ! [X17] :
( p16(X17)
| ? [X18] :
( ~ p17(X18)
& r1(X17,X18) )
| ~ p17(X17)
| ~ r1(X0,X17) ) )
& ( sP82(X0)
| sP84(X0)
| sP83(X0)
| ! [X15] :
( ~ p17(X15)
| ? [X16] :
( ~ p17(X16)
& r1(X15,X16) )
| ~ p17(X15)
| p18(X15)
| ~ r1(X0,X15) )
| ! [X13] :
( p17(X13)
| ? [X14] :
( ~ p18(X14)
& r1(X13,X14) )
| ~ p18(X13)
| ~ r1(X0,X13) ) )
& ( sP87(X0)
| sP89(X0)
| sP88(X0)
| ! [X11] :
( ~ p18(X11)
| ? [X12] :
( ~ p18(X12)
& r1(X11,X12) )
| ~ p18(X11)
| p19(X11)
| ~ r1(X0,X11) )
| ! [X9] :
( p18(X9)
| ? [X10] :
( ~ p19(X10)
& r1(X9,X10) )
| ~ p19(X9)
| ~ r1(X0,X9) ) )
& ( sP92(X0)
| sP94(X0)
| sP93(X0)
| ! [X7] :
( ~ p19(X7)
| ? [X8] :
( ~ p19(X8)
& r1(X7,X8) )
| ~ p19(X7)
| p20(X7)
| ~ r1(X0,X7) )
| ! [X5] :
( p19(X5)
| ? [X6] :
( ~ p20(X6)
& r1(X5,X6) )
| ~ p20(X5)
| ~ r1(X0,X5) ) )
& ( sP97(X0)
| sP99(X0)
| sP98(X0)
| ! [X3] :
( ~ p20(X3)
| ? [X4] :
( ~ p20(X4)
& r1(X3,X4) )
| ~ p20(X3)
| p21(X3)
| ~ r1(X0,X3) )
| ! [X1] :
( p20(X1)
| ? [X2] :
( ~ p21(X2)
& r1(X1,X2) )
| ~ p21(X1)
| ~ r1(X0,X1) ) ) ),
inference(rectify,[],[f107]) ).
fof(f409,plain,
( ( sP2(sK200)
| sP4(sK200)
| sP3(sK200)
| ! [X83] :
( ~ p1(X83)
| ( ~ p1(sK242(X83))
& r1(X83,sK242(X83)) )
| ~ p1(X83)
| p2(X83)
| ~ r1(sK200,X83) )
| ! [X81] :
( p1(X81)
| ( ~ p2(sK241(X81))
& r1(X81,sK241(X81)) )
| ~ p2(X81)
| ~ r1(sK200,X81) ) )
& ( sP7(sK200)
| sP9(sK200)
| sP8(sK200)
| ! [X79] :
( ~ p2(X79)
| ( ~ p2(sK240(X79))
& r1(X79,sK240(X79)) )
| ~ p2(X79)
| p3(X79)
| ~ r1(sK200,X79) )
| ! [X77] :
( p2(X77)
| ( ~ p3(sK239(X77))
& r1(X77,sK239(X77)) )
| ~ p3(X77)
| ~ r1(sK200,X77) ) )
& ( sP12(sK200)
| sP14(sK200)
| sP13(sK200)
| ! [X75] :
( ~ p3(X75)
| ( ~ p3(sK238(X75))
& r1(X75,sK238(X75)) )
| ~ p3(X75)
| p4(X75)
| ~ r1(sK200,X75) )
| ! [X73] :
( p3(X73)
| ( ~ p4(sK237(X73))
& r1(X73,sK237(X73)) )
| ~ p4(X73)
| ~ r1(sK200,X73) ) )
& ( sP17(sK200)
| sP19(sK200)
| sP18(sK200)
| ! [X71] :
( ~ p4(X71)
| ( ~ p4(sK236(X71))
& r1(X71,sK236(X71)) )
| ~ p4(X71)
| p5(X71)
| ~ r1(sK200,X71) )
| ! [X69] :
( p4(X69)
| ( ~ p5(sK235(X69))
& r1(X69,sK235(X69)) )
| ~ p5(X69)
| ~ r1(sK200,X69) ) )
& ( sP22(sK200)
| sP24(sK200)
| sP23(sK200)
| ! [X67] :
( ~ p5(X67)
| ( ~ p5(sK234(X67))
& r1(X67,sK234(X67)) )
| ~ p5(X67)
| p6(X67)
| ~ r1(sK200,X67) )
| ! [X65] :
( p5(X65)
| ( ~ p6(sK233(X65))
& r1(X65,sK233(X65)) )
| ~ p6(X65)
| ~ r1(sK200,X65) ) )
& ( sP27(sK200)
| sP29(sK200)
| sP28(sK200)
| ! [X63] :
( ~ p6(X63)
| ( ~ p6(sK232(X63))
& r1(X63,sK232(X63)) )
| ~ p6(X63)
| p7(X63)
| ~ r1(sK200,X63) )
| ! [X61] :
( p6(X61)
| ( ~ p7(sK231(X61))
& r1(X61,sK231(X61)) )
| ~ p7(X61)
| ~ r1(sK200,X61) ) )
& p20(sK230)
& ! [X60] :
( p20(X60)
| ~ r1(sK230,X60) )
& ~ p20(sK230)
& r1(sK200,sK230)
& p20(sK229)
& ! [X58] :
( p20(X58)
| ~ r1(sK229,X58) )
& ~ p20(sK229)
& r1(sK200,sK229)
& ( sP32(sK200)
| sP34(sK200)
| sP33(sK200)
| ! [X55] :
( ~ p7(X55)
| ( ~ p7(sK228(X55))
& r1(X55,sK228(X55)) )
| ~ p7(X55)
| p8(X55)
| ~ r1(sK200,X55) )
| ! [X53] :
( p7(X53)
| ( ~ p8(sK227(X53))
& r1(X53,sK227(X53)) )
| ~ p8(X53)
| ~ r1(sK200,X53) ) )
& ( sP37(sK200)
| sP39(sK200)
| sP38(sK200)
| ! [X51] :
( ~ p8(X51)
| ( ~ p8(sK226(X51))
& r1(X51,sK226(X51)) )
| ~ p8(X51)
| p9(X51)
| ~ r1(sK200,X51) )
| ! [X49] :
( p8(X49)
| ( ~ p9(sK225(X49))
& r1(X49,sK225(X49)) )
| ~ p9(X49)
| ~ r1(sK200,X49) ) )
& ( sP42(sK200)
| sP44(sK200)
| sP43(sK200)
| ! [X47] :
( ~ p9(X47)
| ( ~ p9(sK224(X47))
& r1(X47,sK224(X47)) )
| ~ p9(X47)
| p10(X47)
| ~ r1(sK200,X47) )
| ! [X45] :
( p9(X45)
| ( ~ p10(sK223(X45))
& r1(X45,sK223(X45)) )
| ~ p10(X45)
| ~ r1(sK200,X45) ) )
& ( sP47(sK200)
| sP49(sK200)
| sP48(sK200)
| ! [X43] :
( ~ p10(X43)
| ( ~ p10(sK222(X43))
& r1(X43,sK222(X43)) )
| ~ p10(X43)
| p11(X43)
| ~ r1(sK200,X43) )
| ! [X41] :
( p10(X41)
| ( ~ p11(sK221(X41))
& r1(X41,sK221(X41)) )
| ~ p11(X41)
| ~ r1(sK200,X41) ) )
& ( sP52(sK200)
| sP54(sK200)
| sP53(sK200)
| ! [X39] :
( ~ p11(X39)
| ( ~ p11(sK220(X39))
& r1(X39,sK220(X39)) )
| ~ p11(X39)
| p12(X39)
| ~ r1(sK200,X39) )
| ! [X37] :
( p11(X37)
| ( ~ p12(sK219(X37))
& r1(X37,sK219(X37)) )
| ~ p12(X37)
| ~ r1(sK200,X37) ) )
& ( sP57(sK200)
| sP59(sK200)
| sP58(sK200)
| ! [X35] :
( ~ p12(X35)
| ( ~ p12(sK218(X35))
& r1(X35,sK218(X35)) )
| ~ p12(X35)
| p13(X35)
| ~ r1(sK200,X35) )
| ! [X33] :
( p12(X33)
| ( ~ p13(sK217(X33))
& r1(X33,sK217(X33)) )
| ~ p13(X33)
| ~ r1(sK200,X33) ) )
& ( sP62(sK200)
| sP64(sK200)
| sP63(sK200)
| ! [X31] :
( ~ p13(X31)
| ( ~ p13(sK216(X31))
& r1(X31,sK216(X31)) )
| ~ p13(X31)
| p14(X31)
| ~ r1(sK200,X31) )
| ! [X29] :
( p13(X29)
| ( ~ p14(sK215(X29))
& r1(X29,sK215(X29)) )
| ~ p14(X29)
| ~ r1(sK200,X29) ) )
& ( sP67(sK200)
| sP69(sK200)
| sP68(sK200)
| ! [X27] :
( ~ p14(X27)
| ( ~ p14(sK214(X27))
& r1(X27,sK214(X27)) )
| ~ p14(X27)
| p15(X27)
| ~ r1(sK200,X27) )
| ! [X25] :
( p14(X25)
| ( ~ p15(sK213(X25))
& r1(X25,sK213(X25)) )
| ~ p15(X25)
| ~ r1(sK200,X25) ) )
& ( sP72(sK200)
| sP74(sK200)
| sP73(sK200)
| ! [X23] :
( ~ p15(X23)
| ( ~ p15(sK212(X23))
& r1(X23,sK212(X23)) )
| ~ p15(X23)
| p16(X23)
| ~ r1(sK200,X23) )
| ! [X21] :
( p15(X21)
| ( ~ p16(sK211(X21))
& r1(X21,sK211(X21)) )
| ~ p16(X21)
| ~ r1(sK200,X21) ) )
& ( sP77(sK200)
| sP79(sK200)
| sP78(sK200)
| ! [X19] :
( ~ p16(X19)
| ( ~ p16(sK210(X19))
& r1(X19,sK210(X19)) )
| ~ p16(X19)
| p17(X19)
| ~ r1(sK200,X19) )
| ! [X17] :
( p16(X17)
| ( ~ p17(sK209(X17))
& r1(X17,sK209(X17)) )
| ~ p17(X17)
| ~ r1(sK200,X17) ) )
& ( sP82(sK200)
| sP84(sK200)
| sP83(sK200)
| ! [X15] :
( ~ p17(X15)
| ( ~ p17(sK208(X15))
& r1(X15,sK208(X15)) )
| ~ p17(X15)
| p18(X15)
| ~ r1(sK200,X15) )
| ! [X13] :
( p17(X13)
| ( ~ p18(sK207(X13))
& r1(X13,sK207(X13)) )
| ~ p18(X13)
| ~ r1(sK200,X13) ) )
& ( sP87(sK200)
| sP89(sK200)
| sP88(sK200)
| ! [X11] :
( ~ p18(X11)
| ( ~ p18(sK206(X11))
& r1(X11,sK206(X11)) )
| ~ p18(X11)
| p19(X11)
| ~ r1(sK200,X11) )
| ! [X9] :
( p18(X9)
| ( ~ p19(sK205(X9))
& r1(X9,sK205(X9)) )
| ~ p19(X9)
| ~ r1(sK200,X9) ) )
& ( sP92(sK200)
| sP94(sK200)
| sP93(sK200)
| ! [X7] :
( ~ p19(X7)
| ( ~ p19(sK204(X7))
& r1(X7,sK204(X7)) )
| ~ p19(X7)
| p20(X7)
| ~ r1(sK200,X7) )
| ! [X5] :
( p19(X5)
| ( ~ p20(sK203(X5))
& r1(X5,sK203(X5)) )
| ~ p20(X5)
| ~ r1(sK200,X5) ) )
& ( sP97(sK200)
| sP99(sK200)
| sP98(sK200)
| ! [X3] :
( ~ p20(X3)
| ( ~ p20(sK202(X3))
& r1(X3,sK202(X3)) )
| ~ p20(X3)
| p21(X3)
| ~ r1(sK200,X3) )
| ! [X1] :
( p20(X1)
| ( ~ p21(sK201(X1))
& r1(X1,sK201(X1)) )
| ~ p21(X1)
| ~ r1(sK200,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK200,sK201,sK202,sK203,sK204,sK205,sK206,sK207,sK208,sK209,sK210,sK211,sK212,sK213,sK214,sK215,sK216,sK217,sK218,sK219,sK220,sK221,sK222,sK223,sK224,sK225,sK226,sK227,sK228,sK229,sK230,sK231,sK232,sK233,sK234,sK235,sK236,sK237,sK238,sK239,sK240,sK241,sK242]),skolemize(X0,sK200),skolemize(X2,sK201(X1)),skolemize(X4,sK202(X3)),skolemize(X6,sK203(X5)),skolemize(X8,sK204(X7)),skolemize(X10,sK205(X9)),skolemize(X12,sK206(X11)),skolemize(X14,sK207(X13)),skolemize(X16,sK208(X15)),skolemize(X18,sK209(X17)),skolemize(X20,sK210(X19)),skolemize(X22,sK211(X21)),skolemize(X24,sK212(X23)),skolemize(X26,sK213(X25)),skolemize(X28,sK214(X27)),skolemize(X30,sK215(X29)),skolemize(X32,sK216(X31)),skolemize(X34,sK217(X33)),skolemize(X36,sK218(X35)),skolemize(X38,sK219(X37)),skolemize(X40,sK220(X39)),skolemize(X42,sK221(X41)),skolemize(X44,sK222(X43)),skolemize(X46,sK223(X45)),skolemize(X48,sK224(X47)),skolemize(X50,sK225(X49)),skolemize(X52,sK226(X51)),skolemize(X54,sK227(X53)),skolemize(X56,sK228(X55)),skolemize(X57,sK229),skolemize(X59,sK230),skolemize(X62,sK231(X61)),skolemize(X64,sK232(X63)),skolemize(X66,sK233(X65)),skolemize(X68,sK234(X67)),skolemize(X70,sK235(X69)),skolemize(X72,sK236(X71)),skolemize(X74,sK237(X73)),skolemize(X76,sK238(X75)),skolemize(X78,sK239(X77)),skolemize(X80,sK240(X79)),skolemize(X82,sK241(X81)),skolemize(X84,sK242(X83))],[f408]) ).
fof(f994,plain,
p20(sK230),
inference(cnf_transformation,[],[f409]) ).
fof(f996,plain,
~ p20(sK230),
inference(cnf_transformation,[],[f409]) ).
tcf(c_670,negated_conjecture,
~ p20(sK230),
inference(cnf_transformation,[],[f996]) ).
tcf(c_672,negated_conjecture,
p20(sK230),
inference(cnf_transformation,[],[f994]) ).
tcf(c_697,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_670,c_672]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL644+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n015.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 : Wed Sep 23 23:58:25 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.42 Running first-order theorem proving
% 0.14/0.42 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.14/0.43
% 0.14/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.43
% 0.14/0.44 % Detected problem language: tptp
% 0.14/0.45 % Proving...
% 3.25/1.43 % SZS status Started for theBenchmark.p
% 3.25/1.43 % SZS status Theorem for theBenchmark.p
% 3.25/1.43
% 3.25/1.43 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.25/1.43
% 3.25/1.43 % ------ iProver source info
% 3.25/1.43
% 3.25/1.43 % git: date: 2026-07-19 20:42:38 +0200
% 3.25/1.43 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.25/1.43 % git: non_committed_changes: false
% 3.25/1.43
% 3.25/1.43 % ------ Parsing...
% 3.25/1.43 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.25/1.43
% 3.25/1.43 % ------ Preprocessing...%
% 3.25/1.43
% 3.25/1.43 % SZS status Theorem for theBenchmark.p
% 3.25/1.43
% 3.25/1.43 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.25/1.43
% 3.25/1.43
%------------------------------------------------------------------------------