%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP081+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:10 PM UTC 2026 % Result : Theorem 3.59s 1.30s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP081+1 : TPTP v9.2.1. Released v2.4.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n007.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % 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:24 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 3.59/1.29 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/1.29 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/1.29 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/1.29 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/1.29 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/1.29 Execution lmodel_grow ended with status: unsatisfiable % 3.59/1.29 Used heuristic: lmodel_grow % 3.59/1.29 % 3.59/1.29 Input Clauses: % 3.59/1.30 % 3.59/1.30 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 % 3.59/1.30 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc11 skc12 skc13 skc14 skc15 skc16 skc17 % 3.59/1.30 Fol Functions: skf8 skf9 skf10 skf18 skf19 skf20 % 3.59/1.30 Problem Properties: % 3.59/1.30 This is a full first-order problem without equality. % 3.59/1.30 % 3.59/1.30 After reduction: Problem Properties: % 3.59/1.30 This is a full first-order problem without equality. % 3.59/1.30 % 3.59/1.30 % 3.59/1.30 Reduced Input Clauses: % 3.59/1.30 % 3.59/1.30 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,x1) man(x0,x1) cannon(x0,x2) six(x0,x3) group(x0,x3) 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) % 3.59/1.30 % 3.59/1.30 === Starting SPASS-SCL-FOL A Little Less Naive, considering 69 atoms initially, heuristics mode: lmodel_grow === % 3.59/1.30 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 75 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 79 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 82 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 85 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 88 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 91 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 94 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 103 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 107 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 112 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 126 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 131 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 135 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 139 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 143 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 147 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 150 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 153 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 157 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 161 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 165 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 167 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 168 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 169 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 170 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 177 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 179 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 185 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 188 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 190 % 3.59/1.30 === Backtracking. Learning clause 62:2:1:[20.2,11.1,10.1]:Top: -> ren4,ren3(skc1,x0,skc4) % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 205 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 211 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 216 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 227 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 236 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 247 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 256 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 262 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 270 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 275 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 282 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 288 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 292 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 296 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 300 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 306 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 310 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 321 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 328 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 340 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 346 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 351 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 356 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 361 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 365 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 370 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 375 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 379 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 382 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 389 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 395 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 406 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 416 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 424 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 430 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 436 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 442 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 447 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 452 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 458 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 463 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 466 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 470 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 480 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 483 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 487 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 496 % 3.59/1.30 === Backtracking. Learning clause 63:2:0:[9.6,6.2,1.2,2.2,5.2,4.2,7.2,3.2,17.2,8.1,30.6,14.1,29.1,15.1,19.1,22.1,28.1,23.1,25.1,26.1,24.1,12.1,16.1,13.1,27.1,21.1,62.2,61.1,55.2]:: six(skc1,skc4) -> patient(skc11,skc17,skc15) % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 516 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 529 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 537 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 545 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 552 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 567 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 574 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 581 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 587 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 592 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 596 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 601 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 605 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 609 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 614 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 618 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 623 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 629 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 635 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 639 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 642 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 645 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 649 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 653 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 656 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 661 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 666 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 672 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 675 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 678 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 682 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 685 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 688 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 699 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 703 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 714 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 719 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 722 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 724 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 726 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 729 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 731 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 733 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 737 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 741 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 745 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 748 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 751 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 759 % 3.59/1.30 === Backtracking. Learning clause 64:3:4:[39.2,32.2,35.2,34.2,31.2,37.2,36.2,33.2,47.2,38.1]:TopTopTopTop: -> ren6(skc11,x0,x1,skc12,skc13),ren8,ren6(skc11,x0,skc14,x2,x3) % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 774 % 3.59/1.30 === Backtracking. Learning clause 69:4:8:[31.1,65.1,34.1,66.3,35.1,67.4,36.1,68.5,32.2,9.2]:TopTopTopTopTopTopTopTop: ren5(x0,x1,x2,x3,x4),patient(x0,x1,x5),from_loc(x0,x1,x6) -> ren2(x0,x5,x7,x2,x6) % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 790 % 3.59/1.30 === Clause set with instances from active satisfied. Growing active. New size: 812 % 3.59/1.30 === Backtracking. Learning clause 70:2:1:[50.1,40.1,41.1]:Top: -> ren8,ren7(skc11,x0,skc14) % 3.59/1.30 === Backtracking. Learning clause 71:2:1:[60.6,64.1,70.2,44.1,54.1,52.1,43.1,57.1,48.1,56.1,53.1,58.1,46.1,45.1,51.1,42.1,59.1,49.1,61.2,62.1]:Top: patient(skc11,skc17,skc15) -> ren3(skc1,x0,skc4) % 3.59/1.30 === Backtracking. Learning clause 72:3:0:[9.6,6.2,1.2,5.2,4.2,2.2,3.2,7.2,17.2,8.1,30.6,28.1,24.1,22.1,13.1,27.1,25.1,29.1,21.1,14.1,26.1,23.1,16.1,19.1,15.1,12.1,61.1]:: six(skc1,skc4),ren3(skc1,skf10(skc1,skc4),skc4),ren8 -> % 3.59/1.30 === Backtracking. Learning clause 75:1:0:[18.0,73.0,62.1,74.1,9.5,5.2,4.2,1.2,7.2,3.2,2.2,6.2,17.2,8.1,30.6,15.1,14.1,21.1,22.1,28.1,26.1,12.1,16.1,29.1,23.1,25.1,13.1,19.1,27.1,24.1]:: -> ren4 % 3.59/1.30 % 3.59/1.30 SZS status Unsatisfiable % 3.59/1.30 % 3.59/1.30 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/1.30 % 3.59/1.30 SPASS-SCL-FOL Statistics: % 3.59/1.30 Number of learned clauses: 8 % 3.59/1.30 Number of propagations: 1011 % 3.59/1.30 Number of decisions: 1958 % 3.59/1.30 Number of resolutions: 132 % 3.59/1.30 Number of condensations: 2 % 3.59/1.30 Number of sub resolutions: 6 % 3.59/1.30 Number of input literals (deduplicated): 69 % 3.59/1.30 Number of grows: 129 % 3.59/1.30 Number of considered ground atoms: 812 % 3.59/1.30 % 3.59/1.30 Needed: 0:00:00.75 % 3.59/1.30 %------------------------------------------------------------------------------