%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CSR040+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n009.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 : 0s
% DateTime : Fri Jul 15 02:01:10 EDT 2022
% Result : Theorem 0.78s 1.17s
% Output : Refutation 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : CSR040+1 : TPTP v8.1.0. Released v3.4.0.
% 0.09/0.15 % Command : bliksem %s
% 0.14/0.37 % Computer : n009.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % DateTime : Sat Jun 11 14:54:23 EDT 2022
% 0.14/0.37 % CPUTime :
% 0.78/1.17 *** allocated 10000 integers for termspace/termends
% 0.78/1.17 *** allocated 10000 integers for clauses
% 0.78/1.17 *** allocated 10000 integers for justifications
% 0.78/1.17 Bliksem 1.12
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Automatic Strategy Selection
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Clauses:
% 0.78/1.17
% 0.78/1.17 { genlmt( f_contentmtofcdafromeventfn( f_urlreferentfn( f_urlfn(
% 0.78/1.17 s_http_wwwthedailybulletincompostcardsmar9chtm ) ), c_translation_14 ),
% 0.78/1.17 c_machinelearningspindleheadmt ) }.
% 0.78/1.17 { genlmt( c_cycorpproductsmt, c_basekb ) }.
% 0.78/1.17 { genls( c_firstordercollection, c_fixedordercollection ) }.
% 0.78/1.17 { ! firstordercollection( X ), fixedordercollection( X ) }.
% 0.78/1.17 { genlmt( c_cycnounlearnermt, c_cycorpproductsmt ) }.
% 0.78/1.17 { genlmt( c_universalvocabularymt, c_corecyclmt ) }.
% 0.78/1.17 { transitivebinarypredicate( c_genlmt ) }.
% 0.78/1.17 { genlmt( c_corecyclmt, c_logicaltruthmt ) }.
% 0.78/1.17 { ! collection( X ), ! individual( X ) }.
% 0.78/1.17 { disjointwith( c_collection, c_individual ) }.
% 0.78/1.17 { genlmt( c_machinelearningspindleheadmt, c_cycnounlearnermt ) }.
% 0.78/1.17 { genlmt( c_basekb, c_universalvocabularymt ) }.
% 0.78/1.17 { genls( c_fixedordercollection, c_collection ) }.
% 0.78/1.17 { ! fixedordercollection( X ), collection( X ) }.
% 0.78/1.17 { genls( c_tptpcol_0_0, c_individual ) }.
% 0.78/1.17 { ! tptpcol_0_0( X ), individual( X ) }.
% 0.78/1.17 { firstordercollection( c_tptpcol_16_62187 ) }.
% 0.78/1.17 { genls( c_tptpcol_1_65536, c_tptpcol_0_0 ) }.
% 0.78/1.17 { ! tptpcol_1_65536( X ), tptpcol_0_0( X ) }.
% 0.78/1.17 { genls( c_tptpcol_2_98304, c_tptpcol_1_65536 ) }.
% 0.78/1.17 { ! tptpcol_2_98304( X ), tptpcol_1_65536( X ) }.
% 0.78/1.17 { genls( c_tptpcol_3_98305, c_tptpcol_2_98304 ) }.
% 0.78/1.17 { ! tptpcol_3_98305( X ), tptpcol_2_98304( X ) }.
% 0.78/1.17 { genls( c_tptpcol_4_106497, c_tptpcol_3_98305 ) }.
% 0.78/1.17 { ! tptpcol_4_106497( X ), tptpcol_3_98305( X ) }.
% 0.78/1.17 { genls( c_tptpcol_5_106498, c_tptpcol_4_106497 ) }.
% 0.78/1.17 { ! tptpcol_5_106498( X ), tptpcol_4_106497( X ) }.
% 0.78/1.17 { genls( c_tptpcol_6_108546, c_tptpcol_5_106498 ) }.
% 0.78/1.17 { ! tptpcol_6_108546( X ), tptpcol_5_106498( X ) }.
% 0.78/1.17 { genls( c_tptpcol_7_108547, c_tptpcol_6_108546 ) }.
% 0.78/1.17 { ! tptpcol_7_108547( X ), tptpcol_6_108546( X ) }.
% 0.78/1.17 { genls( c_tptpcol_8_109059, c_tptpcol_7_108547 ) }.
% 0.78/1.17 { ! tptpcol_8_109059( X ), tptpcol_7_108547( X ) }.
% 0.78/1.17 { genls( c_tptpcol_9_109060, c_tptpcol_8_109059 ) }.
% 0.78/1.17 { ! tptpcol_9_109060( X ), tptpcol_8_109059( X ) }.
% 0.78/1.17 { genls( c_tptpcol_10_109061, c_tptpcol_9_109060 ) }.
% 0.78/1.17 { ! tptpcol_10_109061( X ), tptpcol_9_109060( X ) }.
% 0.78/1.17 { genls( c_tptpcol_11_109125, c_tptpcol_10_109061 ) }.
% 0.78/1.17 { ! tptpcol_11_109125( X ), tptpcol_10_109061( X ) }.
% 0.78/1.17 { genls( c_tptpcol_12_109157, c_tptpcol_11_109125 ) }.
% 0.78/1.17 { ! tptpcol_12_109157( X ), tptpcol_11_109125( X ) }.
% 0.78/1.17 { genls( c_tptpcol_13_109173, c_tptpcol_12_109157 ) }.
% 0.78/1.17 { ! tptpcol_13_109173( X ), tptpcol_12_109157( X ) }.
% 0.78/1.17 { genls( c_tptpcol_14_109181, c_tptpcol_13_109173 ) }.
% 0.78/1.17 { ! tptpcol_14_109181( X ), tptpcol_13_109173( X ) }.
% 0.78/1.17 { genls( c_tptpcol_15_109185, c_tptpcol_14_109181 ) }.
% 0.78/1.17 { ! tptpcol_15_109185( X ), tptpcol_14_109181( X ) }.
% 0.78/1.17 { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith( Y, Z ) }.
% 0.78/1.17 { ! genlinverse( X, Z ), ! genlinverse( Z, Y ), genlpreds( X, Y ) }.
% 0.78/1.17 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.78/1.17 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.78/1.17 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.78/1.17 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.78/1.17 { ! genlpreds( X, Z ), ! genlpreds( Z, Y ), genlpreds( X, Y ) }.
% 0.78/1.17 { ! predicate( X ), genlpreds( X, X ) }.
% 0.78/1.17 { ! predicate( X ), genlpreds( X, X ) }.
% 0.78/1.17 { ! genlinverse( Y, X ), binarypredicate( X ) }.
% 0.78/1.17 { ! genlinverse( X, Y ), binarypredicate( X ) }.
% 0.78/1.17 { ! genlinverse( Z, X ), ! genlpreds( Y, Z ), genlinverse( Y, X ) }.
% 0.78/1.17 { ! genlinverse( X, Z ), ! genlpreds( Z, Y ), genlinverse( X, Y ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_15_109185 ), tptpcol_15_109185( X ) }.
% 0.78/1.17 { ! tptpcol_15_109185( X ), isa( X, c_tptpcol_15_109185 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_14_109181 ), tptpcol_14_109181( X ) }.
% 0.78/1.17 { ! tptpcol_14_109181( X ), isa( X, c_tptpcol_14_109181 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_13_109173 ), tptpcol_13_109173( X ) }.
% 0.78/1.17 { ! tptpcol_13_109173( X ), isa( X, c_tptpcol_13_109173 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_12_109157 ), tptpcol_12_109157( X ) }.
% 0.78/1.17 { ! tptpcol_12_109157( X ), isa( X, c_tptpcol_12_109157 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_11_109125 ), tptpcol_11_109125( X ) }.
% 0.78/1.17 { ! tptpcol_11_109125( X ), isa( X, c_tptpcol_11_109125 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_10_109061 ), tptpcol_10_109061( X ) }.
% 0.78/1.17 { ! tptpcol_10_109061( X ), isa( X, c_tptpcol_10_109061 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_9_109060 ), tptpcol_9_109060( X ) }.
% 0.78/1.17 { ! tptpcol_9_109060( X ), isa( X, c_tptpcol_9_109060 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_8_109059 ), tptpcol_8_109059( X ) }.
% 0.78/1.17 { ! tptpcol_8_109059( X ), isa( X, c_tptpcol_8_109059 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_7_108547 ), tptpcol_7_108547( X ) }.
% 0.78/1.17 { ! tptpcol_7_108547( X ), isa( X, c_tptpcol_7_108547 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_6_108546 ), tptpcol_6_108546( X ) }.
% 0.78/1.17 { ! tptpcol_6_108546( X ), isa( X, c_tptpcol_6_108546 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_5_106498 ), tptpcol_5_106498( X ) }.
% 0.78/1.17 { ! tptpcol_5_106498( X ), isa( X, c_tptpcol_5_106498 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_4_106497 ), tptpcol_4_106497( X ) }.
% 0.78/1.17 { ! tptpcol_4_106497( X ), isa( X, c_tptpcol_4_106497 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_3_98305 ), tptpcol_3_98305( X ) }.
% 0.78/1.17 { ! tptpcol_3_98305( X ), isa( X, c_tptpcol_3_98305 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_2_98304 ), tptpcol_2_98304( X ) }.
% 0.78/1.17 { ! tptpcol_2_98304( X ), isa( X, c_tptpcol_2_98304 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_1_65536 ), tptpcol_1_65536( X ) }.
% 0.78/1.17 { ! tptpcol_1_65536( X ), isa( X, c_tptpcol_1_65536 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_16_62187 ), tptpcol_16_62187( X ) }.
% 0.78/1.17 { ! tptpcol_16_62187( X ), isa( X, c_tptpcol_16_62187 ) }.
% 0.78/1.17 { ! isa( X, c_tptpcol_0_0 ), tptpcol_0_0( X ) }.
% 0.78/1.17 { ! tptpcol_0_0( X ), isa( X, c_tptpcol_0_0 ) }.
% 0.78/1.17 { ! isa( X, c_individual ), individual( X ) }.
% 0.78/1.17 { ! individual( X ), isa( X, c_individual ) }.
% 0.78/1.17 { ! isa( X, c_collection ), collection( X ) }.
% 0.78/1.17 { ! collection( X ), isa( X, c_collection ) }.
% 0.78/1.17 { ! disjointwith( Y, X ), collection( X ) }.
% 0.78/1.17 { ! disjointwith( X, Y ), collection( X ) }.
% 0.78/1.17 { ! disjointwith( X, Y ), disjointwith( Y, X ) }.
% 0.78/1.17 { ! disjointwith( X, Z ), ! genls( Y, Z ), disjointwith( X, Y ) }.
% 0.78/1.17 { ! disjointwith( Z, X ), ! genls( Y, Z ), disjointwith( Y, X ) }.
% 0.78/1.17 { mtvisible( c_logicaltruthmt ) }.
% 0.78/1.17 { ! isa( X, c_transitivebinarypredicate ), transitivebinarypredicate( X ) }
% 0.78/1.17 .
% 0.78/1.17 { ! transitivebinarypredicate( X ), isa( X, c_transitivebinarypredicate ) }
% 0.78/1.17 .
% 0.78/1.17 { ! isa( Y, X ), collection( X ) }.
% 0.78/1.17 { ! isa( Y, X ), collection( X ) }.
% 0.78/1.17 { ! isa( X, Y ), thing( X ) }.
% 0.78/1.17 { ! isa( X, Y ), thing( X ) }.
% 0.78/1.17 { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y ) }.
% 0.78/1.17 { mtvisible( c_corecyclmt ) }.
% 0.78/1.17 { ! isa( X, c_fixedordercollection ), fixedordercollection( X ) }.
% 0.78/1.17 { ! fixedordercollection( X ), isa( X, c_fixedordercollection ) }.
% 0.78/1.17 { ! isa( X, c_firstordercollection ), firstordercollection( X ) }.
% 0.78/1.17 { ! firstordercollection( X ), isa( X, c_firstordercollection ) }.
% 0.78/1.17 { ! genls( Y, X ), collection( X ) }.
% 0.78/1.17 { ! genls( Y, X ), collection( X ) }.
% 0.78/1.17 { ! genls( X, Y ), collection( X ) }.
% 0.78/1.17 { ! genls( X, Y ), collection( X ) }.
% 0.78/1.17 { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y ) }.
% 0.78/1.17 { ! collection( X ), genls( X, X ) }.
% 0.78/1.17 { ! collection( X ), genls( X, X ) }.
% 0.78/1.17 { ! genls( Z, X ), ! genls( Y, Z ), genls( Y, X ) }.
% 0.78/1.17 { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y ) }.
% 0.78/1.17 { mtvisible( c_basekb ) }.
% 0.78/1.17 { natfunction( f_urlfn( X ), c_urlfn ) }.
% 0.78/1.17 { natargument( f_urlfn( X ), n_1, X ) }.
% 0.78/1.17 { uniformresourcelocator( f_urlfn( X ) ) }.
% 0.78/1.17 { natfunction( f_urlreferentfn( X ), c_urlreferentfn ) }.
% 0.78/1.17 { natargument( f_urlreferentfn( X ), n_1, X ) }.
% 0.78/1.17 { computerdataartifact( f_urlreferentfn( X ) ) }.
% 0.78/1.17 { natfunction( f_contentmtofcdafromeventfn( X, Y ),
% 0.78/1.17 c_contentmtofcdafromeventfn ) }.
% 0.78/1.17 { natargument( f_contentmtofcdafromeventfn( X, Y ), n_1, X ) }.
% 0.78/1.17 { natargument( f_contentmtofcdafromeventfn( X, Y ), n_2, Y ) }.
% 0.78/1.17 { microtheory( f_contentmtofcdafromeventfn( X, Y ) ) }.
% 0.78/1.17 { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible( X ) }.
% 0.78/1.17 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.78/1.17 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.78/1.17 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.78/1.17 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.78/1.17 { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X, Y ) }.
% 0.78/1.17 { ! microtheory( X ), genlmt( X, X ) }.
% 0.78/1.17 { ! microtheory( X ), genlmt( X, X ) }.
% 0.78/1.17 { mtvisible( c_universalvocabularymt ) }.
% 0.78/1.17 { mtvisible( f_contentmtofcdafromeventfn( f_urlreferentfn( f_urlfn(
% 0.78/1.17 s_http_wwwthedailybulletincompostcardsmar9chtm ) ), c_translation_14 ) )
% 0.78/1.17 }.
% 0.78/1.17 { tptpcol_15_109185( c_tptpcol_16_62187 ) }.
% 0.78/1.17
% 0.78/1.17 percentage equality = 0.000000, percentage horn = 1.000000
% 0.78/1.17 This is a near-Horn, non-equality problem
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Options Used:
% 0.78/1.17
% 0.78/1.17 useres = 1
% 0.78/1.17 useparamod = 0
% 0.78/1.17 useeqrefl = 0
% 0.78/1.17 useeqfact = 0
% 0.78/1.17 usefactor = 1
% 0.78/1.17 usesimpsplitting = 0
% 0.78/1.17 usesimpdemod = 0
% 0.78/1.17 usesimpres = 4
% 0.78/1.17
% 0.78/1.17 resimpinuse = 1000
% 0.78/1.17 resimpclauses = 20000
% 0.78/1.17 substype = standard
% 0.78/1.17 backwardsubs = 1
% 0.78/1.17 selectoldest = 5
% 0.78/1.17
% 0.78/1.17 litorderings [0] = split
% 0.78/1.17 litorderings [1] = liftord
% 0.78/1.17
% 0.78/1.17 termordering = none
% 0.78/1.17
% 0.78/1.17 litapriori = 1
% 0.78/1.17 termapriori = 0
% 0.78/1.17 litaposteriori = 0
% 0.78/1.17 termaposteriori = 0
% 0.78/1.17 demodaposteriori = 0
% 0.78/1.17 ordereqreflfact = 0
% 0.78/1.17
% 0.78/1.17 litselect = negative
% 0.78/1.17
% 0.78/1.17 maxweight = 30000
% 0.78/1.17 maxdepth = 30000
% 0.78/1.17 maxlength = 115
% 0.78/1.17 maxnrvars = 195
% 0.78/1.17 excuselevel = 0
% 0.78/1.17 increasemaxweight = 0
% 0.78/1.17
% 0.78/1.17 maxselected = 10000000
% 0.78/1.17 maxnrclauses = 10000000
% 0.78/1.17
% 0.78/1.17 showgenerated = 0
% 0.78/1.17 showkept = 0
% 0.78/1.17 showselected = 0
% 0.78/1.17 showdeleted = 0
% 0.78/1.17 showresimp = 1
% 0.78/1.17 showstatus = 2000
% 0.78/1.17
% 0.78/1.17 prologoutput = 0
% 0.78/1.17 nrgoals = 5000000
% 0.78/1.17 totalproof = 1
% 0.78/1.17
% 0.78/1.17 Symbols occurring in the translation:
% 0.78/1.17
% 0.78/1.17 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.78/1.17 . [1, 2] (w:1, o:95, a:1, s:1, b:0),
% 0.78/1.17 ! [4, 1] (w:1, o:59, a:1, s:1, b:0),
% 0.78/1.17 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.78/1.17 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.78/1.17 s_http_wwwthedailybulletincompostcardsmar9chtm [35, 0] (w:1, o:6, a:1
% 0.78/1.17 , s:1, b:0),
% 0.78/1.17 f_urlfn [36, 1] (w:1, o:64, a:1, s:1, b:0),
% 0.78/1.17 f_urlreferentfn [37, 1] (w:1, o:65, a:1, s:1, b:0),
% 0.78/1.17 c_translation_14 [38, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.78/1.17 f_contentmtofcdafromeventfn [39, 2] (w:1, o:119, a:1, s:1, b:0),
% 0.78/1.17 c_machinelearningspindleheadmt [40, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.78/1.17 genlmt [41, 2] (w:1, o:120, a:1, s:1, b:0),
% 0.78/1.17 c_cycorpproductsmt [42, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.78/1.17 c_basekb [43, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.78/1.17 c_firstordercollection [44, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.78/1.17 c_fixedordercollection [45, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.78/1.17 genls [46, 2] (w:1, o:121, a:1, s:1, b:0),
% 0.78/1.17 firstordercollection [48, 1] (w:1, o:66, a:1, s:1, b:0),
% 0.78/1.17 fixedordercollection [49, 1] (w:1, o:67, a:1, s:1, b:0),
% 0.78/1.17 c_cycnounlearnermt [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.78/1.17 c_universalvocabularymt [51, 0] (w:1, o:35, a:1, s:1, b:0),
% 0.78/1.17 c_corecyclmt [52, 0] (w:1, o:36, a:1, s:1, b:0),
% 0.78/1.17 c_genlmt [53, 0] (w:1, o:37, a:1, s:1, b:0),
% 0.78/1.17 transitivebinarypredicate [54, 1] (w:1, o:68, a:1, s:1, b:0),
% 0.78/1.17 c_logicaltruthmt [55, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.78/1.17 collection [56, 1] (w:1, o:70, a:1, s:1, b:0),
% 0.78/1.17 individual [57, 1] (w:1, o:71, a:1, s:1, b:0),
% 0.78/1.17 c_collection [58, 0] (w:1, o:38, a:1, s:1, b:0),
% 0.78/1.17 c_individual [59, 0] (w:1, o:39, a:1, s:1, b:0),
% 0.78/1.17 disjointwith [60, 2] (w:1, o:122, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_0_0 [61, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_0_0 [62, 1] (w:1, o:72, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_16_62187 [63, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_1_65536 [64, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_1_65536 [65, 1] (w:1, o:73, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_2_98304 [66, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_2_98304 [67, 1] (w:1, o:81, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_3_98305 [68, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_3_98305 [69, 1] (w:1, o:82, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_4_106497 [70, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_4_106497 [71, 1] (w:1, o:83, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_5_106498 [72, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_5_106498 [73, 1] (w:1, o:84, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_6_108546 [74, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_6_108546 [75, 1] (w:1, o:85, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_7_108547 [76, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_7_108547 [77, 1] (w:1, o:86, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_8_109059 [78, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_8_109059 [79, 1] (w:1, o:87, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_9_109060 [80, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_9_109060 [81, 1] (w:1, o:88, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_10_109061 [82, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_10_109061 [83, 1] (w:1, o:74, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_11_109125 [84, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_11_109125 [85, 1] (w:1, o:75, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_12_109157 [86, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_12_109157 [87, 1] (w:1, o:76, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_13_109173 [88, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_13_109173 [89, 1] (w:1, o:77, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_14_109181 [90, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_14_109181 [91, 1] (w:1, o:78, a:1, s:1, b:0),
% 0.78/1.17 c_tptpcol_15_109185 [92, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_15_109185 [93, 1] (w:1, o:79, a:1, s:1, b:0),
% 0.78/1.17 isa [96, 2] (w:1, o:123, a:1, s:1, b:0),
% 0.78/1.17 genlinverse [100, 2] (w:1, o:124, a:1, s:1, b:0),
% 0.78/1.17 genlpreds [101, 2] (w:1, o:125, a:1, s:1, b:0),
% 0.78/1.17 predicate [104, 1] (w:1, o:89, a:1, s:1, b:0),
% 0.78/1.17 binarypredicate [109, 1] (w:1, o:69, a:1, s:1, b:0),
% 0.78/1.17 tptpcol_16_62187 [112, 1] (w:1, o:80, a:1, s:1, b:0),
% 0.78/1.17 mtvisible [113, 1] (w:1, o:90, a:1, s:1, b:0),
% 0.78/1.17 c_transitivebinarypredicate [114, 0] (w:1, o:34, a:1, s:1, b:0),
% 0.78/1.17 thing [115, 1] (w:1, o:91, a:1, s:1, b:0),
% 0.78/1.17 c_urlfn [116, 0] (w:1, o:52, a:1, s:1, b:0),
% 0.78/1.17 natfunction [117, 2] (w:1, o:126, a:1, s:1, b:0),
% 0.78/1.17 n_1 [118, 0] (w:1, o:53, a:1, s:1, b:0),
% 0.78/1.17 natargument [119, 3] (w:1, o:127, a:1, s:1, b:0),
% 0.78/1.17 uniformresourcelocator [120, 1] (w:1, o:92, a:1, s:1, b:0),
% 0.78/1.17 c_urlreferentfn [121, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.78/1.17 computerdataartifact [122, 1] (w:1, o:93, a:1, s:1, b:0),
% 0.78/1.17 c_contentmtofcdafromeventfn [123, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.78/1.17 n_2 [124, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.78/1.17 microtheory [125, 1] (w:1, o:94, a:1, s:1, b:0).
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Starting Search:
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Bliksems!, er is een bewijs:
% 0.78/1.17 % SZS status Theorem
% 0.78/1.17 % SZS output start Refutation
% 0.78/1.17
% 0.78/1.17 (3) {G0,W5,D2,L2,V1,M1} I { fixedordercollection( X ), !
% 0.78/1.17 firstordercollection( X ) }.
% 0.78/1.17 (8) {G0,W6,D2,L2,V1,M1} I { ! individual( X ), ! collection( X ) }.
% 0.78/1.17 (13) {G0,W5,D2,L2,V1,M1} I { collection( X ), ! fixedordercollection( X )
% 0.78/1.17 }.
% 0.78/1.17 (15) {G0,W5,D2,L2,V1,M1} I { individual( X ), ! tptpcol_0_0( X ) }.
% 0.78/1.17 (16) {G0,W2,D2,L1,V0,M1} I { firstordercollection( c_tptpcol_16_62187 ) }.
% 0.78/1.17 (18) {G0,W5,D2,L2,V1,M1} I { tptpcol_0_0( X ), ! tptpcol_1_65536( X ) }.
% 0.78/1.17 (20) {G0,W5,D2,L2,V1,M1} I { tptpcol_1_65536( X ), ! tptpcol_2_98304( X )
% 0.78/1.17 }.
% 0.78/1.17 (22) {G0,W5,D2,L2,V1,M1} I { tptpcol_2_98304( X ), ! tptpcol_3_98305( X )
% 0.78/1.17 }.
% 0.78/1.17 (24) {G0,W5,D2,L2,V1,M1} I { tptpcol_3_98305( X ), ! tptpcol_4_106497( X )
% 0.78/1.17 }.
% 0.78/1.17 (26) {G0,W5,D2,L2,V1,M1} I { tptpcol_4_106497( X ), ! tptpcol_5_106498( X )
% 0.78/1.17 }.
% 0.78/1.17 (28) {G0,W5,D2,L2,V1,M1} I { tptpcol_5_106498( X ), ! tptpcol_6_108546( X )
% 0.78/1.17 }.
% 0.78/1.17 (30) {G0,W5,D2,L2,V1,M1} I { tptpcol_6_108546( X ), ! tptpcol_7_108547( X )
% 0.78/1.17 }.
% 0.78/1.17 (32) {G0,W5,D2,L2,V1,M1} I { tptpcol_7_108547( X ), ! tptpcol_8_109059( X )
% 0.78/1.17 }.
% 0.78/1.17 (34) {G0,W5,D2,L2,V1,M1} I { tptpcol_8_109059( X ), ! tptpcol_9_109060( X )
% 0.78/1.17 }.
% 0.78/1.17 (36) {G0,W5,D2,L2,V1,M1} I { tptpcol_9_109060( X ), ! tptpcol_10_109061( X
% 0.78/1.17 ) }.
% 0.78/1.17 (38) {G0,W5,D2,L2,V1,M1} I { tptpcol_10_109061( X ), ! tptpcol_11_109125( X
% 0.78/1.17 ) }.
% 0.78/1.17 (40) {G0,W5,D2,L2,V1,M1} I { tptpcol_11_109125( X ), ! tptpcol_12_109157( X
% 0.78/1.17 ) }.
% 0.78/1.17 (42) {G0,W5,D2,L2,V1,M1} I { tptpcol_12_109157( X ), ! tptpcol_13_109173( X
% 0.78/1.17 ) }.
% 0.78/1.17 (44) {G0,W5,D2,L2,V1,M1} I { tptpcol_13_109173( X ), ! tptpcol_14_109181( X
% 0.78/1.17 ) }.
% 0.78/1.17 (46) {G0,W5,D2,L2,V1,M1} I { tptpcol_14_109181( X ), ! tptpcol_15_109185( X
% 0.78/1.17 ) }.
% 0.78/1.17 (133) {G0,W2,D2,L1,V0,M1} I { tptpcol_15_109185( c_tptpcol_16_62187 ) }.
% 0.78/1.17 (136) {G1,W2,D2,L1,V0,M1} R(3,16) { fixedordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 (137) {G2,W2,D2,L1,V0,M1} R(13,136) { collection( c_tptpcol_16_62187 ) }.
% 0.78/1.17 (138) {G3,W3,D2,L1,V0,M1} R(137,8) { ! individual( c_tptpcol_16_62187 ) }.
% 0.78/1.17 (139) {G1,W2,D2,L1,V0,M1} R(46,133) { tptpcol_14_109181( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (140) {G2,W2,D2,L1,V0,M1} R(44,139) { tptpcol_13_109173( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (141) {G3,W2,D2,L1,V0,M1} R(42,140) { tptpcol_12_109157( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (142) {G4,W2,D2,L1,V0,M1} R(40,141) { tptpcol_11_109125( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (143) {G5,W2,D2,L1,V0,M1} R(38,142) { tptpcol_10_109061( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (144) {G6,W2,D2,L1,V0,M1} R(36,143) { tptpcol_9_109060( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (145) {G7,W2,D2,L1,V0,M1} R(34,144) { tptpcol_8_109059( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (146) {G8,W2,D2,L1,V0,M1} R(32,145) { tptpcol_7_108547( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (147) {G9,W2,D2,L1,V0,M1} R(30,146) { tptpcol_6_108546( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (148) {G10,W2,D2,L1,V0,M1} R(28,147) { tptpcol_5_106498( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (149) {G11,W2,D2,L1,V0,M1} R(26,148) { tptpcol_4_106497( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (151) {G12,W2,D2,L1,V0,M1} R(149,24) { tptpcol_3_98305( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (152) {G13,W2,D2,L1,V0,M1} R(151,22) { tptpcol_2_98304( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (153) {G14,W2,D2,L1,V0,M1} R(152,20) { tptpcol_1_65536( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 (154) {G15,W2,D2,L1,V0,M1} R(153,18) { tptpcol_0_0( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 (155) {G16,W0,D0,L0,V0,M0} R(154,15);r(138) { }.
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 % SZS output end Refutation
% 0.78/1.17 found a proof!
% 0.78/1.17
% 0.78/1.17 *** allocated 15000 integers for clauses
% 0.78/1.17
% 0.78/1.17 Unprocessed initial clauses:
% 0.78/1.17
% 0.78/1.17 (157) {G0,W7,D5,L1,V0,M1} { genlmt( f_contentmtofcdafromeventfn(
% 0.78/1.17 f_urlreferentfn( f_urlfn( s_http_wwwthedailybulletincompostcardsmar9chtm
% 0.78/1.17 ) ), c_translation_14 ), c_machinelearningspindleheadmt ) }.
% 0.78/1.17 (158) {G0,W3,D2,L1,V0,M1} { genlmt( c_cycorpproductsmt, c_basekb ) }.
% 0.78/1.17 (159) {G0,W3,D2,L1,V0,M1} { genls( c_firstordercollection,
% 0.78/1.17 c_fixedordercollection ) }.
% 0.78/1.17 (160) {G0,W5,D2,L2,V1,M2} { ! firstordercollection( X ),
% 0.78/1.17 fixedordercollection( X ) }.
% 0.78/1.17 (161) {G0,W3,D2,L1,V0,M1} { genlmt( c_cycnounlearnermt, c_cycorpproductsmt
% 0.78/1.17 ) }.
% 0.78/1.17 (162) {G0,W3,D2,L1,V0,M1} { genlmt( c_universalvocabularymt, c_corecyclmt
% 0.78/1.17 ) }.
% 0.78/1.17 (163) {G0,W2,D2,L1,V0,M1} { transitivebinarypredicate( c_genlmt ) }.
% 0.78/1.17 (164) {G0,W3,D2,L1,V0,M1} { genlmt( c_corecyclmt, c_logicaltruthmt ) }.
% 0.78/1.17 (165) {G0,W6,D2,L2,V1,M2} { ! collection( X ), ! individual( X ) }.
% 0.78/1.17 (166) {G0,W3,D2,L1,V0,M1} { disjointwith( c_collection, c_individual ) }.
% 0.78/1.17 (167) {G0,W3,D2,L1,V0,M1} { genlmt( c_machinelearningspindleheadmt,
% 0.78/1.17 c_cycnounlearnermt ) }.
% 0.78/1.17 (168) {G0,W3,D2,L1,V0,M1} { genlmt( c_basekb, c_universalvocabularymt )
% 0.78/1.17 }.
% 0.78/1.17 (169) {G0,W3,D2,L1,V0,M1} { genls( c_fixedordercollection, c_collection )
% 0.78/1.17 }.
% 0.78/1.17 (170) {G0,W5,D2,L2,V1,M2} { ! fixedordercollection( X ), collection( X )
% 0.78/1.17 }.
% 0.78/1.17 (171) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_0_0, c_individual ) }.
% 0.78/1.17 (172) {G0,W5,D2,L2,V1,M2} { ! tptpcol_0_0( X ), individual( X ) }.
% 0.78/1.17 (173) {G0,W2,D2,L1,V0,M1} { firstordercollection( c_tptpcol_16_62187 ) }.
% 0.78/1.17 (174) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_1_65536, c_tptpcol_0_0 ) }.
% 0.78/1.17 (175) {G0,W5,D2,L2,V1,M2} { ! tptpcol_1_65536( X ), tptpcol_0_0( X ) }.
% 0.78/1.17 (176) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_2_98304, c_tptpcol_1_65536 )
% 0.78/1.17 }.
% 0.78/1.17 (177) {G0,W5,D2,L2,V1,M2} { ! tptpcol_2_98304( X ), tptpcol_1_65536( X )
% 0.78/1.17 }.
% 0.78/1.17 (178) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_3_98305, c_tptpcol_2_98304 )
% 0.78/1.17 }.
% 0.78/1.17 (179) {G0,W5,D2,L2,V1,M2} { ! tptpcol_3_98305( X ), tptpcol_2_98304( X )
% 0.78/1.17 }.
% 0.78/1.17 (180) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_106497, c_tptpcol_3_98305 )
% 0.78/1.17 }.
% 0.78/1.17 (181) {G0,W5,D2,L2,V1,M2} { ! tptpcol_4_106497( X ), tptpcol_3_98305( X )
% 0.78/1.17 }.
% 0.78/1.17 (182) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_106498, c_tptpcol_4_106497
% 0.78/1.17 ) }.
% 0.78/1.17 (183) {G0,W5,D2,L2,V1,M2} { ! tptpcol_5_106498( X ), tptpcol_4_106497( X )
% 0.78/1.17 }.
% 0.78/1.17 (184) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_108546, c_tptpcol_5_106498
% 0.78/1.17 ) }.
% 0.78/1.17 (185) {G0,W5,D2,L2,V1,M2} { ! tptpcol_6_108546( X ), tptpcol_5_106498( X )
% 0.78/1.17 }.
% 0.78/1.17 (186) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_108547, c_tptpcol_6_108546
% 0.78/1.17 ) }.
% 0.78/1.17 (187) {G0,W5,D2,L2,V1,M2} { ! tptpcol_7_108547( X ), tptpcol_6_108546( X )
% 0.78/1.17 }.
% 0.78/1.17 (188) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_109059, c_tptpcol_7_108547
% 0.78/1.17 ) }.
% 0.78/1.17 (189) {G0,W5,D2,L2,V1,M2} { ! tptpcol_8_109059( X ), tptpcol_7_108547( X )
% 0.78/1.17 }.
% 0.78/1.17 (190) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_109060, c_tptpcol_8_109059
% 0.78/1.17 ) }.
% 0.78/1.17 (191) {G0,W5,D2,L2,V1,M2} { ! tptpcol_9_109060( X ), tptpcol_8_109059( X )
% 0.78/1.17 }.
% 0.78/1.17 (192) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_109061, c_tptpcol_9_109060
% 0.78/1.17 ) }.
% 0.78/1.17 (193) {G0,W5,D2,L2,V1,M2} { ! tptpcol_10_109061( X ), tptpcol_9_109060( X
% 0.78/1.17 ) }.
% 0.78/1.17 (194) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_109125,
% 0.78/1.17 c_tptpcol_10_109061 ) }.
% 0.78/1.17 (195) {G0,W5,D2,L2,V1,M2} { ! tptpcol_11_109125( X ), tptpcol_10_109061( X
% 0.78/1.17 ) }.
% 0.78/1.17 (196) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_109157,
% 0.78/1.17 c_tptpcol_11_109125 ) }.
% 0.78/1.17 (197) {G0,W5,D2,L2,V1,M2} { ! tptpcol_12_109157( X ), tptpcol_11_109125( X
% 0.78/1.17 ) }.
% 0.78/1.17 (198) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_109173,
% 0.78/1.17 c_tptpcol_12_109157 ) }.
% 0.78/1.17 (199) {G0,W5,D2,L2,V1,M2} { ! tptpcol_13_109173( X ), tptpcol_12_109157( X
% 0.78/1.17 ) }.
% 0.78/1.17 (200) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_109181,
% 0.78/1.17 c_tptpcol_13_109173 ) }.
% 0.78/1.17 (201) {G0,W5,D2,L2,V1,M2} { ! tptpcol_14_109181( X ), tptpcol_13_109173( X
% 0.78/1.17 ) }.
% 0.78/1.17 (202) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_15_109185,
% 0.78/1.17 c_tptpcol_14_109181 ) }.
% 0.78/1.17 (203) {G0,W5,D2,L2,V1,M2} { ! tptpcol_15_109185( X ), tptpcol_14_109181( X
% 0.78/1.17 ) }.
% 0.78/1.17 (204) {G0,W12,D2,L3,V3,M3} { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith
% 0.78/1.17 ( Y, Z ) }.
% 0.78/1.17 (205) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlinverse( Z, Y )
% 0.78/1.17 , genlpreds( X, Y ) }.
% 0.78/1.17 (206) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.78/1.17 (207) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.78/1.17 (208) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.78/1.17 (209) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.78/1.17 (210) {G0,W11,D2,L3,V3,M3} { ! genlpreds( X, Z ), ! genlpreds( Z, Y ),
% 0.78/1.17 genlpreds( X, Y ) }.
% 0.78/1.17 (211) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.78/1.17 (212) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.78/1.17 (213) {G0,W6,D2,L2,V2,M2} { ! genlinverse( Y, X ), binarypredicate( X )
% 0.78/1.17 }.
% 0.78/1.17 (214) {G0,W6,D2,L2,V2,M2} { ! genlinverse( X, Y ), binarypredicate( X )
% 0.78/1.17 }.
% 0.78/1.17 (215) {G0,W11,D2,L3,V3,M3} { ! genlinverse( Z, X ), ! genlpreds( Y, Z ),
% 0.78/1.17 genlinverse( Y, X ) }.
% 0.78/1.17 (216) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlpreds( Z, Y ),
% 0.78/1.17 genlinverse( X, Y ) }.
% 0.78/1.17 (217) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_15_109185 ),
% 0.78/1.17 tptpcol_15_109185( X ) }.
% 0.78/1.17 (218) {G0,W6,D2,L2,V1,M2} { ! tptpcol_15_109185( X ), isa( X,
% 0.78/1.17 c_tptpcol_15_109185 ) }.
% 0.78/1.17 (219) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_14_109181 ),
% 0.78/1.17 tptpcol_14_109181( X ) }.
% 0.78/1.17 (220) {G0,W6,D2,L2,V1,M2} { ! tptpcol_14_109181( X ), isa( X,
% 0.78/1.17 c_tptpcol_14_109181 ) }.
% 0.78/1.17 (221) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_13_109173 ),
% 0.78/1.17 tptpcol_13_109173( X ) }.
% 0.78/1.17 (222) {G0,W6,D2,L2,V1,M2} { ! tptpcol_13_109173( X ), isa( X,
% 0.78/1.17 c_tptpcol_13_109173 ) }.
% 0.78/1.17 (223) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_12_109157 ),
% 0.78/1.17 tptpcol_12_109157( X ) }.
% 0.78/1.17 (224) {G0,W6,D2,L2,V1,M2} { ! tptpcol_12_109157( X ), isa( X,
% 0.78/1.17 c_tptpcol_12_109157 ) }.
% 0.78/1.17 (225) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_11_109125 ),
% 0.78/1.17 tptpcol_11_109125( X ) }.
% 0.78/1.17 (226) {G0,W6,D2,L2,V1,M2} { ! tptpcol_11_109125( X ), isa( X,
% 0.78/1.17 c_tptpcol_11_109125 ) }.
% 0.78/1.17 (227) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_10_109061 ),
% 0.78/1.17 tptpcol_10_109061( X ) }.
% 0.78/1.17 (228) {G0,W6,D2,L2,V1,M2} { ! tptpcol_10_109061( X ), isa( X,
% 0.78/1.17 c_tptpcol_10_109061 ) }.
% 0.78/1.17 (229) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_9_109060 ),
% 0.78/1.17 tptpcol_9_109060( X ) }.
% 0.78/1.17 (230) {G0,W6,D2,L2,V1,M2} { ! tptpcol_9_109060( X ), isa( X,
% 0.78/1.17 c_tptpcol_9_109060 ) }.
% 0.78/1.17 (231) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_8_109059 ),
% 0.78/1.17 tptpcol_8_109059( X ) }.
% 0.78/1.17 (232) {G0,W6,D2,L2,V1,M2} { ! tptpcol_8_109059( X ), isa( X,
% 0.78/1.17 c_tptpcol_8_109059 ) }.
% 0.78/1.17 (233) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_7_108547 ),
% 0.78/1.17 tptpcol_7_108547( X ) }.
% 0.78/1.17 (234) {G0,W6,D2,L2,V1,M2} { ! tptpcol_7_108547( X ), isa( X,
% 0.78/1.17 c_tptpcol_7_108547 ) }.
% 0.78/1.17 (235) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_6_108546 ),
% 0.78/1.17 tptpcol_6_108546( X ) }.
% 0.78/1.17 (236) {G0,W6,D2,L2,V1,M2} { ! tptpcol_6_108546( X ), isa( X,
% 0.78/1.17 c_tptpcol_6_108546 ) }.
% 0.78/1.17 (237) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_5_106498 ),
% 0.78/1.17 tptpcol_5_106498( X ) }.
% 0.78/1.17 (238) {G0,W6,D2,L2,V1,M2} { ! tptpcol_5_106498( X ), isa( X,
% 0.78/1.17 c_tptpcol_5_106498 ) }.
% 0.78/1.17 (239) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_4_106497 ),
% 0.78/1.17 tptpcol_4_106497( X ) }.
% 0.78/1.17 (240) {G0,W6,D2,L2,V1,M2} { ! tptpcol_4_106497( X ), isa( X,
% 0.78/1.17 c_tptpcol_4_106497 ) }.
% 0.78/1.17 (241) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_3_98305 ), tptpcol_3_98305
% 0.78/1.17 ( X ) }.
% 0.78/1.17 (242) {G0,W6,D2,L2,V1,M2} { ! tptpcol_3_98305( X ), isa( X,
% 0.78/1.17 c_tptpcol_3_98305 ) }.
% 0.78/1.17 (243) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_2_98304 ), tptpcol_2_98304
% 0.78/1.17 ( X ) }.
% 0.78/1.17 (244) {G0,W6,D2,L2,V1,M2} { ! tptpcol_2_98304( X ), isa( X,
% 0.78/1.17 c_tptpcol_2_98304 ) }.
% 0.78/1.17 (245) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_1_65536 ), tptpcol_1_65536
% 0.78/1.17 ( X ) }.
% 0.78/1.17 (246) {G0,W6,D2,L2,V1,M2} { ! tptpcol_1_65536( X ), isa( X,
% 0.78/1.17 c_tptpcol_1_65536 ) }.
% 0.78/1.17 (247) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_16_62187 ),
% 0.78/1.17 tptpcol_16_62187( X ) }.
% 0.78/1.17 (248) {G0,W6,D2,L2,V1,M2} { ! tptpcol_16_62187( X ), isa( X,
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 (249) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_0_0 ), tptpcol_0_0( X )
% 0.78/1.17 }.
% 0.78/1.17 (250) {G0,W6,D2,L2,V1,M2} { ! tptpcol_0_0( X ), isa( X, c_tptpcol_0_0 )
% 0.78/1.17 }.
% 0.78/1.17 (251) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_individual ), individual( X ) }.
% 0.78/1.17 (252) {G0,W6,D2,L2,V1,M2} { ! individual( X ), isa( X, c_individual ) }.
% 0.78/1.17 (253) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_collection ), collection( X ) }.
% 0.78/1.17 (254) {G0,W6,D2,L2,V1,M2} { ! collection( X ), isa( X, c_collection ) }.
% 0.78/1.17 (255) {G0,W6,D2,L2,V2,M2} { ! disjointwith( Y, X ), collection( X ) }.
% 0.78/1.17 (256) {G0,W6,D2,L2,V2,M2} { ! disjointwith( X, Y ), collection( X ) }.
% 0.78/1.17 (257) {G0,W7,D2,L2,V2,M2} { ! disjointwith( X, Y ), disjointwith( Y, X )
% 0.78/1.17 }.
% 0.78/1.17 (258) {G0,W11,D2,L3,V3,M3} { ! disjointwith( X, Z ), ! genls( Y, Z ),
% 0.78/1.17 disjointwith( X, Y ) }.
% 0.78/1.17 (259) {G0,W11,D2,L3,V3,M3} { ! disjointwith( Z, X ), ! genls( Y, Z ),
% 0.78/1.17 disjointwith( Y, X ) }.
% 0.78/1.17 (260) {G0,W2,D2,L1,V0,M1} { mtvisible( c_logicaltruthmt ) }.
% 0.78/1.17 (261) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_transitivebinarypredicate ),
% 0.78/1.17 transitivebinarypredicate( X ) }.
% 0.78/1.17 (262) {G0,W6,D2,L2,V1,M2} { ! transitivebinarypredicate( X ), isa( X,
% 0.78/1.17 c_transitivebinarypredicate ) }.
% 0.78/1.17 (263) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.78/1.17 (264) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.78/1.17 (265) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.78/1.17 (266) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.78/1.17 (267) {G0,W11,D2,L3,V3,M3} { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y )
% 0.78/1.17 }.
% 0.78/1.17 (268) {G0,W2,D2,L1,V0,M1} { mtvisible( c_corecyclmt ) }.
% 0.78/1.17 (269) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_fixedordercollection ),
% 0.78/1.17 fixedordercollection( X ) }.
% 0.78/1.17 (270) {G0,W6,D2,L2,V1,M2} { ! fixedordercollection( X ), isa( X,
% 0.78/1.17 c_fixedordercollection ) }.
% 0.78/1.17 (271) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_firstordercollection ),
% 0.78/1.17 firstordercollection( X ) }.
% 0.78/1.17 (272) {G0,W6,D2,L2,V1,M2} { ! firstordercollection( X ), isa( X,
% 0.78/1.17 c_firstordercollection ) }.
% 0.78/1.17 (273) {G0,W6,D2,L2,V2,M2} { ! genls( Y, X ), collection( X ) }.
% 0.78/1.17 (274) {G0,W6,D2,L2,V2,M2} { ! genls( Y, X ), collection( X ) }.
% 0.78/1.17 (275) {G0,W6,D2,L2,V2,M2} { ! genls( X, Y ), collection( X ) }.
% 0.78/1.17 (276) {G0,W6,D2,L2,V2,M2} { ! genls( X, Y ), collection( X ) }.
% 0.78/1.17 (277) {G0,W11,D2,L3,V3,M3} { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y
% 0.78/1.17 ) }.
% 0.78/1.17 (278) {G0,W6,D2,L2,V1,M2} { ! collection( X ), genls( X, X ) }.
% 0.78/1.17 (279) {G0,W6,D2,L2,V1,M2} { ! collection( X ), genls( X, X ) }.
% 0.78/1.17 (280) {G0,W11,D2,L3,V3,M3} { ! genls( Z, X ), ! genls( Y, Z ), genls( Y, X
% 0.78/1.17 ) }.
% 0.78/1.17 (281) {G0,W11,D2,L3,V3,M3} { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y
% 0.78/1.17 ) }.
% 0.78/1.17 (282) {G0,W2,D2,L1,V0,M1} { mtvisible( c_basekb ) }.
% 0.78/1.17 (283) {G0,W4,D3,L1,V1,M1} { natfunction( f_urlfn( X ), c_urlfn ) }.
% 0.78/1.17 (284) {G0,W5,D3,L1,V1,M1} { natargument( f_urlfn( X ), n_1, X ) }.
% 0.78/1.17 (285) {G0,W3,D3,L1,V1,M1} { uniformresourcelocator( f_urlfn( X ) ) }.
% 0.78/1.17 (286) {G0,W4,D3,L1,V1,M1} { natfunction( f_urlreferentfn( X ),
% 0.78/1.17 c_urlreferentfn ) }.
% 0.78/1.17 (287) {G0,W5,D3,L1,V1,M1} { natargument( f_urlreferentfn( X ), n_1, X )
% 0.78/1.17 }.
% 0.78/1.17 (288) {G0,W3,D3,L1,V1,M1} { computerdataartifact( f_urlreferentfn( X ) )
% 0.78/1.17 }.
% 0.78/1.17 (289) {G0,W5,D3,L1,V2,M1} { natfunction( f_contentmtofcdafromeventfn( X, Y
% 0.78/1.17 ), c_contentmtofcdafromeventfn ) }.
% 0.78/1.17 (290) {G0,W6,D3,L1,V2,M1} { natargument( f_contentmtofcdafromeventfn( X, Y
% 0.78/1.17 ), n_1, X ) }.
% 0.78/1.17 (291) {G0,W6,D3,L1,V2,M1} { natargument( f_contentmtofcdafromeventfn( X, Y
% 0.78/1.17 ), n_2, Y ) }.
% 0.78/1.17 (292) {G0,W4,D3,L1,V2,M1} { microtheory( f_contentmtofcdafromeventfn( X, Y
% 0.78/1.17 ) ) }.
% 0.78/1.17 (293) {G0,W9,D2,L3,V2,M3} { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible
% 0.78/1.17 ( X ) }.
% 0.78/1.17 (294) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.78/1.17 (295) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.78/1.17 (296) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.78/1.17 (297) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.78/1.17 (298) {G0,W11,D2,L3,V3,M3} { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X
% 0.78/1.17 , Y ) }.
% 0.78/1.17 (299) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.78/1.17 (300) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.78/1.17 (301) {G0,W2,D2,L1,V0,M1} { mtvisible( c_universalvocabularymt ) }.
% 0.78/1.17 (302) {G0,W6,D5,L1,V0,M1} { mtvisible( f_contentmtofcdafromeventfn(
% 0.78/1.17 f_urlreferentfn( f_urlfn( s_http_wwwthedailybulletincompostcardsmar9chtm
% 0.78/1.17 ) ), c_translation_14 ) ) }.
% 0.78/1.17 (303) {G0,W2,D2,L1,V0,M1} { tptpcol_15_109185( c_tptpcol_16_62187 ) }.
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Total Proof:
% 0.78/1.17
% 0.78/1.17 subsumption: (3) {G0,W5,D2,L2,V1,M1} I { fixedordercollection( X ), !
% 0.78/1.17 firstordercollection( X ) }.
% 0.78/1.17 parent0: (160) {G0,W5,D2,L2,V1,M2} { ! firstordercollection( X ),
% 0.78/1.17 fixedordercollection( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (8) {G0,W6,D2,L2,V1,M1} I { ! individual( X ), ! collection( X
% 0.78/1.17 ) }.
% 0.78/1.17 parent0: (165) {G0,W6,D2,L2,V1,M2} { ! collection( X ), ! individual( X )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (13) {G0,W5,D2,L2,V1,M1} I { collection( X ), !
% 0.78/1.17 fixedordercollection( X ) }.
% 0.78/1.17 parent0: (170) {G0,W5,D2,L2,V1,M2} { ! fixedordercollection( X ),
% 0.78/1.17 collection( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (15) {G0,W5,D2,L2,V1,M1} I { individual( X ), ! tptpcol_0_0( X
% 0.78/1.17 ) }.
% 0.78/1.17 parent0: (172) {G0,W5,D2,L2,V1,M2} { ! tptpcol_0_0( X ), individual( X )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (16) {G0,W2,D2,L1,V0,M1} I { firstordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (173) {G0,W2,D2,L1,V0,M1} { firstordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (18) {G0,W5,D2,L2,V1,M1} I { tptpcol_0_0( X ), !
% 0.78/1.17 tptpcol_1_65536( X ) }.
% 0.78/1.17 parent0: (175) {G0,W5,D2,L2,V1,M2} { ! tptpcol_1_65536( X ), tptpcol_0_0(
% 0.78/1.17 X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (20) {G0,W5,D2,L2,V1,M1} I { tptpcol_1_65536( X ), !
% 0.78/1.17 tptpcol_2_98304( X ) }.
% 0.78/1.17 parent0: (177) {G0,W5,D2,L2,V1,M2} { ! tptpcol_2_98304( X ),
% 0.78/1.17 tptpcol_1_65536( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (22) {G0,W5,D2,L2,V1,M1} I { tptpcol_2_98304( X ), !
% 0.78/1.17 tptpcol_3_98305( X ) }.
% 0.78/1.17 parent0: (179) {G0,W5,D2,L2,V1,M2} { ! tptpcol_3_98305( X ),
% 0.78/1.17 tptpcol_2_98304( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (24) {G0,W5,D2,L2,V1,M1} I { tptpcol_3_98305( X ), !
% 0.78/1.17 tptpcol_4_106497( X ) }.
% 0.78/1.17 parent0: (181) {G0,W5,D2,L2,V1,M2} { ! tptpcol_4_106497( X ),
% 0.78/1.17 tptpcol_3_98305( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (26) {G0,W5,D2,L2,V1,M1} I { tptpcol_4_106497( X ), !
% 0.78/1.17 tptpcol_5_106498( X ) }.
% 0.78/1.17 parent0: (183) {G0,W5,D2,L2,V1,M2} { ! tptpcol_5_106498( X ),
% 0.78/1.17 tptpcol_4_106497( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (28) {G0,W5,D2,L2,V1,M1} I { tptpcol_5_106498( X ), !
% 0.78/1.17 tptpcol_6_108546( X ) }.
% 0.78/1.17 parent0: (185) {G0,W5,D2,L2,V1,M2} { ! tptpcol_6_108546( X ),
% 0.78/1.17 tptpcol_5_106498( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (30) {G0,W5,D2,L2,V1,M1} I { tptpcol_6_108546( X ), !
% 0.78/1.17 tptpcol_7_108547( X ) }.
% 0.78/1.17 parent0: (187) {G0,W5,D2,L2,V1,M2} { ! tptpcol_7_108547( X ),
% 0.78/1.17 tptpcol_6_108546( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (32) {G0,W5,D2,L2,V1,M1} I { tptpcol_7_108547( X ), !
% 0.78/1.17 tptpcol_8_109059( X ) }.
% 0.78/1.17 parent0: (189) {G0,W5,D2,L2,V1,M2} { ! tptpcol_8_109059( X ),
% 0.78/1.17 tptpcol_7_108547( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (34) {G0,W5,D2,L2,V1,M1} I { tptpcol_8_109059( X ), !
% 0.78/1.17 tptpcol_9_109060( X ) }.
% 0.78/1.17 parent0: (191) {G0,W5,D2,L2,V1,M2} { ! tptpcol_9_109060( X ),
% 0.78/1.17 tptpcol_8_109059( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (36) {G0,W5,D2,L2,V1,M1} I { tptpcol_9_109060( X ), !
% 0.78/1.17 tptpcol_10_109061( X ) }.
% 0.78/1.17 parent0: (193) {G0,W5,D2,L2,V1,M2} { ! tptpcol_10_109061( X ),
% 0.78/1.17 tptpcol_9_109060( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (38) {G0,W5,D2,L2,V1,M1} I { tptpcol_10_109061( X ), !
% 0.78/1.17 tptpcol_11_109125( X ) }.
% 0.78/1.17 parent0: (195) {G0,W5,D2,L2,V1,M2} { ! tptpcol_11_109125( X ),
% 0.78/1.17 tptpcol_10_109061( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (40) {G0,W5,D2,L2,V1,M1} I { tptpcol_11_109125( X ), !
% 0.78/1.17 tptpcol_12_109157( X ) }.
% 0.78/1.17 parent0: (197) {G0,W5,D2,L2,V1,M2} { ! tptpcol_12_109157( X ),
% 0.78/1.17 tptpcol_11_109125( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (42) {G0,W5,D2,L2,V1,M1} I { tptpcol_12_109157( X ), !
% 0.78/1.17 tptpcol_13_109173( X ) }.
% 0.78/1.17 parent0: (199) {G0,W5,D2,L2,V1,M2} { ! tptpcol_13_109173( X ),
% 0.78/1.17 tptpcol_12_109157( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (44) {G0,W5,D2,L2,V1,M1} I { tptpcol_13_109173( X ), !
% 0.78/1.17 tptpcol_14_109181( X ) }.
% 0.78/1.17 parent0: (201) {G0,W5,D2,L2,V1,M2} { ! tptpcol_14_109181( X ),
% 0.78/1.17 tptpcol_13_109173( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (46) {G0,W5,D2,L2,V1,M1} I { tptpcol_14_109181( X ), !
% 0.78/1.17 tptpcol_15_109185( X ) }.
% 0.78/1.17 parent0: (203) {G0,W5,D2,L2,V1,M2} { ! tptpcol_15_109185( X ),
% 0.78/1.17 tptpcol_14_109181( X ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := X
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 1
% 0.78/1.17 1 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (133) {G0,W2,D2,L1,V0,M1} I { tptpcol_15_109185(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (303) {G0,W2,D2,L1,V0,M1} { tptpcol_15_109185( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (311) {G1,W2,D2,L1,V0,M1} { fixedordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (3) {G0,W5,D2,L2,V1,M1} I { fixedordercollection( X ), !
% 0.78/1.17 firstordercollection( X ) }.
% 0.78/1.17 parent1[0]: (16) {G0,W2,D2,L1,V0,M1} I { firstordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (136) {G1,W2,D2,L1,V0,M1} R(3,16) { fixedordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (311) {G1,W2,D2,L1,V0,M1} { fixedordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (312) {G1,W2,D2,L1,V0,M1} { collection( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 parent0[1]: (13) {G0,W5,D2,L2,V1,M1} I { collection( X ), !
% 0.78/1.17 fixedordercollection( X ) }.
% 0.78/1.17 parent1[0]: (136) {G1,W2,D2,L1,V0,M1} R(3,16) { fixedordercollection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (137) {G2,W2,D2,L1,V0,M1} R(13,136) { collection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (312) {G1,W2,D2,L1,V0,M1} { collection( c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (313) {G1,W3,D2,L1,V0,M1} { ! individual( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 parent0[1]: (8) {G0,W6,D2,L2,V1,M1} I { ! individual( X ), ! collection( X
% 0.78/1.17 ) }.
% 0.78/1.17 parent1[0]: (137) {G2,W2,D2,L1,V0,M1} R(13,136) { collection(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (138) {G3,W3,D2,L1,V0,M1} R(137,8) { ! individual(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (313) {G1,W3,D2,L1,V0,M1} { ! individual( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (314) {G1,W2,D2,L1,V0,M1} { tptpcol_14_109181(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (46) {G0,W5,D2,L2,V1,M1} I { tptpcol_14_109181( X ), !
% 0.78/1.17 tptpcol_15_109185( X ) }.
% 0.78/1.17 parent1[0]: (133) {G0,W2,D2,L1,V0,M1} I { tptpcol_15_109185(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (139) {G1,W2,D2,L1,V0,M1} R(46,133) { tptpcol_14_109181(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (314) {G1,W2,D2,L1,V0,M1} { tptpcol_14_109181( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (315) {G1,W2,D2,L1,V0,M1} { tptpcol_13_109173(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (44) {G0,W5,D2,L2,V1,M1} I { tptpcol_13_109173( X ), !
% 0.78/1.17 tptpcol_14_109181( X ) }.
% 0.78/1.17 parent1[0]: (139) {G1,W2,D2,L1,V0,M1} R(46,133) { tptpcol_14_109181(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (140) {G2,W2,D2,L1,V0,M1} R(44,139) { tptpcol_13_109173(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (315) {G1,W2,D2,L1,V0,M1} { tptpcol_13_109173( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (316) {G1,W2,D2,L1,V0,M1} { tptpcol_12_109157(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (42) {G0,W5,D2,L2,V1,M1} I { tptpcol_12_109157( X ), !
% 0.78/1.17 tptpcol_13_109173( X ) }.
% 0.78/1.17 parent1[0]: (140) {G2,W2,D2,L1,V0,M1} R(44,139) { tptpcol_13_109173(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (141) {G3,W2,D2,L1,V0,M1} R(42,140) { tptpcol_12_109157(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (316) {G1,W2,D2,L1,V0,M1} { tptpcol_12_109157( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (317) {G1,W2,D2,L1,V0,M1} { tptpcol_11_109125(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (40) {G0,W5,D2,L2,V1,M1} I { tptpcol_11_109125( X ), !
% 0.78/1.17 tptpcol_12_109157( X ) }.
% 0.78/1.17 parent1[0]: (141) {G3,W2,D2,L1,V0,M1} R(42,140) { tptpcol_12_109157(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (142) {G4,W2,D2,L1,V0,M1} R(40,141) { tptpcol_11_109125(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (317) {G1,W2,D2,L1,V0,M1} { tptpcol_11_109125( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (318) {G1,W2,D2,L1,V0,M1} { tptpcol_10_109061(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (38) {G0,W5,D2,L2,V1,M1} I { tptpcol_10_109061( X ), !
% 0.78/1.17 tptpcol_11_109125( X ) }.
% 0.78/1.17 parent1[0]: (142) {G4,W2,D2,L1,V0,M1} R(40,141) { tptpcol_11_109125(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (143) {G5,W2,D2,L1,V0,M1} R(38,142) { tptpcol_10_109061(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (318) {G1,W2,D2,L1,V0,M1} { tptpcol_10_109061( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (319) {G1,W2,D2,L1,V0,M1} { tptpcol_9_109060(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (36) {G0,W5,D2,L2,V1,M1} I { tptpcol_9_109060( X ), !
% 0.78/1.17 tptpcol_10_109061( X ) }.
% 0.78/1.17 parent1[0]: (143) {G5,W2,D2,L1,V0,M1} R(38,142) { tptpcol_10_109061(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (144) {G6,W2,D2,L1,V0,M1} R(36,143) { tptpcol_9_109060(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (319) {G1,W2,D2,L1,V0,M1} { tptpcol_9_109060( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (320) {G1,W2,D2,L1,V0,M1} { tptpcol_8_109059(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (34) {G0,W5,D2,L2,V1,M1} I { tptpcol_8_109059( X ), !
% 0.78/1.17 tptpcol_9_109060( X ) }.
% 0.78/1.17 parent1[0]: (144) {G6,W2,D2,L1,V0,M1} R(36,143) { tptpcol_9_109060(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (145) {G7,W2,D2,L1,V0,M1} R(34,144) { tptpcol_8_109059(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (320) {G1,W2,D2,L1,V0,M1} { tptpcol_8_109059( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (321) {G1,W2,D2,L1,V0,M1} { tptpcol_7_108547(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (32) {G0,W5,D2,L2,V1,M1} I { tptpcol_7_108547( X ), !
% 0.78/1.17 tptpcol_8_109059( X ) }.
% 0.78/1.17 parent1[0]: (145) {G7,W2,D2,L1,V0,M1} R(34,144) { tptpcol_8_109059(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (146) {G8,W2,D2,L1,V0,M1} R(32,145) { tptpcol_7_108547(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (321) {G1,W2,D2,L1,V0,M1} { tptpcol_7_108547( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (322) {G1,W2,D2,L1,V0,M1} { tptpcol_6_108546(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (30) {G0,W5,D2,L2,V1,M1} I { tptpcol_6_108546( X ), !
% 0.78/1.17 tptpcol_7_108547( X ) }.
% 0.78/1.17 parent1[0]: (146) {G8,W2,D2,L1,V0,M1} R(32,145) { tptpcol_7_108547(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (147) {G9,W2,D2,L1,V0,M1} R(30,146) { tptpcol_6_108546(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (322) {G1,W2,D2,L1,V0,M1} { tptpcol_6_108546( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (323) {G1,W2,D2,L1,V0,M1} { tptpcol_5_106498(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (28) {G0,W5,D2,L2,V1,M1} I { tptpcol_5_106498( X ), !
% 0.78/1.17 tptpcol_6_108546( X ) }.
% 0.78/1.17 parent1[0]: (147) {G9,W2,D2,L1,V0,M1} R(30,146) { tptpcol_6_108546(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (148) {G10,W2,D2,L1,V0,M1} R(28,147) { tptpcol_5_106498(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (323) {G1,W2,D2,L1,V0,M1} { tptpcol_5_106498( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (324) {G1,W2,D2,L1,V0,M1} { tptpcol_4_106497(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (26) {G0,W5,D2,L2,V1,M1} I { tptpcol_4_106497( X ), !
% 0.78/1.17 tptpcol_5_106498( X ) }.
% 0.78/1.17 parent1[0]: (148) {G10,W2,D2,L1,V0,M1} R(28,147) { tptpcol_5_106498(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (149) {G11,W2,D2,L1,V0,M1} R(26,148) { tptpcol_4_106497(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (324) {G1,W2,D2,L1,V0,M1} { tptpcol_4_106497( c_tptpcol_16_62187
% 0.78/1.17 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (325) {G1,W2,D2,L1,V0,M1} { tptpcol_3_98305(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (24) {G0,W5,D2,L2,V1,M1} I { tptpcol_3_98305( X ), !
% 0.78/1.17 tptpcol_4_106497( X ) }.
% 0.78/1.17 parent1[0]: (149) {G11,W2,D2,L1,V0,M1} R(26,148) { tptpcol_4_106497(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (151) {G12,W2,D2,L1,V0,M1} R(149,24) { tptpcol_3_98305(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (325) {G1,W2,D2,L1,V0,M1} { tptpcol_3_98305( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (326) {G1,W2,D2,L1,V0,M1} { tptpcol_2_98304(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (22) {G0,W5,D2,L2,V1,M1} I { tptpcol_2_98304( X ), !
% 0.78/1.17 tptpcol_3_98305( X ) }.
% 0.78/1.17 parent1[0]: (151) {G12,W2,D2,L1,V0,M1} R(149,24) { tptpcol_3_98305(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (152) {G13,W2,D2,L1,V0,M1} R(151,22) { tptpcol_2_98304(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (326) {G1,W2,D2,L1,V0,M1} { tptpcol_2_98304( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (327) {G1,W2,D2,L1,V0,M1} { tptpcol_1_65536(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0[1]: (20) {G0,W5,D2,L2,V1,M1} I { tptpcol_1_65536( X ), !
% 0.78/1.17 tptpcol_2_98304( X ) }.
% 0.78/1.17 parent1[0]: (152) {G13,W2,D2,L1,V0,M1} R(151,22) { tptpcol_2_98304(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (153) {G14,W2,D2,L1,V0,M1} R(152,20) { tptpcol_1_65536(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (327) {G1,W2,D2,L1,V0,M1} { tptpcol_1_65536( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (328) {G1,W2,D2,L1,V0,M1} { tptpcol_0_0( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 parent0[1]: (18) {G0,W5,D2,L2,V1,M1} I { tptpcol_0_0( X ), !
% 0.78/1.17 tptpcol_1_65536( X ) }.
% 0.78/1.17 parent1[0]: (153) {G14,W2,D2,L1,V0,M1} R(152,20) { tptpcol_1_65536(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (154) {G15,W2,D2,L1,V0,M1} R(153,18) { tptpcol_0_0(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent0: (328) {G1,W2,D2,L1,V0,M1} { tptpcol_0_0( c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 0 ==> 0
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (329) {G1,W2,D2,L1,V0,M1} { individual( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 parent0[1]: (15) {G0,W5,D2,L2,V1,M1} I { individual( X ), ! tptpcol_0_0( X
% 0.78/1.17 ) }.
% 0.78/1.17 parent1[0]: (154) {G15,W2,D2,L1,V0,M1} R(153,18) { tptpcol_0_0(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 substitution0:
% 0.78/1.17 X := c_tptpcol_16_62187
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 resolution: (330) {G2,W0,D0,L0,V0,M0} { }.
% 0.78/1.17 parent0[0]: (138) {G3,W3,D2,L1,V0,M1} R(137,8) { ! individual(
% 0.78/1.17 c_tptpcol_16_62187 ) }.
% 0.78/1.17 parent1[0]: (329) {G1,W2,D2,L1,V0,M1} { individual( c_tptpcol_16_62187 )
% 0.78/1.17 }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 substitution1:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 subsumption: (155) {G16,W0,D0,L0,V0,M0} R(154,15);r(138) { }.
% 0.78/1.17 parent0: (330) {G2,W0,D0,L0,V0,M0} { }.
% 0.78/1.17 substitution0:
% 0.78/1.17 end
% 0.78/1.17 permutation0:
% 0.78/1.17 end
% 0.78/1.17
% 0.78/1.17 Proof check complete!
% 0.78/1.17
% 0.78/1.17 Memory use:
% 0.78/1.17
% 0.78/1.17 space for terms: 3148
% 0.78/1.17 space for clauses: 7789
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 clauses generated: 172
% 0.78/1.17 clauses kept: 156
% 0.78/1.17 clauses selected: 77
% 0.78/1.17 clauses deleted: 0
% 0.78/1.17 clauses inuse deleted: 0
% 0.78/1.17
% 0.78/1.17 subsentry: 27
% 0.78/1.17 literals s-matched: 25
% 0.78/1.17 literals matched: 25
% 0.78/1.17 full subsumption: 2
% 0.78/1.17
% 0.78/1.17 checksum: -1399086721
% 0.78/1.17
% 0.78/1.17
% 0.78/1.17 Bliksem ended
%------------------------------------------------------------------------------