%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS151+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 : n026.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:15 AM UTC 2026
% Result : Theorem 20.67s 3.29s
% Output : CNFRefutation 20.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 53
% Syntax : Number of formulae : 280 ( 80 unt; 0 def)
% Number of atoms : 3377 ( 0 equ)
% Maximal formula atoms : 54 ( 12 avg)
% Number of connectives : 6034 (2937 ~;2923 |; 135 &)
% ( 39 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 55 ( 13 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 60 ( 59 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 11 con; 0-0 aty)
% Number of variables : 102 ( 2 sgn 42 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ).
fof(axiom_1,axiom,
! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) ) ).
fof(axiom_2,axiom,
! [X0] :
( cC10(X0)
<=> ( cC4(X0)
& cC8(X0) ) ) ).
fof(axiom_7,axiom,
! [X0] :
( cC110(X0)
<=> ( cTOP(X0)
& cC108(X0) ) ) ).
fof(axiom_8,axiom,
! [X0] :
( cC112(X0)
<=> ( cC110(X0)
& cC90(X0) ) ) ).
fof(axiom_9,axiom,
! [X0] :
( cC114(X0)
<=> cTOP(X0) ) ).
fof(axiom_10,axiom,
! [X0] :
( cC116(X0)
<=> ( cC112(X0)
& cC114(X0) ) ) ).
fof(axiom_18,axiom,
! [X0] :
( cC132(X0)
<=> ( cC130(X0)
& cTOP(X0) ) ) ).
fof(axiom_19,axiom,
! [X0] :
( cC134(X0)
<=> ( cC116(X0)
& cC132(X0) ) ) ).
fof(axiom_20,axiom,
! [X0] :
( cC136(X0)
<=> cTOP(X0) ) ).
fof(axiom_21,axiom,
! [X0] :
( cC138(X0)
<=> ( cC134(X0)
& cC136(X0) ) ) ).
fof(axiom_30,axiom,
! [X0] :
( cC154(X0)
<=> ( cC152(X0)
& cTOP(X0) ) ) ).
fof(axiom_31,axiom,
! [X0] :
( cC156(X0)
<=> ( cC138(X0)
& cC154(X0) ) ) ).
fof(axiom_32,axiom,
! [X0] :
( cC158(X0)
<=> ( cC156(X0)
& cC22(X0) ) ) ).
fof(axiom_33,axiom,
! [X0] :
( cC16(X0)
<=> ( cC10(X0)
& cC14(X0) ) ) ).
fof(axiom_41,axiom,
! [X0] :
( cC174(X0)
<=> ( ~ cC172(X0)
& cC168(X0) ) ) ).
fof(axiom_44,axiom,
! [X0] :
( cC180(X0)
<=> ( cC174(X0)
& ~ cC178(X0) ) ) ).
fof(axiom_46,axiom,
! [X0] :
( cC22(X0)
<=> ( cC20(X0)
& cC16(X0) ) ) ).
fof(axiom_47,axiom,
! [X0] :
( cC24(X0)
<=> ? [X1] :
( ~ cC2(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_50,axiom,
! [X0] :
( cC30(X0)
<=> ? [X1] :
( ~ cC12(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_54,axiom,
! [X0] :
( cC38(X0)
<=> ( cTOP(X0)
& cC36(X0) ) ) ).
fof(axiom_56,axiom,
! [X0] :
( cC40(X0)
<=> cTOP(X0) ) ).
fof(axiom_57,axiom,
! [X0] :
( cC42(X0)
<=> ( cC38(X0)
& cC40(X0) ) ) ).
fof(axiom_58,axiom,
! [X0] :
( cC44(X0)
<=> ? [X1] :
( ~ cC2(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_61,axiom,
! [X0] :
( cC50(X0)
<=> ? [X1] :
( ~ cC12(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_65,axiom,
! [X0] :
( cC58(X0)
<=> ( cTOP(X0)
& cC56(X0) ) ) ).
fof(axiom_66,axiom,
! [X0] :
( cC60(X0)
<=> ( cC42(X0)
& cC58(X0) ) ) ).
fof(axiom_67,axiom,
! [X0] :
( cC62(X0)
<=> cTOP(X0) ) ).
fof(axiom_68,axiom,
! [X0] :
( cC64(X0)
<=> ( cC60(X0)
& cC62(X0) ) ) ).
fof(axiom_69,axiom,
! [X0] :
( cC66(X0)
<=> ? [X1] :
( ~ cC2(X1)
& rR1(X0,X1) ) ) ).
fof(axiom_73,axiom,
! [X0] :
( cC74(X0)
<=> ( ~ cC72(X0)
& ~ cC18(X0) ) ) ).
fof(axiom_77,axiom,
! [X0] :
( cC80(X0)
<=> ( cC78(X0)
& cTOP(X0) ) ) ).
fof(axiom_78,axiom,
! [X0] :
( cC82(X0)
<=> ( cC64(X0)
& cC80(X0) ) ) ).
fof(axiom_79,axiom,
! [X0] :
( cC84(X0)
<=> cTOP(X0) ) ).
fof(axiom_80,axiom,
! [X0] :
( cC86(X0)
<=> ( cC84(X0)
& cC82(X0) ) ) ).
fof(axiom_81,axiom,
! [X0] :
( cC88(X0)
<=> cTOP(X0) ) ).
fof(axiom_82,axiom,
! [X0] :
( cC90(X0)
<=> ( cC86(X0)
& cC88(X0) ) ) ).
fof(axiom_86,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC180(X0)
& cC158(X0) ) ) ).
fof(axiom_88,axiom,
cTOP(iV21026) ).
fof(axiom_89,axiom,
cTEST(iV21026) ).
fof(axiom_152,axiom,
rR1(iV21027,iV21036) ).
fof(axiom_153,axiom,
rR1(iV21027,iV21035) ).
fof(axiom_181,axiom,
rR1(iV21029,iV21034) ).
fof(axiom_182,axiom,
rR1(iV21029,iV21033) ).
fof(axiom_192,axiom,
~ cC74(iV21030) ).
fof(axiom_202,axiom,
~ cC18(iV21030) ).
fof(axiom_209,axiom,
rR1(iV21030,iV21032) ).
fof(axiom_214,axiom,
~ cC2(iV21032) ).
fof(axiom_222,axiom,
~ cC12(iV21033) ).
fof(axiom_228,axiom,
~ cC2(iV21034) ).
fof(axiom_232,axiom,
~ cC12(iV21035) ).
fof(axiom_240,axiom,
~ cC2(iV21036) ).
fof(the_axiom,conjecture,
( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [X0] :
( 'xsd$ustring'(X0)
<=> ~ 'xsd$uinteger'(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [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(c4,plain,
( cC8(X0)
| ~ cC10(X0) ),
inference(clausification,[status(esa)],[axiom_2]) ).
cnf(c5,plain,
( cC4(X0)
| ~ cC10(X0) ),
inference(clausification,[status(esa)],[axiom_2]) ).
cnf(c19,plain,
( cC108(X0)
| ~ cC110(X0) ),
inference(clausification,[status(esa)],[axiom_7]) ).
cnf(c22,plain,
( cC90(X0)
| ~ cC112(X0) ),
inference(clausification,[status(esa)],[axiom_8]) ).
cnf(c23,plain,
( cC110(X0)
| ~ cC112(X0) ),
inference(clausification,[status(esa)],[axiom_8]) ).
cnf(c26,plain,
( ~ cTOP(X0)
| cC114(X0) ),
inference(clausification,[status(esa)],[axiom_9]) ).
cnf(c28,plain,
( cC112(X0)
| ~ cC116(X0) ),
inference(clausification,[status(esa)],[axiom_10]) ).
cnf(c52,plain,
( cC130(X0)
| ~ cC132(X0) ),
inference(clausification,[status(esa)],[axiom_18]) ).
cnf(c54,plain,
( cC132(X0)
| ~ cC134(X0) ),
inference(clausification,[status(esa)],[axiom_19]) ).
cnf(c55,plain,
( cC116(X0)
| ~ cC134(X0) ),
inference(clausification,[status(esa)],[axiom_19]) ).
cnf(c58,plain,
( ~ cTOP(X0)
| cC136(X0) ),
inference(clausification,[status(esa)],[axiom_20]) ).
cnf(c60,plain,
( cC134(X0)
| ~ cC138(X0) ),
inference(clausification,[status(esa)],[axiom_21]) ).
cnf(c87,plain,
( cC152(X0)
| ~ cC154(X0) ),
inference(clausification,[status(esa)],[axiom_30]) ).
cnf(c89,plain,
( cC154(X0)
| ~ cC156(X0) ),
inference(clausification,[status(esa)],[axiom_31]) ).
cnf(c90,plain,
( cC138(X0)
| ~ cC156(X0) ),
inference(clausification,[status(esa)],[axiom_31]) ).
cnf(c92,plain,
( cC22(X0)
| ~ cC158(X0) ),
inference(clausification,[status(esa)],[axiom_32]) ).
cnf(c93,plain,
( cC156(X0)
| ~ cC158(X0) ),
inference(clausification,[status(esa)],[axiom_32]) ).
cnf(c95,plain,
( cC14(X0)
| ~ cC16(X0) ),
inference(clausification,[status(esa)],[axiom_33]) ).
cnf(c96,plain,
( cC10(X0)
| ~ cC16(X0) ),
inference(clausification,[status(esa)],[axiom_33]) ).
cnf(c119,plain,
( cC168(X0)
| ~ cC174(X0) ),
inference(clausification,[status(esa)],[axiom_41]) ).
cnf(c129,plain,
( cC174(X0)
| ~ cC180(X0) ),
inference(clausification,[status(esa)],[axiom_44]) ).
cnf(c134,plain,
( cC16(X0)
| ~ cC22(X0) ),
inference(clausification,[status(esa)],[axiom_46]) ).
cnf(c135,plain,
( cC20(X0)
| ~ cC22(X0) ),
inference(clausification,[status(esa)],[axiom_46]) ).
cnf(c139,plain,
( cC2(X1)
| ~ rR1(X0,X1)
| cC24(X0) ),
inference(clausification,[status(esa)],[axiom_47]) ).
cnf(c148,plain,
( cC12(X1)
| ~ rR1(X0,X1)
| cC30(X0) ),
inference(clausification,[status(esa)],[axiom_50]) ).
cnf(c158,plain,
( cC36(X0)
| ~ cC38(X0) ),
inference(clausification,[status(esa)],[axiom_54]) ).
cnf(c165,plain,
( ~ cTOP(X0)
| cC40(X0) ),
inference(clausification,[status(esa)],[axiom_56]) ).
cnf(c167,plain,
( cC38(X0)
| ~ cC42(X0) ),
inference(clausification,[status(esa)],[axiom_57]) ).
cnf(c171,plain,
( cC2(X1)
| ~ rR1(X0,X1)
| cC44(X0) ),
inference(clausification,[status(esa)],[axiom_58]) ).
cnf(c180,plain,
( cC12(X1)
| ~ rR1(X0,X1)
| cC50(X0) ),
inference(clausification,[status(esa)],[axiom_61]) ).
cnf(c190,plain,
( cC56(X0)
| ~ cC58(X0) ),
inference(clausification,[status(esa)],[axiom_65]) ).
cnf(c193,plain,
( cC58(X0)
| ~ cC60(X0) ),
inference(clausification,[status(esa)],[axiom_66]) ).
cnf(c194,plain,
( cC42(X0)
| ~ cC60(X0) ),
inference(clausification,[status(esa)],[axiom_66]) ).
cnf(c197,plain,
( ~ cTOP(X0)
| cC62(X0) ),
inference(clausification,[status(esa)],[axiom_67]) ).
cnf(c199,plain,
( cC60(X0)
| ~ cC64(X0) ),
inference(clausification,[status(esa)],[axiom_68]) ).
cnf(c203,plain,
( cC2(X1)
| ~ rR1(X0,X1)
| cC66(X0) ),
inference(clausification,[status(esa)],[axiom_69]) ).
cnf(c215,plain,
( cC72(X0)
| cC18(X0)
| cC74(X0) ),
inference(clausification,[status(esa)],[axiom_73]) ).
cnf(c226,plain,
( cC78(X0)
| ~ cC80(X0) ),
inference(clausification,[status(esa)],[axiom_77]) ).
cnf(c228,plain,
( cC80(X0)
| ~ cC82(X0) ),
inference(clausification,[status(esa)],[axiom_78]) ).
cnf(c229,plain,
( cC64(X0)
| ~ cC82(X0) ),
inference(clausification,[status(esa)],[axiom_78]) ).
cnf(c232,plain,
( ~ cTOP(X0)
| cC84(X0) ),
inference(clausification,[status(esa)],[axiom_79]) ).
cnf(c233,plain,
( cC82(X0)
| ~ cC86(X0) ),
inference(clausification,[status(esa)],[axiom_80]) ).
cnf(c237,plain,
( ~ cTOP(X0)
| cC88(X0) ),
inference(clausification,[status(esa)],[axiom_81]) ).
cnf(c239,plain,
( cC86(X0)
| ~ cC90(X0) ),
inference(clausification,[status(esa)],[axiom_82]) ).
cnf(c250,plain,
( cC158(X0)
| ~ cTEST(X0) ),
inference(clausification,[status(esa)],[axiom_86]) ).
cnf(c251,plain,
( cC180(X0)
| ~ cTEST(X0) ),
inference(clausification,[status(esa)],[axiom_86]) ).
cnf(c254,plain,
cTOP(iV21026),
inference(clausification,[status(esa)],[axiom_88]) ).
cnf(c255,plain,
cTEST(iV21026),
inference(clausification,[status(esa)],[axiom_89]) ).
cnf(c318,plain,
rR1(iV21027,iV21036),
inference(clausification,[status(esa)],[axiom_152]) ).
cnf(c319,plain,
rR1(iV21027,iV21035),
inference(clausification,[status(esa)],[axiom_153]) ).
cnf(c347,plain,
rR1(iV21029,iV21034),
inference(clausification,[status(esa)],[axiom_181]) ).
cnf(c348,plain,
rR1(iV21029,iV21033),
inference(clausification,[status(esa)],[axiom_182]) ).
cnf(c358,plain,
~ cC74(iV21030),
inference(clausification,[status(esa)],[axiom_192]) ).
cnf(c368,plain,
~ cC18(iV21030),
inference(clausification,[status(esa)],[axiom_202]) ).
cnf(c375,plain,
rR1(iV21030,iV21032),
inference(clausification,[status(esa)],[axiom_209]) ).
cnf(c380,plain,
~ cC2(iV21032),
inference(clausification,[status(esa)],[axiom_214]) ).
cnf(c388,plain,
~ cC12(iV21033),
inference(clausification,[status(esa)],[axiom_222]) ).
cnf(c394,plain,
~ cC2(iV21034),
inference(clausification,[status(esa)],[axiom_228]) ).
cnf(c398,plain,
~ cC12(iV21035),
inference(clausification,[status(esa)],[axiom_232]) ).
cnf(c406,plain,
~ cC2(iV21036),
inference(clausification,[status(esa)],[axiom_240]) ).
cnf(c409,plain,
( 'xsd$ustring'(sK188)
| ~ cC86(iV21026)
| ~ cC20(iV21026)
| ~ cowlThing(iV21026)
| ~ cC136(iV21026)
| ~ cC154(iV21026)
| ~ cC10(iV21026)
| cowlNothing(sK187)
| ~ cowlThing(iV21030)
| ~ cC4(iV21026)
| ~ cC180(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC66(iV21030)
| ~ cC134(iV21026)
| ~ 'xsd$uinteger'(sK188)
| ~ cC72(iV21030)
| ~ cC112(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC58(iV21026)
| ~ cC64(iV21026)
| ~ cC156(iV21026)
| ~ cC168(iV21026)
| ~ cC108(iV21026)
| ~ cowlThing(sK187)
| ~ cC40(iV21026)
| ~ cC60(iV21026)
| ~ cC116(iV21026)
| ~ cC56(iV21026)
| ~ cC152(iV21026)
| ~ cC110(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC38(iV21026)
| ~ cC174(iV21026)
| ~ cC22(iV21026)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cowlThing(iV21027)
| ~ cC36(iV21026)
| ~ cC62(iV21026)
| ~ cC84(iV21026)
| ~ cC138(iV21026)
| ~ cC130(iV21026)
| ~ cC50(iV21029)
| ~ cC14(iV21026)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cowlThing(iV21029)
| ~ cC78(iV21026)
| ~ cC82(iV21026)
| ~ cC132(iV21026)
| ~ cC158(iV21026) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c410,plain,
( ~ cC20(iV21026)
| ~ cowlThing(iV21026)
| ~ cC136(iV21026)
| ~ cC154(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| ~ cC84(iV21026)
| cowlNothing(sK187)
| ~ cowlThing(iV21030)
| ~ cC4(iV21026)
| ~ cC180(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC66(iV21030)
| ~ cC134(iV21026)
| ~ cC72(iV21030)
| ~ cC112(iV21026)
| 'xsd$uinteger'(sK188)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC58(iV21026)
| ~ cC64(iV21026)
| ~ cC156(iV21026)
| ~ cC168(iV21026)
| ~ cC108(iV21026)
| ~ cowlThing(sK187)
| ~ cC40(iV21026)
| ~ cC60(iV21026)
| ~ cC116(iV21026)
| ~ cC56(iV21026)
| ~ cC152(iV21026)
| ~ cC110(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC38(iV21026)
| ~ cC174(iV21026)
| ~ cC22(iV21026)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cowlThing(iV21027)
| ~ cC36(iV21026)
| ~ cC62(iV21026)
| ~ cC86(iV21026)
| ~ cC138(iV21026)
| ~ cC130(iV21026)
| ~ cC50(iV21029)
| ~ cC14(iV21026)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cowlThing(iV21029)
| ~ cC78(iV21026)
| ~ cC82(iV21026)
| ~ cC132(iV21026)
| ~ cC158(iV21026) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| cowlNothing(sK187)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[c0,c409]) ).
cnf(d1,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[c1,d0]) ).
cnf(d2,plain,
cC114(iV21026),
inference(resolution,[status(thm)],[c26,c254]) ).
cnf(d3,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
cC136(iV21026),
inference(resolution,[status(thm)],[c58,c254]) ).
cnf(d5,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
cC40(iV21026),
inference(resolution,[status(thm)],[c165,c254]) ).
cnf(d7,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d6,d5]) ).
cnf(d8,plain,
cC62(iV21026),
inference(resolution,[status(thm)],[c197,c254]) ).
cnf(d9,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d8,d7]) ).
cnf(d10,plain,
cC84(iV21026),
inference(resolution,[status(thm)],[c232,c254]) ).
cnf(d11,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
cC88(iV21026),
inference(resolution,[status(thm)],[c237,c254]) ).
cnf(d13,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d12,d11]) ).
cnf(d14,plain,
cC158(iV21026),
inference(resolution,[status(thm)],[c250,c255]) ).
cnf(d15,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d14,d13]) ).
cnf(d16,plain,
cC156(iV21026),
inference(resolution,[status(thm)],[d14,c93]) ).
cnf(d17,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d16,d15]) ).
cnf(d18,plain,
cC22(iV21026),
inference(resolution,[status(thm)],[d14,c92]) ).
cnf(d19,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d18,d17]) ).
cnf(d20,plain,
cC154(iV21026),
inference(resolution,[status(thm)],[d16,c89]) ).
cnf(d21,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d20,d19]) ).
cnf(d22,plain,
cC138(iV21026),
inference(resolution,[status(thm)],[d16,c90]) ).
cnf(d23,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d22,d21]) ).
cnf(d24,plain,
cC20(iV21026),
inference(resolution,[status(thm)],[d18,c135]) ).
cnf(d25,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d24,d23]) ).
cnf(d26,plain,
cC16(iV21026),
inference(resolution,[status(thm)],[d18,c134]) ).
cnf(d27,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d26,d25]) ).
cnf(d28,plain,
cC152(iV21026),
inference(resolution,[status(thm)],[d20,c87]) ).
cnf(d29,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d28,d27]) ).
cnf(d30,plain,
cC134(iV21026),
inference(resolution,[status(thm)],[d22,c60]) ).
cnf(d31,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC14(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d30,d29]) ).
cnf(d32,plain,
cC14(iV21026),
inference(resolution,[status(thm)],[d26,c95]) ).
cnf(d33,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d32,d31]) ).
cnf(d34,plain,
cC10(iV21026),
inference(resolution,[status(thm)],[d26,c96]) ).
cnf(d35,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d34,d33]) ).
cnf(d36,plain,
cC116(iV21026),
inference(resolution,[status(thm)],[d30,c55]) ).
cnf(d37,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d36,d35]) ).
cnf(d38,plain,
cC132(iV21026),
inference(resolution,[status(thm)],[d30,c54]) ).
cnf(d39,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d38,d37]) ).
cnf(d40,plain,
cC8(iV21026),
inference(resolution,[status(thm)],[d34,c4]) ).
cnf(d41,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d40,d39]) ).
cnf(d42,plain,
cC4(iV21026),
inference(resolution,[status(thm)],[d34,c5]) ).
cnf(d43,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d42,d41]) ).
cnf(d44,plain,
cC112(iV21026),
inference(resolution,[status(thm)],[d36,c28]) ).
cnf(d45,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d44,d43]) ).
cnf(d46,plain,
cC130(iV21026),
inference(resolution,[status(thm)],[d38,c52]) ).
cnf(d47,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC90(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d46,d45]) ).
cnf(d48,plain,
cC110(iV21026),
inference(resolution,[status(thm)],[d44,c23]) ).
cnf(d49,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC90(iV21026)
| ~ cC108(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d48,d47]) ).
cnf(d50,plain,
cC90(iV21026),
inference(resolution,[status(thm)],[d44,c22]) ).
cnf(d51,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC108(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d50,d49]) ).
cnf(d52,plain,
cC180(iV21026),
inference(resolution,[status(thm)],[c251,c255]) ).
cnf(d53,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC108(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d52,d51]) ).
cnf(d54,plain,
cC108(iV21026),
inference(resolution,[status(thm)],[d48,c19]) ).
cnf(d55,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d54,d53]) ).
cnf(d56,plain,
cC86(iV21026),
inference(resolution,[status(thm)],[d50,c239]) ).
cnf(d57,plain,
( ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d56,d55]) ).
cnf(d58,plain,
cC174(iV21026),
inference(resolution,[status(thm)],[d52,c129]) ).
cnf(d59,plain,
( ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC168(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d58,d57]) ).
cnf(d60,plain,
cC82(iV21026),
inference(resolution,[status(thm)],[d56,c233]) ).
cnf(d61,plain,
( ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC168(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d60,d59]) ).
cnf(d62,plain,
( ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC168(iV21026)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[c0,d61]) ).
cnf(d63,plain,
cC168(iV21026),
inference(resolution,[status(thm)],[d58,c119]) ).
cnf(d64,plain,
( ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d63,d62]) ).
cnf(d65,plain,
cC80(iV21026),
inference(resolution,[status(thm)],[d60,c228]) ).
cnf(d66,plain,
( ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d65,d64]) ).
cnf(d67,plain,
cC64(iV21026),
inference(resolution,[status(thm)],[d60,c229]) ).
cnf(d68,plain,
( ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d67,d66]) ).
cnf(d69,plain,
cC78(iV21026),
inference(resolution,[status(thm)],[d65,c226]) ).
cnf(d70,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d69,d68]) ).
cnf(d71,plain,
cC60(iV21026),
inference(resolution,[status(thm)],[d67,c199]) ).
cnf(d72,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d71,d70]) ).
cnf(d73,plain,
cC42(iV21026),
inference(resolution,[status(thm)],[d71,c194]) ).
cnf(d74,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d73,d72]) ).
cnf(d75,plain,
cC58(iV21026),
inference(resolution,[status(thm)],[d71,c193]) ).
cnf(d76,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d75,d74]) ).
cnf(d77,plain,
cC38(iV21026),
inference(resolution,[status(thm)],[d73,c167]) ).
cnf(d78,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d77,d76]) ).
cnf(d79,plain,
cC56(iV21026),
inference(resolution,[status(thm)],[d75,c190]) ).
cnf(d80,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d79,d78]) ).
cnf(d81,plain,
cC36(iV21026),
inference(resolution,[status(thm)],[d77,c158]) ).
cnf(d82,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d81,d80]) ).
cnf(d83,plain,
( cC2(iV21036)
| cC24(iV21027) ),
inference(resolution,[status(thm)],[c139,c318]) ).
cnf(d84,plain,
cC24(iV21027),
inference(resolution,[status(thm)],[c406,d83]) ).
cnf(d85,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d84,d82]) ).
cnf(d86,plain,
( cC30(iV21027)
| cC12(iV21035) ),
inference(resolution,[status(thm)],[c148,c319]) ).
cnf(d87,plain,
cC30(iV21027),
inference(resolution,[status(thm)],[c398,d86]) ).
cnf(d88,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d87,d85]) ).
cnf(d89,plain,
( cC44(iV21029)
| cC2(iV21034) ),
inference(resolution,[status(thm)],[c171,c347]) ).
cnf(d90,plain,
cC44(iV21029),
inference(resolution,[status(thm)],[c394,d89]) ).
cnf(d91,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d90,d88]) ).
cnf(d92,plain,
( cC50(iV21029)
| cC12(iV21033) ),
inference(resolution,[status(thm)],[c180,c348]) ).
cnf(d93,plain,
cC50(iV21029),
inference(resolution,[status(thm)],[c388,d92]) ).
cnf(d94,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d93,d91]) ).
cnf(d95,plain,
( cC66(iV21030)
| cC2(iV21032) ),
inference(resolution,[status(thm)],[c203,c375]) ).
cnf(d96,plain,
cC66(iV21030),
inference(resolution,[status(thm)],[c380,d95]) ).
cnf(d97,plain,
( ~ cC72(iV21030)
| 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d96,d94]) ).
cnf(d98,plain,
( cC72(iV21030)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[c215,c358]) ).
cnf(d99,plain,
cC72(iV21030),
inference(resolution,[status(thm)],[c368,d98]) ).
cnf(d100,plain,
( 'xsd$ustring'(sK188)
| ~ 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d99,d97]) ).
cnf(d101,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| cowlNothing(sK187)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[c0,c410]) ).
cnf(d102,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[c1,d101]) ).
cnf(d103,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d2,d102]) ).
cnf(d104,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d4,d103]) ).
cnf(d105,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d6,d104]) ).
cnf(d106,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d8,d105]) ).
cnf(d107,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d10,d106]) ).
cnf(d108,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d12,d107]) ).
cnf(d109,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d14,d108]) ).
cnf(d110,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d16,d109]) ).
cnf(d111,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d18,d110]) ).
cnf(d112,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d20,d111]) ).
cnf(d113,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d22,d112]) ).
cnf(d114,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d24,d113]) ).
cnf(d115,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d26,d114]) ).
cnf(d116,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC14(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d28,d115]) ).
cnf(d117,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC14(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d30,d116]) ).
cnf(d118,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d32,d117]) ).
cnf(d119,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d34,d118]) ).
cnf(d120,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d36,d119]) ).
cnf(d121,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d38,d120]) ).
cnf(d122,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d40,d121]) ).
cnf(d123,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d42,d122]) ).
cnf(d124,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC90(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d44,d123]) ).
cnf(d125,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC90(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d46,d124]) ).
cnf(d126,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC90(iV21026)
| ~ cC108(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d48,d125]) ).
cnf(d127,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC108(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d50,d126]) ).
cnf(d128,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC108(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d52,d127]) ).
cnf(d129,plain,
( ~ cC86(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d54,d128]) ).
cnf(d130,plain,
( ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d56,d129]) ).
cnf(d131,plain,
( ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC168(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d58,d130]) ).
cnf(d132,plain,
( ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC168(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030) ),
inference(resolution,[status(thm)],[d60,d131]) ).
cnf(d133,plain,
( ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC168(iV21026)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[c0,d132]) ).
cnf(d134,plain,
( ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d63,d133]) ).
cnf(d135,plain,
( ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d65,d134]) ).
cnf(d136,plain,
( ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d67,d135]) ).
cnf(d137,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d69,d136]) ).
cnf(d138,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d71,d137]) ).
cnf(d139,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d73,d138]) ).
cnf(d140,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d75,d139]) ).
cnf(d141,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d77,d140]) ).
cnf(d142,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d79,d141]) ).
cnf(d143,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d81,d142]) ).
cnf(d144,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d84,d143]) ).
cnf(d145,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d87,d144]) ).
cnf(d146,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d90,d145]) ).
cnf(d147,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d93,d146]) ).
cnf(d148,plain,
( ~ cC72(iV21030)
| ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d96,d147]) ).
cnf(d149,plain,
( ~ 'xsd$ustring'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d99,d148]) ).
cnf(d150,plain,
( 'xsd$uinteger'(sK188)
| 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d149,c3]) ).
cnf(d151,plain,
( 'xsd$uinteger'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029) ),
inference(resolution,[status(thm)],[c0,d150]) ).
cnf(d152,plain,
( 'xsd$uinteger'(sK188)
| ~ cowlThing(iV21029) ),
inference(resolution,[status(thm)],[d151,c0]) ).
cnf(d153,plain,
'xsd$uinteger'(sK188),
inference(resolution,[status(thm)],[c0,d152]) ).
cnf(d154,plain,
( 'xsd$ustring'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027) ),
inference(resolution,[status(thm)],[d153,d100]) ).
cnf(d155,plain,
( 'xsd$ustring'(sK188)
| ~ cowlThing(sK187)
| ~ cowlThing(iV21029) ),
inference(resolution,[status(thm)],[c0,d154]) ).
cnf(d156,plain,
( 'xsd$ustring'(sK188)
| ~ cowlThing(iV21029) ),
inference(resolution,[status(thm)],[d155,c0]) ).
cnf(d157,plain,
'xsd$ustring'(sK188),
inference(resolution,[status(thm)],[c0,d156]) ).
cnf(d158,plain,
~ 'xsd$uinteger'(sK188),
inference(resolution,[status(thm)],[d157,c2]) ).
cnf(d159,plain,
$false,
inference(resolution,[status(thm)],[d153,d158]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.52 % Computer : n026.cluster.edu
% 0.11/0.52 % Model : x86_64 x86_64
% 0.11/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.52 % Memory : 8046.5625MB
% 0.11/0.52 % OS : Linux 6.8.0-71-generic
% 0.11/0.52 % CPULimit : 300
% 0.11/0.52 % WCLimit : 300
% 0.11/0.52 % DateTime : Fri Sep 25 19:44:27 UTC 2026
% 0.11/0.52 % CPUTime :
% 0.11/0.52 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.67/3.29 % SZS status Theorem for theBenchmark.p
% 20.67/3.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------