%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS153+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 : n002.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:16 AM UTC 2026
% Result : Theorem 35.05s 5.69s
% Output : CNFRefutation 35.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 53
% Syntax : Number of formulae : 261 ( 98 unt; 0 def)
% Number of atoms : 2802 ( 0 equ)
% Maximal formula atoms : 49 ( 10 avg)
% Number of connectives : 4978 (2437 ~;2407 |; 111 &)
% ( 19 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 50 ( 11 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 : 60 ( 2 sgn 26 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ).
fof(axiom_1,axiom,
! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) ) ).
fof(axiom_5,axiom,
! [X0] :
( cC106(X0)
<=> ( cC104(X0)
& ~ cC100(X0) ) ) ).
fof(axiom_6,axiom,
! [X0] :
( cC108(X0)
<=> ( cC106(X0)
& cC28(X0) ) ) ).
fof(axiom_25,axiom,
! [X0] :
( cC34(X0)
<=> ( ~ cC30(X0)
& ~ cC32(X0) ) ) ).
fof(axiom_27,axiom,
! [X0] :
( cC38(X0)
<=> ( cTOP(X0)
& ~ cC36(X0) ) ) ).
fof(axiom_29,axiom,
! [X0] :
( cC42(X0)
<=> ? [X1] :
( ~ cC8(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_30,axiom,
! [X0] :
( cC44(X0)
<=> ( cC42(X0)
& ~ cC40(X0) ) ) ).
fof(axiom_33,axiom,
! [X0] :
( cC50(X0)
<=> ( ~ cC48(X0)
& ~ cC46(X0) ) ) ).
fof(axiom_36,axiom,
! [X0] :
( cC56(X0)
<=> ( ~ cC54(X0)
& cC44(X0) ) ) ).
fof(axiom_39,axiom,
! [X0] :
( cC60(X0)
<=> ? [X1] :
( ~ cC12(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_40,axiom,
! [X0] :
( cC62(X0)
<=> ( ~ cC58(X0)
& cC60(X0) ) ) ).
fof(axiom_43,axiom,
! [X0] :
( cC68(X0)
<=> ( ~ cC66(X0)
& ~ cC64(X0) ) ) ).
fof(axiom_47,axiom,
! [X0] :
( cC76(X0)
<=> ( cC62(X0)
& ~ cC74(X0) ) ) ).
fof(axiom_50,axiom,
! [X0] :
( cC82(X0)
<=> ( cC80(X0)
& ~ cC78(X0) ) ) ).
fof(axiom_53,axiom,
! [X0] :
( cC88(X0)
<=> ( ~ cC86(X0)
& ~ cC84(X0) ) ) ).
fof(axiom_58,axiom,
! [X0] :
( cC98(X0)
<=> ( cC82(X0)
& ~ cC96(X0) ) ) ).
fof(axiom_59,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC130(X0)
& cC108(X0) ) ) ).
fof(axiom_60,axiom,
! [X0] :
( rR1(iV16439,X0)
=> cC98(X0) ) ).
fof(axiom_61,axiom,
cTEST(iV16439) ).
fof(axiom_64,axiom,
rR1(iV16439,iV16440) ).
fof(axiom_67,axiom,
! [X0] :
( rR1(iV16440,X0)
=> cC76(X0) ) ).
fof(axiom_73,axiom,
rR1(iV16440,iV16463) ).
fof(axiom_76,axiom,
~ cC36(iV16448) ).
fof(axiom_79,axiom,
cTOP(iV16448) ).
fof(axiom_91,axiom,
~ cC58(iV16453) ).
fof(axiom_92,axiom,
~ cC74(iV16453) ).
fof(axiom_93,axiom,
! [X0] :
( rR1(iV16453,X0)
=> cC56(X0) ) ).
fof(axiom_96,axiom,
rR1(iV16453,iV16461) ).
fof(axiom_98,axiom,
~ cC40(iV16455) ).
fof(axiom_103,axiom,
~ cC54(iV16455) ).
fof(axiom_107,axiom,
rR1(iV16455,iV16460) ).
fof(axiom_108,axiom,
~ cC36(iV16457) ).
fof(axiom_113,axiom,
cTOP(iV16457) ).
fof(axiom_120,axiom,
~ cC48(iV16459) ).
fof(axiom_121,axiom,
~ cC30(iV16459) ).
fof(axiom_123,axiom,
~ cC86(iV16459) ).
fof(axiom_124,axiom,
~ cC46(iV16459) ).
fof(axiom_127,axiom,
~ cC66(iV16459) ).
fof(axiom_132,axiom,
~ cC84(iV16459) ).
fof(axiom_133,axiom,
~ cC64(iV16459) ).
fof(axiom_135,axiom,
~ cC32(iV16459) ).
fof(axiom_137,axiom,
~ cC36(iV16460) ).
fof(axiom_140,axiom,
cTOP(iV16460) ).
fof(axiom_141,axiom,
~ cC8(iV16460) ).
fof(axiom_151,axiom,
~ cC12(iV16461) ).
fof(axiom_161,axiom,
~ cC36(iV16462) ).
fof(axiom_162,axiom,
cTOP(iV16462) ).
fof(axiom_171,axiom,
! [X0] :
( rR1(iV16463,X0)
=> cC56(X0) ) ).
fof(axiom_177,axiom,
rR1(iV16463,iV16464) ).
fof(axiom_195,axiom,
~ cC36(iV16465) ).
fof(axiom_196,axiom,
cTOP(iV16465) ).
fof(the_axiom,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)
& ! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ) ).
fof(negated_conjecture,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)
& ! [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(c14,plain,
( cC104(X0)
| ~ cC106(X0) ),
inference(clausification,[status(esa)],[axiom_5]) ).
cnf(c16,plain,
( cC28(X0)
| ~ cC108(X0) ),
inference(clausification,[status(esa)],[axiom_6]) ).
cnf(c17,plain,
( cC106(X0)
| ~ cC108(X0) ),
inference(clausification,[status(esa)],[axiom_6]) ).
cnf(c75,plain,
( cC30(X0)
| cC32(X0)
| cC34(X0) ),
inference(clausification,[status(esa)],[axiom_25]) ).
cnf(c81,plain,
( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ),
inference(clausification,[status(esa)],[axiom_27]) ).
cnf(c87,plain,
( cC8(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(clausification,[status(esa)],[axiom_29]) ).
cnf(c89,plain,
( cC42(X0)
| ~ cC44(X0) ),
inference(clausification,[status(esa)],[axiom_30]) ).
cnf(c90,plain,
( ~ cC42(X0)
| cC40(X0)
| cC44(X0) ),
inference(clausification,[status(esa)],[axiom_30]) ).
cnf(c99,plain,
( cC48(X0)
| cC46(X0)
| cC50(X0) ),
inference(clausification,[status(esa)],[axiom_33]) ).
cnf(c106,plain,
( cC44(X0)
| ~ cC56(X0) ),
inference(clausification,[status(esa)],[axiom_36]) ).
cnf(c108,plain,
( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ),
inference(clausification,[status(esa)],[axiom_36]) ).
cnf(c117,plain,
( cC12(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(clausification,[status(esa)],[axiom_39]) ).
cnf(c118,plain,
( cC60(X0)
| ~ cC62(X0) ),
inference(clausification,[status(esa)],[axiom_40]) ).
cnf(c120,plain,
( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(clausification,[status(esa)],[axiom_40]) ).
cnf(c129,plain,
( cC66(X0)
| cC64(X0)
| cC68(X0) ),
inference(clausification,[status(esa)],[axiom_43]) ).
cnf(c140,plain,
( cC62(X0)
| ~ cC76(X0) ),
inference(clausification,[status(esa)],[axiom_47]) ).
cnf(c141,plain,
( ~ cC62(X0)
| cC74(X0)
| cC76(X0) ),
inference(clausification,[status(esa)],[axiom_47]) ).
cnf(c149,plain,
( cC80(X0)
| ~ cC82(X0) ),
inference(clausification,[status(esa)],[axiom_50]) ).
cnf(c159,plain,
( cC86(X0)
| cC84(X0)
| cC88(X0) ),
inference(clausification,[status(esa)],[axiom_53]) ).
cnf(c173,plain,
( cC82(X0)
| ~ cC98(X0) ),
inference(clausification,[status(esa)],[axiom_58]) ).
cnf(c175,plain,
( cC108(X0)
| ~ cTEST(X0) ),
inference(clausification,[status(esa)],[axiom_59]) ).
cnf(c176,plain,
( cC130(X0)
| ~ cTEST(X0) ),
inference(clausification,[status(esa)],[axiom_59]) ).
cnf(c178,plain,
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(clausification,[status(esa)],[axiom_60]) ).
cnf(c179,plain,
cTEST(iV16439),
inference(clausification,[status(esa)],[axiom_61]) ).
cnf(c182,plain,
rR1(iV16439,iV16440),
inference(clausification,[status(esa)],[axiom_64]) ).
cnf(c185,plain,
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(clausification,[status(esa)],[axiom_67]) ).
cnf(c191,plain,
rR1(iV16440,iV16463),
inference(clausification,[status(esa)],[axiom_73]) ).
cnf(c194,plain,
~ cC36(iV16448),
inference(clausification,[status(esa)],[axiom_76]) ).
cnf(c197,plain,
cTOP(iV16448),
inference(clausification,[status(esa)],[axiom_79]) ).
cnf(c209,plain,
~ cC58(iV16453),
inference(clausification,[status(esa)],[axiom_91]) ).
cnf(c210,plain,
~ cC74(iV16453),
inference(clausification,[status(esa)],[axiom_92]) ).
cnf(c211,plain,
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(clausification,[status(esa)],[axiom_93]) ).
cnf(c214,plain,
rR1(iV16453,iV16461),
inference(clausification,[status(esa)],[axiom_96]) ).
cnf(c216,plain,
~ cC40(iV16455),
inference(clausification,[status(esa)],[axiom_98]) ).
cnf(c221,plain,
~ cC54(iV16455),
inference(clausification,[status(esa)],[axiom_103]) ).
cnf(c225,plain,
rR1(iV16455,iV16460),
inference(clausification,[status(esa)],[axiom_107]) ).
cnf(c226,plain,
~ cC36(iV16457),
inference(clausification,[status(esa)],[axiom_108]) ).
cnf(c231,plain,
cTOP(iV16457),
inference(clausification,[status(esa)],[axiom_113]) ).
cnf(c238,plain,
~ cC48(iV16459),
inference(clausification,[status(esa)],[axiom_120]) ).
cnf(c239,plain,
~ cC30(iV16459),
inference(clausification,[status(esa)],[axiom_121]) ).
cnf(c241,plain,
~ cC86(iV16459),
inference(clausification,[status(esa)],[axiom_123]) ).
cnf(c242,plain,
~ cC46(iV16459),
inference(clausification,[status(esa)],[axiom_124]) ).
cnf(c245,plain,
~ cC66(iV16459),
inference(clausification,[status(esa)],[axiom_127]) ).
cnf(c250,plain,
~ cC84(iV16459),
inference(clausification,[status(esa)],[axiom_132]) ).
cnf(c251,plain,
~ cC64(iV16459),
inference(clausification,[status(esa)],[axiom_133]) ).
cnf(c253,plain,
~ cC32(iV16459),
inference(clausification,[status(esa)],[axiom_135]) ).
cnf(c255,plain,
~ cC36(iV16460),
inference(clausification,[status(esa)],[axiom_137]) ).
cnf(c258,plain,
cTOP(iV16460),
inference(clausification,[status(esa)],[axiom_140]) ).
cnf(c259,plain,
~ cC8(iV16460),
inference(clausification,[status(esa)],[axiom_141]) ).
cnf(c269,plain,
~ cC12(iV16461),
inference(clausification,[status(esa)],[axiom_151]) ).
cnf(c279,plain,
~ cC36(iV16462),
inference(clausification,[status(esa)],[axiom_161]) ).
cnf(c280,plain,
cTOP(iV16462),
inference(clausification,[status(esa)],[axiom_162]) ).
cnf(c289,plain,
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(clausification,[status(esa)],[axiom_171]) ).
cnf(c295,plain,
rR1(iV16463,iV16464),
inference(clausification,[status(esa)],[axiom_177]) ).
cnf(c313,plain,
~ cC36(iV16465),
inference(clausification,[status(esa)],[axiom_195]) ).
cnf(c314,plain,
cTOP(iV16465),
inference(clausification,[status(esa)],[axiom_196]) ).
cnf(c319,plain,
( ~ cC38(iV16465)
| ~ cC76(iV16453)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| 'xsd$ustring'(sK158)
| ~ cC108(iV16439)
| ~ cowlThing(sK157)
| ~ cC60(iV16463)
| ~ 'xsd$uinteger'(sK158)
| ~ 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)
| cowlNothing(sK157)
| ~ cC62(iV16453)
| ~ 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)
| ~ cowlThing(iV16465)
| ~ cC88(iV16459)
| ~ cowlThing(iV16439)
| ~ cC106(iV16439)
| ~ cC60(iV16453)
| ~ cC44(iV16461)
| ~ cowlThing(iV16460) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c320,plain,
( ~ cC38(iV16465)
| ~ cC76(iV16453)
| ~ 'xsd$ustring'(sK158)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC108(iV16439)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ cC60(iV16463)
| ~ 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)
| cowlNothing(sK157)
| ~ cC62(iV16453)
| ~ 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)
| ~ cowlThing(iV16465)
| ~ cC88(iV16459)
| ~ cowlThing(iV16439)
| ~ cC106(iV16439)
| ~ cC60(iV16453)
| ~ cC44(iV16461)
| ~ cowlThing(iV16460) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,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)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| cowlNothing(sK157)
| ~ cowlThing(sK157)
| ~ 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,c319]) ).
cnf(d1,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)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[c175,c179]) ).
cnf(d3,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)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
cC28(iV16439),
inference(resolution,[status(thm)],[d2,c16]) ).
cnf(d5,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)
| ~ cC130(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
cC106(iV16439),
inference(resolution,[status(thm)],[d2,c17]) ).
cnf(d7,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)
| ~ cC130(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d6,c14]) ).
cnf(d9,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)
| ~ cC130(iV16439)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[c176,c179]) ).
cnf(d11,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)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC34(iV16459)
| cC30(iV16459) ),
inference(resolution,[status(thm)],[c75,c253]) ).
cnf(d13,plain,
cC34(iV16459),
inference(resolution,[status(thm)],[c239,d12]) ).
cnf(d14,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)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d13,d11]) ).
cnf(d15,plain,
( cC38(iV16460)
| cC36(iV16460) ),
inference(resolution,[status(thm)],[c81,c258]) ).
cnf(d16,plain,
cC38(iV16460),
inference(resolution,[status(thm)],[c255,d15]) ).
cnf(d17,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(iV16448)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d14]) ).
cnf(d18,plain,
( cC38(iV16462)
| cC36(iV16462) ),
inference(resolution,[status(thm)],[c81,c280]) ).
cnf(d19,plain,
cC38(iV16462),
inference(resolution,[status(thm)],[c279,d18]) ).
cnf(d20,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(iV16457)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d19,d17]) ).
cnf(d21,plain,
( cC38(iV16457)
| cC36(iV16457) ),
inference(resolution,[status(thm)],[c81,c231]) ).
cnf(d22,plain,
cC38(iV16457),
inference(resolution,[status(thm)],[c226,d21]) ).
cnf(d23,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(iV16448)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d20]) ).
cnf(d24,plain,
( cC38(iV16448)
| cC36(iV16448) ),
inference(resolution,[status(thm)],[c81,c197]) ).
cnf(d25,plain,
cC38(iV16448),
inference(resolution,[status(thm)],[c194,d24]) ).
cnf(d26,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)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d25,d23]) ).
cnf(d27,plain,
( cC38(iV16465)
| cC36(iV16465) ),
inference(resolution,[status(thm)],[c314,c81]) ).
cnf(d28,plain,
cC38(iV16465),
inference(resolution,[status(thm)],[c313,d27]) ).
cnf(d29,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)
| ~ cC98(iV16440)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d26]) ).
cnf(d30,plain,
cC98(iV16440),
inference(resolution,[status(thm)],[c178,c182]) ).
cnf(d31,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d30,d29]) ).
cnf(d32,plain,
cC76(iV16463),
inference(resolution,[status(thm)],[c185,c191]) ).
cnf(d33,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d32,d31]) ).
cnf(d34,plain,
cC82(iV16440),
inference(resolution,[status(thm)],[d30,c173]) ).
cnf(d35,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d34,d33]) ).
cnf(d36,plain,
cC62(iV16463),
inference(resolution,[status(thm)],[d32,c140]) ).
cnf(d37,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d36,d35]) ).
cnf(d38,plain,
cC80(iV16440),
inference(resolution,[status(thm)],[d34,c149]) ).
cnf(d39,plain,
( ~ cC88(iV16459)
| ~ 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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d38,d37]) ).
cnf(d40,plain,
cC56(iV16461),
inference(resolution,[status(thm)],[c211,c214]) ).
cnf(d41,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d40,d39]) ).
cnf(d42,plain,
cC60(iV16463),
inference(resolution,[status(thm)],[d36,c118]) ).
cnf(d43,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d42,d41]) ).
cnf(d44,plain,
cC44(iV16461),
inference(resolution,[status(thm)],[d40,c106]) ).
cnf(d45,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d44,d43]) ).
cnf(d46,plain,
cC56(iV16464),
inference(resolution,[status(thm)],[c289,c295]) ).
cnf(d47,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d46,d45]) ).
cnf(d48,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)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d47]) ).
cnf(d49,plain,
cC42(iV16461),
inference(resolution,[status(thm)],[d44,c89]) ).
cnf(d50,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d49,d48]) ).
cnf(d51,plain,
cC44(iV16464),
inference(resolution,[status(thm)],[d46,c106]) ).
cnf(d52,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d51,d50]) ).
cnf(d53,plain,
cC42(iV16464),
inference(resolution,[status(thm)],[d51,c89]) ).
cnf(d54,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d52]) ).
cnf(d55,plain,
( cC42(iV16455)
| cC8(iV16460) ),
inference(resolution,[status(thm)],[c225,c87]) ).
cnf(d56,plain,
cC42(iV16455),
inference(resolution,[status(thm)],[c259,d55]) ).
cnf(d57,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC50(iV16459)
| cC46(iV16459) ),
inference(resolution,[status(thm)],[c99,c238]) ).
cnf(d59,plain,
cC50(iV16459),
inference(resolution,[status(thm)],[c242,d58]) ).
cnf(d60,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC60(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[c117,c214]) ).
cnf(d62,plain,
cC60(iV16453),
inference(resolution,[status(thm)],[c269,d61]) ).
cnf(d63,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC68(iV16459)
| cC64(iV16459) ),
inference(resolution,[status(thm)],[c129,c245]) ).
cnf(d65,plain,
cC68(iV16459),
inference(resolution,[status(thm)],[c251,d64]) ).
cnf(d66,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC88(iV16459)
| cC84(iV16459) ),
inference(resolution,[status(thm)],[c159,c241]) ).
cnf(d68,plain,
cC88(iV16459),
inference(resolution,[status(thm)],[c250,d67]) ).
cnf(d69,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC44(iV16455)
| cC40(iV16455) ),
inference(resolution,[status(thm)],[d56,c90]) ).
cnf(d71,plain,
cC44(iV16455),
inference(resolution,[status(thm)],[c216,d70]) ).
cnf(d72,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)
| cC58(iV16453) ),
inference(resolution,[status(thm)],[d62,c120]) ).
cnf(d74,plain,
cC62(iV16453),
inference(resolution,[status(thm)],[c209,d73]) ).
cnf(d75,plain,
( ~ cC76(iV16453)
| ~ cC56(iV16455)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC56(iV16455)
| cC54(iV16455) ),
inference(resolution,[status(thm)],[d71,c108]) ).
cnf(d77,plain,
cC56(iV16455),
inference(resolution,[status(thm)],[c221,d76]) ).
cnf(d78,plain,
( ~ cC76(iV16453)
| 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,
( cC76(iV16453)
| cC74(iV16453) ),
inference(resolution,[status(thm)],[d74,c141]) ).
cnf(d80,plain,
cC76(iV16453),
inference(resolution,[status(thm)],[c210,d79]) ).
cnf(d81,plain,
( 'xsd$ustring'(sK158)
| ~ 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d80,d78]) ).
cnf(d82,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)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| cowlNothing(sK157)
| ~ cowlThing(sK157)
| ~ 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,c320]) ).
cnf(d83,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)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d82]) ).
cnf(d84,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)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d83]) ).
cnf(d85,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)
| ~ cC130(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,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)
| ~ cC130(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d85]) ).
cnf(d87,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)
| ~ cC130(iV16439)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d86]) ).
cnf(d88,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)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d87]) ).
cnf(d89,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)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d13,d88]) ).
cnf(d90,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(iV16448)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d89]) ).
cnf(d91,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(iV16457)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d19,d90]) ).
cnf(d92,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(iV16448)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d91]) ).
cnf(d93,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)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d25,d92]) ).
cnf(d94,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)
| ~ cC98(iV16440)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)
| ~ 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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d30,d94]) ).
cnf(d96,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d32,d95]) ).
cnf(d97,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d34,d96]) ).
cnf(d98,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d36,d97]) ).
cnf(d99,plain,
( ~ cC88(iV16459)
| ~ 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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d38,d98]) ).
cnf(d100,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d40,d99]) ).
cnf(d101,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d42,d100]) ).
cnf(d102,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d44,d101]) ).
cnf(d103,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d46,d102]) ).
cnf(d104,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)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d103]) ).
cnf(d105,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d49,d104]) ).
cnf(d106,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d51,d105]) ).
cnf(d107,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d106]) ).
cnf(d108,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d107]) ).
cnf(d109,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d108]) ).
cnf(d110,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d109]) ).
cnf(d111,plain,
( ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d110]) ).
cnf(d112,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d111]) ).
cnf(d113,plain,
( ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d112]) ).
cnf(d114,plain,
( ~ cC76(iV16453)
| ~ cC56(iV16455)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d113]) ).
cnf(d115,plain,
( ~ cC76(iV16453)
| ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d114]) ).
cnf(d116,plain,
( ~ 'xsd$ustring'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d80,d115]) ).
cnf(d117,plain,
( 'xsd$uinteger'(sK158)
| 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d116,c3]) ).
cnf(d118,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d117]) ).
cnf(d119,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448) ),
inference(resolution,[status(thm)],[d118,c0]) ).
cnf(d120,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[c0,d119]) ).
cnf(d121,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[d120,c0]) ).
cnf(d122,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[c0,d121]) ).
cnf(d123,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[d122,c0]) ).
cnf(d124,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[c0,d123]) ).
cnf(d125,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[d124,c0]) ).
cnf(d126,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[c0,d125]) ).
cnf(d127,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[d126,c0]) ).
cnf(d128,plain,
( 'xsd$uinteger'(sK158)
| ~ cowlThing(iV16457) ),
inference(resolution,[status(thm)],[c0,d127]) ).
cnf(d129,plain,
'xsd$uinteger'(sK158),
inference(resolution,[status(thm)],[d128,c0]) ).
cnf(d130,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(sK157)
| ~ 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)],[d129,d81]) ).
cnf(d131,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(sK157)
| ~ 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,d130]) ).
cnf(d132,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448) ),
inference(resolution,[status(thm)],[d131,c0]) ).
cnf(d133,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[c0,d132]) ).
cnf(d134,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453) ),
inference(resolution,[status(thm)],[d133,c0]) ).
cnf(d135,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[c0,d134]) ).
cnf(d136,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461) ),
inference(resolution,[status(thm)],[d135,c0]) ).
cnf(d137,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[c0,d136]) ).
cnf(d138,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455) ),
inference(resolution,[status(thm)],[d137,c0]) ).
cnf(d139,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[c0,d138]) ).
cnf(d140,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460) ),
inference(resolution,[status(thm)],[d139,c0]) ).
cnf(d141,plain,
( 'xsd$ustring'(sK158)
| ~ cowlThing(iV16457) ),
inference(resolution,[status(thm)],[c0,d140]) ).
cnf(d142,plain,
'xsd$ustring'(sK158),
inference(resolution,[status(thm)],[d141,c0]) ).
cnf(d143,plain,
~ 'xsd$uinteger'(sK158),
inference(resolution,[status(thm)],[d142,c2]) ).
cnf(d144,plain,
$false,
inference(resolution,[status(thm)],[d129,d143]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/1.02 % Computer : n002.cluster.edu
% 0.13/1.02 % Model : x86_64 x86_64
% 0.13/1.02 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/1.02 % Memory : 8046.5625MB
% 0.13/1.02 % OS : Linux 6.8.0-71-generic
% 0.13/1.02 % CPULimit : 300
% 0.13/1.02 % WCLimit : 300
% 0.13/1.02 % DateTime : Fri Sep 25 19:44:23 UTC 2026
% 0.13/1.02 % CPUTime :
% 0.13/1.02 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.05/5.69 % SZS status Theorem for theBenchmark.p
% 35.05/5.69 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------