%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO682-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 : n012.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 46.91s 9.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SYO682-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.06 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.24 % Computer : n012.cluster.edu
% 0.07/0.24 % Model : x86_64 x86_64
% 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.24 % Memory : 8042.1875MB
% 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.24 % CPULimit : 300
% 0.07/0.24 % WCLimit : 300
% 0.07/0.24 % DateTime : Thu May 7 13:56:01 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 SPASS-SCL-FOL version:
% 0.07/0.29 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 46.91/9.71 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.91/9.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.91/9.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.91/9.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.91/9.71 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.91/9.71 Execution lmodel_grow ended with status: unsatisfiable
% 46.91/9.71 Used heuristic: lmodel_grow
% 46.91/9.71
% 46.91/9.71 Input Clauses:
% 46.91/9.71
% 46.91/9.71 Predicates: 'E' iLEQ 'LE'
% 46.91/9.71 Fol Constants: '0' z
% 46.91/9.71 Fol Functions: s suc f
% 46.91/9.71 Problem Properties:
% 46.91/9.71 This is a full first-order problem without equality.
% 46.91/9.71
% 46.91/9.71 After reduction: Problem Properties:
% 46.91/9.71 This is a full first-order problem without equality.
% 46.91/9.71
% 46.91/9.71
% 46.91/9.71 Reduced Input Clauses:
% 46.91/9.71 87:17:4:[25.16,1.9]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x1),f(suc(x1)))
% 46.91/9.71 88:16:4:[33.15,2.9]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x2)))),iLEQ(suc(x3),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 46.91/9.71 89:16:4:[85.13,3.3]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 90:15:4:[80.12,5.4]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 91:15:4:[75.14,6.8]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 92:18:4:[18.17,7.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) ->
% 46.91/9.71 93:4:1:[86.2,8.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 46.91/9.71 94:16:4:[66.14,9.1]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 95:4:1:[46.2,10.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 46.91/9.71 96:16:4:[36.13,12.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 97:15:4:[75.12,14.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 98:16:4:[66.13,15.13]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 99:17:4:[31.16,16.4]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x3),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3)))
% 46.91/9.71 100:17:4:[96.15,17.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x0),f(suc(x0)))
% 46.91/9.71 101:17:4:[96.16,18.8]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x1),f(suc(x1)))
% 46.91/9.71 102:15:4:[73.11,19.12]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 46.91/9.71 104:15:4:[85.14,20.4,90.14,103.11]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 105:16:4:[33.14,21.7]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 107:15:4:[59.14,24.4,90.15,106.12]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 46.91/9.71 108:16:4:[33.13,25.10]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x3)))),iLEQ(suc(x3),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 109:17:4:[37.16,26.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3)))
% 46.91/9.71 110:15:4:[67.12,29.6]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x0)))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 111:16:4:[102.13,30.1]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 46.91/9.71 112:16:4:[59.15,31.10]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 113:17:4:[107.15,32.3]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 46.91/9.71 114:15:4:[67.14,33.10]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 116:16:4:[51.15,34.1,111.15,115.13]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x3),f(suc(x3)))
% 46.91/9.71 117:15:4:[75.11,35.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 118:15:4:[75.13,36.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 120:15:4:[118.15,37.8,91.15,119.9]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 46.91/9.71 121:17:4:[64.15,38.6]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(f(x1),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x2),f(suc(x2)))
% 46.91/9.71 122:17:4:[42.15,39.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x2),f(suc(x2)))
% 46.91/9.71 123:4:1:[52.2,40.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 46.91/9.71 125:16:4:[50.16,41.1,94.16,124.13]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> 'E'(f(x0),f(suc(x0)))
% 46.91/9.71 127:15:4:[117.15,42.8,91.13,126.9]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) ->
% 46.91/9.71 131:16:4:[108.15,45.7,105.15,130.12]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x2),f(suc(x2)))
% 46.91/9.71 132:15:4:[73.12,47.1]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 46.91/9.71 133:2:1:[23.0,48.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 46.91/9.71 135:17:4:[99.17,49.3,113.17,134.14]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x3)),'E'('0',f(suc(x1))) ->
% 46.91/9.71 136:16:4:[66.15,50.11]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 46.91/9.71 137:16:4:[102.14,51.11]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 46.91/9.71 139:16:4:[88.16,54.7,105.16,138.10]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),iLEQ(suc(x3),suc(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3)))
% 46.91/9.71 141:15:4:[117.13,55.7,97.13,140.8]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 142:15:4:[73.13,56.10]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 46.91/9.71 144:15:4:[91.14,57.7,97.15,143.9]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 146:15:4:[63.14,58.6,110.14,145.9]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 147:15:4:[80.14,59.10]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 46.91/9.71 148:16:4:[90.13,61.3]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 149:15:4:[80.11,62.3]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 150:15:4:[67.13,63.8]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 152:15:4:[72.14,64.8,150.13,151.11]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 154:16:4:[104.15,65.3,89.15,153.5]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0)))
% 46.91/9.71 155:15:4:[73.14,66.12]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 157:16:4:[98.16,69.12,136.15,156.15]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> 'E'(f(x1),f(suc(x1)))
% 46.91/9.71 159:17:4:[157.17,71.1,125.17,158.17]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) ->
% 46.91/9.71 160:15:4:[67.11,72.9]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x3)))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 162:15:4:[118.14,74.7,97.14,161.8]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 164:16:4:[98.15,77.1,94.15,163.15]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> 'E'(f(x2),f(suc(x2)))
% 46.91/9.71 166:15:4:[147.13,78.3,149.15,165.12]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 46.91/9.71 167:4:1:[27.2,79.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 46.91/9.71 169:15:4:[142.14,81.1,132.14,168.12]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 46.91/9.71 171:16:4:[112.15,82.3,166.16,170.12]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(x2)))
% 46.91/9.71 173:15:4:[160.13,84.6,110.13,172.11]:TopTopTopTop: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x2)),iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x3)),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x0)))),iLEQ(suc(x3),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x3))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 46.91/9.71 174:15:4:[80.13,85.9]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71
% 46.91/9.71 Most General Atoms: 'E'(s(s(s('0'))),f(x0)) 'E'('0',f(x3)) 'E'(f(x2),f(suc(x2))) 'LE'(f(x0),'0') 'E'(s('0'),f(x3)) 'E'(s(s('0')),f(x0)) 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s('0')) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s(s(s(s('0'))))) iLEQ(suc(x3),suc(x0))
% 46.91/9.71
% 46.91/9.71 === Starting SPASS-SCL-FOL A Little Less Naive, considering 57 atoms initially, heuristics mode: lmodel_grow ===
% 46.91/9.71
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 46.91/9.71 === Backtracking. Learning clause 175:4:1:[129.10,114.13,93.4,133.1,70.2,11.2,60.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 176:3:1:[67.6,86.4]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 66
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 69
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 72
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 76
% 46.91/9.71 === Backtracking. Learning clause 178:3:1:[133.0,177.1,11.1,23.1,93.1]:Top: 'E'(s(s(s('0'))),f(suc(x0))) -> 'LE'(f(x0),s(s(s('0')))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Conflict found: 159:17:4:[157.17,71.1,125.17,158.17]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x2),suc(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(x1)),iLEQ(suc(x1),suc(x2)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x3),f(suc(x3))) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 46.91/9.71 === Backtracking. Learning clause 179:5:1:[159.14,132.13,167.4,68.2,83.2,175.3]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 89
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 108
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z), x3 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 182:2:1:[133.0,180.0,133.0,181.1,129.10,176.3,70.2,23.1,178.3]:Top: -> 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(x0),s(s(s('0'))))
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z), x3 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 183:6:1:[129.7,93.4,176.3,70.2,11.2,23.1,83.1,27.2]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s('0')),f(x0)) -> 'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z), x3 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 184:5:1:[129.10,176.3,93.4,70.2,11.2,83.1,73.2,183.6,23.1]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s('0')),f(x0)) -> 'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 === Backtracking. Learning clause 185:6:1:[70.2,178.1,83.1,27.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Backtracking. Learning clause 186:5:1:[70.2,178.1,83.1,73.2,185.6]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 === Conflict found: 133:2:1:[23.0,48.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 187:5:1:[133.1,184.1,83.1,27.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s('0')),f(x0)) -> 'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Conflict found: 133:2:1:[23.0,48.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 188:4:1:[133.1,184.1,83.1,73.2,187.5]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'E'(s(s('0')),f(x0)) -> 'LE'(f(x0),s(s('0'))),'E'(f(x0),f(suc(x0)))
% 46.91/9.71 === Backtracking. Learning clause 189:3:1:[11.2,129.1,23.1,176.3,178.3,133.1,70.2,83.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 193:5:1:[178.1,190.1,23.0,191.2,23.0,192.3,70.3,179.1,93.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) -> 'LE'(f(x0),s(s('0'))),iLEQ(suc(suc(x0)),suc(suc(x0)))
% 46.91/9.71 === Backtracking. Learning clause 194:7:1:[70.3,179.1,129.1,176.3,193.5]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) -> 'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 195:6:1:[70.3,179.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 196:5:1:[11.2,129.1,23.1,178.3,176.3,179.1,195.5,23.1]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Conflict found: 133:2:1:[23.0,48.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(z))}
% 46.91/9.71 === Backtracking. Learning clause 197:4:1:[133.1,196.1,179.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 198:2:1:[11.1,23.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z), x3 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 199:3:1:[129.10,173.14,133.1,178.3,70.2,198.1,197.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 200:3:1:[70.2,178.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s(s('0')))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 46.91/9.71 === Backtracking. Learning clause 201:2:1:[129.1,198.1,67.12,133.1,200.3,70.2]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s(s('0'))))
% 46.91/9.71 === Backtracking. Learning clause 202:2:1:[70.1,23.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 125
% 46.91/9.71 === Conflict found: 201:2:1:[129.1,198.1,67.12,133.1,200.3,70.2]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc(s('0')))))}
% 46.91/9.71 === Backtracking. Learning clause 203:1:1:[201.1,23.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 46.91/9.71 === Conflict found: 123:4:1:[52.2,40.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 204:9:1:[123.1,28.2,13.2,76.1,95.2,43.2,22.3,52.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'('0',f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))),'E'(s('0'),f(suc(x0))) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Conflict found: 95:4:1:[46.2,10.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 46.91/9.71 === Backtracking. Learning clause 205:9:1:[95.3,43.2,76.2,13.3,22.3,204.5]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'('0',f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Conflict found: 123:4:1:[52.2,40.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 206:8:1:[123.1,28.2,13.2,22.2,76.1,46.2,43.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s('0')) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 46.91/9.71 === Conflict found: 123:4:1:[52.2,40.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 46.91/9.71 === Backtracking. Learning clause 207:8:1:[123.3,22.2,28.2,13.2,206.4]:Top: 'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 208:5:1:[4.1,22.3,95.1,76.2,13.3]:Top: 'E'('0',f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 46.91/9.71 === Backtracking. Learning clause 209:8:1:[13.3,4.1,123.1,95.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),iLEQ(suc(suc(x0)),suc(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Backtracking. Learning clause 210:7:1:[28.2,123.1,76.1,209.4,208.5,43.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s('0')) -> iLEQ(suc(suc(x0)),suc(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 46.91/9.71 === Conflict found: 123:4:1:[52.2,40.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 46.91/9.71 === Backtracking. Learning clause 211:7:1:[123.3,22.2,28.2,210.4]:Top: 'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> iLEQ(suc(suc(x0)),suc(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 212:4:1:[43.2,208.1,28.3]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(x0))))
% 46.91/9.71 === Conflict found: 197:4:1:[133.1,196.1,179.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(z)))}
% 46.91/9.71 === Backtracking. Learning clause 213:8:1:[197.4,209.1,203.1,23.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),iLEQ(suc(suc(x0)),suc(suc(x0))),iLEQ(suc(x0),suc(x0))
% 46.91/9.71 === Backtracking. Learning clause 214:8:1:[13.3,43.1,211.3]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'E'('0',f(x0)),iLEQ(suc(suc(x0)),suc(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 135
% 46.91/9.71 === Conflict found: 129:17:4:[87.17,44.7,121.17,128.16]:TopTopTopTop: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x1))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x1),suc(x2)),'E'(s(s(s('0'))),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(suc(x3)))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x3))) -> {x0 -> s('0'), x1 -> s('0'), x2 -> s('0'), x3 -> s('0')}
% 46.91/9.71 === Backtracking. Learning clause 216:3:1:[93.3,215.1,129.10,110.13]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) ->
% 46.91/9.71 === Backtracking. Learning clause 217:2:0:[43.3,53.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 46.91/9.71 === Conflict found: 107:15:4:[59.14,24.4,90.15,106.12]:TopTopTopTop: 'E'('0',f(x0)),'E'('0',f(x1)),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x2)),'E'('0',f(x3)),'E'('0',f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))) {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 46.91/9.71 === Backtracking. Learning clause 218:3:1:[107.14,135.5,95.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 46.91/9.71 === Conflict found: 199:3:1:[129.10,173.14,133.1,178.3,70.2,198.1,197.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 46.91/9.71 === Backtracking. Learning clause 219:4:0:[199.3,22.1,23.1,4.1,53.1,218.1]:: 'LE'(f(suc(suc(suc(z)))),s(s(s(s('0'))))),'E'('0',f(suc(z))),'E'('0',f(z)) -> 'E'(s('0'),f(suc(suc(z))))
% 46.91/9.71 === Conflict found: 199:3:1:[129.10,173.14,133.1,178.3,70.2,198.1,197.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 46.91/9.71 === Backtracking. Learning clause 220:3:0:[199.3,13.1,23.1,76.1,53.1,219.2,217.2]:: 'LE'(f(suc(suc(suc(z)))),s(s(s(s('0'))))),'LE'(f(z),s('0')) -> 'E'(s('0'),f(suc(suc(z))))
% 46.91/9.71 === Conflict found: 199:3:1:[129.10,173.14,133.1,178.3,70.2,198.1,197.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 46.91/9.71 === Backtracking. Learning clause 221:2:0:[199.3,28.1,23.1,220.2]:: 'LE'(f(suc(suc(suc(z)))),s(s(s(s('0'))))) -> 'E'(s('0'),f(suc(suc(z))))
% 46.91/9.71 === Conflict found: 92:18:4:[18.17,7.7]:TopTopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(x3))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),iLEQ(suc(x3),suc(x1)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x2)),'E'(s('0'),f(suc(suc(x3)))) -> {x0 -> suc(z), x1 -> suc(z), x2 -> suc(z), x3 -> suc(z)}
% 46.91/9.71 === Backtracking. Learning clause 222:3:1:[92.9,162.14,123.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 46.91/9.71 === Conflict found: 197:4:1:[133.1,196.1,179.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(z)))}
% 46.91/9.71 === Backtracking. Learning clause 223:4:1:[197.3,23.1,203.1,13.1,222.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(suc(x0)),s('0'))
% 46.91/9.71 === Backtracking. Learning clause 224:7:1:[28.2,222.1,76.1,95.2,4.2,223.4,208.5]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'E'(s('0'),f(suc(x0))),'E'('0',f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 46.91/9.71 === Conflict found: 222:3:1:[92.9,162.14,123.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> suc('0')}
% 46.91/9.71 === Backtracking. Learning clause 225:6:1:[222.1,28.2,13.2,76.1,218.2,4.2]:Top: 'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'('0',f(x0)),'LE'(f(suc(suc(x0))),s('0')) -> 'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 226:6:1:[22.2,223.2,225.5,43.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 227:6:1:[28.3,226.5]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 228:6:1:[22.2,222.3,226.5,227.5]:Top: 'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0')
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 145
% 46.91/9.71 === Backtracking. Learning clause 229:4:1:[60.3,28.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 46.91/9.71 === Clause set with instances from active satisfied. Growing active. New size: 170
% 46.91/9.71 === Conflict found: 199:3:1:[129.10,173.14,133.1,178.3,70.2,198.1,197.1]:Top: 'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(f('0'))))}
% 46.91/9.71 === Backtracking. Learning clause 230:1:1:[199.1,23.1,23.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 46.91/9.71 === Backtracking. Learning clause 231:3:0:[4.1,22.3,53.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'('0',f(suc(suc(z)))),'E'(s('0'),f(suc(suc(z))))
% 46.91/9.71 === Backtracking. Learning clause 232:3:1:[28.2,222.1,230.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),s('0'))
% 46.91/9.71 === Backtracking. Learning clause 233:2:0:[13.1,230.1,232.1,4.1,53.1,231.3,230.1,218.1]:: 'E'('0',f(suc(z))),'E'('0',f(z)) ->
% 46.91/9.71 === Backtracking. Learning clause 234:3:1:[13.3,76.1,230.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'E'('0',f(suc(x0))),'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 236:3:1:[234.0,235.1,22.1,230.1,222.3,76.1]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'('0',f(suc(x0))),'LE'(f(x0),'0')
% 46.91/9.71 === Backtracking. Learning clause 237:1:0:[28.1,230.1,76.1,236.1,53.1,233.1,217.2]:: 'LE'(f(z),s('0')) ->
% 46.91/9.71 === Backtracking. Learning clause 238:1:0:[28.1,230.1,237.1]:: -> 'E'(s('0'),f(suc(suc(z))))
% 46.91/9.71 === Backtracking. Learning clause 239:3:1:[13.1,230.1,222.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0'))
% 46.91/9.71 === Conflict found: 228:6:1:[22.2,222.3,226.5,227.5]:Top: 'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0') {x0 -> z}
% 46.91/9.71 === Backtracking. Learning clause 240:3:1:[228.1,230.1,23.1,230.1]:Top: 'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),'0')
% 46.91/9.71
% 46.91/9.71 SZS status Unsatisfiable
% 46.91/9.71
% 46.91/9.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 46.91/9.71
% 46.91/9.71 SPASS-SCL-FOL Statistics:
% 46.91/9.71 Number of learned clauses: 58
% 46.91/9.71 Number of propagations: 883
% 46.91/9.71 Number of decisions: 488
% 46.91/9.71 Number of resolutions: 208
% 46.91/9.71 Number of condensations: 1
% 46.91/9.71 Number of sub resolutions: 96
% 46.91/9.71 Number of input literals (deduplicated): 29
% 46.91/9.71 Number of grows: 10
% 46.91/9.71 Number of considered ground atoms: 170
% 46.91/9.71
% 46.91/9.71 Needed: 0:00:09.36
% 46.91/9.71
%------------------------------------------------------------------------------