%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO646-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:42 PM UTC 2026
% Result : Unsatisfiable 1.87s 0.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO646-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 12:07:55 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.23/0.49 % Drodi V4.1.1
% 1.87/0.81 % Refutation found
% 1.87/0.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.87/0.81 % SZS output start CNFRefutation for theBenchmark
% 1.87/0.81 fof(f31,axiom,(
% 1.87/0.81 (![E,B_2,B_1,A_0,B_0,B]: (( ~ 'E'('0',f(suc(suc(suc(B_2)))))| ~ 'E'(f(B_2),f(suc(suc(B_2))))| ~ 'E'(f(B_1),f(suc(B_1)))| ~ iLEQ(suc(B_1),suc(B_2))| ~ 'E'('0',f(suc(suc(A_0))))| ~ iLEQ(suc(B_0),suc(B_1))| ~ 'E'('0',f(B_1))| ~ 'E'('0',f(suc(suc(B_0))))| ~ 'E'('0',f(suc(suc(suc(B_0)))))| ~ 'E'(f(B_0),f(suc(B_0)))| ~ 'E'('0',f(suc(suc(suc(B)))))| ~ 'E'(f(B),f(suc(B)))| ~ iLEQ(suc(A_0),suc(B))| ~ 'E'(f(A_0),f(suc(suc(A_0))))| ~ 'E'('0',f(suc(B_0)))| ~ 'E'('0',f(suc(B_2)))| ~ 'E'('0',f(suc(suc(suc(A_0)))))| ~ 'E'(f(B_2),f(suc(B_2)))| ~ 'E'(f(A_0),f(suc(A_0)))| ~ 'E'('0',f(B_0))| ~ 'E'('0',f(B_2))| ~ 'E'('0',f(suc(A_0)))| ~ 'E'('0',f(B))| ~ 'E'('0',f(suc(suc(B))))| ~ 'E'(f(B),f(suc(suc(B))))| ~ 'E'('0',f(suc(suc(suc(B_1)))))| ~ 'E'('0',f(suc(B)))| ~ 'E'('0',f(suc(B_1)))| ~ 'E'('0',f(suc(suc(B_2))))| ~ 'E'('0',f(suc(suc(B_1))))| ~ 'E'('0',f(A_0))| ~ 'E'(f(B_0),f(suc(suc(B_0))))| ~ iLEQ(suc(B),suc(B_0))| ~ 'E'(f(B_1),f(suc(suc(B_1)))) ) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f93,axiom,(
% 1.87/0.81 (![E,A_0]: (( ~ 'E'('0',f(suc(suc(A_0))))| ~ 'E'(f(A_0),f(suc(suc(A_0))))| ~ 'E'('0',f(suc(suc(suc(A_0)))))| ~ 'E'(f(A_0),f(suc(A_0)))| ~ 'E'('0',f(suc(A_0)))| ~ 'E'('0',f(A_0))| iLEQ(suc(A_0),suc(A_0)) ) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f116,axiom,(
% 1.87/0.81 (![E,B_1,B_2,A_0,B_0,B]: (( ~ 'E'(f(B_1),f(suc(B_1)))| ~ iLEQ(suc(B_1),suc(B_2))| ~ 'E'('0',f(suc(suc(A_0))))| ~ iLEQ(suc(B_0),suc(B_1))| ~ 'E'('0',f(B_1))| ~ 'E'('0',f(suc(suc(B_0))))| ~ 'E'(f(B_0),f(suc(B_0)))| ~ 'E'(f(B),f(suc(B)))| ~ iLEQ(suc(A_0),suc(B))| ~ 'E'('0',f(suc(B_0)))| ~ 'E'('0',f(suc(B_2)))| ~ 'E'(f(B_2),f(suc(B_2)))| ~ 'E'(f(A_0),f(suc(A_0)))| ~ 'E'('0',f(B_0))| ~ 'E'('0',f(B_2))| ~ 'E'('0',f(suc(A_0)))| ~ 'E'('0',f(B))| ~ 'E'('0',f(suc(suc(B))))| ~ 'E'('0',f(suc(B)))| ~ 'E'('0',f(suc(B_1)))| ~ 'E'('0',f(suc(suc(B_2))))| ~ 'E'('0',f(suc(suc(B_1))))| ~ 'E'('0',f(A_0))| ~ iLEQ(suc(B),suc(B_0))| 'E'(f(B_2),f(suc(suc(B_2))))| 'E'(f(A_0),f(suc(suc(A_0))))| 'E'(f(B),f(suc(suc(B))))| 'E'(f(B_0),f(suc(suc(B_0))))| 'E'(f(B_1),f(suc(suc(B_1)))) ) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f124,axiom,(
% 1.87/0.81 (![E,A_0]: (( ~ 'E'('0',f(A_0))| ~ 'E'('0',f(suc(A_0)))| 'E'(f(A_0),f(suc(A_0)))| iLEQ(suc(A_0),suc(A_0)) ) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f137,axiom,(
% 1.87/0.81 (![E,A]: ('E'('0',f(A)) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f151,axiom,(
% 1.87/0.81 (![E,A_0]: (( ~ 'E'('0',f(suc(suc(A_0))))| ~ 'E'('0',f(suc(A_0)))| ~ 'E'(f(A_0),f(suc(A_0)))| ~ 'E'('0',f(A_0))| 'E'(f(A_0),f(suc(suc(A_0))))| iLEQ(suc(A_0),suc(A_0)) ) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f243,axiom,(
% 1.87/0.81 (![B_1,B_2,B_0,E,A_0,B]: (( ~ iLEQ(suc(B_1),suc(B_2))| ~ iLEQ(suc(B_0),suc(B_1))| ~ 'E'('0',f(B_1))| ~ iLEQ(suc(A_0),suc(B))| ~ 'E'('0',f(suc(B_0)))| ~ 'E'('0',f(suc(B_2)))| ~ 'E'('0',f(B_0))| ~ 'E'('0',f(B_2))| ~ 'E'('0',f(suc(A_0)))| ~ 'E'('0',f(B))| ~ 'E'('0',f(suc(B)))| ~ 'E'('0',f(suc(B_1)))| ~ 'E'('0',f(A_0))| ~ iLEQ(suc(B),suc(B_0))| 'E'(f(B_1),f(suc(B_1)))| 'E'(f(B_0),f(suc(B_0)))| 'E'(f(B),f(suc(B)))| 'E'(f(B_2),f(suc(B_2)))| 'E'(f(A_0),f(suc(A_0))) ) ))),
% 1.87/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.87/0.81 fof(f308,plain,(
% 1.87/0.81 ![B_1]: ((![B_0,B]: (((![A_0]: (((![B_2]: ((((((((((((((((((((((((((((~'E'('0',f(suc(suc(suc(B_2)))))|~'E'(f(B_2),f(suc(suc(B_2)))))|~'E'(f(B_1),f(suc(B_1))))|~iLEQ(suc(B_1),suc(B_2)))|~'E'('0',f(suc(suc(A_0)))))|~iLEQ(suc(B_0),suc(B_1)))|~'E'('0',f(B_1)))|~'E'('0',f(suc(suc(B_0)))))|~'E'('0',f(suc(suc(suc(B_0))))))|~'E'(f(B_0),f(suc(B_0))))|~'E'('0',f(suc(suc(suc(B))))))|~'E'(f(B),f(suc(B))))|~iLEQ(suc(A_0),suc(B)))|~'E'(f(A_0),f(suc(suc(A_0)))))|~'E'('0',f(suc(B_0))))|~'E'('0',f(suc(B_2))))|~'E'('0',f(suc(suc(suc(A_0))))))|~'E'(f(B_2),f(suc(B_2))))|~'E'(f(A_0),f(suc(A_0))))|~'E'('0',f(B_0)))|~'E'('0',f(B_2)))|~'E'('0',f(suc(A_0))))|~'E'('0',f(B)))|~'E'('0',f(suc(suc(B)))))|~'E'(f(B),f(suc(suc(B)))))|~'E'('0',f(suc(suc(suc(B_1))))))|~'E'('0',f(suc(B))))|~'E'('0',f(suc(B_1))))|~'E'('0',f(suc(suc(B_2))))))|~'E'('0',f(suc(suc(B_1)))))|~'E'('0',f(A_0))))|~'E'(f(B_0),f(suc(suc(B_0)))))|~iLEQ(suc(B),suc(B_0))))|~'E'(f(B_1),f(suc(suc(B_1)))))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f31])).
% 1.87/0.81 fof(f309,plain,(
% 1.87/0.81 ![E,X0,X1,X2,X3,X4]: (~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X4)))))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X4),f(suc(suc(X4))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'(f(X3),f(suc(suc(X3))))|~iLEQ(suc(X4),suc(X3))|~'E'(f(X1),f(suc(suc(X1)))))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f308])).
% 1.87/0.81 fof(f432,plain,(
% 1.87/0.81 ![A_0]: ((((((~'E'('0',f(suc(suc(A_0))))|~'E'(f(A_0),f(suc(suc(A_0)))))|~'E'('0',f(suc(suc(suc(A_0))))))|~'E'(f(A_0),f(suc(A_0))))|~'E'('0',f(suc(A_0))))|~'E'('0',f(A_0)))|iLEQ(suc(A_0),suc(A_0)))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f93])).
% 1.87/0.81 fof(f433,plain,(
% 1.87/0.81 ![E,X0]: (~'E'('0',f(suc(suc(X0))))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f432])).
% 1.87/0.81 fof(f478,plain,(
% 1.87/0.81 ![B_1]: ((![B_0]: ((![B]: ((![A_0]: ((![B_2]: ((((((((((((((((((((((((~'E'(f(B_1),f(suc(B_1)))|~iLEQ(suc(B_1),suc(B_2)))|~'E'('0',f(suc(suc(A_0)))))|~iLEQ(suc(B_0),suc(B_1)))|~'E'('0',f(B_1)))|~'E'('0',f(suc(suc(B_0)))))|~'E'(f(B_0),f(suc(B_0))))|~'E'(f(B),f(suc(B))))|~iLEQ(suc(A_0),suc(B)))|~'E'('0',f(suc(B_0))))|~'E'('0',f(suc(B_2))))|~'E'(f(B_2),f(suc(B_2))))|~'E'(f(A_0),f(suc(A_0))))|~'E'('0',f(B_0)))|~'E'('0',f(B_2)))|~'E'('0',f(suc(A_0))))|~'E'('0',f(B)))|~'E'('0',f(suc(suc(B)))))|~'E'('0',f(suc(B))))|~'E'('0',f(suc(B_1))))|~'E'('0',f(suc(suc(B_2)))))|~'E'('0',f(suc(suc(B_1)))))|~'E'('0',f(A_0)))|~iLEQ(suc(B),suc(B_0)))|'E'(f(B_2),f(suc(suc(B_2))))))|'E'(f(A_0),f(suc(suc(A_0))))))|'E'(f(B),f(suc(suc(B))))))|'E'(f(B_0),f(suc(suc(B_0))))))|'E'(f(B_1),f(suc(suc(B_1)))))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f116])).
% 1.87/0.81 fof(f479,plain,(
% 1.87/0.81 ![E,X0,X1,X2,X3,X4]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~iLEQ(suc(X4),suc(X3))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X4),f(suc(suc(X4))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f478])).
% 1.87/0.81 fof(f494,plain,(
% 1.87/0.81 ![A_0]: (((~'E'('0',f(A_0))|~'E'('0',f(suc(A_0))))|'E'(f(A_0),f(suc(A_0))))|iLEQ(suc(A_0),suc(A_0)))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f124])).
% 1.87/0.81 fof(f495,plain,(
% 1.87/0.81 ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f494])).
% 1.87/0.81 fof(f520,plain,(
% 1.87/0.81 ![A]: 'E'('0',f(A))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f137])).
% 1.87/0.81 fof(f521,plain,(
% 1.87/0.81 ![E,X0]: ('E'('0',f(X0)))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f520])).
% 1.87/0.81 fof(f548,plain,(
% 1.87/0.81 ![A_0]: (((((~'E'('0',f(suc(suc(A_0))))|~'E'('0',f(suc(A_0))))|~'E'(f(A_0),f(suc(A_0))))|~'E'('0',f(A_0)))|'E'(f(A_0),f(suc(suc(A_0)))))|iLEQ(suc(A_0),suc(A_0)))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f151])).
% 1.87/0.81 fof(f549,plain,(
% 1.87/0.81 ![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)))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f548])).
% 1.87/0.81 fof(f732,plain,(
% 1.87/0.81 ![A_0]: ((![B_2]: ((![B]: ((![B_0]: ((![B_1]: ((((((((((((((~iLEQ(suc(B_1),suc(B_2))|~iLEQ(suc(B_0),suc(B_1)))|~'E'('0',f(B_1)))|~iLEQ(suc(A_0),suc(B)))|~'E'('0',f(suc(B_0))))|~'E'('0',f(suc(B_2))))|~'E'('0',f(B_0)))|~'E'('0',f(B_2)))|~'E'('0',f(suc(A_0))))|~'E'('0',f(B)))|~'E'('0',f(suc(B))))|~'E'('0',f(suc(B_1))))|~'E'('0',f(A_0)))|~iLEQ(suc(B),suc(B_0)))|'E'(f(B_1),f(suc(B_1)))))|'E'(f(B_0),f(suc(B_0)))))|'E'(f(B),f(suc(B)))))|'E'(f(B_2),f(suc(B_2)))))|'E'(f(A_0),f(suc(A_0))))),
% 1.87/0.81 inference(miniscoping,[status(thm)],[f243])).
% 1.87/0.81 fof(f733,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3,X4]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X0))|~iLEQ(suc(X3),suc(X4))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X4))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X3))|~iLEQ(suc(X4),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X4),f(suc(X4)))|'E'(f(X1),f(suc(X1)))|'E'(f(X3),f(suc(X3))))),
% 1.87/0.81 inference(cnf_transformation,[status(thm)],[f732])).
% 1.87/0.81 fof(f742,plain,(
% 1.87/0.81 ![E,X0]: (~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f495,f521])).
% 1.87/0.81 fof(f743,plain,(
% 1.87/0.81 ![E,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)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f549,f521])).
% 1.87/0.81 fof(f745,plain,(
% 1.87/0.81 ![E,X0]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f433,f521])).
% 1.87/0.81 fof(f746,plain,(
% 1.87/0.81 ![E,X0]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(resolution,[status(thm)],[f745,f521])).
% 1.87/0.81 fof(f749,plain,(
% 1.87/0.81 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f746,f743])).
% 1.87/0.81 fof(f752,plain,(
% 1.87/0.81 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f749,f742])).
% 1.87/0.81 fof(f753,plain,(
% 1.87/0.81 ![E,X0]: (~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(resolution,[status(thm)],[f752,f521])).
% 1.87/0.81 fof(f754,plain,(
% 1.87/0.81 ![X0]: (iLEQ(suc(X0),suc(X0)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f753,f521])).
% 1.87/0.81 fof(f765,plain,(
% 1.87/0.81 ![X0,X1,X2,X3,X4,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X3),suc(X4))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X4))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X3))|~iLEQ(suc(X4),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X4),f(suc(X4)))|'E'(f(X1),f(suc(X1)))|'E'(f(X3),f(suc(X3))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f733,f521])).
% 1.87/0.81 fof(f766,plain,(
% 1.87/0.81 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X3),suc(X3))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~'E'('0',f(X3))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1)))|'E'(f(X3),f(suc(X3))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f765,f521])).
% 1.87/0.81 fof(f770,plain,(
% 1.87/0.81 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X3),suc(X3))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(duplicate_literals_removal,[status(thm)],[f766])).
% 1.87/0.81 fof(f771,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f770,f754])).
% 1.87/0.81 fof(f775,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f771,f521])).
% 1.87/0.81 fof(f776,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f775,f521])).
% 1.87/0.81 fof(f777,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f776,f521])).
% 1.87/0.81 fof(f778,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X3))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f777,f521])).
% 1.87/0.81 fof(f779,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X3))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f778,f521])).
% 1.87/0.81 fof(f780,plain,(
% 1.87/0.81 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X3),suc(X2))|'E'(f(X0),f(suc(X0)))|'E'(f(X2),f(suc(X2)))|'E'(f(X3),f(suc(X3)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f779,f521])).
% 1.87/0.81 fof(f781,plain,(
% 1.87/0.81 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f780,f754])).
% 1.87/0.81 fof(f784,plain,(
% 1.87/0.81 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|'E'(f(X0),f(suc(X0)))|'E'(f(X1),f(suc(X1))))),
% 1.87/0.81 inference(duplicate_literals_removal,[status(thm)],[f781])).
% 1.87/0.81 fof(f789,plain,(
% 1.87/0.81 ![E,X0]: ('E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f784,f754])).
% 1.87/0.81 fof(f791,plain,(
% 1.87/0.81 ![E,X0]: ('E'(f(X0),f(suc(X0))))),
% 1.87/0.81 inference(duplicate_literals_removal,[status(thm)],[f789])).
% 1.87/0.81 fof(f798,plain,(
% 1.87/0.81 ![E,X0,X1,X2,X3,X4]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X4)))))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X4),f(suc(suc(X4))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'(f(X3),f(suc(suc(X3))))|~iLEQ(suc(X4),suc(X3))|~'E'(f(X1),f(suc(suc(X1)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f309,f521])).
% 1.87/0.81 fof(f800,plain,(
% 1.87/0.81 ![X0,X1,E,X2,X3,X4]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X3))))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~iLEQ(suc(X4),suc(X3))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X4),f(suc(suc(X4))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f479,f791])).
% 1.87/0.81 fof(f801,plain,(
% 1.87/0.81 ![X0,X1,E,X2,X3]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X0))|~'E'(f(X3),f(suc(X3)))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~iLEQ(suc(X3),suc(X3))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f800,f521])).
% 1.87/0.81 fof(f804,plain,(
% 1.87/0.81 ![X0,X1,E,X2,X3]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X0))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~iLEQ(suc(X3),suc(X3))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(duplicate_literals_removal,[status(thm)],[f801])).
% 1.87/0.81 fof(f805,plain,(
% 1.87/0.81 ![X0,X1,E,X2,X3]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X0))|~'E'(f(X3),f(suc(X3)))|~iLEQ(suc(X2),suc(X3))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f804,f754])).
% 1.87/0.81 fof(f809,plain,(
% 1.87/0.81 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(X0))|~'E'(f(X2),f(suc(X2)))|~iLEQ(suc(X3),suc(X2))|~'E'('0',f(suc(X2)))|~'E'('0',f(suc(X1)))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X3))|'E'(f(X1),f(suc(suc(X1))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X2),f(suc(suc(X2))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f805,f521])).
% 1.87/0.81 fof(f810,plain,(
% 1.87/0.81 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(X0))|~'E'('0',f(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(suc(X0))))|'E'(f(X0),f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f809,f521])).
% 1.87/0.81 fof(f828,plain,(
% 1.87/0.81 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(duplicate_literals_removal,[status(thm)],[f810])).
% 1.87/0.81 fof(f829,plain,(
% 1.87/0.81 ![E,X0]: (~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f828,f754])).
% 1.87/0.81 fof(f853,plain,(
% 1.87/0.81 ![E,X0,X1,X2,X3,X4]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X4)))))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X4),f(suc(suc(X4))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'(f(X3),f(suc(suc(X3))))|~iLEQ(suc(X4),suc(X3)))),
% 1.87/0.81 inference(backward_subsumption_resolution,[status(thm)],[f798,f854])).
% 1.87/0.81 fof(f854,plain,(
% 1.87/0.81 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f829,f521])).
% 1.87/0.81 fof(f855,plain,(
% 1.87/0.81 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(resolution,[status(thm)],[f854,f521])).
% 1.87/0.81 fof(f856,plain,(
% 1.87/0.81 ![E,X0,X1,X2,X3,X4]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X4)))))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X0),f(suc(X0)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X4),f(suc(suc(X4))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X2))|~iLEQ(suc(X4),suc(X3)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f853,f854])).
% 1.87/0.81 fof(f857,plain,(
% 1.87/0.81 ![E,X0]: ('E'(f(X0),f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f855,f791])).
% 1.87/0.81 fof(f858,plain,(
% 1.87/0.81 ![E,X0,X1,X2,X3,X4]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X2))))|~iLEQ(suc(X3),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X3))))|~'E'('0',f(suc(suc(suc(X3)))))|~'E'(f(X3),f(suc(X3)))|~'E'('0',f(suc(suc(suc(X4)))))|~'E'(f(X4),f(suc(X4)))|~iLEQ(suc(X2),suc(X4))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X1),f(suc(X1)))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X4),f(suc(suc(X4))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X2))|~iLEQ(suc(X4),suc(X3)))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f856,f857])).
% 1.87/0.81 fof(f867,plain,(
% 1.87/0.81 ![E,X0,X1]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X1))|~iLEQ(suc(X1),suc(X1)))),
% 1.87/0.81 inference(resolution,[status(thm)],[f858,f791])).
% 1.87/0.81 fof(f918,plain,(
% 1.87/0.81 ![E,X0,X1]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 1.87/0.81 inference(duplicate_literals_removal,[status(thm)],[f867])).
% 1.87/0.81 fof(f919,plain,(
% 1.87/0.81 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X1)))))|~iLEQ(suc(X1),suc(X1))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 1.87/0.81 inference(forward_subsumption_resolution,[status(thm)],[f918,f791])).
% 1.87/0.81 fof(f976,plain,(
% 1.87/0.81 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X1),f(suc(suc(X1))))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 1.74/0.81 inference(forward_subsumption_resolution,[status(thm)],[f919,f754])).
% 1.74/0.81 fof(f977,plain,(
% 1.74/0.81 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 1.74/0.81 inference(resolution,[status(thm)],[f976,f521])).
% 1.74/0.81 fof(f980,plain,(
% 1.74/0.81 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X0))))),
% 1.74/0.81 inference(duplicate_literals_removal,[status(thm)],[f977])).
% 1.74/0.81 fof(f981,plain,(
% 1.74/0.81 ![E,X0]: (~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X0))))),
% 1.74/0.81 inference(forward_subsumption_resolution,[status(thm)],[f980,f754])).
% 1.74/0.81 fof(f984,plain,(
% 1.74/0.81 ![E,X0]: (~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0))))|~'E'('0',f(suc(X0))))),
% 1.74/0.81 inference(forward_subsumption_resolution,[status(thm)],[f981,f521])).
% 1.74/0.81 fof(f985,plain,(
% 1.74/0.81 ![E,X0]: (~'E'('0',f(X0))|~'E'(f(X0),f(suc(suc(X0)))))),
% 1.74/0.81 inference(resolution,[status(thm)],[f984,f521])).
% 1.74/0.81 fof(f986,plain,(
% 1.74/0.81 ![E,X0]: (~'E'(f(X0),f(suc(suc(X0)))))),
% 1.74/0.81 inference(forward_subsumption_resolution,[status(thm)],[f985,f521])).
% 1.74/0.81 fof(f987,plain,(
% 1.74/0.81 $false),
% 1.74/0.81 inference(forward_subsumption_resolution,[status(thm)],[f986,f857])).
% 1.74/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 1.74/0.82 % Elapsed time: 0.454653 seconds
% 1.74/0.82 % CPU time: 2.510927 seconds
% 1.74/0.82 % Total memory used: 67.636 MB
% 1.74/0.82 % Net memory used: 65.148 MB
%------------------------------------------------------------------------------