%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : PHI024+1 : TPTP v9.0.0. Released v7.4.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % 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 : Sat Jun 21 05:22:46 AM UTC 2025 % Result : CounterSatisfiable 0.11s 0.39s % Output : Model 0.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : PHI024+1 : TPTP v9.0.0. Released v7.4.0. % 0.10/0.12 % Command : run_E %s %d THM % 0.11/0.33 % Computer : n016.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.34 % CPULimit : 300 % 0.11/0.34 % WCLimit : 300 % 0.11/0.34 % DateTime : Fri Jun 20 02:19:02 EDT 2025 % 0.11/0.34 % CPUTime : % 0.11/0.39 % SZS status CounterSatisfiable % 0.11/0.39 % SZS output start Model % 0.11/0.39 tff(existsOnlyByNecessityOfOwnNature_type, type, ( % 0.11/0.39 existsOnlyByNecessityOfOwnNature: $i > $o)). % 0.11/0.39 tff(determinedByDefiniteMethod_type, type, ( % 0.11/0.39 determinedByDefiniteMethod: ( $i * $i ) > $o)). % 0.11/0.39 tff(absolutelyInfinite_type, type, ( % 0.11/0.39 absolutelyInfinite: $i > $o)). % 0.11/0.39 tff(existsIn_type, type, ( % 0.11/0.39 existsIn: ( $i * $i ) > $o)). % 0.11/0.39 tff(sameKind_type, type, ( % 0.11/0.39 sameKind: ( $i * $i ) > $o)). % 0.11/0.39 tff(free_type, type, ( % 0.11/0.39 free: $i > $o)). % 0.11/0.39 tff(necessary_type, type, ( % 0.11/0.39 necessary: $i > $o)). % 0.11/0.39 tff(isMethodAction_type, type, ( % 0.11/0.39 isMethodAction: $i > $o)). % 0.11/0.39 tff(substance_type, type, ( % 0.11/0.39 substance: $i > $o)). % 0.11/0.39 tff(expressesInfiniteEssentiality_type, type, ( % 0.11/0.39 expressesInfiniteEssentiality: $i > $o)). % 0.11/0.39 tff(ideateOf_type, type, ( % 0.11/0.39 ideateOf: ( $i * $i ) > $o)). % 0.11/0.39 tff(attributeOf_type, type, ( % 0.11/0.39 attributeOf: ( $i * $i ) > $o)). % 0.11/0.39 tff(constInInfAttributes_type, type, ( % 0.11/0.39 constInInfAttributes: $i > $o)). % 0.11/0.39 tff(isMethodExistence_type, type, ( % 0.11/0.39 isMethodExistence: $i > $o)). % 0.11/0.39 tff(knowledgeOfACause_type, type, ( % 0.11/0.39 knowledgeOfACause: $i > $o)). % 0.11/0.39 tff(canBeConceivedAsNonExisting_type, type, ( % 0.11/0.39 canBeConceivedAsNonExisting: $i > $o)). % 0.11/0.39 tff(selfCaused_type, type, ( % 0.11/0.39 selfCaused: $i > $o)). % 0.11/0.39 tff(expressesEternalEssentiality_type, type, ( % 0.11/0.39 expressesEternalEssentiality: $i > $o)). % 0.11/0.39 tff(natureConcOnlyByExistence_type, type, ( % 0.11/0.39 natureConcOnlyByExistence: $i > $o)). % 0.11/0.39 tff(correspondWith_type, type, ( % 0.11/0.39 correspondWith: ( $i * $i ) > $o)). % 0.11/0.39 tff(god_type, type, ( % 0.11/0.39 god: $i > $o)). % 0.11/0.39 tff(tptp_fun__i_val_0_type, type, ( % 0.11/0.39 tptp_fun__i_val_0: $i)). % 0.11/0.39 tff(being_type, type, ( % 0.11/0.39 being: $i > $o)). % 0.11/0.39 tff(conceivedThruItself_type, type, ( % 0.11/0.39 conceivedThruItself: $i > $o)). % 0.11/0.39 tff(exists_type, type, ( % 0.11/0.39 exists: $i > $o)). % 0.11/0.39 tff(conceivedThru_type, type, ( % 0.11/0.39 conceivedThru: ( $i * $i ) > $o)). % 0.11/0.39 tff(canBeLimitedBy_type, type, ( % 0.11/0.39 canBeLimitedBy: ( $i * $i ) > $o)). % 0.11/0.39 tff(finiteAfterItsKind_type, type, ( % 0.11/0.39 finiteAfterItsKind: $i > $o)). % 0.11/0.39 tff(existConcFollowFromDefEternal_type, type, ( % 0.11/0.39 existConcFollowFromDefEternal: $i > $o)). % 0.11/0.39 tff(determinedByFixedMethod_type, type, ( % 0.11/0.39 determinedByFixedMethod: ( $i * $i ) > $o)). % 0.11/0.39 tff(effectNecessarilyFollowsFrom_type, type, ( % 0.11/0.39 effectNecessarilyFollowsFrom: ( $i * $i ) > $o)). % 0.11/0.39 tff(actionOf_type, type, ( % 0.11/0.39 actionOf: ( $i * $i ) > $o)). % 0.11/0.39 tff(modification_type, type, ( % 0.11/0.39 modification: ( $i * $i ) > $o)). % 0.11/0.39 tff(externalTo_type, type, ( % 0.11/0.39 externalTo: ( $i * $i ) > $o)). % 0.11/0.39 tff(haveNothingInCommon_type, type, ( % 0.11/0.39 haveNothingInCommon: ( $i * $i ) > $o)). % 0.11/0.39 tff(determinedByItselfAlone_type, type, ( % 0.11/0.39 determinedByItselfAlone: ( $i * $i ) > $o)). % 0.11/0.39 tff(eternity_type, type, ( % 0.11/0.39 eternity: $i > $o)). % 0.11/0.39 tff(inItself_type, type, ( % 0.11/0.39 inItself: $i > $o)). % 0.11/0.39 tff(canBeUnderstoodInTermsOf_type, type, ( % 0.11/0.39 canBeUnderstoodInTermsOf: ( $i * $i ) > $o)). % 0.11/0.39 tff(mode_type, type, ( % 0.11/0.39 mode: $i > $o)). % 0.11/0.39 tff(trueIdea_type, type, ( % 0.11/0.39 trueIdea: $i > $o)). % 0.11/0.39 tff(objectOf_type, type, ( % 0.11/0.39 objectOf: ( $i * $i ) > $o)). % 0.11/0.39 tff(definiteCause_type, type, ( % 0.11/0.39 definiteCause: $i > $o)). % 0.11/0.39 tff(intPercAsConstEssSub_type, type, ( % 0.11/0.39 intPercAsConstEssSub: $i > $o)). % 0.11/0.39 tff(essenceInvExistence_type, type, ( % 0.11/0.39 essenceInvExistence: $i > $o)). % 0.11/0.39 tff(attribute_type, type, ( % 0.11/0.39 attribute: $i > $o)). % 0.11/0.39 tff(knowledgeOfEffect_type, type, ( % 0.11/0.39 knowledgeOfEffect: ( $i * $i ) > $o)). % 0.11/0.39 tff(conceptionInvolves_type, type, ( % 0.11/0.39 conceptionInvolves: ( $i * $i ) > $o)). % 0.11/0.39 tff(hasEssence_type, type, ( % 0.11/0.39 hasEssence: $i > $o)). % 0.11/0.39 tff(formula1, axiom, % 0.11/0.39 ![X0: $i] : (existsOnlyByNecessityOfOwnNature(X0) <=> $true)). % 0.11/0.39 tff(formula2, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (determinedByDefiniteMethod(X0, X1) <=> $true)). % 0.11/0.39 tff(formula3, axiom, % 0.11/0.39 ![X0: $i] : (absolutelyInfinite(X0) <=> $false)). % 0.11/0.39 tff(formula4, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (existsIn(X0, X1) <=> $false)). % 0.11/0.39 tff(formula5, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (sameKind(X0, X1) <=> $false)). % 0.11/0.39 tff(formula6, axiom, % 0.11/0.39 ![X0: $i] : (free(X0) <=> $false)). % 0.11/0.39 tff(formula7, axiom, % 0.11/0.39 ![X0: $i] : (necessary(X0) <=> $true)). % 0.11/0.39 tff(formula8, axiom, % 0.11/0.39 ![X0: $i] : (isMethodAction(X0) <=> $true)). % 0.11/0.39 tff(formula9, axiom, % 0.11/0.39 ![X0: $i] : (substance(X0) <=> $true)). % 0.11/0.39 tff(formula10, axiom, % 0.11/0.39 ![X0: $i] : (expressesInfiniteEssentiality(X0) <=> $true)). % 0.11/0.39 tff(formula11, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (ideateOf(X0, X1) <=> $true)). % 0.11/0.39 tff(formula12, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (attributeOf(X0, X1) <=> $true)). % 0.11/0.39 tff(formula13, axiom, % 0.11/0.39 ![X0: $i] : (constInInfAttributes(X0) <=> $false)). % 0.11/0.39 tff(formula14, axiom, % 0.11/0.39 ![X0: $i] : (isMethodExistence(X0) <=> $true)). % 0.11/0.39 tff(formula15, axiom, % 0.11/0.39 ![X0: $i] : (knowledgeOfACause(X0) <=> $true)). % 0.11/0.39 tff(formula16, axiom, % 0.11/0.39 ![X0: $i] : (canBeConceivedAsNonExisting(X0) <=> $false)). % 0.11/0.39 tff(formula17, axiom, % 0.11/0.39 ![X0: $i] : (selfCaused(X0) <=> $true)). % 0.11/0.39 tff(formula18, axiom, % 0.11/0.39 ![X0: $i] : (expressesEternalEssentiality(X0) <=> $true)). % 0.11/0.39 tff(formula19, axiom, % 0.11/0.39 ![X0: $i] : (natureConcOnlyByExistence(X0) <=> $true)). % 0.11/0.39 tff(formula20, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (correspondWith(X0, X1) <=> $true)). % 0.11/0.39 tff(formula21, axiom, % 0.11/0.39 god($i!val!0) <=> $false). % 0.11/0.39 tff(formula22, axiom, % 0.11/0.39 ![X0: $i] : ((~(($i!val!0 = X0))) => (god(X0) <=> (~((~being(X0)) | (~absolutelyInfinite(X0))))))). % 0.11/0.39 tff(formula23, axiom, % 0.11/0.39 ![X0: $i] : (conceivedThruItself(X0) <=> $true)). % 0.11/0.39 tff(formula24, axiom, % 0.11/0.39 ![X0: $i] : (exists(X0) <=> $false)). % 0.11/0.39 tff(formula25, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (conceivedThru(X0, X1) <=> $true)). % 0.11/0.39 tff(formula26, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (canBeLimitedBy(X0, X1) <=> $false)). % 0.11/0.39 tff(formula27, axiom, % 0.11/0.39 ![X0: $i] : (finiteAfterItsKind(X0) <=> $false)). % 0.11/0.39 tff(formula28, axiom, % 0.11/0.39 ![X0: $i] : (existConcFollowFromDefEternal(X0) <=> $false)). % 0.11/0.39 tff(formula29, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (determinedByFixedMethod(X0, X1) <=> $true)). % 0.11/0.39 tff(formula30, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (effectNecessarilyFollowsFrom(X0, X1) <=> $true)). % 0.11/0.39 tff(formula31, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (actionOf(X0, X1) <=> $true)). % 0.11/0.39 tff(formula32, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (modification(X0, X1) <=> $false)). % 0.11/0.39 tff(formula33, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (externalTo(X0, X1) <=> $true)). % 0.11/0.39 tff(formula34, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (haveNothingInCommon(X0, X1) <=> $false)). % 0.11/0.39 tff(formula35, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (determinedByItselfAlone(X0, X1) <=> $false)). % 0.11/0.39 tff(formula36, axiom, % 0.11/0.39 ![X0: $i] : (eternity(X0) <=> existConcFollowFromDefEternal(X0))). % 0.11/0.39 tff(formula37, axiom, % 0.11/0.39 ![X0: $i] : (inItself(X0) <=> $true)). % 0.11/0.39 tff(formula38, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (canBeUnderstoodInTermsOf(X0, X1) <=> $false)). % 0.11/0.39 tff(formula39, axiom, % 0.11/0.39 ![X0: $i] : (mode(X0) <=> $false)). % 0.11/0.39 tff(formula40, axiom, % 0.11/0.39 ![X0: $i] : (trueIdea(X0) <=> $false)). % 0.11/0.39 tff(formula41, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (objectOf(X0, X1) <=> $true)). % 0.11/0.39 tff(formula42, axiom, % 0.11/0.39 ![X0: $i] : (being(X0) <=> $false)). % 0.11/0.39 tff(formula43, axiom, % 0.11/0.39 ![X0: $i] : (definiteCause(X0) <=> $true)). % 0.11/0.39 tff(formula44, axiom, % 0.11/0.39 ![X0: $i] : (intPercAsConstEssSub(X0) <=> $false)). % 0.11/0.39 tff(formula45, axiom, % 0.11/0.39 ![X0: $i] : (essenceInvExistence(X0) <=> $true)). % 0.11/0.39 tff(formula46, axiom, % 0.11/0.39 ![X0: $i] : (attribute(X0) <=> intPercAsConstEssSub(X0))). % 0.11/0.39 tff(formula47, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (knowledgeOfEffect(X0, X1) <=> knowledgeOfACause(X1))). % 0.11/0.39 tff(formula48, axiom, % 0.11/0.39 ![X0: $i, X1: $i] : (conceptionInvolves(X0, X1) <=> $true)). % 0.11/0.39 tff(formula49, axiom, % 0.11/0.39 ![X0: $i] : (hasEssence(X0) <=> $false)). % 0.11/0.39 % SZS output end Model % 0.11/0.40 % E exiting %------------------------------------------------------------------------------