%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : CSR045+1 : TPTP v9.2.1. Released v3.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/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:19:46 PM UTC 2026 % Result : Theorem 0.30s 0.80s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.16 % Problem : CSR045+1 : TPTP v9.2.1. Released v3.4.0. % 0.11/0.16 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.58 % Computer : n022.cluster.edu % 0.17/0.58 % Model : x86_64 x86_64 % 0.17/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.58 % Memory : 8042.1875MB % 0.17/0.58 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.58 % CPULimit : 300 % 0.17/0.58 % WCLimit : 300 % 0.17/0.58 % DateTime : Thu May 7 11:39:54 EDT 2026 % 0.17/0.58 % CPUTime : % 0.17/0.58 SPASS-SCL-FOL version: % 0.20/0.67 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.30/0.80 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.80 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.80 Execution resolution_1 ended with status: unsatisfiable % 0.30/0.80 Used heuristic: resolution_1 % 0.30/0.80 % 0.30/0.80 Input Clauses: % 0.30/0.80 % 0.30/0.80 Predicates: applicationcontext genls microtheory aspatialinformationstore genlmt intangibleindividual partiallyintangibleindividual individual transitivebinarypredicate collection disjointwith isa genlinverse genlpreds arg1isa relation predicate binarypredicate mtvisible thing % 0.30/0.80 Fol Constants: c_wamt_evalinitial_p14 c_microtheory c_aspatialinformationstore c_universalvocabularymt c_corecyclmt c_intangibleindividual c_partiallyintangibleindividual c_individual c_genlmt c_logicaltruthmt c_applicationcontext c_collection c_genls c_basekb c_transitivebinarypredicate c_tptpcol_15_80088 % 0.30/0.80 Fol Functions: % 0.30/0.80 Problem Properties: % 0.30/0.80 This is a Bernays Schoenfinkel problem. % 0.30/0.80 % 0.30/0.80 After reduction: Problem Properties: % 0.30/0.80 This is a Bernays Schoenfinkel problem. % 0.30/0.80 % 0.30/0.80 % 0.30/0.80 Reduced Input Clauses: % 0.30/0.80 % 0.30/0.80 Most General Atoms: aspatialinformationstore(x0) intangibleindividual(x0) partiallyintangibleindividual(x0) individual(x0) applicationcontext(x0) isa(x0,x2) collection(x1) relation(x0) thing(x0) arg1isa(x0,x2) predicate(x0) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) disjointwith(x2,x1) transitivebinarypredicate(x0) mtvisible(x1) genls(x0,x2) microtheory(x1) genlmt(x0,x2) % 0.30/0.80 % 0.30/0.80 === Starting SPASS-SCL-FOL A Little Less Naive, considering 52 atoms initially, heuristics mode: resolution_1 === % 0.30/0.80 % 0.30/0.80 === Backtracking. Learning clause 86:1:0:[41.1,16.1]:: -> collection(c_individual) % 0.30/0.80 === Backtracking. Learning clause 87:1:0:[42.1,16.1]:: -> collection(c_collection) % 0.30/0.80 === Backtracking. Learning clause 88:1:0:[43.1,16.1]:: -> disjointwith(c_individual,c_collection) % 0.30/0.80 === Backtracking. Learning clause 89:2:1:[80.1,78.2]:Top: applicationcontext(x0) -> collection(c_applicationcontext) % 0.30/0.80 === Backtracking. Learning clause 90:2:1:[82.1,78.2]:Top: applicationcontext(x0) -> thing(x0) % 0.30/0.80 === Backtracking. Learning clause 91:3:3:[22.3,28.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2) % 0.30/0.80 === Backtracking. Learning clause 92:1:0:[24.1,19.1]:: -> relation(c_genls) % 0.30/0.80 === Clause set with instances from active satisfied. Growing active. New size: 93 % 0.30/0.80 === Restarting. % 0.30/0.80 === Backtracking. Learning clause 93:1:0:[69.1,85.1]:: -> collection(c_tptpcol_15_80088) % 0.30/0.80 % 0.30/0.80 SZS status Unsatisfiable % 0.30/0.80 % 0.30/0.80 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.80 % 0.30/0.80 SPASS-SCL-FOL Statistics: % 0.30/0.80 Number of learned clauses: 8 % 0.30/0.80 Number of propagations: 312 % 0.30/0.80 Number of decisions: 114 % 0.30/0.80 Number of resolutions: 16 % 0.30/0.80 Number of condensations: 0 % 0.30/0.80 Number of sub resolutions: 0 % 0.30/0.80 Number of input literals (deduplicated): 47 % 0.30/0.80 Number of grows: 1 % 0.30/0.80 Number of considered ground atoms: 93 % 0.30/0.80 % 0.30/0.80 Needed: 0:00:00.01 % 0.30/0.80 %------------------------------------------------------------------------------