%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO687-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 4.51s 1.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYO687-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.35 % Computer : n011.cluster.edu
% 0.18/0.35 % Model : x86_64 x86_64
% 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35 % Memory : 8042.1875MB
% 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.35 % DateTime : Thu May 7 13:55:48 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 SPASS-SCL-FOL version:
% 0.20/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 4.51/1.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.51/1.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.51/1.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.51/1.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.51/1.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.51/1.61 Execution normal ended with status: unsatisfiable
% 4.51/1.61 Used heuristic: normal
% 4.51/1.61
% 4.51/1.61 Input Clauses:
% 4.51/1.61
% 4.51/1.61 Predicates: 'E' iLEQ 'LE'
% 4.51/1.61 Fol Constants: '0' z
% 4.51/1.61 Fol Functions: s f suc
% 4.51/1.61 Problem Properties:
% 4.51/1.61 This is a full first-order problem without equality.
% 4.51/1.61
% 4.51/1.61 After reduction: Problem Properties:
% 4.51/1.61 This is a full first-order problem without equality.
% 4.51/1.61
% 4.51/1.61
% 4.51/1.61 Reduced Input Clauses:
% 4.51/1.61 129:13:2:[48.11,1.6,94.9,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'(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(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.61 130:10:2:[19.6,2.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))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.61 132:11:2:[93.10,4.3,119.8,131.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'(f(x1),f(suc(x1))),'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)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.61 135:11:2:[93.10,5.3,132.12,133.5,119.8,134.10]: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(suc(x0)))))),'E'(f(x1),f(suc(x1))),'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))))
% 4.51/1.61 138:14:2:[47.15,7.1,112.13,136.8,81.11,137.11]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(f(x0),f(suc(suc(x0)))),'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(suc(suc(suc(x1)))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(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))) ->
% 4.51/1.61 140:10:2:[19.6,10.0,130.10,139.8]:TopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(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)))
% 4.51/1.61 141:7:1:[31.2,11.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)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.61 143:6:1:[117.4,12.1,28.2,142.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)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.61 144:15:2:[121.11,14.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(suc(x1)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),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)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.61 146:10:2:[119.7,16.4,29.5,145.7]: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(suc(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(x1),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.61 148:9:2:[126.7,17.5,53.5,147.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 4.51/1.61 149:15:2:[122.9,20.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'(f(x0),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)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.61 151:14:2:[127.10,21.0,140.11,150.13]:TopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(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'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.61 152:14:2:[122.9,23.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)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 153:11:2:[56.5,24.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'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(x1)))
% 4.51/1.62 155:11:2:[93.9,25.3,110.7,154.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 158:6:1:[117.4,26.2,28.2,156.4,143.6,157.6]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(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))
% 4.51/1.62 159:10:2:[87.7,30.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'(s(s(s(s('0')))),f(x1)),'E'(f(x0),f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 162:9:2:[148.9,33.3,126.7,160.6,53.5,161.8]: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(suc(suc(suc(suc(x1)))))),'E'(s(s(s(s('0')))),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.62 165:6:1:[120.6,35.0,75.4,163.3,22.2,164.5]: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(suc(suc(suc(suc(x0)))))),'E'(s(s(s(s('0')))),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 4.51/1.62 169:13:2:[44.15,36.4,100.13,166.7,99.11,167.9,162.11,168.16]: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(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(suc(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'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))) ->
% 4.51/1.62 171:7:1:[80.4,37.0,32.2,170.7]: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(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0))
% 4.51/1.62 172:8:1:[27.2,39.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> iLEQ(suc(x0),suc(x0))
% 4.51/1.62 173:8:2:[19.5,40.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)))
% 4.51/1.62 176:11:2:[85.12,41.1,73.10,174.6,69.8,175.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(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(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 179:9:2:[123.10,42.1,60.8,177.6,124.6,178.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x1)))))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.62 180:8:2:[19.6,43.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))))
% 4.51/1.62 184:12:2:[100.13,44.6,99.11,181.8,129.14,182.9,148.10,183.14]: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'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 186:10:2:[110.8,45.3,29.6,185.8]:TopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(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)))
% 4.51/1.62 188:10:2:[19.5,46.8,173.7,187.10]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),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(x0),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(x1)))
% 4.51/1.62 190:14:2:[85.11,47.1,123.9,189.14]: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'(f(x1),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(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(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 192:11:2:[94.9,48.6,159.10,191.7]: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'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 194:11:2:[173.8,50.0,130.9,193.10]: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'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 196:9:2:[110.8,51.3,29.6,195.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))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 198:9:2:[69.7,52.1,124.5,197.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(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 4.51/1.62 200:9:2:[119.7,54.3,29.5,199.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 4.51/1.62 203:12:2:[127.10,57.0,130.9,201.11,194.11,202.12]: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'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 204:7:1:[27.2,59.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)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.62 205:8:2:[124.6,60.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))))
% 4.51/1.62 207:13:2:[85.11,61.1,198.10,206.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(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(f(x1),f(suc(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(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 208:10:2:[116.7,62.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))))
% 4.51/1.62 210:9:2:[173.8,63.0,180.7,209.8]:TopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 211:10:2:[56.5,64.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(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 4.51/1.62 214:13:2:[132.11,65.4,196.9,212.8,146.11,213.11]: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(suc(suc(x1)))))),'E'(f(x0),f(suc(suc(x0)))),'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(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 216:11:2:[116.7,66.1,208.9,215.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(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 4.51/1.62 219:11:2:[116.7,67.1,216.11,217.7,208.9,218.9]: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'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 4.51/1.62 220:8:2:[124.5,69.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)))
% 4.51/1.62 222:11:2:[122.9,70.1,208.10,221.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)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 226:12:2:[188.11,71.1,130.9,223.12,203.13,224.13,194.11,225.14]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x1)))),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(suc(suc(x1))))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 229:10:2:[127.10,72.0,180.7,227.9,210.9,228.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(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 231:9:2:[220.8,73.4,205.7,230.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 4.51/1.62 235:11:2:[132.11,74.3,155.12,232.4,196.9,233.7,200.10,234.10]: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(suc(suc(suc(x0))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 236:5:1:[22.2,75.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))
% 4.51/1.62 239:14:2:[135.13,76.4,214.15,237.7,146.11,238.13]: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(suc(suc(x1)))))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(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(x1),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 4.51/1.62 240:5:1:[27.2,77.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))
% 4.51/1.62 244:12:2:[207.14,78.1,176.13,241.2,198.10,242.10,179.11,243.14]: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'(f(x1),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(suc(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(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 248:10:2:[188.11,79.1,180.7,245.10,229.11,246.11,210.9,247.12]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x1)))),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(suc(x1))))
% 4.51/1.62 250:4:1:[32.2,80.2,231.0,249.5]: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))))
% 4.51/1.62 253:9:2:[220.7,81.1,198.9,251.7,124.5,252.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'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 4.51/1.62 255:15:2:[188.11,82.1,248.13,254.10]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x1)))))),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(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(x0)))) ->
% 4.51/1.62 259:12:2:[135.13,84.3,155.12,256.4,235.14,257.6,200.10,258.12]: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(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'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 320:9:2:[19.5,127.7,173.7,319.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(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 4.51/1.62 318:8:2:[53.5,126.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)))
% 4.51/1.62 260:8:2:[53.6,87.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))))
% 4.51/1.62 262:4:1:[31.2,91.2,210.2,261.5]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 265:10:2:[159.9,92.6,260.7,263.8,148.10,264.10]: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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 266:10:2:[110.7,93.5]:TopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 268:9:2:[260.8,94.5,53.6,267.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))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 271:11:2:[266.9,96.4,110.7,269.7,146.11,270.9]: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(suc(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(x1),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 275:12:2:[129.13,97.4,192.11,272.7,268.9,273.9,162.11,274.14]: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(suc(suc(suc(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(suc(suc(x0)))))
% 4.51/1.62 277:6:1:[250.4,98.0,32.2,276.5]: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)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.62 280:9:2:[268.10,99.5,260.8,278.6,53.6,279.10]: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'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(x1)))
% 4.51/1.62 283:11:2:[280.11,100.6,192.12,281.7,159.10,282.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'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1))))
% 4.51/1.62 286:11:2:[121.11,101.1,222.12,284.8,208.10,285.12]: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(suc(x1)))))),'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))))
% 4.51/1.62 287:2:1:[18.0,102.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 291:13:2:[121.11,103.1,144.15,288.8,286.13,289.12,219.13,290.15]: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(suc(x1)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) ->
% 4.51/1.62 295:10:2:[265.11,105.4,159.9,292.7,260.7,293.9,162.11,294.12]: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(suc(suc(suc(suc(x1)))))),'E'(s(s(s(s('0')))),f(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 296:8:2:[29.6,110.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))))
% 4.51/1.62 299:11:2:[231.9,112.1,253.11,297.7,205.7,298.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(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(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(x1),f(suc(suc(x1))))
% 4.51/1.62 301:12:2:[173.8,113.0,210.10,300.8]:TopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(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'(f(x0),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))))
% 4.51/1.62 302:8:2:[56.5,115.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)))
% 4.51/1.62 303:8:2:[56.6,116.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))))
% 4.51/1.62 304:5:1:[28.2,117.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))
% 4.51/1.62 307:6:1:[31.2,118.5,141.6,305.6,262.4,306.7]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0))
% 4.51/1.62 308:8:2:[29.5,119.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)))
% 4.51/1.62 310:6:1:[236.4,120.2,22.2,309.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)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.62 313:9:2:[122.10,121.6,56.6,311.8,303.8,312.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(suc(suc(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)))
% 4.51/1.62 315:9:2:[56.6,122.6,303.8,314.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))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62 317:9:2:[205.8,123.5,124.6,316.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))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 4.51/1.62
% 4.51/1.62 Most General Atoms: 'E'(s(s(s(s('0')))),f(x1)) 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'('0',f(x0)) 'E'(f(x1),f(suc(x1))) 'LE'(f(x0),s(s(s('0')))) 'E'(s(s('0')),f(x1)) 'E'(f(x1),f(suc(suc(x1)))) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) iLEQ(suc(x0),suc(x1)) 'E'(s(s(s('0'))),f(x0)) 'LE'(f(x0),'0') 'E'(s('0'),f(x1)) 'LE'(f(x0),s(s(s(s('0'))))) 'LE'(f(x0),s(s(s(s(s('0'))))))
% 4.51/1.62
% 4.51/1.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 57 atoms initially, heuristics mode: normal ===
% 4.51/1.62
% 4.51/1.62 === Conflict found: 275:12:2:[129.13,97.4,192.11,272.7,268.9,273.9,162.11,274.14]: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(suc(suc(suc(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(suc(suc(x0))))) {x0 -> '0', x1 -> '0'}
% 4.51/1.62 === Backtracking. Learning clause 322:6:1:[165.5,321.2,275.12,169.8,159.9]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(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)),'E'(f(x0),f(suc(x0))) ->
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 121
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 185
% 4.51/1.62 === Conflict found: 159:10:2:[87.7,30.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'(s(s(s(s('0')))),f(x1)),'E'(f(x0),f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))) {x0 -> s('0'), x1 -> s('0')}
% 4.51/1.62 === Backtracking. Learning clause 323:4:1:[159.8,318.8,236.5]: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))))
% 4.51/1.62 === Conflict found: 323:4:1:[159.8,318.8,236.5]: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)))) {x0 -> s('0')}
% 4.51/1.62 === Backtracking. Learning clause 324:4:1:[323.3,287.1,89.2]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 === Backtracking. Learning clause 325:3:1:[28.4,29.4]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 249
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 313
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 377
% 4.51/1.62 === Backtracking. Learning clause 327:7:1:[287.0,326.1,34.1,18.1,322.2,325.3,111.2]:Top: 'E'(s(s(s(s('0')))),f(suc(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('0')),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'LE'(f(x0),s(s('0')))
% 4.51/1.62 === Backtracking. Learning clause 329:7:1:[287.0,328.2,56.1,165.6,322.6,34.2,18.1,88.2]:Top: 'E'(s('0'),f(x0)),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 280:9:2:[268.10,99.5,260.8,278.6,53.6,279.10]: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'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(x1))) {x0 -> suc('0'), x1 -> suc('0')}
% 4.51/1.62 === Backtracking. Learning clause 331:4:1:[287.0,330.1,280.2,165.6,322.6,34.2,18.1]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'LE'(f(suc(suc(x0))),s(s(s(s('0')))))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 441
% 4.51/1.62 === Backtracking. Learning clause 332:4:1:[89.1,18.1,106.1,9.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 4.51/1.62 === Backtracking. Learning clause 334:5:1:[287.0,333.3,15.1,18.1,165.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))) -> 'LE'(f(x0),s(s(s(s('0'))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.62 === Conflict found: 322:6:1:[165.5,321.2,275.12,169.8,159.9]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(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)),'E'(f(x0),f(suc(x0))) -> {x0 -> s('0')}
% 4.51/1.62 === Backtracking. Learning clause 335:4:1:[322.6,53.6,15.2,334.5,18.1,34.2,49.2,287.1,89.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 === Conflict found: 171:7:1:[80.4,37.0,32.2,170.7]: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(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc('0')}
% 4.51/1.62 === Backtracking. Learning clause 336:7:1:[171.5,277.5,114.2,107.2,108.2,106.2,3.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'LE'(f(x0),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s(s('0'))))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 505
% 4.51/1.62 === Backtracking. Learning clause 337:3:1:[89.1,18.1,331.1]:Top: 'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'LE'(f(suc(suc(x0))),s(s(s(s('0')))))
% 4.51/1.62 === Conflict found: 240:5:1:[27.2,77.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)) {x0 -> s('0')}
% 4.51/1.62 === Backtracking. Learning clause 338:7:1:[240.2,88.2,88.2,125.3,111.3]:Top: 'E'(s('0'),f(x0)),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0')),'E'(s(s('0')),f(suc(suc(suc(x0)))))
% 4.51/1.62 === Backtracking. Learning clause 339:3:1:[32.4,124.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.62 === Conflict found: 240:5:1:[27.2,77.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)) {x0 -> f('0')}
% 4.51/1.62 === Backtracking. Learning clause 340:6:1:[240.4,204.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 569
% 4.51/1.62 === Backtracking. Learning clause 341:3:1:[34.1,18.1,337.1,89.2]:Top: 'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 === Conflict found: 310:6:1:[236.4,120.2,22.2,309.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)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 4.51/1.62 === Backtracking. Learning clause 343:6:1:[323.3,342.2,310.6,129.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'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 === Conflict found: 339:3:1:[32.4,124.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0))) {x0 -> z}
% 4.51/1.62 === Backtracking. Learning clause 344:6:1:[339.2,106.2,107.2,9.1,6.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(x0),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 304:5:1:[28.2,117.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)) {x0 -> s(z)}
% 4.51/1.62 === Backtracking. Learning clause 345:6:1:[304.2,125.2,9.2,106.3,3.3,111.2,107.3,250.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(suc(x0))))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 633
% 4.51/1.62 === Conflict found: 335:4:1:[322.6,53.6,15.2,334.5,18.1,34.2,49.2,287.1,89.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(f(z))}
% 4.51/1.62 === Backtracking. Learning clause 346:3:1:[335.2,18.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 === Conflict found: 346:3:1:[335.2,18.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(f(z))}
% 4.51/1.62 === Backtracking. Learning clause 347:2:1:[346.2,18.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 === Conflict found: 335:4:1:[322.6,53.6,15.2,334.5,18.1,34.2,49.2,287.1,89.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(x0)),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc(f(z))}
% 4.51/1.62 === Backtracking. Learning clause 348:1:1:[335.1,18.1,18.1,18.1]:Top: -> 'LE'(f(x0),s(s(s(s('0')))))
% 4.51/1.62 === Conflict found: 207:13:2:[85.11,61.1,198.10,206.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(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(f(x1),f(suc(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(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> f(z), x1 -> f(z)}
% 4.51/1.62 === Backtracking. Learning clause 354:2:1:[348.0,349.0,348.0,350.2,348.0,351.3,348.0,352.4,348.0,353.5,207.12,138.10,336.6,250.4,339.3,108.2,114.2,106.2,3.2]:Top: 'E'(s(s(s('0'))),f(x0)) -> 'LE'(f(x0),s(s(s('0'))))
% 4.51/1.62 === Backtracking. Learning clause 356:1:1:[348.0,355.0,107.2,354.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 4.51/1.62 === Conflict found: 239:14:2:[135.13,76.4,214.15,237.7,146.11,238.13]: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(suc(suc(x1)))))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(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(x1),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> z, x1 -> z}
% 4.51/1.62 === Backtracking. Learning clause 362:1:1:[356.0,357.0,356.0,358.1,356.0,359.2,356.0,360.3,356.0,361.4,239.5,135.11,235.10,325.3,158.6,125.2,38.2,111.2,58.2,9.2]:Top: -> 'LE'(f(x0),s(s('0')))
% 4.51/1.62 === Conflict found: 208:10:2:[116.7,62.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)))) {x0 -> suc(z), x1 -> suc(z)}
% 4.51/1.62 === Backtracking. Learning clause 363:5:1:[208.9,152.9,315.8,340.6]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 === Conflict found: 291:13:2:[121.11,103.1,144.15,288.8,286.13,289.12,219.13,290.15]: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(suc(x1)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> {x0 -> f('0'), x1 -> f('0')}
% 4.51/1.62 === Backtracking. Learning clause 365:8:1:[362.0,364.5,291.1,240.5,363.5,6.2,83.1]:Top: 'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(x0))),'LE'(f(suc(x0)),'0')
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 697
% 4.51/1.62 === Backtracking. Learning clause 366:3:1:[31.4,19.1]:Top: 'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 761
% 4.51/1.62 === Backtracking. Learning clause 368:3:1:[362.0,367.1,56.1,27.4,95.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 291:13:2:[121.11,103.1,144.15,288.8,286.13,289.12,219.13,290.15]: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(suc(x1)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> {x0 -> suc(z), x1 -> suc(z)}
% 4.51/1.62 === Backtracking. Learning clause 370:6:1:[363.4,369.2,291.11,313.9,172.8]: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)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) ->
% 4.51/1.62 === Conflict found: 208:10:2:[116.7,62.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)))) {x0 -> suc(z), x1 -> suc(z)}
% 4.51/1.62 === Backtracking. Learning clause 377:5:1:[362.0,371.0,362.0,372.1,362.0,373.2,362.0,374.3,348.0,375.4,348.0,376.5,208.7,302.8,240.5,370.4,55.2,362.1,88.2,95.2,109.2,6.2,8.1,31.2,83.2,344.6]:Top: -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s('0'),f(x0))
% 4.51/1.62 === Backtracking. Learning clause 379:4:1:[362.0,378.0,8.2,366.1,6.3,83.2,88.3,27.2,377.5]:Top: -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x0))
% 4.51/1.62 === Backtracking. Learning clause 380:2:1:[6.1,362.1]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 4.51/1.62 === Backtracking. Learning clause 382:4:1:[362.0,381.1,95.1,362.1,370.1,88.2,362.1,109.2,362.1,55.2,362.1,380.1,8.1,366.1,83.2,6.3]:Top: 'E'(f(suc(x0)),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0'),'E'(s('0'),f(x0))
% 4.51/1.62 === Backtracking. Learning clause 383:4:1:[88.1,362.1,83.1,366.2,8.2,380.2,27.2,382.4]:Top: 'E'(f(suc(x0)),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0')
% 4.51/1.62 === Backtracking. Learning clause 384:3:1:[88.1,362.1,83.1,366.2,8.2,380.2]:Top: -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(x0)))
% 4.51/1.62 === Backtracking. Learning clause 386:3:1:[380.0,385.0,95.1,362.1,240.1,88.2,362.1]:Top: -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 208:10:2:[116.7,62.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)))) {x0 -> suc(z), x1 -> suc(z)}
% 4.51/1.62 === Backtracking. Learning clause 387:2:0:[208.7,56.6,88.2,362.1,95.2,362.1,386.2,383.1,8.1,366.1,83.2,380.2,27.1,384.3,68.1]:: -> iLEQ(suc(z),suc(z)),'E'(f(z),f(suc(z)))
% 4.51/1.62 === Backtracking. Learning clause 388:2:1:[88.1,362.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 4.51/1.62 === Backtracking. Learning clause 389:2:0:[8.3,68.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 4.51/1.62 === Conflict found: 315:9:2:[56.6,122.6,303.8,314.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))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> f(z), x1 -> f(z)}
% 4.51/1.62 === Backtracking. Learning clause 392:5:1:[362.0,390.1,362.0,391.2,315.2,384.3,380.1,109.2,95.2,83.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(x0))),'E'('0',f(x0)),'LE'(f(x0),'0')
% 4.51/1.62 === Backtracking. Learning clause 394:2:1:[362.0,393.0,109.2,368.1]:Top: -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 141:7:1:[31.2,11.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)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)) {x0 -> f(z)}
% 4.51/1.62 === Backtracking. Learning clause 396:5:1:[262.3,395.2,141.7,203.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 825
% 4.51/1.62 === Backtracking. Learning clause 397:2:1:[95.1,362.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 208:10:2:[116.7,62.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)))) {x0 -> suc(suc(suc(z))), x1 -> suc(suc(suc(z)))}
% 4.51/1.62 === Backtracking. Learning clause 398:4:1:[208.7,302.8,240.5]: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))))
% 4.51/1.62 === Backtracking. Learning clause 400:8:1:[362.0,399.3,104.2,307.1,388.2,90.2,95.3,398.1]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(suc(x0)))))))
% 4.51/1.62 === Backtracking. Learning clause 401:7:1:[104.2,307.1,380.2,90.2,388.2,400.4,13.2,380.2]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)),'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 4.51/1.62 === Conflict found: 396:5:1:[262.3,395.2,141.7,203.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> f(z)}
% 4.51/1.62 === Backtracking. Learning clause 403:3:1:[362.0,402.0,396.3,8.2,90.2,13.2,388.2,83.2,380.2,95.3,109.3]:Top: -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0)))))
% 4.51/1.62 === Conflict found: 262:4:1:[31.2,91.2,210.2,261.5]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> s('0')}
% 4.51/1.62 === Backtracking. Learning clause 404:5:1:[262.1,13.2,8.2,83.2]:Top: 'LE'(f(suc(suc(x0))),s('0')),'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0')) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),'0')
% 4.51/1.62 === Backtracking. Learning clause 405:3:1:[27.4,56.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 4.51/1.62 === Clause set with instances from active satisfied. Growing active. New size: 889
% 4.51/1.62 === Backtracking. Learning clause 409:3:1:[397.0,406.1,380.0,407.2,362.0,408.3,109.1,362.1,370.6,398.4,6.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))) -> 'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 409:3:1:[397.0,406.1,380.0,407.2,362.0,408.3,109.1,362.1,370.6,398.4,6.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))) -> 'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(z)))}
% 4.51/1.62 === Backtracking. Learning clause 410:2:1:[409.1,397.1]:Top: -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0'))
% 4.51/1.62 === Conflict found: 370:6:1:[363.4,369.2,291.11,313.9,172.8]: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)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> {x0 -> s(s('0'))}
% 4.51/1.62 === Backtracking. Learning clause 413:1:1:[362.0,411.0,362.0,412.1,370.2,109.2,398.4,388.1,397.1,55.2,380.1]:Top: -> 'LE'(f(x0),s('0'))
% 4.51/1.62 === Conflict found: 255:15:2:[188.11,82.1,248.13,254.10]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x1)))))),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(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(x0)))) -> {x0 -> z, x1 -> z}
% 4.51/1.62 === Backtracking. Learning clause 418:2:0:[413.0,414.0,413.0,415.1,413.0,416.4,413.0,417.5,255.15,404.4,396.5,307.6,366.3,13.2,413.1,90.2,104.2,68.1]:: 'E'('0',f(suc(z))),'E'('0',f(z)) ->
% 4.51/1.62
% 4.51/1.62 SZS status Unsatisfiable
% 4.51/1.62
% 4.51/1.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.51/1.62
% 4.51/1.62 SPASS-SCL-FOL Statistics:
% 4.51/1.62 Number of learned clauses: 54
% 4.51/1.62 Number of propagations: 5492
% 4.51/1.62 Number of decisions: 3334
% 4.51/1.62 Number of resolutions: 221
% 4.51/1.62 Number of condensations: 1
% 4.51/1.62 Number of sub resolutions: 237
% 4.51/1.62 Number of input literals (deduplicated): 57
% 4.51/1.62 Number of grows: 13
% 4.51/1.62 Number of considered ground atoms: 889
% 4.51/1.62
% 4.51/1.62 Needed: 0:00:01.05
% 4.51/1.62
%------------------------------------------------------------------------------