Drodi-SAT---4.1.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n003.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 03:44:46 PM UTC 2026

% Result   : Unsatisfiable 198.99s 25.82s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35  % Computer : n003.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Mon Sep 21 12:10:31 UTC 2026
% 0.08/0.36  % CPUTime  : 
% 0.41/0.68  % Drodi V4.1.1
% 198.99/25.82  % Refutation found
% 198.99/25.82  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 198.99/25.82  % SZS output start CNFRefutation for theBenchmark
% 198.99/25.82  fof(f22,axiom,(
% 198.99/25.82    (![A_2,B_57,E,B_58]: (( ~ iLEQ(suc(A_2),suc(B_57))| ~ 'E'(s(s(s('0'))),f(B_57))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| ~ iLEQ(suc(B_57),suc(B_58))| ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(B_57)))| ~ 'E'(s(s(s('0'))),f(B_58))| ~ 'E'(s(s(s('0'))),f(suc(B_58)))| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(A_2)))| 'E'(f(B_57),f(suc(B_57)))| 'E'(f(B_58),f(suc(B_58))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f92,axiom,(
% 198.99/25.82    (![LE,A]: ('LE'(f(A),s(s(s(s(s('0')))))) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f125,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(suc(B_94))))| ~ 'E'('0',f(suc(suc(B_95))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'('0',f(suc(suc(A_5))))| ~ 'E'(f(B_95),f(suc(B_95)))| ~ 'E'(f(B_94),f(suc(B_94)))| ~ 'E'(f(A_5),f(suc(A_5)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f129,axiom,(
% 198.99/25.82    (![E,B_75,A_3,B_76]: (( ~ 'E'(s(s('0')),f(suc(B_75)))| ~ 'E'(s(s('0')),f(suc(A_3)))| ~ 'E'(s(s('0')),f(suc(B_76)))| ~ 'E'(s(s('0')),f(B_76))| ~ 'E'(s(s('0')),f(suc(suc(A_3))))| ~ iLEQ(suc(B_75),suc(B_76))| ~ 'E'(f(A_3),f(suc(A_3)))| ~ iLEQ(suc(A_3),suc(B_75))| ~ 'E'(s(s('0')),f(B_75))| ~ 'E'(s(s('0')),f(A_3))| 'E'(f(B_75),f(suc(B_75)))| 'E'(f(B_76),f(suc(B_76))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f135,axiom,(
% 198.99/25.82    (![LE,B_74,E]: (( ~ 'LE'(f(suc(B_74)),s(s(s('0'))))| 'E'(s(s('0')),f(suc(B_74)))| 'LE'(f(B_74),s(s('0'))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f139,axiom,(
% 198.99/25.82    (![LE,B_56,E]: (( ~ 'LE'(f(suc(suc(B_56))),s(s(s(s('0')))))| 'E'(s(s(s('0'))),f(suc(suc(B_56))))| 'LE'(f(B_56),s(s(s('0')))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f145,axiom,(
% 198.99/25.82    (![E,B_32,B_33,A_1]: (( ~ 'E'(f(B_32),f(suc(B_32)))| ~ iLEQ(suc(B_32),suc(B_33))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| ~ 'E'(s(s(s(s('0')))),f(B_33))| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_32))))| ~ iLEQ(suc(A_1),suc(B_32))| ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(B_32))| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_33),f(suc(B_33))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f148,axiom,(
% 198.99/25.82    (![E,A_2]: (( ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| 'E'(f(A_2),f(suc(A_2)))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f153,axiom,(
% 198.99/25.82    (![LE,B_86,E]: (( ~ 'LE'(f(B_86),s(s('0')))| 'E'(s('0'),f(B_86))| 'LE'(f(B_86),s('0')) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f169,axiom,(
% 198.99/25.82    (![LE,B_56,E]: (( ~ 'LE'(f(suc(B_56)),s(s(s(s('0')))))| 'E'(s(s(s('0'))),f(suc(B_56)))| 'LE'(f(B_56),s(s(s('0')))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f190,axiom,(
% 198.99/25.82    (![E,A_2]: (( ~ 'E'(s(s(s('0'))),f(suc(suc(A_2))))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| ~ 'E'(f(A_2),f(suc(A_2)))| ~ 'E'(s(s(s('0'))),f(A_2))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f208,axiom,(
% 198.99/25.82    (![E,B_58,A_2,B_57]: (( ~ 'E'(s(s(s('0'))),f(suc(suc(B_58))))| ~ iLEQ(suc(A_2),suc(B_57))| ~ 'E'(s(s(s('0'))),f(B_57))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| ~ iLEQ(suc(B_57),suc(B_58))| ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(B_57)))| ~ 'E'(f(B_58),f(suc(B_58)))| ~ 'E'(s(s(s('0'))),f(B_58))| ~ 'E'(s(s(s('0'))),f(suc(B_58)))| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(A_2)))| 'E'(f(B_57),f(suc(B_57))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f213,axiom,(
% 198.99/25.82    (![E,B_33,B_32,A_1]: (( ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_33))))| ~ iLEQ(suc(B_32),suc(B_33))| ~ 'E'(f(B_33),f(suc(B_33)))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| ~ 'E'(s(s(s(s('0')))),f(B_33))| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))| ~ iLEQ(suc(A_1),suc(B_32))| ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(B_32))| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_32),f(suc(B_32))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f226,axiom,(
% 198.99/25.82    (![LE,B_93,E]: (( ~ 'LE'(f(B_93),s('0'))| 'E'('0',f(B_93))| 'LE'(f(B_93),'0') ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f279,axiom,(
% 198.99/25.82    (![E,A_3]: (( ~ 'E'(s(s('0')),f(suc(suc(A_3))))| ~ 'E'(s(s('0')),f(suc(A_3)))| ~ 'E'(f(A_3),f(suc(A_3)))| ~ 'E'(s(s('0')),f(A_3))| iLEQ(suc(A_3),suc(A_3)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f308,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(suc(B_95))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'('0',f(suc(suc(A_5))))| ~ 'E'(f(B_95),f(suc(B_95)))| ~ 'E'(f(A_5),f(suc(A_5)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(B_94),f(suc(B_94))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f335,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(suc(B_95))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'(f(B_95),f(suc(B_95)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(A_5),f(suc(A_5)))| 'E'(f(B_94),f(suc(B_94))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f360,axiom,(
% 198.99/25.82    (![E,A_4]: (( ~ 'E'(s('0'),f(suc(suc(A_4))))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(f(A_4),f(suc(A_4)))| ~ 'E'(s('0'),f(A_4))| iLEQ(suc(A_4),suc(A_4)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f366,axiom,(
% 198.99/25.82    (![LE]: (~ 'LE'(f(z),'0') ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f384,axiom,(
% 198.99/25.82    (![E,B_88,A_4,B_87]: (( ~ 'E'(s('0'),f(B_88))| ~ 'E'(f(A_4),f(suc(A_4)))| ~ 'E'(s('0'),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(suc(A_4))))| ~ 'E'(s('0'),f(suc(suc(B_87))))| ~ 'E'(f(B_87),f(suc(B_87)))| ~ 'E'(f(B_88),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(B_87)))| ~ 'E'(s('0'),f(B_87))| ~ iLEQ(suc(B_87),suc(B_88))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(s('0'),f(suc(suc(B_88))))| ~ 'E'(s('0'),f(A_4))| ~ iLEQ(suc(A_4),suc(B_87)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f402,axiom,(
% 198.99/25.82    (![E,B_33,A_1,B_32]: (( ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_33))))| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1))))| ~ 'E'(f(B_32),f(suc(B_32)))| ~ iLEQ(suc(B_32),suc(B_33))| ~ 'E'(f(B_33),f(suc(B_33)))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| ~ 'E'(s(s(s(s('0')))),f(B_33))| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_32))))| ~ iLEQ(suc(A_1),suc(B_32))| ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(B_32))| ~ 'E'(s(s(s(s('0')))),f(suc(B_33))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f470,axiom,(
% 198.99/25.82    (![E,A_1]: (( ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1))))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s(s(s(s('0')))),f(A_1))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f471,axiom,(
% 198.99/25.82    (![E,B_88,B_87,A_4]: (( ~ 'E'(s('0'),f(B_88))| ~ 'E'(s('0'),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(suc(B_87))))| ~ 'E'(f(B_87),f(suc(B_87)))| ~ 'E'(s('0'),f(suc(B_87)))| ~ 'E'(s('0'),f(B_87))| ~ iLEQ(suc(B_87),suc(B_88))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(s('0'),f(A_4))| ~ iLEQ(suc(A_4),suc(B_87))| 'E'(f(A_4),f(suc(A_4)))| 'E'(f(B_88),f(suc(B_88))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f502,axiom,(
% 198.99/25.82    (![LE,B_74,E]: (( ~ 'LE'(f(B_74),s(s(s('0'))))| 'E'(s(s('0')),f(B_74))| 'LE'(f(B_74),s(s('0'))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f535,axiom,(
% 198.99/25.82    (![LE,B_86,E]: (( ~ 'LE'(f(suc(suc(B_86))),s(s('0')))| 'E'(s('0'),f(suc(suc(B_86))))| 'LE'(f(B_86),s('0')) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f580,axiom,(
% 198.99/25.82    (![LE,B_31,E]: (( ~ 'LE'(f(suc(suc(B_31))),s(s(s(s(s('0'))))))| 'E'(s(s(s(s('0')))),f(suc(suc(B_31))))| 'LE'(f(B_31),s(s(s(s('0'))))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f581,axiom,(
% 198.99/25.82    (![E,A_5]: (( ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(A_5)))| 'E'(f(A_5),f(suc(A_5)))| iLEQ(suc(A_5),suc(A_5)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f587,axiom,(
% 198.99/25.82    (![E,B_75,A_3,B_76]: (( ~ 'E'(s(s('0')),f(suc(B_75)))| ~ 'E'(s(s('0')),f(suc(A_3)))| ~ 'E'(s(s('0')),f(suc(B_76)))| ~ 'E'(s(s('0')),f(B_76))| ~ iLEQ(suc(B_75),suc(B_76))| ~ iLEQ(suc(A_3),suc(B_75))| ~ 'E'(s(s('0')),f(B_75))| ~ 'E'(s(s('0')),f(A_3))| 'E'(f(A_3),f(suc(A_3)))| 'E'(f(B_75),f(suc(B_75)))| 'E'(f(B_76),f(suc(B_76))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f590,axiom,(
% 198.99/25.82    (![E,B_75,A_3,B_76]: (( ~ 'E'(s(s('0')),f(suc(B_75)))| ~ 'E'(s(s('0')),f(suc(A_3)))| ~ 'E'(s(s('0')),f(suc(B_76)))| ~ 'E'(s(s('0')),f(B_76))| ~ 'E'(s(s('0')),f(suc(suc(A_3))))| ~ iLEQ(suc(B_75),suc(B_76))| ~ 'E'(f(A_3),f(suc(A_3)))| ~ 'E'(s(s('0')),f(suc(suc(B_75))))| ~ iLEQ(suc(A_3),suc(B_75))| ~ 'E'(s(s('0')),f(B_75))| ~ 'E'(f(B_75),f(suc(B_75)))| ~ 'E'(s(s('0')),f(A_3))| 'E'(f(B_76),f(suc(B_76))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f660,axiom,(
% 198.99/25.82    (![LE,B_93,E]: (( ~ 'LE'(f(suc(suc(B_93))),s('0'))| 'E'('0',f(suc(suc(B_93))))| 'LE'(f(B_93),'0') ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f692,axiom,(
% 198.99/25.82    (![LE,B_86,E]: (( ~ 'LE'(f(suc(B_86)),s(s('0')))| 'E'(s('0'),f(suc(B_86)))| 'LE'(f(B_86),s('0')) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f708,axiom,(
% 198.99/25.82    (![E,B_88,A_4,B_87]: (( ~ 'E'(s('0'),f(B_88))| ~ 'E'(f(A_4),f(suc(A_4)))| ~ 'E'(s('0'),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(suc(A_4))))| ~ 'E'(s('0'),f(suc(suc(B_87))))| ~ 'E'(f(B_87),f(suc(B_87)))| ~ 'E'(s('0'),f(suc(B_87)))| ~ 'E'(s('0'),f(B_87))| ~ iLEQ(suc(B_87),suc(B_88))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(s('0'),f(A_4))| ~ iLEQ(suc(A_4),suc(B_87))| 'E'(f(B_88),f(suc(B_88))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f720,axiom,(
% 198.99/25.82    (![E,A_5]: (( ~ 'E'('0',f(suc(suc(A_5))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'(f(A_5),f(suc(A_5)))| ~ 'E'('0',f(A_5))| iLEQ(suc(A_5),suc(A_5)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f756,axiom,(
% 198.99/25.82    (![E,B_88,B_87,A_4]: (( ~ 'E'(s('0'),f(B_88))| ~ 'E'(s('0'),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(B_87)))| ~ 'E'(s('0'),f(B_87))| ~ iLEQ(suc(B_87),suc(B_88))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(s('0'),f(A_4))| ~ iLEQ(suc(A_4),suc(B_87))| 'E'(f(A_4),f(suc(A_4)))| 'E'(f(B_87),f(suc(B_87)))| 'E'(f(B_88),f(suc(B_88))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f809,axiom,(
% 198.99/25.82    (![B_32,B_33,E,A_1]: (( ~ iLEQ(suc(B_32),suc(B_33))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| ~ 'E'(s(s(s(s('0')))),f(B_33))| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))| ~ iLEQ(suc(A_1),suc(B_32))| ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(B_32))| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_32),f(suc(B_32)))| 'E'(f(B_33),f(suc(B_33))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f852,axiom,(
% 198.99/25.82    (![E,A_4]: (( ~ 'E'(s('0'),f(A_4))| ~ 'E'(s('0'),f(suc(A_4)))| 'E'(f(A_4),f(suc(A_4)))| iLEQ(suc(A_4),suc(A_4)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f859,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'('0',f(suc(suc(A_5))))| ~ 'E'(f(A_5),f(suc(A_5)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(B_94),f(suc(B_94)))| 'E'(f(B_95),f(suc(B_95))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f894,axiom,(
% 198.99/25.82    (![LE,B_31,E]: (( ~ 'LE'(f(B_31),s(s(s(s(s('0'))))))| 'E'(s(s(s(s('0')))),f(B_31))| 'LE'(f(B_31),s(s(s(s('0'))))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f903,axiom,(
% 198.99/25.82    (![E,B_88,B_87,A_4]: (( ~ 'E'(s('0'),f(B_88))| ~ 'E'(s('0'),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(suc(B_87))))| ~ 'E'(f(B_87),f(suc(B_87)))| ~ 'E'(f(B_88),f(suc(B_88)))| ~ 'E'(s('0'),f(suc(B_87)))| ~ 'E'(s('0'),f(B_87))| ~ iLEQ(suc(B_87),suc(B_88))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(s('0'),f(suc(suc(B_88))))| ~ 'E'(s('0'),f(A_4))| ~ iLEQ(suc(A_4),suc(B_87))| 'E'(f(A_4),f(suc(A_4))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f914,axiom,(
% 198.99/25.82    (![LE,B_74,E]: (( ~ 'LE'(f(suc(suc(B_74))),s(s(s('0'))))| 'E'(s(s('0')),f(suc(suc(B_74))))| 'LE'(f(B_74),s(s('0'))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f932,axiom,(
% 198.99/25.82    (![E,B_58,A_2,B_57]: (( ~ 'E'(s(s(s('0'))),f(suc(suc(B_58))))| ~ iLEQ(suc(A_2),suc(B_57))| ~ 'E'(s(s(s('0'))),f(B_57))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| ~ iLEQ(suc(B_57),suc(B_58))| ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(B_57)))| ~ 'E'(f(B_58),f(suc(B_58)))| ~ 'E'(f(B_57),f(suc(B_57)))| ~ 'E'(s(s(s('0'))),f(B_58))| ~ 'E'(s(s(s('0'))),f(suc(B_58)))| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(A_2)))| ~ 'E'(s(s(s('0'))),f(suc(suc(B_57)))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f943,axiom,(
% 198.99/25.82    (![E,A_3]: (( ~ 'E'(s(s('0')),f(A_3))| ~ 'E'(s(s('0')),f(suc(A_3)))| 'E'(f(A_3),f(suc(A_3)))| iLEQ(suc(A_3),suc(A_3)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f976,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(suc(B_94))))| ~ 'E'('0',f(suc(suc(B_95))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'(f(B_95),f(suc(B_95)))| ~ 'E'(f(B_94),f(suc(B_94)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(A_5),f(suc(A_5))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f982,axiom,(
% 198.99/25.82    (![E,B_75,A_3,B_76]: (( ~ 'E'(s(s('0')),f(suc(B_75)))| ~ 'E'(s(s('0')),f(suc(A_3)))| ~ 'E'(s(s('0')),f(suc(B_76)))| ~ 'E'(f(B_76),f(suc(B_76)))| ~ 'E'(s(s('0')),f(B_76))| ~ 'E'(s(s('0')),f(suc(suc(A_3))))| ~ iLEQ(suc(B_75),suc(B_76))| ~ 'E'(s(s('0')),f(suc(suc(B_76))))| ~ 'E'(f(A_3),f(suc(A_3)))| ~ 'E'(s(s('0')),f(suc(suc(B_75))))| ~ iLEQ(suc(A_3),suc(B_75))| ~ 'E'(s(s('0')),f(B_75))| ~ 'E'(f(B_75),f(suc(B_75)))| ~ 'E'(s(s('0')),f(A_3)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1030,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(A_5)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(A_5),f(suc(A_5)))| 'E'(f(B_94),f(suc(B_94)))| 'E'(f(B_95),f(suc(B_95))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1031,axiom,(
% 198.99/25.82    (![LE,B_56,E]: (( ~ 'LE'(f(B_56),s(s(s(s('0')))))| 'E'(s(s(s('0'))),f(B_56))| 'LE'(f(B_56),s(s(s('0')))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1072,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(suc(B_94))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'(f(B_94),f(suc(B_94)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(A_5),f(suc(A_5)))| 'E'(f(B_95),f(suc(B_95))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1075,axiom,(
% 198.99/25.82    (![LE,B_93,E]: (( ~ 'LE'(f(suc(B_93)),s('0'))| 'E'('0',f(suc(B_93)))| 'LE'(f(B_93),'0') ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1085,axiom,(
% 198.99/25.82    (![E,A_1]: (( ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| 'E'(f(A_1),f(suc(A_1)))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1109,axiom,(
% 198.99/25.82    (![A_5,B_94,E,B_95]: (( ~ iLEQ(suc(A_5),suc(B_94))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(B_94)))| ~ 'E'('0',f(suc(suc(B_94))))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'('0',f(suc(suc(A_5))))| ~ 'E'(f(B_94),f(suc(B_94)))| ~ 'E'(f(A_5),f(suc(A_5)))| ~ iLEQ(suc(B_94),suc(B_95))| ~ 'E'('0',f(B_94))| ~ 'E'('0',f(suc(B_95)))| ~ 'E'('0',f(B_95))| 'E'(f(B_95),f(suc(B_95))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1151,axiom,(
% 198.99/25.82    (![LE,B_31,E]: (( ~ 'LE'(f(suc(B_31)),s(s(s(s(s('0'))))))| 'E'(s(s(s(s('0')))),f(suc(B_31)))| 'LE'(f(B_31),s(s(s(s('0'))))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1160,axiom,(
% 198.99/25.82    (![A_2,B_57,E,B_58]: (( ~ iLEQ(suc(A_2),suc(B_57))| ~ 'E'(s(s(s('0'))),f(B_57))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| ~ iLEQ(suc(B_57),suc(B_58))| ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(B_57)))| ~ 'E'(s(s(s('0'))),f(B_58))| ~ 'E'(s(s(s('0'))),f(suc(B_58)))| 'E'(f(A_2),f(suc(A_2)))| 'E'(f(B_57),f(suc(B_57)))| 'E'(f(B_58),f(suc(B_58))) ) ))),
% 198.99/25.82    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 198.99/25.82  fof(f1210,plain,(
% 198.99/25.82    ![B_58]: ((![B_57]: ((![A_2]: (((((((((~iLEQ(suc(A_2),suc(B_57))|~'E'(s(s(s('0'))),f(B_57)))|~'E'(s(s(s('0'))),f(suc(A_2))))|~iLEQ(suc(B_57),suc(B_58)))|~'E'(s(s(s('0'))),f(A_2)))|~'E'(s(s(s('0'))),f(suc(B_57))))|~'E'(s(s(s('0'))),f(B_58)))|~'E'(s(s(s('0'))),f(suc(B_58))))|~'E'(s(s(s('0'))),f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(A_2)))))|'E'(f(B_57),f(suc(B_57)))))|'E'(f(B_58),f(suc(B_58))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f22])).
% 198.99/25.82  fof(f1211,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1210])).
% 198.99/25.82  fof(f1350,plain,(
% 198.99/25.82    ![A]: 'LE'(f(A),s(s(s(s(s('0'))))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f92])).
% 198.99/25.82  fof(f1351,plain,(
% 198.99/25.82    ![LE,X0]: ('LE'(f(X0),s(s(s(s(s('0')))))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1350])).
% 198.99/25.82  fof(f1416,plain,(
% 198.99/25.82    ![B_95]: (((![B_94]: (((![A_5]: (((((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(suc(B_94)))))|~'E'('0',f(suc(suc(B_95)))))|~'E'('0',f(suc(A_5))))|~'E'('0',f(suc(suc(A_5)))))|~'E'(f(B_95),f(suc(B_95))))|~'E'(f(B_94),f(suc(B_94))))|~'E'(f(A_5),f(suc(A_5)))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94))))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f125])).
% 198.99/25.82  fof(f1417,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1416])).
% 198.99/25.82  fof(f1424,plain,(
% 198.99/25.82    ![B_76]: ((![B_75]: ((![A_3]: (((((((((~'E'(s(s('0')),f(suc(B_75)))|~'E'(s(s('0')),f(suc(A_3))))|~'E'(s(s('0')),f(suc(B_76))))|~'E'(s(s('0')),f(B_76)))|~'E'(s(s('0')),f(suc(suc(A_3)))))|~iLEQ(suc(B_75),suc(B_76)))|~'E'(f(A_3),f(suc(A_3))))|~iLEQ(suc(A_3),suc(B_75)))|~'E'(s(s('0')),f(B_75)))|~'E'(s(s('0')),f(A_3))))|'E'(f(B_75),f(suc(B_75)))))|'E'(f(B_76),f(suc(B_76))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f129])).
% 198.99/25.82  fof(f1425,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1424])).
% 198.99/25.82  fof(f1436,plain,(
% 198.99/25.82    ![B_74]: ((~'LE'(f(suc(B_74)),s(s(s('0'))))|'E'(s(s('0')),f(suc(B_74))))|'LE'(f(B_74),s(s('0'))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f135])).
% 198.99/25.82  fof(f1437,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s(s('0'))))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1436])).
% 198.99/25.82  fof(f1444,plain,(
% 198.99/25.82    ![B_56]: ((~'LE'(f(suc(suc(B_56))),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(suc(B_56)))))|'LE'(f(B_56),s(s(s('0')))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f139])).
% 198.99/25.82  fof(f1445,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(suc(X0))))|'LE'(f(X0),s(s(s('0')))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1444])).
% 198.99/25.82  fof(f1456,plain,(
% 198.99/25.82    ![B_33]: ((![A_1]: (((![B_32]: ((((((((~'E'(f(B_32),f(suc(B_32)))|~iLEQ(suc(B_32),suc(B_33)))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|~'E'(s(s(s(s('0')))),f(B_33)))|~'E'(s(s(s(s('0')))),f(suc(B_32))))|~'E'(s(s(s(s('0')))),f(suc(suc(B_32)))))|~iLEQ(suc(A_1),suc(B_32)))|~'E'(s(s(s(s('0')))),f(A_1)))|~'E'(s(s(s(s('0')))),f(B_32))))|~'E'(s(s(s(s('0')))),f(suc(B_33))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_33),f(suc(B_33))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f145])).
% 198.99/25.82  fof(f1457,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1456])).
% 198.99/25.82  fof(f1462,plain,(
% 198.99/25.82    ![A_2]: (((~'E'(s(s(s('0'))),f(A_2))|~'E'(s(s(s('0'))),f(suc(A_2))))|'E'(f(A_2),f(suc(A_2))))|iLEQ(suc(A_2),suc(A_2)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f148])).
% 198.99/25.82  fof(f1463,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1462])).
% 198.99/25.82  fof(f1472,plain,(
% 198.99/25.82    ![B_86]: ((~'LE'(f(B_86),s(s('0')))|'E'(s('0'),f(B_86)))|'LE'(f(B_86),s('0')))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f153])).
% 198.99/25.82  fof(f1473,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(X0),s(s('0')))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1472])).
% 198.99/25.82  fof(f1504,plain,(
% 198.99/25.82    ![B_56]: ((~'LE'(f(suc(B_56)),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(B_56))))|'LE'(f(B_56),s(s(s('0')))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f169])).
% 198.99/25.82  fof(f1505,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1504])).
% 198.99/25.82  fof(f1546,plain,(
% 198.99/25.82    ![A_2]: ((((~'E'(s(s(s('0'))),f(suc(suc(A_2))))|~'E'(s(s(s('0'))),f(suc(A_2))))|~'E'(f(A_2),f(suc(A_2))))|~'E'(s(s(s('0'))),f(A_2)))|iLEQ(suc(A_2),suc(A_2)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f190])).
% 198.99/25.82  fof(f1547,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1546])).
% 198.99/25.82  fof(f1582,plain,(
% 198.99/25.82    ![B_57]: ((![A_2]: (((![B_58]: (((((((((~'E'(s(s(s('0'))),f(suc(suc(B_58))))|~iLEQ(suc(A_2),suc(B_57)))|~'E'(s(s(s('0'))),f(B_57)))|~'E'(s(s(s('0'))),f(suc(A_2))))|~iLEQ(suc(B_57),suc(B_58)))|~'E'(s(s(s('0'))),f(A_2)))|~'E'(s(s(s('0'))),f(suc(B_57))))|~'E'(f(B_58),f(suc(B_58))))|~'E'(s(s(s('0'))),f(B_58)))|~'E'(s(s(s('0'))),f(suc(B_58)))))|~'E'(s(s(s('0'))),f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(A_2)))))|'E'(f(B_57),f(suc(B_57))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f208])).
% 198.99/25.82  fof(f1583,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1582])).
% 198.99/25.82  fof(f1592,plain,(
% 198.99/25.82    ![B_32]: ((![A_1]: ((![B_33]: (((((((((~'E'(s(s(s(s('0')))),f(suc(suc(B_33))))|~iLEQ(suc(B_32),suc(B_33)))|~'E'(f(B_33),f(suc(B_33))))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|~'E'(s(s(s(s('0')))),f(B_33)))|~'E'(s(s(s(s('0')))),f(suc(B_32))))|~iLEQ(suc(A_1),suc(B_32)))|~'E'(s(s(s(s('0')))),f(A_1)))|~'E'(s(s(s(s('0')))),f(B_32)))|~'E'(s(s(s(s('0')))),f(suc(B_33)))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_32),f(suc(B_32))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f213])).
% 198.99/25.82  fof(f1593,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|~iLEQ(suc(X2),suc(X1))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1592])).
% 198.99/25.82  fof(f1618,plain,(
% 198.99/25.82    ![B_93]: ((~'LE'(f(B_93),s('0'))|'E'('0',f(B_93)))|'LE'(f(B_93),'0'))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f226])).
% 198.99/25.82  fof(f1619,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(X0),s('0'))|'E'('0',f(X0))|'LE'(f(X0),'0'))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1618])).
% 198.99/25.82  fof(f1724,plain,(
% 198.99/25.82    ![A_3]: ((((~'E'(s(s('0')),f(suc(suc(A_3))))|~'E'(s(s('0')),f(suc(A_3))))|~'E'(f(A_3),f(suc(A_3))))|~'E'(s(s('0')),f(A_3)))|iLEQ(suc(A_3),suc(A_3)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f279])).
% 198.99/25.82  fof(f1725,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s('0')),f(suc(suc(X0))))|~'E'(s(s('0')),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1724])).
% 198.99/25.82  fof(f1782,plain,(
% 198.99/25.82    ![B_94]: ((![B_95]: (((((![A_5]: (((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(suc(B_95)))))|~'E'('0',f(suc(A_5))))|~'E'('0',f(suc(suc(A_5)))))|~'E'(f(B_95),f(suc(B_95))))|~'E'(f(A_5),f(suc(A_5)))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94)))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95))))|'E'(f(B_94),f(suc(B_94))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f308])).
% 198.99/25.82  fof(f1783,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X1),f(suc(X1))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1782])).
% 198.99/25.82  fof(f1836,plain,(
% 198.99/25.82    ![B_94]: ((![A_5]: ((![B_95]: (((((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(suc(B_95)))))|~'E'('0',f(suc(A_5))))|~'E'(f(B_95),f(suc(B_95))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94)))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95))))|'E'(f(A_5),f(suc(A_5)))))|'E'(f(B_94),f(suc(B_94))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f335])).
% 198.99/25.82  fof(f1837,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1836])).
% 198.99/25.82  fof(f1886,plain,(
% 198.99/25.82    ![A_4]: ((((~'E'(s('0'),f(suc(suc(A_4))))|~'E'(s('0'),f(suc(A_4))))|~'E'(f(A_4),f(suc(A_4))))|~'E'(s('0'),f(A_4)))|iLEQ(suc(A_4),suc(A_4)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f360])).
% 198.99/25.82  fof(f1887,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1886])).
% 198.99/25.82  fof(f1898,plain,(
% 198.99/25.82    ![LE]: (~'LE'(f(z),'0'))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f366])).
% 198.99/25.82  fof(f1933,plain,(
% 198.99/25.82    ![A_4,B_87]: (((![B_88]: (((((((((((~'E'(s('0'),f(B_88))|~'E'(f(A_4),f(suc(A_4))))|~'E'(s('0'),f(suc(B_88))))|~'E'(s('0'),f(suc(suc(A_4)))))|~'E'(s('0'),f(suc(suc(B_87)))))|~'E'(f(B_87),f(suc(B_87))))|~'E'(f(B_88),f(suc(B_88))))|~'E'(s('0'),f(suc(B_87))))|~'E'(s('0'),f(B_87)))|~iLEQ(suc(B_87),suc(B_88)))|~'E'(s('0'),f(suc(A_4))))|~'E'(s('0'),f(suc(suc(B_88))))))|~'E'(s('0'),f(A_4)))|~iLEQ(suc(A_4),suc(B_87)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f384])).
% 198.99/25.82  fof(f1934,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(f(X1),f(suc(X1)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X2)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1933])).
% 198.99/25.82  fof(f1969,plain,(
% 198.99/25.82    ![B_33]: ((![B_32]: ((![A_1]: (((((((((((~'E'(s(s(s(s('0')))),f(suc(suc(B_33))))|~'E'(s(s(s(s('0')))),f(suc(suc(A_1)))))|~'E'(f(B_32),f(suc(B_32))))|~iLEQ(suc(B_32),suc(B_33)))|~'E'(f(B_33),f(suc(B_33))))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|~'E'(s(s(s(s('0')))),f(B_33)))|~'E'(s(s(s(s('0')))),f(suc(B_32))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s(s(s(s('0')))),f(suc(suc(B_32)))))|~iLEQ(suc(A_1),suc(B_32)))|~'E'(s(s(s(s('0')))),f(A_1))))|~'E'(s(s(s(s('0')))),f(B_32))))|~'E'(s(s(s(s('0')))),f(suc(B_33))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f402])).
% 198.99/25.82  fof(f1970,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(s(s(s(s('0')))),f(suc(suc(X1))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X2),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(suc(X2))))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(suc(X0))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f1969])).
% 198.99/25.82  fof(f2105,plain,(
% 198.99/25.82    ![A_1]: ((((~'E'(s(s(s(s('0')))),f(suc(suc(A_1))))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s(s(s(s('0')))),f(A_1)))|iLEQ(suc(A_1),suc(A_1)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f470])).
% 198.99/25.82  fof(f2106,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2105])).
% 198.99/25.82  fof(f2107,plain,(
% 198.99/25.82    ![B_88]: ((![A_4]: ((![B_87]: (((((((((~'E'(s('0'),f(B_88))|~'E'(s('0'),f(suc(B_88))))|~'E'(s('0'),f(suc(suc(B_87)))))|~'E'(f(B_87),f(suc(B_87))))|~'E'(s('0'),f(suc(B_87))))|~'E'(s('0'),f(B_87)))|~iLEQ(suc(B_87),suc(B_88)))|~'E'(s('0'),f(suc(A_4))))|~'E'(s('0'),f(A_4)))|~iLEQ(suc(A_4),suc(B_87))))|'E'(f(A_4),f(suc(A_4)))))|'E'(f(B_88),f(suc(B_88))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f471])).
% 198.99/25.82  fof(f2108,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X1))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2107])).
% 198.99/25.82  fof(f2169,plain,(
% 198.99/25.82    ![B_74]: ((~'LE'(f(B_74),s(s(s('0'))))|'E'(s(s('0')),f(B_74)))|'LE'(f(B_74),s(s('0'))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f502])).
% 198.99/25.82  fof(f2170,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(X0),s(s(s('0'))))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2169])).
% 198.99/25.82  fof(f2235,plain,(
% 198.99/25.82    ![B_86]: ((~'LE'(f(suc(suc(B_86))),s(s('0')))|'E'(s('0'),f(suc(suc(B_86)))))|'LE'(f(B_86),s('0')))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f535])).
% 198.99/25.82  fof(f2236,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s(s('0')))|'E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2235])).
% 198.99/25.82  fof(f2325,plain,(
% 198.99/25.82    ![B_31]: ((~'LE'(f(suc(suc(B_31))),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(suc(suc(B_31)))))|'LE'(f(B_31),s(s(s(s('0'))))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f580])).
% 198.99/25.82  fof(f2326,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(suc(suc(X0))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2325])).
% 198.99/25.82  fof(f2327,plain,(
% 198.99/25.82    ![A_5]: (((~'E'('0',f(A_5))|~'E'('0',f(suc(A_5))))|'E'(f(A_5),f(suc(A_5))))|iLEQ(suc(A_5),suc(A_5)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f581])).
% 198.99/25.82  fof(f2328,plain,(
% 198.99/25.82    ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2327])).
% 198.99/25.82  fof(f2339,plain,(
% 198.99/25.82    ![B_76]: ((![B_75]: ((![A_3]: ((((((((~'E'(s(s('0')),f(suc(B_75)))|~'E'(s(s('0')),f(suc(A_3))))|~'E'(s(s('0')),f(suc(B_76))))|~'E'(s(s('0')),f(B_76)))|~iLEQ(suc(B_75),suc(B_76)))|~iLEQ(suc(A_3),suc(B_75)))|~'E'(s(s('0')),f(B_75)))|~'E'(s(s('0')),f(A_3)))|'E'(f(A_3),f(suc(A_3)))))|'E'(f(B_75),f(suc(B_75)))))|'E'(f(B_76),f(suc(B_76))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f587])).
% 198.99/25.82  fof(f2340,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~iLEQ(suc(X0),suc(X2))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2339])).
% 198.99/25.82  fof(f2345,plain,(
% 198.99/25.82    ![B_76]: ((![A_3]: ((![B_75]: ((((((((((~'E'(s(s('0')),f(suc(B_75)))|~'E'(s(s('0')),f(suc(A_3))))|~'E'(s(s('0')),f(suc(B_76))))|~'E'(s(s('0')),f(B_76)))|~'E'(s(s('0')),f(suc(suc(A_3)))))|~iLEQ(suc(B_75),suc(B_76)))|~'E'(f(A_3),f(suc(A_3))))|~'E'(s(s('0')),f(suc(suc(B_75)))))|~iLEQ(suc(A_3),suc(B_75)))|~'E'(s(s('0')),f(B_75)))|~'E'(f(B_75),f(suc(B_75)))))|~'E'(s(s('0')),f(A_3))))|'E'(f(B_76),f(suc(B_76))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f590])).
% 198.99/25.82  fof(f2346,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2345])).
% 198.99/25.82  fof(f2485,plain,(
% 198.99/25.82    ![B_93]: ((~'LE'(f(suc(suc(B_93))),s('0'))|'E'('0',f(suc(suc(B_93)))))|'LE'(f(B_93),'0'))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f660])).
% 198.99/25.82  fof(f2486,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s('0'))|'E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2485])).
% 198.99/25.82  fof(f2549,plain,(
% 198.99/25.82    ![B_86]: ((~'LE'(f(suc(B_86)),s(s('0')))|'E'(s('0'),f(suc(B_86))))|'LE'(f(B_86),s('0')))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f692])).
% 198.99/25.82  fof(f2550,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s('0')))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2549])).
% 198.99/25.82  fof(f2581,plain,(
% 198.99/25.82    ![B_88]: ((![A_4,B_87]: (((((((((((~'E'(s('0'),f(B_88))|~'E'(f(A_4),f(suc(A_4))))|~'E'(s('0'),f(suc(B_88))))|~'E'(s('0'),f(suc(suc(A_4)))))|~'E'(s('0'),f(suc(suc(B_87)))))|~'E'(f(B_87),f(suc(B_87))))|~'E'(s('0'),f(suc(B_87))))|~'E'(s('0'),f(B_87)))|~iLEQ(suc(B_87),suc(B_88)))|~'E'(s('0'),f(suc(A_4))))|~'E'(s('0'),f(A_4)))|~iLEQ(suc(A_4),suc(B_87))))|'E'(f(B_88),f(suc(B_88))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f708])).
% 198.99/25.82  fof(f2582,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(f(X1),f(suc(X1)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X2))|'E'(f(X0),f(suc(X0))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2581])).
% 198.99/25.82  fof(f2605,plain,(
% 198.99/25.82    ![A_5]: ((((~'E'('0',f(suc(suc(A_5))))|~'E'('0',f(suc(A_5))))|~'E'(f(A_5),f(suc(A_5))))|~'E'('0',f(A_5)))|iLEQ(suc(A_5),suc(A_5)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f720])).
% 198.99/25.82  fof(f2606,plain,(
% 198.99/25.82    ![E,X0]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2605])).
% 198.99/25.82  fof(f2677,plain,(
% 198.99/25.82    ![B_88]: ((![B_87]: ((![A_4]: ((((((((~'E'(s('0'),f(B_88))|~'E'(s('0'),f(suc(B_88))))|~'E'(s('0'),f(suc(B_87))))|~'E'(s('0'),f(B_87)))|~iLEQ(suc(B_87),suc(B_88)))|~'E'(s('0'),f(suc(A_4))))|~'E'(s('0'),f(A_4)))|~iLEQ(suc(A_4),suc(B_87)))|'E'(f(A_4),f(suc(A_4)))))|'E'(f(B_87),f(suc(B_87)))))|'E'(f(B_88),f(suc(B_88))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f756])).
% 198.99/25.82  fof(f2678,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X1))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2677])).
% 198.99/25.82  fof(f2783,plain,(
% 198.99/25.82    ![B_33]: ((![B_32]: ((![A_1]: ((((((((~iLEQ(suc(B_32),suc(B_33))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|~'E'(s(s(s(s('0')))),f(B_33)))|~'E'(s(s(s(s('0')))),f(suc(B_32))))|~iLEQ(suc(A_1),suc(B_32)))|~'E'(s(s(s(s('0')))),f(A_1)))|~'E'(s(s(s(s('0')))),f(B_32)))|~'E'(s(s(s(s('0')))),f(suc(B_33))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_32),f(suc(B_32)))))|'E'(f(B_33),f(suc(B_33))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f809])).
% 198.99/25.82  fof(f2784,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2783])).
% 198.99/25.82  fof(f2869,plain,(
% 198.99/25.82    ![A_4]: (((~'E'(s('0'),f(A_4))|~'E'(s('0'),f(suc(A_4))))|'E'(f(A_4),f(suc(A_4))))|iLEQ(suc(A_4),suc(A_4)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f852])).
% 198.99/25.82  fof(f2870,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2869])).
% 198.99/25.82  fof(f2883,plain,(
% 198.99/25.82    ![B_95]: ((![B_94]: ((((((![A_5]: (((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(A_5))))|~'E'('0',f(suc(suc(A_5)))))|~'E'(f(A_5),f(suc(A_5)))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94)))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95)))|'E'(f(B_94),f(suc(B_94)))))|'E'(f(B_95),f(suc(B_95))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f859])).
% 198.99/25.82  fof(f2884,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2883])).
% 198.99/25.82  fof(f2953,plain,(
% 198.99/25.82    ![B_31]: ((~'LE'(f(B_31),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(B_31)))|'LE'(f(B_31),s(s(s(s('0'))))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f894])).
% 198.99/25.82  fof(f2954,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(X0),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(X0))|'LE'(f(X0),s(s(s(s('0'))))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2953])).
% 198.99/25.82  fof(f2971,plain,(
% 198.99/25.82    ![A_4]: ((![B_87]: (((![B_88]: (((((((((~'E'(s('0'),f(B_88))|~'E'(s('0'),f(suc(B_88))))|~'E'(s('0'),f(suc(suc(B_87)))))|~'E'(f(B_87),f(suc(B_87))))|~'E'(f(B_88),f(suc(B_88))))|~'E'(s('0'),f(suc(B_87))))|~'E'(s('0'),f(B_87)))|~iLEQ(suc(B_87),suc(B_88)))|~'E'(s('0'),f(suc(A_4))))|~'E'(s('0'),f(suc(suc(B_88))))))|~'E'(s('0'),f(A_4)))|~iLEQ(suc(A_4),suc(B_87))))|'E'(f(A_4),f(suc(A_4))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f903])).
% 198.99/25.82  fof(f2972,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X1))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2971])).
% 198.99/25.82  fof(f2993,plain,(
% 198.99/25.82    ![B_74]: ((~'LE'(f(suc(suc(B_74))),s(s(s('0'))))|'E'(s(s('0')),f(suc(suc(B_74)))))|'LE'(f(B_74),s(s('0'))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f914])).
% 198.99/25.82  fof(f2994,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s(s(s('0'))))|'E'(s(s('0')),f(suc(suc(X0))))|'LE'(f(X0),s(s('0'))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f2993])).
% 198.99/25.82  fof(f3029,plain,(
% 198.99/25.82    ![B_57]: ((![A_2]: (((![B_58]: ((((((((((~'E'(s(s(s('0'))),f(suc(suc(B_58))))|~iLEQ(suc(A_2),suc(B_57)))|~'E'(s(s(s('0'))),f(B_57)))|~'E'(s(s(s('0'))),f(suc(A_2))))|~iLEQ(suc(B_57),suc(B_58)))|~'E'(s(s(s('0'))),f(A_2)))|~'E'(s(s(s('0'))),f(suc(B_57))))|~'E'(f(B_58),f(suc(B_58))))|~'E'(f(B_57),f(suc(B_57))))|~'E'(s(s(s('0'))),f(B_58)))|~'E'(s(s(s('0'))),f(suc(B_58)))))|~'E'(s(s(s('0'))),f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(A_2)))))|~'E'(s(s(s('0'))),f(suc(suc(B_57)))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f932])).
% 198.99/25.82  fof(f3030,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s('0'))),f(suc(suc(X2)))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3029])).
% 198.99/25.82  fof(f3051,plain,(
% 198.99/25.82    ![A_3]: (((~'E'(s(s('0')),f(A_3))|~'E'(s(s('0')),f(suc(A_3))))|'E'(f(A_3),f(suc(A_3))))|iLEQ(suc(A_3),suc(A_3)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f943])).
% 198.99/25.82  fof(f3052,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3051])).
% 198.99/25.82  fof(f3117,plain,(
% 198.99/25.82    ![A_5]: ((![B_95]: (((![B_94]: (((((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(suc(B_94)))))|~'E'('0',f(suc(suc(B_95)))))|~'E'('0',f(suc(A_5))))|~'E'(f(B_95),f(suc(B_95))))|~'E'(f(B_94),f(suc(B_94))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94))))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95))))|'E'(f(A_5),f(suc(A_5))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f976])).
% 198.99/25.82  fof(f3118,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3117])).
% 198.99/25.82  fof(f3129,plain,(
% 198.99/25.82    ![A_3]: ((![B_75]: ((((((![B_76]: (((((((~'E'(s(s('0')),f(suc(B_75)))|~'E'(s(s('0')),f(suc(A_3))))|~'E'(s(s('0')),f(suc(B_76))))|~'E'(f(B_76),f(suc(B_76))))|~'E'(s(s('0')),f(B_76)))|~'E'(s(s('0')),f(suc(suc(A_3)))))|~iLEQ(suc(B_75),suc(B_76)))|~'E'(s(s('0')),f(suc(suc(B_76))))))|~'E'(f(A_3),f(suc(A_3))))|~'E'(s(s('0')),f(suc(suc(B_75)))))|~iLEQ(suc(A_3),suc(B_75)))|~'E'(s(s('0')),f(B_75)))|~'E'(f(B_75),f(suc(B_75)))))|~'E'(s(s('0')),f(A_3)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f982])).
% 198.99/25.82  fof(f3130,plain,(
% 198.99/25.82    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(f(X2),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(suc(X2))))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3129])).
% 198.99/25.82  fof(f3225,plain,(
% 198.99/25.82    ![B_95]: ((![B_94]: ((![A_5]: ((((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(A_5))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94)))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95)))|'E'(f(A_5),f(suc(A_5)))))|'E'(f(B_94),f(suc(B_94)))))|'E'(f(B_95),f(suc(B_95))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1030])).
% 198.99/25.82  fof(f3226,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3225])).
% 198.99/25.82  fof(f3227,plain,(
% 198.99/25.82    ![B_56]: ((~'LE'(f(B_56),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(B_56)))|'LE'(f(B_56),s(s(s('0')))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1031])).
% 198.99/25.82  fof(f3228,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(X0),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3227])).
% 198.99/25.82  fof(f3309,plain,(
% 198.99/25.82    ![B_95]: ((![A_5]: ((((![B_94]: (((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(suc(B_94)))))|~'E'('0',f(suc(A_5))))|~'E'(f(B_94),f(suc(B_94))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94))))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95)))|'E'(f(A_5),f(suc(A_5)))))|'E'(f(B_95),f(suc(B_95))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1072])).
% 198.99/25.82  fof(f3310,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3309])).
% 198.99/25.82  fof(f3315,plain,(
% 198.99/25.82    ![B_93]: ((~'LE'(f(suc(B_93)),s('0'))|'E'('0',f(suc(B_93))))|'LE'(f(B_93),'0'))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1075])).
% 198.99/25.82  fof(f3316,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(X0)),s('0'))|'E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3315])).
% 198.99/25.82  fof(f3335,plain,(
% 198.99/25.82    ![A_1]: (((~'E'(s(s(s(s('0')))),f(A_1))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|'E'(f(A_1),f(suc(A_1))))|iLEQ(suc(A_1),suc(A_1)))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1085])).
% 198.99/25.82  fof(f3336,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3335])).
% 198.99/25.82  fof(f3383,plain,(
% 198.99/25.82    ![B_95]: ((((![B_94]: (((![A_5]: (((((((~iLEQ(suc(A_5),suc(B_94))|~'E'('0',f(A_5)))|~'E'('0',f(suc(B_94))))|~'E'('0',f(suc(suc(B_94)))))|~'E'('0',f(suc(A_5))))|~'E'('0',f(suc(suc(A_5)))))|~'E'(f(B_94),f(suc(B_94))))|~'E'(f(A_5),f(suc(A_5)))))|~iLEQ(suc(B_94),suc(B_95)))|~'E'('0',f(B_94))))|~'E'('0',f(suc(B_95))))|~'E'('0',f(B_95)))|'E'(f(B_95),f(suc(B_95))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1109])).
% 198.99/25.82  fof(f3384,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3383])).
% 198.99/25.82  fof(f3467,plain,(
% 198.99/25.82    ![B_31]: ((~'LE'(f(suc(B_31)),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(suc(B_31))))|'LE'(f(B_31),s(s(s(s('0'))))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1151])).
% 198.99/25.82  fof(f3468,plain,(
% 198.99/25.82    ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0'))))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3467])).
% 198.99/25.82  fof(f3485,plain,(
% 198.99/25.82    ![B_58]: ((![B_57]: ((![A_2]: ((((((((~iLEQ(suc(A_2),suc(B_57))|~'E'(s(s(s('0'))),f(B_57)))|~'E'(s(s(s('0'))),f(suc(A_2))))|~iLEQ(suc(B_57),suc(B_58)))|~'E'(s(s(s('0'))),f(A_2)))|~'E'(s(s(s('0'))),f(suc(B_57))))|~'E'(s(s(s('0'))),f(B_58)))|~'E'(s(s(s('0'))),f(suc(B_58))))|'E'(f(A_2),f(suc(A_2)))))|'E'(f(B_57),f(suc(B_57)))))|'E'(f(B_58),f(suc(B_58))))),
% 198.99/25.82    inference(miniscoping,[status(thm)],[f1160])).
% 198.99/25.82  fof(f3486,plain,(
% 198.99/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 198.99/25.82    inference(cnf_transformation,[status(thm)],[f3485])).
% 198.99/25.82  fof(f4444,plain,(
% 198.99/25.82    ![E,X0]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f2606,f2328])).
% 198.99/25.82  fof(f4449,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1887,f2870])).
% 198.99/25.82  fof(f4451,plain,(
% 198.99/25.82    ![E,X0]: (~'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)))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1725,f3052])).
% 198.99/25.82  fof(f4453,plain,(
% 198.99/25.82    ![E,X0,LE]: ('E'(s(s(s(s('0')))),f(X0))|'LE'(f(X0),s(s(s(s('0'))))))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f2954,f1351])).
% 198.99/25.82  fof(f4460,plain,(
% 198.99/25.82    ![E,X0]: (~'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)))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1547,f1463])).
% 198.99/25.82  fof(f4472,plain,(
% 198.99/25.82    ![E,X0,LE]: ('E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0'))))))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f3468,f1351])).
% 198.99/25.82  fof(f4502,plain,(
% 198.99/25.82    ![E,X0]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f2106,f3336])).
% 198.99/25.82  fof(f4546,plain,(
% 198.99/25.82    ![E,X0,LE]: ('E'(s(s(s(s('0')))),f(suc(suc(X0))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f2326,f1351])).
% 198.99/25.82  fof(f4548,plain,(
% 198.99/25.82    ![LE,X0,E]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(resolution,[status(thm)],[f4546,f4502])).
% 198.99/25.82  fof(f4550,plain,(
% 198.99/25.82    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1))))),
% 198.99/25.82    inference(resolution,[status(thm)],[f4546,f1457])).
% 198.99/25.82  fof(f4560,plain,(
% 198.99/25.82    ![LE,X0,E]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(s(s(s(s('0')))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 198.99/25.82    inference(forward_subsumption_resolution,[status(thm)],[f4548,f4472])).
% 198.99/25.82  fof(f4562,plain,(
% 198.99/25.82    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f4550,f4472])).
% 199.78/25.82  fof(f4570,plain,(
% 199.78/25.82    ![LE,X0]: ('LE'(f(X0),s(s(s(s('0')))))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f4560,f4453])).
% 199.78/25.82  fof(f4571,plain,(
% 199.78/25.82    ![X0,E,LE]: (iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))|'E'(s(s(s('0'))),f(suc(suc(X0))))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f4570,f1445])).
% 199.78/25.82  fof(f4572,plain,(
% 199.78/25.82    ![X0,E,LE]: (iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f4570,f1505])).
% 199.78/25.82  fof(f4573,plain,(
% 199.78/25.82    ![X0,E,LE]: (iLEQ(suc(X0),suc(X0))|'E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f4570,f3228])).
% 199.78/25.82  fof(f4595,plain,(
% 199.78/25.82    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f1593,f4546])).
% 199.78/25.82  fof(f4598,plain,(
% 199.78/25.82    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f4595,f4472])).
% 199.78/25.82  fof(f4924,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1783,f1837])).
% 199.78/25.82  fof(f4968,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f3118,f1837])).
% 199.78/25.82  fof(f5214,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2)))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1417,f3384])).
% 199.78/25.82  fof(f5473,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f1425,f2340])).
% 199.78/25.82  fof(f5486,plain,(
% 199.78/25.82    ![E,X0,X1]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(X1))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(factoring,[status(thm)],[f2340])).
% 199.78/25.82  fof(f5494,plain,(
% 199.78/25.82    ![E,X0,X1]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(X1))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(duplicate_literals_removal,[status(thm)],[f5486])).
% 199.78/25.82  fof(f5805,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1583,f1211])).
% 199.78/25.82  fof(f6440,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X1))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f2108,f2678])).
% 199.78/25.82  fof(f6451,plain,(
% 199.78/25.82    ![E,X0,X1]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(factoring,[status(thm)],[f2678])).
% 199.78/25.82  fof(f6455,plain,(
% 199.78/25.82    ![E,X0,X1]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X1),suc(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(duplicate_literals_removal,[status(thm)],[f6451])).
% 199.78/25.82  fof(f6456,plain,(
% 199.78/25.82    ![E,X0,X1]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f6455,f2870])).
% 199.78/25.82  fof(f6471,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(f(X1),f(suc(X1)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X2))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f2582,f6456])).
% 199.78/25.82  fof(f6605,plain,(
% 199.78/25.82    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f2784,f4472])).
% 199.78/25.82  fof(f6608,plain,(
% 199.78/25.82    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f6605,f4453])).
% 199.78/25.82  fof(f6679,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f4924,f6680])).
% 199.78/25.82  fof(f6680,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f2884,f3226])).
% 199.78/25.82  fof(f6694,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2)))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f5214,f6679])).
% 199.78/25.82  fof(f7533,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f4968,f7534])).
% 199.78/25.82  fof(f7534,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f3310,f3226])).
% 199.78/25.82  fof(f7581,plain,(
% 199.78/25.82    ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X2)))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f6694,f7533])).
% 199.78/25.82  fof(f7910,plain,(
% 199.78/25.82    ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X0)))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(s(s(s('0'))),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(factoring,[status(thm)],[f3486])).
% 199.78/25.82  fof(f7921,plain,(
% 199.78/25.82    ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X0)))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(duplicate_literals_removal,[status(thm)],[f7910])).
% 199.78/25.82  fof(f7922,plain,(
% 199.78/25.82    ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f7921,f1463])).
% 199.78/25.82  fof(f7932,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f5805,f7922])).
% 199.78/25.82  fof(f8240,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(f(X1),f(suc(X1)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X2)))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f1934,f6471])).
% 199.78/25.82  fof(f8497,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f1970,f4546])).
% 199.78/25.82  fof(f8507,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(X0))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(duplicate_literals_removal,[status(thm)],[f8497])).
% 199.78/25.82  fof(f8508,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(X0))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f8507,f4472])).
% 199.78/25.82  fof(f9213,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s(s('0')))),f(X0))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f8508,f4453])).
% 199.78/25.82  fof(f9214,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X0),suc(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f9213,f4546])).
% 199.78/25.82  fof(f9217,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f9214,f4570])).
% 199.78/25.82  fof(f9220,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f9217,f4453])).
% 199.78/25.82  fof(f9222,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f9220,f4472])).
% 199.78/25.82  fof(f9224,plain,(
% 199.78/25.82    ![E,X0,X1,LE]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.82    inference(duplicate_literals_removal,[status(thm)],[f9222])).
% 199.78/25.82  fof(f9934,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X2)))),
% 199.78/25.82    inference(backward_subsumption_resolution,[status(thm)],[f8240,f9935])).
% 199.78/25.82  fof(f9935,plain,(
% 199.78/25.82    ![E,X0,X1,X2]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X1))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f2972,f6440])).
% 199.78/25.82  fof(f10195,plain,(
% 199.78/25.82    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f4562,f4453])).
% 199.78/25.82  fof(f10197,plain,(
% 199.78/25.82    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.82    inference(resolution,[status(thm)],[f10195,f4472])).
% 199.78/25.82  fof(f10200,plain,(
% 199.78/25.82    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.82    inference(forward_subsumption_resolution,[status(thm)],[f10197,f4453])).
% 199.78/25.82  fof(f10266,plain,(
% 199.78/25.82    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f4598,f4453])).
% 199.78/25.83  fof(f10268,plain,(
% 199.78/25.83    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X2))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f10266,f4472])).
% 199.78/25.83  fof(f10271,plain,(
% 199.78/25.83    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f10268,f4453])).
% 199.78/25.83  fof(f10375,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(suc(X1)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f10200,f9224])).
% 199.78/25.83  fof(f10377,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X2),suc(X0))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f10375,f4472])).
% 199.78/25.83  fof(f10380,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f10377,f4453])).
% 199.78/25.83  fof(f10412,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f10380,f9224])).
% 199.78/25.83  fof(f12277,plain,(
% 199.78/25.83    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(X1))|'E'(f(X2),f(suc(X2))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f2346,f5473])).
% 199.78/25.83  fof(f13993,plain,(
% 199.78/25.83    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f6608,f4472])).
% 199.78/25.83  fof(f13996,plain,(
% 199.78/25.83    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f13993,f4453])).
% 199.78/25.83  fof(f15492,plain,(
% 199.78/25.83    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f13996,f10271])).
% 199.78/25.83  fof(f15494,plain,(
% 199.78/25.83    ![X0,X1,X2,E,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f15492,f4472])).
% 199.78/25.83  fof(f15497,plain,(
% 199.78/25.83    ![X0,X1,X2,E,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f15494,f4453])).
% 199.78/25.83  fof(f15526,plain,(
% 199.78/25.83    ![X0,X1,X2,E,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'E'(f(X2),f(suc(X2)))|'LE'(f(X2),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f15497,f10412])).
% 199.78/25.83  fof(f15571,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f15526,f4570])).
% 199.78/25.83  fof(f15619,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f15571])).
% 199.78/25.83  fof(f15620,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(backward_subsumption_resolution,[status(thm)],[f9224,f15619])).
% 199.78/25.83  fof(f15667,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f15619,f4570])).
% 199.78/25.83  fof(f15715,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0'))))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f15667])).
% 199.78/25.83  fof(f16106,plain,(
% 199.78/25.83    ![X0,X1,LE]: (~iLEQ(suc(X0),suc(X1))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X1),s(s(s(s('0'))))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f15620,f15715])).
% 199.78/25.83  fof(f16125,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(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(X0))))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16106,f4571])).
% 199.78/25.83  fof(f16148,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(X0)),s(s(s(s('0')))))|'LE'(f(suc(X0)),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16106,f4572])).
% 199.78/25.83  fof(f16150,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16106,f4573])).
% 199.78/25.83  fof(f16170,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(suc(X0))),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(suc(X0))))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f16125])).
% 199.78/25.83  fof(f16171,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s(s(s('0'))),f(suc(suc(X0))))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f16170,f1445])).
% 199.78/25.83  fof(f16194,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(X0)),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f16148])).
% 199.78/25.83  fof(f16195,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f16194,f1505])).
% 199.78/25.83  fof(f16197,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f16150])).
% 199.78/25.83  fof(f16198,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f16197,f3228])).
% 199.78/25.83  fof(f16382,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(s(s(s('0'))),f(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16195,f7922])).
% 199.78/25.83  fof(f16470,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(s(s(s('0'))),f(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f16382,f16198])).
% 199.78/25.83  fof(f16530,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16171,f4460])).
% 199.78/25.83  fof(f16620,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f16530,f16195])).
% 199.78/25.83  fof(f16674,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s(s(s('0'))))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f16620,f16198])).
% 199.78/25.83  fof(f16676,plain,(
% 199.78/25.83    ![X0,E,LE]: (iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16674,f1437])).
% 199.78/25.83  fof(f16677,plain,(
% 199.78/25.83    ![X0,E,LE]: (iLEQ(suc(X0),suc(X0))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16674,f2170])).
% 199.78/25.83  fof(f17348,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s(s('0'))),f(X1))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f16470,f16195])).
% 199.78/25.83  fof(f17351,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X0))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f17348,f16198])).
% 199.78/25.83  fof(f17380,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f17351,f16674])).
% 199.78/25.83  fof(f17399,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f17380])).
% 199.78/25.83  fof(f17694,plain,(
% 199.78/25.83    ![E,X0,X1,X2]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s('0'))),f(suc(suc(X2)))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f3030,f7932])).
% 199.78/25.83  fof(f17704,plain,(
% 199.78/25.83    ![E,X0,X1]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(factoring,[status(thm)],[f17694])).
% 199.78/25.83  fof(f17715,plain,(
% 199.78/25.83    ![E,X0,X1]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f17704])).
% 199.78/25.83  fof(f17716,plain,(
% 199.78/25.83    ![E,X0,X1]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(s(s(s('0'))),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f17715,f4460])).
% 199.78/25.83  fof(f17797,plain,(
% 199.78/25.83    ![E,X0,X1,LE]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f17716,f16171])).
% 199.78/25.83  fof(f17800,plain,(
% 199.78/25.83    ![E,X0,X1,LE]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~'E'(s(s(s('0'))),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f17797,f16195])).
% 199.78/25.83  fof(f17807,plain,(
% 199.78/25.83    ![E,X0,X1,LE]: (~'E'(s(s(s('0'))),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f17800,f16198])).
% 199.78/25.83  fof(f17808,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f17807,f16171])).
% 199.78/25.83  fof(f17811,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f17808,f17399])).
% 199.78/25.83  fof(f18033,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f17811,f16198])).
% 199.78/25.83  fof(f18035,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X1),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18033,f16195])).
% 199.78/25.83  fof(f18038,plain,(
% 199.78/25.83    ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f18035])).
% 199.78/25.83  fof(f18039,plain,(
% 199.78/25.83    ![X0,X1,LE]: (~iLEQ(suc(X0),suc(X1))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18038,f17399])).
% 199.78/25.83  fof(f18058,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(X0)),s(s(s('0'))))|'LE'(f(suc(X0)),s(s(s('0'))))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18039,f16676])).
% 199.78/25.83  fof(f18059,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s('0'))))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18039,f16677])).
% 199.78/25.83  fof(f18060,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18039,f16674])).
% 199.78/25.83  fof(f18079,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(X0)),s(s(s('0'))))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f18058])).
% 199.78/25.83  fof(f18080,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18079,f1437])).
% 199.78/25.83  fof(f18081,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f18059])).
% 199.78/25.83  fof(f18082,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18081,f2170])).
% 199.78/25.83  fof(f18083,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s(s(s('0')))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f18060])).
% 199.78/25.83  fof(f18084,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s(s('0')),f(suc(suc(X0))))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(backward_subsumption_resolution,[status(thm)],[f2994,f18083])).
% 199.78/25.83  fof(f18209,plain,(
% 199.78/25.83    ![LE,X0,E,X1]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(X0))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s('0')),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18080,f5494])).
% 199.78/25.83  fof(f18270,plain,(
% 199.78/25.83    ![LE,X0,E,X1]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s('0')),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18209,f18082])).
% 199.78/25.83  fof(f18319,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18084,f4451])).
% 199.78/25.83  fof(f18380,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18319,f18080])).
% 199.78/25.83  fof(f18405,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s(s('0')))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18380,f18082])).
% 199.78/25.83  fof(f18406,plain,(
% 199.78/25.83    ![X0,E,LE]: (iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))|'E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18405,f2236])).
% 199.78/25.83  fof(f18407,plain,(
% 199.78/25.83    ![X0,E,LE]: (iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18405,f2550])).
% 199.78/25.83  fof(f18408,plain,(
% 199.78/25.83    ![X0,E,LE]: (iLEQ(suc(X0),suc(X0))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18405,f1473])).
% 199.78/25.83  fof(f18447,plain,(
% 199.78/25.83    ![E,X0,X1,X2]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(suc(X2))))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f3130,f12277])).
% 199.78/25.83  fof(f18448,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1))|'LE'(f(X2),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18447,f18084])).
% 199.78/25.83  fof(f18451,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1))|'LE'(f(X2),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18448,f18080])).
% 199.78/25.83  fof(f18942,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s('0')),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18270,f18080])).
% 199.78/25.83  fof(f18944,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18942,f18082])).
% 199.78/25.83  fof(f18956,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X0),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f18944,f18405])).
% 199.78/25.83  fof(f18972,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X0),suc(X0))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f18956])).
% 199.78/25.83  fof(f18973,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18972,f18405])).
% 199.78/25.83  fof(f19076,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1))|'LE'(f(X2),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f18451,f18082])).
% 199.78/25.83  fof(f19077,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X1))|'LE'(f(X2),s(s('0')))|'LE'(f(X1),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19076,f18084])).
% 199.78/25.83  fof(f19080,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X2),f(suc(X2)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(s(s('0')),f(X2))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19077,f18080])).
% 199.78/25.83  fof(f19732,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X2),f(suc(X2)))|~'E'(s(s('0')),f(suc(suc(X0))))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19080,f18082])).
% 199.78/25.83  fof(f19733,plain,(
% 199.78/25.83    ![E,X0,X1,X2,LE]: (~'E'(s(s('0')),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19732,f18084])).
% 199.78/25.83  fof(f19736,plain,(
% 199.78/25.83    ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19733,f18080])).
% 199.78/25.83  fof(f19739,plain,(
% 199.78/25.83    ![X0,X1,X2,E,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19736,f18973])).
% 199.78/25.83  fof(f19742,plain,(
% 199.78/25.83    ![X0,X1,X2,E,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0')))|'LE'(f(X0),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19739,f18082])).
% 199.78/25.83  fof(f19745,plain,(
% 199.78/25.83    ![X0,X1,X2,E,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f19742])).
% 199.78/25.83  fof(f19746,plain,(
% 199.78/25.83    ![X0,X1,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19745,f18973])).
% 199.78/25.83  fof(f19758,plain,(
% 199.78/25.83    ![X0,X1,LE]: (~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s(s('0')))|'LE'(f(X0),s(s('0')))|'LE'(f(X0),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19746,f18405])).
% 199.78/25.83  fof(f19773,plain,(
% 199.78/25.83    ![X0,X1,LE]: (~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f19758])).
% 199.78/25.83  fof(f19775,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(suc(X0))),s(s('0')))|'LE'(f(suc(suc(X0))),s(s('0')))|'E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19773,f18406])).
% 199.78/25.83  fof(f19783,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(X0)),s(s('0')))|'LE'(f(suc(X0)),s(s('0')))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19773,f18407])).
% 199.78/25.83  fof(f19784,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|'LE'(f(X0),s(s('0')))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19773,f18408])).
% 199.78/25.83  fof(f19787,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(suc(X0))),s(s('0')))|'E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f19775])).
% 199.78/25.83  fof(f19788,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19787,f2236])).
% 199.78/25.83  fof(f19796,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(suc(X0)),s(s('0')))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f19783])).
% 199.78/25.83  fof(f19797,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19796,f2550])).
% 199.78/25.83  fof(f19798,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f19784])).
% 199.78/25.83  fof(f19799,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19798,f1473])).
% 199.78/25.83  fof(f19891,plain,(
% 199.78/25.83    ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X0))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19797,f6456])).
% 199.78/25.83  fof(f19931,plain,(
% 199.78/25.83    ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19891,f19799])).
% 199.78/25.83  fof(f19937,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0)))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19788,f9934])).
% 199.78/25.83  fof(f19953,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19788,f4449])).
% 199.78/25.83  fof(f19959,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19937,f19799])).
% 199.78/25.83  fof(f19975,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19953,f19797])).
% 199.78/25.83  fof(f19979,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s('0'))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19975,f19799])).
% 199.78/25.83  fof(f20036,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f19959,f19797])).
% 199.78/25.83  fof(f20050,plain,(
% 199.78/25.83    ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f19931,f19797])).
% 199.78/25.83  fof(f20053,plain,(
% 199.78/25.83    ![LE,X0,X1,E]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20050,f19799])).
% 199.78/25.83  fof(f20060,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s('0'))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),s('0'))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20053,f19979])).
% 199.78/25.83  fof(f20067,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),s('0'))|'E'(f(X0),f(suc(X0))))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f20060])).
% 199.78/25.83  fof(f20068,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(suc(suc(X2))))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0)))),
% 199.78/25.83    inference(backward_subsumption_resolution,[status(thm)],[f20036,f20067])).
% 199.78/25.83  fof(f20069,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(X2))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20068,f19788])).
% 199.78/25.83  fof(f20072,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(X2)))|~'E'(s('0'),f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20069,f19799])).
% 199.78/25.83  fof(f20140,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20072,f19797])).
% 199.78/25.83  fof(f20141,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s('0'))|'LE'(f(X1),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20140,f19788])).
% 199.78/25.83  fof(f20144,plain,(
% 199.78/25.83    ![LE,X0,E,X1,X2]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s('0'))|'LE'(f(X1),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20141,f19799])).
% 199.78/25.83  fof(f20146,plain,(
% 199.78/25.83    ![LE,X0,X1,X2]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),s('0'))|'LE'(f(X1),s('0')))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20144,f19797])).
% 199.78/25.83  fof(f20153,plain,(
% 199.78/25.83    ![LE,X0,X1]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X0),s('0'))|'LE'(f(X1),s('0'))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20146,f19979])).
% 199.78/25.83  fof(f20160,plain,(
% 199.78/25.83    ![LE,X0,X1]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s('0')))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f20153])).
% 199.78/25.83  fof(f20167,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s('0'))|'LE'(f(X0),s('0'))|'LE'(f(X0),s('0')))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20160,f19979])).
% 199.78/25.83  fof(f20174,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),s('0')))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f20167])).
% 199.78/25.83  fof(f20184,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 199.78/25.83    inference(backward_subsumption_resolution,[status(thm)],[f2486,f20174])).
% 199.78/25.83  fof(f20185,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 199.78/25.83    inference(backward_subsumption_resolution,[status(thm)],[f3316,f20174])).
% 199.78/25.83  fof(f20186,plain,(
% 199.78/25.83    ![E,X0,LE]: ('E'('0',f(X0))|'LE'(f(X0),'0'))),
% 199.78/25.83    inference(backward_subsumption_resolution,[status(thm)],[f1619,f20174])).
% 199.78/25.83  fof(f20187,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0)))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20184,f7581])).
% 199.78/25.83  fof(f20197,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20184,f4444])).
% 199.78/25.83  fof(f20293,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X0))))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20187,f20186])).
% 199.78/25.83  fof(f20294,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X0)))|'LE'(f(X2),'0'))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20293,f20184])).
% 199.78/25.83  fof(f20297,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(X0)))|'LE'(f(X2),'0'))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20294,f20186])).
% 199.78/25.83  fof(f20300,plain,(
% 199.78/25.83    ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20197,f20185])).
% 199.78/25.83  fof(f20303,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),'0')|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20300,f20186])).
% 199.78/25.83  fof(f20304,plain,(
% 199.78/25.83    ![LE,X0]: ('LE'(f(X0),'0')|iLEQ(suc(X0),suc(X0)))),
% 199.78/25.83    inference(duplicate_literals_removal,[status(thm)],[f20303])).
% 199.78/25.83  fof(f20671,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),'0'))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20297,f20185])).
% 199.78/25.83  fof(f20672,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),'0')|'LE'(f(X1),'0'))),
% 199.78/25.83    inference(resolution,[status(thm)],[f20671,f20184])).
% 199.78/25.83  fof(f20675,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),'0')|'LE'(f(X1),'0'))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20672,f20186])).
% 199.78/25.83  fof(f20717,plain,(
% 199.78/25.83    ![LE,X0,X1,X2,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),'0')|'LE'(f(X1),'0'))),
% 199.78/25.83    inference(forward_subsumption_resolution,[status(thm)],[f20675,f20185])).
% 199.78/25.85  fof(f20719,plain,(
% 199.78/25.85    ![LE,X0,X1,X2]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),'0')|'LE'(f(X1),'0')|'LE'(f(X1),'0'))),
% 199.78/25.85    inference(resolution,[status(thm)],[f20717,f20185])).
% 199.78/25.85  fof(f20721,plain,(
% 199.78/25.85    ![LE,X0,X1,X2]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X2))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X2),'0')|'LE'(f(X1),'0'))),
% 199.78/25.85    inference(duplicate_literals_removal,[status(thm)],[f20719])).
% 199.78/25.85  fof(f20724,plain,(
% 199.78/25.85    ![LE,X0,X1]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X0))|'LE'(f(X0),'0')|'LE'(f(X1),'0')|'LE'(f(X0),'0'))),
% 199.78/25.85    inference(resolution,[status(thm)],[f20721,f20304])).
% 199.78/25.85  fof(f20727,plain,(
% 199.78/25.85    ![LE,X0,X1]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),'0'))),
% 199.78/25.85    inference(duplicate_literals_removal,[status(thm)],[f20724])).
% 199.78/25.85  fof(f20730,plain,(
% 199.78/25.85    ![LE,X0]: ('LE'(f(X0),'0')|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 199.78/25.85    inference(resolution,[status(thm)],[f20727,f20304])).
% 199.78/25.85  fof(f20733,plain,(
% 199.78/25.85    ![LE,X0]: ('LE'(f(X0),'0'))),
% 199.78/25.85    inference(duplicate_literals_removal,[status(thm)],[f20730])).
% 199.78/25.85  fof(f20741,plain,(
% 199.78/25.85    $false),
% 199.78/25.85    inference(backward_subsumption_resolution,[status(thm)],[f1898,f20733])).
% 199.78/25.85  % SZS output end CNFRefutation for theBenchmark.p
% 199.78/25.89  % Elapsed time: 25.528059 seconds
% 199.78/25.89  % CPU time: 200.254333 seconds
% 199.78/25.89  % Total memory used: 331.671 MB
% 199.78/25.89  % Net memory used: 299.224 MB
%------------------------------------------------------------------------------