%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO689-1 : 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 : 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:41:17 PM UTC 2026
% Result : Unsatisfiable 3.39s 1.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO689-1 : 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.17/0.34 % Computer : n010.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.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:55:52 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 3.39/1.30 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.39/1.30 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.39/1.30 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.39/1.30 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.39/1.30 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.39/1.30 Execution resolution_1 ended with status: unsatisfiable
% 3.39/1.30 Used heuristic: resolution_1
% 3.39/1.30
% 3.39/1.30 Input Clauses:
% 3.39/1.30
% 3.39/1.30 Predicates: 'E' iLEQ 'LE'
% 3.39/1.30 Fol Constants: '0' z
% 3.39/1.30 Fol Functions: s f suc
% 3.39/1.30 Problem Properties:
% 3.39/1.30 This is a full first-order problem without equality.
% 3.39/1.30
% 3.39/1.30 After reduction: Problem Properties:
% 3.39/1.30 This is a full first-order problem without equality.
% 3.39/1.30
% 3.39/1.30
% 3.39/1.30 Reduced Input Clauses:
% 3.39/1.30 23:2:1:[4.0,17.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0')))))
% 3.39/1.30
% 3.39/1.30 Most General Atoms: 'E'(s('0'),f(x3)) 'LE'(f(x0),s(s(s(s(s('0')))))) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) 'E'(s(s(s('0'))),f(x4)) 'LE'(f(x0),'0') 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s(s(s(s('0'))))) 'E'('0',f(x2)) 'E'(s(s(s(s('0')))),f(x2)) 'E'(s(s('0')),f(x4)) iLEQ(suc(x2),suc(x5))
% 3.39/1.30
% 3.39/1.30 === Starting SPASS-SCL-FOL A Little Less Naive, considering 11 atoms initially, heuristics mode: resolution_1 ===
% 3.39/1.30
% 3.39/1.30 === Backtracking. Learning clause 24:2:1:[13.2,10.3]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) ->
% 3.39/1.30 === Conflict found: 23:2:1:[4.0,17.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> '0'}
% 3.39/1.30 === Backtracking. Learning clause 25:3:1:[23.2,12.1]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 3.39/1.30 === Conflict found: 23:2:1:[4.0,17.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc('0')}
% 3.39/1.30 === Backtracking. Learning clause 26:4:1:[23.2,16.1,14.2,25.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 3.39/1.30 === Backtracking. Learning clause 27:3:1:[20.1,4.1,14.2,12.1,25.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 3.39/1.30 === Clause set with instances from active satisfied. Growing active. New size: 16
% 3.39/1.30 === Restarting.
% 3.39/1.30 === Conflict found: 27:3:1:[20.1,4.1,14.2,12.1,25.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc('0')}
% 3.39/1.30 === Backtracking. Learning clause 28:5:1:[27.3,6.1,7.2]:Top: iLEQ(suc(suc(x0)),suc(suc(x0))),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x0),suc(x0)) -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 3.39/1.30 === Clause set with instances from active satisfied. Growing active. New size: 19
% 3.39/1.30 === Restarting.
% 3.39/1.30 === Clause set with instances from active satisfied. Growing active. New size: 83
% 3.39/1.30 === Backtracking. Learning clause 29:2:1:[14.3,1.3,23.1]:Top: 'E'(s(s(s(s('0')))),f(suc(x0))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 3.39/1.30 === Backtracking. Learning clause 30:2:1:[7.5,18.3]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) ->
% 3.39/1.30 === Backtracking. Learning clause 31:2:1:[20.2,29.1]:Top: 'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 3.39/1.30 === Backtracking. Learning clause 32:1:1:[20.1,4.1,29.1]:Top: -> 'LE'(f(x0),s(s(s(s('0')))))
% 3.39/1.30 === Clause set with instances from active satisfied. Growing active. New size: 147
% 3.39/1.30 === Backtracking. Learning clause 33:5:1:[6.1,25.3,2.2]:Top: 'E'(s(s('0')),f(x0)) -> 'LE'(f(x0),s(s('0'))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 3.39/1.30 === Backtracking. Learning clause 34:4:1:[16.1,32.1,9.1,33.1,1.2]:Top: 'E'(s(s(s(s('0')))),f(x0)) -> 'LE'(f(x0),s(s('0'))),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 3.39/1.30 === Backtracking. Learning clause 35:4:1:[6.2,2.2,12.3,9.2,16.3,32.1,5.1]:Top: -> iLEQ(suc(x0),suc(x0)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 3.39/1.30 === Backtracking. Learning clause 36:5:1:[19.1,9.3,15.2,35.3,2.2]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'E'(s(s('0')),f(x0)) -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s('0')),iLEQ(suc(x0),suc(x0))
% 3.39/1.30 === Backtracking. Learning clause 37:5:1:[19.2,15.2,9.3]:Top: 'E'(s('0'),f(x0)),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s('0')),iLEQ(suc(x0),suc(x0)),'E'(s(s('0')),f(suc(x0)))
% 3.39/1.30 === Backtracking. Learning clause 38:2:1:[16.2,30.2,32.1]:Top: 'E'(s(s(s('0'))),f(x0)) -> 'LE'(f(x0),s(s(s('0'))))
% 3.39/1.30 === Backtracking. Learning clause 40:2:1:[32.0,39.0,12.2,38.1,9.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 3.39/1.30 === Backtracking. Learning clause 41:5:1:[3.1,19.2,5.2,8.1]:Top: iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))) -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 3.39/1.30 === Clause set with instances from active satisfied. Growing active. New size: 211
% 3.39/1.30 === Backtracking. Learning clause 42:5:1:[5.1,9.3,22.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(s('0'),f(suc(x0))),'E'(s(s('0')),f(suc(x0))),'E'('0',f(suc(x0))),'LE'(f(x0),'0')
% 3.39/1.30 === Backtracking. Learning clause 43:2:1:[21.6,2.3]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) ->
% 3.39/1.30 === Backtracking. Learning clause 44:7:1:[6.3,5.1,21.2,42.3,35.1,22.1,13.3,8.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0')) -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(x0),'0')
% 3.39/1.30 === Backtracking. Learning clause 46:1:1:[32.0,45.0,12.2,38.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 3.39/1.30 === Conflict found: 43:2:1:[21.6,2.3]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) -> {x0 -> suc('0')}
% 3.39/1.30 === Backtracking. Learning clause 48:1:1:[46.0,47.0,43.1,40.1,6.2]:Top: -> 'LE'(f(x0),s(s('0')))
% 3.39/1.30 === Backtracking. Learning clause 51:3:1:[48.0,49.1,48.0,50.2,15.3,41.1,5.2,8.1]:Top: 'E'(s('0'),f(suc(x0))) -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 3.39/1.30 === Conflict found: 37:5:1:[19.2,15.2,9.3]:Top: 'E'(s('0'),f(x0)),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s('0')),iLEQ(suc(x0),suc(x0)),'E'(s(s('0')),f(suc(x0))) {x0 -> '0'}
% 3.39/1.30 === Backtracking. Learning clause 55:3:1:[46.0,52.0,40.1,53.1,48.0,54.2,37.4,41.1,5.2,8.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'E'('0',f(x0)),'LE'(f(x0),'0')
% 3.39/1.30 === Backtracking. Learning clause 58:1:1:[48.0,56.0,48.0,57.1,3.4,15.3,19.2,5.2]:Top: -> 'LE'(f(x0),s('0'))
% 3.39/1.30 === Conflict found: 24:2:1:[13.2,10.3]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> {x0 -> z}
% 3.39/1.30 === Backtracking. Learning clause 59:1:0:[24.2,22.2,55.2,11.1,58.1]:: -> 'E'(s(s('0')),f(suc(z)))
% 3.39/1.30
% 3.39/1.30 SZS status Unsatisfiable
% 3.39/1.30
% 3.39/1.30 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.39/1.30
% 3.39/1.30 SPASS-SCL-FOL Statistics:
% 3.39/1.30 Number of learned clauses: 26
% 3.39/1.30 Number of propagations: 1089
% 3.39/1.30 Number of decisions: 262
% 3.39/1.30 Number of resolutions: 73
% 3.39/1.30 Number of condensations: 0
% 3.39/1.30 Number of sub resolutions: 11
% 3.39/1.30 Number of input literals (deduplicated): 24
% 3.39/1.30 Number of grows: 5
% 3.39/1.30 Number of considered ground atoms: 211
% 3.39/1.30
% 3.39/1.30 Needed: 0:00:00.75
% 3.39/1.30
%------------------------------------------------------------------------------