%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PLA001-1 : TPTP v9.2.1. Released v1.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n020.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:31:11 PM UTC 2026 % Result : Unsatisfiable 0.39s 0.96s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PLA001-1 : TPTP v9.2.1. Released v1.0.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 : n020.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.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Thu May 7 12:55:51 EDT 2026 % 0.17/0.35 % CPUTime : % 0.17/0.35 SPASS-SCL-FOL version: % 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.39/0.96 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.96 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.96 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.96 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.96 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.96 Execution lmodel_grow ended with status: unsatisfiable % 0.39/0.96 Used heuristic: lmodel_grow % 0.39/0.96 % 0.39/0.96 Input Clauses: % 0.39/0.96 % 0.39/0.96 Predicates: at next_to % 0.39/0.96 Fol Constants: winnemucca elko saltLakeCity rockSprings laramie cheyenne northPlatte grandIsland lincoln omaha desMoines none start initial_situation % 0.39/0.96 Fol Functions: s drive wait_at buy % 0.39/0.96 Problem Properties: % 0.39/0.96 This is a full first-order problem without equality. % 0.39/0.96 % 0.39/0.96 After reduction: Problem Properties: % 0.39/0.96 This is a full first-order problem without equality. % 0.39/0.96 % 0.39/0.96 % 0.39/0.96 Reduced Input Clauses: % 0.39/0.96 % 0.39/0.96 Most General Atoms: at(x0,x1,x2,x3) next_to(x4,x0) % 0.39/0.96 % 0.39/0.96 === Starting SPASS-SCL-FOL A Little Less Naive, considering 29 atoms initially, heuristics mode: lmodel_grow === % 0.39/0.96 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 35 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 38 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 41 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 42 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 47 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 53 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 58 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 63 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 71 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 78 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 86 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 92 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 97 % 0.39/0.96 === Backtracking. Learning clause 17:2:3:[1.3,16.1]:TopTopTop: at(x0,s(none),x1,x2),next_to(x0,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 105 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 113 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 122 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 129 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 136 % 0.39/0.96 === Backtracking. Learning clause 18:3:4:[2.3,17.1]:TopTopTopTop: at(x0,s(none),x1,x2),next_to(x3,x0),next_to(x3,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 145 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 154 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 164 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 175 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 185 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 194 % 0.39/0.96 === Backtracking. Learning clause 19:3:4:[4.2,18.1]:TopTopTopTop: at(x0,none,x1,x2),next_to(x3,x0),next_to(x3,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 200 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 206 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 211 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 217 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 223 % 0.39/0.96 === Backtracking. Learning clause 20:4:5:[1.3,19.1]:TopTopTopTopTop: at(x0,none,x1,x2),next_to(x0,x3),next_to(x4,x3),next_to(x4,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 228 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 232 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 236 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 242 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 245 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 250 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 257 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 265 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 271 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 277 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 284 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 292 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 298 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 306 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 314 % 0.39/0.96 === Backtracking. Learning clause 21:3:4:[1.3,17.1]:TopTopTopTop: at(x0,s(none),x1,x2),next_to(x0,x3),next_to(x3,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 322 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 330 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 337 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 342 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 347 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 353 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 357 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 362 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 366 % 0.39/0.96 === Backtracking. Learning clause 22:4:5:[1.3,21.1]:TopTopTopTopTop: at(x0,s(none),x1,x2),next_to(x0,x3),next_to(x3,x4),next_to(x4,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 374 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 380 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 384 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 389 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 394 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 401 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 408 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 414 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 422 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 429 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 437 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 444 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 452 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 460 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 468 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 475 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 480 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 488 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 495 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 502 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 510 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 517 % 0.39/0.96 === Backtracking. Learning clause 23:6:7:[1.1,1.3,20.1]:TopTopTopTopTopTopTop: next_to(x0,x1),at(x2,none,x3,x4),next_to(x2,x0),next_to(x1,x5),next_to(x6,x5),next_to(x6,desMoines) -> % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 523 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 526 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 531 % 0.39/0.96 === Clause set with instances from active satisfied. Growing active. New size: 536 % 0.39/0.96 % 0.39/0.96 SZS status Unsatisfiable % 0.39/0.96 % 0.39/0.96 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.96 % 0.39/0.96 SPASS-SCL-FOL Statistics: % 0.39/0.96 Number of learned clauses: 7 % 0.39/0.96 Number of propagations: 1018 % 0.39/0.96 Number of decisions: 1257 % 0.39/0.96 Number of resolutions: 16 % 0.39/0.96 Number of condensations: 0 % 0.39/0.96 Number of sub resolutions: 0 % 0.39/0.96 Number of input literals (deduplicated): 17 % 0.39/0.96 Number of grows: 79 % 0.39/0.96 Number of considered ground atoms: 536 % 0.39/0.96 % 0.39/0.96 Needed: 0:00:00.39 % 0.39/0.96 %------------------------------------------------------------------------------