%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 08:47:25 AM UTC 2026
% Result : Theorem 42.65s 43.02s
% Output : Proof 42.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 85
% Syntax : Number of formulae : 1113 ( 443 unt; 0 def)
% Number of atoms : 3493 ( 0 equ)
% Maximal formula atoms : 62 ( 3 avg)
% Number of connectives : 4083 (1703 ~;1680 |; 635 &)
% ( 64 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 56 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 131 ( 130 usr; 3 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 9 con; 0-1 aty)
% Number of variables : 959 ( 12 sgn 707 !; 118 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('theBenchmark.p',axiom_1) ).
fof(axiom_2,axiom,
! [X] :
( cC10(X)
<=> ( cC4(X)
& cC8(X) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_15,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X] :
( cC112(X)
<=> ( cC90(X)
& cC110(X) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_18,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_40,axiom,
! [X] :
( cC132(X)
<=> ( cTOP(X)
& cC130(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC134(X)
<=> ( cC132(X)
& cC116(X) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_43,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_64,axiom,
! [X] :
( cC154(X)
<=> ( cTOP(X)
& cC152(X) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC156(X)
<=> ( cC138(X)
& cC154(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cC16(X)
<=> ( cC14(X)
& cC10(X) ) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_87,axiom,
! [X] :
( cC174(X)
<=> ( cC168(X)
& cC172xcomp(X) ) ),
file('theBenchmark.p',axiom_87) ).
fof(axiom_96,axiom,
! [X] :
( cC180(X)
<=> ( cC178xcomp(X)
& cC174(X) ) ),
file('theBenchmark.p',axiom_96) ).
fof(axiom_100,axiom,
! [X] :
( cC22(X)
<=> ( cC16(X)
& cC20(X) ) ),
file('theBenchmark.p',axiom_100) ).
fof(axiom_101,axiom,
! [X] :
( cC24(X)
<=> ? [Y0] : ra_Px5(X,Y0) ),
file('theBenchmark.p',axiom_101) ).
fof(axiom_103,axiom,
! [X] :
( cC24xcomp(X)
<=> ~ ? [Y] : ra_Px5(X,Y) ),
file('theBenchmark.p',axiom_103) ).
fof(axiom_105,axiom,
! [X] :
( cC26(X)
<=> ( cC2xcomp(X)
& cC24xcomp(X) ) ),
file('theBenchmark.p',axiom_105) ).
fof(axiom_107,axiom,
! [X] :
( cC28(X)
<=> ? [Y] :
( cC26(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_107) ).
fof(axiom_108,axiom,
! [X] :
( cC28(X)
<=> ? [Y0] : ra_Px9(X,Y0) ),
file('theBenchmark.p',axiom_108) ).
fof(axiom_109,axiom,
! [X] :
( cC28xcomp(X)
<=> ~ ? [Y] : ra_Px9(X,Y) ),
file('theBenchmark.p',axiom_109) ).
fof(axiom_111,axiom,
! [X] :
( cC30(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_111) ).
fof(axiom_119,axiom,
! [X] :
( cC36(X)
<=> ( cC28xcomp(X)
& cC34xcomp(X) ) ),
file('theBenchmark.p',axiom_119) ).
fof(axiom_120,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('theBenchmark.p',axiom_120) ).
fof(axiom_122,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_122) ).
fof(axiom_123,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('theBenchmark.p',axiom_123) ).
fof(axiom_124,axiom,
! [X] :
( cC44(X)
<=> ~ ? [Y] : ra_Px13(X,Y) ),
file('theBenchmark.p',axiom_124) ).
fof(axiom_126,axiom,
! [X] :
( cC44xcomp(X)
<=> ? [Y0] : ra_Px13(X,Y0) ),
file('theBenchmark.p',axiom_126) ).
fof(axiom_127,axiom,
! [X] :
( cC46(X)
<=> ? [Y0] : ra_Px90(X,Y0) ),
file('theBenchmark.p',axiom_127) ).
fof(axiom_128,axiom,
! [X] :
( cC46(X)
<=> ( cC12xcomp(X)
& cC44xcomp(X) ) ),
file('theBenchmark.p',axiom_128) ).
fof(axiom_129,axiom,
! [X] :
( cC46xcomp(X)
<=> ~ ? [Y] : ra_Px90(X,Y) ),
file('theBenchmark.p',axiom_129) ).
fof(axiom_131,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( cC46(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_131) ).
fof(axiom_134,axiom,
! [X] :
( cC50(X)
<=> ~ ? [Y] : ra_Px16(X,Y) ),
file('theBenchmark.p',axiom_134) ).
fof(axiom_135,axiom,
! [X] :
( cC50xcomp(X)
<=> ? [Y0] : ra_Px16(X,Y0) ),
file('theBenchmark.p',axiom_135) ).
fof(axiom_137,axiom,
! [X] :
( cC52(X)
<=> ( cC12xcomp(X)
& cC50xcomp(X) ) ),
file('theBenchmark.p',axiom_137) ).
fof(axiom_139,axiom,
! [X] :
( cC54(X)
<=> ? [Y] :
( cC52(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_139) ).
fof(axiom_140,axiom,
! [X] :
( cC54(X)
<=> ? [Y0] : ra_Px18(X,Y0) ),
file('theBenchmark.p',axiom_140) ).
fof(axiom_141,axiom,
! [X] :
( cC54xcomp(X)
<=> ~ ? [Y] : ra_Px18(X,Y) ),
file('theBenchmark.p',axiom_141) ).
fof(axiom_142,axiom,
! [X] :
( cC56(X)
<=> ( cC54xcomp(X)
& cC48xcomp(X) ) ),
file('theBenchmark.p',axiom_142) ).
fof(axiom_143,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('theBenchmark.p',axiom_143) ).
fof(axiom_146,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('theBenchmark.p',axiom_146) ).
fof(axiom_147,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_147) ).
fof(axiom_148,axiom,
! [X] :
( cC64(X)
<=> ( cC62(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_148) ).
fof(axiom_149,axiom,
! [X] :
( cC66(X)
<=> ? [Y0] : ra_Px21(X,Y0) ),
file('theBenchmark.p',axiom_149) ).
fof(axiom_151,axiom,
! [X] :
( cC66xcomp(X)
<=> ~ ? [Y] : ra_Px21(X,Y) ),
file('theBenchmark.p',axiom_151) ).
fof(axiom_153,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC18xcomp(X) ) ),
file('theBenchmark.p',axiom_153) ).
fof(axiom_155,axiom,
! [X] :
( cC70(X)
<=> ? [Y] :
( cC68(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_155) ).
fof(axiom_156,axiom,
! [X] :
( cC70(X)
<=> ~ ? [Y] : ra_Px25(X,Y) ),
file('theBenchmark.p',axiom_156) ).
fof(axiom_157,axiom,
! [X] :
( cC70xcomp(X)
<=> ? [Y0] : ra_Px25(X,Y0) ),
file('theBenchmark.p',axiom_157) ).
fof(axiom_158,axiom,
! [X] :
( cC72(X)
<=> ? [Y0] : ra_Px24(X,Y0) ),
file('theBenchmark.p',axiom_158) ).
fof(axiom_160,axiom,
! [X] :
( cC72xcomp(X)
<=> ~ ? [Y] : ra_Px24(X,Y) ),
file('theBenchmark.p',axiom_160) ).
fof(axiom_161,axiom,
! [X] :
( cC74(X)
<=> ( cC18xcomp(X)
& cC72xcomp(X) ) ),
file('theBenchmark.p',axiom_161) ).
fof(axiom_164,axiom,
! [X] :
( cC76(X)
<=> ? [Y] :
( cC74(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_164) ).
fof(axiom_165,axiom,
! [X] :
( cC76(X)
<=> ? [Y0] : ra_Px26(X,Y0) ),
file('theBenchmark.p',axiom_165) ).
fof(axiom_166,axiom,
! [X] :
( cC76xcomp(X)
<=> ~ ? [Y] : ra_Px26(X,Y) ),
file('theBenchmark.p',axiom_166) ).
fof(axiom_167,axiom,
! [X] :
( cC78(X)
<=> ( cC76xcomp(X)
& cC70xcomp(X) ) ),
file('theBenchmark.p',axiom_167) ).
fof(axiom_169,axiom,
! [X] :
( cC80(X)
<=> ( cTOP(X)
& cC78(X) ) ),
file('theBenchmark.p',axiom_169) ).
fof(axiom_170,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& cC64(X) ) ),
file('theBenchmark.p',axiom_170) ).
fof(axiom_171,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_171) ).
fof(axiom_172,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('theBenchmark.p',axiom_172) ).
fof(axiom_174,axiom,
! [X] :
( cC90(X)
<=> ( cC88(X)
& cC86(X) ) ),
file('theBenchmark.p',axiom_174) ).
fof(axiom_186,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('theBenchmark.p',axiom_186) ).
fof(axiom_189,axiom,
! [X] :
( rR1(iV21026,X)
=> cC46xcomp(X) ),
file('theBenchmark.p',axiom_189) ).
fof(axiom_190,axiom,
cTOP(iV21026),
file('theBenchmark.p',axiom_190) ).
fof(axiom_195,axiom,
cC76xcomp(iV21026),
file('theBenchmark.p',axiom_195) ).
fof(axiom_203,axiom,
cC34xcomp(iV21026),
file('theBenchmark.p',axiom_203) ).
fof(axiom_205,axiom,
cC28xcomp(iV21026),
file('theBenchmark.p',axiom_205) ).
fof(axiom_209,axiom,
cC54xcomp(iV21026),
file('theBenchmark.p',axiom_209) ).
fof(axiom_215,axiom,
cC70xcomp(iV21026),
file('theBenchmark.p',axiom_215) ).
fof(axiom_217,axiom,
cC48xcomp(iV21026),
file('theBenchmark.p',axiom_217) ).
fof(axiom_219,axiom,
cowlThing(iV21026),
file('theBenchmark.p',axiom_219) ).
fof(axiom_221,axiom,
cTEST(iV21026),
file('theBenchmark.p',axiom_221) ).
fof(axiom_222,axiom,
rR1(iV21026,iV21030),
file('theBenchmark.p',axiom_222) ).
fof(axiom_223,axiom,
rR1(iV21026,iV21027),
file('theBenchmark.p',axiom_223) ).
fof(axiom_225,axiom,
rR1(iV21026,iV21029),
file('theBenchmark.p',axiom_225) ).
fof(axiom_237,axiom,
cC2xcomp(iV21027),
file('theBenchmark.p',axiom_237) ).
fof(axiom_248,axiom,
cowlThing(iV21027),
file('theBenchmark.p',axiom_248) ).
fof(axiom_253,axiom,
rR1(iV21027,iV21035),
file('theBenchmark.p',axiom_253) ).
fof(axiom_265,axiom,
cC12xcomp(iV21029),
file('theBenchmark.p',axiom_265) ).
fof(axiom_278,axiom,
cowlThing(iV21029),
file('theBenchmark.p',axiom_278) ).
fof(axiom_293,axiom,
cC18xcomp(iV21030),
file('theBenchmark.p',axiom_293) ).
fof(axiom_306,axiom,
cowlThing(iV21030),
file('theBenchmark.p',axiom_306) ).
fof(axiom_331,axiom,
cC12xcomp(iV21035),
file('theBenchmark.p',axiom_331) ).
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)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(f_1_1,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(fof_nnf,[status(thm)],[axiom_0]) ).
fof(f_1_2,plain,
! [U_0] :
( ~ cowlNothing(U_0)
& cowlThing(U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_2] : ~ cowlNothing(U_2)
& ! [U_1] : cowlThing(U_1) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
( ! [U_2] : ~ cowlNothing(U_2)
& ! [U_1] : cowlThing(U_1) ),
inference(definitional_conversion,[status(esa)],[f_1_3]) ).
cnf(f_1_5,plain,
cowlThing(U_1),
inference(clausify,[status(thm)],[f_1_4]) ).
cnf(f_1_6,plain,
~ cowlNothing(U_2),
inference(clausify,[status(thm)],[f_1_4]) ).
fof(f_2_1,plain,
! [X] :
( ( xsd_string(X)
| xsd_integer(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_1]) ).
fof(f_2_2,plain,
! [U_3] :
( ( xsd_string(U_3)
| xsd_integer(U_3) )
& ( ~ xsd_integer(U_3)
| ~ xsd_string(U_3) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_5] :
( xsd_string(U_5)
| xsd_integer(U_5) )
& ! [U_4] :
( ~ xsd_integer(U_4)
| ~ xsd_string(U_4) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
fof(f_2_4,plain,
( ! [U_5] :
( xsd_string(U_5)
| xsd_integer(U_5) )
& ! [U_4] :
( ~ xsd_integer(U_4)
| ~ xsd_string(U_4) ) ),
inference(definitional_conversion,[status(esa)],[f_2_3]) ).
cnf(f_2_5,plain,
( ~ xsd_integer(U_4)
| ~ xsd_string(U_4) ),
inference(clausify,[status(thm)],[f_2_4]) ).
cnf(f_2_6,plain,
( xsd_string(U_5)
| xsd_integer(U_5) ),
inference(clausify,[status(thm)],[f_2_4]) ).
fof(f_3_1,plain,
! [X] :
( ( cC10(X)
| ~ cC4(X)
| ~ cC8(X) )
& ( ( cC4(X)
& cC8(X) )
| ~ cC10(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(f_3_2,plain,
! [U_6] :
( ( cC10(U_6)
| ~ cC4(U_6)
| ~ cC8(U_6) )
& ( ( cC4(U_6)
& cC8(U_6) )
| ~ cC10(U_6) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_8] :
( cC10(U_8)
| ~ cC4(U_8)
| ~ cC8(U_8) )
& ! [U_7] :
( ( cC4(U_7)
& cC8(U_7) )
| ~ cC10(U_7) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_7] :
( cC4(U_7)
| ~ sP0(U_7) )
& ! [U_7] :
( cC8(U_7)
| ~ sP0(U_7) )
& ! [U_8] :
( cC10(U_8)
| ~ cC4(U_8)
| ~ cC8(U_8) )
& ! [U_7] :
( sP0(U_7)
| ~ cC10(U_7) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_3_3]) ).
cnf(f_3_5,plain,
( sP0(U_7)
| ~ cC10(U_7) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_7,plain,
( cC8(U_7)
| ~ sP0(U_7) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_8,plain,
( cC4(U_7)
| ~ sP0(U_7) ),
inference(clausify,[status(thm)],[f_3_4]) ).
fof(f_16_1,plain,
! [X] :
( ( cC110(X)
| ~ cTOP(X)
| ~ cC108(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_15]) ).
fof(f_16_2,plain,
! [U_65] :
( ( cC110(U_65)
| ~ cTOP(U_65)
| ~ cC108(U_65) )
& ( ( cTOP(U_65)
& cC108(U_65) )
| ~ cC110(U_65) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_67] :
( cC110(U_67)
| ~ cTOP(U_67)
| ~ cC108(U_67) )
& ! [U_66] :
( ( cTOP(U_66)
& cC108(U_66) )
| ~ cC110(U_66) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_66] :
( cTOP(U_66)
| ~ sP5(U_66) )
& ! [U_66] :
( cC108(U_66)
| ~ sP5(U_66) )
& ! [U_67] :
( cC110(U_67)
| ~ cTOP(U_67)
| ~ cC108(U_67) )
& ! [U_66] :
( sP5(U_66)
| ~ cC110(U_66) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5])],[f_16_3]) ).
cnf(f_16_5,plain,
( sP5(U_66)
| ~ cC110(U_66) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_7,plain,
( cC108(U_66)
| ~ sP5(U_66) ),
inference(clausify,[status(thm)],[f_16_4]) ).
fof(f_17_1,plain,
! [X] :
( ( cC112(X)
| ~ cC90(X)
| ~ cC110(X) )
& ( ( cC90(X)
& cC110(X) )
| ~ cC112(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(f_17_2,plain,
! [U_68] :
( ( cC112(U_68)
| ~ cC90(U_68)
| ~ cC110(U_68) )
& ( ( cC90(U_68)
& cC110(U_68) )
| ~ cC112(U_68) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_70] :
( cC112(U_70)
| ~ cC90(U_70)
| ~ cC110(U_70) )
& ! [U_69] :
( ( cC90(U_69)
& cC110(U_69) )
| ~ cC112(U_69) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_69] :
( cC90(U_69)
| ~ sP6(U_69) )
& ! [U_69] :
( cC110(U_69)
| ~ sP6(U_69) )
& ! [U_70] :
( cC112(U_70)
| ~ cC90(U_70)
| ~ cC110(U_70) )
& ! [U_69] :
( sP6(U_69)
| ~ cC112(U_69) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP6])],[f_17_3]) ).
cnf(f_17_5,plain,
( sP6(U_69)
| ~ cC112(U_69) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_7,plain,
( cC110(U_69)
| ~ sP6(U_69) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_8,plain,
( cC90(U_69)
| ~ sP6(U_69) ),
inference(clausify,[status(thm)],[f_17_4]) ).
fof(f_19_1,plain,
! [X] :
( ( cC116(X)
| ~ cC112(X)
| ~ cC114(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_18]) ).
fof(f_19_2,plain,
! [U_74] :
( ( cC116(U_74)
| ~ cC112(U_74)
| ~ cC114(U_74) )
& ( ( cC112(U_74)
& cC114(U_74) )
| ~ cC116(U_74) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_76] :
( cC116(U_76)
| ~ cC112(U_76)
| ~ cC114(U_76) )
& ! [U_75] :
( ( cC112(U_75)
& cC114(U_75) )
| ~ cC116(U_75) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
fof(f_19_4,plain,
( ! [U_75] :
( cC112(U_75)
| ~ sP7(U_75) )
& ! [U_75] :
( cC114(U_75)
| ~ sP7(U_75) )
& ! [U_76] :
( cC116(U_76)
| ~ cC112(U_76)
| ~ cC114(U_76) )
& ! [U_75] :
( sP7(U_75)
| ~ cC116(U_75) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP7])],[f_19_3]) ).
cnf(f_19_5,plain,
( sP7(U_75)
| ~ cC116(U_75) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_7,plain,
( cC114(U_75)
| ~ sP7(U_75) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_8,plain,
( cC112(U_75)
| ~ sP7(U_75) ),
inference(clausify,[status(thm)],[f_19_4]) ).
fof(f_41_1,plain,
! [X] :
( ( cC132(X)
| ~ cTOP(X)
| ~ cC130(X) )
& ( ( cTOP(X)
& cC130(X) )
| ~ cC132(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_176] :
( ( cC132(U_176)
| ~ cTOP(U_176)
| ~ cC130(U_176) )
& ( ( cTOP(U_176)
& cC130(U_176) )
| ~ cC132(U_176) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_178] :
( cC132(U_178)
| ~ cTOP(U_178)
| ~ cC130(U_178) )
& ! [U_177] :
( ( cTOP(U_177)
& cC130(U_177) )
| ~ cC132(U_177) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
fof(f_41_4,plain,
( ! [U_177] :
( cTOP(U_177)
| ~ sP15(U_177) )
& ! [U_177] :
( cC130(U_177)
| ~ sP15(U_177) )
& ! [U_178] :
( cC132(U_178)
| ~ cTOP(U_178)
| ~ cC130(U_178) )
& ! [U_177] :
( sP15(U_177)
| ~ cC132(U_177) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP15])],[f_41_3]) ).
cnf(f_41_5,plain,
( sP15(U_177)
| ~ cC132(U_177) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_7,plain,
( cC130(U_177)
| ~ sP15(U_177) ),
inference(clausify,[status(thm)],[f_41_4]) ).
fof(f_42_1,plain,
! [X] :
( ( cC134(X)
| ~ cC132(X)
| ~ cC116(X) )
& ( ( cC132(X)
& cC116(X) )
| ~ cC134(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_41]) ).
fof(f_42_2,plain,
! [U_179] :
( ( cC134(U_179)
| ~ cC132(U_179)
| ~ cC116(U_179) )
& ( ( cC132(U_179)
& cC116(U_179) )
| ~ cC134(U_179) ) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
( ! [U_181] :
( cC134(U_181)
| ~ cC132(U_181)
| ~ cC116(U_181) )
& ! [U_180] :
( ( cC132(U_180)
& cC116(U_180) )
| ~ cC134(U_180) ) ),
inference(miniscope,[status(thm)],[f_42_2]) ).
fof(f_42_4,plain,
( ! [U_180] :
( cC132(U_180)
| ~ sP16(U_180) )
& ! [U_180] :
( cC116(U_180)
| ~ sP16(U_180) )
& ! [U_181] :
( cC134(U_181)
| ~ cC132(U_181)
| ~ cC116(U_181) )
& ! [U_180] :
( sP16(U_180)
| ~ cC134(U_180) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP16])],[f_42_3]) ).
cnf(f_42_5,plain,
( sP16(U_180)
| ~ cC134(U_180) ),
inference(clausify,[status(thm)],[f_42_4]) ).
cnf(f_42_7,plain,
( cC116(U_180)
| ~ sP16(U_180) ),
inference(clausify,[status(thm)],[f_42_4]) ).
cnf(f_42_8,plain,
( cC132(U_180)
| ~ sP16(U_180) ),
inference(clausify,[status(thm)],[f_42_4]) ).
fof(f_44_1,plain,
! [X] :
( ( cC138(X)
| ~ cC134(X)
| ~ cC136(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_185] :
( ( cC138(U_185)
| ~ cC134(U_185)
| ~ cC136(U_185) )
& ( ( cC134(U_185)
& cC136(U_185) )
| ~ cC138(U_185) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_187] :
( cC138(U_187)
| ~ cC134(U_187)
| ~ cC136(U_187) )
& ! [U_186] :
( ( cC134(U_186)
& cC136(U_186) )
| ~ cC138(U_186) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
fof(f_44_4,plain,
( ! [U_186] :
( cC134(U_186)
| ~ sP17(U_186) )
& ! [U_186] :
( cC136(U_186)
| ~ sP17(U_186) )
& ! [U_187] :
( cC138(U_187)
| ~ cC134(U_187)
| ~ cC136(U_187) )
& ! [U_186] :
( sP17(U_186)
| ~ cC138(U_186) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP17])],[f_44_3]) ).
cnf(f_44_5,plain,
( sP17(U_186)
| ~ cC138(U_186) ),
inference(clausify,[status(thm)],[f_44_4]) ).
cnf(f_44_7,plain,
( cC136(U_186)
| ~ sP17(U_186) ),
inference(clausify,[status(thm)],[f_44_4]) ).
cnf(f_44_8,plain,
( cC134(U_186)
| ~ sP17(U_186) ),
inference(clausify,[status(thm)],[f_44_4]) ).
fof(f_65_1,plain,
! [X] :
( ( cC154(X)
| ~ cTOP(X)
| ~ cC152(X) )
& ( ( cTOP(X)
& cC152(X) )
| ~ cC154(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
! [U_282] :
( ( cC154(U_282)
| ~ cTOP(U_282)
| ~ cC152(U_282) )
& ( ( cTOP(U_282)
& cC152(U_282) )
| ~ cC154(U_282) ) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
( ! [U_284] :
( cC154(U_284)
| ~ cTOP(U_284)
| ~ cC152(U_284) )
& ! [U_283] :
( ( cTOP(U_283)
& cC152(U_283) )
| ~ cC154(U_283) ) ),
inference(miniscope,[status(thm)],[f_65_2]) ).
fof(f_65_4,plain,
( ! [U_283] :
( cTOP(U_283)
| ~ sP26(U_283) )
& ! [U_283] :
( cC152(U_283)
| ~ sP26(U_283) )
& ! [U_284] :
( cC154(U_284)
| ~ cTOP(U_284)
| ~ cC152(U_284) )
& ! [U_283] :
( sP26(U_283)
| ~ cC154(U_283) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP26])],[f_65_3]) ).
cnf(f_65_5,plain,
( sP26(U_283)
| ~ cC154(U_283) ),
inference(clausify,[status(thm)],[f_65_4]) ).
cnf(f_65_7,plain,
( cC152(U_283)
| ~ sP26(U_283) ),
inference(clausify,[status(thm)],[f_65_4]) ).
fof(f_66_1,plain,
! [X] :
( ( cC156(X)
| ~ cC138(X)
| ~ cC154(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_285] :
( ( cC156(U_285)
| ~ cC138(U_285)
| ~ cC154(U_285) )
& ( ( cC138(U_285)
& cC154(U_285) )
| ~ cC156(U_285) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_287] :
( cC156(U_287)
| ~ cC138(U_287)
| ~ cC154(U_287) )
& ! [U_286] :
( ( cC138(U_286)
& cC154(U_286) )
| ~ cC156(U_286) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
fof(f_66_4,plain,
( ! [U_286] :
( cC138(U_286)
| ~ sP27(U_286) )
& ! [U_286] :
( cC154(U_286)
| ~ sP27(U_286) )
& ! [U_287] :
( cC156(U_287)
| ~ cC138(U_287)
| ~ cC154(U_287) )
& ! [U_286] :
( sP27(U_286)
| ~ cC156(U_286) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP27])],[f_66_3]) ).
cnf(f_66_5,plain,
( sP27(U_286)
| ~ cC156(U_286) ),
inference(clausify,[status(thm)],[f_66_4]) ).
cnf(f_66_7,plain,
( cC154(U_286)
| ~ sP27(U_286) ),
inference(clausify,[status(thm)],[f_66_4]) ).
cnf(f_66_8,plain,
( cC138(U_286)
| ~ sP27(U_286) ),
inference(clausify,[status(thm)],[f_66_4]) ).
fof(f_67_1,plain,
! [X] :
( ( cC158(X)
| ~ cC156(X)
| ~ cC22(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_66]) ).
fof(f_67_2,plain,
! [U_288] :
( ( cC158(U_288)
| ~ cC156(U_288)
| ~ cC22(U_288) )
& ( ( cC156(U_288)
& cC22(U_288) )
| ~ cC158(U_288) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_290] :
( cC158(U_290)
| ~ cC156(U_290)
| ~ cC22(U_290) )
& ! [U_289] :
( ( cC156(U_289)
& cC22(U_289) )
| ~ cC158(U_289) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
fof(f_67_4,plain,
( ! [U_289] :
( cC156(U_289)
| ~ sP28(U_289) )
& ! [U_289] :
( cC22(U_289)
| ~ sP28(U_289) )
& ! [U_290] :
( cC158(U_290)
| ~ cC156(U_290)
| ~ cC22(U_290) )
& ! [U_289] :
( sP28(U_289)
| ~ cC158(U_289) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP28])],[f_67_3]) ).
cnf(f_67_5,plain,
( sP28(U_289)
| ~ cC158(U_289) ),
inference(clausify,[status(thm)],[f_67_4]) ).
cnf(f_67_7,plain,
( cC22(U_289)
| ~ sP28(U_289) ),
inference(clausify,[status(thm)],[f_67_4]) ).
cnf(f_67_8,plain,
( cC156(U_289)
| ~ sP28(U_289) ),
inference(clausify,[status(thm)],[f_67_4]) ).
fof(f_68_1,plain,
! [X] :
( ( cC16(X)
| ~ cC14(X)
| ~ cC10(X) )
& ( ( cC14(X)
& cC10(X) )
| ~ cC16(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_67]) ).
fof(f_68_2,plain,
! [U_291] :
( ( cC16(U_291)
| ~ cC14(U_291)
| ~ cC10(U_291) )
& ( ( cC14(U_291)
& cC10(U_291) )
| ~ cC16(U_291) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_293] :
( cC16(U_293)
| ~ cC14(U_293)
| ~ cC10(U_293) )
& ! [U_292] :
( ( cC14(U_292)
& cC10(U_292) )
| ~ cC16(U_292) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
fof(f_68_4,plain,
( ! [U_292] :
( cC14(U_292)
| ~ sP29(U_292) )
& ! [U_292] :
( cC10(U_292)
| ~ sP29(U_292) )
& ! [U_293] :
( cC16(U_293)
| ~ cC14(U_293)
| ~ cC10(U_293) )
& ! [U_292] :
( sP29(U_292)
| ~ cC16(U_292) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP29])],[f_68_3]) ).
cnf(f_68_5,plain,
( sP29(U_292)
| ~ cC16(U_292) ),
inference(clausify,[status(thm)],[f_68_4]) ).
cnf(f_68_7,plain,
( cC10(U_292)
| ~ sP29(U_292) ),
inference(clausify,[status(thm)],[f_68_4]) ).
cnf(f_68_8,plain,
( cC14(U_292)
| ~ sP29(U_292) ),
inference(clausify,[status(thm)],[f_68_4]) ).
fof(f_88_1,plain,
! [X] :
( ( cC174(X)
| ~ cC168(X)
| ~ cC172xcomp(X) )
& ( ( cC168(X)
& cC172xcomp(X) )
| ~ cC174(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_87]) ).
fof(f_88_2,plain,
! [U_387] :
( ( cC174(U_387)
| ~ cC168(U_387)
| ~ cC172xcomp(U_387) )
& ( ( cC168(U_387)
& cC172xcomp(U_387) )
| ~ cC174(U_387) ) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
fof(f_88_3,plain,
( ! [U_389] :
( cC174(U_389)
| ~ cC168(U_389)
| ~ cC172xcomp(U_389) )
& ! [U_388] :
( ( cC168(U_388)
& cC172xcomp(U_388) )
| ~ cC174(U_388) ) ),
inference(miniscope,[status(thm)],[f_88_2]) ).
fof(f_88_4,plain,
( ! [U_388] :
( cC168(U_388)
| ~ sP37(U_388) )
& ! [U_388] :
( cC172xcomp(U_388)
| ~ sP37(U_388) )
& ! [U_389] :
( cC174(U_389)
| ~ cC168(U_389)
| ~ cC172xcomp(U_389) )
& ! [U_388] :
( sP37(U_388)
| ~ cC174(U_388) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP37])],[f_88_3]) ).
cnf(f_88_5,plain,
( sP37(U_388)
| ~ cC174(U_388) ),
inference(clausify,[status(thm)],[f_88_4]) ).
cnf(f_88_8,plain,
( cC168(U_388)
| ~ sP37(U_388) ),
inference(clausify,[status(thm)],[f_88_4]) ).
fof(f_97_1,plain,
! [X] :
( ( cC180(X)
| ~ cC178xcomp(X)
| ~ cC174(X) )
& ( ( cC178xcomp(X)
& cC174(X) )
| ~ cC180(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_96]) ).
fof(f_97_2,plain,
! [U_430] :
( ( cC180(U_430)
| ~ cC178xcomp(U_430)
| ~ cC174(U_430) )
& ( ( cC178xcomp(U_430)
& cC174(U_430) )
| ~ cC180(U_430) ) ),
inference(variable_rename,[status(thm)],[f_97_1]) ).
fof(f_97_3,plain,
( ! [U_432] :
( cC180(U_432)
| ~ cC178xcomp(U_432)
| ~ cC174(U_432) )
& ! [U_431] :
( ( cC178xcomp(U_431)
& cC174(U_431) )
| ~ cC180(U_431) ) ),
inference(miniscope,[status(thm)],[f_97_2]) ).
fof(f_97_4,plain,
( ! [U_431] :
( cC178xcomp(U_431)
| ~ sP40(U_431) )
& ! [U_431] :
( cC174(U_431)
| ~ sP40(U_431) )
& ! [U_432] :
( cC180(U_432)
| ~ cC178xcomp(U_432)
| ~ cC174(U_432) )
& ! [U_431] :
( sP40(U_431)
| ~ cC180(U_431) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP40])],[f_97_3]) ).
cnf(f_97_5,plain,
( sP40(U_431)
| ~ cC180(U_431) ),
inference(clausify,[status(thm)],[f_97_4]) ).
cnf(f_97_7,plain,
( cC174(U_431)
| ~ sP40(U_431) ),
inference(clausify,[status(thm)],[f_97_4]) ).
fof(f_101_1,plain,
! [X] :
( ( cC22(X)
| ~ cC16(X)
| ~ cC20(X) )
& ( ( cC16(X)
& cC20(X) )
| ~ cC22(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_100]) ).
fof(f_101_2,plain,
! [U_448] :
( ( cC22(U_448)
| ~ cC16(U_448)
| ~ cC20(U_448) )
& ( ( cC16(U_448)
& cC20(U_448) )
| ~ cC22(U_448) ) ),
inference(variable_rename,[status(thm)],[f_101_1]) ).
fof(f_101_3,plain,
( ! [U_450] :
( cC22(U_450)
| ~ cC16(U_450)
| ~ cC20(U_450) )
& ! [U_449] :
( ( cC16(U_449)
& cC20(U_449) )
| ~ cC22(U_449) ) ),
inference(miniscope,[status(thm)],[f_101_2]) ).
fof(f_101_4,plain,
( ! [U_449] :
( cC16(U_449)
| ~ sP42(U_449) )
& ! [U_449] :
( cC20(U_449)
| ~ sP42(U_449) )
& ! [U_450] :
( cC22(U_450)
| ~ cC16(U_450)
| ~ cC20(U_450) )
& ! [U_449] :
( sP42(U_449)
| ~ cC22(U_449) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP42])],[f_101_3]) ).
cnf(f_101_5,plain,
( sP42(U_449)
| ~ cC22(U_449) ),
inference(clausify,[status(thm)],[f_101_4]) ).
cnf(f_101_6,plain,
( cC22(U_450)
| ~ cC16(U_450)
| ~ cC20(U_450) ),
inference(clausify,[status(thm)],[f_101_4]) ).
cnf(f_101_7,plain,
( cC20(U_449)
| ~ sP42(U_449) ),
inference(clausify,[status(thm)],[f_101_4]) ).
cnf(f_101_8,plain,
( cC16(U_449)
| ~ sP42(U_449) ),
inference(clausify,[status(thm)],[f_101_4]) ).
fof(f_102_1,plain,
! [X] :
( ( cC24(X)
| ! [Y0] : ~ ra_Px5(X,Y0) )
& ( ? [Y0] : ra_Px5(X,Y0)
| ~ cC24(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_101]) ).
fof(f_102_2,plain,
! [U_453] :
( ( cC24(U_453)
| ! [U_452] : ~ ra_Px5(U_453,U_452) )
& ( ? [U_451] : ra_Px5(U_453,U_451)
| ~ cC24(U_453) ) ),
inference(variable_rename,[status(thm)],[f_102_1]) ).
fof(f_102_3,plain,
( ! [U_455] :
( cC24(U_455)
| ! [U_452] : ~ ra_Px5(U_455,U_452) )
& ! [U_454] :
( ? [U_451] : ra_Px5(U_454,U_451)
| ~ cC24(U_454) ) ),
inference(miniscope,[status(thm)],[f_102_2]) ).
fof(f_102_4,plain,
( ! [U_455] :
( cC24(U_455)
| ! [U_452] : ~ ra_Px5(U_455,U_452) )
& ! [U_454] :
( ra_Px5(U_454,sK75(U_454))
| ~ cC24(U_454) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75]),skolemize(U_451,sK75(U_454))],[f_102_3]) ).
fof(f_102_5,plain,
( ! [U_452,U_455] :
( cC24(U_455)
| ~ ra_Px5(U_455,U_452) )
& ! [U_454] :
( ra_Px5(U_454,sK75(U_454))
| ~ cC24(U_454) ) ),
inference(definitional_conversion,[status(esa)],[f_102_4]) ).
cnf(f_102_7,plain,
( cC24(U_455)
| ~ ra_Px5(U_455,U_452) ),
inference(clausify,[status(thm)],[f_102_5]) ).
fof(f_104_1,plain,
! [X] :
( ( cC24xcomp(X)
| ? [Y] : ra_Px5(X,Y) )
& ( ! [Y] : ~ ra_Px5(X,Y)
| ~ cC24xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_103]) ).
fof(f_104_2,plain,
! [U_463] :
( ( cC24xcomp(U_463)
| ? [U_462] : ra_Px5(U_463,U_462) )
& ( ! [U_461] : ~ ra_Px5(U_463,U_461)
| ~ cC24xcomp(U_463) ) ),
inference(variable_rename,[status(thm)],[f_104_1]) ).
fof(f_104_3,plain,
( ! [U_465] :
( cC24xcomp(U_465)
| ? [U_462] : ra_Px5(U_465,U_462) )
& ! [U_464] :
( ! [U_461] : ~ ra_Px5(U_464,U_461)
| ~ cC24xcomp(U_464) ) ),
inference(miniscope,[status(thm)],[f_104_2]) ).
fof(f_104_4,plain,
( ! [U_465] :
( cC24xcomp(U_465)
| ra_Px5(U_465,sK77(U_465)) )
& ! [U_464] :
( ! [U_461] : ~ ra_Px5(U_464,U_461)
| ~ cC24xcomp(U_464) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77]),skolemize(U_462,sK77(U_465))],[f_104_3]) ).
fof(f_104_5,plain,
( ! [U_465] :
( cC24xcomp(U_465)
| ra_Px5(U_465,sK77(U_465)) )
& ! [U_464,U_461] :
( ~ ra_Px5(U_464,U_461)
| ~ cC24xcomp(U_464) ) ),
inference(definitional_conversion,[status(esa)],[f_104_4]) ).
cnf(f_104_7,plain,
( cC24xcomp(U_465)
| ra_Px5(U_465,sK77(U_465)) ),
inference(clausify,[status(thm)],[f_104_5]) ).
fof(f_106_1,plain,
! [X] :
( ( cC26(X)
| ~ cC2xcomp(X)
| ~ cC24xcomp(X) )
& ( ( cC2xcomp(X)
& cC24xcomp(X) )
| ~ cC26(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_105]) ).
fof(f_106_2,plain,
! [U_471] :
( ( cC26(U_471)
| ~ cC2xcomp(U_471)
| ~ cC24xcomp(U_471) )
& ( ( cC2xcomp(U_471)
& cC24xcomp(U_471) )
| ~ cC26(U_471) ) ),
inference(variable_rename,[status(thm)],[f_106_1]) ).
fof(f_106_3,plain,
( ! [U_473] :
( cC26(U_473)
| ~ cC2xcomp(U_473)
| ~ cC24xcomp(U_473) )
& ! [U_472] :
( ( cC2xcomp(U_472)
& cC24xcomp(U_472) )
| ~ cC26(U_472) ) ),
inference(miniscope,[status(thm)],[f_106_2]) ).
fof(f_106_4,plain,
( ! [U_472] :
( cC2xcomp(U_472)
| ~ sP44(U_472) )
& ! [U_472] :
( cC24xcomp(U_472)
| ~ sP44(U_472) )
& ! [U_473] :
( cC26(U_473)
| ~ cC2xcomp(U_473)
| ~ cC24xcomp(U_473) )
& ! [U_472] :
( sP44(U_472)
| ~ cC26(U_472) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP44])],[f_106_3]) ).
cnf(f_106_6,plain,
( cC26(U_473)
| ~ cC2xcomp(U_473)
| ~ cC24xcomp(U_473) ),
inference(clausify,[status(thm)],[f_106_4]) ).
fof(f_108_1,plain,
! [X] :
( ( cC28(X)
| ! [Y] :
( ~ cC26(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC26(Y)
& rR1(X,Y) )
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_107]) ).
fof(f_108_2,plain,
! [U_481] :
( ( cC28(U_481)
| ! [U_480] :
( ~ cC26(U_480)
| ~ rR1(U_481,U_480) ) )
& ( ? [U_479] :
( cC26(U_479)
& rR1(U_481,U_479) )
| ~ cC28(U_481) ) ),
inference(variable_rename,[status(thm)],[f_108_1]) ).
fof(f_108_3,plain,
( ! [U_483] :
( cC28(U_483)
| ! [U_480] :
( ~ cC26(U_480)
| ~ rR1(U_483,U_480) ) )
& ! [U_482] :
( ? [U_479] :
( cC26(U_479)
& rR1(U_482,U_479) )
| ~ cC28(U_482) ) ),
inference(miniscope,[status(thm)],[f_108_2]) ).
fof(f_108_4,plain,
( ! [U_483] :
( cC28(U_483)
| ! [U_480] :
( ~ cC26(U_480)
| ~ rR1(U_483,U_480) ) )
& ! [U_482] :
( ( cC26(sK80(U_482))
& rR1(U_482,sK80(U_482)) )
| ~ cC28(U_482) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK80]),skolemize(U_479,sK80(U_482))],[f_108_3]) ).
fof(f_108_5,plain,
( ! [U_482] :
( cC26(sK80(U_482))
| ~ sP45(U_482) )
& ! [U_482] :
( rR1(U_482,sK80(U_482))
| ~ sP45(U_482) )
& ! [U_480,U_483] :
( cC28(U_483)
| ~ cC26(U_480)
| ~ rR1(U_483,U_480) )
& ! [U_482] :
( sP45(U_482)
| ~ cC28(U_482) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP45])],[f_108_4]) ).
cnf(f_108_7,plain,
( cC28(U_483)
| ~ cC26(U_480)
| ~ rR1(U_483,U_480) ),
inference(clausify,[status(thm)],[f_108_5]) ).
fof(f_109_1,plain,
! [X] :
( ( cC28(X)
| ! [Y0] : ~ ra_Px9(X,Y0) )
& ( ? [Y0] : ra_Px9(X,Y0)
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_108]) ).
fof(f_109_2,plain,
! [U_486] :
( ( cC28(U_486)
| ! [U_485] : ~ ra_Px9(U_486,U_485) )
& ( ? [U_484] : ra_Px9(U_486,U_484)
| ~ cC28(U_486) ) ),
inference(variable_rename,[status(thm)],[f_109_1]) ).
fof(f_109_3,plain,
( ! [U_488] :
( cC28(U_488)
| ! [U_485] : ~ ra_Px9(U_488,U_485) )
& ! [U_487] :
( ? [U_484] : ra_Px9(U_487,U_484)
| ~ cC28(U_487) ) ),
inference(miniscope,[status(thm)],[f_109_2]) ).
fof(f_109_4,plain,
( ! [U_488] :
( cC28(U_488)
| ! [U_485] : ~ ra_Px9(U_488,U_485) )
& ! [U_487] :
( ra_Px9(U_487,sK81(U_487))
| ~ cC28(U_487) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81]),skolemize(U_484,sK81(U_487))],[f_109_3]) ).
fof(f_109_5,plain,
( ! [U_488,U_485] :
( cC28(U_488)
| ~ ra_Px9(U_488,U_485) )
& ! [U_487] :
( ra_Px9(U_487,sK81(U_487))
| ~ cC28(U_487) ) ),
inference(definitional_conversion,[status(esa)],[f_109_4]) ).
cnf(f_109_6,plain,
( ra_Px9(U_487,sK81(U_487))
| ~ cC28(U_487) ),
inference(clausify,[status(thm)],[f_109_5]) ).
fof(f_110_1,plain,
! [X] :
( ( cC28xcomp(X)
| ? [Y] : ra_Px9(X,Y) )
& ( ! [Y] : ~ ra_Px9(X,Y)
| ~ cC28xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_109]) ).
fof(f_110_2,plain,
! [U_491] :
( ( cC28xcomp(U_491)
| ? [U_490] : ra_Px9(U_491,U_490) )
& ( ! [U_489] : ~ ra_Px9(U_491,U_489)
| ~ cC28xcomp(U_491) ) ),
inference(variable_rename,[status(thm)],[f_110_1]) ).
fof(f_110_3,plain,
( ! [U_493] :
( cC28xcomp(U_493)
| ? [U_490] : ra_Px9(U_493,U_490) )
& ! [U_492] :
( ! [U_489] : ~ ra_Px9(U_492,U_489)
| ~ cC28xcomp(U_492) ) ),
inference(miniscope,[status(thm)],[f_110_2]) ).
fof(f_110_4,plain,
( ! [U_493] :
( cC28xcomp(U_493)
| ra_Px9(U_493,sK82(U_493)) )
& ! [U_492] :
( ! [U_489] : ~ ra_Px9(U_492,U_489)
| ~ cC28xcomp(U_492) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK82]),skolemize(U_490,sK82(U_493))],[f_110_3]) ).
fof(f_110_5,plain,
( ! [U_493] :
( cC28xcomp(U_493)
| ra_Px9(U_493,sK82(U_493)) )
& ! [U_489,U_492] :
( ~ ra_Px9(U_492,U_489)
| ~ cC28xcomp(U_492) ) ),
inference(definitional_conversion,[status(esa)],[f_110_4]) ).
cnf(f_110_6,plain,
( ~ ra_Px9(U_492,U_489)
| ~ cC28xcomp(U_492) ),
inference(clausify,[status(thm)],[f_110_5]) ).
fof(f_112_1,plain,
! [X] :
( ( cC30(X)
| ! [Y] :
( ~ cC12xcomp(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) )
| ~ cC30(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_111]) ).
fof(f_112_2,plain,
! [U_501] :
( ( cC30(U_501)
| ! [U_500] :
( ~ cC12xcomp(U_500)
| ~ rR1(U_501,U_500) ) )
& ( ? [U_499] :
( cC12xcomp(U_499)
& rR1(U_501,U_499) )
| ~ cC30(U_501) ) ),
inference(variable_rename,[status(thm)],[f_112_1]) ).
fof(f_112_3,plain,
( ! [U_503] :
( cC30(U_503)
| ! [U_500] :
( ~ cC12xcomp(U_500)
| ~ rR1(U_503,U_500) ) )
& ! [U_502] :
( ? [U_499] :
( cC12xcomp(U_499)
& rR1(U_502,U_499) )
| ~ cC30(U_502) ) ),
inference(miniscope,[status(thm)],[f_112_2]) ).
fof(f_112_4,plain,
( ! [U_503] :
( cC30(U_503)
| ! [U_500] :
( ~ cC12xcomp(U_500)
| ~ rR1(U_503,U_500) ) )
& ! [U_502] :
( ( cC12xcomp(sK84(U_502))
& rR1(U_502,sK84(U_502)) )
| ~ cC30(U_502) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84]),skolemize(U_499,sK84(U_502))],[f_112_3]) ).
fof(f_112_5,plain,
( ! [U_502] :
( cC12xcomp(sK84(U_502))
| ~ sP46(U_502) )
& ! [U_502] :
( rR1(U_502,sK84(U_502))
| ~ sP46(U_502) )
& ! [U_500,U_503] :
( cC30(U_503)
| ~ cC12xcomp(U_500)
| ~ rR1(U_503,U_500) )
& ! [U_502] :
( sP46(U_502)
| ~ cC30(U_502) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP46])],[f_112_4]) ).
cnf(f_112_7,plain,
( cC30(U_503)
| ~ cC12xcomp(U_500)
| ~ rR1(U_503,U_500) ),
inference(clausify,[status(thm)],[f_112_5]) ).
fof(f_120_1,plain,
! [X] :
( ( cC36(X)
| ~ cC28xcomp(X)
| ~ cC34xcomp(X) )
& ( ( cC28xcomp(X)
& cC34xcomp(X) )
| ~ cC36(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_119]) ).
fof(f_120_2,plain,
! [U_537] :
( ( cC36(U_537)
| ~ cC28xcomp(U_537)
| ~ cC34xcomp(U_537) )
& ( ( cC28xcomp(U_537)
& cC34xcomp(U_537) )
| ~ cC36(U_537) ) ),
inference(variable_rename,[status(thm)],[f_120_1]) ).
fof(f_120_3,plain,
( ! [U_539] :
( cC36(U_539)
| ~ cC28xcomp(U_539)
| ~ cC34xcomp(U_539) )
& ! [U_538] :
( ( cC28xcomp(U_538)
& cC34xcomp(U_538) )
| ~ cC36(U_538) ) ),
inference(miniscope,[status(thm)],[f_120_2]) ).
fof(f_120_4,plain,
( ! [U_538] :
( cC28xcomp(U_538)
| ~ sP49(U_538) )
& ! [U_538] :
( cC34xcomp(U_538)
| ~ sP49(U_538) )
& ! [U_539] :
( cC36(U_539)
| ~ cC28xcomp(U_539)
| ~ cC34xcomp(U_539) )
& ! [U_538] :
( sP49(U_538)
| ~ cC36(U_538) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP49])],[f_120_3]) ).
cnf(f_120_6,plain,
( cC36(U_539)
| ~ cC28xcomp(U_539)
| ~ cC34xcomp(U_539) ),
inference(clausify,[status(thm)],[f_120_4]) ).
fof(f_121_1,plain,
! [X] :
( ( cC38(X)
| ~ cTOP(X)
| ~ cC36(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_120]) ).
fof(f_121_2,plain,
! [U_540] :
( ( cC38(U_540)
| ~ cTOP(U_540)
| ~ cC36(U_540) )
& ( ( cTOP(U_540)
& cC36(U_540) )
| ~ cC38(U_540) ) ),
inference(variable_rename,[status(thm)],[f_121_1]) ).
fof(f_121_3,plain,
( ! [U_542] :
( cC38(U_542)
| ~ cTOP(U_542)
| ~ cC36(U_542) )
& ! [U_541] :
( ( cTOP(U_541)
& cC36(U_541) )
| ~ cC38(U_541) ) ),
inference(miniscope,[status(thm)],[f_121_2]) ).
fof(f_121_4,plain,
( ! [U_541] :
( cTOP(U_541)
| ~ sP50(U_541) )
& ! [U_541] :
( cC36(U_541)
| ~ sP50(U_541) )
& ! [U_542] :
( cC38(U_542)
| ~ cTOP(U_542)
| ~ cC36(U_542) )
& ! [U_541] :
( sP50(U_541)
| ~ cC38(U_541) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP50])],[f_121_3]) ).
cnf(f_121_5,plain,
( sP50(U_541)
| ~ cC38(U_541) ),
inference(clausify,[status(thm)],[f_121_4]) ).
cnf(f_121_6,plain,
( cC38(U_542)
| ~ cTOP(U_542)
| ~ cC36(U_542) ),
inference(clausify,[status(thm)],[f_121_4]) ).
cnf(f_121_7,plain,
( cC36(U_541)
| ~ sP50(U_541) ),
inference(clausify,[status(thm)],[f_121_4]) ).
fof(f_123_1,plain,
! [X] :
( ( cC40(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_122]) ).
fof(f_123_2,plain,
! [U_548] :
( ( cC40(U_548)
| ~ cTOP(U_548) )
& ( cTOP(U_548)
| ~ cC40(U_548) ) ),
inference(variable_rename,[status(thm)],[f_123_1]) ).
fof(f_123_3,plain,
( ! [U_550] :
( cC40(U_550)
| ~ cTOP(U_550) )
& ! [U_549] :
( cTOP(U_549)
| ~ cC40(U_549) ) ),
inference(miniscope,[status(thm)],[f_123_2]) ).
fof(f_123_4,plain,
( ! [U_550] :
( cC40(U_550)
| ~ cTOP(U_550) )
& ! [U_549] :
( cTOP(U_549)
| ~ cC40(U_549) ) ),
inference(definitional_conversion,[status(esa)],[f_123_3]) ).
cnf(f_123_6,plain,
( cC40(U_550)
| ~ cTOP(U_550) ),
inference(clausify,[status(thm)],[f_123_4]) ).
fof(f_124_1,plain,
! [X] :
( ( cC42(X)
| ~ cC38(X)
| ~ cC40(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_123]) ).
fof(f_124_2,plain,
! [U_551] :
( ( cC42(U_551)
| ~ cC38(U_551)
| ~ cC40(U_551) )
& ( ( cC38(U_551)
& cC40(U_551) )
| ~ cC42(U_551) ) ),
inference(variable_rename,[status(thm)],[f_124_1]) ).
fof(f_124_3,plain,
( ! [U_553] :
( cC42(U_553)
| ~ cC38(U_553)
| ~ cC40(U_553) )
& ! [U_552] :
( ( cC38(U_552)
& cC40(U_552) )
| ~ cC42(U_552) ) ),
inference(miniscope,[status(thm)],[f_124_2]) ).
fof(f_124_4,plain,
( ! [U_552] :
( cC38(U_552)
| ~ sP52(U_552) )
& ! [U_552] :
( cC40(U_552)
| ~ sP52(U_552) )
& ! [U_553] :
( cC42(U_553)
| ~ cC38(U_553)
| ~ cC40(U_553) )
& ! [U_552] :
( sP52(U_552)
| ~ cC42(U_552) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP52])],[f_124_3]) ).
cnf(f_124_5,plain,
( sP52(U_552)
| ~ cC42(U_552) ),
inference(clausify,[status(thm)],[f_124_4]) ).
cnf(f_124_6,plain,
( cC42(U_553)
| ~ cC38(U_553)
| ~ cC40(U_553) ),
inference(clausify,[status(thm)],[f_124_4]) ).
cnf(f_124_7,plain,
( cC40(U_552)
| ~ sP52(U_552) ),
inference(clausify,[status(thm)],[f_124_4]) ).
cnf(f_124_8,plain,
( cC38(U_552)
| ~ sP52(U_552) ),
inference(clausify,[status(thm)],[f_124_4]) ).
fof(f_125_1,plain,
! [X] :
( ( cC44(X)
| ? [Y] : ra_Px13(X,Y) )
& ( ! [Y] : ~ ra_Px13(X,Y)
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_124]) ).
fof(f_125_2,plain,
! [U_556] :
( ( cC44(U_556)
| ? [U_555] : ra_Px13(U_556,U_555) )
& ( ! [U_554] : ~ ra_Px13(U_556,U_554)
| ~ cC44(U_556) ) ),
inference(variable_rename,[status(thm)],[f_125_1]) ).
fof(f_125_3,plain,
( ! [U_558] :
( cC44(U_558)
| ? [U_555] : ra_Px13(U_558,U_555) )
& ! [U_557] :
( ! [U_554] : ~ ra_Px13(U_557,U_554)
| ~ cC44(U_557) ) ),
inference(miniscope,[status(thm)],[f_125_2]) ).
fof(f_125_4,plain,
( ! [U_558] :
( cC44(U_558)
| ra_Px13(U_558,sK92(U_558)) )
& ! [U_557] :
( ! [U_554] : ~ ra_Px13(U_557,U_554)
| ~ cC44(U_557) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92]),skolemize(U_555,sK92(U_558))],[f_125_3]) ).
fof(f_125_5,plain,
( ! [U_558] :
( cC44(U_558)
| ra_Px13(U_558,sK92(U_558)) )
& ! [U_554,U_557] :
( ~ ra_Px13(U_557,U_554)
| ~ cC44(U_557) ) ),
inference(definitional_conversion,[status(esa)],[f_125_4]) ).
cnf(f_125_7,plain,
( cC44(U_558)
| ra_Px13(U_558,sK92(U_558)) ),
inference(clausify,[status(thm)],[f_125_5]) ).
fof(f_127_1,plain,
! [X] :
( ( cC44xcomp(X)
| ! [Y0] : ~ ra_Px13(X,Y0) )
& ( ? [Y0] : ra_Px13(X,Y0)
| ~ cC44xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_126]) ).
fof(f_127_2,plain,
! [U_566] :
( ( cC44xcomp(U_566)
| ! [U_565] : ~ ra_Px13(U_566,U_565) )
& ( ? [U_564] : ra_Px13(U_566,U_564)
| ~ cC44xcomp(U_566) ) ),
inference(variable_rename,[status(thm)],[f_127_1]) ).
fof(f_127_3,plain,
( ! [U_568] :
( cC44xcomp(U_568)
| ! [U_565] : ~ ra_Px13(U_568,U_565) )
& ! [U_567] :
( ? [U_564] : ra_Px13(U_567,U_564)
| ~ cC44xcomp(U_567) ) ),
inference(miniscope,[status(thm)],[f_127_2]) ).
fof(f_127_4,plain,
( ! [U_568] :
( cC44xcomp(U_568)
| ! [U_565] : ~ ra_Px13(U_568,U_565) )
& ! [U_567] :
( ra_Px13(U_567,sK94(U_567))
| ~ cC44xcomp(U_567) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94]),skolemize(U_564,sK94(U_567))],[f_127_3]) ).
fof(f_127_5,plain,
( ! [U_568,U_565] :
( cC44xcomp(U_568)
| ~ ra_Px13(U_568,U_565) )
& ! [U_567] :
( ra_Px13(U_567,sK94(U_567))
| ~ cC44xcomp(U_567) ) ),
inference(definitional_conversion,[status(esa)],[f_127_4]) ).
cnf(f_127_7,plain,
( cC44xcomp(U_568)
| ~ ra_Px13(U_568,U_565) ),
inference(clausify,[status(thm)],[f_127_5]) ).
fof(f_128_1,plain,
! [X] :
( ( cC46(X)
| ! [Y0] : ~ ra_Px90(X,Y0) )
& ( ? [Y0] : ra_Px90(X,Y0)
| ~ cC46(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_127]) ).
fof(f_128_2,plain,
! [U_571] :
( ( cC46(U_571)
| ! [U_570] : ~ ra_Px90(U_571,U_570) )
& ( ? [U_569] : ra_Px90(U_571,U_569)
| ~ cC46(U_571) ) ),
inference(variable_rename,[status(thm)],[f_128_1]) ).
fof(f_128_3,plain,
( ! [U_573] :
( cC46(U_573)
| ! [U_570] : ~ ra_Px90(U_573,U_570) )
& ! [U_572] :
( ? [U_569] : ra_Px90(U_572,U_569)
| ~ cC46(U_572) ) ),
inference(miniscope,[status(thm)],[f_128_2]) ).
fof(f_128_4,plain,
( ! [U_573] :
( cC46(U_573)
| ! [U_570] : ~ ra_Px90(U_573,U_570) )
& ! [U_572] :
( ra_Px90(U_572,sK95(U_572))
| ~ cC46(U_572) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95]),skolemize(U_569,sK95(U_572))],[f_128_3]) ).
fof(f_128_5,plain,
( ! [U_573,U_570] :
( cC46(U_573)
| ~ ra_Px90(U_573,U_570) )
& ! [U_572] :
( ra_Px90(U_572,sK95(U_572))
| ~ cC46(U_572) ) ),
inference(definitional_conversion,[status(esa)],[f_128_4]) ).
cnf(f_128_6,plain,
( ra_Px90(U_572,sK95(U_572))
| ~ cC46(U_572) ),
inference(clausify,[status(thm)],[f_128_5]) ).
fof(f_129_1,plain,
! [X] :
( ( cC46(X)
| ~ cC12xcomp(X)
| ~ cC44xcomp(X) )
& ( ( cC12xcomp(X)
& cC44xcomp(X) )
| ~ cC46(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_128]) ).
fof(f_129_2,plain,
! [U_574] :
( ( cC46(U_574)
| ~ cC12xcomp(U_574)
| ~ cC44xcomp(U_574) )
& ( ( cC12xcomp(U_574)
& cC44xcomp(U_574) )
| ~ cC46(U_574) ) ),
inference(variable_rename,[status(thm)],[f_129_1]) ).
fof(f_129_3,plain,
( ! [U_576] :
( cC46(U_576)
| ~ cC12xcomp(U_576)
| ~ cC44xcomp(U_576) )
& ! [U_575] :
( ( cC12xcomp(U_575)
& cC44xcomp(U_575) )
| ~ cC46(U_575) ) ),
inference(miniscope,[status(thm)],[f_129_2]) ).
fof(f_129_4,plain,
( ! [U_575] :
( cC12xcomp(U_575)
| ~ sP54(U_575) )
& ! [U_575] :
( cC44xcomp(U_575)
| ~ sP54(U_575) )
& ! [U_576] :
( cC46(U_576)
| ~ cC12xcomp(U_576)
| ~ cC44xcomp(U_576) )
& ! [U_575] :
( sP54(U_575)
| ~ cC46(U_575) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP54])],[f_129_3]) ).
cnf(f_129_6,plain,
( cC46(U_576)
| ~ cC12xcomp(U_576)
| ~ cC44xcomp(U_576) ),
inference(clausify,[status(thm)],[f_129_4]) ).
fof(f_130_1,plain,
! [X] :
( ( cC46xcomp(X)
| ? [Y] : ra_Px90(X,Y) )
& ( ! [Y] : ~ ra_Px90(X,Y)
| ~ cC46xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_129]) ).
fof(f_130_2,plain,
! [U_579] :
( ( cC46xcomp(U_579)
| ? [U_578] : ra_Px90(U_579,U_578) )
& ( ! [U_577] : ~ ra_Px90(U_579,U_577)
| ~ cC46xcomp(U_579) ) ),
inference(variable_rename,[status(thm)],[f_130_1]) ).
fof(f_130_3,plain,
( ! [U_581] :
( cC46xcomp(U_581)
| ? [U_578] : ra_Px90(U_581,U_578) )
& ! [U_580] :
( ! [U_577] : ~ ra_Px90(U_580,U_577)
| ~ cC46xcomp(U_580) ) ),
inference(miniscope,[status(thm)],[f_130_2]) ).
fof(f_130_4,plain,
( ! [U_581] :
( cC46xcomp(U_581)
| ra_Px90(U_581,sK96(U_581)) )
& ! [U_580] :
( ! [U_577] : ~ ra_Px90(U_580,U_577)
| ~ cC46xcomp(U_580) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96]),skolemize(U_578,sK96(U_581))],[f_130_3]) ).
fof(f_130_5,plain,
( ! [U_581] :
( cC46xcomp(U_581)
| ra_Px90(U_581,sK96(U_581)) )
& ! [U_580,U_577] :
( ~ ra_Px90(U_580,U_577)
| ~ cC46xcomp(U_580) ) ),
inference(definitional_conversion,[status(esa)],[f_130_4]) ).
cnf(f_130_6,plain,
( ~ ra_Px90(U_580,U_577)
| ~ cC46xcomp(U_580) ),
inference(clausify,[status(thm)],[f_130_5]) ).
fof(f_132_1,plain,
! [X] :
( ( cC48(X)
| ! [Y] :
( ~ cC46(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC46(Y)
& rR1(X,Y) )
| ~ cC48(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_131]) ).
fof(f_132_2,plain,
! [U_589] :
( ( cC48(U_589)
| ! [U_588] :
( ~ cC46(U_588)
| ~ rR1(U_589,U_588) ) )
& ( ? [U_587] :
( cC46(U_587)
& rR1(U_589,U_587) )
| ~ cC48(U_589) ) ),
inference(variable_rename,[status(thm)],[f_132_1]) ).
fof(f_132_3,plain,
( ! [U_591] :
( cC48(U_591)
| ! [U_588] :
( ~ cC46(U_588)
| ~ rR1(U_591,U_588) ) )
& ! [U_590] :
( ? [U_587] :
( cC46(U_587)
& rR1(U_590,U_587) )
| ~ cC48(U_590) ) ),
inference(miniscope,[status(thm)],[f_132_2]) ).
fof(f_132_4,plain,
( ! [U_591] :
( cC48(U_591)
| ! [U_588] :
( ~ cC46(U_588)
| ~ rR1(U_591,U_588) ) )
& ! [U_590] :
( ( cC46(sK98(U_590))
& rR1(U_590,sK98(U_590)) )
| ~ cC48(U_590) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK98]),skolemize(U_587,sK98(U_590))],[f_132_3]) ).
fof(f_132_5,plain,
( ! [U_590] :
( cC46(sK98(U_590))
| ~ sP55(U_590) )
& ! [U_590] :
( rR1(U_590,sK98(U_590))
| ~ sP55(U_590) )
& ! [U_588,U_591] :
( cC48(U_591)
| ~ cC46(U_588)
| ~ rR1(U_591,U_588) )
& ! [U_590] :
( sP55(U_590)
| ~ cC48(U_590) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP55])],[f_132_4]) ).
cnf(f_132_6,plain,
( sP55(U_590)
| ~ cC48(U_590) ),
inference(clausify,[status(thm)],[f_132_5]) ).
cnf(f_132_7,plain,
( cC48(U_591)
| ~ cC46(U_588)
| ~ rR1(U_591,U_588) ),
inference(clausify,[status(thm)],[f_132_5]) ).
cnf(f_132_8,plain,
( rR1(U_590,sK98(U_590))
| ~ sP55(U_590) ),
inference(clausify,[status(thm)],[f_132_5]) ).
cnf(f_132_9,plain,
( cC46(sK98(U_590))
| ~ sP55(U_590) ),
inference(clausify,[status(thm)],[f_132_5]) ).
fof(f_135_1,plain,
! [X] :
( ( cC50(X)
| ? [Y] : ra_Px16(X,Y) )
& ( ! [Y] : ~ ra_Px16(X,Y)
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_134]) ).
fof(f_135_2,plain,
! [U_604] :
( ( cC50(U_604)
| ? [U_603] : ra_Px16(U_604,U_603) )
& ( ! [U_602] : ~ ra_Px16(U_604,U_602)
| ~ cC50(U_604) ) ),
inference(variable_rename,[status(thm)],[f_135_1]) ).
fof(f_135_3,plain,
( ! [U_606] :
( cC50(U_606)
| ? [U_603] : ra_Px16(U_606,U_603) )
& ! [U_605] :
( ! [U_602] : ~ ra_Px16(U_605,U_602)
| ~ cC50(U_605) ) ),
inference(miniscope,[status(thm)],[f_135_2]) ).
fof(f_135_4,plain,
( ! [U_606] :
( cC50(U_606)
| ra_Px16(U_606,sK101(U_606)) )
& ! [U_605] :
( ! [U_602] : ~ ra_Px16(U_605,U_602)
| ~ cC50(U_605) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK101]),skolemize(U_603,sK101(U_606))],[f_135_3]) ).
fof(f_135_5,plain,
( ! [U_606] :
( cC50(U_606)
| ra_Px16(U_606,sK101(U_606)) )
& ! [U_605,U_602] :
( ~ ra_Px16(U_605,U_602)
| ~ cC50(U_605) ) ),
inference(definitional_conversion,[status(esa)],[f_135_4]) ).
cnf(f_135_7,plain,
( cC50(U_606)
| ra_Px16(U_606,sK101(U_606)) ),
inference(clausify,[status(thm)],[f_135_5]) ).
fof(f_136_1,plain,
! [X] :
( ( cC50xcomp(X)
| ! [Y0] : ~ ra_Px16(X,Y0) )
& ( ? [Y0] : ra_Px16(X,Y0)
| ~ cC50xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_135]) ).
fof(f_136_2,plain,
! [U_609] :
( ( cC50xcomp(U_609)
| ! [U_608] : ~ ra_Px16(U_609,U_608) )
& ( ? [U_607] : ra_Px16(U_609,U_607)
| ~ cC50xcomp(U_609) ) ),
inference(variable_rename,[status(thm)],[f_136_1]) ).
fof(f_136_3,plain,
( ! [U_611] :
( cC50xcomp(U_611)
| ! [U_608] : ~ ra_Px16(U_611,U_608) )
& ! [U_610] :
( ? [U_607] : ra_Px16(U_610,U_607)
| ~ cC50xcomp(U_610) ) ),
inference(miniscope,[status(thm)],[f_136_2]) ).
fof(f_136_4,plain,
( ! [U_611] :
( cC50xcomp(U_611)
| ! [U_608] : ~ ra_Px16(U_611,U_608) )
& ! [U_610] :
( ra_Px16(U_610,sK102(U_610))
| ~ cC50xcomp(U_610) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK102]),skolemize(U_607,sK102(U_610))],[f_136_3]) ).
fof(f_136_5,plain,
( ! [U_608,U_611] :
( cC50xcomp(U_611)
| ~ ra_Px16(U_611,U_608) )
& ! [U_610] :
( ra_Px16(U_610,sK102(U_610))
| ~ cC50xcomp(U_610) ) ),
inference(definitional_conversion,[status(esa)],[f_136_4]) ).
cnf(f_136_7,plain,
( cC50xcomp(U_611)
| ~ ra_Px16(U_611,U_608) ),
inference(clausify,[status(thm)],[f_136_5]) ).
fof(f_138_1,plain,
! [X] :
( ( cC52(X)
| ~ cC12xcomp(X)
| ~ cC50xcomp(X) )
& ( ( cC12xcomp(X)
& cC50xcomp(X) )
| ~ cC52(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_137]) ).
fof(f_138_2,plain,
! [U_617] :
( ( cC52(U_617)
| ~ cC12xcomp(U_617)
| ~ cC50xcomp(U_617) )
& ( ( cC12xcomp(U_617)
& cC50xcomp(U_617) )
| ~ cC52(U_617) ) ),
inference(variable_rename,[status(thm)],[f_138_1]) ).
fof(f_138_3,plain,
( ! [U_619] :
( cC52(U_619)
| ~ cC12xcomp(U_619)
| ~ cC50xcomp(U_619) )
& ! [U_618] :
( ( cC12xcomp(U_618)
& cC50xcomp(U_618) )
| ~ cC52(U_618) ) ),
inference(miniscope,[status(thm)],[f_138_2]) ).
fof(f_138_4,plain,
( ! [U_618] :
( cC12xcomp(U_618)
| ~ sP57(U_618) )
& ! [U_618] :
( cC50xcomp(U_618)
| ~ sP57(U_618) )
& ! [U_619] :
( cC52(U_619)
| ~ cC12xcomp(U_619)
| ~ cC50xcomp(U_619) )
& ! [U_618] :
( sP57(U_618)
| ~ cC52(U_618) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP57])],[f_138_3]) ).
cnf(f_138_6,plain,
( cC52(U_619)
| ~ cC12xcomp(U_619)
| ~ cC50xcomp(U_619) ),
inference(clausify,[status(thm)],[f_138_4]) ).
fof(f_140_1,plain,
! [X] :
( ( cC54(X)
| ! [Y] :
( ~ cC52(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC52(Y)
& rR1(X,Y) )
| ~ cC54(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_139]) ).
fof(f_140_2,plain,
! [U_627] :
( ( cC54(U_627)
| ! [U_626] :
( ~ cC52(U_626)
| ~ rR1(U_627,U_626) ) )
& ( ? [U_625] :
( cC52(U_625)
& rR1(U_627,U_625) )
| ~ cC54(U_627) ) ),
inference(variable_rename,[status(thm)],[f_140_1]) ).
fof(f_140_3,plain,
( ! [U_629] :
( cC54(U_629)
| ! [U_626] :
( ~ cC52(U_626)
| ~ rR1(U_629,U_626) ) )
& ! [U_628] :
( ? [U_625] :
( cC52(U_625)
& rR1(U_628,U_625) )
| ~ cC54(U_628) ) ),
inference(miniscope,[status(thm)],[f_140_2]) ).
fof(f_140_4,plain,
( ! [U_629] :
( cC54(U_629)
| ! [U_626] :
( ~ cC52(U_626)
| ~ rR1(U_629,U_626) ) )
& ! [U_628] :
( ( cC52(sK105(U_628))
& rR1(U_628,sK105(U_628)) )
| ~ cC54(U_628) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK105]),skolemize(U_625,sK105(U_628))],[f_140_3]) ).
fof(f_140_5,plain,
( ! [U_628] :
( cC52(sK105(U_628))
| ~ sP58(U_628) )
& ! [U_628] :
( rR1(U_628,sK105(U_628))
| ~ sP58(U_628) )
& ! [U_626,U_629] :
( cC54(U_629)
| ~ cC52(U_626)
| ~ rR1(U_629,U_626) )
& ! [U_628] :
( sP58(U_628)
| ~ cC54(U_628) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP58])],[f_140_4]) ).
cnf(f_140_7,plain,
( cC54(U_629)
| ~ cC52(U_626)
| ~ rR1(U_629,U_626) ),
inference(clausify,[status(thm)],[f_140_5]) ).
fof(f_141_1,plain,
! [X] :
( ( cC54(X)
| ! [Y0] : ~ ra_Px18(X,Y0) )
& ( ? [Y0] : ra_Px18(X,Y0)
| ~ cC54(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_140]) ).
fof(f_141_2,plain,
! [U_632] :
( ( cC54(U_632)
| ! [U_631] : ~ ra_Px18(U_632,U_631) )
& ( ? [U_630] : ra_Px18(U_632,U_630)
| ~ cC54(U_632) ) ),
inference(variable_rename,[status(thm)],[f_141_1]) ).
fof(f_141_3,plain,
( ! [U_634] :
( cC54(U_634)
| ! [U_631] : ~ ra_Px18(U_634,U_631) )
& ! [U_633] :
( ? [U_630] : ra_Px18(U_633,U_630)
| ~ cC54(U_633) ) ),
inference(miniscope,[status(thm)],[f_141_2]) ).
fof(f_141_4,plain,
( ! [U_634] :
( cC54(U_634)
| ! [U_631] : ~ ra_Px18(U_634,U_631) )
& ! [U_633] :
( ra_Px18(U_633,sK106(U_633))
| ~ cC54(U_633) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK106]),skolemize(U_630,sK106(U_633))],[f_141_3]) ).
fof(f_141_5,plain,
( ! [U_634,U_631] :
( cC54(U_634)
| ~ ra_Px18(U_634,U_631) )
& ! [U_633] :
( ra_Px18(U_633,sK106(U_633))
| ~ cC54(U_633) ) ),
inference(definitional_conversion,[status(esa)],[f_141_4]) ).
cnf(f_141_6,plain,
( ra_Px18(U_633,sK106(U_633))
| ~ cC54(U_633) ),
inference(clausify,[status(thm)],[f_141_5]) ).
fof(f_142_1,plain,
! [X] :
( ( cC54xcomp(X)
| ? [Y] : ra_Px18(X,Y) )
& ( ! [Y] : ~ ra_Px18(X,Y)
| ~ cC54xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_141]) ).
fof(f_142_2,plain,
! [U_637] :
( ( cC54xcomp(U_637)
| ? [U_636] : ra_Px18(U_637,U_636) )
& ( ! [U_635] : ~ ra_Px18(U_637,U_635)
| ~ cC54xcomp(U_637) ) ),
inference(variable_rename,[status(thm)],[f_142_1]) ).
fof(f_142_3,plain,
( ! [U_639] :
( cC54xcomp(U_639)
| ? [U_636] : ra_Px18(U_639,U_636) )
& ! [U_638] :
( ! [U_635] : ~ ra_Px18(U_638,U_635)
| ~ cC54xcomp(U_638) ) ),
inference(miniscope,[status(thm)],[f_142_2]) ).
fof(f_142_4,plain,
( ! [U_639] :
( cC54xcomp(U_639)
| ra_Px18(U_639,sK107(U_639)) )
& ! [U_638] :
( ! [U_635] : ~ ra_Px18(U_638,U_635)
| ~ cC54xcomp(U_638) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107]),skolemize(U_636,sK107(U_639))],[f_142_3]) ).
fof(f_142_5,plain,
( ! [U_639] :
( cC54xcomp(U_639)
| ra_Px18(U_639,sK107(U_639)) )
& ! [U_635,U_638] :
( ~ ra_Px18(U_638,U_635)
| ~ cC54xcomp(U_638) ) ),
inference(definitional_conversion,[status(esa)],[f_142_4]) ).
cnf(f_142_6,plain,
( ~ ra_Px18(U_638,U_635)
| ~ cC54xcomp(U_638) ),
inference(clausify,[status(thm)],[f_142_5]) ).
fof(f_143_1,plain,
! [X] :
( ( cC56(X)
| ~ cC54xcomp(X)
| ~ cC48xcomp(X) )
& ( ( cC54xcomp(X)
& cC48xcomp(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_142]) ).
fof(f_143_2,plain,
! [U_640] :
( ( cC56(U_640)
| ~ cC54xcomp(U_640)
| ~ cC48xcomp(U_640) )
& ( ( cC54xcomp(U_640)
& cC48xcomp(U_640) )
| ~ cC56(U_640) ) ),
inference(variable_rename,[status(thm)],[f_143_1]) ).
fof(f_143_3,plain,
( ! [U_642] :
( cC56(U_642)
| ~ cC54xcomp(U_642)
| ~ cC48xcomp(U_642) )
& ! [U_641] :
( ( cC54xcomp(U_641)
& cC48xcomp(U_641) )
| ~ cC56(U_641) ) ),
inference(miniscope,[status(thm)],[f_143_2]) ).
fof(f_143_4,plain,
( ! [U_641] :
( cC54xcomp(U_641)
| ~ sP59(U_641) )
& ! [U_641] :
( cC48xcomp(U_641)
| ~ sP59(U_641) )
& ! [U_642] :
( cC56(U_642)
| ~ cC54xcomp(U_642)
| ~ cC48xcomp(U_642) )
& ! [U_641] :
( sP59(U_641)
| ~ cC56(U_641) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP59])],[f_143_3]) ).
cnf(f_143_6,plain,
( cC56(U_642)
| ~ cC54xcomp(U_642)
| ~ cC48xcomp(U_642) ),
inference(clausify,[status(thm)],[f_143_4]) ).
fof(f_144_1,plain,
! [X] :
( ( cC58(X)
| ~ cTOP(X)
| ~ cC56(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_143]) ).
fof(f_144_2,plain,
! [U_643] :
( ( cC58(U_643)
| ~ cTOP(U_643)
| ~ cC56(U_643) )
& ( ( cTOP(U_643)
& cC56(U_643) )
| ~ cC58(U_643) ) ),
inference(variable_rename,[status(thm)],[f_144_1]) ).
fof(f_144_3,plain,
( ! [U_645] :
( cC58(U_645)
| ~ cTOP(U_645)
| ~ cC56(U_645) )
& ! [U_644] :
( ( cTOP(U_644)
& cC56(U_644) )
| ~ cC58(U_644) ) ),
inference(miniscope,[status(thm)],[f_144_2]) ).
fof(f_144_4,plain,
( ! [U_644] :
( cTOP(U_644)
| ~ sP60(U_644) )
& ! [U_644] :
( cC56(U_644)
| ~ sP60(U_644) )
& ! [U_645] :
( cC58(U_645)
| ~ cTOP(U_645)
| ~ cC56(U_645) )
& ! [U_644] :
( sP60(U_644)
| ~ cC58(U_644) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP60])],[f_144_3]) ).
cnf(f_144_5,plain,
( sP60(U_644)
| ~ cC58(U_644) ),
inference(clausify,[status(thm)],[f_144_4]) ).
cnf(f_144_6,plain,
( cC58(U_645)
| ~ cTOP(U_645)
| ~ cC56(U_645) ),
inference(clausify,[status(thm)],[f_144_4]) ).
cnf(f_144_7,plain,
( cC56(U_644)
| ~ sP60(U_644) ),
inference(clausify,[status(thm)],[f_144_4]) ).
fof(f_147_1,plain,
! [X] :
( ( cC60(X)
| ~ cC42(X)
| ~ cC58(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_146]) ).
fof(f_147_2,plain,
! [U_656] :
( ( cC60(U_656)
| ~ cC42(U_656)
| ~ cC58(U_656) )
& ( ( cC42(U_656)
& cC58(U_656) )
| ~ cC60(U_656) ) ),
inference(variable_rename,[status(thm)],[f_147_1]) ).
fof(f_147_3,plain,
( ! [U_658] :
( cC60(U_658)
| ~ cC42(U_658)
| ~ cC58(U_658) )
& ! [U_657] :
( ( cC42(U_657)
& cC58(U_657) )
| ~ cC60(U_657) ) ),
inference(miniscope,[status(thm)],[f_147_2]) ).
fof(f_147_4,plain,
( ! [U_657] :
( cC42(U_657)
| ~ sP61(U_657) )
& ! [U_657] :
( cC58(U_657)
| ~ sP61(U_657) )
& ! [U_658] :
( cC60(U_658)
| ~ cC42(U_658)
| ~ cC58(U_658) )
& ! [U_657] :
( sP61(U_657)
| ~ cC60(U_657) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP61])],[f_147_3]) ).
cnf(f_147_5,plain,
( sP61(U_657)
| ~ cC60(U_657) ),
inference(clausify,[status(thm)],[f_147_4]) ).
cnf(f_147_6,plain,
( cC60(U_658)
| ~ cC42(U_658)
| ~ cC58(U_658) ),
inference(clausify,[status(thm)],[f_147_4]) ).
cnf(f_147_7,plain,
( cC58(U_657)
| ~ sP61(U_657) ),
inference(clausify,[status(thm)],[f_147_4]) ).
cnf(f_147_8,plain,
( cC42(U_657)
| ~ sP61(U_657) ),
inference(clausify,[status(thm)],[f_147_4]) ).
fof(f_148_1,plain,
! [X] :
( ( cC62(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_147]) ).
fof(f_148_2,plain,
! [U_659] :
( ( cC62(U_659)
| ~ cTOP(U_659) )
& ( cTOP(U_659)
| ~ cC62(U_659) ) ),
inference(variable_rename,[status(thm)],[f_148_1]) ).
fof(f_148_3,plain,
( ! [U_661] :
( cC62(U_661)
| ~ cTOP(U_661) )
& ! [U_660] :
( cTOP(U_660)
| ~ cC62(U_660) ) ),
inference(miniscope,[status(thm)],[f_148_2]) ).
fof(f_148_4,plain,
( ! [U_661] :
( cC62(U_661)
| ~ cTOP(U_661) )
& ! [U_660] :
( cTOP(U_660)
| ~ cC62(U_660) ) ),
inference(definitional_conversion,[status(esa)],[f_148_3]) ).
cnf(f_148_6,plain,
( cC62(U_661)
| ~ cTOP(U_661) ),
inference(clausify,[status(thm)],[f_148_4]) ).
fof(f_149_1,plain,
! [X] :
( ( cC64(X)
| ~ cC62(X)
| ~ cC60(X) )
& ( ( cC62(X)
& cC60(X) )
| ~ cC64(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_148]) ).
fof(f_149_2,plain,
! [U_662] :
( ( cC64(U_662)
| ~ cC62(U_662)
| ~ cC60(U_662) )
& ( ( cC62(U_662)
& cC60(U_662) )
| ~ cC64(U_662) ) ),
inference(variable_rename,[status(thm)],[f_149_1]) ).
fof(f_149_3,plain,
( ! [U_664] :
( cC64(U_664)
| ~ cC62(U_664)
| ~ cC60(U_664) )
& ! [U_663] :
( ( cC62(U_663)
& cC60(U_663) )
| ~ cC64(U_663) ) ),
inference(miniscope,[status(thm)],[f_149_2]) ).
fof(f_149_4,plain,
( ! [U_663] :
( cC62(U_663)
| ~ sP62(U_663) )
& ! [U_663] :
( cC60(U_663)
| ~ sP62(U_663) )
& ! [U_664] :
( cC64(U_664)
| ~ cC62(U_664)
| ~ cC60(U_664) )
& ! [U_663] :
( sP62(U_663)
| ~ cC64(U_663) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP62])],[f_149_3]) ).
cnf(f_149_5,plain,
( sP62(U_663)
| ~ cC64(U_663) ),
inference(clausify,[status(thm)],[f_149_4]) ).
cnf(f_149_6,plain,
( cC64(U_664)
| ~ cC62(U_664)
| ~ cC60(U_664) ),
inference(clausify,[status(thm)],[f_149_4]) ).
cnf(f_149_7,plain,
( cC60(U_663)
| ~ sP62(U_663) ),
inference(clausify,[status(thm)],[f_149_4]) ).
cnf(f_149_8,plain,
( cC62(U_663)
| ~ sP62(U_663) ),
inference(clausify,[status(thm)],[f_149_4]) ).
fof(f_150_1,plain,
! [X] :
( ( cC66(X)
| ! [Y0] : ~ ra_Px21(X,Y0) )
& ( ? [Y0] : ra_Px21(X,Y0)
| ~ cC66(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_149]) ).
fof(f_150_2,plain,
! [U_667] :
( ( cC66(U_667)
| ! [U_666] : ~ ra_Px21(U_667,U_666) )
& ( ? [U_665] : ra_Px21(U_667,U_665)
| ~ cC66(U_667) ) ),
inference(variable_rename,[status(thm)],[f_150_1]) ).
fof(f_150_3,plain,
( ! [U_669] :
( cC66(U_669)
| ! [U_666] : ~ ra_Px21(U_669,U_666) )
& ! [U_668] :
( ? [U_665] : ra_Px21(U_668,U_665)
| ~ cC66(U_668) ) ),
inference(miniscope,[status(thm)],[f_150_2]) ).
fof(f_150_4,plain,
( ! [U_669] :
( cC66(U_669)
| ! [U_666] : ~ ra_Px21(U_669,U_666) )
& ! [U_668] :
( ra_Px21(U_668,sK110(U_668))
| ~ cC66(U_668) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110]),skolemize(U_665,sK110(U_668))],[f_150_3]) ).
fof(f_150_5,plain,
( ! [U_669,U_666] :
( cC66(U_669)
| ~ ra_Px21(U_669,U_666) )
& ! [U_668] :
( ra_Px21(U_668,sK110(U_668))
| ~ cC66(U_668) ) ),
inference(definitional_conversion,[status(esa)],[f_150_4]) ).
cnf(f_150_7,plain,
( cC66(U_669)
| ~ ra_Px21(U_669,U_666) ),
inference(clausify,[status(thm)],[f_150_5]) ).
fof(f_152_1,plain,
! [X] :
( ( cC66xcomp(X)
| ? [Y] : ra_Px21(X,Y) )
& ( ! [Y] : ~ ra_Px21(X,Y)
| ~ cC66xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_151]) ).
fof(f_152_2,plain,
! [U_677] :
( ( cC66xcomp(U_677)
| ? [U_676] : ra_Px21(U_677,U_676) )
& ( ! [U_675] : ~ ra_Px21(U_677,U_675)
| ~ cC66xcomp(U_677) ) ),
inference(variable_rename,[status(thm)],[f_152_1]) ).
fof(f_152_3,plain,
( ! [U_679] :
( cC66xcomp(U_679)
| ? [U_676] : ra_Px21(U_679,U_676) )
& ! [U_678] :
( ! [U_675] : ~ ra_Px21(U_678,U_675)
| ~ cC66xcomp(U_678) ) ),
inference(miniscope,[status(thm)],[f_152_2]) ).
fof(f_152_4,plain,
( ! [U_679] :
( cC66xcomp(U_679)
| ra_Px21(U_679,sK112(U_679)) )
& ! [U_678] :
( ! [U_675] : ~ ra_Px21(U_678,U_675)
| ~ cC66xcomp(U_678) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK112]),skolemize(U_676,sK112(U_679))],[f_152_3]) ).
fof(f_152_5,plain,
( ! [U_679] :
( cC66xcomp(U_679)
| ra_Px21(U_679,sK112(U_679)) )
& ! [U_678,U_675] :
( ~ ra_Px21(U_678,U_675)
| ~ cC66xcomp(U_678) ) ),
inference(definitional_conversion,[status(esa)],[f_152_4]) ).
cnf(f_152_7,plain,
( cC66xcomp(U_679)
| ra_Px21(U_679,sK112(U_679)) ),
inference(clausify,[status(thm)],[f_152_5]) ).
fof(f_154_1,plain,
! [X] :
( ( cC68(X)
| ~ cC66xcomp(X)
| ~ cC18xcomp(X) )
& ( ( cC66xcomp(X)
& cC18xcomp(X) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_153]) ).
fof(f_154_2,plain,
! [U_685] :
( ( cC68(U_685)
| ~ cC66xcomp(U_685)
| ~ cC18xcomp(U_685) )
& ( ( cC66xcomp(U_685)
& cC18xcomp(U_685) )
| ~ cC68(U_685) ) ),
inference(variable_rename,[status(thm)],[f_154_1]) ).
fof(f_154_3,plain,
( ! [U_687] :
( cC68(U_687)
| ~ cC66xcomp(U_687)
| ~ cC18xcomp(U_687) )
& ! [U_686] :
( ( cC66xcomp(U_686)
& cC18xcomp(U_686) )
| ~ cC68(U_686) ) ),
inference(miniscope,[status(thm)],[f_154_2]) ).
fof(f_154_4,plain,
( ! [U_686] :
( cC66xcomp(U_686)
| ~ sP64(U_686) )
& ! [U_686] :
( cC18xcomp(U_686)
| ~ sP64(U_686) )
& ! [U_687] :
( cC68(U_687)
| ~ cC66xcomp(U_687)
| ~ cC18xcomp(U_687) )
& ! [U_686] :
( sP64(U_686)
| ~ cC68(U_686) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP64])],[f_154_3]) ).
cnf(f_154_6,plain,
( cC68(U_687)
| ~ cC66xcomp(U_687)
| ~ cC18xcomp(U_687) ),
inference(clausify,[status(thm)],[f_154_4]) ).
fof(f_156_1,plain,
! [X] :
( ( cC70(X)
| ! [Y] :
( ~ cC68(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC68(Y)
& rR1(X,Y) )
| ~ cC70(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_155]) ).
fof(f_156_2,plain,
! [U_695] :
( ( cC70(U_695)
| ! [U_694] :
( ~ cC68(U_694)
| ~ rR1(U_695,U_694) ) )
& ( ? [U_693] :
( cC68(U_693)
& rR1(U_695,U_693) )
| ~ cC70(U_695) ) ),
inference(variable_rename,[status(thm)],[f_156_1]) ).
fof(f_156_3,plain,
( ! [U_697] :
( cC70(U_697)
| ! [U_694] :
( ~ cC68(U_694)
| ~ rR1(U_697,U_694) ) )
& ! [U_696] :
( ? [U_693] :
( cC68(U_693)
& rR1(U_696,U_693) )
| ~ cC70(U_696) ) ),
inference(miniscope,[status(thm)],[f_156_2]) ).
fof(f_156_4,plain,
( ! [U_697] :
( cC70(U_697)
| ! [U_694] :
( ~ cC68(U_694)
| ~ rR1(U_697,U_694) ) )
& ! [U_696] :
( ( cC68(sK115(U_696))
& rR1(U_696,sK115(U_696)) )
| ~ cC70(U_696) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115]),skolemize(U_693,sK115(U_696))],[f_156_3]) ).
fof(f_156_5,plain,
( ! [U_696] :
( cC68(sK115(U_696))
| ~ sP65(U_696) )
& ! [U_696] :
( rR1(U_696,sK115(U_696))
| ~ sP65(U_696) )
& ! [U_697,U_694] :
( cC70(U_697)
| ~ cC68(U_694)
| ~ rR1(U_697,U_694) )
& ! [U_696] :
( sP65(U_696)
| ~ cC70(U_696) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP65])],[f_156_4]) ).
cnf(f_156_7,plain,
( cC70(U_697)
| ~ cC68(U_694)
| ~ rR1(U_697,U_694) ),
inference(clausify,[status(thm)],[f_156_5]) ).
fof(f_157_1,plain,
! [X] :
( ( cC70(X)
| ? [Y] : ra_Px25(X,Y) )
& ( ! [Y] : ~ ra_Px25(X,Y)
| ~ cC70(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_156]) ).
fof(f_157_2,plain,
! [U_700] :
( ( cC70(U_700)
| ? [U_699] : ra_Px25(U_700,U_699) )
& ( ! [U_698] : ~ ra_Px25(U_700,U_698)
| ~ cC70(U_700) ) ),
inference(variable_rename,[status(thm)],[f_157_1]) ).
fof(f_157_3,plain,
( ! [U_702] :
( cC70(U_702)
| ? [U_699] : ra_Px25(U_702,U_699) )
& ! [U_701] :
( ! [U_698] : ~ ra_Px25(U_701,U_698)
| ~ cC70(U_701) ) ),
inference(miniscope,[status(thm)],[f_157_2]) ).
fof(f_157_4,plain,
( ! [U_702] :
( cC70(U_702)
| ra_Px25(U_702,sK116(U_702)) )
& ! [U_701] :
( ! [U_698] : ~ ra_Px25(U_701,U_698)
| ~ cC70(U_701) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116]),skolemize(U_699,sK116(U_702))],[f_157_3]) ).
fof(f_157_5,plain,
( ! [U_702] :
( cC70(U_702)
| ra_Px25(U_702,sK116(U_702)) )
& ! [U_701,U_698] :
( ~ ra_Px25(U_701,U_698)
| ~ cC70(U_701) ) ),
inference(definitional_conversion,[status(esa)],[f_157_4]) ).
cnf(f_157_6,plain,
( ~ ra_Px25(U_701,U_698)
| ~ cC70(U_701) ),
inference(clausify,[status(thm)],[f_157_5]) ).
fof(f_158_1,plain,
! [X] :
( ( cC70xcomp(X)
| ! [Y0] : ~ ra_Px25(X,Y0) )
& ( ? [Y0] : ra_Px25(X,Y0)
| ~ cC70xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_157]) ).
fof(f_158_2,plain,
! [U_705] :
( ( cC70xcomp(U_705)
| ! [U_704] : ~ ra_Px25(U_705,U_704) )
& ( ? [U_703] : ra_Px25(U_705,U_703)
| ~ cC70xcomp(U_705) ) ),
inference(variable_rename,[status(thm)],[f_158_1]) ).
fof(f_158_3,plain,
( ! [U_707] :
( cC70xcomp(U_707)
| ! [U_704] : ~ ra_Px25(U_707,U_704) )
& ! [U_706] :
( ? [U_703] : ra_Px25(U_706,U_703)
| ~ cC70xcomp(U_706) ) ),
inference(miniscope,[status(thm)],[f_158_2]) ).
fof(f_158_4,plain,
( ! [U_707] :
( cC70xcomp(U_707)
| ! [U_704] : ~ ra_Px25(U_707,U_704) )
& ! [U_706] :
( ra_Px25(U_706,sK117(U_706))
| ~ cC70xcomp(U_706) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK117]),skolemize(U_703,sK117(U_706))],[f_158_3]) ).
fof(f_158_5,plain,
( ! [U_707,U_704] :
( cC70xcomp(U_707)
| ~ ra_Px25(U_707,U_704) )
& ! [U_706] :
( ra_Px25(U_706,sK117(U_706))
| ~ cC70xcomp(U_706) ) ),
inference(definitional_conversion,[status(esa)],[f_158_4]) ).
cnf(f_158_6,plain,
( ra_Px25(U_706,sK117(U_706))
| ~ cC70xcomp(U_706) ),
inference(clausify,[status(thm)],[f_158_5]) ).
fof(f_159_1,plain,
! [X] :
( ( cC72(X)
| ! [Y0] : ~ ra_Px24(X,Y0) )
& ( ? [Y0] : ra_Px24(X,Y0)
| ~ cC72(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_158]) ).
fof(f_159_2,plain,
! [U_710] :
( ( cC72(U_710)
| ! [U_709] : ~ ra_Px24(U_710,U_709) )
& ( ? [U_708] : ra_Px24(U_710,U_708)
| ~ cC72(U_710) ) ),
inference(variable_rename,[status(thm)],[f_159_1]) ).
fof(f_159_3,plain,
( ! [U_712] :
( cC72(U_712)
| ! [U_709] : ~ ra_Px24(U_712,U_709) )
& ! [U_711] :
( ? [U_708] : ra_Px24(U_711,U_708)
| ~ cC72(U_711) ) ),
inference(miniscope,[status(thm)],[f_159_2]) ).
fof(f_159_4,plain,
( ! [U_712] :
( cC72(U_712)
| ! [U_709] : ~ ra_Px24(U_712,U_709) )
& ! [U_711] :
( ra_Px24(U_711,sK118(U_711))
| ~ cC72(U_711) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118]),skolemize(U_708,sK118(U_711))],[f_159_3]) ).
fof(f_159_5,plain,
( ! [U_712,U_709] :
( cC72(U_712)
| ~ ra_Px24(U_712,U_709) )
& ! [U_711] :
( ra_Px24(U_711,sK118(U_711))
| ~ cC72(U_711) ) ),
inference(definitional_conversion,[status(esa)],[f_159_4]) ).
cnf(f_159_7,plain,
( cC72(U_712)
| ~ ra_Px24(U_712,U_709) ),
inference(clausify,[status(thm)],[f_159_5]) ).
fof(f_161_1,plain,
! [X] :
( ( cC72xcomp(X)
| ? [Y] : ra_Px24(X,Y) )
& ( ! [Y] : ~ ra_Px24(X,Y)
| ~ cC72xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_160]) ).
fof(f_161_2,plain,
! [U_720] :
( ( cC72xcomp(U_720)
| ? [U_719] : ra_Px24(U_720,U_719) )
& ( ! [U_718] : ~ ra_Px24(U_720,U_718)
| ~ cC72xcomp(U_720) ) ),
inference(variable_rename,[status(thm)],[f_161_1]) ).
fof(f_161_3,plain,
( ! [U_722] :
( cC72xcomp(U_722)
| ? [U_719] : ra_Px24(U_722,U_719) )
& ! [U_721] :
( ! [U_718] : ~ ra_Px24(U_721,U_718)
| ~ cC72xcomp(U_721) ) ),
inference(miniscope,[status(thm)],[f_161_2]) ).
fof(f_161_4,plain,
( ! [U_722] :
( cC72xcomp(U_722)
| ra_Px24(U_722,sK120(U_722)) )
& ! [U_721] :
( ! [U_718] : ~ ra_Px24(U_721,U_718)
| ~ cC72xcomp(U_721) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK120]),skolemize(U_719,sK120(U_722))],[f_161_3]) ).
fof(f_161_5,plain,
( ! [U_722] :
( cC72xcomp(U_722)
| ra_Px24(U_722,sK120(U_722)) )
& ! [U_718,U_721] :
( ~ ra_Px24(U_721,U_718)
| ~ cC72xcomp(U_721) ) ),
inference(definitional_conversion,[status(esa)],[f_161_4]) ).
cnf(f_161_7,plain,
( cC72xcomp(U_722)
| ra_Px24(U_722,sK120(U_722)) ),
inference(clausify,[status(thm)],[f_161_5]) ).
fof(f_162_1,plain,
! [X] :
( ( cC74(X)
| ~ cC18xcomp(X)
| ~ cC72xcomp(X) )
& ( ( cC18xcomp(X)
& cC72xcomp(X) )
| ~ cC74(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_161]) ).
fof(f_162_2,plain,
! [U_723] :
( ( cC74(U_723)
| ~ cC18xcomp(U_723)
| ~ cC72xcomp(U_723) )
& ( ( cC18xcomp(U_723)
& cC72xcomp(U_723) )
| ~ cC74(U_723) ) ),
inference(variable_rename,[status(thm)],[f_162_1]) ).
fof(f_162_3,plain,
( ! [U_725] :
( cC74(U_725)
| ~ cC18xcomp(U_725)
| ~ cC72xcomp(U_725) )
& ! [U_724] :
( ( cC18xcomp(U_724)
& cC72xcomp(U_724) )
| ~ cC74(U_724) ) ),
inference(miniscope,[status(thm)],[f_162_2]) ).
fof(f_162_4,plain,
( ! [U_724] :
( cC18xcomp(U_724)
| ~ sP67(U_724) )
& ! [U_724] :
( cC72xcomp(U_724)
| ~ sP67(U_724) )
& ! [U_725] :
( cC74(U_725)
| ~ cC18xcomp(U_725)
| ~ cC72xcomp(U_725) )
& ! [U_724] :
( sP67(U_724)
| ~ cC74(U_724) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP67])],[f_162_3]) ).
cnf(f_162_6,plain,
( cC74(U_725)
| ~ cC18xcomp(U_725)
| ~ cC72xcomp(U_725) ),
inference(clausify,[status(thm)],[f_162_4]) ).
fof(f_165_1,plain,
! [X] :
( ( cC76(X)
| ! [Y] :
( ~ cC74(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC74(Y)
& rR1(X,Y) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_164]) ).
fof(f_165_2,plain,
! [U_738] :
( ( cC76(U_738)
| ! [U_737] :
( ~ cC74(U_737)
| ~ rR1(U_738,U_737) ) )
& ( ? [U_736] :
( cC74(U_736)
& rR1(U_738,U_736) )
| ~ cC76(U_738) ) ),
inference(variable_rename,[status(thm)],[f_165_1]) ).
fof(f_165_3,plain,
( ! [U_740] :
( cC76(U_740)
| ! [U_737] :
( ~ cC74(U_737)
| ~ rR1(U_740,U_737) ) )
& ! [U_739] :
( ? [U_736] :
( cC74(U_736)
& rR1(U_739,U_736) )
| ~ cC76(U_739) ) ),
inference(miniscope,[status(thm)],[f_165_2]) ).
fof(f_165_4,plain,
( ! [U_740] :
( cC76(U_740)
| ! [U_737] :
( ~ cC74(U_737)
| ~ rR1(U_740,U_737) ) )
& ! [U_739] :
( ( cC74(sK123(U_739))
& rR1(U_739,sK123(U_739)) )
| ~ cC76(U_739) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123]),skolemize(U_736,sK123(U_739))],[f_165_3]) ).
fof(f_165_5,plain,
( ! [U_739] :
( cC74(sK123(U_739))
| ~ sP68(U_739) )
& ! [U_739] :
( rR1(U_739,sK123(U_739))
| ~ sP68(U_739) )
& ! [U_737,U_740] :
( cC76(U_740)
| ~ cC74(U_737)
| ~ rR1(U_740,U_737) )
& ! [U_739] :
( sP68(U_739)
| ~ cC76(U_739) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP68])],[f_165_4]) ).
cnf(f_165_7,plain,
( cC76(U_740)
| ~ cC74(U_737)
| ~ rR1(U_740,U_737) ),
inference(clausify,[status(thm)],[f_165_5]) ).
fof(f_166_1,plain,
! [X] :
( ( cC76(X)
| ! [Y0] : ~ ra_Px26(X,Y0) )
& ( ? [Y0] : ra_Px26(X,Y0)
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_165]) ).
fof(f_166_2,plain,
! [U_743] :
( ( cC76(U_743)
| ! [U_742] : ~ ra_Px26(U_743,U_742) )
& ( ? [U_741] : ra_Px26(U_743,U_741)
| ~ cC76(U_743) ) ),
inference(variable_rename,[status(thm)],[f_166_1]) ).
fof(f_166_3,plain,
( ! [U_745] :
( cC76(U_745)
| ! [U_742] : ~ ra_Px26(U_745,U_742) )
& ! [U_744] :
( ? [U_741] : ra_Px26(U_744,U_741)
| ~ cC76(U_744) ) ),
inference(miniscope,[status(thm)],[f_166_2]) ).
fof(f_166_4,plain,
( ! [U_745] :
( cC76(U_745)
| ! [U_742] : ~ ra_Px26(U_745,U_742) )
& ! [U_744] :
( ra_Px26(U_744,sK124(U_744))
| ~ cC76(U_744) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK124]),skolemize(U_741,sK124(U_744))],[f_166_3]) ).
fof(f_166_5,plain,
( ! [U_742,U_745] :
( cC76(U_745)
| ~ ra_Px26(U_745,U_742) )
& ! [U_744] :
( ra_Px26(U_744,sK124(U_744))
| ~ cC76(U_744) ) ),
inference(definitional_conversion,[status(esa)],[f_166_4]) ).
cnf(f_166_6,plain,
( ra_Px26(U_744,sK124(U_744))
| ~ cC76(U_744) ),
inference(clausify,[status(thm)],[f_166_5]) ).
fof(f_167_1,plain,
! [X] :
( ( cC76xcomp(X)
| ? [Y] : ra_Px26(X,Y) )
& ( ! [Y] : ~ ra_Px26(X,Y)
| ~ cC76xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_166]) ).
fof(f_167_2,plain,
! [U_748] :
( ( cC76xcomp(U_748)
| ? [U_747] : ra_Px26(U_748,U_747) )
& ( ! [U_746] : ~ ra_Px26(U_748,U_746)
| ~ cC76xcomp(U_748) ) ),
inference(variable_rename,[status(thm)],[f_167_1]) ).
fof(f_167_3,plain,
( ! [U_750] :
( cC76xcomp(U_750)
| ? [U_747] : ra_Px26(U_750,U_747) )
& ! [U_749] :
( ! [U_746] : ~ ra_Px26(U_749,U_746)
| ~ cC76xcomp(U_749) ) ),
inference(miniscope,[status(thm)],[f_167_2]) ).
fof(f_167_4,plain,
( ! [U_750] :
( cC76xcomp(U_750)
| ra_Px26(U_750,sK125(U_750)) )
& ! [U_749] :
( ! [U_746] : ~ ra_Px26(U_749,U_746)
| ~ cC76xcomp(U_749) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK125]),skolemize(U_747,sK125(U_750))],[f_167_3]) ).
fof(f_167_5,plain,
( ! [U_750] :
( cC76xcomp(U_750)
| ra_Px26(U_750,sK125(U_750)) )
& ! [U_746,U_749] :
( ~ ra_Px26(U_749,U_746)
| ~ cC76xcomp(U_749) ) ),
inference(definitional_conversion,[status(esa)],[f_167_4]) ).
cnf(f_167_6,plain,
( ~ ra_Px26(U_749,U_746)
| ~ cC76xcomp(U_749) ),
inference(clausify,[status(thm)],[f_167_5]) ).
fof(f_168_1,plain,
! [X] :
( ( cC78(X)
| ~ cC76xcomp(X)
| ~ cC70xcomp(X) )
& ( ( cC76xcomp(X)
& cC70xcomp(X) )
| ~ cC78(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_167]) ).
fof(f_168_2,plain,
! [U_751] :
( ( cC78(U_751)
| ~ cC76xcomp(U_751)
| ~ cC70xcomp(U_751) )
& ( ( cC76xcomp(U_751)
& cC70xcomp(U_751) )
| ~ cC78(U_751) ) ),
inference(variable_rename,[status(thm)],[f_168_1]) ).
fof(f_168_3,plain,
( ! [U_753] :
( cC78(U_753)
| ~ cC76xcomp(U_753)
| ~ cC70xcomp(U_753) )
& ! [U_752] :
( ( cC76xcomp(U_752)
& cC70xcomp(U_752) )
| ~ cC78(U_752) ) ),
inference(miniscope,[status(thm)],[f_168_2]) ).
fof(f_168_4,plain,
( ! [U_752] :
( cC76xcomp(U_752)
| ~ sP69(U_752) )
& ! [U_752] :
( cC70xcomp(U_752)
| ~ sP69(U_752) )
& ! [U_753] :
( cC78(U_753)
| ~ cC76xcomp(U_753)
| ~ cC70xcomp(U_753) )
& ! [U_752] :
( sP69(U_752)
| ~ cC78(U_752) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP69])],[f_168_3]) ).
cnf(f_168_6,plain,
( cC78(U_753)
| ~ cC76xcomp(U_753)
| ~ cC70xcomp(U_753) ),
inference(clausify,[status(thm)],[f_168_4]) ).
fof(f_170_1,plain,
! [X] :
( ( cC80(X)
| ~ cTOP(X)
| ~ cC78(X) )
& ( ( cTOP(X)
& cC78(X) )
| ~ cC80(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_169]) ).
fof(f_170_2,plain,
! [U_759] :
( ( cC80(U_759)
| ~ cTOP(U_759)
| ~ cC78(U_759) )
& ( ( cTOP(U_759)
& cC78(U_759) )
| ~ cC80(U_759) ) ),
inference(variable_rename,[status(thm)],[f_170_1]) ).
fof(f_170_3,plain,
( ! [U_761] :
( cC80(U_761)
| ~ cTOP(U_761)
| ~ cC78(U_761) )
& ! [U_760] :
( ( cTOP(U_760)
& cC78(U_760) )
| ~ cC80(U_760) ) ),
inference(miniscope,[status(thm)],[f_170_2]) ).
fof(f_170_4,plain,
( ! [U_760] :
( cTOP(U_760)
| ~ sP71(U_760) )
& ! [U_760] :
( cC78(U_760)
| ~ sP71(U_760) )
& ! [U_761] :
( cC80(U_761)
| ~ cTOP(U_761)
| ~ cC78(U_761) )
& ! [U_760] :
( sP71(U_760)
| ~ cC80(U_760) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP71])],[f_170_3]) ).
cnf(f_170_5,plain,
( sP71(U_760)
| ~ cC80(U_760) ),
inference(clausify,[status(thm)],[f_170_4]) ).
cnf(f_170_6,plain,
( cC80(U_761)
| ~ cTOP(U_761)
| ~ cC78(U_761) ),
inference(clausify,[status(thm)],[f_170_4]) ).
cnf(f_170_7,plain,
( cC78(U_760)
| ~ sP71(U_760) ),
inference(clausify,[status(thm)],[f_170_4]) ).
fof(f_171_1,plain,
! [X] :
( ( cC82(X)
| ~ cC80(X)
| ~ cC64(X) )
& ( ( cC80(X)
& cC64(X) )
| ~ cC82(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_170]) ).
fof(f_171_2,plain,
! [U_762] :
( ( cC82(U_762)
| ~ cC80(U_762)
| ~ cC64(U_762) )
& ( ( cC80(U_762)
& cC64(U_762) )
| ~ cC82(U_762) ) ),
inference(variable_rename,[status(thm)],[f_171_1]) ).
fof(f_171_3,plain,
( ! [U_764] :
( cC82(U_764)
| ~ cC80(U_764)
| ~ cC64(U_764) )
& ! [U_763] :
( ( cC80(U_763)
& cC64(U_763) )
| ~ cC82(U_763) ) ),
inference(miniscope,[status(thm)],[f_171_2]) ).
fof(f_171_4,plain,
( ! [U_763] :
( cC80(U_763)
| ~ sP72(U_763) )
& ! [U_763] :
( cC64(U_763)
| ~ sP72(U_763) )
& ! [U_764] :
( cC82(U_764)
| ~ cC80(U_764)
| ~ cC64(U_764) )
& ! [U_763] :
( sP72(U_763)
| ~ cC82(U_763) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP72])],[f_171_3]) ).
cnf(f_171_5,plain,
( sP72(U_763)
| ~ cC82(U_763) ),
inference(clausify,[status(thm)],[f_171_4]) ).
cnf(f_171_6,plain,
( cC82(U_764)
| ~ cC80(U_764)
| ~ cC64(U_764) ),
inference(clausify,[status(thm)],[f_171_4]) ).
cnf(f_171_7,plain,
( cC64(U_763)
| ~ sP72(U_763) ),
inference(clausify,[status(thm)],[f_171_4]) ).
cnf(f_171_8,plain,
( cC80(U_763)
| ~ sP72(U_763) ),
inference(clausify,[status(thm)],[f_171_4]) ).
fof(f_172_1,plain,
! [X] :
( ( cC84(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_171]) ).
fof(f_172_2,plain,
! [U_765] :
( ( cC84(U_765)
| ~ cTOP(U_765) )
& ( cTOP(U_765)
| ~ cC84(U_765) ) ),
inference(variable_rename,[status(thm)],[f_172_1]) ).
fof(f_172_3,plain,
( ! [U_767] :
( cC84(U_767)
| ~ cTOP(U_767) )
& ! [U_766] :
( cTOP(U_766)
| ~ cC84(U_766) ) ),
inference(miniscope,[status(thm)],[f_172_2]) ).
fof(f_172_4,plain,
( ! [U_767] :
( cC84(U_767)
| ~ cTOP(U_767) )
& ! [U_766] :
( cTOP(U_766)
| ~ cC84(U_766) ) ),
inference(definitional_conversion,[status(esa)],[f_172_3]) ).
cnf(f_172_6,plain,
( cC84(U_767)
| ~ cTOP(U_767) ),
inference(clausify,[status(thm)],[f_172_4]) ).
fof(f_173_1,plain,
! [X] :
( ( cC86(X)
| ~ cC84(X)
| ~ cC82(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_172]) ).
fof(f_173_2,plain,
! [U_768] :
( ( cC86(U_768)
| ~ cC84(U_768)
| ~ cC82(U_768) )
& ( ( cC84(U_768)
& cC82(U_768) )
| ~ cC86(U_768) ) ),
inference(variable_rename,[status(thm)],[f_173_1]) ).
fof(f_173_3,plain,
( ! [U_770] :
( cC86(U_770)
| ~ cC84(U_770)
| ~ cC82(U_770) )
& ! [U_769] :
( ( cC84(U_769)
& cC82(U_769) )
| ~ cC86(U_769) ) ),
inference(miniscope,[status(thm)],[f_173_2]) ).
fof(f_173_4,plain,
( ! [U_769] :
( cC84(U_769)
| ~ sP73(U_769) )
& ! [U_769] :
( cC82(U_769)
| ~ sP73(U_769) )
& ! [U_770] :
( cC86(U_770)
| ~ cC84(U_770)
| ~ cC82(U_770) )
& ! [U_769] :
( sP73(U_769)
| ~ cC86(U_769) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP73])],[f_173_3]) ).
cnf(f_173_5,plain,
( sP73(U_769)
| ~ cC86(U_769) ),
inference(clausify,[status(thm)],[f_173_4]) ).
cnf(f_173_6,plain,
( cC86(U_770)
| ~ cC84(U_770)
| ~ cC82(U_770) ),
inference(clausify,[status(thm)],[f_173_4]) ).
cnf(f_173_7,plain,
( cC82(U_769)
| ~ sP73(U_769) ),
inference(clausify,[status(thm)],[f_173_4]) ).
cnf(f_173_8,plain,
( cC84(U_769)
| ~ sP73(U_769) ),
inference(clausify,[status(thm)],[f_173_4]) ).
fof(f_175_1,plain,
! [X] :
( ( cC90(X)
| ~ cC88(X)
| ~ cC86(X) )
& ( ( cC88(X)
& cC86(X) )
| ~ cC90(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_174]) ).
fof(f_175_2,plain,
! [U_774] :
( ( cC90(U_774)
| ~ cC88(U_774)
| ~ cC86(U_774) )
& ( ( cC88(U_774)
& cC86(U_774) )
| ~ cC90(U_774) ) ),
inference(variable_rename,[status(thm)],[f_175_1]) ).
fof(f_175_3,plain,
( ! [U_776] :
( cC90(U_776)
| ~ cC88(U_776)
| ~ cC86(U_776) )
& ! [U_775] :
( ( cC88(U_775)
& cC86(U_775) )
| ~ cC90(U_775) ) ),
inference(miniscope,[status(thm)],[f_175_2]) ).
fof(f_175_4,plain,
( ! [U_775] :
( cC88(U_775)
| ~ sP74(U_775) )
& ! [U_775] :
( cC86(U_775)
| ~ sP74(U_775) )
& ! [U_776] :
( cC90(U_776)
| ~ cC88(U_776)
| ~ cC86(U_776) )
& ! [U_775] :
( sP74(U_775)
| ~ cC90(U_775) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP74])],[f_175_3]) ).
cnf(f_175_5,plain,
( sP74(U_775)
| ~ cC90(U_775) ),
inference(clausify,[status(thm)],[f_175_4]) ).
cnf(f_175_6,plain,
( cC90(U_776)
| ~ cC88(U_776)
| ~ cC86(U_776) ),
inference(clausify,[status(thm)],[f_175_4]) ).
cnf(f_175_8,plain,
( cC88(U_775)
| ~ sP74(U_775) ),
inference(clausify,[status(thm)],[f_175_4]) ).
fof(f_187_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC180(X)
| ~ cC158(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_186]) ).
fof(f_187_2,plain,
! [U_830] :
( ( cTEST(U_830)
| ~ cC180(U_830)
| ~ cC158(U_830) )
& ( ( cC180(U_830)
& cC158(U_830) )
| ~ cTEST(U_830) ) ),
inference(variable_rename,[status(thm)],[f_187_1]) ).
fof(f_187_3,plain,
( ! [U_832] :
( cTEST(U_832)
| ~ cC180(U_832)
| ~ cC158(U_832) )
& ! [U_831] :
( ( cC180(U_831)
& cC158(U_831) )
| ~ cTEST(U_831) ) ),
inference(miniscope,[status(thm)],[f_187_2]) ).
fof(f_187_4,plain,
( ! [U_831] :
( cC180(U_831)
| ~ sP78(U_831) )
& ! [U_831] :
( cC158(U_831)
| ~ sP78(U_831) )
& ! [U_832] :
( cTEST(U_832)
| ~ cC180(U_832)
| ~ cC158(U_832) )
& ! [U_831] :
( sP78(U_831)
| ~ cTEST(U_831) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP78])],[f_187_3]) ).
cnf(f_187_5,plain,
( sP78(U_831)
| ~ cTEST(U_831) ),
inference(clausify,[status(thm)],[f_187_4]) ).
cnf(f_187_7,plain,
( cC158(U_831)
| ~ sP78(U_831) ),
inference(clausify,[status(thm)],[f_187_4]) ).
cnf(f_187_8,plain,
( cC180(U_831)
| ~ sP78(U_831) ),
inference(clausify,[status(thm)],[f_187_4]) ).
fof(f_190_1,plain,
! [X] :
( cC46xcomp(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_189]) ).
fof(f_190_2,plain,
! [U_834] :
( cC46xcomp(U_834)
| ~ rR1(iV21026,U_834) ),
inference(variable_rename,[status(thm)],[f_190_1]) ).
fof(f_190_3,plain,
! [U_834] :
( cC46xcomp(U_834)
| ~ rR1(iV21026,U_834) ),
inference(definitional_conversion,[status(esa)],[f_190_2]) ).
cnf(f_190_4,plain,
( cC46xcomp(U_834)
| ~ rR1(iV21026,U_834) ),
inference(clausify,[status(thm)],[f_190_3]) ).
fof(f_191_1,plain,
cTOP(iV21026),
inference(fof_nnf,[status(thm)],[axiom_190]) ).
fof(f_191_2,plain,
cTOP(iV21026),
inference(definitional_conversion,[status(esa)],[f_191_1]) ).
cnf(f_191_3,plain,
cTOP(iV21026),
inference(clausify,[status(thm)],[f_191_2]) ).
fof(f_196_1,plain,
cC76xcomp(iV21026),
inference(fof_nnf,[status(thm)],[axiom_195]) ).
fof(f_196_2,plain,
cC76xcomp(iV21026),
inference(definitional_conversion,[status(esa)],[f_196_1]) ).
cnf(f_196_3,plain,
cC76xcomp(iV21026),
inference(clausify,[status(thm)],[f_196_2]) ).
fof(f_204_1,plain,
cC34xcomp(iV21026),
inference(fof_nnf,[status(thm)],[axiom_203]) ).
fof(f_204_2,plain,
cC34xcomp(iV21026),
inference(definitional_conversion,[status(esa)],[f_204_1]) ).
cnf(f_204_3,plain,
cC34xcomp(iV21026),
inference(clausify,[status(thm)],[f_204_2]) ).
fof(f_206_1,plain,
cC28xcomp(iV21026),
inference(fof_nnf,[status(thm)],[axiom_205]) ).
fof(f_206_2,plain,
cC28xcomp(iV21026),
inference(definitional_conversion,[status(esa)],[f_206_1]) ).
cnf(f_206_3,plain,
cC28xcomp(iV21026),
inference(clausify,[status(thm)],[f_206_2]) ).
fof(f_210_1,plain,
cC54xcomp(iV21026),
inference(fof_nnf,[status(thm)],[axiom_209]) ).
fof(f_210_2,plain,
cC54xcomp(iV21026),
inference(definitional_conversion,[status(esa)],[f_210_1]) ).
cnf(f_210_3,plain,
cC54xcomp(iV21026),
inference(clausify,[status(thm)],[f_210_2]) ).
fof(f_216_1,plain,
cC70xcomp(iV21026),
inference(fof_nnf,[status(thm)],[axiom_215]) ).
fof(f_216_2,plain,
cC70xcomp(iV21026),
inference(definitional_conversion,[status(esa)],[f_216_1]) ).
cnf(f_216_3,plain,
cC70xcomp(iV21026),
inference(clausify,[status(thm)],[f_216_2]) ).
fof(f_218_1,plain,
cC48xcomp(iV21026),
inference(fof_nnf,[status(thm)],[axiom_217]) ).
fof(f_218_2,plain,
cC48xcomp(iV21026),
inference(definitional_conversion,[status(esa)],[f_218_1]) ).
cnf(f_218_3,plain,
cC48xcomp(iV21026),
inference(clausify,[status(thm)],[f_218_2]) ).
fof(f_220_1,plain,
cowlThing(iV21026),
inference(fof_nnf,[status(thm)],[axiom_219]) ).
fof(f_220_2,plain,
cowlThing(iV21026),
inference(definitional_conversion,[status(esa)],[f_220_1]) ).
cnf(f_220_3,plain,
cowlThing(iV21026),
inference(clausify,[status(thm)],[f_220_2]) ).
fof(f_222_1,plain,
cTEST(iV21026),
inference(fof_nnf,[status(thm)],[axiom_221]) ).
fof(f_222_2,plain,
cTEST(iV21026),
inference(definitional_conversion,[status(esa)],[f_222_1]) ).
cnf(f_222_3,plain,
cTEST(iV21026),
inference(clausify,[status(thm)],[f_222_2]) ).
fof(f_223_1,plain,
rR1(iV21026,iV21030),
inference(fof_nnf,[status(thm)],[axiom_222]) ).
fof(f_223_2,plain,
rR1(iV21026,iV21030),
inference(definitional_conversion,[status(esa)],[f_223_1]) ).
cnf(f_223_3,plain,
rR1(iV21026,iV21030),
inference(clausify,[status(thm)],[f_223_2]) ).
fof(f_224_1,plain,
rR1(iV21026,iV21027),
inference(fof_nnf,[status(thm)],[axiom_223]) ).
fof(f_224_2,plain,
rR1(iV21026,iV21027),
inference(definitional_conversion,[status(esa)],[f_224_1]) ).
cnf(f_224_3,plain,
rR1(iV21026,iV21027),
inference(clausify,[status(thm)],[f_224_2]) ).
fof(f_226_1,plain,
rR1(iV21026,iV21029),
inference(fof_nnf,[status(thm)],[axiom_225]) ).
fof(f_226_2,plain,
rR1(iV21026,iV21029),
inference(definitional_conversion,[status(esa)],[f_226_1]) ).
cnf(f_226_3,plain,
rR1(iV21026,iV21029),
inference(clausify,[status(thm)],[f_226_2]) ).
fof(f_238_1,plain,
cC2xcomp(iV21027),
inference(fof_nnf,[status(thm)],[axiom_237]) ).
fof(f_238_2,plain,
cC2xcomp(iV21027),
inference(definitional_conversion,[status(esa)],[f_238_1]) ).
cnf(f_238_3,plain,
cC2xcomp(iV21027),
inference(clausify,[status(thm)],[f_238_2]) ).
fof(f_249_1,plain,
cowlThing(iV21027),
inference(fof_nnf,[status(thm)],[axiom_248]) ).
fof(f_249_2,plain,
cowlThing(iV21027),
inference(definitional_conversion,[status(esa)],[f_249_1]) ).
cnf(f_249_3,plain,
cowlThing(iV21027),
inference(clausify,[status(thm)],[f_249_2]) ).
fof(f_254_1,plain,
rR1(iV21027,iV21035),
inference(fof_nnf,[status(thm)],[axiom_253]) ).
fof(f_254_2,plain,
rR1(iV21027,iV21035),
inference(definitional_conversion,[status(esa)],[f_254_1]) ).
cnf(f_254_3,plain,
rR1(iV21027,iV21035),
inference(clausify,[status(thm)],[f_254_2]) ).
fof(f_266_1,plain,
cC12xcomp(iV21029),
inference(fof_nnf,[status(thm)],[axiom_265]) ).
fof(f_266_2,plain,
cC12xcomp(iV21029),
inference(definitional_conversion,[status(esa)],[f_266_1]) ).
cnf(f_266_3,plain,
cC12xcomp(iV21029),
inference(clausify,[status(thm)],[f_266_2]) ).
fof(f_279_1,plain,
cowlThing(iV21029),
inference(fof_nnf,[status(thm)],[axiom_278]) ).
fof(f_279_2,plain,
cowlThing(iV21029),
inference(definitional_conversion,[status(esa)],[f_279_1]) ).
cnf(f_279_3,plain,
cowlThing(iV21029),
inference(clausify,[status(thm)],[f_279_2]) ).
fof(f_294_1,plain,
cC18xcomp(iV21030),
inference(fof_nnf,[status(thm)],[axiom_293]) ).
fof(f_294_2,plain,
cC18xcomp(iV21030),
inference(definitional_conversion,[status(esa)],[f_294_1]) ).
cnf(f_294_3,plain,
cC18xcomp(iV21030),
inference(clausify,[status(thm)],[f_294_2]) ).
fof(f_307_1,plain,
cowlThing(iV21030),
inference(fof_nnf,[status(thm)],[axiom_306]) ).
fof(f_307_2,plain,
cowlThing(iV21030),
inference(definitional_conversion,[status(esa)],[f_307_1]) ).
cnf(f_307_3,plain,
cowlThing(iV21030),
inference(clausify,[status(thm)],[f_307_2]) ).
fof(f_332_1,plain,
cC12xcomp(iV21035),
inference(fof_nnf,[status(thm)],[axiom_331]) ).
fof(f_332_2,plain,
cC12xcomp(iV21035),
inference(definitional_conversion,[status(esa)],[f_332_1]) ).
cnf(f_332_3,plain,
cC12xcomp(iV21035),
inference(clausify,[status(thm)],[f_332_2]) ).
fof(f_343_1,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)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_343_2,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)
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_343_1]) ).
fof(f_343_3,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)
| ? [U_862] :
( ( ~ xsd_string(U_862)
& ~ xsd_integer(U_862) )
| ( xsd_integer(U_862)
& xsd_string(U_862) ) )
| ? [U_861] :
( cowlNothing(U_861)
| ~ cowlThing(U_861) ) ),
inference(variable_rename,[status(thm)],[f_343_2]) ).
fof(f_343_4,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)
| ? [U_866] :
( ~ xsd_string(U_866)
& ~ xsd_integer(U_866) )
| ? [U_865] :
( xsd_integer(U_865)
& xsd_string(U_865) )
| ? [U_864] : cowlNothing(U_864)
| ? [U_863] : ~ cowlThing(U_863) ),
inference(miniscope,[status(thm)],[f_343_3]) ).
fof(f_343_5,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)
| ? [U_866] :
( ~ xsd_string(U_866)
& ~ xsd_integer(U_866) )
| ? [U_865] :
( xsd_integer(U_865)
& xsd_string(U_865) )
| ? [U_864] : cowlNothing(U_864)
| ~ cowlThing(sK137) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK137]),skolemize(U_863,sK137)],[f_343_4]) ).
fof(f_343_6,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)
| ? [U_866] :
( ~ xsd_string(U_866)
& ~ xsd_integer(U_866) )
| ? [U_865] :
( xsd_integer(U_865)
& xsd_string(U_865) )
| cowlNothing(sK138)
| ~ cowlThing(sK137) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK138]),skolemize(U_864,sK138)],[f_343_5]) ).
fof(f_343_7,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)
| ? [U_866] :
( ~ xsd_string(U_866)
& ~ xsd_integer(U_866) )
| ( xsd_integer(sK139)
& xsd_string(sK139) )
| cowlNothing(sK138)
| ~ cowlThing(sK137) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK139]),skolemize(U_865,sK139)],[f_343_6]) ).
fof(f_343_8,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)
| ( ~ xsd_string(sK140)
& ~ xsd_integer(sK140) )
| ( xsd_integer(sK139)
& xsd_string(sK139) )
| cowlNothing(sK138)
| ~ cowlThing(sK137) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK140]),skolemize(U_866,sK140)],[f_343_7]) ).
fof(f_343_9,negated_conjecture,
( ( ~ xsd_string(sK140)
| ~ sP80 )
& ( ~ xsd_integer(sK140)
| ~ sP80 )
& ( xsd_integer(sK139)
| ~ sP79 )
& ( xsd_string(sK139)
| ~ sP79 )
& ( ~ 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)
| sP80
| sP79
| cowlNothing(sK138)
| ~ cowlThing(sK137) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP79,sP80])],[f_343_8]) ).
cnf(f_343_10,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)
| sP80
| sP79
| cowlNothing(sK138)
| ~ cowlThing(sK137) ),
inference(clausify,[status(thm)],[f_343_9]) ).
cnf(f_343_11,negated_conjecture,
( xsd_string(sK139)
| ~ sP79 ),
inference(clausify,[status(thm)],[f_343_9]) ).
cnf(f_343_12,negated_conjecture,
( xsd_integer(sK139)
| ~ sP79 ),
inference(clausify,[status(thm)],[f_343_9]) ).
cnf(f_343_13,negated_conjecture,
( ~ xsd_integer(sK140)
| ~ sP80 ),
inference(clausify,[status(thm)],[f_343_9]) ).
cnf(f_343_14,negated_conjecture,
( ~ xsd_string(sK140)
| ~ sP80 ),
inference(clausify,[status(thm)],[f_343_9]) ).
cnf(t1,plain,
( cowlNothing(sK138)
| sP79
| sP80
| ~ 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)
| ~ cowlThing(sK137) ),
inference(start,[status(thm),parent(0:0)],[f_343_10]) ).
cnf(t2,plain,
cowlThing(sK137),
inference(extension,[status(thm),parent(t1:1)],[f_1_5]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
cowlThing(iV21030),
inference(extension,[status(thm),parent(t1:2)],[f_307_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t1:2]) ).
cnf(t6,plain,
( ~ ra_Px21(iV21030,sK112(iV21030))
| cC66(iV21030) ),
inference(extension,[status(thm),parent(t1:3)],[f_150_7]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t1:3]) ).
cnf(t8,plain,
( cC66xcomp(iV21030)
| ra_Px21(iV21030,sK112(iV21030)) ),
inference(extension,[status(thm),parent(t6:2)],[f_152_7]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( cC68(iV21030)
| ~ cC18xcomp(iV21030)
| ~ cC66xcomp(iV21030) ),
inference(extension,[status(thm),parent(t8:2)],[f_154_6]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
cC18xcomp(iV21030),
inference(extension,[status(thm),parent(t10:2)],[f_294_3]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
( cC70(iV21026)
| ~ rR1(iV21026,iV21030)
| ~ cC68(iV21030) ),
inference(extension,[status(thm),parent(t10:3)],[f_156_7]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t10:3]) ).
cnf(t16,plain,
rR1(iV21026,iV21030),
inference(extension,[status(thm),parent(t14:2)],[f_223_3]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
( ~ ra_Px25(iV21026,sK117(iV21026))
| ~ cC70(iV21026) ),
inference(extension,[status(thm),parent(t14:3)],[f_157_6]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t14:3]) ).
cnf(t20,plain,
( ~ cC70xcomp(iV21026)
| ra_Px25(iV21026,sK117(iV21026)) ),
inference(extension,[status(thm),parent(t18:2)],[f_158_6]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
cC70xcomp(iV21026),
inference(extension,[status(thm),parent(t20:2)],[f_216_3]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
( ~ ra_Px24(iV21030,sK120(iV21030))
| cC72(iV21030) ),
inference(extension,[status(thm),parent(t1:4)],[f_159_7]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t1:4]) ).
cnf(t26,plain,
( cC72xcomp(iV21030)
| ra_Px24(iV21030,sK120(iV21030)) ),
inference(extension,[status(thm),parent(t24:2)],[f_161_7]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t24:2]) ).
cnf(t28,plain,
( ~ cC18xcomp(iV21030)
| cC74(iV21030)
| ~ cC72xcomp(iV21030) ),
inference(extension,[status(thm),parent(t26:2)],[f_162_6]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
( cC76(iV21026)
| ~ rR1(iV21026,iV21030)
| ~ cC74(iV21030) ),
inference(extension,[status(thm),parent(t28:2)],[f_165_7]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
rR1(iV21026,iV21030),
inference(extension,[status(thm),parent(t30:2)],[f_223_3]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
( ra_Px26(iV21026,sK124(iV21026))
| ~ cC76(iV21026) ),
inference(extension,[status(thm),parent(t30:3)],[f_166_6]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t30:3]) ).
cnf(t36,plain,
( ~ cC76xcomp(iV21026)
| ~ ra_Px26(iV21026,sK124(iV21026)) ),
inference(extension,[status(thm),parent(t34:2)],[f_167_6]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
cC76xcomp(iV21026),
inference(extension,[status(thm),parent(t36:2)],[f_196_3]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
cnf(t40,plain,
cC18xcomp(iV21030),
inference(extension,[status(thm),parent(t28:3)],[f_294_3]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t28:3]) ).
cnf(t42,plain,
cowlThing(iV21029),
inference(extension,[status(thm),parent(t1:5)],[f_279_3]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t1:5]) ).
cnf(t44,plain,
( ra_Px13(iV21029,sK92(iV21029))
| cC44(iV21029) ),
inference(extension,[status(thm),parent(t1:6)],[f_125_7]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t1:6]) ).
cnf(t46,plain,
( cC44xcomp(iV21029)
| ~ ra_Px13(iV21029,sK92(iV21029)) ),
inference(extension,[status(thm),parent(t44:2)],[f_127_7]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t44:2]) ).
cnf(t48,plain,
( ~ cC12xcomp(iV21029)
| cC46(iV21029)
| ~ cC44xcomp(iV21029) ),
inference(extension,[status(thm),parent(t46:2)],[f_129_6]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(t50,plain,
( cC48(iV21026)
| ~ rR1(iV21026,iV21029)
| ~ cC46(iV21029) ),
inference(extension,[status(thm),parent(t48:2)],[f_132_7]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
rR1(iV21026,iV21029),
inference(extension,[status(thm),parent(t50:2)],[f_226_3]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t50:2]) ).
cnf(t54,plain,
( sP55(iV21026)
| ~ cC48(iV21026) ),
inference(extension,[status(thm),parent(t50:3)],[f_132_6]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t50:3]) ).
cnf(t56,plain,
( cC46(sK98(iV21026))
| ~ sP55(iV21026) ),
inference(extension,[status(thm),parent(t54:2)],[f_132_9]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(t58,plain,
( ra_Px90(sK98(iV21026),sK95(sK98(iV21026)))
| ~ cC46(sK98(iV21026)) ),
inference(extension,[status(thm),parent(t56:2)],[f_128_6]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t56:2]) ).
cnf(t60,plain,
( ~ cC46xcomp(sK98(iV21026))
| ~ ra_Px90(sK98(iV21026),sK95(sK98(iV21026))) ),
inference(extension,[status(thm),parent(t58:2)],[f_130_6]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
( ~ rR1(iV21026,sK98(iV21026))
| cC46xcomp(sK98(iV21026)) ),
inference(extension,[status(thm),parent(t60:2)],[f_190_4]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t60:2]) ).
cnf(t64,plain,
( ~ sP55(iV21026)
| rR1(iV21026,sK98(iV21026)) ),
inference(extension,[status(thm),parent(t62:2)],[f_132_8]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
$false,
inference(reduction,[status(thm),parent(t64:2)],[t64:2,t54:2]) ).
cnf(t67,plain,
cC12xcomp(iV21029),
inference(extension,[status(thm),parent(t48:3)],[f_266_3]) ).
cnf(t68,plain,
$false,
inference(connection,[status(thm),parent(t67:1)],[t67:1,t48:3]) ).
cnf(t69,plain,
( ra_Px16(iV21029,sK101(iV21029))
| cC50(iV21029) ),
inference(extension,[status(thm),parent(t1:7)],[f_135_7]) ).
cnf(t70,plain,
$false,
inference(connection,[status(thm),parent(t69:1)],[t69:1,t1:7]) ).
cnf(t71,plain,
( cC50xcomp(iV21029)
| ~ ra_Px16(iV21029,sK101(iV21029)) ),
inference(extension,[status(thm),parent(t69:2)],[f_136_7]) ).
cnf(t72,plain,
$false,
inference(connection,[status(thm),parent(t71:1)],[t71:1,t69:2]) ).
cnf(t73,plain,
( ~ cC12xcomp(iV21029)
| cC52(iV21029)
| ~ cC50xcomp(iV21029) ),
inference(extension,[status(thm),parent(t71:2)],[f_138_6]) ).
cnf(t74,plain,
$false,
inference(connection,[status(thm),parent(t73:1)],[t73:1,t71:2]) ).
cnf(t75,plain,
( cC54(iV21026)
| ~ rR1(iV21026,iV21029)
| ~ cC52(iV21029) ),
inference(extension,[status(thm),parent(t73:2)],[f_140_7]) ).
cnf(t76,plain,
$false,
inference(connection,[status(thm),parent(t75:1)],[t75:1,t73:2]) ).
cnf(t77,plain,
rR1(iV21026,iV21029),
inference(extension,[status(thm),parent(t75:2)],[f_226_3]) ).
cnf(t78,plain,
$false,
inference(connection,[status(thm),parent(t77:1)],[t77:1,t75:2]) ).
cnf(t79,plain,
( ra_Px18(iV21026,sK106(iV21026))
| ~ cC54(iV21026) ),
inference(extension,[status(thm),parent(t75:3)],[f_141_6]) ).
cnf(t80,plain,
$false,
inference(connection,[status(thm),parent(t79:1)],[t79:1,t75:3]) ).
cnf(t81,plain,
( ~ cC54xcomp(iV21026)
| ~ ra_Px18(iV21026,sK106(iV21026)) ),
inference(extension,[status(thm),parent(t79:2)],[f_142_6]) ).
cnf(t82,plain,
$false,
inference(connection,[status(thm),parent(t81:1)],[t81:1,t79:2]) ).
cnf(t83,plain,
cC54xcomp(iV21026),
inference(extension,[status(thm),parent(t81:2)],[f_210_3]) ).
cnf(t84,plain,
$false,
inference(connection,[status(thm),parent(t83:1)],[t83:1,t81:2]) ).
cnf(t85,plain,
cC12xcomp(iV21029),
inference(extension,[status(thm),parent(t73:3)],[f_266_3]) ).
cnf(t86,plain,
$false,
inference(connection,[status(thm),parent(t85:1)],[t85:1,t73:3]) ).
cnf(t87,plain,
( ~ ra_Px5(iV21027,sK77(iV21027))
| cC24(iV21027) ),
inference(extension,[status(thm),parent(t1:8)],[f_102_7]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t1:8]) ).
cnf(t89,plain,
( cC24xcomp(iV21027)
| ra_Px5(iV21027,sK77(iV21027)) ),
inference(extension,[status(thm),parent(t87:2)],[f_104_7]) ).
cnf(t90,plain,
$false,
inference(connection,[status(thm),parent(t89:1)],[t89:1,t87:2]) ).
cnf(t91,plain,
( ~ cC2xcomp(iV21027)
| cC26(iV21027)
| ~ cC24xcomp(iV21027) ),
inference(extension,[status(thm),parent(t89:2)],[f_106_6]) ).
cnf(t92,plain,
$false,
inference(connection,[status(thm),parent(t91:1)],[t91:1,t89:2]) ).
cnf(t93,plain,
( cC28(iV21026)
| ~ rR1(iV21026,iV21027)
| ~ cC26(iV21027) ),
inference(extension,[status(thm),parent(t91:2)],[f_108_7]) ).
cnf(t94,plain,
$false,
inference(connection,[status(thm),parent(t93:1)],[t93:1,t91:2]) ).
cnf(t95,plain,
rR1(iV21026,iV21027),
inference(extension,[status(thm),parent(t93:2)],[f_224_3]) ).
cnf(t96,plain,
$false,
inference(connection,[status(thm),parent(t95:1)],[t95:1,t93:2]) ).
cnf(t97,plain,
( ra_Px9(iV21026,sK81(iV21026))
| ~ cC28(iV21026) ),
inference(extension,[status(thm),parent(t93:3)],[f_109_6]) ).
cnf(t98,plain,
$false,
inference(connection,[status(thm),parent(t97:1)],[t97:1,t93:3]) ).
cnf(t99,plain,
( ~ cC28xcomp(iV21026)
| ~ ra_Px9(iV21026,sK81(iV21026)) ),
inference(extension,[status(thm),parent(t97:2)],[f_110_6]) ).
cnf(t100,plain,
$false,
inference(connection,[status(thm),parent(t99:1)],[t99:1,t97:2]) ).
cnf(t101,plain,
cC28xcomp(iV21026),
inference(extension,[status(thm),parent(t99:2)],[f_206_3]) ).
cnf(t102,plain,
$false,
inference(connection,[status(thm),parent(t101:1)],[t101:1,t99:2]) ).
cnf(t103,plain,
cC2xcomp(iV21027),
inference(extension,[status(thm),parent(t91:3)],[f_238_3]) ).
cnf(t104,plain,
$false,
inference(connection,[status(thm),parent(t103:1)],[t103:1,t91:3]) ).
cnf(t105,plain,
cowlThing(iV21027),
inference(extension,[status(thm),parent(t1:9)],[f_249_3]) ).
cnf(t106,plain,
$false,
inference(connection,[status(thm),parent(t105:1)],[t105:1,t1:9]) ).
cnf(t107,plain,
( ~ cC12xcomp(iV21035)
| ~ rR1(iV21027,iV21035)
| cC30(iV21027) ),
inference(extension,[status(thm),parent(t1:10)],[f_112_7]) ).
cnf(t108,plain,
$false,
inference(connection,[status(thm),parent(t107:1)],[t107:1,t1:10]) ).
cnf(t109,plain,
rR1(iV21027,iV21035),
inference(extension,[status(thm),parent(t107:2)],[f_254_3]) ).
cnf(t110,plain,
$false,
inference(connection,[status(thm),parent(t109:1)],[t109:1,t107:2]) ).
cnf(t111,plain,
cC12xcomp(iV21035),
inference(extension,[status(thm),parent(t107:3)],[f_332_3]) ).
cnf(t112,plain,
$false,
inference(connection,[status(thm),parent(t111:1)],[t111:1,t107:3]) ).
cnf(t113,plain,
( ~ cC84(iV21026)
| ~ cC82(iV21026)
| cC86(iV21026) ),
inference(extension,[status(thm),parent(t1:11)],[f_173_6]) ).
cnf(t114,plain,
$false,
inference(connection,[status(thm),parent(t113:1)],[t113:1,t1:11]) ).
cnf(t115,plain,
( ~ cC80(iV21026)
| ~ cC64(iV21026)
| cC82(iV21026) ),
inference(extension,[status(thm),parent(t113:2)],[f_171_6]) ).
cnf(t116,plain,
$false,
inference(connection,[status(thm),parent(t115:1)],[t115:1,t113:2]) ).
cnf(t117,plain,
( ~ cC62(iV21026)
| ~ cC60(iV21026)
| cC64(iV21026) ),
inference(extension,[status(thm),parent(t115:2)],[f_149_6]) ).
cnf(t118,plain,
$false,
inference(connection,[status(thm),parent(t117:1)],[t117:1,t115:2]) ).
cnf(t119,plain,
( ~ cC42(iV21026)
| ~ cC58(iV21026)
| cC60(iV21026) ),
inference(extension,[status(thm),parent(t117:2)],[f_147_6]) ).
cnf(t120,plain,
$false,
inference(connection,[status(thm),parent(t119:1)],[t119:1,t117:2]) ).
cnf(t121,plain,
( ~ cTOP(iV21026)
| ~ cC56(iV21026)
| cC58(iV21026) ),
inference(extension,[status(thm),parent(t119:2)],[f_144_6]) ).
cnf(t122,plain,
$false,
inference(connection,[status(thm),parent(t121:1)],[t121:1,t119:2]) ).
cnf(t123,plain,
( ~ cC54xcomp(iV21026)
| ~ cC48xcomp(iV21026)
| cC56(iV21026) ),
inference(extension,[status(thm),parent(t121:2)],[f_143_6]) ).
cnf(t124,plain,
$false,
inference(connection,[status(thm),parent(t123:1)],[t123:1,t121:2]) ).
cnf(t125,plain,
cC48xcomp(iV21026),
inference(extension,[status(thm),parent(t123:2)],[f_218_3]) ).
cnf(t126,plain,
$false,
inference(connection,[status(thm),parent(t125:1)],[t125:1,t123:2]) ).
cnf(t127,plain,
cC54xcomp(iV21026),
inference(extension,[status(thm),parent(t123:3)],[f_210_3]) ).
cnf(t128,plain,
$false,
inference(connection,[status(thm),parent(t127:1)],[t127:1,t123:3]) ).
cnf(t129,plain,
cTOP(iV21026),
inference(extension,[status(thm),parent(t121:3)],[f_191_3]) ).
cnf(t130,plain,
$false,
inference(connection,[status(thm),parent(t129:1)],[t129:1,t121:3]) ).
cnf(t131,plain,
( ~ cC38(iV21026)
| ~ cC40(iV21026)
| cC42(iV21026) ),
inference(extension,[status(thm),parent(t119:3)],[f_124_6]) ).
cnf(t132,plain,
$false,
inference(connection,[status(thm),parent(t131:1)],[t131:1,t119:3]) ).
cnf(t133,plain,
( ~ cTOP(iV21026)
| cC40(iV21026) ),
inference(extension,[status(thm),parent(t131:2)],[f_123_6]) ).
cnf(t134,plain,
$false,
inference(connection,[status(thm),parent(t133:1)],[t133:1,t131:2]) ).
cnf(t135,plain,
cTOP(iV21026),
inference(extension,[status(thm),parent(t133:2)],[f_191_3]) ).
cnf(t136,plain,
$false,
inference(connection,[status(thm),parent(t135:1)],[t135:1,t133:2]) ).
cnf(t137,plain,
( ~ cTOP(iV21026)
| ~ cC36(iV21026)
| cC38(iV21026) ),
inference(extension,[status(thm),parent(t131:3)],[f_121_6]) ).
cnf(t138,plain,
$false,
inference(connection,[status(thm),parent(t137:1)],[t137:1,t131:3]) ).
cnf(t139,plain,
( ~ cC28xcomp(iV21026)
| ~ cC34xcomp(iV21026)
| cC36(iV21026) ),
inference(extension,[status(thm),parent(t137:2)],[f_120_6]) ).
cnf(t140,plain,
$false,
inference(connection,[status(thm),parent(t139:1)],[t139:1,t137:2]) ).
cnf(t141,plain,
cC34xcomp(iV21026),
inference(extension,[status(thm),parent(t139:2)],[f_204_3]) ).
cnf(t142,plain,
$false,
inference(connection,[status(thm),parent(t141:1)],[t141:1,t139:2]) ).
cnf(t143,plain,
cC28xcomp(iV21026),
inference(extension,[status(thm),parent(t139:3)],[f_206_3]) ).
cnf(t144,plain,
$false,
inference(connection,[status(thm),parent(t143:1)],[t143:1,t139:3]) ).
cnf(t145,plain,
cTOP(iV21026),
inference(extension,[status(thm),parent(t137:3)],[f_191_3]) ).
cnf(t146,plain,
$false,
inference(connection,[status(thm),parent(t145:1)],[t145:1,t137:3]) ).
cnf(t147,plain,
( ~ cTOP(iV21026)
| cC62(iV21026) ),
inference(extension,[status(thm),parent(t117:3)],[f_148_6]) ).
cnf(t148,plain,
$false,
inference(connection,[status(thm),parent(t147:1)],[t147:1,t117:3]) ).
cnf(t149,plain,
cTOP(iV21026),
inference(extension,[status(thm),parent(t147:2)],[f_191_3]) ).
cnf(t150,plain,
$false,
inference(connection,[status(thm),parent(t149:1)],[t149:1,t147:2]) ).
cnf(t151,plain,
( ~ cTOP(iV21026)
| ~ cC78(iV21026)
| cC80(iV21026) ),
inference(extension,[status(thm),parent(t115:3)],[f_170_6]) ).
cnf(t152,plain,
$false,
inference(connection,[status(thm),parent(t151:1)],[t151:1,t115:3]) ).
cnf(t153,plain,
( ~ cC76xcomp(iV21026)
| ~ cC70xcomp(iV21026)
| cC78(iV21026) ),
inference(extension,[status(thm),parent(t151:2)],[f_168_6]) ).
cnf(t154,plain,
$false,
inference(connection,[status(thm),parent(t153:1)],[t153:1,t151:2]) ).
cnf(t155,plain,
cC70xcomp(iV21026),
inference(extension,[status(thm),parent(t153:2)],[f_216_3]) ).
cnf(t156,plain,
$false,
inference(connection,[status(thm),parent(t155:1)],[t155:1,t153:2]) ).
cnf(t157,plain,
cC76xcomp(iV21026),
inference(extension,[status(thm),parent(t153:3)],[f_196_3]) ).
cnf(t158,plain,
$false,
inference(connection,[status(thm),parent(t157:1)],[t157:1,t153:3]) ).
cnf(t159,plain,
cTOP(iV21026),
inference(extension,[status(thm),parent(t151:3)],[f_191_3]) ).
cnf(t160,plain,
$false,
inference(connection,[status(thm),parent(t159:1)],[t159:1,t151:3]) ).
cnf(t161,plain,
( ~ cTOP(iV21026)
| cC84(iV21026) ),
inference(extension,[status(thm),parent(t113:3)],[f_172_6]) ).
cnf(t162,plain,
$false,
inference(connection,[status(thm),parent(t161:1)],[t161:1,t113:3]) ).
cnf(t163,plain,
cTOP(iV21026),
inference(extension,[status(thm),parent(t161:2)],[f_191_3]) ).
cnf(t164,plain,
$false,
inference(connection,[status(thm),parent(t163:1)],[t163:1,t161:2]) ).
cnf(l57,lemma,
cC86(iV21026),
inference(lemma,[status(cth),parent(t1:11),below(0:0)],[t1:11]) ).
cnf(t165,plain,
( ~ sP28(iV21026)
| cC156(iV21026) ),
inference(extension,[status(thm),parent(t1:12)],[f_67_8]) ).
cnf(t166,plain,
$false,
inference(connection,[status(thm),parent(t165:1)],[t165:1,t1:12]) ).
cnf(t167,plain,
( ~ cC158(iV21026)
| sP28(iV21026) ),
inference(extension,[status(thm),parent(t165:2)],[f_67_5]) ).
cnf(t168,plain,
$false,
inference(connection,[status(thm),parent(t167:1)],[t167:1,t165:2]) ).
cnf(t169,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t167:2)],[f_187_7]) ).
cnf(t170,plain,
$false,
inference(connection,[status(thm),parent(t169:1)],[t169:1,t167:2]) ).
cnf(t171,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t169:2)],[f_187_5]) ).
cnf(t172,plain,
$false,
inference(connection,[status(thm),parent(t171:1)],[t171:1,t169:2]) ).
cnf(t173,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t171:2)],[f_222_3]) ).
cnf(t174,plain,
$false,
inference(connection,[status(thm),parent(t173:1)],[t173:1,t171:2]) ).
cnf(l83,lemma,
cC156(iV21026),
inference(lemma,[status(cth),parent(t1:12),below(0:0)],[t1:12]) ).
cnf(t175,plain,
( ~ sP61(iV21026)
| cC42(iV21026) ),
inference(extension,[status(thm),parent(t1:13)],[f_147_8]) ).
cnf(t176,plain,
$false,
inference(connection,[status(thm),parent(t175:1)],[t175:1,t1:13]) ).
cnf(t177,plain,
( ~ cC60(iV21026)
| sP61(iV21026) ),
inference(extension,[status(thm),parent(t175:2)],[f_147_5]) ).
cnf(t178,plain,
$false,
inference(connection,[status(thm),parent(t177:1)],[t177:1,t175:2]) ).
cnf(t179,plain,
( ~ sP62(iV21026)
| cC60(iV21026) ),
inference(extension,[status(thm),parent(t177:2)],[f_149_7]) ).
cnf(t180,plain,
$false,
inference(connection,[status(thm),parent(t179:1)],[t179:1,t177:2]) ).
cnf(t181,plain,
( ~ cC64(iV21026)
| sP62(iV21026) ),
inference(extension,[status(thm),parent(t179:2)],[f_149_5]) ).
cnf(t182,plain,
$false,
inference(connection,[status(thm),parent(t181:1)],[t181:1,t179:2]) ).
cnf(t183,plain,
( ~ sP72(iV21026)
| cC64(iV21026) ),
inference(extension,[status(thm),parent(t181:2)],[f_171_7]) ).
cnf(t184,plain,
$false,
inference(connection,[status(thm),parent(t183:1)],[t183:1,t181:2]) ).
cnf(t185,plain,
( ~ cC82(iV21026)
| sP72(iV21026) ),
inference(extension,[status(thm),parent(t183:2)],[f_171_5]) ).
cnf(t186,plain,
$false,
inference(connection,[status(thm),parent(t185:1)],[t185:1,t183:2]) ).
cnf(t187,plain,
( ~ sP73(iV21026)
| cC82(iV21026) ),
inference(extension,[status(thm),parent(t185:2)],[f_173_7]) ).
cnf(t188,plain,
$false,
inference(connection,[status(thm),parent(t187:1)],[t187:1,t185:2]) ).
cnf(t189,plain,
( ~ cC86(iV21026)
| sP73(iV21026) ),
inference(extension,[status(thm),parent(t187:2)],[f_173_5]) ).
cnf(t190,plain,
$false,
inference(connection,[status(thm),parent(t189:1)],[t189:1,t187:2]) ).
cnf(t191,plain,
cC86(iV21026),
inference(lemma_extension,[status(thm),parent(t189:2)],[l57:1]) ).
cnf(t192,plain,
$false,
inference(connection,[status(thm),parent(t191:1)],[t191:1,t189:2]) ).
cnf(l88,lemma,
cC42(iV21026),
inference(lemma,[status(cth),parent(t1:13),below(0:0)],[t1:13]) ).
cnf(t193,plain,
( ~ sP17(iV21026)
| cC134(iV21026) ),
inference(extension,[status(thm),parent(t1:14)],[f_44_8]) ).
cnf(t194,plain,
$false,
inference(connection,[status(thm),parent(t193:1)],[t193:1,t1:14]) ).
cnf(t195,plain,
( ~ cC138(iV21026)
| sP17(iV21026) ),
inference(extension,[status(thm),parent(t193:2)],[f_44_5]) ).
cnf(t196,plain,
$false,
inference(connection,[status(thm),parent(t195:1)],[t195:1,t193:2]) ).
cnf(t197,plain,
( ~ sP27(iV21026)
| cC138(iV21026) ),
inference(extension,[status(thm),parent(t195:2)],[f_66_8]) ).
cnf(t198,plain,
$false,
inference(connection,[status(thm),parent(t197:1)],[t197:1,t195:2]) ).
cnf(t199,plain,
( ~ cC156(iV21026)
| sP27(iV21026) ),
inference(extension,[status(thm),parent(t197:2)],[f_66_5]) ).
cnf(t200,plain,
$false,
inference(connection,[status(thm),parent(t199:1)],[t199:1,t197:2]) ).
cnf(t201,plain,
cC156(iV21026),
inference(lemma_extension,[status(thm),parent(t199:2)],[l83:1]) ).
cnf(t202,plain,
$false,
inference(connection,[status(thm),parent(t201:1)],[t201:1,t199:2]) ).
cnf(l96,lemma,
cC134(iV21026),
inference(lemma,[status(cth),parent(t1:14),below(0:0)],[t1:14]) ).
cnf(t203,plain,
( ~ sP0(iV21026)
| cC4(iV21026) ),
inference(extension,[status(thm),parent(t1:15)],[f_3_8]) ).
cnf(t204,plain,
$false,
inference(connection,[status(thm),parent(t203:1)],[t203:1,t1:15]) ).
cnf(t205,plain,
( ~ cC10(iV21026)
| sP0(iV21026) ),
inference(extension,[status(thm),parent(t203:2)],[f_3_5]) ).
cnf(t206,plain,
$false,
inference(connection,[status(thm),parent(t205:1)],[t205:1,t203:2]) ).
cnf(t207,plain,
( ~ sP29(iV21026)
| cC10(iV21026) ),
inference(extension,[status(thm),parent(t205:2)],[f_68_7]) ).
cnf(t208,plain,
$false,
inference(connection,[status(thm),parent(t207:1)],[t207:1,t205:2]) ).
cnf(t209,plain,
( ~ cC16(iV21026)
| sP29(iV21026) ),
inference(extension,[status(thm),parent(t207:2)],[f_68_5]) ).
cnf(t210,plain,
$false,
inference(connection,[status(thm),parent(t209:1)],[t209:1,t207:2]) ).
cnf(t211,plain,
( ~ sP42(iV21026)
| cC16(iV21026) ),
inference(extension,[status(thm),parent(t209:2)],[f_101_8]) ).
cnf(t212,plain,
$false,
inference(connection,[status(thm),parent(t211:1)],[t211:1,t209:2]) ).
cnf(t213,plain,
( ~ cC22(iV21026)
| sP42(iV21026) ),
inference(extension,[status(thm),parent(t211:2)],[f_101_5]) ).
cnf(t214,plain,
$false,
inference(connection,[status(thm),parent(t213:1)],[t213:1,t211:2]) ).
cnf(t215,plain,
( ~ sP28(iV21026)
| cC22(iV21026) ),
inference(extension,[status(thm),parent(t213:2)],[f_67_7]) ).
cnf(t216,plain,
$false,
inference(connection,[status(thm),parent(t215:1)],[t215:1,t213:2]) ).
cnf(t217,plain,
( ~ cC158(iV21026)
| sP28(iV21026) ),
inference(extension,[status(thm),parent(t215:2)],[f_67_5]) ).
cnf(t218,plain,
$false,
inference(connection,[status(thm),parent(t217:1)],[t217:1,t215:2]) ).
cnf(t219,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t217:2)],[f_187_7]) ).
cnf(t220,plain,
$false,
inference(connection,[status(thm),parent(t219:1)],[t219:1,t217:2]) ).
cnf(t221,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t219:2)],[f_187_5]) ).
cnf(t222,plain,
$false,
inference(connection,[status(thm),parent(t221:1)],[t221:1,t219:2]) ).
cnf(t223,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t221:2)],[f_222_3]) ).
cnf(t224,plain,
$false,
inference(connection,[status(thm),parent(t223:1)],[t223:1,t221:2]) ).
cnf(t225,plain,
( ~ sP37(iV21026)
| cC168(iV21026) ),
inference(extension,[status(thm),parent(t1:16)],[f_88_8]) ).
cnf(t226,plain,
$false,
inference(connection,[status(thm),parent(t225:1)],[t225:1,t1:16]) ).
cnf(t227,plain,
( ~ cC174(iV21026)
| sP37(iV21026) ),
inference(extension,[status(thm),parent(t225:2)],[f_88_5]) ).
cnf(t228,plain,
$false,
inference(connection,[status(thm),parent(t227:1)],[t227:1,t225:2]) ).
cnf(t229,plain,
( ~ sP40(iV21026)
| cC174(iV21026) ),
inference(extension,[status(thm),parent(t227:2)],[f_97_7]) ).
cnf(t230,plain,
$false,
inference(connection,[status(thm),parent(t229:1)],[t229:1,t227:2]) ).
cnf(t231,plain,
( ~ cC180(iV21026)
| sP40(iV21026) ),
inference(extension,[status(thm),parent(t229:2)],[f_97_5]) ).
cnf(t232,plain,
$false,
inference(connection,[status(thm),parent(t231:1)],[t231:1,t229:2]) ).
cnf(t233,plain,
( ~ sP78(iV21026)
| cC180(iV21026) ),
inference(extension,[status(thm),parent(t231:2)],[f_187_8]) ).
cnf(t234,plain,
$false,
inference(connection,[status(thm),parent(t233:1)],[t233:1,t231:2]) ).
cnf(t235,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t233:2)],[f_187_5]) ).
cnf(t236,plain,
$false,
inference(connection,[status(thm),parent(t235:1)],[t235:1,t233:2]) ).
cnf(t237,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t235:2)],[f_222_3]) ).
cnf(t238,plain,
$false,
inference(connection,[status(thm),parent(t237:1)],[t237:1,t235:2]) ).
cnf(t239,plain,
( ~ sP15(iV21026)
| cC130(iV21026) ),
inference(extension,[status(thm),parent(t1:17)],[f_41_7]) ).
cnf(t240,plain,
$false,
inference(connection,[status(thm),parent(t239:1)],[t239:1,t1:17]) ).
cnf(t241,plain,
( ~ cC132(iV21026)
| sP15(iV21026) ),
inference(extension,[status(thm),parent(t239:2)],[f_41_5]) ).
cnf(t242,plain,
$false,
inference(connection,[status(thm),parent(t241:1)],[t241:1,t239:2]) ).
cnf(t243,plain,
( ~ sP16(iV21026)
| cC132(iV21026) ),
inference(extension,[status(thm),parent(t241:2)],[f_42_8]) ).
cnf(t244,plain,
$false,
inference(connection,[status(thm),parent(t243:1)],[t243:1,t241:2]) ).
cnf(t245,plain,
( ~ cC134(iV21026)
| sP16(iV21026) ),
inference(extension,[status(thm),parent(t243:2)],[f_42_5]) ).
cnf(t246,plain,
$false,
inference(connection,[status(thm),parent(t245:1)],[t245:1,t243:2]) ).
cnf(t247,plain,
cC134(iV21026),
inference(lemma_extension,[status(thm),parent(t245:2)],[l96:1]) ).
cnf(t248,plain,
$false,
inference(connection,[status(thm),parent(t247:1)],[t247:1,t245:2]) ).
cnf(t249,plain,
( ~ sP74(iV21026)
| cC88(iV21026) ),
inference(extension,[status(thm),parent(t1:18)],[f_175_8]) ).
cnf(t250,plain,
$false,
inference(connection,[status(thm),parent(t249:1)],[t249:1,t1:18]) ).
cnf(t251,plain,
( ~ cC90(iV21026)
| sP74(iV21026) ),
inference(extension,[status(thm),parent(t249:2)],[f_175_5]) ).
cnf(t252,plain,
$false,
inference(connection,[status(thm),parent(t251:1)],[t251:1,t249:2]) ).
cnf(t253,plain,
( ~ sP6(iV21026)
| cC90(iV21026) ),
inference(extension,[status(thm),parent(t251:2)],[f_17_8]) ).
cnf(t254,plain,
$false,
inference(connection,[status(thm),parent(t253:1)],[t253:1,t251:2]) ).
cnf(t255,plain,
( ~ cC112(iV21026)
| sP6(iV21026) ),
inference(extension,[status(thm),parent(t253:2)],[f_17_5]) ).
cnf(t256,plain,
$false,
inference(connection,[status(thm),parent(t255:1)],[t255:1,t253:2]) ).
cnf(t257,plain,
( ~ sP7(iV21026)
| cC112(iV21026) ),
inference(extension,[status(thm),parent(t255:2)],[f_19_8]) ).
cnf(t258,plain,
$false,
inference(connection,[status(thm),parent(t257:1)],[t257:1,t255:2]) ).
cnf(t259,plain,
( ~ cC116(iV21026)
| sP7(iV21026) ),
inference(extension,[status(thm),parent(t257:2)],[f_19_5]) ).
cnf(t260,plain,
$false,
inference(connection,[status(thm),parent(t259:1)],[t259:1,t257:2]) ).
cnf(t261,plain,
( ~ sP16(iV21026)
| cC116(iV21026) ),
inference(extension,[status(thm),parent(t259:2)],[f_42_7]) ).
cnf(t262,plain,
$false,
inference(connection,[status(thm),parent(t261:1)],[t261:1,t259:2]) ).
cnf(t263,plain,
( ~ cC134(iV21026)
| sP16(iV21026) ),
inference(extension,[status(thm),parent(t261:2)],[f_42_5]) ).
cnf(t264,plain,
$false,
inference(connection,[status(thm),parent(t263:1)],[t263:1,t261:2]) ).
cnf(t265,plain,
cC134(iV21026),
inference(lemma_extension,[status(thm),parent(t263:2)],[l96:1]) ).
cnf(t266,plain,
$false,
inference(connection,[status(thm),parent(t265:1)],[t265:1,t263:2]) ).
cnf(l122,lemma,
cC88(iV21026),
inference(lemma,[status(cth),parent(t1:18),below(0:0)],[t1:18]) ).
cnf(t267,plain,
( ~ sP72(iV21026)
| cC80(iV21026) ),
inference(extension,[status(thm),parent(t1:19)],[f_171_8]) ).
cnf(t268,plain,
$false,
inference(connection,[status(thm),parent(t267:1)],[t267:1,t1:19]) ).
cnf(t269,plain,
( ~ cC82(iV21026)
| sP72(iV21026) ),
inference(extension,[status(thm),parent(t267:2)],[f_171_5]) ).
cnf(t270,plain,
$false,
inference(connection,[status(thm),parent(t269:1)],[t269:1,t267:2]) ).
cnf(t271,plain,
( ~ sP73(iV21026)
| cC82(iV21026) ),
inference(extension,[status(thm),parent(t269:2)],[f_173_7]) ).
cnf(t272,plain,
$false,
inference(connection,[status(thm),parent(t271:1)],[t271:1,t269:2]) ).
cnf(t273,plain,
( ~ cC86(iV21026)
| sP73(iV21026) ),
inference(extension,[status(thm),parent(t271:2)],[f_173_5]) ).
cnf(t274,plain,
$false,
inference(connection,[status(thm),parent(t273:1)],[t273:1,t271:2]) ).
cnf(t275,plain,
cC86(iV21026),
inference(lemma_extension,[status(thm),parent(t273:2)],[l57:1]) ).
cnf(t276,plain,
$false,
inference(connection,[status(thm),parent(t275:1)],[t275:1,t273:2]) ).
cnf(l130,lemma,
cC80(iV21026),
inference(lemma,[status(cth),parent(t1:19),below(0:0)],[t1:19]) ).
cnf(t277,plain,
( ~ sP26(iV21026)
| cC152(iV21026) ),
inference(extension,[status(thm),parent(t1:20)],[f_65_7]) ).
cnf(t278,plain,
$false,
inference(connection,[status(thm),parent(t277:1)],[t277:1,t1:20]) ).
cnf(t279,plain,
( ~ cC154(iV21026)
| sP26(iV21026) ),
inference(extension,[status(thm),parent(t277:2)],[f_65_5]) ).
cnf(t280,plain,
$false,
inference(connection,[status(thm),parent(t279:1)],[t279:1,t277:2]) ).
cnf(t281,plain,
( ~ sP27(iV21026)
| cC154(iV21026) ),
inference(extension,[status(thm),parent(t279:2)],[f_66_7]) ).
cnf(t282,plain,
$false,
inference(connection,[status(thm),parent(t281:1)],[t281:1,t279:2]) ).
cnf(t283,plain,
( ~ cC156(iV21026)
| sP27(iV21026) ),
inference(extension,[status(thm),parent(t281:2)],[f_66_5]) ).
cnf(t284,plain,
$false,
inference(connection,[status(thm),parent(t283:1)],[t283:1,t281:2]) ).
cnf(t285,plain,
cC156(iV21026),
inference(lemma_extension,[status(thm),parent(t283:2)],[l83:1]) ).
cnf(t286,plain,
$false,
inference(connection,[status(thm),parent(t285:1)],[t285:1,t283:2]) ).
cnf(t287,plain,
( ~ sP29(iV21026)
| cC14(iV21026) ),
inference(extension,[status(thm),parent(t1:21)],[f_68_8]) ).
cnf(t288,plain,
$false,
inference(connection,[status(thm),parent(t287:1)],[t287:1,t1:21]) ).
cnf(t289,plain,
( ~ cC16(iV21026)
| sP29(iV21026) ),
inference(extension,[status(thm),parent(t287:2)],[f_68_5]) ).
cnf(t290,plain,
$false,
inference(connection,[status(thm),parent(t289:1)],[t289:1,t287:2]) ).
cnf(t291,plain,
( ~ sP42(iV21026)
| cC16(iV21026) ),
inference(extension,[status(thm),parent(t289:2)],[f_101_8]) ).
cnf(t292,plain,
$false,
inference(connection,[status(thm),parent(t291:1)],[t291:1,t289:2]) ).
cnf(t293,plain,
( ~ cC22(iV21026)
| sP42(iV21026) ),
inference(extension,[status(thm),parent(t291:2)],[f_101_5]) ).
cnf(t294,plain,
$false,
inference(connection,[status(thm),parent(t293:1)],[t293:1,t291:2]) ).
cnf(t295,plain,
( ~ sP28(iV21026)
| cC22(iV21026) ),
inference(extension,[status(thm),parent(t293:2)],[f_67_7]) ).
cnf(t296,plain,
$false,
inference(connection,[status(thm),parent(t295:1)],[t295:1,t293:2]) ).
cnf(t297,plain,
( ~ cC158(iV21026)
| sP28(iV21026) ),
inference(extension,[status(thm),parent(t295:2)],[f_67_5]) ).
cnf(t298,plain,
$false,
inference(connection,[status(thm),parent(t297:1)],[t297:1,t295:2]) ).
cnf(t299,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t297:2)],[f_187_7]) ).
cnf(t300,plain,
$false,
inference(connection,[status(thm),parent(t299:1)],[t299:1,t297:2]) ).
cnf(t301,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t299:2)],[f_187_5]) ).
cnf(t302,plain,
$false,
inference(connection,[status(thm),parent(t301:1)],[t301:1,t299:2]) ).
cnf(t303,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t301:2)],[f_222_3]) ).
cnf(t304,plain,
$false,
inference(connection,[status(thm),parent(t303:1)],[t303:1,t301:2]) ).
cnf(t305,plain,
( ~ sP73(iV21026)
| cC82(iV21026) ),
inference(extension,[status(thm),parent(t1:22)],[f_173_7]) ).
cnf(t306,plain,
$false,
inference(connection,[status(thm),parent(t305:1)],[t305:1,t1:22]) ).
cnf(t307,plain,
( ~ cC86(iV21026)
| sP73(iV21026) ),
inference(extension,[status(thm),parent(t305:2)],[f_173_5]) ).
cnf(t308,plain,
$false,
inference(connection,[status(thm),parent(t307:1)],[t307:1,t305:2]) ).
cnf(t309,plain,
cC86(iV21026),
inference(lemma_extension,[status(thm),parent(t307:2)],[l57:1]) ).
cnf(t310,plain,
$false,
inference(connection,[status(thm),parent(t309:1)],[t309:1,t307:2]) ).
cnf(l147,lemma,
cC82(iV21026),
inference(lemma,[status(cth),parent(t1:22),below(0:0)],[t1:22]) ).
cnf(t311,plain,
( ~ sP16(iV21026)
| cC116(iV21026) ),
inference(extension,[status(thm),parent(t1:23)],[f_42_7]) ).
cnf(t312,plain,
$false,
inference(connection,[status(thm),parent(t311:1)],[t311:1,t1:23]) ).
cnf(t313,plain,
( ~ cC134(iV21026)
| sP16(iV21026) ),
inference(extension,[status(thm),parent(t311:2)],[f_42_5]) ).
cnf(t314,plain,
$false,
inference(connection,[status(thm),parent(t313:1)],[t313:1,t311:2]) ).
cnf(t315,plain,
cC134(iV21026),
inference(lemma_extension,[status(thm),parent(t313:2)],[l96:1]) ).
cnf(t316,plain,
$false,
inference(connection,[status(thm),parent(t315:1)],[t315:1,t313:2]) ).
cnf(l149,lemma,
cC116(iV21026),
inference(lemma,[status(cth),parent(t1:23),below(0:0)],[t1:23]) ).
cnf(t317,plain,
( ~ sP72(iV21026)
| cC64(iV21026) ),
inference(extension,[status(thm),parent(t1:24)],[f_171_7]) ).
cnf(t318,plain,
$false,
inference(connection,[status(thm),parent(t317:1)],[t317:1,t1:24]) ).
cnf(t319,plain,
( ~ cC82(iV21026)
| sP72(iV21026) ),
inference(extension,[status(thm),parent(t317:2)],[f_171_5]) ).
cnf(t320,plain,
$false,
inference(connection,[status(thm),parent(t319:1)],[t319:1,t317:2]) ).
cnf(t321,plain,
cC82(iV21026),
inference(lemma_extension,[status(thm),parent(t319:2)],[l147:1]) ).
cnf(t322,plain,
$false,
inference(connection,[status(thm),parent(t321:1)],[t321:1,t319:2]) ).
cnf(l151,lemma,
cC64(iV21026),
inference(lemma,[status(cth),parent(t1:24),below(0:0)],[t1:24]) ).
cnf(t323,plain,
( ~ sP7(iV21026)
| cC112(iV21026) ),
inference(extension,[status(thm),parent(t1:25)],[f_19_8]) ).
cnf(t324,plain,
$false,
inference(connection,[status(thm),parent(t323:1)],[t323:1,t1:25]) ).
cnf(t325,plain,
( ~ cC116(iV21026)
| sP7(iV21026) ),
inference(extension,[status(thm),parent(t323:2)],[f_19_5]) ).
cnf(t326,plain,
$false,
inference(connection,[status(thm),parent(t325:1)],[t325:1,t323:2]) ).
cnf(t327,plain,
cC116(iV21026),
inference(lemma_extension,[status(thm),parent(t325:2)],[l149:1]) ).
cnf(t328,plain,
$false,
inference(connection,[status(thm),parent(t327:1)],[t327:1,t325:2]) ).
cnf(l153,lemma,
cC112(iV21026),
inference(lemma,[status(cth),parent(t1:25),below(0:0)],[t1:25]) ).
cnf(t329,plain,
( ~ sP50(iV21026)
| cC36(iV21026) ),
inference(extension,[status(thm),parent(t1:26)],[f_121_7]) ).
cnf(t330,plain,
$false,
inference(connection,[status(thm),parent(t329:1)],[t329:1,t1:26]) ).
cnf(t331,plain,
( ~ cC38(iV21026)
| sP50(iV21026) ),
inference(extension,[status(thm),parent(t329:2)],[f_121_5]) ).
cnf(t332,plain,
$false,
inference(connection,[status(thm),parent(t331:1)],[t331:1,t329:2]) ).
cnf(t333,plain,
( ~ sP52(iV21026)
| cC38(iV21026) ),
inference(extension,[status(thm),parent(t331:2)],[f_124_8]) ).
cnf(t334,plain,
$false,
inference(connection,[status(thm),parent(t333:1)],[t333:1,t331:2]) ).
cnf(t335,plain,
( ~ cC42(iV21026)
| sP52(iV21026) ),
inference(extension,[status(thm),parent(t333:2)],[f_124_5]) ).
cnf(t336,plain,
$false,
inference(connection,[status(thm),parent(t335:1)],[t335:1,t333:2]) ).
cnf(t337,plain,
cC42(iV21026),
inference(lemma_extension,[status(thm),parent(t335:2)],[l88:1]) ).
cnf(t338,plain,
$false,
inference(connection,[status(thm),parent(t337:1)],[t337:1,t335:2]) ).
cnf(t339,plain,
( ~ sP0(iV21026)
| cC8(iV21026) ),
inference(extension,[status(thm),parent(t1:27)],[f_3_7]) ).
cnf(t340,plain,
$false,
inference(connection,[status(thm),parent(t339:1)],[t339:1,t1:27]) ).
cnf(t341,plain,
( ~ cC10(iV21026)
| sP0(iV21026) ),
inference(extension,[status(thm),parent(t339:2)],[f_3_5]) ).
cnf(t342,plain,
$false,
inference(connection,[status(thm),parent(t341:1)],[t341:1,t339:2]) ).
cnf(t343,plain,
( ~ sP29(iV21026)
| cC10(iV21026) ),
inference(extension,[status(thm),parent(t341:2)],[f_68_7]) ).
cnf(t344,plain,
$false,
inference(connection,[status(thm),parent(t343:1)],[t343:1,t341:2]) ).
cnf(t345,plain,
( ~ cC16(iV21026)
| sP29(iV21026) ),
inference(extension,[status(thm),parent(t343:2)],[f_68_5]) ).
cnf(t346,plain,
$false,
inference(connection,[status(thm),parent(t345:1)],[t345:1,t343:2]) ).
cnf(t347,plain,
( ~ sP42(iV21026)
| cC16(iV21026) ),
inference(extension,[status(thm),parent(t345:2)],[f_101_8]) ).
cnf(t348,plain,
$false,
inference(connection,[status(thm),parent(t347:1)],[t347:1,t345:2]) ).
cnf(t349,plain,
( ~ cC22(iV21026)
| sP42(iV21026) ),
inference(extension,[status(thm),parent(t347:2)],[f_101_5]) ).
cnf(t350,plain,
$false,
inference(connection,[status(thm),parent(t349:1)],[t349:1,t347:2]) ).
cnf(t351,plain,
( ~ sP28(iV21026)
| cC22(iV21026) ),
inference(extension,[status(thm),parent(t349:2)],[f_67_7]) ).
cnf(t352,plain,
$false,
inference(connection,[status(thm),parent(t351:1)],[t351:1,t349:2]) ).
cnf(t353,plain,
( ~ cC158(iV21026)
| sP28(iV21026) ),
inference(extension,[status(thm),parent(t351:2)],[f_67_5]) ).
cnf(t354,plain,
$false,
inference(connection,[status(thm),parent(t353:1)],[t353:1,t351:2]) ).
cnf(t355,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t353:2)],[f_187_7]) ).
cnf(t356,plain,
$false,
inference(connection,[status(thm),parent(t355:1)],[t355:1,t353:2]) ).
cnf(t357,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t355:2)],[f_187_5]) ).
cnf(t358,plain,
$false,
inference(connection,[status(thm),parent(t357:1)],[t357:1,t355:2]) ).
cnf(t359,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t357:2)],[f_222_3]) ).
cnf(t360,plain,
$false,
inference(connection,[status(thm),parent(t359:1)],[t359:1,t357:2]) ).
cnf(t361,plain,
( ~ sP62(iV21026)
| cC62(iV21026) ),
inference(extension,[status(thm),parent(t1:28)],[f_149_8]) ).
cnf(t362,plain,
$false,
inference(connection,[status(thm),parent(t361:1)],[t361:1,t1:28]) ).
cnf(t363,plain,
( ~ cC64(iV21026)
| sP62(iV21026) ),
inference(extension,[status(thm),parent(t361:2)],[f_149_5]) ).
cnf(t364,plain,
$false,
inference(connection,[status(thm),parent(t363:1)],[t363:1,t361:2]) ).
cnf(t365,plain,
cC64(iV21026),
inference(lemma_extension,[status(thm),parent(t363:2)],[l151:1]) ).
cnf(t366,plain,
$false,
inference(connection,[status(thm),parent(t365:1)],[t365:1,t363:2]) ).
cnf(t367,plain,
( ~ sP40(iV21026)
| cC174(iV21026) ),
inference(extension,[status(thm),parent(t1:29)],[f_97_7]) ).
cnf(t368,plain,
$false,
inference(connection,[status(thm),parent(t367:1)],[t367:1,t1:29]) ).
cnf(t369,plain,
( ~ cC180(iV21026)
| sP40(iV21026) ),
inference(extension,[status(thm),parent(t367:2)],[f_97_5]) ).
cnf(t370,plain,
$false,
inference(connection,[status(thm),parent(t369:1)],[t369:1,t367:2]) ).
cnf(t371,plain,
( ~ sP78(iV21026)
| cC180(iV21026) ),
inference(extension,[status(thm),parent(t369:2)],[f_187_8]) ).
cnf(t372,plain,
$false,
inference(connection,[status(thm),parent(t371:1)],[t371:1,t369:2]) ).
cnf(t373,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t371:2)],[f_187_5]) ).
cnf(t374,plain,
$false,
inference(connection,[status(thm),parent(t373:1)],[t373:1,t371:2]) ).
cnf(t375,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t373:2)],[f_222_3]) ).
cnf(t376,plain,
$false,
inference(connection,[status(thm),parent(t375:1)],[t375:1,t373:2]) ).
cnf(t377,plain,
( ~ sP27(iV21026)
| cC138(iV21026) ),
inference(extension,[status(thm),parent(t1:30)],[f_66_8]) ).
cnf(t378,plain,
$false,
inference(connection,[status(thm),parent(t377:1)],[t377:1,t1:30]) ).
cnf(t379,plain,
( ~ cC156(iV21026)
| sP27(iV21026) ),
inference(extension,[status(thm),parent(t377:2)],[f_66_5]) ).
cnf(t380,plain,
$false,
inference(connection,[status(thm),parent(t379:1)],[t379:1,t377:2]) ).
cnf(t381,plain,
cC156(iV21026),
inference(lemma_extension,[status(thm),parent(t379:2)],[l83:1]) ).
cnf(t382,plain,
$false,
inference(connection,[status(thm),parent(t381:1)],[t381:1,t379:2]) ).
cnf(l177,lemma,
cC138(iV21026),
inference(lemma,[status(cth),parent(t1:30),below(0:0)],[t1:30]) ).
cnf(t383,plain,
( ~ sP52(iV21026)
| cC38(iV21026) ),
inference(extension,[status(thm),parent(t1:31)],[f_124_8]) ).
cnf(t384,plain,
$false,
inference(connection,[status(thm),parent(t383:1)],[t383:1,t1:31]) ).
cnf(t385,plain,
( ~ cC42(iV21026)
| sP52(iV21026) ),
inference(extension,[status(thm),parent(t383:2)],[f_124_5]) ).
cnf(t386,plain,
$false,
inference(connection,[status(thm),parent(t385:1)],[t385:1,t383:2]) ).
cnf(t387,plain,
cC42(iV21026),
inference(lemma_extension,[status(thm),parent(t385:2)],[l88:1]) ).
cnf(t388,plain,
$false,
inference(connection,[status(thm),parent(t387:1)],[t387:1,t385:2]) ).
cnf(t389,plain,
( ~ sP73(iV21026)
| cC84(iV21026) ),
inference(extension,[status(thm),parent(t1:32)],[f_173_8]) ).
cnf(t390,plain,
$false,
inference(connection,[status(thm),parent(t389:1)],[t389:1,t1:32]) ).
cnf(t391,plain,
( ~ cC86(iV21026)
| sP73(iV21026) ),
inference(extension,[status(thm),parent(t389:2)],[f_173_5]) ).
cnf(t392,plain,
$false,
inference(connection,[status(thm),parent(t391:1)],[t391:1,t389:2]) ).
cnf(t393,plain,
cC86(iV21026),
inference(lemma_extension,[status(thm),parent(t391:2)],[l57:1]) ).
cnf(t394,plain,
$false,
inference(connection,[status(thm),parent(t393:1)],[t393:1,t391:2]) ).
cnf(t395,plain,
( ~ sP42(iV21026)
| cC20(iV21026) ),
inference(extension,[status(thm),parent(t1:33)],[f_101_7]) ).
cnf(t396,plain,
$false,
inference(connection,[status(thm),parent(t395:1)],[t395:1,t1:33]) ).
cnf(t397,plain,
( ~ cC22(iV21026)
| sP42(iV21026) ),
inference(extension,[status(thm),parent(t395:2)],[f_101_5]) ).
cnf(t398,plain,
$false,
inference(connection,[status(thm),parent(t397:1)],[t397:1,t395:2]) ).
cnf(t399,plain,
( ~ sP28(iV21026)
| cC22(iV21026) ),
inference(extension,[status(thm),parent(t397:2)],[f_67_7]) ).
cnf(t400,plain,
$false,
inference(connection,[status(thm),parent(t399:1)],[t399:1,t397:2]) ).
cnf(t401,plain,
( ~ cC158(iV21026)
| sP28(iV21026) ),
inference(extension,[status(thm),parent(t399:2)],[f_67_5]) ).
cnf(t402,plain,
$false,
inference(connection,[status(thm),parent(t401:1)],[t401:1,t399:2]) ).
cnf(t403,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t401:2)],[f_187_7]) ).
cnf(t404,plain,
$false,
inference(connection,[status(thm),parent(t403:1)],[t403:1,t401:2]) ).
cnf(t405,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t403:2)],[f_187_5]) ).
cnf(t406,plain,
$false,
inference(connection,[status(thm),parent(t405:1)],[t405:1,t403:2]) ).
cnf(t407,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t405:2)],[f_222_3]) ).
cnf(t408,plain,
$false,
inference(connection,[status(thm),parent(t407:1)],[t407:1,t405:2]) ).
cnf(l183,lemma,
cC20(iV21026),
inference(lemma,[status(cth),parent(t1:33),below(0:0)],[t1:33]) ).
cnf(t409,plain,
( ~ sP7(iV21026)
| cC114(iV21026) ),
inference(extension,[status(thm),parent(t1:34)],[f_19_7]) ).
cnf(t410,plain,
$false,
inference(connection,[status(thm),parent(t409:1)],[t409:1,t1:34]) ).
cnf(t411,plain,
( ~ cC116(iV21026)
| sP7(iV21026) ),
inference(extension,[status(thm),parent(t409:2)],[f_19_5]) ).
cnf(t412,plain,
$false,
inference(connection,[status(thm),parent(t411:1)],[t411:1,t409:2]) ).
cnf(t413,plain,
cC116(iV21026),
inference(lemma_extension,[status(thm),parent(t411:2)],[l149:1]) ).
cnf(t414,plain,
$false,
inference(connection,[status(thm),parent(t413:1)],[t413:1,t411:2]) ).
cnf(t415,plain,
( ~ sP16(iV21026)
| cC132(iV21026) ),
inference(extension,[status(thm),parent(t1:35)],[f_42_8]) ).
cnf(t416,plain,
$false,
inference(connection,[status(thm),parent(t415:1)],[t415:1,t1:35]) ).
cnf(t417,plain,
( ~ cC134(iV21026)
| sP16(iV21026) ),
inference(extension,[status(thm),parent(t415:2)],[f_42_5]) ).
cnf(t418,plain,
$false,
inference(connection,[status(thm),parent(t417:1)],[t417:1,t415:2]) ).
cnf(t419,plain,
cC134(iV21026),
inference(lemma_extension,[status(thm),parent(t417:2)],[l96:1]) ).
cnf(t420,plain,
$false,
inference(connection,[status(thm),parent(t419:1)],[t419:1,t417:2]) ).
cnf(t421,plain,
( ~ sP42(iV21026)
| cC16(iV21026) ),
inference(extension,[status(thm),parent(t1:36)],[f_101_8]) ).
cnf(t422,plain,
$false,
inference(connection,[status(thm),parent(t421:1)],[t421:1,t1:36]) ).
cnf(t423,plain,
( ~ cC22(iV21026)
| sP42(iV21026) ),
inference(extension,[status(thm),parent(t421:2)],[f_101_5]) ).
cnf(t424,plain,
$false,
inference(connection,[status(thm),parent(t423:1)],[t423:1,t421:2]) ).
cnf(t425,plain,
( ~ sP28(iV21026)
| cC22(iV21026) ),
inference(extension,[status(thm),parent(t423:2)],[f_67_7]) ).
cnf(t426,plain,
$false,
inference(connection,[status(thm),parent(t425:1)],[t425:1,t423:2]) ).
cnf(t427,plain,
( ~ cC158(iV21026)
| sP28(iV21026) ),
inference(extension,[status(thm),parent(t425:2)],[f_67_5]) ).
cnf(t428,plain,
$false,
inference(connection,[status(thm),parent(t427:1)],[t427:1,t425:2]) ).
cnf(t429,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t427:2)],[f_187_7]) ).
cnf(t430,plain,
$false,
inference(connection,[status(thm),parent(t429:1)],[t429:1,t427:2]) ).
cnf(t431,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t429:2)],[f_187_5]) ).
cnf(t432,plain,
$false,
inference(connection,[status(thm),parent(t431:1)],[t431:1,t429:2]) ).
cnf(t433,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t431:2)],[f_222_3]) ).
cnf(t434,plain,
$false,
inference(connection,[status(thm),parent(t433:1)],[t433:1,t431:2]) ).
cnf(l194,lemma,
cC16(iV21026),
inference(lemma,[status(cth),parent(t1:36),below(0:0)],[t1:36]) ).
cnf(t435,plain,
( ~ sP71(iV21026)
| cC78(iV21026) ),
inference(extension,[status(thm),parent(t1:37)],[f_170_7]) ).
cnf(t436,plain,
$false,
inference(connection,[status(thm),parent(t435:1)],[t435:1,t1:37]) ).
cnf(t437,plain,
( ~ cC80(iV21026)
| sP71(iV21026) ),
inference(extension,[status(thm),parent(t435:2)],[f_170_5]) ).
cnf(t438,plain,
$false,
inference(connection,[status(thm),parent(t437:1)],[t437:1,t435:2]) ).
cnf(t439,plain,
cC80(iV21026),
inference(lemma_extension,[status(thm),parent(t437:2)],[l130:1]) ).
cnf(t440,plain,
$false,
inference(connection,[status(thm),parent(t439:1)],[t439:1,t437:2]) ).
cnf(t441,plain,
( ~ sP78(iV21026)
| cC180(iV21026) ),
inference(extension,[status(thm),parent(t1:38)],[f_187_8]) ).
cnf(t442,plain,
$false,
inference(connection,[status(thm),parent(t441:1)],[t441:1,t1:38]) ).
cnf(t443,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t441:2)],[f_187_5]) ).
cnf(t444,plain,
$false,
inference(connection,[status(thm),parent(t443:1)],[t443:1,t441:2]) ).
cnf(t445,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t443:2)],[f_222_3]) ).
cnf(t446,plain,
$false,
inference(connection,[status(thm),parent(t445:1)],[t445:1,t443:2]) ).
cnf(t447,plain,
( ~ sP27(iV21026)
| cC154(iV21026) ),
inference(extension,[status(thm),parent(t1:39)],[f_66_7]) ).
cnf(t448,plain,
$false,
inference(connection,[status(thm),parent(t447:1)],[t447:1,t1:39]) ).
cnf(t449,plain,
( ~ cC156(iV21026)
| sP27(iV21026) ),
inference(extension,[status(thm),parent(t447:2)],[f_66_5]) ).
cnf(t450,plain,
$false,
inference(connection,[status(thm),parent(t449:1)],[t449:1,t447:2]) ).
cnf(t451,plain,
cC156(iV21026),
inference(lemma_extension,[status(thm),parent(t449:2)],[l83:1]) ).
cnf(t452,plain,
$false,
inference(connection,[status(thm),parent(t451:1)],[t451:1,t449:2]) ).
cnf(t453,plain,
( ~ sP62(iV21026)
| cC60(iV21026) ),
inference(extension,[status(thm),parent(t1:40)],[f_149_7]) ).
cnf(t454,plain,
$false,
inference(connection,[status(thm),parent(t453:1)],[t453:1,t1:40]) ).
cnf(t455,plain,
( ~ cC64(iV21026)
| sP62(iV21026) ),
inference(extension,[status(thm),parent(t453:2)],[f_149_5]) ).
cnf(t456,plain,
$false,
inference(connection,[status(thm),parent(t455:1)],[t455:1,t453:2]) ).
cnf(t457,plain,
cC64(iV21026),
inference(lemma_extension,[status(thm),parent(t455:2)],[l151:1]) ).
cnf(t458,plain,
$false,
inference(connection,[status(thm),parent(t457:1)],[t457:1,t455:2]) ).
cnf(l208,lemma,
cC60(iV21026),
inference(lemma,[status(cth),parent(t1:40),below(0:0)],[t1:40]) ).
cnf(t459,plain,
( ~ cC16(iV21026)
| ~ cC20(iV21026)
| cC22(iV21026) ),
inference(extension,[status(thm),parent(t1:41)],[f_101_6]) ).
cnf(t460,plain,
$false,
inference(connection,[status(thm),parent(t459:1)],[t459:1,t1:41]) ).
cnf(t461,plain,
cC20(iV21026),
inference(lemma_extension,[status(thm),parent(t459:2)],[l183:1]) ).
cnf(t462,plain,
$false,
inference(connection,[status(thm),parent(t461:1)],[t461:1,t459:2]) ).
cnf(t463,plain,
cC16(iV21026),
inference(lemma_extension,[status(thm),parent(t459:3)],[l194:1]) ).
cnf(t464,plain,
$false,
inference(connection,[status(thm),parent(t463:1)],[t463:1,t459:3]) ).
cnf(t465,plain,
( ~ sP6(iV21026)
| cC110(iV21026) ),
inference(extension,[status(thm),parent(t1:42)],[f_17_7]) ).
cnf(t466,plain,
$false,
inference(connection,[status(thm),parent(t465:1)],[t465:1,t1:42]) ).
cnf(t467,plain,
( ~ cC112(iV21026)
| sP6(iV21026) ),
inference(extension,[status(thm),parent(t465:2)],[f_17_5]) ).
cnf(t468,plain,
$false,
inference(connection,[status(thm),parent(t467:1)],[t467:1,t465:2]) ).
cnf(t469,plain,
cC112(iV21026),
inference(lemma_extension,[status(thm),parent(t467:2)],[l153:1]) ).
cnf(t470,plain,
$false,
inference(connection,[status(thm),parent(t469:1)],[t469:1,t467:2]) ).
cnf(l211,lemma,
cC110(iV21026),
inference(lemma,[status(cth),parent(t1:42),below(0:0)],[t1:42]) ).
cnf(t471,plain,
( ~ sP78(iV21026)
| cC158(iV21026) ),
inference(extension,[status(thm),parent(t1:43)],[f_187_7]) ).
cnf(t472,plain,
$false,
inference(connection,[status(thm),parent(t471:1)],[t471:1,t1:43]) ).
cnf(t473,plain,
( ~ cTEST(iV21026)
| sP78(iV21026) ),
inference(extension,[status(thm),parent(t471:2)],[f_187_5]) ).
cnf(t474,plain,
$false,
inference(connection,[status(thm),parent(t473:1)],[t473:1,t471:2]) ).
cnf(t475,plain,
cTEST(iV21026),
inference(extension,[status(thm),parent(t473:2)],[f_222_3]) ).
cnf(t476,plain,
$false,
inference(connection,[status(thm),parent(t475:1)],[t475:1,t473:2]) ).
cnf(t477,plain,
( ~ sP60(iV21026)
| cC56(iV21026) ),
inference(extension,[status(thm),parent(t1:44)],[f_144_7]) ).
cnf(t478,plain,
$false,
inference(connection,[status(thm),parent(t477:1)],[t477:1,t1:44]) ).
cnf(t479,plain,
( ~ cC58(iV21026)
| sP60(iV21026) ),
inference(extension,[status(thm),parent(t477:2)],[f_144_5]) ).
cnf(t480,plain,
$false,
inference(connection,[status(thm),parent(t479:1)],[t479:1,t477:2]) ).
cnf(t481,plain,
( ~ sP61(iV21026)
| cC58(iV21026) ),
inference(extension,[status(thm),parent(t479:2)],[f_147_7]) ).
cnf(t482,plain,
$false,
inference(connection,[status(thm),parent(t481:1)],[t481:1,t479:2]) ).
cnf(t483,plain,
( ~ cC60(iV21026)
| sP61(iV21026) ),
inference(extension,[status(thm),parent(t481:2)],[f_147_5]) ).
cnf(t484,plain,
$false,
inference(connection,[status(thm),parent(t483:1)],[t483:1,t481:2]) ).
cnf(t485,plain,
cC60(iV21026),
inference(lemma_extension,[status(thm),parent(t483:2)],[l208:1]) ).
cnf(t486,plain,
$false,
inference(connection,[status(thm),parent(t485:1)],[t485:1,t483:2]) ).
cnf(t487,plain,
( ~ sP61(iV21026)
| cC58(iV21026) ),
inference(extension,[status(thm),parent(t1:45)],[f_147_7]) ).
cnf(t488,plain,
$false,
inference(connection,[status(thm),parent(t487:1)],[t487:1,t1:45]) ).
cnf(t489,plain,
( ~ cC60(iV21026)
| sP61(iV21026) ),
inference(extension,[status(thm),parent(t487:2)],[f_147_5]) ).
cnf(t490,plain,
$false,
inference(connection,[status(thm),parent(t489:1)],[t489:1,t487:2]) ).
cnf(t491,plain,
cC60(iV21026),
inference(lemma_extension,[status(thm),parent(t489:2)],[l208:1]) ).
cnf(t492,plain,
$false,
inference(connection,[status(thm),parent(t491:1)],[t491:1,t489:2]) ).
cnf(t493,plain,
cowlThing(iV21026),
inference(extension,[status(thm),parent(t1:46)],[f_220_3]) ).
cnf(t494,plain,
$false,
inference(connection,[status(thm),parent(t493:1)],[t493:1,t1:46]) ).
cnf(t495,plain,
( ~ cC88(iV21026)
| ~ cC86(iV21026)
| cC90(iV21026) ),
inference(extension,[status(thm),parent(t1:47)],[f_175_6]) ).
cnf(t496,plain,
$false,
inference(connection,[status(thm),parent(t495:1)],[t495:1,t1:47]) ).
cnf(t497,plain,
cC86(iV21026),
inference(lemma_extension,[status(thm),parent(t495:2)],[l57:1]) ).
cnf(t498,plain,
$false,
inference(connection,[status(thm),parent(t497:1)],[t497:1,t495:2]) ).
cnf(t499,plain,
cC88(iV21026),
inference(lemma_extension,[status(thm),parent(t495:3)],[l122:1]) ).
cnf(t500,plain,
$false,
inference(connection,[status(thm),parent(t499:1)],[t499:1,t495:3]) ).
cnf(t501,plain,
( ~ sP29(iV21026)
| cC10(iV21026) ),
inference(extension,[status(thm),parent(t1:48)],[f_68_7]) ).
cnf(t502,plain,
$false,
inference(connection,[status(thm),parent(t501:1)],[t501:1,t1:48]) ).
cnf(t503,plain,
( ~ cC16(iV21026)
| sP29(iV21026) ),
inference(extension,[status(thm),parent(t501:2)],[f_68_5]) ).
cnf(t504,plain,
$false,
inference(connection,[status(thm),parent(t503:1)],[t503:1,t501:2]) ).
cnf(t505,plain,
cC16(iV21026),
inference(lemma_extension,[status(thm),parent(t503:2)],[l194:1]) ).
cnf(t506,plain,
$false,
inference(connection,[status(thm),parent(t505:1)],[t505:1,t503:2]) ).
cnf(t507,plain,
( ~ sP17(iV21026)
| cC136(iV21026) ),
inference(extension,[status(thm),parent(t1:49)],[f_44_7]) ).
cnf(t508,plain,
$false,
inference(connection,[status(thm),parent(t507:1)],[t507:1,t1:49]) ).
cnf(t509,plain,
( ~ cC138(iV21026)
| sP17(iV21026) ),
inference(extension,[status(thm),parent(t507:2)],[f_44_5]) ).
cnf(t510,plain,
$false,
inference(connection,[status(thm),parent(t509:1)],[t509:1,t507:2]) ).
cnf(t511,plain,
cC138(iV21026),
inference(lemma_extension,[status(thm),parent(t509:2)],[l177:1]) ).
cnf(t512,plain,
$false,
inference(connection,[status(thm),parent(t511:1)],[t511:1,t509:2]) ).
cnf(t513,plain,
( ~ sP52(iV21026)
| cC40(iV21026) ),
inference(extension,[status(thm),parent(t1:50)],[f_124_7]) ).
cnf(t514,plain,
$false,
inference(connection,[status(thm),parent(t513:1)],[t513:1,t1:50]) ).
cnf(t515,plain,
( ~ cC42(iV21026)
| sP52(iV21026) ),
inference(extension,[status(thm),parent(t513:2)],[f_124_5]) ).
cnf(t516,plain,
$false,
inference(connection,[status(thm),parent(t515:1)],[t515:1,t513:2]) ).
cnf(t517,plain,
cC42(iV21026),
inference(lemma_extension,[status(thm),parent(t515:2)],[l88:1]) ).
cnf(t518,plain,
$false,
inference(connection,[status(thm),parent(t517:1)],[t517:1,t515:2]) ).
cnf(t519,plain,
( ~ sP5(iV21026)
| cC108(iV21026) ),
inference(extension,[status(thm),parent(t1:51)],[f_16_7]) ).
cnf(t520,plain,
$false,
inference(connection,[status(thm),parent(t519:1)],[t519:1,t1:51]) ).
cnf(t521,plain,
( ~ cC110(iV21026)
| sP5(iV21026) ),
inference(extension,[status(thm),parent(t519:2)],[f_16_5]) ).
cnf(t522,plain,
$false,
inference(connection,[status(thm),parent(t521:1)],[t521:1,t519:2]) ).
cnf(t523,plain,
cC110(iV21026),
inference(lemma_extension,[status(thm),parent(t521:2)],[l211:1]) ).
cnf(t524,plain,
$false,
inference(connection,[status(thm),parent(t523:1)],[t523:1,t521:2]) ).
cnf(t525,plain,
( ~ xsd_string(sK140)
| ~ sP80 ),
inference(extension,[status(thm),parent(t1:52)],[f_343_14]) ).
cnf(t526,plain,
$false,
inference(connection,[status(thm),parent(t525:1)],[t525:1,t1:52]) ).
cnf(t527,plain,
( xsd_integer(sK140)
| xsd_string(sK140) ),
inference(extension,[status(thm),parent(t525:2)],[f_2_6]) ).
cnf(t528,plain,
$false,
inference(connection,[status(thm),parent(t527:1)],[t527:1,t525:2]) ).
cnf(t529,plain,
( ~ sP80
| ~ xsd_integer(sK140) ),
inference(extension,[status(thm),parent(t527:2)],[f_343_13]) ).
cnf(t530,plain,
$false,
inference(connection,[status(thm),parent(t529:1)],[t529:1,t527:2]) ).
cnf(t531,plain,
$false,
inference(reduction,[status(thm),parent(t529:2)],[t529:2,t1:52]) ).
cnf(t532,plain,
( xsd_integer(sK139)
| ~ sP79 ),
inference(extension,[status(thm),parent(t1:53)],[f_343_12]) ).
cnf(t533,plain,
$false,
inference(connection,[status(thm),parent(t532:1)],[t532:1,t1:53]) ).
cnf(t534,plain,
( ~ xsd_string(sK139)
| ~ xsd_integer(sK139) ),
inference(extension,[status(thm),parent(t532:2)],[f_2_5]) ).
cnf(t535,plain,
$false,
inference(connection,[status(thm),parent(t534:1)],[t534:1,t532:2]) ).
cnf(t536,plain,
( ~ sP79
| xsd_string(sK139) ),
inference(extension,[status(thm),parent(t534:2)],[f_343_11]) ).
cnf(t537,plain,
$false,
inference(connection,[status(thm),parent(t536:1)],[t536:1,t534:2]) ).
cnf(t538,plain,
$false,
inference(reduction,[status(thm),parent(t536:2)],[t536:2,t1:53]) ).
cnf(t539,plain,
~ cowlNothing(sK138),
inference(extension,[status(thm),parent(t1:54)],[f_1_6]) ).
cnf(t540,plain,
$false,
inference(connection,[status(thm),parent(t539:1)],[t539:1,t1:54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 12:16:35 UTC 2026
% 0.12/0.36 % CPUTime :
% 42.65/43.02 % SZS status Theorem for theBenchmark
% 42.65/43.02 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------