%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO648-1 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : 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:08 PM UTC 2025
% Result : Unsatisfiable 17.35s 2.59s
% Output : CNFRefutation 17.35s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_299)
% Comments :
%------------------------------------------------------------------------------
cnf(7,plain,
'LE'(f(X0),s('0')),
inference(cnf,[status(esa)],[clause_299]) ).
cnf(l0,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(18,plain,
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_114]) ).
cnf(l1,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[18]) ).
cnf(3,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(suc(X0))))
| 'E'(f(X1),f(suc(suc(X1)))) ),
inference(cnf,[status(esa)],[clause_79]) ).
cnf(l2,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(5,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(X0))))) ),
inference(cnf,[status(esa)],[clause_326]) ).
cnf(l819,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(20,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_160]) ).
cnf(l16,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(2,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0))) ),
inference(cnf,[status(esa)],[clause_48]) ).
cnf(l877,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(25,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_62]) ).
cnf(l11,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(13,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
inference(cnf,[status(esa)],[clause_168]) ).
cnf(l1002,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(4,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| 'E'(f(X1),f(suc(suc(suc(X1))))) ),
inference(cnf,[status(esa)],[clause_90]) ).
cnf(l945,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(suc(z)))))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(8,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_157]) ).
cnf(l44,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l948,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l977,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l993,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(9,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_328]) ).
cnf(l1065,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l994,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1043,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l853,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1034,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l970,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1057,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l82,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1032,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(23,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1))))) ),
inference(cnf,[status(esa)],[clause_145]) ).
cnf(l1033,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1098,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1166,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1101,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1026,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l95,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1005,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1116,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1006,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l128,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1007,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1206,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l831,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1150,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l968,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1143,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(1,plain,
( ~ 'LE'(f(suc(suc(suc(X0)))),s('0'))
| 'E'('0',f(suc(suc(suc(X0)))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_260]) ).
cnf(l846,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1011,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1278,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l829,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1035,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1145,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l129,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1050,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l957,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1199,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1301,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l975,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1103,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1425,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l976,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1232,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l55,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1077,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(14,plain,
( ~ 'LE'(f(suc(suc(suc(suc(X0))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(X0))))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_231]) ).
cnf(l130,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(17,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(cnf,[status(esa)],[clause_254]) ).
cnf(l467,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l57,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l820,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1153,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1151,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1028,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1069,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1019,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1244,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1173,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1089,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l133,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l136,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1072,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1264,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1139,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1045,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1272,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1119,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1039,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l873,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1216,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l185,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l898,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1274,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1123,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l879,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1450,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1027,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1147,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1082,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1520,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1060,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1292,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1225,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l836,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1058,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1042,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1451,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1068,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l350,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l997,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1273,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1521,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1181,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1176,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1412,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1157,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l980,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1012,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1275,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1376,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l854,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1029,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1230,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1440,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1044,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1207,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1146,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1066,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l178,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1423,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l964,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l842,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1436,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1527,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1345,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1038,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l960,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1508,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l469,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1266,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1083,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1047,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1284,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1282,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1221,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1084,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1507,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1408,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1114,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1004,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1574,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l826,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1265,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1008,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1518,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1363,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1366,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l182,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1330,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l861,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l179,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1287,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1415,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1022,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1458,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1193,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1179,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1107,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1059,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1298,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l153,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1603,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1237,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1416,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l961,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l992,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1300,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l170,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l966,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1368,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1523,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1522,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1484,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1051,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1289,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1460,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1025,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1643,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1097,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1112,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1085,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1619,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1124,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1421,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l48,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1197,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1055,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1573,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1037,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1067,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1017,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1152,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l561,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1270,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1459,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l251,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1515,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1524,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1503,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l407,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1156,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1293,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1234,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1597,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1099,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1115,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1486,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1599,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1268,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1490,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l821,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1435,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1635,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1478,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1175,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1267,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1646,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1531,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1480,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1655,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1323,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1670,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1672,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l856,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1634,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1556,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1463,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1514,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1331,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1070,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1595,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1500,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1049,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l982,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1353,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1111,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1481,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l851,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1575,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1694,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1164,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1299,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1121,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1509,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1338,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1571,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1730,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1214,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1516,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1741,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l912,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1472,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l924,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1724,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1699,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l849,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l971,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1428,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1290,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1782,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1205,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1622,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1260,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1763,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1385,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l270,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1700,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1288,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1559,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1048,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1245,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1247,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1664,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1277,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1009,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1596,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1249,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1320,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1504,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l844,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l916,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l848,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1598,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1547,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l852,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1506,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1537,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1401,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1118,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1018,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1511,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1569,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1644,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1155,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1056,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1354,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1341,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1294,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1566,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1785,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1564,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1375,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1144,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1212,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1722,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1488,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1822,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1346,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1659,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1410,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1513,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l171,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1510,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l823,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1696,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1656,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l822,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1767,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1550,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1851,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1746,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l995,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1159,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1660,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(suc(z)))))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1938,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1786,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1637,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1525,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1302,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1731,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1567,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1403,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1558,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1903,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1397,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1877,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1841,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1836,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2019,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1803,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1698,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l913,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1652,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1658,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1918,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1357,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1788,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1154,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1476,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1610,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1738,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1691,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1772,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1561,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1883,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1095,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1308,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1917,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1565,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2061,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2064,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1945,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1657,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2011,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2199,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1729,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2003,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2007,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1666,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1723,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2053,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1911,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1661,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2045,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2156,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1307,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1939,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2017,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2020,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1987,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2203,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2205,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2049,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1833,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2242,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1759,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1126,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1870,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2025,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2054,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l983,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2207,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2048,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1620,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1695,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1483,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2243,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1563,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2027,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1921,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2032,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1818,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l910,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1394,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l934,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1933,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1916,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1912,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1977,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1806,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2231,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1924,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l946,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1871,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2122,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1350,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1015,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1811,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1930,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1600,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2197,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1915,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2171,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2026,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2029,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1882,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1623,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2004,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2241,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2047,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2204,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1805,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1955,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1540,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1799,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l950,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2044,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1925,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2196,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1849,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1318,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l990,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2202,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l981,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2232,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1040,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2200,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1808,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l987,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1948,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2219,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1422,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1654,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l996,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2159,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2182,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1489,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2016,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1976,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l984,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l951,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(z))))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1867,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2167,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2198,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1810,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1936,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2056,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2057,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1024,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2177,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l947,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2221,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2236,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1295,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2018,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l972,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1063,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1847,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2033,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1732,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2050,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2059,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2015,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1964,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2060,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1931,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2097,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2114,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1755,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2083,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1990,plain,
'LE'(f(suc(suc(suc(suc(z))))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2190,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2230,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2248,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l985,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1718,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1352,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2062,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2051,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l953,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l988,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2070,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2108,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2058,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2157,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1570,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l967,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1873,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1576,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1751,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1952,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2252,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1407,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1719,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1913,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2244,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2201,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1784,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1036,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1974,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1838,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1853,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1953,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l986,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1928,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2055,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2046,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2155,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1914,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2034,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1852,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1975,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2250,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1713,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2028,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1827,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2052,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1720,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2089,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1965,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1954,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1406,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1956,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1835,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2063,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2265,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2251,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2249,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2145,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l991,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2071,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l989,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2140,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(suc(z)))))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2038,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1568,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2309,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2316,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2041,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1922,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2335,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2336,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2313,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2338,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2339,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2331,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1837,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2065,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2311,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2323,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2308,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1923,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(suc(z))))
| 'E'(f(z),f(suc(suc(suc(z)))))
| 'E'(f(z),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2305,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2326,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2342,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2330,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2341,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1721,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2349,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2036,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2334,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2364,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2307,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2356,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2344,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2037,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2306,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2389,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2328,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2350,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2352,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2319,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2340,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2345,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2373,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2366,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2347,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2321,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2348,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2329,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2343,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2310,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2353,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2370,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2368,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2362,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2357,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2358,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2355,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2365,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2314,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| 'E'('0',f(suc(suc(suc(z)))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2346,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2390,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2369,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2363,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2324,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2354,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2367,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l958,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1581,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2315,plain,
'LE'(f(suc(suc(suc(z)))),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2245,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1580,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2224,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2246,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2372,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1949,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2371,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1950,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2351,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1951,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2292,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2397,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[7]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l819,l16,l877,l11,l1002,l945,l44,l948,l977,l993,l1065,l994,l1043,l853,l1034,l970,l1057,l82,l1032,l1033,l1098,l1166,l1101,l1026,l95,l1005,l1116,l1006,l128,l1007,l1206,l831,l1150,l968,l1143,l846,l1011,l1278,l829,l1035,l1145,l129,l1050,l957,l1199,l1301,l975,l1103,l1425,l976,l1232,l55,l1077,l130,l467,l57,l820,l1153,l1151,l1028,l1069,l1019,l1244,l1173,l1089,l133,l136,l1072,l1264,l1139,l1045,l1272,l4,l1119,l1039,l873,l1216,l185,l898,l1274,l1123,l879,l1450,l7,l1027,l1147,l1082,l1520,l1060,l1292,l1225,l836,l1058,l1042,l1451,l1068,l350,l997,l1273,l1521,l1181,l1176,l1412,l1157,l980,l1012,l1275,l1376,l854,l1029,l1230,l1440,l1044,l1207,l1146,l1066,l178,l1423,l964,l842,l1436,l1527,l1345,l1038,l960,l1508,l469,l1266,l1083,l1047,l1284,l1282,l1221,l1084,l1507,l1408,l1114,l1004,l1574,l826,l1265,l1008,l1518,l1363,l1366,l182,l1330,l861,l179,l1287,l1415,l1022,l1458,l1193,l1179,l1107,l1059,l1298,l153,l1603,l1237,l1416,l961,l992,l1300,l170,l966,l1368,l1523,l1522,l1484,l1051,l1289,l1460,l1025,l1643,l1097,l1112,l1085,l1619,l1124,l1421,l48,l1197,l1055,l1573,l1037,l1067,l1017,l1152,l561,l1270,l1459,l251,l1515,l1524,l1503,l407,l1156,l1293,l1234,l1597,l1099,l1115,l1486,l1599,l1268,l1490,l821,l1435,l1635,l1478,l1175,l1267,l1646,l1531,l1480,l1655,l1323,l1670,l1672,l856,l1634,l1556,l1463,l1514,l1331,l1070,l1595,l1500,l1049,l982,l1353,l1111,l1481,l851,l1575,l1694,l1164,l1299,l1121,l1509,l1338,l1571,l1730,l1214,l1516,l1741,l912,l1472,l924,l1724,l1699,l849,l971,l1428,l1290,l1782,l1205,l1622,l1260,l1763,l1385,l270,l1700,l1288,l1559,l1048,l1245,l1247,l1664,l1277,l1009,l1596,l1249,l1320,l1504,l844,l916,l848,l1598,l1547,l852,l1506,l1537,l1401,l1118,l1018,l1511,l1569,l1644,l1155,l1056,l1354,l1341,l1294,l1566,l1785,l1564,l1375,l1144,l1212,l1722,l1488,l1822,l1346,l1659,l1410,l1513,l171,l1510,l823,l1696,l1656,l822,l1767,l1550,l1851,l1746,l995,l1159,l1660,l1938,l1786,l1637,l1525,l1302,l1731,l1567,l1403,l1558,l1903,l1397,l1877,l1841,l1836,l2019,l1803,l1698,l913,l1652,l1658,l1918,l1357,l1788,l1154,l1476,l1610,l1738,l1691,l1772,l1561,l1883,l1095,l1308,l1917,l1565,l2061,l2064,l1945,l1657,l2011,l2199,l1729,l2003,l2007,l1666,l1723,l2053,l1911,l1661,l2045,l2156,l1307,l1939,l2017,l2020,l1987,l2203,l2205,l2049,l1833,l2242,l1759,l1126,l1870,l2025,l2054,l983,l2207,l2048,l1620,l1695,l1483,l2243,l1563,l2027,l1921,l2032,l1818,l910,l1394,l934,l1933,l1916,l1912,l1977,l1806,l2231,l1924,l946,l1871,l2122,l1350,l1015,l1811,l1930,l1600,l2197,l1915,l2171,l2026,l2029,l1882,l1623,l2004,l2241,l2047,l2204,l1805,l1955,l1540,l1799,l950,l2044,l1925,l2196,l1849,l1318,l990,l2202,l981,l2232,l1040,l2200,l1808,l987,l1948,l2219,l1422,l1654,l996,l2159,l2182,l1489,l2016,l1976,l984,l951,l1867,l2167,l2198,l1810,l1936,l2056,l2057,l1024,l2177,l947,l2221,l2236,l1295,l2018,l972,l1063,l1847,l2033,l1732,l2050,l2059,l2015,l1964,l2060,l1931,l2097,l2114,l1755,l2083,l1990,l2190,l2230,l2248,l985,l1718,l1352,l2062,l2051,l953,l988,l2070,l2108,l2058,l2157,l1570,l967,l1873,l1576,l1751,l1952,l2252,l1407,l1719,l1913,l2244,l2201,l1784,l1036,l1974,l1838,l1853,l1953,l986,l1928,l2055,l2046,l2155,l1914,l2034,l1852,l1975,l2250,l1713,l2028,l1827,l2052,l1720,l2089,l1965,l1954,l1406,l1956,l1835,l2063,l2265,l2251,l2249,l2145,l991,l2071,l989,l2140,l2038,l1568,l2309,l2316,l2041,l1922,l2335,l2336,l2313,l2338,l2339,l2331,l1837,l2065,l2311,l2323,l2308,l1923,l2305,l2326,l2342,l2330,l2341,l1721,l2349,l2036,l2334,l2364,l2307,l2356,l2344,l2037,l2306,l2389,l2328,l2350,l2352,l2319,l2340,l2345,l2373,l2366,l2347,l2321,l2348,l2329,l2343,l2310,l2353,l2370,l2368,l2362,l2357,l2358,l2355,l2365,l2314,l2346,l2390,l2369,l2363,l2324,l2354,l2367,l958,l1581,l2315,l2245,l1580,l2224,l2246,l2372,l1949,l2371,l1950,l2351,l1951,l2292,l2397]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYO648-1 : TPTP v9.0.0. Released v7.3.0.
% 0.07/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jul 22 20:06:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.35 % launching worker at depth: 4
% 0.13/0.35 % launching worker at depth: 6
% 0.13/0.35 % launching worker at depth: 1
% 0.13/0.35 % launching worker at depth: 2
% 0.13/0.35 % launching worker at depth: 5
% 0.13/0.35 % launching worker at depth: 7
% 0.13/0.35 % launching worker at depth: 8
% 0.13/0.35 % launching worker at depth: 3
% 0.13/0.35 % launching worker at depth: 9
% 0.13/0.37 % launching worker at depth: 10
% 0.13/0.40 % launching worker at depth: 11
% 1.96/0.58 % launching worker at depth: 12
% 12.57/1.91 % launching worker at depth: 13
% 17.35/2.59 % SZS status Theorem for theBenchmark
% 17.35/2.59 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------