%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PHI023+1 : TPTP v8.1.0. Released v7.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 : Mon Jul 18 16:43:08 EDT 2022
% Result : Theorem 0.43s 1.07s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PHI023+1 : TPTP v8.1.0. Released v7.4.0.
% 0.11/0.13 % Command : bliksem %s
% 0.13/0.33 % Computer : n021.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Thu Jun 2 01:10:01 EDT 2022
% 0.19/0.34 % CPUTime :
% 0.43/1.06 *** allocated 10000 integers for termspace/termends
% 0.43/1.06 *** allocated 10000 integers for clauses
% 0.43/1.06 *** allocated 10000 integers for justifications
% 0.43/1.06 Bliksem 1.12
% 0.43/1.06
% 0.43/1.06
% 0.43/1.06 Automatic Strategy Selection
% 0.43/1.06
% 0.43/1.06
% 0.43/1.06 Clauses:
% 0.43/1.06
% 0.43/1.06 { ! selfCaused( X ), essenceInvExistence( X ) }.
% 0.43/1.06 { ! selfCaused( X ), natureConcOnlyByExistence( X ) }.
% 0.43/1.06 { ! essenceInvExistence( X ), ! natureConcOnlyByExistence( X ), selfCaused
% 0.43/1.06 ( X ) }.
% 0.43/1.06 { ! finiteAfterItsKind( X ), canBeLimitedBy( X, Y ) }.
% 0.43/1.06 { ! finiteAfterItsKind( X ), sameKind( X, Y ) }.
% 0.43/1.06 { ! canBeLimitedBy( X, Y ), ! sameKind( X, Y ), finiteAfterItsKind( X ) }.
% 0.43/1.06 { ! substance( X ), inItself( X ) }.
% 0.43/1.06 { ! substance( X ), conceivedThruItself( X ) }.
% 0.43/1.06 { ! inItself( X ), ! conceivedThruItself( X ), substance( X ) }.
% 0.43/1.06 { ! attribute( X ), intPercAsConstEssSub( X ) }.
% 0.43/1.06 { ! intPercAsConstEssSub( X ), attribute( X ) }.
% 0.43/1.06 { ! mode( X ), alpha1( X, Y ), alpha6( X, Z ) }.
% 0.43/1.06 { ! alpha1( X, Y ), mode( X ) }.
% 0.43/1.06 { ! alpha6( X, Z ), mode( X ) }.
% 0.43/1.06 { ! alpha6( X, Y ), existsIn( X, Y ) }.
% 0.43/1.06 { ! alpha6( X, Y ), conceivedThru( X, Y ) }.
% 0.43/1.06 { ! existsIn( X, Y ), ! conceivedThru( X, Y ), alpha6( X, Y ) }.
% 0.43/1.06 { ! alpha1( X, Y ), modification( X, Y ) }.
% 0.43/1.06 { ! alpha1( X, Y ), substance( Y ) }.
% 0.43/1.06 { ! modification( X, Y ), ! substance( Y ), alpha1( X, Y ) }.
% 0.43/1.06 { ! god( X ), being( X ) }.
% 0.43/1.06 { ! god( X ), absolutelyInfinite( X ) }.
% 0.43/1.06 { ! being( X ), ! absolutelyInfinite( X ), god( X ) }.
% 0.43/1.06 { ! absolutelyInfinite( X ), substance( X ) }.
% 0.43/1.06 { ! absolutelyInfinite( X ), alpha7( X, Y ) }.
% 0.43/1.06 { ! substance( X ), ! alpha7( X, Y ), absolutelyInfinite( X ) }.
% 0.43/1.06 { ! alpha7( X, Y ), constInInfAttributes( X ) }.
% 0.43/1.06 { ! alpha7( X, Y ), alpha9( X, Y ) }.
% 0.43/1.06 { ! constInInfAttributes( X ), ! alpha9( X, Y ), alpha7( X, Y ) }.
% 0.43/1.06 { ! alpha9( X, Y ), ! attributeOf( Y, X ), alpha2( Y ) }.
% 0.43/1.06 { attributeOf( Y, X ), alpha9( X, Y ) }.
% 0.43/1.06 { ! alpha2( Y ), alpha9( X, Y ) }.
% 0.43/1.06 { ! alpha2( X ), expressesEternalEssentiality( X ) }.
% 0.43/1.06 { ! alpha2( X ), expressesInfiniteEssentiality( X ) }.
% 0.43/1.06 { ! expressesEternalEssentiality( X ), ! expressesInfiniteEssentiality( X )
% 0.43/1.06 , alpha2( X ) }.
% 0.43/1.06 { ! free( X ), existsOnlyByNecessityOfOwnNature( X ) }.
% 0.43/1.06 { ! free( X ), alpha3( X, Y ) }.
% 0.43/1.06 { ! existsOnlyByNecessityOfOwnNature( X ), ! alpha3( X, Y ), free( X ) }.
% 0.43/1.06 { ! alpha3( X, Y ), ! actionOf( Y, X ), determinedByItselfAlone( Y, X ) }.
% 0.43/1.06 { actionOf( Y, X ), alpha3( X, Y ) }.
% 0.43/1.06 { ! determinedByItselfAlone( Y, X ), alpha3( X, Y ) }.
% 0.43/1.06 { ! necessary( X ), externalTo( Y, X ) }.
% 0.43/1.06 { ! necessary( X ), alpha8( X, Y ) }.
% 0.43/1.06 { ! externalTo( Y, X ), ! alpha8( X, Y ), necessary( X ) }.
% 0.43/1.06 { ! alpha8( X, Y ), determinedByFixedMethod( X, Y ) }.
% 0.43/1.06 { ! alpha8( X, Y ), alpha10( X, Y ) }.
% 0.43/1.06 { ! determinedByFixedMethod( X, Y ), ! alpha10( X, Y ), alpha8( X, Y ) }.
% 0.43/1.06 { ! alpha10( X, Y ), determinedByDefiniteMethod( X, Y ) }.
% 0.43/1.06 { ! alpha10( X, Y ), alpha4( Y ) }.
% 0.43/1.06 { ! determinedByDefiniteMethod( X, Y ), ! alpha4( Y ), alpha10( X, Y ) }.
% 0.43/1.06 { ! alpha4( X ), isMethodAction( X ), isMethodExistence( X ) }.
% 0.43/1.06 { ! isMethodAction( X ), alpha4( X ) }.
% 0.43/1.06 { ! isMethodExistence( X ), alpha4( X ) }.
% 0.43/1.06 { ! eternity( X ), existConcFollowFromDefEternal( X ) }.
% 0.43/1.06 { ! existConcFollowFromDefEternal( X ), eternity( X ) }.
% 0.43/1.06 { ! exists( X ), existsIn( X, X ), alpha5( X, Y ) }.
% 0.43/1.06 { ! existsIn( X, X ), exists( X ) }.
% 0.43/1.06 { ! alpha5( X, Y ), exists( X ) }.
% 0.43/1.06 { ! alpha5( X, Y ), existsIn( X, Y ) }.
% 0.43/1.06 { ! alpha5( X, Y ), ! X = Y }.
% 0.43/1.06 { ! existsIn( X, Y ), X = Y, alpha5( X, Y ) }.
% 0.43/1.06 { conceivedThru( X, X ), conceivedThru( X, Y ) }.
% 0.43/1.06 { conceivedThru( X, X ), ! X = Y }.
% 0.43/1.06 { ! definiteCause( X ), effectNecessarilyFollowsFrom( Y, X ) }.
% 0.43/1.06 { ! definiteCause( X ), definiteCause( X ), ! effectNecessarilyFollowsFrom
% 0.43/1.06 ( Y, X ) }.
% 0.43/1.06 { ! knowledgeOfEffect( X, Y ), knowledgeOfACause( X ) }.
% 0.43/1.06 { ! knowledgeOfACause( X ), knowledgeOfEffect( X, Y ) }.
% 0.43/1.06 { ! haveNothingInCommon( X, Y ), alpha11( X, Y ) }.
% 0.43/1.06 { ! haveNothingInCommon( X, Y ), ! conceptionInvolves( Y, X ) }.
% 0.43/1.06 { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf( X, Y ) }.
% 0.43/1.06 { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf( Y, X ) }.
% 0.43/1.06 { ! alpha11( X, Y ), ! conceptionInvolves( X, Y ) }.
% 0.43/1.06 { canBeUnderstoodInTermsOf( X, Y ), canBeUnderstoodInTermsOf( Y, X ),
% 0.43/1.06 conceptionInvolves( X, Y ), alpha11( X, Y ) }.
% 0.43/1.06 { ! trueIdea( X ), correspondWith( X, Y ) }.
% 0.43/1.07 { ! trueIdea( X ), ideateOf( Y, X ), objectOf( Y, X ) }.
% 0.43/1.07 { ! canBeConceivedAsNonExisting( X ), ! essenceInvExistence( X ) }.
% 0.43/1.07 { ! inItself( X ), selfCaused( X ) }.
% 0.43/1.07 { ! being( X ), hasEssence( X ) }.
% 0.43/1.07 { ! essenceInvExistence( X ), ! hasEssence( X ), exists( X ) }.
% 0.43/1.07 { god( skol1 ) }.
% 0.43/1.07 { ! exists( skol1 ) }.
% 0.43/1.07
% 0.43/1.07 percentage equality = 0.011173, percentage horn = 0.886076
% 0.43/1.07 This is a problem with some equality
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 Options Used:
% 0.43/1.07
% 0.43/1.07 useres = 1
% 0.43/1.07 useparamod = 1
% 0.43/1.07 useeqrefl = 1
% 0.43/1.07 useeqfact = 1
% 0.43/1.07 usefactor = 1
% 0.43/1.07 usesimpsplitting = 0
% 0.43/1.07 usesimpdemod = 5
% 0.43/1.07 usesimpres = 3
% 0.43/1.07
% 0.43/1.07 resimpinuse = 1000
% 0.43/1.07 resimpclauses = 20000
% 0.43/1.07 substype = eqrewr
% 0.43/1.07 backwardsubs = 1
% 0.43/1.07 selectoldest = 5
% 0.43/1.07
% 0.43/1.07 litorderings [0] = split
% 0.43/1.07 litorderings [1] = extend the termordering, first sorting on arguments
% 0.43/1.07
% 0.43/1.07 termordering = kbo
% 0.43/1.07
% 0.43/1.07 litapriori = 0
% 0.43/1.07 termapriori = 1
% 0.43/1.07 litaposteriori = 0
% 0.43/1.07 termaposteriori = 0
% 0.43/1.07 demodaposteriori = 0
% 0.43/1.07 ordereqreflfact = 0
% 0.43/1.07
% 0.43/1.07 litselect = negord
% 0.43/1.07
% 0.43/1.07 maxweight = 15
% 0.43/1.07 maxdepth = 30000
% 0.43/1.07 maxlength = 115
% 0.43/1.07 maxnrvars = 195
% 0.43/1.07 excuselevel = 1
% 0.43/1.07 increasemaxweight = 1
% 0.43/1.07
% 0.43/1.07 maxselected = 10000000
% 0.43/1.07 maxnrclauses = 10000000
% 0.43/1.07
% 0.43/1.07 showgenerated = 0
% 0.43/1.07 showkept = 0
% 0.43/1.07 showselected = 0
% 0.43/1.07 showdeleted = 0
% 0.43/1.07 showresimp = 1
% 0.43/1.07 showstatus = 2000
% 0.43/1.07
% 0.43/1.07 prologoutput = 0
% 0.43/1.07 nrgoals = 5000000
% 0.43/1.07 totalproof = 1
% 0.43/1.07
% 0.43/1.07 Symbols occurring in the translation:
% 0.43/1.07
% 0.43/1.07 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.43/1.07 . [1, 2] (w:1, o:46, a:1, s:1, b:0),
% 0.43/1.07 ! [4, 1] (w:0, o:10, a:1, s:1, b:0),
% 0.43/1.07 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.43/1.07 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.43/1.07 selfCaused [36, 1] (w:1, o:15, a:1, s:1, b:0),
% 0.43/1.07 essenceInvExistence [37, 1] (w:1, o:18, a:1, s:1, b:0),
% 0.43/1.07 natureConcOnlyByExistence [38, 1] (w:1, o:20, a:1, s:1, b:0),
% 0.43/1.07 finiteAfterItsKind [40, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.43/1.07 canBeLimitedBy [41, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.43/1.07 sameKind [42, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.43/1.07 substance [43, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.43/1.07 inItself [44, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.43/1.07 conceivedThruItself [45, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.43/1.07 attribute [46, 1] (w:1, o:36, a:1, s:1, b:0),
% 0.43/1.07 intPercAsConstEssSub [47, 1] (w:1, o:37, a:1, s:1, b:0),
% 0.43/1.07 mode [49, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.43/1.07 modification [50, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.43/1.07 existsIn [51, 2] (w:1, o:79, a:1, s:1, b:0),
% 0.43/1.07 conceivedThru [52, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.43/1.07 god [53, 1] (w:1, o:39, a:1, s:1, b:0),
% 0.43/1.07 being [54, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.43/1.07 absolutelyInfinite [55, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.43/1.07 constInInfAttributes [56, 1] (w:1, o:40, a:1, s:1, b:0),
% 0.43/1.07 attributeOf [57, 2] (w:1, o:81, a:1, s:1, b:0),
% 0.43/1.07 expressesEternalEssentiality [58, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.43/1.07 expressesInfiniteEssentiality [59, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.43/1.07 free [60, 1] (w:1, o:38, a:1, s:1, b:0),
% 0.43/1.07 existsOnlyByNecessityOfOwnNature [61, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.43/1.07
% 0.43/1.07 actionOf [62, 2] (w:1, o:82, a:1, s:1, b:0),
% 0.43/1.07 determinedByItselfAlone [63, 2] (w:1, o:76, a:1, s:1, b:0),
% 0.43/1.07 necessary [64, 1] (w:1, o:41, a:1, s:1, b:0),
% 0.43/1.07 externalTo [65, 2] (w:1, o:83, a:1, s:1, b:0),
% 0.43/1.07 determinedByFixedMethod [66, 2] (w:1, o:77, a:1, s:1, b:0),
% 0.43/1.07 determinedByDefiniteMethod [67, 2] (w:1, o:78, a:1, s:1, b:0),
% 0.43/1.07 isMethodAction [68, 1] (w:1, o:42, a:1, s:1, b:0),
% 0.43/1.07 isMethodExistence [69, 1] (w:1, o:43, a:1, s:1, b:0),
% 0.43/1.07 eternity [70, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.43/1.07 existConcFollowFromDefEternal [71, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.43/1.07 exists [72, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.43/1.07 definiteCause [73, 1] (w:1, o:17, a:1, s:1, b:0),
% 0.43/1.07 effectNecessarilyFollowsFrom [74, 2] (w:1, o:84, a:1, s:1, b:0),
% 0.43/1.07 knowledgeOfEffect [75, 2] (w:1, o:85, a:1, s:1, b:0),
% 0.43/1.07 knowledgeOfACause [76, 1] (w:1, o:44, a:1, s:1, b:0),
% 0.43/1.07 haveNothingInCommon [77, 2] (w:1, o:86, a:1, s:1, b:0),
% 0.43/1.07 canBeUnderstoodInTermsOf [78, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.43/1.07 conceptionInvolves [79, 2] (w:1, o:74, a:1, s:1, b:0),
% 0.43/1.07 trueIdea [80, 1] (w:1, o:45, a:1, s:1, b:0),
% 0.43/1.07 correspondWith [81, 2] (w:1, o:75, a:1, s:1, b:0),
% 0.43/1.07 ideateOf [82, 2] (w:1, o:87, a:1, s:1, b:0),
% 0.43/1.07 objectOf [83, 2] (w:1, o:88, a:1, s:1, b:0),
% 0.43/1.07 canBeConceivedAsNonExisting [84, 1] (w:1, o:16, a:1, s:1, b:0),
% 0.43/1.07 hasEssence [85, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.43/1.07 alpha1 [86, 2] (w:1, o:89, a:1, s:1, b:1),
% 0.43/1.07 alpha2 [87, 1] (w:1, o:32, a:1, s:1, b:1),
% 0.43/1.07 alpha3 [88, 2] (w:1, o:90, a:1, s:1, b:1),
% 0.43/1.07 alpha4 [89, 1] (w:1, o:33, a:1, s:1, b:1),
% 0.43/1.07 alpha5 [90, 2] (w:1, o:91, a:1, s:1, b:1),
% 0.43/1.07 alpha6 [91, 2] (w:1, o:92, a:1, s:1, b:1),
% 0.43/1.07 alpha7 [92, 2] (w:1, o:93, a:1, s:1, b:1),
% 0.43/1.07 alpha8 [93, 2] (w:1, o:94, a:1, s:1, b:1),
% 0.43/1.07 alpha9 [94, 2] (w:1, o:95, a:1, s:1, b:1),
% 0.43/1.07 alpha10 [95, 2] (w:1, o:96, a:1, s:1, b:1),
% 0.43/1.07 alpha11 [96, 2] (w:1, o:97, a:1, s:1, b:1),
% 0.43/1.07 skol1 [97, 0] (w:1, o:9, a:1, s:1, b:1).
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 Starting Search:
% 0.43/1.07
% 0.43/1.07 *** allocated 15000 integers for clauses
% 0.43/1.07 *** allocated 22500 integers for clauses
% 0.43/1.07
% 0.43/1.07 Bliksems!, er is een bewijs:
% 0.43/1.07 % SZS status Theorem
% 0.43/1.07 % SZS output start Refutation
% 0.43/1.07
% 0.43/1.07 (0) {G0,W4,D2,L2,V1,M2} I { ! selfCaused( X ), essenceInvExistence( X ) }.
% 0.43/1.07 (6) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), inItself( X ) }.
% 0.43/1.07 (20) {G0,W4,D2,L2,V1,M2} I { ! god( X ), being( X ) }.
% 0.43/1.07 (21) {G0,W4,D2,L2,V1,M2} I { ! god( X ), absolutelyInfinite( X ) }.
% 0.43/1.07 (23) {G0,W4,D2,L2,V1,M2} I { ! absolutelyInfinite( X ), substance( X ) }.
% 0.43/1.07 (74) {G0,W4,D2,L2,V1,M2} I { ! inItself( X ), selfCaused( X ) }.
% 0.43/1.07 (75) {G0,W4,D2,L2,V1,M2} I { ! being( X ), hasEssence( X ) }.
% 0.43/1.07 (76) {G0,W6,D2,L3,V1,M3} I { ! essenceInvExistence( X ), ! hasEssence( X )
% 0.43/1.07 , exists( X ) }.
% 0.43/1.07 (77) {G0,W2,D2,L1,V0,M1} I { god( skol1 ) }.
% 0.43/1.07 (78) {G0,W2,D2,L1,V0,M1} I { ! exists( skol1 ) }.
% 0.43/1.07 (82) {G1,W4,D2,L2,V1,M2} R(74,0) { ! inItself( X ), essenceInvExistence( X
% 0.43/1.07 ) }.
% 0.43/1.07 (87) {G1,W2,D2,L1,V0,M1} R(21,77) { absolutelyInfinite( skol1 ) }.
% 0.43/1.07 (88) {G2,W2,D2,L1,V0,M1} R(87,23) { substance( skol1 ) }.
% 0.43/1.07 (90) {G1,W2,D2,L1,V0,M1} R(20,77) { being( skol1 ) }.
% 0.43/1.07 (91) {G2,W2,D2,L1,V0,M1} R(90,75) { hasEssence( skol1 ) }.
% 0.43/1.07 (95) {G3,W2,D2,L1,V0,M1} R(6,88) { inItself( skol1 ) }.
% 0.43/1.07 (103) {G4,W2,D2,L1,V0,M1} R(95,82) { essenceInvExistence( skol1 ) }.
% 0.43/1.07 (400) {G5,W2,D2,L1,V0,M1} R(76,103);r(91) { exists( skol1 ) }.
% 0.43/1.07 (405) {G6,W0,D0,L0,V0,M0} S(400);r(78) { }.
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 % SZS output end Refutation
% 0.43/1.07 found a proof!
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 Unprocessed initial clauses:
% 0.43/1.07
% 0.43/1.07 (407) {G0,W4,D2,L2,V1,M2} { ! selfCaused( X ), essenceInvExistence( X )
% 0.43/1.07 }.
% 0.43/1.07 (408) {G0,W4,D2,L2,V1,M2} { ! selfCaused( X ), natureConcOnlyByExistence(
% 0.43/1.07 X ) }.
% 0.43/1.07 (409) {G0,W6,D2,L3,V1,M3} { ! essenceInvExistence( X ), !
% 0.43/1.07 natureConcOnlyByExistence( X ), selfCaused( X ) }.
% 0.43/1.07 (410) {G0,W5,D2,L2,V2,M2} { ! finiteAfterItsKind( X ), canBeLimitedBy( X,
% 0.43/1.07 Y ) }.
% 0.43/1.07 (411) {G0,W5,D2,L2,V2,M2} { ! finiteAfterItsKind( X ), sameKind( X, Y )
% 0.43/1.07 }.
% 0.43/1.07 (412) {G0,W8,D2,L3,V2,M3} { ! canBeLimitedBy( X, Y ), ! sameKind( X, Y ),
% 0.43/1.07 finiteAfterItsKind( X ) }.
% 0.43/1.07 (413) {G0,W4,D2,L2,V1,M2} { ! substance( X ), inItself( X ) }.
% 0.43/1.07 (414) {G0,W4,D2,L2,V1,M2} { ! substance( X ), conceivedThruItself( X ) }.
% 0.43/1.07 (415) {G0,W6,D2,L3,V1,M3} { ! inItself( X ), ! conceivedThruItself( X ),
% 0.43/1.07 substance( X ) }.
% 0.43/1.07 (416) {G0,W4,D2,L2,V1,M2} { ! attribute( X ), intPercAsConstEssSub( X )
% 0.43/1.07 }.
% 0.43/1.07 (417) {G0,W4,D2,L2,V1,M2} { ! intPercAsConstEssSub( X ), attribute( X )
% 0.43/1.07 }.
% 0.43/1.07 (418) {G0,W8,D2,L3,V3,M3} { ! mode( X ), alpha1( X, Y ), alpha6( X, Z )
% 0.43/1.07 }.
% 0.43/1.07 (419) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), mode( X ) }.
% 0.43/1.07 (420) {G0,W5,D2,L2,V2,M2} { ! alpha6( X, Z ), mode( X ) }.
% 0.43/1.07 (421) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), existsIn( X, Y ) }.
% 0.43/1.07 (422) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), conceivedThru( X, Y ) }.
% 0.43/1.07 (423) {G0,W9,D2,L3,V2,M3} { ! existsIn( X, Y ), ! conceivedThru( X, Y ),
% 0.43/1.07 alpha6( X, Y ) }.
% 0.43/1.07 (424) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), modification( X, Y ) }.
% 0.43/1.07 (425) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), substance( Y ) }.
% 0.43/1.07 (426) {G0,W8,D2,L3,V2,M3} { ! modification( X, Y ), ! substance( Y ),
% 0.43/1.07 alpha1( X, Y ) }.
% 0.43/1.07 (427) {G0,W4,D2,L2,V1,M2} { ! god( X ), being( X ) }.
% 0.43/1.07 (428) {G0,W4,D2,L2,V1,M2} { ! god( X ), absolutelyInfinite( X ) }.
% 0.43/1.07 (429) {G0,W6,D2,L3,V1,M3} { ! being( X ), ! absolutelyInfinite( X ), god(
% 0.43/1.07 X ) }.
% 0.43/1.07 (430) {G0,W4,D2,L2,V1,M2} { ! absolutelyInfinite( X ), substance( X ) }.
% 0.43/1.07 (431) {G0,W5,D2,L2,V2,M2} { ! absolutelyInfinite( X ), alpha7( X, Y ) }.
% 0.43/1.07 (432) {G0,W7,D2,L3,V2,M3} { ! substance( X ), ! alpha7( X, Y ),
% 0.43/1.07 absolutelyInfinite( X ) }.
% 0.43/1.07 (433) {G0,W5,D2,L2,V2,M2} { ! alpha7( X, Y ), constInInfAttributes( X )
% 0.43/1.07 }.
% 0.43/1.07 (434) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), alpha9( X, Y ) }.
% 0.43/1.07 (435) {G0,W8,D2,L3,V2,M3} { ! constInInfAttributes( X ), ! alpha9( X, Y )
% 0.43/1.07 , alpha7( X, Y ) }.
% 0.43/1.07 (436) {G0,W8,D2,L3,V2,M3} { ! alpha9( X, Y ), ! attributeOf( Y, X ),
% 0.43/1.07 alpha2( Y ) }.
% 0.43/1.07 (437) {G0,W6,D2,L2,V2,M2} { attributeOf( Y, X ), alpha9( X, Y ) }.
% 0.43/1.07 (438) {G0,W5,D2,L2,V2,M2} { ! alpha2( Y ), alpha9( X, Y ) }.
% 0.43/1.07 (439) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), expressesEternalEssentiality( X
% 0.43/1.07 ) }.
% 0.43/1.07 (440) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), expressesInfiniteEssentiality(
% 0.43/1.07 X ) }.
% 0.43/1.07 (441) {G0,W6,D2,L3,V1,M3} { ! expressesEternalEssentiality( X ), !
% 0.43/1.07 expressesInfiniteEssentiality( X ), alpha2( X ) }.
% 0.43/1.07 (442) {G0,W4,D2,L2,V1,M2} { ! free( X ), existsOnlyByNecessityOfOwnNature
% 0.43/1.07 ( X ) }.
% 0.43/1.07 (443) {G0,W5,D2,L2,V2,M2} { ! free( X ), alpha3( X, Y ) }.
% 0.43/1.07 (444) {G0,W7,D2,L3,V2,M3} { ! existsOnlyByNecessityOfOwnNature( X ), !
% 0.43/1.07 alpha3( X, Y ), free( X ) }.
% 0.43/1.07 (445) {G0,W9,D2,L3,V2,M3} { ! alpha3( X, Y ), ! actionOf( Y, X ),
% 0.43/1.07 determinedByItselfAlone( Y, X ) }.
% 0.43/1.07 (446) {G0,W6,D2,L2,V2,M2} { actionOf( Y, X ), alpha3( X, Y ) }.
% 0.43/1.07 (447) {G0,W6,D2,L2,V2,M2} { ! determinedByItselfAlone( Y, X ), alpha3( X,
% 0.43/1.07 Y ) }.
% 0.43/1.07 (448) {G0,W5,D2,L2,V2,M2} { ! necessary( X ), externalTo( Y, X ) }.
% 0.43/1.07 (449) {G0,W5,D2,L2,V2,M2} { ! necessary( X ), alpha8( X, Y ) }.
% 0.43/1.07 (450) {G0,W8,D2,L3,V2,M3} { ! externalTo( Y, X ), ! alpha8( X, Y ),
% 0.43/1.07 necessary( X ) }.
% 0.43/1.07 (451) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), determinedByFixedMethod( X,
% 0.43/1.07 Y ) }.
% 0.43/1.07 (452) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), alpha10( X, Y ) }.
% 0.43/1.07 (453) {G0,W9,D2,L3,V2,M3} { ! determinedByFixedMethod( X, Y ), ! alpha10(
% 0.43/1.07 X, Y ), alpha8( X, Y ) }.
% 0.43/1.07 (454) {G0,W6,D2,L2,V2,M2} { ! alpha10( X, Y ), determinedByDefiniteMethod
% 0.43/1.07 ( X, Y ) }.
% 0.43/1.07 (455) {G0,W5,D2,L2,V2,M2} { ! alpha10( X, Y ), alpha4( Y ) }.
% 0.43/1.07 (456) {G0,W8,D2,L3,V2,M3} { ! determinedByDefiniteMethod( X, Y ), ! alpha4
% 0.43/1.07 ( Y ), alpha10( X, Y ) }.
% 0.43/1.07 (457) {G0,W6,D2,L3,V1,M3} { ! alpha4( X ), isMethodAction( X ),
% 0.43/1.07 isMethodExistence( X ) }.
% 0.43/1.07 (458) {G0,W4,D2,L2,V1,M2} { ! isMethodAction( X ), alpha4( X ) }.
% 0.43/1.07 (459) {G0,W4,D2,L2,V1,M2} { ! isMethodExistence( X ), alpha4( X ) }.
% 0.43/1.07 (460) {G0,W4,D2,L2,V1,M2} { ! eternity( X ), existConcFollowFromDefEternal
% 0.43/1.07 ( X ) }.
% 0.43/1.07 (461) {G0,W4,D2,L2,V1,M2} { ! existConcFollowFromDefEternal( X ), eternity
% 0.43/1.07 ( X ) }.
% 0.43/1.07 (462) {G0,W8,D2,L3,V2,M3} { ! exists( X ), existsIn( X, X ), alpha5( X, Y
% 0.43/1.07 ) }.
% 0.43/1.07 (463) {G0,W5,D2,L2,V1,M2} { ! existsIn( X, X ), exists( X ) }.
% 0.43/1.07 (464) {G0,W5,D2,L2,V2,M2} { ! alpha5( X, Y ), exists( X ) }.
% 0.43/1.07 (465) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), existsIn( X, Y ) }.
% 0.43/1.07 (466) {G0,W6,D2,L2,V2,M2} { ! alpha5( X, Y ), ! X = Y }.
% 0.43/1.07 (467) {G0,W9,D2,L3,V2,M3} { ! existsIn( X, Y ), X = Y, alpha5( X, Y ) }.
% 0.43/1.07 (468) {G0,W6,D2,L2,V2,M2} { conceivedThru( X, X ), conceivedThru( X, Y )
% 0.43/1.07 }.
% 0.43/1.07 (469) {G0,W6,D2,L2,V2,M2} { conceivedThru( X, X ), ! X = Y }.
% 0.43/1.07 (470) {G0,W5,D2,L2,V2,M2} { ! definiteCause( X ),
% 0.43/1.07 effectNecessarilyFollowsFrom( Y, X ) }.
% 0.43/1.07 (471) {G0,W7,D2,L3,V2,M3} { ! definiteCause( X ), definiteCause( X ), !
% 0.43/1.07 effectNecessarilyFollowsFrom( Y, X ) }.
% 0.43/1.07 (472) {G0,W5,D2,L2,V2,M2} { ! knowledgeOfEffect( X, Y ), knowledgeOfACause
% 0.43/1.07 ( X ) }.
% 0.43/1.07 (473) {G0,W5,D2,L2,V2,M2} { ! knowledgeOfACause( X ), knowledgeOfEffect( X
% 0.43/1.07 , Y ) }.
% 0.43/1.07 (474) {G0,W6,D2,L2,V2,M2} { ! haveNothingInCommon( X, Y ), alpha11( X, Y )
% 0.43/1.07 }.
% 0.43/1.07 (475) {G0,W6,D2,L2,V2,M2} { ! haveNothingInCommon( X, Y ), !
% 0.43/1.07 conceptionInvolves( Y, X ) }.
% 0.43/1.07 (476) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf
% 0.43/1.07 ( X, Y ) }.
% 0.43/1.07 (477) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), ! canBeUnderstoodInTermsOf
% 0.43/1.07 ( Y, X ) }.
% 0.43/1.07 (478) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), ! conceptionInvolves( X, Y
% 0.43/1.07 ) }.
% 0.43/1.07 (479) {G0,W12,D2,L4,V2,M4} { canBeUnderstoodInTermsOf( X, Y ),
% 0.43/1.07 canBeUnderstoodInTermsOf( Y, X ), conceptionInvolves( X, Y ), alpha11( X
% 0.43/1.07 , Y ) }.
% 0.43/1.07 (480) {G0,W5,D2,L2,V2,M2} { ! trueIdea( X ), correspondWith( X, Y ) }.
% 0.43/1.07 (481) {G0,W8,D2,L3,V2,M3} { ! trueIdea( X ), ideateOf( Y, X ), objectOf( Y
% 0.43/1.07 , X ) }.
% 0.43/1.07 (482) {G0,W4,D2,L2,V1,M2} { ! canBeConceivedAsNonExisting( X ), !
% 0.43/1.07 essenceInvExistence( X ) }.
% 0.43/1.07 (483) {G0,W4,D2,L2,V1,M2} { ! inItself( X ), selfCaused( X ) }.
% 0.43/1.07 (484) {G0,W4,D2,L2,V1,M2} { ! being( X ), hasEssence( X ) }.
% 0.43/1.07 (485) {G0,W6,D2,L3,V1,M3} { ! essenceInvExistence( X ), ! hasEssence( X )
% 0.43/1.07 , exists( X ) }.
% 0.43/1.07 (486) {G0,W2,D2,L1,V0,M1} { god( skol1 ) }.
% 0.43/1.07 (487) {G0,W2,D2,L1,V0,M1} { ! exists( skol1 ) }.
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 Total Proof:
% 0.43/1.07
% 0.43/1.07 subsumption: (0) {G0,W4,D2,L2,V1,M2} I { ! selfCaused( X ),
% 0.43/1.07 essenceInvExistence( X ) }.
% 0.43/1.07 parent0: (407) {G0,W4,D2,L2,V1,M2} { ! selfCaused( X ),
% 0.43/1.07 essenceInvExistence( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (6) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), inItself( X )
% 0.43/1.07 }.
% 0.43/1.07 parent0: (413) {G0,W4,D2,L2,V1,M2} { ! substance( X ), inItself( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (20) {G0,W4,D2,L2,V1,M2} I { ! god( X ), being( X ) }.
% 0.43/1.07 parent0: (427) {G0,W4,D2,L2,V1,M2} { ! god( X ), being( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (21) {G0,W4,D2,L2,V1,M2} I { ! god( X ), absolutelyInfinite( X
% 0.43/1.07 ) }.
% 0.43/1.07 parent0: (428) {G0,W4,D2,L2,V1,M2} { ! god( X ), absolutelyInfinite( X )
% 0.43/1.07 }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (23) {G0,W4,D2,L2,V1,M2} I { ! absolutelyInfinite( X ),
% 0.43/1.07 substance( X ) }.
% 0.43/1.07 parent0: (430) {G0,W4,D2,L2,V1,M2} { ! absolutelyInfinite( X ), substance
% 0.43/1.07 ( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (74) {G0,W4,D2,L2,V1,M2} I { ! inItself( X ), selfCaused( X )
% 0.43/1.07 }.
% 0.43/1.07 parent0: (483) {G0,W4,D2,L2,V1,M2} { ! inItself( X ), selfCaused( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (75) {G0,W4,D2,L2,V1,M2} I { ! being( X ), hasEssence( X ) }.
% 0.43/1.07 parent0: (484) {G0,W4,D2,L2,V1,M2} { ! being( X ), hasEssence( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (76) {G0,W6,D2,L3,V1,M3} I { ! essenceInvExistence( X ), !
% 0.43/1.07 hasEssence( X ), exists( X ) }.
% 0.43/1.07 parent0: (485) {G0,W6,D2,L3,V1,M3} { ! essenceInvExistence( X ), !
% 0.43/1.07 hasEssence( X ), exists( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 1 ==> 1
% 0.43/1.07 2 ==> 2
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (77) {G0,W2,D2,L1,V0,M1} I { god( skol1 ) }.
% 0.43/1.07 parent0: (486) {G0,W2,D2,L1,V0,M1} { god( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (78) {G0,W2,D2,L1,V0,M1} I { ! exists( skol1 ) }.
% 0.43/1.07 parent0: (487) {G0,W2,D2,L1,V0,M1} { ! exists( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (513) {G1,W4,D2,L2,V1,M2} { essenceInvExistence( X ), !
% 0.43/1.07 inItself( X ) }.
% 0.43/1.07 parent0[0]: (0) {G0,W4,D2,L2,V1,M2} I { ! selfCaused( X ),
% 0.43/1.07 essenceInvExistence( X ) }.
% 0.43/1.07 parent1[1]: (74) {G0,W4,D2,L2,V1,M2} I { ! inItself( X ), selfCaused( X )
% 0.43/1.07 }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (82) {G1,W4,D2,L2,V1,M2} R(74,0) { ! inItself( X ),
% 0.43/1.07 essenceInvExistence( X ) }.
% 0.43/1.07 parent0: (513) {G1,W4,D2,L2,V1,M2} { essenceInvExistence( X ), ! inItself
% 0.43/1.07 ( X ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := X
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 1
% 0.43/1.07 1 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (514) {G1,W2,D2,L1,V0,M1} { absolutelyInfinite( skol1 ) }.
% 0.43/1.07 parent0[0]: (21) {G0,W4,D2,L2,V1,M2} I { ! god( X ), absolutelyInfinite( X
% 0.43/1.07 ) }.
% 0.43/1.07 parent1[0]: (77) {G0,W2,D2,L1,V0,M1} I { god( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (87) {G1,W2,D2,L1,V0,M1} R(21,77) { absolutelyInfinite( skol1
% 0.43/1.07 ) }.
% 0.43/1.07 parent0: (514) {G1,W2,D2,L1,V0,M1} { absolutelyInfinite( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (515) {G1,W2,D2,L1,V0,M1} { substance( skol1 ) }.
% 0.43/1.07 parent0[0]: (23) {G0,W4,D2,L2,V1,M2} I { ! absolutelyInfinite( X ),
% 0.43/1.07 substance( X ) }.
% 0.43/1.07 parent1[0]: (87) {G1,W2,D2,L1,V0,M1} R(21,77) { absolutelyInfinite( skol1 )
% 0.43/1.07 }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (88) {G2,W2,D2,L1,V0,M1} R(87,23) { substance( skol1 ) }.
% 0.43/1.07 parent0: (515) {G1,W2,D2,L1,V0,M1} { substance( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (516) {G1,W2,D2,L1,V0,M1} { being( skol1 ) }.
% 0.43/1.07 parent0[0]: (20) {G0,W4,D2,L2,V1,M2} I { ! god( X ), being( X ) }.
% 0.43/1.07 parent1[0]: (77) {G0,W2,D2,L1,V0,M1} I { god( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (90) {G1,W2,D2,L1,V0,M1} R(20,77) { being( skol1 ) }.
% 0.43/1.07 parent0: (516) {G1,W2,D2,L1,V0,M1} { being( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (517) {G1,W2,D2,L1,V0,M1} { hasEssence( skol1 ) }.
% 0.43/1.07 parent0[0]: (75) {G0,W4,D2,L2,V1,M2} I { ! being( X ), hasEssence( X ) }.
% 0.43/1.07 parent1[0]: (90) {G1,W2,D2,L1,V0,M1} R(20,77) { being( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (91) {G2,W2,D2,L1,V0,M1} R(90,75) { hasEssence( skol1 ) }.
% 0.43/1.07 parent0: (517) {G1,W2,D2,L1,V0,M1} { hasEssence( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (518) {G1,W2,D2,L1,V0,M1} { inItself( skol1 ) }.
% 0.43/1.07 parent0[0]: (6) {G0,W4,D2,L2,V1,M2} I { ! substance( X ), inItself( X ) }.
% 0.43/1.07 parent1[0]: (88) {G2,W2,D2,L1,V0,M1} R(87,23) { substance( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (95) {G3,W2,D2,L1,V0,M1} R(6,88) { inItself( skol1 ) }.
% 0.43/1.07 parent0: (518) {G1,W2,D2,L1,V0,M1} { inItself( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (519) {G2,W2,D2,L1,V0,M1} { essenceInvExistence( skol1 ) }.
% 0.43/1.07 parent0[0]: (82) {G1,W4,D2,L2,V1,M2} R(74,0) { ! inItself( X ),
% 0.43/1.07 essenceInvExistence( X ) }.
% 0.43/1.07 parent1[0]: (95) {G3,W2,D2,L1,V0,M1} R(6,88) { inItself( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (103) {G4,W2,D2,L1,V0,M1} R(95,82) { essenceInvExistence(
% 0.43/1.07 skol1 ) }.
% 0.43/1.07 parent0: (519) {G2,W2,D2,L1,V0,M1} { essenceInvExistence( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (520) {G1,W4,D2,L2,V0,M2} { ! hasEssence( skol1 ), exists(
% 0.43/1.07 skol1 ) }.
% 0.43/1.07 parent0[0]: (76) {G0,W6,D2,L3,V1,M3} I { ! essenceInvExistence( X ), !
% 0.43/1.07 hasEssence( X ), exists( X ) }.
% 0.43/1.07 parent1[0]: (103) {G4,W2,D2,L1,V0,M1} R(95,82) { essenceInvExistence( skol1
% 0.43/1.07 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 X := skol1
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (521) {G2,W2,D2,L1,V0,M1} { exists( skol1 ) }.
% 0.43/1.07 parent0[0]: (520) {G1,W4,D2,L2,V0,M2} { ! hasEssence( skol1 ), exists(
% 0.43/1.07 skol1 ) }.
% 0.43/1.07 parent1[0]: (91) {G2,W2,D2,L1,V0,M1} R(90,75) { hasEssence( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (400) {G5,W2,D2,L1,V0,M1} R(76,103);r(91) { exists( skol1 )
% 0.43/1.07 }.
% 0.43/1.07 parent0: (521) {G2,W2,D2,L1,V0,M1} { exists( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 0 ==> 0
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 resolution: (522) {G1,W0,D0,L0,V0,M0} { }.
% 0.43/1.07 parent0[0]: (78) {G0,W2,D2,L1,V0,M1} I { ! exists( skol1 ) }.
% 0.43/1.07 parent1[0]: (400) {G5,W2,D2,L1,V0,M1} R(76,103);r(91) { exists( skol1 ) }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 substitution1:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 subsumption: (405) {G6,W0,D0,L0,V0,M0} S(400);r(78) { }.
% 0.43/1.07 parent0: (522) {G1,W0,D0,L0,V0,M0} { }.
% 0.43/1.07 substitution0:
% 0.43/1.07 end
% 0.43/1.07 permutation0:
% 0.43/1.07 end
% 0.43/1.07
% 0.43/1.07 Proof check complete!
% 0.43/1.07
% 0.43/1.07 Memory use:
% 0.43/1.07
% 0.43/1.07 space for terms: 4376
% 0.43/1.07 space for clauses: 17355
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 clauses generated: 963
% 0.43/1.07 clauses kept: 406
% 0.43/1.07 clauses selected: 195
% 0.43/1.07 clauses deleted: 2
% 0.43/1.07 clauses inuse deleted: 0
% 0.43/1.07
% 0.43/1.07 subsentry: 690
% 0.43/1.07 literals s-matched: 678
% 0.43/1.07 literals matched: 676
% 0.43/1.07 full subsumption: 0
% 0.43/1.07
% 0.43/1.07 checksum: -1502273864
% 0.43/1.07
% 0.43/1.07
% 0.43/1.07 Bliksem ended
%------------------------------------------------------------------------------