%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS146+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 : n026.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:22 AM UTC 2026
% Result : Theorem 0.09s 0.44s
% Output : Proof 0.09s
% 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] :
( cC100(X)
<=> ? [Y] :
( cC98(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X] :
( cC102(X)
<=> ( cC100(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X] :
( cC104(X)
<=> ( cC4(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_5,axiom,
! [X] :
( cC106(X)
<=> ? [Y] :
( cC104(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_5) ).
fof(axiom_6,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& ~ cC34(X) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_7,axiom,
! [X] :
( cC110(X)
<=> ( ~ cC108(X)
& ~ cC102(X) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_8,axiom,
! [X] :
( cC112(X)
<=> ( cC4(X)
& ~ cC110(X) ) ),
file('theBenchmark.p',axiom_8) ).
fof(axiom_9,axiom,
! [X] :
( cC114(X)
<=> ( ~ cC112(X)
& ~ cC96(X) ) ),
file('theBenchmark.p',axiom_9) ).
fof(axiom_10,axiom,
! [X] :
( cC116(X)
<=> ( cC80(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_10) ).
fof(axiom_11,axiom,
! [X] :
( cC118(X)
<=> ( cC4(X)
& ~ cC10(X) ) ),
file('theBenchmark.p',axiom_11) ).
fof(axiom_12,axiom,
! [X] :
( cC12(X)
<=> ( ~ cC4(X)
& cC10(X) ) ),
file('theBenchmark.p',axiom_12) ).
fof(axiom_13,axiom,
! [X] :
( cC120(X)
<=> ( cC118(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_13) ).
fof(axiom_14,axiom,
! [X] :
( cC122(X)
<=> ? [Y] :
( cC120(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_14) ).
fof(axiom_15,axiom,
! [X] :
( cC124(X)
<=> ( cC4(X)
& ~ cC10(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X] :
( cC126(X)
<=> ( cC124(X)
& ~ cC34(X) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_17,axiom,
! [X] :
( cC128(X)
<=> ? [Y] :
( cC126(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_18,axiom,
! [X] :
( cC130(X)
<=> ( cC128(X)
& cC122(X) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_19,axiom,
! [X] :
( cC132(X)
<=> ( cC2(X)
& ~ cC4(X) ) ),
file('theBenchmark.p',axiom_19) ).
fof(axiom_20,axiom,
! [X] :
( cC134(X)
<=> ( cC132(X)
& ~ cC130(X) ) ),
file('theBenchmark.p',axiom_20) ).
fof(axiom_21,axiom,
! [X] :
( cC136(X)
<=> ( ~ cC134(X)
& cC116(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cC138(X)
<=> ? [Y] :
( ~ cC136(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_23,axiom,
! [X] :
( cC14(X)
<=> ( ~ cC12(X)
& ~ cC8(X) ) ),
file('theBenchmark.p',axiom_23) ).
fof(axiom_24,axiom,
! [X] :
( cC140(X)
<=> ( cC74(X)
& ~ cC138(X) ) ),
file('theBenchmark.p',axiom_24) ).
fof(axiom_25,axiom,
! [X] :
( cC18(X)
<=> ( cC2(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_26,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( cC18(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_26) ).
fof(axiom_27,axiom,
! [X] :
( cC22(X)
<=> ( cC20(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_28,axiom,
! [X] :
( cC24(X)
<=> ( cC2(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_28) ).
fof(axiom_29,axiom,
! [X] :
( cC26(X)
<=> ? [Y] :
( cC24(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC28(X)
<=> ( cC26(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_31,axiom,
! [X] :
( cC30(X)
<=> ( ~ cC22(X)
& ~ cC28(X) ) ),
file('theBenchmark.p',axiom_31) ).
fof(axiom_32,axiom,
! [X] :
( cC32(X)
<=> ( cC2(X)
& ~ cC30(X) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_33,axiom,
! [X] :
( cC36(X)
<=> ( cC4(X)
& ~ cC34(X) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_34,axiom,
! [X] :
( cC38(X)
<=> ? [Y] :
( cC36(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_34) ).
fof(axiom_35,axiom,
! [X] :
( cC40(X)
<=> ( cC38(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_35) ).
fof(axiom_36,axiom,
! [X] :
( cC42(X)
<=> ( cC4(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_36) ).
fof(axiom_37,axiom,
! [X] :
( cC44(X)
<=> ? [Y] :
( cC42(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_37) ).
fof(axiom_38,axiom,
! [X] :
( cC46(X)
<=> ( ~ cC34(X)
& cC44(X) ) ),
file('theBenchmark.p',axiom_38) ).
fof(axiom_39,axiom,
! [X] :
( cC48(X)
<=> ( ~ cC46(X)
& ~ cC40(X) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC50(X)
<=> ( ~ cC48(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC52(X)
<=> ( ~ cC32(X)
& ~ cC50(X) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_42,axiom,
! [X] :
( cC54(X)
<=> ( cC52(X)
& cC14(X) ) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_43,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC10(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_44,axiom,
! [X] :
( cC58(X)
<=> ( cC56(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_45,axiom,
! [X] :
( cC6(X)
<=> ( ~ cC4(X)
& cC2(X) ) ),
file('theBenchmark.p',axiom_45) ).
fof(axiom_46,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( cC58(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_46) ).
fof(axiom_47,axiom,
! [X] :
( cC62(X)
<=> ( ~ cC10(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_47) ).
fof(axiom_48,axiom,
! [X] :
( cC64(X)
<=> ( ~ cC34(X)
& cC62(X) ) ),
file('theBenchmark.p',axiom_48) ).
fof(axiom_49,axiom,
! [X] :
( cC66(X)
<=> ? [Y] :
( cC64(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_49) ).
fof(axiom_50,axiom,
! [X] :
( cC68(X)
<=> ( cC66(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_51,axiom,
! [X] :
( cC70(X)
<=> ( cC2(X)
& ~ cC4(X) ) ),
file('theBenchmark.p',axiom_51) ).
fof(axiom_52,axiom,
! [X] :
( cC72(X)
<=> ( cC70(X)
& ~ cC68(X) ) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_53,axiom,
! [X] :
( cC74(X)
<=> ( ~ cC72(X)
& cC54(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_54,axiom,
! [X] :
( cC76(X)
<=> ( cC4(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_54) ).
fof(axiom_55,axiom,
! [X] :
( cC78(X)
<=> ( cC10(X)
& ~ cC4(X) ) ),
file('theBenchmark.p',axiom_55) ).
fof(axiom_56,axiom,
! [X] :
( cC8(X)
<=> ( ~ cC2(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_56) ).
fof(axiom_57,axiom,
! [X] :
( cC80(X)
<=> ( ~ cC76(X)
& ~ cC78(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_58,axiom,
! [X] :
( cC82(X)
<=> ( cC2(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_58) ).
fof(axiom_59,axiom,
! [X] :
( cC84(X)
<=> ? [Y] :
( cC82(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_60,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_60) ).
fof(axiom_61,axiom,
! [X] :
( cC88(X)
<=> ( cC2(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_61) ).
fof(axiom_62,axiom,
! [X] :
( cC90(X)
<=> ? [Y] :
( cC88(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_62) ).
fof(axiom_63,axiom,
! [X] :
( cC92(X)
<=> ( ~ cC16(X)
& cC90(X) ) ),
file('theBenchmark.p',axiom_63) ).
fof(axiom_64,axiom,
! [X] :
( cC94(X)
<=> ( ~ cC92(X)
& ~ cC86(X) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC96(X)
<=> ( cC2(X)
& ~ cC94(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC98(X)
<=> ( ~ cC34(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cTEST(X)
<=> ( cC6(X)
& cC140(X) ) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_68,axiom,
~ cC84(iV822576),
file('theBenchmark.p',axiom_68) ).
fof(axiom_69,axiom,
~ cC132(iV822576),
file('theBenchmark.p',axiom_69) ).
fof(axiom_70,axiom,
~ cC102(iV822576),
file('theBenchmark.p',axiom_70) ).
fof(axiom_71,axiom,
~ cC134(iV822576),
file('theBenchmark.p',axiom_71) ).
fof(axiom_72,axiom,
cC16(iV822576),
file('theBenchmark.p',axiom_72) ).
fof(axiom_73,axiom,
! [X] :
( rR1(iV822576,X)
=> ~ cC88(X) ),
file('theBenchmark.p',axiom_73) ).
fof(axiom_74,axiom,
cC34(iV822576),
file('theBenchmark.p',axiom_74) ).
fof(axiom_75,axiom,
cC4(iV822576),
file('theBenchmark.p',axiom_75) ).
fof(axiom_76,axiom,
~ cC96(iV822576),
file('theBenchmark.p',axiom_76) ).
fof(axiom_77,axiom,
~ cC86(iV822576),
file('theBenchmark.p',axiom_77) ).
fof(axiom_78,axiom,
~ cC92(iV822576),
file('theBenchmark.p',axiom_78) ).
fof(axiom_79,axiom,
~ cC108(iV822576),
file('theBenchmark.p',axiom_79) ).
fof(axiom_80,axiom,
cowlThing(iV822576),
file('theBenchmark.p',axiom_80) ).
fof(axiom_81,axiom,
! [X] :
( rR1(iV822576,X)
=> ~ cC98(X) ),
file('theBenchmark.p',axiom_81) ).
fof(axiom_82,axiom,
~ cC90(iV822576),
file('theBenchmark.p',axiom_82) ).
fof(axiom_83,axiom,
~ cC100(iV822576),
file('theBenchmark.p',axiom_83) ).
fof(axiom_84,axiom,
~ cC10(iV822576),
file('theBenchmark.p',axiom_84) ).
fof(axiom_85,axiom,
~ cC18(iV822576),
file('theBenchmark.p',axiom_85) ).
fof(axiom_86,axiom,
~ cC76(iV822576),
file('theBenchmark.p',axiom_86) ).
fof(axiom_87,axiom,
~ cC112(iV822576),
file('theBenchmark.p',axiom_87) ).
fof(axiom_88,axiom,
~ cC78(iV822576),
file('theBenchmark.p',axiom_88) ).
fof(axiom_89,axiom,
cC2(iV822576),
file('theBenchmark.p',axiom_89) ).
fof(axiom_90,axiom,
! [X] :
( rR1(iV822576,X)
=> ~ cC82(X) ),
file('theBenchmark.p',axiom_90) ).
fof(the_axiom,conjecture,
( cC80(iV822576)
& cC136(iV822576)
& cC114(iV822576)
& cC110(iV822576)
& cC56(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& ! [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] :
( ( cC100(X)
| ! [Y] :
( ~ cC98(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC98(Y)
& rR1(X,Y) )
| ~ cC100(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(f_3_2,plain,
! [U_8] :
( ( cC100(U_8)
| ! [U_7] :
( ~ cC98(U_7)
| ~ rR1(U_8,U_7) ) )
& ( ? [U_6] :
( cC98(U_6)
& rR1(U_8,U_6) )
| ~ cC100(U_8) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_10] :
( cC100(U_10)
| ! [U_7] :
( ~ cC98(U_7)
| ~ rR1(U_10,U_7) ) )
& ! [U_9] :
( ? [U_6] :
( cC98(U_6)
& rR1(U_9,U_6) )
| ~ cC100(U_9) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_10] :
( cC100(U_10)
| ! [U_7] :
( ~ cC98(U_7)
| ~ rR1(U_10,U_7) ) )
& ! [U_9] :
( ( cC98(sK1(U_9))
& rR1(U_9,sK1(U_9)) )
| ~ cC100(U_9) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_6,sK1(U_9))],[f_3_3]) ).
cnf(f_3_5,plain,
( rR1(U_9,sK1(U_9))
| ~ cC100(U_9) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_6,plain,
( cC98(sK1(U_9))
| ~ cC100(U_9) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_7,plain,
( cC100(U_10)
| ~ cC98(U_7)
| ~ rR1(U_10,U_7) ),
inference(clausify,[status(thm)],[f_3_4]) ).
fof(f_4_1,plain,
! [X] :
( ( cC102(X)
| ~ cC100(X)
| ~ cC34(X) )
& ( ( cC100(X)
& cC34(X) )
| ~ cC102(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(f_4_2,plain,
! [U_11] :
( ( cC102(U_11)
| ~ cC100(U_11)
| ~ cC34(U_11) )
& ( ( cC100(U_11)
& cC34(U_11) )
| ~ cC102(U_11) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_13] :
( cC102(U_13)
| ~ cC100(U_13)
| ~ cC34(U_13) )
& ! [U_12] :
( ( cC100(U_12)
& cC34(U_12) )
| ~ cC102(U_12) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( cC34(U_12)
| ~ cC102(U_12) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_5,plain,
( cC100(U_12)
| ~ cC102(U_12) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_6,plain,
( cC102(U_13)
| ~ cC100(U_13)
| ~ cC34(U_13) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [X] :
( ( cC104(X)
| ~ cC4(X)
| ~ cC34(X) )
& ( ( cC4(X)
& cC34(X) )
| ~ cC104(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_4]) ).
fof(f_5_2,plain,
! [U_14] :
( ( cC104(U_14)
| ~ cC4(U_14)
| ~ cC34(U_14) )
& ( ( cC4(U_14)
& cC34(U_14) )
| ~ cC104(U_14) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_16] :
( cC104(U_16)
| ~ cC4(U_16)
| ~ cC34(U_16) )
& ! [U_15] :
( ( cC4(U_15)
& cC34(U_15) )
| ~ cC104(U_15) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
cnf(f_5_4,plain,
( cC34(U_15)
| ~ cC104(U_15) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_5,plain,
( cC4(U_15)
| ~ cC104(U_15) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_6,plain,
( cC104(U_16)
| ~ cC4(U_16)
| ~ cC34(U_16) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_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_5]) ).
fof(f_6_2,plain,
! [U_19] :
( ( cC106(U_19)
| ! [U_18] :
( ~ cC104(U_18)
| ~ rR1(U_19,U_18) ) )
& ( ? [U_17] :
( cC104(U_17)
& rR1(U_19,U_17) )
| ~ cC106(U_19) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_21] :
( cC106(U_21)
| ! [U_18] :
( ~ cC104(U_18)
| ~ rR1(U_21,U_18) ) )
& ! [U_20] :
( ? [U_17] :
( cC104(U_17)
& rR1(U_20,U_17) )
| ~ cC106(U_20) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_21] :
( cC106(U_21)
| ! [U_18] :
( ~ cC104(U_18)
| ~ rR1(U_21,U_18) ) )
& ! [U_20] :
( ( cC104(sK2(U_20))
& rR1(U_20,sK2(U_20)) )
| ~ cC106(U_20) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_17,sK2(U_20))],[f_6_3]) ).
cnf(f_6_5,plain,
( rR1(U_20,sK2(U_20))
| ~ cC106(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_6,plain,
( cC104(sK2(U_20))
| ~ cC106(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_7,plain,
( cC106(U_21)
| ~ cC104(U_18)
| ~ rR1(U_21,U_18) ),
inference(clausify,[status(thm)],[f_6_4]) ).
fof(f_7_1,plain,
! [X] :
( ( cC108(X)
| ~ cC106(X)
| cC34(X) )
& ( ( cC106(X)
& ~ cC34(X) )
| ~ cC108(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_6]) ).
fof(f_7_2,plain,
! [U_22] :
( ( cC108(U_22)
| ~ cC106(U_22)
| cC34(U_22) )
& ( ( cC106(U_22)
& ~ cC34(U_22) )
| ~ cC108(U_22) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_24] :
( cC108(U_24)
| ~ cC106(U_24)
| cC34(U_24) )
& ! [U_23] :
( ( cC106(U_23)
& ~ cC34(U_23) )
| ~ cC108(U_23) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
cnf(f_7_4,plain,
( ~ cC34(U_23)
| ~ cC108(U_23) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_5,plain,
( cC106(U_23)
| ~ cC108(U_23) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_6,plain,
( cC108(U_24)
| ~ cC106(U_24)
| cC34(U_24) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [X] :
( ( cC110(X)
| cC108(X)
| cC102(X) )
& ( ( ~ cC108(X)
& ~ cC102(X) )
| ~ cC110(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_7]) ).
fof(f_8_2,plain,
! [U_25] :
( ( cC110(U_25)
| cC108(U_25)
| cC102(U_25) )
& ( ( ~ cC108(U_25)
& ~ cC102(U_25) )
| ~ cC110(U_25) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_27] :
( cC110(U_27)
| cC108(U_27)
| cC102(U_27) )
& ! [U_26] :
( ( ~ cC108(U_26)
& ~ cC102(U_26) )
| ~ cC110(U_26) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( ~ cC102(U_26)
| ~ cC110(U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( ~ cC108(U_26)
| ~ cC110(U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( cC110(U_27)
| cC108(U_27)
| cC102(U_27) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X] :
( ( cC112(X)
| ~ cC4(X)
| cC110(X) )
& ( ( cC4(X)
& ~ cC110(X) )
| ~ cC112(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_8]) ).
fof(f_9_2,plain,
! [U_28] :
( ( cC112(U_28)
| ~ cC4(U_28)
| cC110(U_28) )
& ( ( cC4(U_28)
& ~ cC110(U_28) )
| ~ cC112(U_28) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_30] :
( cC112(U_30)
| ~ cC4(U_30)
| cC110(U_30) )
& ! [U_29] :
( ( cC4(U_29)
& ~ cC110(U_29) )
| ~ cC112(U_29) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( ~ cC110(U_29)
| ~ cC112(U_29) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( cC4(U_29)
| ~ cC112(U_29) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( cC112(U_30)
| ~ cC4(U_30)
| cC110(U_30) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X] :
( ( cC114(X)
| cC112(X)
| cC96(X) )
& ( ( ~ cC112(X)
& ~ cC96(X) )
| ~ cC114(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_9]) ).
fof(f_10_2,plain,
! [U_31] :
( ( cC114(U_31)
| cC112(U_31)
| cC96(U_31) )
& ( ( ~ cC112(U_31)
& ~ cC96(U_31) )
| ~ cC114(U_31) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_33] :
( cC114(U_33)
| cC112(U_33)
| cC96(U_33) )
& ! [U_32] :
( ( ~ cC112(U_32)
& ~ cC96(U_32) )
| ~ cC114(U_32) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
cnf(f_10_4,plain,
( ~ cC96(U_32)
| ~ cC114(U_32) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_5,plain,
( ~ cC112(U_32)
| ~ cC114(U_32) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_6,plain,
( cC114(U_33)
| cC112(U_33)
| cC96(U_33) ),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
! [X] :
( ( cC116(X)
| ~ cC80(X)
| ~ cC114(X) )
& ( ( cC80(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_10]) ).
fof(f_11_2,plain,
! [U_34] :
( ( cC116(U_34)
| ~ cC80(U_34)
| ~ cC114(U_34) )
& ( ( cC80(U_34)
& cC114(U_34) )
| ~ cC116(U_34) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_36] :
( cC116(U_36)
| ~ cC80(U_36)
| ~ cC114(U_36) )
& ! [U_35] :
( ( cC80(U_35)
& cC114(U_35) )
| ~ cC116(U_35) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
cnf(f_11_4,plain,
( cC114(U_35)
| ~ cC116(U_35) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_5,plain,
( cC80(U_35)
| ~ cC116(U_35) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_6,plain,
( cC116(U_36)
| ~ cC80(U_36)
| ~ cC114(U_36) ),
inference(clausify,[status(thm)],[f_11_3]) ).
fof(f_12_1,plain,
! [X] :
( ( cC118(X)
| ~ cC4(X)
| cC10(X) )
& ( ( cC4(X)
& ~ cC10(X) )
| ~ cC118(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_11]) ).
fof(f_12_2,plain,
! [U_37] :
( ( cC118(U_37)
| ~ cC4(U_37)
| cC10(U_37) )
& ( ( cC4(U_37)
& ~ cC10(U_37) )
| ~ cC118(U_37) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_39] :
( cC118(U_39)
| ~ cC4(U_39)
| cC10(U_39) )
& ! [U_38] :
( ( cC4(U_38)
& ~ cC10(U_38) )
| ~ cC118(U_38) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( ~ cC10(U_38)
| ~ cC118(U_38) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_5,plain,
( cC4(U_38)
| ~ cC118(U_38) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_6,plain,
( cC118(U_39)
| ~ cC4(U_39)
| cC10(U_39) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [X] :
( ( cC12(X)
| cC4(X)
| ~ cC10(X) )
& ( ( ~ cC4(X)
& cC10(X) )
| ~ cC12(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_12]) ).
fof(f_13_2,plain,
! [U_40] :
( ( cC12(U_40)
| cC4(U_40)
| ~ cC10(U_40) )
& ( ( ~ cC4(U_40)
& cC10(U_40) )
| ~ cC12(U_40) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_42] :
( cC12(U_42)
| cC4(U_42)
| ~ cC10(U_42) )
& ! [U_41] :
( ( ~ cC4(U_41)
& cC10(U_41) )
| ~ cC12(U_41) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( cC10(U_41)
| ~ cC12(U_41) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( ~ cC4(U_41)
| ~ cC12(U_41) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_6,plain,
( cC12(U_42)
| cC4(U_42)
| ~ cC10(U_42) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X] :
( ( cC120(X)
| ~ cC118(X)
| ~ cC34(X) )
& ( ( cC118(X)
& cC34(X) )
| ~ cC120(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_13]) ).
fof(f_14_2,plain,
! [U_43] :
( ( cC120(U_43)
| ~ cC118(U_43)
| ~ cC34(U_43) )
& ( ( cC118(U_43)
& cC34(U_43) )
| ~ cC120(U_43) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_45] :
( cC120(U_45)
| ~ cC118(U_45)
| ~ cC34(U_45) )
& ! [U_44] :
( ( cC118(U_44)
& cC34(U_44) )
| ~ cC120(U_44) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
cnf(f_14_4,plain,
( cC34(U_44)
| ~ cC120(U_44) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_5,plain,
( cC118(U_44)
| ~ cC120(U_44) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_6,plain,
( cC120(U_45)
| ~ cC118(U_45)
| ~ cC34(U_45) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [X] :
( ( cC122(X)
| ! [Y] :
( ~ cC120(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC120(Y)
& rR1(X,Y) )
| ~ cC122(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_14]) ).
fof(f_15_2,plain,
! [U_48] :
( ( cC122(U_48)
| ! [U_47] :
( ~ cC120(U_47)
| ~ rR1(U_48,U_47) ) )
& ( ? [U_46] :
( cC120(U_46)
& rR1(U_48,U_46) )
| ~ cC122(U_48) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_50] :
( cC122(U_50)
| ! [U_47] :
( ~ cC120(U_47)
| ~ rR1(U_50,U_47) ) )
& ! [U_49] :
( ? [U_46] :
( cC120(U_46)
& rR1(U_49,U_46) )
| ~ cC122(U_49) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_50] :
( cC122(U_50)
| ! [U_47] :
( ~ cC120(U_47)
| ~ rR1(U_50,U_47) ) )
& ! [U_49] :
( ( cC120(sK3(U_49))
& rR1(U_49,sK3(U_49)) )
| ~ cC122(U_49) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_46,sK3(U_49))],[f_15_3]) ).
cnf(f_15_5,plain,
( rR1(U_49,sK3(U_49))
| ~ cC122(U_49) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_6,plain,
( cC120(sK3(U_49))
| ~ cC122(U_49) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_7,plain,
( cC122(U_50)
| ~ cC120(U_47)
| ~ rR1(U_50,U_47) ),
inference(clausify,[status(thm)],[f_15_4]) ).
fof(f_16_1,plain,
! [X] :
( ( cC124(X)
| ~ cC4(X)
| cC10(X) )
& ( ( cC4(X)
& ~ cC10(X) )
| ~ cC124(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_15]) ).
fof(f_16_2,plain,
! [U_51] :
( ( cC124(U_51)
| ~ cC4(U_51)
| cC10(U_51) )
& ( ( cC4(U_51)
& ~ cC10(U_51) )
| ~ cC124(U_51) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_53] :
( cC124(U_53)
| ~ cC4(U_53)
| cC10(U_53) )
& ! [U_52] :
( ( cC4(U_52)
& ~ cC10(U_52) )
| ~ cC124(U_52) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( ~ cC10(U_52)
| ~ cC124(U_52) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( cC4(U_52)
| ~ cC124(U_52) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_6,plain,
( cC124(U_53)
| ~ cC4(U_53)
| cC10(U_53) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X] :
( ( cC126(X)
| ~ cC124(X)
| cC34(X) )
& ( ( cC124(X)
& ~ cC34(X) )
| ~ cC126(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(f_17_2,plain,
! [U_54] :
( ( cC126(U_54)
| ~ cC124(U_54)
| cC34(U_54) )
& ( ( cC124(U_54)
& ~ cC34(U_54) )
| ~ cC126(U_54) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_56] :
( cC126(U_56)
| ~ cC124(U_56)
| cC34(U_56) )
& ! [U_55] :
( ( cC124(U_55)
& ~ cC34(U_55) )
| ~ cC126(U_55) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( ~ cC34(U_55)
| ~ cC126(U_55) ),
inference(clausify,[status(thm)],[f_17_3]) ).
cnf(f_17_5,plain,
( cC124(U_55)
| ~ cC126(U_55) ),
inference(clausify,[status(thm)],[f_17_3]) ).
cnf(f_17_6,plain,
( cC126(U_56)
| ~ cC124(U_56)
| cC34(U_56) ),
inference(clausify,[status(thm)],[f_17_3]) ).
fof(f_18_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_17]) ).
fof(f_18_2,plain,
! [U_59] :
( ( cC128(U_59)
| ! [U_58] :
( ~ cC126(U_58)
| ~ rR1(U_59,U_58) ) )
& ( ? [U_57] :
( cC126(U_57)
& rR1(U_59,U_57) )
| ~ cC128(U_59) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_61] :
( cC128(U_61)
| ! [U_58] :
( ~ cC126(U_58)
| ~ rR1(U_61,U_58) ) )
& ! [U_60] :
( ? [U_57] :
( cC126(U_57)
& rR1(U_60,U_57) )
| ~ cC128(U_60) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
( ! [U_61] :
( cC128(U_61)
| ! [U_58] :
( ~ cC126(U_58)
| ~ rR1(U_61,U_58) ) )
& ! [U_60] :
( ( cC126(sK4(U_60))
& rR1(U_60,sK4(U_60)) )
| ~ cC128(U_60) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_57,sK4(U_60))],[f_18_3]) ).
cnf(f_18_5,plain,
( rR1(U_60,sK4(U_60))
| ~ cC128(U_60) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_6,plain,
( cC126(sK4(U_60))
| ~ cC128(U_60) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_7,plain,
( cC128(U_61)
| ~ cC126(U_58)
| ~ rR1(U_61,U_58) ),
inference(clausify,[status(thm)],[f_18_4]) ).
fof(f_19_1,plain,
! [X] :
( ( cC130(X)
| ~ cC128(X)
| ~ cC122(X) )
& ( ( cC128(X)
& cC122(X) )
| ~ cC130(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_18]) ).
fof(f_19_2,plain,
! [U_62] :
( ( cC130(U_62)
| ~ cC128(U_62)
| ~ cC122(U_62) )
& ( ( cC128(U_62)
& cC122(U_62) )
| ~ cC130(U_62) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_64] :
( cC130(U_64)
| ~ cC128(U_64)
| ~ cC122(U_64) )
& ! [U_63] :
( ( cC128(U_63)
& cC122(U_63) )
| ~ cC130(U_63) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( cC122(U_63)
| ~ cC130(U_63) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( cC128(U_63)
| ~ cC130(U_63) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_6,plain,
( cC130(U_64)
| ~ cC128(U_64)
| ~ cC122(U_64) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [X] :
( ( cC132(X)
| ~ cC2(X)
| cC4(X) )
& ( ( cC2(X)
& ~ cC4(X) )
| ~ cC132(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_19]) ).
fof(f_20_2,plain,
! [U_65] :
( ( cC132(U_65)
| ~ cC2(U_65)
| cC4(U_65) )
& ( ( cC2(U_65)
& ~ cC4(U_65) )
| ~ cC132(U_65) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_67] :
( cC132(U_67)
| ~ cC2(U_67)
| cC4(U_67) )
& ! [U_66] :
( ( cC2(U_66)
& ~ cC4(U_66) )
| ~ cC132(U_66) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( ~ cC4(U_66)
| ~ cC132(U_66) ),
inference(clausify,[status(thm)],[f_20_3]) ).
cnf(f_20_5,plain,
( cC2(U_66)
| ~ cC132(U_66) ),
inference(clausify,[status(thm)],[f_20_3]) ).
cnf(f_20_6,plain,
( cC132(U_67)
| ~ cC2(U_67)
| cC4(U_67) ),
inference(clausify,[status(thm)],[f_20_3]) ).
fof(f_21_1,plain,
! [X] :
( ( cC134(X)
| ~ cC132(X)
| cC130(X) )
& ( ( cC132(X)
& ~ cC130(X) )
| ~ cC134(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_20]) ).
fof(f_21_2,plain,
! [U_68] :
( ( cC134(U_68)
| ~ cC132(U_68)
| cC130(U_68) )
& ( ( cC132(U_68)
& ~ cC130(U_68) )
| ~ cC134(U_68) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ! [U_70] :
( cC134(U_70)
| ~ cC132(U_70)
| cC130(U_70) )
& ! [U_69] :
( ( cC132(U_69)
& ~ cC130(U_69) )
| ~ cC134(U_69) ) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( ~ cC130(U_69)
| ~ cC134(U_69) ),
inference(clausify,[status(thm)],[f_21_3]) ).
cnf(f_21_5,plain,
( cC132(U_69)
| ~ cC134(U_69) ),
inference(clausify,[status(thm)],[f_21_3]) ).
cnf(f_21_6,plain,
( cC134(U_70)
| ~ cC132(U_70)
| cC130(U_70) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [X] :
( ( cC136(X)
| cC134(X)
| ~ cC116(X) )
& ( ( ~ cC134(X)
& cC116(X) )
| ~ cC136(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_21]) ).
fof(f_22_2,plain,
! [U_71] :
( ( cC136(U_71)
| cC134(U_71)
| ~ cC116(U_71) )
& ( ( ~ cC134(U_71)
& cC116(U_71) )
| ~ cC136(U_71) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_73] :
( cC136(U_73)
| cC134(U_73)
| ~ cC116(U_73) )
& ! [U_72] :
( ( ~ cC134(U_72)
& cC116(U_72) )
| ~ cC136(U_72) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( cC116(U_72)
| ~ cC136(U_72) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( ~ cC134(U_72)
| ~ cC136(U_72) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_6,plain,
( cC136(U_73)
| cC134(U_73)
| ~ cC116(U_73) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_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_22]) ).
fof(f_23_2,plain,
! [U_76] :
( ( cC138(U_76)
| ! [U_75] :
( cC136(U_75)
| ~ rR1(U_76,U_75) ) )
& ( ? [U_74] :
( ~ cC136(U_74)
& rR1(U_76,U_74) )
| ~ cC138(U_76) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_78] :
( cC138(U_78)
| ! [U_75] :
( cC136(U_75)
| ~ rR1(U_78,U_75) ) )
& ! [U_77] :
( ? [U_74] :
( ~ cC136(U_74)
& rR1(U_77,U_74) )
| ~ cC138(U_77) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_78] :
( cC138(U_78)
| ! [U_75] :
( cC136(U_75)
| ~ rR1(U_78,U_75) ) )
& ! [U_77] :
( ( ~ cC136(sK5(U_77))
& rR1(U_77,sK5(U_77)) )
| ~ cC138(U_77) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_74,sK5(U_77))],[f_23_3]) ).
cnf(f_23_5,plain,
( rR1(U_77,sK5(U_77))
| ~ cC138(U_77) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( ~ cC136(sK5(U_77))
| ~ cC138(U_77) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( cC138(U_78)
| cC136(U_75)
| ~ rR1(U_78,U_75) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
! [X] :
( ( cC14(X)
| cC12(X)
| cC8(X) )
& ( ( ~ cC12(X)
& ~ cC8(X) )
| ~ cC14(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_23]) ).
fof(f_24_2,plain,
! [U_79] :
( ( cC14(U_79)
| cC12(U_79)
| cC8(U_79) )
& ( ( ~ cC12(U_79)
& ~ cC8(U_79) )
| ~ cC14(U_79) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_81] :
( cC14(U_81)
| cC12(U_81)
| cC8(U_81) )
& ! [U_80] :
( ( ~ cC12(U_80)
& ~ cC8(U_80) )
| ~ cC14(U_80) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
cnf(f_24_4,plain,
( ~ cC8(U_80)
| ~ cC14(U_80) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_5,plain,
( ~ cC12(U_80)
| ~ cC14(U_80) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_6,plain,
( cC14(U_81)
| cC12(U_81)
| cC8(U_81) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
! [X] :
( ( cC140(X)
| ~ cC74(X)
| cC138(X) )
& ( ( cC74(X)
& ~ cC138(X) )
| ~ cC140(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_24]) ).
fof(f_25_2,plain,
! [U_82] :
( ( cC140(U_82)
| ~ cC74(U_82)
| cC138(U_82) )
& ( ( cC74(U_82)
& ~ cC138(U_82) )
| ~ cC140(U_82) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_84] :
( cC140(U_84)
| ~ cC74(U_84)
| cC138(U_84) )
& ! [U_83] :
( ( cC74(U_83)
& ~ cC138(U_83) )
| ~ cC140(U_83) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( ~ cC138(U_83)
| ~ cC140(U_83) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( cC74(U_83)
| ~ cC140(U_83) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_6,plain,
( cC140(U_84)
| ~ cC74(U_84)
| cC138(U_84) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [X] :
( ( cC18(X)
| ~ cC2(X)
| cC16(X) )
& ( ( cC2(X)
& ~ cC16(X) )
| ~ cC18(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_25]) ).
fof(f_26_2,plain,
! [U_85] :
( ( cC18(U_85)
| ~ cC2(U_85)
| cC16(U_85) )
& ( ( cC2(U_85)
& ~ cC16(U_85) )
| ~ cC18(U_85) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_87] :
( cC18(U_87)
| ~ cC2(U_87)
| cC16(U_87) )
& ! [U_86] :
( ( cC2(U_86)
& ~ cC16(U_86) )
| ~ cC18(U_86) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
cnf(f_26_4,plain,
( ~ cC16(U_86)
| ~ cC18(U_86) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_5,plain,
( cC2(U_86)
| ~ cC18(U_86) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_6,plain,
( cC18(U_87)
| ~ cC2(U_87)
| cC16(U_87) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_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_26]) ).
fof(f_27_2,plain,
! [U_90] :
( ( cC20(U_90)
| ! [U_89] :
( ~ cC18(U_89)
| ~ rR1(U_90,U_89) ) )
& ( ? [U_88] :
( cC18(U_88)
& rR1(U_90,U_88) )
| ~ cC20(U_90) ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_92] :
( cC20(U_92)
| ! [U_89] :
( ~ cC18(U_89)
| ~ rR1(U_92,U_89) ) )
& ! [U_91] :
( ? [U_88] :
( cC18(U_88)
& rR1(U_91,U_88) )
| ~ cC20(U_91) ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
( ! [U_92] :
( cC20(U_92)
| ! [U_89] :
( ~ cC18(U_89)
| ~ rR1(U_92,U_89) ) )
& ! [U_91] :
( ( cC18(sK6(U_91))
& rR1(U_91,sK6(U_91)) )
| ~ cC20(U_91) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_88,sK6(U_91))],[f_27_3]) ).
cnf(f_27_5,plain,
( rR1(U_91,sK6(U_91))
| ~ cC20(U_91) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_6,plain,
( cC18(sK6(U_91))
| ~ cC20(U_91) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_7,plain,
( cC20(U_92)
| ~ cC18(U_89)
| ~ rR1(U_92,U_89) ),
inference(clausify,[status(thm)],[f_27_4]) ).
fof(f_28_1,plain,
! [X] :
( ( cC22(X)
| ~ cC20(X)
| ~ cC16(X) )
& ( ( cC20(X)
& cC16(X) )
| ~ cC22(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_27]) ).
fof(f_28_2,plain,
! [U_93] :
( ( cC22(U_93)
| ~ cC20(U_93)
| ~ cC16(U_93) )
& ( ( cC20(U_93)
& cC16(U_93) )
| ~ cC22(U_93) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_95] :
( cC22(U_95)
| ~ cC20(U_95)
| ~ cC16(U_95) )
& ! [U_94] :
( ( cC20(U_94)
& cC16(U_94) )
| ~ cC22(U_94) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
cnf(f_28_4,plain,
( cC16(U_94)
| ~ cC22(U_94) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( cC20(U_94)
| ~ cC22(U_94) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_6,plain,
( cC22(U_95)
| ~ cC20(U_95)
| ~ cC16(U_95) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X] :
( ( cC24(X)
| ~ cC2(X)
| ~ cC16(X) )
& ( ( cC2(X)
& cC16(X) )
| ~ cC24(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_28]) ).
fof(f_29_2,plain,
! [U_96] :
( ( cC24(U_96)
| ~ cC2(U_96)
| ~ cC16(U_96) )
& ( ( cC2(U_96)
& cC16(U_96) )
| ~ cC24(U_96) ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_98] :
( cC24(U_98)
| ~ cC2(U_98)
| ~ cC16(U_98) )
& ! [U_97] :
( ( cC2(U_97)
& cC16(U_97) )
| ~ cC24(U_97) ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( cC16(U_97)
| ~ cC24(U_97) ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_5,plain,
( cC2(U_97)
| ~ cC24(U_97) ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_6,plain,
( cC24(U_98)
| ~ cC2(U_98)
| ~ cC16(U_98) ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_1,plain,
! [X] :
( ( cC26(X)
| ! [Y] :
( ~ cC24(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC24(Y)
& rR1(X,Y) )
| ~ cC26(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_29]) ).
fof(f_30_2,plain,
! [U_101] :
( ( cC26(U_101)
| ! [U_100] :
( ~ cC24(U_100)
| ~ rR1(U_101,U_100) ) )
& ( ? [U_99] :
( cC24(U_99)
& rR1(U_101,U_99) )
| ~ cC26(U_101) ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_103] :
( cC26(U_103)
| ! [U_100] :
( ~ cC24(U_100)
| ~ rR1(U_103,U_100) ) )
& ! [U_102] :
( ? [U_99] :
( cC24(U_99)
& rR1(U_102,U_99) )
| ~ cC26(U_102) ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
fof(f_30_4,plain,
( ! [U_103] :
( cC26(U_103)
| ! [U_100] :
( ~ cC24(U_100)
| ~ rR1(U_103,U_100) ) )
& ! [U_102] :
( ( cC24(sK7(U_102))
& rR1(U_102,sK7(U_102)) )
| ~ cC26(U_102) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_99,sK7(U_102))],[f_30_3]) ).
cnf(f_30_5,plain,
( rR1(U_102,sK7(U_102))
| ~ cC26(U_102) ),
inference(clausify,[status(thm)],[f_30_4]) ).
cnf(f_30_6,plain,
( cC24(sK7(U_102))
| ~ cC26(U_102) ),
inference(clausify,[status(thm)],[f_30_4]) ).
cnf(f_30_7,plain,
( cC26(U_103)
| ~ cC24(U_100)
| ~ rR1(U_103,U_100) ),
inference(clausify,[status(thm)],[f_30_4]) ).
fof(f_31_1,plain,
! [X] :
( ( cC28(X)
| ~ cC26(X)
| cC16(X) )
& ( ( cC26(X)
& ~ cC16(X) )
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_30]) ).
fof(f_31_2,plain,
! [U_104] :
( ( cC28(U_104)
| ~ cC26(U_104)
| cC16(U_104) )
& ( ( cC26(U_104)
& ~ cC16(U_104) )
| ~ cC28(U_104) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_106] :
( cC28(U_106)
| ~ cC26(U_106)
| cC16(U_106) )
& ! [U_105] :
( ( cC26(U_105)
& ~ cC16(U_105) )
| ~ cC28(U_105) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( ~ cC16(U_105)
| ~ cC28(U_105) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_5,plain,
( cC26(U_105)
| ~ cC28(U_105) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_6,plain,
( cC28(U_106)
| ~ cC26(U_106)
| cC16(U_106) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [X] :
( ( cC30(X)
| cC22(X)
| cC28(X) )
& ( ( ~ cC22(X)
& ~ cC28(X) )
| ~ cC30(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_31]) ).
fof(f_32_2,plain,
! [U_107] :
( ( cC30(U_107)
| cC22(U_107)
| cC28(U_107) )
& ( ( ~ cC22(U_107)
& ~ cC28(U_107) )
| ~ cC30(U_107) ) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
( ! [U_109] :
( cC30(U_109)
| cC22(U_109)
| cC28(U_109) )
& ! [U_108] :
( ( ~ cC22(U_108)
& ~ cC28(U_108) )
| ~ cC30(U_108) ) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
cnf(f_32_4,plain,
( ~ cC28(U_108)
| ~ cC30(U_108) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_5,plain,
( ~ cC22(U_108)
| ~ cC30(U_108) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_6,plain,
( cC30(U_109)
| cC22(U_109)
| cC28(U_109) ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [X] :
( ( cC32(X)
| ~ cC2(X)
| cC30(X) )
& ( ( cC2(X)
& ~ cC30(X) )
| ~ cC32(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_32]) ).
fof(f_33_2,plain,
! [U_110] :
( ( cC32(U_110)
| ~ cC2(U_110)
| cC30(U_110) )
& ( ( cC2(U_110)
& ~ cC30(U_110) )
| ~ cC32(U_110) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_112] :
( cC32(U_112)
| ~ cC2(U_112)
| cC30(U_112) )
& ! [U_111] :
( ( cC2(U_111)
& ~ cC30(U_111) )
| ~ cC32(U_111) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
cnf(f_33_4,plain,
( ~ cC30(U_111)
| ~ cC32(U_111) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_5,plain,
( cC2(U_111)
| ~ cC32(U_111) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_6,plain,
( cC32(U_112)
| ~ cC2(U_112)
| cC30(U_112) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [X] :
( ( cC36(X)
| ~ cC4(X)
| cC34(X) )
& ( ( cC4(X)
& ~ cC34(X) )
| ~ cC36(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_33]) ).
fof(f_34_2,plain,
! [U_113] :
( ( cC36(U_113)
| ~ cC4(U_113)
| cC34(U_113) )
& ( ( cC4(U_113)
& ~ cC34(U_113) )
| ~ cC36(U_113) ) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
( ! [U_115] :
( cC36(U_115)
| ~ cC4(U_115)
| cC34(U_115) )
& ! [U_114] :
( ( cC4(U_114)
& ~ cC34(U_114) )
| ~ cC36(U_114) ) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
cnf(f_34_4,plain,
( ~ cC34(U_114)
| ~ cC36(U_114) ),
inference(clausify,[status(thm)],[f_34_3]) ).
cnf(f_34_5,plain,
( cC4(U_114)
| ~ cC36(U_114) ),
inference(clausify,[status(thm)],[f_34_3]) ).
cnf(f_34_6,plain,
( cC36(U_115)
| ~ cC4(U_115)
| cC34(U_115) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_35_1,plain,
! [X] :
( ( cC38(X)
| ! [Y] :
( ~ cC36(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC36(Y)
& rR1(X,Y) )
| ~ cC38(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_34]) ).
fof(f_35_2,plain,
! [U_118] :
( ( cC38(U_118)
| ! [U_117] :
( ~ cC36(U_117)
| ~ rR1(U_118,U_117) ) )
& ( ? [U_116] :
( cC36(U_116)
& rR1(U_118,U_116) )
| ~ cC38(U_118) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_120] :
( cC38(U_120)
| ! [U_117] :
( ~ cC36(U_117)
| ~ rR1(U_120,U_117) ) )
& ! [U_119] :
( ? [U_116] :
( cC36(U_116)
& rR1(U_119,U_116) )
| ~ cC38(U_119) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
fof(f_35_4,plain,
( ! [U_120] :
( cC38(U_120)
| ! [U_117] :
( ~ cC36(U_117)
| ~ rR1(U_120,U_117) ) )
& ! [U_119] :
( ( cC36(sK8(U_119))
& rR1(U_119,sK8(U_119)) )
| ~ cC38(U_119) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_116,sK8(U_119))],[f_35_3]) ).
cnf(f_35_5,plain,
( rR1(U_119,sK8(U_119))
| ~ cC38(U_119) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_6,plain,
( cC36(sK8(U_119))
| ~ cC38(U_119) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_7,plain,
( cC38(U_120)
| ~ cC36(U_117)
| ~ rR1(U_120,U_117) ),
inference(clausify,[status(thm)],[f_35_4]) ).
fof(f_36_1,plain,
! [X] :
( ( cC40(X)
| ~ cC38(X)
| ~ cC34(X) )
& ( ( cC38(X)
& cC34(X) )
| ~ cC40(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_35]) ).
fof(f_36_2,plain,
! [U_121] :
( ( cC40(U_121)
| ~ cC38(U_121)
| ~ cC34(U_121) )
& ( ( cC38(U_121)
& cC34(U_121) )
| ~ cC40(U_121) ) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_123] :
( cC40(U_123)
| ~ cC38(U_123)
| ~ cC34(U_123) )
& ! [U_122] :
( ( cC38(U_122)
& cC34(U_122) )
| ~ cC40(U_122) ) ),
inference(miniscope,[status(thm)],[f_36_2]) ).
cnf(f_36_4,plain,
( cC34(U_122)
| ~ cC40(U_122) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_5,plain,
( cC38(U_122)
| ~ cC40(U_122) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_6,plain,
( cC40(U_123)
| ~ cC38(U_123)
| ~ cC34(U_123) ),
inference(clausify,[status(thm)],[f_36_3]) ).
fof(f_37_1,plain,
! [X] :
( ( cC42(X)
| ~ cC4(X)
| ~ cC34(X) )
& ( ( cC4(X)
& cC34(X) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_36]) ).
fof(f_37_2,plain,
! [U_124] :
( ( cC42(U_124)
| ~ cC4(U_124)
| ~ cC34(U_124) )
& ( ( cC4(U_124)
& cC34(U_124) )
| ~ cC42(U_124) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_126] :
( cC42(U_126)
| ~ cC4(U_126)
| ~ cC34(U_126) )
& ! [U_125] :
( ( cC4(U_125)
& cC34(U_125) )
| ~ cC42(U_125) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
cnf(f_37_4,plain,
( cC34(U_125)
| ~ cC42(U_125) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_5,plain,
( cC4(U_125)
| ~ cC42(U_125) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_6,plain,
( cC42(U_126)
| ~ cC4(U_126)
| ~ cC34(U_126) ),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_38_1,plain,
! [X] :
( ( cC44(X)
| ! [Y] :
( ~ cC42(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC42(Y)
& rR1(X,Y) )
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_37]) ).
fof(f_38_2,plain,
! [U_129] :
( ( cC44(U_129)
| ! [U_128] :
( ~ cC42(U_128)
| ~ rR1(U_129,U_128) ) )
& ( ? [U_127] :
( cC42(U_127)
& rR1(U_129,U_127) )
| ~ cC44(U_129) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_131] :
( cC44(U_131)
| ! [U_128] :
( ~ cC42(U_128)
| ~ rR1(U_131,U_128) ) )
& ! [U_130] :
( ? [U_127] :
( cC42(U_127)
& rR1(U_130,U_127) )
| ~ cC44(U_130) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
fof(f_38_4,plain,
( ! [U_131] :
( cC44(U_131)
| ! [U_128] :
( ~ cC42(U_128)
| ~ rR1(U_131,U_128) ) )
& ! [U_130] :
( ( cC42(sK9(U_130))
& rR1(U_130,sK9(U_130)) )
| ~ cC44(U_130) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_127,sK9(U_130))],[f_38_3]) ).
cnf(f_38_5,plain,
( rR1(U_130,sK9(U_130))
| ~ cC44(U_130) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_6,plain,
( cC42(sK9(U_130))
| ~ cC44(U_130) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_7,plain,
( cC44(U_131)
| ~ cC42(U_128)
| ~ rR1(U_131,U_128) ),
inference(clausify,[status(thm)],[f_38_4]) ).
fof(f_39_1,plain,
! [X] :
( ( cC46(X)
| cC34(X)
| ~ cC44(X) )
& ( ( ~ cC34(X)
& cC44(X) )
| ~ cC46(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_38]) ).
fof(f_39_2,plain,
! [U_132] :
( ( cC46(U_132)
| cC34(U_132)
| ~ cC44(U_132) )
& ( ( ~ cC34(U_132)
& cC44(U_132) )
| ~ cC46(U_132) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_134] :
( cC46(U_134)
| cC34(U_134)
| ~ cC44(U_134) )
& ! [U_133] :
( ( ~ cC34(U_133)
& cC44(U_133) )
| ~ cC46(U_133) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( cC44(U_133)
| ~ cC46(U_133) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_5,plain,
( ~ cC34(U_133)
| ~ cC46(U_133) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_6,plain,
( cC46(U_134)
| cC34(U_134)
| ~ cC44(U_134) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [X] :
( ( cC48(X)
| cC46(X)
| cC40(X) )
& ( ( ~ cC46(X)
& ~ cC40(X) )
| ~ cC48(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_39]) ).
fof(f_40_2,plain,
! [U_135] :
( ( cC48(U_135)
| cC46(U_135)
| cC40(U_135) )
& ( ( ~ cC46(U_135)
& ~ cC40(U_135) )
| ~ cC48(U_135) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_137] :
( cC48(U_137)
| cC46(U_137)
| cC40(U_137) )
& ! [U_136] :
( ( ~ cC46(U_136)
& ~ cC40(U_136) )
| ~ cC48(U_136) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
cnf(f_40_4,plain,
( ~ cC40(U_136)
| ~ cC48(U_136) ),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_5,plain,
( ~ cC46(U_136)
| ~ cC48(U_136) ),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_6,plain,
( cC48(U_137)
| cC46(U_137)
| cC40(U_137) ),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,plain,
! [X] :
( ( cC50(X)
| cC48(X)
| ~ cC4(X) )
& ( ( ~ cC48(X)
& cC4(X) )
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_138] :
( ( cC50(U_138)
| cC48(U_138)
| ~ cC4(U_138) )
& ( ( ~ cC48(U_138)
& cC4(U_138) )
| ~ cC50(U_138) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_140] :
( cC50(U_140)
| cC48(U_140)
| ~ cC4(U_140) )
& ! [U_139] :
( ( ~ cC48(U_139)
& cC4(U_139) )
| ~ cC50(U_139) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
cnf(f_41_4,plain,
( cC4(U_139)
| ~ cC50(U_139) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_5,plain,
( ~ cC48(U_139)
| ~ cC50(U_139) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_6,plain,
( cC50(U_140)
| cC48(U_140)
| ~ cC4(U_140) ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_1,plain,
! [X] :
( ( cC52(X)
| cC32(X)
| cC50(X) )
& ( ( ~ cC32(X)
& ~ cC50(X) )
| ~ cC52(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_41]) ).
fof(f_42_2,plain,
! [U_141] :
( ( cC52(U_141)
| cC32(U_141)
| cC50(U_141) )
& ( ( ~ cC32(U_141)
& ~ cC50(U_141) )
| ~ cC52(U_141) ) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
( ! [U_143] :
( cC52(U_143)
| cC32(U_143)
| cC50(U_143) )
& ! [U_142] :
( ( ~ cC32(U_142)
& ~ cC50(U_142) )
| ~ cC52(U_142) ) ),
inference(miniscope,[status(thm)],[f_42_2]) ).
cnf(f_42_4,plain,
( ~ cC50(U_142)
| ~ cC52(U_142) ),
inference(clausify,[status(thm)],[f_42_3]) ).
cnf(f_42_5,plain,
( ~ cC32(U_142)
| ~ cC52(U_142) ),
inference(clausify,[status(thm)],[f_42_3]) ).
cnf(f_42_6,plain,
( cC52(U_143)
| cC32(U_143)
| cC50(U_143) ),
inference(clausify,[status(thm)],[f_42_3]) ).
fof(f_43_1,plain,
! [X] :
( ( cC54(X)
| ~ cC52(X)
| ~ cC14(X) )
& ( ( cC52(X)
& cC14(X) )
| ~ cC54(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_42]) ).
fof(f_43_2,plain,
! [U_144] :
( ( cC54(U_144)
| ~ cC52(U_144)
| ~ cC14(U_144) )
& ( ( cC52(U_144)
& cC14(U_144) )
| ~ cC54(U_144) ) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
( ! [U_146] :
( cC54(U_146)
| ~ cC52(U_146)
| ~ cC14(U_146) )
& ! [U_145] :
( ( cC52(U_145)
& cC14(U_145) )
| ~ cC54(U_145) ) ),
inference(miniscope,[status(thm)],[f_43_2]) ).
cnf(f_43_4,plain,
( cC14(U_145)
| ~ cC54(U_145) ),
inference(clausify,[status(thm)],[f_43_3]) ).
cnf(f_43_5,plain,
( cC52(U_145)
| ~ cC54(U_145) ),
inference(clausify,[status(thm)],[f_43_3]) ).
cnf(f_43_6,plain,
( cC54(U_146)
| ~ cC52(U_146)
| ~ cC14(U_146) ),
inference(clausify,[status(thm)],[f_43_3]) ).
fof(f_44_1,plain,
! [X] :
( ( cC56(X)
| cC10(X)
| ~ cC4(X) )
& ( ( ~ cC10(X)
& cC4(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_147] :
( ( cC56(U_147)
| cC10(U_147)
| ~ cC4(U_147) )
& ( ( ~ cC10(U_147)
& cC4(U_147) )
| ~ cC56(U_147) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_149] :
( cC56(U_149)
| cC10(U_149)
| ~ cC4(U_149) )
& ! [U_148] :
( ( ~ cC10(U_148)
& cC4(U_148) )
| ~ cC56(U_148) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
cnf(f_44_4,plain,
( cC4(U_148)
| ~ cC56(U_148) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_5,plain,
( ~ cC10(U_148)
| ~ cC56(U_148) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_6,plain,
( cC56(U_149)
| cC10(U_149)
| ~ cC4(U_149) ),
inference(clausify,[status(thm)],[f_44_3]) ).
fof(f_45_1,plain,
! [X] :
( ( cC58(X)
| ~ cC56(X)
| ~ cC34(X) )
& ( ( cC56(X)
& cC34(X) )
| ~ cC58(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_44]) ).
fof(f_45_2,plain,
! [U_150] :
( ( cC58(U_150)
| ~ cC56(U_150)
| ~ cC34(U_150) )
& ( ( cC56(U_150)
& cC34(U_150) )
| ~ cC58(U_150) ) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
( ! [U_152] :
( cC58(U_152)
| ~ cC56(U_152)
| ~ cC34(U_152) )
& ! [U_151] :
( ( cC56(U_151)
& cC34(U_151) )
| ~ cC58(U_151) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
cnf(f_45_4,plain,
( cC34(U_151)
| ~ cC58(U_151) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_5,plain,
( cC56(U_151)
| ~ cC58(U_151) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_6,plain,
( cC58(U_152)
| ~ cC56(U_152)
| ~ cC34(U_152) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [X] :
( ( cC6(X)
| cC4(X)
| ~ cC2(X) )
& ( ( ~ cC4(X)
& cC2(X) )
| ~ cC6(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_45]) ).
fof(f_46_2,plain,
! [U_153] :
( ( cC6(U_153)
| cC4(U_153)
| ~ cC2(U_153) )
& ( ( ~ cC4(U_153)
& cC2(U_153) )
| ~ cC6(U_153) ) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_155] :
( cC6(U_155)
| cC4(U_155)
| ~ cC2(U_155) )
& ! [U_154] :
( ( ~ cC4(U_154)
& cC2(U_154) )
| ~ cC6(U_154) ) ),
inference(miniscope,[status(thm)],[f_46_2]) ).
cnf(f_46_4,plain,
( cC2(U_154)
| ~ cC6(U_154) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_5,plain,
( ~ cC4(U_154)
| ~ cC6(U_154) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_6,plain,
( cC6(U_155)
| cC4(U_155)
| ~ cC2(U_155) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [X] :
( ( cC60(X)
| ! [Y] :
( ~ cC58(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC58(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_46]) ).
fof(f_47_2,plain,
! [U_158] :
( ( cC60(U_158)
| ! [U_157] :
( ~ cC58(U_157)
| ~ rR1(U_158,U_157) ) )
& ( ? [U_156] :
( cC58(U_156)
& rR1(U_158,U_156) )
| ~ cC60(U_158) ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_160] :
( cC60(U_160)
| ! [U_157] :
( ~ cC58(U_157)
| ~ rR1(U_160,U_157) ) )
& ! [U_159] :
( ? [U_156] :
( cC58(U_156)
& rR1(U_159,U_156) )
| ~ cC60(U_159) ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
fof(f_47_4,plain,
( ! [U_160] :
( cC60(U_160)
| ! [U_157] :
( ~ cC58(U_157)
| ~ rR1(U_160,U_157) ) )
& ! [U_159] :
( ( cC58(sK10(U_159))
& rR1(U_159,sK10(U_159)) )
| ~ cC60(U_159) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_156,sK10(U_159))],[f_47_3]) ).
cnf(f_47_5,plain,
( rR1(U_159,sK10(U_159))
| ~ cC60(U_159) ),
inference(clausify,[status(thm)],[f_47_4]) ).
cnf(f_47_6,plain,
( cC58(sK10(U_159))
| ~ cC60(U_159) ),
inference(clausify,[status(thm)],[f_47_4]) ).
cnf(f_47_7,plain,
( cC60(U_160)
| ~ cC58(U_157)
| ~ rR1(U_160,U_157) ),
inference(clausify,[status(thm)],[f_47_4]) ).
fof(f_48_1,plain,
! [X] :
( ( cC62(X)
| cC10(X)
| ~ cC4(X) )
& ( ( ~ cC10(X)
& cC4(X) )
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_47]) ).
fof(f_48_2,plain,
! [U_161] :
( ( cC62(U_161)
| cC10(U_161)
| ~ cC4(U_161) )
& ( ( ~ cC10(U_161)
& cC4(U_161) )
| ~ cC62(U_161) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_163] :
( cC62(U_163)
| cC10(U_163)
| ~ cC4(U_163) )
& ! [U_162] :
( ( ~ cC10(U_162)
& cC4(U_162) )
| ~ cC62(U_162) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( cC4(U_162)
| ~ cC62(U_162) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_5,plain,
( ~ cC10(U_162)
| ~ cC62(U_162) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_6,plain,
( cC62(U_163)
| cC10(U_163)
| ~ cC4(U_163) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [X] :
( ( cC64(X)
| cC34(X)
| ~ cC62(X) )
& ( ( ~ cC34(X)
& cC62(X) )
| ~ cC64(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_48]) ).
fof(f_49_2,plain,
! [U_164] :
( ( cC64(U_164)
| cC34(U_164)
| ~ cC62(U_164) )
& ( ( ~ cC34(U_164)
& cC62(U_164) )
| ~ cC64(U_164) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_166] :
( cC64(U_166)
| cC34(U_166)
| ~ cC62(U_166) )
& ! [U_165] :
( ( ~ cC34(U_165)
& cC62(U_165) )
| ~ cC64(U_165) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
cnf(f_49_4,plain,
( cC62(U_165)
| ~ cC64(U_165) ),
inference(clausify,[status(thm)],[f_49_3]) ).
cnf(f_49_5,plain,
( ~ cC34(U_165)
| ~ cC64(U_165) ),
inference(clausify,[status(thm)],[f_49_3]) ).
cnf(f_49_6,plain,
( cC64(U_166)
| cC34(U_166)
| ~ cC62(U_166) ),
inference(clausify,[status(thm)],[f_49_3]) ).
fof(f_50_1,plain,
! [X] :
( ( cC66(X)
| ! [Y] :
( ~ cC64(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC64(Y)
& rR1(X,Y) )
| ~ cC66(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_49]) ).
fof(f_50_2,plain,
! [U_169] :
( ( cC66(U_169)
| ! [U_168] :
( ~ cC64(U_168)
| ~ rR1(U_169,U_168) ) )
& ( ? [U_167] :
( cC64(U_167)
& rR1(U_169,U_167) )
| ~ cC66(U_169) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_171] :
( cC66(U_171)
| ! [U_168] :
( ~ cC64(U_168)
| ~ rR1(U_171,U_168) ) )
& ! [U_170] :
( ? [U_167] :
( cC64(U_167)
& rR1(U_170,U_167) )
| ~ cC66(U_170) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
fof(f_50_4,plain,
( ! [U_171] :
( cC66(U_171)
| ! [U_168] :
( ~ cC64(U_168)
| ~ rR1(U_171,U_168) ) )
& ! [U_170] :
( ( cC64(sK11(U_170))
& rR1(U_170,sK11(U_170)) )
| ~ cC66(U_170) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_167,sK11(U_170))],[f_50_3]) ).
cnf(f_50_5,plain,
( rR1(U_170,sK11(U_170))
| ~ cC66(U_170) ),
inference(clausify,[status(thm)],[f_50_4]) ).
cnf(f_50_6,plain,
( cC64(sK11(U_170))
| ~ cC66(U_170) ),
inference(clausify,[status(thm)],[f_50_4]) ).
cnf(f_50_7,plain,
( cC66(U_171)
| ~ cC64(U_168)
| ~ rR1(U_171,U_168) ),
inference(clausify,[status(thm)],[f_50_4]) ).
fof(f_51_1,plain,
! [X] :
( ( cC68(X)
| ~ cC66(X)
| ~ cC60(X) )
& ( ( cC66(X)
& cC60(X) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_50]) ).
fof(f_51_2,plain,
! [U_172] :
( ( cC68(U_172)
| ~ cC66(U_172)
| ~ cC60(U_172) )
& ( ( cC66(U_172)
& cC60(U_172) )
| ~ cC68(U_172) ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_174] :
( cC68(U_174)
| ~ cC66(U_174)
| ~ cC60(U_174) )
& ! [U_173] :
( ( cC66(U_173)
& cC60(U_173) )
| ~ cC68(U_173) ) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
cnf(f_51_4,plain,
( cC60(U_173)
| ~ cC68(U_173) ),
inference(clausify,[status(thm)],[f_51_3]) ).
cnf(f_51_5,plain,
( cC66(U_173)
| ~ cC68(U_173) ),
inference(clausify,[status(thm)],[f_51_3]) ).
cnf(f_51_6,plain,
( cC68(U_174)
| ~ cC66(U_174)
| ~ cC60(U_174) ),
inference(clausify,[status(thm)],[f_51_3]) ).
fof(f_52_1,plain,
! [X] :
( ( cC70(X)
| ~ cC2(X)
| cC4(X) )
& ( ( cC2(X)
& ~ cC4(X) )
| ~ cC70(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_51]) ).
fof(f_52_2,plain,
! [U_175] :
( ( cC70(U_175)
| ~ cC2(U_175)
| cC4(U_175) )
& ( ( cC2(U_175)
& ~ cC4(U_175) )
| ~ cC70(U_175) ) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_177] :
( cC70(U_177)
| ~ cC2(U_177)
| cC4(U_177) )
& ! [U_176] :
( ( cC2(U_176)
& ~ cC4(U_176) )
| ~ cC70(U_176) ) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
cnf(f_52_4,plain,
( ~ cC4(U_176)
| ~ cC70(U_176) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_5,plain,
( cC2(U_176)
| ~ cC70(U_176) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_6,plain,
( cC70(U_177)
| ~ cC2(U_177)
| cC4(U_177) ),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_1,plain,
! [X] :
( ( cC72(X)
| ~ cC70(X)
| cC68(X) )
& ( ( cC70(X)
& ~ cC68(X) )
| ~ cC72(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_52]) ).
fof(f_53_2,plain,
! [U_178] :
( ( cC72(U_178)
| ~ cC70(U_178)
| cC68(U_178) )
& ( ( cC70(U_178)
& ~ cC68(U_178) )
| ~ cC72(U_178) ) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_180] :
( cC72(U_180)
| ~ cC70(U_180)
| cC68(U_180) )
& ! [U_179] :
( ( cC70(U_179)
& ~ cC68(U_179) )
| ~ cC72(U_179) ) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
cnf(f_53_4,plain,
( ~ cC68(U_179)
| ~ cC72(U_179) ),
inference(clausify,[status(thm)],[f_53_3]) ).
cnf(f_53_5,plain,
( cC70(U_179)
| ~ cC72(U_179) ),
inference(clausify,[status(thm)],[f_53_3]) ).
cnf(f_53_6,plain,
( cC72(U_180)
| ~ cC70(U_180)
| cC68(U_180) ),
inference(clausify,[status(thm)],[f_53_3]) ).
fof(f_54_1,plain,
! [X] :
( ( cC74(X)
| cC72(X)
| ~ cC54(X) )
& ( ( ~ cC72(X)
& cC54(X) )
| ~ cC74(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_53]) ).
fof(f_54_2,plain,
! [U_181] :
( ( cC74(U_181)
| cC72(U_181)
| ~ cC54(U_181) )
& ( ( ~ cC72(U_181)
& cC54(U_181) )
| ~ cC74(U_181) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_183] :
( cC74(U_183)
| cC72(U_183)
| ~ cC54(U_183) )
& ! [U_182] :
( ( ~ cC72(U_182)
& cC54(U_182) )
| ~ cC74(U_182) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( cC54(U_182)
| ~ cC74(U_182) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( ~ cC72(U_182)
| ~ cC74(U_182) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_6,plain,
( cC74(U_183)
| cC72(U_183)
| ~ cC54(U_183) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [X] :
( ( cC76(X)
| ~ cC4(X)
| cC2(X) )
& ( ( cC4(X)
& ~ cC2(X) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_54]) ).
fof(f_55_2,plain,
! [U_184] :
( ( cC76(U_184)
| ~ cC4(U_184)
| cC2(U_184) )
& ( ( cC4(U_184)
& ~ cC2(U_184) )
| ~ cC76(U_184) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_186] :
( cC76(U_186)
| ~ cC4(U_186)
| cC2(U_186) )
& ! [U_185] :
( ( cC4(U_185)
& ~ cC2(U_185) )
| ~ cC76(U_185) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
cnf(f_55_4,plain,
( ~ cC2(U_185)
| ~ cC76(U_185) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_5,plain,
( cC4(U_185)
| ~ cC76(U_185) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_6,plain,
( cC76(U_186)
| ~ cC4(U_186)
| cC2(U_186) ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_56_1,plain,
! [X] :
( ( cC78(X)
| ~ cC10(X)
| cC4(X) )
& ( ( cC10(X)
& ~ cC4(X) )
| ~ cC78(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_55]) ).
fof(f_56_2,plain,
! [U_187] :
( ( cC78(U_187)
| ~ cC10(U_187)
| cC4(U_187) )
& ( ( cC10(U_187)
& ~ cC4(U_187) )
| ~ cC78(U_187) ) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
( ! [U_189] :
( cC78(U_189)
| ~ cC10(U_189)
| cC4(U_189) )
& ! [U_188] :
( ( cC10(U_188)
& ~ cC4(U_188) )
| ~ cC78(U_188) ) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
cnf(f_56_4,plain,
( ~ cC4(U_188)
| ~ cC78(U_188) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_5,plain,
( cC10(U_188)
| ~ cC78(U_188) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_6,plain,
( cC78(U_189)
| ~ cC10(U_189)
| cC4(U_189) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
! [X] :
( ( cC8(X)
| cC2(X)
| ~ cC4(X) )
& ( ( ~ cC2(X)
& cC4(X) )
| ~ cC8(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_56]) ).
fof(f_57_2,plain,
! [U_190] :
( ( cC8(U_190)
| cC2(U_190)
| ~ cC4(U_190) )
& ( ( ~ cC2(U_190)
& cC4(U_190) )
| ~ cC8(U_190) ) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
( ! [U_192] :
( cC8(U_192)
| cC2(U_192)
| ~ cC4(U_192) )
& ! [U_191] :
( ( ~ cC2(U_191)
& cC4(U_191) )
| ~ cC8(U_191) ) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( cC4(U_191)
| ~ cC8(U_191) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( ~ cC2(U_191)
| ~ cC8(U_191) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_6,plain,
( cC8(U_192)
| cC2(U_192)
| ~ cC4(U_192) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [X] :
( ( cC80(X)
| cC76(X)
| cC78(X) )
& ( ( ~ cC76(X)
& ~ cC78(X) )
| ~ cC80(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_57]) ).
fof(f_58_2,plain,
! [U_193] :
( ( cC80(U_193)
| cC76(U_193)
| cC78(U_193) )
& ( ( ~ cC76(U_193)
& ~ cC78(U_193) )
| ~ cC80(U_193) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_195] :
( cC80(U_195)
| cC76(U_195)
| cC78(U_195) )
& ! [U_194] :
( ( ~ cC76(U_194)
& ~ cC78(U_194) )
| ~ cC80(U_194) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_4,plain,
( ~ cC78(U_194)
| ~ cC80(U_194) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( ~ cC76(U_194)
| ~ cC80(U_194) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_6,plain,
( cC80(U_195)
| cC76(U_195)
| cC78(U_195) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_1,plain,
! [X] :
( ( cC82(X)
| ~ cC2(X)
| cC16(X) )
& ( ( cC2(X)
& ~ cC16(X) )
| ~ cC82(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_58]) ).
fof(f_59_2,plain,
! [U_196] :
( ( cC82(U_196)
| ~ cC2(U_196)
| cC16(U_196) )
& ( ( cC2(U_196)
& ~ cC16(U_196) )
| ~ cC82(U_196) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_198] :
( cC82(U_198)
| ~ cC2(U_198)
| cC16(U_198) )
& ! [U_197] :
( ( cC2(U_197)
& ~ cC16(U_197) )
| ~ cC82(U_197) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
cnf(f_59_4,plain,
( ~ cC16(U_197)
| ~ cC82(U_197) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_5,plain,
( cC2(U_197)
| ~ cC82(U_197) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_6,plain,
( cC82(U_198)
| ~ cC2(U_198)
| cC16(U_198) ),
inference(clausify,[status(thm)],[f_59_3]) ).
fof(f_60_1,plain,
! [X] :
( ( cC84(X)
| ! [Y] :
( ~ cC82(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC82(Y)
& rR1(X,Y) )
| ~ cC84(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_59]) ).
fof(f_60_2,plain,
! [U_201] :
( ( cC84(U_201)
| ! [U_200] :
( ~ cC82(U_200)
| ~ rR1(U_201,U_200) ) )
& ( ? [U_199] :
( cC82(U_199)
& rR1(U_201,U_199) )
| ~ cC84(U_201) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_203] :
( cC84(U_203)
| ! [U_200] :
( ~ cC82(U_200)
| ~ rR1(U_203,U_200) ) )
& ! [U_202] :
( ? [U_199] :
( cC82(U_199)
& rR1(U_202,U_199) )
| ~ cC84(U_202) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
fof(f_60_4,plain,
( ! [U_203] :
( cC84(U_203)
| ! [U_200] :
( ~ cC82(U_200)
| ~ rR1(U_203,U_200) ) )
& ! [U_202] :
( ( cC82(sK12(U_202))
& rR1(U_202,sK12(U_202)) )
| ~ cC84(U_202) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_199,sK12(U_202))],[f_60_3]) ).
cnf(f_60_5,plain,
( rR1(U_202,sK12(U_202))
| ~ cC84(U_202) ),
inference(clausify,[status(thm)],[f_60_4]) ).
cnf(f_60_6,plain,
( cC82(sK12(U_202))
| ~ cC84(U_202) ),
inference(clausify,[status(thm)],[f_60_4]) ).
cnf(f_60_7,plain,
( cC84(U_203)
| ~ cC82(U_200)
| ~ rR1(U_203,U_200) ),
inference(clausify,[status(thm)],[f_60_4]) ).
fof(f_61_1,plain,
! [X] :
( ( cC86(X)
| ~ cC84(X)
| ~ cC16(X) )
& ( ( cC84(X)
& cC16(X) )
| ~ cC86(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_60]) ).
fof(f_61_2,plain,
! [U_204] :
( ( cC86(U_204)
| ~ cC84(U_204)
| ~ cC16(U_204) )
& ( ( cC84(U_204)
& cC16(U_204) )
| ~ cC86(U_204) ) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
( ! [U_206] :
( cC86(U_206)
| ~ cC84(U_206)
| ~ cC16(U_206) )
& ! [U_205] :
( ( cC84(U_205)
& cC16(U_205) )
| ~ cC86(U_205) ) ),
inference(miniscope,[status(thm)],[f_61_2]) ).
cnf(f_61_4,plain,
( cC16(U_205)
| ~ cC86(U_205) ),
inference(clausify,[status(thm)],[f_61_3]) ).
cnf(f_61_5,plain,
( cC84(U_205)
| ~ cC86(U_205) ),
inference(clausify,[status(thm)],[f_61_3]) ).
cnf(f_61_6,plain,
( cC86(U_206)
| ~ cC84(U_206)
| ~ cC16(U_206) ),
inference(clausify,[status(thm)],[f_61_3]) ).
fof(f_62_1,plain,
! [X] :
( ( cC88(X)
| ~ cC2(X)
| ~ cC16(X) )
& ( ( cC2(X)
& cC16(X) )
| ~ cC88(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_61]) ).
fof(f_62_2,plain,
! [U_207] :
( ( cC88(U_207)
| ~ cC2(U_207)
| ~ cC16(U_207) )
& ( ( cC2(U_207)
& cC16(U_207) )
| ~ cC88(U_207) ) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
fof(f_62_3,plain,
( ! [U_209] :
( cC88(U_209)
| ~ cC2(U_209)
| ~ cC16(U_209) )
& ! [U_208] :
( ( cC2(U_208)
& cC16(U_208) )
| ~ cC88(U_208) ) ),
inference(miniscope,[status(thm)],[f_62_2]) ).
cnf(f_62_4,plain,
( cC16(U_208)
| ~ cC88(U_208) ),
inference(clausify,[status(thm)],[f_62_3]) ).
cnf(f_62_5,plain,
( cC2(U_208)
| ~ cC88(U_208) ),
inference(clausify,[status(thm)],[f_62_3]) ).
cnf(f_62_6,plain,
( cC88(U_209)
| ~ cC2(U_209)
| ~ cC16(U_209) ),
inference(clausify,[status(thm)],[f_62_3]) ).
fof(f_63_1,plain,
! [X] :
( ( cC90(X)
| ! [Y] :
( ~ cC88(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC88(Y)
& rR1(X,Y) )
| ~ cC90(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_62]) ).
fof(f_63_2,plain,
! [U_212] :
( ( cC90(U_212)
| ! [U_211] :
( ~ cC88(U_211)
| ~ rR1(U_212,U_211) ) )
& ( ? [U_210] :
( cC88(U_210)
& rR1(U_212,U_210) )
| ~ cC90(U_212) ) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
fof(f_63_3,plain,
( ! [U_214] :
( cC90(U_214)
| ! [U_211] :
( ~ cC88(U_211)
| ~ rR1(U_214,U_211) ) )
& ! [U_213] :
( ? [U_210] :
( cC88(U_210)
& rR1(U_213,U_210) )
| ~ cC90(U_213) ) ),
inference(miniscope,[status(thm)],[f_63_2]) ).
fof(f_63_4,plain,
( ! [U_214] :
( cC90(U_214)
| ! [U_211] :
( ~ cC88(U_211)
| ~ rR1(U_214,U_211) ) )
& ! [U_213] :
( ( cC88(sK13(U_213))
& rR1(U_213,sK13(U_213)) )
| ~ cC90(U_213) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_210,sK13(U_213))],[f_63_3]) ).
cnf(f_63_5,plain,
( rR1(U_213,sK13(U_213))
| ~ cC90(U_213) ),
inference(clausify,[status(thm)],[f_63_4]) ).
cnf(f_63_6,plain,
( cC88(sK13(U_213))
| ~ cC90(U_213) ),
inference(clausify,[status(thm)],[f_63_4]) ).
cnf(f_63_7,plain,
( cC90(U_214)
| ~ cC88(U_211)
| ~ rR1(U_214,U_211) ),
inference(clausify,[status(thm)],[f_63_4]) ).
fof(f_64_1,plain,
! [X] :
( ( cC92(X)
| cC16(X)
| ~ cC90(X) )
& ( ( ~ cC16(X)
& cC90(X) )
| ~ cC92(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_63]) ).
fof(f_64_2,plain,
! [U_215] :
( ( cC92(U_215)
| cC16(U_215)
| ~ cC90(U_215) )
& ( ( ~ cC16(U_215)
& cC90(U_215) )
| ~ cC92(U_215) ) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
fof(f_64_3,plain,
( ! [U_217] :
( cC92(U_217)
| cC16(U_217)
| ~ cC90(U_217) )
& ! [U_216] :
( ( ~ cC16(U_216)
& cC90(U_216) )
| ~ cC92(U_216) ) ),
inference(miniscope,[status(thm)],[f_64_2]) ).
cnf(f_64_4,plain,
( cC90(U_216)
| ~ cC92(U_216) ),
inference(clausify,[status(thm)],[f_64_3]) ).
cnf(f_64_5,plain,
( ~ cC16(U_216)
| ~ cC92(U_216) ),
inference(clausify,[status(thm)],[f_64_3]) ).
cnf(f_64_6,plain,
( cC92(U_217)
| cC16(U_217)
| ~ cC90(U_217) ),
inference(clausify,[status(thm)],[f_64_3]) ).
fof(f_65_1,plain,
! [X] :
( ( cC94(X)
| cC92(X)
| cC86(X) )
& ( ( ~ cC92(X)
& ~ cC86(X) )
| ~ cC94(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
! [U_218] :
( ( cC94(U_218)
| cC92(U_218)
| cC86(U_218) )
& ( ( ~ cC92(U_218)
& ~ cC86(U_218) )
| ~ cC94(U_218) ) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
( ! [U_220] :
( cC94(U_220)
| cC92(U_220)
| cC86(U_220) )
& ! [U_219] :
( ( ~ cC92(U_219)
& ~ cC86(U_219) )
| ~ cC94(U_219) ) ),
inference(miniscope,[status(thm)],[f_65_2]) ).
cnf(f_65_4,plain,
( ~ cC86(U_219)
| ~ cC94(U_219) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_5,plain,
( ~ cC92(U_219)
| ~ cC94(U_219) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_6,plain,
( cC94(U_220)
| cC92(U_220)
| cC86(U_220) ),
inference(clausify,[status(thm)],[f_65_3]) ).
fof(f_66_1,plain,
! [X] :
( ( cC96(X)
| ~ cC2(X)
| cC94(X) )
& ( ( cC2(X)
& ~ cC94(X) )
| ~ cC96(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_221] :
( ( cC96(U_221)
| ~ cC2(U_221)
| cC94(U_221) )
& ( ( cC2(U_221)
& ~ cC94(U_221) )
| ~ cC96(U_221) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_223] :
( cC96(U_223)
| ~ cC2(U_223)
| cC94(U_223) )
& ! [U_222] :
( ( cC2(U_222)
& ~ cC94(U_222) )
| ~ cC96(U_222) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( ~ cC94(U_222)
| ~ cC96(U_222) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( cC2(U_222)
| ~ cC96(U_222) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_6,plain,
( cC96(U_223)
| ~ cC2(U_223)
| cC94(U_223) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_1,plain,
! [X] :
( ( cC98(X)
| cC34(X)
| ~ cC4(X) )
& ( ( ~ cC34(X)
& cC4(X) )
| ~ cC98(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_66]) ).
fof(f_67_2,plain,
! [U_224] :
( ( cC98(U_224)
| cC34(U_224)
| ~ cC4(U_224) )
& ( ( ~ cC34(U_224)
& cC4(U_224) )
| ~ cC98(U_224) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_226] :
( cC98(U_226)
| cC34(U_226)
| ~ cC4(U_226) )
& ! [U_225] :
( ( ~ cC34(U_225)
& cC4(U_225) )
| ~ cC98(U_225) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
cnf(f_67_4,plain,
( cC4(U_225)
| ~ cC98(U_225) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_5,plain,
( ~ cC34(U_225)
| ~ cC98(U_225) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_6,plain,
( cC98(U_226)
| cC34(U_226)
| ~ cC4(U_226) ),
inference(clausify,[status(thm)],[f_67_3]) ).
fof(f_68_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC6(X)
| ~ cC140(X) )
& ( ( cC6(X)
& cC140(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_67]) ).
fof(f_68_2,plain,
! [U_227] :
( ( cTEST(U_227)
| ~ cC6(U_227)
| ~ cC140(U_227) )
& ( ( cC6(U_227)
& cC140(U_227) )
| ~ cTEST(U_227) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_229] :
( cTEST(U_229)
| ~ cC6(U_229)
| ~ cC140(U_229) )
& ! [U_228] :
( ( cC6(U_228)
& cC140(U_228) )
| ~ cTEST(U_228) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( cC140(U_228)
| ~ cTEST(U_228) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( cC6(U_228)
| ~ cTEST(U_228) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_6,plain,
( cTEST(U_229)
| ~ cC6(U_229)
| ~ cC140(U_229) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
~ cC84(iV822576),
inference(fof_nnf,[status(thm)],[axiom_68]) ).
cnf(f_69_2,plain,
~ cC84(iV822576),
inference(clausify,[status(thm)],[f_69_1]) ).
fof(f_70_1,plain,
~ cC132(iV822576),
inference(fof_nnf,[status(thm)],[axiom_69]) ).
cnf(f_70_2,plain,
~ cC132(iV822576),
inference(clausify,[status(thm)],[f_70_1]) ).
fof(f_71_1,plain,
~ cC102(iV822576),
inference(fof_nnf,[status(thm)],[axiom_70]) ).
cnf(f_71_2,plain,
~ cC102(iV822576),
inference(clausify,[status(thm)],[f_71_1]) ).
fof(f_72_1,plain,
~ cC134(iV822576),
inference(fof_nnf,[status(thm)],[axiom_71]) ).
cnf(f_72_2,plain,
~ cC134(iV822576),
inference(clausify,[status(thm)],[f_72_1]) ).
fof(f_73_1,plain,
cC16(iV822576),
inference(fof_nnf,[status(thm)],[axiom_72]) ).
cnf(f_73_2,plain,
cC16(iV822576),
inference(clausify,[status(thm)],[f_73_1]) ).
fof(f_74_1,plain,
! [X] :
( ~ cC88(X)
| ~ rR1(iV822576,X) ),
inference(fof_nnf,[status(thm)],[axiom_73]) ).
fof(f_74_2,plain,
! [U_230] :
( ~ cC88(U_230)
| ~ rR1(iV822576,U_230) ),
inference(variable_rename,[status(thm)],[f_74_1]) ).
cnf(f_74_3,plain,
( ~ cC88(U_230)
| ~ rR1(iV822576,U_230) ),
inference(clausify,[status(thm)],[f_74_2]) ).
fof(f_75_1,plain,
cC34(iV822576),
inference(fof_nnf,[status(thm)],[axiom_74]) ).
cnf(f_75_2,plain,
cC34(iV822576),
inference(clausify,[status(thm)],[f_75_1]) ).
fof(f_76_1,plain,
cC4(iV822576),
inference(fof_nnf,[status(thm)],[axiom_75]) ).
cnf(f_76_2,plain,
cC4(iV822576),
inference(clausify,[status(thm)],[f_76_1]) ).
fof(f_77_1,plain,
~ cC96(iV822576),
inference(fof_nnf,[status(thm)],[axiom_76]) ).
cnf(f_77_2,plain,
~ cC96(iV822576),
inference(clausify,[status(thm)],[f_77_1]) ).
fof(f_78_1,plain,
~ cC86(iV822576),
inference(fof_nnf,[status(thm)],[axiom_77]) ).
cnf(f_78_2,plain,
~ cC86(iV822576),
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
~ cC92(iV822576),
inference(fof_nnf,[status(thm)],[axiom_78]) ).
cnf(f_79_2,plain,
~ cC92(iV822576),
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
~ cC108(iV822576),
inference(fof_nnf,[status(thm)],[axiom_79]) ).
cnf(f_80_2,plain,
~ cC108(iV822576),
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_81_1,plain,
cowlThing(iV822576),
inference(fof_nnf,[status(thm)],[axiom_80]) ).
cnf(f_81_2,plain,
cowlThing(iV822576),
inference(clausify,[status(thm)],[f_81_1]) ).
fof(f_82_1,plain,
! [X] :
( ~ cC98(X)
| ~ rR1(iV822576,X) ),
inference(fof_nnf,[status(thm)],[axiom_81]) ).
fof(f_82_2,plain,
! [U_231] :
( ~ cC98(U_231)
| ~ rR1(iV822576,U_231) ),
inference(variable_rename,[status(thm)],[f_82_1]) ).
cnf(f_82_3,plain,
( ~ cC98(U_231)
| ~ rR1(iV822576,U_231) ),
inference(clausify,[status(thm)],[f_82_2]) ).
fof(f_83_1,plain,
~ cC90(iV822576),
inference(fof_nnf,[status(thm)],[axiom_82]) ).
cnf(f_83_2,plain,
~ cC90(iV822576),
inference(clausify,[status(thm)],[f_83_1]) ).
fof(f_84_1,plain,
~ cC100(iV822576),
inference(fof_nnf,[status(thm)],[axiom_83]) ).
cnf(f_84_2,plain,
~ cC100(iV822576),
inference(clausify,[status(thm)],[f_84_1]) ).
fof(f_85_1,plain,
~ cC10(iV822576),
inference(fof_nnf,[status(thm)],[axiom_84]) ).
cnf(f_85_2,plain,
~ cC10(iV822576),
inference(clausify,[status(thm)],[f_85_1]) ).
fof(f_86_1,plain,
~ cC18(iV822576),
inference(fof_nnf,[status(thm)],[axiom_85]) ).
cnf(f_86_2,plain,
~ cC18(iV822576),
inference(clausify,[status(thm)],[f_86_1]) ).
fof(f_87_1,plain,
~ cC76(iV822576),
inference(fof_nnf,[status(thm)],[axiom_86]) ).
cnf(f_87_2,plain,
~ cC76(iV822576),
inference(clausify,[status(thm)],[f_87_1]) ).
fof(f_88_1,plain,
~ cC112(iV822576),
inference(fof_nnf,[status(thm)],[axiom_87]) ).
cnf(f_88_2,plain,
~ cC112(iV822576),
inference(clausify,[status(thm)],[f_88_1]) ).
fof(f_89_1,plain,
~ cC78(iV822576),
inference(fof_nnf,[status(thm)],[axiom_88]) ).
cnf(f_89_2,plain,
~ cC78(iV822576),
inference(clausify,[status(thm)],[f_89_1]) ).
fof(f_90_1,plain,
cC2(iV822576),
inference(fof_nnf,[status(thm)],[axiom_89]) ).
cnf(f_90_2,plain,
cC2(iV822576),
inference(clausify,[status(thm)],[f_90_1]) ).
fof(f_91_1,plain,
! [X] :
( ~ cC82(X)
| ~ rR1(iV822576,X) ),
inference(fof_nnf,[status(thm)],[axiom_90]) ).
fof(f_91_2,plain,
! [U_232] :
( ~ cC82(U_232)
| ~ rR1(iV822576,U_232) ),
inference(variable_rename,[status(thm)],[f_91_1]) ).
cnf(f_91_3,plain,
( ~ cC82(U_232)
| ~ rR1(iV822576,U_232) ),
inference(clausify,[status(thm)],[f_91_2]) ).
fof(f_92_1,negated_conjecture,
~ ( cC80(iV822576)
& cC136(iV822576)
& cC114(iV822576)
& cC110(iV822576)
& cC56(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_92_2,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_92_1]) ).
fof(f_92_3,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [U_234] :
( ( ~ xsd_string(U_234)
& ~ xsd_integer(U_234) )
| ( xsd_integer(U_234)
& xsd_string(U_234) ) )
| ? [U_233] :
( cowlNothing(U_233)
| ~ cowlThing(U_233) ) ),
inference(variable_rename,[status(thm)],[f_92_2]) ).
fof(f_92_4,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [U_238] :
( ~ xsd_string(U_238)
& ~ xsd_integer(U_238) )
| ? [U_237] :
( xsd_integer(U_237)
& xsd_string(U_237) )
| ? [U_236] : cowlNothing(U_236)
| ? [U_235] : ~ cowlThing(U_235) ),
inference(miniscope,[status(thm)],[f_92_3]) ).
fof(f_92_5,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [U_238] :
( ~ xsd_string(U_238)
& ~ xsd_integer(U_238) )
| ? [U_237] :
( xsd_integer(U_237)
& xsd_string(U_237) )
| ? [U_236] : cowlNothing(U_236)
| ~ cowlThing(sK14) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_235,sK14)],[f_92_4]) ).
fof(f_92_6,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [U_238] :
( ~ xsd_string(U_238)
& ~ xsd_integer(U_238) )
| ? [U_237] :
( xsd_integer(U_237)
& xsd_string(U_237) )
| cowlNothing(sK15)
| ~ cowlThing(sK14) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_236,sK15)],[f_92_5]) ).
fof(f_92_7,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [U_238] :
( ~ xsd_string(U_238)
& ~ xsd_integer(U_238) )
| ( xsd_integer(sK16)
& xsd_string(sK16) )
| cowlNothing(sK15)
| ~ cowlThing(sK14) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_237,sK16)],[f_92_6]) ).
fof(f_92_8,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ( ~ xsd_string(sK17)
& ~ xsd_integer(sK17) )
| ( xsd_integer(sK16)
& xsd_string(sK16) )
| cowlNothing(sK15)
| ~ cowlThing(sK14) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_238,sK17)],[f_92_7]) ).
fof(f_92_9,negated_conjecture,
( ( ~ xsd_string(sK17)
| ~ sP1 )
& ( ~ xsd_integer(sK17)
| ~ sP1 )
& ( xsd_integer(sK16)
| ~ sP0 )
& ( xsd_string(sK16)
| ~ sP0 )
& ( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| sP1
| sP0
| cowlNothing(sK15)
| ~ cowlThing(sK14) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_92_8]) ).
cnf(f_92_10,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| sP1
| sP0
| cowlNothing(sK15)
| ~ cowlThing(sK14) ),
inference(clausify,[status(thm)],[f_92_9]) ).
cnf(f_92_11,negated_conjecture,
( xsd_string(sK16)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_92_9]) ).
cnf(f_92_12,negated_conjecture,
( xsd_integer(sK16)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_92_9]) ).
cnf(f_92_13,negated_conjecture,
( ~ xsd_integer(sK17)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_92_9]) ).
cnf(f_92_14,negated_conjecture,
( ~ xsd_string(sK17)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_92_9]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS146+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 : n026.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.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 12:18:51 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.44 % SZS status Theorem for theBenchmark
% 0.09/0.44 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------