%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYO651-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 : n002.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:28 PM UTC 2026
% Result : Unsatisfiable 1.56s 1.82s
% Output : CNFRefutation 1.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 74
% Syntax : Number of clauses : 234 ( 11 unt; 190 nHn; 226 RR)
% Number of literals : 3530 ( 0 equ;3029 neg)
% Maximal clause size : 26 ( 15 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 : 609 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1875,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1875) ).
cnf(clause_2887,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(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2887) ).
cnf(clause_3275,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3275) ).
cnf(clause_1550,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1550) ).
cnf(clause_1816,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1816) ).
cnf(clause_1366,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1366) ).
cnf(clause_896,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_896) ).
cnf(clause_3823,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3823) ).
cnf(clause_3679,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3679) ).
cnf(clause_1427,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1427) ).
cnf(clause_2899,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2899) ).
cnf(clause_2665,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2665) ).
cnf(clause_1375,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1375) ).
cnf(clause_3408,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3408) ).
cnf(clause_2612,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2612) ).
cnf(clause_2277,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2277) ).
cnf(clause_408,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_408) ).
cnf(clause_3339,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3339) ).
cnf(clause_492,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_492) ).
cnf(clause_2573,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2573) ).
cnf(clause_935,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_935) ).
cnf(clause_1229,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1229) ).
cnf(clause_1587,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1587) ).
cnf(clause_2312,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2312) ).
cnf(clause_3718,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3718) ).
cnf(clause_2195,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2195) ).
cnf(clause_2518,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2518) ).
cnf(clause_2721,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2721) ).
cnf(clause_1536,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1536) ).
cnf(clause_3412,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3412) ).
cnf(clause_1564,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1564) ).
cnf(clause_3129,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3129) ).
cnf(clause_3155,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3155) ).
cnf(clause_627,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_627) ).
cnf(clause_733,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_733) ).
cnf(clause_3677,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3677) ).
cnf(clause_2054,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2054) ).
cnf(clause_3578,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3578) ).
cnf(clause_2891,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2891) ).
cnf(clause_249,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_249) ).
cnf(clause_930,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_930) ).
cnf(clause_55,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_55) ).
cnf(clause_613,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_613) ).
cnf(clause_752,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_752) ).
cnf(clause_3337,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3337) ).
cnf(clause_2529,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2529) ).
cnf(clause_1318,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1318) ).
cnf(clause_1532,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1532) ).
cnf(clause_3274,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3274) ).
cnf(clause_698,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_698) ).
cnf(clause_426,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_426) ).
cnf(clause_187,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_187) ).
cnf(clause_2015,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2015) ).
cnf(clause_2993,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 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_2993) ).
cnf(clause_636,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_636) ).
cnf(clause_960,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_960) ).
cnf(clause_3575,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3575) ).
cnf(clause_2802,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2802) ).
cnf(clause_2744,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2744) ).
cnf(clause_3669,axiom,
( 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3669) ).
cnf(clause_255,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_255) ).
cnf(clause_1772,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1772) ).
cnf(clause_3827,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3827) ).
cnf(clause_1098,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1098) ).
cnf(clause_403,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_403) ).
cnf(clause_1563,axiom,
( 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1563) ).
cnf(clause_3293,axiom,
( 'E'('0',f(suc(suc(suc(X1)))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(suc(X1)))),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3293) ).
cnf(clause_3530,axiom,
'LE'(f(X1),s('0')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3530) ).
cnf(clause_3112,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_3112) ).
cnf(clause_2650,axiom,
( 'E'('0',f(suc(X1)))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(X1)),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2650) ).
cnf(clause_2386,axiom,
( 'E'('0',f(X1))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(X1),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2386) ).
cnf(clause_619,axiom,
( 'E'('0',f(suc(suc(suc(suc(X1))))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(suc(suc(X1))))),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_619) ).
cnf(clause_3360,axiom,
( ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3360) ).
cnf(clause_1829,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1829) ).
cnf(c_0_74,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_1875 ).
cnf(c_0_75,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(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_2887 ).
cnf(c_0_76,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_3275 ).
cnf(c_0_77,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_1550 ).
cnf(c_0_78,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_1816 ).
cnf(c_0_79,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_80,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_1366 ).
cnf(c_0_81,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[c_0_76,c_0_75]) ).
cnf(c_0_82,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_896 ).
cnf(c_0_83,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3823 ).
cnf(c_0_84,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[c_0_77,c_0_75]) ).
cnf(c_0_85,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3679 ).
cnf(c_0_86,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_1427 ).
cnf(c_0_87,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_2899 ).
cnf(c_0_88,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_2665 ).
cnf(c_0_89,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_78,c_0_75]),c_0_79]) ).
cnf(c_0_90,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_80,c_0_81]),c_0_79]) ).
cnf(c_0_91,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_1375 ).
cnf(c_0_92,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_82,c_0_75]),c_0_81]) ).
cnf(c_0_93,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_3408 ).
cnf(c_0_94,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_83,c_0_79]),c_0_84]) ).
cnf(c_0_95,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2612 ).
cnf(c_0_96,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_85,c_0_81]),c_0_84]) ).
cnf(c_0_97,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2277 ).
cnf(c_0_98,axiom,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_408 ).
cnf(c_0_99,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3339 ).
cnf(c_0_100,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_86,c_0_75]),c_0_84]) ).
cnf(c_0_101,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_492 ).
cnf(c_0_102,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2573 ).
cnf(c_0_103,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_935 ).
cnf(c_0_104,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_87,c_0_75]),c_0_79]) ).
cnf(c_0_105,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_88,c_0_81]),c_0_89]),c_0_90]) ).
cnf(c_0_106,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X2))) ),
clause_1229 ).
cnf(c_0_107,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_91,c_0_92]),c_0_79]),c_0_90]) ).
cnf(c_0_108,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_1587 ).
cnf(c_0_109,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_93,c_0_84]),c_0_89]),c_0_94]) ).
cnf(c_0_110,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_2312 ).
cnf(c_0_111,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_95,c_0_90]),c_0_96]),c_0_94]) ).
cnf(c_0_112,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3718 ).
cnf(c_0_113,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_97,c_0_92]),c_0_84]),c_0_96]) ).
cnf(c_0_114,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2195 ).
cnf(c_0_115,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_98,c_0_75]),c_0_81]) ).
cnf(c_0_116,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2518 ).
cnf(c_0_117,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_99,c_0_81]),c_0_100]),c_0_96]) ).
cnf(c_0_118,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_2721 ).
cnf(c_0_119,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_1536 ).
cnf(c_0_120,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_101,c_0_79]),c_0_100]),c_0_94]) ).
cnf(c_0_121,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_3412 ).
cnf(c_0_122,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_1564 ).
cnf(c_0_123,plain,
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_102,c_0_75]),c_0_84]) ).
cnf(c_0_124,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3129 ).
cnf(c_0_125,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_3155 ).
cnf(c_0_126,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_103,c_0_81]),c_0_104]),c_0_90]),c_0_105]) ).
cnf(c_0_127,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_106,c_0_92]),c_0_89]),c_0_107]),c_0_105]) ).
cnf(c_0_128,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_627 ).
cnf(c_0_129,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_108,c_0_84]),c_0_104]),c_0_94]),c_0_109]) ).
cnf(c_0_130,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_110,c_0_96]),c_0_105]),c_0_109]),c_0_111]) ).
cnf(c_0_131,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_733 ).
cnf(c_0_132,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_112,c_0_107]),c_0_113]),c_0_94]),c_0_111]) ).
cnf(c_0_133,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3677 ).
cnf(c_0_134,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_114,c_0_115]),c_0_84]),c_0_96]),c_0_113]) ).
cnf(c_0_135,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_116,c_0_92]),c_0_100]),c_0_113]),c_0_117]) ).
cnf(c_0_136,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2054 ).
cnf(c_0_137,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_118,c_0_115]),c_0_79]),c_0_90]),c_0_107]) ).
cnf(c_0_138,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_3578 ).
cnf(c_0_139,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_119,c_0_90]),c_0_117]),c_0_120]),c_0_111]) ).
cnf(c_0_140,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_2891 ).
cnf(c_0_141,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_249 ).
cnf(c_0_142,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_121,c_0_100]),c_0_89]),c_0_120]),c_0_109]) ).
cnf(c_0_143,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_930 ).
cnf(c_0_144,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_55 ).
cnf(c_0_145,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_122,c_0_79]),c_0_123]),c_0_94]),c_0_120]) ).
cnf(c_0_146,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_613 ).
cnf(c_0_147,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_124,c_0_81]),c_0_123]),c_0_96]),c_0_117]) ).
cnf(c_0_148,axiom,
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_752 ).
cnf(c_0_149,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(X2))) ),
clause_3337 ).
cnf(c_0_150,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_2529 ).
cnf(c_0_151,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_125,c_0_92]),c_0_104]),c_0_107]),c_0_126]),c_0_127]) ).
cnf(c_0_152,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_128,c_0_96]),c_0_126]),c_0_129]),c_0_111]),c_0_130]) ).
cnf(c_0_153,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_131,c_0_113]),c_0_127]),c_0_109]),c_0_132]),c_0_130]) ).
cnf(c_0_154,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_1318 ).
cnf(c_0_155,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_133,c_0_115]),c_0_100]),c_0_134]),c_0_117]),c_0_135]) ).
cnf(c_0_156,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_136,c_0_137]),c_0_134]),c_0_94]),c_0_111]),c_0_132]) ).
cnf(c_0_157,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_138,c_0_107]),c_0_135]),c_0_120]),c_0_132]),c_0_139]) ).
cnf(c_0_158,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_1532 ).
cnf(c_0_159,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_140,c_0_115]),c_0_89]),c_0_137]),c_0_105]),c_0_127]) ).
cnf(c_0_160,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_3274 ).
cnf(c_0_161,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_141,c_0_117]),c_0_105]),c_0_142]),c_0_139]),c_0_130]) ).
cnf(c_0_162,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_698 ).
cnf(c_0_163,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_143,c_0_100]),c_0_104]),c_0_120]),c_0_129]),c_0_142]) ).
cnf(c_0_164,axiom,
( 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_426 ).
cnf(c_0_165,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_187 ).
cnf(c_0_166,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_144,c_0_123]),c_0_89]),c_0_145]),c_0_109]),c_0_142]) ).
cnf(c_0_167,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_146,c_0_90]),c_0_147]),c_0_145]),c_0_111]),c_0_139]) ).
cnf(c_0_168,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_2015 ).
cnf(c_0_169,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_148,c_0_92]),c_0_123]),c_0_113]),c_0_147]),c_0_135]) ).
cnf(c_0_170,axiom,
( 'E'(f(X1),f(suc(suc(X1))))
| 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_2993 ).
cnf(c_0_171,axiom,
( 'E'(f(X1),f(suc(X1)))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1))) ),
clause_636 ).
cnf(c_0_172,axiom,
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_960 ).
cnf(c_0_173,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_3575 ).
cnf(c_0_174,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_149,c_0_115]),c_0_104]),c_0_137]),c_0_126]) ).
cnf(c_0_175,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_150,c_0_113]),c_0_151]),c_0_129]),c_0_132]),c_0_152]),c_0_153]) ).
cnf(c_0_176,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_2802 ).
cnf(c_0_177,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_154,c_0_137]),c_0_155]),c_0_120]),c_0_156]),c_0_139]),c_0_157]) ).
cnf(c_0_178,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_158,c_0_134]),c_0_159]),c_0_109]),c_0_156]),c_0_130]),c_0_153]) ).
cnf(c_0_179,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_160,c_0_135]),c_0_127]),c_0_142]),c_0_157]),c_0_153]),c_0_161]) ).
cnf(c_0_180,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_2744 ).
cnf(c_0_181,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_162,c_0_117]),c_0_126]),c_0_163]),c_0_139]),c_0_152]),c_0_161]) ).
cnf(c_0_182,axiom,
( 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_3669 ).
cnf(c_0_183,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_164,c_0_123]),c_0_104]),c_0_145]),c_0_129]) ).
cnf(c_0_184,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_165,c_0_147]),c_0_105]),c_0_166]),c_0_167]),c_0_130]),c_0_161]) ).
cnf(c_0_185,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_255 ).
cnf(c_0_186,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_168,c_0_107]),c_0_169]),c_0_145]),c_0_132]),c_0_167]),c_0_157]) ).
cnf(c_0_187,axiom,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1)))))) ),
clause_1772 ).
cnf(c_0_188,plain,
( iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[c_0_170,c_0_171]) ).
cnf(c_0_189,axiom,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1))) ),
clause_3827 ).
cnf(c_0_190,axiom,
( 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1))) ),
clause_1098 ).
cnf(c_0_191,plain,
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_172,c_0_115]),c_0_123]),c_0_134]),c_0_147]) ).
cnf(c_0_192,axiom,
( 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_403 ).
cnf(c_0_193,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_173,c_0_134]),c_0_174]),c_0_129]),c_0_156]),c_0_152]),c_0_175]) ).
cnf(c_0_194,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ '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)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_176,c_0_155]),c_0_159]),c_0_142]),c_0_177]),c_0_178]),c_0_161]),c_0_179]) ).
cnf(c_0_195,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_180,c_0_135]),c_0_151]),c_0_163]),c_0_157]),c_0_175]),c_0_181]),c_0_179]) ).
cnf(c_0_196,axiom,
( 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_1563 ).
cnf(c_0_197,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_182,c_0_147]),c_0_126]),c_0_183]),c_0_167]),c_0_152]),c_0_184]),c_0_181]) ).
cnf(c_0_198,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_185,c_0_169]),c_0_127]),c_0_166]),c_0_186]),c_0_153]),c_0_184]),c_0_179]) ).
cnf(c_0_199,axiom,
( 'E'('0',f(suc(suc(suc(X1)))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(suc(X1)))),s('0')) ),
clause_3293 ).
cnf(c_0_200,axiom,
'LE'(f(X1),s('0')),
clause_3530 ).
cnf(c_0_201,axiom,
( 'E'('0',f(suc(suc(X1))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(X1))),s('0')) ),
clause_3112 ).
cnf(c_0_202,axiom,
( 'E'('0',f(suc(X1)))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(X1)),s('0')) ),
clause_2650 ).
cnf(c_0_203,axiom,
( 'E'('0',f(X1))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(X1),s('0')) ),
clause_2386 ).
cnf(c_0_204,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_187,c_0_171]),c_0_188]) ).
cnf(c_0_205,plain,
( iLEQ(suc(X1),suc(X1))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_189,c_0_171]),c_0_188]) ).
cnf(c_0_206,axiom,
( 'E'('0',f(suc(suc(suc(suc(X1))))))
| 'LE'(f(X1),'0')
| ~ 'LE'(f(suc(suc(suc(suc(X1))))),s('0')) ),
clause_619 ).
cnf(c_0_207,axiom,
( ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X2))) ),
clause_3360 ).
cnf(c_0_208,plain,
( 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_190,c_0_137]),c_0_191]),c_0_145]),c_0_156]),c_0_167]) ).
cnf(c_0_209,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_192,c_0_155]),c_0_174]),c_0_163]),c_0_177]),c_0_193]),c_0_181]),c_0_194]),c_0_195]) ).
cnf(c_0_210,plain,
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_196,c_0_169]),c_0_151]),c_0_183]),c_0_186]),c_0_175]),c_0_197]),c_0_198]),c_0_195]) ).
cnf(c_0_211,axiom,
~ 'LE'(f(z),'0'),
clause_1829 ).
cnf(c_0_212,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(suc(X1))))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_199,c_0_200])]) ).
cnf(c_0_213,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(X1)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_201,c_0_200])]) ).
cnf(c_0_214,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_202,c_0_200])]) ).
cnf(c_0_215,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_203,c_0_200])]) ).
cnf(c_0_216,plain,
( iLEQ(suc(X1),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
inference(csr,[status(thm)],[c_0_204,c_0_205]) ).
cnf(c_0_217,plain,
( 'LE'(f(X1),'0')
| 'E'('0',f(suc(suc(suc(suc(X1)))))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_206,c_0_200])]) ).
cnf(c_0_218,plain,
( ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_207,c_0_191]),c_0_174]),c_0_183]),c_0_208]),c_0_193]),c_0_197]),c_0_209]),c_0_210]) ).
cnf(c_0_219,plain,
'E'('0',f(suc(suc(suc(z))))),
inference(spm,[status(thm)],[c_0_211,c_0_212]) ).
cnf(c_0_220,plain,
'E'('0',f(suc(suc(z)))),
inference(spm,[status(thm)],[c_0_211,c_0_213]) ).
cnf(c_0_221,plain,
'E'('0',f(suc(z))),
inference(spm,[status(thm)],[c_0_211,c_0_214]) ).
cnf(c_0_222,plain,
'E'('0',f(z)),
inference(spm,[status(thm)],[c_0_211,c_0_215]) ).
cnf(c_0_223,plain,
( 'LE'(f(X1),'0')
| iLEQ(suc(X1),suc(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_216,c_0_217]),c_0_215]),c_0_214]),c_0_213]),c_0_212]) ).
cnf(c_0_224,plain,
( 'LE'(f(X1),'0')
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X3),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(suc(X2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_218,c_0_217]),c_0_215]),c_0_214]),c_0_213]),c_0_212]) ).
cnf(c_0_225,plain,
( 'E'(f(z),f(suc(suc(suc(z)))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X2),f(suc(suc(suc(X2)))))
| ~ iLEQ(suc(X2),suc(z))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_179,c_0_219]),c_0_220]),c_0_221]),c_0_222])]) ).
cnf(c_0_226,plain,
iLEQ(suc(z),suc(z)),
inference(spm,[status(thm)],[c_0_211,c_0_223]) ).
cnf(c_0_227,plain,
( 'LE'(f(X1),'0')
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(suc(X3))))))
| ~ 'E'(f(X3),f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X3)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_224,c_0_217]),c_0_215]),c_0_214]),c_0_213]),c_0_212]) ).
cnf(c_0_228,plain,
( 'E'(f(z),f(suc(suc(suc(z)))))
| 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X1),suc(z))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_225,c_0_219]),c_0_226]),c_0_220]),c_0_221]),c_0_222])]) ).
cnf(c_0_229,plain,
( 'LE'(f(X1),'0')
| 'LE'(f(X2),'0')
| 'LE'(f(X3),'0')
| ~ iLEQ(suc(X3),suc(X2))
| ~ iLEQ(suc(X1),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(suc(X1))))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_227,c_0_217]),c_0_215]),c_0_214]),c_0_213]),c_0_212]) ).
cnf(c_0_230,plain,
'E'(f(z),f(suc(suc(suc(z))))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_228,c_0_219]),c_0_226]),c_0_220]),c_0_221]),c_0_222])]) ).
cnf(c_0_231,plain,
( 'LE'(f(X1),'0')
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(z),suc(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_229,c_0_230]),c_0_211]) ).
cnf(c_0_232,plain,
( 'LE'(f(X1),'0')
| ~ iLEQ(suc(z),suc(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_231,c_0_226]),c_0_211]) ).
cnf(c_0_233,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_211,c_0_232]),c_0_226])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO651-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 : n002.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:19:31 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.56/1.82 % Version : CSE_E---1.7
% 1.56/1.82 % Problem : theBenchmark.p
% 1.56/1.82 % SZS status Unsatisfiable for theBenchmark.p
% 1.56/1.82 % SZS output start CNFRefutation
% See solution above
% 1.56/1.83 % Total time : 1.421s
%------------------------------------------------------------------------------