%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO677-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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 : Thu May 9 17:51:08 EDT 2024
% Result : Unsatisfiable 48.45s 48.61s
% Output : Refutation 48.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 30
% Syntax : Number of clauses : 109 ( 12 unt; 61 nHn; 84 RR)
% Number of literals : 368 ( 0 equ; 205 neg)
% Maximal clause size : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 99 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_77,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_77) ).
cnf(clause_145,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_145) ).
cnf(clause_15,axiom,
( ~ 'LE'(f(X5),s(s('0')))
| 'E'(s('0'),f(X5))
| 'LE'(f(X5),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
cnf(clause_73,axiom,
( ~ 'LE'(f(X11),s(s(s('0'))))
| 'E'(s(s('0')),f(X11))
| 'LE'(f(X11),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_73) ).
cnf(clause_113,axiom,
'LE'(f(X2),s(s(s(s('0'))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_113) ).
cnf(clause_61,axiom,
( ~ 'LE'(f(X17),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(X17))
| 'LE'(f(X17),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_61) ).
cnf(c3,plain,
( 'E'(s(s(s('0'))),f(X18))
| 'LE'(f(X18),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_61,clause_113]) ).
cnf(clause_13,axiom,
( ~ 'LE'(f(suc(X31)),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(X31)))
| 'LE'(f(X31),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13) ).
cnf(c52,plain,
( 'E'(s(s(s('0'))),f(suc(X32)))
| 'LE'(f(X32),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_13,clause_113]) ).
cnf(clause_65,axiom,
( ~ 'E'(s(s(s('0'))),f(X43))
| ~ 'E'(s(s(s('0'))),f(suc(X43)))
| 'E'(f(X43),f(suc(X43)))
| iLEQ(suc(X43),suc(X43)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_65) ).
cnf(c115,plain,
( ~ 'E'(s(s(s('0'))),f(X44))
| 'E'(f(X44),f(suc(X44)))
| iLEQ(suc(X44),suc(X44))
| 'LE'(f(X44),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_65,c52]) ).
cnf(c120,plain,
( 'E'(f(X45),f(suc(X45)))
| iLEQ(suc(X45),suc(X45))
| 'LE'(f(X45),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c115,c3]) ).
cnf(clause_51,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X55)))
| ~ iLEQ(suc(X54),suc(X55))
| ~ 'E'(s(s(s('0'))),f(X55))
| ~ 'E'(s(s(s('0'))),f(X54))
| ~ 'E'(s(s(s('0'))),f(suc(X54)))
| 'E'(f(X54),f(suc(X54)))
| 'E'(f(X55),f(suc(X55))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_51) ).
cnf(c199,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X56)))
| ~ iLEQ(suc(X56),suc(X56))
| ~ 'E'(s(s(s('0'))),f(X56))
| 'E'(f(X56),f(suc(X56))) ),
inference(factor,[status(thm)],[clause_51]) ).
cnf(c229,plain,
( ~ iLEQ(suc(X57),suc(X57))
| ~ 'E'(s(s(s('0'))),f(X57))
| 'E'(f(X57),f(suc(X57)))
| 'LE'(f(X57),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c199,c52]) ).
cnf(c236,plain,
( ~ iLEQ(suc(X58),suc(X58))
| 'E'(f(X58),f(suc(X58)))
| 'LE'(f(X58),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c229,c3]) ).
cnf(c251,plain,
( 'E'(f(X59),f(suc(X59)))
| 'LE'(f(X59),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c236,c120]) ).
cnf(clause_143,axiom,
( ~ 'LE'(f(suc(suc(X20))),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(suc(X20))))
| 'LE'(f(X20),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_143) ).
cnf(c10,plain,
( 'E'(s(s(s('0'))),f(suc(suc(X21))))
| 'LE'(f(X21),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_143,clause_113]) ).
cnf(clause_140,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(suc(X92))))
| ~ 'E'(s(s(s('0'))),f(suc(X92)))
| ~ 'E'(f(X92),f(suc(X92)))
| ~ 'E'(s(s(s('0'))),f(X92))
| iLEQ(suc(X92),suc(X92)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_140) ).
cnf(c559,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X371)))
| ~ 'E'(f(X371),f(suc(X371)))
| ~ 'E'(s(s(s('0'))),f(X371))
| iLEQ(suc(X371),suc(X371))
| 'LE'(f(X371),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_140,c10]) ).
cnf(c8611,plain,
( ~ 'E'(f(X372),f(suc(X372)))
| ~ 'E'(s(s(s('0'))),f(X372))
| iLEQ(suc(X372),suc(X372))
| 'LE'(f(X372),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c559,c52]) ).
cnf(c8692,plain,
( ~ 'E'(f(X373),f(suc(X373)))
| iLEQ(suc(X373),suc(X373))
| 'LE'(f(X373),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c8611,c3]) ).
cnf(c8746,plain,
( iLEQ(suc(X375),suc(X375))
| 'LE'(f(X375),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c8692,c251]) ).
cnf(clause_121,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(X109)))
| ~ 'E'(f(X109),f(suc(X109)))
| ~ iLEQ(suc(X108),suc(X109))
| ~ 'E'(s(s(s('0'))),f(X109))
| ~ 'E'(s(s(s('0'))),f(X108))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X108))))
| ~ 'E'(f(X108),f(suc(X108)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X109))))
| ~ 'E'(s(s(s('0'))),f(suc(X108))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_121) ).
cnf(c857,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X962)))
| ~ 'E'(f(X962),f(suc(X962)))
| ~ iLEQ(suc(X962),suc(X962))
| ~ 'E'(s(s(s('0'))),f(X962))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X962)))) ),
inference(factor,[status(thm)],[clause_121]) ).
cnf(c30925,plain,
( ~ 'E'(s(s(s('0'))),f(suc(X963)))
| ~ 'E'(f(X963),f(suc(X963)))
| ~ iLEQ(suc(X963),suc(X963))
| ~ 'E'(s(s(s('0'))),f(X963))
| 'LE'(f(X963),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c857,c10]) ).
cnf(c31122,plain,
( ~ 'E'(f(X964),f(suc(X964)))
| ~ iLEQ(suc(X964),suc(X964))
| ~ 'E'(s(s(s('0'))),f(X964))
| 'LE'(f(X964),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c30925,c52]) ).
cnf(c31249,plain,
( ~ 'E'(f(X965),f(suc(X965)))
| ~ iLEQ(suc(X965),suc(X965))
| 'LE'(f(X965),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c31122,c3]) ).
cnf(c31342,plain,
( ~ iLEQ(suc(X966),suc(X966))
| 'LE'(f(X966),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c31249,c251]) ).
cnf(c31503,plain,
'LE'(f(X967),s(s(s('0')))),
inference(resolution,[status(thm)],[c31342,c8746]) ).
cnf(c31567,plain,
( 'E'(s(s('0')),f(X968))
| 'LE'(f(X968),s(s('0'))) ),
inference(resolution,[status(thm)],[c31503,clause_73]) ).
cnf(clause_38,axiom,
( ~ 'E'(s(s('0')),f(X41))
| ~ 'E'(s(s('0')),f(suc(X40)))
| ~ iLEQ(suc(X40),suc(X41))
| ~ 'E'(s(s('0')),f(suc(X41)))
| ~ 'E'(s(s('0')),f(X40))
| 'E'(f(X40),f(suc(X40)))
| 'E'(f(X41),f(suc(X41))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_38) ).
cnf(c84,plain,
( ~ 'E'(s(s('0')),f(X42))
| ~ 'E'(s(s('0')),f(suc(X42)))
| ~ iLEQ(suc(X42),suc(X42))
| 'E'(f(X42),f(suc(X42))) ),
inference(factor,[status(thm)],[clause_38]) ).
cnf(clause_87,axiom,
( ~ 'LE'(f(suc(X16)),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(X16)))
| 'LE'(f(X16),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_87) ).
cnf(c31568,plain,
( 'E'(s(s('0')),f(suc(X969)))
| 'LE'(f(X969),s(s('0'))) ),
inference(resolution,[status(thm)],[c31503,clause_87]) ).
cnf(c31644,plain,
( 'LE'(f(X991),s(s('0')))
| ~ 'E'(s(s('0')),f(X991))
| ~ iLEQ(suc(X991),suc(X991))
| 'E'(f(X991),f(suc(X991))) ),
inference(resolution,[status(thm)],[c31568,c84]) ).
cnf(c32975,plain,
( 'LE'(f(X993),s(s('0')))
| ~ iLEQ(suc(X993),suc(X993))
| 'E'(f(X993),f(suc(X993))) ),
inference(resolution,[status(thm)],[c31644,c31567]) ).
cnf(clause_84,axiom,
( ~ 'E'(s(s('0')),f(X24))
| ~ 'E'(s(s('0')),f(suc(X24)))
| 'E'(f(X24),f(suc(X24)))
| iLEQ(suc(X24),suc(X24)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_84) ).
cnf(c31660,plain,
( 'LE'(f(X994),s(s('0')))
| ~ 'E'(s(s('0')),f(X994))
| 'E'(f(X994),f(suc(X994)))
| iLEQ(suc(X994),suc(X994)) ),
inference(resolution,[status(thm)],[c31568,clause_84]) ).
cnf(c33100,plain,
( 'LE'(f(X995),s(s('0')))
| 'E'(f(X995),f(suc(X995)))
| iLEQ(suc(X995),suc(X995)) ),
inference(resolution,[status(thm)],[c31660,c31567]) ).
cnf(c33139,plain,
( 'LE'(f(X996),s(s('0')))
| 'E'(f(X996),f(suc(X996))) ),
inference(resolution,[status(thm)],[c33100,c32975]) ).
cnf(clause_24,axiom,
( ~ 'E'(s(s('0')),f(X7))
| ~ 'E'(s(s('0')),f(suc(X6)))
| ~ 'E'(f(X7),f(suc(X7)))
| ~ iLEQ(suc(X6),suc(X7))
| ~ 'E'(s(s('0')),f(suc(X7)))
| ~ 'E'(s(s('0')),f(suc(suc(X6))))
| ~ 'E'(s(s('0')),f(X6))
| ~ 'E'(f(X6),f(suc(X6)))
| ~ 'E'(s(s('0')),f(suc(suc(X7)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_24) ).
cnf(c1,plain,
( ~ 'E'(s(s('0')),f(X133))
| ~ 'E'(s(s('0')),f(suc(X133)))
| ~ 'E'(f(X133),f(suc(X133)))
| ~ iLEQ(suc(X133),suc(X133))
| ~ 'E'(s(s('0')),f(suc(suc(X133)))) ),
inference(factor,[status(thm)],[clause_24]) ).
cnf(clause_18,axiom,
( ~ 'LE'(f(suc(suc(X28))),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(suc(X28))))
| 'LE'(f(X28),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
cnf(c31569,plain,
( 'E'(s(s('0')),f(suc(suc(X970))))
| 'LE'(f(X970),s(s('0'))) ),
inference(resolution,[status(thm)],[c31503,clause_18]) ).
cnf(c31732,plain,
( 'LE'(f(X1306),s(s('0')))
| ~ 'E'(s(s('0')),f(X1306))
| ~ 'E'(s(s('0')),f(suc(X1306)))
| ~ 'E'(f(X1306),f(suc(X1306)))
| ~ iLEQ(suc(X1306),suc(X1306)) ),
inference(resolution,[status(thm)],[c31569,c1]) ).
cnf(c40410,plain,
( 'LE'(f(X1308),s(s('0')))
| ~ 'E'(s(s('0')),f(X1308))
| ~ 'E'(f(X1308),f(suc(X1308)))
| ~ iLEQ(suc(X1308),suc(X1308)) ),
inference(resolution,[status(thm)],[c31732,c31568]) ).
cnf(c40523,plain,
( 'LE'(f(X1309),s(s('0')))
| ~ 'E'(s(s('0')),f(X1309))
| ~ iLEQ(suc(X1309),suc(X1309)) ),
inference(resolution,[status(thm)],[c40410,c33139]) ).
cnf(c40576,plain,
( 'LE'(f(X1310),s(s('0')))
| ~ iLEQ(suc(X1310),suc(X1310)) ),
inference(resolution,[status(thm)],[c40523,c31567]) ).
cnf(clause_97,axiom,
( ~ 'E'(s(s('0')),f(suc(suc(X67))))
| ~ 'E'(s(s('0')),f(suc(X67)))
| ~ 'E'(f(X67),f(suc(X67)))
| ~ 'E'(s(s('0')),f(X67))
| iLEQ(suc(X67),suc(X67)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_97) ).
cnf(c31738,plain,
( 'LE'(f(X1333),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1333)))
| ~ 'E'(f(X1333),f(suc(X1333)))
| ~ 'E'(s(s('0')),f(X1333))
| iLEQ(suc(X1333),suc(X1333)) ),
inference(resolution,[status(thm)],[c31569,clause_97]) ).
cnf(c40997,plain,
( 'LE'(f(X1334),s(s('0')))
| ~ 'E'(f(X1334),f(suc(X1334)))
| ~ 'E'(s(s('0')),f(X1334))
| iLEQ(suc(X1334),suc(X1334)) ),
inference(resolution,[status(thm)],[c31738,c31568]) ).
cnf(c41046,plain,
( 'LE'(f(X1335),s(s('0')))
| ~ 'E'(f(X1335),f(suc(X1335)))
| iLEQ(suc(X1335),suc(X1335)) ),
inference(resolution,[status(thm)],[c40997,c31567]) ).
cnf(c41111,plain,
( 'LE'(f(X1337),s(s('0')))
| iLEQ(suc(X1337),suc(X1337)) ),
inference(resolution,[status(thm)],[c41046,c33139]) ).
cnf(c41188,plain,
'LE'(f(X1338),s(s('0'))),
inference(resolution,[status(thm)],[c41111,c40576]) ).
cnf(c41192,plain,
( 'E'(s('0'),f(X1339))
| 'LE'(f(X1339),s('0')) ),
inference(resolution,[status(thm)],[c41188,clause_15]) ).
cnf(clause_39,axiom,
( ~ 'LE'(f(suc(X9)),s(s('0')))
| 'E'(s('0'),f(suc(X9)))
| 'LE'(f(X9),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_39) ).
cnf(c41191,plain,
( 'E'(s('0'),f(suc(X1340)))
| 'LE'(f(X1340),s('0')) ),
inference(resolution,[status(thm)],[c41188,clause_39]) ).
cnf(clause_112,axiom,
( ~ 'E'(s('0'),f(suc(X121)))
| ~ 'E'(s('0'),f(suc(X120)))
| ~ 'E'(s('0'),f(X121))
| ~ 'E'(s('0'),f(X120))
| ~ iLEQ(suc(X120),suc(X121))
| 'E'(f(X120),f(suc(X120)))
| 'E'(f(X121),f(suc(X121))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_112) ).
cnf(c1071,plain,
( ~ 'E'(s('0'),f(suc(X122)))
| ~ 'E'(s('0'),f(X122))
| ~ iLEQ(suc(X122),suc(X122))
| 'E'(f(X122),f(suc(X122))) ),
inference(factor,[status(thm)],[clause_112]) ).
cnf(c41217,plain,
( 'LE'(f(X1359),s('0'))
| ~ 'E'(s('0'),f(X1359))
| ~ iLEQ(suc(X1359),suc(X1359))
| 'E'(f(X1359),f(suc(X1359))) ),
inference(resolution,[status(thm)],[c41191,c1071]) ).
cnf(clause_115,axiom,
( ~ 'E'(s('0'),f(X15))
| ~ 'E'(s('0'),f(suc(X15)))
| 'E'(f(X15),f(suc(X15)))
| iLEQ(suc(X15),suc(X15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_115) ).
cnf(c41219,plain,
( 'LE'(f(X1360),s('0'))
| ~ 'E'(s('0'),f(X1360))
| 'E'(f(X1360),f(suc(X1360)))
| iLEQ(suc(X1360),suc(X1360)) ),
inference(resolution,[status(thm)],[c41191,clause_115]) ).
cnf(c41623,plain,
( 'LE'(f(X1361),s('0'))
| 'E'(f(X1361),f(suc(X1361)))
| iLEQ(suc(X1361),suc(X1361)) ),
inference(resolution,[status(thm)],[c41219,c41192]) ).
cnf(c41668,plain,
( 'LE'(f(X1362),s('0'))
| 'E'(f(X1362),f(suc(X1362)))
| ~ 'E'(s('0'),f(X1362)) ),
inference(resolution,[status(thm)],[c41623,c41217]) ).
cnf(c41671,plain,
( 'LE'(f(X1364),s('0'))
| 'E'(f(X1364),f(suc(X1364))) ),
inference(resolution,[status(thm)],[c41668,c41192]) ).
cnf(clause_31,axiom,
( ~ 'E'(s('0'),f(suc(suc(X94))))
| ~ 'E'(s('0'),f(suc(X94)))
| ~ 'E'(f(X94),f(suc(X94)))
| ~ 'E'(s('0'),f(X94))
| iLEQ(suc(X94),suc(X94)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_31) ).
cnf(clause_49,axiom,
( ~ 'LE'(f(suc(suc(X12))),s(s('0')))
| 'E'(s('0'),f(suc(suc(X12))))
| 'LE'(f(X12),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_49) ).
cnf(c41190,plain,
( 'E'(s('0'),f(suc(suc(X1341))))
| 'LE'(f(X1341),s('0')) ),
inference(resolution,[status(thm)],[c41188,clause_49]) ).
cnf(c41241,plain,
( 'LE'(f(X1551),s('0'))
| ~ 'E'(s('0'),f(suc(X1551)))
| ~ 'E'(f(X1551),f(suc(X1551)))
| ~ 'E'(s('0'),f(X1551))
| iLEQ(suc(X1551),suc(X1551)) ),
inference(resolution,[status(thm)],[c41190,clause_31]) ).
cnf(c43185,plain,
( 'LE'(f(X1554),s('0'))
| ~ 'E'(s('0'),f(suc(X1554)))
| ~ 'E'(s('0'),f(X1554))
| iLEQ(suc(X1554),suc(X1554)) ),
inference(resolution,[status(thm)],[c41241,c41671]) ).
cnf(c43206,plain,
( 'LE'(f(X1555),s('0'))
| ~ 'E'(s('0'),f(X1555))
| iLEQ(suc(X1555),suc(X1555)) ),
inference(resolution,[status(thm)],[c43185,c41191]) ).
cnf(c43212,plain,
( 'LE'(f(X1556),s('0'))
| iLEQ(suc(X1556),suc(X1556)) ),
inference(resolution,[status(thm)],[c43206,c41192]) ).
cnf(clause_57,axiom,
( ~ 'E'(s('0'),f(suc(X103)))
| ~ 'E'(s('0'),f(suc(suc(X103))))
| ~ 'E'(s('0'),f(suc(X102)))
| ~ 'E'(s('0'),f(X103))
| ~ 'E'(f(X103),f(suc(X103)))
| ~ 'E'(f(X102),f(suc(X102)))
| ~ 'E'(s('0'),f(X102))
| ~ 'E'(s('0'),f(suc(suc(X102))))
| ~ iLEQ(suc(X102),suc(X103)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_57) ).
cnf(c761,plain,
( ~ 'E'(s('0'),f(suc(X104)))
| ~ 'E'(s('0'),f(suc(suc(X104))))
| ~ 'E'(s('0'),f(X104))
| ~ 'E'(f(X104),f(suc(X104)))
| ~ iLEQ(suc(X104),suc(X104)) ),
inference(factor,[status(thm)],[clause_57]) ).
cnf(c41247,plain,
( 'LE'(f(X1635),s('0'))
| ~ 'E'(s('0'),f(suc(X1635)))
| ~ 'E'(s('0'),f(X1635))
| ~ 'E'(f(X1635),f(suc(X1635)))
| ~ iLEQ(suc(X1635),suc(X1635)) ),
inference(resolution,[status(thm)],[c41190,c761]) ).
cnf(c43739,plain,
( 'LE'(f(X1636),s('0'))
| ~ 'E'(s('0'),f(suc(X1636)))
| ~ 'E'(s('0'),f(X1636))
| ~ iLEQ(suc(X1636),suc(X1636)) ),
inference(resolution,[status(thm)],[c41247,c41671]) ).
cnf(c43760,plain,
( 'LE'(f(X1637),s('0'))
| ~ 'E'(s('0'),f(X1637))
| ~ iLEQ(suc(X1637),suc(X1637)) ),
inference(resolution,[status(thm)],[c43739,c41191]) ).
cnf(c43768,plain,
( 'LE'(f(X1638),s('0'))
| ~ 'E'(s('0'),f(X1638)) ),
inference(resolution,[status(thm)],[c43760,c43212]) ).
cnf(c43776,plain,
'LE'(f(X1641),s('0')),
inference(resolution,[status(thm)],[c43768,c41192]) ).
cnf(c43801,plain,
( 'E'('0',f(X1642))
| 'LE'(f(X1642),'0') ),
inference(resolution,[status(thm)],[c43776,clause_145]) ).
cnf(c43810,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c43801,clause_77]) ).
cnf(clause_2,axiom,
( ~ 'LE'(f(suc(X4)),s('0'))
| 'E'('0',f(suc(X4)))
| 'LE'(f(X4),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2) ).
cnf(c43803,plain,
( 'E'('0',f(suc(X1643)))
| 'LE'(f(X1643),'0') ),
inference(resolution,[status(thm)],[c43776,clause_2]) ).
cnf(c43819,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c43803,clause_77]) ).
cnf(clause_0,axiom,
( ~ 'E'('0',f(suc(X73)))
| ~ iLEQ(suc(X72),suc(X73))
| ~ 'E'('0',f(X73))
| ~ 'E'('0',f(suc(X72)))
| ~ 'E'('0',f(X72))
| 'E'(f(X72),f(suc(X72)))
| 'E'(f(X73),f(suc(X73))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_0) ).
cnf(c366,plain,
( ~ 'E'('0',f(suc(X74)))
| ~ iLEQ(suc(X74),suc(X74))
| ~ 'E'('0',f(X74))
| 'E'(f(X74),f(suc(X74))) ),
inference(factor,[status(thm)],[clause_0]) ).
cnf(clause_150,axiom,
( ~ 'E'('0',f(X10))
| ~ 'E'('0',f(suc(X10)))
| 'E'(f(X10),f(suc(X10)))
| iLEQ(suc(X10),suc(X10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_150) ).
cnf(c43822,plain,
( ~ 'E'('0',f(z))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c43819,clause_150]) ).
cnf(c43838,plain,
( 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c43822,c43810]) ).
cnf(c43850,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43838,c366]) ).
cnf(c43853,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43850,c43819]) ).
cnf(c43855,plain,
'E'(f(z),f(suc(z))),
inference(resolution,[status(thm)],[c43853,c43810]) ).
cnf(clause_48,axiom,
( ~ 'E'(f(X79),f(suc(X79)))
| ~ 'E'('0',f(suc(X80)))
| ~ iLEQ(suc(X79),suc(X80))
| ~ 'E'('0',f(suc(suc(X80))))
| ~ 'E'('0',f(suc(suc(X79))))
| ~ 'E'('0',f(X80))
| ~ 'E'('0',f(suc(X79)))
| ~ 'E'(f(X80),f(suc(X80)))
| ~ 'E'('0',f(X79)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_48) ).
cnf(c414,plain,
( ~ 'E'(f(X81),f(suc(X81)))
| ~ 'E'('0',f(suc(X81)))
| ~ iLEQ(suc(X81),suc(X81))
| ~ 'E'('0',f(suc(suc(X81))))
| ~ 'E'('0',f(X81)) ),
inference(factor,[status(thm)],[clause_48]) ).
cnf(clause_27,axiom,
( ~ 'LE'(f(suc(suc(X8))),s('0'))
| 'E'('0',f(suc(suc(X8))))
| 'LE'(f(X8),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_27) ).
cnf(c43802,plain,
( 'E'('0',f(suc(suc(X1645))))
| 'LE'(f(X1645),'0') ),
inference(resolution,[status(thm)],[c43776,clause_27]) ).
cnf(c43830,plain,
'E'('0',f(suc(suc(z)))),
inference(resolution,[status(thm)],[c43802,clause_77]) ).
cnf(c43835,plain,
( ~ 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43830,c414]) ).
cnf(c43931,plain,
( ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43835,c43855]) ).
cnf(clause_114,axiom,
( ~ 'E'('0',f(suc(suc(X38))))
| ~ 'E'('0',f(suc(X38)))
| ~ 'E'(f(X38),f(suc(X38)))
| ~ 'E'('0',f(X38))
| iLEQ(suc(X38),suc(X38)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_114) ).
cnf(c43844,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43838,clause_114]) ).
cnf(c43933,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43844,c43830]) ).
cnf(c43938,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43933,c43819]) ).
cnf(c43940,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c43938,c43810]) ).
cnf(c43942,plain,
( ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c43940,c43931]) ).
cnf(c43946,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c43942,c43819]) ).
cnf(c43948,plain,
$false,
inference(resolution,[status(thm)],[c43946,c43810]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYO677-1 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n017.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 17:52:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 48.45/48.61 % Version: 1.5
% 48.45/48.61 % SZS status Unsatisfiable
% 48.45/48.61 % SZS output start CNFRefutation
% See solution above
% 48.45/48.61
% 48.45/48.61 % Initial clauses : 38
% 48.45/48.61 % Processed clauses : 913
% 48.45/48.61 % Factors computed : 114
% 48.45/48.61 % Resolvents computed: 43835
% 48.45/48.61 % Tautologies deleted: 22
% 48.45/48.61 % Forward subsumed : 1130
% 48.45/48.61 % Backward subsumed : 848
% 48.45/48.61 % -------- CPU Time ---------
% 48.45/48.61 % User time : 48.037 s
% 48.45/48.61 % System time : 0.223 s
% 48.45/48.61 % Total time : 48.260 s
%------------------------------------------------------------------------------