%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO655-1 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:09 PM UTC 2025
% Result : Unsatisfiable 3.56s 0.84s
% Output : CNFRefutation 3.56s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_497)
% Comments :
%------------------------------------------------------------------------------
cnf(34,plain,
'LE'(f(X0),s('0')),
inference(cnf,[status(esa)],[clause_497]) ).
cnf(l0,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(36,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_513]) ).
cnf(l1,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[36]) ).
cnf(10,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_269]) ).
cnf(l17,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(14,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X4)))
| ~ '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(X4))))
| ~ '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(X4),f(suc(X4)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X4))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X0)) ),
inference(cnf,[status(esa)],[clause_125]) ).
cnf(l2,plain,
( ~ 'E'('0',f(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(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(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(8,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_5]) ).
cnf(l3,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(22,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_84]) ).
cnf(l143,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l81,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(33,plain,
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_72]) ).
cnf(l16,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l70,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l7,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l159,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l216,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l96,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l47,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l174,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l144,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l181,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l20,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(21,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)) ),
inference(cnf,[status(esa)],[clause_379]) ).
cnf(l24,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)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l213,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l4,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l46,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l276,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l67,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l11,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l48,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l5,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l201,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l72,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l28,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l177,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l179,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l14,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)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l233,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(15,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X3),suc(X1))
| '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(X4),f(suc(X4))) ),
inference(cnf,[status(esa)],[clause_209]) ).
cnf(l56,plain,
( ~ 'E'('0',f(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),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(z))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l104,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l309,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l89,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l63,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l116,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l196,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l124,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l308,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l176,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l249,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l214,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l252,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l65,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l113,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l215,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l218,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l43,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l105,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l220,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l228,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l6,plain,
( ~ 'E'('0',f(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),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(z))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l139,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l459,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l232,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l571,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l150,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l285,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l170,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l22,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l119,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)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l84,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l325,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l167,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l661,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l9,plain,
( ~ 'E'('0',f(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),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(z))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l771,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l36,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l178,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l288,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l162,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l444,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l735,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l455,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l155,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l85,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l616,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l82,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l955,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l460,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l101,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l227,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l172,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l209,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l148,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l954,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l54,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l625,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l991,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l32,plain,
( ~ 'E'('0',f(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),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(z))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l40,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l98,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l572,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l509,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l448,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l579,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l545,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l495,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l133,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l118,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l573,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l90,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l278,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l631,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l792,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l759,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l874,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l279,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l94,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l134,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l195,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l430,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l59,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l312,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l511,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l236,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l343,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l280,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l114,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l671,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l564,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1017,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l723,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1021,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l705,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l624,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l136,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l783,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l451,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1028,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l994,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1018,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l987,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1096,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l142,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l147,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l264,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1098,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l452,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l18,plain,
( ~ 'E'('0',f(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),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(z))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l357,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l193,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l262,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l241,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l997,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l977,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l656,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1115,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l659,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l493,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l477,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l229,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l501,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1103,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l980,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l235,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l76,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l77,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1022,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l274,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1072,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l151,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l250,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1023,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1118,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l21,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1116,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l281,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l863,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1025,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l736,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l366,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l346,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l983,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l100,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1154,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l347,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l122,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l129,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l773,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l902,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l192,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l183,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l985,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l237,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l360,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1088,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l257,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l230,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l858,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1119,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1024,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1120,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l383,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l570,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1124,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l551,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l394,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1122,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l619,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l153,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l413,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l843,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l494,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1153,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l431,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l154,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)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1125,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1156,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1123,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1026,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1144,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1166,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1164,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l351,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l361,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1155,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1027,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1170,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l462,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l464,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l644,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1167,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l184,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1190,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l391,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l349,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1191,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l490,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1132,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(l244,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l247,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1015,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[34]) ).
cnf(l856,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[10]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l17,l2,l3,l143,l81,l16,l70,l7,l159,l216,l96,l47,l174,l144,l181,l20,l24,l213,l4,l46,l276,l67,l11,l48,l5,l201,l72,l28,l177,l179,l14,l233,l56,l104,l309,l89,l63,l116,l196,l124,l308,l176,l249,l214,l252,l65,l113,l215,l218,l43,l105,l220,l228,l6,l139,l459,l232,l571,l150,l285,l170,l22,l119,l84,l325,l167,l661,l9,l771,l36,l178,l288,l162,l444,l735,l455,l155,l85,l616,l82,l955,l460,l101,l227,l172,l209,l148,l954,l54,l625,l991,l32,l40,l98,l572,l509,l448,l579,l545,l495,l133,l118,l573,l90,l278,l631,l792,l759,l874,l279,l94,l134,l195,l430,l59,l312,l511,l236,l343,l280,l114,l671,l564,l1017,l723,l1021,l705,l624,l136,l783,l451,l1028,l994,l1018,l987,l1096,l142,l147,l264,l1098,l452,l18,l357,l193,l262,l241,l997,l977,l656,l1115,l659,l493,l477,l229,l501,l1103,l980,l235,l76,l77,l1022,l274,l1072,l151,l250,l1023,l1118,l21,l1116,l281,l863,l1025,l736,l366,l346,l983,l100,l1154,l347,l122,l129,l773,l902,l192,l183,l985,l237,l360,l1088,l257,l230,l858,l1119,l1024,l1120,l383,l570,l1124,l551,l394,l1122,l619,l153,l413,l843,l494,l1153,l431,l154,l1125,l1156,l1123,l1026,l1144,l1166,l1164,l351,l361,l1155,l1027,l1170,l462,l464,l644,l1167,l184,l1190,l391,l349,l1191,l490,l1132,l244,l247,l1015,l856]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO655-1 : TPTP v9.0.0. Released v7.3.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n020.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Jul 22 20:07:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.35 % launching worker at depth: 1
% 0.13/0.35 % launching worker at depth: 4
% 0.13/0.35 % launching worker at depth: 2
% 0.13/0.35 % launching worker at depth: 5
% 0.13/0.35 % launching worker at depth: 3
% 0.13/0.35 % launching worker at depth: 6
% 0.13/0.35 % launching worker at depth: 7
% 0.13/0.35 % launching worker at depth: 8
% 0.13/0.35 % launching worker at depth: 9
% 0.13/0.39 % launching worker at depth: 10
% 0.19/0.42 % launching worker at depth: 11
% 2.28/0.66 % launching worker at depth: 12
% 3.56/0.84 % SZS status Theorem for theBenchmark
% 3.56/0.84 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------