%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO653-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:43 PM UTC 2026
% Result : Unsatisfiable 66.58s 8.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO653-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 12:09:31 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 66.58/8.92 % Refutation found
% 66.58/8.92 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 66.58/8.92 % SZS output start CNFRefutation for theBenchmark
% 66.58/8.92 fof(f3,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f5,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f7,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ 'E'('0',f(suc(suc(suc(B_11)))))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'(f(B_11),f(suc(suc(B_11))))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f8,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f9,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f12,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f14,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f18,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f19,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f20,axiom,(
% 66.58/8.92 (![E,A_1]: (( ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(A_1))| 'E'(f(A_1),f(suc(suc(A_1))))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f21,axiom,(
% 66.58/8.92 (![LE]: (~ 'LE'(f(z),'0') ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f24,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f25,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f27,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(suc(B_12))))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f29,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f30,axiom,(
% 66.58/8.92 (![LE,A]: ('LE'(f(A),s('0')) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f31,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f34,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f35,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f38,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(B_12))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f42,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ 'E'('0',f(suc(suc(suc(B_11)))))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'(f(B_11),f(suc(suc(B_11))))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f48,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f50,axiom,(
% 66.58/8.92 (![LE,B_10,E]: (( ~ 'LE'(f(suc(B_10)),s('0'))| 'E'('0',f(suc(B_10)))| 'LE'(f(B_10),'0') ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f52,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(B_11))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f54,axiom,(
% 66.58/8.92 (![LE,B_10,E]: (( ~ 'LE'(f(B_10),s('0'))| 'E'('0',f(B_10))| 'LE'(f(B_10),'0') ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f56,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ 'E'('0',f(suc(suc(suc(B_11)))))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'(f(B_11),f(suc(suc(B_11))))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12)) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f59,axiom,(
% 66.58/8.92 (![LE,B_10,E]: (( ~ 'LE'(f(suc(suc(suc(B_10)))),s('0'))| 'E'('0',f(suc(suc(suc(B_10)))))| 'LE'(f(B_10),'0') ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f60,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(suc(B_12))))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f62,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ 'E'('0',f(suc(suc(suc(B_11)))))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'(f(B_11),f(suc(suc(B_11))))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f63,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(B_11)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f66,axiom,(
% 66.58/8.92 (![E,A_1,B_11,B_12,B_13]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_13),f(suc(suc(B_13))))| ~ 'E'(f(B_12),f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(suc(B_13)))))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ 'E'('0',f(suc(suc(suc(B_12)))))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(B_11),f(suc(B_11))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f68,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(suc(B_12))))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f72,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ 'E'('0',f(suc(suc(suc(B_11)))))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'(f(B_11),f(suc(suc(B_11))))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_12),f(suc(B_12)))| ~ 'E'('0',f(suc(suc(B_12))))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_12),f(suc(suc(B_12))))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f74,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f75,axiom,(
% 66.58/8.92 (![LE,B_10,E]: (( ~ 'LE'(f(suc(suc(B_10))),s('0'))| 'E'('0',f(suc(suc(B_10))))| 'LE'(f(B_10),'0') ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f80,axiom,(
% 66.58/8.92 (![E,A_1]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(A_1),f(suc(A_1)))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f83,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ 'E'('0',f(suc(suc(suc(B_11)))))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'(f(B_11),f(suc(suc(B_11))))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ 'E'('0',f(suc(suc(B_13))))| ~ 'E'(f(B_13),f(suc(B_13)))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(suc(B_13)))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f84,axiom,(
% 66.58/8.92 (![E,A_1]: (( ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(A_1)))| 'E'(f(A_1),f(suc(A_1)))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f87,axiom,(
% 66.58/8.92 (![E,B_11,B_12,B_13,A_1]: (( ~ 'E'('0',f(suc(B_11)))| ~ iLEQ(suc(B_12),suc(B_13))| ~ 'E'('0',f(suc(suc(B_11))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(B_11))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(B_13))| ~ 'E'('0',f(suc(B_12)))| ~ 'E'(f(B_11),f(suc(B_11)))| ~ iLEQ(suc(A_1),suc(B_11))| ~ 'E'('0',f(suc(B_13)))| ~ 'E'('0',f(B_12))| ~ iLEQ(suc(B_11),suc(B_12))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_11),f(suc(suc(B_11))))| 'E'(f(B_12),f(suc(B_12)))| 'E'(f(B_13),f(suc(B_13))) ) ))),
% 66.58/8.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.58/8.92 fof(f95,plain,(
% 66.58/8.92 ![B_13]: ((![B_11]: ((![A_1]: ((![B_12]: ((((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f3])).
% 66.58/8.92 fof(f96,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f95])).
% 66.58/8.92 fof(f99,plain,(
% 66.58/8.92 ![B_13]: ((![B_11]: ((![B_12]: (((((((![A_1]: ((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f5])).
% 66.58/8.92 fof(f100,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f99])).
% 66.58/8.92 fof(f103,plain,(
% 66.58/8.92 ![B_13]: ((![B_11,B_12]: (((((![A_1]: ((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~'E'('0',f(suc(suc(suc(B_11))))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'(f(B_11),f(suc(suc(B_11)))))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f7])).
% 66.58/8.92 fof(f104,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f103])).
% 66.58/8.92 fof(f105,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f8])).
% 66.58/8.92 fof(f106,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f105])).
% 66.58/8.92 fof(f107,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: (((((![A_1]: (((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f9])).
% 66.58/8.92 fof(f108,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f107])).
% 66.58/8.92 fof(f113,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f12])).
% 66.58/8.92 fof(f114,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f113])).
% 66.58/8.92 fof(f117,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f14])).
% 66.58/8.92 fof(f118,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f117])).
% 66.58/8.92 fof(f125,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f18])).
% 66.58/8.92 fof(f126,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f125])).
% 66.58/8.92 fof(f127,plain,(
% 66.58/8.92 ![B_13]: ((![B_11]: ((![A_1]: ((![B_12]: ((((((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f19])).
% 66.58/8.92 fof(f128,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f127])).
% 66.58/8.92 fof(f129,plain,(
% 66.58/8.92 ![A_1]: (((((~'E'('0',f(suc(suc(A_1))))|~'E'('0',f(suc(A_1))))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(A_1)))|'E'(f(A_1),f(suc(suc(A_1)))))|iLEQ(suc(A_1),suc(A_1)))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f20])).
% 66.58/8.92 fof(f130,plain,(
% 66.58/8.92 ![E,X0]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0)))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f129])).
% 66.58/8.92 fof(f131,plain,(
% 66.58/8.92 ![LE]: (~'LE'(f(z),'0'))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f21])).
% 66.58/8.92 fof(f136,plain,(
% 66.58/8.92 ![B_12]: ((![B_11]: ((![A_1]: (((![B_13]: (((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f24])).
% 66.58/8.92 fof(f137,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f136])).
% 66.58/8.92 fof(f138,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: (((((((![A_1]: (((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f25])).
% 66.58/8.92 fof(f139,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f138])).
% 66.58/8.92 fof(f142,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: (((((((![A_1]: (((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(suc(B_12))))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f27])).
% 66.58/8.92 fof(f143,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f142])).
% 66.58/8.92 fof(f146,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: (((((![A_1]: (((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f29])).
% 66.58/8.92 fof(f147,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f146])).
% 66.58/8.92 fof(f148,plain,(
% 66.58/8.92 ![A]: 'LE'(f(A),s('0'))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f30])).
% 66.58/8.92 fof(f149,plain,(
% 66.58/8.92 ![LE,X0]: ('LE'(f(X0),s('0')))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f148])).
% 66.58/8.92 fof(f150,plain,(
% 66.58/8.92 ![B_13]: ((![B_11]: ((![B_12]: (((((((![A_1]: ((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f31])).
% 66.58/8.92 fof(f151,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f150])).
% 66.58/8.92 fof(f156,plain,(
% 66.58/8.92 ![B_11]: ((![A_1]: ((![B_12]: (((![B_13]: ((((((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f34])).
% 66.58/8.92 fof(f157,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f156])).
% 66.58/8.92 fof(f158,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f35])).
% 66.58/8.92 fof(f159,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f158])).
% 66.58/8.92 fof(f164,plain,(
% 66.58/8.92 ![B_12]: ((![B_11]: ((![A_1]: (((![B_13]: (((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(B_12))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f38])).
% 66.58/8.92 fof(f165,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f164])).
% 66.58/8.92 fof(f172,plain,(
% 66.58/8.92 ![B_13]: ((![B_11,B_12]: (((((((![A_1]: ((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~'E'('0',f(suc(suc(suc(B_11))))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'(f(B_11),f(suc(suc(B_11)))))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f42])).
% 66.58/8.92 fof(f173,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f172])).
% 66.58/8.92 fof(f184,plain,(
% 66.58/8.92 ![B_13]: ((![B_11]: ((![A_1]: ((![B_12]: ((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f48])).
% 66.58/8.92 fof(f185,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f184])).
% 66.58/8.92 fof(f188,plain,(
% 66.58/8.92 ![B_10]: ((~'LE'(f(suc(B_10)),s('0'))|'E'('0',f(suc(B_10))))|'LE'(f(B_10),'0'))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f50])).
% 66.58/8.92 fof(f189,plain,(
% 66.58/8.92 ![LE,X0,E]: (~'LE'(f(suc(X0)),s('0'))|'E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f188])).
% 66.58/8.92 fof(f192,plain,(
% 66.58/8.92 ![B_11]: ((![A_1]: ((![B_12]: (((![B_13]: ((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(B_11))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f52])).
% 66.58/8.92 fof(f193,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f192])).
% 66.58/8.92 fof(f196,plain,(
% 66.58/8.92 ![B_10]: ((~'LE'(f(B_10),s('0'))|'E'('0',f(B_10)))|'LE'(f(B_10),'0'))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f54])).
% 66.58/8.92 fof(f197,plain,(
% 66.58/8.92 ![LE,X0,E]: (~'LE'(f(X0),s('0'))|'E'('0',f(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f196])).
% 66.58/8.92 fof(f200,plain,(
% 66.58/8.92 ![B_11,B_12]: (((![B_13]: ((((((![A_1]: (((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~'E'('0',f(suc(suc(suc(B_11))))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'(f(B_11),f(suc(suc(B_11)))))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12)))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f56])).
% 66.58/8.92 fof(f201,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X3),f(suc(suc(X3))))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2)))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f200])).
% 66.58/8.92 fof(f206,plain,(
% 66.58/8.92 ![B_10]: ((~'LE'(f(suc(suc(suc(B_10)))),s('0'))|'E'('0',f(suc(suc(suc(B_10))))))|'LE'(f(B_10),'0'))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f59])).
% 66.58/8.92 fof(f207,plain,(
% 66.58/8.92 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(X0)))),s('0'))|'E'('0',f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f206])).
% 66.58/8.92 fof(f208,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(suc(B_12))))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f60])).
% 66.58/8.92 fof(f209,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f208])).
% 66.58/8.92 fof(f212,plain,(
% 66.58/8.92 ![A_1]: ((![B_11,B_12]: (((![B_13]: ((((((((((((((((((((((~'E'('0',f(suc(B_11)))|~'E'('0',f(suc(suc(suc(B_11))))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'(f(B_11),f(suc(suc(B_11)))))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(suc(A_1)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f62])).
% 66.58/8.92 fof(f213,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f212])).
% 66.58/8.92 fof(f214,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(B_11)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f63])).
% 66.58/8.92 fof(f215,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f214])).
% 66.58/8.92 fof(f220,plain,(
% 66.58/8.92 ![B_11]: ((![B_12]: (((![B_13]: ((((((![A_1]: (((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(B_11))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_13),f(suc(suc(B_13)))))|~'E'(f(B_12),f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_11))))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(suc(B_13))))))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13)))))|~'E'('0',f(suc(suc(suc(B_12))))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(B_11),f(suc(B_11))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f66])).
% 66.58/8.92 fof(f221,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X3),f(suc(suc(X3))))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f220])).
% 66.58/8.92 fof(f224,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(suc(B_12))))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f68])).
% 66.58/8.92 fof(f225,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f224])).
% 66.58/8.92 fof(f232,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![A_1]: ((![B_11]: ((((((((((((((((((~'E'('0',f(suc(B_11)))|~'E'('0',f(suc(suc(suc(B_11))))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'(f(B_11),f(suc(suc(B_11)))))|~'E'('0',f(suc(B_12))))|~'E'(f(B_12),f(suc(B_12))))|~'E'('0',f(suc(suc(B_12)))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_12),f(suc(suc(B_12))))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f72])).
% 66.58/8.92 fof(f233,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f232])).
% 66.58/8.92 fof(f236,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f74])).
% 66.58/8.92 fof(f237,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f236])).
% 66.58/8.92 fof(f238,plain,(
% 66.58/8.92 ![B_10]: ((~'LE'(f(suc(suc(B_10))),s('0'))|'E'('0',f(suc(suc(B_10)))))|'LE'(f(B_10),'0'))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f75])).
% 66.58/8.92 fof(f239,plain,(
% 66.58/8.92 ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s('0'))|'E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f238])).
% 66.58/8.92 fof(f248,plain,(
% 66.58/8.92 ![A_1]: ((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(A_1),f(suc(A_1))))|iLEQ(suc(A_1),suc(A_1)))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f80])).
% 66.58/8.92 fof(f249,plain,(
% 66.58/8.92 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f248])).
% 66.58/8.92 fof(f254,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![A_1]: ((![B_11]: ((((((((((((((((~'E'('0',f(suc(B_11)))|~'E'('0',f(suc(suc(suc(B_11))))))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'(f(B_11),f(suc(suc(B_11)))))|~'E'('0',f(suc(B_12))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~'E'('0',f(suc(suc(B_13)))))|~'E'(f(B_13),f(suc(B_13))))|~iLEQ(suc(B_11),suc(B_12))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(suc(B_13)))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f83])).
% 66.58/8.92 fof(f255,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f254])).
% 66.58/8.92 fof(f256,plain,(
% 66.58/8.92 ![A_1]: (((~'E'('0',f(A_1))|~'E'('0',f(suc(A_1))))|'E'(f(A_1),f(suc(A_1))))|iLEQ(suc(A_1),suc(A_1)))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f84])).
% 66.58/8.92 fof(f257,plain,(
% 66.58/8.92 ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f256])).
% 66.58/8.92 fof(f262,plain,(
% 66.58/8.92 ![B_13]: ((![B_12]: ((![B_11]: ((![A_1]: (((((((((((((~'E'('0',f(suc(B_11)))|~iLEQ(suc(B_12),suc(B_13)))|~'E'('0',f(suc(suc(B_11)))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(B_11)))|~'E'('0',f(A_1)))|~'E'('0',f(B_13)))|~'E'('0',f(suc(B_12))))|~'E'(f(B_11),f(suc(B_11))))|~iLEQ(suc(A_1),suc(B_11)))|~'E'('0',f(suc(B_13))))|~'E'('0',f(B_12)))|~iLEQ(suc(B_11),suc(B_12)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_11),f(suc(suc(B_11))))))|'E'(f(B_12),f(suc(B_12)))))|'E'(f(B_13),f(suc(B_13))))),
% 66.58/8.92 inference(miniscoping,[status(thm)],[f87])).
% 66.58/8.92 fof(f263,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(cnf_transformation,[status(thm)],[f262])).
% 66.58/8.92 fof(f270,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X1),suc(X1))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(factoring,[status(thm)],[f104])).
% 66.58/8.92 fof(f271,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~iLEQ(suc(X1),suc(X1))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(duplicate_literals_removal,[status(thm)],[f270])).
% 66.58/8.92 fof(f272,plain,(
% 66.58/8.92 ![E,X0,LE]: ('E'('0',f(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f197,f149])).
% 66.58/8.92 fof(f273,plain,(
% 66.58/8.92 ![E]: ('E'('0',f(z)))),
% 66.58/8.92 inference(resolution,[status(thm)],[f272,f131])).
% 66.58/8.92 fof(f274,plain,(
% 66.58/8.92 ![E,X0,LE]: ('E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f189,f149])).
% 66.58/8.92 fof(f285,plain,(
% 66.58/8.92 ![E,X0,LE]: ('E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f239,f149])).
% 66.58/8.92 fof(f300,plain,(
% 66.58/8.92 ![E,X0,LE]: ('E'('0',f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f207,f149])).
% 66.58/8.92 fof(f331,plain,(
% 66.58/8.92 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0)))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f249,f257])).
% 66.58/8.92 fof(f332,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f331,f300])).
% 66.58/8.92 fof(f335,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f332,f272])).
% 66.58/8.92 fof(f362,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f335,f274])).
% 66.58/8.92 fof(f364,plain,(
% 66.58/8.92 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f331,f365])).
% 66.58/8.92 fof(f365,plain,(
% 66.58/8.92 ![E,X0]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0)))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f130,f257])).
% 66.58/8.92 fof(f367,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f365,f285])).
% 66.58/8.92 fof(f370,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f367,f272])).
% 66.58/8.92 fof(f372,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f362,f373])).
% 66.58/8.92 fof(f373,plain,(
% 66.58/8.92 ![E,X0,LE]: ('E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f370,f274])).
% 66.58/8.92 fof(f376,plain,(
% 66.58/8.92 ![X0,LE]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f372,f285])).
% 66.58/8.92 fof(f395,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f106,f376])).
% 66.58/8.92 fof(f396,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(duplicate_literals_removal,[status(thm)],[f395])).
% 66.58/8.92 fof(f397,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f396,f272])).
% 66.58/8.92 fof(f409,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f271,f364])).
% 66.58/8.92 fof(f416,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f173,f100])).
% 66.58/8.92 fof(f426,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X1),suc(X1))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(factoring,[status(thm)],[f416])).
% 66.58/8.92 fof(f439,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X1),suc(X1))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(duplicate_literals_removal,[status(thm)],[f426])).
% 66.58/8.92 fof(f440,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f439,f364])).
% 66.58/8.92 fof(f446,definition,(
% 66.58/8.92 sQ0_spl <=> (iLEQ(suc(z),suc(z)))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f447,plain,(
% 66.58/8.92 iLEQ(suc(z),suc(z))|~sQ0_spl),
% 66.58/8.92 inference(component_clause,[status(thm)],[f446])).
% 66.58/8.92 fof(f448,plain,(
% 66.58/8.92 ~iLEQ(suc(z),suc(z))|sQ0_spl),
% 66.58/8.92 inference(component_clause,[status(thm)],[f446])).
% 66.58/8.92 fof(f491,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f108,f114])).
% 66.58/8.92 fof(f492,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f96,f114])).
% 66.58/8.92 fof(f518,plain,(
% 66.58/8.92 ![E,X0,X1]: (~'E'('0',f(suc(z)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(z)))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(z))|~'E'('0',f(z))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(z),f(suc(z)))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~iLEQ(suc(z),suc(X0))|'E'(f(z),f(suc(suc(z))))|'E'(f(z),f(suc(suc(z))))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|~sQ0_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f447,f114])).
% 66.58/8.92 fof(f521,definition,(
% 66.58/8.92 ![E]: (sQ2_spl <=> ('E'('0',f(suc(z)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f523,plain,(
% 66.58/8.92 ![E]: (~'E'('0',f(suc(z)))|sQ2_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f521])).
% 66.58/8.92 fof(f524,definition,(
% 66.58/8.92 ![X0,X1,E]: (sQ3_spl <=> (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f525,plain,(
% 66.58/8.92 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|~sQ3_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f524])).
% 66.58/8.92 fof(f527,definition,(
% 66.58/8.92 ![E]: (sQ4_spl <=> ('E'('0',f(suc(suc(z))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f528,plain,(
% 66.58/8.92 ![E]: ('E'('0',f(suc(suc(z))))|~sQ4_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f527])).
% 66.58/8.92 fof(f529,plain,(
% 66.58/8.92 ![E]: (~'E'('0',f(suc(suc(z))))|sQ4_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f527])).
% 66.58/8.92 fof(f530,definition,(
% 66.58/8.92 ![E]: (sQ5_spl <=> ('E'('0',f(z))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f532,plain,(
% 66.58/8.92 ![E]: (~'E'('0',f(z))|sQ5_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f530])).
% 66.58/8.92 fof(f533,definition,(
% 66.58/8.92 ![E]: (sQ6_spl <=> ('E'(f(z),f(suc(z)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f536,definition,(
% 66.58/8.92 ![E]: (sQ7_spl <=> ('E'(f(z),f(suc(suc(z))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f537,plain,(
% 66.58/8.92 ![E]: ('E'(f(z),f(suc(suc(z))))|~sQ7_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f536])).
% 66.58/8.92 fof(f539,plain,(
% 66.58/8.92 ~sQ2_spl|sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|sQ7_spl|~sQ0_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f518,f521,f524,f527,f530,f533,f536,f446])).
% 66.58/8.92 fof(f541,definition,(
% 66.58/8.92 ![X0,X1,E]: (sQ8_spl <=> (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f542,plain,(
% 66.58/8.92 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|~sQ8_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f541])).
% 66.58/8.92 fof(f545,plain,(
% 66.58/8.92 $false|sQ5_spl),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f532,f273])).
% 66.58/8.92 fof(f546,plain,(
% 66.58/8.92 sQ5_spl),
% 66.58/8.92 inference(contradiction_clause,[status(thm)],[f545])).
% 66.58/8.92 fof(f553,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2)))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f201,f416])).
% 66.58/8.92 fof(f554,plain,(
% 66.58/8.92 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f553,f300])).
% 66.58/8.92 fof(f555,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f553,f300])).
% 66.58/8.92 fof(f557,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'LE'(f(suc(X1)),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f553,f285])).
% 66.58/8.92 fof(f570,plain,(
% 66.58/8.92 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(duplicate_literals_removal,[status(thm)],[f554])).
% 66.58/8.92 fof(f571,plain,(
% 66.58/8.92 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f570,f272])).
% 66.58/8.92 fof(f572,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f555,f272])).
% 66.58/8.92 fof(f575,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X3),f(suc(suc(X3))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X0),suc(X3))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X3),suc(X1))|'LE'(f(suc(X3)),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f557,f272])).
% 66.58/8.92 fof(f614,plain,(
% 66.58/8.92 ![X0,X1,E,X2,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~iLEQ(suc(X2),suc(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f397,f274])).
% 66.58/8.92 fof(f621,plain,(
% 66.58/8.92 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f614,f376])).
% 66.58/8.92 fof(f625,definition,(
% 66.58/8.92 ![LE]: (sQ10_spl <=> ('LE'(f(z),'0')))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f626,plain,(
% 66.58/8.92 ![LE]: ('LE'(f(z),'0')|~sQ10_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f625])).
% 66.58/8.92 fof(f639,plain,(
% 66.58/8.92 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(duplicate_literals_removal,[status(thm)],[f621])).
% 66.58/8.92 fof(f640,plain,(
% 66.58/8.92 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f639,f272])).
% 66.58/8.92 fof(f641,plain,(
% 66.58/8.92 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f640,f274])).
% 66.58/8.92 fof(f642,plain,(
% 66.58/8.92 ![E,LE]: (~'E'('0',f(z))|~'E'('0',f(suc(z)))|'E'(f(z),f(suc(z)))|'E'(f(z),f(suc(z)))|'LE'(f(z),'0')|~sQ0_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f641,f447])).
% 66.58/8.92 fof(f648,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f641,f376])).
% 66.58/8.92 fof(f649,plain,(
% 66.58/8.92 ~sQ5_spl|~sQ2_spl|sQ6_spl|sQ10_spl|~sQ0_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f642,f530,f521,f533,f625,f446])).
% 66.58/8.92 fof(f660,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(duplicate_literals_removal,[status(thm)],[f648])).
% 66.58/8.92 fof(f661,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f660,f272])).
% 66.58/8.92 fof(f662,plain,(
% 66.58/8.92 ![E,X0,LE]: ('E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f661,f274])).
% 66.58/8.92 fof(f663,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f118,f106])).
% 66.58/8.92 fof(f722,plain,(
% 66.58/8.92 ![LE]: ('LE'(f(z),'0')|sQ2_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f523,f274])).
% 66.58/8.92 fof(f723,plain,(
% 66.58/8.92 $false|sQ2_spl),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f722,f131])).
% 66.58/8.92 fof(f724,plain,(
% 66.58/8.92 sQ2_spl),
% 66.58/8.92 inference(contradiction_clause,[status(thm)],[f723])).
% 66.58/8.92 fof(f725,plain,(
% 66.58/8.92 $false|~sQ10_spl),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f626,f131])).
% 66.58/8.92 fof(f726,plain,(
% 66.58/8.92 ~sQ10_spl),
% 66.58/8.92 inference(contradiction_clause,[status(thm)],[f725])).
% 66.58/8.92 fof(f774,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f126,f663])).
% 66.58/8.92 fof(f819,definition,(
% 66.58/8.92 ![X0,X1,E]: (sQ15_spl <=> (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f820,plain,(
% 66.58/8.92 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1))))|~sQ15_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f819])).
% 66.58/8.92 fof(f829,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f213,f409])).
% 66.58/8.92 fof(f892,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f137,f663])).
% 66.58/8.92 fof(f893,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f892,f300])).
% 66.58/8.92 fof(f896,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f893,f272])).
% 66.58/8.92 fof(f900,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f139,f774])).
% 66.58/8.92 fof(f931,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f143,f900])).
% 66.58/8.92 fof(f1002,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f147,f106])).
% 66.58/8.92 fof(f1010,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f151,f931])).
% 66.58/8.92 fof(f1024,plain,(
% 66.58/8.92 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f571,f285])).
% 66.58/8.92 fof(f1025,plain,(
% 66.58/8.92 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X1))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X0),'0')|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f1024,f300])).
% 66.58/8.92 fof(f1028,plain,(
% 66.58/8.92 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X0),'0')|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1025,f272])).
% 66.58/8.92 fof(f1031,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2)))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f553,f1032])).
% 66.58/8.92 fof(f1032,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f221,f1010])).
% 66.58/8.92 fof(f1058,plain,(
% 66.58/8.92 ![X0,E,X1,LE]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X0),'0')|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1028,f274])).
% 66.58/8.92 fof(f1059,plain,(
% 66.58/8.92 ![X0,E,LE]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(z)))|~'E'('0',f(suc(suc(z))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(z),f(suc(z)))|~iLEQ(suc(z),suc(X0))|'LE'(f(X0),'0')|'LE'(f(z),'0')|~sQ7_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1058,f537])).
% 66.58/8.92 fof(f1061,definition,(
% 66.58/8.92 ![X0,E,LE]: (sQ16_spl <=> (~iLEQ(suc(X0),suc(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(z),suc(X0))|'LE'(f(X0),'0')))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f1062,plain,(
% 66.58/8.92 ![X0,E,LE]: (~iLEQ(suc(X0),suc(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(z),suc(X0))|'LE'(f(X0),'0')|~sQ16_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f1061])).
% 66.58/8.92 fof(f1064,plain,(
% 66.58/8.92 sQ16_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|sQ10_spl|~sQ7_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f1059,f1061,f521,f527,f533,f625,f536])).
% 66.58/8.92 fof(f1118,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f157,f128])).
% 66.58/8.92 fof(f1144,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f159,f774])).
% 66.58/8.92 fof(f1145,plain,(
% 66.58/8.92 ![E,X0,X1]: (~'E'('0',f(suc(z)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(z)))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(z))|~'E'('0',f(z))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(z),f(suc(suc(z))))|'E'(f(z),f(suc(suc(z))))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1))))|~sQ0_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1144,f447])).
% 66.58/8.92 fof(f1152,plain,(
% 66.58/8.92 ~sQ2_spl|sQ15_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|sQ7_spl|~sQ0_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f1145,f521,f819,f527,f530,f533,f536,f446])).
% 66.58/8.92 fof(f1172,plain,(
% 66.58/8.92 ![LE]: ('LE'(f(z),'0')|sQ0_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f448,f376])).
% 66.58/8.92 fof(f1173,plain,(
% 66.58/8.92 sQ10_spl|sQ0_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f1172,f625,f446])).
% 66.58/8.92 fof(f1244,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f1118,f1245])).
% 66.58/8.92 fof(f1245,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f165,f1144])).
% 66.58/8.92 fof(f1280,plain,(
% 66.58/8.92 ![LE]: ('LE'(f(z),'0')|sQ4_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f529,f285])).
% 66.58/8.92 fof(f1282,plain,(
% 66.58/8.92 sQ10_spl|sQ4_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f1280,f625,f527])).
% 66.58/8.92 fof(f1283,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(z),suc(X0))|'LE'(f(X0),'0')|~sQ16_spl)),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1062,f376])).
% 66.58/8.92 fof(f1415,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X2),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f896,f274])).
% 66.58/8.92 fof(f1416,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(X2)))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X1))|~'E'(f(z),f(suc(z)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(z),'0')|~sQ4_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1415,f528])).
% 66.58/8.92 fof(f1420,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ20_spl <=> (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(X2)))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f1423,plain,(
% 66.58/8.92 sQ20_spl|~sQ6_spl|sQ10_spl|~sQ4_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f1416,f1420,f533,f625,f527])).
% 66.58/8.92 fof(f1459,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f185,f663])).
% 66.58/8.92 fof(f1495,definition,(
% 66.58/8.92 ![E]: (sQ25_spl <=> ('E'('0',f(suc(suc(suc(z)))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f1496,plain,(
% 66.58/8.92 ![E]: ('E'('0',f(suc(suc(suc(z)))))|~sQ25_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f1495])).
% 66.58/8.92 fof(f1497,plain,(
% 66.58/8.92 ![E]: (~'E'('0',f(suc(suc(suc(z)))))|sQ25_spl)),
% 66.58/8.92 inference(component_clause,[status(thm)],[f1495])).
% 66.58/8.92 fof(f1630,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1))))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f1032,f1631])).
% 66.58/8.92 fof(f1631,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(X0))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f193,f1459])).
% 66.58/8.92 fof(f1777,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f1002,f1781])).
% 66.58/8.92 fof(f1781,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f215,f106])).
% 66.58/8.92 fof(f1875,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ40_spl <=> (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(z),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f1909,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(X3),'0'))),
% 66.58/8.92 inference(resolution,[status(thm)],[f1777,f300])).
% 66.58/8.92 fof(f1913,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(X3),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1909,f272])).
% 66.58/8.92 fof(f1926,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f225,f209])).
% 66.58/8.92 fof(f1927,plain,(
% 66.58/8.92 ![E,X0,X1]: (~'E'('0',f(suc(z)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(z)))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(z))|~'E'('0',f(z))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(z),f(suc(suc(z))))|'E'(f(z),f(suc(suc(z))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|~sQ0_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1926,f447])).
% 66.58/8.92 fof(f1935,plain,(
% 66.58/8.92 ~sQ2_spl|sQ8_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|sQ7_spl|~sQ0_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f1927,f521,f541,f527,f530,f533,f536,f446])).
% 66.58/8.92 fof(f2016,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(X3),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1913,f274])).
% 66.58/8.92 fof(f2017,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(z),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|'LE'(f(z),'0')|~sQ4_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f2016,f528])).
% 66.58/8.92 fof(f2021,plain,(
% 66.58/8.92 sQ40_spl|sQ10_spl|~sQ4_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2017,f1875,f625,f527])).
% 66.58/8.92 fof(f2067,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f233,f209])).
% 66.58/8.92 fof(f2084,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f237,f663])).
% 66.58/8.92 fof(f2110,plain,(
% 66.58/8.92 ![LE]: ('LE'(f(z),'0')|sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1497,f300])).
% 66.58/8.92 fof(f2113,plain,(
% 66.58/8.92 sQ10_spl|sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2110,f625,f1495])).
% 66.58/8.92 fof(f2116,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(z)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(X2)))|~'E'('0',f(z))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(z),f(suc(z)))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1496,f2067])).
% 66.58/8.92 fof(f2120,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(z))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(z)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(z))))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1496,f1630])).
% 66.58/8.92 fof(f2143,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(z))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(z)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(z))))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1496,f1031])).
% 66.58/8.92 fof(f2150,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(z))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(z)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(z))))|~'E'(f(z),f(suc(z)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f1496,f1245])).
% 66.58/8.92 fof(f2166,definition,(
% 66.58/8.92 ![E,X2]: (sQ46_spl <=> (~'E'('0',f(suc(X2)))|~'E'('0',f(X2))|~iLEQ(suc(X2),suc(z))|'E'(f(X2),f(suc(X2)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f2177,plain,(
% 66.58/8.92 ~sQ2_spl|sQ8_spl|~sQ4_spl|sQ46_spl|~sQ5_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2116,f521,f541,f527,f2166,f530,f533,f1495])).
% 66.58/8.92 fof(f2187,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ51_spl <=> (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(X1)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f2190,plain,(
% 66.58/8.92 sQ51_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2120,f2187,f530,f521,f527,f533,f1495])).
% 66.58/8.92 fof(f2255,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ66_spl <=> (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f2258,plain,(
% 66.58/8.92 sQ66_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2143,f2255,f530,f521,f527,f533,f1495])).
% 66.58/8.92 fof(f2274,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ70_spl <=> (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f2277,plain,(
% 66.58/8.92 sQ70_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2150,f2274,f530,f521,f527,f533,f1495])).
% 66.58/8.92 fof(f2296,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ75_spl <=> (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(suc(X2))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f2323,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3)))))),
% 66.58/8.92 inference(backward_subsumption_resolution,[status(thm)],[f829,f2324])).
% 66.58/8.92 fof(f2324,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f440,f409])).
% 66.58/8.92 fof(f2352,plain,(
% 66.58/8.92 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1))))|~sQ3_spl|~sQ15_spl)),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f820,f525])).
% 66.58/8.92 fof(f2373,plain,(
% 66.58/8.92 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|~sQ3_spl|~sQ15_spl|~sQ8_spl)),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f542,f2352])).
% 66.58/8.92 fof(f2374,plain,(
% 66.58/8.92 ![E]: (~'E'('0',f(z))|~'E'('0',f(suc(z)))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(z)))|~'E'('0',f(z))|~'E'('0',f(suc(suc(z))))|~'E'(f(z),f(suc(z)))|~iLEQ(suc(z),suc(z))|'E'(f(z),f(suc(suc(z))))|'E'(f(z),f(suc(suc(z))))|~sQ3_spl|~sQ15_spl|~sQ8_spl|~sQ0_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f2373,f447])).
% 66.58/8.92 fof(f2382,plain,(
% 66.58/8.92 ~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|~sQ0_spl|sQ7_spl|~sQ3_spl|~sQ15_spl|~sQ8_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2374,f530,f521,f527,f533,f446,f536,f524,f819,f541])).
% 66.58/8.92 fof(f2396,plain,(
% 66.58/8.92 ![E,X0,LE]: (~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(z),suc(X0))|'LE'(f(X0),'0')|~sQ16_spl)),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1283,f662])).
% 66.58/8.92 fof(f2516,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(z))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(z)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(suc(X2))))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f2323,f1496])).
% 66.58/8.92 fof(f2529,plain,(
% 66.58/8.92 sQ75_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2516,f2296,f530,f521,f527,f1495])).
% 66.58/8.92 fof(f2634,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f255,f2084])).
% 66.58/8.92 fof(f2635,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(z)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(X2)))|~'E'('0',f(z))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X0)))|~'E'(f(z),f(suc(z)))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(z),suc(X0))|'E'(f(X2),f(suc(X2)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1))))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f2634,f1496])).
% 66.58/8.92 fof(f2639,plain,(
% 66.58/8.92 ~sQ2_spl|sQ15_spl|~sQ4_spl|sQ46_spl|~sQ5_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2635,f521,f819,f527,f2166,f530,f533,f1495])).
% 66.58/8.92 fof(f2680,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'LE'(f(X1),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f572,f285])).
% 66.58/8.92 fof(f2682,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(z))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(z)))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(z))))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'LE'(f(X1),'0')|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f2680,f1496])).
% 66.58/8.92 fof(f2698,definition,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (sQ91_spl <=> (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(z))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X2)))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(X2)))))|~iLEQ(suc(X1),suc(X2))|'LE'(f(X1),'0')))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f2701,plain,(
% 66.58/8.92 sQ91_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f2682,f2698,f530,f521,f527,f533,f1495])).
% 66.58/8.92 fof(f2798,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(X3)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f263,f106])).
% 66.58/8.92 fof(f3036,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X2)))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X2))|~iLEQ(suc(X1),suc(X2))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f491,f2798])).
% 66.58/8.92 fof(f3037,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(z)))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(X0))|~'E'('0',f(z))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(z),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f3036,f1496])).
% 66.58/8.92 fof(f3041,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ121_spl <=> (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(z),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2)))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f3044,plain,(
% 66.58/8.92 sQ121_spl|~sQ2_spl|~sQ4_spl|~sQ5_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f3037,f3041,f521,f527,f530,f1495])).
% 66.58/8.92 fof(f3131,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X3),f(suc(suc(X3))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X0),suc(X3))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X3),suc(X1))|'LE'(f(suc(X3)),'0'))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f575,f274])).
% 66.58/8.92 fof(f3133,plain,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~'E'('0',f(X0))|~'E'('0',f(z))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X2))|~'E'('0',f(suc(z)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(z))))|~'E'(f(z),f(suc(z)))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X1))|'LE'(f(suc(X2)),'0')|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f3131,f1496])).
% 66.58/8.92 fof(f3149,definition,(
% 66.58/8.92 ![E,X0,X1,X2,LE]: (sQ127_spl <=> (~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~'E'('0',f(X0))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X0),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X2),suc(X1))|'LE'(f(suc(X2)),'0')))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f3152,plain,(
% 66.58/8.92 sQ127_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f3133,f3149,f530,f521,f527,f533,f1495])).
% 66.58/8.92 fof(f3549,plain,(
% 66.58/8.92 ![E,X0,X1,X2,X3]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(X0))|~'E'('0',f(X3))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 66.58/8.92 inference(forward_subsumption_resolution,[status(thm)],[f1244,f492])).
% 66.58/8.92 fof(f3551,plain,(
% 66.58/8.92 ![E,X0,X1,X2]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(z))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(z)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(z))))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X0),f(suc(suc(X0))))|~sQ25_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f3549,f1496])).
% 66.58/8.92 fof(f3564,definition,(
% 66.58/8.92 ![E,X0,X1,X2]: (sQ154_spl <=> (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(z))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X0),suc(X1))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X0),f(suc(suc(X0))))))),
% 66.58/8.92 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 66.58/8.92 fof(f3567,plain,(
% 66.58/8.92 sQ154_spl|~sQ5_spl|~sQ2_spl|~sQ4_spl|~sQ25_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f3551,f3564,f530,f521,f527,f1495])).
% 66.58/8.92 fof(f3637,plain,(
% 66.58/8.92 ![LE]: (~iLEQ(suc(z),suc(z))|'LE'(f(z),'0')|~sQ16_spl|~sQ7_spl)),
% 66.58/8.92 inference(resolution,[status(thm)],[f2396,f537])).
% 66.58/8.92 fof(f3640,plain,(
% 66.58/8.92 ~sQ0_spl|sQ10_spl|~sQ16_spl|~sQ7_spl),
% 66.58/8.92 inference(split_clause,[status(thm)],[f3637,f446,f625,f1061,f536])).
% 66.58/8.92 fof(f3642,plain,(
% 66.58/8.92 $false),
% 66.58/8.92 inference(sat_refutation,[status(thm)],[f539,f546,f649,f724,f726,f1064,f1152,f1173,f1282,f1423,f1935,f2021,f2113,f2177,f2190,f2258,f2277,f2382,f2529,f2639,f2701,f3044,f3152,f3567,f3640])).
% 66.58/8.92 % SZS output end CNFRefutation for theBenchmark.p
% 66.58/8.93 % Elapsed time: 8.568329 seconds
% 66.58/8.93 % CPU time: 67.687581 seconds
% 66.58/8.93 % Total memory used: 58.440 MB
% 66.58/8.93 % Net memory used: 53.020 MB
%------------------------------------------------------------------------------