%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS153+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 : n017.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:23 AM UTC 2026
% Result : Theorem 33.05s 33.38s
% Output : Proof 33.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 65
% Syntax : Number of formulae : 600 ( 356 unt; 0 def)
% Number of atoms : 1789 ( 0 equ)
% Maximal formula atoms : 57 ( 2 avg)
% Number of connectives : 2147 ( 958 ~; 878 |; 285 &)
% ( 19 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 63 ( 62 usr; 3 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-1 aty)
% Number of variables : 270 ( 2 sgn 204 !; 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_5,axiom,
! [X] :
( cC106(X)
<=> ( cC104(X)
& ~ cC100(X) ) ),
file('theBenchmark.p',axiom_5) ).
fof(axiom_6,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_25,axiom,
! [X] :
( cC34(X)
<=> ( ~ cC30(X)
& ~ cC32(X) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_27,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& ~ cC36(X) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_29,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& ~ cC40(X) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_33,axiom,
! [X] :
( cC50(X)
<=> ( ~ cC48(X)
& ~ cC46(X) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_36,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& cC44(X) ) ),
file('theBenchmark.p',axiom_36) ).
fof(axiom_39,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC62(X)
<=> ( ~ cC58(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_43,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC66(X)
& ~ cC64(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_47,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& ~ cC74(X) ) ),
file('theBenchmark.p',axiom_47) ).
fof(axiom_50,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& ~ cC78(X) ) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_53,axiom,
! [X] :
( cC88(X)
<=> ( ~ cC86(X)
& ~ cC84(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_58,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& ~ cC96(X) ) ),
file('theBenchmark.p',axiom_58) ).
fof(axiom_59,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_60,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('theBenchmark.p',axiom_60) ).
fof(axiom_61,axiom,
cTEST(iV16439),
file('theBenchmark.p',axiom_61) ).
fof(axiom_63,axiom,
cowlThing(iV16439),
file('theBenchmark.p',axiom_63) ).
fof(axiom_64,axiom,
rR1(iV16439,iV16440),
file('theBenchmark.p',axiom_64) ).
fof(axiom_67,axiom,
! [X] :
( rR1(iV16440,X)
=> cC76(X) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_72,axiom,
cowlThing(iV16440),
file('theBenchmark.p',axiom_72) ).
fof(axiom_73,axiom,
rR1(iV16440,iV16463),
file('theBenchmark.p',axiom_73) ).
fof(axiom_76,axiom,
~ cC36(iV16448),
file('theBenchmark.p',axiom_76) ).
fof(axiom_79,axiom,
cTOP(iV16448),
file('theBenchmark.p',axiom_79) ).
fof(axiom_84,axiom,
cowlThing(iV16448),
file('theBenchmark.p',axiom_84) ).
fof(axiom_91,axiom,
~ cC58(iV16453),
file('theBenchmark.p',axiom_91) ).
fof(axiom_92,axiom,
~ cC74(iV16453),
file('theBenchmark.p',axiom_92) ).
fof(axiom_93,axiom,
! [X] :
( rR1(iV16453,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_93) ).
fof(axiom_94,axiom,
cowlThing(iV16453),
file('theBenchmark.p',axiom_94) ).
fof(axiom_96,axiom,
rR1(iV16453,iV16461),
file('theBenchmark.p',axiom_96) ).
fof(axiom_98,axiom,
~ cC40(iV16455),
file('theBenchmark.p',axiom_98) ).
fof(axiom_103,axiom,
~ cC54(iV16455),
file('theBenchmark.p',axiom_103) ).
fof(axiom_105,axiom,
cowlThing(iV16455),
file('theBenchmark.p',axiom_105) ).
fof(axiom_106,axiom,
! [X] :
( rR1(iV16455,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_106) ).
fof(axiom_107,axiom,
rR1(iV16455,iV16460),
file('theBenchmark.p',axiom_107) ).
fof(axiom_108,axiom,
~ cC36(iV16457),
file('theBenchmark.p',axiom_108) ).
fof(axiom_113,axiom,
cTOP(iV16457),
file('theBenchmark.p',axiom_113) ).
fof(axiom_117,axiom,
cowlThing(iV16457),
file('theBenchmark.p',axiom_117) ).
fof(axiom_120,axiom,
~ cC48(iV16459),
file('theBenchmark.p',axiom_120) ).
fof(axiom_121,axiom,
~ cC30(iV16459),
file('theBenchmark.p',axiom_121) ).
fof(axiom_123,axiom,
~ cC86(iV16459),
file('theBenchmark.p',axiom_123) ).
fof(axiom_124,axiom,
~ cC46(iV16459),
file('theBenchmark.p',axiom_124) ).
fof(axiom_127,axiom,
~ cC66(iV16459),
file('theBenchmark.p',axiom_127) ).
fof(axiom_132,axiom,
~ cC84(iV16459),
file('theBenchmark.p',axiom_132) ).
fof(axiom_133,axiom,
~ cC64(iV16459),
file('theBenchmark.p',axiom_133) ).
fof(axiom_134,axiom,
cowlThing(iV16459),
file('theBenchmark.p',axiom_134) ).
fof(axiom_135,axiom,
~ cC32(iV16459),
file('theBenchmark.p',axiom_135) ).
fof(axiom_141,axiom,
~ cC8(iV16460),
file('theBenchmark.p',axiom_141) ).
fof(axiom_146,axiom,
cowlThing(iV16460),
file('theBenchmark.p',axiom_146) ).
fof(axiom_151,axiom,
~ cC12(iV16461),
file('theBenchmark.p',axiom_151) ).
fof(axiom_154,axiom,
! [X] :
( rR1(iV16461,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_154) ).
fof(axiom_155,axiom,
cowlThing(iV16461),
file('theBenchmark.p',axiom_155) ).
fof(axiom_157,axiom,
rR1(iV16461,iV16462),
file('theBenchmark.p',axiom_157) ).
fof(axiom_168,axiom,
cowlThing(iV16462),
file('theBenchmark.p',axiom_168) ).
fof(axiom_171,axiom,
! [X] :
( rR1(iV16463,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_171) ).
fof(axiom_176,axiom,
cowlThing(iV16463),
file('theBenchmark.p',axiom_176) ).
fof(axiom_177,axiom,
rR1(iV16463,iV16464),
file('theBenchmark.p',axiom_177) ).
fof(axiom_182,axiom,
! [X] :
( rR1(iV16464,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_182) ).
fof(axiom_187,axiom,
cowlThing(iV16464),
file('theBenchmark.p',axiom_187) ).
fof(axiom_188,axiom,
rR1(iV16464,iV16465),
file('theBenchmark.p',axiom_188) ).
fof(axiom_198,axiom,
cowlThing(iV16465),
file('theBenchmark.p',axiom_198) ).
fof(the_axiom,conjecture,
( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(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]) ).
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_6_1,plain,
! [X] :
( ( cC106(X)
| ~ cC104(X)
| cC100(X) )
& ( ( cC104(X)
& ~ cC100(X) )
| ~ cC106(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_5]) ).
fof(f_6_2,plain,
! [U_19] :
( ( cC106(U_19)
| ~ cC104(U_19)
| cC100(U_19) )
& ( ( cC104(U_19)
& ~ cC100(U_19) )
| ~ cC106(U_19) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_21] :
( cC106(U_21)
| ~ cC104(U_21)
| cC100(U_21) )
& ! [U_20] :
( ( cC104(U_20)
& ~ cC100(U_20) )
| ~ cC106(U_20) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_20] :
( cC104(U_20)
| ~ sP3(U_20) )
& ! [U_20] :
( ~ cC100(U_20)
| ~ sP3(U_20) )
& ! [U_21] :
( cC106(U_21)
| ~ cC104(U_21)
| cC100(U_21) )
& ! [U_20] :
( sP3(U_20)
| ~ cC106(U_20) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP3])],[f_6_3]) ).
cnf(f_6_5,plain,
( sP3(U_20)
| ~ cC106(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_8,plain,
( cC104(U_20)
| ~ sP3(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
fof(f_7_1,plain,
! [X] :
( ( cC108(X)
| ~ cC106(X)
| ~ cC28(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_6]) ).
fof(f_7_2,plain,
! [U_22] :
( ( cC108(U_22)
| ~ cC106(U_22)
| ~ cC28(U_22) )
& ( ( cC106(U_22)
& cC28(U_22) )
| ~ cC108(U_22) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_24] :
( cC108(U_24)
| ~ cC106(U_24)
| ~ cC28(U_24) )
& ! [U_23] :
( ( cC106(U_23)
& cC28(U_23) )
| ~ cC108(U_23) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_23] :
( cC106(U_23)
| ~ sP4(U_23) )
& ! [U_23] :
( cC28(U_23)
| ~ sP4(U_23) )
& ! [U_24] :
( cC108(U_24)
| ~ cC106(U_24)
| ~ cC28(U_24) )
& ! [U_23] :
( sP4(U_23)
| ~ cC108(U_23) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP4])],[f_7_3]) ).
cnf(f_7_5,plain,
( sP4(U_23)
| ~ cC108(U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_7,plain,
( cC28(U_23)
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_8,plain,
( cC106(U_23)
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
fof(f_26_1,plain,
! [X] :
( ( cC34(X)
| cC30(X)
| cC32(X) )
& ( ( ~ cC30(X)
& ~ cC32(X) )
| ~ cC34(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_25]) ).
fof(f_26_2,plain,
! [U_99] :
( ( cC34(U_99)
| cC30(U_99)
| cC32(U_99) )
& ( ( ~ cC30(U_99)
& ~ cC32(U_99) )
| ~ cC34(U_99) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_101] :
( cC34(U_101)
| cC30(U_101)
| cC32(U_101) )
& ! [U_100] :
( ( ~ cC30(U_100)
& ~ cC32(U_100) )
| ~ cC34(U_100) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
fof(f_26_4,plain,
( ! [U_100] :
( ~ cC30(U_100)
| ~ sP23(U_100) )
& ! [U_100] :
( ~ cC32(U_100)
| ~ sP23(U_100) )
& ! [U_101] :
( cC34(U_101)
| cC30(U_101)
| cC32(U_101) )
& ! [U_100] :
( sP23(U_100)
| ~ cC34(U_100) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP23])],[f_26_3]) ).
cnf(f_26_6,plain,
( cC34(U_101)
| cC30(U_101)
| cC32(U_101) ),
inference(clausify,[status(thm)],[f_26_4]) ).
fof(f_28_1,plain,
! [X] :
( ( cC38(X)
| ~ cTOP(X)
| cC36(X) )
& ( ( cTOP(X)
& ~ cC36(X) )
| ~ cC38(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_27]) ).
fof(f_28_2,plain,
! [U_107] :
( ( cC38(U_107)
| ~ cTOP(U_107)
| cC36(U_107) )
& ( ( cTOP(U_107)
& ~ cC36(U_107) )
| ~ cC38(U_107) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_109] :
( cC38(U_109)
| ~ cTOP(U_109)
| cC36(U_109) )
& ! [U_108] :
( ( cTOP(U_108)
& ~ cC36(U_108) )
| ~ cC38(U_108) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
fof(f_28_4,plain,
( ! [U_108] :
( cTOP(U_108)
| ~ sP25(U_108) )
& ! [U_108] :
( ~ cC36(U_108)
| ~ sP25(U_108) )
& ! [U_109] :
( cC38(U_109)
| ~ cTOP(U_109)
| cC36(U_109) )
& ! [U_108] :
( sP25(U_108)
| ~ cC38(U_108) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP25])],[f_28_3]) ).
cnf(f_28_6,plain,
( cC38(U_109)
| ~ cTOP(U_109)
| cC36(U_109) ),
inference(clausify,[status(thm)],[f_28_4]) ).
fof(f_30_1,plain,
! [X] :
( ( cC42(X)
| ! [Y] :
( cC8(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_29]) ).
fof(f_30_2,plain,
! [U_117] :
( ( cC42(U_117)
| ! [U_116] :
( cC8(U_116)
| ~ rR1(U_117,U_116) ) )
& ( ? [U_115] :
( ~ cC8(U_115)
& rR1(U_117,U_115) )
| ~ cC42(U_117) ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_119] :
( cC42(U_119)
| ! [U_116] :
( cC8(U_116)
| ~ rR1(U_119,U_116) ) )
& ! [U_118] :
( ? [U_115] :
( ~ cC8(U_115)
& rR1(U_118,U_115) )
| ~ cC42(U_118) ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
fof(f_30_4,plain,
( ! [U_119] :
( cC42(U_119)
| ! [U_116] :
( cC8(U_116)
| ~ rR1(U_119,U_116) ) )
& ! [U_118] :
( ( ~ cC8(sK15(U_118))
& rR1(U_118,sK15(U_118)) )
| ~ cC42(U_118) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_115,sK15(U_118))],[f_30_3]) ).
fof(f_30_5,plain,
( ! [U_118] :
( ~ cC8(sK15(U_118))
| ~ sP27(U_118) )
& ! [U_118] :
( rR1(U_118,sK15(U_118))
| ~ sP27(U_118) )
& ! [U_119,U_116] :
( cC42(U_119)
| cC8(U_116)
| ~ rR1(U_119,U_116) )
& ! [U_118] :
( sP27(U_118)
| ~ cC42(U_118) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP27])],[f_30_4]) ).
cnf(f_30_7,plain,
( cC42(U_119)
| cC8(U_116)
| ~ rR1(U_119,U_116) ),
inference(clausify,[status(thm)],[f_30_5]) ).
fof(f_31_1,plain,
! [X] :
( ( cC44(X)
| ~ cC42(X)
| cC40(X) )
& ( ( cC42(X)
& ~ cC40(X) )
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_30]) ).
fof(f_31_2,plain,
! [U_120] :
( ( cC44(U_120)
| ~ cC42(U_120)
| cC40(U_120) )
& ( ( cC42(U_120)
& ~ cC40(U_120) )
| ~ cC44(U_120) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_122] :
( cC44(U_122)
| ~ cC42(U_122)
| cC40(U_122) )
& ! [U_121] :
( ( cC42(U_121)
& ~ cC40(U_121) )
| ~ cC44(U_121) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
fof(f_31_4,plain,
( ! [U_121] :
( cC42(U_121)
| ~ sP28(U_121) )
& ! [U_121] :
( ~ cC40(U_121)
| ~ sP28(U_121) )
& ! [U_122] :
( cC44(U_122)
| ~ cC42(U_122)
| cC40(U_122) )
& ! [U_121] :
( sP28(U_121)
| ~ cC44(U_121) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP28])],[f_31_3]) ).
cnf(f_31_5,plain,
( sP28(U_121)
| ~ cC44(U_121) ),
inference(clausify,[status(thm)],[f_31_4]) ).
cnf(f_31_6,plain,
( cC44(U_122)
| ~ cC42(U_122)
| cC40(U_122) ),
inference(clausify,[status(thm)],[f_31_4]) ).
cnf(f_31_8,plain,
( cC42(U_121)
| ~ sP28(U_121) ),
inference(clausify,[status(thm)],[f_31_4]) ).
fof(f_34_1,plain,
! [X] :
( ( cC50(X)
| cC48(X)
| cC46(X) )
& ( ( ~ cC48(X)
& ~ cC46(X) )
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_33]) ).
fof(f_34_2,plain,
! [U_129] :
( ( cC50(U_129)
| cC48(U_129)
| cC46(U_129) )
& ( ( ~ cC48(U_129)
& ~ cC46(U_129) )
| ~ cC50(U_129) ) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
( ! [U_131] :
( cC50(U_131)
| cC48(U_131)
| cC46(U_131) )
& ! [U_130] :
( ( ~ cC48(U_130)
& ~ cC46(U_130) )
| ~ cC50(U_130) ) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
fof(f_34_4,plain,
( ! [U_130] :
( ~ cC48(U_130)
| ~ sP31(U_130) )
& ! [U_130] :
( ~ cC46(U_130)
| ~ sP31(U_130) )
& ! [U_131] :
( cC50(U_131)
| cC48(U_131)
| cC46(U_131) )
& ! [U_130] :
( sP31(U_130)
| ~ cC50(U_130) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP31])],[f_34_3]) ).
cnf(f_34_6,plain,
( cC50(U_131)
| cC48(U_131)
| cC46(U_131) ),
inference(clausify,[status(thm)],[f_34_4]) ).
fof(f_37_1,plain,
! [X] :
( ( cC56(X)
| cC54(X)
| ~ cC44(X) )
& ( ( ~ cC54(X)
& cC44(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_36]) ).
fof(f_37_2,plain,
! [U_142] :
( ( cC56(U_142)
| cC54(U_142)
| ~ cC44(U_142) )
& ( ( ~ cC54(U_142)
& cC44(U_142) )
| ~ cC56(U_142) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_144] :
( cC56(U_144)
| cC54(U_144)
| ~ cC44(U_144) )
& ! [U_143] :
( ( ~ cC54(U_143)
& cC44(U_143) )
| ~ cC56(U_143) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
fof(f_37_4,plain,
( ! [U_143] :
( ~ cC54(U_143)
| ~ sP34(U_143) )
& ! [U_143] :
( cC44(U_143)
| ~ sP34(U_143) )
& ! [U_144] :
( cC56(U_144)
| cC54(U_144)
| ~ cC44(U_144) )
& ! [U_143] :
( sP34(U_143)
| ~ cC56(U_143) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP34])],[f_37_3]) ).
cnf(f_37_5,plain,
( sP34(U_143)
| ~ cC56(U_143) ),
inference(clausify,[status(thm)],[f_37_4]) ).
cnf(f_37_6,plain,
( cC56(U_144)
| cC54(U_144)
| ~ cC44(U_144) ),
inference(clausify,[status(thm)],[f_37_4]) ).
cnf(f_37_7,plain,
( cC44(U_143)
| ~ sP34(U_143) ),
inference(clausify,[status(thm)],[f_37_4]) ).
fof(f_40_1,plain,
! [X] :
( ( cC60(X)
| ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_39]) ).
fof(f_40_2,plain,
! [U_155] :
( ( cC60(U_155)
| ! [U_154] :
( cC12(U_154)
| ~ rR1(U_155,U_154) ) )
& ( ? [U_153] :
( ~ cC12(U_153)
& rR1(U_155,U_153) )
| ~ cC60(U_155) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_157] :
( cC60(U_157)
| ! [U_154] :
( cC12(U_154)
| ~ rR1(U_157,U_154) ) )
& ! [U_156] :
( ? [U_153] :
( ~ cC12(U_153)
& rR1(U_156,U_153) )
| ~ cC60(U_156) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
fof(f_40_4,plain,
( ! [U_157] :
( cC60(U_157)
| ! [U_154] :
( cC12(U_154)
| ~ rR1(U_157,U_154) ) )
& ! [U_156] :
( ( ~ cC12(sK19(U_156))
& rR1(U_156,sK19(U_156)) )
| ~ cC60(U_156) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_153,sK19(U_156))],[f_40_3]) ).
fof(f_40_5,plain,
( ! [U_156] :
( ~ cC12(sK19(U_156))
| ~ sP37(U_156) )
& ! [U_156] :
( rR1(U_156,sK19(U_156))
| ~ sP37(U_156) )
& ! [U_157,U_154] :
( cC60(U_157)
| cC12(U_154)
| ~ rR1(U_157,U_154) )
& ! [U_156] :
( sP37(U_156)
| ~ cC60(U_156) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP37])],[f_40_4]) ).
cnf(f_40_7,plain,
( cC60(U_157)
| cC12(U_154)
| ~ rR1(U_157,U_154) ),
inference(clausify,[status(thm)],[f_40_5]) ).
fof(f_41_1,plain,
! [X] :
( ( cC62(X)
| cC58(X)
| ~ cC60(X) )
& ( ( ~ cC58(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_158] :
( ( cC62(U_158)
| cC58(U_158)
| ~ cC60(U_158) )
& ( ( ~ cC58(U_158)
& cC60(U_158) )
| ~ cC62(U_158) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_160] :
( cC62(U_160)
| cC58(U_160)
| ~ cC60(U_160) )
& ! [U_159] :
( ( ~ cC58(U_159)
& cC60(U_159) )
| ~ cC62(U_159) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
fof(f_41_4,plain,
( ! [U_159] :
( ~ cC58(U_159)
| ~ sP38(U_159) )
& ! [U_159] :
( cC60(U_159)
| ~ sP38(U_159) )
& ! [U_160] :
( cC62(U_160)
| cC58(U_160)
| ~ cC60(U_160) )
& ! [U_159] :
( sP38(U_159)
| ~ cC62(U_159) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP38])],[f_41_3]) ).
cnf(f_41_5,plain,
( sP38(U_159)
| ~ cC62(U_159) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_6,plain,
( cC62(U_160)
| cC58(U_160)
| ~ cC60(U_160) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_7,plain,
( cC60(U_159)
| ~ sP38(U_159) ),
inference(clausify,[status(thm)],[f_41_4]) ).
fof(f_44_1,plain,
! [X] :
( ( cC68(X)
| cC66(X)
| cC64(X) )
& ( ( ~ cC66(X)
& ~ cC64(X) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_167] :
( ( cC68(U_167)
| cC66(U_167)
| cC64(U_167) )
& ( ( ~ cC66(U_167)
& ~ cC64(U_167) )
| ~ cC68(U_167) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_169] :
( cC68(U_169)
| cC66(U_169)
| cC64(U_169) )
& ! [U_168] :
( ( ~ cC66(U_168)
& ~ cC64(U_168) )
| ~ cC68(U_168) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
fof(f_44_4,plain,
( ! [U_168] :
( ~ cC66(U_168)
| ~ sP41(U_168) )
& ! [U_168] :
( ~ cC64(U_168)
| ~ sP41(U_168) )
& ! [U_169] :
( cC68(U_169)
| cC66(U_169)
| cC64(U_169) )
& ! [U_168] :
( sP41(U_168)
| ~ cC68(U_168) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP41])],[f_44_3]) ).
cnf(f_44_6,plain,
( cC68(U_169)
| cC66(U_169)
| cC64(U_169) ),
inference(clausify,[status(thm)],[f_44_4]) ).
fof(f_48_1,plain,
! [X] :
( ( cC76(X)
| ~ cC62(X)
| cC74(X) )
& ( ( cC62(X)
& ~ cC74(X) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_47]) ).
fof(f_48_2,plain,
! [U_185] :
( ( cC76(U_185)
| ~ cC62(U_185)
| cC74(U_185) )
& ( ( cC62(U_185)
& ~ cC74(U_185) )
| ~ cC76(U_185) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_187] :
( cC76(U_187)
| ~ cC62(U_187)
| cC74(U_187) )
& ! [U_186] :
( ( cC62(U_186)
& ~ cC74(U_186) )
| ~ cC76(U_186) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
fof(f_48_4,plain,
( ! [U_186] :
( cC62(U_186)
| ~ sP45(U_186) )
& ! [U_186] :
( ~ cC74(U_186)
| ~ sP45(U_186) )
& ! [U_187] :
( cC76(U_187)
| ~ cC62(U_187)
| cC74(U_187) )
& ! [U_186] :
( sP45(U_186)
| ~ cC76(U_186) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP45])],[f_48_3]) ).
cnf(f_48_5,plain,
( sP45(U_186)
| ~ cC76(U_186) ),
inference(clausify,[status(thm)],[f_48_4]) ).
cnf(f_48_6,plain,
( cC76(U_187)
| ~ cC62(U_187)
| cC74(U_187) ),
inference(clausify,[status(thm)],[f_48_4]) ).
cnf(f_48_8,plain,
( cC62(U_186)
| ~ sP45(U_186) ),
inference(clausify,[status(thm)],[f_48_4]) ).
fof(f_51_1,plain,
! [X] :
( ( cC82(X)
| ~ cC80(X)
| cC78(X) )
& ( ( cC80(X)
& ~ cC78(X) )
| ~ cC82(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_50]) ).
fof(f_51_2,plain,
! [U_198] :
( ( cC82(U_198)
| ~ cC80(U_198)
| cC78(U_198) )
& ( ( cC80(U_198)
& ~ cC78(U_198) )
| ~ cC82(U_198) ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_200] :
( cC82(U_200)
| ~ cC80(U_200)
| cC78(U_200) )
& ! [U_199] :
( ( cC80(U_199)
& ~ cC78(U_199) )
| ~ cC82(U_199) ) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
fof(f_51_4,plain,
( ! [U_199] :
( cC80(U_199)
| ~ sP48(U_199) )
& ! [U_199] :
( ~ cC78(U_199)
| ~ sP48(U_199) )
& ! [U_200] :
( cC82(U_200)
| ~ cC80(U_200)
| cC78(U_200) )
& ! [U_199] :
( sP48(U_199)
| ~ cC82(U_199) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP48])],[f_51_3]) ).
cnf(f_51_5,plain,
( sP48(U_199)
| ~ cC82(U_199) ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_8,plain,
( cC80(U_199)
| ~ sP48(U_199) ),
inference(clausify,[status(thm)],[f_51_4]) ).
fof(f_54_1,plain,
! [X] :
( ( cC88(X)
| cC86(X)
| cC84(X) )
& ( ( ~ cC86(X)
& ~ cC84(X) )
| ~ cC88(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_53]) ).
fof(f_54_2,plain,
! [U_207] :
( ( cC88(U_207)
| cC86(U_207)
| cC84(U_207) )
& ( ( ~ cC86(U_207)
& ~ cC84(U_207) )
| ~ cC88(U_207) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_209] :
( cC88(U_209)
| cC86(U_209)
| cC84(U_209) )
& ! [U_208] :
( ( ~ cC86(U_208)
& ~ cC84(U_208) )
| ~ cC88(U_208) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
fof(f_54_4,plain,
( ! [U_208] :
( ~ cC86(U_208)
| ~ sP51(U_208) )
& ! [U_208] :
( ~ cC84(U_208)
| ~ sP51(U_208) )
& ! [U_209] :
( cC88(U_209)
| cC86(U_209)
| cC84(U_209) )
& ! [U_208] :
( sP51(U_208)
| ~ cC88(U_208) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP51])],[f_54_3]) ).
cnf(f_54_6,plain,
( cC88(U_209)
| cC86(U_209)
| cC84(U_209) ),
inference(clausify,[status(thm)],[f_54_4]) ).
fof(f_59_1,plain,
! [X] :
( ( cC98(X)
| ~ cC82(X)
| cC96(X) )
& ( ( cC82(X)
& ~ cC96(X) )
| ~ cC98(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_58]) ).
fof(f_59_2,plain,
! [U_230] :
( ( cC98(U_230)
| ~ cC82(U_230)
| cC96(U_230) )
& ( ( cC82(U_230)
& ~ cC96(U_230) )
| ~ cC98(U_230) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_232] :
( cC98(U_232)
| ~ cC82(U_232)
| cC96(U_232) )
& ! [U_231] :
( ( cC82(U_231)
& ~ cC96(U_231) )
| ~ cC98(U_231) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
fof(f_59_4,plain,
( ! [U_231] :
( cC82(U_231)
| ~ sP56(U_231) )
& ! [U_231] :
( ~ cC96(U_231)
| ~ sP56(U_231) )
& ! [U_232] :
( cC98(U_232)
| ~ cC82(U_232)
| cC96(U_232) )
& ! [U_231] :
( sP56(U_231)
| ~ cC98(U_231) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP56])],[f_59_3]) ).
cnf(f_59_5,plain,
( sP56(U_231)
| ~ cC98(U_231) ),
inference(clausify,[status(thm)],[f_59_4]) ).
cnf(f_59_8,plain,
( cC82(U_231)
| ~ sP56(U_231) ),
inference(clausify,[status(thm)],[f_59_4]) ).
fof(f_60_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC130(X)
| ~ cC108(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_59]) ).
fof(f_60_2,plain,
! [U_233] :
( ( cTEST(U_233)
| ~ cC130(U_233)
| ~ cC108(U_233) )
& ( ( cC130(U_233)
& cC108(U_233) )
| ~ cTEST(U_233) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_235] :
( cTEST(U_235)
| ~ cC130(U_235)
| ~ cC108(U_235) )
& ! [U_234] :
( ( cC130(U_234)
& cC108(U_234) )
| ~ cTEST(U_234) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
fof(f_60_4,plain,
( ! [U_234] :
( cC130(U_234)
| ~ sP57(U_234) )
& ! [U_234] :
( cC108(U_234)
| ~ sP57(U_234) )
& ! [U_235] :
( cTEST(U_235)
| ~ cC130(U_235)
| ~ cC108(U_235) )
& ! [U_234] :
( sP57(U_234)
| ~ cTEST(U_234) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP57])],[f_60_3]) ).
cnf(f_60_5,plain,
( sP57(U_234)
| ~ cTEST(U_234) ),
inference(clausify,[status(thm)],[f_60_4]) ).
cnf(f_60_7,plain,
( cC108(U_234)
| ~ sP57(U_234) ),
inference(clausify,[status(thm)],[f_60_4]) ).
cnf(f_60_8,plain,
( cC130(U_234)
| ~ sP57(U_234) ),
inference(clausify,[status(thm)],[f_60_4]) ).
fof(f_61_1,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(fof_nnf,[status(thm)],[axiom_60]) ).
fof(f_61_2,plain,
! [U_236] :
( cC98(U_236)
| ~ rR1(iV16439,U_236) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
! [U_236] :
( cC98(U_236)
| ~ rR1(iV16439,U_236) ),
inference(definitional_conversion,[status(esa)],[f_61_2]) ).
cnf(f_61_4,plain,
( cC98(U_236)
| ~ rR1(iV16439,U_236) ),
inference(clausify,[status(thm)],[f_61_3]) ).
fof(f_62_1,plain,
cTEST(iV16439),
inference(fof_nnf,[status(thm)],[axiom_61]) ).
fof(f_62_2,plain,
cTEST(iV16439),
inference(definitional_conversion,[status(esa)],[f_62_1]) ).
cnf(f_62_3,plain,
cTEST(iV16439),
inference(clausify,[status(thm)],[f_62_2]) ).
fof(f_64_1,plain,
cowlThing(iV16439),
inference(fof_nnf,[status(thm)],[axiom_63]) ).
fof(f_64_2,plain,
cowlThing(iV16439),
inference(definitional_conversion,[status(esa)],[f_64_1]) ).
cnf(f_64_3,plain,
cowlThing(iV16439),
inference(clausify,[status(thm)],[f_64_2]) ).
fof(f_65_1,plain,
rR1(iV16439,iV16440),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
rR1(iV16439,iV16440),
inference(definitional_conversion,[status(esa)],[f_65_1]) ).
cnf(f_65_3,plain,
rR1(iV16439,iV16440),
inference(clausify,[status(thm)],[f_65_2]) ).
fof(f_68_1,plain,
! [X] :
( cC76(X)
| ~ rR1(iV16440,X) ),
inference(fof_nnf,[status(thm)],[axiom_67]) ).
fof(f_68_2,plain,
! [U_237] :
( cC76(U_237)
| ~ rR1(iV16440,U_237) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
! [U_237] :
( cC76(U_237)
| ~ rR1(iV16440,U_237) ),
inference(definitional_conversion,[status(esa)],[f_68_2]) ).
cnf(f_68_4,plain,
( cC76(U_237)
| ~ rR1(iV16440,U_237) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_73_1,plain,
cowlThing(iV16440),
inference(fof_nnf,[status(thm)],[axiom_72]) ).
fof(f_73_2,plain,
cowlThing(iV16440),
inference(definitional_conversion,[status(esa)],[f_73_1]) ).
cnf(f_73_3,plain,
cowlThing(iV16440),
inference(clausify,[status(thm)],[f_73_2]) ).
fof(f_74_1,plain,
rR1(iV16440,iV16463),
inference(fof_nnf,[status(thm)],[axiom_73]) ).
fof(f_74_2,plain,
rR1(iV16440,iV16463),
inference(definitional_conversion,[status(esa)],[f_74_1]) ).
cnf(f_74_3,plain,
rR1(iV16440,iV16463),
inference(clausify,[status(thm)],[f_74_2]) ).
fof(f_77_1,plain,
~ cC36(iV16448),
inference(fof_nnf,[status(thm)],[axiom_76]) ).
fof(f_77_2,plain,
~ cC36(iV16448),
inference(definitional_conversion,[status(esa)],[f_77_1]) ).
cnf(f_77_3,plain,
~ cC36(iV16448),
inference(clausify,[status(thm)],[f_77_2]) ).
fof(f_80_1,plain,
cTOP(iV16448),
inference(fof_nnf,[status(thm)],[axiom_79]) ).
fof(f_80_2,plain,
cTOP(iV16448),
inference(definitional_conversion,[status(esa)],[f_80_1]) ).
cnf(f_80_3,plain,
cTOP(iV16448),
inference(clausify,[status(thm)],[f_80_2]) ).
fof(f_85_1,plain,
cowlThing(iV16448),
inference(fof_nnf,[status(thm)],[axiom_84]) ).
fof(f_85_2,plain,
cowlThing(iV16448),
inference(definitional_conversion,[status(esa)],[f_85_1]) ).
cnf(f_85_3,plain,
cowlThing(iV16448),
inference(clausify,[status(thm)],[f_85_2]) ).
fof(f_92_1,plain,
~ cC58(iV16453),
inference(fof_nnf,[status(thm)],[axiom_91]) ).
fof(f_92_2,plain,
~ cC58(iV16453),
inference(definitional_conversion,[status(esa)],[f_92_1]) ).
cnf(f_92_3,plain,
~ cC58(iV16453),
inference(clausify,[status(thm)],[f_92_2]) ).
fof(f_93_1,plain,
~ cC74(iV16453),
inference(fof_nnf,[status(thm)],[axiom_92]) ).
fof(f_93_2,plain,
~ cC74(iV16453),
inference(definitional_conversion,[status(esa)],[f_93_1]) ).
cnf(f_93_3,plain,
~ cC74(iV16453),
inference(clausify,[status(thm)],[f_93_2]) ).
fof(f_94_1,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16453,X) ),
inference(fof_nnf,[status(thm)],[axiom_93]) ).
fof(f_94_2,plain,
! [U_245] :
( cC56(U_245)
| ~ rR1(iV16453,U_245) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
fof(f_94_3,plain,
! [U_245] :
( cC56(U_245)
| ~ rR1(iV16453,U_245) ),
inference(definitional_conversion,[status(esa)],[f_94_2]) ).
cnf(f_94_4,plain,
( cC56(U_245)
| ~ rR1(iV16453,U_245) ),
inference(clausify,[status(thm)],[f_94_3]) ).
fof(f_95_1,plain,
cowlThing(iV16453),
inference(fof_nnf,[status(thm)],[axiom_94]) ).
fof(f_95_2,plain,
cowlThing(iV16453),
inference(definitional_conversion,[status(esa)],[f_95_1]) ).
cnf(f_95_3,plain,
cowlThing(iV16453),
inference(clausify,[status(thm)],[f_95_2]) ).
fof(f_97_1,plain,
rR1(iV16453,iV16461),
inference(fof_nnf,[status(thm)],[axiom_96]) ).
fof(f_97_2,plain,
rR1(iV16453,iV16461),
inference(definitional_conversion,[status(esa)],[f_97_1]) ).
cnf(f_97_3,plain,
rR1(iV16453,iV16461),
inference(clausify,[status(thm)],[f_97_2]) ).
fof(f_99_1,plain,
~ cC40(iV16455),
inference(fof_nnf,[status(thm)],[axiom_98]) ).
fof(f_99_2,plain,
~ cC40(iV16455),
inference(definitional_conversion,[status(esa)],[f_99_1]) ).
cnf(f_99_3,plain,
~ cC40(iV16455),
inference(clausify,[status(thm)],[f_99_2]) ).
fof(f_104_1,plain,
~ cC54(iV16455),
inference(fof_nnf,[status(thm)],[axiom_103]) ).
fof(f_104_2,plain,
~ cC54(iV16455),
inference(definitional_conversion,[status(esa)],[f_104_1]) ).
cnf(f_104_3,plain,
~ cC54(iV16455),
inference(clausify,[status(thm)],[f_104_2]) ).
fof(f_106_1,plain,
cowlThing(iV16455),
inference(fof_nnf,[status(thm)],[axiom_105]) ).
fof(f_106_2,plain,
cowlThing(iV16455),
inference(definitional_conversion,[status(esa)],[f_106_1]) ).
cnf(f_106_3,plain,
cowlThing(iV16455),
inference(clausify,[status(thm)],[f_106_2]) ).
fof(f_107_1,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16455,X) ),
inference(fof_nnf,[status(thm)],[axiom_106]) ).
fof(f_107_2,plain,
! [U_249] :
( cC38(U_249)
| ~ rR1(iV16455,U_249) ),
inference(variable_rename,[status(thm)],[f_107_1]) ).
fof(f_107_3,plain,
! [U_249] :
( cC38(U_249)
| ~ rR1(iV16455,U_249) ),
inference(definitional_conversion,[status(esa)],[f_107_2]) ).
cnf(f_107_4,plain,
( cC38(U_249)
| ~ rR1(iV16455,U_249) ),
inference(clausify,[status(thm)],[f_107_3]) ).
fof(f_108_1,plain,
rR1(iV16455,iV16460),
inference(fof_nnf,[status(thm)],[axiom_107]) ).
fof(f_108_2,plain,
rR1(iV16455,iV16460),
inference(definitional_conversion,[status(esa)],[f_108_1]) ).
cnf(f_108_3,plain,
rR1(iV16455,iV16460),
inference(clausify,[status(thm)],[f_108_2]) ).
fof(f_109_1,plain,
~ cC36(iV16457),
inference(fof_nnf,[status(thm)],[axiom_108]) ).
fof(f_109_2,plain,
~ cC36(iV16457),
inference(definitional_conversion,[status(esa)],[f_109_1]) ).
cnf(f_109_3,plain,
~ cC36(iV16457),
inference(clausify,[status(thm)],[f_109_2]) ).
fof(f_114_1,plain,
cTOP(iV16457),
inference(fof_nnf,[status(thm)],[axiom_113]) ).
fof(f_114_2,plain,
cTOP(iV16457),
inference(definitional_conversion,[status(esa)],[f_114_1]) ).
cnf(f_114_3,plain,
cTOP(iV16457),
inference(clausify,[status(thm)],[f_114_2]) ).
fof(f_118_1,plain,
cowlThing(iV16457),
inference(fof_nnf,[status(thm)],[axiom_117]) ).
fof(f_118_2,plain,
cowlThing(iV16457),
inference(definitional_conversion,[status(esa)],[f_118_1]) ).
cnf(f_118_3,plain,
cowlThing(iV16457),
inference(clausify,[status(thm)],[f_118_2]) ).
fof(f_121_1,plain,
~ cC48(iV16459),
inference(fof_nnf,[status(thm)],[axiom_120]) ).
fof(f_121_2,plain,
~ cC48(iV16459),
inference(definitional_conversion,[status(esa)],[f_121_1]) ).
cnf(f_121_3,plain,
~ cC48(iV16459),
inference(clausify,[status(thm)],[f_121_2]) ).
fof(f_122_1,plain,
~ cC30(iV16459),
inference(fof_nnf,[status(thm)],[axiom_121]) ).
fof(f_122_2,plain,
~ cC30(iV16459),
inference(definitional_conversion,[status(esa)],[f_122_1]) ).
cnf(f_122_3,plain,
~ cC30(iV16459),
inference(clausify,[status(thm)],[f_122_2]) ).
fof(f_124_1,plain,
~ cC86(iV16459),
inference(fof_nnf,[status(thm)],[axiom_123]) ).
fof(f_124_2,plain,
~ cC86(iV16459),
inference(definitional_conversion,[status(esa)],[f_124_1]) ).
cnf(f_124_3,plain,
~ cC86(iV16459),
inference(clausify,[status(thm)],[f_124_2]) ).
fof(f_125_1,plain,
~ cC46(iV16459),
inference(fof_nnf,[status(thm)],[axiom_124]) ).
fof(f_125_2,plain,
~ cC46(iV16459),
inference(definitional_conversion,[status(esa)],[f_125_1]) ).
cnf(f_125_3,plain,
~ cC46(iV16459),
inference(clausify,[status(thm)],[f_125_2]) ).
fof(f_128_1,plain,
~ cC66(iV16459),
inference(fof_nnf,[status(thm)],[axiom_127]) ).
fof(f_128_2,plain,
~ cC66(iV16459),
inference(definitional_conversion,[status(esa)],[f_128_1]) ).
cnf(f_128_3,plain,
~ cC66(iV16459),
inference(clausify,[status(thm)],[f_128_2]) ).
fof(f_133_1,plain,
~ cC84(iV16459),
inference(fof_nnf,[status(thm)],[axiom_132]) ).
fof(f_133_2,plain,
~ cC84(iV16459),
inference(definitional_conversion,[status(esa)],[f_133_1]) ).
cnf(f_133_3,plain,
~ cC84(iV16459),
inference(clausify,[status(thm)],[f_133_2]) ).
fof(f_134_1,plain,
~ cC64(iV16459),
inference(fof_nnf,[status(thm)],[axiom_133]) ).
fof(f_134_2,plain,
~ cC64(iV16459),
inference(definitional_conversion,[status(esa)],[f_134_1]) ).
cnf(f_134_3,plain,
~ cC64(iV16459),
inference(clausify,[status(thm)],[f_134_2]) ).
fof(f_135_1,plain,
cowlThing(iV16459),
inference(fof_nnf,[status(thm)],[axiom_134]) ).
fof(f_135_2,plain,
cowlThing(iV16459),
inference(definitional_conversion,[status(esa)],[f_135_1]) ).
cnf(f_135_3,plain,
cowlThing(iV16459),
inference(clausify,[status(thm)],[f_135_2]) ).
fof(f_136_1,plain,
~ cC32(iV16459),
inference(fof_nnf,[status(thm)],[axiom_135]) ).
fof(f_136_2,plain,
~ cC32(iV16459),
inference(definitional_conversion,[status(esa)],[f_136_1]) ).
cnf(f_136_3,plain,
~ cC32(iV16459),
inference(clausify,[status(thm)],[f_136_2]) ).
fof(f_142_1,plain,
~ cC8(iV16460),
inference(fof_nnf,[status(thm)],[axiom_141]) ).
fof(f_142_2,plain,
~ cC8(iV16460),
inference(definitional_conversion,[status(esa)],[f_142_1]) ).
cnf(f_142_3,plain,
~ cC8(iV16460),
inference(clausify,[status(thm)],[f_142_2]) ).
fof(f_147_1,plain,
cowlThing(iV16460),
inference(fof_nnf,[status(thm)],[axiom_146]) ).
fof(f_147_2,plain,
cowlThing(iV16460),
inference(definitional_conversion,[status(esa)],[f_147_1]) ).
cnf(f_147_3,plain,
cowlThing(iV16460),
inference(clausify,[status(thm)],[f_147_2]) ).
fof(f_152_1,plain,
~ cC12(iV16461),
inference(fof_nnf,[status(thm)],[axiom_151]) ).
fof(f_152_2,plain,
~ cC12(iV16461),
inference(definitional_conversion,[status(esa)],[f_152_1]) ).
cnf(f_152_3,plain,
~ cC12(iV16461),
inference(clausify,[status(thm)],[f_152_2]) ).
fof(f_155_1,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16461,X) ),
inference(fof_nnf,[status(thm)],[axiom_154]) ).
fof(f_155_2,plain,
! [U_261] :
( cC38(U_261)
| ~ rR1(iV16461,U_261) ),
inference(variable_rename,[status(thm)],[f_155_1]) ).
fof(f_155_3,plain,
! [U_261] :
( cC38(U_261)
| ~ rR1(iV16461,U_261) ),
inference(definitional_conversion,[status(esa)],[f_155_2]) ).
cnf(f_155_4,plain,
( cC38(U_261)
| ~ rR1(iV16461,U_261) ),
inference(clausify,[status(thm)],[f_155_3]) ).
fof(f_156_1,plain,
cowlThing(iV16461),
inference(fof_nnf,[status(thm)],[axiom_155]) ).
fof(f_156_2,plain,
cowlThing(iV16461),
inference(definitional_conversion,[status(esa)],[f_156_1]) ).
cnf(f_156_3,plain,
cowlThing(iV16461),
inference(clausify,[status(thm)],[f_156_2]) ).
fof(f_158_1,plain,
rR1(iV16461,iV16462),
inference(fof_nnf,[status(thm)],[axiom_157]) ).
fof(f_158_2,plain,
rR1(iV16461,iV16462),
inference(definitional_conversion,[status(esa)],[f_158_1]) ).
cnf(f_158_3,plain,
rR1(iV16461,iV16462),
inference(clausify,[status(thm)],[f_158_2]) ).
fof(f_169_1,plain,
cowlThing(iV16462),
inference(fof_nnf,[status(thm)],[axiom_168]) ).
fof(f_169_2,plain,
cowlThing(iV16462),
inference(definitional_conversion,[status(esa)],[f_169_1]) ).
cnf(f_169_3,plain,
cowlThing(iV16462),
inference(clausify,[status(thm)],[f_169_2]) ).
fof(f_172_1,plain,
! [X] :
( cC56(X)
| ~ rR1(iV16463,X) ),
inference(fof_nnf,[status(thm)],[axiom_171]) ).
fof(f_172_2,plain,
! [U_267] :
( cC56(U_267)
| ~ rR1(iV16463,U_267) ),
inference(variable_rename,[status(thm)],[f_172_1]) ).
fof(f_172_3,plain,
! [U_267] :
( cC56(U_267)
| ~ rR1(iV16463,U_267) ),
inference(definitional_conversion,[status(esa)],[f_172_2]) ).
cnf(f_172_4,plain,
( cC56(U_267)
| ~ rR1(iV16463,U_267) ),
inference(clausify,[status(thm)],[f_172_3]) ).
fof(f_177_1,plain,
cowlThing(iV16463),
inference(fof_nnf,[status(thm)],[axiom_176]) ).
fof(f_177_2,plain,
cowlThing(iV16463),
inference(definitional_conversion,[status(esa)],[f_177_1]) ).
cnf(f_177_3,plain,
cowlThing(iV16463),
inference(clausify,[status(thm)],[f_177_2]) ).
fof(f_178_1,plain,
rR1(iV16463,iV16464),
inference(fof_nnf,[status(thm)],[axiom_177]) ).
fof(f_178_2,plain,
rR1(iV16463,iV16464),
inference(definitional_conversion,[status(esa)],[f_178_1]) ).
cnf(f_178_3,plain,
rR1(iV16463,iV16464),
inference(clausify,[status(thm)],[f_178_2]) ).
fof(f_183_1,plain,
! [X] :
( cC38(X)
| ~ rR1(iV16464,X) ),
inference(fof_nnf,[status(thm)],[axiom_182]) ).
fof(f_183_2,plain,
! [U_270] :
( cC38(U_270)
| ~ rR1(iV16464,U_270) ),
inference(variable_rename,[status(thm)],[f_183_1]) ).
fof(f_183_3,plain,
! [U_270] :
( cC38(U_270)
| ~ rR1(iV16464,U_270) ),
inference(definitional_conversion,[status(esa)],[f_183_2]) ).
cnf(f_183_4,plain,
( cC38(U_270)
| ~ rR1(iV16464,U_270) ),
inference(clausify,[status(thm)],[f_183_3]) ).
fof(f_188_1,plain,
cowlThing(iV16464),
inference(fof_nnf,[status(thm)],[axiom_187]) ).
fof(f_188_2,plain,
cowlThing(iV16464),
inference(definitional_conversion,[status(esa)],[f_188_1]) ).
cnf(f_188_3,plain,
cowlThing(iV16464),
inference(clausify,[status(thm)],[f_188_2]) ).
fof(f_189_1,plain,
rR1(iV16464,iV16465),
inference(fof_nnf,[status(thm)],[axiom_188]) ).
fof(f_189_2,plain,
rR1(iV16464,iV16465),
inference(definitional_conversion,[status(esa)],[f_189_1]) ).
cnf(f_189_3,plain,
rR1(iV16464,iV16465),
inference(clausify,[status(thm)],[f_189_2]) ).
fof(f_199_1,plain,
cowlThing(iV16465),
inference(fof_nnf,[status(thm)],[axiom_198]) ).
fof(f_199_2,plain,
cowlThing(iV16465),
inference(definitional_conversion,[status(esa)],[f_199_1]) ).
cnf(f_199_3,plain,
cowlThing(iV16465),
inference(clausify,[status(thm)],[f_199_2]) ).
fof(f_201_1,negated_conjecture,
~ ( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_201_2,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(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_201_1]) ).
fof(f_201_3,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [U_278] :
( ( ~ xsd_string(U_278)
& ~ xsd_integer(U_278) )
| ( xsd_integer(U_278)
& xsd_string(U_278) ) )
| ? [U_277] :
( cowlNothing(U_277)
| ~ cowlThing(U_277) ) ),
inference(variable_rename,[status(thm)],[f_201_2]) ).
fof(f_201_4,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [U_282] :
( ~ xsd_string(U_282)
& ~ xsd_integer(U_282) )
| ? [U_281] :
( xsd_integer(U_281)
& xsd_string(U_281) )
| ? [U_280] : cowlNothing(U_280)
| ? [U_279] : ~ cowlThing(U_279) ),
inference(miniscope,[status(thm)],[f_201_3]) ).
fof(f_201_5,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [U_282] :
( ~ xsd_string(U_282)
& ~ xsd_integer(U_282) )
| ? [U_281] :
( xsd_integer(U_281)
& xsd_string(U_281) )
| ? [U_280] : cowlNothing(U_280)
| ~ cowlThing(sK29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_279,sK29)],[f_201_4]) ).
fof(f_201_6,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [U_282] :
( ~ xsd_string(U_282)
& ~ xsd_integer(U_282) )
| ? [U_281] :
( xsd_integer(U_281)
& xsd_string(U_281) )
| cowlNothing(sK30)
| ~ cowlThing(sK29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_280,sK30)],[f_201_5]) ).
fof(f_201_7,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [U_282] :
( ~ xsd_string(U_282)
& ~ xsd_integer(U_282) )
| ( xsd_integer(sK31)
& xsd_string(sK31) )
| cowlNothing(sK30)
| ~ cowlThing(sK29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_281,sK31)],[f_201_6]) ).
fof(f_201_8,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ( ~ xsd_string(sK32)
& ~ xsd_integer(sK32) )
| ( xsd_integer(sK31)
& xsd_string(sK31) )
| cowlNothing(sK30)
| ~ cowlThing(sK29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_282,sK32)],[f_201_7]) ).
fof(f_201_9,negated_conjecture,
( ( ~ xsd_string(sK32)
| ~ sP59 )
& ( ~ xsd_integer(sK32)
| ~ sP59 )
& ( xsd_integer(sK31)
| ~ sP58 )
& ( xsd_string(sK31)
| ~ sP58 )
& ( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| sP59
| sP58
| cowlNothing(sK30)
| ~ cowlThing(sK29) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP58,sP59])],[f_201_8]) ).
cnf(f_201_10,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| sP59
| sP58
| cowlNothing(sK30)
| ~ cowlThing(sK29) ),
inference(clausify,[status(thm)],[f_201_9]) ).
cnf(f_201_11,negated_conjecture,
( xsd_string(sK31)
| ~ sP58 ),
inference(clausify,[status(thm)],[f_201_9]) ).
cnf(f_201_12,negated_conjecture,
( xsd_integer(sK31)
| ~ sP58 ),
inference(clausify,[status(thm)],[f_201_9]) ).
cnf(f_201_13,negated_conjecture,
( ~ xsd_integer(sK32)
| ~ sP59 ),
inference(clausify,[status(thm)],[f_201_9]) ).
cnf(f_201_14,negated_conjecture,
( ~ xsd_string(sK32)
| ~ sP59 ),
inference(clausify,[status(thm)],[f_201_9]) ).
cnf(t1,plain,
( cowlNothing(sK30)
| sP58
| sP59
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC130(iV16439)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC80(iV16440)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC76(iV16453)
| ~ cC60(iV16453)
| ~ cC44(iV16455)
| ~ cowlThing(iV16455)
| ~ cC56(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC34(iV16459)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC76(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(sK29) ),
inference(start,[status(thm),parent(0:0)],[f_201_10]) ).
cnf(t2,plain,
cowlThing(sK29),
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,
( ~ rR1(iV16464,iV16465)
| cC38(iV16465) ),
inference(extension,[status(thm),parent(t1:2)],[f_183_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t1:2]) ).
cnf(t6,plain,
rR1(iV16464,iV16465),
inference(extension,[status(thm),parent(t4:2)],[f_189_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
cowlThing(iV16465),
inference(extension,[status(thm),parent(t1:3)],[f_199_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t1:3]) ).
cnf(t10,plain,
( ~ sP28(iV16464)
| cC42(iV16464) ),
inference(extension,[status(thm),parent(t1:4)],[f_31_8]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t1:4]) ).
cnf(t12,plain,
( ~ cC44(iV16464)
| sP28(iV16464) ),
inference(extension,[status(thm),parent(t10:2)],[f_31_5]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
( ~ sP34(iV16464)
| cC44(iV16464) ),
inference(extension,[status(thm),parent(t12:2)],[f_37_7]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
( ~ cC56(iV16464)
| sP34(iV16464) ),
inference(extension,[status(thm),parent(t14:2)],[f_37_5]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
( ~ rR1(iV16463,iV16464)
| cC56(iV16464) ),
inference(extension,[status(thm),parent(t16:2)],[f_172_4]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
cnf(t20,plain,
rR1(iV16463,iV16464),
inference(extension,[status(thm),parent(t18:2)],[f_178_3]) ).
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(t1:5)],[f_172_4]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t1:5]) ).
cnf(t24,plain,
rR1(iV16463,iV16464),
inference(extension,[status(thm),parent(t22:2)],[f_178_3]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(l11,lemma,
cC56(iV16464),
inference(lemma,[status(cth),parent(t1:5),below(0:0)],[t1:5]) ).
cnf(t26,plain,
cowlThing(iV16464),
inference(extension,[status(thm),parent(t1:6)],[f_188_3]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t1:6]) ).
cnf(t28,plain,
( ~ sP34(iV16464)
| cC44(iV16464) ),
inference(extension,[status(thm),parent(t1:7)],[f_37_7]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t1:7]) ).
cnf(t30,plain,
( ~ cC56(iV16464)
| sP34(iV16464) ),
inference(extension,[status(thm),parent(t28:2)],[f_37_5]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
cC56(iV16464),
inference(lemma_extension,[status(thm),parent(t30:2)],[l11:1]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
( ~ sP38(iV16463)
| cC60(iV16463) ),
inference(extension,[status(thm),parent(t1:8)],[f_41_7]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t1:8]) ).
cnf(t36,plain,
( ~ cC62(iV16463)
| sP38(iV16463) ),
inference(extension,[status(thm),parent(t34:2)],[f_41_5]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
( ~ sP45(iV16463)
| cC62(iV16463) ),
inference(extension,[status(thm),parent(t36:2)],[f_48_8]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
cnf(t40,plain,
( ~ cC76(iV16463)
| sP45(iV16463) ),
inference(extension,[status(thm),parent(t38:2)],[f_48_5]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t38:2]) ).
cnf(t42,plain,
( ~ rR1(iV16440,iV16463)
| cC76(iV16463) ),
inference(extension,[status(thm),parent(t40:2)],[f_68_4]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
cnf(t44,plain,
rR1(iV16440,iV16463),
inference(extension,[status(thm),parent(t42:2)],[f_74_3]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t42:2]) ).
cnf(t46,plain,
( ~ rR1(iV16440,iV16463)
| cC76(iV16463) ),
inference(extension,[status(thm),parent(t1:9)],[f_68_4]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t1:9]) ).
cnf(t48,plain,
rR1(iV16440,iV16463),
inference(extension,[status(thm),parent(t46:2)],[f_74_3]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(l22,lemma,
cC76(iV16463),
inference(lemma,[status(cth),parent(t1:9),below(0:0)],[t1:9]) ).
cnf(t50,plain,
cowlThing(iV16463),
inference(extension,[status(thm),parent(t1:10)],[f_177_3]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t1:10]) ).
cnf(t52,plain,
( ~ sP45(iV16463)
| cC62(iV16463) ),
inference(extension,[status(thm),parent(t1:11)],[f_48_8]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t1:11]) ).
cnf(t54,plain,
( ~ cC76(iV16463)
| sP45(iV16463) ),
inference(extension,[status(thm),parent(t52:2)],[f_48_5]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t52:2]) ).
cnf(t56,plain,
cC76(iV16463),
inference(lemma_extension,[status(thm),parent(t54:2)],[l22:1]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(t58,plain,
( ~ rR1(iV16461,iV16462)
| cC38(iV16462) ),
inference(extension,[status(thm),parent(t1:12)],[f_155_4]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t1:12]) ).
cnf(t60,plain,
rR1(iV16461,iV16462),
inference(extension,[status(thm),parent(t58:2)],[f_158_3]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
cowlThing(iV16462),
inference(extension,[status(thm),parent(t1:13)],[f_169_3]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t1:13]) ).
cnf(t64,plain,
( ~ sP28(iV16461)
| cC42(iV16461) ),
inference(extension,[status(thm),parent(t1:14)],[f_31_8]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t1:14]) ).
cnf(t66,plain,
( ~ cC44(iV16461)
| sP28(iV16461) ),
inference(extension,[status(thm),parent(t64:2)],[f_31_5]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t64:2]) ).
cnf(t68,plain,
( ~ sP34(iV16461)
| cC44(iV16461) ),
inference(extension,[status(thm),parent(t66:2)],[f_37_7]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t66:2]) ).
cnf(t70,plain,
( ~ cC56(iV16461)
| sP34(iV16461) ),
inference(extension,[status(thm),parent(t68:2)],[f_37_5]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t68:2]) ).
cnf(t72,plain,
( ~ rR1(iV16453,iV16461)
| cC56(iV16461) ),
inference(extension,[status(thm),parent(t70:2)],[f_94_4]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t70:2]) ).
cnf(t74,plain,
rR1(iV16453,iV16461),
inference(extension,[status(thm),parent(t72:2)],[f_97_3]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t72:2]) ).
cnf(t76,plain,
( ~ rR1(iV16453,iV16461)
| cC56(iV16461) ),
inference(extension,[status(thm),parent(t1:15)],[f_94_4]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t1:15]) ).
cnf(t78,plain,
rR1(iV16453,iV16461),
inference(extension,[status(thm),parent(t76:2)],[f_97_3]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t76:2]) ).
cnf(l36,lemma,
cC56(iV16461),
inference(lemma,[status(cth),parent(t1:15),below(0:0)],[t1:15]) ).
cnf(t80,plain,
cowlThing(iV16461),
inference(extension,[status(thm),parent(t1:16)],[f_156_3]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t1:16]) ).
cnf(t82,plain,
( ~ sP34(iV16461)
| cC44(iV16461) ),
inference(extension,[status(thm),parent(t1:17)],[f_37_7]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t1:17]) ).
cnf(t84,plain,
( ~ cC56(iV16461)
| sP34(iV16461) ),
inference(extension,[status(thm),parent(t82:2)],[f_37_5]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t82:2]) ).
cnf(t86,plain,
cC56(iV16461),
inference(lemma_extension,[status(thm),parent(t84:2)],[l36:1]) ).
cnf(t87,plain,
$false,
inference(connection,[status(thm),parent(t86:1)],[t86:1,t84:2]) ).
cnf(t88,plain,
( ~ rR1(iV16455,iV16460)
| cC38(iV16460) ),
inference(extension,[status(thm),parent(t1:18)],[f_107_4]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t1:18]) ).
cnf(t90,plain,
rR1(iV16455,iV16460),
inference(extension,[status(thm),parent(t88:2)],[f_108_3]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t88:2]) ).
cnf(t92,plain,
cowlThing(iV16460),
inference(extension,[status(thm),parent(t1:19)],[f_147_3]) ).
cnf(t93,plain,
$false,
inference(connection,[status(thm),parent(t92:1)],[t92:1,t1:19]) ).
cnf(t94,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC34(iV16459) ),
inference(extension,[status(thm),parent(t1:20)],[f_26_6]) ).
cnf(t95,plain,
$false,
inference(connection,[status(thm),parent(t94:1)],[t94:1,t1:20]) ).
cnf(t96,plain,
~ cC32(iV16459),
inference(extension,[status(thm),parent(t94:2)],[f_136_3]) ).
cnf(t97,plain,
$false,
inference(connection,[status(thm),parent(t96:1)],[t96:1,t94:2]) ).
cnf(t98,plain,
~ cC30(iV16459),
inference(extension,[status(thm),parent(t94:3)],[f_122_3]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t94:3]) ).
cnf(t100,plain,
( cC48(iV16459)
| cC46(iV16459)
| cC50(iV16459) ),
inference(extension,[status(thm),parent(t1:21)],[f_34_6]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t1:21]) ).
cnf(t102,plain,
~ cC46(iV16459),
inference(extension,[status(thm),parent(t100:2)],[f_125_3]) ).
cnf(t103,plain,
$false,
inference(connection,[status(thm),parent(t102:1)],[t102:1,t100:2]) ).
cnf(t104,plain,
~ cC48(iV16459),
inference(extension,[status(thm),parent(t100:3)],[f_121_3]) ).
cnf(t105,plain,
$false,
inference(connection,[status(thm),parent(t104:1)],[t104:1,t100:3]) ).
cnf(t106,plain,
( cC86(iV16459)
| cC84(iV16459)
| cC88(iV16459) ),
inference(extension,[status(thm),parent(t1:22)],[f_54_6]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t1:22]) ).
cnf(t108,plain,
~ cC84(iV16459),
inference(extension,[status(thm),parent(t106:2)],[f_133_3]) ).
cnf(t109,plain,
$false,
inference(connection,[status(thm),parent(t108:1)],[t108:1,t106:2]) ).
cnf(t110,plain,
~ cC86(iV16459),
inference(extension,[status(thm),parent(t106:3)],[f_124_3]) ).
cnf(t111,plain,
$false,
inference(connection,[status(thm),parent(t110:1)],[t110:1,t106:3]) ).
cnf(t112,plain,
cowlThing(iV16459),
inference(extension,[status(thm),parent(t1:23)],[f_135_3]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t1:23]) ).
cnf(t114,plain,
( cC66(iV16459)
| cC64(iV16459)
| cC68(iV16459) ),
inference(extension,[status(thm),parent(t1:24)],[f_44_6]) ).
cnf(t115,plain,
$false,
inference(connection,[status(thm),parent(t114:1)],[t114:1,t1:24]) ).
cnf(t116,plain,
~ cC64(iV16459),
inference(extension,[status(thm),parent(t114:2)],[f_134_3]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t114:2]) ).
cnf(t118,plain,
~ cC66(iV16459),
inference(extension,[status(thm),parent(t114:3)],[f_128_3]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t114:3]) ).
cnf(t120,plain,
( ~ cTOP(iV16457)
| cC36(iV16457)
| cC38(iV16457) ),
inference(extension,[status(thm),parent(t1:25)],[f_28_6]) ).
cnf(t121,plain,
$false,
inference(connection,[status(thm),parent(t120:1)],[t120:1,t1:25]) ).
cnf(t122,plain,
~ cC36(iV16457),
inference(extension,[status(thm),parent(t120:2)],[f_109_3]) ).
cnf(t123,plain,
$false,
inference(connection,[status(thm),parent(t122:1)],[t122:1,t120:2]) ).
cnf(t124,plain,
cTOP(iV16457),
inference(extension,[status(thm),parent(t120:3)],[f_114_3]) ).
cnf(t125,plain,
$false,
inference(connection,[status(thm),parent(t124:1)],[t124:1,t120:3]) ).
cnf(t126,plain,
cowlThing(iV16457),
inference(extension,[status(thm),parent(t1:26)],[f_118_3]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t1:26]) ).
cnf(t128,plain,
( cC8(iV16460)
| ~ rR1(iV16455,iV16460)
| cC42(iV16455) ),
inference(extension,[status(thm),parent(t1:27)],[f_30_7]) ).
cnf(t129,plain,
$false,
inference(connection,[status(thm),parent(t128:1)],[t128:1,t1:27]) ).
cnf(t130,plain,
rR1(iV16455,iV16460),
inference(extension,[status(thm),parent(t128:2)],[f_108_3]) ).
cnf(t131,plain,
$false,
inference(connection,[status(thm),parent(t130:1)],[t130:1,t128:2]) ).
cnf(t132,plain,
~ cC8(iV16460),
inference(extension,[status(thm),parent(t128:3)],[f_142_3]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t128:3]) ).
cnf(l61,lemma,
cC42(iV16455),
inference(lemma,[status(cth),parent(t1:27),below(0:0)],[t1:27]) ).
cnf(t134,plain,
( cC54(iV16455)
| ~ cC44(iV16455)
| cC56(iV16455) ),
inference(extension,[status(thm),parent(t1:28)],[f_37_6]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t1:28]) ).
cnf(t136,plain,
( ~ cC42(iV16455)
| cC40(iV16455)
| cC44(iV16455) ),
inference(extension,[status(thm),parent(t134:2)],[f_31_6]) ).
cnf(t137,plain,
$false,
inference(connection,[status(thm),parent(t136:1)],[t136:1,t134:2]) ).
cnf(t138,plain,
~ cC40(iV16455),
inference(extension,[status(thm),parent(t136:2)],[f_99_3]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t136:2]) ).
cnf(t140,plain,
cC42(iV16455),
inference(lemma_extension,[status(thm),parent(t136:3)],[l61:1]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t136:3]) ).
cnf(t142,plain,
~ cC54(iV16455),
inference(extension,[status(thm),parent(t134:3)],[f_104_3]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t134:3]) ).
cnf(l64,lemma,
cC56(iV16455),
inference(lemma,[status(cth),parent(t1:28),below(0:0)],[t1:28]) ).
cnf(t144,plain,
cowlThing(iV16455),
inference(extension,[status(thm),parent(t1:29)],[f_106_3]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t1:29]) ).
cnf(t146,plain,
( ~ sP34(iV16455)
| cC44(iV16455) ),
inference(extension,[status(thm),parent(t1:30)],[f_37_7]) ).
cnf(t147,plain,
$false,
inference(connection,[status(thm),parent(t146:1)],[t146:1,t1:30]) ).
cnf(t148,plain,
( ~ cC56(iV16455)
| sP34(iV16455) ),
inference(extension,[status(thm),parent(t146:2)],[f_37_5]) ).
cnf(t149,plain,
$false,
inference(connection,[status(thm),parent(t148:1)],[t148:1,t146:2]) ).
cnf(t150,plain,
cC56(iV16455),
inference(lemma_extension,[status(thm),parent(t148:2)],[l64:1]) ).
cnf(t151,plain,
$false,
inference(connection,[status(thm),parent(t150:1)],[t150:1,t148:2]) ).
cnf(t152,plain,
( cC12(iV16461)
| ~ rR1(iV16453,iV16461)
| cC60(iV16453) ),
inference(extension,[status(thm),parent(t1:31)],[f_40_7]) ).
cnf(t153,plain,
$false,
inference(connection,[status(thm),parent(t152:1)],[t152:1,t1:31]) ).
cnf(t154,plain,
rR1(iV16453,iV16461),
inference(extension,[status(thm),parent(t152:2)],[f_97_3]) ).
cnf(t155,plain,
$false,
inference(connection,[status(thm),parent(t154:1)],[t154:1,t152:2]) ).
cnf(t156,plain,
~ cC12(iV16461),
inference(extension,[status(thm),parent(t152:3)],[f_152_3]) ).
cnf(t157,plain,
$false,
inference(connection,[status(thm),parent(t156:1)],[t156:1,t152:3]) ).
cnf(l71,lemma,
cC60(iV16453),
inference(lemma,[status(cth),parent(t1:31),below(0:0)],[t1:31]) ).
cnf(t158,plain,
( ~ cC62(iV16453)
| cC74(iV16453)
| cC76(iV16453) ),
inference(extension,[status(thm),parent(t1:32)],[f_48_6]) ).
cnf(t159,plain,
$false,
inference(connection,[status(thm),parent(t158:1)],[t158:1,t1:32]) ).
cnf(t160,plain,
~ cC74(iV16453),
inference(extension,[status(thm),parent(t158:2)],[f_93_3]) ).
cnf(t161,plain,
$false,
inference(connection,[status(thm),parent(t160:1)],[t160:1,t158:2]) ).
cnf(t162,plain,
( cC58(iV16453)
| ~ cC60(iV16453)
| cC62(iV16453) ),
inference(extension,[status(thm),parent(t158:3)],[f_41_6]) ).
cnf(t163,plain,
$false,
inference(connection,[status(thm),parent(t162:1)],[t162:1,t158:3]) ).
cnf(t164,plain,
cC60(iV16453),
inference(lemma_extension,[status(thm),parent(t162:2)],[l71:1]) ).
cnf(t165,plain,
$false,
inference(connection,[status(thm),parent(t164:1)],[t164:1,t162:2]) ).
cnf(t166,plain,
~ cC58(iV16453),
inference(extension,[status(thm),parent(t162:3)],[f_92_3]) ).
cnf(t167,plain,
$false,
inference(connection,[status(thm),parent(t166:1)],[t166:1,t162:3]) ).
cnf(l74,lemma,
cC76(iV16453),
inference(lemma,[status(cth),parent(t1:32),below(0:0)],[t1:32]) ).
cnf(t168,plain,
cowlThing(iV16453),
inference(extension,[status(thm),parent(t1:33)],[f_95_3]) ).
cnf(t169,plain,
$false,
inference(connection,[status(thm),parent(t168:1)],[t168:1,t1:33]) ).
cnf(t170,plain,
( ~ sP45(iV16453)
| cC62(iV16453) ),
inference(extension,[status(thm),parent(t1:34)],[f_48_8]) ).
cnf(t171,plain,
$false,
inference(connection,[status(thm),parent(t170:1)],[t170:1,t1:34]) ).
cnf(t172,plain,
( ~ cC76(iV16453)
| sP45(iV16453) ),
inference(extension,[status(thm),parent(t170:2)],[f_48_5]) ).
cnf(t173,plain,
$false,
inference(connection,[status(thm),parent(t172:1)],[t172:1,t170:2]) ).
cnf(t174,plain,
cC76(iV16453),
inference(lemma_extension,[status(thm),parent(t172:2)],[l74:1]) ).
cnf(t175,plain,
$false,
inference(connection,[status(thm),parent(t174:1)],[t174:1,t172:2]) ).
cnf(t176,plain,
( ~ cTOP(iV16448)
| cC36(iV16448)
| cC38(iV16448) ),
inference(extension,[status(thm),parent(t1:35)],[f_28_6]) ).
cnf(t177,plain,
$false,
inference(connection,[status(thm),parent(t176:1)],[t176:1,t1:35]) ).
cnf(t178,plain,
~ cC36(iV16448),
inference(extension,[status(thm),parent(t176:2)],[f_77_3]) ).
cnf(t179,plain,
$false,
inference(connection,[status(thm),parent(t178:1)],[t178:1,t176:2]) ).
cnf(t180,plain,
cTOP(iV16448),
inference(extension,[status(thm),parent(t176:3)],[f_80_3]) ).
cnf(t181,plain,
$false,
inference(connection,[status(thm),parent(t180:1)],[t180:1,t176:3]) ).
cnf(t182,plain,
cowlThing(iV16448),
inference(extension,[status(thm),parent(t1:36)],[f_85_3]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t1:36]) ).
cnf(t184,plain,
( ~ rR1(iV16439,iV16440)
| cC98(iV16440) ),
inference(extension,[status(thm),parent(t1:37)],[f_61_4]) ).
cnf(t185,plain,
$false,
inference(connection,[status(thm),parent(t184:1)],[t184:1,t1:37]) ).
cnf(t186,plain,
rR1(iV16439,iV16440),
inference(extension,[status(thm),parent(t184:2)],[f_65_3]) ).
cnf(t187,plain,
$false,
inference(connection,[status(thm),parent(t186:1)],[t186:1,t184:2]) ).
cnf(l85,lemma,
cC98(iV16440),
inference(lemma,[status(cth),parent(t1:37),below(0:0)],[t1:37]) ).
cnf(t188,plain,
( ~ sP56(iV16440)
| cC82(iV16440) ),
inference(extension,[status(thm),parent(t1:38)],[f_59_8]) ).
cnf(t189,plain,
$false,
inference(connection,[status(thm),parent(t188:1)],[t188:1,t1:38]) ).
cnf(t190,plain,
( ~ cC98(iV16440)
| sP56(iV16440) ),
inference(extension,[status(thm),parent(t188:2)],[f_59_5]) ).
cnf(t191,plain,
$false,
inference(connection,[status(thm),parent(t190:1)],[t190:1,t188:2]) ).
cnf(t192,plain,
cC98(iV16440),
inference(lemma_extension,[status(thm),parent(t190:2)],[l85:1]) ).
cnf(t193,plain,
$false,
inference(connection,[status(thm),parent(t192:1)],[t192:1,t190:2]) ).
cnf(l87,lemma,
cC82(iV16440),
inference(lemma,[status(cth),parent(t1:38),below(0:0)],[t1:38]) ).
cnf(t194,plain,
cowlThing(iV16440),
inference(extension,[status(thm),parent(t1:39)],[f_73_3]) ).
cnf(t195,plain,
$false,
inference(connection,[status(thm),parent(t194:1)],[t194:1,t1:39]) ).
cnf(t196,plain,
( ~ sP48(iV16440)
| cC80(iV16440) ),
inference(extension,[status(thm),parent(t1:40)],[f_51_8]) ).
cnf(t197,plain,
$false,
inference(connection,[status(thm),parent(t196:1)],[t196:1,t1:40]) ).
cnf(t198,plain,
( ~ cC82(iV16440)
| sP48(iV16440) ),
inference(extension,[status(thm),parent(t196:2)],[f_51_5]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t196:2]) ).
cnf(t200,plain,
cC82(iV16440),
inference(lemma_extension,[status(thm),parent(t198:2)],[l87:1]) ).
cnf(t201,plain,
$false,
inference(connection,[status(thm),parent(t200:1)],[t200:1,t198:2]) ).
cnf(t202,plain,
( ~ sP3(iV16439)
| cC104(iV16439) ),
inference(extension,[status(thm),parent(t1:41)],[f_6_8]) ).
cnf(t203,plain,
$false,
inference(connection,[status(thm),parent(t202:1)],[t202:1,t1:41]) ).
cnf(t204,plain,
( ~ cC106(iV16439)
| sP3(iV16439) ),
inference(extension,[status(thm),parent(t202:2)],[f_6_5]) ).
cnf(t205,plain,
$false,
inference(connection,[status(thm),parent(t204:1)],[t204:1,t202:2]) ).
cnf(t206,plain,
( ~ sP4(iV16439)
| cC106(iV16439) ),
inference(extension,[status(thm),parent(t204:2)],[f_7_8]) ).
cnf(t207,plain,
$false,
inference(connection,[status(thm),parent(t206:1)],[t206:1,t204:2]) ).
cnf(t208,plain,
( ~ cC108(iV16439)
| sP4(iV16439) ),
inference(extension,[status(thm),parent(t206:2)],[f_7_5]) ).
cnf(t209,plain,
$false,
inference(connection,[status(thm),parent(t208:1)],[t208:1,t206:2]) ).
cnf(t210,plain,
( ~ sP57(iV16439)
| cC108(iV16439) ),
inference(extension,[status(thm),parent(t208:2)],[f_60_7]) ).
cnf(t211,plain,
$false,
inference(connection,[status(thm),parent(t210:1)],[t210:1,t208:2]) ).
cnf(t212,plain,
( ~ cTEST(iV16439)
| sP57(iV16439) ),
inference(extension,[status(thm),parent(t210:2)],[f_60_5]) ).
cnf(t213,plain,
$false,
inference(connection,[status(thm),parent(t212:1)],[t212:1,t210:2]) ).
cnf(t214,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t212:2)],[f_62_3]) ).
cnf(t215,plain,
$false,
inference(connection,[status(thm),parent(t214:1)],[t214:1,t212:2]) ).
cnf(t216,plain,
( ~ sP57(iV16439)
| cC108(iV16439) ),
inference(extension,[status(thm),parent(t1:42)],[f_60_7]) ).
cnf(t217,plain,
$false,
inference(connection,[status(thm),parent(t216:1)],[t216:1,t1:42]) ).
cnf(t218,plain,
( ~ cTEST(iV16439)
| sP57(iV16439) ),
inference(extension,[status(thm),parent(t216:2)],[f_60_5]) ).
cnf(t219,plain,
$false,
inference(connection,[status(thm),parent(t218:1)],[t218:1,t216:2]) ).
cnf(t220,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t218:2)],[f_62_3]) ).
cnf(t221,plain,
$false,
inference(connection,[status(thm),parent(t220:1)],[t220:1,t218:2]) ).
cnf(l99,lemma,
cC108(iV16439),
inference(lemma,[status(cth),parent(t1:42),below(0:0)],[t1:42]) ).
cnf(t222,plain,
cowlThing(iV16439),
inference(extension,[status(thm),parent(t1:43)],[f_64_3]) ).
cnf(t223,plain,
$false,
inference(connection,[status(thm),parent(t222:1)],[t222:1,t1:43]) ).
cnf(t224,plain,
( ~ sP57(iV16439)
| cC130(iV16439) ),
inference(extension,[status(thm),parent(t1:44)],[f_60_8]) ).
cnf(t225,plain,
$false,
inference(connection,[status(thm),parent(t224:1)],[t224:1,t1:44]) ).
cnf(t226,plain,
( ~ cTEST(iV16439)
| sP57(iV16439) ),
inference(extension,[status(thm),parent(t224:2)],[f_60_5]) ).
cnf(t227,plain,
$false,
inference(connection,[status(thm),parent(t226:1)],[t226:1,t224:2]) ).
cnf(t228,plain,
cTEST(iV16439),
inference(extension,[status(thm),parent(t226:2)],[f_62_3]) ).
cnf(t229,plain,
$false,
inference(connection,[status(thm),parent(t228:1)],[t228:1,t226:2]) ).
cnf(t230,plain,
( ~ sP4(iV16439)
| cC28(iV16439) ),
inference(extension,[status(thm),parent(t1:45)],[f_7_7]) ).
cnf(t231,plain,
$false,
inference(connection,[status(thm),parent(t230:1)],[t230:1,t1:45]) ).
cnf(t232,plain,
( ~ cC108(iV16439)
| sP4(iV16439) ),
inference(extension,[status(thm),parent(t230:2)],[f_7_5]) ).
cnf(t233,plain,
$false,
inference(connection,[status(thm),parent(t232:1)],[t232:1,t230:2]) ).
cnf(t234,plain,
cC108(iV16439),
inference(lemma_extension,[status(thm),parent(t232:2)],[l99:1]) ).
cnf(t235,plain,
$false,
inference(connection,[status(thm),parent(t234:1)],[t234:1,t232:2]) ).
cnf(t236,plain,
( ~ sP4(iV16439)
| cC106(iV16439) ),
inference(extension,[status(thm),parent(t1:46)],[f_7_8]) ).
cnf(t237,plain,
$false,
inference(connection,[status(thm),parent(t236:1)],[t236:1,t1:46]) ).
cnf(t238,plain,
( ~ cC108(iV16439)
| sP4(iV16439) ),
inference(extension,[status(thm),parent(t236:2)],[f_7_5]) ).
cnf(t239,plain,
$false,
inference(connection,[status(thm),parent(t238:1)],[t238:1,t236:2]) ).
cnf(t240,plain,
cC108(iV16439),
inference(lemma_extension,[status(thm),parent(t238:2)],[l99:1]) ).
cnf(t241,plain,
$false,
inference(connection,[status(thm),parent(t240:1)],[t240:1,t238:2]) ).
cnf(t242,plain,
( ~ xsd_string(sK32)
| ~ sP59 ),
inference(extension,[status(thm),parent(t1:47)],[f_201_14]) ).
cnf(t243,plain,
$false,
inference(connection,[status(thm),parent(t242:1)],[t242:1,t1:47]) ).
cnf(t244,plain,
( xsd_integer(sK32)
| xsd_string(sK32) ),
inference(extension,[status(thm),parent(t242:2)],[f_2_6]) ).
cnf(t245,plain,
$false,
inference(connection,[status(thm),parent(t244:1)],[t244:1,t242:2]) ).
cnf(t246,plain,
( ~ sP59
| ~ xsd_integer(sK32) ),
inference(extension,[status(thm),parent(t244:2)],[f_201_13]) ).
cnf(t247,plain,
$false,
inference(connection,[status(thm),parent(t246:1)],[t246:1,t244:2]) ).
cnf(t248,plain,
$false,
inference(reduction,[status(thm),parent(t246:2)],[t246:2,t1:47]) ).
cnf(t249,plain,
( xsd_integer(sK31)
| ~ sP58 ),
inference(extension,[status(thm),parent(t1:48)],[f_201_12]) ).
cnf(t250,plain,
$false,
inference(connection,[status(thm),parent(t249:1)],[t249:1,t1:48]) ).
cnf(t251,plain,
( ~ xsd_string(sK31)
| ~ xsd_integer(sK31) ),
inference(extension,[status(thm),parent(t249:2)],[f_2_5]) ).
cnf(t252,plain,
$false,
inference(connection,[status(thm),parent(t251:1)],[t251:1,t249:2]) ).
cnf(t253,plain,
( ~ sP58
| xsd_string(sK31) ),
inference(extension,[status(thm),parent(t251:2)],[f_201_11]) ).
cnf(t254,plain,
$false,
inference(connection,[status(thm),parent(t253:1)],[t253:1,t251:2]) ).
cnf(t255,plain,
$false,
inference(reduction,[status(thm),parent(t253:2)],[t253:2,t1:48]) ).
cnf(t256,plain,
~ cowlNothing(sK30),
inference(extension,[status(thm),parent(t1:49)],[f_1_6]) ).
cnf(t257,plain,
$false,
inference(connection,[status(thm),parent(t256:1)],[t256:1,t1:49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.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.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 19 12:11:39 UTC 2026
% 0.13/0.36 % CPUTime :
% 33.05/33.38 % SZS status Theorem for theBenchmark
% 33.05/33.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------