%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PHI018+1 : TPTP v9.2.1. Released v7.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:31:09 PM UTC 2026 % Result : CounterSatisfiable 0.30s 0.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PHI018+1 : TPTP v9.2.1. Released v7.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n005.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 12:55:46 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.52 Execution normal ended with status: satisfiable % 0.30/0.52 Used heuristic: normal % 0.30/0.52 % 0.30/0.52 Input Clauses: % 0.30/0.52 % 0.30/0.52 Predicates: selfCaused essenceInvExistence natureConcOnlyByExistence finiteAfterItsKind canBeLimitedBy sameKind substance inItself conceivedThruItself attribute intPercAsConstEssSub mode modification existsIn conceivedThru god being absolutelyInfinite constInInfAttributes attributeOf expressesEternalEssentiality expressesInfiniteEssentiality free existsOnlyByNecessityOfOwnNature actionOf determinedByItselfAlone necessary externalTo determinedByFixedMethod determinedByDefiniteMethod isMethodAction isMethodExistence eternity existConcFollowFromDefEternal exists = definiteCause effectNecessarilyFollowsFrom knowledgeOfEffect knowledgeOfACause haveNothingInCommon canBeUnderstoodInTermsOf conceptionInvolves trueIdea correspondWith ideateOf objectOf canBeConceivedAsNonExisting hasEssence ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 % 0.30/0.52 Fol Constants: skc1 % 0.30/0.52 Fol Functions: % 0.30/0.52 Problem Properties: % 0.30/0.52 This is a Bernays Schoenfinkel Ramsey problem. % 0.30/0.52 % 0.30/0.52 % 0.30/0.52 Reduced Input Clauses: % 0.30/0.52 78:2:2:[59.1,60.1]:TopTop: ren9(x0,x1) -> definiteCause(x1) % 0.30/0.52 % 0.30/0.52 Most General Atoms: selfCaused(x0) essenceInvExistence(x0) natureConcOnlyByExistence(x0) finiteAfterItsKind(x0) canBeLimitedBy(x0,x1) sameKind(x0,x1) inItself(x0) conceivedThruItself(x0) attribute(x0) intPercAsConstEssSub(x0) ren1(x0,x1) modification(x0,x1) substance(x1) existsIn(x0,x1) conceivedThru(x0,x1) mode(x0) ren2(x0,x2) god(x0) being(x0) absolutelyInfinite(x0) ren3(x0) expressesEternalEssentiality(x0) expressesInfiniteEssentiality(x0) attributeOf(x0,x1) constInInfAttributes(x0) ren4(x1,x0) actionOf(x0,x1) determinedByItselfAlone(x0,x1) free(x0) existsOnlyByNecessityOfOwnNature(x0) ren5(x1,x0) isMethodAction(x0) isMethodExistence(x0) ren6(x1) externalTo(x0,x1) determinedByFixedMethod(x1,x0) determinedByDefiniteMethod(x1,x0) necessary(x1) eternity(x0) existConcFollowFromDefEternal(x0) ren7(x0,x1) =(x0,x1) exists(x0) ren8(x0,x1) effectNecessarilyFollowsFrom(x0,x1) definiteCause(x0) ren9(x1,x0) knowledgeOfEffect(x0,x1) knowledgeOfACause(x0) ren10(x0,x1) canBeUnderstoodInTermsOf(x1,x0) conceptionInvolves(x1,x0) haveNothingInCommon(x0,x1) ren11(x0,x1) correspondWith(x0,x1) ideateOf(x1,x0) objectOf(x1,x0) trueIdea(x0) canBeConceivedAsNonExisting(x0) hasEssence(x0) % 0.30/0.52 % 0.30/0.52 === Starting SPASS-SCL-FOL A Little Less Naive, considering 60 atoms initially, heuristics mode: normal === % 0.30/0.52 % 0.30/0.52 === Backtracking. Learning clause 79:1:1:[56.1,58.2]:Top: -> conceivedThru(x0,x0) % 0.30/0.52 === CC is in false state. New clause to be learned: 80:1:0:TAUT:: -> =(skc1,skc1) % 0.30/0.52 === Restarting. % 0.30/0.52 % 0.30/0.52 Linear Model Building succeeded. % 0.30/0.52 SZS status Satisfiable % 0.30/0.52 % 0.30/0.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.52 % 0.30/0.52 SPASS-SCL-FOL Statistics: % 0.30/0.52 Number of learned clauses: 1 % 0.30/0.52 Number of propagations: 80 % 0.30/0.52 Number of decisions: 55 % 0.30/0.52 Number of resolutions: 1 % 0.30/0.52 Number of condensations: 1 % 0.30/0.52 Number of sub resolutions: 1 % 0.30/0.52 Number of input literals (deduplicated): 64 % 0.30/0.52 Number of grows: 0 % 0.30/0.52 Number of considered ground atoms: 60 % 0.30/0.52 % 0.30/0.52 Needed: 0:00:00.00 % 0.30/0.52 %------------------------------------------------------------------------------