%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 01:01:03 PM UTC 2026
% Result : Theorem 0.15s 10.79s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 57
% Syntax : Number of formulae : 210 ( 55 unt; 0 def)
% Number of atoms : 1104 ( 0 equ)
% Maximal formula atoms : 108 ( 5 avg)
% Number of connectives : 1500 ( 606 ~; 590 |; 262 &)
% ( 42 <=>; 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 : 188 ( 4 sgn 108 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(the_axiom,conjecture,
( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X1] :
( ~ cowlNothing(X1)
& cowlThing(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(axiom_0,axiom,
! [X1] :
( ~ cowlNothing(X1)
& cowlThing(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)
<=> ( cC14(X1)
& cC10(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(axiom_15,axiom,
! [X1] :
( cC110(X1)
<=> ( cTOP(X1)
& cC108(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X1] :
( cC112(X1)
<=> ( cC90(X1)
& cC110(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_16) ).
fof(axiom_18,axiom,
! [X1] :
( cC116(X1)
<=> ( cC112(X1)
& cC114(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(axiom_174,axiom,
! [X1] :
( cC90(X1)
<=> ( cC88(X1)
& cC86(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(axiom_41,axiom,
! [X1] :
( cC134(X1)
<=> ( cC132(X1)
& cC116(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
fof(axiom_40,axiom,
! [X1] :
( cC132(X1)
<=> ( cTOP(X1)
& cC130(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(axiom_43,axiom,
! [X1] :
( cC138(X1)
<=> ( cC134(X1)
& cC136(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
fof(axiom_65,axiom,
! [X1] :
( cC156(X1)
<=> ( cC138(X1)
& cC154(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(axiom_64,axiom,
! [X1] :
( cC154(X1)
<=> ( cTOP(X1)
& cC152(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
fof(axiom_66,axiom,
! [X1] :
( cC158(X1)
<=> ( cC156(X1)
& cC22(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(axiom_100,axiom,
! [X1] :
( cC22(X1)
<=> ( cC16(X1)
& cC20(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_100) ).
fof(axiom_87,axiom,
! [X1] :
( cC174(X1)
<=> ( cC168(X1)
& cC172xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_87) ).
fof(axiom_96,axiom,
! [X1] :
( cC180(X1)
<=> ( cC178xcomp(X1)
& cC174(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_96) ).
fof(axiom_120,axiom,
! [X1] :
( cC38(X1)
<=> ( cTOP(X1)
& cC36(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(axiom_123,axiom,
! [X1] :
( cC42(X1)
<=> ( cC38(X1)
& cC40(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
fof(axiom_146,axiom,
! [X1] :
( cC60(X1)
<=> ( cC42(X1)
& cC58(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_146) ).
fof(axiom_143,axiom,
! [X1] :
( cC58(X1)
<=> ( cTOP(X1)
& cC56(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_143) ).
fof(axiom_148,axiom,
! [X1] :
( cC64(X1)
<=> ( cC62(X1)
& cC60(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_148) ).
fof(axiom_170,axiom,
! [X1] :
( cC82(X1)
<=> ( cC80(X1)
& cC64(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_170) ).
fof(axiom_169,axiom,
! [X1] :
( cC80(X1)
<=> ( cTOP(X1)
& cC78(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_169) ).
fof(axiom_172,axiom,
! [X1] :
( cC86(X1)
<=> ( cC84(X1)
& cC82(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_172) ).
fof(axiom_186,axiom,
! [X1] :
( cTEST(X1)
<=> ( cC180(X1)
& cC158(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_173,axiom,
! [X1] :
( cC88(X1)
<=> cTOP(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_173) ).
fof(axiom_121,axiom,
! [X1] :
( cC4(X1)
<=> ? [X3] :
( cC2xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_121) ).
fof(axiom_150,axiom,
! [X1] :
( cC66(X1)
<=> ? [X3] :
( cC2xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_150) ).
fof(axiom_133,axiom,
! [X1] :
( cC50(X1)
<=> ? [X3] :
( cC12xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_133) ).
fof(axiom_125,axiom,
! [X1] :
( cC44(X1)
<=> ? [X3] :
( cC2xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_125) ).
fof(axiom_111,axiom,
! [X1] :
( cC30(X1)
<=> ? [X3] :
( cC12xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_111) ).
fof(axiom_102,axiom,
! [X1] :
( cC24(X1)
<=> ? [X3] :
( cC2xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_102) ).
fof(axiom_99,axiom,
! [X1] :
( cC20(X1)
<=> ? [X3] :
( cC18xcomp(X3)
& rR1(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_99) ).
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_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_161,axiom,
! [X1] :
( cC74(X1)
<=> ( cC18xcomp(X1)
& cC72xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_161) ).
fof(axiom_307,axiom,
cC74xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_307) ).
fof(axiom_2,axiom,
! [X1] :
( cC10(X1)
<=> ( cC4(X1)
& cC8(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(c_0_57,negated_conjecture,
~ ( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X1] :
( ~ cowlNothing(X1)
& cowlThing(X1) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
fof(c_0_58,negated_conjecture,
~ ( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X1] :
( ~ cowlNothing(X1)
& cowlThing(X1) ) ),
inference(fof_simplification,[status(thm)],[c_0_57]) ).
fof(c_0_59,plain,
! [X1] :
( ~ cowlNothing(X1)
& cowlThing(X1) ),
inference(fof_simplification,[status(thm)],[axiom_0]) ).
fof(c_0_60,negated_conjecture,
( ( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| cowlNothing(esk137_0)
| ~ cowlThing(esk137_0)
| ~ xsd_integer(esk138_0)
| xsd_string(esk138_0) )
& ( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| cowlNothing(esk137_0)
| ~ cowlThing(esk137_0)
| xsd_integer(esk138_0)
| ~ xsd_string(esk138_0) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_58])])])])]) ).
fof(c_0_61,plain,
! [X4] :
( ~ cowlNothing(X4)
& cowlThing(X4) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_59])]) ).
fof(c_0_62,plain,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
inference(fof_simplification,[status(thm)],[axiom_1]) ).
cnf(c_0_63,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ cowlThing(esk137_0)
| ~ xsd_integer(esk138_0)
| cowlNothing(esk137_0)
| xsd_string(esk138_0) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_64,plain,
cowlThing(X1),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
fof(c_0_65,plain,
! [X5] :
( ( xsd_string(X5)
| xsd_integer(X5) )
& ( ~ xsd_integer(X5)
| ~ xsd_string(X5) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_62])])]) ).
fof(c_0_66,plain,
! [X206] :
( ( cC16(X206)
| ~ cC14(X206)
| ~ cC10(X206) )
& ( ~ cC16(X206)
| cC14(X206) )
& ( ~ cC16(X206)
| cC10(X206) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_67])])])]) ).
fof(c_0_67,plain,
! [X49] :
( ( cC110(X49)
| ~ cTOP(X49)
| ~ cC108(X49) )
& ( ~ cC110(X49)
| cTOP(X49) )
& ( ~ cC110(X49)
| cC108(X49) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_15])])])]) ).
fof(c_0_68,plain,
! [X50] :
( ( cC112(X50)
| ~ cC90(X50)
| ~ cC110(X50) )
& ( ~ cC112(X50)
| cC90(X50) )
& ( ~ cC112(X50)
| cC110(X50) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_16])])])]) ).
fof(c_0_69,plain,
! [X52] :
( ( cC116(X52)
| ~ cC112(X52)
| ~ cC114(X52) )
& ( ~ cC116(X52)
| cC112(X52) )
& ( ~ cC116(X52)
| cC114(X52) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_18])])])]) ).
fof(c_0_70,plain,
! [X556] :
( ( cC90(X556)
| ~ cC88(X556)
| ~ cC86(X556) )
& ( ~ cC90(X556)
| cC88(X556) )
& ( ~ cC90(X556)
| cC86(X556) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_174])])])]) ).
fof(c_0_71,plain,
! [X129] :
( ( cC134(X129)
| ~ cC132(X129)
| ~ cC116(X129) )
& ( ~ cC134(X129)
| cC132(X129) )
& ( ~ cC134(X129)
| cC116(X129) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_41])])])]) ).
fof(c_0_72,plain,
! [X128] :
( ( cC132(X128)
| ~ cTOP(X128)
| ~ cC130(X128) )
& ( ~ cC132(X128)
| cTOP(X128) )
& ( ~ cC132(X128)
| cC130(X128) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_40])])])]) ).
fof(c_0_73,plain,
! [X131] :
( ( cC138(X131)
| ~ cC134(X131)
| ~ cC136(X131) )
& ( ~ cC138(X131)
| cC134(X131) )
& ( ~ cC138(X131)
| cC136(X131) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_43])])])]) ).
fof(c_0_74,plain,
! [X204] :
( ( cC156(X204)
| ~ cC138(X204)
| ~ cC154(X204) )
& ( ~ cC156(X204)
| cC138(X204) )
& ( ~ cC156(X204)
| cC154(X204) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_65])])])]) ).
fof(c_0_75,plain,
! [X203] :
( ( cC154(X203)
| ~ cTOP(X203)
| ~ cC152(X203) )
& ( ~ cC154(X203)
| cTOP(X203) )
& ( ~ cC154(X203)
| cC152(X203) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_64])])])]) ).
fof(c_0_76,plain,
! [X205] :
( ( cC158(X205)
| ~ cC156(X205)
| ~ cC22(X205) )
& ( ~ cC158(X205)
| cC156(X205) )
& ( ~ cC158(X205)
| cC22(X205) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_66])])])]) ).
fof(c_0_77,plain,
! [X326] :
( ( cC22(X326)
| ~ cC16(X326)
| ~ cC20(X326) )
& ( ~ cC22(X326)
| cC16(X326) )
& ( ~ cC22(X326)
| cC20(X326) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_100])])])]) ).
fof(c_0_78,plain,
! [X280] :
( ( cC174(X280)
| ~ cC168(X280)
| ~ cC172xcomp(X280) )
& ( ~ cC174(X280)
| cC168(X280) )
& ( ~ cC174(X280)
| cC172xcomp(X280) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_87])])])]) ).
fof(c_0_79,plain,
! [X313] :
( ( cC180(X313)
| ~ cC178xcomp(X313)
| ~ cC174(X313) )
& ( ~ cC180(X313)
| cC178xcomp(X313) )
& ( ~ cC180(X313)
| cC174(X313) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_96])])])]) ).
fof(c_0_80,plain,
! [X394] :
( ( cC38(X394)
| ~ cTOP(X394)
| ~ cC36(X394) )
& ( ~ cC38(X394)
| cTOP(X394) )
& ( ~ cC38(X394)
| cC36(X394) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_120])])])]) ).
fof(c_0_81,plain,
! [X400] :
( ( cC42(X400)
| ~ cC38(X400)
| ~ cC40(X400) )
& ( ~ cC42(X400)
| cC38(X400) )
& ( ~ cC42(X400)
| cC40(X400) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_123])])])]) ).
fof(c_0_82,plain,
! [X477] :
( ( cC60(X477)
| ~ cC42(X477)
| ~ cC58(X477) )
& ( ~ cC60(X477)
| cC42(X477) )
& ( ~ cC60(X477)
| cC58(X477) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_146])])])]) ).
fof(c_0_83,plain,
! [X468] :
( ( cC58(X468)
| ~ cTOP(X468)
| ~ cC56(X468) )
& ( ~ cC58(X468)
| cTOP(X468) )
& ( ~ cC58(X468)
| cC56(X468) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_143])])])]) ).
fof(c_0_84,plain,
! [X479] :
( ( cC64(X479)
| ~ cC62(X479)
| ~ cC60(X479) )
& ( ~ cC64(X479)
| cC62(X479) )
& ( ~ cC64(X479)
| cC60(X479) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_148])])])]) ).
fof(c_0_85,plain,
! [X552] :
( ( cC82(X552)
| ~ cC80(X552)
| ~ cC64(X552) )
& ( ~ cC82(X552)
| cC80(X552) )
& ( ~ cC82(X552)
| cC64(X552) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_170])])])]) ).
fof(c_0_86,plain,
! [X551] :
( ( cC80(X551)
| ~ cTOP(X551)
| ~ cC78(X551) )
& ( ~ cC80(X551)
| cTOP(X551) )
& ( ~ cC80(X551)
| cC78(X551) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_169])])])]) ).
fof(c_0_87,plain,
! [X554] :
( ( cC86(X554)
| ~ cC84(X554)
| ~ cC82(X554) )
& ( ~ cC86(X554)
| cC84(X554) )
& ( ~ cC86(X554)
| cC82(X554) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_172])])])]) ).
fof(c_0_88,plain,
! [X598] :
( ( cTEST(X598)
| ~ cC180(X598)
| ~ cC158(X598) )
& ( ~ cTEST(X598)
| cC180(X598) )
& ( ~ cTEST(X598)
| cC158(X598) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_186])])])]) ).
cnf(c_0_89,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ cowlThing(esk137_0)
| ~ xsd_string(esk138_0)
| cowlNothing(esk137_0)
| xsd_integer(esk138_0) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_90,negated_conjecture,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(esk138_0)
| xsd_string(esk138_0)
| cowlNothing(esk137_0) ),
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_63,c_0_64]),c_0_64]),c_0_64]),c_0_64]),c_0_64])]) ).
cnf(c_0_91,plain,
~ cowlNothing(X1),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_92,plain,
( xsd_string(X1)
| xsd_integer(X1) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_93,plain,
( ~ cC16(X1)
| cC10(X1) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_94,plain,
( ~ cC110(X1)
| cC108(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_95,plain,
( ~ cC112(X1)
| cC110(X1) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_96,plain,
( ~ cC116(X1)
| cC112(X1) ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_97,plain,
( ~ cC88(X1)
| ~ cC86(X1)
| cC90(X1) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_98,plain,
( ~ cC116(X1)
| cC114(X1) ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_99,plain,
( ~ cC134(X1)
| cC116(X1) ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
cnf(c_0_100,plain,
( ~ cC132(X1)
| cC130(X1) ),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_101,plain,
( ~ cC134(X1)
| cC132(X1) ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
cnf(c_0_102,plain,
( ~ cC138(X1)
| cC134(X1) ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_103,plain,
( ~ cC138(X1)
| cC136(X1) ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_104,plain,
( ~ cC156(X1)
| cC138(X1) ),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
cnf(c_0_105,plain,
( ~ cC16(X1)
| cC14(X1) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_106,plain,
( ~ cC154(X1)
| cC152(X1) ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
cnf(c_0_107,plain,
( ~ cC156(X1)
| cC154(X1) ),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
cnf(c_0_108,plain,
( ~ cC158(X1)
| cC156(X1) ),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
cnf(c_0_109,plain,
( ~ cC16(X1)
| ~ cC20(X1)
| cC22(X1) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_110,plain,
( ~ cC174(X1)
| cC168(X1) ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
cnf(c_0_111,plain,
( ~ cC180(X1)
| cC174(X1) ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
cnf(c_0_112,plain,
( ~ cC38(X1)
| cC36(X1) ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
cnf(c_0_113,plain,
( ~ cC42(X1)
| cC38(X1) ),
inference(split_conjunct,[status(thm)],[c_0_81]) ).
cnf(c_0_114,plain,
( ~ cC42(X1)
| cC40(X1) ),
inference(split_conjunct,[status(thm)],[c_0_81]) ).
cnf(c_0_115,plain,
( ~ cC60(X1)
| cC42(X1) ),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
cnf(c_0_116,plain,
( ~ cC58(X1)
| cC56(X1) ),
inference(split_conjunct,[status(thm)],[c_0_83]) ).
cnf(c_0_117,plain,
( ~ cC60(X1)
| cC58(X1) ),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
cnf(c_0_118,plain,
( ~ cC64(X1)
| cC60(X1) ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
cnf(c_0_119,plain,
( ~ cC64(X1)
| cC62(X1) ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
cnf(c_0_120,plain,
( ~ cC82(X1)
| cC64(X1) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_121,plain,
( ~ cC80(X1)
| cC78(X1) ),
inference(split_conjunct,[status(thm)],[c_0_86]) ).
cnf(c_0_122,plain,
( ~ cC82(X1)
| cC80(X1) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_123,plain,
( ~ cC86(X1)
| cC82(X1) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_124,plain,
( ~ cC86(X1)
| cC84(X1) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_125,plain,
( ~ cC22(X1)
| cC16(X1) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_126,plain,
( ~ cC158(X1)
| cC22(X1) ),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
cnf(c_0_127,plain,
( ~ cTEST(X1)
| cC158(X1) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
cnf(c_0_128,plain,
cTEST(iV21026),
inference(split_conjunct,[status(thm)],[axiom_221]) ).
cnf(c_0_129,negated_conjecture,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ xsd_string(esk138_0)
| xsd_integer(esk138_0)
| cowlNothing(esk137_0) ),
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_89,c_0_64]),c_0_64]),c_0_64]),c_0_64]),c_0_64])]) ).
cnf(c_0_130,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC158(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| xsd_string(esk138_0) ),
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_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]),c_0_124]) ).
cnf(c_0_131,plain,
( ~ cTEST(X1)
| cC180(X1) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
cnf(c_0_132,plain,
( ~ cC158(X1)
| cC16(X1) ),
inference(spm,[status(thm)],[c_0_125,c_0_126]) ).
cnf(c_0_133,plain,
cC158(iV21026),
inference(spm,[status(thm)],[c_0_127,c_0_128]) ).
cnf(c_0_134,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC158(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| xsd_integer(esk138_0) ),
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_129,c_0_91]),c_0_130]),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]),c_0_124]) ).
cnf(c_0_135,plain,
cC180(iV21026),
inference(spm,[status(thm)],[c_0_131,c_0_128]) ).
cnf(c_0_136,plain,
cC16(iV21026),
inference(spm,[status(thm)],[c_0_132,c_0_133]) ).
cnf(c_0_137,plain,
( ~ xsd_integer(X1)
| ~ xsd_string(X1) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_138,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| xsd_integer(esk138_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_134,c_0_135]),c_0_136]),c_0_133])]) ).
cnf(c_0_139,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| xsd_string(esk138_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_130,c_0_135]),c_0_136]),c_0_133])]) ).
fof(c_0_140,plain,
! [X555] :
( ( cC88(X555)
| ~ cTOP(X555) )
& ( cTOP(X555)
| ~ cC88(X555) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_173])])]) ).
fof(c_0_141,plain,
! [X395,X397,X398] :
( ( cC4(X397)
| ~ cC2xcomp(X398)
| ~ rR1(X397,X398) )
& ( ~ cC4(X395)
| cC2xcomp(esk91_1(X395)) )
& ( ~ cC4(X395)
| rR1(X395,esk91_1(X395)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_142,plain,
! [X484,X486,X487] :
( ( cC66(X486)
| ~ cC2xcomp(X487)
| ~ rR1(X486,X487) )
& ( ~ cC66(X484)
| cC2xcomp(esk111_1(X484)) )
& ( ~ cC66(X484)
| rR1(X484,esk111_1(X484)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_143,plain,
! [X434,X436,X437] :
( ( cC50(X436)
| ~ cC12xcomp(X437)
| ~ rR1(X436,X437) )
& ( ~ cC50(X434)
| cC12xcomp(esk100_1(X434)) )
& ( ~ cC50(X434)
| rR1(X434,esk100_1(X434)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_144,plain,
! [X405,X407,X408] :
( ( cC44(X407)
| ~ cC2xcomp(X408)
| ~ rR1(X407,X408) )
& ( ~ cC44(X405)
| cC2xcomp(esk93_1(X405)) )
& ( ~ cC44(X405)
| rR1(X405,esk93_1(X405)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_145,plain,
! [X364,X366,X367] :
( ( cC30(X366)
| ~ cC12xcomp(X367)
| ~ rR1(X366,X367) )
& ( ~ cC30(X364)
| cC12xcomp(esk84_1(X364)) )
& ( ~ cC30(X364)
| rR1(X364,esk84_1(X364)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_146,plain,
! [X331,X333,X334] :
( ( cC24(X333)
| ~ cC2xcomp(X334)
| ~ rR1(X333,X334) )
& ( ~ cC24(X331)
| cC2xcomp(esk76_1(X331)) )
& ( ~ cC24(X331)
| rR1(X331,esk76_1(X331)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_147,plain,
! [X322,X324,X325] :
( ( cC20(X324)
| ~ cC18xcomp(X325)
| ~ rR1(X324,X325) )
& ( ~ cC20(X322)
| cC18xcomp(esk74_1(X322)) )
& ( ~ cC20(X322)
| rR1(X322,esk74_1(X322)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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_148,plain,
! [X513,X515,X516] :
( ( cC72(X515)
| ~ ra_Px24(X515,X516) )
& ( ra_Px24(X513,esk118_1(X513))
| ~ cC72(X513) ) ),
inference(fof_nnf,[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_158])])])])])]) ).
fof(c_0_149,plain,
! [X521,X522,X523] :
( ( cC72xcomp(X523)
| ra_Px24(X523,esk120_1(X523)) )
& ( ~ ra_Px24(X521,X522)
| ~ cC72xcomp(X521) ) ),
inference(fof_nnf,[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_160])])])])])]) ).
fof(c_0_150,plain,
! [X530,X531,X532] :
( ( cC74xcomp(X532)
| ra_Px87(X532,esk122_1(X532)) )
& ( ~ ra_Px87(X530,X531)
| ~ cC74xcomp(X530) ) ),
inference(fof_nnf,[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_163])])])])])]) ).
fof(c_0_151,plain,
! [X526,X528,X529] :
( ( cC74(X528)
| ~ ra_Px87(X528,X529) )
& ( ra_Px87(X526,esk121_1(X526))
| ~ cC74(X526) ) ),
inference(fof_nnf,[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_162])])])])])]) ).
cnf(c_0_152,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC86(iV21026)
| ~ cC88(iV21026) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_139]) ).
cnf(c_0_153,plain,
( ~ cTOP(X1)
| cC88(X1) ),
inference(split_conjunct,[status(thm)],[c_0_140]) ).
cnf(c_0_154,plain,
cTOP(iV21026),
inference(split_conjunct,[status(thm)],[axiom_190]) ).
cnf(c_0_155,plain,
( ~ cC2xcomp(X2)
| ~ rR1(X1,X2)
| cC4(X1) ),
inference(split_conjunct,[status(thm)],[c_0_141]) ).
cnf(c_0_156,plain,
rR1(iV21026,iV21027),
inference(split_conjunct,[status(thm)],[axiom_223]) ).
cnf(c_0_157,plain,
cC2xcomp(iV21027),
inference(split_conjunct,[status(thm)],[axiom_237]) ).
cnf(c_0_158,plain,
( ~ cC2xcomp(X2)
| ~ rR1(X1,X2)
| cC66(X1) ),
inference(split_conjunct,[status(thm)],[c_0_142]) ).
cnf(c_0_159,plain,
rR1(iV21030,iV21032),
inference(split_conjunct,[status(thm)],[axiom_309]) ).
cnf(c_0_160,plain,
cC2xcomp(iV21032),
inference(split_conjunct,[status(thm)],[axiom_312]) ).
cnf(c_0_161,plain,
( ~ cC12xcomp(X2)
| ~ rR1(X1,X2)
| cC50(X1) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_162,plain,
rR1(iV21029,iV21033),
inference(split_conjunct,[status(thm)],[axiom_282]) ).
cnf(c_0_163,plain,
cC12xcomp(iV21033),
inference(split_conjunct,[status(thm)],[axiom_319]) ).
cnf(c_0_164,plain,
( ~ cC2xcomp(X2)
| ~ rR1(X1,X2)
| cC44(X1) ),
inference(split_conjunct,[status(thm)],[c_0_144]) ).
cnf(c_0_165,plain,
rR1(iV21029,iV21034),
inference(split_conjunct,[status(thm)],[axiom_281]) ).
cnf(c_0_166,plain,
cC2xcomp(iV21034),
inference(split_conjunct,[status(thm)],[axiom_325]) ).
cnf(c_0_167,plain,
( ~ cC12xcomp(X2)
| ~ rR1(X1,X2)
| cC30(X1) ),
inference(split_conjunct,[status(thm)],[c_0_145]) ).
cnf(c_0_168,plain,
rR1(iV21027,iV21035),
inference(split_conjunct,[status(thm)],[axiom_253]) ).
cnf(c_0_169,plain,
cC12xcomp(iV21035),
inference(split_conjunct,[status(thm)],[axiom_331]) ).
cnf(c_0_170,plain,
( ~ cC2xcomp(X2)
| ~ rR1(X1,X2)
| cC24(X1) ),
inference(split_conjunct,[status(thm)],[c_0_146]) ).
cnf(c_0_171,plain,
rR1(iV21027,iV21036),
inference(split_conjunct,[status(thm)],[axiom_252]) ).
cnf(c_0_172,plain,
cC2xcomp(iV21036),
inference(split_conjunct,[status(thm)],[axiom_337]) ).
cnf(c_0_173,plain,
( ~ cC18xcomp(X2)
| ~ rR1(X1,X2)
| cC20(X1) ),
inference(split_conjunct,[status(thm)],[c_0_147]) ).
cnf(c_0_174,plain,
rR1(iV21026,iV21030),
inference(split_conjunct,[status(thm)],[axiom_222]) ).
cnf(c_0_175,plain,
cC18xcomp(iV21030),
inference(split_conjunct,[status(thm)],[axiom_293]) ).
fof(c_0_176,plain,
! [X525] :
( ( cC74(X525)
| ~ cC18xcomp(X525)
| ~ cC72xcomp(X525) )
& ( ~ cC74(X525)
| cC18xcomp(X525) )
& ( ~ cC74(X525)
| cC72xcomp(X525) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_161])])])]) ).
cnf(c_0_177,plain,
( ~ ra_Px24(X1,X2)
| cC72(X1) ),
inference(split_conjunct,[status(thm)],[c_0_148]) ).
cnf(c_0_178,plain,
( cC72xcomp(X1)
| ra_Px24(X1,esk120_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_149]) ).
cnf(c_0_179,plain,
( ~ ra_Px87(X1,X2)
| ~ cC74xcomp(X1) ),
inference(split_conjunct,[status(thm)],[c_0_150]) ).
cnf(c_0_180,plain,
( ~ cC74(X1)
| ra_Px87(X1,esk121_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_151]) ).
cnf(c_0_181,plain,
cC156(iV21026),
inference(spm,[status(thm)],[c_0_108,c_0_133]) ).
cnf(c_0_182,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC4(iV21026)
| ~ cC20(iV21026)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC86(iV21026) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_152,c_0_153]),c_0_154])]) ).
cnf(c_0_183,plain,
cC4(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_184,plain,
cC66(iV21030),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_158,c_0_159]),c_0_160])]) ).
cnf(c_0_185,plain,
cC50(iV21029),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_162]),c_0_163])]) ).
cnf(c_0_186,plain,
cC44(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_187,plain,
cC30(iV21027),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_168]),c_0_169])]) ).
cnf(c_0_188,plain,
cC24(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_189,plain,
cC20(iV21026),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_174]),c_0_175])]) ).
cnf(c_0_190,plain,
( ~ cC18xcomp(X1)
| ~ cC72xcomp(X1)
| cC74(X1) ),
inference(split_conjunct,[status(thm)],[c_0_176]) ).
cnf(c_0_191,plain,
( cC72(X1)
| cC72xcomp(X1) ),
inference(spm,[status(thm)],[c_0_177,c_0_178]) ).
cnf(c_0_192,plain,
( ~ cC74(X1)
| ~ cC74xcomp(X1) ),
inference(spm,[status(thm)],[c_0_179,c_0_180]) ).
cnf(c_0_193,plain,
cC74xcomp(iV21030),
inference(split_conjunct,[status(thm)],[axiom_307]) ).
cnf(c_0_194,plain,
cC138(iV21026),
inference(spm,[status(thm)],[c_0_104,c_0_181]) ).
cnf(c_0_195,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC72(iV21030)
| ~ cC86(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_182,c_0_183])]),c_0_184]),c_0_185]),c_0_186]),c_0_187]),c_0_188]),c_0_189])]) ).
cnf(c_0_196,plain,
( ~ cC18xcomp(X1)
| cC72(X1)
| cC74(X1) ),
inference(spm,[status(thm)],[c_0_190,c_0_191]) ).
cnf(c_0_197,plain,
~ cC74(iV21030),
inference(spm,[status(thm)],[c_0_192,c_0_193]) ).
cnf(c_0_198,plain,
cC134(iV21026),
inference(spm,[status(thm)],[c_0_102,c_0_194]) ).
cnf(c_0_199,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC86(iV21026) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_196]),c_0_175])]),c_0_197]) ).
cnf(c_0_200,plain,
( ~ cC90(X1)
| cC86(X1) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_201,plain,
cC116(iV21026),
inference(spm,[status(thm)],[c_0_99,c_0_198]) ).
cnf(c_0_202,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC90(iV21026) ),
inference(spm,[status(thm)],[c_0_199,c_0_200]) ).
cnf(c_0_203,plain,
( ~ cC112(X1)
| cC90(X1) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_204,plain,
cC112(iV21026),
inference(spm,[status(thm)],[c_0_96,c_0_201]) ).
fof(c_0_205,plain,
! [X6] :
( ( cC10(X6)
| ~ cC4(X6)
| ~ cC8(X6) )
& ( ~ cC10(X6)
| cC4(X6) )
& ( ~ cC10(X6)
| cC8(X6) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_2])])])]) ).
cnf(c_0_206,negated_conjecture,
~ cC8(iV21026),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_202,c_0_203]),c_0_204])]) ).
cnf(c_0_207,plain,
( ~ cC10(X1)
| cC8(X1) ),
inference(split_conjunct,[status(thm)],[c_0_205]) ).
cnf(c_0_208,plain,
cC10(iV21026),
inference(spm,[status(thm)],[c_0_93,c_0_136]) ).
cnf(c_0_209,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_206,c_0_207]),c_0_208])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/10.38 % Computer : n007.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Sun Sep 20 22:53:16 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.11/10.39 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/10.43 Running first-order theorem proving
% 0.15/10.43 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/10.79 % Version: 3.5.1
% 0.15/10.79 % Preprocessing class: FSLMSMSMSSSNFFN.
% 0.15/10.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/10.79 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 0.15/10.79 % Starting new_bool_3 with 600s (2) cores
% 0.15/10.79 % Starting new_bool_1 with 300s (1) cores
% 0.15/10.79 % Starting sh5l with 300s (1) cores
% 0.15/10.79 % G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with pid 3765886 completed with status 0
% 0.15/10.79 % Result found by G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S
% 0.15/10.79 % Preprocessing class: FSLMSMSMSSSNFFN.
% 0.15/10.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/10.79 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 0.15/10.79 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.15/10.79 % No SInE strategy applied
% 0.15/10.79 % Search class: FGHNF-FSLM11-SFFFFFNN
% 0.15/10.79 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.15/10.79 % Starting SubtermCWHack with 109s (1) cores
% 0.15/10.79 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 0.15/10.79 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with 113s (1) cores
% 0.15/10.79 % Starting new_bool_3 with 113s (1) cores
% 0.15/10.79 % G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with pid 3765896 completed with status 0
% 0.15/10.79 % Result found by G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y
% 0.15/10.79 % Preprocessing class: FSLMSMSMSSSNFFN.
% 0.15/10.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/10.79 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 1200s (4) cores
% 0.15/10.79 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.15/10.79 % No SInE strategy applied
% 0.15/10.79 % Search class: FGHNF-FSLM11-SFFFFFNN
% 0.15/10.79 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.15/10.79 % Starting SubtermCWHack with 109s (1) cores
% 0.15/10.79 % Starting G-E--_207_C18_F1_AE_CS_SP_PI_PS_S2S with 121s (1) cores
% 0.15/10.79 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with 113s (1) cores
% 0.15/10.79 % Preprocessing time : 0.007 s
% 0.15/10.79 % Presaturation interreduction done
% 0.15/10.79
% 0.15/10.79 % Proof found!
% 0.15/10.79 % SZS status Theorem
% 0.15/10.79 % SZS output start CNFRefutation
% See solution above
% 0.15/10.79 % Parsed axioms : 343
% 0.15/10.79 % Removed by relevancy pruning/SinE : 0
% 0.15/10.79 % Initial clauses : 610
% 0.15/10.79 % Removed in clause preprocessing : 12
% 0.15/10.79 % Initial clauses in saturation : 598
% 0.15/10.79 % Processed clauses : 2485
% 0.15/10.79 % ...of these trivial : 50
% 0.15/10.79 % ...subsumed : 117
% 0.15/10.79 % ...remaining for further processing : 2318
% 0.15/10.79 % Other redundant clauses eliminated : 0
% 0.15/10.79 % Clauses deleted for lack of memory : 0
% 0.15/10.79 % Backward-subsumed : 250
% 0.15/10.79 % Backward-rewritten : 1
% 0.15/10.79 % Generated clauses : 2906
% 0.15/10.79 % ...of the previous two non-redundant : 2545
% 0.15/10.79 % ...aggressively subsumed : 0
% 0.15/10.79 % Contextual simplify-reflections : 80
% 0.15/10.79 % Paramodulations : 2906
% 0.15/10.79 % Factorizations : 0
% 0.15/10.79 % NegExts : 0
% 0.15/10.79 % Equation resolutions : 0
% 0.15/10.79 % Disequality decompositions : 0
% 0.15/10.79 % Total rewrite steps : 206
% 0.15/10.79 % ...of those cached : 114
% 0.15/10.79 % Propositional unsat checks : 0
% 0.15/10.79 % Propositional check models : 0
% 0.15/10.79 % Propositional check unsatisfiable : 0
% 0.15/10.79 % Propositional clauses : 0
% 0.15/10.79 % Propositional clauses after purity: 0
% 0.15/10.79 % Propositional unsat core size : 0
% 0.15/10.79 % Propositional preprocessing time : 0.000
% 0.15/10.79 % Propositional encoding time : 0.000
% 0.15/10.79 % Propositional solver time : 0.000
% 0.15/10.79 % Success case prop preproc time : 0.000
% 0.15/10.79 % Success case prop encoding time : 0.000
% 0.15/10.79 % Success case prop solver time : 0.000
% 0.15/10.79 % Current number of processed clauses : 1469
% 0.15/10.79 % Positive orientable unit clauses : 208
% 0.15/10.79 % Positive unorientable unit clauses: 0
% 0.15/10.79 % Negative unit clauses : 232
% 0.15/10.79 % Non-unit-clauses : 1029
% 0.15/10.79 % Current number of unprocessed clauses: 1226
% 0.15/10.79 % ...number of literals in the above : 3675
% 0.15/10.79 % Current number of archived formulas : 0
% 0.15/10.79 % Current number of archived clauses : 850
% 0.15/10.79 % Clause-clause subsumption calls (NU) : 308956
% 0.15/10.79 % Rec. Clause-clause subsumption calls : 225356
% 0.15/10.79 % Non-unit clause-clause subsumptions : 108
% 0.15/10.79 % Unit Clause-clause subsumption calls : 39281
% 0.15/10.79 % Rewrite failures with RHS unbound : 0
% 0.15/10.79 % BW rewrite match attempts : 1
% 0.15/10.79 % BW rewrite match successes : 1
% 0.15/10.79 % Condensation attempts : 0
% 0.15/10.79 % Condensation successes : 0
% 0.15/10.79 % Termbank termtop insertions : 58846
% 0.15/10.79 % Search garbage collected termcells : 7850
% 0.15/10.79
% 0.15/10.79 % -------------------------------------------------
% 0.15/10.79 % User time : 0.210 s
% 0.15/10.79 % System time : 0.013 s
% 0.15/10.79 % Total time : 0.223 s
% 0.15/10.79 % Maximum resident set size: 5168 pages
% 0.15/10.79
% 0.15/10.79 % -------------------------------------------------
% 0.15/10.79 % User time : 0.788 s
% 0.15/10.79 % System time : 0.047 s
% 0.15/10.79 % Total time : 0.835 s
% 0.15/10.79 % Maximum resident set size: 5120 pages
% 0.15/10.79 % E exiting
%------------------------------------------------------------------------------