%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO689-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:44:46 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO689-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.07/0.35 % Computer : n018.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 12:10:59 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.65 % Refutation found
% 0.12/0.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.65 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.65 fof(f1,axiom,(
% 0.12/0.65 (![E,A_1]: (( ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| iLEQ(suc(A_1),suc(A_1)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f2,axiom,(
% 0.12/0.65 (![E,A_3]: (( ~ 'E'(s(s('0')),f(A_3))| ~ 'E'(s(s('0')),f(suc(A_3)))| iLEQ(suc(A_3),suc(A_3)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f3,axiom,(
% 0.12/0.65 (![E,B_1137,B_1140,B_1139,B_1138,B_1141,A_4]: (( ~ 'E'(s('0'),f(suc(B_1137)))| ~ 'E'(s('0'),f(B_1140))| ~ 'E'(s('0'),f(suc(B_1139)))| ~ iLEQ(suc(B_1138),suc(B_1139))| ~ 'E'(s('0'),f(B_1141))| ~ 'E'(s('0'),f(B_1137))| ~ 'E'(s('0'),f(suc(B_1138)))| ~ iLEQ(suc(B_1137),suc(B_1138))| ~ iLEQ(suc(A_4),suc(B_1137))| ~ iLEQ(suc(B_1139),suc(B_1140))| ~ 'E'(s('0'),f(suc(B_1140)))| ~ iLEQ(suc(B_1140),suc(B_1141))| ~ 'E'(s('0'),f(suc(A_4)))| ~ 'E'(s('0'),f(suc(B_1141)))| ~ 'E'(s('0'),f(B_1139))| ~ 'E'(s('0'),f(A_4))| ~ 'E'(s('0'),f(B_1138)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f4,axiom,(
% 0.12/0.65 (![LE,A]: ('LE'(f(A),s(s(s(s(s('0')))))) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f5,axiom,(
% 0.12/0.65 (![LE,B_1136,E]: (( ~ 'LE'(f(B_1136),s(s('0')))| 'E'(s('0'),f(B_1136))| 'LE'(f(B_1136),s('0')) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f6,axiom,(
% 0.12/0.65 (![LE,B_1066,E]: (( ~ 'LE'(f(suc(B_1066)),s(s(s('0'))))| 'E'(s(s('0')),f(suc(B_1066)))| 'LE'(f(B_1066),s(s('0'))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f7,axiom,(
% 0.12/0.65 (![E,B_907,A_2,B_911,B_910,B_909,B_908]: (( ~ 'E'(s(s(s('0'))),f(B_907))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| ~ 'E'(s(s(s('0'))),f(B_911))| ~ 'E'(s(s(s('0'))),f(B_910))| ~ iLEQ(suc(B_909),suc(B_910))| ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(B_910)))| ~ 'E'(s(s(s('0'))),f(B_908))| ~ iLEQ(suc(A_2),suc(B_907))| ~ iLEQ(suc(B_908),suc(B_909))| ~ 'E'(s(s(s('0'))),f(suc(B_908)))| ~ 'E'(s(s(s('0'))),f(B_909))| ~ 'E'(s(s(s('0'))),f(suc(B_911)))| ~ 'E'(s(s(s('0'))),f(suc(B_907)))| ~ iLEQ(suc(B_910),suc(B_911))| ~ iLEQ(suc(B_907),suc(B_908))| ~ 'E'(s(s(s('0'))),f(suc(B_909))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f8,axiom,(
% 0.12/0.65 (![LE,B_1161,E]: (( ~ 'LE'(f(B_1161),s('0'))| 'E'('0',f(B_1161))| 'LE'(f(B_1161),'0') ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f9,axiom,(
% 0.12/0.65 (![LE,B_1066,E]: (( ~ 'LE'(f(B_1066),s(s(s('0'))))| 'E'(s(s('0')),f(B_1066))| 'LE'(f(B_1066),s(s('0'))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f10,axiom,(
% 0.12/0.65 (![E,A_5]: (( ~ 'E'('0',f(A_5))| ~ 'E'('0',f(suc(A_5)))| iLEQ(suc(A_5),suc(A_5)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f11,axiom,(
% 0.12/0.65 (![LE]: (~ 'LE'(f(z),'0') ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f12,axiom,(
% 0.12/0.65 (![LE,B_906,E]: (( ~ 'LE'(f(B_906),s(s(s(s('0')))))| 'E'(s(s(s('0'))),f(B_906))| 'LE'(f(B_906),s(s(s('0')))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f13,axiom,(
% 0.12/0.65 (![E,B_1165,B_1162,B_1163,A_5,B_1164,B_1166]: (( ~ 'E'('0',f(B_1165))| ~ iLEQ(suc(B_1162),suc(B_1163))| ~ 'E'('0',f(suc(B_1163)))| ~ iLEQ(suc(A_5),suc(B_1162))| ~ 'E'('0',f(A_5))| ~ 'E'('0',f(B_1162))| ~ 'E'('0',f(B_1164))| ~ 'E'('0',f(suc(A_5)))| ~ 'E'('0',f(suc(B_1166)))| ~ 'E'('0',f(B_1166))| ~ iLEQ(suc(B_1165),suc(B_1166))| ~ iLEQ(suc(B_1163),suc(B_1164))| ~ 'E'('0',f(suc(B_1165)))| ~ 'E'('0',f(suc(B_1164)))| ~ 'E'('0',f(suc(B_1162)))| ~ iLEQ(suc(B_1164),suc(B_1165))| ~ 'E'('0',f(B_1163)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f14,axiom,(
% 0.12/0.65 (![E,B_588,B_586,B_587,B_589,B_590,A_1]: (( ~ 'E'(s(s(s(s('0')))),f(B_588))| ~ 'E'(s(s(s(s('0')))),f(suc(B_588)))| ~ iLEQ(suc(B_586),suc(B_587))| ~ iLEQ(suc(B_588),suc(B_589))| ~ 'E'(s(s(s(s('0')))),f(suc(B_587)))| ~ 'E'(s(s(s(s('0')))),f(B_589))| ~ 'E'(s(s(s(s('0')))),f(B_590))| ~ iLEQ(suc(B_587),suc(B_588))| ~ 'E'(s(s(s(s('0')))),f(B_586))| ~ iLEQ(suc(B_589),suc(B_590))| ~ 'E'(s(s(s(s('0')))),f(suc(B_590)))| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))| ~ iLEQ(suc(A_1),suc(B_586))| ~ 'E'(s(s(s(s('0')))),f(suc(B_586)))| ~ 'E'(s(s(s(s('0')))),f(A_1))| ~ 'E'(s(s(s(s('0')))),f(suc(B_589)))| ~ 'E'(s(s(s(s('0')))),f(B_587)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f15,axiom,(
% 0.12/0.65 (![E,A_4]: (( ~ 'E'(s('0'),f(A_4))| ~ 'E'(s('0'),f(suc(A_4)))| iLEQ(suc(A_4),suc(A_4)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f16,axiom,(
% 0.12/0.65 (![LE,B_906,E]: (( ~ 'LE'(f(suc(B_906)),s(s(s(s('0')))))| 'E'(s(s(s('0'))),f(suc(B_906)))| 'LE'(f(B_906),s(s(s('0')))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f17,axiom,(
% 0.12/0.65 (![LE,B_585,E]: (( ~ 'LE'(f(B_585),s(s(s(s(s('0'))))))| 'E'(s(s(s(s('0')))),f(B_585))| 'LE'(f(B_585),s(s(s(s('0'))))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f18,axiom,(
% 0.12/0.65 (![E,A_2]: (( ~ 'E'(s(s(s('0'))),f(A_2))| ~ 'E'(s(s(s('0'))),f(suc(A_2)))| iLEQ(suc(A_2),suc(A_2)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f19,axiom,(
% 0.12/0.65 (![LE,B_1136,E]: (( ~ 'LE'(f(suc(B_1136)),s(s('0')))| 'E'(s('0'),f(suc(B_1136)))| 'LE'(f(B_1136),s('0')) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f20,axiom,(
% 0.12/0.65 (![LE,B_585,E]: (( ~ 'LE'(f(suc(B_585)),s(s(s(s(s('0'))))))| 'E'(s(s(s(s('0')))),f(suc(B_585)))| 'LE'(f(B_585),s(s(s(s('0'))))) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f21,axiom,(
% 0.12/0.65 (![E,B_1069,B_1067,B_1070,B_1068,A_3,B_1071]: (( ~ 'E'(s(s('0')),f(B_1069))| ~ 'E'(s(s('0')),f(suc(B_1067)))| ~ 'E'(s(s('0')),f(B_1070))| ~ 'E'(s(s('0')),f(B_1068))| ~ 'E'(s(s('0')),f(suc(B_1068)))| ~ iLEQ(suc(B_1067),suc(B_1068))| ~ 'E'(s(s('0')),f(suc(A_3)))| ~ 'E'(s(s('0')),f(B_1067))| ~ iLEQ(suc(B_1068),suc(B_1069))| ~ 'E'(s(s('0')),f(B_1071))| ~ iLEQ(suc(A_3),suc(B_1067))| ~ 'E'(s(s('0')),f(suc(B_1069)))| ~ iLEQ(suc(B_1069),suc(B_1070))| ~ 'E'(s(s('0')),f(suc(B_1071)))| ~ 'E'(s(s('0')),f(suc(B_1070)))| ~ 'E'(s(s('0')),f(A_3))| ~ iLEQ(suc(B_1070),suc(B_1071)) ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f22,axiom,(
% 0.12/0.65 (![LE,B_1161,E]: (( ~ 'LE'(f(suc(B_1161)),s('0'))| 'E'('0',f(suc(B_1161)))| 'LE'(f(B_1161),'0') ) ))),
% 0.12/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.65 fof(f23,plain,(
% 0.12/0.65 ![A_1]: ((~'E'(s(s(s(s('0')))),f(A_1))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|iLEQ(suc(A_1),suc(A_1)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f1])).
% 0.12/0.65 fof(f24,plain,(
% 0.12/0.65 ![E,X0]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f23])).
% 0.12/0.65 fof(f25,plain,(
% 0.12/0.65 ![A_3]: ((~'E'(s(s('0')),f(A_3))|~'E'(s(s('0')),f(suc(A_3))))|iLEQ(suc(A_3),suc(A_3)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f2])).
% 0.12/0.65 fof(f26,plain,(
% 0.12/0.65 ![E,X0]: (~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.65 fof(f27,plain,(
% 0.12/0.65 ![B_1138]: ((![A_4]: ((![B_1139]: ((![B_1141]: (((![B_1140]: ((((![B_1137]: ((((((((~'E'(s('0'),f(suc(B_1137)))|~'E'(s('0'),f(B_1140)))|~'E'(s('0'),f(suc(B_1139))))|~iLEQ(suc(B_1138),suc(B_1139)))|~'E'(s('0'),f(B_1141)))|~'E'(s('0'),f(B_1137)))|~'E'(s('0'),f(suc(B_1138))))|~iLEQ(suc(B_1137),suc(B_1138)))|~iLEQ(suc(A_4),suc(B_1137))))|~iLEQ(suc(B_1139),suc(B_1140)))|~'E'(s('0'),f(suc(B_1140))))|~iLEQ(suc(B_1140),suc(B_1141))))|~'E'(s('0'),f(suc(A_4))))|~'E'(s('0'),f(suc(B_1141)))))|~'E'(s('0'),f(B_1139))))|~'E'(s('0'),f(A_4))))|~'E'(s('0'),f(B_1138)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f3])).
% 0.12/0.65 fof(f28,plain,(
% 0.12/0.65 ![E,X0,X1,X2,X3,X4,X5]: (~'E'(s('0'),f(suc(X0)))|~'E'(s('0'),f(X1))|~'E'(s('0'),f(suc(X2)))|~iLEQ(suc(X3),suc(X2))|~'E'(s('0'),f(X4))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X3)))|~iLEQ(suc(X0),suc(X3))|~iLEQ(suc(X5),suc(X0))|~iLEQ(suc(X2),suc(X1))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X1),suc(X4))|~'E'(s('0'),f(suc(X5)))|~'E'(s('0'),f(suc(X4)))|~'E'(s('0'),f(X2))|~'E'(s('0'),f(X5))|~'E'(s('0'),f(X3)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f27])).
% 0.12/0.65 fof(f29,plain,(
% 0.12/0.65 ![A]: 'LE'(f(A),s(s(s(s(s('0'))))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f4])).
% 0.12/0.65 fof(f30,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s(s(s(s('0')))))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f29])).
% 0.12/0.65 fof(f31,plain,(
% 0.12/0.65 ![B_1136]: ((~'LE'(f(B_1136),s(s('0')))|'E'(s('0'),f(B_1136)))|'LE'(f(B_1136),s('0')))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f5])).
% 0.12/0.65 fof(f32,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(X0),s(s('0')))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f31])).
% 0.12/0.65 fof(f33,plain,(
% 0.12/0.65 ![B_1066]: ((~'LE'(f(suc(B_1066)),s(s(s('0'))))|'E'(s(s('0')),f(suc(B_1066))))|'LE'(f(B_1066),s(s('0'))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f6])).
% 0.12/0.65 fof(f34,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s(s('0'))))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f33])).
% 0.12/0.65 fof(f35,plain,(
% 0.12/0.65 ![B_909]: ((![B_907,B_908]: ((![B_911,B_910]: (((((((![A_2]: ((((((((~'E'(s(s(s('0'))),f(B_907))|~'E'(s(s(s('0'))),f(suc(A_2))))|~'E'(s(s(s('0'))),f(B_911)))|~'E'(s(s(s('0'))),f(B_910)))|~iLEQ(suc(B_909),suc(B_910)))|~'E'(s(s(s('0'))),f(A_2)))|~'E'(s(s(s('0'))),f(suc(B_910))))|~'E'(s(s(s('0'))),f(B_908)))|~iLEQ(suc(A_2),suc(B_907))))|~iLEQ(suc(B_908),suc(B_909)))|~'E'(s(s(s('0'))),f(suc(B_908))))|~'E'(s(s(s('0'))),f(B_909)))|~'E'(s(s(s('0'))),f(suc(B_911))))|~'E'(s(s(s('0'))),f(suc(B_907))))|~iLEQ(suc(B_910),suc(B_911))))|~iLEQ(suc(B_907),suc(B_908))))|~'E'(s(s(s('0'))),f(suc(B_909))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f7])).
% 0.12/0.65 fof(f36,plain,(
% 0.12/0.65 ![E,X0,X1,X2,X3,X4,X5]: (~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(X3))|~iLEQ(suc(X4),suc(X3))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X3)))|~'E'(s(s(s('0'))),f(X5))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X5),suc(X4))|~'E'(s(s(s('0'))),f(suc(X5)))|~'E'(s(s(s('0'))),f(X4))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|~iLEQ(suc(X0),suc(X5))|~'E'(s(s(s('0'))),f(suc(X4))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f35])).
% 0.12/0.65 fof(f37,plain,(
% 0.12/0.65 ![B_1161]: ((~'LE'(f(B_1161),s('0'))|'E'('0',f(B_1161)))|'LE'(f(B_1161),'0'))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f8])).
% 0.12/0.65 fof(f38,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(X0),s('0'))|'E'('0',f(X0))|'LE'(f(X0),'0'))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.65 fof(f39,plain,(
% 0.12/0.65 ![B_1066]: ((~'LE'(f(B_1066),s(s(s('0'))))|'E'(s(s('0')),f(B_1066)))|'LE'(f(B_1066),s(s('0'))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f9])).
% 0.12/0.65 fof(f40,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(X0),s(s(s('0'))))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f39])).
% 0.12/0.65 fof(f41,plain,(
% 0.12/0.65 ![A_5]: ((~'E'('0',f(A_5))|~'E'('0',f(suc(A_5))))|iLEQ(suc(A_5),suc(A_5)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f10])).
% 0.12/0.65 fof(f42,plain,(
% 0.12/0.65 ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f41])).
% 0.12/0.65 fof(f43,plain,(
% 0.12/0.65 ![LE]: (~'LE'(f(z),'0'))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f11])).
% 0.12/0.65 fof(f44,plain,(
% 0.12/0.65 ![B_906]: ((~'LE'(f(B_906),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(B_906)))|'LE'(f(B_906),s(s(s('0')))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f12])).
% 0.12/0.65 fof(f45,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(X0),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.65 fof(f46,plain,(
% 0.12/0.65 ![B_1163]: ((![B_1165,B_1164]: ((![B_1162]: (((((![B_1166]: ((((![A_5]: (((((((~'E'('0',f(B_1165))|~iLEQ(suc(B_1162),suc(B_1163)))|~'E'('0',f(suc(B_1163))))|~iLEQ(suc(A_5),suc(B_1162)))|~'E'('0',f(A_5)))|~'E'('0',f(B_1162)))|~'E'('0',f(B_1164)))|~'E'('0',f(suc(A_5)))))|~'E'('0',f(suc(B_1166))))|~'E'('0',f(B_1166)))|~iLEQ(suc(B_1165),suc(B_1166))))|~iLEQ(suc(B_1163),suc(B_1164)))|~'E'('0',f(suc(B_1165))))|~'E'('0',f(suc(B_1164))))|~'E'('0',f(suc(B_1162)))))|~iLEQ(suc(B_1164),suc(B_1165))))|~'E'('0',f(B_1163)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f13])).
% 0.12/0.65 fof(f47,plain,(
% 0.12/0.65 ![E,X0,X1,X2,X3,X4,X5]: (~'E'('0',f(X0))|~iLEQ(suc(X1),suc(X2))|~'E'('0',f(suc(X2)))|~iLEQ(suc(X3),suc(X1))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(X4))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X5)))|~'E'('0',f(X5))|~iLEQ(suc(X0),suc(X5))|~iLEQ(suc(X2),suc(X4))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X4),suc(X0))|~'E'('0',f(X2)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f46])).
% 0.12/0.65 fof(f48,plain,(
% 0.12/0.65 ![B_587]: ((![B_589]: ((![A_1]: ((![B_586]: ((((![B_590]: ((((![B_588]: (((((((~'E'(s(s(s(s('0')))),f(B_588))|~'E'(s(s(s(s('0')))),f(suc(B_588))))|~iLEQ(suc(B_586),suc(B_587)))|~iLEQ(suc(B_588),suc(B_589)))|~'E'(s(s(s(s('0')))),f(suc(B_587))))|~'E'(s(s(s(s('0')))),f(B_589)))|~'E'(s(s(s(s('0')))),f(B_590)))|~iLEQ(suc(B_587),suc(B_588))))|~'E'(s(s(s(s('0')))),f(B_586)))|~iLEQ(suc(B_589),suc(B_590)))|~'E'(s(s(s(s('0')))),f(suc(B_590)))))|~'E'(s(s(s(s('0')))),f(suc(A_1))))|~iLEQ(suc(A_1),suc(B_586)))|~'E'(s(s(s(s('0')))),f(suc(B_586)))))|~'E'(s(s(s(s('0')))),f(A_1))))|~'E'(s(s(s(s('0')))),f(suc(B_589)))))|~'E'(s(s(s(s('0')))),f(B_587)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f14])).
% 0.12/0.65 fof(f49,plain,(
% 0.12/0.65 ![E,X0,X1,X2,X3,X4,X5]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X1),suc(X2))|~iLEQ(suc(X0),suc(X3))|~'E'(s(s(s(s('0')))),f(suc(X2)))|~'E'(s(s(s(s('0')))),f(X3))|~'E'(s(s(s(s('0')))),f(X4))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X3),suc(X4))|~'E'(s(s(s(s('0')))),f(suc(X4)))|~'E'(s(s(s(s('0')))),f(suc(X5)))|~iLEQ(suc(X5),suc(X1))|~'E'(s(s(s(s('0')))),f(suc(X1)))|~'E'(s(s(s(s('0')))),f(X5))|~'E'(s(s(s(s('0')))),f(suc(X3)))|~'E'(s(s(s(s('0')))),f(X2)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f48])).
% 0.12/0.65 fof(f50,plain,(
% 0.12/0.65 ![A_4]: ((~'E'(s('0'),f(A_4))|~'E'(s('0'),f(suc(A_4))))|iLEQ(suc(A_4),suc(A_4)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f15])).
% 0.12/0.65 fof(f51,plain,(
% 0.12/0.65 ![E,X0]: (~'E'(s('0'),f(X0))|~'E'(s('0'),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f50])).
% 0.12/0.65 fof(f52,plain,(
% 0.12/0.65 ![B_906]: ((~'LE'(f(suc(B_906)),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(B_906))))|'LE'(f(B_906),s(s(s('0')))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f16])).
% 0.12/0.65 fof(f53,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s(s(s('0')))))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f52])).
% 0.12/0.65 fof(f54,plain,(
% 0.12/0.65 ![B_585]: ((~'LE'(f(B_585),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(B_585)))|'LE'(f(B_585),s(s(s(s('0'))))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f17])).
% 0.12/0.65 fof(f55,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(X0),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(X0))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f54])).
% 0.12/0.65 fof(f56,plain,(
% 0.12/0.65 ![A_2]: ((~'E'(s(s(s('0'))),f(A_2))|~'E'(s(s(s('0'))),f(suc(A_2))))|iLEQ(suc(A_2),suc(A_2)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f18])).
% 0.12/0.65 fof(f57,plain,(
% 0.12/0.65 ![E,X0]: (~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/0.65 fof(f58,plain,(
% 0.12/0.65 ![B_1136]: ((~'LE'(f(suc(B_1136)),s(s('0')))|'E'(s('0'),f(suc(B_1136))))|'LE'(f(B_1136),s('0')))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f19])).
% 0.12/0.65 fof(f59,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s('0')))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.65 fof(f60,plain,(
% 0.12/0.65 ![B_585]: ((~'LE'(f(suc(B_585)),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(suc(B_585))))|'LE'(f(B_585),s(s(s(s('0'))))))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f20])).
% 0.12/0.65 fof(f61,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(suc(X0)),s(s(s(s(s('0'))))))|'E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f60])).
% 0.12/0.65 fof(f62,plain,(
% 0.12/0.65 ![B_1070,B_1071]: ((![A_3]: ((((![B_1069]: (((![B_1067]: (((![B_1068]: ((((((((~'E'(s(s('0')),f(B_1069))|~'E'(s(s('0')),f(suc(B_1067))))|~'E'(s(s('0')),f(B_1070)))|~'E'(s(s('0')),f(B_1068)))|~'E'(s(s('0')),f(suc(B_1068))))|~iLEQ(suc(B_1067),suc(B_1068)))|~'E'(s(s('0')),f(suc(A_3))))|~'E'(s(s('0')),f(B_1067)))|~iLEQ(suc(B_1068),suc(B_1069))))|~'E'(s(s('0')),f(B_1071)))|~iLEQ(suc(A_3),suc(B_1067))))|~'E'(s(s('0')),f(suc(B_1069))))|~iLEQ(suc(B_1069),suc(B_1070))))|~'E'(s(s('0')),f(suc(B_1071))))|~'E'(s(s('0')),f(suc(B_1070))))|~'E'(s(s('0')),f(A_3))))|~iLEQ(suc(B_1070),suc(B_1071)))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f21])).
% 0.12/0.65 fof(f63,plain,(
% 0.12/0.65 ![E,X0,X1,X2,X3,X4,X5]: (~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(suc(X1)))|~'E'(s(s('0')),f(X2))|~'E'(s(s('0')),f(X3))|~'E'(s(s('0')),f(suc(X3)))|~iLEQ(suc(X1),suc(X3))|~'E'(s(s('0')),f(suc(X4)))|~'E'(s(s('0')),f(X1))|~iLEQ(suc(X3),suc(X0))|~'E'(s(s('0')),f(X5))|~iLEQ(suc(X4),suc(X1))|~'E'(s(s('0')),f(suc(X0)))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X5)))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X4))|~iLEQ(suc(X2),suc(X5)))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/0.65 fof(f64,plain,(
% 0.12/0.65 ![B_1161]: ((~'LE'(f(suc(B_1161)),s('0'))|'E'('0',f(suc(B_1161))))|'LE'(f(B_1161),'0'))),
% 0.12/0.65 inference(miniscoping,[status(thm)],[f22])).
% 0.12/0.65 fof(f65,plain,(
% 0.12/0.65 ![LE,X0,E]: (~'LE'(f(suc(X0)),s('0'))|'E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 0.12/0.65 inference(cnf_transformation,[status(thm)],[f64])).
% 0.12/0.65 fof(f66,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s(s(s(s('0')))),f(X0))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f55,f30])).
% 0.12/0.65 fof(f68,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s(s(s(s('0')))),f(suc(X0)))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f61,f30])).
% 0.12/0.65 fof(f69,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(X0),s(s(s(s('0')))))|~'E'(s(s(s(s('0')))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(resolution,[status(thm)],[f68,f24])).
% 0.12/0.65 fof(f70,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s(s(s('0')))))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f69,f66])).
% 0.12/0.65 fof(f73,plain,(
% 0.12/0.65 ![X0,E,LE]: (iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f70,f53])).
% 0.12/0.65 fof(f74,plain,(
% 0.12/0.65 ![X0,E,LE]: (iLEQ(suc(X0),suc(X0))|'E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f70,f45])).
% 0.12/0.65 fof(f79,plain,(
% 0.12/0.65 ![E,X0,LE]: (~'E'(s(s(s('0'))),f(X0))|iLEQ(suc(X0),suc(X0))|iLEQ(suc(suc(X0)),suc(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f57,f73])).
% 0.12/0.65 fof(f84,plain,(
% 0.12/0.65 ![X0,LE]: (iLEQ(suc(X0),suc(X0))|iLEQ(suc(suc(X0)),suc(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f79,f74])).
% 0.12/0.65 fof(f450,plain,(
% 0.12/0.65 ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X1),suc(X1))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X1),suc(X1))|~iLEQ(suc(X1),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~'E'(s(s(s(s('0')))),f(X1))|'LE'(f(X1),s(s(s(s('0'))))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f49,f68])).
% 0.12/0.65 fof(f468,plain,(
% 0.12/0.65 ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X1),suc(X1))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s(s(s('0')))),f(X1))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s(s('0'))))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f450])).
% 0.12/0.65 fof(f469,plain,(
% 0.12/0.65 ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X1),suc(X1))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f468,f66])).
% 0.12/0.65 fof(f541,plain,(
% 0.12/0.65 ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(X0))|~'E'(s(s(s(s('0')))),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f469,f70])).
% 0.12/0.65 fof(f542,plain,(
% 0.12/0.65 ![E,X0,X1,LE]: (~'E'(s(s(s(s('0')))),f(X0))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f541,f68])).
% 0.12/0.65 fof(f544,plain,(
% 0.12/0.65 ![X0,X1,LE]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f542,f66])).
% 0.12/0.65 fof(f569,plain,(
% 0.12/0.65 ![X0,LE]: (~iLEQ(suc(suc(X0)),suc(suc(X0)))|'LE'(f(suc(X0)),s(s(s(s('0')))))|'LE'(f(suc(X0)),s(s(s(s('0')))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f544,f84])).
% 0.12/0.65 fof(f574,plain,(
% 0.12/0.65 ![X0,LE]: (~iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f544,f70])).
% 0.12/0.65 fof(f603,plain,(
% 0.12/0.65 ![X0,LE]: (~iLEQ(suc(suc(X0)),suc(suc(X0)))|'LE'(f(suc(X0)),s(s(s(s('0')))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f569])).
% 0.12/0.65 fof(f604,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(suc(X0)),s(s(s(s('0')))))|iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f603,f84])).
% 0.12/0.65 fof(f613,plain,(
% 0.12/0.65 ![X0,LE]: (~iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f574])).
% 0.12/0.65 fof(f614,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f613,f70])).
% 0.12/0.65 fof(f615,plain,(
% 0.12/0.65 ![X0,LE,E]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0'))))|'E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f604,f53])).
% 0.12/0.65 fof(f624,plain,(
% 0.12/0.65 ![X0,LE,E]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0'))))|'E'(s(s(s('0'))),f(suc(X0))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f615])).
% 0.12/0.65 fof(f652,plain,(
% 0.12/0.65 ![X0,LE,E]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(resolution,[status(thm)],[f624,f57])).
% 0.12/0.65 fof(f671,plain,(
% 0.12/0.65 ![X0,LE,E]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X0)))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f652])).
% 0.12/0.65 fof(f672,plain,(
% 0.12/0.65 ![X0,LE]: (iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f671,f74])).
% 0.12/0.65 fof(f673,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s(s('0')))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f672,f544])).
% 0.12/0.65 fof(f680,plain,(
% 0.12/0.65 ![X0,E,LE]: (iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f672,f34])).
% 0.12/0.65 fof(f681,plain,(
% 0.12/0.65 ![X0,E,LE]: (iLEQ(suc(X0),suc(X0))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f672,f40])).
% 0.12/0.65 fof(f682,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f673])).
% 0.12/0.65 fof(f683,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s(s('0'))))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f682,f672])).
% 0.12/0.65 fof(f693,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s(s(s('0'))),f(X0))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(backward_subsumption_resolution,[status(thm)],[f45,f683])).
% 0.12/0.65 fof(f781,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s(s(s('0'))),f(suc(X0)))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(backward_subsumption_resolution,[status(thm)],[f53,f614])).
% 0.12/0.65 fof(f782,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(s(s(s('0'))),f(X2))|~'E'(s(s(s('0'))),f(X0))|~iLEQ(suc(X2),suc(X1))|~iLEQ(suc(X0),suc(X0))|~'E'(s(s(s('0'))),f(X0))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X1),suc(X0)))),
% 0.12/0.65 inference(resolution,[status(thm)],[f781,f36])).
% 0.12/0.65 fof(f792,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(s(s(s('0'))),f(X2))|~iLEQ(suc(X2),suc(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0)))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f782])).
% 0.12/0.65 fof(f793,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~iLEQ(suc(X0),suc(X0))|~'E'(s(s(s('0'))),f(X2))|~iLEQ(suc(X2),suc(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0)))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f792,f693])).
% 0.12/0.65 fof(f875,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(suc(X2)))|~'E'(s(s(s('0'))),f(X2))|~iLEQ(suc(X2),suc(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0)))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f793,f672])).
% 0.12/0.65 fof(f876,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~'E'(s(s(s('0'))),f(X2))|~iLEQ(suc(X2),suc(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X2),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f875,f781])).
% 0.12/0.65 fof(f878,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~iLEQ(suc(X2),suc(X1))|~'E'(s(s(s('0'))),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X2),s(s(s('0')))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f876,f693])).
% 0.12/0.65 fof(f957,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~'E'(s(s(s('0'))),f(X1))|~iLEQ(suc(X2),suc(X1))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X2),s(s(s('0'))))|'LE'(f(X1),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f878,f781])).
% 0.12/0.65 fof(f959,plain,(
% 0.12/0.65 ![LE,X0,X1,X2]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X2))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X1),s(s(s('0'))))|'LE'(f(X2),s(s(s('0')))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f957,f693])).
% 0.12/0.65 fof(f971,plain,(
% 0.12/0.65 ![LE,X0,X1]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s('0'))))|'LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s('0')))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f959,f672])).
% 0.12/0.65 fof(f982,plain,(
% 0.12/0.65 ![LE,X0,X1]: ('LE'(f(X0),s(s(s('0'))))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X1),s(s(s('0')))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f971])).
% 0.12/0.65 fof(f989,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(suc(X0)),s(s(s('0'))))|'LE'(f(suc(X0)),s(s(s('0'))))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f982,f680])).
% 0.12/0.65 fof(f990,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|'LE'(f(X0),s(s(s('0'))))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f982,f681])).
% 0.12/0.65 fof(f998,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(suc(X0)),s(s(s('0'))))|'E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f989])).
% 0.12/0.65 fof(f999,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s(s('0')),f(suc(X0)))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f998,f34])).
% 0.12/0.65 fof(f1000,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(X0),s(s(s('0'))))|'E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f990])).
% 0.12/0.65 fof(f1001,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s(s('0')),f(X0))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1000,f40])).
% 0.12/0.65 fof(f1019,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X0))|~'E'(s(s('0')),f(X0))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X2))|~iLEQ(suc(X0),suc(X1))|~'E'(s(s('0')),f(X0))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(s(s('0')),f(X0))|~iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(resolution,[status(thm)],[f999,f63])).
% 0.12/0.65 fof(f1027,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(resolution,[status(thm)],[f999,f26])).
% 0.12/0.65 fof(f1029,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~'E'(s(s('0')),f(suc(X2)))|~'E'(s(s('0')),f(X0))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X2))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f1019])).
% 0.12/0.65 fof(f1030,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~'E'(s(s('0')),f(suc(X2)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X2))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1029,f1001])).
% 0.12/0.65 fof(f1041,plain,(
% 0.12/0.65 ![LE,X0]: ('LE'(f(X0),s(s('0')))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1027,f1001])).
% 0.12/0.65 fof(f1042,plain,(
% 0.12/0.65 ![X0,E,LE]: (iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1041,f59])).
% 0.12/0.65 fof(f1043,plain,(
% 0.12/0.65 ![X0,E,LE]: (iLEQ(suc(X0),suc(X0))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1041,f32])).
% 0.12/0.65 fof(f1225,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~'E'(s(s('0')),f(suc(X2)))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X2))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0)))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1030,f1041])).
% 0.12/0.65 fof(f1226,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~iLEQ(suc(X2),suc(X0))|~'E'(s(s('0')),f(X2))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X2),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1225,f999])).
% 0.12/0.65 fof(f1228,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X2))|~'E'(s(s('0')),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X2),s(s('0'))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1226,f1001])).
% 0.12/0.65 fof(f1236,plain,(
% 0.12/0.65 ![LE,X0,E,X1,X2]: ('LE'(f(X0),s(s('0')))|~'E'(s(s('0')),f(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X2))|~iLEQ(suc(X1),suc(X0))|'LE'(f(X2),s(s('0')))|'LE'(f(X1),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1228,f999])).
% 0.12/0.65 fof(f1238,plain,(
% 0.12/0.65 ![LE,X0,X1,X2]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X2))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|'LE'(f(X1),s(s('0')))|'LE'(f(X2),s(s('0'))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1236,f1001])).
% 0.12/0.65 fof(f1245,plain,(
% 0.12/0.65 ![LE,X0,X1]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s(s('0')))|'LE'(f(X0),s(s('0')))|'LE'(f(X0),s(s('0'))))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1238,f1041])).
% 0.12/0.65 fof(f1258,plain,(
% 0.12/0.65 ![LE,X0,X1]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s(s('0'))))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f1245])).
% 0.12/0.65 fof(f1259,plain,(
% 0.12/0.65 ![LE,X0,X1]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s(s('0'))))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1258,f1041])).
% 0.12/0.65 fof(f1264,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(suc(X0)),s(s('0')))|~iLEQ(suc(suc(X0)),suc(suc(X0)))|'LE'(f(suc(X0)),s(s('0')))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1259,f1042])).
% 0.12/0.65 fof(f1265,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s(s('0')))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(resolution,[status(thm)],[f1259,f1043])).
% 0.12/0.65 fof(f1275,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(suc(X0)),s(s('0')))|~iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f1264])).
% 0.12/0.65 fof(f1276,plain,(
% 0.12/0.65 ![X0,E,LE]: (~iLEQ(suc(suc(X0)),suc(suc(X0)))|'E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1275,f59])).
% 0.12/0.65 fof(f1277,plain,(
% 0.12/0.65 ![LE,X0,E]: ('LE'(f(X0),s(s('0')))|~iLEQ(suc(X0),suc(X0))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(duplicate_literals_removal,[status(thm)],[f1265])).
% 0.12/0.65 fof(f1278,plain,(
% 0.12/0.65 ![X0,E,LE]: (~iLEQ(suc(X0),suc(X0))|'E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1277,f32])).
% 0.12/0.65 fof(f1281,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s('0'),f(X0))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1278,f1043])).
% 0.12/0.65 fof(f1324,plain,(
% 0.12/0.65 ![E,X0,LE]: ('E'(s('0'),f(suc(X0)))|'LE'(f(X0),s('0')))),
% 0.12/0.65 inference(forward_subsumption_resolution,[status(thm)],[f1276,f1042])).
% 0.12/0.65 fof(f1326,plain,(
% 0.12/0.65 ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(X0))|~'E'(s('0'),f(X0)))),
% 0.12/0.66 inference(resolution,[status(thm)],[f1324,f28])).
% 0.12/0.66 fof(f1336,plain,(
% 0.12/0.66 ![LE,X0,E]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X0))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(resolution,[status(thm)],[f1324,f51])).
% 0.12/0.66 fof(f1339,plain,(
% 0.12/0.66 ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1)))),
% 0.12/0.66 inference(duplicate_literals_removal,[status(thm)],[f1326])).
% 0.12/0.66 fof(f1340,plain,(
% 0.12/0.66 ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(suc(X1)))|~iLEQ(suc(X0),suc(X0))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1)))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1339,f1281])).
% 0.12/0.66 fof(f1354,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),s('0'))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1336,f1281])).
% 0.12/0.66 fof(f1388,plain,(
% 0.12/0.66 ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(suc(X1)))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1)))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1340,f1354])).
% 0.12/0.66 fof(f1389,plain,(
% 0.12/0.66 ![LE,X0,E,X1]: ('LE'(f(X0),s('0'))|~'E'(s('0'),f(X1))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s('0')))),
% 0.12/0.66 inference(resolution,[status(thm)],[f1388,f1324])).
% 0.12/0.66 fof(f1391,plain,(
% 0.12/0.66 ![LE,X0,X1]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X1),suc(X0))|~iLEQ(suc(X0),suc(X1))|'LE'(f(X1),s('0')))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1389,f1281])).
% 0.12/0.66 fof(f1393,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X0),suc(X0))|'LE'(f(X0),s('0'))|'LE'(f(X0),s('0')))),
% 0.12/0.66 inference(resolution,[status(thm)],[f1391,f1354])).
% 0.12/0.66 fof(f1396,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),s('0'))|~iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(duplicate_literals_removal,[status(thm)],[f1393])).
% 0.12/0.66 fof(f1397,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),s('0')))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1396,f1354])).
% 0.12/0.66 fof(f1428,plain,(
% 0.12/0.66 ![E,X0,LE]: ('E'('0',f(suc(X0)))|'LE'(f(X0),'0'))),
% 0.12/0.66 inference(backward_subsumption_resolution,[status(thm)],[f65,f1397])).
% 0.12/0.66 fof(f1429,plain,(
% 0.12/0.66 ![E,X0,LE]: ('E'('0',f(X0))|'LE'(f(X0),'0'))),
% 0.12/0.66 inference(backward_subsumption_resolution,[status(thm)],[f38,f1397])).
% 0.12/0.66 fof(f1449,plain,(
% 0.12/0.66 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(X0))|~'E'('0',f(X0))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0)))),
% 0.12/0.66 inference(resolution,[status(thm)],[f1428,f47])).
% 0.12/0.66 fof(f1461,plain,(
% 0.12/0.66 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(resolution,[status(thm)],[f1428,f42])).
% 0.12/0.66 fof(f1462,plain,(
% 0.12/0.66 ![LE,X0,E]: ('LE'(f(X0),'0')|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(duplicate_literals_removal,[status(thm)],[f1449])).
% 0.12/0.66 fof(f1463,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),'0')|~iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1462,f1429])).
% 0.12/0.66 fof(f1480,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),'0')|iLEQ(suc(X0),suc(X0)))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1461,f1429])).
% 0.12/0.66 fof(f1528,plain,(
% 0.12/0.66 ![LE,X0]: ('LE'(f(X0),'0'))),
% 0.12/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1463,f1480])).
% 0.12/0.66 fof(f1529,plain,(
% 0.12/0.66 $false),
% 0.12/0.66 inference(backward_subsumption_resolution,[status(thm)],[f43,f1528])).
% 0.12/0.66 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.67 % Elapsed time: 0.305140 seconds
% 0.12/0.67 % CPU time: 2.254570 seconds
% 0.12/0.67 % Total memory used: 18.209 MB
% 0.12/0.67 % Net memory used: 16.777 MB
%------------------------------------------------------------------------------