%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO648-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:04 EDT 2024
% Result : Unsatisfiable 3.49s 3.74s
% Output : Refutation 3.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 15
% Syntax : Number of clauses : 68 ( 4 unt; 51 nHn; 54 RR)
% Number of literals : 339 ( 0 equ; 211 neg)
% Maximal clause size : 17 ( 4 avg)
% Maximal term depth : 6 ( 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 : 70 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_160,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_160) ).
cnf(clause_299,axiom,
'LE'(f(X2),s('0')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_299) ).
cnf(clause_62,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_62) ).
cnf(c0,plain,
( 'E'('0',f(X4))
| 'LE'(f(X4),'0') ),
inference(resolution,[status(thm)],[clause_62,clause_299]) ).
cnf(clause_328,axiom,
( ~ 'LE'(f(suc(X7)),s('0'))
| 'E'('0',f(suc(X7)))
| 'LE'(f(X7),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_328) ).
cnf(c2,plain,
( 'E'('0',f(suc(X8)))
| 'LE'(f(X8),'0') ),
inference(resolution,[status(thm)],[clause_328,clause_299]) ).
cnf(clause_114,axiom,
( ~ 'LE'(f(suc(suc(X9))),s('0'))
| 'E'('0',f(suc(suc(X9))))
| 'LE'(f(X9),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_114) ).
cnf(c4,plain,
( 'E'('0',f(suc(suc(X10))))
| 'LE'(f(X10),'0') ),
inference(resolution,[status(thm)],[clause_114,clause_299]) ).
cnf(clause_48,axiom,
( ~ 'E'('0',f(X13))
| ~ 'E'('0',f(suc(X13)))
| 'E'(f(X13),f(suc(X13)))
| iLEQ(suc(X13),suc(X13)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_48) ).
cnf(c13,plain,
( ~ 'E'('0',f(X16))
| 'E'(f(X16),f(suc(X16)))
| iLEQ(suc(X16),suc(X16))
| 'LE'(f(X16),'0') ),
inference(resolution,[status(thm)],[clause_48,c2]) ).
cnf(c29,plain,
( 'E'(f(X17),f(suc(X17)))
| iLEQ(suc(X17),suc(X17))
| 'LE'(f(X17),'0') ),
inference(resolution,[status(thm)],[c13,c0]) ).
cnf(clause_168,axiom,
( ~ 'E'('0',f(suc(X45)))
| ~ 'E'('0',f(X45))
| ~ 'E'('0',f(suc(X44)))
| ~ iLEQ(suc(X45),suc(X44))
| ~ 'E'('0',f(X44))
| 'E'(f(X45),f(suc(X45)))
| 'E'(f(X44),f(suc(X44))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_168) ).
cnf(c110,plain,
( ~ 'E'('0',f(suc(X48)))
| ~ 'E'('0',f(X48))
| 'E'(f(X48),f(suc(X48)))
| 'LE'(f(X48),'0') ),
inference(resolution,[status(thm)],[clause_168,c29]) ).
cnf(c127,plain,
( ~ 'E'('0',f(X49))
| 'E'(f(X49),f(suc(X49)))
| 'LE'(f(X49),'0') ),
inference(resolution,[status(thm)],[c110,c2]) ).
cnf(c132,plain,
( 'E'(f(X50),f(suc(X50)))
| 'LE'(f(X50),'0') ),
inference(resolution,[status(thm)],[c127,c0]) ).
cnf(clause_260,axiom,
( ~ 'LE'(f(suc(suc(suc(X11)))),s('0'))
| 'E'('0',f(suc(suc(suc(X11)))))
| 'LE'(f(X11),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_260) ).
cnf(c6,plain,
( 'E'('0',f(suc(suc(suc(X12)))))
| 'LE'(f(X12),'0') ),
inference(resolution,[status(thm)],[clause_260,clause_299]) ).
cnf(clause_254,axiom,
( ~ 'E'('0',f(suc(suc(X54))))
| ~ 'E'('0',f(suc(X54)))
| ~ 'E'(f(X54),f(suc(X54)))
| ~ 'E'('0',f(X54))
| 'E'(f(X54),f(suc(suc(X54))))
| iLEQ(suc(X54),suc(X54)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_254) ).
cnf(c143,plain,
( ~ 'E'('0',f(suc(suc(X107))))
| ~ 'E'('0',f(suc(X107)))
| ~ 'E'('0',f(X107))
| 'E'(f(X107),f(suc(suc(X107))))
| iLEQ(suc(X107),suc(X107))
| 'LE'(f(X107),'0') ),
inference(resolution,[status(thm)],[clause_254,c132]) ).
cnf(c280,plain,
( ~ 'E'('0',f(suc(X108)))
| ~ 'E'('0',f(X108))
| 'E'(f(X108),f(suc(suc(X108))))
| iLEQ(suc(X108),suc(X108))
| 'LE'(f(X108),'0') ),
inference(resolution,[status(thm)],[c143,c4]) ).
cnf(c291,plain,
( ~ 'E'('0',f(X109))
| 'E'(f(X109),f(suc(suc(X109))))
| iLEQ(suc(X109),suc(X109))
| 'LE'(f(X109),'0') ),
inference(resolution,[status(thm)],[c280,c2]) ).
cnf(c299,plain,
( 'E'(f(X112),f(suc(suc(X112))))
| iLEQ(suc(X112),suc(X112))
| 'LE'(f(X112),'0') ),
inference(resolution,[status(thm)],[c291,c0]) ).
cnf(clause_79,axiom,
( ~ 'E'('0',f(suc(X15)))
| ~ 'E'('0',f(suc(suc(X15))))
| ~ 'E'('0',f(X15))
| ~ 'E'('0',f(suc(X14)))
| ~ 'E'(f(X14),f(suc(X14)))
| ~ iLEQ(suc(X15),suc(X14))
| ~ 'E'('0',f(X14))
| ~ 'E'(f(X15),f(suc(X15)))
| ~ 'E'('0',f(suc(suc(X14))))
| 'E'(f(X15),f(suc(suc(X15))))
| 'E'(f(X14),f(suc(suc(X14)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_79) ).
cnf(c18,plain,
( ~ 'E'('0',f(suc(X81)))
| ~ 'E'('0',f(suc(suc(X81))))
| ~ 'E'('0',f(X81))
| ~ 'E'(f(X81),f(suc(X81)))
| ~ iLEQ(suc(X81),suc(X81))
| 'E'(f(X81),f(suc(suc(X81)))) ),
inference(factor,[status(thm)],[clause_79]) ).
cnf(c225,plain,
( ~ 'E'('0',f(suc(X121)))
| ~ 'E'('0',f(suc(suc(X121))))
| ~ 'E'('0',f(X121))
| ~ iLEQ(suc(X121),suc(X121))
| 'E'(f(X121),f(suc(suc(X121))))
| 'LE'(f(X121),'0') ),
inference(resolution,[status(thm)],[c18,c132]) ).
cnf(c333,plain,
( ~ 'E'('0',f(suc(X122)))
| ~ 'E'('0',f(X122))
| ~ iLEQ(suc(X122),suc(X122))
| 'E'(f(X122),f(suc(suc(X122))))
| 'LE'(f(X122),'0') ),
inference(resolution,[status(thm)],[c225,c4]) ).
cnf(c341,plain,
( ~ 'E'('0',f(suc(X123)))
| ~ 'E'('0',f(X123))
| 'E'(f(X123),f(suc(suc(X123))))
| 'LE'(f(X123),'0') ),
inference(resolution,[status(thm)],[c333,c299]) ).
cnf(c346,plain,
( ~ 'E'('0',f(X124))
| 'E'(f(X124),f(suc(suc(X124))))
| 'LE'(f(X124),'0') ),
inference(resolution,[status(thm)],[c341,c2]) ).
cnf(c354,plain,
( 'E'(f(X125),f(suc(suc(X125))))
| 'LE'(f(X125),'0') ),
inference(resolution,[status(thm)],[c346,c0]) ).
cnf(clause_231,axiom,
( ~ 'LE'(f(suc(suc(suc(suc(X22))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(X22))))))
| 'LE'(f(X22),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_231) ).
cnf(c46,plain,
( 'E'('0',f(suc(suc(suc(suc(X24))))))
| 'LE'(f(X24),'0') ),
inference(resolution,[status(thm)],[clause_231,clause_299]) ).
cnf(clause_157,axiom,
( ~ 'E'('0',f(suc(suc(suc(X29)))))
| ~ 'E'('0',f(suc(X29)))
| ~ 'E'(f(X29),f(suc(suc(suc(X29)))))
| ~ 'E'('0',f(suc(suc(X29))))
| ~ 'E'('0',f(X29))
| ~ 'E'(f(X29),f(suc(suc(X29))))
| ~ 'E'(f(X29),f(suc(X29)))
| ~ 'E'('0',f(suc(suc(suc(suc(X29))))))
| iLEQ(suc(X29),suc(X29)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_157) ).
cnf(c80,plain,
( ~ 'E'('0',f(suc(suc(suc(X207)))))
| ~ 'E'('0',f(suc(X207)))
| ~ 'E'(f(X207),f(suc(suc(suc(X207)))))
| ~ 'E'('0',f(suc(suc(X207))))
| ~ 'E'('0',f(X207))
| ~ 'E'(f(X207),f(suc(suc(X207))))
| ~ 'E'(f(X207),f(suc(X207)))
| iLEQ(suc(X207),suc(X207))
| 'LE'(f(X207),'0') ),
inference(resolution,[status(thm)],[clause_157,c46]) ).
cnf(clause_326,axiom,
( ~ 'E'('0',f(suc(suc(suc(X23)))))
| ~ 'E'('0',f(suc(X23)))
| ~ 'E'('0',f(suc(suc(X23))))
| ~ 'E'('0',f(X23))
| ~ 'E'(f(X23),f(suc(suc(X23))))
| ~ 'E'(f(X23),f(suc(X23)))
| 'E'(f(X23),f(suc(suc(suc(X23)))))
| iLEQ(suc(X23),suc(X23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_326) ).
cnf(c318,plain,
( iLEQ(suc(X253),suc(X253))
| 'LE'(f(X253),'0')
| ~ 'E'('0',f(suc(suc(suc(X253)))))
| ~ 'E'('0',f(suc(X253)))
| ~ 'E'('0',f(suc(suc(X253))))
| ~ 'E'('0',f(X253))
| ~ 'E'(f(X253),f(suc(X253)))
| 'E'(f(X253),f(suc(suc(suc(X253))))) ),
inference(resolution,[status(thm)],[c299,clause_326]) ).
cnf(c637,plain,
( iLEQ(suc(X254),suc(X254))
| 'LE'(f(X254),'0')
| ~ 'E'('0',f(suc(X254)))
| ~ 'E'('0',f(suc(suc(X254))))
| ~ 'E'('0',f(X254))
| ~ 'E'(f(X254),f(suc(X254)))
| 'E'(f(X254),f(suc(suc(suc(X254))))) ),
inference(resolution,[status(thm)],[c318,c6]) ).
cnf(c640,plain,
( iLEQ(suc(X255),suc(X255))
| 'LE'(f(X255),'0')
| ~ 'E'('0',f(suc(X255)))
| ~ 'E'('0',f(suc(suc(X255))))
| ~ 'E'('0',f(X255))
| 'E'(f(X255),f(suc(suc(suc(X255))))) ),
inference(resolution,[status(thm)],[c637,c132]) ).
cnf(c648,plain,
( iLEQ(suc(X256),suc(X256))
| 'LE'(f(X256),'0')
| ~ 'E'('0',f(suc(X256)))
| ~ 'E'('0',f(X256))
| 'E'(f(X256),f(suc(suc(suc(X256))))) ),
inference(resolution,[status(thm)],[c640,c4]) ).
cnf(c659,plain,
( iLEQ(suc(X259),suc(X259))
| 'LE'(f(X259),'0')
| ~ 'E'('0',f(X259))
| 'E'(f(X259),f(suc(suc(suc(X259))))) ),
inference(resolution,[status(thm)],[c648,c2]) ).
cnf(c667,plain,
( iLEQ(suc(X260),suc(X260))
| 'LE'(f(X260),'0')
| 'E'(f(X260),f(suc(suc(suc(X260))))) ),
inference(resolution,[status(thm)],[c659,c0]) ).
cnf(c677,plain,
( iLEQ(suc(X304),suc(X304))
| 'LE'(f(X304),'0')
| ~ 'E'('0',f(suc(suc(suc(X304)))))
| ~ 'E'('0',f(suc(X304)))
| ~ 'E'('0',f(suc(suc(X304))))
| ~ 'E'('0',f(X304))
| ~ 'E'(f(X304),f(suc(suc(X304))))
| ~ 'E'(f(X304),f(suc(X304))) ),
inference(resolution,[status(thm)],[c667,c80]) ).
cnf(c814,plain,
( iLEQ(suc(X305),suc(X305))
| 'LE'(f(X305),'0')
| ~ 'E'('0',f(suc(suc(suc(X305)))))
| ~ 'E'('0',f(suc(X305)))
| ~ 'E'('0',f(suc(suc(X305))))
| ~ 'E'('0',f(X305))
| ~ 'E'(f(X305),f(suc(X305))) ),
inference(resolution,[status(thm)],[c677,c354]) ).
cnf(c826,plain,
( iLEQ(suc(X306),suc(X306))
| 'LE'(f(X306),'0')
| ~ 'E'('0',f(suc(X306)))
| ~ 'E'('0',f(suc(suc(X306))))
| ~ 'E'('0',f(X306))
| ~ 'E'(f(X306),f(suc(X306))) ),
inference(resolution,[status(thm)],[c814,c6]) ).
cnf(c829,plain,
( iLEQ(suc(X308),suc(X308))
| 'LE'(f(X308),'0')
| ~ 'E'('0',f(suc(X308)))
| ~ 'E'('0',f(suc(suc(X308))))
| ~ 'E'('0',f(X308)) ),
inference(resolution,[status(thm)],[c826,c132]) ).
cnf(c839,plain,
( iLEQ(suc(X309),suc(X309))
| 'LE'(f(X309),'0')
| ~ 'E'('0',f(suc(X309)))
| ~ 'E'('0',f(X309)) ),
inference(resolution,[status(thm)],[c829,c4]) ).
cnf(c850,plain,
( iLEQ(suc(X310),suc(X310))
| 'LE'(f(X310),'0')
| ~ 'E'('0',f(X310)) ),
inference(resolution,[status(thm)],[c839,c2]) ).
cnf(c858,plain,
( iLEQ(suc(X311),suc(X311))
| 'LE'(f(X311),'0') ),
inference(resolution,[status(thm)],[c850,c0]) ).
cnf(clause_90,axiom,
( ~ 'E'('0',f(suc(suc(suc(X19)))))
| ~ 'E'('0',f(suc(suc(suc(X18)))))
| ~ 'E'(f(X18),f(suc(suc(X18))))
| ~ 'E'('0',f(suc(X19)))
| ~ 'E'('0',f(suc(suc(X19))))
| ~ 'E'('0',f(X19))
| ~ 'E'('0',f(suc(X18)))
| ~ 'E'(f(X18),f(suc(X18)))
| ~ iLEQ(suc(X19),suc(X18))
| ~ 'E'('0',f(X18))
| ~ 'E'(f(X19),f(suc(suc(X19))))
| ~ 'E'(f(X19),f(suc(X19)))
| ~ 'E'('0',f(suc(suc(X18))))
| 'E'(f(X19),f(suc(suc(suc(X19)))))
| 'E'(f(X18),f(suc(suc(suc(X18))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_90) ).
cnf(c37,plain,
( ~ 'E'('0',f(suc(suc(suc(X131)))))
| ~ 'E'(f(X131),f(suc(suc(X131))))
| ~ 'E'('0',f(suc(X131)))
| ~ 'E'('0',f(suc(suc(X131))))
| ~ 'E'('0',f(X131))
| ~ 'E'(f(X131),f(suc(X131)))
| ~ iLEQ(suc(X131),suc(X131))
| 'E'(f(X131),f(suc(suc(suc(X131))))) ),
inference(factor,[status(thm)],[clause_90]) ).
cnf(c375,plain,
( ~ 'E'('0',f(suc(suc(suc(X351)))))
| ~ 'E'('0',f(suc(X351)))
| ~ 'E'('0',f(suc(suc(X351))))
| ~ 'E'('0',f(X351))
| ~ 'E'(f(X351),f(suc(X351)))
| ~ iLEQ(suc(X351),suc(X351))
| 'E'(f(X351),f(suc(suc(suc(X351)))))
| 'LE'(f(X351),'0') ),
inference(resolution,[status(thm)],[c37,c354]) ).
cnf(c907,plain,
( ~ 'E'('0',f(suc(X354)))
| ~ 'E'('0',f(suc(suc(X354))))
| ~ 'E'('0',f(X354))
| ~ 'E'(f(X354),f(suc(X354)))
| ~ iLEQ(suc(X354),suc(X354))
| 'E'(f(X354),f(suc(suc(suc(X354)))))
| 'LE'(f(X354),'0') ),
inference(resolution,[status(thm)],[c375,c6]) ).
cnf(c910,plain,
( ~ 'E'('0',f(suc(X355)))
| ~ 'E'('0',f(suc(suc(X355))))
| ~ 'E'('0',f(X355))
| ~ iLEQ(suc(X355),suc(X355))
| 'E'(f(X355),f(suc(suc(suc(X355)))))
| 'LE'(f(X355),'0') ),
inference(resolution,[status(thm)],[c907,c132]) ).
cnf(c918,plain,
( ~ 'E'('0',f(suc(X356)))
| ~ 'E'('0',f(X356))
| ~ iLEQ(suc(X356),suc(X356))
| 'E'(f(X356),f(suc(suc(suc(X356)))))
| 'LE'(f(X356),'0') ),
inference(resolution,[status(thm)],[c910,c4]) ).
cnf(c929,plain,
( ~ 'E'('0',f(suc(X357)))
| ~ 'E'('0',f(X357))
| 'E'(f(X357),f(suc(suc(suc(X357)))))
| 'LE'(f(X357),'0') ),
inference(resolution,[status(thm)],[c918,c858]) ).
cnf(c935,plain,
( ~ 'E'('0',f(X358))
| 'E'(f(X358),f(suc(suc(suc(X358)))))
| 'LE'(f(X358),'0') ),
inference(resolution,[status(thm)],[c929,c2]) ).
cnf(c943,plain,
( 'E'(f(X360),f(suc(suc(suc(X360)))))
| 'LE'(f(X360),'0') ),
inference(resolution,[status(thm)],[c935,c0]) ).
cnf(clause_145,axiom,
( ~ 'E'('0',f(suc(suc(suc(X69)))))
| ~ 'E'('0',f(suc(suc(suc(X68)))))
| ~ 'E'(f(X68),f(suc(suc(X68))))
| ~ 'E'('0',f(suc(X69)))
| ~ 'E'(f(X69),f(suc(suc(suc(X69)))))
| ~ 'E'('0',f(suc(suc(X69))))
| ~ 'E'('0',f(X69))
| ~ 'E'('0',f(suc(X68)))
| ~ 'E'('0',f(suc(suc(suc(suc(X68))))))
| ~ 'E'(f(X68),f(suc(X68)))
| ~ iLEQ(suc(X69),suc(X68))
| ~ 'E'('0',f(X68))
| ~ 'E'(f(X69),f(suc(suc(X69))))
| ~ 'E'(f(X68),f(suc(suc(suc(X68)))))
| ~ 'E'(f(X69),f(suc(X69)))
| ~ 'E'('0',f(suc(suc(X68))))
| ~ 'E'('0',f(suc(suc(suc(suc(X69)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_145) ).
cnf(c197,plain,
( ~ 'E'('0',f(suc(suc(suc(X365)))))
| ~ 'E'(f(X365),f(suc(suc(X365))))
| ~ 'E'('0',f(suc(X365)))
| ~ 'E'(f(X365),f(suc(suc(suc(X365)))))
| ~ 'E'('0',f(suc(suc(X365))))
| ~ 'E'('0',f(X365))
| ~ 'E'('0',f(suc(suc(suc(suc(X365))))))
| ~ 'E'(f(X365),f(suc(X365)))
| ~ iLEQ(suc(X365),suc(X365)) ),
inference(factor,[status(thm)],[clause_145]) ).
cnf(c1007,plain,
( ~ 'E'('0',f(suc(suc(suc(X466)))))
| ~ 'E'(f(X466),f(suc(suc(X466))))
| ~ 'E'('0',f(suc(X466)))
| ~ 'E'(f(X466),f(suc(suc(suc(X466)))))
| ~ 'E'('0',f(suc(suc(X466))))
| ~ 'E'('0',f(X466))
| ~ 'E'(f(X466),f(suc(X466)))
| ~ iLEQ(suc(X466),suc(X466))
| 'LE'(f(X466),'0') ),
inference(resolution,[status(thm)],[c197,c46]) ).
cnf(c1142,plain,
( ~ 'E'('0',f(suc(suc(suc(X467)))))
| ~ 'E'(f(X467),f(suc(suc(X467))))
| ~ 'E'('0',f(suc(X467)))
| ~ 'E'('0',f(suc(suc(X467))))
| ~ 'E'('0',f(X467))
| ~ 'E'(f(X467),f(suc(X467)))
| ~ iLEQ(suc(X467),suc(X467))
| 'LE'(f(X467),'0') ),
inference(resolution,[status(thm)],[c1007,c943]) ).
cnf(c1144,plain,
( ~ 'E'('0',f(suc(suc(suc(X469)))))
| ~ 'E'('0',f(suc(X469)))
| ~ 'E'('0',f(suc(suc(X469))))
| ~ 'E'('0',f(X469))
| ~ 'E'(f(X469),f(suc(X469)))
| ~ iLEQ(suc(X469),suc(X469))
| 'LE'(f(X469),'0') ),
inference(resolution,[status(thm)],[c1142,c354]) ).
cnf(c1156,plain,
( ~ 'E'('0',f(suc(X470)))
| ~ 'E'('0',f(suc(suc(X470))))
| ~ 'E'('0',f(X470))
| ~ 'E'(f(X470),f(suc(X470)))
| ~ iLEQ(suc(X470),suc(X470))
| 'LE'(f(X470),'0') ),
inference(resolution,[status(thm)],[c1144,c6]) ).
cnf(c1159,plain,
( ~ 'E'('0',f(suc(X471)))
| ~ 'E'('0',f(suc(suc(X471))))
| ~ 'E'('0',f(X471))
| ~ iLEQ(suc(X471),suc(X471))
| 'LE'(f(X471),'0') ),
inference(resolution,[status(thm)],[c1156,c132]) ).
cnf(c1167,plain,
( ~ 'E'('0',f(suc(X472)))
| ~ 'E'('0',f(X472))
| ~ iLEQ(suc(X472),suc(X472))
| 'LE'(f(X472),'0') ),
inference(resolution,[status(thm)],[c1159,c4]) ).
cnf(c1176,plain,
( ~ 'E'('0',f(suc(X473)))
| ~ 'E'('0',f(X473))
| 'LE'(f(X473),'0') ),
inference(resolution,[status(thm)],[c1167,c858]) ).
cnf(c1180,plain,
( ~ 'E'('0',f(X475))
| 'LE'(f(X475),'0') ),
inference(resolution,[status(thm)],[c1176,c2]) ).
cnf(c1188,plain,
'LE'(f(X476),'0'),
inference(resolution,[status(thm)],[c1180,c0]) ).
cnf(c1196,plain,
$false,
inference(resolution,[status(thm)],[c1188,clause_160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO648-1 : TPTP v8.1.2. Released v7.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n010.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 17:58:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 3.49/3.74 % Version: 1.5
% 3.49/3.74 % SZS status Unsatisfiable
% 3.49/3.74 % SZS output start CNFRefutation
% See solution above
% 3.49/3.74
% 3.49/3.74 % Initial clauses : 27
% 3.49/3.74 % Processed clauses : 229
% 3.49/3.74 % Factors computed : 40
% 3.49/3.74 % Resolvents computed: 1157
% 3.49/3.74 % Tautologies deleted: 1
% 3.49/3.74 % Forward subsumed : 504
% 3.49/3.74 % Backward subsumed : 168
% 3.49/3.74 % -------- CPU Time ---------
% 3.49/3.74 % User time : 3.355 s
% 3.49/3.74 % System time : 0.017 s
% 3.49/3.74 % Total time : 3.372 s
%------------------------------------------------------------------------------