%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYO688-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:54:39 PM UTC 2026
% Result : Unsatisfiable 3.26s 3.11s
% Output : CNFRefutation 3.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 64
% Syntax : Number of clauses : 217 ( 13 unt; 129 nHn; 192 RR)
% Number of literals : 1668 ( 0 equ;1322 neg)
% Maximal clause size : 14 ( 7 avg)
% Maximal term depth : 6 ( 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 : 457 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_904,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_904) ).
cnf(clause_105,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_105) ).
cnf(clause_650,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_650) ).
cnf(clause_1074,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1074) ).
cnf(clause_740,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_740) ).
cnf(clause_748,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_748) ).
cnf(clause_159,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_159) ).
cnf(clause_436,axiom,
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_436) ).
cnf(clause_231,axiom,
( 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'LE'(f(suc(suc(X1))),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_231) ).
cnf(clause_299,axiom,
'LE'(f(X1),s(s(s(s(s('0')))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_299) ).
cnf(clause_298,axiom,
( 'E'(s(s(s(s('0')))),f(X1))
| 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'LE'(f(X1),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_298) ).
cnf(clause_297,axiom,
( 'E'(s(s(s(s('0')))),f(suc(X1)))
| 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'LE'(f(suc(X1)),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_297) ).
cnf(clause_473,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_473) ).
cnf(clause_698,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_698) ).
cnf(clause_715,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_715) ).
cnf(clause_249,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_249) ).
cnf(clause_314,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_314) ).
cnf(clause_968,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_968) ).
cnf(clause_915,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_915) ).
cnf(clause_514,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_514) ).
cnf(clause_114,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_114) ).
cnf(clause_1016,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1016) ).
cnf(clause_1123,axiom,
( 'E'(s(s(s('0'))),f(suc(suc(X1))))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1123) ).
cnf(clause_24,axiom,
( 'E'(s(s(s('0'))),f(X1))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'LE'(f(X1),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_24) ).
cnf(clause_269,axiom,
( 'E'(s(s(s('0'))),f(suc(X1)))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'LE'(f(suc(X1)),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_269) ).
cnf(clause_1023,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1023) ).
cnf(clause_171,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_171) ).
cnf(clause_335,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_335) ).
cnf(clause_778,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(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(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_778) ).
cnf(clause_64,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(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(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_64) ).
cnf(clause_722,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(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(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_722) ).
cnf(clause_191,axiom,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_191) ).
cnf(clause_985,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_985) ).
cnf(clause_207,axiom,
( 'E'(f(X3),f(suc(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(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_207) ).
cnf(clause_115,axiom,
( ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_115) ).
cnf(clause_569,axiom,
( 'E'(s(s('0')),f(suc(suc(X1))))
| 'LE'(f(X1),s(s('0')))
| ~ 'LE'(f(suc(suc(X1))),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_569) ).
cnf(clause_1143,axiom,
( 'E'(s(s('0')),f(X1))
| 'LE'(f(X1),s(s('0')))
| ~ 'LE'(f(X1),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1143) ).
cnf(clause_773,axiom,
( 'E'(s(s('0')),f(suc(X1)))
| 'LE'(f(X1),s(s('0')))
| ~ 'LE'(f(suc(X1)),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_773) ).
cnf(clause_237,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_237) ).
cnf(clause_794,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_794) ).
cnf(clause_912,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_912) ).
cnf(clause_694,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_694) ).
cnf(clause_174,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_174) ).
cnf(clause_826,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_826) ).
cnf(clause_709,axiom,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_709) ).
cnf(clause_447,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_447) ).
cnf(clause_281,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_281) ).
cnf(clause_813,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_813) ).
cnf(clause_160,axiom,
( 'E'(s('0'),f(suc(suc(X1))))
| 'LE'(f(X1),s('0'))
| ~ 'LE'(f(suc(suc(X1))),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_160) ).
cnf(clause_1158,axiom,
( 'E'(s('0'),f(X1))
| 'LE'(f(X1),s('0'))
| ~ 'LE'(f(X1),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1158) ).
cnf(clause_149,axiom,
( 'E'(s('0'),f(suc(X1)))
| 'LE'(f(X1),s('0'))
| ~ 'LE'(f(suc(X1)),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_149) ).
cnf(clause_340,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_340) ).
cnf(clause_1089,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1089) ).
cnf(clause_699,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_699) ).
cnf(clause_303,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_303) ).
cnf(clause_840,axiom,
( 'E'('0',f(suc(suc(X1))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(X1))),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_840) ).
cnf(clause_199,axiom,
( 'E'('0',f(X1))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(X1),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_199) ).
cnf(clause_713,axiom,
( 'E'('0',f(suc(X1)))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(X1)),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_713) ).
cnf(clause_483,axiom,
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_483) ).
cnf(clause_910,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_910) ).
cnf(clause_546,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_546) ).
cnf(clause_743,axiom,
( ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_743) ).
cnf(clause_106,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_106) ).
cnf(clause_256,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_256) ).
cnf(c_0_64,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2))) ),
clause_904 ).
cnf(c_0_65,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2))) ),
clause_105 ).
cnf(c_0_66,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3))) ),
clause_650 ).
cnf(c_0_67,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
clause_1074 ).
cnf(c_0_68,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3))) ),
clause_740 ).
cnf(c_0_69,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_70,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[c_0_66,c_0_65]) ).
cnf(c_0_71,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
clause_748 ).
cnf(c_0_72,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3)) ),
inference(csr,[status(thm)],[c_0_67,c_0_65]) ).
cnf(c_0_73,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
clause_159 ).
cnf(c_0_74,axiom,
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
clause_436 ).
cnf(c_0_75,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_68,c_0_69]),c_0_70]) ).
cnf(c_0_76,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_71,c_0_69]),c_0_72]) ).
cnf(c_0_77,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_73,c_0_70]),c_0_72]) ).
cnf(c_0_78,axiom,
( 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'LE'(f(suc(suc(X1))),s(s(s(s(s('0')))))) ),
clause_231 ).
cnf(c_0_79,axiom,
'LE'(f(X1),s(s(s(s(s('0')))))),
clause_299 ).
cnf(c_0_80,axiom,
( 'E'(s(s(s(s('0')))),f(X1))
| 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'LE'(f(X1),s(s(s(s(s('0')))))) ),
clause_298 ).
cnf(c_0_81,axiom,
( 'E'(s(s(s(s('0')))),f(suc(X1)))
| 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'LE'(f(suc(X1)),s(s(s(s(s('0')))))) ),
clause_297 ).
cnf(c_0_82,plain,
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_74,c_0_75]),c_0_76]),c_0_77]) ).
cnf(c_0_83,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78,c_0_79])]) ).
cnf(c_0_84,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_80,c_0_79])]) ).
cnf(c_0_85,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_81,c_0_79])]) ).
cnf(c_0_86,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_83]),c_0_84]),c_0_85]) ).
cnf(c_0_87,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1)) ),
clause_473 ).
cnf(c_0_88,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1))) ),
clause_698 ).
cnf(c_0_89,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X3))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X3)))
| ~ 'E'(s(s(s(s('0')))),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_83]),c_0_84]),c_0_85]) ).
cnf(c_0_90,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1)) ),
inference(csr,[status(thm)],[c_0_87,c_0_88]) ).
cnf(c_0_91,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) ),
clause_715 ).
cnf(c_0_92,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3))) ),
clause_249 ).
cnf(c_0_93,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1))) ),
clause_314 ).
cnf(c_0_94,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1))) ),
clause_968 ).
cnf(c_0_95,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'LE'(f(X3),s(s(s(s('0')))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_83]),c_0_84]),c_0_85]) ).
cnf(c_0_96,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_83]),c_0_84]),c_0_85]) ).
cnf(c_0_97,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) ),
clause_915 ).
cnf(c_0_98,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ '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(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3)) ),
inference(csr,[status(thm)],[c_0_91,c_0_92]) ).
cnf(c_0_99,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[c_0_93,c_0_92]) ).
cnf(c_0_100,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3)))) ),
clause_514 ).
cnf(c_0_101,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[c_0_94,c_0_92]) ).
cnf(c_0_102,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2))) ),
clause_114 ).
cnf(c_0_103,plain,
( 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0')))))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(spm,[status(thm)],[c_0_95,c_0_96]) ).
cnf(c_0_104,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3)))) ),
clause_1016 ).
cnf(c_0_105,plain,
( 'E'(f(X1),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(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_97,c_0_98]),c_0_99]) ).
cnf(c_0_106,plain,
( 'E'(f(X1),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(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_100,c_0_98]),c_0_101]) ).
cnf(c_0_107,plain,
( 'E'(f(X1),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(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_102,c_0_99]),c_0_101]) ).
cnf(c_0_108,axiom,
( 'E'(s(s(s('0'))),f(suc(suc(X1))))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0'))))) ),
clause_1123 ).
cnf(c_0_109,plain,
'LE'(f(X1),s(s(s(s('0'))))),
inference(spm,[status(thm)],[c_0_103,c_0_96]) ).
cnf(c_0_110,axiom,
( 'E'(s(s(s('0'))),f(X1))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'LE'(f(X1),s(s(s(s('0'))))) ),
clause_24 ).
cnf(c_0_111,axiom,
( 'E'(s(s(s('0'))),f(suc(X1)))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'LE'(f(suc(X1)),s(s(s(s('0'))))) ),
clause_269 ).
cnf(c_0_112,plain,
( ~ 'E'(s(s(s('0'))),f(suc(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(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_104,c_0_105]),c_0_106]),c_0_107]) ).
cnf(c_0_113,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_108,c_0_109])]) ).
cnf(c_0_114,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_110,c_0_109])]) ).
cnf(c_0_115,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_111,c_0_109])]) ).
cnf(c_0_116,plain,
( 'LE'(f(X1),s(s(s('0'))))
| ~ '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(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_112,c_0_113]),c_0_114]),c_0_115]) ).
cnf(c_0_117,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1)) ),
clause_1023 ).
cnf(c_0_118,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X1))) ),
clause_171 ).
cnf(c_0_119,plain,
( 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X3))))
| ~ 'E'(s(s(s('0'))),f(suc(X3)))
| ~ 'E'(s(s(s('0'))),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_113]),c_0_114]),c_0_115]) ).
cnf(c_0_120,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1)) ),
inference(csr,[status(thm)],[c_0_117,c_0_118]) ).
cnf(c_0_121,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_335 ).
cnf(c_0_122,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(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(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_778 ).
cnf(c_0_123,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(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(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_64 ).
cnf(c_0_124,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(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(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_722 ).
cnf(c_0_125,plain,
( 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X3),s(s(s('0'))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_113]),c_0_114]),c_0_115]) ).
cnf(c_0_126,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_120,c_0_113]),c_0_114]),c_0_115]) ).
cnf(c_0_127,axiom,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_191 ).
cnf(c_0_128,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3)) ),
inference(csr,[status(thm)],[c_0_121,c_0_122]) ).
cnf(c_0_129,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ '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(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[c_0_123,c_0_122]) ).
cnf(c_0_130,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_985 ).
cnf(c_0_131,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[c_0_124,c_0_122]) ).
cnf(c_0_132,axiom,
( 'E'(f(X3),f(suc(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(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_207 ).
cnf(c_0_133,plain,
( 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(spm,[status(thm)],[c_0_125,c_0_126]) ).
cnf(c_0_134,axiom,
( ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2)) ),
clause_115 ).
cnf(c_0_135,plain,
( 'E'(f(X1),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(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_127,c_0_128]),c_0_129]) ).
cnf(c_0_136,plain,
( 'E'(f(X1),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(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_130,c_0_128]),c_0_131]) ).
cnf(c_0_137,plain,
( 'E'(f(X1),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(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_132,c_0_129]),c_0_131]) ).
cnf(c_0_138,axiom,
( 'E'(s(s('0')),f(suc(suc(X1))))
| 'LE'(f(X1),s(s('0')))
| ~ 'LE'(f(suc(suc(X1))),s(s(s('0')))) ),
clause_569 ).
cnf(c_0_139,plain,
'LE'(f(X1),s(s(s('0')))),
inference(spm,[status(thm)],[c_0_133,c_0_126]) ).
cnf(c_0_140,axiom,
( 'E'(s(s('0')),f(X1))
| 'LE'(f(X1),s(s('0')))
| ~ 'LE'(f(X1),s(s(s('0')))) ),
clause_1143 ).
cnf(c_0_141,axiom,
( 'E'(s(s('0')),f(suc(X1)))
| 'LE'(f(X1),s(s('0')))
| ~ 'LE'(f(suc(X1)),s(s(s('0')))) ),
clause_773 ).
cnf(c_0_142,plain,
( ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(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(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_134,c_0_135]),c_0_136]),c_0_137]) ).
cnf(c_0_143,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_138,c_0_139])]) ).
cnf(c_0_144,plain,
( 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_140,c_0_139])]) ).
cnf(c_0_145,plain,
( 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141,c_0_139])]) ).
cnf(c_0_146,plain,
( 'LE'(f(X1),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_143]),c_0_144]),c_0_145]) ).
cnf(c_0_147,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1)) ),
clause_237 ).
cnf(c_0_148,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X1))) ),
clause_794 ).
cnf(c_0_149,plain,
( 'LE'(f(X1),s(s('0')))
| 'LE'(f(X2),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(suc(X3))))
| ~ 'E'(s(s('0')),f(suc(X3)))
| ~ 'E'(s(s('0')),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_146,c_0_143]),c_0_144]),c_0_145]) ).
cnf(c_0_150,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1)) ),
inference(csr,[status(thm)],[c_0_147,c_0_148]) ).
cnf(c_0_151,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
clause_912 ).
cnf(c_0_152,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
clause_694 ).
cnf(c_0_153,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
clause_174 ).
cnf(c_0_154,axiom,
( 'E'(f(X3),f(suc(X3)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
clause_826 ).
cnf(c_0_155,plain,
( 'LE'(f(X1),s(s('0')))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X3),s(s('0')))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_149,c_0_143]),c_0_144]),c_0_145]) ).
cnf(c_0_156,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_150,c_0_143]),c_0_144]),c_0_145]) ).
cnf(c_0_157,axiom,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
clause_709 ).
cnf(c_0_158,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[c_0_151,c_0_152]) ).
cnf(c_0_159,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[c_0_153,c_0_152]) ).
cnf(c_0_160,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X2)) ),
clause_447 ).
cnf(c_0_161,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3)) ),
inference(csr,[status(thm)],[c_0_154,c_0_152]) ).
cnf(c_0_162,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
clause_281 ).
cnf(c_0_163,plain,
( 'LE'(f(X1),s(s('0')))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(spm,[status(thm)],[c_0_155,c_0_156]) ).
cnf(c_0_164,axiom,
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
clause_813 ).
cnf(c_0_165,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_157,c_0_158]),c_0_159]) ).
cnf(c_0_166,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_160,c_0_158]),c_0_161]) ).
cnf(c_0_167,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_162,c_0_159]),c_0_161]) ).
cnf(c_0_168,axiom,
( 'E'(s('0'),f(suc(suc(X1))))
| 'LE'(f(X1),s('0'))
| ~ 'LE'(f(suc(suc(X1))),s(s('0'))) ),
clause_160 ).
cnf(c_0_169,plain,
'LE'(f(X1),s(s('0'))),
inference(spm,[status(thm)],[c_0_163,c_0_156]) ).
cnf(c_0_170,axiom,
( 'E'(s('0'),f(X1))
| 'LE'(f(X1),s('0'))
| ~ 'LE'(f(X1),s(s('0'))) ),
clause_1158 ).
cnf(c_0_171,axiom,
( 'E'(s('0'),f(suc(X1)))
| 'LE'(f(X1),s('0'))
| ~ 'LE'(f(suc(X1)),s(s('0'))) ),
clause_149 ).
cnf(c_0_172,plain,
( ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_164,c_0_165]),c_0_166]),c_0_167]) ).
cnf(c_0_173,plain,
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_168,c_0_169])]) ).
cnf(c_0_174,plain,
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_170,c_0_169])]) ).
cnf(c_0_175,plain,
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_171,c_0_169])]) ).
cnf(c_0_176,plain,
( 'LE'(f(X1),s('0'))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_172,c_0_173]),c_0_174]),c_0_175]) ).
cnf(c_0_177,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1)) ),
clause_340 ).
cnf(c_0_178,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1))) ),
clause_1089 ).
cnf(c_0_179,plain,
( 'LE'(f(X1),s('0'))
| 'LE'(f(X2),s('0'))
| ~ 'E'(s('0'),f(suc(suc(X3))))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_176,c_0_173]),c_0_174]),c_0_175]) ).
cnf(c_0_180,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1)) ),
inference(csr,[status(thm)],[c_0_177,c_0_178]) ).
cnf(c_0_181,plain,
( 'LE'(f(X1),s('0'))
| 'LE'(f(X2),s('0'))
| 'LE'(f(X3),s('0'))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_179,c_0_173]),c_0_174]),c_0_175]) ).
cnf(c_0_182,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_180,c_0_173]),c_0_174]),c_0_175]) ).
cnf(c_0_183,plain,
( 'LE'(f(X1),s('0'))
| 'LE'(f(X2),s('0'))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(spm,[status(thm)],[c_0_181,c_0_182]) ).
cnf(c_0_184,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
clause_699 ).
cnf(c_0_185,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
clause_303 ).
cnf(c_0_186,axiom,
( 'E'('0',f(suc(suc(X1))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(X1))),s('0')) ),
clause_840 ).
cnf(c_0_187,plain,
'LE'(f(X1),s('0')),
inference(spm,[status(thm)],[c_0_183,c_0_182]) ).
cnf(c_0_188,axiom,
( 'E'('0',f(X1))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(X1),s('0')) ),
clause_199 ).
cnf(c_0_189,axiom,
( 'E'('0',f(suc(X1)))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(X1)),s('0')) ),
clause_713 ).
cnf(c_0_190,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(csr,[status(thm)],[c_0_184,c_0_185]) ).
cnf(c_0_191,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_186,c_0_187])]) ).
cnf(c_0_192,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_188,c_0_187])]) ).
cnf(c_0_193,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_189,c_0_187])]) ).
cnf(c_0_194,axiom,
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
clause_483 ).
cnf(c_0_195,plain,
( 'LE'(f(X1),'0')
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_190,c_0_191]),c_0_192]),c_0_193]) ).
cnf(c_0_196,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
clause_910 ).
cnf(c_0_197,axiom,
~ 'LE'(f(z),'0'),
clause_546 ).
cnf(c_0_198,axiom,
( ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
clause_743 ).
cnf(c_0_199,plain,
( 'LE'(f(X1),'0')
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_194,c_0_191]),c_0_192]),c_0_193]),c_0_195]) ).
cnf(c_0_200,plain,
( 'LE'(f(X1),'0')
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_191]),c_0_192]),c_0_193]),c_0_195]) ).
cnf(c_0_201,plain,
'E'('0',f(suc(z))),
inference(spm,[status(thm)],[c_0_197,c_0_193]) ).
cnf(c_0_202,plain,
'E'('0',f(z)),
inference(spm,[status(thm)],[c_0_197,c_0_192]) ).
cnf(c_0_203,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1))) ),
clause_106 ).
cnf(c_0_204,plain,
( 'LE'(f(X1),'0')
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_191]),c_0_192]),c_0_193]),c_0_199]),c_0_200]) ).
cnf(c_0_205,plain,
( 'E'(f(z),f(suc(z)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(z))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_185,c_0_201]),c_0_202])]) ).
cnf(c_0_206,plain,
( 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_203,c_0_201]),c_0_202])]) ).
cnf(c_0_207,plain,
( 'LE'(f(X1),'0')
| 'LE'(f(X2),'0')
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_204,c_0_191]),c_0_192]),c_0_193]) ).
cnf(c_0_208,plain,
( 'E'(f(z),f(suc(z)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X1),suc(z)) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_201]),c_0_202])]),c_0_206]) ).
cnf(c_0_209,plain,
( 'LE'(f(X1),'0')
| 'LE'(f(X2),'0')
| 'LE'(f(X3),'0')
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_207,c_0_191]),c_0_192]),c_0_193]) ).
cnf(c_0_210,plain,
'E'(f(z),f(suc(z))),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_208,c_0_201]),c_0_202])]),c_0_206]) ).
cnf(c_0_211,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
clause_256 ).
cnf(c_0_212,plain,
( 'LE'(f(X1),'0')
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X1),suc(z))
| ~ iLEQ(suc(X2),suc(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_209,c_0_210]),c_0_197]) ).
cnf(c_0_213,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[c_0_211,c_0_203]) ).
cnf(c_0_214,plain,
( 'LE'(f(X1),'0')
| ~ 'E'('0',f(suc(suc(z))))
| ~ iLEQ(suc(X1),suc(z)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_212,c_0_213]),c_0_201]),c_0_202])]),c_0_197]) ).
cnf(c_0_215,plain,
~ 'E'('0',f(suc(suc(z)))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_214,c_0_213]),c_0_201]),c_0_202])]),c_0_197]) ).
cnf(c_0_216,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_215,c_0_191]),c_0_197]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO688-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n019.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 09:20:44 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 3.26/3.11 % Version : CSE_E---1.7
% 3.26/3.11 % Problem : theBenchmark.p
% 3.26/3.11 % SZS status Unsatisfiable for theBenchmark.p
% 3.26/3.11 % SZS output start CNFRefutation
% See solution above
% 3.26/3.12 % Total time : 2.581s
%------------------------------------------------------------------------------