%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO669-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 : n022.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.91s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO669-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 : n022.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:56:21 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.91/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/0.67 Execution lmodel_grow ended with status: unsatisfiable
% 0.91/0.67 Used heuristic: lmodel_grow
% 0.91/0.67
% 0.91/0.67 Input Clauses:
% 0.91/0.67
% 0.91/0.67 Predicates: 'E' iLEQ 'LE'
% 0.91/0.67 Fol Constants: '0' z
% 0.91/0.67 Fol Functions: f suc s
% 0.91/0.67 Problem Properties:
% 0.91/0.67 This is a full first-order problem without equality.
% 0.91/0.67
% 0.91/0.67 After reduction: Problem Properties:
% 0.91/0.67 This is a full first-order problem without equality.
% 0.91/0.67
% 0.91/0.67
% 0.91/0.67 Reduced Input Clauses:
% 0.91/0.67 52:5:1:[39.4,2.0,28.2,51.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.91/0.67 53:5:1:[15.2,4.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.91/0.67 55:10:2:[20.9,5.0,38.7,54.8]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 56:8:2:[30.5,8.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.91/0.67 58:9:2:[41.7,11.6,56.8,57.8]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.91/0.67 60:5:1:[53.4,12.2,15.2,59.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0))
% 0.91/0.67 62:8:2:[56.7,13.2,30.5,61.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.91/0.67 64:8:2:[41.8,16.4,30.6,63.8]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.91/0.67 66:5:1:[37.4,18.0,1.2,65.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> iLEQ(suc(x0),suc(x0))
% 0.91/0.67 67:8:2:[34.5,19.4]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.91/0.67 68:10:2:[47.8,20.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 70:11:2:[50.11,21.0,55.11,69.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) ->
% 0.91/0.67 72:8:2:[47.7,22.0,23.5,71.6]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.91/0.67 75:10:2:[42.11,25.4,64.9,73.10,62.9,74.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) ->
% 0.91/0.67 76:11:2:[35.9,26.1]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 79:9:2:[58.9,27.3,41.7,77.8,62.9,78.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.91/0.67 80:9:2:[34.6,29.1]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.91/0.67 82:11:2:[35.9,32.1,76.11,81.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) ->
% 0.91/0.67 84:8:2:[67.7,35.3,34.5,83.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.91/0.67 86:4:1:[1.2,37.2,58.7,85.5]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.91/0.67 87:8:2:[23.6,38.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 88:5:1:[28.2,39.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.91/0.67 89:2:1:[14.0,40.0]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.91/0.67 103:9:2:[68.10,50.3,98.8,101.6,97.9,102.8]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.91/0.67 92:9:2:[58.10,42.4,64.9,90.8,56.8,91.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 93:8:2:[34.6,43.1]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 95:9:2:[67.8,44.1,93.7,94.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.91/0.67 97:8:2:[87.8,46.3,23.6,96.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.91/0.67 98:8:2:[23.5,47.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.91/0.67 100:10:2:[67.8,49.1,95.10,99.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.91/0.67
% 0.91/0.67 Most General Atoms: 'LE'(f(x0),s(s('0'))) 'E'(s('0'),f(x1)) 'E'(f(x1),f(suc(x1))) 'E'(f(x1),f(suc(suc(x1)))) 'LE'(f(x0),'0') 'E'('0',f(x1)) iLEQ(suc(x1),suc(x0)) 'LE'(f(x0),s('0')) 'LE'(f(x0),s(s(s('0')))) 'E'(s(s('0')),f(x1))
% 0.91/0.67
% 0.91/0.67 === Starting SPASS-SCL-FOL A Little Less Naive, considering 59 atoms initially, heuristics mode: lmodel_grow ===
% 0.91/0.67
% 0.91/0.67 === Conflict found: 82:11:2:[35.9,32.1,76.11,81.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> {x0 -> '0', x1 -> '0'}
% 0.91/0.67 === Backtracking. Learning clause 104:4:1:[82.8,84.8,95.8,60.5,3.2,31.2,6.2,89.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.91/0.67 === Conflict found: 97:8:2:[87.8,46.3,23.6,96.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))) {x0 -> z, x1 -> z}
% 0.91/0.67 === Backtracking. Learning clause 105:6:1:[97.8,70.6,52.5,33.2,6.3]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(suc(x0)),s('0')),'E'(s(s('0')),f(suc(suc(suc(x0)))))
% 0.91/0.67 === Conflict found: 52:5:1:[39.4,2.0,28.2,51.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.91/0.67 === Backtracking. Learning clause 106:5:1:[52.5,70.11]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 0.91/0.67 === Clause set with instances from active satisfied. Growing active. New size: 75
% 0.91/0.67 === Conflict found: 104:4:1:[82.8,84.8,95.8,60.5,3.2,31.2,6.2,89.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(z)}
% 0.91/0.67 === Backtracking. Learning clause 107:3:1:[104.1,14.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.91/0.67 === Conflict found: 66:5:1:[37.4,18.0,1.2,65.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(suc('0'))}
% 0.91/0.67 === Backtracking. Learning clause 109:4:1:[86.3,108.0,66.5,75.10]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) ->
% 0.91/0.67 === Clause set with instances from active satisfied. Growing active. New size: 94
% 0.91/0.67 === Clause set with instances from active satisfied. Growing active. New size: 127
% 0.91/0.67 === Conflict found: 107:3:1:[104.1,14.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc('0')))}
% 0.91/0.67 === Backtracking. Learning clause 110:1:1:[107.2,14.1,14.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.91/0.67 === Conflict found: 106:5:1:[52.5,70.11]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> z}
% 0.91/0.67 === Backtracking. Learning clause 114:3:1:[110.0,111.2,110.0,112.3,110.0,113.4,106.5,33.2,48.2,36.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))) -> 'LE'(f(x0),s('0'))
% 0.91/0.67 === Backtracking. Learning clause 115:3:1:[1.4,30.5]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.91/0.67 === Conflict found: 106:5:1:[52.5,70.11]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> '0'}
% 0.91/0.67 === Backtracking. Learning clause 116:6:1:[106.2,10.2,33.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(suc(x0)),s('0'))
% 0.91/0.67 === Backtracking. Learning clause 117:3:1:[34.3,15.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.91/0.67 === Backtracking. Learning clause 118:3:1:[28.4,23.5]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.91/0.67 === Clause set with instances from active satisfied. Growing active. New size: 154
% 0.91/0.67 === Backtracking. Learning clause 119:2:1:[10.1,110.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.91/0.67 === Clause set with instances from active satisfied. Growing active. New size: 181
% 0.91/0.67 === Conflict found: 114:3:1:[110.0,111.2,110.0,112.3,110.0,113.4,106.5,33.2,48.2,36.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(suc('0')))}
% 0.91/0.67 === Backtracking. Learning clause 120:2:1:[114.1,119.1]:Top: 'E'(f(x0),f(suc(x0))) -> 'LE'(f(x0),s('0'))
% 0.91/0.67 === Conflict found: 118:3:1:[28.4,23.5]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0))) {x0 -> suc(suc(suc('0')))}
% 0.91/0.67 === Backtracking. Learning clause 122:1:1:[110.0,121.0,118.3,120.1,33.2,119.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.91/0.67 === Conflict found: 109:4:1:[86.3,108.0,66.5,75.10]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> {x0 -> z}
% 0.91/0.67
% 0.91/0.67 SZS status Unsatisfiable
% 0.91/0.67
% 0.91/0.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/0.67
% 0.91/0.67 SPASS-SCL-FOL Statistics:
% 0.91/0.67 Number of learned clauses: 14
% 0.91/0.67 Number of propagations: 287
% 0.91/0.67 Number of decisions: 369
% 0.91/0.67 Number of resolutions: 38
% 0.91/0.67 Number of condensations: 0
% 0.91/0.67 Number of sub resolutions: 58
% 0.91/0.67 Number of input literals (deduplicated): 30
% 0.91/0.67 Number of grows: 5
% 0.91/0.67 Number of considered ground atoms: 181
% 0.91/0.67
% 0.91/0.67 Needed: 0:00:00.14
% 0.91/0.67
%------------------------------------------------------------------------------