%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : PHI023+1 : TPTP v9.3.1. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n011.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 : Sun Sep 27 08:19:39 AM UTC 2026 % Result : Theorem 11.37s 2.11s % Output : CNFRefutation 11.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : PHI023+1 : TPTP v9.3.1. Released v7.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.37 % Computer : n011.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Sat Sep 26 04:40:14 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.37/2.11 % SZS status Theorem for theBenchmark.p % 11.37/2.11 % SZS output start CNFRefutation for theBenchmark.p % 11.37/2.11 fof(is_in_itself_is_self_caused, axiom, ! [X0] : ((inItself(X0) => selfCaused(X0)))). % 11.37/2.11 fof(being_has_essense, axiom, ! [X0] : ((being(X0) => hasEssence(X0)))). % 11.37/2.11 fof(essence_involves_existence_exists, axiom, ! [X0] : (((essenceInvExistence(X0) & hasEssence(X0)) => exists(X0)))). % 11.37/2.11 fof(self_caused, axiom, ! [X0] : ((selfCaused(X0) <=> (essenceInvExistence(X0) & natureConcOnlyByExistence(X0))))). % 11.37/2.11 fof(substance, axiom, ! [X0] : ((substance(X0) <=> (inItself(X0) & conceivedThruItself(X0))))). % 11.37/2.11 fof(god, axiom, ! [X0] : ((god(X0) <=> (being(X0) & absolutelyInfinite(X0))))). % 11.37/2.11 fof(absolutely_infinite, axiom, ! [X0] : ! [X1] : ((absolutelyInfinite(X0) <=> (substance(X0) & (constInInfAttributes(X0) & (attributeOf(X1,X0) => (expressesEternalEssentiality(X1) & expressesInfiniteEssentiality(X1)))))))). % 11.37/2.11 fof(if_god_then_exists, conjecture, ! [X0] : ((god(X0) => exists(X0)))). % 11.37/2.11 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((god(X0) => exists(X0))), inference(negate_conjecture, [status(cth)], [if_god_then_exists])). % 11.37/2.11 cnf(c0, plain, ~inItself(X0) | selfCaused(X0), inference(clausification, [status(esa)], [is_in_itself_is_self_caused])). % 11.37/2.11 cnf(c1, plain, ~being(X0) | hasEssence(X0), inference(clausification, [status(esa)], [being_has_essense])). % 11.37/2.11 cnf(c2, plain, ~essenceInvExistence(X0) | ~hasEssence(X0) | exists(X0), inference(clausification, [status(esa)], [essence_involves_existence_exists])). % 11.37/2.11 cnf(c3, plain, ~selfCaused(X0) | essenceInvExistence(X0), inference(clausification, [status(esa)], [self_caused])). % 11.37/2.11 cnf(c9, plain, ~substance(X0) | inItself(X0), inference(clausification, [status(esa)], [substance])). % 11.37/2.11 cnf(c22, plain, ~god(X0) | being(X0), inference(clausification, [status(esa)], [god])). % 11.37/2.11 cnf(c23, plain, ~god(X0) | absolutelyInfinite(X0), inference(clausification, [status(esa)], [god])). % 11.37/2.11 cnf(c25, plain, ~absolutelyInfinite(X0) | X1(X0,X2), inference(clausification, [status(esa)], [absolutely_infinite])). % 11.37/2.11 cnf(c27, plain, ~X0(X1,X2) | substance(X1), inference(clausification, [status(esa)], [absolutely_infinite])). % 11.37/2.11 cnf(c64, plain, god(sK35), inference(clausification, [status(esa)], [negated_conjecture])). % 11.37/2.11 cnf(c65, plain, ~exists(sK35), inference(clausification, [status(esa)], [negated_conjecture])). % 11.37/2.11 cnf(d0, plain, absolutelyInfinite(sK35), inference(resolution, [status(thm)], [c23,c64])). % 11.37/2.11 cnf(d1, plain, substance(X0) | ~absolutelyInfinite(X0), inference(resolution, [status(thm)], [c27,c25])). % 11.37/2.11 cnf(d2, plain, substance(sK35), inference(resolution, [status(thm)], [d1,d0])). % 11.37/2.11 cnf(d3, plain, inItself(sK35), inference(resolution, [status(thm)], [d2,c9])). % 11.37/2.11 cnf(d4, plain, selfCaused(sK35), inference(resolution, [status(thm)], [d3,c0])). % 11.37/2.11 cnf(d5, plain, essenceInvExistence(sK35), inference(resolution, [status(thm)], [d4,c3])). % 11.37/2.11 cnf(d6, plain, ~hasEssence(sK35) | exists(sK35), inference(resolution, [status(thm)], [d5,c2])). % 11.37/2.11 cnf(d7, plain, ~hasEssence(sK35), inference(resolution, [status(thm)], [c65,d6])). % 11.37/2.11 cnf(d8, plain, being(sK35), inference(resolution, [status(thm)], [c22,c64])). % 11.37/2.11 cnf(d9, plain, hasEssence(sK35), inference(resolution, [status(thm)], [d8,c1])). % 11.37/2.11 cnf(d10, plain, $false, inference(resolution, [status(thm)], [d9,d7])). % 11.37/2.11 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------