%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO666-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:10 PM UTC 2025
% Result : Unsatisfiable 263.85s 33.72s
% Output : CNFRefutation 264.65s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_83)
% Comments :
%------------------------------------------------------------------------------
cnf(5,plain,
'LE'(f(X0),s(s('0'))),
inference(cnf,[status(esa)],[clause_83]) ).
cnf(l0,plain,
'LE'(f(suc(suc(z))),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(7,plain,
( ~ 'LE'(f(suc(X0)),s(s('0')))
| 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X0),s('0')) ),
inference(cnf,[status(esa)],[clause_29]) ).
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)],[7]) ).
cnf(3,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_123]) ).
cnf(l4,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(1,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_12]) ).
cnf(l81,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(9,plain,
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X3))
| ~ 'E'(s('0'),f(X4))
| ~ 'E'(s('0'),f(X5))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X3)))
| ~ 'E'(s('0'),f(suc(X4)))
| ~ 'E'(s('0'),f(suc(X5)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X4),suc(X1)) ),
inference(cnf,[status(esa)],[clause_179]) ).
cnf(l134,plain,
( ~ '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(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1228,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1415,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1230,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(8,plain,
( ~ 'LE'(f(X0),s(s('0')))
| 'E'(s('0'),f(X0))
| 'LE'(f(X0),s('0')) ),
inference(cnf,[status(esa)],[clause_185]) ).
cnf(l1478,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(4,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_42]) ).
cnf(l1456,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l136,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1436,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l163,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1479,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(0,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X4),suc(X5))
| ~ iLEQ(suc(X5),suc(X0)) ),
inference(cnf,[status(esa)],[clause_102]) ).
cnf(l5641,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1472,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5377,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5378,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1235,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1236,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1531,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1229,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1425,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l180,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(2,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_98]) ).
cnf(l7,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5631,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l276,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l198,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5627,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1412,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5404,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1483,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5660,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1422,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1459,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(6,plain,
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_70]) ).
cnf(l296,plain,
( ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1480,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5652,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l314,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5512,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1473,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5380,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5702,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5640,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5661,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5630,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5642,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5410,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5632,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1420,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5405,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5650,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5659,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5379,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1534,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1451,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5435,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5657,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5671,plain,
( ~ '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(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(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l5703,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5704,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5629,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1448,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5696,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1485,plain,
( ~ 'LE'(f(z),s(s('0')))
| 'E'(s('0'),f(z))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5384,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5628,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5709,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2,plain,
( ~ '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(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))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 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)))
| ~ iLEQ(suc(suc(z)),suc(suc(z))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l19,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l11,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)],[6]) ).
cnf(l20,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
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)],[7]) ).
cnf(l77,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5699,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l36,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)],[6]) ).
cnf(l5694,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5705,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5408,plain,
'LE'(f(z),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5406,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l39,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l56,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5648,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5651,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1458,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l49,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l55,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5634,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l9,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)],[6]) ).
cnf(l128,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l61,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l15,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5693,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l51,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l65,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l8,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)],[6]) ).
cnf(l22,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l217,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l204,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l37,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l125,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l50,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5649,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5695,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l89,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l329,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l76,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l26,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5697,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l80,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12,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)],[6]) ).
cnf(l53,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l68,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l126,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3136,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3141,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l75,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l97,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5698,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l380,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l158,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l413,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5701,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5736,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l101,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l271,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3156,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3934,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l159,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1315,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3126,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l330,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l74,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3383,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5820,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5803,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l29,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l375,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l312,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l17,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l23,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l108,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l245,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3133,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l265,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l127,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5776,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l268,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l109,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l84,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5700,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l192,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l87,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5779,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3199,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l321,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4336,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l332,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l319,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l18,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l13,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l100,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3234,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4478,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3197,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l381,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4483,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3307,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5835,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l95,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l103,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l78,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4200,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3224,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3188,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3547,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3335,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3246,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l110,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l160,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5895,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5831,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3531,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3578,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3395,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4108,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l257,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4476,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l45,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l46,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l294,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3321,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l170,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5804,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3767,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l52,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5874,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3979,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3308,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l25,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l169,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3252,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5849,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3648,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5872,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5829,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l226,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5827,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5942,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l200,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l14,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3186,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l315,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3647,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3657,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5975,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l290,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5881,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5844,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6096,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5852,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5897,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l210,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5903,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6151,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l27,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l58,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5828,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4171,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5839,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5838,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l24,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l57,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l6053,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l234,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4366,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l274,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5856,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l405,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l107,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3250,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5814,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6063,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3221,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5822,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5713,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l72,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5884,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3819,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l202,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3924,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3768,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l221,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l291,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6168,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4084,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5807,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5993,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6104,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l214,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l172,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l218,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3809,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5987,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3650,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l285,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4235,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3190,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3328,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l99,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3201,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l219,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l184,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5813,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3454,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l30,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5857,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4367,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3645,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3684,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3202,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6061,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3233,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l224,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l389,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4737,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3501,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l343,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l34,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5847,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5833,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5933,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5913,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l31,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l416,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5875,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5781,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3811,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3212,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6106,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3229,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3343,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l4163,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5854,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l28,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l261,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3783,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3662,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3332,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3203,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3330,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3243,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5907,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5865,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3139,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l316,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l417,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5914,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3895,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3540,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3667,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5711,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3898,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6021,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3492,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l181,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3687,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6110,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5936,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3497,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3689,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3448,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3800,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5805,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4085,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3784,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5808,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3878,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5889,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5131,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5851,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3742,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5819,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6009,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5932,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3963,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l230,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6344,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4095,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3635,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3247,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5860,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6049,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6121,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4340,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5790,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6108,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3579,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6169,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3539,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5986,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3455,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5830,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3493,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6136,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6122,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5842,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4111,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3254,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l394,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l183,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6072,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3506,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4480,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3765,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5935,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6238,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5923,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5855,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6170,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l62,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3857,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3507,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6148,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3129,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l33,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5816,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l318,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5934,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3556,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6362,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5899,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4073,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6209,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5834,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5898,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6231,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l371,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l44,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3791,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l309,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
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)],[7]) ).
cnf(l201,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6308,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4227,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5837,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5716,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3237,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6134,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3722,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5848,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4474,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6156,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5771,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l264,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3227,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5821,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3896,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6187,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5840,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l216,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l228,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3325,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l205,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l21,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5905,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5783,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5773,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3132,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5894,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6099,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l66,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5836,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5864,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4234,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3498,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3310,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5902,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3500,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3342,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3326,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3347,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6315,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5915,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6129,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6031,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l35,plain,
( ~ 'E'('0',f(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)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3744,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5846,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5772,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5843,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6152,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6171,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3346,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6130,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3466,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5863,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l187,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5789,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6347,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l157,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3255,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3815,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l340,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5802,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3823,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l114,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6154,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5892,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l149,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4780,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6240,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3725,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5810,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5823,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3897,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6274,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l41,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6214,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l144,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l135,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l189,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3499,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l151,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6103,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l233,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l364,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6239,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6114,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l212,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5917,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5762,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4238,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5793,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l43,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l347,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6180,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3336,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5926,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l42,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l241,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l182,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5939,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5908,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3712,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l146,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3240,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3244,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5906,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l356,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6070,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3900,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3215,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6201,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5850,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3223,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5870,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3382,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5883,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6333,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6230,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6126,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3419,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l194,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6380,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3871,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l162,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6402,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6185,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5759,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6216,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l352,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5925,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3435,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4750,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5799,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6219,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6112,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5770,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6232,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l153,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3721,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l367,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3529,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5877,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6318,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3538,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5890,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l145,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l195,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5927,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3537,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6234,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4792,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6113,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6150,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3137,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l148,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6401,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5801,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5929,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5901,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5866,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6284,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6370,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3849,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5786,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4123,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6203,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6316,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3891,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3562,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6008,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6282,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6117,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4145,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6367,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l237,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6039,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5931,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5853,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4261,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l152,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3658,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5909,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3191,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4745,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l346,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5989,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5826,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3708,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l359,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4348,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4749,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l378,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l166,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6215,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5924,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5904,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3194,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l138,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l38,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6363,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l143,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l193,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3504,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5780,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3879,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4260,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l393,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3459,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6125,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5930,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3491,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l133,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6279,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6373,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6196,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l338,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5800,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6376,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4759,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5778,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6119,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3261,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4844,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5916,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3813,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5858,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l397,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l361,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5867,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4467,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3486,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6002,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6366,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5992,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6355,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6354,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4420,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4318,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4386,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6349,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5268,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6205,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6365,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6176,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6042,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6211,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6178,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5763,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6338,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6160,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3883,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4757,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l139,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6368,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6392,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l225,plain,
( ~ 'LE'(f(suc(z)),s(s('0')))
| 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l150,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3426,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3487,plain,
'LE'(f(suc(z)),s(s('0'))),
inference(instantiation,[status(thm)],[5]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l4,l81,l134,l1228,l1415,l1230,l1478,l1456,l136,l1436,l163,l1479,l5641,l1472,l5377,l5378,l1235,l1236,l1531,l1229,l1425,l180,l7,l5631,l276,l198,l5627,l1412,l5404,l1483,l5660,l1422,l1459,l296,l1480,l5652,l314,l5512,l1473,l5380,l5702,l5640,l5661,l5630,l5642,l5410,l5632,l1420,l5405,l5650,l5659,l5379,l1534,l1451,l5435,l5657,l5671,l5703,l5704,l5629,l1448,l5696,l1485,l5384,l5628,l5709,l2,l19,l11,l20,l40,l77,l5699,l36,l5694,l5705,l5408,l5406,l39,l56,l5648,l5651,l1458,l49,l55,l5634,l9,l128,l5,l61,l6,l15,l5693,l51,l65,l8,l22,l217,l204,l37,l125,l3,l50,l5649,l5695,l89,l329,l76,l26,l5697,l80,l12,l53,l68,l126,l3136,l3141,l75,l97,l5698,l380,l158,l413,l5701,l5736,l101,l271,l3156,l3934,l159,l1315,l3126,l330,l74,l3383,l5820,l5803,l29,l375,l312,l17,l23,l108,l245,l3133,l265,l127,l5776,l268,l109,l84,l5700,l192,l10,l87,l5779,l3199,l321,l4336,l332,l319,l18,l13,l100,l3234,l4478,l3197,l381,l4483,l3307,l5835,l95,l103,l78,l4200,l3224,l3188,l3547,l3335,l3246,l110,l160,l5895,l5831,l3531,l3578,l3395,l4108,l257,l4476,l45,l46,l294,l3321,l170,l5804,l3767,l52,l5874,l3979,l3308,l25,l169,l3252,l5849,l3648,l5872,l5829,l226,l5827,l5942,l200,l14,l3186,l315,l3647,l3657,l5975,l290,l5881,l5844,l6096,l5852,l5897,l210,l5903,l6151,l27,l58,l5828,l4171,l5839,l5838,l24,l57,l6053,l234,l4366,l274,l5856,l405,l107,l3250,l5814,l6063,l3221,l5822,l5713,l72,l5884,l3819,l202,l3924,l3768,l221,l291,l6168,l4084,l5807,l5993,l6104,l214,l172,l218,l3809,l5987,l3650,l285,l4235,l3190,l3328,l99,l3201,l219,l184,l5813,l3454,l30,l5857,l4367,l3645,l3684,l3202,l6061,l3233,l224,l389,l4737,l3501,l343,l34,l5847,l5833,l5933,l5913,l31,l416,l5875,l5781,l3811,l3212,l6106,l3229,l3343,l4163,l5854,l28,l261,l3783,l3662,l3332,l3203,l3330,l3243,l5907,l5865,l3139,l316,l417,l5914,l3895,l3540,l3667,l5711,l3898,l6021,l3492,l181,l3687,l6110,l5936,l3497,l3689,l3448,l3800,l5805,l4085,l3784,l5808,l3878,l5889,l5131,l5851,l3742,l5819,l6009,l5932,l3963,l230,l6344,l4095,l3635,l3247,l5860,l6049,l6121,l4340,l5790,l6108,l3579,l6169,l3539,l5986,l3455,l5830,l3493,l6136,l6122,l5842,l4111,l3254,l394,l183,l6072,l3506,l4480,l3765,l5935,l6238,l5923,l5855,l6170,l62,l3857,l3507,l6148,l3129,l33,l5816,l318,l5934,l3556,l6362,l5899,l4073,l6209,l5834,l5898,l6231,l371,l44,l3791,l309,l63,l201,l6308,l4227,l5837,l5716,l3237,l6134,l3722,l5848,l4474,l6156,l5771,l264,l3227,l5821,l3896,l6187,l5840,l216,l228,l3325,l205,l21,l5905,l5783,l5773,l3132,l5894,l6099,l66,l5836,l5864,l4234,l3498,l3310,l5902,l3500,l3342,l3326,l3347,l6315,l5915,l6129,l6031,l35,l3744,l5846,l5772,l5843,l6152,l6171,l3346,l6130,l3466,l5863,l187,l5789,l6347,l157,l3255,l3815,l340,l5802,l3823,l114,l6154,l5892,l149,l4780,l6240,l3725,l5810,l5823,l3897,l6274,l41,l6214,l144,l135,l189,l3499,l151,l6103,l233,l364,l6239,l6114,l212,l5917,l5762,l4238,l5793,l43,l347,l6180,l3336,l5926,l42,l241,l182,l5939,l5908,l3712,l146,l3240,l3244,l5906,l356,l6070,l3900,l3215,l6201,l5850,l3223,l5870,l3382,l5883,l6333,l6230,l6126,l3419,l194,l6380,l3871,l162,l6402,l6185,l5759,l6216,l352,l5925,l3435,l4750,l5799,l6219,l6112,l5770,l6232,l153,l3721,l367,l3529,l5877,l6318,l3538,l5890,l145,l195,l5927,l3537,l6234,l4792,l6113,l6150,l3137,l148,l6401,l5801,l5929,l5901,l5866,l6284,l6370,l3849,l5786,l4123,l6203,l6316,l3891,l3562,l6008,l6282,l6117,l4145,l6367,l237,l6039,l5931,l5853,l4261,l152,l3658,l5909,l3191,l4745,l346,l5989,l5826,l3708,l359,l4348,l4749,l378,l166,l6215,l5924,l5904,l3194,l138,l38,l6363,l143,l193,l3504,l5780,l3879,l4260,l393,l3459,l6125,l5930,l3491,l133,l6279,l6373,l6196,l338,l5800,l6376,l4759,l5778,l6119,l3261,l4844,l5916,l3813,l5858,l397,l361,l5867,l4467,l3486,l6002,l6366,l5992,l6355,l6354,l4420,l4318,l4386,l6349,l5268,l6205,l6365,l6176,l6042,l6211,l6178,l5763,l6338,l6160,l3883,l4757,l139,l6368,l6392,l225,l150,l3426,l3487]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : SYO666-1 : TPTP v9.0.0. Released v7.3.0.
% 0.07/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.36 % Computer : n024.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8042.1875MB
% 0.12/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Tue Jul 22 20:10:00 EDT 2025
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % launching worker at depth: 5
% 0.12/0.36 % launching worker at depth: 4
% 0.12/0.36 % launching worker at depth: 6
% 0.12/0.36 % launching worker at depth: 8
% 0.12/0.36 % launching worker at depth: 3
% 0.12/0.36 % launching worker at depth: 2
% 0.12/0.36 % launching worker at depth: 1
% 0.12/0.36 % launching worker at depth: 7
% 0.12/0.36 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 0.12/0.37 % launching worker at depth: 11
% 0.12/0.38 % launching worker at depth: 12
% 0.18/0.45 % launching worker at depth: 13
% 2.31/0.67 % launching worker at depth: 14
% 10.64/1.73 % launching worker at depth: 15
% 113.14/14.65 % launching worker at depth: 16
% 263.85/33.72 % SZS status Theorem for theBenchmark
% 263.85/33.72 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------