%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO659-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 0.15s 10.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO659-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/10.39 % Computer : n009.cluster.edu
% 0.11/10.39 % Model : x86_64 x86_64
% 0.11/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.39 % Memory : 8046.5625MB
% 0.11/10.39 % OS : Linux 6.8.0-71-generic
% 0.11/10.39 % CPULimit : 300
% 0.11/10.39 % WCLimit : 300
% 0.11/10.39 % DateTime : Mon Sep 21 12:08:23 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.15/10.40 % Drodi V4.1.1
% 0.15/10.70 % Refutation found
% 0.15/10.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/10.70 % SZS output start CNFRefutation for theBenchmark
% 0.15/10.70 fof(f2,axiom,(
% 0.15/10.70 (![E,A_1]: (( ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(A_1)))| 'E'(f(A_1),f(suc(A_1)))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f3,axiom,(
% 0.15/10.70 (![LE,B_5,E]: (( ~ 'LE'(f(suc(suc(suc(B_5)))),s('0'))| 'E'('0',f(suc(suc(suc(B_5)))))| 'LE'(f(B_5),'0') ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f4,axiom,(
% 0.15/10.70 (![LE,B_2,E]: (( ~ 'LE'(f(suc(suc(B_2))),s(s('0')))| 'E'(s('0'),f(suc(suc(B_2))))| 'LE'(f(B_2),s('0')) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f7,axiom,(
% 0.15/10.70 (![E,A_2]: (( ~ 'E'('0',f(suc(suc(A_2))))| ~ 'E'('0',f(suc(A_2)))| ~ 'E'(f(A_2),f(suc(A_2)))| ~ 'E'('0',f(A_2))| 'E'(f(A_2),f(suc(suc(A_2))))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f8,axiom,(
% 0.15/10.70 (![E,A_1]: (( ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))| 'E'(f(A_1),f(suc(suc(suc(A_1)))))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f10,axiom,(
% 0.15/10.70 (![LE,B_2,E]: (( ~ 'LE'(f(B_2),s(s('0')))| 'E'(s('0'),f(B_2))| 'LE'(f(B_2),s('0')) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f12,axiom,(
% 0.15/10.70 (![LE,B_2,E]: (( ~ 'LE'(f(suc(suc(suc(suc(B_2))))),s(s('0')))| 'E'(s('0'),f(suc(suc(suc(suc(B_2))))))| 'LE'(f(B_2),s('0')) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f13,axiom,(
% 0.15/10.70 (![A_1,B_3,E]: (( ~ iLEQ(suc(A_1),suc(B_3))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(B_3)))| ~ 'E'(s('0'),f(B_3))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_3),f(suc(B_3))) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f14,axiom,(
% 0.15/10.70 (![A_1,B_3,E]: (( ~ iLEQ(suc(A_1),suc(B_3))| ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(suc(B_3))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(B_3)))| ~ 'E'(s('0'),f(B_3))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_3),f(suc(B_3)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))| 'E'(f(A_1),f(suc(suc(suc(A_1)))))| 'E'(f(B_3),f(suc(suc(B_3)))) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f15,axiom,(
% 0.15/10.70 (![A_1,B_3,E]: (( ~ iLEQ(suc(A_1),suc(B_3))| ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(suc(B_3))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))| ~ 'E'(s('0'),f(suc(B_3)))| ~ 'E'(s('0'),f(B_3))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_3),f(suc(B_3)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))| ~ 'E'(f(B_3),f(suc(suc(B_3))))| 'E'(f(A_1),f(suc(suc(suc(A_1)))))| 'E'(f(B_3),f(suc(suc(suc(B_3))))) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f18,axiom,(
% 0.15/10.70 (![E,A_2]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(suc(A_2))))| ~ 'E'('0',f(A_2))| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))| ~ 'E'('0',f(suc(suc(suc(A_2)))))| ~ 'E'(f(A_2),f(suc(A_2)))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f19,axiom,(
% 0.15/10.70 (![LE,B_5,E]: (( ~ 'LE'(f(suc(B_5)),s('0'))| 'E'('0',f(suc(B_5)))| 'LE'(f(B_5),'0') ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f20,axiom,(
% 0.15/10.70 (![LE,B_5,E]: (( ~ 'LE'(f(B_5),s('0'))| 'E'('0',f(B_5))| 'LE'(f(B_5),'0') ) ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f21,axiom,(
% 0.15/10.70 (![LE]: (~ 'LE'(f(z),'0') ))),
% 0.15/10.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.70 fof(f22,axiom,(
% 0.15/10.70 (![E,A_2,B_6]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(B_6))))| ~ 'E'('0',f(A_2))| ~ iLEQ(suc(A_2),suc(B_6))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_2),f(suc(A_2)))| 'E'(f(B_6),f(suc(suc(suc(B_6))))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f23,axiom,(
% 0.15/10.71 (![E,A_1]: (( ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s('0'),f(A_1))| 'E'(f(A_1),f(suc(suc(A_1))))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f24,axiom,(
% 0.15/10.71 (![LE,A]: ('LE'(f(A),s(s('0'))) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f26,axiom,(
% 0.15/10.71 (![E,A_1]: (( ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f33,axiom,(
% 0.15/10.71 (![E,A_2,B_6]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(A_2))| ~ iLEQ(suc(A_2),suc(B_6))| ~ 'E'('0',f(B_6))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_2),f(suc(A_2)))| 'E'(f(B_6),f(suc(B_6))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f34,axiom,(
% 0.15/10.71 (![A_1,B_3,E]: (( ~ iLEQ(suc(A_1),suc(B_3))| ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(suc(B_3))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(B_3)))| ~ 'E'(s('0'),f(B_3))| ~ 'E'(f(B_3),f(suc(B_3)))| ~ 'E'(f(A_1),f(suc(A_1)))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_3),f(suc(suc(B_3)))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f35,axiom,(
% 0.15/10.71 (![E,A_2,B_6]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(suc(A_2))))| ~ 'E'('0',f(A_2))| ~ iLEQ(suc(A_2),suc(B_6))| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))| ~ 'E'('0',f(suc(suc(suc(A_2)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'(f(A_2),f(suc(A_2)))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f36,axiom,(
% 0.15/10.71 (![E,A_2,B_6]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(A_2))))| ~ 'E'('0',f(A_2))| ~ iLEQ(suc(A_2),suc(B_6))| ~ 'E'('0',f(B_6))| ~ 'E'(f(A_2),f(suc(A_2)))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_2),f(suc(suc(A_2))))| 'E'(f(B_6),f(suc(suc(B_6)))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f37,axiom,(
% 0.15/10.71 (![E,A_2,B_6]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(suc(A_2))))| ~ 'E'('0',f(A_2))| ~ iLEQ(suc(A_2),suc(B_6))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'('0',f(suc(suc(suc(A_2)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'(f(A_2),f(suc(A_2)))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_2),f(suc(suc(suc(A_2)))))| 'E'(f(B_6),f(suc(suc(suc(B_6))))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f38,axiom,(
% 0.15/10.71 (![LE,B_2,E]: (( ~ 'LE'(f(suc(suc(suc(B_2)))),s(s('0')))| 'E'(s('0'),f(suc(suc(suc(B_2)))))| 'LE'(f(B_2),s('0')) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f39,axiom,(
% 0.15/10.71 (![LE,B_5,E]: (( ~ 'LE'(f(suc(suc(suc(suc(B_5))))),s('0'))| 'E'('0',f(suc(suc(suc(suc(B_5))))))| 'LE'(f(B_5),'0') ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f40,axiom,(
% 0.15/10.71 (![A_1,B_3,E]: (( ~ iLEQ(suc(A_1),suc(B_3))| ~ 'E'(s('0'),f(suc(suc(A_1))))| ~ 'E'(s('0'),f(suc(suc(suc(suc(B_3))))))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(suc(B_3))))| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))| ~ 'E'(s('0'),f(suc(B_3)))| ~ 'E'(s('0'),f(B_3))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ 'E'(f(B_3),f(suc(B_3)))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'(f(B_3),f(suc(suc(suc(B_3)))))| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))| ~ 'E'(f(B_3),f(suc(suc(B_3)))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f41,axiom,(
% 0.15/10.71 (![E,A_2]: (( ~ 'E'('0',f(A_2))| ~ 'E'('0',f(suc(A_2)))| 'E'(f(A_2),f(suc(A_2)))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f42,axiom,(
% 0.15/10.71 (![LE,B_2,E]: (( ~ 'LE'(f(suc(B_2)),s(s('0')))| 'E'(s('0'),f(suc(B_2)))| 'LE'(f(B_2),s('0')) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f43,axiom,(
% 0.15/10.71 (![E,A_2]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(A_2))))| ~ 'E'(f(A_2),f(suc(suc(A_2))))| ~ 'E'('0',f(A_2))| ~ 'E'('0',f(suc(suc(suc(A_2)))))| ~ 'E'(f(A_2),f(suc(A_2)))| 'E'(f(A_2),f(suc(suc(suc(A_2)))))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f46,axiom,(
% 0.15/10.71 (![A_1,B_3,E]: (( ~ iLEQ(suc(A_1),suc(B_3))| ~ 'E'(s('0'),f(A_1))| ~ 'E'(s('0'),f(suc(suc(B_3))))| ~ 'E'(s('0'),f(suc(A_1)))| ~ 'E'(s('0'),f(suc(B_3)))| ~ 'E'(s('0'),f(B_3))| ~ 'E'(f(B_3),f(suc(B_3)))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_3),f(suc(suc(B_3)))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f48,axiom,(
% 0.15/10.71 (![E,A_2,B_6]: (( ~ 'E'('0',f(suc(A_2)))| ~ 'E'('0',f(suc(suc(B_6))))| ~ 'E'('0',f(A_2))| ~ iLEQ(suc(A_2),suc(B_6))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_2),f(suc(A_2)))| 'E'(f(B_6),f(suc(suc(B_6)))) ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f51,axiom,(
% 0.15/10.71 (![LE,B_5,E]: (( ~ 'LE'(f(suc(suc(B_5))),s('0'))| 'E'('0',f(suc(suc(B_5))))| 'LE'(f(B_5),'0') ) ))),
% 0.15/10.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.71 fof(f55,plain,(
% 0.15/10.71 ![A_1]: (((~'E'(s('0'),f(A_1))|~'E'(s('0'),f(suc(A_1))))|'E'(f(A_1),f(suc(A_1))))|iLEQ(suc(A_1),suc(A_1)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f2])).
% 0.15/10.71 fof(f56,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f55])).
% 0.15/10.71 fof(f57,plain,(
% 0.15/10.71 ![B_5]: ((~'LE'(f(suc(suc(suc(B_5)))),s('0'))|'E'('0',f(suc(suc(suc(B_5))))))|'LE'(f(B_5),'0'))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f3])).
% 0.15/10.71 fof(f58,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(X0)))),s('0'))|'E'('0',f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/10.71 fof(f59,plain,(
% 0.15/10.71 ![B_2]: ((~'LE'(f(suc(suc(B_2))),s(s('0')))|'E'(s('0'),f(suc(suc(B_2)))))|'LE'(f(B_2),s('0')))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f4])).
% 0.15/10.71 fof(f60,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s(s('0')))|'E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f59])).
% 0.15/10.71 fof(f65,plain,(
% 0.15/10.71 ![A_2]: (((((~'E'('0',f(suc(suc(A_2))))|~'E'('0',f(suc(A_2))))|~'E'(f(A_2),f(suc(A_2))))|~'E'('0',f(A_2)))|'E'(f(A_2),f(suc(suc(A_2)))))|iLEQ(suc(A_2),suc(A_2)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f7])).
% 0.15/10.71 fof(f66,plain,(
% 0.15/10.71 ![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)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f65])).
% 0.15/10.71 fof(f67,plain,(
% 0.15/10.71 ![A_1]: (((((((~'E'(s('0'),f(suc(suc(A_1))))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(A_1))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(A_1))))))|'E'(f(A_1),f(suc(suc(suc(A_1))))))|iLEQ(suc(A_1),suc(A_1)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f8])).
% 0.15/10.71 fof(f68,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f67])).
% 0.15/10.71 fof(f71,plain,(
% 0.15/10.71 ![B_2]: ((~'LE'(f(B_2),s(s('0')))|'E'(s('0'),f(B_2)))|'LE'(f(B_2),s('0')))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f10])).
% 0.15/10.71 fof(f72,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(X0),s(s('0')))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f71])).
% 0.15/10.71 fof(f75,plain,(
% 0.15/10.71 ![B_2]: ((~'LE'(f(suc(suc(suc(suc(B_2))))),s(s('0')))|'E'(s('0'),f(suc(suc(suc(suc(B_2)))))))|'LE'(f(B_2),s('0')))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f12])).
% 0.15/10.71 fof(f76,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(suc(X0))))),s(s('0')))|'E'(s('0'),f(suc(suc(suc(suc(X0))))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/10.71 fof(f77,plain,(
% 0.15/10.71 ![B_3]: ((![A_1]: (((((~iLEQ(suc(A_1),suc(B_3))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(B_3))))|~'E'(s('0'),f(B_3)))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_3),f(suc(B_3))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f13])).
% 0.15/10.71 fof(f78,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f77])).
% 0.15/10.71 fof(f79,plain,(
% 0.15/10.71 ![B_3]: ((![A_1]: (((((((((((~iLEQ(suc(A_1),suc(B_3))|~'E'(s('0'),f(suc(suc(A_1)))))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(suc(B_3)))))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(B_3))))|~'E'(s('0'),f(B_3)))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_3),f(suc(B_3))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(A_1))))))|'E'(f(A_1),f(suc(suc(suc(A_1)))))))|'E'(f(B_3),f(suc(suc(B_3)))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f14])).
% 0.15/10.71 fof(f80,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f79])).
% 0.15/10.71 fof(f81,plain,(
% 0.15/10.71 ![B_3]: ((![A_1]: (((((((((((((~iLEQ(suc(A_1),suc(B_3))|~'E'(s('0'),f(suc(suc(A_1)))))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(suc(B_3)))))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(B_3))))))|~'E'(s('0'),f(suc(B_3))))|~'E'(s('0'),f(B_3)))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_3),f(suc(B_3))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(A_1))))))|~'E'(f(B_3),f(suc(suc(B_3)))))|'E'(f(A_1),f(suc(suc(suc(A_1)))))))|'E'(f(B_3),f(suc(suc(suc(B_3))))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f15])).
% 0.15/10.71 fof(f82,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X1)))))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f81])).
% 0.15/10.71 fof(f87,plain,(
% 0.15/10.71 ![A_2]: ((((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(suc(A_2)))))|~'E'('0',f(A_2)))|~'E'('0',f(suc(suc(suc(suc(A_2)))))))|~'E'(f(A_2),f(suc(suc(suc(A_2))))))|~'E'('0',f(suc(suc(suc(A_2))))))|~'E'(f(A_2),f(suc(A_2))))|iLEQ(suc(A_2),suc(A_2)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f18])).
% 0.15/10.71 fof(f88,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f87])).
% 0.15/10.71 fof(f89,plain,(
% 0.15/10.71 ![B_5]: ((~'LE'(f(suc(B_5)),s('0'))|'E'('0',f(suc(B_5))))|'LE'(f(B_5),'0'))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f19])).
% 0.15/10.71 fof(f90,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(X0)),s('0'))|'E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f89])).
% 0.15/10.71 fof(f91,plain,(
% 0.15/10.71 ![B_5]: ((~'LE'(f(B_5),s('0'))|'E'('0',f(B_5)))|'LE'(f(B_5),'0'))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f20])).
% 0.15/10.71 fof(f92,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(X0),s('0'))|'E'('0',f(X0))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f91])).
% 0.15/10.71 fof(f93,plain,(
% 0.15/10.71 ![LE]: (~'LE'(f(z),'0'))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f21])).
% 0.15/10.71 fof(f94,plain,(
% 0.15/10.71 ![B_6]: ((![A_2]: (((((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(B_6)))))|~'E'('0',f(A_2)))|~iLEQ(suc(A_2),suc(B_6)))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'('0',f(B_6)))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_2),f(suc(A_2)))))|'E'(f(B_6),f(suc(suc(suc(B_6))))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f22])).
% 0.15/10.71 fof(f95,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f94])).
% 0.15/10.71 fof(f96,plain,(
% 0.15/10.71 ![A_1]: (((((~'E'(s('0'),f(suc(suc(A_1))))|~'E'(s('0'),f(suc(A_1))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s('0'),f(A_1)))|'E'(f(A_1),f(suc(suc(A_1)))))|iLEQ(suc(A_1),suc(A_1)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f23])).
% 0.15/10.71 fof(f97,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(X0))|'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f96])).
% 0.15/10.71 fof(f98,plain,(
% 0.15/10.71 ![A]: 'LE'(f(A),s(s('0')))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f24])).
% 0.15/10.71 fof(f99,plain,(
% 0.15/10.71 ![LE,X0]: ('LE'(f(X0),s(s('0'))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f98])).
% 0.15/10.71 fof(f102,plain,(
% 0.15/10.71 ![A_1]: ((((((((~'E'(s('0'),f(suc(suc(A_1))))|~'E'(s('0'),f(A_1)))|~'E'(f(A_1),f(suc(suc(suc(A_1))))))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(suc(A_1)))))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(A_1))))))|iLEQ(suc(A_1),suc(A_1)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f26])).
% 0.15/10.71 fof(f103,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/10.71 fof(f116,plain,(
% 0.15/10.71 ![B_6]: ((![A_2]: (((((~'E'('0',f(suc(A_2)))|~'E'('0',f(A_2)))|~iLEQ(suc(A_2),suc(B_6)))|~'E'('0',f(B_6)))|~'E'('0',f(suc(B_6))))|'E'(f(A_2),f(suc(A_2)))))|'E'(f(B_6),f(suc(B_6))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f33])).
% 0.15/10.71 fof(f117,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|~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))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f116])).
% 0.15/10.71 fof(f118,plain,(
% 0.15/10.71 ![B_3]: ((![A_1]: (((((((((~iLEQ(suc(A_1),suc(B_3))|~'E'(s('0'),f(suc(suc(A_1)))))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(suc(B_3)))))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(B_3))))|~'E'(s('0'),f(B_3)))|~'E'(f(B_3),f(suc(B_3))))|~'E'(f(A_1),f(suc(A_1))))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_3),f(suc(suc(B_3)))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f34])).
% 0.15/10.71 fof(f119,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f118])).
% 0.15/10.71 fof(f120,plain,(
% 0.15/10.71 ![B_6]: (((![A_2]: ((((((((((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(suc(A_2)))))|~'E'('0',f(A_2)))|~iLEQ(suc(A_2),suc(B_6)))|~'E'('0',f(suc(suc(suc(suc(A_2)))))))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'(f(A_2),f(suc(suc(suc(A_2))))))|~'E'('0',f(suc(suc(suc(suc(B_6)))))))|~'E'(f(B_6),f(suc(suc(suc(B_6))))))|~'E'('0',f(suc(suc(suc(A_2))))))|~'E'('0',f(B_6)))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'(f(A_2),f(suc(A_2)))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f35])).
% 0.15/10.71 fof(f121,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f120])).
% 0.15/10.71 fof(f122,plain,(
% 0.15/10.71 ![B_6]: ((![A_2]: (((((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(A_2)))))|~'E'('0',f(A_2)))|~iLEQ(suc(A_2),suc(B_6)))|~'E'('0',f(B_6)))|~'E'(f(A_2),f(suc(A_2))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_2),f(suc(suc(A_2))))))|'E'(f(B_6),f(suc(suc(B_6)))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f36])).
% 0.15/10.71 fof(f123,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f122])).
% 0.15/10.71 fof(f124,plain,(
% 0.15/10.71 ![B_6]: ((![A_2]: (((((((((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(suc(A_2)))))|~'E'('0',f(A_2)))|~iLEQ(suc(A_2),suc(B_6)))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'('0',f(suc(suc(suc(A_2))))))|~'E'('0',f(B_6)))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'(f(A_2),f(suc(A_2))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_2),f(suc(suc(suc(A_2)))))))|'E'(f(B_6),f(suc(suc(suc(B_6))))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f37])).
% 0.15/10.71 fof(f125,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f124])).
% 0.15/10.71 fof(f126,plain,(
% 0.15/10.71 ![B_2]: ((~'LE'(f(suc(suc(suc(B_2)))),s(s('0')))|'E'(s('0'),f(suc(suc(suc(B_2))))))|'LE'(f(B_2),s('0')))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f38])).
% 0.15/10.71 fof(f127,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(X0)))),s(s('0')))|'E'(s('0'),f(suc(suc(suc(X0)))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f126])).
% 0.15/10.71 fof(f128,plain,(
% 0.15/10.71 ![B_5]: ((~'LE'(f(suc(suc(suc(suc(B_5))))),s('0'))|'E'('0',f(suc(suc(suc(suc(B_5)))))))|'LE'(f(B_5),'0'))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f39])).
% 0.15/10.71 fof(f129,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(suc(X0))))),s('0'))|'E'('0',f(suc(suc(suc(suc(X0))))))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f128])).
% 0.15/10.71 fof(f130,plain,(
% 0.15/10.71 ![B_3]: ((![A_1]: (((((((((((((((~iLEQ(suc(A_1),suc(B_3))|~'E'(s('0'),f(suc(suc(A_1)))))|~'E'(s('0'),f(suc(suc(suc(suc(B_3)))))))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(suc(B_3)))))|~'E'(f(A_1),f(suc(suc(suc(A_1))))))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(suc(suc(suc(A_1)))))))|~'E'(s('0'),f(suc(suc(suc(B_3))))))|~'E'(s('0'),f(suc(B_3))))|~'E'(s('0'),f(B_3)))|~'E'(f(A_1),f(suc(suc(A_1)))))|~'E'(f(B_3),f(suc(B_3))))|~'E'(f(A_1),f(suc(A_1))))|~'E'(f(B_3),f(suc(suc(suc(B_3))))))|~'E'(s('0'),f(suc(suc(suc(A_1)))))))|~'E'(f(B_3),f(suc(suc(B_3)))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f40])).
% 0.15/10.71 fof(f131,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X1))))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X1)))))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f130])).
% 0.15/10.71 fof(f132,plain,(
% 0.15/10.71 ![A_2]: (((~'E'('0',f(A_2))|~'E'('0',f(suc(A_2))))|'E'(f(A_2),f(suc(A_2))))|iLEQ(suc(A_2),suc(A_2)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f41])).
% 0.15/10.71 fof(f133,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f132])).
% 0.15/10.71 fof(f134,plain,(
% 0.15/10.71 ![B_2]: ((~'LE'(f(suc(B_2)),s(s('0')))|'E'(s('0'),f(suc(B_2))))|'LE'(f(B_2),s('0')))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f42])).
% 0.15/10.71 fof(f135,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s('0')))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f134])).
% 0.15/10.71 fof(f136,plain,(
% 0.15/10.71 ![A_2]: (((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(A_2)))))|~'E'(f(A_2),f(suc(suc(A_2)))))|~'E'('0',f(A_2)))|~'E'('0',f(suc(suc(suc(A_2))))))|~'E'(f(A_2),f(suc(A_2))))|'E'(f(A_2),f(suc(suc(suc(A_2))))))|iLEQ(suc(A_2),suc(A_2)))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f43])).
% 0.15/10.71 fof(f137,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f136])).
% 0.15/10.71 fof(f142,plain,(
% 0.15/10.71 ![B_3]: ((![A_1]: (((((((~iLEQ(suc(A_1),suc(B_3))|~'E'(s('0'),f(A_1)))|~'E'(s('0'),f(suc(suc(B_3)))))|~'E'(s('0'),f(suc(A_1))))|~'E'(s('0'),f(suc(B_3))))|~'E'(s('0'),f(B_3)))|~'E'(f(B_3),f(suc(B_3))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_3),f(suc(suc(B_3)))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f46])).
% 0.15/10.71 fof(f143,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f142])).
% 0.15/10.71 fof(f146,plain,(
% 0.15/10.71 ![B_6]: ((![A_2]: (((((((~'E'('0',f(suc(A_2)))|~'E'('0',f(suc(suc(B_6)))))|~'E'('0',f(A_2)))|~iLEQ(suc(A_2),suc(B_6)))|~'E'('0',f(B_6)))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_2),f(suc(A_2)))))|'E'(f(B_6),f(suc(suc(B_6)))))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f48])).
% 0.15/10.71 fof(f147,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f146])).
% 0.15/10.71 fof(f152,plain,(
% 0.15/10.71 ![B_5]: ((~'LE'(f(suc(suc(B_5))),s('0'))|'E'('0',f(suc(suc(B_5)))))|'LE'(f(B_5),'0'))),
% 0.15/10.71 inference(miniscoping,[status(thm)],[f51])).
% 0.15/10.71 fof(f153,plain,(
% 0.15/10.71 ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s('0'))|'E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(cnf_transformation,[status(thm)],[f152])).
% 0.15/10.71 fof(f162,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f72,f99])).
% 0.15/10.71 fof(f176,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f135,f99])).
% 0.15/10.71 fof(f205,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'(s('0'),f(suc(suc(X0))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f60,f99])).
% 0.15/10.71 fof(f244,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'(s('0'),f(suc(suc(suc(X0)))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f127,f99])).
% 0.15/10.71 fof(f273,plain,(
% 0.15/10.71 ![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)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f66,f133])).
% 0.15/10.71 fof(f274,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'(s('0'),f(suc(suc(suc(suc(X0))))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f76,f99])).
% 0.15/10.71 fof(f303,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f68,f56])).
% 0.15/10.71 fof(f306,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f303,f307])).
% 0.15/10.71 fof(f307,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|'E'(f(X0),f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f97,f56])).
% 0.15/10.71 fof(f326,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X0))|~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(suc(X1)))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f147,f117])).
% 0.15/10.71 fof(f328,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X1)))))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f82,f80])).
% 0.15/10.71 fof(f329,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f137,f273])).
% 0.15/10.71 fof(f338,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f143,f78])).
% 0.15/10.71 fof(f339,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f88,f273])).
% 0.15/10.71 fof(f340,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f123,f326])).
% 0.15/10.71 fof(f341,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0)))))),
% 0.15/10.71 inference(factoring,[status(thm)],[f340])).
% 0.15/10.71 fof(f342,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0)))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f341])).
% 0.15/10.71 fof(f343,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0)))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f342,f273])).
% 0.15/10.71 fof(f345,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f95,f326])).
% 0.15/10.71 fof(f346,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f103,f56])).
% 0.15/10.71 fof(f348,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(resolution,[status(thm)],[f346,f306])).
% 0.15/10.71 fof(f351,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f348])).
% 0.15/10.71 fof(f352,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f351,f307])).
% 0.15/10.71 fof(f355,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(resolution,[status(thm)],[f352,f328])).
% 0.15/10.71 fof(f356,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(resolution,[status(thm)],[f352,f78])).
% 0.15/10.71 fof(f359,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f355])).
% 0.15/10.71 fof(f360,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f356])).
% 0.15/10.71 fof(f365,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f359,f360])).
% 0.15/10.71 fof(f370,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f119,f338])).
% 0.15/10.71 fof(f371,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(resolution,[status(thm)],[f370,f352])).
% 0.15/10.71 fof(f372,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f371])).
% 0.15/10.71 fof(f373,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f372,f360])).
% 0.15/10.71 fof(f374,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f365,f373])).
% 0.15/10.71 fof(f385,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f121,f343])).
% 0.15/10.71 fof(f386,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0))))),
% 0.15/10.71 inference(factoring,[status(thm)],[f385])).
% 0.15/10.71 fof(f387,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f386])).
% 0.15/10.71 fof(f388,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f387,f339])).
% 0.15/10.71 fof(f389,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f388,f343])).
% 0.15/10.71 fof(f391,plain,(
% 0.15/10.71 ![E,X0,X1]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f125,f345])).
% 0.15/10.71 fof(f392,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(factoring,[status(thm)],[f391])).
% 0.15/10.71 fof(f394,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f392])).
% 0.15/10.71 fof(f395,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f394,f343])).
% 0.15/10.71 fof(f396,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f389,f397])).
% 0.15/10.71 fof(f397,plain,(
% 0.15/10.71 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f395,f329])).
% 0.15/10.71 fof(f398,plain,(
% 0.15/10.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X1))))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X1))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X1)))))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X1),f(suc(suc(X1)))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f131,f374])).
% 0.15/10.71 fof(f399,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(resolution,[status(thm)],[f398,f352])).
% 0.15/10.71 fof(f400,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f399])).
% 0.15/10.71 fof(f401,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f400,f373])).
% 0.15/10.71 fof(f402,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f374,f403])).
% 0.15/10.71 fof(f403,plain,(
% 0.15/10.71 ![E,X0]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(suc(suc(suc(suc(X0))))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(suc(X0))))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f401,f360])).
% 0.15/10.71 fof(f408,plain,(
% 0.15/10.71 ![E,X0,LE]: (~'E'(s('0'),f(suc(suc(X0))))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(resolution,[status(thm)],[f402,f274])).
% 0.15/10.71 fof(f418,plain,(
% 0.15/10.71 ![E,X0,LE]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f408,f205])).
% 0.15/10.71 fof(f427,plain,(
% 0.15/10.71 ![E,X0,LE]: (~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(suc(suc(suc(X0)))))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f418,f162])).
% 0.15/10.71 fof(f429,plain,(
% 0.15/10.71 ![E,X0,LE]: (~'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0'))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(resolution,[status(thm)],[f427,f244])).
% 0.15/10.71 fof(f434,plain,(
% 0.15/10.71 ![E,X0,LE]: (~'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f429])).
% 0.15/10.71 fof(f435,plain,(
% 0.15/10.71 ![LE,X0]: ('LE'(f(X0),s('0')))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f434,f176])).
% 0.15/10.71 fof(f439,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'('0',f(suc(suc(suc(suc(X0))))))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f129,f435])).
% 0.15/10.71 fof(f440,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'('0',f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f58,f435])).
% 0.15/10.71 fof(f441,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f153,f435])).
% 0.15/10.71 fof(f442,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f90,f435])).
% 0.15/10.71 fof(f443,plain,(
% 0.15/10.71 ![E,X0,LE]: ('E'('0',f(X0))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f92,f435])).
% 0.15/10.71 fof(f503,plain,(
% 0.15/10.71 ![LE,X0,E,X1]: ('LE'(f(X0),'0')|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(X0))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(resolution,[status(thm)],[f442,f117])).
% 0.15/10.71 fof(f504,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(resolution,[status(thm)],[f442,f133])).
% 0.15/10.71 fof(f536,plain,(
% 0.15/10.71 ![LE,X0,E,X1]: ('LE'(f(X0),'0')|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~iLEQ(suc(X1),suc(X0))|'E'(f(X1),f(suc(X1)))|'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f503,f443])).
% 0.15/10.71 fof(f537,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f504,f443])).
% 0.15/10.71 fof(f660,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(resolution,[status(thm)],[f439,f396])).
% 0.15/10.71 fof(f688,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f660,f442])).
% 0.15/10.71 fof(f933,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f688,f441])).
% 0.15/10.71 fof(f935,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(resolution,[status(thm)],[f933,f440])).
% 0.15/10.71 fof(f945,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f935])).
% 0.15/10.71 fof(f946,plain,(
% 0.15/10.71 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'(f(X0),f(suc(X0))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f945,f443])).
% 0.15/10.71 fof(f956,plain,(
% 0.15/10.71 ![LE,X0]: ('LE'(f(X0),'0')|iLEQ(suc(X0),suc(X0)))),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f537,f946])).
% 0.15/10.71 fof(f1020,plain,(
% 0.15/10.71 ![LE,X0,E,X1]: ('LE'(f(X0),'0')|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~iLEQ(suc(X1),suc(X0))|'E'(f(X1),f(suc(X1))))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f536,f946])).
% 0.15/10.71 fof(f1024,plain,(
% 0.15/10.71 ![LE,X0,E,X1]: ('LE'(f(X0),'0')|~'E'('0',f(X1))|~iLEQ(suc(X1),suc(X0))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),'0'))),
% 0.15/10.71 inference(resolution,[status(thm)],[f1020,f442])).
% 0.15/10.71 fof(f1029,plain,(
% 0.15/10.71 ![LE,X0,X1,E]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X0))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),'0'))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f1024,f443])).
% 0.15/10.71 fof(f1052,plain,(
% 0.15/10.71 ![LE,X0,X1]: ('LE'(f(X0),'0')|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),'0'))),
% 0.15/10.71 inference(forward_subsumption_resolution,[status(thm)],[f1029,f946])).
% 0.15/10.71 fof(f1060,plain,(
% 0.15/10.71 ![LE,X0]: ('LE'(f(X0),'0')|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 0.15/10.71 inference(resolution,[status(thm)],[f1052,f956])).
% 0.15/10.71 fof(f1068,plain,(
% 0.15/10.71 ![LE,X0]: ('LE'(f(X0),'0'))),
% 0.15/10.71 inference(duplicate_literals_removal,[status(thm)],[f1060])).
% 0.15/10.71 fof(f1070,plain,(
% 0.15/10.71 $false),
% 0.15/10.71 inference(backward_subsumption_resolution,[status(thm)],[f93,f1068])).
% 0.15/10.71 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/10.72 % Elapsed time: 0.321027 seconds
% 0.15/10.72 % CPU time: 2.345716 seconds
% 0.15/10.72 % Total memory used: 32.518 MB
% 0.15/10.72 % Net memory used: 26.514 MB
%------------------------------------------------------------------------------