%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO664-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 : n024.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 61.31s 8.07s
% Output : CNFRefutation 61.31s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_58)
% Comments :
%------------------------------------------------------------------------------
cnf(4,plain,
'LE'(f(X0),s(s('0'))),
inference(cnf,[status(esa)],[clause_58]) ).
cnf(l0,plain,
'LE'(f(suc(suc(z))),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(9,plain,
( ~ 'LE'(f(suc(X0)),s(s('0')))
| 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X0),s('0')) ),
inference(cnf,[status(esa)],[clause_83]) ).
cnf(l1,plain,
( ~ 'LE'(f(suc(suc(z))),s(s('0')))
| 'E'(s('0'),f(suc(suc(z))))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(6,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_117]) ).
cnf(l6,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(1,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_70]) ).
cnf(l31,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(3,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X4),suc(X2))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1))) ),
inference(cnf,[status(esa)],[clause_66]) ).
cnf(l36,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(8,plain,
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_50]) ).
cnf(l476,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(2,plain,
( ~ 'LE'(f(X0),s(s('0')))
| 'E'(s('0'),f(X0))
| 'LE'(f(X0),s('0')) ),
inference(cnf,[status(esa)],[clause_20]) ).
cnf(l806,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(7,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_94]) ).
cnf(l1315,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(5,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_6]) ).
cnf(l52,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(0,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X4),suc(X2))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X4))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X4)))
| ~ 'E'(s('0'),f(suc(X3))) ),
inference(cnf,[status(esa)],[clause_37]) ).
cnf(l2,plain,
( ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l26,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l62,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l63,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l75,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l193,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l495,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l221,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l501,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1283,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1430,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1386,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1252,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l496,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l7,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l85,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l475,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1259,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1431,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l482,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l620,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1279,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l832,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l786,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l505,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1439,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1310,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l499,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1444,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1291,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1264,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1334,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1285,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l484,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l487,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l488,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l477,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l497,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1440,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1325,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l498,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1262,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l478,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1441,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1434,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1263,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1458,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1277,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l509,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1465,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l506,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1442,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1471,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l480,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l481,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l474,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1448,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1492,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1280,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1451,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1435,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1311,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l527,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l25,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| iLEQ(suc(suc(z)),suc(suc(z))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l621,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l492,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1447,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l618,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1466,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1501,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1349,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l40,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l557,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1502,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l554,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1450,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l561,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l562,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1464,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1479,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l485,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l616,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l911,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1549,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1551,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l828,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l12,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l49,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1468,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1322,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l486,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1558,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1524,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l845,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1265,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1562,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1582,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l836,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1304,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l563,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1357,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1385,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1432,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1552,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1321,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1363,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1516,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1509,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l881,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1596,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l535,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1281,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1449,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1626,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1662,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l502,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1433,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l493,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l500,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1475,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1360,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1462,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1661,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l876,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l843,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1778,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l815,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1542,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l981,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1586,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1274,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l666,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1053,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l847,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1593,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l853,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1382,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1288,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1512,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l835,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1711,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1163,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1371,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1361,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l890,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l889,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l86,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1599,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l528,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1594,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1491,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1517,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1421,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1605,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1261,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1589,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1476,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1170,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1384,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1424,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1485,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1604,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1364,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1511,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1294,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1316,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(z))) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l529,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1038,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1347,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1228,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1388,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1922,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1333,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1653,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1295,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l743,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l984,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1370,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1716,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1614,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l507,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1533,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1796,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1039,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l628,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l844,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1411,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l860,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1495,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1637,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l839,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l838,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1544,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1314,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1331,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1282,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1270,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l841,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1675,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1052,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1169,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l508,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l852,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1707,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1554,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1629,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l491,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1526,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1497,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1358,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1802,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1301,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1268,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1499,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1560,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1436,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1821,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1290,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1336,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l855,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1359,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1473,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1530,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1906,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1627,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1672,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1366,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1896,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1703,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1588,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1591,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1397,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1494,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1774,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1731,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1592,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l867,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l691,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1403,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1438,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1607,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1343,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l858,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1986,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1977,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1393,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1665,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l510,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1297,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l559,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1740,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1864,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1287,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1362,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1767,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1993,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1826,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1632,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1746,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1437,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1777,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1858,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1419,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1302,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1719,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l516,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1776,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l872,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1645,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1498,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1817,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1666,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1887,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l880,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1754,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1702,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1978,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1813,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2047,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2019,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1522,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l898,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1590,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1380,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l840,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l522,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1752,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1712,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1750,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l519,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1601,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1919,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1962,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1799,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l866,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l885,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1266,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l2067,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1976,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2041,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1575,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1329,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1323,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1383,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2062,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1814,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l869,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1642,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1550,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l503,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1771,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l871,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l42,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1676,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2053,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1553,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l908,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1865,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l553,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1339,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l2052,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1563,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l536,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1529,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1576,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1979,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2037,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1818,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l842,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1907,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l874,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1532,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1756,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1981,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1408,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1762,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1566,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1811,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1307,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1519,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1488,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l873,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l878,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1715,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l868,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l483,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1801,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1577,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1600,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l579,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1489,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1779,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1982,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l978,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1022,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1780,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1685,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1398,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2048,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1751,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1585,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1757,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1537,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2050,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1508,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l903,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l596,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l587,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l540,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l489,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1670,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1677,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1706,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l524,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1935,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2061,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2072,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1538,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1983,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1597,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2055,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l870,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2065,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1365,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2094,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2044,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1987,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1617,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1957,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1980,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1045,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2233,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1733,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1924,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1644,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l504,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2095,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1950,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2178,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1991,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1829,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1807,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2159,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l565,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1469,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1606,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1573,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2042,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1791,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2077,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1638,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2104,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l531,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1074,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1062,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1619,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1071,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1063,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1669,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1836,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1658,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1618,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2083,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2016,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1781,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1640,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1192,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2075,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1197,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1747,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1622,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1639,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2057,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1578,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1917,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1214,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1869,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1182,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1547,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1186,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l530,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2014,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1933,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1612,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1770,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1581,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1838,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1914,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1651,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2015,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1625,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1195,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1772,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2244,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1233,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1194,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2234,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1183,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1193,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1587,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1949,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l532,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2064,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1909,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1292,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1820,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2211,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1918,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l895,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 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(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))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2247,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2186,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l533,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2126,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2207,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1960,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2193,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l877,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1659,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2112,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1959,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2138,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2197,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2124,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1615,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2258,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2039,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2098,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2134,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1806,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2238,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2139,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2132,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1235,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1784,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2214,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1571,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2153,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2054,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2149,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1572,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l560,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1768,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1564,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1912,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2033,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1580,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2040,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1569,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l879,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1470,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2331,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1636,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2118,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1945,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1755,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1608,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2224,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2217,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2169,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l875,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1472,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1958,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2205,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2145,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2206,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1565,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1624,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1633,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2188,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2121,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2248,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2332,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2316,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1609,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2329,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l550,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2036,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2323,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1567,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2140,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2151,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2074,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2319,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1568,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1667,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2168,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2230,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1531,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l946,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2063,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2034,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1487,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2076,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2163,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2192,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2180,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2152,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l583,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2227,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2194,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2058,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2164,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[4]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l6,l31,l36,l476,l806,l1315,l52,l2,l26,l62,l3,l63,l75,l193,l495,l221,l501,l1283,l1430,l1386,l1252,l496,l7,l85,l475,l1259,l1431,l482,l620,l1279,l832,l786,l505,l4,l1439,l1310,l499,l1444,l1291,l1264,l1334,l1285,l484,l487,l488,l477,l497,l1440,l1325,l498,l1262,l478,l1441,l1434,l1263,l1458,l1277,l509,l1465,l506,l1442,l1471,l480,l481,l474,l1448,l1492,l1280,l1451,l1435,l1311,l527,l25,l621,l492,l1447,l618,l1466,l1501,l1349,l40,l557,l1502,l554,l1450,l561,l562,l1464,l1479,l485,l616,l911,l1549,l1551,l828,l12,l49,l1468,l1322,l486,l1558,l1524,l845,l1265,l1562,l1582,l836,l1304,l563,l1357,l1385,l1432,l1552,l1321,l1363,l1516,l1509,l881,l1596,l535,l1281,l1449,l1626,l1662,l502,l1433,l493,l500,l1475,l1360,l1462,l1661,l876,l843,l1778,l815,l1542,l981,l1586,l1274,l666,l1053,l847,l1593,l853,l1382,l1288,l1512,l835,l1711,l1163,l1371,l1361,l890,l889,l86,l1599,l528,l1594,l1491,l1517,l1421,l1605,l1261,l1589,l1476,l1170,l1384,l1424,l1485,l1604,l1364,l1511,l1294,l1316,l529,l1038,l1347,l1228,l1388,l1922,l1333,l1653,l1295,l743,l984,l1370,l1716,l1614,l507,l1533,l1796,l1039,l628,l844,l1411,l860,l1495,l1637,l839,l838,l1544,l1314,l1331,l1282,l1270,l841,l1675,l1052,l1169,l508,l852,l1707,l1554,l1629,l491,l1526,l1497,l1358,l1802,l1301,l1268,l1499,l1560,l1436,l1821,l1290,l1336,l855,l1359,l1473,l1530,l1906,l1627,l1672,l1366,l1896,l1703,l1588,l1591,l1397,l1494,l1774,l1731,l1592,l867,l691,l1403,l1438,l1607,l1343,l858,l1986,l1977,l1393,l1665,l510,l1297,l559,l1740,l1864,l1287,l1362,l1767,l1993,l1826,l1632,l1746,l1437,l1777,l1858,l1419,l1302,l1719,l516,l1776,l872,l1645,l1498,l1817,l1666,l1887,l880,l1754,l1702,l1978,l1813,l2047,l2019,l1522,l898,l1590,l1380,l840,l522,l1752,l1712,l1750,l519,l1601,l1919,l1962,l1799,l866,l885,l1266,l2067,l1976,l2041,l1575,l1329,l1323,l1383,l2062,l1814,l869,l1642,l1550,l503,l1771,l871,l42,l1676,l2053,l1553,l908,l1865,l553,l1339,l2052,l1563,l536,l1529,l1576,l1979,l2037,l1818,l842,l1907,l874,l1532,l1756,l1981,l1408,l1762,l1566,l1811,l1307,l1519,l1488,l873,l878,l1715,l868,l483,l1801,l1577,l1600,l579,l1489,l1779,l1982,l978,l1022,l1780,l1685,l1398,l2048,l1751,l1585,l1757,l1537,l2050,l1508,l903,l596,l587,l540,l489,l1670,l1677,l1706,l524,l1935,l2061,l2072,l1538,l1983,l1597,l2055,l870,l2065,l1365,l2094,l2044,l1987,l1617,l1957,l1980,l1045,l2233,l1733,l1924,l1644,l504,l2095,l1950,l2178,l1991,l1829,l1807,l2159,l565,l1469,l1606,l1573,l2042,l1791,l2077,l1638,l2104,l531,l1074,l1062,l1619,l1071,l1063,l1669,l1836,l1658,l1618,l2083,l2016,l1781,l1640,l1192,l2075,l1197,l1747,l1622,l1639,l2057,l1578,l1917,l1214,l1869,l1182,l1547,l1186,l530,l2014,l1933,l1612,l1770,l1581,l1838,l1914,l1651,l2015,l1625,l1195,l1772,l2244,l1233,l1194,l2234,l1183,l1193,l1587,l1949,l532,l2064,l1909,l1292,l1820,l2211,l1918,l895,l2247,l2186,l533,l2126,l2207,l1960,l2193,l877,l1659,l2112,l1959,l2138,l2197,l2124,l1615,l2258,l2039,l2098,l2134,l1806,l2238,l2139,l2132,l1235,l1784,l2214,l1571,l2153,l2054,l2149,l1572,l560,l1768,l1564,l1912,l2033,l1580,l2040,l1569,l879,l1470,l2331,l1636,l2118,l1945,l1755,l1608,l2224,l2217,l2169,l875,l1472,l1958,l2205,l2145,l2206,l1565,l1624,l1633,l2188,l2121,l2248,l2332,l2316,l1609,l2329,l550,l2036,l2323,l1567,l2140,l2151,l2074,l2319,l1568,l1667,l2168,l2230,l1531,l946,l2063,l2034,l1487,l2076,l2163,l2192,l2180,l2152,l583,l2227,l2194,l2058,l2164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYO664-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 : n024.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:09:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.34 % launching worker at depth: 11
% 0.12/0.35 % launching worker at depth: 12
% 0.18/0.40 % launching worker at depth: 13
% 1.68/0.55 % launching worker at depth: 14
% 12.27/1.95 % launching worker at depth: 15
% 46.50/6.20 % launching worker at depth: 16
% 61.31/8.07 % SZS status Theorem for theBenchmark
% 61.31/8.07 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------