%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PHI028+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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.10s 0.45s
% Output : FiniteModel 0.10s
% 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.02 % Problem : PHI028+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n016.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:12:18 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.45 % (3041105)Will run a generic schedule for satisfiability detection.
% 0.10/0.45 % (3041110)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2081635851_2999 on theBenchmark for (2999ds/0Mi)
% 0.10/0.45 % TRYING [1]
% 0.10/0.45 % Finite Model Found!
% 0.10/0.45 % SZS status CounterSatisfiable for theBenchmark
% 0.10/0.45 % (3041110) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3041105-3041110"...
% 0.10/0.45 % (3041110)...printing done.
% 0.10/0.45 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.10/0.46 % (3041110)------------------------------
% 0.10/0.46 % (3041110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.46 % (3041110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.46 % (3041110)CaDiCaL version: 2.1.3
% 0.10/0.46 % (3041110)Termination reason: Satisfiable
% 0.10/0.46 % (3041110)Time elapsed: 0.001 s
% 0.10/0.46 % (3041110)Peak memory usage: 12 MB
% 0.10/0.46 % (3041110)Instructions burned: 2 (million)
% 0.10/0.46 % (3041105)Success in time 0.032 s
% 0.10/0.46 % Vampire exiting
%------------------------------------------------------------------------------