%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO691-1.000 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n029.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:41:18 PM UTC 2026
% Result : Unsatisfiable 1.68s 0.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO691-1.000 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n029.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 13:56:15 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.68/0.88 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.68/0.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.68/0.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.68/0.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.68/0.88 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.68/0.88 Execution resolution_2 ended with status: unsatisfiable
% 1.68/0.88 Used heuristic: resolution_2
% 1.68/0.88
% 1.68/0.88 Input Clauses:
% 1.68/0.88
% 1.68/0.88 Predicates: top seq step
% 1.68/0.88 Fol Constants: a zero
% 1.68/0.88 Fol Functions: f succ
% 1.68/0.88 Problem Properties:
% 1.68/0.88 This is a full first-order problem without equality.
% 1.68/0.88
% 1.68/0.88 After reduction: Problem Properties:
% 1.68/0.88 This is a full first-order problem without equality.
% 1.68/0.88
% 1.68/0.88
% 1.68/0.88 Reduced Input Clauses:
% 1.68/0.88
% 1.68/0.88 Most General Atoms: top(x0,x1) seq(x0,x1,x2) step(x2,x3)
% 1.68/0.88
% 1.68/0.88 === Starting SPASS-SCL-FOL A Little Less Naive, considering 54 atoms initially, heuristics mode: resolution_2 ===
% 1.68/0.88
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 55
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 8:1:3:[3.1,1.1]:TopTopTop: -> step(f(f(x0,x1),f(x2,a)),f(f(x2,f(x1,a)),x0))
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 56
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 9:2:2:[7.3,2.1]:TopTop: seq(succ(succ(zero)),x0,x1),step(x1,x0) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 56
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 10:2:2:[7.1,6.1]:TopTop: step(x0,x1) -> seq(succ(zero),x0,x1)
% 1.68/0.88 === Backtracking. Learning clause 11:3:3:[7.3,9.1,10.2]:TopTopTop: step(x0,x1),step(x1,x2),step(x2,x0) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 64
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 11:3:3:[7.3,9.1,10.2]:TopTopTop: step(x0,x1),step(x1,x2),step(x2,x0) -> {x0 -> f(f(a,f(a,a)),a), x1 -> a, x2 -> f(f(a,a),f(a,a))}
% 1.68/0.88 === Backtracking. Learning clause 12:2:4:[11.3,8.1]:TopTopTopTop: step(f(f(x0,f(x1,a)),x2),x3),step(x3,f(f(x2,x1),f(x0,a))) ->
% 1.68/0.88 === Backtracking. Learning clause 13:2:5:[7.2,8.1]:TopTopTopTopTop: seq(x0,x1,f(f(x2,x3),f(x4,a))) -> seq(succ(x0),x1,f(f(x4,f(x3,a)),x2))
% 1.68/0.88 === Backtracking. Learning clause 14:1:4:[5.1,8.1]:TopTopTopTop: -> step(f(x0,f(f(x1,x2),f(x3,a))),f(x0,f(f(x3,f(x2,a)),x1)))
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 128
% 1.68/0.88 === Backtracking. Learning clause 15:3:4:[3.2,7.2]:TopTopTopTop: top(x0,x1),seq(x2,x3,x0) -> seq(succ(x2),x3,x1)
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 138
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 16:2:6:[7.2,14.1]:TopTopTopTopTopTop: seq(x0,x1,f(x2,f(f(x3,x4),f(x5,a)))) -> seq(succ(x0),x1,f(x2,f(f(x5,f(x4,a)),x3)))
% 1.68/0.88 === Conflict found: 9:2:2:[7.3,2.1]:TopTop: seq(succ(succ(zero)),x0,x1),step(x1,x0) -> {x0 -> f(f(a,f(a,a)),f(f(a,f(a,a)),a)), x1 -> f(f(a,f(a,a)),f(f(a,a),f(a,a)))}
% 1.68/0.88 === Backtracking. Learning clause 17:1:4:[9.2,14.1]:TopTopTopTop: seq(succ(succ(zero)),f(x0,f(f(x1,f(x2,a)),x3)),f(x0,f(f(x3,x2),f(x1,a)))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 144
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 18:2:5:[7.3,17.1,3.2]:TopTopTopTopTop: seq(succ(zero),f(x0,f(f(x1,f(x2,a)),x3)),x4),top(x4,f(x0,f(f(x3,x2),f(x1,a)))) ->
% 1.68/0.88 === Conflict found: 13:2:5:[7.2,8.1]:TopTopTopTopTop: seq(x0,x1,f(f(x2,x3),f(x4,a))) -> seq(succ(x0),x1,f(f(x4,f(x3,a)),x2)) {x0 -> succ(zero), x1 -> f(f(a,f(a,a)),f(f(a,f(f(a,a),a)),a)), x2 -> f(f(a,f(a,a)),f(a,a)), x3 -> a, x4 -> a}
% 1.68/0.88 === Backtracking. Learning clause 19:1:5:[13.2,17.1]:TopTopTopTopTop: seq(succ(zero),f(f(x0,f(x1,a)),f(f(x2,f(x3,a)),x4)),f(f(f(f(x4,x3),f(x2,a)),x1),f(x0,a))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 151
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 20:2:6:[7.3,19.1,3.2]:TopTopTopTopTopTop: seq(zero,f(f(x0,f(x1,a)),f(f(x2,f(x3,a)),x4)),x5),top(x5,f(f(f(f(x4,x3),f(x2,a)),x1),f(x0,a))) ->
% 1.68/0.88 === Conflict found: 16:2:6:[7.2,14.1]:TopTopTopTopTopTop: seq(x0,x1,f(x2,f(f(x3,x4),f(x5,a)))) -> seq(succ(x0),x1,f(x2,f(f(x5,f(x4,a)),x3))) {x0 -> zero, x1 -> f(f(f(a,f(a,a)),f(f(a,a),a)),f(f(a,f(a,a)),a)), x2 -> f(f(f(a,a),f(a,a)),f(a,a)), x3 -> a, x4 -> a, x5 -> a}
% 1.68/0.88 === Backtracking. Learning clause 21:1:6:[16.2,19.1]:TopTopTopTopTopTop: seq(zero,f(f(f(x0,f(x1,a)),f(x2,a)),f(f(x3,f(x4,a)),x5)),f(f(f(f(x5,x4),f(x3,a)),x2),f(f(a,x1),f(x0,a)))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 161
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 22:3:5:[7.2,4.2]:TopTopTopTopTop: seq(x0,x1,f(x2,x3)),step(x2,x4) -> seq(succ(x0),x1,f(x4,x3))
% 1.68/0.88 === Conflict found: 10:2:2:[7.1,6.1]:TopTop: step(x0,x1) -> seq(succ(zero),x0,x1) {x0 -> f(f(a,f(a,a)),a), x1 -> f(a,a)}
% 1.68/0.88 === Backtracking. Learning clause 23:2:3:[10.1,4.2]:TopTopTop: step(x0,x1) -> seq(succ(zero),f(x0,x2),f(x1,x2))
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 225
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 232
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 16:2:6:[7.2,14.1]:TopTopTopTopTopTop: seq(x0,x1,f(x2,f(f(x3,x4),f(x5,a)))) -> seq(succ(x0),x1,f(x2,f(f(x5,f(x4,a)),x3))) {x0 -> succ(zero), x1 -> f(f(a,f(a,a)),f(f(a,f(f(a,a),a)),a)), x2 -> f(a,f(a,a)), x3 -> f(a,a), x4 -> a, x5 -> a}
% 1.68/0.88 === Backtracking. Learning clause 24:1:4:[16.2,17.1]:TopTopTopTop: seq(succ(zero),f(x0,f(f(x1,f(f(x2,a),a)),x3)),f(x0,f(f(f(x1,a),x2),f(x3,a)))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 241
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Backtracking. Learning clause 25:2:5:[7.3,24.1,3.2]:TopTopTopTopTop: seq(zero,f(x0,f(f(x1,f(f(x2,a),a)),x3)),x4),top(x4,f(x0,f(f(f(x1,a),x2),f(x3,a)))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 250
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 23:2:3:[10.1,4.2]:TopTopTop: step(x0,x1) -> seq(succ(zero),f(x0,x2),f(x1,x2)) {x0 -> a, x1 -> f(a,f(a,a)), x2 -> f(f(a,f(a,a)),a)}
% 1.68/0.88 === Backtracking. Learning clause 26:2:5:[23.2,18.1]:TopTopTopTopTop: step(x0,x1),top(f(x1,f(f(x2,f(x3,a)),x4)),f(x0,f(f(x4,x3),f(x2,a)))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 251
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 20:2:6:[7.3,19.1,3.2]:TopTopTopTopTopTop: seq(zero,f(f(x0,f(x1,a)),f(f(x2,f(x3,a)),x4)),x5),top(x5,f(f(f(f(x4,x3),f(x2,a)),x1),f(x0,a))) -> {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> a, x5 -> f(f(a,f(a,a)),f(f(a,f(a,a)),a))}
% 1.68/0.88 === Backtracking. Learning clause 27:1:5:[20.1,6.1]:TopTopTopTopTop: top(f(f(x0,f(x1,a)),f(f(x2,f(x3,a)),x4)),f(f(f(f(x4,x3),f(x2,a)),x1),f(x0,a))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 315
% 1.68/0.88 === Conflict found: 23:2:3:[10.1,4.2]:TopTopTop: step(x0,x1) -> seq(succ(zero),f(x0,x2),f(x1,x2)) {x0 -> a, x1 -> f(a,f(f(a,f(a,a)),a)), x2 -> a}
% 1.68/0.88 === Backtracking. Learning clause 28:3:4:[23.2,22.1]:TopTopTopTop: step(x0,x1),step(x1,x2) -> seq(succ(succ(zero)),f(x0,x3),f(x2,x3))
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 317
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 25:2:5:[7.3,24.1,3.2]:TopTopTopTopTop: seq(zero,f(x0,f(f(x1,f(f(x2,a),a)),x3)),x4),top(x4,f(x0,f(f(f(x1,a),x2),f(x3,a)))) -> {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> f(a,f(f(a,f(f(a,a),a)),a))}
% 1.68/0.88 === Backtracking. Learning clause 29:1:4:[25.1,6.1]:TopTopTopTop: top(f(x0,f(f(x1,f(f(x2,a),a)),x3)),f(x0,f(f(f(x1,a),x2),f(x3,a)))) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 319
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 26:2:5:[23.2,18.1]:TopTopTopTopTop: step(x0,x1),top(f(x1,f(f(x2,f(x3,a)),x4)),f(x0,f(f(x4,x3),f(x2,a)))) -> {x0 -> f(f(a,f(a,a)),f(a,a)), x1 -> f(f(f(a,a),f(a,a)),a), x2 -> a, x3 -> a, x4 -> a}
% 1.68/0.88 === Backtracking. Learning clause 30:1:3:[26.2,1.1]:TopTopTop: step(f(f(x0,f(x1,a)),f(x2,a)),f(f(f(a,x1),f(x0,a)),x2)) ->
% 1.68/0.88 === Clause set with instances from active satisfied. Growing active. New size: 321
% 1.68/0.88 === Restarting.
% 1.68/0.88 === Conflict found: 30:1:3:[26.2,1.1]:TopTopTop: step(f(f(x0,f(x1,a)),f(x2,a)),f(f(f(a,x1),f(x0,a)),x2)) -> {x0 -> f(a,a), x1 -> a, x2 -> f(a,a)}
% 1.68/0.88
% 1.68/0.88 SZS status Unsatisfiable
% 1.68/0.88
% 1.68/0.88 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.68/0.88
% 1.68/0.88 SPASS-SCL-FOL Statistics:
% 1.68/0.88 Number of learned clauses: 23
% 1.68/0.88 Number of propagations: 2147
% 1.68/0.88 Number of decisions: 1121
% 1.68/0.88 Number of resolutions: 28
% 1.68/0.88 Number of condensations: 0
% 1.68/0.88 Number of sub resolutions: 0
% 1.68/0.88 Number of input literals (deduplicated): 9
% 1.68/0.88 Number of grows: 18
% 1.68/0.88 Number of considered ground atoms: 321
% 1.68/0.88
% 1.68/0.88 Needed: 0:00:00.33
% 1.68/0.88
%------------------------------------------------------------------------------