%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 : Thu Sep 24 12:59:48 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 151
% Syntax : Number of formulae : 596 ( 92 unt; 74 def)
% Number of atoms : 2132 ( 0 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 2625 (1089 ~;1091 |; 322 &)
% ( 122 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 55 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 153 ( 152 usr; 75 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-1 aty)
% Number of variables : 291 ( 278 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] :
( cC10(X)
<=> ( cC4(X)
& cC8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( cC108(X)
<=> ( ~ cC98(X)
& ~ cC106(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] :
( cC112(X)
<=> ( cC110(X)
& cC90(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] :
( cC114(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X] :
( cC130(X)
<=> ( ~ cC128(X)
& ~ cC122(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] :
( cC132(X)
<=> ( cC130(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X] :
( cC134(X)
<=> ( cC116(X)
& cC132(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X] :
( cC136(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] :
( cC152(X)
<=> ( ~ cC144(X)
& ~ cC150(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X] :
( cC154(X)
<=> ( cC152(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X] :
( cC156(X)
<=> ( cC138(X)
& cC154(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X] :
( cC16(X)
<=> ( cC10(X)
& cC14(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] :
( cC168(X)
<=> ( ~ cC162(X)
& ~ cC166(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X] :
( cC174(X)
<=> ( ~ cC172(X)
& cC168(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X] :
( cC180(X)
<=> ( cC174(X)
& ~ cC178(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] :
( cC22(X)
<=> ( cC20(X)
& cC16(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] :
( cC26(X)
<=> ( ~ cC2(X)
& ~ cC24(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] :
( cC32(X)
<=> ( ~ cC30(X)
& ~ cC2(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] :
( cC36(X)
<=> ( ~ cC34(X)
& ~ cC28(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] :
( cC46(X)
<=> ( ~ cC44(X)
& ~ cC12(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X] :
( cC52(X)
<=> ( ~ cC50(X)
& ~ cC12(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& ~ cC48(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [X] :
( cC64(X)
<=> ( cC60(X)
& cC62(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC18(X)
& ~ cC66(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [X] :
( cC74(X)
<=> ( ~ cC72(X)
& ~ cC18(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [X] :
( cC78(X)
<=> ( ~ cC76(X)
& ~ cC70(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [X] :
( cC80(X)
<=> ( cC78(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [X] :
( cC82(X)
<=> ( cC64(X)
& cC80(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [X] :
( cC88(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [X] :
( cC90(X)
<=> ( cC86(X)
& cC88(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
~ cC98(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,axiom,
~ cC122(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,axiom,
~ cC34(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
~ cC28(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
~ cC70(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
~ cC178(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
~ cC162(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,axiom,
~ cC166(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
~ cC150(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,axiom,
~ cC54(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,axiom,
~ cC106(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,axiom,
~ cC144(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,axiom,
~ cC48(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
~ cC76(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,axiom,
~ cC128(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,axiom,
~ cC172(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
rR1(iV21026,iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,axiom,
rR1(iV21026,iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
~ cC26(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
~ cC32(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
~ cC2(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
~ cC46(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,axiom,
~ cC12(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,axiom,
~ cC52(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,axiom,
~ cC68(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,axiom,
~ cC74(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,axiom,
~ cC18(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f243]) ).
fof(f245,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f246,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f247,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f248,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f249,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f248]) ).
fof(f250,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f251,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f252,plain,
! [X] :
( ( ~ cC4(X)
| ~ cC8(X)
| cC10(X) )
& ( ( cC4(X)
& cC8(X) )
| ~ cC10(X) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f253,plain,
( ! [X] :
( ~ cC4(X)
| ~ cC8(X)
| cC10(X) )
& ! [X] :
( ( cC4(X)
& cC8(X) )
| ~ cC10(X) ) ),
inference(miniscoping,[status(thm)],[f252]) ).
fof(f254,plain,
! [X0] :
( cC8(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f256,plain,
! [X0] :
( ~ cC4(X0)
| ~ cC8(X0)
| cC10(X0) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f274,plain,
! [X] :
( ( cC98(X)
| cC106(X)
| cC108(X) )
& ( ( ~ cC98(X)
& ~ cC106(X) )
| ~ cC108(X) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f275,plain,
( ! [X] :
( cC98(X)
| cC106(X)
| cC108(X) )
& ! [X] :
( ( ~ cC98(X)
& ~ cC106(X) )
| ~ cC108(X) ) ),
inference(miniscoping,[status(thm)],[f274]) ).
fof(f278,plain,
! [X0] :
( cC98(X0)
| cC106(X0)
| cC108(X0) ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f279,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC108(X)
| cC110(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f280,plain,
( ! [X] :
( ~ cTOP(X)
| ~ cC108(X)
| cC110(X) )
& ! [X] :
( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(miniscoping,[status(thm)],[f279]) ).
fof(f283,plain,
! [X0] :
( ~ cTOP(X0)
| ~ cC108(X0)
| cC110(X0) ),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f284,plain,
! [X] :
( ( ~ cC110(X)
| ~ cC90(X)
| cC112(X) )
& ( ( cC110(X)
& cC90(X) )
| ~ cC112(X) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f285,plain,
( ! [X] :
( ~ cC110(X)
| ~ cC90(X)
| cC112(X) )
& ! [X] :
( ( cC110(X)
& cC90(X) )
| ~ cC112(X) ) ),
inference(miniscoping,[status(thm)],[f284]) ).
fof(f288,plain,
! [X0] :
( ~ cC110(X0)
| ~ cC90(X0)
| cC112(X0) ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f289,plain,
! [X] :
( ( ~ cTOP(X)
| cC114(X) )
& ( cTOP(X)
| ~ cC114(X) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f290,plain,
( ! [X] :
( ~ cTOP(X)
| cC114(X) )
& ! [X] :
( cTOP(X)
| ~ cC114(X) ) ),
inference(miniscoping,[status(thm)],[f289]) ).
fof(f292,plain,
! [X0] :
( ~ cTOP(X0)
| cC114(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f293,plain,
! [X] :
( ( ~ cC112(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f294,plain,
( ! [X] :
( ~ cC112(X)
| ~ cC114(X)
| cC116(X) )
& ! [X] :
( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(miniscoping,[status(thm)],[f293]) ).
fof(f297,plain,
! [X0] :
( ~ cC112(X0)
| ~ cC114(X0)
| cC116(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f332,plain,
! [X] :
( ( cC128(X)
| cC122(X)
| cC130(X) )
& ( ( ~ cC128(X)
& ~ cC122(X) )
| ~ cC130(X) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f333,plain,
( ! [X] :
( cC128(X)
| cC122(X)
| cC130(X) )
& ! [X] :
( ( ~ cC128(X)
& ~ cC122(X) )
| ~ cC130(X) ) ),
inference(miniscoping,[status(thm)],[f332]) ).
fof(f336,plain,
! [X0] :
( cC128(X0)
| cC122(X0)
| cC130(X0) ),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f337,plain,
! [X] :
( ( ~ cC130(X)
| ~ cTOP(X)
| cC132(X) )
& ( ( cC130(X)
& cTOP(X) )
| ~ cC132(X) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f338,plain,
( ! [X] :
( ~ cC130(X)
| ~ cTOP(X)
| cC132(X) )
& ! [X] :
( ( cC130(X)
& cTOP(X) )
| ~ cC132(X) ) ),
inference(miniscoping,[status(thm)],[f337]) ).
fof(f340,plain,
! [X0] :
( cC130(X0)
| ~ cC132(X0) ),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f341,plain,
! [X0] :
( ~ cC130(X0)
| ~ cTOP(X0)
| cC132(X0) ),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f342,plain,
! [X] :
( ( ~ cC116(X)
| ~ cC132(X)
| cC134(X) )
& ( ( cC116(X)
& cC132(X) )
| ~ cC134(X) ) ),
inference(NNF_transformation,[status(thm)],[f20]) ).
fof(f343,plain,
( ! [X] :
( ~ cC116(X)
| ~ cC132(X)
| cC134(X) )
& ! [X] :
( ( cC116(X)
& cC132(X) )
| ~ cC134(X) ) ),
inference(miniscoping,[status(thm)],[f342]) ).
fof(f346,plain,
! [X0] :
( ~ cC116(X0)
| ~ cC132(X0)
| cC134(X0) ),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f347,plain,
! [X] :
( ( ~ cTOP(X)
| cC136(X) )
& ( cTOP(X)
| ~ cC136(X) ) ),
inference(NNF_transformation,[status(thm)],[f21]) ).
fof(f348,plain,
( ! [X] :
( ~ cTOP(X)
| cC136(X) )
& ! [X] :
( cTOP(X)
| ~ cC136(X) ) ),
inference(miniscoping,[status(thm)],[f347]) ).
fof(f350,plain,
! [X0] :
( ~ cTOP(X0)
| cC136(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f351,plain,
! [X] :
( ( ~ cC134(X)
| ~ cC136(X)
| cC138(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f352,plain,
( ! [X] :
( ~ cC134(X)
| ~ cC136(X)
| cC138(X) )
& ! [X] :
( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(miniscoping,[status(thm)],[f351]) ).
fof(f355,plain,
! [X0] :
( ~ cC134(X0)
| ~ cC136(X0)
| cC138(X0) ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f356,plain,
! [X] :
( ( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(NNF_transformation,[status(thm)],[f23]) ).
fof(f357,plain,
( ! [X] :
( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ! [X] :
( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(miniscoping,[status(thm)],[f356]) ).
fof(f358,plain,
( ! [X] :
( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ! [X] :
( ( ~ cC12(sK6_skl(X))
& rR1(X,sK6_skl(X)) )
| ~ cC14(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(Y,sK6_skl(X))],[f357]) ).
fof(f361,plain,
! [X0,X1] :
( cC12(X1)
| ~ rR1(X0,X1)
| cC14(X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f396,plain,
! [X] :
( ( cC144(X)
| cC150(X)
| cC152(X) )
& ( ( ~ cC144(X)
& ~ cC150(X) )
| ~ cC152(X) ) ),
inference(NNF_transformation,[status(thm)],[f30]) ).
fof(f397,plain,
( ! [X] :
( cC144(X)
| cC150(X)
| cC152(X) )
& ! [X] :
( ( ~ cC144(X)
& ~ cC150(X) )
| ~ cC152(X) ) ),
inference(miniscoping,[status(thm)],[f396]) ).
fof(f400,plain,
! [X0] :
( cC144(X0)
| cC150(X0)
| cC152(X0) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f401,plain,
! [X] :
( ( ~ cC152(X)
| ~ cTOP(X)
| cC154(X) )
& ( ( cC152(X)
& cTOP(X) )
| ~ cC154(X) ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f402,plain,
( ! [X] :
( ~ cC152(X)
| ~ cTOP(X)
| cC154(X) )
& ! [X] :
( ( cC152(X)
& cTOP(X) )
| ~ cC154(X) ) ),
inference(miniscoping,[status(thm)],[f401]) ).
fof(f404,plain,
! [X0] :
( cC152(X0)
| ~ cC154(X0) ),
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f405,plain,
! [X0] :
( ~ cC152(X0)
| ~ cTOP(X0)
| cC154(X0) ),
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f406,plain,
! [X] :
( ( ~ cC138(X)
| ~ cC154(X)
| cC156(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(NNF_transformation,[status(thm)],[f32]) ).
fof(f407,plain,
( ! [X] :
( ~ cC138(X)
| ~ cC154(X)
| cC156(X) )
& ! [X] :
( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(miniscoping,[status(thm)],[f406]) ).
fof(f410,plain,
! [X0] :
( ~ cC138(X0)
| ~ cC154(X0)
| cC156(X0) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f411,plain,
! [X] :
( ( ~ cC156(X)
| ~ cC22(X)
| cC158(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(NNF_transformation,[status(thm)],[f33]) ).
fof(f412,plain,
( ! [X] :
( ~ cC156(X)
| ~ cC22(X)
| cC158(X) )
& ! [X] :
( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(miniscoping,[status(thm)],[f411]) ).
fof(f413,plain,
! [X0] :
( cC22(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f415,plain,
! [X0] :
( ~ cC156(X0)
| ~ cC22(X0)
| cC158(X0) ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f416,plain,
! [X] :
( ( ~ cC10(X)
| ~ cC14(X)
| cC16(X) )
& ( ( cC10(X)
& cC14(X) )
| ~ cC16(X) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f417,plain,
( ! [X] :
( ~ cC10(X)
| ~ cC14(X)
| cC16(X) )
& ! [X] :
( ( cC10(X)
& cC14(X) )
| ~ cC16(X) ) ),
inference(miniscoping,[status(thm)],[f416]) ).
fof(f418,plain,
! [X0] :
( cC14(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f419,plain,
! [X0] :
( cC10(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f420,plain,
! [X0] :
( ~ cC10(X0)
| ~ cC14(X0)
| cC16(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f445,plain,
! [X] :
( ( cC162(X)
| cC166(X)
| cC168(X) )
& ( ( ~ cC162(X)
& ~ cC166(X) )
| ~ cC168(X) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f446,plain,
( ! [X] :
( cC162(X)
| cC166(X)
| cC168(X) )
& ! [X] :
( ( ~ cC162(X)
& ~ cC166(X) )
| ~ cC168(X) ) ),
inference(miniscoping,[status(thm)],[f445]) ).
fof(f449,plain,
! [X0] :
( cC162(X0)
| cC166(X0)
| cC168(X0) ),
inference(cnf_transformation,[status(thm)],[f446]) ).
fof(f462,plain,
! [X] :
( ( cC172(X)
| ~ cC168(X)
| cC174(X) )
& ( ( ~ cC172(X)
& cC168(X) )
| ~ cC174(X) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f463,plain,
( ! [X] :
( cC172(X)
| ~ cC168(X)
| cC174(X) )
& ! [X] :
( ( ~ cC172(X)
& cC168(X) )
| ~ cC174(X) ) ),
inference(miniscoping,[status(thm)],[f462]) ).
fof(f466,plain,
! [X0] :
( cC172(X0)
| ~ cC168(X0)
| cC174(X0) ),
inference(cnf_transformation,[status(thm)],[f463]) ).
fof(f479,plain,
! [X] :
( ( ~ cC174(X)
| cC178(X)
| cC180(X) )
& ( ( cC174(X)
& ~ cC178(X) )
| ~ cC180(X) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f480,plain,
( ! [X] :
( ~ cC174(X)
| cC178(X)
| cC180(X) )
& ! [X] :
( ( cC174(X)
& ~ cC178(X) )
| ~ cC180(X) ) ),
inference(miniscoping,[status(thm)],[f479]) ).
fof(f483,plain,
! [X0] :
( ~ cC174(X0)
| cC178(X0)
| cC180(X0) ),
inference(cnf_transformation,[status(thm)],[f480]) ).
fof(f490,plain,
! [X] :
( ( ~ cC20(X)
| ~ cC16(X)
| cC22(X) )
& ( ( cC20(X)
& cC16(X) )
| ~ cC22(X) ) ),
inference(NNF_transformation,[status(thm)],[f47]) ).
fof(f491,plain,
( ! [X] :
( ~ cC20(X)
| ~ cC16(X)
| cC22(X) )
& ! [X] :
( ( cC20(X)
& cC16(X) )
| ~ cC22(X) ) ),
inference(miniscoping,[status(thm)],[f490]) ).
fof(f492,plain,
! [X0] :
( cC16(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f493,plain,
! [X0] :
( cC20(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f501,plain,
! [X] :
( ( cC2(X)
| cC24(X)
| cC26(X) )
& ( ( ~ cC2(X)
& ~ cC24(X) )
| ~ cC26(X) ) ),
inference(NNF_transformation,[status(thm)],[f49]) ).
fof(f502,plain,
( ! [X] :
( cC2(X)
| cC24(X)
| cC26(X) )
& ! [X] :
( ( ~ cC2(X)
& ~ cC24(X) )
| ~ cC26(X) ) ),
inference(miniscoping,[status(thm)],[f501]) ).
fof(f505,plain,
! [X0] :
( cC2(X0)
| cC24(X0)
| cC26(X0) ),
inference(cnf_transformation,[status(thm)],[f502]) ).
fof(f518,plain,
! [X] :
( ( cC30(X)
| cC2(X)
| cC32(X) )
& ( ( ~ cC30(X)
& ~ cC2(X) )
| ~ cC32(X) ) ),
inference(NNF_transformation,[status(thm)],[f52]) ).
fof(f519,plain,
( ! [X] :
( cC30(X)
| cC2(X)
| cC32(X) )
& ! [X] :
( ( ~ cC30(X)
& ~ cC2(X) )
| ~ cC32(X) ) ),
inference(miniscoping,[status(thm)],[f518]) ).
fof(f522,plain,
! [X0] :
( cC30(X0)
| cC2(X0)
| cC32(X0) ),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f529,plain,
! [X] :
( ( cC34(X)
| cC28(X)
| cC36(X) )
& ( ( ~ cC34(X)
& ~ cC28(X) )
| ~ cC36(X) ) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f530,plain,
( ! [X] :
( cC34(X)
| cC28(X)
| cC36(X) )
& ! [X] :
( ( ~ cC34(X)
& ~ cC28(X) )
| ~ cC36(X) ) ),
inference(miniscoping,[status(thm)],[f529]) ).
fof(f533,plain,
! [X0] :
( cC34(X0)
| cC28(X0)
| cC36(X0) ),
inference(cnf_transformation,[status(thm)],[f530]) ).
fof(f534,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f535,plain,
( ! [X] :
( ~ cTOP(X)
| ~ cC36(X)
| cC38(X) )
& ! [X] :
( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(miniscoping,[status(thm)],[f534]) ).
fof(f536,plain,
! [X0] :
( cC36(X0)
| ~ cC38(X0) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f537,plain,
! [X0] :
( cTOP(X0)
| ~ cC38(X0) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f538,plain,
! [X0] :
( ~ cTOP(X0)
| ~ cC36(X0)
| cC38(X0) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f539,plain,
! [X] :
( ( ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC4(X) ) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f540,plain,
( ! [X] :
( ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ! [X] :
( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC4(X) ) ),
inference(miniscoping,[status(thm)],[f539]) ).
fof(f541,plain,
( ! [X] :
( ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ! [X] :
( ( ~ cC2(sK24_skl(X))
& rR1(X,sK24_skl(X)) )
| ~ cC4(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(Y,sK24_skl(X))],[f540]) ).
fof(f544,plain,
! [X0,X1] :
( cC2(X1)
| ~ rR1(X0,X1)
| cC4(X0) ),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f545,plain,
! [X] :
( ( ~ cTOP(X)
| cC40(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(NNF_transformation,[status(thm)],[f57]) ).
fof(f546,plain,
( ! [X] :
( ~ cTOP(X)
| cC40(X) )
& ! [X] :
( cTOP(X)
| ~ cC40(X) ) ),
inference(miniscoping,[status(thm)],[f545]) ).
fof(f548,plain,
! [X0] :
( ~ cTOP(X0)
| cC40(X0) ),
inference(cnf_transformation,[status(thm)],[f546]) ).
fof(f549,plain,
! [X] :
( ( ~ cC38(X)
| ~ cC40(X)
| cC42(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f550,plain,
( ! [X] :
( ~ cC38(X)
| ~ cC40(X)
| cC42(X) )
& ! [X] :
( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(miniscoping,[status(thm)],[f549]) ).
fof(f551,plain,
! [X0] :
( cC40(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[status(thm)],[f550]) ).
fof(f553,plain,
! [X0] :
( ~ cC38(X0)
| ~ cC40(X0)
| cC42(X0) ),
inference(cnf_transformation,[status(thm)],[f550]) ).
fof(f560,plain,
! [X] :
( ( cC44(X)
| cC12(X)
| cC46(X) )
& ( ( ~ cC44(X)
& ~ cC12(X) )
| ~ cC46(X) ) ),
inference(NNF_transformation,[status(thm)],[f60]) ).
fof(f561,plain,
( ! [X] :
( cC44(X)
| cC12(X)
| cC46(X) )
& ! [X] :
( ( ~ cC44(X)
& ~ cC12(X) )
| ~ cC46(X) ) ),
inference(miniscoping,[status(thm)],[f560]) ).
fof(f564,plain,
! [X0] :
( cC44(X0)
| cC12(X0)
| cC46(X0) ),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f577,plain,
! [X] :
( ( cC50(X)
| cC12(X)
| cC52(X) )
& ( ( ~ cC50(X)
& ~ cC12(X) )
| ~ cC52(X) ) ),
inference(NNF_transformation,[status(thm)],[f63]) ).
fof(f578,plain,
( ! [X] :
( cC50(X)
| cC12(X)
| cC52(X) )
& ! [X] :
( ( ~ cC50(X)
& ~ cC12(X) )
| ~ cC52(X) ) ),
inference(miniscoping,[status(thm)],[f577]) ).
fof(f581,plain,
! [X0] :
( cC50(X0)
| cC12(X0)
| cC52(X0) ),
inference(cnf_transformation,[status(thm)],[f578]) ).
fof(f588,plain,
! [X] :
( ( cC54(X)
| cC48(X)
| cC56(X) )
& ( ( ~ cC54(X)
& ~ cC48(X) )
| ~ cC56(X) ) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f589,plain,
( ! [X] :
( cC54(X)
| cC48(X)
| cC56(X) )
& ! [X] :
( ( ~ cC54(X)
& ~ cC48(X) )
| ~ cC56(X) ) ),
inference(miniscoping,[status(thm)],[f588]) ).
fof(f592,plain,
! [X0] :
( cC54(X0)
| cC48(X0)
| cC56(X0) ),
inference(cnf_transformation,[status(thm)],[f589]) ).
fof(f593,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC56(X)
| cC58(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(NNF_transformation,[status(thm)],[f66]) ).
fof(f594,plain,
( ! [X] :
( ~ cTOP(X)
| ~ cC56(X)
| cC58(X) )
& ! [X] :
( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(miniscoping,[status(thm)],[f593]) ).
fof(f595,plain,
! [X0] :
( cC56(X0)
| ~ cC58(X0) ),
inference(cnf_transformation,[status(thm)],[f594]) ).
fof(f597,plain,
! [X0] :
( ~ cTOP(X0)
| ~ cC56(X0)
| cC58(X0) ),
inference(cnf_transformation,[status(thm)],[f594]) ).
fof(f598,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC58(X)
| cC60(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f599,plain,
( ! [X] :
( ~ cC42(X)
| ~ cC58(X)
| cC60(X) )
& ! [X] :
( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(miniscoping,[status(thm)],[f598]) ).
fof(f602,plain,
! [X0] :
( ~ cC42(X0)
| ~ cC58(X0)
| cC60(X0) ),
inference(cnf_transformation,[status(thm)],[f599]) ).
fof(f603,plain,
! [X] :
( ( ~ cTOP(X)
| cC62(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f604,plain,
( ! [X] :
( ~ cTOP(X)
| cC62(X) )
& ! [X] :
( cTOP(X)
| ~ cC62(X) ) ),
inference(miniscoping,[status(thm)],[f603]) ).
fof(f606,plain,
! [X0] :
( ~ cTOP(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(thm)],[f604]) ).
fof(f607,plain,
! [X] :
( ( ~ cC60(X)
| ~ cC62(X)
| cC64(X) )
& ( ( cC60(X)
& cC62(X) )
| ~ cC64(X) ) ),
inference(NNF_transformation,[status(thm)],[f69]) ).
fof(f608,plain,
( ! [X] :
( ~ cC60(X)
| ~ cC62(X)
| cC64(X) )
& ! [X] :
( ( cC60(X)
& cC62(X) )
| ~ cC64(X) ) ),
inference(miniscoping,[status(thm)],[f607]) ).
fof(f609,plain,
! [X0] :
( cC62(X0)
| ~ cC64(X0) ),
inference(cnf_transformation,[status(thm)],[f608]) ).
fof(f611,plain,
! [X0] :
( ~ cC60(X0)
| ~ cC62(X0)
| cC64(X0) ),
inference(cnf_transformation,[status(thm)],[f608]) ).
fof(f618,plain,
! [X] :
( ( cC18(X)
| cC66(X)
| cC68(X) )
& ( ( ~ cC18(X)
& ~ cC66(X) )
| ~ cC68(X) ) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f619,plain,
( ! [X] :
( cC18(X)
| cC66(X)
| cC68(X) )
& ! [X] :
( ( ~ cC18(X)
& ~ cC66(X) )
| ~ cC68(X) ) ),
inference(miniscoping,[status(thm)],[f618]) ).
fof(f622,plain,
! [X0] :
( cC18(X0)
| cC66(X0)
| cC68(X0) ),
inference(cnf_transformation,[status(thm)],[f619]) ).
fof(f635,plain,
! [X] :
( ( cC72(X)
| cC18(X)
| cC74(X) )
& ( ( ~ cC72(X)
& ~ cC18(X) )
| ~ cC74(X) ) ),
inference(NNF_transformation,[status(thm)],[f74]) ).
fof(f636,plain,
( ! [X] :
( cC72(X)
| cC18(X)
| cC74(X) )
& ! [X] :
( ( ~ cC72(X)
& ~ cC18(X) )
| ~ cC74(X) ) ),
inference(miniscoping,[status(thm)],[f635]) ).
fof(f639,plain,
! [X0] :
( cC72(X0)
| cC18(X0)
| cC74(X0) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f646,plain,
! [X] :
( ( cC76(X)
| cC70(X)
| cC78(X) )
& ( ( ~ cC76(X)
& ~ cC70(X) )
| ~ cC78(X) ) ),
inference(NNF_transformation,[status(thm)],[f76]) ).
fof(f647,plain,
( ! [X] :
( cC76(X)
| cC70(X)
| cC78(X) )
& ! [X] :
( ( ~ cC76(X)
& ~ cC70(X) )
| ~ cC78(X) ) ),
inference(miniscoping,[status(thm)],[f646]) ).
fof(f650,plain,
! [X0] :
( cC76(X0)
| cC70(X0)
| cC78(X0) ),
inference(cnf_transformation,[status(thm)],[f647]) ).
fof(f657,plain,
! [X] :
( ( ~ cC78(X)
| ~ cTOP(X)
| cC80(X) )
& ( ( cC78(X)
& cTOP(X) )
| ~ cC80(X) ) ),
inference(NNF_transformation,[status(thm)],[f78]) ).
fof(f658,plain,
( ! [X] :
( ~ cC78(X)
| ~ cTOP(X)
| cC80(X) )
& ! [X] :
( ( cC78(X)
& cTOP(X) )
| ~ cC80(X) ) ),
inference(miniscoping,[status(thm)],[f657]) ).
fof(f660,plain,
! [X0] :
( cC78(X0)
| ~ cC80(X0) ),
inference(cnf_transformation,[status(thm)],[f658]) ).
fof(f661,plain,
! [X0] :
( ~ cC78(X0)
| ~ cTOP(X0)
| cC80(X0) ),
inference(cnf_transformation,[status(thm)],[f658]) ).
fof(f662,plain,
! [X] :
( ( ~ cC64(X)
| ~ cC80(X)
| cC82(X) )
& ( ( cC64(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(NNF_transformation,[status(thm)],[f79]) ).
fof(f663,plain,
( ! [X] :
( ~ cC64(X)
| ~ cC80(X)
| cC82(X) )
& ! [X] :
( ( cC64(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(miniscoping,[status(thm)],[f662]) ).
fof(f666,plain,
! [X0] :
( ~ cC64(X0)
| ~ cC80(X0)
| cC82(X0) ),
inference(cnf_transformation,[status(thm)],[f663]) ).
fof(f667,plain,
! [X] :
( ( ~ cTOP(X)
| cC84(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f668,plain,
( ! [X] :
( ~ cTOP(X)
| cC84(X) )
& ! [X] :
( cTOP(X)
| ~ cC84(X) ) ),
inference(miniscoping,[status(thm)],[f667]) ).
fof(f670,plain,
! [X0] :
( ~ cTOP(X0)
| cC84(X0) ),
inference(cnf_transformation,[status(thm)],[f668]) ).
fof(f671,plain,
! [X] :
( ( ~ cC84(X)
| ~ cC82(X)
| cC86(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f672,plain,
( ! [X] :
( ~ cC84(X)
| ~ cC82(X)
| cC86(X) )
& ! [X] :
( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(miniscoping,[status(thm)],[f671]) ).
fof(f675,plain,
! [X0] :
( ~ cC84(X0)
| ~ cC82(X0)
| cC86(X0) ),
inference(cnf_transformation,[status(thm)],[f672]) ).
fof(f676,plain,
! [X] :
( ( ~ cTOP(X)
| cC88(X) )
& ( cTOP(X)
| ~ cC88(X) ) ),
inference(NNF_transformation,[status(thm)],[f82]) ).
fof(f677,plain,
( ! [X] :
( ~ cTOP(X)
| cC88(X) )
& ! [X] :
( cTOP(X)
| ~ cC88(X) ) ),
inference(miniscoping,[status(thm)],[f676]) ).
fof(f679,plain,
! [X0] :
( ~ cTOP(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(thm)],[f677]) ).
fof(f680,plain,
! [X] :
( ( ~ cC86(X)
| ~ cC88(X)
| cC90(X) )
& ( ( cC86(X)
& cC88(X) )
| ~ cC90(X) ) ),
inference(NNF_transformation,[status(thm)],[f83]) ).
fof(f681,plain,
( ! [X] :
( ~ cC86(X)
| ~ cC88(X)
| cC90(X) )
& ! [X] :
( ( cC86(X)
& cC88(X) )
| ~ cC90(X) ) ),
inference(miniscoping,[status(thm)],[f680]) ).
fof(f684,plain,
! [X0] :
( ~ cC86(X0)
| ~ cC88(X0)
| cC90(X0) ),
inference(cnf_transformation,[status(thm)],[f681]) ).
fof(f702,plain,
! [X] :
( ( ~ cC180(X)
| ~ cC158(X)
| cTEST(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(NNF_transformation,[status(thm)],[f87]) ).
fof(f703,plain,
( ! [X] :
( ~ cC180(X)
| ~ cC158(X)
| cTEST(X) )
& ! [X] :
( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(miniscoping,[status(thm)],[f702]) ).
fof(f704,plain,
! [X0] :
( cC158(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f703]) ).
fof(f709,plain,
cTOP(iV21026),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f710,plain,
cTEST(iV21026),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f713,plain,
~ cC98(iV21026),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f714,plain,
~ cC122(iV21026),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f719,plain,
~ cC34(iV21026),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f720,plain,
~ cC28(iV21026),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f723,plain,
~ cC70(iV21026),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f724,plain,
~ cC178(iV21026),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f725,plain,
~ cC162(iV21026),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f726,plain,
~ cC166(iV21026),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f739,plain,
~ cC150(iV21026),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f740,plain,
~ cC54(iV21026),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f741,plain,
~ cC106(iV21026),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f742,plain,
~ cC144(iV21026),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f743,plain,
~ cC48(iV21026),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f744,plain,
~ cC76(iV21026),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f747,plain,
~ cC128(iV21026),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f748,plain,
~ cC172(iV21026),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f759,plain,
rR1(iV21026,iV21027),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f761,plain,
rR1(iV21026,iV21029),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f762,plain,
~ cC26(iV21027),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f774,plain,
~ cC32(iV21027),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f790,plain,
~ cC2(iV21027),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f797,plain,
~ cC46(iV21029),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f805,plain,
~ cC12(iV21029),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f810,plain,
~ cC52(iV21029),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f837,plain,
~ cC68(iV21030),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f838,plain,
~ cC74(iV21030),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f849,plain,
~ cC18(iV21030),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f890,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)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f244]) ).
fof(f891,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)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f890]) ).
fof(f892,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)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f891]) ).
fof(f893,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_integer(sK38_skl)
| ~ xsd_string(sK38_skl) )
& ( ~ xsd_integer(sK38_skl)
| xsd_string(sK38_skl) ) )
| cowlNothing(sK37_skl)
| ~ cowlThing(sK36_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl,sK38_skl]),skolemize(X,sK36_skl),skolemize(X,sK37_skl),skolemize(X,sK38_skl)],[f892]) ).
fof(f894,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_integer(sK38_skl)
| xsd_string(sK38_skl)
| cowlNothing(sK37_skl)
| ~ cowlThing(sK36_skl) ),
inference(cnf_transformation,[status(thm)],[f893]) ).
fof(f895,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_integer(sK38_skl)
| ~ xsd_string(sK38_skl)
| cowlNothing(sK37_skl)
| ~ cowlThing(sK36_skl) ),
inference(cnf_transformation,[status(thm)],[f893]) ).
fof(f896,definition,
( sQ0_spl
<=> cowlThing(sK36_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f898,plain,
( sQ0_spl
| ~ cowlThing(sK36_skl) ),
inference(component_clause,[status(thm)],[f896]) ).
fof(f899,definition,
( sQ1_spl
<=> cowlNothing(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f900,plain,
( ~ sQ1_spl
| cowlNothing(sK37_skl) ),
inference(component_clause,[status(thm)],[f899]) ).
fof(f902,definition,
( sQ2_spl
<=> xsd_string(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f903,plain,
( ~ sQ2_spl
| xsd_string(sK38_skl) ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f904,plain,
( sQ2_spl
| ~ xsd_string(sK38_skl) ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f905,definition,
( sQ3_spl
<=> xsd_integer(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f906,plain,
( ~ sQ3_spl
| xsd_integer(sK38_skl) ),
inference(component_clause,[status(thm)],[f905]) ).
fof(f908,definition,
( sQ4_spl
<=> cowlThing(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f910,plain,
( sQ4_spl
| ~ cowlThing(iV21026) ),
inference(component_clause,[status(thm)],[f908]) ).
fof(f911,definition,
( sQ5_spl
<=> cC84(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f913,plain,
( sQ5_spl
| ~ cC84(iV21026) ),
inference(component_clause,[status(thm)],[f911]) ).
fof(f914,definition,
( sQ6_spl
<=> cC16(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f917,definition,
( sQ7_spl
<=> cC36(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f919,plain,
( sQ7_spl
| ~ cC36(iV21026) ),
inference(component_clause,[status(thm)],[f917]) ).
fof(f920,definition,
( sQ8_spl
<=> cC42(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f922,plain,
( sQ8_spl
| ~ cC42(iV21026) ),
inference(component_clause,[status(thm)],[f920]) ).
fof(f923,definition,
( sQ9_spl
<=> cC88(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f925,plain,
( sQ9_spl
| ~ cC88(iV21026) ),
inference(component_clause,[status(thm)],[f923]) ).
fof(f926,definition,
( sQ10_spl
<=> cC86(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f927,plain,
( ~ sQ10_spl
| cC86(iV21026) ),
inference(component_clause,[status(thm)],[f926]) ).
fof(f929,definition,
( sQ11_spl
<=> cC174(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f931,plain,
( sQ11_spl
| ~ cC174(iV21026) ),
inference(component_clause,[status(thm)],[f929]) ).
fof(f932,definition,
( sQ12_spl
<=> cC20(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f934,plain,
( sQ12_spl
| ~ cC20(iV21026) ),
inference(component_clause,[status(thm)],[f932]) ).
fof(f935,definition,
( sQ13_spl
<=> cC156(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f936,plain,
( ~ sQ13_spl
| cC156(iV21026) ),
inference(component_clause,[status(thm)],[f935]) ).
fof(f938,definition,
( sQ14_spl
<=> cC60(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f939,plain,
( ~ sQ14_spl
| cC60(iV21026) ),
inference(component_clause,[status(thm)],[f938]) ).
fof(f941,definition,
( sQ15_spl
<=> cC38(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( ~ sQ15_spl
| cC38(iV21026) ),
inference(component_clause,[status(thm)],[f941]) ).
fof(f944,definition,
( sQ16_spl
<=> cC158(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f947,definition,
( sQ17_spl
<=> cC10(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f949,plain,
( sQ17_spl
| ~ cC10(iV21026) ),
inference(component_clause,[status(thm)],[f947]) ).
fof(f950,definition,
( sQ18_spl
<=> cC134(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( ~ sQ18_spl
| cC134(iV21026) ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f953,definition,
( sQ19_spl
<=> cC22(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f954,plain,
( ~ sQ19_spl
| cC22(iV21026) ),
inference(component_clause,[status(thm)],[f953]) ).
fof(f955,plain,
( sQ19_spl
| ~ cC22(iV21026) ),
inference(component_clause,[status(thm)],[f953]) ).
fof(f956,definition,
( sQ20_spl
<=> cC168(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f958,plain,
( sQ20_spl
| ~ cC168(iV21026) ),
inference(component_clause,[status(thm)],[f956]) ).
fof(f959,definition,
( sQ21_spl
<=> cC56(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f961,plain,
( sQ21_spl
| ~ cC56(iV21026) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f962,definition,
( sQ22_spl
<=> cC78(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f964,plain,
( sQ22_spl
| ~ cC78(iV21026) ),
inference(component_clause,[status(thm)],[f962]) ).
fof(f965,definition,
( sQ23_spl
<=> cC58(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f966,plain,
( ~ sQ23_spl
| cC58(iV21026) ),
inference(component_clause,[status(thm)],[f965]) ).
fof(f968,definition,
( sQ24_spl
<=> cC152(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( sQ24_spl
| ~ cC152(iV21026) ),
inference(component_clause,[status(thm)],[f968]) ).
fof(f971,definition,
( sQ25_spl
<=> cC40(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f973,plain,
( sQ25_spl
| ~ cC40(iV21026) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,definition,
( sQ26_spl
<=> cC132(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( ~ sQ26_spl
| cC132(iV21026) ),
inference(component_clause,[status(thm)],[f974]) ).
fof(f977,definition,
( sQ27_spl
<=> cC130(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f979,plain,
( sQ27_spl
| ~ cC130(iV21026) ),
inference(component_clause,[status(thm)],[f977]) ).
fof(f980,definition,
( sQ28_spl
<=> cC62(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( sQ28_spl
| ~ cC62(iV21026) ),
inference(component_clause,[status(thm)],[f980]) ).
fof(f983,definition,
( sQ29_spl
<=> cC154(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f984,plain,
( ~ sQ29_spl
| cC154(iV21026) ),
inference(component_clause,[status(thm)],[f983]) ).
fof(f986,definition,
( sQ30_spl
<=> cC80(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f987,plain,
( ~ sQ30_spl
| cC80(iV21026) ),
inference(component_clause,[status(thm)],[f986]) ).
fof(f989,definition,
( sQ31_spl
<=> cC8(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f991,plain,
( sQ31_spl
| ~ cC8(iV21026) ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f992,definition,
( sQ32_spl
<=> cC136(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f994,plain,
( sQ32_spl
| ~ cC136(iV21026) ),
inference(component_clause,[status(thm)],[f992]) ).
fof(f995,definition,
( sQ33_spl
<=> cC112(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f996,plain,
( ~ sQ33_spl
| cC112(iV21026) ),
inference(component_clause,[status(thm)],[f995]) ).
fof(f998,definition,
( sQ34_spl
<=> cC180(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1000,plain,
( sQ34_spl
| ~ cC180(iV21026) ),
inference(component_clause,[status(thm)],[f998]) ).
fof(f1001,definition,
( sQ35_spl
<=> cC114(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( sQ35_spl
| ~ cC114(iV21026) ),
inference(component_clause,[status(thm)],[f1001]) ).
fof(f1004,definition,
( sQ36_spl
<=> cC64(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1005,plain,
( ~ sQ36_spl
| cC64(iV21026) ),
inference(component_clause,[status(thm)],[f1004]) ).
fof(f1007,definition,
( sQ37_spl
<=> cC110(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1010,definition,
( sQ38_spl
<=> cC116(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
( ~ sQ38_spl
| cC116(iV21026) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,definition,
( sQ39_spl
<=> cC82(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1014,plain,
( ~ sQ39_spl
| cC82(iV21026) ),
inference(component_clause,[status(thm)],[f1013]) ).
fof(f1016,definition,
( sQ40_spl
<=> cC138(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1017,plain,
( ~ sQ40_spl
| cC138(iV21026) ),
inference(component_clause,[status(thm)],[f1016]) ).
fof(f1019,definition,
( sQ41_spl
<=> cC4(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1021,plain,
( sQ41_spl
| ~ cC4(iV21026) ),
inference(component_clause,[status(thm)],[f1019]) ).
fof(f1022,definition,
( sQ42_spl
<=> cC108(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1023,plain,
( ~ sQ42_spl
| cC108(iV21026) ),
inference(component_clause,[status(thm)],[f1022]) ).
fof(f1025,definition,
( sQ43_spl
<=> cC14(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1027,plain,
( sQ43_spl
| ~ cC14(iV21026) ),
inference(component_clause,[status(thm)],[f1025]) ).
fof(f1028,definition,
( sQ44_spl
<=> cC90(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1029,plain,
( ~ sQ44_spl
| cC90(iV21026) ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1031,definition,
( sQ45_spl
<=> cowlThing(iV21027) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1033,plain,
( sQ45_spl
| ~ cowlThing(iV21027) ),
inference(component_clause,[status(thm)],[f1031]) ).
fof(f1034,definition,
( sQ46_spl
<=> cC30(iV21027) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1036,plain,
( sQ46_spl
| ~ cC30(iV21027) ),
inference(component_clause,[status(thm)],[f1034]) ).
fof(f1037,definition,
( sQ47_spl
<=> cC24(iV21027) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1039,plain,
( sQ47_spl
| ~ cC24(iV21027) ),
inference(component_clause,[status(thm)],[f1037]) ).
fof(f1040,definition,
( sQ48_spl
<=> cowlThing(iV21029) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( sQ48_spl
| ~ cowlThing(iV21029) ),
inference(component_clause,[status(thm)],[f1040]) ).
fof(f1043,definition,
( sQ49_spl
<=> cC50(iV21029) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1045,plain,
( sQ49_spl
| ~ cC50(iV21029) ),
inference(component_clause,[status(thm)],[f1043]) ).
fof(f1046,definition,
( sQ50_spl
<=> cC44(iV21029) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1048,plain,
( sQ50_spl
| ~ cC44(iV21029) ),
inference(component_clause,[status(thm)],[f1046]) ).
fof(f1049,definition,
( sQ51_spl
<=> cowlThing(iV21030) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( sQ51_spl
| ~ cowlThing(iV21030) ),
inference(component_clause,[status(thm)],[f1049]) ).
fof(f1052,definition,
( sQ52_spl
<=> cC66(iV21030) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( sQ52_spl
| ~ cC66(iV21030) ),
inference(component_clause,[status(thm)],[f1052]) ).
fof(f1055,definition,
( sQ53_spl
<=> cC72(iV21030) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1058,plain,
( ~ sQ53_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ47_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f894,f896,f899,f902,f905,f908,f911,f914,f917,f920,f923,f926,f929,f932,f935,f938,f941,f944,f947,f950,f953,f956,f959,f962,f965,f968,f971,f974,f977,f980,f983,f986,f989,f992,f995,f998,f1001,f1004,f1007,f1010,f1013,f1016,f1019,f1022,f1025,f1028,f1031,f1034,f1037,f1040,f1043,f1046,f1049,f1052,f1055]) ).
fof(f1059,plain,
( ~ sQ53_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ47_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f895,f896,f899,f902,f905,f908,f911,f914,f917,f920,f923,f926,f929,f932,f935,f938,f941,f944,f947,f950,f953,f956,f959,f962,f965,f968,f971,f974,f977,f980,f983,f986,f989,f992,f995,f998,f1001,f1004,f1007,f1010,f1013,f1016,f1019,f1022,f1025,f1028,f1031,f1034,f1037,f1040,f1043,f1046,f1049,f1052,f1055]) ).
fof(f1060,plain,
cC114(iV21026),
inference(resolution,[status(thm)],[f709,f292]) ).
fof(f1062,plain,
( cC106(iV21026)
| cC108(iV21026) ),
inference(resolution,[status(thm)],[f278,f713]) ).
fof(f1063,definition,
( sQ54_spl
<=> cC98(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
( ~ sQ54_spl
| cC98(iV21026) ),
inference(component_clause,[status(thm)],[f1063]) ).
fof(f1067,definition,
( sQ55_spl
<=> cC106(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1068,plain,
( ~ sQ55_spl
| cC106(iV21026) ),
inference(component_clause,[status(thm)],[f1067]) ).
fof(f1070,plain,
( sQ55_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f1062,f1022,f1067]) ).
fof(f1071,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1068,f741]) ).
fof(f1072,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f1071]) ).
fof(f1073,plain,
( ~ sQ42_spl
| ~ cTOP(iV21026)
| cC110(iV21026) ),
inference(resolution,[status(thm)],[f1023,f283]) ).
fof(f1074,definition,
( sQ56_spl
<=> cTOP(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1076,plain,
( sQ56_spl
| ~ cTOP(iV21026) ),
inference(component_clause,[status(thm)],[f1074]) ).
fof(f1077,plain,
( ~ sQ42_spl
| ~ sQ56_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1073,f1007,f1074,f1022]) ).
fof(f1085,plain,
! [X0] :
( cC128(X0)
| cC122(X0)
| ~ cTOP(X0)
| cC132(X0) ),
inference(resolution,[status(thm)],[f341,f336]) ).
fof(f1086,plain,
( cC128(iV21026)
| ~ cTOP(iV21026)
| cC132(iV21026) ),
inference(resolution,[status(thm)],[f1085,f714]) ).
fof(f1088,definition,
( sQ57_spl
<=> cC128(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1089,plain,
( ~ sQ57_spl
| cC128(iV21026) ),
inference(component_clause,[status(thm)],[f1088]) ).
fof(f1091,plain,
( sQ57_spl
| ~ sQ56_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f1086,f974,f1074,f1088]) ).
fof(f1096,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1076,f709]) ).
fof(f1097,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f1096]) ).
fof(f1098,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1089,f747]) ).
fof(f1099,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1098]) ).
fof(f1102,plain,
( ~ sQ26_spl
| cC130(iV21026) ),
inference(resolution,[status(thm)],[f975,f340]) ).
fof(f1136,plain,
! [X0] :
( cC144(X0)
| cC150(X0)
| ~ cTOP(X0)
| cC154(X0) ),
inference(resolution,[status(thm)],[f405,f400]) ).
fof(f1137,plain,
( cC144(iV21026)
| ~ cTOP(iV21026)
| cC154(iV21026) ),
inference(resolution,[status(thm)],[f1136,f739]) ).
fof(f1139,definition,
( sQ64_spl
<=> cC144(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
( ~ sQ64_spl
| cC144(iV21026) ),
inference(component_clause,[status(thm)],[f1139]) ).
fof(f1142,plain,
( sQ64_spl
| ~ sQ56_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f1137,f983,f1074,f1139]) ).
fof(f1147,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1140,f742]) ).
fof(f1148,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f1147]) ).
fof(f1149,plain,
( ~ sQ29_spl
| cC152(iV21026) ),
inference(resolution,[status(thm)],[f984,f404]) ).
fof(f1153,plain,
! [X0,X1] :
( cC12(X1)
| ~ rR1(X0,X1)
| ~ cC10(X0)
| cC16(X0) ),
inference(resolution,[status(thm)],[f420,f361]) ).
fof(f1154,plain,
! [X0] :
( cC34(X0)
| cC28(X0)
| ~ cTOP(X0)
| cC38(X0) ),
inference(resolution,[status(thm)],[f538,f533]) ).
fof(f1155,plain,
( cC34(iV21026)
| ~ cTOP(iV21026)
| cC38(iV21026) ),
inference(resolution,[status(thm)],[f1154,f720]) ).
fof(f1157,definition,
( sQ66_spl
<=> cC34(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1158,plain,
( ~ sQ66_spl
| cC34(iV21026) ),
inference(component_clause,[status(thm)],[f1157]) ).
fof(f1160,plain,
( sQ66_spl
| ~ sQ56_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f1155,f941,f1074,f1157]) ).
fof(f1165,plain,
( ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1158,f719]) ).
fof(f1166,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1165]) ).
fof(f1168,plain,
( ~ sQ15_spl
| cC36(iV21026) ),
inference(resolution,[status(thm)],[f942,f536]) ).
fof(f1171,plain,
! [X0] :
( ~ cTOP(X0)
| ~ cC38(X0)
| cC42(X0) ),
inference(resolution,[status(thm)],[f553,f548]) ).
fof(f1172,plain,
! [X0] :
( ~ cC38(X0)
| cC42(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1171,f537]) ).
fof(f1173,plain,
( ~ sQ15_spl
| cC42(iV21026) ),
inference(resolution,[status(thm)],[f1172,f942]) ).
fof(f1175,plain,
( ~ sQ15_spl
| cC40(iV21026) ),
inference(resolution,[status(thm)],[f1173,f551]) ).
fof(f1177,plain,
! [X0] :
( cC54(X0)
| cC48(X0)
| ~ cTOP(X0)
| cC58(X0) ),
inference(resolution,[status(thm)],[f597,f592]) ).
fof(f1178,plain,
( cC54(iV21026)
| ~ cTOP(iV21026)
| cC58(iV21026) ),
inference(resolution,[status(thm)],[f1177,f743]) ).
fof(f1180,definition,
( sQ68_spl
<=> cC54(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1181,plain,
( ~ sQ68_spl
| cC54(iV21026) ),
inference(component_clause,[status(thm)],[f1180]) ).
fof(f1183,plain,
( sQ68_spl
| ~ sQ56_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f1178,f965,f1074,f1180]) ).
fof(f1188,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1181,f740]) ).
fof(f1189,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1188]) ).
fof(f1191,plain,
( ~ sQ23_spl
| cC56(iV21026) ),
inference(resolution,[status(thm)],[f966,f595]) ).
fof(f1194,plain,
( ~ sQ23_spl
| ~ cC42(iV21026)
| cC60(iV21026) ),
inference(resolution,[status(thm)],[f602,f966]) ).
fof(f1195,plain,
( ~ sQ23_spl
| ~ sQ8_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1194,f938,f920,f965]) ).
fof(f1196,plain,
( sQ8_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f922,f1173]) ).
fof(f1197,plain,
( sQ8_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1196]) ).
fof(f1200,plain,
! [X0] :
( ~ cTOP(X0)
| ~ cC60(X0)
| cC64(X0) ),
inference(resolution,[status(thm)],[f611,f606]) ).
fof(f1201,plain,
! [X0] :
( cC76(X0)
| cC70(X0)
| ~ cTOP(X0)
| cC80(X0) ),
inference(resolution,[status(thm)],[f661,f650]) ).
fof(f1202,plain,
( cC76(iV21026)
| ~ cTOP(iV21026)
| cC80(iV21026) ),
inference(resolution,[status(thm)],[f1201,f723]) ).
fof(f1204,definition,
( sQ70_spl
<=> cC76(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1205,plain,
( ~ sQ70_spl
| cC76(iV21026) ),
inference(component_clause,[status(thm)],[f1204]) ).
fof(f1207,plain,
( sQ70_spl
| ~ sQ56_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1202,f986,f1074,f1204]) ).
fof(f1212,plain,
( ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1205,f744]) ).
fof(f1213,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1212]) ).
fof(f1214,plain,
( ~ sQ30_spl
| cC78(iV21026) ),
inference(resolution,[status(thm)],[f987,f660]) ).
fof(f1218,plain,
( ~ sQ14_spl
| ~ cTOP(iV21026)
| cC64(iV21026) ),
inference(resolution,[status(thm)],[f1200,f939]) ).
fof(f1219,plain,
( ~ sQ14_spl
| ~ sQ56_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1218,f1004,f1074,f938]) ).
fof(f1220,plain,
( ~ sQ36_spl
| ~ cC80(iV21026)
| cC82(iV21026) ),
inference(resolution,[status(thm)],[f1005,f666]) ).
fof(f1222,plain,
( ~ sQ36_spl
| cC62(iV21026) ),
inference(resolution,[status(thm)],[f1005,f609]) ).
fof(f1223,plain,
( ~ sQ36_spl
| ~ sQ30_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1220,f1013,f986,f1004]) ).
fof(f1227,plain,
( ~ sQ39_spl
| ~ cC84(iV21026)
| cC86(iV21026) ),
inference(resolution,[status(thm)],[f1014,f675]) ).
fof(f1230,plain,
( ~ sQ39_spl
| ~ sQ5_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f1227,f926,f911,f1013]) ).
fof(f1231,plain,
( sQ5_spl
| ~ cTOP(iV21026) ),
inference(resolution,[status(thm)],[f913,f670]) ).
fof(f1232,plain,
( sQ5_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1231,f1074,f911]) ).
fof(f1234,plain,
( ~ sQ10_spl
| ~ cC88(iV21026)
| cC90(iV21026) ),
inference(resolution,[status(thm)],[f927,f684]) ).
fof(f1237,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1234,f1028,f923,f926]) ).
fof(f1239,plain,
( sQ9_spl
| ~ cTOP(iV21026) ),
inference(resolution,[status(thm)],[f925,f679]) ).
fof(f1240,plain,
( sQ9_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1239,f1074,f923]) ).
fof(f1244,plain,
( ~ sQ44_spl
| ~ cC110(iV21026)
| cC112(iV21026) ),
inference(resolution,[status(thm)],[f1029,f288]) ).
fof(f1245,plain,
( ~ sQ44_spl
| ~ sQ37_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1244,f995,f1007,f1028]) ).
fof(f1248,plain,
( ~ sQ33_spl
| ~ cC114(iV21026)
| cC116(iV21026) ),
inference(resolution,[status(thm)],[f996,f297]) ).
fof(f1250,plain,
( ~ sQ33_spl
| ~ sQ35_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1248,f1010,f1001,f995]) ).
fof(f1251,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1003,f1060]) ).
fof(f1252,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f1251]) ).
fof(f1253,plain,
( ~ sQ38_spl
| ~ cC132(iV21026)
| cC134(iV21026) ),
inference(resolution,[status(thm)],[f1011,f346]) ).
fof(f1256,plain,
( ~ sQ38_spl
| ~ sQ26_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1253,f950,f974,f1010]) ).
fof(f1257,plain,
( ~ sQ18_spl
| ~ cC136(iV21026)
| cC138(iV21026) ),
inference(resolution,[status(thm)],[f951,f355]) ).
fof(f1260,plain,
( ~ sQ18_spl
| ~ sQ32_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1257,f1016,f992,f950]) ).
fof(f1261,plain,
( sQ32_spl
| ~ cTOP(iV21026) ),
inference(resolution,[status(thm)],[f994,f350]) ).
fof(f1262,plain,
( sQ32_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1261,f1074,f992]) ).
fof(f1264,plain,
( ~ sQ40_spl
| ~ cC154(iV21026)
| cC156(iV21026) ),
inference(resolution,[status(thm)],[f1017,f410]) ).
fof(f1267,plain,
( ~ sQ40_spl
| ~ sQ29_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f1264,f935,f983,f1016]) ).
fof(f1268,plain,
( ~ sQ13_spl
| ~ cC22(iV21026)
| cC158(iV21026) ),
inference(resolution,[status(thm)],[f936,f415]) ).
fof(f1271,plain,
( ~ sQ13_spl
| ~ sQ19_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f1268,f944,f953,f935]) ).
fof(f1272,plain,
( sQ19_spl
| ~ cC158(iV21026) ),
inference(resolution,[status(thm)],[f955,f413]) ).
fof(f1288,plain,
! [X0] :
( ~ rR1(X0,iV21029)
| ~ cC10(X0)
| cC16(X0) ),
inference(resolution,[status(thm)],[f805,f1153]) ).
fof(f1314,plain,
! [X0] :
( ~ cC4(X0)
| ~ cC8(X0)
| ~ rR1(X0,iV21029)
| cC16(X0) ),
inference(resolution,[status(thm)],[f1288,f256]) ).
fof(f1315,plain,
( ~ cC4(iV21026)
| ~ cC8(iV21026)
| cC16(iV21026) ),
inference(resolution,[status(thm)],[f1314,f761]) ).
fof(f1316,plain,
( ~ sQ41_spl
| ~ sQ31_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1315,f914,f989,f1019]) ).
fof(f1317,plain,
! [X0] :
( sQ41_spl
| cC2(X0)
| ~ rR1(iV21026,X0) ),
inference(resolution,[status(thm)],[f1021,f544]) ).
fof(f1321,plain,
( sQ41_spl
| ~ rR1(iV21026,iV21027) ),
inference(resolution,[status(thm)],[f1317,f790]) ).
fof(f1322,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1321,f759]) ).
fof(f1323,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1322]) ).
fof(f1325,plain,
( sQ31_spl
| ~ cC10(iV21026) ),
inference(resolution,[status(thm)],[f991,f254]) ).
fof(f1336,plain,
( cC72(iV21030)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[f838,f639]) ).
fof(f1337,definition,
( sQ78_spl
<=> cC18(iV21030) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1338,plain,
( ~ sQ78_spl
| cC18(iV21030) ),
inference(component_clause,[status(thm)],[f1337]) ).
fof(f1340,plain,
( sQ53_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1336,f1337,f1055]) ).
fof(f1343,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f849,f1338]) ).
fof(f1344,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1343]) ).
fof(f1379,plain,
cC158(iV21026),
inference(resolution,[status(thm)],[f704,f710]) ).
fof(f1380,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1379,f1272]) ).
fof(f1381,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1380]) ).
fof(f1382,plain,
( ~ sQ19_spl
| cC16(iV21026) ),
inference(resolution,[status(thm)],[f954,f492]) ).
fof(f1386,plain,
( ~ sQ19_spl
| cC10(iV21026) ),
inference(resolution,[status(thm)],[f1382,f419]) ).
fof(f1387,plain,
( ~ sQ19_spl
| cC14(iV21026) ),
inference(resolution,[status(thm)],[f1382,f418]) ).
fof(f1389,plain,
( ~ sQ19_spl
| sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1386,f1325]) ).
fof(f1390,plain,
( ~ sQ19_spl
| sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1389]) ).
fof(f1391,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1064,f713]) ).
fof(f1392,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f1391]) ).
fof(f1400,plain,
( sQ17_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f949,f1386]) ).
fof(f1401,plain,
( sQ17_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1400]) ).
fof(f1403,plain,
( sQ52_spl
| cC18(iV21030)
| cC68(iV21030) ),
inference(resolution,[status(thm)],[f1054,f622]) ).
fof(f1404,definition,
( sQ82_spl
<=> cC68(iV21030) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1405,plain,
( ~ sQ82_spl
| cC68(iV21030) ),
inference(component_clause,[status(thm)],[f1404]) ).
fof(f1407,plain,
( sQ52_spl
| sQ78_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f1403,f1404,f1337,f1052]) ).
fof(f1408,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1051,f246]) ).
fof(f1409,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f1408]) ).
fof(f1410,plain,
( ~ sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1405,f837]) ).
fof(f1411,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f1410]) ).
fof(f1413,plain,
( sQ50_spl
| cC12(iV21029)
| cC46(iV21029) ),
inference(resolution,[status(thm)],[f1048,f564]) ).
fof(f1414,definition,
( sQ83_spl
<=> cC46(iV21029) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1415,plain,
( ~ sQ83_spl
| cC46(iV21029) ),
inference(component_clause,[status(thm)],[f1414]) ).
fof(f1417,definition,
( sQ84_spl
<=> cC12(iV21029) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1418,plain,
( ~ sQ84_spl
| cC12(iV21029) ),
inference(component_clause,[status(thm)],[f1417]) ).
fof(f1420,plain,
( sQ50_spl
| sQ84_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1413,f1414,f1417,f1046]) ).
fof(f1421,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1042,f246]) ).
fof(f1422,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f1421]) ).
fof(f1423,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1033,f246]) ).
fof(f1424,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1423]) ).
fof(f1425,plain,
( sQ43_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1027,f1387]) ).
fof(f1426,plain,
( sQ43_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1425]) ).
fof(f1427,plain,
( sQ28_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f1222]) ).
fof(f1428,plain,
( sQ28_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f1427]) ).
fof(f1429,plain,
( sQ27_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f979,f1102]) ).
fof(f1430,plain,
( sQ27_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f1429]) ).
fof(f1431,plain,
( sQ25_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f973,f1175]) ).
fof(f1432,plain,
( sQ25_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1431]) ).
fof(f1433,plain,
( sQ24_spl
| ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f970,f1149]) ).
fof(f1434,plain,
( sQ24_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f1433]) ).
fof(f1435,plain,
( sQ22_spl
| ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f964,f1214]) ).
fof(f1436,plain,
( sQ22_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f1435]) ).
fof(f1437,plain,
( sQ21_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f961,f1191]) ).
fof(f1438,plain,
( sQ21_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f1437]) ).
fof(f1439,plain,
( sQ7_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f919,f1168]) ).
fof(f1440,plain,
( sQ7_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1439]) ).
fof(f1441,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f910,f246]) ).
fof(f1442,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1441]) ).
fof(f1443,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f900,f247]) ).
fof(f1444,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1443]) ).
fof(f1445,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f898,f246]) ).
fof(f1446,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1445]) ).
fof(f1447,plain,
( ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1418,f805]) ).
fof(f1448,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f1447]) ).
fof(f1449,plain,
( ~ sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1415,f797]) ).
fof(f1450,plain,
~ sQ83_spl,
inference(contradiction_clause,[status(thm)],[f1449]) ).
fof(f1452,plain,
( sQ49_spl
| cC12(iV21029)
| cC52(iV21029) ),
inference(resolution,[status(thm)],[f1045,f581]) ).
fof(f1453,definition,
( sQ85_spl
<=> cC52(iV21029) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1454,plain,
( ~ sQ85_spl
| cC52(iV21029) ),
inference(component_clause,[status(thm)],[f1453]) ).
fof(f1456,plain,
( sQ49_spl
| sQ84_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1452,f1453,f1417,f1043]) ).
fof(f1457,plain,
( ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1454,f810]) ).
fof(f1458,plain,
~ sQ85_spl,
inference(contradiction_clause,[status(thm)],[f1457]) ).
fof(f1460,plain,
( sQ47_spl
| cC2(iV21027)
| cC26(iV21027) ),
inference(resolution,[status(thm)],[f1039,f505]) ).
fof(f1461,definition,
( sQ86_spl
<=> cC26(iV21027) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1462,plain,
( ~ sQ86_spl
| cC26(iV21027) ),
inference(component_clause,[status(thm)],[f1461]) ).
fof(f1464,definition,
( sQ87_spl
<=> cC2(iV21027) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1465,plain,
( ~ sQ87_spl
| cC2(iV21027) ),
inference(component_clause,[status(thm)],[f1464]) ).
fof(f1467,plain,
( sQ47_spl
| sQ87_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1460,f1461,f1464,f1037]) ).
fof(f1468,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1465,f790]) ).
fof(f1469,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1468]) ).
fof(f1470,plain,
( ~ sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1462,f762]) ).
fof(f1471,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f1470]) ).
fof(f1473,plain,
( sQ46_spl
| cC2(iV21027)
| cC32(iV21027) ),
inference(resolution,[status(thm)],[f1036,f522]) ).
fof(f1474,definition,
( sQ88_spl
<=> cC32(iV21027) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1475,plain,
( ~ sQ88_spl
| cC32(iV21027) ),
inference(component_clause,[status(thm)],[f1474]) ).
fof(f1477,plain,
( sQ46_spl
| sQ87_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1473,f1474,f1464,f1034]) ).
fof(f1478,plain,
( ~ sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1475,f774]) ).
fof(f1479,plain,
~ sQ88_spl,
inference(contradiction_clause,[status(thm)],[f1478]) ).
fof(f1480,plain,
( sQ34_spl
| ~ cC174(iV21026)
| cC178(iV21026) ),
inference(resolution,[status(thm)],[f1000,f483]) ).
fof(f1481,definition,
( sQ89_spl
<=> cC178(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1482,plain,
( ~ sQ89_spl
| cC178(iV21026) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1484,plain,
( sQ34_spl
| ~ sQ11_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f1480,f1481,f929,f998]) ).
fof(f1486,plain,
( sQ11_spl
| cC172(iV21026)
| ~ cC168(iV21026) ),
inference(resolution,[status(thm)],[f931,f466]) ).
fof(f1487,definition,
( sQ90_spl
<=> cC172(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1488,plain,
( ~ sQ90_spl
| cC172(iV21026) ),
inference(component_clause,[status(thm)],[f1487]) ).
fof(f1490,plain,
( sQ11_spl
| sQ90_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1486,f956,f1487,f929]) ).
fof(f1491,plain,
( ~ sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1488,f748]) ).
fof(f1492,plain,
~ sQ90_spl,
inference(contradiction_clause,[status(thm)],[f1491]) ).
fof(f1493,plain,
( ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1482,f724]) ).
fof(f1494,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f1493]) ).
fof(f1496,plain,
( sQ20_spl
| cC162(iV21026)
| cC166(iV21026) ),
inference(resolution,[status(thm)],[f958,f449]) ).
fof(f1497,definition,
( sQ91_spl
<=> cC166(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1498,plain,
( ~ sQ91_spl
| cC166(iV21026) ),
inference(component_clause,[status(thm)],[f1497]) ).
fof(f1500,definition,
( sQ92_spl
<=> cC162(iV21026) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1501,plain,
( ~ sQ92_spl
| cC162(iV21026) ),
inference(component_clause,[status(thm)],[f1500]) ).
fof(f1503,plain,
( sQ20_spl
| sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1496,f1497,f1500,f956]) ).
fof(f1504,plain,
( ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1498,f726]) ).
fof(f1505,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f1504]) ).
fof(f1506,plain,
( ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1501,f725]) ).
fof(f1507,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f1506]) ).
fof(f1508,plain,
( sQ12_spl
| ~ cC22(iV21026) ),
inference(resolution,[status(thm)],[f934,f493]) ).
fof(f1510,plain,
( sQ12_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1508,f953,f932]) ).
fof(f1511,plain,
( ~ sQ3_spl
| ~ xsd_string(sK38_skl) ),
inference(resolution,[status(thm)],[f906,f250]) ).
fof(f1512,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1511,f903]) ).
fof(f1513,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1512]) ).
fof(f1514,plain,
( sQ2_spl
| xsd_integer(sK38_skl) ),
inference(resolution,[status(thm)],[f904,f251]) ).
fof(f1515,plain,
( sQ2_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1514,f905,f902]) ).
fof(f1516,plain,
$false,
inference(sat_refutation,[status(thm)],[f1058,f1059,f1070,f1072,f1077,f1091,f1097,f1099,f1142,f1148,f1160,f1166,f1183,f1189,f1195,f1197,f1207,f1213,f1219,f1223,f1230,f1232,f1237,f1240,f1245,f1250,f1252,f1256,f1260,f1262,f1267,f1271,f1316,f1323,f1340,f1344,f1381,f1390,f1392,f1401,f1407,f1409,f1411,f1420,f1422,f1424,f1426,f1428,f1430,f1432,f1434,f1436,f1438,f1440,f1442,f1444,f1446,f1448,f1450,f1456,f1458,f1467,f1469,f1471,f1477,f1479,f1484,f1490,f1492,f1494,f1503,f1505,f1507,f1510,f1513,f1515]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 22:54:43 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.42 % Elapsed time: 0.056063 seconds
% 0.09/0.42 % CPU time: 0.191689 seconds
% 0.09/0.42 % Total memory used: 32.521 MB
% 0.09/0.42 % Net memory used: 32.374 MB
%------------------------------------------------------------------------------