%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP023+1 : TPTP v9.2.1. Released v2.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n003.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:29:03 PM UTC 2026 % Result : CounterSatisfiable 9.94s 2.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : NLP023+1 : TPTP v9.2.1. Released v2.4.0. % 0.13/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.37 % Computer : n003.cluster.edu % 0.18/0.37 % Model : x86_64 x86_64 % 0.18/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.37 % Memory : 8042.1875MB % 0.18/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.37 % CPULimit : 300 % 0.18/0.37 % WCLimit : 300 % 0.18/0.37 % DateTime : Thu May 7 12:43:12 EDT 2026 % 0.18/0.37 % CPUTime : % 0.18/0.37 SPASS-SCL-FOL version: % 0.29/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 9.94/2.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.94/2.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.94/2.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.94/2.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.94/2.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.94/2.56 Execution resolution_2 ended with status: satisfiable % 9.94/2.56 Used heuristic: resolution_2 % 9.94/2.56 % 9.94/2.56 Input Clauses: % 9.94/2.56 % 9.94/2.56 Predicates: woman female human_person animate human organism living impartial entity existent specific thing mia_forename forename relname relation abstraction unisex general nonhuman proposition desire_want event eventuality nonexistent singleton dance accessible_world of theme agent present = actual_world % 9.94/2.56 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 % 9.94/2.56 Fol Functions: % 9.94/2.56 Problem Properties: % 9.94/2.56 This is a Bernays Schoenfinkel Ramsey problem. % 9.94/2.56 % 9.94/2.56 % 9.94/2.56 Reduced Input Clauses: % 9.94/2.56 % 9.94/2.56 Most General Atoms: accessible_world(x0,x1) female(x1,x2) animate(x1,x2) human(x1,x2) living(x1,x2) impartial(x1,x2) existent(x1,x2) entity(x1,x2) organism(x1,x2) human_person(x1,x2) woman(x1,x2) mia_forename(x1,x2) relname(x1,x2) general(x1,x2) nonhuman(x1,x2) abstraction(x1,x2) relation(x1,x2) agent(x1,x2,x3) present(x1,x2) unisex(x1,x2) nonexistent(x1,x2) specific(x1,x2) singleton(x1,x2) thing(x1,x2) eventuality(x1,x2) event(x1,x2) dance(x1,x2) forename(x0,x3) of(x0,x3,x1) desire_want(x0,x3) proposition(x0,x4) theme(x0,x3,x4) =(x2,x4) actual_world(skc1) % 9.94/2.56 % 9.94/2.56 === Starting SPASS-SCL-FOL A Little Less Naive, considering 1729 atoms initially, heuristics mode: resolution_2 === % 9.94/2.56 % 9.94/2.56 === CC is in false state. New clause to be learned: 81:3:0:TAUT:: =(skc5,skc6),agent(skc1,skc2,skc6) -> agent(skc1,skc2,skc5) % 9.94/2.56 === Restarting. % 9.94/2.56 === Backtracking. Learning clause 82:1:0:[1.1,68.1,32.2,15.2,19.2,20.2]:: proposition(skc1,skc2) -> % 9.94/2.56 === CC is in false state. New clause to be learned: 83:3:0:TAUT:: =(skc5,skc6),organism(skc6,skc4) -> organism(skc5,skc4) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 85:2:0:[74.0,84.1]:: =(skc2,skc5) -> desire_want(skc1,skc2) % 9.94/2.56 === Restarting. % 9.94/2.56 === Backtracking. Learning clause 86:2:1:[47.1,76.1,31.2,7.2,16.2,19.2,9.2,10.2,11.2,20.2]:Top: woman(skc4,x0),proposition(skc1,x0) -> % 9.94/2.56 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc1,skc4),agent(skc1,skc2,skc1) -> agent(skc4,skc2,skc4) % 9.94/2.56 === Restarting. % 9.94/2.56 === Backtracking. Learning clause 88:1:0:[20.1,71.1,19.1,16.1]:: -> general(skc1,skc4) % 9.94/2.56 === CC is in false state. New clause to be learned: 90:2:0:[68.0,89.1]:: =(skc2,skc6) -> woman(skc1,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 92:2:0:[69.0,91.1]:: =(skc2,skc3) -> mia_forename(skc1,skc2) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 94:2:0:[80.0,93.1]:: =(skc4,skc6) -> dance(skc4,skc4) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc5,skc6),of(skc5,skc2,skc6) -> of(skc5,skc2,skc5) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 96:2:0:TAUT:: =(skc6,skc2) -> =(skc2,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 98:2:0:[68.0,97.1]:: =(skc2,skc1) -> woman(skc1,skc1) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 99:1:0:TAUT:: -> =(skc5,skc5) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 100:2:0:TAUT:: =(skc4,skc5) -> =(skc5,skc4) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 102:2:0:[74.0,101.1]:: =(skc4,skc5) -> desire_want(skc1,skc4) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 104:2:0:[76.0,103.1]:: =(skc1,skc4) -> accessible_world(skc4,skc4) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc6,skc1),human_person(skc2,skc1) -> human_person(skc2,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 106:2:0:TAUT:: =(skc1,skc2) -> =(skc2,skc1) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc1,skc4),abstraction(skc1,skc4) -> abstraction(skc1,skc1) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 108:3:0:TAUT:: =(skc5,skc6),human(skc6,skc5) -> human(skc6,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 110:2:0:[74.0,109.1]:: =(skc5,skc6) -> desire_want(skc1,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 111:3:0:TAUT:: =(skc3,skc1),eventuality(skc1,skc6) -> eventuality(skc3,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === Backtracking. Learning clause 112:2:1:[46.2,70.1,14.1,13.1,19.1,15.1,32.1,1.2]:Top: accessible_world(skc1,x0),woman(x0,skc3) -> % 9.94/2.56 === CC is in false state. New clause to be learned: 113:2:0:TAUT:: =(skc6,skc4) -> =(skc4,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 114:2:0:TAUT:: =(skc6,skc1) -> =(skc1,skc6) % 9.94/2.56 === Restarting. % 9.94/2.56 === CC is in false state. New clause to be learned: 116:2:0:[76.0,115.1]:: =(skc1,skc4) -> accessible_world(skc4,skc1) % 9.94/2.56 === Restarting. % 9.94/2.56 % 9.94/2.56 Linear Model Building succeeded. % 9.94/2.56 SZS status Satisfiable % 9.94/2.56 % 9.94/2.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 9.94/2.56 % 9.94/2.56 SPASS-SCL-FOL Statistics: % 9.94/2.56 Number of learned clauses: 4 % 9.94/2.56 Number of propagations: 14174 % 9.94/2.56 Number of decisions: 4319 % 9.94/2.56 Number of resolutions: 24 % 9.94/2.56 Number of condensations: 0 % 9.94/2.56 Number of sub resolutions: 9 % 9.94/2.56 Number of input literals (deduplicated): 48 % 9.94/2.56 Number of grows: 0 % 9.94/2.56 Number of considered ground atoms: 1729 % 9.94/2.56 % 9.94/2.56 Needed: 0:00:01.95 % 9.94/2.56 %------------------------------------------------------------------------------