%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP067-1 : TPTP v9.2.1. Released v2.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n007.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:08 PM UTC 2026 % Result : Satisfiable 0.49s 0.58s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP067-1 : TPTP v9.2.1. Released v2.4.0. % 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.33 % Computer : n007.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 12:43:39 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.18/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.49/0.58 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.58 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.58 Execution lmodel_grow ended with status: satisfiable % 0.49/0.58 Used heuristic: lmodel_grow % 0.49/0.58 % 0.49/0.58 Input Clauses: % 0.49/0.58 % 0.49/0.58 Predicates: actual_world ssSkC0 group six ssSkP1 male ssSkP0 cannon man of member shot fire nonreflexive present event patient from_loc agent % 0.49/0.58 Fol Constants: skc46 skc4 skc47 skc5 % 0.49/0.58 Fol Functions: skf12 skf14 skf19 skf16 skf15 skf21 skf9 skf10 % 0.49/0.58 Problem Properties: % 0.49/0.58 This is a full first-order problem without equality. % 0.49/0.58 % 0.49/0.58 After reduction: Problem Properties: % 0.49/0.58 This is a full first-order problem without equality. % 0.49/0.58 % 0.49/0.58 % 0.49/0.58 Reduced Input Clauses: % 0.49/0.58 % 0.49/0.58 Most General Atoms: ssSkC0 shot(skc46,x0) shot(skc4,x0) member(x0,x1,x2) cannon(x0,x1) of(x0,x1,x2) patient(x0,skf15(x0,x1),x1) from_loc(x0,skf15(x0,x1),x1) shot(x0,skf21(x0,x1)) actual_world(x0) group(x0,x1) six(x0,x1) male(x0,x1) shot(x0,skf9(x0,x1)) man(x0,x3) patient(x0,skf10(x0,x3,x1),x1) from_loc(x0,skf10(x0,x3,x1),x1) from_loc(x0,x1,skf12(x0,x2)) fire(x0,x1) nonreflexive(x0,x1) present(x0,x1) patient(x0,x1,skf12(x0,x2)) event(x0,x1) ssSkP0(x3,x0) patient(x0,x1,skf19(x0,x2)) from_loc(x0,x1,skf19(x0,x2)) agent(x0,x1,x3) ssSkP1(x4,x0) % 0.49/0.58 % 0.49/0.58 === Starting SPASS-SCL-FOL A Little Less Naive, considering 61 atoms initially, heuristics mode: lmodel_grow === % 0.49/0.58 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 70 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 76 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 83 % 0.49/0.58 === Backtracking. Learning clause 45:6:4:[3.1,41.0,4.1,42.1,6.1,43.2,1.0,44.3,18.3,27.1,28.7,12.1,33.4,15.1]:TopTopTopTop: of(skc46,x0,x1),cannon(skc46,x0),member(skc46,x0,x1) -> ssSkC0,nonreflexive(skc46,skf10(skc46,x2,x3)),member(skc46,skf12(skc46,x1),x1) % 0.49/0.58 === Backtracking. Learning clause 50:2:1:[3.1,46.0,4.1,47.1,6.1,48.2,1.0,49.3,18.3,27.1,28.7,12.1]:Top: -> ssSkC0,man(skc46,skf14(skc46,x0)) % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 92 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 121 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 133 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 139 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 141 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 151 % 0.49/0.58 === Backtracking. Learning clause 51:3:3:[21.2,11.2,14.2,15.2]:TopTopTop: ssSkP1(x0,x1) -> fire(x1,skf15(x1,x2)),ssSkP0(x0,x1) % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 162 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 181 % 0.49/0.58 === Backtracking. Learning clause 53:3:3:[15.1,52.0,20.2,11.2,14.2]:TopTopTop: ssSkP1(x0,x1) -> man(x1,skf16(x1,x2)),ssSkP0(x0,x1) % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 189 % 0.49/0.58 === Backtracking. Learning clause 54:7:4:[40.3,34.6,45.5,36.6,35.6,37.6,32.6,38.6,15.1]:TopTopTopTop: of(skc46,skf19(skc46,x0),x1),cannon(skc46,skf19(skc46,x0)),member(skc46,skf19(skc46,x0),x1),man(skc46,x2) -> ssSkP1(x3,skc46),ssSkC0,member(skc46,skf12(skc46,x1),x1) % 0.49/0.58 === Backtracking. Learning clause 60:6:4:[3.1,55.0,4.1,56.1,6.1,57.2,1.0,58.3,5.1,59.4,18.1,28.7,27.1,53.3,37.4]:TopTopTopTop: of(skc46,x0,x1),cannon(skc46,x0),member(skc46,x0,x1),ssSkP0(x1,skc46) -> ssSkC0,agent(skc46,skf10(skc46,skf16(skc46,x2),x3),skf16(skc46,x2)) % 0.49/0.58 === Backtracking. Learning clause 63:10:4:[60.5,61.4,13.1,62.6,40.6,38.6,36.6,20.5,5.2,15.2,14.2,11.2]:TopTopTopTop: event(skc46,skf10(skc46,skf16(skc46,x0),skf19(skc46,x1))),present(skc46,skf10(skc46,skf16(skc46,x0),skf19(skc46,x1))),nonreflexive(skc46,skf10(skc46,skf16(skc46,x0),skf19(skc46,x1))),fire(skc46,skf10(skc46,skf16(skc46,x0),skf19(skc46,x1))),of(skc46,skf19(skc46,x1),x2),member(skc46,skf19(skc46,x1),x2),ssSkP0(x2,skc46) -> ssSkP1(x3,skc46),ssSkC0,ssSkP0(skc47,skc46) % 0.49/0.58 === Backtracking. Learning clause 65:3:0:[1.0,64.1,28.2,4.2,3.2,6.2]:: ssSkP0(skc47,skc46) -> member(skc46,skf21(skc46,skc47),skc47),ssSkC0 % 0.49/0.58 === Backtracking. Learning clause 67:10:6:[1.0,66.0,27.3,4.2,6.2,3.2,18.3,65.2,63.10,34.6,33.6,35.6,32.6]:TopTopTopTopTopTop: of(skc46,skf19(skc46,x0),x1),member(skc46,skf19(skc46,x0),x1),ssSkP0(x1,skc46),of(skc46,x2,x3),cannon(skc46,x2),member(skc46,x2,x3),man(skc46,x4),ssSkP0(x3,skc46) -> ssSkP1(x5,skc46),ssSkC0 % 0.49/0.58 === Clause set with instances from active satisfied. Growing active. New size: 191 % 0.49/0.58 % 0.49/0.58 Linear Model Building succeeded. % 0.49/0.58 SZS status Satisfiable % 0.49/0.58 % 0.49/0.58 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.49/0.58 % 0.49/0.58 SPASS-SCL-FOL Statistics: % 0.49/0.58 Number of learned clauses: 9 % 0.49/0.58 Number of propagations: 318 % 0.49/0.58 Number of decisions: 525 % 0.49/0.58 Number of resolutions: 45 % 0.49/0.58 Number of condensations: 5 % 0.49/0.58 Number of sub resolutions: 18 % 0.49/0.58 Number of input literals (deduplicated): 61 % 0.49/0.58 Number of grows: 13 % 0.49/0.58 Number of considered ground atoms: 191 % 0.49/0.58 % 0.49/0.58 Needed: 0:00:00.04 % 0.49/0.58 %------------------------------------------------------------------------------