%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO672-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 : n005.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 40.32s 8.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYO672-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n005.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:01 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 40.32/8.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.32/8.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.32/8.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.32/8.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.32/8.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.32/8.56 Execution lmodel_grow ended with status: unsatisfiable
% 40.32/8.56 Used heuristic: lmodel_grow
% 40.32/8.56
% 40.32/8.56 Input Clauses:
% 40.32/8.56
% 40.32/8.56 Predicates: 'E' iLEQ 'LE'
% 40.32/8.56 Fol Constants: '0' z
% 40.32/8.56 Fol Functions: s f suc
% 40.32/8.56 Problem Properties:
% 40.32/8.56 This is a full first-order problem without equality.
% 40.32/8.56
% 40.32/8.56 After reduction: Problem Properties:
% 40.32/8.56 This is a full first-order problem without equality.
% 40.32/8.56
% 40.32/8.56
% 40.32/8.56 Reduced Input Clauses:
% 40.32/8.56 106:14:3:[56.12,1.2,100.10,105.12]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0)))
% 40.32/8.56 108:15:3:[35.15,2.6,67.13,107.12]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x2),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0)))
% 40.32/8.56 110:14:3:[13.14,3.3,36.12,109.11]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 111:15:3:[6.12,4.7]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 40.32/8.56 112:12:3:[62.8,6.6]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 114:16:3:[96.15,7.5,70.13,113.7]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 116:12:3:[93.12,8.3,5.10,115.9]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 117:5:1:[68.2,9.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))
% 40.32/8.56 119:15:3:[77.13,10.7,111.14,118.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x1),f(suc(x1)))
% 40.32/8.56 121:16:3:[29.16,11.3,110.15,120.8]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 123:17:3:[28.16,12.3,23.14,122.14]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 124:14:3:[93.10,13.8]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 126:14:3:[124.12,14.2,93.10,125.10]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 128:5:1:[69.4,15.2,91.2,127.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))
% 40.32/8.56 129:12:3:[75.10,16.7]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 131:17:3:[114.16,17.2,76.14,130.11]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 133:14:3:[25.13,18.4,24.11,132.6]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 135:14:3:[70.12,19.1,129.10,134.8]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 138:16:3:[121.16,20.2,61.14,136.14,106.15,137.15]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 140:14:3:[70.14,21.1,24.12,139.11]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0)))
% 40.32/8.56 141:12:3:[75.9,22.4]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 143:14:3:[63.13,23.4,93.11,142.8]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 144:12:3:[75.8,24.5]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 146:13:3:[144.11,25.5,141.10,145.7]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 148:12:3:[141.11,27.4,75.9,147.5]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 151:15:3:[29.15,28.4,124.13,149.8,143.14,150.12]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 152:16:3:[124.13,29.6]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 153:12:3:[62.9,30.6]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 155:14:3:[48.13,31.6,54.11,154.10]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(s(s('0')),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 157:15:3:[140.14,32.1,135.15,156.2]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0)))
% 40.32/8.56 159:5:1:[117.4,33.0,68.2,158.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))
% 40.32/8.56 161:12:3:[129.12,34.1,75.10,160.9]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 40.32/8.56 162:15:3:[153.12,35.7]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 163:12:3:[5.8,36.8]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 40.32/8.56 164:2:1:[92.0,37.0]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 40.32/8.56 166:17:3:[88.16,38.6,155.14,165.11]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 168:16:3:[152.14,39.2,126.14,167.7]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 170:13:3:[129.11,40.5,141.12,169.9]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 172:16:3:[95.14,42.7,162.14,171.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 175:16:3:[86.15,43.7,172.16,173.9,162.14,174.11]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 177:12:3:[163.10,44.2,5.8,176.10]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 40.32/8.56 179:16:3:[58.15,45.6,155.14,178.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 181:18:3:[102.18,47.3,123.18,180.5]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) ->
% 40.32/8.56 182:14:3:[153.12,48.7]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 183:14:3:[112.12,49.7]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 185:15:3:[143.15,51.4,116.13,184.10]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(x2)))
% 40.32/8.56 188:15:3:[96.16,53.2,140.15,186.7,146.14,187.13]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 189:12:3:[62.10,54.7]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 191:15:3:[133.14,55.2,148.12,190.10]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x2),f(suc(x2)))
% 40.32/8.56 192:14:3:[163.11,56.6]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0)))
% 40.32/8.56 194:17:3:[188.16,57.2,157.16,193.9]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 196:15:3:[95.14,58.7,182.12,195.8]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 199:17:3:[104.18,60.2,131.18,197.3,157.16,198.10]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)) ->
% 40.32/8.56 201:14:3:[63.14,61.3,116.13,200.8]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.56 202:14:3:[93.11,63.6]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.56 204:12:3:[100.11,64.4,5.9,203.8]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 40.32/8.56 206:12:3:[62.10,67.7,189.12,205.8]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x2))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 40.32/8.56 207:5:1:[91.2,69.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))
% 40.32/8.56 209:13:3:[129.10,70.6,144.12,208.9]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 212:13:3:[192.13,71.4,163.11,210.8,204.12,211.12]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1)))
% 40.32/8.56 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) ->
% 40.32/8.56 215:5:1:[52.2,73.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))
% 40.32/8.56 218:14:3:[76.15,74.2,161.13,216.7,148.13,217.12]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2)))
% 40.32/8.56 221:13:3:[170.13,76.5,129.11,219.6,148.13,220.10]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.56 223:12:3:[112.10,77.6,62.8,222.8]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 40.32/8.56 225:15:3:[86.14,79.5,223.12,224.11]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(x2)))
% 40.32/8.57 228:13:3:[170.14,80.2,161.13,226.6,141.12,227.11]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.57 230:14:3:[95.13,81.5,112.11,229.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.57 232:12:3:[144.10,82.1,75.8,231.7]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 40.32/8.57 234:12:3:[153.11,83.5,62.9,233.8]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 40.32/8.57 237:13:3:[146.12,84.2,232.12,235.7,141.10,236.9]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.57 240:13:3:[95.12,86.6,153.10,238.8,223.12,239.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.57 244:13:3:[212.14,87.3,106.14,241.5,177.12,242.9,204.12,243.14]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x2)) -> 'E'(f(x1),f(suc(x1)))
% 40.32/8.57 247:15:3:[240.15,88.7,196.14,245.8,182.12,246.10]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.57 251:14:3:[96.14,89.2,135.14,248.8,170.12,249.10,237.15,250.13]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.57 252:12:3:[5.10,93.7]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.57 255:16:3:[172.17,94.6,230.15,253.8,111.15,254.13]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 40.32/8.57 257:13:3:[153.10,95.6,112.11,256.7]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 40.32/8.57 260:14:3:[209.13,96.6,170.12,258.8,146.14,259.11]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 40.32/8.57 263:13:3:[223.13,97.7,183.12,261.8,189.10,262.10]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.57 267:13:3:[110.14,98.2,126.15,264.4,116.12,265.12,177.13,266.13]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(x2)))
% 40.32/8.57 269:5:1:[215.4,99.0,52.2,268.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))
% 40.32/8.57 270:12:3:[5.9,100.6]:TopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(x2)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(x1)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0)))
% 40.32/8.57 274:15:3:[151.17,102.4,121.17,271.5,110.15,272.10,212.15,273.15]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.57 278:15:3:[114.17,104.2,188.17,275.6,140.15,276.8,133.15,277.14]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2))))
% 40.32/8.57
% 40.32/8.57 Most General Atoms: 'E'(s('0'),f(x1)) 'E'(s(s('0')),f(x2)) 'E'(f(x1),f(suc(x1))) 'E'(f(x0),f(suc(suc(x0)))) 'E'('0',f(x1)) iLEQ(suc(x0),suc(x2)) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0') 'LE'(f(x0),s(s(s('0'))))
% 40.32/8.57
% 40.32/8.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 59 atoms initially, heuristics mode: lmodel_grow ===
% 40.32/8.57
% 40.32/8.57 === Conflict found: 151:15:3:[29.15,28.4,124.13,149.8,143.14,150.12]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> '0', x1 -> '0', x2 -> '0'}
% 40.32/8.57 === Backtracking. Learning clause 279:5:1:[151.14,181.5,267.13,269.5,59.2,85.2,41.2,78.2]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 40.32/8.57 === Conflict found: 159:5:1:[117.4,33.0,68.2,158.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 -> z}
% 40.32/8.57 === Backtracking. Learning clause 280:6:1:[159.5,199.15]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))) ->
% 40.32/8.57 === Clause set with instances from active satisfied. Growing active. New size: 75
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 281:8:1:[214.9,247.14,5.9,128.5,101.2,92.1,41.1,269.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('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> 'LE'(f(suc(suc(suc(x0)))),s('0')),iLEQ(suc(x0),suc(x0))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 282:12:1:[214.9,247.14,5.9,128.5,101.2,92.1,41.1,181.1,281.8,50.1,280.6]: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('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x0),f(suc(x0))) -> 'LE'(f(x0),'0')
% 40.32/8.57 === Backtracking. Learning clause 283:11:1:[50.1,281.7,159.1]: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('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0'),iLEQ(suc(x0),suc(x0))
% 40.32/8.57 === Conflict found: 251:14:3:[96.14,89.2,135.14,248.8,170.12,249.10,237.15,250.13]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z, x2 -> z}
% 40.32/8.57 === Backtracking. Learning clause 285:16:2:[283.10,284.5,251.13,282.7]:TopTop: '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(x1)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))) -> 'LE'(f(x1),'0')
% 40.32/8.57 === Conflict found: 260:14:3:[209.13,96.6,170.12,258.8,146.14,259.11]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z, x2 -> z}
% 40.32/8.57 === Backtracking. Learning clause 286:11:1:[260.12,282.7,283.11]:Top: 'E'(f(x0),f(suc(x0))),'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('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0')
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 288:11:1:[52.2,287.1,214.8,5.9,260.12,128.5,101.2,78.1,103.1,92.1,286.8,269.3]:Top: 'E'('0',f(suc(suc(suc(x0))))),'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'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0'),iLEQ(suc(x0),suc(x0))
% 40.32/8.57 === Backtracking. Learning clause 289:10:1:[50.1,281.7,288.1]: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'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0'),iLEQ(suc(x0),suc(x0))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 290:11:1:[214.9,260.12,5.9,128.5,101.2,41.1]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s('0'))
% 40.32/8.57 === Backtracking. Learning clause 291:14:1:[103.1,279.5,286.8]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(f(x0),f(suc(x0))),'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('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0')
% 40.32/8.57 === Conflict found: 290:11:1:[214.9,260.12,5.9,128.5,101.2,41.1]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s('0')) {x0 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 293:12:1:[281.7,292.7,290.9,92.1,181.1]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'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'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(suc(suc(suc(x0)))),s('0'))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 295:6:1:[164.0,294.5,214.8,223.11,260.12,128.5,101.2,92.1]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) -> 'LE'(f(suc(suc(x0))),s(s('0')))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 296:13:1:[214.9,247.14,223.11,128.5,101.2,92.1,291.4]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0))),'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('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0')
% 40.32/8.57 === Backtracking. Learning clause 297:3:1:[91.4,62.5]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 40.32/8.57 === Conflict found: 251:14:3:[96.14,89.2,135.14,248.8,170.12,249.10,237.15,250.13]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z, x2 -> z}
% 40.32/8.57 === Backtracking. Learning clause 298:9:1:[251.13,280.1,159.5,103.2,279.5]:Top: 'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0')
% 40.32/8.57 === Clause set with instances from active satisfied. Growing active. New size: 86
% 40.32/8.57 === Clause set with instances from active satisfied. Growing active. New size: 94
% 40.32/8.57 === Backtracking. Learning clause 299:2:1:[26.1,92.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 40.32/8.57 === Backtracking. Learning clause 300:5:1:[5.1,85.2,59.2,26.3,46.3]:Top: iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'E'(f(suc(x0)),f(suc(suc(x0)))),'LE'(f(x0),s('0')),'E'(s(s('0')),f(suc(suc(suc(suc(x0))))))
% 40.32/8.57 === Backtracking. Learning clause 301:3:1:[52.4,5.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 40.32/8.57 === Conflict found: 301:3:1:[52.4,5.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0))) {x0 -> suc(suc(suc(suc(suc('0')))))}
% 40.32/8.57 === Backtracking. Learning clause 302:4:1:[301.1,78.2,59.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 40.32/8.57 === Clause set with instances from active satisfied. Growing active. New size: 130
% 40.32/8.57 === Backtracking. Learning clause 303:3:1:[101.1,92.1,62.1,299.1]:Top: iLEQ(suc(suc(x0)),suc(suc(x0))) -> 'E'(f(suc(x0)),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 40.32/8.57 === Conflict found: 223:12:3:[112.10,77.6,62.8,222.8]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))) {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 304:6:1:[223.2,101.2,299.1,164.1,85.1,301.2]:Top: 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0')),'E'(f(suc(x0)),f(suc(suc(x0))))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(suc(z)), x1 -> suc(suc(z)), x2 -> suc(suc(z))}
% 40.32/8.57 === Backtracking. Learning clause 305:6:1:[214.9,179.15,128.5,46.2,297.3,92.1,164.1,101.2,59.1,304.4,300.5]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'E'(f(suc(x0)),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 40.32/8.57 === Backtracking. Learning clause 306:3:1:[68.4,75.7]:Top: 'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 40.32/8.57 === Conflict found: 247:15:3:[240.15,88.7,196.14,245.8,182.12,246.10]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))) {x0 -> suc(suc(suc(suc(suc('0'))))), x1 -> suc(suc(suc(suc(suc('0'))))), x2 -> suc(suc(suc(suc(suc('0')))))}
% 40.32/8.57 === Backtracking. Learning clause 307:6:1:[247.14,214.9,128.5,299.1,46.2,59.1]:Top: 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s(s('0')))) -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 40.32/8.57 === Clause set with instances from active satisfied. Growing active. New size: 148
% 40.32/8.57 === Conflict found: 269:5:1:[215.4,99.0,52.2,268.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 -> suc(suc(z))}
% 40.32/8.57 === Backtracking. Learning clause 308:9:1:[269.3,307.5]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(suc(suc(suc(suc(suc(suc(x0))))))),s(s(s('0')))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s('0'))
% 40.32/8.57 === Conflict found: 181:18:3:[102.18,47.3,123.18,180.5]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> {x0 -> suc(suc(z)), x1 -> suc(suc(z)), x2 -> suc(suc(z))}
% 40.32/8.57 === Backtracking. Learning clause 309:12:1:[181.5,152.14,307.5,308.8,297.3,101.2,164.1,279.4,59.2,92.1,92.1,164.2,66.1,159.3,90.2,41.3,41.2]:Top: 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s('0'))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(suc(suc(suc(suc(z))))), x1 -> suc(suc(suc(suc(suc(z))))), x2 -> suc(suc(suc(suc(suc(z)))))}
% 40.32/8.57 === Backtracking. Learning clause 310:5:1:[214.9,247.14,128.5,46.2,299.1,297.3,101.2,92.1,92.1,164.1,279.4,164.2,66.1,306.1,90.2,41.3,301.2,46.3,299.2,101.3]:Top: 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'LE'(f(x0),'0'),'E'(f(suc(x0)),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(suc(x0))))))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(suc(suc(suc(suc(z))))), x1 -> suc(suc(suc(suc(suc(z))))), x2 -> suc(suc(suc(suc(suc(z)))))}
% 40.32/8.57 === Backtracking. Learning clause 313:2:1:[164.0,311.1,92.0,312.2,214.9,247.14,128.5,299.1,46.2,297.3,101.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 40.32/8.57 === Conflict found: 269:5:1:[215.4,99.0,52.2,268.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 -> suc(suc(z))}
% 40.32/8.57 === Backtracking. Learning clause 314:6:1:[269.2,85.2,59.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s('0'))
% 40.32/8.57 === Conflict found: 181:18:3:[102.18,47.3,123.18,180.5]:TopTopTop: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(suc(x1)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 316:4:1:[301.2,315.0,181.5,274.15,269.5]: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)) ->
% 40.32/8.57 === Conflict found: 279:5:1:[151.14,181.5,267.13,269.5,59.2,85.2,41.2,78.2]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 40.32/8.57 === Backtracking. Learning clause 317:5:1:[279.3,313.2]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s('0'))
% 40.32/8.57 === Backtracking. Learning clause 318:5:0:[103.3,65.1,159.2]:: 'LE'(f(z),s('0')),'E'('0',f(suc(suc(suc(z))))),'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))) -> iLEQ(suc(z),suc(z))
% 40.32/8.57 === Conflict found: 232:12:3:[144.10,82.1,75.8,231.7]:TopTopTop: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x0)),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))) {x0 -> z, x1 -> z, x2 -> z}
% 40.32/8.57 === Backtracking. Learning clause 319:8:0:[232.11,298.1,103.2,65.1,318.5]:: 'LE'(f(suc(suc(z))),s(s('0'))),'LE'(f(suc(z)),s(s('0'))),'LE'(f(z),s(s('0'))),'LE'(f(suc(suc(suc(z)))),s(s('0'))),'LE'(f(z),s('0')),'E'('0',f(suc(suc(suc(z))))),'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))) ->
% 40.32/8.57 === Conflict found: 313:2:1:[164.0,311.1,92.0,312.2,214.9,247.14,128.5,299.1,46.2,297.3,101.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(suc(suc(suc(z))))))}
% 40.32/8.57 === Backtracking. Learning clause 320:4:1:[313.1,92.1,317.3]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s('0'))
% 40.32/8.57 === Conflict found: 320:4:1:[313.1,92.1,317.3]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 321:8:1:[320.3,92.1,90.1,159.4,66.2,279.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 40.32/8.57 === Conflict found: 313:2:1:[164.0,311.1,92.0,312.2,214.9,247.14,128.5,299.1,46.2,297.3,101.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 322:8:1:[313.2,320.2,92.1,103.1,321.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'E'('0',f(suc(suc(suc(x0))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 40.32/8.57 === Conflict found: 319:8:0:[232.11,298.1,103.2,65.1,318.5]:: 'LE'(f(suc(suc(z))),s(s('0'))),'LE'(f(suc(z)),s(s('0'))),'LE'(f(z),s(s('0'))),'LE'(f(suc(suc(suc(z)))),s(s('0'))),'LE'(f(z),s('0')),'E'('0',f(suc(suc(suc(z))))),'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))) -> {}
% 40.32/8.57 === Backtracking. Learning clause 323:2:0:[319.3,313.2,66.2,90.2,279.5,320.4,320.4,313.2,92.1,50.2,65.1,320.4,164.2,313.2,92.1,313.2,92.1,299.2]:: 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) -> 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
% 40.32/8.57 === Conflict found: 214:18:3:[175.18,72.6,166.18,213.9]:TopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x2))))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x1)))) -> {x0 -> suc(suc(z)), x1 -> suc(suc(z)), x2 -> suc(suc(z))}
% 40.32/8.57 === Backtracking. Learning clause 325:4:1:[297.2,324.0,214.9,247.14,128.5]: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)))) ->
% 40.32/8.57 === Backtracking. Learning clause 326:5:1:[101.1,92.1,325.4,101.2,299.1,320.2,92.1,313.2,92.1,320.1]:Top: 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(suc(suc(suc(x0)))),s('0')),'LE'(f(x0),s('0'))
% 40.32/8.57 === Conflict found: 325:4:1:[297.2,324.0,214.9,247.14,128.5]: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)))) -> {x0 -> suc(suc(suc(z)))}
% 40.32/8.57 === Backtracking. Learning clause 329:3:1:[164.0,327.0,92.0,328.2,325.1,101.2,299.1]:Top: 'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0')))
% 40.32/8.57 === Conflict found: 313:2:1:[164.0,311.1,92.0,312.2,214.9,247.14,128.5,299.1,46.2,297.3,101.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 40.32/8.57 === Backtracking. Learning clause 330:3:1:[313.1,92.1,320.1]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s('0'))
% 40.32/8.57 === Backtracking. Learning clause 331:2:0:[46.1,92.1,325.3,323.2,101.2,92.1,299.1,330.1,92.1]:: 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) -> 'LE'(f(suc(suc(suc(z)))),s('0'))
% 40.32/8.57 === Conflict found: 313:2:1:[164.0,311.1,92.0,312.2,214.9,247.14,128.5,299.1,46.2,297.3,101.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(z)}
% 40.32/8.57 === Backtracking. Learning clause 332:2:1:[313.2,330.1,92.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s('0'))
% 40.32/8.57 === Conflict found: 319:8:0:[232.11,298.1,103.2,65.1,318.5]:: 'LE'(f(suc(suc(z))),s(s('0'))),'LE'(f(suc(z)),s(s('0'))),'LE'(f(z),s(s('0'))),'LE'(f(suc(suc(suc(z)))),s(s('0'))),'LE'(f(z),s('0')),'E'('0',f(suc(suc(suc(z))))),'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))) -> {}
% 40.32/8.57
% 40.32/8.57 SZS status Unsatisfiable
% 40.32/8.57
% 40.32/8.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.32/8.57
% 40.32/8.57 SPASS-SCL-FOL Statistics:
% 40.32/8.57 Number of learned clauses: 44
% 40.32/8.57 Number of propagations: 707
% 40.32/8.57 Number of decisions: 381
% 40.32/8.57 Number of resolutions: 220
% 40.32/8.57 Number of condensations: 0
% 40.32/8.57 Number of sub resolutions: 184
% 40.32/8.57 Number of input literals (deduplicated): 30
% 40.32/8.57 Number of grows: 5
% 40.32/8.57 Number of considered ground atoms: 148
% 40.32/8.57
% 40.32/8.57 Needed: 0:00:08.07
% 40.32/8.57
%------------------------------------------------------------------------------