%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CSR066+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.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:38 EDT 2022
% Result : Theorem 0.43s 1.09s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : CSR066+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n025.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 01:41:21 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.43/1.09 *** allocated 10000 integers for termspace/termends
% 0.43/1.09 *** allocated 10000 integers for clauses
% 0.43/1.09 *** allocated 10000 integers for justifications
% 0.43/1.09 Bliksem 1.12
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Automatic Strategy Selection
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Clauses:
% 0.43/1.09
% 0.43/1.09 { genlmt( c_cycorpproductsmt, c_basekb ) }.
% 0.43/1.09 { genlmt( c_cycnounlearnermt, c_cycorpproductsmt ) }.
% 0.43/1.09 { genlmt( f_contentmtofcdafromeventfn( f_urlreferentfn( f_urlfn(
% 0.43/1.09 s_http_webnjiteducjohnsontreebiochhtm ) ), c_translation_21 ),
% 0.43/1.09 c_machinelearningspindleheadmt ) }.
% 0.43/1.09 { ! isa( X, Y ), ! relationexistsall( Z, T, Y ), isa( f_relationexistsallfn
% 0.43/1.09 ( X, Z, T, Y ), T ) }.
% 0.43/1.09 { resultisaarg( c_relationexistsallfn, n_3 ) }.
% 0.43/1.09 { transitivebinarypredicate( c_genlmt ) }.
% 0.43/1.09 { genlmt( c_machinelearningspindleheadmt, c_cycnounlearnermt ) }.
% 0.43/1.09 { genlmt( c_basekb, c_universalvocabularymt ) }.
% 0.43/1.09 { ! shavingrazor_manual( X ), tptp_8_271( f_relationexistsallfn( X,
% 0.43/1.09 c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual ), X ) }.
% 0.43/1.09 { relationexistsall( c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ) }.
% 0.43/1.09 { shavingrazor_manual( c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith( Y, Z ) }.
% 0.43/1.09 { ! genlinverse( X, Z ), ! genlinverse( Z, Y ), genlpreds( X, Y ) }.
% 0.43/1.09 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.43/1.09 { ! genlpreds( Y, X ), predicate( X ) }.
% 0.43/1.09 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.43/1.09 { ! genlpreds( X, Y ), predicate( X ) }.
% 0.43/1.09 { ! genlpreds( X, Z ), ! genlpreds( Z, Y ), genlpreds( X, Y ) }.
% 0.43/1.09 { ! predicate( X ), genlpreds( X, X ) }.
% 0.43/1.09 { ! predicate( X ), genlpreds( X, X ) }.
% 0.43/1.09 { ! genlinverse( Y, X ), binarypredicate( X ) }.
% 0.43/1.09 { ! genlinverse( X, Y ), binarypredicate( X ) }.
% 0.43/1.09 { ! genlinverse( Z, X ), ! genlpreds( Y, Z ), genlinverse( Y, X ) }.
% 0.43/1.09 { ! genlinverse( X, Z ), ! genlpreds( Z, Y ), genlinverse( X, Y ) }.
% 0.43/1.09 { ! disjointwith( Y, X ), collection( X ) }.
% 0.43/1.09 { ! disjointwith( X, Y ), collection( X ) }.
% 0.43/1.09 { ! disjointwith( X, Y ), disjointwith( Y, X ) }.
% 0.43/1.09 { ! disjointwith( X, Z ), ! genls( Y, Z ), disjointwith( X, Y ) }.
% 0.43/1.09 { ! disjointwith( Z, X ), ! genls( Y, Z ), disjointwith( Y, X ) }.
% 0.43/1.09 { ! isa( X, c_shavingrazor_manual ), shavingrazor_manual( X ) }.
% 0.43/1.09 { ! shavingrazor_manual( X ), isa( X, c_shavingrazor_manual ) }.
% 0.43/1.09 { ! isa( X, c_tptpcol_16_25972 ), tptpcol_16_25972( X ) }.
% 0.43/1.09 { ! tptpcol_16_25972( X ), isa( X, c_tptpcol_16_25972 ) }.
% 0.43/1.09 { ! tptp_8_271( Y, X ), razor( X ) }.
% 0.43/1.09 { ! tptp_8_271( X, Y ), tptpcol_5_24579( X ) }.
% 0.43/1.09 { ! relationexistsall( Y, Z, X ), collection( X ) }.
% 0.43/1.09 { ! relationexistsall( Y, X, Z ), collection( X ) }.
% 0.43/1.09 { ! relationexistsall( X, Y, Z ), binarypredicate( X ) }.
% 0.43/1.09 { ! isa( X, c_transitivebinarypredicate ), transitivebinarypredicate( X ) }
% 0.43/1.09 .
% 0.43/1.09 { ! transitivebinarypredicate( X ), isa( X, c_transitivebinarypredicate ) }
% 0.43/1.09 .
% 0.43/1.09 { ! isa( Y, X ), collection( X ) }.
% 0.43/1.09 { ! isa( Y, X ), collection( X ) }.
% 0.43/1.09 { ! isa( X, Y ), thing( X ) }.
% 0.43/1.09 { ! isa( X, Y ), thing( X ) }.
% 0.43/1.09 { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y ) }.
% 0.43/1.09 { natfunction( f_relationexistsallfn( X, Y, Z, T ), c_relationexistsallfn )
% 0.43/1.09 }.
% 0.43/1.09 { natargument( f_relationexistsallfn( X, Y, Z, T ), n_1, X ) }.
% 0.43/1.09 { natargument( f_relationexistsallfn( X, Y, Z, T ), n_2, Y ) }.
% 0.43/1.09 { natargument( f_relationexistsallfn( X, Y, Z, T ), n_3, Z ) }.
% 0.43/1.09 { natargument( f_relationexistsallfn( X, Y, Z, T ), n_4, T ) }.
% 0.43/1.09 { thing( f_relationexistsallfn( X, Y, Z, T ) ) }.
% 0.43/1.09 { ! resultisaarg( Y, X ), positiveinteger( X ) }.
% 0.43/1.09 { ! resultisaarg( X, Y ), function_denotational( X ) }.
% 0.43/1.09 { natfunction( f_urlfn( X ), c_urlfn ) }.
% 0.43/1.09 { natargument( f_urlfn( X ), n_1, X ) }.
% 0.43/1.09 { uniformresourcelocator( f_urlfn( X ) ) }.
% 0.43/1.09 { natfunction( f_urlreferentfn( X ), c_urlreferentfn ) }.
% 0.43/1.09 { natargument( f_urlreferentfn( X ), n_1, X ) }.
% 0.43/1.09 { computerdataartifact( f_urlreferentfn( X ) ) }.
% 0.43/1.09 { natfunction( f_contentmtofcdafromeventfn( X, Y ),
% 0.43/1.09 c_contentmtofcdafromeventfn ) }.
% 0.43/1.09 { natargument( f_contentmtofcdafromeventfn( X, Y ), n_1, X ) }.
% 0.43/1.09 { natargument( f_contentmtofcdafromeventfn( X, Y ), n_2, Y ) }.
% 0.43/1.09 { microtheory( f_contentmtofcdafromeventfn( X, Y ) ) }.
% 0.43/1.09 { mtvisible( c_universalvocabularymt ) }.
% 0.43/1.09 { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible( X ) }.
% 0.43/1.09 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.43/1.09 { ! genlmt( Y, X ), microtheory( X ) }.
% 0.43/1.09 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.43/1.09 { ! genlmt( X, Y ), microtheory( X ) }.
% 0.43/1.09 { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X, Y ) }.
% 0.43/1.09 { ! microtheory( X ), genlmt( X, X ) }.
% 0.43/1.09 { ! microtheory( X ), genlmt( X, X ) }.
% 0.43/1.09 { mtvisible( c_basekb ) }.
% 0.43/1.09 { mtvisible( f_contentmtofcdafromeventfn( f_urlreferentfn( f_urlfn(
% 0.43/1.09 s_http_webnjiteducjohnsontreebiochhtm ) ), c_translation_21 ) ) }.
% 0.43/1.09 { ! tptp_8_271( X, c_theprototypicalshavingrazor_manual ), !
% 0.43/1.09 tptpcol_16_25972( X ) }.
% 0.43/1.09
% 0.43/1.09 percentage equality = 0.000000, percentage horn = 1.000000
% 0.43/1.09 This is a near-Horn, non-equality problem
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Options Used:
% 0.43/1.09
% 0.43/1.09 useres = 1
% 0.43/1.09 useparamod = 0
% 0.43/1.09 useeqrefl = 0
% 0.43/1.09 useeqfact = 0
% 0.43/1.09 usefactor = 1
% 0.43/1.09 usesimpsplitting = 0
% 0.43/1.09 usesimpdemod = 0
% 0.43/1.09 usesimpres = 4
% 0.43/1.09
% 0.43/1.09 resimpinuse = 1000
% 0.43/1.09 resimpclauses = 20000
% 0.43/1.09 substype = standard
% 0.43/1.09 backwardsubs = 1
% 0.43/1.09 selectoldest = 5
% 0.43/1.09
% 0.43/1.09 litorderings [0] = split
% 0.43/1.09 litorderings [1] = liftord
% 0.43/1.09
% 0.43/1.09 termordering = none
% 0.43/1.09
% 0.43/1.09 litapriori = 1
% 0.43/1.09 termapriori = 0
% 0.43/1.09 litaposteriori = 0
% 0.43/1.09 termaposteriori = 0
% 0.43/1.09 demodaposteriori = 0
% 0.43/1.09 ordereqreflfact = 0
% 0.43/1.09
% 0.43/1.09 litselect = negative
% 0.43/1.09
% 0.43/1.09 maxweight = 30000
% 0.43/1.09 maxdepth = 30000
% 0.43/1.09 maxlength = 115
% 0.43/1.09 maxnrvars = 195
% 0.43/1.09 excuselevel = 0
% 0.43/1.09 increasemaxweight = 0
% 0.43/1.09
% 0.43/1.09 maxselected = 10000000
% 0.43/1.09 maxnrclauses = 10000000
% 0.43/1.09
% 0.43/1.09 showgenerated = 0
% 0.43/1.09 showkept = 0
% 0.43/1.09 showselected = 0
% 0.43/1.09 showdeleted = 0
% 0.43/1.09 showresimp = 1
% 0.43/1.09 showstatus = 2000
% 0.43/1.09
% 0.43/1.09 prologoutput = 0
% 0.43/1.09 nrgoals = 5000000
% 0.43/1.09 totalproof = 1
% 0.43/1.09
% 0.43/1.09 Symbols occurring in the translation:
% 0.43/1.09
% 0.43/1.09 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.43/1.09 . [1, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.43/1.09 ! [4, 1] (w:1, o:48, a:1, s:1, b:0),
% 0.43/1.09 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.43/1.09 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.43/1.09 c_cycorpproductsmt [35, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.43/1.09 c_basekb [36, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.43/1.09 genlmt [37, 2] (w:1, o:95, a:1, s:1, b:0),
% 0.43/1.09 c_cycnounlearnermt [38, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.43/1.09 s_http_webnjiteducjohnsontreebiochhtm [39, 0] (w:1, o:9, a:1, s:1, b:
% 0.43/1.09 0),
% 0.43/1.09 f_urlfn [40, 1] (w:1, o:53, a:1, s:1, b:0),
% 0.43/1.09 f_urlreferentfn [41, 1] (w:1, o:54, a:1, s:1, b:0),
% 0.43/1.09 c_translation_21 [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.43/1.09 f_contentmtofcdafromeventfn [43, 2] (w:1, o:94, a:1, s:1, b:0),
% 0.43/1.09 c_machinelearningspindleheadmt [44, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.43/1.09 isa [49, 2] (w:1, o:96, a:1, s:1, b:0),
% 0.43/1.09 relationexistsall [50, 3] (w:1, o:104, a:1, s:1, b:0),
% 0.43/1.09 f_relationexistsallfn [51, 4] (w:1, o:106, a:1, s:1, b:0),
% 0.43/1.09 c_relationexistsallfn [52, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.43/1.09 n_3 [53, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.43/1.09 resultisaarg [54, 2] (w:1, o:97, a:1, s:1, b:0),
% 0.43/1.09 c_genlmt [55, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.43/1.09 transitivebinarypredicate [56, 1] (w:1, o:57, a:1, s:1, b:0),
% 0.43/1.09 c_universalvocabularymt [57, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.43/1.09 shavingrazor_manual [58, 1] (w:1, o:56, a:1, s:1, b:0),
% 0.43/1.09 c_tptp_8_271 [59, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.43/1.09 c_tptpcol_16_25972 [60, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.43/1.09 c_shavingrazor_manual [61, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.43/1.09 tptp_8_271 [62, 2] (w:1, o:98, a:1, s:1, b:0),
% 0.43/1.09 c_theprototypicalshavingrazor_manual [63, 0] (w:1, o:30, a:1, s:1, b:
% 0.43/1.09 0),
% 0.43/1.09 disjointwith [67, 2] (w:1, o:99, a:1, s:1, b:0),
% 0.43/1.09 genlinverse [70, 2] (w:1, o:100, a:1, s:1, b:0),
% 0.43/1.09 genlpreds [71, 2] (w:1, o:101, a:1, s:1, b:0),
% 0.43/1.09 predicate [74, 1] (w:1, o:58, a:1, s:1, b:0),
% 0.43/1.09 binarypredicate [79, 1] (w:1, o:59, a:1, s:1, b:0),
% 0.43/1.09 collection [82, 1] (w:1, o:60, a:1, s:1, b:0),
% 0.43/1.09 genls [83, 2] (w:1, o:102, a:1, s:1, b:0),
% 0.43/1.09 tptpcol_16_25972 [84, 1] (w:1, o:61, a:1, s:1, b:0),
% 0.43/1.09 razor [85, 1] (w:1, o:55, a:1, s:1, b:0),
% 0.43/1.09 tptpcol_5_24579 [86, 1] (w:1, o:62, a:1, s:1, b:0),
% 0.43/1.09 c_transitivebinarypredicate [88, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.43/1.09 thing [89, 1] (w:1, o:63, a:1, s:1, b:0),
% 0.43/1.09 natfunction [91, 2] (w:1, o:103, a:1, s:1, b:0),
% 0.43/1.09 n_1 [92, 0] (w:1, o:42, a:1, s:1, b:0),
% 0.43/1.09 natargument [93, 3] (w:1, o:105, a:1, s:1, b:0),
% 0.43/1.09 n_2 [94, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.43/1.09 n_4 [95, 0] (w:1, o:43, a:1, s:1, b:0),
% 0.43/1.09 positiveinteger [96, 1] (w:1, o:64, a:1, s:1, b:0),
% 0.43/1.09 function_denotational [97, 1] (w:1, o:65, a:1, s:1, b:0),
% 0.43/1.09 c_urlfn [98, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.43/1.09 uniformresourcelocator [99, 1] (w:1, o:66, a:1, s:1, b:0),
% 0.43/1.09 c_urlreferentfn [100, 0] (w:1, o:45, a:1, s:1, b:0),
% 0.43/1.09 computerdataartifact [101, 1] (w:1, o:67, a:1, s:1, b:0),
% 0.43/1.09 c_contentmtofcdafromeventfn [102, 0] (w:1, o:46, a:1, s:1, b:0),
% 0.43/1.09 microtheory [103, 1] (w:1, o:68, a:1, s:1, b:0),
% 0.43/1.09 mtvisible [104, 1] (w:1, o:69, a:1, s:1, b:0).
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Starting Search:
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Bliksems!, er is een bewijs:
% 0.43/1.09 % SZS status Theorem
% 0.43/1.09 % SZS output start Refutation
% 0.43/1.09
% 0.43/1.09 (3) {G0,W16,D3,L3,V4,M1} I { ! relationexistsall( Z, T, Y ), isa(
% 0.43/1.09 f_relationexistsallfn( X, Z, T, Y ), T ), ! isa( X, Y ) }.
% 0.43/1.09 (8) {G0,W10,D3,L2,V1,M1} I { tptp_8_271( f_relationexistsallfn( X,
% 0.43/1.09 c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual ), X ), !
% 0.43/1.09 shavingrazor_manual( X ) }.
% 0.43/1.09 (9) {G0,W4,D2,L1,V0,M1} I { relationexistsall( c_tptp_8_271,
% 0.43/1.09 c_tptpcol_16_25972, c_shavingrazor_manual ) }.
% 0.43/1.09 (10) {G0,W2,D2,L1,V0,M1} I { shavingrazor_manual(
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 (27) {G0,W6,D2,L2,V1,M1} I { isa( X, c_shavingrazor_manual ), !
% 0.43/1.09 shavingrazor_manual( X ) }.
% 0.43/1.09 (28) {G0,W6,D2,L2,V1,M1} I { tptpcol_16_25972( X ), ! isa( X,
% 0.43/1.09 c_tptpcol_16_25972 ) }.
% 0.43/1.09 (66) {G0,W7,D2,L2,V1,M1} I { ! tptpcol_16_25972( X ), ! tptp_8_271( X,
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 (69) {G1,W7,D3,L1,V0,M1} R(8,10) { tptp_8_271( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 (88) {G1,W3,D2,L1,V0,M1} R(27,10) { isa(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_shavingrazor_manual ) }.
% 0.43/1.09 (92) {G2,W12,D3,L2,V2,M1} R(88,3) { isa( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, X, Y, c_shavingrazor_manual ), Y )
% 0.43/1.09 , ! relationexistsall( X, Y, c_shavingrazor_manual ) }.
% 0.43/1.09 (97) {G2,W7,D3,L1,V0,M1} R(69,66) { ! tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 (117) {G3,W7,D3,L1,V0,M1} R(92,9) { isa( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), c_tptpcol_16_25972 ) }.
% 0.43/1.09 (131) {G4,W0,D0,L0,V0,M0} R(117,28);r(97) { }.
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 % SZS output end Refutation
% 0.43/1.09 found a proof!
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Unprocessed initial clauses:
% 0.43/1.09
% 0.43/1.09 (133) {G0,W3,D2,L1,V0,M1} { genlmt( c_cycorpproductsmt, c_basekb ) }.
% 0.43/1.09 (134) {G0,W3,D2,L1,V0,M1} { genlmt( c_cycnounlearnermt, c_cycorpproductsmt
% 0.43/1.09 ) }.
% 0.43/1.09 (135) {G0,W7,D5,L1,V0,M1} { genlmt( f_contentmtofcdafromeventfn(
% 0.43/1.09 f_urlreferentfn( f_urlfn( s_http_webnjiteducjohnsontreebiochhtm ) ),
% 0.43/1.09 c_translation_21 ), c_machinelearningspindleheadmt ) }.
% 0.43/1.09 (136) {G0,W16,D3,L3,V4,M3} { ! isa( X, Y ), ! relationexistsall( Z, T, Y )
% 0.43/1.09 , isa( f_relationexistsallfn( X, Z, T, Y ), T ) }.
% 0.43/1.09 (137) {G0,W3,D2,L1,V0,M1} { resultisaarg( c_relationexistsallfn, n_3 ) }.
% 0.43/1.09 (138) {G0,W2,D2,L1,V0,M1} { transitivebinarypredicate( c_genlmt ) }.
% 0.43/1.09 (139) {G0,W3,D2,L1,V0,M1} { genlmt( c_machinelearningspindleheadmt,
% 0.43/1.09 c_cycnounlearnermt ) }.
% 0.43/1.09 (140) {G0,W3,D2,L1,V0,M1} { genlmt( c_basekb, c_universalvocabularymt )
% 0.43/1.09 }.
% 0.43/1.09 (141) {G0,W10,D3,L2,V1,M2} { ! shavingrazor_manual( X ), tptp_8_271(
% 0.43/1.09 f_relationexistsallfn( X, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), X ) }.
% 0.43/1.09 (142) {G0,W4,D2,L1,V0,M1} { relationexistsall( c_tptp_8_271,
% 0.43/1.09 c_tptpcol_16_25972, c_shavingrazor_manual ) }.
% 0.43/1.09 (143) {G0,W2,D2,L1,V0,M1} { shavingrazor_manual(
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 (144) {G0,W12,D2,L3,V3,M3} { ! isa( X, Y ), ! isa( X, Z ), ! disjointwith
% 0.43/1.09 ( Y, Z ) }.
% 0.43/1.09 (145) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlinverse( Z, Y )
% 0.43/1.09 , genlpreds( X, Y ) }.
% 0.43/1.09 (146) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.43/1.09 (147) {G0,W6,D2,L2,V2,M2} { ! genlpreds( Y, X ), predicate( X ) }.
% 0.43/1.09 (148) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.43/1.09 (149) {G0,W6,D2,L2,V2,M2} { ! genlpreds( X, Y ), predicate( X ) }.
% 0.43/1.09 (150) {G0,W11,D2,L3,V3,M3} { ! genlpreds( X, Z ), ! genlpreds( Z, Y ),
% 0.43/1.09 genlpreds( X, Y ) }.
% 0.43/1.09 (151) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.43/1.09 (152) {G0,W6,D2,L2,V1,M2} { ! predicate( X ), genlpreds( X, X ) }.
% 0.43/1.09 (153) {G0,W6,D2,L2,V2,M2} { ! genlinverse( Y, X ), binarypredicate( X )
% 0.43/1.09 }.
% 0.43/1.09 (154) {G0,W6,D2,L2,V2,M2} { ! genlinverse( X, Y ), binarypredicate( X )
% 0.43/1.09 }.
% 0.43/1.09 (155) {G0,W11,D2,L3,V3,M3} { ! genlinverse( Z, X ), ! genlpreds( Y, Z ),
% 0.43/1.09 genlinverse( Y, X ) }.
% 0.43/1.09 (156) {G0,W11,D2,L3,V3,M3} { ! genlinverse( X, Z ), ! genlpreds( Z, Y ),
% 0.43/1.09 genlinverse( X, Y ) }.
% 0.43/1.09 (157) {G0,W6,D2,L2,V2,M2} { ! disjointwith( Y, X ), collection( X ) }.
% 0.43/1.09 (158) {G0,W6,D2,L2,V2,M2} { ! disjointwith( X, Y ), collection( X ) }.
% 0.43/1.09 (159) {G0,W7,D2,L2,V2,M2} { ! disjointwith( X, Y ), disjointwith( Y, X )
% 0.43/1.09 }.
% 0.43/1.09 (160) {G0,W11,D2,L3,V3,M3} { ! disjointwith( X, Z ), ! genls( Y, Z ),
% 0.43/1.09 disjointwith( X, Y ) }.
% 0.43/1.09 (161) {G0,W11,D2,L3,V3,M3} { ! disjointwith( Z, X ), ! genls( Y, Z ),
% 0.43/1.09 disjointwith( Y, X ) }.
% 0.43/1.09 (162) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_shavingrazor_manual ),
% 0.43/1.09 shavingrazor_manual( X ) }.
% 0.43/1.09 (163) {G0,W6,D2,L2,V1,M2} { ! shavingrazor_manual( X ), isa( X,
% 0.43/1.09 c_shavingrazor_manual ) }.
% 0.43/1.09 (164) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_16_25972 ),
% 0.43/1.09 tptpcol_16_25972( X ) }.
% 0.43/1.09 (165) {G0,W6,D2,L2,V1,M2} { ! tptpcol_16_25972( X ), isa( X,
% 0.43/1.09 c_tptpcol_16_25972 ) }.
% 0.43/1.09 (166) {G0,W6,D2,L2,V2,M2} { ! tptp_8_271( Y, X ), razor( X ) }.
% 0.43/1.09 (167) {G0,W6,D2,L2,V2,M2} { ! tptp_8_271( X, Y ), tptpcol_5_24579( X ) }.
% 0.43/1.09 (168) {G0,W7,D2,L2,V3,M2} { ! relationexistsall( Y, Z, X ), collection( X
% 0.43/1.09 ) }.
% 0.43/1.09 (169) {G0,W7,D2,L2,V3,M2} { ! relationexistsall( Y, X, Z ), collection( X
% 0.43/1.09 ) }.
% 0.43/1.09 (170) {G0,W7,D2,L2,V3,M2} { ! relationexistsall( X, Y, Z ),
% 0.43/1.09 binarypredicate( X ) }.
% 0.43/1.09 (171) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_transitivebinarypredicate ),
% 0.43/1.09 transitivebinarypredicate( X ) }.
% 0.43/1.09 (172) {G0,W6,D2,L2,V1,M2} { ! transitivebinarypredicate( X ), isa( X,
% 0.43/1.09 c_transitivebinarypredicate ) }.
% 0.43/1.09 (173) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.43/1.09 (174) {G0,W6,D2,L2,V2,M2} { ! isa( Y, X ), collection( X ) }.
% 0.43/1.09 (175) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.43/1.09 (176) {G0,W6,D2,L2,V2,M2} { ! isa( X, Y ), thing( X ) }.
% 0.43/1.09 (177) {G0,W11,D2,L3,V3,M3} { ! isa( X, Z ), ! genls( Z, Y ), isa( X, Y )
% 0.43/1.09 }.
% 0.43/1.09 (178) {G0,W7,D3,L1,V4,M1} { natfunction( f_relationexistsallfn( X, Y, Z, T
% 0.43/1.09 ), c_relationexistsallfn ) }.
% 0.43/1.09 (179) {G0,W8,D3,L1,V4,M1} { natargument( f_relationexistsallfn( X, Y, Z, T
% 0.43/1.09 ), n_1, X ) }.
% 0.43/1.09 (180) {G0,W8,D3,L1,V4,M1} { natargument( f_relationexistsallfn( X, Y, Z, T
% 0.43/1.09 ), n_2, Y ) }.
% 0.43/1.09 (181) {G0,W8,D3,L1,V4,M1} { natargument( f_relationexistsallfn( X, Y, Z, T
% 0.43/1.09 ), n_3, Z ) }.
% 0.43/1.09 (182) {G0,W8,D3,L1,V4,M1} { natargument( f_relationexistsallfn( X, Y, Z, T
% 0.43/1.09 ), n_4, T ) }.
% 0.43/1.09 (183) {G0,W6,D3,L1,V4,M1} { thing( f_relationexistsallfn( X, Y, Z, T ) )
% 0.43/1.09 }.
% 0.43/1.09 (184) {G0,W6,D2,L2,V2,M2} { ! resultisaarg( Y, X ), positiveinteger( X )
% 0.43/1.09 }.
% 0.43/1.09 (185) {G0,W6,D2,L2,V2,M2} { ! resultisaarg( X, Y ), function_denotational
% 0.43/1.09 ( X ) }.
% 0.43/1.09 (186) {G0,W4,D3,L1,V1,M1} { natfunction( f_urlfn( X ), c_urlfn ) }.
% 0.43/1.09 (187) {G0,W5,D3,L1,V1,M1} { natargument( f_urlfn( X ), n_1, X ) }.
% 0.43/1.09 (188) {G0,W3,D3,L1,V1,M1} { uniformresourcelocator( f_urlfn( X ) ) }.
% 0.43/1.09 (189) {G0,W4,D3,L1,V1,M1} { natfunction( f_urlreferentfn( X ),
% 0.43/1.09 c_urlreferentfn ) }.
% 0.43/1.09 (190) {G0,W5,D3,L1,V1,M1} { natargument( f_urlreferentfn( X ), n_1, X )
% 0.43/1.09 }.
% 0.43/1.09 (191) {G0,W3,D3,L1,V1,M1} { computerdataartifact( f_urlreferentfn( X ) )
% 0.43/1.09 }.
% 0.43/1.09 (192) {G0,W5,D3,L1,V2,M1} { natfunction( f_contentmtofcdafromeventfn( X, Y
% 0.43/1.09 ), c_contentmtofcdafromeventfn ) }.
% 0.43/1.09 (193) {G0,W6,D3,L1,V2,M1} { natargument( f_contentmtofcdafromeventfn( X, Y
% 0.43/1.09 ), n_1, X ) }.
% 0.43/1.09 (194) {G0,W6,D3,L1,V2,M1} { natargument( f_contentmtofcdafromeventfn( X, Y
% 0.43/1.09 ), n_2, Y ) }.
% 0.43/1.09 (195) {G0,W4,D3,L1,V2,M1} { microtheory( f_contentmtofcdafromeventfn( X, Y
% 0.43/1.09 ) ) }.
% 0.43/1.09 (196) {G0,W2,D2,L1,V0,M1} { mtvisible( c_universalvocabularymt ) }.
% 0.43/1.09 (197) {G0,W9,D2,L3,V2,M3} { ! mtvisible( Y ), ! genlmt( Y, X ), mtvisible
% 0.43/1.09 ( X ) }.
% 0.43/1.09 (198) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.43/1.09 (199) {G0,W6,D2,L2,V2,M2} { ! genlmt( Y, X ), microtheory( X ) }.
% 0.43/1.09 (200) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.43/1.09 (201) {G0,W6,D2,L2,V2,M2} { ! genlmt( X, Y ), microtheory( X ) }.
% 0.43/1.09 (202) {G0,W11,D2,L3,V3,M3} { ! genlmt( X, Z ), ! genlmt( Z, Y ), genlmt( X
% 0.43/1.09 , Y ) }.
% 0.43/1.09 (203) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.43/1.09 (204) {G0,W6,D2,L2,V1,M2} { ! microtheory( X ), genlmt( X, X ) }.
% 0.43/1.09 (205) {G0,W2,D2,L1,V0,M1} { mtvisible( c_basekb ) }.
% 0.43/1.09 (206) {G0,W6,D5,L1,V0,M1} { mtvisible( f_contentmtofcdafromeventfn(
% 0.43/1.09 f_urlreferentfn( f_urlfn( s_http_webnjiteducjohnsontreebiochhtm ) ),
% 0.43/1.09 c_translation_21 ) ) }.
% 0.43/1.09 (207) {G0,W7,D2,L2,V1,M2} { ! tptp_8_271( X,
% 0.43/1.09 c_theprototypicalshavingrazor_manual ), ! tptpcol_16_25972( X ) }.
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Total Proof:
% 0.43/1.09
% 0.43/1.09 subsumption: (3) {G0,W16,D3,L3,V4,M1} I { ! relationexistsall( Z, T, Y ),
% 0.43/1.09 isa( f_relationexistsallfn( X, Z, T, Y ), T ), ! isa( X, Y ) }.
% 0.43/1.09 parent0: (136) {G0,W16,D3,L3,V4,M3} { ! isa( X, Y ), ! relationexistsall(
% 0.43/1.09 Z, T, Y ), isa( f_relationexistsallfn( X, Z, T, Y ), T ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := X
% 0.43/1.09 Y := Y
% 0.43/1.09 Z := Z
% 0.43/1.09 T := T
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 2
% 0.43/1.09 1 ==> 0
% 0.43/1.09 2 ==> 1
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (8) {G0,W10,D3,L2,V1,M1} I { tptp_8_271( f_relationexistsallfn
% 0.43/1.09 ( X, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual ), X ), !
% 0.43/1.09 shavingrazor_manual( X ) }.
% 0.43/1.09 parent0: (141) {G0,W10,D3,L2,V1,M2} { ! shavingrazor_manual( X ),
% 0.43/1.09 tptp_8_271( f_relationexistsallfn( X, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), X ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := X
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 1
% 0.43/1.09 1 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (9) {G0,W4,D2,L1,V0,M1} I { relationexistsall( c_tptp_8_271,
% 0.43/1.09 c_tptpcol_16_25972, c_shavingrazor_manual ) }.
% 0.43/1.09 parent0: (142) {G0,W4,D2,L1,V0,M1} { relationexistsall( c_tptp_8_271,
% 0.43/1.09 c_tptpcol_16_25972, c_shavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (10) {G0,W2,D2,L1,V0,M1} I { shavingrazor_manual(
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 parent0: (143) {G0,W2,D2,L1,V0,M1} { shavingrazor_manual(
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (27) {G0,W6,D2,L2,V1,M1} I { isa( X, c_shavingrazor_manual ),
% 0.43/1.09 ! shavingrazor_manual( X ) }.
% 0.43/1.09 parent0: (163) {G0,W6,D2,L2,V1,M2} { ! shavingrazor_manual( X ), isa( X,
% 0.43/1.09 c_shavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := X
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 1
% 0.43/1.09 1 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (28) {G0,W6,D2,L2,V1,M1} I { tptpcol_16_25972( X ), ! isa( X,
% 0.43/1.09 c_tptpcol_16_25972 ) }.
% 0.43/1.09 parent0: (164) {G0,W6,D2,L2,V1,M2} { ! isa( X, c_tptpcol_16_25972 ),
% 0.43/1.09 tptpcol_16_25972( X ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := X
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 1
% 0.43/1.09 1 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (66) {G0,W7,D2,L2,V1,M1} I { ! tptpcol_16_25972( X ), !
% 0.43/1.09 tptp_8_271( X, c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 parent0: (207) {G0,W7,D2,L2,V1,M2} { ! tptp_8_271( X,
% 0.43/1.09 c_theprototypicalshavingrazor_manual ), ! tptpcol_16_25972( X ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := X
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 1
% 0.43/1.09 1 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (218) {G1,W7,D3,L1,V0,M1} { tptp_8_271( f_relationexistsallfn
% 0.43/1.09 ( c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972
% 0.43/1.09 , c_shavingrazor_manual ), c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 parent0[1]: (8) {G0,W10,D3,L2,V1,M1} I { tptp_8_271( f_relationexistsallfn
% 0.43/1.09 ( X, c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual ), X ), !
% 0.43/1.09 shavingrazor_manual( X ) }.
% 0.43/1.09 parent1[0]: (10) {G0,W2,D2,L1,V0,M1} I { shavingrazor_manual(
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := c_theprototypicalshavingrazor_manual
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (69) {G1,W7,D3,L1,V0,M1} R(8,10) { tptp_8_271(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ),
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 parent0: (218) {G1,W7,D3,L1,V0,M1} { tptp_8_271( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (219) {G1,W3,D2,L1,V0,M1} { isa(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_shavingrazor_manual ) }.
% 0.43/1.09 parent0[1]: (27) {G0,W6,D2,L2,V1,M1} I { isa( X, c_shavingrazor_manual ), !
% 0.43/1.09 shavingrazor_manual( X ) }.
% 0.43/1.09 parent1[0]: (10) {G0,W2,D2,L1,V0,M1} I { shavingrazor_manual(
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := c_theprototypicalshavingrazor_manual
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (88) {G1,W3,D2,L1,V0,M1} R(27,10) { isa(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_shavingrazor_manual ) }.
% 0.43/1.09 parent0: (219) {G1,W3,D2,L1,V0,M1} { isa(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_shavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (220) {G1,W12,D3,L2,V2,M2} { ! relationexistsall( X, Y,
% 0.43/1.09 c_shavingrazor_manual ), isa( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, X, Y, c_shavingrazor_manual ), Y )
% 0.43/1.09 }.
% 0.43/1.09 parent0[2]: (3) {G0,W16,D3,L3,V4,M1} I { ! relationexistsall( Z, T, Y ),
% 0.43/1.09 isa( f_relationexistsallfn( X, Z, T, Y ), T ), ! isa( X, Y ) }.
% 0.43/1.09 parent1[0]: (88) {G1,W3,D2,L1,V0,M1} R(27,10) { isa(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_shavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := c_theprototypicalshavingrazor_manual
% 0.43/1.09 Y := c_shavingrazor_manual
% 0.43/1.09 Z := X
% 0.43/1.09 T := Y
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (92) {G2,W12,D3,L2,V2,M1} R(88,3) { isa( f_relationexistsallfn
% 0.43/1.09 ( c_theprototypicalshavingrazor_manual, X, Y, c_shavingrazor_manual ), Y
% 0.43/1.09 ), ! relationexistsall( X, Y, c_shavingrazor_manual ) }.
% 0.43/1.09 parent0: (220) {G1,W12,D3,L2,V2,M2} { ! relationexistsall( X, Y,
% 0.43/1.09 c_shavingrazor_manual ), isa( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, X, Y, c_shavingrazor_manual ), Y )
% 0.43/1.09 }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := X
% 0.43/1.09 Y := Y
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 1
% 0.43/1.09 1 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (221) {G1,W7,D3,L1,V0,M1} { ! tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 parent0[1]: (66) {G0,W7,D2,L2,V1,M1} I { ! tptpcol_16_25972( X ), !
% 0.43/1.09 tptp_8_271( X, c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 parent1[0]: (69) {G1,W7,D3,L1,V0,M1} R(8,10) { tptp_8_271(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ),
% 0.43/1.09 c_theprototypicalshavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := f_relationexistsallfn( c_theprototypicalshavingrazor_manual,
% 0.43/1.09 c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual )
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (97) {G2,W7,D3,L1,V0,M1} R(69,66) { ! tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 parent0: (221) {G1,W7,D3,L1,V0,M1} { ! tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (222) {G1,W7,D3,L1,V0,M1} { isa( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), c_tptpcol_16_25972 ) }.
% 0.43/1.09 parent0[1]: (92) {G2,W12,D3,L2,V2,M1} R(88,3) { isa( f_relationexistsallfn
% 0.43/1.09 ( c_theprototypicalshavingrazor_manual, X, Y, c_shavingrazor_manual ), Y
% 0.43/1.09 ), ! relationexistsall( X, Y, c_shavingrazor_manual ) }.
% 0.43/1.09 parent1[0]: (9) {G0,W4,D2,L1,V0,M1} I { relationexistsall( c_tptp_8_271,
% 0.43/1.09 c_tptpcol_16_25972, c_shavingrazor_manual ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := c_tptp_8_271
% 0.43/1.09 Y := c_tptpcol_16_25972
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (117) {G3,W7,D3,L1,V0,M1} R(92,9) { isa( f_relationexistsallfn
% 0.43/1.09 ( c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972
% 0.43/1.09 , c_shavingrazor_manual ), c_tptpcol_16_25972 ) }.
% 0.43/1.09 parent0: (222) {G1,W7,D3,L1,V0,M1} { isa( f_relationexistsallfn(
% 0.43/1.09 c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972,
% 0.43/1.09 c_shavingrazor_manual ), c_tptpcol_16_25972 ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 0 ==> 0
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (223) {G1,W6,D3,L1,V0,M1} { tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 parent0[1]: (28) {G0,W6,D2,L2,V1,M1} I { tptpcol_16_25972( X ), ! isa( X,
% 0.43/1.09 c_tptpcol_16_25972 ) }.
% 0.43/1.09 parent1[0]: (117) {G3,W7,D3,L1,V0,M1} R(92,9) { isa( f_relationexistsallfn
% 0.43/1.09 ( c_theprototypicalshavingrazor_manual, c_tptp_8_271, c_tptpcol_16_25972
% 0.43/1.09 , c_shavingrazor_manual ), c_tptpcol_16_25972 ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 X := f_relationexistsallfn( c_theprototypicalshavingrazor_manual,
% 0.43/1.09 c_tptp_8_271, c_tptpcol_16_25972, c_shavingrazor_manual )
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 resolution: (224) {G2,W0,D0,L0,V0,M0} { }.
% 0.43/1.09 parent0[0]: (97) {G2,W7,D3,L1,V0,M1} R(69,66) { ! tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 parent1[0]: (223) {G1,W6,D3,L1,V0,M1} { tptpcol_16_25972(
% 0.43/1.09 f_relationexistsallfn( c_theprototypicalshavingrazor_manual, c_tptp_8_271
% 0.43/1.09 , c_tptpcol_16_25972, c_shavingrazor_manual ) ) }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 substitution1:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 subsumption: (131) {G4,W0,D0,L0,V0,M0} R(117,28);r(97) { }.
% 0.43/1.09 parent0: (224) {G2,W0,D0,L0,V0,M0} { }.
% 0.43/1.09 substitution0:
% 0.43/1.09 end
% 0.43/1.09 permutation0:
% 0.43/1.09 end
% 0.43/1.09
% 0.43/1.09 Proof check complete!
% 0.43/1.09
% 0.43/1.09 Memory use:
% 0.43/1.09
% 0.43/1.09 space for terms: 2194
% 0.43/1.09 space for clauses: 6852
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 clauses generated: 216
% 0.43/1.09 clauses kept: 132
% 0.43/1.09 clauses selected: 124
% 0.43/1.09 clauses deleted: 1
% 0.43/1.09 clauses inuse deleted: 0
% 0.43/1.09
% 0.43/1.09 subsentry: 128
% 0.43/1.09 literals s-matched: 97
% 0.43/1.09 literals matched: 97
% 0.43/1.09 full subsumption: 0
% 0.43/1.09
% 0.43/1.09 checksum: -451861858
% 0.43/1.09
% 0.43/1.09
% 0.43/1.09 Bliksem ended
%------------------------------------------------------------------------------