%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO686-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 : n007.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.39s 0.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.13 % Problem : SYO686-1 : TPTP v9.2.1. Released v7.3.0.
% 0.10/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.35 % Computer : n007.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Thu May 7 13:55:24 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 SPASS-SCL-FOL version:
% 0.17/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.39/0.76 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.76 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.76 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.76 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.76 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.76 Execution resolution_1 ended with status: unsatisfiable
% 0.39/0.76 Used heuristic: resolution_1
% 0.39/0.76
% 0.39/0.76 Input Clauses:
% 0.39/0.76
% 0.39/0.76 Predicates: 'E' iLEQ 'LE'
% 0.39/0.76 Fol Constants: '0' z
% 0.39/0.76 Fol Functions: s suc f
% 0.39/0.76 Problem Properties:
% 0.39/0.76 This is a full first-order problem without equality.
% 0.39/0.76
% 0.39/0.76 After reduction: Problem Properties:
% 0.39/0.76 This is a full first-order problem without equality.
% 0.39/0.76
% 0.39/0.76
% 0.39/0.76 Reduced Input Clauses:
% 0.39/0.76 84:10:2:[68.9,1.3,13.7,83.6]: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(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 85:8:2:[24.5,2.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(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.39/0.76 86:6:1:[75.2,3.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.76 87:12:2:[63.9,6.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(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)),'E'(f(x1),f(suc(suc(x1)))) ->
% 0.39/0.76 88:11:2:[12.9,8.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(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(x1)),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 89:8:2:[39.5,11.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(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.39/0.76 91:8:2:[62.8,12.5,72.6,90.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(x1))),'E'(s(s(s(s('0')))),f(x1)),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.76 92:8:2:[33.6,13.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))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 94:11:2:[66.11,14.3,84.11,93.4]: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(x1),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 0.39/0.76 96:5:1:[20.4,15.1,17.2,95.3]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.76 98:5:1:[44.4,18.2,4.2,97.4]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(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(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.76 99:9:2:[24.6,19.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(suc(suc(x0))))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.76 100:5:1:[17.2,20.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.39/0.76 101:10:2:[89.8,21.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'(s(s(s('0'))),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 103:8:2:[61.8,22.5,39.6,102.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(suc(suc(suc(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.39/0.76 104:5:1:[75.2,25.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.39/0.76 107:9:2:[101.10,26.5,89.8,105.6,103.9,106.10]: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(suc(suc(suc(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)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 108:6:1:[5.2,29.4]:Top: 'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.76 109:9:2:[67.5,31.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(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.76 110:8:2:[72.5,32.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(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.39/0.76 111:8:2:[33.5,34.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(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.39/0.76 112:10:2:[59.7,35.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)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 114:10:2:[59.7,37.1,112.9,113.8]: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(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 116:10:2:[63.9,38.1,112.10,115.10]: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(suc(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 117:10:2:[85.8,40.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(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 119:10:2:[47.9,42.0,117.9,118.10]:TopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 121:11:2:[88.11,43.6,91.9,120.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(suc(x1))))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(x1)),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))) ->
% 0.39/0.76 122:5:1:[4.2,44.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)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.39/0.76 124:10:2:[101.9,46.1,61.7,123.10]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(f(x1),f(suc(x1))),'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)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 126:8:2:[24.5,47.7,85.7,125.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(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.39/0.76 127:5:1:[27.2,48.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)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.39/0.76 129:10:2:[51.9,49.6,62.7,128.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(suc(x1))))),'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))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 131:11:2:[126.9,50.0,119.11,130.8]:TopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))) ->
% 0.39/0.76 133:9:2:[62.7,51.6,110.8,132.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)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 135:8:2:[92.8,53.3,33.6,134.6]: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(suc(suc(suc(x0))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.76 137:8:2:[89.7,54.1,39.5,136.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(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.39/0.76 141:9:2:[107.11,57.1,124.11,138.7,137.9,139.8,103.9,140.12]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(suc(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.39/0.76 143:8:2:[110.7,58.5,72.5,142.7]: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(suc(x1))))),'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.39/0.76 144:8:2:[67.6,59.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))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 145:8:2:[39.6,61.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))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 146:8:2:[72.6,62.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))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 148:8:2:[67.6,63.6,144.8,147.8]: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(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.39/0.76 151:4:1:[127.4,64.0,27.2,149.5,141.0,150.6]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) ->
% 0.39/0.76 154:9:2:[68.10,66.3,135.9,152.6,111.8,153.8]: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(suc(suc(suc(x0))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76 156:9:2:[92.7,68.5,111.8,155.6]: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'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 157:5:1:[5.2,69.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.39/0.76 158:8:2:[67.5,73.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(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.39/0.76 159:8:2:[24.6,74.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))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 161:8:2:[111.7,78.3,33.5,160.6]: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(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.39/0.76 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 164:10:2:[85.8,80.0,117.10,163.7]: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(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.76
% 0.39/0.76 Most General Atoms: 'E'(s(s('0')),f(x1)) iLEQ(suc(x0),suc(x1)) 'E'('0',f(x1)) 'E'(f(x1),f(suc(x1))) 'E'(s('0'),f(x1)) 'E'(f(x1),f(suc(suc(x1)))) 'LE'(f(x0),s('0')) 'E'(s(s(s(s('0')))),f(x1)) 'LE'(f(x0),s(s(s('0')))) 'E'(s(s(s('0'))),f(x0)) 'LE'(f(x0),s(s(s(s(s('0')))))) 'LE'(f(x0),s(s(s(s('0'))))) 'LE'(f(x0),'0') 'LE'(f(x0),s(s('0')))
% 0.39/0.76
% 0.39/0.76 === Starting SPASS-SCL-FOL A Little Less Naive, considering 26 atoms initially, heuristics mode: resolution_1 ===
% 0.39/0.76
% 0.39/0.76 === Conflict found: 131:11:2:[126.9,50.0,119.11,130.8]:TopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))) -> {x0 -> '0', x1 -> '0'}
% 0.39/0.76 === Backtracking. Learning clause 165:6:1:[131.11,117.9]:Top: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x0),f(suc(x0))) ->
% 0.39/0.76 === Conflict found: 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> '0'}
% 0.39/0.76 === Backtracking. Learning clause 166:3:1:[162.2,45.1]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Conflict found: 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc('0')}
% 0.39/0.76 === Backtracking. Learning clause 167:3:1:[162.2,60.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Conflict found: 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(suc('0'))}
% 0.39/0.76 === Backtracking. Learning clause 168:3:1:[162.2,76.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Conflict found: 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(suc(suc('0')))}
% 0.39/0.76 === Backtracking. Learning clause 169:8:1:[162.2,10.1,121.5,168.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(x0)),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Backtracking. Learning clause 170:7:1:[23.1,16.1,121.5,76.1,168.1,167.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(x0)),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Backtracking. Learning clause 171:2:1:[23.1,16.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(x0))),'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 === Conflict found: 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(suc(suc('0')))}
% 0.39/0.76 === Backtracking. Learning clause 173:7:1:[162.0,172.1,162.2,10.1,121.5,171.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(x0)),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0')))))
% 0.39/0.76 === Backtracking. Learning clause 174:6:1:[52.1,16.1,121.5,171.1,60.1,167.1,166.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Conflict found: 171:2:1:[23.1,16.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(x0))),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(suc('0'))}
% 0.39/0.76 === Backtracking. Learning clause 176:6:1:[162.0,175.2,171.1,121.5,76.1,168.1,171.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0')))),'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 === Backtracking. Learning clause 177:2:1:[52.1,16.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 === Conflict found: 162:2:1:[16.0,79.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(suc(suc('0')))}
% 0.39/0.76 === Backtracking. Learning clause 180:6:1:[171.0,178.1,162.0,179.3,162.2,10.1,121.5,177.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0')))),'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 === Backtracking. Learning clause 181:5:1:[71.1,16.1,121.5,177.1,171.1,45.1,166.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))) -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 36
% 0.39/0.76 === Restarting.
% 0.39/0.76 === Conflict found: 122:5:1:[4.2,44.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)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 0.39/0.76 === Backtracking. Learning clause 182:4:1:[122.1,177.1,171.1,45.1,166.1]:Top: -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Conflict found: 171:2:1:[23.1,16.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(x0))),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc('0')}
% 0.39/0.76 === Backtracking. Learning clause 184:4:1:[162.0,183.0,171.1,122.1]:Top: 'E'(s(s(s(s('0')))),f(x0)) -> 'LE'(f(suc(x0)),s(s(s(s('0'))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 38
% 0.39/0.76 === Restarting.
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 102
% 0.39/0.76 === Conflict found: 121:11:2:[88.11,43.6,91.9,120.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(suc(x1))))),'E'(s(s(s(s('0')))),f(suc(suc(x1)))),'E'(s(s(s(s('0')))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(x1)),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))) -> {x0 -> z, x1 -> z}
% 0.39/0.76 === Backtracking. Learning clause 186:2:1:[171.0,185.1,121.8,133.8,91.8,98.5,177.1,162.1]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 166
% 0.39/0.76 === Backtracking. Learning clause 187:1:1:[71.1,16.1,186.1]:Top: -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.39/0.76 === Conflict found: 151:4:1:[127.4,64.0,27.2,149.5,141.0,150.6]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> {x0 -> '0'}
% 0.39/0.76 === Backtracking. Learning clause 192:1:1:[187.0,188.0,187.0,189.1,187.0,190.2,187.0,191.3,151.3,45.2,60.2,76.2,10.2]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.39/0.76 === Conflict found: 122:5:1:[4.2,44.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)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 0.39/0.76 === Backtracking. Learning clause 193:4:1:[122.5,133.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)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 230
% 0.39/0.76 === Backtracking. Learning clause 195:6:1:[192.0,194.0,7.1,65.3,56.1,24.2]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))) -> 'E'(s('0'),f(suc(x0))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0)))
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 294
% 0.39/0.76 === Backtracking. Learning clause 197:5:1:[192.0,196.1,82.1,81.3,195.2,65.3]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(x0)))
% 0.39/0.76 === Backtracking. Learning clause 200:5:1:[192.0,198.0,195.2,199.1,81.1,41.3,67.3,56.1,24.2]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))) -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0)))
% 0.39/0.76 === Conflict found: 96:5:1:[20.4,15.1,17.2,95.3]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 0.39/0.76 === Backtracking. Learning clause 204:3:1:[192.0,201.1,192.0,202.2,192.0,203.3,96.2,41.2,30.2,65.2]:Top: 'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0')))
% 0.39/0.76 === Conflict found: 161:8:2:[111.7,78.3,33.5,160.6]: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(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0))) {x0 -> z, x1 -> z}
% 0.39/0.76 === Backtracking. Learning clause 208:6:1:[192.0,205.0,192.0,206.1,192.0,207.2,161.2,65.2,30.2,36.2,200.3,81.1,67.3,7.2]:Top: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.39/0.76 === Backtracking. Learning clause 209:3:1:[72.2,4.4]:Top: 'E'(s(s(s(s('0')))),f(x0)),'E'(s(s(s(s('0')))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.39/0.76 === Backtracking. Learning clause 210:2:0:[56.3,77.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 0.39/0.76 === Conflict found: 94:11:2:[66.11,14.3,84.11,93.4]: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(x1),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> z, x1 -> z}
% 0.39/0.76 === Backtracking. Learning clause 211:1:1:[94.6,161.8,96.5,30.2,192.1,65.2,192.1,41.2,192.1,36.2,192.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.39/0.76 === Clause set with instances from active satisfied. Growing active. New size: 358
% 0.39/0.76 === Backtracking. Learning clause 212:2:1:[9.1,211.1]:Top: -> 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.39/0.76 === Backtracking. Learning clause 215:5:1:[7.1,213.1,211.0,214.3,75.4,208.2]:Top: 'E'(s('0'),f(x0)),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.39/0.76 === Conflict found: 87:12:2:[63.9,6.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(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)),'E'(f(x1),f(suc(suc(x1)))) -> {x0 -> z, x1 -> z}
% 0.39/0.76 === Backtracking. Learning clause 216:5:1:[87.9,116.10,70.2,211.1,212.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),s('0'))
% 0.39/0.76 === Conflict found: 86:6:1:[75.2,3.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.39/0.76 === Backtracking. Learning clause 217:5:1:[86.4,104.4,70.2,211.1,212.1,216.1,215.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0'),'LE'(f(x0),s('0'))
% 0.39/0.76 === Backtracking. Learning clause 218:4:1:[67.6,216.3]:Top: iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),s('0'))
% 0.39/0.76 === Conflict found: 86:6:1:[75.2,3.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.39/0.76 === Backtracking. Learning clause 219:3:0:[86.4,104.4,70.2,212.1,211.1,218.1,7.2,81.2,210.1]:: 'LE'(f(suc(z)),s(s('0'))),'LE'(f(z),s(s('0'))) -> 'E'('0',f(z))
% 0.39/0.76 === Backtracking. Learning clause 220:7:0:[82.1,81.3,77.1,148.2]:: 'LE'(f(suc(z)),s(s('0'))),iLEQ(suc(z),suc(z)),'E'(s('0'),f(suc(suc(z)))),'E'(s('0'),f(suc(suc(suc(z))))),'E'(s('0'),f(z)) -> 'E'('0',f(suc(z))),'E'(f(z),f(suc(z)))
% 0.39/0.76 === Backtracking. Learning clause 221:3:0:[82.1,81.3,77.1]:: 'LE'(f(suc(z)),s(s('0'))) -> 'E'('0',f(suc(z))),'E'(s('0'),f(suc(z)))
% 0.39/0.76 === Conflict found: 86:6:1:[75.2,3.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> f('0')}
% 0.39/0.76 === Backtracking. Learning clause 224:2:1:[211.0,222.1,211.0,223.2,86.4,104.4,218.1,212.1,7.2,81.2,70.2]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.39/0.76 === Backtracking. Learning clause 225:5:0:[24.3,221.2]:: iLEQ(suc(z),suc(z)),'E'('0',f(z)),'LE'(f(suc(z)),s(s('0'))) -> 'E'(f(z),f(suc(z))),'E'(s('0'),f(suc(z)))
% 0.39/0.76 === Conflict found: 224:2:1:[211.0,222.1,211.0,223.2,86.4,104.4,218.1,212.1,7.2,81.2,70.2]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> f('0')}
% 0.39/0.76 === Backtracking. Learning clause 226:1:1:[224.1,211.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.39/0.76 === Backtracking. Learning clause 227:2:0:[56.1,226.1,24.2,82.2,226.1,77.1]:: iLEQ(suc(z),suc(z)) -> 'E'(f(z),f(suc(z)))
% 0.39/0.76 === Backtracking. Learning clause 228:6:1:[28.1,226.1,131.4,55.2,226.1]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))) -> 'LE'(f(x0),'0')
% 0.39/0.76 === Backtracking. Learning clause 229:1:0:[55.1,226.1,117.1,228.5,56.2,226.1,82.2,226.1,77.1,227.2]:: iLEQ(suc(z),suc(z)) ->
% 0.39/0.76 === Backtracking. Learning clause 231:1:0:[227.0,230.1,56.1,226.1,5.1,82.2,226.1,77.1]:: -> 'E'(f(z),f(suc(z)))
% 0.39/0.76 === Backtracking. Learning clause 232:5:1:[28.2,108.2,226.1,55.2,226.1]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 0.39/0.76
% 0.39/0.76 SZS status Unsatisfiable
% 0.39/0.76
% 0.39/0.76 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.76
% 0.39/0.76 SPASS-SCL-FOL Statistics:
% 0.39/0.76 Number of learned clauses: 43
% 0.39/0.76 Number of propagations: 1795
% 0.39/0.76 Number of decisions: 549
% 0.39/0.76 Number of resolutions: 155
% 0.39/0.76 Number of condensations: 1
% 0.39/0.76 Number of sub resolutions: 107
% 0.39/0.76 Number of input literals (deduplicated): 46
% 0.39/0.76 Number of grows: 7
% 0.39/0.76 Number of considered ground atoms: 358
% 0.39/0.76
% 0.39/0.76 Needed: 0:00:00.21
% 0.39/0.76
%------------------------------------------------------------------------------