%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP060+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 : 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:07 PM UTC 2026
% Result : CounterSatisfiable 269.61s 54.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP060+1 : TPTP v9.2.1. Released v2.4.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.34 % Computer : n003.cluster.edu
% 0.19/0.34 % Model : x86_64 x86_64
% 0.19/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.34 % Memory : 8042.1875MB
% 0.19/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.34 % CPULimit : 300
% 0.19/0.34 % WCLimit : 300
% 0.19/0.34 % DateTime : Thu May 7 12:44:27 EDT 2026
% 0.19/0.34 % CPUTime :
% 0.19/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 269.61/54.48 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 269.61/54.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 269.61/54.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 269.61/54.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 269.61/54.48 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 269.61/54.48 Execution lmodel_grow ended with status: satisfiable
% 269.61/54.48 Used heuristic: lmodel_grow
% 269.61/54.48
% 269.61/54.48 Input Clauses:
% 269.61/54.48
% 269.61/54.48 Predicates: actual_world male man member of cannon event agent patient present nonreflexive fire from_loc six group shot ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8
% 269.61/54.48 Fol Constants: skc1 skc2 skc3 skc10 skc11 skc12
% 269.61/54.48 Fol Functions: skf4 skf5 skf6 skf7 skf8 skf9 skf13 skf14 skf15 skf16
% 269.61/54.49 Problem Properties:
% 269.61/54.49 This is a full first-order problem without equality.
% 269.61/54.49
% 269.61/54.49 After reduction: Problem Properties:
% 269.61/54.49 This is a full first-order problem without equality.
% 269.61/54.49
% 269.61/54.49
% 269.61/54.49 Reduced Input Clauses:
% 269.61/54.49
% 269.61/54.49 Most General Atoms: ren1(x0,x1,x2,x3,x4,x5) of(x0,x1,x2) cannon(x0,x1) man(x0,x1) member(x0,x1,x2) event(x0,x1) agent(x0,x1,x2) patient(x0,x1,x3) present(x0,x1) nonreflexive(x0,x1) fire(x0,x1) from_loc(x0,x1,x4) ren2(x0,x2,x4,x5,x3,x6) ren3(x0,x1,x2) shot(x0,x1) ren4 actual_world(x0) male(x0,x1) six(x0,x2) group(x0,x2) ren5(x0,x1,x2,x3,x4) ren6(x0,x4,x5,x6,x2) ren7(x0,x1,x2) ren8
% 269.61/54.49
% 269.61/54.49 === Starting SPASS-SCL-FOL A Little Less Naive, considering 82 atoms initially, heuristics mode: lmodel_grow ===
% 269.61/54.49
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 94
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 103
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 109
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 117
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 131
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 136
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 147
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 152
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 156
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 162
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 168
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 173
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 178
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 185
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 191
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 196
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 199
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 202
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 205
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 208
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 210
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 213
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 218
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 221
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 224
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 227
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 229
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 231
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 233
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 239
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 244
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 248
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 251
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 252
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 254
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 256
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 259
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 261
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 263
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 264
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 265
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 267
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 269
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 271
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 274
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 276
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 279
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 283
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 288
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 291
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 294
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 297
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 299
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 301
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 304
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 305
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 307
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 308
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 311
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 316
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 317
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 318
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 320
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 322
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 325
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 327
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 330
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 332
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 336
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 339
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 341
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 344
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 348
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 352
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 357
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 367
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 373
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 379
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 390
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 398
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 405
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 416
% 269.61/54.49 === Backtracking. Learning clause 44:6:13:[33.4,25.2,27.2,29.2,24.2,30.2,28.2,26.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: of(x0,x1,x2),cannon(x0,x1),ren5(x0,x3,x4,x5,x6),ren5(x0,x3,x7,x8,x1),ren5(x0,x3,x9,x10,x11) -> ren6(x0,x4,x10,x12,x2)
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 435
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 451
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 464
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 477
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 492
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 505
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 516
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 527
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 537
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 548
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 558
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 567
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 577
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 590
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 600
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 608
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 615
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 621
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 628
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 634
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 641
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 647
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 652
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 657
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 664
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 670
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 675
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 681
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 686
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 692
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 697
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 703
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 709
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 714
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 722
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 731
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 742
% 269.61/54.49 === Backtracking. Learning clause 45:6:5:[38.5,44.3,31.1]:TopTopTopTopTop: of(skc10,x0,skc11),member(skc10,x1,skc12),of(skc10,x0,x2),cannon(skc10,x0) -> ren8,ren6(skc10,x3,x1,x4,x2)
% 269.61/54.49 === Backtracking. Learning clause 46:6:7:[32.1,45.2]:TopTopTopTopTopTopTop: of(skc10,x0,skc11),of(skc10,x0,x1),cannon(skc10,x0) -> ren6(skc10,x2,x3,skc12,x4),ren8,ren6(skc10,x5,x3,x6,x1)
% 269.61/54.49 === Conflict found: 46:6:7:[32.1,45.2]:TopTopTopTopTopTopTop: of(skc10,x0,skc11),of(skc10,x0,x1),cannon(skc10,x0) -> ren6(skc10,x2,x3,skc12,x4),ren8,ren6(skc10,x5,x3,x6,x1) {x0 -> skc3, x1 -> skc11, x2 -> skf14(skc10,skc11,skc12), x3 -> skf15(skc10,skc11,skc12), x4 -> skc11, x5 -> skf14(skc10,skc11,skc12), x6 -> skc12}
% 269.61/54.49 === Backtracking. Learning clause 50:6:2:[36.0,47.3,39.0,48.5,40.0,49.6,46.4,42.3]:TopTop: of(skc10,x0,skc11),of(skc10,x0,x1),cannon(skc10,x0),male(skc10,x1),ren7(skc10,skf16(skc10,skc12),skc12) -> ren8
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 752
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 759
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 764
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 771
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 776
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 780
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 784
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 790
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 794
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 798
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 804
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 809
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 813
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 819
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 823
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 827
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 832
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 836
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 841
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 846
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 850
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 856
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 861
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 867
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 871
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 876
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 881
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 887
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 890
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 894
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 899
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 903
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 907
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 910
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 914
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 916
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 919
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 920
% 269.61/54.49 === Clause set with instances from active satisfied. Growing active. New size: 922
% 269.61/54.49
% 269.61/54.49 Linear Model Building succeeded.
% 269.61/54.49 SZS status Satisfiable
% 269.61/54.49
% 269.61/54.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 269.61/54.49
% 269.61/54.49 SPASS-SCL-FOL Statistics:
% 269.61/54.49 Number of learned clauses: 4
% 269.61/54.49 Number of propagations: 912
% 269.61/54.49 Number of decisions: 1359
% 269.61/54.49 Number of resolutions: 11
% 269.61/54.49 Number of condensations: 2
% 269.61/54.49 Number of sub resolutions: 3
% 269.61/54.49 Number of input literals (deduplicated): 46
% 269.61/54.49 Number of grows: 158
% 269.61/54.49 Number of considered ground atoms: 922
% 269.61/54.49
% 269.61/54.49 Needed: 0:0:53.91
% 269.61/54.49
%------------------------------------------------------------------------------