%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PHI022+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 08:53:58 AM UTC 2026
% Result : Theorem 0.12s 0.41s
% Output : Proof 0.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(self_caused,axiom,
! [X] :
( selfCaused(X)
<=> ( natureConcOnlyByExistence(X)
& essenceInvExistence(X) ) ),
file('PHI002+0.ax',self_caused) ).
fof(finite_after_its_kind,axiom,
! [X,Y] :
( finiteAfterItsKind(X)
<=> ( sameKind(X,Y)
& canBeLimitedBy(X,Y) ) ),
file('PHI002+0.ax',finite_after_its_kind) ).
fof(substance,axiom,
! [X] :
( substance(X)
<=> ( conceivedThruItself(X)
& inItself(X) ) ),
file('PHI002+0.ax',substance) ).
fof(attribute,axiom,
! [X] :
( attribute(X)
<=> intPercAsConstEssSub(X) ),
file('PHI002+0.ax',attribute) ).
fof(mode,axiom,
! [X,Y,Z] :
( mode(X)
<=> ( ( conceivedThru(X,Z)
& existsIn(X,Z) )
| ( substance(Y)
& modification(X,Y) ) ) ),
file('PHI002+0.ax',mode) ).
fof(god,axiom,
! [X] :
( god(X)
<=> ( absolutelyInfinite(X)
& being(X) ) ),
file('PHI002+0.ax',god) ).
fof(absolutely_infinite,axiom,
! [X,Y] :
( absolutelyInfinite(X)
<=> ( ( attributeOf(Y,X)
=> ( expressesInfiniteEssentiality(Y)
& expressesEternalEssentiality(Y) ) )
& constInInfAttributes(X)
& substance(X) ) ),
file('PHI002+0.ax',absolutely_infinite) ).
fof(free,axiom,
! [X,Y] :
( free(X)
<=> ( ( actionOf(Y,X)
=> determinedByItselfAlone(Y,X) )
& existsOnlyByNecessityOfOwnNature(X) ) ),
file('PHI002+0.ax',free) ).
fof(necessary,axiom,
! [X,Y] :
( necessary(X)
<=> ( ( isMethodExistence(Y)
| isMethodAction(Y) )
& determinedByDefiniteMethod(X,Y)
& determinedByFixedMethod(X,Y)
& externalTo(Y,X) ) ),
file('PHI002+0.ax',necessary) ).
fof(eternity,axiom,
! [X] :
( eternity(X)
<=> existConcFollowFromDefEternal(X) ),
file('PHI002+0.ax',eternity) ).
fof(exists,axiom,
! [X,Y] :
( exists(X)
<=> ( ( X != Y
& existsIn(X,Y) )
| existsIn(X,X) ) ),
file('PHI002+1.ax',exists) ).
fof(conceived_through,axiom,
! [X,Y] :
( ~ conceivedThru(X,X)
=> ( X != Y
& conceivedThru(X,Y) ) ),
file('PHI002+1.ax',conceived_through) ).
fof(definite_cause,axiom,
! [X,Y] :
( definiteCause(X)
=> ( ( ~ definiteCause(X)
=> ~ effectNecessarilyFollowsFrom(Y,X) )
& effectNecessarilyFollowsFrom(Y,X) ) ),
file('PHI002+1.ax',definite_cause) ).
fof(knowledge_of_effect,axiom,
! [X,Y] :
( knowledgeOfEffect(X,Y)
<=> knowledgeOfACause(X) ),
file('PHI002+1.ax',knowledge_of_effect) ).
fof(have_nothing_in_common,axiom,
! [X,Y] :
( haveNothingInCommon(X,Y)
=> ( ~ conceptionInvolves(Y,X)
& ~ conceptionInvolves(X,Y)
& ~ canBeUnderstoodInTermsOf(Y,X)
& ~ canBeUnderstoodInTermsOf(X,Y) ) ),
file('PHI002+1.ax',have_nothing_in_common) ).
fof(true_idea,axiom,
! [X,Y] :
( trueIdea(X)
=> ( ( objectOf(Y,X)
| ideateOf(Y,X) )
& correspondWith(X,Y) ) ),
file('PHI002+1.ax',true_idea) ).
fof(can_be_conceived_as_non_existing,axiom,
! [X] :
( canBeConceivedAsNonExisting(X)
=> ~ essenceInvExistence(X) ),
file('PHI002+1.ax',can_be_conceived_as_non_existing) ).
fof(has_substance_being,axiom,
! [X] :
( substance(X)
=> being(X) ),
file('theBenchmark.p',has_substance_being) ).
fof(is_in_itself_is_self_caused,axiom,
! [X] :
( inItself(X)
=> selfCaused(X) ),
file('theBenchmark.p',is_in_itself_is_self_caused) ).
fof(being_has_essense,axiom,
! [X] :
( being(X)
=> hasEssence(X) ),
file('theBenchmark.p',being_has_essense) ).
fof(essence_involves_existence_exists,axiom,
! [X] :
( ( hasEssence(X)
& essenceInvExistence(X) )
=> exists(X) ),
file('theBenchmark.p',essence_involves_existence_exists) ).
fof(has_substance_exists,conjecture,
! [X] :
( substance(X)
=> exists(X) ),
file('theBenchmark.p',has_substance_exists) ).
fof(f_1_1,plain,
! [X] :
( ( selfCaused(X)
| ~ natureConcOnlyByExistence(X)
| ~ essenceInvExistence(X) )
& ( ( natureConcOnlyByExistence(X)
& essenceInvExistence(X) )
| ~ selfCaused(X) ) ),
inference(fof_nnf,[status(thm)],[self_caused]) ).
fof(f_1_2,plain,
! [U_0] :
( ( selfCaused(U_0)
| ~ natureConcOnlyByExistence(U_0)
| ~ essenceInvExistence(U_0) )
& ( ( natureConcOnlyByExistence(U_0)
& essenceInvExistence(U_0) )
| ~ selfCaused(U_0) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_2] :
( selfCaused(U_2)
| ~ natureConcOnlyByExistence(U_2)
| ~ essenceInvExistence(U_2) )
& ! [U_1] :
( ( natureConcOnlyByExistence(U_1)
& essenceInvExistence(U_1) )
| ~ selfCaused(U_1) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( essenceInvExistence(U_1)
| ~ selfCaused(U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_5,plain,
( natureConcOnlyByExistence(U_1)
| ~ selfCaused(U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_6,plain,
( selfCaused(U_2)
| ~ natureConcOnlyByExistence(U_2)
| ~ essenceInvExistence(U_2) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [X,Y] :
( ( finiteAfterItsKind(X)
| ~ sameKind(X,Y)
| ~ canBeLimitedBy(X,Y) )
& ( ( sameKind(X,Y)
& canBeLimitedBy(X,Y) )
| ~ finiteAfterItsKind(X) ) ),
inference(fof_nnf,[status(thm)],[finite_after_its_kind]) ).
fof(f_2_2,plain,
! [U_4,U_3] :
( ( finiteAfterItsKind(U_4)
| ~ sameKind(U_4,U_3)
| ~ canBeLimitedBy(U_4,U_3) )
& ( ( sameKind(U_4,U_3)
& canBeLimitedBy(U_4,U_3) )
| ~ finiteAfterItsKind(U_4) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_10] :
( ! [U_6] :
( ~ sameKind(U_10,U_6)
| ~ canBeLimitedBy(U_10,U_6) )
| finiteAfterItsKind(U_10) )
& ! [U_9] :
( ( ! [U_8] : sameKind(U_9,U_8)
& ! [U_7] : canBeLimitedBy(U_9,U_7) )
| ~ finiteAfterItsKind(U_9) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
cnf(f_2_4,plain,
( canBeLimitedBy(U_9,U_7)
| ~ finiteAfterItsKind(U_9) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( sameKind(U_9,U_8)
| ~ finiteAfterItsKind(U_9) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_6,plain,
( ~ sameKind(U_10,U_6)
| ~ canBeLimitedBy(U_10,U_6)
| finiteAfterItsKind(U_10) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [X] :
( ( substance(X)
| ~ conceivedThruItself(X)
| ~ inItself(X) )
& ( ( conceivedThruItself(X)
& inItself(X) )
| ~ substance(X) ) ),
inference(fof_nnf,[status(thm)],[substance]) ).
fof(f_3_2,plain,
! [U_11] :
( ( substance(U_11)
| ~ conceivedThruItself(U_11)
| ~ inItself(U_11) )
& ( ( conceivedThruItself(U_11)
& inItself(U_11) )
| ~ substance(U_11) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_13] :
( substance(U_13)
| ~ conceivedThruItself(U_13)
| ~ inItself(U_13) )
& ! [U_12] :
( ( conceivedThruItself(U_12)
& inItself(U_12) )
| ~ substance(U_12) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
( inItself(U_12)
| ~ substance(U_12) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_5,plain,
( conceivedThruItself(U_12)
| ~ substance(U_12) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_6,plain,
( substance(U_13)
| ~ conceivedThruItself(U_13)
| ~ inItself(U_13) ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X] :
( ( attribute(X)
| ~ intPercAsConstEssSub(X) )
& ( intPercAsConstEssSub(X)
| ~ attribute(X) ) ),
inference(fof_nnf,[status(thm)],[attribute]) ).
fof(f_4_2,plain,
! [U_14] :
( ( attribute(U_14)
| ~ intPercAsConstEssSub(U_14) )
& ( intPercAsConstEssSub(U_14)
| ~ attribute(U_14) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_16] :
( attribute(U_16)
| ~ intPercAsConstEssSub(U_16) )
& ! [U_15] :
( intPercAsConstEssSub(U_15)
| ~ attribute(U_15) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( intPercAsConstEssSub(U_15)
| ~ attribute(U_15) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_5,plain,
( attribute(U_16)
| ~ intPercAsConstEssSub(U_16) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [X,Y,Z] :
( ( mode(X)
| ( ( ~ conceivedThru(X,Z)
| ~ existsIn(X,Z) )
& ( ~ substance(Y)
| ~ modification(X,Y) ) ) )
& ( ( conceivedThru(X,Z)
& existsIn(X,Z) )
| ( substance(Y)
& modification(X,Y) )
| ~ mode(X) ) ),
inference(fof_nnf,[status(thm)],[mode]) ).
fof(f_5_2,plain,
! [U_19,U_18,U_17] :
( ( mode(U_19)
| ( ( ~ conceivedThru(U_19,U_17)
| ~ existsIn(U_19,U_17) )
& ( ~ substance(U_18)
| ~ modification(U_19,U_18) ) ) )
& ( ( conceivedThru(U_19,U_17)
& existsIn(U_19,U_17) )
| ( substance(U_18)
& modification(U_19,U_18) )
| ~ mode(U_19) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_29] :
( ( ! [U_25] :
( ~ substance(U_25)
| ~ modification(U_29,U_25) )
& ! [U_21] :
( ~ conceivedThru(U_29,U_21)
| ~ existsIn(U_29,U_21) ) )
| mode(U_29) )
& ! [U_28] :
( ( ! [U_27] : substance(U_27)
& ! [U_26] : modification(U_28,U_26) )
| ( ! [U_23] : conceivedThru(U_28,U_23)
& ! [U_22] : existsIn(U_28,U_22) )
| ~ mode(U_28) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
cnf(f_5_4,plain,
( modification(U_28,U_26)
| existsIn(U_28,U_22)
| ~ mode(U_28) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_5,plain,
( substance(U_27)
| existsIn(U_28,U_22)
| ~ mode(U_28) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_6,plain,
( modification(U_28,U_26)
| conceivedThru(U_28,U_23)
| ~ mode(U_28) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_7,plain,
( substance(U_27)
| conceivedThru(U_28,U_23)
| ~ mode(U_28) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_8,plain,
( ~ conceivedThru(U_29,U_21)
| ~ existsIn(U_29,U_21)
| mode(U_29) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_9,plain,
( ~ substance(U_25)
| ~ modification(U_29,U_25)
| mode(U_29) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [X] :
( ( god(X)
| ~ absolutelyInfinite(X)
| ~ being(X) )
& ( ( absolutelyInfinite(X)
& being(X) )
| ~ god(X) ) ),
inference(fof_nnf,[status(thm)],[god]) ).
fof(f_6_2,plain,
! [U_30] :
( ( god(U_30)
| ~ absolutelyInfinite(U_30)
| ~ being(U_30) )
& ( ( absolutelyInfinite(U_30)
& being(U_30) )
| ~ god(U_30) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_32] :
( god(U_32)
| ~ absolutelyInfinite(U_32)
| ~ being(U_32) )
& ! [U_31] :
( ( absolutelyInfinite(U_31)
& being(U_31) )
| ~ god(U_31) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
cnf(f_6_4,plain,
( being(U_31)
| ~ god(U_31) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( absolutelyInfinite(U_31)
| ~ god(U_31) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_6,plain,
( god(U_32)
| ~ absolutelyInfinite(U_32)
| ~ being(U_32) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [X,Y] :
( ( absolutelyInfinite(X)
| ( ( ~ expressesInfiniteEssentiality(Y)
| ~ expressesEternalEssentiality(Y) )
& attributeOf(Y,X) )
| ~ constInInfAttributes(X)
| ~ substance(X) )
& ( ( ( ( expressesInfiniteEssentiality(Y)
& expressesEternalEssentiality(Y) )
| ~ attributeOf(Y,X) )
& constInInfAttributes(X)
& substance(X) )
| ~ absolutelyInfinite(X) ) ),
inference(fof_nnf,[status(thm)],[absolutely_infinite]) ).
fof(f_7_2,plain,
! [U_34,U_33] :
( ( absolutelyInfinite(U_34)
| ( ( ~ expressesInfiniteEssentiality(U_33)
| ~ expressesEternalEssentiality(U_33) )
& attributeOf(U_33,U_34) )
| ~ constInInfAttributes(U_34)
| ~ substance(U_34) )
& ( ( ( ( expressesInfiniteEssentiality(U_33)
& expressesEternalEssentiality(U_33) )
| ~ attributeOf(U_33,U_34) )
& constInInfAttributes(U_34)
& substance(U_34) )
| ~ absolutelyInfinite(U_34) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_40] :
( ( ! [U_38] :
( ~ expressesInfiniteEssentiality(U_38)
| ~ expressesEternalEssentiality(U_38) )
& ! [U_37] : attributeOf(U_37,U_40) )
| ~ constInInfAttributes(U_40)
| ~ substance(U_40)
| absolutelyInfinite(U_40) )
& ! [U_39] :
( ( ! [U_35] :
( ( expressesInfiniteEssentiality(U_35)
& expressesEternalEssentiality(U_35) )
| ~ attributeOf(U_35,U_39) )
& constInInfAttributes(U_39)
& substance(U_39) )
| ~ absolutelyInfinite(U_39) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
cnf(f_7_4,plain,
( substance(U_39)
| ~ absolutelyInfinite(U_39) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_5,plain,
( constInInfAttributes(U_39)
| ~ absolutelyInfinite(U_39) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_6,plain,
( expressesEternalEssentiality(U_35)
| ~ attributeOf(U_35,U_39)
| ~ absolutelyInfinite(U_39) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_7,plain,
( expressesInfiniteEssentiality(U_35)
| ~ attributeOf(U_35,U_39)
| ~ absolutelyInfinite(U_39) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_8,plain,
( attributeOf(U_37,U_40)
| ~ constInInfAttributes(U_40)
| ~ substance(U_40)
| absolutelyInfinite(U_40) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_9,plain,
( ~ expressesInfiniteEssentiality(U_38)
| ~ expressesEternalEssentiality(U_38)
| ~ constInInfAttributes(U_40)
| ~ substance(U_40)
| absolutelyInfinite(U_40) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [X,Y] :
( ( free(X)
| ( ~ determinedByItselfAlone(Y,X)
& actionOf(Y,X) )
| ~ existsOnlyByNecessityOfOwnNature(X) )
& ( ( ( determinedByItselfAlone(Y,X)
| ~ actionOf(Y,X) )
& existsOnlyByNecessityOfOwnNature(X) )
| ~ free(X) ) ),
inference(fof_nnf,[status(thm)],[free]) ).
fof(f_8_2,plain,
! [U_42,U_41] :
( ( free(U_42)
| ( ~ determinedByItselfAlone(U_41,U_42)
& actionOf(U_41,U_42) )
| ~ existsOnlyByNecessityOfOwnNature(U_42) )
& ( ( ( determinedByItselfAlone(U_41,U_42)
| ~ actionOf(U_41,U_42) )
& existsOnlyByNecessityOfOwnNature(U_42) )
| ~ free(U_42) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_48] :
( ( ! [U_46] : ~ determinedByItselfAlone(U_46,U_48)
& ! [U_45] : actionOf(U_45,U_48) )
| ~ existsOnlyByNecessityOfOwnNature(U_48)
| free(U_48) )
& ! [U_47] :
( ( ! [U_43] :
( determinedByItselfAlone(U_43,U_47)
| ~ actionOf(U_43,U_47) )
& existsOnlyByNecessityOfOwnNature(U_47) )
| ~ free(U_47) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( existsOnlyByNecessityOfOwnNature(U_47)
| ~ free(U_47) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( determinedByItselfAlone(U_43,U_47)
| ~ actionOf(U_43,U_47)
| ~ free(U_47) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( actionOf(U_45,U_48)
| ~ existsOnlyByNecessityOfOwnNature(U_48)
| free(U_48) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_7,plain,
( ~ determinedByItselfAlone(U_46,U_48)
| ~ existsOnlyByNecessityOfOwnNature(U_48)
| free(U_48) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X,Y] :
( ( necessary(X)
| ( ~ isMethodExistence(Y)
& ~ isMethodAction(Y) )
| ~ determinedByDefiniteMethod(X,Y)
| ~ determinedByFixedMethod(X,Y)
| ~ externalTo(Y,X) )
& ( ( ( isMethodExistence(Y)
| isMethodAction(Y) )
& determinedByDefiniteMethod(X,Y)
& determinedByFixedMethod(X,Y)
& externalTo(Y,X) )
| ~ necessary(X) ) ),
inference(fof_nnf,[status(thm)],[necessary]) ).
fof(f_9_2,plain,
! [U_50,U_49] :
( ( necessary(U_50)
| ( ~ isMethodExistence(U_49)
& ~ isMethodAction(U_49) )
| ~ determinedByDefiniteMethod(U_50,U_49)
| ~ determinedByFixedMethod(U_50,U_49)
| ~ externalTo(U_49,U_50) )
& ( ( ( isMethodExistence(U_49)
| isMethodAction(U_49) )
& determinedByDefiniteMethod(U_50,U_49)
& determinedByFixedMethod(U_50,U_49)
& externalTo(U_49,U_50) )
| ~ necessary(U_50) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_58] :
( ! [U_52] :
( ( ~ isMethodExistence(U_52)
& ~ isMethodAction(U_52) )
| ~ determinedByDefiniteMethod(U_58,U_52)
| ~ determinedByFixedMethod(U_58,U_52)
| ~ externalTo(U_52,U_58) )
| necessary(U_58) )
& ! [U_57] :
( ( ! [U_56] :
( isMethodExistence(U_56)
| isMethodAction(U_56) )
& ! [U_55] : determinedByDefiniteMethod(U_57,U_55)
& ! [U_54] : determinedByFixedMethod(U_57,U_54)
& ! [U_53] : externalTo(U_53,U_57) )
| ~ necessary(U_57) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( externalTo(U_53,U_57)
| ~ necessary(U_57) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( determinedByFixedMethod(U_57,U_54)
| ~ necessary(U_57) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( determinedByDefiniteMethod(U_57,U_55)
| ~ necessary(U_57) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_7,plain,
( isMethodExistence(U_56)
| isMethodAction(U_56)
| ~ necessary(U_57) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_8,plain,
( ~ isMethodAction(U_52)
| ~ determinedByDefiniteMethod(U_58,U_52)
| ~ determinedByFixedMethod(U_58,U_52)
| ~ externalTo(U_52,U_58)
| necessary(U_58) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_9,plain,
( ~ isMethodExistence(U_52)
| ~ determinedByDefiniteMethod(U_58,U_52)
| ~ determinedByFixedMethod(U_58,U_52)
| ~ externalTo(U_52,U_58)
| necessary(U_58) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X] :
( ( eternity(X)
| ~ existConcFollowFromDefEternal(X) )
& ( existConcFollowFromDefEternal(X)
| ~ eternity(X) ) ),
inference(fof_nnf,[status(thm)],[eternity]) ).
fof(f_10_2,plain,
! [U_59] :
( ( eternity(U_59)
| ~ existConcFollowFromDefEternal(U_59) )
& ( existConcFollowFromDefEternal(U_59)
| ~ eternity(U_59) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_61] :
( eternity(U_61)
| ~ existConcFollowFromDefEternal(U_61) )
& ! [U_60] :
( existConcFollowFromDefEternal(U_60)
| ~ eternity(U_60) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
cnf(f_10_4,plain,
( existConcFollowFromDefEternal(U_60)
| ~ eternity(U_60) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_5,plain,
( eternity(U_61)
| ~ existConcFollowFromDefEternal(U_61) ),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
! [X,Y] :
( ( exists(X)
| ( ( X = Y
| ~ existsIn(X,Y) )
& ~ existsIn(X,X) ) )
& ( ( X != Y
& existsIn(X,Y) )
| existsIn(X,X)
| ~ exists(X) ) ),
inference(fof_nnf,[status(thm)],[exists]) ).
fof(f_11_2,plain,
! [U_63,U_62] :
( ( exists(U_63)
| ( ( U_63 = U_62
| ~ existsIn(U_63,U_62) )
& ~ existsIn(U_63,U_63) ) )
& ( ( U_63 != U_62
& existsIn(U_63,U_62) )
| existsIn(U_63,U_63)
| ~ exists(U_63) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_69] :
( ( ! [U_65] :
( U_69 = U_65
| ~ existsIn(U_69,U_65) )
& ~ existsIn(U_69,U_69) )
| exists(U_69) )
& ! [U_68] :
( ( ! [U_67] : U_68 != U_67
& ! [U_66] : existsIn(U_68,U_66) )
| existsIn(U_68,U_68)
| ~ exists(U_68) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
cnf(f_11_4,plain,
( existsIn(U_68,U_66)
| existsIn(U_68,U_68)
| ~ exists(U_68) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_5,plain,
( U_68 != U_67
| existsIn(U_68,U_68)
| ~ exists(U_68) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_6,plain,
( ~ existsIn(U_69,U_69)
| exists(U_69) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_7,plain,
( U_69 = U_65
| ~ existsIn(U_69,U_65)
| exists(U_69) ),
inference(clausify,[status(thm)],[f_11_3]) ).
fof(f_12_1,plain,
! [X,Y] :
( ( X != Y
& conceivedThru(X,Y) )
| conceivedThru(X,X) ),
inference(fof_nnf,[status(thm)],[conceived_through]) ).
fof(f_12_2,plain,
! [U_71,U_70] :
( ( U_71 != U_70
& conceivedThru(U_71,U_70) )
| conceivedThru(U_71,U_71) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_71] :
( ( ! [U_73] : U_71 != U_73
& ! [U_72] : conceivedThru(U_71,U_72) )
| conceivedThru(U_71,U_71) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( conceivedThru(U_71,U_72)
| conceivedThru(U_71,U_71) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_5,plain,
( U_71 != U_73
| conceivedThru(U_71,U_71) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [X,Y] :
( ( ( ~ effectNecessarilyFollowsFrom(Y,X)
| definiteCause(X) )
& effectNecessarilyFollowsFrom(Y,X) )
| ~ definiteCause(X) ),
inference(fof_nnf,[status(thm)],[definite_cause]) ).
fof(f_13_2,plain,
! [U_75,U_74] :
( ( ( ~ effectNecessarilyFollowsFrom(U_74,U_75)
| definiteCause(U_75) )
& effectNecessarilyFollowsFrom(U_74,U_75) )
| ~ definiteCause(U_75) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_75] :
( ( ( ! [U_77] : ~ effectNecessarilyFollowsFrom(U_77,U_75)
| definiteCause(U_75) )
& ! [U_76] : effectNecessarilyFollowsFrom(U_76,U_75) )
| ~ definiteCause(U_75) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( effectNecessarilyFollowsFrom(U_76,U_75)
| ~ definiteCause(U_75) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( ~ effectNecessarilyFollowsFrom(U_77,U_75)
| definiteCause(U_75)
| ~ definiteCause(U_75) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X,Y] :
( ( knowledgeOfEffect(X,Y)
| ~ knowledgeOfACause(X) )
& ( knowledgeOfACause(X)
| ~ knowledgeOfEffect(X,Y) ) ),
inference(fof_nnf,[status(thm)],[knowledge_of_effect]) ).
fof(f_14_2,plain,
! [U_79,U_78] :
( ( knowledgeOfEffect(U_79,U_78)
| ~ knowledgeOfACause(U_79) )
& ( knowledgeOfACause(U_79)
| ~ knowledgeOfEffect(U_79,U_78) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_83] :
( ! [U_81] : knowledgeOfEffect(U_83,U_81)
| ~ knowledgeOfACause(U_83) )
& ! [U_82] :
( ! [U_80] : ~ knowledgeOfEffect(U_82,U_80)
| knowledgeOfACause(U_82) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
cnf(f_14_4,plain,
( ~ knowledgeOfEffect(U_82,U_80)
| knowledgeOfACause(U_82) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_5,plain,
( knowledgeOfEffect(U_83,U_81)
| ~ knowledgeOfACause(U_83) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [X,Y] :
( ( ~ conceptionInvolves(Y,X)
& ~ conceptionInvolves(X,Y)
& ~ canBeUnderstoodInTermsOf(Y,X)
& ~ canBeUnderstoodInTermsOf(X,Y) )
| ~ haveNothingInCommon(X,Y) ),
inference(fof_nnf,[status(thm)],[have_nothing_in_common]) ).
fof(f_15_2,plain,
! [U_85,U_84] :
( ( ~ conceptionInvolves(U_84,U_85)
& ~ conceptionInvolves(U_85,U_84)
& ~ canBeUnderstoodInTermsOf(U_84,U_85)
& ~ canBeUnderstoodInTermsOf(U_85,U_84) )
| ~ haveNothingInCommon(U_85,U_84) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( ~ canBeUnderstoodInTermsOf(U_85,U_84)
| ~ haveNothingInCommon(U_85,U_84) ),
inference(clausify,[status(thm)],[f_15_2]) ).
cnf(f_15_4,plain,
( ~ canBeUnderstoodInTermsOf(U_84,U_85)
| ~ haveNothingInCommon(U_85,U_84) ),
inference(clausify,[status(thm)],[f_15_2]) ).
cnf(f_15_5,plain,
( ~ conceptionInvolves(U_85,U_84)
| ~ haveNothingInCommon(U_85,U_84) ),
inference(clausify,[status(thm)],[f_15_2]) ).
cnf(f_15_6,plain,
( ~ conceptionInvolves(U_84,U_85)
| ~ haveNothingInCommon(U_85,U_84) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [X,Y] :
( ( ( objectOf(Y,X)
| ideateOf(Y,X) )
& correspondWith(X,Y) )
| ~ trueIdea(X) ),
inference(fof_nnf,[status(thm)],[true_idea]) ).
fof(f_16_2,plain,
! [U_87,U_86] :
( ( ( objectOf(U_86,U_87)
| ideateOf(U_86,U_87) )
& correspondWith(U_87,U_86) )
| ~ trueIdea(U_87) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
! [U_87] :
( ( ! [U_89] :
( objectOf(U_89,U_87)
| ideateOf(U_89,U_87) )
& ! [U_88] : correspondWith(U_87,U_88) )
| ~ trueIdea(U_87) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( correspondWith(U_87,U_88)
| ~ trueIdea(U_87) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( objectOf(U_89,U_87)
| ideateOf(U_89,U_87)
| ~ trueIdea(U_87) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X] :
( ~ essenceInvExistence(X)
| ~ canBeConceivedAsNonExisting(X) ),
inference(fof_nnf,[status(thm)],[can_be_conceived_as_non_existing]) ).
fof(f_17_2,plain,
! [U_90] :
( ~ essenceInvExistence(U_90)
| ~ canBeConceivedAsNonExisting(U_90) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( ~ essenceInvExistence(U_90)
| ~ canBeConceivedAsNonExisting(U_90) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [X] :
( being(X)
| ~ substance(X) ),
inference(fof_nnf,[status(thm)],[has_substance_being]) ).
fof(f_18_2,plain,
! [U_91] :
( being(U_91)
| ~ substance(U_91) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( being(U_91)
| ~ substance(U_91) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [X] :
( selfCaused(X)
| ~ inItself(X) ),
inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused]) ).
fof(f_19_2,plain,
! [U_92] :
( selfCaused(U_92)
| ~ inItself(U_92) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( selfCaused(U_92)
| ~ inItself(U_92) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [X] :
( hasEssence(X)
| ~ being(X) ),
inference(fof_nnf,[status(thm)],[being_has_essense]) ).
fof(f_20_2,plain,
! [U_93] :
( hasEssence(U_93)
| ~ being(U_93) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( hasEssence(U_93)
| ~ being(U_93) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X] :
( exists(X)
| ~ hasEssence(X)
| ~ essenceInvExistence(X) ),
inference(fof_nnf,[status(thm)],[essence_involves_existence_exists]) ).
fof(f_21_2,plain,
! [U_94] :
( exists(U_94)
| ~ hasEssence(U_94)
| ~ essenceInvExistence(U_94) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( exists(U_94)
| ~ hasEssence(U_94)
| ~ essenceInvExistence(U_94) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,negated_conjecture,
~ ! [X] :
( substance(X)
=> exists(X) ),
inference(negate,[status(cth)],[has_substance_exists]) ).
fof(f_22_2,negated_conjecture,
? [X] :
( ~ exists(X)
& substance(X) ),
inference(fof_nnf,[status(thm)],[f_22_1]) ).
fof(f_22_3,negated_conjecture,
? [U_95] :
( ~ exists(U_95)
& substance(U_95) ),
inference(variable_rename,[status(thm)],[f_22_2]) ).
fof(f_22_4,negated_conjecture,
( ~ exists(sK1)
& substance(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_95,sK1)],[f_22_3]) ).
fof(f_22_5,negated_conjecture,
( ~ exists(sK1)
& substance(sK1) ),
inference(definitional_conversion,[status(esa)],[f_22_4]) ).
cnf(f_22_6,negated_conjecture,
substance(sK1),
inference(clausify,[status(thm)],[f_22_5]) ).
cnf(f_22_7,negated_conjecture,
~ exists(sK1),
inference(clausify,[status(thm)],[f_22_5]) ).
cnf(f_13_5_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_13_5]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( selfCaused(Eq_y_0)
| ~ selfCaused(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_5,axiom,
( essenceInvExistence(Eq_y_0)
| ~ essenceInvExistence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_6,axiom,
( natureConcOnlyByExistence(Eq_y_0)
| ~ natureConcOnlyByExistence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_7,axiom,
( finiteAfterItsKind(Eq_y_0)
| ~ finiteAfterItsKind(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_8,axiom,
( canBeLimitedBy(Eq_y_0,Eq_y_1)
| ~ canBeLimitedBy(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( sameKind(Eq_y_0,Eq_y_1)
| ~ sameKind(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( substance(Eq_y_0)
| ~ substance(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( inItself(Eq_y_0)
| ~ inItself(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( conceivedThruItself(Eq_y_0)
| ~ conceivedThruItself(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( attribute(Eq_y_0)
| ~ attribute(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( intPercAsConstEssSub(Eq_y_0)
| ~ intPercAsConstEssSub(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( mode(Eq_y_0)
| ~ mode(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( modification(Eq_y_0,Eq_y_1)
| ~ modification(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( existsIn(Eq_y_0,Eq_y_1)
| ~ existsIn(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( conceivedThru(Eq_y_0,Eq_y_1)
| ~ conceivedThru(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( god(Eq_y_0)
| ~ god(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( being(Eq_y_0)
| ~ being(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( absolutelyInfinite(Eq_y_0)
| ~ absolutelyInfinite(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( constInInfAttributes(Eq_y_0)
| ~ constInInfAttributes(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( attributeOf(Eq_y_0,Eq_y_1)
| ~ attributeOf(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( expressesEternalEssentiality(Eq_y_0)
| ~ expressesEternalEssentiality(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( expressesInfiniteEssentiality(Eq_y_0)
| ~ expressesInfiniteEssentiality(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( free(Eq_y_0)
| ~ free(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( existsOnlyByNecessityOfOwnNature(Eq_y_0)
| ~ existsOnlyByNecessityOfOwnNature(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( actionOf(Eq_y_0,Eq_y_1)
| ~ actionOf(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( determinedByItselfAlone(Eq_y_0,Eq_y_1)
| ~ determinedByItselfAlone(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( necessary(Eq_y_0)
| ~ necessary(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( externalTo(Eq_y_0,Eq_y_1)
| ~ externalTo(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( determinedByFixedMethod(Eq_y_0,Eq_y_1)
| ~ determinedByFixedMethod(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_33,axiom,
( determinedByDefiniteMethod(Eq_y_0,Eq_y_1)
| ~ determinedByDefiniteMethod(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( isMethodAction(Eq_y_0)
| ~ isMethodAction(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( isMethodExistence(Eq_y_0)
| ~ isMethodExistence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( eternity(Eq_y_0)
| ~ eternity(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( existConcFollowFromDefEternal(Eq_y_0)
| ~ existConcFollowFromDefEternal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( exists(Eq_y_0)
| ~ exists(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( definiteCause(Eq_y_0)
| ~ definiteCause(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( effectNecessarilyFollowsFrom(Eq_y_0,Eq_y_1)
| ~ effectNecessarilyFollowsFrom(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( knowledgeOfEffect(Eq_y_0,Eq_y_1)
| ~ knowledgeOfEffect(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( knowledgeOfACause(Eq_y_0)
| ~ knowledgeOfACause(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( haveNothingInCommon(Eq_y_0,Eq_y_1)
| ~ haveNothingInCommon(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_44,axiom,
( canBeUnderstoodInTermsOf(Eq_y_0,Eq_y_1)
| ~ canBeUnderstoodInTermsOf(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_45,axiom,
( conceptionInvolves(Eq_y_0,Eq_y_1)
| ~ conceptionInvolves(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_46,axiom,
( trueIdea(Eq_y_0)
| ~ trueIdea(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_47,axiom,
( correspondWith(Eq_y_0,Eq_y_1)
| ~ correspondWith(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_48,axiom,
( ideateOf(Eq_y_0,Eq_y_1)
| ~ ideateOf(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_49,axiom,
( objectOf(Eq_y_0,Eq_y_1)
| ~ objectOf(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_50,axiom,
( canBeConceivedAsNonExisting(Eq_y_0)
| ~ canBeConceivedAsNonExisting(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_51,axiom,
( hasEssence(Eq_y_0)
| ~ hasEssence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI022+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 19 19:36:03 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.41 % SZS status Theorem for theBenchmark
% 0.12/0.41 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------