%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO651-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 : n006.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:14 PM UTC 2026
% Result : Unsatisfiable 7.81s 2.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO651-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n006.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:17 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]
% 7.81/2.12 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/2.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/2.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/2.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/2.12 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/2.12 Execution normal ended with status: unsatisfiable
% 7.81/2.12 Used heuristic: normal
% 7.81/2.12
% 7.81/2.12 Input Clauses:
% 7.81/2.12
% 7.81/2.12 Predicates: 'E' iLEQ 'LE'
% 7.81/2.12 Fol Constants: '0' z
% 7.81/2.12 Fol Functions: suc f s
% 7.81/2.12 Problem Properties:
% 7.81/2.12 This is a full first-order problem without equality.
% 7.81/2.12
% 7.81/2.12 After reduction: Problem Properties:
% 7.81/2.12 This is a full first-order problem without equality.
% 7.81/2.12
% 7.81/2.12
% 7.81/2.12 Reduced Input Clauses:
% 7.81/2.12 76:23:3:[24.18,1.5]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 7.81/2.12 77:23:3:[53.19,2.5]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 80:6:1:[46.6,3.2,67.4,78.5,74.2,79.6]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(suc(x0)))))) -> iLEQ(suc(x0),suc(x0))
% 7.81/2.12 81:19:3:[40.17,4.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 82:21:3:[43.16,5.5]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 7.81/2.12 83:14:3:[58.10,6.7]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 84:20:3:[43.16,7.5]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 85:18:3:[17.16,8.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 87:20:3:[17.16,9.4,85.18,86.13]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 7.81/2.12 88:19:3:[65.14,10.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 7.81/2.12 89:19:3:[38.14,12.4]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 7.81/2.12 91:21:3:[40.17,13.4,87.21,90.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1))))
% 7.81/2.12 93:19:3:[17.16,15.4,85.18,92.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 95:20:3:[50.19,16.5,81.18,94.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 97:15:3:[65.12,17.8,83.13,96.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 100:13:3:[65.13,18.8,58.11,98.10,29.9,99.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 101:12:3:[29.10,19.3]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 103:21:3:[24.18,20.5,93.18,102.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 104:12:3:[29.8,21.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 105:19:3:[51.17,22.5]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 106:16:3:[58.12,23.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 108:17:3:[97.14,24.8,65.12,107.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 109:16:3:[83.14,25.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 112:19:3:[51.17,26.5,84.18,110.6,106.14,111.12]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 114:16:3:[54.15,27.4,101.10,113.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 117:21:3:[50.19,28.5,103.21,115.14,84.19,116.17]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 120:22:3:[34.20,30.5,117.22,118.6,112.20,119.18]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 122:17:3:[83.14,31.4,106.14,121.9]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 124:15:3:[65.14,32.4,101.11,123.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 126:17:3:[43.16,33.5,109.14,125.9]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 129:18:3:[50.18,34.5,40.16,127.9,100.14,128.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(x2)))
% 7.81/2.12 132:20:3:[51.17,35.5,82.20,130.6,112.21,131.13]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 7.81/2.12 134:17:3:[65.14,37.4,124.16,133.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 136:13:3:[104.10,38.6,29.8,135.8]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 140:14:3:[100.14,40.8,97.15,137.10,83.13,138.12,104.11,139.14]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 142:14:3:[29.10,41.3,101.12,141.9]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 7.81/2.12 145:22:3:[50.19,42.5,91.22,143.10,95.21,144.17]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 7.81/2.12 148:14:3:[83.12,43.7,58.10,146.9,136.13,147.12]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 152:21:3:[53.19,45.5,76.22,149.6,87.20,150.11,88.18,151.13]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 7.81/2.12 154:6:1:[67.4,46.4,74.2,153.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 7.81/2.12 157:18:3:[100.15,47.4,88.19,155.10,142.15,156.18]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1)))
% 7.81/2.12 160:17:3:[100.15,48.4,134.17,158.10,106.15,159.13]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 163:18:3:[54.15,49.4,89.18,161.5,142.14,162.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 7.81/2.12 168:15:3:[140.16,50.8,100.14,164.10,108.17,165.12,148.15,166.14,136.13,167.16]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 171:15:3:[148.14,51.5,83.12,169.8,58.10,170.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 173:13:3:[29.10,52.3,101.12,172.8]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 177:16:3:[108.16,53.5,97.14,174.9,65.12,175.11,171.16,176.13]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 180:13:3:[136.12,54.4,104.10,178.7,29.8,179.9]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 183:20:3:[129.20,55.5,95.20,181.6,81.18,182.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 185:16:3:[104.12,56.3,142.14,184.8]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 7.81/2.12 186:2:1:[14.0,57.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 7.81/2.12 187:12:3:[29.9,58.8]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 190:15:3:[100.15,59.4,124.15,188.10,101.11,189.14]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 192:17:3:[136.14,60.4,173.12,191.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 195:18:3:[108.18,62.5,85.16,193.10,124.14,194.12]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 199:18:3:[177.19,63.5,195.18,196.6,85.16,197.11,124.14,198.13]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 204:21:3:[129.20,64.5,145.24,200.6,91.22,201.11,157.20,202.13,152.24,203.15]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x2),f(suc(suc(suc(x2))))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) ->
% 7.81/2.12 206:13:3:[187.11,65.8,29.9,205.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(x2)))
% 7.81/2.12 209:19:3:[140.17,66.4,160.18,207.10,122.17,208.15]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 210:5:1:[74.2,67.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))
% 7.81/2.12 212:16:3:[187.12,68.4,106.16,211.8]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 7.81/2.12 214:13:3:[104.12,69.3,101.10,213.8]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 217:14:3:[136.14,70.4,214.12,215.8,101.10,216.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12 220:14:3:[104.12,71.3,173.12,218.8,214.14,219.10]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 224:16:3:[180.15,72.4,192.16,221.5,220.14,222.9,173.12,223.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(suc(x2)))))
% 7.81/2.12 227:17:3:[83.14,73.4,212.16,225.9,122.18,226.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(suc(x2)))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 7.81/2.12 229:13:3:[187.12,75.4,101.11,228.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 7.81/2.12
% 7.81/2.12 Most General Atoms: 'E'(f(x1),f(suc(suc(x1)))) 'E'('0',f(x2)) 'E'(f(x1),f(suc(suc(suc(x1))))) iLEQ(suc(x0),suc(x2)) 'E'(f(x2),f(suc(x2))) 'LE'(f(x0),'0') 'LE'(f(x0),s('0'))
% 7.81/2.12
% 7.81/2.12 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: normal ===
% 7.81/2.12
% 7.81/2.12 === Conflict found: 103:21:3:[24.18,20.5,93.18,102.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(suc(suc(x2))))) {x0 -> z, x1 -> z, x2 -> z}
% 7.81/2.12
% 7.81/2.12 SZS status Unsatisfiable
% 7.81/2.12
% 7.81/2.12 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/2.12
% 7.81/2.12 SPASS-SCL-FOL Statistics:
% 7.81/2.12 Number of learned clauses: 0
% 7.81/2.12 Number of propagations: 25
% 7.81/2.12 Number of decisions: 0
% 7.81/2.12 Number of resolutions: 14
% 7.81/2.12 Number of condensations: 0
% 7.81/2.12 Number of sub resolutions: 154
% 7.81/2.12 Number of input literals (deduplicated): 17
% 7.81/2.12 Number of grows: 0
% 7.81/2.12 Number of considered ground atoms: 49
% 7.81/2.12
% 7.81/2.12 Needed: 0:00:01.60
% 7.81/2.12
%------------------------------------------------------------------------------