%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO657-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:15 PM UTC 2026
% Result : Unsatisfiable 0.31s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO657-1 : TPTP v9.2.1. Released v7.3.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 : n013.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:56:12 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.21/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/0.57 Execution normal ended with status: unsatisfiable
% 0.31/0.57 Used heuristic: normal
% 0.31/0.57
% 0.31/0.57 Input Clauses:
% 0.31/0.57
% 0.31/0.57 Predicates: 'E' iLEQ 'LE'
% 0.31/0.57 Fol Constants: '0' z
% 0.31/0.57 Fol Functions: suc f s
% 0.31/0.57 Problem Properties:
% 0.31/0.57 This is a full first-order problem without equality.
% 0.31/0.57
% 0.31/0.57 After reduction: Problem Properties:
% 0.31/0.57 This is a full first-order problem without equality.
% 0.31/0.57
% 0.31/0.57
% 0.31/0.57 Reduced Input Clauses:
% 0.31/0.57 21:7:2:[17.5,5.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.31/0.57 22:7:2:[1.6,6.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0)))
% 0.31/0.57 23:2:1:[3.0,7.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.31/0.57 24:4:1:[11.2,9.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.31/0.57 25:7:2:[1.5,10.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 0.31/0.57 27:7:2:[22.7,12.6,25.7,26.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) ->
% 0.31/0.57 28:4:1:[4.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.31/0.57 29:7:2:[17.6,19.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.31/0.57 31:7:2:[21.7,20.7,29.7,30.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) ->
% 0.31/0.57
% 0.31/0.57 Most General Atoms: iLEQ(suc(x0),suc(x1)) 'E'('0',f(x1)) 'E'(f(x1),f(suc(x1))) 'LE'(f(x0),s('0')) 'LE'(f(x0),s(s('0'))) 'E'(s('0'),f(x1)) 'LE'(f(x0),'0')
% 0.31/0.57
% 0.31/0.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: normal ===
% 0.31/0.57
% 0.31/0.57 === Backtracking. Learning clause 32:3:1:[17.1,4.4]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.31/0.57 === Backtracking. Learning clause 33:4:1:[11.4,1.3,8.2,13.2,16.3,23.2,32.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0)))
% 0.31/0.57 === Clause set with instances from active satisfied. Growing active. New size: 113
% 0.31/0.57 === Clause set with instances from active satisfied. Growing active. New size: 177
% 0.31/0.57 === Conflict found: 31:7:2:[21.7,20.7,29.7,30.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> {x0 -> suc(z), x1 -> suc(z)}
% 0.31/0.57 === Backtracking. Learning clause 34:5:1:[31.1,28.4,2.2,3.1,16.2,23.1,13.1,1.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),iLEQ(suc(x0),suc(x0)),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0)))
% 0.31/0.57 === Conflict found: 28:4:1:[4.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.31/0.57 === Backtracking. Learning clause 35:4:1:[28.4,31.1,2.2,3.1,16.2,23.1,13.1,11.2,34.2,8.2,23.2,33.2]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0)))
% 0.31/0.57 === Backtracking. Learning clause 36:5:1:[14.2,27.2,23.2,8.2,2.3]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 0.31/0.57 === Conflict found: 28:4:1:[4.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.31/0.57 === Backtracking. Learning clause 37:6:1:[28.4,31.1,16.2,14.1,27.2,8.2,23.2,31.3,36.5,13.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s('0')) -> 'LE'(f(x0),'0')
% 0.31/0.57 === Conflict found: 28:4:1:[4.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.31/0.57 === Backtracking. Learning clause 38:5:1:[28.4,31.1,2.2,16.2,37.5]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0')
% 0.31/0.57 === Backtracking. Learning clause 39:4:1:[14.1,23.2,24.1,13.2,8.2,2.3,16.3]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 0.31/0.57 === Conflict found: 28:4:1:[4.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.31/0.57 === Backtracking. Learning clause 40:7:1:[28.4,31.1,16.2,14.1,24.1,8.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'('0',f(suc(x0))),'LE'(f(x0),s('0')) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 0.31/0.57 === Conflict found: 28:4:1:[4.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.31/0.57 === Backtracking. Learning clause 41:3:1:[28.4,31.1]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 0.31/0.57 === Conflict found: 23:2:1:[3.0,7.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> z}
% 0.31/0.57 === Backtracking. Learning clause 42:4:1:[23.1,28.3,40.5,13.2,2.3,41.1,39.4,38.3]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0')
% 0.31/0.57 === Conflict found: 36:5:1:[14.2,27.2,23.2,8.2,2.3]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0)))) {x0 -> z}
% 0.31/0.57 === Backtracking. Learning clause 43:3:1:[36.1,39.2,13.2,16.3]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 0.31/0.57 === Conflict found: 24:4:1:[11.2,9.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc('0')}
% 0.31/0.57 === Backtracking. Learning clause 44:3:1:[24.4,27.5]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))) ->
% 0.31/0.57 === Conflict found: 41:3:1:[28.4,31.1]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> f(z)}
% 0.31/0.57 === Backtracking. Learning clause 45:4:1:[41.3,23.1,16.2,8.1]:Top: 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s('0'))) -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.31/0.57 === Clause set with instances from active satisfied. Growing active. New size: 241
% 0.31/0.57 === Conflict found: 41:3:1:[28.4,31.1]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> f(suc('0'))}
% 0.31/0.57 === Backtracking. Learning clause 46:3:1:[41.1,2.2,16.2,23.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.31/0.57 === Conflict found: 42:4:1:[23.1,28.3,40.5,13.2,2.3,41.1,39.4,38.3]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0') {x0 -> z}
% 0.31/0.57 === Backtracking. Learning clause 47:1:0:[42.4,15.1,3.1,3.1]:: 'E'(s('0'),f(suc(z))) ->
% 0.31/0.57 === Conflict found: 36:5:1:[14.2,27.2,23.2,8.2,2.3]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0)))) {x0 -> z}
% 0.31/0.57 === Backtracking. Learning clause 48:3:0:[36.4,15.1,3.1]:: iLEQ(suc(z),suc(z)),'E'('0',f(suc(z))) -> 'E'(s('0'),f(suc(suc(z))))
% 0.31/0.57 === Conflict found: 39:4:1:[14.1,23.2,24.1,13.2,8.2,2.3,16.3]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0)))) {x0 -> z}
% 0.31/0.57 === Backtracking. Learning clause 49:2:0:[39.1,3.1,15.1,48.1]:: 'E'('0',f(suc(z))) -> 'E'(s('0'),f(suc(suc(z))))
% 0.31/0.57 === Backtracking. Learning clause 50:1:0:[13.3,15.1,16.3,3.1,49.1]:: -> 'E'(s('0'),f(suc(suc(z))))
% 0.31/0.57 === Backtracking. Learning clause 51:3:1:[11.4,1.3]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.31/0.57 === Clause set with instances from active satisfied. Growing active. New size: 305
% 0.31/0.57 === Conflict found: 46:3:1:[41.1,2.2,16.2,23.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(s(z))}
% 0.31/0.57 === Backtracking. Learning clause 52:2:1:[46.1,3.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.31/0.57 === Conflict found: 52:2:1:[46.1,3.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 0.31/0.57 === Backtracking. Learning clause 53:4:1:[52.1,3.1,14.1,27.2,8.2]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.31/0.57 === Conflict found: 52:2:1:[46.1,3.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 0.31/0.57 === Backtracking. Learning clause 54:3:1:[52.1,3.1,53.3]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0')
% 0.31/0.57 === Conflict found: 52:2:1:[46.1,3.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 0.31/0.57 === Backtracking. Learning clause 56:3:1:[53.0,55.2,52.1,3.1,14.1,24.1,8.2]:Top: 'E'('0',f(suc(x0))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.31/0.57 === Conflict found: 52:2:1:[46.1,3.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 0.31/0.57
% 0.31/0.57 SZS status Unsatisfiable
% 0.31/0.57
% 0.31/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/0.57
% 0.31/0.57 SPASS-SCL-FOL Statistics:
% 0.31/0.57 Number of learned clauses: 24
% 0.31/0.57 Number of propagations: 792
% 0.31/0.57 Number of decisions: 302
% 0.31/0.57 Number of resolutions: 101
% 0.31/0.57 Number of condensations: 0
% 0.31/0.57 Number of sub resolutions: 12
% 0.31/0.57 Number of input literals (deduplicated): 17
% 0.31/0.57 Number of grows: 4
% 0.31/0.57 Number of considered ground atoms: 305
% 0.31/0.57
% 0.31/0.57 Needed: 0:00:00.06
% 0.31/0.57
%------------------------------------------------------------------------------