%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:50 PM UTC 2026
% Result : Theorem 0.13s 0.40s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 121
% Syntax : Number of formulae : 457 ( 131 unt; 64 def)
% Number of atoms : 1457 ( 0 equ)
% Maximal formula atoms : 51 ( 3 avg)
% Number of connectives : 1671 ( 671 ~; 715 |; 192 &)
% ( 84 <=>; 8 =>; 0 <=; 1 <~>)
% Maximal formula depth : 50 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 110 ( 109 usr; 65 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 17 con; 0-1 aty)
% Number of variables : 168 ( 152 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] :
( cC104(X)
<=> ? [Y] :
( cC102xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] :
( cC106(X)
<=> ( cC100xcomp(X)
& cC104(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] :
( cC34(X)
<=> ( cC32xcomp(X)
& cC30xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X] :
( cC38(X)
<=> ( cC36xcomp(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& cC40xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [X] :
( cC50(X)
<=> ( cC48xcomp(X)
& cC46xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [X] :
( cC56(X)
<=> ( cC44(X)
& cC54xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [X] :
( cC62(X)
<=> ( cC58xcomp(X)
& cC60(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC64xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& cC74xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,axiom,
! [X] :
( cC82(X)
<=> ( cC78xcomp(X)
& cC80(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [X] :
( cC88(X)
<=> ( cC86xcomp(X)
& cC84xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& cC96xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,axiom,
cC100xcomp(iV16439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,axiom,
! [X] :
( rR1(iV16440,X)
=> cC76(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,axiom,
cC102xcomp(iV16440),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
cC36xcomp(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [X] :
( rR1(iV16448,X)
=> cC88(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
rR1(iV16448,iV16449),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,axiom,
cC74xcomp(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [X] :
( rR1(iV16453,X)
=> cC56(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,axiom,
cC58xcomp(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,axiom,
cC40xcomp(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,axiom,
! [X] :
( rR1(iV16455,X)
=> cC38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,axiom,
cC54xcomp(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,axiom,
cC36xcomp(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,axiom,
cC30xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,axiom,
cC84xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,axiom,
cC46xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f214,axiom,
cC64xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,axiom,
cC86xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,axiom,
cC32xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,axiom,
cC48xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f222,axiom,
cC66xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f228,axiom,
cC8xcomp(iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f238,axiom,
cC12xcomp(iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,axiom,
! [X] :
( rR1(iV16461,X)
=> cC38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,axiom,
rR1(iV16461,iV16462),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,axiom,
! [X] :
( rR1(iV16463,X)
=> cC56(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,axiom,
! [X] :
( rR1(iV16464,X)
=> cC38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,axiom,
rR1(iV16464,iV16465),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f287,conjecture,
( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f288,negated_conjecture,
~ ( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f287]) ).
fof(f289,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f290,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f291,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f292,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f293,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f292]) ).
fof(f294,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f295,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f340,plain,
! [X] :
( ( ! [Y] :
( ~ cC102xcomp(Y)
| ~ rR1(X,Y) )
| cC104(X) )
& ( ? [Y] :
( cC102xcomp(Y)
& rR1(X,Y) )
| ~ cC104(X) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f341,plain,
( ! [X] :
( ! [Y] :
( ~ cC102xcomp(Y)
| ~ rR1(X,Y) )
| cC104(X) )
& ! [X] :
( ? [Y] :
( cC102xcomp(Y)
& rR1(X,Y) )
| ~ cC104(X) ) ),
inference(miniscoping,[status(thm)],[f340]) ).
fof(f342,plain,
( ! [X] :
( ! [Y] :
( ~ cC102xcomp(Y)
| ~ rR1(X,Y) )
| cC104(X) )
& ! [X] :
( ( cC102xcomp(sK7_skl(X))
& rR1(X,sK7_skl(X)) )
| ~ cC104(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Y,sK7_skl(X))],[f341]) ).
fof(f345,plain,
! [X0,X1] :
( ~ cC102xcomp(X1)
| ~ rR1(X0,X1)
| cC104(X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f346,plain,
! [X] :
( ( ~ cC100xcomp(X)
| ~ cC104(X)
| cC106(X) )
& ( ( cC100xcomp(X)
& cC104(X) )
| ~ cC106(X) ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f347,plain,
( ! [X] :
( ~ cC100xcomp(X)
| ~ cC104(X)
| cC106(X) )
& ! [X] :
( ( cC100xcomp(X)
& cC104(X) )
| ~ cC106(X) ) ),
inference(miniscoping,[status(thm)],[f346]) ).
fof(f350,plain,
! [X0] :
( ~ cC100xcomp(X0)
| ~ cC104(X0)
| cC106(X0) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f351,plain,
! [X] :
( ( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f352,plain,
( ! [X] :
( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ! [X] :
( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(miniscoping,[status(thm)],[f351]) ).
fof(f353,plain,
! [X0] :
( cC28(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f355,plain,
! [X0] :
( ~ cC106(X0)
| ~ cC28(X0)
| cC108(X0) ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f571,plain,
! [X] :
( ( ~ cC32xcomp(X)
| ~ cC30xcomp(X)
| cC34(X) )
& ( ( cC32xcomp(X)
& cC30xcomp(X) )
| ~ cC34(X) ) ),
inference(NNF_transformation,[status(thm)],[f53]) ).
fof(f572,plain,
( ! [X] :
( ~ cC32xcomp(X)
| ~ cC30xcomp(X)
| cC34(X) )
& ! [X] :
( ( cC32xcomp(X)
& cC30xcomp(X) )
| ~ cC34(X) ) ),
inference(miniscoping,[status(thm)],[f571]) ).
fof(f575,plain,
! [X0] :
( ~ cC32xcomp(X0)
| ~ cC30xcomp(X0)
| cC34(X0) ),
inference(cnf_transformation,[status(thm)],[f572]) ).
fof(f599,plain,
! [X] :
( ( ~ cC36xcomp(X)
| ~ cTOP(X)
| cC38(X) )
& ( ( cC36xcomp(X)
& cTOP(X) )
| ~ cC38(X) ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f600,plain,
( ! [X] :
( ~ cC36xcomp(X)
| ~ cTOP(X)
| cC38(X) )
& ! [X] :
( ( cC36xcomp(X)
& cTOP(X) )
| ~ cC38(X) ) ),
inference(miniscoping,[status(thm)],[f599]) ).
fof(f603,plain,
! [X0] :
( ~ cC36xcomp(X0)
| ~ cTOP(X0)
| cC38(X0) ),
inference(cnf_transformation,[status(thm)],[f600]) ).
fof(f643,plain,
! [X] :
( ( ! [Y] :
( ~ cC8xcomp(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ( ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(NNF_transformation,[status(thm)],[f66]) ).
fof(f644,plain,
( ! [X] :
( ! [Y] :
( ~ cC8xcomp(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ! [X] :
( ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(miniscoping,[status(thm)],[f643]) ).
fof(f645,plain,
( ! [X] :
( ! [Y] :
( ~ cC8xcomp(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ! [X] :
( ( cC8xcomp(sK50_skl(X))
& rR1(X,sK50_skl(X)) )
| ~ cC42(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(Y,sK50_skl(X))],[f644]) ).
fof(f648,plain,
! [X0,X1] :
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(cnf_transformation,[status(thm)],[f645]) ).
fof(f649,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC40xcomp(X)
| cC44(X) )
& ( ( cC42(X)
& cC40xcomp(X) )
| ~ cC44(X) ) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f650,plain,
( ! [X] :
( ~ cC42(X)
| ~ cC40xcomp(X)
| cC44(X) )
& ! [X] :
( ( cC42(X)
& cC40xcomp(X) )
| ~ cC44(X) ) ),
inference(miniscoping,[status(thm)],[f649]) ).
fof(f652,plain,
! [X0] :
( cC42(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[status(thm)],[f650]) ).
fof(f653,plain,
! [X0] :
( ~ cC42(X0)
| ~ cC40xcomp(X0)
| cC44(X0) ),
inference(cnf_transformation,[status(thm)],[f650]) ).
fof(f686,plain,
! [X] :
( ( ~ cC48xcomp(X)
| ~ cC46xcomp(X)
| cC50(X) )
& ( ( cC48xcomp(X)
& cC46xcomp(X) )
| ~ cC50(X) ) ),
inference(NNF_transformation,[status(thm)],[f74]) ).
fof(f687,plain,
( ! [X] :
( ~ cC48xcomp(X)
| ~ cC46xcomp(X)
| cC50(X) )
& ! [X] :
( ( cC48xcomp(X)
& cC46xcomp(X) )
| ~ cC50(X) ) ),
inference(miniscoping,[status(thm)],[f686]) ).
fof(f690,plain,
! [X0] :
( ~ cC48xcomp(X0)
| ~ cC46xcomp(X0)
| cC50(X0) ),
inference(cnf_transformation,[status(thm)],[f687]) ).
fof(f736,plain,
! [X] :
( ( ~ cC44(X)
| ~ cC54xcomp(X)
| cC56(X) )
& ( ( cC44(X)
& cC54xcomp(X) )
| ~ cC56(X) ) ),
inference(NNF_transformation,[status(thm)],[f83]) ).
fof(f737,plain,
( ! [X] :
( ~ cC44(X)
| ~ cC54xcomp(X)
| cC56(X) )
& ! [X] :
( ( cC44(X)
& cC54xcomp(X) )
| ~ cC56(X) ) ),
inference(miniscoping,[status(thm)],[f736]) ).
fof(f739,plain,
! [X0] :
( cC44(X0)
| ~ cC56(X0) ),
inference(cnf_transformation,[status(thm)],[f737]) ).
fof(f740,plain,
! [X0] :
( ~ cC44(X0)
| ~ cC54xcomp(X0)
| cC56(X0) ),
inference(cnf_transformation,[status(thm)],[f737]) ).
fof(f785,plain,
! [X] :
( ( ! [Y] :
( ~ cC12xcomp(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ( ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(NNF_transformation,[status(thm)],[f92]) ).
fof(f786,plain,
( ! [X] :
( ! [Y] :
( ~ cC12xcomp(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ! [X] :
( ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(miniscoping,[status(thm)],[f785]) ).
fof(f787,plain,
( ! [X] :
( ! [Y] :
( ~ cC12xcomp(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ! [X] :
( ( cC12xcomp(sK70_skl(X))
& rR1(X,sK70_skl(X)) )
| ~ cC60(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70_skl]),skolemize(Y,sK70_skl(X))],[f786]) ).
fof(f790,plain,
! [X0,X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(cnf_transformation,[status(thm)],[f787]) ).
fof(f791,plain,
! [X] :
( ( ~ cC58xcomp(X)
| ~ cC60(X)
| cC62(X) )
& ( ( cC58xcomp(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(NNF_transformation,[status(thm)],[f93]) ).
fof(f792,plain,
( ! [X] :
( ~ cC58xcomp(X)
| ~ cC60(X)
| cC62(X) )
& ! [X] :
( ( cC58xcomp(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(miniscoping,[status(thm)],[f791]) ).
fof(f793,plain,
! [X0] :
( cC60(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f792]) ).
fof(f795,plain,
! [X0] :
( ~ cC58xcomp(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f792]) ).
fof(f833,plain,
! [X] :
( ( ~ cC66xcomp(X)
| ~ cC64xcomp(X)
| cC68(X) )
& ( ( cC66xcomp(X)
& cC64xcomp(X) )
| ~ cC68(X) ) ),
inference(NNF_transformation,[status(thm)],[f101]) ).
fof(f834,plain,
( ! [X] :
( ~ cC66xcomp(X)
| ~ cC64xcomp(X)
| cC68(X) )
& ! [X] :
( ( cC66xcomp(X)
& cC64xcomp(X) )
| ~ cC68(X) ) ),
inference(miniscoping,[status(thm)],[f833]) ).
fof(f837,plain,
! [X0] :
( ~ cC66xcomp(X0)
| ~ cC64xcomp(X0)
| cC68(X0) ),
inference(cnf_transformation,[status(thm)],[f834]) ).
fof(f900,plain,
! [X] :
( ( ~ cC62(X)
| ~ cC74xcomp(X)
| cC76(X) )
& ( ( cC62(X)
& cC74xcomp(X) )
| ~ cC76(X) ) ),
inference(NNF_transformation,[status(thm)],[f113]) ).
fof(f901,plain,
( ! [X] :
( ~ cC62(X)
| ~ cC74xcomp(X)
| cC76(X) )
& ! [X] :
( ( cC62(X)
& cC74xcomp(X) )
| ~ cC76(X) ) ),
inference(miniscoping,[status(thm)],[f900]) ).
fof(f903,plain,
! [X0] :
( cC62(X0)
| ~ cC76(X0) ),
inference(cnf_transformation,[status(thm)],[f901]) ).
fof(f904,plain,
! [X0] :
( ~ cC62(X0)
| ~ cC74xcomp(X0)
| cC76(X0) ),
inference(cnf_transformation,[status(thm)],[f901]) ).
fof(f945,plain,
! [X] :
( ( ~ cC78xcomp(X)
| ~ cC80(X)
| cC82(X) )
& ( ( cC78xcomp(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(NNF_transformation,[status(thm)],[f121]) ).
fof(f946,plain,
( ! [X] :
( ~ cC78xcomp(X)
| ~ cC80(X)
| cC82(X) )
& ! [X] :
( ( cC78xcomp(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(miniscoping,[status(thm)],[f945]) ).
fof(f947,plain,
! [X0] :
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(thm)],[f946]) ).
fof(f987,plain,
! [X] :
( ( ~ cC86xcomp(X)
| ~ cC84xcomp(X)
| cC88(X) )
& ( ( cC86xcomp(X)
& cC84xcomp(X) )
| ~ cC88(X) ) ),
inference(NNF_transformation,[status(thm)],[f129]) ).
fof(f988,plain,
( ! [X] :
( ~ cC86xcomp(X)
| ~ cC84xcomp(X)
| cC88(X) )
& ! [X] :
( ( cC86xcomp(X)
& cC84xcomp(X) )
| ~ cC88(X) ) ),
inference(miniscoping,[status(thm)],[f987]) ).
fof(f989,plain,
! [X0] :
( cC84xcomp(X0)
| ~ cC88(X0) ),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f990,plain,
! [X0] :
( cC86xcomp(X0)
| ~ cC88(X0) ),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f991,plain,
! [X0] :
( ~ cC86xcomp(X0)
| ~ cC84xcomp(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f1071,plain,
! [X] :
( ( ~ cC82(X)
| ~ cC96xcomp(X)
| cC98(X) )
& ( ( cC82(X)
& cC96xcomp(X) )
| ~ cC98(X) ) ),
inference(NNF_transformation,[status(thm)],[f144]) ).
fof(f1072,plain,
( ! [X] :
( ~ cC82(X)
| ~ cC96xcomp(X)
| cC98(X) )
& ! [X] :
( ( cC82(X)
& cC96xcomp(X) )
| ~ cC98(X) ) ),
inference(miniscoping,[status(thm)],[f1071]) ).
fof(f1074,plain,
! [X0] :
( cC82(X0)
| ~ cC98(X0) ),
inference(cnf_transformation,[status(thm)],[f1072]) ).
fof(f1082,plain,
! [X] :
( ( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(NNF_transformation,[status(thm)],[f146]) ).
fof(f1083,plain,
( ! [X] :
( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ! [X] :
( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(miniscoping,[status(thm)],[f1082]) ).
fof(f1084,plain,
! [X0] :
( cC108(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f1083]) ).
fof(f1085,plain,
! [X0] :
( cC130(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f1083]) ).
fof(f1087,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(pre_NNF_transformation,[status(thm)],[f147]) ).
fof(f1088,plain,
! [X0] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[status(thm)],[f1087]) ).
fof(f1090,plain,
cC100xcomp(iV16439),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f1091,plain,
cTEST(iV16439),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f1092,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f1099,plain,
! [X] :
( cC76(X)
| ~ rR1(iV16440,X) ),
inference(pre_NNF_transformation,[status(thm)],[f157]) ).
fof(f1100,plain,
! [X0] :
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(cnf_transformation,[status(thm)],[f1099]) ).
fof(f1101,plain,
cC102xcomp(iV16440),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f1103,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f1107,plain,
cTOP(iV16448),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f1115,plain,
cC36xcomp(iV16448),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f1117,plain,
! [X] :
( cC88(X)
| ~ rR1(iV16448,X) ),
inference(pre_NNF_transformation,[status(thm)],[f171]) ).
fof(f1118,plain,
! [X0] :
( cC88(X0)
| ~ rR1(iV16448,X0) ),
inference(cnf_transformation,[status(thm)],[f1117]) ).
fof(f1120,plain,
rR1(iV16448,iV16449),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f1122,plain,
cC74xcomp(iV16453),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f1127,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16453,X) ),
inference(pre_NNF_transformation,[status(thm)],[f179]) ).
fof(f1128,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(cnf_transformation,[status(thm)],[f1127]) ).
fof(f1132,plain,
cC58xcomp(iV16453),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f1133,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f1137,plain,
cC40xcomp(iV16455),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f1141,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16455,X) ),
inference(pre_NNF_transformation,[status(thm)],[f189]) ).
fof(f1142,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16455,X0) ),
inference(cnf_transformation,[status(thm)],[f1141]) ).
fof(f1144,plain,
cC54xcomp(iV16455),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f1148,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f1154,plain,
cTOP(iV16457),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f1159,plain,
cC36xcomp(iV16457),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f1168,plain,
cC30xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f1169,plain,
cC84xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f1171,plain,
cC46xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f1172,plain,
cC64xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f1174,plain,
cC86xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f1175,plain,
cC32xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f1176,plain,
cC48xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f1180,plain,
cC66xcomp(iV16459),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f1188,plain,
cC8xcomp(iV16460),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f1202,plain,
cC12xcomp(iV16461),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f1207,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16461,X) ),
inference(pre_NNF_transformation,[status(thm)],[f242]) ).
fof(f1208,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16461,X0) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1210,plain,
rR1(iV16461,iV16462),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f1234,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16463,X) ),
inference(pre_NNF_transformation,[status(thm)],[f262]) ).
fof(f1235,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(cnf_transformation,[status(thm)],[f1234]) ).
fof(f1237,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f1239,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16464,X) ),
inference(pre_NNF_transformation,[status(thm)],[f266]) ).
fof(f1240,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16464,X0) ),
inference(cnf_transformation,[status(thm)],[f1239]) ).
fof(f1252,plain,
rR1(iV16464,iV16465),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f1268,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f288]) ).
fof(f1269,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f1268]) ).
fof(f1270,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1269]) ).
fof(f1271,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ( ( xsd_integer(sK116_skl)
| ~ xsd_string(sK116_skl) )
& ( ~ xsd_integer(sK116_skl)
| xsd_string(sK116_skl) ) )
| cowlNothing(sK115_skl)
| ~ cowlThing(sK114_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK114_skl,sK115_skl,sK116_skl]),skolemize(X,sK114_skl),skolemize(X,sK115_skl),skolemize(X,sK116_skl)],[f1270]) ).
fof(f1272,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK116_skl)
| xsd_string(sK116_skl)
| cowlNothing(sK115_skl)
| ~ cowlThing(sK114_skl) ),
inference(cnf_transformation,[status(thm)],[f1271]) ).
fof(f1273,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK116_skl)
| ~ xsd_string(sK116_skl)
| cowlNothing(sK115_skl)
| ~ cowlThing(sK114_skl) ),
inference(cnf_transformation,[status(thm)],[f1271]) ).
fof(f1274,definition,
( sQ0_spl
<=> cowlThing(sK114_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1276,plain,
( sQ0_spl
| ~ cowlThing(sK114_skl) ),
inference(component_clause,[status(thm)],[f1274]) ).
fof(f1277,definition,
( sQ1_spl
<=> cowlNothing(sK115_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1278,plain,
( ~ sQ1_spl
| cowlNothing(sK115_skl) ),
inference(component_clause,[status(thm)],[f1277]) ).
fof(f1280,definition,
( sQ2_spl
<=> xsd_string(sK116_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1281,plain,
( ~ sQ2_spl
| xsd_string(sK116_skl) ),
inference(component_clause,[status(thm)],[f1280]) ).
fof(f1283,definition,
( sQ3_spl
<=> xsd_integer(sK116_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1284,plain,
( ~ sQ3_spl
| xsd_integer(sK116_skl) ),
inference(component_clause,[status(thm)],[f1283]) ).
fof(f1285,plain,
( sQ3_spl
| ~ xsd_integer(sK116_skl) ),
inference(component_clause,[status(thm)],[f1283]) ).
fof(f1286,definition,
( sQ4_spl
<=> cC130(iV16439) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1288,plain,
( sQ4_spl
| ~ cC130(iV16439) ),
inference(component_clause,[status(thm)],[f1286]) ).
fof(f1289,definition,
( sQ5_spl
<=> cC108(iV16439) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1292,definition,
( sQ6_spl
<=> cC104(iV16439) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1295,definition,
( sQ7_spl
<=> cC106(iV16439) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1296,plain,
( ~ sQ7_spl
| cC106(iV16439) ),
inference(component_clause,[status(thm)],[f1295]) ).
fof(f1298,definition,
( sQ8_spl
<=> cC28(iV16439) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1300,plain,
( sQ8_spl
| ~ cC28(iV16439) ),
inference(component_clause,[status(thm)],[f1298]) ).
fof(f1301,definition,
( sQ9_spl
<=> cowlThing(iV16439) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( sQ9_spl
| ~ cowlThing(iV16439) ),
inference(component_clause,[status(thm)],[f1301]) ).
fof(f1304,definition,
( sQ10_spl
<=> cC98(iV16440) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1306,plain,
( sQ10_spl
| ~ cC98(iV16440) ),
inference(component_clause,[status(thm)],[f1304]) ).
fof(f1307,definition,
( sQ11_spl
<=> cC80(iV16440) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1309,plain,
( sQ11_spl
| ~ cC80(iV16440) ),
inference(component_clause,[status(thm)],[f1307]) ).
fof(f1310,definition,
( sQ12_spl
<=> cC82(iV16440) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1312,plain,
( sQ12_spl
| ~ cC82(iV16440) ),
inference(component_clause,[status(thm)],[f1310]) ).
fof(f1313,definition,
( sQ13_spl
<=> cowlThing(iV16440) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1315,plain,
( sQ13_spl
| ~ cowlThing(iV16440) ),
inference(component_clause,[status(thm)],[f1313]) ).
fof(f1316,definition,
( sQ14_spl
<=> cC38(iV16448) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1319,definition,
( sQ15_spl
<=> cowlThing(iV16448) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1321,plain,
( sQ15_spl
| ~ cowlThing(iV16448) ),
inference(component_clause,[status(thm)],[f1319]) ).
fof(f1322,definition,
( sQ16_spl
<=> cC76(iV16453) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1325,definition,
( sQ17_spl
<=> cC62(iV16453) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1327,plain,
( sQ17_spl
| ~ cC62(iV16453) ),
inference(component_clause,[status(thm)],[f1325]) ).
fof(f1328,definition,
( sQ18_spl
<=> cowlThing(iV16453) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1330,plain,
( sQ18_spl
| ~ cowlThing(iV16453) ),
inference(component_clause,[status(thm)],[f1328]) ).
fof(f1331,definition,
( sQ19_spl
<=> cC60(iV16453) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1333,plain,
( sQ19_spl
| ~ cC60(iV16453) ),
inference(component_clause,[status(thm)],[f1331]) ).
fof(f1334,definition,
( sQ20_spl
<=> cC56(iV16455) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1336,plain,
( sQ20_spl
| ~ cC56(iV16455) ),
inference(component_clause,[status(thm)],[f1334]) ).
fof(f1337,definition,
( sQ21_spl
<=> cC44(iV16455) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( sQ21_spl
| ~ cC44(iV16455) ),
inference(component_clause,[status(thm)],[f1337]) ).
fof(f1340,definition,
( sQ22_spl
<=> cC42(iV16455) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1342,plain,
( sQ22_spl
| ~ cC42(iV16455) ),
inference(component_clause,[status(thm)],[f1340]) ).
fof(f1343,definition,
( sQ23_spl
<=> cowlThing(iV16455) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1345,plain,
( sQ23_spl
| ~ cowlThing(iV16455) ),
inference(component_clause,[status(thm)],[f1343]) ).
fof(f1346,definition,
( sQ24_spl
<=> cC38(iV16457) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f1349,definition,
( sQ25_spl
<=> cowlThing(iV16457) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1351,plain,
( sQ25_spl
| ~ cowlThing(iV16457) ),
inference(component_clause,[status(thm)],[f1349]) ).
fof(f1352,definition,
( sQ26_spl
<=> cC50(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1354,plain,
( sQ26_spl
| ~ cC50(iV16459) ),
inference(component_clause,[status(thm)],[f1352]) ).
fof(f1355,definition,
( sQ27_spl
<=> cC88(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1358,definition,
( sQ28_spl
<=> cC34(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
( sQ28_spl
| ~ cC34(iV16459) ),
inference(component_clause,[status(thm)],[f1358]) ).
fof(f1361,definition,
( sQ29_spl
<=> cC68(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1363,plain,
( sQ29_spl
| ~ cC68(iV16459) ),
inference(component_clause,[status(thm)],[f1361]) ).
fof(f1364,definition,
( sQ30_spl
<=> cowlThing(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1366,plain,
( sQ30_spl
| ~ cowlThing(iV16459) ),
inference(component_clause,[status(thm)],[f1364]) ).
fof(f1367,definition,
( sQ31_spl
<=> cC38(iV16460) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1369,plain,
( sQ31_spl
| ~ cC38(iV16460) ),
inference(component_clause,[status(thm)],[f1367]) ).
fof(f1370,definition,
( sQ32_spl
<=> cowlThing(iV16460) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( sQ32_spl
| ~ cowlThing(iV16460) ),
inference(component_clause,[status(thm)],[f1370]) ).
fof(f1373,definition,
( sQ33_spl
<=> cC42(iV16461) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1375,plain,
( sQ33_spl
| ~ cC42(iV16461) ),
inference(component_clause,[status(thm)],[f1373]) ).
fof(f1376,definition,
( sQ34_spl
<=> cC56(iV16461) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1378,plain,
( sQ34_spl
| ~ cC56(iV16461) ),
inference(component_clause,[status(thm)],[f1376]) ).
fof(f1379,definition,
( sQ35_spl
<=> cC44(iV16461) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
( sQ35_spl
| ~ cC44(iV16461) ),
inference(component_clause,[status(thm)],[f1379]) ).
fof(f1382,definition,
( sQ36_spl
<=> cowlThing(iV16461) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( sQ36_spl
| ~ cowlThing(iV16461) ),
inference(component_clause,[status(thm)],[f1382]) ).
fof(f1385,definition,
( sQ37_spl
<=> cC38(iV16462) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1387,plain,
( sQ37_spl
| ~ cC38(iV16462) ),
inference(component_clause,[status(thm)],[f1385]) ).
fof(f1388,definition,
( sQ38_spl
<=> cowlThing(iV16462) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1390,plain,
( sQ38_spl
| ~ cowlThing(iV16462) ),
inference(component_clause,[status(thm)],[f1388]) ).
fof(f1391,definition,
( sQ39_spl
<=> cC76(iV16463) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( sQ39_spl
| ~ cC76(iV16463) ),
inference(component_clause,[status(thm)],[f1391]) ).
fof(f1394,definition,
( sQ40_spl
<=> cC62(iV16463) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1396,plain,
( sQ40_spl
| ~ cC62(iV16463) ),
inference(component_clause,[status(thm)],[f1394]) ).
fof(f1397,definition,
( sQ41_spl
<=> cowlThing(iV16463) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1399,plain,
( sQ41_spl
| ~ cowlThing(iV16463) ),
inference(component_clause,[status(thm)],[f1397]) ).
fof(f1400,definition,
( sQ42_spl
<=> cC60(iV16463) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( sQ42_spl
| ~ cC60(iV16463) ),
inference(component_clause,[status(thm)],[f1400]) ).
fof(f1403,definition,
( sQ43_spl
<=> cC56(iV16464) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1405,plain,
( sQ43_spl
| ~ cC56(iV16464) ),
inference(component_clause,[status(thm)],[f1403]) ).
fof(f1406,definition,
( sQ44_spl
<=> cC42(iV16464) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1408,plain,
( sQ44_spl
| ~ cC42(iV16464) ),
inference(component_clause,[status(thm)],[f1406]) ).
fof(f1409,definition,
( sQ45_spl
<=> cC44(iV16464) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1411,plain,
( sQ45_spl
| ~ cC44(iV16464) ),
inference(component_clause,[status(thm)],[f1409]) ).
fof(f1412,definition,
( sQ46_spl
<=> cowlThing(iV16464) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1414,plain,
( sQ46_spl
| ~ cowlThing(iV16464) ),
inference(component_clause,[status(thm)],[f1412]) ).
fof(f1415,definition,
( sQ47_spl
<=> cC38(iV16465) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1417,plain,
( sQ47_spl
| ~ cC38(iV16465) ),
inference(component_clause,[status(thm)],[f1415]) ).
fof(f1418,definition,
( sQ48_spl
<=> cowlThing(iV16465) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1420,plain,
( sQ48_spl
| ~ cowlThing(iV16465) ),
inference(component_clause,[status(thm)],[f1418]) ).
fof(f1421,plain,
( ~ sQ48_spl
| ~ sQ47_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ 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)],[f1272,f1274,f1277,f1280,f1283,f1286,f1289,f1292,f1295,f1298,f1301,f1304,f1307,f1310,f1313,f1316,f1319,f1322,f1325,f1328,f1331,f1334,f1337,f1340,f1343,f1346,f1349,f1352,f1355,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391,f1394,f1397,f1400,f1403,f1406,f1409,f1412,f1415,f1418]) ).
fof(f1422,plain,
( ~ sQ48_spl
| ~ sQ47_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ 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)],[f1273,f1274,f1277,f1280,f1283,f1286,f1289,f1292,f1295,f1298,f1301,f1304,f1307,f1310,f1313,f1316,f1319,f1322,f1325,f1328,f1331,f1334,f1337,f1340,f1343,f1346,f1349,f1352,f1355,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391,f1394,f1397,f1400,f1403,f1406,f1409,f1412,f1415,f1418]) ).
fof(f1423,plain,
( sQ48_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1420,f290]) ).
fof(f1424,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f1423]) ).
fof(f1427,plain,
( ~ cC102xcomp(iV16440)
| cC104(iV16439) ),
inference(resolution,[status(thm)],[f1092,f345]) ).
fof(f1428,definition,
( sQ49_spl
<=> cC102xcomp(iV16440) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1430,plain,
( sQ49_spl
| ~ cC102xcomp(iV16440) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,plain,
( ~ sQ49_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1427,f1292,f1428]) ).
fof(f1440,plain,
cC98(iV16440),
inference(resolution,[status(thm)],[f1088,f1092]) ).
fof(f1444,plain,
cC82(iV16440),
inference(resolution,[status(thm)],[f1440,f1074]) ).
fof(f1445,plain,
cC80(iV16440),
inference(resolution,[status(thm)],[f1444,f947]) ).
fof(f1446,plain,
cC76(iV16463),
inference(resolution,[status(thm)],[f1100,f1103]) ).
fof(f1447,plain,
cC62(iV16463),
inference(resolution,[status(thm)],[f1446,f903]) ).
fof(f1448,plain,
cC60(iV16463),
inference(resolution,[status(thm)],[f1447,f793]) ).
fof(f1492,plain,
cC56(iV16461),
inference(resolution,[status(thm)],[f1128,f1133]) ).
fof(f1493,plain,
cC38(iV16460),
inference(resolution,[status(thm)],[f1142,f1148]) ).
fof(f1496,plain,
cC44(iV16461),
inference(resolution,[status(thm)],[f1492,f739]) ).
fof(f1497,plain,
cC42(iV16461),
inference(resolution,[status(thm)],[f1496,f652]) ).
fof(f1498,plain,
! [X0] :
( ~ rR1(X0,iV16460)
| cC42(X0) ),
inference(resolution,[status(thm)],[f1188,f648]) ).
fof(f1499,plain,
! [X0] :
( ~ rR1(X0,iV16461)
| cC60(X0) ),
inference(resolution,[status(thm)],[f1202,f790]) ).
fof(f1502,plain,
cC38(iV16462),
inference(resolution,[status(thm)],[f1208,f1210]) ).
fof(f1503,plain,
cC56(iV16464),
inference(resolution,[status(thm)],[f1235,f1237]) ).
fof(f1504,plain,
cC44(iV16464),
inference(resolution,[status(thm)],[f1503,f739]) ).
fof(f1505,plain,
cC42(iV16464),
inference(resolution,[status(thm)],[f1504,f652]) ).
fof(f1506,plain,
cC38(iV16465),
inference(resolution,[status(thm)],[f1240,f1252]) ).
fof(f1507,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1506,f1417]) ).
fof(f1508,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f1507]) ).
fof(f1509,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1414,f290]) ).
fof(f1510,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f1509]) ).
fof(f1511,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1411,f1504]) ).
fof(f1512,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1511]) ).
fof(f1513,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1408,f1505]) ).
fof(f1514,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f1513]) ).
fof(f1515,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1405,f1503]) ).
fof(f1516,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f1515]) ).
fof(f1517,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1402,f1448]) ).
fof(f1518,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f1517]) ).
fof(f1519,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1399,f290]) ).
fof(f1520,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1519]) ).
fof(f1521,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1396,f1447]) ).
fof(f1522,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f1521]) ).
fof(f1523,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1393,f1446]) ).
fof(f1524,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1523]) ).
fof(f1525,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1390,f290]) ).
fof(f1526,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1525]) ).
fof(f1527,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1387,f1502]) ).
fof(f1528,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f1527]) ).
fof(f1529,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1384,f290]) ).
fof(f1530,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1529]) ).
fof(f1531,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1381,f1496]) ).
fof(f1532,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f1531]) ).
fof(f1533,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1378,f1492]) ).
fof(f1534,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1533]) ).
fof(f1535,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1375,f1497]) ).
fof(f1536,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1535]) ).
fof(f1537,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1372,f290]) ).
fof(f1538,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1537]) ).
fof(f1539,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1369,f1493]) ).
fof(f1540,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f1539]) ).
fof(f1541,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1366,f290]) ).
fof(f1542,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1541]) ).
fof(f1560,plain,
( ~ cC104(iV16439)
| cC106(iV16439) ),
inference(resolution,[status(thm)],[f350,f1090]) ).
fof(f1561,plain,
( ~ sQ6_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1560,f1295,f1292]) ).
fof(f1562,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1430,f1101]) ).
fof(f1563,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1562]) ).
fof(f1566,plain,
( ~ sQ7_spl
| ~ cC28(iV16439)
| cC108(iV16439) ),
inference(resolution,[status(thm)],[f1296,f355]) ).
fof(f1568,plain,
( ~ sQ7_spl
| ~ sQ8_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1566,f1289,f1298,f1295]) ).
fof(f1569,plain,
( sQ8_spl
| ~ cC108(iV16439) ),
inference(resolution,[status(thm)],[f1300,f353]) ).
fof(f1572,plain,
cC42(iV16455),
inference(resolution,[status(thm)],[f1498,f1148]) ).
fof(f1578,plain,
cC60(iV16453),
inference(resolution,[status(thm)],[f1499,f1133]) ).
fof(f1652,plain,
cC108(iV16439),
inference(resolution,[status(thm)],[f1084,f1091]) ).
fof(f1653,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1652,f1569]) ).
fof(f1654,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1653]) ).
fof(f1656,plain,
cC130(iV16439),
inference(resolution,[status(thm)],[f1085,f1091]) ).
fof(f1677,plain,
cC88(iV16449),
inference(resolution,[status(thm)],[f1120,f1118]) ).
fof(f1689,plain,
cC86xcomp(iV16449),
inference(resolution,[status(thm)],[f1677,f990]) ).
fof(f1690,plain,
cC84xcomp(iV16449),
inference(resolution,[status(thm)],[f1677,f989]) ).
fof(f1822,plain,
( ~ cC36xcomp(iV16457)
| cC38(iV16457) ),
inference(resolution,[status(thm)],[f603,f1154]) ).
fof(f1823,plain,
( ~ cC36xcomp(iV16448)
| cC38(iV16448) ),
inference(resolution,[status(thm)],[f603,f1107]) ).
fof(f1837,definition,
( sQ79_spl
<=> cC36xcomp(iV16457) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1839,plain,
( sQ79_spl
| ~ cC36xcomp(iV16457) ),
inference(component_clause,[status(thm)],[f1837]) ).
fof(f1840,plain,
( ~ sQ79_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1822,f1346,f1837]) ).
fof(f1841,definition,
( sQ80_spl
<=> cC36xcomp(iV16448) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1843,plain,
( sQ80_spl
| ~ cC36xcomp(iV16448) ),
inference(component_clause,[status(thm)],[f1841]) ).
fof(f1844,plain,
( ~ sQ80_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1823,f1316,f1841]) ).
fof(f1916,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1351,f290]) ).
fof(f1917,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f1916]) ).
fof(f1918,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1345,f290]) ).
fof(f1919,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1918]) ).
fof(f1920,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1342,f1572]) ).
fof(f1921,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1920]) ).
fof(f1922,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1333,f1578]) ).
fof(f1923,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1922]) ).
fof(f1924,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1330,f290]) ).
fof(f1925,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1924]) ).
fof(f1926,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1321,f290]) ).
fof(f1927,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1926]) ).
fof(f1928,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1315,f290]) ).
fof(f1929,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1928]) ).
fof(f1930,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1312,f1444]) ).
fof(f1931,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1930]) ).
fof(f1932,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1309,f1445]) ).
fof(f1933,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1932]) ).
fof(f1934,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1306,f1440]) ).
fof(f1935,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1934]) ).
fof(f1936,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1303,f290]) ).
fof(f1937,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1936]) ).
fof(f1938,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1288,f1656]) ).
fof(f1939,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1938]) ).
fof(f1940,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1278,f291]) ).
fof(f1941,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1940]) ).
fof(f1942,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1276,f290]) ).
fof(f1943,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1942]) ).
fof(f1944,plain,
( sQ28_spl
| ~ cC32xcomp(iV16459)
| ~ cC30xcomp(iV16459) ),
inference(resolution,[status(thm)],[f1360,f575]) ).
fof(f1945,definition,
( sQ87_spl
<=> cC30xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1947,plain,
( sQ87_spl
| ~ cC30xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f1945]) ).
fof(f1948,definition,
( sQ88_spl
<=> cC32xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1950,plain,
( sQ88_spl
| ~ cC32xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f1948]) ).
fof(f1951,plain,
( sQ28_spl
| ~ sQ88_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f1944,f1945,f1948,f1358]) ).
fof(f1952,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1950,f1175]) ).
fof(f1953,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f1952]) ).
fof(f1954,plain,
( sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1947,f1168]) ).
fof(f1955,plain,
sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1954]) ).
fof(f1956,plain,
( sQ21_spl
| ~ cC42(iV16455)
| ~ cC40xcomp(iV16455) ),
inference(resolution,[status(thm)],[f1339,f653]) ).
fof(f1957,definition,
( sQ89_spl
<=> cC40xcomp(iV16455) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1959,plain,
( sQ89_spl
| ~ cC40xcomp(iV16455) ),
inference(component_clause,[status(thm)],[f1957]) ).
fof(f1960,plain,
( sQ21_spl
| ~ sQ22_spl
| ~ sQ89_spl ),
inference(split_clause,[status(thm)],[f1956,f1957,f1340,f1337]) ).
fof(f1961,plain,
( sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1959,f1137]) ).
fof(f1962,plain,
sQ89_spl,
inference(contradiction_clause,[status(thm)],[f1961]) ).
fof(f1977,plain,
( sQ26_spl
| ~ cC48xcomp(iV16459)
| ~ cC46xcomp(iV16459) ),
inference(resolution,[status(thm)],[f690,f1354]) ).
fof(f1980,definition,
( sQ90_spl
<=> cC46xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1982,plain,
( sQ90_spl
| ~ cC46xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f1980]) ).
fof(f1983,definition,
( sQ91_spl
<=> cC48xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1985,plain,
( sQ91_spl
| ~ cC48xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f1983]) ).
fof(f1986,plain,
( sQ26_spl
| ~ sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f1977,f1980,f1983,f1352]) ).
fof(f1987,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1985,f1176]) ).
fof(f1988,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f1987]) ).
fof(f1989,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1982,f1171]) ).
fof(f1990,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f1989]) ).
fof(f2029,plain,
( sQ20_spl
| ~ cC44(iV16455)
| ~ cC54xcomp(iV16455) ),
inference(resolution,[status(thm)],[f740,f1336]) ).
fof(f2032,definition,
( sQ96_spl
<=> cC54xcomp(iV16455) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f2034,plain,
( sQ96_spl
| ~ cC54xcomp(iV16455) ),
inference(component_clause,[status(thm)],[f2032]) ).
fof(f2035,plain,
( sQ20_spl
| ~ sQ21_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f2029,f2032,f1337,f1334]) ).
fof(f2036,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2034,f1144]) ).
fof(f2037,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f2036]) ).
fof(f2071,plain,
( sQ17_spl
| ~ cC58xcomp(iV16453)
| ~ cC60(iV16453) ),
inference(resolution,[status(thm)],[f795,f1327]) ).
fof(f2074,definition,
( sQ98_spl
<=> cC58xcomp(iV16453) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2076,plain,
( sQ98_spl
| ~ cC58xcomp(iV16453) ),
inference(component_clause,[status(thm)],[f2074]) ).
fof(f2077,plain,
( sQ17_spl
| ~ sQ98_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f2071,f1331,f2074,f1325]) ).
fof(f2078,plain,
( sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f1132]) ).
fof(f2079,plain,
sQ98_spl,
inference(contradiction_clause,[status(thm)],[f2078]) ).
fof(f2129,plain,
( sQ29_spl
| ~ cC66xcomp(iV16459)
| ~ cC64xcomp(iV16459) ),
inference(resolution,[status(thm)],[f837,f1363]) ).
fof(f2132,definition,
( sQ100_spl
<=> cC64xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2134,plain,
( sQ100_spl
| ~ cC64xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f2132]) ).
fof(f2135,definition,
( sQ101_spl
<=> cC66xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2137,plain,
( sQ101_spl
| ~ cC66xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f2135]) ).
fof(f2138,plain,
( sQ29_spl
| ~ sQ101_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f2129,f2132,f2135,f1361]) ).
fof(f2139,plain,
( sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2137,f1180]) ).
fof(f2140,plain,
sQ101_spl,
inference(contradiction_clause,[status(thm)],[f2139]) ).
fof(f2141,plain,
( sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2134,f1172]) ).
fof(f2142,plain,
sQ100_spl,
inference(contradiction_clause,[status(thm)],[f2141]) ).
fof(f2240,plain,
( ~ cC62(iV16453)
| cC76(iV16453) ),
inference(resolution,[status(thm)],[f904,f1122]) ).
fof(f2243,plain,
( ~ sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f2240,f1322,f1325]) ).
fof(f2858,plain,
( ~ cC84xcomp(iV16449)
| cC88(iV16449) ),
inference(resolution,[status(thm)],[f991,f1689]) ).
fof(f2859,plain,
( ~ cC84xcomp(iV16459)
| cC88(iV16459) ),
inference(resolution,[status(thm)],[f991,f1174]) ).
fof(f2860,definition,
( sQ223_spl
<=> cC88(iV16449) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2863,definition,
( sQ224_spl
<=> cC84xcomp(iV16449) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f2865,plain,
( sQ224_spl
| ~ cC84xcomp(iV16449) ),
inference(component_clause,[status(thm)],[f2863]) ).
fof(f2866,plain,
( ~ sQ224_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f2858,f2860,f2863]) ).
fof(f2867,definition,
( sQ225_spl
<=> cC84xcomp(iV16459) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f2869,plain,
( sQ225_spl
| ~ cC84xcomp(iV16459) ),
inference(component_clause,[status(thm)],[f2867]) ).
fof(f2870,plain,
( ~ sQ225_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f2859,f1355,f2867]) ).
fof(f2871,plain,
( sQ225_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2869,f1169]) ).
fof(f2872,plain,
sQ225_spl,
inference(contradiction_clause,[status(thm)],[f2871]) ).
fof(f2873,plain,
( sQ224_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2865,f1690]) ).
fof(f2874,plain,
sQ224_spl,
inference(contradiction_clause,[status(thm)],[f2873]) ).
fof(f2879,plain,
( ~ sQ3_spl
| ~ xsd_string(sK116_skl) ),
inference(resolution,[status(thm)],[f1284,f294]) ).
fof(f2880,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2879,f1281]) ).
fof(f2881,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f2880]) ).
fof(f2902,plain,
( sQ3_spl
| xsd_string(sK116_skl) ),
inference(resolution,[status(thm)],[f1285,f295]) ).
fof(f2903,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2902,f1280,f1283]) ).
fof(f2904,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1843,f1115]) ).
fof(f2905,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f2904]) ).
fof(f2906,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1839,f1159]) ).
fof(f2907,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f2906]) ).
fof(f2908,plain,
$false,
inference(sat_refutation,[status(thm)],[f1421,f1422,f1424,f1431,f1508,f1510,f1512,f1514,f1516,f1518,f1520,f1522,f1524,f1526,f1528,f1530,f1532,f1534,f1536,f1538,f1540,f1542,f1561,f1563,f1568,f1654,f1840,f1844,f1917,f1919,f1921,f1923,f1925,f1927,f1929,f1931,f1933,f1935,f1937,f1939,f1941,f1943,f1951,f1953,f1955,f1960,f1962,f1986,f1988,f1990,f2035,f2037,f2077,f2079,f2138,f2140,f2142,f2243,f2866,f2870,f2872,f2874,f2881,f2903,f2905,f2907]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n005.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:55:03 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.44 % Elapsed time: 0.060540 seconds
% 0.13/0.44 % CPU time: 0.209990 seconds
% 0.13/0.44 % Total memory used: 37.870 MB
% 0.13/0.44 % Net memory used: 37.764 MB
%------------------------------------------------------------------------------