%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n016.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:32 EDT 2022
% Result : Theorem 0.72s 1.09s
% Output : Refutation 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : bliksem %s
% 0.14/0.34 % Computer : n016.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % DateTime : Sat Jun 11 06:57:41 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.72/1.08 *** allocated 10000 integers for termspace/termends
% 0.72/1.08 *** allocated 10000 integers for clauses
% 0.72/1.08 *** allocated 10000 integers for justifications
% 0.72/1.08 Bliksem 1.12
% 0.72/1.08
% 0.72/1.08
% 0.72/1.08 Automatic Strategy Selection
% 0.72/1.08
% 0.72/1.08
% 0.72/1.08 Clauses:
% 0.72/1.08
% 0.72/1.08 { transitivebinarypredicate( c_genlmt ) }.
% 0.72/1.08 { genlmt( c_generictemporalmt, c_basekb ) }.
% 0.72/1.08 { genlmt( c_timehasnoendmt, c_generictemporalmt ) }.
% 0.72/1.08 { genlmt( c_basekb, c_universalvocabularymt ) }.
% 0.72/1.08 { genls( c_tptpcol_4_106497, c_tptpcol_3_98305 ) }.
% 0.72/1.08 { ! tptpcol_4_106497( X ), tptpcol_3_98305( X ) }.
% 0.72/1.08 { genls( c_tptpcol_5_110593, c_tptpcol_4_106497 ) }.
% 0.72/1.08 { ! tptpcol_5_110593( X ), tptpcol_4_106497( X ) }.
% 0.72/1.08 { genls( c_tptpcol_6_112641, c_tptpcol_5_110593 ) }.
% 0.72/1.08 { ! tptpcol_6_112641( X ), tptpcol_5_110593( X ) }.
% 0.72/1.08 { genls( c_tptpcol_7_113665, c_tptpcol_6_112641 ) }.
% 0.72/1.08 { ! tptpcol_7_113665( X ), tptpcol_6_112641( X ) }.
% 0.72/1.08 { genls( c_tptpcol_8_114177, c_tptpcol_7_113665 ) }.
% 0.72/1.08 { ! tptpcol_8_114177( X ), tptpcol_7_113665( X ) }.
% 0.72/1.08 { genls( c_tptpcol_4_114689, c_tptpcol_3_114688 ) }.
% 0.72/1.08 { ! tptpcol_4_114689( X ), tptpcol_3_114688( X ) }.
% 0.72/1.08 { genls( c_tptpcol_5_114690, c_tptpcol_4_114689 ) }.
% 0.72/1.08 { ! tptpcol_5_114690( X ), tptpcol_4_114689( X ) }.
% 0.72/1.08 { genls( c_tptpcol_6_116738, c_tptpcol_5_114690 ) }.
% 0.72/1.08 { ! tptpcol_6_116738( X ), tptpcol_5_114690( X ) }.
% 0.72/1.08 { genls( c_tptpcol_7_117762, c_tptpcol_6_116738 ) }.
% 0.72/1.08 { ! tptpcol_7_117762( X ), tptpcol_6_116738( X ) }.
% 0.72/1.08 { genls( c_tptpcol_8_117763, c_tptpcol_7_117762 ) }.
% 0.72/1.08 { ! tptpcol_8_117763( X ), tptpcol_7_117762( X ) }.
% 0.72/1.08 { genls( c_tptpcol_9_118019, c_tptpcol_8_117763 ) }.
% 0.72/1.08 { ! tptpcol_9_118019( X ), tptpcol_8_117763( X ) }.
% 0.72/1.08 { genls( c_tptpcol_10_118020, c_tptpcol_9_118019 ) }.
% 0.72/1.08 { ! tptpcol_10_118020( X ), tptpcol_9_118019( X ) }.
% 0.72/1.08 { genls( c_tptpcol_11_118084, c_tptpcol_10_118020 ) }.
% 0.72/1.08 { ! tptpcol_11_118084( X ), tptpcol_10_118020( X ) }.
% 0.72/1.08 { genls( c_tptpcol_12_118116, c_tptpcol_11_118084 ) }.
% 0.72/1.08 { ! tptpcol_12_118116( X ), tptpcol_11_118084( X ) }.
% 0.72/1.08 { genls( c_tptpcol_13_118117, c_tptpcol_12_118116 ) }.
% 0.72/1.08 { ! tptpcol_13_118117( X ), tptpcol_12_118116( X ) }.
% 0.72/1.08 { genls( c_tptpcol_14_118118, c_tptpcol_13_118117 ) }.
% 0.72/1.08 { ! tptpcol_14_118118( X ), tptpcol_13_118117( X ) }.
% 0.72/1.08 { disjointwith( c_tptpcol_3_98305, c_tptpcol_3_114688 ) }.
% 0.72/1.08 { ! tptpcol_3_98305( X ), ! tptpcol_3_114688( X ) }.
% 0.72/1.08 { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith( Y, Z ) }.
% 0.72/1.08 { ! genlinverse( X, Z ), ! genlinverse( Z, Y ), genlpreds( X, Y ) }.
% 0.72/1.08 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.72/1.08 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.72/1.08 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.72/1.08 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.72/1.08 { ! genlpreds( X, Z ), ! genlpreds( Z, Y ), genlpreds( X, Y ) }.
% 0.72/1.08 { ! predicate( X ), genlpreds( X, X ) }.
% 0.72/1.08 { ! predicate( X ), genlpreds( X, X ) }.
% 0.72/1.08 { ! genlinverse( Y, X ), binarypredicate( X ) }.
% 0.72/1.08 { ! genlinverse( X, Y ), binarypredicate( X ) }.
% 0.72/1.08 { ! genlinverse( Z, X ), ! genlpreds( Y, Z ), genlinverse( Y, X ) }.
% 0.72/1.08 { ! genlinverse( X, Z ), ! genlpreds( Z, Y ), genlinverse( X, Y ) }.
% 0.72/1.08 { ! disjointwith( Y, X ), collection( X ) }.
% 0.72/1.08 { ! disjointwith( X, Y ), collection( X ) }.
% 0.72/1.08 { ! disjointwith( X, Y ), disjointwith( Y, X ) }.
% 0.72/1.08 { ! disjointwith( X, Z ), ! genls( Y, Z ), disjointwith( X, Y ) }.
% 0.72/1.08 { ! disjointwith( Z, X ), ! genls( Y, Z ), disjointwith( Y, X ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_14_118118 ), tptpcol_14_118118( X ) }.
% 0.72/1.08 { ! tptpcol_14_118118( X ), isa( X, c_tptpcol_14_118118 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_13_118117 ), tptpcol_13_118117( X ) }.
% 0.72/1.08 { ! tptpcol_13_118117( X ), isa( X, c_tptpcol_13_118117 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_12_118116 ), tptpcol_12_118116( X ) }.
% 0.72/1.08 { ! tptpcol_12_118116( X ), isa( X, c_tptpcol_12_118116 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_11_118084 ), tptpcol_11_118084( X ) }.
% 0.72/1.08 { ! tptpcol_11_118084( X ), isa( X, c_tptpcol_11_118084 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_10_118020 ), tptpcol_10_118020( X ) }.
% 0.72/1.08 { ! tptpcol_10_118020( X ), isa( X, c_tptpcol_10_118020 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_9_118019 ), tptpcol_9_118019( X ) }.
% 0.72/1.08 { ! tptpcol_9_118019( X ), isa( X, c_tptpcol_9_118019 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_8_117763 ), tptpcol_8_117763( X ) }.
% 0.72/1.08 { ! tptpcol_8_117763( X ), isa( X, c_tptpcol_8_117763 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_7_117762 ), tptpcol_7_117762( X ) }.
% 0.72/1.08 { ! tptpcol_7_117762( X ), isa( X, c_tptpcol_7_117762 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_6_116738 ), tptpcol_6_116738( X ) }.
% 0.72/1.08 { ! tptpcol_6_116738( X ), isa( X, c_tptpcol_6_116738 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_5_114690 ), tptpcol_5_114690( X ) }.
% 0.72/1.08 { ! tptpcol_5_114690( X ), isa( X, c_tptpcol_5_114690 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_3_114688 ), tptpcol_3_114688( X ) }.
% 0.72/1.08 { ! tptpcol_3_114688( X ), isa( X, c_tptpcol_3_114688 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_4_114689 ), tptpcol_4_114689( X ) }.
% 0.72/1.08 { ! tptpcol_4_114689( X ), isa( X, c_tptpcol_4_114689 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_8_114177 ), tptpcol_8_114177( X ) }.
% 0.72/1.08 { ! tptpcol_8_114177( X ), isa( X, c_tptpcol_8_114177 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_7_113665 ), tptpcol_7_113665( X ) }.
% 0.72/1.08 { ! tptpcol_7_113665( X ), isa( X, c_tptpcol_7_113665 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_6_112641 ), tptpcol_6_112641( X ) }.
% 0.72/1.08 { ! tptpcol_6_112641( X ), isa( X, c_tptpcol_6_112641 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_5_110593 ), tptpcol_5_110593( X ) }.
% 0.72/1.08 { ! tptpcol_5_110593( X ), isa( X, c_tptpcol_5_110593 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_3_98305 ), tptpcol_3_98305( X ) }.
% 0.72/1.08 { ! tptpcol_3_98305( X ), isa( X, c_tptpcol_3_98305 ) }.
% 0.72/1.08 { ! isa( X, c_tptpcol_4_106497 ), tptpcol_4_106497( X ) }.
% 0.72/1.08 { ! tptpcol_4_106497( X ), isa( X, c_tptpcol_4_106497 ) }.
% 0.72/1.08 { ! genls( Y, X ), collection( X ) }.
% 0.72/1.08 { ! genls( Y, X ), collection( X ) }.
% 0.72/1.08 { ! genls( X, Y ), collection( X ) }.
% 0.72/1.08 { ! genls( X, Y ), collection( X ) }.
% 0.72/1.08 { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y ) }.
% 0.72/1.08 { ! collection( X ), genls( X, X ) }.
% 0.72/1.08 { ! collection( X ), genls( X, X ) }.
% 0.72/1.08 { ! genls( Z, X ), ! genls( Y, Z ), genls( Y, X ) }.
% 0.72/1.08 { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y ) }.
% 0.72/1.08 { mtvisible( c_basekb ) }.
% 0.72/1.08 { ! isa( X, c_transitivebinarypredicate ), transitivebinarypredicate( X ) }
% 0.72/1.08 .
% 0.72/1.08 { ! transitivebinarypredicate( X ), isa( X, c_transitivebinarypredicate ) }
% 0.72/1.08 .
% 0.72/1.08 { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible( X ) }.
% 0.72/1.08 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.72/1.08 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.72/1.08 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.72/1.08 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.72/1.08 { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X, Y ) }.
% 0.72/1.08 { ! microtheory( X ), genlmt( X, X ) }.
% 0.72/1.08 { ! microtheory( X ), genlmt( X, X ) }.
% 0.72/1.08 { ! isa( Y, X ), collection( X ) }.
% 0.72/1.08 { ! isa( Y, X ), collection( X ) }.
% 0.72/1.08 { ! isa( X, Y ), thing( X ) }.
% 0.72/1.08 { ! isa( X, Y ), thing( X ) }.
% 0.72/1.08 { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y ) }.
% 0.72/1.08 { mtvisible( c_universalvocabularymt ) }.
% 0.72/1.08 { mtvisible( c_timehasnoendmt ) }.
% 0.72/1.08 { ! disjointwith( c_tptpcol_8_114177, c_tptpcol_14_118118 ) }.
% 0.72/1.08
% 0.72/1.08 percentage equality = 0.000000, percentage horn = 1.000000
% 0.72/1.08 This is a near-Horn, non-equality problem
% 0.72/1.08
% 0.72/1.08
% 0.72/1.08 Options Used:
% 0.72/1.08
% 0.72/1.08 useres = 1
% 0.72/1.08 useparamod = 0
% 0.72/1.08 useeqrefl = 0
% 0.72/1.08 useeqfact = 0
% 0.72/1.08 usefactor = 1
% 0.72/1.08 usesimpsplitting = 0
% 0.72/1.08 usesimpdemod = 0
% 0.72/1.08 usesimpres = 4
% 0.72/1.08
% 0.72/1.08 resimpinuse = 1000
% 0.72/1.08 resimpclauses = 20000
% 0.72/1.08 substype = standard
% 0.72/1.08 backwardsubs = 1
% 0.72/1.08 selectoldest = 5
% 0.72/1.08
% 0.72/1.08 litorderings [0] = split
% 0.72/1.08 litorderings [1] = liftord
% 0.72/1.08
% 0.72/1.08 termordering = none
% 0.72/1.08
% 0.72/1.08 litapriori = 1
% 0.72/1.08 termapriori = 0
% 0.72/1.08 litaposteriori = 0
% 0.72/1.08 termaposteriori = 0
% 0.72/1.08 demodaposteriori = 0
% 0.72/1.08 ordereqreflfact = 0
% 0.72/1.08
% 0.72/1.08 litselect = negative
% 0.72/1.08
% 0.72/1.08 maxweight = 30000
% 0.72/1.08 maxdepth = 30000
% 0.72/1.08 maxlength = 115
% 0.72/1.08 maxnrvars = 195
% 0.72/1.08 excuselevel = 0
% 0.72/1.08 increasemaxweight = 0
% 0.72/1.08
% 0.72/1.08 maxselected = 10000000
% 0.72/1.08 maxnrclauses = 10000000
% 0.72/1.08
% 0.72/1.08 showgenerated = 0
% 0.72/1.08 showkept = 0
% 0.72/1.08 showselected = 0
% 0.72/1.08 showdeleted = 0
% 0.72/1.08 showresimp = 1
% 0.72/1.08 showstatus = 2000
% 0.72/1.08
% 0.72/1.08 prologoutput = 0
% 0.72/1.08 nrgoals = 5000000
% 0.72/1.08 totalproof = 1
% 0.72/1.08
% 0.72/1.08 Symbols occurring in the translation:
% 0.72/1.08
% 0.72/1.08 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.72/1.08 . [1, 2] (w:1, o:76, a:1, s:1, b:0),
% 0.72/1.08 ! [4, 1] (w:1, o:46, a:1, s:1, b:0),
% 0.72/1.08 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.08 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.08 c_genlmt [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.72/1.08 transitivebinarypredicate [36, 1] (w:1, o:51, a:1, s:1, b:0),
% 0.72/1.08 c_generictemporalmt [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.72/1.08 c_basekb [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.72/1.08 genlmt [39, 2] (w:1, o:100, a:1, s:1, b:0),
% 0.72/1.08 c_timehasnoendmt [40, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.72/1.08 c_universalvocabularymt [41, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_4_106497 [42, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_3_98305 [43, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.72/1.08 genls [44, 2] (w:1, o:101, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_4_106497 [46, 1] (w:1, o:54, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_3_98305 [47, 1] (w:1, o:52, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_5_110593 [48, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_5_110593 [49, 1] (w:1, o:56, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_6_112641 [50, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_6_112641 [51, 1] (w:1, o:58, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_7_113665 [52, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_7_113665 [53, 1] (w:1, o:60, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_8_114177 [54, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_8_114177 [55, 1] (w:1, o:62, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_4_114689 [56, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.72/1.08 c_tptpcol_3_114688 [57, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.72/1.08 tptpcol_4_114689 [58, 1] (w:1, o:55, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_3_114688 [59, 1] (w:1, o:53, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_5_114690 [60, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_5_114690 [61, 1] (w:1, o:57, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_6_116738 [62, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_6_116738 [63, 1] (w:1, o:59, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_7_117762 [64, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_7_117762 [65, 1] (w:1, o:61, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_8_117763 [66, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_8_117763 [67, 1] (w:1, o:63, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_9_118019 [68, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_9_118019 [69, 1] (w:1, o:64, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_10_118020 [70, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_10_118020 [71, 1] (w:1, o:65, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_11_118084 [72, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_11_118084 [73, 1] (w:1, o:66, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_12_118116 [74, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_12_118116 [75, 1] (w:1, o:67, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_13_118117 [76, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_13_118117 [77, 1] (w:1, o:68, a:1, s:1, b:0),
% 0.72/1.09 c_tptpcol_14_118118 [78, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.72/1.09 tptpcol_14_118118 [79, 1] (w:1, o:69, a:1, s:1, b:0),
% 0.72/1.09 disjointwith [80, 2] (w:1, o:102, a:1, s:1, b:0),
% 0.72/1.09 isa [83, 2] (w:1, o:103, a:1, s:1, b:0),
% 0.72/1.09 genlinverse [87, 2] (w:1, o:104, a:1, s:1, b:0),
% 0.72/1.09 genlpreds [88, 2] (w:1, o:105, a:1, s:1, b:0),
% 0.72/1.09 predicate [91, 1] (w:1, o:70, a:1, s:1, b:0),
% 0.72/1.09 binarypredicate [96, 1] (w:1, o:71, a:1, s:1, b:0),
% 0.72/1.09 collection [99, 1] (w:1, o:72, a:1, s:1, b:0),
% 0.72/1.09 mtvisible [100, 1] (w:1, o:73, a:1, s:1, b:0),
% 0.72/1.09 c_transitivebinarypredicate [101, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.72/1.09 microtheory [104, 1] (w:1, o:74, a:1, s:1, b:0),
% 0.72/1.09 thing [105, 1] (w:1, o:75, a:1, s:1, b:0).
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 Starting Search:
% 0.72/1.09
% 0.72/1.09 *** allocated 15000 integers for clauses
% 0.72/1.09 *** allocated 22500 integers for clauses
% 0.72/1.09
% 0.72/1.09 Bliksems!, er is een bewijs:
% 0.72/1.09 % SZS status Theorem
% 0.72/1.09 % SZS output start Refutation
% 0.72/1.09
% 0.72/1.09 (4) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_106497, c_tptpcol_3_98305 )
% 0.72/1.09 }.
% 0.72/1.09 (6) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_110593, c_tptpcol_4_106497 )
% 0.72/1.09 }.
% 0.72/1.09 (8) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_112641, c_tptpcol_5_110593 )
% 0.72/1.09 }.
% 0.72/1.09 (10) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_113665, c_tptpcol_6_112641
% 0.72/1.09 ) }.
% 0.72/1.09 (12) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_114177, c_tptpcol_7_113665
% 0.72/1.09 ) }.
% 0.72/1.09 (14) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_114689, c_tptpcol_3_114688
% 0.72/1.09 ) }.
% 0.72/1.09 (16) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_114690, c_tptpcol_4_114689
% 0.72/1.09 ) }.
% 0.72/1.09 (18) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_116738, c_tptpcol_5_114690
% 0.72/1.09 ) }.
% 0.72/1.09 (20) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_117762, c_tptpcol_6_116738
% 0.72/1.09 ) }.
% 0.72/1.09 (22) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_117763, c_tptpcol_7_117762
% 0.72/1.09 ) }.
% 0.72/1.09 (24) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_118019, c_tptpcol_8_117763
% 0.72/1.09 ) }.
% 0.72/1.09 (26) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_118020, c_tptpcol_9_118019
% 0.72/1.09 ) }.
% 0.72/1.09 (28) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_118084,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 (30) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_118116,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 (32) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_118117,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 (34) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_118118,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 (36) {G0,W3,D2,L1,V0,M1} I { disjointwith( c_tptpcol_3_98305,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 (50) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), ! disjointwith( X, Y )
% 0.72/1.09 }.
% 0.72/1.09 (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ), disjointwith( X, Y )
% 0.72/1.09 , ! genls( Y, Z ) }.
% 0.72/1.09 (52) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( Z, X ), disjointwith( Y, X )
% 0.72/1.09 , ! genls( Y, Z ) }.
% 0.72/1.09 (106) {G0,W4,D2,L1,V0,M1} I { ! disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_14_118118 ) }.
% 0.72/1.09 (139) {G1,W3,D2,L1,V0,M1} R(50,36) { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 (159) {G1,W7,D2,L2,V1,M1} R(51,6) { disjointwith( X, c_tptpcol_5_110593 ),
% 0.72/1.09 ! disjointwith( X, c_tptpcol_4_106497 ) }.
% 0.72/1.09 (160) {G1,W7,D2,L2,V1,M1} R(51,8) { disjointwith( X, c_tptpcol_6_112641 ),
% 0.72/1.09 ! disjointwith( X, c_tptpcol_5_110593 ) }.
% 0.72/1.09 (162) {G1,W7,D2,L2,V1,M1} R(51,4) { disjointwith( X, c_tptpcol_4_106497 ),
% 0.72/1.09 ! disjointwith( X, c_tptpcol_3_98305 ) }.
% 0.72/1.09 (163) {G1,W7,D2,L2,V1,M1} R(51,12) { disjointwith( X, c_tptpcol_8_114177 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_7_113665 ) }.
% 0.72/1.09 (164) {G1,W7,D2,L2,V1,M1} R(51,14) { disjointwith( X, c_tptpcol_4_114689 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_3_114688 ) }.
% 0.72/1.09 (165) {G1,W7,D2,L2,V1,M1} R(51,16) { disjointwith( X, c_tptpcol_5_114690 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_4_114689 ) }.
% 0.72/1.09 (166) {G1,W7,D2,L2,V1,M1} R(51,18) { disjointwith( X, c_tptpcol_6_116738 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_5_114690 ) }.
% 0.72/1.09 (167) {G1,W7,D2,L2,V1,M1} R(51,20) { disjointwith( X, c_tptpcol_7_117762 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_6_116738 ) }.
% 0.72/1.09 (168) {G1,W7,D2,L2,V1,M1} R(51,22) { disjointwith( X, c_tptpcol_8_117763 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_7_117762 ) }.
% 0.72/1.09 (169) {G1,W7,D2,L2,V1,M1} R(51,24) { disjointwith( X, c_tptpcol_9_118019 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_8_117763 ) }.
% 0.72/1.09 (170) {G1,W7,D2,L2,V1,M1} R(51,26) { disjointwith( X, c_tptpcol_10_118020 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_9_118019 ) }.
% 0.72/1.09 (171) {G1,W7,D2,L2,V1,M1} R(51,28) { disjointwith( X, c_tptpcol_11_118084 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_10_118020 ) }.
% 0.72/1.09 (172) {G1,W7,D2,L2,V1,M1} R(51,30) { disjointwith( X, c_tptpcol_12_118116 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_11_118084 ) }.
% 0.72/1.09 (173) {G1,W7,D2,L2,V1,M1} R(51,32) { disjointwith( X, c_tptpcol_13_118117 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_12_118116 ) }.
% 0.72/1.09 (174) {G1,W7,D2,L2,V1,M1} R(51,34) { disjointwith( X, c_tptpcol_14_118118 )
% 0.72/1.09 , ! disjointwith( X, c_tptpcol_13_118117 ) }.
% 0.72/1.09 (177) {G1,W7,D2,L2,V1,M1} R(52,10) { disjointwith( c_tptpcol_7_113665, X )
% 0.72/1.09 , ! disjointwith( c_tptpcol_6_112641, X ) }.
% 0.72/1.09 (248) {G2,W3,D2,L1,V0,M1} R(162,139) { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 (251) {G3,W3,D2,L1,V0,M1} R(248,159) { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 (258) {G4,W3,D2,L1,V0,M1} R(251,160) { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 (261) {G5,W3,D2,L1,V0,M1} R(258,50) { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 (263) {G6,W3,D2,L1,V0,M1} R(164,261) { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 (273) {G7,W3,D2,L1,V0,M1} R(165,263) { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 (274) {G8,W3,D2,L1,V0,M1} R(273,177) { disjointwith( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 (282) {G9,W3,D2,L1,V0,M1} R(166,274) { disjointwith( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 (284) {G10,W3,D2,L1,V0,M1} R(282,50) { disjointwith( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 (286) {G11,W3,D2,L1,V0,M1} R(284,163) { disjointwith( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_8_114177 ) }.
% 0.72/1.09 (287) {G12,W3,D2,L1,V0,M1} R(286,50) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 (289) {G13,W3,D2,L1,V0,M1} R(167,287) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 (296) {G14,W3,D2,L1,V0,M1} R(168,289) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 (301) {G15,W3,D2,L1,V0,M1} R(169,296) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 (308) {G16,W3,D2,L1,V0,M1} R(170,301) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 (313) {G17,W3,D2,L1,V0,M1} R(171,308) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 (320) {G18,W3,D2,L1,V0,M1} R(172,313) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 (325) {G19,W3,D2,L1,V0,M1} R(173,320) { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 (332) {G20,W0,D0,L0,V0,M0} R(174,325);r(106) { }.
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 % SZS output end Refutation
% 0.72/1.09 found a proof!
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 Unprocessed initial clauses:
% 0.72/1.09
% 0.72/1.09 (334) {G0,W2,D2,L1,V0,M1} { transitivebinarypredicate( c_genlmt ) }.
% 0.72/1.09 (335) {G0,W3,D2,L1,V0,M1} { genlmt( c_generictemporalmt, c_basekb ) }.
% 0.72/1.09 (336) {G0,W3,D2,L1,V0,M1} { genlmt( c_timehasnoendmt, c_generictemporalmt
% 0.72/1.09 ) }.
% 0.72/1.09 (337) {G0,W3,D2,L1,V0,M1} { genlmt( c_basekb, c_universalvocabularymt )
% 0.72/1.09 }.
% 0.72/1.09 (338) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_106497, c_tptpcol_3_98305 )
% 0.72/1.09 }.
% 0.72/1.09 (339) {G0,W5,D2,L2,V1,M2} { ! tptpcol_4_106497( X ), tptpcol_3_98305( X )
% 0.72/1.09 }.
% 0.72/1.09 (340) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_110593, c_tptpcol_4_106497
% 0.72/1.09 ) }.
% 0.72/1.09 (341) {G0,W5,D2,L2,V1,M2} { ! tptpcol_5_110593( X ), tptpcol_4_106497( X )
% 0.72/1.09 }.
% 0.72/1.09 (342) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_112641, c_tptpcol_5_110593
% 0.72/1.09 ) }.
% 0.72/1.09 (343) {G0,W5,D2,L2,V1,M2} { ! tptpcol_6_112641( X ), tptpcol_5_110593( X )
% 0.72/1.09 }.
% 0.72/1.09 (344) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_113665, c_tptpcol_6_112641
% 0.72/1.09 ) }.
% 0.72/1.09 (345) {G0,W5,D2,L2,V1,M2} { ! tptpcol_7_113665( X ), tptpcol_6_112641( X )
% 0.72/1.09 }.
% 0.72/1.09 (346) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_114177, c_tptpcol_7_113665
% 0.72/1.09 ) }.
% 0.72/1.09 (347) {G0,W5,D2,L2,V1,M2} { ! tptpcol_8_114177( X ), tptpcol_7_113665( X )
% 0.72/1.09 }.
% 0.72/1.09 (348) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_114689, c_tptpcol_3_114688
% 0.72/1.09 ) }.
% 0.72/1.09 (349) {G0,W5,D2,L2,V1,M2} { ! tptpcol_4_114689( X ), tptpcol_3_114688( X )
% 0.72/1.09 }.
% 0.72/1.09 (350) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_114690, c_tptpcol_4_114689
% 0.72/1.09 ) }.
% 0.72/1.09 (351) {G0,W5,D2,L2,V1,M2} { ! tptpcol_5_114690( X ), tptpcol_4_114689( X )
% 0.72/1.09 }.
% 0.72/1.09 (352) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_116738, c_tptpcol_5_114690
% 0.72/1.09 ) }.
% 0.72/1.09 (353) {G0,W5,D2,L2,V1,M2} { ! tptpcol_6_116738( X ), tptpcol_5_114690( X )
% 0.72/1.09 }.
% 0.72/1.09 (354) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_117762, c_tptpcol_6_116738
% 0.72/1.09 ) }.
% 0.72/1.09 (355) {G0,W5,D2,L2,V1,M2} { ! tptpcol_7_117762( X ), tptpcol_6_116738( X )
% 0.72/1.09 }.
% 0.72/1.09 (356) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_117763, c_tptpcol_7_117762
% 0.72/1.09 ) }.
% 0.72/1.09 (357) {G0,W5,D2,L2,V1,M2} { ! tptpcol_8_117763( X ), tptpcol_7_117762( X )
% 0.72/1.09 }.
% 0.72/1.09 (358) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_118019, c_tptpcol_8_117763
% 0.72/1.09 ) }.
% 0.72/1.09 (359) {G0,W5,D2,L2,V1,M2} { ! tptpcol_9_118019( X ), tptpcol_8_117763( X )
% 0.72/1.09 }.
% 0.72/1.09 (360) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_118020, c_tptpcol_9_118019
% 0.72/1.09 ) }.
% 0.72/1.09 (361) {G0,W5,D2,L2,V1,M2} { ! tptpcol_10_118020( X ), tptpcol_9_118019( X
% 0.72/1.09 ) }.
% 0.72/1.09 (362) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_118084,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 (363) {G0,W5,D2,L2,V1,M2} { ! tptpcol_11_118084( X ), tptpcol_10_118020( X
% 0.72/1.09 ) }.
% 0.72/1.09 (364) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_118116,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 (365) {G0,W5,D2,L2,V1,M2} { ! tptpcol_12_118116( X ), tptpcol_11_118084( X
% 0.72/1.09 ) }.
% 0.72/1.09 (366) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_118117,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 (367) {G0,W5,D2,L2,V1,M2} { ! tptpcol_13_118117( X ), tptpcol_12_118116( X
% 0.72/1.09 ) }.
% 0.72/1.09 (368) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_118118,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 (369) {G0,W5,D2,L2,V1,M2} { ! tptpcol_14_118118( X ), tptpcol_13_118117( X
% 0.72/1.09 ) }.
% 0.72/1.09 (370) {G0,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_98305,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 (371) {G0,W6,D2,L2,V1,M2} { ! tptpcol_3_98305( X ), ! tptpcol_3_114688( X
% 0.72/1.09 ) }.
% 0.72/1.09 (372) {G0,W12,D2,L3,V3,M3} { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith
% 0.72/1.09 ( Y, Z ) }.
% 0.72/1.09 (373) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlinverse( Z, Y )
% 0.72/1.09 , genlpreds( X, Y ) }.
% 0.72/1.09 (374) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.72/1.09 (375) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.72/1.09 (376) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.72/1.09 (377) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.72/1.09 (378) {G0,W11,D2,L3,V3,M3} { ! genlpreds( X, Z ), ! genlpreds( Z, Y ),
% 0.72/1.09 genlpreds( X, Y ) }.
% 0.72/1.09 (379) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.72/1.09 (380) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.72/1.09 (381) {G0,W6,D2,L2,V2,M2} { ! genlinverse( Y, X ), binarypredicate( X )
% 0.72/1.09 }.
% 0.72/1.09 (382) {G0,W6,D2,L2,V2,M2} { ! genlinverse( X, Y ), binarypredicate( X )
% 0.72/1.09 }.
% 0.72/1.09 (383) {G0,W11,D2,L3,V3,M3} { ! genlinverse( Z, X ), ! genlpreds( Y, Z ),
% 0.72/1.09 genlinverse( Y, X ) }.
% 0.72/1.09 (384) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlpreds( Z, Y ),
% 0.72/1.09 genlinverse( X, Y ) }.
% 0.72/1.09 (385) {G0,W6,D2,L2,V2,M2} { ! disjointwith( Y, X ), collection( X ) }.
% 0.72/1.09 (386) {G0,W6,D2,L2,V2,M2} { ! disjointwith( X, Y ), collection( X ) }.
% 0.72/1.09 (387) {G0,W7,D2,L2,V2,M2} { ! disjointwith( X, Y ), disjointwith( Y, X )
% 0.72/1.09 }.
% 0.72/1.09 (388) {G0,W11,D2,L3,V3,M3} { ! disjointwith( X, Z ), ! genls( Y, Z ),
% 0.72/1.09 disjointwith( X, Y ) }.
% 0.72/1.09 (389) {G0,W11,D2,L3,V3,M3} { ! disjointwith( Z, X ), ! genls( Y, Z ),
% 0.72/1.09 disjointwith( Y, X ) }.
% 0.72/1.09 (390) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_14_118118 ),
% 0.72/1.09 tptpcol_14_118118( X ) }.
% 0.72/1.09 (391) {G0,W6,D2,L2,V1,M2} { ! tptpcol_14_118118( X ), isa( X,
% 0.72/1.09 c_tptpcol_14_118118 ) }.
% 0.72/1.09 (392) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_13_118117 ),
% 0.72/1.09 tptpcol_13_118117( X ) }.
% 0.72/1.09 (393) {G0,W6,D2,L2,V1,M2} { ! tptpcol_13_118117( X ), isa( X,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 (394) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_12_118116 ),
% 0.72/1.09 tptpcol_12_118116( X ) }.
% 0.72/1.09 (395) {G0,W6,D2,L2,V1,M2} { ! tptpcol_12_118116( X ), isa( X,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 (396) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_11_118084 ),
% 0.72/1.09 tptpcol_11_118084( X ) }.
% 0.72/1.09 (397) {G0,W6,D2,L2,V1,M2} { ! tptpcol_11_118084( X ), isa( X,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 (398) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_10_118020 ),
% 0.72/1.09 tptpcol_10_118020( X ) }.
% 0.72/1.09 (399) {G0,W6,D2,L2,V1,M2} { ! tptpcol_10_118020( X ), isa( X,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 (400) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_9_118019 ),
% 0.72/1.09 tptpcol_9_118019( X ) }.
% 0.72/1.09 (401) {G0,W6,D2,L2,V1,M2} { ! tptpcol_9_118019( X ), isa( X,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 (402) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_8_117763 ),
% 0.72/1.09 tptpcol_8_117763( X ) }.
% 0.72/1.09 (403) {G0,W6,D2,L2,V1,M2} { ! tptpcol_8_117763( X ), isa( X,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 (404) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_7_117762 ),
% 0.72/1.09 tptpcol_7_117762( X ) }.
% 0.72/1.09 (405) {G0,W6,D2,L2,V1,M2} { ! tptpcol_7_117762( X ), isa( X,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 (406) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_6_116738 ),
% 0.72/1.09 tptpcol_6_116738( X ) }.
% 0.72/1.09 (407) {G0,W6,D2,L2,V1,M2} { ! tptpcol_6_116738( X ), isa( X,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 (408) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_5_114690 ),
% 0.72/1.09 tptpcol_5_114690( X ) }.
% 0.72/1.09 (409) {G0,W6,D2,L2,V1,M2} { ! tptpcol_5_114690( X ), isa( X,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 (410) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_3_114688 ),
% 0.72/1.09 tptpcol_3_114688( X ) }.
% 0.72/1.09 (411) {G0,W6,D2,L2,V1,M2} { ! tptpcol_3_114688( X ), isa( X,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 (412) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_4_114689 ),
% 0.72/1.09 tptpcol_4_114689( X ) }.
% 0.72/1.09 (413) {G0,W6,D2,L2,V1,M2} { ! tptpcol_4_114689( X ), isa( X,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 (414) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_8_114177 ),
% 0.72/1.09 tptpcol_8_114177( X ) }.
% 0.72/1.09 (415) {G0,W6,D2,L2,V1,M2} { ! tptpcol_8_114177( X ), isa( X,
% 0.72/1.09 c_tptpcol_8_114177 ) }.
% 0.72/1.09 (416) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_7_113665 ),
% 0.72/1.09 tptpcol_7_113665( X ) }.
% 0.72/1.09 (417) {G0,W6,D2,L2,V1,M2} { ! tptpcol_7_113665( X ), isa( X,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 (418) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_6_112641 ),
% 0.72/1.09 tptpcol_6_112641( X ) }.
% 0.72/1.09 (419) {G0,W6,D2,L2,V1,M2} { ! tptpcol_6_112641( X ), isa( X,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 (420) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_5_110593 ),
% 0.72/1.09 tptpcol_5_110593( X ) }.
% 0.72/1.09 (421) {G0,W6,D2,L2,V1,M2} { ! tptpcol_5_110593( X ), isa( X,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 (422) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_3_98305 ), tptpcol_3_98305
% 0.72/1.09 ( X ) }.
% 0.72/1.09 (423) {G0,W6,D2,L2,V1,M2} { ! tptpcol_3_98305( X ), isa( X,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 (424) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_4_106497 ),
% 0.72/1.09 tptpcol_4_106497( X ) }.
% 0.72/1.09 (425) {G0,W6,D2,L2,V1,M2} { ! tptpcol_4_106497( X ), isa( X,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 (426) {G0,W6,D2,L2,V2,M2} { ! genls( Y, X ), collection( X ) }.
% 0.72/1.09 (427) {G0,W6,D2,L2,V2,M2} { ! genls( Y, X ), collection( X ) }.
% 0.72/1.09 (428) {G0,W6,D2,L2,V2,M2} { ! genls( X, Y ), collection( X ) }.
% 0.72/1.09 (429) {G0,W6,D2,L2,V2,M2} { ! genls( X, Y ), collection( X ) }.
% 0.72/1.09 (430) {G0,W11,D2,L3,V3,M3} { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y
% 0.72/1.09 ) }.
% 0.72/1.09 (431) {G0,W6,D2,L2,V1,M2} { ! collection( X ), genls( X, X ) }.
% 0.72/1.09 (432) {G0,W6,D2,L2,V1,M2} { ! collection( X ), genls( X, X ) }.
% 0.72/1.09 (433) {G0,W11,D2,L3,V3,M3} { ! genls( Z, X ), ! genls( Y, Z ), genls( Y, X
% 0.72/1.09 ) }.
% 0.72/1.09 (434) {G0,W11,D2,L3,V3,M3} { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y
% 0.72/1.09 ) }.
% 0.72/1.09 (435) {G0,W2,D2,L1,V0,M1} { mtvisible( c_basekb ) }.
% 0.72/1.09 (436) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_transitivebinarypredicate ),
% 0.72/1.09 transitivebinarypredicate( X ) }.
% 0.72/1.09 (437) {G0,W6,D2,L2,V1,M2} { ! transitivebinarypredicate( X ), isa( X,
% 0.72/1.09 c_transitivebinarypredicate ) }.
% 0.72/1.09 (438) {G0,W9,D2,L3,V2,M3} { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible
% 0.72/1.09 ( X ) }.
% 0.72/1.09 (439) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.72/1.09 (440) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.72/1.09 (441) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.72/1.09 (442) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.72/1.09 (443) {G0,W11,D2,L3,V3,M3} { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X
% 0.72/1.09 , Y ) }.
% 0.72/1.09 (444) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.72/1.09 (445) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.72/1.09 (446) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.72/1.09 (447) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.72/1.09 (448) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.72/1.09 (449) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.72/1.09 (450) {G0,W11,D2,L3,V3,M3} { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y )
% 0.72/1.09 }.
% 0.72/1.09 (451) {G0,W2,D2,L1,V0,M1} { mtvisible( c_universalvocabularymt ) }.
% 0.72/1.09 (452) {G0,W2,D2,L1,V0,M1} { mtvisible( c_timehasnoendmt ) }.
% 0.72/1.09 (453) {G0,W4,D2,L1,V0,M1} { ! disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_14_118118 ) }.
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 Total Proof:
% 0.72/1.09
% 0.72/1.09 subsumption: (4) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_106497,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 parent0: (338) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_106497,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (6) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_110593,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 parent0: (340) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_110593,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (8) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 parent0: (342) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (10) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 parent0: (344) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (12) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 parent0: (346) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (14) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_114689,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 parent0: (348) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_114689,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (16) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_114690,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 parent0: (350) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_114690,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (18) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0: (352) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (20) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_117762,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0: (354) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_117762,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (22) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_117763,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 parent0: (356) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_117763,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (24) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_118019,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 parent0: (358) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_118019,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (26) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_118020,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 parent0: (360) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_118020,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (28) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_118084,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 parent0: (362) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_118084,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (30) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_118116,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 parent0: (364) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_118116,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (32) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_118117,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 parent0: (366) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_118117,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (34) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_118118,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 parent0: (368) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_118118,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (36) {G0,W3,D2,L1,V0,M1} I { disjointwith( c_tptpcol_3_98305,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 parent0: (370) {G0,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_98305,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (50) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.72/1.09 disjointwith( X, Y ) }.
% 0.72/1.09 parent0: (387) {G0,W7,D2,L2,V2,M2} { ! disjointwith( X, Y ), disjointwith
% 0.72/1.09 ( Y, X ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := Y
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent0: (388) {G0,W11,D2,L3,V3,M3} { ! disjointwith( X, Z ), ! genls( Y,
% 0.72/1.09 Z ), disjointwith( X, Y ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := Y
% 0.72/1.09 Z := Z
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 1 ==> 2
% 0.72/1.09 2 ==> 1
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (52) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( Z, X ),
% 0.72/1.09 disjointwith( Y, X ), ! genls( Y, Z ) }.
% 0.72/1.09 parent0: (389) {G0,W11,D2,L3,V3,M3} { ! disjointwith( Z, X ), ! genls( Y,
% 0.72/1.09 Z ), disjointwith( Y, X ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := Y
% 0.72/1.09 Z := Z
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 1 ==> 2
% 0.72/1.09 2 ==> 1
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (106) {G0,W4,D2,L1,V0,M1} I { ! disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_14_118118 ) }.
% 0.72/1.09 parent0: (453) {G0,W4,D2,L1,V0,M1} { ! disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_14_118118 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (470) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 parent0[1]: (50) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.72/1.09 disjointwith( X, Y ) }.
% 0.72/1.09 parent1[0]: (36) {G0,W3,D2,L1,V0,M1} I { disjointwith( c_tptpcol_3_98305,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_3_98305
% 0.72/1.09 Y := c_tptpcol_3_114688
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (139) {G1,W3,D2,L1,V0,M1} R(50,36) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_3_98305 ) }.
% 0.72/1.09 parent0: (470) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (471) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_4_106497 ), disjointwith( X, c_tptpcol_5_110593 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (6) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_110593,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_5_110593
% 0.72/1.09 Z := c_tptpcol_4_106497
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (159) {G1,W7,D2,L2,V1,M1} R(51,6) { disjointwith( X,
% 0.72/1.09 c_tptpcol_5_110593 ), ! disjointwith( X, c_tptpcol_4_106497 ) }.
% 0.72/1.09 parent0: (471) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_4_106497
% 0.72/1.09 ), disjointwith( X, c_tptpcol_5_110593 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (472) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_5_110593 ), disjointwith( X, c_tptpcol_6_112641 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (8) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_6_112641
% 0.72/1.09 Z := c_tptpcol_5_110593
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (160) {G1,W7,D2,L2,V1,M1} R(51,8) { disjointwith( X,
% 0.72/1.09 c_tptpcol_6_112641 ), ! disjointwith( X, c_tptpcol_5_110593 ) }.
% 0.72/1.09 parent0: (472) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_5_110593
% 0.72/1.09 ), disjointwith( X, c_tptpcol_6_112641 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (473) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_3_98305 ), disjointwith( X, c_tptpcol_4_106497 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (4) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_106497,
% 0.72/1.09 c_tptpcol_3_98305 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_4_106497
% 0.72/1.09 Z := c_tptpcol_3_98305
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (162) {G1,W7,D2,L2,V1,M1} R(51,4) { disjointwith( X,
% 0.72/1.09 c_tptpcol_4_106497 ), ! disjointwith( X, c_tptpcol_3_98305 ) }.
% 0.72/1.09 parent0: (473) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_3_98305
% 0.72/1.09 ), disjointwith( X, c_tptpcol_4_106497 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (474) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_7_113665 ), disjointwith( X, c_tptpcol_8_114177 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (12) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_8_114177
% 0.72/1.09 Z := c_tptpcol_7_113665
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (163) {G1,W7,D2,L2,V1,M1} R(51,12) { disjointwith( X,
% 0.72/1.09 c_tptpcol_8_114177 ), ! disjointwith( X, c_tptpcol_7_113665 ) }.
% 0.72/1.09 parent0: (474) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_7_113665
% 0.72/1.09 ), disjointwith( X, c_tptpcol_8_114177 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (475) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_3_114688 ), disjointwith( X, c_tptpcol_4_114689 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (14) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_114689,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_4_114689
% 0.72/1.09 Z := c_tptpcol_3_114688
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (164) {G1,W7,D2,L2,V1,M1} R(51,14) { disjointwith( X,
% 0.72/1.09 c_tptpcol_4_114689 ), ! disjointwith( X, c_tptpcol_3_114688 ) }.
% 0.72/1.09 parent0: (475) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_3_114688
% 0.72/1.09 ), disjointwith( X, c_tptpcol_4_114689 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (476) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_4_114689 ), disjointwith( X, c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (16) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_114690,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_5_114690
% 0.72/1.09 Z := c_tptpcol_4_114689
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (165) {G1,W7,D2,L2,V1,M1} R(51,16) { disjointwith( X,
% 0.72/1.09 c_tptpcol_5_114690 ), ! disjointwith( X, c_tptpcol_4_114689 ) }.
% 0.72/1.09 parent0: (476) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_4_114689
% 0.72/1.09 ), disjointwith( X, c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (477) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_5_114690 ), disjointwith( X, c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (18) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_6_116738
% 0.72/1.09 Z := c_tptpcol_5_114690
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (166) {G1,W7,D2,L2,V1,M1} R(51,18) { disjointwith( X,
% 0.72/1.09 c_tptpcol_6_116738 ), ! disjointwith( X, c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0: (477) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_5_114690
% 0.72/1.09 ), disjointwith( X, c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (478) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_6_116738 ), disjointwith( X, c_tptpcol_7_117762 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (20) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_117762,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_7_117762
% 0.72/1.09 Z := c_tptpcol_6_116738
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (167) {G1,W7,D2,L2,V1,M1} R(51,20) { disjointwith( X,
% 0.72/1.09 c_tptpcol_7_117762 ), ! disjointwith( X, c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0: (478) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_6_116738
% 0.72/1.09 ), disjointwith( X, c_tptpcol_7_117762 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (479) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_7_117762 ), disjointwith( X, c_tptpcol_8_117763 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (22) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_117763,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_8_117763
% 0.72/1.09 Z := c_tptpcol_7_117762
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (168) {G1,W7,D2,L2,V1,M1} R(51,22) { disjointwith( X,
% 0.72/1.09 c_tptpcol_8_117763 ), ! disjointwith( X, c_tptpcol_7_117762 ) }.
% 0.72/1.09 parent0: (479) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_7_117762
% 0.72/1.09 ), disjointwith( X, c_tptpcol_8_117763 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (480) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_8_117763 ), disjointwith( X, c_tptpcol_9_118019 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (24) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_118019,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_9_118019
% 0.72/1.09 Z := c_tptpcol_8_117763
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (169) {G1,W7,D2,L2,V1,M1} R(51,24) { disjointwith( X,
% 0.72/1.09 c_tptpcol_9_118019 ), ! disjointwith( X, c_tptpcol_8_117763 ) }.
% 0.72/1.09 parent0: (480) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_8_117763
% 0.72/1.09 ), disjointwith( X, c_tptpcol_9_118019 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (481) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_9_118019 ), disjointwith( X, c_tptpcol_10_118020 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (26) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_118020,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_10_118020
% 0.72/1.09 Z := c_tptpcol_9_118019
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (170) {G1,W7,D2,L2,V1,M1} R(51,26) { disjointwith( X,
% 0.72/1.09 c_tptpcol_10_118020 ), ! disjointwith( X, c_tptpcol_9_118019 ) }.
% 0.72/1.09 parent0: (481) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_9_118019
% 0.72/1.09 ), disjointwith( X, c_tptpcol_10_118020 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (482) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_10_118020 ), disjointwith( X, c_tptpcol_11_118084 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (28) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_118084,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_11_118084
% 0.72/1.09 Z := c_tptpcol_10_118020
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (171) {G1,W7,D2,L2,V1,M1} R(51,28) { disjointwith( X,
% 0.72/1.09 c_tptpcol_11_118084 ), ! disjointwith( X, c_tptpcol_10_118020 ) }.
% 0.72/1.09 parent0: (482) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_10_118020 ), disjointwith( X, c_tptpcol_11_118084 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (483) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_11_118084 ), disjointwith( X, c_tptpcol_12_118116 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (30) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_118116,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_12_118116
% 0.72/1.09 Z := c_tptpcol_11_118084
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (172) {G1,W7,D2,L2,V1,M1} R(51,30) { disjointwith( X,
% 0.72/1.09 c_tptpcol_12_118116 ), ! disjointwith( X, c_tptpcol_11_118084 ) }.
% 0.72/1.09 parent0: (483) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_11_118084 ), disjointwith( X, c_tptpcol_12_118116 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (484) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_12_118116 ), disjointwith( X, c_tptpcol_13_118117 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (32) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_118117,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_13_118117
% 0.72/1.09 Z := c_tptpcol_12_118116
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (173) {G1,W7,D2,L2,V1,M1} R(51,32) { disjointwith( X,
% 0.72/1.09 c_tptpcol_13_118117 ), ! disjointwith( X, c_tptpcol_12_118116 ) }.
% 0.72/1.09 parent0: (484) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_12_118116 ), disjointwith( X, c_tptpcol_13_118117 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (485) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_13_118117 ), disjointwith( X, c_tptpcol_14_118118 ) }.
% 0.72/1.09 parent0[2]: (51) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.72/1.09 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (34) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_118118,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_14_118118
% 0.72/1.09 Z := c_tptpcol_13_118117
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (174) {G1,W7,D2,L2,V1,M1} R(51,34) { disjointwith( X,
% 0.72/1.09 c_tptpcol_14_118118 ), ! disjointwith( X, c_tptpcol_13_118117 ) }.
% 0.72/1.09 parent0: (485) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.72/1.09 c_tptpcol_13_118117 ), disjointwith( X, c_tptpcol_14_118118 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (486) {G1,W7,D2,L2,V1,M2} { ! disjointwith( c_tptpcol_6_112641
% 0.72/1.09 , X ), disjointwith( c_tptpcol_7_113665, X ) }.
% 0.72/1.09 parent0[2]: (52) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( Z, X ),
% 0.72/1.09 disjointwith( Y, X ), ! genls( Y, Z ) }.
% 0.72/1.09 parent1[0]: (10) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 Y := c_tptpcol_7_113665
% 0.72/1.09 Z := c_tptpcol_6_112641
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (177) {G1,W7,D2,L2,V1,M1} R(52,10) { disjointwith(
% 0.72/1.09 c_tptpcol_7_113665, X ), ! disjointwith( c_tptpcol_6_112641, X ) }.
% 0.72/1.09 parent0: (486) {G1,W7,D2,L2,V1,M2} { ! disjointwith( c_tptpcol_6_112641, X
% 0.72/1.09 ), disjointwith( c_tptpcol_7_113665, X ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := X
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 1
% 0.72/1.09 1 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (487) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 parent0[1]: (162) {G1,W7,D2,L2,V1,M1} R(51,4) { disjointwith( X,
% 0.72/1.09 c_tptpcol_4_106497 ), ! disjointwith( X, c_tptpcol_3_98305 ) }.
% 0.72/1.09 parent1[0]: (139) {G1,W3,D2,L1,V0,M1} R(50,36) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_3_98305 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_3_114688
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (248) {G2,W3,D2,L1,V0,M1} R(162,139) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_4_106497 ) }.
% 0.72/1.09 parent0: (487) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_4_106497 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (488) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 parent0[1]: (159) {G1,W7,D2,L2,V1,M1} R(51,6) { disjointwith( X,
% 0.72/1.09 c_tptpcol_5_110593 ), ! disjointwith( X, c_tptpcol_4_106497 ) }.
% 0.72/1.09 parent1[0]: (248) {G2,W3,D2,L1,V0,M1} R(162,139) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_4_106497 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_3_114688
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (251) {G3,W3,D2,L1,V0,M1} R(248,159) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_5_110593 ) }.
% 0.72/1.09 parent0: (488) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_5_110593 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (489) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 parent0[1]: (160) {G1,W7,D2,L2,V1,M1} R(51,8) { disjointwith( X,
% 0.72/1.09 c_tptpcol_6_112641 ), ! disjointwith( X, c_tptpcol_5_110593 ) }.
% 0.72/1.09 parent1[0]: (251) {G3,W3,D2,L1,V0,M1} R(248,159) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_5_110593 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_3_114688
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (258) {G4,W3,D2,L1,V0,M1} R(251,160) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_6_112641 ) }.
% 0.72/1.09 parent0: (489) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_3_114688,
% 0.72/1.09 c_tptpcol_6_112641 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (490) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 parent0[1]: (50) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.72/1.09 disjointwith( X, Y ) }.
% 0.72/1.09 parent1[0]: (258) {G4,W3,D2,L1,V0,M1} R(251,160) { disjointwith(
% 0.72/1.09 c_tptpcol_3_114688, c_tptpcol_6_112641 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_3_114688
% 0.72/1.09 Y := c_tptpcol_6_112641
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (261) {G5,W3,D2,L1,V0,M1} R(258,50) { disjointwith(
% 0.72/1.09 c_tptpcol_6_112641, c_tptpcol_3_114688 ) }.
% 0.72/1.09 parent0: (490) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_3_114688 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (491) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 parent0[1]: (164) {G1,W7,D2,L2,V1,M1} R(51,14) { disjointwith( X,
% 0.72/1.09 c_tptpcol_4_114689 ), ! disjointwith( X, c_tptpcol_3_114688 ) }.
% 0.72/1.09 parent1[0]: (261) {G5,W3,D2,L1,V0,M1} R(258,50) { disjointwith(
% 0.72/1.09 c_tptpcol_6_112641, c_tptpcol_3_114688 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_6_112641
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (263) {G6,W3,D2,L1,V0,M1} R(164,261) { disjointwith(
% 0.72/1.09 c_tptpcol_6_112641, c_tptpcol_4_114689 ) }.
% 0.72/1.09 parent0: (491) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_4_114689 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (492) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0[1]: (165) {G1,W7,D2,L2,V1,M1} R(51,16) { disjointwith( X,
% 0.72/1.09 c_tptpcol_5_114690 ), ! disjointwith( X, c_tptpcol_4_114689 ) }.
% 0.72/1.09 parent1[0]: (263) {G6,W3,D2,L1,V0,M1} R(164,261) { disjointwith(
% 0.72/1.09 c_tptpcol_6_112641, c_tptpcol_4_114689 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_6_112641
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (273) {G7,W3,D2,L1,V0,M1} R(165,263) { disjointwith(
% 0.72/1.09 c_tptpcol_6_112641, c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0: (492) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_112641,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (493) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0[1]: (177) {G1,W7,D2,L2,V1,M1} R(52,10) { disjointwith(
% 0.72/1.09 c_tptpcol_7_113665, X ), ! disjointwith( c_tptpcol_6_112641, X ) }.
% 0.72/1.09 parent1[0]: (273) {G7,W3,D2,L1,V0,M1} R(165,263) { disjointwith(
% 0.72/1.09 c_tptpcol_6_112641, c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_5_114690
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (274) {G8,W3,D2,L1,V0,M1} R(273,177) { disjointwith(
% 0.72/1.09 c_tptpcol_7_113665, c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent0: (493) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (494) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0[1]: (166) {G1,W7,D2,L2,V1,M1} R(51,18) { disjointwith( X,
% 0.72/1.09 c_tptpcol_6_116738 ), ! disjointwith( X, c_tptpcol_5_114690 ) }.
% 0.72/1.09 parent1[0]: (274) {G8,W3,D2,L1,V0,M1} R(273,177) { disjointwith(
% 0.72/1.09 c_tptpcol_7_113665, c_tptpcol_5_114690 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_7_113665
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (282) {G9,W3,D2,L1,V0,M1} R(166,274) { disjointwith(
% 0.72/1.09 c_tptpcol_7_113665, c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0: (494) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_7_113665,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (495) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 parent0[1]: (50) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.72/1.09 disjointwith( X, Y ) }.
% 0.72/1.09 parent1[0]: (282) {G9,W3,D2,L1,V0,M1} R(166,274) { disjointwith(
% 0.72/1.09 c_tptpcol_7_113665, c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_7_113665
% 0.72/1.09 Y := c_tptpcol_6_116738
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (284) {G10,W3,D2,L1,V0,M1} R(282,50) { disjointwith(
% 0.72/1.09 c_tptpcol_6_116738, c_tptpcol_7_113665 ) }.
% 0.72/1.09 parent0: (495) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_7_113665 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (496) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_8_114177 ) }.
% 0.72/1.09 parent0[1]: (163) {G1,W7,D2,L2,V1,M1} R(51,12) { disjointwith( X,
% 0.72/1.09 c_tptpcol_8_114177 ), ! disjointwith( X, c_tptpcol_7_113665 ) }.
% 0.72/1.09 parent1[0]: (284) {G10,W3,D2,L1,V0,M1} R(282,50) { disjointwith(
% 0.72/1.09 c_tptpcol_6_116738, c_tptpcol_7_113665 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_6_116738
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (286) {G11,W3,D2,L1,V0,M1} R(284,163) { disjointwith(
% 0.72/1.09 c_tptpcol_6_116738, c_tptpcol_8_114177 ) }.
% 0.72/1.09 parent0: (496) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_6_116738,
% 0.72/1.09 c_tptpcol_8_114177 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (497) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0[1]: (50) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.72/1.09 disjointwith( X, Y ) }.
% 0.72/1.09 parent1[0]: (286) {G11,W3,D2,L1,V0,M1} R(284,163) { disjointwith(
% 0.72/1.09 c_tptpcol_6_116738, c_tptpcol_8_114177 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_6_116738
% 0.72/1.09 Y := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (287) {G12,W3,D2,L1,V0,M1} R(286,50) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent0: (497) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (498) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 parent0[1]: (167) {G1,W7,D2,L2,V1,M1} R(51,20) { disjointwith( X,
% 0.72/1.09 c_tptpcol_7_117762 ), ! disjointwith( X, c_tptpcol_6_116738 ) }.
% 0.72/1.09 parent1[0]: (287) {G12,W3,D2,L1,V0,M1} R(286,50) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_6_116738 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (289) {G13,W3,D2,L1,V0,M1} R(167,287) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_7_117762 ) }.
% 0.72/1.09 parent0: (498) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_7_117762 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (499) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 parent0[1]: (168) {G1,W7,D2,L2,V1,M1} R(51,22) { disjointwith( X,
% 0.72/1.09 c_tptpcol_8_117763 ), ! disjointwith( X, c_tptpcol_7_117762 ) }.
% 0.72/1.09 parent1[0]: (289) {G13,W3,D2,L1,V0,M1} R(167,287) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_7_117762 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (296) {G14,W3,D2,L1,V0,M1} R(168,289) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_8_117763 ) }.
% 0.72/1.09 parent0: (499) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_8_117763 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (500) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 parent0[1]: (169) {G1,W7,D2,L2,V1,M1} R(51,24) { disjointwith( X,
% 0.72/1.09 c_tptpcol_9_118019 ), ! disjointwith( X, c_tptpcol_8_117763 ) }.
% 0.72/1.09 parent1[0]: (296) {G14,W3,D2,L1,V0,M1} R(168,289) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_8_117763 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (301) {G15,W3,D2,L1,V0,M1} R(169,296) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_9_118019 ) }.
% 0.72/1.09 parent0: (500) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_9_118019 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (501) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 parent0[1]: (170) {G1,W7,D2,L2,V1,M1} R(51,26) { disjointwith( X,
% 0.72/1.09 c_tptpcol_10_118020 ), ! disjointwith( X, c_tptpcol_9_118019 ) }.
% 0.72/1.09 parent1[0]: (301) {G15,W3,D2,L1,V0,M1} R(169,296) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_9_118019 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (308) {G16,W3,D2,L1,V0,M1} R(170,301) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_10_118020 ) }.
% 0.72/1.09 parent0: (501) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_10_118020 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (502) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 parent0[1]: (171) {G1,W7,D2,L2,V1,M1} R(51,28) { disjointwith( X,
% 0.72/1.09 c_tptpcol_11_118084 ), ! disjointwith( X, c_tptpcol_10_118020 ) }.
% 0.72/1.09 parent1[0]: (308) {G16,W3,D2,L1,V0,M1} R(170,301) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_10_118020 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (313) {G17,W3,D2,L1,V0,M1} R(171,308) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_11_118084 ) }.
% 0.72/1.09 parent0: (502) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_11_118084 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (503) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 parent0[1]: (172) {G1,W7,D2,L2,V1,M1} R(51,30) { disjointwith( X,
% 0.72/1.09 c_tptpcol_12_118116 ), ! disjointwith( X, c_tptpcol_11_118084 ) }.
% 0.72/1.09 parent1[0]: (313) {G17,W3,D2,L1,V0,M1} R(171,308) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_11_118084 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (320) {G18,W3,D2,L1,V0,M1} R(172,313) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_12_118116 ) }.
% 0.72/1.09 parent0: (503) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_12_118116 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (504) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 parent0[1]: (173) {G1,W7,D2,L2,V1,M1} R(51,32) { disjointwith( X,
% 0.72/1.09 c_tptpcol_13_118117 ), ! disjointwith( X, c_tptpcol_12_118116 ) }.
% 0.72/1.09 parent1[0]: (320) {G18,W3,D2,L1,V0,M1} R(172,313) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_12_118116 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (325) {G19,W3,D2,L1,V0,M1} R(173,320) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_13_118117 ) }.
% 0.72/1.09 parent0: (504) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_13_118117 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 0 ==> 0
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (505) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_14_118118 ) }.
% 0.72/1.09 parent0[1]: (174) {G1,W7,D2,L2,V1,M1} R(51,34) { disjointwith( X,
% 0.72/1.09 c_tptpcol_14_118118 ), ! disjointwith( X, c_tptpcol_13_118117 ) }.
% 0.72/1.09 parent1[0]: (325) {G19,W3,D2,L1,V0,M1} R(173,320) { disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_13_118117 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 X := c_tptpcol_8_114177
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 resolution: (506) {G1,W0,D0,L0,V0,M0} { }.
% 0.72/1.09 parent0[0]: (106) {G0,W4,D2,L1,V0,M1} I { ! disjointwith(
% 0.72/1.09 c_tptpcol_8_114177, c_tptpcol_14_118118 ) }.
% 0.72/1.09 parent1[0]: (505) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_114177,
% 0.72/1.09 c_tptpcol_14_118118 ) }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 substitution1:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 subsumption: (332) {G20,W0,D0,L0,V0,M0} R(174,325);r(106) { }.
% 0.72/1.09 parent0: (506) {G1,W0,D0,L0,V0,M0} { }.
% 0.72/1.09 substitution0:
% 0.72/1.09 end
% 0.72/1.09 permutation0:
% 0.72/1.09 end
% 0.72/1.09
% 0.72/1.09 Proof check complete!
% 0.72/1.09
% 0.72/1.09 Memory use:
% 0.72/1.09
% 0.72/1.09 space for terms: 3744
% 0.72/1.09 space for clauses: 15611
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 clauses generated: 681
% 0.72/1.09 clauses kept: 333
% 0.72/1.09 clauses selected: 266
% 0.72/1.09 clauses deleted: 0
% 0.72/1.09 clauses inuse deleted: 0
% 0.72/1.09
% 0.72/1.09 subsentry: 404
% 0.72/1.09 literals s-matched: 350
% 0.72/1.09 literals matched: 350
% 0.72/1.09 full subsumption: 2
% 0.72/1.09
% 0.72/1.09 checksum: 1545827581
% 0.72/1.09
% 0.72/1.09
% 0.72/1.09 Bliksem ended
%------------------------------------------------------------------------------