%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO652-1 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 09:59:08 PM UTC 2025
% Result : Unsatisfiable 1.27s 0.52s
% Output : CNFRefutation 1.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause_199)
% Comments :
%------------------------------------------------------------------------------
cnf(5,plain,
'LE'(f(X0),s('0')),
inference(cnf,[status(esa)],[clause_199]) ).
cnf(l0,plain,
'LE'(f(z),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(11,plain,
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_17]) ).
cnf(l1,plain,
( ~ 'LE'(f(z),s('0'))
| 'E'('0',f(z))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[11]) ).
cnf(15,plain,
~ 'LE'(f(z),'0'),
inference(cnf,[status(esa)],[clause_99]) ).
cnf(l7,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(2,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X3),f(suc(X3))) ),
inference(cnf,[status(esa)],[clause_16]) ).
cnf(l2,plain,
( ~ '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)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z)))
| 'E'(f(z),f(suc(z))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(6,plain,
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_191]) ).
cnf(l25,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(3,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_149]) ).
cnf(l17,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l18,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l51,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l29,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l21,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(21,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(cnf,[status(esa)],[clause_44]) ).
cnf(l3,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l164,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l260,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(10,plain,
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X0)) ),
inference(cnf,[status(esa)],[clause_96]) ).
cnf(l4,plain,
( ~ '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(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l35,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l59,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l187,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l122,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l97,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l19,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l198,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l66,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l240,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l192,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l262,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l273,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l73,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l229,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l266,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l98,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l250,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(13,plain,
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
inference(cnf,[status(esa)],[clause_3]) ).
cnf(l261,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l318,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l185,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l307,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l272,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l294,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l265,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l20,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l228,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l224,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l333,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l302,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l226,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l285,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l300,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l13,plain,
( ~ '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(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l311,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l355,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l186,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l72,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l105,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l243,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l65,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l263,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l335,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l117,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l288,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5,plain,
( ~ '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(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l28,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l280,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l112,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l36,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l356,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l277,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l85,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l167,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l301,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l374,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l303,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l136,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l107,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l159,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l71,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l77,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l425,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l386,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l418,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l400,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l426,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l304,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l276,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l364,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l391,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l331,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l427,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l382,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l369,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l278,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l113,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l363,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l131,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l284,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l41,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l306,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l222,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l324,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l367,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l275,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l428,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l357,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l379,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l423,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l40,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l404,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l456,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l481,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l286,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l358,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l241,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l282,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l362,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l422,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l135,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l435,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l430,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l138,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l361,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l52,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l293,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l60,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l348,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l314,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l454,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l319,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l279,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l381,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l453,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l368,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l380,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l64,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l408,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l248,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l281,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l421,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l111,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l397,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l365,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6,plain,
( ~ '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(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l405,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l387,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l330,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l94,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l424,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l63,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l431,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l441,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l494,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l123,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l336,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l149,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l58,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l480,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l419,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l289,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l398,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l132,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l401,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l30,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l194,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l154,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l473,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l148,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l26,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l406,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l527,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l420,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l523,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l332,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l516,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l385,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l31,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l517,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l442,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l70,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l522,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l37,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l482,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l475,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l443,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l371,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l251,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l528,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l377,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l116,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l478,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l498,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l296,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l399,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l171,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l495,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l496,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l520,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l532,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l515,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l43,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l487,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l518,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l485,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l433,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l519,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l366,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l119,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l484,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l429,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l96,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l444,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l432,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l99,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l499,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l534,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l486,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l257,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l256,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l434,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l530,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l533,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l526,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l507,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l524,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l514,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l474,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| 'E'('0',f(suc(z)))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l512,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l476,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l529,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l102,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0') ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l535,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l521,plain,
'LE'(f(suc(z)),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l477,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l525,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l483,plain,
'LE'(f(suc(suc(z))),s('0')),
inference(instantiation,[status(thm)],[5]) ).
cnf(l497,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(l531,plain,
~ 'LE'(f(z),'0'),
inference(instantiation,[status(thm)],[15]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l7,l2,l25,l17,l18,l51,l29,l21,l3,l164,l260,l4,l35,l59,l187,l122,l97,l19,l198,l66,l240,l192,l262,l273,l73,l229,l266,l98,l250,l261,l318,l185,l307,l272,l294,l265,l20,l228,l224,l333,l302,l226,l285,l300,l13,l311,l355,l186,l72,l105,l243,l65,l263,l335,l117,l288,l5,l28,l280,l112,l36,l356,l277,l85,l167,l301,l374,l303,l136,l107,l159,l71,l77,l425,l386,l418,l400,l426,l304,l276,l364,l391,l331,l427,l382,l369,l278,l113,l363,l131,l284,l41,l306,l222,l324,l367,l275,l428,l357,l379,l423,l40,l404,l456,l481,l286,l358,l241,l282,l362,l422,l135,l435,l430,l138,l361,l52,l293,l60,l348,l314,l454,l319,l279,l381,l453,l368,l380,l64,l408,l248,l281,l421,l111,l397,l365,l6,l405,l387,l330,l94,l424,l63,l431,l441,l494,l123,l336,l149,l58,l480,l419,l289,l398,l132,l401,l30,l194,l154,l473,l148,l26,l406,l527,l420,l523,l332,l516,l385,l31,l517,l442,l70,l522,l37,l482,l475,l443,l371,l251,l528,l377,l116,l478,l498,l296,l399,l171,l495,l496,l520,l532,l515,l43,l487,l518,l485,l433,l519,l366,l119,l484,l429,l96,l444,l432,l99,l499,l534,l486,l257,l256,l434,l530,l533,l526,l507,l524,l514,l474,l512,l476,l529,l102,l535,l521,l477,l525,l483,l497,l531]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYO652-1 : TPTP v9.0.0. Released v7.3.0.
% 0.06/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.33 % Computer : n028.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jul 22 20:07:34 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.11/0.34 % launching worker at depth: 1
% 0.11/0.34 % launching worker at depth: 2
% 0.11/0.34 % launching worker at depth: 9
% 0.11/0.34 % launching worker at depth: 3
% 0.11/0.34 % launching worker at depth: 4
% 0.11/0.34 % launching worker at depth: 5
% 0.11/0.34 % launching worker at depth: 6
% 0.11/0.34 % launching worker at depth: 7
% 0.11/0.34 % launching worker at depth: 8
% 0.11/0.35 % launching worker at depth: 10
% 0.11/0.38 % launching worker at depth: 11
% 0.18/0.48 % launching worker at depth: 12
% 1.27/0.52 % SZS status Theorem for theBenchmark
% 1.27/0.52 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------