%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS149+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 : n015.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.97s 1.29s
% Output : Proof 1.06s
% 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)
<=> ? [Y] :
( ~ cC98(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X] :
( cC102(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_5,axiom,
! [X] :
( cC104(X)
<=> ( cC16(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)
<=> ( ~ cC16(X)
& ~ cC106(X) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_8,axiom,
! [X] :
( cC110(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_8) ).
fof(axiom_9,axiom,
! [X] :
( cC112(X)
<=> ( cC16(X)
& cC110(X) ) ),
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)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_11) ).
fof(axiom_12,axiom,
! [X] :
( cC118(X)
<=> ? [Y] :
( cC116(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)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X] :
( cC124(X)
<=> ( cC16(X)
& cC122(X) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_17,axiom,
! [X] :
( cC126(X)
<=> ? [Y] :
( cC124(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_18,axiom,
! [X] :
( cC128(X)
<=> ( ~ cC126(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_19,axiom,
! [X] :
( cC130(X)
<=> ? [Y] :
( cC128(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_19) ).
fof(axiom_20,axiom,
! [X] :
( cC132(X)
<=> ( cC120(X)
& ~ cC130(X) ) ),
file('theBenchmark.p',axiom_20) ).
fof(axiom_21,axiom,
! [X] :
( cC134(X)
<=> ( ~ cC108(X)
& ~ cC132(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cC136(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_23,axiom,
! [X] :
( cC138(X)
<=> ( cC16(X)
& cC136(X) ) ),
file('theBenchmark.p',axiom_23) ).
fof(axiom_24,axiom,
! [X] :
( cC14(X)
<=> ( ~ cC2(X)
& ~ cC12(X) ) ),
file('theBenchmark.p',axiom_24) ).
fof(axiom_25,axiom,
! [X] :
( cC140(X)
<=> ? [Y] :
( cC138(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_26,axiom,
! [X] :
( cC142(X)
<=> ( ~ cC16(X)
& ~ cC140(X) ) ),
file('theBenchmark.p',axiom_26) ).
fof(axiom_27,axiom,
! [X] :
( cC144(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_28,axiom,
! [X] :
( cC146(X)
<=> ( cC16(X)
& cC144(X) ) ),
file('theBenchmark.p',axiom_28) ).
fof(axiom_29,axiom,
! [X] :
( cC148(X)
<=> ? [Y] :
( cC146(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC150(X)
<=> ( ~ cC148(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_31,axiom,
! [X] :
( cC152(X)
<=> ? [Y] :
( cC150(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_31) ).
fof(axiom_32,axiom,
! [X] :
( cC154(X)
<=> ? [Y] :
( cC152(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_33,axiom,
! [X] :
( cC156(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_34,axiom,
! [X] :
( cC158(X)
<=> ( cC16(X)
& cC156(X) ) ),
file('theBenchmark.p',axiom_34) ).
fof(axiom_35,axiom,
! [X] :
( cC160(X)
<=> ? [Y] :
( cC158(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_35) ).
fof(axiom_36,axiom,
! [X] :
( cC162(X)
<=> ( ~ cC160(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_36) ).
fof(axiom_37,axiom,
! [X] :
( cC164(X)
<=> ? [Y] :
( cC162(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_37) ).
fof(axiom_38,axiom,
! [X] :
( cC166(X)
<=> ( ~ cC164(X)
& cC154(X) ) ),
file('theBenchmark.p',axiom_38) ).
fof(axiom_39,axiom,
! [X] :
( cC168(X)
<=> ( ~ cC142(X)
& ~ cC166(X) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC170(X)
<=> ? [Y] :
( ~ cC168(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC172(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_42,axiom,
! [X] :
( cC174(X)
<=> ( cC16(X)
& cC172(X) ) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_43,axiom,
! [X] :
( cC176(X)
<=> ? [Y] :
( cC174(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_44,axiom,
! [X] :
( cC178(X)
<=> ( ~ cC176(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_45,axiom,
! [X] :
( cC18(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_45) ).
fof(axiom_46,axiom,
! [X] :
( cC180(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_46) ).
fof(axiom_47,axiom,
! [X] :
( cC182(X)
<=> ( cC180(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_47) ).
fof(axiom_48,axiom,
! [X] :
( cC184(X)
<=> ? [Y] :
( cC182(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_48) ).
fof(axiom_49,axiom,
! [X] :
( cC186(X)
<=> ( ~ cC184(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_49) ).
fof(axiom_50,axiom,
! [X] :
( cC188(X)
<=> ? [Y] :
( cC186(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_51,axiom,
! [X] :
( cC190(X)
<=> ? [Y] :
( cC188(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_51) ).
fof(axiom_52,axiom,
! [X] :
( cC192(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_53,axiom,
! [X] :
( cC194(X)
<=> ( cC16(X)
& cC192(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_54,axiom,
! [X] :
( cC196(X)
<=> ? [Y] :
( cC194(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_54) ).
fof(axiom_55,axiom,
! [X] :
( cC198(X)
<=> ( ~ cC16(X)
& ~ cC196(X) ) ),
file('theBenchmark.p',axiom_55) ).
fof(axiom_56,axiom,
! [X] :
( cC20(X)
<=> ( cC16(X)
& cC18(X) ) ),
file('theBenchmark.p',axiom_56) ).
fof(axiom_57,axiom,
! [X] :
( cC200(X)
<=> ? [Y] :
( cC198(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_58,axiom,
! [X] :
( cC202(X)
<=> ( ~ cC200(X)
& cC190(X) ) ),
file('theBenchmark.p',axiom_58) ).
fof(axiom_59,axiom,
! [X] :
( cC204(X)
<=> ( ~ cC202(X)
& ~ cC178(X) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_60,axiom,
! [X] :
( cC206(X)
<=> ( cC204(X)
& cC170(X) ) ),
file('theBenchmark.p',axiom_60) ).
fof(axiom_61,axiom,
! [X] :
( cC208(X)
<=> ? [Y] :
( cC206(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_61) ).
fof(axiom_62,axiom,
! [X] :
( cC210(X)
<=> ( ~ cC134(X)
& ~ cC208(X) ) ),
file('theBenchmark.p',axiom_62) ).
fof(axiom_63,axiom,
! [X] :
( cC212(X)
<=> ? [Y] :
( cC210(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_63) ).
fof(axiom_64,axiom,
! [X] :
( cC214(X)
<=> ( ~ cC212(X)
& cC100(X) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC216(X)
<=> ( cC64(X)
& ~ cC214(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC22(X)
<=> ? [Y] :
( cC20(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cC24(X)
<=> ( ~ cC16(X)
& ~ cC22(X) ) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_68,axiom,
! [X] :
( cC26(X)
<=> ? [Y] :
( cC24(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_68) ).
fof(axiom_69,axiom,
! [X] :
( cC28(X)
<=> ( ~ cC16(X)
& ~ cC26(X) ) ),
file('theBenchmark.p',axiom_69) ).
fof(axiom_70,axiom,
! [X] :
( cC30(X)
<=> ( cC28(X)
& cC14(X) ) ),
file('theBenchmark.p',axiom_70) ).
fof(axiom_71,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( ~ cC32(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_71) ).
fof(axiom_72,axiom,
! [X] :
( cC36(X)
<=> ( cC34(X)
& cC32(X) ) ),
file('theBenchmark.p',axiom_72) ).
fof(axiom_73,axiom,
! [X] :
( cC38(X)
<=> ? [Y] :
( cC36(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_73) ).
fof(axiom_74,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_74) ).
fof(axiom_75,axiom,
! [X] :
( cC40(X)
<=> ( ~ cC32(X)
& ~ cC38(X) ) ),
file('theBenchmark.p',axiom_75) ).
fof(axiom_76,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( cC40(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_76) ).
fof(axiom_77,axiom,
! [X] :
( cC44(X)
<=> ( ~ cC42(X)
& ~ cC32(X) ) ),
file('theBenchmark.p',axiom_77) ).
fof(axiom_78,axiom,
! [X] :
( cC46(X)
<=> ( cC44(X)
& cC30(X) ) ),
file('theBenchmark.p',axiom_78) ).
fof(axiom_79,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_79) ).
fof(axiom_80,axiom,
! [X] :
( cC50(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_80) ).
fof(axiom_81,axiom,
! [X] :
( cC52(X)
<=> ( cC16(X)
& cC50(X) ) ),
file('theBenchmark.p',axiom_81) ).
fof(axiom_82,axiom,
! [X] :
( cC54(X)
<=> ? [Y] :
( cC52(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_82) ).
fof(axiom_83,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_83) ).
fof(axiom_84,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( cC56(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_84) ).
fof(axiom_85,axiom,
! [X] :
( cC6(X)
<=> ( cC4(X)
& cC2(X) ) ),
file('theBenchmark.p',axiom_85) ).
fof(axiom_86,axiom,
! [X] :
( cC60(X)
<=> ( ~ cC58(X)
& cC48(X) ) ),
file('theBenchmark.p',axiom_86) ).
fof(axiom_87,axiom,
! [X] :
( cC62(X)
<=> ? [Y] :
( cC60(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_87) ).
fof(axiom_88,axiom,
! [X] :
( cC64(X)
<=> ( cTOP(X)
& ~ cC62(X) ) ),
file('theBenchmark.p',axiom_88) ).
fof(axiom_89,axiom,
! [X] :
( cC66(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_89) ).
fof(axiom_90,axiom,
! [X] :
( cC68(X)
<=> ( cC16(X)
& cC66(X) ) ),
file('theBenchmark.p',axiom_90) ).
fof(axiom_91,axiom,
! [X] :
( cC70(X)
<=> ? [Y] :
( cC68(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_91) ).
fof(axiom_92,axiom,
! [X] :
( cC72(X)
<=> ( ~ cC16(X)
& ~ cC70(X) ) ),
file('theBenchmark.p',axiom_92) ).
fof(axiom_93,axiom,
! [X] :
( cC74(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_93) ).
fof(axiom_94,axiom,
! [X] :
( cC76(X)
<=> ( cC16(X)
& cC74(X) ) ),
file('theBenchmark.p',axiom_94) ).
fof(axiom_95,axiom,
! [X] :
( cC78(X)
<=> ? [Y] :
( cC76(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_95) ).
fof(axiom_96,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_96) ).
fof(axiom_97,axiom,
! [X] :
( cC80(X)
<=> ( ~ cC78(X)
& ~ cC16(X) ) ),
file('theBenchmark.p',axiom_97) ).
fof(axiom_98,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( cC80(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_98) ).
fof(axiom_99,axiom,
! [X] :
( cC84(X)
<=> ? [Y] :
( cC82(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_99) ).
fof(axiom_100,axiom,
! [X] :
( cC86(X)
<=> ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_100) ).
fof(axiom_101,axiom,
! [X] :
( cC88(X)
<=> ( cC16(X)
& cC86(X) ) ),
file('theBenchmark.p',axiom_101) ).
fof(axiom_102,axiom,
! [X] :
( cC90(X)
<=> ? [Y] :
( cC88(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_102) ).
fof(axiom_103,axiom,
! [X] :
( cC92(X)
<=> ( ~ cC16(X)
& ~ cC90(X) ) ),
file('theBenchmark.p',axiom_103) ).
fof(axiom_104,axiom,
! [X] :
( cC94(X)
<=> ? [Y] :
( cC92(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_104) ).
fof(axiom_105,axiom,
! [X] :
( cC96(X)
<=> ( ~ cC94(X)
& cC84(X) ) ),
file('theBenchmark.p',axiom_105) ).
fof(axiom_106,axiom,
! [X] :
( cC98(X)
<=> ( ~ cC96(X)
& ~ cC72(X) ) ),
file('theBenchmark.p',axiom_106) ).
fof(axiom_107,axiom,
! [X] :
( cTEST(X)
<=> ( cC46(X)
& cC216(X) ) ),
file('theBenchmark.p',axiom_107) ).
fof(axiom_108,axiom,
cTEST(iV3102),
file('theBenchmark.p',axiom_108) ).
fof(axiom_109,axiom,
cowlThing(iV3102),
file('theBenchmark.p',axiom_109) ).
fof(axiom_110,axiom,
! [X] :
( rR1(iV3102,X)
=> ~ cC60(X) ),
file('theBenchmark.p',axiom_110) ).
fof(axiom_111,axiom,
! [X] :
( rR1(iV3102,X)
=> ~ cC10(X) ),
file('theBenchmark.p',axiom_111) ).
fof(axiom_112,axiom,
cTOP(iV3102),
file('theBenchmark.p',axiom_112) ).
fof(axiom_113,axiom,
! [X] :
( rR1(iV3102,X)
=> ~ cC24(X) ),
file('theBenchmark.p',axiom_113) ).
fof(axiom_114,axiom,
~ cC42(iV3102),
file('theBenchmark.p',axiom_114) ).
fof(axiom_115,axiom,
~ cC12(iV3102),
file('theBenchmark.p',axiom_115) ).
fof(axiom_116,axiom,
~ cC26(iV3102),
file('theBenchmark.p',axiom_116) ).
fof(axiom_117,axiom,
! [X] :
( rR1(iV3102,X)
=> cC98(X) ),
file('theBenchmark.p',axiom_117) ).
fof(axiom_118,axiom,
~ cC214(iV3102),
file('theBenchmark.p',axiom_118) ).
fof(axiom_119,axiom,
~ cC62(iV3102),
file('theBenchmark.p',axiom_119) ).
fof(axiom_120,axiom,
! [X] :
( rR1(iV3102,X)
=> ~ cC40(X) ),
file('theBenchmark.p',axiom_120) ).
fof(axiom_121,axiom,
~ cC16(iV3102),
file('theBenchmark.p',axiom_121) ).
fof(axiom_122,axiom,
~ cC2(iV3102),
file('theBenchmark.p',axiom_122) ).
fof(axiom_123,axiom,
~ cC32(iV3102),
file('theBenchmark.p',axiom_123) ).
fof(axiom_124,axiom,
~ cC100(iV3102),
file('theBenchmark.p',axiom_124) ).
fof(the_axiom,conjecture,
( cowlThing(iV3102)
& cC14(iV3102)
& cC64(iV3102)
& cC28(iV3102)
& cC44(iV3102)
& cC30(iV3102)
& cC46(iV3102)
& cC216(iV3102)
& ! [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)
| ! [Y] :
( cC98(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC98(Y)
& rR1(X,Y) )
| ~ cC100(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(f_4_2,plain,
! [U_11] :
( ( cC100(U_11)
| ! [U_10] :
( cC98(U_10)
| ~ rR1(U_11,U_10) ) )
& ( ? [U_9] :
( ~ cC98(U_9)
& rR1(U_11,U_9) )
| ~ cC100(U_11) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_13] :
( cC100(U_13)
| ! [U_10] :
( cC98(U_10)
| ~ rR1(U_13,U_10) ) )
& ! [U_12] :
( ? [U_9] :
( ~ cC98(U_9)
& rR1(U_12,U_9) )
| ~ cC100(U_12) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
( ! [U_13] :
( cC100(U_13)
| ! [U_10] :
( cC98(U_10)
| ~ rR1(U_13,U_10) ) )
& ! [U_12] :
( ( ~ cC98(sK1(U_12))
& rR1(U_12,sK1(U_12)) )
| ~ cC100(U_12) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_9,sK1(U_12))],[f_4_3]) ).
cnf(f_4_5,plain,
( rR1(U_12,sK1(U_12))
| ~ cC100(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_6,plain,
( ~ cC98(sK1(U_12))
| ~ cC100(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_7,plain,
( cC100(U_13)
| cC98(U_10)
| ~ rR1(U_13,U_10) ),
inference(clausify,[status(thm)],[f_4_4]) ).
fof(f_5_1,plain,
! [X] :
( ( cC102(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC102(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_4]) ).
fof(f_5_2,plain,
! [U_16] :
( ( cC102(U_16)
| ! [U_15] :
( cC16(U_15)
| ~ rR1(U_16,U_15) ) )
& ( ? [U_14] :
( ~ cC16(U_14)
& rR1(U_16,U_14) )
| ~ cC102(U_16) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_18] :
( cC102(U_18)
| ! [U_15] :
( cC16(U_15)
| ~ rR1(U_18,U_15) ) )
& ! [U_17] :
( ? [U_14] :
( ~ cC16(U_14)
& rR1(U_17,U_14) )
| ~ cC102(U_17) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_18] :
( cC102(U_18)
| ! [U_15] :
( cC16(U_15)
| ~ rR1(U_18,U_15) ) )
& ! [U_17] :
( ( ~ cC16(sK2(U_17))
& rR1(U_17,sK2(U_17)) )
| ~ cC102(U_17) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_14,sK2(U_17))],[f_5_3]) ).
cnf(f_5_5,plain,
( rR1(U_17,sK2(U_17))
| ~ cC102(U_17) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_6,plain,
( ~ cC16(sK2(U_17))
| ~ cC102(U_17) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_7,plain,
( cC102(U_18)
| cC16(U_15)
| ~ rR1(U_18,U_15) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_6_1,plain,
! [X] :
( ( cC104(X)
| ~ cC16(X)
| ~ cC102(X) )
& ( ( cC16(X)
& cC102(X) )
| ~ cC104(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_5]) ).
fof(f_6_2,plain,
! [U_19] :
( ( cC104(U_19)
| ~ cC16(U_19)
| ~ cC102(U_19) )
& ( ( cC16(U_19)
& cC102(U_19) )
| ~ cC104(U_19) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_21] :
( cC104(U_21)
| ~ cC16(U_21)
| ~ cC102(U_21) )
& ! [U_20] :
( ( cC16(U_20)
& cC102(U_20) )
| ~ cC104(U_20) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
cnf(f_6_4,plain,
( cC102(U_20)
| ~ cC104(U_20) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( cC16(U_20)
| ~ cC104(U_20) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_6,plain,
( cC104(U_21)
| ~ cC16(U_21)
| ~ cC102(U_21) ),
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_24] :
( ( cC106(U_24)
| ! [U_23] :
( ~ cC104(U_23)
| ~ rR1(U_24,U_23) ) )
& ( ? [U_22] :
( cC104(U_22)
& rR1(U_24,U_22) )
| ~ cC106(U_24) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_26] :
( cC106(U_26)
| ! [U_23] :
( ~ cC104(U_23)
| ~ rR1(U_26,U_23) ) )
& ! [U_25] :
( ? [U_22] :
( cC104(U_22)
& rR1(U_25,U_22) )
| ~ cC106(U_25) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_26] :
( cC106(U_26)
| ! [U_23] :
( ~ cC104(U_23)
| ~ rR1(U_26,U_23) ) )
& ! [U_25] :
( ( cC104(sK3(U_25))
& rR1(U_25,sK3(U_25)) )
| ~ cC106(U_25) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_22,sK3(U_25))],[f_7_3]) ).
cnf(f_7_5,plain,
( rR1(U_25,sK3(U_25))
| ~ cC106(U_25) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_6,plain,
( cC104(sK3(U_25))
| ~ cC106(U_25) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_7,plain,
( cC106(U_26)
| ~ cC104(U_23)
| ~ rR1(U_26,U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
fof(f_8_1,plain,
! [X] :
( ( cC108(X)
| cC16(X)
| cC106(X) )
& ( ( ~ cC16(X)
& ~ cC106(X) )
| ~ cC108(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_7]) ).
fof(f_8_2,plain,
! [U_27] :
( ( cC108(U_27)
| cC16(U_27)
| cC106(U_27) )
& ( ( ~ cC16(U_27)
& ~ cC106(U_27) )
| ~ cC108(U_27) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_29] :
( cC108(U_29)
| cC16(U_29)
| cC106(U_29) )
& ! [U_28] :
( ( ~ cC16(U_28)
& ~ cC106(U_28) )
| ~ cC108(U_28) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( ~ cC106(U_28)
| ~ cC108(U_28) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( ~ cC16(U_28)
| ~ cC108(U_28) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( cC108(U_29)
| cC16(U_29)
| cC106(U_29) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X] :
( ( cC110(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC110(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_8]) ).
fof(f_9_2,plain,
! [U_32] :
( ( cC110(U_32)
| ! [U_31] :
( cC16(U_31)
| ~ rR1(U_32,U_31) ) )
& ( ? [U_30] :
( ~ cC16(U_30)
& rR1(U_32,U_30) )
| ~ cC110(U_32) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_34] :
( cC110(U_34)
| ! [U_31] :
( cC16(U_31)
| ~ rR1(U_34,U_31) ) )
& ! [U_33] :
( ? [U_30] :
( ~ cC16(U_30)
& rR1(U_33,U_30) )
| ~ cC110(U_33) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
fof(f_9_4,plain,
( ! [U_34] :
( cC110(U_34)
| ! [U_31] :
( cC16(U_31)
| ~ rR1(U_34,U_31) ) )
& ! [U_33] :
( ( ~ cC16(sK4(U_33))
& rR1(U_33,sK4(U_33)) )
| ~ cC110(U_33) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_30,sK4(U_33))],[f_9_3]) ).
cnf(f_9_5,plain,
( rR1(U_33,sK4(U_33))
| ~ cC110(U_33) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_6,plain,
( ~ cC16(sK4(U_33))
| ~ cC110(U_33) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_7,plain,
( cC110(U_34)
| cC16(U_31)
| ~ rR1(U_34,U_31) ),
inference(clausify,[status(thm)],[f_9_4]) ).
fof(f_10_1,plain,
! [X] :
( ( cC112(X)
| ~ cC16(X)
| ~ cC110(X) )
& ( ( cC16(X)
& cC110(X) )
| ~ cC112(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_9]) ).
fof(f_10_2,plain,
! [U_35] :
( ( cC112(U_35)
| ~ cC16(U_35)
| ~ cC110(U_35) )
& ( ( cC16(U_35)
& cC110(U_35) )
| ~ cC112(U_35) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_37] :
( cC112(U_37)
| ~ cC16(U_37)
| ~ cC110(U_37) )
& ! [U_36] :
( ( cC16(U_36)
& cC110(U_36) )
| ~ cC112(U_36) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
cnf(f_10_4,plain,
( cC110(U_36)
| ~ cC112(U_36) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_5,plain,
( cC16(U_36)
| ~ cC112(U_36) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_6,plain,
( cC112(U_37)
| ~ cC16(U_37)
| ~ cC110(U_37) ),
inference(clausify,[status(thm)],[f_10_3]) ).
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_40] :
( ( cC114(U_40)
| ! [U_39] :
( ~ cC112(U_39)
| ~ rR1(U_40,U_39) ) )
& ( ? [U_38] :
( cC112(U_38)
& rR1(U_40,U_38) )
| ~ cC114(U_40) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_42] :
( cC114(U_42)
| ! [U_39] :
( ~ cC112(U_39)
| ~ rR1(U_42,U_39) ) )
& ! [U_41] :
( ? [U_38] :
( cC112(U_38)
& rR1(U_41,U_38) )
| ~ cC114(U_41) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_42] :
( cC114(U_42)
| ! [U_39] :
( ~ cC112(U_39)
| ~ rR1(U_42,U_39) ) )
& ! [U_41] :
( ( cC112(sK5(U_41))
& rR1(U_41,sK5(U_41)) )
| ~ cC114(U_41) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_38,sK5(U_41))],[f_11_3]) ).
cnf(f_11_5,plain,
( rR1(U_41,sK5(U_41))
| ~ cC114(U_41) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( cC112(sK5(U_41))
| ~ cC114(U_41) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( cC114(U_42)
| ~ cC112(U_39)
| ~ rR1(U_42,U_39) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_12_1,plain,
! [X] :
( ( cC116(X)
| cC114(X)
| cC16(X) )
& ( ( ~ cC114(X)
& ~ cC16(X) )
| ~ cC116(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_11]) ).
fof(f_12_2,plain,
! [U_43] :
( ( cC116(U_43)
| cC114(U_43)
| cC16(U_43) )
& ( ( ~ cC114(U_43)
& ~ cC16(U_43) )
| ~ cC116(U_43) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_45] :
( cC116(U_45)
| cC114(U_45)
| cC16(U_45) )
& ! [U_44] :
( ( ~ cC114(U_44)
& ~ cC16(U_44) )
| ~ cC116(U_44) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( ~ cC16(U_44)
| ~ cC116(U_44) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_5,plain,
( ~ cC114(U_44)
| ~ cC116(U_44) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_6,plain,
( cC116(U_45)
| cC114(U_45)
| cC16(U_45) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [X] :
( ( cC118(X)
| ! [Y] :
( ~ cC116(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC116(Y)
& rR1(X,Y) )
| ~ cC118(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_12]) ).
fof(f_13_2,plain,
! [U_48] :
( ( cC118(U_48)
| ! [U_47] :
( ~ cC116(U_47)
| ~ rR1(U_48,U_47) ) )
& ( ? [U_46] :
( cC116(U_46)
& rR1(U_48,U_46) )
| ~ cC118(U_48) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_50] :
( cC118(U_50)
| ! [U_47] :
( ~ cC116(U_47)
| ~ rR1(U_50,U_47) ) )
& ! [U_49] :
( ? [U_46] :
( cC116(U_46)
& rR1(U_49,U_46) )
| ~ cC118(U_49) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_50] :
( cC118(U_50)
| ! [U_47] :
( ~ cC116(U_47)
| ~ rR1(U_50,U_47) ) )
& ! [U_49] :
( ( cC116(sK6(U_49))
& rR1(U_49,sK6(U_49)) )
| ~ cC118(U_49) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_46,sK6(U_49))],[f_13_3]) ).
cnf(f_13_5,plain,
( rR1(U_49,sK6(U_49))
| ~ cC118(U_49) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_6,plain,
( cC116(sK6(U_49))
| ~ cC118(U_49) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_7,plain,
( cC118(U_50)
| ~ cC116(U_47)
| ~ rR1(U_50,U_47) ),
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_53] :
( ( cC12(U_53)
| ! [U_52] :
( ~ cC10(U_52)
| ~ rR1(U_53,U_52) ) )
& ( ? [U_51] :
( cC10(U_51)
& rR1(U_53,U_51) )
| ~ cC12(U_53) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_55] :
( cC12(U_55)
| ! [U_52] :
( ~ cC10(U_52)
| ~ rR1(U_55,U_52) ) )
& ! [U_54] :
( ? [U_51] :
( cC10(U_51)
& rR1(U_54,U_51) )
| ~ cC12(U_54) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_55] :
( cC12(U_55)
| ! [U_52] :
( ~ cC10(U_52)
| ~ rR1(U_55,U_52) ) )
& ! [U_54] :
( ( cC10(sK7(U_54))
& rR1(U_54,sK7(U_54)) )
| ~ cC12(U_54) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_51,sK7(U_54))],[f_14_3]) ).
cnf(f_14_5,plain,
( rR1(U_54,sK7(U_54))
| ~ cC12(U_54) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_6,plain,
( cC10(sK7(U_54))
| ~ cC12(U_54) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_7,plain,
( cC12(U_55)
| ~ cC10(U_52)
| ~ rR1(U_55,U_52) ),
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_58] :
( ( cC120(U_58)
| ! [U_57] :
( ~ cC118(U_57)
| ~ rR1(U_58,U_57) ) )
& ( ? [U_56] :
( cC118(U_56)
& rR1(U_58,U_56) )
| ~ cC120(U_58) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_60] :
( cC120(U_60)
| ! [U_57] :
( ~ cC118(U_57)
| ~ rR1(U_60,U_57) ) )
& ! [U_59] :
( ? [U_56] :
( cC118(U_56)
& rR1(U_59,U_56) )
| ~ cC120(U_59) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_60] :
( cC120(U_60)
| ! [U_57] :
( ~ cC118(U_57)
| ~ rR1(U_60,U_57) ) )
& ! [U_59] :
( ( cC118(sK8(U_59))
& rR1(U_59,sK8(U_59)) )
| ~ cC120(U_59) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_56,sK8(U_59))],[f_15_3]) ).
cnf(f_15_5,plain,
( rR1(U_59,sK8(U_59))
| ~ cC120(U_59) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_6,plain,
( cC118(sK8(U_59))
| ~ cC120(U_59) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_7,plain,
( cC120(U_60)
| ~ cC118(U_57)
| ~ rR1(U_60,U_57) ),
inference(clausify,[status(thm)],[f_15_4]) ).
fof(f_16_1,plain,
! [X] :
( ( cC122(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC122(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_15]) ).
fof(f_16_2,plain,
! [U_63] :
( ( cC122(U_63)
| ! [U_62] :
( cC16(U_62)
| ~ rR1(U_63,U_62) ) )
& ( ? [U_61] :
( ~ cC16(U_61)
& rR1(U_63,U_61) )
| ~ cC122(U_63) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_65] :
( cC122(U_65)
| ! [U_62] :
( cC16(U_62)
| ~ rR1(U_65,U_62) ) )
& ! [U_64] :
( ? [U_61] :
( ~ cC16(U_61)
& rR1(U_64,U_61) )
| ~ cC122(U_64) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_65] :
( cC122(U_65)
| ! [U_62] :
( cC16(U_62)
| ~ rR1(U_65,U_62) ) )
& ! [U_64] :
( ( ~ cC16(sK9(U_64))
& rR1(U_64,sK9(U_64)) )
| ~ cC122(U_64) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_61,sK9(U_64))],[f_16_3]) ).
cnf(f_16_5,plain,
( rR1(U_64,sK9(U_64))
| ~ cC122(U_64) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_6,plain,
( ~ cC16(sK9(U_64))
| ~ cC122(U_64) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_7,plain,
( cC122(U_65)
| cC16(U_62)
| ~ rR1(U_65,U_62) ),
inference(clausify,[status(thm)],[f_16_4]) ).
fof(f_17_1,plain,
! [X] :
( ( cC124(X)
| ~ cC16(X)
| ~ cC122(X) )
& ( ( cC16(X)
& cC122(X) )
| ~ cC124(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(f_17_2,plain,
! [U_66] :
( ( cC124(U_66)
| ~ cC16(U_66)
| ~ cC122(U_66) )
& ( ( cC16(U_66)
& cC122(U_66) )
| ~ cC124(U_66) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_68] :
( cC124(U_68)
| ~ cC16(U_68)
| ~ cC122(U_68) )
& ! [U_67] :
( ( cC16(U_67)
& cC122(U_67) )
| ~ cC124(U_67) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( cC122(U_67)
| ~ cC124(U_67) ),
inference(clausify,[status(thm)],[f_17_3]) ).
cnf(f_17_5,plain,
( cC16(U_67)
| ~ cC124(U_67) ),
inference(clausify,[status(thm)],[f_17_3]) ).
cnf(f_17_6,plain,
( cC124(U_68)
| ~ cC16(U_68)
| ~ cC122(U_68) ),
inference(clausify,[status(thm)],[f_17_3]) ).
fof(f_18_1,plain,
! [X] :
( ( cC126(X)
| ! [Y] :
( ~ cC124(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC124(Y)
& rR1(X,Y) )
| ~ cC126(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_17]) ).
fof(f_18_2,plain,
! [U_71] :
( ( cC126(U_71)
| ! [U_70] :
( ~ cC124(U_70)
| ~ rR1(U_71,U_70) ) )
& ( ? [U_69] :
( cC124(U_69)
& rR1(U_71,U_69) )
| ~ cC126(U_71) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_73] :
( cC126(U_73)
| ! [U_70] :
( ~ cC124(U_70)
| ~ rR1(U_73,U_70) ) )
& ! [U_72] :
( ? [U_69] :
( cC124(U_69)
& rR1(U_72,U_69) )
| ~ cC126(U_72) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
( ! [U_73] :
( cC126(U_73)
| ! [U_70] :
( ~ cC124(U_70)
| ~ rR1(U_73,U_70) ) )
& ! [U_72] :
( ( cC124(sK10(U_72))
& rR1(U_72,sK10(U_72)) )
| ~ cC126(U_72) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_69,sK10(U_72))],[f_18_3]) ).
cnf(f_18_5,plain,
( rR1(U_72,sK10(U_72))
| ~ cC126(U_72) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_6,plain,
( cC124(sK10(U_72))
| ~ cC126(U_72) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_7,plain,
( cC126(U_73)
| ~ cC124(U_70)
| ~ rR1(U_73,U_70) ),
inference(clausify,[status(thm)],[f_18_4]) ).
fof(f_19_1,plain,
! [X] :
( ( cC128(X)
| cC126(X)
| cC16(X) )
& ( ( ~ cC126(X)
& ~ cC16(X) )
| ~ cC128(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_18]) ).
fof(f_19_2,plain,
! [U_74] :
( ( cC128(U_74)
| cC126(U_74)
| cC16(U_74) )
& ( ( ~ cC126(U_74)
& ~ cC16(U_74) )
| ~ cC128(U_74) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_76] :
( cC128(U_76)
| cC126(U_76)
| cC16(U_76) )
& ! [U_75] :
( ( ~ cC126(U_75)
& ~ cC16(U_75) )
| ~ cC128(U_75) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( ~ cC16(U_75)
| ~ cC128(U_75) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( ~ cC126(U_75)
| ~ cC128(U_75) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_6,plain,
( cC128(U_76)
| cC126(U_76)
| cC16(U_76) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [X] :
( ( cC130(X)
| ! [Y] :
( ~ cC128(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC128(Y)
& rR1(X,Y) )
| ~ cC130(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_19]) ).
fof(f_20_2,plain,
! [U_79] :
( ( cC130(U_79)
| ! [U_78] :
( ~ cC128(U_78)
| ~ rR1(U_79,U_78) ) )
& ( ? [U_77] :
( cC128(U_77)
& rR1(U_79,U_77) )
| ~ cC130(U_79) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_81] :
( cC130(U_81)
| ! [U_78] :
( ~ cC128(U_78)
| ~ rR1(U_81,U_78) ) )
& ! [U_80] :
( ? [U_77] :
( cC128(U_77)
& rR1(U_80,U_77) )
| ~ cC130(U_80) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
fof(f_20_4,plain,
( ! [U_81] :
( cC130(U_81)
| ! [U_78] :
( ~ cC128(U_78)
| ~ rR1(U_81,U_78) ) )
& ! [U_80] :
( ( cC128(sK11(U_80))
& rR1(U_80,sK11(U_80)) )
| ~ cC130(U_80) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_77,sK11(U_80))],[f_20_3]) ).
cnf(f_20_5,plain,
( rR1(U_80,sK11(U_80))
| ~ cC130(U_80) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_6,plain,
( cC128(sK11(U_80))
| ~ cC130(U_80) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_7,plain,
( cC130(U_81)
| ~ cC128(U_78)
| ~ rR1(U_81,U_78) ),
inference(clausify,[status(thm)],[f_20_4]) ).
fof(f_21_1,plain,
! [X] :
( ( cC132(X)
| ~ cC120(X)
| cC130(X) )
& ( ( cC120(X)
& ~ cC130(X) )
| ~ cC132(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_20]) ).
fof(f_21_2,plain,
! [U_82] :
( ( cC132(U_82)
| ~ cC120(U_82)
| cC130(U_82) )
& ( ( cC120(U_82)
& ~ cC130(U_82) )
| ~ cC132(U_82) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ! [U_84] :
( cC132(U_84)
| ~ cC120(U_84)
| cC130(U_84) )
& ! [U_83] :
( ( cC120(U_83)
& ~ cC130(U_83) )
| ~ cC132(U_83) ) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( ~ cC130(U_83)
| ~ cC132(U_83) ),
inference(clausify,[status(thm)],[f_21_3]) ).
cnf(f_21_5,plain,
( cC120(U_83)
| ~ cC132(U_83) ),
inference(clausify,[status(thm)],[f_21_3]) ).
cnf(f_21_6,plain,
( cC132(U_84)
| ~ cC120(U_84)
| cC130(U_84) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [X] :
( ( cC134(X)
| cC108(X)
| cC132(X) )
& ( ( ~ cC108(X)
& ~ cC132(X) )
| ~ cC134(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_21]) ).
fof(f_22_2,plain,
! [U_85] :
( ( cC134(U_85)
| cC108(U_85)
| cC132(U_85) )
& ( ( ~ cC108(U_85)
& ~ cC132(U_85) )
| ~ cC134(U_85) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_87] :
( cC134(U_87)
| cC108(U_87)
| cC132(U_87) )
& ! [U_86] :
( ( ~ cC108(U_86)
& ~ cC132(U_86) )
| ~ cC134(U_86) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( ~ cC132(U_86)
| ~ cC134(U_86) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( ~ cC108(U_86)
| ~ cC134(U_86) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_6,plain,
( cC134(U_87)
| cC108(U_87)
| cC132(U_87) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [X] :
( ( cC136(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC136(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_22]) ).
fof(f_23_2,plain,
! [U_90] :
( ( cC136(U_90)
| ! [U_89] :
( cC16(U_89)
| ~ rR1(U_90,U_89) ) )
& ( ? [U_88] :
( ~ cC16(U_88)
& rR1(U_90,U_88) )
| ~ cC136(U_90) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_92] :
( cC136(U_92)
| ! [U_89] :
( cC16(U_89)
| ~ rR1(U_92,U_89) ) )
& ! [U_91] :
( ? [U_88] :
( ~ cC16(U_88)
& rR1(U_91,U_88) )
| ~ cC136(U_91) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_92] :
( cC136(U_92)
| ! [U_89] :
( cC16(U_89)
| ~ rR1(U_92,U_89) ) )
& ! [U_91] :
( ( ~ cC16(sK12(U_91))
& rR1(U_91,sK12(U_91)) )
| ~ cC136(U_91) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_88,sK12(U_91))],[f_23_3]) ).
cnf(f_23_5,plain,
( rR1(U_91,sK12(U_91))
| ~ cC136(U_91) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( ~ cC16(sK12(U_91))
| ~ cC136(U_91) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( cC136(U_92)
| cC16(U_89)
| ~ rR1(U_92,U_89) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
! [X] :
( ( cC138(X)
| ~ cC16(X)
| ~ cC136(X) )
& ( ( cC16(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_23]) ).
fof(f_24_2,plain,
! [U_93] :
( ( cC138(U_93)
| ~ cC16(U_93)
| ~ cC136(U_93) )
& ( ( cC16(U_93)
& cC136(U_93) )
| ~ cC138(U_93) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_95] :
( cC138(U_95)
| ~ cC16(U_95)
| ~ cC136(U_95) )
& ! [U_94] :
( ( cC16(U_94)
& cC136(U_94) )
| ~ cC138(U_94) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
cnf(f_24_4,plain,
( cC136(U_94)
| ~ cC138(U_94) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_5,plain,
( cC16(U_94)
| ~ cC138(U_94) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_6,plain,
( cC138(U_95)
| ~ cC16(U_95)
| ~ cC136(U_95) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
! [X] :
( ( cC14(X)
| cC2(X)
| cC12(X) )
& ( ( ~ cC2(X)
& ~ cC12(X) )
| ~ cC14(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_24]) ).
fof(f_25_2,plain,
! [U_96] :
( ( cC14(U_96)
| cC2(U_96)
| cC12(U_96) )
& ( ( ~ cC2(U_96)
& ~ cC12(U_96) )
| ~ cC14(U_96) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_98] :
( cC14(U_98)
| cC2(U_98)
| cC12(U_98) )
& ! [U_97] :
( ( ~ cC2(U_97)
& ~ cC12(U_97) )
| ~ cC14(U_97) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( ~ cC12(U_97)
| ~ cC14(U_97) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( ~ cC2(U_97)
| ~ cC14(U_97) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_6,plain,
( cC14(U_98)
| cC2(U_98)
| cC12(U_98) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [X] :
( ( cC140(X)
| ! [Y] :
( ~ cC138(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC138(Y)
& rR1(X,Y) )
| ~ cC140(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_25]) ).
fof(f_26_2,plain,
! [U_101] :
( ( cC140(U_101)
| ! [U_100] :
( ~ cC138(U_100)
| ~ rR1(U_101,U_100) ) )
& ( ? [U_99] :
( cC138(U_99)
& rR1(U_101,U_99) )
| ~ cC140(U_101) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_103] :
( cC140(U_103)
| ! [U_100] :
( ~ cC138(U_100)
| ~ rR1(U_103,U_100) ) )
& ! [U_102] :
( ? [U_99] :
( cC138(U_99)
& rR1(U_102,U_99) )
| ~ cC140(U_102) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
fof(f_26_4,plain,
( ! [U_103] :
( cC140(U_103)
| ! [U_100] :
( ~ cC138(U_100)
| ~ rR1(U_103,U_100) ) )
& ! [U_102] :
( ( cC138(sK13(U_102))
& rR1(U_102,sK13(U_102)) )
| ~ cC140(U_102) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_99,sK13(U_102))],[f_26_3]) ).
cnf(f_26_5,plain,
( rR1(U_102,sK13(U_102))
| ~ cC140(U_102) ),
inference(clausify,[status(thm)],[f_26_4]) ).
cnf(f_26_6,plain,
( cC138(sK13(U_102))
| ~ cC140(U_102) ),
inference(clausify,[status(thm)],[f_26_4]) ).
cnf(f_26_7,plain,
( cC140(U_103)
| ~ cC138(U_100)
| ~ rR1(U_103,U_100) ),
inference(clausify,[status(thm)],[f_26_4]) ).
fof(f_27_1,plain,
! [X] :
( ( cC142(X)
| cC16(X)
| cC140(X) )
& ( ( ~ cC16(X)
& ~ cC140(X) )
| ~ cC142(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_26]) ).
fof(f_27_2,plain,
! [U_104] :
( ( cC142(U_104)
| cC16(U_104)
| cC140(U_104) )
& ( ( ~ cC16(U_104)
& ~ cC140(U_104) )
| ~ cC142(U_104) ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_106] :
( cC142(U_106)
| cC16(U_106)
| cC140(U_106) )
& ! [U_105] :
( ( ~ cC16(U_105)
& ~ cC140(U_105) )
| ~ cC142(U_105) ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
cnf(f_27_4,plain,
( ~ cC140(U_105)
| ~ cC142(U_105) ),
inference(clausify,[status(thm)],[f_27_3]) ).
cnf(f_27_5,plain,
( ~ cC16(U_105)
| ~ cC142(U_105) ),
inference(clausify,[status(thm)],[f_27_3]) ).
cnf(f_27_6,plain,
( cC142(U_106)
| cC16(U_106)
| cC140(U_106) ),
inference(clausify,[status(thm)],[f_27_3]) ).
fof(f_28_1,plain,
! [X] :
( ( cC144(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC144(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_27]) ).
fof(f_28_2,plain,
! [U_109] :
( ( cC144(U_109)
| ! [U_108] :
( cC16(U_108)
| ~ rR1(U_109,U_108) ) )
& ( ? [U_107] :
( ~ cC16(U_107)
& rR1(U_109,U_107) )
| ~ cC144(U_109) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_111] :
( cC144(U_111)
| ! [U_108] :
( cC16(U_108)
| ~ rR1(U_111,U_108) ) )
& ! [U_110] :
( ? [U_107] :
( ~ cC16(U_107)
& rR1(U_110,U_107) )
| ~ cC144(U_110) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
fof(f_28_4,plain,
( ! [U_111] :
( cC144(U_111)
| ! [U_108] :
( cC16(U_108)
| ~ rR1(U_111,U_108) ) )
& ! [U_110] :
( ( ~ cC16(sK14(U_110))
& rR1(U_110,sK14(U_110)) )
| ~ cC144(U_110) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_107,sK14(U_110))],[f_28_3]) ).
cnf(f_28_5,plain,
( rR1(U_110,sK14(U_110))
| ~ cC144(U_110) ),
inference(clausify,[status(thm)],[f_28_4]) ).
cnf(f_28_6,plain,
( ~ cC16(sK14(U_110))
| ~ cC144(U_110) ),
inference(clausify,[status(thm)],[f_28_4]) ).
cnf(f_28_7,plain,
( cC144(U_111)
| cC16(U_108)
| ~ rR1(U_111,U_108) ),
inference(clausify,[status(thm)],[f_28_4]) ).
fof(f_29_1,plain,
! [X] :
( ( cC146(X)
| ~ cC16(X)
| ~ cC144(X) )
& ( ( cC16(X)
& cC144(X) )
| ~ cC146(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_28]) ).
fof(f_29_2,plain,
! [U_112] :
( ( cC146(U_112)
| ~ cC16(U_112)
| ~ cC144(U_112) )
& ( ( cC16(U_112)
& cC144(U_112) )
| ~ cC146(U_112) ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_114] :
( cC146(U_114)
| ~ cC16(U_114)
| ~ cC144(U_114) )
& ! [U_113] :
( ( cC16(U_113)
& cC144(U_113) )
| ~ cC146(U_113) ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( cC144(U_113)
| ~ cC146(U_113) ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_5,plain,
( cC16(U_113)
| ~ cC146(U_113) ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_6,plain,
( cC146(U_114)
| ~ cC16(U_114)
| ~ cC144(U_114) ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_1,plain,
! [X] :
( ( cC148(X)
| ! [Y] :
( ~ cC146(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC146(Y)
& rR1(X,Y) )
| ~ cC148(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_29]) ).
fof(f_30_2,plain,
! [U_117] :
( ( cC148(U_117)
| ! [U_116] :
( ~ cC146(U_116)
| ~ rR1(U_117,U_116) ) )
& ( ? [U_115] :
( cC146(U_115)
& rR1(U_117,U_115) )
| ~ cC148(U_117) ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_119] :
( cC148(U_119)
| ! [U_116] :
( ~ cC146(U_116)
| ~ rR1(U_119,U_116) ) )
& ! [U_118] :
( ? [U_115] :
( cC146(U_115)
& rR1(U_118,U_115) )
| ~ cC148(U_118) ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
fof(f_30_4,plain,
( ! [U_119] :
( cC148(U_119)
| ! [U_116] :
( ~ cC146(U_116)
| ~ rR1(U_119,U_116) ) )
& ! [U_118] :
( ( cC146(sK15(U_118))
& rR1(U_118,sK15(U_118)) )
| ~ cC148(U_118) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_115,sK15(U_118))],[f_30_3]) ).
cnf(f_30_5,plain,
( rR1(U_118,sK15(U_118))
| ~ cC148(U_118) ),
inference(clausify,[status(thm)],[f_30_4]) ).
cnf(f_30_6,plain,
( cC146(sK15(U_118))
| ~ cC148(U_118) ),
inference(clausify,[status(thm)],[f_30_4]) ).
cnf(f_30_7,plain,
( cC148(U_119)
| ~ cC146(U_116)
| ~ rR1(U_119,U_116) ),
inference(clausify,[status(thm)],[f_30_4]) ).
fof(f_31_1,plain,
! [X] :
( ( cC150(X)
| cC148(X)
| cC16(X) )
& ( ( ~ cC148(X)
& ~ cC16(X) )
| ~ cC150(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_30]) ).
fof(f_31_2,plain,
! [U_120] :
( ( cC150(U_120)
| cC148(U_120)
| cC16(U_120) )
& ( ( ~ cC148(U_120)
& ~ cC16(U_120) )
| ~ cC150(U_120) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_122] :
( cC150(U_122)
| cC148(U_122)
| cC16(U_122) )
& ! [U_121] :
( ( ~ cC148(U_121)
& ~ cC16(U_121) )
| ~ cC150(U_121) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( ~ cC16(U_121)
| ~ cC150(U_121) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_5,plain,
( ~ cC148(U_121)
| ~ cC150(U_121) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_6,plain,
( cC150(U_122)
| cC148(U_122)
| cC16(U_122) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [X] :
( ( cC152(X)
| ! [Y] :
( ~ cC150(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC150(Y)
& rR1(X,Y) )
| ~ cC152(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_31]) ).
fof(f_32_2,plain,
! [U_125] :
( ( cC152(U_125)
| ! [U_124] :
( ~ cC150(U_124)
| ~ rR1(U_125,U_124) ) )
& ( ? [U_123] :
( cC150(U_123)
& rR1(U_125,U_123) )
| ~ cC152(U_125) ) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
( ! [U_127] :
( cC152(U_127)
| ! [U_124] :
( ~ cC150(U_124)
| ~ rR1(U_127,U_124) ) )
& ! [U_126] :
( ? [U_123] :
( cC150(U_123)
& rR1(U_126,U_123) )
| ~ cC152(U_126) ) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
fof(f_32_4,plain,
( ! [U_127] :
( cC152(U_127)
| ! [U_124] :
( ~ cC150(U_124)
| ~ rR1(U_127,U_124) ) )
& ! [U_126] :
( ( cC150(sK16(U_126))
& rR1(U_126,sK16(U_126)) )
| ~ cC152(U_126) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_123,sK16(U_126))],[f_32_3]) ).
cnf(f_32_5,plain,
( rR1(U_126,sK16(U_126))
| ~ cC152(U_126) ),
inference(clausify,[status(thm)],[f_32_4]) ).
cnf(f_32_6,plain,
( cC150(sK16(U_126))
| ~ cC152(U_126) ),
inference(clausify,[status(thm)],[f_32_4]) ).
cnf(f_32_7,plain,
( cC152(U_127)
| ~ cC150(U_124)
| ~ rR1(U_127,U_124) ),
inference(clausify,[status(thm)],[f_32_4]) ).
fof(f_33_1,plain,
! [X] :
( ( cC154(X)
| ! [Y] :
( ~ cC152(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC152(Y)
& rR1(X,Y) )
| ~ cC154(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_32]) ).
fof(f_33_2,plain,
! [U_130] :
( ( cC154(U_130)
| ! [U_129] :
( ~ cC152(U_129)
| ~ rR1(U_130,U_129) ) )
& ( ? [U_128] :
( cC152(U_128)
& rR1(U_130,U_128) )
| ~ cC154(U_130) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_132] :
( cC154(U_132)
| ! [U_129] :
( ~ cC152(U_129)
| ~ rR1(U_132,U_129) ) )
& ! [U_131] :
( ? [U_128] :
( cC152(U_128)
& rR1(U_131,U_128) )
| ~ cC154(U_131) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
fof(f_33_4,plain,
( ! [U_132] :
( cC154(U_132)
| ! [U_129] :
( ~ cC152(U_129)
| ~ rR1(U_132,U_129) ) )
& ! [U_131] :
( ( cC152(sK17(U_131))
& rR1(U_131,sK17(U_131)) )
| ~ cC154(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))
| ~ cC154(U_131) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_6,plain,
( cC152(sK17(U_131))
| ~ cC154(U_131) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_7,plain,
( cC154(U_132)
| ~ cC152(U_129)
| ~ rR1(U_132,U_129) ),
inference(clausify,[status(thm)],[f_33_4]) ).
fof(f_34_1,plain,
! [X] :
( ( cC156(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC156(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_33]) ).
fof(f_34_2,plain,
! [U_135] :
( ( cC156(U_135)
| ! [U_134] :
( cC16(U_134)
| ~ rR1(U_135,U_134) ) )
& ( ? [U_133] :
( ~ cC16(U_133)
& rR1(U_135,U_133) )
| ~ cC156(U_135) ) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
( ! [U_137] :
( cC156(U_137)
| ! [U_134] :
( cC16(U_134)
| ~ rR1(U_137,U_134) ) )
& ! [U_136] :
( ? [U_133] :
( ~ cC16(U_133)
& rR1(U_136,U_133) )
| ~ cC156(U_136) ) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
fof(f_34_4,plain,
( ! [U_137] :
( cC156(U_137)
| ! [U_134] :
( cC16(U_134)
| ~ rR1(U_137,U_134) ) )
& ! [U_136] :
( ( ~ cC16(sK18(U_136))
& rR1(U_136,sK18(U_136)) )
| ~ cC156(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))
| ~ cC156(U_136) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_6,plain,
( ~ cC16(sK18(U_136))
| ~ cC156(U_136) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_7,plain,
( cC156(U_137)
| cC16(U_134)
| ~ rR1(U_137,U_134) ),
inference(clausify,[status(thm)],[f_34_4]) ).
fof(f_35_1,plain,
! [X] :
( ( cC158(X)
| ~ cC16(X)
| ~ cC156(X) )
& ( ( cC16(X)
& cC156(X) )
| ~ cC158(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_34]) ).
fof(f_35_2,plain,
! [U_138] :
( ( cC158(U_138)
| ~ cC16(U_138)
| ~ cC156(U_138) )
& ( ( cC16(U_138)
& cC156(U_138) )
| ~ cC158(U_138) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_140] :
( cC158(U_140)
| ~ cC16(U_140)
| ~ cC156(U_140) )
& ! [U_139] :
( ( cC16(U_139)
& cC156(U_139) )
| ~ cC158(U_139) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
cnf(f_35_4,plain,
( cC156(U_139)
| ~ cC158(U_139) ),
inference(clausify,[status(thm)],[f_35_3]) ).
cnf(f_35_5,plain,
( cC16(U_139)
| ~ cC158(U_139) ),
inference(clausify,[status(thm)],[f_35_3]) ).
cnf(f_35_6,plain,
( cC158(U_140)
| ~ cC16(U_140)
| ~ cC156(U_140) ),
inference(clausify,[status(thm)],[f_35_3]) ).
fof(f_36_1,plain,
! [X] :
( ( cC160(X)
| ! [Y] :
( ~ cC158(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC158(Y)
& rR1(X,Y) )
| ~ cC160(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_35]) ).
fof(f_36_2,plain,
! [U_143] :
( ( cC160(U_143)
| ! [U_142] :
( ~ cC158(U_142)
| ~ rR1(U_143,U_142) ) )
& ( ? [U_141] :
( cC158(U_141)
& rR1(U_143,U_141) )
| ~ cC160(U_143) ) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_145] :
( cC160(U_145)
| ! [U_142] :
( ~ cC158(U_142)
| ~ rR1(U_145,U_142) ) )
& ! [U_144] :
( ? [U_141] :
( cC158(U_141)
& rR1(U_144,U_141) )
| ~ cC160(U_144) ) ),
inference(miniscope,[status(thm)],[f_36_2]) ).
fof(f_36_4,plain,
( ! [U_145] :
( cC160(U_145)
| ! [U_142] :
( ~ cC158(U_142)
| ~ rR1(U_145,U_142) ) )
& ! [U_144] :
( ( cC158(sK19(U_144))
& rR1(U_144,sK19(U_144)) )
| ~ cC160(U_144) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_141,sK19(U_144))],[f_36_3]) ).
cnf(f_36_5,plain,
( rR1(U_144,sK19(U_144))
| ~ cC160(U_144) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_6,plain,
( cC158(sK19(U_144))
| ~ cC160(U_144) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_7,plain,
( cC160(U_145)
| ~ cC158(U_142)
| ~ rR1(U_145,U_142) ),
inference(clausify,[status(thm)],[f_36_4]) ).
fof(f_37_1,plain,
! [X] :
( ( cC162(X)
| cC160(X)
| cC16(X) )
& ( ( ~ cC160(X)
& ~ cC16(X) )
| ~ cC162(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_36]) ).
fof(f_37_2,plain,
! [U_146] :
( ( cC162(U_146)
| cC160(U_146)
| cC16(U_146) )
& ( ( ~ cC160(U_146)
& ~ cC16(U_146) )
| ~ cC162(U_146) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_148] :
( cC162(U_148)
| cC160(U_148)
| cC16(U_148) )
& ! [U_147] :
( ( ~ cC160(U_147)
& ~ cC16(U_147) )
| ~ cC162(U_147) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
cnf(f_37_4,plain,
( ~ cC16(U_147)
| ~ cC162(U_147) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_5,plain,
( ~ cC160(U_147)
| ~ cC162(U_147) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_6,plain,
( cC162(U_148)
| cC160(U_148)
| cC16(U_148) ),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_38_1,plain,
! [X] :
( ( cC164(X)
| ! [Y] :
( ~ cC162(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC162(Y)
& rR1(X,Y) )
| ~ cC164(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_37]) ).
fof(f_38_2,plain,
! [U_151] :
( ( cC164(U_151)
| ! [U_150] :
( ~ cC162(U_150)
| ~ rR1(U_151,U_150) ) )
& ( ? [U_149] :
( cC162(U_149)
& rR1(U_151,U_149) )
| ~ cC164(U_151) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_153] :
( cC164(U_153)
| ! [U_150] :
( ~ cC162(U_150)
| ~ rR1(U_153,U_150) ) )
& ! [U_152] :
( ? [U_149] :
( cC162(U_149)
& rR1(U_152,U_149) )
| ~ cC164(U_152) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
fof(f_38_4,plain,
( ! [U_153] :
( cC164(U_153)
| ! [U_150] :
( ~ cC162(U_150)
| ~ rR1(U_153,U_150) ) )
& ! [U_152] :
( ( cC162(sK20(U_152))
& rR1(U_152,sK20(U_152)) )
| ~ cC164(U_152) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_149,sK20(U_152))],[f_38_3]) ).
cnf(f_38_5,plain,
( rR1(U_152,sK20(U_152))
| ~ cC164(U_152) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_6,plain,
( cC162(sK20(U_152))
| ~ cC164(U_152) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_7,plain,
( cC164(U_153)
| ~ cC162(U_150)
| ~ rR1(U_153,U_150) ),
inference(clausify,[status(thm)],[f_38_4]) ).
fof(f_39_1,plain,
! [X] :
( ( cC166(X)
| cC164(X)
| ~ cC154(X) )
& ( ( ~ cC164(X)
& cC154(X) )
| ~ cC166(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_38]) ).
fof(f_39_2,plain,
! [U_154] :
( ( cC166(U_154)
| cC164(U_154)
| ~ cC154(U_154) )
& ( ( ~ cC164(U_154)
& cC154(U_154) )
| ~ cC166(U_154) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_156] :
( cC166(U_156)
| cC164(U_156)
| ~ cC154(U_156) )
& ! [U_155] :
( ( ~ cC164(U_155)
& cC154(U_155) )
| ~ cC166(U_155) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( cC154(U_155)
| ~ cC166(U_155) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_5,plain,
( ~ cC164(U_155)
| ~ cC166(U_155) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_6,plain,
( cC166(U_156)
| cC164(U_156)
| ~ cC154(U_156) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [X] :
( ( cC168(X)
| cC142(X)
| cC166(X) )
& ( ( ~ cC142(X)
& ~ cC166(X) )
| ~ cC168(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_39]) ).
fof(f_40_2,plain,
! [U_157] :
( ( cC168(U_157)
| cC142(U_157)
| cC166(U_157) )
& ( ( ~ cC142(U_157)
& ~ cC166(U_157) )
| ~ cC168(U_157) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_159] :
( cC168(U_159)
| cC142(U_159)
| cC166(U_159) )
& ! [U_158] :
( ( ~ cC142(U_158)
& ~ cC166(U_158) )
| ~ cC168(U_158) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
cnf(f_40_4,plain,
( ~ cC166(U_158)
| ~ cC168(U_158) ),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_5,plain,
( ~ cC142(U_158)
| ~ cC168(U_158) ),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_6,plain,
( cC168(U_159)
| cC142(U_159)
| cC166(U_159) ),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,plain,
! [X] :
( ( cC170(X)
| ! [Y] :
( cC168(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC168(Y)
& rR1(X,Y) )
| ~ cC170(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_162] :
( ( cC170(U_162)
| ! [U_161] :
( cC168(U_161)
| ~ rR1(U_162,U_161) ) )
& ( ? [U_160] :
( ~ cC168(U_160)
& rR1(U_162,U_160) )
| ~ cC170(U_162) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_164] :
( cC170(U_164)
| ! [U_161] :
( cC168(U_161)
| ~ rR1(U_164,U_161) ) )
& ! [U_163] :
( ? [U_160] :
( ~ cC168(U_160)
& rR1(U_163,U_160) )
| ~ cC170(U_163) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
fof(f_41_4,plain,
( ! [U_164] :
( cC170(U_164)
| ! [U_161] :
( cC168(U_161)
| ~ rR1(U_164,U_161) ) )
& ! [U_163] :
( ( ~ cC168(sK21(U_163))
& rR1(U_163,sK21(U_163)) )
| ~ cC170(U_163) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_160,sK21(U_163))],[f_41_3]) ).
cnf(f_41_5,plain,
( rR1(U_163,sK21(U_163))
| ~ cC170(U_163) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_6,plain,
( ~ cC168(sK21(U_163))
| ~ cC170(U_163) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_7,plain,
( cC170(U_164)
| cC168(U_161)
| ~ rR1(U_164,U_161) ),
inference(clausify,[status(thm)],[f_41_4]) ).
fof(f_42_1,plain,
! [X] :
( ( cC172(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC172(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_41]) ).
fof(f_42_2,plain,
! [U_167] :
( ( cC172(U_167)
| ! [U_166] :
( cC16(U_166)
| ~ rR1(U_167,U_166) ) )
& ( ? [U_165] :
( ~ cC16(U_165)
& rR1(U_167,U_165) )
| ~ cC172(U_167) ) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
( ! [U_169] :
( cC172(U_169)
| ! [U_166] :
( cC16(U_166)
| ~ rR1(U_169,U_166) ) )
& ! [U_168] :
( ? [U_165] :
( ~ cC16(U_165)
& rR1(U_168,U_165) )
| ~ cC172(U_168) ) ),
inference(miniscope,[status(thm)],[f_42_2]) ).
fof(f_42_4,plain,
( ! [U_169] :
( cC172(U_169)
| ! [U_166] :
( cC16(U_166)
| ~ rR1(U_169,U_166) ) )
& ! [U_168] :
( ( ~ cC16(sK22(U_168))
& rR1(U_168,sK22(U_168)) )
| ~ cC172(U_168) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_165,sK22(U_168))],[f_42_3]) ).
cnf(f_42_5,plain,
( rR1(U_168,sK22(U_168))
| ~ cC172(U_168) ),
inference(clausify,[status(thm)],[f_42_4]) ).
cnf(f_42_6,plain,
( ~ cC16(sK22(U_168))
| ~ cC172(U_168) ),
inference(clausify,[status(thm)],[f_42_4]) ).
cnf(f_42_7,plain,
( cC172(U_169)
| cC16(U_166)
| ~ rR1(U_169,U_166) ),
inference(clausify,[status(thm)],[f_42_4]) ).
fof(f_43_1,plain,
! [X] :
( ( cC174(X)
| ~ cC16(X)
| ~ cC172(X) )
& ( ( cC16(X)
& cC172(X) )
| ~ cC174(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_42]) ).
fof(f_43_2,plain,
! [U_170] :
( ( cC174(U_170)
| ~ cC16(U_170)
| ~ cC172(U_170) )
& ( ( cC16(U_170)
& cC172(U_170) )
| ~ cC174(U_170) ) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
( ! [U_172] :
( cC174(U_172)
| ~ cC16(U_172)
| ~ cC172(U_172) )
& ! [U_171] :
( ( cC16(U_171)
& cC172(U_171) )
| ~ cC174(U_171) ) ),
inference(miniscope,[status(thm)],[f_43_2]) ).
cnf(f_43_4,plain,
( cC172(U_171)
| ~ cC174(U_171) ),
inference(clausify,[status(thm)],[f_43_3]) ).
cnf(f_43_5,plain,
( cC16(U_171)
| ~ cC174(U_171) ),
inference(clausify,[status(thm)],[f_43_3]) ).
cnf(f_43_6,plain,
( cC174(U_172)
| ~ cC16(U_172)
| ~ cC172(U_172) ),
inference(clausify,[status(thm)],[f_43_3]) ).
fof(f_44_1,plain,
! [X] :
( ( cC176(X)
| ! [Y] :
( ~ cC174(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC174(Y)
& rR1(X,Y) )
| ~ cC176(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_175] :
( ( cC176(U_175)
| ! [U_174] :
( ~ cC174(U_174)
| ~ rR1(U_175,U_174) ) )
& ( ? [U_173] :
( cC174(U_173)
& rR1(U_175,U_173) )
| ~ cC176(U_175) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_177] :
( cC176(U_177)
| ! [U_174] :
( ~ cC174(U_174)
| ~ rR1(U_177,U_174) ) )
& ! [U_176] :
( ? [U_173] :
( cC174(U_173)
& rR1(U_176,U_173) )
| ~ cC176(U_176) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
fof(f_44_4,plain,
( ! [U_177] :
( cC176(U_177)
| ! [U_174] :
( ~ cC174(U_174)
| ~ rR1(U_177,U_174) ) )
& ! [U_176] :
( ( cC174(sK23(U_176))
& rR1(U_176,sK23(U_176)) )
| ~ cC176(U_176) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_173,sK23(U_176))],[f_44_3]) ).
cnf(f_44_5,plain,
( rR1(U_176,sK23(U_176))
| ~ cC176(U_176) ),
inference(clausify,[status(thm)],[f_44_4]) ).
cnf(f_44_6,plain,
( cC174(sK23(U_176))
| ~ cC176(U_176) ),
inference(clausify,[status(thm)],[f_44_4]) ).
cnf(f_44_7,plain,
( cC176(U_177)
| ~ cC174(U_174)
| ~ rR1(U_177,U_174) ),
inference(clausify,[status(thm)],[f_44_4]) ).
fof(f_45_1,plain,
! [X] :
( ( cC178(X)
| cC176(X)
| cC16(X) )
& ( ( ~ cC176(X)
& ~ cC16(X) )
| ~ cC178(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_44]) ).
fof(f_45_2,plain,
! [U_178] :
( ( cC178(U_178)
| cC176(U_178)
| cC16(U_178) )
& ( ( ~ cC176(U_178)
& ~ cC16(U_178) )
| ~ cC178(U_178) ) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
( ! [U_180] :
( cC178(U_180)
| cC176(U_180)
| cC16(U_180) )
& ! [U_179] :
( ( ~ cC176(U_179)
& ~ cC16(U_179) )
| ~ cC178(U_179) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
cnf(f_45_4,plain,
( ~ cC16(U_179)
| ~ cC178(U_179) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_5,plain,
( ~ cC176(U_179)
| ~ cC178(U_179) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_6,plain,
( cC178(U_180)
| cC176(U_180)
| cC16(U_180) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [X] :
( ( cC18(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC18(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_45]) ).
fof(f_46_2,plain,
! [U_183] :
( ( cC18(U_183)
| ! [U_182] :
( cC16(U_182)
| ~ rR1(U_183,U_182) ) )
& ( ? [U_181] :
( ~ cC16(U_181)
& rR1(U_183,U_181) )
| ~ cC18(U_183) ) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_185] :
( cC18(U_185)
| ! [U_182] :
( cC16(U_182)
| ~ rR1(U_185,U_182) ) )
& ! [U_184] :
( ? [U_181] :
( ~ cC16(U_181)
& rR1(U_184,U_181) )
| ~ cC18(U_184) ) ),
inference(miniscope,[status(thm)],[f_46_2]) ).
fof(f_46_4,plain,
( ! [U_185] :
( cC18(U_185)
| ! [U_182] :
( cC16(U_182)
| ~ rR1(U_185,U_182) ) )
& ! [U_184] :
( ( ~ cC16(sK24(U_184))
& rR1(U_184,sK24(U_184)) )
| ~ cC18(U_184) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_181,sK24(U_184))],[f_46_3]) ).
cnf(f_46_5,plain,
( rR1(U_184,sK24(U_184))
| ~ cC18(U_184) ),
inference(clausify,[status(thm)],[f_46_4]) ).
cnf(f_46_6,plain,
( ~ cC16(sK24(U_184))
| ~ cC18(U_184) ),
inference(clausify,[status(thm)],[f_46_4]) ).
cnf(f_46_7,plain,
( cC18(U_185)
| cC16(U_182)
| ~ rR1(U_185,U_182) ),
inference(clausify,[status(thm)],[f_46_4]) ).
fof(f_47_1,plain,
! [X] :
( ( cC180(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC180(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_46]) ).
fof(f_47_2,plain,
! [U_188] :
( ( cC180(U_188)
| ! [U_187] :
( cC16(U_187)
| ~ rR1(U_188,U_187) ) )
& ( ? [U_186] :
( ~ cC16(U_186)
& rR1(U_188,U_186) )
| ~ cC180(U_188) ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_190] :
( cC180(U_190)
| ! [U_187] :
( cC16(U_187)
| ~ rR1(U_190,U_187) ) )
& ! [U_189] :
( ? [U_186] :
( ~ cC16(U_186)
& rR1(U_189,U_186) )
| ~ cC180(U_189) ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
fof(f_47_4,plain,
( ! [U_190] :
( cC180(U_190)
| ! [U_187] :
( cC16(U_187)
| ~ rR1(U_190,U_187) ) )
& ! [U_189] :
( ( ~ cC16(sK25(U_189))
& rR1(U_189,sK25(U_189)) )
| ~ cC180(U_189) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_186,sK25(U_189))],[f_47_3]) ).
cnf(f_47_5,plain,
( rR1(U_189,sK25(U_189))
| ~ cC180(U_189) ),
inference(clausify,[status(thm)],[f_47_4]) ).
cnf(f_47_6,plain,
( ~ cC16(sK25(U_189))
| ~ cC180(U_189) ),
inference(clausify,[status(thm)],[f_47_4]) ).
cnf(f_47_7,plain,
( cC180(U_190)
| cC16(U_187)
| ~ rR1(U_190,U_187) ),
inference(clausify,[status(thm)],[f_47_4]) ).
fof(f_48_1,plain,
! [X] :
( ( cC182(X)
| ~ cC180(X)
| ~ cC16(X) )
& ( ( cC180(X)
& cC16(X) )
| ~ cC182(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_47]) ).
fof(f_48_2,plain,
! [U_191] :
( ( cC182(U_191)
| ~ cC180(U_191)
| ~ cC16(U_191) )
& ( ( cC180(U_191)
& cC16(U_191) )
| ~ cC182(U_191) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_193] :
( cC182(U_193)
| ~ cC180(U_193)
| ~ cC16(U_193) )
& ! [U_192] :
( ( cC180(U_192)
& cC16(U_192) )
| ~ cC182(U_192) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( cC16(U_192)
| ~ cC182(U_192) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_5,plain,
( cC180(U_192)
| ~ cC182(U_192) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_6,plain,
( cC182(U_193)
| ~ cC180(U_193)
| ~ cC16(U_193) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [X] :
( ( cC184(X)
| ! [Y] :
( ~ cC182(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC182(Y)
& rR1(X,Y) )
| ~ cC184(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_48]) ).
fof(f_49_2,plain,
! [U_196] :
( ( cC184(U_196)
| ! [U_195] :
( ~ cC182(U_195)
| ~ rR1(U_196,U_195) ) )
& ( ? [U_194] :
( cC182(U_194)
& rR1(U_196,U_194) )
| ~ cC184(U_196) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_198] :
( cC184(U_198)
| ! [U_195] :
( ~ cC182(U_195)
| ~ rR1(U_198,U_195) ) )
& ! [U_197] :
( ? [U_194] :
( cC182(U_194)
& rR1(U_197,U_194) )
| ~ cC184(U_197) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
fof(f_49_4,plain,
( ! [U_198] :
( cC184(U_198)
| ! [U_195] :
( ~ cC182(U_195)
| ~ rR1(U_198,U_195) ) )
& ! [U_197] :
( ( cC182(sK26(U_197))
& rR1(U_197,sK26(U_197)) )
| ~ cC184(U_197) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_194,sK26(U_197))],[f_49_3]) ).
cnf(f_49_5,plain,
( rR1(U_197,sK26(U_197))
| ~ cC184(U_197) ),
inference(clausify,[status(thm)],[f_49_4]) ).
cnf(f_49_6,plain,
( cC182(sK26(U_197))
| ~ cC184(U_197) ),
inference(clausify,[status(thm)],[f_49_4]) ).
cnf(f_49_7,plain,
( cC184(U_198)
| ~ cC182(U_195)
| ~ rR1(U_198,U_195) ),
inference(clausify,[status(thm)],[f_49_4]) ).
fof(f_50_1,plain,
! [X] :
( ( cC186(X)
| cC184(X)
| cC16(X) )
& ( ( ~ cC184(X)
& ~ cC16(X) )
| ~ cC186(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_49]) ).
fof(f_50_2,plain,
! [U_199] :
( ( cC186(U_199)
| cC184(U_199)
| cC16(U_199) )
& ( ( ~ cC184(U_199)
& ~ cC16(U_199) )
| ~ cC186(U_199) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_201] :
( cC186(U_201)
| cC184(U_201)
| cC16(U_201) )
& ! [U_200] :
( ( ~ cC184(U_200)
& ~ cC16(U_200) )
| ~ cC186(U_200) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
cnf(f_50_4,plain,
( ~ cC16(U_200)
| ~ cC186(U_200) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_5,plain,
( ~ cC184(U_200)
| ~ cC186(U_200) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_6,plain,
( cC186(U_201)
| cC184(U_201)
| cC16(U_201) ),
inference(clausify,[status(thm)],[f_50_3]) ).
fof(f_51_1,plain,
! [X] :
( ( cC188(X)
| ! [Y] :
( ~ cC186(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC186(Y)
& rR1(X,Y) )
| ~ cC188(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_50]) ).
fof(f_51_2,plain,
! [U_204] :
( ( cC188(U_204)
| ! [U_203] :
( ~ cC186(U_203)
| ~ rR1(U_204,U_203) ) )
& ( ? [U_202] :
( cC186(U_202)
& rR1(U_204,U_202) )
| ~ cC188(U_204) ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_206] :
( cC188(U_206)
| ! [U_203] :
( ~ cC186(U_203)
| ~ rR1(U_206,U_203) ) )
& ! [U_205] :
( ? [U_202] :
( cC186(U_202)
& rR1(U_205,U_202) )
| ~ cC188(U_205) ) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
fof(f_51_4,plain,
( ! [U_206] :
( cC188(U_206)
| ! [U_203] :
( ~ cC186(U_203)
| ~ rR1(U_206,U_203) ) )
& ! [U_205] :
( ( cC186(sK27(U_205))
& rR1(U_205,sK27(U_205)) )
| ~ cC188(U_205) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_202,sK27(U_205))],[f_51_3]) ).
cnf(f_51_5,plain,
( rR1(U_205,sK27(U_205))
| ~ cC188(U_205) ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_6,plain,
( cC186(sK27(U_205))
| ~ cC188(U_205) ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_7,plain,
( cC188(U_206)
| ~ cC186(U_203)
| ~ rR1(U_206,U_203) ),
inference(clausify,[status(thm)],[f_51_4]) ).
fof(f_52_1,plain,
! [X] :
( ( cC190(X)
| ! [Y] :
( ~ cC188(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC188(Y)
& rR1(X,Y) )
| ~ cC190(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_51]) ).
fof(f_52_2,plain,
! [U_209] :
( ( cC190(U_209)
| ! [U_208] :
( ~ cC188(U_208)
| ~ rR1(U_209,U_208) ) )
& ( ? [U_207] :
( cC188(U_207)
& rR1(U_209,U_207) )
| ~ cC190(U_209) ) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_211] :
( cC190(U_211)
| ! [U_208] :
( ~ cC188(U_208)
| ~ rR1(U_211,U_208) ) )
& ! [U_210] :
( ? [U_207] :
( cC188(U_207)
& rR1(U_210,U_207) )
| ~ cC190(U_210) ) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
fof(f_52_4,plain,
( ! [U_211] :
( cC190(U_211)
| ! [U_208] :
( ~ cC188(U_208)
| ~ rR1(U_211,U_208) ) )
& ! [U_210] :
( ( cC188(sK28(U_210))
& rR1(U_210,sK28(U_210)) )
| ~ cC190(U_210) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_207,sK28(U_210))],[f_52_3]) ).
cnf(f_52_5,plain,
( rR1(U_210,sK28(U_210))
| ~ cC190(U_210) ),
inference(clausify,[status(thm)],[f_52_4]) ).
cnf(f_52_6,plain,
( cC188(sK28(U_210))
| ~ cC190(U_210) ),
inference(clausify,[status(thm)],[f_52_4]) ).
cnf(f_52_7,plain,
( cC190(U_211)
| ~ cC188(U_208)
| ~ rR1(U_211,U_208) ),
inference(clausify,[status(thm)],[f_52_4]) ).
fof(f_53_1,plain,
! [X] :
( ( cC192(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC192(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_52]) ).
fof(f_53_2,plain,
! [U_214] :
( ( cC192(U_214)
| ! [U_213] :
( cC16(U_213)
| ~ rR1(U_214,U_213) ) )
& ( ? [U_212] :
( ~ cC16(U_212)
& rR1(U_214,U_212) )
| ~ cC192(U_214) ) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_216] :
( cC192(U_216)
| ! [U_213] :
( cC16(U_213)
| ~ rR1(U_216,U_213) ) )
& ! [U_215] :
( ? [U_212] :
( ~ cC16(U_212)
& rR1(U_215,U_212) )
| ~ cC192(U_215) ) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
fof(f_53_4,plain,
( ! [U_216] :
( cC192(U_216)
| ! [U_213] :
( cC16(U_213)
| ~ rR1(U_216,U_213) ) )
& ! [U_215] :
( ( ~ cC16(sK29(U_215))
& rR1(U_215,sK29(U_215)) )
| ~ cC192(U_215) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_212,sK29(U_215))],[f_53_3]) ).
cnf(f_53_5,plain,
( rR1(U_215,sK29(U_215))
| ~ cC192(U_215) ),
inference(clausify,[status(thm)],[f_53_4]) ).
cnf(f_53_6,plain,
( ~ cC16(sK29(U_215))
| ~ cC192(U_215) ),
inference(clausify,[status(thm)],[f_53_4]) ).
cnf(f_53_7,plain,
( cC192(U_216)
| cC16(U_213)
| ~ rR1(U_216,U_213) ),
inference(clausify,[status(thm)],[f_53_4]) ).
fof(f_54_1,plain,
! [X] :
( ( cC194(X)
| ~ cC16(X)
| ~ cC192(X) )
& ( ( cC16(X)
& cC192(X) )
| ~ cC194(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_53]) ).
fof(f_54_2,plain,
! [U_217] :
( ( cC194(U_217)
| ~ cC16(U_217)
| ~ cC192(U_217) )
& ( ( cC16(U_217)
& cC192(U_217) )
| ~ cC194(U_217) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_219] :
( cC194(U_219)
| ~ cC16(U_219)
| ~ cC192(U_219) )
& ! [U_218] :
( ( cC16(U_218)
& cC192(U_218) )
| ~ cC194(U_218) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( cC192(U_218)
| ~ cC194(U_218) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( cC16(U_218)
| ~ cC194(U_218) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_6,plain,
( cC194(U_219)
| ~ cC16(U_219)
| ~ cC192(U_219) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [X] :
( ( cC196(X)
| ! [Y] :
( ~ cC194(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC194(Y)
& rR1(X,Y) )
| ~ cC196(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_54]) ).
fof(f_55_2,plain,
! [U_222] :
( ( cC196(U_222)
| ! [U_221] :
( ~ cC194(U_221)
| ~ rR1(U_222,U_221) ) )
& ( ? [U_220] :
( cC194(U_220)
& rR1(U_222,U_220) )
| ~ cC196(U_222) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_224] :
( cC196(U_224)
| ! [U_221] :
( ~ cC194(U_221)
| ~ rR1(U_224,U_221) ) )
& ! [U_223] :
( ? [U_220] :
( cC194(U_220)
& rR1(U_223,U_220) )
| ~ cC196(U_223) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
fof(f_55_4,plain,
( ! [U_224] :
( cC196(U_224)
| ! [U_221] :
( ~ cC194(U_221)
| ~ rR1(U_224,U_221) ) )
& ! [U_223] :
( ( cC194(sK30(U_223))
& rR1(U_223,sK30(U_223)) )
| ~ cC196(U_223) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_220,sK30(U_223))],[f_55_3]) ).
cnf(f_55_5,plain,
( rR1(U_223,sK30(U_223))
| ~ cC196(U_223) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_6,plain,
( cC194(sK30(U_223))
| ~ cC196(U_223) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_7,plain,
( cC196(U_224)
| ~ cC194(U_221)
| ~ rR1(U_224,U_221) ),
inference(clausify,[status(thm)],[f_55_4]) ).
fof(f_56_1,plain,
! [X] :
( ( cC198(X)
| cC16(X)
| cC196(X) )
& ( ( ~ cC16(X)
& ~ cC196(X) )
| ~ cC198(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_55]) ).
fof(f_56_2,plain,
! [U_225] :
( ( cC198(U_225)
| cC16(U_225)
| cC196(U_225) )
& ( ( ~ cC16(U_225)
& ~ cC196(U_225) )
| ~ cC198(U_225) ) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
( ! [U_227] :
( cC198(U_227)
| cC16(U_227)
| cC196(U_227) )
& ! [U_226] :
( ( ~ cC16(U_226)
& ~ cC196(U_226) )
| ~ cC198(U_226) ) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
cnf(f_56_4,plain,
( ~ cC196(U_226)
| ~ cC198(U_226) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_5,plain,
( ~ cC16(U_226)
| ~ cC198(U_226) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_6,plain,
( cC198(U_227)
| cC16(U_227)
| cC196(U_227) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
! [X] :
( ( cC20(X)
| ~ cC16(X)
| ~ cC18(X) )
& ( ( cC16(X)
& cC18(X) )
| ~ cC20(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_56]) ).
fof(f_57_2,plain,
! [U_228] :
( ( cC20(U_228)
| ~ cC16(U_228)
| ~ cC18(U_228) )
& ( ( cC16(U_228)
& cC18(U_228) )
| ~ cC20(U_228) ) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
( ! [U_230] :
( cC20(U_230)
| ~ cC16(U_230)
| ~ cC18(U_230) )
& ! [U_229] :
( ( cC16(U_229)
& cC18(U_229) )
| ~ cC20(U_229) ) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( cC18(U_229)
| ~ cC20(U_229) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( cC16(U_229)
| ~ cC20(U_229) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_6,plain,
( cC20(U_230)
| ~ cC16(U_230)
| ~ cC18(U_230) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [X] :
( ( cC200(X)
| ! [Y] :
( ~ cC198(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC198(Y)
& rR1(X,Y) )
| ~ cC200(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_57]) ).
fof(f_58_2,plain,
! [U_233] :
( ( cC200(U_233)
| ! [U_232] :
( ~ cC198(U_232)
| ~ rR1(U_233,U_232) ) )
& ( ? [U_231] :
( cC198(U_231)
& rR1(U_233,U_231) )
| ~ cC200(U_233) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_235] :
( cC200(U_235)
| ! [U_232] :
( ~ cC198(U_232)
| ~ rR1(U_235,U_232) ) )
& ! [U_234] :
( ? [U_231] :
( cC198(U_231)
& rR1(U_234,U_231) )
| ~ cC200(U_234) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
fof(f_58_4,plain,
( ! [U_235] :
( cC200(U_235)
| ! [U_232] :
( ~ cC198(U_232)
| ~ rR1(U_235,U_232) ) )
& ! [U_234] :
( ( cC198(sK31(U_234))
& rR1(U_234,sK31(U_234)) )
| ~ cC200(U_234) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_231,sK31(U_234))],[f_58_3]) ).
cnf(f_58_5,plain,
( rR1(U_234,sK31(U_234))
| ~ cC200(U_234) ),
inference(clausify,[status(thm)],[f_58_4]) ).
cnf(f_58_6,plain,
( cC198(sK31(U_234))
| ~ cC200(U_234) ),
inference(clausify,[status(thm)],[f_58_4]) ).
cnf(f_58_7,plain,
( cC200(U_235)
| ~ cC198(U_232)
| ~ rR1(U_235,U_232) ),
inference(clausify,[status(thm)],[f_58_4]) ).
fof(f_59_1,plain,
! [X] :
( ( cC202(X)
| cC200(X)
| ~ cC190(X) )
& ( ( ~ cC200(X)
& cC190(X) )
| ~ cC202(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_58]) ).
fof(f_59_2,plain,
! [U_236] :
( ( cC202(U_236)
| cC200(U_236)
| ~ cC190(U_236) )
& ( ( ~ cC200(U_236)
& cC190(U_236) )
| ~ cC202(U_236) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_238] :
( cC202(U_238)
| cC200(U_238)
| ~ cC190(U_238) )
& ! [U_237] :
( ( ~ cC200(U_237)
& cC190(U_237) )
| ~ cC202(U_237) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
cnf(f_59_4,plain,
( cC190(U_237)
| ~ cC202(U_237) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_5,plain,
( ~ cC200(U_237)
| ~ cC202(U_237) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_6,plain,
( cC202(U_238)
| cC200(U_238)
| ~ cC190(U_238) ),
inference(clausify,[status(thm)],[f_59_3]) ).
fof(f_60_1,plain,
! [X] :
( ( cC204(X)
| cC202(X)
| cC178(X) )
& ( ( ~ cC202(X)
& ~ cC178(X) )
| ~ cC204(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_59]) ).
fof(f_60_2,plain,
! [U_239] :
( ( cC204(U_239)
| cC202(U_239)
| cC178(U_239) )
& ( ( ~ cC202(U_239)
& ~ cC178(U_239) )
| ~ cC204(U_239) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_241] :
( cC204(U_241)
| cC202(U_241)
| cC178(U_241) )
& ! [U_240] :
( ( ~ cC202(U_240)
& ~ cC178(U_240) )
| ~ cC204(U_240) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
cnf(f_60_4,plain,
( ~ cC178(U_240)
| ~ cC204(U_240) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_5,plain,
( ~ cC202(U_240)
| ~ cC204(U_240) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_6,plain,
( cC204(U_241)
| cC202(U_241)
| cC178(U_241) ),
inference(clausify,[status(thm)],[f_60_3]) ).
fof(f_61_1,plain,
! [X] :
( ( cC206(X)
| ~ cC204(X)
| ~ cC170(X) )
& ( ( cC204(X)
& cC170(X) )
| ~ cC206(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_60]) ).
fof(f_61_2,plain,
! [U_242] :
( ( cC206(U_242)
| ~ cC204(U_242)
| ~ cC170(U_242) )
& ( ( cC204(U_242)
& cC170(U_242) )
| ~ cC206(U_242) ) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
( ! [U_244] :
( cC206(U_244)
| ~ cC204(U_244)
| ~ cC170(U_244) )
& ! [U_243] :
( ( cC204(U_243)
& cC170(U_243) )
| ~ cC206(U_243) ) ),
inference(miniscope,[status(thm)],[f_61_2]) ).
cnf(f_61_4,plain,
( cC170(U_243)
| ~ cC206(U_243) ),
inference(clausify,[status(thm)],[f_61_3]) ).
cnf(f_61_5,plain,
( cC204(U_243)
| ~ cC206(U_243) ),
inference(clausify,[status(thm)],[f_61_3]) ).
cnf(f_61_6,plain,
( cC206(U_244)
| ~ cC204(U_244)
| ~ cC170(U_244) ),
inference(clausify,[status(thm)],[f_61_3]) ).
fof(f_62_1,plain,
! [X] :
( ( cC208(X)
| ! [Y] :
( ~ cC206(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC206(Y)
& rR1(X,Y) )
| ~ cC208(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_61]) ).
fof(f_62_2,plain,
! [U_247] :
( ( cC208(U_247)
| ! [U_246] :
( ~ cC206(U_246)
| ~ rR1(U_247,U_246) ) )
& ( ? [U_245] :
( cC206(U_245)
& rR1(U_247,U_245) )
| ~ cC208(U_247) ) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
fof(f_62_3,plain,
( ! [U_249] :
( cC208(U_249)
| ! [U_246] :
( ~ cC206(U_246)
| ~ rR1(U_249,U_246) ) )
& ! [U_248] :
( ? [U_245] :
( cC206(U_245)
& rR1(U_248,U_245) )
| ~ cC208(U_248) ) ),
inference(miniscope,[status(thm)],[f_62_2]) ).
fof(f_62_4,plain,
( ! [U_249] :
( cC208(U_249)
| ! [U_246] :
( ~ cC206(U_246)
| ~ rR1(U_249,U_246) ) )
& ! [U_248] :
( ( cC206(sK32(U_248))
& rR1(U_248,sK32(U_248)) )
| ~ cC208(U_248) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_245,sK32(U_248))],[f_62_3]) ).
cnf(f_62_5,plain,
( rR1(U_248,sK32(U_248))
| ~ cC208(U_248) ),
inference(clausify,[status(thm)],[f_62_4]) ).
cnf(f_62_6,plain,
( cC206(sK32(U_248))
| ~ cC208(U_248) ),
inference(clausify,[status(thm)],[f_62_4]) ).
cnf(f_62_7,plain,
( cC208(U_249)
| ~ cC206(U_246)
| ~ rR1(U_249,U_246) ),
inference(clausify,[status(thm)],[f_62_4]) ).
fof(f_63_1,plain,
! [X] :
( ( cC210(X)
| cC134(X)
| cC208(X) )
& ( ( ~ cC134(X)
& ~ cC208(X) )
| ~ cC210(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_62]) ).
fof(f_63_2,plain,
! [U_250] :
( ( cC210(U_250)
| cC134(U_250)
| cC208(U_250) )
& ( ( ~ cC134(U_250)
& ~ cC208(U_250) )
| ~ cC210(U_250) ) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
fof(f_63_3,plain,
( ! [U_252] :
( cC210(U_252)
| cC134(U_252)
| cC208(U_252) )
& ! [U_251] :
( ( ~ cC134(U_251)
& ~ cC208(U_251) )
| ~ cC210(U_251) ) ),
inference(miniscope,[status(thm)],[f_63_2]) ).
cnf(f_63_4,plain,
( ~ cC208(U_251)
| ~ cC210(U_251) ),
inference(clausify,[status(thm)],[f_63_3]) ).
cnf(f_63_5,plain,
( ~ cC134(U_251)
| ~ cC210(U_251) ),
inference(clausify,[status(thm)],[f_63_3]) ).
cnf(f_63_6,plain,
( cC210(U_252)
| cC134(U_252)
| cC208(U_252) ),
inference(clausify,[status(thm)],[f_63_3]) ).
fof(f_64_1,plain,
! [X] :
( ( cC212(X)
| ! [Y] :
( ~ cC210(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC210(Y)
& rR1(X,Y) )
| ~ cC212(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_63]) ).
fof(f_64_2,plain,
! [U_255] :
( ( cC212(U_255)
| ! [U_254] :
( ~ cC210(U_254)
| ~ rR1(U_255,U_254) ) )
& ( ? [U_253] :
( cC210(U_253)
& rR1(U_255,U_253) )
| ~ cC212(U_255) ) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
fof(f_64_3,plain,
( ! [U_257] :
( cC212(U_257)
| ! [U_254] :
( ~ cC210(U_254)
| ~ rR1(U_257,U_254) ) )
& ! [U_256] :
( ? [U_253] :
( cC210(U_253)
& rR1(U_256,U_253) )
| ~ cC212(U_256) ) ),
inference(miniscope,[status(thm)],[f_64_2]) ).
fof(f_64_4,plain,
( ! [U_257] :
( cC212(U_257)
| ! [U_254] :
( ~ cC210(U_254)
| ~ rR1(U_257,U_254) ) )
& ! [U_256] :
( ( cC210(sK33(U_256))
& rR1(U_256,sK33(U_256)) )
| ~ cC212(U_256) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_253,sK33(U_256))],[f_64_3]) ).
cnf(f_64_5,plain,
( rR1(U_256,sK33(U_256))
| ~ cC212(U_256) ),
inference(clausify,[status(thm)],[f_64_4]) ).
cnf(f_64_6,plain,
( cC210(sK33(U_256))
| ~ cC212(U_256) ),
inference(clausify,[status(thm)],[f_64_4]) ).
cnf(f_64_7,plain,
( cC212(U_257)
| ~ cC210(U_254)
| ~ rR1(U_257,U_254) ),
inference(clausify,[status(thm)],[f_64_4]) ).
fof(f_65_1,plain,
! [X] :
( ( cC214(X)
| cC212(X)
| ~ cC100(X) )
& ( ( ~ cC212(X)
& cC100(X) )
| ~ cC214(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
! [U_258] :
( ( cC214(U_258)
| cC212(U_258)
| ~ cC100(U_258) )
& ( ( ~ cC212(U_258)
& cC100(U_258) )
| ~ cC214(U_258) ) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
( ! [U_260] :
( cC214(U_260)
| cC212(U_260)
| ~ cC100(U_260) )
& ! [U_259] :
( ( ~ cC212(U_259)
& cC100(U_259) )
| ~ cC214(U_259) ) ),
inference(miniscope,[status(thm)],[f_65_2]) ).
cnf(f_65_4,plain,
( cC100(U_259)
| ~ cC214(U_259) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_5,plain,
( ~ cC212(U_259)
| ~ cC214(U_259) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_6,plain,
( cC214(U_260)
| cC212(U_260)
| ~ cC100(U_260) ),
inference(clausify,[status(thm)],[f_65_3]) ).
fof(f_66_1,plain,
! [X] :
( ( cC216(X)
| ~ cC64(X)
| cC214(X) )
& ( ( cC64(X)
& ~ cC214(X) )
| ~ cC216(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_261] :
( ( cC216(U_261)
| ~ cC64(U_261)
| cC214(U_261) )
& ( ( cC64(U_261)
& ~ cC214(U_261) )
| ~ cC216(U_261) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_263] :
( cC216(U_263)
| ~ cC64(U_263)
| cC214(U_263) )
& ! [U_262] :
( ( cC64(U_262)
& ~ cC214(U_262) )
| ~ cC216(U_262) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( ~ cC214(U_262)
| ~ cC216(U_262) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( cC64(U_262)
| ~ cC216(U_262) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_6,plain,
( cC216(U_263)
| ~ cC64(U_263)
| cC214(U_263) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_1,plain,
! [X] :
( ( cC22(X)
| ! [Y] :
( ~ cC20(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC20(Y)
& rR1(X,Y) )
| ~ cC22(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_66]) ).
fof(f_67_2,plain,
! [U_266] :
( ( cC22(U_266)
| ! [U_265] :
( ~ cC20(U_265)
| ~ rR1(U_266,U_265) ) )
& ( ? [U_264] :
( cC20(U_264)
& rR1(U_266,U_264) )
| ~ cC22(U_266) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_268] :
( cC22(U_268)
| ! [U_265] :
( ~ cC20(U_265)
| ~ rR1(U_268,U_265) ) )
& ! [U_267] :
( ? [U_264] :
( cC20(U_264)
& rR1(U_267,U_264) )
| ~ cC22(U_267) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
fof(f_67_4,plain,
( ! [U_268] :
( cC22(U_268)
| ! [U_265] :
( ~ cC20(U_265)
| ~ rR1(U_268,U_265) ) )
& ! [U_267] :
( ( cC20(sK34(U_267))
& rR1(U_267,sK34(U_267)) )
| ~ cC22(U_267) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_264,sK34(U_267))],[f_67_3]) ).
cnf(f_67_5,plain,
( rR1(U_267,sK34(U_267))
| ~ cC22(U_267) ),
inference(clausify,[status(thm)],[f_67_4]) ).
cnf(f_67_6,plain,
( cC20(sK34(U_267))
| ~ cC22(U_267) ),
inference(clausify,[status(thm)],[f_67_4]) ).
cnf(f_67_7,plain,
( cC22(U_268)
| ~ cC20(U_265)
| ~ rR1(U_268,U_265) ),
inference(clausify,[status(thm)],[f_67_4]) ).
fof(f_68_1,plain,
! [X] :
( ( cC24(X)
| cC16(X)
| cC22(X) )
& ( ( ~ cC16(X)
& ~ cC22(X) )
| ~ cC24(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_67]) ).
fof(f_68_2,plain,
! [U_269] :
( ( cC24(U_269)
| cC16(U_269)
| cC22(U_269) )
& ( ( ~ cC16(U_269)
& ~ cC22(U_269) )
| ~ cC24(U_269) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_271] :
( cC24(U_271)
| cC16(U_271)
| cC22(U_271) )
& ! [U_270] :
( ( ~ cC16(U_270)
& ~ cC22(U_270) )
| ~ cC24(U_270) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( ~ cC22(U_270)
| ~ cC24(U_270) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( ~ cC16(U_270)
| ~ cC24(U_270) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_6,plain,
( cC24(U_271)
| cC16(U_271)
| cC22(U_271) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_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_68]) ).
fof(f_69_2,plain,
! [U_274] :
( ( cC26(U_274)
| ! [U_273] :
( ~ cC24(U_273)
| ~ rR1(U_274,U_273) ) )
& ( ? [U_272] :
( cC24(U_272)
& rR1(U_274,U_272) )
| ~ cC26(U_274) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_276] :
( cC26(U_276)
| ! [U_273] :
( ~ cC24(U_273)
| ~ rR1(U_276,U_273) ) )
& ! [U_275] :
( ? [U_272] :
( cC24(U_272)
& rR1(U_275,U_272) )
| ~ cC26(U_275) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
fof(f_69_4,plain,
( ! [U_276] :
( cC26(U_276)
| ! [U_273] :
( ~ cC24(U_273)
| ~ rR1(U_276,U_273) ) )
& ! [U_275] :
( ( cC24(sK35(U_275))
& rR1(U_275,sK35(U_275)) )
| ~ cC26(U_275) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(U_272,sK35(U_275))],[f_69_3]) ).
cnf(f_69_5,plain,
( rR1(U_275,sK35(U_275))
| ~ cC26(U_275) ),
inference(clausify,[status(thm)],[f_69_4]) ).
cnf(f_69_6,plain,
( cC24(sK35(U_275))
| ~ cC26(U_275) ),
inference(clausify,[status(thm)],[f_69_4]) ).
cnf(f_69_7,plain,
( cC26(U_276)
| ~ cC24(U_273)
| ~ rR1(U_276,U_273) ),
inference(clausify,[status(thm)],[f_69_4]) ).
fof(f_70_1,plain,
! [X] :
( ( cC28(X)
| cC16(X)
| cC26(X) )
& ( ( ~ cC16(X)
& ~ cC26(X) )
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_69]) ).
fof(f_70_2,plain,
! [U_277] :
( ( cC28(U_277)
| cC16(U_277)
| cC26(U_277) )
& ( ( ~ cC16(U_277)
& ~ cC26(U_277) )
| ~ cC28(U_277) ) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
fof(f_70_3,plain,
( ! [U_279] :
( cC28(U_279)
| cC16(U_279)
| cC26(U_279) )
& ! [U_278] :
( ( ~ cC16(U_278)
& ~ cC26(U_278) )
| ~ cC28(U_278) ) ),
inference(miniscope,[status(thm)],[f_70_2]) ).
cnf(f_70_4,plain,
( ~ cC26(U_278)
| ~ cC28(U_278) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_5,plain,
( ~ cC16(U_278)
| ~ cC28(U_278) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_6,plain,
( cC28(U_279)
| cC16(U_279)
| cC26(U_279) ),
inference(clausify,[status(thm)],[f_70_3]) ).
fof(f_71_1,plain,
! [X] :
( ( cC30(X)
| ~ cC28(X)
| ~ cC14(X) )
& ( ( cC28(X)
& cC14(X) )
| ~ cC30(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_70]) ).
fof(f_71_2,plain,
! [U_280] :
( ( cC30(U_280)
| ~ cC28(U_280)
| ~ cC14(U_280) )
& ( ( cC28(U_280)
& cC14(U_280) )
| ~ cC30(U_280) ) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
( ! [U_282] :
( cC30(U_282)
| ~ cC28(U_282)
| ~ cC14(U_282) )
& ! [U_281] :
( ( cC28(U_281)
& cC14(U_281) )
| ~ cC30(U_281) ) ),
inference(miniscope,[status(thm)],[f_71_2]) ).
cnf(f_71_4,plain,
( cC14(U_281)
| ~ cC30(U_281) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_5,plain,
( cC28(U_281)
| ~ cC30(U_281) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_6,plain,
( cC30(U_282)
| ~ cC28(U_282)
| ~ cC14(U_282) ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_1,plain,
! [X] :
( ( cC34(X)
| ! [Y] :
( cC32(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC32(Y)
& rR1(X,Y) )
| ~ cC34(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_71]) ).
fof(f_72_2,plain,
! [U_285] :
( ( cC34(U_285)
| ! [U_284] :
( cC32(U_284)
| ~ rR1(U_285,U_284) ) )
& ( ? [U_283] :
( ~ cC32(U_283)
& rR1(U_285,U_283) )
| ~ cC34(U_285) ) ),
inference(variable_rename,[status(thm)],[f_72_1]) ).
fof(f_72_3,plain,
( ! [U_287] :
( cC34(U_287)
| ! [U_284] :
( cC32(U_284)
| ~ rR1(U_287,U_284) ) )
& ! [U_286] :
( ? [U_283] :
( ~ cC32(U_283)
& rR1(U_286,U_283) )
| ~ cC34(U_286) ) ),
inference(miniscope,[status(thm)],[f_72_2]) ).
fof(f_72_4,plain,
( ! [U_287] :
( cC34(U_287)
| ! [U_284] :
( cC32(U_284)
| ~ rR1(U_287,U_284) ) )
& ! [U_286] :
( ( ~ cC32(sK36(U_286))
& rR1(U_286,sK36(U_286)) )
| ~ cC34(U_286) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(U_283,sK36(U_286))],[f_72_3]) ).
cnf(f_72_5,plain,
( rR1(U_286,sK36(U_286))
| ~ cC34(U_286) ),
inference(clausify,[status(thm)],[f_72_4]) ).
cnf(f_72_6,plain,
( ~ cC32(sK36(U_286))
| ~ cC34(U_286) ),
inference(clausify,[status(thm)],[f_72_4]) ).
cnf(f_72_7,plain,
( cC34(U_287)
| cC32(U_284)
| ~ rR1(U_287,U_284) ),
inference(clausify,[status(thm)],[f_72_4]) ).
fof(f_73_1,plain,
! [X] :
( ( cC36(X)
| ~ cC34(X)
| ~ cC32(X) )
& ( ( cC34(X)
& cC32(X) )
| ~ cC36(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_72]) ).
fof(f_73_2,plain,
! [U_288] :
( ( cC36(U_288)
| ~ cC34(U_288)
| ~ cC32(U_288) )
& ( ( cC34(U_288)
& cC32(U_288) )
| ~ cC36(U_288) ) ),
inference(variable_rename,[status(thm)],[f_73_1]) ).
fof(f_73_3,plain,
( ! [U_290] :
( cC36(U_290)
| ~ cC34(U_290)
| ~ cC32(U_290) )
& ! [U_289] :
( ( cC34(U_289)
& cC32(U_289) )
| ~ cC36(U_289) ) ),
inference(miniscope,[status(thm)],[f_73_2]) ).
cnf(f_73_4,plain,
( cC32(U_289)
| ~ cC36(U_289) ),
inference(clausify,[status(thm)],[f_73_3]) ).
cnf(f_73_5,plain,
( cC34(U_289)
| ~ cC36(U_289) ),
inference(clausify,[status(thm)],[f_73_3]) ).
cnf(f_73_6,plain,
( cC36(U_290)
| ~ cC34(U_290)
| ~ cC32(U_290) ),
inference(clausify,[status(thm)],[f_73_3]) ).
fof(f_74_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_73]) ).
fof(f_74_2,plain,
! [U_293] :
( ( cC38(U_293)
| ! [U_292] :
( ~ cC36(U_292)
| ~ rR1(U_293,U_292) ) )
& ( ? [U_291] :
( cC36(U_291)
& rR1(U_293,U_291) )
| ~ cC38(U_293) ) ),
inference(variable_rename,[status(thm)],[f_74_1]) ).
fof(f_74_3,plain,
( ! [U_295] :
( cC38(U_295)
| ! [U_292] :
( ~ cC36(U_292)
| ~ rR1(U_295,U_292) ) )
& ! [U_294] :
( ? [U_291] :
( cC36(U_291)
& rR1(U_294,U_291) )
| ~ cC38(U_294) ) ),
inference(miniscope,[status(thm)],[f_74_2]) ).
fof(f_74_4,plain,
( ! [U_295] :
( cC38(U_295)
| ! [U_292] :
( ~ cC36(U_292)
| ~ rR1(U_295,U_292) ) )
& ! [U_294] :
( ( cC36(sK37(U_294))
& rR1(U_294,sK37(U_294)) )
| ~ cC38(U_294) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(U_291,sK37(U_294))],[f_74_3]) ).
cnf(f_74_5,plain,
( rR1(U_294,sK37(U_294))
| ~ cC38(U_294) ),
inference(clausify,[status(thm)],[f_74_4]) ).
cnf(f_74_6,plain,
( cC36(sK37(U_294))
| ~ cC38(U_294) ),
inference(clausify,[status(thm)],[f_74_4]) ).
cnf(f_74_7,plain,
( cC38(U_295)
| ~ cC36(U_292)
| ~ rR1(U_295,U_292) ),
inference(clausify,[status(thm)],[f_74_4]) ).
fof(f_75_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_74]) ).
fof(f_75_2,plain,
! [U_298] :
( ( cC4(U_298)
| ! [U_297] :
( cC2(U_297)
| ~ rR1(U_298,U_297) ) )
& ( ? [U_296] :
( ~ cC2(U_296)
& rR1(U_298,U_296) )
| ~ cC4(U_298) ) ),
inference(variable_rename,[status(thm)],[f_75_1]) ).
fof(f_75_3,plain,
( ! [U_300] :
( cC4(U_300)
| ! [U_297] :
( cC2(U_297)
| ~ rR1(U_300,U_297) ) )
& ! [U_299] :
( ? [U_296] :
( ~ cC2(U_296)
& rR1(U_299,U_296) )
| ~ cC4(U_299) ) ),
inference(miniscope,[status(thm)],[f_75_2]) ).
fof(f_75_4,plain,
( ! [U_300] :
( cC4(U_300)
| ! [U_297] :
( cC2(U_297)
| ~ rR1(U_300,U_297) ) )
& ! [U_299] :
( ( ~ cC2(sK38(U_299))
& rR1(U_299,sK38(U_299)) )
| ~ cC4(U_299) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(U_296,sK38(U_299))],[f_75_3]) ).
cnf(f_75_5,plain,
( rR1(U_299,sK38(U_299))
| ~ cC4(U_299) ),
inference(clausify,[status(thm)],[f_75_4]) ).
cnf(f_75_6,plain,
( ~ cC2(sK38(U_299))
| ~ cC4(U_299) ),
inference(clausify,[status(thm)],[f_75_4]) ).
cnf(f_75_7,plain,
( cC4(U_300)
| cC2(U_297)
| ~ rR1(U_300,U_297) ),
inference(clausify,[status(thm)],[f_75_4]) ).
fof(f_76_1,plain,
! [X] :
( ( cC40(X)
| cC32(X)
| cC38(X) )
& ( ( ~ cC32(X)
& ~ cC38(X) )
| ~ cC40(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_75]) ).
fof(f_76_2,plain,
! [U_301] :
( ( cC40(U_301)
| cC32(U_301)
| cC38(U_301) )
& ( ( ~ cC32(U_301)
& ~ cC38(U_301) )
| ~ cC40(U_301) ) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
fof(f_76_3,plain,
( ! [U_303] :
( cC40(U_303)
| cC32(U_303)
| cC38(U_303) )
& ! [U_302] :
( ( ~ cC32(U_302)
& ~ cC38(U_302) )
| ~ cC40(U_302) ) ),
inference(miniscope,[status(thm)],[f_76_2]) ).
cnf(f_76_4,plain,
( ~ cC38(U_302)
| ~ cC40(U_302) ),
inference(clausify,[status(thm)],[f_76_3]) ).
cnf(f_76_5,plain,
( ~ cC32(U_302)
| ~ cC40(U_302) ),
inference(clausify,[status(thm)],[f_76_3]) ).
cnf(f_76_6,plain,
( cC40(U_303)
| cC32(U_303)
| cC38(U_303) ),
inference(clausify,[status(thm)],[f_76_3]) ).
fof(f_77_1,plain,
! [X] :
( ( cC42(X)
| ! [Y] :
( ~ cC40(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC40(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_76]) ).
fof(f_77_2,plain,
! [U_306] :
( ( cC42(U_306)
| ! [U_305] :
( ~ cC40(U_305)
| ~ rR1(U_306,U_305) ) )
& ( ? [U_304] :
( cC40(U_304)
& rR1(U_306,U_304) )
| ~ cC42(U_306) ) ),
inference(variable_rename,[status(thm)],[f_77_1]) ).
fof(f_77_3,plain,
( ! [U_308] :
( cC42(U_308)
| ! [U_305] :
( ~ cC40(U_305)
| ~ rR1(U_308,U_305) ) )
& ! [U_307] :
( ? [U_304] :
( cC40(U_304)
& rR1(U_307,U_304) )
| ~ cC42(U_307) ) ),
inference(miniscope,[status(thm)],[f_77_2]) ).
fof(f_77_4,plain,
( ! [U_308] :
( cC42(U_308)
| ! [U_305] :
( ~ cC40(U_305)
| ~ rR1(U_308,U_305) ) )
& ! [U_307] :
( ( cC40(sK39(U_307))
& rR1(U_307,sK39(U_307)) )
| ~ cC42(U_307) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(U_304,sK39(U_307))],[f_77_3]) ).
cnf(f_77_5,plain,
( rR1(U_307,sK39(U_307))
| ~ cC42(U_307) ),
inference(clausify,[status(thm)],[f_77_4]) ).
cnf(f_77_6,plain,
( cC40(sK39(U_307))
| ~ cC42(U_307) ),
inference(clausify,[status(thm)],[f_77_4]) ).
cnf(f_77_7,plain,
( cC42(U_308)
| ~ cC40(U_305)
| ~ rR1(U_308,U_305) ),
inference(clausify,[status(thm)],[f_77_4]) ).
fof(f_78_1,plain,
! [X] :
( ( cC44(X)
| cC42(X)
| cC32(X) )
& ( ( ~ cC42(X)
& ~ cC32(X) )
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_77]) ).
fof(f_78_2,plain,
! [U_309] :
( ( cC44(U_309)
| cC42(U_309)
| cC32(U_309) )
& ( ( ~ cC42(U_309)
& ~ cC32(U_309) )
| ~ cC44(U_309) ) ),
inference(variable_rename,[status(thm)],[f_78_1]) ).
fof(f_78_3,plain,
( ! [U_311] :
( cC44(U_311)
| cC42(U_311)
| cC32(U_311) )
& ! [U_310] :
( ( ~ cC42(U_310)
& ~ cC32(U_310) )
| ~ cC44(U_310) ) ),
inference(miniscope,[status(thm)],[f_78_2]) ).
cnf(f_78_4,plain,
( ~ cC32(U_310)
| ~ cC44(U_310) ),
inference(clausify,[status(thm)],[f_78_3]) ).
cnf(f_78_5,plain,
( ~ cC42(U_310)
| ~ cC44(U_310) ),
inference(clausify,[status(thm)],[f_78_3]) ).
cnf(f_78_6,plain,
( cC44(U_311)
| cC42(U_311)
| cC32(U_311) ),
inference(clausify,[status(thm)],[f_78_3]) ).
fof(f_79_1,plain,
! [X] :
( ( cC46(X)
| ~ cC44(X)
| ~ cC30(X) )
& ( ( cC44(X)
& cC30(X) )
| ~ cC46(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_78]) ).
fof(f_79_2,plain,
! [U_312] :
( ( cC46(U_312)
| ~ cC44(U_312)
| ~ cC30(U_312) )
& ( ( cC44(U_312)
& cC30(U_312) )
| ~ cC46(U_312) ) ),
inference(variable_rename,[status(thm)],[f_79_1]) ).
fof(f_79_3,plain,
( ! [U_314] :
( cC46(U_314)
| ~ cC44(U_314)
| ~ cC30(U_314) )
& ! [U_313] :
( ( cC44(U_313)
& cC30(U_313) )
| ~ cC46(U_313) ) ),
inference(miniscope,[status(thm)],[f_79_2]) ).
cnf(f_79_4,plain,
( cC30(U_313)
| ~ cC46(U_313) ),
inference(clausify,[status(thm)],[f_79_3]) ).
cnf(f_79_5,plain,
( cC44(U_313)
| ~ cC46(U_313) ),
inference(clausify,[status(thm)],[f_79_3]) ).
cnf(f_79_6,plain,
( cC46(U_314)
| ~ cC44(U_314)
| ~ cC30(U_314) ),
inference(clausify,[status(thm)],[f_79_3]) ).
fof(f_80_1,plain,
! [X] :
( ( cC48(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC48(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_79]) ).
fof(f_80_2,plain,
! [U_317] :
( ( cC48(U_317)
| ! [U_316] :
( cC16(U_316)
| ~ rR1(U_317,U_316) ) )
& ( ? [U_315] :
( ~ cC16(U_315)
& rR1(U_317,U_315) )
| ~ cC48(U_317) ) ),
inference(variable_rename,[status(thm)],[f_80_1]) ).
fof(f_80_3,plain,
( ! [U_319] :
( cC48(U_319)
| ! [U_316] :
( cC16(U_316)
| ~ rR1(U_319,U_316) ) )
& ! [U_318] :
( ? [U_315] :
( ~ cC16(U_315)
& rR1(U_318,U_315) )
| ~ cC48(U_318) ) ),
inference(miniscope,[status(thm)],[f_80_2]) ).
fof(f_80_4,plain,
( ! [U_319] :
( cC48(U_319)
| ! [U_316] :
( cC16(U_316)
| ~ rR1(U_319,U_316) ) )
& ! [U_318] :
( ( ~ cC16(sK40(U_318))
& rR1(U_318,sK40(U_318)) )
| ~ cC48(U_318) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(U_315,sK40(U_318))],[f_80_3]) ).
cnf(f_80_5,plain,
( rR1(U_318,sK40(U_318))
| ~ cC48(U_318) ),
inference(clausify,[status(thm)],[f_80_4]) ).
cnf(f_80_6,plain,
( ~ cC16(sK40(U_318))
| ~ cC48(U_318) ),
inference(clausify,[status(thm)],[f_80_4]) ).
cnf(f_80_7,plain,
( cC48(U_319)
| cC16(U_316)
| ~ rR1(U_319,U_316) ),
inference(clausify,[status(thm)],[f_80_4]) ).
fof(f_81_1,plain,
! [X] :
( ( cC50(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_80]) ).
fof(f_81_2,plain,
! [U_322] :
( ( cC50(U_322)
| ! [U_321] :
( cC16(U_321)
| ~ rR1(U_322,U_321) ) )
& ( ? [U_320] :
( ~ cC16(U_320)
& rR1(U_322,U_320) )
| ~ cC50(U_322) ) ),
inference(variable_rename,[status(thm)],[f_81_1]) ).
fof(f_81_3,plain,
( ! [U_324] :
( cC50(U_324)
| ! [U_321] :
( cC16(U_321)
| ~ rR1(U_324,U_321) ) )
& ! [U_323] :
( ? [U_320] :
( ~ cC16(U_320)
& rR1(U_323,U_320) )
| ~ cC50(U_323) ) ),
inference(miniscope,[status(thm)],[f_81_2]) ).
fof(f_81_4,plain,
( ! [U_324] :
( cC50(U_324)
| ! [U_321] :
( cC16(U_321)
| ~ rR1(U_324,U_321) ) )
& ! [U_323] :
( ( ~ cC16(sK41(U_323))
& rR1(U_323,sK41(U_323)) )
| ~ cC50(U_323) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(U_320,sK41(U_323))],[f_81_3]) ).
cnf(f_81_5,plain,
( rR1(U_323,sK41(U_323))
| ~ cC50(U_323) ),
inference(clausify,[status(thm)],[f_81_4]) ).
cnf(f_81_6,plain,
( ~ cC16(sK41(U_323))
| ~ cC50(U_323) ),
inference(clausify,[status(thm)],[f_81_4]) ).
cnf(f_81_7,plain,
( cC50(U_324)
| cC16(U_321)
| ~ rR1(U_324,U_321) ),
inference(clausify,[status(thm)],[f_81_4]) ).
fof(f_82_1,plain,
! [X] :
( ( cC52(X)
| ~ cC16(X)
| ~ cC50(X) )
& ( ( cC16(X)
& cC50(X) )
| ~ cC52(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_81]) ).
fof(f_82_2,plain,
! [U_325] :
( ( cC52(U_325)
| ~ cC16(U_325)
| ~ cC50(U_325) )
& ( ( cC16(U_325)
& cC50(U_325) )
| ~ cC52(U_325) ) ),
inference(variable_rename,[status(thm)],[f_82_1]) ).
fof(f_82_3,plain,
( ! [U_327] :
( cC52(U_327)
| ~ cC16(U_327)
| ~ cC50(U_327) )
& ! [U_326] :
( ( cC16(U_326)
& cC50(U_326) )
| ~ cC52(U_326) ) ),
inference(miniscope,[status(thm)],[f_82_2]) ).
cnf(f_82_4,plain,
( cC50(U_326)
| ~ cC52(U_326) ),
inference(clausify,[status(thm)],[f_82_3]) ).
cnf(f_82_5,plain,
( cC16(U_326)
| ~ cC52(U_326) ),
inference(clausify,[status(thm)],[f_82_3]) ).
cnf(f_82_6,plain,
( cC52(U_327)
| ~ cC16(U_327)
| ~ cC50(U_327) ),
inference(clausify,[status(thm)],[f_82_3]) ).
fof(f_83_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_82]) ).
fof(f_83_2,plain,
! [U_330] :
( ( cC54(U_330)
| ! [U_329] :
( ~ cC52(U_329)
| ~ rR1(U_330,U_329) ) )
& ( ? [U_328] :
( cC52(U_328)
& rR1(U_330,U_328) )
| ~ cC54(U_330) ) ),
inference(variable_rename,[status(thm)],[f_83_1]) ).
fof(f_83_3,plain,
( ! [U_332] :
( cC54(U_332)
| ! [U_329] :
( ~ cC52(U_329)
| ~ rR1(U_332,U_329) ) )
& ! [U_331] :
( ? [U_328] :
( cC52(U_328)
& rR1(U_331,U_328) )
| ~ cC54(U_331) ) ),
inference(miniscope,[status(thm)],[f_83_2]) ).
fof(f_83_4,plain,
( ! [U_332] :
( cC54(U_332)
| ! [U_329] :
( ~ cC52(U_329)
| ~ rR1(U_332,U_329) ) )
& ! [U_331] :
( ( cC52(sK42(U_331))
& rR1(U_331,sK42(U_331)) )
| ~ cC54(U_331) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(U_328,sK42(U_331))],[f_83_3]) ).
cnf(f_83_5,plain,
( rR1(U_331,sK42(U_331))
| ~ cC54(U_331) ),
inference(clausify,[status(thm)],[f_83_4]) ).
cnf(f_83_6,plain,
( cC52(sK42(U_331))
| ~ cC54(U_331) ),
inference(clausify,[status(thm)],[f_83_4]) ).
cnf(f_83_7,plain,
( cC54(U_332)
| ~ cC52(U_329)
| ~ rR1(U_332,U_329) ),
inference(clausify,[status(thm)],[f_83_4]) ).
fof(f_84_1,plain,
! [X] :
( ( cC56(X)
| cC54(X)
| cC16(X) )
& ( ( ~ cC54(X)
& ~ cC16(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_83]) ).
fof(f_84_2,plain,
! [U_333] :
( ( cC56(U_333)
| cC54(U_333)
| cC16(U_333) )
& ( ( ~ cC54(U_333)
& ~ cC16(U_333) )
| ~ cC56(U_333) ) ),
inference(variable_rename,[status(thm)],[f_84_1]) ).
fof(f_84_3,plain,
( ! [U_335] :
( cC56(U_335)
| cC54(U_335)
| cC16(U_335) )
& ! [U_334] :
( ( ~ cC54(U_334)
& ~ cC16(U_334) )
| ~ cC56(U_334) ) ),
inference(miniscope,[status(thm)],[f_84_2]) ).
cnf(f_84_4,plain,
( ~ cC16(U_334)
| ~ cC56(U_334) ),
inference(clausify,[status(thm)],[f_84_3]) ).
cnf(f_84_5,plain,
( ~ cC54(U_334)
| ~ cC56(U_334) ),
inference(clausify,[status(thm)],[f_84_3]) ).
cnf(f_84_6,plain,
( cC56(U_335)
| cC54(U_335)
| cC16(U_335) ),
inference(clausify,[status(thm)],[f_84_3]) ).
fof(f_85_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_84]) ).
fof(f_85_2,plain,
! [U_338] :
( ( cC58(U_338)
| ! [U_337] :
( ~ cC56(U_337)
| ~ rR1(U_338,U_337) ) )
& ( ? [U_336] :
( cC56(U_336)
& rR1(U_338,U_336) )
| ~ cC58(U_338) ) ),
inference(variable_rename,[status(thm)],[f_85_1]) ).
fof(f_85_3,plain,
( ! [U_340] :
( cC58(U_340)
| ! [U_337] :
( ~ cC56(U_337)
| ~ rR1(U_340,U_337) ) )
& ! [U_339] :
( ? [U_336] :
( cC56(U_336)
& rR1(U_339,U_336) )
| ~ cC58(U_339) ) ),
inference(miniscope,[status(thm)],[f_85_2]) ).
fof(f_85_4,plain,
( ! [U_340] :
( cC58(U_340)
| ! [U_337] :
( ~ cC56(U_337)
| ~ rR1(U_340,U_337) ) )
& ! [U_339] :
( ( cC56(sK43(U_339))
& rR1(U_339,sK43(U_339)) )
| ~ cC58(U_339) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(U_336,sK43(U_339))],[f_85_3]) ).
cnf(f_85_5,plain,
( rR1(U_339,sK43(U_339))
| ~ cC58(U_339) ),
inference(clausify,[status(thm)],[f_85_4]) ).
cnf(f_85_6,plain,
( cC56(sK43(U_339))
| ~ cC58(U_339) ),
inference(clausify,[status(thm)],[f_85_4]) ).
cnf(f_85_7,plain,
( cC58(U_340)
| ~ cC56(U_337)
| ~ rR1(U_340,U_337) ),
inference(clausify,[status(thm)],[f_85_4]) ).
fof(f_86_1,plain,
! [X] :
( ( cC6(X)
| ~ cC4(X)
| ~ cC2(X) )
& ( ( cC4(X)
& cC2(X) )
| ~ cC6(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_85]) ).
fof(f_86_2,plain,
! [U_341] :
( ( cC6(U_341)
| ~ cC4(U_341)
| ~ cC2(U_341) )
& ( ( cC4(U_341)
& cC2(U_341) )
| ~ cC6(U_341) ) ),
inference(variable_rename,[status(thm)],[f_86_1]) ).
fof(f_86_3,plain,
( ! [U_343] :
( cC6(U_343)
| ~ cC4(U_343)
| ~ cC2(U_343) )
& ! [U_342] :
( ( cC4(U_342)
& cC2(U_342) )
| ~ cC6(U_342) ) ),
inference(miniscope,[status(thm)],[f_86_2]) ).
cnf(f_86_4,plain,
( cC2(U_342)
| ~ cC6(U_342) ),
inference(clausify,[status(thm)],[f_86_3]) ).
cnf(f_86_5,plain,
( cC4(U_342)
| ~ cC6(U_342) ),
inference(clausify,[status(thm)],[f_86_3]) ).
cnf(f_86_6,plain,
( cC6(U_343)
| ~ cC4(U_343)
| ~ cC2(U_343) ),
inference(clausify,[status(thm)],[f_86_3]) ).
fof(f_87_1,plain,
! [X] :
( ( cC60(X)
| cC58(X)
| ~ cC48(X) )
& ( ( ~ cC58(X)
& cC48(X) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_86]) ).
fof(f_87_2,plain,
! [U_344] :
( ( cC60(U_344)
| cC58(U_344)
| ~ cC48(U_344) )
& ( ( ~ cC58(U_344)
& cC48(U_344) )
| ~ cC60(U_344) ) ),
inference(variable_rename,[status(thm)],[f_87_1]) ).
fof(f_87_3,plain,
( ! [U_346] :
( cC60(U_346)
| cC58(U_346)
| ~ cC48(U_346) )
& ! [U_345] :
( ( ~ cC58(U_345)
& cC48(U_345) )
| ~ cC60(U_345) ) ),
inference(miniscope,[status(thm)],[f_87_2]) ).
cnf(f_87_4,plain,
( cC48(U_345)
| ~ cC60(U_345) ),
inference(clausify,[status(thm)],[f_87_3]) ).
cnf(f_87_5,plain,
( ~ cC58(U_345)
| ~ cC60(U_345) ),
inference(clausify,[status(thm)],[f_87_3]) ).
cnf(f_87_6,plain,
( cC60(U_346)
| cC58(U_346)
| ~ cC48(U_346) ),
inference(clausify,[status(thm)],[f_87_3]) ).
fof(f_88_1,plain,
! [X] :
( ( cC62(X)
| ! [Y] :
( ~ cC60(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC60(Y)
& rR1(X,Y) )
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_87]) ).
fof(f_88_2,plain,
! [U_349] :
( ( cC62(U_349)
| ! [U_348] :
( ~ cC60(U_348)
| ~ rR1(U_349,U_348) ) )
& ( ? [U_347] :
( cC60(U_347)
& rR1(U_349,U_347) )
| ~ cC62(U_349) ) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
fof(f_88_3,plain,
( ! [U_351] :
( cC62(U_351)
| ! [U_348] :
( ~ cC60(U_348)
| ~ rR1(U_351,U_348) ) )
& ! [U_350] :
( ? [U_347] :
( cC60(U_347)
& rR1(U_350,U_347) )
| ~ cC62(U_350) ) ),
inference(miniscope,[status(thm)],[f_88_2]) ).
fof(f_88_4,plain,
( ! [U_351] :
( cC62(U_351)
| ! [U_348] :
( ~ cC60(U_348)
| ~ rR1(U_351,U_348) ) )
& ! [U_350] :
( ( cC60(sK44(U_350))
& rR1(U_350,sK44(U_350)) )
| ~ cC62(U_350) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(U_347,sK44(U_350))],[f_88_3]) ).
cnf(f_88_5,plain,
( rR1(U_350,sK44(U_350))
| ~ cC62(U_350) ),
inference(clausify,[status(thm)],[f_88_4]) ).
cnf(f_88_6,plain,
( cC60(sK44(U_350))
| ~ cC62(U_350) ),
inference(clausify,[status(thm)],[f_88_4]) ).
cnf(f_88_7,plain,
( cC62(U_351)
| ~ cC60(U_348)
| ~ rR1(U_351,U_348) ),
inference(clausify,[status(thm)],[f_88_4]) ).
fof(f_89_1,plain,
! [X] :
( ( cC64(X)
| ~ cTOP(X)
| cC62(X) )
& ( ( cTOP(X)
& ~ cC62(X) )
| ~ cC64(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_88]) ).
fof(f_89_2,plain,
! [U_352] :
( ( cC64(U_352)
| ~ cTOP(U_352)
| cC62(U_352) )
& ( ( cTOP(U_352)
& ~ cC62(U_352) )
| ~ cC64(U_352) ) ),
inference(variable_rename,[status(thm)],[f_89_1]) ).
fof(f_89_3,plain,
( ! [U_354] :
( cC64(U_354)
| ~ cTOP(U_354)
| cC62(U_354) )
& ! [U_353] :
( ( cTOP(U_353)
& ~ cC62(U_353) )
| ~ cC64(U_353) ) ),
inference(miniscope,[status(thm)],[f_89_2]) ).
cnf(f_89_4,plain,
( ~ cC62(U_353)
| ~ cC64(U_353) ),
inference(clausify,[status(thm)],[f_89_3]) ).
cnf(f_89_5,plain,
( cTOP(U_353)
| ~ cC64(U_353) ),
inference(clausify,[status(thm)],[f_89_3]) ).
cnf(f_89_6,plain,
( cC64(U_354)
| ~ cTOP(U_354)
| cC62(U_354) ),
inference(clausify,[status(thm)],[f_89_3]) ).
fof(f_90_1,plain,
! [X] :
( ( cC66(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC66(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_89]) ).
fof(f_90_2,plain,
! [U_357] :
( ( cC66(U_357)
| ! [U_356] :
( cC16(U_356)
| ~ rR1(U_357,U_356) ) )
& ( ? [U_355] :
( ~ cC16(U_355)
& rR1(U_357,U_355) )
| ~ cC66(U_357) ) ),
inference(variable_rename,[status(thm)],[f_90_1]) ).
fof(f_90_3,plain,
( ! [U_359] :
( cC66(U_359)
| ! [U_356] :
( cC16(U_356)
| ~ rR1(U_359,U_356) ) )
& ! [U_358] :
( ? [U_355] :
( ~ cC16(U_355)
& rR1(U_358,U_355) )
| ~ cC66(U_358) ) ),
inference(miniscope,[status(thm)],[f_90_2]) ).
fof(f_90_4,plain,
( ! [U_359] :
( cC66(U_359)
| ! [U_356] :
( cC16(U_356)
| ~ rR1(U_359,U_356) ) )
& ! [U_358] :
( ( ~ cC16(sK45(U_358))
& rR1(U_358,sK45(U_358)) )
| ~ cC66(U_358) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(U_355,sK45(U_358))],[f_90_3]) ).
cnf(f_90_5,plain,
( rR1(U_358,sK45(U_358))
| ~ cC66(U_358) ),
inference(clausify,[status(thm)],[f_90_4]) ).
cnf(f_90_6,plain,
( ~ cC16(sK45(U_358))
| ~ cC66(U_358) ),
inference(clausify,[status(thm)],[f_90_4]) ).
cnf(f_90_7,plain,
( cC66(U_359)
| cC16(U_356)
| ~ rR1(U_359,U_356) ),
inference(clausify,[status(thm)],[f_90_4]) ).
fof(f_91_1,plain,
! [X] :
( ( cC68(X)
| ~ cC16(X)
| ~ cC66(X) )
& ( ( cC16(X)
& cC66(X) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_90]) ).
fof(f_91_2,plain,
! [U_360] :
( ( cC68(U_360)
| ~ cC16(U_360)
| ~ cC66(U_360) )
& ( ( cC16(U_360)
& cC66(U_360) )
| ~ cC68(U_360) ) ),
inference(variable_rename,[status(thm)],[f_91_1]) ).
fof(f_91_3,plain,
( ! [U_362] :
( cC68(U_362)
| ~ cC16(U_362)
| ~ cC66(U_362) )
& ! [U_361] :
( ( cC16(U_361)
& cC66(U_361) )
| ~ cC68(U_361) ) ),
inference(miniscope,[status(thm)],[f_91_2]) ).
cnf(f_91_4,plain,
( cC66(U_361)
| ~ cC68(U_361) ),
inference(clausify,[status(thm)],[f_91_3]) ).
cnf(f_91_5,plain,
( cC16(U_361)
| ~ cC68(U_361) ),
inference(clausify,[status(thm)],[f_91_3]) ).
cnf(f_91_6,plain,
( cC68(U_362)
| ~ cC16(U_362)
| ~ cC66(U_362) ),
inference(clausify,[status(thm)],[f_91_3]) ).
fof(f_92_1,plain,
! [X] :
( ( cC70(X)
| ! [Y] :
( ~ cC68(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC68(Y)
& rR1(X,Y) )
| ~ cC70(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_91]) ).
fof(f_92_2,plain,
! [U_365] :
( ( cC70(U_365)
| ! [U_364] :
( ~ cC68(U_364)
| ~ rR1(U_365,U_364) ) )
& ( ? [U_363] :
( cC68(U_363)
& rR1(U_365,U_363) )
| ~ cC70(U_365) ) ),
inference(variable_rename,[status(thm)],[f_92_1]) ).
fof(f_92_3,plain,
( ! [U_367] :
( cC70(U_367)
| ! [U_364] :
( ~ cC68(U_364)
| ~ rR1(U_367,U_364) ) )
& ! [U_366] :
( ? [U_363] :
( cC68(U_363)
& rR1(U_366,U_363) )
| ~ cC70(U_366) ) ),
inference(miniscope,[status(thm)],[f_92_2]) ).
fof(f_92_4,plain,
( ! [U_367] :
( cC70(U_367)
| ! [U_364] :
( ~ cC68(U_364)
| ~ rR1(U_367,U_364) ) )
& ! [U_366] :
( ( cC68(sK46(U_366))
& rR1(U_366,sK46(U_366)) )
| ~ cC70(U_366) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(U_363,sK46(U_366))],[f_92_3]) ).
cnf(f_92_5,plain,
( rR1(U_366,sK46(U_366))
| ~ cC70(U_366) ),
inference(clausify,[status(thm)],[f_92_4]) ).
cnf(f_92_6,plain,
( cC68(sK46(U_366))
| ~ cC70(U_366) ),
inference(clausify,[status(thm)],[f_92_4]) ).
cnf(f_92_7,plain,
( cC70(U_367)
| ~ cC68(U_364)
| ~ rR1(U_367,U_364) ),
inference(clausify,[status(thm)],[f_92_4]) ).
fof(f_93_1,plain,
! [X] :
( ( cC72(X)
| cC16(X)
| cC70(X) )
& ( ( ~ cC16(X)
& ~ cC70(X) )
| ~ cC72(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_92]) ).
fof(f_93_2,plain,
! [U_368] :
( ( cC72(U_368)
| cC16(U_368)
| cC70(U_368) )
& ( ( ~ cC16(U_368)
& ~ cC70(U_368) )
| ~ cC72(U_368) ) ),
inference(variable_rename,[status(thm)],[f_93_1]) ).
fof(f_93_3,plain,
( ! [U_370] :
( cC72(U_370)
| cC16(U_370)
| cC70(U_370) )
& ! [U_369] :
( ( ~ cC16(U_369)
& ~ cC70(U_369) )
| ~ cC72(U_369) ) ),
inference(miniscope,[status(thm)],[f_93_2]) ).
cnf(f_93_4,plain,
( ~ cC70(U_369)
| ~ cC72(U_369) ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_5,plain,
( ~ cC16(U_369)
| ~ cC72(U_369) ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_6,plain,
( cC72(U_370)
| cC16(U_370)
| cC70(U_370) ),
inference(clausify,[status(thm)],[f_93_3]) ).
fof(f_94_1,plain,
! [X] :
( ( cC74(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC74(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_93]) ).
fof(f_94_2,plain,
! [U_373] :
( ( cC74(U_373)
| ! [U_372] :
( cC16(U_372)
| ~ rR1(U_373,U_372) ) )
& ( ? [U_371] :
( ~ cC16(U_371)
& rR1(U_373,U_371) )
| ~ cC74(U_373) ) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
fof(f_94_3,plain,
( ! [U_375] :
( cC74(U_375)
| ! [U_372] :
( cC16(U_372)
| ~ rR1(U_375,U_372) ) )
& ! [U_374] :
( ? [U_371] :
( ~ cC16(U_371)
& rR1(U_374,U_371) )
| ~ cC74(U_374) ) ),
inference(miniscope,[status(thm)],[f_94_2]) ).
fof(f_94_4,plain,
( ! [U_375] :
( cC74(U_375)
| ! [U_372] :
( cC16(U_372)
| ~ rR1(U_375,U_372) ) )
& ! [U_374] :
( ( ~ cC16(sK47(U_374))
& rR1(U_374,sK47(U_374)) )
| ~ cC74(U_374) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(U_371,sK47(U_374))],[f_94_3]) ).
cnf(f_94_5,plain,
( rR1(U_374,sK47(U_374))
| ~ cC74(U_374) ),
inference(clausify,[status(thm)],[f_94_4]) ).
cnf(f_94_6,plain,
( ~ cC16(sK47(U_374))
| ~ cC74(U_374) ),
inference(clausify,[status(thm)],[f_94_4]) ).
cnf(f_94_7,plain,
( cC74(U_375)
| cC16(U_372)
| ~ rR1(U_375,U_372) ),
inference(clausify,[status(thm)],[f_94_4]) ).
fof(f_95_1,plain,
! [X] :
( ( cC76(X)
| ~ cC16(X)
| ~ cC74(X) )
& ( ( cC16(X)
& cC74(X) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_94]) ).
fof(f_95_2,plain,
! [U_376] :
( ( cC76(U_376)
| ~ cC16(U_376)
| ~ cC74(U_376) )
& ( ( cC16(U_376)
& cC74(U_376) )
| ~ cC76(U_376) ) ),
inference(variable_rename,[status(thm)],[f_95_1]) ).
fof(f_95_3,plain,
( ! [U_378] :
( cC76(U_378)
| ~ cC16(U_378)
| ~ cC74(U_378) )
& ! [U_377] :
( ( cC16(U_377)
& cC74(U_377) )
| ~ cC76(U_377) ) ),
inference(miniscope,[status(thm)],[f_95_2]) ).
cnf(f_95_4,plain,
( cC74(U_377)
| ~ cC76(U_377) ),
inference(clausify,[status(thm)],[f_95_3]) ).
cnf(f_95_5,plain,
( cC16(U_377)
| ~ cC76(U_377) ),
inference(clausify,[status(thm)],[f_95_3]) ).
cnf(f_95_6,plain,
( cC76(U_378)
| ~ cC16(U_378)
| ~ cC74(U_378) ),
inference(clausify,[status(thm)],[f_95_3]) ).
fof(f_96_1,plain,
! [X] :
( ( cC78(X)
| ! [Y] :
( ~ cC76(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC76(Y)
& rR1(X,Y) )
| ~ cC78(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_95]) ).
fof(f_96_2,plain,
! [U_381] :
( ( cC78(U_381)
| ! [U_380] :
( ~ cC76(U_380)
| ~ rR1(U_381,U_380) ) )
& ( ? [U_379] :
( cC76(U_379)
& rR1(U_381,U_379) )
| ~ cC78(U_381) ) ),
inference(variable_rename,[status(thm)],[f_96_1]) ).
fof(f_96_3,plain,
( ! [U_383] :
( cC78(U_383)
| ! [U_380] :
( ~ cC76(U_380)
| ~ rR1(U_383,U_380) ) )
& ! [U_382] :
( ? [U_379] :
( cC76(U_379)
& rR1(U_382,U_379) )
| ~ cC78(U_382) ) ),
inference(miniscope,[status(thm)],[f_96_2]) ).
fof(f_96_4,plain,
( ! [U_383] :
( cC78(U_383)
| ! [U_380] :
( ~ cC76(U_380)
| ~ rR1(U_383,U_380) ) )
& ! [U_382] :
( ( cC76(sK48(U_382))
& rR1(U_382,sK48(U_382)) )
| ~ cC78(U_382) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(U_379,sK48(U_382))],[f_96_3]) ).
cnf(f_96_5,plain,
( rR1(U_382,sK48(U_382))
| ~ cC78(U_382) ),
inference(clausify,[status(thm)],[f_96_4]) ).
cnf(f_96_6,plain,
( cC76(sK48(U_382))
| ~ cC78(U_382) ),
inference(clausify,[status(thm)],[f_96_4]) ).
cnf(f_96_7,plain,
( cC78(U_383)
| ~ cC76(U_380)
| ~ rR1(U_383,U_380) ),
inference(clausify,[status(thm)],[f_96_4]) ).
fof(f_97_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_96]) ).
fof(f_97_2,plain,
! [U_386] :
( ( cC8(U_386)
| ! [U_385] :
( ~ cC6(U_385)
| ~ rR1(U_386,U_385) ) )
& ( ? [U_384] :
( cC6(U_384)
& rR1(U_386,U_384) )
| ~ cC8(U_386) ) ),
inference(variable_rename,[status(thm)],[f_97_1]) ).
fof(f_97_3,plain,
( ! [U_388] :
( cC8(U_388)
| ! [U_385] :
( ~ cC6(U_385)
| ~ rR1(U_388,U_385) ) )
& ! [U_387] :
( ? [U_384] :
( cC6(U_384)
& rR1(U_387,U_384) )
| ~ cC8(U_387) ) ),
inference(miniscope,[status(thm)],[f_97_2]) ).
fof(f_97_4,plain,
( ! [U_388] :
( cC8(U_388)
| ! [U_385] :
( ~ cC6(U_385)
| ~ rR1(U_388,U_385) ) )
& ! [U_387] :
( ( cC6(sK49(U_387))
& rR1(U_387,sK49(U_387)) )
| ~ cC8(U_387) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_384,sK49(U_387))],[f_97_3]) ).
cnf(f_97_5,plain,
( rR1(U_387,sK49(U_387))
| ~ cC8(U_387) ),
inference(clausify,[status(thm)],[f_97_4]) ).
cnf(f_97_6,plain,
( cC6(sK49(U_387))
| ~ cC8(U_387) ),
inference(clausify,[status(thm)],[f_97_4]) ).
cnf(f_97_7,plain,
( cC8(U_388)
| ~ cC6(U_385)
| ~ rR1(U_388,U_385) ),
inference(clausify,[status(thm)],[f_97_4]) ).
fof(f_98_1,plain,
! [X] :
( ( cC80(X)
| cC78(X)
| cC16(X) )
& ( ( ~ cC78(X)
& ~ cC16(X) )
| ~ cC80(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_97]) ).
fof(f_98_2,plain,
! [U_389] :
( ( cC80(U_389)
| cC78(U_389)
| cC16(U_389) )
& ( ( ~ cC78(U_389)
& ~ cC16(U_389) )
| ~ cC80(U_389) ) ),
inference(variable_rename,[status(thm)],[f_98_1]) ).
fof(f_98_3,plain,
( ! [U_391] :
( cC80(U_391)
| cC78(U_391)
| cC16(U_391) )
& ! [U_390] :
( ( ~ cC78(U_390)
& ~ cC16(U_390) )
| ~ cC80(U_390) ) ),
inference(miniscope,[status(thm)],[f_98_2]) ).
cnf(f_98_4,plain,
( ~ cC16(U_390)
| ~ cC80(U_390) ),
inference(clausify,[status(thm)],[f_98_3]) ).
cnf(f_98_5,plain,
( ~ cC78(U_390)
| ~ cC80(U_390) ),
inference(clausify,[status(thm)],[f_98_3]) ).
cnf(f_98_6,plain,
( cC80(U_391)
| cC78(U_391)
| cC16(U_391) ),
inference(clausify,[status(thm)],[f_98_3]) ).
fof(f_99_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_98]) ).
fof(f_99_2,plain,
! [U_394] :
( ( cC82(U_394)
| ! [U_393] :
( ~ cC80(U_393)
| ~ rR1(U_394,U_393) ) )
& ( ? [U_392] :
( cC80(U_392)
& rR1(U_394,U_392) )
| ~ cC82(U_394) ) ),
inference(variable_rename,[status(thm)],[f_99_1]) ).
fof(f_99_3,plain,
( ! [U_396] :
( cC82(U_396)
| ! [U_393] :
( ~ cC80(U_393)
| ~ rR1(U_396,U_393) ) )
& ! [U_395] :
( ? [U_392] :
( cC80(U_392)
& rR1(U_395,U_392) )
| ~ cC82(U_395) ) ),
inference(miniscope,[status(thm)],[f_99_2]) ).
fof(f_99_4,plain,
( ! [U_396] :
( cC82(U_396)
| ! [U_393] :
( ~ cC80(U_393)
| ~ rR1(U_396,U_393) ) )
& ! [U_395] :
( ( cC80(sK50(U_395))
& rR1(U_395,sK50(U_395)) )
| ~ cC82(U_395) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_392,sK50(U_395))],[f_99_3]) ).
cnf(f_99_5,plain,
( rR1(U_395,sK50(U_395))
| ~ cC82(U_395) ),
inference(clausify,[status(thm)],[f_99_4]) ).
cnf(f_99_6,plain,
( cC80(sK50(U_395))
| ~ cC82(U_395) ),
inference(clausify,[status(thm)],[f_99_4]) ).
cnf(f_99_7,plain,
( cC82(U_396)
| ~ cC80(U_393)
| ~ rR1(U_396,U_393) ),
inference(clausify,[status(thm)],[f_99_4]) ).
fof(f_100_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_99]) ).
fof(f_100_2,plain,
! [U_399] :
( ( cC84(U_399)
| ! [U_398] :
( ~ cC82(U_398)
| ~ rR1(U_399,U_398) ) )
& ( ? [U_397] :
( cC82(U_397)
& rR1(U_399,U_397) )
| ~ cC84(U_399) ) ),
inference(variable_rename,[status(thm)],[f_100_1]) ).
fof(f_100_3,plain,
( ! [U_401] :
( cC84(U_401)
| ! [U_398] :
( ~ cC82(U_398)
| ~ rR1(U_401,U_398) ) )
& ! [U_400] :
( ? [U_397] :
( cC82(U_397)
& rR1(U_400,U_397) )
| ~ cC84(U_400) ) ),
inference(miniscope,[status(thm)],[f_100_2]) ).
fof(f_100_4,plain,
( ! [U_401] :
( cC84(U_401)
| ! [U_398] :
( ~ cC82(U_398)
| ~ rR1(U_401,U_398) ) )
& ! [U_400] :
( ( cC82(sK51(U_400))
& rR1(U_400,sK51(U_400)) )
| ~ cC84(U_400) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_397,sK51(U_400))],[f_100_3]) ).
cnf(f_100_5,plain,
( rR1(U_400,sK51(U_400))
| ~ cC84(U_400) ),
inference(clausify,[status(thm)],[f_100_4]) ).
cnf(f_100_6,plain,
( cC82(sK51(U_400))
| ~ cC84(U_400) ),
inference(clausify,[status(thm)],[f_100_4]) ).
cnf(f_100_7,plain,
( cC84(U_401)
| ~ cC82(U_398)
| ~ rR1(U_401,U_398) ),
inference(clausify,[status(thm)],[f_100_4]) ).
fof(f_101_1,plain,
! [X] :
( ( cC86(X)
| ! [Y] :
( cC16(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC16(Y)
& rR1(X,Y) )
| ~ cC86(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_100]) ).
fof(f_101_2,plain,
! [U_404] :
( ( cC86(U_404)
| ! [U_403] :
( cC16(U_403)
| ~ rR1(U_404,U_403) ) )
& ( ? [U_402] :
( ~ cC16(U_402)
& rR1(U_404,U_402) )
| ~ cC86(U_404) ) ),
inference(variable_rename,[status(thm)],[f_101_1]) ).
fof(f_101_3,plain,
( ! [U_406] :
( cC86(U_406)
| ! [U_403] :
( cC16(U_403)
| ~ rR1(U_406,U_403) ) )
& ! [U_405] :
( ? [U_402] :
( ~ cC16(U_402)
& rR1(U_405,U_402) )
| ~ cC86(U_405) ) ),
inference(miniscope,[status(thm)],[f_101_2]) ).
fof(f_101_4,plain,
( ! [U_406] :
( cC86(U_406)
| ! [U_403] :
( cC16(U_403)
| ~ rR1(U_406,U_403) ) )
& ! [U_405] :
( ( ~ cC16(sK52(U_405))
& rR1(U_405,sK52(U_405)) )
| ~ cC86(U_405) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(U_402,sK52(U_405))],[f_101_3]) ).
cnf(f_101_5,plain,
( rR1(U_405,sK52(U_405))
| ~ cC86(U_405) ),
inference(clausify,[status(thm)],[f_101_4]) ).
cnf(f_101_6,plain,
( ~ cC16(sK52(U_405))
| ~ cC86(U_405) ),
inference(clausify,[status(thm)],[f_101_4]) ).
cnf(f_101_7,plain,
( cC86(U_406)
| cC16(U_403)
| ~ rR1(U_406,U_403) ),
inference(clausify,[status(thm)],[f_101_4]) ).
fof(f_102_1,plain,
! [X] :
( ( cC88(X)
| ~ cC16(X)
| ~ cC86(X) )
& ( ( cC16(X)
& cC86(X) )
| ~ cC88(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_101]) ).
fof(f_102_2,plain,
! [U_407] :
( ( cC88(U_407)
| ~ cC16(U_407)
| ~ cC86(U_407) )
& ( ( cC16(U_407)
& cC86(U_407) )
| ~ cC88(U_407) ) ),
inference(variable_rename,[status(thm)],[f_102_1]) ).
fof(f_102_3,plain,
( ! [U_409] :
( cC88(U_409)
| ~ cC16(U_409)
| ~ cC86(U_409) )
& ! [U_408] :
( ( cC16(U_408)
& cC86(U_408) )
| ~ cC88(U_408) ) ),
inference(miniscope,[status(thm)],[f_102_2]) ).
cnf(f_102_4,plain,
( cC86(U_408)
| ~ cC88(U_408) ),
inference(clausify,[status(thm)],[f_102_3]) ).
cnf(f_102_5,plain,
( cC16(U_408)
| ~ cC88(U_408) ),
inference(clausify,[status(thm)],[f_102_3]) ).
cnf(f_102_6,plain,
( cC88(U_409)
| ~ cC16(U_409)
| ~ cC86(U_409) ),
inference(clausify,[status(thm)],[f_102_3]) ).
fof(f_103_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_102]) ).
fof(f_103_2,plain,
! [U_412] :
( ( cC90(U_412)
| ! [U_411] :
( ~ cC88(U_411)
| ~ rR1(U_412,U_411) ) )
& ( ? [U_410] :
( cC88(U_410)
& rR1(U_412,U_410) )
| ~ cC90(U_412) ) ),
inference(variable_rename,[status(thm)],[f_103_1]) ).
fof(f_103_3,plain,
( ! [U_414] :
( cC90(U_414)
| ! [U_411] :
( ~ cC88(U_411)
| ~ rR1(U_414,U_411) ) )
& ! [U_413] :
( ? [U_410] :
( cC88(U_410)
& rR1(U_413,U_410) )
| ~ cC90(U_413) ) ),
inference(miniscope,[status(thm)],[f_103_2]) ).
fof(f_103_4,plain,
( ! [U_414] :
( cC90(U_414)
| ! [U_411] :
( ~ cC88(U_411)
| ~ rR1(U_414,U_411) ) )
& ! [U_413] :
( ( cC88(sK53(U_413))
& rR1(U_413,sK53(U_413)) )
| ~ cC90(U_413) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(U_410,sK53(U_413))],[f_103_3]) ).
cnf(f_103_5,plain,
( rR1(U_413,sK53(U_413))
| ~ cC90(U_413) ),
inference(clausify,[status(thm)],[f_103_4]) ).
cnf(f_103_6,plain,
( cC88(sK53(U_413))
| ~ cC90(U_413) ),
inference(clausify,[status(thm)],[f_103_4]) ).
cnf(f_103_7,plain,
( cC90(U_414)
| ~ cC88(U_411)
| ~ rR1(U_414,U_411) ),
inference(clausify,[status(thm)],[f_103_4]) ).
fof(f_104_1,plain,
! [X] :
( ( cC92(X)
| cC16(X)
| cC90(X) )
& ( ( ~ cC16(X)
& ~ cC90(X) )
| ~ cC92(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_103]) ).
fof(f_104_2,plain,
! [U_415] :
( ( cC92(U_415)
| cC16(U_415)
| cC90(U_415) )
& ( ( ~ cC16(U_415)
& ~ cC90(U_415) )
| ~ cC92(U_415) ) ),
inference(variable_rename,[status(thm)],[f_104_1]) ).
fof(f_104_3,plain,
( ! [U_417] :
( cC92(U_417)
| cC16(U_417)
| cC90(U_417) )
& ! [U_416] :
( ( ~ cC16(U_416)
& ~ cC90(U_416) )
| ~ cC92(U_416) ) ),
inference(miniscope,[status(thm)],[f_104_2]) ).
cnf(f_104_4,plain,
( ~ cC90(U_416)
| ~ cC92(U_416) ),
inference(clausify,[status(thm)],[f_104_3]) ).
cnf(f_104_5,plain,
( ~ cC16(U_416)
| ~ cC92(U_416) ),
inference(clausify,[status(thm)],[f_104_3]) ).
cnf(f_104_6,plain,
( cC92(U_417)
| cC16(U_417)
| cC90(U_417) ),
inference(clausify,[status(thm)],[f_104_3]) ).
fof(f_105_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_104]) ).
fof(f_105_2,plain,
! [U_420] :
( ( cC94(U_420)
| ! [U_419] :
( ~ cC92(U_419)
| ~ rR1(U_420,U_419) ) )
& ( ? [U_418] :
( cC92(U_418)
& rR1(U_420,U_418) )
| ~ cC94(U_420) ) ),
inference(variable_rename,[status(thm)],[f_105_1]) ).
fof(f_105_3,plain,
( ! [U_422] :
( cC94(U_422)
| ! [U_419] :
( ~ cC92(U_419)
| ~ rR1(U_422,U_419) ) )
& ! [U_421] :
( ? [U_418] :
( cC92(U_418)
& rR1(U_421,U_418) )
| ~ cC94(U_421) ) ),
inference(miniscope,[status(thm)],[f_105_2]) ).
fof(f_105_4,plain,
( ! [U_422] :
( cC94(U_422)
| ! [U_419] :
( ~ cC92(U_419)
| ~ rR1(U_422,U_419) ) )
& ! [U_421] :
( ( cC92(sK54(U_421))
& rR1(U_421,sK54(U_421)) )
| ~ cC94(U_421) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(U_418,sK54(U_421))],[f_105_3]) ).
cnf(f_105_5,plain,
( rR1(U_421,sK54(U_421))
| ~ cC94(U_421) ),
inference(clausify,[status(thm)],[f_105_4]) ).
cnf(f_105_6,plain,
( cC92(sK54(U_421))
| ~ cC94(U_421) ),
inference(clausify,[status(thm)],[f_105_4]) ).
cnf(f_105_7,plain,
( cC94(U_422)
| ~ cC92(U_419)
| ~ rR1(U_422,U_419) ),
inference(clausify,[status(thm)],[f_105_4]) ).
fof(f_106_1,plain,
! [X] :
( ( cC96(X)
| cC94(X)
| ~ cC84(X) )
& ( ( ~ cC94(X)
& cC84(X) )
| ~ cC96(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_105]) ).
fof(f_106_2,plain,
! [U_423] :
( ( cC96(U_423)
| cC94(U_423)
| ~ cC84(U_423) )
& ( ( ~ cC94(U_423)
& cC84(U_423) )
| ~ cC96(U_423) ) ),
inference(variable_rename,[status(thm)],[f_106_1]) ).
fof(f_106_3,plain,
( ! [U_425] :
( cC96(U_425)
| cC94(U_425)
| ~ cC84(U_425) )
& ! [U_424] :
( ( ~ cC94(U_424)
& cC84(U_424) )
| ~ cC96(U_424) ) ),
inference(miniscope,[status(thm)],[f_106_2]) ).
cnf(f_106_4,plain,
( cC84(U_424)
| ~ cC96(U_424) ),
inference(clausify,[status(thm)],[f_106_3]) ).
cnf(f_106_5,plain,
( ~ cC94(U_424)
| ~ cC96(U_424) ),
inference(clausify,[status(thm)],[f_106_3]) ).
cnf(f_106_6,plain,
( cC96(U_425)
| cC94(U_425)
| ~ cC84(U_425) ),
inference(clausify,[status(thm)],[f_106_3]) ).
fof(f_107_1,plain,
! [X] :
( ( cC98(X)
| cC96(X)
| cC72(X) )
& ( ( ~ cC96(X)
& ~ cC72(X) )
| ~ cC98(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_106]) ).
fof(f_107_2,plain,
! [U_426] :
( ( cC98(U_426)
| cC96(U_426)
| cC72(U_426) )
& ( ( ~ cC96(U_426)
& ~ cC72(U_426) )
| ~ cC98(U_426) ) ),
inference(variable_rename,[status(thm)],[f_107_1]) ).
fof(f_107_3,plain,
( ! [U_428] :
( cC98(U_428)
| cC96(U_428)
| cC72(U_428) )
& ! [U_427] :
( ( ~ cC96(U_427)
& ~ cC72(U_427) )
| ~ cC98(U_427) ) ),
inference(miniscope,[status(thm)],[f_107_2]) ).
cnf(f_107_4,plain,
( ~ cC72(U_427)
| ~ cC98(U_427) ),
inference(clausify,[status(thm)],[f_107_3]) ).
cnf(f_107_5,plain,
( ~ cC96(U_427)
| ~ cC98(U_427) ),
inference(clausify,[status(thm)],[f_107_3]) ).
cnf(f_107_6,plain,
( cC98(U_428)
| cC96(U_428)
| cC72(U_428) ),
inference(clausify,[status(thm)],[f_107_3]) ).
fof(f_108_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC46(X)
| ~ cC216(X) )
& ( ( cC46(X)
& cC216(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_107]) ).
fof(f_108_2,plain,
! [U_429] :
( ( cTEST(U_429)
| ~ cC46(U_429)
| ~ cC216(U_429) )
& ( ( cC46(U_429)
& cC216(U_429) )
| ~ cTEST(U_429) ) ),
inference(variable_rename,[status(thm)],[f_108_1]) ).
fof(f_108_3,plain,
( ! [U_431] :
( cTEST(U_431)
| ~ cC46(U_431)
| ~ cC216(U_431) )
& ! [U_430] :
( ( cC46(U_430)
& cC216(U_430) )
| ~ cTEST(U_430) ) ),
inference(miniscope,[status(thm)],[f_108_2]) ).
cnf(f_108_4,plain,
( cC216(U_430)
| ~ cTEST(U_430) ),
inference(clausify,[status(thm)],[f_108_3]) ).
cnf(f_108_5,plain,
( cC46(U_430)
| ~ cTEST(U_430) ),
inference(clausify,[status(thm)],[f_108_3]) ).
cnf(f_108_6,plain,
( cTEST(U_431)
| ~ cC46(U_431)
| ~ cC216(U_431) ),
inference(clausify,[status(thm)],[f_108_3]) ).
fof(f_109_1,plain,
cTEST(iV3102),
inference(fof_nnf,[status(thm)],[axiom_108]) ).
cnf(f_109_2,plain,
cTEST(iV3102),
inference(clausify,[status(thm)],[f_109_1]) ).
fof(f_110_1,plain,
cowlThing(iV3102),
inference(fof_nnf,[status(thm)],[axiom_109]) ).
cnf(f_110_2,plain,
cowlThing(iV3102),
inference(clausify,[status(thm)],[f_110_1]) ).
fof(f_111_1,plain,
! [X] :
( ~ cC60(X)
| ~ rR1(iV3102,X) ),
inference(fof_nnf,[status(thm)],[axiom_110]) ).
fof(f_111_2,plain,
! [U_432] :
( ~ cC60(U_432)
| ~ rR1(iV3102,U_432) ),
inference(variable_rename,[status(thm)],[f_111_1]) ).
cnf(f_111_3,plain,
( ~ cC60(U_432)
| ~ rR1(iV3102,U_432) ),
inference(clausify,[status(thm)],[f_111_2]) ).
fof(f_112_1,plain,
! [X] :
( ~ cC10(X)
| ~ rR1(iV3102,X) ),
inference(fof_nnf,[status(thm)],[axiom_111]) ).
fof(f_112_2,plain,
! [U_433] :
( ~ cC10(U_433)
| ~ rR1(iV3102,U_433) ),
inference(variable_rename,[status(thm)],[f_112_1]) ).
cnf(f_112_3,plain,
( ~ cC10(U_433)
| ~ rR1(iV3102,U_433) ),
inference(clausify,[status(thm)],[f_112_2]) ).
fof(f_113_1,plain,
cTOP(iV3102),
inference(fof_nnf,[status(thm)],[axiom_112]) ).
cnf(f_113_2,plain,
cTOP(iV3102),
inference(clausify,[status(thm)],[f_113_1]) ).
fof(f_114_1,plain,
! [X] :
( ~ cC24(X)
| ~ rR1(iV3102,X) ),
inference(fof_nnf,[status(thm)],[axiom_113]) ).
fof(f_114_2,plain,
! [U_434] :
( ~ cC24(U_434)
| ~ rR1(iV3102,U_434) ),
inference(variable_rename,[status(thm)],[f_114_1]) ).
cnf(f_114_3,plain,
( ~ cC24(U_434)
| ~ rR1(iV3102,U_434) ),
inference(clausify,[status(thm)],[f_114_2]) ).
fof(f_115_1,plain,
~ cC42(iV3102),
inference(fof_nnf,[status(thm)],[axiom_114]) ).
cnf(f_115_2,plain,
~ cC42(iV3102),
inference(clausify,[status(thm)],[f_115_1]) ).
fof(f_116_1,plain,
~ cC12(iV3102),
inference(fof_nnf,[status(thm)],[axiom_115]) ).
cnf(f_116_2,plain,
~ cC12(iV3102),
inference(clausify,[status(thm)],[f_116_1]) ).
fof(f_117_1,plain,
~ cC26(iV3102),
inference(fof_nnf,[status(thm)],[axiom_116]) ).
cnf(f_117_2,plain,
~ cC26(iV3102),
inference(clausify,[status(thm)],[f_117_1]) ).
fof(f_118_1,plain,
! [X] :
( cC98(X)
| ~ rR1(iV3102,X) ),
inference(fof_nnf,[status(thm)],[axiom_117]) ).
fof(f_118_2,plain,
! [U_435] :
( cC98(U_435)
| ~ rR1(iV3102,U_435) ),
inference(variable_rename,[status(thm)],[f_118_1]) ).
cnf(f_118_3,plain,
( cC98(U_435)
| ~ rR1(iV3102,U_435) ),
inference(clausify,[status(thm)],[f_118_2]) ).
fof(f_119_1,plain,
~ cC214(iV3102),
inference(fof_nnf,[status(thm)],[axiom_118]) ).
cnf(f_119_2,plain,
~ cC214(iV3102),
inference(clausify,[status(thm)],[f_119_1]) ).
fof(f_120_1,plain,
~ cC62(iV3102),
inference(fof_nnf,[status(thm)],[axiom_119]) ).
cnf(f_120_2,plain,
~ cC62(iV3102),
inference(clausify,[status(thm)],[f_120_1]) ).
fof(f_121_1,plain,
! [X] :
( ~ cC40(X)
| ~ rR1(iV3102,X) ),
inference(fof_nnf,[status(thm)],[axiom_120]) ).
fof(f_121_2,plain,
! [U_436] :
( ~ cC40(U_436)
| ~ rR1(iV3102,U_436) ),
inference(variable_rename,[status(thm)],[f_121_1]) ).
cnf(f_121_3,plain,
( ~ cC40(U_436)
| ~ rR1(iV3102,U_436) ),
inference(clausify,[status(thm)],[f_121_2]) ).
fof(f_122_1,plain,
~ cC16(iV3102),
inference(fof_nnf,[status(thm)],[axiom_121]) ).
cnf(f_122_2,plain,
~ cC16(iV3102),
inference(clausify,[status(thm)],[f_122_1]) ).
fof(f_123_1,plain,
~ cC2(iV3102),
inference(fof_nnf,[status(thm)],[axiom_122]) ).
cnf(f_123_2,plain,
~ cC2(iV3102),
inference(clausify,[status(thm)],[f_123_1]) ).
fof(f_124_1,plain,
~ cC32(iV3102),
inference(fof_nnf,[status(thm)],[axiom_123]) ).
cnf(f_124_2,plain,
~ cC32(iV3102),
inference(clausify,[status(thm)],[f_124_1]) ).
fof(f_125_1,plain,
~ cC100(iV3102),
inference(fof_nnf,[status(thm)],[axiom_124]) ).
cnf(f_125_2,plain,
~ cC100(iV3102),
inference(clausify,[status(thm)],[f_125_1]) ).
fof(f_126_1,negated_conjecture,
~ ( cowlThing(iV3102)
& cC14(iV3102)
& cC64(iV3102)
& cC28(iV3102)
& cC44(iV3102)
& cC30(iV3102)
& cC46(iV3102)
& cC216(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_126_2,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_126_1]) ).
fof(f_126_3,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [U_438] :
( ( ~ xsd_string(U_438)
& ~ xsd_integer(U_438) )
| ( xsd_integer(U_438)
& xsd_string(U_438) ) )
| ? [U_437] :
( cowlNothing(U_437)
| ~ cowlThing(U_437) ) ),
inference(variable_rename,[status(thm)],[f_126_2]) ).
fof(f_126_4,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [U_442] :
( ~ xsd_string(U_442)
& ~ xsd_integer(U_442) )
| ? [U_441] :
( xsd_integer(U_441)
& xsd_string(U_441) )
| ? [U_440] : cowlNothing(U_440)
| ? [U_439] : ~ cowlThing(U_439) ),
inference(miniscope,[status(thm)],[f_126_3]) ).
fof(f_126_5,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [U_442] :
( ~ xsd_string(U_442)
& ~ xsd_integer(U_442) )
| ? [U_441] :
( xsd_integer(U_441)
& xsd_string(U_441) )
| ? [U_440] : cowlNothing(U_440)
| ~ cowlThing(sK55) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(U_439,sK55)],[f_126_4]) ).
fof(f_126_6,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [U_442] :
( ~ xsd_string(U_442)
& ~ xsd_integer(U_442) )
| ? [U_441] :
( xsd_integer(U_441)
& xsd_string(U_441) )
| cowlNothing(sK56)
| ~ cowlThing(sK55) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(U_440,sK56)],[f_126_5]) ).
fof(f_126_7,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [U_442] :
( ~ xsd_string(U_442)
& ~ xsd_integer(U_442) )
| ( xsd_integer(sK57)
& xsd_string(sK57) )
| cowlNothing(sK56)
| ~ cowlThing(sK55) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(U_441,sK57)],[f_126_6]) ).
fof(f_126_8,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ( ~ xsd_string(sK58)
& ~ xsd_integer(sK58) )
| ( xsd_integer(sK57)
& xsd_string(sK57) )
| cowlNothing(sK56)
| ~ cowlThing(sK55) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(U_442,sK58)],[f_126_7]) ).
fof(f_126_9,negated_conjecture,
( ( ~ xsd_string(sK58)
| ~ sP1 )
& ( ~ xsd_integer(sK58)
| ~ sP1 )
& ( xsd_integer(sK57)
| ~ sP0 )
& ( xsd_string(sK57)
| ~ sP0 )
& ( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| sP1
| sP0
| cowlNothing(sK56)
| ~ cowlThing(sK55) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_126_8]) ).
cnf(f_126_10,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| sP1
| sP0
| cowlNothing(sK56)
| ~ cowlThing(sK55) ),
inference(clausify,[status(thm)],[f_126_9]) ).
cnf(f_126_11,negated_conjecture,
( xsd_string(sK57)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_126_9]) ).
cnf(f_126_12,negated_conjecture,
( xsd_integer(sK57)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_126_9]) ).
cnf(f_126_13,negated_conjecture,
( ~ xsd_integer(sK58)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_126_9]) ).
cnf(f_126_14,negated_conjecture,
( ~ xsd_string(sK58)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_126_9]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS149+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 19 12:19:33 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.97/1.29 % SZS status Theorem for theBenchmark
% 0.97/1.29 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------