%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL660+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 : n001.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:47 PM UTC 2026
% Result : Theorem 26.27s 4.20s
% Output : CNFRefutation 26.28s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f17ERROR: Could not build tree for root c_25539ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f19,plain,
! [X0] :
( ~ sP8(X0)
| ( ! [X13] :
( ? [X14] :
( p2(X14)
& ? [X15] :
( ~ p2(X15)
& r1(X14,X15) )
& r1(X13,X14) )
| p2(X13)
| ~ r1(X0,X13) )
& ? [X12] :
( ~ p2(X12)
& r1(X0,X12) ) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f20,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,[],[f19]) ).
fof(f21,plain,
! [X0] :
( ~ sP8(X0)
| ( ! [X2] :
( ( p2(sK10(X2))
& ~ p2(sK11(X2))
& r1(sK10(X2),sK11(X2))
& r1(X2,sK10(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK9(X0))
& r1(X0,sK9(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X1,sK9(X0)),skolemize(X3,sK10(X2)),skolemize(X4,sK11(X2))],[f20]) ).
fof(f22,plain,
! [X0] :
( ~ sP7(X0)
| ( ( ? [X27] :
( p2(X27)
& ? [X28] :
( ~ p2(X28)
& r1(X27,X28) )
& r1(X0,X27) )
| p2(X0) )
& ( ? [X24] :
( ! [X25] :
( ~ p2(X25)
| ! [X26] :
( p2(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
& ~ p2(X24)
& r1(X0,X24) )
| sP6(X0) ) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f23,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,[],[f22]) ).
fof(f24,plain,
! [X0] :
( ~ sP7(X0)
| ( ( ( p2(sK13(X0))
& ~ p2(sK14(X0))
& r1(sK13(X0),sK14(X0))
& r1(X0,sK13(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK12(X0),X2) )
& ~ p2(sK12(X0))
& r1(X0,sK12(X0)) )
| sP6(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X1,sK12(X0)),skolemize(X4,sK13(X0)),skolemize(X5,sK14(X0))],[f23]) ).
fof(f25,plain,
! [X0] :
( ~ sP6(X0)
| ! [X20] :
( ! [X21] :
( ? [X22] :
( p2(X22)
& ? [X23] :
( ~ p2(X23)
& r1(X22,X23) )
& r1(X21,X22) )
| p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X0,X20) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f26,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,[],[f25]) ).
fof(f27,plain,
! [X0] :
( ~ sP6(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK15(X2))
& ~ p2(sK16(X2))
& r1(sK15(X2),sK16(X2))
& r1(X2,sK15(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X3,sK15(X2)),skolemize(X4,sK16(X2))],[f26]) ).
fof(f28,plain,
! [X29] :
( ~ sP5(X29)
| ( ! [X34] :
( ? [X35] :
( p2(X35)
& ? [X36] :
( ~ p2(X36)
& r1(X35,X36) )
& r1(X34,X35) )
| p2(X34)
| ~ r1(X29,X34) )
& ? [X30] :
( ? [X31] :
( ! [X32] :
( ~ p2(X32)
| ! [X33] :
( p2(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
& ~ p2(X31)
& r1(X30,X31) )
& r1(X29,X30) ) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f29,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,[],[f28]) ).
fof(f30,plain,
! [X0] :
( ~ sP5(X0)
| ( ! [X5] :
( ( p2(sK19(X5))
& ~ p2(sK20(X5))
& r1(sK19(X5),sK20(X5))
& r1(X5,sK19(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK18(X0),X3) )
& ~ p2(sK18(X0))
& r1(sK17(X0),sK18(X0))
& r1(X0,sK17(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19,sK20]),skolemize(X1,sK17(X0)),skolemize(X2,sK18(X0)),skolemize(X6,sK19(X5)),skolemize(X7,sK20(X5))],[f29]) ).
fof(f31,plain,
! [X39] :
( ~ sP4(X39)
| ! [X40] :
( ( ( ? [X48] :
( p2(X48)
& ? [X49] :
( ~ p2(X49)
& r1(X48,X49) )
& r1(X40,X48) )
| p2(X40) )
& ( ? [X45] :
( ! [X46] :
( ~ p2(X46)
| ! [X47] :
( p2(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p2(X45)
& r1(X40,X45) )
| sP2(X40) ) )
| ~ r1(X39,X40) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f32,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,[],[f31]) ).
fof(f33,plain,
! [X0] :
( ~ sP4(X0)
| ! [X1] :
( ( ( ( p2(sK22(X1))
& ~ p2(sK23(X1))
& r1(sK22(X1),sK23(X1))
& r1(X1,sK22(X1)) )
| p2(X1) )
& ( ( ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK21(X1),X3) )
& ~ p2(sK21(X1))
& r1(X1,sK21(X1)) )
| sP2(X1) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23]),skolemize(X2,sK21(X1)),skolemize(X5,sK22(X1)),skolemize(X6,sK23(X1))],[f32]) ).
fof(f34,plain,
! [X39] :
( ~ sP3(X39)
| ( ! [X54] :
( ? [X55] :
( p2(X55)
& ? [X56] :
( ~ p2(X56)
& r1(X55,X56) )
& r1(X54,X55) )
| p2(X54)
| ~ r1(X39,X54) )
& ? [X50] :
( ? [X51] :
( ! [X52] :
( ~ p2(X52)
| ! [X53] :
( p2(X53)
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
& ~ p2(X51)
& r1(X50,X51) )
& r1(X39,X50) ) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f35,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,[],[f34]) ).
fof(f36,plain,
! [X0] :
( ~ sP3(X0)
| ( ! [X5] :
( ( p2(sK26(X5))
& ~ p2(sK27(X5))
& r1(sK26(X5),sK27(X5))
& r1(X5,sK26(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK25(X0),X3) )
& ~ p2(sK25(X0))
& r1(sK24(X0),sK25(X0))
& r1(X0,sK24(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26,sK27]),skolemize(X1,sK24(X0)),skolemize(X2,sK25(X0)),skolemize(X6,sK26(X5)),skolemize(X7,sK27(X5))],[f35]) ).
fof(f46,plain,
? [X0] :
( ! [X42] :
( ? [X43] :
( ! [X44] :
( ~ p2(X44)
| ! [X45] :
( p2(X45)
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
& ~ p2(X43)
& r1(X42,X43) )
| p2(X42)
| ~ r1(X0,X42) )
& ( ? [X36] :
( ! [X38] :
( ( ? [X41] : r1(X38,X41)
& ~ p1(X38) )
| ! [X39] :
( ! [X40] : ~ r1(X39,X40)
| p1(X39)
| ~ r1(X38,X39) )
| ~ r1(X36,X38) )
& ? [X37] : r1(X36,X37)
& ~ p1(X36)
& r1(X0,X36) )
| ! [X35] : ~ r1(X0,X35)
| p1(X0) )
& ( ? [X29] :
( ! [X31] :
( ( ? [X34] : r1(X31,X34)
& ~ p1(X31)
& ~ p2(X31) )
| ! [X32] :
( ! [X33] : ~ r1(X32,X33)
| p1(X32)
| p2(X32)
| ~ r1(X31,X32) )
| ~ r1(X29,X31) )
& ? [X30] : r1(X29,X30)
& ~ p1(X29)
& ~ p2(X29)
& r1(X0,X29) )
| ! [X28] : ~ r1(X0,X28)
| p1(X0)
| p2(X0) )
& ( ? [X26] :
( sP0(X26)
& ? [X27] : r1(X26,X27)
& ~ p1(X26)
& ~ p2(X26)
& ~ p3(X26)
& r1(X0,X26) )
| ! [X25] : ~ r1(X0,X25)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X23] :
( sP1(X23)
& ? [X24] : r1(X23,X24)
& ~ p1(X23)
& ~ p2(X23)
& ~ p3(X23)
& ~ p4(X23)
& r1(X0,X23) )
| ! [X22] : ~ r1(X0,X22)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X16] :
( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP3(X19)
| sP4(X19)
| ~ r1(X16,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
& ~ p2(X16) )
| sP5(X16) )
& r1(X0,X16) )
| sP7(X0) )
& ! [X13] :
( ? [X14] :
( p1(X14)
& ? [X15] :
( ~ p1(X15)
& r1(X14,X15) )
& r1(X13,X14) )
| p1(X13)
| ~ r1(X0,X13) )
& ? [X12] :
( ~ p1(X12)
& r1(X0,X12) )
& ( sP8(X0)
| ! [X10] :
( ? [X11] :
( p5(X11)
& r1(X10,X11) )
| ~ r1(X0,X10) ) )
& ! [X7] :
( ? [X8] :
( p3(X8)
& ? [X9] :
( ~ p3(X9)
& r1(X8,X9) )
& r1(X7,X8) )
| p3(X7)
| ~ r1(X0,X7) )
& ? [X6] :
( ~ p3(X6)
& r1(X0,X6) )
& ( ( ! [X3] :
( ? [X4] :
( p2(X4)
& ? [X5] :
( ~ p2(X5)
& r1(X4,X5) )
& r1(X3,X4) )
| p2(X3)
| ~ r1(X0,X3) )
& ? [X2] :
( ~ p2(X2)
& r1(X0,X2) ) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(X0,X1) ) ) ),
inference(rectify,[],[f18]) ).
fof(f47,plain,
( ! [X42] :
( ( ! [X44] :
( ~ p2(X44)
| ! [X45] :
( p2(X45)
| ~ r1(X44,X45) )
| ~ r1(sK54(X42),X44) )
& ~ p2(sK54(X42))
& r1(X42,sK54(X42)) )
| p2(X42)
| ~ r1(sK32,X42) )
& ( ( ! [X38] :
( ( r1(X38,sK53(X38))
& ~ p1(X38) )
| ! [X39] :
( ! [X40] : ~ r1(X39,X40)
| p1(X39)
| ~ r1(X38,X39) )
| ~ r1(sK51,X38) )
& r1(sK51,sK52)
& ~ p1(sK51)
& r1(sK32,sK51) )
| ! [X35] : ~ r1(sK32,X35)
| p1(sK32) )
& ( ( ! [X31] :
( ( r1(X31,sK50(X31))
& ~ p1(X31)
& ~ p2(X31) )
| ! [X32] :
( ! [X33] : ~ r1(X32,X33)
| p1(X32)
| p2(X32)
| ~ r1(X31,X32) )
| ~ r1(sK48,X31) )
& r1(sK48,sK49)
& ~ p1(sK48)
& ~ p2(sK48)
& r1(sK32,sK48) )
| ! [X28] : ~ r1(sK32,X28)
| p1(sK32)
| p2(sK32) )
& ( ( sP0(sK46)
& r1(sK46,sK47)
& ~ p1(sK46)
& ~ p2(sK46)
& ~ p3(sK46)
& r1(sK32,sK46) )
| ! [X25] : ~ r1(sK32,X25)
| p1(sK32)
| p2(sK32)
| p3(sK32) )
& ( ( sP1(sK44)
& r1(sK44,sK45)
& ~ p1(sK44)
& ~ p2(sK44)
& ~ p3(sK44)
& ~ p4(sK44)
& r1(sK32,sK44) )
| ! [X22] : ~ r1(sK32,X22)
| p1(sK32)
| p2(sK32)
| p3(sK32)
| p4(sK32) )
& ( ( ! [X19] :
( ( ! [X20] :
( ~ p2(X20)
| ! [X21] :
( p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
& ~ p2(X19) )
| sP3(X19)
| sP4(X19)
| ~ r1(sK43,X19) )
& ( ( ! [X17] :
( ~ p2(X17)
| ! [X18] :
( p2(X18)
| ~ r1(X17,X18) )
| ~ r1(sK43,X17) )
& ~ p2(sK43) )
| sP5(sK43) )
& r1(sK32,sK43) )
| sP7(sK32) )
& ! [X13] :
( ( p1(sK41(X13))
& ~ p1(sK42(X13))
& r1(sK41(X13),sK42(X13))
& r1(X13,sK41(X13)) )
| p1(X13)
| ~ r1(sK32,X13) )
& ~ p1(sK40)
& r1(sK32,sK40)
& ( sP8(sK32)
| ! [X10] :
( ( p5(sK39(X10))
& r1(X10,sK39(X10)) )
| ~ r1(sK32,X10) ) )
& ! [X7] :
( ( p3(sK37(X7))
& ~ p3(sK38(X7))
& r1(sK37(X7),sK38(X7))
& r1(X7,sK37(X7)) )
| p3(X7)
| ~ r1(sK32,X7) )
& ~ p3(sK36)
& r1(sK32,sK36)
& ( ( ! [X3] :
( ( p2(sK34(X3))
& ~ p2(sK35(X3))
& r1(sK34(X3),sK35(X3))
& r1(X3,sK34(X3)) )
| p2(X3)
| ~ r1(sK32,X3) )
& ~ p2(sK33)
& r1(sK32,sK33) )
| ! [X1] :
( ~ p5(X1)
| ~ r1(sK32,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51,sK52,sK53,sK54]),skolemize(X0,sK32),skolemize(X2,sK33),skolemize(X4,sK34(X3)),skolemize(X5,sK35(X3)),skolemize(X6,sK36),skolemize(X8,sK37(X7)),skolemize(X9,sK38(X7)),skolemize(X11,sK39(X10)),skolemize(X12,sK40),skolemize(X14,sK41(X13)),skolemize(X15,sK42(X13)),skolemize(X16,sK43),skolemize(X23,sK44),skolemize(X24,sK45),skolemize(X26,sK46),skolemize(X27,sK47),skolemize(X29,sK48),skolemize(X30,sK49),skolemize(X34,sK50(X31)),skolemize(X36,sK51),skolemize(X37,sK52),skolemize(X41,sK53(X38)),skolemize(X43,sK54(X42))],[f46]) ).
fof(f48,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f49,plain,
! [X2,X0] :
( ~ sP8(X0)
| p2(sK10(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f50,plain,
! [X2,X0] :
( ~ sP8(X0)
| ~ p2(sK11(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f51,plain,
! [X2,X0] :
( ~ sP8(X0)
| r1(sK10(X2),sK11(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f52,plain,
! [X2,X0] :
( ~ sP8(X0)
| r1(X2,sK10(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f53,plain,
! [X0] :
( ~ sP8(X0)
| ~ p2(sK9(X0)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f54,plain,
! [X0] :
( ~ sP8(X0)
| r1(X0,sK9(X0)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f59,plain,
! [X2,X3,X0] :
( ~ sP7(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK12(X0),X2)
| sP6(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f60,plain,
! [X0] :
( ~ sP7(X0)
| ~ p2(sK12(X0))
| sP6(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f61,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK12(X0))
| sP6(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f62,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| p2(sK15(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
fof(f63,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| ~ p2(sK16(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
fof(f64,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| r1(sK15(X2),sK16(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
fof(f65,plain,
! [X2,X0,X1] :
( ~ sP6(X0)
| r1(X2,sK15(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
fof(f66,plain,
! [X0,X5] :
( ~ sP5(X0)
| p2(sK19(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f30]) ).
fof(f67,plain,
! [X0,X5] :
( ~ sP5(X0)
| ~ p2(sK20(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f30]) ).
fof(f68,plain,
! [X0,X5] :
( ~ sP5(X0)
| r1(sK19(X5),sK20(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f30]) ).
fof(f69,plain,
! [X0,X5] :
( ~ sP5(X0)
| r1(X5,sK19(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f30]) ).
fof(f70,plain,
! [X3,X0,X4] :
( ~ sP5(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK18(X0),X3) ),
inference(cnf_transformation,[],[f30]) ).
fof(f71,plain,
! [X0] :
( ~ sP5(X0)
| ~ p2(sK18(X0)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f72,plain,
! [X0] :
( ~ sP5(X0)
| r1(sK17(X0),sK18(X0)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f73,plain,
! [X0] :
( ~ sP5(X0)
| r1(X0,sK17(X0)) ),
inference(cnf_transformation,[],[f30]) ).
fof(f74,plain,
! [X0,X1] :
( ~ sP4(X0)
| p2(sK22(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f75,plain,
! [X0,X1] :
( ~ sP4(X0)
| ~ p2(sK23(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f76,plain,
! [X0,X1] :
( ~ sP4(X0)
| r1(sK22(X1),sK23(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f77,plain,
! [X0,X1] :
( ~ sP4(X0)
| r1(X1,sK22(X1))
| p2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f81,plain,
! [X0,X5] :
( ~ sP3(X0)
| p2(sK26(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f36]) ).
fof(f82,plain,
! [X0,X5] :
( ~ sP3(X0)
| ~ p2(sK27(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f36]) ).
fof(f83,plain,
! [X0,X5] :
( ~ sP3(X0)
| r1(sK26(X5),sK27(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f36]) ).
fof(f84,plain,
! [X0,X5] :
( ~ sP3(X0)
| r1(X5,sK26(X5))
| p2(X5)
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f36]) ).
fof(f102,plain,
! [X44,X45,X42] :
( ~ p2(X44)
| p2(X45)
| ~ r1(X44,X45)
| ~ r1(sK54(X42),X44)
| p2(X42)
| ~ r1(sK32,X42) ),
inference(cnf_transformation,[],[f47]) ).
fof(f103,plain,
! [X42] :
( ~ p2(sK54(X42))
| p2(X42)
| ~ r1(sK32,X42) ),
inference(cnf_transformation,[],[f47]) ).
fof(f104,plain,
! [X42] :
( r1(X42,sK54(X42))
| p2(X42)
| ~ r1(sK32,X42) ),
inference(cnf_transformation,[],[f47]) ).
fof(f130,plain,
! [X21,X19,X20] :
( ~ p2(X20)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| sP3(X19)
| sP4(X19)
| ~ r1(sK43,X19)
| sP7(sK32) ),
inference(cnf_transformation,[],[f47]) ).
fof(f131,plain,
! [X19] :
( ~ p2(X19)
| sP3(X19)
| sP4(X19)
| ~ r1(sK43,X19)
| sP7(sK32) ),
inference(cnf_transformation,[],[f47]) ).
fof(f132,plain,
! [X18,X17] :
( ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(sK43,X17)
| sP5(sK43)
| sP7(sK32) ),
inference(cnf_transformation,[],[f47]) ).
fof(f133,plain,
( ~ p2(sK43)
| sP5(sK43)
| sP7(sK32) ),
inference(cnf_transformation,[],[f47]) ).
fof(f134,plain,
( r1(sK32,sK43)
| sP7(sK32) ),
inference(cnf_transformation,[],[f47]) ).
fof(f141,plain,
! [X10] :
( sP8(sK32)
| p5(sK39(X10))
| ~ r1(sK32,X10) ),
inference(cnf_transformation,[],[f47]) ).
fof(f142,plain,
! [X10] :
( sP8(sK32)
| r1(X10,sK39(X10))
| ~ r1(sK32,X10) ),
inference(cnf_transformation,[],[f47]) ).
fof(f146,plain,
! [X7] :
( r1(X7,sK37(X7))
| p3(X7)
| ~ r1(sK32,X7) ),
inference(cnf_transformation,[],[f47]) ).
fof(f149,plain,
! [X3,X1] :
( p2(sK34(X3))
| p2(X3)
| ~ r1(sK32,X3)
| ~ p5(X1)
| ~ r1(sK32,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f150,plain,
! [X3,X1] :
( ~ p2(sK35(X3))
| p2(X3)
| ~ r1(sK32,X3)
| ~ p5(X1)
| ~ r1(sK32,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f151,plain,
! [X3,X1] :
( r1(sK34(X3),sK35(X3))
| p2(X3)
| ~ r1(sK32,X3)
| ~ p5(X1)
| ~ r1(sK32,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f152,plain,
! [X3,X1] :
( r1(X3,sK34(X3))
| p2(X3)
| ~ r1(sK32,X3)
| ~ p5(X1)
| ~ r1(sK32,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f153,plain,
! [X1] :
( ~ p2(sK33)
| ~ p5(X1)
| ~ r1(sK32,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f154,plain,
! [X1] :
( r1(sK32,sK33)
| ~ p5(X1)
| ~ r1(sK32,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f48]) ).
tcf(c_50,plain,
! [X0: $i] :
( r1(X0,sK9(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_51,negated_conjecture,
! [X0: $i] :
( ~ sP8(X0)
| ~ p2(sK9(X0)) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK10(X1))
| ~ sP8(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK10(X1),sK11(X1))
| ~ sP8(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP8(X0)
| ~ p2(sK11(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK10(X1))
| ~ sP8(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_56,plain,
! [X0: $i] :
( sP6(X0)
| r1(X0,sK12(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_57,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP7(X0)
| ~ p2(sK12(X0)) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP6(X0)
| p2(X2)
| ~ sP7(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK12(X0),X1) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK15(X2))
| ~ sP6(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK15(X2),sK16(X2))
| ~ sP6(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP6(X0)
| ~ p2(sK16(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK15(X2))
| ~ sP6(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_67,plain,
! [X0: $i] :
( r1(X0,sK17(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_68,plain,
! [X0: $i] :
( r1(sK17(X0),sK18(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_69,negated_conjecture,
! [X0: $i] :
( ~ sP5(X0)
| ~ p2(sK18(X0)) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP5(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK18(X0),X1) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK19(X1))
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK19(X1),sK20(X1))
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP5(X0)
| ~ p2(sK20(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK19(X1))
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK22(X1))
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK22(X1),sK23(X1))
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP4(X0)
| ~ p2(sK23(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK22(X1))
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK26(X1))
| ~ sP3(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK26(X1),sK27(X1))
| ~ sP3(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP3(X0)
| ~ p2(sK27(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK26(X1))
| ~ sP3(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_103,negated_conjecture,
! [X0: $i] :
( r1(sK32,sK33)
| ~ p5(X0)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_104,negated_conjecture,
! [X0: $i] :
( ~ p2(sK33)
| ~ p5(X0)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_105,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(X0,sK34(X0))
| ~ p5(X1)
| ~ r1(sK32,X1)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_106,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(sK34(X0),sK35(X0))
| ~ p5(X1)
| ~ r1(sK32,X1)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_107,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| ~ p5(X1)
| ~ p2(sK35(X0))
| ~ r1(sK32,X1)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_108,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X0)
| p2(sK34(X0))
| ~ p5(X1)
| ~ r1(sK32,X1)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_111,negated_conjecture,
! [X0: $i] :
( p3(X0)
| r1(X0,sK37(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_115,negated_conjecture,
! [X0: $i] :
( sP8(sK32)
| r1(X0,sK39(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_116,negated_conjecture,
! [X0: $i] :
( sP8(sK32)
| p5(sK39(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_123,negated_conjecture,
( sP7(sK32)
| r1(sK32,sK43) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_124,negated_conjecture,
( sP5(sK43)
| sP7(sK32)
| ~ p2(sK43) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_125,negated_conjecture,
! [X0: $i,X1: $i] :
( sP5(sK43)
| sP7(sK32)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK43,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_126,negated_conjecture,
! [X0: $i] :
( sP7(sK32)
| sP3(X0)
| sP4(X0)
| ~ p2(X0)
| ~ r1(sK43,X0) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_127,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP7(sK32)
| sP3(X0)
| sP4(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_153,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK54(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_154,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK54(X0))
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_155,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK32,X0)
| ~ r1(X1,X2)
| ~ r1(sK54(X0),X1) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_156,plain,
r1(sK32,sK32),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_159,plain,
( ~ sP8(sK32)
| ~ p2(sK9(sK32)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_162,plain,
( r1(sK32,sK9(sK32))
| ~ sP8(sK32) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_170,plain,
( sP8(sK32)
| p5(sK39(sK32))
| ~ r1(sK32,sK32) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_174,plain,
( sP6(sK32)
| ~ sP7(sK32)
| ~ p2(sK12(sK32)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_175,plain,
( sP6(sK32)
| r1(sK32,sK12(sK32))
| ~ sP7(sK32) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_180,plain,
( sP8(sK32)
| r1(sK32,sK39(sK32))
| ~ r1(sK32,sK32) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_292,plain,
! [X0: $i] :
( p2(sK9(X0))
| r1(sK9(X0),sK54(sK9(X0)))
| ~ r1(sK32,sK9(X0)) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_293,plain,
( p2(sK9(sK32))
| r1(sK9(sK32),sK54(sK9(sK32)))
| ~ r1(sK32,sK9(sK32)) ),
inference(instantiation,[status(thm)],[c_292]) ).
tcf(c_294,plain,
( p2(sK33)
| r1(sK33,sK54(sK33))
| ~ r1(sK32,sK33) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_403,plain,
! [X0: $i] :
( sP5(sK43)
| sP7(sK32)
| p2(X0)
| ~ p2(sK10(sK43))
| ~ r1(sK43,sK10(sK43))
| ~ r1(sK10(sK43),X0) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_477,plain,
( sP8(sK32)
| ~ p2(sK33)
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK32) ),
inference(superposition,[status(thm)],[c_115,c_104]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK54(X1))
| ~ sP6(X2)
| ~ r1(X2,X0)
| ~ p2(sK16(sK54(X1)))
| ~ r1(X0,sK54(X1)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_520,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK54(X1))
| p2(sK15(sK54(X1)))
| ~ sP6(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK54(X1)) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_530,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK54(X1))
| r1(sK54(X1),sK15(sK54(X1)))
| ~ sP6(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK54(X1)) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_540,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK54(X1))
| r1(sK15(sK54(X1)),sK16(sK54(X1)))
| ~ sP6(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK54(X1)) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_626,plain,
( p2(sK9(sK32))
| ~ sP8(sK32)
| ~ p2(sK54(sK9(sK32))) ),
inference(superposition,[status(thm)],[c_50,c_154]) ).
tcf(c_753,plain,
( sP8(sK32)
| p5(sK39(sK32)) ),
inference(resolution,[status(thm)],[c_49,c_116]) ).
tcf(c_1070,plain,
( sP8(sK32)
| r1(sK32,sK33)
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK32) ),
inference(resolution,[status(thm)],[c_103,c_115]) ).
tcf(c_1077,plain,
! [X0: $i,X1: $i] :
( p2(sK54(sK9(X0)))
| ~ sP6(X1)
| ~ r1(X1,sK9(X0))
| ~ p2(sK16(sK54(sK9(X0))))
| ~ r1(sK9(X0),sK54(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_1078,plain,
( p2(sK54(sK9(sK32)))
| ~ sP6(sK32)
| ~ r1(sK32,sK9(sK32))
| ~ p2(sK16(sK54(sK9(sK32))))
| ~ r1(sK9(sK32),sK54(sK9(sK32))) ),
inference(instantiation,[status(thm)],[c_1077]) ).
tcf(c_1110,plain,
! [X0: $i,X1: $i] :
( p2(sK54(sK9(X0)))
| p2(sK15(sK54(sK9(X0))))
| ~ sP6(X1)
| ~ r1(X1,sK9(X0))
| ~ r1(sK9(X0),sK54(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_520]) ).
tcf(c_1111,plain,
( p2(sK54(sK9(sK32)))
| p2(sK15(sK54(sK9(sK32))))
| ~ sP6(sK32)
| ~ r1(sK32,sK9(sK32))
| ~ r1(sK9(sK32),sK54(sK9(sK32))) ),
inference(instantiation,[status(thm)],[c_1110]) ).
tcf(c_1116,plain,
! [X0: $i,X1: $i] :
( p2(sK54(sK9(X0)))
| r1(sK54(sK9(X0)),sK15(sK54(sK9(X0))))
| ~ sP6(X1)
| ~ r1(X1,sK9(X0))
| ~ r1(sK9(X0),sK54(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_530]) ).
tcf(c_1117,plain,
( p2(sK54(sK9(sK32)))
| r1(sK54(sK9(sK32)),sK15(sK54(sK9(sK32))))
| ~ sP6(sK32)
| ~ r1(sK32,sK9(sK32))
| ~ r1(sK9(sK32),sK54(sK9(sK32))) ),
inference(instantiation,[status(thm)],[c_1116]) ).
tcf(c_1122,plain,
! [X0: $i,X1: $i] :
( p2(sK54(sK9(X0)))
| r1(sK15(sK54(sK9(X0))),sK16(sK54(sK9(X0))))
| ~ sP6(X1)
| ~ r1(X1,sK9(X0))
| ~ r1(sK9(X0),sK54(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_540]) ).
tcf(c_1123,plain,
( p2(sK54(sK9(sK32)))
| r1(sK15(sK54(sK9(sK32))),sK16(sK54(sK9(sK32))))
| ~ sP6(sK32)
| ~ r1(sK32,sK9(sK32))
| ~ r1(sK9(sK32),sK54(sK9(sK32))) ),
inference(instantiation,[status(thm)],[c_1122]) ).
tcf(c_1182,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| p2(sK34(X0))
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK32)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_108,c_115]) ).
tcf(c_1324,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(X0,sK34(X0))
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK32)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_105,c_115]) ).
tcf(c_1398,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| p2(sK10(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(superposition,[status(thm)],[c_56,c_55]) ).
tcf(c_1413,plain,
( sP7(sK32)
| p2(sK43)
| p2(sK10(sK43))
| ~ sP8(sK32) ),
inference(superposition,[status(thm)],[c_123,c_55]) ).
tcf(c_1465,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(sK34(X0),sK35(X0))
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK32)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_106,c_115]) ).
tcf(c_1483,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK9(X0))
| ~ r1(sK32,sK9(X0))
| ~ p2(sK15(sK54(sK9(X0))))
| ~ r1(sK15(sK54(sK9(X0))),X1)
| ~ r1(sK54(sK9(X0)),sK15(sK54(sK9(X0)))) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_1533,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(sK34(X0),sK35(X0))
| ~ r1(sK32,sK32)
| ~ r1(sK32,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1465,c_753]) ).
tcf(c_1534,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| p2(sK34(X0))
| ~ r1(sK32,sK32)
| ~ r1(sK32,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1182,c_753]) ).
tcf(c_1535,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(X0,sK34(X0))
| ~ r1(sK32,sK32)
| ~ r1(sK32,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1324,c_753]) ).
tcf(c_1536,plain,
( sP8(sK32)
| r1(sK32,sK33)
| ~ r1(sK32,sK32) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1070,c_753]) ).
tcf(c_2105,plain,
( sP8(sK32)
| r1(sK32,sK33) ),
inference(global_subsumption_just,[status(thm)],[c_1536,c_156,c_1536]) ).
tcf(c_2117,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| p2(sK34(X0))
| ~ p5(sK33)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_2105,c_108]) ).
tcf(c_2118,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(X0,sK34(X0))
| ~ p5(sK33)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_2105,c_105]) ).
tcf(c_2119,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(sK34(X0),sK35(X0))
| ~ p5(sK33)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_2105,c_106]) ).
tcf(c_2138,plain,
! [X0: $i] :
( p2(X0)
| p2(sK54(X0))
| p2(sK19(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(superposition,[status(thm)],[c_153,c_74]) ).
tcf(c_2192,plain,
! [X0: $i,X1: $i] :
( p2(sK9(X0))
| p2(sK16(sK54(sK9(X1))))
| ~ r1(sK32,sK9(X0))
| ~ p2(sK15(sK54(sK9(X0))))
| ~ r1(sK54(sK9(X0)),sK15(sK54(sK9(X0))))
| ~ r1(sK15(sK54(sK9(X0))),sK16(sK54(sK9(X1)))) ),
inference(instantiation,[status(thm)],[c_1483]) ).
tcf(c_2193,plain,
( p2(sK9(sK32))
| p2(sK16(sK54(sK9(sK32))))
| ~ r1(sK32,sK9(sK32))
| ~ p2(sK15(sK54(sK9(sK32))))
| ~ r1(sK54(sK9(sK32)),sK15(sK54(sK9(sK32))))
| ~ r1(sK15(sK54(sK9(sK32))),sK16(sK54(sK9(sK32)))) ),
inference(instantiation,[status(thm)],[c_2192]) ).
tcf(c_2198,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| p2(sK34(X0))
| ~ r1(sK32,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2117,c_156,c_1534]) ).
tcf(c_2223,plain,
( sP7(sK32)
| p2(sK43)
| sP8(sK32)
| p2(sK34(sK43)) ),
inference(resolution,[status(thm)],[c_2198,c_123]) ).
tcf(c_2336,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK34(X1),sK35(X1))
| ~ p5(sK39(X0))
| ~ r1(sK32,X1)
| ~ r1(sK32,sK39(X0)) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_2337,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK34(X1))
| ~ p5(sK39(X0))
| ~ r1(sK32,X1)
| ~ r1(sK32,sK39(X0)) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_2339,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ p5(sK39(X0))
| ~ p2(sK35(X1))
| ~ r1(sK32,X1)
| ~ r1(sK32,sK39(X0)) ),
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_2528,plain,
! [X0: $i] :
( p2(sK54(sK33))
| r1(sK15(sK54(sK33)),sK16(sK54(sK33)))
| ~ sP6(X0)
| ~ r1(X0,sK33)
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_540]) ).
tcf(c_2529,plain,
! [X0: $i] :
( p2(sK54(sK33))
| r1(sK54(sK33),sK15(sK54(sK33)))
| ~ sP6(X0)
| ~ r1(X0,sK33)
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_530]) ).
tcf(c_2530,plain,
! [X0: $i] :
( p2(sK54(sK33))
| p2(sK15(sK54(sK33)))
| ~ sP6(X0)
| ~ r1(X0,sK33)
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_520]) ).
tcf(c_2531,plain,
! [X0: $i] :
( p2(sK54(sK33))
| ~ sP6(X0)
| ~ r1(X0,sK33)
| ~ p2(sK16(sK54(sK33)))
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_2533,plain,
( p2(sK54(sK33))
| ~ sP6(sK32)
| ~ r1(sK32,sK33)
| ~ p2(sK16(sK54(sK33)))
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_2531]) ).
tcf(c_2534,plain,
( p2(sK54(sK33))
| p2(sK15(sK54(sK33)))
| ~ sP6(sK32)
| ~ r1(sK32,sK33)
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_2530]) ).
tcf(c_2535,plain,
( p2(sK54(sK33))
| r1(sK54(sK33),sK15(sK54(sK33)))
| ~ sP6(sK32)
| ~ r1(sK32,sK33)
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_2529]) ).
tcf(c_2536,plain,
( p2(sK54(sK33))
| r1(sK15(sK54(sK33)),sK16(sK54(sK33)))
| ~ sP6(sK32)
| ~ r1(sK32,sK33)
| ~ r1(sK33,sK54(sK33)) ),
inference(instantiation,[status(thm)],[c_2528]) ).
tcf(c_2724,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(X0,sK34(X0))
| ~ r1(sK32,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2118,c_156,c_1535]) ).
tcf(c_2749,plain,
! [X0: $i] :
( sP5(sK43)
| sP7(sK32)
| p2(sK43)
| sP8(sK32)
| p2(X0)
| ~ p2(sK34(sK43))
| ~ r1(sK32,sK43)
| ~ r1(sK34(sK43),X0) ),
inference(resolution,[status(thm)],[c_2724,c_125]) ).
tcf(c_2924,plain,
! [X0: $i,X1: $i] :
( p2(sK12(X0))
| ~ p5(sK39(X1))
| ~ p2(sK35(sK12(X0)))
| ~ r1(sK32,sK39(X1))
| ~ r1(sK32,sK12(X0)) ),
inference(instantiation,[status(thm)],[c_2339]) ).
tcf(c_2925,plain,
( p2(sK12(sK32))
| ~ p5(sK39(sK32))
| ~ p2(sK35(sK12(sK32)))
| ~ r1(sK32,sK39(sK32))
| ~ r1(sK32,sK12(sK32)) ),
inference(instantiation,[status(thm)],[c_2924]) ).
tcf(c_2928,plain,
! [X0: $i] :
( p2(sK43)
| ~ p2(sK35(sK43))
| ~ r1(sK32,sK43)
| ~ p5(sK39(X0))
| ~ r1(sK32,sK39(X0)) ),
inference(instantiation,[status(thm)],[c_2339]) ).
tcf(c_2929,plain,
( p2(sK43)
| ~ p5(sK39(sK32))
| ~ p2(sK35(sK43))
| ~ r1(sK32,sK43)
| ~ r1(sK32,sK39(sK32)) ),
inference(instantiation,[status(thm)],[c_2928]) ).
tcf(c_2994,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| r1(sK34(X0),sK35(X0))
| ~ r1(sK32,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2119,c_156,c_1533]) ).
tcf(c_3321,plain,
! [X0: $i,X1: $i] :
( p2(sK12(X0))
| r1(sK12(X0),sK34(sK12(X0)))
| ~ p5(sK39(X1))
| ~ r1(sK32,sK39(X1))
| ~ r1(sK32,sK12(X0)) ),
inference(instantiation,[status(thm)],[c_2337]) ).
tcf(c_3322,plain,
( p2(sK12(sK32))
| r1(sK12(sK32),sK34(sK12(sK32)))
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK39(sK32))
| ~ r1(sK32,sK12(sK32)) ),
inference(instantiation,[status(thm)],[c_3321]) ).
tcf(c_3339,plain,
! [X0: $i,X1: $i] :
( p2(sK12(X0))
| r1(sK34(sK12(X0)),sK35(sK12(X0)))
| ~ p5(sK39(X1))
| ~ r1(sK32,sK39(X1))
| ~ r1(sK32,sK12(X0)) ),
inference(instantiation,[status(thm)],[c_2336]) ).
tcf(c_3340,plain,
( p2(sK12(sK32))
| r1(sK34(sK12(sK32)),sK35(sK12(sK32)))
| ~ p5(sK39(sK32))
| ~ r1(sK32,sK39(sK32))
| ~ r1(sK32,sK12(sK32)) ),
inference(instantiation,[status(thm)],[c_3339]) ).
tcf(c_3674,plain,
! [X0: $i] :
( p2(sK18(X0))
| p2(sK26(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(superposition,[status(thm)],[c_68,c_89]) ).
tcf(c_3767,plain,
! [X0: $i] :
( p2(sK33)
| p2(X0)
| ~ r1(sK32,sK33)
| ~ p2(sK15(sK54(sK33)))
| ~ r1(sK15(sK54(sK33)),X0)
| ~ r1(sK54(sK33),sK15(sK54(sK33))) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_3946,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| r1(sK12(X0),sK10(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(superposition,[status(thm)],[c_56,c_52]) ).
tcf(c_3964,plain,
( sP7(sK32)
| p2(sK43)
| r1(sK43,sK10(sK43))
| ~ sP8(sK32) ),
inference(superposition,[status(thm)],[c_123,c_52]) ).
tcf(c_4051,plain,
( p2(sK33)
| p2(sK16(sK54(sK33)))
| ~ r1(sK32,sK33)
| ~ p2(sK15(sK54(sK33)))
| ~ r1(sK54(sK33),sK15(sK54(sK33)))
| ~ r1(sK15(sK54(sK33)),sK16(sK54(sK33))) ),
inference(instantiation,[status(thm)],[c_3767]) ).
tcf(c_4075,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| ~ sP7(X0)
| ~ sP8(X0)
| ~ p2(sK11(sK12(X0))) ),
inference(superposition,[status(thm)],[c_56,c_54]) ).
tcf(c_4093,plain,
( sP7(sK32)
| p2(sK43)
| ~ sP8(sK32)
| ~ p2(sK11(sK43)) ),
inference(superposition,[status(thm)],[c_123,c_54]) ).
tcf(c_4101,plain,
( sP6(sK32)
| p2(sK12(sK32))
| ~ sP7(sK32)
| ~ sP8(sK32)
| ~ p2(sK11(sK12(sK32))) ),
inference(instantiation,[status(thm)],[c_4075]) ).
tcf(c_4142,plain,
( p2(sK33)
| ~ p2(sK54(sK33))
| ~ r1(sK32,sK33) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_4392,plain,
! [X0: $i] :
( p2(X0)
| p2(sK54(X0))
| r1(sK54(X0),sK19(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(superposition,[status(thm)],[c_153,c_71]) ).
tcf(c_4512,plain,
! [X0: $i,X1: $i] :
( sP6(X0)
| p2(X1)
| ~ sP7(X0)
| ~ p2(sK34(sK12(X0)))
| ~ r1(sK34(sK12(X0)),X1)
| ~ r1(sK12(X0),sK34(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_4589,plain,
! [X0: $i] :
( p2(X0)
| p2(sK54(X0))
| ~ sP5(X0)
| ~ r1(sK32,X0)
| ~ p2(sK20(sK54(X0))) ),
inference(superposition,[status(thm)],[c_153,c_73]) ).
tcf(c_4659,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK35(sK12(X0)))
| ~ sP7(X0)
| ~ p2(sK34(sK12(X0)))
| ~ r1(sK12(X0),sK34(sK12(X0)))
| ~ r1(sK34(sK12(X0)),sK35(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_4512]) ).
tcf(c_4660,plain,
( sP6(sK32)
| p2(sK35(sK12(sK32)))
| ~ sP7(sK32)
| ~ p2(sK34(sK12(sK32)))
| ~ r1(sK12(sK32),sK34(sK12(sK32)))
| ~ r1(sK34(sK12(sK32)),sK35(sK12(sK32))) ),
inference(instantiation,[status(thm)],[c_4659]) ).
tcf(c_4662,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP5(sK43)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK18(sK43),X0) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_4663,plain,
! [X0: $i] :
( p2(X0)
| r1(sK19(X0),sK20(X0))
| ~ sP5(sK43)
| ~ r1(sK43,X0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_4664,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK19(X0))
| ~ sP5(sK43)
| ~ r1(sK43,X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_4665,plain,
! [X0: $i] :
( p2(X0)
| p2(sK19(X0))
| ~ sP5(sK43)
| ~ r1(sK43,X0) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_4666,plain,
! [X0: $i] :
( p2(X0)
| ~ sP5(sK43)
| ~ p2(sK20(X0))
| ~ r1(sK43,X0) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_4667,plain,
( r1(sK17(sK43),sK18(sK43))
| ~ sP5(sK43) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_4668,plain,
( r1(sK43,sK17(sK43))
| ~ sP5(sK43) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_4669,plain,
( ~ sP5(sK43)
| ~ p2(sK18(sK43)) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_4995,plain,
! [X0: $i,X1: $i] :
( sP7(sK32)
| p2(X1)
| sP3(sK17(sK43))
| sP4(sK17(sK43))
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK43,sK17(sK43))
| ~ r1(sK17(sK43),X0) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_4997,plain,
( sP7(sK32)
| sP3(sK17(sK43))
| sP4(sK17(sK43))
| ~ p2(sK17(sK43))
| ~ r1(sK43,sK17(sK43)) ),
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_5118,plain,
( p2(sK17(sK43))
| p2(sK19(sK17(sK43)))
| ~ sP5(sK43)
| ~ r1(sK43,sK17(sK43)) ),
inference(instantiation,[status(thm)],[c_4665]) ).
tcf(c_5175,plain,
( p2(sK17(sK43))
| r1(sK17(sK43),sK19(sK17(sK43)))
| ~ sP5(sK43)
| ~ r1(sK43,sK17(sK43)) ),
inference(instantiation,[status(thm)],[c_4664]) ).
tcf(c_5200,plain,
( p2(sK17(sK43))
| ~ sP5(sK43)
| ~ p2(sK20(sK17(sK43)))
| ~ r1(sK43,sK17(sK43)) ),
inference(instantiation,[status(thm)],[c_4666]) ).
tcf(c_5209,plain,
( p2(sK17(sK43))
| r1(sK19(sK17(sK43)),sK20(sK17(sK43)))
| ~ sP5(sK43)
| ~ r1(sK43,sK17(sK43)) ),
inference(instantiation,[status(thm)],[c_4663]) ).
tcf(c_5599,plain,
! [X0: $i] :
( sP5(sK43)
| sP7(sK32)
| ~ r1(sK34(sK43),X0)
| p2(X0)
| sP8(sK32) ),
inference(global_subsumption_just,[status(thm)],[c_2749,c_123,c_124,c_2223,c_2749]) ).
tcf(c_5600,plain,
! [X0: $i] :
( sP5(sK43)
| sP7(sK32)
| sP8(sK32)
| p2(X0)
| ~ r1(sK34(sK43),X0) ),
inference(renaming,[status(thm)],[c_5599]) ).
tcf(c_5625,plain,
( sP5(sK43)
| sP7(sK32)
| p2(sK43)
| sP8(sK32)
| p2(sK35(sK43))
| ~ r1(sK32,sK43) ),
inference(resolution,[status(thm)],[c_5600,c_2994]) ).
tcf(c_5627,plain,
( sP5(sK43)
| sP7(sK32)
| sP8(sK32)
| p2(sK39(sK34(sK43)))
| ~ r1(sK32,sK34(sK43)) ),
inference(resolution,[status(thm)],[c_5600,c_115]) ).
tcf(c_5647,plain,
( sP5(sK43)
| sP7(sK32)
| sP8(sK32) ),
inference(global_subsumption_just,[status(thm)],[c_5627,c_156,c_123,c_124,c_170,c_180,c_2929,c_5625]) ).
tcf(c_5712,plain,
! [X0: $i,X1: $i] :
( sP7(sK32)
| p2(X1)
| sP3(sK17(sK43))
| sP4(sK17(sK43))
| ~ sP5(sK43)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK17(sK43),X0) ),
inference(resolution,[status(thm)],[c_67,c_127]) ).
tcf(c_5763,plain,
! [X0: $i] :
( p2(sK18(X0))
| r1(sK18(X0),sK26(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(superposition,[status(thm)],[c_68,c_86]) ).
tcf(c_5830,plain,
! [X0: $i] :
( p2(sK18(X0))
| p2(sK26(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(resolution,[status(thm)],[c_68,c_89]) ).
tcf(c_5831,plain,
! [X0: $i] :
( p2(sK18(X0))
| r1(sK18(X0),sK26(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(resolution,[status(thm)],[c_68,c_86]) ).
tcf(c_5832,plain,
! [X0: $i] :
( p2(sK18(X0))
| r1(sK26(sK18(X0)),sK27(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(resolution,[status(thm)],[c_68,c_87]) ).
tcf(c_5883,plain,
! [X0: $i] :
( p2(X0)
| r1(sK22(X0),sK23(X0))
| ~ sP4(sK17(sK43))
| ~ r1(sK17(sK43),X0) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_5884,plain,
! [X0: $i] :
( p2(X0)
| r1(X0,sK22(X0))
| ~ sP4(sK17(sK43))
| ~ r1(sK17(sK43),X0) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_5886,plain,
! [X0: $i] :
( p2(X0)
| p2(sK22(X0))
| ~ sP4(sK17(sK43))
| ~ r1(sK17(sK43),X0) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_5887,plain,
! [X0: $i] :
( p2(X0)
| ~ sP4(sK17(sK43))
| ~ p2(sK23(X0))
| ~ r1(sK17(sK43),X0) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_6460,plain,
! [X0: $i] :
( p2(sK18(X0))
| ~ sP5(X0)
| ~ sP3(sK17(X0))
| ~ p2(sK27(sK18(X0))) ),
inference(superposition,[status(thm)],[c_68,c_88]) ).
tcf(c_6537,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| r1(sK10(sK12(X0)),sK11(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(superposition,[status(thm)],[c_56,c_53]) ).
tcf(c_6555,plain,
( sP7(sK32)
| p2(sK43)
| r1(sK10(sK43),sK11(sK43))
| ~ sP8(sK32) ),
inference(superposition,[status(thm)],[c_123,c_53]) ).
tcf(c_6663,plain,
! [X0: $i] :
( p2(X0)
| p2(sK54(X0))
| r1(sK19(sK54(X0)),sK20(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(superposition,[status(thm)],[c_153,c_72]) ).
tcf(c_6705,plain,
! [X0: $i] :
( p2(X0)
| p2(sK54(X0))
| r1(sK54(X0),sK19(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_71,c_153]) ).
tcf(c_6999,plain,
( p2(sK18(sK43))
| p2(sK22(sK18(sK43)))
| ~ sP4(sK17(sK43))
| ~ r1(sK17(sK43),sK18(sK43)) ),
inference(instantiation,[status(thm)],[c_5886]) ).
tcf(c_7028,plain,
( p2(sK18(sK43))
| ~ sP4(sK17(sK43))
| ~ p2(sK23(sK18(sK43)))
| ~ r1(sK17(sK43),sK18(sK43)) ),
inference(instantiation,[status(thm)],[c_5887]) ).
tcf(c_7046,plain,
( p2(sK18(sK43))
| r1(sK18(sK43),sK22(sK18(sK43)))
| ~ sP4(sK17(sK43))
| ~ r1(sK17(sK43),sK18(sK43)) ),
inference(instantiation,[status(thm)],[c_5884]) ).
tcf(c_7055,plain,
( p2(sK18(sK43))
| r1(sK22(sK18(sK43)),sK23(sK18(sK43)))
| ~ sP4(sK17(sK43))
| ~ r1(sK17(sK43),sK18(sK43)) ),
inference(instantiation,[status(thm)],[c_5883]) ).
tcf(c_7084,plain,
! [X0: $i] :
( p2(X0)
| p2(sK54(X0))
| r1(sK19(sK54(X0)),sK20(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_72,c_153]) ).
tcf(c_7346,plain,
! [X0: $i] :
( sP7(sK32)
| p2(X0)
| sP3(sK17(sK43))
| sP4(sK17(sK43))
| ~ p2(sK19(sK17(sK43)))
| ~ r1(sK43,sK17(sK43))
| ~ r1(sK19(sK17(sK43)),X0)
| ~ r1(sK17(sK43),sK19(sK17(sK43))) ),
inference(instantiation,[status(thm)],[c_4995]) ).
tcf(c_8279,plain,
( sP7(sK32)
| sP3(sK17(sK43))
| sP4(sK17(sK43))
| p2(sK20(sK17(sK43)))
| ~ p2(sK19(sK17(sK43)))
| ~ r1(sK43,sK17(sK43))
| ~ r1(sK17(sK43),sK19(sK17(sK43)))
| ~ r1(sK19(sK17(sK43)),sK20(sK17(sK43))) ),
inference(instantiation,[status(thm)],[c_7346]) ).
tcf(c_8464,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK32,X0)
| ~ sP5(X0)
| r1(sK54(X0),sK19(sK54(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_6705,c_154,c_4392]) ).
tcf(c_8465,plain,
! [X0: $i] :
( p2(X0)
| r1(sK54(X0),sK19(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(renaming,[status(thm)],[c_8464]) ).
tcf(c_8570,plain,
! [X0: $i] :
( ~ sP3(sK17(X0))
| ~ sP5(X0)
| p2(sK26(sK18(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_5830,c_69,c_3674]) ).
tcf(c_8571,plain,
! [X0: $i] :
( p2(sK26(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(renaming,[status(thm)],[c_8570]) ).
tcf(c_8593,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP5(X0)
| ~ r1(sK32,X0)
| ~ p2(sK19(sK54(X0)))
| ~ r1(sK19(sK54(X0)),X1) ),
inference(resolution,[status(thm)],[c_8465,c_155]) ).
tcf(c_8931,plain,
! [X0: $i] :
( p2(X0)
| ~ sP5(sK43)
| ~ p2(sK22(sK18(sK43)))
| ~ r1(sK22(sK18(sK43)),X0)
| ~ r1(sK18(sK43),sK22(sK18(sK43))) ),
inference(instantiation,[status(thm)],[c_4662]) ).
tcf(c_8936,plain,
! [X0: $i] :
( p2(X0)
| ~ r1(sK32,X0)
| ~ sP5(X0)
| r1(sK19(sK54(X0)),sK20(sK54(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_7084,c_154,c_6663]) ).
tcf(c_8937,plain,
! [X0: $i] :
( p2(X0)
| r1(sK19(sK54(X0)),sK20(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(renaming,[status(thm)],[c_8936]) ).
tcf(c_9066,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ sP5(X0)
| ~ r1(sK32,X0)
| ~ r1(sK19(sK54(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_8593,c_154,c_2138,c_8593]) ).
tcf(c_9097,plain,
! [X0: $i] :
( sP8(sK32)
| p2(X0)
| p2(sK39(sK19(sK54(X0))))
| ~ sP5(X0)
| ~ r1(sK32,X0)
| ~ r1(sK32,sK19(sK54(X0))) ),
inference(resolution,[status(thm)],[c_9066,c_115]) ).
tcf(c_9106,plain,
! [X0: $i] :
( p2(X0)
| p2(sK20(sK54(X0)))
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(resolution,[status(thm)],[c_9066,c_8937]) ).
tcf(c_9225,plain,
( p2(sK23(sK18(sK43)))
| ~ sP5(sK43)
| ~ p2(sK22(sK18(sK43)))
| ~ r1(sK18(sK43),sK22(sK18(sK43)))
| ~ r1(sK22(sK18(sK43)),sK23(sK18(sK43))) ),
inference(instantiation,[status(thm)],[c_8931]) ).
tcf(c_9590,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ r1(sK32,X0)
| p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_9097,c_154,c_4589,c_9106]) ).
tcf(c_9591,plain,
! [X0: $i] :
( p2(X0)
| ~ sP5(X0)
| ~ r1(sK32,X0) ),
inference(renaming,[status(thm)],[c_9590]) ).
tcf(c_9622,plain,
( sP7(sK32)
| p2(sK43)
| ~ sP5(sK43) ),
inference(resolution,[status(thm)],[c_9591,c_123]) ).
tcf(c_9653,plain,
( sP7(sK32)
| p2(sK43)
| sP8(sK32) ),
inference(resolution,[status(thm)],[c_9622,c_5647]) ).
tcf(c_9724,plain,
! [X0: $i] :
( ~ sP3(sK17(X0))
| ~ sP5(X0)
| r1(sK18(X0),sK26(sK18(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_5831,c_69,c_5763]) ).
tcf(c_9725,plain,
! [X0: $i] :
( r1(sK18(X0),sK26(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(renaming,[status(thm)],[c_9724]) ).
tcf(c_9771,plain,
! [X0: $i] :
( ~ sP3(sK17(X0))
| ~ sP5(X0)
| r1(sK26(sK18(X0)),sK27(sK18(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_5832,c_69,c_5832]) ).
tcf(c_9772,plain,
! [X0: $i] :
( r1(sK26(sK18(X0)),sK27(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(renaming,[status(thm)],[c_9771]) ).
tcf(c_10215,plain,
( sP7(sK32)
| ~ sP5(sK43)
| sP4(sK17(sK43))
| sP3(sK17(sK43)) ),
inference(global_subsumption_just,[status(thm)],[c_5712,c_4668,c_4997,c_5118,c_5175,c_5200,c_5209,c_8279]) ).
tcf(c_10216,plain,
( sP7(sK32)
| sP3(sK17(sK43))
| sP4(sK17(sK43))
| ~ sP5(sK43) ),
inference(renaming,[status(thm)],[c_10215]) ).
tcf(c_10217,plain,
( sP7(sK32)
| sP3(sK17(sK43))
| ~ sP5(sK43) ),
inference(global_subsumption_just,[status(thm)],[c_10216,c_4669,c_4667,c_6999,c_7028,c_7046,c_7055,c_9225,c_10216]) ).
tcf(c_11577,plain,
( sP6(sK32)
| sP8(sK32)
| p5(sK39(sK12(sK32)))
| ~ sP7(sK32) ),
inference(resolution,[status(thm)],[c_56,c_116]) ).
tcf(c_11579,plain,
( sP6(sK32)
| sP8(sK32)
| p2(sK12(sK32))
| p2(sK34(sK12(sK32)))
| ~ sP7(sK32) ),
inference(resolution,[status(thm)],[c_56,c_2198]) ).
tcf(c_12174,plain,
( sP6(sK32)
| sP8(sK32)
| ~ sP7(sK32) ),
inference(global_subsumption_just,[status(thm)],[c_11577,c_156,c_170,c_174,c_175,c_180,c_294,c_477,c_1536,c_2533,c_2534,c_2535,c_2536,c_2925,c_3322,c_3340,c_4051,c_4142,c_4660,c_11579]) ).
tcf(c_12176,plain,
( ~ sP7(sK32)
| sP8(sK32) ),
inference(global_subsumption_just,[status(thm)],[c_12174,c_156,c_170,c_294,c_477,c_1536,c_2533,c_2534,c_2535,c_2536,c_4051,c_4142,c_12174]) ).
tcf(c_12177,plain,
( sP8(sK32)
| ~ sP7(sK32) ),
inference(renaming,[status(thm)],[c_12176]) ).
tcf(c_12186,plain,
( p2(sK43)
| sP8(sK32) ),
inference(backward_subsumption_resolution,[status(thm)],[c_9653,c_12177]) ).
tcf(c_12208,plain,
( sP5(sK43)
| sP8(sK32) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5647,c_12177]) ).
tcf(c_13015,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP5(X0)
| ~ sP3(sK17(X0))
| ~ p2(sK26(sK18(X0)))
| ~ r1(sK26(sK18(X0)),X1) ),
inference(resolution,[status(thm)],[c_9725,c_70]) ).
tcf(c_15736,plain,
! [X0: $i] :
( p2(sK18(X0))
| ~ sP5(X0)
| ~ sP3(sK17(X0))
| ~ p2(sK27(sK18(X0))) ),
inference(resolution,[status(thm)],[c_88,c_68]) ).
tcf(c_16008,plain,
! [X0: $i] :
( ~ p2(sK27(sK18(X0)))
| ~ sP3(sK17(X0))
| ~ sP5(X0) ),
inference(global_subsumption_just,[status(thm)],[c_15736,c_69,c_6460]) ).
tcf(c_16009,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ sP3(sK17(X0))
| ~ p2(sK27(sK18(X0))) ),
inference(renaming,[status(thm)],[c_16008]) ).
tcf(c_18036,plain,
( sP7(sK32)
| p2(sK43)
| p2(sK10(sK43)) ),
inference(global_subsumption_just,[status(thm)],[c_1413,c_1413,c_12186]) ).
tcf(c_19988,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP5(X0)
| ~ sP3(sK17(X0))
| ~ r1(sK26(sK18(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_13015,c_8571,c_13015]) ).
tcf(c_20017,plain,
! [X0: $i] :
( sP8(sK32)
| p2(sK39(sK26(sK18(X0))))
| ~ sP5(X0)
| ~ sP3(sK17(X0))
| ~ r1(sK32,sK26(sK18(X0))) ),
inference(resolution,[status(thm)],[c_19988,c_115]) ).
tcf(c_20026,plain,
! [X0: $i] :
( p2(sK27(sK18(X0)))
| ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(resolution,[status(thm)],[c_19988,c_9772]) ).
tcf(c_20028,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ sP3(sK17(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_20017,c_16009,c_20026]) ).
tcf(c_20038,plain,
( sP7(sK32)
| ~ sP5(sK43) ),
inference(backward_subsumption_resolution,[status(thm)],[c_10217,c_20028]) ).
tcf(c_20043,plain,
( sP7(sK32)
| ~ p2(sK43) ),
inference(backward_subsumption_resolution,[status(thm)],[c_124,c_20038]) ).
tcf(c_20045,plain,
! [X0: $i,X1: $i] :
( sP7(sK32)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK43,X0)
| ~ r1(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_125,c_20038]) ).
tcf(c_20053,plain,
( sP7(sK32)
| sP8(sK32) ),
inference(resolution,[status(thm)],[c_20038,c_12208]) ).
tcf(c_20082,plain,
sP8(sK32),
inference(global_subsumption_just,[status(thm)],[c_12177,c_12177,c_20053]) ).
tcf(c_20128,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| p2(sK10(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(resolution,[status(thm)],[c_55,c_56]) ).
tcf(c_20141,plain,
( sP7(sK32)
| p2(sK43)
| p2(sK10(sK43))
| ~ sP8(sK32) ),
inference(resolution,[status(thm)],[c_55,c_123]) ).
tcf(c_20198,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| r1(sK12(X0),sK10(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(resolution,[status(thm)],[c_52,c_56]) ).
tcf(c_20211,plain,
( sP7(sK32)
| p2(sK43)
| r1(sK43,sK10(sK43))
| ~ sP8(sK32) ),
inference(resolution,[status(thm)],[c_52,c_123]) ).
tcf(c_20268,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK12(X0))
| r1(sK10(sK12(X0)),sK11(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(resolution,[status(thm)],[c_53,c_56]) ).
tcf(c_20281,plain,
( sP7(sK32)
| p2(sK43)
| r1(sK10(sK43),sK11(sK43))
| ~ sP8(sK32) ),
inference(resolution,[status(thm)],[c_53,c_123]) ).
tcf(c_20406,plain,
( sP7(sK32)
| p2(sK10(sK43)) ),
inference(global_subsumption_just,[status(thm)],[c_20141,c_18036,c_20043]) ).
tcf(c_21093,plain,
( sP7(sK32)
| r1(sK43,sK10(sK43)) ),
inference(global_subsumption_just,[status(thm)],[c_20211,c_3964,c_20043,c_20082]) ).
tcf(c_21116,plain,
( sP7(sK32)
| r1(sK10(sK43),sK11(sK43)) ),
inference(global_subsumption_just,[status(thm)],[c_20281,c_6555,c_12177,c_20043,c_20053]) ).
tcf(c_21176,plain,
! [X0: $i] :
( sP7(sK32)
| p2(X0)
| ~ p2(sK10(sK43))
| ~ r1(sK10(sK43),X0) ),
inference(resolution,[status(thm)],[c_20045,c_21093]) ).
tcf(c_22062,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP8(X0)
| ~ sP7(X0)
| p2(sK10(sK12(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_20128,c_57,c_1398]) ).
tcf(c_22063,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK10(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(renaming,[status(thm)],[c_22062]) ).
tcf(c_22523,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP8(X0)
| ~ sP7(X0)
| r1(sK12(X0),sK10(sK12(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_20198,c_57,c_3946]) ).
tcf(c_22524,plain,
! [X0: $i] :
( sP6(X0)
| r1(sK12(X0),sK10(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(renaming,[status(thm)],[c_22523]) ).
tcf(c_22666,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP8(X0)
| ~ sP7(X0)
| r1(sK10(sK12(X0)),sK11(sK12(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_20268,c_57,c_6537]) ).
tcf(c_22667,plain,
! [X0: $i] :
( sP6(X0)
| r1(sK10(sK12(X0)),sK11(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(renaming,[status(thm)],[c_22666]) ).
tcf(c_22707,plain,
! [X0: $i] :
( sP7(sK32)
| p2(X0)
| ~ r1(sK10(sK43),X0) ),
inference(global_subsumption_just,[status(thm)],[c_21176,c_403,c_20038,c_20406,c_21093]) ).
tcf(c_22727,plain,
( sP7(sK32)
| p3(sK10(sK43))
| p2(sK37(sK10(sK43)))
| ~ r1(sK32,sK10(sK43)) ),
inference(resolution,[status(thm)],[c_22707,c_111]) ).
tcf(c_22730,plain,
( sP7(sK32)
| p2(sK11(sK43)) ),
inference(resolution,[status(thm)],[c_22707,c_21116]) ).
tcf(c_22735,plain,
sP7(sK32),
inference(global_subsumption_just,[status(thm)],[c_22727,c_4093,c_20043,c_20082,c_22730]) ).
tcf(c_23297,plain,
! [X0: $i,X1: $i] :
( sP6(X0)
| p2(X1)
| ~ sP7(X0)
| ~ sP8(X0)
| ~ p2(sK10(sK12(X0)))
| ~ r1(sK10(sK12(X0)),X1) ),
inference(resolution,[status(thm)],[c_22524,c_58]) ).
tcf(c_25499,plain,
! [X0: $i,X1: $i] :
( sP6(X0)
| p2(X1)
| ~ sP7(X0)
| ~ sP8(X0)
| ~ r1(sK10(sK12(X0)),X1) ),
inference(global_subsumption_just,[status(thm)],[c_23297,c_22063,c_23297]) ).
tcf(c_25537,plain,
! [X0: $i] :
( sP6(X0)
| p2(sK11(sK12(X0)))
| ~ sP7(X0)
| ~ sP8(X0) ),
inference(resolution,[status(thm)],[c_25499,c_22667]) ).
tcf(c_25538,plain,
( sP6(sK32)
| p2(sK11(sK12(sK32)))
| ~ sP7(sK32)
| ~ sP8(sK32) ),
inference(instantiation,[status(thm)],[c_25537]) ).
tcf(c_25539,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_25538,c_22735,c_20082,c_4101,c_2193,c_1123,c_1117,c_1111,c_1078,c_626,c_293,c_174,c_162,c_159]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL660+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 00:10:07 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 26.27/4.20 % SZS status Started for theBenchmark.p
% 26.27/4.20 % SZS status Theorem for theBenchmark.p
% 26.27/4.20
% 26.27/4.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.27/4.20
% 26.27/4.20 % ------ iProver source info
% 26.27/4.20
% 26.27/4.20 % git: date: 2026-07-19 20:42:38 +0200
% 26.27/4.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.27/4.20 % git: non_committed_changes: false
% 26.27/4.20
% 26.27/4.20 % ------ Parsing...
% 26.27/4.20 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.27/4.20
% 26.27/4.20 % ------ Preprocessing... sf_s rm: 36 0s sf_e sf_s rm: 0 0s sf_e %
% 26.27/4.20
% 26.27/4.20 % ------ Preprocessing...
% 26.27/4.20 % ------ Proving...
% 26.27/4.20 % ------ Problem Properties
% 26.27/4.20
% 26.27/4.20 %
% 26.27/4.20 % clauses 71
% 26.27/4.20 % conjectures 29
% 26.27/4.20 % EPR 12
% 26.27/4.20 % Horn 30
% 26.27/4.20 % unary 5
% 26.27/4.20 % binary 9
% 26.27/4.20 % lits 260
% 26.27/4.20 % lits eq 0
% 26.27/4.20 % fd_pure 0
% 26.27/4.20 % fd_pseudo 0
% 26.27/4.20 % fd_cond 0
% 26.27/4.20 % fd_pseudo_cond 0
% 26.27/4.20 % AC symbols 0
% 26.27/4.20
% 26.27/4.20 % ------ Input Options Time Limit: Unbounded
% 26.27/4.20
% 26.27/4.20
% 26.27/4.20 % ------
% 26.27/4.20 % Current options:
% 26.27/4.20 % ------
% 26.27/4.20
% 26.27/4.20
% 26.27/4.20 %
% 26.27/4.20
% 26.27/4.20 % ------ Proving...
% 26.27/4.20 %
% 26.27/4.20
% 26.27/4.20 % SZS status Theorem for theBenchmark.p
% 26.27/4.20
% 26.27/4.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.28/4.20
% 26.28/4.20
%------------------------------------------------------------------------------