%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO653-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 : n014.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:15 PM UTC 2026
% Result : Unsatisfiable 209.73s 42.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO653-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n014.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:56:37 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 209.73/42.51 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.73/42.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.73/42.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.73/42.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.73/42.51 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.73/42.51 Execution resolution_3 ended with status: unsatisfiable
% 209.73/42.51 Used heuristic: resolution_3
% 209.73/42.51
% 209.73/42.51 Input Clauses:
% 209.73/42.51
% 209.73/42.51 Predicates: 'E' iLEQ 'LE'
% 209.73/42.51 Fol Constants: '0' z
% 209.73/42.51 Fol Functions: suc f s
% 209.73/42.51 Problem Properties:
% 209.73/42.51 This is a full first-order problem without equality.
% 209.73/42.51
% 209.73/42.51 After reduction: Problem Properties:
% 209.73/42.51 This is a full first-order problem without equality.
% 209.73/42.51
% 209.73/42.51
% 209.73/42.51 Reduced Input Clauses:
% 209.73/42.51 92:23:4:[88.23,1.10,15.21,91.21]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 93:20:4:[18.17,2.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 95:20:4:[82.19,3.9,12.17,94.10]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 97:23:4:[49.22,4.9,77.20,96.15]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.51 99:23:4:[88.22,5.10,13.20,98.12]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 101:21:4:[27.21,6.9,67.19,100.19]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 103:22:4:[23.21,7.10,11.19,102.17]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3)))
% 209.73/42.51 105:18:4:[12.15,9.10,87.13,104.11]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 209.73/42.51 107:19:4:[25.19,10.9,29.17,106.17]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 109:19:4:[67.18,11.9,29.16,108.11]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 209.73/42.51 110:18:4:[87.13,12.9]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 113:19:4:[35.17,13.10,74.15,111.11,105.19,112.17]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 114:16:4:[8.14,14.11]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 116:20:4:[82.17,15.10,105.18,115.11]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3)))
% 209.73/42.51 118:21:4:[39.20,16.8,48.18,117.13]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 119:16:4:[8.13,17.7]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 120:18:4:[114.13,18.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 123:21:4:[68.21,19.9,35.19,121.10,95.21,122.18]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 124:5:1:[84.2,20.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))
% 209.73/42.51 126:20:4:[82.18,22.9,78.16,125.14]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 129:20:4:[116.20,23.10,95.19,127.11,105.18,128.12]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x3),f(suc(x3)))
% 209.73/42.51 131:16:4:[114.16,24.7,8.14,130.13]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 209.73/42.51 133:18:4:[120.15,25.9,114.13,132.10]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 135:21:4:[39.21,26.8,36.19,134.18]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0))))
% 209.73/42.51 137:20:4:[93.17,27.9,133.18,136.10]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 139:18:4:[81.16,28.8,119.14,138.12]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 141:16:4:[63.13,29.9,8.11,140.10]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 209.73/42.51 144:20:4:[137.20,31.9,133.18,142.11,109.20,143.18]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 146:18:4:[110.16,32.9,63.14,145.12]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 148:21:4:[64.21,33.8,86.19,147.18]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0)))
% 209.73/42.51 150:23:4:[123.23,34.9,135.21,149.13]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0))))
% 209.73/42.51 152:19:4:[74.15,35.9,120.16,151.10]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 154:18:4:[81.17,36.8,87.15,153.9]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 156:24:4:[92.23,37.10,97.23,155.13]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x3),f(suc(suc(x3)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 158:20:4:[152.20,38.9,110.18,157.17]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 209.73/42.51 161:19:4:[60.19,39.8,74.17,159.9,154.19,160.16]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 163:20:4:[60.20,40.8,81.18,162.17]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.51 166:18:4:[105.17,41.10,146.17,164.12,141.15,165.14]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 209.73/42.51 168:24:4:[99.23,42.10,118.21,167.16]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 171:20:4:[113.21,43.10,158.19,169.11,105.19,170.19]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 174:20:4:[113.19,44.10,133.17,172.14,166.20,173.19]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 176:19:4:[154.18,45.8,139.18,175.10]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 209.73/42.51 179:20:4:[163.20,46.8,58.18,177.13,139.19,178.19]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.51 182:20:4:[158.20,47.9,89.18,180.13,146.19,181.19]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x1),f(suc(x1)))
% 209.73/42.51 184:18:4:[85.17,48.7,114.15,183.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.51 186:22:4:[68.22,49.9,158.21,185.10]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.51 189:22:4:[88.21,51.10,174.21,187.13,137.19,188.16]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.51 191:19:4:[184.19,52.7,131.17,190.9]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0)))
% 209.73/42.52 194:21:4:[68.20,53.9,93.18,192.14,126.21,193.19]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 195:2:1:[30.0,54.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 209.73/42.52 198:20:4:[95.20,55.9,126.20,196.11,146.18,197.12]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 201:24:4:[71.25,56.10,168.25,199.12,103.23,200.24]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) ->
% 209.73/42.52 204:19:4:[152.18,57.9,120.16,202.12,146.19,203.17]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 207:17:4:[85.18,58.7,131.17,205.8,119.16,206.15]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.52 208:20:4:[74.17,60.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 212:20:4:[171.21,61.10,174.22,209.12,107.19,210.15,166.20,211.21]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(x2)))
% 209.73/42.52 216:22:4:[150.24,62.9,97.24,213.12,182.22,214.13,198.22,215.22]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.52 217:16:4:[8.11,63.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 220:19:4:[93.19,64.8,120.17,218.9,184.17,219.11]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 223:21:4:[135.22,65.8,118.22,221.10,191.20,222.14]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3)))
% 209.73/42.52 227:20:4:[144.22,66.9,101.22,224.10,107.20,225.12,109.20,226.20]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1)))
% 209.73/42.52 230:17:4:[78.15,67.9,141.16,228.10,119.13,229.12]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3)))
% 209.73/42.52 232:21:4:[152.19,68.9,208.17,231.11]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 234:16:4:[119.15,69.7,8.13,233.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 236:19:4:[90.18,70.8,131.16,235.11]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x2),f(suc(suc(x2)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 209.73/42.52 240:22:4:[99.24,71.10,92.24,237.11,171.22,238.13,227.23,239.16]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.52 243:19:4:[208.18,72.8,85.16,241.12,139.19,242.17]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 247:19:4:[116.19,73.10,126.19,244.12,166.19,245.13,230.17,246.16]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3)))
% 209.73/42.52 248:18:4:[114.14,74.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 250:16:4:[87.14,76.8,8.12,249.10]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 252:20:4:[93.20,77.8,207.17,251.11]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 209.73/42.52 254:17:4:[217.15,78.8,119.13,253.10]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 258:21:4:[123.22,79.9,194.22,255.11,204.20,256.12,220.20,257.15]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 260:5:1:[124.4,80.4,84.2,259.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 209.73/42.52 262:17:4:[87.15,81.8,119.14,261.10]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 265:18:4:[110.17,82.9,262.15,263.11,254.16,264.12]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 268:17:4:[248.16,83.8,114.14,266.10,250.17,267.15]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 270:17:4:[114.15,85.7,119.16,269.13]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 209.73/42.52 273:17:4:[254.17,86.8,217.15,271.9,234.15,272.11]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 274:16:4:[8.12,87.8]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 209.73/42.52 277:21:4:[232.19,88.10,113.20,275.11,208.17,276.13]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x3),f(suc(suc(x3))))
% 209.73/42.52 280:17:4:[120.18,89.8,131.15,278.9,217.16,279.15]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x3)))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(suc(x3)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 209.73/42.52 283:17:4:[248.18,90.8,131.16,281.9,274.16,282.15]:TopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x3))),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(x2)),'E'('0',f(suc(x1))),iLEQ(suc(x3),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 209.73/42.52
% 209.73/42.52 Most General Atoms: 'E'('0',f(x2)) 'E'(f(x3),f(suc(x3))) iLEQ(suc(x3),suc(x0)) 'E'(f(x3),f(suc(suc(x3)))) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0')
% 209.73/42.52
% 209.73/42.52 === Starting SPASS-SCL-FOL A Little Less Naive, considering 13 atoms initially, heuristics mode: resolution_3 ===
% 209.73/42.52
% 209.73/42.52 === Conflict found: 195:2:1:[30.0,54.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0') {x0 -> z}
% 209.73/42.52 === Backtracking. Learning clause 284:1:0:[195.2,21.1]:: -> 'E'('0',f(z))
% 209.73/42.52 === Conflict found: 201:24:4:[71.25,56.10,168.25,199.12,103.23,200.24]:TopTopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x2))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x3))))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(suc(suc(x2))))),iLEQ(suc(x1),suc(x2)) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 209.73/42.52 === Backtracking. Learning clause 286:5:1:[260.4,285.5,201.12,232.18]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))) ->
% 209.73/42.52 === Backtracking. Learning clause 288:4:1:[195.0,287.2,59.1,30.1,286.1,8.12]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),'0')
% 209.73/42.52 === Backtracking. Learning clause 289:3:1:[75.1,30.1,288.1]:Top: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),'0')
% 209.73/42.52 === Backtracking. Learning clause 292:3:1:[195.0,290.2,288.2,291.4,59.1,30.1,260.1]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))) -> 'LE'(f(x0),'0')
% 209.73/42.52 === Backtracking. Learning clause 293:2:1:[75.1,30.1,292.2]:Top: 'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0')
% 209.73/42.52 === Backtracking. Learning clause 294:1:1:[50.1,30.1,293.1]:Top: -> 'LE'(f(x0),'0')
% 209.73/42.52 === Conflict found: 294:1:1:[50.1,30.1,293.1]:Top: -> 'LE'(f(x0),'0') {x0 -> z}
% 209.73/42.52
% 209.73/42.52 SZS status Unsatisfiable
% 209.73/42.52
% 209.73/42.52 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.73/42.52
% 209.73/42.52 SPASS-SCL-FOL Statistics:
% 209.73/42.52 Number of learned clauses: 7
% 209.73/42.52 Number of propagations: 33
% 209.73/42.52 Number of decisions: 18
% 209.73/42.52 Number of resolutions: 14
% 209.73/42.52 Number of condensations: 1
% 209.73/42.52 Number of sub resolutions: 197
% 209.73/42.52 Number of input literals (deduplicated): 14
% 209.73/42.52 Number of grows: 0
% 209.73/42.52 Number of considered ground atoms: 13
% 209.73/42.52
% 209.73/42.52 Needed: 0:0:41.98
% 209.73/42.52
%------------------------------------------------------------------------------