%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:54:17 PM UTC 2026
% Result : Theorem 4.42s 1.84s
% Output : CNFRefutation 4.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 66
% Syntax : Number of formulae : 356 ( 141 unt; 0 def)
% Number of atoms : 2008 ( 0 equ)
% Maximal formula atoms : 51 ( 5 avg)
% Number of connectives : 3078 (1426 ~;1399 |; 227 &)
% ( 20 <=>; 5 =>; 0 <=; 1 <~>)
% Maximal formula depth : 50 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 15 con; 0-1 aty)
% Number of variables : 177 ( 0 sgn 167 !; 10 ?; 62 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f6,axiom,
! [X0] :
( cC106(X0)
<=> ( cC104(X0)
& ~ cC100(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
fof(f7,axiom,
! [X0] :
( cC108(X0)
<=> ( cC106(X0)
& cC28(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f26,axiom,
! [X0] :
( cC34(X0)
<=> ( ~ cC30(X0)
& ~ cC32(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(f28,axiom,
! [X0] :
( cC38(X0)
<=> ( cTOP(X0)
& ~ cC36(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_27) ).
fof(f30,axiom,
! [X0] :
( cC42(X0)
<=> ? [X1] :
( ~ cC8(X1)
& rR1(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(f31,axiom,
! [X0] :
( cC44(X0)
<=> ( cC42(X0)
& ~ cC40(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_30) ).
fof(f34,axiom,
! [X0] :
( cC50(X0)
<=> ( ~ cC48(X0)
& ~ cC46(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_33) ).
fof(f37,axiom,
! [X0] :
( cC56(X0)
<=> ( ~ cC54(X0)
& cC44(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_36) ).
fof(f40,axiom,
! [X0] :
( cC60(X0)
<=> ? [X1] :
( ~ cC12(X1)
& rR1(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_39) ).
fof(f41,axiom,
! [X0] :
( cC62(X0)
<=> ( ~ cC58(X0)
& cC60(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_40) ).
fof(f44,axiom,
! [X0] :
( cC68(X0)
<=> ( ~ cC66(X0)
& ~ cC64(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_43) ).
fof(f48,axiom,
! [X0] :
( cC76(X0)
<=> ( cC62(X0)
& ~ cC74(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_47) ).
fof(f51,axiom,
! [X0] :
( cC82(X0)
<=> ( cC80(X0)
& ~ cC78(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_50) ).
fof(f54,axiom,
! [X0] :
( cC88(X0)
<=> ( ~ cC86(X0)
& ~ cC84(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_53) ).
fof(f59,axiom,
! [X0] :
( cC98(X0)
<=> ( cC82(X0)
& ~ cC96(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_58) ).
fof(f60,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC130(X0)
& cC108(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_59) ).
fof(f61,axiom,
! [X0] :
( rR1(iV16439,X0)
=> cC98(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_60) ).
fof(f62,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_61) ).
fof(f64,axiom,
cowlThing(iV16439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_63) ).
fof(f65,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_64) ).
fof(f68,axiom,
! [X0] :
( rR1(iV16440,X0)
=> cC76(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_67) ).
fof(f73,axiom,
cowlThing(iV16440),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_72) ).
fof(f74,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_73) ).
fof(f77,axiom,
~ cC36(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_76) ).
fof(f80,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_79) ).
fof(f85,axiom,
cowlThing(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_84) ).
fof(f92,axiom,
~ cC58(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_91) ).
fof(f93,axiom,
~ cC74(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_92) ).
fof(f94,axiom,
! [X0] :
( rR1(iV16453,X0)
=> cC56(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_93) ).
fof(f95,axiom,
cowlThing(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_94) ).
fof(f97,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_96) ).
fof(f99,axiom,
~ cC40(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_98) ).
fof(f104,axiom,
~ cC54(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_103) ).
fof(f106,axiom,
cowlThing(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_105) ).
fof(f108,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_107) ).
fof(f109,axiom,
~ cC36(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_108) ).
fof(f114,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_113) ).
fof(f118,axiom,
cowlThing(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_117) ).
fof(f121,axiom,
~ cC48(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_120) ).
fof(f122,axiom,
~ cC30(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_121) ).
fof(f124,axiom,
~ cC86(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_123) ).
fof(f125,axiom,
~ cC46(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_124) ).
fof(f128,axiom,
~ cC66(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_127) ).
fof(f133,axiom,
~ cC84(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_132) ).
fof(f134,axiom,
~ cC64(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_133) ).
fof(f135,axiom,
cowlThing(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_134) ).
fof(f136,axiom,
~ cC32(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_135) ).
fof(f138,axiom,
~ cC36(iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_137) ).
fof(f141,axiom,
cTOP(iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_140) ).
fof(f142,axiom,
~ cC8(iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_141) ).
fof(f147,axiom,
cowlThing(iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_146) ).
fof(f152,axiom,
~ cC12(iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_151) ).
fof(f156,axiom,
cowlThing(iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_155) ).
fof(f162,axiom,
~ cC36(iV16462),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_161) ).
fof(f163,axiom,
cTOP(iV16462),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_162) ).
fof(f169,axiom,
cowlThing(iV16462),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_168) ).
fof(f172,axiom,
! [X0] :
( rR1(iV16463,X0)
=> cC56(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_171) ).
fof(f177,axiom,
cowlThing(iV16463),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_176) ).
fof(f178,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_177) ).
fof(f188,axiom,
cowlThing(iV16464),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_187) ).
fof(f196,axiom,
~ cC36(iV16465),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_195) ).
fof(f197,axiom,
cTOP(iV16465),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_196) ).
fof(f199,axiom,
cowlThing(iV16465),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_198) ).
fof(f201,conjecture,
( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(f202,negated_conjecture,
~ ( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(negated_conjecture,[status(cth)],[f201]) ).
fof(f203,plain,
~ ( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(rectify,[],[f202]) ).
fof(f204,plain,
! [X0] :
( cTEST(X0)
=> ( cC130(X0)
& cC108(X0) ) ),
inference(unused_predicate_definition_removal,[],[f60]) ).
fof(f205,plain,
! [X0] :
( ~ cTEST(X0)
| ( cC130(X0)
& cC108(X0) ) ),
inference(ennf_transformation,[],[f204]) ).
fof(f206,plain,
! [X0] :
( ~ rR1(iV16439,X0)
| cC98(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f207,plain,
! [X0] :
( ~ rR1(iV16440,X0)
| cC76(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f215,plain,
! [X0] :
( ~ rR1(iV16453,X0)
| cC56(X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f237,plain,
! [X0] :
( ~ rR1(iV16463,X0)
| cC56(X0) ),
inference(ennf_transformation,[],[f172]) ).
fof(f247,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(ennf_transformation,[],[f203]) ).
fof(f248,plain,
! [X0] :
( ( ~ xsd_string(X0)
| ~ xsd_integer(X0) )
& ( xsd_integer(X0)
| xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f257,plain,
! [X0] :
( ( ~ cC106(X0)
| ( cC104(X0)
& ~ cC100(X0) ) )
& ( ~ cC104(X0)
| cC100(X0)
| cC106(X0) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f258,plain,
! [X0] :
( ( ~ cC106(X0)
| ( cC104(X0)
& ~ cC100(X0) ) )
& ( ~ cC104(X0)
| cC100(X0)
| cC106(X0) ) ),
inference(flattening,[],[f257]) ).
fof(f259,plain,
! [X0] :
( ( ~ cC108(X0)
| ( cC106(X0)
& cC28(X0) ) )
& ( ~ cC106(X0)
| ~ cC28(X0)
| cC108(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f260,plain,
! [X0] :
( ( ~ cC108(X0)
| ( cC106(X0)
& cC28(X0) ) )
& ( ~ cC106(X0)
| ~ cC28(X0)
| cC108(X0) ) ),
inference(flattening,[],[f259]) ).
fof(f307,plain,
! [X0] :
( ( ~ cC34(X0)
| ( ~ cC30(X0)
& ~ cC32(X0) ) )
& ( cC30(X0)
| cC32(X0)
| cC34(X0) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f308,plain,
! [X0] :
( ( ~ cC34(X0)
| ( ~ cC30(X0)
& ~ cC32(X0) ) )
& ( cC30(X0)
| cC32(X0)
| cC34(X0) ) ),
inference(flattening,[],[f307]) ).
fof(f312,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cTOP(X0)
& ~ cC36(X0) ) )
& ( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f313,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cTOP(X0)
& ~ cC36(X0) ) )
& ( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ) ),
inference(flattening,[],[f312]) ).
fof(f317,plain,
! [X0] :
( ( ~ cC42(X0)
| ? [X1] :
( ~ cC8(X1)
& rR1(X0,X1) ) )
& ( ! [X1] :
( cC8(X1)
| ~ rR1(X0,X1) )
| cC42(X0) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f318,plain,
! [X0] :
( ( ~ cC42(X0)
| ? [X2] :
( ~ cC8(X2)
& rR1(X0,X2) ) )
& ( ! [X1] :
( cC8(X1)
| ~ rR1(X0,X1) )
| cC42(X0) ) ),
inference(rectify,[],[f317]) ).
fof(f319,plain,
! [X0] :
( ( ~ cC42(X0)
| ( ~ cC8(sK14(X0))
& rR1(X0,sK14(X0)) ) )
& ( ! [X1] :
( cC8(X1)
| ~ rR1(X0,X1) )
| cC42(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0))],[f318]) ).
fof(f320,plain,
! [X0] :
( ( ~ cC44(X0)
| ( cC42(X0)
& ~ cC40(X0) ) )
& ( ~ cC42(X0)
| cC40(X0)
| cC44(X0) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f321,plain,
! [X0] :
( ( ~ cC44(X0)
| ( cC42(X0)
& ~ cC40(X0) ) )
& ( ~ cC42(X0)
| cC40(X0)
| cC44(X0) ) ),
inference(flattening,[],[f320]) ).
fof(f326,plain,
! [X0] :
( ( ~ cC50(X0)
| ( ~ cC48(X0)
& ~ cC46(X0) ) )
& ( cC48(X0)
| cC46(X0)
| cC50(X0) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f327,plain,
! [X0] :
( ( ~ cC50(X0)
| ( ~ cC48(X0)
& ~ cC46(X0) ) )
& ( cC48(X0)
| cC46(X0)
| cC50(X0) ) ),
inference(flattening,[],[f326]) ).
fof(f334,plain,
! [X0] :
( ( ~ cC56(X0)
| ( ~ cC54(X0)
& cC44(X0) ) )
& ( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f335,plain,
! [X0] :
( ( ~ cC56(X0)
| ( ~ cC54(X0)
& cC44(X0) ) )
& ( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ) ),
inference(flattening,[],[f334]) ).
fof(f341,plain,
! [X0] :
( ( ~ cC60(X0)
| ? [X1] :
( ~ cC12(X1)
& rR1(X0,X1) ) )
& ( ! [X1] :
( cC12(X1)
| ~ rR1(X0,X1) )
| cC60(X0) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f342,plain,
! [X0] :
( ( ~ cC60(X0)
| ? [X2] :
( ~ cC12(X2)
& rR1(X0,X2) ) )
& ( ! [X1] :
( cC12(X1)
| ~ rR1(X0,X1) )
| cC60(X0) ) ),
inference(rectify,[],[f341]) ).
fof(f343,plain,
! [X0] :
( ( ~ cC60(X0)
| ( ~ cC12(sK18(X0))
& rR1(X0,sK18(X0)) ) )
& ( ! [X1] :
( cC12(X1)
| ~ rR1(X0,X1) )
| cC60(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0))],[f342]) ).
fof(f344,plain,
! [X0] :
( ( ~ cC62(X0)
| ( ~ cC58(X0)
& cC60(X0) ) )
& ( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f345,plain,
! [X0] :
( ( ~ cC62(X0)
| ( ~ cC58(X0)
& cC60(X0) ) )
& ( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ) ),
inference(flattening,[],[f344]) ).
fof(f350,plain,
! [X0] :
( ( ~ cC68(X0)
| ( ~ cC66(X0)
& ~ cC64(X0) ) )
& ( cC66(X0)
| cC64(X0)
| cC68(X0) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f351,plain,
! [X0] :
( ( ~ cC68(X0)
| ( ~ cC66(X0)
& ~ cC64(X0) ) )
& ( cC66(X0)
| cC64(X0)
| cC68(X0) ) ),
inference(flattening,[],[f350]) ).
fof(f361,plain,
! [X0] :
( ( ~ cC76(X0)
| ( cC62(X0)
& ~ cC74(X0) ) )
& ( ~ cC62(X0)
| cC74(X0)
| cC76(X0) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f362,plain,
! [X0] :
( ( ~ cC76(X0)
| ( cC62(X0)
& ~ cC74(X0) ) )
& ( ~ cC62(X0)
| cC74(X0)
| cC76(X0) ) ),
inference(flattening,[],[f361]) ).
fof(f369,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC80(X0)
& ~ cC78(X0) ) )
& ( ~ cC80(X0)
| cC78(X0)
| cC82(X0) ) ),
inference(nnf_transformation,[],[f51]) ).
fof(f370,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC80(X0)
& ~ cC78(X0) ) )
& ( ~ cC80(X0)
| cC78(X0)
| cC82(X0) ) ),
inference(flattening,[],[f369]) ).
fof(f375,plain,
! [X0] :
( ( ~ cC88(X0)
| ( ~ cC86(X0)
& ~ cC84(X0) ) )
& ( cC86(X0)
| cC84(X0)
| cC88(X0) ) ),
inference(nnf_transformation,[],[f54]) ).
fof(f376,plain,
! [X0] :
( ( ~ cC88(X0)
| ( ~ cC86(X0)
& ~ cC84(X0) ) )
& ( cC86(X0)
| cC84(X0)
| cC88(X0) ) ),
inference(flattening,[],[f375]) ).
fof(f389,plain,
! [X0] :
( ( ~ cC98(X0)
| ( cC82(X0)
& ~ cC96(X0) ) )
& ( ~ cC82(X0)
| cC96(X0)
| cC98(X0) ) ),
inference(nnf_transformation,[],[f59]) ).
fof(f390,plain,
! [X0] :
( ( ~ cC98(X0)
| ( cC82(X0)
& ~ cC96(X0) ) )
& ( ~ cC82(X0)
| cC96(X0)
| cC98(X0) ) ),
inference(flattening,[],[f389]) ).
fof(f391,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [X1] :
( ( xsd_string(X1)
| ~ xsd_integer(X1) )
& ( ~ xsd_string(X1)
| xsd_integer(X1) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(nnf_transformation,[],[f247]) ).
fof(f392,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ( ( xsd_string(sK29)
| ~ xsd_integer(sK29) )
& ( ~ xsd_string(sK29)
| xsd_integer(sK29) ) )
| cowlNothing(sK28)
| ~ cowlThing(sK28) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28,sK29]),skolemize(X0,sK28),skolemize(X1,sK29)],[f391]) ).
fof(f393,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f394,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f395,plain,
! [X0] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f396,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f406,plain,
! [X0] :
( ~ cC106(X0)
| cC104(X0) ),
inference(cnf_transformation,[],[f258]) ).
fof(f409,plain,
! [X0] :
( ~ cC108(X0)
| cC106(X0) ),
inference(cnf_transformation,[],[f260]) ).
fof(f410,plain,
! [X0] :
( ~ cC108(X0)
| cC28(X0) ),
inference(cnf_transformation,[],[f260]) ).
fof(f468,plain,
! [X0] :
( cC30(X0)
| cC32(X0)
| cC34(X0) ),
inference(cnf_transformation,[],[f308]) ).
fof(f474,plain,
! [X0] :
( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ),
inference(cnf_transformation,[],[f313]) ).
fof(f480,plain,
! [X0,X1] :
( cC8(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(cnf_transformation,[],[f319]) ).
fof(f481,plain,
! [X0] :
( ~ cC44(X0)
| cC42(X0) ),
inference(cnf_transformation,[],[f321]) ).
fof(f483,plain,
! [X0] :
( ~ cC42(X0)
| cC40(X0)
| cC44(X0) ),
inference(cnf_transformation,[],[f321]) ).
fof(f492,plain,
! [X0] :
( cC48(X0)
| cC46(X0)
| cC50(X0) ),
inference(cnf_transformation,[],[f327]) ).
fof(f500,plain,
! [X0] :
( ~ cC56(X0)
| cC44(X0) ),
inference(cnf_transformation,[],[f335]) ).
fof(f501,plain,
! [X0] :
( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f335]) ).
fof(f510,plain,
! [X0,X1] :
( cC12(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(cnf_transformation,[],[f343]) ).
fof(f512,plain,
! [X0] :
( ~ cC62(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f345]) ).
fof(f513,plain,
! [X0] :
( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f345]) ).
fof(f522,plain,
! [X0] :
( cC66(X0)
| cC64(X0)
| cC68(X0) ),
inference(cnf_transformation,[],[f351]) ).
fof(f532,plain,
! [X0] :
( ~ cC76(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f362]) ).
fof(f534,plain,
! [X0] :
( ~ cC62(X0)
| cC74(X0)
| cC76(X0) ),
inference(cnf_transformation,[],[f362]) ).
fof(f541,plain,
! [X0] :
( ~ cC82(X0)
| cC80(X0) ),
inference(cnf_transformation,[],[f370]) ).
fof(f552,plain,
! [X0] :
( cC86(X0)
| cC84(X0)
| cC88(X0) ),
inference(cnf_transformation,[],[f376]) ).
fof(f565,plain,
! [X0] :
( ~ cC98(X0)
| cC82(X0) ),
inference(cnf_transformation,[],[f390]) ).
fof(f568,plain,
! [X0] :
( ~ cTEST(X0)
| cC130(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f569,plain,
! [X0] :
( ~ cTEST(X0)
| cC108(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f570,plain,
! [X0] :
( ~ rR1(iV16439,X0)
| cC98(X0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f571,plain,
cTEST(iV16439),
inference(cnf_transformation,[],[f62]) ).
fof(f573,plain,
cowlThing(iV16439),
inference(cnf_transformation,[],[f64]) ).
fof(f574,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[],[f65]) ).
fof(f577,plain,
! [X0] :
( ~ rR1(iV16440,X0)
| cC76(X0) ),
inference(cnf_transformation,[],[f207]) ).
fof(f582,plain,
cowlThing(iV16440),
inference(cnf_transformation,[],[f73]) ).
fof(f583,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[],[f74]) ).
fof(f586,plain,
~ cC36(iV16448),
inference(cnf_transformation,[],[f77]) ).
fof(f589,plain,
cTOP(iV16448),
inference(cnf_transformation,[],[f80]) ).
fof(f594,plain,
cowlThing(iV16448),
inference(cnf_transformation,[],[f85]) ).
fof(f601,plain,
~ cC58(iV16453),
inference(cnf_transformation,[],[f92]) ).
fof(f602,plain,
~ cC74(iV16453),
inference(cnf_transformation,[],[f93]) ).
fof(f603,plain,
! [X0] :
( ~ rR1(iV16453,X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f215]) ).
fof(f604,plain,
cowlThing(iV16453),
inference(cnf_transformation,[],[f95]) ).
fof(f606,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[],[f97]) ).
fof(f608,plain,
~ cC40(iV16455),
inference(cnf_transformation,[],[f99]) ).
fof(f613,plain,
~ cC54(iV16455),
inference(cnf_transformation,[],[f104]) ).
fof(f615,plain,
cowlThing(iV16455),
inference(cnf_transformation,[],[f106]) ).
fof(f617,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[],[f108]) ).
fof(f618,plain,
~ cC36(iV16457),
inference(cnf_transformation,[],[f109]) ).
fof(f623,plain,
cTOP(iV16457),
inference(cnf_transformation,[],[f114]) ).
fof(f627,plain,
cowlThing(iV16457),
inference(cnf_transformation,[],[f118]) ).
fof(f630,plain,
~ cC48(iV16459),
inference(cnf_transformation,[],[f121]) ).
fof(f631,plain,
~ cC30(iV16459),
inference(cnf_transformation,[],[f122]) ).
fof(f633,plain,
~ cC86(iV16459),
inference(cnf_transformation,[],[f124]) ).
fof(f634,plain,
~ cC46(iV16459),
inference(cnf_transformation,[],[f125]) ).
fof(f637,plain,
~ cC66(iV16459),
inference(cnf_transformation,[],[f128]) ).
fof(f642,plain,
~ cC84(iV16459),
inference(cnf_transformation,[],[f133]) ).
fof(f643,plain,
~ cC64(iV16459),
inference(cnf_transformation,[],[f134]) ).
fof(f644,plain,
cowlThing(iV16459),
inference(cnf_transformation,[],[f135]) ).
fof(f645,plain,
~ cC32(iV16459),
inference(cnf_transformation,[],[f136]) ).
fof(f647,plain,
~ cC36(iV16460),
inference(cnf_transformation,[],[f138]) ).
fof(f650,plain,
cTOP(iV16460),
inference(cnf_transformation,[],[f141]) ).
fof(f651,plain,
~ cC8(iV16460),
inference(cnf_transformation,[],[f142]) ).
fof(f656,plain,
cowlThing(iV16460),
inference(cnf_transformation,[],[f147]) ).
fof(f661,plain,
~ cC12(iV16461),
inference(cnf_transformation,[],[f152]) ).
fof(f665,plain,
cowlThing(iV16461),
inference(cnf_transformation,[],[f156]) ).
fof(f671,plain,
~ cC36(iV16462),
inference(cnf_transformation,[],[f162]) ).
fof(f672,plain,
cTOP(iV16462),
inference(cnf_transformation,[],[f163]) ).
fof(f678,plain,
cowlThing(iV16462),
inference(cnf_transformation,[],[f169]) ).
fof(f681,plain,
! [X0] :
( ~ rR1(iV16463,X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f686,plain,
cowlThing(iV16463),
inference(cnf_transformation,[],[f177]) ).
fof(f687,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[],[f178]) ).
fof(f697,plain,
cowlThing(iV16464),
inference(cnf_transformation,[],[f188]) ).
fof(f705,plain,
~ cC36(iV16465),
inference(cnf_transformation,[],[f196]) ).
fof(f706,plain,
cTOP(iV16465),
inference(cnf_transformation,[],[f197]) ).
fof(f708,plain,
cowlThing(iV16465),
inference(cnf_transformation,[],[f199]) ).
fof(f710,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_string(sK29)
| ~ xsd_integer(sK29)
| cowlNothing(sK28)
| ~ cowlThing(sK28) ),
inference(cnf_transformation,[],[f392]) ).
fof(f711,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_string(sK29)
| xsd_integer(sK29)
| cowlNothing(sK28)
| ~ cowlThing(sK28) ),
inference(cnf_transformation,[],[f392]) ).
tcf(c_49,plain,
! [X0: $i] : cowlThing(X0),
inference(cnf_transformation,[],[f394]) ).
tcf(c_50,plain,
! [X0: $i] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f393]) ).
tcf(c_51,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f396]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f395]) ).
tcf(c_64,plain,
! [X0: $i] :
( cC104(X0)
| ~ cC106(X0) ),
inference(cnf_transformation,[],[f406]) ).
tcf(c_66,plain,
! [X0: $i] :
( cC28(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[],[f410]) ).
tcf(c_67,plain,
! [X0: $i] :
( cC106(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[],[f409]) ).
tcf(c_122,plain,
! [X0: $i] :
( cC34(X0)
| cC32(X0)
| cC30(X0) ),
inference(cnf_transformation,[],[f468]) ).
tcf(c_128,plain,
! [X0: $i] :
( cC38(X0)
| cC36(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f474]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] :
( cC42(X0)
| cC8(X1)
| ~ rR1(X0,X1) ),
inference(cnf_transformation,[],[f480]) ).
tcf(c_137,plain,
! [X0: $i] :
( cC44(X0)
| cC40(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[],[f483]) ).
tcf(c_139,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[],[f481]) ).
tcf(c_146,plain,
! [X0: $i] :
( cC50(X0)
| cC48(X0)
| cC46(X0) ),
inference(cnf_transformation,[],[f492]) ).
tcf(c_155,plain,
! [X0: $i] :
( cC56(X0)
| cC54(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_156,plain,
! [X0: $i] :
( cC44(X0)
| ~ cC56(X0) ),
inference(cnf_transformation,[],[f500]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( cC60(X0)
| cC12(X1)
| ~ rR1(X0,X1) ),
inference(cnf_transformation,[],[f510]) ).
tcf(c_167,plain,
! [X0: $i] :
( cC62(X0)
| cC58(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[],[f513]) ).
tcf(c_168,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[],[f512]) ).
tcf(c_176,plain,
! [X0: $i] :
( cC68(X0)
| cC66(X0)
| cC64(X0) ),
inference(cnf_transformation,[],[f522]) ).
tcf(c_188,plain,
! [X0: $i] :
( cC76(X0)
| cC74(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[],[f534]) ).
tcf(c_190,plain,
! [X0: $i] :
( cC62(X0)
| ~ cC76(X0) ),
inference(cnf_transformation,[],[f532]) ).
tcf(c_199,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[],[f541]) ).
tcf(c_206,plain,
! [X0: $i] :
( cC88(X0)
| cC86(X0)
| cC84(X0) ),
inference(cnf_transformation,[],[f552]) ).
tcf(c_223,plain,
! [X0: $i] :
( cC82(X0)
| ~ cC98(X0) ),
inference(cnf_transformation,[],[f565]) ).
tcf(c_224,plain,
! [X0: $i] :
( cC108(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f569]) ).
tcf(c_225,plain,
! [X0: $i] :
( cC130(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f568]) ).
tcf(c_226,plain,
! [X0: $i] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[],[f570]) ).
tcf(c_227,plain,
cTEST(iV16439),
inference(cnf_transformation,[],[f571]) ).
tcf(c_229,plain,
cowlThing(iV16439),
inference(cnf_transformation,[],[f573]) ).
tcf(c_230,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[],[f574]) ).
tcf(c_233,plain,
! [X0: $i] :
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(cnf_transformation,[],[f577]) ).
tcf(c_238,plain,
cowlThing(iV16440),
inference(cnf_transformation,[],[f582]) ).
tcf(c_239,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[],[f583]) ).
tcf(c_242,plain,
~ cC36(iV16448),
inference(cnf_transformation,[],[f586]) ).
tcf(c_245,plain,
cTOP(iV16448),
inference(cnf_transformation,[],[f589]) ).
tcf(c_250,plain,
cowlThing(iV16448),
inference(cnf_transformation,[],[f594]) ).
tcf(c_257,plain,
~ cC58(iV16453),
inference(cnf_transformation,[],[f601]) ).
tcf(c_258,plain,
~ cC74(iV16453),
inference(cnf_transformation,[],[f602]) ).
tcf(c_259,plain,
! [X0: $i] :
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(cnf_transformation,[],[f603]) ).
tcf(c_260,plain,
cowlThing(iV16453),
inference(cnf_transformation,[],[f604]) ).
tcf(c_262,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[],[f606]) ).
tcf(c_264,plain,
~ cC40(iV16455),
inference(cnf_transformation,[],[f608]) ).
tcf(c_269,plain,
~ cC54(iV16455),
inference(cnf_transformation,[],[f613]) ).
tcf(c_271,plain,
cowlThing(iV16455),
inference(cnf_transformation,[],[f615]) ).
tcf(c_273,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[],[f617]) ).
tcf(c_274,plain,
~ cC36(iV16457),
inference(cnf_transformation,[],[f618]) ).
tcf(c_279,plain,
cTOP(iV16457),
inference(cnf_transformation,[],[f623]) ).
tcf(c_283,plain,
cowlThing(iV16457),
inference(cnf_transformation,[],[f627]) ).
tcf(c_286,plain,
~ cC48(iV16459),
inference(cnf_transformation,[],[f630]) ).
tcf(c_287,plain,
~ cC30(iV16459),
inference(cnf_transformation,[],[f631]) ).
tcf(c_289,plain,
~ cC86(iV16459),
inference(cnf_transformation,[],[f633]) ).
tcf(c_290,plain,
~ cC46(iV16459),
inference(cnf_transformation,[],[f634]) ).
tcf(c_293,plain,
~ cC66(iV16459),
inference(cnf_transformation,[],[f637]) ).
tcf(c_298,plain,
~ cC84(iV16459),
inference(cnf_transformation,[],[f642]) ).
tcf(c_299,plain,
~ cC64(iV16459),
inference(cnf_transformation,[],[f643]) ).
tcf(c_300,plain,
cowlThing(iV16459),
inference(cnf_transformation,[],[f644]) ).
tcf(c_301,plain,
~ cC32(iV16459),
inference(cnf_transformation,[],[f645]) ).
tcf(c_303,plain,
~ cC36(iV16460),
inference(cnf_transformation,[],[f647]) ).
tcf(c_306,plain,
cTOP(iV16460),
inference(cnf_transformation,[],[f650]) ).
tcf(c_307,plain,
~ cC8(iV16460),
inference(cnf_transformation,[],[f651]) ).
tcf(c_312,plain,
cowlThing(iV16460),
inference(cnf_transformation,[],[f656]) ).
tcf(c_317,plain,
~ cC12(iV16461),
inference(cnf_transformation,[],[f661]) ).
tcf(c_321,plain,
cowlThing(iV16461),
inference(cnf_transformation,[],[f665]) ).
tcf(c_327,plain,
~ cC36(iV16462),
inference(cnf_transformation,[],[f671]) ).
tcf(c_328,plain,
cTOP(iV16462),
inference(cnf_transformation,[],[f672]) ).
tcf(c_334,plain,
cowlThing(iV16462),
inference(cnf_transformation,[],[f678]) ).
tcf(c_337,plain,
! [X0: $i] :
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(cnf_transformation,[],[f681]) ).
tcf(c_342,plain,
cowlThing(iV16463),
inference(cnf_transformation,[],[f686]) ).
tcf(c_343,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[],[f687]) ).
tcf(c_353,plain,
cowlThing(iV16464),
inference(cnf_transformation,[],[f697]) ).
tcf(c_361,plain,
~ cC36(iV16465),
inference(cnf_transformation,[],[f705]) ).
tcf(c_362,plain,
cTOP(iV16465),
inference(cnf_transformation,[],[f706]) ).
tcf(c_364,plain,
cowlThing(iV16465),
inference(cnf_transformation,[],[f708]) ).
tcf(c_366,negated_conjecture,
( xsd_integer(sK29)
| cowlNothing(sK28)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_string(sK29)
| ~ cowlThing(sK28)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440)
| ~ cowlThing(iV16439) ),
inference(cnf_transformation,[],[f711]) ).
tcf(c_367,negated_conjecture,
( xsd_string(sK29)
| cowlNothing(sK28)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_integer(sK29)
| ~ cowlThing(sK28)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440)
| ~ cowlThing(iV16439) ),
inference(cnf_transformation,[],[f710]) ).
tcf(c_416,plain,
( cC88(iV16459)
| cC86(iV16459)
| cC84(iV16459) ),
inference(instantiation,[status(thm)],[c_206]) ).
tcf(c_421,plain,
( cC68(iV16459)
| cC66(iV16459)
| cC64(iV16459) ),
inference(instantiation,[status(thm)],[c_176]) ).
tcf(c_425,plain,
( cC50(iV16459)
| cC48(iV16459)
| cC46(iV16459) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_428,plain,
( cC34(iV16459)
| cC32(iV16459)
| cC30(iV16459) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_539,plain,
( xsd_string(sK29)
| cowlNothing(sK28)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_integer(sK29)
| ~ cowlThing(sK28)
| ~ cC38(iV16448)
| ~ cC38(iV16460)
| ~ cC38(iV16457)
| ~ cC38(iV16462)
| ~ cC38(iV16465)
| ~ cC42(iV16461)
| ~ cC42(iV16455)
| ~ cC42(iV16464)
| ~ cC44(iV16461)
| ~ cC44(iV16455)
| ~ cC44(iV16464)
| ~ cC76(iV16463)
| ~ cC76(iV16453)
| ~ cC80(iV16440)
| ~ cC82(iV16440) ),
inference(global_subsumption_just,[status(thm)],[c_367,c_364,c_353,c_342,c_334,c_321,c_312,c_300,c_283,c_271,c_260,c_250,c_238,c_229,c_301,c_299,c_298,c_293,c_290,c_289,c_287,c_286,c_416,c_421,c_425,c_428,c_367]) ).
tcf(c_540,negated_conjecture,
( xsd_string(sK29)
| cowlNothing(sK28)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_integer(sK29)
| ~ cowlThing(sK28) ),
inference(renaming,[status(thm)],[c_539]) ).
tcf(c_541,plain,
( xsd_integer(sK29)
| cowlNothing(sK28)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_string(sK29)
| ~ cowlThing(sK28)
| ~ cC38(iV16448)
| ~ cC38(iV16460)
| ~ cC38(iV16457)
| ~ cC38(iV16462)
| ~ cC38(iV16465)
| ~ cC42(iV16461)
| ~ cC42(iV16455)
| ~ cC42(iV16464)
| ~ cC44(iV16461)
| ~ cC44(iV16455)
| ~ cC44(iV16464)
| ~ cC76(iV16463)
| ~ cC76(iV16453)
| ~ cC80(iV16440)
| ~ cC82(iV16440) ),
inference(global_subsumption_just,[status(thm)],[c_366,c_364,c_353,c_342,c_334,c_321,c_312,c_300,c_283,c_271,c_260,c_250,c_238,c_229,c_301,c_299,c_298,c_293,c_290,c_289,c_287,c_286,c_416,c_421,c_425,c_428,c_366]) ).
tcf(c_542,negated_conjecture,
( xsd_integer(sK29)
| cowlNothing(sK28)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_string(sK29)
| ~ cowlThing(sK28) ),
inference(renaming,[status(thm)],[c_541]) ).
tcf(c_543,plain,
! [X0: $i] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_52]) ).
tcf(c_544,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(renaming,[status(thm)],[c_543]) ).
tcf(c_545,plain,
! [X0: $i] :
( xsd_string(X0)
| xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_51]) ).
tcf(c_546,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(renaming,[status(thm)],[c_545]) ).
tcf(c_581,plain,
! [X0: $i] :
( ~ cC106(X0)
| cC104(X0) ),
inference(prop_impl_just,[status(thm)],[c_64]) ).
tcf(c_582,plain,
! [X0: $i] :
( cC104(X0)
| ~ cC106(X0) ),
inference(renaming,[status(thm)],[c_581]) ).
tcf(c_589,plain,
! [X0: $i] :
( ~ cC108(X0)
| cC106(X0) ),
inference(prop_impl_just,[status(thm)],[c_67]) ).
tcf(c_590,plain,
! [X0: $i] :
( cC106(X0)
| ~ cC108(X0) ),
inference(renaming,[status(thm)],[c_589]) ).
tcf(c_593,plain,
! [X0: $i] :
( cC28(X0)
| ~ cC108(X0) ),
inference(prop_impl_just,[status(thm)],[c_66]) ).
tcf(c_601,plain,
! [X0: $i] :
( ~ cTEST(X0)
| cC108(X0) ),
inference(prop_impl_just,[status(thm)],[c_224]) ).
tcf(c_602,plain,
! [X0: $i] :
( cC108(X0)
| ~ cTEST(X0) ),
inference(renaming,[status(thm)],[c_601]) ).
tcf(c_677,plain,
! [X0: $i] :
( ~ cTEST(X0)
| cC130(X0) ),
inference(prop_impl_just,[status(thm)],[c_225]) ).
tcf(c_678,plain,
! [X0: $i] :
( cC130(X0)
| ~ cTEST(X0) ),
inference(renaming,[status(thm)],[c_677]) ).
tcf(c_777,plain,
! [X0: $i] :
( ~ cC44(X0)
| cC42(X0) ),
inference(prop_impl_just,[status(thm)],[c_139]) ).
tcf(c_778,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC44(X0) ),
inference(renaming,[status(thm)],[c_777]) ).
tcf(c_785,plain,
! [X0: $i] :
( ~ cC56(X0)
| cC44(X0) ),
inference(prop_impl_just,[status(thm)],[c_156]) ).
tcf(c_786,plain,
! [X0: $i] :
( cC44(X0)
| ~ cC56(X0) ),
inference(renaming,[status(thm)],[c_785]) ).
tcf(c_851,plain,
! [X0: $i] :
( ~ cC62(X0)
| cC60(X0) ),
inference(prop_impl_just,[status(thm)],[c_168]) ).
tcf(c_852,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC62(X0) ),
inference(renaming,[status(thm)],[c_851]) ).
tcf(c_859,plain,
! [X0: $i] :
( ~ cC76(X0)
| cC62(X0) ),
inference(prop_impl_just,[status(thm)],[c_190]) ).
tcf(c_860,plain,
! [X0: $i] :
( cC62(X0)
| ~ cC76(X0) ),
inference(renaming,[status(thm)],[c_859]) ).
tcf(c_931,plain,
! [X0: $i] :
( ~ cC82(X0)
| cC80(X0) ),
inference(prop_impl_just,[status(thm)],[c_199]) ).
tcf(c_932,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC82(X0) ),
inference(renaming,[status(thm)],[c_931]) ).
tcf(c_939,plain,
! [X0: $i] :
( ~ cC98(X0)
| cC82(X0) ),
inference(prop_impl_just,[status(thm)],[c_223]) ).
tcf(c_940,plain,
! [X0: $i] :
( cC82(X0)
| ~ cC98(X0) ),
inference(renaming,[status(thm)],[c_939]) ).
tcf(c_1003,plain,
! [X0: $i] :
( ~ rR1(iV16439,X0)
| cC98(X0) ),
inference(prop_impl_just,[status(thm)],[c_226]) ).
tcf(c_1004,plain,
! [X0: $i] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(renaming,[status(thm)],[c_1003]) ).
tcf(c_1548,plain,
( xsd_integer(sK29)
| cowlNothing(sK28)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_string(sK29) ),
inference(backward_subsumption_resolution,[status(thm)],[c_542,c_49]) ).
tcf(c_1549,plain,
( xsd_string(sK29)
| cowlNothing(sK28)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_integer(sK29) ),
inference(backward_subsumption_resolution,[status(thm)],[c_540,c_49]) ).
tcf(c_1568,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_integer(sK29) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1549,c_50]) ).
tcf(c_1569,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440)
| ~ xsd_string(sK29) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1548,c_50]) ).
tcf(c_1723,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1569,c_546]) ).
tcf(c_1725,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1568,c_546]) ).
tcf(c_1758,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1723,c_582]) ).
tcf(c_1759,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1725,c_582]) ).
tcf(c_1764,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1759,c_590]) ).
tcf(c_1765,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1758,c_590]) ).
tcf(c_1770,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1765,c_593]) ).
tcf(c_1771,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1764,c_593]) ).
tcf(c_1836,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1771,c_778]) ).
tcf(c_1837,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1770,c_778]) ).
tcf(c_1842,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1837,c_786]) ).
tcf(c_1843,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1836,c_786]) ).
tcf(c_1848,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1843,c_852]) ).
tcf(c_1849,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1842,c_852]) ).
tcf(c_1854,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1849,c_860]) ).
tcf(c_1855,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1848,c_860]) ).
tcf(c_1860,plain,
( xsd_string(sK29)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1855,c_932]) ).
tcf(c_1861,plain,
( xsd_integer(sK29)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1854,c_932]) ).
tcf(c_1866,plain,
( xsd_integer(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1861,c_940]) ).
tcf(c_1867,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1860,c_940]) ).
tcf(c_2738,plain,
( xsd_integer(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1866,c_860,c_852,c_786,c_786,c_778,c_778]) ).
tcf(c_2801,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1867,c_860,c_852,c_786,c_786,c_778,c_778]) ).
tcf(c_2844,plain,
cC130(iV16439),
inference(resolution,[status(thm)],[c_678,c_227]) ).
tcf(c_2848,plain,
cC108(iV16439),
inference(resolution,[status(thm)],[c_602,c_227]) ).
tcf(c_2854,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2801,c_2844]) ).
tcf(c_2856,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2854,c_2848]) ).
tcf(c_3237,plain,
( cC38(iV16448)
| cC36(iV16448) ),
inference(resolution,[status(thm)],[c_128,c_245]) ).
tcf(c_3238,plain,
cC38(iV16448),
inference(global_subsumption_just,[status(thm)],[c_3237,c_242,c_3237]) ).
tcf(c_3243,plain,
( cC38(iV16457)
| cC36(iV16457) ),
inference(resolution,[status(thm)],[c_128,c_279]) ).
tcf(c_3244,plain,
cC38(iV16457),
inference(global_subsumption_just,[status(thm)],[c_3243,c_274,c_3243]) ).
tcf(c_3249,plain,
( cC38(iV16460)
| cC36(iV16460) ),
inference(resolution,[status(thm)],[c_128,c_306]) ).
tcf(c_3250,plain,
cC38(iV16460),
inference(global_subsumption_just,[status(thm)],[c_3249,c_303,c_3249]) ).
tcf(c_3255,plain,
( cC38(iV16462)
| cC36(iV16462) ),
inference(resolution,[status(thm)],[c_128,c_328]) ).
tcf(c_3256,plain,
cC38(iV16462),
inference(global_subsumption_just,[status(thm)],[c_3255,c_327,c_3255]) ).
tcf(c_3261,plain,
( cC38(iV16465)
| cC36(iV16465) ),
inference(resolution,[status(thm)],[c_128,c_362]) ).
tcf(c_3262,plain,
cC38(iV16465),
inference(global_subsumption_just,[status(thm)],[c_3261,c_361,c_3261]) ).
tcf(c_3269,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2856,c_3238]) ).
tcf(c_3271,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16460)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3269,c_3244]) ).
tcf(c_3275,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3271,c_3250]) ).
tcf(c_3277,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3275,c_3256]) ).
tcf(c_3281,plain,
( xsd_string(sK29)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC98(iV16440) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3277,c_3262]) ).
tcf(c_3283,plain,
( ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC98(iV16440)
| ~ xsd_integer(sK29) ),
inference(resolution,[status(thm)],[c_544,c_3281]) ).
tcf(c_3284,plain,
( ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC98(iV16440) ),
inference(global_subsumption_just,[status(thm)],[c_3283,c_361,c_327,c_303,c_274,c_242,c_2738,c_2844,c_2848,c_3237,c_3243,c_3249,c_3255,c_3261,c_3283]) ).
tcf(c_4026,plain,
! [X0: $i] :
( cC56(X0)
| cC54(X0)
| cC40(X0)
| ~ cC42(X0) ),
inference(resolution,[status(thm)],[c_137,c_155]) ).
tcf(c_4131,plain,
! [X0: $i] :
( cC76(X0)
| cC74(X0)
| cC58(X0)
| ~ cC60(X0) ),
inference(resolution,[status(thm)],[c_167,c_188]) ).
tcf(c_5384,plain,
( cC76(iV16453)
| cC74(iV16453)
| ~ cC60(iV16453) ),
inference(resolution,[status(thm)],[c_4131,c_257]) ).
tcf(c_5385,plain,
( cC76(iV16453)
| ~ cC60(iV16453) ),
inference(global_subsumption_just,[status(thm)],[c_5384,c_258,c_5384]) ).
tcf(c_5782,plain,
( cC56(iV16455)
| cC54(iV16455)
| ~ cC42(iV16455) ),
inference(resolution,[status(thm)],[c_4026,c_264]) ).
tcf(c_6944,plain,
( ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ rR1(iV16439,iV16440) ),
inference(resolution,[status(thm)],[c_1004,c_3284]) ).
tcf(c_6945,plain,
( ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461) ),
inference(global_subsumption_just,[status(thm)],[c_6944,c_230,c_6944]) ).
tcf(c_16437,plain,
( cC76(iV16463)
| ~ rR1(iV16440,iV16463) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_16438,plain,
( cC56(iV16461)
| ~ rR1(iV16453,iV16461) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_16441,plain,
( cC56(iV16464)
| ~ rR1(iV16463,iV16464) ),
inference(instantiation,[status(thm)],[c_337]) ).
tcf(c_16517,plain,
( cC42(iV16455)
| cC8(iV16460)
| ~ rR1(iV16455,iV16460) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_16532,plain,
! [X0: $i] :
( cC12(iV16461)
| cC60(X0)
| ~ rR1(X0,iV16461) ),
inference(instantiation,[status(thm)],[c_164]) ).
tcf(c_16817,plain,
( cC60(iV16453)
| cC12(iV16461)
| ~ rR1(iV16453,iV16461) ),
inference(instantiation,[status(thm)],[c_16532]) ).
tcf(c_16818,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_16817,c_16517,c_16441,c_16438,c_16437,c_6945,c_5782,c_5385,c_239,c_262,c_269,c_273,c_307,c_317,c_343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/0.42 % Computer : n014.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Wed Sep 23 19:32:03 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/0.48 Running first-order theorem proving
% 0.15/0.48 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.50
% 0.15/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.50
% 0.25/0.50 % Detected problem language: tptp
% 0.25/0.52 % Proving...
% 4.42/1.84 % SZS status Started for theBenchmark.p
% 4.42/1.84 % SZS status Theorem for theBenchmark.p
% 4.42/1.84
% 4.42/1.84 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.42/1.84
% 4.42/1.84 % ------ iProver source info
% 4.42/1.84
% 4.42/1.84 % git: date: 2026-07-19 20:42:38 +0200
% 4.42/1.84 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.42/1.84 % git: non_committed_changes: false
% 4.42/1.84
% 4.42/1.84 % ------ Parsing...
% 4.42/1.84 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.42/1.84
% 4.42/1.84 % ------ Preprocessing... sf_s rm: 2 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 4.42/1.84
% 4.42/1.84 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 4.42/1.84 % ------ Proving...
% 4.42/1.84 % ------ Problem Properties
% 4.42/1.84
% 4.42/1.84 %
% 4.42/1.84 % clauses 242
% 4.42/1.84 % conjectures 0
% 4.42/1.84 % EPR 186
% 4.42/1.84 % Horn 213
% 4.42/1.84 % unary 78
% 4.42/1.84 % binary 115
% 4.42/1.84 % lits 463
% 4.42/1.84 % lits eq 0
% 4.42/1.84 % fd_pure 0
% 4.42/1.84 % fd_pseudo 0
% 4.42/1.84 % fd_cond 0
% 4.42/1.84 % fd_pseudo_cond 0
% 4.42/1.84 % AC symbols 0
% 4.42/1.84
% 4.42/1.84 % ------ Schedule dynamic 5 is on
% 4.42/1.84
% 4.42/1.84 % ------ no conjectures: strip conj schedule
% 4.42/1.84
% 4.42/1.84 % ------ no equalities: superposition off
% 4.42/1.84
% 4.42/1.84 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 4.42/1.84
% 4.42/1.84
% 4.42/1.84 % ------
% 4.42/1.84 % Current options:
% 4.42/1.84 % ------
% 4.42/1.84
% 4.42/1.84
% 4.42/1.84 %
% 4.42/1.84
% 4.42/1.84 % ------ Proving...
% 4.42/1.84 %
% 4.42/1.84
% 4.42/1.84 % SZS status Theorem for theBenchmark.p
% 4.42/1.84
% 4.42/1.84 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.42/1.85
% 4.42/1.85
%------------------------------------------------------------------------------