%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS148+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 0.54s 0.84s
% Output : Proof 0.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('theBenchmark.p',axiom_1) ).
fof(axiom_2,axiom,
! [X] :
( cC10(X)
<=> ( ~ cC2(X)
& ~ cC8(X) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X] :
( cC100(X)
<=> ( cC94(X)
& ~ cC98(X) ) ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X] :
( cC102(X)
<=> ? [Y] :
( cC100(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_5,axiom,
! [X] :
( cC104(X)
<=> ( cC88(X)
& ~ cC102(X) ) ),
file('theBenchmark.p',axiom_5) ).
fof(axiom_6,axiom,
! [X] :
( cC106(X)
<=> ? [Y] :
( cC104(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_7,axiom,
! [X] :
( cC108(X)
<=> ( ~ cC106(X)
& cC84(X) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_8,axiom,
! [X] :
( cC110(X)
<=> ( ~ cC108(X)
& cC62(X) ) ),
file('theBenchmark.p',axiom_8) ).
fof(axiom_9,axiom,
! [X] :
( cC112(X)
<=> ? [Y] :
( ~ cC110(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_9) ).
fof(axiom_10,axiom,
! [X] :
( cC114(X)
<=> ? [Y] :
( cC112(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_10) ).
fof(axiom_11,axiom,
! [X] :
( cC116(X)
<=> ( ~ cC114(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_11) ).
fof(axiom_12,axiom,
! [X] :
( cC118(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_12) ).
fof(axiom_13,axiom,
! [X] :
( cC12(X)
<=> ? [Y] :
( cC10(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_13) ).
fof(axiom_14,axiom,
! [X] :
( cC120(X)
<=> ? [Y] :
( ~ cC118(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_14) ).
fof(axiom_15,axiom,
! [X] :
( cC122(X)
<=> ( cC120(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X] :
( cC124(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_17,axiom,
! [X] :
( cC126(X)
<=> ( cC2(X)
& cC124(X) ) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_18,axiom,
! [X] :
( cC128(X)
<=> ? [Y] :
( cC126(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_19,axiom,
! [X] :
( cC130(X)
<=> ( ~ cC128(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_19) ).
fof(axiom_20,axiom,
! [X] :
( cC132(X)
<=> ? [Y] :
( cC130(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_20) ).
fof(axiom_21,axiom,
! [X] :
( cC134(X)
<=> ( ~ cC132(X)
& cC122(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cC136(X)
<=> ? [Y] :
( cC134(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_23,axiom,
! [X] :
( cC138(X)
<=> ? [Y] :
( cC136(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_23) ).
fof(axiom_24,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_24) ).
fof(axiom_25,axiom,
! [X] :
( cC140(X)
<=> ( cC138(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_26,axiom,
! [X] :
( cC16(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_26) ).
fof(axiom_27,axiom,
! [X] :
( cC18(X)
<=> ( cC2(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_28,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( cC18(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_28) ).
fof(axiom_29,axiom,
! [X] :
( cC22(X)
<=> ( ~ cC2(X)
& ~ cC20(X) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC24(X)
<=> ? [Y] :
( cC22(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_31,axiom,
! [X] :
( cC26(X)
<=> ( ~ cC24(X)
& cC14(X) ) ),
file('theBenchmark.p',axiom_31) ).
fof(axiom_32,axiom,
! [X] :
( cC28(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_33,axiom,
! [X] :
( cC30(X)
<=> ? [Y] :
( cC28(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_34,axiom,
! [X] :
( cC32(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_34) ).
fof(axiom_35,axiom,
! [X] :
( cC34(X)
<=> ( ~ cC32(X)
& cC30(X) ) ),
file('theBenchmark.p',axiom_35) ).
fof(axiom_36,axiom,
! [X] :
( cC36(X)
<=> ? [Y] :
( cC34(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_36) ).
fof(axiom_37,axiom,
! [X] :
( cC38(X)
<=> ( ~ cC26(X)
& ~ cC36(X) ) ),
file('theBenchmark.p',axiom_37) ).
fof(axiom_38,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_38) ).
fof(axiom_39,axiom,
! [X] :
( cC40(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC42(X)
<=> ( cC40(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC44(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_42,axiom,
! [X] :
( cC46(X)
<=> ? [Y] :
( ~ cC44(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_43,axiom,
! [X] :
( cC48(X)
<=> ( cC46(X)
& cC42(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_44,axiom,
! [X] :
( cC50(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_45,axiom,
! [X] :
( cC52(X)
<=> ( cC50(X)
& cC2(X) ) ),
file('theBenchmark.p',axiom_45) ).
fof(axiom_46,axiom,
! [X] :
( cC54(X)
<=> ? [Y] :
( cC52(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_46) ).
fof(axiom_47,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC2(X)
& ~ cC54(X) ) ),
file('theBenchmark.p',axiom_47) ).
fof(axiom_48,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( cC56(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_48) ).
fof(axiom_49,axiom,
! [X] :
( cC6(X)
<=> ( cC4(X)
& cC2(X) ) ),
file('theBenchmark.p',axiom_49) ).
fof(axiom_50,axiom,
! [X] :
( cC60(X)
<=> ( ~ cC58(X)
& cC48(X) ) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_51,axiom,
! [X] :
( cC62(X)
<=> ( ~ cC60(X)
& cC38(X) ) ),
file('theBenchmark.p',axiom_51) ).
fof(axiom_52,axiom,
! [X] :
( cC64(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_53,axiom,
! [X] :
( cC66(X)
<=> ( cC2(X)
& cC64(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_54,axiom,
! [X] :
( cC68(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_54) ).
fof(axiom_55,axiom,
! [X] :
( cC70(X)
<=> ( cC68(X)
& cC2(X) ) ),
file('theBenchmark.p',axiom_55) ).
fof(axiom_56,axiom,
! [X] :
( cC72(X)
<=> ? [Y] :
( cC70(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_56) ).
fof(axiom_57,axiom,
! [X] :
( cC74(X)
<=> ( cC72(X)
& cC66(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_58,axiom,
! [X] :
( cC76(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_58) ).
fof(axiom_59,axiom,
! [X] :
( cC78(X)
<=> ( cC2(X)
& cC76(X) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_60,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_60) ).
fof(axiom_61,axiom,
! [X] :
( cC80(X)
<=> ? [Y] :
( cC78(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_61) ).
fof(axiom_62,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( ~ cC80(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_62) ).
fof(axiom_63,axiom,
! [X] :
( cC84(X)
<=> ( cC74(X)
& cC82(X) ) ),
file('theBenchmark.p',axiom_63) ).
fof(axiom_64,axiom,
! [X] :
( cC86(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC88(X)
<=> ( cC2(X)
& cC86(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC90(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cC92(X)
<=> ( cC90(X)
& cC2(X) ) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_68,axiom,
! [X] :
( cC94(X)
<=> ? [Y] :
( cC92(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_68) ).
fof(axiom_69,axiom,
! [X] :
( cC96(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_69) ).
fof(axiom_70,axiom,
! [X] :
( cC98(X)
<=> ( cC2(X)
& cC96(X) ) ),
file('theBenchmark.p',axiom_70) ).
fof(axiom_71,axiom,
! [X] :
( cTEST(X)
<=> ( cC116(X)
& cC140(X) ) ),
file('theBenchmark.p',axiom_71) ).
fof(axiom_72,axiom,
cTEST(iV5475),
file('theBenchmark.p',axiom_72) ).
fof(axiom_73,axiom,
cTOP(iV5475),
file('theBenchmark.p',axiom_73) ).
fof(axiom_74,axiom,
cowlThing(iV5475),
file('theBenchmark.p',axiom_74) ).
fof(axiom_75,axiom,
! [X] :
( rR1(iV5475,X)
=> ~ cC112(X) ),
file('theBenchmark.p',axiom_75) ).
fof(axiom_76,axiom,
~ cC114(iV5475),
file('theBenchmark.p',axiom_76) ).
fof(axiom_77,axiom,
rR1(iV5475,iV5476),
file('theBenchmark.p',axiom_77) ).
fof(axiom_78,axiom,
cowlThing(iV5476),
file('theBenchmark.p',axiom_78) ).
fof(axiom_79,axiom,
~ cC34(iV5478),
file('theBenchmark.p',axiom_79) ).
fof(axiom_80,axiom,
~ cC12(iV5478),
file('theBenchmark.p',axiom_80) ).
fof(axiom_81,axiom,
! [X] :
( rR1(iV5478,X)
=> cC2(X) ),
file('theBenchmark.p',axiom_81) ).
fof(axiom_82,axiom,
~ cC30(iV5478),
file('theBenchmark.p',axiom_82) ).
fof(axiom_83,axiom,
~ cC130(iV5478),
file('theBenchmark.p',axiom_83) ).
fof(axiom_84,axiom,
~ cC118(iV5478),
file('theBenchmark.p',axiom_84) ).
fof(axiom_85,axiom,
cowlThing(iV5478),
file('theBenchmark.p',axiom_85) ).
fof(axiom_86,axiom,
cC2(iV5478),
file('theBenchmark.p',axiom_86) ).
fof(axiom_87,axiom,
! [X] :
( rR1(iV5478,X)
=> ~ cC28(X) ),
file('theBenchmark.p',axiom_87) ).
fof(axiom_88,axiom,
! [X] :
( rR1(iV5478,X)
=> ~ cC10(X) ),
file('theBenchmark.p',axiom_88) ).
fof(the_axiom,conjecture,
( cC140(iV5475)
& cC116(iV5475)
& cowlThing(iV5475)
& cC138(iV5475)
& ! [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_3_1,plain,
! [X] :
( ( cC10(X)
| cC2(X)
| cC8(X) )
& ( ( ~ cC2(X)
& ~ cC8(X) )
| ~ cC10(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(f_3_2,plain,
! [U_6] :
( ( cC10(U_6)
| cC2(U_6)
| cC8(U_6) )
& ( ( ~ cC2(U_6)
& ~ cC8(U_6) )
| ~ cC10(U_6) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_8] :
( cC10(U_8)
| cC2(U_8)
| cC8(U_8) )
& ! [U_7] :
( ( ~ cC2(U_7)
& ~ cC8(U_7) )
| ~ cC10(U_7) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
( ~ cC8(U_7)
| ~ cC10(U_7) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_5,plain,
( ~ cC2(U_7)
| ~ cC10(U_7) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_6,plain,
( cC10(U_8)
| cC2(U_8)
| cC8(U_8) ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X] :
( ( cC100(X)
| ~ cC94(X)
| cC98(X) )
& ( ( cC94(X)
& ~ cC98(X) )
| ~ cC100(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(f_4_2,plain,
! [U_9] :
( ( cC100(U_9)
| ~ cC94(U_9)
| cC98(U_9) )
& ( ( cC94(U_9)
& ~ cC98(U_9) )
| ~ cC100(U_9) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_11] :
( cC100(U_11)
| ~ cC94(U_11)
| cC98(U_11) )
& ! [U_10] :
( ( cC94(U_10)
& ~ cC98(U_10) )
| ~ cC100(U_10) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( ~ cC98(U_10)
| ~ cC100(U_10) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_5,plain,
( cC94(U_10)
| ~ cC100(U_10) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_6,plain,
( cC100(U_11)
| ~ cC94(U_11)
| cC98(U_11) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [X] :
( ( cC102(X)
| ! [Y] :
( ~ cC100(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC100(Y)
& rR1(X,Y) )
| ~ cC102(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_4]) ).
fof(f_5_2,plain,
! [U_14] :
( ( cC102(U_14)
| ! [U_13] :
( ~ cC100(U_13)
| ~ rR1(U_14,U_13) ) )
& ( ? [U_12] :
( cC100(U_12)
& rR1(U_14,U_12) )
| ~ cC102(U_14) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_16] :
( cC102(U_16)
| ! [U_13] :
( ~ cC100(U_13)
| ~ rR1(U_16,U_13) ) )
& ! [U_15] :
( ? [U_12] :
( cC100(U_12)
& rR1(U_15,U_12) )
| ~ cC102(U_15) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_16] :
( cC102(U_16)
| ! [U_13] :
( ~ cC100(U_13)
| ~ rR1(U_16,U_13) ) )
& ! [U_15] :
( ( cC100(sK1(U_15))
& rR1(U_15,sK1(U_15)) )
| ~ cC102(U_15) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_12,sK1(U_15))],[f_5_3]) ).
cnf(f_5_5,plain,
( rR1(U_15,sK1(U_15))
| ~ cC102(U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_6,plain,
( cC100(sK1(U_15))
| ~ cC102(U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_7,plain,
( cC102(U_16)
| ~ cC100(U_13)
| ~ rR1(U_16,U_13) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_6_1,plain,
! [X] :
( ( cC104(X)
| ~ cC88(X)
| cC102(X) )
& ( ( cC88(X)
& ~ cC102(X) )
| ~ cC104(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_5]) ).
fof(f_6_2,plain,
! [U_17] :
( ( cC104(U_17)
| ~ cC88(U_17)
| cC102(U_17) )
& ( ( cC88(U_17)
& ~ cC102(U_17) )
| ~ cC104(U_17) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_19] :
( cC104(U_19)
| ~ cC88(U_19)
| cC102(U_19) )
& ! [U_18] :
( ( cC88(U_18)
& ~ cC102(U_18) )
| ~ cC104(U_18) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
cnf(f_6_4,plain,
( ~ cC102(U_18)
| ~ cC104(U_18) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( cC88(U_18)
| ~ cC104(U_18) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_6,plain,
( cC104(U_19)
| ~ cC88(U_19)
| cC102(U_19) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [X] :
( ( cC106(X)
| ! [Y] :
( ~ cC104(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC104(Y)
& rR1(X,Y) )
| ~ cC106(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_6]) ).
fof(f_7_2,plain,
! [U_22] :
( ( cC106(U_22)
| ! [U_21] :
( ~ cC104(U_21)
| ~ rR1(U_22,U_21) ) )
& ( ? [U_20] :
( cC104(U_20)
& rR1(U_22,U_20) )
| ~ cC106(U_22) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_24] :
( cC106(U_24)
| ! [U_21] :
( ~ cC104(U_21)
| ~ rR1(U_24,U_21) ) )
& ! [U_23] :
( ? [U_20] :
( cC104(U_20)
& rR1(U_23,U_20) )
| ~ cC106(U_23) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_24] :
( cC106(U_24)
| ! [U_21] :
( ~ cC104(U_21)
| ~ rR1(U_24,U_21) ) )
& ! [U_23] :
( ( cC104(sK2(U_23))
& rR1(U_23,sK2(U_23)) )
| ~ cC106(U_23) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_20,sK2(U_23))],[f_7_3]) ).
cnf(f_7_5,plain,
( rR1(U_23,sK2(U_23))
| ~ cC106(U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_6,plain,
( cC104(sK2(U_23))
| ~ cC106(U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_7,plain,
( cC106(U_24)
| ~ cC104(U_21)
| ~ rR1(U_24,U_21) ),
inference(clausify,[status(thm)],[f_7_4]) ).
fof(f_8_1,plain,
! [X] :
( ( cC108(X)
| cC106(X)
| ~ cC84(X) )
& ( ( ~ cC106(X)
& cC84(X) )
| ~ cC108(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_7]) ).
fof(f_8_2,plain,
! [U_25] :
( ( cC108(U_25)
| cC106(U_25)
| ~ cC84(U_25) )
& ( ( ~ cC106(U_25)
& cC84(U_25) )
| ~ cC108(U_25) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_27] :
( cC108(U_27)
| cC106(U_27)
| ~ cC84(U_27) )
& ! [U_26] :
( ( ~ cC106(U_26)
& cC84(U_26) )
| ~ cC108(U_26) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( cC84(U_26)
| ~ cC108(U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( ~ cC106(U_26)
| ~ cC108(U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( cC108(U_27)
| cC106(U_27)
| ~ cC84(U_27) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X] :
( ( cC110(X)
| cC108(X)
| ~ cC62(X) )
& ( ( ~ cC108(X)
& cC62(X) )
| ~ cC110(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_8]) ).
fof(f_9_2,plain,
! [U_28] :
( ( cC110(U_28)
| cC108(U_28)
| ~ cC62(U_28) )
& ( ( ~ cC108(U_28)
& cC62(U_28) )
| ~ cC110(U_28) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_30] :
( cC110(U_30)
| cC108(U_30)
| ~ cC62(U_30) )
& ! [U_29] :
( ( ~ cC108(U_29)
& cC62(U_29) )
| ~ cC110(U_29) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( cC62(U_29)
| ~ cC110(U_29) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( ~ cC108(U_29)
| ~ cC110(U_29) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( cC110(U_30)
| cC108(U_30)
| ~ cC62(U_30) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X] :
( ( cC112(X)
| ! [Y] :
( cC110(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC110(Y)
& rR1(X,Y) )
| ~ cC112(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_9]) ).
fof(f_10_2,plain,
! [U_33] :
( ( cC112(U_33)
| ! [U_32] :
( cC110(U_32)
| ~ rR1(U_33,U_32) ) )
& ( ? [U_31] :
( ~ cC110(U_31)
& rR1(U_33,U_31) )
| ~ cC112(U_33) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_35] :
( cC112(U_35)
| ! [U_32] :
( cC110(U_32)
| ~ rR1(U_35,U_32) ) )
& ! [U_34] :
( ? [U_31] :
( ~ cC110(U_31)
& rR1(U_34,U_31) )
| ~ cC112(U_34) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
( ! [U_35] :
( cC112(U_35)
| ! [U_32] :
( cC110(U_32)
| ~ rR1(U_35,U_32) ) )
& ! [U_34] :
( ( ~ cC110(sK3(U_34))
& rR1(U_34,sK3(U_34)) )
| ~ cC112(U_34) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_31,sK3(U_34))],[f_10_3]) ).
cnf(f_10_5,plain,
( rR1(U_34,sK3(U_34))
| ~ cC112(U_34) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_6,plain,
( ~ cC110(sK3(U_34))
| ~ cC112(U_34) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_7,plain,
( cC112(U_35)
| cC110(U_32)
| ~ rR1(U_35,U_32) ),
inference(clausify,[status(thm)],[f_10_4]) ).
fof(f_11_1,plain,
! [X] :
( ( cC114(X)
| ! [Y] :
( ~ cC112(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC112(Y)
& rR1(X,Y) )
| ~ cC114(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_10]) ).
fof(f_11_2,plain,
! [U_38] :
( ( cC114(U_38)
| ! [U_37] :
( ~ cC112(U_37)
| ~ rR1(U_38,U_37) ) )
& ( ? [U_36] :
( cC112(U_36)
& rR1(U_38,U_36) )
| ~ cC114(U_38) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_40] :
( cC114(U_40)
| ! [U_37] :
( ~ cC112(U_37)
| ~ rR1(U_40,U_37) ) )
& ! [U_39] :
( ? [U_36] :
( cC112(U_36)
& rR1(U_39,U_36) )
| ~ cC114(U_39) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_40] :
( cC114(U_40)
| ! [U_37] :
( ~ cC112(U_37)
| ~ rR1(U_40,U_37) ) )
& ! [U_39] :
( ( cC112(sK4(U_39))
& rR1(U_39,sK4(U_39)) )
| ~ cC114(U_39) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_36,sK4(U_39))],[f_11_3]) ).
cnf(f_11_5,plain,
( rR1(U_39,sK4(U_39))
| ~ cC114(U_39) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( cC112(sK4(U_39))
| ~ cC114(U_39) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( cC114(U_40)
| ~ cC112(U_37)
| ~ rR1(U_40,U_37) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_12_1,plain,
! [X] :
( ( cC116(X)
| cC114(X)
| ~ cTOP(X) )
& ( ( ~ cC114(X)
& cTOP(X) )
| ~ cC116(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_11]) ).
fof(f_12_2,plain,
! [U_41] :
( ( cC116(U_41)
| cC114(U_41)
| ~ cTOP(U_41) )
& ( ( ~ cC114(U_41)
& cTOP(U_41) )
| ~ cC116(U_41) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_43] :
( cC116(U_43)
| cC114(U_43)
| ~ cTOP(U_43) )
& ! [U_42] :
( ( ~ cC114(U_42)
& cTOP(U_42) )
| ~ cC116(U_42) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( cTOP(U_42)
| ~ cC116(U_42) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_5,plain,
( ~ cC114(U_42)
| ~ cC116(U_42) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_6,plain,
( cC116(U_43)
| cC114(U_43)
| ~ cTOP(U_43) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [X] :
( ( cC118(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC118(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_12]) ).
fof(f_13_2,plain,
! [U_46] :
( ( cC118(U_46)
| ! [U_45] :
( cC2(U_45)
| ~ rR1(U_46,U_45) ) )
& ( ? [U_44] :
( ~ cC2(U_44)
& rR1(U_46,U_44) )
| ~ cC118(U_46) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_48] :
( cC118(U_48)
| ! [U_45] :
( cC2(U_45)
| ~ rR1(U_48,U_45) ) )
& ! [U_47] :
( ? [U_44] :
( ~ cC2(U_44)
& rR1(U_47,U_44) )
| ~ cC118(U_47) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_48] :
( cC118(U_48)
| ! [U_45] :
( cC2(U_45)
| ~ rR1(U_48,U_45) ) )
& ! [U_47] :
( ( ~ cC2(sK5(U_47))
& rR1(U_47,sK5(U_47)) )
| ~ cC118(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_44,sK5(U_47))],[f_13_3]) ).
cnf(f_13_5,plain,
( rR1(U_47,sK5(U_47))
| ~ cC118(U_47) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_6,plain,
( ~ cC2(sK5(U_47))
| ~ cC118(U_47) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_7,plain,
( cC118(U_48)
| cC2(U_45)
| ~ rR1(U_48,U_45) ),
inference(clausify,[status(thm)],[f_13_4]) ).
fof(f_14_1,plain,
! [X] :
( ( cC12(X)
| ! [Y] :
( ~ cC10(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC10(Y)
& rR1(X,Y) )
| ~ cC12(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_13]) ).
fof(f_14_2,plain,
! [U_51] :
( ( cC12(U_51)
| ! [U_50] :
( ~ cC10(U_50)
| ~ rR1(U_51,U_50) ) )
& ( ? [U_49] :
( cC10(U_49)
& rR1(U_51,U_49) )
| ~ cC12(U_51) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_53] :
( cC12(U_53)
| ! [U_50] :
( ~ cC10(U_50)
| ~ rR1(U_53,U_50) ) )
& ! [U_52] :
( ? [U_49] :
( cC10(U_49)
& rR1(U_52,U_49) )
| ~ cC12(U_52) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_53] :
( cC12(U_53)
| ! [U_50] :
( ~ cC10(U_50)
| ~ rR1(U_53,U_50) ) )
& ! [U_52] :
( ( cC10(sK6(U_52))
& rR1(U_52,sK6(U_52)) )
| ~ cC12(U_52) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_49,sK6(U_52))],[f_14_3]) ).
cnf(f_14_5,plain,
( rR1(U_52,sK6(U_52))
| ~ cC12(U_52) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_6,plain,
( cC10(sK6(U_52))
| ~ cC12(U_52) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_7,plain,
( cC12(U_53)
| ~ cC10(U_50)
| ~ rR1(U_53,U_50) ),
inference(clausify,[status(thm)],[f_14_4]) ).
fof(f_15_1,plain,
! [X] :
( ( cC120(X)
| ! [Y] :
( cC118(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC118(Y)
& rR1(X,Y) )
| ~ cC120(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_14]) ).
fof(f_15_2,plain,
! [U_56] :
( ( cC120(U_56)
| ! [U_55] :
( cC118(U_55)
| ~ rR1(U_56,U_55) ) )
& ( ? [U_54] :
( ~ cC118(U_54)
& rR1(U_56,U_54) )
| ~ cC120(U_56) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_58] :
( cC120(U_58)
| ! [U_55] :
( cC118(U_55)
| ~ rR1(U_58,U_55) ) )
& ! [U_57] :
( ? [U_54] :
( ~ cC118(U_54)
& rR1(U_57,U_54) )
| ~ cC120(U_57) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_58] :
( cC120(U_58)
| ! [U_55] :
( cC118(U_55)
| ~ rR1(U_58,U_55) ) )
& ! [U_57] :
( ( ~ cC118(sK7(U_57))
& rR1(U_57,sK7(U_57)) )
| ~ cC120(U_57) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_54,sK7(U_57))],[f_15_3]) ).
cnf(f_15_5,plain,
( rR1(U_57,sK7(U_57))
| ~ cC120(U_57) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_6,plain,
( ~ cC118(sK7(U_57))
| ~ cC120(U_57) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_7,plain,
( cC120(U_58)
| cC118(U_55)
| ~ rR1(U_58,U_55) ),
inference(clausify,[status(thm)],[f_15_4]) ).
fof(f_16_1,plain,
! [X] :
( ( cC122(X)
| ~ cC120(X)
| cC2(X) )
& ( ( cC120(X)
& ~ cC2(X) )
| ~ cC122(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_15]) ).
fof(f_16_2,plain,
! [U_59] :
( ( cC122(U_59)
| ~ cC120(U_59)
| cC2(U_59) )
& ( ( cC120(U_59)
& ~ cC2(U_59) )
| ~ cC122(U_59) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_61] :
( cC122(U_61)
| ~ cC120(U_61)
| cC2(U_61) )
& ! [U_60] :
( ( cC120(U_60)
& ~ cC2(U_60) )
| ~ cC122(U_60) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( ~ cC2(U_60)
| ~ cC122(U_60) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( cC120(U_60)
| ~ cC122(U_60) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_6,plain,
( cC122(U_61)
| ~ cC120(U_61)
| cC2(U_61) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X] :
( ( cC124(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC124(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(f_17_2,plain,
! [U_64] :
( ( cC124(U_64)
| ! [U_63] :
( cC2(U_63)
| ~ rR1(U_64,U_63) ) )
& ( ? [U_62] :
( ~ cC2(U_62)
& rR1(U_64,U_62) )
| ~ cC124(U_64) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_66] :
( cC124(U_66)
| ! [U_63] :
( cC2(U_63)
| ~ rR1(U_66,U_63) ) )
& ! [U_65] :
( ? [U_62] :
( ~ cC2(U_62)
& rR1(U_65,U_62) )
| ~ cC124(U_65) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_66] :
( cC124(U_66)
| ! [U_63] :
( cC2(U_63)
| ~ rR1(U_66,U_63) ) )
& ! [U_65] :
( ( ~ cC2(sK8(U_65))
& rR1(U_65,sK8(U_65)) )
| ~ cC124(U_65) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_62,sK8(U_65))],[f_17_3]) ).
cnf(f_17_5,plain,
( rR1(U_65,sK8(U_65))
| ~ cC124(U_65) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_6,plain,
( ~ cC2(sK8(U_65))
| ~ cC124(U_65) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_7,plain,
( cC124(U_66)
| cC2(U_63)
| ~ rR1(U_66,U_63) ),
inference(clausify,[status(thm)],[f_17_4]) ).
fof(f_18_1,plain,
! [X] :
( ( cC126(X)
| ~ cC2(X)
| ~ cC124(X) )
& ( ( cC2(X)
& cC124(X) )
| ~ cC126(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_17]) ).
fof(f_18_2,plain,
! [U_67] :
( ( cC126(U_67)
| ~ cC2(U_67)
| ~ cC124(U_67) )
& ( ( cC2(U_67)
& cC124(U_67) )
| ~ cC126(U_67) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_69] :
( cC126(U_69)
| ~ cC2(U_69)
| ~ cC124(U_69) )
& ! [U_68] :
( ( cC2(U_68)
& cC124(U_68) )
| ~ cC126(U_68) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
cnf(f_18_4,plain,
( cC124(U_68)
| ~ cC126(U_68) ),
inference(clausify,[status(thm)],[f_18_3]) ).
cnf(f_18_5,plain,
( cC2(U_68)
| ~ cC126(U_68) ),
inference(clausify,[status(thm)],[f_18_3]) ).
cnf(f_18_6,plain,
( cC126(U_69)
| ~ cC2(U_69)
| ~ cC124(U_69) ),
inference(clausify,[status(thm)],[f_18_3]) ).
fof(f_19_1,plain,
! [X] :
( ( cC128(X)
| ! [Y] :
( ~ cC126(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC126(Y)
& rR1(X,Y) )
| ~ cC128(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_18]) ).
fof(f_19_2,plain,
! [U_72] :
( ( cC128(U_72)
| ! [U_71] :
( ~ cC126(U_71)
| ~ rR1(U_72,U_71) ) )
& ( ? [U_70] :
( cC126(U_70)
& rR1(U_72,U_70) )
| ~ cC128(U_72) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_74] :
( cC128(U_74)
| ! [U_71] :
( ~ cC126(U_71)
| ~ rR1(U_74,U_71) ) )
& ! [U_73] :
( ? [U_70] :
( cC126(U_70)
& rR1(U_73,U_70) )
| ~ cC128(U_73) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
fof(f_19_4,plain,
( ! [U_74] :
( cC128(U_74)
| ! [U_71] :
( ~ cC126(U_71)
| ~ rR1(U_74,U_71) ) )
& ! [U_73] :
( ( cC126(sK9(U_73))
& rR1(U_73,sK9(U_73)) )
| ~ cC128(U_73) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_70,sK9(U_73))],[f_19_3]) ).
cnf(f_19_5,plain,
( rR1(U_73,sK9(U_73))
| ~ cC128(U_73) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_6,plain,
( cC126(sK9(U_73))
| ~ cC128(U_73) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_7,plain,
( cC128(U_74)
| ~ cC126(U_71)
| ~ rR1(U_74,U_71) ),
inference(clausify,[status(thm)],[f_19_4]) ).
fof(f_20_1,plain,
! [X] :
( ( cC130(X)
| cC128(X)
| cC2(X) )
& ( ( ~ cC128(X)
& ~ cC2(X) )
| ~ cC130(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_19]) ).
fof(f_20_2,plain,
! [U_75] :
( ( cC130(U_75)
| cC128(U_75)
| cC2(U_75) )
& ( ( ~ cC128(U_75)
& ~ cC2(U_75) )
| ~ cC130(U_75) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_77] :
( cC130(U_77)
| cC128(U_77)
| cC2(U_77) )
& ! [U_76] :
( ( ~ cC128(U_76)
& ~ cC2(U_76) )
| ~ cC130(U_76) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( ~ cC2(U_76)
| ~ cC130(U_76) ),
inference(clausify,[status(thm)],[f_20_3]) ).
cnf(f_20_5,plain,
( ~ cC128(U_76)
| ~ cC130(U_76) ),
inference(clausify,[status(thm)],[f_20_3]) ).
cnf(f_20_6,plain,
( cC130(U_77)
| cC128(U_77)
| cC2(U_77) ),
inference(clausify,[status(thm)],[f_20_3]) ).
fof(f_21_1,plain,
! [X] :
( ( cC132(X)
| ! [Y] :
( ~ cC130(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC130(Y)
& rR1(X,Y) )
| ~ cC132(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_20]) ).
fof(f_21_2,plain,
! [U_80] :
( ( cC132(U_80)
| ! [U_79] :
( ~ cC130(U_79)
| ~ rR1(U_80,U_79) ) )
& ( ? [U_78] :
( cC130(U_78)
& rR1(U_80,U_78) )
| ~ cC132(U_80) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ! [U_82] :
( cC132(U_82)
| ! [U_79] :
( ~ cC130(U_79)
| ~ rR1(U_82,U_79) ) )
& ! [U_81] :
( ? [U_78] :
( cC130(U_78)
& rR1(U_81,U_78) )
| ~ cC132(U_81) ) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
fof(f_21_4,plain,
( ! [U_82] :
( cC132(U_82)
| ! [U_79] :
( ~ cC130(U_79)
| ~ rR1(U_82,U_79) ) )
& ! [U_81] :
( ( cC130(sK10(U_81))
& rR1(U_81,sK10(U_81)) )
| ~ cC132(U_81) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_78,sK10(U_81))],[f_21_3]) ).
cnf(f_21_5,plain,
( rR1(U_81,sK10(U_81))
| ~ cC132(U_81) ),
inference(clausify,[status(thm)],[f_21_4]) ).
cnf(f_21_6,plain,
( cC130(sK10(U_81))
| ~ cC132(U_81) ),
inference(clausify,[status(thm)],[f_21_4]) ).
cnf(f_21_7,plain,
( cC132(U_82)
| ~ cC130(U_79)
| ~ rR1(U_82,U_79) ),
inference(clausify,[status(thm)],[f_21_4]) ).
fof(f_22_1,plain,
! [X] :
( ( cC134(X)
| cC132(X)
| ~ cC122(X) )
& ( ( ~ cC132(X)
& cC122(X) )
| ~ cC134(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_21]) ).
fof(f_22_2,plain,
! [U_83] :
( ( cC134(U_83)
| cC132(U_83)
| ~ cC122(U_83) )
& ( ( ~ cC132(U_83)
& cC122(U_83) )
| ~ cC134(U_83) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_85] :
( cC134(U_85)
| cC132(U_85)
| ~ cC122(U_85) )
& ! [U_84] :
( ( ~ cC132(U_84)
& cC122(U_84) )
| ~ cC134(U_84) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( cC122(U_84)
| ~ cC134(U_84) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( ~ cC132(U_84)
| ~ cC134(U_84) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_6,plain,
( cC134(U_85)
| cC132(U_85)
| ~ cC122(U_85) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [X] :
( ( cC136(X)
| ! [Y] :
( ~ cC134(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC134(Y)
& rR1(X,Y) )
| ~ cC136(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_22]) ).
fof(f_23_2,plain,
! [U_88] :
( ( cC136(U_88)
| ! [U_87] :
( ~ cC134(U_87)
| ~ rR1(U_88,U_87) ) )
& ( ? [U_86] :
( cC134(U_86)
& rR1(U_88,U_86) )
| ~ cC136(U_88) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_90] :
( cC136(U_90)
| ! [U_87] :
( ~ cC134(U_87)
| ~ rR1(U_90,U_87) ) )
& ! [U_89] :
( ? [U_86] :
( cC134(U_86)
& rR1(U_89,U_86) )
| ~ cC136(U_89) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_90] :
( cC136(U_90)
| ! [U_87] :
( ~ cC134(U_87)
| ~ rR1(U_90,U_87) ) )
& ! [U_89] :
( ( cC134(sK11(U_89))
& rR1(U_89,sK11(U_89)) )
| ~ cC136(U_89) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_86,sK11(U_89))],[f_23_3]) ).
cnf(f_23_5,plain,
( rR1(U_89,sK11(U_89))
| ~ cC136(U_89) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( cC134(sK11(U_89))
| ~ cC136(U_89) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( cC136(U_90)
| ~ cC134(U_87)
| ~ rR1(U_90,U_87) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
! [X] :
( ( cC138(X)
| ! [Y] :
( ~ cC136(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC136(Y)
& rR1(X,Y) )
| ~ cC138(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_23]) ).
fof(f_24_2,plain,
! [U_93] :
( ( cC138(U_93)
| ! [U_92] :
( ~ cC136(U_92)
| ~ rR1(U_93,U_92) ) )
& ( ? [U_91] :
( cC136(U_91)
& rR1(U_93,U_91) )
| ~ cC138(U_93) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_95] :
( cC138(U_95)
| ! [U_92] :
( ~ cC136(U_92)
| ~ rR1(U_95,U_92) ) )
& ! [U_94] :
( ? [U_91] :
( cC136(U_91)
& rR1(U_94,U_91) )
| ~ cC138(U_94) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
fof(f_24_4,plain,
( ! [U_95] :
( cC138(U_95)
| ! [U_92] :
( ~ cC136(U_92)
| ~ rR1(U_95,U_92) ) )
& ! [U_94] :
( ( cC136(sK12(U_94))
& rR1(U_94,sK12(U_94)) )
| ~ cC138(U_94) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_91,sK12(U_94))],[f_24_3]) ).
cnf(f_24_5,plain,
( rR1(U_94,sK12(U_94))
| ~ cC138(U_94) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_6,plain,
( cC136(sK12(U_94))
| ~ cC138(U_94) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_7,plain,
( cC138(U_95)
| ~ cC136(U_92)
| ~ rR1(U_95,U_92) ),
inference(clausify,[status(thm)],[f_24_4]) ).
fof(f_25_1,plain,
! [X] :
( ( cC14(X)
| ! [Y] :
( ~ cC12(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC12(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_24]) ).
fof(f_25_2,plain,
! [U_98] :
( ( cC14(U_98)
| ! [U_97] :
( ~ cC12(U_97)
| ~ rR1(U_98,U_97) ) )
& ( ? [U_96] :
( cC12(U_96)
& rR1(U_98,U_96) )
| ~ cC14(U_98) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_100] :
( cC14(U_100)
| ! [U_97] :
( ~ cC12(U_97)
| ~ rR1(U_100,U_97) ) )
& ! [U_99] :
( ? [U_96] :
( cC12(U_96)
& rR1(U_99,U_96) )
| ~ cC14(U_99) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
fof(f_25_4,plain,
( ! [U_100] :
( cC14(U_100)
| ! [U_97] :
( ~ cC12(U_97)
| ~ rR1(U_100,U_97) ) )
& ! [U_99] :
( ( cC12(sK13(U_99))
& rR1(U_99,sK13(U_99)) )
| ~ cC14(U_99) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_96,sK13(U_99))],[f_25_3]) ).
cnf(f_25_5,plain,
( rR1(U_99,sK13(U_99))
| ~ cC14(U_99) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_6,plain,
( cC12(sK13(U_99))
| ~ cC14(U_99) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_7,plain,
( cC14(U_100)
| ~ cC12(U_97)
| ~ rR1(U_100,U_97) ),
inference(clausify,[status(thm)],[f_25_4]) ).
fof(f_26_1,plain,
! [X] :
( ( cC140(X)
| ~ cC138(X)
| ~ cTOP(X) )
& ( ( cC138(X)
& cTOP(X) )
| ~ cC140(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_25]) ).
fof(f_26_2,plain,
! [U_101] :
( ( cC140(U_101)
| ~ cC138(U_101)
| ~ cTOP(U_101) )
& ( ( cC138(U_101)
& cTOP(U_101) )
| ~ cC140(U_101) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_103] :
( cC140(U_103)
| ~ cC138(U_103)
| ~ cTOP(U_103) )
& ! [U_102] :
( ( cC138(U_102)
& cTOP(U_102) )
| ~ cC140(U_102) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
cnf(f_26_4,plain,
( cTOP(U_102)
| ~ cC140(U_102) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_5,plain,
( cC138(U_102)
| ~ cC140(U_102) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_6,plain,
( cC140(U_103)
| ~ cC138(U_103)
| ~ cTOP(U_103) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [X] :
( ( cC16(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC16(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_26]) ).
fof(f_27_2,plain,
! [U_106] :
( ( cC16(U_106)
| ! [U_105] :
( cC2(U_105)
| ~ rR1(U_106,U_105) ) )
& ( ? [U_104] :
( ~ cC2(U_104)
& rR1(U_106,U_104) )
| ~ cC16(U_106) ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_108] :
( cC16(U_108)
| ! [U_105] :
( cC2(U_105)
| ~ rR1(U_108,U_105) ) )
& ! [U_107] :
( ? [U_104] :
( ~ cC2(U_104)
& rR1(U_107,U_104) )
| ~ cC16(U_107) ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
( ! [U_108] :
( cC16(U_108)
| ! [U_105] :
( cC2(U_105)
| ~ rR1(U_108,U_105) ) )
& ! [U_107] :
( ( ~ cC2(sK14(U_107))
& rR1(U_107,sK14(U_107)) )
| ~ cC16(U_107) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_104,sK14(U_107))],[f_27_3]) ).
cnf(f_27_5,plain,
( rR1(U_107,sK14(U_107))
| ~ cC16(U_107) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_6,plain,
( ~ cC2(sK14(U_107))
| ~ cC16(U_107) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_7,plain,
( cC16(U_108)
| cC2(U_105)
| ~ rR1(U_108,U_105) ),
inference(clausify,[status(thm)],[f_27_4]) ).
fof(f_28_1,plain,
! [X] :
( ( cC18(X)
| ~ cC2(X)
| ~ cC16(X) )
& ( ( cC2(X)
& cC16(X) )
| ~ cC18(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_27]) ).
fof(f_28_2,plain,
! [U_109] :
( ( cC18(U_109)
| ~ cC2(U_109)
| ~ cC16(U_109) )
& ( ( cC2(U_109)
& cC16(U_109) )
| ~ cC18(U_109) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_111] :
( cC18(U_111)
| ~ cC2(U_111)
| ~ cC16(U_111) )
& ! [U_110] :
( ( cC2(U_110)
& cC16(U_110) )
| ~ cC18(U_110) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
cnf(f_28_4,plain,
( cC16(U_110)
| ~ cC18(U_110) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( cC2(U_110)
| ~ cC18(U_110) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_6,plain,
( cC18(U_111)
| ~ cC2(U_111)
| ~ cC16(U_111) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X] :
( ( cC20(X)
| ! [Y] :
( ~ cC18(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC18(Y)
& rR1(X,Y) )
| ~ cC20(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_28]) ).
fof(f_29_2,plain,
! [U_114] :
( ( cC20(U_114)
| ! [U_113] :
( ~ cC18(U_113)
| ~ rR1(U_114,U_113) ) )
& ( ? [U_112] :
( cC18(U_112)
& rR1(U_114,U_112) )
| ~ cC20(U_114) ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_116] :
( cC20(U_116)
| ! [U_113] :
( ~ cC18(U_113)
| ~ rR1(U_116,U_113) ) )
& ! [U_115] :
( ? [U_112] :
( cC18(U_112)
& rR1(U_115,U_112) )
| ~ cC20(U_115) ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
fof(f_29_4,plain,
( ! [U_116] :
( cC20(U_116)
| ! [U_113] :
( ~ cC18(U_113)
| ~ rR1(U_116,U_113) ) )
& ! [U_115] :
( ( cC18(sK15(U_115))
& rR1(U_115,sK15(U_115)) )
| ~ cC20(U_115) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_112,sK15(U_115))],[f_29_3]) ).
cnf(f_29_5,plain,
( rR1(U_115,sK15(U_115))
| ~ cC20(U_115) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_6,plain,
( cC18(sK15(U_115))
| ~ cC20(U_115) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_7,plain,
( cC20(U_116)
| ~ cC18(U_113)
| ~ rR1(U_116,U_113) ),
inference(clausify,[status(thm)],[f_29_4]) ).
fof(f_30_1,plain,
! [X] :
( ( cC22(X)
| cC2(X)
| cC20(X) )
& ( ( ~ cC2(X)
& ~ cC20(X) )
| ~ cC22(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_29]) ).
fof(f_30_2,plain,
! [U_117] :
( ( cC22(U_117)
| cC2(U_117)
| cC20(U_117) )
& ( ( ~ cC2(U_117)
& ~ cC20(U_117) )
| ~ cC22(U_117) ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_119] :
( cC22(U_119)
| cC2(U_119)
| cC20(U_119) )
& ! [U_118] :
( ( ~ cC2(U_118)
& ~ cC20(U_118) )
| ~ cC22(U_118) ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
cnf(f_30_4,plain,
( ~ cC20(U_118)
| ~ cC22(U_118) ),
inference(clausify,[status(thm)],[f_30_3]) ).
cnf(f_30_5,plain,
( ~ cC2(U_118)
| ~ cC22(U_118) ),
inference(clausify,[status(thm)],[f_30_3]) ).
cnf(f_30_6,plain,
( cC22(U_119)
| cC2(U_119)
| cC20(U_119) ),
inference(clausify,[status(thm)],[f_30_3]) ).
fof(f_31_1,plain,
! [X] :
( ( cC24(X)
| ! [Y] :
( ~ cC22(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC22(Y)
& rR1(X,Y) )
| ~ cC24(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_30]) ).
fof(f_31_2,plain,
! [U_122] :
( ( cC24(U_122)
| ! [U_121] :
( ~ cC22(U_121)
| ~ rR1(U_122,U_121) ) )
& ( ? [U_120] :
( cC22(U_120)
& rR1(U_122,U_120) )
| ~ cC24(U_122) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_124] :
( cC24(U_124)
| ! [U_121] :
( ~ cC22(U_121)
| ~ rR1(U_124,U_121) ) )
& ! [U_123] :
( ? [U_120] :
( cC22(U_120)
& rR1(U_123,U_120) )
| ~ cC24(U_123) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
fof(f_31_4,plain,
( ! [U_124] :
( cC24(U_124)
| ! [U_121] :
( ~ cC22(U_121)
| ~ rR1(U_124,U_121) ) )
& ! [U_123] :
( ( cC22(sK16(U_123))
& rR1(U_123,sK16(U_123)) )
| ~ cC24(U_123) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_120,sK16(U_123))],[f_31_3]) ).
cnf(f_31_5,plain,
( rR1(U_123,sK16(U_123))
| ~ cC24(U_123) ),
inference(clausify,[status(thm)],[f_31_4]) ).
cnf(f_31_6,plain,
( cC22(sK16(U_123))
| ~ cC24(U_123) ),
inference(clausify,[status(thm)],[f_31_4]) ).
cnf(f_31_7,plain,
( cC24(U_124)
| ~ cC22(U_121)
| ~ rR1(U_124,U_121) ),
inference(clausify,[status(thm)],[f_31_4]) ).
fof(f_32_1,plain,
! [X] :
( ( cC26(X)
| cC24(X)
| ~ cC14(X) )
& ( ( ~ cC24(X)
& cC14(X) )
| ~ cC26(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_31]) ).
fof(f_32_2,plain,
! [U_125] :
( ( cC26(U_125)
| cC24(U_125)
| ~ cC14(U_125) )
& ( ( ~ cC24(U_125)
& cC14(U_125) )
| ~ cC26(U_125) ) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
( ! [U_127] :
( cC26(U_127)
| cC24(U_127)
| ~ cC14(U_127) )
& ! [U_126] :
( ( ~ cC24(U_126)
& cC14(U_126) )
| ~ cC26(U_126) ) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
cnf(f_32_4,plain,
( cC14(U_126)
| ~ cC26(U_126) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_5,plain,
( ~ cC24(U_126)
| ~ cC26(U_126) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_6,plain,
( cC26(U_127)
| cC24(U_127)
| ~ cC14(U_127) ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [X] :
( ( cC28(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_32]) ).
fof(f_33_2,plain,
! [U_130] :
( ( cC28(U_130)
| ! [U_129] :
( cC2(U_129)
| ~ rR1(U_130,U_129) ) )
& ( ? [U_128] :
( ~ cC2(U_128)
& rR1(U_130,U_128) )
| ~ cC28(U_130) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_132] :
( cC28(U_132)
| ! [U_129] :
( cC2(U_129)
| ~ rR1(U_132,U_129) ) )
& ! [U_131] :
( ? [U_128] :
( ~ cC2(U_128)
& rR1(U_131,U_128) )
| ~ cC28(U_131) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
fof(f_33_4,plain,
( ! [U_132] :
( cC28(U_132)
| ! [U_129] :
( cC2(U_129)
| ~ rR1(U_132,U_129) ) )
& ! [U_131] :
( ( ~ cC2(sK17(U_131))
& rR1(U_131,sK17(U_131)) )
| ~ cC28(U_131) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_128,sK17(U_131))],[f_33_3]) ).
cnf(f_33_5,plain,
( rR1(U_131,sK17(U_131))
| ~ cC28(U_131) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_6,plain,
( ~ cC2(sK17(U_131))
| ~ cC28(U_131) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_7,plain,
( cC28(U_132)
| cC2(U_129)
| ~ rR1(U_132,U_129) ),
inference(clausify,[status(thm)],[f_33_4]) ).
fof(f_34_1,plain,
! [X] :
( ( cC30(X)
| ! [Y] :
( ~ cC28(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC28(Y)
& rR1(X,Y) )
| ~ cC30(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_33]) ).
fof(f_34_2,plain,
! [U_135] :
( ( cC30(U_135)
| ! [U_134] :
( ~ cC28(U_134)
| ~ rR1(U_135,U_134) ) )
& ( ? [U_133] :
( cC28(U_133)
& rR1(U_135,U_133) )
| ~ cC30(U_135) ) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
( ! [U_137] :
( cC30(U_137)
| ! [U_134] :
( ~ cC28(U_134)
| ~ rR1(U_137,U_134) ) )
& ! [U_136] :
( ? [U_133] :
( cC28(U_133)
& rR1(U_136,U_133) )
| ~ cC30(U_136) ) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
fof(f_34_4,plain,
( ! [U_137] :
( cC30(U_137)
| ! [U_134] :
( ~ cC28(U_134)
| ~ rR1(U_137,U_134) ) )
& ! [U_136] :
( ( cC28(sK18(U_136))
& rR1(U_136,sK18(U_136)) )
| ~ cC30(U_136) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_133,sK18(U_136))],[f_34_3]) ).
cnf(f_34_5,plain,
( rR1(U_136,sK18(U_136))
| ~ cC30(U_136) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_6,plain,
( cC28(sK18(U_136))
| ~ cC30(U_136) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_7,plain,
( cC30(U_137)
| ~ cC28(U_134)
| ~ rR1(U_137,U_134) ),
inference(clausify,[status(thm)],[f_34_4]) ).
fof(f_35_1,plain,
! [X] :
( ( cC32(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC32(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_34]) ).
fof(f_35_2,plain,
! [U_140] :
( ( cC32(U_140)
| ! [U_139] :
( cC2(U_139)
| ~ rR1(U_140,U_139) ) )
& ( ? [U_138] :
( ~ cC2(U_138)
& rR1(U_140,U_138) )
| ~ cC32(U_140) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_142] :
( cC32(U_142)
| ! [U_139] :
( cC2(U_139)
| ~ rR1(U_142,U_139) ) )
& ! [U_141] :
( ? [U_138] :
( ~ cC2(U_138)
& rR1(U_141,U_138) )
| ~ cC32(U_141) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
fof(f_35_4,plain,
( ! [U_142] :
( cC32(U_142)
| ! [U_139] :
( cC2(U_139)
| ~ rR1(U_142,U_139) ) )
& ! [U_141] :
( ( ~ cC2(sK19(U_141))
& rR1(U_141,sK19(U_141)) )
| ~ cC32(U_141) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_138,sK19(U_141))],[f_35_3]) ).
cnf(f_35_5,plain,
( rR1(U_141,sK19(U_141))
| ~ cC32(U_141) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_6,plain,
( ~ cC2(sK19(U_141))
| ~ cC32(U_141) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_7,plain,
( cC32(U_142)
| cC2(U_139)
| ~ rR1(U_142,U_139) ),
inference(clausify,[status(thm)],[f_35_4]) ).
fof(f_36_1,plain,
! [X] :
( ( cC34(X)
| cC32(X)
| ~ cC30(X) )
& ( ( ~ cC32(X)
& cC30(X) )
| ~ cC34(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_35]) ).
fof(f_36_2,plain,
! [U_143] :
( ( cC34(U_143)
| cC32(U_143)
| ~ cC30(U_143) )
& ( ( ~ cC32(U_143)
& cC30(U_143) )
| ~ cC34(U_143) ) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_145] :
( cC34(U_145)
| cC32(U_145)
| ~ cC30(U_145) )
& ! [U_144] :
( ( ~ cC32(U_144)
& cC30(U_144) )
| ~ cC34(U_144) ) ),
inference(miniscope,[status(thm)],[f_36_2]) ).
cnf(f_36_4,plain,
( cC30(U_144)
| ~ cC34(U_144) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_5,plain,
( ~ cC32(U_144)
| ~ cC34(U_144) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_6,plain,
( cC34(U_145)
| cC32(U_145)
| ~ cC30(U_145) ),
inference(clausify,[status(thm)],[f_36_3]) ).
fof(f_37_1,plain,
! [X] :
( ( cC36(X)
| ! [Y] :
( ~ cC34(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC34(Y)
& rR1(X,Y) )
| ~ cC36(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_36]) ).
fof(f_37_2,plain,
! [U_148] :
( ( cC36(U_148)
| ! [U_147] :
( ~ cC34(U_147)
| ~ rR1(U_148,U_147) ) )
& ( ? [U_146] :
( cC34(U_146)
& rR1(U_148,U_146) )
| ~ cC36(U_148) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_150] :
( cC36(U_150)
| ! [U_147] :
( ~ cC34(U_147)
| ~ rR1(U_150,U_147) ) )
& ! [U_149] :
( ? [U_146] :
( cC34(U_146)
& rR1(U_149,U_146) )
| ~ cC36(U_149) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
fof(f_37_4,plain,
( ! [U_150] :
( cC36(U_150)
| ! [U_147] :
( ~ cC34(U_147)
| ~ rR1(U_150,U_147) ) )
& ! [U_149] :
( ( cC34(sK20(U_149))
& rR1(U_149,sK20(U_149)) )
| ~ cC36(U_149) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_146,sK20(U_149))],[f_37_3]) ).
cnf(f_37_5,plain,
( rR1(U_149,sK20(U_149))
| ~ cC36(U_149) ),
inference(clausify,[status(thm)],[f_37_4]) ).
cnf(f_37_6,plain,
( cC34(sK20(U_149))
| ~ cC36(U_149) ),
inference(clausify,[status(thm)],[f_37_4]) ).
cnf(f_37_7,plain,
( cC36(U_150)
| ~ cC34(U_147)
| ~ rR1(U_150,U_147) ),
inference(clausify,[status(thm)],[f_37_4]) ).
fof(f_38_1,plain,
! [X] :
( ( cC38(X)
| cC26(X)
| cC36(X) )
& ( ( ~ cC26(X)
& ~ cC36(X) )
| ~ cC38(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_37]) ).
fof(f_38_2,plain,
! [U_151] :
( ( cC38(U_151)
| cC26(U_151)
| cC36(U_151) )
& ( ( ~ cC26(U_151)
& ~ cC36(U_151) )
| ~ cC38(U_151) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_153] :
( cC38(U_153)
| cC26(U_153)
| cC36(U_153) )
& ! [U_152] :
( ( ~ cC26(U_152)
& ~ cC36(U_152) )
| ~ cC38(U_152) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
cnf(f_38_4,plain,
( ~ cC36(U_152)
| ~ cC38(U_152) ),
inference(clausify,[status(thm)],[f_38_3]) ).
cnf(f_38_5,plain,
( ~ cC26(U_152)
| ~ cC38(U_152) ),
inference(clausify,[status(thm)],[f_38_3]) ).
cnf(f_38_6,plain,
( cC38(U_153)
| cC26(U_153)
| cC36(U_153) ),
inference(clausify,[status(thm)],[f_38_3]) ).
fof(f_39_1,plain,
! [X] :
( ( cC4(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC4(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_38]) ).
fof(f_39_2,plain,
! [U_156] :
( ( cC4(U_156)
| ! [U_155] :
( cC2(U_155)
| ~ rR1(U_156,U_155) ) )
& ( ? [U_154] :
( ~ cC2(U_154)
& rR1(U_156,U_154) )
| ~ cC4(U_156) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_158] :
( cC4(U_158)
| ! [U_155] :
( cC2(U_155)
| ~ rR1(U_158,U_155) ) )
& ! [U_157] :
( ? [U_154] :
( ~ cC2(U_154)
& rR1(U_157,U_154) )
| ~ cC4(U_157) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
fof(f_39_4,plain,
( ! [U_158] :
( cC4(U_158)
| ! [U_155] :
( cC2(U_155)
| ~ rR1(U_158,U_155) ) )
& ! [U_157] :
( ( ~ cC2(sK21(U_157))
& rR1(U_157,sK21(U_157)) )
| ~ cC4(U_157) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_154,sK21(U_157))],[f_39_3]) ).
cnf(f_39_5,plain,
( rR1(U_157,sK21(U_157))
| ~ cC4(U_157) ),
inference(clausify,[status(thm)],[f_39_4]) ).
cnf(f_39_6,plain,
( ~ cC2(sK21(U_157))
| ~ cC4(U_157) ),
inference(clausify,[status(thm)],[f_39_4]) ).
cnf(f_39_7,plain,
( cC4(U_158)
| cC2(U_155)
| ~ rR1(U_158,U_155) ),
inference(clausify,[status(thm)],[f_39_4]) ).
fof(f_40_1,plain,
! [X] :
( ( cC40(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC40(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_39]) ).
fof(f_40_2,plain,
! [U_161] :
( ( cC40(U_161)
| ! [U_160] :
( cC2(U_160)
| ~ rR1(U_161,U_160) ) )
& ( ? [U_159] :
( ~ cC2(U_159)
& rR1(U_161,U_159) )
| ~ cC40(U_161) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_163] :
( cC40(U_163)
| ! [U_160] :
( cC2(U_160)
| ~ rR1(U_163,U_160) ) )
& ! [U_162] :
( ? [U_159] :
( ~ cC2(U_159)
& rR1(U_162,U_159) )
| ~ cC40(U_162) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
fof(f_40_4,plain,
( ! [U_163] :
( cC40(U_163)
| ! [U_160] :
( cC2(U_160)
| ~ rR1(U_163,U_160) ) )
& ! [U_162] :
( ( ~ cC2(sK22(U_162))
& rR1(U_162,sK22(U_162)) )
| ~ cC40(U_162) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_159,sK22(U_162))],[f_40_3]) ).
cnf(f_40_5,plain,
( rR1(U_162,sK22(U_162))
| ~ cC40(U_162) ),
inference(clausify,[status(thm)],[f_40_4]) ).
cnf(f_40_6,plain,
( ~ cC2(sK22(U_162))
| ~ cC40(U_162) ),
inference(clausify,[status(thm)],[f_40_4]) ).
cnf(f_40_7,plain,
( cC40(U_163)
| cC2(U_160)
| ~ rR1(U_163,U_160) ),
inference(clausify,[status(thm)],[f_40_4]) ).
fof(f_41_1,plain,
! [X] :
( ( cC42(X)
| ~ cC40(X)
| cC2(X) )
& ( ( cC40(X)
& ~ cC2(X) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_164] :
( ( cC42(U_164)
| ~ cC40(U_164)
| cC2(U_164) )
& ( ( cC40(U_164)
& ~ cC2(U_164) )
| ~ cC42(U_164) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_166] :
( cC42(U_166)
| ~ cC40(U_166)
| cC2(U_166) )
& ! [U_165] :
( ( cC40(U_165)
& ~ cC2(U_165) )
| ~ cC42(U_165) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
cnf(f_41_4,plain,
( ~ cC2(U_165)
| ~ cC42(U_165) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_5,plain,
( cC40(U_165)
| ~ cC42(U_165) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_6,plain,
( cC42(U_166)
| ~ cC40(U_166)
| cC2(U_166) ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_1,plain,
! [X] :
( ( cC44(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_41]) ).
fof(f_42_2,plain,
! [U_169] :
( ( cC44(U_169)
| ! [U_168] :
( cC2(U_168)
| ~ rR1(U_169,U_168) ) )
& ( ? [U_167] :
( ~ cC2(U_167)
& rR1(U_169,U_167) )
| ~ cC44(U_169) ) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
( ! [U_171] :
( cC44(U_171)
| ! [U_168] :
( cC2(U_168)
| ~ rR1(U_171,U_168) ) )
& ! [U_170] :
( ? [U_167] :
( ~ cC2(U_167)
& rR1(U_170,U_167) )
| ~ cC44(U_170) ) ),
inference(miniscope,[status(thm)],[f_42_2]) ).
fof(f_42_4,plain,
( ! [U_171] :
( cC44(U_171)
| ! [U_168] :
( cC2(U_168)
| ~ rR1(U_171,U_168) ) )
& ! [U_170] :
( ( ~ cC2(sK23(U_170))
& rR1(U_170,sK23(U_170)) )
| ~ cC44(U_170) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_167,sK23(U_170))],[f_42_3]) ).
cnf(f_42_5,plain,
( rR1(U_170,sK23(U_170))
| ~ cC44(U_170) ),
inference(clausify,[status(thm)],[f_42_4]) ).
cnf(f_42_6,plain,
( ~ cC2(sK23(U_170))
| ~ cC44(U_170) ),
inference(clausify,[status(thm)],[f_42_4]) ).
cnf(f_42_7,plain,
( cC44(U_171)
| cC2(U_168)
| ~ rR1(U_171,U_168) ),
inference(clausify,[status(thm)],[f_42_4]) ).
fof(f_43_1,plain,
! [X] :
( ( cC46(X)
| ! [Y] :
( cC44(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC44(Y)
& rR1(X,Y) )
| ~ cC46(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_42]) ).
fof(f_43_2,plain,
! [U_174] :
( ( cC46(U_174)
| ! [U_173] :
( cC44(U_173)
| ~ rR1(U_174,U_173) ) )
& ( ? [U_172] :
( ~ cC44(U_172)
& rR1(U_174,U_172) )
| ~ cC46(U_174) ) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
( ! [U_176] :
( cC46(U_176)
| ! [U_173] :
( cC44(U_173)
| ~ rR1(U_176,U_173) ) )
& ! [U_175] :
( ? [U_172] :
( ~ cC44(U_172)
& rR1(U_175,U_172) )
| ~ cC46(U_175) ) ),
inference(miniscope,[status(thm)],[f_43_2]) ).
fof(f_43_4,plain,
( ! [U_176] :
( cC46(U_176)
| ! [U_173] :
( cC44(U_173)
| ~ rR1(U_176,U_173) ) )
& ! [U_175] :
( ( ~ cC44(sK24(U_175))
& rR1(U_175,sK24(U_175)) )
| ~ cC46(U_175) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_172,sK24(U_175))],[f_43_3]) ).
cnf(f_43_5,plain,
( rR1(U_175,sK24(U_175))
| ~ cC46(U_175) ),
inference(clausify,[status(thm)],[f_43_4]) ).
cnf(f_43_6,plain,
( ~ cC44(sK24(U_175))
| ~ cC46(U_175) ),
inference(clausify,[status(thm)],[f_43_4]) ).
cnf(f_43_7,plain,
( cC46(U_176)
| cC44(U_173)
| ~ rR1(U_176,U_173) ),
inference(clausify,[status(thm)],[f_43_4]) ).
fof(f_44_1,plain,
! [X] :
( ( cC48(X)
| ~ cC46(X)
| ~ cC42(X) )
& ( ( cC46(X)
& cC42(X) )
| ~ cC48(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_177] :
( ( cC48(U_177)
| ~ cC46(U_177)
| ~ cC42(U_177) )
& ( ( cC46(U_177)
& cC42(U_177) )
| ~ cC48(U_177) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_179] :
( cC48(U_179)
| ~ cC46(U_179)
| ~ cC42(U_179) )
& ! [U_178] :
( ( cC46(U_178)
& cC42(U_178) )
| ~ cC48(U_178) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
cnf(f_44_4,plain,
( cC42(U_178)
| ~ cC48(U_178) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_5,plain,
( cC46(U_178)
| ~ cC48(U_178) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_6,plain,
( cC48(U_179)
| ~ cC46(U_179)
| ~ cC42(U_179) ),
inference(clausify,[status(thm)],[f_44_3]) ).
fof(f_45_1,plain,
! [X] :
( ( cC50(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_44]) ).
fof(f_45_2,plain,
! [U_182] :
( ( cC50(U_182)
| ! [U_181] :
( cC2(U_181)
| ~ rR1(U_182,U_181) ) )
& ( ? [U_180] :
( ~ cC2(U_180)
& rR1(U_182,U_180) )
| ~ cC50(U_182) ) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
( ! [U_184] :
( cC50(U_184)
| ! [U_181] :
( cC2(U_181)
| ~ rR1(U_184,U_181) ) )
& ! [U_183] :
( ? [U_180] :
( ~ cC2(U_180)
& rR1(U_183,U_180) )
| ~ cC50(U_183) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
fof(f_45_4,plain,
( ! [U_184] :
( cC50(U_184)
| ! [U_181] :
( cC2(U_181)
| ~ rR1(U_184,U_181) ) )
& ! [U_183] :
( ( ~ cC2(sK25(U_183))
& rR1(U_183,sK25(U_183)) )
| ~ cC50(U_183) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_180,sK25(U_183))],[f_45_3]) ).
cnf(f_45_5,plain,
( rR1(U_183,sK25(U_183))
| ~ cC50(U_183) ),
inference(clausify,[status(thm)],[f_45_4]) ).
cnf(f_45_6,plain,
( ~ cC2(sK25(U_183))
| ~ cC50(U_183) ),
inference(clausify,[status(thm)],[f_45_4]) ).
cnf(f_45_7,plain,
( cC50(U_184)
| cC2(U_181)
| ~ rR1(U_184,U_181) ),
inference(clausify,[status(thm)],[f_45_4]) ).
fof(f_46_1,plain,
! [X] :
( ( cC52(X)
| ~ cC50(X)
| ~ cC2(X) )
& ( ( cC50(X)
& cC2(X) )
| ~ cC52(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_45]) ).
fof(f_46_2,plain,
! [U_185] :
( ( cC52(U_185)
| ~ cC50(U_185)
| ~ cC2(U_185) )
& ( ( cC50(U_185)
& cC2(U_185) )
| ~ cC52(U_185) ) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_187] :
( cC52(U_187)
| ~ cC50(U_187)
| ~ cC2(U_187) )
& ! [U_186] :
( ( cC50(U_186)
& cC2(U_186) )
| ~ cC52(U_186) ) ),
inference(miniscope,[status(thm)],[f_46_2]) ).
cnf(f_46_4,plain,
( cC2(U_186)
| ~ cC52(U_186) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_5,plain,
( cC50(U_186)
| ~ cC52(U_186) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_6,plain,
( cC52(U_187)
| ~ cC50(U_187)
| ~ cC2(U_187) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [X] :
( ( cC54(X)
| ! [Y] :
( ~ cC52(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC52(Y)
& rR1(X,Y) )
| ~ cC54(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_46]) ).
fof(f_47_2,plain,
! [U_190] :
( ( cC54(U_190)
| ! [U_189] :
( ~ cC52(U_189)
| ~ rR1(U_190,U_189) ) )
& ( ? [U_188] :
( cC52(U_188)
& rR1(U_190,U_188) )
| ~ cC54(U_190) ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_192] :
( cC54(U_192)
| ! [U_189] :
( ~ cC52(U_189)
| ~ rR1(U_192,U_189) ) )
& ! [U_191] :
( ? [U_188] :
( cC52(U_188)
& rR1(U_191,U_188) )
| ~ cC54(U_191) ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
fof(f_47_4,plain,
( ! [U_192] :
( cC54(U_192)
| ! [U_189] :
( ~ cC52(U_189)
| ~ rR1(U_192,U_189) ) )
& ! [U_191] :
( ( cC52(sK26(U_191))
& rR1(U_191,sK26(U_191)) )
| ~ cC54(U_191) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_188,sK26(U_191))],[f_47_3]) ).
cnf(f_47_5,plain,
( rR1(U_191,sK26(U_191))
| ~ cC54(U_191) ),
inference(clausify,[status(thm)],[f_47_4]) ).
cnf(f_47_6,plain,
( cC52(sK26(U_191))
| ~ cC54(U_191) ),
inference(clausify,[status(thm)],[f_47_4]) ).
cnf(f_47_7,plain,
( cC54(U_192)
| ~ cC52(U_189)
| ~ rR1(U_192,U_189) ),
inference(clausify,[status(thm)],[f_47_4]) ).
fof(f_48_1,plain,
! [X] :
( ( cC56(X)
| cC2(X)
| cC54(X) )
& ( ( ~ cC2(X)
& ~ cC54(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_47]) ).
fof(f_48_2,plain,
! [U_193] :
( ( cC56(U_193)
| cC2(U_193)
| cC54(U_193) )
& ( ( ~ cC2(U_193)
& ~ cC54(U_193) )
| ~ cC56(U_193) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_195] :
( cC56(U_195)
| cC2(U_195)
| cC54(U_195) )
& ! [U_194] :
( ( ~ cC2(U_194)
& ~ cC54(U_194) )
| ~ cC56(U_194) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( ~ cC54(U_194)
| ~ cC56(U_194) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_5,plain,
( ~ cC2(U_194)
| ~ cC56(U_194) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_6,plain,
( cC56(U_195)
| cC2(U_195)
| cC54(U_195) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [X] :
( ( cC58(X)
| ! [Y] :
( ~ cC56(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC56(Y)
& rR1(X,Y) )
| ~ cC58(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_48]) ).
fof(f_49_2,plain,
! [U_198] :
( ( cC58(U_198)
| ! [U_197] :
( ~ cC56(U_197)
| ~ rR1(U_198,U_197) ) )
& ( ? [U_196] :
( cC56(U_196)
& rR1(U_198,U_196) )
| ~ cC58(U_198) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_200] :
( cC58(U_200)
| ! [U_197] :
( ~ cC56(U_197)
| ~ rR1(U_200,U_197) ) )
& ! [U_199] :
( ? [U_196] :
( cC56(U_196)
& rR1(U_199,U_196) )
| ~ cC58(U_199) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
fof(f_49_4,plain,
( ! [U_200] :
( cC58(U_200)
| ! [U_197] :
( ~ cC56(U_197)
| ~ rR1(U_200,U_197) ) )
& ! [U_199] :
( ( cC56(sK27(U_199))
& rR1(U_199,sK27(U_199)) )
| ~ cC58(U_199) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_196,sK27(U_199))],[f_49_3]) ).
cnf(f_49_5,plain,
( rR1(U_199,sK27(U_199))
| ~ cC58(U_199) ),
inference(clausify,[status(thm)],[f_49_4]) ).
cnf(f_49_6,plain,
( cC56(sK27(U_199))
| ~ cC58(U_199) ),
inference(clausify,[status(thm)],[f_49_4]) ).
cnf(f_49_7,plain,
( cC58(U_200)
| ~ cC56(U_197)
| ~ rR1(U_200,U_197) ),
inference(clausify,[status(thm)],[f_49_4]) ).
fof(f_50_1,plain,
! [X] :
( ( cC6(X)
| ~ cC4(X)
| ~ cC2(X) )
& ( ( cC4(X)
& cC2(X) )
| ~ cC6(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_49]) ).
fof(f_50_2,plain,
! [U_201] :
( ( cC6(U_201)
| ~ cC4(U_201)
| ~ cC2(U_201) )
& ( ( cC4(U_201)
& cC2(U_201) )
| ~ cC6(U_201) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_203] :
( cC6(U_203)
| ~ cC4(U_203)
| ~ cC2(U_203) )
& ! [U_202] :
( ( cC4(U_202)
& cC2(U_202) )
| ~ cC6(U_202) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
cnf(f_50_4,plain,
( cC2(U_202)
| ~ cC6(U_202) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_5,plain,
( cC4(U_202)
| ~ cC6(U_202) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_6,plain,
( cC6(U_203)
| ~ cC4(U_203)
| ~ cC2(U_203) ),
inference(clausify,[status(thm)],[f_50_3]) ).
fof(f_51_1,plain,
! [X] :
( ( cC60(X)
| cC58(X)
| ~ cC48(X) )
& ( ( ~ cC58(X)
& cC48(X) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_50]) ).
fof(f_51_2,plain,
! [U_204] :
( ( cC60(U_204)
| cC58(U_204)
| ~ cC48(U_204) )
& ( ( ~ cC58(U_204)
& cC48(U_204) )
| ~ cC60(U_204) ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_206] :
( cC60(U_206)
| cC58(U_206)
| ~ cC48(U_206) )
& ! [U_205] :
( ( ~ cC58(U_205)
& cC48(U_205) )
| ~ cC60(U_205) ) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
cnf(f_51_4,plain,
( cC48(U_205)
| ~ cC60(U_205) ),
inference(clausify,[status(thm)],[f_51_3]) ).
cnf(f_51_5,plain,
( ~ cC58(U_205)
| ~ cC60(U_205) ),
inference(clausify,[status(thm)],[f_51_3]) ).
cnf(f_51_6,plain,
( cC60(U_206)
| cC58(U_206)
| ~ cC48(U_206) ),
inference(clausify,[status(thm)],[f_51_3]) ).
fof(f_52_1,plain,
! [X] :
( ( cC62(X)
| cC60(X)
| ~ cC38(X) )
& ( ( ~ cC60(X)
& cC38(X) )
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_51]) ).
fof(f_52_2,plain,
! [U_207] :
( ( cC62(U_207)
| cC60(U_207)
| ~ cC38(U_207) )
& ( ( ~ cC60(U_207)
& cC38(U_207) )
| ~ cC62(U_207) ) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_209] :
( cC62(U_209)
| cC60(U_209)
| ~ cC38(U_209) )
& ! [U_208] :
( ( ~ cC60(U_208)
& cC38(U_208) )
| ~ cC62(U_208) ) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
cnf(f_52_4,plain,
( cC38(U_208)
| ~ cC62(U_208) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_5,plain,
( ~ cC60(U_208)
| ~ cC62(U_208) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_6,plain,
( cC62(U_209)
| cC60(U_209)
| ~ cC38(U_209) ),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_1,plain,
! [X] :
( ( cC64(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC64(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_52]) ).
fof(f_53_2,plain,
! [U_212] :
( ( cC64(U_212)
| ! [U_211] :
( cC2(U_211)
| ~ rR1(U_212,U_211) ) )
& ( ? [U_210] :
( ~ cC2(U_210)
& rR1(U_212,U_210) )
| ~ cC64(U_212) ) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_214] :
( cC64(U_214)
| ! [U_211] :
( cC2(U_211)
| ~ rR1(U_214,U_211) ) )
& ! [U_213] :
( ? [U_210] :
( ~ cC2(U_210)
& rR1(U_213,U_210) )
| ~ cC64(U_213) ) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
fof(f_53_4,plain,
( ! [U_214] :
( cC64(U_214)
| ! [U_211] :
( cC2(U_211)
| ~ rR1(U_214,U_211) ) )
& ! [U_213] :
( ( ~ cC2(sK28(U_213))
& rR1(U_213,sK28(U_213)) )
| ~ cC64(U_213) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_210,sK28(U_213))],[f_53_3]) ).
cnf(f_53_5,plain,
( rR1(U_213,sK28(U_213))
| ~ cC64(U_213) ),
inference(clausify,[status(thm)],[f_53_4]) ).
cnf(f_53_6,plain,
( ~ cC2(sK28(U_213))
| ~ cC64(U_213) ),
inference(clausify,[status(thm)],[f_53_4]) ).
cnf(f_53_7,plain,
( cC64(U_214)
| cC2(U_211)
| ~ rR1(U_214,U_211) ),
inference(clausify,[status(thm)],[f_53_4]) ).
fof(f_54_1,plain,
! [X] :
( ( cC66(X)
| ~ cC2(X)
| ~ cC64(X) )
& ( ( cC2(X)
& cC64(X) )
| ~ cC66(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_53]) ).
fof(f_54_2,plain,
! [U_215] :
( ( cC66(U_215)
| ~ cC2(U_215)
| ~ cC64(U_215) )
& ( ( cC2(U_215)
& cC64(U_215) )
| ~ cC66(U_215) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_217] :
( cC66(U_217)
| ~ cC2(U_217)
| ~ cC64(U_217) )
& ! [U_216] :
( ( cC2(U_216)
& cC64(U_216) )
| ~ cC66(U_216) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( cC64(U_216)
| ~ cC66(U_216) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( cC2(U_216)
| ~ cC66(U_216) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_6,plain,
( cC66(U_217)
| ~ cC2(U_217)
| ~ cC64(U_217) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [X] :
( ( cC68(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_54]) ).
fof(f_55_2,plain,
! [U_220] :
( ( cC68(U_220)
| ! [U_219] :
( cC2(U_219)
| ~ rR1(U_220,U_219) ) )
& ( ? [U_218] :
( ~ cC2(U_218)
& rR1(U_220,U_218) )
| ~ cC68(U_220) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_222] :
( cC68(U_222)
| ! [U_219] :
( cC2(U_219)
| ~ rR1(U_222,U_219) ) )
& ! [U_221] :
( ? [U_218] :
( ~ cC2(U_218)
& rR1(U_221,U_218) )
| ~ cC68(U_221) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
fof(f_55_4,plain,
( ! [U_222] :
( cC68(U_222)
| ! [U_219] :
( cC2(U_219)
| ~ rR1(U_222,U_219) ) )
& ! [U_221] :
( ( ~ cC2(sK29(U_221))
& rR1(U_221,sK29(U_221)) )
| ~ cC68(U_221) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_218,sK29(U_221))],[f_55_3]) ).
cnf(f_55_5,plain,
( rR1(U_221,sK29(U_221))
| ~ cC68(U_221) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_6,plain,
( ~ cC2(sK29(U_221))
| ~ cC68(U_221) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_7,plain,
( cC68(U_222)
| cC2(U_219)
| ~ rR1(U_222,U_219) ),
inference(clausify,[status(thm)],[f_55_4]) ).
fof(f_56_1,plain,
! [X] :
( ( cC70(X)
| ~ cC68(X)
| ~ cC2(X) )
& ( ( cC68(X)
& cC2(X) )
| ~ cC70(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_55]) ).
fof(f_56_2,plain,
! [U_223] :
( ( cC70(U_223)
| ~ cC68(U_223)
| ~ cC2(U_223) )
& ( ( cC68(U_223)
& cC2(U_223) )
| ~ cC70(U_223) ) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
( ! [U_225] :
( cC70(U_225)
| ~ cC68(U_225)
| ~ cC2(U_225) )
& ! [U_224] :
( ( cC68(U_224)
& cC2(U_224) )
| ~ cC70(U_224) ) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
cnf(f_56_4,plain,
( cC2(U_224)
| ~ cC70(U_224) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_5,plain,
( cC68(U_224)
| ~ cC70(U_224) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_6,plain,
( cC70(U_225)
| ~ cC68(U_225)
| ~ cC2(U_225) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
! [X] :
( ( cC72(X)
| ! [Y] :
( ~ cC70(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC70(Y)
& rR1(X,Y) )
| ~ cC72(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_56]) ).
fof(f_57_2,plain,
! [U_228] :
( ( cC72(U_228)
| ! [U_227] :
( ~ cC70(U_227)
| ~ rR1(U_228,U_227) ) )
& ( ? [U_226] :
( cC70(U_226)
& rR1(U_228,U_226) )
| ~ cC72(U_228) ) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
( ! [U_230] :
( cC72(U_230)
| ! [U_227] :
( ~ cC70(U_227)
| ~ rR1(U_230,U_227) ) )
& ! [U_229] :
( ? [U_226] :
( cC70(U_226)
& rR1(U_229,U_226) )
| ~ cC72(U_229) ) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
fof(f_57_4,plain,
( ! [U_230] :
( cC72(U_230)
| ! [U_227] :
( ~ cC70(U_227)
| ~ rR1(U_230,U_227) ) )
& ! [U_229] :
( ( cC70(sK30(U_229))
& rR1(U_229,sK30(U_229)) )
| ~ cC72(U_229) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_226,sK30(U_229))],[f_57_3]) ).
cnf(f_57_5,plain,
( rR1(U_229,sK30(U_229))
| ~ cC72(U_229) ),
inference(clausify,[status(thm)],[f_57_4]) ).
cnf(f_57_6,plain,
( cC70(sK30(U_229))
| ~ cC72(U_229) ),
inference(clausify,[status(thm)],[f_57_4]) ).
cnf(f_57_7,plain,
( cC72(U_230)
| ~ cC70(U_227)
| ~ rR1(U_230,U_227) ),
inference(clausify,[status(thm)],[f_57_4]) ).
fof(f_58_1,plain,
! [X] :
( ( cC74(X)
| ~ cC72(X)
| ~ cC66(X) )
& ( ( cC72(X)
& cC66(X) )
| ~ cC74(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_57]) ).
fof(f_58_2,plain,
! [U_231] :
( ( cC74(U_231)
| ~ cC72(U_231)
| ~ cC66(U_231) )
& ( ( cC72(U_231)
& cC66(U_231) )
| ~ cC74(U_231) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_233] :
( cC74(U_233)
| ~ cC72(U_233)
| ~ cC66(U_233) )
& ! [U_232] :
( ( cC72(U_232)
& cC66(U_232) )
| ~ cC74(U_232) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_4,plain,
( cC66(U_232)
| ~ cC74(U_232) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( cC72(U_232)
| ~ cC74(U_232) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_6,plain,
( cC74(U_233)
| ~ cC72(U_233)
| ~ cC66(U_233) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_1,plain,
! [X] :
( ( cC76(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_58]) ).
fof(f_59_2,plain,
! [U_236] :
( ( cC76(U_236)
| ! [U_235] :
( cC2(U_235)
| ~ rR1(U_236,U_235) ) )
& ( ? [U_234] :
( ~ cC2(U_234)
& rR1(U_236,U_234) )
| ~ cC76(U_236) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_238] :
( cC76(U_238)
| ! [U_235] :
( cC2(U_235)
| ~ rR1(U_238,U_235) ) )
& ! [U_237] :
( ? [U_234] :
( ~ cC2(U_234)
& rR1(U_237,U_234) )
| ~ cC76(U_237) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
fof(f_59_4,plain,
( ! [U_238] :
( cC76(U_238)
| ! [U_235] :
( cC2(U_235)
| ~ rR1(U_238,U_235) ) )
& ! [U_237] :
( ( ~ cC2(sK31(U_237))
& rR1(U_237,sK31(U_237)) )
| ~ cC76(U_237) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_234,sK31(U_237))],[f_59_3]) ).
cnf(f_59_5,plain,
( rR1(U_237,sK31(U_237))
| ~ cC76(U_237) ),
inference(clausify,[status(thm)],[f_59_4]) ).
cnf(f_59_6,plain,
( ~ cC2(sK31(U_237))
| ~ cC76(U_237) ),
inference(clausify,[status(thm)],[f_59_4]) ).
cnf(f_59_7,plain,
( cC76(U_238)
| cC2(U_235)
| ~ rR1(U_238,U_235) ),
inference(clausify,[status(thm)],[f_59_4]) ).
fof(f_60_1,plain,
! [X] :
( ( cC78(X)
| ~ cC2(X)
| ~ cC76(X) )
& ( ( cC2(X)
& cC76(X) )
| ~ cC78(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_59]) ).
fof(f_60_2,plain,
! [U_239] :
( ( cC78(U_239)
| ~ cC2(U_239)
| ~ cC76(U_239) )
& ( ( cC2(U_239)
& cC76(U_239) )
| ~ cC78(U_239) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_241] :
( cC78(U_241)
| ~ cC2(U_241)
| ~ cC76(U_241) )
& ! [U_240] :
( ( cC2(U_240)
& cC76(U_240) )
| ~ cC78(U_240) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
cnf(f_60_4,plain,
( cC76(U_240)
| ~ cC78(U_240) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_5,plain,
( cC2(U_240)
| ~ cC78(U_240) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_6,plain,
( cC78(U_241)
| ~ cC2(U_241)
| ~ cC76(U_241) ),
inference(clausify,[status(thm)],[f_60_3]) ).
fof(f_61_1,plain,
! [X] :
( ( cC8(X)
| ! [Y] :
( ~ cC6(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC6(Y)
& rR1(X,Y) )
| ~ cC8(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_60]) ).
fof(f_61_2,plain,
! [U_244] :
( ( cC8(U_244)
| ! [U_243] :
( ~ cC6(U_243)
| ~ rR1(U_244,U_243) ) )
& ( ? [U_242] :
( cC6(U_242)
& rR1(U_244,U_242) )
| ~ cC8(U_244) ) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
( ! [U_246] :
( cC8(U_246)
| ! [U_243] :
( ~ cC6(U_243)
| ~ rR1(U_246,U_243) ) )
& ! [U_245] :
( ? [U_242] :
( cC6(U_242)
& rR1(U_245,U_242) )
| ~ cC8(U_245) ) ),
inference(miniscope,[status(thm)],[f_61_2]) ).
fof(f_61_4,plain,
( ! [U_246] :
( cC8(U_246)
| ! [U_243] :
( ~ cC6(U_243)
| ~ rR1(U_246,U_243) ) )
& ! [U_245] :
( ( cC6(sK32(U_245))
& rR1(U_245,sK32(U_245)) )
| ~ cC8(U_245) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_242,sK32(U_245))],[f_61_3]) ).
cnf(f_61_5,plain,
( rR1(U_245,sK32(U_245))
| ~ cC8(U_245) ),
inference(clausify,[status(thm)],[f_61_4]) ).
cnf(f_61_6,plain,
( cC6(sK32(U_245))
| ~ cC8(U_245) ),
inference(clausify,[status(thm)],[f_61_4]) ).
cnf(f_61_7,plain,
( cC8(U_246)
| ~ cC6(U_243)
| ~ rR1(U_246,U_243) ),
inference(clausify,[status(thm)],[f_61_4]) ).
fof(f_62_1,plain,
! [X] :
( ( cC80(X)
| ! [Y] :
( ~ cC78(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC78(Y)
& rR1(X,Y) )
| ~ cC80(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_61]) ).
fof(f_62_2,plain,
! [U_249] :
( ( cC80(U_249)
| ! [U_248] :
( ~ cC78(U_248)
| ~ rR1(U_249,U_248) ) )
& ( ? [U_247] :
( cC78(U_247)
& rR1(U_249,U_247) )
| ~ cC80(U_249) ) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
fof(f_62_3,plain,
( ! [U_251] :
( cC80(U_251)
| ! [U_248] :
( ~ cC78(U_248)
| ~ rR1(U_251,U_248) ) )
& ! [U_250] :
( ? [U_247] :
( cC78(U_247)
& rR1(U_250,U_247) )
| ~ cC80(U_250) ) ),
inference(miniscope,[status(thm)],[f_62_2]) ).
fof(f_62_4,plain,
( ! [U_251] :
( cC80(U_251)
| ! [U_248] :
( ~ cC78(U_248)
| ~ rR1(U_251,U_248) ) )
& ! [U_250] :
( ( cC78(sK33(U_250))
& rR1(U_250,sK33(U_250)) )
| ~ cC80(U_250) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_247,sK33(U_250))],[f_62_3]) ).
cnf(f_62_5,plain,
( rR1(U_250,sK33(U_250))
| ~ cC80(U_250) ),
inference(clausify,[status(thm)],[f_62_4]) ).
cnf(f_62_6,plain,
( cC78(sK33(U_250))
| ~ cC80(U_250) ),
inference(clausify,[status(thm)],[f_62_4]) ).
cnf(f_62_7,plain,
( cC80(U_251)
| ~ cC78(U_248)
| ~ rR1(U_251,U_248) ),
inference(clausify,[status(thm)],[f_62_4]) ).
fof(f_63_1,plain,
! [X] :
( ( cC82(X)
| ! [Y] :
( cC80(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC80(Y)
& rR1(X,Y) )
| ~ cC82(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_62]) ).
fof(f_63_2,plain,
! [U_254] :
( ( cC82(U_254)
| ! [U_253] :
( cC80(U_253)
| ~ rR1(U_254,U_253) ) )
& ( ? [U_252] :
( ~ cC80(U_252)
& rR1(U_254,U_252) )
| ~ cC82(U_254) ) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
fof(f_63_3,plain,
( ! [U_256] :
( cC82(U_256)
| ! [U_253] :
( cC80(U_253)
| ~ rR1(U_256,U_253) ) )
& ! [U_255] :
( ? [U_252] :
( ~ cC80(U_252)
& rR1(U_255,U_252) )
| ~ cC82(U_255) ) ),
inference(miniscope,[status(thm)],[f_63_2]) ).
fof(f_63_4,plain,
( ! [U_256] :
( cC82(U_256)
| ! [U_253] :
( cC80(U_253)
| ~ rR1(U_256,U_253) ) )
& ! [U_255] :
( ( ~ cC80(sK34(U_255))
& rR1(U_255,sK34(U_255)) )
| ~ cC82(U_255) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_252,sK34(U_255))],[f_63_3]) ).
cnf(f_63_5,plain,
( rR1(U_255,sK34(U_255))
| ~ cC82(U_255) ),
inference(clausify,[status(thm)],[f_63_4]) ).
cnf(f_63_6,plain,
( ~ cC80(sK34(U_255))
| ~ cC82(U_255) ),
inference(clausify,[status(thm)],[f_63_4]) ).
cnf(f_63_7,plain,
( cC82(U_256)
| cC80(U_253)
| ~ rR1(U_256,U_253) ),
inference(clausify,[status(thm)],[f_63_4]) ).
fof(f_64_1,plain,
! [X] :
( ( cC84(X)
| ~ cC74(X)
| ~ cC82(X) )
& ( ( cC74(X)
& cC82(X) )
| ~ cC84(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_63]) ).
fof(f_64_2,plain,
! [U_257] :
( ( cC84(U_257)
| ~ cC74(U_257)
| ~ cC82(U_257) )
& ( ( cC74(U_257)
& cC82(U_257) )
| ~ cC84(U_257) ) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
fof(f_64_3,plain,
( ! [U_259] :
( cC84(U_259)
| ~ cC74(U_259)
| ~ cC82(U_259) )
& ! [U_258] :
( ( cC74(U_258)
& cC82(U_258) )
| ~ cC84(U_258) ) ),
inference(miniscope,[status(thm)],[f_64_2]) ).
cnf(f_64_4,plain,
( cC82(U_258)
| ~ cC84(U_258) ),
inference(clausify,[status(thm)],[f_64_3]) ).
cnf(f_64_5,plain,
( cC74(U_258)
| ~ cC84(U_258) ),
inference(clausify,[status(thm)],[f_64_3]) ).
cnf(f_64_6,plain,
( cC84(U_259)
| ~ cC74(U_259)
| ~ cC82(U_259) ),
inference(clausify,[status(thm)],[f_64_3]) ).
fof(f_65_1,plain,
! [X] :
( ( cC86(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC86(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
! [U_262] :
( ( cC86(U_262)
| ! [U_261] :
( cC2(U_261)
| ~ rR1(U_262,U_261) ) )
& ( ? [U_260] :
( ~ cC2(U_260)
& rR1(U_262,U_260) )
| ~ cC86(U_262) ) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
( ! [U_264] :
( cC86(U_264)
| ! [U_261] :
( cC2(U_261)
| ~ rR1(U_264,U_261) ) )
& ! [U_263] :
( ? [U_260] :
( ~ cC2(U_260)
& rR1(U_263,U_260) )
| ~ cC86(U_263) ) ),
inference(miniscope,[status(thm)],[f_65_2]) ).
fof(f_65_4,plain,
( ! [U_264] :
( cC86(U_264)
| ! [U_261] :
( cC2(U_261)
| ~ rR1(U_264,U_261) ) )
& ! [U_263] :
( ( ~ cC2(sK35(U_263))
& rR1(U_263,sK35(U_263)) )
| ~ cC86(U_263) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(U_260,sK35(U_263))],[f_65_3]) ).
cnf(f_65_5,plain,
( rR1(U_263,sK35(U_263))
| ~ cC86(U_263) ),
inference(clausify,[status(thm)],[f_65_4]) ).
cnf(f_65_6,plain,
( ~ cC2(sK35(U_263))
| ~ cC86(U_263) ),
inference(clausify,[status(thm)],[f_65_4]) ).
cnf(f_65_7,plain,
( cC86(U_264)
| cC2(U_261)
| ~ rR1(U_264,U_261) ),
inference(clausify,[status(thm)],[f_65_4]) ).
fof(f_66_1,plain,
! [X] :
( ( cC88(X)
| ~ cC2(X)
| ~ cC86(X) )
& ( ( cC2(X)
& cC86(X) )
| ~ cC88(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_265] :
( ( cC88(U_265)
| ~ cC2(U_265)
| ~ cC86(U_265) )
& ( ( cC2(U_265)
& cC86(U_265) )
| ~ cC88(U_265) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_267] :
( cC88(U_267)
| ~ cC2(U_267)
| ~ cC86(U_267) )
& ! [U_266] :
( ( cC2(U_266)
& cC86(U_266) )
| ~ cC88(U_266) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( cC86(U_266)
| ~ cC88(U_266) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( cC2(U_266)
| ~ cC88(U_266) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_6,plain,
( cC88(U_267)
| ~ cC2(U_267)
| ~ cC86(U_267) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_1,plain,
! [X] :
( ( cC90(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC90(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_66]) ).
fof(f_67_2,plain,
! [U_270] :
( ( cC90(U_270)
| ! [U_269] :
( cC2(U_269)
| ~ rR1(U_270,U_269) ) )
& ( ? [U_268] :
( ~ cC2(U_268)
& rR1(U_270,U_268) )
| ~ cC90(U_270) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_272] :
( cC90(U_272)
| ! [U_269] :
( cC2(U_269)
| ~ rR1(U_272,U_269) ) )
& ! [U_271] :
( ? [U_268] :
( ~ cC2(U_268)
& rR1(U_271,U_268) )
| ~ cC90(U_271) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
fof(f_67_4,plain,
( ! [U_272] :
( cC90(U_272)
| ! [U_269] :
( cC2(U_269)
| ~ rR1(U_272,U_269) ) )
& ! [U_271] :
( ( ~ cC2(sK36(U_271))
& rR1(U_271,sK36(U_271)) )
| ~ cC90(U_271) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(U_268,sK36(U_271))],[f_67_3]) ).
cnf(f_67_5,plain,
( rR1(U_271,sK36(U_271))
| ~ cC90(U_271) ),
inference(clausify,[status(thm)],[f_67_4]) ).
cnf(f_67_6,plain,
( ~ cC2(sK36(U_271))
| ~ cC90(U_271) ),
inference(clausify,[status(thm)],[f_67_4]) ).
cnf(f_67_7,plain,
( cC90(U_272)
| cC2(U_269)
| ~ rR1(U_272,U_269) ),
inference(clausify,[status(thm)],[f_67_4]) ).
fof(f_68_1,plain,
! [X] :
( ( cC92(X)
| ~ cC90(X)
| ~ cC2(X) )
& ( ( cC90(X)
& cC2(X) )
| ~ cC92(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_67]) ).
fof(f_68_2,plain,
! [U_273] :
( ( cC92(U_273)
| ~ cC90(U_273)
| ~ cC2(U_273) )
& ( ( cC90(U_273)
& cC2(U_273) )
| ~ cC92(U_273) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_275] :
( cC92(U_275)
| ~ cC90(U_275)
| ~ cC2(U_275) )
& ! [U_274] :
( ( cC90(U_274)
& cC2(U_274) )
| ~ cC92(U_274) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( cC2(U_274)
| ~ cC92(U_274) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( cC90(U_274)
| ~ cC92(U_274) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_6,plain,
( cC92(U_275)
| ~ cC90(U_275)
| ~ cC2(U_275) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
! [X] :
( ( cC94(X)
| ! [Y] :
( ~ cC92(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC92(Y)
& rR1(X,Y) )
| ~ cC94(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_68]) ).
fof(f_69_2,plain,
! [U_278] :
( ( cC94(U_278)
| ! [U_277] :
( ~ cC92(U_277)
| ~ rR1(U_278,U_277) ) )
& ( ? [U_276] :
( cC92(U_276)
& rR1(U_278,U_276) )
| ~ cC94(U_278) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_280] :
( cC94(U_280)
| ! [U_277] :
( ~ cC92(U_277)
| ~ rR1(U_280,U_277) ) )
& ! [U_279] :
( ? [U_276] :
( cC92(U_276)
& rR1(U_279,U_276) )
| ~ cC94(U_279) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
fof(f_69_4,plain,
( ! [U_280] :
( cC94(U_280)
| ! [U_277] :
( ~ cC92(U_277)
| ~ rR1(U_280,U_277) ) )
& ! [U_279] :
( ( cC92(sK37(U_279))
& rR1(U_279,sK37(U_279)) )
| ~ cC94(U_279) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(U_276,sK37(U_279))],[f_69_3]) ).
cnf(f_69_5,plain,
( rR1(U_279,sK37(U_279))
| ~ cC94(U_279) ),
inference(clausify,[status(thm)],[f_69_4]) ).
cnf(f_69_6,plain,
( cC92(sK37(U_279))
| ~ cC94(U_279) ),
inference(clausify,[status(thm)],[f_69_4]) ).
cnf(f_69_7,plain,
( cC94(U_280)
| ~ cC92(U_277)
| ~ rR1(U_280,U_277) ),
inference(clausify,[status(thm)],[f_69_4]) ).
fof(f_70_1,plain,
! [X] :
( ( cC96(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC96(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_69]) ).
fof(f_70_2,plain,
! [U_283] :
( ( cC96(U_283)
| ! [U_282] :
( cC2(U_282)
| ~ rR1(U_283,U_282) ) )
& ( ? [U_281] :
( ~ cC2(U_281)
& rR1(U_283,U_281) )
| ~ cC96(U_283) ) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
fof(f_70_3,plain,
( ! [U_285] :
( cC96(U_285)
| ! [U_282] :
( cC2(U_282)
| ~ rR1(U_285,U_282) ) )
& ! [U_284] :
( ? [U_281] :
( ~ cC2(U_281)
& rR1(U_284,U_281) )
| ~ cC96(U_284) ) ),
inference(miniscope,[status(thm)],[f_70_2]) ).
fof(f_70_4,plain,
( ! [U_285] :
( cC96(U_285)
| ! [U_282] :
( cC2(U_282)
| ~ rR1(U_285,U_282) ) )
& ! [U_284] :
( ( ~ cC2(sK38(U_284))
& rR1(U_284,sK38(U_284)) )
| ~ cC96(U_284) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(U_281,sK38(U_284))],[f_70_3]) ).
cnf(f_70_5,plain,
( rR1(U_284,sK38(U_284))
| ~ cC96(U_284) ),
inference(clausify,[status(thm)],[f_70_4]) ).
cnf(f_70_6,plain,
( ~ cC2(sK38(U_284))
| ~ cC96(U_284) ),
inference(clausify,[status(thm)],[f_70_4]) ).
cnf(f_70_7,plain,
( cC96(U_285)
| cC2(U_282)
| ~ rR1(U_285,U_282) ),
inference(clausify,[status(thm)],[f_70_4]) ).
fof(f_71_1,plain,
! [X] :
( ( cC98(X)
| ~ cC2(X)
| ~ cC96(X) )
& ( ( cC2(X)
& cC96(X) )
| ~ cC98(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_70]) ).
fof(f_71_2,plain,
! [U_286] :
( ( cC98(U_286)
| ~ cC2(U_286)
| ~ cC96(U_286) )
& ( ( cC2(U_286)
& cC96(U_286) )
| ~ cC98(U_286) ) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
( ! [U_288] :
( cC98(U_288)
| ~ cC2(U_288)
| ~ cC96(U_288) )
& ! [U_287] :
( ( cC2(U_287)
& cC96(U_287) )
| ~ cC98(U_287) ) ),
inference(miniscope,[status(thm)],[f_71_2]) ).
cnf(f_71_4,plain,
( cC96(U_287)
| ~ cC98(U_287) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_5,plain,
( cC2(U_287)
| ~ cC98(U_287) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_6,plain,
( cC98(U_288)
| ~ cC2(U_288)
| ~ cC96(U_288) ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC116(X)
| ~ cC140(X) )
& ( ( cC116(X)
& cC140(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_71]) ).
fof(f_72_2,plain,
! [U_289] :
( ( cTEST(U_289)
| ~ cC116(U_289)
| ~ cC140(U_289) )
& ( ( cC116(U_289)
& cC140(U_289) )
| ~ cTEST(U_289) ) ),
inference(variable_rename,[status(thm)],[f_72_1]) ).
fof(f_72_3,plain,
( ! [U_291] :
( cTEST(U_291)
| ~ cC116(U_291)
| ~ cC140(U_291) )
& ! [U_290] :
( ( cC116(U_290)
& cC140(U_290) )
| ~ cTEST(U_290) ) ),
inference(miniscope,[status(thm)],[f_72_2]) ).
cnf(f_72_4,plain,
( cC140(U_290)
| ~ cTEST(U_290) ),
inference(clausify,[status(thm)],[f_72_3]) ).
cnf(f_72_5,plain,
( cC116(U_290)
| ~ cTEST(U_290) ),
inference(clausify,[status(thm)],[f_72_3]) ).
cnf(f_72_6,plain,
( cTEST(U_291)
| ~ cC116(U_291)
| ~ cC140(U_291) ),
inference(clausify,[status(thm)],[f_72_3]) ).
fof(f_73_1,plain,
cTEST(iV5475),
inference(fof_nnf,[status(thm)],[axiom_72]) ).
cnf(f_73_2,plain,
cTEST(iV5475),
inference(clausify,[status(thm)],[f_73_1]) ).
fof(f_74_1,plain,
cTOP(iV5475),
inference(fof_nnf,[status(thm)],[axiom_73]) ).
cnf(f_74_2,plain,
cTOP(iV5475),
inference(clausify,[status(thm)],[f_74_1]) ).
fof(f_75_1,plain,
cowlThing(iV5475),
inference(fof_nnf,[status(thm)],[axiom_74]) ).
cnf(f_75_2,plain,
cowlThing(iV5475),
inference(clausify,[status(thm)],[f_75_1]) ).
fof(f_76_1,plain,
! [X] :
( ~ cC112(X)
| ~ rR1(iV5475,X) ),
inference(fof_nnf,[status(thm)],[axiom_75]) ).
fof(f_76_2,plain,
! [U_292] :
( ~ cC112(U_292)
| ~ rR1(iV5475,U_292) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
cnf(f_76_3,plain,
( ~ cC112(U_292)
| ~ rR1(iV5475,U_292) ),
inference(clausify,[status(thm)],[f_76_2]) ).
fof(f_77_1,plain,
~ cC114(iV5475),
inference(fof_nnf,[status(thm)],[axiom_76]) ).
cnf(f_77_2,plain,
~ cC114(iV5475),
inference(clausify,[status(thm)],[f_77_1]) ).
fof(f_78_1,plain,
rR1(iV5475,iV5476),
inference(fof_nnf,[status(thm)],[axiom_77]) ).
cnf(f_78_2,plain,
rR1(iV5475,iV5476),
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
cowlThing(iV5476),
inference(fof_nnf,[status(thm)],[axiom_78]) ).
cnf(f_79_2,plain,
cowlThing(iV5476),
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
~ cC34(iV5478),
inference(fof_nnf,[status(thm)],[axiom_79]) ).
cnf(f_80_2,plain,
~ cC34(iV5478),
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_81_1,plain,
~ cC12(iV5478),
inference(fof_nnf,[status(thm)],[axiom_80]) ).
cnf(f_81_2,plain,
~ cC12(iV5478),
inference(clausify,[status(thm)],[f_81_1]) ).
fof(f_82_1,plain,
! [X] :
( cC2(X)
| ~ rR1(iV5478,X) ),
inference(fof_nnf,[status(thm)],[axiom_81]) ).
fof(f_82_2,plain,
! [U_293] :
( cC2(U_293)
| ~ rR1(iV5478,U_293) ),
inference(variable_rename,[status(thm)],[f_82_1]) ).
cnf(f_82_3,plain,
( cC2(U_293)
| ~ rR1(iV5478,U_293) ),
inference(clausify,[status(thm)],[f_82_2]) ).
fof(f_83_1,plain,
~ cC30(iV5478),
inference(fof_nnf,[status(thm)],[axiom_82]) ).
cnf(f_83_2,plain,
~ cC30(iV5478),
inference(clausify,[status(thm)],[f_83_1]) ).
fof(f_84_1,plain,
~ cC130(iV5478),
inference(fof_nnf,[status(thm)],[axiom_83]) ).
cnf(f_84_2,plain,
~ cC130(iV5478),
inference(clausify,[status(thm)],[f_84_1]) ).
fof(f_85_1,plain,
~ cC118(iV5478),
inference(fof_nnf,[status(thm)],[axiom_84]) ).
cnf(f_85_2,plain,
~ cC118(iV5478),
inference(clausify,[status(thm)],[f_85_1]) ).
fof(f_86_1,plain,
cowlThing(iV5478),
inference(fof_nnf,[status(thm)],[axiom_85]) ).
cnf(f_86_2,plain,
cowlThing(iV5478),
inference(clausify,[status(thm)],[f_86_1]) ).
fof(f_87_1,plain,
cC2(iV5478),
inference(fof_nnf,[status(thm)],[axiom_86]) ).
cnf(f_87_2,plain,
cC2(iV5478),
inference(clausify,[status(thm)],[f_87_1]) ).
fof(f_88_1,plain,
! [X] :
( ~ cC28(X)
| ~ rR1(iV5478,X) ),
inference(fof_nnf,[status(thm)],[axiom_87]) ).
fof(f_88_2,plain,
! [U_294] :
( ~ cC28(U_294)
| ~ rR1(iV5478,U_294) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
cnf(f_88_3,plain,
( ~ cC28(U_294)
| ~ rR1(iV5478,U_294) ),
inference(clausify,[status(thm)],[f_88_2]) ).
fof(f_89_1,plain,
! [X] :
( ~ cC10(X)
| ~ rR1(iV5478,X) ),
inference(fof_nnf,[status(thm)],[axiom_88]) ).
fof(f_89_2,plain,
! [U_295] :
( ~ cC10(U_295)
| ~ rR1(iV5478,U_295) ),
inference(variable_rename,[status(thm)],[f_89_1]) ).
cnf(f_89_3,plain,
( ~ cC10(U_295)
| ~ rR1(iV5478,U_295) ),
inference(clausify,[status(thm)],[f_89_2]) ).
fof(f_90_1,negated_conjecture,
~ ( cC140(iV5475)
& cC116(iV5475)
& cowlThing(iV5475)
& cC138(iV5475)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_90_2,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_90_1]) ).
fof(f_90_3,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ? [U_297] :
( ( ~ xsd_string(U_297)
& ~ xsd_integer(U_297) )
| ( xsd_integer(U_297)
& xsd_string(U_297) ) )
| ? [U_296] :
( cowlNothing(U_296)
| ~ cowlThing(U_296) ) ),
inference(variable_rename,[status(thm)],[f_90_2]) ).
fof(f_90_4,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ? [U_301] :
( ~ xsd_string(U_301)
& ~ xsd_integer(U_301) )
| ? [U_300] :
( xsd_integer(U_300)
& xsd_string(U_300) )
| ? [U_299] : cowlNothing(U_299)
| ? [U_298] : ~ cowlThing(U_298) ),
inference(miniscope,[status(thm)],[f_90_3]) ).
fof(f_90_5,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ? [U_301] :
( ~ xsd_string(U_301)
& ~ xsd_integer(U_301) )
| ? [U_300] :
( xsd_integer(U_300)
& xsd_string(U_300) )
| ? [U_299] : cowlNothing(U_299)
| ~ cowlThing(sK39) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(U_298,sK39)],[f_90_4]) ).
fof(f_90_6,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ? [U_301] :
( ~ xsd_string(U_301)
& ~ xsd_integer(U_301) )
| ? [U_300] :
( xsd_integer(U_300)
& xsd_string(U_300) )
| cowlNothing(sK40)
| ~ cowlThing(sK39) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(U_299,sK40)],[f_90_5]) ).
fof(f_90_7,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ? [U_301] :
( ~ xsd_string(U_301)
& ~ xsd_integer(U_301) )
| ( xsd_integer(sK41)
& xsd_string(sK41) )
| cowlNothing(sK40)
| ~ cowlThing(sK39) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(U_300,sK41)],[f_90_6]) ).
fof(f_90_8,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| ( ~ xsd_string(sK42)
& ~ xsd_integer(sK42) )
| ( xsd_integer(sK41)
& xsd_string(sK41) )
| cowlNothing(sK40)
| ~ cowlThing(sK39) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(U_301,sK42)],[f_90_7]) ).
fof(f_90_9,negated_conjecture,
( ( ~ xsd_string(sK42)
| ~ sP1 )
& ( ~ xsd_integer(sK42)
| ~ sP1 )
& ( xsd_integer(sK41)
| ~ sP0 )
& ( xsd_string(sK41)
| ~ sP0 )
& ( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| sP1
| sP0
| cowlNothing(sK40)
| ~ cowlThing(sK39) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_90_8]) ).
cnf(f_90_10,negated_conjecture,
( ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ cowlThing(iV5475)
| ~ cC138(iV5475)
| sP1
| sP0
| cowlNothing(sK40)
| ~ cowlThing(sK39) ),
inference(clausify,[status(thm)],[f_90_9]) ).
cnf(f_90_11,negated_conjecture,
( xsd_string(sK41)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_90_9]) ).
cnf(f_90_12,negated_conjecture,
( xsd_integer(sK41)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_90_9]) ).
cnf(f_90_13,negated_conjecture,
( ~ xsd_integer(sK42)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_90_9]) ).
cnf(f_90_14,negated_conjecture,
( ~ xsd_string(sK42)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_90_9]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS148+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 12:15:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.54/0.84 % SZS status Theorem for theBenchmark
% 0.54/0.84 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------