%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO649-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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 20.86s 21.07s
% Output : Refutation 20.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 18
% Syntax : Number of clauses : 94 ( 4 unt; 74 nHn; 77 RR)
% Number of literals : 539 ( 0 equ; 354 neg)
% Maximal clause size : 21 ( 5 avg)
% Maximal term depth : 7 ( 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 : 97 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_716,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_716) ).
cnf(clause_1382,axiom,
'LE'(f(X2),s('0')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1382) ).
cnf(clause_314,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_314) ).
cnf(c0,plain,
( 'E'('0',f(X4))
| 'LE'(f(X4),'0') ),
inference(resolution,[status(thm)],[clause_314,clause_1382]) ).
cnf(clause_1518,axiom,
( ~ 'LE'(f(suc(X7)),s('0'))
| 'E'('0',f(suc(X7)))
| 'LE'(f(X7),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1518) ).
cnf(c8,plain,
( 'E'('0',f(suc(X8)))
| 'LE'(f(X8),'0') ),
inference(resolution,[status(thm)],[clause_1518,clause_1382]) ).
cnf(clause_519,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_519) ).
cnf(c11,plain,
( 'E'('0',f(suc(suc(X10))))
| 'LE'(f(X10),'0') ),
inference(resolution,[status(thm)],[clause_519,clause_1382]) ).
cnf(clause_258,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_258) ).
cnf(c23,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_258,c8]) ).
cnf(c38,plain,
( 'E'(f(X17),f(suc(X17)))
| iLEQ(suc(X17),suc(X17))
| 'LE'(f(X17),'0') ),
inference(resolution,[status(thm)],[c23,c0]) ).
cnf(clause_771,axiom,
( ~ 'E'('0',f(suc(X42)))
| ~ 'E'('0',f(X42))
| ~ 'E'('0',f(suc(X41)))
| ~ iLEQ(suc(X42),suc(X41))
| ~ 'E'('0',f(X41))
| 'E'(f(X42),f(suc(X42)))
| 'E'(f(X41),f(suc(X41))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_771) ).
cnf(c117,plain,
( ~ 'E'('0',f(suc(X45)))
| ~ 'E'('0',f(X45))
| 'E'(f(X45),f(suc(X45)))
| 'LE'(f(X45),'0') ),
inference(resolution,[status(thm)],[clause_771,c38]) ).
cnf(c134,plain,
( ~ 'E'('0',f(X46))
| 'E'(f(X46),f(suc(X46)))
| 'LE'(f(X46),'0') ),
inference(resolution,[status(thm)],[c117,c8]) ).
cnf(c147,plain,
( 'E'(f(X47),f(suc(X47)))
| 'LE'(f(X47),'0') ),
inference(resolution,[status(thm)],[c134,c0]) ).
cnf(clause_1214,axiom,
( ~ 'LE'(f(suc(suc(suc(X22)))),s('0'))
| 'E'('0',f(suc(suc(suc(X22)))))
| 'LE'(f(X22),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1214) ).
cnf(c47,plain,
( 'E'('0',f(suc(suc(suc(X23)))))
| 'LE'(f(X23),'0') ),
inference(resolution,[status(thm)],[clause_1214,clause_1382]) ).
cnf(clause_1172,axiom,
( ~ 'E'('0',f(suc(suc(X65))))
| ~ 'E'('0',f(suc(X65)))
| ~ 'E'(f(X65),f(suc(X65)))
| ~ 'E'('0',f(X65))
| 'E'(f(X65),f(suc(suc(X65))))
| iLEQ(suc(X65),suc(X65)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1172) ).
cnf(c203,plain,
( ~ 'E'('0',f(suc(suc(X119))))
| ~ 'E'('0',f(suc(X119)))
| ~ 'E'('0',f(X119))
| 'E'(f(X119),f(suc(suc(X119))))
| iLEQ(suc(X119),suc(X119))
| 'LE'(f(X119),'0') ),
inference(resolution,[status(thm)],[clause_1172,c147]) ).
cnf(c322,plain,
( ~ 'E'('0',f(suc(X120)))
| ~ 'E'('0',f(X120))
| 'E'(f(X120),f(suc(suc(X120))))
| iLEQ(suc(X120),suc(X120))
| 'LE'(f(X120),'0') ),
inference(resolution,[status(thm)],[c203,c11]) ).
cnf(c335,plain,
( ~ 'E'('0',f(X121))
| 'E'(f(X121),f(suc(suc(X121))))
| iLEQ(suc(X121),suc(X121))
| 'LE'(f(X121),'0') ),
inference(resolution,[status(thm)],[c322,c8]) ).
cnf(c347,plain,
( 'E'(f(X122),f(suc(suc(X122))))
| iLEQ(suc(X122),suc(X122))
| 'LE'(f(X122),'0') ),
inference(resolution,[status(thm)],[c335,c0]) ).
cnf(clause_375,axiom,
( ~ 'E'('0',f(suc(X12)))
| ~ 'E'('0',f(suc(suc(X12))))
| ~ 'E'('0',f(X12))
| ~ 'E'('0',f(suc(X11)))
| ~ 'E'(f(X11),f(suc(X11)))
| ~ iLEQ(suc(X12),suc(X11))
| ~ 'E'('0',f(X11))
| ~ 'E'(f(X12),f(suc(X12)))
| ~ 'E'('0',f(suc(suc(X11))))
| 'E'(f(X12),f(suc(suc(X12))))
| 'E'(f(X11),f(suc(suc(X11)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_375) ).
cnf(c15,plain,
( ~ 'E'('0',f(suc(X136)))
| ~ 'E'('0',f(suc(suc(X136))))
| ~ 'E'('0',f(X136))
| ~ 'E'(f(X136),f(suc(X136)))
| ~ iLEQ(suc(X136),suc(X136))
| 'E'(f(X136),f(suc(suc(X136)))) ),
inference(factor,[status(thm)],[clause_375]) ).
cnf(c374,plain,
( ~ 'E'('0',f(suc(X141)))
| ~ 'E'('0',f(suc(suc(X141))))
| ~ 'E'('0',f(X141))
| ~ iLEQ(suc(X141),suc(X141))
| 'E'(f(X141),f(suc(suc(X141))))
| 'LE'(f(X141),'0') ),
inference(resolution,[status(thm)],[c15,c147]) ).
cnf(c393,plain,
( ~ 'E'('0',f(suc(X142)))
| ~ 'E'('0',f(X142))
| ~ iLEQ(suc(X142),suc(X142))
| 'E'(f(X142),f(suc(suc(X142))))
| 'LE'(f(X142),'0') ),
inference(resolution,[status(thm)],[c374,c11]) ).
cnf(c403,plain,
( ~ 'E'('0',f(suc(X143)))
| ~ 'E'('0',f(X143))
| 'E'(f(X143),f(suc(suc(X143))))
| 'LE'(f(X143),'0') ),
inference(resolution,[status(thm)],[c393,c347]) ).
cnf(c407,plain,
( ~ 'E'('0',f(X144))
| 'E'(f(X144),f(suc(suc(X144))))
| 'LE'(f(X144),'0') ),
inference(resolution,[status(thm)],[c403,c8]) ).
cnf(c419,plain,
( 'E'(f(X147),f(suc(suc(X147))))
| 'LE'(f(X147),'0') ),
inference(resolution,[status(thm)],[c407,c0]) ).
cnf(clause_1514,axiom,
( ~ 'E'('0',f(suc(suc(suc(X117)))))
| ~ 'E'('0',f(suc(X117)))
| ~ 'E'('0',f(suc(suc(X117))))
| ~ 'E'('0',f(X117))
| ~ 'E'(f(X117),f(suc(suc(X117))))
| ~ 'E'(f(X117),f(suc(X117)))
| 'E'(f(X117),f(suc(suc(suc(X117)))))
| iLEQ(suc(X117),suc(X117)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1514) ).
cnf(c355,plain,
( iLEQ(suc(X318),suc(X318))
| 'LE'(f(X318),'0')
| ~ 'E'('0',f(suc(suc(suc(X318)))))
| ~ 'E'('0',f(suc(X318)))
| ~ 'E'('0',f(suc(suc(X318))))
| ~ 'E'('0',f(X318))
| ~ 'E'(f(X318),f(suc(X318)))
| 'E'(f(X318),f(suc(suc(suc(X318))))) ),
inference(resolution,[status(thm)],[c347,clause_1514]) ).
cnf(c847,plain,
( iLEQ(suc(X321),suc(X321))
| 'LE'(f(X321),'0')
| ~ 'E'('0',f(suc(X321)))
| ~ 'E'('0',f(suc(suc(X321))))
| ~ 'E'('0',f(X321))
| ~ 'E'(f(X321),f(suc(X321)))
| 'E'(f(X321),f(suc(suc(suc(X321))))) ),
inference(resolution,[status(thm)],[c355,c47]) ).
cnf(c858,plain,
( iLEQ(suc(X322),suc(X322))
| 'LE'(f(X322),'0')
| ~ 'E'('0',f(suc(X322)))
| ~ 'E'('0',f(suc(suc(X322))))
| ~ 'E'('0',f(X322))
| 'E'(f(X322),f(suc(suc(suc(X322))))) ),
inference(resolution,[status(thm)],[c847,c147]) ).
cnf(c863,plain,
( iLEQ(suc(X323),suc(X323))
| 'LE'(f(X323),'0')
| ~ 'E'('0',f(suc(X323)))
| ~ 'E'('0',f(X323))
| 'E'(f(X323),f(suc(suc(suc(X323))))) ),
inference(resolution,[status(thm)],[c858,c11]) ).
cnf(c876,plain,
( iLEQ(suc(X324),suc(X324))
| 'LE'(f(X324),'0')
| ~ 'E'('0',f(X324))
| 'E'(f(X324),f(suc(suc(suc(X324))))) ),
inference(resolution,[status(thm)],[c863,c8]) ).
cnf(c888,plain,
( iLEQ(suc(X325),suc(X325))
| 'LE'(f(X325),'0')
| 'E'(f(X325),f(suc(suc(suc(X325))))) ),
inference(resolution,[status(thm)],[c876,c0]) ).
cnf(clause_412,axiom,
( ~ 'E'('0',f(suc(suc(suc(X101)))))
| ~ 'E'('0',f(suc(suc(suc(X100)))))
| ~ 'E'(f(X100),f(suc(suc(X100))))
| ~ 'E'('0',f(suc(X101)))
| ~ 'E'('0',f(suc(suc(X101))))
| ~ 'E'('0',f(X101))
| ~ 'E'('0',f(suc(X100)))
| ~ 'E'(f(X100),f(suc(X100)))
| ~ iLEQ(suc(X101),suc(X100))
| ~ 'E'('0',f(X100))
| ~ 'E'(f(X101),f(suc(suc(X101))))
| ~ 'E'(f(X101),f(suc(X101)))
| ~ 'E'('0',f(suc(suc(X100))))
| 'E'(f(X101),f(suc(suc(suc(X101)))))
| 'E'(f(X100),f(suc(suc(suc(X100))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_412) ).
cnf(c308,plain,
( ~ 'E'('0',f(suc(suc(suc(X437)))))
| ~ 'E'(f(X437),f(suc(suc(X437))))
| ~ 'E'('0',f(suc(X437)))
| ~ 'E'('0',f(suc(suc(X437))))
| ~ 'E'('0',f(X437))
| ~ 'E'(f(X437),f(suc(X437)))
| ~ iLEQ(suc(X437),suc(X437))
| 'E'(f(X437),f(suc(suc(suc(X437))))) ),
inference(factor,[status(thm)],[clause_412]) ).
cnf(c1135,plain,
( ~ 'E'('0',f(suc(suc(suc(X439)))))
| ~ 'E'('0',f(suc(X439)))
| ~ 'E'('0',f(suc(suc(X439))))
| ~ 'E'('0',f(X439))
| ~ 'E'(f(X439),f(suc(X439)))
| ~ iLEQ(suc(X439),suc(X439))
| 'E'(f(X439),f(suc(suc(suc(X439)))))
| 'LE'(f(X439),'0') ),
inference(resolution,[status(thm)],[c308,c419]) ).
cnf(c1144,plain,
( ~ 'E'('0',f(suc(X440)))
| ~ 'E'('0',f(suc(suc(X440))))
| ~ 'E'('0',f(X440))
| ~ 'E'(f(X440),f(suc(X440)))
| ~ iLEQ(suc(X440),suc(X440))
| 'E'(f(X440),f(suc(suc(suc(X440)))))
| 'LE'(f(X440),'0') ),
inference(resolution,[status(thm)],[c1135,c47]) ).
cnf(c1155,plain,
( ~ 'E'('0',f(suc(X441)))
| ~ 'E'('0',f(suc(suc(X441))))
| ~ 'E'('0',f(X441))
| ~ iLEQ(suc(X441),suc(X441))
| 'E'(f(X441),f(suc(suc(suc(X441)))))
| 'LE'(f(X441),'0') ),
inference(resolution,[status(thm)],[c1144,c147]) ).
cnf(c1160,plain,
( ~ 'E'('0',f(suc(X442)))
| ~ 'E'('0',f(X442))
| ~ iLEQ(suc(X442),suc(X442))
| 'E'(f(X442),f(suc(suc(suc(X442)))))
| 'LE'(f(X442),'0') ),
inference(resolution,[status(thm)],[c1155,c11]) ).
cnf(c1170,plain,
( ~ 'E'('0',f(suc(X443)))
| ~ 'E'('0',f(X443))
| 'E'(f(X443),f(suc(suc(suc(X443)))))
| 'LE'(f(X443),'0') ),
inference(resolution,[status(thm)],[c1160,c888]) ).
cnf(c1177,plain,
( ~ 'E'('0',f(X445))
| 'E'(f(X445),f(suc(suc(suc(X445)))))
| 'LE'(f(X445),'0') ),
inference(resolution,[status(thm)],[c1170,c8]) ).
cnf(c1189,plain,
( 'E'(f(X446),f(suc(suc(suc(X446)))))
| 'LE'(f(X446),'0') ),
inference(resolution,[status(thm)],[c1177,c0]) ).
cnf(clause_1033,axiom,
( ~ 'LE'(f(suc(suc(suc(suc(X25))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(X25))))))
| 'LE'(f(X25),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1033) ).
cnf(c57,plain,
( 'E'('0',f(suc(suc(suc(suc(X26))))))
| 'LE'(f(X26),'0') ),
inference(resolution,[status(thm)],[clause_1033,clause_1382]) ).
cnf(clause_1501,axiom,
( ~ 'E'('0',f(suc(suc(suc(X51)))))
| ~ 'E'('0',f(suc(X51)))
| ~ 'E'(f(X51),f(suc(suc(suc(X51)))))
| ~ 'E'('0',f(suc(suc(X51))))
| ~ 'E'('0',f(X51))
| ~ 'E'(f(X51),f(suc(suc(X51))))
| ~ 'E'(f(X51),f(suc(X51)))
| ~ 'E'('0',f(suc(suc(suc(suc(X51))))))
| 'E'(f(X51),f(suc(suc(suc(suc(X51))))))
| iLEQ(suc(X51),suc(X51)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1501) ).
cnf(c153,plain,
( ~ 'E'('0',f(suc(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'(f(X365),f(suc(suc(X365))))
| ~ 'E'(f(X365),f(suc(X365)))
| 'E'(f(X365),f(suc(suc(suc(suc(X365))))))
| iLEQ(suc(X365),suc(X365))
| 'LE'(f(X365),'0') ),
inference(resolution,[status(thm)],[clause_1501,c57]) ).
cnf(c984,plain,
( ~ 'E'('0',f(suc(suc(suc(X522)))))
| ~ 'E'('0',f(suc(X522)))
| ~ 'E'('0',f(suc(suc(X522))))
| ~ 'E'('0',f(X522))
| ~ 'E'(f(X522),f(suc(suc(X522))))
| ~ 'E'(f(X522),f(suc(X522)))
| 'E'(f(X522),f(suc(suc(suc(suc(X522))))))
| iLEQ(suc(X522),suc(X522))
| 'LE'(f(X522),'0') ),
inference(resolution,[status(thm)],[c153,c888]) ).
cnf(c1334,plain,
( ~ 'E'('0',f(suc(suc(suc(X524)))))
| ~ 'E'('0',f(suc(X524)))
| ~ 'E'('0',f(suc(suc(X524))))
| ~ 'E'('0',f(X524))
| ~ 'E'(f(X524),f(suc(X524)))
| 'E'(f(X524),f(suc(suc(suc(suc(X524))))))
| iLEQ(suc(X524),suc(X524))
| 'LE'(f(X524),'0') ),
inference(resolution,[status(thm)],[c984,c419]) ).
cnf(c1343,plain,
( ~ 'E'('0',f(suc(X525)))
| ~ 'E'('0',f(suc(suc(X525))))
| ~ 'E'('0',f(X525))
| ~ 'E'(f(X525),f(suc(X525)))
| 'E'(f(X525),f(suc(suc(suc(suc(X525))))))
| iLEQ(suc(X525),suc(X525))
| 'LE'(f(X525),'0') ),
inference(resolution,[status(thm)],[c1334,c47]) ).
cnf(c1354,plain,
( ~ 'E'('0',f(suc(X526)))
| ~ 'E'('0',f(suc(suc(X526))))
| ~ 'E'('0',f(X526))
| 'E'(f(X526),f(suc(suc(suc(suc(X526))))))
| iLEQ(suc(X526),suc(X526))
| 'LE'(f(X526),'0') ),
inference(resolution,[status(thm)],[c1343,c147]) ).
cnf(c1359,plain,
( ~ 'E'('0',f(suc(X527)))
| ~ 'E'('0',f(X527))
| 'E'(f(X527),f(suc(suc(suc(suc(X527))))))
| iLEQ(suc(X527),suc(X527))
| 'LE'(f(X527),'0') ),
inference(resolution,[status(thm)],[c1354,c11]) ).
cnf(c1372,plain,
( ~ 'E'('0',f(X528))
| 'E'(f(X528),f(suc(suc(suc(suc(X528))))))
| iLEQ(suc(X528),suc(X528))
| 'LE'(f(X528),'0') ),
inference(resolution,[status(thm)],[c1359,c8]) ).
cnf(c1384,plain,
( 'E'(f(X530),f(suc(suc(suc(suc(X530))))))
| iLEQ(suc(X530),suc(X530))
| 'LE'(f(X530),'0') ),
inference(resolution,[status(thm)],[c1372,c0]) ).
cnf(clause_102,axiom,
( ~ 'E'('0',f(suc(suc(suc(X112)))))
| ~ 'E'('0',f(suc(suc(suc(X111)))))
| ~ 'E'(f(X111),f(suc(suc(X111))))
| ~ 'E'('0',f(suc(X112)))
| ~ 'E'(f(X112),f(suc(suc(suc(X112)))))
| ~ 'E'('0',f(suc(suc(X112))))
| ~ 'E'('0',f(X112))
| ~ 'E'('0',f(suc(X111)))
| ~ 'E'('0',f(suc(suc(suc(suc(X111))))))
| ~ 'E'(f(X111),f(suc(X111)))
| ~ iLEQ(suc(X112),suc(X111))
| ~ 'E'('0',f(X111))
| ~ 'E'(f(X112),f(suc(suc(X112))))
| ~ 'E'(f(X111),f(suc(suc(suc(X111)))))
| ~ 'E'(f(X112),f(suc(X112)))
| ~ 'E'('0',f(suc(suc(X111))))
| ~ 'E'('0',f(suc(suc(suc(suc(X112))))))
| 'E'(f(X112),f(suc(suc(suc(suc(X112))))))
| 'E'(f(X111),f(suc(suc(suc(suc(X111)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_102) ).
cnf(c311,plain,
( ~ 'E'('0',f(suc(suc(suc(X661)))))
| ~ 'E'(f(X661),f(suc(suc(X661))))
| ~ 'E'('0',f(suc(X661)))
| ~ 'E'(f(X661),f(suc(suc(suc(X661)))))
| ~ 'E'('0',f(suc(suc(X661))))
| ~ 'E'('0',f(X661))
| ~ 'E'('0',f(suc(suc(suc(suc(X661))))))
| ~ 'E'(f(X661),f(suc(X661)))
| ~ iLEQ(suc(X661),suc(X661))
| 'E'(f(X661),f(suc(suc(suc(suc(X661)))))) ),
inference(factor,[status(thm)],[clause_102]) ).
cnf(c1760,plain,
( ~ 'E'('0',f(suc(suc(suc(X782)))))
| ~ 'E'(f(X782),f(suc(suc(X782))))
| ~ 'E'('0',f(suc(X782)))
| ~ 'E'(f(X782),f(suc(suc(suc(X782)))))
| ~ 'E'('0',f(suc(suc(X782))))
| ~ 'E'('0',f(X782))
| ~ 'E'(f(X782),f(suc(X782)))
| ~ iLEQ(suc(X782),suc(X782))
| 'E'(f(X782),f(suc(suc(suc(suc(X782))))))
| 'LE'(f(X782),'0') ),
inference(resolution,[status(thm)],[c311,c57]) ).
cnf(c1978,plain,
( ~ 'E'('0',f(suc(suc(suc(X783)))))
| ~ 'E'(f(X783),f(suc(suc(X783))))
| ~ 'E'('0',f(suc(X783)))
| ~ 'E'('0',f(suc(suc(X783))))
| ~ 'E'('0',f(X783))
| ~ 'E'(f(X783),f(suc(X783)))
| ~ iLEQ(suc(X783),suc(X783))
| 'E'(f(X783),f(suc(suc(suc(suc(X783))))))
| 'LE'(f(X783),'0') ),
inference(resolution,[status(thm)],[c1760,c1189]) ).
cnf(c1981,plain,
( ~ 'E'('0',f(suc(suc(suc(X784)))))
| ~ 'E'('0',f(suc(X784)))
| ~ 'E'('0',f(suc(suc(X784))))
| ~ 'E'('0',f(X784))
| ~ 'E'(f(X784),f(suc(X784)))
| ~ iLEQ(suc(X784),suc(X784))
| 'E'(f(X784),f(suc(suc(suc(suc(X784))))))
| 'LE'(f(X784),'0') ),
inference(resolution,[status(thm)],[c1978,c419]) ).
cnf(c1992,plain,
( ~ 'E'('0',f(suc(X785)))
| ~ 'E'('0',f(suc(suc(X785))))
| ~ 'E'('0',f(X785))
| ~ 'E'(f(X785),f(suc(X785)))
| ~ iLEQ(suc(X785),suc(X785))
| 'E'(f(X785),f(suc(suc(suc(suc(X785))))))
| 'LE'(f(X785),'0') ),
inference(resolution,[status(thm)],[c1981,c47]) ).
cnf(c2003,plain,
( ~ 'E'('0',f(suc(X787)))
| ~ 'E'('0',f(suc(suc(X787))))
| ~ 'E'('0',f(X787))
| ~ iLEQ(suc(X787),suc(X787))
| 'E'(f(X787),f(suc(suc(suc(suc(X787))))))
| 'LE'(f(X787),'0') ),
inference(resolution,[status(thm)],[c1992,c147]) ).
cnf(c2008,plain,
( ~ 'E'('0',f(suc(X788)))
| ~ 'E'('0',f(X788))
| ~ iLEQ(suc(X788),suc(X788))
| 'E'(f(X788),f(suc(suc(suc(suc(X788))))))
| 'LE'(f(X788),'0') ),
inference(resolution,[status(thm)],[c2003,c11]) ).
cnf(c2019,plain,
( ~ 'E'('0',f(suc(X789)))
| ~ 'E'('0',f(X789))
| 'E'(f(X789),f(suc(suc(suc(suc(X789))))))
| 'LE'(f(X789),'0') ),
inference(resolution,[status(thm)],[c2008,c1384]) ).
cnf(c2023,plain,
( ~ 'E'('0',f(X790))
| 'E'(f(X790),f(suc(suc(suc(suc(X790))))))
| 'LE'(f(X790),'0') ),
inference(resolution,[status(thm)],[c2019,c8]) ).
cnf(c2035,plain,
( 'E'(f(X791),f(suc(suc(suc(suc(X791))))))
| 'LE'(f(X791),'0') ),
inference(resolution,[status(thm)],[c2023,c0]) ).
cnf(clause_62,axiom,
( ~ 'LE'(f(suc(suc(suc(suc(suc(X27)))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(suc(X27)))))))
| 'LE'(f(X27),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_62) ).
cnf(c71,plain,
( 'E'('0',f(suc(suc(suc(suc(suc(X28)))))))
| 'LE'(f(X28),'0') ),
inference(resolution,[status(thm)],[clause_62,clause_1382]) ).
cnf(clause_1046,axiom,
( ~ 'E'('0',f(suc(suc(suc(X70)))))
| ~ 'E'('0',f(suc(suc(suc(X69)))))
| ~ 'E'(f(X69),f(suc(suc(X69))))
| ~ 'E'('0',f(suc(X70)))
| ~ 'E'(f(X70),f(suc(suc(suc(X70)))))
| ~ 'E'('0',f(suc(suc(X70))))
| ~ 'E'('0',f(X70))
| ~ 'E'('0',f(suc(X69)))
| ~ 'E'('0',f(suc(suc(suc(suc(X69))))))
| ~ 'E'(f(X69),f(suc(suc(suc(suc(X69))))))
| ~ 'E'(f(X69),f(suc(X69)))
| ~ iLEQ(suc(X70),suc(X69))
| ~ 'E'('0',f(X69))
| ~ 'E'(f(X70),f(suc(suc(X70))))
| ~ 'E'(f(X69),f(suc(suc(suc(X69)))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X70)))))))
| ~ 'E'(f(X70),f(suc(X70)))
| ~ 'E'(f(X70),f(suc(suc(suc(suc(X70))))))
| ~ 'E'('0',f(suc(suc(X69))))
| ~ 'E'('0',f(suc(suc(suc(suc(X70))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X69))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1046) ).
cnf(c211,plain,
( ~ 'E'('0',f(suc(suc(suc(X454)))))
| ~ 'E'(f(X454),f(suc(suc(X454))))
| ~ 'E'('0',f(suc(X454)))
| ~ 'E'(f(X454),f(suc(suc(suc(X454)))))
| ~ 'E'('0',f(suc(suc(X454))))
| ~ 'E'('0',f(X454))
| ~ 'E'('0',f(suc(suc(suc(suc(X454))))))
| ~ 'E'(f(X454),f(suc(suc(suc(suc(X454))))))
| ~ 'E'(f(X454),f(suc(X454)))
| ~ iLEQ(suc(X454),suc(X454))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X454))))))) ),
inference(factor,[status(thm)],[clause_1046]) ).
cnf(c1255,plain,
( ~ 'E'('0',f(suc(suc(suc(X1136)))))
| ~ 'E'(f(X1136),f(suc(suc(X1136))))
| ~ 'E'('0',f(suc(X1136)))
| ~ 'E'(f(X1136),f(suc(suc(suc(X1136)))))
| ~ 'E'('0',f(suc(suc(X1136))))
| ~ 'E'('0',f(X1136))
| ~ 'E'('0',f(suc(suc(suc(suc(X1136))))))
| ~ 'E'(f(X1136),f(suc(suc(suc(suc(X1136))))))
| ~ 'E'(f(X1136),f(suc(X1136)))
| ~ iLEQ(suc(X1136),suc(X1136))
| 'LE'(f(X1136),'0') ),
inference(resolution,[status(thm)],[c211,c71]) ).
cnf(c2791,plain,
( ~ 'E'('0',f(suc(suc(suc(X1137)))))
| ~ 'E'(f(X1137),f(suc(suc(X1137))))
| ~ 'E'('0',f(suc(X1137)))
| ~ 'E'(f(X1137),f(suc(suc(suc(X1137)))))
| ~ 'E'('0',f(suc(suc(X1137))))
| ~ 'E'('0',f(X1137))
| ~ 'E'('0',f(suc(suc(suc(suc(X1137))))))
| ~ 'E'(f(X1137),f(suc(X1137)))
| ~ iLEQ(suc(X1137),suc(X1137))
| 'LE'(f(X1137),'0') ),
inference(resolution,[status(thm)],[c1255,c2035]) ).
cnf(c2798,plain,
( ~ 'E'('0',f(suc(suc(suc(X1140)))))
| ~ 'E'(f(X1140),f(suc(suc(X1140))))
| ~ 'E'('0',f(suc(X1140)))
| ~ 'E'(f(X1140),f(suc(suc(suc(X1140)))))
| ~ 'E'('0',f(suc(suc(X1140))))
| ~ 'E'('0',f(X1140))
| ~ 'E'(f(X1140),f(suc(X1140)))
| ~ iLEQ(suc(X1140),suc(X1140))
| 'LE'(f(X1140),'0') ),
inference(resolution,[status(thm)],[c2791,c57]) ).
cnf(c2805,plain,
( ~ 'E'('0',f(suc(suc(suc(X1141)))))
| ~ 'E'(f(X1141),f(suc(suc(X1141))))
| ~ 'E'('0',f(suc(X1141)))
| ~ 'E'('0',f(suc(suc(X1141))))
| ~ 'E'('0',f(X1141))
| ~ 'E'(f(X1141),f(suc(X1141)))
| ~ iLEQ(suc(X1141),suc(X1141))
| 'LE'(f(X1141),'0') ),
inference(resolution,[status(thm)],[c2798,c1189]) ).
cnf(c2808,plain,
( ~ 'E'('0',f(suc(suc(suc(X1142)))))
| ~ 'E'('0',f(suc(X1142)))
| ~ 'E'('0',f(suc(suc(X1142))))
| ~ 'E'('0',f(X1142))
| ~ 'E'(f(X1142),f(suc(X1142)))
| ~ iLEQ(suc(X1142),suc(X1142))
| 'LE'(f(X1142),'0') ),
inference(resolution,[status(thm)],[c2805,c419]) ).
cnf(c2823,plain,
( ~ 'E'('0',f(suc(X1143)))
| ~ 'E'('0',f(suc(suc(X1143))))
| ~ 'E'('0',f(X1143))
| ~ 'E'(f(X1143),f(suc(X1143)))
| ~ iLEQ(suc(X1143),suc(X1143))
| 'LE'(f(X1143),'0') ),
inference(resolution,[status(thm)],[c2808,c47]) ).
cnf(c2834,plain,
( ~ 'E'('0',f(suc(X1144)))
| ~ 'E'('0',f(suc(suc(X1144))))
| ~ 'E'('0',f(X1144))
| ~ iLEQ(suc(X1144),suc(X1144))
| 'LE'(f(X1144),'0') ),
inference(resolution,[status(thm)],[c2823,c147]) ).
cnf(c2839,plain,
( ~ 'E'('0',f(suc(X1147)))
| ~ 'E'('0',f(X1147))
| ~ iLEQ(suc(X1147),suc(X1147))
| 'LE'(f(X1147),'0') ),
inference(resolution,[status(thm)],[c2834,c11]) ).
cnf(clause_1507,axiom,
( ~ 'E'('0',f(suc(suc(suc(X24)))))
| ~ 'E'('0',f(suc(X24)))
| ~ 'E'(f(X24),f(suc(suc(suc(X24)))))
| ~ 'E'('0',f(suc(suc(X24))))
| ~ 'E'('0',f(X24))
| ~ 'E'(f(X24),f(suc(suc(X24))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X24)))))))
| ~ 'E'(f(X24),f(suc(X24)))
| ~ 'E'(f(X24),f(suc(suc(suc(suc(X24))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X24))))))
| iLEQ(suc(X24),suc(X24)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1507) ).
cnf(c1413,plain,
( iLEQ(suc(X1183),suc(X1183))
| 'LE'(f(X1183),'0')
| ~ 'E'('0',f(suc(suc(suc(X1183)))))
| ~ 'E'('0',f(suc(X1183)))
| ~ 'E'(f(X1183),f(suc(suc(suc(X1183)))))
| ~ 'E'('0',f(suc(suc(X1183))))
| ~ 'E'('0',f(X1183))
| ~ 'E'(f(X1183),f(suc(suc(X1183))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X1183)))))))
| ~ 'E'(f(X1183),f(suc(X1183)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1183)))))) ),
inference(resolution,[status(thm)],[c1384,clause_1507]) ).
cnf(c2855,plain,
( iLEQ(suc(X1184),suc(X1184))
| 'LE'(f(X1184),'0')
| ~ 'E'('0',f(suc(suc(suc(X1184)))))
| ~ 'E'('0',f(suc(X1184)))
| ~ 'E'(f(X1184),f(suc(suc(suc(X1184)))))
| ~ 'E'('0',f(suc(suc(X1184))))
| ~ 'E'('0',f(X1184))
| ~ 'E'(f(X1184),f(suc(suc(X1184))))
| ~ 'E'(f(X1184),f(suc(X1184)))
| ~ 'E'('0',f(suc(suc(suc(suc(X1184)))))) ),
inference(resolution,[status(thm)],[c1413,c71]) ).
cnf(c2864,plain,
( iLEQ(suc(X1186),suc(X1186))
| 'LE'(f(X1186),'0')
| ~ 'E'('0',f(suc(suc(suc(X1186)))))
| ~ 'E'('0',f(suc(X1186)))
| ~ 'E'(f(X1186),f(suc(suc(suc(X1186)))))
| ~ 'E'('0',f(suc(suc(X1186))))
| ~ 'E'('0',f(X1186))
| ~ 'E'(f(X1186),f(suc(suc(X1186))))
| ~ 'E'(f(X1186),f(suc(X1186))) ),
inference(resolution,[status(thm)],[c2855,c57]) ).
cnf(c2871,plain,
( iLEQ(suc(X1187),suc(X1187))
| 'LE'(f(X1187),'0')
| ~ 'E'('0',f(suc(suc(suc(X1187)))))
| ~ 'E'('0',f(suc(X1187)))
| ~ 'E'('0',f(suc(suc(X1187))))
| ~ 'E'('0',f(X1187))
| ~ 'E'(f(X1187),f(suc(suc(X1187))))
| ~ 'E'(f(X1187),f(suc(X1187))) ),
inference(resolution,[status(thm)],[c2864,c1189]) ).
cnf(c2874,plain,
( iLEQ(suc(X1188),suc(X1188))
| 'LE'(f(X1188),'0')
| ~ 'E'('0',f(suc(suc(suc(X1188)))))
| ~ 'E'('0',f(suc(X1188)))
| ~ 'E'('0',f(suc(suc(X1188))))
| ~ 'E'('0',f(X1188))
| ~ 'E'(f(X1188),f(suc(X1188))) ),
inference(resolution,[status(thm)],[c2871,c419]) ).
cnf(c2889,plain,
( iLEQ(suc(X1189),suc(X1189))
| 'LE'(f(X1189),'0')
| ~ 'E'('0',f(suc(X1189)))
| ~ 'E'('0',f(suc(suc(X1189))))
| ~ 'E'('0',f(X1189))
| ~ 'E'(f(X1189),f(suc(X1189))) ),
inference(resolution,[status(thm)],[c2874,c47]) ).
cnf(c2900,plain,
( iLEQ(suc(X1190),suc(X1190))
| 'LE'(f(X1190),'0')
| ~ 'E'('0',f(suc(X1190)))
| ~ 'E'('0',f(suc(suc(X1190))))
| ~ 'E'('0',f(X1190)) ),
inference(resolution,[status(thm)],[c2889,c147]) ).
cnf(c2905,plain,
( iLEQ(suc(X1191),suc(X1191))
| 'LE'(f(X1191),'0')
| ~ 'E'('0',f(suc(X1191)))
| ~ 'E'('0',f(X1191)) ),
inference(resolution,[status(thm)],[c2900,c11]) ).
cnf(c2918,plain,
( iLEQ(suc(X1192),suc(X1192))
| 'LE'(f(X1192),'0')
| ~ 'E'('0',f(X1192)) ),
inference(resolution,[status(thm)],[c2905,c8]) ).
cnf(c2930,plain,
( iLEQ(suc(X1193),suc(X1193))
| 'LE'(f(X1193),'0') ),
inference(resolution,[status(thm)],[c2918,c0]) ).
cnf(c2938,plain,
( 'LE'(f(X1194),'0')
| ~ 'E'('0',f(suc(X1194)))
| ~ 'E'('0',f(X1194)) ),
inference(resolution,[status(thm)],[c2930,c2839]) ).
cnf(c2948,plain,
( 'LE'(f(X1195),'0')
| ~ 'E'('0',f(X1195)) ),
inference(resolution,[status(thm)],[c2938,c8]) ).
cnf(c2960,plain,
'LE'(f(X1196),'0'),
inference(resolution,[status(thm)],[c2948,c0]) ).
cnf(c2968,plain,
$false,
inference(resolution,[status(thm)],[c2960,clause_716]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYO649-1 : TPTP v8.1.2. Released v7.3.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed May 8 17:45:53 EDT 2024
% 0.13/0.36 % CPUTime :
% 20.86/21.07 % Version: 1.5
% 20.86/21.07 % SZS status Unsatisfiable
% 20.86/21.07 % SZS output start CNFRefutation
% See solution above
% 20.86/21.07
% 20.86/21.07 % Initial clauses : 38
% 20.86/21.07 % Processed clauses : 428
% 20.86/21.07 % Factors computed : 65
% 20.86/21.07 % Resolvents computed: 2904
% 20.86/21.07 % Tautologies deleted: 4
% 20.86/21.07 % Forward subsumed : 1299
% 20.86/21.07 % Backward subsumed : 323
% 20.86/21.07 % -------- CPU Time ---------
% 20.86/21.07 % User time : 20.669 s
% 20.86/21.07 % System time : 0.039 s
% 20.86/21.07 % Total time : 20.708 s
%------------------------------------------------------------------------------