%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:48:26 PM UTC 2026
% Result : Unsatisfiable 0.55s 0.49s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 54
% Syntax : Number of clauses : 230 ( 10 unt; 136 nHn; 209 RR)
% Number of literals : 1886 ( 0 equ;1523 neg)
% Maximal clause size : 14 ( 8 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 504 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_330,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_330) ).
cnf(clause_486,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_486) ).
cnf(clause_473,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_473) ).
cnf(clause_227,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_227) ).
cnf(clause_534,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_534) ).
cnf(clause_291,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_291) ).
cnf(clause_137,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_137) ).
cnf(clause_131,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_131) ).
cnf(clause_103,axiom,
( ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_103) ).
cnf(clause_658,axiom,
( ~ 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_658) ).
cnf(clause_550,axiom,
( ~ 'LE'(f(suc(X1)),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_550) ).
cnf(clause_556,axiom,
'LE'(f(X1),s(s(s(s('0'))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_556) ).
cnf(clause_663,axiom,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_663) ).
cnf(clause_283,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_283) ).
cnf(clause_594,axiom,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_594) ).
cnf(clause_463,axiom,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_463) ).
cnf(clause_501,axiom,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_501) ).
cnf(clause_723,axiom,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_723) ).
cnf(clause_515,axiom,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_515) ).
cnf(clause_325,axiom,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_325) ).
cnf(clause_352,axiom,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_352) ).
cnf(clause_528,axiom,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_528) ).
cnf(clause_607,axiom,
( ~ 'LE'(f(suc(suc(X1))),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_607) ).
cnf(clause_300,axiom,
( ~ 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_300) ).
cnf(clause_457,axiom,
( ~ 'LE'(f(suc(X1)),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_457) ).
cnf(clause_415,axiom,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_415) ).
cnf(clause_383,axiom,
( ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_383) ).
cnf(clause_228,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_228) ).
cnf(clause_687,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_687) ).
cnf(clause_80,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_80) ).
cnf(clause_592,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_592) ).
cnf(clause_145,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_145) ).
cnf(clause_671,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_671) ).
cnf(clause_35,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_35) ).
cnf(clause_41,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_41) ).
cnf(clause_508,axiom,
( ~ 'LE'(f(suc(suc(X1))),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_508) ).
cnf(clause_44,axiom,
( ~ 'LE'(f(X1),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44) ).
cnf(clause_95,axiom,
( ~ 'LE'(f(suc(X1)),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_95) ).
cnf(clause_125,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_125) ).
cnf(clause_563,axiom,
( ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_563) ).
cnf(clause_223,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_223) ).
cnf(clause_614,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_614) ).
cnf(clause_458,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_458) ).
cnf(clause_450,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_450) ).
cnf(clause_479,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_479) ).
cnf(clause_209,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_209) ).
cnf(clause_572,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_572) ).
cnf(clause_61,axiom,
( ~ 'LE'(f(suc(suc(X1))),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_61) ).
cnf(clause_497,axiom,
( ~ 'LE'(f(X1),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_497) ).
cnf(clause_595,axiom,
( ~ 'LE'(f(suc(X1)),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_595) ).
cnf(clause_363,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_363) ).
cnf(clause_560,axiom,
( ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_560) ).
cnf(clause_713,axiom,
( ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_713) ).
cnf(clause_359,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_359) ).
cnf(c_0_54,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_330]) ).
cnf(c_0_55,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_486]) ).
cnf(c_0_56,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_473]) ).
cnf(c_0_57,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_227]) ).
cnf(c_0_58,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_534]) ).
cnf(c_0_59,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
c_0_54 ).
cnf(c_0_60,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_55 ).
cnf(c_0_61,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_56 ).
cnf(c_0_62,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
inference(fof_simplification,[status(thm)],[clause_291]) ).
cnf(c_0_63,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_57 ).
cnf(c_0_64,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_137]) ).
cnf(c_0_65,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(fof_simplification,[status(thm)],[clause_131]) ).
cnf(c_0_66,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
c_0_58 ).
cnf(c_0_67,plain,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_68,plain,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_61,c_0_60]) ).
cnf(c_0_69,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
c_0_62 ).
cnf(c_0_70,plain,
( ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_63,c_0_60]) ).
cnf(c_0_71,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X3),f(suc(X3))) ),
c_0_64 ).
cnf(c_0_72,plain,
( ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X1)))) ),
inference(fof_simplification,[status(thm)],[clause_103]) ).
cnf(c_0_73,plain,
( ~ 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X1)) ),
inference(fof_simplification,[status(thm)],[clause_658]) ).
cnf(c_0_74,plain,
( ~ 'LE'(f(suc(X1)),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_550]) ).
cnf(c_0_75,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2)) ),
c_0_65 ).
cnf(c_0_76,plain,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_66,c_0_67]),c_0_68]) ).
cnf(c_0_77,plain,
( ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_69,c_0_67]),c_0_70]) ).
cnf(c_0_78,plain,
( ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_71,c_0_68]),c_0_70]) ).
cnf(c_0_79,plain,
( ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X1)))) ),
c_0_72 ).
cnf(c_0_80,axiom,
'LE'(f(X1),s(s(s(s('0'))))),
clause_556 ).
cnf(c_0_81,plain,
( ~ 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X1)) ),
c_0_73 ).
cnf(c_0_82,plain,
( ~ 'LE'(f(suc(X1)),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X1))) ),
c_0_74 ).
cnf(c_0_83,plain,
( ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_75,c_0_76]),c_0_77]),c_0_78]) ).
cnf(c_0_84,plain,
( 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_79,c_0_80])]) ).
cnf(c_0_85,plain,
( 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_81,c_0_80])]) ).
cnf(c_0_86,plain,
( 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82,c_0_80])]) ).
cnf(c_0_87,plain,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(fof_simplification,[status(thm)],[clause_663]) ).
cnf(c_0_88,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_283]) ).
cnf(c_0_89,plain,
( ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s(s(s('0')))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_83,c_0_84]),c_0_85]),c_0_86]) ).
cnf(c_0_90,plain,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
c_0_87 ).
cnf(c_0_91,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
c_0_88 ).
cnf(c_0_92,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_594]) ).
cnf(c_0_93,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_463]) ).
cnf(c_0_94,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_501]) ).
cnf(c_0_95,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_723]) ).
cnf(c_0_96,plain,
( ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_84]),c_0_85]),c_0_86]) ).
cnf(c_0_97,plain,
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[c_0_90,c_0_91]) ).
cnf(c_0_98,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_515]) ).
cnf(c_0_99,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
c_0_92 ).
cnf(c_0_100,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_93 ).
cnf(c_0_101,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_94 ).
cnf(c_0_102,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
inference(fof_simplification,[status(thm)],[clause_325]) ).
cnf(c_0_103,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_95 ).
cnf(c_0_104,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_352]) ).
cnf(c_0_105,plain,
( ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X3),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_84]),c_0_85]),c_0_86]) ).
cnf(c_0_106,plain,
( 'LE'(f(X1),s(s(s('0'))))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_84]),c_0_85]),c_0_86]) ).
cnf(c_0_107,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_528]) ).
cnf(c_0_108,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X1),f(suc(X1))) ),
c_0_98 ).
cnf(c_0_109,plain,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_99,c_0_100]) ).
cnf(c_0_110,plain,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_101,c_0_100]) ).
cnf(c_0_111,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
c_0_102 ).
cnf(c_0_112,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_103,c_0_100]) ).
cnf(c_0_113,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_104 ).
cnf(c_0_114,plain,
( ~ 'LE'(f(suc(suc(X1))),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X1)))) ),
inference(fof_simplification,[status(thm)],[clause_607]) ).
cnf(c_0_115,plain,
( ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) ),
inference(spm,[status(thm)],[c_0_105,c_0_106]) ).
cnf(c_0_116,plain,
( ~ 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(X1)) ),
inference(fof_simplification,[status(thm)],[clause_300]) ).
cnf(c_0_117,plain,
( ~ 'LE'(f(suc(X1)),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_457]) ).
cnf(c_0_118,plain,
( ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1))) ),
c_0_107 ).
cnf(c_0_119,plain,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_108,c_0_109]),c_0_110]) ).
cnf(c_0_120,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_111,c_0_109]),c_0_112]) ).
cnf(c_0_121,plain,
( ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_113,c_0_110]),c_0_112]) ).
cnf(c_0_122,plain,
( ~ 'LE'(f(suc(suc(X1))),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X1)))) ),
c_0_114 ).
cnf(c_0_123,plain,
'LE'(f(X1),s(s(s('0')))),
inference(spm,[status(thm)],[c_0_115,c_0_106]) ).
cnf(c_0_124,plain,
( ~ 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(X1)) ),
c_0_116 ).
cnf(c_0_125,plain,
( ~ 'LE'(f(suc(X1)),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(X1))) ),
c_0_117 ).
cnf(c_0_126,plain,
( ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_118,c_0_119]),c_0_120]),c_0_121]) ).
cnf(c_0_127,plain,
( 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_122,c_0_123])]) ).
cnf(c_0_128,plain,
( 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_124,c_0_123])]) ).
cnf(c_0_129,plain,
( 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_125,c_0_123])]) ).
cnf(c_0_130,plain,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(fof_simplification,[status(thm)],[clause_415]) ).
cnf(c_0_131,plain,
( ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_383]) ).
cnf(c_0_132,plain,
( ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s(s('0'))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_126,c_0_127]),c_0_128]),c_0_129]) ).
cnf(c_0_133,plain,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
c_0_130 ).
cnf(c_0_134,plain,
( ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
c_0_131 ).
cnf(c_0_135,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_228]) ).
cnf(c_0_136,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_687]) ).
cnf(c_0_137,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_80]) ).
cnf(c_0_138,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_592]) ).
cnf(c_0_139,plain,
( ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X1),s(s('0'))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_132,c_0_127]),c_0_128]),c_0_129]) ).
cnf(c_0_140,plain,
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[c_0_133,c_0_134]) ).
cnf(c_0_141,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_145]) ).
cnf(c_0_142,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
c_0_135 ).
cnf(c_0_143,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_136 ).
cnf(c_0_144,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_137 ).
cnf(c_0_145,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
inference(fof_simplification,[status(thm)],[clause_671]) ).
cnf(c_0_146,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_138 ).
cnf(c_0_147,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_35]) ).
cnf(c_0_148,plain,
( ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X3),s(s('0')))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X1),s(s('0'))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_139,c_0_127]),c_0_128]),c_0_129]) ).
cnf(c_0_149,plain,
( 'LE'(f(X1),s(s('0')))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_140,c_0_127]),c_0_128]),c_0_129]) ).
cnf(c_0_150,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(fof_simplification,[status(thm)],[clause_41]) ).
cnf(c_0_151,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
c_0_141 ).
cnf(c_0_152,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_142,c_0_143]) ).
cnf(c_0_153,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_144,c_0_143]) ).
cnf(c_0_154,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
c_0_145 ).
cnf(c_0_155,plain,
( ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_146,c_0_143]) ).
cnf(c_0_156,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X3),f(suc(X3))) ),
c_0_147 ).
cnf(c_0_157,plain,
( ~ 'LE'(f(suc(suc(X1))),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) ),
inference(fof_simplification,[status(thm)],[clause_508]) ).
cnf(c_0_158,plain,
( ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X1),s(s('0'))) ),
inference(spm,[status(thm)],[c_0_148,c_0_149]) ).
cnf(c_0_159,plain,
( ~ 'LE'(f(X1),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) ),
inference(fof_simplification,[status(thm)],[clause_44]) ).
cnf(c_0_160,plain,
( ~ 'LE'(f(suc(X1)),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_95]) ).
cnf(c_0_161,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2)) ),
c_0_150 ).
cnf(c_0_162,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_151,c_0_152]),c_0_153]) ).
cnf(c_0_163,plain,
( ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_154,c_0_152]),c_0_155]) ).
cnf(c_0_164,plain,
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_156,c_0_153]),c_0_155]) ).
cnf(c_0_165,plain,
( ~ 'LE'(f(suc(suc(X1))),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) ),
c_0_157 ).
cnf(c_0_166,plain,
'LE'(f(X1),s(s('0'))),
inference(spm,[status(thm)],[c_0_158,c_0_149]) ).
cnf(c_0_167,plain,
( ~ 'LE'(f(X1),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) ),
c_0_159 ).
cnf(c_0_168,plain,
( ~ 'LE'(f(suc(X1)),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(X1))) ),
c_0_160 ).
cnf(c_0_169,plain,
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_161,c_0_162]),c_0_163]),c_0_164]) ).
cnf(c_0_170,plain,
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_165,c_0_166])]) ).
cnf(c_0_171,plain,
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167,c_0_166])]) ).
cnf(c_0_172,plain,
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_168,c_0_166])]) ).
cnf(c_0_173,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(fof_simplification,[status(thm)],[clause_125]) ).
cnf(c_0_174,plain,
( ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_563]) ).
cnf(c_0_175,plain,
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s('0')) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_169,c_0_170]),c_0_171]),c_0_172]) ).
cnf(c_0_176,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
c_0_173 ).
cnf(c_0_177,plain,
( ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
c_0_174 ).
cnf(c_0_178,plain,
( ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'LE'(f(X2),s('0'))
| 'LE'(f(X1),s('0')) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_175,c_0_170]),c_0_171]),c_0_172]) ).
cnf(c_0_179,plain,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[c_0_176,c_0_177]) ).
cnf(c_0_180,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_223]) ).
cnf(c_0_181,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_614]) ).
cnf(c_0_182,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_458]) ).
cnf(c_0_183,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_450]) ).
cnf(c_0_184,plain,
( ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X3),s('0'))
| 'LE'(f(X2),s('0'))
| 'LE'(f(X1),s('0')) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_178,c_0_170]),c_0_171]),c_0_172]) ).
cnf(c_0_185,plain,
( 'LE'(f(X1),s('0'))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_179,c_0_170]),c_0_171]),c_0_172]) ).
cnf(c_0_186,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
inference(fof_simplification,[status(thm)],[clause_479]) ).
cnf(c_0_187,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
c_0_180 ).
cnf(c_0_188,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_181 ).
cnf(c_0_189,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_182 ).
cnf(c_0_190,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
inference(fof_simplification,[status(thm)],[clause_209]) ).
cnf(c_0_191,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_183 ).
cnf(c_0_192,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_572]) ).
cnf(c_0_193,plain,
( ~ 'LE'(f(suc(suc(X1))),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(X1)))) ),
inference(fof_simplification,[status(thm)],[clause_61]) ).
cnf(c_0_194,plain,
( ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),s('0'))
| 'LE'(f(X1),s('0')) ),
inference(spm,[status(thm)],[c_0_184,c_0_185]) ).
cnf(c_0_195,plain,
( ~ 'LE'(f(X1),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(X1)) ),
inference(fof_simplification,[status(thm)],[clause_497]) ).
cnf(c_0_196,plain,
( ~ 'LE'(f(suc(X1)),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_595]) ).
cnf(c_0_197,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_363]) ).
cnf(c_0_198,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
c_0_186 ).
cnf(c_0_199,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_187,c_0_188]) ).
cnf(c_0_200,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_189,c_0_188]) ).
cnf(c_0_201,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X3),f(suc(X3))) ),
c_0_190 ).
cnf(c_0_202,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[c_0_191,c_0_188]) ).
cnf(c_0_203,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X1),f(suc(X1))) ),
c_0_192 ).
cnf(c_0_204,plain,
( ~ 'LE'(f(suc(suc(X1))),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(X1)))) ),
c_0_193 ).
cnf(c_0_205,plain,
'LE'(f(X1),s('0')),
inference(spm,[status(thm)],[c_0_194,c_0_185]) ).
cnf(c_0_206,plain,
( ~ 'LE'(f(X1),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(X1)) ),
c_0_195 ).
cnf(c_0_207,plain,
( ~ 'LE'(f(suc(X1)),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ),
c_0_196 ).
cnf(c_0_208,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1))) ),
c_0_197 ).
cnf(c_0_209,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_198,c_0_199]),c_0_200]) ).
cnf(c_0_210,plain,
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_201,c_0_202]),c_0_200]) ).
cnf(c_0_211,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_203,c_0_199]),c_0_202]) ).
cnf(c_0_212,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_204,c_0_205])]) ).
cnf(c_0_213,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_206,c_0_205])]) ).
cnf(c_0_214,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_207,c_0_205])]) ).
cnf(c_0_215,plain,
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_208,c_0_209]),c_0_210]) ).
cnf(c_0_216,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),'0')
| 'E'(f(X1),f(suc(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_211,c_0_212]),c_0_213]),c_0_214]) ).
cnf(c_0_217,plain,
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),'0') ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_215,c_0_212]),c_0_213]),c_0_214]),c_0_216]) ).
cnf(c_0_218,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(fof_simplification,[status(thm)],[clause_560]) ).
cnf(c_0_219,plain,
( ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(fof_simplification,[status(thm)],[clause_713]) ).
cnf(c_0_220,plain,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_217,c_0_212]),c_0_213]),c_0_214]) ).
cnf(c_0_221,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
c_0_218 ).
cnf(c_0_222,plain,
( ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
c_0_219 ).
cnf(c_0_223,plain,
( ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X3),'0')
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_220,c_0_212]),c_0_213]),c_0_214]) ).
cnf(c_0_224,plain,
( ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[c_0_221,c_0_222]) ).
cnf(c_0_225,plain,
~ 'LE'(f(z),'0'),
inference(fof_simplification,[status(thm)],[clause_359]) ).
cnf(c_0_226,plain,
( ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_223,c_0_224]),c_0_213]),c_0_214]),c_0_212]) ).
cnf(c_0_227,plain,
~ 'LE'(f(z),'0'),
c_0_225 ).
cnf(c_0_228,plain,
'LE'(f(X1),'0'),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_226,c_0_224]),c_0_213]),c_0_214]),c_0_212]) ).
cnf(c_0_229,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_227,c_0_228])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 12:14:30 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.55/0.49 % Version: 3.5.1
% 0.55/0.49 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.55/0.49 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.55/0.49 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.55/0.49 % Starting new_bool_3 with 300s (1) cores
% 0.55/0.49 % Starting new_bool_1 with 300s (1) cores
% 0.55/0.49 % Starting sh5l with 300s (1) cores
% 0.55/0.49 % new_bool_1 with pid 3076418 completed with status 9
% 0.55/0.49 % sh5l with pid 3076419 completed with status 9
% 0.55/0.49 % new_bool_3 with pid 3076417 completed with status 9
% 0.55/0.49 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 3076416 completed with status 0
% 0.55/0.49 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 0.55/0.49 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.55/0.49 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.55/0.49 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.55/0.49 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.55/0.49 % No SInE strategy applied
% 0.55/0.49 % Search class: FGHNF-FSLF11-MFFFFFNN
% 0.55/0.49 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.55/0.49 % Starting SubtermCWHack with 136s (1) cores
% 0.55/0.49 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 0.55/0.49 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 0.55/0.49 % Starting new_bool_3 with 136s (1) cores
% 0.55/0.49 % Starting new_bool_1 with 136s (1) cores
% 0.55/0.49 % G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with pid 3076431 completed with status 0
% 0.55/0.49 % Result found by G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
% 0.55/0.49 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.55/0.49 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.55/0.49 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.55/0.49 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.55/0.49 % No SInE strategy applied
% 0.55/0.49 % Search class: FGHNF-FSLF11-MFFFFFNN
% 0.55/0.49 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.55/0.49 % Starting SubtermCWHack with 136s (1) cores
% 0.55/0.49 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 0.55/0.49 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 0.55/0.49 % Preprocessing time : 0.003 s
% 0.55/0.49 % Presaturation interreduction done
% 0.55/0.49
% 0.55/0.49 % Proof found!
% 0.55/0.49 % SZS status Unsatisfiable
% 0.55/0.49 % SZS output start CNFRefutation
% See solution above
% 0.55/0.50 % Parsed axioms : 54
% 0.55/0.50 % Removed by relevancy pruning/SinE : 0
% 0.55/0.50 % Initial clauses : 54
% 0.55/0.50 % Removed in clause preprocessing : 0
% 0.55/0.50 % Initial clauses in saturation : 54
% 0.55/0.50 % Processed clauses : 300
% 0.55/0.50 % ...of these trivial : 1
% 0.55/0.50 % ...subsumed : 63
% 0.55/0.50 % ...remaining for further processing : 236
% 0.55/0.50 % Other redundant clauses eliminated : 0
% 0.55/0.50 % Clauses deleted for lack of memory : 0
% 0.55/0.50 % Backward-subsumed : 93
% 0.55/0.50 % Backward-rewritten : 48
% 0.55/0.50 % Generated clauses : 486
% 0.55/0.50 % ...of the previous two non-redundant : 493
% 0.55/0.50 % ...aggressively subsumed : 0
% 0.55/0.50 % Contextual simplify-reflections : 122
% 0.55/0.50 % Paramodulations : 486
% 0.55/0.50 % Factorizations : 0
% 0.55/0.50 % NegExts : 0
% 0.55/0.50 % Equation resolutions : 0
% 0.55/0.50 % Disequality decompositions : 0
% 0.55/0.50 % Total rewrite steps : 75
% 0.55/0.50 % ...of those cached : 52
% 0.55/0.50 % Propositional unsat checks : 0
% 0.55/0.50 % Propositional check models : 0
% 0.55/0.50 % Propositional check unsatisfiable : 0
% 0.55/0.50 % Propositional clauses : 0
% 0.55/0.50 % Propositional clauses after purity: 0
% 0.55/0.50 % Propositional unsat core size : 0
% 0.55/0.50 % Propositional preprocessing time : 0.000
% 0.55/0.50 % Propositional encoding time : 0.000
% 0.55/0.50 % Propositional solver time : 0.000
% 0.55/0.50 % Success case prop preproc time : 0.000
% 0.55/0.50 % Success case prop encoding time : 0.000
% 0.55/0.50 % Success case prop solver time : 0.000
% 0.55/0.50 % Current number of processed clauses : 41
% 0.55/0.50 % Positive orientable unit clauses : 8
% 0.55/0.50 % Positive unorientable unit clauses: 0
% 0.55/0.50 % Negative unit clauses : 0
% 0.55/0.50 % Non-unit-clauses : 33
% 0.55/0.50 % Current number of unprocessed clauses: 159
% 0.55/0.50 % ...number of literals in the above : 1557
% 0.55/0.50 % Current number of archived formulas : 0
% 0.55/0.50 % Current number of archived clauses : 195
% 0.55/0.50 % Clause-clause subsumption calls (NU) : 6214
% 0.55/0.50 % Rec. Clause-clause subsumption calls : 1456
% 0.55/0.50 % Non-unit clause-clause subsumptions : 260
% 0.55/0.50 % Unit Clause-clause subsumption calls : 110
% 0.55/0.50 % Rewrite failures with RHS unbound : 0
% 0.55/0.50 % BW rewrite match attempts : 31
% 0.55/0.50 % BW rewrite match successes : 19
% 0.55/0.50 % Condensation attempts : 0
% 0.55/0.50 % Condensation successes : 0
% 0.55/0.50 % Termbank termtop insertions : 38655
% 0.55/0.50 % Search garbage collected termcells : 466
% 0.55/0.50
% 0.55/0.50 % -------------------------------------------------
% 0.55/0.50 % User time : 0.063 s
% 0.55/0.50 % System time : 0.004 s
% 0.55/0.50 % Total time : 0.067 s
% 0.55/0.50 % Maximum resident set size: 3712 pages
% 0.55/0.50
% 0.55/0.50 % -------------------------------------------------
% 0.55/0.50 % User time : 0.360 s
% 0.55/0.50 % System time : 0.047 s
% 0.55/0.50 % Total time : 0.407 s
% 0.55/0.50 % Maximum resident set size: 4608 pages
% 0.55/0.50 % E exiting
%------------------------------------------------------------------------------