%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO658-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:05 EDT 2024
% Result : Unsatisfiable 258.93s 259.12s
% Output : Refutation 258.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 22
% Syntax : Number of clauses : 134 ( 5 unt; 106 nHn; 97 RR)
% Number of literals : 589 ( 0 equ; 306 neg)
% Maximal clause size : 13 ( 4 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 : 138 ( 3 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_87,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_87) ).
cnf(clause_109,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_109) ).
cnf(clause_72,axiom,
'LE'(f(X2),s(s('0'))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_72) ).
cnf(clause_51,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_51) ).
cnf(c0,plain,
( 'E'(s('0'),f(X8))
| 'LE'(f(X8),s('0')) ),
inference(resolution,[status(thm)],[clause_51,clause_72]) ).
cnf(clause_104,axiom,
( ~ 'LE'(f(suc(X16)),s(s('0')))
| 'E'(s('0'),f(suc(X16)))
| 'LE'(f(X16),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_104) ).
cnf(c13,plain,
( 'E'(s('0'),f(suc(X17)))
| 'LE'(f(X17),s('0')) ),
inference(resolution,[status(thm)],[clause_104,clause_72]) ).
cnf(clause_81,axiom,
( ~ 'E'(s('0'),f(X20))
| ~ 'E'(s('0'),f(suc(X20)))
| 'E'(f(X20),f(suc(X20)))
| iLEQ(suc(X20),suc(X20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_81) ).
cnf(c26,plain,
( ~ 'E'(s('0'),f(X28))
| 'E'(f(X28),f(suc(X28)))
| iLEQ(suc(X28),suc(X28))
| 'LE'(f(X28),s('0')) ),
inference(resolution,[status(thm)],[clause_81,c13]) ).
cnf(c96,plain,
( 'E'(f(X31),f(suc(X31)))
| iLEQ(suc(X31),suc(X31))
| 'LE'(f(X31),s('0')) ),
inference(resolution,[status(thm)],[c26,c0]) ).
cnf(clause_142,axiom,
( ~ iLEQ(suc(X44),suc(X43))
| ~ 'E'(s('0'),f(X44))
| ~ 'E'(s('0'),f(suc(X44)))
| ~ 'E'(s('0'),f(suc(X43)))
| ~ 'E'(s('0'),f(X43))
| 'E'(f(X44),f(suc(X44)))
| 'E'(f(X43),f(suc(X43))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_142) ).
cnf(c181,plain,
( ~ iLEQ(suc(X46),suc(X46))
| ~ 'E'(s('0'),f(X46))
| ~ 'E'(s('0'),f(suc(X46)))
| 'E'(f(X46),f(suc(X46))) ),
inference(factor,[status(thm)],[clause_142]) ).
cnf(c265,plain,
( ~ iLEQ(suc(X47),suc(X47))
| ~ 'E'(s('0'),f(X47))
| 'E'(f(X47),f(suc(X47)))
| 'LE'(f(X47),s('0')) ),
inference(resolution,[status(thm)],[c181,c13]) ).
cnf(c302,plain,
( ~ iLEQ(suc(X48),suc(X48))
| 'E'(f(X48),f(suc(X48)))
| 'LE'(f(X48),s('0')) ),
inference(resolution,[status(thm)],[c265,c0]) ).
cnf(c309,plain,
( 'E'(f(X49),f(suc(X49)))
| 'LE'(f(X49),s('0')) ),
inference(resolution,[status(thm)],[c302,c96]) ).
cnf(clause_129,axiom,
( ~ 'LE'(f(suc(suc(X33))),s(s('0')))
| 'E'(s('0'),f(suc(suc(X33))))
| 'LE'(f(X33),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_129) ).
cnf(c123,plain,
( 'E'(s('0'),f(suc(suc(X34))))
| 'LE'(f(X34),s('0')) ),
inference(resolution,[status(thm)],[clause_129,clause_72]) ).
cnf(clause_16,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))
| 'E'(f(X94),f(suc(suc(X94))))
| iLEQ(suc(X94),suc(X94)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
cnf(c851,plain,
( ~ 'E'(s('0'),f(suc(X829)))
| ~ 'E'(f(X829),f(suc(X829)))
| ~ 'E'(s('0'),f(X829))
| 'E'(f(X829),f(suc(suc(X829))))
| iLEQ(suc(X829),suc(X829))
| 'LE'(f(X829),s('0')) ),
inference(resolution,[status(thm)],[clause_16,c123]) ).
cnf(c7391,plain,
( ~ 'E'(s('0'),f(suc(X830)))
| ~ 'E'(s('0'),f(X830))
| 'E'(f(X830),f(suc(suc(X830))))
| iLEQ(suc(X830),suc(X830))
| 'LE'(f(X830),s('0')) ),
inference(resolution,[status(thm)],[c851,c309]) ).
cnf(c7454,plain,
( ~ 'E'(s('0'),f(X832))
| 'E'(f(X832),f(suc(suc(X832))))
| iLEQ(suc(X832),suc(X832))
| 'LE'(f(X832),s('0')) ),
inference(resolution,[status(thm)],[c7391,c13]) ).
cnf(c7495,plain,
( 'E'(f(X833),f(suc(suc(X833))))
| iLEQ(suc(X833),suc(X833))
| 'LE'(f(X833),s('0')) ),
inference(resolution,[status(thm)],[c7454,c0]) ).
cnf(clause_41,axiom,
( ~ iLEQ(suc(X65),suc(X64))
| ~ 'E'(s('0'),f(suc(suc(X65))))
| ~ 'E'(s('0'),f(X65))
| ~ 'E'(s('0'),f(suc(suc(X64))))
| ~ 'E'(s('0'),f(suc(X65)))
| ~ 'E'(s('0'),f(suc(X64)))
| ~ 'E'(s('0'),f(X64))
| ~ 'E'(f(X64),f(suc(X64)))
| ~ 'E'(f(X65),f(suc(X65)))
| 'E'(f(X65),f(suc(suc(X65))))
| 'E'(f(X64),f(suc(suc(X64)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_41) ).
cnf(c458,plain,
( ~ iLEQ(suc(X1229),suc(X1229))
| ~ 'E'(s('0'),f(suc(suc(X1229))))
| ~ 'E'(s('0'),f(X1229))
| ~ 'E'(s('0'),f(suc(X1229)))
| ~ 'E'(f(X1229),f(suc(X1229)))
| 'E'(f(X1229),f(suc(suc(X1229)))) ),
inference(factor,[status(thm)],[clause_41]) ).
cnf(c11549,plain,
( ~ iLEQ(suc(X1238),suc(X1238))
| ~ 'E'(s('0'),f(X1238))
| ~ 'E'(s('0'),f(suc(X1238)))
| ~ 'E'(f(X1238),f(suc(X1238)))
| 'E'(f(X1238),f(suc(suc(X1238))))
| 'LE'(f(X1238),s('0')) ),
inference(resolution,[status(thm)],[c458,c123]) ).
cnf(c12005,plain,
( ~ iLEQ(suc(X1239),suc(X1239))
| ~ 'E'(s('0'),f(X1239))
| ~ 'E'(s('0'),f(suc(X1239)))
| 'E'(f(X1239),f(suc(suc(X1239))))
| 'LE'(f(X1239),s('0')) ),
inference(resolution,[status(thm)],[c11549,c309]) ).
cnf(c12075,plain,
( ~ iLEQ(suc(X1240),suc(X1240))
| ~ 'E'(s('0'),f(X1240))
| 'E'(f(X1240),f(suc(suc(X1240))))
| 'LE'(f(X1240),s('0')) ),
inference(resolution,[status(thm)],[c12005,c13]) ).
cnf(c12118,plain,
( ~ iLEQ(suc(X1243),suc(X1243))
| 'E'(f(X1243),f(suc(suc(X1243))))
| 'LE'(f(X1243),s('0')) ),
inference(resolution,[status(thm)],[c12075,c0]) ).
cnf(c12250,plain,
( 'E'(f(X1244),f(suc(suc(X1244))))
| 'LE'(f(X1244),s('0')) ),
inference(resolution,[status(thm)],[c12118,c7495]) ).
cnf(clause_75,axiom,
( ~ 'LE'(f(suc(suc(suc(X11)))),s(s('0')))
| 'E'(s('0'),f(suc(suc(suc(X11)))))
| 'LE'(f(X11),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_75) ).
cnf(c6,plain,
( 'E'(s('0'),f(suc(suc(suc(X12)))))
| 'LE'(f(X12),s('0')) ),
inference(resolution,[status(thm)],[clause_75,clause_72]) ).
cnf(clause_134,axiom,
( ~ 'E'(s('0'),f(suc(suc(X106))))
| ~ 'E'(s('0'),f(X106))
| ~ 'E'(s('0'),f(suc(X106)))
| ~ 'E'(f(X106),f(suc(suc(X106))))
| ~ 'E'(f(X106),f(suc(X106)))
| ~ 'E'(s('0'),f(suc(suc(suc(X106)))))
| iLEQ(suc(X106),suc(X106)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_134) ).
cnf(c1033,plain,
( ~ 'E'(s('0'),f(suc(suc(X2812))))
| ~ 'E'(s('0'),f(X2812))
| ~ 'E'(s('0'),f(suc(X2812)))
| ~ 'E'(f(X2812),f(suc(suc(X2812))))
| ~ 'E'(f(X2812),f(suc(X2812)))
| iLEQ(suc(X2812),suc(X2812))
| 'LE'(f(X2812),s('0')) ),
inference(resolution,[status(thm)],[clause_134,c6]) ).
cnf(c35709,plain,
( ~ 'E'(s('0'),f(suc(suc(X2813))))
| ~ 'E'(s('0'),f(X2813))
| ~ 'E'(s('0'),f(suc(X2813)))
| ~ 'E'(f(X2813),f(suc(X2813)))
| iLEQ(suc(X2813),suc(X2813))
| 'LE'(f(X2813),s('0')) ),
inference(resolution,[status(thm)],[c1033,c12250]) ).
cnf(c35775,plain,
( ~ 'E'(s('0'),f(X2814))
| ~ 'E'(s('0'),f(suc(X2814)))
| ~ 'E'(f(X2814),f(suc(X2814)))
| iLEQ(suc(X2814),suc(X2814))
| 'LE'(f(X2814),s('0')) ),
inference(resolution,[status(thm)],[c35709,c123]) ).
cnf(c35855,plain,
( ~ 'E'(s('0'),f(X2815))
| ~ 'E'(s('0'),f(suc(X2815)))
| iLEQ(suc(X2815),suc(X2815))
| 'LE'(f(X2815),s('0')) ),
inference(resolution,[status(thm)],[c35775,c309]) ).
cnf(c35945,plain,
( ~ 'E'(s('0'),f(X2816))
| iLEQ(suc(X2816),suc(X2816))
| 'LE'(f(X2816),s('0')) ),
inference(resolution,[status(thm)],[c35855,c13]) ).
cnf(c36004,plain,
( iLEQ(suc(X2817),suc(X2817))
| 'LE'(f(X2817),s('0')) ),
inference(resolution,[status(thm)],[c35945,c0]) ).
cnf(c36047,plain,
( iLEQ(suc(X2819),suc(X2819))
| 'E'('0',f(X2819))
| 'LE'(f(X2819),'0') ),
inference(resolution,[status(thm)],[c36004,clause_109]) ).
cnf(c3,plain,
( 'E'(s('0'),f(X9))
| 'E'('0',f(X9))
| 'LE'(f(X9),'0') ),
inference(resolution,[status(thm)],[c0,clause_109]) ).
cnf(c14,plain,
( 'E'(s('0'),f(suc(X18)))
| 'E'('0',f(X18))
| 'LE'(f(X18),'0') ),
inference(resolution,[status(thm)],[c13,clause_109]) ).
cnf(c313,plain,
( 'E'(f(X52),f(suc(X52)))
| 'E'('0',f(X52))
| 'LE'(f(X52),'0') ),
inference(resolution,[status(thm)],[c309,clause_109]) ).
cnf(c127,plain,
( 'E'(s('0'),f(suc(suc(X37))))
| 'E'('0',f(X37))
| 'LE'(f(X37),'0') ),
inference(resolution,[status(thm)],[c123,clause_109]) ).
cnf(c12361,plain,
( 'E'(f(X1245),f(suc(suc(X1245))))
| 'E'('0',f(X1245))
| 'LE'(f(X1245),'0') ),
inference(resolution,[status(thm)],[c12250,clause_109]) ).
cnf(clause_140,axiom,
( ~ iLEQ(suc(X55),suc(X54))
| ~ 'E'(s('0'),f(suc(suc(X55))))
| ~ 'E'(s('0'),f(X55))
| ~ 'E'(s('0'),f(suc(suc(X54))))
| ~ 'E'(s('0'),f(suc(X55)))
| ~ 'E'(s('0'),f(suc(suc(suc(X54)))))
| ~ 'E'(s('0'),f(suc(X54)))
| ~ 'E'(s('0'),f(X54))
| ~ 'E'(f(X55),f(suc(suc(X55))))
| ~ 'E'(f(X54),f(suc(X54)))
| ~ 'E'(f(X55),f(suc(X55)))
| ~ 'E'(s('0'),f(suc(suc(suc(X55)))))
| ~ 'E'(f(X54),f(suc(suc(X54)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_140) ).
cnf(c338,plain,
( ~ iLEQ(suc(X835),suc(X835))
| ~ 'E'(s('0'),f(suc(suc(X835))))
| ~ 'E'(s('0'),f(X835))
| ~ 'E'(s('0'),f(suc(X835)))
| ~ 'E'(s('0'),f(suc(suc(suc(X835)))))
| ~ 'E'(f(X835),f(suc(suc(X835))))
| ~ 'E'(f(X835),f(suc(X835))) ),
inference(factor,[status(thm)],[clause_140]) ).
cnf(c7,plain,
( 'E'(s('0'),f(suc(suc(suc(X13)))))
| 'E'('0',f(X13))
| 'LE'(f(X13),'0') ),
inference(resolution,[status(thm)],[c6,clause_109]) ).
cnf(clause_122,axiom,
( ~ 'LE'(f(suc(X4)),s('0'))
| 'E'('0',f(suc(X4)))
| 'LE'(f(X4),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_122) ).
cnf(c128,plain,
( 'E'(s('0'),f(suc(suc(suc(X38)))))
| 'E'('0',f(suc(X38)))
| 'LE'(f(X38),'0') ),
inference(resolution,[status(thm)],[c123,clause_122]) ).
cnf(clause_141,axiom,
( ~ 'LE'(f(suc(suc(X14))),s('0'))
| 'E'('0',f(suc(suc(X14))))
| 'LE'(f(X14),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_141) ).
cnf(c16,plain,
( 'E'(s('0'),f(suc(suc(suc(X22)))))
| 'E'('0',f(suc(suc(X22))))
| 'LE'(f(X22),'0') ),
inference(resolution,[status(thm)],[c13,clause_141]) ).
cnf(clause_55,axiom,
( ~ 'E'('0',f(suc(X99)))
| ~ 'E'('0',f(X99))
| ~ iLEQ(suc(X99),suc(X100))
| ~ 'E'('0',f(X100))
| ~ 'E'('0',f(suc(X100)))
| 'E'(f(X99),f(suc(X99)))
| 'E'(f(X100),f(suc(X100))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_55) ).
cnf(c914,plain,
( ~ 'E'('0',f(suc(X101)))
| ~ 'E'('0',f(X101))
| ~ iLEQ(suc(X101),suc(X101))
| 'E'(f(X101),f(suc(X101))) ),
inference(factor,[status(thm)],[clause_55]) ).
cnf(clause_93,axiom,
( ~ 'E'('0',f(X25))
| ~ 'E'('0',f(suc(X25)))
| 'E'(f(X25),f(suc(X25)))
| iLEQ(suc(X25),suc(X25)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_93) ).
cnf(c144,plain,
( 'E'(s('0'),f(suc(suc(suc(X229)))))
| 'LE'(f(X229),'0')
| ~ 'E'('0',f(X229))
| 'E'(f(X229),f(suc(X229)))
| iLEQ(suc(X229),suc(X229)) ),
inference(resolution,[status(thm)],[c128,clause_93]) ).
cnf(c2834,plain,
( 'E'(s('0'),f(suc(suc(suc(X230)))))
| 'LE'(f(X230),'0')
| 'E'(f(X230),f(suc(X230)))
| iLEQ(suc(X230),suc(X230)) ),
inference(resolution,[status(thm)],[c144,c7]) ).
cnf(c2912,plain,
( 'E'(s('0'),f(suc(suc(suc(X265)))))
| 'LE'(f(X265),'0')
| 'E'(f(X265),f(suc(X265)))
| ~ 'E'('0',f(suc(X265)))
| ~ 'E'('0',f(X265)) ),
inference(resolution,[status(thm)],[c2834,c914]) ).
cnf(c3296,plain,
( 'E'(s('0'),f(suc(suc(suc(X266)))))
| 'LE'(f(X266),'0')
| 'E'(f(X266),f(suc(X266)))
| ~ 'E'('0',f(X266)) ),
inference(resolution,[status(thm)],[c2912,c128]) ).
cnf(c3301,plain,
( 'E'(s('0'),f(suc(suc(suc(X267)))))
| 'LE'(f(X267),'0')
| 'E'(f(X267),f(suc(X267))) ),
inference(resolution,[status(thm)],[c3296,c7]) ).
cnf(clause_151,axiom,
( ~ 'LE'(f(suc(suc(suc(X26)))),s('0'))
| 'E'('0',f(suc(suc(suc(X26)))))
| 'LE'(f(X26),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_151) ).
cnf(c70,plain,
( 'E'('0',f(suc(suc(suc(X27)))))
| 'LE'(f(X27),'0')
| 'E'(s('0'),f(suc(suc(suc(X27))))) ),
inference(resolution,[status(thm)],[clause_151,c0]) ).
cnf(clause_139,axiom,
( ~ 'E'('0',f(suc(X68)))
| ~ 'E'('0',f(suc(suc(X68))))
| ~ 'E'(f(X68),f(suc(suc(X68))))
| ~ 'E'('0',f(X68))
| ~ 'E'('0',f(suc(suc(suc(X68)))))
| ~ 'E'(f(X68),f(suc(X68)))
| iLEQ(suc(X68),suc(X68)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_139) ).
cnf(c519,plain,
( ~ 'E'('0',f(suc(X1409)))
| ~ 'E'('0',f(suc(suc(X1409))))
| ~ 'E'(f(X1409),f(suc(suc(X1409))))
| ~ 'E'('0',f(X1409))
| ~ 'E'(f(X1409),f(suc(X1409)))
| iLEQ(suc(X1409),suc(X1409))
| 'LE'(f(X1409),'0')
| 'E'(s('0'),f(suc(suc(suc(X1409))))) ),
inference(resolution,[status(thm)],[clause_139,c70]) ).
cnf(clause_4,axiom,
( ~ 'E'('0',f(suc(suc(X40))))
| ~ 'E'('0',f(suc(X40)))
| ~ 'E'(f(X40),f(suc(X40)))
| ~ 'E'('0',f(X40))
| 'E'(f(X40),f(suc(suc(X40))))
| iLEQ(suc(X40),suc(X40)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
cnf(c2908,plain,
( 'E'(s('0'),f(suc(suc(suc(X3261)))))
| 'LE'(f(X3261),'0')
| iLEQ(suc(X3261),suc(X3261))
| ~ 'E'('0',f(suc(suc(X3261))))
| ~ 'E'('0',f(suc(X3261)))
| ~ 'E'('0',f(X3261))
| 'E'(f(X3261),f(suc(suc(X3261)))) ),
inference(resolution,[status(thm)],[c2834,clause_4]) ).
cnf(c41756,plain,
( 'E'(s('0'),f(suc(suc(suc(X3262)))))
| 'LE'(f(X3262),'0')
| iLEQ(suc(X3262),suc(X3262))
| ~ 'E'('0',f(suc(X3262)))
| ~ 'E'('0',f(X3262))
| 'E'(f(X3262),f(suc(suc(X3262)))) ),
inference(resolution,[status(thm)],[c2908,c16]) ).
cnf(c41848,plain,
( 'E'(s('0'),f(suc(suc(suc(X3263)))))
| 'LE'(f(X3263),'0')
| iLEQ(suc(X3263),suc(X3263))
| ~ 'E'('0',f(X3263))
| 'E'(f(X3263),f(suc(suc(X3263)))) ),
inference(resolution,[status(thm)],[c41756,c128]) ).
cnf(c41909,plain,
( 'E'(s('0'),f(suc(suc(suc(X3264)))))
| 'LE'(f(X3264),'0')
| iLEQ(suc(X3264),suc(X3264))
| 'E'(f(X3264),f(suc(suc(X3264)))) ),
inference(resolution,[status(thm)],[c41848,c12361]) ).
cnf(c42312,plain,
( 'E'(s('0'),f(suc(suc(suc(X3291)))))
| 'LE'(f(X3291),'0')
| iLEQ(suc(X3291),suc(X3291))
| ~ 'E'('0',f(suc(X3291)))
| ~ 'E'('0',f(suc(suc(X3291))))
| ~ 'E'('0',f(X3291))
| ~ 'E'(f(X3291),f(suc(X3291))) ),
inference(resolution,[status(thm)],[c41909,c519]) ).
cnf(c42858,plain,
( 'E'(s('0'),f(suc(suc(suc(X3292)))))
| 'LE'(f(X3292),'0')
| iLEQ(suc(X3292),suc(X3292))
| ~ 'E'('0',f(suc(X3292)))
| ~ 'E'('0',f(suc(suc(X3292))))
| ~ 'E'('0',f(X3292)) ),
inference(resolution,[status(thm)],[c42312,c3301]) ).
cnf(c42926,plain,
( 'E'(s('0'),f(suc(suc(suc(X3293)))))
| 'LE'(f(X3293),'0')
| iLEQ(suc(X3293),suc(X3293))
| ~ 'E'('0',f(suc(X3293)))
| ~ 'E'('0',f(X3293)) ),
inference(resolution,[status(thm)],[c42858,c16]) ).
cnf(c43018,plain,
( 'E'(s('0'),f(suc(suc(suc(X3294)))))
| 'LE'(f(X3294),'0')
| iLEQ(suc(X3294),suc(X3294))
| ~ 'E'('0',f(X3294)) ),
inference(resolution,[status(thm)],[c42926,c128]) ).
cnf(c43096,plain,
( 'E'(s('0'),f(suc(suc(suc(X3296)))))
| 'LE'(f(X3296),'0')
| iLEQ(suc(X3296),suc(X3296)) ),
inference(resolution,[status(thm)],[c43018,c36047]) ).
cnf(clause_167,axiom,
( ~ 'E'('0',f(suc(X6)))
| ~ 'E'('0',f(suc(suc(X7))))
| ~ 'E'('0',f(suc(suc(X6))))
| ~ 'E'(f(X6),f(suc(suc(X6))))
| ~ 'E'('0',f(X6))
| ~ iLEQ(suc(X6),suc(X7))
| ~ 'E'('0',f(suc(suc(suc(X7)))))
| ~ 'E'('0',f(suc(suc(suc(X6)))))
| ~ 'E'('0',f(X7))
| ~ 'E'(f(X7),f(suc(suc(X7))))
| ~ 'E'(f(X6),f(suc(X6)))
| ~ 'E'(f(X7),f(suc(X7)))
| ~ 'E'('0',f(suc(X7))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_167) ).
cnf(c1,plain,
( ~ 'E'('0',f(suc(X109)))
| ~ 'E'('0',f(suc(suc(X109))))
| ~ 'E'(f(X109),f(suc(suc(X109))))
| ~ 'E'('0',f(X109))
| ~ iLEQ(suc(X109),suc(X109))
| ~ 'E'('0',f(suc(suc(suc(X109)))))
| ~ 'E'(f(X109),f(suc(X109))) ),
inference(factor,[status(thm)],[clause_167]) ).
cnf(c1063,plain,
( ~ 'E'('0',f(suc(X2902)))
| ~ 'E'('0',f(suc(suc(X2902))))
| ~ 'E'(f(X2902),f(suc(suc(X2902))))
| ~ 'E'('0',f(X2902))
| ~ iLEQ(suc(X2902),suc(X2902))
| ~ 'E'(f(X2902),f(suc(X2902)))
| 'LE'(f(X2902),'0')
| 'E'(s('0'),f(suc(suc(suc(X2902))))) ),
inference(resolution,[status(thm)],[c1,c70]) ).
cnf(clause_78,axiom,
( ~ 'E'('0',f(suc(X35)))
| ~ 'E'('0',f(suc(suc(X36))))
| ~ 'E'('0',f(suc(suc(X35))))
| ~ 'E'('0',f(X35))
| ~ iLEQ(suc(X35),suc(X36))
| ~ 'E'('0',f(X36))
| ~ 'E'(f(X35),f(suc(X35)))
| ~ 'E'(f(X36),f(suc(X36)))
| ~ 'E'('0',f(suc(X36)))
| 'E'(f(X35),f(suc(suc(X35))))
| 'E'(f(X36),f(suc(suc(X36)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_78) ).
cnf(c131,plain,
( ~ 'E'('0',f(suc(X380)))
| ~ 'E'('0',f(suc(suc(X380))))
| ~ 'E'('0',f(X380))
| ~ iLEQ(suc(X380),suc(X380))
| ~ 'E'(f(X380),f(suc(X380)))
| 'E'(f(X380),f(suc(suc(X380)))) ),
inference(factor,[status(thm)],[clause_78]) ).
cnf(c3903,plain,
( ~ 'E'('0',f(suc(X3429)))
| ~ 'E'('0',f(suc(suc(X3429))))
| ~ 'E'('0',f(X3429))
| ~ iLEQ(suc(X3429),suc(X3429))
| 'E'(f(X3429),f(suc(suc(X3429))))
| 'E'(s('0'),f(suc(suc(suc(X3429)))))
| 'LE'(f(X3429),'0') ),
inference(resolution,[status(thm)],[c131,c3301]) ).
cnf(c44424,plain,
( ~ 'E'('0',f(suc(X3430)))
| ~ 'E'('0',f(X3430))
| ~ iLEQ(suc(X3430),suc(X3430))
| 'E'(f(X3430),f(suc(suc(X3430))))
| 'E'(s('0'),f(suc(suc(suc(X3430)))))
| 'LE'(f(X3430),'0') ),
inference(resolution,[status(thm)],[c3903,c16]) ).
cnf(c44464,plain,
( ~ 'E'('0',f(suc(X3431)))
| ~ 'E'('0',f(X3431))
| 'E'(f(X3431),f(suc(suc(X3431))))
| 'E'(s('0'),f(suc(suc(suc(X3431)))))
| 'LE'(f(X3431),'0') ),
inference(resolution,[status(thm)],[c44424,c43096]) ).
cnf(c44564,plain,
( ~ 'E'('0',f(X3432))
| 'E'(f(X3432),f(suc(suc(X3432))))
| 'E'(s('0'),f(suc(suc(suc(X3432)))))
| 'LE'(f(X3432),'0') ),
inference(resolution,[status(thm)],[c44464,c128]) ).
cnf(c44628,plain,
( 'E'(f(X3433),f(suc(suc(X3433))))
| 'E'(s('0'),f(suc(suc(suc(X3433)))))
| 'LE'(f(X3433),'0') ),
inference(resolution,[status(thm)],[c44564,c12361]) ).
cnf(c44782,plain,
( 'E'(s('0'),f(suc(suc(suc(X3492)))))
| 'LE'(f(X3492),'0')
| ~ 'E'('0',f(suc(X3492)))
| ~ 'E'('0',f(suc(suc(X3492))))
| ~ 'E'('0',f(X3492))
| ~ iLEQ(suc(X3492),suc(X3492))
| ~ 'E'(f(X3492),f(suc(X3492))) ),
inference(resolution,[status(thm)],[c44628,c1063]) ).
cnf(c45576,plain,
( 'E'(s('0'),f(suc(suc(suc(X3494)))))
| 'LE'(f(X3494),'0')
| ~ 'E'('0',f(suc(X3494)))
| ~ 'E'('0',f(suc(suc(X3494))))
| ~ 'E'('0',f(X3494))
| ~ iLEQ(suc(X3494),suc(X3494)) ),
inference(resolution,[status(thm)],[c44782,c3301]) ).
cnf(c45647,plain,
( 'E'(s('0'),f(suc(suc(suc(X3495)))))
| 'LE'(f(X3495),'0')
| ~ 'E'('0',f(suc(X3495)))
| ~ 'E'('0',f(X3495))
| ~ iLEQ(suc(X3495),suc(X3495)) ),
inference(resolution,[status(thm)],[c45576,c16]) ).
cnf(c45687,plain,
( 'E'(s('0'),f(suc(suc(suc(X3496)))))
| 'LE'(f(X3496),'0')
| ~ 'E'('0',f(suc(X3496)))
| ~ 'E'('0',f(X3496)) ),
inference(resolution,[status(thm)],[c45647,c43096]) ).
cnf(c45787,plain,
( 'E'(s('0'),f(suc(suc(suc(X3497)))))
| 'LE'(f(X3497),'0')
| ~ 'E'('0',f(X3497)) ),
inference(resolution,[status(thm)],[c45687,c128]) ).
cnf(c45938,plain,
( 'E'(s('0'),f(suc(suc(suc(X3498)))))
| 'LE'(f(X3498),'0') ),
inference(resolution,[status(thm)],[c45787,c7]) ).
cnf(c46021,plain,
( 'LE'(f(X4313),'0')
| ~ iLEQ(suc(X4313),suc(X4313))
| ~ 'E'(s('0'),f(suc(suc(X4313))))
| ~ 'E'(s('0'),f(X4313))
| ~ 'E'(s('0'),f(suc(X4313)))
| ~ 'E'(f(X4313),f(suc(suc(X4313))))
| ~ 'E'(f(X4313),f(suc(X4313))) ),
inference(resolution,[status(thm)],[c45938,c338]) ).
cnf(c61109,plain,
( 'LE'(f(X4315),'0')
| ~ iLEQ(suc(X4315),suc(X4315))
| ~ 'E'(s('0'),f(suc(suc(X4315))))
| ~ 'E'(s('0'),f(X4315))
| ~ 'E'(s('0'),f(suc(X4315)))
| ~ 'E'(f(X4315),f(suc(X4315)))
| 'E'('0',f(X4315)) ),
inference(resolution,[status(thm)],[c46021,c12361]) ).
cnf(c61156,plain,
( 'LE'(f(X4316),'0')
| ~ iLEQ(suc(X4316),suc(X4316))
| ~ 'E'(s('0'),f(X4316))
| ~ 'E'(s('0'),f(suc(X4316)))
| ~ 'E'(f(X4316),f(suc(X4316)))
| 'E'('0',f(X4316)) ),
inference(resolution,[status(thm)],[c61109,c127]) ).
cnf(c61222,plain,
( 'LE'(f(X4317),'0')
| ~ iLEQ(suc(X4317),suc(X4317))
| ~ 'E'(s('0'),f(X4317))
| ~ 'E'(s('0'),f(suc(X4317)))
| 'E'('0',f(X4317)) ),
inference(resolution,[status(thm)],[c61156,c313]) ).
cnf(c61372,plain,
( 'LE'(f(X4318),'0')
| ~ iLEQ(suc(X4318),suc(X4318))
| ~ 'E'(s('0'),f(X4318))
| 'E'('0',f(X4318)) ),
inference(resolution,[status(thm)],[c61222,c14]) ).
cnf(c61422,plain,
( 'LE'(f(X4319),'0')
| ~ iLEQ(suc(X4319),suc(X4319))
| 'E'('0',f(X4319)) ),
inference(resolution,[status(thm)],[c61372,c3]) ).
cnf(c61457,plain,
( 'LE'(f(X4321),'0')
| 'E'('0',f(X4321)) ),
inference(resolution,[status(thm)],[c61422,c36047]) ).
cnf(c7742,plain,
( ~ iLEQ(suc(X5768),suc(X5768))
| ~ 'E'(s('0'),f(suc(suc(X5768))))
| ~ 'E'(s('0'),f(X5768))
| ~ 'E'(s('0'),f(suc(X5768)))
| ~ 'E'(f(X5768),f(suc(suc(X5768))))
| ~ 'E'(f(X5768),f(suc(X5768)))
| 'LE'(f(X5768),s('0')) ),
inference(resolution,[status(thm)],[c338,c6]) ).
cnf(c84673,plain,
( ~ iLEQ(suc(X5769),suc(X5769))
| ~ 'E'(s('0'),f(suc(suc(X5769))))
| ~ 'E'(s('0'),f(X5769))
| ~ 'E'(s('0'),f(suc(X5769)))
| ~ 'E'(f(X5769),f(suc(X5769)))
| 'LE'(f(X5769),s('0')) ),
inference(resolution,[status(thm)],[c7742,c12250]) ).
cnf(c84737,plain,
( ~ iLEQ(suc(X5770),suc(X5770))
| ~ 'E'(s('0'),f(X5770))
| ~ 'E'(s('0'),f(suc(X5770)))
| ~ 'E'(f(X5770),f(suc(X5770)))
| 'LE'(f(X5770),s('0')) ),
inference(resolution,[status(thm)],[c84673,c123]) ).
cnf(c84803,plain,
( ~ iLEQ(suc(X5773),suc(X5773))
| ~ 'E'(s('0'),f(X5773))
| ~ 'E'(s('0'),f(suc(X5773)))
| 'LE'(f(X5773),s('0')) ),
inference(resolution,[status(thm)],[c84737,c309]) ).
cnf(c84871,plain,
( ~ iLEQ(suc(X5774),suc(X5774))
| ~ 'E'(s('0'),f(X5774))
| 'LE'(f(X5774),s('0')) ),
inference(resolution,[status(thm)],[c84803,c13]) ).
cnf(c84906,plain,
( ~ iLEQ(suc(X5775),suc(X5775))
| 'LE'(f(X5775),s('0')) ),
inference(resolution,[status(thm)],[c84871,c0]) ).
cnf(c84955,plain,
'LE'(f(X5776),s('0')),
inference(resolution,[status(thm)],[c84906,c36004]) ).
cnf(c84959,plain,
( 'E'('0',f(suc(X5777)))
| 'LE'(f(X5777),'0') ),
inference(resolution,[status(thm)],[c84955,clause_122]) ).
cnf(c84961,plain,
( 'E'('0',f(suc(suc(X5779))))
| 'LE'(f(X5779),'0') ),
inference(resolution,[status(thm)],[c84955,clause_141]) ).
cnf(c85000,plain,
( 'LE'(f(X5790),'0')
| ~ 'E'('0',f(X5790))
| 'E'(f(X5790),f(suc(X5790)))
| iLEQ(suc(X5790),suc(X5790)) ),
inference(resolution,[status(thm)],[c84959,clause_93]) ).
cnf(c85183,plain,
( 'LE'(f(X5791),'0')
| 'E'(f(X5791),f(suc(X5791)))
| iLEQ(suc(X5791),suc(X5791)) ),
inference(resolution,[status(thm)],[c85000,c61457]) ).
cnf(c85218,plain,
( 'LE'(f(X5793),'0')
| 'E'(f(X5793),f(suc(X5793)))
| ~ 'E'('0',f(suc(X5793)))
| ~ 'E'('0',f(X5793)) ),
inference(resolution,[status(thm)],[c85183,c914]) ).
cnf(c85220,plain,
( 'LE'(f(X5794),'0')
| 'E'(f(X5794),f(suc(X5794)))
| ~ 'E'('0',f(X5794)) ),
inference(resolution,[status(thm)],[c85218,c84959]) ).
cnf(c85233,plain,
( 'LE'(f(X5795),'0')
| 'E'(f(X5795),f(suc(X5795))) ),
inference(resolution,[status(thm)],[c85220,c61457]) ).
cnf(c85195,plain,
( 'LE'(f(X5952),'0')
| iLEQ(suc(X5952),suc(X5952))
| ~ 'E'('0',f(suc(suc(X5952))))
| ~ 'E'('0',f(suc(X5952)))
| ~ 'E'('0',f(X5952))
| 'E'(f(X5952),f(suc(suc(X5952)))) ),
inference(resolution,[status(thm)],[c85183,clause_4]) ).
cnf(c86405,plain,
( 'LE'(f(X5953),'0')
| iLEQ(suc(X5953),suc(X5953))
| ~ 'E'('0',f(suc(X5953)))
| ~ 'E'('0',f(X5953))
| 'E'(f(X5953),f(suc(suc(X5953)))) ),
inference(resolution,[status(thm)],[c85195,c84961]) ).
cnf(c86408,plain,
( 'LE'(f(X5954),'0')
| iLEQ(suc(X5954),suc(X5954))
| ~ 'E'('0',f(X5954))
| 'E'(f(X5954),f(suc(suc(X5954)))) ),
inference(resolution,[status(thm)],[c86405,c84959]) ).
cnf(c86421,plain,
( 'LE'(f(X5955),'0')
| iLEQ(suc(X5955),suc(X5955))
| 'E'(f(X5955),f(suc(suc(X5955)))) ),
inference(resolution,[status(thm)],[c86408,c61457]) ).
cnf(c85257,plain,
( 'LE'(f(X5964),'0')
| ~ 'E'('0',f(suc(X5964)))
| ~ 'E'('0',f(suc(suc(X5964))))
| ~ 'E'('0',f(X5964))
| ~ iLEQ(suc(X5964),suc(X5964))
| 'E'(f(X5964),f(suc(suc(X5964)))) ),
inference(resolution,[status(thm)],[c85233,c131]) ).
cnf(c86485,plain,
( 'LE'(f(X5965),'0')
| ~ 'E'('0',f(suc(X5965)))
| ~ 'E'('0',f(X5965))
| ~ iLEQ(suc(X5965),suc(X5965))
| 'E'(f(X5965),f(suc(suc(X5965)))) ),
inference(resolution,[status(thm)],[c85257,c84961]) ).
cnf(c86488,plain,
( 'LE'(f(X5966),'0')
| ~ 'E'('0',f(suc(X5966)))
| ~ 'E'('0',f(X5966))
| 'E'(f(X5966),f(suc(suc(X5966)))) ),
inference(resolution,[status(thm)],[c86485,c86421]) ).
cnf(c86492,plain,
( 'LE'(f(X5967),'0')
| ~ 'E'('0',f(X5967))
| 'E'(f(X5967),f(suc(suc(X5967)))) ),
inference(resolution,[status(thm)],[c86488,c84959]) ).
cnf(c86505,plain,
( 'LE'(f(X5970),'0')
| 'E'(f(X5970),f(suc(suc(X5970)))) ),
inference(resolution,[status(thm)],[c86492,c61457]) ).
cnf(c84960,plain,
( 'E'('0',f(suc(suc(suc(X5780)))))
| 'LE'(f(X5780),'0') ),
inference(resolution,[status(thm)],[c84955,clause_151]) ).
cnf(c85111,plain,
( 'LE'(f(X6063),'0')
| ~ 'E'('0',f(suc(X6063)))
| ~ 'E'('0',f(suc(suc(X6063))))
| ~ 'E'(f(X6063),f(suc(suc(X6063))))
| ~ 'E'('0',f(X6063))
| ~ iLEQ(suc(X6063),suc(X6063))
| ~ 'E'(f(X6063),f(suc(X6063))) ),
inference(resolution,[status(thm)],[c84960,c1]) ).
cnf(c86572,plain,
( 'LE'(f(X6064),'0')
| ~ 'E'('0',f(suc(X6064)))
| ~ 'E'('0',f(suc(suc(X6064))))
| ~ 'E'('0',f(X6064))
| ~ iLEQ(suc(X6064),suc(X6064))
| ~ 'E'(f(X6064),f(suc(X6064))) ),
inference(resolution,[status(thm)],[c85111,c86505]) ).
cnf(c86576,plain,
( 'LE'(f(X6065),'0')
| ~ 'E'('0',f(suc(X6065)))
| ~ 'E'('0',f(suc(suc(X6065))))
| ~ 'E'('0',f(X6065))
| ~ iLEQ(suc(X6065),suc(X6065)) ),
inference(resolution,[status(thm)],[c86572,c85233]) ).
cnf(c86585,plain,
( 'LE'(f(X6066),'0')
| ~ 'E'('0',f(suc(X6066)))
| ~ 'E'('0',f(X6066))
| ~ iLEQ(suc(X6066),suc(X6066)) ),
inference(resolution,[status(thm)],[c86576,c84961]) ).
cnf(c85112,plain,
( 'LE'(f(X6072),'0')
| ~ 'E'('0',f(suc(X6072)))
| ~ 'E'('0',f(suc(suc(X6072))))
| ~ 'E'(f(X6072),f(suc(suc(X6072))))
| ~ 'E'('0',f(X6072))
| ~ 'E'(f(X6072),f(suc(X6072)))
| iLEQ(suc(X6072),suc(X6072)) ),
inference(resolution,[status(thm)],[c84960,clause_139]) ).
cnf(c86588,plain,
( 'LE'(f(X6074),'0')
| ~ 'E'('0',f(suc(X6074)))
| ~ 'E'('0',f(suc(suc(X6074))))
| ~ 'E'('0',f(X6074))
| ~ 'E'(f(X6074),f(suc(X6074)))
| iLEQ(suc(X6074),suc(X6074)) ),
inference(resolution,[status(thm)],[c85112,c86505]) ).
cnf(c86592,plain,
( 'LE'(f(X6075),'0')
| ~ 'E'('0',f(suc(X6075)))
| ~ 'E'('0',f(suc(suc(X6075))))
| ~ 'E'('0',f(X6075))
| iLEQ(suc(X6075),suc(X6075)) ),
inference(resolution,[status(thm)],[c86588,c85233]) ).
cnf(c86601,plain,
( 'LE'(f(X6076),'0')
| ~ 'E'('0',f(suc(X6076)))
| ~ 'E'('0',f(X6076))
| iLEQ(suc(X6076),suc(X6076)) ),
inference(resolution,[status(thm)],[c86592,c84961]) ).
cnf(c86604,plain,
( 'LE'(f(X6077),'0')
| ~ 'E'('0',f(X6077))
| iLEQ(suc(X6077),suc(X6077)) ),
inference(resolution,[status(thm)],[c86601,c84959]) ).
cnf(c86617,plain,
( 'LE'(f(X6078),'0')
| iLEQ(suc(X6078),suc(X6078)) ),
inference(resolution,[status(thm)],[c86604,c61457]) ).
cnf(c86622,plain,
( 'LE'(f(X6080),'0')
| ~ 'E'('0',f(suc(X6080)))
| ~ 'E'('0',f(X6080)) ),
inference(resolution,[status(thm)],[c86617,c86585]) ).
cnf(c86626,plain,
( 'LE'(f(X6081),'0')
| ~ 'E'('0',f(X6081)) ),
inference(resolution,[status(thm)],[c86622,c84959]) ).
cnf(c86639,plain,
'LE'(f(X6082),'0'),
inference(resolution,[status(thm)],[c86626,c61457]) ).
cnf(c86641,plain,
$false,
inference(resolution,[status(thm)],[c86639,clause_87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO658-1 : TPTP v8.1.2. Released v7.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.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 : Wed May 8 18:05:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 258.93/259.12 % Version: 1.5
% 258.93/259.12 % SZS status Unsatisfiable
% 258.93/259.12 % SZS output start CNFRefutation
% See solution above
% 258.93/259.12
% 258.93/259.12 % Initial clauses : 34
% 258.93/259.12 % Processed clauses : 1663
% 258.93/259.12 % Factors computed : 261
% 258.93/259.12 % Resolvents computed: 86381
% 258.93/259.12 % Tautologies deleted: 179
% 258.93/259.12 % Forward subsumed : 8952
% 258.93/259.12 % Backward subsumed : 1581
% 258.93/259.12 % -------- CPU Time ---------
% 258.93/259.12 % User time : 258.268 s
% 258.93/259.12 % System time : 0.519 s
% 258.93/259.12 % Total time : 258.787 s
%------------------------------------------------------------------------------