%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:47:54 AM UTC 2026
% Result : Unsatisfiable 241.12s 35.47s
% Output : CNFRefutation 241.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_299,axiom,
'\'LE\''(f(X0),s(s(s(s(s('\'0\'')))))) ).
cnf(clause_743,axiom,
( ~ '\'E\''('\'0\'',f(X2))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ) ).
cnf(clause_773,axiom,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'LE\''(f(suc(X0)),s(s(s('\'0\'')))) ) ).
cnf(clause_1123,axiom,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'LE\''(f(suc(suc(X0))),s(s(s(s('\'0\''))))) ) ).
cnf(clause_171,axiom,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0)) ) ).
cnf(clause_1158,axiom,
( '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(s('\'0\''),f(X0))
| ~ '\'LE\''(f(X0),s(s('\'0\''))) ) ).
cnf(clause_269,axiom,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'LE\''(f(suc(X0)),s(s(s(s('\'0\''))))) ) ).
cnf(clause_1023,axiom,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ) ).
cnf(clause_199,axiom,
( '\'LE\''(f(X0),'\'0\'')
| '\'E\''('\'0\'',f(X0))
| ~ '\'LE\''(f(X0),s('\'0\'')) ) ).
cnf(clause_237,axiom,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s('\'0\'')),f(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ) ).
cnf(clause_340,axiom,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s('\'0\''),f(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0)))) ) ).
cnf(clause_546,axiom,
~ '\'LE\''(f(z),'\'0\'') ).
cnf(clause_813,axiom,
( ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s('\'0\''),f(X1))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(s('\'0\''),f(X2))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(X0)) ) ).
cnf(clause_436,axiom,
( ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X2))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ) ).
cnf(clause_473,axiom,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ) ).
cnf(clause_1143,axiom,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s(s('\'0\'')),f(X0))
| ~ '\'LE\''(f(X0),s(s(s('\'0\'')))) ) ).
cnf(clause_160,axiom,
( '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'LE\''(f(suc(suc(X0))),s(s('\'0\''))) ) ).
cnf(clause_231,axiom,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'LE\''(f(suc(suc(X0))),s(s(s(s(s('\'0\'')))))) ) ).
cnf(clause_106,axiom,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(X0)) ) ).
cnf(clause_778,axiom,
( '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(X1))
| ~ '\'E\''(s(s('\'0\'')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(s(s('\'0\'')),f(X2))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ) ).
cnf(clause_840,axiom,
( '\'LE\''(f(X0),'\'0\'')
| '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'LE\''(f(suc(suc(X0))),s('\'0\'')) ) ).
cnf(clause_149,axiom,
( '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'LE\''(f(suc(X0)),s(s('\'0\''))) ) ).
cnf(clause_256,axiom,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''('\'0\'',f(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0)))) ) ).
cnf(clause_694,axiom,
( '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(s('\'0\''),f(X2))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(s('\'0\''),f(X1))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(X0)) ) ).
cnf(clause_105,axiom,
( '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X1))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ) ).
cnf(clause_1089,axiom,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(X0)) ) ).
cnf(clause_298,axiom,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| ~ '\'LE\''(f(X0),s(s(s(s(s('\'0\'')))))) ) ).
cnf(clause_569,axiom,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'LE\''(f(suc(suc(X0))),s(s(s('\'0\'')))) ) ).
cnf(clause_1016,axiom,
( ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ) ).
cnf(clause_794,axiom,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(X0)) ) ).
cnf(clause_115,axiom,
( ~ '\'E\''(s(s('\'0\'')),f(X1))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ) ).
cnf(clause_303,axiom,
( '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(X2))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ) ).
cnf(clause_24,axiom,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s(s('\'0\''))),f(X0))
| ~ '\'LE\''(f(X0),s(s(s(s('\'0\''))))) ) ).
cnf(clause_713,axiom,
( '\'LE\''(f(X0),'\'0\'')
| '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'LE\''(f(suc(X0)),s('\'0\'')) ) ).
cnf(clause_698,axiom,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ) ).
cnf(clause_297,axiom,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'LE\''(f(suc(X0)),s(s(s(s(s('\'0\'')))))) ) ).
cnf(clause_249,axiom,
( '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ) ).
cnf(c91,plain,
'\'LE\''(f(X0),s(s(s(s(s('\'0\'')))))),
inference(clausification,[status(esa)],[clause_299]) ).
cnf(c124,plain,
( ~ '\'E\''('\'0\'',f(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''('\'0\'',f(X1))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(X0))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(clausification,[status(esa)],[clause_743]) ).
cnf(c134,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| ~ '\'LE\''(f(suc(X0)),s(s(s('\'0\''))))
| '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_773]) ).
cnf(c138,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ '\'LE\''(f(suc(suc(X0))),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ),
inference(clausification,[status(esa)],[clause_1123]) ).
cnf(c147,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_171]) ).
cnf(c152,plain,
( '\'LE\''(f(X0),s('\'0\''))
| ~ '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s('\'0\''),f(X0)) ),
inference(clausification,[status(esa)],[clause_1158]) ).
cnf(c168,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ '\'LE\''(f(suc(X0)),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_269]) ).
cnf(c189,plain,
( ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_1023]) ).
cnf(c225,plain,
( '\'LE\''(f(X0),'\'0\'')
| ~ '\'LE\''(f(X0),s('\'0\''))
| '\'E\''('\'0\'',f(X0)) ),
inference(clausification,[status(esa)],[clause_199]) ).
cnf(c278,plain,
( ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s('\'0\'')),f(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_237]) ).
cnf(c359,plain,
( ~ '\'E\''(s('\'0\''),f(X0))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_340]) ).
cnf(c365,plain,
~ '\'LE\''(f(z),'\'0\''),
inference(clausification,[status(esa)],[clause_546]) ).
cnf(c383,plain,
( ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(X0))
| ~ '\'E\''(s('\'0\''),f(X1))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_813]) ).
cnf(c401,plain,
( ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X1))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_436]) ).
cnf(c469,plain,
( ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(clausification,[status(esa)],[clause_473]) ).
cnf(c501,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| ~ '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s('\'0\'')),f(X0)) ),
inference(clausification,[status(esa)],[clause_1143]) ).
cnf(c534,plain,
( '\'LE\''(f(X0),s('\'0\''))
| ~ '\'LE\''(f(suc(suc(X0))),s(s('\'0\'')))
| '\'E\''(s('\'0\''),f(suc(suc(X0)))) ),
inference(clausification,[status(esa)],[clause_160]) ).
cnf(c579,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ '\'LE\''(f(suc(suc(X0))),s(s(s(s(s('\'0\''))))))
| '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ),
inference(clausification,[status(esa)],[clause_231]) ).
cnf(c580,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_106]) ).
cnf(c586,plain,
( ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(X1))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(X2))
| '\'E\''(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_778]) ).
cnf(c659,plain,
( '\'LE\''(f(X0),'\'0\'')
| ~ '\'LE\''(f(suc(suc(X0))),s('\'0\''))
| '\'E\''('\'0\'',f(suc(suc(X0)))) ),
inference(clausification,[status(esa)],[clause_840]) ).
cnf(c691,plain,
( '\'LE\''(f(X0),s('\'0\''))
| ~ '\'LE\''(f(suc(X0)),s(s('\'0\'')))
| '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_149]) ).
cnf(c719,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(X0)) ),
inference(clausification,[status(esa)],[clause_256]) ).
cnf(c755,plain,
( '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(X2))
| ~ '\'E\''(s('\'0\''),f(X0))
| ~ '\'E\''(s('\'0\''),f(X1))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(clausification,[status(esa)],[clause_694]) ).
cnf(c808,plain,
( '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X1))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_105]) ).
cnf(c851,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_1089]) ).
cnf(c893,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ '\'LE\''(f(X0),s(s(s(s(s('\'0\''))))))
| '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(clausification,[status(esa)],[clause_298]) ).
cnf(c913,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| ~ '\'LE\''(f(suc(suc(X0))),s(s(s('\'0\''))))
| '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ),
inference(clausification,[status(esa)],[clause_569]) ).
cnf(c931,plain,
( ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(X1))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0)) ),
inference(clausification,[status(esa)],[clause_1016]) ).
cnf(c942,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_794]) ).
cnf(c981,plain,
( ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(X1))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(X2))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(X0)) ),
inference(clausification,[status(esa)],[clause_115]) ).
cnf(c1029,plain,
( ~ '\'E\''('\'0\'',f(X1))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''('\'0\'',f(X0))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(X2))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(clausification,[status(esa)],[clause_303]) ).
cnf(c1030,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s('\'0\''))),f(X0)) ),
inference(clausification,[status(esa)],[clause_24]) ).
cnf(c1074,plain,
( '\'LE\''(f(X0),'\'0\'')
| ~ '\'LE\''(f(suc(X0)),s('\'0\''))
| '\'E\''('\'0\'',f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_713]) ).
cnf(c1084,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_698]) ).
cnf(c1150,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ '\'LE\''(f(suc(X0)),s(s(s(s(s('\'0\''))))))
| '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_297]) ).
cnf(c1159,plain,
( ~ '\'E\''(s(s(s('\'0\''))),f(X0))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(s(s(s('\'0\''))),f(X1))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(clausification,[status(esa)],[clause_249]) ).
cnf(d0,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c91,c1150]) ).
cnf(d1,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(resolution,[status(thm)],[c91,c893]) ).
cnf(d2,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c1084,d1]) ).
cnf(d3,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d2,d0]) ).
cnf(d4,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c91,c579]) ).
cnf(d5,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c469,d1]) ).
cnf(d6,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d5,d0]) ).
cnf(d7,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d6,d4]) ).
cnf(d8,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[d7,d3]) ).
cnf(d9,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X1))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(resolution,[status(thm)],[c808,d1]) ).
cnf(d10,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(resolution,[status(thm)],[d9,d1]) ).
cnf(d11,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d10,d1]) ).
cnf(d12,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d11,d0]) ).
cnf(d13,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d12,d0]) ).
cnf(d14,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d13,d0]) ).
cnf(d15,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d14,d8]) ).
cnf(d16,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d15,d8]) ).
cnf(d17,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X1))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(resolution,[status(thm)],[c401,d1]) ).
cnf(d18,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(X0)) ),
inference(resolution,[status(thm)],[d17,d1]) ).
cnf(d19,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d18,d1]) ).
cnf(d20,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d19,d0]) ).
cnf(d21,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d20,d0]) ).
cnf(d22,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d21,d0]) ).
cnf(d23,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d22,d4]) ).
cnf(d24,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s(s('\'0\'')))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d23,d4]) ).
cnf(d25,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d24,d4]) ).
cnf(d26,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d25,d16]) ).
cnf(d27,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d26,d16]) ).
cnf(d28,plain,
( '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X2),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d27,d16]) ).
cnf(d29,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X1),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d28,d8]) ).
cnf(d30,plain,
( '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\'')))))
| '\'LE\''(f(X0),s(s(s(s('\'0\''))))) ),
inference(resolution,[status(thm)],[d29,d8]) ).
cnf(d31,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d30,c168]) ).
cnf(d32,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s(s('\'0\''))),f(X0)) ),
inference(resolution,[status(thm)],[d30,c1030]) ).
cnf(d33,plain,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| '\'LE\''(f(X0),s(s(s('\'0\'')))) ),
inference(resolution,[status(thm)],[d32,c147]) ).
cnf(d34,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d33,d31]) ).
cnf(d35,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d30,c138]) ).
cnf(d36,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| '\'LE\''(f(X0),s(s(s('\'0\'')))) ),
inference(resolution,[status(thm)],[d32,c189]) ).
cnf(d37,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d36,d31]) ).
cnf(d38,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d37,d35]) ).
cnf(d39,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| iLEQ(suc(X0),suc(X0))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[d38,d34]) ).
cnf(d40,plain,
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(X1))
| '\'LE\''(f(X0),s(s(s('\'0\'')))) ),
inference(resolution,[status(thm)],[d32,c1159]) ).
cnf(d41,plain,
( '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0)) ),
inference(resolution,[status(thm)],[d40,d32]) ).
cnf(d42,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d41,d32]) ).
cnf(d43,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d42,d31]) ).
cnf(d44,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d43,d31]) ).
cnf(d45,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d44,d31]) ).
cnf(d46,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d45,d39]) ).
cnf(d47,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d46,d39]) ).
cnf(d48,plain,
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X2))
| ~ '\'E\''(s(s(s('\'0\''))),f(X1))
| '\'LE\''(f(X0),s(s(s('\'0\'')))) ),
inference(resolution,[status(thm)],[d32,c931]) ).
cnf(d49,plain,
( '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(X0)) ),
inference(resolution,[status(thm)],[d48,d32]) ).
cnf(d50,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d49,d32]) ).
cnf(d51,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d50,d31]) ).
cnf(d52,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(X0))) ),
inference(resolution,[status(thm)],[d51,d31]) ).
cnf(d53,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X2))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d52,d31]) ).
cnf(d54,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X1))))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d53,d35]) ).
cnf(d55,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s(s('\'0\''))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d54,d35]) ).
cnf(d56,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d55,d35]) ).
cnf(d57,plain,
( '\'LE\''(f(X2),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d56,d47]) ).
cnf(d58,plain,
( '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d57,d47]) ).
cnf(d59,plain,
( '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X2),s(s(s('\'0\''))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d58,d47]) ).
cnf(d60,plain,
( '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| '\'LE\''(f(X1),s(s(s('\'0\''))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d59,d39]) ).
cnf(d61,plain,
( '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\''))))
| '\'LE\''(f(X0),s(s(s('\'0\'')))) ),
inference(resolution,[status(thm)],[d60,d39]) ).
cnf(d62,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d61,c134]) ).
cnf(d63,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s(s('\'0\'')),f(X0)) ),
inference(resolution,[status(thm)],[d61,c501]) ).
cnf(d64,plain,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| '\'LE\''(f(X0),s(s('\'0\''))) ),
inference(resolution,[status(thm)],[d63,c942]) ).
cnf(d65,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d64,d62]) ).
cnf(d66,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d61,c913]) ).
cnf(d67,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| '\'LE\''(f(X0),s(s('\'0\''))) ),
inference(resolution,[status(thm)],[d63,c278]) ).
cnf(d68,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d67,d62]) ).
cnf(d69,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d68,d66]) ).
cnf(d70,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| iLEQ(suc(X0),suc(X0))
| '\'LE\''(f(X0),s(s('\'0\'')))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[d69,d65]) ).
cnf(d71,plain,
( ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(X2))
| ~ '\'E\''(s(s('\'0\'')),f(X1))
| '\'LE\''(f(X0),s(s('\'0\''))) ),
inference(resolution,[status(thm)],[d63,c586]) ).
cnf(d72,plain,
( '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(X0)) ),
inference(resolution,[status(thm)],[d71,d63]) ).
cnf(d73,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d72,d63]) ).
cnf(d74,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X0))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d73,d62]) ).
cnf(d75,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d74,d62]) ).
cnf(d76,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d75,d62]) ).
cnf(d77,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d76,d70]) ).
cnf(d78,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d77,d70]) ).
cnf(d79,plain,
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(X2))
| ~ '\'E\''(s(s('\'0\'')),f(X1))
| '\'LE\''(f(X0),s(s('\'0\''))) ),
inference(resolution,[status(thm)],[d63,c981]) ).
cnf(d80,plain,
( '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(X0)) ),
inference(resolution,[status(thm)],[d79,d63]) ).
cnf(d81,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d80,d63]) ).
cnf(d82,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d81,d62]) ).
cnf(d83,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(X0))) ),
inference(resolution,[status(thm)],[d82,d62]) ).
cnf(d84,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X2))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d83,d62]) ).
cnf(d85,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X1))))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d84,d66]) ).
cnf(d86,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s(s('\'0\'')),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d85,d66]) ).
cnf(d87,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d86,d66]) ).
cnf(d88,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d87,d78]) ).
cnf(d89,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d88,d78]) ).
cnf(d90,plain,
( '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X2),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d89,d78]) ).
cnf(d91,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X1),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d90,d70]) ).
cnf(d92,plain,
( '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\'')))
| '\'LE\''(f(X0),s(s('\'0\''))) ),
inference(resolution,[status(thm)],[d91,d70]) ).
cnf(d93,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d92,c691]) ).
cnf(d94,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(s('\'0\''),f(X0)) ),
inference(resolution,[status(thm)],[d92,c152]) ).
cnf(d95,plain,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| '\'LE\''(f(X0),s('\'0\'')) ),
inference(resolution,[status(thm)],[d94,c851]) ).
cnf(d96,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d95,d93]) ).
cnf(d97,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(s('\'0\''),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d92,c534]) ).
cnf(d98,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| '\'LE\''(f(X0),s('\'0\'')) ),
inference(resolution,[status(thm)],[d94,c359]) ).
cnf(d99,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d98,d93]) ).
cnf(d100,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d99,d97]) ).
cnf(d101,plain,
( '\'LE\''(f(X0),s('\'0\''))
| iLEQ(suc(X0),suc(X0))
| '\'LE\''(f(X0),s('\'0\''))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[d100,d96]) ).
cnf(d102,plain,
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(X2))
| ~ '\'E\''(s('\'0\''),f(X1))
| '\'LE\''(f(X0),s('\'0\'')) ),
inference(resolution,[status(thm)],[d94,c755]) ).
cnf(d103,plain,
( '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(X0)) ),
inference(resolution,[status(thm)],[d102,d94]) ).
cnf(d104,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d103,d94]) ).
cnf(d105,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d104,d93]) ).
cnf(d106,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d105,d93]) ).
cnf(d107,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d106,d93]) ).
cnf(d108,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d107,d101]) ).
cnf(d109,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d108,d101]) ).
cnf(d110,plain,
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(X2))
| ~ '\'E\''(s('\'0\''),f(X1))
| '\'LE\''(f(X0),s('\'0\'')) ),
inference(resolution,[status(thm)],[d94,c383]) ).
cnf(d111,plain,
( '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(X0)) ),
inference(resolution,[status(thm)],[d110,d94]) ).
cnf(d112,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d111,d94]) ).
cnf(d113,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d112,d93]) ).
cnf(d114,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(X0))) ),
inference(resolution,[status(thm)],[d113,d93]) ).
cnf(d115,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X2))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d114,d93]) ).
cnf(d116,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X1))))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d115,d97]) ).
cnf(d117,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(s('\'0\''),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d116,d97]) ).
cnf(d118,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d117,d97]) ).
cnf(d119,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d118,d109]) ).
cnf(d120,plain,
( '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d119,d109]) ).
cnf(d121,plain,
( '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X2),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d120,d109]) ).
cnf(d122,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X1),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d121,d101]) ).
cnf(d123,plain,
( '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\''))
| '\'LE\''(f(X0),s('\'0\'')) ),
inference(resolution,[status(thm)],[d122,d101]) ).
cnf(d124,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d123,c1074]) ).
cnf(d125,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'E\''('\'0\'',f(X0)) ),
inference(resolution,[status(thm)],[d123,c225]) ).
cnf(d126,plain,
( iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| '\'LE\''(f(X0),'\'0\'') ),
inference(resolution,[status(thm)],[d125,c580]) ).
cnf(d127,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| iLEQ(suc(X0),suc(X0))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d126,d124]) ).
cnf(d128,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'E\''('\'0\'',f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d123,c659]) ).
cnf(d129,plain,
( iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| '\'LE\''(f(X0),'\'0\'') ),
inference(resolution,[status(thm)],[d125,c719]) ).
cnf(d130,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d129,d124]) ).
cnf(d131,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| iLEQ(suc(X0),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d130,d128]) ).
cnf(d132,plain,
( '\'LE\''(f(X0),'\'0\'')
| iLEQ(suc(X0),suc(X0))
| '\'LE\''(f(X0),'\'0\'')
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[d131,d127]) ).
cnf(d133,plain,
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(X2))
| ~ '\'E\''('\'0\'',f(X1))
| '\'LE\''(f(X0),'\'0\'') ),
inference(resolution,[status(thm)],[d125,c1029]) ).
cnf(d134,plain,
( '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(X0)) ),
inference(resolution,[status(thm)],[d133,d125]) ).
cnf(d135,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d134,d125]) ).
cnf(d136,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d135,d124]) ).
cnf(d137,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d136,d124]) ).
cnf(d138,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| '\'E\''(f(X2),f(suc(X2)))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d137,d124]) ).
cnf(d139,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X1),suc(X0))
| '\'E\''(f(X1),f(suc(X1)))
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d138,d132]) ).
cnf(d140,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'E\''(f(X0),f(suc(X0)))
| '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d139,d132]) ).
cnf(d141,plain,
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(X2))
| ~ '\'E\''('\'0\'',f(X1))
| '\'LE\''(f(X0),'\'0\'') ),
inference(resolution,[status(thm)],[d125,c124]) ).
cnf(d142,plain,
( '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(X0)) ),
inference(resolution,[status(thm)],[d141,d125]) ).
cnf(d143,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d142,d125]) ).
cnf(d144,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d143,d124]) ).
cnf(d145,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0))))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(X0))) ),
inference(resolution,[status(thm)],[d144,d124]) ).
cnf(d146,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''('\'0\'',f(suc(suc(X2))))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d145,d124]) ).
cnf(d147,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''('\'0\'',f(suc(suc(X1))))
| ~ '\'E\''('\'0\'',f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d146,d128]) ).
cnf(d148,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ '\'E\''(f(X0),f(suc(X0)))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''('\'0\'',f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[d147,d128]) ).
cnf(d149,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X2),f(suc(X2)))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d148,d128]) ).
cnf(d150,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ '\'E\''(f(X1),f(suc(X1)))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d149,d140]) ).
cnf(d151,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ '\'E\''(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[d150,d140]) ).
cnf(d152,plain,
( '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X2),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d151,d140]) ).
cnf(d153,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X1),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[status(thm)],[d152,d132]) ).
cnf(d154,plain,
( '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'')
| '\'LE\''(f(X0),'\'0\'') ),
inference(resolution,[status(thm)],[d153,d132]) ).
cnf(d155,plain,
$false,
inference(resolution,[status(thm)],[d154,c365]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n004.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sat Sep 26 19:45:36 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 241.12/35.47 % SZS status Unsatisfiable for theBenchmark.p
% 241.12/35.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------