%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PHI030+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:27:30 PM UTC 2026
% Result : CounterSatisfiable 0.17s 0.46s
% Output : FiniteModel 0.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] : ( X = 'fmb_$i_1' ) ).
tff(declare_selfCaused,type,
selfCaused: $i > $o ).
tff(predicate_selfCaused,axiom,
selfCaused('fmb_$i_1') ).
tff(declare_essenceInvExistence,type,
essenceInvExistence: $i > $o ).
tff(predicate_essenceInvExistence,axiom,
essenceInvExistence('fmb_$i_1') ).
tff(declare_natureConcOnlyByExistence,type,
natureConcOnlyByExistence: $i > $o ).
tff(predicate_natureConcOnlyByExistence,axiom,
natureConcOnlyByExistence('fmb_$i_1') ).
tff(declare_finiteAfterItsKind,type,
finiteAfterItsKind: $i > $o ).
tff(predicate_finiteAfterItsKind,axiom,
finiteAfterItsKind('fmb_$i_1') ).
tff(declare_canBeLimitedBy,type,
canBeLimitedBy: ( $i * $i ) > $o ).
tff(predicate_canBeLimitedBy,axiom,
canBeLimitedBy('fmb_$i_1','fmb_$i_1') ).
tff(declare_sameKind,type,
sameKind: ( $i * $i ) > $o ).
tff(predicate_sameKind,axiom,
sameKind('fmb_$i_1','fmb_$i_1') ).
tff(declare_substance,type,
substance: $i > $o ).
tff(predicate_substance,axiom,
~ substance('fmb_$i_1') ).
tff(declare_inItself,type,
inItself: $i > $o ).
tff(predicate_inItself,axiom,
~ inItself('fmb_$i_1') ).
tff(declare_conceivedThruItself,type,
conceivedThruItself: $i > $o ).
tff(predicate_conceivedThruItself,axiom,
conceivedThruItself('fmb_$i_1') ).
tff(declare_attribute,type,
attribute: $i > $o ).
tff(predicate_attribute,axiom,
attribute('fmb_$i_1') ).
tff(declare_intPercAsConstEssSub,type,
intPercAsConstEssSub: $i > $o ).
tff(predicate_intPercAsConstEssSub,axiom,
intPercAsConstEssSub('fmb_$i_1') ).
tff(declare_mode,type,
mode: $i > $o ).
tff(predicate_mode,axiom,
~ mode('fmb_$i_1') ).
tff(declare_modification,type,
modification: ( $i * $i ) > $o ).
tff(predicate_modification,axiom,
modification('fmb_$i_1','fmb_$i_1') ).
tff(declare_existsIn,type,
existsIn: ( $i * $i ) > $o ).
tff(predicate_existsIn,axiom,
~ existsIn('fmb_$i_1','fmb_$i_1') ).
tff(declare_conceivedThru,type,
conceivedThru: ( $i * $i ) > $o ).
tff(predicate_conceivedThru,axiom,
conceivedThru('fmb_$i_1','fmb_$i_1') ).
tff(declare_god,type,
god: $i > $o ).
tff(predicate_god,axiom,
~ god('fmb_$i_1') ).
tff(declare_being,type,
being: $i > $o ).
tff(predicate_being,axiom,
~ being('fmb_$i_1') ).
tff(declare_absolutelyInfinite,type,
absolutelyInfinite: $i > $o ).
tff(predicate_absolutelyInfinite,axiom,
~ absolutelyInfinite('fmb_$i_1') ).
tff(declare_constInInfAttributes,type,
constInInfAttributes: $i > $o ).
tff(predicate_constInInfAttributes,axiom,
constInInfAttributes('fmb_$i_1') ).
tff(declare_attributeOf,type,
attributeOf: ( $i * $i ) > $o ).
tff(predicate_attributeOf,axiom,
attributeOf('fmb_$i_1','fmb_$i_1') ).
tff(declare_expressesEternalEssentiality,type,
expressesEternalEssentiality: $i > $o ).
tff(predicate_expressesEternalEssentiality,axiom,
expressesEternalEssentiality('fmb_$i_1') ).
tff(declare_expressesInfiniteEssentiality,type,
expressesInfiniteEssentiality: $i > $o ).
tff(predicate_expressesInfiniteEssentiality,axiom,
expressesInfiniteEssentiality('fmb_$i_1') ).
tff(declare_free,type,
free: $i > $o ).
tff(predicate_free,axiom,
~ free('fmb_$i_1') ).
tff(declare_existsOnlyByNecessityOfOwnNature,type,
existsOnlyByNecessityOfOwnNature: $i > $o ).
tff(predicate_existsOnlyByNecessityOfOwnNature,axiom,
existsOnlyByNecessityOfOwnNature('fmb_$i_1') ).
tff(declare_actionOf,type,
actionOf: ( $i * $i ) > $o ).
tff(predicate_actionOf,axiom,
actionOf('fmb_$i_1','fmb_$i_1') ).
tff(declare_determinedByItselfAlone,type,
determinedByItselfAlone: ( $i * $i ) > $o ).
tff(predicate_determinedByItselfAlone,axiom,
~ determinedByItselfAlone('fmb_$i_1','fmb_$i_1') ).
tff(declare_necessary,type,
necessary: $i > $o ).
tff(predicate_necessary,axiom,
~ necessary('fmb_$i_1') ).
tff(declare_externalTo,type,
externalTo: ( $i * $i ) > $o ).
tff(predicate_externalTo,axiom,
~ externalTo('fmb_$i_1','fmb_$i_1') ).
tff(declare_determinedByFixedMethod,type,
determinedByFixedMethod: ( $i * $i ) > $o ).
tff(predicate_determinedByFixedMethod,axiom,
~ determinedByFixedMethod('fmb_$i_1','fmb_$i_1') ).
tff(declare_determinedByDefiniteMethod,type,
determinedByDefiniteMethod: ( $i * $i ) > $o ).
tff(predicate_determinedByDefiniteMethod,axiom,
determinedByDefiniteMethod('fmb_$i_1','fmb_$i_1') ).
tff(declare_isMethodAction,type,
isMethodAction: $i > $o ).
tff(predicate_isMethodAction,axiom,
~ isMethodAction('fmb_$i_1') ).
tff(declare_isMethodExistence,type,
isMethodExistence: $i > $o ).
tff(predicate_isMethodExistence,axiom,
isMethodExistence('fmb_$i_1') ).
tff(declare_eternity,type,
eternity: $i > $o ).
tff(predicate_eternity,axiom,
eternity('fmb_$i_1') ).
tff(declare_existConcFollowFromDefEternal,type,
existConcFollowFromDefEternal: $i > $o ).
tff(predicate_existConcFollowFromDefEternal,axiom,
existConcFollowFromDefEternal('fmb_$i_1') ).
tff(declare_exists,type,
exists: $i > $o ).
tff(predicate_exists,axiom,
~ exists('fmb_$i_1') ).
tff(declare_definiteCause,type,
definiteCause: $i > $o ).
tff(predicate_definiteCause,axiom,
~ definiteCause('fmb_$i_1') ).
tff(declare_effectNecessarilyFollowsFrom,type,
effectNecessarilyFollowsFrom: ( $i * $i ) > $o ).
tff(predicate_effectNecessarilyFollowsFrom,axiom,
effectNecessarilyFollowsFrom('fmb_$i_1','fmb_$i_1') ).
tff(declare_knowledgeOfEffect,type,
knowledgeOfEffect: ( $i * $i ) > $o ).
tff(predicate_knowledgeOfEffect,axiom,
~ knowledgeOfEffect('fmb_$i_1','fmb_$i_1') ).
tff(declare_knowledgeOfACause,type,
knowledgeOfACause: $i > $o ).
tff(predicate_knowledgeOfACause,axiom,
~ knowledgeOfACause('fmb_$i_1') ).
tff(declare_haveNothingInCommon,type,
haveNothingInCommon: ( $i * $i ) > $o ).
tff(predicate_haveNothingInCommon,axiom,
haveNothingInCommon('fmb_$i_1','fmb_$i_1') ).
tff(declare_canBeUnderstoodInTermsOf,type,
canBeUnderstoodInTermsOf: ( $i * $i ) > $o ).
tff(predicate_canBeUnderstoodInTermsOf,axiom,
canBeUnderstoodInTermsOf('fmb_$i_1','fmb_$i_1') ).
tff(declare_conceptionInvolves,type,
conceptionInvolves: ( $i * $i ) > $o ).
tff(predicate_conceptionInvolves,axiom,
conceptionInvolves('fmb_$i_1','fmb_$i_1') ).
tff(declare_trueIdea,type,
trueIdea: $i > $o ).
tff(predicate_trueIdea,axiom,
trueIdea('fmb_$i_1') ).
tff(declare_correspondWith,type,
correspondWith: ( $i * $i ) > $o ).
tff(predicate_correspondWith,axiom,
correspondWith('fmb_$i_1','fmb_$i_1') ).
tff(declare_ideateOf,type,
ideateOf: ( $i * $i ) > $o ).
tff(predicate_ideateOf,axiom,
ideateOf('fmb_$i_1','fmb_$i_1') ).
tff(declare_objectOf,type,
objectOf: ( $i * $i ) > $o ).
tff(predicate_objectOf,axiom,
objectOf('fmb_$i_1','fmb_$i_1') ).
tff(declare_canBeConceivedAsNonExisting,type,
canBeConceivedAsNonExisting: $i > $o ).
tff(predicate_canBeConceivedAsNonExisting,axiom,
~ canBeConceivedAsNonExisting('fmb_$i_1') ).
tff(declare_hasEssence,type,
hasEssence: $i > $o ).
tff(predicate_hasEssence,axiom,
~ hasEssence('fmb_$i_1') ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI030+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n014.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:07:17 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % (1219009)Will run a generic schedule for satisfiability detection.
% 0.17/0.46 % (1219014)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1358609550_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.46 % TRYING [1]
% 0.17/0.46 % Finite Model Found!
% 0.17/0.46 % SZS status CounterSatisfiable for theBenchmark
% 0.17/0.46 % (1219014) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1219009-1219014"...
% 0.17/0.46 % (1219014)...printing done.
% 0.17/0.46 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.17/0.47 % (1219014)------------------------------
% 0.17/0.47 % (1219014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.47 % (1219014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.47 % (1219014)CaDiCaL version: 2.1.3
% 0.17/0.47 % (1219014)Termination reason: Satisfiable
% 0.17/0.47 % (1219014)Time elapsed: 0.001 s
% 0.17/0.47 % (1219014)Peak memory usage: 11 MB
% 0.17/0.47 % (1219014)Instructions burned: 2 (million)
% 0.17/0.47 % (1219009)Success in time 0.029 s
% 0.17/0.47 % Vampire exiting
%------------------------------------------------------------------------------