%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : KRS159+1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:36:45 PM UTC 2026
% Result : Theorem 1.58s 1.84s
% Output : CNFRefutation 1.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 57
% Syntax : Number of formulae : 209 ( 56 unt; 0 def)
% Number of atoms : 1048 ( 0 equ)
% Maximal formula atoms : 108 ( 5 avg)
% Number of connectives : 1440 ( 601 ~; 588 |; 210 &)
% ( 41 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 56 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 64 ( 63 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-1 aty)
% Number of variables : 185 ( 4 sgn 106 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(the_axiom,conjecture,
( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC108(iV21026)
& cC40(iV21026)
& cC136(iV21026)
& cC10(iV21026)
& cC90(iV21026)
& cowlThing(iV21026)
& cC58(iV21026)
& cC56(iV21026)
& cC158(iV21026)
& cC110(iV21026)
& cC22(iV21026)
& cC60(iV21026)
& cC154(iV21026)
& cC180(iV21026)
& cC78(iV21026)
& cC16(iV21026)
& cC132(iV21026)
& cC114(iV21026)
& cC20(iV21026)
& cC84(iV21026)
& cC38(iV21026)
& cC138(iV21026)
& cC174(iV21026)
& cC62(iV21026)
& cC8(iV21026)
& cC36(iV21026)
& cC112(iV21026)
& cC64(iV21026)
& cC116(iV21026)
& cC82(iV21026)
& cC14(iV21026)
& cC152(iV21026)
& cC80(iV21026)
& cC88(iV21026)
& cC130(iV21026)
& cC168(iV21026)
& cC4(iV21026)
& cC134(iV21026)
& cC42(iV21026)
& cC156(iV21026)
& cC86(iV21026)
& cC30(iV21027)
& cowlThing(iV21027)
& cC24(iV21027)
& cC50(iV21029)
& cC44(iV21029)
& cowlThing(iV21029)
& cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(axiom_0,axiom,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(axiom_67,axiom,
! [X1] :
( cC16(X1)
<=> ( cC10(X1)
& cC14(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(axiom_15,axiom,
! [X1] :
( cC110(X1)
<=> ( cC108(X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X1] :
( cC112(X1)
<=> ( cC110(X1)
& cC90(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_16) ).
fof(axiom_18,axiom,
! [X1] :
( cC116(X1)
<=> ( cC114(X1)
& cC112(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(axiom_174,axiom,
! [X1] :
( cC90(X1)
<=> ( cC86(X1)
& cC88(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(axiom_41,axiom,
! [X1] :
( cC134(X1)
<=> ( cC116(X1)
& cC132(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
fof(axiom_40,axiom,
! [X1] :
( cC132(X1)
<=> ( cC130(X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(axiom_43,axiom,
! [X1] :
( cC138(X1)
<=> ( cC136(X1)
& cC134(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
fof(axiom_65,axiom,
! [X1] :
( cC156(X1)
<=> ( cC154(X1)
& cC138(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(axiom_64,axiom,
! [X1] :
( cC154(X1)
<=> ( cC152(X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
fof(axiom_66,axiom,
! [X1] :
( cC158(X1)
<=> ( cC22(X1)
& cC156(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(axiom_87,axiom,
! [X1] :
( cC174(X1)
<=> ( cC172xcomp(X1)
& cC168(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_87) ).
fof(axiom_96,axiom,
! [X1] :
( cC180(X1)
<=> ( cC174(X1)
& cC178xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_96) ).
fof(axiom_120,axiom,
! [X1] :
( cC38(X1)
<=> ( cC36(X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(axiom_123,axiom,
! [X1] :
( cC42(X1)
<=> ( cC40(X1)
& cC38(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
fof(axiom_146,axiom,
! [X1] :
( cC60(X1)
<=> ( cC58(X1)
& cC42(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_146) ).
fof(axiom_143,axiom,
! [X1] :
( cC58(X1)
<=> ( cC56(X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_143) ).
fof(axiom_148,axiom,
! [X1] :
( cC64(X1)
<=> ( cC60(X1)
& cC62(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_148) ).
fof(axiom_170,axiom,
! [X1] :
( cC82(X1)
<=> ( cC64(X1)
& cC80(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_170) ).
fof(axiom_169,axiom,
! [X1] :
( cC80(X1)
<=> ( cC78(X1)
& cTOP(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_169) ).
fof(axiom_172,axiom,
! [X1] :
( cC86(X1)
<=> ( cC82(X1)
& cC84(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_172) ).
fof(axiom_100,axiom,
! [X1] :
( cC22(X1)
<=> ( cC20(X1)
& cC16(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_100) ).
fof(axiom_186,axiom,
! [X1] :
( cTEST(X1)
<=> ( cC158(X1)
& cC180(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_186) ).
fof(axiom_221,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_221) ).
fof(axiom_158,axiom,
! [X1] :
( cC72(X1)
<=> ? [X2] : ra_Px24(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_158) ).
fof(axiom_160,axiom,
! [X1] :
( cC72xcomp(X1)
<=> ~ ? [X3] : ra_Px24(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_160) ).
fof(axiom_163,axiom,
! [X1] :
( cC74xcomp(X1)
<=> ~ ? [X3] : ra_Px87(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(axiom_162,axiom,
! [X1] :
( cC74(X1)
<=> ? [X2] : ra_Px87(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_162) ).
fof(axiom_173,axiom,
! [X1] :
( cC88(X1)
<=> cTOP(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_173) ).
fof(axiom_121,axiom,
! [X1] :
( cC4(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC2xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_121) ).
fof(axiom_150,axiom,
! [X1] :
( cC66(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC2xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_150) ).
fof(axiom_133,axiom,
! [X1] :
( cC50(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC12xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_133) ).
fof(axiom_125,axiom,
! [X1] :
( cC44(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC2xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_125) ).
fof(axiom_111,axiom,
! [X1] :
( cC30(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC12xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_111) ).
fof(axiom_102,axiom,
! [X1] :
( cC24(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC2xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_102) ).
fof(axiom_99,axiom,
! [X1] :
( cC20(X1)
<=> ? [X3] :
( rR1(X1,X3)
& cC18xcomp(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_99) ).
fof(axiom_161,axiom,
! [X1] :
( cC74(X1)
<=> ( cC72xcomp(X1)
& cC18xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_161) ).
fof(axiom_190,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_190) ).
fof(axiom_223,axiom,
rR1(iV21026,iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_223) ).
fof(axiom_237,axiom,
cC2xcomp(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_237) ).
fof(axiom_309,axiom,
rR1(iV21030,iV21032),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_309) ).
fof(axiom_312,axiom,
cC2xcomp(iV21032),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_312) ).
fof(axiom_282,axiom,
rR1(iV21029,iV21033),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_282) ).
fof(axiom_319,axiom,
cC12xcomp(iV21033),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_319) ).
fof(axiom_281,axiom,
rR1(iV21029,iV21034),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_281) ).
fof(axiom_325,axiom,
cC2xcomp(iV21034),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_325) ).
fof(axiom_253,axiom,
rR1(iV21027,iV21035),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_253) ).
fof(axiom_331,axiom,
cC12xcomp(iV21035),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_331) ).
fof(axiom_252,axiom,
rR1(iV21027,iV21036),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_252) ).
fof(axiom_337,axiom,
cC2xcomp(iV21036),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_337) ).
fof(axiom_222,axiom,
rR1(iV21026,iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_222) ).
fof(axiom_293,axiom,
cC18xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_293) ).
fof(axiom_307,axiom,
cC74xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_307) ).
fof(axiom_2,axiom,
! [X1] :
( cC10(X1)
<=> ( cC8(X1)
& cC4(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(c_0_57,negated_conjecture,
~ ( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC108(iV21026)
& cC40(iV21026)
& cC136(iV21026)
& cC10(iV21026)
& cC90(iV21026)
& cowlThing(iV21026)
& cC58(iV21026)
& cC56(iV21026)
& cC158(iV21026)
& cC110(iV21026)
& cC22(iV21026)
& cC60(iV21026)
& cC154(iV21026)
& cC180(iV21026)
& cC78(iV21026)
& cC16(iV21026)
& cC132(iV21026)
& cC114(iV21026)
& cC20(iV21026)
& cC84(iV21026)
& cC38(iV21026)
& cC138(iV21026)
& cC174(iV21026)
& cC62(iV21026)
& cC8(iV21026)
& cC36(iV21026)
& cC112(iV21026)
& cC64(iV21026)
& cC116(iV21026)
& cC82(iV21026)
& cC14(iV21026)
& cC152(iV21026)
& cC80(iV21026)
& cC88(iV21026)
& cC130(iV21026)
& cC168(iV21026)
& cC4(iV21026)
& cC134(iV21026)
& cC42(iV21026)
& cC156(iV21026)
& cC86(iV21026)
& cC30(iV21027)
& cowlThing(iV21027)
& cC24(iV21027)
& cC50(iV21029)
& cC44(iV21029)
& cowlThing(iV21029)
& cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[the_axiom])]) ).
fof(c_0_58,plain,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
inference(fof_simplification,[status(thm)],[axiom_0]) ).
fof(c_0_59,negated_conjecture,
( ( ~ xsd_string(esk138_0)
| xsd_integer(esk138_0)
| ~ cowlThing(esk137_0)
| cowlNothing(esk137_0)
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) )
& ( xsd_string(esk138_0)
| ~ xsd_integer(esk138_0)
| ~ cowlThing(esk137_0)
| cowlNothing(esk137_0)
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_57])])])]) ).
fof(c_0_60,plain,
! [X357] :
( cowlThing(X357)
& ~ cowlNothing(X357) ),
inference(variable_rename,[status(thm)],[c_0_58]) ).
fof(c_0_61,plain,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
inference(fof_simplification,[status(thm)],[axiom_1]) ).
cnf(c_0_62,negated_conjecture,
( xsd_string(esk138_0)
| cowlNothing(esk137_0)
| ~ xsd_integer(esk138_0)
| ~ cowlThing(esk137_0)
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
cnf(c_0_63,plain,
cowlThing(X1),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
fof(c_0_64,plain,
! [X358] :
( ( ~ xsd_string(X358)
| ~ xsd_integer(X358) )
& ( xsd_integer(X358)
| xsd_string(X358) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_61])]) ).
fof(c_0_65,plain,
! [X559] :
( ( cC10(X559)
| ~ cC16(X559) )
& ( cC14(X559)
| ~ cC16(X559) )
& ( ~ cC10(X559)
| ~ cC14(X559)
| cC16(X559) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_67])])]) ).
fof(c_0_66,plain,
! [X402] :
( ( cC108(X402)
| ~ cC110(X402) )
& ( cTOP(X402)
| ~ cC110(X402) )
& ( ~ cC108(X402)
| ~ cTOP(X402)
| cC110(X402) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_15])])]) ).
fof(c_0_67,plain,
! [X403] :
( ( cC110(X403)
| ~ cC112(X403) )
& ( cC90(X403)
| ~ cC112(X403) )
& ( ~ cC110(X403)
| ~ cC90(X403)
| cC112(X403) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_16])])]) ).
fof(c_0_68,plain,
! [X405] :
( ( cC114(X405)
| ~ cC116(X405) )
& ( cC112(X405)
| ~ cC116(X405) )
& ( ~ cC114(X405)
| ~ cC112(X405)
| cC116(X405) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_18])])]) ).
fof(c_0_69,plain,
! [X909] :
( ( cC86(X909)
| ~ cC90(X909) )
& ( cC88(X909)
| ~ cC90(X909) )
& ( ~ cC86(X909)
| ~ cC88(X909)
| cC90(X909) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_174])])]) ).
fof(c_0_70,plain,
! [X482] :
( ( cC116(X482)
| ~ cC134(X482) )
& ( cC132(X482)
| ~ cC134(X482) )
& ( ~ cC116(X482)
| ~ cC132(X482)
| cC134(X482) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_41])])]) ).
fof(c_0_71,plain,
! [X481] :
( ( cC130(X481)
| ~ cC132(X481) )
& ( cTOP(X481)
| ~ cC132(X481) )
& ( ~ cC130(X481)
| ~ cTOP(X481)
| cC132(X481) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_40])])]) ).
fof(c_0_72,plain,
! [X484] :
( ( cC136(X484)
| ~ cC138(X484) )
& ( cC134(X484)
| ~ cC138(X484) )
& ( ~ cC136(X484)
| ~ cC134(X484)
| cC138(X484) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_43])])]) ).
fof(c_0_73,plain,
! [X557] :
( ( cC154(X557)
| ~ cC156(X557) )
& ( cC138(X557)
| ~ cC156(X557) )
& ( ~ cC154(X557)
| ~ cC138(X557)
| cC156(X557) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_65])])]) ).
fof(c_0_74,plain,
! [X556] :
( ( cC152(X556)
| ~ cC154(X556) )
& ( cTOP(X556)
| ~ cC154(X556) )
& ( ~ cC152(X556)
| ~ cTOP(X556)
| cC154(X556) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_64])])]) ).
fof(c_0_75,plain,
! [X558] :
( ( cC22(X558)
| ~ cC158(X558) )
& ( cC156(X558)
| ~ cC158(X558) )
& ( ~ cC22(X558)
| ~ cC156(X558)
| cC158(X558) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_66])])]) ).
fof(c_0_76,plain,
! [X633] :
( ( cC172xcomp(X633)
| ~ cC174(X633) )
& ( cC168(X633)
| ~ cC174(X633) )
& ( ~ cC172xcomp(X633)
| ~ cC168(X633)
| cC174(X633) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_87])])]) ).
fof(c_0_77,plain,
! [X666] :
( ( cC174(X666)
| ~ cC180(X666) )
& ( cC178xcomp(X666)
| ~ cC180(X666) )
& ( ~ cC174(X666)
| ~ cC178xcomp(X666)
| cC180(X666) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_96])])]) ).
fof(c_0_78,plain,
! [X747] :
( ( cC36(X747)
| ~ cC38(X747) )
& ( cTOP(X747)
| ~ cC38(X747) )
& ( ~ cC36(X747)
| ~ cTOP(X747)
| cC38(X747) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_120])])]) ).
fof(c_0_79,plain,
! [X753] :
( ( cC40(X753)
| ~ cC42(X753) )
& ( cC38(X753)
| ~ cC42(X753) )
& ( ~ cC40(X753)
| ~ cC38(X753)
| cC42(X753) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_123])])]) ).
fof(c_0_80,plain,
! [X830] :
( ( cC58(X830)
| ~ cC60(X830) )
& ( cC42(X830)
| ~ cC60(X830) )
& ( ~ cC58(X830)
| ~ cC42(X830)
| cC60(X830) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_146])])]) ).
fof(c_0_81,plain,
! [X821] :
( ( cC56(X821)
| ~ cC58(X821) )
& ( cTOP(X821)
| ~ cC58(X821) )
& ( ~ cC56(X821)
| ~ cTOP(X821)
| cC58(X821) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_143])])]) ).
fof(c_0_82,plain,
! [X832] :
( ( cC60(X832)
| ~ cC64(X832) )
& ( cC62(X832)
| ~ cC64(X832) )
& ( ~ cC60(X832)
| ~ cC62(X832)
| cC64(X832) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_148])])]) ).
fof(c_0_83,plain,
! [X905] :
( ( cC64(X905)
| ~ cC82(X905) )
& ( cC80(X905)
| ~ cC82(X905) )
& ( ~ cC64(X905)
| ~ cC80(X905)
| cC82(X905) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_170])])]) ).
fof(c_0_84,plain,
! [X904] :
( ( cC78(X904)
| ~ cC80(X904) )
& ( cTOP(X904)
| ~ cC80(X904) )
& ( ~ cC78(X904)
| ~ cTOP(X904)
| cC80(X904) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_169])])]) ).
fof(c_0_85,plain,
! [X907] :
( ( cC82(X907)
| ~ cC86(X907) )
& ( cC84(X907)
| ~ cC86(X907) )
& ( ~ cC82(X907)
| ~ cC84(X907)
| cC86(X907) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_172])])]) ).
fof(c_0_86,plain,
! [X679] :
( ( cC20(X679)
| ~ cC22(X679) )
& ( cC16(X679)
| ~ cC22(X679) )
& ( ~ cC20(X679)
| ~ cC16(X679)
| cC22(X679) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_100])])]) ).
fof(c_0_87,plain,
! [X951] :
( ( cC158(X951)
| ~ cTEST(X951) )
& ( cC180(X951)
| ~ cTEST(X951) )
& ( ~ cC158(X951)
| ~ cC180(X951)
| cTEST(X951) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_186])])]) ).
cnf(c_0_88,negated_conjecture,
( xsd_integer(esk138_0)
| cowlNothing(esk137_0)
| ~ xsd_string(esk138_0)
| ~ cowlThing(esk137_0)
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
cnf(c_0_89,negated_conjecture,
( cowlNothing(esk137_0)
| xsd_string(esk138_0)
| ~ xsd_integer(esk138_0)
| ~ cC10(iV21026)
| ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC108(iV21026)
| ~ cC110(iV21026)
| ~ cC112(iV21026)
| ~ cC90(iV21026)
| ~ cC114(iV21026)
| ~ cC116(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC134(iV21026)
| ~ cC136(iV21026)
| ~ cC138(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC154(iV21026)
| ~ cC156(iV21026)
| ~ cC158(iV21026)
| ~ cC22(iV21026)
| ~ cC16(iV21026)
| ~ cC168(iV21026)
| ~ cC174(iV21026)
| ~ cC180(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC36(iV21026)
| ~ cC38(iV21026)
| ~ cC40(iV21026)
| ~ cC42(iV21026)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC60(iV21026)
| ~ cC62(iV21026)
| ~ cC64(iV21026)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC78(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC84(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_62,c_0_63]),c_0_63]),c_0_63]),c_0_63]),c_0_63])]) ).
cnf(c_0_90,plain,
~ cowlNothing(X1),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_91,plain,
( xsd_integer(X1)
| xsd_string(X1) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_92,plain,
( cC10(X1)
| ~ cC16(X1) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_93,plain,
( cC108(X1)
| ~ cC110(X1) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_94,plain,
( cC110(X1)
| ~ cC112(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_95,plain,
( cC112(X1)
| ~ cC116(X1) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_96,plain,
( cC90(X1)
| ~ cC86(X1)
| ~ cC88(X1) ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_97,plain,
( cC114(X1)
| ~ cC116(X1) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_98,plain,
( cC116(X1)
| ~ cC134(X1) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_99,plain,
( cC130(X1)
| ~ cC132(X1) ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
cnf(c_0_100,plain,
( cC132(X1)
| ~ cC134(X1) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_101,plain,
( cC134(X1)
| ~ cC138(X1) ),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_102,plain,
( cC136(X1)
| ~ cC138(X1) ),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_103,plain,
( cC138(X1)
| ~ cC156(X1) ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_104,plain,
( cC14(X1)
| ~ cC16(X1) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_105,plain,
( cC152(X1)
| ~ cC154(X1) ),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
cnf(c_0_106,plain,
( cC154(X1)
| ~ cC156(X1) ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_107,plain,
( cC156(X1)
| ~ cC158(X1) ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
cnf(c_0_108,plain,
( cC22(X1)
| ~ cC158(X1) ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
cnf(c_0_109,plain,
( cC168(X1)
| ~ cC174(X1) ),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
cnf(c_0_110,plain,
( cC174(X1)
| ~ cC180(X1) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_111,plain,
( cC36(X1)
| ~ cC38(X1) ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
cnf(c_0_112,plain,
( cC38(X1)
| ~ cC42(X1) ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
cnf(c_0_113,plain,
( cC40(X1)
| ~ cC42(X1) ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
cnf(c_0_114,plain,
( cC42(X1)
| ~ cC60(X1) ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
cnf(c_0_115,plain,
( cC56(X1)
| ~ cC58(X1) ),
inference(split_conjunct,[status(thm)],[c_0_81]) ).
cnf(c_0_116,plain,
( cC58(X1)
| ~ cC60(X1) ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
cnf(c_0_117,plain,
( cC60(X1)
| ~ cC64(X1) ),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
cnf(c_0_118,plain,
( cC62(X1)
| ~ cC64(X1) ),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
cnf(c_0_119,plain,
( cC64(X1)
| ~ cC82(X1) ),
inference(split_conjunct,[status(thm)],[c_0_83]) ).
cnf(c_0_120,plain,
( cC78(X1)
| ~ cC80(X1) ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
cnf(c_0_121,plain,
( cC80(X1)
| ~ cC82(X1) ),
inference(split_conjunct,[status(thm)],[c_0_83]) ).
cnf(c_0_122,plain,
( cC82(X1)
| ~ cC86(X1) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_123,plain,
( cC84(X1)
| ~ cC86(X1) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_124,plain,
( cC16(X1)
| ~ cC22(X1) ),
inference(split_conjunct,[status(thm)],[c_0_86]) ).
cnf(c_0_125,plain,
( cC158(X1)
| ~ cTEST(X1) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_126,plain,
cTEST(iV21026),
inference(split_conjunct,[status(thm)],[axiom_221]) ).
cnf(c_0_127,negated_conjecture,
( cowlNothing(esk137_0)
| xsd_integer(esk138_0)
| ~ xsd_string(esk138_0)
| ~ cC10(iV21026)
| ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC108(iV21026)
| ~ cC110(iV21026)
| ~ cC112(iV21026)
| ~ cC90(iV21026)
| ~ cC114(iV21026)
| ~ cC116(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC134(iV21026)
| ~ cC136(iV21026)
| ~ cC138(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC154(iV21026)
| ~ cC156(iV21026)
| ~ cC158(iV21026)
| ~ cC22(iV21026)
| ~ cC16(iV21026)
| ~ cC168(iV21026)
| ~ cC174(iV21026)
| ~ cC180(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC36(iV21026)
| ~ cC38(iV21026)
| ~ cC40(iV21026)
| ~ cC42(iV21026)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC60(iV21026)
| ~ cC62(iV21026)
| ~ cC64(iV21026)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC78(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC84(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_88,c_0_63]),c_0_63]),c_0_63]),c_0_63]),c_0_63])]) ).
cnf(c_0_128,negated_conjecture,
( xsd_string(esk138_0)
| ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC16(iV21026)
| ~ cC158(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_89,c_0_90]),c_0_91]),c_0_92]),c_0_93]),c_0_94]),c_0_95]),c_0_96]),c_0_97]),c_0_98]),c_0_99]),c_0_100]),c_0_101]),c_0_102]),c_0_103]),c_0_104]),c_0_105]),c_0_106]),c_0_107]),c_0_108]),c_0_109]),c_0_110]),c_0_111]),c_0_112]),c_0_113]),c_0_114]),c_0_115]),c_0_116]),c_0_117]),c_0_118]),c_0_119]),c_0_120]),c_0_121]),c_0_122]),c_0_123]) ).
cnf(c_0_129,plain,
( cC180(X1)
| ~ cTEST(X1) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_130,plain,
( cC16(X1)
| ~ cC158(X1) ),
inference(spm,[status(thm)],[c_0_124,c_0_108]) ).
cnf(c_0_131,plain,
cC158(iV21026),
inference(spm,[status(thm)],[c_0_125,c_0_126]) ).
cnf(c_0_132,negated_conjecture,
( xsd_integer(esk138_0)
| ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC16(iV21026)
| ~ cC158(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_127,c_0_90]),c_0_128]),c_0_92]),c_0_93]),c_0_94]),c_0_95]),c_0_96]),c_0_97]),c_0_98]),c_0_99]),c_0_100]),c_0_101]),c_0_102]),c_0_103]),c_0_104]),c_0_105]),c_0_106]),c_0_107]),c_0_108]),c_0_109]),c_0_110]),c_0_111]),c_0_112]),c_0_113]),c_0_114]),c_0_115]),c_0_116]),c_0_117]),c_0_118]),c_0_119]),c_0_120]),c_0_121]),c_0_122]),c_0_123]) ).
cnf(c_0_133,plain,
cC180(iV21026),
inference(spm,[status(thm)],[c_0_129,c_0_126]) ).
cnf(c_0_134,plain,
cC16(iV21026),
inference(spm,[status(thm)],[c_0_130,c_0_131]) ).
fof(c_0_135,plain,
! [X866,X868,X869] :
( ( ~ cC72(X866)
| ra_Px24(X866,esk118_1(X866)) )
& ( ~ ra_Px24(X868,X869)
| cC72(X868) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_158])])])])]) ).
fof(c_0_136,plain,
! [X874,X875,X876] :
( ( ~ cC72xcomp(X874)
| ~ ra_Px24(X874,X875) )
& ( ra_Px24(X876,esk120_1(X876))
| cC72xcomp(X876) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_160])])])])]) ).
fof(c_0_137,plain,
! [X883,X884,X885] :
( ( ~ cC74xcomp(X883)
| ~ ra_Px87(X883,X884) )
& ( ra_Px87(X885,esk122_1(X885))
| cC74xcomp(X885) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_163])])])])]) ).
fof(c_0_138,plain,
! [X879,X881,X882] :
( ( ~ cC74(X879)
| ra_Px87(X879,esk121_1(X879)) )
& ( ~ ra_Px87(X881,X882)
| cC74(X881) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_162])])])])]) ).
cnf(c_0_139,plain,
( ~ xsd_string(X1)
| ~ xsd_integer(X1) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_140,negated_conjecture,
( xsd_integer(esk138_0)
| ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_132,c_0_133]),c_0_134]),c_0_131])]) ).
cnf(c_0_141,negated_conjecture,
( xsd_string(esk138_0)
| ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_128,c_0_133]),c_0_134]),c_0_131])]) ).
fof(c_0_142,plain,
! [X908] :
( ( ~ cC88(X908)
| cTOP(X908) )
& ( ~ cTOP(X908)
| cC88(X908) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_173])]) ).
fof(c_0_143,plain,
! [X748,X750,X751] :
( ( rR1(X748,esk91_1(X748))
| ~ cC4(X748) )
& ( cC2xcomp(esk91_1(X748))
| ~ cC4(X748) )
& ( ~ rR1(X750,X751)
| ~ cC2xcomp(X751)
| cC4(X750) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_121])])])])])]) ).
fof(c_0_144,plain,
! [X837,X839,X840] :
( ( rR1(X837,esk111_1(X837))
| ~ cC66(X837) )
& ( cC2xcomp(esk111_1(X837))
| ~ cC66(X837) )
& ( ~ rR1(X839,X840)
| ~ cC2xcomp(X840)
| cC66(X839) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_150])])])])])]) ).
fof(c_0_145,plain,
! [X787,X789,X790] :
( ( rR1(X787,esk100_1(X787))
| ~ cC50(X787) )
& ( cC12xcomp(esk100_1(X787))
| ~ cC50(X787) )
& ( ~ rR1(X789,X790)
| ~ cC12xcomp(X790)
| cC50(X789) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_133])])])])])]) ).
fof(c_0_146,plain,
! [X758,X760,X761] :
( ( rR1(X758,esk93_1(X758))
| ~ cC44(X758) )
& ( cC2xcomp(esk93_1(X758))
| ~ cC44(X758) )
& ( ~ rR1(X760,X761)
| ~ cC2xcomp(X761)
| cC44(X760) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_125])])])])])]) ).
fof(c_0_147,plain,
! [X717,X719,X720] :
( ( rR1(X717,esk84_1(X717))
| ~ cC30(X717) )
& ( cC12xcomp(esk84_1(X717))
| ~ cC30(X717) )
& ( ~ rR1(X719,X720)
| ~ cC12xcomp(X720)
| cC30(X719) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_111])])])])])]) ).
fof(c_0_148,plain,
! [X684,X686,X687] :
( ( rR1(X684,esk76_1(X684))
| ~ cC24(X684) )
& ( cC2xcomp(esk76_1(X684))
| ~ cC24(X684) )
& ( ~ rR1(X686,X687)
| ~ cC2xcomp(X687)
| cC24(X686) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_102])])])])])]) ).
fof(c_0_149,plain,
! [X675,X677,X678] :
( ( rR1(X675,esk74_1(X675))
| ~ cC20(X675) )
& ( cC18xcomp(esk74_1(X675))
| ~ cC20(X675) )
& ( ~ rR1(X677,X678)
| ~ cC18xcomp(X678)
| cC20(X677) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_99])])])])])]) ).
fof(c_0_150,plain,
! [X878] :
( ( cC72xcomp(X878)
| ~ cC74(X878) )
& ( cC18xcomp(X878)
| ~ cC74(X878) )
& ( ~ cC72xcomp(X878)
| ~ cC18xcomp(X878)
| cC74(X878) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_161])])]) ).
cnf(c_0_151,plain,
( cC72(X1)
| ~ ra_Px24(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_135]) ).
cnf(c_0_152,plain,
( ra_Px24(X1,esk120_1(X1))
| cC72xcomp(X1) ),
inference(split_conjunct,[status(thm)],[c_0_136]) ).
cnf(c_0_153,plain,
( ~ cC74xcomp(X1)
| ~ ra_Px87(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_137]) ).
cnf(c_0_154,plain,
( ra_Px87(X1,esk121_1(X1))
| ~ cC74(X1) ),
inference(split_conjunct,[status(thm)],[c_0_138]) ).
cnf(c_0_155,negated_conjecture,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_139,c_0_140]),c_0_141]) ).
cnf(c_0_156,plain,
( cC88(X1)
| ~ cTOP(X1) ),
inference(split_conjunct,[status(thm)],[c_0_142]) ).
cnf(c_0_157,plain,
cTOP(iV21026),
inference(split_conjunct,[status(thm)],[axiom_190]) ).
cnf(c_0_158,plain,
( cC4(X1)
| ~ rR1(X1,X2)
| ~ cC2xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_159,plain,
rR1(iV21026,iV21027),
inference(split_conjunct,[status(thm)],[axiom_223]) ).
cnf(c_0_160,plain,
cC2xcomp(iV21027),
inference(split_conjunct,[status(thm)],[axiom_237]) ).
cnf(c_0_161,plain,
( cC66(X1)
| ~ rR1(X1,X2)
| ~ cC2xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_144]) ).
cnf(c_0_162,plain,
rR1(iV21030,iV21032),
inference(split_conjunct,[status(thm)],[axiom_309]) ).
cnf(c_0_163,plain,
cC2xcomp(iV21032),
inference(split_conjunct,[status(thm)],[axiom_312]) ).
cnf(c_0_164,plain,
( cC50(X1)
| ~ rR1(X1,X2)
| ~ cC12xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_145]) ).
cnf(c_0_165,plain,
rR1(iV21029,iV21033),
inference(split_conjunct,[status(thm)],[axiom_282]) ).
cnf(c_0_166,plain,
cC12xcomp(iV21033),
inference(split_conjunct,[status(thm)],[axiom_319]) ).
cnf(c_0_167,plain,
( cC44(X1)
| ~ rR1(X1,X2)
| ~ cC2xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_146]) ).
cnf(c_0_168,plain,
rR1(iV21029,iV21034),
inference(split_conjunct,[status(thm)],[axiom_281]) ).
cnf(c_0_169,plain,
cC2xcomp(iV21034),
inference(split_conjunct,[status(thm)],[axiom_325]) ).
cnf(c_0_170,plain,
( cC30(X1)
| ~ rR1(X1,X2)
| ~ cC12xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_147]) ).
cnf(c_0_171,plain,
rR1(iV21027,iV21035),
inference(split_conjunct,[status(thm)],[axiom_253]) ).
cnf(c_0_172,plain,
cC12xcomp(iV21035),
inference(split_conjunct,[status(thm)],[axiom_331]) ).
cnf(c_0_173,plain,
( cC24(X1)
| ~ rR1(X1,X2)
| ~ cC2xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_148]) ).
cnf(c_0_174,plain,
rR1(iV21027,iV21036),
inference(split_conjunct,[status(thm)],[axiom_252]) ).
cnf(c_0_175,plain,
cC2xcomp(iV21036),
inference(split_conjunct,[status(thm)],[axiom_337]) ).
cnf(c_0_176,plain,
( cC20(X1)
| ~ rR1(X1,X2)
| ~ cC18xcomp(X2) ),
inference(split_conjunct,[status(thm)],[c_0_149]) ).
cnf(c_0_177,plain,
rR1(iV21026,iV21030),
inference(split_conjunct,[status(thm)],[axiom_222]) ).
cnf(c_0_178,plain,
cC18xcomp(iV21030),
inference(split_conjunct,[status(thm)],[axiom_293]) ).
cnf(c_0_179,plain,
( cC74(X1)
| ~ cC72xcomp(X1)
| ~ cC18xcomp(X1) ),
inference(split_conjunct,[status(thm)],[c_0_150]) ).
cnf(c_0_180,plain,
( cC72xcomp(X1)
| cC72(X1) ),
inference(spm,[status(thm)],[c_0_151,c_0_152]) ).
cnf(c_0_181,plain,
( ~ cC74xcomp(X1)
| ~ cC74(X1) ),
inference(spm,[status(thm)],[c_0_153,c_0_154]) ).
cnf(c_0_182,plain,
cC74xcomp(iV21030),
inference(split_conjunct,[status(thm)],[axiom_307]) ).
cnf(c_0_183,plain,
cC156(iV21026),
inference(spm,[status(thm)],[c_0_107,c_0_131]) ).
cnf(c_0_184,negated_conjecture,
( ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_155,c_0_156]),c_0_157])]) ).
cnf(c_0_185,plain,
cC4(iV21026),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_158,c_0_159]),c_0_160])]) ).
cnf(c_0_186,plain,
cC66(iV21030),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_162]),c_0_163])]) ).
cnf(c_0_187,plain,
cC50(iV21029),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164,c_0_165]),c_0_166])]) ).
cnf(c_0_188,plain,
cC44(iV21029),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_168]),c_0_169])]) ).
cnf(c_0_189,plain,
cC30(iV21027),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_171]),c_0_172])]) ).
cnf(c_0_190,plain,
cC24(iV21027),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_174]),c_0_175])]) ).
cnf(c_0_191,plain,
cC20(iV21026),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176,c_0_177]),c_0_178])]) ).
cnf(c_0_192,plain,
( cC74(X1)
| cC72(X1)
| ~ cC18xcomp(X1) ),
inference(spm,[status(thm)],[c_0_179,c_0_180]) ).
cnf(c_0_193,plain,
~ cC74(iV21030),
inference(spm,[status(thm)],[c_0_181,c_0_182]) ).
cnf(c_0_194,plain,
cC138(iV21026),
inference(spm,[status(thm)],[c_0_103,c_0_183]) ).
cnf(c_0_195,negated_conjecture,
( ~ cC86(iV21026)
| ~ cC72(iV21030)
| ~ cC8(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_184,c_0_185])]),c_0_186]),c_0_187]),c_0_188]),c_0_189]),c_0_190]),c_0_191])]) ).
cnf(c_0_196,plain,
cC72(iV21030),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_192,c_0_178]),c_0_193]) ).
cnf(c_0_197,plain,
cC134(iV21026),
inference(spm,[status(thm)],[c_0_101,c_0_194]) ).
cnf(c_0_198,negated_conjecture,
( ~ cC86(iV21026)
| ~ cC8(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_195,c_0_196])]) ).
cnf(c_0_199,plain,
( cC86(X1)
| ~ cC90(X1) ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_200,plain,
cC116(iV21026),
inference(spm,[status(thm)],[c_0_98,c_0_197]) ).
cnf(c_0_201,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC8(iV21026) ),
inference(spm,[status(thm)],[c_0_198,c_0_199]) ).
cnf(c_0_202,plain,
( cC90(X1)
| ~ cC112(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_203,plain,
cC112(iV21026),
inference(spm,[status(thm)],[c_0_95,c_0_200]) ).
fof(c_0_204,plain,
! [X359] :
( ( cC8(X359)
| ~ cC10(X359) )
& ( cC4(X359)
| ~ cC10(X359) )
& ( ~ cC8(X359)
| ~ cC4(X359)
| cC10(X359) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_2])])]) ).
cnf(c_0_205,negated_conjecture,
~ cC8(iV21026),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_201,c_0_202]),c_0_203])]) ).
cnf(c_0_206,plain,
( cC8(X1)
| ~ cC10(X1) ),
inference(split_conjunct,[status(thm)],[c_0_204]) ).
cnf(c_0_207,plain,
cC10(iV21026),
inference(spm,[status(thm)],[c_0_92,c_0_134]) ).
cnf(c_0_208,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_206]),c_0_207])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : KRS159+1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.13/0.32 % Computer : n002.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Mon May 4 20:48:31 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.33 % start to proof: theBenchmark
% 1.58/1.84 % Version : CSE_E---1.7
% 1.58/1.84 % Problem : theBenchmark.p
% 1.58/1.84 % SZS status Theorem for theBenchmark.p
% 1.58/1.84 % SZS output start CNFRefutation
% See solution above
% 1.58/1.84 % Total time : 1.423s
%------------------------------------------------------------------------------