%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Sun Sep 27 07:45:17 AM UTC 2026
% Result : Theorem 42.29s 11.17s
% Output : CNFRefutation 42.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 52
% Syntax : Number of formulae : 256 ( 90 unt; 0 def)
% Number of atoms : 2800 ( 0 equ)
% Maximal formula atoms : 49 ( 10 avg)
% Number of connectives : 4955 (2411 ~;2407 |; 111 &)
% ( 19 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 50 ( 12 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 66 ( 2 sgn 29 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ).
fof(axiom_1,axiom,
! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) ) ).
fof(axiom_11,axiom,
! [X0] :
( cC106(X0)
<=> ( cC100xcomp(X0)
& cC104(X0) ) ) ).
fof(axiom_12,axiom,
! [X0] :
( cC108(X0)
<=> ( cC106(X0)
& cC28(X0) ) ) ).
fof(axiom_52,axiom,
! [X0] :
( cC34(X0)
<=> ( cC32xcomp(X0)
& cC30xcomp(X0) ) ) ).
fof(axiom_57,axiom,
! [X0] :
( cC38(X0)
<=> ( cC36xcomp(X0)
& cTOP(X0) ) ) ).
fof(axiom_65,axiom,
! [X0] :
( cC42(X0)
<=> ? [X1] :
( cC8xcomp(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_66,axiom,
! [X0] :
( cC44(X0)
<=> ( cC42(X0)
& cC40xcomp(X0) ) ) ).
fof(axiom_73,axiom,
! [X0] :
( cC50(X0)
<=> ( cC48xcomp(X0)
& cC46xcomp(X0) ) ) ).
fof(axiom_82,axiom,
! [X0] :
( cC56(X0)
<=> ( cC44(X0)
& cC54xcomp(X0) ) ) ).
fof(axiom_91,axiom,
! [X0] :
( cC60(X0)
<=> ? [X1] :
( cC12xcomp(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_92,axiom,
! [X0] :
( cC62(X0)
<=> ( cC58xcomp(X0)
& cC60(X0) ) ) ).
fof(axiom_100,axiom,
! [X0] :
( cC68(X0)
<=> ( cC66xcomp(X0)
& cC64xcomp(X0) ) ) ).
fof(axiom_112,axiom,
! [X0] :
( cC76(X0)
<=> ( cC62(X0)
& cC74xcomp(X0) ) ) ).
fof(axiom_120,axiom,
! [X0] :
( cC82(X0)
<=> ( cC78xcomp(X0)
& cC80(X0) ) ) ).
fof(axiom_128,axiom,
! [X0] :
( cC88(X0)
<=> ( cC86xcomp(X0)
& cC84xcomp(X0) ) ) ).
fof(axiom_143,axiom,
! [X0] :
( cC98(X0)
<=> ( cC82(X0)
& cC96xcomp(X0) ) ) ).
fof(axiom_145,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC130(X0)
& cC108(X0) ) ) ).
fof(axiom_146,axiom,
! [X0] :
( rR1(iV16439,X0)
=> cC98(X0) ) ).
fof(axiom_149,axiom,
cTEST(iV16439) ).
fof(axiom_150,axiom,
rR1(iV16439,iV16440) ).
fof(axiom_156,axiom,
! [X0] :
( rR1(iV16440,X0)
=> cC76(X0) ) ).
fof(axiom_159,axiom,
rR1(iV16440,iV16463) ).
fof(axiom_163,axiom,
cTOP(iV16448) ).
fof(axiom_168,axiom,
cC36xcomp(iV16448) ).
fof(axiom_174,axiom,
cC74xcomp(iV16453) ).
fof(axiom_178,axiom,
! [X0] :
( rR1(iV16453,X0)
=> cC56(X0) ) ).
fof(axiom_181,axiom,
cC58xcomp(iV16453) ).
fof(axiom_182,axiom,
rR1(iV16453,iV16461) ).
fof(axiom_185,axiom,
cC40xcomp(iV16455) ).
fof(axiom_188,axiom,
! [X0] :
( rR1(iV16455,X0)
=> cC38(X0) ) ).
fof(axiom_190,axiom,
cC54xcomp(iV16455) ).
fof(axiom_193,axiom,
rR1(iV16455,iV16460) ).
fof(axiom_197,axiom,
cTOP(iV16457) ).
fof(axiom_201,axiom,
cC36xcomp(iV16457) ).
fof(axiom_209,axiom,
cC30xcomp(iV16459) ).
fof(axiom_210,axiom,
cC84xcomp(iV16459) ).
fof(axiom_212,axiom,
cC46xcomp(iV16459) ).
fof(axiom_213,axiom,
cC64xcomp(iV16459) ).
fof(axiom_215,axiom,
cC86xcomp(iV16459) ).
fof(axiom_216,axiom,
cC32xcomp(iV16459) ).
fof(axiom_217,axiom,
cC48xcomp(iV16459) ).
fof(axiom_221,axiom,
cC66xcomp(iV16459) ).
fof(axiom_227,axiom,
cC8xcomp(iV16460) ).
fof(axiom_237,axiom,
cC12xcomp(iV16461) ).
fof(axiom_241,axiom,
! [X0] :
( rR1(iV16461,X0)
=> cC38(X0) ) ).
fof(axiom_243,axiom,
rR1(iV16461,iV16462) ).
fof(axiom_261,axiom,
! [X0] :
( rR1(iV16463,X0)
=> cC56(X0) ) ).
fof(axiom_263,axiom,
rR1(iV16463,iV16464) ).
fof(axiom_265,axiom,
! [X0] :
( rR1(iV16464,X0)
=> cC38(X0) ) ).
fof(axiom_274,axiom,
rR1(iV16464,iV16465) ).
fof(the_axiom,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)
& ! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ) ).
fof(negated_conjecture,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)
& ! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(negate_conjecture,[status(cth)],[the_axiom]) ).
cnf(c0,plain,
cowlThing(X0),
inference(clausification,[status(esa)],[axiom_0]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(clausification,[status(esa)],[axiom_0]) ).
cnf(c2,plain,
( ~ 'xsd$uinteger'(X0)
| ~ 'xsd$ustring'(X0) ),
inference(clausification,[status(esa)],[axiom_1]) ).
cnf(c3,plain,
( 'xsd$uinteger'(X0)
| 'xsd$ustring'(X0) ),
inference(clausification,[status(esa)],[axiom_1]) ).
cnf(c25,plain,
( cC104(X0)
| ~ cC106(X0) ),
inference(clausification,[status(esa)],[axiom_11]) ).
cnf(c28,plain,
( cC28(X0)
| ~ cC108(X0) ),
inference(clausification,[status(esa)],[axiom_12]) ).
cnf(c29,plain,
( cC106(X0)
| ~ cC108(X0) ),
inference(clausification,[status(esa)],[axiom_12]) ).
cnf(c129,plain,
( ~ cC32xcomp(X0)
| ~ cC30xcomp(X0)
| cC34(X0) ),
inference(clausification,[status(esa)],[axiom_52]) ).
cnf(c141,plain,
( ~ cC36xcomp(X0)
| ~ cTOP(X0)
| cC38(X0) ),
inference(clausification,[status(esa)],[axiom_57]) ).
cnf(c159,plain,
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(clausification,[status(esa)],[axiom_65]) ).
cnf(c161,plain,
( cC42(X0)
| ~ cC44(X0) ),
inference(clausification,[status(esa)],[axiom_66]) ).
cnf(c162,plain,
( ~ cC42(X0)
| ~ cC40xcomp(X0)
| cC44(X0) ),
inference(clausification,[status(esa)],[axiom_66]) ).
cnf(c179,plain,
( ~ cC48xcomp(X0)
| ~ cC46xcomp(X0)
| cC50(X0) ),
inference(clausification,[status(esa)],[axiom_73]) ).
cnf(c199,plain,
( cC44(X0)
| ~ cC56(X0) ),
inference(clausification,[status(esa)],[axiom_82]) ).
cnf(c200,plain,
( ~ cC44(X0)
| ~ cC54xcomp(X0)
| cC56(X0) ),
inference(clausification,[status(esa)],[axiom_82]) ).
cnf(c221,plain,
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(clausification,[status(esa)],[axiom_91]) ).
cnf(c222,plain,
( cC60(X0)
| ~ cC62(X0) ),
inference(clausification,[status(esa)],[axiom_92]) ).
cnf(c224,plain,
( ~ cC58xcomp(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(clausification,[status(esa)],[axiom_92]) ).
cnf(c243,plain,
( ~ cC66xcomp(X0)
| ~ cC64xcomp(X0)
| cC68(X0) ),
inference(clausification,[status(esa)],[axiom_100]) ).
cnf(c270,plain,
( cC62(X0)
| ~ cC76(X0) ),
inference(clausification,[status(esa)],[axiom_112]) ).
cnf(c271,plain,
( ~ cC62(X0)
| ~ cC74xcomp(X0)
| cC76(X0) ),
inference(clausification,[status(esa)],[axiom_112]) ).
cnf(c288,plain,
( cC80(X0)
| ~ cC82(X0) ),
inference(clausification,[status(esa)],[axiom_120]) ).
cnf(c309,plain,
( ~ cC86xcomp(X0)
| ~ cC84xcomp(X0)
| cC88(X0) ),
inference(clausification,[status(esa)],[axiom_128]) ).
cnf(c343,plain,
( cC82(X0)
| ~ cC98(X0) ),
inference(clausification,[status(esa)],[axiom_143]) ).
cnf(c347,plain,
( cC108(X0)
| ~ cTEST(X0) ),
inference(clausification,[status(esa)],[axiom_145]) ).
cnf(c348,plain,
( cC130(X0)
| ~ cTEST(X0) ),
inference(clausification,[status(esa)],[axiom_145]) ).
cnf(c350,plain,
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(clausification,[status(esa)],[axiom_146]) ).
cnf(c353,plain,
cTEST(iV16439),
inference(clausification,[status(esa)],[axiom_149]) ).
cnf(c354,plain,
rR1(iV16439,iV16440),
inference(clausification,[status(esa)],[axiom_150]) ).
cnf(c360,plain,
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(clausification,[status(esa)],[axiom_156]) ).
cnf(c363,plain,
rR1(iV16440,iV16463),
inference(clausification,[status(esa)],[axiom_159]) ).
cnf(c367,plain,
cTOP(iV16448),
inference(clausification,[status(esa)],[axiom_163]) ).
cnf(c372,plain,
cC36xcomp(iV16448),
inference(clausification,[status(esa)],[axiom_168]) ).
cnf(c378,plain,
cC74xcomp(iV16453),
inference(clausification,[status(esa)],[axiom_174]) ).
cnf(c382,plain,
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(clausification,[status(esa)],[axiom_178]) ).
cnf(c385,plain,
cC58xcomp(iV16453),
inference(clausification,[status(esa)],[axiom_181]) ).
cnf(c386,plain,
rR1(iV16453,iV16461),
inference(clausification,[status(esa)],[axiom_182]) ).
cnf(c389,plain,
cC40xcomp(iV16455),
inference(clausification,[status(esa)],[axiom_185]) ).
cnf(c392,plain,
( cC38(X0)
| ~ rR1(iV16455,X0) ),
inference(clausification,[status(esa)],[axiom_188]) ).
cnf(c394,plain,
cC54xcomp(iV16455),
inference(clausification,[status(esa)],[axiom_190]) ).
cnf(c397,plain,
rR1(iV16455,iV16460),
inference(clausification,[status(esa)],[axiom_193]) ).
cnf(c401,plain,
cTOP(iV16457),
inference(clausification,[status(esa)],[axiom_197]) ).
cnf(c405,plain,
cC36xcomp(iV16457),
inference(clausification,[status(esa)],[axiom_201]) ).
cnf(c413,plain,
cC30xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_209]) ).
cnf(c414,plain,
cC84xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_210]) ).
cnf(c416,plain,
cC46xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_212]) ).
cnf(c417,plain,
cC64xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_213]) ).
cnf(c419,plain,
cC86xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_215]) ).
cnf(c420,plain,
cC32xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_216]) ).
cnf(c421,plain,
cC48xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_217]) ).
cnf(c425,plain,
cC66xcomp(iV16459),
inference(clausification,[status(esa)],[axiom_221]) ).
cnf(c431,plain,
cC8xcomp(iV16460),
inference(clausification,[status(esa)],[axiom_227]) ).
cnf(c441,plain,
cC12xcomp(iV16461),
inference(clausification,[status(esa)],[axiom_237]) ).
cnf(c445,plain,
( cC38(X0)
| ~ rR1(iV16461,X0) ),
inference(clausification,[status(esa)],[axiom_241]) ).
cnf(c447,plain,
rR1(iV16461,iV16462),
inference(clausification,[status(esa)],[axiom_243]) ).
cnf(c465,plain,
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(clausification,[status(esa)],[axiom_261]) ).
cnf(c467,plain,
rR1(iV16463,iV16464),
inference(clausification,[status(esa)],[axiom_263]) ).
cnf(c469,plain,
( cC38(X0)
| ~ rR1(iV16464,X0) ),
inference(clausification,[status(esa)],[axiom_265]) ).
cnf(c478,plain,
rR1(iV16464,iV16465),
inference(clausification,[status(esa)],[axiom_274]) ).
cnf(c491,plain,
( ~ cC38(iV16465)
| ~ cC76(iV16453)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC44(iV16464)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC56(iV16455)
| ~ cC76(iV16463)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC56(iV16461)
| ~ cowlThing(iV16453)
| ~ cC42(iV16464)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC62(iV16453)
| 'xsd$ustring'(sK416)
| ~ cC34(iV16459)
| ~ cowlThing(iV16459)
| ~ cC104(iV16439)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16463)
| ~ cC38(iV16448)
| ~ cC44(iV16455)
| ~ cC38(iV16460)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16448)
| ~ cC82(iV16440)
| ~ cC62(iV16463)
| ~ cowlThing(iV16462)
| ~ cC130(iV16439)
| ~ cowlThing(iV16455)
| ~ cC56(iV16464)
| ~ cC38(iV16457)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16465)
| ~ cC88(iV16459)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC60(iV16463)
| ~ cC106(iV16439)
| ~ cC60(iV16453)
| ~ cC44(iV16461)
| ~ cowlThing(sK415)
| cowlNothing(sK415)
| ~ cowlThing(iV16460) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c492,plain,
( ~ cC38(iV16465)
| ~ cC76(iV16453)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC44(iV16464)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC56(iV16455)
| ~ cC76(iV16463)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC56(iV16461)
| ~ cowlThing(iV16453)
| ~ cC42(iV16464)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC62(iV16453)
| ~ 'xsd$ustring'(sK416)
| ~ cC34(iV16459)
| ~ cowlThing(iV16459)
| 'xsd$uinteger'(sK416)
| ~ cC104(iV16439)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16463)
| ~ cC38(iV16448)
| ~ cC44(iV16455)
| ~ cC38(iV16460)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16448)
| ~ cC82(iV16440)
| ~ cC62(iV16463)
| ~ cowlThing(iV16462)
| ~ cC130(iV16439)
| ~ cowlThing(iV16455)
| ~ cC56(iV16464)
| ~ cC38(iV16457)
| ~ cowlThing(iV16465)
| ~ cC88(iV16459)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC60(iV16463)
| ~ cC106(iV16439)
| ~ cC60(iV16453)
| ~ cC44(iV16461)
| ~ cowlThing(sK415)
| cowlNothing(sK415)
| ~ cowlThing(iV16460) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| cowlNothing(sK415)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[c0,c491]) ).
cnf(d1,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[c1,d0]) ).
cnf(d2,plain,
cC108(iV16439),
inference(resolution,[status(thm)],[c347,c353]) ).
cnf(d3,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
cC106(iV16439),
inference(resolution,[status(thm)],[d2,c29]) ).
cnf(d5,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC104(iV16439)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
cC28(iV16439),
inference(resolution,[status(thm)],[d2,c28]) ).
cnf(d7,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC104(iV16439)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d6,d5]) ).
cnf(d8,plain,
cC104(iV16439),
inference(resolution,[status(thm)],[d4,c25]) ).
cnf(d9,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d8,d7]) ).
cnf(d10,plain,
cC130(iV16439),
inference(resolution,[status(thm)],[c348,c353]) ).
cnf(d11,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
cC98(iV16440),
inference(resolution,[status(thm)],[c350,c354]) ).
cnf(d13,plain,
( ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d12,d11]) ).
cnf(d14,plain,
cC76(iV16463),
inference(resolution,[status(thm)],[c360,c363]) ).
cnf(d15,plain,
( ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d14,d13]) ).
cnf(d16,plain,
cC82(iV16440),
inference(resolution,[status(thm)],[d12,c343]) ).
cnf(d17,plain,
( ~ cC88(iV16459)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d16,d15]) ).
cnf(d18,plain,
cC62(iV16463),
inference(resolution,[status(thm)],[d14,c270]) ).
cnf(d19,plain,
( ~ cC88(iV16459)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d18,d17]) ).
cnf(d20,plain,
cC56(iV16461),
inference(resolution,[status(thm)],[c382,c386]) ).
cnf(d21,plain,
( ~ cC88(iV16459)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d20,d19]) ).
cnf(d22,plain,
cC80(iV16440),
inference(resolution,[status(thm)],[d16,c288]) ).
cnf(d23,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d22,d21]) ).
cnf(d24,plain,
cC38(iV16460),
inference(resolution,[status(thm)],[c392,c397]) ).
cnf(d25,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d24,d23]) ).
cnf(d26,plain,
cC60(iV16463),
inference(resolution,[status(thm)],[d18,c222]) ).
cnf(d27,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d26,d25]) ).
cnf(d28,plain,
cC44(iV16461),
inference(resolution,[status(thm)],[d20,c199]) ).
cnf(d29,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d28,d27]) ).
cnf(d30,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[c0,d29]) ).
cnf(d31,plain,
cC38(iV16462),
inference(resolution,[status(thm)],[c445,c447]) ).
cnf(d32,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d31,d30]) ).
cnf(d33,plain,
cC56(iV16464),
inference(resolution,[status(thm)],[c465,c467]) ).
cnf(d34,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d33,d32]) ).
cnf(d35,plain,
cC38(iV16465),
inference(resolution,[status(thm)],[c469,c478]) ).
cnf(d36,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d35,d34]) ).
cnf(d37,plain,
cC42(iV16461),
inference(resolution,[status(thm)],[d28,c161]) ).
cnf(d38,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d37,d36]) ).
cnf(d39,plain,
cC44(iV16464),
inference(resolution,[status(thm)],[d33,c199]) ).
cnf(d40,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d39,d38]) ).
cnf(d41,plain,
cC42(iV16464),
inference(resolution,[status(thm)],[d39,c161]) ).
cnf(d42,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d41,d40]) ).
cnf(d43,plain,
( cC34(iV16459)
| ~ cC30xcomp(iV16459) ),
inference(resolution,[status(thm)],[c129,c420]) ).
cnf(d44,plain,
cC34(iV16459),
inference(resolution,[status(thm)],[c413,d43]) ).
cnf(d45,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d44,d42]) ).
cnf(d46,plain,
( cC38(iV16448)
| ~ cC36xcomp(iV16448) ),
inference(resolution,[status(thm)],[c141,c367]) ).
cnf(d47,plain,
cC38(iV16448),
inference(resolution,[status(thm)],[c372,d46]) ).
cnf(d48,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d47,d45]) ).
cnf(d49,plain,
( cC38(iV16457)
| ~ cC36xcomp(iV16457) ),
inference(resolution,[status(thm)],[c141,c401]) ).
cnf(d50,plain,
cC38(iV16457),
inference(resolution,[status(thm)],[c405,d49]) ).
cnf(d51,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d50,d48]) ).
cnf(d52,plain,
( ~ cC8xcomp(iV16460)
| cC42(iV16455) ),
inference(resolution,[status(thm)],[c159,c397]) ).
cnf(d53,plain,
cC42(iV16455),
inference(resolution,[status(thm)],[c431,d52]) ).
cnf(d54,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d53,d51]) ).
cnf(d55,plain,
( cC50(iV16459)
| ~ cC46xcomp(iV16459) ),
inference(resolution,[status(thm)],[c179,c421]) ).
cnf(d56,plain,
cC50(iV16459),
inference(resolution,[status(thm)],[c416,d55]) ).
cnf(d57,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d56,d54]) ).
cnf(d58,plain,
( cC60(iV16453)
| ~ cC12xcomp(iV16461) ),
inference(resolution,[status(thm)],[c221,c386]) ).
cnf(d59,plain,
cC60(iV16453),
inference(resolution,[status(thm)],[c441,d58]) ).
cnf(d60,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d59,d57]) ).
cnf(d61,plain,
( cC68(iV16459)
| ~ cC64xcomp(iV16459) ),
inference(resolution,[status(thm)],[c243,c425]) ).
cnf(d62,plain,
cC68(iV16459),
inference(resolution,[status(thm)],[c417,d61]) ).
cnf(d63,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d62,d60]) ).
cnf(d64,plain,
( cC88(iV16459)
| ~ cC84xcomp(iV16459) ),
inference(resolution,[status(thm)],[c309,c419]) ).
cnf(d65,plain,
cC88(iV16459),
inference(resolution,[status(thm)],[c414,d64]) ).
cnf(d66,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d65,d63]) ).
cnf(d67,plain,
( cC44(iV16455)
| ~ cC40xcomp(iV16455) ),
inference(resolution,[status(thm)],[d53,c162]) ).
cnf(d68,plain,
cC44(iV16455),
inference(resolution,[status(thm)],[c389,d67]) ).
cnf(d69,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d68,d66]) ).
cnf(d70,plain,
( cC56(iV16455)
| ~ cC44(iV16455) ),
inference(resolution,[status(thm)],[c200,c394]) ).
cnf(d71,plain,
cC56(iV16455),
inference(resolution,[status(thm)],[d68,d70]) ).
cnf(d72,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d71,d69]) ).
cnf(d73,plain,
( cC62(iV16453)
| ~ cC58xcomp(iV16453) ),
inference(resolution,[status(thm)],[d59,c224]) ).
cnf(d74,plain,
cC62(iV16453),
inference(resolution,[status(thm)],[c385,d73]) ).
cnf(d75,plain,
( ~ cC76(iV16453)
| 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d74,d72]) ).
cnf(d76,plain,
( cC76(iV16453)
| ~ cC62(iV16453) ),
inference(resolution,[status(thm)],[c271,c378]) ).
cnf(d77,plain,
cC76(iV16453),
inference(resolution,[status(thm)],[d74,d76]) ).
cnf(d78,plain,
( 'xsd$ustring'(sK416)
| ~ 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d77,d75]) ).
cnf(d79,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| cowlNothing(sK415)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[c0,c492]) ).
cnf(d80,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[c1,d79]) ).
cnf(d81,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d2,d80]) ).
cnf(d82,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC104(iV16439)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d4,d81]) ).
cnf(d83,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC104(iV16439)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d6,d82]) ).
cnf(d84,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d8,d83]) ).
cnf(d85,plain,
( ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d10,d84]) ).
cnf(d86,plain,
( ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d12,d85]) ).
cnf(d87,plain,
( ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d14,d86]) ).
cnf(d88,plain,
( ~ cC88(iV16459)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d16,d87]) ).
cnf(d89,plain,
( ~ cC88(iV16459)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d18,d88]) ).
cnf(d90,plain,
( ~ cC88(iV16459)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d20,d89]) ).
cnf(d91,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d22,d90]) ).
cnf(d92,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d24,d91]) ).
cnf(d93,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d26,d92]) ).
cnf(d94,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440) ),
inference(resolution,[status(thm)],[d28,d93]) ).
cnf(d95,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[c0,d94]) ).
cnf(d96,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d31,d95]) ).
cnf(d97,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d33,d96]) ).
cnf(d98,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d35,d97]) ).
cnf(d99,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d37,d98]) ).
cnf(d100,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d39,d99]) ).
cnf(d101,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d41,d100]) ).
cnf(d102,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC38(iV16448)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d44,d101]) ).
cnf(d103,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d47,d102]) ).
cnf(d104,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d50,d103]) ).
cnf(d105,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d53,d104]) ).
cnf(d106,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d56,d105]) ).
cnf(d107,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d59,d106]) ).
cnf(d108,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d62,d107]) ).
cnf(d109,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d65,d108]) ).
cnf(d110,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d68,d109]) ).
cnf(d111,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d71,d110]) ).
cnf(d112,plain,
( ~ cC76(iV16453)
| ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d74,d111]) ).
cnf(d113,plain,
( ~ 'xsd$ustring'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d77,d112]) ).
cnf(d114,plain,
( 'xsd$uinteger'(sK416)
| 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d113,c3]) ).
cnf(d115,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448) ),
inference(resolution,[status(thm)],[c0,d114]) ).
cnf(d116,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448) ),
inference(resolution,[status(thm)],[d115,c0]) ).
cnf(d117,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[c0,d116]) ).
cnf(d118,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[d117,c0]) ).
cnf(d119,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[c0,d118]) ).
cnf(d120,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[d119,c0]) ).
cnf(d121,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[c0,d120]) ).
cnf(d122,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[d121,c0]) ).
cnf(d123,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[c0,d122]) ).
cnf(d124,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[d123,c0]) ).
cnf(d125,plain,
( 'xsd$uinteger'(sK416)
| ~ cowlThing(iV16457) ),
inference(resolution,[status(thm)],[c0,d124]) ).
cnf(d126,plain,
'xsd$uinteger'(sK416),
inference(resolution,[status(thm)],[d125,c0]) ).
cnf(d127,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463) ),
inference(resolution,[status(thm)],[d126,d78]) ).
cnf(d128,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(sK415)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448) ),
inference(resolution,[status(thm)],[c0,d127]) ).
cnf(d129,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448) ),
inference(resolution,[status(thm)],[d128,c0]) ).
cnf(d130,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[c0,d129]) ).
cnf(d131,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[d130,c0]) ).
cnf(d132,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[c0,d131]) ).
cnf(d133,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[d132,c0]) ).
cnf(d134,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[c0,d133]) ).
cnf(d135,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[d134,c0]) ).
cnf(d136,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[c0,d135]) ).
cnf(d137,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[d136,c0]) ).
cnf(d138,plain,
( 'xsd$ustring'(sK416)
| ~ cowlThing(iV16457) ),
inference(resolution,[status(thm)],[c0,d137]) ).
cnf(d139,plain,
'xsd$ustring'(sK416),
inference(resolution,[status(thm)],[d138,c0]) ).
cnf(d140,plain,
~ 'xsd$uinteger'(sK416),
inference(resolution,[status(thm)],[d139,c2]) ).
cnf(d141,plain,
$false,
inference(resolution,[status(thm)],[d126,d140]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n014.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Fri Sep 25 19:41:38 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.17/5.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.29/11.17 % SZS status Theorem for theBenchmark.p
% 42.29/11.17 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------