%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.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 : Fri Sep 25 01:54:17 PM UTC 2026
% Result : Theorem 2.71s 1.29s
% Output : CNFRefutation 2.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 52
% Syntax : Number of formulae : 318 ( 50 unt; 0 def)
% Number of atoms : 1468 ( 0 equ)
% Maximal formula atoms : 56 ( 4 avg)
% Number of connectives : 1961 ( 811 ~; 798 |; 312 &)
% ( 38 <=>; 1 =>; 0 <=; 1 <~>)
% Maximal formula depth : 55 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 64 ( 63 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 215 ( 0 sgn 211 !; 4 ?; 54 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f3,axiom,
! [X0] :
( cC10(X0)
<=> ( cC4(X0)
& cC8(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(f8,axiom,
! [X0] :
( cC110(X0)
<=> ( cTOP(X0)
& cC108(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
fof(f9,axiom,
! [X0] :
( cC112(X0)
<=> ( cC110(X0)
& cC90(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
fof(f11,axiom,
! [X0] :
( cC116(X0)
<=> ( cC112(X0)
& cC114(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_10) ).
fof(f19,axiom,
! [X0] :
( cC132(X0)
<=> ( cC130(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f20,axiom,
! [X0] :
( cC134(X0)
<=> ( cC116(X0)
& cC132(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_19) ).
fof(f22,axiom,
! [X0] :
( cC138(X0)
<=> ( cC134(X0)
& cC136(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
fof(f31,axiom,
! [X0] :
( cC154(X0)
<=> ( cC152(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f32,axiom,
! [X0] :
( cC156(X0)
<=> ( cC138(X0)
& cC154(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_31) ).
fof(f33,axiom,
! [X0] :
( cC158(X0)
<=> ( cC156(X0)
& cC22(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_32) ).
fof(f34,axiom,
! [X0] :
( cC16(X0)
<=> ( cC10(X0)
& cC14(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_33) ).
fof(f42,axiom,
! [X0] :
( cC174(X0)
<=> ( ~ cC172(X0)
& cC168(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
fof(f45,axiom,
! [X0] :
( cC180(X0)
<=> ( cC174(X0)
& ~ cC178(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_44) ).
fof(f47,axiom,
! [X0] :
( cC22(X0)
<=> ( cC20(X0)
& cC16(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_46) ).
fof(f49,axiom,
! [X0] :
( cC26(X0)
<=> ( ~ cC2(X0)
& ~ cC24(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_48) ).
fof(f52,axiom,
! [X0] :
( cC32(X0)
<=> ( ~ cC30(X0)
& ~ cC2(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_51) ).
fof(f55,axiom,
! [X0] :
( cC38(X0)
<=> ( cTOP(X0)
& cC36(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_54) ).
fof(f57,axiom,
! [X0] :
( cC40(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_56) ).
fof(f58,axiom,
! [X0] :
( cC42(X0)
<=> ( cC38(X0)
& cC40(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
fof(f60,axiom,
! [X0] :
( cC46(X0)
<=> ( ~ cC44(X0)
& ~ cC12(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_59) ).
fof(f63,axiom,
! [X0] :
( cC52(X0)
<=> ( ~ cC50(X0)
& ~ cC12(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_62) ).
fof(f66,axiom,
! [X0] :
( cC58(X0)
<=> ( cTOP(X0)
& cC56(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(f67,axiom,
! [X0] :
( cC60(X0)
<=> ( cC42(X0)
& cC58(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(f68,axiom,
! [X0] :
( cC62(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(f69,axiom,
! [X0] :
( cC64(X0)
<=> ( cC60(X0)
& cC62(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_68) ).
fof(f71,axiom,
! [X0] :
( cC68(X0)
<=> ( ~ cC18(X0)
& ~ cC66(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_70) ).
fof(f74,axiom,
! [X0] :
( cC74(X0)
<=> ( ~ cC72(X0)
& ~ cC18(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_73) ).
fof(f78,axiom,
! [X0] :
( cC80(X0)
<=> ( cC78(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_77) ).
fof(f79,axiom,
! [X0] :
( cC82(X0)
<=> ( cC64(X0)
& cC80(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_78) ).
fof(f80,axiom,
! [X0] :
( cC84(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_79) ).
fof(f81,axiom,
! [X0] :
( cC86(X0)
<=> ( cC84(X0)
& cC82(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_80) ).
fof(f82,axiom,
! [X0] :
( cC88(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_81) ).
fof(f83,axiom,
! [X0] :
( cC90(X0)
<=> ( cC86(X0)
& cC88(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_82) ).
fof(f87,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC180(X0)
& cC158(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_86) ).
fof(f89,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_88) ).
fof(f90,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_89) ).
fof(f121,axiom,
cowlThing(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f127,axiom,
~ cC26(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_126) ).
fof(f137,axiom,
~ cC32(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_136) ).
fof(f151,axiom,
~ cC2(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_150) ).
fof(f152,axiom,
cowlThing(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_151) ).
fof(f158,axiom,
~ cC46(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_157) ).
fof(f164,axiom,
~ cC12(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(f169,axiom,
~ cC52(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_168) ).
fof(f181,axiom,
cowlThing(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_180) ).
fof(f192,axiom,
~ cC68(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_191) ).
fof(f193,axiom,
~ cC74(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_192) ).
fof(f203,axiom,
~ cC18(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_202) ).
fof(f208,axiom,
cowlThing(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_207) ).
fof(f243,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_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f244,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_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(negated_conjecture,[status(cth)],[f243]) ).
fof(f245,plain,
~ ( 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)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(rectify,[],[f244]) ).
fof(f246,plain,
! [X0] :
( cTEST(X0)
=> ( cC180(X0)
& cC158(X0) ) ),
inference(unused_predicate_definition_removal,[],[f87]) ).
fof(f247,plain,
! [X0] :
( ~ cTEST(X0)
| ( cC180(X0)
& cC158(X0) ) ),
inference(ennf_transformation,[],[f246]) ).
fof(f276,plain,
( ~ 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)
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(ennf_transformation,[],[f245]) ).
fof(f277,plain,
! [X0] :
( ( ~ xsd_string(X0)
| ~ xsd_integer(X0) )
& ( xsd_integer(X0)
| xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f278,plain,
! [X0] :
( ( ~ cC10(X0)
| ( cC4(X0)
& cC8(X0) ) )
& ( ~ cC4(X0)
| ~ cC8(X0)
| cC10(X0) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f279,plain,
! [X0] :
( ( ~ cC10(X0)
| ( cC4(X0)
& cC8(X0) ) )
& ( ~ cC4(X0)
| ~ cC8(X0)
| cC10(X0) ) ),
inference(flattening,[],[f278]) ).
fof(f290,plain,
! [X0] :
( ( ~ cC110(X0)
| ( cTOP(X0)
& cC108(X0) ) )
& ( ~ cTOP(X0)
| ~ cC108(X0)
| cC110(X0) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f291,plain,
! [X0] :
( ( ~ cC110(X0)
| ( cTOP(X0)
& cC108(X0) ) )
& ( ~ cTOP(X0)
| ~ cC108(X0)
| cC110(X0) ) ),
inference(flattening,[],[f290]) ).
fof(f292,plain,
! [X0] :
( ( ~ cC112(X0)
| ( cC110(X0)
& cC90(X0) ) )
& ( ~ cC110(X0)
| ~ cC90(X0)
| cC112(X0) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f293,plain,
! [X0] :
( ( ~ cC112(X0)
| ( cC110(X0)
& cC90(X0) ) )
& ( ~ cC110(X0)
| ~ cC90(X0)
| cC112(X0) ) ),
inference(flattening,[],[f292]) ).
fof(f295,plain,
! [X0] :
( ( ~ cC116(X0)
| ( cC112(X0)
& cC114(X0) ) )
& ( ~ cC112(X0)
| ~ cC114(X0)
| cC116(X0) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f296,plain,
! [X0] :
( ( ~ cC116(X0)
| ( cC112(X0)
& cC114(X0) ) )
& ( ~ cC112(X0)
| ~ cC114(X0)
| cC116(X0) ) ),
inference(flattening,[],[f295]) ).
fof(f315,plain,
! [X0] :
( ( ~ cC132(X0)
| ( cC130(X0)
& cTOP(X0) ) )
& ( ~ cC130(X0)
| ~ cTOP(X0)
| cC132(X0) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f316,plain,
! [X0] :
( ( ~ cC132(X0)
| ( cC130(X0)
& cTOP(X0) ) )
& ( ~ cC130(X0)
| ~ cTOP(X0)
| cC132(X0) ) ),
inference(flattening,[],[f315]) ).
fof(f317,plain,
! [X0] :
( ( ~ cC134(X0)
| ( cC116(X0)
& cC132(X0) ) )
& ( ~ cC116(X0)
| ~ cC132(X0)
| cC134(X0) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f318,plain,
! [X0] :
( ( ~ cC134(X0)
| ( cC116(X0)
& cC132(X0) ) )
& ( ~ cC116(X0)
| ~ cC132(X0)
| cC134(X0) ) ),
inference(flattening,[],[f317]) ).
fof(f320,plain,
! [X0] :
( ( ~ cC138(X0)
| ( cC134(X0)
& cC136(X0) ) )
& ( ~ cC134(X0)
| ~ cC136(X0)
| cC138(X0) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f321,plain,
! [X0] :
( ( ~ cC138(X0)
| ( cC134(X0)
& cC136(X0) ) )
& ( ~ cC134(X0)
| ~ cC136(X0)
| cC138(X0) ) ),
inference(flattening,[],[f320]) ).
fof(f343,plain,
! [X0] :
( ( ~ cC154(X0)
| ( cC152(X0)
& cTOP(X0) ) )
& ( ~ cC152(X0)
| ~ cTOP(X0)
| cC154(X0) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f344,plain,
! [X0] :
( ( ~ cC154(X0)
| ( cC152(X0)
& cTOP(X0) ) )
& ( ~ cC152(X0)
| ~ cTOP(X0)
| cC154(X0) ) ),
inference(flattening,[],[f343]) ).
fof(f345,plain,
! [X0] :
( ( ~ cC156(X0)
| ( cC138(X0)
& cC154(X0) ) )
& ( ~ cC138(X0)
| ~ cC154(X0)
| cC156(X0) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f346,plain,
! [X0] :
( ( ~ cC156(X0)
| ( cC138(X0)
& cC154(X0) ) )
& ( ~ cC138(X0)
| ~ cC154(X0)
| cC156(X0) ) ),
inference(flattening,[],[f345]) ).
fof(f347,plain,
! [X0] :
( ( ~ cC158(X0)
| ( cC156(X0)
& cC22(X0) ) )
& ( ~ cC156(X0)
| ~ cC22(X0)
| cC158(X0) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f348,plain,
! [X0] :
( ( ~ cC158(X0)
| ( cC156(X0)
& cC22(X0) ) )
& ( ~ cC156(X0)
| ~ cC22(X0)
| cC158(X0) ) ),
inference(flattening,[],[f347]) ).
fof(f349,plain,
! [X0] :
( ( ~ cC16(X0)
| ( cC10(X0)
& cC14(X0) ) )
& ( ~ cC10(X0)
| ~ cC14(X0)
| cC16(X0) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f350,plain,
! [X0] :
( ( ~ cC16(X0)
| ( cC10(X0)
& cC14(X0) ) )
& ( ~ cC10(X0)
| ~ cC14(X0)
| cC16(X0) ) ),
inference(flattening,[],[f349]) ).
fof(f371,plain,
! [X0] :
( ( ~ cC174(X0)
| ( ~ cC172(X0)
& cC168(X0) ) )
& ( cC172(X0)
| ~ cC168(X0)
| cC174(X0) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f372,plain,
! [X0] :
( ( ~ cC174(X0)
| ( ~ cC172(X0)
& cC168(X0) ) )
& ( cC172(X0)
| ~ cC168(X0)
| cC174(X0) ) ),
inference(flattening,[],[f371]) ).
fof(f379,plain,
! [X0] :
( ( ~ cC180(X0)
| ( cC174(X0)
& ~ cC178(X0) ) )
& ( ~ cC174(X0)
| cC178(X0)
| cC180(X0) ) ),
inference(nnf_transformation,[],[f45]) ).
fof(f380,plain,
! [X0] :
( ( ~ cC180(X0)
| ( cC174(X0)
& ~ cC178(X0) ) )
& ( ~ cC174(X0)
| cC178(X0)
| cC180(X0) ) ),
inference(flattening,[],[f379]) ).
fof(f384,plain,
! [X0] :
( ( ~ cC22(X0)
| ( cC20(X0)
& cC16(X0) ) )
& ( ~ cC20(X0)
| ~ cC16(X0)
| cC22(X0) ) ),
inference(nnf_transformation,[],[f47]) ).
fof(f385,plain,
! [X0] :
( ( ~ cC22(X0)
| ( cC20(X0)
& cC16(X0) ) )
& ( ~ cC20(X0)
| ~ cC16(X0)
| cC22(X0) ) ),
inference(flattening,[],[f384]) ).
fof(f389,plain,
! [X0] :
( ( ~ cC26(X0)
| ( ~ cC2(X0)
& ~ cC24(X0) ) )
& ( cC2(X0)
| cC24(X0)
| cC26(X0) ) ),
inference(nnf_transformation,[],[f49]) ).
fof(f390,plain,
! [X0] :
( ( ~ cC26(X0)
| ( ~ cC2(X0)
& ~ cC24(X0) ) )
& ( cC2(X0)
| cC24(X0)
| cC26(X0) ) ),
inference(flattening,[],[f389]) ).
fof(f397,plain,
! [X0] :
( ( ~ cC32(X0)
| ( ~ cC30(X0)
& ~ cC2(X0) ) )
& ( cC30(X0)
| cC2(X0)
| cC32(X0) ) ),
inference(nnf_transformation,[],[f52]) ).
fof(f398,plain,
! [X0] :
( ( ~ cC32(X0)
| ( ~ cC30(X0)
& ~ cC2(X0) ) )
& ( cC30(X0)
| cC2(X0)
| cC32(X0) ) ),
inference(flattening,[],[f397]) ).
fof(f404,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cTOP(X0)
& cC36(X0) ) )
& ( ~ cTOP(X0)
| ~ cC36(X0)
| cC38(X0) ) ),
inference(nnf_transformation,[],[f55]) ).
fof(f405,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cTOP(X0)
& cC36(X0) ) )
& ( ~ cTOP(X0)
| ~ cC36(X0)
| cC38(X0) ) ),
inference(flattening,[],[f404]) ).
fof(f409,plain,
! [X0] :
( ( ~ cC40(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC40(X0) ) ),
inference(nnf_transformation,[],[f57]) ).
fof(f410,plain,
! [X0] :
( ( ~ cC42(X0)
| ( cC38(X0)
& cC40(X0) ) )
& ( ~ cC38(X0)
| ~ cC40(X0)
| cC42(X0) ) ),
inference(nnf_transformation,[],[f58]) ).
fof(f411,plain,
! [X0] :
( ( ~ cC42(X0)
| ( cC38(X0)
& cC40(X0) ) )
& ( ~ cC38(X0)
| ~ cC40(X0)
| cC42(X0) ) ),
inference(flattening,[],[f410]) ).
fof(f415,plain,
! [X0] :
( ( ~ cC46(X0)
| ( ~ cC44(X0)
& ~ cC12(X0) ) )
& ( cC44(X0)
| cC12(X0)
| cC46(X0) ) ),
inference(nnf_transformation,[],[f60]) ).
fof(f416,plain,
! [X0] :
( ( ~ cC46(X0)
| ( ~ cC44(X0)
& ~ cC12(X0) ) )
& ( cC44(X0)
| cC12(X0)
| cC46(X0) ) ),
inference(flattening,[],[f415]) ).
fof(f423,plain,
! [X0] :
( ( ~ cC52(X0)
| ( ~ cC50(X0)
& ~ cC12(X0) ) )
& ( cC50(X0)
| cC12(X0)
| cC52(X0) ) ),
inference(nnf_transformation,[],[f63]) ).
fof(f424,plain,
! [X0] :
( ( ~ cC52(X0)
| ( ~ cC50(X0)
& ~ cC12(X0) ) )
& ( cC50(X0)
| cC12(X0)
| cC52(X0) ) ),
inference(flattening,[],[f423]) ).
fof(f430,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cTOP(X0)
& cC56(X0) ) )
& ( ~ cTOP(X0)
| ~ cC56(X0)
| cC58(X0) ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f431,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cTOP(X0)
& cC56(X0) ) )
& ( ~ cTOP(X0)
| ~ cC56(X0)
| cC58(X0) ) ),
inference(flattening,[],[f430]) ).
fof(f432,plain,
! [X0] :
( ( ~ cC60(X0)
| ( cC42(X0)
& cC58(X0) ) )
& ( ~ cC42(X0)
| ~ cC58(X0)
| cC60(X0) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f433,plain,
! [X0] :
( ( ~ cC60(X0)
| ( cC42(X0)
& cC58(X0) ) )
& ( ~ cC42(X0)
| ~ cC58(X0)
| cC60(X0) ) ),
inference(flattening,[],[f432]) ).
fof(f434,plain,
! [X0] :
( ( ~ cC62(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC62(X0) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f435,plain,
! [X0] :
( ( ~ cC64(X0)
| ( cC60(X0)
& cC62(X0) ) )
& ( ~ cC60(X0)
| ~ cC62(X0)
| cC64(X0) ) ),
inference(nnf_transformation,[],[f69]) ).
fof(f436,plain,
! [X0] :
( ( ~ cC64(X0)
| ( cC60(X0)
& cC62(X0) ) )
& ( ~ cC60(X0)
| ~ cC62(X0)
| cC64(X0) ) ),
inference(flattening,[],[f435]) ).
fof(f440,plain,
! [X0] :
( ( ~ cC68(X0)
| ( ~ cC18(X0)
& ~ cC66(X0) ) )
& ( cC18(X0)
| cC66(X0)
| cC68(X0) ) ),
inference(nnf_transformation,[],[f71]) ).
fof(f441,plain,
! [X0] :
( ( ~ cC68(X0)
| ( ~ cC18(X0)
& ~ cC66(X0) ) )
& ( cC18(X0)
| cC66(X0)
| cC68(X0) ) ),
inference(flattening,[],[f440]) ).
fof(f448,plain,
! [X0] :
( ( ~ cC74(X0)
| ( ~ cC72(X0)
& ~ cC18(X0) ) )
& ( cC72(X0)
| cC18(X0)
| cC74(X0) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f449,plain,
! [X0] :
( ( ~ cC74(X0)
| ( ~ cC72(X0)
& ~ cC18(X0) ) )
& ( cC72(X0)
| cC18(X0)
| cC74(X0) ) ),
inference(flattening,[],[f448]) ).
fof(f458,plain,
! [X0] :
( ( ~ cC80(X0)
| ( cC78(X0)
& cTOP(X0) ) )
& ( ~ cC78(X0)
| ~ cTOP(X0)
| cC80(X0) ) ),
inference(nnf_transformation,[],[f78]) ).
fof(f459,plain,
! [X0] :
( ( ~ cC80(X0)
| ( cC78(X0)
& cTOP(X0) ) )
& ( ~ cC78(X0)
| ~ cTOP(X0)
| cC80(X0) ) ),
inference(flattening,[],[f458]) ).
fof(f460,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC64(X0)
& cC80(X0) ) )
& ( ~ cC64(X0)
| ~ cC80(X0)
| cC82(X0) ) ),
inference(nnf_transformation,[],[f79]) ).
fof(f461,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC64(X0)
& cC80(X0) ) )
& ( ~ cC64(X0)
| ~ cC80(X0)
| cC82(X0) ) ),
inference(flattening,[],[f460]) ).
fof(f462,plain,
! [X0] :
( ( ~ cC84(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC84(X0) ) ),
inference(nnf_transformation,[],[f80]) ).
fof(f463,plain,
! [X0] :
( ( ~ cC86(X0)
| ( cC84(X0)
& cC82(X0) ) )
& ( ~ cC84(X0)
| ~ cC82(X0)
| cC86(X0) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f464,plain,
! [X0] :
( ( ~ cC86(X0)
| ( cC84(X0)
& cC82(X0) ) )
& ( ~ cC84(X0)
| ~ cC82(X0)
| cC86(X0) ) ),
inference(flattening,[],[f463]) ).
fof(f465,plain,
! [X0] :
( ( ~ cC88(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC88(X0) ) ),
inference(nnf_transformation,[],[f82]) ).
fof(f466,plain,
! [X0] :
( ( ~ cC90(X0)
| ( cC86(X0)
& cC88(X0) ) )
& ( ~ cC86(X0)
| ~ cC88(X0)
| cC90(X0) ) ),
inference(nnf_transformation,[],[f83]) ).
fof(f467,plain,
! [X0] :
( ( ~ cC90(X0)
| ( cC86(X0)
& cC88(X0) ) )
& ( ~ cC86(X0)
| ~ cC88(X0)
| cC90(X0) ) ),
inference(flattening,[],[f466]) ).
fof(f476,plain,
( ~ 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)
| ? [X1] :
( ( xsd_string(X1)
| ~ xsd_integer(X1) )
& ( ~ xsd_string(X1)
| xsd_integer(X1) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(nnf_transformation,[],[f276]) ).
fof(f477,plain,
( ~ 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)
| ( ( xsd_string(sK37)
| ~ xsd_integer(sK37) )
& ( ~ xsd_string(sK37)
| xsd_integer(sK37) ) )
| cowlNothing(sK36)
| ~ cowlThing(sK36) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X0,sK36),skolemize(X1,sK37)],[f476]) ).
fof(f478,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f479,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f480,plain,
! [X0] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f481,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f482,plain,
! [X0] :
( ~ cC10(X0)
| cC4(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f483,plain,
! [X0] :
( ~ cC10(X0)
| cC8(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f498,plain,
! [X0] :
( ~ cC110(X0)
| cC108(X0) ),
inference(cnf_transformation,[],[f291]) ).
fof(f500,plain,
! [X0] :
( ~ cC112(X0)
| cC110(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f501,plain,
! [X0] :
( ~ cC112(X0)
| cC90(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f505,plain,
! [X0] :
( ~ cC116(X0)
| cC112(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f506,plain,
! [X0] :
( ~ cC116(X0)
| cC114(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f529,plain,
! [X0] :
( ~ cC132(X0)
| cC130(X0) ),
inference(cnf_transformation,[],[f316]) ).
fof(f532,plain,
! [X0] :
( ~ cC134(X0)
| cC116(X0) ),
inference(cnf_transformation,[],[f318]) ).
fof(f533,plain,
! [X0] :
( ~ cC134(X0)
| cC132(X0) ),
inference(cnf_transformation,[],[f318]) ).
fof(f537,plain,
! [X0] :
( ~ cC138(X0)
| cC134(X0) ),
inference(cnf_transformation,[],[f321]) ).
fof(f538,plain,
! [X0] :
( ~ cC138(X0)
| cC136(X0) ),
inference(cnf_transformation,[],[f321]) ).
fof(f564,plain,
! [X0] :
( ~ cC154(X0)
| cC152(X0) ),
inference(cnf_transformation,[],[f344]) ).
fof(f567,plain,
! [X0] :
( ~ cC156(X0)
| cC138(X0) ),
inference(cnf_transformation,[],[f346]) ).
fof(f568,plain,
! [X0] :
( ~ cC156(X0)
| cC154(X0) ),
inference(cnf_transformation,[],[f346]) ).
fof(f570,plain,
! [X0] :
( ~ cC158(X0)
| cC156(X0) ),
inference(cnf_transformation,[],[f348]) ).
fof(f571,plain,
! [X0] :
( ~ cC158(X0)
| cC22(X0) ),
inference(cnf_transformation,[],[f348]) ).
fof(f573,plain,
! [X0] :
( ~ cC16(X0)
| cC10(X0) ),
inference(cnf_transformation,[],[f350]) ).
fof(f574,plain,
! [X0] :
( ~ cC16(X0)
| cC14(X0) ),
inference(cnf_transformation,[],[f350]) ).
fof(f598,plain,
! [X0] :
( ~ cC174(X0)
| cC168(X0) ),
inference(cnf_transformation,[],[f372]) ).
fof(f606,plain,
! [X0] :
( ~ cC180(X0)
| cC174(X0) ),
inference(cnf_transformation,[],[f380]) ).
fof(f612,plain,
! [X0] :
( ~ cC22(X0)
| cC20(X0) ),
inference(cnf_transformation,[],[f385]) ).
fof(f613,plain,
! [X0] :
( ~ cC22(X0)
| cC16(X0) ),
inference(cnf_transformation,[],[f385]) ).
fof(f620,plain,
! [X0] :
( cC2(X0)
| cC24(X0)
| cC26(X0) ),
inference(cnf_transformation,[],[f390]) ).
fof(f629,plain,
! [X0] :
( cC30(X0)
| cC2(X0)
| cC32(X0) ),
inference(cnf_transformation,[],[f398]) ).
fof(f637,plain,
! [X0] :
( ~ cC38(X0)
| cC36(X0) ),
inference(cnf_transformation,[],[f405]) ).
fof(f643,plain,
! [X0] :
( ~ cTOP(X0)
| cC40(X0) ),
inference(cnf_transformation,[],[f409]) ).
fof(f644,plain,
! [X0] :
( ~ cC42(X0)
| cC38(X0) ),
inference(cnf_transformation,[],[f411]) ).
fof(f652,plain,
! [X0] :
( cC44(X0)
| cC12(X0)
| cC46(X0) ),
inference(cnf_transformation,[],[f416]) ).
fof(f661,plain,
! [X0] :
( cC50(X0)
| cC12(X0)
| cC52(X0) ),
inference(cnf_transformation,[],[f424]) ).
fof(f669,plain,
! [X0] :
( ~ cC58(X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f431]) ).
fof(f671,plain,
! [X0] :
( ~ cC60(X0)
| cC42(X0) ),
inference(cnf_transformation,[],[f433]) ).
fof(f672,plain,
! [X0] :
( ~ cC60(X0)
| cC58(X0) ),
inference(cnf_transformation,[],[f433]) ).
fof(f675,plain,
! [X0] :
( ~ cTOP(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f434]) ).
fof(f676,plain,
! [X0] :
( ~ cC64(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f436]) ).
fof(f684,plain,
! [X0] :
( cC18(X0)
| cC66(X0)
| cC68(X0) ),
inference(cnf_transformation,[],[f441]) ).
fof(f693,plain,
! [X0] :
( cC72(X0)
| cC18(X0)
| cC74(X0) ),
inference(cnf_transformation,[],[f449]) ).
fof(f703,plain,
! [X0] :
( ~ cC80(X0)
| cC78(X0) ),
inference(cnf_transformation,[],[f459]) ).
fof(f706,plain,
! [X0] :
( ~ cC82(X0)
| cC64(X0) ),
inference(cnf_transformation,[],[f461]) ).
fof(f707,plain,
! [X0] :
( ~ cC82(X0)
| cC80(X0) ),
inference(cnf_transformation,[],[f461]) ).
fof(f710,plain,
! [X0] :
( ~ cTOP(X0)
| cC84(X0) ),
inference(cnf_transformation,[],[f462]) ).
fof(f712,plain,
! [X0] :
( ~ cC86(X0)
| cC82(X0) ),
inference(cnf_transformation,[],[f464]) ).
fof(f715,plain,
! [X0] :
( ~ cTOP(X0)
| cC88(X0) ),
inference(cnf_transformation,[],[f465]) ).
fof(f716,plain,
! [X0] :
( ~ cC90(X0)
| cC86(X0) ),
inference(cnf_transformation,[],[f467]) ).
fof(f728,plain,
! [X0] :
( ~ cTEST(X0)
| cC180(X0) ),
inference(cnf_transformation,[],[f247]) ).
fof(f729,plain,
! [X0] :
( ~ cTEST(X0)
| cC158(X0) ),
inference(cnf_transformation,[],[f247]) ).
fof(f731,plain,
cTOP(iV21026),
inference(cnf_transformation,[],[f89]) ).
fof(f732,plain,
cTEST(iV21026),
inference(cnf_transformation,[],[f90]) ).
fof(f763,plain,
cowlThing(iV21026),
inference(cnf_transformation,[],[f121]) ).
fof(f769,plain,
~ cC26(iV21027),
inference(cnf_transformation,[],[f127]) ).
fof(f779,plain,
~ cC32(iV21027),
inference(cnf_transformation,[],[f137]) ).
fof(f793,plain,
~ cC2(iV21027),
inference(cnf_transformation,[],[f151]) ).
fof(f794,plain,
cowlThing(iV21027),
inference(cnf_transformation,[],[f152]) ).
fof(f800,plain,
~ cC46(iV21029),
inference(cnf_transformation,[],[f158]) ).
fof(f806,plain,
~ cC12(iV21029),
inference(cnf_transformation,[],[f164]) ).
fof(f811,plain,
~ cC52(iV21029),
inference(cnf_transformation,[],[f169]) ).
fof(f823,plain,
cowlThing(iV21029),
inference(cnf_transformation,[],[f181]) ).
fof(f834,plain,
~ cC68(iV21030),
inference(cnf_transformation,[],[f192]) ).
fof(f835,plain,
~ cC74(iV21030),
inference(cnf_transformation,[],[f193]) ).
fof(f845,plain,
~ cC18(iV21030),
inference(cnf_transformation,[],[f203]) ).
fof(f850,plain,
cowlThing(iV21030),
inference(cnf_transformation,[],[f208]) ).
fof(f885,plain,
( ~ 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)
| xsd_string(sK37)
| ~ xsd_integer(sK37)
| cowlNothing(sK36)
| ~ cowlThing(sK36) ),
inference(cnf_transformation,[],[f477]) ).
fof(f886,plain,
( ~ 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)
| ~ xsd_string(sK37)
| xsd_integer(sK37)
| cowlNothing(sK36)
| ~ cowlThing(sK36) ),
inference(cnf_transformation,[],[f477]) ).
tcf(c_49,plain,
! [X0: $i] : cowlThing(X0),
inference(cnf_transformation,[],[f479]) ).
tcf(c_50,plain,
! [X0: $i] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f478]) ).
tcf(c_51,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f481]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f480]) ).
tcf(c_54,plain,
! [X0: $i] :
( cC8(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[],[f483]) ).
tcf(c_55,plain,
! [X0: $i] :
( cC4(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_69,plain,
! [X0: $i] :
( cC108(X0)
| ~ cC110(X0) ),
inference(cnf_transformation,[],[f498]) ).
tcf(c_72,plain,
! [X0: $i] :
( cC90(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_73,plain,
! [X0: $i] :
( cC110(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[],[f500]) ).
tcf(c_77,plain,
! [X0: $i] :
( cC114(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[],[f506]) ).
tcf(c_78,plain,
! [X0: $i] :
( cC112(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[],[f505]) ).
tcf(c_102,plain,
! [X0: $i] :
( cC130(X0)
| ~ cC132(X0) ),
inference(cnf_transformation,[],[f529]) ).
tcf(c_104,plain,
! [X0: $i] :
( cC132(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[],[f533]) ).
tcf(c_105,plain,
! [X0: $i] :
( cC116(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[],[f532]) ).
tcf(c_109,plain,
! [X0: $i] :
( cC136(X0)
| ~ cC138(X0) ),
inference(cnf_transformation,[],[f538]) ).
tcf(c_110,plain,
! [X0: $i] :
( cC134(X0)
| ~ cC138(X0) ),
inference(cnf_transformation,[],[f537]) ).
tcf(c_137,plain,
! [X0: $i] :
( cC152(X0)
| ~ cC154(X0) ),
inference(cnf_transformation,[],[f564]) ).
tcf(c_139,plain,
! [X0: $i] :
( cC154(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[],[f568]) ).
tcf(c_140,plain,
! [X0: $i] :
( cC138(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[],[f567]) ).
tcf(c_142,plain,
! [X0: $i] :
( cC22(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[],[f571]) ).
tcf(c_143,plain,
! [X0: $i] :
( cC156(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[],[f570]) ).
tcf(c_145,plain,
! [X0: $i] :
( cC14(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[],[f574]) ).
tcf(c_146,plain,
! [X0: $i] :
( cC10(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[],[f573]) ).
tcf(c_169,plain,
! [X0: $i] :
( cC168(X0)
| ~ cC174(X0) ),
inference(cnf_transformation,[],[f598]) ).
tcf(c_179,plain,
! [X0: $i] :
( cC174(X0)
| ~ cC180(X0) ),
inference(cnf_transformation,[],[f606]) ).
tcf(c_184,plain,
! [X0: $i] :
( cC16(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[],[f613]) ).
tcf(c_185,plain,
! [X0: $i] :
( cC20(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[],[f612]) ).
tcf(c_189,plain,
! [X0: $i] :
( cC26(X0)
| cC2(X0)
| cC24(X0) ),
inference(cnf_transformation,[],[f620]) ).
tcf(c_198,plain,
! [X0: $i] :
( cC32(X0)
| cC30(X0)
| cC2(X0) ),
inference(cnf_transformation,[],[f629]) ).
tcf(c_208,plain,
! [X0: $i] :
( cC36(X0)
| ~ cC38(X0) ),
inference(cnf_transformation,[],[f637]) ).
tcf(c_213,plain,
! [X0: $i] :
( cC40(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f643]) ).
tcf(c_217,plain,
! [X0: $i] :
( cC38(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[],[f644]) ).
tcf(c_221,plain,
! [X0: $i] :
( cC46(X0)
| cC44(X0)
| cC12(X0) ),
inference(cnf_transformation,[],[f652]) ).
tcf(c_230,plain,
! [X0: $i] :
( cC52(X0)
| cC50(X0)
| cC12(X0) ),
inference(cnf_transformation,[],[f661]) ).
tcf(c_240,plain,
! [X0: $i] :
( cC56(X0)
| ~ cC58(X0) ),
inference(cnf_transformation,[],[f669]) ).
tcf(c_243,plain,
! [X0: $i] :
( cC58(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[],[f672]) ).
tcf(c_244,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[],[f671]) ).
tcf(c_245,plain,
! [X0: $i] :
( cC62(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f675]) ).
tcf(c_249,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC64(X0) ),
inference(cnf_transformation,[],[f676]) ).
tcf(c_253,plain,
! [X0: $i] :
( cC68(X0)
| cC66(X0)
| cC18(X0) ),
inference(cnf_transformation,[],[f684]) ).
tcf(c_262,plain,
! [X0: $i] :
( cC74(X0)
| cC72(X0)
| cC18(X0) ),
inference(cnf_transformation,[],[f693]) ).
tcf(c_276,plain,
! [X0: $i] :
( cC78(X0)
| ~ cC80(X0) ),
inference(cnf_transformation,[],[f703]) ).
tcf(c_278,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[],[f707]) ).
tcf(c_279,plain,
! [X0: $i] :
( cC64(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[],[f706]) ).
tcf(c_280,plain,
! [X0: $i] :
( cC84(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f710]) ).
tcf(c_283,plain,
! [X0: $i] :
( cC82(X0)
| ~ cC86(X0) ),
inference(cnf_transformation,[],[f712]) ).
tcf(c_285,plain,
! [X0: $i] :
( cC88(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f715]) ).
tcf(c_289,plain,
! [X0: $i] :
( cC86(X0)
| ~ cC90(X0) ),
inference(cnf_transformation,[],[f716]) ).
tcf(c_299,plain,
! [X0: $i] :
( cC158(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f729]) ).
tcf(c_300,plain,
! [X0: $i] :
( cC180(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f728]) ).
tcf(c_302,plain,
cTOP(iV21026),
inference(cnf_transformation,[],[f731]) ).
tcf(c_303,plain,
cTEST(iV21026),
inference(cnf_transformation,[],[f732]) ).
tcf(c_334,plain,
cowlThing(iV21026),
inference(cnf_transformation,[],[f763]) ).
tcf(c_340,plain,
~ cC26(iV21027),
inference(cnf_transformation,[],[f769]) ).
tcf(c_350,plain,
~ cC32(iV21027),
inference(cnf_transformation,[],[f779]) ).
tcf(c_364,plain,
~ cC2(iV21027),
inference(cnf_transformation,[],[f793]) ).
tcf(c_365,plain,
cowlThing(iV21027),
inference(cnf_transformation,[],[f794]) ).
tcf(c_371,plain,
~ cC46(iV21029),
inference(cnf_transformation,[],[f800]) ).
tcf(c_377,plain,
~ cC12(iV21029),
inference(cnf_transformation,[],[f806]) ).
tcf(c_382,plain,
~ cC52(iV21029),
inference(cnf_transformation,[],[f811]) ).
tcf(c_394,plain,
cowlThing(iV21029),
inference(cnf_transformation,[],[f823]) ).
tcf(c_405,plain,
~ cC68(iV21030),
inference(cnf_transformation,[],[f834]) ).
tcf(c_406,plain,
~ cC74(iV21030),
inference(cnf_transformation,[],[f835]) ).
tcf(c_416,plain,
~ cC18(iV21030),
inference(cnf_transformation,[],[f845]) ).
tcf(c_421,plain,
cowlThing(iV21030),
inference(cnf_transformation,[],[f850]) ).
tcf(c_456,negated_conjecture,
( xsd_integer(sK37)
| cowlNothing(sK36)
| ~ 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_string(sK37)
| ~ cowlThing(sK36)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030)
| ~ cowlThing(iV21026) ),
inference(cnf_transformation,[],[f886]) ).
tcf(c_457,negated_conjecture,
( xsd_string(sK37)
| cowlNothing(sK36)
| ~ 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_integer(sK37)
| ~ cowlThing(sK36)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030)
| ~ cowlThing(iV21026) ),
inference(cnf_transformation,[],[f885]) ).
tcf(c_460,plain,
( cC180(iV21026)
| ~ cTEST(iV21026) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_461,plain,
( cC158(iV21026)
| ~ cTEST(iV21026) ),
inference(instantiation,[status(thm)],[c_299]) ).
tcf(c_462,plain,
( cC86(iV21026)
| ~ cC90(iV21026) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_464,plain,
( cC88(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_466,plain,
( cC82(iV21026)
| ~ cC86(iV21026) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_467,plain,
( cC84(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_468,plain,
( cC64(iV21026)
| ~ cC82(iV21026) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_469,plain,
( cC80(iV21026)
| ~ cC82(iV21026) ),
inference(instantiation,[status(thm)],[c_278]) ).
tcf(c_470,plain,
( cC78(iV21026)
| ~ cC80(iV21026) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_471,plain,
( cC60(iV21026)
| ~ cC64(iV21026) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_473,plain,
( cC62(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_245]) ).
tcf(c_474,plain,
( cC42(iV21026)
| ~ cC60(iV21026) ),
inference(instantiation,[status(thm)],[c_244]) ).
tcf(c_475,plain,
( cC58(iV21026)
| ~ cC60(iV21026) ),
inference(instantiation,[status(thm)],[c_243]) ).
tcf(c_476,plain,
( cC56(iV21026)
| ~ cC58(iV21026) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_477,plain,
( cC38(iV21026)
| ~ cC42(iV21026) ),
inference(instantiation,[status(thm)],[c_217]) ).
tcf(c_479,plain,
( cC40(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_480,plain,
( cC36(iV21026)
| ~ cC38(iV21026) ),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_481,plain,
( cC20(iV21026)
| ~ cC22(iV21026) ),
inference(instantiation,[status(thm)],[c_185]) ).
tcf(c_482,plain,
( cC16(iV21026)
| ~ cC22(iV21026) ),
inference(instantiation,[status(thm)],[c_184]) ).
tcf(c_483,plain,
( cC174(iV21026)
| ~ cC180(iV21026) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_484,plain,
( cC168(iV21026)
| ~ cC174(iV21026) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_485,plain,
( cC10(iV21026)
| ~ cC16(iV21026) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_486,plain,
( cC14(iV21026)
| ~ cC16(iV21026) ),
inference(instantiation,[status(thm)],[c_145]) ).
tcf(c_487,plain,
( cC156(iV21026)
| ~ cC158(iV21026) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_488,plain,
( cC22(iV21026)
| ~ cC158(iV21026) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_489,plain,
( cC138(iV21026)
| ~ cC156(iV21026) ),
inference(instantiation,[status(thm)],[c_140]) ).
tcf(c_490,plain,
( cC154(iV21026)
| ~ cC156(iV21026) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_491,plain,
( cC152(iV21026)
| ~ cC154(iV21026) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_492,plain,
( cC134(iV21026)
| ~ cC138(iV21026) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_493,plain,
( cC136(iV21026)
| ~ cC138(iV21026) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_495,plain,
( cC116(iV21026)
| ~ cC134(iV21026) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_496,plain,
( cC132(iV21026)
| ~ cC134(iV21026) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_497,plain,
( cC130(iV21026)
| ~ cC132(iV21026) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_498,plain,
( cC112(iV21026)
| ~ cC116(iV21026) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_499,plain,
( cC114(iV21026)
| ~ cC116(iV21026) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_501,plain,
( cC110(iV21026)
| ~ cC112(iV21026) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_502,plain,
( cC90(iV21026)
| ~ cC112(iV21026) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_503,plain,
( cC108(iV21026)
| ~ cC110(iV21026) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_504,plain,
( cC4(iV21026)
| ~ cC10(iV21026) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_505,plain,
( cC8(iV21026)
| ~ cC10(iV21026) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_679,plain,
( xsd_string(sK37)
| cowlNothing(sK36)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ xsd_integer(sK37)
| ~ cowlThing(sK36)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029) ),
inference(global_subsumption_just,[status(thm)],[c_457,c_421,c_394,c_365,c_334,c_303,c_302,c_460,c_461,c_462,c_464,c_466,c_467,c_468,c_469,c_470,c_471,c_473,c_474,c_475,c_476,c_477,c_479,c_480,c_481,c_482,c_483,c_484,c_485,c_486,c_487,c_488,c_489,c_490,c_491,c_492,c_493,c_495,c_496,c_497,c_498,c_499,c_501,c_502,c_503,c_504,c_505,c_457]) ).
tcf(c_680,negated_conjecture,
( xsd_string(sK37)
| cowlNothing(sK36)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK37)
| ~ cowlThing(sK36) ),
inference(renaming,[status(thm)],[c_679]) ).
tcf(c_681,plain,
( xsd_integer(sK37)
| cowlNothing(sK36)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ xsd_string(sK37)
| ~ cowlThing(sK36)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029) ),
inference(global_subsumption_just,[status(thm)],[c_456,c_421,c_394,c_365,c_334,c_303,c_302,c_460,c_461,c_462,c_464,c_466,c_467,c_468,c_469,c_470,c_471,c_473,c_474,c_475,c_476,c_477,c_479,c_480,c_481,c_482,c_483,c_484,c_485,c_486,c_487,c_488,c_489,c_490,c_491,c_492,c_493,c_495,c_496,c_497,c_498,c_499,c_501,c_502,c_503,c_504,c_505,c_456]) ).
tcf(c_682,negated_conjecture,
( xsd_integer(sK37)
| cowlNothing(sK36)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_string(sK37)
| ~ cowlThing(sK36) ),
inference(renaming,[status(thm)],[c_681]) ).
tcf(c_683,plain,
! [X0: $i] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_52]) ).
tcf(c_684,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(renaming,[status(thm)],[c_683]) ).
tcf(c_685,plain,
! [X0: $i] :
( xsd_string(X0)
| xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_51]) ).
tcf(c_686,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(renaming,[status(thm)],[c_685]) ).
tcf(c_1950,plain,
( xsd_integer(sK37)
| cowlNothing(sK36)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_string(sK37) ),
inference(backward_subsumption_resolution,[status(thm)],[c_682,c_49]) ).
tcf(c_1951,plain,
( xsd_string(sK37)
| cowlNothing(sK36)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK37) ),
inference(backward_subsumption_resolution,[status(thm)],[c_680,c_49]) ).
tcf(c_2022,plain,
( xsd_string(sK37)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK37) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1951,c_50]) ).
tcf(c_2023,plain,
( xsd_integer(sK37)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_string(sK37) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1950,c_50]) ).
tcf(c_2193,plain,
( xsd_string(sK37)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2022,c_686]) ).
tcf(c_3900,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK37) ),
inference(resolution,[status(thm)],[c_684,c_2193]) ).
tcf(c_3901,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027) ),
inference(global_subsumption_just,[status(thm)],[c_3900,c_2023,c_2193,c_3900]) ).
tcf(c_5556,plain,
( cC2(iV21027)
| cC24(iV21027) ),
inference(resolution,[status(thm)],[c_189,c_340]) ).
tcf(c_5638,plain,
( cC30(iV21027)
| cC2(iV21027) ),
inference(resolution,[status(thm)],[c_198,c_350]) ).
tcf(c_5721,plain,
( cC44(iV21029)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[c_221,c_371]) ).
tcf(c_5802,plain,
( cC50(iV21029)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[c_230,c_382]) ).
tcf(c_5885,plain,
( cC66(iV21030)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[c_253,c_405]) ).
tcf(c_5967,plain,
( cC72(iV21030)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[c_262,c_406]) ).
tcf(c_5968,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_5967,c_5885,c_5802,c_5721,c_5638,c_5556,c_3901,c_364,c_377,c_416]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 19:27:02 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 2.71/1.29 % SZS status Started for theBenchmark.p
% 2.71/1.29 % SZS status Theorem for theBenchmark.p
% 2.71/1.29
% 2.71/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.71/1.29
% 2.71/1.29 % ------ iProver source info
% 2.71/1.29
% 2.71/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.71/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.71/1.29 % git: non_committed_changes: false
% 2.71/1.29
% 2.71/1.29 % ------ Parsing...
% 2.71/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.71/1.29
% 2.71/1.29 % ------ Preprocessing... sf_s rm: 7 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s%
% 2.71/1.29
% 2.71/1.29 % SZS status Theorem for theBenchmark.p
% 2.71/1.29
% 2.71/1.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.71/1.29
% 2.71/1.29
%------------------------------------------------------------------------------