%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : CSR040+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:14:18 PM UTC 2026
% Result : Theorem 0.27s 1.64s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 146
% Syntax : Number of formulae : 467 ( 126 unt; 0 def)
% Number of atoms : 852 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 666 ( 281 ~; 266 |; 16 &)
% ( 0 <=>; 103 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 1 prp; 0-3 aty)
% Number of functors : 40 ( 40 usr; 37 con; 0-2 aty)
% Number of variables : 538 ( 38 sgn 326 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query40,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query40) ).
fof(just135,axiom,
! [X7,X9] : natargument(f_contentmtofcdafromeventfn(X7,X9),n_2,X9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just135) ).
fof(just134,axiom,
! [X7,X9] : natargument(f_contentmtofcdafromeventfn(X7,X9),n_1,X7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just134) ).
fof(just48,axiom,
! [X1,X2,X3] :
~ ( isa(X1,X2)
& isa(X1,X3)
& disjointwith(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just48) ).
fof(just54,axiom,
! [X10,X11,X12] :
( ( genlpreds(X10,X11)
& genlpreds(X11,X12) )
=> genlpreds(X10,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just54) ).
fof(just49,axiom,
! [X4,X5,X6] :
( ( genlinverse(X4,X5)
& genlinverse(X5,X6) )
=> genlpreds(X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just49) ).
fof(just60,axiom,
! [X7,X13,X14] :
( ( genlinverse(X7,X13)
& genlpreds(X13,X14) )
=> genlinverse(X7,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just60) ).
fof(just59,axiom,
! [X13,X9,X14] :
( ( genlinverse(X13,X9)
& genlpreds(X14,X13) )
=> genlinverse(X14,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just59) ).
fof(just111,axiom,
! [X7,X13,X14] :
( ( isa(X7,X13)
& genls(X13,X14) )
=> isa(X7,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just111) ).
fof(just102,axiom,
! [X7,X13,X14] :
( ( disjointwith(X7,X13)
& genls(X14,X13) )
=> disjointwith(X7,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just102) ).
fof(just103,axiom,
! [X13,X9,X14] :
( ( disjointwith(X13,X9)
& genls(X14,X13) )
=> disjointwith(X14,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just103) ).
fof(just125,axiom,
! [X7,X13,X14] :
( ( genls(X7,X13)
& genls(X13,X14) )
=> genls(X7,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just125) ).
fof(just121,axiom,
! [X10,X11,X12] :
( ( genls(X10,X11)
& genls(X11,X12) )
=> genls(X10,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just121) ).
fof(just124,axiom,
! [X13,X9,X14] :
( ( genls(X13,X9)
& genls(X14,X13) )
=> genls(X14,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just124) ).
fof(just142,axiom,
! [X10,X11,X12] :
( ( genlmt(X10,X11)
& genlmt(X11,X12) )
=> genlmt(X10,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just142) ).
fof(just131,axiom,
! [X7] : natargument(f_urlreferentfn(X7),n_1,X7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just131) ).
fof(just128,axiom,
! [X7] : natargument(f_urlfn(X7),n_1,X7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just128) ).
fof(just133,axiom,
! [X7,X9] : natfunction(f_contentmtofcdafromeventfn(X7,X9),c_contentmtofcdafromeventfn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just133) ).
fof(just101,axiom,
! [X10,X11] :
( disjointwith(X10,X11)
=> disjointwith(X11,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just101) ).
fof(just137,axiom,
! [X15,X16] :
( ( mtvisible(X15)
& genlmt(X15,X16) )
=> mtvisible(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just137) ).
fof(just136,axiom,
! [X7,X9] : microtheory(f_contentmtofcdafromeventfn(X7,X9)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just136) ).
fof(just141,axiom,
! [X8,X9] :
( genlmt(X8,X9)
=> microtheory(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just141) ).
fof(just140,axiom,
! [X8,X9] :
( genlmt(X8,X9)
=> microtheory(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just140) ).
fof(just139,axiom,
! [X7,X8] :
( genlmt(X7,X8)
=> microtheory(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just139) ).
fof(just138,axiom,
! [X7,X8] :
( genlmt(X7,X8)
=> microtheory(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just138) ).
fof(just110,axiom,
! [X8,X9] :
( isa(X8,X9)
=> thing(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just110) ).
fof(just109,axiom,
! [X8,X9] :
( isa(X8,X9)
=> thing(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just109) ).
fof(just58,axiom,
! [X8,X9] :
( genlinverse(X8,X9)
=> binarypredicate(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just58) ).
fof(just57,axiom,
! [X7,X8] :
( genlinverse(X7,X8)
=> binarypredicate(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just57) ).
fof(just53,axiom,
! [X8,X9] :
( genlpreds(X8,X9)
=> predicate(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just53) ).
fof(just52,axiom,
! [X8,X9] :
( genlpreds(X8,X9)
=> predicate(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just52) ).
fof(just51,axiom,
! [X7,X8] :
( genlpreds(X7,X8)
=> predicate(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just51) ).
fof(just50,axiom,
! [X7,X8] :
( genlpreds(X7,X8)
=> predicate(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just50) ).
fof(just100,axiom,
! [X8,X9] :
( disjointwith(X8,X9)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just100) ).
fof(just120,axiom,
! [X8,X9] :
( genls(X8,X9)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just120) ).
fof(just119,axiom,
! [X8,X9] :
( genls(X8,X9)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just119) ).
fof(just108,axiom,
! [X7,X8] :
( isa(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just108) ).
fof(just107,axiom,
! [X7,X8] :
( isa(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just107) ).
fof(just99,axiom,
! [X7,X8] :
( disjointwith(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just99) ).
fof(just118,axiom,
! [X7,X8] :
( genls(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just118) ).
fof(just117,axiom,
! [X7,X8] :
( genls(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just117) ).
fof(just91,axiom,
! [X10] :
( isa(X10,c_tptpcol_16_62187)
=> tptpcol_16_62187(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just91) ).
fof(just61,axiom,
! [X10] :
( isa(X10,c_tptpcol_15_109185)
=> tptpcol_15_109185(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just61) ).
fof(just63,axiom,
! [X10] :
( isa(X10,c_tptpcol_14_109181)
=> tptpcol_14_109181(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just63) ).
fof(just65,axiom,
! [X10] :
( isa(X10,c_tptpcol_13_109173)
=> tptpcol_13_109173(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just65) ).
fof(just67,axiom,
! [X10] :
( isa(X10,c_tptpcol_12_109157)
=> tptpcol_12_109157(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just67) ).
fof(just69,axiom,
! [X10] :
( isa(X10,c_tptpcol_11_109125)
=> tptpcol_11_109125(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just69) ).
fof(just71,axiom,
! [X10] :
( isa(X10,c_tptpcol_10_109061)
=> tptpcol_10_109061(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just71) ).
fof(just73,axiom,
! [X10] :
( isa(X10,c_tptpcol_9_109060)
=> tptpcol_9_109060(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just73) ).
fof(just75,axiom,
! [X10] :
( isa(X10,c_tptpcol_8_109059)
=> tptpcol_8_109059(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just75) ).
fof(just77,axiom,
! [X10] :
( isa(X10,c_tptpcol_7_108547)
=> tptpcol_7_108547(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just77) ).
fof(just79,axiom,
! [X10] :
( isa(X10,c_tptpcol_6_108546)
=> tptpcol_6_108546(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just79) ).
fof(just81,axiom,
! [X10] :
( isa(X10,c_tptpcol_5_106498)
=> tptpcol_5_106498(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just81) ).
fof(just83,axiom,
! [X10] :
( isa(X10,c_tptpcol_4_106497)
=> tptpcol_4_106497(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just83) ).
fof(just85,axiom,
! [X10] :
( isa(X10,c_tptpcol_3_98305)
=> tptpcol_3_98305(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just85) ).
fof(just87,axiom,
! [X10] :
( isa(X10,c_tptpcol_2_98304)
=> tptpcol_2_98304(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just87) ).
fof(just89,axiom,
! [X10] :
( isa(X10,c_tptpcol_1_65536)
=> tptpcol_1_65536(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just89) ).
fof(just93,axiom,
! [X10] :
( isa(X10,c_tptpcol_0_0)
=> tptpcol_0_0(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just93) ).
fof(just95,axiom,
! [X10] :
( isa(X10,c_individual)
=> individual(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just95) ).
fof(just97,axiom,
! [X10] :
( isa(X10,c_collection)
=> collection(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just97) ).
fof(just105,axiom,
! [X10] :
( isa(X10,c_transitivebinarypredicate)
=> transitivebinarypredicate(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just105) ).
fof(just113,axiom,
! [X10] :
( isa(X10,c_fixedordercollection)
=> fixedordercollection(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just113) ).
fof(just115,axiom,
! [X10] :
( isa(X10,c_firstordercollection)
=> firstordercollection(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just115) ).
fof(just56,axiom,
! [X10] :
( predicate(X10)
=> genlpreds(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just56) ).
fof(just55,axiom,
! [X10] :
( predicate(X10)
=> genlpreds(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just55) ).
fof(just123,axiom,
! [X10] :
( collection(X10)
=> genls(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just123) ).
fof(just122,axiom,
! [X10] :
( collection(X10)
=> genls(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just122) ).
fof(just144,axiom,
! [X10] :
( microtheory(X10)
=> genlmt(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just144) ).
fof(just143,axiom,
! [X10] :
( microtheory(X10)
=> genlmt(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just143) ).
fof(just106,axiom,
! [X10] :
( transitivebinarypredicate(X10)
=> isa(X10,c_transitivebinarypredicate) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just106) ).
fof(just62,axiom,
! [X10] :
( tptpcol_15_109185(X10)
=> isa(X10,c_tptpcol_15_109185) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just62) ).
fof(just64,axiom,
! [X10] :
( tptpcol_14_109181(X10)
=> isa(X10,c_tptpcol_14_109181) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just64) ).
fof(just66,axiom,
! [X10] :
( tptpcol_13_109173(X10)
=> isa(X10,c_tptpcol_13_109173) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just66) ).
fof(just68,axiom,
! [X10] :
( tptpcol_12_109157(X10)
=> isa(X10,c_tptpcol_12_109157) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just68) ).
fof(just70,axiom,
! [X10] :
( tptpcol_11_109125(X10)
=> isa(X10,c_tptpcol_11_109125) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just70) ).
fof(just72,axiom,
! [X10] :
( tptpcol_10_109061(X10)
=> isa(X10,c_tptpcol_10_109061) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just72) ).
fof(just74,axiom,
! [X10] :
( tptpcol_9_109060(X10)
=> isa(X10,c_tptpcol_9_109060) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just74) ).
fof(just76,axiom,
! [X10] :
( tptpcol_8_109059(X10)
=> isa(X10,c_tptpcol_8_109059) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just76) ).
fof(just78,axiom,
! [X10] :
( tptpcol_7_108547(X10)
=> isa(X10,c_tptpcol_7_108547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just78) ).
fof(just80,axiom,
! [X10] :
( tptpcol_6_108546(X10)
=> isa(X10,c_tptpcol_6_108546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just80) ).
fof(just82,axiom,
! [X10] :
( tptpcol_5_106498(X10)
=> isa(X10,c_tptpcol_5_106498) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just82) ).
fof(just84,axiom,
! [X10] :
( tptpcol_4_106497(X10)
=> isa(X10,c_tptpcol_4_106497) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just84) ).
fof(just86,axiom,
! [X10] :
( tptpcol_3_98305(X10)
=> isa(X10,c_tptpcol_3_98305) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just86) ).
fof(just88,axiom,
! [X10] :
( tptpcol_2_98304(X10)
=> isa(X10,c_tptpcol_2_98304) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just88) ).
fof(just90,axiom,
! [X10] :
( tptpcol_1_65536(X10)
=> isa(X10,c_tptpcol_1_65536) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just90) ).
fof(just92,axiom,
! [X10] :
( tptpcol_16_62187(X10)
=> isa(X10,c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just92) ).
fof(just94,axiom,
! [X10] :
( tptpcol_0_0(X10)
=> isa(X10,c_tptpcol_0_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just94) ).
fof(just96,axiom,
! [X10] :
( individual(X10)
=> isa(X10,c_individual) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just96) ).
fof(just98,axiom,
! [X10] :
( collection(X10)
=> isa(X10,c_collection) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just98) ).
fof(just114,axiom,
! [X10] :
( fixedordercollection(X10)
=> isa(X10,c_fixedordercollection) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just114) ).
fof(just116,axiom,
! [X10] :
( firstordercollection(X10)
=> isa(X10,c_firstordercollection) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just116) ).
fof(just130,axiom,
! [X7] : natfunction(f_urlreferentfn(X7),c_urlreferentfn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just130) ).
fof(just127,axiom,
! [X7] : natfunction(f_urlfn(X7),c_urlfn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just127) ).
fof(just9,axiom,
! [X1] :
~ ( collection(X1)
& individual(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just9) ).
fof(just47,axiom,
! [X1] :
( tptpcol_15_109185(X1)
=> tptpcol_14_109181(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just47) ).
fof(just45,axiom,
! [X1] :
( tptpcol_14_109181(X1)
=> tptpcol_13_109173(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just45) ).
fof(just43,axiom,
! [X1] :
( tptpcol_13_109173(X1)
=> tptpcol_12_109157(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just43) ).
fof(just41,axiom,
! [X1] :
( tptpcol_12_109157(X1)
=> tptpcol_11_109125(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just41) ).
fof(just39,axiom,
! [X1] :
( tptpcol_11_109125(X1)
=> tptpcol_10_109061(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just39) ).
fof(just37,axiom,
! [X1] :
( tptpcol_10_109061(X1)
=> tptpcol_9_109060(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just37) ).
fof(just35,axiom,
! [X1] :
( tptpcol_9_109060(X1)
=> tptpcol_8_109059(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just35) ).
fof(just33,axiom,
! [X1] :
( tptpcol_8_109059(X1)
=> tptpcol_7_108547(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just33) ).
fof(just31,axiom,
! [X1] :
( tptpcol_7_108547(X1)
=> tptpcol_6_108546(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just31) ).
fof(just29,axiom,
! [X1] :
( tptpcol_6_108546(X1)
=> tptpcol_5_106498(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just29) ).
fof(just27,axiom,
! [X1] :
( tptpcol_5_106498(X1)
=> tptpcol_4_106497(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just27) ).
fof(just25,axiom,
! [X1] :
( tptpcol_4_106497(X1)
=> tptpcol_3_98305(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just25) ).
fof(just23,axiom,
! [X1] :
( tptpcol_3_98305(X1)
=> tptpcol_2_98304(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just23) ).
fof(just21,axiom,
! [X1] :
( tptpcol_2_98304(X1)
=> tptpcol_1_65536(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just21) ).
fof(just19,axiom,
! [X1] :
( tptpcol_1_65536(X1)
=> tptpcol_0_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just19) ).
fof(just16,axiom,
! [X1] :
( tptpcol_0_0(X1)
=> individual(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just16) ).
fof(just14,axiom,
! [X1] :
( fixedordercollection(X1)
=> collection(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just14) ).
fof(just4,axiom,
! [X1] :
( firstordercollection(X1)
=> fixedordercollection(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just4) ).
fof(just132,axiom,
! [X7] : computerdataartifact(f_urlreferentfn(X7)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just132) ).
fof(just129,axiom,
! [X7] : uniformresourcelocator(f_urlfn(X7)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just129) ).
fof(just1,axiom,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14),c_machinelearningspindleheadmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just1) ).
fof(just10,axiom,
disjointwith(c_collection,c_individual),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just10) ).
fof(just46,axiom,
genls(c_tptpcol_15_109185,c_tptpcol_14_109181),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just46) ).
fof(just44,axiom,
genls(c_tptpcol_14_109181,c_tptpcol_13_109173),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just44) ).
fof(just42,axiom,
genls(c_tptpcol_13_109173,c_tptpcol_12_109157),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just42) ).
fof(just40,axiom,
genls(c_tptpcol_12_109157,c_tptpcol_11_109125),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just40) ).
fof(just38,axiom,
genls(c_tptpcol_11_109125,c_tptpcol_10_109061),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just38) ).
fof(just36,axiom,
genls(c_tptpcol_10_109061,c_tptpcol_9_109060),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just36) ).
fof(just34,axiom,
genls(c_tptpcol_9_109060,c_tptpcol_8_109059),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just34) ).
fof(just32,axiom,
genls(c_tptpcol_8_109059,c_tptpcol_7_108547),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just32) ).
fof(just30,axiom,
genls(c_tptpcol_7_108547,c_tptpcol_6_108546),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just30) ).
fof(just28,axiom,
genls(c_tptpcol_6_108546,c_tptpcol_5_106498),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just28) ).
fof(just26,axiom,
genls(c_tptpcol_5_106498,c_tptpcol_4_106497),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just26) ).
fof(just24,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just24) ).
fof(just22,axiom,
genls(c_tptpcol_3_98305,c_tptpcol_2_98304),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just22) ).
fof(just20,axiom,
genls(c_tptpcol_2_98304,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just20) ).
fof(just18,axiom,
genls(c_tptpcol_1_65536,c_tptpcol_0_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just18) ).
fof(just15,axiom,
genls(c_tptpcol_0_0,c_individual),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just15) ).
fof(just13,axiom,
genls(c_fixedordercollection,c_collection),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just13) ).
fof(just3,axiom,
genls(c_firstordercollection,c_fixedordercollection),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just3) ).
fof(just8,axiom,
genlmt(c_corecyclmt,c_logicaltruthmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just8) ).
fof(just6,axiom,
genlmt(c_universalvocabularymt,c_corecyclmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just6) ).
fof(just5,axiom,
genlmt(c_cycnounlearnermt,c_cycorpproductsmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just5) ).
fof(just12,axiom,
genlmt(c_basekb,c_universalvocabularymt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just12) ).
fof(just2,axiom,
genlmt(c_cycorpproductsmt,c_basekb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just2) ).
fof(just11,axiom,
genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just11) ).
fof(just104,axiom,
mtvisible(c_logicaltruthmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just104) ).
fof(just112,axiom,
mtvisible(c_corecyclmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just112) ).
fof(just145,axiom,
mtvisible(c_universalvocabularymt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just145) ).
fof(just126,axiom,
mtvisible(c_basekb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just126) ).
fof(just7,axiom,
transitivebinarypredicate(c_genlmt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just7) ).
fof(just17,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just17) ).
fof(i_0_146,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[query40])]) ).
fof(i_0_147,plain,
! [X324,X325] : natargument(f_contentmtofcdafromeventfn(X324,X325),n_2,X325),
inference(variable_rename,[status(thm)],[just135]) ).
fof(i_0_148,plain,
! [X322,X323] : natargument(f_contentmtofcdafromeventfn(X322,X323),n_1,X322),
inference(variable_rename,[status(thm)],[just134]) ).
fof(i_0_149,plain,
! [X199,X200,X201] :
( ~ isa(X199,X200)
| ~ isa(X199,X201)
| ~ disjointwith(X200,X201) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just48])]) ).
fof(i_0_150,plain,
! [X213,X214,X215] :
( ~ genlpreds(X213,X214)
| ~ genlpreds(X214,X215)
| genlpreds(X213,X215) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just54])]) ).
fof(i_0_151,plain,
! [X202,X203,X204] :
( ~ genlinverse(X202,X203)
| ~ genlinverse(X203,X204)
| genlpreds(X202,X204) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just49])]) ).
fof(i_0_152,plain,
! [X225,X226,X227] :
( ~ genlinverse(X225,X226)
| ~ genlpreds(X226,X227)
| genlinverse(X225,X227) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just60])]) ).
fof(i_0_153,plain,
! [X222,X223,X224] :
( ~ genlinverse(X222,X223)
| ~ genlpreds(X224,X222)
| genlinverse(X224,X223) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just59])]) ).
fof(i_0_154,plain,
! [X288,X289,X290] :
( ~ isa(X288,X289)
| ~ genls(X289,X290)
| isa(X288,X290) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just111])]) ).
fof(i_0_155,plain,
! [X272,X273,X274] :
( ~ disjointwith(X272,X273)
| ~ genls(X274,X273)
| disjointwith(X272,X274) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just102])]) ).
fof(i_0_156,plain,
! [X275,X276,X277] :
( ~ disjointwith(X275,X276)
| ~ genls(X277,X275)
| disjointwith(X277,X276) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just103])]) ).
fof(i_0_157,plain,
! [X311,X312,X313] :
( ~ genls(X311,X312)
| ~ genls(X312,X313)
| genls(X311,X313) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just125])]) ).
fof(i_0_158,plain,
! [X303,X304,X305] :
( ~ genls(X303,X304)
| ~ genls(X304,X305)
| genls(X303,X305) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just121])]) ).
fof(i_0_159,plain,
! [X308,X309,X310] :
( ~ genls(X308,X309)
| ~ genls(X310,X308)
| genls(X310,X309) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just124])]) ).
fof(i_0_160,plain,
! [X338,X339,X340] :
( ~ genlmt(X338,X339)
| ~ genlmt(X339,X340)
| genlmt(X338,X340) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just142])]) ).
fof(i_0_161,plain,
! [X318] : natargument(f_urlreferentfn(X318),n_1,X318),
inference(variable_rename,[status(thm)],[just131]) ).
fof(i_0_162,plain,
! [X315] : natargument(f_urlfn(X315),n_1,X315),
inference(variable_rename,[status(thm)],[just128]) ).
fof(i_0_163,negated_conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
& tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(fof_nnf,[status(thm)],[i_0_146]) ).
fof(i_0_164,plain,
! [X320,X321] : natfunction(f_contentmtofcdafromeventfn(X320,X321),c_contentmtofcdafromeventfn),
inference(variable_rename,[status(thm)],[just133]) ).
fof(i_0_165,plain,
! [X270,X271] :
( ~ disjointwith(X270,X271)
| disjointwith(X271,X270) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just101])]) ).
fof(i_0_166,plain,
! [X328,X329] :
( ~ mtvisible(X328)
| ~ genlmt(X328,X329)
| mtvisible(X329) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just137])]) ).
fof(i_0_167,plain,
! [X326,X327] : microtheory(f_contentmtofcdafromeventfn(X326,X327)),
inference(variable_rename,[status(thm)],[just136]) ).
fof(i_0_168,plain,
! [X336,X337] :
( ~ genlmt(X336,X337)
| microtheory(X336) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just141])]) ).
fof(i_0_169,plain,
! [X334,X335] :
( ~ genlmt(X334,X335)
| microtheory(X334) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just140])]) ).
fof(i_0_170,plain,
! [X332,X333] :
( ~ genlmt(X332,X333)
| microtheory(X333) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just139])]) ).
fof(i_0_171,plain,
! [X330,X331] :
( ~ genlmt(X330,X331)
| microtheory(X331) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just138])]) ).
fof(i_0_172,plain,
! [X286,X287] :
( ~ isa(X286,X287)
| thing(X286) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just110])]) ).
fof(i_0_173,plain,
! [X284,X285] :
( ~ isa(X284,X285)
| thing(X284) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just109])]) ).
fof(i_0_174,plain,
! [X220,X221] :
( ~ genlinverse(X220,X221)
| binarypredicate(X220) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just58])]) ).
fof(i_0_175,plain,
! [X218,X219] :
( ~ genlinverse(X218,X219)
| binarypredicate(X219) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just57])]) ).
fof(i_0_176,plain,
! [X211,X212] :
( ~ genlpreds(X211,X212)
| predicate(X211) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just53])]) ).
fof(i_0_177,plain,
! [X209,X210] :
( ~ genlpreds(X209,X210)
| predicate(X209) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just52])]) ).
fof(i_0_178,plain,
! [X207,X208] :
( ~ genlpreds(X207,X208)
| predicate(X208) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just51])]) ).
fof(i_0_179,plain,
! [X205,X206] :
( ~ genlpreds(X205,X206)
| predicate(X206) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just50])]) ).
fof(i_0_180,plain,
! [X268,X269] :
( ~ disjointwith(X268,X269)
| collection(X268) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just100])]) ).
fof(i_0_181,plain,
! [X301,X302] :
( ~ genls(X301,X302)
| collection(X301) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just120])]) ).
fof(i_0_182,plain,
! [X299,X300] :
( ~ genls(X299,X300)
| collection(X299) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just119])]) ).
fof(i_0_183,plain,
! [X282,X283] :
( ~ isa(X282,X283)
| collection(X283) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just108])]) ).
fof(i_0_184,plain,
! [X280,X281] :
( ~ isa(X280,X281)
| collection(X281) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just107])]) ).
fof(i_0_185,plain,
! [X266,X267] :
( ~ disjointwith(X266,X267)
| collection(X267) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just99])]) ).
fof(i_0_186,plain,
! [X297,X298] :
( ~ genls(X297,X298)
| collection(X298) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just118])]) ).
fof(i_0_187,plain,
! [X295,X296] :
( ~ genls(X295,X296)
| collection(X296) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just117])]) ).
fof(i_0_188,plain,
! [X258] :
( ~ isa(X258,c_tptpcol_16_62187)
| tptpcol_16_62187(X258) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just91])]) ).
fof(i_0_189,plain,
! [X228] :
( ~ isa(X228,c_tptpcol_15_109185)
| tptpcol_15_109185(X228) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just61])]) ).
fof(i_0_190,plain,
! [X230] :
( ~ isa(X230,c_tptpcol_14_109181)
| tptpcol_14_109181(X230) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just63])]) ).
fof(i_0_191,plain,
! [X232] :
( ~ isa(X232,c_tptpcol_13_109173)
| tptpcol_13_109173(X232) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just65])]) ).
fof(i_0_192,plain,
! [X234] :
( ~ isa(X234,c_tptpcol_12_109157)
| tptpcol_12_109157(X234) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just67])]) ).
fof(i_0_193,plain,
! [X236] :
( ~ isa(X236,c_tptpcol_11_109125)
| tptpcol_11_109125(X236) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just69])]) ).
fof(i_0_194,plain,
! [X238] :
( ~ isa(X238,c_tptpcol_10_109061)
| tptpcol_10_109061(X238) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just71])]) ).
fof(i_0_195,plain,
! [X240] :
( ~ isa(X240,c_tptpcol_9_109060)
| tptpcol_9_109060(X240) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just73])]) ).
fof(i_0_196,plain,
! [X242] :
( ~ isa(X242,c_tptpcol_8_109059)
| tptpcol_8_109059(X242) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just75])]) ).
fof(i_0_197,plain,
! [X244] :
( ~ isa(X244,c_tptpcol_7_108547)
| tptpcol_7_108547(X244) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just77])]) ).
fof(i_0_198,plain,
! [X246] :
( ~ isa(X246,c_tptpcol_6_108546)
| tptpcol_6_108546(X246) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just79])]) ).
fof(i_0_199,plain,
! [X248] :
( ~ isa(X248,c_tptpcol_5_106498)
| tptpcol_5_106498(X248) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just81])]) ).
fof(i_0_200,plain,
! [X250] :
( ~ isa(X250,c_tptpcol_4_106497)
| tptpcol_4_106497(X250) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just83])]) ).
fof(i_0_201,plain,
! [X252] :
( ~ isa(X252,c_tptpcol_3_98305)
| tptpcol_3_98305(X252) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just85])]) ).
fof(i_0_202,plain,
! [X254] :
( ~ isa(X254,c_tptpcol_2_98304)
| tptpcol_2_98304(X254) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just87])]) ).
fof(i_0_203,plain,
! [X256] :
( ~ isa(X256,c_tptpcol_1_65536)
| tptpcol_1_65536(X256) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just89])]) ).
fof(i_0_204,plain,
! [X260] :
( ~ isa(X260,c_tptpcol_0_0)
| tptpcol_0_0(X260) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just93])]) ).
fof(i_0_205,plain,
! [X262] :
( ~ isa(X262,c_individual)
| individual(X262) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just95])]) ).
fof(i_0_206,plain,
! [X264] :
( ~ isa(X264,c_collection)
| collection(X264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just97])]) ).
fof(i_0_207,plain,
! [X278] :
( ~ isa(X278,c_transitivebinarypredicate)
| transitivebinarypredicate(X278) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just105])]) ).
fof(i_0_208,plain,
! [X291] :
( ~ isa(X291,c_fixedordercollection)
| fixedordercollection(X291) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just113])]) ).
fof(i_0_209,plain,
! [X293] :
( ~ isa(X293,c_firstordercollection)
| firstordercollection(X293) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just115])]) ).
fof(i_0_210,plain,
! [X217] :
( ~ predicate(X217)
| genlpreds(X217,X217) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just56])]) ).
fof(i_0_211,plain,
! [X216] :
( ~ predicate(X216)
| genlpreds(X216,X216) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just55])]) ).
fof(i_0_212,plain,
! [X307] :
( ~ collection(X307)
| genls(X307,X307) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just123])]) ).
fof(i_0_213,plain,
! [X306] :
( ~ collection(X306)
| genls(X306,X306) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just122])]) ).
fof(i_0_214,plain,
! [X342] :
( ~ microtheory(X342)
| genlmt(X342,X342) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just144])]) ).
fof(i_0_215,plain,
! [X341] :
( ~ microtheory(X341)
| genlmt(X341,X341) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just143])]) ).
fof(i_0_216,plain,
! [X279] :
( ~ transitivebinarypredicate(X279)
| isa(X279,c_transitivebinarypredicate) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just106])]) ).
fof(i_0_217,plain,
! [X229] :
( ~ tptpcol_15_109185(X229)
| isa(X229,c_tptpcol_15_109185) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just62])]) ).
fof(i_0_218,plain,
! [X231] :
( ~ tptpcol_14_109181(X231)
| isa(X231,c_tptpcol_14_109181) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just64])]) ).
fof(i_0_219,plain,
! [X233] :
( ~ tptpcol_13_109173(X233)
| isa(X233,c_tptpcol_13_109173) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just66])]) ).
fof(i_0_220,plain,
! [X235] :
( ~ tptpcol_12_109157(X235)
| isa(X235,c_tptpcol_12_109157) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just68])]) ).
fof(i_0_221,plain,
! [X237] :
( ~ tptpcol_11_109125(X237)
| isa(X237,c_tptpcol_11_109125) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just70])]) ).
fof(i_0_222,plain,
! [X239] :
( ~ tptpcol_10_109061(X239)
| isa(X239,c_tptpcol_10_109061) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just72])]) ).
fof(i_0_223,plain,
! [X241] :
( ~ tptpcol_9_109060(X241)
| isa(X241,c_tptpcol_9_109060) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just74])]) ).
fof(i_0_224,plain,
! [X243] :
( ~ tptpcol_8_109059(X243)
| isa(X243,c_tptpcol_8_109059) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just76])]) ).
fof(i_0_225,plain,
! [X245] :
( ~ tptpcol_7_108547(X245)
| isa(X245,c_tptpcol_7_108547) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just78])]) ).
fof(i_0_226,plain,
! [X247] :
( ~ tptpcol_6_108546(X247)
| isa(X247,c_tptpcol_6_108546) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just80])]) ).
fof(i_0_227,plain,
! [X249] :
( ~ tptpcol_5_106498(X249)
| isa(X249,c_tptpcol_5_106498) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just82])]) ).
fof(i_0_228,plain,
! [X251] :
( ~ tptpcol_4_106497(X251)
| isa(X251,c_tptpcol_4_106497) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just84])]) ).
fof(i_0_229,plain,
! [X253] :
( ~ tptpcol_3_98305(X253)
| isa(X253,c_tptpcol_3_98305) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just86])]) ).
fof(i_0_230,plain,
! [X255] :
( ~ tptpcol_2_98304(X255)
| isa(X255,c_tptpcol_2_98304) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just88])]) ).
fof(i_0_231,plain,
! [X257] :
( ~ tptpcol_1_65536(X257)
| isa(X257,c_tptpcol_1_65536) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just90])]) ).
fof(i_0_232,plain,
! [X259] :
( ~ tptpcol_16_62187(X259)
| isa(X259,c_tptpcol_16_62187) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just92])]) ).
fof(i_0_233,plain,
! [X261] :
( ~ tptpcol_0_0(X261)
| isa(X261,c_tptpcol_0_0) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just94])]) ).
fof(i_0_234,plain,
! [X263] :
( ~ individual(X263)
| isa(X263,c_individual) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just96])]) ).
fof(i_0_235,plain,
! [X265] :
( ~ collection(X265)
| isa(X265,c_collection) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just98])]) ).
fof(i_0_236,plain,
! [X292] :
( ~ fixedordercollection(X292)
| isa(X292,c_fixedordercollection) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just114])]) ).
fof(i_0_237,plain,
! [X294] :
( ~ firstordercollection(X294)
| isa(X294,c_firstordercollection) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just116])]) ).
fof(i_0_238,plain,
! [X317] : natfunction(f_urlreferentfn(X317),c_urlreferentfn),
inference(variable_rename,[status(thm)],[just130]) ).
fof(i_0_239,plain,
! [X314] : natfunction(f_urlfn(X314),c_urlfn),
inference(variable_rename,[status(thm)],[just127]) ).
fof(i_0_240,plain,
! [X181] :
( ~ collection(X181)
| ~ individual(X181) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just9])]) ).
fof(i_0_241,plain,
! [X198] :
( ~ tptpcol_15_109185(X198)
| tptpcol_14_109181(X198) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just47])]) ).
fof(i_0_242,plain,
! [X197] :
( ~ tptpcol_14_109181(X197)
| tptpcol_13_109173(X197) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just45])]) ).
fof(i_0_243,plain,
! [X196] :
( ~ tptpcol_13_109173(X196)
| tptpcol_12_109157(X196) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just43])]) ).
fof(i_0_244,plain,
! [X195] :
( ~ tptpcol_12_109157(X195)
| tptpcol_11_109125(X195) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just41])]) ).
fof(i_0_245,plain,
! [X194] :
( ~ tptpcol_11_109125(X194)
| tptpcol_10_109061(X194) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just39])]) ).
fof(i_0_246,plain,
! [X193] :
( ~ tptpcol_10_109061(X193)
| tptpcol_9_109060(X193) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just37])]) ).
fof(i_0_247,plain,
! [X192] :
( ~ tptpcol_9_109060(X192)
| tptpcol_8_109059(X192) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just35])]) ).
fof(i_0_248,plain,
! [X191] :
( ~ tptpcol_8_109059(X191)
| tptpcol_7_108547(X191) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just33])]) ).
fof(i_0_249,plain,
! [X190] :
( ~ tptpcol_7_108547(X190)
| tptpcol_6_108546(X190) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just31])]) ).
fof(i_0_250,plain,
! [X189] :
( ~ tptpcol_6_108546(X189)
| tptpcol_5_106498(X189) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just29])]) ).
fof(i_0_251,plain,
! [X188] :
( ~ tptpcol_5_106498(X188)
| tptpcol_4_106497(X188) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just27])]) ).
fof(i_0_252,plain,
! [X187] :
( ~ tptpcol_4_106497(X187)
| tptpcol_3_98305(X187) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just25])]) ).
fof(i_0_253,plain,
! [X186] :
( ~ tptpcol_3_98305(X186)
| tptpcol_2_98304(X186) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just23])]) ).
fof(i_0_254,plain,
! [X185] :
( ~ tptpcol_2_98304(X185)
| tptpcol_1_65536(X185) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just21])]) ).
fof(i_0_255,plain,
! [X184] :
( ~ tptpcol_1_65536(X184)
| tptpcol_0_0(X184) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just19])]) ).
fof(i_0_256,plain,
! [X183] :
( ~ tptpcol_0_0(X183)
| individual(X183) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just16])]) ).
fof(i_0_257,plain,
! [X182] :
( ~ fixedordercollection(X182)
| collection(X182) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just14])]) ).
fof(i_0_258,plain,
! [X180] :
( ~ firstordercollection(X180)
| fixedordercollection(X180) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just4])]) ).
fof(i_0_259,plain,
! [X319] : computerdataartifact(f_urlreferentfn(X319)),
inference(variable_rename,[status(thm)],[just132]) ).
fof(i_0_260,plain,
! [X316] : uniformresourcelocator(f_urlfn(X316)),
inference(variable_rename,[status(thm)],[just129]) ).
cnf(i_0_261,plain,
natargument(f_contentmtofcdafromeventfn(X1,X2),n_2,X2),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_262,plain,
natargument(f_contentmtofcdafromeventfn(X1,X2),n_1,X1),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_263,plain,
( ~ isa(X1,X2)
| ~ isa(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_264,plain,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14),c_machinelearningspindleheadmt),
inference(split_conjunct,[status(thm)],[just1]),
[final] ).
cnf(i_0_265,plain,
( genlpreds(X1,X3)
| ~ genlpreds(X1,X2)
| ~ genlpreds(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_266,plain,
( genlpreds(X1,X3)
| ~ genlinverse(X1,X2)
| ~ genlinverse(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_267,plain,
( genlinverse(X1,X3)
| ~ genlinverse(X1,X2)
| ~ genlpreds(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_268,plain,
( genlinverse(X3,X2)
| ~ genlinverse(X1,X2)
| ~ genlpreds(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_269,plain,
( isa(X1,X3)
| ~ isa(X1,X2)
| ~ genls(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_154]),
[final] ).
cnf(i_0_270,plain,
( disjointwith(X1,X3)
| ~ disjointwith(X1,X2)
| ~ genls(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_271,plain,
( disjointwith(X3,X2)
| ~ disjointwith(X1,X2)
| ~ genls(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_272,plain,
( genls(X1,X3)
| ~ genls(X1,X2)
| ~ genls(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_273,plain,
( genls(X1,X3)
| ~ genls(X1,X2)
| ~ genls(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_274,plain,
( genls(X3,X2)
| ~ genls(X1,X2)
| ~ genls(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_275,plain,
( genlmt(X1,X3)
| ~ genlmt(X1,X2)
| ~ genlmt(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_276,plain,
natargument(f_urlreferentfn(X1),n_1,X1),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_277,plain,
natargument(f_urlfn(X1),n_1,X1),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_278,negated_conjecture,
mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_279,plain,
natfunction(f_contentmtofcdafromeventfn(X1,X2),c_contentmtofcdafromeventfn),
inference(split_conjunct,[status(thm)],[i_0_164]),
[final] ).
cnf(i_0_280,plain,
( disjointwith(X2,X1)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_281,plain,
( mtvisible(X2)
| ~ mtvisible(X1)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_282,plain,
microtheory(f_contentmtofcdafromeventfn(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_283,plain,
( microtheory(X1)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_284,plain,
( microtheory(X1)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_169]),
[final] ).
cnf(i_0_285,plain,
( microtheory(X2)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_286,plain,
( microtheory(X2)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_171]),
[final] ).
cnf(i_0_287,plain,
( thing(X1)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_172]),
[final] ).
cnf(i_0_288,plain,
( thing(X1)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_173]),
[final] ).
cnf(i_0_289,plain,
( binarypredicate(X1)
| ~ genlinverse(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_174]),
[final] ).
cnf(i_0_290,plain,
( binarypredicate(X2)
| ~ genlinverse(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_291,plain,
( predicate(X1)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_292,plain,
( predicate(X1)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_293,plain,
( predicate(X2)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_294,plain,
( predicate(X2)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_295,plain,
( collection(X1)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_296,plain,
( collection(X1)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_297,plain,
( collection(X1)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_298,plain,
( collection(X2)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_299,plain,
( collection(X2)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_300,plain,
( collection(X2)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_185]),
[final] ).
cnf(i_0_301,plain,
( collection(X2)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_186]),
[final] ).
cnf(i_0_302,plain,
( collection(X2)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_187]),
[final] ).
cnf(i_0_303,plain,
( tptpcol_16_62187(X1)
| ~ isa(X1,c_tptpcol_16_62187) ),
inference(split_conjunct,[status(thm)],[i_0_188]),
[final] ).
cnf(i_0_304,plain,
( tptpcol_15_109185(X1)
| ~ isa(X1,c_tptpcol_15_109185) ),
inference(split_conjunct,[status(thm)],[i_0_189]),
[final] ).
cnf(i_0_305,plain,
( tptpcol_14_109181(X1)
| ~ isa(X1,c_tptpcol_14_109181) ),
inference(split_conjunct,[status(thm)],[i_0_190]),
[final] ).
cnf(i_0_306,plain,
( tptpcol_13_109173(X1)
| ~ isa(X1,c_tptpcol_13_109173) ),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_307,plain,
( tptpcol_12_109157(X1)
| ~ isa(X1,c_tptpcol_12_109157) ),
inference(split_conjunct,[status(thm)],[i_0_192]),
[final] ).
cnf(i_0_308,plain,
( tptpcol_11_109125(X1)
| ~ isa(X1,c_tptpcol_11_109125) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_309,plain,
( tptpcol_10_109061(X1)
| ~ isa(X1,c_tptpcol_10_109061) ),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_310,plain,
( tptpcol_9_109060(X1)
| ~ isa(X1,c_tptpcol_9_109060) ),
inference(split_conjunct,[status(thm)],[i_0_195]),
[final] ).
cnf(i_0_311,plain,
( tptpcol_8_109059(X1)
| ~ isa(X1,c_tptpcol_8_109059) ),
inference(split_conjunct,[status(thm)],[i_0_196]),
[final] ).
cnf(i_0_312,plain,
( tptpcol_7_108547(X1)
| ~ isa(X1,c_tptpcol_7_108547) ),
inference(split_conjunct,[status(thm)],[i_0_197]),
[final] ).
cnf(i_0_313,plain,
( tptpcol_6_108546(X1)
| ~ isa(X1,c_tptpcol_6_108546) ),
inference(split_conjunct,[status(thm)],[i_0_198]),
[final] ).
cnf(i_0_314,plain,
( tptpcol_5_106498(X1)
| ~ isa(X1,c_tptpcol_5_106498) ),
inference(split_conjunct,[status(thm)],[i_0_199]),
[final] ).
cnf(i_0_315,plain,
( tptpcol_4_106497(X1)
| ~ isa(X1,c_tptpcol_4_106497) ),
inference(split_conjunct,[status(thm)],[i_0_200]),
[final] ).
cnf(i_0_316,plain,
( tptpcol_3_98305(X1)
| ~ isa(X1,c_tptpcol_3_98305) ),
inference(split_conjunct,[status(thm)],[i_0_201]),
[final] ).
cnf(i_0_317,plain,
( tptpcol_2_98304(X1)
| ~ isa(X1,c_tptpcol_2_98304) ),
inference(split_conjunct,[status(thm)],[i_0_202]),
[final] ).
cnf(i_0_318,plain,
( tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(split_conjunct,[status(thm)],[i_0_203]),
[final] ).
cnf(i_0_319,plain,
( tptpcol_0_0(X1)
| ~ isa(X1,c_tptpcol_0_0) ),
inference(split_conjunct,[status(thm)],[i_0_204]),
[final] ).
cnf(i_0_320,plain,
( individual(X1)
| ~ isa(X1,c_individual) ),
inference(split_conjunct,[status(thm)],[i_0_205]),
[final] ).
cnf(i_0_321,plain,
( collection(X1)
| ~ isa(X1,c_collection) ),
inference(split_conjunct,[status(thm)],[i_0_206]),
[final] ).
cnf(i_0_322,plain,
( transitivebinarypredicate(X1)
| ~ isa(X1,c_transitivebinarypredicate) ),
inference(split_conjunct,[status(thm)],[i_0_207]),
[final] ).
cnf(i_0_323,plain,
( fixedordercollection(X1)
| ~ isa(X1,c_fixedordercollection) ),
inference(split_conjunct,[status(thm)],[i_0_208]),
[final] ).
cnf(i_0_324,plain,
( firstordercollection(X1)
| ~ isa(X1,c_firstordercollection) ),
inference(split_conjunct,[status(thm)],[i_0_209]),
[final] ).
cnf(i_0_325,plain,
( genlpreds(X1,X1)
| ~ predicate(X1) ),
inference(split_conjunct,[status(thm)],[i_0_210]),
[final] ).
cnf(i_0_326,plain,
( genlpreds(X1,X1)
| ~ predicate(X1) ),
inference(split_conjunct,[status(thm)],[i_0_211]),
[final] ).
cnf(i_0_327,plain,
( genls(X1,X1)
| ~ collection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_212]),
[final] ).
cnf(i_0_328,plain,
( genls(X1,X1)
| ~ collection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_213]),
[final] ).
cnf(i_0_329,plain,
( genlmt(X1,X1)
| ~ microtheory(X1) ),
inference(split_conjunct,[status(thm)],[i_0_214]),
[final] ).
cnf(i_0_330,plain,
( genlmt(X1,X1)
| ~ microtheory(X1) ),
inference(split_conjunct,[status(thm)],[i_0_215]),
[final] ).
cnf(i_0_331,plain,
( isa(X1,c_transitivebinarypredicate)
| ~ transitivebinarypredicate(X1) ),
inference(split_conjunct,[status(thm)],[i_0_216]),
[final] ).
cnf(i_0_332,plain,
( isa(X1,c_tptpcol_15_109185)
| ~ tptpcol_15_109185(X1) ),
inference(split_conjunct,[status(thm)],[i_0_217]),
[final] ).
cnf(i_0_333,plain,
( isa(X1,c_tptpcol_14_109181)
| ~ tptpcol_14_109181(X1) ),
inference(split_conjunct,[status(thm)],[i_0_218]),
[final] ).
cnf(i_0_334,plain,
( isa(X1,c_tptpcol_13_109173)
| ~ tptpcol_13_109173(X1) ),
inference(split_conjunct,[status(thm)],[i_0_219]),
[final] ).
cnf(i_0_335,plain,
( isa(X1,c_tptpcol_12_109157)
| ~ tptpcol_12_109157(X1) ),
inference(split_conjunct,[status(thm)],[i_0_220]),
[final] ).
cnf(i_0_336,plain,
( isa(X1,c_tptpcol_11_109125)
| ~ tptpcol_11_109125(X1) ),
inference(split_conjunct,[status(thm)],[i_0_221]),
[final] ).
cnf(i_0_337,plain,
( isa(X1,c_tptpcol_10_109061)
| ~ tptpcol_10_109061(X1) ),
inference(split_conjunct,[status(thm)],[i_0_222]),
[final] ).
cnf(i_0_338,plain,
( isa(X1,c_tptpcol_9_109060)
| ~ tptpcol_9_109060(X1) ),
inference(split_conjunct,[status(thm)],[i_0_223]),
[final] ).
cnf(i_0_339,plain,
( isa(X1,c_tptpcol_8_109059)
| ~ tptpcol_8_109059(X1) ),
inference(split_conjunct,[status(thm)],[i_0_224]),
[final] ).
cnf(i_0_340,plain,
( isa(X1,c_tptpcol_7_108547)
| ~ tptpcol_7_108547(X1) ),
inference(split_conjunct,[status(thm)],[i_0_225]),
[final] ).
cnf(i_0_341,plain,
( isa(X1,c_tptpcol_6_108546)
| ~ tptpcol_6_108546(X1) ),
inference(split_conjunct,[status(thm)],[i_0_226]),
[final] ).
cnf(i_0_342,plain,
( isa(X1,c_tptpcol_5_106498)
| ~ tptpcol_5_106498(X1) ),
inference(split_conjunct,[status(thm)],[i_0_227]),
[final] ).
cnf(i_0_343,plain,
( isa(X1,c_tptpcol_4_106497)
| ~ tptpcol_4_106497(X1) ),
inference(split_conjunct,[status(thm)],[i_0_228]),
[final] ).
cnf(i_0_344,plain,
( isa(X1,c_tptpcol_3_98305)
| ~ tptpcol_3_98305(X1) ),
inference(split_conjunct,[status(thm)],[i_0_229]),
[final] ).
cnf(i_0_345,plain,
( isa(X1,c_tptpcol_2_98304)
| ~ tptpcol_2_98304(X1) ),
inference(split_conjunct,[status(thm)],[i_0_230]),
[final] ).
cnf(i_0_346,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(split_conjunct,[status(thm)],[i_0_231]),
[final] ).
cnf(i_0_347,plain,
( isa(X1,c_tptpcol_16_62187)
| ~ tptpcol_16_62187(X1) ),
inference(split_conjunct,[status(thm)],[i_0_232]),
[final] ).
cnf(i_0_348,plain,
( isa(X1,c_tptpcol_0_0)
| ~ tptpcol_0_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_233]),
[final] ).
cnf(i_0_349,plain,
( isa(X1,c_individual)
| ~ individual(X1) ),
inference(split_conjunct,[status(thm)],[i_0_234]),
[final] ).
cnf(i_0_350,plain,
( isa(X1,c_collection)
| ~ collection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_235]),
[final] ).
cnf(i_0_351,plain,
( isa(X1,c_fixedordercollection)
| ~ fixedordercollection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_236]),
[final] ).
cnf(i_0_352,plain,
( isa(X1,c_firstordercollection)
| ~ firstordercollection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_237]),
[final] ).
cnf(i_0_353,plain,
natfunction(f_urlreferentfn(X1),c_urlreferentfn),
inference(split_conjunct,[status(thm)],[i_0_238]),
[final] ).
cnf(i_0_354,plain,
natfunction(f_urlfn(X1),c_urlfn),
inference(split_conjunct,[status(thm)],[i_0_239]),
[final] ).
cnf(i_0_355,plain,
( ~ collection(X1)
| ~ individual(X1) ),
inference(split_conjunct,[status(thm)],[i_0_240]),
[final] ).
cnf(i_0_356,plain,
( tptpcol_14_109181(X1)
| ~ tptpcol_15_109185(X1) ),
inference(split_conjunct,[status(thm)],[i_0_241]),
[final] ).
cnf(i_0_357,plain,
( tptpcol_13_109173(X1)
| ~ tptpcol_14_109181(X1) ),
inference(split_conjunct,[status(thm)],[i_0_242]),
[final] ).
cnf(i_0_358,plain,
( tptpcol_12_109157(X1)
| ~ tptpcol_13_109173(X1) ),
inference(split_conjunct,[status(thm)],[i_0_243]),
[final] ).
cnf(i_0_359,plain,
( tptpcol_11_109125(X1)
| ~ tptpcol_12_109157(X1) ),
inference(split_conjunct,[status(thm)],[i_0_244]),
[final] ).
cnf(i_0_360,plain,
( tptpcol_10_109061(X1)
| ~ tptpcol_11_109125(X1) ),
inference(split_conjunct,[status(thm)],[i_0_245]),
[final] ).
cnf(i_0_361,plain,
( tptpcol_9_109060(X1)
| ~ tptpcol_10_109061(X1) ),
inference(split_conjunct,[status(thm)],[i_0_246]),
[final] ).
cnf(i_0_362,plain,
( tptpcol_8_109059(X1)
| ~ tptpcol_9_109060(X1) ),
inference(split_conjunct,[status(thm)],[i_0_247]),
[final] ).
cnf(i_0_363,plain,
( tptpcol_7_108547(X1)
| ~ tptpcol_8_109059(X1) ),
inference(split_conjunct,[status(thm)],[i_0_248]),
[final] ).
cnf(i_0_364,plain,
( tptpcol_6_108546(X1)
| ~ tptpcol_7_108547(X1) ),
inference(split_conjunct,[status(thm)],[i_0_249]),
[final] ).
cnf(i_0_365,plain,
( tptpcol_5_106498(X1)
| ~ tptpcol_6_108546(X1) ),
inference(split_conjunct,[status(thm)],[i_0_250]),
[final] ).
cnf(i_0_366,plain,
( tptpcol_4_106497(X1)
| ~ tptpcol_5_106498(X1) ),
inference(split_conjunct,[status(thm)],[i_0_251]),
[final] ).
cnf(i_0_367,plain,
( tptpcol_3_98305(X1)
| ~ tptpcol_4_106497(X1) ),
inference(split_conjunct,[status(thm)],[i_0_252]),
[final] ).
cnf(i_0_368,plain,
( tptpcol_2_98304(X1)
| ~ tptpcol_3_98305(X1) ),
inference(split_conjunct,[status(thm)],[i_0_253]),
[final] ).
cnf(i_0_369,plain,
( tptpcol_1_65536(X1)
| ~ tptpcol_2_98304(X1) ),
inference(split_conjunct,[status(thm)],[i_0_254]),
[final] ).
cnf(i_0_370,plain,
( tptpcol_0_0(X1)
| ~ tptpcol_1_65536(X1) ),
inference(split_conjunct,[status(thm)],[i_0_255]),
[final] ).
cnf(i_0_371,plain,
( individual(X1)
| ~ tptpcol_0_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_256]),
[final] ).
cnf(i_0_372,plain,
( collection(X1)
| ~ fixedordercollection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_257]),
[final] ).
cnf(i_0_373,plain,
( fixedordercollection(X1)
| ~ firstordercollection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_258]),
[final] ).
cnf(i_0_374,plain,
disjointwith(c_collection,c_individual),
inference(split_conjunct,[status(thm)],[just10]),
[final] ).
cnf(i_0_375,plain,
genls(c_tptpcol_15_109185,c_tptpcol_14_109181),
inference(split_conjunct,[status(thm)],[just46]),
[final] ).
cnf(i_0_376,plain,
genls(c_tptpcol_14_109181,c_tptpcol_13_109173),
inference(split_conjunct,[status(thm)],[just44]),
[final] ).
cnf(i_0_377,plain,
genls(c_tptpcol_13_109173,c_tptpcol_12_109157),
inference(split_conjunct,[status(thm)],[just42]),
[final] ).
cnf(i_0_378,plain,
genls(c_tptpcol_12_109157,c_tptpcol_11_109125),
inference(split_conjunct,[status(thm)],[just40]),
[final] ).
cnf(i_0_379,plain,
genls(c_tptpcol_11_109125,c_tptpcol_10_109061),
inference(split_conjunct,[status(thm)],[just38]),
[final] ).
cnf(i_0_380,plain,
genls(c_tptpcol_10_109061,c_tptpcol_9_109060),
inference(split_conjunct,[status(thm)],[just36]),
[final] ).
cnf(i_0_381,plain,
genls(c_tptpcol_9_109060,c_tptpcol_8_109059),
inference(split_conjunct,[status(thm)],[just34]),
[final] ).
cnf(i_0_382,plain,
genls(c_tptpcol_8_109059,c_tptpcol_7_108547),
inference(split_conjunct,[status(thm)],[just32]),
[final] ).
cnf(i_0_383,plain,
genls(c_tptpcol_7_108547,c_tptpcol_6_108546),
inference(split_conjunct,[status(thm)],[just30]),
[final] ).
cnf(i_0_384,plain,
genls(c_tptpcol_6_108546,c_tptpcol_5_106498),
inference(split_conjunct,[status(thm)],[just28]),
[final] ).
cnf(i_0_385,plain,
genls(c_tptpcol_5_106498,c_tptpcol_4_106497),
inference(split_conjunct,[status(thm)],[just26]),
[final] ).
cnf(i_0_386,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(split_conjunct,[status(thm)],[just24]),
[final] ).
cnf(i_0_387,plain,
genls(c_tptpcol_3_98305,c_tptpcol_2_98304),
inference(split_conjunct,[status(thm)],[just22]),
[final] ).
cnf(i_0_388,plain,
genls(c_tptpcol_2_98304,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[just20]),
[final] ).
cnf(i_0_389,plain,
genls(c_tptpcol_1_65536,c_tptpcol_0_0),
inference(split_conjunct,[status(thm)],[just18]),
[final] ).
cnf(i_0_390,plain,
genls(c_tptpcol_0_0,c_individual),
inference(split_conjunct,[status(thm)],[just15]),
[final] ).
cnf(i_0_391,plain,
genls(c_fixedordercollection,c_collection),
inference(split_conjunct,[status(thm)],[just13]),
[final] ).
cnf(i_0_392,plain,
genls(c_firstordercollection,c_fixedordercollection),
inference(split_conjunct,[status(thm)],[just3]),
[final] ).
cnf(i_0_393,plain,
genlmt(c_corecyclmt,c_logicaltruthmt),
inference(split_conjunct,[status(thm)],[just8]),
[final] ).
cnf(i_0_394,plain,
genlmt(c_universalvocabularymt,c_corecyclmt),
inference(split_conjunct,[status(thm)],[just6]),
[final] ).
cnf(i_0_395,plain,
genlmt(c_cycnounlearnermt,c_cycorpproductsmt),
inference(split_conjunct,[status(thm)],[just5]),
[final] ).
cnf(i_0_396,plain,
genlmt(c_basekb,c_universalvocabularymt),
inference(split_conjunct,[status(thm)],[just12]),
[final] ).
cnf(i_0_397,plain,
genlmt(c_cycorpproductsmt,c_basekb),
inference(split_conjunct,[status(thm)],[just2]),
[final] ).
cnf(i_0_398,plain,
genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt),
inference(split_conjunct,[status(thm)],[just11]),
[final] ).
cnf(i_0_399,plain,
computerdataartifact(f_urlreferentfn(X1)),
inference(split_conjunct,[status(thm)],[i_0_259]),
[final] ).
cnf(i_0_400,plain,
uniformresourcelocator(f_urlfn(X1)),
inference(split_conjunct,[status(thm)],[i_0_260]),
[final] ).
cnf(i_0_401,plain,
mtvisible(c_logicaltruthmt),
inference(split_conjunct,[status(thm)],[just104]),
[final] ).
cnf(i_0_402,plain,
mtvisible(c_corecyclmt),
inference(split_conjunct,[status(thm)],[just112]),
[final] ).
cnf(i_0_403,plain,
mtvisible(c_universalvocabularymt),
inference(split_conjunct,[status(thm)],[just145]),
[final] ).
cnf(i_0_404,plain,
mtvisible(c_basekb),
inference(split_conjunct,[status(thm)],[just126]),
[final] ).
cnf(i_0_405,negated_conjecture,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_406,plain,
transitivebinarypredicate(c_genlmt),
inference(split_conjunct,[status(thm)],[just7]),
[final] ).
cnf(i_0_407,plain,
firstordercollection(c_tptpcol_16_62187),
inference(split_conjunct,[status(thm)],[just17]),
[final] ).
cnf(i_0_408,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_356]) ).
cnf(i_0_409,plain,
( ~ tptpcol_15_109185(X1)
| tptpcol_14_109181(X1) ),
inference(rename_variables,[],[i_0_356]) ).
cnf(i_0_410,plain,
genlmt(f_contentmtofcdafromeventfn(X1,X2),f_contentmtofcdafromeventfn(X1,X2)),
inference(scs_inference,[],[i_0_405,i_0_282,i_0_356,i_0_330]) ).
cnf(i_0_411,plain,
( ~ microtheory(X1)
| genlmt(X1,X1) ),
inference(rename_variables,[],[i_0_330]) ).
cnf(i_0_412,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_282,i_0_356,i_0_330,i_0_357]) ).
cnf(i_0_413,plain,
( ~ tptpcol_14_109181(X1)
| tptpcol_13_109173(X1) ),
inference(rename_variables,[],[i_0_357]) ).
cnf(i_0_414,plain,
disjointwith(c_individual,c_collection),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280]) ).
cnf(i_0_415,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_280]) ).
cnf(i_0_416,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358]) ).
cnf(i_0_417,plain,
( ~ tptpcol_13_109173(X1)
| tptpcol_12_109157(X1) ),
inference(rename_variables,[],[i_0_358]) ).
cnf(i_0_418,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359]) ).
cnf(i_0_419,plain,
( ~ tptpcol_12_109157(X1)
| tptpcol_11_109125(X1) ),
inference(rename_variables,[],[i_0_359]) ).
cnf(i_0_420,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360]) ).
cnf(i_0_421,plain,
( ~ tptpcol_11_109125(X1)
| tptpcol_10_109061(X1) ),
inference(rename_variables,[],[i_0_360]) ).
cnf(i_0_422,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361]) ).
cnf(i_0_423,plain,
( ~ tptpcol_10_109061(X1)
| tptpcol_9_109060(X1) ),
inference(rename_variables,[],[i_0_361]) ).
cnf(i_0_424,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362]) ).
cnf(i_0_425,plain,
( ~ tptpcol_9_109060(X1)
| tptpcol_8_109059(X1) ),
inference(rename_variables,[],[i_0_362]) ).
cnf(i_0_426,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363]) ).
cnf(i_0_427,plain,
( ~ tptpcol_8_109059(X1)
| tptpcol_7_108547(X1) ),
inference(rename_variables,[],[i_0_363]) ).
cnf(i_0_428,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364]) ).
cnf(i_0_429,plain,
( ~ tptpcol_7_108547(X1)
| tptpcol_6_108546(X1) ),
inference(rename_variables,[],[i_0_364]) ).
cnf(i_0_430,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365]) ).
cnf(i_0_431,plain,
( ~ tptpcol_6_108546(X1)
| tptpcol_5_106498(X1) ),
inference(rename_variables,[],[i_0_365]) ).
cnf(i_0_432,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366]) ).
cnf(i_0_433,plain,
( ~ tptpcol_5_106498(X1)
| tptpcol_4_106497(X1) ),
inference(rename_variables,[],[i_0_366]) ).
cnf(i_0_434,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367]) ).
cnf(i_0_435,plain,
( ~ tptpcol_4_106497(X1)
| tptpcol_3_98305(X1) ),
inference(rename_variables,[],[i_0_367]) ).
cnf(i_0_436,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368]) ).
cnf(i_0_437,plain,
( ~ tptpcol_3_98305(X1)
| tptpcol_2_98304(X1) ),
inference(rename_variables,[],[i_0_368]) ).
cnf(i_0_438,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369]) ).
cnf(i_0_439,plain,
( ~ tptpcol_2_98304(X1)
| tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_369]) ).
cnf(i_0_440,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370]) ).
cnf(i_0_441,plain,
( ~ tptpcol_1_65536(X1)
| tptpcol_0_0(X1) ),
inference(rename_variables,[],[i_0_370]) ).
cnf(i_0_442,plain,
individual(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371]) ).
cnf(i_0_443,plain,
( ~ tptpcol_0_0(X1)
| individual(X1) ),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_444,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_405,i_0_374,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373]) ).
cnf(i_0_445,plain,
( ~ firstordercollection(X1)
| fixedordercollection(X1) ),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_446,plain,
mtvisible(c_machinelearningspindleheadmt),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_264,i_0_374,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281]) ).
cnf(i_0_447,plain,
( ~ genlmt(X1,X2)
| mtvisible(X2)
| ~ mtvisible(X1) ),
inference(rename_variables,[],[i_0_281]) ).
cnf(i_0_448,plain,
genlmt(c_universalvocabularymt,c_logicaltruthmt),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275]) ).
cnf(i_0_449,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_275]) ).
cnf(i_0_450,plain,
disjointwith(c_collection,c_tptpcol_0_0),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270]) ).
cnf(i_0_451,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_270]) ).
cnf(i_0_452,plain,
disjointwith(c_tptpcol_0_0,c_collection),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271]) ).
cnf(i_0_453,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_454,plain,
genls(c_tptpcol_15_109185,c_tptpcol_13_109173),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274]) ).
cnf(i_0_455,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_274]) ).
cnf(i_0_456,plain,
~ collection(c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274,i_0_355]) ).
cnf(i_0_457,plain,
( ~ individual(X1)
| ~ collection(X1) ),
inference(rename_variables,[],[i_0_355]) ).
cnf(i_0_458,plain,
~ disjointwith(c_tptpcol_16_62187,X1),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274,i_0_355,i_0_295]) ).
cnf(i_0_459,plain,
( collection(X1)
| ~ disjointwith(X1,X2) ),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_460,plain,
~ genls(c_tptpcol_16_62187,X1),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274,i_0_355,i_0_295,i_0_297]) ).
cnf(i_0_461,plain,
( collection(X1)
| ~ genls(X1,X2) ),
inference(rename_variables,[],[i_0_297]) ).
cnf(i_0_462,plain,
~ disjointwith(X1,c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274,i_0_355,i_0_295,i_0_297,i_0_300]) ).
cnf(i_0_463,plain,
( collection(X1)
| ~ disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_300]) ).
cnf(i_0_464,plain,
~ genls(X1,c_tptpcol_16_62187),
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274,i_0_355,i_0_295,i_0_297,i_0_300,i_0_302]) ).
cnf(i_0_465,plain,
( collection(X1)
| ~ genls(X2,X1) ),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_466,plain,
$false,
inference(scs_inference,[],[i_0_278,i_0_405,i_0_393,i_0_394,i_0_264,i_0_374,i_0_375,i_0_376,i_0_390,i_0_282,i_0_407,i_0_356,i_0_330,i_0_357,i_0_280,i_0_358,i_0_359,i_0_360,i_0_361,i_0_362,i_0_363,i_0_364,i_0_365,i_0_366,i_0_367,i_0_368,i_0_369,i_0_370,i_0_371,i_0_373,i_0_281,i_0_275,i_0_270,i_0_271,i_0_274,i_0_355,i_0_295,i_0_297,i_0_300,i_0_302,i_0_372]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : CSR040+1 : TPTP v9.2.1. Released v3.4.0.
% 0.11/0.14 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.35 % Computer : n031.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Mon May 4 16:31:53 EDT 2026
% 0.15/0.36 % CPUTime :
% 0.15/0.37 % start to proof: theBenchmark
% 0.27/1.64 % Version : CSE_E---1.7
% 0.27/1.64 % Problem : theBenchmark.p
% 0.27/1.64 % SZS status Theorem for theBenchmark.p
% 0.27/1.64 % SZS output start CNFRefutation
% See solution above
% 0.55/1.90 % Total time : 1.271s
%------------------------------------------------------------------------------