%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS153+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 : n008.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.10s 0.47s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 55
% Syntax : Number of formulae : 274 ( 75 unt; 0 def)
% Number of atoms : 2897 ( 0 equ)
% Maximal formula atoms : 51 ( 10 avg)
% Number of connectives : 5131 (2508 ~;2406 |; 192 &)
% ( 20 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 50 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-1 aty)
% Number of variables : 157 ( 141 !; 16 ?)
% 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(f4,axiom,
! [X] :
( cC100(X)
<=> ? [Y] :
( ~ cC98(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] :
( cC106(X)
<=> ( cC104(X)
& ~ cC100(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X] :
( cC34(X)
<=> ( ~ cC30(X)
& ~ cC32(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& ~ cC36(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& ~ cC40(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X] :
( cC50(X)
<=> ( ~ cC48(X)
& ~ cC46(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& cC44(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] :
( cC62(X)
<=> ( ~ cC58(X)
& cC60(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC66(X)
& ~ cC64(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& ~ cC74(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& ~ cC78(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] :
( cC88(X)
<=> ( ~ cC86(X)
& ~ cC84(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& ~ cC96(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
~ cC100(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X] :
( rR1(iV16440,X)
=> cC76(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
~ cC36(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
~ cC58(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,axiom,
~ cC74(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [X] :
( rR1(iV16453,X)
=> cC56(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
~ cC40(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
~ cC54(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
~ cC36(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,axiom,
~ cC48(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
~ cC30(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
~ cC86(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,axiom,
~ cC46(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
~ cC66(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
~ cC84(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
~ cC64(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,axiom,
~ cC32(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
~ cC36(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
cTOP(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,axiom,
~ cC8(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
~ cC12(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,axiom,
~ cC36(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,axiom,
cTOP(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [X] :
( rR1(iV16463,X)
=> cC56(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,axiom,
~ cC36(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,axiom,
cTOP(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,conjecture,
( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,negated_conjecture,
~ ( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f201]) ).
fof(f203,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f204,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f205,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f206,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f207,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f208,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f209,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f215,plain,
! [X] :
( ( ! [Y] :
( cC98(Y)
| ~ rR1(X,Y) )
| cC100(X) )
& ( ? [Y] :
( ~ cC98(Y)
& rR1(X,Y) )
| ~ cC100(X) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f216,plain,
( ! [X] :
( ! [Y] :
( cC98(Y)
| ~ rR1(X,Y) )
| cC100(X) )
& ! [X] :
( ? [Y] :
( ~ cC98(Y)
& rR1(X,Y) )
| ~ cC100(X) ) ),
inference(miniscoping,[status(thm)],[f215]) ).
fof(f217,plain,
( ! [X] :
( ! [Y] :
( cC98(Y)
| ~ rR1(X,Y) )
| cC100(X) )
& ! [X] :
( ( ~ cC98(sK0_skl(X))
& rR1(X,sK0_skl(X)) )
| ~ cC100(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f216]) ).
fof(f220,plain,
! [X0,X1] :
( cC98(X1)
| ~ rR1(X0,X1)
| cC100(X0) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f227,plain,
! [X] :
( ( ~ cC104(X)
| cC100(X)
| cC106(X) )
& ( ( cC104(X)
& ~ cC100(X) )
| ~ cC106(X) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f228,plain,
( ! [X] :
( ~ cC104(X)
| cC100(X)
| cC106(X) )
& ! [X] :
( ( cC104(X)
& ~ cC100(X) )
| ~ cC106(X) ) ),
inference(miniscoping,[status(thm)],[f227]) ).
fof(f230,plain,
! [X0] :
( cC104(X0)
| ~ cC106(X0) ),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f232,plain,
! [X] :
( ( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f233,plain,
( ! [X] :
( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ! [X] :
( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(miniscoping,[status(thm)],[f232]) ).
fof(f234,plain,
! [X0] :
( cC28(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f235,plain,
! [X0] :
( cC106(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f337,plain,
! [X] :
( ( cC30(X)
| cC32(X)
| cC34(X) )
& ( ( ~ cC30(X)
& ~ cC32(X) )
| ~ cC34(X) ) ),
inference(NNF_transformation,[status(thm)],[f26]) ).
fof(f338,plain,
( ! [X] :
( cC30(X)
| cC32(X)
| cC34(X) )
& ! [X] :
( ( ~ cC30(X)
& ~ cC32(X) )
| ~ cC34(X) ) ),
inference(miniscoping,[status(thm)],[f337]) ).
fof(f341,plain,
! [X0] :
( cC30(X0)
| cC32(X0)
| cC34(X0) ),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f348,plain,
! [X] :
( ( ~ cTOP(X)
| cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& ~ cC36(X) )
| ~ cC38(X) ) ),
inference(NNF_transformation,[status(thm)],[f28]) ).
fof(f349,plain,
( ! [X] :
( ~ cTOP(X)
| cC36(X)
| cC38(X) )
& ! [X] :
( ( cTOP(X)
& ~ cC36(X) )
| ~ cC38(X) ) ),
inference(miniscoping,[status(thm)],[f348]) ).
fof(f352,plain,
! [X0] :
( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f359,plain,
! [X] :
( ( ! [Y] :
( cC8(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ( ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(NNF_transformation,[status(thm)],[f30]) ).
fof(f360,plain,
( ! [X] :
( ! [Y] :
( cC8(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ! [X] :
( ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(miniscoping,[status(thm)],[f359]) ).
fof(f361,plain,
( ! [X] :
( ! [Y] :
( cC8(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ! [X] :
( ( ~ cC8(sK14_skl(X))
& rR1(X,sK14_skl(X)) )
| ~ cC42(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(Y,sK14_skl(X))],[f360]) ).
fof(f364,plain,
! [X0,X1] :
( cC8(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f365,plain,
! [X] :
( ( ~ cC42(X)
| cC40(X)
| cC44(X) )
& ( ( cC42(X)
& ~ cC40(X) )
| ~ cC44(X) ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f366,plain,
( ! [X] :
( ~ cC42(X)
| cC40(X)
| cC44(X) )
& ! [X] :
( ( cC42(X)
& ~ cC40(X) )
| ~ cC44(X) ) ),
inference(miniscoping,[status(thm)],[f365]) ).
fof(f368,plain,
! [X0] :
( cC42(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f369,plain,
! [X0] :
( ~ cC42(X0)
| cC40(X0)
| cC44(X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f380,plain,
! [X] :
( ( cC48(X)
| cC46(X)
| cC50(X) )
& ( ( ~ cC48(X)
& ~ cC46(X) )
| ~ cC50(X) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f381,plain,
( ! [X] :
( cC48(X)
| cC46(X)
| cC50(X) )
& ! [X] :
( ( ~ cC48(X)
& ~ cC46(X) )
| ~ cC50(X) ) ),
inference(miniscoping,[status(thm)],[f380]) ).
fof(f384,plain,
! [X0] :
( cC48(X0)
| cC46(X0)
| cC50(X0) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f397,plain,
! [X] :
( ( cC54(X)
| ~ cC44(X)
| cC56(X) )
& ( ( ~ cC54(X)
& cC44(X) )
| ~ cC56(X) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f398,plain,
( ! [X] :
( cC54(X)
| ~ cC44(X)
| cC56(X) )
& ! [X] :
( ( ~ cC54(X)
& cC44(X) )
| ~ cC56(X) ) ),
inference(miniscoping,[status(thm)],[f397]) ).
fof(f399,plain,
! [X0] :
( cC44(X0)
| ~ cC56(X0) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f401,plain,
! [X0] :
( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f413,plain,
! [X] :
( ( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f414,plain,
( ! [X] :
( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ! [X] :
( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(miniscoping,[status(thm)],[f413]) ).
fof(f415,plain,
( ! [X] :
( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ! [X] :
( ( ~ cC12(sK18_skl(X))
& rR1(X,sK18_skl(X)) )
| ~ cC60(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(Y,sK18_skl(X))],[f414]) ).
fof(f418,plain,
! [X0,X1] :
( cC12(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f419,plain,
! [X] :
( ( cC58(X)
| ~ cC60(X)
| cC62(X) )
& ( ( ~ cC58(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(NNF_transformation,[status(thm)],[f41]) ).
fof(f420,plain,
( ! [X] :
( cC58(X)
| ~ cC60(X)
| cC62(X) )
& ! [X] :
( ( ~ cC58(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(miniscoping,[status(thm)],[f419]) ).
fof(f421,plain,
! [X0] :
( cC60(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f423,plain,
! [X0] :
( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f434,plain,
! [X] :
( ( cC66(X)
| cC64(X)
| cC68(X) )
& ( ( ~ cC66(X)
& ~ cC64(X) )
| ~ cC68(X) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f435,plain,
( ! [X] :
( cC66(X)
| cC64(X)
| cC68(X) )
& ! [X] :
( ( ~ cC66(X)
& ~ cC64(X) )
| ~ cC68(X) ) ),
inference(miniscoping,[status(thm)],[f434]) ).
fof(f438,plain,
! [X0] :
( cC66(X0)
| cC64(X0)
| cC68(X0) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f457,plain,
! [X] :
( ( ~ cC62(X)
| cC74(X)
| cC76(X) )
& ( ( cC62(X)
& ~ cC74(X) )
| ~ cC76(X) ) ),
inference(NNF_transformation,[status(thm)],[f48]) ).
fof(f458,plain,
( ! [X] :
( ~ cC62(X)
| cC74(X)
| cC76(X) )
& ! [X] :
( ( cC62(X)
& ~ cC74(X) )
| ~ cC76(X) ) ),
inference(miniscoping,[status(thm)],[f457]) ).
fof(f460,plain,
! [X0] :
( cC62(X0)
| ~ cC76(X0) ),
inference(cnf_transformation,[status(thm)],[f458]) ).
fof(f461,plain,
! [X0] :
( ~ cC62(X0)
| cC74(X0)
| cC76(X0) ),
inference(cnf_transformation,[status(thm)],[f458]) ).
fof(f474,plain,
! [X] :
( ( ~ cC80(X)
| cC78(X)
| cC82(X) )
& ( ( cC80(X)
& ~ cC78(X) )
| ~ cC82(X) ) ),
inference(NNF_transformation,[status(thm)],[f51]) ).
fof(f475,plain,
( ! [X] :
( ~ cC80(X)
| cC78(X)
| cC82(X) )
& ! [X] :
( ( cC80(X)
& ~ cC78(X) )
| ~ cC82(X) ) ),
inference(miniscoping,[status(thm)],[f474]) ).
fof(f477,plain,
! [X0] :
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f489,plain,
! [X] :
( ( cC86(X)
| cC84(X)
| cC88(X) )
& ( ( ~ cC86(X)
& ~ cC84(X) )
| ~ cC88(X) ) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f490,plain,
( ! [X] :
( cC86(X)
| cC84(X)
| cC88(X) )
& ! [X] :
( ( ~ cC86(X)
& ~ cC84(X) )
| ~ cC88(X) ) ),
inference(miniscoping,[status(thm)],[f489]) ).
fof(f493,plain,
! [X0] :
( cC86(X0)
| cC84(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(thm)],[f490]) ).
fof(f518,plain,
! [X] :
( ( ~ cC82(X)
| cC96(X)
| cC98(X) )
& ( ( cC82(X)
& ~ cC96(X) )
| ~ cC98(X) ) ),
inference(NNF_transformation,[status(thm)],[f59]) ).
fof(f519,plain,
( ! [X] :
( ~ cC82(X)
| cC96(X)
| cC98(X) )
& ! [X] :
( ( cC82(X)
& ~ cC96(X) )
| ~ cC98(X) ) ),
inference(miniscoping,[status(thm)],[f518]) ).
fof(f521,plain,
! [X0] :
( cC82(X0)
| ~ cC98(X0) ),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f523,plain,
! [X] :
( ( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(NNF_transformation,[status(thm)],[f60]) ).
fof(f524,plain,
( ! [X] :
( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ! [X] :
( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(miniscoping,[status(thm)],[f523]) ).
fof(f525,plain,
! [X0] :
( cC108(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f524]) ).
fof(f526,plain,
! [X0] :
( cC130(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f524]) ).
fof(f528,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f529,plain,
! [X0] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[status(thm)],[f528]) ).
fof(f530,plain,
cTEST(iV16439),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f531,plain,
~ cC100(iV16439),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f533,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f536,plain,
! [X] :
( cC76(X)
| ~ rR1(iV16440,X) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f537,plain,
! [X0] :
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(cnf_transformation,[status(thm)],[f536]) ).
fof(f544,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f547,plain,
~ cC36(iV16448),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f552,plain,
cTOP(iV16448),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f568,plain,
~ cC58(iV16453),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f569,plain,
~ cC74(iV16453),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f570,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16453,X) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f571,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(cnf_transformation,[status(thm)],[f570]) ).
fof(f574,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f576,plain,
~ cC40(iV16455),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f584,plain,
~ cC54(iV16455),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f589,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f590,plain,
~ cC36(iV16457),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f598,plain,
cTOP(iV16457),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f606,plain,
~ cC48(iV16459),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f607,plain,
~ cC30(iV16459),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f609,plain,
~ cC86(iV16459),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f610,plain,
~ cC46(iV16459),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f613,plain,
~ cC66(iV16459),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f618,plain,
~ cC84(iV16459),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f619,plain,
~ cC64(iV16459),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f621,plain,
~ cC32(iV16459),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f623,plain,
~ cC36(iV16460),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f627,plain,
cTOP(iV16460),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f628,plain,
~ cC8(iV16460),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f643,plain,
~ cC12(iV16461),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f656,plain,
~ cC36(iV16462),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f657,plain,
cTOP(iV16462),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f670,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16463,X) ),
inference(pre_NNF_transformation,[status(thm)],[f172]) ).
fof(f671,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(cnf_transformation,[status(thm)],[f670]) ).
fof(f678,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f703,plain,
~ cC36(iV16465),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f704,plain,
cTOP(iV16465),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f709,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f202]) ).
fof(f710,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f709]) ).
fof(f711,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f710]) ).
fof(f712,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ( ( xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl) )
& ( ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl) ) )
| cowlNothing(sK29_skl)
| ~ cowlThing(sK28_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl,sK30_skl]),skolemize(X,sK28_skl),skolemize(X,sK29_skl),skolemize(X,sK30_skl)],[f711]) ).
fof(f713,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl)
| cowlNothing(sK29_skl)
| ~ cowlThing(sK28_skl) ),
inference(cnf_transformation,[status(thm)],[f712]) ).
fof(f714,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl)
| cowlNothing(sK29_skl)
| ~ cowlThing(sK28_skl) ),
inference(cnf_transformation,[status(thm)],[f712]) ).
fof(f715,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl)
| cowlNothing(sK29_skl)
| ~ cowlThing(sK28_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f714,f204]) ).
fof(f716,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl)
| cowlNothing(sK29_skl)
| ~ cowlThing(sK28_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f713,f204]) ).
fof(f717,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl)
| cowlNothing(sK29_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f715,f204]) ).
fof(f718,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl)
| cowlNothing(sK29_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f204]) ).
fof(f719,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl)
| cowlNothing(sK29_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f204]) ).
fof(f720,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl)
| cowlNothing(sK29_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f718,f204]) ).
fof(f721,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f720,f205]) ).
fof(f722,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f719,f205]) ).
fof(f723,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl)
| xsd_string(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f721,f204]) ).
fof(f724,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl)
| ~ xsd_string(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f722,f204]) ).
fof(f727,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f208]) ).
fof(f728,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(resolution,[status(thm)],[f727,f204]) ).
fof(f729,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f204]) ).
fof(f730,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f729,f204]) ).
fof(f731,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(resolution,[status(thm)],[f730,f204]) ).
fof(f732,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f204]) ).
fof(f733,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f204]) ).
fof(f734,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(resolution,[status(thm)],[f733,f204]) ).
fof(f735,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f734,f204]) ).
fof(f736,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f735,f204]) ).
fof(f738,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f209]) ).
fof(f741,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f738,f230]) ).
fof(f742,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f736,f230]) ).
fof(f743,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f741,f204]) ).
fof(f744,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f742,f204]) ).
fof(f747,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK30_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f744,f234]) ).
fof(f748,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f743,f747]) ).
fof(f749,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439) ),
inference(resolution,[status(thm)],[f748,f204]) ).
fof(f750,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f749,f234]) ).
fof(f751,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f204]) ).
fof(f752,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(resolution,[status(thm)],[f751,f204]) ).
fof(f753,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f752,f204]) ).
fof(f754,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f753,f204]) ).
fof(f755,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(resolution,[status(thm)],[f754,f204]) ).
fof(f756,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC106(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f755,f204]) ).
fof(f767,plain,
! [X0] :
( ~ rR1(X0,iV16460)
| cC42(X0) ),
inference(resolution,[status(thm)],[f364,f628]) ).
fof(f773,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f756,f235]) ).
fof(f774,plain,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(resolution,[status(thm)],[f773,f204]) ).
fof(f775,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f774,f368]) ).
fof(f776,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f775,f368]) ).
fof(f777,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(resolution,[status(thm)],[f776,f204]) ).
fof(f778,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f368]) ).
fof(f780,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[f778,f399]) ).
fof(f781,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f780,f399]) ).
fof(f792,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f477]) ).
fof(f793,plain,
! [X0] :
( ~ rR1(X0,iV16440)
| cC100(X0)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(resolution,[status(thm)],[f792,f220]) ).
fof(f794,plain,
! [X0] :
( ~ rR1(X0,iV16440)
| cC100(X0)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f793,f460]) ).
fof(f795,plain,
! [X0] :
( ~ rR1(X0,iV16440)
| cC100(X0)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f794,f421]) ).
fof(f796,plain,
( ~ rR1(iV16439,iV16440)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(resolution,[status(thm)],[f795,f531]) ).
fof(f798,plain,
( ~ rR1(iV16439,iV16440)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f399]) ).
fof(f800,plain,
( ~ rR1(iV16439,iV16440)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f798,f460]) ).
fof(f801,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC108(iV16439)
| ~ cC130(iV16439) ),
inference(resolution,[status(thm)],[f800,f533]) ).
fof(f810,plain,
! [X0] :
( ~ rR1(X0,iV16461)
| cC60(X0) ),
inference(resolution,[status(thm)],[f643,f418]) ).
fof(f932,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC130(iV16439)
| ~ cTEST(iV16439) ),
inference(resolution,[status(thm)],[f525,f801]) ).
fof(f933,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC130(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[f932,f530]) ).
fof(f963,plain,
( ~ cTEST(iV16439)
| ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f933,f526]) ).
fof(f965,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f963,f530]) ).
fof(f1066,plain,
( cC32(iV16459)
| cC34(iV16459) ),
inference(resolution,[status(thm)],[f341,f607]) ).
fof(f1071,plain,
cC34(iV16459),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f621]) ).
fof(f1077,plain,
( ~ cC38(iV16465)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[f965,f1071]) ).
fof(f1116,plain,
( ~ cTOP(iV16465)
| cC38(iV16465) ),
inference(resolution,[status(thm)],[f352,f703]) ).
fof(f1117,plain,
( ~ cTOP(iV16462)
| cC38(iV16462) ),
inference(resolution,[status(thm)],[f352,f656]) ).
fof(f1118,plain,
( ~ cTOP(iV16460)
| cC38(iV16460) ),
inference(resolution,[status(thm)],[f352,f623]) ).
fof(f1119,plain,
( ~ cTOP(iV16457)
| cC38(iV16457) ),
inference(resolution,[status(thm)],[f352,f590]) ).
fof(f1120,plain,
( ~ cTOP(iV16448)
| cC38(iV16448) ),
inference(resolution,[status(thm)],[f352,f547]) ).
fof(f1122,plain,
cC38(iV16465),
inference(forward_subsumption_resolution,[status(thm)],[f1116,f704]) ).
fof(f1123,plain,
cC38(iV16462),
inference(forward_subsumption_resolution,[status(thm)],[f1117,f657]) ).
fof(f1124,plain,
cC38(iV16460),
inference(forward_subsumption_resolution,[status(thm)],[f1118,f627]) ).
fof(f1125,plain,
cC38(iV16457),
inference(forward_subsumption_resolution,[status(thm)],[f1119,f598]) ).
fof(f1126,plain,
cC38(iV16448),
inference(forward_subsumption_resolution,[status(thm)],[f1120,f552]) ).
fof(f1138,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[f1077,f1122]) ).
fof(f1278,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC38(iV16460)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1138,f1126]) ).
fof(f1279,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1278,f1124]) ).
fof(f1284,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1279,f1125]) ).
fof(f1413,plain,
( ~ cC42(iV16455)
| cC44(iV16455) ),
inference(resolution,[status(thm)],[f369,f576]) ).
fof(f1431,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1284,f1123]) ).
fof(f1480,plain,
( cC48(iV16459)
| cC50(iV16459) ),
inference(resolution,[status(thm)],[f384,f610]) ).
fof(f1484,plain,
cC50(iV16459),
inference(forward_subsumption_resolution,[status(thm)],[f1480,f606]) ).
fof(f1543,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC56(iV16461)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[f1431,f1484]) ).
fof(f1566,plain,
( ~ cC44(iV16455)
| cC56(iV16455) ),
inference(resolution,[status(thm)],[f401,f584]) ).
fof(f1588,plain,
( ~ rR1(iV16453,iV16461)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1543,f571]) ).
fof(f1589,plain,
( ~ rR1(iV16453,iV16461)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC56(iV16455)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1588,f810]) ).
fof(f1590,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC56(iV16455)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1589,f574]) ).
fof(f1608,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC44(iV16455) ),
inference(resolution,[status(thm)],[f1566,f1590]) ).
fof(f1638,plain,
( ~ cC60(iV16453)
| cC62(iV16453) ),
inference(resolution,[status(thm)],[f423,f568]) ).
fof(f1666,plain,
( ~ cC42(iV16455)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1608,f1413]) ).
fof(f1673,plain,
( ~ rR1(iV16455,iV16460)
| ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1666,f767]) ).
fof(f1678,plain,
( ~ cC56(iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1673,f589]) ).
fof(f1681,plain,
( ~ rR1(iV16463,iV16464)
| ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1678,f671]) ).
fof(f1683,plain,
( ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1681,f678]) ).
fof(f1754,plain,
( cC66(iV16459)
| cC68(iV16459) ),
inference(resolution,[status(thm)],[f438,f619]) ).
fof(f1758,plain,
cC68(iV16459),
inference(forward_subsumption_resolution,[status(thm)],[f1754,f613]) ).
fof(f1821,plain,
( ~ cC76(iV16463)
| ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[f1683,f1758]) ).
fof(f1861,plain,
( ~ rR1(iV16440,iV16463)
| ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1821,f537]) ).
fof(f1862,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1861,f544]) ).
fof(f1865,plain,
( ~ cC62(iV16453)
| cC76(iV16453) ),
inference(resolution,[status(thm)],[f461,f569]) ).
fof(f1867,plain,
( ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC62(iV16453) ),
inference(resolution,[status(thm)],[f1865,f1862]) ).
fof(f1933,plain,
( cC86(iV16459)
| cC88(iV16459) ),
inference(resolution,[status(thm)],[f493,f618]) ).
fof(f1936,plain,
cC88(iV16459),
inference(forward_subsumption_resolution,[status(thm)],[f1933,f609]) ).
fof(f1937,plain,
( ~ cC60(iV16453)
| ~ cC88(iV16459)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1867,f1638]) ).
fof(f1944,plain,
( ~ rR1(iV16453,iV16461)
| ~ cC88(iV16459)
| ~ cC82(iV16440) ),
inference(resolution,[status(thm)],[f1937,f810]) ).
fof(f1948,plain,
( ~ cC88(iV16459)
| ~ cC82(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[f1944,f574]) ).
fof(f1950,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459) ),
inference(resolution,[status(thm)],[f1948,f521]) ).
fof(f1953,plain,
( ~ rR1(iV16439,iV16440)
| ~ cC88(iV16459) ),
inference(resolution,[status(thm)],[f1950,f529]) ).
fof(f1955,plain,
~ cC88(iV16459),
inference(forward_subsumption_resolution,[status(thm)],[f1953,f533]) ).
fof(f1967,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1936,f1955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS153+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 : n008.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:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.47 % Refutation found
% 0.10/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.49 % Elapsed time: 0.118934 seconds
% 0.10/0.49 % CPU time: 0.705722 seconds
% 0.10/0.49 % Total memory used: 38.232 MB
% 0.10/0.49 % Net memory used: 38.001 MB
%------------------------------------------------------------------------------