%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NUN076+1 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 12:34:39 PM UTC 2025
% Result : Theorem 101.10s 13.07s
% Output : CNFRefutation 101.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 13
% Syntax : Number of formulae : 91 ( 38 unt; 0 def)
% Number of atoms : 226 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 244 ( 109 ~; 102 |; 33 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-6 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-2 aty)
% Number of variables : 222 ( 28 sgn 33 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(thereexistsanevennumberid,plain,
? [Y1,Y2,Y3] :
( ? [Y4] :
( id(Y4,Y1)
& ? [Y6] :
( r4(Y6,Y2,Y4)
& ? [Y7] :
( r2(Y7,Y6)
& ? [Y8] :
( r1(Y8)
& r2(Y8,Y7) ) ) ) )
& ? [Y5] :
( id(Y5,Y1)
& r3(Y2,Y3,Y5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thereexistsanevennumberid) ).
fof(thereexistsanevennumberid_negated,plain,
~ ? [Y1,Y2,Y3] :
( ? [Y4] :
( id(Y4,Y1)
& ? [Y6] :
( r4(Y6,Y2,Y4)
& ? [Y7] :
( r2(Y7,Y6)
& ? [Y8] :
( r1(Y8)
& r2(Y8,Y7) ) ) ) )
& ? [Y5] :
( id(Y5,Y1)
& r3(Y2,Y3,Y5) ) ),
inference(negate_conjecture,[status(cth)],[thereexistsanevennumberid]) ).
cnf(58,plain,
( ~ id(X0,X1)
| ~ id(X2,X1)
| ~ r1(X3)
| ~ r2(X4,X5)
| ~ r2(X3,X4)
| ~ r3(X6,X7,X2)
| ~ r4(X5,X6,X0) ),
inference(cnf,[status(esa)],[thereexistsanevennumberid_negated]) ).
cnf(l0,plain,
( ~ id(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK17(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ id(sK1,sK17(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ r1(sK1)
| ~ r2(sK7(X1_5,sK1),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ r2(sK1,sK7(X1_5,sK1))
| ~ r3(sK1,sK14(sK1),sK1)
| ~ r4(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK1,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[58]) ).
fof(axiom_5a,plain,
! [X5] :
? [Y8] :
( ? [Y17] :
( r1(Y17)
& r4(X5,Y17,Y8) )
& ? [Y18] :
( id(Y8,Y18)
& r1(Y18) ) ),
file('Axioms/NUM009+0.ax',axiom_5a) ).
cnf(51,plain,
id(sK15(X0),sK17(X0)),
inference(cnf,[status(esa)],[axiom_5a]) ).
cnf(l2,plain,
id(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK17(sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_1,plain,
? [Y24] :
! [X19] :
( ( id(X19,Y24)
& r1(X19) )
| ( ~ r1(X19)
& ~ id(X19,Y24) ) ),
file('Axioms/NUM009+0.ax',axiom_1) ).
cnf(1,plain,
( sP0(X0)
| r1(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l1,plain,
( sP0(sK1)
| r1(sK1) ),
inference(instantiation,[status(thm)],[1]) ).
fof(axiom_6,plain,
! [X21,X22] :
( ~ id(X21,X22)
| id(X22,X21) ),
file('Axioms/NUM009+0.ax',axiom_6) ).
cnf(17,plain,
( ~ id(X0,X1)
| id(X1,X0) ),
inference(cnf,[status(esa)],[axiom_6]) ).
cnf(l13,plain,
( ~ id(sK17(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK1)
| id(sK1,sK17(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(2,plain,
( ~ id(X0,sK1)
| ~ sP0(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l4,plain,
( ~ id(sK1,sK1)
| ~ sP0(sK1) ),
inference(instantiation,[status(thm)],[2]) ).
fof(axiom_9,plain,
! [X28,X29,X30,X31] :
( ~ id(X28,X30)
| ~ id(X29,X31)
| ( ~ r2(X28,X29)
& ~ r2(X30,X31) )
| ( r2(X28,X29)
& r2(X30,X31) ) ),
file('Axioms/NUM009+0.ax',axiom_9) ).
cnf(26,plain,
( r2(X0,X1)
| ~ sP5(X1,X0,X2,X3) ),
inference(cnf,[status(esa)],[axiom_9]) ).
cnf(l8,plain,
( r2(sK7(X1_5,sK1),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ sP5(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_5,sK1),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK13(sK13(sK7(X1_5,sK1)))) ),
inference(instantiation,[status(thm)],[26]) ).
fof(axiom_1a,plain,
! [X1,X8] :
? [Y4] :
( ? [Y5] :
( id(Y5,Y4)
& ? [Y15] :
( r2(X8,Y15)
& r3(X1,Y15,Y5) ) )
& ? [Y7] :
( r2(Y7,Y4)
& r3(X1,X8,Y7) ) ),
file('Axioms/NUM009+0.ax',axiom_1a) ).
cnf(36,plain,
r2(X0,sK7(X1,X0)),
inference(cnf,[status(esa)],[axiom_1a]) ).
cnf(l5,plain,
r2(sK1,sK7(X1_5,sK1)),
inference(instantiation,[status(thm)],[36]) ).
cnf(24,plain,
( ~ id(X0,X1)
| ~ id(X2,X3)
| ~ r2(X1,X3)
| sP5(X2,X0,X3,X1) ),
inference(cnf,[status(esa)],[axiom_9]) ).
cnf(l9,plain,
( ~ id(sK7(X1_5,sK1),sK13(sK13(sK7(X1_5,sK1))))
| ~ id(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ r2(sK13(sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| sP5(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_5,sK1),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK13(sK13(sK7(X1_5,sK1)))) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(0,plain,
( id(X0,sK1)
| sP0(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l187,plain,
( id(sK17(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK1)
| sP0(sK17(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_10,plain,
! [X32,X33,X34,X35,X36,X37] :
( ~ id(X32,X35)
| ~ id(X33,X36)
| ~ id(X34,X37)
| ( ~ r3(X32,X33,X34)
& ~ r3(X35,X36,X37) )
| ( r3(X32,X33,X34)
& r3(X35,X36,X37) ) ),
file('Axioms/NUM009+0.ax',axiom_10) ).
cnf(29,plain,
( r3(X0,X1,X2)
| ~ sP6(X2,X1,X3,X4,X0,X5) ),
inference(cnf,[status(esa)],[axiom_10]) ).
cnf(l33,plain,
( r3(sK1,sK14(sK1),sK1)
| ~ sP6(sK1,sK14(sK1),sK14(sK1),sK1,sK1,sK13(sK1)) ),
inference(instantiation,[status(thm)],[29]) ).
fof(axiom_7,plain,
! [X23,X24,X25] :
( ~ id(X23,X24)
| id(X23,X25)
| ~ id(X24,X25) ),
file('Axioms/NUM009+0.ax',axiom_7) ).
cnf(18,plain,
( ~ id(X0,X1)
| ~ id(X1,X2)
| id(X0,X2) ),
inference(cnf,[status(esa)],[axiom_7]) ).
cnf(l25,plain,
( ~ id(sK7(X1_5,sK1),sK13(sK7(X1_5,sK1)))
| ~ id(sK13(sK7(X1_5,sK1)),sK13(sK13(sK7(X1_5,sK1))))
| id(sK7(X1_5,sK1),sK13(sK13(sK7(X1_5,sK1)))) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(27,plain,
( ~ id(X0,X1)
| ~ id(X2,X3)
| ~ id(X4,X5)
| ~ r3(X0,X2,X4)
| sP6(X5,X3,X2,X0,X1,X4) ),
inference(cnf,[status(esa)],[axiom_10]) ).
cnf(l38,plain,
( ~ id(sK1,sK1)
| ~ id(sK14(sK1),sK14(sK1))
| ~ id(sK13(sK1),sK1)
| ~ r3(sK1,sK14(sK1),sK13(sK1))
| sP6(sK1,sK14(sK1),sK14(sK1),sK1,sK1,sK13(sK1)) ),
inference(instantiation,[status(thm)],[27]) ).
fof(axiom_5,plain,
! [X20] : id(X20,X20),
file('Axioms/NUM009+0.ax',axiom_5) ).
cnf(16,plain,
id(X0,X0),
inference(cnf,[status(esa)],[axiom_5]) ).
cnf(l10,plain,
id(sK1,sK1),
inference(instantiation,[status(thm)],[16]) ).
fof(axiom_4a,plain,
! [X4] :
? [Y9] :
( id(Y9,X4)
& ? [Y16] :
( r1(Y16)
& r3(X4,Y16,Y9) ) ),
file('Axioms/NUM009+0.ax',axiom_4a) ).
cnf(48,plain,
r3(X0,sK14(X0),sK13(X0)),
inference(cnf,[status(esa)],[axiom_4a]) ).
cnf(l48,plain,
r3(sK1,sK14(sK1),sK13(sK1)),
inference(instantiation,[status(thm)],[48]) ).
cnf(l32,plain,
( ~ id(sK13(sK7(X1_5,sK1)),sK7(X1_5,sK1))
| id(sK7(X1_5,sK1),sK13(sK7(X1_5,sK1))) ),
inference(instantiation,[status(thm)],[17]) ).
fof(axiom_11,plain,
! [X38,X39,X40,X41,X42,X43] :
( ~ id(X38,X41)
| ~ id(X39,X42)
| ~ id(X40,X43)
| ( ~ r4(X38,X39,X40)
& ~ r4(X41,X42,X43) )
| ( r4(X38,X39,X40)
& r4(X41,X42,X43) ) ),
file('Axioms/NUM009+0.ax',axiom_11) ).
cnf(33,plain,
( r4(X0,X1,X2)
| ~ sP7(X2,X1,X3,X4,X0,X5) ),
inference(cnf,[status(esa)],[axiom_11]) ).
cnf(l3,plain,
( r4(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK1,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ sP7(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK1,sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l23,plain,
( r2(sK13(sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ sP5(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK13(sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK13(sK7(X1_5,sK1))) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l35,plain,
( ~ id(sK13(sK13(sK7(X1_5,sK1))),sK13(sK7(X1_5,sK1)))
| id(sK13(sK7(X1_5,sK1)),sK13(sK13(sK7(X1_5,sK1)))) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(3,plain,
( ~ r1(X0)
| ~ sP0(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l188,plain,
( ~ r1(sK17(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ sP0(sK17(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l39,plain,
id(sK14(sK1),sK14(sK1)),
inference(instantiation,[status(thm)],[16]) ).
cnf(46,plain,
id(sK13(X0),X0),
inference(cnf,[status(esa)],[axiom_4a]) ).
cnf(l106,plain,
id(sK13(sK7(X1_5,sK1)),sK7(X1_5,sK1)),
inference(instantiation,[status(thm)],[46]) ).
cnf(l42,plain,
id(sK13(sK1),sK1),
inference(instantiation,[status(thm)],[46]) ).
cnf(52,plain,
r1(sK17(X0)),
inference(cnf,[status(esa)],[axiom_5a]) ).
cnf(l218,plain,
r1(sK17(sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[52]) ).
cnf(l27,plain,
( ~ id(sK13(sK13(sK7(X1_5,sK1))),sK13(sK7(X1_5,sK1)))
| ~ id(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ r2(sK13(sK7(X1_5,sK1)),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| sP5(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK13(sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK13(sK7(X1_5,sK1))) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l65,plain,
id(sK13(sK13(sK7(X1_5,sK1))),sK13(sK7(X1_5,sK1))),
inference(instantiation,[status(thm)],[46]) ).
fof(axiom_3a,plain,
! [X3,X10] :
( ! [Y12] :
( ! [Y13] :
( ~ id(Y13,Y12)
| ~ r2(X3,Y13) )
| ~ r2(X10,Y12) )
| id(X3,X10) ),
file('Axioms/NUM009+0.ax',axiom_3a) ).
cnf(45,plain,
( ~ id(X0,X1)
| ~ r2(X2,X0)
| ~ r2(X3,X1)
| id(X2,X3) ),
inference(cnf,[status(esa)],[axiom_3a]) ).
cnf(l44,plain,
( ~ id(sK11(X1_49,sK1),sK11(X1_49,sK1))
| ~ r2(sK1,sK11(X1_49,sK1))
| ~ r2(sK1,sK11(X1_49,sK1))
| id(sK1,sK1) ),
inference(instantiation,[status(thm)],[45]) ).
fof(axiom_2a,plain,
! [X2,X9] :
? [Y2] :
( ? [Y3] :
( id(Y3,Y2)
& ? [Y14] :
( r2(X9,Y14)
& r4(X2,Y14,Y3) ) )
& ? [Y6] :
( r3(Y6,X2,Y2)
& r4(X2,X9,Y6) ) ),
file('Axioms/NUM009+0.ax',axiom_2a) ).
cnf(41,plain,
r2(X0,sK11(X1,X0)),
inference(cnf,[status(esa)],[axiom_2a]) ).
cnf(l73,plain,
r2(sK1,sK11(X1_49,sK1)),
inference(instantiation,[status(thm)],[41]) ).
cnf(31,plain,
( ~ id(X0,X1)
| ~ id(X2,X3)
| ~ id(X4,X5)
| ~ r4(X0,X2,X4)
| sP7(X5,X3,X2,X0,X1,X4) ),
inference(cnf,[status(esa)],[axiom_11]) ).
cnf(l7,plain,
( ~ id(sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ id(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK1)
| ~ id(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ r4(sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| sP7(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK1,sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l16,plain,
id(sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1)))),
inference(instantiation,[status(thm)],[46]) ).
cnf(l19,plain,
( ~ id(sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ r2(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ r2(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| id(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1)))) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l41,plain,
r2(sK13(sK7(X1_5,sK1)),sK7(X1_41,sK13(sK7(X1_5,sK1)))),
inference(instantiation,[status(thm)],[36]) ).
cnf(l52,plain,
r2(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[36]) ).
cnf(l15,plain,
( ~ id(sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))),sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))))
| ~ r2(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))))
| ~ r2(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))))
| id(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l20,plain,
id(sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[16]) ).
cnf(l57,plain,
r2(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))),
inference(instantiation,[status(thm)],[36]) ).
cnf(l36,plain,
id(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_41,sK13(sK7(X1_5,sK1)))),
inference(instantiation,[status(thm)],[16]) ).
cnf(l37,plain,
id(sK13(sK13(sK7(X1_5,sK1))),sK13(sK7(X1_5,sK1))),
inference(instantiation,[status(thm)],[46]) ).
cnf(l49,plain,
r2(sK1,sK11(X1_49,sK1)),
inference(instantiation,[status(thm)],[41]) ).
cnf(l208,plain,
r2(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK7(X1_208,sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[36]) ).
cnf(l24,plain,
r2(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))),
inference(instantiation,[status(thm)],[36]) ).
cnf(34,plain,
( r4(X0,X1,X2)
| ~ sP7(X3,X4,X1,X0,X5,X2) ),
inference(cnf,[status(esa)],[axiom_11]) ).
cnf(l14,plain,
( r4(sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ sP7(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l12,plain,
( id(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK1)
| sP0(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l55,plain,
id(sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))),sK7(X1_57,sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))),
inference(instantiation,[status(thm)],[16]) ).
cnf(l46,plain,
id(sK11(X1_49,sK1),sK11(X1_49,sK1)),
inference(instantiation,[status(thm)],[16]) ).
cnf(32,plain,
( ~ id(X0,X1)
| ~ id(X2,X3)
| ~ id(X4,X5)
| ~ r4(X1,X3,X5)
| sP7(X5,X3,X2,X0,X1,X4) ),
inference(cnf,[status(esa)],[axiom_11]) ).
cnf(l113,plain,
( ~ id(sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1))))
| ~ id(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ id(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ r4(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| sP7(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l129,plain,
( ~ r1(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))))
| ~ sP0(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l124,plain,
id(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[16]) ).
cnf(49,plain,
r1(sK16(X0)),
inference(cnf,[status(esa)],[axiom_5a]) ).
cnf(l132,plain,
r1(sK16(sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[49]) ).
cnf(l114,plain,
id(sK13(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK7(X1_41,sK13(sK7(X1_5,sK1)))),
inference(instantiation,[status(thm)],[46]) ).
cnf(l130,plain,
id(sK15(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[16]) ).
cnf(50,plain,
r4(X0,sK16(X0),sK15(X0)),
inference(cnf,[status(esa)],[axiom_5a]) ).
cnf(l126,plain,
r4(sK7(X1_41,sK13(sK7(X1_5,sK1))),sK16(sK7(X1_41,sK13(sK7(X1_5,sK1)))),sK15(sK7(X1_41,sK13(sK7(X1_5,sK1))))),
inference(instantiation,[status(thm)],[50]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l2,l1,l13,l4,l8,l5,l9,l187,l33,l25,l38,l10,l48,l32,l3,l23,l35,l188,l39,l106,l42,l218,l27,l65,l44,l73,l7,l16,l19,l41,l52,l15,l20,l57,l36,l37,l49,l208,l24,l14,l12,l55,l46,l113,l129,l124,l132,l114,l130,l126]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN076+1 : TPTP v9.0.0. Released v7.3.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Jul 21 14:47:34 EDT 2025
% 0.18/0.33 % CPUTime :
% 0.18/0.34 % launching worker at depth: 4
% 0.18/0.34 % launching worker at depth: 8
% 0.18/0.34 % launching worker at depth: 5
% 0.18/0.34 % launching worker at depth: 2
% 0.18/0.34 % launching worker at depth: 3
% 0.18/0.34 % launching worker at depth: 6
% 0.18/0.34 % launching worker at depth: 7
% 0.18/0.34 % launching worker at depth: 1
% 0.18/0.35 % launching worker at depth: 9
% 0.18/0.49 % launching worker at depth: 10
% 101.10/13.07 % SZS status Theorem for theBenchmark
% 101.10/13.07 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------