%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PHI025+1 : TPTP v9.0.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 08:22:27 PM UTC 2025 % Result : Satisfiable 3.54s 1.87s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PHI025+1 : TPTP v9.0.0. Released v7.4.0. % 0.14/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.34 % Computer : n016.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 16:28:53 EDT 2025 % 0.14/0.34 % CPUTime : % 3.54/1.87 % 3.54/1.87 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.54/1.87 % 3.54/1.87 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.54/1.88 %$ sameKind > objectOf > modification > knowledgeOfEffect > ideateOf > haveNothingInCommon > externalTo > existsIn > effectNecessarilyFollowsFrom > determinedByItselfAlone > determinedByFixedMethod > determinedByDefiniteMethod > correspondWith > conceptionInvolves > conceivedThru > canBeUnderstoodInTermsOf > canBeLimitedBy > attributeOf > actionOf > trueIdea > substance > selfCaused > necessary > natureConcOnlyByExistence > mode > knowledgeOfACause > isMethodExistence > isMethodAction > intPercAsConstEssSub > inItself > god > free > finiteAfterItsKind > expressesInfiniteEssentiality > expressesEternalEssentiality > existsOnlyByNecessityOfOwnNature > exists > existConcFollowFromDefEternal > eternity > essenceInvExistence > definiteCause > constInInfAttributes > conceivedThruItself > canBeConceivedAsNonExisting > being > attribute > absolutelyInfinite > #nlpp % 3.54/1.88 % 3.54/1.88 %Foreground sorts: % 3.54/1.88 % 3.54/1.88 % 3.54/1.88 %Background operators: % 3.54/1.88 % 3.54/1.88 % 3.54/1.88 %Foreground operators: % 3.54/1.88 tff(being, type, being: $i > $o). % 3.54/1.88 tff(externalTo, type, externalTo: ($i * $i) > $o). % 3.54/1.88 tff(isMethodAction, type, isMethodAction: $i > $o). % 3.54/1.88 tff(intPercAsConstEssSub, type, intPercAsConstEssSub: $i > $o). % 3.54/1.88 tff(necessary, type, necessary: $i > $o). % 3.54/1.88 tff(attributeOf, type, attributeOf: ($i * $i) > $o). % 3.54/1.88 tff(finiteAfterItsKind, type, finiteAfterItsKind: $i > $o). % 3.54/1.88 tff(existsIn, type, existsIn: ($i * $i) > $o). % 3.54/1.88 tff(definiteCause, type, definiteCause: $i > $o). % 3.54/1.88 tff(trueIdea, type, trueIdea: $i > $o). % 3.54/1.88 tff(substance, type, substance: $i > $o). % 3.54/1.88 tff(free, type, free: $i > $o). % 3.54/1.88 tff(knowledgeOfACause, type, knowledgeOfACause: $i > $o). % 3.54/1.88 tff(attribute, type, attribute: $i > $o). % 3.54/1.88 tff(canBeUnderstoodInTermsOf, type, canBeUnderstoodInTermsOf: ($i * $i) > $o). % 3.54/1.88 tff(god, type, god: $i > $o). % 3.54/1.88 tff(existsOnlyByNecessityOfOwnNature, type, existsOnlyByNecessityOfOwnNature: $i > $o). % 3.54/1.88 tff(correspondWith, type, correspondWith: ($i * $i) > $o). % 3.54/1.88 tff(essenceInvExistence, type, essenceInvExistence: $i > $o). % 3.54/1.88 tff(ideateOf, type, ideateOf: ($i * $i) > $o). % 3.54/1.88 tff(mode, type, mode: $i > $o). % 3.54/1.88 tff(haveNothingInCommon, type, haveNothingInCommon: ($i * $i) > $o). % 3.54/1.88 tff(effectNecessarilyFollowsFrom, type, effectNecessarilyFollowsFrom: ($i * $i) > $o). % 3.54/1.88 tff(actionOf, type, actionOf: ($i * $i) > $o). % 3.54/1.88 tff(isMethodExistence, type, isMethodExistence: $i > $o). % 3.54/1.88 tff(determinedByDefiniteMethod, type, determinedByDefiniteMethod: ($i * $i) > $o). % 3.54/1.88 tff(expressesInfiniteEssentiality, type, expressesInfiniteEssentiality: $i > $o). % 3.54/1.88 tff(modification, type, modification: ($i * $i) > $o). % 3.54/1.88 tff(eternity, type, eternity: $i > $o). % 3.54/1.88 tff(determinedByFixedMethod, type, determinedByFixedMethod: ($i * $i) > $o). % 3.54/1.88 tff(selfCaused, type, selfCaused: $i > $o). % 3.54/1.88 tff(determinedByItselfAlone, type, determinedByItselfAlone: ($i * $i) > $o). % 3.54/1.88 tff(inItself, type, inItself: $i > $o). % 3.54/1.88 tff(objectOf, type, objectOf: ($i * $i) > $o). % 3.54/1.88 tff(canBeConceivedAsNonExisting, type, canBeConceivedAsNonExisting: $i > $o). % 3.54/1.88 tff(conceivedThru, type, conceivedThru: ($i * $i) > $o). % 3.54/1.88 tff(absolutelyInfinite, type, absolutelyInfinite: $i > $o). % 3.54/1.88 tff(conceivedThruItself, type, conceivedThruItself: $i > $o). % 3.54/1.88 tff(canBeLimitedBy, type, canBeLimitedBy: ($i * $i) > $o). % 3.54/1.88 tff(conceptionInvolves, type, conceptionInvolves: ($i * $i) > $o). % 3.54/1.88 tff(natureConcOnlyByExistence, type, natureConcOnlyByExistence: $i > $o). % 3.54/1.88 tff(knowledgeOfEffect, type, knowledgeOfEffect: ($i * $i) > $o). % 3.54/1.88 tff(exists, type, exists: $i > $o). % 3.54/1.88 tff(constInInfAttributes, type, constInInfAttributes: $i > $o). % 3.54/1.88 tff(existConcFollowFromDefEternal, type, existConcFollowFromDefEternal: $i > $o). % 3.54/1.88 tff(expressesEternalEssentiality, type, expressesEternalEssentiality: $i > $o). % 3.54/1.88 tff(sameKind, type, sameKind: ($i * $i) > $o). % 3.54/1.88 % 3.54/1.88 %Saturated clause set: % 3.54/1.88 tff(c_262, plain, (![Y_15, X_14]: (~isMethodExistence(Y_15) | ~determinedByDefiniteMethod(X_14, Y_15) | ~determinedByFixedMethod(X_14, Y_15) | ~externalTo(Y_15, X_14)))). % 3.54/1.88 tff(c_260, plain, (![Y_15, X_14]: (~isMethodAction(Y_15) | ~determinedByDefiniteMethod(X_14, Y_15) | ~determinedByFixedMethod(X_14, Y_15) | ~externalTo(Y_15, X_14)))). % 3.54/1.88 tff(c_258, plain, (![Y_11]: (~expressesInfiniteEssentiality(Y_11) | ~expressesEternalEssentiality(Y_11)))). % 3.54/1.88 tff(c_52, plain, (![Y_11, X_10]: (attributeOf(Y_11, X_10) | absolutelyInfinite(X_10) | ~constInInfAttributes(X_10) | ~substance(X_10)))). % 3.54/1.88 tff(c_54, plain, (![Y_13, X_12]: (determinedByItselfAlone(Y_13, X_12) | ~actionOf(Y_13, X_12) | ~free(X_12)))). % 3.54/1.88 tff(c_106, plain, (![Y_28, X_27]: (objectOf(Y_28, X_27) | ideateOf(Y_28, X_27) | ~trueIdea(X_27)))). % 3.54/1.88 tff(c_8, plain, (![X_2, Y_3]: (finiteAfterItsKind(X_2) | ~sameKind(X_2, Y_3) | ~canBeLimitedBy(X_2, Y_3)))). % 3.54/1.88 tff(c_232, plain, (![Y_18]: (mode(Y_18) | ~exists(Y_18)))). % 3.54/1.89 tff(c_32, plain, (![X_6, Z_8]: (~conceivedThru(X_6, Z_8) | ~existsIn(X_6, Z_8) | mode(X_6)))). % 3.54/1.89 tff(c_220, plain, (![Z_94]: (exists(Z_94) | ~mode(Z_94)))). % 3.54/1.89 tff(c_210, plain, (![X_6, Z_8]: (existsIn(X_6, Z_8) | ~mode(X_6)))). % 3.54/1.89 tff(c_48, plain, (![Y_11, X_10]: (expressesEternalEssentiality(Y_11) | ~attributeOf(Y_11, X_10) | ~absolutelyInfinite(X_10)))). % 3.54/1.89 tff(c_207, plain, (![X_6, Z_8]: (conceivedThru(X_6, Z_8) | ~mode(X_6)))). % 3.54/1.89 tff(c_82, plain, (![Y_18, X_17]: (Y_18=X_17 | ~existsIn(X_17, Y_18) | exists(X_17)))). % 3.54/1.89 tff(c_58, plain, (![Y_13, X_12]: (~determinedByItselfAlone(Y_13, X_12) | free(X_12) | ~existsOnlyByNecessityOfOwnNature(X_12)))). % 3.54/1.89 tff(c_60, plain, (![Y_13, X_12]: (actionOf(Y_13, X_12) | free(X_12) | ~existsOnlyByNecessityOfOwnNature(X_12)))). % 3.54/1.89 tff(c_34, plain, (![Y_7, X_6]: (~substance(Y_7) | ~modification(X_6, Y_7) | mode(X_6)))). % 3.54/1.89 tff(c_46, plain, (![Y_11, X_10]: (expressesInfiniteEssentiality(Y_11) | ~attributeOf(Y_11, X_10) | ~absolutelyInfinite(X_10)))). % 3.54/1.89 tff(c_2, plain, (![X_1]: (selfCaused(X_1) | ~natureConcOnlyByExistence(X_1) | ~essenceInvExistence(X_1)))). % 3.54/1.89 tff(c_14, plain, (![X_4]: (substance(X_4) | ~conceivedThruItself(X_4) | ~inItself(X_4)))). % 3.54/1.89 tff(c_177, plain, (![X_14]: (~necessary(X_14)))). % 3.54/1.89 tff(c_102, plain, (![Y_26, X_25]: (~canBeUnderstoodInTermsOf(Y_26, X_25) | ~haveNothingInCommon(X_25, Y_26)))). % 3.54/1.89 tff(c_36, plain, (![X_9]: (god(X_9) | ~absolutelyInfinite(X_9) | ~being(X_9)))). % 3.54/1.89 tff(c_104, plain, (![X_25, Y_26]: (~canBeUnderstoodInTermsOf(X_25, Y_26) | ~haveNothingInCommon(X_25, Y_26)))). % 3.54/1.89 tff(c_100, plain, (![X_25, Y_26]: (~conceptionInvolves(X_25, Y_26) | ~haveNothingInCommon(X_25, Y_26)))). % 3.54/1.89 tff(c_98, plain, (![Y_26, X_25]: (~conceptionInvolves(Y_26, X_25) | ~haveNothingInCommon(X_25, Y_26)))). % 3.54/1.89 tff(c_84, plain, (![X_17]: (~existsIn(X_17, X_17) | exists(X_17)))). % 3.54/1.89 tff(c_92, plain, (![Y_22, X_21]: (effectNecessarilyFollowsFrom(Y_22, X_21) | ~definiteCause(X_21)))). % 3.54/1.89 tff(c_12, plain, (![X_2, Y_3]: (canBeLimitedBy(X_2, Y_3) | ~finiteAfterItsKind(X_2)))). % 3.54/1.89 tff(c_78, plain, (![Y_18]: (existsIn(Y_18, Y_18) | ~exists(Y_18)))). % 3.54/1.89 tff(c_94, plain, (![X_23, Y_24]: (knowledgeOfACause(X_23) | ~knowledgeOfEffect(X_23, Y_24)))). % 3.54/1.89 tff(c_10, plain, (![X_2, Y_3]: (sameKind(X_2, Y_3) | ~finiteAfterItsKind(X_2)))). % 3.54/1.89 tff(c_108, plain, (![X_27, Y_28]: (correspondWith(X_27, Y_28) | ~trueIdea(X_27)))). % 3.54/1.89 tff(c_137, plain, (![X_10]: (conceivedThruItself(X_10) | ~absolutelyInfinite(X_10)))). % 3.54/1.89 tff(c_132, plain, (![X_10]: (inItself(X_10) | ~absolutelyInfinite(X_10)))). % 3.54/1.89 tff(c_96, plain, (![X_23, Y_24]: (knowledgeOfEffect(X_23, Y_24) | ~knowledgeOfACause(X_23)))). % 3.54/1.89 tff(c_76, plain, (![X_16]: (eternity(X_16) | ~existConcFollowFromDefEternal(X_16)))). % 3.54/1.89 tff(c_16, plain, (![X_4]: (conceivedThruItself(X_4) | ~substance(X_4)))). % 3.54/1.89 tff(c_18, plain, (![X_4]: (inItself(X_4) | ~substance(X_4)))). % 3.54/1.89 tff(c_20, plain, (![X_5]: (intPercAsConstEssSub(X_5) | ~attribute(X_5)))). % 3.54/1.89 tff(c_22, plain, (![X_5]: (attribute(X_5) | ~intPercAsConstEssSub(X_5)))). % 3.54/1.89 tff(c_56, plain, (![X_12]: (existsOnlyByNecessityOfOwnNature(X_12) | ~free(X_12)))). % 3.54/1.89 tff(c_6, plain, (![X_1]: (essenceInvExistence(X_1) | ~selfCaused(X_1)))). % 3.54/1.89 tff(c_4, plain, (![X_1]: (natureConcOnlyByExistence(X_1) | ~selfCaused(X_1)))). % 3.54/1.89 tff(c_44, plain, (![X_10]: (substance(X_10) | ~absolutelyInfinite(X_10)))). % 3.54/1.89 tff(c_38, plain, (![X_9]: (absolutelyInfinite(X_9) | ~god(X_9)))). % 3.54/1.89 tff(c_40, plain, (![X_9]: (being(X_9) | ~god(X_9)))). % 3.54/1.89 tff(c_42, plain, (![X_10]: (constInInfAttributes(X_10) | ~absolutelyInfinite(X_10)))). % 3.54/1.89 tff(c_74, plain, (![X_16]: (existConcFollowFromDefEternal(X_16) | ~eternity(X_16)))). % 3.54/1.89 tff(c_110, plain, (![X_29]: (~essenceInvExistence(X_29) | ~canBeConceivedAsNonExisting(X_29)))). % 3.54/1.89 tff(c_86, plain, (![Y_20]: (conceivedThru(Y_20, Y_20)))). % 3.54/1.89 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.54/1.89 %------------------------------------------------------------------------------