%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PUZ008-3 : TPTP v9.2.1. Released v1.2.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:31:23 PM UTC 2026
% Result : Unsatisfiable 0.86s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PUZ008-3 : TPTP v9.2.1. Released v1.2.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 : n028.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:58:01 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.17/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.86/0.65 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/0.65 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/0.65 Execution resolution_1 ended with status: unsatisfiable
% 0.86/0.65 Used heuristic: resolution_1
% 0.86/0.65
% 0.86/0.65 Input Clauses:
% 0.86/0.65
% 0.86/0.65 Predicates: safe greater_or_equal achievable
% 0.86/0.65 Fol Constants: n0 boatonwest boatoneast
% 0.86/0.65 Fol Functions: s m c west east
% 0.86/0.65 Problem Properties:
% 0.86/0.65 This is a full first-order problem without equality.
% 0.86/0.65
% 0.86/0.65 After reduction: Problem Properties:
% 0.86/0.65 This is a full first-order problem without equality.
% 0.86/0.65
% 0.86/0.65
% 0.86/0.65 Reduced Input Clauses:
% 0.86/0.65
% 0.86/0.65 Most General Atoms: greater_or_equal(x0,x1) achievable(west(m(x0),c(s(x1))),boatonwest,east(m(x2),c(x3))) achievable(west(m(x0),c(x1)),boatoneast,east(m(x2),c(s(x3)))) safe(x2,x3) achievable(west(m(s(x0)),c(x1)),boatonwest,east(m(x2),c(x3))) achievable(west(m(x0),c(x1)),boatoneast,east(m(s(x2)),c(x3))) achievable(west(m(n0),c(n0)),x0,east(m(s(s(s(n0)))),c(s(s(s(n0))))))
% 0.86/0.65
% 0.86/0.65 === Starting SPASS-SCL-FOL A Little Less Naive, considering 46 atoms initially, heuristics mode: resolution_1 ===
% 0.86/0.65
% 0.86/0.65 === Backtracking. Learning clause 17:2:2:[2.1,4.2]:TopTop: greater_or_equal(x0,x1) -> safe(s(x0),s(x1))
% 0.86/0.65 === Backtracking. Learning clause 18:6:4:[6.4,7.1]:TopTopTopTop: achievable(west(m(x0),c(s(x1))),boatoneast,east(m(x2),c(s(x3)))),safe(x0,s(s(x1))),safe(x2,x3),safe(x0,x1),safe(x2,s(s(x3))) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(x2),c(s(s(x3)))))
% 0.86/0.65 === Backtracking. Learning clause 19:6:4:[6.4,13.1]:TopTopTopTop: achievable(west(m(s(x0)),c(x1)),boatoneast,east(m(x2),c(s(x3)))),safe(s(x0),s(x1)),safe(x2,x3),safe(x0,x1),safe(s(x2),s(x3)) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(s(x2)),c(s(x3))))
% 0.86/0.65 === Backtracking. Learning clause 20:6:4:[10.4,11.1]:TopTopTopTop: achievable(west(m(s(x0)),c(x1)),boatoneast,east(m(s(x2)),c(x3))),safe(s(s(x0)),x1),safe(x2,x3),safe(x0,x1),safe(s(s(x2)),x3) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(s(s(x2))),c(x3)))
% 0.86/0.65 === Backtracking. Learning clause 21:6:4:[8.4,13.1]:TopTopTopTop: achievable(west(m(s(x0)),c(x1)),boatoneast,east(m(x2),c(s(s(x3))))),safe(s(x0),s(s(x1))),safe(x2,x3),safe(x0,s(x1)),safe(s(x2),s(x3)) -> achievable(west(m(x0),c(s(x1))),boatoneast,east(m(s(x2)),c(s(x3))))
% 0.86/0.65 === Backtracking. Learning clause 22:6:4:[8.4,11.1]:TopTopTopTop: achievable(west(m(s(s(x0))),c(x1)),boatoneast,east(m(x2),c(s(s(x3))))),safe(s(s(x0)),s(s(x1))),safe(x2,x3),safe(x0,s(s(x1))),safe(s(s(x2)),x3) -> achievable(west(m(x0),c(s(s(x1)))),boatoneast,east(m(s(s(x2))),c(x3)))
% 0.86/0.65 === Backtracking. Learning clause 23:3:0:[5.1,15.1]:: safe(s(s(s(n0))),s(s(n0))),safe(n0,s(n0)) -> achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatoneast,east(m(n0),c(s(n0))))
% 0.86/0.65 === Backtracking. Learning clause 24:3:0:[9.1,15.1]:: safe(s(s(n0)),s(s(s(n0)))),safe(s(n0),n0) -> achievable(west(m(s(s(n0))),c(s(s(s(n0))))),boatoneast,east(m(s(n0)),c(n0)))
% 0.86/0.65 === Backtracking. Learning clause 25:3:0:[7.1,15.1]:: safe(s(s(s(n0))),s(n0)),safe(n0,s(s(n0))) -> achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0)))))
% 0.86/0.65 === Backtracking. Learning clause 26:3:0:[13.1,15.1]:: safe(s(s(n0)),s(s(n0))),safe(s(n0),s(n0)) -> achievable(west(m(s(s(n0))),c(s(s(n0)))),boatoneast,east(m(s(n0)),c(s(n0))))
% 0.86/0.65 === Backtracking. Learning clause 27:3:0:[11.1,15.1]:: safe(s(n0),s(s(s(n0)))),safe(s(s(n0)),n0) -> achievable(west(m(s(n0)),c(s(s(s(n0))))),boatoneast,east(m(s(s(n0))),c(n0)))
% 0.86/0.65 === Clause set with instances from active satisfied. Growing active. New size: 53
% 0.86/0.65 === Restarting.
% 0.86/0.65 === Clause set with instances from active satisfied. Growing active. New size: 117
% 0.86/0.65 === Backtracking. Learning clause 28:1:1:[2.1,3.1]:Top: -> safe(x0,n0)
% 0.86/0.65 === Clause set with instances from active satisfied. Growing active. New size: 181
% 0.86/0.65 === Conflict found: 18:6:4:[6.4,7.1]:TopTopTopTop: achievable(west(m(x0),c(s(x1))),boatoneast,east(m(x2),c(s(x3)))),safe(x0,s(s(x1))),safe(x2,x3),safe(x0,x1),safe(x2,s(s(x3))) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(x2),c(s(s(x3))))) {x0 -> s(n0), x1 -> n0, x2 -> s(s(n0)), x3 -> s(n0)}
% 0.86/0.65 === Backtracking. Learning clause 29:10:4:[18.1,11.4,19.1]:TopTopTopTop: safe(s(x0),s(s(x1))),safe(s(s(x2)),x3),safe(s(x0),x1),safe(s(s(x2)),s(s(x3))),achievable(west(m(s(s(s(x0)))),c(s(x1))),boatonwest,east(m(x2),c(s(x3)))),safe(s(x0),s(x1)),safe(s(s(x2)),s(x3)),safe(x0,x1),safe(s(s(s(x2))),s(s(x3))) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(s(s(s(x2)))),c(s(s(x3)))))
% 0.86/0.65 === Conflict found: 20:6:4:[10.4,11.1]:TopTopTopTop: achievable(west(m(s(x0)),c(x1)),boatoneast,east(m(s(x2)),c(x3))),safe(s(s(x0)),x1),safe(x2,x3),safe(x0,x1),safe(s(s(x2)),x3) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(s(s(x2))),c(x3))) {x0 -> n0, x1 -> s(n0), x2 -> s(n0), x3 -> s(s(n0))}
% 0.86/0.65 === Backtracking. Learning clause 30:12:4:[20.6,18.1,11.4]:TopTopTopTop: safe(s(s(x0)),s(x1)),safe(s(x2),s(x3)),safe(x0,s(x1)),safe(s(s(s(x2))),s(x3)),safe(x0,s(s(x1))),safe(s(s(s(x2))),x3),safe(x0,x1),safe(s(s(s(x2))),s(s(x3))),achievable(west(m(s(s(s(x0)))),c(s(x1))),boatonwest,east(m(x2),c(s(x3)))),safe(s(x0),s(x1)),safe(s(s(x2)),s(x3)) -> achievable(west(m(x0),c(x1)),boatoneast,east(m(s(s(s(x2)))),c(s(s(x3)))))
% 0.86/0.65
% 0.86/0.65 SZS status Unsatisfiable
% 0.86/0.65
% 0.86/0.65 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/0.65
% 0.86/0.65 SPASS-SCL-FOL Statistics:
% 0.86/0.65 Number of learned clauses: 14
% 0.86/0.65 Number of propagations: 301
% 0.86/0.65 Number of decisions: 186
% 0.86/0.65 Number of resolutions: 41
% 0.86/0.65 Number of condensations: 0
% 0.86/0.65 Number of sub resolutions: 0
% 0.86/0.65 Number of input literals (deduplicated): 22
% 0.86/0.65 Number of grows: 3
% 0.86/0.65 Number of considered ground atoms: 181
% 0.86/0.65
% 0.86/0.65 Needed: 0:00:00.11
% 0.86/0.65
%------------------------------------------------------------------------------