%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : KRS154+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 : n031.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.19s 0.42s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 24
% Syntax : Number of formulae : 175 ( 104 unt; 0 def)
% Number of atoms : 381 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 376 ( 170 ~; 164 |; 31 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 26 ( 2 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(the_axiom,plain,
( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC58(iV822576)
& cC116(iV822576)
& cC114(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& cC80(iV822576)
& cC110(iV822576)
& cC136(iV822576)
& cC56(iV822576) ),
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) )
& cC58(iV822576)
& cC116(iV822576)
& cC114(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& cC80(iV822576)
& cC110(iV822576)
& cC136(iV822576)
& cC56(iV822576) ),
inference(negate_conjecture,[status(cth)],[the_axiom]) ).
cnf(381,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK144)
| ~ xsd_integer(sK145)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| cowlNothing(sK144)
| xsd_string(sK145) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l0,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK144)
| ~ xsd_integer(sK145)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| cowlNothing(sK144)
| xsd_string(sK145) ),
inference(instantiation,[status(thm)],[381]) ).
fof(axiom_21,plain,
! [X] :
( cC114(X)
<=> ( cC112xcomp(X)
& cC96xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
cnf(51,plain,
( ~ cC112xcomp(X0)
| ~ cC96xcomp(X0)
| cC114(X0) ),
inference(cnf,[status(esa)],[axiom_21]) ).
cnf(l1,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_22,plain,
! [X] :
( cC116(X)
<=> ( cC114(X)
& cC80(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
cnf(54,plain,
( ~ cC114(X0)
| ~ cC80(X0)
| cC116(X0) ),
inference(cnf,[status(esa)],[axiom_22]) ).
cnf(l30,plain,
( ~ cC114(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[54]) ).
fof(axiom_15,plain,
! [X] :
( cC110(X)
<=> ( cC102xcomp(X)
& cC108xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
cnf(37,plain,
( ~ cC102xcomp(X0)
| ~ cC108xcomp(X0)
| cC110(X0) ),
inference(cnf,[status(esa)],[axiom_15]) ).
cnf(l3,plain,
( ~ cC102xcomp(iV822576)
| ~ cC108xcomp(iV822576)
| cC110(iV822576) ),
inference(instantiation,[status(thm)],[37]) ).
fof(axiom_147,plain,
cC102xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_147) ).
cnf(359,plain,
cC102xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_147]) ).
cnf(l44,plain,
cC102xcomp(iV822576),
inference(instantiation,[status(thm)],[359]) ).
fof(axiom_94,plain,
! [X] :
( cC58(X)
<=> ( cC34(X)
& cC56(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_94) ).
cnf(232,plain,
( ~ cC34(X0)
| ~ cC56(X0)
| cC58(X0) ),
inference(cnf,[status(esa)],[axiom_94]) ).
cnf(l19,plain,
( ~ cC34(iV822576)
| ~ cC56(iV822576)
| cC58(iV822576) ),
inference(instantiation,[status(thm)],[232]) ).
fof(axiom_93,plain,
! [X] :
( cC56(X)
<=> ( cC4(X)
& cC10xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_93) ).
cnf(229,plain,
( ~ cC10xcomp(X0)
| ~ cC4(X0)
| cC56(X0) ),
inference(cnf,[status(esa)],[axiom_93]) ).
cnf(l57,plain,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[229]) ).
cnf(l35,plain,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[229]) ).
cnf(382,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK144)
| ~ xsd_string(sK145)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| cowlNothing(sK144)
| xsd_integer(sK145) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l29,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK144)
| ~ xsd_string(sK145)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| cowlNothing(sK144)
| xsd_integer(sK145) ),
inference(instantiation,[status(thm)],[382]) ).
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(l79,plain,
cowlThing(sK144),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_117,plain,
! [X] :
( cC80(X)
<=> ( cC78xcomp(X)
& cC76xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_117) ).
cnf(291,plain,
( ~ cC76xcomp(X0)
| ~ cC78xcomp(X0)
| cC80(X0) ),
inference(cnf,[status(esa)],[axiom_117]) ).
cnf(l152,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l2,plain,
cowlThing(iV822576),
inference(instantiation,[status(thm)],[0]) ).
cnf(l78,plain,
( ~ cC102xcomp(iV822576)
| ~ cC108xcomp(iV822576)
| cC110(iV822576) ),
inference(instantiation,[status(thm)],[37]) ).
fof(axiom_42,plain,
! [X] :
( cC136(X)
<=> ( cC134xcomp(X)
& cC116(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_42) ).
cnf(105,plain,
( ~ cC116(X0)
| ~ cC134xcomp(X0)
| cC136(X0) ),
inference(cnf,[status(esa)],[axiom_42]) ).
cnf(l15,plain,
( ~ cC116(iV822576)
| ~ cC134xcomp(iV822576)
| cC136(iV822576) ),
inference(instantiation,[status(thm)],[105]) ).
cnf(l11,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
fof(axiom_158,plain,
cC78xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_158) ).
cnf(370,plain,
cC78xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_158]) ).
cnf(l65,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
fof(axiom_152,plain,
cC76xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_152) ).
cnf(364,plain,
cC76xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_152]) ).
cnf(l156,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l159,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
fof(axiom_148,plain,
cC108xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_148) ).
cnf(360,plain,
cC108xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_148]) ).
cnf(l127,plain,
cC108xcomp(iV822576),
inference(instantiation,[status(thm)],[360]) ).
cnf(l90,plain,
( ~ cC116(iV822576)
| ~ cC134xcomp(iV822576)
| cC136(iV822576) ),
inference(instantiation,[status(thm)],[105]) ).
cnf(1,plain,
~ cowlNothing(X0),
inference(cnf,[status(esa)],[axiom_0]) ).
cnf(l110,plain,
~ cowlNothing(sK144),
inference(instantiation,[status(thm)],[1]) ).
fof(axiom_136,plain,
! [X] :
( cC94(X)
<=> ( cC86xcomp(X)
& cC92xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_136) ).
cnf(336,plain,
( ~ cC86xcomp(X0)
| ~ cC92xcomp(X0)
| cC94(X0) ),
inference(cnf,[status(esa)],[axiom_136]) ).
cnf(l14,plain,
( ~ cC86xcomp(iV822576)
| ~ cC92xcomp(iV822576)
| cC94(iV822576) ),
inference(instantiation,[status(thm)],[336]) ).
fof(axiom_153,plain,
cC96xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_153) ).
cnf(365,plain,
cC96xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_153]) ).
cnf(l150,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
fof(axiom_161,plain,
cC86xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_161) ).
cnf(373,plain,
cC86xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_161]) ).
cnf(l34,plain,
cC86xcomp(iV822576),
inference(instantiation,[status(thm)],[373]) ).
cnf(l6,plain,
cowlThing(sK144),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_160,plain,
cC134xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_160) ).
cnf(372,plain,
cC134xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_160]) ).
cnf(l104,plain,
cC134xcomp(iV822576),
inference(instantiation,[status(thm)],[372]) ).
cnf(l84,plain,
( ~ cC86xcomp(iV822576)
| ~ cC92xcomp(iV822576)
| cC94(iV822576) ),
inference(instantiation,[status(thm)],[336]) ).
fof(axiom_168,plain,
cC92xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_168) ).
cnf(380,plain,
cC92xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_168]) ).
cnf(l59,plain,
cC92xcomp(iV822576),
inference(instantiation,[status(thm)],[380]) ).
fof(axiom_167,plain,
cC10xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_167) ).
cnf(379,plain,
cC10xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_167]) ).
cnf(l61,plain,
cC10xcomp(iV822576),
inference(instantiation,[status(thm)],[379]) ).
cnf(l106,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l108,plain,
cC92xcomp(iV822576),
inference(instantiation,[status(thm)],[380]) ).
fof(axiom_166,plain,
cowlThing(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_166) ).
cnf(378,plain,
cowlThing(iV822576),
inference(cnf,[status(esa)],[axiom_166]) ).
cnf(l36,plain,
cowlThing(iV822576),
inference(instantiation,[status(thm)],[378]) ).
cnf(l125,plain,
cC102xcomp(iV822576),
inference(instantiation,[status(thm)],[359]) ).
cnf(l83,plain,
( ~ cC34(iV822576)
| ~ cC56(iV822576)
| cC58(iV822576) ),
inference(instantiation,[status(thm)],[232]) ).
cnf(l80,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_151,plain,
cC112xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_151) ).
cnf(363,plain,
cC112xcomp(iV822576),
inference(cnf,[status(esa)],[axiom_151]) ).
cnf(l4,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l111,plain,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[229]) ).
cnf(l218,plain,
cC10xcomp(iV822576),
inference(instantiation,[status(thm)],[379]) ).
cnf(l99,plain,
( ~ cC114(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l180,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l141,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l168,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l143,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l186,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l5,plain,
cC108xcomp(iV822576),
inference(instantiation,[status(thm)],[360]) ).
cnf(l27,plain,
cC134xcomp(iV822576),
inference(instantiation,[status(thm)],[372]) ).
fof(axiom_162,plain,
cC34(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_162) ).
cnf(374,plain,
cC34(iV822576),
inference(cnf,[status(esa)],[axiom_162]) ).
cnf(l32,plain,
cC34(iV822576),
inference(instantiation,[status(thm)],[374]) ).
fof(axiom_149,plain,
cC4(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_149) ).
cnf(361,plain,
cC4(iV822576),
inference(cnf,[status(esa)],[axiom_149]) ).
cnf(l37,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[361]) ).
cnf(l93,plain,
cC86xcomp(iV822576),
inference(instantiation,[status(thm)],[373]) ).
cnf(l92,plain,
cC34(iV822576),
inference(instantiation,[status(thm)],[374]) ).
cnf(l185,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l81,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l182,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l173,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l7,plain,
~ cowlNothing(sK144),
inference(instantiation,[status(thm)],[1]) ).
cnf(l139,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l77,plain,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[229]) ).
cnf(l177,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l101,plain,
( ~ cC114(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l68,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[361]) ).
cnf(l85,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l179,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[361]) ).
cnf(l97,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l131,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l21,plain,
( ~ cC114(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l202,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l130,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l200,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l189,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l100,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l87,plain,
cC10xcomp(iV822576),
inference(instantiation,[status(thm)],[379]) ).
fof(axiom_1,plain,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
cnf(3,plain,
( xsd_string(X0)
| xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l82,plain,
( xsd_string(sK145)
| xsd_integer(sK145) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l129,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l253,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l201,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l187,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l9,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK144)
| ~ xsd_string(sK145)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| cowlNothing(sK144)
| xsd_integer(sK145) ),
inference(instantiation,[status(thm)],[382]) ).
cnf(l13,plain,
cowlThing(sK144),
inference(instantiation,[status(thm)],[0]) ).
cnf(l22,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l96,plain,
cC10xcomp(iV822576),
inference(instantiation,[status(thm)],[379]) ).
cnf(l134,plain,
( ~ cC102xcomp(iV822576)
| ~ cC108xcomp(iV822576)
| cC110(iV822576) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l137,plain,
cC108xcomp(iV822576),
inference(instantiation,[status(thm)],[360]) ).
cnf(l164,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l163,plain,
cC102xcomp(iV822576),
inference(instantiation,[status(thm)],[359]) ).
cnf(l28,plain,
( ~ cC114(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l20,plain,
( ~ cC116(iV822576)
| ~ cC134xcomp(iV822576)
| cC136(iV822576) ),
inference(instantiation,[status(thm)],[105]) ).
cnf(l138,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l157,plain,
cC134xcomp(iV822576),
inference(instantiation,[status(thm)],[372]) ).
cnf(l147,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l18,plain,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[229]) ).
cnf(l222,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l26,plain,
( ~ cC86xcomp(iV822576)
| ~ cC92xcomp(iV822576)
| cC94(iV822576) ),
inference(instantiation,[status(thm)],[336]) ).
cnf(l23,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l123,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(2,plain,
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l17,plain,
( ~ xsd_string(sK145)
| ~ xsd_integer(sK145) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l155,plain,
( ~ cC114(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l224,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l299,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l113,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[361]) ).
cnf(l160,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l267,plain,
( ~ cC76xcomp(iV822576)
| ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(instantiation,[status(thm)],[291]) ).
cnf(l166,plain,
cC92xcomp(iV822576),
inference(instantiation,[status(thm)],[380]) ).
cnf(l136,plain,
( ~ cC112xcomp(iV822576)
| ~ cC96xcomp(iV822576)
| cC114(iV822576) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l158,plain,
cC86xcomp(iV822576),
inference(instantiation,[status(thm)],[373]) ).
cnf(l135,plain,
cowlThing(iV822576),
inference(instantiation,[status(thm)],[378]) ).
cnf(l124,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l281,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l145,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l12,plain,
( ~ cC34(iV822576)
| ~ cC56(iV822576)
| cC58(iV822576) ),
inference(instantiation,[status(thm)],[232]) ).
cnf(l149,plain,
cC10xcomp(iV822576),
inference(instantiation,[status(thm)],[379]) ).
cnf(l10,plain,
~ cowlNothing(sK144),
inference(instantiation,[status(thm)],[1]) ).
cnf(l167,plain,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[229]) ).
cnf(l270,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l300,plain,
cC96xcomp(iV822576),
inference(instantiation,[status(thm)],[365]) ).
cnf(l171,plain,
cC10xcomp(iV822576),
inference(instantiation,[status(thm)],[379]) ).
cnf(l140,plain,
cC76xcomp(iV822576),
inference(instantiation,[status(thm)],[364]) ).
cnf(l146,plain,
cC112xcomp(iV822576),
inference(instantiation,[status(thm)],[363]) ).
cnf(l226,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l126,plain,
cC78xcomp(iV822576),
inference(instantiation,[status(thm)],[370]) ).
cnf(l170,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[361]) ).
cnf(l148,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[361]) ).
cnf(l165,plain,
cC34(iV822576),
inference(instantiation,[status(thm)],[374]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l30,l3,l44,l19,l57,l35,l29,l79,l152,l2,l78,l15,l11,l65,l156,l159,l127,l90,l110,l14,l150,l34,l6,l104,l84,l59,l61,l106,l108,l36,l125,l83,l80,l4,l111,l218,l99,l180,l141,l168,l143,l186,l5,l27,l32,l37,l93,l92,l185,l81,l182,l173,l7,l139,l77,l177,l101,l68,l85,l179,l97,l131,l21,l202,l130,l200,l189,l100,l87,l82,l129,l253,l201,l187,l9,l13,l22,l96,l134,l137,l164,l163,l28,l20,l138,l157,l147,l18,l222,l26,l23,l123,l17,l155,l224,l299,l113,l160,l267,l166,l136,l158,l135,l124,l281,l145,l12,l149,l10,l167,l270,l300,l171,l140,l146,l226,l126,l170,l148,l165]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS154+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n031.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 22:16:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.35 % launching worker at depth: 11
% 0.12/0.37 % launching worker at depth: 12
% 0.19/0.42 % SZS status Theorem for theBenchmark
% 0.19/0.42 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------