%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP136+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 : n011.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:18 PM UTC 2026 % Result : CounterSatisfiable 5.81s 1.70s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NLP136+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 : n011.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:45:03 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] % 5.81/1.70 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.70 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.70 Execution lmodel_grow ended with status: satisfiable % 5.81/1.70 Used heuristic: lmodel_grow % 5.81/1.70 % 5.81/1.70 Input Clauses: % 5.81/1.70 % 5.81/1.70 Predicates: actual_world of city hollywood_placename placename chevy white dirty old street lonely event agent present barrel down in frontseat member state be two group fellow young ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 % 5.81/1.70 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc12 skc13 skc14 skc15 skc16 skc17 % 5.81/1.70 Fol Functions: skf8 skf9 skf10 skf11 skf18 skf19 skf20 skf21 % 5.81/1.70 Problem Properties: % 5.81/1.70 This is a full first-order problem without equality. % 5.81/1.70 % 5.81/1.70 After reduction: Problem Properties: % 5.81/1.70 This is a full first-order problem without equality. % 5.81/1.70 % 5.81/1.70 % 5.81/1.70 Reduced Input Clauses: % 5.81/1.70 % 5.81/1.70 Most General Atoms: ren1(x0,x1,x2,x3) state(x0,x1) be(x0,x1,x2,x3) ren2(x0,x1) fellow(x0,x1) young(x0,x1) frontseat(x0,x1) member(x0,x1,x2) ren3(x0,x2,x4) ren4(x0,x1,x2) ren5 actual_world(x0) ren6(x0,x1,x2,x3) ren7(x0,x1) ren8(x0,x2,x4) ren9(x0,x1,x2) ren10 of(x0,x1,x2) city(x0,x2) hollywood_placename(x0,x1) placename(x0,x1) chevy(x0,x3) white(x0,x3) dirty(x0,x3) old(x0,x3) street(x0,x4) lonely(x0,x4) event(x0,x5) agent(x0,x5,x3) present(x0,x5) barrel(x0,x5) down(x0,x5,x4) in(x0,x5,x2) two(x0,x6) group(x0,x6) % 5.81/1.70 % 5.81/1.70 === Starting SPASS-SCL-FOL A Little Less Naive, considering 85 atoms initially, heuristics mode: lmodel_grow === % 5.81/1.70 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 98 % 5.81/1.70 === Backtracking. Learning clause 66:4:6:[8.3,3.2]:TopTopTopTopTopTop: state(x0,x1),be(x0,x1,x2,x3),ren1(x0,x4,x2,x3) -> ren3(x0,x2,x5) % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 128 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 135 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 142 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 148 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 155 % 5.81/1.70 === Backtracking. Learning clause 67:4:6:[35.2,40.3]:TopTopTopTopTopTop: ren6(x0,x1,x2,x3),state(x0,x4),be(x0,x4,x2,x3) -> ren8(x0,x2,x5) % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 162 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 166 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 170 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 177 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 185 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 190 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 197 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 204 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 212 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 219 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 226 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 232 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 239 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 246 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 253 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 258 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 263 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 267 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 277 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 281 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 287 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 290 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 295 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 300 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 305 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 310 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 313 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 318 % 5.81/1.70 === Backtracking. Learning clause 69:2:5:[33.1,68.1,34.2,67.3]:TopTopTopTopTop: ren6(x0,x1,x2,x3) -> ren8(x0,x2,x4) % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 333 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 344 % 5.81/1.70 === Backtracking. Learning clause 73:18:5:[43.0,70.0,61.0,71.17,62.0,72.18,60.3,69.1,39.1,38.1,64.18]:TopTopTopTopTop: of(skc12,x0,x1),city(skc12,x1),hollywood_placename(skc12,x0),placename(skc12,x0),chevy(skc12,x2),white(skc12,x2),dirty(skc12,x2),old(skc12,x2),street(skc12,x3),lonely(skc12,x3),event(skc12,x4),agent(skc12,x4,x2),present(skc12,x4),barrel(skc12,x4),down(skc12,x4,x3),in(skc12,x4,x1),ren9(skc12,skf21(skc12,skc17),skc17) -> ren10 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 356 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 366 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 371 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 377 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 385 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 393 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 401 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 408 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 415 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 423 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 431 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 438 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 444 % 5.81/1.70 === Backtracking. Learning clause 74:3:1:[37.1,63.2]:Top: member(skc12,x0,skc17) -> young(skc12,x0),ren10 % 5.81/1.70 === Backtracking. Learning clause 75:1:0:[42.1,36.2,74.2,63.2,41.1,73.17,47.1,52.1,54.1,53.1,50.1,57.1,56.1,55.1,44.1,59.1,46.1,45.1,49.1,58.1,51.1,48.1,65.2,19.2]:: -> old(skc1,skc4) % 5.81/1.70 === Backtracking. Learning clause 76:2:5:[8.1,33.2,35.2,34.2]:TopTopTopTopTop: ren6(x0,x1,x2,x3) -> ren3(x0,x2,x4) % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 456 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 465 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 472 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 479 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 486 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 492 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 498 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 504 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 510 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 516 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 522 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 527 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 532 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 538 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 543 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 549 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 556 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 562 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 568 % 5.81/1.70 === Backtracking. Learning clause 77:3:1:[31.2,5.1]:Top: member(skc1,x0,skc7) -> ren5,young(skc1,x0) % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 583 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 590 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 593 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 606 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 608 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 610 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 614 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 619 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 624 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 626 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 628 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 631 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 633 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 636 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 639 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 640 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 641 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 642 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 643 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 644 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 645 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 646 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 647 % 5.81/1.70 === Clause set with instances from active satisfied. Growing active. New size: 648 % 5.81/1.70 % 5.81/1.70 Linear Model Building succeeded. % 5.81/1.70 SZS status Satisfiable % 5.81/1.70 % 5.81/1.70 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.81/1.70 % 5.81/1.70 SPASS-SCL-FOL Statistics: % 5.81/1.70 Number of learned clauses: 8 % 5.81/1.70 Number of propagations: 663 % 5.81/1.70 Number of decisions: 1650 % 5.81/1.70 Number of resolutions: 35 % 5.81/1.70 Number of condensations: 2 % 5.81/1.70 Number of sub resolutions: 4 % 5.81/1.70 Number of input literals (deduplicated): 85 % 5.81/1.70 Number of grows: 92 % 5.81/1.70 Number of considered ground atoms: 648 % 5.81/1.70 % 5.81/1.70 Needed: 0:00:01.17 % 5.81/1.70 %------------------------------------------------------------------------------