%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PHI034+1 : TPTP v9.2.1. Released v7.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n022.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:10 PM UTC 2026 % Result : CounterSatisfiable 0.38s 0.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PHI034+1 : TPTP v9.2.1. Released v7.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.35 % Computer : n022.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Thu May 7 12:55:51 EDT 2026 % 0.18/0.35 % CPUTime : % 0.18/0.35 SPASS-SCL-FOL version: % 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.38/0.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.56 Execution normal ended with status: satisfiable % 0.38/0.56 Used heuristic: normal % 0.38/0.56 % 0.38/0.56 Input Clauses: % 0.38/0.56 % 0.38/0.56 Predicates: exists existsIn = conceivedThru definiteCause effectNecessarilyFollowsFrom knowledgeOfEffect knowledgeOfACause haveNothingInCommon canBeUnderstoodInTermsOf conceptionInvolves trueIdea correspondWith ideateOf objectOf canBeConceivedAsNonExisting essenceInvExistence selfCaused natureConcOnlyByExistence finiteAfterItsKind canBeLimitedBy sameKind substance inItself conceivedThruItself attribute intPercAsConstEssSub mode modification god being absolutelyInfinite constInInfAttributes attributeOf expressesEternalEssentiality expressesInfiniteEssentiality free existsOnlyByNecessityOfOwnNature actionOf determinedByItselfAlone necessary externalTo determinedByFixedMethod determinedByDefiniteMethod isMethodAction isMethodExistence eternity existConcFollowFromDefEternal hasEssence ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 % 0.38/0.56 Fol Constants: skc1 skc2 % 0.38/0.56 Fol Functions: % 0.38/0.56 Problem Properties: % 0.38/0.56 This is a Bernays Schoenfinkel Ramsey problem. % 0.38/0.56 % 0.38/0.56 % 0.38/0.56 Reduced Input Clauses: % 0.38/0.56 77:2:2:[10.1,11.1]:TopTop: ren3(x0,x1) -> definiteCause(x1) % 0.38/0.56 % 0.38/0.56 Most General Atoms: ren1(x0,x1) existsIn(x0,x1) =(x0,x1) exists(x0) ren2(x0,x1) conceivedThru(x0,x1) effectNecessarilyFollowsFrom(x0,x1) definiteCause(x0) ren3(x1,x0) knowledgeOfEffect(x0,x1) knowledgeOfACause(x0) ren4(x0,x1) canBeUnderstoodInTermsOf(x1,x0) conceptionInvolves(x1,x0) haveNothingInCommon(x0,x1) ren5(x0,x1) correspondWith(x0,x1) ideateOf(x1,x0) objectOf(x1,x0) trueIdea(x0) canBeConceivedAsNonExisting(x0) essenceInvExistence(x0) selfCaused(x0) natureConcOnlyByExistence(x0) finiteAfterItsKind(skc1) canBeLimitedBy(skc1,skc2) sameKind(skc1,skc2) inItself(x0) conceivedThruItself(x0) attribute(x0) intPercAsConstEssSub(x0) ren6(x0,x1) modification(x0,x1) substance(x1) mode(x0) ren7(x0,x2) god(x0) being(x0) absolutelyInfinite(x0) ren8(x0) expressesEternalEssentiality(x0) expressesInfiniteEssentiality(x0) attributeOf(x0,x1) constInInfAttributes(x0) ren9(x1,x0) actionOf(x0,x1) determinedByItselfAlone(x0,x1) free(x0) existsOnlyByNecessityOfOwnNature(x0) ren10(x1,x0) isMethodAction(x0) isMethodExistence(x0) ren11(x1) externalTo(x0,x1) determinedByFixedMethod(x1,x0) determinedByDefiniteMethod(x1,x0) necessary(x1) eternity(x0) existConcFollowFromDefEternal(x0) hasEssence(x0) % 0.38/0.56 % 0.38/0.56 === Starting SPASS-SCL-FOL A Little Less Naive, considering 171 atoms initially, heuristics mode: normal === % 0.38/0.56 % 0.38/0.56 === Backtracking. Learning clause 78:1:1:[7.1,9.2]:Top: -> conceivedThru(x0,x0) % 0.38/0.56 === Backtracking. Learning clause 80:2:1:[78.0,79.1,4.3,1.1,40.1,43.1]:Top: exists(x0) -> mode(x0) % 0.38/0.56 === Backtracking. Learning clause 82:2:1:[78.0,81.1,1.1,4.3,40.1]:Top: exists(x0) -> ren7(x0,x0) % 0.38/0.56 === CC is in false state. New clause to be learned: 83:1:0:TAUT:: -> =(skc2,skc2) % 0.38/0.56 === Restarting. % 0.38/0.56 === CC is in false state. New clause to be learned: 84:1:0:TAUT:: -> =(skc1,skc1) % 0.38/0.56 === Restarting. % 0.38/0.56 === CC is in false state. New clause to be learned: 85:2:0:TAUT:: =(skc1,skc2) -> =(skc2,skc1) % 0.38/0.56 === Restarting. % 0.38/0.56 === Backtracking. Learning clause 86:3:3:[76.1,24.2,75.2,74.2,30.2,73.2,36.2,41.2]:TopTopTop: mode(x0) -> exists(x1),ren7(x0,x2) % 0.38/0.56 === CC is in false state. New clause to be learned: 87:2:0:TAUT:: =(skc2,skc1) -> =(skc1,skc2) % 0.38/0.56 === Restarting. % 0.38/0.56 === Backtracking. Learning clause 88:2:1:[75.1,73.2,76.2,24.2,74.2,30.2]:Top: substance(x0) -> exists(x0) % 0.38/0.56 % 0.38/0.56 Linear Model Building succeeded. % 0.38/0.56 SZS status Satisfiable % 0.38/0.56 % 0.38/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.56 % 0.38/0.56 SPASS-SCL-FOL Statistics: % 0.38/0.56 Number of learned clauses: 5 % 0.38/0.56 Number of propagations: 372 % 0.38/0.56 Number of decisions: 200 % 0.38/0.56 Number of resolutions: 18 % 0.38/0.56 Number of condensations: 1 % 0.38/0.56 Number of sub resolutions: 3 % 0.38/0.56 Number of input literals (deduplicated): 62 % 0.38/0.56 Number of grows: 0 % 0.38/0.56 Number of considered ground atoms: 171 % 0.38/0.56 % 0.38/0.56 Needed: 0:00:00.01 % 0.38/0.56 %------------------------------------------------------------------------------