%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO685-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 : n008.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 0.88s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO685-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.16/0.34 % Computer : n008.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:56:14 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Execution normal ended with status: unsatisfiable
% 0.88/0.67 Used heuristic: normal
% 0.88/0.67
% 0.88/0.67 Input Clauses:
% 0.88/0.67
% 0.88/0.67 Predicates: 'E' iLEQ 'LE'
% 0.88/0.67 Fol Constants: '0' z
% 0.88/0.67 Fol Functions: s f suc
% 0.88/0.67 Problem Properties:
% 0.88/0.67 This is a full first-order problem without equality.
% 0.88/0.67
% 0.88/0.67 After reduction: Problem Properties:
% 0.88/0.67 This is a full first-order problem without equality.
% 0.88/0.67
% 0.88/0.67
% 0.88/0.67 Reduced Input Clauses:
% 0.88/0.67 48:4:1:[44.2,4.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.88/0.67 49:7:2:[22.6,6.4]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 50:8:2:[25.7,9.5]:TopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 0.88/0.67 51:4:1:[7.2,10.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.88/0.67 52:4:1:[2.2,11.2]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.88/0.67 53:7:2:[32.6,12.5]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 54:7:2:[37.6,14.6]:TopTop: 'E'(s(s(s(s('0')))),f(x0)),iLEQ(suc(x1),suc(x0)),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(s(s(s(s('0')))),f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 55:4:1:[1.2,17.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.88/0.67 56:8:2:[53.7,21.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) ->
% 0.88/0.67 57:7:2:[40.5,24.5]:TopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 58:7:2:[40.6,25.4]:TopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 59:7:2:[5.5,26.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 60:7:2:[5.6,27.0]:TopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(x1))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 61:7:2:[22.5,28.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 62:7:2:[32.5,30.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 64:7:2:[59.7,33.0,60.7,63.8]:TopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 0.88/0.67 65:2:1:[45.0,35.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0')))))
% 0.88/0.67 67:3:1:[39.2,36.2,64.2,66.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 0.88/0.67 68:7:2:[37.5,42.5]:TopTop: 'E'(s(s(s(s('0')))),f(x0)),iLEQ(suc(x1),suc(x0)),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(s(s(s(s('0')))),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 70:7:2:[61.7,43.4,49.7,69.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))) ->
% 0.88/0.67 72:7:2:[54.7,46.6,68.7,71.8]:TopTop: 'E'(s(s(s(s('0')))),f(x0)),iLEQ(suc(x1),suc(x0)),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(s(s(s(s('0')))),f(x1)) ->
% 0.88/0.67
% 0.88/0.67 Most General Atoms: 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s(s('0'))) 'E'('0',f(x1)) 'E'(f(x1),f(suc(x1))) 'E'(s(s(s('0'))),f(x0)) iLEQ(suc(x1),suc(x0)) 'E'(s(s('0')),f(x1)) 'E'(s('0'),f(x1)) 'LE'(f(x0),s('0')) 'E'(s(s(s(s('0')))),f(x1)) 'LE'(f(x0),s(s(s(s('0'))))) 'LE'(f(x0),'0') 'LE'(f(x0),s(s(s(s(s('0'))))))
% 0.88/0.67
% 0.88/0.67 === Starting SPASS-SCL-FOL A Little Less Naive, considering 69 atoms initially, heuristics mode: normal ===
% 0.88/0.67
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 133
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 197
% 0.88/0.67 === Backtracking. Learning clause 74:6:1:[16.2,73.3,38.1,15.3,49.2,18.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),iLEQ(suc(x0),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Backtracking. Learning clause 75:3:1:[32.1,44.4]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 261
% 0.88/0.67 === Conflict found: 72:7:2:[54.7,46.6,68.7,71.8]:TopTop: 'E'(s(s(s(s('0')))),f(x0)),iLEQ(suc(x1),suc(x0)),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(s(s(s(s('0')))),f(x1)) -> {x0 -> suc('0'), x1 -> suc('0')}
% 0.88/0.67 === Backtracking. Learning clause 76:3:1:[72.2,52.4,16.2,45.1,15.2,65.1,38.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))) -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Conflict found: 72:7:2:[54.7,46.6,68.7,71.8]:TopTop: 'E'(s(s(s(s('0')))),f(x0)),iLEQ(suc(x1),suc(x0)),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(s(s(s(s('0')))),f(x1)) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 77:3:1:[72.2,52.4,15.2,16.2,65.1]:Top: 'LE'(f(suc(x0)),s(s(s(s(s('0')))))),'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.88/0.67 === Conflict found: 72:7:2:[54.7,46.6,68.7,71.8]:TopTop: 'E'(s(s(s(s('0')))),f(x0)),iLEQ(suc(x1),suc(x0)),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(s(s(s(s('0')))),f(x1)) -> {x0 -> '0', x1 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 78:3:1:[72.2,52.4]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) ->
% 0.88/0.67 === Backtracking. Learning clause 79:4:1:[22.1,7.4,18.2,38.2]:Top: 'LE'(f(x0),s(s(s(s('0'))))),'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 325
% 0.88/0.67 === Backtracking. Learning clause 80:2:1:[16.1,45.1,78.1,65.1]:Top: 'E'(s(s(s(s('0')))),f(suc(x0))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.88/0.67 === Conflict found: 51:4:1:[7.2,10.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 -> z}
% 0.88/0.67 === Backtracking. Learning clause 81:5:1:[51.2,76.2,18.2,23.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(x0),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Conflict found: 50:8:2:[25.7,9.5]:TopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> '0', x1 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 82:5:1:[50.6,40.6,3.2,19.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Conflict found: 67:3:1:[39.2,36.2,64.2,66.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> {x0 -> f('0')}
% 0.88/0.67 === Backtracking. Learning clause 83:4:1:[67.3,47.2,29.2]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0')) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Backtracking. Learning clause 84:5:1:[40.4,1.4,3.2,13.1,75.1]:Top: 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s(s('0')))),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),s('0')),'E'(f(x0),f(suc(x0)))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 389
% 0.88/0.67 === Backtracking. Learning clause 85:4:1:[18.3,19.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 453
% 0.88/0.67 === Backtracking. Learning clause 87:1:1:[80.0,86.0,15.1,45.1]:Top: -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.88/0.67 === Conflict found: 70:7:2:[61.7,43.4,49.7,69.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> {x0 -> suc('0'), x1 -> suc('0')}
% 0.88/0.67 === Backtracking. Learning clause 92:2:1:[87.0,88.0,45.0,89.1,87.0,90.2,87.0,91.3,70.6,23.2,38.2,81.4,19.1,85.2]:Top: -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Backtracking. Learning clause 93:3:1:[40.4,1.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 === Conflict found: 70:7:2:[61.7,43.4,49.7,69.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 97:1:1:[87.0,94.0,87.0,95.1,45.0,96.2,70.1,81.4,23.2,18.2,76.2]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Conflict found: 82:5:1:[50.6,40.6,3.2,19.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 99:2:1:[97.0,98.1,82.3,97.1,8.2,97.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Conflict found: 55:4:1:[1.2,17.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)) {x0 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 101:1:1:[97.0,100.0,55.3,3.2,19.2,8.2,97.1,97.1,99.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Conflict found: 56:8:2:[53.7,21.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> {x0 -> f('0'), x1 -> f('0')}
% 0.88/0.67 === Backtracking. Learning clause 105:3:1:[101.0,102.0,101.0,103.1,101.0,104.2,56.7,75.3,48.4,13.2,47.1,31.2,13.2,29.1]:Top: -> 'E'('0',f(x0)),'E'('0',f(suc(x0))),'LE'(f(x0),'0')
% 0.88/0.67 === Conflict found: 56:8:2:[53.7,21.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> {x0 -> suc(z), x1 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 109:3:1:[101.0,106.0,101.0,107.1,101.0,108.2,56.1,48.4,34.2,75.3,31.2,13.2,83.3]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Conflict found: 48:4:1:[44.2,4.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 -> z}
% 0.88/0.67 === Backtracking. Learning clause 113:3:1:[101.0,110.0,101.0,111.1,101.0,112.2,48.3,13.2,34.2,31.2,109.2]:Top: 'E'('0',f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 0.88/0.67 === Backtracking. Learning clause 114:3:1:[7.4,22.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 === Conflict found: 62:7:2:[32.5,30.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x1),f(suc(x1))) {x0 -> '0', x1 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 118:3:1:[99.1,115.1,101.0,116.2,101.0,117.3,62.3,13.2,34.2,31.2]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 56:8:2:[53.7,21.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> {x0 -> f(z), x1 -> f(z)}
% 0.88/0.67 === Backtracking. Learning clause 121:2:1:[101.0,119.1,101.0,120.2,56.7,75.3,48.4,13.2,31.2]:Top: 'E'(s('0'),f(x0)) -> 'LE'(f(suc(x0)),s('0'))
% 0.88/0.67 === Conflict found: 56:8:2:[53.7,21.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> {x0 -> f('0'), x1 -> f('0')}
% 0.88/0.67 === Backtracking. Learning clause 124:2:1:[101.0,122.0,101.0,123.1,56.3,34.2,118.2,13.2,109.2,113.2,41.2,121.2]:Top: 'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Backtracking. Learning clause 126:2:1:[101.0,125.0,31.2,124.1,47.1]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 517
% 0.88/0.67 === Conflict found: 56:8:2:[53.7,21.1]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> {x0 -> s(s('0')), x1 -> s(s('0'))}
% 0.88/0.67 === Backtracking. Learning clause 128:3:1:[75.2,127.0,56.1,48.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 581
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 645
% 0.88/0.67 === Backtracking. Learning clause 131:1:1:[101.0,129.0,101.0,130.1,34.1,101.1,128.1,13.2,31.2]:Top: -> 'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 83:4:1:[67.3,47.2,29.2]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0')) -> 'LE'(f(x0),'0') {x0 -> z}
% 0.88/0.67
% 0.88/0.67 SZS status Unsatisfiable
% 0.88/0.67
% 0.88/0.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67
% 0.88/0.67 SPASS-SCL-FOL Statistics:
% 0.88/0.67 Number of learned clauses: 28
% 0.88/0.67 Number of propagations: 3391
% 0.88/0.67 Number of decisions: 1278
% 0.88/0.67 Number of resolutions: 98
% 0.88/0.67 Number of condensations: 0
% 0.88/0.67 Number of sub resolutions: 56
% 0.88/0.67 Number of input literals (deduplicated): 35
% 0.88/0.67 Number of grows: 9
% 0.88/0.67 Number of considered ground atoms: 645
% 0.88/0.67
% 0.88/0.67 Needed: 0:00:00.15
% 0.88/0.67
%------------------------------------------------------------------------------