%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP080+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 : n028.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 : Theorem 6.68s 1.83s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NLP080+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.17/0.34 % Computer : n028.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 12:44:31 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 6.68/1.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.68/1.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.68/1.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.68/1.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.68/1.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.68/1.83 Execution lmodel_grow ended with status: unsatisfiable % 6.68/1.83 Used heuristic: lmodel_grow % 6.68/1.83 % 6.68/1.83 Input Clauses: % 6.68/1.83 % 6.68/1.83 Predicates: actual_world male man of cannon member event agent patient present nonreflexive fire from_loc six group shot revenge cry scream ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 % 6.68/1.83 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc11 skc12 skc13 skc14 skc15 skc16 skc17 % 6.68/1.83 Fol Functions: skf8 skf9 skf10 skf18 skf19 skf20 % 6.68/1.83 Problem Properties: % 6.68/1.83 This is a full first-order problem without equality. % 6.68/1.83 % 6.68/1.83 After reduction: Problem Properties: % 6.68/1.83 This is a full first-order problem without equality. % 6.68/1.83 % 6.68/1.83 % 6.68/1.83 Reduced Input Clauses: % 6.68/1.83 % 6.68/1.83 Most General Atoms: ren1(x0,x1,x2,x3,x4) fire(x0,x1) from_loc(x0,x1,x4) member(x0,x1,x2) ren2(x0,x3,x5,x2,x4) ren3(x0,x1,x2) shot(x0,x1) ren4 actual_world(x0) male(x0,x2) man(x0,x2) cannon(x0,x3) six(x0,x1) group(x0,x1) event(x0,x6) agent(x0,x6,x1) present(x0,x6) nonreflexive(x0,x6) scream(x0,x6) ren5(x0,x1,x2,x3,x4) ren6(x0,x3,x5,x2,x4) ren7(x0,x1,x2) ren8 revenge(x0,x4) cry(x0,x5) patient(x0,x6,x5) of(x0,x6,x4) % 6.68/1.83 % 6.68/1.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 71 atoms initially, heuristics mode: lmodel_grow === % 6.68/1.83 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 79 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 92 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 102 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 104 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 107 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 110 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 113 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 117 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 122 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 126 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 129 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 132 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 135 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 138 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 141 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 144 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 147 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 150 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 153 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 156 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 159 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 162 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 165 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 168 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 172 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 176 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 179 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 181 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 183 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 185 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 187 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 189 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 191 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 192 % 6.68/1.83 === Backtracking. Learning clause 64:2:1:[21.2,11.1,10.1]:Top: -> ren4,ren3(skc1,x0,skc4) % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 196 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 200 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 203 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 206 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 210 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 220 % 6.68/1.83 === Backtracking. Learning clause 65:4:10:[9.2,2.2,4.2,1.2,7.2,5.2,6.2]:TopTopTopTopTopTopTopTopTopTop: patient(x0,x1,x2),ren1(x0,x1,x3,x4,x5),ren1(x0,x1,x6,x7,x8) -> ren2(x0,x2,x9,x3,x8) % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 238 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 253 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 262 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 270 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 275 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 280 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 285 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 291 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 298 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 303 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 306 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 309 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 312 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 315 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 318 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 321 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 324 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 327 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 330 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 332 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 334 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 336 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 339 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 342 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 344 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 347 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 350 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 353 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 355 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 357 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 367 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 371 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 374 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 377 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 380 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 383 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 385 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 387 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 389 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 392 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 394 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 397 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 399 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 400 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 410 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 413 % 6.68/1.83 === Backtracking. Learning clause 66:3:4:[3.2,65.1,18.2,8.1]:TopTopTopTop: -> ren2(skc1,x0,x1,skc2,skc3),ren4,ren2(skc1,x0,skc4,x2,x3) % 6.68/1.83 === Backtracking. Learning clause 67:2:0:[31.7,66.1,24.1,25.1,15.1,28.1,27.1,29.1,13.1,26.1,30.1,17.1,14.1,22.1,20.1,16.1,23.1,12.1,64.2,63.1,57.2]:: six(skc1,skc4) -> patient(skc11,skc17,skc15) % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 436 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 442 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 449 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 456 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 471 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 477 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 483 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 489 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 496 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 502 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 505 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 510 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 515 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 520 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 525 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 530 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 534 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 538 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 542 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 548 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 553 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 559 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 564 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 566 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 570 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 576 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 580 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 584 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 589 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 593 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 597 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 602 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 607 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 610 % 6.68/1.83 === Backtracking. Learning clause 68:2:1:[52.2,42.1,41.1]:Top: -> ren8,ren7(skc11,x0,skc14) % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 622 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 629 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 636 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 641 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 647 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 653 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 659 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 664 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 669 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 674 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 679 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 683 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 688 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 693 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 698 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 702 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 710 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 715 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 720 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 723 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 726 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 729 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 732 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 735 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 738 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 741 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 744 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 746 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 748 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 750 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 754 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 758 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 760 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 764 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 767 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 770 % 6.68/1.83 === Clause set with instances from active satisfied. Growing active. New size: 780 % 6.68/1.83 === Backtracking. Learning clause 69:3:4:[40.7,38.2,37.2,36.2,32.2,33.2,35.2,34.2,49.2,39.1]:TopTopTopTop: -> ren6(skc11,x0,x1,skc12,skc13),ren8,ren6(skc11,x0,skc14,x2,x3) % 6.68/1.83 === Backtracking. Learning clause 70:2:1:[62.7,69.1,60.1,51.1,56.1,61.1,54.1,48.1,53.1,59.1,55.1,47.1,43.1,58.1,50.1,46.1,45.1,44.1,68.2,63.2,64.1]:Top: patient(skc11,skc17,skc15) -> ren3(skc1,x0,skc4) % 6.68/1.83 === Backtracking. Learning clause 71:3:1:[31.7,66.1,28.1,26.1,29.1,30.1,13.1,15.1,20.1,22.1,16.1,24.1,23.1,25.1,17.1,14.1,12.1,27.1,63.1,68.1]:Top: six(skc1,skc4),ren3(skc1,skf10(skc1,skc4),skc4) -> ren7(skc11,x0,skc14) % 6.68/1.83 === Backtracking. Learning clause 72:3:0:[31.7,66.1,15.1,28.1,14.1,25.1,29.1,20.1,22.1,17.1,12.1,24.1,27.1,23.1,16.1,13.1,30.1,26.1,63.1]:: six(skc1,skc4),ren3(skc1,skf10(skc1,skc4),skc4),ren8 -> % 6.68/1.83 === Backtracking. Learning clause 73:1:0:[62.7,69.1,59.1,61.1,45.1,47.1,53.1,54.1,48.1,44.1,56.1,46.1,60.1,55.1,43.1,50.1,51.1,58.1,71.3,72.3,70.2,67.2]:: six(skc1,skc4) -> % 6.68/1.83 === Backtracking. Learning clause 74:1:0:[19.1,73.1,63.1]:: ren8 -> % 6.68/1.83 % 6.68/1.83 SZS status Unsatisfiable % 6.68/1.83 % 6.68/1.83 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.68/1.83 % 6.68/1.83 SPASS-SCL-FOL Statistics: % 6.68/1.83 Number of learned clauses: 11 % 6.68/1.83 Number of propagations: 899 % 6.68/1.83 Number of decisions: 1388 % 6.68/1.83 Number of resolutions: 142 % 6.68/1.83 Number of condensations: 3 % 6.68/1.83 Number of sub resolutions: 0 % 6.68/1.83 Number of input literals (deduplicated): 71 % 6.68/1.83 Number of grows: 157 % 6.68/1.83 Number of considered ground atoms: 780 % 6.68/1.83 % 6.68/1.83 Needed: 0:00:01.29 % 6.68/1.83 %------------------------------------------------------------------------------