%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO650-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 : n028.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 17.37s 2.61s
% Output : CNFRefutation 17.37s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_406)
% Comments :
%------------------------------------------------------------------------------
cnf(9,plain,
'LE'(f(X0),s('0')),
inference(cnf,[status(esa)],[clause_406]) ).
cnf(l0,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(18,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_313]) ).
cnf(l1,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[18]) ).
cnf(27,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_206]) ).
cnf(l5,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(14,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X0),f(suc(suc(X0))))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2)))) ),
inference(cnf,[status(esa)],[clause_309]) ).
cnf(l2,plain,
( ~ '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(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)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),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)],[14]) ).
cnf(6,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_278]) ).
cnf(l6,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l53,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l58,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(25,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(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_345]) ).
cnf(l30,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(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)],[25]) ).
cnf(l11,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l19,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(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)],[25]) ).
cnf(l16,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(10,plain,
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_359]) ).
cnf(l14,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l557,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l15,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l126,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l54,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l616,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(13,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_189]) ).
cnf(l124,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)],[13]) ).
cnf(l760,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l449,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(21,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_376]) ).
cnf(l653,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l144,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l832,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l47,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l41,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l664,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l489,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l654,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l690,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l657,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l748,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l498,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(23,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ '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))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(cnf,[status(esa)],[clause_135]) ).
cnf(l9,plain,
( ~ '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(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'(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))))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l120,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l391,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l656,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l26,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l59,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l62,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l56,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l50,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l154,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l493,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l129,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l665,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l33,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l149,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)],[13]) ).
cnf(l150,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l125,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l152,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1207,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1100,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l590,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1114,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1063,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(20,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
inference(cnf,[status(esa)],[clause_333]) ).
cnf(l3,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1102,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l135,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l42,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l46,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l86,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1132,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(33,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_64]) ).
cnf(l138,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)],[33]) ).
cnf(l1214,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1389,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l198,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1230,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l70,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l4,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)],[33]) ).
cnf(l107,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)],[33]) ).
cnf(l74,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l73,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l758,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l39,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l108,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l24,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l167,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)],[33]) ).
cnf(l1135,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l48,plain,
( ~ '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(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'(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))))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l413,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l518,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)],[13]) ).
cnf(l501,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l66,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l414,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1374,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l110,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1319,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1574,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1024,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l460,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l581,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1805,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l435,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1799,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l429,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1162,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l208,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1101,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1050,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1820,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l607,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1779,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l772,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l703,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l52,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)],[33]) ).
cnf(l25,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1231,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1161,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l638,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l721,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l743,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)],[33]) ).
cnf(l1806,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1500,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1848,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l29,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l674,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l768,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l84,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l192,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)],[33]) ).
cnf(l1049,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1821,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l529,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l38,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1332,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1045,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1170,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l164,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1499,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1266,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1845,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1336,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l461,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1323,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)],[13]) ).
cnf(l1961,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1689,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1997,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l600,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1187,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1415,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)],[33]) ).
cnf(l1911,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1322,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1940,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1390,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2029,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l580,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l647,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)],[33]) ).
cnf(l1632,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l431,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l618,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l432,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1209,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l422,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)],[33]) ).
cnf(l1186,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l430,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1015,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l584,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l448,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2020,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l826,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1375,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1131,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l7,plain,
( ~ '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(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'(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))))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2124,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)],[13]) ).
cnf(l1044,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1495,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l972,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l548,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l693,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1381,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2137,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1982,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1192,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2024,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l45,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1953,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1996,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1939,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l27,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2127,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l67,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1823,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2030,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1850,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2132,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1331,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l44,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1048,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l40,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l35,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l503,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1977,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1278,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1976,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l10,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l543,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l517,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2082,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l17,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l490,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)],[33]) ).
cnf(l2209,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l524,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1204,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)],[33]) ).
cnf(l2031,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l808,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1405,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2057,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l628,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1962,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1168,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l467,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2015,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2201,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2195,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2301,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2400,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
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)],[33]) ).
cnf(l1123,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)],[33]) ).
cnf(l1019,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1481,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1917,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2504,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2500,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1167,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1808,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1794,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1448,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1184,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)],[33]) ).
cnf(l1960,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)],[33]) ).
cnf(l2215,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l780,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1969,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2206,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1650,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1450,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2401,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1127,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1986,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l492,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2325,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)],[33]) ).
cnf(l2510,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2126,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2573,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1171,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l975,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1175,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1837,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1789,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2306,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2190,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l130,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2104,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1346,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1351,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)],[33]) ).
cnf(l1868,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1488,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2070,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2449,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l500,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2004,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2603,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2025,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2526,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2084,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2502,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1999,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)],[33]) ).
cnf(l1610,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l477,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2381,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2033,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2017,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2077,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1995,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1629,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1264,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1201,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2512,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2314,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1884,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2217,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1446,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l451,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)],[33]) ).
cnf(l792,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2276,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2519,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2289,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2354,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2371,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l545,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2387,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2189,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)],[33]) ).
cnf(l2151,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l700,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l488,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2380,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1377,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2382,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1807,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)],[33]) ).
cnf(l31,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2457,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2797,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1353,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l531,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2199,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2636,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1117,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)],[33]) ).
cnf(l731,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l496,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2541,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2379,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l669,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)],[33]) ).
cnf(l1983,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2119,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l487,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1344,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)],[33]) ).
cnf(l2383,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l756,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l801,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2518,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1645,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1964,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l589,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1618,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2109,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2539,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1798,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1593,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2133,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)],[13]) ).
cnf(l2333,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1654,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2807,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2558,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1572,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2787,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2551,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2826,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2602,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2367,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2658,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l506,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l667,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1378,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)],[33]) ).
cnf(l513,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2868,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2120,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)],[33]) ).
cnf(l2698,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2416,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l491,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l577,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2927,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2536,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2192,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2912,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2876,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l21,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2866,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1043,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2113,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l701,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)],[33]) ).
cnf(l549,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2864,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l800,plain,
( ~ '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)))
| ~ 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))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2509,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2687,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2576,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2591,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1587,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2659,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2597,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2115,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)],[33]) ).
cnf(l2153,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2182,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1781,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1804,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2081,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1621,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l514,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2411,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1156,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2795,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2128,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)],[33]) ).
cnf(l2865,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2974,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2975,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2863,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2370,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1163,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2881,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2186,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2819,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2116,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2870,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2971,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1164,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2976,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2831,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2177,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)],[33]) ).
cnf(l2295,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2725,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2810,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2978,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1099,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)],[13]) ).
cnf(l847,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2542,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2855,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2818,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2977,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2980,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2972,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2034,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2913,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2979,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2973,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2983,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2805,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2987,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2134,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2883,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2882,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2511,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2981,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2877,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2878,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2873,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1743,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2986,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2984,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2299,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2985,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1584,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1657,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1108,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2032,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1583,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2997,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1963,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)],[13]) ).
cnf(l2101,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2607,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2751,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2248,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2456,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3035,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1980,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2340,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3034,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[27]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l5,l2,l6,l53,l58,l30,l11,l19,l16,l14,l557,l15,l126,l54,l616,l124,l760,l449,l653,l144,l832,l47,l41,l664,l489,l654,l690,l657,l748,l498,l9,l120,l391,l656,l26,l59,l62,l56,l50,l154,l493,l129,l665,l33,l149,l150,l125,l152,l1207,l1100,l590,l1114,l1063,l3,l1102,l135,l42,l46,l86,l1132,l138,l1214,l1389,l198,l1230,l70,l4,l107,l74,l73,l758,l39,l108,l24,l167,l1135,l48,l413,l518,l501,l66,l414,l1374,l110,l1319,l1574,l1024,l460,l581,l1805,l435,l1799,l429,l1162,l208,l1101,l1050,l1820,l607,l1779,l772,l703,l52,l25,l1231,l1161,l638,l721,l743,l1806,l1500,l1848,l29,l674,l768,l84,l192,l1049,l1821,l529,l38,l1332,l1045,l1170,l164,l1499,l1266,l1845,l1336,l461,l1323,l1961,l1689,l1997,l600,l1187,l1415,l1911,l1322,l1940,l1390,l2029,l580,l647,l1632,l431,l618,l432,l1209,l422,l1186,l430,l1015,l584,l448,l2020,l826,l1375,l1131,l7,l2124,l1044,l1495,l972,l548,l693,l1381,l2137,l1982,l1192,l2024,l45,l1953,l1996,l1939,l27,l2127,l67,l1823,l2030,l1850,l2132,l1331,l44,l1048,l40,l35,l503,l1977,l1278,l1976,l10,l543,l517,l2082,l17,l490,l2209,l524,l1204,l2031,l808,l1405,l2057,l628,l1962,l1168,l467,l2015,l2201,l2195,l2301,l2400,l193,l1123,l1019,l1481,l1917,l2504,l2500,l1167,l1808,l1794,l1448,l1184,l1960,l2215,l780,l1969,l2206,l1650,l1450,l2401,l1127,l1986,l492,l2325,l2510,l2126,l2573,l1171,l975,l1175,l1837,l1789,l2306,l2190,l130,l2104,l1346,l1351,l1868,l1488,l2070,l2449,l500,l2004,l2603,l2025,l2526,l2084,l2502,l1999,l1610,l477,l2381,l2033,l2017,l2077,l1995,l1629,l1264,l1201,l2512,l2314,l1884,l2217,l1446,l451,l792,l2276,l2519,l2289,l2354,l2371,l545,l2387,l2189,l2151,l700,l488,l2380,l1377,l2382,l1807,l31,l2457,l2797,l1353,l531,l2199,l2636,l1117,l731,l496,l2541,l2379,l669,l1983,l2119,l487,l1344,l2383,l756,l801,l2518,l1645,l1964,l589,l1618,l2109,l2539,l1798,l1593,l2133,l2333,l1654,l2807,l2558,l1572,l2787,l2551,l2826,l2602,l2367,l2658,l506,l667,l1378,l513,l2868,l2120,l2698,l2416,l491,l577,l2927,l2536,l2192,l2912,l2876,l21,l2866,l1043,l2113,l701,l549,l2864,l800,l2509,l2687,l2576,l2591,l1587,l2659,l2597,l2115,l2153,l2182,l1781,l1804,l2081,l1621,l514,l2411,l1156,l2795,l2128,l2865,l2974,l2975,l2863,l2370,l1163,l2881,l2186,l2819,l2116,l2870,l2971,l1164,l2976,l2831,l2177,l2295,l2725,l2810,l2978,l1099,l847,l2542,l2855,l2818,l2977,l2980,l2972,l2034,l2913,l2979,l2973,l2983,l2805,l2987,l2134,l2883,l2882,l2511,l2981,l2877,l2878,l2873,l1743,l2986,l2984,l2299,l2985,l1584,l1657,l1108,l2032,l1583,l2997,l1963,l2101,l2607,l2751,l2248,l2456,l3035,l1980,l2340,l3034]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYO650-1 : TPTP v9.0.0. Released v7.3.0.
% 0.06/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jul 22 20:07:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.37 % launching worker at depth: 10
% 0.12/0.38 % launching worker at depth: 11
% 2.28/0.69 % launching worker at depth: 12
% 17.37/2.61 % SZS status Theorem for theBenchmark
% 17.37/2.61 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------