%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL676+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:08:04 PM UTC 2026
% Result : Theorem 49.01s 8.06s
% Output : CNFRefutation 49.01s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f21ERROR: Could not build tree for root c_24919ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X1,X2)
& r1(X0,X1) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox/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(f23,plain,
! [X0] :
( ~ sP9(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,[],[f21]) ).
fof(f24,plain,
! [X0] :
( ~ sP9(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,[],[f23]) ).
fof(f25,plain,
! [X0] :
( ~ sP9(X0)
| ( ! [X2] :
( ( p2(sK11(X2))
& ~ p2(sK12(X2))
& r1(sK11(X2),sK12(X2))
& r1(X2,sK11(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK10(X0))
& r1(X0,sK10(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X1,sK10(X0)),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f24]) ).
fof(f26,plain,
! [X0] :
( ~ sP8(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,[],[f20]) ).
fof(f27,plain,
! [X0] :
( ~ sP8(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,[],[f26]) ).
fof(f28,plain,
! [X0] :
( ~ sP8(X0)
| ( ! [X2] :
( ( p2(sK14(X2))
& ~ p2(sK15(X2))
& r1(sK14(X2),sK15(X2))
& r1(X2,sK14(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK13(X0))
& r1(X0,sK13(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X1,sK13(X0)),skolemize(X3,sK14(X2)),skolemize(X4,sK15(X2))],[f27]) ).
fof(f53,plain,
? [X0] :
( ! [X40] :
( ? [X41] :
( ! [X42] :
( ~ p2(X42)
| ! [X43] :
( p2(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
& ~ p2(X41)
& r1(X40,X41) )
| p2(X40)
| ~ r1(X0,X40) )
& ( ? [X34] :
( ! [X36] :
( ( ? [X39] : r1(X36,X39)
& ~ p1(X36) )
| ! [X37] :
( ! [X38] : ~ r1(X37,X38)
| p1(X37)
| ~ r1(X36,X37) )
| ~ r1(X34,X36) )
& ? [X35] : r1(X34,X35)
& ~ p1(X34)
& r1(X0,X34) )
| ! [X33] : ~ r1(X0,X33)
| p1(X0) )
& ( ? [X27] :
( ! [X29] :
( ( ? [X32] : r1(X29,X32)
& ~ p1(X29)
& ~ p2(X29) )
| ! [X30] :
( ! [X31] : ~ r1(X30,X31)
| p1(X30)
| p2(X30)
| ~ r1(X29,X30) )
| ~ r1(X27,X29) )
& ? [X28] : r1(X27,X28)
& ~ p1(X27)
& ~ p2(X27)
& r1(X0,X27) )
| ! [X26] : ~ r1(X0,X26)
| p1(X0)
| p2(X0) )
& ( ? [X24] :
( sP0(X24)
& ? [X25] : r1(X24,X25)
& ~ p1(X24)
& ~ p2(X24)
& ~ p3(X24)
& r1(X0,X24) )
| ! [X23] : ~ r1(X0,X23)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X21] :
( sP1(X21)
& ? [X22] : r1(X21,X22)
& ~ p1(X21)
& ~ p2(X21)
& ~ p3(X21)
& ~ p4(X21)
& r1(X0,X21) )
| ! [X20] : ~ r1(X0,X20)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X14] :
( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP3(X17)
| sP4(X17)
| ~ r1(X14,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
& ~ p2(X14) )
| sP5(X14) )
& r1(X0,X14) )
| sP7(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) )
& ( sP8(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) )
& ( sP9(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p5(X3)
| ~ r1(X2,X3) )
& r1(X1,X2) )
& ~ p1(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f22]) ).
fof(f54,plain,
( ! [X40] :
( ( ! [X42] :
( ~ p2(X42)
| ! [X43] :
( p2(X43)
| ~ r1(X42,X43) )
| ~ r1(sK57(X40),X42) )
& ~ p2(sK57(X40))
& r1(X40,sK57(X40)) )
| p2(X40)
| ~ r1(sK36,X40) )
& ( ( ! [X36] :
( ( r1(X36,sK56(X36))
& ~ p1(X36) )
| ! [X37] :
( ! [X38] : ~ r1(X37,X38)
| p1(X37)
| ~ r1(X36,X37) )
| ~ r1(sK54,X36) )
& r1(sK54,sK55)
& ~ p1(sK54)
& r1(sK36,sK54) )
| ! [X33] : ~ r1(sK36,X33)
| p1(sK36) )
& ( ( ! [X29] :
( ( r1(X29,sK53(X29))
& ~ p1(X29)
& ~ p2(X29) )
| ! [X30] :
( ! [X31] : ~ r1(X30,X31)
| p1(X30)
| p2(X30)
| ~ r1(X29,X30) )
| ~ r1(sK51,X29) )
& r1(sK51,sK52)
& ~ p1(sK51)
& ~ p2(sK51)
& r1(sK36,sK51) )
| ! [X26] : ~ r1(sK36,X26)
| p1(sK36)
| p2(sK36) )
& ( ( sP0(sK49)
& r1(sK49,sK50)
& ~ p1(sK49)
& ~ p2(sK49)
& ~ p3(sK49)
& r1(sK36,sK49) )
| ! [X23] : ~ r1(sK36,X23)
| p1(sK36)
| p2(sK36)
| p3(sK36) )
& ( ( sP1(sK47)
& r1(sK47,sK48)
& ~ p1(sK47)
& ~ p2(sK47)
& ~ p3(sK47)
& ~ p4(sK47)
& r1(sK36,sK47) )
| ! [X20] : ~ r1(sK36,X20)
| p1(sK36)
| p2(sK36)
| p3(sK36)
| p4(sK36) )
& ( ( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP3(X17)
| sP4(X17)
| ~ r1(sK46,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(sK46,X15) )
& ~ p2(sK46) )
| sP5(sK46) )
& r1(sK36,sK46) )
| sP7(sK36) )
& ! [X11] :
( ( p1(sK44(X11))
& ~ p1(sK45(X11))
& r1(sK44(X11),sK45(X11))
& r1(X11,sK44(X11)) )
| p1(X11)
| ~ r1(sK36,X11) )
& ~ p1(sK43)
& r1(sK36,sK43)
& ( sP8(sK36)
| ! [X8] :
( ( p5(sK42(X8))
& r1(X8,sK42(X8)) )
| ~ r1(sK36,X8) ) )
& ! [X5] :
( ( p3(sK40(X5))
& ~ p3(sK41(X5))
& r1(sK40(X5),sK41(X5))
& r1(X5,sK40(X5)) )
| p3(X5)
| ~ r1(sK36,X5) )
& ~ p3(sK39)
& r1(sK36,sK39)
& ( sP9(sK36)
| ( ! [X3] :
( ~ p5(X3)
| ~ r1(sK38,X3) )
& r1(sK37,sK38)
& ~ p1(sK37)
& r1(sK36,sK37) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57]),skolemize(X0,sK36),skolemize(X1,sK37),skolemize(X2,sK38),skolemize(X4,sK39),skolemize(X6,sK40(X5)),skolemize(X7,sK41(X5)),skolemize(X9,sK42(X8)),skolemize(X10,sK43),skolemize(X12,sK44(X11)),skolemize(X13,sK45(X11)),skolemize(X14,sK46),skolemize(X21,sK47),skolemize(X22,sK48),skolemize(X24,sK49),skolemize(X25,sK50),skolemize(X27,sK51),skolemize(X28,sK52),skolemize(X32,sK53(X29)),skolemize(X34,sK54),skolemize(X35,sK55),skolemize(X39,sK56(X36)),skolemize(X41,sK57(X40))],[f53]) ).
fof(f56,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f57,plain,
! [X2,X0] :
( ~ sP9(X0)
| p2(sK11(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f58,plain,
! [X2,X0] :
( ~ sP9(X0)
| ~ p2(sK12(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f59,plain,
! [X2,X0] :
( ~ sP9(X0)
| r1(sK11(X2),sK12(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f60,plain,
! [X2,X0] :
( ~ sP9(X0)
| r1(X2,sK11(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f61,plain,
! [X0] :
( ~ sP9(X0)
| ~ p2(sK10(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f62,plain,
! [X0] :
( ~ sP9(X0)
| r1(X0,sK10(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f63,plain,
! [X2,X0] :
( ~ sP8(X0)
| p2(sK14(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f64,plain,
! [X2,X0] :
( ~ sP8(X0)
| ~ p2(sK15(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f65,plain,
! [X2,X0] :
( ~ sP8(X0)
| r1(sK14(X2),sK15(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f66,plain,
! [X2,X0] :
( ~ sP8(X0)
| r1(X2,sK14(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f67,plain,
! [X0] :
( ~ sP8(X0)
| ~ p2(sK13(X0)) ),
inference(cnf_transformation,[],[f28]) ).
fof(f68,plain,
! [X0] :
( ~ sP8(X0)
| r1(X0,sK13(X0)) ),
inference(cnf_transformation,[],[f28]) ).
fof(f116,plain,
! [X40,X42,X43] :
( ~ p2(X42)
| p2(X43)
| ~ r1(X42,X43)
| ~ r1(sK57(X40),X42)
| p2(X40)
| ~ r1(sK36,X40) ),
inference(cnf_transformation,[],[f54]) ).
fof(f117,plain,
! [X40] :
( ~ p2(sK57(X40))
| p2(X40)
| ~ r1(sK36,X40) ),
inference(cnf_transformation,[],[f54]) ).
fof(f118,plain,
! [X40] :
( r1(X40,sK57(X40))
| p2(X40)
| ~ r1(sK36,X40) ),
inference(cnf_transformation,[],[f54]) ).
fof(f155,plain,
! [X8] :
( sP8(sK36)
| p5(sK42(X8))
| ~ r1(sK36,X8) ),
inference(cnf_transformation,[],[f54]) ).
fof(f156,plain,
! [X8] :
( sP8(sK36)
| r1(X8,sK42(X8))
| ~ r1(sK36,X8) ),
inference(cnf_transformation,[],[f54]) ).
fof(f163,plain,
! [X3] :
( sP9(sK36)
| ~ p5(X3)
| ~ r1(sK38,X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f164,plain,
( sP9(sK36)
| r1(sK37,sK38) ),
inference(cnf_transformation,[],[f54]) ).
fof(f166,plain,
( sP9(sK36)
| r1(sK36,sK37) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_51,plain,
! [X0: $i] :
( r1(X0,sK10(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ sP9(X0)
| ~ p2(sK10(X0)) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK11(X1))
| ~ sP9(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK11(X1),sK12(X1))
| ~ sP9(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP9(X0)
| ~ p2(sK12(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK11(X1))
| ~ sP9(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_57,plain,
! [X0: $i] :
( r1(X0,sK13(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_58,plain,
! [X0: $i] :
( ~ sP8(X0)
| ~ p2(sK13(X0)) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK14(X1))
| ~ sP8(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK14(X1),sK15(X1))
| ~ sP8(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP8(X0)
| ~ p2(sK15(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK14(X1))
| ~ sP8(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_110,negated_conjecture,
( sP9(sK36)
| r1(sK36,sK37) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_112,negated_conjecture,
( sP9(sK36)
| r1(sK37,sK38) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_113,negated_conjecture,
! [X0: $i] :
( sP9(sK36)
| ~ p5(X0)
| ~ r1(sK38,X0) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_120,negated_conjecture,
! [X0: $i] :
( sP8(sK36)
| r1(X0,sK42(X0))
| ~ r1(sK36,X0) ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_121,negated_conjecture,
! [X0: $i] :
( sP8(sK36)
| p5(sK42(X0))
| ~ r1(sK36,X0) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_158,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK57(X0))
| ~ r1(sK36,X0) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_159,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK57(X0))
| ~ r1(sK36,X0) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_160,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK36,X0)
| ~ r1(X1,X2)
| ~ r1(sK57(X0),X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_166,plain,
( ~ sP8(sK36)
| ~ p2(sK13(sK36)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_167,plain,
( r1(sK36,sK13(sK36))
| ~ sP8(sK36) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_168,plain,
( ~ sP9(sK36)
| ~ p2(sK10(sK36)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_169,plain,
( r1(sK36,sK10(sK36))
| ~ sP9(sK36) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_1220,plain,
! [X0: $i] :
( sP8(sK36)
| sP9(sK36)
| ~ r1(sK36,X0)
| ~ r1(sK38,sK42(X0)) ),
inference(resolution,[status(thm)],[c_113,c_121]) ).
tcf(c_9187,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ r1(sK36,X0)
| ~ r1(sK38,sK42(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_1220]) ).
tcf(c_9188,plain,
( iPr_def_10
| sP8(sK36)
| sP9(sK36) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1220]) ).
tcf(c_9210,plain,
! [X0: $i] :
( p2(sK13(X0))
| r1(sK13(X0),sK57(sK13(X0)))
| ~ r1(sK36,sK13(X0)) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_9211,plain,
( p2(sK13(sK36))
| r1(sK13(sK36),sK57(sK13(sK36)))
| ~ r1(sK36,sK13(sK36)) ),
inference(instantiation,[status(thm)],[c_9210]) ).
tcf(c_9224,plain,
! [X0: $i] :
( p2(sK10(X0))
| r1(sK10(X0),sK57(sK10(X0)))
| ~ r1(sK36,sK10(X0)) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_9225,plain,
( p2(sK10(sK36))
| r1(sK10(sK36),sK57(sK10(sK36)))
| ~ r1(sK36,sK10(sK36)) ),
inference(instantiation,[status(thm)],[c_9224]) ).
tcf(c_9248,plain,
( ~ iPr_def_10
| ~ r1(sK36,sK38)
| ~ r1(sK38,sK42(sK38)) ),
inference(instantiation,[status(thm)],[c_9187]) ).
tcf(c_9268,plain,
! [X0: $i] :
( r1(sK36,sK38)
| ~ r1(sK36,X0)
| ~ r1(X0,sK38) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_9322,plain,
( sP8(sK36)
| r1(sK38,sK42(sK38))
| ~ r1(sK36,sK38) ),
inference(instantiation,[status(thm)],[c_120]) ).
tcf(c_9332,plain,
( r1(sK36,sK38)
| ~ r1(sK37,sK38)
| ~ r1(sK36,sK37) ),
inference(instantiation,[status(thm)],[c_9268]) ).
tcf(c_9369,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| ~ sP8(X0)
| ~ p2(sK15(sK57(X1)))
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_9375,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| p2(sK14(sK57(X1)))
| ~ sP8(X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_9382,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| r1(sK57(X1),sK14(sK57(X1)))
| ~ sP8(X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_9388,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| r1(sK14(sK57(X1)),sK15(sK57(X1)))
| ~ sP8(X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_9411,plain,
! [X0: $i,X1: $i] :
( r1(sK36,sK57(X1))
| ~ r1(sK36,X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_9577,plain,
! [X0: $i] :
( r1(sK36,sK57(sK13(X0)))
| ~ r1(sK36,sK13(X0))
| ~ r1(sK13(X0),sK57(sK13(X0))) ),
inference(instantiation,[status(thm)],[c_9411]) ).
tcf(c_9578,plain,
( r1(sK36,sK57(sK13(sK36)))
| ~ r1(sK36,sK13(sK36))
| ~ r1(sK13(sK36),sK57(sK13(sK36))) ),
inference(instantiation,[status(thm)],[c_9577]) ).
tcf(c_9744,plain,
! [X0: $i] :
( p2(sK57(sK13(X0)))
| r1(sK14(sK57(sK13(X0))),sK15(sK57(sK13(X0))))
| ~ sP8(sK36)
| ~ r1(sK36,sK57(sK13(X0))) ),
inference(instantiation,[status(thm)],[c_9388]) ).
tcf(c_9745,plain,
! [X0: $i] :
( p2(sK57(sK13(X0)))
| r1(sK57(sK13(X0)),sK14(sK57(sK13(X0))))
| ~ sP8(sK36)
| ~ r1(sK36,sK57(sK13(X0))) ),
inference(instantiation,[status(thm)],[c_9382]) ).
tcf(c_9746,plain,
! [X0: $i] :
( p2(sK57(sK13(X0)))
| p2(sK14(sK57(sK13(X0))))
| ~ sP8(sK36)
| ~ r1(sK36,sK57(sK13(X0))) ),
inference(instantiation,[status(thm)],[c_9375]) ).
tcf(c_9747,plain,
! [X0: $i] :
( p2(sK57(sK13(X0)))
| ~ sP8(sK36)
| ~ p2(sK15(sK57(sK13(X0))))
| ~ r1(sK36,sK57(sK13(X0))) ),
inference(instantiation,[status(thm)],[c_9369]) ).
tcf(c_9748,plain,
( p2(sK57(sK13(sK36)))
| ~ sP8(sK36)
| ~ p2(sK15(sK57(sK13(sK36))))
| ~ r1(sK36,sK57(sK13(sK36))) ),
inference(instantiation,[status(thm)],[c_9747]) ).
tcf(c_9749,plain,
( p2(sK57(sK13(sK36)))
| p2(sK14(sK57(sK13(sK36))))
| ~ sP8(sK36)
| ~ r1(sK36,sK57(sK13(sK36))) ),
inference(instantiation,[status(thm)],[c_9746]) ).
tcf(c_9750,plain,
( p2(sK57(sK13(sK36)))
| r1(sK57(sK13(sK36)),sK14(sK57(sK13(sK36))))
| ~ sP8(sK36)
| ~ r1(sK36,sK57(sK13(sK36))) ),
inference(instantiation,[status(thm)],[c_9745]) ).
tcf(c_9751,plain,
( p2(sK57(sK13(sK36)))
| r1(sK14(sK57(sK13(sK36))),sK15(sK57(sK13(sK36))))
| ~ sP8(sK36)
| ~ r1(sK36,sK57(sK13(sK36))) ),
inference(instantiation,[status(thm)],[c_9744]) ).
tcf(c_9905,plain,
( sP9(sK36)
| sP8(sK36) ),
inference(global_subsumption_just,[status(thm)],[c_9188,c_112,c_110,c_9188,c_9248,c_9322,c_9332]) ).
tcf(c_9906,plain,
( sP8(sK36)
| sP9(sK36) ),
inference(renaming,[status(thm)],[c_9905]) ).
tcf(c_10125,plain,
( p2(sK10(sK36))
| ~ sP9(sK36)
| ~ p2(sK57(sK10(sK36))) ),
inference(superposition,[status(thm)],[c_51,c_159]) ).
tcf(c_10126,plain,
( p2(sK13(sK36))
| ~ sP8(sK36)
| ~ p2(sK57(sK13(sK36))) ),
inference(superposition,[status(thm)],[c_57,c_159]) ).
tcf(c_10195,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK13(X0))
| ~ r1(sK36,sK13(X0))
| ~ p2(sK14(sK57(sK13(X0))))
| ~ r1(sK14(sK57(sK13(X0))),X1)
| ~ r1(sK57(sK13(X0)),sK14(sK57(sK13(X0)))) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_10965,plain,
! [X0: $i] :
( sP9(sK36)
| r1(X0,sK37)
| ~ r1(X0,sK36) ),
inference(resolution,[status(thm)],[c_50,c_110]) ).
tcf(c_11298,plain,
! [X0: $i] :
( p2(sK13(X0))
| p2(sK15(sK57(sK13(X0))))
| ~ r1(sK36,sK13(X0))
| ~ p2(sK14(sK57(sK13(X0))))
| ~ r1(sK57(sK13(X0)),sK14(sK57(sK13(X0))))
| ~ r1(sK14(sK57(sK13(X0))),sK15(sK57(sK13(X0)))) ),
inference(instantiation,[status(thm)],[c_10195]) ).
tcf(c_11299,plain,
( p2(sK13(sK36))
| p2(sK15(sK57(sK13(sK36))))
| ~ r1(sK36,sK13(sK36))
| ~ p2(sK14(sK57(sK13(sK36))))
| ~ r1(sK57(sK13(sK36)),sK14(sK57(sK13(sK36))))
| ~ r1(sK14(sK57(sK13(sK36))),sK15(sK57(sK13(sK36)))) ),
inference(instantiation,[status(thm)],[c_11298]) ).
tcf(c_11454,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| p2(sK11(sK57(X1)))
| ~ sP9(X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_11464,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| r1(sK57(X1),sK11(sK57(X1)))
| ~ sP9(X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_11472,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| r1(sK11(sK57(X1)),sK12(sK57(X1)))
| ~ sP9(X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_11500,plain,
! [X0: $i,X1: $i] :
( r1(sK36,sK57(X1))
| ~ r1(sK36,X0)
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_11677,plain,
! [X0: $i] :
( r1(sK36,sK57(sK10(X0)))
| ~ r1(sK36,sK10(X0))
| ~ r1(sK10(X0),sK57(sK10(X0))) ),
inference(instantiation,[status(thm)],[c_11500]) ).
tcf(c_11678,plain,
( r1(sK36,sK57(sK10(sK36)))
| ~ r1(sK36,sK10(sK36))
| ~ r1(sK10(sK36),sK57(sK10(sK36))) ),
inference(instantiation,[status(thm)],[c_11677]) ).
tcf(c_11857,plain,
! [X0: $i] :
( p2(sK57(sK10(X0)))
| r1(sK11(sK57(sK10(X0))),sK12(sK57(sK10(X0))))
| ~ sP9(sK36)
| ~ r1(sK36,sK57(sK10(X0))) ),
inference(instantiation,[status(thm)],[c_11472]) ).
tcf(c_11858,plain,
! [X0: $i] :
( p2(sK57(sK10(X0)))
| r1(sK57(sK10(X0)),sK11(sK57(sK10(X0))))
| ~ sP9(sK36)
| ~ r1(sK36,sK57(sK10(X0))) ),
inference(instantiation,[status(thm)],[c_11464]) ).
tcf(c_11859,plain,
! [X0: $i] :
( p2(sK57(sK10(X0)))
| p2(sK11(sK57(sK10(X0))))
| ~ sP9(sK36)
| ~ r1(sK36,sK57(sK10(X0))) ),
inference(instantiation,[status(thm)],[c_11454]) ).
tcf(c_11860,plain,
( p2(sK57(sK10(sK36)))
| p2(sK11(sK57(sK10(sK36))))
| ~ sP9(sK36)
| ~ r1(sK36,sK57(sK10(sK36))) ),
inference(instantiation,[status(thm)],[c_11859]) ).
tcf(c_11861,plain,
( p2(sK57(sK10(sK36)))
| r1(sK57(sK10(sK36)),sK11(sK57(sK10(sK36))))
| ~ sP9(sK36)
| ~ r1(sK36,sK57(sK10(sK36))) ),
inference(instantiation,[status(thm)],[c_11858]) ).
tcf(c_11862,plain,
( p2(sK57(sK10(sK36)))
| r1(sK11(sK57(sK10(sK36))),sK12(sK57(sK10(sK36))))
| ~ sP9(sK36)
| ~ r1(sK36,sK57(sK10(sK36))) ),
inference(instantiation,[status(thm)],[c_11857]) ).
tcf(c_12452,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK10(X0))
| ~ r1(sK36,sK10(X0))
| ~ p2(sK11(sK57(sK10(X0))))
| ~ r1(sK11(sK57(sK10(X0))),X1)
| ~ r1(sK57(sK10(X0)),sK11(sK57(sK10(X0)))) ),
inference(instantiation,[status(thm)],[c_160]) ).
tcf(c_12910,plain,
sP9(sK36),
inference(global_subsumption_just,[status(thm)],[c_10965,c_166,c_167,c_9211,c_9578,c_9748,c_9749,c_9750,c_9751,c_9906,c_10126,c_11299]) ).
tcf(c_13584,plain,
! [X0: $i] :
( p2(sK10(X0))
| p2(sK12(sK57(sK10(X0))))
| ~ r1(sK36,sK10(X0))
| ~ p2(sK11(sK57(sK10(X0))))
| ~ r1(sK57(sK10(X0)),sK11(sK57(sK10(X0))))
| ~ r1(sK11(sK57(sK10(X0))),sK12(sK57(sK10(X0)))) ),
inference(instantiation,[status(thm)],[c_12452]) ).
tcf(c_13585,plain,
( p2(sK10(sK36))
| p2(sK12(sK57(sK10(sK36))))
| ~ r1(sK36,sK10(sK36))
| ~ p2(sK11(sK57(sK10(sK36))))
| ~ r1(sK57(sK10(sK36)),sK11(sK57(sK10(sK36))))
| ~ r1(sK11(sK57(sK10(sK36))),sK12(sK57(sK10(sK36)))) ),
inference(instantiation,[status(thm)],[c_13584]) ).
tcf(c_24155,plain,
! [X0: $i,X1: $i] :
( p2(sK57(X1))
| ~ sP9(X0)
| ~ p2(sK12(sK57(X1)))
| ~ r1(X0,sK57(X1)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_24917,plain,
! [X0: $i] :
( p2(sK57(sK10(X0)))
| ~ sP9(sK36)
| ~ p2(sK12(sK57(sK10(X0))))
| ~ r1(sK36,sK57(sK10(X0))) ),
inference(instantiation,[status(thm)],[c_24155]) ).
tcf(c_24918,plain,
( p2(sK57(sK10(sK36)))
| ~ sP9(sK36)
| ~ p2(sK12(sK57(sK10(sK36))))
| ~ r1(sK36,sK57(sK10(sK36))) ),
inference(instantiation,[status(thm)],[c_24917]) ).
tcf(c_24919,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_24918,c_13585,c_12910,c_11862,c_11861,c_11860,c_11678,c_10125,c_9225,c_169,c_168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL676+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/0.42 % Computer : n018.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Thu Sep 24 00:15:32 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/0.49 Running first-order theorem proving
% 0.17/0.49 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.17/0.50
% 0.17/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.17/0.50
% 0.17/0.50 % Detected problem language: tptp
% 0.26/0.52 % Proving...
% 49.01/8.06 % SZS status Started for theBenchmark.p
% 49.01/8.06 % SZS status Theorem for theBenchmark.p
% 49.01/8.06
% 49.01/8.06 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 49.01/8.06
% 49.01/8.06 % ------ iProver source info
% 49.01/8.06
% 49.01/8.06 % git: date: 2026-07-19 20:42:38 +0200
% 49.01/8.06 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 49.01/8.06 % git: non_committed_changes: false
% 49.01/8.06
% 49.01/8.06 % ------ Parsing...
% 49.01/8.06 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 49.01/8.06
% 49.01/8.06 % ------ Preprocessing... sf_s rm: 34 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 49.01/8.06
% 49.01/8.06 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e
% 49.01/8.06 % ------ Proving...
% 49.01/8.06 % ------ Problem Properties
% 49.01/8.06
% 49.01/8.06 %
% 49.01/8.06 % clauses 79
% 49.01/8.06 % conjectures 25
% 49.01/8.06 % EPR 18
% 49.01/8.06 % Horn 34
% 49.01/8.06 % unary 5
% 49.01/8.06 % binary 15
% 49.01/8.06 % lits 273
% 49.01/8.06 % lits eq 0
% 49.01/8.06 % fd_pure 0
% 49.01/8.06 % fd_pseudo 0
% 49.01/8.06 % fd_cond 0
% 49.01/8.06 % fd_pseudo_cond 0
% 49.01/8.06 % AC symbols 0
% 49.01/8.06
% 49.01/8.06 % ------ Input Options Time Limit: Unbounded
% 49.01/8.06
% 49.01/8.06
% 49.01/8.06 % ------
% 49.01/8.06 % Current options:
% 49.01/8.06 % ------
% 49.01/8.06
% 49.01/8.06
% 49.01/8.06 %
% 49.01/8.06
% 49.01/8.06 % ------ Proving...
% 49.01/8.06 %
% 49.01/8.06
% 49.01/8.06 % SZS status Theorem for theBenchmark.p
% 49.01/8.06
% 49.01/8.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 49.01/8.07
% 49.01/8.07
%------------------------------------------------------------------------------