%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PHI022+1 : TPTP v8.1.0. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n024.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 : Mon Jul 18 16:43:07 EDT 2022
% Result : Theorem 0.49s 1.14s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : PHI022+1 : TPTP v8.1.0. Released v7.4.0.
% 0.08/0.14 % Command : bliksem %s
% 0.14/0.36 % Computer : n024.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % DateTime : Thu Jun 2 01:47:36 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.49/1.13 *** allocated 10000 integers for termspace/termends
% 0.49/1.13 *** allocated 10000 integers for clauses
% 0.49/1.13 *** allocated 10000 integers for justifications
% 0.49/1.13 Bliksem 1.12
% 0.49/1.13
% 0.49/1.13
% 0.49/1.13 Automatic Strategy Selection
% 0.49/1.13
% 0.49/1.13
% 0.49/1.13 Clauses:
% 0.49/1.13
% 0.49/1.13 { ! selfCaused( X ), essenceInvExistence( X ) }.
% 0.49/1.13 { ! selfCaused( X ), natureConcOnlyByExistence( X ) }.
% 0.49/1.13 { ! essenceInvExistence( X ), ! natureConcOnlyByExistence( X ), selfCaused
% 0.49/1.13 ( X ) }.
% 0.49/1.13 { ! finiteAfterItsKind( X ), canBeLimitedBy( X, Y ) }.
% 0.49/1.13 { ! finiteAfterItsKind( X ), sameKind( X, Y ) }.
% 0.49/1.13 { ! canBeLimitedBy( X, Y ), ! sameKind( X, Y ), finiteAfterItsKind( X ) }.
% 0.49/1.13 { ! substance( X ), inItself( X ) }.
% 0.49/1.13 { ! substance( X ), conceivedThruItself( X ) }.
% 0.49/1.13 { ! inItself( X ), ! conceivedThruItself( X ), substance( X ) }.
% 0.49/1.13 { ! attribute( X ), intPercAsConstEssSub( X ) }.
% 0.49/1.13 { ! intPercAsConstEssSub( X ), attribute( X ) }.
% 0.49/1.13 { ! mode( X ), alpha1( X, Y ), alpha6( X, Z ) }.
% 0.49/1.13 { ! alpha1( X, Y ), mode( X ) }.
% 0.49/1.13 { ! alpha6( X, Z ), mode( X ) }.
% 0.49/1.13 { ! alpha6( X, Y ), existsIn( X, Y ) }.
% 0.49/1.13 { ! alpha6( X, Y ), conceivedThru( X, Y ) }.
% 0.49/1.13 { ! existsIn( X, Y ), ! conceivedThru( X, Y ), alpha6( X, Y ) }.
% 0.49/1.13 { ! alpha1( X, Y ), modification( X, Y ) }.
% 0.49/1.13 { ! alpha1( X, Y ), substance( Y ) }.
% 0.49/1.13 { ! modification( X, Y ), ! substance( Y ), alpha1( X, Y ) }.
% 0.49/1.13 { ! god( X ), being( X ) }.
% 0.49/1.13 { ! god( X ), absolutelyInfinite( X ) }.
% 0.49/1.13 { ! being( X ), ! absolutelyInfinite( X ), god( X ) }.
% 0.49/1.13 { ! absolutelyInfinite( X ), substance( X ) }.
% 0.49/1.13 { ! absolutelyInfinite( X ), alpha7( X, Y ) }.
% 0.49/1.13 { ! substance( X ), ! alpha7( X, Y ), absolutelyInfinite( X ) }.
% 0.49/1.13 { ! alpha7( X, Y ), constInInfAttributes( X ) }.
% 0.49/1.13 { ! alpha7( X, Y ), alpha9( X, Y ) }.
% 0.49/1.13 { ! constInInfAttributes( X ), ! alpha9( X, Y ), alpha7( X, Y ) }.
% 0.49/1.13 { ! alpha9( X, Y ), ! attributeOf( Y, X ), alpha2( Y ) }.
% 0.49/1.13 { attributeOf( Y, X ), alpha9( X, Y ) }.
% 0.49/1.13 { ! alpha2( Y ), alpha9( X, Y ) }.
% 0.49/1.13 { ! alpha2( X ), expressesEternalEssentiality( X ) }.
% 0.49/1.13 { ! alpha2( X ), expressesInfiniteEssentiality( X ) }.
% 0.49/1.13 { ! expressesEternalEssentiality( X ), ! expressesInfiniteEssentiality( X )
% 0.49/1.13 , alpha2( X ) }.
% 0.49/1.13 { ! free( X ), existsOnlyByNecessityOfOwnNature( X ) }.
% 0.49/1.13 { ! free( X ), alpha3( X, Y ) }.
% 0.49/1.13 { ! existsOnlyByNecessityOfOwnNature( X ), ! alpha3( X, Y ), free( X ) }.
% 0.49/1.13 { ! alpha3( X, Y ), ! actionOf( Y, X ), determinedByItselfAlone( Y, X ) }.
% 0.49/1.13 { actionOf( Y, X ), alpha3( X, Y ) }.
% 0.49/1.13 { ! determinedByItselfAlone( Y, X ), alpha3( X, Y ) }.
% 0.49/1.13 { ! necessary( X ), externalTo( Y, X ) }.
% 0.49/1.13 { ! necessary( X ), alpha8( X, Y ) }.
% 0.49/1.13 { ! externalTo( Y, X ), ! alpha8( X, Y ), necessary( X ) }.
% 0.49/1.13 { ! alpha8( X, Y ), determinedByFixedMethod( X, Y ) }.
% 0.49/1.13 { ! alpha8( X, Y ), alpha10( X, Y ) }.
% 0.49/1.13 { ! determinedByFixedMethod( X, Y ), ! alpha10( X, Y ), alpha8( X, Y ) }.
% 0.49/1.13 { ! alpha10( X, Y ), determinedByDefiniteMethod( X, Y ) }.
% 0.49/1.13 { ! alpha10( X, Y ), alpha4( Y ) }.
% 0.49/1.13 { ! determinedByDefiniteMethod( X, Y ), ! alpha4( Y ), alpha10( X, Y ) }.
% 0.49/1.13 { ! alpha4( X ), isMethodAction( X ), isMethodExistence( X ) }.
% 0.49/1.13 { ! isMethodAction( X ), alpha4( X ) }.
% 0.49/1.13 { ! isMethodExistence( X ), alpha4( X ) }.
% 0.49/1.13 { ! eternity( X ), existConcFollowFromDefEternal( X ) }.
% 0.49/1.13 { ! existConcFollowFromDefEternal( X ), eternity( X ) }.
% 0.49/1.13 { ! exists( X ), existsIn( X, X ), alpha5( X, Y ) }.
% 0.49/1.13 { ! existsIn( X, X ), exists( X ) }.
% 0.49/1.13 { ! alpha5( X, Y ), exists( X ) }.
% 0.49/1.13 { ! alpha5( X, Y ), existsIn( X, Y ) }.
% 0.49/1.13 { ! alpha5( X, Y ), ! X = Y }.
% 0.49/1.13 { ! existsIn( X, Y ), X = Y, alpha5( X, Y ) }.
% 0.49/1.13 { conceivedThru( X, X ), conceivedThru( X, Y ) }.
% 0.49/1.13 { conceivedThru( X, X ), ! X = Y }.
% 0.49/1.13 { ! definiteCause( X ), effectNecessarilyFollowsFrom( Y, X ) }.
% 0.49/1.13 { ! definiteCause( X ), definiteCause( X ), ! effectNecessarilyFollowsFrom
% 0.49/1.13 ( Y, X ) }.
% 0.49/1.13 { ! knowledgeOfEffect( X, Y ), knowledgeOfACause( X ) }.
% 0.49/1.13 { ! knowledgeOfACause( X ), knowledgeOfEffect( X, Y ) }.
% 0.49/1.13 { ! haveNothingInCommon( X, Y ), alpha11( X, Y ) }.
% 0.49/1.13 { ! haveNothingInCommon( X, Y ), ! conceptionInvolves( Y, X ) }.
% 0.49/1.13 { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf( X, Y ) }.
% 0.49/1.13 { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf( Y, X ) }.
% 0.49/1.13 { ! alpha11( X, Y ), ! conceptionInvolves( X, Y ) }.
% 0.49/1.13 { canBeUnderstoodInTermsOf( X, Y ), canBeUnderstoodInTermsOf( Y, X ),
% 0.49/1.13 conceptionInvolves( X, Y ), alpha11( X, Y ) }.
% 0.49/1.13 { ! trueIdea( X ), correspondWith( X, Y ) }.
% 0.49/1.14 { ! trueIdea( X ), ideateOf( Y, X ), objectOf( Y, X ) }.
% 0.49/1.14 { ! canBeConceivedAsNonExisting( X ), ! essenceInvExistence( X ) }.
% 0.49/1.14 { ! substance( X ), being( X ) }.
% 0.49/1.14 { ! inItself( X ), selfCaused( X ) }.
% 0.49/1.14 { ! being( X ), hasEssence( X ) }.
% 0.49/1.14 { ! essenceInvExistence( X ), ! hasEssence( X ), exists( X ) }.
% 0.49/1.14 { substance( skol1 ) }.
% 0.49/1.14 { ! exists( skol1 ) }.
% 0.49/1.14
% 0.49/1.14 percentage equality = 0.011050, percentage horn = 0.887500
% 0.49/1.14 This is a problem with some equality
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 Options Used:
% 0.49/1.14
% 0.49/1.14 useres = 1
% 0.49/1.14 useparamod = 1
% 0.49/1.14 useeqrefl = 1
% 0.49/1.14 useeqfact = 1
% 0.49/1.14 usefactor = 1
% 0.49/1.14 usesimpsplitting = 0
% 0.49/1.14 usesimpdemod = 5
% 0.49/1.14 usesimpres = 3
% 0.49/1.14
% 0.49/1.14 resimpinuse = 1000
% 0.49/1.14 resimpclauses = 20000
% 0.49/1.14 substype = eqrewr
% 0.49/1.14 backwardsubs = 1
% 0.49/1.14 selectoldest = 5
% 0.49/1.14
% 0.49/1.14 litorderings [0] = split
% 0.49/1.14 litorderings [1] = extend the termordering, first sorting on arguments
% 0.49/1.14
% 0.49/1.14 termordering = kbo
% 0.49/1.14
% 0.49/1.14 litapriori = 0
% 0.49/1.14 termapriori = 1
% 0.49/1.14 litaposteriori = 0
% 0.49/1.14 termaposteriori = 0
% 0.49/1.14 demodaposteriori = 0
% 0.49/1.14 ordereqreflfact = 0
% 0.49/1.14
% 0.49/1.14 litselect = negord
% 0.49/1.14
% 0.49/1.14 maxweight = 15
% 0.49/1.14 maxdepth = 30000
% 0.49/1.14 maxlength = 115
% 0.49/1.14 maxnrvars = 195
% 0.49/1.14 excuselevel = 1
% 0.49/1.14 increasemaxweight = 1
% 0.49/1.14
% 0.49/1.14 maxselected = 10000000
% 0.49/1.14 maxnrclauses = 10000000
% 0.49/1.14
% 0.49/1.14 showgenerated = 0
% 0.49/1.14 showkept = 0
% 0.49/1.14 showselected = 0
% 0.49/1.14 showdeleted = 0
% 0.49/1.14 showresimp = 1
% 0.49/1.14 showstatus = 2000
% 0.49/1.14
% 0.49/1.14 prologoutput = 0
% 0.49/1.14 nrgoals = 5000000
% 0.49/1.14 totalproof = 1
% 0.49/1.14
% 0.49/1.14 Symbols occurring in the translation:
% 0.49/1.14
% 0.49/1.14 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.49/1.14 . [1, 2] (w:1, o:46, a:1, s:1, b:0),
% 0.49/1.14 ! [4, 1] (w:0, o:10, a:1, s:1, b:0),
% 0.49/1.14 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.49/1.14 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.49/1.14 selfCaused [36, 1] (w:1, o:15, a:1, s:1, b:0),
% 0.49/1.14 essenceInvExistence [37, 1] (w:1, o:18, a:1, s:1, b:0),
% 0.49/1.14 natureConcOnlyByExistence [38, 1] (w:1, o:20, a:1, s:1, b:0),
% 0.49/1.14 finiteAfterItsKind [40, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.49/1.14 canBeLimitedBy [41, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.49/1.14 sameKind [42, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.49/1.14 substance [43, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.49/1.14 inItself [44, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.49/1.14 conceivedThruItself [45, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.49/1.14 attribute [46, 1] (w:1, o:36, a:1, s:1, b:0),
% 0.49/1.14 intPercAsConstEssSub [47, 1] (w:1, o:37, a:1, s:1, b:0),
% 0.49/1.14 mode [49, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.49/1.14 modification [50, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.49/1.14 existsIn [51, 2] (w:1, o:79, a:1, s:1, b:0),
% 0.49/1.14 conceivedThru [52, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.49/1.14 god [53, 1] (w:1, o:39, a:1, s:1, b:0),
% 0.49/1.14 being [54, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.49/1.14 absolutelyInfinite [55, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.49/1.14 constInInfAttributes [56, 1] (w:1, o:40, a:1, s:1, b:0),
% 0.49/1.14 attributeOf [57, 2] (w:1, o:81, a:1, s:1, b:0),
% 0.49/1.14 expressesEternalEssentiality [58, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.49/1.14 expressesInfiniteEssentiality [59, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.49/1.14 free [60, 1] (w:1, o:38, a:1, s:1, b:0),
% 0.49/1.14 existsOnlyByNecessityOfOwnNature [61, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.49/1.14
% 0.49/1.14 actionOf [62, 2] (w:1, o:82, a:1, s:1, b:0),
% 0.49/1.14 determinedByItselfAlone [63, 2] (w:1, o:76, a:1, s:1, b:0),
% 0.49/1.14 necessary [64, 1] (w:1, o:41, a:1, s:1, b:0),
% 0.49/1.14 externalTo [65, 2] (w:1, o:83, a:1, s:1, b:0),
% 0.49/1.14 determinedByFixedMethod [66, 2] (w:1, o:77, a:1, s:1, b:0),
% 0.49/1.14 determinedByDefiniteMethod [67, 2] (w:1, o:78, a:1, s:1, b:0),
% 0.49/1.14 isMethodAction [68, 1] (w:1, o:42, a:1, s:1, b:0),
% 0.49/1.14 isMethodExistence [69, 1] (w:1, o:43, a:1, s:1, b:0),
% 0.49/1.14 eternity [70, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.49/1.14 existConcFollowFromDefEternal [71, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.49/1.14 exists [72, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.49/1.14 definiteCause [73, 1] (w:1, o:17, a:1, s:1, b:0),
% 0.49/1.14 effectNecessarilyFollowsFrom [74, 2] (w:1, o:84, a:1, s:1, b:0),
% 0.49/1.14 knowledgeOfEffect [75, 2] (w:1, o:85, a:1, s:1, b:0),
% 0.49/1.14 knowledgeOfACause [76, 1] (w:1, o:44, a:1, s:1, b:0),
% 0.49/1.14 haveNothingInCommon [77, 2] (w:1, o:86, a:1, s:1, b:0),
% 0.49/1.14 canBeUnderstoodInTermsOf [78, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.49/1.14 conceptionInvolves [79, 2] (w:1, o:74, a:1, s:1, b:0),
% 0.49/1.14 trueIdea [80, 1] (w:1, o:45, a:1, s:1, b:0),
% 0.49/1.14 correspondWith [81, 2] (w:1, o:75, a:1, s:1, b:0),
% 0.49/1.14 ideateOf [82, 2] (w:1, o:87, a:1, s:1, b:0),
% 0.49/1.14 objectOf [83, 2] (w:1, o:88, a:1, s:1, b:0),
% 0.49/1.14 canBeConceivedAsNonExisting [84, 1] (w:1, o:16, a:1, s:1, b:0),
% 0.49/1.14 hasEssence [85, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.49/1.14 alpha1 [86, 2] (w:1, o:89, a:1, s:1, b:1),
% 0.49/1.14 alpha2 [87, 1] (w:1, o:32, a:1, s:1, b:1),
% 0.49/1.14 alpha3 [88, 2] (w:1, o:90, a:1, s:1, b:1),
% 0.49/1.14 alpha4 [89, 1] (w:1, o:33, a:1, s:1, b:1),
% 0.49/1.14 alpha5 [90, 2] (w:1, o:91, a:1, s:1, b:1),
% 0.49/1.14 alpha6 [91, 2] (w:1, o:92, a:1, s:1, b:1),
% 0.49/1.14 alpha7 [92, 2] (w:1, o:93, a:1, s:1, b:1),
% 0.49/1.14 alpha8 [93, 2] (w:1, o:94, a:1, s:1, b:1),
% 0.49/1.14 alpha9 [94, 2] (w:1, o:95, a:1, s:1, b:1),
% 0.49/1.14 alpha10 [95, 2] (w:1, o:96, a:1, s:1, b:1),
% 0.49/1.14 alpha11 [96, 2] (w:1, o:97, a:1, s:1, b:1),
% 0.49/1.14 skol1 [97, 0] (w:1, o:9, a:1, s:1, b:1).
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 Starting Search:
% 0.49/1.14
% 0.49/1.14 *** allocated 15000 integers for clauses
% 0.49/1.14 *** allocated 22500 integers for clauses
% 0.49/1.14
% 0.49/1.14 Bliksems!, er is een bewijs:
% 0.49/1.14 % SZS status Theorem
% 0.49/1.14 % SZS output start Refutation
% 0.49/1.14
% 0.49/1.14 (0) {G0,W4,D2,L2,V1,M2} I { ! selfCaused( X ), essenceInvExistence( X ) }.
% 0.49/1.14 (6) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), inItself( X ) }.
% 0.49/1.14 (74) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), being( X ) }.
% 0.49/1.14 (75) {G0,W4,D2,L2,V1,M2} I { ! inItself( X ), selfCaused( X ) }.
% 0.49/1.14 (76) {G0,W4,D2,L2,V1,M2} I { ! being( X ), hasEssence( X ) }.
% 0.49/1.14 (77) {G0,W6,D2,L3,V1,M3} I { ! essenceInvExistence( X ), ! hasEssence( X )
% 0.49/1.14 , exists( X ) }.
% 0.49/1.14 (78) {G0,W2,D2,L1,V0,M1} I { substance( skol1 ) }.
% 0.49/1.14 (79) {G0,W2,D2,L1,V0,M1} I { ! exists( skol1 ) }.
% 0.49/1.14 (83) {G1,W4,D2,L2,V1,M2} R(75,0) { ! inItself( X ), essenceInvExistence( X
% 0.49/1.14 ) }.
% 0.49/1.14 (85) {G1,W2,D2,L1,V0,M1} R(74,78) { being( skol1 ) }.
% 0.49/1.14 (86) {G2,W2,D2,L1,V0,M1} R(85,76) { hasEssence( skol1 ) }.
% 0.49/1.14 (102) {G1,W2,D2,L1,V0,M1} R(6,78) { inItself( skol1 ) }.
% 0.49/1.14 (105) {G2,W2,D2,L1,V0,M1} R(102,83) { essenceInvExistence( skol1 ) }.
% 0.49/1.14 (427) {G3,W2,D2,L1,V0,M1} R(77,105);r(86) { exists( skol1 ) }.
% 0.49/1.14 (432) {G4,W0,D0,L0,V0,M0} S(427);r(79) { }.
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 % SZS output end Refutation
% 0.49/1.14 found a proof!
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 Unprocessed initial clauses:
% 0.49/1.14
% 0.49/1.14 (434) {G0,W4,D2,L2,V1,M2} { ! selfCaused( X ), essenceInvExistence( X )
% 0.49/1.14 }.
% 0.49/1.14 (435) {G0,W4,D2,L2,V1,M2} { ! selfCaused( X ), natureConcOnlyByExistence(
% 0.49/1.14 X ) }.
% 0.49/1.14 (436) {G0,W6,D2,L3,V1,M3} { ! essenceInvExistence( X ), !
% 0.49/1.14 natureConcOnlyByExistence( X ), selfCaused( X ) }.
% 0.49/1.14 (437) {G0,W5,D2,L2,V2,M2} { ! finiteAfterItsKind( X ), canBeLimitedBy( X,
% 0.49/1.14 Y ) }.
% 0.49/1.14 (438) {G0,W5,D2,L2,V2,M2} { ! finiteAfterItsKind( X ), sameKind( X, Y )
% 0.49/1.14 }.
% 0.49/1.14 (439) {G0,W8,D2,L3,V2,M3} { ! canBeLimitedBy( X, Y ), ! sameKind( X, Y ),
% 0.49/1.14 finiteAfterItsKind( X ) }.
% 0.49/1.14 (440) {G0,W4,D2,L2,V1,M2} { ! substance( X ), inItself( X ) }.
% 0.49/1.14 (441) {G0,W4,D2,L2,V1,M2} { ! substance( X ), conceivedThruItself( X ) }.
% 0.49/1.14 (442) {G0,W6,D2,L3,V1,M3} { ! inItself( X ), ! conceivedThruItself( X ),
% 0.49/1.14 substance( X ) }.
% 0.49/1.14 (443) {G0,W4,D2,L2,V1,M2} { ! attribute( X ), intPercAsConstEssSub( X )
% 0.49/1.14 }.
% 0.49/1.14 (444) {G0,W4,D2,L2,V1,M2} { ! intPercAsConstEssSub( X ), attribute( X )
% 0.49/1.14 }.
% 0.49/1.14 (445) {G0,W8,D2,L3,V3,M3} { ! mode( X ), alpha1( X, Y ), alpha6( X, Z )
% 0.49/1.14 }.
% 0.49/1.14 (446) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), mode( X ) }.
% 0.49/1.14 (447) {G0,W5,D2,L2,V2,M2} { ! alpha6( X, Z ), mode( X ) }.
% 0.49/1.14 (448) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), existsIn( X, Y ) }.
% 0.49/1.14 (449) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), conceivedThru( X, Y ) }.
% 0.49/1.14 (450) {G0,W9,D2,L3,V2,M3} { ! existsIn( X, Y ), ! conceivedThru( X, Y ),
% 0.49/1.14 alpha6( X, Y ) }.
% 0.49/1.14 (451) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), modification( X, Y ) }.
% 0.49/1.14 (452) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), substance( Y ) }.
% 0.49/1.14 (453) {G0,W8,D2,L3,V2,M3} { ! modification( X, Y ), ! substance( Y ),
% 0.49/1.14 alpha1( X, Y ) }.
% 0.49/1.14 (454) {G0,W4,D2,L2,V1,M2} { ! god( X ), being( X ) }.
% 0.49/1.14 (455) {G0,W4,D2,L2,V1,M2} { ! god( X ), absolutelyInfinite( X ) }.
% 0.49/1.14 (456) {G0,W6,D2,L3,V1,M3} { ! being( X ), ! absolutelyInfinite( X ), god(
% 0.49/1.14 X ) }.
% 0.49/1.14 (457) {G0,W4,D2,L2,V1,M2} { ! absolutelyInfinite( X ), substance( X ) }.
% 0.49/1.14 (458) {G0,W5,D2,L2,V2,M2} { ! absolutelyInfinite( X ), alpha7( X, Y ) }.
% 0.49/1.14 (459) {G0,W7,D2,L3,V2,M3} { ! substance( X ), ! alpha7( X, Y ),
% 0.49/1.14 absolutelyInfinite( X ) }.
% 0.49/1.14 (460) {G0,W5,D2,L2,V2,M2} { ! alpha7( X, Y ), constInInfAttributes( X )
% 0.49/1.14 }.
% 0.49/1.14 (461) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), alpha9( X, Y ) }.
% 0.49/1.14 (462) {G0,W8,D2,L3,V2,M3} { ! constInInfAttributes( X ), ! alpha9( X, Y )
% 0.49/1.14 , alpha7( X, Y ) }.
% 0.49/1.14 (463) {G0,W8,D2,L3,V2,M3} { ! alpha9( X, Y ), ! attributeOf( Y, X ),
% 0.49/1.14 alpha2( Y ) }.
% 0.49/1.14 (464) {G0,W6,D2,L2,V2,M2} { attributeOf( Y, X ), alpha9( X, Y ) }.
% 0.49/1.14 (465) {G0,W5,D2,L2,V2,M2} { ! alpha2( Y ), alpha9( X, Y ) }.
% 0.49/1.14 (466) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), expressesEternalEssentiality( X
% 0.49/1.14 ) }.
% 0.49/1.14 (467) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), expressesInfiniteEssentiality(
% 0.49/1.14 X ) }.
% 0.49/1.14 (468) {G0,W6,D2,L3,V1,M3} { ! expressesEternalEssentiality( X ), !
% 0.49/1.14 expressesInfiniteEssentiality( X ), alpha2( X ) }.
% 0.49/1.14 (469) {G0,W4,D2,L2,V1,M2} { ! free( X ), existsOnlyByNecessityOfOwnNature
% 0.49/1.14 ( X ) }.
% 0.49/1.14 (470) {G0,W5,D2,L2,V2,M2} { ! free( X ), alpha3( X, Y ) }.
% 0.49/1.14 (471) {G0,W7,D2,L3,V2,M3} { ! existsOnlyByNecessityOfOwnNature( X ), !
% 0.49/1.14 alpha3( X, Y ), free( X ) }.
% 0.49/1.14 (472) {G0,W9,D2,L3,V2,M3} { ! alpha3( X, Y ), ! actionOf( Y, X ),
% 0.49/1.14 determinedByItselfAlone( Y, X ) }.
% 0.49/1.14 (473) {G0,W6,D2,L2,V2,M2} { actionOf( Y, X ), alpha3( X, Y ) }.
% 0.49/1.14 (474) {G0,W6,D2,L2,V2,M2} { ! determinedByItselfAlone( Y, X ), alpha3( X,
% 0.49/1.14 Y ) }.
% 0.49/1.14 (475) {G0,W5,D2,L2,V2,M2} { ! necessary( X ), externalTo( Y, X ) }.
% 0.49/1.14 (476) {G0,W5,D2,L2,V2,M2} { ! necessary( X ), alpha8( X, Y ) }.
% 0.49/1.14 (477) {G0,W8,D2,L3,V2,M3} { ! externalTo( Y, X ), ! alpha8( X, Y ),
% 0.49/1.14 necessary( X ) }.
% 0.49/1.14 (478) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), determinedByFixedMethod( X,
% 0.49/1.14 Y ) }.
% 0.49/1.14 (479) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), alpha10( X, Y ) }.
% 0.49/1.14 (480) {G0,W9,D2,L3,V2,M3} { ! determinedByFixedMethod( X, Y ), ! alpha10(
% 0.49/1.14 X, Y ), alpha8( X, Y ) }.
% 0.49/1.14 (481) {G0,W6,D2,L2,V2,M2} { ! alpha10( X, Y ), determinedByDefiniteMethod
% 0.49/1.14 ( X, Y ) }.
% 0.49/1.14 (482) {G0,W5,D2,L2,V2,M2} { ! alpha10( X, Y ), alpha4( Y ) }.
% 0.49/1.14 (483) {G0,W8,D2,L3,V2,M3} { ! determinedByDefiniteMethod( X, Y ), ! alpha4
% 0.49/1.14 ( Y ), alpha10( X, Y ) }.
% 0.49/1.14 (484) {G0,W6,D2,L3,V1,M3} { ! alpha4( X ), isMethodAction( X ),
% 0.49/1.14 isMethodExistence( X ) }.
% 0.49/1.14 (485) {G0,W4,D2,L2,V1,M2} { ! isMethodAction( X ), alpha4( X ) }.
% 0.49/1.14 (486) {G0,W4,D2,L2,V1,M2} { ! isMethodExistence( X ), alpha4( X ) }.
% 0.49/1.14 (487) {G0,W4,D2,L2,V1,M2} { ! eternity( X ), existConcFollowFromDefEternal
% 0.49/1.14 ( X ) }.
% 0.49/1.14 (488) {G0,W4,D2,L2,V1,M2} { ! existConcFollowFromDefEternal( X ), eternity
% 0.49/1.14 ( X ) }.
% 0.49/1.14 (489) {G0,W8,D2,L3,V2,M3} { ! exists( X ), existsIn( X, X ), alpha5( X, Y
% 0.49/1.14 ) }.
% 0.49/1.14 (490) {G0,W5,D2,L2,V1,M2} { ! existsIn( X, X ), exists( X ) }.
% 0.49/1.14 (491) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), exists( X ) }.
% 0.49/1.14 (492) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), existsIn( X, Y ) }.
% 0.49/1.14 (493) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), ! X = Y }.
% 0.49/1.14 (494) {G0,W9,D2,L3,V2,M3} { ! existsIn( X, Y ), X = Y, alpha5( X, Y ) }.
% 0.49/1.14 (495) {G0,W6,D2,L2,V2,M2} { conceivedThru( X, X ), conceivedThru( X, Y )
% 0.49/1.14 }.
% 0.49/1.14 (496) {G0,W6,D2,L2,V2,M2} { conceivedThru( X, X ), ! X = Y }.
% 0.49/1.14 (497) {G0,W5,D2,L2,V2,M2} { ! definiteCause( X ),
% 0.49/1.14 effectNecessarilyFollowsFrom( Y, X ) }.
% 0.49/1.14 (498) {G0,W7,D2,L3,V2,M3} { ! definiteCause( X ), definiteCause( X ), !
% 0.49/1.14 effectNecessarilyFollowsFrom( Y, X ) }.
% 0.49/1.14 (499) {G0,W5,D2,L2,V2,M2} { ! knowledgeOfEffect( X, Y ), knowledgeOfACause
% 0.49/1.14 ( X ) }.
% 0.49/1.14 (500) {G0,W5,D2,L2,V2,M2} { ! knowledgeOfACause( X ), knowledgeOfEffect( X
% 0.49/1.14 , Y ) }.
% 0.49/1.14 (501) {G0,W6,D2,L2,V2,M2} { ! haveNothingInCommon( X, Y ), alpha11( X, Y )
% 0.49/1.14 }.
% 0.49/1.14 (502) {G0,W6,D2,L2,V2,M2} { ! haveNothingInCommon( X, Y ), !
% 0.49/1.14 conceptionInvolves( Y, X ) }.
% 0.49/1.14 (503) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf
% 0.49/1.14 ( X, Y ) }.
% 0.49/1.14 (504) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf
% 0.49/1.14 ( Y, X ) }.
% 0.49/1.14 (505) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), ! conceptionInvolves( X, Y
% 0.49/1.14 ) }.
% 0.49/1.14 (506) {G0,W12,D2,L4,V2,M4} { canBeUnderstoodInTermsOf( X, Y ),
% 0.49/1.14 canBeUnderstoodInTermsOf( Y, X ), conceptionInvolves( X, Y ), alpha11( X
% 0.49/1.14 , Y ) }.
% 0.49/1.14 (507) {G0,W5,D2,L2,V2,M2} { ! trueIdea( X ), correspondWith( X, Y ) }.
% 0.49/1.14 (508) {G0,W8,D2,L3,V2,M3} { ! trueIdea( X ), ideateOf( Y, X ), objectOf( Y
% 0.49/1.14 , X ) }.
% 0.49/1.14 (509) {G0,W4,D2,L2,V1,M2} { ! canBeConceivedAsNonExisting( X ), !
% 0.49/1.14 essenceInvExistence( X ) }.
% 0.49/1.14 (510) {G0,W4,D2,L2,V1,M2} { ! substance( X ), being( X ) }.
% 0.49/1.14 (511) {G0,W4,D2,L2,V1,M2} { ! inItself( X ), selfCaused( X ) }.
% 0.49/1.14 (512) {G0,W4,D2,L2,V1,M2} { ! being( X ), hasEssence( X ) }.
% 0.49/1.14 (513) {G0,W6,D2,L3,V1,M3} { ! essenceInvExistence( X ), ! hasEssence( X )
% 0.49/1.14 , exists( X ) }.
% 0.49/1.14 (514) {G0,W2,D2,L1,V0,M1} { substance( skol1 ) }.
% 0.49/1.14 (515) {G0,W2,D2,L1,V0,M1} { ! exists( skol1 ) }.
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 Total Proof:
% 0.49/1.14
% 0.49/1.14 subsumption: (0) {G0,W4,D2,L2,V1,M2} I { ! selfCaused( X ),
% 0.49/1.14 essenceInvExistence( X ) }.
% 0.49/1.14 parent0: (434) {G0,W4,D2,L2,V1,M2} { ! selfCaused( X ),
% 0.49/1.14 essenceInvExistence( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 1 ==> 1
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (6) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), inItself( X )
% 0.49/1.14 }.
% 0.49/1.14 parent0: (440) {G0,W4,D2,L2,V1,M2} { ! substance( X ), inItself( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 1 ==> 1
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (74) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), being( X ) }.
% 0.49/1.14 parent0: (510) {G0,W4,D2,L2,V1,M2} { ! substance( X ), being( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 1 ==> 1
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (75) {G0,W4,D2,L2,V1,M2} I { ! inItself( X ), selfCaused( X )
% 0.49/1.14 }.
% 0.49/1.14 parent0: (511) {G0,W4,D2,L2,V1,M2} { ! inItself( X ), selfCaused( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 1 ==> 1
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (76) {G0,W4,D2,L2,V1,M2} I { ! being( X ), hasEssence( X ) }.
% 0.49/1.14 parent0: (512) {G0,W4,D2,L2,V1,M2} { ! being( X ), hasEssence( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 1 ==> 1
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (77) {G0,W6,D2,L3,V1,M3} I { ! essenceInvExistence( X ), !
% 0.49/1.14 hasEssence( X ), exists( X ) }.
% 0.49/1.14 parent0: (513) {G0,W6,D2,L3,V1,M3} { ! essenceInvExistence( X ), !
% 0.49/1.14 hasEssence( X ), exists( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 1 ==> 1
% 0.49/1.14 2 ==> 2
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (78) {G0,W2,D2,L1,V0,M1} I { substance( skol1 ) }.
% 0.49/1.14 parent0: (514) {G0,W2,D2,L1,V0,M1} { substance( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (79) {G0,W2,D2,L1,V0,M1} I { ! exists( skol1 ) }.
% 0.49/1.14 parent0: (515) {G0,W2,D2,L1,V0,M1} { ! exists( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (546) {G1,W4,D2,L2,V1,M2} { essenceInvExistence( X ), !
% 0.49/1.14 inItself( X ) }.
% 0.49/1.14 parent0[0]: (0) {G0,W4,D2,L2,V1,M2} I { ! selfCaused( X ),
% 0.49/1.14 essenceInvExistence( X ) }.
% 0.49/1.14 parent1[1]: (75) {G0,W4,D2,L2,V1,M2} I { ! inItself( X ), selfCaused( X )
% 0.49/1.14 }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (83) {G1,W4,D2,L2,V1,M2} R(75,0) { ! inItself( X ),
% 0.49/1.14 essenceInvExistence( X ) }.
% 0.49/1.14 parent0: (546) {G1,W4,D2,L2,V1,M2} { essenceInvExistence( X ), ! inItself
% 0.49/1.14 ( X ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := X
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 1
% 0.49/1.14 1 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (547) {G1,W2,D2,L1,V0,M1} { being( skol1 ) }.
% 0.49/1.14 parent0[0]: (74) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), being( X ) }.
% 0.49/1.14 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { substance( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := skol1
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (85) {G1,W2,D2,L1,V0,M1} R(74,78) { being( skol1 ) }.
% 0.49/1.14 parent0: (547) {G1,W2,D2,L1,V0,M1} { being( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (548) {G1,W2,D2,L1,V0,M1} { hasEssence( skol1 ) }.
% 0.49/1.14 parent0[0]: (76) {G0,W4,D2,L2,V1,M2} I { ! being( X ), hasEssence( X ) }.
% 0.49/1.14 parent1[0]: (85) {G1,W2,D2,L1,V0,M1} R(74,78) { being( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := skol1
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (86) {G2,W2,D2,L1,V0,M1} R(85,76) { hasEssence( skol1 ) }.
% 0.49/1.14 parent0: (548) {G1,W2,D2,L1,V0,M1} { hasEssence( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (549) {G1,W2,D2,L1,V0,M1} { inItself( skol1 ) }.
% 0.49/1.14 parent0[0]: (6) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), inItself( X ) }.
% 0.49/1.14 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { substance( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := skol1
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (102) {G1,W2,D2,L1,V0,M1} R(6,78) { inItself( skol1 ) }.
% 0.49/1.14 parent0: (549) {G1,W2,D2,L1,V0,M1} { inItself( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (550) {G2,W2,D2,L1,V0,M1} { essenceInvExistence( skol1 ) }.
% 0.49/1.14 parent0[0]: (83) {G1,W4,D2,L2,V1,M2} R(75,0) { ! inItself( X ),
% 0.49/1.14 essenceInvExistence( X ) }.
% 0.49/1.14 parent1[0]: (102) {G1,W2,D2,L1,V0,M1} R(6,78) { inItself( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := skol1
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (105) {G2,W2,D2,L1,V0,M1} R(102,83) { essenceInvExistence(
% 0.49/1.14 skol1 ) }.
% 0.49/1.14 parent0: (550) {G2,W2,D2,L1,V0,M1} { essenceInvExistence( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (551) {G1,W4,D2,L2,V0,M2} { ! hasEssence( skol1 ), exists(
% 0.49/1.14 skol1 ) }.
% 0.49/1.14 parent0[0]: (77) {G0,W6,D2,L3,V1,M3} I { ! essenceInvExistence( X ), !
% 0.49/1.14 hasEssence( X ), exists( X ) }.
% 0.49/1.14 parent1[0]: (105) {G2,W2,D2,L1,V0,M1} R(102,83) { essenceInvExistence(
% 0.49/1.14 skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 X := skol1
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (552) {G2,W2,D2,L1,V0,M1} { exists( skol1 ) }.
% 0.49/1.14 parent0[0]: (551) {G1,W4,D2,L2,V0,M2} { ! hasEssence( skol1 ), exists(
% 0.49/1.14 skol1 ) }.
% 0.49/1.14 parent1[0]: (86) {G2,W2,D2,L1,V0,M1} R(85,76) { hasEssence( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (427) {G3,W2,D2,L1,V0,M1} R(77,105);r(86) { exists( skol1 )
% 0.49/1.14 }.
% 0.49/1.14 parent0: (552) {G2,W2,D2,L1,V0,M1} { exists( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 0 ==> 0
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 resolution: (553) {G1,W0,D0,L0,V0,M0} { }.
% 0.49/1.14 parent0[0]: (79) {G0,W2,D2,L1,V0,M1} I { ! exists( skol1 ) }.
% 0.49/1.14 parent1[0]: (427) {G3,W2,D2,L1,V0,M1} R(77,105);r(86) { exists( skol1 ) }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 substitution1:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 subsumption: (432) {G4,W0,D0,L0,V0,M0} S(427);r(79) { }.
% 0.49/1.14 parent0: (553) {G1,W0,D0,L0,V0,M0} { }.
% 0.49/1.14 substitution0:
% 0.49/1.14 end
% 0.49/1.14 permutation0:
% 0.49/1.14 end
% 0.49/1.14
% 0.49/1.14 Proof check complete!
% 0.49/1.14
% 0.49/1.14 Memory use:
% 0.49/1.14
% 0.49/1.14 space for terms: 4619
% 0.49/1.14 space for clauses: 18124
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 clauses generated: 1085
% 0.49/1.14 clauses kept: 433
% 0.49/1.14 clauses selected: 204
% 0.49/1.14 clauses deleted: 3
% 0.49/1.14 clauses inuse deleted: 0
% 0.49/1.14
% 0.49/1.14 subsentry: 851
% 0.49/1.14 literals s-matched: 823
% 0.49/1.14 literals matched: 815
% 0.49/1.14 full subsumption: 0
% 0.49/1.14
% 0.49/1.14 checksum: 345346552
% 0.49/1.14
% 0.49/1.14
% 0.49/1.14 Bliksem ended
%------------------------------------------------------------------------------