%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 1.55s 1.88s
% Output : Proof 1.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 66
% Syntax : Number of formulae : 481 ( 296 unt; 0 def)
% Number of atoms : 1498 ( 0 equ)
% Maximal formula atoms : 57 ( 3 avg)
% Number of connectives : 1785 ( 768 ~; 756 |; 235 &)
% ( 19 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 47 ( 46 usr; 3 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-1 aty)
% Number of variables : 183 ( 2 sgn 127 !; 22 ?)
% 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_11,axiom,
! [X] :
( cC106(X)
<=> ( cC100xcomp(X)
& cC104(X) ) ),
file('theBenchmark.p',axiom_11) ).
fof(axiom_12,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('theBenchmark.p',axiom_12) ).
fof(axiom_52,axiom,
! [X] :
( cC34(X)
<=> ( cC32xcomp(X)
& cC30xcomp(X) ) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_57,axiom,
! [X] :
( cC38(X)
<=> ( cC36xcomp(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_65,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& cC40xcomp(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_73,axiom,
! [X] :
( cC50(X)
<=> ( cC48xcomp(X)
& cC46xcomp(X) ) ),
file('theBenchmark.p',axiom_73) ).
fof(axiom_82,axiom,
! [X] :
( cC56(X)
<=> ( cC44(X)
& cC54xcomp(X) ) ),
file('theBenchmark.p',axiom_82) ).
fof(axiom_91,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_91) ).
fof(axiom_92,axiom,
! [X] :
( cC62(X)
<=> ( cC58xcomp(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_92) ).
fof(axiom_100,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC64xcomp(X) ) ),
file('theBenchmark.p',axiom_100) ).
fof(axiom_112,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& cC74xcomp(X) ) ),
file('theBenchmark.p',axiom_112) ).
fof(axiom_120,axiom,
! [X] :
( cC82(X)
<=> ( cC78xcomp(X)
& cC80(X) ) ),
file('theBenchmark.p',axiom_120) ).
fof(axiom_128,axiom,
! [X] :
( cC88(X)
<=> ( cC86xcomp(X)
& cC84xcomp(X) ) ),
file('theBenchmark.p',axiom_128) ).
fof(axiom_143,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& cC96xcomp(X) ) ),
file('theBenchmark.p',axiom_143) ).
fof(axiom_145,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_145) ).
fof(axiom_146,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('theBenchmark.p',axiom_146) ).
fof(axiom_147,axiom,
cowlThing(iV16439),
file('theBenchmark.p',axiom_147) ).
fof(axiom_149,axiom,
cTEST(iV16439),
file('theBenchmark.p',axiom_149) ).
fof(axiom_150,axiom,
rR1(iV16439,iV16440),
file('theBenchmark.p',axiom_150) ).
fof(axiom_153,axiom,
cowlThing(iV16440),
file('theBenchmark.p',axiom_153) ).
fof(axiom_156,axiom,
! [X] :
( rR1(iV16440,X)
=> cC76(X) ),
file('theBenchmark.p',axiom_156) ).
fof(axiom_159,axiom,
rR1(iV16440,iV16463),
file('theBenchmark.p',axiom_159) ).
fof(axiom_162,axiom,
cowlThing(iV16448),
file('theBenchmark.p',axiom_162) ).
fof(axiom_163,axiom,
cTOP(iV16448),
file('theBenchmark.p',axiom_163) ).
fof(axiom_168,axiom,
cC36xcomp(iV16448),
file('theBenchmark.p',axiom_168) ).
fof(axiom_174,axiom,
cC74xcomp(iV16453),
file('theBenchmark.p',axiom_174) ).
fof(axiom_175,axiom,
cowlThing(iV16453),
file('theBenchmark.p',axiom_175) ).
fof(axiom_178,axiom,
! [X] :
( rR1(iV16453,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_178) ).
fof(axiom_181,axiom,
cC58xcomp(iV16453),
file('theBenchmark.p',axiom_181) ).
fof(axiom_182,axiom,
rR1(iV16453,iV16461),
file('theBenchmark.p',axiom_182) ).
fof(axiom_184,axiom,
cowlThing(iV16455),
file('theBenchmark.p',axiom_184) ).
fof(axiom_185,axiom,
cC40xcomp(iV16455),
file('theBenchmark.p',axiom_185) ).
fof(axiom_188,axiom,
! [X] :
( rR1(iV16455,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_188) ).
fof(axiom_190,axiom,
cC54xcomp(iV16455),
file('theBenchmark.p',axiom_190) ).
fof(axiom_193,axiom,
rR1(iV16455,iV16460),
file('theBenchmark.p',axiom_193) ).
fof(axiom_195,axiom,
cowlThing(iV16457),
file('theBenchmark.p',axiom_195) ).
fof(axiom_197,axiom,
cTOP(iV16457),
file('theBenchmark.p',axiom_197) ).
fof(axiom_201,axiom,
cC36xcomp(iV16457),
file('theBenchmark.p',axiom_201) ).
fof(axiom_205,axiom,
cowlThing(iV16459),
file('theBenchmark.p',axiom_205) ).
fof(axiom_209,axiom,
cC30xcomp(iV16459),
file('theBenchmark.p',axiom_209) ).
fof(axiom_210,axiom,
cC84xcomp(iV16459),
file('theBenchmark.p',axiom_210) ).
fof(axiom_212,axiom,
cC46xcomp(iV16459),
file('theBenchmark.p',axiom_212) ).
fof(axiom_213,axiom,
cC64xcomp(iV16459),
file('theBenchmark.p',axiom_213) ).
fof(axiom_215,axiom,
cC86xcomp(iV16459),
file('theBenchmark.p',axiom_215) ).
fof(axiom_216,axiom,
cC32xcomp(iV16459),
file('theBenchmark.p',axiom_216) ).
fof(axiom_217,axiom,
cC48xcomp(iV16459),
file('theBenchmark.p',axiom_217) ).
fof(axiom_221,axiom,
cC66xcomp(iV16459),
file('theBenchmark.p',axiom_221) ).
fof(axiom_223,axiom,
cowlThing(iV16460),
file('theBenchmark.p',axiom_223) ).
fof(axiom_227,axiom,
cC8xcomp(iV16460),
file('theBenchmark.p',axiom_227) ).
fof(axiom_233,axiom,
cowlThing(iV16461),
file('theBenchmark.p',axiom_233) ).
fof(axiom_237,axiom,
cC12xcomp(iV16461),
file('theBenchmark.p',axiom_237) ).
fof(axiom_241,axiom,
! [X] :
( rR1(iV16461,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_241) ).
fof(axiom_243,axiom,
rR1(iV16461,iV16462),
file('theBenchmark.p',axiom_243) ).
fof(axiom_246,axiom,
cowlThing(iV16462),
file('theBenchmark.p',axiom_246) ).
fof(axiom_256,axiom,
cowlThing(iV16463),
file('theBenchmark.p',axiom_256) ).
fof(axiom_261,axiom,
! [X] :
( rR1(iV16463,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_261) ).
fof(axiom_263,axiom,
rR1(iV16463,iV16464),
file('theBenchmark.p',axiom_263) ).
fof(axiom_264,axiom,
cowlThing(iV16464),
file('theBenchmark.p',axiom_264) ).
fof(axiom_265,axiom,
! [X] :
( rR1(iV16464,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_265) ).
fof(axiom_267,axiom,
cC12xcomp(iV16464),
file('theBenchmark.p',axiom_267) ).
fof(axiom_274,axiom,
rR1(iV16464,iV16465),
file('theBenchmark.p',axiom_274) ).
fof(axiom_276,axiom,
cowlThing(iV16465),
file('theBenchmark.p',axiom_276) ).
fof(the_axiom,conjecture,
( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [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]) ).
cnf(f_1_4,plain,
cowlThing(U_1),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_5,plain,
~ cowlNothing(U_2),
inference(clausify,[status(thm)],[f_1_3]) ).
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]) ).
cnf(f_2_4,plain,
( ~ xsd_integer(U_4)
| ~ xsd_string(U_4) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( xsd_string(U_5)
| xsd_integer(U_5) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_12_1,plain,
! [X] :
( ( cC106(X)
| ~ cC100xcomp(X)
| ~ cC104(X) )
& ( ( cC100xcomp(X)
& cC104(X) )
| ~ cC106(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_11]) ).
fof(f_12_2,plain,
! [U_49] :
( ( cC106(U_49)
| ~ cC100xcomp(U_49)
| ~ cC104(U_49) )
& ( ( cC100xcomp(U_49)
& cC104(U_49) )
| ~ cC106(U_49) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_51] :
( cC106(U_51)
| ~ cC100xcomp(U_51)
| ~ cC104(U_51) )
& ! [U_50] :
( ( cC100xcomp(U_50)
& cC104(U_50) )
| ~ cC106(U_50) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( cC104(U_50)
| ~ cC106(U_50) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [X] :
( ( cC108(X)
| ~ cC106(X)
| ~ cC28(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_12]) ).
fof(f_13_2,plain,
! [U_52] :
( ( cC108(U_52)
| ~ cC106(U_52)
| ~ cC28(U_52) )
& ( ( cC106(U_52)
& cC28(U_52) )
| ~ cC108(U_52) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_54] :
( cC108(U_54)
| ~ cC106(U_54)
| ~ cC28(U_54) )
& ! [U_53] :
( ( cC106(U_53)
& cC28(U_53) )
| ~ cC108(U_53) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( cC28(U_53)
| ~ cC108(U_53) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( cC106(U_53)
| ~ cC108(U_53) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_53_1,plain,
! [X] :
( ( cC34(X)
| ~ cC32xcomp(X)
| ~ cC30xcomp(X) )
& ( ( cC32xcomp(X)
& cC30xcomp(X) )
| ~ cC34(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_52]) ).
fof(f_53_2,plain,
! [U_234] :
( ( cC34(U_234)
| ~ cC32xcomp(U_234)
| ~ cC30xcomp(U_234) )
& ( ( cC32xcomp(U_234)
& cC30xcomp(U_234) )
| ~ cC34(U_234) ) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_236] :
( cC34(U_236)
| ~ cC32xcomp(U_236)
| ~ cC30xcomp(U_236) )
& ! [U_235] :
( ( cC32xcomp(U_235)
& cC30xcomp(U_235) )
| ~ cC34(U_235) ) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
cnf(f_53_6,plain,
( cC34(U_236)
| ~ cC32xcomp(U_236)
| ~ cC30xcomp(U_236) ),
inference(clausify,[status(thm)],[f_53_3]) ).
fof(f_58_1,plain,
! [X] :
( ( cC38(X)
| ~ cC36xcomp(X)
| ~ cTOP(X) )
& ( ( cC36xcomp(X)
& cTOP(X) )
| ~ cC38(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_57]) ).
fof(f_58_2,plain,
! [U_257] :
( ( cC38(U_257)
| ~ cC36xcomp(U_257)
| ~ cTOP(U_257) )
& ( ( cC36xcomp(U_257)
& cTOP(U_257) )
| ~ cC38(U_257) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_259] :
( cC38(U_259)
| ~ cC36xcomp(U_259)
| ~ cTOP(U_259) )
& ! [U_258] :
( ( cC36xcomp(U_258)
& cTOP(U_258) )
| ~ cC38(U_258) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_6,plain,
( cC38(U_259)
| ~ cC36xcomp(U_259)
| ~ cTOP(U_259) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_66_1,plain,
! [X] :
( ( cC42(X)
| ! [Y] :
( ~ cC8xcomp(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_297] :
( ( cC42(U_297)
| ! [U_296] :
( ~ cC8xcomp(U_296)
| ~ rR1(U_297,U_296) ) )
& ( ? [U_295] :
( cC8xcomp(U_295)
& rR1(U_297,U_295) )
| ~ cC42(U_297) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_299] :
( cC42(U_299)
| ! [U_296] :
( ~ cC8xcomp(U_296)
| ~ rR1(U_299,U_296) ) )
& ! [U_298] :
( ? [U_295] :
( cC8xcomp(U_295)
& rR1(U_298,U_295) )
| ~ cC42(U_298) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
fof(f_66_4,plain,
( ! [U_299] :
( cC42(U_299)
| ! [U_296] :
( ~ cC8xcomp(U_296)
| ~ rR1(U_299,U_296) ) )
& ! [U_298] :
( ( cC8xcomp(sK51(U_298))
& rR1(U_298,sK51(U_298)) )
| ~ cC42(U_298) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_295,sK51(U_298))],[f_66_3]) ).
cnf(f_66_7,plain,
( cC42(U_299)
| ~ cC8xcomp(U_296)
| ~ rR1(U_299,U_296) ),
inference(clausify,[status(thm)],[f_66_4]) ).
fof(f_67_1,plain,
! [X] :
( ( cC44(X)
| ~ cC42(X)
| ~ cC40xcomp(X) )
& ( ( cC42(X)
& cC40xcomp(X) )
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_66]) ).
fof(f_67_2,plain,
! [U_300] :
( ( cC44(U_300)
| ~ cC42(U_300)
| ~ cC40xcomp(U_300) )
& ( ( cC42(U_300)
& cC40xcomp(U_300) )
| ~ cC44(U_300) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_302] :
( cC44(U_302)
| ~ cC42(U_302)
| ~ cC40xcomp(U_302) )
& ! [U_301] :
( ( cC42(U_301)
& cC40xcomp(U_301) )
| ~ cC44(U_301) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
cnf(f_67_5,plain,
( cC42(U_301)
| ~ cC44(U_301) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_6,plain,
( cC44(U_302)
| ~ cC42(U_302)
| ~ cC40xcomp(U_302) ),
inference(clausify,[status(thm)],[f_67_3]) ).
fof(f_74_1,plain,
! [X] :
( ( cC50(X)
| ~ cC48xcomp(X)
| ~ cC46xcomp(X) )
& ( ( cC48xcomp(X)
& cC46xcomp(X) )
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_73]) ).
fof(f_74_2,plain,
! [U_329] :
( ( cC50(U_329)
| ~ cC48xcomp(U_329)
| ~ cC46xcomp(U_329) )
& ( ( cC48xcomp(U_329)
& cC46xcomp(U_329) )
| ~ cC50(U_329) ) ),
inference(variable_rename,[status(thm)],[f_74_1]) ).
fof(f_74_3,plain,
( ! [U_331] :
( cC50(U_331)
| ~ cC48xcomp(U_331)
| ~ cC46xcomp(U_331) )
& ! [U_330] :
( ( cC48xcomp(U_330)
& cC46xcomp(U_330) )
| ~ cC50(U_330) ) ),
inference(miniscope,[status(thm)],[f_74_2]) ).
cnf(f_74_6,plain,
( cC50(U_331)
| ~ cC48xcomp(U_331)
| ~ cC46xcomp(U_331) ),
inference(clausify,[status(thm)],[f_74_3]) ).
fof(f_83_1,plain,
! [X] :
( ( cC56(X)
| ~ cC44(X)
| ~ cC54xcomp(X) )
& ( ( cC44(X)
& cC54xcomp(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_82]) ).
fof(f_83_2,plain,
! [U_372] :
( ( cC56(U_372)
| ~ cC44(U_372)
| ~ cC54xcomp(U_372) )
& ( ( cC44(U_372)
& cC54xcomp(U_372) )
| ~ cC56(U_372) ) ),
inference(variable_rename,[status(thm)],[f_83_1]) ).
fof(f_83_3,plain,
( ! [U_374] :
( cC56(U_374)
| ~ cC44(U_374)
| ~ cC54xcomp(U_374) )
& ! [U_373] :
( ( cC44(U_373)
& cC54xcomp(U_373) )
| ~ cC56(U_373) ) ),
inference(miniscope,[status(thm)],[f_83_2]) ).
cnf(f_83_5,plain,
( cC44(U_373)
| ~ cC56(U_373) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_6,plain,
( cC56(U_374)
| ~ cC44(U_374)
| ~ cC54xcomp(U_374) ),
inference(clausify,[status(thm)],[f_83_3]) ).
fof(f_92_1,plain,
! [X] :
( ( cC60(X)
| ! [Y] :
( ~ cC12xcomp(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_91]) ).
fof(f_92_2,plain,
! [U_415] :
( ( cC60(U_415)
| ! [U_414] :
( ~ cC12xcomp(U_414)
| ~ rR1(U_415,U_414) ) )
& ( ? [U_413] :
( cC12xcomp(U_413)
& rR1(U_415,U_413) )
| ~ cC60(U_415) ) ),
inference(variable_rename,[status(thm)],[f_92_1]) ).
fof(f_92_3,plain,
( ! [U_417] :
( cC60(U_417)
| ! [U_414] :
( ~ cC12xcomp(U_414)
| ~ rR1(U_417,U_414) ) )
& ! [U_416] :
( ? [U_413] :
( cC12xcomp(U_413)
& rR1(U_416,U_413) )
| ~ cC60(U_416) ) ),
inference(miniscope,[status(thm)],[f_92_2]) ).
fof(f_92_4,plain,
( ! [U_417] :
( cC60(U_417)
| ! [U_414] :
( ~ cC12xcomp(U_414)
| ~ rR1(U_417,U_414) ) )
& ! [U_416] :
( ( cC12xcomp(sK71(U_416))
& rR1(U_416,sK71(U_416)) )
| ~ cC60(U_416) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71]),skolemize(U_413,sK71(U_416))],[f_92_3]) ).
cnf(f_92_7,plain,
( cC60(U_417)
| ~ cC12xcomp(U_414)
| ~ rR1(U_417,U_414) ),
inference(clausify,[status(thm)],[f_92_4]) ).
fof(f_93_1,plain,
! [X] :
( ( cC62(X)
| ~ cC58xcomp(X)
| ~ cC60(X) )
& ( ( cC58xcomp(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_92]) ).
fof(f_93_2,plain,
! [U_418] :
( ( cC62(U_418)
| ~ cC58xcomp(U_418)
| ~ cC60(U_418) )
& ( ( cC58xcomp(U_418)
& cC60(U_418) )
| ~ cC62(U_418) ) ),
inference(variable_rename,[status(thm)],[f_93_1]) ).
fof(f_93_3,plain,
( ! [U_420] :
( cC62(U_420)
| ~ cC58xcomp(U_420)
| ~ cC60(U_420) )
& ! [U_419] :
( ( cC58xcomp(U_419)
& cC60(U_419) )
| ~ cC62(U_419) ) ),
inference(miniscope,[status(thm)],[f_93_2]) ).
cnf(f_93_6,plain,
( cC62(U_420)
| ~ cC58xcomp(U_420)
| ~ cC60(U_420) ),
inference(clausify,[status(thm)],[f_93_3]) ).
fof(f_101_1,plain,
! [X] :
( ( cC68(X)
| ~ cC66xcomp(X)
| ~ cC64xcomp(X) )
& ( ( cC66xcomp(X)
& cC64xcomp(X) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_100]) ).
fof(f_101_2,plain,
! [U_452] :
( ( cC68(U_452)
| ~ cC66xcomp(U_452)
| ~ cC64xcomp(U_452) )
& ( ( cC66xcomp(U_452)
& cC64xcomp(U_452) )
| ~ cC68(U_452) ) ),
inference(variable_rename,[status(thm)],[f_101_1]) ).
fof(f_101_3,plain,
( ! [U_454] :
( cC68(U_454)
| ~ cC66xcomp(U_454)
| ~ cC64xcomp(U_454) )
& ! [U_453] :
( ( cC66xcomp(U_453)
& cC64xcomp(U_453) )
| ~ cC68(U_453) ) ),
inference(miniscope,[status(thm)],[f_101_2]) ).
cnf(f_101_6,plain,
( cC68(U_454)
| ~ cC66xcomp(U_454)
| ~ cC64xcomp(U_454) ),
inference(clausify,[status(thm)],[f_101_3]) ).
fof(f_113_1,plain,
! [X] :
( ( cC76(X)
| ~ cC62(X)
| ~ cC74xcomp(X) )
& ( ( cC62(X)
& cC74xcomp(X) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_112]) ).
fof(f_113_2,plain,
! [U_510] :
( ( cC76(U_510)
| ~ cC62(U_510)
| ~ cC74xcomp(U_510) )
& ( ( cC62(U_510)
& cC74xcomp(U_510) )
| ~ cC76(U_510) ) ),
inference(variable_rename,[status(thm)],[f_113_1]) ).
fof(f_113_3,plain,
( ! [U_512] :
( cC76(U_512)
| ~ cC62(U_512)
| ~ cC74xcomp(U_512) )
& ! [U_511] :
( ( cC62(U_511)
& cC74xcomp(U_511) )
| ~ cC76(U_511) ) ),
inference(miniscope,[status(thm)],[f_113_2]) ).
cnf(f_113_5,plain,
( cC62(U_511)
| ~ cC76(U_511) ),
inference(clausify,[status(thm)],[f_113_3]) ).
cnf(f_113_6,plain,
( cC76(U_512)
| ~ cC62(U_512)
| ~ cC74xcomp(U_512) ),
inference(clausify,[status(thm)],[f_113_3]) ).
fof(f_121_1,plain,
! [X] :
( ( cC82(X)
| ~ cC78xcomp(X)
| ~ cC80(X) )
& ( ( cC78xcomp(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_120]) ).
fof(f_121_2,plain,
! [U_548] :
( ( cC82(U_548)
| ~ cC78xcomp(U_548)
| ~ cC80(U_548) )
& ( ( cC78xcomp(U_548)
& cC80(U_548) )
| ~ cC82(U_548) ) ),
inference(variable_rename,[status(thm)],[f_121_1]) ).
fof(f_121_3,plain,
( ! [U_550] :
( cC82(U_550)
| ~ cC78xcomp(U_550)
| ~ cC80(U_550) )
& ! [U_549] :
( ( cC78xcomp(U_549)
& cC80(U_549) )
| ~ cC82(U_549) ) ),
inference(miniscope,[status(thm)],[f_121_2]) ).
cnf(f_121_4,plain,
( cC80(U_549)
| ~ cC82(U_549) ),
inference(clausify,[status(thm)],[f_121_3]) ).
fof(f_129_1,plain,
! [X] :
( ( cC88(X)
| ~ cC86xcomp(X)
| ~ cC84xcomp(X) )
& ( ( cC86xcomp(X)
& cC84xcomp(X) )
| ~ cC88(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_128]) ).
fof(f_129_2,plain,
! [U_582] :
( ( cC88(U_582)
| ~ cC86xcomp(U_582)
| ~ cC84xcomp(U_582) )
& ( ( cC86xcomp(U_582)
& cC84xcomp(U_582) )
| ~ cC88(U_582) ) ),
inference(variable_rename,[status(thm)],[f_129_1]) ).
fof(f_129_3,plain,
( ! [U_584] :
( cC88(U_584)
| ~ cC86xcomp(U_584)
| ~ cC84xcomp(U_584) )
& ! [U_583] :
( ( cC86xcomp(U_583)
& cC84xcomp(U_583) )
| ~ cC88(U_583) ) ),
inference(miniscope,[status(thm)],[f_129_2]) ).
cnf(f_129_6,plain,
( cC88(U_584)
| ~ cC86xcomp(U_584)
| ~ cC84xcomp(U_584) ),
inference(clausify,[status(thm)],[f_129_3]) ).
fof(f_144_1,plain,
! [X] :
( ( cC98(X)
| ~ cC82(X)
| ~ cC96xcomp(X) )
& ( ( cC82(X)
& cC96xcomp(X) )
| ~ cC98(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_143]) ).
fof(f_144_2,plain,
! [U_655] :
( ( cC98(U_655)
| ~ cC82(U_655)
| ~ cC96xcomp(U_655) )
& ( ( cC82(U_655)
& cC96xcomp(U_655) )
| ~ cC98(U_655) ) ),
inference(variable_rename,[status(thm)],[f_144_1]) ).
fof(f_144_3,plain,
( ! [U_657] :
( cC98(U_657)
| ~ cC82(U_657)
| ~ cC96xcomp(U_657) )
& ! [U_656] :
( ( cC82(U_656)
& cC96xcomp(U_656) )
| ~ cC98(U_656) ) ),
inference(miniscope,[status(thm)],[f_144_2]) ).
cnf(f_144_5,plain,
( cC82(U_656)
| ~ cC98(U_656) ),
inference(clausify,[status(thm)],[f_144_3]) ).
fof(f_146_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC130(X)
| ~ cC108(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_145]) ).
fof(f_146_2,plain,
! [U_663] :
( ( cTEST(U_663)
| ~ cC130(U_663)
| ~ cC108(U_663) )
& ( ( cC130(U_663)
& cC108(U_663) )
| ~ cTEST(U_663) ) ),
inference(variable_rename,[status(thm)],[f_146_1]) ).
fof(f_146_3,plain,
( ! [U_665] :
( cTEST(U_665)
| ~ cC130(U_665)
| ~ cC108(U_665) )
& ! [U_664] :
( ( cC130(U_664)
& cC108(U_664) )
| ~ cTEST(U_664) ) ),
inference(miniscope,[status(thm)],[f_146_2]) ).
cnf(f_146_4,plain,
( cC108(U_664)
| ~ cTEST(U_664) ),
inference(clausify,[status(thm)],[f_146_3]) ).
cnf(f_146_5,plain,
( cC130(U_664)
| ~ cTEST(U_664) ),
inference(clausify,[status(thm)],[f_146_3]) ).
fof(f_147_1,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(fof_nnf,[status(thm)],[axiom_146]) ).
fof(f_147_2,plain,
! [U_666] :
( cC98(U_666)
| ~ rR1(iV16439,U_666) ),
inference(variable_rename,[status(thm)],[f_147_1]) ).
cnf(f_147_3,plain,
( cC98(U_666)
| ~ rR1(iV16439,U_666) ),
inference(clausify,[status(thm)],[f_147_2]) ).
fof(f_148_1,plain,
cowlThing(iV16439),
inference(fof_nnf,[status(thm)],[axiom_147]) ).
cnf(f_148_2,plain,
cowlThing(iV16439),
inference(clausify,[status(thm)],[f_148_1]) ).
fof(f_150_1,plain,
cTEST(iV16439),
inference(fof_nnf,[status(thm)],[axiom_149]) ).
cnf(f_150_2,plain,
cTEST(iV16439),
inference(clausify,[status(thm)],[f_150_1]) ).
fof(f_151_1,plain,
rR1(iV16439,iV16440),
inference(fof_nnf,[status(thm)],[axiom_150]) ).
cnf(f_151_2,plain,
rR1(iV16439,iV16440),
inference(clausify,[status(thm)],[f_151_1]) ).
fof(f_154_1,plain,
cowlThing(iV16440),
inference(fof_nnf,[status(thm)],[axiom_153]) ).
cnf(f_154_2,plain,
cowlThing(iV16440),
inference(clausify,[status(thm)],[f_154_1]) ).
fof(f_157_1,plain,
! [X] :
( cC76(X)
| ~ rR1(iV16440,X) ),
inference(fof_nnf,[status(thm)],[axiom_156]) ).
fof(f_157_2,plain,
! [U_668] :
( cC76(U_668)
| ~ rR1(iV16440,U_668) ),
inference(variable_rename,[status(thm)],[f_157_1]) ).
cnf(f_157_3,plain,
( cC76(U_668)
| ~ rR1(iV16440,U_668) ),
inference(clausify,[status(thm)],[f_157_2]) ).
fof(f_160_1,plain,
rR1(iV16440,iV16463),
inference(fof_nnf,[status(thm)],[axiom_159]) ).
cnf(f_160_2,plain,
rR1(iV16440,iV16463),
inference(clausify,[status(thm)],[f_160_1]) ).
fof(f_163_1,plain,
cowlThing(iV16448),
inference(fof_nnf,[status(thm)],[axiom_162]) ).
cnf(f_163_2,plain,
cowlThing(iV16448),
inference(clausify,[status(thm)],[f_163_1]) ).
fof(f_164_1,plain,
cTOP(iV16448),
inference(fof_nnf,[status(thm)],[axiom_163]) ).
cnf(f_164_2,plain,
cTOP(iV16448),
inference(clausify,[status(thm)],[f_164_1]) ).
fof(f_169_1,plain,
cC36xcomp(iV16448),
inference(fof_nnf,[status(thm)],[axiom_168]) ).
cnf(f_169_2,plain,
cC36xcomp(iV16448),
inference(clausify,[status(thm)],[f_169_1]) ).
fof(f_175_1,plain,
cC74xcomp(iV16453),
inference(fof_nnf,[status(thm)],[axiom_174]) ).
cnf(f_175_2,plain,
cC74xcomp(iV16453),
inference(clausify,[status(thm)],[f_175_1]) ).
fof(f_176_1,plain,
cowlThing(iV16453),
inference(fof_nnf,[status(thm)],[axiom_175]) ).
cnf(f_176_2,plain,
cowlThing(iV16453),
inference(clausify,[status(thm)],[f_176_1]) ).
fof(f_179_1,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16453,X) ),
inference(fof_nnf,[status(thm)],[axiom_178]) ).
fof(f_179_2,plain,
! [U_674] :
( cC56(U_674)
| ~ rR1(iV16453,U_674) ),
inference(variable_rename,[status(thm)],[f_179_1]) ).
cnf(f_179_3,plain,
( cC56(U_674)
| ~ rR1(iV16453,U_674) ),
inference(clausify,[status(thm)],[f_179_2]) ).
fof(f_182_1,plain,
cC58xcomp(iV16453),
inference(fof_nnf,[status(thm)],[axiom_181]) ).
cnf(f_182_2,plain,
cC58xcomp(iV16453),
inference(clausify,[status(thm)],[f_182_1]) ).
fof(f_183_1,plain,
rR1(iV16453,iV16461),
inference(fof_nnf,[status(thm)],[axiom_182]) ).
cnf(f_183_2,plain,
rR1(iV16453,iV16461),
inference(clausify,[status(thm)],[f_183_1]) ).
fof(f_185_1,plain,
cowlThing(iV16455),
inference(fof_nnf,[status(thm)],[axiom_184]) ).
cnf(f_185_2,plain,
cowlThing(iV16455),
inference(clausify,[status(thm)],[f_185_1]) ).
fof(f_186_1,plain,
cC40xcomp(iV16455),
inference(fof_nnf,[status(thm)],[axiom_185]) ).
cnf(f_186_2,plain,
cC40xcomp(iV16455),
inference(clausify,[status(thm)],[f_186_1]) ).
fof(f_189_1,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16455,X) ),
inference(fof_nnf,[status(thm)],[axiom_188]) ).
fof(f_189_2,plain,
! [U_678] :
( cC38(U_678)
| ~ rR1(iV16455,U_678) ),
inference(variable_rename,[status(thm)],[f_189_1]) ).
cnf(f_189_3,plain,
( cC38(U_678)
| ~ rR1(iV16455,U_678) ),
inference(clausify,[status(thm)],[f_189_2]) ).
fof(f_191_1,plain,
cC54xcomp(iV16455),
inference(fof_nnf,[status(thm)],[axiom_190]) ).
cnf(f_191_2,plain,
cC54xcomp(iV16455),
inference(clausify,[status(thm)],[f_191_1]) ).
fof(f_194_1,plain,
rR1(iV16455,iV16460),
inference(fof_nnf,[status(thm)],[axiom_193]) ).
cnf(f_194_2,plain,
rR1(iV16455,iV16460),
inference(clausify,[status(thm)],[f_194_1]) ).
fof(f_196_1,plain,
cowlThing(iV16457),
inference(fof_nnf,[status(thm)],[axiom_195]) ).
cnf(f_196_2,plain,
cowlThing(iV16457),
inference(clausify,[status(thm)],[f_196_1]) ).
fof(f_198_1,plain,
cTOP(iV16457),
inference(fof_nnf,[status(thm)],[axiom_197]) ).
cnf(f_198_2,plain,
cTOP(iV16457),
inference(clausify,[status(thm)],[f_198_1]) ).
fof(f_202_1,plain,
cC36xcomp(iV16457),
inference(fof_nnf,[status(thm)],[axiom_201]) ).
cnf(f_202_2,plain,
cC36xcomp(iV16457),
inference(clausify,[status(thm)],[f_202_1]) ).
fof(f_206_1,plain,
cowlThing(iV16459),
inference(fof_nnf,[status(thm)],[axiom_205]) ).
cnf(f_206_2,plain,
cowlThing(iV16459),
inference(clausify,[status(thm)],[f_206_1]) ).
fof(f_210_1,plain,
cC30xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_209]) ).
cnf(f_210_2,plain,
cC30xcomp(iV16459),
inference(clausify,[status(thm)],[f_210_1]) ).
fof(f_211_1,plain,
cC84xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_210]) ).
cnf(f_211_2,plain,
cC84xcomp(iV16459),
inference(clausify,[status(thm)],[f_211_1]) ).
fof(f_213_1,plain,
cC46xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_212]) ).
cnf(f_213_2,plain,
cC46xcomp(iV16459),
inference(clausify,[status(thm)],[f_213_1]) ).
fof(f_214_1,plain,
cC64xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_213]) ).
cnf(f_214_2,plain,
cC64xcomp(iV16459),
inference(clausify,[status(thm)],[f_214_1]) ).
fof(f_216_1,plain,
cC86xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_215]) ).
cnf(f_216_2,plain,
cC86xcomp(iV16459),
inference(clausify,[status(thm)],[f_216_1]) ).
fof(f_217_1,plain,
cC32xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_216]) ).
cnf(f_217_2,plain,
cC32xcomp(iV16459),
inference(clausify,[status(thm)],[f_217_1]) ).
fof(f_218_1,plain,
cC48xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_217]) ).
cnf(f_218_2,plain,
cC48xcomp(iV16459),
inference(clausify,[status(thm)],[f_218_1]) ).
fof(f_222_1,plain,
cC66xcomp(iV16459),
inference(fof_nnf,[status(thm)],[axiom_221]) ).
cnf(f_222_2,plain,
cC66xcomp(iV16459),
inference(clausify,[status(thm)],[f_222_1]) ).
fof(f_224_1,plain,
cowlThing(iV16460),
inference(fof_nnf,[status(thm)],[axiom_223]) ).
cnf(f_224_2,plain,
cowlThing(iV16460),
inference(clausify,[status(thm)],[f_224_1]) ).
fof(f_228_1,plain,
cC8xcomp(iV16460),
inference(fof_nnf,[status(thm)],[axiom_227]) ).
cnf(f_228_2,plain,
cC8xcomp(iV16460),
inference(clausify,[status(thm)],[f_228_1]) ).
fof(f_234_1,plain,
cowlThing(iV16461),
inference(fof_nnf,[status(thm)],[axiom_233]) ).
cnf(f_234_2,plain,
cowlThing(iV16461),
inference(clausify,[status(thm)],[f_234_1]) ).
fof(f_238_1,plain,
cC12xcomp(iV16461),
inference(fof_nnf,[status(thm)],[axiom_237]) ).
cnf(f_238_2,plain,
cC12xcomp(iV16461),
inference(clausify,[status(thm)],[f_238_1]) ).
fof(f_242_1,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16461,X) ),
inference(fof_nnf,[status(thm)],[axiom_241]) ).
fof(f_242_2,plain,
! [U_691] :
( cC38(U_691)
| ~ rR1(iV16461,U_691) ),
inference(variable_rename,[status(thm)],[f_242_1]) ).
cnf(f_242_3,plain,
( cC38(U_691)
| ~ rR1(iV16461,U_691) ),
inference(clausify,[status(thm)],[f_242_2]) ).
fof(f_244_1,plain,
rR1(iV16461,iV16462),
inference(fof_nnf,[status(thm)],[axiom_243]) ).
cnf(f_244_2,plain,
rR1(iV16461,iV16462),
inference(clausify,[status(thm)],[f_244_1]) ).
fof(f_247_1,plain,
cowlThing(iV16462),
inference(fof_nnf,[status(thm)],[axiom_246]) ).
cnf(f_247_2,plain,
cowlThing(iV16462),
inference(clausify,[status(thm)],[f_247_1]) ).
fof(f_257_1,plain,
cowlThing(iV16463),
inference(fof_nnf,[status(thm)],[axiom_256]) ).
cnf(f_257_2,plain,
cowlThing(iV16463),
inference(clausify,[status(thm)],[f_257_1]) ).
fof(f_262_1,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16463,X) ),
inference(fof_nnf,[status(thm)],[axiom_261]) ).
fof(f_262_2,plain,
! [U_698] :
( cC56(U_698)
| ~ rR1(iV16463,U_698) ),
inference(variable_rename,[status(thm)],[f_262_1]) ).
cnf(f_262_3,plain,
( cC56(U_698)
| ~ rR1(iV16463,U_698) ),
inference(clausify,[status(thm)],[f_262_2]) ).
fof(f_264_1,plain,
rR1(iV16463,iV16464),
inference(fof_nnf,[status(thm)],[axiom_263]) ).
cnf(f_264_2,plain,
rR1(iV16463,iV16464),
inference(clausify,[status(thm)],[f_264_1]) ).
fof(f_265_1,plain,
cowlThing(iV16464),
inference(fof_nnf,[status(thm)],[axiom_264]) ).
cnf(f_265_2,plain,
cowlThing(iV16464),
inference(clausify,[status(thm)],[f_265_1]) ).
fof(f_266_1,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16464,X) ),
inference(fof_nnf,[status(thm)],[axiom_265]) ).
fof(f_266_2,plain,
! [U_699] :
( cC38(U_699)
| ~ rR1(iV16464,U_699) ),
inference(variable_rename,[status(thm)],[f_266_1]) ).
cnf(f_266_3,plain,
( cC38(U_699)
| ~ rR1(iV16464,U_699) ),
inference(clausify,[status(thm)],[f_266_2]) ).
fof(f_268_1,plain,
cC12xcomp(iV16464),
inference(fof_nnf,[status(thm)],[axiom_267]) ).
cnf(f_268_2,plain,
cC12xcomp(iV16464),
inference(clausify,[status(thm)],[f_268_1]) ).
fof(f_275_1,plain,
rR1(iV16464,iV16465),
inference(fof_nnf,[status(thm)],[axiom_274]) ).
cnf(f_275_2,plain,
rR1(iV16464,iV16465),
inference(clausify,[status(thm)],[f_275_1]) ).
fof(f_277_1,plain,
cowlThing(iV16465),
inference(fof_nnf,[status(thm)],[axiom_276]) ).
cnf(f_277_2,plain,
cowlThing(iV16465),
inference(clausify,[status(thm)],[f_277_1]) ).
fof(f_287_1,negated_conjecture,
~ ( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_287_2,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_287_1]) ).
fof(f_287_3,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [U_708] :
( ( ~ xsd_string(U_708)
& ~ xsd_integer(U_708) )
| ( xsd_integer(U_708)
& xsd_string(U_708) ) )
| ? [U_707] :
( cowlNothing(U_707)
| ~ cowlThing(U_707) ) ),
inference(variable_rename,[status(thm)],[f_287_2]) ).
fof(f_287_4,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [U_712] :
( ~ xsd_string(U_712)
& ~ xsd_integer(U_712) )
| ? [U_711] :
( xsd_integer(U_711)
& xsd_string(U_711) )
| ? [U_710] : cowlNothing(U_710)
| ? [U_709] : ~ cowlThing(U_709) ),
inference(miniscope,[status(thm)],[f_287_3]) ).
fof(f_287_5,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [U_712] :
( ~ xsd_string(U_712)
& ~ xsd_integer(U_712) )
| ? [U_711] :
( xsd_integer(U_711)
& xsd_string(U_711) )
| ? [U_710] : cowlNothing(U_710)
| ~ cowlThing(sK115) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115]),skolemize(U_709,sK115)],[f_287_4]) ).
fof(f_287_6,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [U_712] :
( ~ xsd_string(U_712)
& ~ xsd_integer(U_712) )
| ? [U_711] :
( xsd_integer(U_711)
& xsd_string(U_711) )
| cowlNothing(sK116)
| ~ cowlThing(sK115) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116]),skolemize(U_710,sK116)],[f_287_5]) ).
fof(f_287_7,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [U_712] :
( ~ xsd_string(U_712)
& ~ xsd_integer(U_712) )
| ( xsd_integer(sK117)
& xsd_string(sK117) )
| cowlNothing(sK116)
| ~ cowlThing(sK115) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK117]),skolemize(U_711,sK117)],[f_287_6]) ).
fof(f_287_8,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ( ~ xsd_string(sK118)
& ~ xsd_integer(sK118) )
| ( xsd_integer(sK117)
& xsd_string(sK117) )
| cowlNothing(sK116)
| ~ cowlThing(sK115) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118]),skolemize(U_712,sK118)],[f_287_7]) ).
fof(f_287_9,negated_conjecture,
( ( ~ xsd_string(sK118)
| ~ sP1 )
& ( ~ xsd_integer(sK118)
| ~ sP1 )
& ( xsd_integer(sK117)
| ~ sP0 )
& ( xsd_string(sK117)
| ~ sP0 )
& ( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| sP1
| sP0
| cowlNothing(sK116)
| ~ cowlThing(sK115) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_287_8]) ).
cnf(f_287_10,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| sP1
| sP0
| cowlNothing(sK116)
| ~ cowlThing(sK115) ),
inference(clausify,[status(thm)],[f_287_9]) ).
cnf(f_287_11,negated_conjecture,
( xsd_string(sK117)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_287_9]) ).
cnf(f_287_12,negated_conjecture,
( xsd_integer(sK117)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_287_9]) ).
cnf(f_287_13,negated_conjecture,
( ~ xsd_integer(sK118)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_287_9]) ).
cnf(f_287_14,negated_conjecture,
( ~ xsd_string(sK118)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_287_9]) ).
cnf(t1,plain,
~ cowlNothing(sK116),
inference(start,[status(thm),parent(0:0)],[f_1_5]) ).
cnf(t2,plain,
( ~ cowlThing(iV16465)
| sP0
| sP1
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cowlThing(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16455)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC38(iV16465)
| ~ cowlThing(sK115)
| cowlNothing(sK116) ),
inference(extension,[status(thm),parent(t1:1)],[f_287_10]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
cowlThing(sK115),
inference(extension,[status(thm),parent(t2:2)],[f_1_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ rR1(iV16464,iV16465)
| cC38(iV16465) ),
inference(extension,[status(thm),parent(t2:3)],[f_266_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(t8,plain,
rR1(iV16464,iV16465),
inference(extension,[status(thm),parent(t6:2)],[f_275_2]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
cowlThing(iV16464),
inference(extension,[status(thm),parent(t2:4)],[f_265_2]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t2:4]) ).
cnf(t12,plain,
( ~ cC56(iV16464)
| cC44(iV16464) ),
inference(extension,[status(thm),parent(t2:5)],[f_83_5]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t2:5]) ).
cnf(t14,plain,
( ~ rR1(iV16463,iV16464)
| cC56(iV16464) ),
inference(extension,[status(thm),parent(t12:2)],[f_262_3]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
rR1(iV16463,iV16464),
inference(extension,[status(thm),parent(t14:2)],[f_264_2]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(l6,lemma,
cC44(iV16464),
inference(lemma,[status(cth),parent(t2:5),below(t1:1)],[t2:5]) ).
cnf(t18,plain,
( ~ cC44(iV16464)
| cC42(iV16464) ),
inference(extension,[status(thm),parent(t2:6)],[f_67_5]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t2:6]) ).
cnf(t20,plain,
cC44(iV16464),
inference(lemma_extension,[status(thm),parent(t18:2)],[l6:1]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
( ~ rR1(iV16463,iV16464)
| cC56(iV16464) ),
inference(extension,[status(thm),parent(t2:7)],[f_262_3]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t2:7]) ).
cnf(t24,plain,
rR1(iV16463,iV16464),
inference(extension,[status(thm),parent(t22:2)],[f_264_2]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
( ~ cC12xcomp(iV16464)
| ~ rR1(iV16463,iV16464)
| cC60(iV16463) ),
inference(extension,[status(thm),parent(t2:8)],[f_92_7]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t2:8]) ).
cnf(t28,plain,
rR1(iV16463,iV16464),
inference(extension,[status(thm),parent(t26:2)],[f_264_2]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
cC12xcomp(iV16464),
inference(extension,[status(thm),parent(t26:3)],[f_268_2]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t26:3]) ).
cnf(t32,plain,
cowlThing(iV16463),
inference(extension,[status(thm),parent(t2:9)],[f_257_2]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t2:9]) ).
cnf(t34,plain,
( ~ cC76(iV16463)
| cC62(iV16463) ),
inference(extension,[status(thm),parent(t2:10)],[f_113_5]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t2:10]) ).
cnf(t36,plain,
( ~ rR1(iV16440,iV16463)
| cC76(iV16463) ),
inference(extension,[status(thm),parent(t34:2)],[f_157_3]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
rR1(iV16440,iV16463),
inference(extension,[status(thm),parent(t36:2)],[f_160_2]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
cnf(t40,plain,
( ~ rR1(iV16440,iV16463)
| cC76(iV16463) ),
inference(extension,[status(thm),parent(t2:11)],[f_157_3]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t2:11]) ).
cnf(t42,plain,
rR1(iV16440,iV16463),
inference(extension,[status(thm),parent(t40:2)],[f_160_2]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
cnf(t44,plain,
cowlThing(iV16462),
inference(extension,[status(thm),parent(t2:12)],[f_247_2]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t2:12]) ).
cnf(t46,plain,
( ~ rR1(iV16461,iV16462)
| cC38(iV16462) ),
inference(extension,[status(thm),parent(t2:13)],[f_242_3]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t2:13]) ).
cnf(t48,plain,
rR1(iV16461,iV16462),
inference(extension,[status(thm),parent(t46:2)],[f_244_2]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(t50,plain,
cowlThing(iV16461),
inference(extension,[status(thm),parent(t2:14)],[f_234_2]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t2:14]) ).
cnf(t52,plain,
( ~ cC56(iV16461)
| cC44(iV16461) ),
inference(extension,[status(thm),parent(t2:15)],[f_83_5]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t2:15]) ).
cnf(t54,plain,
( ~ rR1(iV16453,iV16461)
| cC56(iV16461) ),
inference(extension,[status(thm),parent(t52:2)],[f_179_3]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t52:2]) ).
cnf(t56,plain,
rR1(iV16453,iV16461),
inference(extension,[status(thm),parent(t54:2)],[f_183_2]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(l25,lemma,
cC44(iV16461),
inference(lemma,[status(cth),parent(t2:15),below(t1:1)],[t2:15]) ).
cnf(t58,plain,
( ~ rR1(iV16453,iV16461)
| cC56(iV16461) ),
inference(extension,[status(thm),parent(t2:16)],[f_179_3]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t2:16]) ).
cnf(t60,plain,
rR1(iV16453,iV16461),
inference(extension,[status(thm),parent(t58:2)],[f_183_2]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
( ~ cC44(iV16461)
| cC42(iV16461) ),
inference(extension,[status(thm),parent(t2:17)],[f_67_5]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t2:17]) ).
cnf(t64,plain,
cC44(iV16461),
inference(lemma_extension,[status(thm),parent(t62:2)],[l25:1]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
cowlThing(iV16460),
inference(extension,[status(thm),parent(t2:18)],[f_224_2]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t2:18]) ).
cnf(t68,plain,
( ~ rR1(iV16455,iV16460)
| cC38(iV16460) ),
inference(extension,[status(thm),parent(t2:19)],[f_189_3]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t2:19]) ).
cnf(t70,plain,
rR1(iV16455,iV16460),
inference(extension,[status(thm),parent(t68:2)],[f_194_2]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t68:2]) ).
cnf(t72,plain,
cowlThing(iV16459),
inference(extension,[status(thm),parent(t2:20)],[f_206_2]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t2:20]) ).
cnf(t74,plain,
( ~ cC66xcomp(iV16459)
| ~ cC64xcomp(iV16459)
| cC68(iV16459) ),
inference(extension,[status(thm),parent(t2:21)],[f_101_6]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t2:21]) ).
cnf(t76,plain,
cC64xcomp(iV16459),
inference(extension,[status(thm),parent(t74:2)],[f_214_2]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
cC66xcomp(iV16459),
inference(extension,[status(thm),parent(t74:3)],[f_222_2]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t74:3]) ).
cnf(t80,plain,
( ~ cC32xcomp(iV16459)
| ~ cC30xcomp(iV16459)
| cC34(iV16459) ),
inference(extension,[status(thm),parent(t2:22)],[f_53_6]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t2:22]) ).
cnf(t82,plain,
cC30xcomp(iV16459),
inference(extension,[status(thm),parent(t80:2)],[f_210_2]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t80:2]) ).
cnf(t84,plain,
cC32xcomp(iV16459),
inference(extension,[status(thm),parent(t80:3)],[f_217_2]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t80:3]) ).
cnf(t86,plain,
( ~ cC86xcomp(iV16459)
| ~ cC84xcomp(iV16459)
| cC88(iV16459) ),
inference(extension,[status(thm),parent(t2:23)],[f_129_6]) ).
cnf(t87,plain,
$false,
inference(connection,[status(thm),parent(t86:1)],[t86:1,t2:23]) ).
cnf(t88,plain,
cC84xcomp(iV16459),
inference(extension,[status(thm),parent(t86:2)],[f_211_2]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t86:2]) ).
cnf(t90,plain,
cC86xcomp(iV16459),
inference(extension,[status(thm),parent(t86:3)],[f_216_2]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t86:3]) ).
cnf(t92,plain,
( ~ cC48xcomp(iV16459)
| ~ cC46xcomp(iV16459)
| cC50(iV16459) ),
inference(extension,[status(thm),parent(t2:24)],[f_74_6]) ).
cnf(t93,plain,
$false,
inference(connection,[status(thm),parent(t92:1)],[t92:1,t2:24]) ).
cnf(t94,plain,
cC46xcomp(iV16459),
inference(extension,[status(thm),parent(t92:2)],[f_213_2]) ).
cnf(t95,plain,
$false,
inference(connection,[status(thm),parent(t94:1)],[t94:1,t92:2]) ).
cnf(t96,plain,
cC48xcomp(iV16459),
inference(extension,[status(thm),parent(t92:3)],[f_218_2]) ).
cnf(t97,plain,
$false,
inference(connection,[status(thm),parent(t96:1)],[t96:1,t92:3]) ).
cnf(t98,plain,
cowlThing(iV16457),
inference(extension,[status(thm),parent(t2:25)],[f_196_2]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t2:25]) ).
cnf(t100,plain,
( ~ cC36xcomp(iV16457)
| ~ cTOP(iV16457)
| cC38(iV16457) ),
inference(extension,[status(thm),parent(t2:26)],[f_58_6]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t2:26]) ).
cnf(t102,plain,
cTOP(iV16457),
inference(extension,[status(thm),parent(t100:2)],[f_198_2]) ).
cnf(t103,plain,
$false,
inference(connection,[status(thm),parent(t102:1)],[t102:1,t100:2]) ).
cnf(t104,plain,
cC36xcomp(iV16457),
inference(extension,[status(thm),parent(t100:3)],[f_202_2]) ).
cnf(t105,plain,
$false,
inference(connection,[status(thm),parent(t104:1)],[t104:1,t100:3]) ).
cnf(t106,plain,
cowlThing(iV16455),
inference(extension,[status(thm),parent(t2:27)],[f_185_2]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t2:27]) ).
cnf(t108,plain,
( ~ cC8xcomp(iV16460)
| ~ rR1(iV16455,iV16460)
| cC42(iV16455) ),
inference(extension,[status(thm),parent(t2:28)],[f_66_7]) ).
cnf(t109,plain,
$false,
inference(connection,[status(thm),parent(t108:1)],[t108:1,t2:28]) ).
cnf(t110,plain,
rR1(iV16455,iV16460),
inference(extension,[status(thm),parent(t108:2)],[f_194_2]) ).
cnf(t111,plain,
$false,
inference(connection,[status(thm),parent(t110:1)],[t110:1,t108:2]) ).
cnf(t112,plain,
cC8xcomp(iV16460),
inference(extension,[status(thm),parent(t108:3)],[f_228_2]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t108:3]) ).
cnf(l52,lemma,
cC42(iV16455),
inference(lemma,[status(cth),parent(t2:28),below(t1:1)],[t2:28]) ).
cnf(t114,plain,
( ~ cC42(iV16455)
| ~ cC40xcomp(iV16455)
| cC44(iV16455) ),
inference(extension,[status(thm),parent(t2:29)],[f_67_6]) ).
cnf(t115,plain,
$false,
inference(connection,[status(thm),parent(t114:1)],[t114:1,t2:29]) ).
cnf(t116,plain,
cC40xcomp(iV16455),
inference(extension,[status(thm),parent(t114:2)],[f_186_2]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t114:2]) ).
cnf(t118,plain,
cC42(iV16455),
inference(lemma_extension,[status(thm),parent(t114:3)],[l52:1]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t114:3]) ).
cnf(l55,lemma,
cC44(iV16455),
inference(lemma,[status(cth),parent(t2:29),below(t1:1)],[t2:29]) ).
cnf(t120,plain,
( ~ cC44(iV16455)
| ~ cC54xcomp(iV16455)
| cC56(iV16455) ),
inference(extension,[status(thm),parent(t2:30)],[f_83_6]) ).
cnf(t121,plain,
$false,
inference(connection,[status(thm),parent(t120:1)],[t120:1,t2:30]) ).
cnf(t122,plain,
cC54xcomp(iV16455),
inference(extension,[status(thm),parent(t120:2)],[f_191_2]) ).
cnf(t123,plain,
$false,
inference(connection,[status(thm),parent(t122:1)],[t122:1,t120:2]) ).
cnf(t124,plain,
cC44(iV16455),
inference(lemma_extension,[status(thm),parent(t120:3)],[l55:1]) ).
cnf(t125,plain,
$false,
inference(connection,[status(thm),parent(t124:1)],[t124:1,t120:3]) ).
cnf(t126,plain,
( ~ cC12xcomp(iV16461)
| ~ rR1(iV16453,iV16461)
| cC60(iV16453) ),
inference(extension,[status(thm),parent(t2:31)],[f_92_7]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t2:31]) ).
cnf(t128,plain,
rR1(iV16453,iV16461),
inference(extension,[status(thm),parent(t126:2)],[f_183_2]) ).
cnf(t129,plain,
$false,
inference(connection,[status(thm),parent(t128:1)],[t128:1,t126:2]) ).
cnf(t130,plain,
cC12xcomp(iV16461),
inference(extension,[status(thm),parent(t126:3)],[f_238_2]) ).
cnf(t131,plain,
$false,
inference(connection,[status(thm),parent(t130:1)],[t130:1,t126:3]) ).
cnf(l59,lemma,
cC60(iV16453),
inference(lemma,[status(cth),parent(t2:31),below(t1:1)],[t2:31]) ).
cnf(t132,plain,
cowlThing(iV16453),
inference(extension,[status(thm),parent(t2:32)],[f_176_2]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t2:32]) ).
cnf(t134,plain,
( ~ cC58xcomp(iV16453)
| ~ cC60(iV16453)
| cC62(iV16453) ),
inference(extension,[status(thm),parent(t2:33)],[f_93_6]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t2:33]) ).
cnf(t136,plain,
cC60(iV16453),
inference(lemma_extension,[status(thm),parent(t134:2)],[l59:1]) ).
cnf(t137,plain,
$false,
inference(connection,[status(thm),parent(t136:1)],[t136:1,t134:2]) ).
cnf(t138,plain,
cC58xcomp(iV16453),
inference(extension,[status(thm),parent(t134:3)],[f_182_2]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t134:3]) ).
cnf(l63,lemma,
cC62(iV16453),
inference(lemma,[status(cth),parent(t2:33),below(t1:1)],[t2:33]) ).
cnf(t140,plain,
( ~ cC62(iV16453)
| ~ cC74xcomp(iV16453)
| cC76(iV16453) ),
inference(extension,[status(thm),parent(t2:34)],[f_113_6]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t2:34]) ).
cnf(t142,plain,
cC74xcomp(iV16453),
inference(extension,[status(thm),parent(t140:2)],[f_175_2]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t140:2]) ).
cnf(t144,plain,
cC62(iV16453),
inference(lemma_extension,[status(thm),parent(t140:3)],[l63:1]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t140:3]) ).
cnf(t146,plain,
cowlThing(iV16448),
inference(extension,[status(thm),parent(t2:35)],[f_163_2]) ).
cnf(t147,plain,
$false,
inference(connection,[status(thm),parent(t146:1)],[t146:1,t2:35]) ).
cnf(t148,plain,
( ~ cC36xcomp(iV16448)
| ~ cTOP(iV16448)
| cC38(iV16448) ),
inference(extension,[status(thm),parent(t2:36)],[f_58_6]) ).
cnf(t149,plain,
$false,
inference(connection,[status(thm),parent(t148:1)],[t148:1,t2:36]) ).
cnf(t150,plain,
cTOP(iV16448),
inference(extension,[status(thm),parent(t148:2)],[f_164_2]) ).
cnf(t151,plain,
$false,
inference(connection,[status(thm),parent(t150:1)],[t150:1,t148:2]) ).
cnf(t152,plain,
cC36xcomp(iV16448),
inference(extension,[status(thm),parent(t148:3)],[f_169_2]) ).
cnf(t153,plain,
$false,
inference(connection,[status(thm),parent(t152:1)],[t152:1,t148:3]) ).
cnf(t154,plain,
cowlThing(iV16440),
inference(extension,[status(thm),parent(t2:37)],[f_154_2]) ).
cnf(t155,plain,
$false,
inference(connection,[status(thm),parent(t154:1)],[t154:1,t2:37]) ).
cnf(t156,plain,
( ~ cC98(iV16440)
| cC82(iV16440) ),
inference(extension,[status(thm),parent(t2:38)],[f_144_5]) ).
cnf(t157,plain,
$false,
inference(connection,[status(thm),parent(t156:1)],[t156:1,t2:38]) ).
cnf(t158,plain,
( ~ rR1(iV16439,iV16440)
| cC98(iV16440) ),
inference(extension,[status(thm),parent(t156:2)],[f_147_3]) ).
cnf(t159,plain,
$false,
inference(connection,[status(thm),parent(t158:1)],[t158:1,t156:2]) ).
cnf(t160,plain,
rR1(iV16439,iV16440),
inference(extension,[status(thm),parent(t158:2)],[f_151_2]) ).
cnf(t161,plain,
$false,
inference(connection,[status(thm),parent(t160:1)],[t160:1,t158:2]) ).
cnf(l72,lemma,
cC82(iV16440),
inference(lemma,[status(cth),parent(t2:38),below(t1:1)],[t2:38]) ).
cnf(t162,plain,
( ~ cC82(iV16440)
| cC80(iV16440) ),
inference(extension,[status(thm),parent(t2:39)],[f_121_4]) ).
cnf(t163,plain,
$false,
inference(connection,[status(thm),parent(t162:1)],[t162:1,t2:39]) ).
cnf(t164,plain,
cC82(iV16440),
inference(lemma_extension,[status(thm),parent(t162:2)],[l72:1]) ).
cnf(t165,plain,
$false,
inference(connection,[status(thm),parent(t164:1)],[t164:1,t162:2]) ).
cnf(t166,plain,
( ~ rR1(iV16439,iV16440)
| cC98(iV16440) ),
inference(extension,[status(thm),parent(t2:40)],[f_147_3]) ).
cnf(t167,plain,
$false,
inference(connection,[status(thm),parent(t166:1)],[t166:1,t2:40]) ).
cnf(t168,plain,
rR1(iV16439,iV16440),
inference(extension,[status(thm),parent(t166:2)],[f_151_2]) ).
cnf(t169,plain,
$false,
inference(connection,[status(thm),parent(t168:1)],[t168:1,t166:2]) ).
cnf(t170,plain,
cowlThing(iV16439),
inference(extension,[status(thm),parent(t2:41)],[f_148_2]) ).
cnf(t171,plain,
$false,
inference(connection,[status(thm),parent(t170:1)],[t170:1,t2:41]) ).
cnf(t172,plain,
( ~ cC108(iV16439)
| cC28(iV16439) ),
inference(extension,[status(thm),parent(t2:42)],[f_13_4]) ).
cnf(t173,plain,
$false,
inference(connection,[status(thm),parent(t172:1)],[t172:1,t2:42]) ).
cnf(t174,plain,
( ~ cTEST(iV16439)
| cC108(iV16439) ),
inference(extension,[status(thm),parent(t172:2)],[f_146_4]) ).
cnf(t175,plain,
$false,
inference(connection,[status(thm),parent(t174:1)],[t174:1,t172:2]) ).
cnf(t176,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t174:2)],[f_150_2]) ).
cnf(t177,plain,
$false,
inference(connection,[status(thm),parent(t176:1)],[t176:1,t174:2]) ).
cnf(t178,plain,
( ~ cC108(iV16439)
| cC106(iV16439) ),
inference(extension,[status(thm),parent(t2:43)],[f_13_5]) ).
cnf(t179,plain,
$false,
inference(connection,[status(thm),parent(t178:1)],[t178:1,t2:43]) ).
cnf(t180,plain,
( ~ cTEST(iV16439)
| cC108(iV16439) ),
inference(extension,[status(thm),parent(t178:2)],[f_146_4]) ).
cnf(t181,plain,
$false,
inference(connection,[status(thm),parent(t180:1)],[t180:1,t178:2]) ).
cnf(t182,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t180:2)],[f_150_2]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t180:2]) ).
cnf(l82,lemma,
cC106(iV16439),
inference(lemma,[status(cth),parent(t2:43),below(t1:1)],[t2:43]) ).
cnf(t184,plain,
( ~ cC106(iV16439)
| cC104(iV16439) ),
inference(extension,[status(thm),parent(t2:44)],[f_12_4]) ).
cnf(t185,plain,
$false,
inference(connection,[status(thm),parent(t184:1)],[t184:1,t2:44]) ).
cnf(t186,plain,
cC106(iV16439),
inference(lemma_extension,[status(thm),parent(t184:2)],[l82:1]) ).
cnf(t187,plain,
$false,
inference(connection,[status(thm),parent(t186:1)],[t186:1,t184:2]) ).
cnf(t188,plain,
( ~ cTEST(iV16439)
| cC108(iV16439) ),
inference(extension,[status(thm),parent(t2:45)],[f_146_4]) ).
cnf(t189,plain,
$false,
inference(connection,[status(thm),parent(t188:1)],[t188:1,t2:45]) ).
cnf(t190,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t188:2)],[f_150_2]) ).
cnf(t191,plain,
$false,
inference(connection,[status(thm),parent(t190:1)],[t190:1,t188:2]) ).
cnf(t192,plain,
( ~ cTEST(iV16439)
| cC130(iV16439) ),
inference(extension,[status(thm),parent(t2:46)],[f_146_5]) ).
cnf(t193,plain,
$false,
inference(connection,[status(thm),parent(t192:1)],[t192:1,t2:46]) ).
cnf(t194,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t192:2)],[f_150_2]) ).
cnf(t195,plain,
$false,
inference(connection,[status(thm),parent(t194:1)],[t194:1,t192:2]) ).
cnf(t196,plain,
( ~ xsd_string(sK118)
| ~ sP1 ),
inference(extension,[status(thm),parent(t2:47)],[f_287_14]) ).
cnf(t197,plain,
$false,
inference(connection,[status(thm),parent(t196:1)],[t196:1,t2:47]) ).
cnf(t198,plain,
( xsd_integer(sK118)
| xsd_string(sK118) ),
inference(extension,[status(thm),parent(t196:2)],[f_2_5]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t196:2]) ).
cnf(t200,plain,
( ~ sP1
| ~ xsd_integer(sK118) ),
inference(extension,[status(thm),parent(t198:2)],[f_287_13]) ).
cnf(t201,plain,
$false,
inference(connection,[status(thm),parent(t200:1)],[t200:1,t198:2]) ).
cnf(t202,plain,
$false,
inference(reduction,[status(thm),parent(t200:2)],[t200:2,t2:47]) ).
cnf(t203,plain,
( xsd_integer(sK117)
| ~ sP0 ),
inference(extension,[status(thm),parent(t2:48)],[f_287_12]) ).
cnf(t204,plain,
$false,
inference(connection,[status(thm),parent(t203:1)],[t203:1,t2:48]) ).
cnf(t205,plain,
( ~ xsd_string(sK117)
| ~ xsd_integer(sK117) ),
inference(extension,[status(thm),parent(t203:2)],[f_2_4]) ).
cnf(t206,plain,
$false,
inference(connection,[status(thm),parent(t205:1)],[t205:1,t203:2]) ).
cnf(t207,plain,
( ~ sP0
| xsd_string(sK117) ),
inference(extension,[status(thm),parent(t205:2)],[f_287_11]) ).
cnf(t208,plain,
$false,
inference(connection,[status(thm),parent(t207:1)],[t207:1,t205:2]) ).
cnf(t209,plain,
$false,
inference(reduction,[status(thm),parent(t207:2)],[t207:2,t2:48]) ).
cnf(t210,plain,
cowlThing(iV16465),
inference(extension,[status(thm),parent(t2:49)],[f_277_2]) ).
cnf(t211,plain,
$false,
inference(connection,[status(thm),parent(t210:1)],[t210:1,t2:49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS161+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/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 19 12:17:08 UTC 2026
% 0.11/0.37 % CPUTime :
% 1.55/1.88 % SZS status Theorem for theBenchmark
% 1.55/1.88 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------