%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : KRS149+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:45 PM UTC 2025
% Result : Theorem 0.20s 0.42s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 25
% Syntax : Number of formulae : 151 ( 68 unt; 0 def)
% Number of atoms : 337 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 350 ( 164 ~; 140 |; 31 &)
% ( 13 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 42 ( 2 sgn 18 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(the_axiom,plain,
( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC216(iV3102)
& cC46(iV3102)
& cC30(iV3102)
& cC44(iV3102)
& cC28(iV3102)
& cC64(iV3102)
& cC14(iV3102)
& cowlThing(iV3102) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(the_axiom_negated,plain,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC216(iV3102)
& cC46(iV3102)
& cC30(iV3102)
& cC44(iV3102)
& cC28(iV3102)
& cC64(iV3102)
& cC14(iV3102)
& cowlThing(iV3102) ),
inference(negate_conjecture,[status(cth)],[the_axiom]) ).
cnf(339,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK109)
| ~ xsd_integer(sK110)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC46(iV3102)
| cowlNothing(sK109)
| xsd_string(sK110) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l0,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK109)
| ~ xsd_integer(sK110)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC46(iV3102)
| cowlNothing(sK109)
| xsd_string(sK110) ),
inference(instantiation,[status(thm)],[339]) ).
fof(axiom_65,plain,
! [X] :
( cC216(X)
<=> ( ~ cC214(X)
& cC64(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
cnf(195,plain,
( ~ cC64(X0)
| cC216(X0)
| cC214(X0) ),
inference(cnf,[status(esa)],[axiom_65]) ).
cnf(l1,plain,
( ~ cC64(iV3102)
| cC216(iV3102)
| cC214(iV3102) ),
inference(instantiation,[status(thm)],[195]) ).
fof(axiom_107,plain,
! [X] :
( cTEST(X)
<=> ( cC216(X)
& cC46(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_107) ).
cnf(320,plain,
( ~ cTEST(X0)
| cC46(X0) ),
inference(cnf,[status(esa)],[axiom_107]) ).
cnf(l41,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
fof(axiom_0,plain,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
cnf(0,plain,
cowlThing(X0),
inference(cnf,[status(esa)],[axiom_0]) ).
cnf(l6,plain,
cowlThing(sK109),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_77,plain,
! [X] :
( cC44(X)
<=> ( ~ cC32(X)
& ~ cC42(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_77) ).
cnf(231,plain,
( cC32(X0)
| cC42(X0)
| cC44(X0) ),
inference(cnf,[status(esa)],[axiom_77]) ).
cnf(l32,plain,
( cC32(iV3102)
| cC42(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[231]) ).
cnf(1,plain,
~ cowlNothing(X0),
inference(cnf,[status(esa)],[axiom_0]) ).
cnf(l13,plain,
~ cowlNothing(sK109),
inference(instantiation,[status(thm)],[1]) ).
fof(axiom_76,plain,
! [X] :
( cC42(X)
<=> ? [Y] :
( rR1(X,Y)
& cC40(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_76) ).
cnf(227,plain,
( ~ cC42(X0)
| cC40(sK77(X0)) ),
inference(cnf,[status(esa)],[axiom_76]) ).
cnf(l35,plain,
( ~ cC42(iV3102)
| cC40(sK77(iV3102)) ),
inference(instantiation,[status(thm)],[227]) ).
fof(axiom_88,plain,
! [X] :
( cC64(X)
<=> ( ~ cC62(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_88) ).
cnf(264,plain,
( ~ cTOP(X0)
| cC64(X0)
| cC62(X0) ),
inference(cnf,[status(esa)],[axiom_88]) ).
cnf(l4,plain,
( ~ cTOP(iV3102)
| cC64(iV3102)
| cC62(iV3102) ),
inference(instantiation,[status(thm)],[264]) ).
fof(axiom_119,plain,
~ cC62(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_119) ).
cnf(333,plain,
~ cC62(iV3102),
inference(cnf,[status(esa)],[axiom_119]) ).
cnf(l194,plain,
~ cC62(iV3102),
inference(instantiation,[status(thm)],[333]) ).
fof(axiom_70,plain,
! [X] :
( cC30(X)
<=> ( cC14(X)
& cC28(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_70) ).
cnf(209,plain,
( ~ cC30(X0)
| cC28(X0) ),
inference(cnf,[status(esa)],[axiom_70]) ).
cnf(l33,plain,
( ~ cC30(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[209]) ).
cnf(l2,plain,
cowlThing(iV3102),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_108,plain,
cTEST(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_108) ).
cnf(322,plain,
cTEST(iV3102),
inference(cnf,[status(esa)],[axiom_108]) ).
cnf(l62,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(194,plain,
( ~ cC216(X0)
| cC64(X0) ),
inference(cnf,[status(esa)],[axiom_65]) ).
cnf(l36,plain,
( ~ cC216(iV3102)
| cC64(iV3102) ),
inference(instantiation,[status(thm)],[194]) ).
fof(axiom_24,plain,
! [X] :
( cC14(X)
<=> ( ~ cC12(X)
& ~ cC2(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_24) ).
cnf(72,plain,
( cC2(X0)
| cC12(X0)
| cC14(X0) ),
inference(cnf,[status(esa)],[axiom_24]) ).
cnf(l3,plain,
( cC2(iV3102)
| cC12(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[72]) ).
fof(axiom_122,plain,
~ cC2(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_122) ).
cnf(336,plain,
~ cC2(iV3102),
inference(cnf,[status(esa)],[axiom_122]) ).
cnf(l15,plain,
~ cC2(iV3102),
inference(instantiation,[status(thm)],[336]) ).
cnf(340,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK109)
| ~ xsd_string(sK110)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC46(iV3102)
| cowlNothing(sK109)
| xsd_integer(sK110) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l7,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK109)
| ~ xsd_string(sK110)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC46(iV3102)
| cowlNothing(sK109)
| xsd_integer(sK110) ),
inference(instantiation,[status(thm)],[340]) ).
fof(axiom_78,plain,
! [X] :
( cC46(X)
<=> ( cC30(X)
& cC44(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_78) ).
cnf(233,plain,
( ~ cC46(X0)
| cC44(X0) ),
inference(cnf,[status(esa)],[axiom_78]) ).
cnf(l29,plain,
( ~ cC46(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[233]) ).
cnf(319,plain,
( ~ cTEST(X0)
| cC216(X0) ),
inference(cnf,[status(esa)],[axiom_107]) ).
cnf(l75,plain,
( ~ cTEST(iV3102)
| cC216(iV3102) ),
inference(instantiation,[status(thm)],[319]) ).
cnf(l12,plain,
cowlThing(sK109),
inference(instantiation,[status(thm)],[0]) ).
cnf(210,plain,
( ~ cC14(X0)
| ~ cC28(X0)
| cC30(X0) ),
inference(cnf,[status(esa)],[axiom_70]) ).
cnf(l19,plain,
( ~ cC14(iV3102)
| ~ cC28(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l22,plain,
( cC2(iV3102)
| cC12(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[72]) ).
fof(axiom_109,plain,
cowlThing(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_109) ).
cnf(323,plain,
cowlThing(iV3102),
inference(cnf,[status(esa)],[axiom_109]) ).
cnf(l8,plain,
cowlThing(iV3102),
inference(instantiation,[status(thm)],[323]) ).
cnf(l70,plain,
~ cowlNothing(sK109),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9,plain,
( cC2(iV3102)
| cC12(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(232,plain,
( ~ cC46(X0)
| cC30(X0) ),
inference(cnf,[status(esa)],[axiom_78]) ).
cnf(l50,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[232]) ).
cnf(l72,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
cnf(l34,plain,
( ~ cC64(iV3102)
| cC216(iV3102)
| cC214(iV3102) ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l17,plain,
( ~ cC216(iV3102)
| cC64(iV3102) ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l76,plain,
~ cC2(iV3102),
inference(instantiation,[status(thm)],[336]) ).
cnf(l23,plain,
( ~ cTEST(iV3102)
| cC216(iV3102) ),
inference(instantiation,[status(thm)],[319]) ).
cnf(l30,plain,
( ~ cC46(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[232]) ).
fof(axiom_115,plain,
~ cC12(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_115) ).
cnf(329,plain,
~ cC12(iV3102),
inference(cnf,[status(esa)],[axiom_115]) ).
cnf(l78,plain,
~ cC12(iV3102),
inference(instantiation,[status(thm)],[329]) ).
cnf(l21,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
fof(axiom_1,plain,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
cnf(3,plain,
( xsd_string(X0)
| xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l39,plain,
( xsd_string(sK110)
| xsd_integer(sK110) ),
inference(instantiation,[status(thm)],[3]) ).
fof(axiom_118,plain,
~ cC214(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_118) ).
cnf(332,plain,
~ cC214(iV3102),
inference(cnf,[status(esa)],[axiom_118]) ).
cnf(l192,plain,
~ cC214(iV3102),
inference(instantiation,[status(thm)],[332]) ).
fof(axiom_120,plain,
! [X] :
( rR1(iV3102,X)
=> ~ cC40(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
cnf(334,plain,
( ~ rR1(iV3102,X0)
| ~ cC40(X0) ),
inference(cnf,[status(esa)],[axiom_120]) ).
cnf(l37,plain,
( ~ rR1(iV3102,sK77(iV3102))
| ~ cC40(sK77(iV3102)) ),
inference(instantiation,[status(thm)],[334]) ).
fof(axiom_69,plain,
! [X] :
( cC28(X)
<=> ( ~ cC26(X)
& ~ cC16(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_69) ).
cnf(207,plain,
( cC16(X0)
| cC26(X0)
| cC28(X0) ),
inference(cnf,[status(esa)],[axiom_69]) ).
cnf(l11,plain,
( cC16(iV3102)
| cC26(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l27,plain,
( cC16(iV3102)
| cC26(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l223,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(l67,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
cnf(l73,plain,
( ~ cTOP(iV3102)
| cC64(iV3102)
| cC62(iV3102) ),
inference(instantiation,[status(thm)],[264]) ).
cnf(l79,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
cnf(l10,plain,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK109)
| ~ xsd_string(sK110)
| ~ cC14(iV3102)
| ~ cC216(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC46(iV3102)
| cowlNothing(sK109)
| xsd_integer(sK110) ),
inference(instantiation,[status(thm)],[340]) ).
cnf(l91,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
fof(axiom_112,plain,
cTOP(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_112) ).
cnf(326,plain,
cTOP(iV3102),
inference(cnf,[status(esa)],[axiom_112]) ).
cnf(l119,plain,
cTOP(iV3102),
inference(instantiation,[status(thm)],[326]) ).
cnf(226,plain,
( ~ cC42(X0)
| rR1(X0,sK77(X0)) ),
inference(cnf,[status(esa)],[axiom_76]) ).
cnf(l202,plain,
( ~ cC42(iV3102)
| rR1(iV3102,sK77(iV3102)) ),
inference(instantiation,[status(thm)],[226]) ).
cnf(l222,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(l121,plain,
cowlThing(iV3102),
inference(instantiation,[status(thm)],[323]) ).
fof(axiom_13,plain,
! [X] :
( cC12(X)
<=> ? [Y] :
( rR1(X,Y)
& cC10(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_13) ).
cnf(38,plain,
( ~ cC12(X0)
| cC10(sK13(X0)) ),
inference(cnf,[status(esa)],[axiom_13]) ).
cnf(l5,plain,
( ~ cC12(iV3102)
| cC10(sK13(iV3102)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l128,plain,
( ~ cC14(iV3102)
| ~ cC28(iV3102)
| cC30(iV3102) ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l126,plain,
( cC2(iV3102)
| cC12(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(l16,plain,
cowlThing(sK109),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_116,plain,
~ cC26(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_116) ).
cnf(330,plain,
~ cC26(iV3102),
inference(cnf,[status(esa)],[axiom_116]) ).
cnf(l81,plain,
~ cC26(iV3102),
inference(instantiation,[status(thm)],[330]) ).
cnf(l115,plain,
( ~ cTOP(iV3102)
| cC64(iV3102)
| cC62(iV3102) ),
inference(instantiation,[status(thm)],[264]) ).
cnf(l124,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
cnf(2,plain,
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l147,plain,
( ~ xsd_string(sK110)
| ~ xsd_integer(sK110) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l196,plain,
cTOP(iV3102),
inference(instantiation,[status(thm)],[326]) ).
cnf(l31,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
fof(axiom_123,plain,
~ cC32(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
cnf(337,plain,
~ cC32(iV3102),
inference(cnf,[status(esa)],[axiom_123]) ).
cnf(l38,plain,
~ cC32(iV3102),
inference(instantiation,[status(thm)],[337]) ).
cnf(l137,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(l113,plain,
~ cC26(iV3102),
inference(instantiation,[status(thm)],[330]) ).
cnf(l120,plain,
( ~ cTEST(iV3102)
| cC216(iV3102) ),
inference(instantiation,[status(thm)],[319]) ).
cnf(l131,plain,
~ cC12(iV3102),
inference(instantiation,[status(thm)],[329]) ).
cnf(l116,plain,
~ cC62(iV3102),
inference(instantiation,[status(thm)],[333]) ).
cnf(l114,plain,
~ cC12(iV3102),
inference(instantiation,[status(thm)],[329]) ).
cnf(l122,plain,
cTOP(iV3102),
inference(instantiation,[status(thm)],[326]) ).
cnf(l14,plain,
~ cC2(iV3102),
inference(instantiation,[status(thm)],[336]) ).
cnf(l174,plain,
( cC16(iV3102)
| cC26(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l108,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(l118,plain,
( ~ cC46(iV3102)
| cC44(iV3102) ),
inference(instantiation,[status(thm)],[233]) ).
cnf(l123,plain,
~ cC62(iV3102),
inference(instantiation,[status(thm)],[333]) ).
cnf(l146,plain,
( cC16(iV3102)
| cC26(iV3102)
| cC28(iV3102) ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l127,plain,
~ cC2(iV3102),
inference(instantiation,[status(thm)],[336]) ).
cnf(l173,plain,
~ cC26(iV3102),
inference(instantiation,[status(thm)],[330]) ).
cnf(l142,plain,
~ cowlNothing(sK109),
inference(instantiation,[status(thm)],[1]) ).
cnf(l129,plain,
( cC2(iV3102)
| cC12(iV3102)
| cC14(iV3102) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(l144,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(l152,plain,
~ cC12(iV3102),
inference(instantiation,[status(thm)],[329]) ).
cnf(l133,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
fof(axiom_111,plain,
! [X] :
( rR1(iV3102,X)
=> ~ cC10(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_111) ).
cnf(325,plain,
( ~ cC10(X0)
| ~ rR1(iV3102,X0) ),
inference(cnf,[status(esa)],[axiom_111]) ).
cnf(l193,plain,
( ~ cC10(sK13(iV3102))
| ~ rR1(iV3102,sK13(iV3102)) ),
inference(instantiation,[status(thm)],[325]) ).
fof(axiom_121,plain,
~ cC16(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_121) ).
cnf(335,plain,
~ cC16(iV3102),
inference(cnf,[status(esa)],[axiom_121]) ).
cnf(l179,plain,
~ cC16(iV3102),
inference(instantiation,[status(thm)],[335]) ).
cnf(l136,plain,
~ cC2(iV3102),
inference(instantiation,[status(thm)],[336]) ).
cnf(37,plain,
( ~ cC12(X0)
| rR1(X0,sK13(X0)) ),
inference(cnf,[status(esa)],[axiom_13]) ).
cnf(l198,plain,
( ~ cC12(iV3102)
| rR1(iV3102,sK13(iV3102)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l112,plain,
~ cC214(iV3102),
inference(instantiation,[status(thm)],[332]) ).
cnf(l178,plain,
~ cC26(iV3102),
inference(instantiation,[status(thm)],[330]) ).
cnf(l166,plain,
( ~ cTEST(iV3102)
| cC46(iV3102) ),
inference(instantiation,[status(thm)],[320]) ).
cnf(l168,plain,
cTEST(iV3102),
inference(instantiation,[status(thm)],[322]) ).
cnf(l151,plain,
~ cC16(iV3102),
inference(instantiation,[status(thm)],[335]) ).
cnf(l28,plain,
~ cC16(iV3102),
inference(instantiation,[status(thm)],[335]) ).
cnf(l47,plain,
~ cC16(iV3102),
inference(instantiation,[status(thm)],[335]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l41,l6,l32,l13,l35,l4,l194,l33,l2,l62,l36,l3,l15,l7,l29,l75,l12,l19,l22,l8,l70,l9,l50,l72,l34,l17,l76,l23,l30,l78,l21,l39,l192,l37,l11,l27,l223,l67,l73,l79,l10,l91,l119,l202,l222,l121,l5,l128,l126,l16,l81,l115,l124,l147,l196,l31,l38,l137,l113,l120,l131,l116,l114,l122,l14,l174,l108,l118,l123,l146,l127,l173,l142,l129,l144,l152,l133,l193,l179,l136,l198,l112,l178,l166,l168,l151,l28,l47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS149+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jul 20 22:16:04 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.35 % launching worker at depth: 1
% 0.12/0.35 % launching worker at depth: 3
% 0.12/0.35 % launching worker at depth: 2
% 0.12/0.35 % launching worker at depth: 4
% 0.12/0.35 % launching worker at depth: 5
% 0.12/0.35 % launching worker at depth: 6
% 0.12/0.35 % launching worker at depth: 7
% 0.12/0.35 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 0.12/0.36 % launching worker at depth: 11
% 0.20/0.42 % SZS status Theorem for theBenchmark
% 0.20/0.42 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------