%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO677-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 : n031.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:16 PM UTC 2026
% Result : Unsatisfiable 0.48s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO677-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n031.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:58:12 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Execution lmodel_grow ended with status: unsatisfiable
% 0.48/0.57 Used heuristic: lmodel_grow
% 0.48/0.57
% 0.48/0.57 Input Clauses:
% 0.48/0.57
% 0.48/0.57 Predicates: 'E' iLEQ 'LE'
% 0.48/0.57 Fol Constants: '0' z
% 0.48/0.57 Fol Functions: s f suc
% 0.48/0.57 Problem Properties:
% 0.48/0.57 This is a full first-order problem without equality.
% 0.48/0.57
% 0.48/0.57 After reduction: Problem Properties:
% 0.48/0.57 This is a full first-order problem without equality.
% 0.48/0.57
% 0.48/0.57
% 0.48/0.57 Reduced Input Clauses:
% 0.48/0.57 39:8:2:[26.7,1.2]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 0.48/0.57 40:7:2:[17.6,2.5]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.48/0.57 41:7:2:[10.5,4.5]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x0),f(suc(x0)))
% 0.48/0.57 42:7:2:[17.5,5.0]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.48/0.57 43:7:2:[35.6,8.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.48/0.57 44:7:2:[35.5,11.3]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.48/0.57 45:4:1:[34.2,12.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.48/0.57 46:2:1:[18.0,16.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.48/0.57 48:7:2:[40.7,20.0,42.7,47.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) ->
% 0.48/0.57 49:7:2:[10.6,21.1]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 0.48/0.57 50:4:1:[32.2,22.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.48/0.57 51:4:1:[37.2,24.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.48/0.57 52:7:2:[6.5,26.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.48/0.57 54:7:2:[44.7,29.4,43.7,53.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) ->
% 0.48/0.57 56:7:2:[41.7,30.1,49.7,55.6]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))) ->
% 0.48/0.57 57:7:2:[6.6,33.2]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.48/0.57 59:3:1:[23.2,38.2,48.2,58.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 0.48/0.57
% 0.48/0.57 Most General Atoms: iLEQ(suc(x1),suc(x0)) 'E'(s(s('0')),f(x1)) 'E'('0',f(x1)) 'LE'(f(x0),s(s(s('0')))) 'E'(s(s(s('0'))),f(x1)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) 'E'(s('0'),f(x1)) 'LE'(f(x0),'0') 'LE'(f(x0),s(s(s(s('0')))))
% 0.48/0.57
% 0.48/0.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 57 atoms initially, heuristics mode: lmodel_grow ===
% 0.48/0.57
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 63
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 69
% 0.48/0.57 === Conflict found: 39:8:2:[26.7,1.2]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> suc(suc('0')), x1 -> suc(suc('0'))}
% 0.48/0.57 === Backtracking. Learning clause 60:3:1:[39.7,57.7,45.4]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) ->
% 0.48/0.57 === Conflict found: 54:7:2:[44.7,29.4,43.7,53.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> '0', x1 -> '0'}
% 0.48/0.57 === Backtracking. Learning clause 61:4:1:[54.7,51.4,25.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(suc(x0)),s('0'))
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 82
% 0.48/0.57 === Conflict found: 50:4:1:[32.2,22.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.48/0.57 === Backtracking. Learning clause 62:2:1:[50.4,56.2,3.2,18.1,46.1]:Top: 'E'(s(s(s('0'))),f(suc(x0))) -> 'LE'(f(x0),s(s(s('0'))))
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 96
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 104
% 0.48/0.57 === Backtracking. Learning clause 63:2:1:[3.1,18.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.48/0.57 === Backtracking. Learning clause 64:2:1:[9.2,62.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s(s('0'))))
% 0.48/0.57 === Backtracking. Learning clause 65:1:1:[9.1,18.1,62.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.48/0.57 === Backtracking. Learning clause 68:1:1:[65.0,66.0,65.0,67.1,15.2,60.1,65.1,19.2,31.2]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.48/0.57 === Conflict found: 56:7:2:[41.7,30.1,49.7,55.6]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> {x0 -> suc(suc(f('0'))), x1 -> suc(suc(f('0')))}
% 0.48/0.57 === Backtracking. Learning clause 69:3:1:[56.2,50.4]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) ->
% 0.48/0.57 === Conflict found: 54:7:2:[44.7,29.4,43.7,53.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> z, x1 -> z}
% 0.48/0.57 === Backtracking. Learning clause 71:4:1:[68.0,70.3,54.7,51.4,27.2,14.1,59.3,13.2,61.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0')
% 0.48/0.57 === Conflict found: 59:3:1:[23.2,38.2,48.2,58.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> {x0 -> '0'}
% 0.48/0.57 === Backtracking. Learning clause 72:4:1:[59.3,14.2,36.2]:Top: 'E'('0',f(suc(x0))),'LE'(f(x0),s('0')),'LE'(f(suc(suc(x0))),s('0')) -> 'LE'(f(x0),'0')
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 123
% 0.48/0.57 === Conflict found: 51:4:1:[37.2,24.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.48/0.57 === Backtracking. Learning clause 76:2:1:[68.0,73.0,68.0,74.1,68.0,75.2,51.1,27.2,7.2,25.2]:Top: -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0'))
% 0.48/0.57 === Conflict found: 72:4:1:[59.3,14.2,36.2]:Top: 'E'('0',f(suc(x0))),'LE'(f(x0),s('0')),'LE'(f(suc(suc(x0))),s('0')) -> 'LE'(f(x0),'0') {x0 -> z}
% 0.48/0.57 === Backtracking. Learning clause 78:3:1:[68.0,77.1,72.3,7.3,27.3]:Top: 'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 0.48/0.57 === Backtracking. Learning clause 81:3:1:[78.2,79.0,68.0,80.1,27.2,54.2,68.1,76.1,25.2,72.3]:Top: 'E'('0',f(suc(x0))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.48/0.57 === Conflict found: 54:7:2:[44.7,29.4,43.7,53.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> z, x1 -> z}
% 0.48/0.57 === Backtracking. Learning clause 84:2:1:[68.0,82.0,68.0,83.1,54.4,7.2,76.1,25.2,78.3,81.2,13.2,76.2]:Top: -> 'LE'(f(x0),'0'),iLEQ(suc(suc(x0)),suc(suc(x0)))
% 0.48/0.57 === Conflict found: 71:4:1:[68.0,70.3,54.7,51.4,27.2,14.1,59.3,13.2,61.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0') {x0 -> z}
% 0.48/0.57 === Backtracking. Learning clause 85:4:1:[71.1,36.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s('0')) -> 'LE'(f(x0),'0')
% 0.48/0.57 === Backtracking. Learning clause 86:3:1:[25.1,68.1,13.1,81.1]:Top: 'LE'(f(x0),s('0')) -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),'0')
% 0.48/0.57 === Conflict found: 54:7:2:[44.7,29.4,43.7,53.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> z, x1 -> z}
% 0.48/0.57 === Backtracking. Learning clause 87:3:1:[54.7,51.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 0.48/0.57 === Backtracking. Learning clause 89:2:1:[68.0,88.0,27.1,68.1,87.1,7.2,13.1,81.1,86.2]:Top: 'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.48/0.57 === Backtracking. Learning clause 90:2:1:[27.1,68.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.48/0.57 === Conflict found: 87:3:1:[54.7,51.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> z}
% 0.48/0.57
% 0.48/0.57 SZS status Unsatisfiable
% 0.48/0.57
% 0.48/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57
% 0.48/0.57 SPASS-SCL-FOL Statistics:
% 0.48/0.57 Number of learned clauses: 19
% 0.48/0.57 Number of propagations: 341
% 0.48/0.57 Number of decisions: 299
% 0.48/0.57 Number of resolutions: 61
% 0.48/0.57 Number of condensations: 0
% 0.48/0.57 Number of sub resolutions: 33
% 0.48/0.57 Number of input literals (deduplicated): 29
% 0.48/0.57 Number of grows: 7
% 0.48/0.57 Number of considered ground atoms: 123
% 0.48/0.57
% 0.48/0.57 Needed: 0:00:00.04
% 0.48/0.57
%------------------------------------------------------------------------------