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