%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL676+1.010 : 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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:08:04 PM UTC 2026
% Result : Theorem 31.18s 5.34s
% Output : CNFRefutation 31.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f33ERROR: Could not build tree for root c_42871ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X1,X2)
& r1(X0,X1) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
fof(f8,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f9,plain,
! [X0,X1,X2] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(flattening,[],[f8]) ).
fof(f37,plain,
! [X0] :
( ~ sP23(X0)
| ( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] :
( ~ p2(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p2(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p2(X4)
& r1(X0,X4) ) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f38,plain,
! [X0] :
( ~ sP23(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,[],[f37]) ).
fof(f39,plain,
! [X0] :
( ~ sP23(X0)
| ( ! [X2] :
( ( p2(sK25(X2))
& ~ p2(sK26(X2))
& r1(sK25(X2),sK26(X2))
& r1(X2,sK25(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK24(X0))
& r1(X0,sK24(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26]),skolemize(X1,sK24(X0)),skolemize(X3,sK25(X2)),skolemize(X4,sK26(X2))],[f38]) ).
fof(f40,plain,
! [X0] :
( ~ sP22(X0)
| ( ! [X15] :
( ? [X16] :
( p2(X16)
& ? [X17] :
( ~ p2(X17)
& r1(X16,X17) )
& r1(X15,X16) )
| p2(X15)
| ~ r1(X0,X15) )
& ? [X14] :
( ~ p2(X14)
& r1(X0,X14) ) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f41,plain,
! [X0] :
( ~ sP22(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,[],[f40]) ).
fof(f42,plain,
! [X0] :
( ~ sP22(X0)
| ( ! [X2] :
( ( p2(sK28(X2))
& ~ p2(sK29(X2))
& r1(sK28(X2),sK29(X2))
& r1(X2,sK28(X2)) )
| p2(X2)
| ~ r1(X0,X2) )
& ~ p2(sK27(X0))
& r1(X0,sK27(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29]),skolemize(X1,sK27(X0)),skolemize(X3,sK28(X2)),skolemize(X4,sK29(X2))],[f41]) ).
fof(f43,plain,
! [X0] :
( ~ sP21(X0)
| ( ( ? [X29] :
( p2(X29)
& ? [X30] :
( ~ p2(X30)
& r1(X29,X30) )
& r1(X0,X29) )
| p2(X0) )
& ( ? [X26] :
( ! [X27] :
( ~ p2(X27)
| ! [X28] :
( p2(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
& ~ p2(X26)
& r1(X0,X26) )
| sP20(X0) ) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f44,plain,
! [X0] :
( ~ sP21(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) )
| sP20(X0) ) ) ),
inference(rectify,[],[f43]) ).
fof(f45,plain,
! [X0] :
( ~ sP21(X0)
| ( ( ( p2(sK31(X0))
& ~ p2(sK32(X0))
& r1(sK31(X0),sK32(X0))
& r1(X0,sK31(X0)) )
| p2(X0) )
& ( ( ! [X2] :
( ~ p2(X2)
| ! [X3] :
( p2(X3)
| ~ r1(X2,X3) )
| ~ r1(sK30(X0),X2) )
& ~ p2(sK30(X0))
& r1(X0,sK30(X0)) )
| sP20(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32]),skolemize(X1,sK30(X0)),skolemize(X4,sK31(X0)),skolemize(X5,sK32(X0))],[f44]) ).
fof(f46,plain,
! [X0] :
( ~ sP20(X0)
| ! [X22] :
( ! [X23] :
( ? [X24] :
( p2(X24)
& ? [X25] :
( ~ p2(X25)
& r1(X24,X25) )
& r1(X23,X24) )
| p2(X23)
| ~ r1(X22,X23) )
| ~ r1(X0,X22) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f47,plain,
! [X0] :
( ~ sP20(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,[],[f46]) ).
fof(f48,plain,
! [X0] :
( ~ sP20(X0)
| ! [X1] :
( ! [X2] :
( ( p2(sK33(X2))
& ~ p2(sK34(X2))
& r1(sK33(X2),sK34(X2))
& r1(X2,sK33(X2)) )
| p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33,sK34]),skolemize(X3,sK33(X2)),skolemize(X4,sK34(X2))],[f47]) ).
fof(f49,plain,
! [X31] :
( ~ sP19(X31)
| ( ! [X36] :
( ? [X37] :
( p2(X37)
& ? [X38] :
( ~ p2(X38)
& r1(X37,X38) )
& r1(X36,X37) )
| p2(X36)
| ~ r1(X31,X36) )
& ? [X32] :
( ? [X33] :
( ! [X34] :
( ~ p2(X34)
| ! [X35] :
( p2(X35)
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
& ~ p2(X33)
& r1(X32,X33) )
& r1(X31,X32) ) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f50,plain,
! [X0] :
( ~ sP19(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,[],[f49]) ).
fof(f51,plain,
! [X0] :
( ~ sP19(X0)
| ( ! [X5] :
( ( p2(sK37(X5))
& ~ p2(sK38(X5))
& r1(sK37(X5),sK38(X5))
& r1(X5,sK37(X5)) )
| p2(X5)
| ~ r1(X0,X5) )
& ! [X3] :
( ~ p2(X3)
| ! [X4] :
( p2(X4)
| ~ r1(X3,X4) )
| ~ r1(sK36(X0),X3) )
& ~ p2(sK36(X0))
& r1(sK35(X0),sK36(X0))
& r1(X0,sK35(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36,sK37,sK38]),skolemize(X1,sK35(X0)),skolemize(X2,sK36(X0)),skolemize(X6,sK37(X5)),skolemize(X7,sK38(X5))],[f50]) ).
fof(f107,plain,
? [X0] :
( ! [X56] :
( ? [X57] :
( ! [X58] :
( ~ p2(X58)
| ! [X59] :
( p2(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
& ~ p2(X57)
& r1(X56,X57) )
| p2(X56)
| ~ r1(X0,X56) )
& ( ? [X50] :
( ! [X52] :
( ( ? [X55] : r1(X52,X55)
& ~ p1(X52) )
| ! [X53] :
( ! [X54] : ~ r1(X53,X54)
| p1(X53)
| ~ r1(X52,X53) )
| ~ r1(X50,X52) )
& ? [X51] : r1(X50,X51)
& ~ p1(X50)
& r1(X0,X50) )
| ! [X49] : ~ r1(X0,X49)
| p1(X0) )
& ( ? [X43] :
( ! [X45] :
( ( ? [X48] : r1(X45,X48)
& ~ p1(X45)
& ~ p2(X45) )
| ! [X46] :
( ! [X47] : ~ r1(X46,X47)
| p1(X46)
| p2(X46)
| ~ r1(X45,X46) )
| ~ r1(X43,X45) )
& ? [X44] : r1(X43,X44)
& ~ p1(X43)
& ~ p2(X43)
& r1(X0,X43) )
| ! [X42] : ~ r1(X0,X42)
| p1(X0)
| p2(X0) )
& ( ? [X40] :
( sP0(X40)
& ? [X41] : r1(X40,X41)
& ~ p1(X40)
& ~ p2(X40)
& ~ p3(X40)
& r1(X0,X40) )
| ! [X39] : ~ r1(X0,X39)
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X37] :
( sP1(X37)
& ? [X38] : r1(X37,X38)
& ~ p1(X37)
& ~ p2(X37)
& ~ p3(X37)
& ~ p4(X37)
& r1(X0,X37) )
| ! [X36] : ~ r1(X0,X36)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X35] :
( sP2(X35)
& sP3(X35)
& ~ p1(X35)
& r1(X0,X35) )
| ! [X33] :
( ! [X34] : ~ r1(X33,X34)
| p1(X33)
| p2(X33)
| p3(X33)
| p4(X33)
| ~ r1(X0,X33) )
| p1(X0) )
& ( ? [X32] :
( sP4(X32)
& sP5(X32)
& ~ p1(X32)
& ~ p2(X32)
& r1(X0,X32) )
| ! [X30] :
( ! [X31] : ~ r1(X30,X31)
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(X0,X30) )
| p1(X0)
| p2(X0) )
& ( ? [X29] :
( sP8(X29)
& sP7(X29)
& ~ p1(X29)
& ~ p2(X29)
& ~ p3(X29)
& r1(X0,X29) )
| ! [X27] :
( ! [X28] : ~ r1(X27,X28)
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(X0,X27) )
| p1(X0)
| p2(X0)
| p3(X0) )
& ( ? [X26] :
( sP11(X26)
& sP10(X26)
& ~ p1(X26)
& ~ p2(X26)
& ~ p3(X26)
& ~ p4(X26)
& r1(X0,X26) )
| ! [X24] :
( ! [X25] : ~ r1(X24,X25)
| p1(X24)
| p2(X24)
| p3(X24)
| p4(X24)
| ~ r1(X0,X24) )
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0) )
& ( ? [X23] :
( sP14(X23)
& sP15(X23)
& ~ p1(X23)
& r1(X0,X23) )
| ! [X20] :
( ! [X21] :
( ! [X22] : ~ r1(X21,X22)
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21) )
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(X0,X20) )
| p1(X0) )
& ( ? [X14] :
( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP17(X17)
| sP18(X17)
| ~ r1(X14,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
& ~ p2(X14) )
| sP19(X14) )
& r1(X0,X14) )
| sP21(X0) )
& ! [X11] :
( ? [X12] :
( p1(X12)
& ? [X13] :
( ~ p1(X13)
& r1(X12,X13) )
& r1(X11,X12) )
| p1(X11)
| ~ r1(X0,X11) )
& ? [X10] :
( ~ p1(X10)
& r1(X0,X10) )
& ( sP22(X0)
| ! [X8] :
( ? [X9] :
( p5(X9)
& r1(X8,X9) )
| ~ r1(X0,X8) ) )
& ! [X5] :
( ? [X6] :
( p3(X6)
& ? [X7] :
( ~ p3(X7)
& r1(X6,X7) )
& r1(X5,X6) )
| p3(X5)
| ~ r1(X0,X5) )
& ? [X4] :
( ~ p3(X4)
& r1(X0,X4) )
& ( sP23(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ p5(X3)
| ~ r1(X2,X3) )
& r1(X1,X2) )
& ~ p1(X1)
& r1(X0,X1) ) ) ),
inference(rectify,[],[f36]) ).
fof(f108,plain,
( ! [X56] :
( ( ! [X58] :
( ~ p2(X58)
| ! [X59] :
( p2(X59)
| ~ r1(X58,X59) )
| ~ r1(sK98(X56),X58) )
& ~ p2(sK98(X56))
& r1(X56,sK98(X56)) )
| p2(X56)
| ~ r1(sK72,X56) )
& ( ( ! [X52] :
( ( r1(X52,sK97(X52))
& ~ p1(X52) )
| ! [X53] :
( ! [X54] : ~ r1(X53,X54)
| p1(X53)
| ~ r1(X52,X53) )
| ~ r1(sK95,X52) )
& r1(sK95,sK96)
& ~ p1(sK95)
& r1(sK72,sK95) )
| ! [X49] : ~ r1(sK72,X49)
| p1(sK72) )
& ( ( ! [X45] :
( ( r1(X45,sK94(X45))
& ~ p1(X45)
& ~ p2(X45) )
| ! [X46] :
( ! [X47] : ~ r1(X46,X47)
| p1(X46)
| p2(X46)
| ~ r1(X45,X46) )
| ~ r1(sK92,X45) )
& r1(sK92,sK93)
& ~ p1(sK92)
& ~ p2(sK92)
& r1(sK72,sK92) )
| ! [X42] : ~ r1(sK72,X42)
| p1(sK72)
| p2(sK72) )
& ( ( sP0(sK90)
& r1(sK90,sK91)
& ~ p1(sK90)
& ~ p2(sK90)
& ~ p3(sK90)
& r1(sK72,sK90) )
| ! [X39] : ~ r1(sK72,X39)
| p1(sK72)
| p2(sK72)
| p3(sK72) )
& ( ( sP1(sK88)
& r1(sK88,sK89)
& ~ p1(sK88)
& ~ p2(sK88)
& ~ p3(sK88)
& ~ p4(sK88)
& r1(sK72,sK88) )
| ! [X36] : ~ r1(sK72,X36)
| p1(sK72)
| p2(sK72)
| p3(sK72)
| p4(sK72) )
& ( ( sP2(sK87)
& sP3(sK87)
& ~ p1(sK87)
& r1(sK72,sK87) )
| ! [X33] :
( ! [X34] : ~ r1(X33,X34)
| p1(X33)
| p2(X33)
| p3(X33)
| p4(X33)
| ~ r1(sK72,X33) )
| p1(sK72) )
& ( ( sP4(sK86)
& sP5(sK86)
& ~ p1(sK86)
& ~ p2(sK86)
& r1(sK72,sK86) )
| ! [X30] :
( ! [X31] : ~ r1(X30,X31)
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(sK72,X30) )
| p1(sK72)
| p2(sK72) )
& ( ( sP8(sK85)
& sP7(sK85)
& ~ p1(sK85)
& ~ p2(sK85)
& ~ p3(sK85)
& r1(sK72,sK85) )
| ! [X27] :
( ! [X28] : ~ r1(X27,X28)
| p1(X27)
| p2(X27)
| p3(X27)
| p4(X27)
| ~ r1(sK72,X27) )
| p1(sK72)
| p2(sK72)
| p3(sK72) )
& ( ( sP11(sK84)
& sP10(sK84)
& ~ p1(sK84)
& ~ p2(sK84)
& ~ p3(sK84)
& ~ p4(sK84)
& r1(sK72,sK84) )
| ! [X24] :
( ! [X25] : ~ r1(X24,X25)
| p1(X24)
| p2(X24)
| p3(X24)
| p4(X24)
| ~ r1(sK72,X24) )
| p1(sK72)
| p2(sK72)
| p3(sK72)
| p4(sK72) )
& ( ( sP14(sK83)
& sP15(sK83)
& ~ p1(sK83)
& r1(sK72,sK83) )
| ! [X20] :
( ! [X21] :
( ! [X22] : ~ r1(X21,X22)
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21) )
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(sK72,X20) )
| p1(sK72) )
& ( ( ! [X17] :
( ( ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p2(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
& ~ p2(X17) )
| sP17(X17)
| sP18(X17)
| ~ r1(sK82,X17) )
& ( ( ! [X15] :
( ~ p2(X15)
| ! [X16] :
( p2(X16)
| ~ r1(X15,X16) )
| ~ r1(sK82,X15) )
& ~ p2(sK82) )
| sP19(sK82) )
& r1(sK72,sK82) )
| sP21(sK72) )
& ! [X11] :
( ( p1(sK80(X11))
& ~ p1(sK81(X11))
& r1(sK80(X11),sK81(X11))
& r1(X11,sK80(X11)) )
| p1(X11)
| ~ r1(sK72,X11) )
& ~ p1(sK79)
& r1(sK72,sK79)
& ( sP22(sK72)
| ! [X8] :
( ( p5(sK78(X8))
& r1(X8,sK78(X8)) )
| ~ r1(sK72,X8) ) )
& ! [X5] :
( ( p3(sK76(X5))
& ~ p3(sK77(X5))
& r1(sK76(X5),sK77(X5))
& r1(X5,sK76(X5)) )
| p3(X5)
| ~ r1(sK72,X5) )
& ~ p3(sK75)
& r1(sK72,sK75)
& ( sP23(sK72)
| ( ! [X3] :
( ~ p5(X3)
| ~ r1(sK74,X3) )
& r1(sK73,sK74)
& ~ p1(sK73)
& r1(sK72,sK73) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72,sK73,sK74,sK75,sK76,sK77,sK78,sK79,sK80,sK81,sK82,sK83,sK84,sK85,sK86,sK87,sK88,sK89,sK90,sK91,sK92,sK93,sK94,sK95,sK96,sK97,sK98]),skolemize(X0,sK72),skolemize(X1,sK73),skolemize(X2,sK74),skolemize(X4,sK75),skolemize(X6,sK76(X5)),skolemize(X7,sK77(X5)),skolemize(X9,sK78(X8)),skolemize(X10,sK79),skolemize(X12,sK80(X11)),skolemize(X13,sK81(X11)),skolemize(X14,sK82),skolemize(X23,sK83),skolemize(X26,sK84),skolemize(X29,sK85),skolemize(X32,sK86),skolemize(X35,sK87),skolemize(X37,sK88),skolemize(X38,sK89),skolemize(X40,sK90),skolemize(X41,sK91),skolemize(X43,sK92),skolemize(X44,sK93),skolemize(X48,sK94(X45)),skolemize(X50,sK95),skolemize(X51,sK96),skolemize(X55,sK97(X52)),skolemize(X57,sK98(X56))],[f107]) ).
fof(f109,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f110,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f111,plain,
! [X2,X0] :
( ~ sP23(X0)
| p2(sK25(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f112,plain,
! [X2,X0] :
( ~ sP23(X0)
| ~ p2(sK26(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f113,plain,
! [X2,X0] :
( ~ sP23(X0)
| r1(sK25(X2),sK26(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f114,plain,
! [X2,X0] :
( ~ sP23(X0)
| r1(X2,sK25(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f115,plain,
! [X0] :
( ~ sP23(X0)
| ~ p2(sK24(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f116,plain,
! [X0] :
( ~ sP23(X0)
| r1(X0,sK24(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f117,plain,
! [X2,X0] :
( ~ sP22(X0)
| p2(sK28(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f118,plain,
! [X2,X0] :
( ~ sP22(X0)
| ~ p2(sK29(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f119,plain,
! [X2,X0] :
( ~ sP22(X0)
| r1(sK28(X2),sK29(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f120,plain,
! [X2,X0] :
( ~ sP22(X0)
| r1(X2,sK28(X2))
| p2(X2)
| ~ r1(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f121,plain,
! [X0] :
( ~ sP22(X0)
| ~ p2(sK27(X0)) ),
inference(cnf_transformation,[],[f42]) ).
fof(f122,plain,
! [X0] :
( ~ sP22(X0)
| r1(X0,sK27(X0)) ),
inference(cnf_transformation,[],[f42]) ).
fof(f127,plain,
! [X2,X3,X0] :
( ~ sP21(X0)
| ~ p2(X2)
| p2(X3)
| ~ r1(X2,X3)
| ~ r1(sK30(X0),X2)
| sP20(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f128,plain,
! [X0] :
( ~ sP21(X0)
| ~ p2(sK30(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f129,plain,
! [X0] :
( ~ sP21(X0)
| r1(X0,sK30(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| p2(sK33(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ p2(sK34(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f132,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| r1(sK33(X2),sK34(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f133,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| r1(X2,sK33(X2))
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f138,plain,
! [X3,X0,X4] :
( ~ sP19(X0)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK36(X0),X3) ),
inference(cnf_transformation,[],[f51]) ).
fof(f139,plain,
! [X0] :
( ~ sP19(X0)
| ~ p2(sK36(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f140,plain,
! [X0] :
( ~ sP19(X0)
| r1(sK35(X0),sK36(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f141,plain,
! [X0] :
( ~ sP19(X0)
| r1(X0,sK35(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f255,plain,
! [X58,X59,X56] :
( ~ p2(X58)
| p2(X59)
| ~ r1(X58,X59)
| ~ r1(sK98(X56),X58)
| p2(X56)
| ~ r1(sK72,X56) ),
inference(cnf_transformation,[],[f108]) ).
fof(f256,plain,
! [X56] :
( ~ p2(sK98(X56))
| p2(X56)
| ~ r1(sK72,X56) ),
inference(cnf_transformation,[],[f108]) ).
fof(f257,plain,
! [X56] :
( r1(X56,sK98(X56))
| p2(X56)
| ~ r1(sK72,X56) ),
inference(cnf_transformation,[],[f108]) ).
fof(f309,plain,
! [X18,X19,X17] :
( ~ p2(X18)
| p2(X19)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| sP17(X17)
| sP18(X17)
| ~ r1(sK82,X17)
| sP21(sK72) ),
inference(cnf_transformation,[],[f108]) ).
fof(f311,plain,
! [X16,X15] :
( ~ p2(X15)
| p2(X16)
| ~ r1(X15,X16)
| ~ r1(sK82,X15)
| sP19(sK82)
| sP21(sK72) ),
inference(cnf_transformation,[],[f108]) ).
fof(f312,plain,
( ~ p2(sK82)
| sP19(sK82)
| sP21(sK72) ),
inference(cnf_transformation,[],[f108]) ).
fof(f313,plain,
( r1(sK72,sK82)
| sP21(sK72) ),
inference(cnf_transformation,[],[f108]) ).
fof(f317,plain,
! [X11] :
( r1(X11,sK80(X11))
| p1(X11)
| ~ r1(sK72,X11) ),
inference(cnf_transformation,[],[f108]) ).
fof(f320,plain,
! [X8] :
( sP22(sK72)
| p5(sK78(X8))
| ~ r1(sK72,X8) ),
inference(cnf_transformation,[],[f108]) ).
fof(f321,plain,
! [X8] :
( sP22(sK72)
| r1(X8,sK78(X8))
| ~ r1(sK72,X8) ),
inference(cnf_transformation,[],[f108]) ).
fof(f328,plain,
! [X3] :
( sP23(sK72)
| ~ p5(X3)
| ~ r1(sK74,X3) ),
inference(cnf_transformation,[],[f108]) ).
fof(f329,plain,
( sP23(sK72)
| r1(sK73,sK74) ),
inference(cnf_transformation,[],[f108]) ).
fof(f331,plain,
( sP23(sK72)
| r1(sK72,sK73) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f109]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_51,plain,
! [X0: $i] :
( r1(X0,sK24(X0))
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( ~ sP23(X0)
| ~ p2(sK24(X0)) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK25(X1))
| ~ sP23(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK25(X1),sK26(X1))
| ~ sP23(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP23(X0)
| ~ p2(sK26(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK25(X1))
| ~ sP23(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_57,plain,
! [X0: $i] :
( r1(X0,sK27(X0))
| ~ sP22(X0) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_58,negated_conjecture,
! [X0: $i] :
( ~ sP22(X0)
| ~ p2(sK27(X0)) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(X1,sK28(X1))
| ~ sP22(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| r1(sK28(X1),sK29(X1))
| ~ sP22(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP22(X0)
| ~ p2(sK29(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK28(X1))
| ~ sP22(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_63,plain,
! [X0: $i] :
( sP20(X0)
| r1(X0,sK30(X0))
| ~ sP21(X0) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_64,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP21(X0)
| ~ p2(sK30(X0)) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP20(X0)
| p2(X2)
| ~ sP21(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK30(X0),X1) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(X2,sK33(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| r1(sK33(X2),sK34(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP20(X0)
| ~ p2(sK34(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(sK33(X2))
| ~ sP20(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_74,plain,
! [X0: $i] :
( r1(X0,sK35(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_75,plain,
! [X0: $i] :
( r1(sK35(X0),sK36(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_76,negated_conjecture,
! [X0: $i] :
( ~ sP19(X0)
| ~ p2(sK36(X0)) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP19(X0)
| ~ p2(X1)
| ~ r1(X1,X2)
| ~ r1(sK36(X0),X1) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_195,negated_conjecture,
( sP23(sK72)
| r1(sK72,sK73) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_197,negated_conjecture,
( sP23(sK72)
| r1(sK73,sK74) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_198,negated_conjecture,
! [X0: $i] :
( sP23(sK72)
| ~ p5(X0)
| ~ r1(sK74,X0) ),
inference(cnf_transformation,[],[f328]) ).
tcf(c_205,negated_conjecture,
! [X0: $i] :
( sP22(sK72)
| r1(X0,sK78(X0))
| ~ r1(sK72,X0) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_206,negated_conjecture,
! [X0: $i] :
( sP22(sK72)
| p5(sK78(X0))
| ~ r1(sK72,X0) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_209,negated_conjecture,
! [X0: $i] :
( p1(X0)
| r1(X0,sK80(X0))
| ~ r1(sK72,X0) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_213,negated_conjecture,
( sP21(sK72)
| r1(sK72,sK82) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_214,negated_conjecture,
( sP19(sK82)
| sP21(sK72)
| ~ p2(sK82) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_215,negated_conjecture,
! [X0: $i,X1: $i] :
( sP19(sK82)
| sP21(sK72)
| p2(X1)
| ~ p2(X0)
| ~ r1(sK82,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_217,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP21(sK72)
| sP17(X0)
| sP18(X0)
| p2(X2)
| ~ p2(X1)
| ~ r1(sK82,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_269,negated_conjecture,
! [X0: $i] :
( p2(X0)
| r1(X0,sK98(X0))
| ~ r1(sK72,X0) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_270,negated_conjecture,
! [X0: $i] :
( p2(X0)
| ~ p2(sK98(X0))
| ~ r1(sK72,X0) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_271,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| p2(X0)
| ~ p2(X1)
| ~ r1(sK72,X0)
| ~ r1(X1,X2)
| ~ r1(sK98(X0),X1) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_272,plain,
r1(sK72,sK72),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_312,plain,
( ~ sP22(sK72)
| ~ p2(sK27(sK72)) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_313,plain,
( ~ sP23(sK72)
| ~ p2(sK24(sK72)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_325,plain,
( r1(sK72,sK27(sK72))
| ~ sP22(sK72) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_326,plain,
( r1(sK72,sK24(sK72))
| ~ sP23(sK72) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_347,plain,
( sP20(sK72)
| ~ sP21(sK72)
| ~ p2(sK30(sK72)) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_348,plain,
( sP20(sK72)
| r1(sK72,sK30(sK72))
| ~ sP21(sK72) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_527,plain,
! [X0: $i] :
( p2(sK27(X0))
| r1(sK27(X0),sK98(sK27(X0)))
| ~ r1(sK72,sK27(X0)) ),
inference(instantiation,[status(thm)],[c_269]) ).
tcf(c_528,plain,
( p2(sK27(sK72))
| r1(sK27(sK72),sK98(sK27(sK72)))
| ~ r1(sK72,sK27(sK72)) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_554,plain,
! [X0: $i,X1: $i] :
( p2(sK98(X1))
| p2(sK28(sK98(X1)))
| ~ sP22(X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_564,plain,
! [X0: $i,X1: $i] :
( p2(sK98(X1))
| r1(sK98(X1),sK28(sK98(X1)))
| ~ sP22(X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i] :
( p2(sK98(X1))
| r1(sK28(sK98(X1)),sK29(sK98(X1)))
| ~ sP22(X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_627,plain,
! [X0: $i,X1: $i] :
( r1(sK72,sK98(X1))
| ~ r1(sK72,X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_654,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(X0)
| ~ r1(sK72,X0)
| ~ p2(sK28(sK98(X0)))
| ~ r1(sK28(sK98(X0)),X1)
| ~ r1(sK98(X0),sK28(sK98(X0))) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_729,plain,
( sP22(sK72)
| sP23(sK72)
| ~ p5(sK78(sK74))
| ~ r1(sK72,sK74) ),
inference(superposition,[status(thm)],[c_205,c_198]) ).
tcf(c_746,plain,
! [X0: $i] :
( r1(sK72,sK98(sK27(X0)))
| ~ r1(sK72,sK27(X0))
| ~ r1(sK27(X0),sK98(sK27(X0))) ),
inference(instantiation,[status(thm)],[c_627]) ).
tcf(c_747,plain,
( r1(sK72,sK98(sK27(sK72)))
| ~ r1(sK72,sK27(sK72))
| ~ r1(sK27(sK72),sK98(sK27(sK72))) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_795,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK98(X1))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ p2(sK34(sK98(X1)))
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_803,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK98(X1))
| p2(sK33(sK98(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_811,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK98(X1))
| r1(sK98(X1),sK33(sK98(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_823,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK98(X1))
| r1(sK33(sK98(X1)),sK34(sK98(X1)))
| ~ sP20(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK98(X1)) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_826,plain,
( p2(sK24(sK72))
| ~ sP23(sK72)
| ~ p2(sK98(sK24(sK72))) ),
inference(superposition,[status(thm)],[c_51,c_270]) ).
tcf(c_827,plain,
( p2(sK27(sK72))
| ~ sP22(sK72)
| ~ p2(sK98(sK27(sK72))) ),
inference(superposition,[status(thm)],[c_57,c_270]) ).
tcf(c_1102,plain,
! [X0: $i] :
( p2(sK24(X0))
| r1(sK24(X0),sK98(sK24(X0)))
| ~ r1(sK72,sK24(X0)) ),
inference(instantiation,[status(thm)],[c_269]) ).
tcf(c_1103,plain,
( p2(sK24(sK72))
| r1(sK24(sK72),sK98(sK24(sK72)))
| ~ r1(sK72,sK24(sK72)) ),
inference(instantiation,[status(thm)],[c_1102]) ).
tcf(c_1614,plain,
! [X0: $i] :
( sP23(sK72)
| r1(X0,sK74)
| ~ r1(X0,sK73) ),
inference(resolution,[status(thm)],[c_50,c_197]) ).
tcf(c_1615,plain,
( sP23(sK72)
| r1(sK72,sK74)
| ~ r1(sK72,sK73) ),
inference(instantiation,[status(thm)],[c_1614]) ).
tcf(c_1625,plain,
! [X0: $i] :
( sP21(sK72)
| r1(X0,sK82)
| ~ r1(X0,sK72) ),
inference(resolution,[status(thm)],[c_50,c_213]) ).
tcf(c_1720,plain,
! [X0: $i] :
( p2(sK82)
| ~ sP23(X0)
| ~ p2(sK26(sK82))
| ~ r1(X0,sK82) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_1721,plain,
( p2(sK82)
| ~ sP23(sK72)
| ~ p2(sK26(sK82))
| ~ r1(sK72,sK82) ),
inference(instantiation,[status(thm)],[c_1720]) ).
tcf(c_1783,plain,
! [X0: $i,X1: $i] :
( p2(sK30(X1))
| r1(sK25(sK30(X1)),sK26(sK30(X1)))
| ~ sP23(X0)
| ~ r1(X0,sK30(X1)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_1784,plain,
! [X0: $i,X1: $i] :
( p2(sK30(X1))
| ~ sP23(X0)
| ~ p2(sK26(sK30(X1)))
| ~ r1(X0,sK30(X1)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_1799,plain,
( p2(sK30(sK72))
| ~ sP23(sK72)
| ~ p2(sK26(sK30(sK72)))
| ~ r1(sK72,sK30(sK72)) ),
inference(instantiation,[status(thm)],[c_1784]) ).
tcf(c_1800,plain,
( p2(sK30(sK72))
| r1(sK25(sK30(sK72)),sK26(sK30(sK72)))
| ~ sP23(sK72)
| ~ r1(sK72,sK30(sK72)) ),
inference(instantiation,[status(thm)],[c_1783]) ).
tcf(c_1880,plain,
( sP22(sK72)
| sP23(sK72)
| p5(sK78(sK74))
| ~ r1(sK72,sK73) ),
inference(resolution,[status(thm)],[c_1614,c_206]) ).
tcf(c_1910,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK30(X0))
| p2(sK25(sK30(X0)))
| ~ sP21(X0)
| ~ sP23(X0) ),
inference(superposition,[status(thm)],[c_63,c_56]) ).
tcf(c_1971,plain,
! [X0: $i,X1: $i] :
( p2(sK98(sK24(X0)))
| r1(sK33(sK98(sK24(X0))),sK34(sK98(sK24(X0))))
| ~ sP20(X1)
| ~ r1(X1,sK24(X0))
| ~ r1(sK24(X0),sK98(sK24(X0))) ),
inference(instantiation,[status(thm)],[c_823]) ).
tcf(c_1972,plain,
! [X0: $i,X1: $i] :
( p2(sK98(sK24(X0)))
| r1(sK98(sK24(X0)),sK33(sK98(sK24(X0))))
| ~ sP20(X1)
| ~ r1(X1,sK24(X0))
| ~ r1(sK24(X0),sK98(sK24(X0))) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1973,plain,
! [X0: $i,X1: $i] :
( p2(sK98(sK24(X0)))
| p2(sK33(sK98(sK24(X0))))
| ~ sP20(X1)
| ~ r1(X1,sK24(X0))
| ~ r1(sK24(X0),sK98(sK24(X0))) ),
inference(instantiation,[status(thm)],[c_803]) ).
tcf(c_1974,plain,
! [X0: $i,X1: $i] :
( p2(sK98(sK24(X0)))
| ~ sP20(X1)
| ~ r1(X1,sK24(X0))
| ~ p2(sK34(sK98(sK24(X0))))
| ~ r1(sK24(X0),sK98(sK24(X0))) ),
inference(instantiation,[status(thm)],[c_795]) ).
tcf(c_1979,plain,
( p2(sK98(sK24(sK72)))
| ~ sP20(sK72)
| ~ r1(sK72,sK24(sK72))
| ~ p2(sK34(sK98(sK24(sK72))))
| ~ r1(sK24(sK72),sK98(sK24(sK72))) ),
inference(instantiation,[status(thm)],[c_1974]) ).
tcf(c_1980,plain,
( p2(sK98(sK24(sK72)))
| p2(sK33(sK98(sK24(sK72))))
| ~ sP20(sK72)
| ~ r1(sK72,sK24(sK72))
| ~ r1(sK24(sK72),sK98(sK24(sK72))) ),
inference(instantiation,[status(thm)],[c_1973]) ).
tcf(c_1981,plain,
( p2(sK98(sK24(sK72)))
| r1(sK98(sK24(sK72)),sK33(sK98(sK24(sK72))))
| ~ sP20(sK72)
| ~ r1(sK72,sK24(sK72))
| ~ r1(sK24(sK72),sK98(sK24(sK72))) ),
inference(instantiation,[status(thm)],[c_1972]) ).
tcf(c_1982,plain,
( p2(sK98(sK24(sK72)))
| r1(sK33(sK98(sK24(sK72))),sK34(sK98(sK24(sK72))))
| ~ sP20(sK72)
| ~ r1(sK72,sK24(sK72))
| ~ r1(sK24(sK72),sK98(sK24(sK72))) ),
inference(instantiation,[status(thm)],[c_1971]) ).
tcf(c_2014,plain,
( sP22(sK72)
| sP23(sK72) ),
inference(global_subsumption_just,[status(thm)],[c_1880,c_195,c_729,c_1615,c_1880]) ).
tcf(c_3171,plain,
! [X0: $i,X1: $i] :
( p1(sK82)
| sP21(sK72)
| p2(X1)
| sP17(sK80(sK82))
| sP18(sK80(sK82))
| ~ p2(X0)
| ~ r1(sK72,sK82)
| ~ r1(X0,X1)
| ~ r1(sK80(sK82),X0) ),
inference(resolution,[status(thm)],[c_217,c_209]) ).
tcf(c_3437,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK24(X0))
| ~ r1(sK72,sK24(X0))
| ~ p2(sK33(sK98(sK24(X0))))
| ~ r1(sK33(sK98(sK24(X0))),X1)
| ~ r1(sK98(sK24(X0)),sK33(sK98(sK24(X0)))) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_3668,plain,
! [X0: $i,X1: $i] :
( p2(sK24(X0))
| p2(sK34(sK98(sK24(X1))))
| ~ r1(sK72,sK24(X0))
| ~ p2(sK33(sK98(sK24(X0))))
| ~ r1(sK98(sK24(X0)),sK33(sK98(sK24(X0))))
| ~ r1(sK33(sK98(sK24(X0))),sK34(sK98(sK24(X1)))) ),
inference(instantiation,[status(thm)],[c_3437]) ).
tcf(c_3669,plain,
( p2(sK24(sK72))
| p2(sK34(sK98(sK24(sK72))))
| ~ r1(sK72,sK24(sK72))
| ~ p2(sK33(sK98(sK24(sK72))))
| ~ r1(sK98(sK24(sK72)),sK33(sK98(sK24(sK72))))
| ~ r1(sK33(sK98(sK24(sK72))),sK34(sK98(sK24(sK72)))) ),
inference(instantiation,[status(thm)],[c_3668]) ).
tcf(c_3683,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK30(X0))
| r1(sK30(X0),sK25(sK30(X0)))
| ~ sP21(X0)
| ~ sP23(X0) ),
inference(superposition,[status(thm)],[c_63,c_53]) ).
tcf(c_3699,plain,
( sP21(sK72)
| p2(sK82)
| r1(sK82,sK25(sK82))
| ~ sP23(sK72) ),
inference(superposition,[status(thm)],[c_213,c_53]) ).
tcf(c_4229,plain,
! [X0: $i] :
( p2(sK98(sK27(X0)))
| r1(sK28(sK98(sK27(X0))),sK29(sK98(sK27(X0))))
| ~ sP22(sK72)
| ~ r1(sK72,sK98(sK27(X0))) ),
inference(instantiation,[status(thm)],[c_572]) ).
tcf(c_4240,plain,
! [X0: $i] :
( p2(sK98(sK27(X0)))
| r1(sK98(sK27(X0)),sK28(sK98(sK27(X0))))
| ~ sP22(sK72)
| ~ r1(sK72,sK98(sK27(X0))) ),
inference(instantiation,[status(thm)],[c_564]) ).
tcf(c_4241,plain,
( p2(sK98(sK27(sK72)))
| r1(sK98(sK27(sK72)),sK28(sK98(sK27(sK72))))
| ~ sP22(sK72)
| ~ r1(sK72,sK98(sK27(sK72))) ),
inference(instantiation,[status(thm)],[c_4240]) ).
tcf(c_4250,plain,
( p2(sK98(sK27(sK72)))
| r1(sK28(sK98(sK27(sK72))),sK29(sK98(sK27(sK72))))
| ~ sP22(sK72)
| ~ r1(sK72,sK98(sK27(sK72))) ),
inference(instantiation,[status(thm)],[c_4229]) ).
tcf(c_5739,plain,
! [X0: $i] :
( sP21(sK72)
| r1(sK72,X0)
| ~ r1(sK82,X0) ),
inference(superposition,[status(thm)],[c_213,c_50]) ).
tcf(c_6204,plain,
( sP21(sK72)
| r1(sK72,sK35(sK82))
| ~ sP19(sK82) ),
inference(superposition,[status(thm)],[c_74,c_5739]) ).
tcf(c_6542,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| p2(sK27(X0))
| ~ r1(sK72,sK27(X0))
| ~ p2(sK28(sK98(sK27(X0))))
| ~ r1(sK28(sK98(sK27(X0))),X1)
| ~ r1(sK98(sK27(X0)),sK28(sK98(sK27(X0)))) ),
inference(instantiation,[status(thm)],[c_654]) ).
tcf(c_9512,plain,
! [X0: $i] :
( p2(sK27(X0))
| p2(sK29(sK98(sK27(X0))))
| ~ r1(sK72,sK27(X0))
| ~ p2(sK28(sK98(sK27(X0))))
| ~ r1(sK98(sK27(X0)),sK28(sK98(sK27(X0))))
| ~ r1(sK28(sK98(sK27(X0))),sK29(sK98(sK27(X0)))) ),
inference(instantiation,[status(thm)],[c_6542]) ).
tcf(c_9513,plain,
( p2(sK27(sK72))
| p2(sK29(sK98(sK27(sK72))))
| ~ r1(sK72,sK27(sK72))
| ~ p2(sK28(sK98(sK27(sK72))))
| ~ r1(sK98(sK27(sK72)),sK28(sK98(sK27(sK72))))
| ~ r1(sK28(sK98(sK27(sK72))),sK29(sK98(sK27(sK72)))) ),
inference(instantiation,[status(thm)],[c_9512]) ).
tcf(c_13946,plain,
! [X0: $i] :
( sP23(sK72)
| r1(sK73,X0)
| ~ r1(sK74,X0) ),
inference(superposition,[status(thm)],[c_197,c_50]) ).
tcf(c_13977,plain,
( sP21(sK72)
| p2(sK82)
| p2(sK25(sK82))
| ~ sP23(sK72) ),
inference(superposition,[status(thm)],[c_213,c_56]) ).
tcf(c_14512,plain,
( sP23(sK72)
| r1(sK73,sK35(sK74))
| ~ sP19(sK74) ),
inference(superposition,[status(thm)],[c_74,c_13946]) ).
tcf(c_16742,plain,
! [X0: $i] :
( p2(sK98(sK27(X0)))
| p2(sK28(sK98(sK27(X0))))
| ~ sP22(sK72)
| ~ r1(sK72,sK98(sK27(X0))) ),
inference(instantiation,[status(thm)],[c_554]) ).
tcf(c_16743,plain,
( p2(sK98(sK27(sK72)))
| p2(sK28(sK98(sK27(sK72))))
| ~ sP22(sK72)
| ~ r1(sK72,sK98(sK27(sK72))) ),
inference(instantiation,[status(thm)],[c_16742]) ).
tcf(c_21250,plain,
( r1(sK35(sK82),sK36(sK82))
| ~ sP19(sK82) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_21252,plain,
( ~ sP19(sK82)
| ~ p2(sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_23674,plain,
! [X0: $i,X1: $i] :
( p2(sK98(sK27(X1)))
| ~ sP22(X0)
| ~ p2(sK29(sK98(sK27(X1))))
| ~ r1(X0,sK98(sK27(X1))) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_23675,plain,
( p2(sK98(sK27(sK72)))
| ~ sP22(sK72)
| ~ p2(sK29(sK98(sK27(sK72))))
| ~ r1(sK72,sK98(sK27(sK72))) ),
inference(instantiation,[status(thm)],[c_23674]) ).
tcf(c_24010,plain,
sP23(sK72),
inference(global_subsumption_just,[status(thm)],[c_14512,c_312,c_325,c_528,c_747,c_827,c_2014,c_4241,c_4250,c_9513,c_16743,c_23675]) ).
tcf(c_24606,plain,
! [X0: $i] :
( sP21(sK72)
| p2(sK82)
| p2(sK25(sK82))
| ~ sP23(X0)
| ~ r1(X0,sK72) ),
inference(resolution,[status(thm)],[c_56,c_1625]) ).
tcf(c_24607,plain,
( sP21(sK72)
| p2(sK82)
| p2(sK25(sK82))
| ~ sP23(sK72)
| ~ r1(sK72,sK72) ),
inference(instantiation,[status(thm)],[c_24606]) ).
tcf(c_24705,plain,
( sP21(sK72)
| p2(sK82)
| r1(sK82,sK25(sK82))
| ~ sP23(sK72) ),
inference(resolution,[status(thm)],[c_53,c_213]) ).
tcf(c_24790,plain,
( sP21(sK72)
| p2(sK82)
| p2(sK25(sK82)) ),
inference(global_subsumption_just,[status(thm)],[c_13977,c_272,c_312,c_325,c_528,c_747,c_827,c_2014,c_4241,c_4250,c_9513,c_16743,c_23675,c_24607]) ).
tcf(c_26768,plain,
( sP21(sK72)
| p2(sK82)
| r1(sK25(sK82),sK26(sK82))
| ~ sP23(sK72) ),
inference(resolution,[status(thm)],[c_54,c_213]) ).
tcf(c_26773,plain,
! [X0: $i] :
( sP21(sK72)
| p2(sK82)
| r1(sK25(sK82),sK26(sK82))
| ~ sP23(X0)
| ~ r1(X0,sK72) ),
inference(resolution,[status(thm)],[c_54,c_1625]) ).
tcf(c_26774,plain,
( sP21(sK72)
| p2(sK82)
| r1(sK25(sK82),sK26(sK82))
| ~ sP23(sK72)
| ~ r1(sK72,sK72) ),
inference(instantiation,[status(thm)],[c_26773]) ).
tcf(c_26894,plain,
! [X0: $i] :
( p2(sK36(sK82))
| r1(sK25(sK36(sK82)),sK26(sK36(sK82)))
| ~ sP23(X0)
| ~ r1(X0,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_26895,plain,
! [X0: $i] :
( p2(sK36(sK82))
| ~ sP23(X0)
| ~ p2(sK26(sK36(sK82)))
| ~ r1(X0,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_26896,plain,
! [X0: $i] :
( p2(sK36(sK82))
| r1(sK36(sK82),sK25(sK36(sK82)))
| ~ sP23(X0)
| ~ r1(X0,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_26897,plain,
! [X0: $i] :
( p2(sK36(sK82))
| p2(sK25(sK36(sK82)))
| ~ sP23(X0)
| ~ r1(X0,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_26905,plain,
( p2(sK36(sK82))
| p2(sK25(sK36(sK82)))
| ~ sP23(sK72)
| ~ r1(sK72,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_26897]) ).
tcf(c_26906,plain,
( p2(sK36(sK82))
| r1(sK36(sK82),sK25(sK36(sK82)))
| ~ sP23(sK72)
| ~ r1(sK72,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_26896]) ).
tcf(c_26907,plain,
( p2(sK36(sK82))
| ~ sP23(sK72)
| ~ p2(sK26(sK36(sK82)))
| ~ r1(sK72,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_26895]) ).
tcf(c_26908,plain,
( p2(sK36(sK82))
| r1(sK25(sK36(sK82)),sK26(sK36(sK82)))
| ~ sP23(sK72)
| ~ r1(sK72,sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_26894]) ).
tcf(c_28815,plain,
( sP21(sK72)
| p2(sK82)
| r1(sK82,sK25(sK82)) ),
inference(global_subsumption_just,[status(thm)],[c_24705,c_312,c_325,c_528,c_747,c_827,c_2014,c_3699,c_4241,c_4250,c_9513,c_16743,c_23675]) ).
tcf(c_28844,plain,
! [X0: $i] :
( sP19(sK82)
| sP21(sK72)
| p2(sK82)
| p2(X0)
| ~ p2(sK25(sK82))
| ~ r1(sK25(sK82),X0) ),
inference(resolution,[status(thm)],[c_28815,c_215]) ).
tcf(c_28992,plain,
( sP21(sK72)
| p2(sK82)
| r1(sK25(sK82),sK26(sK82)) ),
inference(global_subsumption_just,[status(thm)],[c_26768,c_272,c_312,c_325,c_528,c_747,c_827,c_2014,c_4241,c_4250,c_9513,c_16743,c_23675,c_26774]) ).
tcf(c_29631,plain,
! [X0: $i] :
( sP21(sK72)
| r1(sK72,X0)
| ~ r1(sK82,X0) ),
inference(superposition,[status(thm)],[c_213,c_50]) ).
tcf(c_30143,plain,
( sP21(sK72)
| r1(sK72,sK35(sK82))
| ~ sP19(sK82) ),
inference(superposition,[status(thm)],[c_74,c_29631]) ).
tcf(c_33386,plain,
! [X0: $i] :
( sP19(sK82)
| sP21(sK72)
| ~ r1(sK25(sK82),X0)
| p2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_28844,c_214,c_24790,c_28844]) ).
tcf(c_33387,plain,
! [X0: $i] :
( sP19(sK82)
| sP21(sK72)
| p2(X0)
| ~ r1(sK25(sK82),X0) ),
inference(renaming,[status(thm)],[c_33386]) ).
tcf(c_33411,plain,
( sP19(sK82)
| sP21(sK72)
| sP22(sK72)
| p2(sK78(sK25(sK82)))
| ~ r1(sK72,sK25(sK82)) ),
inference(resolution,[status(thm)],[c_33387,c_205]) ).
tcf(c_33435,plain,
( sP19(sK82)
| sP21(sK72)
| p2(sK82)
| p2(sK26(sK82)) ),
inference(resolution,[status(thm)],[c_33387,c_28992]) ).
tcf(c_33717,plain,
( sP19(sK82)
| sP21(sK72) ),
inference(global_subsumption_just,[status(thm)],[c_33411,c_213,c_214,c_312,c_325,c_528,c_747,c_827,c_1721,c_2014,c_4241,c_4250,c_9513,c_16743,c_23675,c_33435]) ).
tcf(c_35731,plain,
( sP21(sK72)
| r1(sK72,sK35(sK82)) ),
inference(global_subsumption_just,[status(thm)],[c_30143,c_213,c_214,c_312,c_325,c_528,c_747,c_827,c_1721,c_2014,c_4241,c_4250,c_6204,c_9513,c_16743,c_23675,c_33435]) ).
tcf(c_38070,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK30(X0))
| p2(sK25(sK30(X0)))
| ~ sP21(X0)
| ~ sP23(X0) ),
inference(resolution,[status(thm)],[c_63,c_56]) ).
tcf(c_38071,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK30(X0))
| r1(sK30(X0),sK25(sK30(X0)))
| ~ sP21(X0)
| ~ sP23(X0) ),
inference(resolution,[status(thm)],[c_63,c_53]) ).
tcf(c_38581,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP23(X0)
| ~ sP21(X0)
| p2(sK25(sK30(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_38070,c_64,c_1910]) ).
tcf(c_38582,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK25(sK30(X0)))
| ~ sP21(X0)
| ~ sP23(X0) ),
inference(renaming,[status(thm)],[c_38581]) ).
tcf(c_38583,plain,
( sP20(sK72)
| p2(sK25(sK30(sK72)))
| ~ sP21(sK72)
| ~ sP23(sK72) ),
inference(instantiation,[status(thm)],[c_38582]) ).
tcf(c_39324,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP23(X0)
| ~ sP21(X0)
| r1(sK30(X0),sK25(sK30(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_38071,c_64,c_3683]) ).
tcf(c_39325,plain,
! [X0: $i] :
( sP20(X0)
| r1(sK30(X0),sK25(sK30(X0)))
| ~ sP21(X0)
| ~ sP23(X0) ),
inference(renaming,[status(thm)],[c_39324]) ).
tcf(c_39326,plain,
( sP20(sK72)
| r1(sK30(sK72),sK25(sK30(sK72)))
| ~ sP21(sK72)
| ~ sP23(sK72) ),
inference(instantiation,[status(thm)],[c_39325]) ).
tcf(c_40071,plain,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ sP19(sK82)
| ~ p2(X0)
| ~ r1(X0,X1)
| ~ r1(sK36(sK82),X0) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_40176,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK36(X1))
| ~ r1(X2,X0)
| ~ r1(X0,sK36(X1)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_40188,plain,
! [X0: $i] :
( p2(X0)
| ~ sP19(sK82)
| ~ p2(sK25(sK36(sK82)))
| ~ r1(sK25(sK36(sK82)),X0)
| ~ r1(sK36(sK82),sK25(sK36(sK82))) ),
inference(instantiation,[status(thm)],[c_40071]) ).
tcf(c_40891,plain,
! [X0: $i] :
( r1(X0,sK36(sK82))
| ~ r1(X0,sK35(sK82))
| ~ r1(sK35(sK82),sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_40176]) ).
tcf(c_40892,plain,
( r1(sK72,sK36(sK82))
| ~ r1(sK72,sK35(sK82))
| ~ r1(sK35(sK82),sK36(sK82)) ),
inference(instantiation,[status(thm)],[c_40891]) ).
tcf(c_41268,plain,
( p2(sK26(sK36(sK82)))
| ~ sP19(sK82)
| ~ p2(sK25(sK36(sK82)))
| ~ r1(sK36(sK82),sK25(sK36(sK82)))
| ~ r1(sK25(sK36(sK82)),sK26(sK36(sK82))) ),
inference(instantiation,[status(thm)],[c_40188]) ).
tcf(c_41940,plain,
! [X0: $i,X1: $i] :
( sP20(X0)
| p2(X1)
| ~ sP21(X0)
| ~ p2(sK25(sK30(X0)))
| ~ r1(sK25(sK30(X0)),X1)
| ~ r1(sK30(X0),sK25(sK30(X0))) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_42325,plain,
sP21(sK72),
inference(global_subsumption_just,[status(thm)],[c_3171,c_21252,c_21250,c_24010,c_26905,c_26906,c_26907,c_26908,c_33717,c_35731,c_40892,c_41268]) ).
tcf(c_42868,plain,
! [X0: $i] :
( sP20(X0)
| p2(sK26(sK30(X0)))
| ~ sP21(X0)
| ~ p2(sK25(sK30(X0)))
| ~ r1(sK30(X0),sK25(sK30(X0)))
| ~ r1(sK25(sK30(X0)),sK26(sK30(X0))) ),
inference(instantiation,[status(thm)],[c_41940]) ).
tcf(c_42870,plain,
( sP20(sK72)
| p2(sK26(sK30(sK72)))
| ~ sP21(sK72)
| ~ p2(sK25(sK30(sK72)))
| ~ r1(sK30(sK72),sK25(sK30(sK72)))
| ~ r1(sK25(sK30(sK72)),sK26(sK30(sK72))) ),
inference(instantiation,[status(thm)],[c_42868]) ).
tcf(c_42871,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_42870,c_42325,c_39326,c_38583,c_24010,c_3669,c_1982,c_1981,c_1980,c_1979,c_1800,c_1799,c_1103,c_826,c_348,c_347,c_326,c_313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL676+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 00:15:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 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.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 31.18/5.34 % SZS status Started for theBenchmark.p
% 31.18/5.34 % SZS status Theorem for theBenchmark.p
% 31.18/5.34
% 31.18/5.34 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 31.18/5.34
% 31.18/5.34 % ------ iProver source info
% 31.18/5.34
% 31.18/5.34 % git: date: 2026-07-19 20:42:38 +0200
% 31.18/5.34 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 31.18/5.34 % git: non_committed_changes: false
% 31.18/5.34
% 31.18/5.34 % ------ Parsing...
% 31.18/5.34 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 31.18/5.34
% 31.18/5.34 % ------ Preprocessing... sf_s rm: 145 0s sf_e sf_s rm: 0 0s sf_e %
% 31.18/5.34
% 31.18/5.34 % ------ Preprocessing...
% 31.18/5.34 % ------ Proving...
% 31.18/5.34 % ------ Problem Properties
% 31.18/5.34
% 31.18/5.34 %
% 31.18/5.34 % clauses 78
% 31.18/5.34 % conjectures 30
% 31.18/5.34 % EPR 17
% 31.18/5.34 % Horn 33
% 31.18/5.34 % unary 5
% 31.18/5.34 % binary 14
% 31.18/5.34 % lits 273
% 31.18/5.34 % lits eq 0
% 31.18/5.34 % fd_pure 0
% 31.18/5.34 % fd_pseudo 0
% 31.18/5.34 % fd_cond 0
% 31.18/5.34 % fd_pseudo_cond 0
% 31.18/5.34 % AC symbols 0
% 31.18/5.34
% 31.18/5.34 % ------ Input Options Time Limit: Unbounded
% 31.18/5.34
% 31.18/5.34
% 31.18/5.34 % ------
% 31.18/5.34 % Current options:
% 31.18/5.34 % ------
% 31.18/5.34
% 31.18/5.34
% 31.18/5.34 %
% 31.18/5.34
% 31.18/5.34 % ------ Proving...
% 31.18/5.34 %
% 31.18/5.34
% 31.18/5.34 % SZS status Theorem for theBenchmark.p
% 31.18/5.34
% 31.18/5.34 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 31.18/5.34
% 31.18/5.34
%------------------------------------------------------------------------------