%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN549+1 : TPTP v9.2.1. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:40:00 PM UTC 2026
% Result : Theorem 1.61s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN549+1 : TPTP v9.2.1. Released v2.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n010.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 13:45:37 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.21/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.61/0.84 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/0.84 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/0.84 Execution resolution_2 ended with status: unsatisfiable
% 1.61/0.84 Used heuristic: resolution_2
% 1.61/0.84
% 1.61/0.84 Input Clauses:
% 1.61/0.84
% 1.61/0.84 Predicates: reachable p q ren1 ren2 ren3 ren4 ren5 ren6
% 1.61/0.84 Fol Constants: initial_world
% 1.61/0.84 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8
% 1.61/0.84 Problem Properties:
% 1.61/0.84 This is a full first-order problem without equality.
% 1.61/0.84
% 1.61/0.84 After reduction: Problem Properties:
% 1.61/0.84 This is a full first-order problem without equality.
% 1.61/0.84
% 1.61/0.84
% 1.61/0.84 Reduced Input Clauses:
% 1.61/0.84
% 1.61/0.84 Most General Atoms: reachable(x0,x2) ren1(x0,x1) q(x1) p(x1) ren5(x0) ren2(x1) ren3(x0,x2) ren4(x0,x2) ren6(x1,x0)
% 1.61/0.84
% 1.61/0.84 === Starting SPASS-SCL-FOL A Little Less Naive, considering 63 atoms initially, heuristics mode: resolution_2 ===
% 1.61/0.84
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 63
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 27:2:1:[11.1,1.1]:Top: p(x0) -> ren3(x0,x0)
% 1.61/0.84 === Backtracking. Learning clause 28:2:1:[5.1,1.1]:Top: q(x0) -> ren1(x0,x0)
% 1.61/0.84 === Backtracking. Learning clause 29:1:0:[26.1,1.1]:: ren6(initial_world,skf8(initial_world)) ->
% 1.61/0.84 === Backtracking. Learning clause 30:3:1:[14.2,4.2,3.2,6.3]:Top: ren2(x0) -> ren4(x0,skf1(x0)),p(x0)
% 1.61/0.84 === Backtracking. Learning clause 31:4:2:[15.4,16.2,18.2]:TopTop: reachable(x0,x1),ren2(x1),ren5(x0) -> reachable(x0,skf4(x0))
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 65
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 32:1:0:[24.2,29.1]:: -> reachable(initial_world,skf8(initial_world))
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 73
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 33:2:0:[11.1,32.1]:: p(skf8(initial_world)) -> ren3(initial_world,skf8(initial_world))
% 1.61/0.84 === Backtracking. Learning clause 34:3:1:[21.1,32.1]:Top: ren2(skf8(initial_world)),ren4(initial_world,x0) -> ren5(initial_world)
% 1.61/0.84 === Backtracking. Learning clause 35:3:1:[20.1,32.1]:Top: ren2(skf8(initial_world)),ren3(initial_world,x0) -> ren5(initial_world)
% 1.61/0.84 === Backtracking. Learning clause 36:2:0:[14.1,32.1]:: q(skf8(initial_world)) -> ren4(initial_world,skf8(initial_world))
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 73
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 37:4:4:[8.2,20.2]:TopTopTopTop: ren1(x0,x1),reachable(x2,x0),ren3(x2,x3) -> ren5(x2)
% 1.61/0.84 === Backtracking. Learning clause 38:4:3:[23.3,21.3,20.3,25.1]:TopTopTop: reachable(x0,x1),ren2(x1) -> ren2(skf5(x0)),ren6(x2,x0)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 137
% 1.61/0.84 === Conflict found: 28:2:1:[5.1,1.1]:Top: q(x0) -> ren1(x0,x0) {x0 -> skf1(initial_world)}
% 1.61/0.84 === Backtracking. Learning clause 39:2:1:[28.2,8.1]:Top: q(x0) -> ren2(x0)
% 1.61/0.84 === Backtracking. Learning clause 40:4:3:[17.1,20.4]:TopTopTop: reachable(x0,x1),ren2(x1),ren3(x0,x2) -> ren2(skf4(x0))
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 137
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 41:4:2:[6.2,11.2,3.1]:TopTop: ren2(x0),reachable(x1,x0) -> ren3(x1,x0),reachable(x0,skf1(x0))
% 1.61/0.84 === Backtracking. Learning clause 42:7:3:[14.3,21.3,41.4]:TopTopTop: q(skf1(x0)),reachable(x0,x1),ren2(x1),ren2(x0),reachable(x2,x0) -> ren5(x0),ren3(x2,x0)
% 1.61/0.84 === Conflict found: 42:7:3:[14.3,21.3,41.4]:TopTopTop: q(skf1(x0)),reachable(x0,x1),ren2(x1),ren2(x0),reachable(x2,x0) -> ren5(x0),ren3(x2,x0) {x0 -> initial_world, x1 -> initial_world, x2 -> initial_world}
% 1.61/0.84 === Backtracking. Learning clause 43:7:3:[42.7,20.3]:TopTopTop: q(skf1(x0)),reachable(x0,x1),ren2(x1),ren2(x0),reachable(x2,x0) -> ren5(x0),ren5(x2)
% 1.61/0.84 === Backtracking. Learning clause 44:6:3:[11.2,6.2,20.3,4.1,43.1]:TopTopTop: reachable(x0,x1),ren2(x1),ren2(x0),reachable(x2,x0) -> ren5(x0),ren5(x2)
% 1.61/0.84 === Backtracking. Learning clause 45:5:4:[11.3,37.3]:TopTopTopTop: reachable(x0,x1),p(x1),ren1(x2,x3),reachable(x0,x2) -> ren5(x0)
% 1.61/0.84 === Backtracking. Learning clause 46:5:4:[20.4,25.1,11.3]:TopTopTopTop: reachable(x0,x1),ren2(x1),reachable(x0,x2),p(x2) -> ren6(x3,x0)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 140
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 47:3:1:[7.2,20.2,10.2,1.1,33.2]:Top: ren3(x0,initial_world),p(skf8(initial_world)) -> ren5(initial_world)
% 1.61/0.84 === Conflict found: 39:2:1:[28.2,8.1]:Top: q(x0) -> ren2(x0) {x0 -> initial_world}
% 1.61/0.84 === Backtracking. Learning clause 48:2:2:[39.1,13.2,44.2,1.1]:TopTop: ren4(x0,x1) -> ren5(x1)
% 1.61/0.84 === Conflict found: 46:5:4:[20.4,25.1,11.3]:TopTopTopTop: reachable(x0,x1),ren2(x1),reachable(x0,x2),p(x2) -> ren6(x3,x0) {x0 -> skf8(initial_world), x1 -> initial_world, x2 -> initial_world, x3 -> initial_world}
% 1.61/0.84 === Backtracking. Learning clause 49:4:2:[46.5,29.1]:TopTop: reachable(skf8(initial_world),x0),ren2(x0),reachable(skf8(initial_world),x1),p(x1) ->
% 1.61/0.84 === Conflict found: 49:4:2:[46.5,29.1]:TopTop: reachable(skf8(initial_world),x0),ren2(x0),reachable(skf8(initial_world),x1),p(x1) -> {x0 -> skf8(initial_world), x1 -> skf8(initial_world)}
% 1.61/0.84 === Backtracking. Learning clause 50:1:0:[49.1,1.1,7.2]:: p(skf8(initial_world)) ->
% 1.61/0.84 === Backtracking. Learning clause 51:3:4:[7.2,46.2,10.2]:TopTopTopTop: reachable(x0,x1),ren3(x2,x1) -> ren6(x3,x0)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 140
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 52:2:0:[6.2,50.1]:: ren2(skf8(initial_world)) -> ren1(skf8(initial_world),skf1(skf8(initial_world)))
% 1.61/0.84 === Conflict found: 44:6:3:[11.2,6.2,20.3,4.1,43.1]:TopTopTop: reachable(x0,x1),ren2(x1),ren2(x0),reachable(x2,x0) -> ren5(x0),ren5(x2) {x0 -> skf8(initial_world), x1 -> skf8(initial_world), x2 -> skf8(initial_world)}
% 1.61/0.84 === Backtracking. Learning clause 53:1:0:[44.5,25.1,1.1,29.1]:: ren2(skf8(initial_world)) ->
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 140
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 54:1:1:[8.2,53.1]:Top: ren1(skf8(initial_world),x0) ->
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 204
% 1.61/0.84 === Backtracking. Learning clause 55:3:2:[8.1,5.3]:TopTop: reachable(x0,x1),q(x1) -> ren2(x0)
% 1.61/0.84 === Backtracking. Learning clause 56:5:2:[5.2,13.2,12.2,15.5,10.1,7.1]:TopTop: ren5(x0),reachable(x0,x1),ren2(x1) -> ren1(x0,skf3(x0)),ren2(skf2(x0))
% 1.61/0.84 === Backtracking. Learning clause 57:2:2:[5.1,12.2,13.2]:TopTop: ren4(x0,x1) -> ren1(x0,x1)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 205
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Conflict found: 55:3:2:[8.1,5.3]:TopTop: reachable(x0,x1),q(x1) -> ren2(x0) {x0 -> skf8(initial_world), x1 -> skf1(skf8(initial_world))}
% 1.61/0.84 === Backtracking. Learning clause 58:2:2:[55.2,13.2,12.2]:TopTop: ren4(x0,x1) -> ren2(x0)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 205
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 59:3:2:[3.2,11.1,57.2]:TopTop: p(x0),ren4(x1,x0) -> ren3(x1,x0)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 205
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 60:2:1:[25.1,48.2,29.1,14.3]:Top: reachable(x0,skf8(initial_world)),q(skf8(initial_world)) ->
% 1.61/0.84 === Backtracking. Learning clause 61:4:2:[15.3,17.3,16.3]:TopTop: ren5(x0),ren3(x0,x1) -> ren3(x0,skf2(x0)),ren4(x0,skf3(x0))
% 1.61/0.84 === Backtracking. Learning clause 62:3:4:[2.3,51.1,9.2]:TopTopTopTop: reachable(x0,x1),ren3(x1,x2) -> ren6(x3,x0)
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 205
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 63:1:0:[25.2,29.1]:: ren5(skf8(initial_world)) ->
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 269
% 1.61/0.84 === Conflict found: 44:6:3:[11.2,6.2,20.3,4.1,43.1]:TopTopTop: reachable(x0,x1),ren2(x1),ren2(x0),reachable(x2,x0) -> ren5(x0),ren5(x2) {x0 -> skf6(initial_world), x1 -> skf6(initial_world), x2 -> skf6(initial_world)}
% 1.61/0.84 === Backtracking. Learning clause 64:2:1:[44.1,1.1]:Top: ren2(x0) -> ren5(x0)
% 1.61/0.84 === Backtracking. Learning clause 65:4:2:[15.4,40.3,19.2]:TopTop: reachable(x0,x1),ren2(x1),ren5(x0) -> ren2(skf4(x0))
% 1.61/0.84 === Clause set with instances from active satisfied. Growing active. New size: 272
% 1.61/0.84 === Restarting.
% 1.61/0.84 === Backtracking. Learning clause 66:4:3:[10.2,49.4]:TopTopTop: ren3(x0,x1),reachable(skf8(initial_world),x2),ren2(x2),reachable(skf8(initial_world),x1) ->
% 1.61/0.84 === Backtracking. Learning clause 67:8:4:[2.3,2.2,9.2,66.4,15.4,12.1]:TopTopTopTop: reachable(x0,x1),reachable(skf8(initial_world),x0),reachable(skf8(initial_world),x2),ren2(x2),ren5(x1),reachable(x1,x3),ren2(x3) -> reachable(x1,skf3(x1))
% 1.61/0.84 === Backtracking. Learning clause 68:4:2:[2.3,55.1,41.4,4.2,6.3,66.1,49.4]:TopTop: reachable(x0,x1),ren2(x1),reachable(skf8(initial_world),x1) -> ren2(x0)
% 1.61/0.84 === Conflict found: 68:4:2:[2.3,55.1,41.4,4.2,6.3,66.1,49.4]:TopTop: reachable(x0,x1),ren2(x1),reachable(skf8(initial_world),x1) -> ren2(x0) {x0 -> skf8(initial_world), x1 -> skf5(skf8(initial_world))}
% 1.61/0.84
% 1.61/0.84 SZS status Unsatisfiable
% 1.61/0.84
% 1.61/0.84 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/0.84
% 1.61/0.84 SPASS-SCL-FOL Statistics:
% 1.61/0.84 Number of learned clauses: 42
% 1.61/0.84 Number of propagations: 2472
% 1.61/0.84 Number of decisions: 1193
% 1.61/0.84 Number of resolutions: 91
% 1.61/0.84 Number of condensations: 10
% 1.61/0.84 Number of sub resolutions: 0
% 1.61/0.84 Number of input literals (deduplicated): 21
% 1.61/0.84 Number of grows: 16
% 1.61/0.84 Number of considered ground atoms: 272
% 1.61/0.84
% 1.61/0.84 Needed: 0:00:00.30
% 1.61/0.84
%------------------------------------------------------------------------------