%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:47:23 AM UTC 2026
% Result : Theorem 9.16s 9.45s
% Output : Proof 9.23s
% 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)
<=> ( cC4(X)
& cC8(X) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X] :
( cC102(X)
<=> ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X] :
( cC104(X)
<=> ( ~ cC102(X)
& ~ cC100(X) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_5,axiom,
! [X] :
( cC106(X)
<=> ? [Y] :
( cC104(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_5) ).
fof(axiom_6,axiom,
! [X] :
( cC108(X)
<=> ( ~ cC98(X)
& ~ cC106(X) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_7,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_8,axiom,
! [X] :
( cC112(X)
<=> ( cC110(X)
& cC90(X) ) ),
file('theBenchmark.p',axiom_8) ).
fof(axiom_9,axiom,
! [X] :
( cC114(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_9) ).
fof(axiom_10,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_10) ).
fof(axiom_11,axiom,
! [X] :
( cC118(X)
<=> ? [Y] :
( ~ cC92(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_11) ).
fof(axiom_12,axiom,
! [X] :
( cC120(X)
<=> ( ~ cC92(X)
& ~ cC118(X) ) ),
file('theBenchmark.p',axiom_12) ).
fof(axiom_13,axiom,
! [X] :
( cC122(X)
<=> ? [Y] :
( cC120(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_13) ).
fof(axiom_14,axiom,
! [X] :
( cC124(X)
<=> ? [Y] :
( ~ cC92(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_14) ).
fof(axiom_15,axiom,
! [X] :
( cC126(X)
<=> ( ~ cC100(X)
& ~ cC124(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X] :
( cC128(X)
<=> ? [Y] :
( cC126(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_17,axiom,
! [X] :
( cC130(X)
<=> ( ~ cC128(X)
& ~ cC122(X) ) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_18,axiom,
! [X] :
( cC132(X)
<=> ( cC130(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_19,axiom,
! [X] :
( cC134(X)
<=> ( cC116(X)
& cC132(X) ) ),
file('theBenchmark.p',axiom_19) ).
fof(axiom_20,axiom,
! [X] :
( cC136(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_20) ).
fof(axiom_21,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_23,axiom,
! [X] :
( cC140(X)
<=> ? [Y] :
( ~ cC100(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_23) ).
fof(axiom_24,axiom,
! [X] :
( cC142(X)
<=> ( ~ cC92(X)
& ~ cC140(X) ) ),
file('theBenchmark.p',axiom_24) ).
fof(axiom_25,axiom,
! [X] :
( cC144(X)
<=> ? [Y] :
( cC142(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_26,axiom,
! [X] :
( cC146(X)
<=> ? [Y] :
( ~ cC100(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_26) ).
fof(axiom_27,axiom,
! [X] :
( cC148(X)
<=> ( ~ cC100(X)
& ~ cC146(X) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_28,axiom,
! [X] :
( cC150(X)
<=> ? [Y] :
( cC148(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_28) ).
fof(axiom_29,axiom,
! [X] :
( cC152(X)
<=> ( ~ cC144(X)
& ~ cC150(X) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC154(X)
<=> ( cC152(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_31,axiom,
! [X] :
( cC156(X)
<=> ( cC138(X)
& cC154(X) ) ),
file('theBenchmark.p',axiom_31) ).
fof(axiom_32,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_33,axiom,
! [X] :
( cC16(X)
<=> ( cC10(X)
& cC14(X) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_34,axiom,
! [X] :
( cC160(X)
<=> ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_34) ).
fof(axiom_35,axiom,
! [X] :
( cC162(X)
<=> ? [Y] :
( cC160(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_35) ).
fof(axiom_36,axiom,
! [X] :
( cC164(X)
<=> ? [Y] :
( ~ cC92(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_36) ).
fof(axiom_37,axiom,
! [X] :
( cC166(X)
<=> ? [Y] :
( cC164(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_37) ).
fof(axiom_38,axiom,
! [X] :
( cC168(X)
<=> ( ~ cC162(X)
& ~ cC166(X) ) ),
file('theBenchmark.p',axiom_38) ).
fof(axiom_39,axiom,
! [X] :
( cC170(X)
<=> ? [Y] :
( ~ cC18(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC172(X)
<=> ? [Y] :
( cC170(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC174(X)
<=> ( ~ cC172(X)
& cC168(X) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_42,axiom,
! [X] :
( cC176(X)
<=> ? [Y] :
( ~ cC100(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_43,axiom,
! [X] :
( cC178(X)
<=> ? [Y] :
( cC176(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_44,axiom,
! [X] :
( cC180(X)
<=> ( cC174(X)
& ~ cC178(X) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_45,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( ~ cC18(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_45) ).
fof(axiom_46,axiom,
! [X] :
( cC22(X)
<=> ( cC20(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_46) ).
fof(axiom_47,axiom,
! [X] :
( cC24(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_47) ).
fof(axiom_48,axiom,
! [X] :
( cC26(X)
<=> ( ~ cC2(X)
& ~ cC24(X) ) ),
file('theBenchmark.p',axiom_48) ).
fof(axiom_49,axiom,
! [X] :
( cC28(X)
<=> ? [Y] :
( cC26(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_49) ).
fof(axiom_50,axiom,
! [X] :
( cC30(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_51,axiom,
! [X] :
( cC32(X)
<=> ( ~ cC30(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_51) ).
fof(axiom_52,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( cC32(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_53,axiom,
! [X] :
( cC36(X)
<=> ( ~ cC34(X)
& ~ cC28(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_54,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('theBenchmark.p',axiom_54) ).
fof(axiom_55,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_55) ).
fof(axiom_56,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_56) ).
fof(axiom_57,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_58,axiom,
! [X] :
( cC44(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_58) ).
fof(axiom_59,axiom,
! [X] :
( cC46(X)
<=> ( ~ cC44(X)
& ~ cC12(X) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_60,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( cC46(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_60) ).
fof(axiom_61,axiom,
! [X] :
( cC50(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_61) ).
fof(axiom_62,axiom,
! [X] :
( cC52(X)
<=> ( ~ cC50(X)
& ~ cC12(X) ) ),
file('theBenchmark.p',axiom_62) ).
fof(axiom_63,axiom,
! [X] :
( cC54(X)
<=> ? [Y] :
( cC52(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_63) ).
fof(axiom_64,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& ~ cC48(X) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_68,axiom,
! [X] :
( cC64(X)
<=> ( cC60(X)
& cC62(X) ) ),
file('theBenchmark.p',axiom_68) ).
fof(axiom_69,axiom,
! [X] :
( cC66(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_69) ).
fof(axiom_70,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC18(X)
& ~ cC66(X) ) ),
file('theBenchmark.p',axiom_70) ).
fof(axiom_71,axiom,
! [X] :
( cC70(X)
<=> ? [Y] :
( cC68(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_71) ).
fof(axiom_72,axiom,
! [X] :
( cC72(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_72) ).
fof(axiom_73,axiom,
! [X] :
( cC74(X)
<=> ( ~ cC72(X)
& ~ cC18(X) ) ),
file('theBenchmark.p',axiom_73) ).
fof(axiom_74,axiom,
! [X] :
( cC76(X)
<=> ? [Y] :
( cC74(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_74) ).
fof(axiom_75,axiom,
! [X] :
( cC78(X)
<=> ( ~ cC76(X)
& ~ cC70(X) ) ),
file('theBenchmark.p',axiom_75) ).
fof(axiom_76,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_76) ).
fof(axiom_77,axiom,
! [X] :
( cC80(X)
<=> ( cC78(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_77) ).
fof(axiom_78,axiom,
! [X] :
( cC82(X)
<=> ( cC64(X)
& cC80(X) ) ),
file('theBenchmark.p',axiom_78) ).
fof(axiom_79,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_79) ).
fof(axiom_80,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('theBenchmark.p',axiom_80) ).
fof(axiom_81,axiom,
! [X] :
( cC88(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_81) ).
fof(axiom_82,axiom,
! [X] :
( cC90(X)
<=> ( cC86(X)
& cC88(X) ) ),
file('theBenchmark.p',axiom_82) ).
fof(axiom_83,axiom,
! [X] :
( cC94(X)
<=> ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_83) ).
fof(axiom_84,axiom,
! [X] :
( cC96(X)
<=> ( ~ cC94(X)
& ~ cC92(X) ) ),
file('theBenchmark.p',axiom_84) ).
fof(axiom_85,axiom,
! [X] :
( cC98(X)
<=> ? [Y] :
( cC96(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_85) ).
fof(axiom_86,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('theBenchmark.p',axiom_86) ).
fof(axiom_87,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC26(X) ),
file('theBenchmark.p',axiom_87) ).
fof(axiom_88,axiom,
cTOP(iV21026),
file('theBenchmark.p',axiom_88) ).
fof(axiom_89,axiom,
cTEST(iV21026),
file('theBenchmark.p',axiom_89) ).
fof(axiom_90,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC104(X) ),
file('theBenchmark.p',axiom_90) ).
fof(axiom_91,axiom,
~ cC98(iV21026),
file('theBenchmark.p',axiom_91) ).
fof(axiom_92,axiom,
~ cC122(iV21026),
file('theBenchmark.p',axiom_92) ).
fof(axiom_93,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC148(X) ),
file('theBenchmark.p',axiom_93) ).
fof(axiom_94,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC160(X) ),
file('theBenchmark.p',axiom_94) ).
fof(axiom_95,axiom,
~ cC34(iV21026),
file('theBenchmark.p',axiom_95) ).
fof(axiom_96,axiom,
~ cC28(iV21026),
file('theBenchmark.p',axiom_96) ).
fof(axiom_97,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC126(X) ),
file('theBenchmark.p',axiom_97) ).
fof(axiom_98,axiom,
~ cC70(iV21026),
file('theBenchmark.p',axiom_98) ).
fof(axiom_99,axiom,
~ cC178(iV21026),
file('theBenchmark.p',axiom_99) ).
fof(axiom_100,axiom,
~ cC162(iV21026),
file('theBenchmark.p',axiom_100) ).
fof(axiom_101,axiom,
~ cC166(iV21026),
file('theBenchmark.p',axiom_101) ).
fof(axiom_102,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC68(X) ),
file('theBenchmark.p',axiom_102) ).
fof(axiom_103,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC164(X) ),
file('theBenchmark.p',axiom_103) ).
fof(axiom_104,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC46(X) ),
file('theBenchmark.p',axiom_104) ).
fof(axiom_105,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC52(X) ),
file('theBenchmark.p',axiom_105) ).
fof(axiom_106,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC176(X) ),
file('theBenchmark.p',axiom_106) ).
fof(axiom_107,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC142(X) ),
file('theBenchmark.p',axiom_107) ).
fof(axiom_108,axiom,
~ cC150(iV21026),
file('theBenchmark.p',axiom_108) ).
fof(axiom_109,axiom,
~ cC54(iV21026),
file('theBenchmark.p',axiom_109) ).
fof(axiom_110,axiom,
~ cC106(iV21026),
file('theBenchmark.p',axiom_110) ).
fof(axiom_111,axiom,
~ cC144(iV21026),
file('theBenchmark.p',axiom_111) ).
fof(axiom_112,axiom,
~ cC48(iV21026),
file('theBenchmark.p',axiom_112) ).
fof(axiom_113,axiom,
~ cC76(iV21026),
file('theBenchmark.p',axiom_113) ).
fof(axiom_114,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC32(X) ),
file('theBenchmark.p',axiom_114) ).
fof(axiom_115,axiom,
~ cC128(iV21026),
file('theBenchmark.p',axiom_115) ).
fof(axiom_116,axiom,
~ cC172(iV21026),
file('theBenchmark.p',axiom_116) ).
fof(axiom_117,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC120(X) ),
file('theBenchmark.p',axiom_117) ).
fof(axiom_118,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC96(X) ),
file('theBenchmark.p',axiom_118) ).
fof(axiom_119,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC170(X) ),
file('theBenchmark.p',axiom_119) ).
fof(axiom_120,axiom,
cowlThing(iV21026),
file('theBenchmark.p',axiom_120) ).
fof(axiom_121,axiom,
! [X] :
( rR1(iV21026,X)
=> ~ cC74(X) ),
file('theBenchmark.p',axiom_121) ).
fof(axiom_122,axiom,
rR1(iV21026,iV21030),
file('theBenchmark.p',axiom_122) ).
fof(axiom_123,axiom,
rR1(iV21026,iV21027),
file('theBenchmark.p',axiom_123) ).
fof(axiom_124,axiom,
rR1(iV21026,iV21028),
file('theBenchmark.p',axiom_124) ).
fof(axiom_125,axiom,
rR1(iV21026,iV21029),
file('theBenchmark.p',axiom_125) ).
fof(axiom_126,axiom,
~ cC26(iV21027),
file('theBenchmark.p',axiom_126) ).
fof(axiom_127,axiom,
~ cC176(iV21027),
file('theBenchmark.p',axiom_127) ).
fof(axiom_128,axiom,
! [X] :
( rR1(iV21027,X)
=> cC18(X) ),
file('theBenchmark.p',axiom_128) ).
fof(axiom_129,axiom,
~ cC46(iV21027),
file('theBenchmark.p',axiom_129) ).
fof(axiom_130,axiom,
~ cC170(iV21027),
file('theBenchmark.p',axiom_130) ).
fof(axiom_131,axiom,
cC12(iV21027),
file('theBenchmark.p',axiom_131) ).
fof(axiom_132,axiom,
~ cC120(iV21027),
file('theBenchmark.p',axiom_132) ).
fof(axiom_133,axiom,
~ cC74(iV21027),
file('theBenchmark.p',axiom_133) ).
fof(axiom_134,axiom,
! [X] :
( rR1(iV21027,X)
=> cC6(X) ),
file('theBenchmark.p',axiom_134) ).
fof(axiom_135,axiom,
~ cC52(iV21027),
file('theBenchmark.p',axiom_135) ).
fof(axiom_136,axiom,
~ cC32(iV21027),
file('theBenchmark.p',axiom_136) ).
fof(axiom_137,axiom,
~ cC96(iV21027),
file('theBenchmark.p',axiom_137) ).
fof(axiom_138,axiom,
~ cC68(iV21027),
file('theBenchmark.p',axiom_138) ).
fof(axiom_139,axiom,
cC92(iV21027),
file('theBenchmark.p',axiom_139) ).
fof(axiom_140,axiom,
~ cC126(iV21027),
file('theBenchmark.p',axiom_140) ).
fof(axiom_141,axiom,
cC100(iV21027),
file('theBenchmark.p',axiom_141) ).
fof(axiom_142,axiom,
~ cC160(iV21027),
file('theBenchmark.p',axiom_142) ).
fof(axiom_143,axiom,
~ cC104(iV21027),
file('theBenchmark.p',axiom_143) ).
fof(axiom_144,axiom,
~ cC148(iV21027),
file('theBenchmark.p',axiom_144) ).
fof(axiom_145,axiom,
~ cC142(iV21027),
file('theBenchmark.p',axiom_145) ).
fof(axiom_146,axiom,
cC18(iV21027),
file('theBenchmark.p',axiom_146) ).
fof(axiom_147,axiom,
! [X] :
( rR1(iV21027,X)
=> cC92(X) ),
file('theBenchmark.p',axiom_147) ).
fof(axiom_148,axiom,
! [X] :
( rR1(iV21027,X)
=> cC100(X) ),
file('theBenchmark.p',axiom_148) ).
fof(axiom_149,axiom,
~ cC164(iV21027),
file('theBenchmark.p',axiom_149) ).
fof(axiom_150,axiom,
~ cC2(iV21027),
file('theBenchmark.p',axiom_150) ).
fof(axiom_151,axiom,
cowlThing(iV21027),
file('theBenchmark.p',axiom_151) ).
fof(axiom_152,axiom,
rR1(iV21027,iV21036),
file('theBenchmark.p',axiom_152) ).
fof(axiom_153,axiom,
rR1(iV21027,iV21035),
file('theBenchmark.p',axiom_153) ).
fof(axiom_154,axiom,
cowlThing(iV21028),
file('theBenchmark.p',axiom_154) ).
fof(axiom_155,axiom,
~ cC148(iV21029),
file('theBenchmark.p',axiom_155) ).
fof(axiom_156,axiom,
~ cC68(iV21029),
file('theBenchmark.p',axiom_156) ).
fof(axiom_157,axiom,
~ cC46(iV21029),
file('theBenchmark.p',axiom_157) ).
fof(axiom_158,axiom,
~ cC104(iV21029),
file('theBenchmark.p',axiom_158) ).
fof(axiom_159,axiom,
! [X] :
( rR1(iV21029,X)
=> cC100(X) ),
file('theBenchmark.p',axiom_159) ).
fof(axiom_160,axiom,
~ cC176(iV21029),
file('theBenchmark.p',axiom_160) ).
fof(axiom_161,axiom,
~ cC142(iV21029),
file('theBenchmark.p',axiom_161) ).
fof(axiom_162,axiom,
! [X] :
( rR1(iV21029,X)
=> cC92(X) ),
file('theBenchmark.p',axiom_162) ).
fof(axiom_163,axiom,
~ cC12(iV21029),
file('theBenchmark.p',axiom_163) ).
fof(axiom_164,axiom,
cC2(iV21029),
file('theBenchmark.p',axiom_164) ).
fof(axiom_165,axiom,
~ cC74(iV21029),
file('theBenchmark.p',axiom_165) ).
fof(axiom_166,axiom,
~ cC120(iV21029),
file('theBenchmark.p',axiom_166) ).
fof(axiom_167,axiom,
cC92(iV21029),
file('theBenchmark.p',axiom_167) ).
fof(axiom_168,axiom,
~ cC52(iV21029),
file('theBenchmark.p',axiom_168) ).
fof(axiom_169,axiom,
~ cC32(iV21029),
file('theBenchmark.p',axiom_169) ).
fof(axiom_170,axiom,
cC100(iV21029),
file('theBenchmark.p',axiom_170) ).
fof(axiom_171,axiom,
cC18(iV21029),
file('theBenchmark.p',axiom_171) ).
fof(axiom_172,axiom,
~ cC170(iV21029),
file('theBenchmark.p',axiom_172) ).
fof(axiom_173,axiom,
~ cC26(iV21029),
file('theBenchmark.p',axiom_173) ).
fof(axiom_174,axiom,
~ cC96(iV21029),
file('theBenchmark.p',axiom_174) ).
fof(axiom_175,axiom,
~ cC126(iV21029),
file('theBenchmark.p',axiom_175) ).
fof(axiom_176,axiom,
! [X] :
( rR1(iV21029,X)
=> cC6(X) ),
file('theBenchmark.p',axiom_176) ).
fof(axiom_177,axiom,
~ cC164(iV21029),
file('theBenchmark.p',axiom_177) ).
fof(axiom_178,axiom,
~ cC160(iV21029),
file('theBenchmark.p',axiom_178) ).
fof(axiom_179,axiom,
! [X] :
( rR1(iV21029,X)
=> cC18(X) ),
file('theBenchmark.p',axiom_179) ).
fof(axiom_180,axiom,
cowlThing(iV21029),
file('theBenchmark.p',axiom_180) ).
fof(axiom_181,axiom,
rR1(iV21029,iV21034),
file('theBenchmark.p',axiom_181) ).
fof(axiom_182,axiom,
rR1(iV21029,iV21033),
file('theBenchmark.p',axiom_182) ).
fof(axiom_183,axiom,
~ cC32(iV21030),
file('theBenchmark.p',axiom_183) ).
fof(axiom_184,axiom,
~ cC26(iV21030),
file('theBenchmark.p',axiom_184) ).
fof(axiom_185,axiom,
~ cC126(iV21030),
file('theBenchmark.p',axiom_185) ).
fof(axiom_186,axiom,
! [X] :
( rR1(iV21030,X)
=> cC18(X) ),
file('theBenchmark.p',axiom_186) ).
fof(axiom_187,axiom,
~ cC148(iV21030),
file('theBenchmark.p',axiom_187) ).
fof(axiom_188,axiom,
~ cC46(iV21030),
file('theBenchmark.p',axiom_188) ).
fof(axiom_189,axiom,
! [X] :
( rR1(iV21030,X)
=> cC6(X) ),
file('theBenchmark.p',axiom_189) ).
fof(axiom_190,axiom,
cC12(iV21030),
file('theBenchmark.p',axiom_190) ).
fof(axiom_191,axiom,
~ cC68(iV21030),
file('theBenchmark.p',axiom_191) ).
fof(axiom_192,axiom,
~ cC74(iV21030),
file('theBenchmark.p',axiom_192) ).
fof(axiom_193,axiom,
~ cC96(iV21030),
file('theBenchmark.p',axiom_193) ).
fof(axiom_194,axiom,
~ cC176(iV21030),
file('theBenchmark.p',axiom_194) ).
fof(axiom_195,axiom,
cC2(iV21030),
file('theBenchmark.p',axiom_195) ).
fof(axiom_196,axiom,
~ cC104(iV21030),
file('theBenchmark.p',axiom_196) ).
fof(axiom_197,axiom,
cC92(iV21030),
file('theBenchmark.p',axiom_197) ).
fof(axiom_198,axiom,
cC100(iV21030),
file('theBenchmark.p',axiom_198) ).
fof(axiom_199,axiom,
~ cC120(iV21030),
file('theBenchmark.p',axiom_199) ).
fof(axiom_200,axiom,
! [X] :
( rR1(iV21030,X)
=> cC100(X) ),
file('theBenchmark.p',axiom_200) ).
fof(axiom_201,axiom,
~ cC170(iV21030),
file('theBenchmark.p',axiom_201) ).
fof(axiom_202,axiom,
~ cC18(iV21030),
file('theBenchmark.p',axiom_202) ).
fof(axiom_203,axiom,
! [X] :
( rR1(iV21030,X)
=> cC92(X) ),
file('theBenchmark.p',axiom_203) ).
fof(axiom_204,axiom,
~ cC52(iV21030),
file('theBenchmark.p',axiom_204) ).
fof(axiom_205,axiom,
~ cC160(iV21030),
file('theBenchmark.p',axiom_205) ).
fof(axiom_206,axiom,
~ cC164(iV21030),
file('theBenchmark.p',axiom_206) ).
fof(axiom_207,axiom,
cowlThing(iV21030),
file('theBenchmark.p',axiom_207) ).
fof(axiom_208,axiom,
~ cC142(iV21030),
file('theBenchmark.p',axiom_208) ).
fof(axiom_209,axiom,
rR1(iV21030,iV21032),
file('theBenchmark.p',axiom_209) ).
fof(axiom_210,axiom,
rR1(iV21030,iV21031),
file('theBenchmark.p',axiom_210) ).
fof(axiom_211,axiom,
cowlThing(iV21031),
file('theBenchmark.p',axiom_211) ).
fof(axiom_212,axiom,
cC92(iV21032),
file('theBenchmark.p',axiom_212) ).
fof(axiom_213,axiom,
cC100(iV21032),
file('theBenchmark.p',axiom_213) ).
fof(axiom_214,axiom,
~ cC2(iV21032),
file('theBenchmark.p',axiom_214) ).
fof(axiom_215,axiom,
cC18(iV21032),
file('theBenchmark.p',axiom_215) ).
fof(axiom_216,axiom,
cC6(iV21032),
file('theBenchmark.p',axiom_216) ).
fof(axiom_217,axiom,
cowlThing(iV21032),
file('theBenchmark.p',axiom_217) ).
fof(axiom_218,axiom,
cC92(iV21033),
file('theBenchmark.p',axiom_218) ).
fof(axiom_219,axiom,
cC100(iV21033),
file('theBenchmark.p',axiom_219) ).
fof(axiom_220,axiom,
cC18(iV21033),
file('theBenchmark.p',axiom_220) ).
fof(axiom_221,axiom,
cC6(iV21033),
file('theBenchmark.p',axiom_221) ).
fof(axiom_222,axiom,
~ cC12(iV21033),
file('theBenchmark.p',axiom_222) ).
fof(axiom_223,axiom,
cowlThing(iV21033),
file('theBenchmark.p',axiom_223) ).
fof(axiom_224,axiom,
cC92(iV21034),
file('theBenchmark.p',axiom_224) ).
fof(axiom_225,axiom,
cC100(iV21034),
file('theBenchmark.p',axiom_225) ).
fof(axiom_226,axiom,
cC18(iV21034),
file('theBenchmark.p',axiom_226) ).
fof(axiom_227,axiom,
cC6(iV21034),
file('theBenchmark.p',axiom_227) ).
fof(axiom_228,axiom,
~ cC2(iV21034),
file('theBenchmark.p',axiom_228) ).
fof(axiom_229,axiom,
cowlThing(iV21034),
file('theBenchmark.p',axiom_229) ).
fof(axiom_230,axiom,
cC92(iV21035),
file('theBenchmark.p',axiom_230) ).
fof(axiom_231,axiom,
cC100(iV21035),
file('theBenchmark.p',axiom_231) ).
fof(axiom_232,axiom,
~ cC12(iV21035),
file('theBenchmark.p',axiom_232) ).
fof(axiom_233,axiom,
cC18(iV21035),
file('theBenchmark.p',axiom_233) ).
fof(axiom_234,axiom,
cC6(iV21035),
file('theBenchmark.p',axiom_234) ).
fof(axiom_235,axiom,
cowlThing(iV21035),
file('theBenchmark.p',axiom_235) ).
fof(axiom_236,axiom,
cC92(iV21036),
file('theBenchmark.p',axiom_236) ).
fof(axiom_237,axiom,
cC100(iV21036),
file('theBenchmark.p',axiom_237) ).
fof(axiom_238,axiom,
cC18(iV21036),
file('theBenchmark.p',axiom_238) ).
fof(axiom_239,axiom,
cC6(iV21036),
file('theBenchmark.p',axiom_239) ).
fof(axiom_240,axiom,
~ cC2(iV21036),
file('theBenchmark.p',axiom_240) ).
fof(axiom_241,axiom,
cowlThing(iV21036),
file('theBenchmark.p',axiom_241) ).
fof(the_axiom,conjecture,
( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [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)
| ~ cC4(X)
| ~ cC8(X) )
& ( ( cC4(X)
& cC8(X) )
| ~ cC10(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(f_3_2,plain,
! [U_6] :
( ( cC10(U_6)
| ~ cC4(U_6)
| ~ cC8(U_6) )
& ( ( cC4(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)
| ~ cC4(U_8)
| ~ cC8(U_8) )
& ! [U_7] :
( ( cC4(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,
( cC4(U_7)
| ~ cC10(U_7) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_6,plain,
( cC10(U_8)
| ~ cC4(U_8)
| ~ cC8(U_8) ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X] :
( ( cC102(X)
| ! [Y] :
( cC6(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) )
| ~ cC102(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(f_4_2,plain,
! [U_11] :
( ( cC102(U_11)
| ! [U_10] :
( cC6(U_10)
| ~ rR1(U_11,U_10) ) )
& ( ? [U_9] :
( ~ cC6(U_9)
& rR1(U_11,U_9) )
| ~ cC102(U_11) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_13] :
( cC102(U_13)
| ! [U_10] :
( cC6(U_10)
| ~ rR1(U_13,U_10) ) )
& ! [U_12] :
( ? [U_9] :
( ~ cC6(U_9)
& rR1(U_12,U_9) )
| ~ cC102(U_12) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
( ! [U_13] :
( cC102(U_13)
| ! [U_10] :
( cC6(U_10)
| ~ rR1(U_13,U_10) ) )
& ! [U_12] :
( ( ~ cC6(sK1(U_12))
& rR1(U_12,sK1(U_12)) )
| ~ cC102(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))
| ~ cC102(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_6,plain,
( ~ cC6(sK1(U_12))
| ~ cC102(U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_7,plain,
( cC102(U_13)
| cC6(U_10)
| ~ rR1(U_13,U_10) ),
inference(clausify,[status(thm)],[f_4_4]) ).
fof(f_5_1,plain,
! [X] :
( ( cC104(X)
| cC102(X)
| cC100(X) )
& ( ( ~ cC102(X)
& ~ cC100(X) )
| ~ cC104(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_4]) ).
fof(f_5_2,plain,
! [U_14] :
( ( cC104(U_14)
| cC102(U_14)
| cC100(U_14) )
& ( ( ~ cC102(U_14)
& ~ cC100(U_14) )
| ~ cC104(U_14) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_16] :
( cC104(U_16)
| cC102(U_16)
| cC100(U_16) )
& ! [U_15] :
( ( ~ cC102(U_15)
& ~ cC100(U_15) )
| ~ cC104(U_15) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
cnf(f_5_4,plain,
( ~ cC100(U_15)
| ~ cC104(U_15) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_5,plain,
( ~ cC102(U_15)
| ~ cC104(U_15) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_6,plain,
( cC104(U_16)
| cC102(U_16)
| cC100(U_16) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [X] :
( ( cC106(X)
| ! [Y] :
( ~ cC104(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC104(Y)
& rR1(X,Y) )
| ~ cC106(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_5]) ).
fof(f_6_2,plain,
! [U_19] :
( ( cC106(U_19)
| ! [U_18] :
( ~ cC104(U_18)
| ~ rR1(U_19,U_18) ) )
& ( ? [U_17] :
( cC104(U_17)
& rR1(U_19,U_17) )
| ~ cC106(U_19) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_21] :
( cC106(U_21)
| ! [U_18] :
( ~ cC104(U_18)
| ~ rR1(U_21,U_18) ) )
& ! [U_20] :
( ? [U_17] :
( cC104(U_17)
& rR1(U_20,U_17) )
| ~ cC106(U_20) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_21] :
( cC106(U_21)
| ! [U_18] :
( ~ cC104(U_18)
| ~ rR1(U_21,U_18) ) )
& ! [U_20] :
( ( cC104(sK2(U_20))
& rR1(U_20,sK2(U_20)) )
| ~ cC106(U_20) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_17,sK2(U_20))],[f_6_3]) ).
cnf(f_6_5,plain,
( rR1(U_20,sK2(U_20))
| ~ cC106(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_6,plain,
( cC104(sK2(U_20))
| ~ cC106(U_20) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_7,plain,
( cC106(U_21)
| ~ cC104(U_18)
| ~ rR1(U_21,U_18) ),
inference(clausify,[status(thm)],[f_6_4]) ).
fof(f_7_1,plain,
! [X] :
( ( cC108(X)
| cC98(X)
| cC106(X) )
& ( ( ~ cC98(X)
& ~ cC106(X) )
| ~ cC108(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_6]) ).
fof(f_7_2,plain,
! [U_22] :
( ( cC108(U_22)
| cC98(U_22)
| cC106(U_22) )
& ( ( ~ cC98(U_22)
& ~ cC106(U_22) )
| ~ cC108(U_22) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_24] :
( cC108(U_24)
| cC98(U_24)
| cC106(U_24) )
& ! [U_23] :
( ( ~ cC98(U_23)
& ~ cC106(U_23) )
| ~ cC108(U_23) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
cnf(f_7_4,plain,
( ~ cC106(U_23)
| ~ cC108(U_23) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_5,plain,
( ~ cC98(U_23)
| ~ cC108(U_23) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_6,plain,
( cC108(U_24)
| cC98(U_24)
| cC106(U_24) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [X] :
( ( cC110(X)
| ~ cTOP(X)
| ~ cC108(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_7]) ).
fof(f_8_2,plain,
! [U_25] :
( ( cC110(U_25)
| ~ cTOP(U_25)
| ~ cC108(U_25) )
& ( ( cTOP(U_25)
& cC108(U_25) )
| ~ cC110(U_25) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_27] :
( cC110(U_27)
| ~ cTOP(U_27)
| ~ cC108(U_27) )
& ! [U_26] :
( ( cTOP(U_26)
& cC108(U_26) )
| ~ cC110(U_26) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( cC108(U_26)
| ~ cC110(U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( cTOP(U_26)
| ~ cC110(U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( cC110(U_27)
| ~ cTOP(U_27)
| ~ cC108(U_27) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X] :
( ( cC112(X)
| ~ cC110(X)
| ~ cC90(X) )
& ( ( cC110(X)
& cC90(X) )
| ~ cC112(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_8]) ).
fof(f_9_2,plain,
! [U_28] :
( ( cC112(U_28)
| ~ cC110(U_28)
| ~ cC90(U_28) )
& ( ( cC110(U_28)
& cC90(U_28) )
| ~ cC112(U_28) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_30] :
( cC112(U_30)
| ~ cC110(U_30)
| ~ cC90(U_30) )
& ! [U_29] :
( ( cC110(U_29)
& cC90(U_29) )
| ~ cC112(U_29) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( cC90(U_29)
| ~ cC112(U_29) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( cC110(U_29)
| ~ cC112(U_29) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( cC112(U_30)
| ~ cC110(U_30)
| ~ cC90(U_30) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X] :
( ( cC114(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC114(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_9]) ).
fof(f_10_2,plain,
! [U_31] :
( ( cC114(U_31)
| ~ cTOP(U_31) )
& ( cTOP(U_31)
| ~ cC114(U_31) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_33] :
( cC114(U_33)
| ~ cTOP(U_33) )
& ! [U_32] :
( cTOP(U_32)
| ~ cC114(U_32) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
cnf(f_10_4,plain,
( cTOP(U_32)
| ~ cC114(U_32) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_5,plain,
( cC114(U_33)
| ~ cTOP(U_33) ),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
! [X] :
( ( cC116(X)
| ~ cC112(X)
| ~ cC114(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_10]) ).
fof(f_11_2,plain,
! [U_34] :
( ( cC116(U_34)
| ~ cC112(U_34)
| ~ cC114(U_34) )
& ( ( cC112(U_34)
& cC114(U_34) )
| ~ cC116(U_34) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_36] :
( cC116(U_36)
| ~ cC112(U_36)
| ~ cC114(U_36) )
& ! [U_35] :
( ( cC112(U_35)
& cC114(U_35) )
| ~ cC116(U_35) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
cnf(f_11_4,plain,
( cC114(U_35)
| ~ cC116(U_35) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_5,plain,
( cC112(U_35)
| ~ cC116(U_35) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_6,plain,
( cC116(U_36)
| ~ cC112(U_36)
| ~ cC114(U_36) ),
inference(clausify,[status(thm)],[f_11_3]) ).
fof(f_12_1,plain,
! [X] :
( ( cC118(X)
| ! [Y] :
( cC92(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC92(Y)
& rR1(X,Y) )
| ~ cC118(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_11]) ).
fof(f_12_2,plain,
! [U_39] :
( ( cC118(U_39)
| ! [U_38] :
( cC92(U_38)
| ~ rR1(U_39,U_38) ) )
& ( ? [U_37] :
( ~ cC92(U_37)
& rR1(U_39,U_37) )
| ~ cC118(U_39) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_41] :
( cC118(U_41)
| ! [U_38] :
( cC92(U_38)
| ~ rR1(U_41,U_38) ) )
& ! [U_40] :
( ? [U_37] :
( ~ cC92(U_37)
& rR1(U_40,U_37) )
| ~ cC118(U_40) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
fof(f_12_4,plain,
( ! [U_41] :
( cC118(U_41)
| ! [U_38] :
( cC92(U_38)
| ~ rR1(U_41,U_38) ) )
& ! [U_40] :
( ( ~ cC92(sK3(U_40))
& rR1(U_40,sK3(U_40)) )
| ~ cC118(U_40) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_37,sK3(U_40))],[f_12_3]) ).
cnf(f_12_5,plain,
( rR1(U_40,sK3(U_40))
| ~ cC118(U_40) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_6,plain,
( ~ cC92(sK3(U_40))
| ~ cC118(U_40) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_7,plain,
( cC118(U_41)
| cC92(U_38)
| ~ rR1(U_41,U_38) ),
inference(clausify,[status(thm)],[f_12_4]) ).
fof(f_13_1,plain,
! [X] :
( ( cC120(X)
| cC92(X)
| cC118(X) )
& ( ( ~ cC92(X)
& ~ cC118(X) )
| ~ cC120(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_12]) ).
fof(f_13_2,plain,
! [U_42] :
( ( cC120(U_42)
| cC92(U_42)
| cC118(U_42) )
& ( ( ~ cC92(U_42)
& ~ cC118(U_42) )
| ~ cC120(U_42) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_44] :
( cC120(U_44)
| cC92(U_44)
| cC118(U_44) )
& ! [U_43] :
( ( ~ cC92(U_43)
& ~ cC118(U_43) )
| ~ cC120(U_43) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( ~ cC118(U_43)
| ~ cC120(U_43) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( ~ cC92(U_43)
| ~ cC120(U_43) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_6,plain,
( cC120(U_44)
| cC92(U_44)
| cC118(U_44) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X] :
( ( cC122(X)
| ! [Y] :
( ~ cC120(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC120(Y)
& rR1(X,Y) )
| ~ cC122(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_13]) ).
fof(f_14_2,plain,
! [U_47] :
( ( cC122(U_47)
| ! [U_46] :
( ~ cC120(U_46)
| ~ rR1(U_47,U_46) ) )
& ( ? [U_45] :
( cC120(U_45)
& rR1(U_47,U_45) )
| ~ cC122(U_47) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_49] :
( cC122(U_49)
| ! [U_46] :
( ~ cC120(U_46)
| ~ rR1(U_49,U_46) ) )
& ! [U_48] :
( ? [U_45] :
( cC120(U_45)
& rR1(U_48,U_45) )
| ~ cC122(U_48) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_49] :
( cC122(U_49)
| ! [U_46] :
( ~ cC120(U_46)
| ~ rR1(U_49,U_46) ) )
& ! [U_48] :
( ( cC120(sK4(U_48))
& rR1(U_48,sK4(U_48)) )
| ~ cC122(U_48) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_45,sK4(U_48))],[f_14_3]) ).
cnf(f_14_5,plain,
( rR1(U_48,sK4(U_48))
| ~ cC122(U_48) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_6,plain,
( cC120(sK4(U_48))
| ~ cC122(U_48) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_7,plain,
( cC122(U_49)
| ~ cC120(U_46)
| ~ rR1(U_49,U_46) ),
inference(clausify,[status(thm)],[f_14_4]) ).
fof(f_15_1,plain,
! [X] :
( ( cC124(X)
| ! [Y] :
( cC92(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC92(Y)
& rR1(X,Y) )
| ~ cC124(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_14]) ).
fof(f_15_2,plain,
! [U_52] :
( ( cC124(U_52)
| ! [U_51] :
( cC92(U_51)
| ~ rR1(U_52,U_51) ) )
& ( ? [U_50] :
( ~ cC92(U_50)
& rR1(U_52,U_50) )
| ~ cC124(U_52) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_54] :
( cC124(U_54)
| ! [U_51] :
( cC92(U_51)
| ~ rR1(U_54,U_51) ) )
& ! [U_53] :
( ? [U_50] :
( ~ cC92(U_50)
& rR1(U_53,U_50) )
| ~ cC124(U_53) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_54] :
( cC124(U_54)
| ! [U_51] :
( cC92(U_51)
| ~ rR1(U_54,U_51) ) )
& ! [U_53] :
( ( ~ cC92(sK5(U_53))
& rR1(U_53,sK5(U_53)) )
| ~ cC124(U_53) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_50,sK5(U_53))],[f_15_3]) ).
cnf(f_15_5,plain,
( rR1(U_53,sK5(U_53))
| ~ cC124(U_53) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_6,plain,
( ~ cC92(sK5(U_53))
| ~ cC124(U_53) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_7,plain,
( cC124(U_54)
| cC92(U_51)
| ~ rR1(U_54,U_51) ),
inference(clausify,[status(thm)],[f_15_4]) ).
fof(f_16_1,plain,
! [X] :
( ( cC126(X)
| cC100(X)
| cC124(X) )
& ( ( ~ cC100(X)
& ~ cC124(X) )
| ~ cC126(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_15]) ).
fof(f_16_2,plain,
! [U_55] :
( ( cC126(U_55)
| cC100(U_55)
| cC124(U_55) )
& ( ( ~ cC100(U_55)
& ~ cC124(U_55) )
| ~ cC126(U_55) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_57] :
( cC126(U_57)
| cC100(U_57)
| cC124(U_57) )
& ! [U_56] :
( ( ~ cC100(U_56)
& ~ cC124(U_56) )
| ~ cC126(U_56) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( ~ cC124(U_56)
| ~ cC126(U_56) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( ~ cC100(U_56)
| ~ cC126(U_56) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_6,plain,
( cC126(U_57)
| cC100(U_57)
| cC124(U_57) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X] :
( ( cC128(X)
| ! [Y] :
( ~ cC126(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC126(Y)
& rR1(X,Y) )
| ~ cC128(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(f_17_2,plain,
! [U_60] :
( ( cC128(U_60)
| ! [U_59] :
( ~ cC126(U_59)
| ~ rR1(U_60,U_59) ) )
& ( ? [U_58] :
( cC126(U_58)
& rR1(U_60,U_58) )
| ~ cC128(U_60) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_62] :
( cC128(U_62)
| ! [U_59] :
( ~ cC126(U_59)
| ~ rR1(U_62,U_59) ) )
& ! [U_61] :
( ? [U_58] :
( cC126(U_58)
& rR1(U_61,U_58) )
| ~ cC128(U_61) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_62] :
( cC128(U_62)
| ! [U_59] :
( ~ cC126(U_59)
| ~ rR1(U_62,U_59) ) )
& ! [U_61] :
( ( cC126(sK6(U_61))
& rR1(U_61,sK6(U_61)) )
| ~ cC128(U_61) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_58,sK6(U_61))],[f_17_3]) ).
cnf(f_17_5,plain,
( rR1(U_61,sK6(U_61))
| ~ cC128(U_61) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_6,plain,
( cC126(sK6(U_61))
| ~ cC128(U_61) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_7,plain,
( cC128(U_62)
| ~ cC126(U_59)
| ~ rR1(U_62,U_59) ),
inference(clausify,[status(thm)],[f_17_4]) ).
fof(f_18_1,plain,
! [X] :
( ( cC130(X)
| cC128(X)
| cC122(X) )
& ( ( ~ cC128(X)
& ~ cC122(X) )
| ~ cC130(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_17]) ).
fof(f_18_2,plain,
! [U_63] :
( ( cC130(U_63)
| cC128(U_63)
| cC122(U_63) )
& ( ( ~ cC128(U_63)
& ~ cC122(U_63) )
| ~ cC130(U_63) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_65] :
( cC130(U_65)
| cC128(U_65)
| cC122(U_65) )
& ! [U_64] :
( ( ~ cC128(U_64)
& ~ cC122(U_64) )
| ~ cC130(U_64) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
cnf(f_18_4,plain,
( ~ cC122(U_64)
| ~ cC130(U_64) ),
inference(clausify,[status(thm)],[f_18_3]) ).
cnf(f_18_5,plain,
( ~ cC128(U_64)
| ~ cC130(U_64) ),
inference(clausify,[status(thm)],[f_18_3]) ).
cnf(f_18_6,plain,
( cC130(U_65)
| cC128(U_65)
| cC122(U_65) ),
inference(clausify,[status(thm)],[f_18_3]) ).
fof(f_19_1,plain,
! [X] :
( ( cC132(X)
| ~ cC130(X)
| ~ cTOP(X) )
& ( ( cC130(X)
& cTOP(X) )
| ~ cC132(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_18]) ).
fof(f_19_2,plain,
! [U_66] :
( ( cC132(U_66)
| ~ cC130(U_66)
| ~ cTOP(U_66) )
& ( ( cC130(U_66)
& cTOP(U_66) )
| ~ cC132(U_66) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_68] :
( cC132(U_68)
| ~ cC130(U_68)
| ~ cTOP(U_68) )
& ! [U_67] :
( ( cC130(U_67)
& cTOP(U_67) )
| ~ cC132(U_67) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( cTOP(U_67)
| ~ cC132(U_67) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( cC130(U_67)
| ~ cC132(U_67) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_6,plain,
( cC132(U_68)
| ~ cC130(U_68)
| ~ cTOP(U_68) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [X] :
( ( cC134(X)
| ~ cC116(X)
| ~ cC132(X) )
& ( ( cC116(X)
& cC132(X) )
| ~ cC134(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_19]) ).
fof(f_20_2,plain,
! [U_69] :
( ( cC134(U_69)
| ~ cC116(U_69)
| ~ cC132(U_69) )
& ( ( cC116(U_69)
& cC132(U_69) )
| ~ cC134(U_69) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_71] :
( cC134(U_71)
| ~ cC116(U_71)
| ~ cC132(U_71) )
& ! [U_70] :
( ( cC116(U_70)
& cC132(U_70) )
| ~ cC134(U_70) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( cC132(U_70)
| ~ cC134(U_70) ),
inference(clausify,[status(thm)],[f_20_3]) ).
cnf(f_20_5,plain,
( cC116(U_70)
| ~ cC134(U_70) ),
inference(clausify,[status(thm)],[f_20_3]) ).
cnf(f_20_6,plain,
( cC134(U_71)
| ~ cC116(U_71)
| ~ cC132(U_71) ),
inference(clausify,[status(thm)],[f_20_3]) ).
fof(f_21_1,plain,
! [X] :
( ( cC136(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC136(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_20]) ).
fof(f_21_2,plain,
! [U_72] :
( ( cC136(U_72)
| ~ cTOP(U_72) )
& ( cTOP(U_72)
| ~ cC136(U_72) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ! [U_74] :
( cC136(U_74)
| ~ cTOP(U_74) )
& ! [U_73] :
( cTOP(U_73)
| ~ cC136(U_73) ) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( cTOP(U_73)
| ~ cC136(U_73) ),
inference(clausify,[status(thm)],[f_21_3]) ).
cnf(f_21_5,plain,
( cC136(U_74)
| ~ cTOP(U_74) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [X] :
( ( cC138(X)
| ~ cC134(X)
| ~ cC136(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_21]) ).
fof(f_22_2,plain,
! [U_75] :
( ( cC138(U_75)
| ~ cC134(U_75)
| ~ cC136(U_75) )
& ( ( cC134(U_75)
& cC136(U_75) )
| ~ cC138(U_75) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_77] :
( cC138(U_77)
| ~ cC134(U_77)
| ~ cC136(U_77) )
& ! [U_76] :
( ( cC134(U_76)
& cC136(U_76) )
| ~ cC138(U_76) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( cC136(U_76)
| ~ cC138(U_76) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( cC134(U_76)
| ~ cC138(U_76) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_6,plain,
( cC138(U_77)
| ~ cC134(U_77)
| ~ cC136(U_77) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [X] :
( ( cC14(X)
| ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_22]) ).
fof(f_23_2,plain,
! [U_80] :
( ( cC14(U_80)
| ! [U_79] :
( cC12(U_79)
| ~ rR1(U_80,U_79) ) )
& ( ? [U_78] :
( ~ cC12(U_78)
& rR1(U_80,U_78) )
| ~ cC14(U_80) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_82] :
( cC14(U_82)
| ! [U_79] :
( cC12(U_79)
| ~ rR1(U_82,U_79) ) )
& ! [U_81] :
( ? [U_78] :
( ~ cC12(U_78)
& rR1(U_81,U_78) )
| ~ cC14(U_81) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_82] :
( cC14(U_82)
| ! [U_79] :
( cC12(U_79)
| ~ rR1(U_82,U_79) ) )
& ! [U_81] :
( ( ~ cC12(sK7(U_81))
& rR1(U_81,sK7(U_81)) )
| ~ cC14(U_81) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_78,sK7(U_81))],[f_23_3]) ).
cnf(f_23_5,plain,
( rR1(U_81,sK7(U_81))
| ~ cC14(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( ~ cC12(sK7(U_81))
| ~ cC14(U_81) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( cC14(U_82)
| cC12(U_79)
| ~ rR1(U_82,U_79) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
! [X] :
( ( cC140(X)
| ! [Y] :
( cC100(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC100(Y)
& rR1(X,Y) )
| ~ cC140(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_23]) ).
fof(f_24_2,plain,
! [U_85] :
( ( cC140(U_85)
| ! [U_84] :
( cC100(U_84)
| ~ rR1(U_85,U_84) ) )
& ( ? [U_83] :
( ~ cC100(U_83)
& rR1(U_85,U_83) )
| ~ cC140(U_85) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_87] :
( cC140(U_87)
| ! [U_84] :
( cC100(U_84)
| ~ rR1(U_87,U_84) ) )
& ! [U_86] :
( ? [U_83] :
( ~ cC100(U_83)
& rR1(U_86,U_83) )
| ~ cC140(U_86) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
fof(f_24_4,plain,
( ! [U_87] :
( cC140(U_87)
| ! [U_84] :
( cC100(U_84)
| ~ rR1(U_87,U_84) ) )
& ! [U_86] :
( ( ~ cC100(sK8(U_86))
& rR1(U_86,sK8(U_86)) )
| ~ cC140(U_86) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_83,sK8(U_86))],[f_24_3]) ).
cnf(f_24_5,plain,
( rR1(U_86,sK8(U_86))
| ~ cC140(U_86) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_6,plain,
( ~ cC100(sK8(U_86))
| ~ cC140(U_86) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_7,plain,
( cC140(U_87)
| cC100(U_84)
| ~ rR1(U_87,U_84) ),
inference(clausify,[status(thm)],[f_24_4]) ).
fof(f_25_1,plain,
! [X] :
( ( cC142(X)
| cC92(X)
| cC140(X) )
& ( ( ~ cC92(X)
& ~ cC140(X) )
| ~ cC142(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_24]) ).
fof(f_25_2,plain,
! [U_88] :
( ( cC142(U_88)
| cC92(U_88)
| cC140(U_88) )
& ( ( ~ cC92(U_88)
& ~ cC140(U_88) )
| ~ cC142(U_88) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_90] :
( cC142(U_90)
| cC92(U_90)
| cC140(U_90) )
& ! [U_89] :
( ( ~ cC92(U_89)
& ~ cC140(U_89) )
| ~ cC142(U_89) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( ~ cC140(U_89)
| ~ cC142(U_89) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( ~ cC92(U_89)
| ~ cC142(U_89) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_6,plain,
( cC142(U_90)
| cC92(U_90)
| cC140(U_90) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [X] :
( ( cC144(X)
| ! [Y] :
( ~ cC142(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC142(Y)
& rR1(X,Y) )
| ~ cC144(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_25]) ).
fof(f_26_2,plain,
! [U_93] :
( ( cC144(U_93)
| ! [U_92] :
( ~ cC142(U_92)
| ~ rR1(U_93,U_92) ) )
& ( ? [U_91] :
( cC142(U_91)
& rR1(U_93,U_91) )
| ~ cC144(U_93) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_95] :
( cC144(U_95)
| ! [U_92] :
( ~ cC142(U_92)
| ~ rR1(U_95,U_92) ) )
& ! [U_94] :
( ? [U_91] :
( cC142(U_91)
& rR1(U_94,U_91) )
| ~ cC144(U_94) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
fof(f_26_4,plain,
( ! [U_95] :
( cC144(U_95)
| ! [U_92] :
( ~ cC142(U_92)
| ~ rR1(U_95,U_92) ) )
& ! [U_94] :
( ( cC142(sK9(U_94))
& rR1(U_94,sK9(U_94)) )
| ~ cC144(U_94) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_91,sK9(U_94))],[f_26_3]) ).
cnf(f_26_5,plain,
( rR1(U_94,sK9(U_94))
| ~ cC144(U_94) ),
inference(clausify,[status(thm)],[f_26_4]) ).
cnf(f_26_6,plain,
( cC142(sK9(U_94))
| ~ cC144(U_94) ),
inference(clausify,[status(thm)],[f_26_4]) ).
cnf(f_26_7,plain,
( cC144(U_95)
| ~ cC142(U_92)
| ~ rR1(U_95,U_92) ),
inference(clausify,[status(thm)],[f_26_4]) ).
fof(f_27_1,plain,
! [X] :
( ( cC146(X)
| ! [Y] :
( cC100(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC100(Y)
& rR1(X,Y) )
| ~ cC146(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_26]) ).
fof(f_27_2,plain,
! [U_98] :
( ( cC146(U_98)
| ! [U_97] :
( cC100(U_97)
| ~ rR1(U_98,U_97) ) )
& ( ? [U_96] :
( ~ cC100(U_96)
& rR1(U_98,U_96) )
| ~ cC146(U_98) ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_100] :
( cC146(U_100)
| ! [U_97] :
( cC100(U_97)
| ~ rR1(U_100,U_97) ) )
& ! [U_99] :
( ? [U_96] :
( ~ cC100(U_96)
& rR1(U_99,U_96) )
| ~ cC146(U_99) ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
( ! [U_100] :
( cC146(U_100)
| ! [U_97] :
( cC100(U_97)
| ~ rR1(U_100,U_97) ) )
& ! [U_99] :
( ( ~ cC100(sK10(U_99))
& rR1(U_99,sK10(U_99)) )
| ~ cC146(U_99) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_96,sK10(U_99))],[f_27_3]) ).
cnf(f_27_5,plain,
( rR1(U_99,sK10(U_99))
| ~ cC146(U_99) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_6,plain,
( ~ cC100(sK10(U_99))
| ~ cC146(U_99) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_7,plain,
( cC146(U_100)
| cC100(U_97)
| ~ rR1(U_100,U_97) ),
inference(clausify,[status(thm)],[f_27_4]) ).
fof(f_28_1,plain,
! [X] :
( ( cC148(X)
| cC100(X)
| cC146(X) )
& ( ( ~ cC100(X)
& ~ cC146(X) )
| ~ cC148(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_27]) ).
fof(f_28_2,plain,
! [U_101] :
( ( cC148(U_101)
| cC100(U_101)
| cC146(U_101) )
& ( ( ~ cC100(U_101)
& ~ cC146(U_101) )
| ~ cC148(U_101) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_103] :
( cC148(U_103)
| cC100(U_103)
| cC146(U_103) )
& ! [U_102] :
( ( ~ cC100(U_102)
& ~ cC146(U_102) )
| ~ cC148(U_102) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
cnf(f_28_4,plain,
( ~ cC146(U_102)
| ~ cC148(U_102) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( ~ cC100(U_102)
| ~ cC148(U_102) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_6,plain,
( cC148(U_103)
| cC100(U_103)
| cC146(U_103) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X] :
( ( cC150(X)
| ! [Y] :
( ~ cC148(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC148(Y)
& rR1(X,Y) )
| ~ cC150(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_28]) ).
fof(f_29_2,plain,
! [U_106] :
( ( cC150(U_106)
| ! [U_105] :
( ~ cC148(U_105)
| ~ rR1(U_106,U_105) ) )
& ( ? [U_104] :
( cC148(U_104)
& rR1(U_106,U_104) )
| ~ cC150(U_106) ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_108] :
( cC150(U_108)
| ! [U_105] :
( ~ cC148(U_105)
| ~ rR1(U_108,U_105) ) )
& ! [U_107] :
( ? [U_104] :
( cC148(U_104)
& rR1(U_107,U_104) )
| ~ cC150(U_107) ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
fof(f_29_4,plain,
( ! [U_108] :
( cC150(U_108)
| ! [U_105] :
( ~ cC148(U_105)
| ~ rR1(U_108,U_105) ) )
& ! [U_107] :
( ( cC148(sK11(U_107))
& rR1(U_107,sK11(U_107)) )
| ~ cC150(U_107) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_104,sK11(U_107))],[f_29_3]) ).
cnf(f_29_5,plain,
( rR1(U_107,sK11(U_107))
| ~ cC150(U_107) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_6,plain,
( cC148(sK11(U_107))
| ~ cC150(U_107) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_7,plain,
( cC150(U_108)
| ~ cC148(U_105)
| ~ rR1(U_108,U_105) ),
inference(clausify,[status(thm)],[f_29_4]) ).
fof(f_30_1,plain,
! [X] :
( ( cC152(X)
| cC144(X)
| cC150(X) )
& ( ( ~ cC144(X)
& ~ cC150(X) )
| ~ cC152(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_29]) ).
fof(f_30_2,plain,
! [U_109] :
( ( cC152(U_109)
| cC144(U_109)
| cC150(U_109) )
& ( ( ~ cC144(U_109)
& ~ cC150(U_109) )
| ~ cC152(U_109) ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_111] :
( cC152(U_111)
| cC144(U_111)
| cC150(U_111) )
& ! [U_110] :
( ( ~ cC144(U_110)
& ~ cC150(U_110) )
| ~ cC152(U_110) ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
cnf(f_30_4,plain,
( ~ cC150(U_110)
| ~ cC152(U_110) ),
inference(clausify,[status(thm)],[f_30_3]) ).
cnf(f_30_5,plain,
( ~ cC144(U_110)
| ~ cC152(U_110) ),
inference(clausify,[status(thm)],[f_30_3]) ).
cnf(f_30_6,plain,
( cC152(U_111)
| cC144(U_111)
| cC150(U_111) ),
inference(clausify,[status(thm)],[f_30_3]) ).
fof(f_31_1,plain,
! [X] :
( ( cC154(X)
| ~ cC152(X)
| ~ cTOP(X) )
& ( ( cC152(X)
& cTOP(X) )
| ~ cC154(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_30]) ).
fof(f_31_2,plain,
! [U_112] :
( ( cC154(U_112)
| ~ cC152(U_112)
| ~ cTOP(U_112) )
& ( ( cC152(U_112)
& cTOP(U_112) )
| ~ cC154(U_112) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_114] :
( cC154(U_114)
| ~ cC152(U_114)
| ~ cTOP(U_114) )
& ! [U_113] :
( ( cC152(U_113)
& cTOP(U_113) )
| ~ cC154(U_113) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( cTOP(U_113)
| ~ cC154(U_113) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_5,plain,
( cC152(U_113)
| ~ cC154(U_113) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_6,plain,
( cC154(U_114)
| ~ cC152(U_114)
| ~ cTOP(U_114) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [X] :
( ( cC156(X)
| ~ cC138(X)
| ~ cC154(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_31]) ).
fof(f_32_2,plain,
! [U_115] :
( ( cC156(U_115)
| ~ cC138(U_115)
| ~ cC154(U_115) )
& ( ( cC138(U_115)
& cC154(U_115) )
| ~ cC156(U_115) ) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
( ! [U_117] :
( cC156(U_117)
| ~ cC138(U_117)
| ~ cC154(U_117) )
& ! [U_116] :
( ( cC138(U_116)
& cC154(U_116) )
| ~ cC156(U_116) ) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
cnf(f_32_4,plain,
( cC154(U_116)
| ~ cC156(U_116) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_5,plain,
( cC138(U_116)
| ~ cC156(U_116) ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_6,plain,
( cC156(U_117)
| ~ cC138(U_117)
| ~ cC154(U_117) ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [X] :
( ( cC158(X)
| ~ cC156(X)
| ~ cC22(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_32]) ).
fof(f_33_2,plain,
! [U_118] :
( ( cC158(U_118)
| ~ cC156(U_118)
| ~ cC22(U_118) )
& ( ( cC156(U_118)
& cC22(U_118) )
| ~ cC158(U_118) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_120] :
( cC158(U_120)
| ~ cC156(U_120)
| ~ cC22(U_120) )
& ! [U_119] :
( ( cC156(U_119)
& cC22(U_119) )
| ~ cC158(U_119) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
cnf(f_33_4,plain,
( cC22(U_119)
| ~ cC158(U_119) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_5,plain,
( cC156(U_119)
| ~ cC158(U_119) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_6,plain,
( cC158(U_120)
| ~ cC156(U_120)
| ~ cC22(U_120) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [X] :
( ( cC16(X)
| ~ cC10(X)
| ~ cC14(X) )
& ( ( cC10(X)
& cC14(X) )
| ~ cC16(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_33]) ).
fof(f_34_2,plain,
! [U_121] :
( ( cC16(U_121)
| ~ cC10(U_121)
| ~ cC14(U_121) )
& ( ( cC10(U_121)
& cC14(U_121) )
| ~ cC16(U_121) ) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
( ! [U_123] :
( cC16(U_123)
| ~ cC10(U_123)
| ~ cC14(U_123) )
& ! [U_122] :
( ( cC10(U_122)
& cC14(U_122) )
| ~ cC16(U_122) ) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
cnf(f_34_4,plain,
( cC14(U_122)
| ~ cC16(U_122) ),
inference(clausify,[status(thm)],[f_34_3]) ).
cnf(f_34_5,plain,
( cC10(U_122)
| ~ cC16(U_122) ),
inference(clausify,[status(thm)],[f_34_3]) ).
cnf(f_34_6,plain,
( cC16(U_123)
| ~ cC10(U_123)
| ~ cC14(U_123) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_35_1,plain,
! [X] :
( ( cC160(X)
| ! [Y] :
( cC6(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) )
| ~ cC160(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_34]) ).
fof(f_35_2,plain,
! [U_126] :
( ( cC160(U_126)
| ! [U_125] :
( cC6(U_125)
| ~ rR1(U_126,U_125) ) )
& ( ? [U_124] :
( ~ cC6(U_124)
& rR1(U_126,U_124) )
| ~ cC160(U_126) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_128] :
( cC160(U_128)
| ! [U_125] :
( cC6(U_125)
| ~ rR1(U_128,U_125) ) )
& ! [U_127] :
( ? [U_124] :
( ~ cC6(U_124)
& rR1(U_127,U_124) )
| ~ cC160(U_127) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
fof(f_35_4,plain,
( ! [U_128] :
( cC160(U_128)
| ! [U_125] :
( cC6(U_125)
| ~ rR1(U_128,U_125) ) )
& ! [U_127] :
( ( ~ cC6(sK12(U_127))
& rR1(U_127,sK12(U_127)) )
| ~ cC160(U_127) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_124,sK12(U_127))],[f_35_3]) ).
cnf(f_35_5,plain,
( rR1(U_127,sK12(U_127))
| ~ cC160(U_127) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_6,plain,
( ~ cC6(sK12(U_127))
| ~ cC160(U_127) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_7,plain,
( cC160(U_128)
| cC6(U_125)
| ~ rR1(U_128,U_125) ),
inference(clausify,[status(thm)],[f_35_4]) ).
fof(f_36_1,plain,
! [X] :
( ( cC162(X)
| ! [Y] :
( ~ cC160(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC160(Y)
& rR1(X,Y) )
| ~ cC162(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_35]) ).
fof(f_36_2,plain,
! [U_131] :
( ( cC162(U_131)
| ! [U_130] :
( ~ cC160(U_130)
| ~ rR1(U_131,U_130) ) )
& ( ? [U_129] :
( cC160(U_129)
& rR1(U_131,U_129) )
| ~ cC162(U_131) ) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_133] :
( cC162(U_133)
| ! [U_130] :
( ~ cC160(U_130)
| ~ rR1(U_133,U_130) ) )
& ! [U_132] :
( ? [U_129] :
( cC160(U_129)
& rR1(U_132,U_129) )
| ~ cC162(U_132) ) ),
inference(miniscope,[status(thm)],[f_36_2]) ).
fof(f_36_4,plain,
( ! [U_133] :
( cC162(U_133)
| ! [U_130] :
( ~ cC160(U_130)
| ~ rR1(U_133,U_130) ) )
& ! [U_132] :
( ( cC160(sK13(U_132))
& rR1(U_132,sK13(U_132)) )
| ~ cC162(U_132) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_129,sK13(U_132))],[f_36_3]) ).
cnf(f_36_5,plain,
( rR1(U_132,sK13(U_132))
| ~ cC162(U_132) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_6,plain,
( cC160(sK13(U_132))
| ~ cC162(U_132) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_7,plain,
( cC162(U_133)
| ~ cC160(U_130)
| ~ rR1(U_133,U_130) ),
inference(clausify,[status(thm)],[f_36_4]) ).
fof(f_37_1,plain,
! [X] :
( ( cC164(X)
| ! [Y] :
( cC92(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC92(Y)
& rR1(X,Y) )
| ~ cC164(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_36]) ).
fof(f_37_2,plain,
! [U_136] :
( ( cC164(U_136)
| ! [U_135] :
( cC92(U_135)
| ~ rR1(U_136,U_135) ) )
& ( ? [U_134] :
( ~ cC92(U_134)
& rR1(U_136,U_134) )
| ~ cC164(U_136) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_138] :
( cC164(U_138)
| ! [U_135] :
( cC92(U_135)
| ~ rR1(U_138,U_135) ) )
& ! [U_137] :
( ? [U_134] :
( ~ cC92(U_134)
& rR1(U_137,U_134) )
| ~ cC164(U_137) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
fof(f_37_4,plain,
( ! [U_138] :
( cC164(U_138)
| ! [U_135] :
( cC92(U_135)
| ~ rR1(U_138,U_135) ) )
& ! [U_137] :
( ( ~ cC92(sK14(U_137))
& rR1(U_137,sK14(U_137)) )
| ~ cC164(U_137) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_134,sK14(U_137))],[f_37_3]) ).
cnf(f_37_5,plain,
( rR1(U_137,sK14(U_137))
| ~ cC164(U_137) ),
inference(clausify,[status(thm)],[f_37_4]) ).
cnf(f_37_6,plain,
( ~ cC92(sK14(U_137))
| ~ cC164(U_137) ),
inference(clausify,[status(thm)],[f_37_4]) ).
cnf(f_37_7,plain,
( cC164(U_138)
| cC92(U_135)
| ~ rR1(U_138,U_135) ),
inference(clausify,[status(thm)],[f_37_4]) ).
fof(f_38_1,plain,
! [X] :
( ( cC166(X)
| ! [Y] :
( ~ cC164(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC164(Y)
& rR1(X,Y) )
| ~ cC166(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_37]) ).
fof(f_38_2,plain,
! [U_141] :
( ( cC166(U_141)
| ! [U_140] :
( ~ cC164(U_140)
| ~ rR1(U_141,U_140) ) )
& ( ? [U_139] :
( cC164(U_139)
& rR1(U_141,U_139) )
| ~ cC166(U_141) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_143] :
( cC166(U_143)
| ! [U_140] :
( ~ cC164(U_140)
| ~ rR1(U_143,U_140) ) )
& ! [U_142] :
( ? [U_139] :
( cC164(U_139)
& rR1(U_142,U_139) )
| ~ cC166(U_142) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
fof(f_38_4,plain,
( ! [U_143] :
( cC166(U_143)
| ! [U_140] :
( ~ cC164(U_140)
| ~ rR1(U_143,U_140) ) )
& ! [U_142] :
( ( cC164(sK15(U_142))
& rR1(U_142,sK15(U_142)) )
| ~ cC166(U_142) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_139,sK15(U_142))],[f_38_3]) ).
cnf(f_38_5,plain,
( rR1(U_142,sK15(U_142))
| ~ cC166(U_142) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_6,plain,
( cC164(sK15(U_142))
| ~ cC166(U_142) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_7,plain,
( cC166(U_143)
| ~ cC164(U_140)
| ~ rR1(U_143,U_140) ),
inference(clausify,[status(thm)],[f_38_4]) ).
fof(f_39_1,plain,
! [X] :
( ( cC168(X)
| cC162(X)
| cC166(X) )
& ( ( ~ cC162(X)
& ~ cC166(X) )
| ~ cC168(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_38]) ).
fof(f_39_2,plain,
! [U_144] :
( ( cC168(U_144)
| cC162(U_144)
| cC166(U_144) )
& ( ( ~ cC162(U_144)
& ~ cC166(U_144) )
| ~ cC168(U_144) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_146] :
( cC168(U_146)
| cC162(U_146)
| cC166(U_146) )
& ! [U_145] :
( ( ~ cC162(U_145)
& ~ cC166(U_145) )
| ~ cC168(U_145) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( ~ cC166(U_145)
| ~ cC168(U_145) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_5,plain,
( ~ cC162(U_145)
| ~ cC168(U_145) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_6,plain,
( cC168(U_146)
| cC162(U_146)
| cC166(U_146) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [X] :
( ( cC170(X)
| ! [Y] :
( cC18(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC18(Y)
& rR1(X,Y) )
| ~ cC170(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_39]) ).
fof(f_40_2,plain,
! [U_149] :
( ( cC170(U_149)
| ! [U_148] :
( cC18(U_148)
| ~ rR1(U_149,U_148) ) )
& ( ? [U_147] :
( ~ cC18(U_147)
& rR1(U_149,U_147) )
| ~ cC170(U_149) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_151] :
( cC170(U_151)
| ! [U_148] :
( cC18(U_148)
| ~ rR1(U_151,U_148) ) )
& ! [U_150] :
( ? [U_147] :
( ~ cC18(U_147)
& rR1(U_150,U_147) )
| ~ cC170(U_150) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
fof(f_40_4,plain,
( ! [U_151] :
( cC170(U_151)
| ! [U_148] :
( cC18(U_148)
| ~ rR1(U_151,U_148) ) )
& ! [U_150] :
( ( ~ cC18(sK16(U_150))
& rR1(U_150,sK16(U_150)) )
| ~ cC170(U_150) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_147,sK16(U_150))],[f_40_3]) ).
cnf(f_40_5,plain,
( rR1(U_150,sK16(U_150))
| ~ cC170(U_150) ),
inference(clausify,[status(thm)],[f_40_4]) ).
cnf(f_40_6,plain,
( ~ cC18(sK16(U_150))
| ~ cC170(U_150) ),
inference(clausify,[status(thm)],[f_40_4]) ).
cnf(f_40_7,plain,
( cC170(U_151)
| cC18(U_148)
| ~ rR1(U_151,U_148) ),
inference(clausify,[status(thm)],[f_40_4]) ).
fof(f_41_1,plain,
! [X] :
( ( cC172(X)
| ! [Y] :
( ~ cC170(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC170(Y)
& rR1(X,Y) )
| ~ cC172(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_154] :
( ( cC172(U_154)
| ! [U_153] :
( ~ cC170(U_153)
| ~ rR1(U_154,U_153) ) )
& ( ? [U_152] :
( cC170(U_152)
& rR1(U_154,U_152) )
| ~ cC172(U_154) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_156] :
( cC172(U_156)
| ! [U_153] :
( ~ cC170(U_153)
| ~ rR1(U_156,U_153) ) )
& ! [U_155] :
( ? [U_152] :
( cC170(U_152)
& rR1(U_155,U_152) )
| ~ cC172(U_155) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
fof(f_41_4,plain,
( ! [U_156] :
( cC172(U_156)
| ! [U_153] :
( ~ cC170(U_153)
| ~ rR1(U_156,U_153) ) )
& ! [U_155] :
( ( cC170(sK17(U_155))
& rR1(U_155,sK17(U_155)) )
| ~ cC172(U_155) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_152,sK17(U_155))],[f_41_3]) ).
cnf(f_41_5,plain,
( rR1(U_155,sK17(U_155))
| ~ cC172(U_155) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_6,plain,
( cC170(sK17(U_155))
| ~ cC172(U_155) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_7,plain,
( cC172(U_156)
| ~ cC170(U_153)
| ~ rR1(U_156,U_153) ),
inference(clausify,[status(thm)],[f_41_4]) ).
fof(f_42_1,plain,
! [X] :
( ( cC174(X)
| cC172(X)
| ~ cC168(X) )
& ( ( ~ cC172(X)
& cC168(X) )
| ~ cC174(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_41]) ).
fof(f_42_2,plain,
! [U_157] :
( ( cC174(U_157)
| cC172(U_157)
| ~ cC168(U_157) )
& ( ( ~ cC172(U_157)
& cC168(U_157) )
| ~ cC174(U_157) ) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
( ! [U_159] :
( cC174(U_159)
| cC172(U_159)
| ~ cC168(U_159) )
& ! [U_158] :
( ( ~ cC172(U_158)
& cC168(U_158) )
| ~ cC174(U_158) ) ),
inference(miniscope,[status(thm)],[f_42_2]) ).
cnf(f_42_4,plain,
( cC168(U_158)
| ~ cC174(U_158) ),
inference(clausify,[status(thm)],[f_42_3]) ).
cnf(f_42_5,plain,
( ~ cC172(U_158)
| ~ cC174(U_158) ),
inference(clausify,[status(thm)],[f_42_3]) ).
cnf(f_42_6,plain,
( cC174(U_159)
| cC172(U_159)
| ~ cC168(U_159) ),
inference(clausify,[status(thm)],[f_42_3]) ).
fof(f_43_1,plain,
! [X] :
( ( cC176(X)
| ! [Y] :
( cC100(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC100(Y)
& rR1(X,Y) )
| ~ cC176(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_42]) ).
fof(f_43_2,plain,
! [U_162] :
( ( cC176(U_162)
| ! [U_161] :
( cC100(U_161)
| ~ rR1(U_162,U_161) ) )
& ( ? [U_160] :
( ~ cC100(U_160)
& rR1(U_162,U_160) )
| ~ cC176(U_162) ) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
( ! [U_164] :
( cC176(U_164)
| ! [U_161] :
( cC100(U_161)
| ~ rR1(U_164,U_161) ) )
& ! [U_163] :
( ? [U_160] :
( ~ cC100(U_160)
& rR1(U_163,U_160) )
| ~ cC176(U_163) ) ),
inference(miniscope,[status(thm)],[f_43_2]) ).
fof(f_43_4,plain,
( ! [U_164] :
( cC176(U_164)
| ! [U_161] :
( cC100(U_161)
| ~ rR1(U_164,U_161) ) )
& ! [U_163] :
( ( ~ cC100(sK18(U_163))
& rR1(U_163,sK18(U_163)) )
| ~ cC176(U_163) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_160,sK18(U_163))],[f_43_3]) ).
cnf(f_43_5,plain,
( rR1(U_163,sK18(U_163))
| ~ cC176(U_163) ),
inference(clausify,[status(thm)],[f_43_4]) ).
cnf(f_43_6,plain,
( ~ cC100(sK18(U_163))
| ~ cC176(U_163) ),
inference(clausify,[status(thm)],[f_43_4]) ).
cnf(f_43_7,plain,
( cC176(U_164)
| cC100(U_161)
| ~ rR1(U_164,U_161) ),
inference(clausify,[status(thm)],[f_43_4]) ).
fof(f_44_1,plain,
! [X] :
( ( cC178(X)
| ! [Y] :
( ~ cC176(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC176(Y)
& rR1(X,Y) )
| ~ cC178(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_167] :
( ( cC178(U_167)
| ! [U_166] :
( ~ cC176(U_166)
| ~ rR1(U_167,U_166) ) )
& ( ? [U_165] :
( cC176(U_165)
& rR1(U_167,U_165) )
| ~ cC178(U_167) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_169] :
( cC178(U_169)
| ! [U_166] :
( ~ cC176(U_166)
| ~ rR1(U_169,U_166) ) )
& ! [U_168] :
( ? [U_165] :
( cC176(U_165)
& rR1(U_168,U_165) )
| ~ cC178(U_168) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
fof(f_44_4,plain,
( ! [U_169] :
( cC178(U_169)
| ! [U_166] :
( ~ cC176(U_166)
| ~ rR1(U_169,U_166) ) )
& ! [U_168] :
( ( cC176(sK19(U_168))
& rR1(U_168,sK19(U_168)) )
| ~ cC178(U_168) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_165,sK19(U_168))],[f_44_3]) ).
cnf(f_44_5,plain,
( rR1(U_168,sK19(U_168))
| ~ cC178(U_168) ),
inference(clausify,[status(thm)],[f_44_4]) ).
cnf(f_44_6,plain,
( cC176(sK19(U_168))
| ~ cC178(U_168) ),
inference(clausify,[status(thm)],[f_44_4]) ).
cnf(f_44_7,plain,
( cC178(U_169)
| ~ cC176(U_166)
| ~ rR1(U_169,U_166) ),
inference(clausify,[status(thm)],[f_44_4]) ).
fof(f_45_1,plain,
! [X] :
( ( cC180(X)
| ~ cC174(X)
| cC178(X) )
& ( ( cC174(X)
& ~ cC178(X) )
| ~ cC180(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_44]) ).
fof(f_45_2,plain,
! [U_170] :
( ( cC180(U_170)
| ~ cC174(U_170)
| cC178(U_170) )
& ( ( cC174(U_170)
& ~ cC178(U_170) )
| ~ cC180(U_170) ) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
( ! [U_172] :
( cC180(U_172)
| ~ cC174(U_172)
| cC178(U_172) )
& ! [U_171] :
( ( cC174(U_171)
& ~ cC178(U_171) )
| ~ cC180(U_171) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
cnf(f_45_4,plain,
( ~ cC178(U_171)
| ~ cC180(U_171) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_5,plain,
( cC174(U_171)
| ~ cC180(U_171) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_6,plain,
( cC180(U_172)
| ~ cC174(U_172)
| cC178(U_172) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [X] :
( ( cC20(X)
| ! [Y] :
( cC18(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC18(Y)
& rR1(X,Y) )
| ~ cC20(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_45]) ).
fof(f_46_2,plain,
! [U_175] :
( ( cC20(U_175)
| ! [U_174] :
( cC18(U_174)
| ~ rR1(U_175,U_174) ) )
& ( ? [U_173] :
( ~ cC18(U_173)
& rR1(U_175,U_173) )
| ~ cC20(U_175) ) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_177] :
( cC20(U_177)
| ! [U_174] :
( cC18(U_174)
| ~ rR1(U_177,U_174) ) )
& ! [U_176] :
( ? [U_173] :
( ~ cC18(U_173)
& rR1(U_176,U_173) )
| ~ cC20(U_176) ) ),
inference(miniscope,[status(thm)],[f_46_2]) ).
fof(f_46_4,plain,
( ! [U_177] :
( cC20(U_177)
| ! [U_174] :
( cC18(U_174)
| ~ rR1(U_177,U_174) ) )
& ! [U_176] :
( ( ~ cC18(sK20(U_176))
& rR1(U_176,sK20(U_176)) )
| ~ cC20(U_176) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_173,sK20(U_176))],[f_46_3]) ).
cnf(f_46_5,plain,
( rR1(U_176,sK20(U_176))
| ~ cC20(U_176) ),
inference(clausify,[status(thm)],[f_46_4]) ).
cnf(f_46_6,plain,
( ~ cC18(sK20(U_176))
| ~ cC20(U_176) ),
inference(clausify,[status(thm)],[f_46_4]) ).
cnf(f_46_7,plain,
( cC20(U_177)
| cC18(U_174)
| ~ rR1(U_177,U_174) ),
inference(clausify,[status(thm)],[f_46_4]) ).
fof(f_47_1,plain,
! [X] :
( ( cC22(X)
| ~ cC20(X)
| ~ cC16(X) )
& ( ( cC20(X)
& cC16(X) )
| ~ cC22(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_46]) ).
fof(f_47_2,plain,
! [U_178] :
( ( cC22(U_178)
| ~ cC20(U_178)
| ~ cC16(U_178) )
& ( ( cC20(U_178)
& cC16(U_178) )
| ~ cC22(U_178) ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_180] :
( cC22(U_180)
| ~ cC20(U_180)
| ~ cC16(U_180) )
& ! [U_179] :
( ( cC20(U_179)
& cC16(U_179) )
| ~ cC22(U_179) ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
cnf(f_47_4,plain,
( cC16(U_179)
| ~ cC22(U_179) ),
inference(clausify,[status(thm)],[f_47_3]) ).
cnf(f_47_5,plain,
( cC20(U_179)
| ~ cC22(U_179) ),
inference(clausify,[status(thm)],[f_47_3]) ).
cnf(f_47_6,plain,
( cC22(U_180)
| ~ cC20(U_180)
| ~ cC16(U_180) ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [X] :
( ( cC24(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC24(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_47]) ).
fof(f_48_2,plain,
! [U_183] :
( ( cC24(U_183)
| ! [U_182] :
( cC2(U_182)
| ~ rR1(U_183,U_182) ) )
& ( ? [U_181] :
( ~ cC2(U_181)
& rR1(U_183,U_181) )
| ~ cC24(U_183) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_185] :
( cC24(U_185)
| ! [U_182] :
( cC2(U_182)
| ~ rR1(U_185,U_182) ) )
& ! [U_184] :
( ? [U_181] :
( ~ cC2(U_181)
& rR1(U_184,U_181) )
| ~ cC24(U_184) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
fof(f_48_4,plain,
( ! [U_185] :
( cC24(U_185)
| ! [U_182] :
( cC2(U_182)
| ~ rR1(U_185,U_182) ) )
& ! [U_184] :
( ( ~ cC2(sK21(U_184))
& rR1(U_184,sK21(U_184)) )
| ~ cC24(U_184) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_181,sK21(U_184))],[f_48_3]) ).
cnf(f_48_5,plain,
( rR1(U_184,sK21(U_184))
| ~ cC24(U_184) ),
inference(clausify,[status(thm)],[f_48_4]) ).
cnf(f_48_6,plain,
( ~ cC2(sK21(U_184))
| ~ cC24(U_184) ),
inference(clausify,[status(thm)],[f_48_4]) ).
cnf(f_48_7,plain,
( cC24(U_185)
| cC2(U_182)
| ~ rR1(U_185,U_182) ),
inference(clausify,[status(thm)],[f_48_4]) ).
fof(f_49_1,plain,
! [X] :
( ( cC26(X)
| cC2(X)
| cC24(X) )
& ( ( ~ cC2(X)
& ~ cC24(X) )
| ~ cC26(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_48]) ).
fof(f_49_2,plain,
! [U_186] :
( ( cC26(U_186)
| cC2(U_186)
| cC24(U_186) )
& ( ( ~ cC2(U_186)
& ~ cC24(U_186) )
| ~ cC26(U_186) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_188] :
( cC26(U_188)
| cC2(U_188)
| cC24(U_188) )
& ! [U_187] :
( ( ~ cC2(U_187)
& ~ cC24(U_187) )
| ~ cC26(U_187) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
cnf(f_49_4,plain,
( ~ cC24(U_187)
| ~ cC26(U_187) ),
inference(clausify,[status(thm)],[f_49_3]) ).
cnf(f_49_5,plain,
( ~ cC2(U_187)
| ~ cC26(U_187) ),
inference(clausify,[status(thm)],[f_49_3]) ).
cnf(f_49_6,plain,
( cC26(U_188)
| cC2(U_188)
| cC24(U_188) ),
inference(clausify,[status(thm)],[f_49_3]) ).
fof(f_50_1,plain,
! [X] :
( ( cC28(X)
| ! [Y] :
( ~ cC26(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC26(Y)
& rR1(X,Y) )
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_49]) ).
fof(f_50_2,plain,
! [U_191] :
( ( cC28(U_191)
| ! [U_190] :
( ~ cC26(U_190)
| ~ rR1(U_191,U_190) ) )
& ( ? [U_189] :
( cC26(U_189)
& rR1(U_191,U_189) )
| ~ cC28(U_191) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_193] :
( cC28(U_193)
| ! [U_190] :
( ~ cC26(U_190)
| ~ rR1(U_193,U_190) ) )
& ! [U_192] :
( ? [U_189] :
( cC26(U_189)
& rR1(U_192,U_189) )
| ~ cC28(U_192) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
fof(f_50_4,plain,
( ! [U_193] :
( cC28(U_193)
| ! [U_190] :
( ~ cC26(U_190)
| ~ rR1(U_193,U_190) ) )
& ! [U_192] :
( ( cC26(sK22(U_192))
& rR1(U_192,sK22(U_192)) )
| ~ cC28(U_192) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_189,sK22(U_192))],[f_50_3]) ).
cnf(f_50_5,plain,
( rR1(U_192,sK22(U_192))
| ~ cC28(U_192) ),
inference(clausify,[status(thm)],[f_50_4]) ).
cnf(f_50_6,plain,
( cC26(sK22(U_192))
| ~ cC28(U_192) ),
inference(clausify,[status(thm)],[f_50_4]) ).
cnf(f_50_7,plain,
( cC28(U_193)
| ~ cC26(U_190)
| ~ rR1(U_193,U_190) ),
inference(clausify,[status(thm)],[f_50_4]) ).
fof(f_51_1,plain,
! [X] :
( ( cC30(X)
| ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC30(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_50]) ).
fof(f_51_2,plain,
! [U_196] :
( ( cC30(U_196)
| ! [U_195] :
( cC12(U_195)
| ~ rR1(U_196,U_195) ) )
& ( ? [U_194] :
( ~ cC12(U_194)
& rR1(U_196,U_194) )
| ~ cC30(U_196) ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_198] :
( cC30(U_198)
| ! [U_195] :
( cC12(U_195)
| ~ rR1(U_198,U_195) ) )
& ! [U_197] :
( ? [U_194] :
( ~ cC12(U_194)
& rR1(U_197,U_194) )
| ~ cC30(U_197) ) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
fof(f_51_4,plain,
( ! [U_198] :
( cC30(U_198)
| ! [U_195] :
( cC12(U_195)
| ~ rR1(U_198,U_195) ) )
& ! [U_197] :
( ( ~ cC12(sK23(U_197))
& rR1(U_197,sK23(U_197)) )
| ~ cC30(U_197) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_194,sK23(U_197))],[f_51_3]) ).
cnf(f_51_5,plain,
( rR1(U_197,sK23(U_197))
| ~ cC30(U_197) ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_6,plain,
( ~ cC12(sK23(U_197))
| ~ cC30(U_197) ),
inference(clausify,[status(thm)],[f_51_4]) ).
cnf(f_51_7,plain,
( cC30(U_198)
| cC12(U_195)
| ~ rR1(U_198,U_195) ),
inference(clausify,[status(thm)],[f_51_4]) ).
fof(f_52_1,plain,
! [X] :
( ( cC32(X)
| cC30(X)
| cC2(X) )
& ( ( ~ cC30(X)
& ~ cC2(X) )
| ~ cC32(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_51]) ).
fof(f_52_2,plain,
! [U_199] :
( ( cC32(U_199)
| cC30(U_199)
| cC2(U_199) )
& ( ( ~ cC30(U_199)
& ~ cC2(U_199) )
| ~ cC32(U_199) ) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_201] :
( cC32(U_201)
| cC30(U_201)
| cC2(U_201) )
& ! [U_200] :
( ( ~ cC30(U_200)
& ~ cC2(U_200) )
| ~ cC32(U_200) ) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
cnf(f_52_4,plain,
( ~ cC2(U_200)
| ~ cC32(U_200) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_5,plain,
( ~ cC30(U_200)
| ~ cC32(U_200) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_6,plain,
( cC32(U_201)
| cC30(U_201)
| cC2(U_201) ),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_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_52]) ).
fof(f_53_2,plain,
! [U_204] :
( ( cC34(U_204)
| ! [U_203] :
( ~ cC32(U_203)
| ~ rR1(U_204,U_203) ) )
& ( ? [U_202] :
( cC32(U_202)
& rR1(U_204,U_202) )
| ~ cC34(U_204) ) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_206] :
( cC34(U_206)
| ! [U_203] :
( ~ cC32(U_203)
| ~ rR1(U_206,U_203) ) )
& ! [U_205] :
( ? [U_202] :
( cC32(U_202)
& rR1(U_205,U_202) )
| ~ cC34(U_205) ) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
fof(f_53_4,plain,
( ! [U_206] :
( cC34(U_206)
| ! [U_203] :
( ~ cC32(U_203)
| ~ rR1(U_206,U_203) ) )
& ! [U_205] :
( ( cC32(sK24(U_205))
& rR1(U_205,sK24(U_205)) )
| ~ cC34(U_205) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_202,sK24(U_205))],[f_53_3]) ).
cnf(f_53_5,plain,
( rR1(U_205,sK24(U_205))
| ~ cC34(U_205) ),
inference(clausify,[status(thm)],[f_53_4]) ).
cnf(f_53_6,plain,
( cC32(sK24(U_205))
| ~ cC34(U_205) ),
inference(clausify,[status(thm)],[f_53_4]) ).
cnf(f_53_7,plain,
( cC34(U_206)
| ~ cC32(U_203)
| ~ rR1(U_206,U_203) ),
inference(clausify,[status(thm)],[f_53_4]) ).
fof(f_54_1,plain,
! [X] :
( ( cC36(X)
| cC34(X)
| cC28(X) )
& ( ( ~ cC34(X)
& ~ cC28(X) )
| ~ cC36(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_53]) ).
fof(f_54_2,plain,
! [U_207] :
( ( cC36(U_207)
| cC34(U_207)
| cC28(U_207) )
& ( ( ~ cC34(U_207)
& ~ cC28(U_207) )
| ~ cC36(U_207) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_209] :
( cC36(U_209)
| cC34(U_209)
| cC28(U_209) )
& ! [U_208] :
( ( ~ cC34(U_208)
& ~ cC28(U_208) )
| ~ cC36(U_208) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( ~ cC28(U_208)
| ~ cC36(U_208) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( ~ cC34(U_208)
| ~ cC36(U_208) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_6,plain,
( cC36(U_209)
| cC34(U_209)
| cC28(U_209) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [X] :
( ( cC38(X)
| ~ cTOP(X)
| ~ cC36(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_54]) ).
fof(f_55_2,plain,
! [U_210] :
( ( cC38(U_210)
| ~ cTOP(U_210)
| ~ cC36(U_210) )
& ( ( cTOP(U_210)
& cC36(U_210) )
| ~ cC38(U_210) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_212] :
( cC38(U_212)
| ~ cTOP(U_212)
| ~ cC36(U_212) )
& ! [U_211] :
( ( cTOP(U_211)
& cC36(U_211) )
| ~ cC38(U_211) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
cnf(f_55_4,plain,
( cC36(U_211)
| ~ cC38(U_211) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_5,plain,
( cTOP(U_211)
| ~ cC38(U_211) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_6,plain,
( cC38(U_212)
| ~ cTOP(U_212)
| ~ cC36(U_212) ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_56_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_55]) ).
fof(f_56_2,plain,
! [U_215] :
( ( cC4(U_215)
| ! [U_214] :
( cC2(U_214)
| ~ rR1(U_215,U_214) ) )
& ( ? [U_213] :
( ~ cC2(U_213)
& rR1(U_215,U_213) )
| ~ cC4(U_215) ) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
( ! [U_217] :
( cC4(U_217)
| ! [U_214] :
( cC2(U_214)
| ~ rR1(U_217,U_214) ) )
& ! [U_216] :
( ? [U_213] :
( ~ cC2(U_213)
& rR1(U_216,U_213) )
| ~ cC4(U_216) ) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
fof(f_56_4,plain,
( ! [U_217] :
( cC4(U_217)
| ! [U_214] :
( cC2(U_214)
| ~ rR1(U_217,U_214) ) )
& ! [U_216] :
( ( ~ cC2(sK25(U_216))
& rR1(U_216,sK25(U_216)) )
| ~ cC4(U_216) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_213,sK25(U_216))],[f_56_3]) ).
cnf(f_56_5,plain,
( rR1(U_216,sK25(U_216))
| ~ cC4(U_216) ),
inference(clausify,[status(thm)],[f_56_4]) ).
cnf(f_56_6,plain,
( ~ cC2(sK25(U_216))
| ~ cC4(U_216) ),
inference(clausify,[status(thm)],[f_56_4]) ).
cnf(f_56_7,plain,
( cC4(U_217)
| cC2(U_214)
| ~ rR1(U_217,U_214) ),
inference(clausify,[status(thm)],[f_56_4]) ).
fof(f_57_1,plain,
! [X] :
( ( cC40(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_56]) ).
fof(f_57_2,plain,
! [U_218] :
( ( cC40(U_218)
| ~ cTOP(U_218) )
& ( cTOP(U_218)
| ~ cC40(U_218) ) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
( ! [U_220] :
( cC40(U_220)
| ~ cTOP(U_220) )
& ! [U_219] :
( cTOP(U_219)
| ~ cC40(U_219) ) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( cTOP(U_219)
| ~ cC40(U_219) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( cC40(U_220)
| ~ cTOP(U_220) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [X] :
( ( cC42(X)
| ~ cC38(X)
| ~ cC40(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_57]) ).
fof(f_58_2,plain,
! [U_221] :
( ( cC42(U_221)
| ~ cC38(U_221)
| ~ cC40(U_221) )
& ( ( cC38(U_221)
& cC40(U_221) )
| ~ cC42(U_221) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_223] :
( cC42(U_223)
| ~ cC38(U_223)
| ~ cC40(U_223) )
& ! [U_222] :
( ( cC38(U_222)
& cC40(U_222) )
| ~ cC42(U_222) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_4,plain,
( cC40(U_222)
| ~ cC42(U_222) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( cC38(U_222)
| ~ cC42(U_222) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_6,plain,
( cC42(U_223)
| ~ cC38(U_223)
| ~ cC40(U_223) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_1,plain,
! [X] :
( ( cC44(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC44(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_58]) ).
fof(f_59_2,plain,
! [U_226] :
( ( cC44(U_226)
| ! [U_225] :
( cC2(U_225)
| ~ rR1(U_226,U_225) ) )
& ( ? [U_224] :
( ~ cC2(U_224)
& rR1(U_226,U_224) )
| ~ cC44(U_226) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_228] :
( cC44(U_228)
| ! [U_225] :
( cC2(U_225)
| ~ rR1(U_228,U_225) ) )
& ! [U_227] :
( ? [U_224] :
( ~ cC2(U_224)
& rR1(U_227,U_224) )
| ~ cC44(U_227) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
fof(f_59_4,plain,
( ! [U_228] :
( cC44(U_228)
| ! [U_225] :
( cC2(U_225)
| ~ rR1(U_228,U_225) ) )
& ! [U_227] :
( ( ~ cC2(sK26(U_227))
& rR1(U_227,sK26(U_227)) )
| ~ cC44(U_227) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_224,sK26(U_227))],[f_59_3]) ).
cnf(f_59_5,plain,
( rR1(U_227,sK26(U_227))
| ~ cC44(U_227) ),
inference(clausify,[status(thm)],[f_59_4]) ).
cnf(f_59_6,plain,
( ~ cC2(sK26(U_227))
| ~ cC44(U_227) ),
inference(clausify,[status(thm)],[f_59_4]) ).
cnf(f_59_7,plain,
( cC44(U_228)
| cC2(U_225)
| ~ rR1(U_228,U_225) ),
inference(clausify,[status(thm)],[f_59_4]) ).
fof(f_60_1,plain,
! [X] :
( ( cC46(X)
| cC44(X)
| cC12(X) )
& ( ( ~ cC44(X)
& ~ cC12(X) )
| ~ cC46(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_59]) ).
fof(f_60_2,plain,
! [U_229] :
( ( cC46(U_229)
| cC44(U_229)
| cC12(U_229) )
& ( ( ~ cC44(U_229)
& ~ cC12(U_229) )
| ~ cC46(U_229) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_231] :
( cC46(U_231)
| cC44(U_231)
| cC12(U_231) )
& ! [U_230] :
( ( ~ cC44(U_230)
& ~ cC12(U_230) )
| ~ cC46(U_230) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
cnf(f_60_4,plain,
( ~ cC12(U_230)
| ~ cC46(U_230) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_5,plain,
( ~ cC44(U_230)
| ~ cC46(U_230) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_6,plain,
( cC46(U_231)
| cC44(U_231)
| cC12(U_231) ),
inference(clausify,[status(thm)],[f_60_3]) ).
fof(f_61_1,plain,
! [X] :
( ( cC48(X)
| ! [Y] :
( ~ cC46(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC46(Y)
& rR1(X,Y) )
| ~ cC48(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_60]) ).
fof(f_61_2,plain,
! [U_234] :
( ( cC48(U_234)
| ! [U_233] :
( ~ cC46(U_233)
| ~ rR1(U_234,U_233) ) )
& ( ? [U_232] :
( cC46(U_232)
& rR1(U_234,U_232) )
| ~ cC48(U_234) ) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
( ! [U_236] :
( cC48(U_236)
| ! [U_233] :
( ~ cC46(U_233)
| ~ rR1(U_236,U_233) ) )
& ! [U_235] :
( ? [U_232] :
( cC46(U_232)
& rR1(U_235,U_232) )
| ~ cC48(U_235) ) ),
inference(miniscope,[status(thm)],[f_61_2]) ).
fof(f_61_4,plain,
( ! [U_236] :
( cC48(U_236)
| ! [U_233] :
( ~ cC46(U_233)
| ~ rR1(U_236,U_233) ) )
& ! [U_235] :
( ( cC46(sK27(U_235))
& rR1(U_235,sK27(U_235)) )
| ~ cC48(U_235) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_232,sK27(U_235))],[f_61_3]) ).
cnf(f_61_5,plain,
( rR1(U_235,sK27(U_235))
| ~ cC48(U_235) ),
inference(clausify,[status(thm)],[f_61_4]) ).
cnf(f_61_6,plain,
( cC46(sK27(U_235))
| ~ cC48(U_235) ),
inference(clausify,[status(thm)],[f_61_4]) ).
cnf(f_61_7,plain,
( cC48(U_236)
| ~ cC46(U_233)
| ~ rR1(U_236,U_233) ),
inference(clausify,[status(thm)],[f_61_4]) ).
fof(f_62_1,plain,
! [X] :
( ( cC50(X)
| ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC50(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_61]) ).
fof(f_62_2,plain,
! [U_239] :
( ( cC50(U_239)
| ! [U_238] :
( cC12(U_238)
| ~ rR1(U_239,U_238) ) )
& ( ? [U_237] :
( ~ cC12(U_237)
& rR1(U_239,U_237) )
| ~ cC50(U_239) ) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
fof(f_62_3,plain,
( ! [U_241] :
( cC50(U_241)
| ! [U_238] :
( cC12(U_238)
| ~ rR1(U_241,U_238) ) )
& ! [U_240] :
( ? [U_237] :
( ~ cC12(U_237)
& rR1(U_240,U_237) )
| ~ cC50(U_240) ) ),
inference(miniscope,[status(thm)],[f_62_2]) ).
fof(f_62_4,plain,
( ! [U_241] :
( cC50(U_241)
| ! [U_238] :
( cC12(U_238)
| ~ rR1(U_241,U_238) ) )
& ! [U_240] :
( ( ~ cC12(sK28(U_240))
& rR1(U_240,sK28(U_240)) )
| ~ cC50(U_240) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_237,sK28(U_240))],[f_62_3]) ).
cnf(f_62_5,plain,
( rR1(U_240,sK28(U_240))
| ~ cC50(U_240) ),
inference(clausify,[status(thm)],[f_62_4]) ).
cnf(f_62_6,plain,
( ~ cC12(sK28(U_240))
| ~ cC50(U_240) ),
inference(clausify,[status(thm)],[f_62_4]) ).
cnf(f_62_7,plain,
( cC50(U_241)
| cC12(U_238)
| ~ rR1(U_241,U_238) ),
inference(clausify,[status(thm)],[f_62_4]) ).
fof(f_63_1,plain,
! [X] :
( ( cC52(X)
| cC50(X)
| cC12(X) )
& ( ( ~ cC50(X)
& ~ cC12(X) )
| ~ cC52(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_62]) ).
fof(f_63_2,plain,
! [U_242] :
( ( cC52(U_242)
| cC50(U_242)
| cC12(U_242) )
& ( ( ~ cC50(U_242)
& ~ cC12(U_242) )
| ~ cC52(U_242) ) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
fof(f_63_3,plain,
( ! [U_244] :
( cC52(U_244)
| cC50(U_244)
| cC12(U_244) )
& ! [U_243] :
( ( ~ cC50(U_243)
& ~ cC12(U_243) )
| ~ cC52(U_243) ) ),
inference(miniscope,[status(thm)],[f_63_2]) ).
cnf(f_63_4,plain,
( ~ cC12(U_243)
| ~ cC52(U_243) ),
inference(clausify,[status(thm)],[f_63_3]) ).
cnf(f_63_5,plain,
( ~ cC50(U_243)
| ~ cC52(U_243) ),
inference(clausify,[status(thm)],[f_63_3]) ).
cnf(f_63_6,plain,
( cC52(U_244)
| cC50(U_244)
| cC12(U_244) ),
inference(clausify,[status(thm)],[f_63_3]) ).
fof(f_64_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_63]) ).
fof(f_64_2,plain,
! [U_247] :
( ( cC54(U_247)
| ! [U_246] :
( ~ cC52(U_246)
| ~ rR1(U_247,U_246) ) )
& ( ? [U_245] :
( cC52(U_245)
& rR1(U_247,U_245) )
| ~ cC54(U_247) ) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
fof(f_64_3,plain,
( ! [U_249] :
( cC54(U_249)
| ! [U_246] :
( ~ cC52(U_246)
| ~ rR1(U_249,U_246) ) )
& ! [U_248] :
( ? [U_245] :
( cC52(U_245)
& rR1(U_248,U_245) )
| ~ cC54(U_248) ) ),
inference(miniscope,[status(thm)],[f_64_2]) ).
fof(f_64_4,plain,
( ! [U_249] :
( cC54(U_249)
| ! [U_246] :
( ~ cC52(U_246)
| ~ rR1(U_249,U_246) ) )
& ! [U_248] :
( ( cC52(sK29(U_248))
& rR1(U_248,sK29(U_248)) )
| ~ cC54(U_248) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_245,sK29(U_248))],[f_64_3]) ).
cnf(f_64_5,plain,
( rR1(U_248,sK29(U_248))
| ~ cC54(U_248) ),
inference(clausify,[status(thm)],[f_64_4]) ).
cnf(f_64_6,plain,
( cC52(sK29(U_248))
| ~ cC54(U_248) ),
inference(clausify,[status(thm)],[f_64_4]) ).
cnf(f_64_7,plain,
( cC54(U_249)
| ~ cC52(U_246)
| ~ rR1(U_249,U_246) ),
inference(clausify,[status(thm)],[f_64_4]) ).
fof(f_65_1,plain,
! [X] :
( ( cC56(X)
| cC54(X)
| cC48(X) )
& ( ( ~ cC54(X)
& ~ cC48(X) )
| ~ cC56(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
! [U_250] :
( ( cC56(U_250)
| cC54(U_250)
| cC48(U_250) )
& ( ( ~ cC54(U_250)
& ~ cC48(U_250) )
| ~ cC56(U_250) ) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
( ! [U_252] :
( cC56(U_252)
| cC54(U_252)
| cC48(U_252) )
& ! [U_251] :
( ( ~ cC54(U_251)
& ~ cC48(U_251) )
| ~ cC56(U_251) ) ),
inference(miniscope,[status(thm)],[f_65_2]) ).
cnf(f_65_4,plain,
( ~ cC48(U_251)
| ~ cC56(U_251) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_5,plain,
( ~ cC54(U_251)
| ~ cC56(U_251) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_6,plain,
( cC56(U_252)
| cC54(U_252)
| cC48(U_252) ),
inference(clausify,[status(thm)],[f_65_3]) ).
fof(f_66_1,plain,
! [X] :
( ( cC58(X)
| ~ cTOP(X)
| ~ cC56(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_253] :
( ( cC58(U_253)
| ~ cTOP(U_253)
| ~ cC56(U_253) )
& ( ( cTOP(U_253)
& cC56(U_253) )
| ~ cC58(U_253) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_255] :
( cC58(U_255)
| ~ cTOP(U_255)
| ~ cC56(U_255) )
& ! [U_254] :
( ( cTOP(U_254)
& cC56(U_254) )
| ~ cC58(U_254) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( cC56(U_254)
| ~ cC58(U_254) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( cTOP(U_254)
| ~ cC58(U_254) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_6,plain,
( cC58(U_255)
| ~ cTOP(U_255)
| ~ cC56(U_255) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_1,plain,
! [X] :
( ( cC60(X)
| ~ cC42(X)
| ~ cC58(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_66]) ).
fof(f_67_2,plain,
! [U_256] :
( ( cC60(U_256)
| ~ cC42(U_256)
| ~ cC58(U_256) )
& ( ( cC42(U_256)
& cC58(U_256) )
| ~ cC60(U_256) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_258] :
( cC60(U_258)
| ~ cC42(U_258)
| ~ cC58(U_258) )
& ! [U_257] :
( ( cC42(U_257)
& cC58(U_257) )
| ~ cC60(U_257) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
cnf(f_67_4,plain,
( cC58(U_257)
| ~ cC60(U_257) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_5,plain,
( cC42(U_257)
| ~ cC60(U_257) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_6,plain,
( cC60(U_258)
| ~ cC42(U_258)
| ~ cC58(U_258) ),
inference(clausify,[status(thm)],[f_67_3]) ).
fof(f_68_1,plain,
! [X] :
( ( cC62(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_67]) ).
fof(f_68_2,plain,
! [U_259] :
( ( cC62(U_259)
| ~ cTOP(U_259) )
& ( cTOP(U_259)
| ~ cC62(U_259) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_261] :
( cC62(U_261)
| ~ cTOP(U_261) )
& ! [U_260] :
( cTOP(U_260)
| ~ cC62(U_260) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( cTOP(U_260)
| ~ cC62(U_260) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( cC62(U_261)
| ~ cTOP(U_261) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
! [X] :
( ( cC64(X)
| ~ cC60(X)
| ~ cC62(X) )
& ( ( cC60(X)
& cC62(X) )
| ~ cC64(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_68]) ).
fof(f_69_2,plain,
! [U_262] :
( ( cC64(U_262)
| ~ cC60(U_262)
| ~ cC62(U_262) )
& ( ( cC60(U_262)
& cC62(U_262) )
| ~ cC64(U_262) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_264] :
( cC64(U_264)
| ~ cC60(U_264)
| ~ cC62(U_264) )
& ! [U_263] :
( ( cC60(U_263)
& cC62(U_263) )
| ~ cC64(U_263) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
cnf(f_69_4,plain,
( cC62(U_263)
| ~ cC64(U_263) ),
inference(clausify,[status(thm)],[f_69_3]) ).
cnf(f_69_5,plain,
( cC60(U_263)
| ~ cC64(U_263) ),
inference(clausify,[status(thm)],[f_69_3]) ).
cnf(f_69_6,plain,
( cC64(U_264)
| ~ cC60(U_264)
| ~ cC62(U_264) ),
inference(clausify,[status(thm)],[f_69_3]) ).
fof(f_70_1,plain,
! [X] :
( ( cC66(X)
| ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC66(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_69]) ).
fof(f_70_2,plain,
! [U_267] :
( ( cC66(U_267)
| ! [U_266] :
( cC2(U_266)
| ~ rR1(U_267,U_266) ) )
& ( ? [U_265] :
( ~ cC2(U_265)
& rR1(U_267,U_265) )
| ~ cC66(U_267) ) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
fof(f_70_3,plain,
( ! [U_269] :
( cC66(U_269)
| ! [U_266] :
( cC2(U_266)
| ~ rR1(U_269,U_266) ) )
& ! [U_268] :
( ? [U_265] :
( ~ cC2(U_265)
& rR1(U_268,U_265) )
| ~ cC66(U_268) ) ),
inference(miniscope,[status(thm)],[f_70_2]) ).
fof(f_70_4,plain,
( ! [U_269] :
( cC66(U_269)
| ! [U_266] :
( cC2(U_266)
| ~ rR1(U_269,U_266) ) )
& ! [U_268] :
( ( ~ cC2(sK30(U_268))
& rR1(U_268,sK30(U_268)) )
| ~ cC66(U_268) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_265,sK30(U_268))],[f_70_3]) ).
cnf(f_70_5,plain,
( rR1(U_268,sK30(U_268))
| ~ cC66(U_268) ),
inference(clausify,[status(thm)],[f_70_4]) ).
cnf(f_70_6,plain,
( ~ cC2(sK30(U_268))
| ~ cC66(U_268) ),
inference(clausify,[status(thm)],[f_70_4]) ).
cnf(f_70_7,plain,
( cC66(U_269)
| cC2(U_266)
| ~ rR1(U_269,U_266) ),
inference(clausify,[status(thm)],[f_70_4]) ).
fof(f_71_1,plain,
! [X] :
( ( cC68(X)
| cC18(X)
| cC66(X) )
& ( ( ~ cC18(X)
& ~ cC66(X) )
| ~ cC68(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_70]) ).
fof(f_71_2,plain,
! [U_270] :
( ( cC68(U_270)
| cC18(U_270)
| cC66(U_270) )
& ( ( ~ cC18(U_270)
& ~ cC66(U_270) )
| ~ cC68(U_270) ) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
( ! [U_272] :
( cC68(U_272)
| cC18(U_272)
| cC66(U_272) )
& ! [U_271] :
( ( ~ cC18(U_271)
& ~ cC66(U_271) )
| ~ cC68(U_271) ) ),
inference(miniscope,[status(thm)],[f_71_2]) ).
cnf(f_71_4,plain,
( ~ cC66(U_271)
| ~ cC68(U_271) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_5,plain,
( ~ cC18(U_271)
| ~ cC68(U_271) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_6,plain,
( cC68(U_272)
| cC18(U_272)
| cC66(U_272) ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_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_71]) ).
fof(f_72_2,plain,
! [U_275] :
( ( cC70(U_275)
| ! [U_274] :
( ~ cC68(U_274)
| ~ rR1(U_275,U_274) ) )
& ( ? [U_273] :
( cC68(U_273)
& rR1(U_275,U_273) )
| ~ cC70(U_275) ) ),
inference(variable_rename,[status(thm)],[f_72_1]) ).
fof(f_72_3,plain,
( ! [U_277] :
( cC70(U_277)
| ! [U_274] :
( ~ cC68(U_274)
| ~ rR1(U_277,U_274) ) )
& ! [U_276] :
( ? [U_273] :
( cC68(U_273)
& rR1(U_276,U_273) )
| ~ cC70(U_276) ) ),
inference(miniscope,[status(thm)],[f_72_2]) ).
fof(f_72_4,plain,
( ! [U_277] :
( cC70(U_277)
| ! [U_274] :
( ~ cC68(U_274)
| ~ rR1(U_277,U_274) ) )
& ! [U_276] :
( ( cC68(sK31(U_276))
& rR1(U_276,sK31(U_276)) )
| ~ cC70(U_276) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_273,sK31(U_276))],[f_72_3]) ).
cnf(f_72_5,plain,
( rR1(U_276,sK31(U_276))
| ~ cC70(U_276) ),
inference(clausify,[status(thm)],[f_72_4]) ).
cnf(f_72_6,plain,
( cC68(sK31(U_276))
| ~ cC70(U_276) ),
inference(clausify,[status(thm)],[f_72_4]) ).
cnf(f_72_7,plain,
( cC70(U_277)
| ~ cC68(U_274)
| ~ rR1(U_277,U_274) ),
inference(clausify,[status(thm)],[f_72_4]) ).
fof(f_73_1,plain,
! [X] :
( ( cC72(X)
| ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC72(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_72]) ).
fof(f_73_2,plain,
! [U_280] :
( ( cC72(U_280)
| ! [U_279] :
( cC12(U_279)
| ~ rR1(U_280,U_279) ) )
& ( ? [U_278] :
( ~ cC12(U_278)
& rR1(U_280,U_278) )
| ~ cC72(U_280) ) ),
inference(variable_rename,[status(thm)],[f_73_1]) ).
fof(f_73_3,plain,
( ! [U_282] :
( cC72(U_282)
| ! [U_279] :
( cC12(U_279)
| ~ rR1(U_282,U_279) ) )
& ! [U_281] :
( ? [U_278] :
( ~ cC12(U_278)
& rR1(U_281,U_278) )
| ~ cC72(U_281) ) ),
inference(miniscope,[status(thm)],[f_73_2]) ).
fof(f_73_4,plain,
( ! [U_282] :
( cC72(U_282)
| ! [U_279] :
( cC12(U_279)
| ~ rR1(U_282,U_279) ) )
& ! [U_281] :
( ( ~ cC12(sK32(U_281))
& rR1(U_281,sK32(U_281)) )
| ~ cC72(U_281) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_278,sK32(U_281))],[f_73_3]) ).
cnf(f_73_5,plain,
( rR1(U_281,sK32(U_281))
| ~ cC72(U_281) ),
inference(clausify,[status(thm)],[f_73_4]) ).
cnf(f_73_6,plain,
( ~ cC12(sK32(U_281))
| ~ cC72(U_281) ),
inference(clausify,[status(thm)],[f_73_4]) ).
cnf(f_73_7,plain,
( cC72(U_282)
| cC12(U_279)
| ~ rR1(U_282,U_279) ),
inference(clausify,[status(thm)],[f_73_4]) ).
fof(f_74_1,plain,
! [X] :
( ( cC74(X)
| cC72(X)
| cC18(X) )
& ( ( ~ cC72(X)
& ~ cC18(X) )
| ~ cC74(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_73]) ).
fof(f_74_2,plain,
! [U_283] :
( ( cC74(U_283)
| cC72(U_283)
| cC18(U_283) )
& ( ( ~ cC72(U_283)
& ~ cC18(U_283) )
| ~ cC74(U_283) ) ),
inference(variable_rename,[status(thm)],[f_74_1]) ).
fof(f_74_3,plain,
( ! [U_285] :
( cC74(U_285)
| cC72(U_285)
| cC18(U_285) )
& ! [U_284] :
( ( ~ cC72(U_284)
& ~ cC18(U_284) )
| ~ cC74(U_284) ) ),
inference(miniscope,[status(thm)],[f_74_2]) ).
cnf(f_74_4,plain,
( ~ cC18(U_284)
| ~ cC74(U_284) ),
inference(clausify,[status(thm)],[f_74_3]) ).
cnf(f_74_5,plain,
( ~ cC72(U_284)
| ~ cC74(U_284) ),
inference(clausify,[status(thm)],[f_74_3]) ).
cnf(f_74_6,plain,
( cC74(U_285)
| cC72(U_285)
| cC18(U_285) ),
inference(clausify,[status(thm)],[f_74_3]) ).
fof(f_75_1,plain,
! [X] :
( ( cC76(X)
| ! [Y] :
( ~ cC74(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC74(Y)
& rR1(X,Y) )
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_74]) ).
fof(f_75_2,plain,
! [U_288] :
( ( cC76(U_288)
| ! [U_287] :
( ~ cC74(U_287)
| ~ rR1(U_288,U_287) ) )
& ( ? [U_286] :
( cC74(U_286)
& rR1(U_288,U_286) )
| ~ cC76(U_288) ) ),
inference(variable_rename,[status(thm)],[f_75_1]) ).
fof(f_75_3,plain,
( ! [U_290] :
( cC76(U_290)
| ! [U_287] :
( ~ cC74(U_287)
| ~ rR1(U_290,U_287) ) )
& ! [U_289] :
( ? [U_286] :
( cC74(U_286)
& rR1(U_289,U_286) )
| ~ cC76(U_289) ) ),
inference(miniscope,[status(thm)],[f_75_2]) ).
fof(f_75_4,plain,
( ! [U_290] :
( cC76(U_290)
| ! [U_287] :
( ~ cC74(U_287)
| ~ rR1(U_290,U_287) ) )
& ! [U_289] :
( ( cC74(sK33(U_289))
& rR1(U_289,sK33(U_289)) )
| ~ cC76(U_289) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_286,sK33(U_289))],[f_75_3]) ).
cnf(f_75_5,plain,
( rR1(U_289,sK33(U_289))
| ~ cC76(U_289) ),
inference(clausify,[status(thm)],[f_75_4]) ).
cnf(f_75_6,plain,
( cC74(sK33(U_289))
| ~ cC76(U_289) ),
inference(clausify,[status(thm)],[f_75_4]) ).
cnf(f_75_7,plain,
( cC76(U_290)
| ~ cC74(U_287)
| ~ rR1(U_290,U_287) ),
inference(clausify,[status(thm)],[f_75_4]) ).
fof(f_76_1,plain,
! [X] :
( ( cC78(X)
| cC76(X)
| cC70(X) )
& ( ( ~ cC76(X)
& ~ cC70(X) )
| ~ cC78(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_75]) ).
fof(f_76_2,plain,
! [U_291] :
( ( cC78(U_291)
| cC76(U_291)
| cC70(U_291) )
& ( ( ~ cC76(U_291)
& ~ cC70(U_291) )
| ~ cC78(U_291) ) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
fof(f_76_3,plain,
( ! [U_293] :
( cC78(U_293)
| cC76(U_293)
| cC70(U_293) )
& ! [U_292] :
( ( ~ cC76(U_292)
& ~ cC70(U_292) )
| ~ cC78(U_292) ) ),
inference(miniscope,[status(thm)],[f_76_2]) ).
cnf(f_76_4,plain,
( ~ cC70(U_292)
| ~ cC78(U_292) ),
inference(clausify,[status(thm)],[f_76_3]) ).
cnf(f_76_5,plain,
( ~ cC76(U_292)
| ~ cC78(U_292) ),
inference(clausify,[status(thm)],[f_76_3]) ).
cnf(f_76_6,plain,
( cC78(U_293)
| cC76(U_293)
| cC70(U_293) ),
inference(clausify,[status(thm)],[f_76_3]) ).
fof(f_77_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_76]) ).
fof(f_77_2,plain,
! [U_296] :
( ( cC8(U_296)
| ! [U_295] :
( cC6(U_295)
| ~ rR1(U_296,U_295) ) )
& ( ? [U_294] :
( ~ cC6(U_294)
& rR1(U_296,U_294) )
| ~ cC8(U_296) ) ),
inference(variable_rename,[status(thm)],[f_77_1]) ).
fof(f_77_3,plain,
( ! [U_298] :
( cC8(U_298)
| ! [U_295] :
( cC6(U_295)
| ~ rR1(U_298,U_295) ) )
& ! [U_297] :
( ? [U_294] :
( ~ cC6(U_294)
& rR1(U_297,U_294) )
| ~ cC8(U_297) ) ),
inference(miniscope,[status(thm)],[f_77_2]) ).
fof(f_77_4,plain,
( ! [U_298] :
( cC8(U_298)
| ! [U_295] :
( cC6(U_295)
| ~ rR1(U_298,U_295) ) )
& ! [U_297] :
( ( ~ cC6(sK34(U_297))
& rR1(U_297,sK34(U_297)) )
| ~ cC8(U_297) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_294,sK34(U_297))],[f_77_3]) ).
cnf(f_77_5,plain,
( rR1(U_297,sK34(U_297))
| ~ cC8(U_297) ),
inference(clausify,[status(thm)],[f_77_4]) ).
cnf(f_77_6,plain,
( ~ cC6(sK34(U_297))
| ~ cC8(U_297) ),
inference(clausify,[status(thm)],[f_77_4]) ).
cnf(f_77_7,plain,
( cC8(U_298)
| cC6(U_295)
| ~ rR1(U_298,U_295) ),
inference(clausify,[status(thm)],[f_77_4]) ).
fof(f_78_1,plain,
! [X] :
( ( cC80(X)
| ~ cC78(X)
| ~ cTOP(X) )
& ( ( cC78(X)
& cTOP(X) )
| ~ cC80(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_77]) ).
fof(f_78_2,plain,
! [U_299] :
( ( cC80(U_299)
| ~ cC78(U_299)
| ~ cTOP(U_299) )
& ( ( cC78(U_299)
& cTOP(U_299) )
| ~ cC80(U_299) ) ),
inference(variable_rename,[status(thm)],[f_78_1]) ).
fof(f_78_3,plain,
( ! [U_301] :
( cC80(U_301)
| ~ cC78(U_301)
| ~ cTOP(U_301) )
& ! [U_300] :
( ( cC78(U_300)
& cTOP(U_300) )
| ~ cC80(U_300) ) ),
inference(miniscope,[status(thm)],[f_78_2]) ).
cnf(f_78_4,plain,
( cTOP(U_300)
| ~ cC80(U_300) ),
inference(clausify,[status(thm)],[f_78_3]) ).
cnf(f_78_5,plain,
( cC78(U_300)
| ~ cC80(U_300) ),
inference(clausify,[status(thm)],[f_78_3]) ).
cnf(f_78_6,plain,
( cC80(U_301)
| ~ cC78(U_301)
| ~ cTOP(U_301) ),
inference(clausify,[status(thm)],[f_78_3]) ).
fof(f_79_1,plain,
! [X] :
( ( cC82(X)
| ~ cC64(X)
| ~ cC80(X) )
& ( ( cC64(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_78]) ).
fof(f_79_2,plain,
! [U_302] :
( ( cC82(U_302)
| ~ cC64(U_302)
| ~ cC80(U_302) )
& ( ( cC64(U_302)
& cC80(U_302) )
| ~ cC82(U_302) ) ),
inference(variable_rename,[status(thm)],[f_79_1]) ).
fof(f_79_3,plain,
( ! [U_304] :
( cC82(U_304)
| ~ cC64(U_304)
| ~ cC80(U_304) )
& ! [U_303] :
( ( cC64(U_303)
& cC80(U_303) )
| ~ cC82(U_303) ) ),
inference(miniscope,[status(thm)],[f_79_2]) ).
cnf(f_79_4,plain,
( cC80(U_303)
| ~ cC82(U_303) ),
inference(clausify,[status(thm)],[f_79_3]) ).
cnf(f_79_5,plain,
( cC64(U_303)
| ~ cC82(U_303) ),
inference(clausify,[status(thm)],[f_79_3]) ).
cnf(f_79_6,plain,
( cC82(U_304)
| ~ cC64(U_304)
| ~ cC80(U_304) ),
inference(clausify,[status(thm)],[f_79_3]) ).
fof(f_80_1,plain,
! [X] :
( ( cC84(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_79]) ).
fof(f_80_2,plain,
! [U_305] :
( ( cC84(U_305)
| ~ cTOP(U_305) )
& ( cTOP(U_305)
| ~ cC84(U_305) ) ),
inference(variable_rename,[status(thm)],[f_80_1]) ).
fof(f_80_3,plain,
( ! [U_307] :
( cC84(U_307)
| ~ cTOP(U_307) )
& ! [U_306] :
( cTOP(U_306)
| ~ cC84(U_306) ) ),
inference(miniscope,[status(thm)],[f_80_2]) ).
cnf(f_80_4,plain,
( cTOP(U_306)
| ~ cC84(U_306) ),
inference(clausify,[status(thm)],[f_80_3]) ).
cnf(f_80_5,plain,
( cC84(U_307)
| ~ cTOP(U_307) ),
inference(clausify,[status(thm)],[f_80_3]) ).
fof(f_81_1,plain,
! [X] :
( ( cC86(X)
| ~ cC84(X)
| ~ cC82(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_80]) ).
fof(f_81_2,plain,
! [U_308] :
( ( cC86(U_308)
| ~ cC84(U_308)
| ~ cC82(U_308) )
& ( ( cC84(U_308)
& cC82(U_308) )
| ~ cC86(U_308) ) ),
inference(variable_rename,[status(thm)],[f_81_1]) ).
fof(f_81_3,plain,
( ! [U_310] :
( cC86(U_310)
| ~ cC84(U_310)
| ~ cC82(U_310) )
& ! [U_309] :
( ( cC84(U_309)
& cC82(U_309) )
| ~ cC86(U_309) ) ),
inference(miniscope,[status(thm)],[f_81_2]) ).
cnf(f_81_4,plain,
( cC82(U_309)
| ~ cC86(U_309) ),
inference(clausify,[status(thm)],[f_81_3]) ).
cnf(f_81_5,plain,
( cC84(U_309)
| ~ cC86(U_309) ),
inference(clausify,[status(thm)],[f_81_3]) ).
cnf(f_81_6,plain,
( cC86(U_310)
| ~ cC84(U_310)
| ~ cC82(U_310) ),
inference(clausify,[status(thm)],[f_81_3]) ).
fof(f_82_1,plain,
! [X] :
( ( cC88(X)
| ~ cTOP(X) )
& ( cTOP(X)
| ~ cC88(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_81]) ).
fof(f_82_2,plain,
! [U_311] :
( ( cC88(U_311)
| ~ cTOP(U_311) )
& ( cTOP(U_311)
| ~ cC88(U_311) ) ),
inference(variable_rename,[status(thm)],[f_82_1]) ).
fof(f_82_3,plain,
( ! [U_313] :
( cC88(U_313)
| ~ cTOP(U_313) )
& ! [U_312] :
( cTOP(U_312)
| ~ cC88(U_312) ) ),
inference(miniscope,[status(thm)],[f_82_2]) ).
cnf(f_82_4,plain,
( cTOP(U_312)
| ~ cC88(U_312) ),
inference(clausify,[status(thm)],[f_82_3]) ).
cnf(f_82_5,plain,
( cC88(U_313)
| ~ cTOP(U_313) ),
inference(clausify,[status(thm)],[f_82_3]) ).
fof(f_83_1,plain,
! [X] :
( ( cC90(X)
| ~ cC86(X)
| ~ cC88(X) )
& ( ( cC86(X)
& cC88(X) )
| ~ cC90(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_82]) ).
fof(f_83_2,plain,
! [U_314] :
( ( cC90(U_314)
| ~ cC86(U_314)
| ~ cC88(U_314) )
& ( ( cC86(U_314)
& cC88(U_314) )
| ~ cC90(U_314) ) ),
inference(variable_rename,[status(thm)],[f_83_1]) ).
fof(f_83_3,plain,
( ! [U_316] :
( cC90(U_316)
| ~ cC86(U_316)
| ~ cC88(U_316) )
& ! [U_315] :
( ( cC86(U_315)
& cC88(U_315) )
| ~ cC90(U_315) ) ),
inference(miniscope,[status(thm)],[f_83_2]) ).
cnf(f_83_4,plain,
( cC88(U_315)
| ~ cC90(U_315) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_5,plain,
( cC86(U_315)
| ~ cC90(U_315) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_6,plain,
( cC90(U_316)
| ~ cC86(U_316)
| ~ cC88(U_316) ),
inference(clausify,[status(thm)],[f_83_3]) ).
fof(f_84_1,plain,
! [X] :
( ( cC94(X)
| ! [Y] :
( cC6(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) )
| ~ cC94(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_83]) ).
fof(f_84_2,plain,
! [U_319] :
( ( cC94(U_319)
| ! [U_318] :
( cC6(U_318)
| ~ rR1(U_319,U_318) ) )
& ( ? [U_317] :
( ~ cC6(U_317)
& rR1(U_319,U_317) )
| ~ cC94(U_319) ) ),
inference(variable_rename,[status(thm)],[f_84_1]) ).
fof(f_84_3,plain,
( ! [U_321] :
( cC94(U_321)
| ! [U_318] :
( cC6(U_318)
| ~ rR1(U_321,U_318) ) )
& ! [U_320] :
( ? [U_317] :
( ~ cC6(U_317)
& rR1(U_320,U_317) )
| ~ cC94(U_320) ) ),
inference(miniscope,[status(thm)],[f_84_2]) ).
fof(f_84_4,plain,
( ! [U_321] :
( cC94(U_321)
| ! [U_318] :
( cC6(U_318)
| ~ rR1(U_321,U_318) ) )
& ! [U_320] :
( ( ~ cC6(sK35(U_320))
& rR1(U_320,sK35(U_320)) )
| ~ cC94(U_320) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(U_317,sK35(U_320))],[f_84_3]) ).
cnf(f_84_5,plain,
( rR1(U_320,sK35(U_320))
| ~ cC94(U_320) ),
inference(clausify,[status(thm)],[f_84_4]) ).
cnf(f_84_6,plain,
( ~ cC6(sK35(U_320))
| ~ cC94(U_320) ),
inference(clausify,[status(thm)],[f_84_4]) ).
cnf(f_84_7,plain,
( cC94(U_321)
| cC6(U_318)
| ~ rR1(U_321,U_318) ),
inference(clausify,[status(thm)],[f_84_4]) ).
fof(f_85_1,plain,
! [X] :
( ( cC96(X)
| cC94(X)
| cC92(X) )
& ( ( ~ cC94(X)
& ~ cC92(X) )
| ~ cC96(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_84]) ).
fof(f_85_2,plain,
! [U_322] :
( ( cC96(U_322)
| cC94(U_322)
| cC92(U_322) )
& ( ( ~ cC94(U_322)
& ~ cC92(U_322) )
| ~ cC96(U_322) ) ),
inference(variable_rename,[status(thm)],[f_85_1]) ).
fof(f_85_3,plain,
( ! [U_324] :
( cC96(U_324)
| cC94(U_324)
| cC92(U_324) )
& ! [U_323] :
( ( ~ cC94(U_323)
& ~ cC92(U_323) )
| ~ cC96(U_323) ) ),
inference(miniscope,[status(thm)],[f_85_2]) ).
cnf(f_85_4,plain,
( ~ cC92(U_323)
| ~ cC96(U_323) ),
inference(clausify,[status(thm)],[f_85_3]) ).
cnf(f_85_5,plain,
( ~ cC94(U_323)
| ~ cC96(U_323) ),
inference(clausify,[status(thm)],[f_85_3]) ).
cnf(f_85_6,plain,
( cC96(U_324)
| cC94(U_324)
| cC92(U_324) ),
inference(clausify,[status(thm)],[f_85_3]) ).
fof(f_86_1,plain,
! [X] :
( ( cC98(X)
| ! [Y] :
( ~ cC96(Y)
| ~ rR1(X,Y) ) )
& ( ? [Y] :
( cC96(Y)
& rR1(X,Y) )
| ~ cC98(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_85]) ).
fof(f_86_2,plain,
! [U_327] :
( ( cC98(U_327)
| ! [U_326] :
( ~ cC96(U_326)
| ~ rR1(U_327,U_326) ) )
& ( ? [U_325] :
( cC96(U_325)
& rR1(U_327,U_325) )
| ~ cC98(U_327) ) ),
inference(variable_rename,[status(thm)],[f_86_1]) ).
fof(f_86_3,plain,
( ! [U_329] :
( cC98(U_329)
| ! [U_326] :
( ~ cC96(U_326)
| ~ rR1(U_329,U_326) ) )
& ! [U_328] :
( ? [U_325] :
( cC96(U_325)
& rR1(U_328,U_325) )
| ~ cC98(U_328) ) ),
inference(miniscope,[status(thm)],[f_86_2]) ).
fof(f_86_4,plain,
( ! [U_329] :
( cC98(U_329)
| ! [U_326] :
( ~ cC96(U_326)
| ~ rR1(U_329,U_326) ) )
& ! [U_328] :
( ( cC96(sK36(U_328))
& rR1(U_328,sK36(U_328)) )
| ~ cC98(U_328) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(U_325,sK36(U_328))],[f_86_3]) ).
cnf(f_86_5,plain,
( rR1(U_328,sK36(U_328))
| ~ cC98(U_328) ),
inference(clausify,[status(thm)],[f_86_4]) ).
cnf(f_86_6,plain,
( cC96(sK36(U_328))
| ~ cC98(U_328) ),
inference(clausify,[status(thm)],[f_86_4]) ).
cnf(f_86_7,plain,
( cC98(U_329)
| ~ cC96(U_326)
| ~ rR1(U_329,U_326) ),
inference(clausify,[status(thm)],[f_86_4]) ).
fof(f_87_1,plain,
! [X] :
( ( cTEST(X)
| ~ cC180(X)
| ~ cC158(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_86]) ).
fof(f_87_2,plain,
! [U_330] :
( ( cTEST(U_330)
| ~ cC180(U_330)
| ~ cC158(U_330) )
& ( ( cC180(U_330)
& cC158(U_330) )
| ~ cTEST(U_330) ) ),
inference(variable_rename,[status(thm)],[f_87_1]) ).
fof(f_87_3,plain,
( ! [U_332] :
( cTEST(U_332)
| ~ cC180(U_332)
| ~ cC158(U_332) )
& ! [U_331] :
( ( cC180(U_331)
& cC158(U_331) )
| ~ cTEST(U_331) ) ),
inference(miniscope,[status(thm)],[f_87_2]) ).
cnf(f_87_4,plain,
( cC158(U_331)
| ~ cTEST(U_331) ),
inference(clausify,[status(thm)],[f_87_3]) ).
cnf(f_87_5,plain,
( cC180(U_331)
| ~ cTEST(U_331) ),
inference(clausify,[status(thm)],[f_87_3]) ).
cnf(f_87_6,plain,
( cTEST(U_332)
| ~ cC180(U_332)
| ~ cC158(U_332) ),
inference(clausify,[status(thm)],[f_87_3]) ).
fof(f_88_1,plain,
! [X] :
( ~ cC26(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_87]) ).
fof(f_88_2,plain,
! [U_333] :
( ~ cC26(U_333)
| ~ rR1(iV21026,U_333) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
cnf(f_88_3,plain,
( ~ cC26(U_333)
| ~ rR1(iV21026,U_333) ),
inference(clausify,[status(thm)],[f_88_2]) ).
fof(f_89_1,plain,
cTOP(iV21026),
inference(fof_nnf,[status(thm)],[axiom_88]) ).
cnf(f_89_2,plain,
cTOP(iV21026),
inference(clausify,[status(thm)],[f_89_1]) ).
fof(f_90_1,plain,
cTEST(iV21026),
inference(fof_nnf,[status(thm)],[axiom_89]) ).
cnf(f_90_2,plain,
cTEST(iV21026),
inference(clausify,[status(thm)],[f_90_1]) ).
fof(f_91_1,plain,
! [X] :
( ~ cC104(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_90]) ).
fof(f_91_2,plain,
! [U_334] :
( ~ cC104(U_334)
| ~ rR1(iV21026,U_334) ),
inference(variable_rename,[status(thm)],[f_91_1]) ).
cnf(f_91_3,plain,
( ~ cC104(U_334)
| ~ rR1(iV21026,U_334) ),
inference(clausify,[status(thm)],[f_91_2]) ).
fof(f_92_1,plain,
~ cC98(iV21026),
inference(fof_nnf,[status(thm)],[axiom_91]) ).
cnf(f_92_2,plain,
~ cC98(iV21026),
inference(clausify,[status(thm)],[f_92_1]) ).
fof(f_93_1,plain,
~ cC122(iV21026),
inference(fof_nnf,[status(thm)],[axiom_92]) ).
cnf(f_93_2,plain,
~ cC122(iV21026),
inference(clausify,[status(thm)],[f_93_1]) ).
fof(f_94_1,plain,
! [X] :
( ~ cC148(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_93]) ).
fof(f_94_2,plain,
! [U_335] :
( ~ cC148(U_335)
| ~ rR1(iV21026,U_335) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
cnf(f_94_3,plain,
( ~ cC148(U_335)
| ~ rR1(iV21026,U_335) ),
inference(clausify,[status(thm)],[f_94_2]) ).
fof(f_95_1,plain,
! [X] :
( ~ cC160(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_94]) ).
fof(f_95_2,plain,
! [U_336] :
( ~ cC160(U_336)
| ~ rR1(iV21026,U_336) ),
inference(variable_rename,[status(thm)],[f_95_1]) ).
cnf(f_95_3,plain,
( ~ cC160(U_336)
| ~ rR1(iV21026,U_336) ),
inference(clausify,[status(thm)],[f_95_2]) ).
fof(f_96_1,plain,
~ cC34(iV21026),
inference(fof_nnf,[status(thm)],[axiom_95]) ).
cnf(f_96_2,plain,
~ cC34(iV21026),
inference(clausify,[status(thm)],[f_96_1]) ).
fof(f_97_1,plain,
~ cC28(iV21026),
inference(fof_nnf,[status(thm)],[axiom_96]) ).
cnf(f_97_2,plain,
~ cC28(iV21026),
inference(clausify,[status(thm)],[f_97_1]) ).
fof(f_98_1,plain,
! [X] :
( ~ cC126(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_97]) ).
fof(f_98_2,plain,
! [U_337] :
( ~ cC126(U_337)
| ~ rR1(iV21026,U_337) ),
inference(variable_rename,[status(thm)],[f_98_1]) ).
cnf(f_98_3,plain,
( ~ cC126(U_337)
| ~ rR1(iV21026,U_337) ),
inference(clausify,[status(thm)],[f_98_2]) ).
fof(f_99_1,plain,
~ cC70(iV21026),
inference(fof_nnf,[status(thm)],[axiom_98]) ).
cnf(f_99_2,plain,
~ cC70(iV21026),
inference(clausify,[status(thm)],[f_99_1]) ).
fof(f_100_1,plain,
~ cC178(iV21026),
inference(fof_nnf,[status(thm)],[axiom_99]) ).
cnf(f_100_2,plain,
~ cC178(iV21026),
inference(clausify,[status(thm)],[f_100_1]) ).
fof(f_101_1,plain,
~ cC162(iV21026),
inference(fof_nnf,[status(thm)],[axiom_100]) ).
cnf(f_101_2,plain,
~ cC162(iV21026),
inference(clausify,[status(thm)],[f_101_1]) ).
fof(f_102_1,plain,
~ cC166(iV21026),
inference(fof_nnf,[status(thm)],[axiom_101]) ).
cnf(f_102_2,plain,
~ cC166(iV21026),
inference(clausify,[status(thm)],[f_102_1]) ).
fof(f_103_1,plain,
! [X] :
( ~ cC68(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_102]) ).
fof(f_103_2,plain,
! [U_338] :
( ~ cC68(U_338)
| ~ rR1(iV21026,U_338) ),
inference(variable_rename,[status(thm)],[f_103_1]) ).
cnf(f_103_3,plain,
( ~ cC68(U_338)
| ~ rR1(iV21026,U_338) ),
inference(clausify,[status(thm)],[f_103_2]) ).
fof(f_104_1,plain,
! [X] :
( ~ cC164(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_103]) ).
fof(f_104_2,plain,
! [U_339] :
( ~ cC164(U_339)
| ~ rR1(iV21026,U_339) ),
inference(variable_rename,[status(thm)],[f_104_1]) ).
cnf(f_104_3,plain,
( ~ cC164(U_339)
| ~ rR1(iV21026,U_339) ),
inference(clausify,[status(thm)],[f_104_2]) ).
fof(f_105_1,plain,
! [X] :
( ~ cC46(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_104]) ).
fof(f_105_2,plain,
! [U_340] :
( ~ cC46(U_340)
| ~ rR1(iV21026,U_340) ),
inference(variable_rename,[status(thm)],[f_105_1]) ).
cnf(f_105_3,plain,
( ~ cC46(U_340)
| ~ rR1(iV21026,U_340) ),
inference(clausify,[status(thm)],[f_105_2]) ).
fof(f_106_1,plain,
! [X] :
( ~ cC52(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_105]) ).
fof(f_106_2,plain,
! [U_341] :
( ~ cC52(U_341)
| ~ rR1(iV21026,U_341) ),
inference(variable_rename,[status(thm)],[f_106_1]) ).
cnf(f_106_3,plain,
( ~ cC52(U_341)
| ~ rR1(iV21026,U_341) ),
inference(clausify,[status(thm)],[f_106_2]) ).
fof(f_107_1,plain,
! [X] :
( ~ cC176(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_106]) ).
fof(f_107_2,plain,
! [U_342] :
( ~ cC176(U_342)
| ~ rR1(iV21026,U_342) ),
inference(variable_rename,[status(thm)],[f_107_1]) ).
cnf(f_107_3,plain,
( ~ cC176(U_342)
| ~ rR1(iV21026,U_342) ),
inference(clausify,[status(thm)],[f_107_2]) ).
fof(f_108_1,plain,
! [X] :
( ~ cC142(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_107]) ).
fof(f_108_2,plain,
! [U_343] :
( ~ cC142(U_343)
| ~ rR1(iV21026,U_343) ),
inference(variable_rename,[status(thm)],[f_108_1]) ).
cnf(f_108_3,plain,
( ~ cC142(U_343)
| ~ rR1(iV21026,U_343) ),
inference(clausify,[status(thm)],[f_108_2]) ).
fof(f_109_1,plain,
~ cC150(iV21026),
inference(fof_nnf,[status(thm)],[axiom_108]) ).
cnf(f_109_2,plain,
~ cC150(iV21026),
inference(clausify,[status(thm)],[f_109_1]) ).
fof(f_110_1,plain,
~ cC54(iV21026),
inference(fof_nnf,[status(thm)],[axiom_109]) ).
cnf(f_110_2,plain,
~ cC54(iV21026),
inference(clausify,[status(thm)],[f_110_1]) ).
fof(f_111_1,plain,
~ cC106(iV21026),
inference(fof_nnf,[status(thm)],[axiom_110]) ).
cnf(f_111_2,plain,
~ cC106(iV21026),
inference(clausify,[status(thm)],[f_111_1]) ).
fof(f_112_1,plain,
~ cC144(iV21026),
inference(fof_nnf,[status(thm)],[axiom_111]) ).
cnf(f_112_2,plain,
~ cC144(iV21026),
inference(clausify,[status(thm)],[f_112_1]) ).
fof(f_113_1,plain,
~ cC48(iV21026),
inference(fof_nnf,[status(thm)],[axiom_112]) ).
cnf(f_113_2,plain,
~ cC48(iV21026),
inference(clausify,[status(thm)],[f_113_1]) ).
fof(f_114_1,plain,
~ cC76(iV21026),
inference(fof_nnf,[status(thm)],[axiom_113]) ).
cnf(f_114_2,plain,
~ cC76(iV21026),
inference(clausify,[status(thm)],[f_114_1]) ).
fof(f_115_1,plain,
! [X] :
( ~ cC32(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_114]) ).
fof(f_115_2,plain,
! [U_344] :
( ~ cC32(U_344)
| ~ rR1(iV21026,U_344) ),
inference(variable_rename,[status(thm)],[f_115_1]) ).
cnf(f_115_3,plain,
( ~ cC32(U_344)
| ~ rR1(iV21026,U_344) ),
inference(clausify,[status(thm)],[f_115_2]) ).
fof(f_116_1,plain,
~ cC128(iV21026),
inference(fof_nnf,[status(thm)],[axiom_115]) ).
cnf(f_116_2,plain,
~ cC128(iV21026),
inference(clausify,[status(thm)],[f_116_1]) ).
fof(f_117_1,plain,
~ cC172(iV21026),
inference(fof_nnf,[status(thm)],[axiom_116]) ).
cnf(f_117_2,plain,
~ cC172(iV21026),
inference(clausify,[status(thm)],[f_117_1]) ).
fof(f_118_1,plain,
! [X] :
( ~ cC120(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_117]) ).
fof(f_118_2,plain,
! [U_345] :
( ~ cC120(U_345)
| ~ rR1(iV21026,U_345) ),
inference(variable_rename,[status(thm)],[f_118_1]) ).
cnf(f_118_3,plain,
( ~ cC120(U_345)
| ~ rR1(iV21026,U_345) ),
inference(clausify,[status(thm)],[f_118_2]) ).
fof(f_119_1,plain,
! [X] :
( ~ cC96(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_118]) ).
fof(f_119_2,plain,
! [U_346] :
( ~ cC96(U_346)
| ~ rR1(iV21026,U_346) ),
inference(variable_rename,[status(thm)],[f_119_1]) ).
cnf(f_119_3,plain,
( ~ cC96(U_346)
| ~ rR1(iV21026,U_346) ),
inference(clausify,[status(thm)],[f_119_2]) ).
fof(f_120_1,plain,
! [X] :
( ~ cC170(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_119]) ).
fof(f_120_2,plain,
! [U_347] :
( ~ cC170(U_347)
| ~ rR1(iV21026,U_347) ),
inference(variable_rename,[status(thm)],[f_120_1]) ).
cnf(f_120_3,plain,
( ~ cC170(U_347)
| ~ rR1(iV21026,U_347) ),
inference(clausify,[status(thm)],[f_120_2]) ).
fof(f_121_1,plain,
cowlThing(iV21026),
inference(fof_nnf,[status(thm)],[axiom_120]) ).
cnf(f_121_2,plain,
cowlThing(iV21026),
inference(clausify,[status(thm)],[f_121_1]) ).
fof(f_122_1,plain,
! [X] :
( ~ cC74(X)
| ~ rR1(iV21026,X) ),
inference(fof_nnf,[status(thm)],[axiom_121]) ).
fof(f_122_2,plain,
! [U_348] :
( ~ cC74(U_348)
| ~ rR1(iV21026,U_348) ),
inference(variable_rename,[status(thm)],[f_122_1]) ).
cnf(f_122_3,plain,
( ~ cC74(U_348)
| ~ rR1(iV21026,U_348) ),
inference(clausify,[status(thm)],[f_122_2]) ).
fof(f_123_1,plain,
rR1(iV21026,iV21030),
inference(fof_nnf,[status(thm)],[axiom_122]) ).
cnf(f_123_2,plain,
rR1(iV21026,iV21030),
inference(clausify,[status(thm)],[f_123_1]) ).
fof(f_124_1,plain,
rR1(iV21026,iV21027),
inference(fof_nnf,[status(thm)],[axiom_123]) ).
cnf(f_124_2,plain,
rR1(iV21026,iV21027),
inference(clausify,[status(thm)],[f_124_1]) ).
fof(f_125_1,plain,
rR1(iV21026,iV21028),
inference(fof_nnf,[status(thm)],[axiom_124]) ).
cnf(f_125_2,plain,
rR1(iV21026,iV21028),
inference(clausify,[status(thm)],[f_125_1]) ).
fof(f_126_1,plain,
rR1(iV21026,iV21029),
inference(fof_nnf,[status(thm)],[axiom_125]) ).
cnf(f_126_2,plain,
rR1(iV21026,iV21029),
inference(clausify,[status(thm)],[f_126_1]) ).
fof(f_127_1,plain,
~ cC26(iV21027),
inference(fof_nnf,[status(thm)],[axiom_126]) ).
cnf(f_127_2,plain,
~ cC26(iV21027),
inference(clausify,[status(thm)],[f_127_1]) ).
fof(f_128_1,plain,
~ cC176(iV21027),
inference(fof_nnf,[status(thm)],[axiom_127]) ).
cnf(f_128_2,plain,
~ cC176(iV21027),
inference(clausify,[status(thm)],[f_128_1]) ).
fof(f_129_1,plain,
! [X] :
( cC18(X)
| ~ rR1(iV21027,X) ),
inference(fof_nnf,[status(thm)],[axiom_128]) ).
fof(f_129_2,plain,
! [U_349] :
( cC18(U_349)
| ~ rR1(iV21027,U_349) ),
inference(variable_rename,[status(thm)],[f_129_1]) ).
cnf(f_129_3,plain,
( cC18(U_349)
| ~ rR1(iV21027,U_349) ),
inference(clausify,[status(thm)],[f_129_2]) ).
fof(f_130_1,plain,
~ cC46(iV21027),
inference(fof_nnf,[status(thm)],[axiom_129]) ).
cnf(f_130_2,plain,
~ cC46(iV21027),
inference(clausify,[status(thm)],[f_130_1]) ).
fof(f_131_1,plain,
~ cC170(iV21027),
inference(fof_nnf,[status(thm)],[axiom_130]) ).
cnf(f_131_2,plain,
~ cC170(iV21027),
inference(clausify,[status(thm)],[f_131_1]) ).
fof(f_132_1,plain,
cC12(iV21027),
inference(fof_nnf,[status(thm)],[axiom_131]) ).
cnf(f_132_2,plain,
cC12(iV21027),
inference(clausify,[status(thm)],[f_132_1]) ).
fof(f_133_1,plain,
~ cC120(iV21027),
inference(fof_nnf,[status(thm)],[axiom_132]) ).
cnf(f_133_2,plain,
~ cC120(iV21027),
inference(clausify,[status(thm)],[f_133_1]) ).
fof(f_134_1,plain,
~ cC74(iV21027),
inference(fof_nnf,[status(thm)],[axiom_133]) ).
cnf(f_134_2,plain,
~ cC74(iV21027),
inference(clausify,[status(thm)],[f_134_1]) ).
fof(f_135_1,plain,
! [X] :
( cC6(X)
| ~ rR1(iV21027,X) ),
inference(fof_nnf,[status(thm)],[axiom_134]) ).
fof(f_135_2,plain,
! [U_350] :
( cC6(U_350)
| ~ rR1(iV21027,U_350) ),
inference(variable_rename,[status(thm)],[f_135_1]) ).
cnf(f_135_3,plain,
( cC6(U_350)
| ~ rR1(iV21027,U_350) ),
inference(clausify,[status(thm)],[f_135_2]) ).
fof(f_136_1,plain,
~ cC52(iV21027),
inference(fof_nnf,[status(thm)],[axiom_135]) ).
cnf(f_136_2,plain,
~ cC52(iV21027),
inference(clausify,[status(thm)],[f_136_1]) ).
fof(f_137_1,plain,
~ cC32(iV21027),
inference(fof_nnf,[status(thm)],[axiom_136]) ).
cnf(f_137_2,plain,
~ cC32(iV21027),
inference(clausify,[status(thm)],[f_137_1]) ).
fof(f_138_1,plain,
~ cC96(iV21027),
inference(fof_nnf,[status(thm)],[axiom_137]) ).
cnf(f_138_2,plain,
~ cC96(iV21027),
inference(clausify,[status(thm)],[f_138_1]) ).
fof(f_139_1,plain,
~ cC68(iV21027),
inference(fof_nnf,[status(thm)],[axiom_138]) ).
cnf(f_139_2,plain,
~ cC68(iV21027),
inference(clausify,[status(thm)],[f_139_1]) ).
fof(f_140_1,plain,
cC92(iV21027),
inference(fof_nnf,[status(thm)],[axiom_139]) ).
cnf(f_140_2,plain,
cC92(iV21027),
inference(clausify,[status(thm)],[f_140_1]) ).
fof(f_141_1,plain,
~ cC126(iV21027),
inference(fof_nnf,[status(thm)],[axiom_140]) ).
cnf(f_141_2,plain,
~ cC126(iV21027),
inference(clausify,[status(thm)],[f_141_1]) ).
fof(f_142_1,plain,
cC100(iV21027),
inference(fof_nnf,[status(thm)],[axiom_141]) ).
cnf(f_142_2,plain,
cC100(iV21027),
inference(clausify,[status(thm)],[f_142_1]) ).
fof(f_143_1,plain,
~ cC160(iV21027),
inference(fof_nnf,[status(thm)],[axiom_142]) ).
cnf(f_143_2,plain,
~ cC160(iV21027),
inference(clausify,[status(thm)],[f_143_1]) ).
fof(f_144_1,plain,
~ cC104(iV21027),
inference(fof_nnf,[status(thm)],[axiom_143]) ).
cnf(f_144_2,plain,
~ cC104(iV21027),
inference(clausify,[status(thm)],[f_144_1]) ).
fof(f_145_1,plain,
~ cC148(iV21027),
inference(fof_nnf,[status(thm)],[axiom_144]) ).
cnf(f_145_2,plain,
~ cC148(iV21027),
inference(clausify,[status(thm)],[f_145_1]) ).
fof(f_146_1,plain,
~ cC142(iV21027),
inference(fof_nnf,[status(thm)],[axiom_145]) ).
cnf(f_146_2,plain,
~ cC142(iV21027),
inference(clausify,[status(thm)],[f_146_1]) ).
fof(f_147_1,plain,
cC18(iV21027),
inference(fof_nnf,[status(thm)],[axiom_146]) ).
cnf(f_147_2,plain,
cC18(iV21027),
inference(clausify,[status(thm)],[f_147_1]) ).
fof(f_148_1,plain,
! [X] :
( cC92(X)
| ~ rR1(iV21027,X) ),
inference(fof_nnf,[status(thm)],[axiom_147]) ).
fof(f_148_2,plain,
! [U_351] :
( cC92(U_351)
| ~ rR1(iV21027,U_351) ),
inference(variable_rename,[status(thm)],[f_148_1]) ).
cnf(f_148_3,plain,
( cC92(U_351)
| ~ rR1(iV21027,U_351) ),
inference(clausify,[status(thm)],[f_148_2]) ).
fof(f_149_1,plain,
! [X] :
( cC100(X)
| ~ rR1(iV21027,X) ),
inference(fof_nnf,[status(thm)],[axiom_148]) ).
fof(f_149_2,plain,
! [U_352] :
( cC100(U_352)
| ~ rR1(iV21027,U_352) ),
inference(variable_rename,[status(thm)],[f_149_1]) ).
cnf(f_149_3,plain,
( cC100(U_352)
| ~ rR1(iV21027,U_352) ),
inference(clausify,[status(thm)],[f_149_2]) ).
fof(f_150_1,plain,
~ cC164(iV21027),
inference(fof_nnf,[status(thm)],[axiom_149]) ).
cnf(f_150_2,plain,
~ cC164(iV21027),
inference(clausify,[status(thm)],[f_150_1]) ).
fof(f_151_1,plain,
~ cC2(iV21027),
inference(fof_nnf,[status(thm)],[axiom_150]) ).
cnf(f_151_2,plain,
~ cC2(iV21027),
inference(clausify,[status(thm)],[f_151_1]) ).
fof(f_152_1,plain,
cowlThing(iV21027),
inference(fof_nnf,[status(thm)],[axiom_151]) ).
cnf(f_152_2,plain,
cowlThing(iV21027),
inference(clausify,[status(thm)],[f_152_1]) ).
fof(f_153_1,plain,
rR1(iV21027,iV21036),
inference(fof_nnf,[status(thm)],[axiom_152]) ).
cnf(f_153_2,plain,
rR1(iV21027,iV21036),
inference(clausify,[status(thm)],[f_153_1]) ).
fof(f_154_1,plain,
rR1(iV21027,iV21035),
inference(fof_nnf,[status(thm)],[axiom_153]) ).
cnf(f_154_2,plain,
rR1(iV21027,iV21035),
inference(clausify,[status(thm)],[f_154_1]) ).
fof(f_155_1,plain,
cowlThing(iV21028),
inference(fof_nnf,[status(thm)],[axiom_154]) ).
cnf(f_155_2,plain,
cowlThing(iV21028),
inference(clausify,[status(thm)],[f_155_1]) ).
fof(f_156_1,plain,
~ cC148(iV21029),
inference(fof_nnf,[status(thm)],[axiom_155]) ).
cnf(f_156_2,plain,
~ cC148(iV21029),
inference(clausify,[status(thm)],[f_156_1]) ).
fof(f_157_1,plain,
~ cC68(iV21029),
inference(fof_nnf,[status(thm)],[axiom_156]) ).
cnf(f_157_2,plain,
~ cC68(iV21029),
inference(clausify,[status(thm)],[f_157_1]) ).
fof(f_158_1,plain,
~ cC46(iV21029),
inference(fof_nnf,[status(thm)],[axiom_157]) ).
cnf(f_158_2,plain,
~ cC46(iV21029),
inference(clausify,[status(thm)],[f_158_1]) ).
fof(f_159_1,plain,
~ cC104(iV21029),
inference(fof_nnf,[status(thm)],[axiom_158]) ).
cnf(f_159_2,plain,
~ cC104(iV21029),
inference(clausify,[status(thm)],[f_159_1]) ).
fof(f_160_1,plain,
! [X] :
( cC100(X)
| ~ rR1(iV21029,X) ),
inference(fof_nnf,[status(thm)],[axiom_159]) ).
fof(f_160_2,plain,
! [U_353] :
( cC100(U_353)
| ~ rR1(iV21029,U_353) ),
inference(variable_rename,[status(thm)],[f_160_1]) ).
cnf(f_160_3,plain,
( cC100(U_353)
| ~ rR1(iV21029,U_353) ),
inference(clausify,[status(thm)],[f_160_2]) ).
fof(f_161_1,plain,
~ cC176(iV21029),
inference(fof_nnf,[status(thm)],[axiom_160]) ).
cnf(f_161_2,plain,
~ cC176(iV21029),
inference(clausify,[status(thm)],[f_161_1]) ).
fof(f_162_1,plain,
~ cC142(iV21029),
inference(fof_nnf,[status(thm)],[axiom_161]) ).
cnf(f_162_2,plain,
~ cC142(iV21029),
inference(clausify,[status(thm)],[f_162_1]) ).
fof(f_163_1,plain,
! [X] :
( cC92(X)
| ~ rR1(iV21029,X) ),
inference(fof_nnf,[status(thm)],[axiom_162]) ).
fof(f_163_2,plain,
! [U_354] :
( cC92(U_354)
| ~ rR1(iV21029,U_354) ),
inference(variable_rename,[status(thm)],[f_163_1]) ).
cnf(f_163_3,plain,
( cC92(U_354)
| ~ rR1(iV21029,U_354) ),
inference(clausify,[status(thm)],[f_163_2]) ).
fof(f_164_1,plain,
~ cC12(iV21029),
inference(fof_nnf,[status(thm)],[axiom_163]) ).
cnf(f_164_2,plain,
~ cC12(iV21029),
inference(clausify,[status(thm)],[f_164_1]) ).
fof(f_165_1,plain,
cC2(iV21029),
inference(fof_nnf,[status(thm)],[axiom_164]) ).
cnf(f_165_2,plain,
cC2(iV21029),
inference(clausify,[status(thm)],[f_165_1]) ).
fof(f_166_1,plain,
~ cC74(iV21029),
inference(fof_nnf,[status(thm)],[axiom_165]) ).
cnf(f_166_2,plain,
~ cC74(iV21029),
inference(clausify,[status(thm)],[f_166_1]) ).
fof(f_167_1,plain,
~ cC120(iV21029),
inference(fof_nnf,[status(thm)],[axiom_166]) ).
cnf(f_167_2,plain,
~ cC120(iV21029),
inference(clausify,[status(thm)],[f_167_1]) ).
fof(f_168_1,plain,
cC92(iV21029),
inference(fof_nnf,[status(thm)],[axiom_167]) ).
cnf(f_168_2,plain,
cC92(iV21029),
inference(clausify,[status(thm)],[f_168_1]) ).
fof(f_169_1,plain,
~ cC52(iV21029),
inference(fof_nnf,[status(thm)],[axiom_168]) ).
cnf(f_169_2,plain,
~ cC52(iV21029),
inference(clausify,[status(thm)],[f_169_1]) ).
fof(f_170_1,plain,
~ cC32(iV21029),
inference(fof_nnf,[status(thm)],[axiom_169]) ).
cnf(f_170_2,plain,
~ cC32(iV21029),
inference(clausify,[status(thm)],[f_170_1]) ).
fof(f_171_1,plain,
cC100(iV21029),
inference(fof_nnf,[status(thm)],[axiom_170]) ).
cnf(f_171_2,plain,
cC100(iV21029),
inference(clausify,[status(thm)],[f_171_1]) ).
fof(f_172_1,plain,
cC18(iV21029),
inference(fof_nnf,[status(thm)],[axiom_171]) ).
cnf(f_172_2,plain,
cC18(iV21029),
inference(clausify,[status(thm)],[f_172_1]) ).
fof(f_173_1,plain,
~ cC170(iV21029),
inference(fof_nnf,[status(thm)],[axiom_172]) ).
cnf(f_173_2,plain,
~ cC170(iV21029),
inference(clausify,[status(thm)],[f_173_1]) ).
fof(f_174_1,plain,
~ cC26(iV21029),
inference(fof_nnf,[status(thm)],[axiom_173]) ).
cnf(f_174_2,plain,
~ cC26(iV21029),
inference(clausify,[status(thm)],[f_174_1]) ).
fof(f_175_1,plain,
~ cC96(iV21029),
inference(fof_nnf,[status(thm)],[axiom_174]) ).
cnf(f_175_2,plain,
~ cC96(iV21029),
inference(clausify,[status(thm)],[f_175_1]) ).
fof(f_176_1,plain,
~ cC126(iV21029),
inference(fof_nnf,[status(thm)],[axiom_175]) ).
cnf(f_176_2,plain,
~ cC126(iV21029),
inference(clausify,[status(thm)],[f_176_1]) ).
fof(f_177_1,plain,
! [X] :
( cC6(X)
| ~ rR1(iV21029,X) ),
inference(fof_nnf,[status(thm)],[axiom_176]) ).
fof(f_177_2,plain,
! [U_355] :
( cC6(U_355)
| ~ rR1(iV21029,U_355) ),
inference(variable_rename,[status(thm)],[f_177_1]) ).
cnf(f_177_3,plain,
( cC6(U_355)
| ~ rR1(iV21029,U_355) ),
inference(clausify,[status(thm)],[f_177_2]) ).
fof(f_178_1,plain,
~ cC164(iV21029),
inference(fof_nnf,[status(thm)],[axiom_177]) ).
cnf(f_178_2,plain,
~ cC164(iV21029),
inference(clausify,[status(thm)],[f_178_1]) ).
fof(f_179_1,plain,
~ cC160(iV21029),
inference(fof_nnf,[status(thm)],[axiom_178]) ).
cnf(f_179_2,plain,
~ cC160(iV21029),
inference(clausify,[status(thm)],[f_179_1]) ).
fof(f_180_1,plain,
! [X] :
( cC18(X)
| ~ rR1(iV21029,X) ),
inference(fof_nnf,[status(thm)],[axiom_179]) ).
fof(f_180_2,plain,
! [U_356] :
( cC18(U_356)
| ~ rR1(iV21029,U_356) ),
inference(variable_rename,[status(thm)],[f_180_1]) ).
cnf(f_180_3,plain,
( cC18(U_356)
| ~ rR1(iV21029,U_356) ),
inference(clausify,[status(thm)],[f_180_2]) ).
fof(f_181_1,plain,
cowlThing(iV21029),
inference(fof_nnf,[status(thm)],[axiom_180]) ).
cnf(f_181_2,plain,
cowlThing(iV21029),
inference(clausify,[status(thm)],[f_181_1]) ).
fof(f_182_1,plain,
rR1(iV21029,iV21034),
inference(fof_nnf,[status(thm)],[axiom_181]) ).
cnf(f_182_2,plain,
rR1(iV21029,iV21034),
inference(clausify,[status(thm)],[f_182_1]) ).
fof(f_183_1,plain,
rR1(iV21029,iV21033),
inference(fof_nnf,[status(thm)],[axiom_182]) ).
cnf(f_183_2,plain,
rR1(iV21029,iV21033),
inference(clausify,[status(thm)],[f_183_1]) ).
fof(f_184_1,plain,
~ cC32(iV21030),
inference(fof_nnf,[status(thm)],[axiom_183]) ).
cnf(f_184_2,plain,
~ cC32(iV21030),
inference(clausify,[status(thm)],[f_184_1]) ).
fof(f_185_1,plain,
~ cC26(iV21030),
inference(fof_nnf,[status(thm)],[axiom_184]) ).
cnf(f_185_2,plain,
~ cC26(iV21030),
inference(clausify,[status(thm)],[f_185_1]) ).
fof(f_186_1,plain,
~ cC126(iV21030),
inference(fof_nnf,[status(thm)],[axiom_185]) ).
cnf(f_186_2,plain,
~ cC126(iV21030),
inference(clausify,[status(thm)],[f_186_1]) ).
fof(f_187_1,plain,
! [X] :
( cC18(X)
| ~ rR1(iV21030,X) ),
inference(fof_nnf,[status(thm)],[axiom_186]) ).
fof(f_187_2,plain,
! [U_357] :
( cC18(U_357)
| ~ rR1(iV21030,U_357) ),
inference(variable_rename,[status(thm)],[f_187_1]) ).
cnf(f_187_3,plain,
( cC18(U_357)
| ~ rR1(iV21030,U_357) ),
inference(clausify,[status(thm)],[f_187_2]) ).
fof(f_188_1,plain,
~ cC148(iV21030),
inference(fof_nnf,[status(thm)],[axiom_187]) ).
cnf(f_188_2,plain,
~ cC148(iV21030),
inference(clausify,[status(thm)],[f_188_1]) ).
fof(f_189_1,plain,
~ cC46(iV21030),
inference(fof_nnf,[status(thm)],[axiom_188]) ).
cnf(f_189_2,plain,
~ cC46(iV21030),
inference(clausify,[status(thm)],[f_189_1]) ).
fof(f_190_1,plain,
! [X] :
( cC6(X)
| ~ rR1(iV21030,X) ),
inference(fof_nnf,[status(thm)],[axiom_189]) ).
fof(f_190_2,plain,
! [U_358] :
( cC6(U_358)
| ~ rR1(iV21030,U_358) ),
inference(variable_rename,[status(thm)],[f_190_1]) ).
cnf(f_190_3,plain,
( cC6(U_358)
| ~ rR1(iV21030,U_358) ),
inference(clausify,[status(thm)],[f_190_2]) ).
fof(f_191_1,plain,
cC12(iV21030),
inference(fof_nnf,[status(thm)],[axiom_190]) ).
cnf(f_191_2,plain,
cC12(iV21030),
inference(clausify,[status(thm)],[f_191_1]) ).
fof(f_192_1,plain,
~ cC68(iV21030),
inference(fof_nnf,[status(thm)],[axiom_191]) ).
cnf(f_192_2,plain,
~ cC68(iV21030),
inference(clausify,[status(thm)],[f_192_1]) ).
fof(f_193_1,plain,
~ cC74(iV21030),
inference(fof_nnf,[status(thm)],[axiom_192]) ).
cnf(f_193_2,plain,
~ cC74(iV21030),
inference(clausify,[status(thm)],[f_193_1]) ).
fof(f_194_1,plain,
~ cC96(iV21030),
inference(fof_nnf,[status(thm)],[axiom_193]) ).
cnf(f_194_2,plain,
~ cC96(iV21030),
inference(clausify,[status(thm)],[f_194_1]) ).
fof(f_195_1,plain,
~ cC176(iV21030),
inference(fof_nnf,[status(thm)],[axiom_194]) ).
cnf(f_195_2,plain,
~ cC176(iV21030),
inference(clausify,[status(thm)],[f_195_1]) ).
fof(f_196_1,plain,
cC2(iV21030),
inference(fof_nnf,[status(thm)],[axiom_195]) ).
cnf(f_196_2,plain,
cC2(iV21030),
inference(clausify,[status(thm)],[f_196_1]) ).
fof(f_197_1,plain,
~ cC104(iV21030),
inference(fof_nnf,[status(thm)],[axiom_196]) ).
cnf(f_197_2,plain,
~ cC104(iV21030),
inference(clausify,[status(thm)],[f_197_1]) ).
fof(f_198_1,plain,
cC92(iV21030),
inference(fof_nnf,[status(thm)],[axiom_197]) ).
cnf(f_198_2,plain,
cC92(iV21030),
inference(clausify,[status(thm)],[f_198_1]) ).
fof(f_199_1,plain,
cC100(iV21030),
inference(fof_nnf,[status(thm)],[axiom_198]) ).
cnf(f_199_2,plain,
cC100(iV21030),
inference(clausify,[status(thm)],[f_199_1]) ).
fof(f_200_1,plain,
~ cC120(iV21030),
inference(fof_nnf,[status(thm)],[axiom_199]) ).
cnf(f_200_2,plain,
~ cC120(iV21030),
inference(clausify,[status(thm)],[f_200_1]) ).
fof(f_201_1,plain,
! [X] :
( cC100(X)
| ~ rR1(iV21030,X) ),
inference(fof_nnf,[status(thm)],[axiom_200]) ).
fof(f_201_2,plain,
! [U_359] :
( cC100(U_359)
| ~ rR1(iV21030,U_359) ),
inference(variable_rename,[status(thm)],[f_201_1]) ).
cnf(f_201_3,plain,
( cC100(U_359)
| ~ rR1(iV21030,U_359) ),
inference(clausify,[status(thm)],[f_201_2]) ).
fof(f_202_1,plain,
~ cC170(iV21030),
inference(fof_nnf,[status(thm)],[axiom_201]) ).
cnf(f_202_2,plain,
~ cC170(iV21030),
inference(clausify,[status(thm)],[f_202_1]) ).
fof(f_203_1,plain,
~ cC18(iV21030),
inference(fof_nnf,[status(thm)],[axiom_202]) ).
cnf(f_203_2,plain,
~ cC18(iV21030),
inference(clausify,[status(thm)],[f_203_1]) ).
fof(f_204_1,plain,
! [X] :
( cC92(X)
| ~ rR1(iV21030,X) ),
inference(fof_nnf,[status(thm)],[axiom_203]) ).
fof(f_204_2,plain,
! [U_360] :
( cC92(U_360)
| ~ rR1(iV21030,U_360) ),
inference(variable_rename,[status(thm)],[f_204_1]) ).
cnf(f_204_3,plain,
( cC92(U_360)
| ~ rR1(iV21030,U_360) ),
inference(clausify,[status(thm)],[f_204_2]) ).
fof(f_205_1,plain,
~ cC52(iV21030),
inference(fof_nnf,[status(thm)],[axiom_204]) ).
cnf(f_205_2,plain,
~ cC52(iV21030),
inference(clausify,[status(thm)],[f_205_1]) ).
fof(f_206_1,plain,
~ cC160(iV21030),
inference(fof_nnf,[status(thm)],[axiom_205]) ).
cnf(f_206_2,plain,
~ cC160(iV21030),
inference(clausify,[status(thm)],[f_206_1]) ).
fof(f_207_1,plain,
~ cC164(iV21030),
inference(fof_nnf,[status(thm)],[axiom_206]) ).
cnf(f_207_2,plain,
~ cC164(iV21030),
inference(clausify,[status(thm)],[f_207_1]) ).
fof(f_208_1,plain,
cowlThing(iV21030),
inference(fof_nnf,[status(thm)],[axiom_207]) ).
cnf(f_208_2,plain,
cowlThing(iV21030),
inference(clausify,[status(thm)],[f_208_1]) ).
fof(f_209_1,plain,
~ cC142(iV21030),
inference(fof_nnf,[status(thm)],[axiom_208]) ).
cnf(f_209_2,plain,
~ cC142(iV21030),
inference(clausify,[status(thm)],[f_209_1]) ).
fof(f_210_1,plain,
rR1(iV21030,iV21032),
inference(fof_nnf,[status(thm)],[axiom_209]) ).
cnf(f_210_2,plain,
rR1(iV21030,iV21032),
inference(clausify,[status(thm)],[f_210_1]) ).
fof(f_211_1,plain,
rR1(iV21030,iV21031),
inference(fof_nnf,[status(thm)],[axiom_210]) ).
cnf(f_211_2,plain,
rR1(iV21030,iV21031),
inference(clausify,[status(thm)],[f_211_1]) ).
fof(f_212_1,plain,
cowlThing(iV21031),
inference(fof_nnf,[status(thm)],[axiom_211]) ).
cnf(f_212_2,plain,
cowlThing(iV21031),
inference(clausify,[status(thm)],[f_212_1]) ).
fof(f_213_1,plain,
cC92(iV21032),
inference(fof_nnf,[status(thm)],[axiom_212]) ).
cnf(f_213_2,plain,
cC92(iV21032),
inference(clausify,[status(thm)],[f_213_1]) ).
fof(f_214_1,plain,
cC100(iV21032),
inference(fof_nnf,[status(thm)],[axiom_213]) ).
cnf(f_214_2,plain,
cC100(iV21032),
inference(clausify,[status(thm)],[f_214_1]) ).
fof(f_215_1,plain,
~ cC2(iV21032),
inference(fof_nnf,[status(thm)],[axiom_214]) ).
cnf(f_215_2,plain,
~ cC2(iV21032),
inference(clausify,[status(thm)],[f_215_1]) ).
fof(f_216_1,plain,
cC18(iV21032),
inference(fof_nnf,[status(thm)],[axiom_215]) ).
cnf(f_216_2,plain,
cC18(iV21032),
inference(clausify,[status(thm)],[f_216_1]) ).
fof(f_217_1,plain,
cC6(iV21032),
inference(fof_nnf,[status(thm)],[axiom_216]) ).
cnf(f_217_2,plain,
cC6(iV21032),
inference(clausify,[status(thm)],[f_217_1]) ).
fof(f_218_1,plain,
cowlThing(iV21032),
inference(fof_nnf,[status(thm)],[axiom_217]) ).
cnf(f_218_2,plain,
cowlThing(iV21032),
inference(clausify,[status(thm)],[f_218_1]) ).
fof(f_219_1,plain,
cC92(iV21033),
inference(fof_nnf,[status(thm)],[axiom_218]) ).
cnf(f_219_2,plain,
cC92(iV21033),
inference(clausify,[status(thm)],[f_219_1]) ).
fof(f_220_1,plain,
cC100(iV21033),
inference(fof_nnf,[status(thm)],[axiom_219]) ).
cnf(f_220_2,plain,
cC100(iV21033),
inference(clausify,[status(thm)],[f_220_1]) ).
fof(f_221_1,plain,
cC18(iV21033),
inference(fof_nnf,[status(thm)],[axiom_220]) ).
cnf(f_221_2,plain,
cC18(iV21033),
inference(clausify,[status(thm)],[f_221_1]) ).
fof(f_222_1,plain,
cC6(iV21033),
inference(fof_nnf,[status(thm)],[axiom_221]) ).
cnf(f_222_2,plain,
cC6(iV21033),
inference(clausify,[status(thm)],[f_222_1]) ).
fof(f_223_1,plain,
~ cC12(iV21033),
inference(fof_nnf,[status(thm)],[axiom_222]) ).
cnf(f_223_2,plain,
~ cC12(iV21033),
inference(clausify,[status(thm)],[f_223_1]) ).
fof(f_224_1,plain,
cowlThing(iV21033),
inference(fof_nnf,[status(thm)],[axiom_223]) ).
cnf(f_224_2,plain,
cowlThing(iV21033),
inference(clausify,[status(thm)],[f_224_1]) ).
fof(f_225_1,plain,
cC92(iV21034),
inference(fof_nnf,[status(thm)],[axiom_224]) ).
cnf(f_225_2,plain,
cC92(iV21034),
inference(clausify,[status(thm)],[f_225_1]) ).
fof(f_226_1,plain,
cC100(iV21034),
inference(fof_nnf,[status(thm)],[axiom_225]) ).
cnf(f_226_2,plain,
cC100(iV21034),
inference(clausify,[status(thm)],[f_226_1]) ).
fof(f_227_1,plain,
cC18(iV21034),
inference(fof_nnf,[status(thm)],[axiom_226]) ).
cnf(f_227_2,plain,
cC18(iV21034),
inference(clausify,[status(thm)],[f_227_1]) ).
fof(f_228_1,plain,
cC6(iV21034),
inference(fof_nnf,[status(thm)],[axiom_227]) ).
cnf(f_228_2,plain,
cC6(iV21034),
inference(clausify,[status(thm)],[f_228_1]) ).
fof(f_229_1,plain,
~ cC2(iV21034),
inference(fof_nnf,[status(thm)],[axiom_228]) ).
cnf(f_229_2,plain,
~ cC2(iV21034),
inference(clausify,[status(thm)],[f_229_1]) ).
fof(f_230_1,plain,
cowlThing(iV21034),
inference(fof_nnf,[status(thm)],[axiom_229]) ).
cnf(f_230_2,plain,
cowlThing(iV21034),
inference(clausify,[status(thm)],[f_230_1]) ).
fof(f_231_1,plain,
cC92(iV21035),
inference(fof_nnf,[status(thm)],[axiom_230]) ).
cnf(f_231_2,plain,
cC92(iV21035),
inference(clausify,[status(thm)],[f_231_1]) ).
fof(f_232_1,plain,
cC100(iV21035),
inference(fof_nnf,[status(thm)],[axiom_231]) ).
cnf(f_232_2,plain,
cC100(iV21035),
inference(clausify,[status(thm)],[f_232_1]) ).
fof(f_233_1,plain,
~ cC12(iV21035),
inference(fof_nnf,[status(thm)],[axiom_232]) ).
cnf(f_233_2,plain,
~ cC12(iV21035),
inference(clausify,[status(thm)],[f_233_1]) ).
fof(f_234_1,plain,
cC18(iV21035),
inference(fof_nnf,[status(thm)],[axiom_233]) ).
cnf(f_234_2,plain,
cC18(iV21035),
inference(clausify,[status(thm)],[f_234_1]) ).
fof(f_235_1,plain,
cC6(iV21035),
inference(fof_nnf,[status(thm)],[axiom_234]) ).
cnf(f_235_2,plain,
cC6(iV21035),
inference(clausify,[status(thm)],[f_235_1]) ).
fof(f_236_1,plain,
cowlThing(iV21035),
inference(fof_nnf,[status(thm)],[axiom_235]) ).
cnf(f_236_2,plain,
cowlThing(iV21035),
inference(clausify,[status(thm)],[f_236_1]) ).
fof(f_237_1,plain,
cC92(iV21036),
inference(fof_nnf,[status(thm)],[axiom_236]) ).
cnf(f_237_2,plain,
cC92(iV21036),
inference(clausify,[status(thm)],[f_237_1]) ).
fof(f_238_1,plain,
cC100(iV21036),
inference(fof_nnf,[status(thm)],[axiom_237]) ).
cnf(f_238_2,plain,
cC100(iV21036),
inference(clausify,[status(thm)],[f_238_1]) ).
fof(f_239_1,plain,
cC18(iV21036),
inference(fof_nnf,[status(thm)],[axiom_238]) ).
cnf(f_239_2,plain,
cC18(iV21036),
inference(clausify,[status(thm)],[f_239_1]) ).
fof(f_240_1,plain,
cC6(iV21036),
inference(fof_nnf,[status(thm)],[axiom_239]) ).
cnf(f_240_2,plain,
cC6(iV21036),
inference(clausify,[status(thm)],[f_240_1]) ).
fof(f_241_1,plain,
~ cC2(iV21036),
inference(fof_nnf,[status(thm)],[axiom_240]) ).
cnf(f_241_2,plain,
~ cC2(iV21036),
inference(clausify,[status(thm)],[f_241_1]) ).
fof(f_242_1,plain,
cowlThing(iV21036),
inference(fof_nnf,[status(thm)],[axiom_241]) ).
cnf(f_242_2,plain,
cowlThing(iV21036),
inference(clausify,[status(thm)],[f_242_1]) ).
fof(f_243_1,negated_conjecture,
~ ( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_243_2,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_243_1]) ).
fof(f_243_3,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [U_362] :
( ( ~ xsd_string(U_362)
& ~ xsd_integer(U_362) )
| ( xsd_integer(U_362)
& xsd_string(U_362) ) )
| ? [U_361] :
( cowlNothing(U_361)
| ~ cowlThing(U_361) ) ),
inference(variable_rename,[status(thm)],[f_243_2]) ).
fof(f_243_4,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [U_366] :
( ~ xsd_string(U_366)
& ~ xsd_integer(U_366) )
| ? [U_365] :
( xsd_integer(U_365)
& xsd_string(U_365) )
| ? [U_364] : cowlNothing(U_364)
| ? [U_363] : ~ cowlThing(U_363) ),
inference(miniscope,[status(thm)],[f_243_3]) ).
fof(f_243_5,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [U_366] :
( ~ xsd_string(U_366)
& ~ xsd_integer(U_366) )
| ? [U_365] :
( xsd_integer(U_365)
& xsd_string(U_365) )
| ? [U_364] : cowlNothing(U_364)
| ~ cowlThing(sK37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(U_363,sK37)],[f_243_4]) ).
fof(f_243_6,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [U_366] :
( ~ xsd_string(U_366)
& ~ xsd_integer(U_366) )
| ? [U_365] :
( xsd_integer(U_365)
& xsd_string(U_365) )
| cowlNothing(sK38)
| ~ cowlThing(sK37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(U_364,sK38)],[f_243_5]) ).
fof(f_243_7,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [U_366] :
( ~ xsd_string(U_366)
& ~ xsd_integer(U_366) )
| ( xsd_integer(sK39)
& xsd_string(sK39) )
| cowlNothing(sK38)
| ~ cowlThing(sK37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(U_365,sK39)],[f_243_6]) ).
fof(f_243_8,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ( ~ xsd_string(sK40)
& ~ xsd_integer(sK40) )
| ( xsd_integer(sK39)
& xsd_string(sK39) )
| cowlNothing(sK38)
| ~ cowlThing(sK37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(U_366,sK40)],[f_243_7]) ).
fof(f_243_9,negated_conjecture,
( ( ~ xsd_string(sK40)
| ~ sP1 )
& ( ~ xsd_integer(sK40)
| ~ sP1 )
& ( xsd_integer(sK39)
| ~ sP0 )
& ( xsd_string(sK39)
| ~ sP0 )
& ( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| sP1
| sP0
| cowlNothing(sK38)
| ~ cowlThing(sK37) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_243_8]) ).
cnf(f_243_10,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| sP1
| sP0
| cowlNothing(sK38)
| ~ cowlThing(sK37) ),
inference(clausify,[status(thm)],[f_243_9]) ).
cnf(f_243_11,negated_conjecture,
( xsd_string(sK39)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_243_9]) ).
cnf(f_243_12,negated_conjecture,
( xsd_integer(sK39)
| ~ sP0 ),
inference(clausify,[status(thm)],[f_243_9]) ).
cnf(f_243_13,negated_conjecture,
( ~ xsd_integer(sK40)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_243_9]) ).
cnf(f_243_14,negated_conjecture,
( ~ xsd_string(sK40)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_243_9]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS151+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.10/0.34 % Computer : n026.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Sat Sep 19 12:19:05 UTC 2026
% 0.10/0.35 % CPUTime :
% 9.16/9.45 % SZS status Theorem for theBenchmark
% 9.16/9.45 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------