%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO630-1 : TPTP v9.2.1. Released v7.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:13 PM UTC 2026
% Result : Unsatisfiable 0.38s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO630-1 : TPTP v9.2.1. Released v7.1.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n015.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:55:02 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.23/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.38/0.59 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.59 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.59 Execution resolution_2 ended with status: unsatisfiable
% 0.38/0.59 Used heuristic: resolution_2
% 0.38/0.59
% 0.38/0.59 Input Clauses:
% 0.38/0.59
% 0.38/0.59 Predicates: 'E' 'LE' iLEQ
% 0.38/0.59 Fol Constants: '0'
% 0.38/0.59 Fol Functions: s f g
% 0.38/0.59 Problem Properties:
% 0.38/0.59 This is a full first-order problem without equality.
% 0.38/0.59
% 0.38/0.59 After reduction: Problem Properties:
% 0.38/0.59 This is a full first-order problem without equality.
% 0.38/0.59
% 0.38/0.59
% 0.38/0.59 Reduced Input Clauses:
% 0.38/0.59 39:2:1:[31.0,30.2]:Top: 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s(s('0')))),f(g(x0))) ->
% 0.38/0.59 33:3:2:[7.0,6.3]:TopTop: 'LE'(f(x0),s('0')),iLEQ(x0,x1) -> 'E'('0',f(x1))
% 0.38/0.59 38:2:1:[26.0,24.2]:Top: 'E'('0',f(x0)),'E'('0',f(g(x0))) ->
% 0.38/0.59 34:2:1:[21.0,10.2]:Top: 'E'(s(s(s(s(s('0'))))),f(x0)),'E'(s(s(s(s(s('0'))))),f(g(x0))) ->
% 0.38/0.59 35:2:1:[21.0,11.2]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(g(x0))) ->
% 0.38/0.59 36:2:1:[21.0,12.2]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(g(x0))) ->
% 0.38/0.59 37:2:1:[21.0,13.2]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(g(x0))) ->
% 0.38/0.59
% 0.38/0.59 Most General Atoms: 'E'(s(s(s(s(s('0'))))),f(x0)) 'LE'(f(x0),s(s(s(s(s('0')))))) iLEQ(x0,x1) 'E'(f(x0),f(g(x0))) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0') 'E'('0',f(x0)) 'E'(s('0'),f(x0)) 'E'(s(s(s('0'))),f(x1)) 'LE'(f(x0),s(s(s('0')))) 'E'(s(s('0')),f(x1)) 'LE'(f(x1),s(s('0'))) 'E'(s(s(s(s('0')))),f(x1)) 'LE'(f(x1),s(s(s(s('0')))))
% 0.38/0.59
% 0.38/0.59 === Starting SPASS-SCL-FOL A Little Less Naive, considering 66 atoms initially, heuristics mode: resolution_2 ===
% 0.38/0.59
% 0.38/0.59 === Clause set with instances from active satisfied. Growing active. New size: 70
% 0.38/0.59 === Restarting.
% 0.38/0.59 === Backtracking. Learning clause 40:3:1:[32.2,25.1]:Top: 'LE'(f(x0),s(s('0'))) -> 'E'(s('0'),f(g(x0))),'LE'(f(g(x0)),s('0'))
% 0.38/0.59 === Backtracking. Learning clause 41:3:1:[17.2,25.1]:Top: 'LE'(f(x0),s(s(s(s('0'))))) -> 'E'(s(s(s('0'))),f(g(x0))),'LE'(f(g(x0)),s(s(s('0'))))
% 0.38/0.59 === Backtracking. Learning clause 42:3:1:[16.2,25.1]:Top: 'LE'(f(x0),s(s(s(s(s('0')))))) -> 'E'(s(s(s(s('0')))),f(g(x0))),'LE'(f(g(x0)),s(s(s(s('0')))))
% 0.38/0.59 === Backtracking. Learning clause 43:3:1:[15.2,25.1]:Top: 'LE'(f(x0),s(s(s('0')))) -> 'E'(s(s('0')),f(g(x0))),'LE'(f(g(x0)),s(s('0')))
% 0.38/0.59 === Conflict found: 33:3:2:[7.0,6.3]:TopTop: 'LE'(f(x0),s('0')),iLEQ(x0,x1) -> 'E'('0',f(x1)) {x0 -> '0', x1 -> g('0')}
% 0.38/0.59 === Backtracking. Learning clause 44:2:1:[33.2,25.1]:Top: 'LE'(f(x0),s('0')) -> 'E'('0',f(g(x0)))
% 0.38/0.59 === Conflict found: 33:3:2:[7.0,6.3]:TopTop: 'LE'(f(x0),s('0')),iLEQ(x0,x1) -> 'E'('0',f(x1)) {x0 -> '0', x1 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 45:1:1:[33.2,29.1,38.1,44.2]:Top: 'LE'(f(x0),s('0')) ->
% 0.38/0.59 === Conflict found: 37:2:1:[21.0,13.2]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(g(x0))) -> {x0 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 47:11:5:[45.0,46.8,37.2,32.3,32.3,15.4,17.4,35.1,17.3,16.4,1.2,34.1]:TopTopTopTopTop: iLEQ(x0,g(x1)),iLEQ(x0,x1),iLEQ(x2,x0),iLEQ(x3,x2),iLEQ(x3,g(x2)),iLEQ(x4,x3),'E'(s(s(s(s(s('0'))))),f(g(x4))) -> 'LE'(f(g(x1)),s('0')),'E'(s(s('0')),f(x0)),'LE'(f(g(x2)),s(s(s('0')))),'E'(s(s(s(s('0')))),f(x3))
% 0.38/0.59 === Clause set with instances from active satisfied. Growing active. New size: 70
% 0.38/0.59 === Restarting.
% 0.38/0.59 === Conflict found: 47:11:5:[45.0,46.8,37.2,32.3,32.3,15.4,17.4,35.1,17.3,16.4,1.2,34.1]:TopTopTopTopTop: iLEQ(x0,g(x1)),iLEQ(x0,x1),iLEQ(x2,x0),iLEQ(x3,x2),iLEQ(x3,g(x2)),iLEQ(x4,x3),'E'(s(s(s(s(s('0'))))),f(g(x4))) -> 'LE'(f(g(x1)),s('0')),'E'(s(s('0')),f(x0)),'LE'(f(g(x2)),s(s(s('0')))),'E'(s(s(s(s('0')))),f(x3)) {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0', x4 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 48:10:5:[47.8,45.1]:TopTopTopTopTop: iLEQ(x0,g(x1)),iLEQ(x0,x1),iLEQ(x2,x0),iLEQ(x3,x2),iLEQ(x3,g(x2)),iLEQ(x4,x3),'E'(s(s(s(s(s('0'))))),f(g(x4))) -> 'E'(s(s('0')),f(x0)),'LE'(f(g(x2)),s(s(s('0')))),'E'(s(s(s(s('0')))),f(x3))
% 0.38/0.59 === Backtracking. Learning clause 49:2:1:[32.4,45.1,25.1]:Top: 'LE'(f(x0),s(s('0'))) -> 'E'(s('0'),f(g(x0)))
% 0.38/0.59 === Backtracking. Learning clause 50:1:1:[32.2,29.1,45.1,37.1,49.2]:Top: 'LE'(f(x0),s(s('0'))) ->
% 0.38/0.59 === Conflict found: 36:2:1:[21.0,12.2]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(g(x0))) -> {x0 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 53:4:3:[50.0,51.4,50.0,52.5,36.1,15.3,15.3]:TopTopTop: 'LE'(f(x0),s(s(s('0')))),iLEQ(x0,x1),'LE'(f(x2),s(s(s('0')))),iLEQ(x2,g(x1)) ->
% 0.38/0.59 === Clause set with instances from active satisfied. Growing active. New size: 70
% 0.38/0.59 === Restarting.
% 0.38/0.59 === Backtracking. Learning clause 54:2:1:[15.4,50.1,25.1]:Top: 'LE'(f(x0),s(s(s('0')))) -> 'E'(s(s('0')),f(g(x0)))
% 0.38/0.59 === Conflict found: 53:4:3:[50.0,51.4,50.0,52.5,36.1,15.3,15.3]:TopTopTop: 'LE'(f(x0),s(s(s('0')))),iLEQ(x0,x1),'LE'(f(x2),s(s(s('0')))),iLEQ(x2,g(x1)) -> {x0 -> '0', x1 -> '0', x2 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 55:1:1:[53.2,29.1,25.1]:Top: 'LE'(f(x0),s(s(s('0')))) ->
% 0.38/0.59 === Clause set with instances from active satisfied. Growing active. New size: 70
% 0.38/0.59 === Restarting.
% 0.38/0.59 === Conflict found: 47:11:5:[45.0,46.8,37.2,32.3,32.3,15.4,17.4,35.1,17.3,16.4,1.2,34.1]:TopTopTopTopTop: iLEQ(x0,g(x1)),iLEQ(x0,x1),iLEQ(x2,x0),iLEQ(x3,x2),iLEQ(x3,g(x2)),iLEQ(x4,x3),'E'(s(s(s(s(s('0'))))),f(g(x4))) -> 'LE'(f(g(x1)),s('0')),'E'(s(s('0')),f(x0)),'LE'(f(g(x2)),s(s(s('0')))),'E'(s(s(s(s('0')))),f(x3)) {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0', x4 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 56:9:5:[47.10,55.1,45.1]:TopTopTopTopTop: iLEQ(x0,g(x1)),iLEQ(x0,x1),iLEQ(x2,x0),iLEQ(x3,x2),iLEQ(x3,g(x2)),iLEQ(x4,x3),'E'(s(s(s(s(s('0'))))),f(g(x4))) -> 'E'(s(s('0')),f(x0)),'E'(s(s(s(s('0')))),f(x3))
% 0.38/0.59 === Backtracking. Learning clause 57:2:1:[17.4,55.1,25.1]:Top: 'LE'(f(x0),s(s(s(s('0'))))) -> 'E'(s(s(s('0'))),f(g(x0)))
% 0.38/0.59 === Conflict found: 35:2:1:[21.0,11.2]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(g(x0))) -> {x0 -> '0'}
% 0.38/0.59 === Backtracking. Learning clause 58:1:1:[35.1,17.3,57.2,29.1,55.1]:Top: 'LE'(f(x0),s(s(s(s('0'))))) ->
% 0.38/0.59 === Clause set with instances from active satisfied. Growing active. New size: 134
% 0.38/0.59 === Conflict found: 42:3:1:[16.2,25.1]:Top: 'LE'(f(x0),s(s(s(s(s('0')))))) -> 'E'(s(s(s(s('0')))),f(g(x0))),'LE'(f(g(x0)),s(s(s(s('0'))))) {x0 -> s('0')}
% 0.38/0.59 === Backtracking. Learning clause 61:1:1:[29.0,59.0,58.0,60.2,42.3,58.1,39.2,16.3,1.2,34.1]:Top: 'E'(s(s(s(s(s('0'))))),f(g(x0))) ->
% 0.38/0.59 === Backtracking. Learning clause 63:2:1:[58.0,62.1,16.2,29.1,1.2]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s(s(s('0'))))),f(x0))
% 0.38/0.59 === Clause set with instances from active satisfied. Growing active. New size: 134
% 0.38/0.59 === Restarting.
% 0.38/0.59 === Conflict found: 63:2:1:[58.0,62.1,16.2,29.1,1.2]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s(s(s('0'))))),f(x0)) {x0 -> g('0')}
% 0.38/0.59 === Backtracking. Learning clause 64:1:1:[63.2,61.1]:Top: -> 'E'(s(s(s(s('0')))),f(g(x0)))
% 0.38/0.59 === Conflict found: 39:2:1:[31.0,30.2]:Top: 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s(s('0')))),f(g(x0))) -> {x0 -> g('0')}
% 0.38/0.59
% 0.38/0.59 SZS status Unsatisfiable
% 0.38/0.59
% 0.38/0.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.59
% 0.38/0.59 SPASS-SCL-FOL Statistics:
% 0.38/0.59 Number of learned clauses: 19
% 0.38/0.59 Number of propagations: 498
% 0.38/0.59 Number of decisions: 260
% 0.38/0.59 Number of resolutions: 48
% 0.38/0.59 Number of condensations: 0
% 0.38/0.59 Number of sub resolutions: 13
% 0.38/0.59 Number of input literals (deduplicated): 22
% 0.38/0.59 Number of grows: 6
% 0.38/0.59 Number of considered ground atoms: 134
% 0.38/0.59
% 0.38/0.59 Needed: 0:00:00.03
% 0.38/0.59
%------------------------------------------------------------------------------