%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL676+1.001 : 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 : n005.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 48.02s 7.65s
% Output : CNFRefutation 48.02s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f18ERROR: Could not build tree for root c_20319ERROR: 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(f7,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f8,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(flattening,[],[f7]) ).
fof(f20,plain,
! [X0] :
( ~ sP7(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,[],[f18]) ).
fof(f21,plain,
! [X0] :
( ~ sP7(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,[],[f20]) ).
fof(f22,plain,
! [X0] :
( ~ sP7(X0)
| ( ! [X2] :
( ( p2(sK9(X2))
& ~ p2(sK10(X2))
& r1(sK9(X2),sK10(X2))
& r1(X2,sK9(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK8(X0))
& r1(X0,sK8(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X3,sK9(X2)),skolemize(X4,sK10(X2))],[f21]) ).
fof(f23,plain,
! [X0] :
( ~ sP6(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,[],[f17]) ).
fof(f24,plain,
! [X0] :
( ~ sP6(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] :
( ~ sP6(X0)
| ( ! [X2] :
( ( p2(sK12(X2))
& ~ p2(sK13(X2))
& r1(sK12(X2),sK13(X2))
& r1(X2,sK12(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK11(X0))
& r1(X0,sK11(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X1,sK11(X0)),skolemize(X3,sK12(X2)),skolemize(X4,sK13(X2))],[f24]) ).
fof(f44,plain,
? [X0] :
( ! [X20] :
( ? [X21] :
( ! [X22] :
( ~ p2(X22)
| ! [X23] :
( p2(X23)
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
& ~ p2(X21)
& r1(X20,X21) )
| p2(X20)
| ~ r1(X0,X20) )
& ( ? [X14] :
( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP1(X17)
| sP2(X17)
| ~ r1(X14,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
& ~ p2(X14) )
| sP3(X14) )
& r1(X0,X14) )
| sP5(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) )
& ( sP6(X0)
| ! [X8] :
( ? [X9] :
( p3(X9)
& r1(X8,X9) )
| ~ r1(X0,X8) ) )
& ! [X5] :
( ? [X6] :
( p4(X6)
& ? [X7] :
( ~ p4(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p4(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p4(X4)
& r1(X0,X4) )
& ( sP7(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p3(X3)
| ~ r1(X2,X3) )
& r1(X1,X2) )
& ~ p1(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f19]) ).
fof(f45,plain,
( ! [X20] :
( ( ! [X22] :
( ~ p2(X22)
| ! [X23] :
( p2(X23)
| ~ r1(X22,X23) )
| ~ r1(sK43(X20),X22) )
& ~ p2(sK43(X20))
& r1(X20,sK43(X20)) )
| p2(X20)
| ~ r1(sK32,X20) )
& ( ( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP1(X17)
| sP2(X17)
| ~ r1(sK42,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(sK42,X15) )
& ~ p2(sK42) )
| sP3(sK42) )
& r1(sK32,sK42) )
| sP5(sK32) )
& ! [X11] :
( ( p1(sK40(X11))
& ~ p1(sK41(X11))
& r1(sK40(X11),sK41(X11))
& r1(X11,sK40(X11)) )
| p1(X11)
| ~ r1(sK32,X11) )
& ~ p1(sK39)
& r1(sK32,sK39)
& ( sP6(sK32)
| ! [X8] :
( ( p3(sK38(X8))
& r1(X8,sK38(X8)) )
| ~ r1(sK32,X8) ) )
& ! [X5] :
( ( p4(sK36(X5))
& ~ p4(sK37(X5))
& r1(sK36(X5),sK37(X5))
& r1(X5,sK36(X5)) )
| p4(X5)
| ~ r1(sK32,X5) )
& ~ p4(sK35)
& r1(sK32,sK35)
& ( sP7(sK32)
| ( ! [X3] :
( ~ p3(X3)
| ~ r1(sK34,X3) )
& r1(sK33,sK34)
& ~ p1(sK33)
& r1(sK32,sK33) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43]),skolemize(X0,sK32),skolemize(X1,sK33),skolemize(X2,sK34),skolemize(X4,sK35),skolemize(X6,sK36(X5)),skolemize(X7,sK37(X5)),skolemize(X9,sK38(X8)),skolemize(X10,sK39),skolemize(X12,sK40(X11)),skolemize(X13,sK41(X11)),skolemize(X14,sK42),skolemize(X21,sK43(X20))],[f44]) ).
fof(f47,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f48,plain,
! [X2,X0] :
( ~ sP7(X0)
| p2(sK9(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f22]) ).
fof(f49,plain,
! [X2,X0] :
( ~ sP7(X0)
| ~ p2(sK10(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f22]) ).
fof(f50,plain,
! [X2,X0] :
( ~ sP7(X0)
| r1(sK9(X2),sK10(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f22]) ).
fof(f51,plain,
! [X2,X0] :
( ~ sP7(X0)
| r1(X2,sK9(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f22]) ).
fof(f52,plain,
! [X0] :
( ~ sP7(X0)
| ~ p2(sK8(X0)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f53,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK8(X0)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f54,plain,
! [X2,X0] :
( ~ sP6(X0)
| p2(sK12(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f55,plain,
! [X2,X0] :
( ~ sP6(X0)
| ~ p2(sK13(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f56,plain,
! [X2,X0] :
( ~ sP6(X0)
| r1(sK12(X2),sK13(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f57,plain,
! [X2,X0] :
( ~ sP6(X0)
| r1(X2,sK12(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f58,plain,
! [X0] :
( ~ sP6(X0)
| ~ p2(sK11(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f59,plain,
! [X0] :
( ~ sP6(X0)
| r1(X0,sK11(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f98,plain,
! [X22,X23,X20] :
( ~ p2(X22)
| p2(X23)
| ~ r1(X22,X23)
| ~ r1(sK43(X20),X22)
| p2(X20)
| ~ r1(sK32,X20) ),
inference(cnf_transformation,[],[f45]) ).
fof(f99,plain,
! [X20] :
( ~ p2(sK43(X20))
| p2(X20)
| ~ r1(sK32,X20) ),
inference(cnf_transformation,[],[f45]) ).
fof(f100,plain,
! [X20] :
( r1(X20,sK43(X20))
| p2(X20)
| ~ r1(sK32,X20) ),
inference(cnf_transformation,[],[f45]) ).
fof(f112,plain,
! [X8] :
( sP6(sK32)
| p3(sK38(X8))
| ~ r1(sK32,X8) ),
inference(cnf_transformation,[],[f45]) ).
fof(f113,plain,
! [X8] :
( sP6(sK32)
| r1(X8,sK38(X8))
| ~ r1(sK32,X8) ),
inference(cnf_transformation,[],[f45]) ).
fof(f120,plain,
! [X3] :
( sP7(sK32)
| ~ p3(X3)
| ~ r1(sK34,X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f121,plain,
( sP7(sK32)
| r1(sK33,sK34) ),
inference(cnf_transformation,[],[f45]) ).
fof(f123,plain,
( sP7(sK32)
| r1(sK32,sK33) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_51,plain,
! [X0: $i] :
( r1(X0,sK8(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ sP7(X0)
| ~ p2(sK8(X0)) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK9(X1))
| ~ sP7(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK9(X1),sK10(X1))
| ~ sP7(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP7(X0)
| ~ p2(sK10(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK9(X1))
| ~ sP7(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_57,plain,
! [X0: $i] :
( r1(X0,sK11(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_58,plain,
! [X0: $i] :
( ~ sP6(X0)
| ~ p2(sK11(X0)) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK12(X1))
| ~ sP6(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK12(X1),sK13(X1))
| ~ sP6(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP6(X0)
| ~ p2(sK13(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK12(X1))
| ~ sP6(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_101,negated_conjecture,
( sP7(sK32)
| r1(sK32,sK33) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_103,negated_conjecture,
( sP7(sK32)
| r1(sK33,sK34) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_104,negated_conjecture,
! [X0: $i] :
( sP7(sK32)
| ~ p3(X0)
| ~ r1(sK34,X0) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_111,negated_conjecture,
! [X0: $i] :
( sP6(sK32)
| r1(X0,sK38(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_112,negated_conjecture,
! [X0: $i] :
( sP6(sK32)
| p3(sK38(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_124,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK43(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_125,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK43(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_126,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK32,X0)
| ~ r1(X1,X2)
| ~ r1(sK43(X0),X1) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_132,plain,
( ~ sP6(sK32)
| ~ p2(sK11(sK32)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_133,plain,
( r1(sK32,sK11(sK32))
| ~ sP6(sK32) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_134,plain,
( ~ sP7(sK32)
| ~ p2(sK8(sK32)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_135,plain,
( r1(sK32,sK8(sK32))
| ~ sP7(sK32) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_732,plain,
! [X0: $i] :
( sP6(sK32)
| sP7(sK32)
| ~ r1(sK32,X0)
| ~ r1(sK34,sK38(X0)) ),
inference(resolution,[status(thm)],[c_104,c_112]) ).
tcf(c_8689,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ r1(sK32,X0)
| ~ r1(sK34,sK38(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_732]) ).
tcf(c_8690,plain,
( iPr_def_10
| sP6(sK32)
| sP7(sK32) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_732]) ).
tcf(c_8712,plain,
! [X0: $i] :
( p2(sK11(X0))
| r1(sK11(X0),sK43(sK11(X0)))
| ~ r1(sK32,sK11(X0)) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_8713,plain,
( p2(sK11(sK32))
| r1(sK11(sK32),sK43(sK11(sK32)))
| ~ r1(sK32,sK11(sK32)) ),
inference(instantiation,[status(thm)],[c_8712]) ).
tcf(c_8726,plain,
! [X0: $i] :
( p2(sK8(X0))
| r1(sK8(X0),sK43(sK8(X0)))
| ~ r1(sK32,sK8(X0)) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_8727,plain,
( p2(sK8(sK32))
| r1(sK8(sK32),sK43(sK8(sK32)))
| ~ r1(sK32,sK8(sK32)) ),
inference(instantiation,[status(thm)],[c_8726]) ).
tcf(c_8750,plain,
( ~ iPr_def_10
| ~ r1(sK32,sK34)
| ~ r1(sK34,sK38(sK34)) ),
inference(instantiation,[status(thm)],[c_8689]) ).
tcf(c_8770,plain,
! [X0: $i] :
( r1(sK32,sK34)
| ~ r1(sK32,X0)
| ~ r1(X0,sK34) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_8824,plain,
( sP6(sK32)
| r1(sK34,sK38(sK34))
| ~ r1(sK32,sK34) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_8834,plain,
( r1(sK32,sK34)
| ~ r1(sK33,sK34)
| ~ r1(sK32,sK33) ),
inference(instantiation,[status(thm)],[c_8770]) ).
tcf(c_8878,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| ~ sP6(X0)
| ~ p2(sK13(sK43(X1)))
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_8884,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| p2(sK12(sK43(X1)))
| ~ sP6(X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_8891,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| r1(sK43(X1),sK12(sK43(X1)))
| ~ sP6(X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_8897,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| r1(sK12(sK43(X1)),sK13(sK43(X1)))
| ~ sP6(X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_8920,plain,
! [X0: $i,X1: $i] :
( r1(sK32,sK43(X1))
| ~ r1(sK32,X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_9086,plain,
! [X0: $i] :
( r1(sK32,sK43(sK11(X0)))
| ~ r1(sK32,sK11(X0))
| ~ r1(sK11(X0),sK43(sK11(X0))) ),
inference(instantiation,[status(thm)],[c_8920]) ).
tcf(c_9087,plain,
( r1(sK32,sK43(sK11(sK32)))
| ~ r1(sK32,sK11(sK32))
| ~ r1(sK11(sK32),sK43(sK11(sK32))) ),
inference(instantiation,[status(thm)],[c_9086]) ).
tcf(c_9253,plain,
! [X0: $i] :
( p2(sK43(sK11(X0)))
| r1(sK12(sK43(sK11(X0))),sK13(sK43(sK11(X0))))
| ~ sP6(sK32)
| ~ r1(sK32,sK43(sK11(X0))) ),
inference(instantiation,[status(thm)],[c_8897]) ).
tcf(c_9254,plain,
! [X0: $i] :
( p2(sK43(sK11(X0)))
| r1(sK43(sK11(X0)),sK12(sK43(sK11(X0))))
| ~ sP6(sK32)
| ~ r1(sK32,sK43(sK11(X0))) ),
inference(instantiation,[status(thm)],[c_8891]) ).
tcf(c_9255,plain,
! [X0: $i] :
( p2(sK43(sK11(X0)))
| p2(sK12(sK43(sK11(X0))))
| ~ sP6(sK32)
| ~ r1(sK32,sK43(sK11(X0))) ),
inference(instantiation,[status(thm)],[c_8884]) ).
tcf(c_9256,plain,
! [X0: $i] :
( p2(sK43(sK11(X0)))
| ~ sP6(sK32)
| ~ p2(sK13(sK43(sK11(X0))))
| ~ r1(sK32,sK43(sK11(X0))) ),
inference(instantiation,[status(thm)],[c_8878]) ).
tcf(c_9257,plain,
( p2(sK43(sK11(sK32)))
| ~ sP6(sK32)
| ~ p2(sK13(sK43(sK11(sK32))))
| ~ r1(sK32,sK43(sK11(sK32))) ),
inference(instantiation,[status(thm)],[c_9256]) ).
tcf(c_9258,plain,
( p2(sK43(sK11(sK32)))
| p2(sK12(sK43(sK11(sK32))))
| ~ sP6(sK32)
| ~ r1(sK32,sK43(sK11(sK32))) ),
inference(instantiation,[status(thm)],[c_9255]) ).
tcf(c_9259,plain,
( p2(sK43(sK11(sK32)))
| r1(sK43(sK11(sK32)),sK12(sK43(sK11(sK32))))
| ~ sP6(sK32)
| ~ r1(sK32,sK43(sK11(sK32))) ),
inference(instantiation,[status(thm)],[c_9254]) ).
tcf(c_9260,plain,
( p2(sK43(sK11(sK32)))
| r1(sK12(sK43(sK11(sK32))),sK13(sK43(sK11(sK32))))
| ~ sP6(sK32)
| ~ r1(sK32,sK43(sK11(sK32))) ),
inference(instantiation,[status(thm)],[c_9253]) ).
tcf(c_9408,plain,
( sP7(sK32)
| sP6(sK32) ),
inference(global_subsumption_just,[status(thm)],[c_8690,c_103,c_101,c_8690,c_8750,c_8824,c_8834]) ).
tcf(c_9409,plain,
( sP6(sK32)
| sP7(sK32) ),
inference(renaming,[status(thm)],[c_9408]) ).
tcf(c_9597,plain,
( p2(sK8(sK32))
| ~ sP7(sK32)
| ~ p2(sK43(sK8(sK32))) ),
inference(superposition,[status(thm)],[c_51,c_125]) ).
tcf(c_9598,plain,
( p2(sK11(sK32))
| ~ sP6(sK32)
| ~ p2(sK43(sK11(sK32))) ),
inference(superposition,[status(thm)],[c_57,c_125]) ).
tcf(c_9699,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK11(X0))
| ~ r1(sK32,sK11(X0))
| ~ p2(sK12(sK43(sK11(X0))))
| ~ r1(sK12(sK43(sK11(X0))),X1)
| ~ r1(sK43(sK11(X0)),sK12(sK43(sK11(X0)))) ),
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_10425,plain,
! [X0: $i] :
( sP7(sK32)
| r1(X0,sK33)
| ~ r1(X0,sK32) ),
inference(resolution,[status(thm)],[c_50,c_101]) ).
tcf(c_10810,plain,
! [X0: $i] :
( p2(sK11(X0))
| p2(sK13(sK43(sK11(X0))))
| ~ r1(sK32,sK11(X0))
| ~ p2(sK12(sK43(sK11(X0))))
| ~ r1(sK43(sK11(X0)),sK12(sK43(sK11(X0))))
| ~ r1(sK12(sK43(sK11(X0))),sK13(sK43(sK11(X0)))) ),
inference(instantiation,[status(thm)],[c_9699]) ).
tcf(c_10811,plain,
( p2(sK11(sK32))
| p2(sK13(sK43(sK11(sK32))))
| ~ r1(sK32,sK11(sK32))
| ~ p2(sK12(sK43(sK11(sK32))))
| ~ r1(sK43(sK11(sK32)),sK12(sK43(sK11(sK32))))
| ~ r1(sK12(sK43(sK11(sK32))),sK13(sK43(sK11(sK32)))) ),
inference(instantiation,[status(thm)],[c_10810]) ).
tcf(c_10947,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| p2(sK9(sK43(X1)))
| ~ sP7(X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_10957,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| r1(sK43(X1),sK9(sK43(X1)))
| ~ sP7(X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_10965,plain,
! [X0: $i,X1: $i] :
( p2(sK43(X1))
| r1(sK9(sK43(X1)),sK10(sK43(X1)))
| ~ sP7(X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_10993,plain,
! [X0: $i,X1: $i] :
( r1(sK32,sK43(X1))
| ~ r1(sK32,X0)
| ~ r1(X0,sK43(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_11170,plain,
! [X0: $i] :
( r1(sK32,sK43(sK8(X0)))
| ~ r1(sK32,sK8(X0))
| ~ r1(sK8(X0),sK43(sK8(X0))) ),
inference(instantiation,[status(thm)],[c_10993]) ).
tcf(c_11171,plain,
( r1(sK32,sK43(sK8(sK32)))
| ~ r1(sK32,sK8(sK32))
| ~ r1(sK8(sK32),sK43(sK8(sK32))) ),
inference(instantiation,[status(thm)],[c_11170]) ).
tcf(c_11350,plain,
! [X0: $i] :
( p2(sK43(sK8(X0)))
| r1(sK9(sK43(sK8(X0))),sK10(sK43(sK8(X0))))
| ~ sP7(sK32)
| ~ r1(sK32,sK43(sK8(X0))) ),
inference(instantiation,[status(thm)],[c_10965]) ).
tcf(c_11351,plain,
! [X0: $i] :
( p2(sK43(sK8(X0)))
| r1(sK43(sK8(X0)),sK9(sK43(sK8(X0))))
| ~ sP7(sK32)
| ~ r1(sK32,sK43(sK8(X0))) ),
inference(instantiation,[status(thm)],[c_10957]) ).
tcf(c_11352,plain,
! [X0: $i] :
( p2(sK43(sK8(X0)))
| p2(sK9(sK43(sK8(X0))))
| ~ sP7(sK32)
| ~ r1(sK32,sK43(sK8(X0))) ),
inference(instantiation,[status(thm)],[c_10947]) ).
tcf(c_11353,plain,
( p2(sK43(sK8(sK32)))
| p2(sK9(sK43(sK8(sK32))))
| ~ sP7(sK32)
| ~ r1(sK32,sK43(sK8(sK32))) ),
inference(instantiation,[status(thm)],[c_11352]) ).
tcf(c_11354,plain,
( p2(sK43(sK8(sK32)))
| r1(sK43(sK8(sK32)),sK9(sK43(sK8(sK32))))
| ~ sP7(sK32)
| ~ r1(sK32,sK43(sK8(sK32))) ),
inference(instantiation,[status(thm)],[c_11351]) ).
tcf(c_11355,plain,
( p2(sK43(sK8(sK32)))
| r1(sK9(sK43(sK8(sK32))),sK10(sK43(sK8(sK32))))
| ~ sP7(sK32)
| ~ r1(sK32,sK43(sK8(sK32))) ),
inference(instantiation,[status(thm)],[c_11350]) ).
tcf(c_11949,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK8(X0))
| ~ r1(sK32,sK8(X0))
| ~ p2(sK9(sK43(sK8(X0))))
| ~ r1(sK9(sK43(sK8(X0))),X1)
| ~ r1(sK43(sK8(X0)),sK9(sK43(sK8(X0)))) ),
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_12327,plain,
sP7(sK32),
inference(global_subsumption_just,[status(thm)],[c_10425,c_132,c_133,c_8713,c_9087,c_9257,c_9258,c_9259,c_9260,c_9409,c_9598,c_10811]) ).
tcf(c_13112,plain,
! [X0: $i] :
( p2(sK8(X0))
| p2(sK10(sK43(sK8(X0))))
| ~ r1(sK32,sK8(X0))
| ~ p2(sK9(sK43(sK8(X0))))
| ~ r1(sK43(sK8(X0)),sK9(sK43(sK8(X0))))
| ~ r1(sK9(sK43(sK8(X0))),sK10(sK43(sK8(X0)))) ),
inference(instantiation,[status(thm)],[c_11949]) ).
tcf(c_13113,plain,
( p2(sK8(sK32))
| p2(sK10(sK43(sK8(sK32))))
| ~ r1(sK32,sK8(sK32))
| ~ p2(sK9(sK43(sK8(sK32))))
| ~ r1(sK43(sK8(sK32)),sK9(sK43(sK8(sK32))))
| ~ r1(sK9(sK43(sK8(sK32))),sK10(sK43(sK8(sK32)))) ),
inference(instantiation,[status(thm)],[c_13112]) ).
tcf(c_20317,plain,
! [X0: $i,X1: $i] :
( p2(sK43(sK8(X1)))
| ~ sP7(X0)
| ~ p2(sK10(sK43(sK8(X1))))
| ~ r1(X0,sK43(sK8(X1))) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_20318,plain,
( p2(sK43(sK8(sK32)))
| ~ sP7(sK32)
| ~ p2(sK10(sK43(sK8(sK32))))
| ~ r1(sK32,sK43(sK8(sK32))) ),
inference(instantiation,[status(thm)],[c_20317]) ).
tcf(c_20319,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_20318,c_13113,c_12327,c_11355,c_11354,c_11353,c_11171,c_9597,c_8727,c_135,c_134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL676+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.44 % Computer : n005.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Thu Sep 24 00:13:17 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.50 Running first-order theorem proving
% 0.17/0.50 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.24/0.51
% 0.24/0.51 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.51
% 0.24/0.51 % Detected problem language: tptp
% 0.24/0.53 % Proving...
% 48.02/7.65 % SZS status Started for theBenchmark.p
% 48.02/7.65 % SZS status Theorem for theBenchmark.p
% 48.02/7.65
% 48.02/7.65 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 48.02/7.65
% 48.02/7.65 % ------ iProver source info
% 48.02/7.65
% 48.02/7.65 % git: date: 2026-07-19 20:42:38 +0200
% 48.02/7.65 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 48.02/7.65 % git: non_committed_changes: false
% 48.02/7.65
% 48.02/7.65 % ------ Parsing...
% 48.02/7.65 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 48.02/7.65
% 48.02/7.65 % ------ Preprocessing... sf_s rm: 2 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 48.02/7.65
% 48.02/7.65 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e
% 48.02/7.65 % ------ Proving...
% 48.02/7.65 % ------ Problem Properties
% 48.02/7.65
% 48.02/7.65 %
% 48.02/7.65 % clauses 77
% 48.02/7.65 % conjectures 23
% 48.02/7.65 % EPR 16
% 48.02/7.65 % Horn 34
% 48.02/7.65 % unary 5
% 48.02/7.65 % binary 14
% 48.02/7.65 % lits 268
% 48.02/7.65 % lits eq 0
% 48.02/7.65 % fd_pure 0
% 48.02/7.65 % fd_pseudo 0
% 48.02/7.65 % fd_cond 0
% 48.02/7.65 % fd_pseudo_cond 0
% 48.02/7.65 % AC symbols 0
% 48.02/7.65
% 48.02/7.65 % ------ Input Options Time Limit: Unbounded
% 48.02/7.65
% 48.02/7.65
% 48.02/7.65 % ------
% 48.02/7.65 % Current options:
% 48.02/7.65 % ------
% 48.02/7.65
% 48.02/7.65
% 48.02/7.65 %
% 48.02/7.65
% 48.02/7.65 % ------ Proving...
% 48.02/7.65 %
% 48.02/7.65
% 48.02/7.65 % SZS status Theorem for theBenchmark.p
% 48.02/7.65
% 48.02/7.65 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 48.02/7.65
% 48.02/7.65
%------------------------------------------------------------------------------