%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO647-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 : n012.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 6.55s 1.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO647-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 : n012.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:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.55/0.80 % Drodi V4.1.1
% 6.55/1.70 % Refutation found
% 6.55/1.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.55/1.70 % SZS output start CNFRefutation for theBenchmark
% 6.55/1.70 fof(f11,axiom,(
% 6.55/1.70 (![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)) ) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f91,axiom,(
% 6.55/1.70 (![E,A]: ('E'('0',f(A)) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f101,axiom,(
% 6.55/1.70 (![B_1,B_2,B_0,E,A_0,B,B_3]: (( ~ 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)))| ~ iLEQ(suc(B_2),suc(B_3))| ~ 'E'('0',f(B_0))| ~ 'E'('0',f(B_2))| ~ 'E'('0',f(suc(A_0)))| ~ 'E'('0',f(B))| ~ 'E'('0',f(B_3))| ~ 'E'('0',f(suc(B)))| ~ 'E'('0',f(suc(B_1)))| ~ 'E'('0',f(A_0))| ~ 'E'('0',f(suc(B_3)))| ~ 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)))| 'E'(f(B_3),f(suc(B_3))) ) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f113,axiom,(
% 6.55/1.70 (![E,B_1,B_2,A_0,B_0,B,B_3]: (( ~ '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)))| ~ iLEQ(suc(B_2),suc(B_3))| ~ 'E'(f(B_2),f(suc(B_2)))| ~ 'E'('0',f(suc(suc(B_3))))| ~ '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'(f(B_3),f(suc(B_3)))| ~ 'E'('0',f(suc(suc(B))))| ~ 'E'('0',f(B_3))| ~ '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'('0',f(suc(B_3)))| ~ 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_3),f(suc(suc(B_3))))| 'E'(f(B_0),f(suc(suc(B_0))))| 'E'(f(B_1),f(suc(suc(B_1)))) ) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f126,axiom,(
% 6.55/1.70 (![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)) ) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f501,axiom,(
% 6.55/1.70 (![E,B_2,B_1,A_0,B_0,B_3,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(suc(B_3)))))| ~ '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)))| ~ iLEQ(suc(B_2),suc(B_3))| ~ 'E'('0',f(suc(suc(suc(A_0)))))| ~ 'E'(f(B_2),f(suc(B_2)))| ~ 'E'('0',f(suc(suc(B_3))))| ~ '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'(f(B_3),f(suc(B_3)))| ~ 'E'('0',f(suc(suc(B))))| ~ 'E'(f(B),f(suc(suc(B))))| ~ 'E'('0',f(B_3))| ~ '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_3),f(suc(suc(B_3))))| ~ 'E'(f(B_0),f(suc(suc(B_0))))| ~ 'E'('0',f(suc(B_3)))| ~ iLEQ(suc(B),suc(B_0))| ~ 'E'(f(B_1),f(suc(suc(B_1)))) ) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f606,axiom,(
% 6.55/1.70 (![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)) ) ))),
% 6.55/1.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.55/1.70 fof(f754,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f11])).
% 6.55/1.70 fof(f755,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f754])).
% 6.55/1.70 fof(f914,plain,(
% 6.55/1.70 ![A]: 'E'('0',f(A))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f91])).
% 6.55/1.70 fof(f915,plain,(
% 6.55/1.70 ![E,X0]: ('E'('0',f(X0)))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f914])).
% 6.55/1.70 fof(f934,plain,(
% 6.55/1.70 ![B_3]: ((![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))))|~iLEQ(suc(B_2),suc(B_3)))|~'E'('0',f(B_0)))|~'E'('0',f(B_2)))|~'E'('0',f(suc(A_0))))|~'E'('0',f(B)))|~'E'('0',f(B_3)))|~'E'('0',f(suc(B))))|~'E'('0',f(suc(B_1))))|~'E'('0',f(A_0)))|~'E'('0',f(suc(B_3))))|~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)))))|'E'(f(B_3),f(suc(B_3))))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f101])).
% 6.55/1.70 fof(f935,plain,(
% 6.55/1.70 ![X0,X1,X2,E,X3,X4,X5]: (~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)))|~iLEQ(suc(X1),suc(X5))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X4))|~'E'('0',f(X5))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X3))|~'E'('0',f(suc(X5)))|~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)))|'E'(f(X5),f(suc(X5))))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f934])).
% 6.55/1.70 fof(f958,plain,(
% 6.55/1.70 ![B_1]: ((![B_0]: ((![B_3]: ((![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))))|~iLEQ(suc(B_2),suc(B_3)))|~'E'(f(B_2),f(suc(B_2))))|~'E'('0',f(suc(suc(B_3)))))|~'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'(f(B_3),f(suc(B_3))))|~'E'('0',f(suc(suc(B)))))|~'E'('0',f(B_3)))|~'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'('0',f(suc(B_3))))|~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_3),f(suc(suc(B_3))))))|'E'(f(B_0),f(suc(suc(B_0))))))|'E'(f(B_1),f(suc(suc(B_1)))))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f113])).
% 6.55/1.70 fof(f959,plain,(
% 6.55/1.70 ![E,X0,X1,X2,X3,X4,X5]: (~'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)))|~iLEQ(suc(X1),suc(X5))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X5))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'(f(X5),f(suc(X5)))|~'E'('0',f(suc(suc(X4))))|~'E'('0',f(X5))|~'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))|~'E'('0',f(suc(X5)))|~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(X5),f(suc(suc(X5))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f958])).
% 6.55/1.70 fof(f984,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f126])).
% 6.55/1.70 fof(f985,plain,(
% 6.55/1.70 ![E,X0]: (~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f984])).
% 6.55/1.70 fof(f1734,plain,(
% 6.55/1.70 ![B_1]: ((![B_0,B]: ((![B_3]: ((((![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(suc(B_3))))))|~'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))))|~iLEQ(suc(B_2),suc(B_3)))|~'E'('0',f(suc(suc(suc(A_0))))))|~'E'(f(B_2),f(suc(B_2))))|~'E'('0',f(suc(suc(B_3)))))|~'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'(f(B_3),f(suc(B_3))))|~'E'('0',f(suc(suc(B)))))|~'E'(f(B),f(suc(suc(B)))))|~'E'('0',f(B_3)))|~'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_3),f(suc(suc(B_3)))))|~'E'(f(B_0),f(suc(suc(B_0)))))|~'E'('0',f(suc(B_3)))))|~iLEQ(suc(B),suc(B_0))))|~'E'(f(B_1),f(suc(suc(B_1)))))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f501])).
% 6.55/1.70 fof(f1735,plain,(
% 6.55/1.70 ![E,X0,X1,X2,X3,X4,X5]: (~'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(suc(X4)))))|~'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(X5)))))|~'E'(f(X5),f(suc(X5)))|~iLEQ(suc(X2),suc(X5))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X0),suc(X4))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X5))|~'E'(f(X4),f(suc(X4)))|~'E'('0',f(suc(suc(X5))))|~'E'(f(X5),f(suc(suc(X5))))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X5)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'(f(X4),f(suc(suc(X4))))|~'E'(f(X3),f(suc(suc(X3))))|~'E'('0',f(suc(X4)))|~iLEQ(suc(X5),suc(X3))|~'E'(f(X1),f(suc(suc(X1)))))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f1734])).
% 6.55/1.70 fof(f1944,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(miniscoping,[status(thm)],[f606])).
% 6.55/1.70 fof(f1945,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(cnf_transformation,[status(thm)],[f1944])).
% 6.55/1.70 fof(f2200,plain,(
% 6.55/1.70 ![E,X0]: (~'E'('0',f(suc(X0)))|'E'(f(X0),f(suc(X0)))|iLEQ(suc(X0),suc(X0)))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f985,f915])).
% 6.55/1.70 fof(f2201,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f1945,f915])).
% 6.55/1.70 fof(f2203,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f755,f915])).
% 6.55/1.70 fof(f2204,plain,(
% 6.55/1.70 ![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)))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2203,f915])).
% 6.55/1.70 fof(f2207,plain,(
% 6.55/1.70 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2204,f2201])).
% 6.55/1.70 fof(f2210,plain,(
% 6.55/1.70 ![E,X0]: (~'E'('0',f(suc(X0)))|~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2207,f2200])).
% 6.55/1.70 fof(f2211,plain,(
% 6.55/1.70 ![E,X0]: (~'E'('0',f(X0))|iLEQ(suc(X0),suc(X0)))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2210,f915])).
% 6.55/1.70 fof(f2212,plain,(
% 6.55/1.70 ![X0]: (iLEQ(suc(X0),suc(X0)))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2211,f915])).
% 6.55/1.70 fof(f2224,plain,(
% 6.55/1.70 ![X0,X1,X2,X3,X4,E,X5]: (~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)))|~iLEQ(suc(X1),suc(X5))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(suc(X3)))|~'E'('0',f(X4))|~'E'('0',f(X5))|~'E'('0',f(suc(X4)))|~'E'('0',f(suc(X0)))|~'E'('0',f(X3))|~'E'('0',f(suc(X5)))|~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)))|'E'(f(X5),f(suc(X5))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f935,f915])).
% 6.55/1.70 fof(f2225,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X3))|~'E'('0',f(X2))|~'E'('0',f(X1))|~'E'('0',f(X3))|~'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)))|'E'(f(X3),f(suc(X3))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2224,f915])).
% 6.55/1.70 fof(f2230,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(duplicate_literals_removal,[status(thm)],[f2225])).
% 6.55/1.70 fof(f2231,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2230,f2212])).
% 6.55/1.70 fof(f2238,plain,(
% 6.55/1.70 ![X0,X1,X2,E,X3]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2231,f915])).
% 6.55/1.70 fof(f2239,plain,(
% 6.55/1.70 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2238,f915])).
% 6.55/1.70 fof(f2240,plain,(
% 6.55/1.70 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2239,f915])).
% 6.55/1.70 fof(f2241,plain,(
% 6.55/1.70 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2240,f915])).
% 6.55/1.70 fof(f2242,plain,(
% 6.55/1.70 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X1),suc(X3))|~'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))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2241,f915])).
% 6.55/1.70 fof(f2243,plain,(
% 6.55/1.70 ![X0,X1,X2,X3,E]: (~iLEQ(suc(X0),suc(X1))|~iLEQ(suc(X2),suc(X0))|~iLEQ(suc(X1),suc(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))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2242,f915])).
% 6.55/1.70 fof(f2244,plain,(
% 6.55/1.70 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(X0))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2243,f2212])).
% 6.55/1.70 fof(f2249,plain,(
% 6.55/1.70 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|'E'(f(X0),f(suc(X0))))),
% 6.55/1.70 inference(duplicate_literals_removal,[status(thm)],[f2244])).
% 6.55/1.70 fof(f2250,plain,(
% 6.55/1.70 ![E,X0]: ('E'(f(X0),f(suc(X0))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2249,f2212])).
% 6.55/1.70 fof(f2272,plain,(
% 6.55/1.70 ![X0,X1,E,X2,X3,X4,X5]: (~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)))|~iLEQ(suc(X1),suc(X5))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X5))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X1))|~'E'('0',f(suc(X2)))|~'E'('0',f(X4))|~'E'(f(X5),f(suc(X5)))|~'E'('0',f(suc(suc(X4))))|~'E'('0',f(X5))|~'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))|~'E'('0',f(suc(X5)))|~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(X5),f(suc(suc(X5))))|'E'(f(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f959,f2250])).
% 6.55/1.70 fof(f2273,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X3))|~'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'(f(X3),f(suc(X3)))|~'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))|~'E'('0',f(suc(X3)))|~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(X3),f(suc(suc(X3))))|'E'(f(X0),f(suc(suc(X0)))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2272,f915])).
% 6.55/1.70 fof(f2279,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X3))|~'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)))))),
% 6.55/1.70 inference(duplicate_literals_removal,[status(thm)],[f2273])).
% 6.55/1.70 fof(f2280,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X3))|~'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)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2279,f2212])).
% 6.55/1.70 fof(f2286,plain,(
% 6.55/1.70 ![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)))|~iLEQ(suc(X1),suc(X2))|~'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)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2280,f915])).
% 6.55/1.70 fof(f2287,plain,(
% 6.55/1.70 ![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))|~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)))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2286,f915])).
% 6.55/1.70 fof(f2304,plain,(
% 6.55/1.70 ![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)))))),
% 6.55/1.70 inference(duplicate_literals_removal,[status(thm)],[f2287])).
% 6.55/1.70 fof(f2305,plain,(
% 6.55/1.70 ![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)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2304,f2212])).
% 6.55/1.70 fof(f2328,plain,(
% 6.55/1.70 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0))))|'E'(f(X0),f(suc(suc(X0)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2305,f915])).
% 6.55/1.70 fof(f2329,plain,(
% 6.55/1.70 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|'E'(f(X0),f(suc(suc(X0)))))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2328,f915])).
% 6.55/1.70 fof(f2330,plain,(
% 6.55/1.70 ![E,X0]: ('E'(f(X0),f(suc(suc(X0)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2329,f2250])).
% 6.55/1.70 fof(f2331,plain,(
% 6.55/1.70 ![E,X0,X1,X2,X3,X4,X5]: (~'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(suc(X4)))))|~'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(X5)))))|~'E'(f(X5),f(suc(X5)))|~iLEQ(suc(X2),suc(X5))|~'E'(f(X2),f(suc(suc(X2))))|~'E'('0',f(suc(X3)))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X0),suc(X4))|~'E'('0',f(suc(suc(suc(X2)))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X4))))|~'E'(f(X2),f(suc(X2)))|~'E'('0',f(X3))|~'E'('0',f(X0))|~'E'('0',f(suc(X2)))|~'E'('0',f(X5))|~'E'(f(X4),f(suc(X4)))|~'E'('0',f(suc(suc(X5))))|~'E'(f(X5),f(suc(suc(X5))))|~'E'('0',f(X4))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X5)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X2))|~'E'(f(X4),f(suc(suc(X4))))|~'E'(f(X3),f(suc(suc(X3))))|~'E'('0',f(suc(X4)))|~iLEQ(suc(X5),suc(X3))|~'E'(f(X1),f(suc(suc(X1)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f1735,f915])).
% 6.55/1.70 fof(f2344,plain,(
% 6.55/1.70 ![E,X0,X1]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X1))))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X1)))|~'E'('0',f(X1))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(suc(suc(X1))))|~'E'('0',f(X1))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X1)))),
% 6.55/1.70 inference(resolution,[status(thm)],[f2331,f2330])).
% 6.55/1.70 fof(f2404,plain,(
% 6.55/1.70 ![E,X0,X1]: (~'E'(f(X0),f(suc(suc(X0))))|~'E'(f(X1),f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'('0',f(suc(suc(X1))))|~iLEQ(suc(X1),suc(X1))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(suc(X1)))))|~'E'('0',f(suc(X1)))|~'E'('0',f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X0)))))),
% 6.55/1.70 inference(duplicate_literals_removal,[status(thm)],[f2344])).
% 6.55/1.70 fof(f2405,plain,(
% 6.55/1.70 ![E,X0,X1]: (~'E'(f(X0),f(suc(X0)))|~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2404,f2330])).
% 6.55/1.70 fof(f2466,plain,(
% 6.55/1.70 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(suc(X0)))))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1)))))),
% 6.55/1.70 inference(forward_subsumption_resolution,[status(thm)],[f2405,f2250])).
% 6.55/1.70 fof(f2469,plain,(
% 6.55/1.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X0))))|~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1)))))),
% 6.55/1.71 inference(resolution,[status(thm)],[f2466,f915])).
% 6.55/1.71 fof(f2474,plain,(
% 6.55/1.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(suc(suc(X0))))|~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1)))))),
% 6.55/1.71 inference(forward_subsumption_resolution,[status(thm)],[f2469,f2212])).
% 6.55/1.71 fof(f2477,plain,(
% 6.55/1.71 ![X0,X1,E]: (~iLEQ(suc(X0),suc(X1))|~'E'('0',f(X0))|~'E'('0',f(suc(X0)))|~'E'('0',f(suc(X1)))|~iLEQ(suc(X1),suc(X0))|~'E'(f(X1),f(suc(X1)))|~'E'('0',f(X1))|~'E'('0',f(suc(suc(X1)))))),
% 6.55/1.71 inference(forward_subsumption_resolution,[status(thm)],[f2474,f915])).
% 6.55/1.71 fof(f2478,plain,(
% 6.55/1.71 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~iLEQ(suc(X0),suc(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(X0))|~'E'('0',f(suc(suc(X0)))))),
% 6.55/1.71 inference(resolution,[status(thm)],[f2477,f915])).
% 6.55/1.71 fof(f2483,plain,(
% 6.55/1.71 ![X0,E]: (~iLEQ(suc(X0),suc(X0))|~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 6.55/1.71 inference(duplicate_literals_removal,[status(thm)],[f2478])).
% 6.55/1.71 fof(f2484,plain,(
% 6.55/1.71 ![E,X0]: (~'E'('0',f(X0))|~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 6.55/1.71 inference(forward_subsumption_resolution,[status(thm)],[f2483,f2212])).
% 6.55/1.71 fof(f2489,plain,(
% 6.55/1.71 ![E,X0]: (~'E'(f(X0),f(suc(X0)))|~'E'('0',f(suc(suc(X0)))))),
% 6.55/1.71 inference(forward_subsumption_resolution,[status(thm)],[f2484,f915])).
% 6.55/1.71 fof(f2490,plain,(
% 6.55/1.71 ![E,X0]: (~'E'(f(X0),f(suc(X0))))),
% 6.55/1.71 inference(resolution,[status(thm)],[f2489,f915])).
% 6.55/1.71 fof(f2491,plain,(
% 6.55/1.71 $false),
% 6.55/1.71 inference(forward_subsumption_resolution,[status(thm)],[f2490,f2250])).
% 6.55/1.71 % SZS output end CNFRefutation for theBenchmark.p
% 6.28/1.74 % Elapsed time: 1.375216 seconds
% 6.28/1.74 % CPU time: 7.551684 seconds
% 6.28/1.74 % Total memory used: 197.111 MB
% 6.28/1.74 % Net memory used: 192.513 MB
%------------------------------------------------------------------------------