%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:59:49 PM UTC 2026
% Result : Theorem 0.14s 0.41s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 77
% Syntax : Number of formulae : 355 ( 56 unt; 37 def)
% Number of atoms : 1116 ( 0 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 1274 ( 513 ~; 528 |; 170 &)
% ( 62 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 71 ( 70 usr; 38 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 13 con; 0-1 aty)
% Number of variables : 299 ( 244 !; 55 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] :
( cC10(X)
<=> ( cC8(X)
& cC4(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( cTOP(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X] :
( cC20(X)
<=> ? [Y0] : ra_Px5(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] :
( cC20xcomp(X)
<=> ~ ? [Y] : ra_Px5(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X] :
( cC22(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] :
( cC26(X)
<=> ( cC20xcomp(X)
& cC24(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( cC32xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] :
( cC6(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [X] :
( cC60(X)
<=> ( cC58(X)
& cC2xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X] :
( cC62(X)
<=> ? [Y] :
( cC60(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( cC64(X)
<=> ? [Y] :
( cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( cC66(X)
<=> ( cC64(X)
& cC2xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X] :
( cC68(X)
<=> ? [Y] :
( cC66(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [X] :
( cC78(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( cC6xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [X] :
( cC80(X)
<=> ( cC2xcomp(X)
& cC78xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( cC80(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
rR1(iV8467,iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,axiom,
rR1(iV8467,iV8470),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,axiom,
rR1(iV8467,iV8469),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f107,axiom,
rR1(iV8467,iV8474),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,axiom,
rR1(iV8467,iV8472),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,axiom,
cC2xcomp(iV8468),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
cC6xcomp(iV8469),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,axiom,
cTOP(iV8470),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
cC78xcomp(iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,axiom,
cC2xcomp(iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
cC2xcomp(iV8472),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,axiom,
rR1(iV8472,iV8476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,axiom,
cC2xcomp(iV8473),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
cC32xcomp(iV8474),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,axiom,
cC2xcomp(iV8475),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
cC2(iV8476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,conjecture,
( cowlThing(iV8472)
& cC60(iV8472)
& cC58(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC48(iV8467)
& cowlThing(iV8467)
& cC10(iV8467)
& cC34(iV8467)
& cC14(iV8467)
& cC62(iV8467)
& cC82(iV8467)
& cC8(iV8467)
& cC4(iV8467)
& cC20(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,negated_conjecture,
~ ( cowlThing(iV8472)
& cC60(iV8472)
& cC58(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC48(iV8467)
& cowlThing(iV8467)
& cC10(iV8467)
& cC34(iV8467)
& cC14(iV8467)
& cC62(iV8467)
& cC82(iV8467)
& cC8(iV8467)
& cC4(iV8467)
& cC20(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f135]) ).
fof(f137,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f138,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f141,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f140]) ).
fof(f142,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f144,plain,
! [X] :
( ( ~ cC8(X)
| ~ cC4(X)
| cC10(X) )
& ( ( cC8(X)
& cC4(X) )
| ~ cC10(X) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f145,plain,
( ! [X] :
( ~ cC8(X)
| ~ cC4(X)
| cC10(X) )
& ! [X] :
( ( cC8(X)
& cC4(X) )
| ~ cC10(X) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f148,plain,
! [X0] :
( ~ cC8(X0)
| ~ cC4(X0)
| cC10(X0) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f161,plain,
! [X] :
( ( ! [Y] :
( ~ cTOP(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ( ? [Y] :
( cTOP(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f162,plain,
( ! [X] :
( ! [Y] :
( ~ cTOP(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ! [X] :
( ? [Y] :
( cTOP(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f163,plain,
( ! [X] :
( ! [Y] :
( ~ cTOP(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ! [X] :
( ( cTOP(sK2_skl(X))
& rR1(X,sK2_skl(X)) )
| ~ cC14(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(X))],[f162]) ).
fof(f166,plain,
! [X0,X1] :
( ~ cTOP(X1)
| ~ rR1(X0,X1)
| cC14(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f205,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC20(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC20(X) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f206,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC20(X) )
& ! [X] :
( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC20(X) ) ),
inference(miniscoping,[status(thm)],[f205]) ).
fof(f207,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC20(X) )
& ! [X] :
( ( cC2xcomp(sK9_skl(X))
& rR1(X,sK9_skl(X)) )
| ~ cC20(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Y,sK9_skl(X))],[f206]) ).
fof(f208,plain,
! [X0] :
( rR1(X0,sK9_skl(X0))
| ~ cC20(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f209,plain,
! [X0] :
( cC2xcomp(sK9_skl(X0))
| ~ cC20(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f210,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC20(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f211,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px5(X,Y0)
| cC20(X) )
& ( ? [Y0] : ra_Px5(X,Y0)
| ~ cC20(X) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f212,plain,
( ! [X] :
( ! [Y0] : ~ ra_Px5(X,Y0)
| cC20(X) )
& ! [X] :
( ? [Y0] : ra_Px5(X,Y0)
| ~ cC20(X) ) ),
inference(miniscoping,[status(thm)],[f211]) ).
fof(f213,plain,
( ! [X] :
( ! [Y0] : ~ ra_Px5(X,Y0)
| cC20(X) )
& ! [X] :
( ra_Px5(X,sK10_skl(X))
| ~ cC20(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Y0,sK10_skl(X))],[f212]) ).
fof(f214,plain,
! [X0] :
( ra_Px5(X0,sK10_skl(X0))
| ~ cC20(X0) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f216,plain,
! [X] :
( cC20xcomp(X)
<=> ! [Y] : ~ ra_Px5(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f217,plain,
! [X] :
( ( ? [Y] : ra_Px5(X,Y)
| cC20xcomp(X) )
& ( ! [Y] : ~ ra_Px5(X,Y)
| ~ cC20xcomp(X) ) ),
inference(NNF_transformation,[status(thm)],[f216]) ).
fof(f218,plain,
( ! [X] :
( ? [Y] : ra_Px5(X,Y)
| cC20xcomp(X) )
& ! [X] :
( ! [Y] : ~ ra_Px5(X,Y)
| ~ cC20xcomp(X) ) ),
inference(miniscoping,[status(thm)],[f217]) ).
fof(f219,plain,
( ! [X] :
( ra_Px5(X,sK11_skl(X))
| cC20xcomp(X) )
& ! [X] :
( ! [Y] : ~ ra_Px5(X,Y)
| ~ cC20xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Y,sK11_skl(X))],[f218]) ).
fof(f220,plain,
! [X0,X1] :
( ~ ra_Px5(X0,X1)
| ~ cC20xcomp(X0) ),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f222,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC22(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC22(X) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f223,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC22(X) )
& ! [X] :
( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC22(X) ) ),
inference(miniscoping,[status(thm)],[f222]) ).
fof(f224,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC22(X) )
& ! [X] :
( ( cC2xcomp(sK12_skl(X))
& rR1(X,sK12_skl(X)) )
| ~ cC22(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(Y,sK12_skl(X))],[f223]) ).
fof(f226,plain,
! [X0] :
( cC2xcomp(sK12_skl(X0))
| ~ cC22(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f227,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC22(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f234,plain,
! [X] :
( ( ~ cC20xcomp(X)
| ~ cC24(X)
| cC26(X) )
& ( ( cC20xcomp(X)
& cC24(X) )
| ~ cC26(X) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f235,plain,
( ! [X] :
( ~ cC20xcomp(X)
| ~ cC24(X)
| cC26(X) )
& ! [X] :
( ( cC20xcomp(X)
& cC24(X) )
| ~ cC26(X) ) ),
inference(miniscoping,[status(thm)],[f234]) ).
fof(f237,plain,
! [X0] :
( cC20xcomp(X0)
| ~ cC26(X0) ),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f294,plain,
! [X] :
( ( ! [Y] :
( ~ cC32xcomp(Y)
| ~ rR1(X,Y) )
| cC34(X) )
& ( ? [Y] :
( cC32xcomp(Y)
& rR1(X,Y) )
| ~ cC34(X) ) ),
inference(NNF_transformation,[status(thm)],[f30]) ).
fof(f295,plain,
( ! [X] :
( ! [Y] :
( ~ cC32xcomp(Y)
| ~ rR1(X,Y) )
| cC34(X) )
& ! [X] :
( ? [Y] :
( cC32xcomp(Y)
& rR1(X,Y) )
| ~ cC34(X) ) ),
inference(miniscoping,[status(thm)],[f294]) ).
fof(f296,plain,
( ! [X] :
( ! [Y] :
( ~ cC32xcomp(Y)
| ~ rR1(X,Y) )
| cC34(X) )
& ! [X] :
( ( cC32xcomp(sK23_skl(X))
& rR1(X,sK23_skl(X)) )
| ~ cC34(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(Y,sK23_skl(X))],[f295]) ).
fof(f299,plain,
! [X0,X1] :
( ~ cC32xcomp(X1)
| ~ rR1(X0,X1)
| cC34(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f329,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC4(X) ) ),
inference(NNF_transformation,[status(thm)],[f36]) ).
fof(f330,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ! [X] :
( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC4(X) ) ),
inference(miniscoping,[status(thm)],[f329]) ).
fof(f331,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ! [X] :
( ( cC2xcomp(sK29_skl(X))
& rR1(X,sK29_skl(X)) )
| ~ cC4(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(Y,sK29_skl(X))],[f330]) ).
fof(f332,plain,
! [X0] :
( rR1(X0,sK29_skl(X0))
| ~ cC4(X0) ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f333,plain,
! [X0] :
( cC2xcomp(sK29_skl(X0))
| ~ cC4(X0) ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f334,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC4(X0) ),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f379,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC48(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC48(X) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f380,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC48(X) )
& ! [X] :
( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC48(X) ) ),
inference(miniscoping,[status(thm)],[f379]) ).
fof(f381,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC48(X) )
& ! [X] :
( ( cC2xcomp(sK36_skl(X))
& rR1(X,sK36_skl(X)) )
| ~ cC48(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(Y,sK36_skl(X))],[f380]) ).
fof(f382,plain,
! [X0] :
( rR1(X0,sK36_skl(X0))
| ~ cC48(X0) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f383,plain,
! [X0] :
( cC2xcomp(sK36_skl(X0))
| ~ cC48(X0) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f384,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC48(X0) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f451,plain,
! [X] :
( ( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC58(X) )
& ( ? [Y] :
( cC2(Y)
& rR1(X,Y) )
| ~ cC58(X) ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f452,plain,
( ! [X] :
( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC58(X) )
& ! [X] :
( ? [Y] :
( cC2(Y)
& rR1(X,Y) )
| ~ cC58(X) ) ),
inference(miniscoping,[status(thm)],[f451]) ).
fof(f453,plain,
( ! [X] :
( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC58(X) )
& ! [X] :
( ( cC2(sK47_skl(X))
& rR1(X,sK47_skl(X)) )
| ~ cC58(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl]),skolemize(Y,sK47_skl(X))],[f452]) ).
fof(f456,plain,
! [X0,X1] :
( ~ cC2(X1)
| ~ rR1(X0,X1)
| cC58(X0) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f463,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC6(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC6(X) ) ),
inference(NNF_transformation,[status(thm)],[f60]) ).
fof(f464,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC6(X) )
& ! [X] :
( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC6(X) ) ),
inference(miniscoping,[status(thm)],[f463]) ).
fof(f465,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC6(X) )
& ! [X] :
( ( cC2xcomp(sK49_skl(X))
& rR1(X,sK49_skl(X)) )
| ~ cC6(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl]),skolemize(Y,sK49_skl(X))],[f464]) ).
fof(f466,plain,
! [X0] :
( rR1(X0,sK49_skl(X0))
| ~ cC6(X0) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f467,plain,
! [X0] :
( cC2xcomp(sK49_skl(X0))
| ~ cC6(X0) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f468,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC6(X0) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f474,plain,
! [X] :
( ( ~ cC58(X)
| ~ cC2xcomp(X)
| cC60(X) )
& ( ( cC58(X)
& cC2xcomp(X) )
| ~ cC60(X) ) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f475,plain,
( ! [X] :
( ~ cC58(X)
| ~ cC2xcomp(X)
| cC60(X) )
& ! [X] :
( ( cC58(X)
& cC2xcomp(X) )
| ~ cC60(X) ) ),
inference(miniscoping,[status(thm)],[f474]) ).
fof(f476,plain,
! [X0] :
( cC2xcomp(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f477,plain,
! [X0] :
( cC58(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f478,plain,
! [X0] :
( ~ cC58(X0)
| ~ cC2xcomp(X0)
| cC60(X0) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f479,plain,
! [X] :
( ( ! [Y] :
( ~ cC60(Y)
| ~ rR1(X,Y) )
| cC62(X) )
& ( ? [Y] :
( cC60(Y)
& rR1(X,Y) )
| ~ cC62(X) ) ),
inference(NNF_transformation,[status(thm)],[f63]) ).
fof(f480,plain,
( ! [X] :
( ! [Y] :
( ~ cC60(Y)
| ~ rR1(X,Y) )
| cC62(X) )
& ! [X] :
( ? [Y] :
( cC60(Y)
& rR1(X,Y) )
| ~ cC62(X) ) ),
inference(miniscoping,[status(thm)],[f479]) ).
fof(f481,plain,
( ! [X] :
( ! [Y] :
( ~ cC60(Y)
| ~ rR1(X,Y) )
| cC62(X) )
& ! [X] :
( ( cC60(sK51_skl(X))
& rR1(X,sK51_skl(X)) )
| ~ cC62(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl]),skolemize(Y,sK51_skl(X))],[f480]) ).
fof(f483,plain,
! [X0] :
( cC60(sK51_skl(X0))
| ~ cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f484,plain,
! [X0,X1] :
( ~ cC60(X1)
| ~ rR1(X0,X1)
| cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f496,plain,
! [X] :
( ( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC64(X) )
& ( ? [Y] :
( cC2(Y)
& rR1(X,Y) )
| ~ cC64(X) ) ),
inference(NNF_transformation,[status(thm)],[f66]) ).
fof(f497,plain,
( ! [X] :
( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC64(X) )
& ! [X] :
( ? [Y] :
( cC2(Y)
& rR1(X,Y) )
| ~ cC64(X) ) ),
inference(miniscoping,[status(thm)],[f496]) ).
fof(f498,plain,
( ! [X] :
( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC64(X) )
& ! [X] :
( ( cC2(sK54_skl(X))
& rR1(X,sK54_skl(X)) )
| ~ cC64(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl]),skolemize(Y,sK54_skl(X))],[f497]) ).
fof(f501,plain,
! [X0,X1] :
( ~ cC2(X1)
| ~ rR1(X0,X1)
| cC64(X0) ),
inference(cnf_transformation,[status(thm)],[f498]) ).
fof(f502,plain,
! [X] :
( ( ~ cC64(X)
| ~ cC2xcomp(X)
| cC66(X) )
& ( ( cC64(X)
& cC2xcomp(X) )
| ~ cC66(X) ) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f503,plain,
( ! [X] :
( ~ cC64(X)
| ~ cC2xcomp(X)
| cC66(X) )
& ! [X] :
( ( cC64(X)
& cC2xcomp(X) )
| ~ cC66(X) ) ),
inference(miniscoping,[status(thm)],[f502]) ).
fof(f504,plain,
! [X0] :
( cC2xcomp(X0)
| ~ cC66(X0) ),
inference(cnf_transformation,[status(thm)],[f503]) ).
fof(f505,plain,
! [X0] :
( cC64(X0)
| ~ cC66(X0) ),
inference(cnf_transformation,[status(thm)],[f503]) ).
fof(f506,plain,
! [X0] :
( ~ cC64(X0)
| ~ cC2xcomp(X0)
| cC66(X0) ),
inference(cnf_transformation,[status(thm)],[f503]) ).
fof(f507,plain,
! [X] :
( ( ! [Y] :
( ~ cC66(Y)
| ~ rR1(X,Y) )
| cC68(X) )
& ( ? [Y] :
( cC66(Y)
& rR1(X,Y) )
| ~ cC68(X) ) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f508,plain,
( ! [X] :
( ! [Y] :
( ~ cC66(Y)
| ~ rR1(X,Y) )
| cC68(X) )
& ! [X] :
( ? [Y] :
( cC66(Y)
& rR1(X,Y) )
| ~ cC68(X) ) ),
inference(miniscoping,[status(thm)],[f507]) ).
fof(f509,plain,
( ! [X] :
( ! [Y] :
( ~ cC66(Y)
| ~ rR1(X,Y) )
| cC68(X) )
& ! [X] :
( ( cC66(sK55_skl(X))
& rR1(X,sK55_skl(X)) )
| ~ cC68(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(Y,sK55_skl(X))],[f508]) ).
fof(f511,plain,
! [X0] :
( cC66(sK55_skl(X0))
| ~ cC68(X0) ),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f512,plain,
! [X0,X1] :
( ~ cC66(X1)
| ~ rR1(X0,X1)
| cC68(X0) ),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f557,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC78(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC78(X) ) ),
inference(NNF_transformation,[status(thm)],[f77]) ).
fof(f558,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC78(X) )
& ! [X] :
( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC78(X) ) ),
inference(miniscoping,[status(thm)],[f557]) ).
fof(f559,plain,
( ! [X] :
( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC78(X) )
& ! [X] :
( ( cC2xcomp(sK62_skl(X))
& rR1(X,sK62_skl(X)) )
| ~ cC78(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(Y,sK62_skl(X))],[f558]) ).
fof(f561,plain,
! [X0] :
( cC2xcomp(sK62_skl(X0))
| ~ cC78(X0) ),
inference(cnf_transformation,[status(thm)],[f559]) ).
fof(f562,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC78(X0) ),
inference(cnf_transformation,[status(thm)],[f559]) ).
fof(f574,plain,
! [X] :
( ( ! [Y] :
( ~ cC6xcomp(Y)
| ~ rR1(X,Y) )
| cC8(X) )
& ( ? [Y] :
( cC6xcomp(Y)
& rR1(X,Y) )
| ~ cC8(X) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f575,plain,
( ! [X] :
( ! [Y] :
( ~ cC6xcomp(Y)
| ~ rR1(X,Y) )
| cC8(X) )
& ! [X] :
( ? [Y] :
( cC6xcomp(Y)
& rR1(X,Y) )
| ~ cC8(X) ) ),
inference(miniscoping,[status(thm)],[f574]) ).
fof(f576,plain,
( ! [X] :
( ! [Y] :
( ~ cC6xcomp(Y)
| ~ rR1(X,Y) )
| cC8(X) )
& ! [X] :
( ( cC6xcomp(sK65_skl(X))
& rR1(X,sK65_skl(X)) )
| ~ cC8(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65_skl]),skolemize(Y,sK65_skl(X))],[f575]) ).
fof(f579,plain,
! [X0,X1] :
( ~ cC6xcomp(X1)
| ~ rR1(X0,X1)
| cC8(X0) ),
inference(cnf_transformation,[status(thm)],[f576]) ).
fof(f580,plain,
! [X] :
( ( ~ cC2xcomp(X)
| ~ cC78xcomp(X)
| cC80(X) )
& ( ( cC2xcomp(X)
& cC78xcomp(X) )
| ~ cC80(X) ) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f581,plain,
( ! [X] :
( ~ cC2xcomp(X)
| ~ cC78xcomp(X)
| cC80(X) )
& ! [X] :
( ( cC2xcomp(X)
& cC78xcomp(X) )
| ~ cC80(X) ) ),
inference(miniscoping,[status(thm)],[f580]) ).
fof(f584,plain,
! [X0] :
( ~ cC2xcomp(X0)
| ~ cC78xcomp(X0)
| cC80(X0) ),
inference(cnf_transformation,[status(thm)],[f581]) ).
fof(f591,plain,
! [X] :
( ( ! [Y] :
( ~ cC80(Y)
| ~ rR1(X,Y) )
| cC82(X) )
& ( ? [Y] :
( cC80(Y)
& rR1(X,Y) )
| ~ cC82(X) ) ),
inference(NNF_transformation,[status(thm)],[f83]) ).
fof(f592,plain,
( ! [X] :
( ! [Y] :
( ~ cC80(Y)
| ~ rR1(X,Y) )
| cC82(X) )
& ! [X] :
( ? [Y] :
( cC80(Y)
& rR1(X,Y) )
| ~ cC82(X) ) ),
inference(miniscoping,[status(thm)],[f591]) ).
fof(f593,plain,
( ! [X] :
( ! [Y] :
( ~ cC80(Y)
| ~ rR1(X,Y) )
| cC82(X) )
& ! [X] :
( ( cC80(sK67_skl(X))
& rR1(X,sK67_skl(X)) )
| ~ cC82(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl]),skolemize(Y,sK67_skl(X))],[f592]) ).
fof(f596,plain,
! [X0,X1] :
( ~ cC80(X1)
| ~ rR1(X0,X1)
| cC82(X0) ),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f680,plain,
rR1(iV8467,iV8471),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f681,plain,
rR1(iV8467,iV8470),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f682,plain,
rR1(iV8467,iV8469),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f683,plain,
rR1(iV8467,iV8474),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f687,plain,
rR1(iV8467,iV8472),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f688,plain,
cC2xcomp(iV8468),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f690,plain,
cC6xcomp(iV8469),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f694,plain,
cTOP(iV8470),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f696,plain,
cC78xcomp(iV8471),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f697,plain,
cC2xcomp(iV8471),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f701,plain,
cC2xcomp(iV8472),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f703,plain,
rR1(iV8472,iV8476),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f704,plain,
cC2xcomp(iV8473),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f706,plain,
cC32xcomp(iV8474),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f710,plain,
cC2xcomp(iV8475),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f712,plain,
cC2(iV8476),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f714,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f136]) ).
fof(f715,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f714]) ).
fof(f716,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f715]) ).
fof(f717,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ( ( xsd_integer(sK81_skl)
| ~ xsd_string(sK81_skl) )
& ( ~ xsd_integer(sK81_skl)
| xsd_string(sK81_skl) ) )
| cowlNothing(sK80_skl)
| ~ cowlThing(sK79_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK79_skl,sK80_skl,sK81_skl]),skolemize(X,sK79_skl),skolemize(X,sK80_skl),skolemize(X,sK81_skl)],[f716]) ).
fof(f718,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK81_skl)
| xsd_string(sK81_skl)
| cowlNothing(sK80_skl)
| ~ cowlThing(sK79_skl) ),
inference(cnf_transformation,[status(thm)],[f717]) ).
fof(f719,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK81_skl)
| ~ xsd_string(sK81_skl)
| cowlNothing(sK80_skl)
| ~ cowlThing(sK79_skl) ),
inference(cnf_transformation,[status(thm)],[f717]) ).
fof(f720,definition,
( sQ0_spl
<=> cowlThing(sK79_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f722,plain,
( sQ0_spl
| ~ cowlThing(sK79_skl) ),
inference(component_clause,[status(thm)],[f720]) ).
fof(f723,definition,
( sQ1_spl
<=> cowlNothing(sK80_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( ~ sQ1_spl
| cowlNothing(sK80_skl) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f726,definition,
( sQ2_spl
<=> xsd_string(sK81_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( ~ sQ2_spl
| xsd_string(sK81_skl) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f729,definition,
( sQ3_spl
<=> xsd_integer(sK81_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f730,plain,
( ~ sQ3_spl
| xsd_integer(sK81_skl) ),
inference(component_clause,[status(thm)],[f729]) ).
fof(f731,plain,
( sQ3_spl
| ~ xsd_integer(sK81_skl) ),
inference(component_clause,[status(thm)],[f729]) ).
fof(f732,definition,
( sQ4_spl
<=> cC20(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f733,plain,
( ~ sQ4_spl
| cC20(iV8467) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f735,definition,
( sQ5_spl
<=> cC4(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f736,plain,
( ~ sQ5_spl
| cC4(iV8467) ),
inference(component_clause,[status(thm)],[f735]) ).
fof(f738,definition,
( sQ6_spl
<=> cC8(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f740,plain,
( sQ6_spl
| ~ cC8(iV8467) ),
inference(component_clause,[status(thm)],[f738]) ).
fof(f741,definition,
( sQ7_spl
<=> cC82(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f743,plain,
( sQ7_spl
| ~ cC82(iV8467) ),
inference(component_clause,[status(thm)],[f741]) ).
fof(f744,definition,
( sQ8_spl
<=> cC62(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f746,plain,
( sQ8_spl
| ~ cC62(iV8467) ),
inference(component_clause,[status(thm)],[f744]) ).
fof(f747,definition,
( sQ9_spl
<=> cC14(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f749,plain,
( sQ9_spl
| ~ cC14(iV8467) ),
inference(component_clause,[status(thm)],[f747]) ).
fof(f750,definition,
( sQ10_spl
<=> cC34(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f752,plain,
( sQ10_spl
| ~ cC34(iV8467) ),
inference(component_clause,[status(thm)],[f750]) ).
fof(f753,definition,
( sQ11_spl
<=> cC10(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f756,definition,
( sQ12_spl
<=> cowlThing(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ12_spl
| ~ cowlThing(iV8467) ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,definition,
( sQ13_spl
<=> cC48(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f760,plain,
( ~ sQ13_spl
| cC48(iV8467) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,definition,
( sQ14_spl
<=> cowlThing(iV8471) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f764,plain,
( sQ14_spl
| ~ cowlThing(iV8471) ),
inference(component_clause,[status(thm)],[f762]) ).
fof(f765,definition,
( sQ15_spl
<=> cC80(iV8471) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ15_spl
| cC80(iV8471) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f768,definition,
( sQ16_spl
<=> cC58(iV8472) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f770,plain,
( sQ16_spl
| ~ cC58(iV8472) ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f771,definition,
( sQ17_spl
<=> cC60(iV8472) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f772,plain,
( ~ sQ17_spl
| cC60(iV8472) ),
inference(component_clause,[status(thm)],[f771]) ).
fof(f774,definition,
( sQ18_spl
<=> cowlThing(iV8472) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( sQ18_spl
| ~ cowlThing(iV8472) ),
inference(component_clause,[status(thm)],[f774]) ).
fof(f777,plain,
( ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f718,f720,f723,f726,f729,f732,f735,f738,f741,f744,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774]) ).
fof(f778,plain,
( ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f719,f720,f723,f726,f729,f732,f735,f738,f741,f744,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774]) ).
fof(f779,plain,
( sQ18_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f776,f138]) ).
fof(f780,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f779]) ).
fof(f784,definition,
( sQ19_spl
<=> cC2xcomp(iV8471) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f786,plain,
( sQ19_spl
| ~ cC2xcomp(iV8471) ),
inference(component_clause,[status(thm)],[f784]) ).
fof(f788,plain,
( ~ cC2xcomp(iV8472)
| cC20(iV8467) ),
inference(resolution,[status(thm)],[f687,f210]) ).
fof(f789,definition,
( sQ20_spl
<=> cC2xcomp(iV8472) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f791,plain,
( sQ20_spl
| ~ cC2xcomp(iV8472) ),
inference(component_clause,[status(thm)],[f789]) ).
fof(f792,plain,
( ~ sQ20_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f788,f732,f789]) ).
fof(f793,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f791,f701]) ).
fof(f794,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f793]) ).
fof(f799,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f786,f697]) ).
fof(f800,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f799]) ).
fof(f806,plain,
! [X0] :
( ~ rR1(X0,iV8476)
| cC58(X0) ),
inference(resolution,[status(thm)],[f712,f456]) ).
fof(f808,plain,
! [X0] :
( ~ rR1(X0,iV8470)
| cC14(X0) ),
inference(resolution,[status(thm)],[f166,f694]) ).
fof(f840,definition,
( sQ24_spl
<=> cC2xcomp(iV8468) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f842,plain,
( sQ24_spl
| ~ cC2xcomp(iV8468) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f846,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f842,f688]) ).
fof(f847,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f846]) ).
fof(f851,definition,
( sQ25_spl
<=> cC2xcomp(iV8473) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f853,plain,
( sQ25_spl
| ~ cC2xcomp(iV8473) ),
inference(component_clause,[status(thm)],[f851]) ).
fof(f857,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f853,f704]) ).
fof(f858,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f857]) ).
fof(f862,definition,
( sQ26_spl
<=> cC2xcomp(iV8475) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ26_spl
| ~ cC2xcomp(iV8475) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f868,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f710]) ).
fof(f869,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f868]) ).
fof(f870,plain,
cC58(iV8472),
inference(resolution,[status(thm)],[f703,f806]) ).
fof(f889,plain,
( ~ cC2xcomp(iV8472)
| cC60(iV8472) ),
inference(resolution,[status(thm)],[f870,f478]) ).
fof(f890,plain,
( ~ sQ20_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f889,f771,f789]) ).
fof(f891,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f770,f870]) ).
fof(f892,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f891]) ).
fof(f893,plain,
! [X0] :
( ~ sQ17_spl
| ~ rR1(X0,iV8472)
| cC62(X0) ),
inference(resolution,[status(thm)],[f772,f484]) ).
fof(f900,plain,
( ~ sQ17_spl
| cC62(iV8467) ),
inference(resolution,[status(thm)],[f893,f687]) ).
fof(f929,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f764,f138]) ).
fof(f930,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f929]) ).
fof(f931,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f758,f138]) ).
fof(f932,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f931]) ).
fof(f933,plain,
( sQ8_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f746,f900]) ).
fof(f934,plain,
( sQ8_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f933]) ).
fof(f935,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f139]) ).
fof(f936,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f935]) ).
fof(f937,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f722,f138]) ).
fof(f938,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f937]) ).
fof(f947,plain,
( ~ sQ4_spl
| rR1(iV8467,sK9_skl(iV8467)) ),
inference(resolution,[status(thm)],[f208,f733]) ).
fof(f948,plain,
( ~ sQ4_spl
| ra_Px5(iV8467,sK10_skl(iV8467)) ),
inference(resolution,[status(thm)],[f214,f733]) ).
fof(f949,plain,
( ~ sQ4_spl
| ~ cC2xcomp(sK9_skl(iV8467))
| cC48(iV8467) ),
inference(resolution,[status(thm)],[f947,f384]) ).
fof(f952,definition,
( sQ33_spl
<=> cC2xcomp(sK9_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f954,plain,
( sQ33_spl
| ~ cC2xcomp(sK9_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f952]) ).
fof(f955,plain,
( ~ sQ4_spl
| ~ sQ33_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f949,f759,f952,f732]) ).
fof(f958,plain,
( sQ33_spl
| ~ cC20(iV8467) ),
inference(resolution,[status(thm)],[f954,f209]) ).
fof(f960,plain,
( sQ33_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f958,f733]) ).
fof(f961,plain,
( sQ33_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f960]) ).
fof(f982,plain,
! [X0] :
( ~ rR1(X0,iV8472)
| cC22(X0) ),
inference(resolution,[status(thm)],[f227,f701]) ).
fof(f985,plain,
cC22(iV8467),
inference(resolution,[status(thm)],[f982,f687]) ).
fof(f991,definition,
( sQ34_spl
<=> cC2xcomp(sK12_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f993,plain,
( sQ34_spl
| ~ cC2xcomp(sK12_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f991]) ).
fof(f997,plain,
( sQ34_spl
| ~ cC22(iV8467) ),
inference(resolution,[status(thm)],[f993,f226]) ).
fof(f999,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f997,f985]) ).
fof(f1000,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f999]) ).
fof(f1014,plain,
( ~ sQ17_spl
| cC60(sK51_skl(iV8467)) ),
inference(resolution,[status(thm)],[f483,f900]) ).
fof(f1016,plain,
( ~ sQ17_spl
| cC58(sK51_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1014,f477]) ).
fof(f1017,plain,
( ~ sQ17_spl
| cC2xcomp(sK51_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1014,f476]) ).
fof(f1018,plain,
( ~ sQ17_spl
| ~ cC2xcomp(sK51_skl(iV8467))
| cC60(sK51_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1016,f478]) ).
fof(f1019,definition,
( sQ35_spl
<=> cC60(sK51_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1022,definition,
( sQ36_spl
<=> cC2xcomp(sK51_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1024,plain,
( sQ36_spl
| ~ cC2xcomp(sK51_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f1022]) ).
fof(f1025,plain,
( ~ sQ17_spl
| ~ sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1018,f1019,f1022,f771]) ).
fof(f1031,plain,
cC14(iV8467),
inference(resolution,[status(thm)],[f808,f681]) ).
fof(f1035,plain,
! [X0] :
( ~ rR1(X0,iV8474)
| cC34(X0) ),
inference(resolution,[status(thm)],[f299,f706]) ).
fof(f1074,plain,
cC34(iV8467),
inference(resolution,[status(thm)],[f1035,f683]) ).
fof(f1079,plain,
( ~ sQ5_spl
| rR1(iV8467,sK29_skl(iV8467)) ),
inference(resolution,[status(thm)],[f332,f736]) ).
fof(f1084,definition,
( sQ38_spl
<=> cC2xcomp(sK29_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1086,plain,
( sQ38_spl
| ~ cC2xcomp(sK29_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f1084]) ).
fof(f1090,plain,
( sQ38_spl
| ~ cC4(iV8467) ),
inference(resolution,[status(thm)],[f1086,f333]) ).
fof(f1092,plain,
( sQ38_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1090,f736]) ).
fof(f1093,plain,
( sQ38_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1092]) ).
fof(f1220,plain,
( ~ sQ13_spl
| rR1(iV8467,sK36_skl(iV8467)) ),
inference(resolution,[status(thm)],[f382,f760]) ).
fof(f1235,plain,
( ~ sQ13_spl
| ~ cC2xcomp(sK36_skl(iV8467))
| cC4(iV8467) ),
inference(resolution,[status(thm)],[f1220,f334]) ).
fof(f1237,definition,
( sQ46_spl
<=> cC2xcomp(sK36_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1239,plain,
( sQ46_spl
| ~ cC2xcomp(sK36_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f1237]) ).
fof(f1241,plain,
( ~ sQ13_spl
| ~ sQ46_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1235,f735,f1237,f759]) ).
fof(f1243,plain,
( sQ46_spl
| ~ cC48(iV8467) ),
inference(resolution,[status(thm)],[f1239,f383]) ).
fof(f1245,plain,
( sQ46_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1243,f760]) ).
fof(f1246,plain,
( sQ46_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f1245]) ).
fof(f1399,plain,
( ~ sQ5_spl
| ~ cC2xcomp(sK29_skl(iV8467))
| cC6(iV8467) ),
inference(resolution,[status(thm)],[f468,f1079]) ).
fof(f1424,definition,
( sQ57_spl
<=> cC6(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1425,plain,
( ~ sQ57_spl
| cC6(iV8467) ),
inference(component_clause,[status(thm)],[f1424]) ).
fof(f1429,plain,
( ~ sQ5_spl
| ~ sQ38_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1399,f1424,f1084,f735]) ).
fof(f1442,plain,
( ~ sQ57_spl
| rR1(iV8467,sK49_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1425,f466]) ).
fof(f1443,plain,
( ~ sQ57_spl
| cC2xcomp(sK49_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1425,f467]) ).
fof(f1452,definition,
( sQ58_spl
<=> cC2xcomp(sK49_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1454,plain,
( sQ58_spl
| ~ cC2xcomp(sK49_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f1452]) ).
fof(f1480,plain,
( sQ58_spl
| ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1454,f1443]) ).
fof(f1481,plain,
( sQ58_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f1480]) ).
fof(f1500,plain,
( sQ36_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1024,f1017]) ).
fof(f1501,plain,
( sQ36_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f1500]) ).
fof(f1557,plain,
! [X0] :
( ~ rR1(X0,iV8476)
| cC64(X0) ),
inference(resolution,[status(thm)],[f501,f712]) ).
fof(f1578,plain,
cC64(iV8472),
inference(resolution,[status(thm)],[f1557,f703]) ).
fof(f1579,plain,
( ~ cC2xcomp(iV8472)
| cC66(iV8472) ),
inference(resolution,[status(thm)],[f1578,f506]) ).
fof(f1582,definition,
( sQ61_spl
<=> cC66(iV8472) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1583,plain,
( ~ sQ61_spl
| cC66(iV8472) ),
inference(component_clause,[status(thm)],[f1582]) ).
fof(f1585,plain,
( ~ sQ20_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1579,f1582,f789]) ).
fof(f1615,plain,
! [X0] :
( ~ sQ61_spl
| ~ rR1(X0,iV8472)
| cC68(X0) ),
inference(resolution,[status(thm)],[f512,f1583]) ).
fof(f1732,plain,
( ~ sQ61_spl
| cC68(iV8467) ),
inference(resolution,[status(thm)],[f1615,f687]) ).
fof(f1735,plain,
( ~ sQ61_spl
| cC66(sK55_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1732,f511]) ).
fof(f1737,plain,
( ~ sQ61_spl
| cC64(sK55_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1735,f505]) ).
fof(f1738,plain,
( ~ sQ61_spl
| cC2xcomp(sK55_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1735,f504]) ).
fof(f1739,plain,
( ~ sQ61_spl
| ~ cC2xcomp(sK55_skl(iV8467))
| cC66(sK55_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1737,f506]) ).
fof(f1742,definition,
( sQ66_spl
<=> cC66(sK55_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1745,definition,
( sQ67_spl
<=> cC2xcomp(sK55_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1747,plain,
( sQ67_spl
| ~ cC2xcomp(sK55_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f1745]) ).
fof(f1748,plain,
( ~ sQ61_spl
| ~ sQ67_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1739,f1742,f1745,f1582]) ).
fof(f1754,definition,
( sQ68_spl
<=> cC26(iV8467) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1755,plain,
( ~ sQ68_spl
| cC26(iV8467) ),
inference(component_clause,[status(thm)],[f1754]) ).
fof(f1793,plain,
( ~ sQ68_spl
| cC20xcomp(iV8467) ),
inference(resolution,[status(thm)],[f1755,f237]) ).
fof(f1795,plain,
! [X0] :
( ~ sQ68_spl
| ~ ra_Px5(iV8467,X0) ),
inference(resolution,[status(thm)],[f1793,f220]) ).
fof(f1796,plain,
( ~ sQ4_spl
| ~ sQ68_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f948,f1795]) ).
fof(f1798,plain,
( ~ sQ4_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f1796]) ).
fof(f1824,plain,
( sQ67_spl
| ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1747,f1738]) ).
fof(f1825,plain,
( sQ67_spl
| ~ sQ61_spl ),
inference(contradiction_clause,[status(thm)],[f1824]) ).
fof(f1854,plain,
! [X0] :
( ~ sQ57_spl
| ~ rR1(X0,sK49_skl(iV8467))
| cC78(X0) ),
inference(resolution,[status(thm)],[f562,f1443]) ).
fof(f1880,plain,
( ~ sQ57_spl
| cC78(iV8467) ),
inference(resolution,[status(thm)],[f1854,f1442]) ).
fof(f1883,plain,
( ~ sQ57_spl
| cC2xcomp(sK62_skl(iV8467)) ),
inference(resolution,[status(thm)],[f1880,f561]) ).
fof(f1903,definition,
( sQ74_spl
<=> cC2xcomp(sK62_skl(iV8467)) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1905,plain,
( sQ74_spl
| ~ cC2xcomp(sK62_skl(iV8467)) ),
inference(component_clause,[status(thm)],[f1903]) ).
fof(f1910,plain,
( sQ74_spl
| ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1905,f1883]) ).
fof(f1911,plain,
( sQ74_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f1910]) ).
fof(f1917,plain,
! [X0] :
( ~ rR1(X0,iV8469)
| cC8(X0) ),
inference(resolution,[status(thm)],[f579,f690]) ).
fof(f1919,plain,
( ~ cC2xcomp(iV8471)
| cC80(iV8471) ),
inference(resolution,[status(thm)],[f584,f696]) ).
fof(f1921,plain,
( ~ sQ19_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f1919,f765,f784]) ).
fof(f1924,plain,
! [X0] :
( ~ sQ15_spl
| ~ rR1(X0,iV8471)
| cC82(X0) ),
inference(resolution,[status(thm)],[f766,f596]) ).
fof(f1926,plain,
( ~ sQ15_spl
| cC82(iV8467) ),
inference(resolution,[status(thm)],[f1924,f680]) ).
fof(f1945,plain,
cC8(iV8467),
inference(resolution,[status(thm)],[f1917,f682]) ).
fof(f1947,plain,
( ~ cC4(iV8467)
| cC10(iV8467) ),
inference(resolution,[status(thm)],[f1945,f148]) ).
fof(f1948,plain,
( ~ sQ5_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f1947,f753,f735]) ).
fof(f1949,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f752,f1074]) ).
fof(f1950,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1949]) ).
fof(f1951,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f749,f1031]) ).
fof(f1952,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1951]) ).
fof(f1953,plain,
( sQ7_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f743,f1926]) ).
fof(f1954,plain,
( sQ7_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1953]) ).
fof(f1955,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f740,f1945]) ).
fof(f1956,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1955]) ).
fof(f1961,plain,
( ~ sQ3_spl
| ~ xsd_string(sK81_skl) ),
inference(resolution,[status(thm)],[f730,f142]) ).
fof(f1962,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1961,f727]) ).
fof(f1963,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1962]) ).
fof(f1964,plain,
( sQ3_spl
| xsd_string(sK81_skl) ),
inference(resolution,[status(thm)],[f731,f143]) ).
fof(f1965,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1964,f726,f729]) ).
fof(f1966,plain,
$false,
inference(sat_refutation,[status(thm)],[f777,f778,f780,f792,f794,f800,f847,f858,f869,f890,f892,f930,f932,f934,f936,f938,f955,f961,f1000,f1025,f1093,f1241,f1246,f1429,f1481,f1501,f1585,f1748,f1798,f1825,f1911,f1921,f1948,f1950,f1952,f1954,f1956,f1963,f1965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 22:57:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.44 % Elapsed time: 0.066547 seconds
% 0.14/0.44 % CPU time: 0.268359 seconds
% 0.14/0.44 % Total memory used: 29.297 MB
% 0.14/0.44 % Net memory used: 29.152 MB
%------------------------------------------------------------------------------