%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO651-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 : n013.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 14.03s 2.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO651-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n013.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 12:07:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 14.03/2.37 % Refutation found
% 14.03/2.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 14.03/2.37 % SZS output start CNFRefutation for theBenchmark
% 14.03/2.37 fof(f3,axiom,(
% 14.03/2.37 (![E,A_1]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(A_1),f(suc(suc(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)))| ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f7,axiom,(
% 14.03/2.37 (![E,A_1,B_6,B_7]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_7),f(suc(suc(B_7))))| ~ 'E'('0',f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_7))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_1),f(suc(suc(suc(A_1)))))| 'E'(f(B_6),f(suc(suc(B_6))))| 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f11,axiom,(
% 14.03/2.37 (![LE,B_5,E]: (( ~ 'LE'(f(suc(B_5)),s('0'))| 'E'('0',f(suc(B_5)))| 'LE'(f(B_5),'0') ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f14,axiom,(
% 14.03/2.37 (![LE,A]: ('LE'(f(A),s('0')) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f20,axiom,(
% 14.03/2.37 (![E,A_1,B_6,B_7]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_7),f(suc(suc(B_7))))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_7))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_1),f(suc(suc(suc(A_1)))))| 'E'(f(B_6),f(suc(suc(suc(B_6)))))| 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f25,axiom,(
% 14.03/2.37 (![E,B_6,A_1,B_7]: (( ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(B_6))| ~ 'E'('0',f(B_7))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_1),f(suc(suc(A_1))))| 'E'(f(B_6),f(suc(suc(B_6))))| 'E'(f(B_7),f(suc(suc(B_7)))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f29,axiom,(
% 14.03/2.37 (![A_1,B_6,E,B_7]: (( ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'('0',f(A_1))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'('0',f(B_6))| ~ 'E'('0',f(B_7))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_1),f(suc(A_1)))| 'E'(f(B_6),f(suc(B_6)))| 'E'(f(B_7),f(suc(B_7))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f30,axiom,(
% 14.03/2.37 (![E,A_1,B_6,B_7]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_7),f(suc(suc(B_7))))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_7))| ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(B_7),f(suc(suc(suc(B_7))))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f34,axiom,(
% 14.03/2.37 (![E,A_1,B_6,B_7]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'('0',f(B_7))| ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(B_7),f(suc(B_7))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f36,axiom,(
% 14.03/2.37 (![LE,B_5,E]: (( ~ 'LE'(f(suc(suc(B_5))),s('0'))| 'E'('0',f(suc(suc(B_5))))| 'LE'(f(B_5),'0') ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f39,axiom,(
% 14.03/2.37 (![LE]: (~ 'LE'(f(z),'0') ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f44,axiom,(
% 14.03/2.37 (![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') ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f46,axiom,(
% 14.03/2.37 (![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)))| 'E'(f(A_1),f(suc(suc(suc(A_1)))))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f47,axiom,(
% 14.03/2.37 (![E,B_6,A_1,B_7]: (( ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))| ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_7),f(suc(suc(B_7))))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_7))| ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(A_1),f(suc(A_1))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f55,axiom,(
% 14.03/2.37 (![E,A_1,B_6,B_7]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'('0',f(B_7))| ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6)))| 'E'(f(B_7),f(suc(suc(B_7)))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f57,axiom,(
% 14.03/2.37 (![LE,B_5,E]: (( ~ 'LE'(f(B_5),s('0'))| 'E'('0',f(B_5))| 'LE'(f(B_5),'0') ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f61,axiom,(
% 14.03/2.37 (![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') ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f64,axiom,(
% 14.03/2.37 (![E,A_1,B_6,B_7]: (( ~ 'E'('0',f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(B_6))))| ~ iLEQ(suc(A_1),suc(B_6))| ~ 'E'('0',f(suc(B_7)))| ~ 'E'('0',f(suc(A_1)))| ~ 'E'(f(B_7),f(suc(B_7)))| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))| ~ 'E'('0',f(suc(suc(A_1))))| ~ 'E'('0',f(A_1))| ~ 'E'('0',f(suc(suc(B_7))))| ~ 'E'('0',f(suc(suc(suc(B_6)))))| ~ 'E'(f(A_1),f(suc(suc(A_1))))| ~ iLEQ(suc(B_6),suc(B_7))| ~ 'E'(f(A_1),f(suc(A_1)))| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))| ~ 'E'(f(B_7),f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_6))| ~ 'E'(f(B_7),f(suc(suc(B_7))))| ~ 'E'(f(B_6),f(suc(suc(B_6))))| ~ 'E'('0',f(suc(suc(suc(B_7)))))| ~ 'E'('0',f(B_7))| ~ 'E'('0',f(suc(suc(suc(suc(B_7))))))| ~ 'E'('0',f(suc(suc(suc(suc(A_1))))))| ~ 'E'(f(B_6),f(suc(B_6)))| ~ 'E'('0',f(suc(B_6))) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f67,axiom,(
% 14.03/2.37 (![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)) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f74,axiom,(
% 14.03/2.37 (![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)) ) ))),
% 14.03/2.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.03/2.37 fof(f80,plain,(
% 14.03/2.37 ![A_1]: ((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(A_1))))|~'E'(f(A_1),f(suc(suc(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))))|~'E'('0',f(suc(suc(suc(suc(A_1)))))))|iLEQ(suc(A_1),suc(A_1)))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f3])).
% 14.03/2.37 fof(f81,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(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)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|iLEQ(suc(X0),suc(X0)))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f80])).
% 14.03/2.37 fof(f88,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: ((![A_1]: ((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(suc(B_6)))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(B_6)))|~'E'(f(B_7),f(suc(suc(B_7)))))|~'E'('0',f(suc(suc(suc(B_7))))))|~'E'('0',f(B_7)))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_1),f(suc(suc(suc(A_1)))))))|'E'(f(B_6),f(suc(suc(B_6))))))|'E'(f(B_7),f(suc(suc(suc(B_7))))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f7])).
% 14.03/2.37 fof(f89,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(suc(X2))))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f88])).
% 14.03/2.37 fof(f96,plain,(
% 14.03/2.37 ![B_5]: ((~'LE'(f(suc(B_5)),s('0'))|'E'('0',f(suc(B_5))))|'LE'(f(B_5),'0'))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f11])).
% 14.03/2.37 fof(f97,plain,(
% 14.03/2.37 ![LE,X0,E]: (~'LE'(f(suc(X0)),s('0'))|'E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f96])).
% 14.03/2.37 fof(f102,plain,(
% 14.03/2.37 ![A]: 'LE'(f(A),s('0'))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f14])).
% 14.03/2.37 fof(f103,plain,(
% 14.03/2.37 ![LE,X0]: ('LE'(f(X0),s('0')))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f102])).
% 14.03/2.37 fof(f114,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: ((![A_1]: ((((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(suc(B_6)))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(B_6)))|~'E'(f(B_7),f(suc(suc(B_7)))))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(suc(B_7))))))|~'E'('0',f(B_7)))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_1),f(suc(suc(suc(A_1)))))))|'E'(f(B_6),f(suc(suc(suc(B_6)))))))|'E'(f(B_7),f(suc(suc(suc(B_7))))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f20])).
% 14.03/2.37 fof(f115,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1)))))|'E'(f(X2),f(suc(suc(suc(X2))))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f114])).
% 14.03/2.37 fof(f124,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: ((![A_1]: ((((((((((((((~'E'('0',f(suc(suc(B_6))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(B_6)))|~'E'('0',f(B_7)))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))|'E'(f(A_1),f(suc(suc(A_1))))))|'E'(f(B_6),f(suc(suc(B_6))))))|'E'(f(B_7),f(suc(suc(B_7)))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f25])).
% 14.03/2.37 fof(f125,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X0),suc(X2))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X2),f(suc(suc(X2)))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f124])).
% 14.03/2.37 fof(f132,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: ((![A_1]: ((((((((~iLEQ(suc(A_1),suc(B_6))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'('0',f(A_1)))|~iLEQ(suc(B_6),suc(B_7)))|~'E'('0',f(B_6)))|~'E'('0',f(B_7)))|~'E'('0',f(suc(B_6))))|'E'(f(A_1),f(suc(A_1)))))|'E'(f(B_6),f(suc(B_6)))))|'E'(f(B_7),f(suc(B_7))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f29])).
% 14.03/2.37 fof(f133,plain,(
% 14.03/2.37 ![X0,X1,E,X2]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(X1))|~'E'('0',f(X2))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f132])).
% 14.03/2.37 fof(f134,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: (((![A_1]: (((((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(suc(B_6)))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'(f(A_1),f(suc(suc(suc(A_1))))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(suc(suc(suc(suc(B_6)))))))|~'E'(f(B_6),f(suc(suc(suc(B_6))))))|~'E'('0',f(B_6)))|~'E'(f(B_7),f(suc(suc(B_7)))))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(suc(B_7))))))|~'E'('0',f(B_7)))|~'E'('0',f(suc(suc(suc(suc(A_1))))))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6)))))|'E'(f(B_7),f(suc(suc(suc(B_7))))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f30])).
% 14.03/2.37 fof(f135,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X2),f(suc(suc(suc(X2))))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f134])).
% 14.03/2.37 fof(f142,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: (((![A_1]: (((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(suc(B_6)))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(A_1),f(suc(suc(suc(A_1))))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(suc(suc(suc(suc(B_6)))))))|~'E'(f(B_6),f(suc(suc(suc(B_6))))))|~'E'('0',f(B_6)))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'('0',f(B_7)))|~'E'('0',f(suc(suc(suc(suc(A_1))))))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6)))))|'E'(f(B_7),f(suc(B_7))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f34])).
% 14.03/2.37 fof(f143,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X2),f(suc(X2))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f142])).
% 14.03/2.37 fof(f146,plain,(
% 14.03/2.37 ![B_5]: ((~'LE'(f(suc(suc(B_5))),s('0'))|'E'('0',f(suc(suc(B_5)))))|'LE'(f(B_5),'0'))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f36])).
% 14.03/2.37 fof(f147,plain,(
% 14.03/2.37 ![LE,X0,E]: (~'LE'(f(suc(suc(X0))),s('0'))|'E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f146])).
% 14.03/2.37 fof(f152,plain,(
% 14.03/2.37 ![LE]: (~'LE'(f(z),'0'))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f39])).
% 14.03/2.37 fof(f161,plain,(
% 14.03/2.37 ![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'))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f44])).
% 14.03/2.37 fof(f162,plain,(
% 14.03/2.37 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(suc(X0))))),s('0'))|'E'('0',f(suc(suc(suc(suc(X0))))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f161])).
% 14.03/2.37 fof(f165,plain,(
% 14.03/2.37 ![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))))|'E'(f(A_1),f(suc(suc(suc(A_1))))))|iLEQ(suc(A_1),suc(A_1)))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f46])).
% 14.03/2.37 fof(f166,plain,(
% 14.03/2.37 ![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)))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f165])).
% 14.03/2.37 fof(f167,plain,(
% 14.03/2.37 ![A_1]: ((![B_6]: (((![B_7]: (((((((((((((((((~'E'('0',f(suc(suc(B_6))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~'E'('0',f(suc(suc(suc(B_6))))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'('0',f(suc(suc(suc(suc(B_6)))))))|~'E'(f(B_6),f(suc(suc(suc(B_6))))))|~'E'(f(B_7),f(suc(suc(suc(B_7))))))|~'E'('0',f(B_6)))|~'E'(f(B_7),f(suc(suc(B_7)))))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(suc(B_7))))))|~'E'('0',f(B_7)))|~'E'('0',f(suc(suc(suc(suc(B_7))))))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6)))))|'E'(f(A_1),f(suc(A_1))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f47])).
% 14.03/2.37 fof(f168,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X0),suc(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X2),f(suc(suc(suc(X2)))))|~'E'('0',f(X0))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X2))))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f167])).
% 14.03/2.37 fof(f183,plain,(
% 14.03/2.37 ![B_7]: ((![B_6]: (((![A_1]: (((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(suc(B_6)))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'(f(A_1),f(suc(suc(suc(A_1))))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(suc(suc(suc(suc(B_6)))))))|~'E'(f(B_6),f(suc(suc(suc(B_6))))))|~'E'('0',f(B_6)))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'('0',f(B_7)))|~'E'('0',f(suc(suc(suc(suc(A_1))))))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6)))))|'E'(f(B_7),f(suc(suc(B_7)))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f55])).
% 14.03/2.37 fof(f184,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f183])).
% 14.03/2.37 fof(f187,plain,(
% 14.03/2.37 ![B_5]: ((~'LE'(f(B_5),s('0'))|'E'('0',f(B_5)))|'LE'(f(B_5),'0'))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f57])).
% 14.03/2.37 fof(f188,plain,(
% 14.03/2.37 ![LE,X0,E]: (~'LE'(f(X0),s('0'))|'E'('0',f(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f187])).
% 14.03/2.37 fof(f195,plain,(
% 14.03/2.37 ![B_5]: ((~'LE'(f(suc(suc(suc(B_5)))),s('0'))|'E'('0',f(suc(suc(suc(B_5))))))|'LE'(f(B_5),'0'))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f61])).
% 14.03/2.37 fof(f196,plain,(
% 14.03/2.37 ![LE,X0,E]: (~'LE'(f(suc(suc(suc(X0)))),s('0'))|'E'('0',f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f195])).
% 14.03/2.37 fof(f201,plain,(
% 14.03/2.37 ![B_6]: (((![A_1]: ((![B_7]: ((((((((((((((((((((((~'E'('0',f(suc(suc(suc(A_1)))))|~'E'('0',f(suc(suc(B_6)))))|~iLEQ(suc(A_1),suc(B_6)))|~'E'('0',f(suc(B_7))))|~'E'('0',f(suc(A_1))))|~'E'(f(B_7),f(suc(B_7))))|~'E'(f(A_1),f(suc(suc(suc(A_1))))))|~'E'('0',f(suc(suc(A_1)))))|~'E'('0',f(A_1)))|~'E'('0',f(suc(suc(B_7)))))|~'E'('0',f(suc(suc(suc(B_6))))))|~'E'(f(A_1),f(suc(suc(A_1)))))|~iLEQ(suc(B_6),suc(B_7)))|~'E'(f(A_1),f(suc(A_1))))|~'E'('0',f(suc(suc(suc(suc(B_6)))))))|~'E'(f(B_6),f(suc(suc(suc(B_6))))))|~'E'(f(B_7),f(suc(suc(suc(B_7))))))|~'E'('0',f(B_6)))|~'E'(f(B_7),f(suc(suc(B_7)))))|~'E'(f(B_6),f(suc(suc(B_6)))))|~'E'('0',f(suc(suc(suc(B_7))))))|~'E'('0',f(B_7)))|~'E'('0',f(suc(suc(suc(suc(B_7))))))))|~'E'('0',f(suc(suc(suc(suc(A_1))))))))|~'E'(f(B_6),f(suc(B_6))))|~'E'('0',f(suc(B_6))))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f64])).
% 14.03/2.37 fof(f202,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'(f(X2),f(suc(suc(suc(X2)))))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X2))))))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1))))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f201])).
% 14.03/2.37 fof(f207,plain,(
% 14.03/2.37 ![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)))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f67])).
% 14.03/2.37 fof(f208,plain,(
% 14.03/2.37 ![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)))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f207])).
% 14.03/2.37 fof(f221,plain,(
% 14.03/2.37 ![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)))),
% 14.03/2.37 inference(miniscoping,[status(thm)],[f74])).
% 14.03/2.37 fof(f222,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 14.03/2.37 inference(cnf_transformation,[status(thm)],[f221])).
% 14.03/2.37 fof(f225,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(factoring,[status(thm)],[f143])).
% 14.03/2.37 fof(f226,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(X1))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f225])).
% 14.03/2.37 fof(f227,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(X1))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f226,f81])).
% 14.03/2.37 fof(f228,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X0),suc(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X2),f(suc(suc(suc(X2)))))|~'E'('0',f(X0))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X2))))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f168,f227])).
% 14.03/2.37 fof(f230,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'('0',f(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f188,f103])).
% 14.03/2.37 fof(f232,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f97,f103])).
% 14.03/2.37 fof(f241,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'('0',f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f147,f103])).
% 14.03/2.37 fof(f250,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(suc(X0))))))|iLEQ(suc(X0),suc(X0)))),
% 14.03/2.37 inference(backward_subsumption_resolution,[status(thm)],[f81,f222])).
% 14.03/2.37 fof(f252,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f222,f232])).
% 14.03/2.37 fof(f254,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f252,f230])).
% 14.03/2.37 fof(f255,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'('0',f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f196,f103])).
% 14.03/2.37 fof(f264,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'('0',f(suc(suc(suc(suc(X0))))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f162,f103])).
% 14.03/2.37 fof(f273,plain,(
% 14.03/2.37 ![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)))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f208,f222])).
% 14.03/2.37 fof(f289,plain,(
% 14.03/2.37 ![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(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0)))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f166,f273])).
% 14.03/2.37 fof(f291,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'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(suc(X0)))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f289,f255])).
% 14.03/2.37 fof(f295,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f291,f230])).
% 14.03/2.37 fof(f298,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f295,f232])).
% 14.03/2.37 fof(f302,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0')|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f298,f254])).
% 14.03/2.37 fof(f309,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f302])).
% 14.03/2.37 fof(f310,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'(f(X0),f(suc(suc(suc(X0)))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f309,f241])).
% 14.03/2.37 fof(f357,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|iLEQ(suc(X0),suc(X0)))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f250,f273])).
% 14.03/2.37 fof(f358,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f357,f264])).
% 14.03/2.37 fof(f362,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f358,f230])).
% 14.03/2.37 fof(f407,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X2),f(suc(suc(suc(X2))))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f135,f227])).
% 14.03/2.37 fof(f421,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X1),f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 14.03/2.37 inference(factoring,[status(thm)],[f407])).
% 14.03/2.37 fof(f439,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f421])).
% 14.03/2.37 fof(f440,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|'E'(f(X1),f(suc(suc(suc(X1))))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f439,f357])).
% 14.03/2.37 fof(f477,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f362,f255])).
% 14.03/2.37 fof(f482,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0')|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f477,f310])).
% 14.03/2.37 fof(f491,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f482])).
% 14.03/2.37 fof(f492,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f491,f232])).
% 14.03/2.37 fof(f493,plain,(
% 14.03/2.37 ![X0,LE]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f492,f241])).
% 14.03/2.37 fof(f565,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X0),suc(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X2))))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(backward_subsumption_resolution,[status(thm)],[f228,f440])).
% 14.03/2.37 fof(f591,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X2),f(suc(suc(X2)))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f184,f227])).
% 14.03/2.37 fof(f604,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(suc(X1)))))),
% 14.03/2.37 inference(factoring,[status(thm)],[f591])).
% 14.03/2.37 fof(f621,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(X1))|'E'(f(X1),f(suc(suc(X1)))))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f604])).
% 14.03/2.37 fof(f622,plain,(
% 14.03/2.37 ![E,X0,X1]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'('0',f(X1))|'E'(f(X1),f(suc(suc(X1)))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f621,f357])).
% 14.03/2.37 fof(f624,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X0)))))|~iLEQ(suc(X0),suc(X2))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X2))))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 14.03/2.37 inference(backward_subsumption_resolution,[status(thm)],[f565,f622])).
% 14.03/2.37 fof(f705,plain,(
% 14.03/2.37 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f133,f493])).
% 14.03/2.37 fof(f720,plain,(
% 14.03/2.37 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f705])).
% 14.03/2.37 fof(f721,plain,(
% 14.03/2.37 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f720,f230])).
% 14.03/2.37 fof(f722,plain,(
% 14.03/2.37 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1)))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f721,f232])).
% 14.03/2.37 fof(f730,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f722,f493])).
% 14.03/2.37 fof(f745,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f730])).
% 14.03/2.37 fof(f746,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f745,f230])).
% 14.03/2.37 fof(f748,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f746,f232])).
% 14.03/2.37 fof(f813,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(suc(suc(suc(X1))))))|~'E'(f(X1),f(suc(suc(suc(X1)))))|~'E'(f(X2),f(suc(suc(suc(X2)))))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'('0',f(suc(suc(suc(suc(X2))))))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f202,f624])).
% 14.03/2.37 fof(f837,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(suc(suc(X0))))))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0))))),
% 14.03/2.37 inference(factoring,[status(thm)],[f813])).
% 14.03/2.37 fof(f868,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(suc(X0)))))))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f837])).
% 14.03/2.37 fof(f869,plain,(
% 14.03/2.37 ![E,X0]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(suc(X0)))))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f868,f357])).
% 14.03/2.37 fof(f1047,plain,(
% 14.03/2.37 ![E,X0,X1,X2]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X2))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'('0',f(X2))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(X1)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1)))))|'E'(f(X2),f(suc(suc(suc(X2))))))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f115,f89])).
% 14.03/2.37 fof(f1055,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(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(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1)))))|'E'(f(X1),f(suc(suc(suc(X1)))))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f1047,f493])).
% 14.03/2.37 fof(f1070,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X1),f(suc(suc(suc(X1)))))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f1055])).
% 14.03/2.37 fof(f1071,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(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)))))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1070,f230])).
% 14.03/2.37 fof(f1078,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f869,f264])).
% 14.03/2.37 fof(f1082,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1078,f230])).
% 14.03/2.37 fof(f1085,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1082,f255])).
% 14.03/2.37 fof(f1290,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(X1))|~'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))))|'E'(f(X1),f(suc(suc(X1))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f125,f493])).
% 14.03/2.37 fof(f1305,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f1290])).
% 14.03/2.37 fof(f1306,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X1))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1305,f230])).
% 14.03/2.37 fof(f1309,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X0))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1306,f241])).
% 14.03/2.37 fof(f1320,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X0))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X1),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f1309,f748])).
% 14.03/2.37 fof(f1328,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X1),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1320,f230])).
% 14.03/2.37 fof(f1329,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X1),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1328,f232])).
% 14.03/2.37 fof(f1332,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X1),'0')|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f1329,f241])).
% 14.03/2.37 fof(f1336,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(X0)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X1),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f1332])).
% 14.03/2.37 fof(f1337,plain,(
% 14.03/2.37 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'LE'(f(X0),'0')|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1336,f232])).
% 14.03/2.37 fof(f1339,plain,(
% 14.03/2.37 ![X0,X1,E,LE]: (~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X1),f(suc(suc(X1))))|'LE'(f(X0),'0')|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1337,f748])).
% 14.03/2.37 fof(f1347,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0))))|'LE'(f(X0),'0')|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f1339,f493])).
% 14.03/2.37 fof(f1355,plain,(
% 14.03/2.37 ![E,X0,LE]: ('E'(f(X0),f(suc(suc(X0))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(duplicate_literals_removal,[status(thm)],[f1347])).
% 14.03/2.37 fof(f1356,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(backward_subsumption_resolution,[status(thm)],[f1085,f1355])).
% 14.03/2.37 fof(f1357,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1356,f241])).
% 14.03/2.37 fof(f1384,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1357,f232])).
% 14.03/2.37 fof(f2035,plain,(
% 14.03/2.37 ![E,X0,X1,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(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)))))|'LE'(f(X1),'0'))),
% 14.03/2.37 inference(forward_subsumption_resolution,[status(thm)],[f1071,f255])).
% 14.03/2.37 fof(f2043,plain,(
% 14.03/2.37 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'(f(X0),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)))|~'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 14.03/2.37 inference(resolution,[status(thm)],[f2035,f493])).
% 14.03/2.37 fof(f2058,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(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))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(duplicate_literals_removal,[status(thm)],[f2043])).
% 14.03/2.38 fof(f2059,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(forward_subsumption_resolution,[status(thm)],[f2058,f230])).
% 14.03/2.38 fof(f2060,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(forward_subsumption_resolution,[status(thm)],[f2059,f255])).
% 14.03/2.38 fof(f2071,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0')|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(resolution,[status(thm)],[f2060,f1355])).
% 14.03/2.38 fof(f2079,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(duplicate_literals_removal,[status(thm)],[f2071])).
% 14.03/2.38 fof(f2080,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'('0',f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(forward_subsumption_resolution,[status(thm)],[f2079,f241])).
% 14.03/2.38 fof(f2090,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'(f(X0),f(suc(X0)))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(backward_subsumption_resolution,[status(thm)],[f1384,f2091])).
% 14.03/2.38 fof(f2091,plain,(
% 14.03/2.38 ![E,X0,LE]: (~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(suc(X0)))))|'LE'(f(X0),'0'))),
% 14.03/2.38 inference(forward_subsumption_resolution,[status(thm)],[f2080,f232])).
% 14.03/2.38 fof(f2103,plain,(
% 14.03/2.38 ![LE,X0]: ('LE'(f(X0),'0'))),
% 14.03/2.38 inference(forward_subsumption_resolution,[status(thm)],[f2090,f748])).
% 14.03/2.38 fof(f2106,plain,(
% 14.03/2.38 $false),
% 14.03/2.38 inference(backward_subsumption_resolution,[status(thm)],[f152,f2103])).
% 14.03/2.38 % SZS output end CNFRefutation for theBenchmark.p
% 14.03/2.38 % Elapsed time: 2.012474 seconds
% 14.03/2.38 % CPU time: 15.455261 seconds
% 14.03/2.38 % Total memory used: 42.811 MB
% 14.03/2.38 % Net memory used: 39.062 MB
%------------------------------------------------------------------------------