%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL642+1.005 : 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 : n014.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:01 PM UTC 2026
% Result : Theorem 2.53s 1.72s
% Output : CNFRefutation 2.53s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f13ERROR: Could not build tree for root c_13210ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f17,plain,
! [X0] :
( ~ sP7(X0)
| ( ( ? [X20] :
( p2(X20)
& ? [X21] :
( ~ p2(X21)
& r1(X20,X21) )
& r1(X0,X20) )
| p2(X0) )
& ( ? [X17] :
( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17)
& r1(X0,X17) )
| sP6(X0) ) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f18,plain,
! [X0] :
( ~ sP7(X0)
| ( ( ? [X4] :
( p2(X4)
& ? [X5] :
( ~ p2(X5)
& r1(X4,X5) )
& r1(X0,X4) )
| p2(X0) )
& ( ? [X1] :
( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
& ~ p2(X1)
& r1(X0,X1) )
| sP6(X0) ) ) ),
inference(rectify,[],[f17]) ).
fof(f19,plain,
! [X0] :
( ~ sP7(X0)
| ( ( ( p2(sK9(X0))
& ~ p2(sK10(X0))
& r1(sK9(X0),sK10(X0))
& r1(X0,sK9(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK8(X0),X2) )
& ~ p2(sK8(X0))
& r1(X0,sK8(X0)) )
| sP6(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X4,sK9(X0)),skolemize(X5,sK10(X0))],[f18]) ).
fof(f20,plain,
! [X0] :
( ~ sP6(X0)
| ! [X13] :
( ! [X14] :
( ? [X15] :
( p2(X15)
& ? [X16] :
( ~ p2(X16)
& r1(X15,X16) )
& r1(X14,X15) )
| p2(X14)
| ~ r1(X13,X14) )
| ~ r1(X0,X13) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f21,plain,
! [X0] :
( ~ sP6(X0)
| ! [X1] :
( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] :
( ~ p2(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f20]) ).
fof(f22,plain,
! [X0] :
( ~ sP6(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK11(X2))
& ~ p2(sK12(X2))
& r1(sK11(X2),sK12(X2))
& r1(X2,sK11(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f21]) ).
fof(f23,plain,
! [X22] :
( ~ sP5(X22)
| ( ! [X27] :
( ? [X28] :
( p2(X28)
& ? [X29] :
( ~ p2(X29)
& r1(X28,X29) )
& r1(X27,X28) )
| p2(X27)
| ~ r1(X22,X27) )
& ? [X23] :
( ? [X24] :
( ! [X25] :
( ~ p2(X25)
| ! [X26] :
( p2(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
& ~ p2(X24)
& r1(X23,X24) )
& r1(X22,X23) ) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f24,plain,
! [X0] :
( ~ sP5(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
& ~ p2(X2)
& r1(X1,X2) )
& r1(X0,X1) ) ) ),
inference(rectify,[],[f23]) ).
fof(f25,plain,
! [X0] :
( ~ sP5(X0)
| ( ! [X5] :
( ( p2(sK15(X5))
& ~ p2(sK16(X5))
& r1(sK15(X5),sK16(X5))
& r1(X5,sK15(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK14(X0),X3) )
& ~ p2(sK14(X0))
& r1(sK13(X0),sK14(X0))
& r1(X0,sK13(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16]),skolemize(X1,sK13(X0)),skolemize(X2,sK14(X0)),skolemize(X6,sK15(X5)),skolemize(X7,sK16(X5))],[f24]) ).
fof(f26,plain,
! [X32] :
( ~ sP4(X32)
| ! [X33] :
( ( ( ? [X41] :
( p2(X41)
& ? [X42] :
( ~ p2(X42)
& r1(X41,X42) )
& r1(X33,X41) )
| p2(X33) )
& ( ? [X38] :
( ! [X39] :
( ~ p2(X39)
| ! [X40] :
( p2(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
& ~ p2(X38)
& r1(X33,X38) )
| sP2(X33) ) )
| ~ r1(X32,X33) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f27,plain,
! [X0] :
( ~ sP4(X0)
| ! [X1] :
( ( ( ? [X5] :
( p2(X5)
& ? [X6] :
( ~ p2(X6)
& r1(X5,X6) )
& r1(X1,X5) )
| p2(X1) )
& ( ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
& ~ p2(X2)
& r1(X1,X2) )
| sP2(X1) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f26]) ).
fof(f28,plain,
! [X0] :
( ~ sP4(X0)
| ! [X1] :
( ( ( ( p2(sK18(X1))
& ~ p2(sK19(X1))
& r1(sK18(X1),sK19(X1))
& r1(X1,sK18(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK17(X1),X3) )
& ~ p2(sK17(X1))
& r1(X1,sK17(X1)) )
| sP2(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X2,sK17(X1)),skolemize(X5,sK18(X1)),skolemize(X6,sK19(X1))],[f27]) ).
fof(f29,plain,
! [X32] :
( ~ sP3(X32)
| ( ! [X47] :
( ? [X48] :
( p2(X48)
& ? [X49] :
( ~ p2(X49)
& r1(X48,X49) )
& r1(X47,X48) )
| p2(X47)
| ~ r1(X32,X47) )
& ? [X43] :
( ? [X44] :
( ! [X45] :
( ~ p2(X45)
| ! [X46] :
( p2(X46)
| ~ r1(X45,X46) )
| ~ r1(X44,X45) )
& ~ p2(X44)
& r1(X43,X44) )
& r1(X32,X43) ) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f30,plain,
! [X0] :
( ~ sP3(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
& ~ p2(X2)
& r1(X1,X2) )
& r1(X0,X1) ) ) ),
inference(rectify,[],[f29]) ).
fof(f31,plain,
! [X0] :
( ~ sP3(X0)
| ( ! [X5] :
( ( p2(sK22(X5))
& ~ p2(sK23(X5))
& r1(sK22(X5),sK23(X5))
& r1(X5,sK22(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK21(X0),X3) )
& ~ p2(sK21(X0))
& r1(sK20(X0),sK21(X0))
& r1(X0,sK20(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23]),skolemize(X1,sK20(X0)),skolemize(X2,sK21(X0)),skolemize(X6,sK22(X5)),skolemize(X7,sK23(X5))],[f30]) ).
fof(f41,plain,
? [X0] :
( ! [X39] :
( ? [X40] :
( ! [X41] :
( ~ p2(X41)
| ! [X42] :
( p2(X42)
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
& ~ p2(X40)
& r1(X39,X40) )
| p2(X39)
| ~ r1(X0,X39) )
& ( ? [X33] :
( ! [X35] :
( ( ? [X38] : r1(X35,X38)
& ~ p1(X35) )
| ! [X36] :
( ! [X37] : ~ r1(X36,X37)
| p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X33,X35) )
& ? [X34] : r1(X33,X34)
& ~ p1(X33)
& r1(X0,X33) )
| ! [X32] : ~ r1(X0,X32)
| p1(X0) )
& ( ? [X26] :
( ! [X28] :
( ( ? [X31] : r1(X28,X31)
& ~ p1(X28)
& ~ p2(X28) )
| ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| ~ r1(X28,X29) )
| ~ r1(X26,X28) )
& ? [X27] : r1(X26,X27)
& ~ p1(X26)
& ~ p2(X26)
& r1(X0,X26) )
| ! [X25] : ~ r1(X0,X25)
| p1(X0)
| p2(X0) )
& ( ? [X23] :
( sP0(X23)
& ? [X24] : r1(X23,X24)
& ~ p1(X23)
& ~ p2(X23)
& ~ p3(X23)
& r1(X0,X23) )
| ! [X22] : ~ r1(X0,X22)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X20] :
( sP1(X20)
& ? [X21] : r1(X20,X21)
& ~ p1(X20)
& ~ p2(X20)
& ~ p3(X20)
& ~ p4(X20)
& r1(X0,X20) )
| ! [X19] : ~ r1(X0,X19)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X13] :
( ! [X16] :
( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP3(X16)
| sP4(X16)
| ~ r1(X13,X16) )
& ( ( ! [X14] :
( ~ p2(X14)
| ! [X15] :
( p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
& ~ p2(X13) )
| sP5(X13) )
& r1(X0,X13) )
| sP7(X0) )
& ! [X10] :
( ? [X11] :
( p1(X11)
& ? [X12] :
( ~ p1(X12)
& r1(X11,X12) )
& r1(X10,X11) )
| p1(X10)
| ~ r1(X0,X10) )
& ? [X9] :
( ~ p1(X9)
& r1(X0,X9) )
& ! [X6] :
( ? [X7] :
( p2(X7)
& ? [X8] :
( ~ p2(X8)
& r1(X7,X8) )
& r1(X6,X7) )
| p2(X6)
| ~ r1(X0,X6) )
& ? [X5] :
( ~ p2(X5)
& r1(X0,X5) )
& ! [X2] :
( ? [X3] :
( p3(X3)
& ? [X4] :
( ~ p3(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p3(X2)
| ~ r1(X0,X2) )
& ? [X1] :
( ~ p3(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f16]) ).
fof(f42,plain,
( ! [X39] :
( ( ! [X41] :
( ~ p2(X41)
| ! [X42] :
( p2(X42)
| ~ r1(X41,X42) )
| ~ r1(sK49(X39),X41) )
& ~ p2(sK49(X39))
& r1(X39,sK49(X39)) )
| p2(X39)
| ~ r1(sK28,X39) )
& ( ( ! [X35] :
( ( r1(X35,sK48(X35))
& ~ p1(X35) )
| ! [X36] :
( ! [X37] : ~ r1(X36,X37)
| p1(X36)
| ~ r1(X35,X36) )
| ~ r1(sK46,X35) )
& r1(sK46,sK47)
& ~ p1(sK46)
& r1(sK28,sK46) )
| ! [X32] : ~ r1(sK28,X32)
| p1(sK28) )
& ( ( ! [X28] :
( ( r1(X28,sK45(X28))
& ~ p1(X28)
& ~ p2(X28) )
| ! [X29] :
( ! [X30] : ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| ~ r1(X28,X29) )
| ~ r1(sK43,X28) )
& r1(sK43,sK44)
& ~ p1(sK43)
& ~ p2(sK43)
& r1(sK28,sK43) )
| ! [X25] : ~ r1(sK28,X25)
| p1(sK28)
| p2(sK28) )
& ( ( sP0(sK41)
& r1(sK41,sK42)
& ~ p1(sK41)
& ~ p2(sK41)
& ~ p3(sK41)
& r1(sK28,sK41) )
| ! [X22] : ~ r1(sK28,X22)
| p1(sK28)
| p2(sK28)
| p3(sK28) )
& ( ( sP1(sK39)
& r1(sK39,sK40)
& ~ p1(sK39)
& ~ p2(sK39)
& ~ p3(sK39)
& ~ p4(sK39)
& r1(sK28,sK39) )
| ! [X19] : ~ r1(sK28,X19)
| p1(sK28)
| p2(sK28)
| p3(sK28)
| p4(sK28) )
& ( ( ! [X16] :
( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP3(X16)
| sP4(X16)
| ~ r1(sK38,X16) )
& ( ( ! [X14] :
( ~ p2(X14)
| ! [X15] :
( p2(X15)
| ~ r1(X14,X15) )
| ~ r1(sK38,X14) )
& ~ p2(sK38) )
| sP5(sK38) )
& r1(sK28,sK38) )
| sP7(sK28) )
& ! [X10] :
( ( p1(sK36(X10))
& ~ p1(sK37(X10))
& r1(sK36(X10),sK37(X10))
& r1(X10,sK36(X10)) )
| p1(X10)
| ~ r1(sK28,X10) )
& ~ p1(sK35)
& r1(sK28,sK35)
& ! [X6] :
( ( p2(sK33(X6))
& ~ p2(sK34(X6))
& r1(sK33(X6),sK34(X6))
& r1(X6,sK33(X6)) )
| p2(X6)
| ~ r1(sK28,X6) )
& ~ p2(sK32)
& r1(sK28,sK32)
& ! [X2] :
( ( p3(sK30(X2))
& ~ p3(sK31(X2))
& r1(sK30(X2),sK31(X2))
& r1(X2,sK30(X2)) )
| p3(X2)
| ~ r1(sK28,X2) )
& ~ p3(sK29)
& r1(sK28,sK29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49]),skolemize(X0,sK28),skolemize(X1,sK29),skolemize(X3,sK30(X2)),skolemize(X4,sK31(X2)),skolemize(X5,sK32),skolemize(X7,sK33(X6)),skolemize(X8,sK34(X6)),skolemize(X9,sK35),skolemize(X11,sK36(X10)),skolemize(X12,sK37(X10)),skolemize(X13,sK38),skolemize(X20,sK39),skolemize(X21,sK40),skolemize(X23,sK41),skolemize(X24,sK42),skolemize(X26,sK43),skolemize(X27,sK44),skolemize(X31,sK45(X28)),skolemize(X33,sK46),skolemize(X34,sK47),skolemize(X38,sK48(X35)),skolemize(X40,sK49(X39))],[f41]) ).
fof(f43,plain,
! [X0] :
( ~ sP7(X0)
| p2(sK9(X0))
| p2(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f46,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK9(X0))
| p2(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f47,plain,
! [X2,X3,X0] :
( ~ sP7(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK8(X0),X2)
| sP6(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f48,plain,
! [X0] :
( ~ sP7(X0)
| ~ p2(sK8(X0))
| sP6(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f49,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK8(X0))
| sP6(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f50,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| p2(sK11(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f51,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| ~ p2(sK12(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f52,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| r1(sK11(X2),sK12(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f53,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| r1(X2,sK11(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f54,plain,
! [X0,X5] :
( ~ sP5(X0)
| p2(sK15(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f25]) ).
fof(f55,plain,
! [X0,X5] :
( ~ sP5(X0)
| ~ p2(sK16(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f25]) ).
fof(f56,plain,
! [X0,X5] :
( ~ sP5(X0)
| r1(sK15(X5),sK16(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f25]) ).
fof(f57,plain,
! [X0,X5] :
( ~ sP5(X0)
| r1(X5,sK15(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f25]) ).
fof(f58,plain,
! [X3,X0,X4] :
( ~ sP5(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK14(X0),X3) ),
inference(cnf_transformation,[],[f25]) ).
fof(f59,plain,
! [X0] :
( ~ sP5(X0)
| ~ p2(sK14(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f60,plain,
! [X0] :
( ~ sP5(X0)
| r1(sK13(X0),sK14(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f61,plain,
! [X0] :
( ~ sP5(X0)
| r1(X0,sK13(X0)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f62,plain,
! [X0,X1] :
( ~ sP4(X0)
| p2(sK18(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
fof(f63,plain,
! [X0,X1] :
( ~ sP4(X0)
| ~ p2(sK19(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
fof(f64,plain,
! [X0,X1] :
( ~ sP4(X0)
| r1(sK18(X1),sK19(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
fof(f65,plain,
! [X0,X1] :
( ~ sP4(X0)
| r1(X1,sK18(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
fof(f69,plain,
! [X0,X5] :
( ~ sP3(X0)
| p2(sK22(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f31]) ).
fof(f70,plain,
! [X0,X5] :
( ~ sP3(X0)
| ~ p2(sK23(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f31]) ).
fof(f71,plain,
! [X0,X5] :
( ~ sP3(X0)
| r1(sK22(X5),sK23(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f31]) ).
fof(f72,plain,
! [X0,X5] :
( ~ sP3(X0)
| r1(X5,sK22(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f31]) ).
fof(f90,plain,
! [X41,X39,X42] :
( ~ p2(X41)
| p2(X42)
| ~ r1(X41,X42)
| ~ r1(sK49(X39),X41)
| p2(X39)
| ~ r1(sK28,X39) ),
inference(cnf_transformation,[],[f42]) ).
fof(f91,plain,
! [X39] :
( ~ p2(sK49(X39))
| p2(X39)
| ~ r1(sK28,X39) ),
inference(cnf_transformation,[],[f42]) ).
fof(f92,plain,
! [X39] :
( r1(X39,sK49(X39))
| p2(X39)
| ~ r1(sK28,X39) ),
inference(cnf_transformation,[],[f42]) ).
fof(f118,plain,
! [X18,X16,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP3(X16)
| sP4(X16)
| ~ r1(sK38,X16)
| sP7(sK28) ),
inference(cnf_transformation,[],[f42]) ).
fof(f119,plain,
! [X16] :
( ~ p2(X16)
| sP3(X16)
| sP4(X16)
| ~ r1(sK38,X16)
| sP7(sK28) ),
inference(cnf_transformation,[],[f42]) ).
fof(f120,plain,
! [X14,X15] :
( ~ p2(X14)
| p2(X15)
| ~ r1(X14,X15)
| ~ r1(sK38,X14)
| sP5(sK38)
| sP7(sK28) ),
inference(cnf_transformation,[],[f42]) ).
fof(f121,plain,
( ~ p2(sK38)
| sP5(sK38)
| sP7(sK28) ),
inference(cnf_transformation,[],[f42]) ).
fof(f122,plain,
( r1(sK28,sK38)
| sP7(sK28) ),
inference(cnf_transformation,[],[f42]) ).
fof(f129,plain,
! [X6] :
( p2(sK33(X6))
| p2(X6)
| ~ r1(sK28,X6) ),
inference(cnf_transformation,[],[f42]) ).
fof(f130,plain,
! [X6] :
( ~ p2(sK34(X6))
| p2(X6)
| ~ r1(sK28,X6) ),
inference(cnf_transformation,[],[f42]) ).
fof(f131,plain,
! [X6] :
( r1(sK33(X6),sK34(X6))
| p2(X6)
| ~ r1(sK28,X6) ),
inference(cnf_transformation,[],[f42]) ).
fof(f132,plain,
! [X6] :
( r1(X6,sK33(X6))
| p2(X6)
| ~ r1(sK28,X6) ),
inference(cnf_transformation,[],[f42]) ).
fof(f133,plain,
~ p2(sK32),
inference(cnf_transformation,[],[f42]) ).
fof(f134,plain,
r1(sK28,sK32),
inference(cnf_transformation,[],[f42]) ).
fof(f140,plain,
r1(sK28,sK29),
inference(cnf_transformation,[],[f42]) ).
tcf(c_49,plain,
! [X0: $i] :
( sP6(X0)
| r1(X0,sK8(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_50,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP7(X0)
| ~ p2(sK8(X0)) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| sP6(X0)
| ~ p2(X1)
| ~ sP7(X0)
| ~ r1(X1,X2)
| ~ r1(sK8(X0),X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_52,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK9(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_55,plain,
! [X0: $i] :
( p2(X0)
| p2(sK9(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK11(X2))
| ~ sP6(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP6(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP6(X0)
| ~ p2(sK12(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK11(X2))
| ~ sP6(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_60,plain,
! [X0: $i] :
( r1(X0,sK13(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_61,plain,
! [X0: $i] :
( r1(sK13(X0),sK14(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_62,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ p2(sK14(X0)) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP5(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK14(X0),X1) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK15(X1))
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK15(X1),sK16(X1))
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP5(X0)
| ~ p2(sK16(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK15(X1))
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK18(X1))
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK18(X1),sK19(X1))
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP4(X0)
| ~ p2(sK19(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK18(X1))
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK22(X1))
| ~ sP3(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK22(X1),sK23(X1))
| ~ sP3(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP3(X0)
| ~ p2(sK23(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK22(X1))
| ~ sP3(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_96,negated_conjecture,
r1(sK28,sK29),
inference(cnf_transformation,[],[f140]) ).
tcf(c_102,negated_conjecture,
r1(sK28,sK32),
inference(cnf_transformation,[],[f134]) ).
tcf(c_103,negated_conjecture,
~ p2(sK32),
inference(cnf_transformation,[],[f133]) ).
tcf(c_104,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK33(X0))
| ~ r1(sK28,X0) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_105,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(sK33(X0),sK34(X0))
| ~ r1(sK28,X0) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_106,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK34(X0))
| ~ r1(sK28,X0) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_107,negated_conjecture,
! [X0: $i] :
( p2(X0)
| p2(sK33(X0))
| ~ r1(sK28,X0) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_114,negated_conjecture,
( sP7(sK28)
| r1(sK28,sK38) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_115,negated_conjecture,
( sP5(sK38)
| sP7(sK28)
| ~ p2(sK38) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_116,negated_conjecture,
! [X0: $i,X1: $i] :
( sP5(sK38)
| sP7(sK28)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK38,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_117,negated_conjecture,
! [X0: $i] :
( sP7(sK28)
| sP3(X0)
| sP4(X0)
| ~ p2(X0)
| ~ r1(sK38,X0) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_118,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP7(sK28)
| sP3(X0)
| sP4(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK38,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_144,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK49(X0))
| ~ r1(sK28,X0) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_145,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK49(X0))
| ~ r1(sK28,X0) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_146,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK28,X0)
| ~ r1(X1,X2)
| ~ r1(sK49(X0),X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_162,plain,
( sP6(sK28)
| ~ sP7(sK28)
| ~ p2(sK8(sK28)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_163,plain,
( sP6(sK28)
| r1(sK28,sK8(sK28))
| ~ sP7(sK28) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_7655,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| p2(X1)
| ~ p2(X0)
| ~ r1(sK38,X0)
| ~ r1(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_116]) ).
tcf(c_7656,negated_conjecture,
( iPr_def_10
| sP5(sK38)
| sP7(sK28) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_116]) ).
tcf(c_7768,plain,
( ~ p2(sK49(sK32))
| ~ r1(sK28,sK32) ),
inference(resolution,[status(thm)],[c_145,c_103]) ).
tcf(c_7769,plain,
~ p2(sK49(sK32)),
inference(global_subsumption_just,[status(thm)],[c_7768,c_102,c_7768]) ).
tcf(c_7945,plain,
( p2(sK32)
| r1(sK32,sK49(sK32))
| ~ r1(sK28,sK32) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_8033,plain,
( p2(sK38)
| sP7(sK28)
| p2(sK33(sK38)) ),
inference(superposition,[status(thm)],[c_114,c_107]) ).
tcf(c_8062,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ p2(X0)
| ~ r1(sK38,X0)
| ~ r1(X0,sK32) ),
inference(resolution,[status(thm)],[c_7655,c_103]) ).
tcf(c_8098,plain,
( p2(sK38)
| ~ iPr_def_10
| ~ sP7(sK38)
| ~ p2(sK9(sK38))
| ~ r1(sK9(sK38),sK32) ),
inference(resolution,[status(thm)],[c_8062,c_52]) ).
tcf(c_8183,plain,
( p2(sK38)
| sP7(sK28)
| ~ p2(sK34(sK38)) ),
inference(superposition,[status(thm)],[c_114,c_106]) ).
tcf(c_8356,plain,
! [X0: $i] :
( p2(sK49(sK32))
| r1(sK11(sK49(sK32)),sK12(sK49(sK32)))
| ~ sP6(X0)
| ~ r1(X0,sK32)
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_8357,plain,
! [X0: $i] :
( p2(sK49(sK32))
| r1(sK49(sK32),sK11(sK49(sK32)))
| ~ sP6(X0)
| ~ r1(X0,sK32)
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_8358,plain,
! [X0: $i] :
( p2(sK49(sK32))
| p2(sK11(sK49(sK32)))
| ~ sP6(X0)
| ~ r1(X0,sK32)
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_8359,plain,
! [X0: $i] :
( p2(sK49(sK32))
| ~ sP6(X0)
| ~ r1(X0,sK32)
| ~ p2(sK12(sK49(sK32)))
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_8360,plain,
( p2(sK49(sK32))
| ~ sP6(sK28)
| ~ r1(sK28,sK32)
| ~ p2(sK12(sK49(sK32)))
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_8359]) ).
tcf(c_8361,plain,
( p2(sK49(sK32))
| p2(sK11(sK49(sK32)))
| ~ sP6(sK28)
| ~ r1(sK28,sK32)
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_8358]) ).
tcf(c_8362,plain,
( p2(sK49(sK32))
| r1(sK49(sK32),sK11(sK49(sK32)))
| ~ sP6(sK28)
| ~ r1(sK28,sK32)
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_8357]) ).
tcf(c_8363,plain,
( p2(sK49(sK32))
| r1(sK11(sK49(sK32)),sK12(sK49(sK32)))
| ~ sP6(sK28)
| ~ r1(sK28,sK32)
| ~ r1(sK32,sK49(sK32)) ),
inference(instantiation,[status(thm)],[c_8356]) ).
tcf(c_8455,plain,
( p2(sK8(sK28))
| r1(sK33(sK8(sK28)),sK34(sK8(sK28)))
| ~ r1(sK28,sK8(sK28)) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_8456,plain,
( p2(sK8(sK28))
| r1(sK8(sK28),sK33(sK8(sK28)))
| ~ r1(sK28,sK8(sK28)) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_8498,plain,
! [X0: $i,X1: $i] :
( ~ sP6(X1)
| ~ r1(X1,X0)
| ~ p2(sK12(sK49(sK32)))
| ~ r1(X0,sK49(sK32)) ),
inference(resolution,[status(thm)],[c_58,c_7769]) ).
tcf(c_8515,plain,
( sP6(sK28)
| p2(sK8(sK28))
| ~ sP7(sK28)
| ~ p2(sK34(sK8(sK28))) ),
inference(superposition,[status(thm)],[c_49,c_106]) ).
tcf(c_8517,plain,
( sP6(sK28)
| p2(sK8(sK28))
| p2(sK33(sK8(sK28)))
| ~ sP7(sK28) ),
inference(superposition,[status(thm)],[c_49,c_107]) ).
tcf(c_8614,plain,
! [X0: $i] :
( sP6(sK28)
| p2(X0)
| ~ sP7(sK28)
| ~ p2(sK33(sK8(sK28)))
| ~ r1(sK33(sK8(sK28)),X0)
| ~ r1(sK8(sK28),sK33(sK8(sK28))) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_8638,plain,
( p2(sK38)
| sP7(sK28)
| ~ p2(sK49(sK38)) ),
inference(superposition,[status(thm)],[c_114,c_145]) ).
tcf(c_8764,plain,
( sP7(sK28)
| sP3(sK13(sK38))
| sP4(sK13(sK38))
| ~ sP5(sK38)
| ~ p2(sK13(sK38)) ),
inference(superposition,[status(thm)],[c_60,c_117]) ).
tcf(c_8954,plain,
! [X0: $i] :
( p2(sK32)
| p2(X0)
| ~ r1(sK28,sK32)
| ~ p2(sK11(sK49(sK32)))
| ~ r1(sK11(sK49(sK32)),X0)
| ~ r1(sK49(sK32),sK11(sK49(sK32))) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_8990,plain,
( ~ sP6(sK28)
| ~ p2(sK12(sK49(sK32)))
| ~ r1(sK29,sK49(sK32)) ),
inference(resolution,[status(thm)],[c_8498,c_96]) ).
tcf(c_8991,plain,
( ~ sP6(sK28)
| ~ p2(sK12(sK49(sK32))) ),
inference(global_subsumption_just,[status(thm)],[c_8990,c_103,c_102,c_7768,c_7945,c_8360]) ).
tcf(c_9030,plain,
( p2(sK32)
| p2(sK12(sK49(sK32)))
| ~ r1(sK28,sK32)
| ~ p2(sK11(sK49(sK32)))
| ~ r1(sK49(sK32),sK11(sK49(sK32)))
| ~ r1(sK11(sK49(sK32)),sK12(sK49(sK32))) ),
inference(instantiation,[status(thm)],[c_8954]) ).
tcf(c_9091,plain,
( sP6(sK28)
| p2(sK34(sK8(sK28)))
| ~ sP7(sK28)
| ~ p2(sK33(sK8(sK28)))
| ~ r1(sK8(sK28),sK33(sK8(sK28)))
| ~ r1(sK33(sK8(sK28)),sK34(sK8(sK28))) ),
inference(instantiation,[status(thm)],[c_8614]) ).
tcf(c_9095,plain,
! [X0: $i,X1: $i] :
( r1(sK12(sK49(sK32)),sK11(sK12(sK49(sK32))))
| ~ sP6(sK28)
| ~ sP6(X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK12(sK49(sK32))) ),
inference(resolution,[status(thm)],[c_8991,c_56]) ).
tcf(c_9097,plain,
~ sP6(sK28),
inference(global_subsumption_just,[status(thm)],[c_9095,c_103,c_102,c_7768,c_7945,c_8360,c_8361,c_8362,c_8363,c_9030]) ).
tcf(c_9142,plain,
( ~ sP7(sK28)
| ~ p2(sK8(sK28)) ),
inference(resolution,[status(thm)],[c_9097,c_50]) ).
tcf(c_9143,plain,
~ sP7(sK28),
inference(global_subsumption_just,[status(thm)],[c_9142,c_162,c_163,c_8456,c_8455,c_8517,c_8515,c_9091,c_9097]) ).
tcf(c_9147,plain,
( sP5(sK38)
| ~ p2(sK38) ),
inference(resolution,[status(thm)],[c_9143,c_115]) ).
tcf(c_9148,plain,
( iPr_def_10
| sP5(sK38) ),
inference(resolution,[status(thm)],[c_9143,c_7656]) ).
tcf(c_9152,plain,
( ~ p2(sK38)
| ~ p2(sK14(sK38)) ),
inference(resolution,[status(thm)],[c_9147,c_62]) ).
tcf(c_9155,plain,
( iPr_def_10
| ~ p2(sK14(sK38)) ),
inference(resolution,[status(thm)],[c_9148,c_62]) ).
tcf(c_9161,plain,
! [X0: $i] :
( ~ p2(sK38)
| ~ sP3(X0)
| ~ p2(sK23(sK14(sK38)))
| ~ r1(X0,sK14(sK38)) ),
inference(resolution,[status(thm)],[c_9152,c_81]) ).
tcf(c_9162,plain,
! [X0: $i] :
( ~ p2(sK38)
| ~ sP4(X0)
| ~ p2(sK19(sK14(sK38)))
| ~ r1(X0,sK14(sK38)) ),
inference(resolution,[status(thm)],[c_9152,c_73]) ).
tcf(c_9177,plain,
( p2(sK38)
| r1(sK38,sK49(sK38))
| ~ r1(sK28,sK38) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_9180,plain,
( p2(sK38)
| r1(sK33(sK38),sK34(sK38))
| ~ r1(sK28,sK38) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_9181,plain,
( p2(sK38)
| r1(sK38,sK33(sK38))
| ~ r1(sK28,sK38) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_9218,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP5(sK38)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK14(sK38),X0) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_9219,plain,
! [X0: $i] :
( p2(X0)
| r1(sK15(X0),sK16(X0))
| ~ sP5(sK38)
| ~ r1(sK38,X0) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_9220,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK15(X0))
| ~ sP5(sK38)
| ~ r1(sK38,X0) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_9221,plain,
! [X0: $i] :
( p2(X0)
| p2(sK15(X0))
| ~ sP5(sK38)
| ~ r1(sK38,X0) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_9222,plain,
! [X0: $i] :
( p2(X0)
| ~ sP5(sK38)
| ~ p2(sK16(X0))
| ~ r1(sK38,X0) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_9223,plain,
( r1(sK13(sK38),sK14(sK38))
| ~ sP5(sK38) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_9224,plain,
( ~ sP5(sK38)
| ~ p2(sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_9225,plain,
( r1(sK38,sK13(sK38))
| ~ sP5(sK38) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_9464,plain,
( ~ sP5(sK38)
| ~ p2(sK38)
| ~ sP3(sK13(sK38))
| ~ p2(sK23(sK14(sK38))) ),
inference(resolution,[status(thm)],[c_9161,c_61]) ).
tcf(c_9465,plain,
( ~ p2(sK23(sK14(sK38)))
| ~ sP3(sK13(sK38))
| ~ p2(sK38) ),
inference(global_subsumption_just,[status(thm)],[c_9464,c_103,c_102,c_115,c_162,c_163,c_7768,c_7945,c_8360,c_8361,c_8362,c_8363,c_8456,c_8455,c_8517,c_8515,c_9030,c_9091,c_9464]) ).
tcf(c_9466,plain,
( ~ p2(sK38)
| ~ sP3(sK13(sK38))
| ~ p2(sK23(sK14(sK38))) ),
inference(renaming,[status(thm)],[c_9465]) ).
tcf(c_9474,plain,
( ~ sP5(sK38)
| ~ p2(sK38)
| ~ sP4(sK13(sK38))
| ~ p2(sK19(sK14(sK38))) ),
inference(resolution,[status(thm)],[c_9162,c_61]) ).
tcf(c_9475,plain,
( ~ p2(sK19(sK14(sK38)))
| ~ sP4(sK13(sK38))
| ~ p2(sK38) ),
inference(global_subsumption_just,[status(thm)],[c_9474,c_103,c_102,c_115,c_162,c_163,c_7768,c_7945,c_8360,c_8361,c_8362,c_8363,c_8456,c_8455,c_8517,c_8515,c_9030,c_9091,c_9474]) ).
tcf(c_9476,plain,
( ~ p2(sK38)
| ~ sP4(sK13(sK38))
| ~ p2(sK19(sK14(sK38))) ),
inference(renaming,[status(thm)],[c_9475]) ).
tcf(c_9552,plain,
! [X0: $i] :
( p2(X0)
| ~ iPr_def_10
| ~ p2(sK33(sK38))
| ~ r1(sK38,sK33(sK38))
| ~ r1(sK33(sK38),X0) ),
inference(instantiation,[status(thm)],[c_7655]) ).
tcf(c_9657,plain,
( p2(sK34(sK38))
| ~ iPr_def_10
| ~ p2(sK33(sK38))
| ~ r1(sK38,sK33(sK38))
| ~ r1(sK33(sK38),sK34(sK38)) ),
inference(instantiation,[status(thm)],[c_9552]) ).
tcf(c_9735,plain,
( p2(sK38)
| ~ iPr_def_10
| ~ sP7(sK38)
| ~ r1(sK9(sK38),sK32) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8098,c_55]) ).
tcf(c_9740,plain,
( p2(sK38)
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_9735,c_103,c_102,c_114,c_162,c_163,c_7768,c_7945,c_8033,c_8183,c_8360,c_8361,c_8362,c_8363,c_8456,c_8455,c_8517,c_8515,c_9030,c_9091,c_9181,c_9180,c_9657]) ).
tcf(c_9818,plain,
! [X0: $i,X1: $i] :
( sP7(sK28)
| p2(X1)
| sP3(sK13(sK38))
| sP4(sK13(sK38))
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK38,sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_9839,plain,
( p2(sK13(sK38))
| p2(sK15(sK13(sK38)))
| ~ sP5(sK38)
| ~ r1(sK38,sK13(sK38)) ),
inference(instantiation,[status(thm)],[c_9221]) ).
tcf(c_9840,plain,
( p2(sK49(sK38))
| p2(sK15(sK49(sK38)))
| ~ sP5(sK38)
| ~ r1(sK38,sK49(sK38)) ),
inference(instantiation,[status(thm)],[c_9221]) ).
tcf(c_9886,plain,
! [X0: $i,X1: $i] :
( iPr_def_10
| ~ sP5(X0)
| ~ p2(X1)
| ~ r1(X1,sK14(sK38))
| ~ r1(sK14(X0),X1) ),
inference(resolution,[status(thm)],[c_63,c_9155]) ).
tcf(c_9887,plain,
! [X0: $i,X1: $i] :
( ~ p2(sK38)
| ~ sP5(X0)
| ~ p2(X1)
| ~ r1(X1,sK14(sK38))
| ~ r1(sK14(X0),X1) ),
inference(resolution,[status(thm)],[c_63,c_9152]) ).
tcf(c_9890,plain,
! [X0: $i,X1: $i] :
( ~ r1(sK14(X0),X1)
| ~ r1(X1,sK14(sK38))
| ~ p2(X1)
| ~ sP5(X0) ),
inference(global_subsumption_just,[status(thm)],[c_9886,c_103,c_102,c_114,c_162,c_163,c_7768,c_7945,c_8033,c_8183,c_8360,c_8361,c_8362,c_8363,c_8456,c_8455,c_8517,c_8515,c_9030,c_9091,c_9181,c_9180,c_9657,c_9887,c_9886]) ).
tcf(c_9891,plain,
! [X0: $i,X1: $i] :
( ~ sP5(X0)
| ~ p2(X1)
| ~ r1(X1,sK14(sK38))
| ~ r1(sK14(X0),X1) ),
inference(renaming,[status(thm)],[c_9890]) ).
tcf(c_9950,plain,
( p2(sK13(sK38))
| ~ sP5(sK38)
| ~ p2(sK16(sK13(sK38)))
| ~ r1(sK38,sK13(sK38)) ),
inference(instantiation,[status(thm)],[c_9222]) ).
tcf(c_9951,plain,
( p2(sK49(sK38))
| ~ sP5(sK38)
| ~ p2(sK16(sK49(sK38)))
| ~ r1(sK38,sK49(sK38)) ),
inference(instantiation,[status(thm)],[c_9222]) ).
tcf(c_9955,plain,
( p2(sK13(sK38))
| r1(sK15(sK13(sK38)),sK16(sK13(sK38)))
| ~ sP5(sK38)
| ~ r1(sK38,sK13(sK38)) ),
inference(instantiation,[status(thm)],[c_9219]) ).
tcf(c_9956,plain,
( p2(sK49(sK38))
| r1(sK15(sK49(sK38)),sK16(sK49(sK38)))
| ~ sP5(sK38)
| ~ r1(sK38,sK49(sK38)) ),
inference(instantiation,[status(thm)],[c_9219]) ).
tcf(c_9960,plain,
( p2(sK13(sK38))
| r1(sK13(sK38),sK15(sK13(sK38)))
| ~ sP5(sK38)
| ~ r1(sK38,sK13(sK38)) ),
inference(instantiation,[status(thm)],[c_9220]) ).
tcf(c_9961,plain,
( p2(sK49(sK38))
| r1(sK49(sK38),sK15(sK49(sK38)))
| ~ sP5(sK38)
| ~ r1(sK38,sK49(sK38)) ),
inference(instantiation,[status(thm)],[c_9220]) ).
tcf(c_10075,plain,
( ~ sP5(sK38)
| ~ p2(sK14(sK38))
| ~ r1(sK14(sK38),sK14(sK38)) ),
inference(factoring,[status(thm)],[c_9891]) ).
tcf(c_10076,plain,
~ p2(sK14(sK38)),
inference(global_subsumption_just,[status(thm)],[c_10075,c_103,c_102,c_162,c_163,c_7656,c_7768,c_7945,c_8360,c_8361,c_8362,c_8363,c_8456,c_8455,c_8517,c_8515,c_9030,c_9091,c_9147,c_9224,c_9740]) ).
tcf(c_10374,plain,
! [X0: $i] :
( p2(X0)
| r1(sK18(X0),sK19(X0))
| ~ sP4(sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_10375,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK18(X0))
| ~ sP4(sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_10377,plain,
! [X0: $i] :
( p2(X0)
| p2(sK18(X0))
| ~ sP4(sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_10444,plain,
! [X0: $i] :
( p2(sK38)
| p2(X0)
| ~ r1(sK28,sK38)
| ~ p2(sK15(sK49(sK38)))
| ~ r1(sK15(sK49(sK38)),X0)
| ~ r1(sK49(sK38),sK15(sK49(sK38))) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_10639,plain,
( p2(sK38)
| p2(sK16(sK49(sK38)))
| ~ r1(sK28,sK38)
| ~ p2(sK15(sK49(sK38)))
| ~ r1(sK49(sK38),sK15(sK49(sK38)))
| ~ r1(sK15(sK49(sK38)),sK16(sK49(sK38))) ),
inference(instantiation,[status(thm)],[c_10444]) ).
tcf(c_10649,negated_conjecture,
r1(sK28,sK38),
inference(global_subsumption_just,[status(thm)],[c_114,c_114,c_9143]) ).
tcf(c_10651,negated_conjecture,
sP5(sK38),
inference(global_subsumption_just,[status(thm)],[c_7656,c_103,c_102,c_162,c_163,c_7656,c_7768,c_7945,c_8360,c_8361,c_8362,c_8363,c_8456,c_8455,c_8517,c_8515,c_9030,c_9091,c_9147,c_9740]) ).
tcf(c_10660,plain,
( p2(sK38)
| p2(sK33(sK38)) ),
inference(superposition,[status(thm)],[c_10649,c_107]) ).
tcf(c_10695,plain,
p2(sK38),
inference(global_subsumption_just,[status(thm)],[c_10660,c_114,c_8638,c_9143,c_9177,c_9840,c_9951,c_9956,c_9961,c_10639,c_10651]) ).
tcf(c_11140,plain,
( p2(sK14(sK38))
| p2(sK18(sK14(sK38)))
| ~ sP4(sK13(sK38))
| ~ r1(sK13(sK38),sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_10377]) ).
tcf(c_11152,plain,
( p2(sK14(sK38))
| r1(sK18(sK14(sK38)),sK19(sK14(sK38)))
| ~ sP4(sK13(sK38))
| ~ r1(sK13(sK38),sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_10374]) ).
tcf(c_11155,plain,
( p2(sK14(sK38))
| r1(sK14(sK38),sK18(sK14(sK38)))
| ~ sP4(sK13(sK38))
| ~ r1(sK13(sK38),sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_10375]) ).
tcf(c_11296,plain,
! [X0: $i] :
( p2(X0)
| r1(sK22(X0),sK23(X0))
| ~ sP3(sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_11297,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK22(X0))
| ~ sP3(sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_11298,plain,
! [X0: $i] :
( p2(X0)
| p2(sK22(X0))
| ~ sP3(sK13(sK38))
| ~ r1(sK13(sK38),X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_11595,plain,
( p2(sK14(sK38))
| p2(sK22(sK14(sK38)))
| ~ sP3(sK13(sK38))
| ~ r1(sK13(sK38),sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_11298]) ).
tcf(c_11654,plain,
( p2(sK14(sK38))
| r1(sK22(sK14(sK38)),sK23(sK14(sK38)))
| ~ sP3(sK13(sK38))
| ~ r1(sK13(sK38),sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_11296]) ).
tcf(c_11658,plain,
( p2(sK14(sK38))
| r1(sK14(sK38),sK22(sK14(sK38)))
| ~ sP3(sK13(sK38))
| ~ r1(sK13(sK38),sK14(sK38)) ),
inference(instantiation,[status(thm)],[c_11297]) ).
tcf(c_12155,plain,
! [X0: $i] :
( sP7(sK28)
| sP3(sK13(sK38))
| sP4(sK13(sK38))
| p2(sK16(sK13(sK38)))
| ~ p2(X0)
| ~ r1(sK38,sK13(sK38))
| ~ r1(sK13(sK38),X0)
| ~ r1(X0,sK16(sK13(sK38))) ),
inference(instantiation,[status(thm)],[c_9818]) ).
tcf(c_12573,plain,
( sP7(sK28)
| sP3(sK13(sK38))
| sP4(sK13(sK38))
| p2(sK16(sK13(sK38)))
| ~ p2(sK15(sK13(sK38)))
| ~ r1(sK38,sK13(sK38))
| ~ r1(sK13(sK38),sK15(sK13(sK38)))
| ~ r1(sK15(sK13(sK38)),sK16(sK13(sK38))) ),
inference(instantiation,[status(thm)],[c_12155]) ).
tcf(c_12768,plain,
! [X0: $i] :
( p2(X0)
| ~ sP5(sK38)
| ~ p2(sK18(sK14(sK38)))
| ~ r1(sK18(sK14(sK38)),X0)
| ~ r1(sK14(sK38),sK18(sK14(sK38))) ),
inference(instantiation,[status(thm)],[c_9218]) ).
tcf(c_12784,plain,
( p2(sK19(sK14(sK38)))
| ~ sP5(sK38)
| ~ p2(sK18(sK14(sK38)))
| ~ r1(sK14(sK38),sK18(sK14(sK38)))
| ~ r1(sK18(sK14(sK38)),sK19(sK14(sK38))) ),
inference(instantiation,[status(thm)],[c_12768]) ).
tcf(c_13186,plain,
! [X0: $i] :
( p2(X0)
| ~ sP5(sK38)
| ~ p2(sK22(sK14(sK38)))
| ~ r1(sK22(sK14(sK38)),X0)
| ~ r1(sK14(sK38),sK22(sK14(sK38))) ),
inference(instantiation,[status(thm)],[c_9218]) ).
tcf(c_13209,plain,
( p2(sK23(sK14(sK38)))
| ~ sP5(sK38)
| ~ p2(sK22(sK14(sK38)))
| ~ r1(sK14(sK38),sK22(sK14(sK38)))
| ~ r1(sK22(sK14(sK38)),sK23(sK14(sK38))) ),
inference(instantiation,[status(thm)],[c_13186]) ).
tcf(c_13210,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_13209,c_12784,c_12573,c_11658,c_11654,c_11595,c_11155,c_11152,c_11140,c_10695,c_10651,c_10076,c_9960,c_9955,c_9950,c_9839,c_9476,c_9466,c_9223,c_9225,c_9143,c_8764]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL642+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n014.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 23:52:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 2.53/1.72 % SZS status Started for theBenchmark.p
% 2.53/1.72 % SZS status Theorem for theBenchmark.p
% 2.53/1.72
% 2.53/1.72 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.53/1.72
% 2.53/1.72 % ------ iProver source info
% 2.53/1.72
% 2.53/1.72 % git: date: 2026-07-19 20:42:38 +0200
% 2.53/1.72 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.53/1.72 % git: non_committed_changes: false
% 2.53/1.72
% 2.53/1.72 % ------ Parsing...
% 2.53/1.72 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.53/1.72
% 2.53/1.72 % ------ Preprocessing... sf_s rm: 36 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.53/1.72
% 2.53/1.72 % ------ Preprocessing... gs_s sp: 1 0s gs_e snvd_s sp: 0 0s snvd_e
% 2.53/1.72 % ------ Proving...
% 2.53/1.72 % ------ Problem Properties
% 2.53/1.72
% 2.53/1.72 %
% 2.53/1.72 % clauses 63
% 2.53/1.72 % conjectures 25
% 2.53/1.72 % EPR 12
% 2.53/1.72 % Horn 27
% 2.53/1.72 % unary 6
% 2.53/1.72 % binary 7
% 2.53/1.72 % lits 223
% 2.53/1.72 % lits eq 0
% 2.53/1.72 % fd_pure 0
% 2.53/1.72 % fd_pseudo 0
% 2.53/1.72 % fd_cond 0
% 2.53/1.72 % fd_pseudo_cond 0
% 2.53/1.72 % AC symbols 0
% 2.53/1.72
% 2.53/1.72 % ------ Input Options Time Limit: Unbounded
% 2.53/1.72
% 2.53/1.72
% 2.53/1.72 % ------
% 2.53/1.72 % Current options:
% 2.53/1.72 % ------
% 2.53/1.72
% 2.53/1.72
% 2.53/1.72 %
% 2.53/1.72
% 2.53/1.72 % ------ Proving...
% 2.53/1.72 %
% 2.53/1.72
% 2.53/1.72 % SZS status Theorem for theBenchmark.p
% 2.53/1.72
% 2.53/1.72 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.53/1.72
% 2.53/1.72
%------------------------------------------------------------------------------