%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : KRS146+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 : n025.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 7.78s 1.34s
% Output : CNFRefutation 7.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 39
% Syntax : Number of formulae : 260 ( 125 unt; 0 def)
% Number of atoms : 558 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 576 ( 278 ~; 236 |; 41 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 54 ( 2 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(the_axiom,plain,
( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC94(iV822576)
& cowlThing(iV822576)
& cC58(iV822576)
& cC116(iV822576)
& cC56(iV822576)
& cC110(iV822576)
& cC114(iV822576)
& cC136(iV822576)
& cC80(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) )
& cC94(iV822576)
& cowlThing(iV822576)
& cC58(iV822576)
& cC116(iV822576)
& cC56(iV822576)
& cC110(iV822576)
& cC114(iV822576)
& cC136(iV822576)
& cC80(iV822576) ),
inference(negate_conjecture,[status(cth)],[the_axiom]) ).
cnf(225,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK27)
| ~ xsd_integer(sK28)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| cowlNothing(sK27)
| xsd_string(sK28) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l0,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK27)
| ~ xsd_integer(sK28)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| cowlNothing(sK27)
| xsd_string(sK28) ),
inference(instantiation,[status(thm)],[225]) ).
cnf(226,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK27)
| ~ xsd_string(sK28)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| cowlNothing(sK27)
| xsd_integer(sK28) ),
inference(cnf,[status(esa)],[the_axiom_negated]) ).
cnf(l68,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK27)
| ~ xsd_string(sK28)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| cowlNothing(sK27)
| xsd_integer(sK28) ),
inference(instantiation,[status(thm)],[226]) ).
fof(axiom_8,plain,
! [X] :
( cC112(X)
<=> ( ~ cC110(X)
& cC4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_8) ).
cnf(24,plain,
( ~ cC4(X0)
| cC110(X0)
| cC112(X0) ),
inference(cnf,[status(esa)],[axiom_8]) ).
cnf(l76,plain,
( ~ cC4(iV822576)
| cC110(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l30,plain,
( ~ cC4(iV822576)
| cC110(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[24]) ).
fof(axiom_57,plain,
! [X] :
( cC80(X)
<=> ( ~ cC78(X)
& ~ cC76(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_57) ).
cnf(171,plain,
( cC80(X0)
| cC78(X0)
| cC76(X0) ),
inference(cnf,[status(esa)],[axiom_57]) ).
cnf(l119,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l3,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l9,plain,
( ~ cowlThing(iV822576)
| ~ cowlThing(sK27)
| ~ xsd_string(sK28)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| cowlNothing(sK27)
| xsd_integer(sK28) ),
inference(instantiation,[status(thm)],[226]) ).
fof(axiom_43,plain,
! [X] :
( cC56(X)
<=> ( cC4(X)
& ~ cC10(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_43) ).
cnf(129,plain,
( ~ cC4(X0)
| cC10(X0)
| cC56(X0) ),
inference(cnf,[status(esa)],[axiom_43]) ).
cnf(l41,plain,
( ~ cC4(iV822576)
| cC10(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[129]) ).
fof(axiom_75,plain,
cC4(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_75) ).
cnf(209,plain,
cC4(iV822576),
inference(cnf,[status(esa)],[axiom_75]) ).
cnf(l64,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(l93,plain,
( ~ cC4(iV822576)
| cC10(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[129]) ).
fof(axiom_9,plain,
! [X] :
( cC114(X)
<=> ( ~ cC96(X)
& ~ cC112(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
cnf(27,plain,
( cC96(X0)
| cC114(X0)
| cC112(X0) ),
inference(cnf,[status(esa)],[axiom_9]) ).
cnf(l52,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
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(l37,plain,
( ~ xsd_string(sK28)
| ~ xsd_integer(sK28) ),
inference(instantiation,[status(thm)],[2]) ).
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(l116,plain,
cowlThing(iV822576),
inference(instantiation,[status(thm)],[0]) ).
cnf(1,plain,
~ cowlNothing(X0),
inference(cnf,[status(esa)],[axiom_0]) ).
cnf(l7,plain,
~ cowlNothing(sK27),
inference(instantiation,[status(thm)],[1]) ).
fof(axiom_10,plain,
! [X] :
( cC116(X)
<=> ( cC114(X)
& cC80(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
cnf(30,plain,
( ~ cC80(X0)
| ~ cC114(X0)
| cC116(X0) ),
inference(cnf,[status(esa)],[axiom_10]) ).
cnf(l35,plain,
( ~ cC80(iV822576)
| ~ cC114(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[30]) ).
fof(axiom_64,plain,
! [X] :
( cC94(X)
<=> ( ~ cC86(X)
& ~ cC92(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_64) ).
cnf(192,plain,
( cC92(X0)
| cC94(X0)
| cC86(X0) ),
inference(cnf,[status(esa)],[axiom_64]) ).
cnf(l19,plain,
( cC92(iV822576)
| cC94(iV822576)
| cC86(iV822576) ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l73,plain,
cowlThing(sK27),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_21,plain,
! [X] :
( cC136(X)
<=> ( cC116(X)
& ~ cC134(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
cnf(63,plain,
( ~ cC116(X0)
| cC134(X0)
| cC136(X0) ),
inference(cnf,[status(esa)],[axiom_21]) ).
cnf(l14,plain,
( ~ cC116(iV822576)
| cC134(iV822576)
| cC136(iV822576) ),
inference(instantiation,[status(thm)],[63]) ).
fof(axiom_84,plain,
~ cC10(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_84) ).
cnf(218,plain,
~ cC10(iV822576),
inference(cnf,[status(esa)],[axiom_84]) ).
cnf(l217,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
cnf(l48,plain,
( ~ cC116(iV822576)
| cC134(iV822576)
| cC136(iV822576) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l10,plain,
~ cowlNothing(sK27),
inference(instantiation,[status(thm)],[1]) ).
cnf(22,plain,
( ~ cC110(X0)
| ~ cC112(X0) ),
inference(cnf,[status(esa)],[axiom_8]) ).
cnf(l284,plain,
( ~ cC110(iV822576)
| ~ cC112(iV822576) ),
inference(instantiation,[status(thm)],[22]) ).
fof(axiom_44,plain,
! [X] :
( cC58(X)
<=> ( cC34(X)
& cC56(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
cnf(132,plain,
( ~ cC34(X0)
| ~ cC56(X0)
| cC58(X0) ),
inference(cnf,[status(esa)],[axiom_44]) ).
cnf(l17,plain,
( ~ cC34(iV822576)
| ~ cC56(iV822576)
| cC58(iV822576) ),
inference(instantiation,[status(thm)],[132]) ).
cnf(l79,plain,
( ~ cC116(iV822576)
| cC134(iV822576)
| cC136(iV822576) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l18,plain,
( ~ cC80(iV822576)
| ~ cC114(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[30]) ).
fof(axiom_63,plain,
! [X] :
( cC92(X)
<=> ( cC90(X)
& ~ cC16(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_63) ).
cnf(188,plain,
( ~ cC16(X0)
| ~ cC92(X0) ),
inference(cnf,[status(esa)],[axiom_63]) ).
cnf(l90,plain,
( ~ cC16(iV822576)
| ~ cC92(iV822576) ),
inference(instantiation,[status(thm)],[188]) ).
fof(axiom_7,plain,
! [X] :
( cC110(X)
<=> ( ~ cC102(X)
& ~ cC108(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
cnf(21,plain,
( cC108(X0)
| cC102(X0)
| cC110(X0) ),
inference(cnf,[status(esa)],[axiom_7]) ).
cnf(l300,plain,
( cC108(iV822576)
| cC102(iV822576)
| cC110(iV822576) ),
inference(instantiation,[status(thm)],[21]) ).
fof(axiom_72,plain,
cC16(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_72) ).
cnf(206,plain,
cC16(iV822576),
inference(cnf,[status(esa)],[axiom_72]) ).
cnf(l129,plain,
cC16(iV822576),
inference(instantiation,[status(thm)],[206]) ).
cnf(l50,plain,
( cC92(iV822576)
| cC94(iV822576)
| cC86(iV822576) ),
inference(instantiation,[status(thm)],[192]) ).
fof(axiom_77,plain,
~ cC86(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_77) ).
cnf(211,plain,
~ cC86(iV822576),
inference(cnf,[status(esa)],[axiom_77]) ).
cnf(l58,plain,
~ cC86(iV822576),
inference(instantiation,[status(thm)],[211]) ).
cnf(l61,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
fof(axiom_70,plain,
~ cC102(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_70) ).
cnf(204,plain,
~ cC102(iV822576),
inference(cnf,[status(esa)],[axiom_70]) ).
cnf(l722,plain,
~ cC102(iV822576),
inference(instantiation,[status(thm)],[204]) ).
cnf(l72,plain,
( ~ cC80(iV822576)
| ~ cC114(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[30]) ).
fof(axiom_19,plain,
! [X] :
( cC132(X)
<=> ( ~ cC4(X)
& cC2(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
cnf(57,plain,
( ~ cC2(X0)
| cC4(X0)
| cC132(X0) ),
inference(cnf,[status(esa)],[axiom_19]) ).
cnf(l82,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l15,plain,
( ~ cC4(iV822576)
| cC10(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[129]) ).
cnf(l69,plain,
~ cowlNothing(sK27),
inference(instantiation,[status(thm)],[1]) ).
cnf(l36,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l78,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
fof(axiom_88,plain,
~ cC78(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_88) ).
cnf(222,plain,
~ cC78(iV822576),
inference(cnf,[status(esa)],[axiom_88]) ).
cnf(l42,plain,
~ cC78(iV822576),
inference(instantiation,[status(thm)],[222]) ).
cnf(l2,plain,
cowlThing(iV822576),
inference(instantiation,[status(thm)],[0]) ).
fof(axiom_87,plain,
~ cC112(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_87) ).
cnf(221,plain,
~ cC112(iV822576),
inference(cnf,[status(esa)],[axiom_87]) ).
cnf(l83,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
fof(axiom_55,plain,
! [X] :
( cC78(X)
<=> ( ~ cC4(X)
& cC10(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_55) ).
cnf(163,plain,
( ~ cC4(X0)
| ~ cC78(X0) ),
inference(cnf,[status(esa)],[axiom_55]) ).
cnf(l283,plain,
( ~ cC4(iV822576)
| ~ cC78(iV822576) ),
inference(instantiation,[status(thm)],[163]) ).
cnf(l12,plain,
( ~ cC34(iV822576)
| ~ cC56(iV822576)
| cC58(iV822576) ),
inference(instantiation,[status(thm)],[132]) ).
cnf(l11,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l243,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l542,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
fof(axiom_80,plain,
cowlThing(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_80) ).
cnf(214,plain,
cowlThing(iV822576),
inference(cnf,[status(esa)],[axiom_80]) ).
cnf(l63,plain,
cowlThing(iV822576),
inference(instantiation,[status(thm)],[214]) ).
fof(axiom_45,plain,
! [X] :
( cC6(X)
<=> ( cC2(X)
& ~ cC4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_45) ).
cnf(135,plain,
( ~ cC2(X0)
| cC4(X0)
| cC6(X0) ),
inference(cnf,[status(esa)],[axiom_45]) ).
cnf(l21,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC6(iV822576) ),
inference(instantiation,[status(thm)],[135]) ).
cnf(l108,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l115,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l1,plain,
( ~ cC80(iV822576)
| ~ cC114(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l366,plain,
( ~ cC4(iV822576)
| ~ cC78(iV822576) ),
inference(instantiation,[status(thm)],[163]) ).
fof(axiom_76,plain,
~ cC96(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_76) ).
cnf(210,plain,
~ cC96(iV822576),
inference(cnf,[status(esa)],[axiom_76]) ).
cnf(l392,plain,
~ cC96(iV822576),
inference(instantiation,[status(thm)],[210]) ).
fof(axiom_54,plain,
! [X] :
( cC76(X)
<=> ( ~ cC2(X)
& cC4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_54) ).
cnf(161,plain,
( ~ cC76(X0)
| cC4(X0) ),
inference(cnf,[status(esa)],[axiom_54]) ).
cnf(l166,plain,
( ~ cC76(iV822576)
| cC4(iV822576) ),
inference(instantiation,[status(thm)],[161]) ).
cnf(l169,plain,
( ~ cC4(iV822576)
| ~ cC78(iV822576) ),
inference(instantiation,[status(thm)],[163]) ).
fof(axiom_86,plain,
~ cC76(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_86) ).
cnf(220,plain,
~ cC76(iV822576),
inference(cnf,[status(esa)],[axiom_86]) ).
cnf(l274,plain,
~ cC76(iV822576),
inference(instantiation,[status(thm)],[220]) ).
cnf(133,plain,
( ~ cC6(X0)
| cC2(X0) ),
inference(cnf,[status(esa)],[axiom_45]) ).
cnf(l122,plain,
( ~ cC6(iV822576)
| cC2(iV822576) ),
inference(instantiation,[status(thm)],[133]) ).
cnf(l99,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
fof(axiom_89,plain,
cC2(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_89) ).
cnf(223,plain,
cC2(iV822576),
inference(cnf,[status(esa)],[axiom_89]) ).
cnf(l103,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
fof(axiom_20,plain,
! [X] :
( cC134(X)
<=> ( ~ cC130(X)
& cC132(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
cnf(59,plain,
( ~ cC134(X0)
| cC132(X0) ),
inference(cnf,[status(esa)],[axiom_20]) ).
cnf(l153,plain,
( ~ cC134(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[59]) ).
fof(axiom_74,plain,
cC34(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_74) ).
cnf(208,plain,
cC34(iV822576),
inference(cnf,[status(esa)],[axiom_74]) ).
cnf(l118,plain,
cC34(iV822576),
inference(instantiation,[status(thm)],[208]) ).
fof(axiom_65,plain,
! [X] :
( cC96(X)
<=> ( ~ cC94(X)
& cC2(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_65) ).
cnf(193,plain,
( ~ cC96(X0)
| ~ cC94(X0) ),
inference(cnf,[status(esa)],[axiom_65]) ).
cnf(l60,plain,
( ~ cC96(iV822576)
| ~ cC94(iV822576) ),
inference(instantiation,[status(thm)],[193]) ).
cnf(195,plain,
( ~ cC2(X0)
| cC96(X0)
| cC94(X0) ),
inference(cnf,[status(esa)],[axiom_65]) ).
cnf(l114,plain,
( ~ cC2(iV822576)
| cC96(iV822576)
| cC94(iV822576) ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l285,plain,
( cC92(iV822576)
| cC94(iV822576)
| cC86(iV822576) ),
inference(instantiation,[status(thm)],[192]) ).
fof(axiom_78,plain,
~ cC92(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_78) ).
cnf(212,plain,
~ cC92(iV822576),
inference(cnf,[status(esa)],[axiom_78]) ).
cnf(l653,plain,
~ cC92(iV822576),
inference(instantiation,[status(thm)],[212]) ).
cnf(l109,plain,
~ cC96(iV822576),
inference(instantiation,[status(thm)],[210]) ).
cnf(l112,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
fof(axiom_79,plain,
~ cC108(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_79) ).
cnf(213,plain,
~ cC108(iV822576),
inference(cnf,[status(esa)],[axiom_79]) ).
cnf(l708,plain,
~ cC108(iV822576),
inference(instantiation,[status(thm)],[213]) ).
cnf(l570,plain,
~ cC86(iV822576),
inference(instantiation,[status(thm)],[211]) ).
cnf(l367,plain,
~ cC76(iV822576),
inference(instantiation,[status(thm)],[220]) ).
cnf(l240,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l111,plain,
( ~ cC96(iV822576)
| ~ cC94(iV822576) ),
inference(instantiation,[status(thm)],[193]) ).
fof(axiom_71,plain,
~ cC134(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_71) ).
cnf(205,plain,
~ cC134(iV822576),
inference(cnf,[status(esa)],[axiom_71]) ).
cnf(l16,plain,
~ cC134(iV822576),
inference(instantiation,[status(thm)],[205]) ).
cnf(l13,plain,
cowlThing(sK27),
inference(instantiation,[status(thm)],[0]) ).
cnf(l586,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
fof(axiom_69,plain,
~ cC132(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_69) ).
cnf(203,plain,
~ cC132(iV822576),
inference(cnf,[status(esa)],[axiom_69]) ).
cnf(l430,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l6,plain,
cowlThing(sK27),
inference(instantiation,[status(thm)],[0]) ).
cnf(160,plain,
( ~ cC2(X0)
| ~ cC76(X0) ),
inference(cnf,[status(esa)],[axiom_54]) ).
cnf(l39,plain,
( ~ cC2(iV822576)
| ~ cC76(iV822576) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l339,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l216,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l404,plain,
( cC92(iV822576)
| cC94(iV822576)
| cC86(iV822576) ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l696,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[57]) ).
fof(axiom_56,plain,
! [X] :
( cC8(X)
<=> ( cC4(X)
& ~ cC2(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_56) ).
cnf(168,plain,
( ~ cC4(X0)
| cC8(X0)
| cC2(X0) ),
inference(cnf,[status(esa)],[axiom_56]) ).
cnf(l278,plain,
( ~ cC4(iV822576)
| cC8(iV822576)
| cC2(iV822576) ),
inference(instantiation,[status(thm)],[168]) ).
cnf(167,plain,
( ~ cC8(X0)
| ~ cC2(X0) ),
inference(cnf,[status(esa)],[axiom_56]) ).
cnf(l365,plain,
( ~ cC8(iV822576)
| ~ cC2(iV822576) ),
inference(instantiation,[status(thm)],[167]) ).
cnf(l344,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l697,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l54,plain,
( ~ cC4(iV822576)
| cC110(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l409,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l405,plain,
~ cC86(iV822576),
inference(instantiation,[status(thm)],[211]) ).
cnf(l20,plain,
( ~ cC4(iV822576)
| cC10(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[129]) ).
cnf(l368,plain,
( ~ cC2(iV822576)
| ~ cC76(iV822576) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l91,plain,
( ~ cC80(iV822576)
| ~ cC114(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l388,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l66,plain,
( ~ cC134(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l29,plain,
cC34(iV822576),
inference(instantiation,[status(thm)],[208]) ).
cnf(l24,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(187,plain,
( ~ cC92(X0)
| cC90(X0) ),
inference(cnf,[status(esa)],[axiom_63]) ).
cnf(l53,plain,
( ~ cC92(iV822576)
| cC90(iV822576) ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l151,plain,
( ~ cC80(iV822576)
| ~ cC114(iV822576)
| cC116(iV822576) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l407,plain,
~ cC92(iV822576),
inference(instantiation,[status(thm)],[212]) ).
cnf(l26,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
cnf(3,plain,
( xsd_string(X0)
| xsd_integer(X0) ),
inference(cnf,[status(esa)],[axiom_1]) ).
cnf(l81,plain,
( xsd_string(sK28)
| xsd_integer(sK28) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l612,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l414,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l416,plain,
~ cC96(iV822576),
inference(instantiation,[status(thm)],[210]) ).
fof(axiom_82,plain,
~ cC90(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_82) ).
cnf(216,plain,
~ cC90(iV822576),
inference(cnf,[status(esa)],[axiom_82]) ).
cnf(l661,plain,
~ cC90(iV822576),
inference(instantiation,[status(thm)],[216]) ).
cnf(l74,plain,
( ~ cC34(iV822576)
| ~ cC56(iV822576)
| cC58(iV822576) ),
inference(instantiation,[status(thm)],[132]) ).
cnf(l94,plain,
( ~ cC4(iV822576)
| cC10(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[129]) ).
cnf(l251,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
cnf(l505,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l33,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(l98,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l250,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l241,plain,
~ cC78(iV822576),
inference(instantiation,[status(thm)],[222]) ).
cnf(l161,plain,
~ cC76(iV822576),
inference(instantiation,[status(thm)],[220]) ).
cnf(l506,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l84,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l282,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l40,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l415,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l256,plain,
~ cC76(iV822576),
inference(instantiation,[status(thm)],[220]) ).
cnf(l253,plain,
( cC96(iV822576)
| cC114(iV822576)
| cC112(iV822576) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l154,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l254,plain,
~ cC96(iV822576),
inference(instantiation,[status(thm)],[210]) ).
cnf(l22,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
cnf(55,plain,
( ~ cC4(X0)
| ~ cC132(X0) ),
inference(cnf,[status(esa)],[axiom_19]) ).
cnf(l474,plain,
( ~ cC4(iV822576)
| ~ cC132(iV822576) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l67,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l288,plain,
( ~ cC2(iV822576)
| cC4(iV822576)
| cC132(iV822576) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l148,plain,
~ cC96(iV822576),
inference(instantiation,[status(thm)],[210]) ).
cnf(l258,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l293,plain,
~ cC96(iV822576),
inference(instantiation,[status(thm)],[210]) ).
cnf(l105,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l302,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l31,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(l255,plain,
~ cC78(iV822576),
inference(instantiation,[status(thm)],[222]) ).
cnf(l173,plain,
( ~ cC4(iV822576)
| ~ cC78(iV822576) ),
inference(instantiation,[status(thm)],[163]) ).
cnf(l100,plain,
( ~ cC96(iV822576)
| ~ cC94(iV822576) ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l318,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l4,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l157,plain,
( ~ cC4(iV822576)
| cC10(iV822576)
| cC56(iV822576) ),
inference(instantiation,[status(thm)],[129]) ).
cnf(l104,plain,
( cC92(iV822576)
| cC94(iV822576)
| cC86(iV822576) ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l400,plain,
( ~ cC2(iV822576)
| ~ cC76(iV822576) ),
inference(instantiation,[status(thm)],[160]) ).
cnf(l320,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l95,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
cnf(l214,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(l411,plain,
( cC80(iV822576)
| cC78(iV822576)
| cC76(iV822576) ),
inference(instantiation,[status(thm)],[171]) ).
cnf(l554,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l682,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(l641,plain,
cC2(iV822576),
inference(instantiation,[status(thm)],[223]) ).
cnf(l340,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l636,plain,
~ cC78(iV822576),
inference(instantiation,[status(thm)],[222]) ).
cnf(l124,plain,
~ cC86(iV822576),
inference(instantiation,[status(thm)],[211]) ).
cnf(l382,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
cnf(l23,plain,
~ cC76(iV822576),
inference(instantiation,[status(thm)],[220]) ).
cnf(l178,plain,
~ cC112(iV822576),
inference(instantiation,[status(thm)],[221]) ).
cnf(164,plain,
( ~ cC78(X0)
| cC10(X0) ),
inference(cnf,[status(esa)],[axiom_55]) ).
cnf(l8,plain,
( ~ cC78(iV822576)
| cC10(iV822576) ),
inference(instantiation,[status(thm)],[164]) ).
cnf(l28,plain,
( ~ cC96(iV822576)
| ~ cC94(iV822576) ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l180,plain,
( cC92(iV822576)
| cC94(iV822576)
| cC86(iV822576) ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l622,plain,
~ cC76(iV822576),
inference(instantiation,[status(thm)],[220]) ).
cnf(l370,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(l147,plain,
cC34(iV822576),
inference(instantiation,[status(thm)],[208]) ).
cnf(l213,plain,
cC4(iV822576),
inference(instantiation,[status(thm)],[209]) ).
cnf(l110,plain,
~ cC92(iV822576),
inference(instantiation,[status(thm)],[212]) ).
cnf(l242,plain,
~ cC10(iV822576),
inference(instantiation,[status(thm)],[218]) ).
fof(axiom_60,plain,
! [X] :
( cC86(X)
<=> ( cC16(X)
& cC84(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_60) ).
cnf(179,plain,
( ~ cC86(X0)
| cC84(X0) ),
inference(cnf,[status(esa)],[axiom_60]) ).
cnf(l336,plain,
( ~ cC86(iV822576)
| cC84(iV822576) ),
inference(instantiation,[status(thm)],[179]) ).
cnf(l768,plain,
~ cC132(iV822576),
inference(instantiation,[status(thm)],[203]) ).
cnf(l305,plain,
( ~ cC92(iV822576)
| cC90(iV822576) ),
inference(instantiation,[status(thm)],[187]) ).
fof(axiom_68,plain,
~ cC84(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_68) ).
cnf(202,plain,
~ cC84(iV822576),
inference(cnf,[status(esa)],[axiom_68]) ).
cnf(l338,plain,
~ cC84(iV822576),
inference(instantiation,[status(thm)],[202]) ).
cnf(l1112,plain,
~ cC90(iV822576),
inference(instantiation,[status(thm)],[216]) ).
cnf(l106,plain,
~ cC86(iV822576),
inference(instantiation,[status(thm)],[211]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l68,l76,l30,l119,l3,l9,l41,l64,l93,l52,l37,l116,l7,l35,l19,l73,l14,l217,l48,l10,l284,l17,l79,l18,l90,l300,l129,l50,l58,l61,l722,l72,l82,l15,l69,l36,l78,l42,l2,l83,l283,l12,l11,l243,l542,l63,l21,l108,l115,l1,l366,l392,l166,l169,l274,l122,l99,l103,l153,l118,l60,l114,l285,l653,l109,l112,l708,l570,l367,l240,l111,l16,l13,l586,l430,l6,l39,l339,l216,l404,l696,l278,l365,l344,l697,l54,l409,l405,l20,l368,l91,l388,l66,l29,l24,l53,l151,l407,l26,l81,l612,l414,l416,l661,l74,l94,l251,l505,l33,l98,l250,l241,l161,l506,l84,l282,l40,l415,l256,l253,l154,l254,l22,l474,l67,l288,l148,l258,l293,l105,l302,l31,l255,l173,l100,l318,l4,l157,l104,l400,l320,l95,l214,l411,l554,l682,l641,l340,l636,l124,l382,l23,l178,l8,l28,l180,l622,l370,l147,l213,l110,l242,l336,l768,l305,l338,l1112,l106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS146+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n025.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 : Sun Jul 20 22:15:49 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.34 % launching worker at depth: 9
% 0.13/0.34 % launching worker at depth: 10
% 0.13/0.35 % launching worker at depth: 11
% 0.13/0.39 % launching worker at depth: 12
% 7.78/1.34 % SZS status Theorem for theBenchmark
% 7.78/1.34 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------