%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO653-1 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.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 : Fri Jul 25 09:59:08 PM UTC 2025
% Result : Unsatisfiable 94.82s 12.25s
% Output : CNFRefutation 94.82s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_2036)
% Comments :
%------------------------------------------------------------------------------
cnf(29,plain,
'LE'(f(X0),s('0')),
inference(cnf,[status(esa)],[clause_2036]) ).
cnf(l0,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(49,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_1983]) ).
cnf(l1,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[49]) ).
cnf(67,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| 'E'(f(X0),f(suc(suc(X0))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3)))) ),
inference(cnf,[status(esa)],[clause_1384]) ).
cnf(l2,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[67]) ).
cnf(20,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_1057]) ).
cnf(l18,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(74,plain,
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_38]) ).
cnf(l4,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(55,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X3),f(suc(suc(X3)))) ),
inference(cnf,[status(esa)],[clause_1836]) ).
cnf(l161,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(53,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_148]) ).
cnf(l204,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(19,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(cnf,[status(esa)],[clause_1719]) ).
cnf(l43,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l38,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l39,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(58,plain,
( ~ 'LE'(f(suc(suc(suc(X0)))),s('0'))
| 'E'('0',f(suc(suc(suc(X0)))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_1528]) ).
cnf(l162,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l315,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(83,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0))) ),
inference(cnf,[status(esa)],[clause_354]) ).
cnf(l165,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(79,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_972]) ).
cnf(l2103,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l7,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l333,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l332,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l176,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l21,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l854,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(7,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
inference(cnf,[status(esa)],[clause_102]) ).
cnf(l171,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l654,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l482,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l167,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l146,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l19,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l657,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l334,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l3,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l32,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l316,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2229,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l317,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l287,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l585,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l690,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l740,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l527,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l837,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l192,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l831,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l627,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1214,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l816,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l71,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l94,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l26,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l220,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l421,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5186,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1002,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2144,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10953,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1518,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l30,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11199,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l128,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l13,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1178,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l177,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l2420,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l884,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l307,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l832,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l102,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l344,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l717,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1010,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l5606,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l653,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l321,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l318,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1304,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l298,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l53,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l184,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l688,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5005,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l99,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l362,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l620,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2586,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l709,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5819,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2097,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5836,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l761,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l938,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l419,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l901,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l320,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11196,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l640,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l765,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l156,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l299,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l842,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l231,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3063,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l501,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6537,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10762,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1084,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5198,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l645,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1973,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l206,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l327,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l468,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l14,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l29,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l2027,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l132,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l218,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1045,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l614,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6037,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l15,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l10985,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1666,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l247,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l232,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l11129,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11069,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l312,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l609,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l133,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l181,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l828,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l768,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l1757,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l587,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l712,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2414,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l660,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l188,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l5034,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l336,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l115,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5409,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l264,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2215,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l905,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l630,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l1089,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l483,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l474,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l954,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l716,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l154,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l564,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l200,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l924,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1150,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l918,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11078,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l856,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2661,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l563,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l635,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3986,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6079,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l253,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2075,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l159,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l11427,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1817,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6502,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2657,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1709,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6953,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l859,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11416,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2129,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6487,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11247,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l876,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l283,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l11270,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l908,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6169,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l523,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11535,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l453,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l208,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11135,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l580,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11316,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1722,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l4812,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l427,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l130,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l286,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11548,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l126,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3076,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l532,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l916,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l577,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l230,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l34,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2071,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l4956,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1183,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11208,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2410,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l731,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1135,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5838,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5813,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5964,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11554,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l708,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l723,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l994,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l540,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l806,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1145,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6167,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l135,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l718,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l692,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l324,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2013,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5377,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5824,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l922,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l2131,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l536,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l191,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l857,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l139,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l813,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l311,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l942,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11262,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l795,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l794,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6733,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6884,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10758,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6382,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6609,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6371,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l579,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11212,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l16,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l515,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l888,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2662,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l881,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l743,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2396,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l466,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l59,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l345,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l911,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6895,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1946,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l294,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l548,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1714,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l11489,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4796,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l491,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2011,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l570,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6348,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4986,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l113,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l576,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1725,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6134,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1756,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l121,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l54,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1517,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2197,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6434,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11691,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11214,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l129,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1452,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l1009,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l260,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11607,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l52,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l186,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l791,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11521,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2030,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1394,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1659,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6630,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11510,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2680,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l533,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l545,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2930,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l535,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1679,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1187,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l246,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6503,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l524,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10036,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11159,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l465,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11359,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5598,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l151,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l10443,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1780,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6100,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l116,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11493,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l235,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l5384,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11507,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l574,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l150,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1167,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1420,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l588,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6555,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l496,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2147,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11256,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11614,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5714,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11086,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l214,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l3015,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5007,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11739,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l506,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l592,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5687,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l841,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1779,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l179,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l469,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1033,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l243,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3972,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l928,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l136,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5965,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l897,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l1819,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l144,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6485,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7025,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1697,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l575,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6846,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11213,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1227,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6263,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6184,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11426,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l300,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6534,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l830,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11522,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2443,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l122,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l6275,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l7807,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5115,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l123,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11904,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2784,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11725,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11242,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l140,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11425,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1851,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l6463,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11518,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2138,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1463,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1857,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l5356,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l373,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l694,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l219,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6383,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11930,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6501,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5818,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6532,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l485,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l591,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3062,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11490,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3011,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1715,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1462,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5010,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11164,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2392,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11197,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2216,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l632,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4985,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l450,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6675,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11544,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6390,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3122,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11237,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11936,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l261,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10717,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11492,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1126,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11672,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6514,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l812,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l193,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l2462,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l7776,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11476,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11236,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l659,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l10955,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1375,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2032,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1944,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l520,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l6659,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6788,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l73,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l5608,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6359,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2149,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11961,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11733,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l517,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6500,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6322,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l676,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6516,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l586,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11085,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l211,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l920,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6530,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6343,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1059,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11257,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l4996,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l40,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11827,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2755,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l899,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11927,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6676,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l519,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l939,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11962,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11860,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2024,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6877,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l36,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11795,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1085,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5776,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6196,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1383,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11562,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11749,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l639,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l296,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l263,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6702,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11488,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11791,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6417,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1663,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1379,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6590,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l442,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11966,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6971,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4995,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l10963,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6386,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3078,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5098,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11911,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6442,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2587,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11211,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2151,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6456,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6588,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11486,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11563,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1159,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11893,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1469,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1958,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l11969,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11523,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11226,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5380,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11605,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11153,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2807,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l11154,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5466,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11970,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6421,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11792,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5467,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6701,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5358,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11336,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3116,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l661,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11971,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5537,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1263,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11874,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7028,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6319,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l537,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l350,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11958,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2019,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11822,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l998,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11878,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6269,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l262,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2361,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6969,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11814,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6432,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6977,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l860,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1669,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6089,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10624,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11533,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5607,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l929,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6871,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6294,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11973,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11963,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1265,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5008,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6040,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11992,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11875,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11993,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11130,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l138,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l131,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11990,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l495,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l124,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l5004,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11289,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l931,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6791,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10982,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l464,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l5507,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6168,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1419,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11957,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5014,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5294,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12061,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11541,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2277,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6338,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l874,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l1122,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l5867,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6949,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l6321,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6301,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1447,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1770,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l493,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l6950,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2532,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l665,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l11411,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6047,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11747,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1093,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6186,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11938,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10994,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11916,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12118,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6576,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1769,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l6397,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11221,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11854,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2407,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11974,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5281,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1422,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l981,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5784,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l558,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11929,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l127,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l7018,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l578,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11852,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2606,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6830,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1421,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1203,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6862,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11964,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11301,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l521,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11959,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11926,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6974,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6476,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5509,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l12208,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11540,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11914,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6277,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12038,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11249,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1417,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2455,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2139,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6464,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6131,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5656,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5511,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12130,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1261,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1440,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6536,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5811,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l6475,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11991,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12049,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11987,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11570,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6898,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5787,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11545,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3106,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l6279,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5510,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l12240,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11349,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11367,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11529,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6183,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11506,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11994,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12262,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12048,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6202,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12045,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6900,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5810,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6381,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8384,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5717,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1429,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l10942,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11566,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11565,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12135,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1859,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[83]) ).
cnf(l12253,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5727,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2817,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6958,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12299,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5756,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1425,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l12355,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11482,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l494,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l155,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l12379,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1455,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l5025,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l12035,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11918,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12337,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11215,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11910,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12577,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5783,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6931,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12583,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12537,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12571,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6280,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11285,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12116,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12566,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11925,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1418,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l11784,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11778,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12293,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11312,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12096,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12454,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12468,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12272,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12584,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12585,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2458,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12580,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12281,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11960,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l10724,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12586,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10728,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12092,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12120,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12347,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1435,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6135,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12578,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12587,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12444,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11538,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12089,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12553,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11234,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12600,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12593,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12410,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12570,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12601,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12588,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11526,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11417,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12591,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12291,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12395,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12117,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l10947,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l1431,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12279,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12602,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11768,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12592,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12094,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12115,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12581,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l641,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12317,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12197,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11281,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12575,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12042,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12579,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12497,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12608,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11794,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12604,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12327,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11815,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10636,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l12605,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12582,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12228,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12561,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12589,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12619,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12051,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12155,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12498,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6086,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[74]) ).
cnf(l12606,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12056,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12607,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12052,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12599,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12590,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l45,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l70,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12603,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12609,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10506,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l10564,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l11965,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10312,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12757,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12707,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l90,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12790,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12700,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l10315,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12876,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5026,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l12783,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12144,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12620,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12885,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12152,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12886,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12887,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12888,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12889,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12413,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l12748,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12847,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[29]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l18,l4,l161,l204,l43,l9,l38,l39,l162,l315,l165,l2103,l7,l333,l332,l176,l21,l854,l171,l654,l482,l167,l146,l19,l657,l334,l3,l32,l316,l2229,l317,l287,l585,l690,l740,l527,l837,l192,l831,l627,l1214,l816,l71,l94,l26,l220,l421,l5186,l1002,l2144,l10953,l1518,l30,l11199,l128,l13,l1178,l177,l2420,l884,l307,l832,l102,l344,l717,l1010,l5606,l653,l321,l318,l1304,l298,l53,l184,l688,l5005,l99,l362,l620,l2586,l709,l5819,l2097,l5836,l761,l938,l419,l901,l320,l11196,l640,l765,l156,l299,l842,l231,l3063,l501,l6537,l10762,l1084,l5198,l645,l1973,l206,l327,l468,l14,l29,l2027,l132,l218,l1045,l614,l6037,l15,l10985,l1666,l247,l232,l11129,l11069,l312,l609,l133,l181,l828,l768,l1757,l587,l712,l2414,l660,l188,l5034,l336,l115,l5409,l264,l2215,l905,l630,l1089,l483,l474,l954,l716,l154,l564,l200,l924,l1150,l918,l11078,l856,l2661,l563,l635,l3986,l6079,l253,l2075,l159,l11427,l1817,l6502,l2657,l1709,l6953,l859,l11416,l2129,l6487,l11247,l876,l283,l11270,l908,l6169,l523,l11535,l453,l208,l11135,l580,l11316,l1722,l4812,l427,l130,l286,l11548,l126,l3076,l532,l916,l577,l230,l34,l2071,l8,l4956,l1183,l11208,l2410,l731,l1135,l5838,l5813,l5964,l11554,l708,l723,l994,l540,l806,l1145,l6167,l135,l718,l692,l324,l2013,l5377,l5824,l922,l2131,l536,l191,l857,l139,l813,l311,l942,l11262,l795,l794,l6733,l6884,l10758,l6382,l6609,l6371,l579,l11212,l16,l515,l888,l2662,l881,l743,l2396,l466,l59,l345,l911,l6895,l1946,l294,l548,l1714,l11489,l4796,l491,l2011,l570,l6348,l4986,l113,l576,l1725,l6134,l1756,l121,l54,l1517,l2197,l6434,l11691,l11214,l129,l1452,l1009,l260,l11607,l52,l186,l791,l11521,l2030,l1394,l1659,l6630,l11510,l2680,l533,l545,l2930,l535,l1679,l1187,l246,l6503,l524,l10036,l11159,l465,l11359,l5598,l151,l10443,l1780,l6100,l116,l11493,l235,l5384,l11507,l574,l150,l1167,l1420,l588,l6555,l496,l2147,l11256,l11614,l5714,l11086,l214,l3015,l5007,l11739,l506,l592,l5687,l841,l1779,l179,l469,l1033,l243,l3972,l928,l136,l5965,l897,l1819,l144,l6485,l7025,l1697,l575,l6846,l11213,l1227,l6263,l6184,l11426,l300,l6534,l830,l11522,l2443,l122,l6275,l7807,l5115,l123,l11904,l2784,l11725,l11242,l140,l11425,l1851,l6463,l11518,l2138,l1463,l1857,l5356,l373,l694,l219,l6383,l11930,l6501,l5818,l6532,l485,l591,l3062,l11490,l3011,l1715,l1462,l5010,l11164,l2392,l11197,l2216,l632,l4985,l450,l6675,l11544,l6390,l3122,l11237,l11936,l261,l10717,l11492,l1126,l11672,l6514,l812,l193,l2462,l7776,l11476,l11236,l659,l10955,l1375,l2032,l1944,l520,l6659,l6788,l73,l5608,l6359,l2149,l11961,l11733,l517,l6500,l6322,l676,l6516,l586,l11085,l211,l920,l6530,l6343,l1059,l11257,l4996,l40,l11827,l2755,l899,l11927,l6676,l519,l939,l11962,l11860,l2024,l6877,l36,l11795,l1085,l5776,l6196,l1383,l11562,l11749,l639,l296,l263,l6702,l11488,l11791,l6417,l1663,l1379,l6590,l442,l11966,l6971,l4995,l10963,l6386,l3078,l5098,l11911,l6442,l2587,l11211,l2151,l6456,l6588,l11486,l11563,l1159,l11893,l1469,l1958,l11969,l11523,l11226,l5380,l11605,l11153,l2807,l11154,l5466,l11970,l6421,l11792,l5467,l6701,l5358,l11336,l3116,l661,l11971,l5537,l1263,l11874,l7028,l6319,l537,l350,l11958,l2019,l11822,l998,l11878,l6269,l262,l2361,l6969,l11814,l6432,l6977,l860,l1669,l6089,l10624,l11533,l5607,l929,l6871,l6294,l11973,l11963,l1265,l5008,l6040,l11992,l11875,l11993,l11130,l138,l131,l11990,l495,l124,l5004,l11289,l931,l6791,l10982,l464,l5507,l6168,l1419,l11957,l5014,l5294,l12061,l11541,l2277,l6338,l874,l1122,l5867,l6949,l6321,l6301,l1447,l1770,l493,l6950,l2532,l665,l11411,l6047,l11747,l1093,l6186,l11938,l10994,l11916,l12118,l6576,l1769,l6397,l11221,l11854,l2407,l11974,l5281,l1422,l981,l5784,l558,l11929,l127,l7018,l578,l11852,l2606,l6830,l1421,l1203,l6862,l11964,l11301,l521,l11959,l11926,l6974,l6476,l5509,l12208,l11540,l11914,l6277,l12038,l11249,l1417,l2455,l2139,l6464,l6131,l5656,l5511,l12130,l1261,l1440,l6536,l5811,l6475,l11991,l12049,l11987,l11570,l6898,l5787,l11545,l3106,l6279,l5510,l12240,l11349,l11367,l11529,l6183,l11506,l11994,l12262,l12048,l6202,l12045,l6900,l5810,l6381,l8384,l5717,l1429,l10942,l11566,l11565,l12135,l1859,l12253,l5727,l2817,l6958,l12299,l5756,l1425,l12355,l11482,l494,l155,l12379,l1455,l5025,l12035,l11918,l12337,l11215,l11910,l12577,l5783,l6931,l12583,l12537,l12571,l6280,l11285,l12116,l12566,l11925,l1418,l11784,l11778,l12293,l11312,l12096,l12454,l12468,l12272,l12584,l12585,l2458,l12580,l12281,l11960,l10724,l12586,l10728,l12092,l12120,l12347,l1435,l6135,l12578,l12587,l12444,l11538,l12089,l12553,l11234,l12600,l12593,l12410,l12570,l12601,l12588,l11526,l11417,l12591,l12291,l12395,l12117,l10947,l1431,l12279,l12602,l11768,l12592,l12094,l12115,l12581,l641,l12317,l12197,l11281,l12575,l12042,l12579,l12497,l12608,l11794,l12604,l12327,l11815,l10636,l12605,l12582,l12228,l12561,l12589,l12619,l12051,l12155,l12498,l6086,l12606,l12056,l12607,l12052,l12599,l12590,l45,l70,l12603,l12609,l10506,l10564,l11965,l10312,l12757,l12707,l90,l12790,l12700,l10315,l12876,l5026,l12783,l12144,l12620,l12885,l12152,l12886,l12887,l12888,l12889,l12413,l12748,l12847]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO653-1 : TPTP v9.0.0. Released v7.3.0.
% 0.03/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.34 % Computer : n023.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Jul 22 20:07:49 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.38 % launching worker at depth: 1
% 0.14/0.38 % launching worker at depth: 5
% 0.14/0.38 % launching worker at depth: 4
% 0.14/0.38 % launching worker at depth: 2
% 0.14/0.38 % launching worker at depth: 3
% 0.14/0.38 % launching worker at depth: 6
% 0.14/0.38 % launching worker at depth: 7
% 0.20/0.38 % launching worker at depth: 8
% 0.20/0.38 % launching worker at depth: 9
% 0.20/0.51 % launching worker at depth: 10
% 1.50/0.56 % launching worker at depth: 11
% 4.96/1.04 % launching worker at depth: 12
% 60.47/7.96 % launching worker at depth: 13
% 94.82/12.25 % SZS status Theorem for theBenchmark
% 94.82/12.25 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------