%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n021.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:19 EDT 2022
% Result : Theorem 0.71s 1.10s
% Output : Refutation 0.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Fri Jun 10 13:37:39 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.71/1.09 *** allocated 10000 integers for termspace/termends
% 0.71/1.09 *** allocated 10000 integers for clauses
% 0.71/1.09 *** allocated 10000 integers for justifications
% 0.71/1.09 Bliksem 1.12
% 0.71/1.09
% 0.71/1.09
% 0.71/1.09 Automatic Strategy Selection
% 0.71/1.09
% 0.71/1.09
% 0.71/1.09 Clauses:
% 0.71/1.09
% 0.71/1.09 { genlmt( c_gregoriancalendarmt, c_basekb ) }.
% 0.71/1.09 { genlmt( c_unitedstatesgeographypeoplemt, c_peopledatamt ) }.
% 0.71/1.09 { genlmt( c_unitedstatessociallifemt, c_gregoriancalendarmt ) }.
% 0.71/1.09 { transitivebinarypredicate( c_genlmt ) }.
% 0.71/1.09 { genlmt( c_basekb, c_universalvocabularymt ) }.
% 0.71/1.09 { genlmt( c_peopledatamt, c_unitedstatessociallifemt ) }.
% 0.71/1.09 { genls( c_tptpcol_2_2, c_tptpcol_1_1 ) }.
% 0.71/1.09 { ! tptpcol_2_2( X ), tptpcol_1_1( X ) }.
% 0.71/1.09 { genls( c_tptpcol_3_16386, c_tptpcol_2_2 ) }.
% 0.71/1.09 { ! tptpcol_3_16386( X ), tptpcol_2_2( X ) }.
% 0.71/1.09 { genls( c_tptpcol_4_24578, c_tptpcol_3_16386 ) }.
% 0.71/1.09 { ! tptpcol_4_24578( X ), tptpcol_3_16386( X ) }.
% 0.71/1.09 { genls( c_tptpcol_5_24579, c_tptpcol_4_24578 ) }.
% 0.71/1.09 { ! tptpcol_5_24579( X ), tptpcol_4_24578( X ) }.
% 0.71/1.09 { genls( c_tptpcol_6_26627, c_tptpcol_5_24579 ) }.
% 0.71/1.09 { ! tptpcol_6_26627( X ), tptpcol_5_24579( X ) }.
% 0.71/1.09 { genls( c_tptpcol_7_26628, c_tptpcol_6_26627 ) }.
% 0.71/1.09 { ! tptpcol_7_26628( X ), tptpcol_6_26627( X ) }.
% 0.71/1.09 { genls( c_tptpcol_8_26629, c_tptpcol_7_26628 ) }.
% 0.71/1.09 { ! tptpcol_8_26629( X ), tptpcol_7_26628( X ) }.
% 0.71/1.09 { genls( c_tptpcol_9_26885, c_tptpcol_8_26629 ) }.
% 0.71/1.09 { ! tptpcol_9_26885( X ), tptpcol_8_26629( X ) }.
% 0.71/1.09 { genls( c_tptpcol_10_26886, c_tptpcol_9_26885 ) }.
% 0.71/1.09 { ! tptpcol_10_26886( X ), tptpcol_9_26885( X ) }.
% 0.71/1.09 { genls( c_tptpcol_11_26887, c_tptpcol_10_26886 ) }.
% 0.71/1.09 { ! tptpcol_11_26887( X ), tptpcol_10_26886( X ) }.
% 0.71/1.09 { genls( c_tptpcol_12_26919, c_tptpcol_11_26887 ) }.
% 0.71/1.09 { ! tptpcol_12_26919( X ), tptpcol_11_26887( X ) }.
% 0.71/1.09 { genls( c_tptpcol_13_26920, c_tptpcol_12_26919 ) }.
% 0.71/1.09 { ! tptpcol_13_26920( X ), tptpcol_12_26919( X ) }.
% 0.71/1.09 { genls( c_tptpcol_14_26921, c_tptpcol_13_26920 ) }.
% 0.71/1.09 { ! tptpcol_14_26921( X ), tptpcol_13_26920( X ) }.
% 0.71/1.09 { genls( c_tptpcol_15_26925, c_tptpcol_14_26921 ) }.
% 0.71/1.09 { ! tptpcol_15_26925( X ), tptpcol_14_26921( X ) }.
% 0.71/1.09 { genls( c_tptpcol_16_26926, c_tptpcol_15_26925 ) }.
% 0.71/1.09 { ! tptpcol_16_26926( X ), tptpcol_15_26925( X ) }.
% 0.71/1.09 { genls( c_tptpcol_2_65537, c_tptpcol_1_65536 ) }.
% 0.71/1.09 { ! tptpcol_2_65537( X ), tptpcol_1_65536( X ) }.
% 0.71/1.09 { genls( c_tptpcol_3_81921, c_tptpcol_2_65537 ) }.
% 0.71/1.09 { ! tptpcol_3_81921( X ), tptpcol_2_65537( X ) }.
% 0.71/1.09 { genls( c_tptpcol_4_90113, c_tptpcol_3_81921 ) }.
% 0.71/1.09 { ! tptpcol_4_90113( X ), tptpcol_3_81921( X ) }.
% 0.71/1.09 { genls( c_tptpcol_5_90114, c_tptpcol_4_90113 ) }.
% 0.71/1.09 { ! tptpcol_5_90114( X ), tptpcol_4_90113( X ) }.
% 0.71/1.09 { genls( c_tptpcol_6_92162, c_tptpcol_5_90114 ) }.
% 0.71/1.09 { ! tptpcol_6_92162( X ), tptpcol_5_90114( X ) }.
% 0.71/1.09 { genls( c_tptpcol_7_92163, c_tptpcol_6_92162 ) }.
% 0.71/1.09 { ! tptpcol_7_92163( X ), tptpcol_6_92162( X ) }.
% 0.71/1.09 { genls( c_tptpcol_8_92164, c_tptpcol_7_92163 ) }.
% 0.71/1.09 { ! tptpcol_8_92164( X ), tptpcol_7_92163( X ) }.
% 0.71/1.09 { genls( c_tptpcol_9_92165, c_tptpcol_8_92164 ) }.
% 0.71/1.09 { ! tptpcol_9_92165( X ), tptpcol_8_92164( X ) }.
% 0.71/1.09 { genls( c_tptpcol_10_92166, c_tptpcol_9_92165 ) }.
% 0.71/1.09 { ! tptpcol_10_92166( X ), tptpcol_9_92165( X ) }.
% 0.71/1.09 { genls( c_tptpcol_11_92230, c_tptpcol_10_92166 ) }.
% 0.71/1.09 { ! tptpcol_11_92230( X ), tptpcol_10_92166( X ) }.
% 0.71/1.09 { genls( c_tptpcol_12_92262, c_tptpcol_11_92230 ) }.
% 0.71/1.09 { ! tptpcol_12_92262( X ), tptpcol_11_92230( X ) }.
% 0.71/1.09 { genls( c_tptpcol_13_92263, c_tptpcol_12_92262 ) }.
% 0.71/1.09 { ! tptpcol_13_92263( X ), tptpcol_12_92262( X ) }.
% 0.71/1.09 { genls( c_tptpcol_14_92264, c_tptpcol_13_92263 ) }.
% 0.71/1.09 { ! tptpcol_14_92264( X ), tptpcol_13_92263( X ) }.
% 0.71/1.09 { genls( c_tptpcol_15_92268, c_tptpcol_14_92264 ) }.
% 0.71/1.09 { ! tptpcol_15_92268( X ), tptpcol_14_92264( X ) }.
% 0.71/1.09 { genls( c_tptpcol_16_92269, c_tptpcol_15_92268 ) }.
% 0.71/1.09 { ! tptpcol_16_92269( X ), tptpcol_15_92268( X ) }.
% 0.71/1.09 { disjointwith( c_tptpcol_1_1, c_tptpcol_1_65536 ) }.
% 0.71/1.09 { ! tptpcol_1_1( X ), ! tptpcol_1_65536( X ) }.
% 0.71/1.09 { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith( Y, Z ) }.
% 0.71/1.09 { ! genlinverse( X, Z ), ! genlinverse( Z, Y ), genlpreds( X, Y ) }.
% 0.71/1.09 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.71/1.09 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.71/1.09 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.71/1.09 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.71/1.09 { ! genlpreds( X, Z ), ! genlpreds( Z, Y ), genlpreds( X, Y ) }.
% 0.71/1.09 { ! predicate( X ), genlpreds( X, X ) }.
% 0.71/1.09 { ! predicate( X ), genlpreds( X, X ) }.
% 0.71/1.09 { ! genlinverse( Y, X ), binarypredicate( X ) }.
% 0.71/1.09 { ! genlinverse( X, Y ), binarypredicate( X ) }.
% 0.71/1.09 { ! genlinverse( Z, X ), ! genlpreds( Y, Z ), genlinverse( Y, X ) }.
% 0.71/1.09 { ! genlinverse( X, Z ), ! genlpreds( Z, Y ), genlinverse( X, Y ) }.
% 0.71/1.09 { ! disjointwith( Y, X ), collection( X ) }.
% 0.71/1.09 { ! disjointwith( X, Y ), collection( X ) }.
% 0.71/1.09 { ! disjointwith( X, Y ), disjointwith( Y, X ) }.
% 0.71/1.09 { ! disjointwith( X, Z ), ! genls( Y, Z ), disjointwith( X, Y ) }.
% 0.71/1.09 { ! disjointwith( Z, X ), ! genls( Y, Z ), disjointwith( Y, X ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_16_92269 ), tptpcol_16_92269( X ) }.
% 0.71/1.09 { ! tptpcol_16_92269( X ), isa( X, c_tptpcol_16_92269 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_15_92268 ), tptpcol_15_92268( X ) }.
% 0.71/1.09 { ! tptpcol_15_92268( X ), isa( X, c_tptpcol_15_92268 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_14_92264 ), tptpcol_14_92264( X ) }.
% 0.71/1.09 { ! tptpcol_14_92264( X ), isa( X, c_tptpcol_14_92264 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_13_92263 ), tptpcol_13_92263( X ) }.
% 0.71/1.09 { ! tptpcol_13_92263( X ), isa( X, c_tptpcol_13_92263 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_12_92262 ), tptpcol_12_92262( X ) }.
% 0.71/1.09 { ! tptpcol_12_92262( X ), isa( X, c_tptpcol_12_92262 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_11_92230 ), tptpcol_11_92230( X ) }.
% 0.71/1.09 { ! tptpcol_11_92230( X ), isa( X, c_tptpcol_11_92230 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_10_92166 ), tptpcol_10_92166( X ) }.
% 0.71/1.09 { ! tptpcol_10_92166( X ), isa( X, c_tptpcol_10_92166 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_9_92165 ), tptpcol_9_92165( X ) }.
% 0.71/1.09 { ! tptpcol_9_92165( X ), isa( X, c_tptpcol_9_92165 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_8_92164 ), tptpcol_8_92164( X ) }.
% 0.71/1.09 { ! tptpcol_8_92164( X ), isa( X, c_tptpcol_8_92164 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_7_92163 ), tptpcol_7_92163( X ) }.
% 0.71/1.09 { ! tptpcol_7_92163( X ), isa( X, c_tptpcol_7_92163 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_6_92162 ), tptpcol_6_92162( X ) }.
% 0.71/1.09 { ! tptpcol_6_92162( X ), isa( X, c_tptpcol_6_92162 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_5_90114 ), tptpcol_5_90114( X ) }.
% 0.71/1.09 { ! tptpcol_5_90114( X ), isa( X, c_tptpcol_5_90114 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_4_90113 ), tptpcol_4_90113( X ) }.
% 0.71/1.09 { ! tptpcol_4_90113( X ), isa( X, c_tptpcol_4_90113 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_3_81921 ), tptpcol_3_81921( X ) }.
% 0.71/1.09 { ! tptpcol_3_81921( X ), isa( X, c_tptpcol_3_81921 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_1_65536 ), tptpcol_1_65536( X ) }.
% 0.71/1.09 { ! tptpcol_1_65536( X ), isa( X, c_tptpcol_1_65536 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_2_65537 ), tptpcol_2_65537( X ) }.
% 0.71/1.09 { ! tptpcol_2_65537( X ), isa( X, c_tptpcol_2_65537 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_16_26926 ), tptpcol_16_26926( X ) }.
% 0.71/1.09 { ! tptpcol_16_26926( X ), isa( X, c_tptpcol_16_26926 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_15_26925 ), tptpcol_15_26925( X ) }.
% 0.71/1.09 { ! tptpcol_15_26925( X ), isa( X, c_tptpcol_15_26925 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_14_26921 ), tptpcol_14_26921( X ) }.
% 0.71/1.09 { ! tptpcol_14_26921( X ), isa( X, c_tptpcol_14_26921 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_13_26920 ), tptpcol_13_26920( X ) }.
% 0.71/1.09 { ! tptpcol_13_26920( X ), isa( X, c_tptpcol_13_26920 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_12_26919 ), tptpcol_12_26919( X ) }.
% 0.71/1.09 { ! tptpcol_12_26919( X ), isa( X, c_tptpcol_12_26919 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_11_26887 ), tptpcol_11_26887( X ) }.
% 0.71/1.09 { ! tptpcol_11_26887( X ), isa( X, c_tptpcol_11_26887 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_10_26886 ), tptpcol_10_26886( X ) }.
% 0.71/1.09 { ! tptpcol_10_26886( X ), isa( X, c_tptpcol_10_26886 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_9_26885 ), tptpcol_9_26885( X ) }.
% 0.71/1.09 { ! tptpcol_9_26885( X ), isa( X, c_tptpcol_9_26885 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_8_26629 ), tptpcol_8_26629( X ) }.
% 0.71/1.09 { ! tptpcol_8_26629( X ), isa( X, c_tptpcol_8_26629 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_7_26628 ), tptpcol_7_26628( X ) }.
% 0.71/1.09 { ! tptpcol_7_26628( X ), isa( X, c_tptpcol_7_26628 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_6_26627 ), tptpcol_6_26627( X ) }.
% 0.71/1.09 { ! tptpcol_6_26627( X ), isa( X, c_tptpcol_6_26627 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_5_24579 ), tptpcol_5_24579( X ) }.
% 0.71/1.09 { ! tptpcol_5_24579( X ), isa( X, c_tptpcol_5_24579 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_4_24578 ), tptpcol_4_24578( X ) }.
% 0.71/1.09 { ! tptpcol_4_24578( X ), isa( X, c_tptpcol_4_24578 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_3_16386 ), tptpcol_3_16386( X ) }.
% 0.71/1.09 { ! tptpcol_3_16386( X ), isa( X, c_tptpcol_3_16386 ) }.
% 0.71/1.09 { ! isa( X, c_tptpcol_1_1 ), tptpcol_1_1( X ) }.
% 0.71/1.09 { ! tptpcol_1_1( X ), isa( X, c_tptpcol_1_1 ) }.
% 0.71/1.10 { ! isa( X, c_tptpcol_2_2 ), tptpcol_2_2( X ) }.
% 0.71/1.10 { ! tptpcol_2_2( X ), isa( X, c_tptpcol_2_2 ) }.
% 0.71/1.10 { ! genls( Y, X ), collection( X ) }.
% 0.71/1.10 { ! genls( Y, X ), collection( X ) }.
% 0.71/1.10 { ! genls( X, Y ), collection( X ) }.
% 0.71/1.10 { ! genls( X, Y ), collection( X ) }.
% 0.71/1.10 { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y ) }.
% 0.71/1.10 { ! collection( X ), genls( X, X ) }.
% 0.71/1.10 { ! collection( X ), genls( X, X ) }.
% 0.71/1.10 { ! genls( Z, X ), ! genls( Y, Z ), genls( Y, X ) }.
% 0.71/1.10 { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y ) }.
% 0.71/1.10 { ! isa( X, c_transitivebinarypredicate ), transitivebinarypredicate( X ) }
% 0.71/1.10 .
% 0.71/1.10 { ! transitivebinarypredicate( X ), isa( X, c_transitivebinarypredicate ) }
% 0.71/1.10 .
% 0.71/1.10 { ! isa( Y, X ), collection( X ) }.
% 0.71/1.10 { ! isa( Y, X ), collection( X ) }.
% 0.71/1.10 { ! isa( X, Y ), thing( X ) }.
% 0.71/1.10 { ! isa( X, Y ), thing( X ) }.
% 0.71/1.10 { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y ) }.
% 0.71/1.10 { mtvisible( c_universalvocabularymt ) }.
% 0.71/1.10 { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible( X ) }.
% 0.71/1.10 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.71/1.10 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.71/1.10 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.71/1.10 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.71/1.10 { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X, Y ) }.
% 0.71/1.10 { ! microtheory( X ), genlmt( X, X ) }.
% 0.71/1.10 { ! microtheory( X ), genlmt( X, X ) }.
% 0.71/1.10 { mtvisible( c_basekb ) }.
% 0.71/1.10 { mtvisible( c_unitedstatesgeographypeoplemt ) }.
% 0.71/1.10 { ! disjointwith( c_tptpcol_16_26926, c_tptpcol_16_92269 ) }.
% 0.71/1.10
% 0.71/1.10 percentage equality = 0.000000, percentage horn = 1.000000
% 0.71/1.10 This is a near-Horn, non-equality problem
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Options Used:
% 0.71/1.10
% 0.71/1.10 useres = 1
% 0.71/1.10 useparamod = 0
% 0.71/1.10 useeqrefl = 0
% 0.71/1.10 useeqfact = 0
% 0.71/1.10 usefactor = 1
% 0.71/1.10 usesimpsplitting = 0
% 0.71/1.10 usesimpdemod = 0
% 0.71/1.10 usesimpres = 4
% 0.71/1.10
% 0.71/1.10 resimpinuse = 1000
% 0.71/1.10 resimpclauses = 20000
% 0.71/1.10 substype = standard
% 0.71/1.10 backwardsubs = 1
% 0.71/1.10 selectoldest = 5
% 0.71/1.10
% 0.71/1.10 litorderings [0] = split
% 0.71/1.10 litorderings [1] = liftord
% 0.71/1.10
% 0.71/1.10 termordering = none
% 0.71/1.10
% 0.71/1.10 litapriori = 1
% 0.71/1.10 termapriori = 0
% 0.71/1.10 litaposteriori = 0
% 0.71/1.10 termaposteriori = 0
% 0.71/1.10 demodaposteriori = 0
% 0.71/1.10 ordereqreflfact = 0
% 0.71/1.10
% 0.71/1.10 litselect = negative
% 0.71/1.10
% 0.71/1.10 maxweight = 30000
% 0.71/1.10 maxdepth = 30000
% 0.71/1.10 maxlength = 115
% 0.71/1.10 maxnrvars = 195
% 0.71/1.10 excuselevel = 0
% 0.71/1.10 increasemaxweight = 0
% 0.71/1.10
% 0.71/1.10 maxselected = 10000000
% 0.71/1.10 maxnrclauses = 10000000
% 0.71/1.10
% 0.71/1.10 showgenerated = 0
% 0.71/1.10 showkept = 0
% 0.71/1.10 showselected = 0
% 0.71/1.10 showdeleted = 0
% 0.71/1.10 showresimp = 1
% 0.71/1.10 showstatus = 2000
% 0.71/1.10
% 0.71/1.10 prologoutput = 0
% 0.71/1.10 nrgoals = 5000000
% 0.71/1.10 totalproof = 1
% 0.71/1.10
% 0.71/1.10 Symbols occurring in the translation:
% 0.71/1.10
% 0.71/1.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.71/1.10 . [1, 2] (w:1, o:106, a:1, s:1, b:0),
% 0.71/1.10 ! [4, 1] (w:1, o:62, a:1, s:1, b:0),
% 0.71/1.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.71/1.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.71/1.10 c_gregoriancalendarmt [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.71/1.10 c_basekb [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.71/1.10 genlmt [37, 2] (w:1, o:130, a:1, s:1, b:0),
% 0.71/1.10 c_unitedstatesgeographypeoplemt [38, 0] (w:1, o:41, a:1, s:1, b:0),
% 0.71/1.10 c_peopledatamt [39, 0] (w:1, o:42, a:1, s:1, b:0),
% 0.71/1.10 c_unitedstatessociallifemt [40, 0] (w:1, o:43, a:1, s:1, b:0),
% 0.71/1.10 c_genlmt [41, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.71/1.10 transitivebinarypredicate [42, 1] (w:1, o:67, a:1, s:1, b:0),
% 0.71/1.10 c_universalvocabularymt [43, 0] (w:1, o:45, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_2_2 [44, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_1_1 [45, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.71/1.10 genls [46, 2] (w:1, o:131, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_2_2 [48, 1] (w:1, o:84, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_1_1 [49, 1] (w:1, o:68, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_3_16386 [50, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_3_16386 [51, 1] (w:1, o:86, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_4_24578 [52, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_4_24578 [53, 1] (w:1, o:88, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_5_24579 [54, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_5_24579 [55, 1] (w:1, o:90, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_6_26627 [56, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_6_26627 [57, 1] (w:1, o:92, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_7_26628 [58, 0] (w:1, o:34, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_7_26628 [59, 1] (w:1, o:94, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_8_26629 [60, 0] (w:1, o:36, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_8_26629 [61, 1] (w:1, o:96, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_9_26885 [62, 0] (w:1, o:38, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_9_26885 [63, 1] (w:1, o:98, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_10_26886 [64, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_10_26886 [65, 1] (w:1, o:69, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_11_26887 [66, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_11_26887 [67, 1] (w:1, o:71, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_12_26919 [68, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_12_26919 [69, 1] (w:1, o:73, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_13_26920 [70, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_13_26920 [71, 1] (w:1, o:75, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_14_26921 [72, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_14_26921 [73, 1] (w:1, o:77, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_15_26925 [74, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_15_26925 [75, 1] (w:1, o:79, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_16_26926 [76, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_16_26926 [77, 1] (w:1, o:81, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_2_65537 [78, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_1_65536 [79, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_2_65537 [80, 1] (w:1, o:85, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_1_65536 [81, 1] (w:1, o:82, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_3_81921 [82, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_3_81921 [83, 1] (w:1, o:87, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_4_90113 [84, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_4_90113 [85, 1] (w:1, o:89, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_5_90114 [86, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_5_90114 [87, 1] (w:1, o:91, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_6_92162 [88, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_6_92162 [89, 1] (w:1, o:93, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_7_92163 [90, 0] (w:1, o:35, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_7_92163 [91, 1] (w:1, o:95, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_8_92164 [92, 0] (w:1, o:37, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_8_92164 [93, 1] (w:1, o:97, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_9_92165 [94, 0] (w:1, o:39, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_9_92165 [95, 1] (w:1, o:99, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_10_92166 [96, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_10_92166 [97, 1] (w:1, o:70, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_11_92230 [98, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_11_92230 [99, 1] (w:1, o:72, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_12_92262 [100, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_12_92262 [101, 1] (w:1, o:74, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_13_92263 [102, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_13_92263 [103, 1] (w:1, o:76, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_14_92264 [104, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_14_92264 [105, 1] (w:1, o:78, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_15_92268 [106, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_15_92268 [107, 1] (w:1, o:80, a:1, s:1, b:0),
% 0.71/1.10 c_tptpcol_16_92269 [108, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.71/1.10 tptpcol_16_92269 [109, 1] (w:1, o:83, a:1, s:1, b:0),
% 0.71/1.10 disjointwith [110, 2] (w:1, o:132, a:1, s:1, b:0),
% 0.71/1.10 isa [113, 2] (w:1, o:133, a:1, s:1, b:0),
% 0.71/1.10 genlinverse [117, 2] (w:1, o:134, a:1, s:1, b:0),
% 0.71/1.10 genlpreds [118, 2] (w:1, o:135, a:1, s:1, b:0),
% 0.71/1.10 predicate [121, 1] (w:1, o:100, a:1, s:1, b:0),
% 0.71/1.10 binarypredicate [126, 1] (w:1, o:101, a:1, s:1, b:0),
% 0.71/1.10 collection [129, 1] (w:1, o:102, a:1, s:1, b:0),
% 0.71/1.10 c_transitivebinarypredicate [130, 0] (w:1, o:40, a:1, s:1, b:0),
% 0.71/1.10 thing [131, 1] (w:1, o:103, a:1, s:1, b:0),
% 0.71/1.10 mtvisible [132, 1] (w:1, o:104, a:1, s:1, b:0),
% 0.71/1.10 microtheory [135, 1] (w:1, o:105, a:1, s:1, b:0).
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Starting Search:
% 0.71/1.10
% 0.71/1.10 *** allocated 15000 integers for clauses
% 0.71/1.10 *** allocated 22500 integers for clauses
% 0.71/1.10 *** allocated 33750 integers for clauses
% 0.71/1.10
% 0.71/1.10 Bliksems!, er is een bewijs:
% 0.71/1.10 % SZS status Theorem
% 0.71/1.10 % SZS output start Refutation
% 0.71/1.10
% 0.71/1.10 (6) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_2_2, c_tptpcol_1_1 ) }.
% 0.71/1.10 (8) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_3_16386, c_tptpcol_2_2 ) }.
% 0.71/1.10 (10) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_24578, c_tptpcol_3_16386 )
% 0.71/1.10 }.
% 0.71/1.10 (12) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_24579, c_tptpcol_4_24578 )
% 0.71/1.10 }.
% 0.71/1.10 (14) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_26627, c_tptpcol_5_24579 )
% 0.71/1.10 }.
% 0.71/1.10 (16) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_26628, c_tptpcol_6_26627 )
% 0.71/1.10 }.
% 0.71/1.10 (18) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_26629, c_tptpcol_7_26628 )
% 0.71/1.10 }.
% 0.71/1.10 (20) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_26885, c_tptpcol_8_26629 )
% 0.71/1.10 }.
% 0.71/1.10 (22) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_26886, c_tptpcol_9_26885 )
% 0.71/1.10 }.
% 0.71/1.10 (24) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_26887, c_tptpcol_10_26886
% 0.71/1.10 ) }.
% 0.71/1.10 (26) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_26919, c_tptpcol_11_26887
% 0.71/1.10 ) }.
% 0.71/1.10 (28) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_26920, c_tptpcol_12_26919
% 0.71/1.10 ) }.
% 0.71/1.10 (30) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_26921, c_tptpcol_13_26920
% 0.71/1.10 ) }.
% 0.71/1.10 (32) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_15_26925, c_tptpcol_14_26921
% 0.71/1.10 ) }.
% 0.71/1.10 (34) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_16_26926, c_tptpcol_15_26925
% 0.71/1.10 ) }.
% 0.71/1.10 (36) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_2_65537, c_tptpcol_1_65536 )
% 0.71/1.10 }.
% 0.71/1.10 (38) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_3_81921, c_tptpcol_2_65537 )
% 0.71/1.10 }.
% 0.71/1.10 (40) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_90113, c_tptpcol_3_81921 )
% 0.71/1.10 }.
% 0.71/1.10 (42) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_90114, c_tptpcol_4_90113 )
% 0.71/1.10 }.
% 0.71/1.10 (44) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_92162, c_tptpcol_5_90114 )
% 0.71/1.10 }.
% 0.71/1.10 (46) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_92163, c_tptpcol_6_92162 )
% 0.71/1.10 }.
% 0.71/1.10 (48) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_92164, c_tptpcol_7_92163 )
% 0.71/1.10 }.
% 0.71/1.10 (50) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_92165, c_tptpcol_8_92164 )
% 0.71/1.10 }.
% 0.71/1.10 (52) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_92166, c_tptpcol_9_92165 )
% 0.71/1.10 }.
% 0.71/1.10 (54) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_92230, c_tptpcol_10_92166
% 0.71/1.10 ) }.
% 0.71/1.10 (56) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_92262, c_tptpcol_11_92230
% 0.71/1.10 ) }.
% 0.71/1.10 (58) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_92263, c_tptpcol_12_92262
% 0.71/1.10 ) }.
% 0.71/1.10 (60) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_92264, c_tptpcol_13_92263
% 0.71/1.10 ) }.
% 0.71/1.10 (62) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_15_92268, c_tptpcol_14_92264
% 0.71/1.10 ) }.
% 0.71/1.10 (64) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_16_92269, c_tptpcol_15_92268
% 0.71/1.10 ) }.
% 0.71/1.10 (66) {G0,W3,D2,L1,V0,M1} I { disjointwith( c_tptpcol_1_1, c_tptpcol_1_65536
% 0.71/1.10 ) }.
% 0.71/1.10 (80) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), ! disjointwith( X, Y )
% 0.71/1.10 }.
% 0.71/1.10 (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ), disjointwith( X, Y )
% 0.71/1.10 , ! genls( Y, Z ) }.
% 0.71/1.10 (164) {G0,W4,D2,L1,V0,M1} I { ! disjointwith( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 (212) {G1,W3,D2,L1,V0,M1} R(80,66) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_1_1 ) }.
% 0.71/1.10 (213) {G1,W7,D2,L2,V1,M1} R(81,8) { disjointwith( X, c_tptpcol_3_16386 ), !
% 0.71/1.10 disjointwith( X, c_tptpcol_2_2 ) }.
% 0.71/1.10 (214) {G1,W7,D2,L2,V1,M1} R(81,10) { disjointwith( X, c_tptpcol_4_24578 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_3_16386 ) }.
% 0.71/1.10 (215) {G1,W7,D2,L2,V1,M1} R(81,12) { disjointwith( X, c_tptpcol_5_24579 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_4_24578 ) }.
% 0.71/1.10 (216) {G1,W7,D2,L2,V1,M1} R(81,14) { disjointwith( X, c_tptpcol_6_26627 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_5_24579 ) }.
% 0.71/1.10 (217) {G1,W7,D2,L2,V1,M1} R(81,16) { disjointwith( X, c_tptpcol_7_26628 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_6_26627 ) }.
% 0.71/1.10 (218) {G1,W7,D2,L2,V1,M1} R(81,18) { disjointwith( X, c_tptpcol_8_26629 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_7_26628 ) }.
% 0.71/1.10 (219) {G1,W7,D2,L2,V1,M1} R(81,20) { disjointwith( X, c_tptpcol_9_26885 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_8_26629 ) }.
% 0.71/1.10 (220) {G1,W7,D2,L2,V1,M1} R(81,22) { disjointwith( X, c_tptpcol_10_26886 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_9_26885 ) }.
% 0.71/1.10 (221) {G1,W7,D2,L2,V1,M1} R(81,24) { disjointwith( X, c_tptpcol_11_26887 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_10_26886 ) }.
% 0.71/1.10 (222) {G1,W7,D2,L2,V1,M1} R(81,6) { disjointwith( X, c_tptpcol_2_2 ), !
% 0.71/1.10 disjointwith( X, c_tptpcol_1_1 ) }.
% 0.71/1.10 (223) {G1,W7,D2,L2,V1,M1} R(81,26) { disjointwith( X, c_tptpcol_12_26919 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_11_26887 ) }.
% 0.71/1.10 (224) {G1,W7,D2,L2,V1,M1} R(81,28) { disjointwith( X, c_tptpcol_13_26920 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_12_26919 ) }.
% 0.71/1.10 (225) {G1,W7,D2,L2,V1,M1} R(81,30) { disjointwith( X, c_tptpcol_14_26921 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_13_26920 ) }.
% 0.71/1.10 (226) {G1,W7,D2,L2,V1,M1} R(81,32) { disjointwith( X, c_tptpcol_15_26925 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_14_26921 ) }.
% 0.71/1.10 (227) {G1,W7,D2,L2,V1,M1} R(81,34) { disjointwith( X, c_tptpcol_16_26926 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_15_26925 ) }.
% 0.71/1.10 (228) {G1,W7,D2,L2,V1,M1} R(81,36) { disjointwith( X, c_tptpcol_2_65537 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_1_65536 ) }.
% 0.71/1.10 (229) {G1,W7,D2,L2,V1,M1} R(81,38) { disjointwith( X, c_tptpcol_3_81921 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_2_65537 ) }.
% 0.71/1.10 (230) {G1,W7,D2,L2,V1,M1} R(81,40) { disjointwith( X, c_tptpcol_4_90113 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_3_81921 ) }.
% 0.71/1.10 (231) {G1,W7,D2,L2,V1,M1} R(81,42) { disjointwith( X, c_tptpcol_5_90114 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_4_90113 ) }.
% 0.71/1.10 (232) {G1,W7,D2,L2,V1,M1} R(81,44) { disjointwith( X, c_tptpcol_6_92162 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_5_90114 ) }.
% 0.71/1.10 (233) {G1,W7,D2,L2,V1,M1} R(81,46) { disjointwith( X, c_tptpcol_7_92163 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_6_92162 ) }.
% 0.71/1.10 (234) {G1,W7,D2,L2,V1,M1} R(81,48) { disjointwith( X, c_tptpcol_8_92164 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_7_92163 ) }.
% 0.71/1.10 (235) {G1,W7,D2,L2,V1,M1} R(81,50) { disjointwith( X, c_tptpcol_9_92165 ),
% 0.71/1.10 ! disjointwith( X, c_tptpcol_8_92164 ) }.
% 0.71/1.10 (236) {G1,W7,D2,L2,V1,M1} R(81,52) { disjointwith( X, c_tptpcol_10_92166 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_9_92165 ) }.
% 0.71/1.10 (237) {G1,W7,D2,L2,V1,M1} R(81,54) { disjointwith( X, c_tptpcol_11_92230 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_10_92166 ) }.
% 0.71/1.10 (238) {G1,W7,D2,L2,V1,M1} R(81,56) { disjointwith( X, c_tptpcol_12_92262 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_11_92230 ) }.
% 0.71/1.10 (239) {G1,W7,D2,L2,V1,M1} R(81,58) { disjointwith( X, c_tptpcol_13_92263 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_12_92262 ) }.
% 0.71/1.10 (240) {G1,W7,D2,L2,V1,M1} R(81,60) { disjointwith( X, c_tptpcol_14_92264 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_13_92263 ) }.
% 0.71/1.10 (241) {G1,W7,D2,L2,V1,M1} R(81,62) { disjointwith( X, c_tptpcol_15_92268 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_14_92264 ) }.
% 0.71/1.10 (242) {G1,W7,D2,L2,V1,M1} R(81,64) { disjointwith( X, c_tptpcol_16_92269 )
% 0.71/1.10 , ! disjointwith( X, c_tptpcol_15_92268 ) }.
% 0.71/1.10 (409) {G2,W3,D2,L1,V0,M1} R(222,212) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_2_2 ) }.
% 0.71/1.10 (410) {G3,W3,D2,L1,V0,M1} R(409,213) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 (413) {G4,W3,D2,L1,V0,M1} R(410,214) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 (416) {G5,W3,D2,L1,V0,M1} R(413,215) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 (419) {G6,W3,D2,L1,V0,M1} R(416,216) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 (422) {G7,W3,D2,L1,V0,M1} R(419,217) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 (425) {G8,W3,D2,L1,V0,M1} R(422,218) { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 (429) {G9,W3,D2,L1,V0,M1} R(425,80) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 (454) {G10,W3,D2,L1,V0,M1} R(228,429) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 (471) {G11,W3,D2,L1,V0,M1} R(229,454) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 (481) {G12,W3,D2,L1,V0,M1} R(230,471) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 (491) {G13,W3,D2,L1,V0,M1} R(231,481) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 (501) {G14,W3,D2,L1,V0,M1} R(232,491) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 (511) {G15,W3,D2,L1,V0,M1} R(233,501) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 (521) {G16,W3,D2,L1,V0,M1} R(234,511) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 (531) {G17,W3,D2,L1,V0,M1} R(235,521) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 (541) {G18,W3,D2,L1,V0,M1} R(236,531) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 (551) {G19,W3,D2,L1,V0,M1} R(237,541) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 (561) {G20,W3,D2,L1,V0,M1} R(238,551) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 (571) {G21,W3,D2,L1,V0,M1} R(239,561) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 (581) {G22,W3,D2,L1,V0,M1} R(240,571) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 (591) {G23,W3,D2,L1,V0,M1} R(241,581) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 (601) {G24,W3,D2,L1,V0,M1} R(242,591) { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 (602) {G25,W3,D2,L1,V0,M1} R(601,80) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 (604) {G26,W3,D2,L1,V0,M1} R(602,219) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 (605) {G27,W3,D2,L1,V0,M1} R(604,220) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 (608) {G28,W3,D2,L1,V0,M1} R(605,221) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 (611) {G29,W3,D2,L1,V0,M1} R(608,223) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 (614) {G30,W3,D2,L1,V0,M1} R(611,224) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 (617) {G31,W3,D2,L1,V0,M1} R(614,225) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 (620) {G32,W3,D2,L1,V0,M1} R(617,226) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 (623) {G33,W3,D2,L1,V0,M1} R(620,227) { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_16_26926 ) }.
% 0.71/1.10 (626) {G34,W0,D0,L0,V0,M0} R(623,80);r(164) { }.
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 % SZS output end Refutation
% 0.71/1.10 found a proof!
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Unprocessed initial clauses:
% 0.71/1.10
% 0.71/1.10 (628) {G0,W3,D2,L1,V0,M1} { genlmt( c_gregoriancalendarmt, c_basekb ) }.
% 0.71/1.10 (629) {G0,W3,D2,L1,V0,M1} { genlmt( c_unitedstatesgeographypeoplemt,
% 0.71/1.10 c_peopledatamt ) }.
% 0.71/1.10 (630) {G0,W3,D2,L1,V0,M1} { genlmt( c_unitedstatessociallifemt,
% 0.71/1.10 c_gregoriancalendarmt ) }.
% 0.71/1.10 (631) {G0,W2,D2,L1,V0,M1} { transitivebinarypredicate( c_genlmt ) }.
% 0.71/1.10 (632) {G0,W3,D2,L1,V0,M1} { genlmt( c_basekb, c_universalvocabularymt )
% 0.71/1.10 }.
% 0.71/1.10 (633) {G0,W3,D2,L1,V0,M1} { genlmt( c_peopledatamt,
% 0.71/1.10 c_unitedstatessociallifemt ) }.
% 0.71/1.10 (634) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_2_2, c_tptpcol_1_1 ) }.
% 0.71/1.10 (635) {G0,W5,D2,L2,V1,M2} { ! tptpcol_2_2( X ), tptpcol_1_1( X ) }.
% 0.71/1.10 (636) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_3_16386, c_tptpcol_2_2 ) }.
% 0.71/1.10 (637) {G0,W5,D2,L2,V1,M2} { ! tptpcol_3_16386( X ), tptpcol_2_2( X ) }.
% 0.71/1.10 (638) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_24578, c_tptpcol_3_16386 )
% 0.71/1.10 }.
% 0.71/1.10 (639) {G0,W5,D2,L2,V1,M2} { ! tptpcol_4_24578( X ), tptpcol_3_16386( X )
% 0.71/1.10 }.
% 0.71/1.10 (640) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_24579, c_tptpcol_4_24578 )
% 0.71/1.10 }.
% 0.71/1.10 (641) {G0,W5,D2,L2,V1,M2} { ! tptpcol_5_24579( X ), tptpcol_4_24578( X )
% 0.71/1.10 }.
% 0.71/1.10 (642) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_26627, c_tptpcol_5_24579 )
% 0.71/1.10 }.
% 0.71/1.10 (643) {G0,W5,D2,L2,V1,M2} { ! tptpcol_6_26627( X ), tptpcol_5_24579( X )
% 0.71/1.10 }.
% 0.71/1.10 (644) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_26628, c_tptpcol_6_26627 )
% 0.71/1.10 }.
% 0.71/1.10 (645) {G0,W5,D2,L2,V1,M2} { ! tptpcol_7_26628( X ), tptpcol_6_26627( X )
% 0.71/1.10 }.
% 0.71/1.10 (646) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_26629, c_tptpcol_7_26628 )
% 0.71/1.10 }.
% 0.71/1.10 (647) {G0,W5,D2,L2,V1,M2} { ! tptpcol_8_26629( X ), tptpcol_7_26628( X )
% 0.71/1.10 }.
% 0.71/1.10 (648) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_26885, c_tptpcol_8_26629 )
% 0.71/1.10 }.
% 0.71/1.10 (649) {G0,W5,D2,L2,V1,M2} { ! tptpcol_9_26885( X ), tptpcol_8_26629( X )
% 0.71/1.10 }.
% 0.71/1.10 (650) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_26886, c_tptpcol_9_26885 )
% 0.71/1.10 }.
% 0.71/1.10 (651) {G0,W5,D2,L2,V1,M2} { ! tptpcol_10_26886( X ), tptpcol_9_26885( X )
% 0.71/1.10 }.
% 0.71/1.10 (652) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_26887, c_tptpcol_10_26886
% 0.71/1.10 ) }.
% 0.71/1.10 (653) {G0,W5,D2,L2,V1,M2} { ! tptpcol_11_26887( X ), tptpcol_10_26886( X )
% 0.71/1.10 }.
% 0.71/1.10 (654) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_26919, c_tptpcol_11_26887
% 0.71/1.10 ) }.
% 0.71/1.10 (655) {G0,W5,D2,L2,V1,M2} { ! tptpcol_12_26919( X ), tptpcol_11_26887( X )
% 0.71/1.10 }.
% 0.71/1.10 (656) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_26920, c_tptpcol_12_26919
% 0.71/1.10 ) }.
% 0.71/1.10 (657) {G0,W5,D2,L2,V1,M2} { ! tptpcol_13_26920( X ), tptpcol_12_26919( X )
% 0.71/1.10 }.
% 0.71/1.10 (658) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_26921, c_tptpcol_13_26920
% 0.71/1.10 ) }.
% 0.71/1.10 (659) {G0,W5,D2,L2,V1,M2} { ! tptpcol_14_26921( X ), tptpcol_13_26920( X )
% 0.71/1.10 }.
% 0.71/1.10 (660) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_15_26925, c_tptpcol_14_26921
% 0.71/1.10 ) }.
% 0.71/1.10 (661) {G0,W5,D2,L2,V1,M2} { ! tptpcol_15_26925( X ), tptpcol_14_26921( X )
% 0.71/1.10 }.
% 0.71/1.10 (662) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_16_26926, c_tptpcol_15_26925
% 0.71/1.10 ) }.
% 0.71/1.10 (663) {G0,W5,D2,L2,V1,M2} { ! tptpcol_16_26926( X ), tptpcol_15_26925( X )
% 0.71/1.10 }.
% 0.71/1.10 (664) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_2_65537, c_tptpcol_1_65536 )
% 0.71/1.10 }.
% 0.71/1.10 (665) {G0,W5,D2,L2,V1,M2} { ! tptpcol_2_65537( X ), tptpcol_1_65536( X )
% 0.71/1.10 }.
% 0.71/1.10 (666) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_3_81921, c_tptpcol_2_65537 )
% 0.71/1.10 }.
% 0.71/1.10 (667) {G0,W5,D2,L2,V1,M2} { ! tptpcol_3_81921( X ), tptpcol_2_65537( X )
% 0.71/1.10 }.
% 0.71/1.10 (668) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_90113, c_tptpcol_3_81921 )
% 0.71/1.10 }.
% 0.71/1.10 (669) {G0,W5,D2,L2,V1,M2} { ! tptpcol_4_90113( X ), tptpcol_3_81921( X )
% 0.71/1.10 }.
% 0.71/1.10 (670) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_90114, c_tptpcol_4_90113 )
% 0.71/1.10 }.
% 0.71/1.10 (671) {G0,W5,D2,L2,V1,M2} { ! tptpcol_5_90114( X ), tptpcol_4_90113( X )
% 0.71/1.10 }.
% 0.71/1.10 (672) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_92162, c_tptpcol_5_90114 )
% 0.71/1.10 }.
% 0.71/1.10 (673) {G0,W5,D2,L2,V1,M2} { ! tptpcol_6_92162( X ), tptpcol_5_90114( X )
% 0.71/1.10 }.
% 0.71/1.10 (674) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_92163, c_tptpcol_6_92162 )
% 0.71/1.10 }.
% 0.71/1.10 (675) {G0,W5,D2,L2,V1,M2} { ! tptpcol_7_92163( X ), tptpcol_6_92162( X )
% 0.71/1.10 }.
% 0.71/1.10 (676) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_92164, c_tptpcol_7_92163 )
% 0.71/1.10 }.
% 0.71/1.10 (677) {G0,W5,D2,L2,V1,M2} { ! tptpcol_8_92164( X ), tptpcol_7_92163( X )
% 0.71/1.10 }.
% 0.71/1.10 (678) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_92165, c_tptpcol_8_92164 )
% 0.71/1.10 }.
% 0.71/1.10 (679) {G0,W5,D2,L2,V1,M2} { ! tptpcol_9_92165( X ), tptpcol_8_92164( X )
% 0.71/1.10 }.
% 0.71/1.10 (680) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_92166, c_tptpcol_9_92165 )
% 0.71/1.10 }.
% 0.71/1.10 (681) {G0,W5,D2,L2,V1,M2} { ! tptpcol_10_92166( X ), tptpcol_9_92165( X )
% 0.71/1.10 }.
% 0.71/1.10 (682) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_92230, c_tptpcol_10_92166
% 0.71/1.10 ) }.
% 0.71/1.10 (683) {G0,W5,D2,L2,V1,M2} { ! tptpcol_11_92230( X ), tptpcol_10_92166( X )
% 0.71/1.10 }.
% 0.71/1.10 (684) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_92262, c_tptpcol_11_92230
% 0.71/1.10 ) }.
% 0.71/1.10 (685) {G0,W5,D2,L2,V1,M2} { ! tptpcol_12_92262( X ), tptpcol_11_92230( X )
% 0.71/1.10 }.
% 0.71/1.10 (686) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_92263, c_tptpcol_12_92262
% 0.71/1.10 ) }.
% 0.71/1.10 (687) {G0,W5,D2,L2,V1,M2} { ! tptpcol_13_92263( X ), tptpcol_12_92262( X )
% 0.71/1.10 }.
% 0.71/1.10 (688) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_92264, c_tptpcol_13_92263
% 0.71/1.10 ) }.
% 0.71/1.10 (689) {G0,W5,D2,L2,V1,M2} { ! tptpcol_14_92264( X ), tptpcol_13_92263( X )
% 0.71/1.10 }.
% 0.71/1.10 (690) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_15_92268, c_tptpcol_14_92264
% 0.71/1.10 ) }.
% 0.71/1.10 (691) {G0,W5,D2,L2,V1,M2} { ! tptpcol_15_92268( X ), tptpcol_14_92264( X )
% 0.71/1.10 }.
% 0.71/1.10 (692) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_16_92269, c_tptpcol_15_92268
% 0.71/1.10 ) }.
% 0.71/1.10 (693) {G0,W5,D2,L2,V1,M2} { ! tptpcol_16_92269( X ), tptpcol_15_92268( X )
% 0.71/1.10 }.
% 0.71/1.10 (694) {G0,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_1, c_tptpcol_1_65536
% 0.71/1.10 ) }.
% 0.71/1.10 (695) {G0,W6,D2,L2,V1,M2} { ! tptpcol_1_1( X ), ! tptpcol_1_65536( X ) }.
% 0.71/1.10 (696) {G0,W12,D2,L3,V3,M3} { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith
% 0.71/1.10 ( Y, Z ) }.
% 0.71/1.10 (697) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlinverse( Z, Y )
% 0.71/1.10 , genlpreds( X, Y ) }.
% 0.71/1.10 (698) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.71/1.10 (699) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.71/1.10 (700) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.71/1.10 (701) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.71/1.10 (702) {G0,W11,D2,L3,V3,M3} { ! genlpreds( X, Z ), ! genlpreds( Z, Y ),
% 0.71/1.10 genlpreds( X, Y ) }.
% 0.71/1.10 (703) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.71/1.10 (704) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.71/1.10 (705) {G0,W6,D2,L2,V2,M2} { ! genlinverse( Y, X ), binarypredicate( X )
% 0.71/1.10 }.
% 0.71/1.10 (706) {G0,W6,D2,L2,V2,M2} { ! genlinverse( X, Y ), binarypredicate( X )
% 0.71/1.10 }.
% 0.71/1.10 (707) {G0,W11,D2,L3,V3,M3} { ! genlinverse( Z, X ), ! genlpreds( Y, Z ),
% 0.71/1.10 genlinverse( Y, X ) }.
% 0.71/1.10 (708) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlpreds( Z, Y ),
% 0.71/1.10 genlinverse( X, Y ) }.
% 0.71/1.10 (709) {G0,W6,D2,L2,V2,M2} { ! disjointwith( Y, X ), collection( X ) }.
% 0.71/1.10 (710) {G0,W6,D2,L2,V2,M2} { ! disjointwith( X, Y ), collection( X ) }.
% 0.71/1.10 (711) {G0,W7,D2,L2,V2,M2} { ! disjointwith( X, Y ), disjointwith( Y, X )
% 0.71/1.10 }.
% 0.71/1.10 (712) {G0,W11,D2,L3,V3,M3} { ! disjointwith( X, Z ), ! genls( Y, Z ),
% 0.71/1.10 disjointwith( X, Y ) }.
% 0.71/1.10 (713) {G0,W11,D2,L3,V3,M3} { ! disjointwith( Z, X ), ! genls( Y, Z ),
% 0.71/1.10 disjointwith( Y, X ) }.
% 0.71/1.10 (714) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_16_92269 ),
% 0.71/1.10 tptpcol_16_92269( X ) }.
% 0.71/1.10 (715) {G0,W6,D2,L2,V1,M2} { ! tptpcol_16_92269( X ), isa( X,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 (716) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_15_92268 ),
% 0.71/1.10 tptpcol_15_92268( X ) }.
% 0.71/1.10 (717) {G0,W6,D2,L2,V1,M2} { ! tptpcol_15_92268( X ), isa( X,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 (718) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_14_92264 ),
% 0.71/1.10 tptpcol_14_92264( X ) }.
% 0.71/1.10 (719) {G0,W6,D2,L2,V1,M2} { ! tptpcol_14_92264( X ), isa( X,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 (720) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_13_92263 ),
% 0.71/1.10 tptpcol_13_92263( X ) }.
% 0.71/1.10 (721) {G0,W6,D2,L2,V1,M2} { ! tptpcol_13_92263( X ), isa( X,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 (722) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_12_92262 ),
% 0.71/1.10 tptpcol_12_92262( X ) }.
% 0.71/1.10 (723) {G0,W6,D2,L2,V1,M2} { ! tptpcol_12_92262( X ), isa( X,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 (724) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_11_92230 ),
% 0.71/1.10 tptpcol_11_92230( X ) }.
% 0.71/1.10 (725) {G0,W6,D2,L2,V1,M2} { ! tptpcol_11_92230( X ), isa( X,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 (726) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_10_92166 ),
% 0.71/1.10 tptpcol_10_92166( X ) }.
% 0.71/1.10 (727) {G0,W6,D2,L2,V1,M2} { ! tptpcol_10_92166( X ), isa( X,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 (728) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_9_92165 ), tptpcol_9_92165
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (729) {G0,W6,D2,L2,V1,M2} { ! tptpcol_9_92165( X ), isa( X,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 (730) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_8_92164 ), tptpcol_8_92164
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (731) {G0,W6,D2,L2,V1,M2} { ! tptpcol_8_92164( X ), isa( X,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 (732) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_7_92163 ), tptpcol_7_92163
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (733) {G0,W6,D2,L2,V1,M2} { ! tptpcol_7_92163( X ), isa( X,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 (734) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_6_92162 ), tptpcol_6_92162
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (735) {G0,W6,D2,L2,V1,M2} { ! tptpcol_6_92162( X ), isa( X,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 (736) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_5_90114 ), tptpcol_5_90114
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (737) {G0,W6,D2,L2,V1,M2} { ! tptpcol_5_90114( X ), isa( X,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 (738) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_4_90113 ), tptpcol_4_90113
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (739) {G0,W6,D2,L2,V1,M2} { ! tptpcol_4_90113( X ), isa( X,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 (740) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_3_81921 ), tptpcol_3_81921
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (741) {G0,W6,D2,L2,V1,M2} { ! tptpcol_3_81921( X ), isa( X,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 (742) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_1_65536 ), tptpcol_1_65536
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (743) {G0,W6,D2,L2,V1,M2} { ! tptpcol_1_65536( X ), isa( X,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 (744) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_2_65537 ), tptpcol_2_65537
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (745) {G0,W6,D2,L2,V1,M2} { ! tptpcol_2_65537( X ), isa( X,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 (746) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_16_26926 ),
% 0.71/1.10 tptpcol_16_26926( X ) }.
% 0.71/1.10 (747) {G0,W6,D2,L2,V1,M2} { ! tptpcol_16_26926( X ), isa( X,
% 0.71/1.10 c_tptpcol_16_26926 ) }.
% 0.71/1.10 (748) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_15_26925 ),
% 0.71/1.10 tptpcol_15_26925( X ) }.
% 0.71/1.10 (749) {G0,W6,D2,L2,V1,M2} { ! tptpcol_15_26925( X ), isa( X,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 (750) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_14_26921 ),
% 0.71/1.10 tptpcol_14_26921( X ) }.
% 0.71/1.10 (751) {G0,W6,D2,L2,V1,M2} { ! tptpcol_14_26921( X ), isa( X,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 (752) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_13_26920 ),
% 0.71/1.10 tptpcol_13_26920( X ) }.
% 0.71/1.10 (753) {G0,W6,D2,L2,V1,M2} { ! tptpcol_13_26920( X ), isa( X,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 (754) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_12_26919 ),
% 0.71/1.10 tptpcol_12_26919( X ) }.
% 0.71/1.10 (755) {G0,W6,D2,L2,V1,M2} { ! tptpcol_12_26919( X ), isa( X,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 (756) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_11_26887 ),
% 0.71/1.10 tptpcol_11_26887( X ) }.
% 0.71/1.10 (757) {G0,W6,D2,L2,V1,M2} { ! tptpcol_11_26887( X ), isa( X,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 (758) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_10_26886 ),
% 0.71/1.10 tptpcol_10_26886( X ) }.
% 0.71/1.10 (759) {G0,W6,D2,L2,V1,M2} { ! tptpcol_10_26886( X ), isa( X,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 (760) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_9_26885 ), tptpcol_9_26885
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (761) {G0,W6,D2,L2,V1,M2} { ! tptpcol_9_26885( X ), isa( X,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 (762) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_8_26629 ), tptpcol_8_26629
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (763) {G0,W6,D2,L2,V1,M2} { ! tptpcol_8_26629( X ), isa( X,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 (764) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_7_26628 ), tptpcol_7_26628
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (765) {G0,W6,D2,L2,V1,M2} { ! tptpcol_7_26628( X ), isa( X,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 (766) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_6_26627 ), tptpcol_6_26627
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (767) {G0,W6,D2,L2,V1,M2} { ! tptpcol_6_26627( X ), isa( X,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 (768) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_5_24579 ), tptpcol_5_24579
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (769) {G0,W6,D2,L2,V1,M2} { ! tptpcol_5_24579( X ), isa( X,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 (770) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_4_24578 ), tptpcol_4_24578
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (771) {G0,W6,D2,L2,V1,M2} { ! tptpcol_4_24578( X ), isa( X,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 (772) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_3_16386 ), tptpcol_3_16386
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (773) {G0,W6,D2,L2,V1,M2} { ! tptpcol_3_16386( X ), isa( X,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 (774) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_1_1 ), tptpcol_1_1( X )
% 0.71/1.10 }.
% 0.71/1.10 (775) {G0,W6,D2,L2,V1,M2} { ! tptpcol_1_1( X ), isa( X, c_tptpcol_1_1 )
% 0.71/1.10 }.
% 0.71/1.10 (776) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_2_2 ), tptpcol_2_2( X )
% 0.71/1.10 }.
% 0.71/1.10 (777) {G0,W6,D2,L2,V1,M2} { ! tptpcol_2_2( X ), isa( X, c_tptpcol_2_2 )
% 0.71/1.10 }.
% 0.71/1.10 (778) {G0,W6,D2,L2,V2,M2} { ! genls( Y, X ), collection( X ) }.
% 0.71/1.10 (779) {G0,W6,D2,L2,V2,M2} { ! genls( Y, X ), collection( X ) }.
% 0.71/1.10 (780) {G0,W6,D2,L2,V2,M2} { ! genls( X, Y ), collection( X ) }.
% 0.71/1.10 (781) {G0,W6,D2,L2,V2,M2} { ! genls( X, Y ), collection( X ) }.
% 0.71/1.10 (782) {G0,W11,D2,L3,V3,M3} { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y
% 0.71/1.10 ) }.
% 0.71/1.10 (783) {G0,W6,D2,L2,V1,M2} { ! collection( X ), genls( X, X ) }.
% 0.71/1.10 (784) {G0,W6,D2,L2,V1,M2} { ! collection( X ), genls( X, X ) }.
% 0.71/1.10 (785) {G0,W11,D2,L3,V3,M3} { ! genls( Z, X ), ! genls( Y, Z ), genls( Y, X
% 0.71/1.10 ) }.
% 0.71/1.10 (786) {G0,W11,D2,L3,V3,M3} { ! genls( X, Z ), ! genls( Z, Y ), genls( X, Y
% 0.71/1.10 ) }.
% 0.71/1.10 (787) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_transitivebinarypredicate ),
% 0.71/1.10 transitivebinarypredicate( X ) }.
% 0.71/1.10 (788) {G0,W6,D2,L2,V1,M2} { ! transitivebinarypredicate( X ), isa( X,
% 0.71/1.10 c_transitivebinarypredicate ) }.
% 0.71/1.10 (789) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.71/1.10 (790) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.71/1.10 (791) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.71/1.10 (792) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.71/1.10 (793) {G0,W11,D2,L3,V3,M3} { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y )
% 0.71/1.10 }.
% 0.71/1.10 (794) {G0,W2,D2,L1,V0,M1} { mtvisible( c_universalvocabularymt ) }.
% 0.71/1.10 (795) {G0,W9,D2,L3,V2,M3} { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible
% 0.71/1.10 ( X ) }.
% 0.71/1.10 (796) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.71/1.10 (797) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.71/1.10 (798) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.71/1.10 (799) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.71/1.10 (800) {G0,W11,D2,L3,V3,M3} { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X
% 0.71/1.10 , Y ) }.
% 0.71/1.10 (801) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.71/1.10 (802) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.71/1.10 (803) {G0,W2,D2,L1,V0,M1} { mtvisible( c_basekb ) }.
% 0.71/1.10 (804) {G0,W2,D2,L1,V0,M1} { mtvisible( c_unitedstatesgeographypeoplemt )
% 0.71/1.10 }.
% 0.71/1.10 (805) {G0,W4,D2,L1,V0,M1} { ! disjointwith( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Total Proof:
% 0.71/1.10
% 0.71/1.10 subsumption: (6) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_2_2,
% 0.71/1.10 c_tptpcol_1_1 ) }.
% 0.71/1.10 parent0: (634) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_2_2, c_tptpcol_1_1 )
% 0.71/1.10 }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (8) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_3_16386,
% 0.71/1.10 c_tptpcol_2_2 ) }.
% 0.71/1.10 parent0: (636) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_3_16386,
% 0.71/1.10 c_tptpcol_2_2 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (10) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_24578,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 parent0: (638) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_24578,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (12) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_24579,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 parent0: (640) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_24579,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (14) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_26627,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 parent0: (642) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_26627,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (16) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_26628,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 parent0: (644) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_26628,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (18) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 parent0: (646) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (20) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_26885,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0: (648) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_26885,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (22) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_26886,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 parent0: (650) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_26886,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (24) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_26887,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 parent0: (652) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_26887,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (26) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_26919,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 parent0: (654) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_26919,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (28) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_26920,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 parent0: (656) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_26920,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (30) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_26921,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 parent0: (658) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_26921,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (32) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_15_26925,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 parent0: (660) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_15_26925,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (34) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 parent0: (662) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (36) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_2_65537,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 parent0: (664) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_2_65537,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (38) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_3_81921,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 parent0: (666) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_3_81921,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (40) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_90113,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 parent0: (668) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_4_90113,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (42) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_90114,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 parent0: (670) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_5_90114,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (44) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_92162,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 parent0: (672) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_6_92162,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (46) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_92163,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 parent0: (674) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_7_92163,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (48) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_92164,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 parent0: (676) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_8_92164,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (50) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_92165,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 parent0: (678) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_9_92165,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (52) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_92166,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 parent0: (680) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_10_92166,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (54) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_92230,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 parent0: (682) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_11_92230,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (56) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_92262,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 parent0: (684) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_12_92262,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (58) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_92263,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 parent0: (686) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_13_92263,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (60) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_92264,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 parent0: (688) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_14_92264,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (62) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_15_92268,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 parent0: (690) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_15_92268,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (64) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 parent0: (692) {G0,W3,D2,L1,V0,M1} { genls( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (66) {G0,W3,D2,L1,V0,M1} I { disjointwith( c_tptpcol_1_1,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 parent0: (694) {G0,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_1,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (80) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.71/1.10 disjointwith( X, Y ) }.
% 0.71/1.10 parent0: (711) {G0,W7,D2,L2,V2,M2} { ! disjointwith( X, Y ), disjointwith
% 0.71/1.10 ( Y, X ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := Y
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent0: (712) {G0,W11,D2,L3,V3,M3} { ! disjointwith( X, Z ), ! genls( Y,
% 0.71/1.10 Z ), disjointwith( X, Y ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := Y
% 0.71/1.10 Z := Z
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 1 ==> 2
% 0.71/1.10 2 ==> 1
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (164) {G0,W4,D2,L1,V0,M1} I { ! disjointwith(
% 0.71/1.10 c_tptpcol_16_26926, c_tptpcol_16_92269 ) }.
% 0.71/1.10 parent0: (805) {G0,W4,D2,L1,V0,M1} { ! disjointwith( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (819) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_1_1 ) }.
% 0.71/1.10 parent0[1]: (80) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.71/1.10 disjointwith( X, Y ) }.
% 0.71/1.10 parent1[0]: (66) {G0,W3,D2,L1,V0,M1} I { disjointwith( c_tptpcol_1_1,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_1
% 0.71/1.10 Y := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (212) {G1,W3,D2,L1,V0,M1} R(80,66) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_1_1 ) }.
% 0.71/1.10 parent0: (819) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_1_1 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (820) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_2_2 )
% 0.71/1.10 , disjointwith( X, c_tptpcol_3_16386 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (8) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_3_16386,
% 0.71/1.10 c_tptpcol_2_2 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_3_16386
% 0.71/1.10 Z := c_tptpcol_2_2
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (213) {G1,W7,D2,L2,V1,M1} R(81,8) { disjointwith( X,
% 0.71/1.10 c_tptpcol_3_16386 ), ! disjointwith( X, c_tptpcol_2_2 ) }.
% 0.71/1.10 parent0: (820) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_2_2 ),
% 0.71/1.10 disjointwith( X, c_tptpcol_3_16386 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (821) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_3_16386 ), disjointwith( X, c_tptpcol_4_24578 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (10) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_24578,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_4_24578
% 0.71/1.10 Z := c_tptpcol_3_16386
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (214) {G1,W7,D2,L2,V1,M1} R(81,10) { disjointwith( X,
% 0.71/1.10 c_tptpcol_4_24578 ), ! disjointwith( X, c_tptpcol_3_16386 ) }.
% 0.71/1.10 parent0: (821) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_3_16386
% 0.71/1.10 ), disjointwith( X, c_tptpcol_4_24578 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (822) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_4_24578 ), disjointwith( X, c_tptpcol_5_24579 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (12) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_24579,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_5_24579
% 0.71/1.10 Z := c_tptpcol_4_24578
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (215) {G1,W7,D2,L2,V1,M1} R(81,12) { disjointwith( X,
% 0.71/1.10 c_tptpcol_5_24579 ), ! disjointwith( X, c_tptpcol_4_24578 ) }.
% 0.71/1.10 parent0: (822) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_4_24578
% 0.71/1.10 ), disjointwith( X, c_tptpcol_5_24579 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (823) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_5_24579 ), disjointwith( X, c_tptpcol_6_26627 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (14) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_26627,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_6_26627
% 0.71/1.10 Z := c_tptpcol_5_24579
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (216) {G1,W7,D2,L2,V1,M1} R(81,14) { disjointwith( X,
% 0.71/1.10 c_tptpcol_6_26627 ), ! disjointwith( X, c_tptpcol_5_24579 ) }.
% 0.71/1.10 parent0: (823) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_5_24579
% 0.71/1.10 ), disjointwith( X, c_tptpcol_6_26627 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (824) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_6_26627 ), disjointwith( X, c_tptpcol_7_26628 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (16) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_26628,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_7_26628
% 0.71/1.10 Z := c_tptpcol_6_26627
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (217) {G1,W7,D2,L2,V1,M1} R(81,16) { disjointwith( X,
% 0.71/1.10 c_tptpcol_7_26628 ), ! disjointwith( X, c_tptpcol_6_26627 ) }.
% 0.71/1.10 parent0: (824) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_6_26627
% 0.71/1.10 ), disjointwith( X, c_tptpcol_7_26628 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (825) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_7_26628 ), disjointwith( X, c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (18) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_8_26629
% 0.71/1.10 Z := c_tptpcol_7_26628
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (218) {G1,W7,D2,L2,V1,M1} R(81,18) { disjointwith( X,
% 0.71/1.10 c_tptpcol_8_26629 ), ! disjointwith( X, c_tptpcol_7_26628 ) }.
% 0.71/1.10 parent0: (825) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_7_26628
% 0.71/1.10 ), disjointwith( X, c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (826) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_8_26629 ), disjointwith( X, c_tptpcol_9_26885 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (20) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_26885,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_9_26885
% 0.71/1.10 Z := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (219) {G1,W7,D2,L2,V1,M1} R(81,20) { disjointwith( X,
% 0.71/1.10 c_tptpcol_9_26885 ), ! disjointwith( X, c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0: (826) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_8_26629
% 0.71/1.10 ), disjointwith( X, c_tptpcol_9_26885 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (827) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_9_26885 ), disjointwith( X, c_tptpcol_10_26886 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (22) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_26886,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_10_26886
% 0.71/1.10 Z := c_tptpcol_9_26885
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (220) {G1,W7,D2,L2,V1,M1} R(81,22) { disjointwith( X,
% 0.71/1.10 c_tptpcol_10_26886 ), ! disjointwith( X, c_tptpcol_9_26885 ) }.
% 0.71/1.10 parent0: (827) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_9_26885
% 0.71/1.10 ), disjointwith( X, c_tptpcol_10_26886 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (828) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_10_26886 ), disjointwith( X, c_tptpcol_11_26887 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (24) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_26887,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_11_26887
% 0.71/1.10 Z := c_tptpcol_10_26886
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (221) {G1,W7,D2,L2,V1,M1} R(81,24) { disjointwith( X,
% 0.71/1.10 c_tptpcol_11_26887 ), ! disjointwith( X, c_tptpcol_10_26886 ) }.
% 0.71/1.10 parent0: (828) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_10_26886
% 0.71/1.10 ), disjointwith( X, c_tptpcol_11_26887 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (829) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_1_1 )
% 0.71/1.10 , disjointwith( X, c_tptpcol_2_2 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (6) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_2_2, c_tptpcol_1_1
% 0.71/1.10 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_2_2
% 0.71/1.10 Z := c_tptpcol_1_1
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (222) {G1,W7,D2,L2,V1,M1} R(81,6) { disjointwith( X,
% 0.71/1.10 c_tptpcol_2_2 ), ! disjointwith( X, c_tptpcol_1_1 ) }.
% 0.71/1.10 parent0: (829) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_1_1 ),
% 0.71/1.10 disjointwith( X, c_tptpcol_2_2 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (830) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_11_26887 ), disjointwith( X, c_tptpcol_12_26919 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (26) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_26919,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_12_26919
% 0.71/1.10 Z := c_tptpcol_11_26887
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (223) {G1,W7,D2,L2,V1,M1} R(81,26) { disjointwith( X,
% 0.71/1.10 c_tptpcol_12_26919 ), ! disjointwith( X, c_tptpcol_11_26887 ) }.
% 0.71/1.10 parent0: (830) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_11_26887
% 0.71/1.10 ), disjointwith( X, c_tptpcol_12_26919 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (831) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_12_26919 ), disjointwith( X, c_tptpcol_13_26920 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (28) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_26920,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_13_26920
% 0.71/1.10 Z := c_tptpcol_12_26919
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (224) {G1,W7,D2,L2,V1,M1} R(81,28) { disjointwith( X,
% 0.71/1.10 c_tptpcol_13_26920 ), ! disjointwith( X, c_tptpcol_12_26919 ) }.
% 0.71/1.10 parent0: (831) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_12_26919
% 0.71/1.10 ), disjointwith( X, c_tptpcol_13_26920 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (832) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_13_26920 ), disjointwith( X, c_tptpcol_14_26921 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (30) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_26921,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_14_26921
% 0.71/1.10 Z := c_tptpcol_13_26920
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (225) {G1,W7,D2,L2,V1,M1} R(81,30) { disjointwith( X,
% 0.71/1.10 c_tptpcol_14_26921 ), ! disjointwith( X, c_tptpcol_13_26920 ) }.
% 0.71/1.10 parent0: (832) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_13_26920
% 0.71/1.10 ), disjointwith( X, c_tptpcol_14_26921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (833) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_14_26921 ), disjointwith( X, c_tptpcol_15_26925 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (32) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_15_26925,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_15_26925
% 0.71/1.10 Z := c_tptpcol_14_26921
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (226) {G1,W7,D2,L2,V1,M1} R(81,32) { disjointwith( X,
% 0.71/1.10 c_tptpcol_15_26925 ), ! disjointwith( X, c_tptpcol_14_26921 ) }.
% 0.71/1.10 parent0: (833) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_14_26921
% 0.71/1.10 ), disjointwith( X, c_tptpcol_15_26925 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (834) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_15_26925 ), disjointwith( X, c_tptpcol_16_26926 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (34) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_16_26926
% 0.71/1.10 Z := c_tptpcol_15_26925
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (227) {G1,W7,D2,L2,V1,M1} R(81,34) { disjointwith( X,
% 0.71/1.10 c_tptpcol_16_26926 ), ! disjointwith( X, c_tptpcol_15_26925 ) }.
% 0.71/1.10 parent0: (834) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_15_26925
% 0.71/1.10 ), disjointwith( X, c_tptpcol_16_26926 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (835) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_1_65536 ), disjointwith( X, c_tptpcol_2_65537 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (36) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_2_65537,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_2_65537
% 0.71/1.10 Z := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (228) {G1,W7,D2,L2,V1,M1} R(81,36) { disjointwith( X,
% 0.71/1.10 c_tptpcol_2_65537 ), ! disjointwith( X, c_tptpcol_1_65536 ) }.
% 0.71/1.10 parent0: (835) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_1_65536
% 0.71/1.10 ), disjointwith( X, c_tptpcol_2_65537 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (836) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_2_65537 ), disjointwith( X, c_tptpcol_3_81921 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (38) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_3_81921,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_3_81921
% 0.71/1.10 Z := c_tptpcol_2_65537
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (229) {G1,W7,D2,L2,V1,M1} R(81,38) { disjointwith( X,
% 0.71/1.10 c_tptpcol_3_81921 ), ! disjointwith( X, c_tptpcol_2_65537 ) }.
% 0.71/1.10 parent0: (836) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_2_65537
% 0.71/1.10 ), disjointwith( X, c_tptpcol_3_81921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (837) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_3_81921 ), disjointwith( X, c_tptpcol_4_90113 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (40) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_4_90113,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_4_90113
% 0.71/1.10 Z := c_tptpcol_3_81921
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (230) {G1,W7,D2,L2,V1,M1} R(81,40) { disjointwith( X,
% 0.71/1.10 c_tptpcol_4_90113 ), ! disjointwith( X, c_tptpcol_3_81921 ) }.
% 0.71/1.10 parent0: (837) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_3_81921
% 0.71/1.10 ), disjointwith( X, c_tptpcol_4_90113 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (838) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_4_90113 ), disjointwith( X, c_tptpcol_5_90114 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (42) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_5_90114,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_5_90114
% 0.71/1.10 Z := c_tptpcol_4_90113
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (231) {G1,W7,D2,L2,V1,M1} R(81,42) { disjointwith( X,
% 0.71/1.10 c_tptpcol_5_90114 ), ! disjointwith( X, c_tptpcol_4_90113 ) }.
% 0.71/1.10 parent0: (838) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_4_90113
% 0.71/1.10 ), disjointwith( X, c_tptpcol_5_90114 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (839) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_5_90114 ), disjointwith( X, c_tptpcol_6_92162 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (44) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_6_92162,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_6_92162
% 0.71/1.10 Z := c_tptpcol_5_90114
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (232) {G1,W7,D2,L2,V1,M1} R(81,44) { disjointwith( X,
% 0.71/1.10 c_tptpcol_6_92162 ), ! disjointwith( X, c_tptpcol_5_90114 ) }.
% 0.71/1.10 parent0: (839) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_5_90114
% 0.71/1.10 ), disjointwith( X, c_tptpcol_6_92162 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (840) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_6_92162 ), disjointwith( X, c_tptpcol_7_92163 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (46) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_7_92163,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_7_92163
% 0.71/1.10 Z := c_tptpcol_6_92162
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (233) {G1,W7,D2,L2,V1,M1} R(81,46) { disjointwith( X,
% 0.71/1.10 c_tptpcol_7_92163 ), ! disjointwith( X, c_tptpcol_6_92162 ) }.
% 0.71/1.10 parent0: (840) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_6_92162
% 0.71/1.10 ), disjointwith( X, c_tptpcol_7_92163 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (841) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_7_92163 ), disjointwith( X, c_tptpcol_8_92164 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (48) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_8_92164,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_8_92164
% 0.71/1.10 Z := c_tptpcol_7_92163
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (234) {G1,W7,D2,L2,V1,M1} R(81,48) { disjointwith( X,
% 0.71/1.10 c_tptpcol_8_92164 ), ! disjointwith( X, c_tptpcol_7_92163 ) }.
% 0.71/1.10 parent0: (841) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_7_92163
% 0.71/1.10 ), disjointwith( X, c_tptpcol_8_92164 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (842) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_8_92164 ), disjointwith( X, c_tptpcol_9_92165 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (50) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_9_92165,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_9_92165
% 0.71/1.10 Z := c_tptpcol_8_92164
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (235) {G1,W7,D2,L2,V1,M1} R(81,50) { disjointwith( X,
% 0.71/1.10 c_tptpcol_9_92165 ), ! disjointwith( X, c_tptpcol_8_92164 ) }.
% 0.71/1.10 parent0: (842) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_8_92164
% 0.71/1.10 ), disjointwith( X, c_tptpcol_9_92165 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (843) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_9_92165 ), disjointwith( X, c_tptpcol_10_92166 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (52) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_10_92166,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_10_92166
% 0.71/1.10 Z := c_tptpcol_9_92165
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (236) {G1,W7,D2,L2,V1,M1} R(81,52) { disjointwith( X,
% 0.71/1.10 c_tptpcol_10_92166 ), ! disjointwith( X, c_tptpcol_9_92165 ) }.
% 0.71/1.10 parent0: (843) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_9_92165
% 0.71/1.10 ), disjointwith( X, c_tptpcol_10_92166 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (844) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_10_92166 ), disjointwith( X, c_tptpcol_11_92230 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (54) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_11_92230,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_11_92230
% 0.71/1.10 Z := c_tptpcol_10_92166
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (237) {G1,W7,D2,L2,V1,M1} R(81,54) { disjointwith( X,
% 0.71/1.10 c_tptpcol_11_92230 ), ! disjointwith( X, c_tptpcol_10_92166 ) }.
% 0.71/1.10 parent0: (844) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_10_92166
% 0.71/1.10 ), disjointwith( X, c_tptpcol_11_92230 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (845) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_11_92230 ), disjointwith( X, c_tptpcol_12_92262 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (56) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_12_92262,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_12_92262
% 0.71/1.10 Z := c_tptpcol_11_92230
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (238) {G1,W7,D2,L2,V1,M1} R(81,56) { disjointwith( X,
% 0.71/1.10 c_tptpcol_12_92262 ), ! disjointwith( X, c_tptpcol_11_92230 ) }.
% 0.71/1.10 parent0: (845) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_11_92230
% 0.71/1.10 ), disjointwith( X, c_tptpcol_12_92262 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (846) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_12_92262 ), disjointwith( X, c_tptpcol_13_92263 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (58) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_13_92263,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_13_92263
% 0.71/1.10 Z := c_tptpcol_12_92262
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (239) {G1,W7,D2,L2,V1,M1} R(81,58) { disjointwith( X,
% 0.71/1.10 c_tptpcol_13_92263 ), ! disjointwith( X, c_tptpcol_12_92262 ) }.
% 0.71/1.10 parent0: (846) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_12_92262
% 0.71/1.10 ), disjointwith( X, c_tptpcol_13_92263 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 *** allocated 50625 integers for clauses
% 0.71/1.10 resolution: (847) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_13_92263 ), disjointwith( X, c_tptpcol_14_92264 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (60) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_14_92264,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_14_92264
% 0.71/1.10 Z := c_tptpcol_13_92263
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (240) {G1,W7,D2,L2,V1,M1} R(81,60) { disjointwith( X,
% 0.71/1.10 c_tptpcol_14_92264 ), ! disjointwith( X, c_tptpcol_13_92263 ) }.
% 0.71/1.10 parent0: (847) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_13_92263
% 0.71/1.10 ), disjointwith( X, c_tptpcol_14_92264 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (848) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_14_92264 ), disjointwith( X, c_tptpcol_15_92268 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (62) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_15_92268,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_15_92268
% 0.71/1.10 Z := c_tptpcol_14_92264
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (241) {G1,W7,D2,L2,V1,M1} R(81,62) { disjointwith( X,
% 0.71/1.10 c_tptpcol_15_92268 ), ! disjointwith( X, c_tptpcol_14_92264 ) }.
% 0.71/1.10 parent0: (848) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_14_92264
% 0.71/1.10 ), disjointwith( X, c_tptpcol_15_92268 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (849) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X,
% 0.71/1.10 c_tptpcol_15_92268 ), disjointwith( X, c_tptpcol_16_92269 ) }.
% 0.71/1.10 parent0[2]: (81) {G0,W11,D2,L3,V3,M1} I { ! disjointwith( X, Z ),
% 0.71/1.10 disjointwith( X, Y ), ! genls( Y, Z ) }.
% 0.71/1.10 parent1[0]: (64) {G0,W3,D2,L1,V0,M1} I { genls( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 Y := c_tptpcol_16_92269
% 0.71/1.10 Z := c_tptpcol_15_92268
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (242) {G1,W7,D2,L2,V1,M1} R(81,64) { disjointwith( X,
% 0.71/1.10 c_tptpcol_16_92269 ), ! disjointwith( X, c_tptpcol_15_92268 ) }.
% 0.71/1.10 parent0: (849) {G1,W7,D2,L2,V1,M2} { ! disjointwith( X, c_tptpcol_15_92268
% 0.71/1.10 ), disjointwith( X, c_tptpcol_16_92269 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := X
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 1
% 0.71/1.10 1 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (850) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_2_2 ) }.
% 0.71/1.10 parent0[1]: (222) {G1,W7,D2,L2,V1,M1} R(81,6) { disjointwith( X,
% 0.71/1.10 c_tptpcol_2_2 ), ! disjointwith( X, c_tptpcol_1_1 ) }.
% 0.71/1.10 parent1[0]: (212) {G1,W3,D2,L1,V0,M1} R(80,66) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_1_1 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (409) {G2,W3,D2,L1,V0,M1} R(222,212) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_2_2 ) }.
% 0.71/1.10 parent0: (850) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_2_2 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (851) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 parent0[1]: (213) {G1,W7,D2,L2,V1,M1} R(81,8) { disjointwith( X,
% 0.71/1.10 c_tptpcol_3_16386 ), ! disjointwith( X, c_tptpcol_2_2 ) }.
% 0.71/1.10 parent1[0]: (409) {G2,W3,D2,L1,V0,M1} R(222,212) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_2_2 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (410) {G3,W3,D2,L1,V0,M1} R(409,213) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_3_16386 ) }.
% 0.71/1.10 parent0: (851) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_3_16386 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (852) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 parent0[1]: (214) {G1,W7,D2,L2,V1,M1} R(81,10) { disjointwith( X,
% 0.71/1.10 c_tptpcol_4_24578 ), ! disjointwith( X, c_tptpcol_3_16386 ) }.
% 0.71/1.10 parent1[0]: (410) {G3,W3,D2,L1,V0,M1} R(409,213) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_3_16386 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (413) {G4,W3,D2,L1,V0,M1} R(410,214) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_4_24578 ) }.
% 0.71/1.10 parent0: (852) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_4_24578 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (853) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 parent0[1]: (215) {G1,W7,D2,L2,V1,M1} R(81,12) { disjointwith( X,
% 0.71/1.10 c_tptpcol_5_24579 ), ! disjointwith( X, c_tptpcol_4_24578 ) }.
% 0.71/1.10 parent1[0]: (413) {G4,W3,D2,L1,V0,M1} R(410,214) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_4_24578 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (416) {G5,W3,D2,L1,V0,M1} R(413,215) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_5_24579 ) }.
% 0.71/1.10 parent0: (853) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_5_24579 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (854) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 parent0[1]: (216) {G1,W7,D2,L2,V1,M1} R(81,14) { disjointwith( X,
% 0.71/1.10 c_tptpcol_6_26627 ), ! disjointwith( X, c_tptpcol_5_24579 ) }.
% 0.71/1.10 parent1[0]: (416) {G5,W3,D2,L1,V0,M1} R(413,215) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_5_24579 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (419) {G6,W3,D2,L1,V0,M1} R(416,216) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_6_26627 ) }.
% 0.71/1.10 parent0: (854) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_6_26627 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (855) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 parent0[1]: (217) {G1,W7,D2,L2,V1,M1} R(81,16) { disjointwith( X,
% 0.71/1.10 c_tptpcol_7_26628 ), ! disjointwith( X, c_tptpcol_6_26627 ) }.
% 0.71/1.10 parent1[0]: (419) {G6,W3,D2,L1,V0,M1} R(416,216) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_6_26627 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (422) {G7,W3,D2,L1,V0,M1} R(419,217) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_7_26628 ) }.
% 0.71/1.10 parent0: (855) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_7_26628 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (856) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0[1]: (218) {G1,W7,D2,L2,V1,M1} R(81,18) { disjointwith( X,
% 0.71/1.10 c_tptpcol_8_26629 ), ! disjointwith( X, c_tptpcol_7_26628 ) }.
% 0.71/1.10 parent1[0]: (422) {G7,W3,D2,L1,V0,M1} R(419,217) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_7_26628 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (425) {G8,W3,D2,L1,V0,M1} R(422,218) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0: (856) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_1_65536,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (857) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 parent0[1]: (80) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.71/1.10 disjointwith( X, Y ) }.
% 0.71/1.10 parent1[0]: (425) {G8,W3,D2,L1,V0,M1} R(422,218) { disjointwith(
% 0.71/1.10 c_tptpcol_1_65536, c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_1_65536
% 0.71/1.10 Y := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (429) {G9,W3,D2,L1,V0,M1} R(425,80) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_1_65536 ) }.
% 0.71/1.10 parent0: (857) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_1_65536 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (858) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 parent0[1]: (228) {G1,W7,D2,L2,V1,M1} R(81,36) { disjointwith( X,
% 0.71/1.10 c_tptpcol_2_65537 ), ! disjointwith( X, c_tptpcol_1_65536 ) }.
% 0.71/1.10 parent1[0]: (429) {G9,W3,D2,L1,V0,M1} R(425,80) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_1_65536 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (454) {G10,W3,D2,L1,V0,M1} R(228,429) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_2_65537 ) }.
% 0.71/1.10 parent0: (858) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_2_65537 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (859) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 parent0[1]: (229) {G1,W7,D2,L2,V1,M1} R(81,38) { disjointwith( X,
% 0.71/1.10 c_tptpcol_3_81921 ), ! disjointwith( X, c_tptpcol_2_65537 ) }.
% 0.71/1.10 parent1[0]: (454) {G10,W3,D2,L1,V0,M1} R(228,429) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_2_65537 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (471) {G11,W3,D2,L1,V0,M1} R(229,454) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_3_81921 ) }.
% 0.71/1.10 parent0: (859) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_3_81921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (860) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 parent0[1]: (230) {G1,W7,D2,L2,V1,M1} R(81,40) { disjointwith( X,
% 0.71/1.10 c_tptpcol_4_90113 ), ! disjointwith( X, c_tptpcol_3_81921 ) }.
% 0.71/1.10 parent1[0]: (471) {G11,W3,D2,L1,V0,M1} R(229,454) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_3_81921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (481) {G12,W3,D2,L1,V0,M1} R(230,471) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_4_90113 ) }.
% 0.71/1.10 parent0: (860) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_4_90113 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (861) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 parent0[1]: (231) {G1,W7,D2,L2,V1,M1} R(81,42) { disjointwith( X,
% 0.71/1.10 c_tptpcol_5_90114 ), ! disjointwith( X, c_tptpcol_4_90113 ) }.
% 0.71/1.10 parent1[0]: (481) {G12,W3,D2,L1,V0,M1} R(230,471) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_4_90113 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (491) {G13,W3,D2,L1,V0,M1} R(231,481) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_5_90114 ) }.
% 0.71/1.10 parent0: (861) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_5_90114 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (862) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 parent0[1]: (232) {G1,W7,D2,L2,V1,M1} R(81,44) { disjointwith( X,
% 0.71/1.10 c_tptpcol_6_92162 ), ! disjointwith( X, c_tptpcol_5_90114 ) }.
% 0.71/1.10 parent1[0]: (491) {G13,W3,D2,L1,V0,M1} R(231,481) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_5_90114 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (501) {G14,W3,D2,L1,V0,M1} R(232,491) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_6_92162 ) }.
% 0.71/1.10 parent0: (862) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_6_92162 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (863) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 parent0[1]: (233) {G1,W7,D2,L2,V1,M1} R(81,46) { disjointwith( X,
% 0.71/1.10 c_tptpcol_7_92163 ), ! disjointwith( X, c_tptpcol_6_92162 ) }.
% 0.71/1.10 parent1[0]: (501) {G14,W3,D2,L1,V0,M1} R(232,491) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_6_92162 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (511) {G15,W3,D2,L1,V0,M1} R(233,501) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_7_92163 ) }.
% 0.71/1.10 parent0: (863) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_7_92163 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (864) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 parent0[1]: (234) {G1,W7,D2,L2,V1,M1} R(81,48) { disjointwith( X,
% 0.71/1.10 c_tptpcol_8_92164 ), ! disjointwith( X, c_tptpcol_7_92163 ) }.
% 0.71/1.10 parent1[0]: (511) {G15,W3,D2,L1,V0,M1} R(233,501) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_7_92163 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (521) {G16,W3,D2,L1,V0,M1} R(234,511) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_8_92164 ) }.
% 0.71/1.10 parent0: (864) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_8_92164 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (865) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 parent0[1]: (235) {G1,W7,D2,L2,V1,M1} R(81,50) { disjointwith( X,
% 0.71/1.10 c_tptpcol_9_92165 ), ! disjointwith( X, c_tptpcol_8_92164 ) }.
% 0.71/1.10 parent1[0]: (521) {G16,W3,D2,L1,V0,M1} R(234,511) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_8_92164 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (531) {G17,W3,D2,L1,V0,M1} R(235,521) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_9_92165 ) }.
% 0.71/1.10 parent0: (865) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_9_92165 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (866) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 parent0[1]: (236) {G1,W7,D2,L2,V1,M1} R(81,52) { disjointwith( X,
% 0.71/1.10 c_tptpcol_10_92166 ), ! disjointwith( X, c_tptpcol_9_92165 ) }.
% 0.71/1.10 parent1[0]: (531) {G17,W3,D2,L1,V0,M1} R(235,521) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_9_92165 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (541) {G18,W3,D2,L1,V0,M1} R(236,531) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_10_92166 ) }.
% 0.71/1.10 parent0: (866) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_10_92166 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (867) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 parent0[1]: (237) {G1,W7,D2,L2,V1,M1} R(81,54) { disjointwith( X,
% 0.71/1.10 c_tptpcol_11_92230 ), ! disjointwith( X, c_tptpcol_10_92166 ) }.
% 0.71/1.10 parent1[0]: (541) {G18,W3,D2,L1,V0,M1} R(236,531) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_10_92166 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (551) {G19,W3,D2,L1,V0,M1} R(237,541) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_11_92230 ) }.
% 0.71/1.10 parent0: (867) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_11_92230 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (868) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 parent0[1]: (238) {G1,W7,D2,L2,V1,M1} R(81,56) { disjointwith( X,
% 0.71/1.10 c_tptpcol_12_92262 ), ! disjointwith( X, c_tptpcol_11_92230 ) }.
% 0.71/1.10 parent1[0]: (551) {G19,W3,D2,L1,V0,M1} R(237,541) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_11_92230 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (561) {G20,W3,D2,L1,V0,M1} R(238,551) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_12_92262 ) }.
% 0.71/1.10 parent0: (868) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_12_92262 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (869) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 parent0[1]: (239) {G1,W7,D2,L2,V1,M1} R(81,58) { disjointwith( X,
% 0.71/1.10 c_tptpcol_13_92263 ), ! disjointwith( X, c_tptpcol_12_92262 ) }.
% 0.71/1.10 parent1[0]: (561) {G20,W3,D2,L1,V0,M1} R(238,551) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_12_92262 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (571) {G21,W3,D2,L1,V0,M1} R(239,561) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_13_92263 ) }.
% 0.71/1.10 parent0: (869) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_13_92263 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (870) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 parent0[1]: (240) {G1,W7,D2,L2,V1,M1} R(81,60) { disjointwith( X,
% 0.71/1.10 c_tptpcol_14_92264 ), ! disjointwith( X, c_tptpcol_13_92263 ) }.
% 0.71/1.10 parent1[0]: (571) {G21,W3,D2,L1,V0,M1} R(239,561) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_13_92263 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (581) {G22,W3,D2,L1,V0,M1} R(240,571) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_14_92264 ) }.
% 0.71/1.10 parent0: (870) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_14_92264 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (871) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 parent0[1]: (241) {G1,W7,D2,L2,V1,M1} R(81,62) { disjointwith( X,
% 0.71/1.10 c_tptpcol_15_92268 ), ! disjointwith( X, c_tptpcol_14_92264 ) }.
% 0.71/1.10 parent1[0]: (581) {G22,W3,D2,L1,V0,M1} R(240,571) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_14_92264 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (591) {G23,W3,D2,L1,V0,M1} R(241,581) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_15_92268 ) }.
% 0.71/1.10 parent0: (871) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_15_92268 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (872) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 parent0[1]: (242) {G1,W7,D2,L2,V1,M1} R(81,64) { disjointwith( X,
% 0.71/1.10 c_tptpcol_16_92269 ), ! disjointwith( X, c_tptpcol_15_92268 ) }.
% 0.71/1.10 parent1[0]: (591) {G23,W3,D2,L1,V0,M1} R(241,581) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_15_92268 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (601) {G24,W3,D2,L1,V0,M1} R(242,591) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_16_92269 ) }.
% 0.71/1.10 parent0: (872) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_8_26629,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (873) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0[1]: (80) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.71/1.10 disjointwith( X, Y ) }.
% 0.71/1.10 parent1[0]: (601) {G24,W3,D2,L1,V0,M1} R(242,591) { disjointwith(
% 0.71/1.10 c_tptpcol_8_26629, c_tptpcol_16_92269 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_8_26629
% 0.71/1.10 Y := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (602) {G25,W3,D2,L1,V0,M1} R(601,80) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent0: (873) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (874) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 parent0[1]: (219) {G1,W7,D2,L2,V1,M1} R(81,20) { disjointwith( X,
% 0.71/1.10 c_tptpcol_9_26885 ), ! disjointwith( X, c_tptpcol_8_26629 ) }.
% 0.71/1.10 parent1[0]: (602) {G25,W3,D2,L1,V0,M1} R(601,80) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_8_26629 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (604) {G26,W3,D2,L1,V0,M1} R(602,219) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_9_26885 ) }.
% 0.71/1.10 parent0: (874) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_9_26885 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (875) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 parent0[1]: (220) {G1,W7,D2,L2,V1,M1} R(81,22) { disjointwith( X,
% 0.71/1.10 c_tptpcol_10_26886 ), ! disjointwith( X, c_tptpcol_9_26885 ) }.
% 0.71/1.10 parent1[0]: (604) {G26,W3,D2,L1,V0,M1} R(602,219) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_9_26885 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (605) {G27,W3,D2,L1,V0,M1} R(604,220) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_10_26886 ) }.
% 0.71/1.10 parent0: (875) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_10_26886 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (876) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 parent0[1]: (221) {G1,W7,D2,L2,V1,M1} R(81,24) { disjointwith( X,
% 0.71/1.10 c_tptpcol_11_26887 ), ! disjointwith( X, c_tptpcol_10_26886 ) }.
% 0.71/1.10 parent1[0]: (605) {G27,W3,D2,L1,V0,M1} R(604,220) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_10_26886 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (608) {G28,W3,D2,L1,V0,M1} R(605,221) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_11_26887 ) }.
% 0.71/1.10 parent0: (876) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_11_26887 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (877) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 parent0[1]: (223) {G1,W7,D2,L2,V1,M1} R(81,26) { disjointwith( X,
% 0.71/1.10 c_tptpcol_12_26919 ), ! disjointwith( X, c_tptpcol_11_26887 ) }.
% 0.71/1.10 parent1[0]: (608) {G28,W3,D2,L1,V0,M1} R(605,221) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_11_26887 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (611) {G29,W3,D2,L1,V0,M1} R(608,223) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_12_26919 ) }.
% 0.71/1.10 parent0: (877) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_12_26919 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (878) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 parent0[1]: (224) {G1,W7,D2,L2,V1,M1} R(81,28) { disjointwith( X,
% 0.71/1.10 c_tptpcol_13_26920 ), ! disjointwith( X, c_tptpcol_12_26919 ) }.
% 0.71/1.10 parent1[0]: (611) {G29,W3,D2,L1,V0,M1} R(608,223) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_12_26919 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (614) {G30,W3,D2,L1,V0,M1} R(611,224) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_13_26920 ) }.
% 0.71/1.10 parent0: (878) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_13_26920 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (879) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 parent0[1]: (225) {G1,W7,D2,L2,V1,M1} R(81,30) { disjointwith( X,
% 0.71/1.10 c_tptpcol_14_26921 ), ! disjointwith( X, c_tptpcol_13_26920 ) }.
% 0.71/1.10 parent1[0]: (614) {G30,W3,D2,L1,V0,M1} R(611,224) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_13_26920 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (617) {G31,W3,D2,L1,V0,M1} R(614,225) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_14_26921 ) }.
% 0.71/1.10 parent0: (879) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_14_26921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (880) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 parent0[1]: (226) {G1,W7,D2,L2,V1,M1} R(81,32) { disjointwith( X,
% 0.71/1.10 c_tptpcol_15_26925 ), ! disjointwith( X, c_tptpcol_14_26921 ) }.
% 0.71/1.10 parent1[0]: (617) {G31,W3,D2,L1,V0,M1} R(614,225) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_14_26921 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (620) {G32,W3,D2,L1,V0,M1} R(617,226) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_15_26925 ) }.
% 0.71/1.10 parent0: (880) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_15_26925 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (881) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_16_26926 ) }.
% 0.71/1.10 parent0[1]: (227) {G1,W7,D2,L2,V1,M1} R(81,34) { disjointwith( X,
% 0.71/1.10 c_tptpcol_16_26926 ), ! disjointwith( X, c_tptpcol_15_26925 ) }.
% 0.71/1.10 parent1[0]: (620) {G32,W3,D2,L1,V0,M1} R(617,226) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_15_26925 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (623) {G33,W3,D2,L1,V0,M1} R(620,227) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_16_26926 ) }.
% 0.71/1.10 parent0: (881) {G2,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_92269,
% 0.71/1.10 c_tptpcol_16_26926 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 0 ==> 0
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (882) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 parent0[1]: (80) {G0,W7,D2,L2,V2,M1} I { disjointwith( Y, X ), !
% 0.71/1.10 disjointwith( X, Y ) }.
% 0.71/1.10 parent1[0]: (623) {G33,W3,D2,L1,V0,M1} R(620,227) { disjointwith(
% 0.71/1.10 c_tptpcol_16_92269, c_tptpcol_16_26926 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 X := c_tptpcol_16_92269
% 0.71/1.10 Y := c_tptpcol_16_26926
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 resolution: (883) {G1,W0,D0,L0,V0,M0} { }.
% 0.71/1.10 parent0[0]: (164) {G0,W4,D2,L1,V0,M1} I { ! disjointwith(
% 0.71/1.10 c_tptpcol_16_26926, c_tptpcol_16_92269 ) }.
% 0.71/1.10 parent1[0]: (882) {G1,W3,D2,L1,V0,M1} { disjointwith( c_tptpcol_16_26926,
% 0.71/1.10 c_tptpcol_16_92269 ) }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 substitution1:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 subsumption: (626) {G34,W0,D0,L0,V0,M0} R(623,80);r(164) { }.
% 0.71/1.10 parent0: (883) {G1,W0,D0,L0,V0,M0} { }.
% 0.71/1.10 substitution0:
% 0.71/1.10 end
% 0.71/1.10 permutation0:
% 0.71/1.10 end
% 0.71/1.10
% 0.71/1.10 Proof check complete!
% 0.71/1.10
% 0.71/1.10 Memory use:
% 0.71/1.10
% 0.71/1.10 space for terms: 5972
% 0.71/1.10 space for clauses: 29164
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 clauses generated: 1195
% 0.71/1.10 clauses kept: 627
% 0.71/1.10 clauses selected: 436
% 0.71/1.10 clauses deleted: 2
% 0.71/1.10 clauses inuse deleted: 0
% 0.71/1.10
% 0.71/1.10 subsentry: 624
% 0.71/1.10 literals s-matched: 548
% 0.71/1.10 literals matched: 548
% 0.71/1.10 full subsumption: 2
% 0.71/1.10
% 0.71/1.10 checksum: 1890329842
% 0.71/1.10
% 0.71/1.10
% 0.71/1.10 Bliksem ended
%------------------------------------------------------------------------------