%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : KRS157+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n032.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 : Thu Jul 24 08:46:46 PM UTC 2025
% Result : Theorem 0.14s 0.32s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 20
% Syntax : Number of formulae : 146 ( 73 unt; 0 def)
% Number of atoms : 322 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 320 ( 144 ~; 138 |; 28 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 29 ( 2 sgn 13 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(the_axiom,plain,
( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC14(iV3102)
& cC44(iV3102)
& cC216(iV3102)
& cC64(iV3102)
& cC46(iV3102)
& cC28(iV3102)
& cowlThing(iV3102)
& cC30(iV3102) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(the_axiom_negated,plain,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC14(iV3102)
& cC44(iV3102)
& cC216(iV3102)
& cC64(iV3102)
& cC46(iV3102)
& cC28(iV3102)
& cowlThing(iV3102)
& cC30(iV3102) ),
inference(negate_conjecture,[status(cth)],[the_axiom]) ).
cnf(527,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK250)
| ~ xsd_integer(sK251)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC44(iV3102)
| cowlNothing(sK250)
| xsd_string(sK251) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l0,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK250)
| ~ xsd_integer(sK251)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC44(iV3102)
| cowlNothing(sK250)
| xsd_string(sK251) ),
inference(instantiation,[status(thm)],[527]) ).
fof(axiom_201,plain,
! [X] :
( cTEST(X)
<=> ( cC216(X)
& cC46(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_201) ).
cnf(507,plain,
( ~ cTEST(X0)
| cC216(X0) ),
inference(cnf,[status(esa)],[axiom_201]) ).
cnf(l1,plain,
( ~ cTEST(iV3102)
| cC216(iV3102) ),
inference(instantiation,[status(thm)],[507]) ).
fof(axiom_217,plain,
cowlThing(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_217) ).
cnf(525,plain,
cowlThing(iV3102),
inference(cnf,[status(esa)],[axiom_217]) ).
cnf(l2,plain,
cowlThing(iV3102),
inference(instantiation,[status(thm)],[525]) ).
fof(axiom_44,plain,
! [X] :
( cC14(X)
<=> ( cC2xcomp(X)
& cC12xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
cnf(112,plain,
( ~ cC2xcomp(X0)
| ~ cC12xcomp(X0)
| cC14(X0) ),
inference(cnf,[status(esa)],[axiom_44]) ).
cnf(l3,plain,
( ~ cC2xcomp(iV3102)
| ~ cC12xcomp(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[112]) ).
fof(axiom_202,plain,
cTEST(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_202) ).
cnf(510,plain,
cTEST(iV3102),
inference(cnf,[status(esa)],[axiom_202]) ).
cnf(l4,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
fof(axiom_215,plain,
cC12xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_215) ).
cnf(523,plain,
cC12xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_215]) ).
cnf(l5,plain,
cC12xcomp(iV3102),
inference(instantiation,[status(thm)],[523]) ).
fof(axiom_0,plain,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
cnf(0,plain,
cowlThing(X0),
inference(cnf,[status(esa)],[axiom_0]) ).
cnf(l6,plain,
cowlThing(sK250),
inference(instantiation,[status(thm)],[0]) ).
cnf(528,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK250)
| ~ xsd_string(sK251)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC44(iV3102)
| cowlNothing(sK250)
| xsd_integer(sK251) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l7,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK250)
| ~ xsd_string(sK251)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC44(iV3102)
| cowlNothing(sK250)
| xsd_integer(sK251) ),
inference(instantiation,[status(thm)],[528]) ).
cnf(l8,plain,
cowlThing(iV3102),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_132,plain,
! [X] :
( cC30(X)
<=> ( cC28(X)
& cC14(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_132) ).
cnf(333,plain,
( ~ cC30(X0)
| cC14(X0) ),
inference(cnf,[status(esa)],[axiom_132]) ).
cnf(l9,plain,
( ~ cC30(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[333]) ).
fof(axiom_1,plain,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
cnf(2,plain,
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l10,plain,
( ~ xsd_string(sK251)
| ~ xsd_integer(sK251) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(332,plain,
( ~ cC30(X0)
| cC28(X0) ),
inference(cnf,[status(esa)],[axiom_132]) ).
cnf(l11,plain,
( ~ cC30(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[332]) ).
cnf(l12,plain,
cowlThing(sK250),
inference(instantiation,[status(thm)],[0]) ).
cnf(1,plain,
~ cowlNothing(X0),
inference(cnf,[status(esa)],[axiom_0]) ).
cnf(l13,plain,
~ cowlNothing(sK250),
inference(instantiation,[status(thm)],[1]) ).
fof(axiom_166,plain,
! [X] :
( cC64(X)
<=> ( cC62xcomp(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_166) ).
cnf(420,plain,
( ~ cC62xcomp(X0)
| ~ cTOP(X0)
| cC64(X0) ),
inference(cnf,[status(esa)],[axiom_166]) ).
cnf(l19,plain,
( ~ cC62xcomp(iV3102)
| ~ cTOP(iV3102)
| cC64(iV3102) ),
inference(instantiation,[status(thm)],[420]) ).
fof(axiom_148,plain,
! [X] :
( cC46(X)
<=> ( cC30(X)
& cC44(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_148) ).
cnf(372,plain,
( ~ cC46(X0)
| cC30(X0) ),
inference(cnf,[status(esa)],[axiom_148]) ).
cnf(l14,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[372]) ).
fof(axiom_205,plain,
cTOP(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_205) ).
cnf(513,plain,
cTOP(iV3102),
inference(cnf,[status(esa)],[axiom_205]) ).
cnf(l61,plain,
cTOP(iV3102),
inference(instantiation,[status(thm)],[513]) ).
cnf(l39,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[372]) ).
fof(axiom_203,plain,
cC2xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_203) ).
cnf(511,plain,
cC2xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_203]) ).
cnf(l15,plain,
cC2xcomp(iV3102),
inference(instantiation,[status(thm)],[511]) ).
cnf(l16,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK250)
| ~ xsd_string(sK251)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC44(iV3102)
| cowlNothing(sK250)
| xsd_integer(sK251) ),
inference(instantiation,[status(thm)],[528]) ).
cnf(508,plain,
( ~ cTEST(X0)
| cC46(X0) ),
inference(cnf,[status(esa)],[axiom_201]) ).
cnf(l43,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
fof(axiom_147,plain,
! [X] :
( cC44(X)
<=> ( cC42xcomp(X)
& cC32xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_147) ).
cnf(371,plain,
( ~ cC32xcomp(X0)
| ~ cC42xcomp(X0)
| cC44(X0) ),
inference(cnf,[status(esa)],[axiom_147]) ).
cnf(l40,plain,
( ~ cC32xcomp(iV3102)
| ~ cC42xcomp(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[371]) ).
fof(axiom_212,plain,
cC62xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_212) ).
cnf(520,plain,
cC62xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_212]) ).
cnf(l59,plain,
cC62xcomp(iV3102),
inference(instantiation,[status(thm)],[520]) ).
cnf(l67,plain,
( ~ cC30(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[332]) ).
cnf(l83,plain,
( ~ cC62xcomp(iV3102)
| ~ cTOP(iV3102)
| cC64(iV3102) ),
inference(instantiation,[status(thm)],[420]) ).
cnf(l22,plain,
~ cowlNothing(sK250),
inference(instantiation,[status(thm)],[1]) ).
cnf(l84,plain,
cowlThing(sK250),
inference(instantiation,[status(thm)],[0]) ).
cnf(l33,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[372]) ).
cnf(l37,plain,
( ~ cTEST(iV3102)
| cC216(iV3102) ),
inference(instantiation,[status(thm)],[507]) ).
cnf(l81,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
cnf(l17,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[372]) ).
cnf(l44,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l20,plain,
cowlThing(iV3102),
inference(instantiation,[status(thm)],[525]) ).
cnf(334,plain,
( ~ cC14(X0)
| ~ cC28(X0)
| cC30(X0) ),
inference(cnf,[status(esa)],[axiom_132]) ).
cnf(l89,plain,
( ~ cC14(iV3102)
| ~ cC28(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[334]) ).
cnf(l85,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(373,plain,
( ~ cC46(X0)
| cC44(X0) ),
inference(cnf,[status(esa)],[axiom_148]) ).
cnf(l90,plain,
( ~ cC46(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[373]) ).
fof(axiom_131,plain,
! [X] :
( cC28(X)
<=> ( cC16xcomp(X)
& cC26xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_131) ).
cnf(331,plain,
( ~ cC16xcomp(X0)
| ~ cC26xcomp(X0)
| cC28(X0) ),
inference(cnf,[status(esa)],[axiom_131]) ).
cnf(l91,plain,
( ~ cC16xcomp(iV3102)
| ~ cC26xcomp(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[331]) ).
cnf(l26,plain,
( ~ cC16xcomp(iV3102)
| ~ cC26xcomp(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[331]) ).
cnf(374,plain,
( ~ cC30(X0)
| ~ cC44(X0)
| cC46(X0) ),
inference(cnf,[status(esa)],[axiom_148]) ).
cnf(l34,plain,
( ~ cC30(iV3102)
| ~ cC44(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[374]) ).
cnf(l24,plain,
~ cowlNothing(sK250),
inference(instantiation,[status(thm)],[1]) ).
cnf(l45,plain,
( ~ cC46(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[373]) ).
cnf(l79,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[372]) ).
cnf(l52,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
fof(axiom_207,plain,
cC32xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_207) ).
cnf(515,plain,
cC32xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_207]) ).
cnf(l41,plain,
cC32xcomp(iV3102),
inference(instantiation,[status(thm)],[515]) ).
cnf(l35,plain,
( ~ cC32xcomp(iV3102)
| ~ cC42xcomp(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[371]) ).
cnf(l95,plain,
( ~ cC14(iV3102)
| ~ cC28(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[334]) ).
cnf(3,plain,
( xsd_string(X0)
| xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l21,plain,
( xsd_string(sK251)
| xsd_integer(sK251) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l32,plain,
( ~ cC62xcomp(iV3102)
| ~ cTOP(iV3102)
| cC64(iV3102) ),
inference(instantiation,[status(thm)],[420]) ).
cnf(l98,plain,
cC62xcomp(iV3102),
inference(instantiation,[status(thm)],[520]) ).
cnf(l76,plain,
cTOP(iV3102),
inference(instantiation,[status(thm)],[513]) ).
cnf(l86,plain,
cTOP(iV3102),
inference(instantiation,[status(thm)],[513]) ).
cnf(l74,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l107,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l25,plain,
( ~ cTEST(iV3102)
| cC216(iV3102) ),
inference(instantiation,[status(thm)],[507]) ).
cnf(l36,plain,
( ~ cC30(iV3102)
| ~ cC44(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[374]) ).
cnf(l110,plain,
( ~ cC2xcomp(iV3102)
| ~ cC12xcomp(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l28,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l71,plain,
( ~ cC32xcomp(iV3102)
| ~ cC42xcomp(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[371]) ).
cnf(l69,plain,
( ~ cC14(iV3102)
| ~ cC28(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[334]) ).
cnf(l99,plain,
( ~ cC2xcomp(iV3102)
| ~ cC12xcomp(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l121,plain,
cC12xcomp(iV3102),
inference(instantiation,[status(thm)],[523]) ).
cnf(l104,plain,
cC32xcomp(iV3102),
inference(instantiation,[status(thm)],[515]) ).
fof(axiom_210,plain,
cC16xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_210) ).
cnf(518,plain,
cC16xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_210]) ).
cnf(l92,plain,
cC16xcomp(iV3102),
inference(instantiation,[status(thm)],[518]) ).
fof(axiom_206,plain,
cC26xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_206) ).
cnf(514,plain,
cC26xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_206]) ).
cnf(l93,plain,
cC26xcomp(iV3102),
inference(instantiation,[status(thm)],[514]) ).
cnf(l87,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
cnf(l73,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
cnf(l51,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
cnf(l109,plain,
( ~ cC16xcomp(iV3102)
| ~ cC26xcomp(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[331]) ).
cnf(l103,plain,
cC2xcomp(iV3102),
inference(instantiation,[status(thm)],[511]) ).
cnf(l23,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
cnf(l96,plain,
( ~ cC2xcomp(iV3102)
| ~ cC12xcomp(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l77,plain,
cC62xcomp(iV3102),
inference(instantiation,[status(thm)],[520]) ).
cnf(l106,plain,
cC26xcomp(iV3102),
inference(instantiation,[status(thm)],[514]) ).
fof(axiom_211,plain,
cC42xcomp(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_211) ).
cnf(519,plain,
cC42xcomp(iV3102),
inference(cnf,[status(esa)],[axiom_211]) ).
cnf(l94,plain,
cC42xcomp(iV3102),
inference(instantiation,[status(thm)],[519]) ).
cnf(l105,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[508]) ).
cnf(l102,plain,
cC12xcomp(iV3102),
inference(instantiation,[status(thm)],[523]) ).
cnf(l119,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l127,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l126,plain,
cC16xcomp(iV3102),
inference(instantiation,[status(thm)],[518]) ).
cnf(l130,plain,
cC26xcomp(iV3102),
inference(instantiation,[status(thm)],[514]) ).
cnf(l135,plain,
cC12xcomp(iV3102),
inference(instantiation,[status(thm)],[523]) ).
cnf(l115,plain,
cC42xcomp(iV3102),
inference(instantiation,[status(thm)],[519]) ).
cnf(l55,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l137,plain,
cC32xcomp(iV3102),
inference(instantiation,[status(thm)],[515]) ).
cnf(l97,plain,
cC2xcomp(iV3102),
inference(instantiation,[status(thm)],[511]) ).
cnf(l72,plain,
( ~ cC2xcomp(iV3102)
| ~ cC12xcomp(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l78,plain,
cC2xcomp(iV3102),
inference(instantiation,[status(thm)],[511]) ).
cnf(l129,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l75,plain,
cC12xcomp(iV3102),
inference(instantiation,[status(thm)],[523]) ).
cnf(l140,plain,
( ~ cC16xcomp(iV3102)
| ~ cC26xcomp(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[331]) ).
cnf(l70,plain,
cC42xcomp(iV3102),
inference(instantiation,[status(thm)],[519]) ).
cnf(l30,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[510]) ).
cnf(l143,plain,
cC26xcomp(iV3102),
inference(instantiation,[status(thm)],[514]) ).
cnf(l141,plain,
cC16xcomp(iV3102),
inference(instantiation,[status(thm)],[518]) ).
cnf(l122,plain,
cC2xcomp(iV3102),
inference(instantiation,[status(thm)],[511]) ).
cnf(l31,plain,
cC16xcomp(iV3102),
inference(instantiation,[status(thm)],[518]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l19,l14,l61,l39,l15,l16,l43,l40,l59,l67,l83,l22,l84,l33,l37,l81,l17,l44,l20,l89,l85,l90,l91,l26,l34,l24,l45,l79,l52,l41,l35,l95,l21,l32,l98,l76,l86,l74,l107,l25,l36,l110,l28,l71,l69,l99,l121,l104,l92,l93,l87,l73,l51,l109,l103,l23,l96,l77,l106,l94,l105,l102,l119,l127,l126,l130,l135,l115,l55,l137,l97,l72,l78,l129,l75,l140,l70,l30,l143,l141,l122,l31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : KRS157+1 : TPTP v9.0.0. Released v3.1.0.
% 0.02/0.10 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Sun Jul 20 22:16:19 EDT 2025
% 0.10/0.29 % CPUTime :
% 0.10/0.30 % launching worker at depth: 5
% 0.10/0.30 % launching worker at depth: 2
% 0.10/0.30 % launching worker at depth: 3
% 0.10/0.30 % launching worker at depth: 1
% 0.10/0.30 % launching worker at depth: 8
% 0.10/0.30 % launching worker at depth: 4
% 0.10/0.30 % launching worker at depth: 6
% 0.10/0.30 % launching worker at depth: 7
% 0.10/0.30 % launching worker at depth: 9
% 0.10/0.31 % launching worker at depth: 10
% 0.14/0.31 % launching worker at depth: 11
% 0.14/0.32 % SZS status Theorem for theBenchmark
% 0.14/0.32 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------