%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PHI042+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 : n006.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:29 PM UTC 2025
% Result : CounterSatisfiable 3.86s 1.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : PHI042+1 : TPTP v9.0.0. Released v7.4.0.
% 0.12/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.12/0.34 % Computer : n006.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 16:31:07 EDT 2025
% 0.12/0.34 % CPUTime :
% 3.86/1.97
% 3.86/1.97 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.86/1.97
% 3.86/1.97 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.86/1.98 %$ 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 > hasEssence > god > free > finiteAfterItsKind > expressesInfiniteEssentiality > expressesEternalEssentiality > existsOnlyByNecessityOfOwnNature > exists > existConcFollowFromDefEternal > eternity > essenceInvExistence > definiteCause > constInInfAttributes > conceivedThruItself > canBeConceivedAsNonExisting > being > attribute > absolutelyInfinite > #nlpp > #skF_2 > #skF_1
% 3.86/1.98
% 3.86/1.98 %Foreground sorts:
% 3.86/1.98
% 3.86/1.98
% 3.86/1.98 %Background operators:
% 3.86/1.98
% 3.86/1.98
% 3.86/1.98 %Foreground operators:
% 3.86/1.98 tff(being, type, being: $i > $o).
% 3.86/1.98 tff(externalTo, type, externalTo: ($i * $i) > $o).
% 3.86/1.98 tff(isMethodAction, type, isMethodAction: $i > $o).
% 3.86/1.98 tff(intPercAsConstEssSub, type, intPercAsConstEssSub: $i > $o).
% 3.86/1.98 tff(necessary, type, necessary: $i > $o).
% 3.86/1.98 tff(attributeOf, type, attributeOf: ($i * $i) > $o).
% 3.86/1.98 tff(finiteAfterItsKind, type, finiteAfterItsKind: $i > $o).
% 3.86/1.98 tff(existsIn, type, existsIn: ($i * $i) > $o).
% 3.86/1.98 tff(definiteCause, type, definiteCause: $i > $o).
% 3.86/1.98 tff(trueIdea, type, trueIdea: $i > $o).
% 3.86/1.98 tff(substance, type, substance: $i > $o).
% 3.86/1.98 tff(free, type, free: $i > $o).
% 3.86/1.98 tff(knowledgeOfACause, type, knowledgeOfACause: $i > $o).
% 3.86/1.98 tff(attribute, type, attribute: $i > $o).
% 3.86/1.98 tff(canBeUnderstoodInTermsOf, type, canBeUnderstoodInTermsOf: ($i * $i) > $o).
% 3.86/1.98 tff(god, type, god: $i > $o).
% 3.86/1.98 tff(existsOnlyByNecessityOfOwnNature, type, existsOnlyByNecessityOfOwnNature: $i > $o).
% 3.86/1.98 tff(correspondWith, type, correspondWith: ($i * $i) > $o).
% 3.86/1.98 tff(essenceInvExistence, type, essenceInvExistence: $i > $o).
% 3.86/1.98 tff(ideateOf, type, ideateOf: ($i * $i) > $o).
% 3.86/1.98 tff(mode, type, mode: $i > $o).
% 3.86/1.98 tff('#skF_2', type, '#skF_2': $i).
% 3.86/1.98 tff(haveNothingInCommon, type, haveNothingInCommon: ($i * $i) > $o).
% 3.86/1.98 tff('#skF_1', type, '#skF_1': $i).
% 3.86/1.98 tff(effectNecessarilyFollowsFrom, type, effectNecessarilyFollowsFrom: ($i * $i) > $o).
% 3.86/1.98 tff(actionOf, type, actionOf: ($i * $i) > $o).
% 3.86/1.98 tff(isMethodExistence, type, isMethodExistence: $i > $o).
% 3.86/1.98 tff(determinedByDefiniteMethod, type, determinedByDefiniteMethod: ($i * $i) > $o).
% 3.86/1.98 tff(expressesInfiniteEssentiality, type, expressesInfiniteEssentiality: $i > $o).
% 3.86/1.98 tff(modification, type, modification: ($i * $i) > $o).
% 3.86/1.98 tff(eternity, type, eternity: $i > $o).
% 3.86/1.98 tff(determinedByFixedMethod, type, determinedByFixedMethod: ($i * $i) > $o).
% 3.86/1.98 tff(selfCaused, type, selfCaused: $i > $o).
% 3.86/1.98 tff(hasEssence, type, hasEssence: $i > $o).
% 3.86/1.98 tff(determinedByItselfAlone, type, determinedByItselfAlone: ($i * $i) > $o).
% 3.86/1.98 tff(inItself, type, inItself: $i > $o).
% 3.86/1.98 tff(objectOf, type, objectOf: ($i * $i) > $o).
% 3.86/1.98 tff(canBeConceivedAsNonExisting, type, canBeConceivedAsNonExisting: $i > $o).
% 3.86/1.98 tff(conceivedThru, type, conceivedThru: ($i * $i) > $o).
% 3.86/1.98 tff(absolutelyInfinite, type, absolutelyInfinite: $i > $o).
% 3.86/1.98 tff(conceivedThruItself, type, conceivedThruItself: $i > $o).
% 3.86/1.98 tff(canBeLimitedBy, type, canBeLimitedBy: ($i * $i) > $o).
% 3.86/1.98 tff(conceptionInvolves, type, conceptionInvolves: ($i * $i) > $o).
% 3.86/1.98 tff(natureConcOnlyByExistence, type, natureConcOnlyByExistence: $i > $o).
% 3.86/1.98 tff(knowledgeOfEffect, type, knowledgeOfEffect: ($i * $i) > $o).
% 3.86/1.98 tff(exists, type, exists: $i > $o).
% 3.86/1.98 tff(constInInfAttributes, type, constInInfAttributes: $i > $o).
% 3.86/1.98 tff(existConcFollowFromDefEternal, type, existConcFollowFromDefEternal: $i > $o).
% 3.86/1.98 tff(expressesEternalEssentiality, type, expressesEternalEssentiality: $i > $o).
% 3.86/1.98 tff(sameKind, type, sameKind: ($i * $i) > $o).
% 3.86/1.98
% 3.86/1.98 %Saturated clause set:
% 3.86/1.98 tff(c_314, plain, (![Y_28, X_27]: (~isMethodAction(Y_28) | ~determinedByDefiniteMethod(X_27, Y_28) | ~determinedByFixedMethod(X_27, Y_28) | ~externalTo(Y_28, X_27)))).
% 3.86/1.98 tff(c_312, plain, (![Y_28, X_27]: (~isMethodExistence(Y_28) | ~determinedByDefiniteMethod(X_27, Y_28) | ~determinedByFixedMethod(X_27, Y_28) | ~externalTo(Y_28, X_27)))).
% 3.86/1.98 tff(c_310, plain, (![Y_24]: (~expressesInfiniteEssentiality(Y_24) | ~expressesEternalEssentiality(Y_24)))).
% 3.86/1.98 tff(c_86, plain, (![Y_24, X_23]: (attributeOf(Y_24, X_23) | absolutelyInfinite(X_23) | ~constInInfAttributes(X_23) | ~substance(X_23)))).
% 3.86/1.98 tff(c_88, plain, (![Y_26, X_25]: (determinedByItselfAlone(Y_26, X_25) | ~actionOf(Y_26, X_25) | ~free(X_25)))).
% 3.86/1.98 tff(c_30, plain, (![Y_12, X_11]: (objectOf(Y_12, X_11) | ideateOf(Y_12, X_11) | ~trueIdea(X_11)))).
% 3.86/1.98 tff(c_289, plain, (![Y_2]: (mode(Y_2) | ~exists(Y_2)))).
% 3.86/1.98 tff(c_66, plain, (![X_19, Z_21]: (~conceivedThru(X_19, Z_21) | ~existsIn(X_19, Z_21) | mode(X_19)))).
% 3.86/1.98 tff(c_42, plain, (![X_15, Y_16]: (finiteAfterItsKind(X_15) | ~sameKind(X_15, Y_16) | ~canBeLimitedBy(X_15, Y_16)))).
% 3.86/1.98 tff(c_94, plain, (![Y_26, X_25]: (actionOf(Y_26, X_25) | free(X_25) | ~existsOnlyByNecessityOfOwnNature(X_25)))).
% 3.86/1.98 tff(c_82, plain, (![Y_24, X_23]: (expressesEternalEssentiality(Y_24) | ~attributeOf(Y_24, X_23) | ~absolutelyInfinite(X_23)))).
% 3.86/1.98 tff(c_80, plain, (![Y_24, X_23]: (expressesInfiniteEssentiality(Y_24) | ~attributeOf(Y_24, X_23) | ~absolutelyInfinite(X_23)))).
% 3.86/1.98 tff(c_269, plain, (![X_19, Z_21]: (conceivedThru(X_19, Z_21) | ~mode(X_19)))).
% 3.86/1.98 tff(c_6, plain, (![Y_2, X_1]: (Y_2=X_1 | ~existsIn(X_1, Y_2) | exists(X_1)))).
% 3.86/1.99 tff(c_92, plain, (![Y_26, X_25]: (~determinedByItselfAlone(Y_26, X_25) | free(X_25) | ~existsOnlyByNecessityOfOwnNature(X_25)))).
% 3.86/1.99 tff(c_256, plain, (![Z_94]: (exists(Z_94) | ~mode(Z_94)))).
% 3.86/1.99 tff(c_250, plain, (![X_19, Z_21]: (existsIn(X_19, Z_21) | ~mode(X_19)))).
% 3.86/1.99 tff(c_68, plain, (![Y_20, X_19]: (~substance(Y_20) | ~modification(X_19, Y_20) | mode(X_19)))).
% 3.86/1.99 tff(c_213, plain, (![X_76]: (being(X_76) | ~conceivedThruItself(X_76) | ~inItself(X_76)))).
% 3.86/1.99 tff(c_229, plain, (![X_31]: (exists(X_31) | ~essenceInvExistence(X_31) | ~being(X_31)))).
% 3.86/1.99 tff(c_26, plain, (![Y_10, X_9]: (~canBeUnderstoodInTermsOf(Y_10, X_9) | ~haveNothingInCommon(X_9, Y_10)))).
% 3.86/1.99 tff(c_24, plain, (![X_9, Y_10]: (~conceptionInvolves(X_9, Y_10) | ~haveNothingInCommon(X_9, Y_10)))).
% 3.86/1.99 tff(c_70, plain, (![X_22]: (god(X_22) | ~absolutelyInfinite(X_22) | ~being(X_22)))).
% 3.86/1.99 tff(c_22, plain, (![Y_10, X_9]: (~conceptionInvolves(Y_10, X_9) | ~haveNothingInCommon(X_9, Y_10)))).
% 3.86/1.99 tff(c_28, plain, (![X_9, Y_10]: (~canBeUnderstoodInTermsOf(X_9, Y_10) | ~haveNothingInCommon(X_9, Y_10)))).
% 3.86/1.99 tff(c_122, plain, (![X_32]: (exists(X_32) | ~hasEssence(X_32) | ~essenceInvExistence(X_32)))).
% 3.86/1.99 tff(c_36, plain, (![X_14]: (selfCaused(X_14) | ~natureConcOnlyByExistence(X_14) | ~essenceInvExistence(X_14)))).
% 3.86/1.99 tff(c_214, plain, (![X_27]: (~necessary(X_27)))).
% 3.86/1.99 tff(c_48, plain, (![X_17]: (substance(X_17) | ~conceivedThruItself(X_17) | ~inItself(X_17)))).
% 3.86/1.99 tff(c_8, plain, (![X_1]: (~existsIn(X_1, X_1) | exists(X_1)))).
% 3.86/1.99 tff(c_2, plain, (![Y_2]: (existsIn(Y_2, Y_2) | ~exists(Y_2)))).
% 3.86/1.99 tff(c_44, plain, (![X_15, Y_16]: (sameKind(X_15, Y_16) | ~finiteAfterItsKind(X_15)))).
% 3.86/1.99 tff(c_18, plain, (![X_7, Y_8]: (knowledgeOfACause(X_7) | ~knowledgeOfEffect(X_7, Y_8)))).
% 3.86/1.99 tff(c_46, plain, (![X_15, Y_16]: (canBeLimitedBy(X_15, Y_16) | ~finiteAfterItsKind(X_15)))).
% 3.86/1.99 tff(c_20, plain, (![X_7, Y_8]: (knowledgeOfEffect(X_7, Y_8) | ~knowledgeOfACause(X_7)))).
% 3.86/1.99 tff(c_182, plain, (![X_58]: (~canBeConceivedAsNonExisting(X_58) | ~absolutelyInfinite(X_58)))).
% 3.86/1.99 tff(c_176, plain, (![X_23]: (essenceInvExistence(X_23) | ~absolutelyInfinite(X_23)))).
% 3.86/1.99 tff(c_32, plain, (![X_11, Y_12]: (correspondWith(X_11, Y_12) | ~trueIdea(X_11)))).
% 3.86/1.99 tff(c_165, plain, (![X_48]: (essenceInvExistence(X_48) | ~inItself(X_48)))).
% 3.86/1.99 tff(c_166, plain, (![X_48]: (natureConcOnlyByExistence(X_48) | ~inItself(X_48)))).
% 3.86/1.99 tff(c_147, plain, (![X_41]: (being(X_41) | ~absolutelyInfinite(X_41)))).
% 3.86/1.99 tff(c_16, plain, (![Y_6, X_5]: (effectNecessarilyFollowsFrom(Y_6, X_5) | ~definiteCause(X_5)))).
% 3.86/1.99 tff(c_154, plain, (![X_23]: (inItself(X_23) | ~absolutelyInfinite(X_23)))).
% 3.86/1.99 tff(c_146, plain, (![X_41]: (conceivedThruItself(X_41) | ~absolutelyInfinite(X_41)))).
% 3.86/1.99 tff(c_118, plain, (![X_30]: (selfCaused(X_30) | ~inItself(X_30)))).
% 3.86/1.99 tff(c_90, plain, (![X_25]: (existsOnlyByNecessityOfOwnNature(X_25) | ~free(X_25)))).
% 3.86/1.99 tff(c_34, plain, (![X_13]: (~essenceInvExistence(X_13) | ~canBeConceivedAsNonExisting(X_13)))).
% 3.86/1.99 tff(c_40, plain, (![X_14]: (essenceInvExistence(X_14) | ~selfCaused(X_14)))).
% 3.86/1.99 tff(c_52, plain, (![X_17]: (inItself(X_17) | ~substance(X_17)))).
% 3.86/1.99 tff(c_76, plain, (![X_23]: (constInInfAttributes(X_23) | ~absolutelyInfinite(X_23)))).
% 3.86/1.99 tff(c_74, plain, (![X_22]: (being(X_22) | ~god(X_22)))).
% 3.86/1.99 tff(c_78, plain, (![X_23]: (substance(X_23) | ~absolutelyInfinite(X_23)))).
% 3.86/1.99 tff(c_38, plain, (![X_14]: (natureConcOnlyByExistence(X_14) | ~selfCaused(X_14)))).
% 3.86/1.99 tff(c_137, plain, (eternity('#skF_2'))).
% 3.86/1.99 tff(c_50, plain, (![X_17]: (conceivedThruItself(X_17) | ~substance(X_17)))).
% 3.86/1.99 tff(c_135, plain, (~eternity('#skF_1'))).
% 3.86/1.99 tff(c_72, plain, (![X_22]: (absolutelyInfinite(X_22) | ~god(X_22)))).
% 3.86/1.99 tff(c_120, plain, (![X_31]: (hasEssence(X_31) | ~being(X_31)))).
% 3.86/1.99 tff(c_54, plain, (![X_18]: (intPercAsConstEssSub(X_18) | ~attribute(X_18)))).
% 3.86/1.99 tff(c_56, plain, (![X_18]: (attribute(X_18) | ~intPercAsConstEssSub(X_18)))).
% 3.86/1.99 tff(c_126, plain, (~existConcFollowFromDefEternal('#skF_2'))).
% 3.86/1.99 tff(c_116, plain, (![X_29]: (being(X_29) | ~substance(X_29)))).
% 3.86/1.99 tff(c_10, plain, (![Y_4]: (conceivedThru(Y_4, Y_4)))).
% 3.86/1.99 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.86/1.99
%------------------------------------------------------------------------------