%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP080-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 : n006.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:10 PM UTC 2026
% Result : Unsatisfiable 0.86s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP080-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n006.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.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 12:44:16 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.86/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.67 Execution resolution_1 ended with status: unsatisfiable
% 0.86/0.67 Used heuristic: resolution_1
% 0.86/0.67
% 0.86/0.67 Input Clauses:
% 0.86/0.67
% 0.86/0.67 Predicates: actual_world ssSkC0 revenge event present nonreflexive scream group six male cannon man cry of agent patient ssSkP0 member shot fire from_loc
% 0.86/0.67 Fol Constants: skc39 skc14 skc45 skc40 skc42 skc43 skc44 skc41 skc20 skc15 skc17 skc18 skc19 skc16
% 0.86/0.67 Fol Functions: skf9 skf7 skf12 skf6
% 0.86/0.67 Problem Properties:
% 0.86/0.67 This is a full first-order problem without equality.
% 0.86/0.67
% 0.86/0.67 After reduction: Problem Properties:
% 0.86/0.67 This is a full first-order problem without equality.
% 0.86/0.67
% 0.86/0.67
% 0.86/0.67 Reduced Input Clauses:
% 0.86/0.67
% 0.86/0.67 Most General Atoms: ssSkC0 shot(skc39,x0) shot(skc14,x0) member(x0,x1,x2) from_loc(x0,x1,x2) fire(x0,x1) event(x0,x2) present(x0,x2) nonreflexive(x0,x2) scream(x0,x2) agent(x0,x2,x3) shot(x0,skf12(x0,x4)) group(x0,x3) six(x0,x3) actual_world(x0) cannon(x0,x4) ssSkP0(x4,x5,x3,x0) man(x0,x5) male(x0,x5) revenge(x0,x1) of(x0,x2,x1) shot(x0,skf6(x0,x4)) patient(x0,x2,x6) cry(x0,x6)
% 0.86/0.67
% 0.86/0.67 === Starting SPASS-SCL-FOL A Little Less Naive, considering 65 atoms initially, heuristics mode: resolution_1 ===
% 0.86/0.67
% 0.86/0.67 === Backtracking. Learning clause 55:17:8:[40.2,52.1,41.2,53.2,42.2,54.3,49.2,45.3,44.3]:TopTopTopTopTopTopTopTop: cry(x0,x1),scream(x0,skf7(x0,x1,x2,x3)),group(x0,x3),six(x0,x3),male(x0,x3),cannon(x0,x4),ssSkP0(x4,x5,x3,x0),of(x0,x4,x5),man(x0,x5),male(x0,x5),of(x0,skf7(x0,x1,x2,x3),x6),revenge(x0,x6),actual_world(x0),member(x0,x1,x7),ssSkP0(x2,x3,x7,x0) -> ssSkC0,member(x0,skf12(x0,x3),x3)
% 0.86/0.67 === Backtracking. Learning clause 56:3:4:[37.1,39.2]:TopTopTopTop: -> ssSkC0,shot(skc39,skf9(skc42,skc39,x0,x1)),ssSkP0(x2,x3,skc42,skc39)
% 0.86/0.67 === Clause set with instances from active satisfied. Growing active. New size: 71
% 0.86/0.67 === Restarting.
% 0.86/0.67 === Clause set with instances from active satisfied. Growing active. New size: 135
% 0.86/0.67 === Backtracking. Learning clause 61:7:2:[8.1,57.0,9.1,58.1,10.1,59.2,1.0,60.8,49.6,7.2,28.2,14.2,6.2,4.2,27.2,3.2,30.2,5.2,37.1]:TopTop: cannon(skc39,x0),ssSkP0(x0,x1,skc42,skc39),of(skc39,x0,x1),man(skc39,x1),male(skc39,x1) -> ssSkC0,shot(skc39,skf12(skc39,skc42))
% 0.86/0.67 === Backtracking. Learning clause 66:6:2:[8.1,62.0,9.1,63.1,10.1,64.2,1.0,65.3,48.18,3.2,61.7,30.2,6.2,4.2,14.2,5.2,27.2,28.2,7.2]:TopTop: cannon(skc39,x0),ssSkP0(x0,x1,skc42,skc39),of(skc39,x0,x1),man(skc39,x1),male(skc39,x1) -> ssSkC0
% 0.86/0.67 === Conflict found: 61:7:2:[8.1,57.0,9.1,58.1,10.1,59.2,1.0,60.8,49.6,7.2,28.2,14.2,6.2,4.2,27.2,3.2,30.2,5.2,37.1]:TopTop: cannon(skc39,x0),ssSkP0(x0,x1,skc42,skc39),of(skc39,x0,x1),man(skc39,x1),male(skc39,x1) -> ssSkC0,shot(skc39,skf12(skc39,skc42)) {x0 -> skc43, x1 -> skc44}
% 0.86/0.67 === Backtracking. Learning clause 67:2:0:[61.3,29.2,35.2,11.2,12.2,13.2]:: -> shot(skc39,skf12(skc39,skc42)),ssSkC0
% 0.86/0.67 === Conflict found: 66:6:2:[8.1,62.0,9.1,63.1,10.1,64.2,1.0,65.3,48.18,3.2,61.7,30.2,6.2,4.2,14.2,5.2,27.2,28.2,7.2]:TopTop: cannon(skc39,x0),ssSkP0(x0,x1,skc42,skc39),of(skc39,x0,x1),man(skc39,x1),male(skc39,x1) -> ssSkC0 {x0 -> skc43, x1 -> skc44}
% 0.86/0.67 === Backtracking. Learning clause 68:1:0:[66.1,11.2,35.2,13.2,12.2,29.2]:: -> ssSkC0
% 0.86/0.67
% 0.86/0.67 SZS status Unsatisfiable
% 0.86/0.67
% 0.86/0.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.67
% 0.86/0.67 SPASS-SCL-FOL Statistics:
% 0.86/0.67 Number of learned clauses: 6
% 0.86/0.67 Number of propagations: 151
% 0.86/0.67 Number of decisions: 125
% 0.86/0.67 Number of resolutions: 54
% 0.86/0.67 Number of condensations: 2
% 0.86/0.67 Number of sub resolutions: 11
% 0.86/0.67 Number of input literals (deduplicated): 73
% 0.86/0.67 Number of grows: 2
% 0.86/0.67 Number of considered ground atoms: 135
% 0.86/0.67
% 0.86/0.67 Needed: 0:00:00.16
% 0.86/0.67
%------------------------------------------------------------------------------