%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PHI037+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 : n015.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.43s 0.63s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : PHI037+1 : TPTP v9.2.1. Released v7.4.0. % 0.13/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.37 % Computer : n015.cluster.edu % 0.19/0.37 % Model : x86_64 x86_64 % 0.19/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.37 % Memory : 8042.1875MB % 0.19/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.37 % CPULimit : 300 % 0.19/0.37 % WCLimit : 300 % 0.19/0.37 % DateTime : Thu May 7 12:55:47 EDT 2026 % 0.19/0.37 % CPUTime : % 0.19/0.37 SPASS-SCL-FOL version: % 0.30/0.47 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.63 Execution resolution_1 ended with status: satisfiable % 0.43/0.63 Used heuristic: resolution_1 % 0.43/0.63 % 0.43/0.63 Input Clauses: % 0.43/0.63 % 0.43/0.63 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.43/0.63 Fol Constants: skc1 skc2 skc3 % 0.43/0.63 Fol Functions: % 0.43/0.63 Problem Properties: % 0.43/0.63 This is a Bernays Schoenfinkel Ramsey problem. % 0.43/0.63 % 0.43/0.63 % 0.43/0.63 Reduced Input Clauses: % 0.43/0.63 77:2:2:[10.1,11.1]:TopTop: ren3(x0,x1) -> definiteCause(x1) % 0.43/0.63 % 0.43/0.63 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(x0) canBeLimitedBy(x0,x1) sameKind(x0,x1) inItself(x0) conceivedThruItself(x0) attribute(x0) intPercAsConstEssSub(x0) ren6(x0,x1) modification(x0,x1) substance(x1) ren7(x0,x1) mode(skc1) 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.43/0.63 % 0.43/0.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 === % 0.43/0.63 % 0.43/0.63 === CC is in false state. New clause to be learned: 78:1:0:TAUT:: -> =(skc1,skc1) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 79:2:1:[30.2,74.1]:Top: substance(x0) -> selfCaused(x0) % 0.43/0.63 === Backtracking. Learning clause 80:3:0:[40.3,42.2]:: existsIn(skc1,skc3),conceivedThru(skc1,skc3),mode(skc1) -> % 0.43/0.63 === CC model inconsistency. New clause to be learned: 81:4:0:TAUT:: =(skc1,skc3),=(skc1,skc2),existsIn(skc2,skc3) -> existsIn(skc1,skc1) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 82:2:2:[15.1,19.2]:TopTop: canBeUnderstoodInTermsOf(x0,x1),haveNothingInCommon(x0,x1) -> % 0.43/0.63 === Backtracking. Learning clause 83:3:0:[43.3,39.1,35.1]:: -> mode(skc1),conceivedThru(skc1,skc3),modification(skc1,skc2) % 0.43/0.63 === CC is in false state. New clause to be learned: 84:3:0:TAUT:: =(skc1,skc2),substance(skc2) -> substance(skc1) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 85:2:2:[9.2,8.1]:TopTop: =(x0,x1) -> conceivedThru(x0,x0) % 0.43/0.63 === CC model inconsistency. New clause to be learned: 86:2:0:TAUT:: =(skc3,skc1) -> =(skc1,skc3) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 87:2:2:[17.1,19.2]:TopTop: conceptionInvolves(x0,x1),haveNothingInCommon(x0,x1) -> % 0.43/0.63 === Backtracking. Learning clause 88:3:0:[37.3,41.2]:: modification(skc1,skc2),substance(skc2),mode(skc1) -> % 0.43/0.63 === CC is in false state. New clause to be learned: 89:3:0:TAUT:: =(skc1,skc3),existsIn(skc1,skc1) -> existsIn(skc1,skc3) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 90:3:0:[43.3,38.1,36.1]:: -> mode(skc1),existsIn(skc1,skc3),substance(skc2) % 0.43/0.63 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc1,skc3),existsIn(skc1,skc3) -> existsIn(skc1,skc1) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 92:3:2:[50.1,55.2]:TopTop: attributeOf(x0,x1),absolutelyInfinite(x1) -> ren8(x0) % 0.43/0.63 === CC model inconsistency. New clause to be learned: 93:1:0:TAUT:: -> =(skc3,skc3) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 94:2:1:[45.2,53.1]:Top: god(x0) -> substance(x0) % 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 70 % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 95:2:0:[2.1,4.3,78.1]:: exists(skc1) -> existsIn(skc1,skc1) % 0.43/0.63 === CC is in false state. New clause to be learned: 96:2:0:TAUT:: =(skc1,skc3) -> =(skc3,skc1) % 0.43/0.63 === Restarting. % 0.43/0.63 === CC is in false state. New clause to be learned: 97:3:0:TAUT:: =(skc1,skc2),substance(skc1) -> substance(skc2) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 98:3:2:[63.1,69.2]:TopTop: necessary(x0) -> isMethodAction(x1),isMethodExistence(x1) % 0.43/0.63 === Backtracking. Learning clause 99:3:2:[21.1,22.2]:TopTop: trueIdea(x0) -> ideateOf(x1,x0),objectOf(x1,x0) % 0.43/0.63 === Backtracking. Learning clause 100:2:2:[20.1,22.2]:TopTop: trueIdea(x0) -> correspondWith(x0,x1) % 0.43/0.63 === Backtracking. Learning clause 101:4:2:[51.2,56.3]:TopTop: substance(x0),constInInfAttributes(x0) -> attributeOf(x1,x0),absolutelyInfinite(x0) % 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 134 % 0.43/0.63 === CC model inconsistency. New clause to be learned: 102:1:0:TAUT:: -> =(skc2,skc2) % 0.43/0.63 === Restarting. % 0.43/0.63 === CC is in false state. New clause to be learned: 103:2:0:TAUT:: =(skc2,skc1) -> =(skc1,skc2) % 0.43/0.63 === Restarting. % 0.43/0.63 === Backtracking. Learning clause 104:2:0:[3.3,6.1,91.1,95.1]:: existsIn(skc1,skc3) -> existsIn(skc1,skc1) % 0.43/0.63 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc1,skc3),ren10(skc1,skc1) -> ren10(skc3,skc1) % 0.43/0.63 === Restarting. % 0.43/0.63 === CC is in false state. New clause to be learned: 106:3:0:TAUT:: =(skc1,skc3),conceivedThru(skc3,skc3) -> conceivedThru(skc1,skc3) % 0.43/0.63 === Restarting. % 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 199 % 0.43/0.63 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc2,skc3),existsIn(skc1,skc3) -> existsIn(skc1,skc2) % 0.43/0.63 === Restarting. % 0.43/0.63 === CC is in false state. New clause to be learned: 108:3:0:TAUT:: =(skc2,skc3),existsIn(skc1,skc2) -> existsIn(skc1,skc3) % 0.43/0.63 === Restarting. % 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 263 % 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 318 % 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 350 % 0.43/0.63 % 0.43/0.63 Linear Model Building succeeded. % 0.43/0.63 SZS status Satisfiable % 0.43/0.63 % 0.43/0.63 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.63 % 0.43/0.63 SPASS-SCL-FOL Statistics: % 0.43/0.63 Number of learned clauses: 16 % 0.43/0.63 Number of propagations: 1042 % 0.43/0.63 Number of decisions: 878 % 0.43/0.63 Number of resolutions: 21 % 0.43/0.63 Number of condensations: 0 % 0.43/0.63 Number of sub resolutions: 1 % 0.43/0.63 Number of input literals (deduplicated): 64 % 0.43/0.63 Number of grows: 6 % 0.43/0.63 Number of considered ground atoms: 350 % 0.43/0.63 % 0.43/0.63 Needed: 0:00:00.02 % 0.43/0.63 %------------------------------------------------------------------------------