%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO647-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:03 EDT 2024
% Result : Unsatisfiable 35.70s 35.89s
% Output : Refutation 35.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 7
% Syntax : Number of clauses : 48 ( 6 unt; 17 nHn; 42 RR)
% Number of literals : 437 ( 0 equ; 367 neg)
% Maximal clause size : 41 ( 9 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-1 aty)
% Number of variables : 88 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_6244,axiom,
'E'('0',f(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6244) ).
cnf(clause_6279,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X3)))
| 'E'(f(X3),f(suc(X3)))
| iLEQ(suc(X3),suc(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6279) ).
cnf(c0,plain,
( ~ 'E'('0',f(X4))
| 'E'(f(X4),f(suc(X4)))
| iLEQ(suc(X4),suc(X4)) ),
inference(resolution,[status(thm)],[clause_6279,clause_6244]) ).
cnf(c1,plain,
( 'E'(f(X5),f(suc(X5)))
| iLEQ(suc(X5),suc(X5)) ),
inference(resolution,[status(thm)],[c0,clause_6244]) ).
cnf(clause_6260,axiom,
( ~ 'E'('0',f(suc(suc(X6))))
| ~ 'E'('0',f(suc(X6)))
| ~ 'E'(f(X6),f(suc(X6)))
| ~ 'E'('0',f(X6))
| 'E'(f(X6),f(suc(suc(X6))))
| iLEQ(suc(X6),suc(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6260) ).
cnf(c2,plain,
( ~ 'E'('0',f(suc(suc(X13))))
| ~ 'E'('0',f(suc(X13)))
| ~ 'E'('0',f(X13))
| 'E'(f(X13),f(suc(suc(X13))))
| iLEQ(suc(X13),suc(X13)) ),
inference(resolution,[status(thm)],[clause_6260,c1]) ).
cnf(c4,plain,
( ~ 'E'('0',f(suc(X14)))
| ~ 'E'('0',f(X14))
| 'E'(f(X14),f(suc(suc(X14))))
| iLEQ(suc(X14),suc(X14)) ),
inference(resolution,[status(thm)],[c2,clause_6244]) ).
cnf(c5,plain,
( ~ 'E'('0',f(X15))
| 'E'(f(X15),f(suc(suc(X15))))
| iLEQ(suc(X15),suc(X15)) ),
inference(resolution,[status(thm)],[c4,clause_6244]) ).
cnf(c6,plain,
( 'E'(f(X16),f(suc(suc(X16))))
| iLEQ(suc(X16),suc(X16)) ),
inference(resolution,[status(thm)],[c5,clause_6244]) ).
cnf(clause_3293,axiom,
( ~ 'E'('0',f(suc(suc(X17))))
| ~ 'E'(f(X17),f(suc(suc(X17))))
| ~ 'E'('0',f(suc(suc(suc(X17)))))
| ~ 'E'(f(X17),f(suc(X17)))
| ~ 'E'('0',f(suc(X17)))
| ~ 'E'('0',f(X17))
| iLEQ(suc(X17),suc(X17)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3293) ).
cnf(c8,plain,
( ~ 'E'('0',f(suc(suc(X24))))
| ~ 'E'(f(X24),f(suc(suc(X24))))
| ~ 'E'(f(X24),f(suc(X24)))
| ~ 'E'('0',f(suc(X24)))
| ~ 'E'('0',f(X24))
| iLEQ(suc(X24),suc(X24)) ),
inference(resolution,[status(thm)],[clause_3293,clause_6244]) ).
cnf(c13,plain,
( ~ 'E'('0',f(suc(suc(X25))))
| ~ 'E'(f(X25),f(suc(X25)))
| ~ 'E'('0',f(suc(X25)))
| ~ 'E'('0',f(X25))
| iLEQ(suc(X25),suc(X25)) ),
inference(resolution,[status(thm)],[c8,c6]) ).
cnf(c14,plain,
( ~ 'E'('0',f(suc(suc(X26))))
| ~ 'E'('0',f(suc(X26)))
| ~ 'E'('0',f(X26))
| iLEQ(suc(X26),suc(X26)) ),
inference(resolution,[status(thm)],[c13,c1]) ).
cnf(c15,plain,
( ~ 'E'('0',f(suc(X27)))
| ~ 'E'('0',f(X27))
| iLEQ(suc(X27),suc(X27)) ),
inference(resolution,[status(thm)],[c14,clause_6244]) ).
cnf(c16,plain,
( ~ 'E'('0',f(X28))
| iLEQ(suc(X28),suc(X28)) ),
inference(resolution,[status(thm)],[c15,clause_6244]) ).
cnf(c17,plain,
iLEQ(suc(X35),suc(X35)),
inference(resolution,[status(thm)],[c16,clause_6244]) ).
cnf(clause_4556,axiom,
( ~ iLEQ(suc(X40),suc(X39))
| ~ iLEQ(suc(X37),suc(X40))
| ~ 'E'('0',f(X40))
| ~ iLEQ(suc(X36),suc(X41))
| ~ 'E'('0',f(suc(X37)))
| ~ 'E'('0',f(suc(X39)))
| ~ iLEQ(suc(X39),suc(X38))
| ~ 'E'('0',f(X37))
| ~ 'E'('0',f(X39))
| ~ 'E'('0',f(suc(X36)))
| ~ 'E'('0',f(X41))
| ~ 'E'('0',f(X38))
| ~ 'E'('0',f(suc(X41)))
| ~ 'E'('0',f(suc(X40)))
| ~ 'E'('0',f(X36))
| ~ 'E'('0',f(suc(X38)))
| ~ iLEQ(suc(X41),suc(X37))
| 'E'(f(X40),f(suc(X40)))
| 'E'(f(X37),f(suc(X37)))
| 'E'(f(X41),f(suc(X41)))
| 'E'(f(X39),f(suc(X39)))
| 'E'(f(X36),f(suc(X36)))
| 'E'(f(X38),f(suc(X38))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4556) ).
cnf(c20,plain,
( ~ iLEQ(suc(X42),suc(X45))
| ~ iLEQ(suc(X45),suc(X42))
| ~ 'E'('0',f(X42))
| ~ iLEQ(suc(X44),suc(X42))
| ~ 'E'('0',f(suc(X45)))
| ~ iLEQ(suc(X45),suc(X43))
| ~ 'E'('0',f(X45))
| ~ 'E'('0',f(suc(X44)))
| ~ 'E'('0',f(X43))
| ~ 'E'('0',f(suc(X42)))
| ~ 'E'('0',f(X44))
| ~ 'E'('0',f(suc(X43)))
| 'E'(f(X42),f(suc(X42)))
| 'E'(f(X45),f(suc(X45)))
| 'E'(f(X44),f(suc(X44)))
| 'E'(f(X43),f(suc(X43))) ),
inference(factor,[status(thm)],[clause_4556]) ).
cnf(c29,plain,
( ~ iLEQ(suc(X46),suc(X47))
| ~ iLEQ(suc(X47),suc(X46))
| ~ 'E'('0',f(X46))
| ~ iLEQ(suc(X48),suc(X46))
| ~ 'E'('0',f(suc(X47)))
| ~ 'E'('0',f(X47))
| ~ 'E'('0',f(suc(X48)))
| ~ 'E'('0',f(suc(X46)))
| ~ 'E'('0',f(X48))
| 'E'(f(X46),f(suc(X46)))
| 'E'(f(X47),f(suc(X47)))
| 'E'(f(X48),f(suc(X48))) ),
inference(factor,[status(thm)],[c20]) ).
cnf(c32,plain,
( ~ iLEQ(suc(X49),suc(X49))
| ~ 'E'('0',f(X49))
| ~ iLEQ(suc(X50),suc(X49))
| ~ 'E'('0',f(suc(X49)))
| ~ 'E'('0',f(suc(X50)))
| ~ 'E'('0',f(X50))
| 'E'(f(X49),f(suc(X49)))
| 'E'(f(X50),f(suc(X50))) ),
inference(factor,[status(thm)],[c29]) ).
cnf(c38,plain,
( ~ iLEQ(suc(X57),suc(X57))
| ~ 'E'('0',f(X57))
| ~ 'E'('0',f(suc(X57)))
| 'E'(f(X57),f(suc(X57))) ),
inference(factor,[status(thm)],[c32]) ).
cnf(c40,plain,
( ~ iLEQ(suc(X58),suc(X58))
| ~ 'E'('0',f(X58))
| 'E'(f(X58),f(suc(X58))) ),
inference(resolution,[status(thm)],[c38,clause_6244]) ).
cnf(c41,plain,
( ~ 'E'('0',f(X59))
| 'E'(f(X59),f(suc(X59))) ),
inference(resolution,[status(thm)],[c40,c17]) ).
cnf(c42,plain,
'E'(f(X60),f(suc(X60))),
inference(resolution,[status(thm)],[c41,clause_6244]) ).
cnf(clause_433,axiom,
( ~ 'E'(f(X2547),f(suc(X2547)))
| ~ iLEQ(suc(X2547),suc(X2546))
| ~ 'E'('0',f(suc(suc(X2543))))
| ~ iLEQ(suc(X2544),suc(X2547))
| ~ 'E'('0',f(X2547))
| ~ 'E'('0',f(suc(suc(X2544))))
| ~ 'E'(f(X2544),f(suc(X2544)))
| ~ 'E'(f(X2548),f(suc(X2548)))
| ~ iLEQ(suc(X2543),suc(X2548))
| ~ 'E'('0',f(suc(X2544)))
| ~ 'E'('0',f(suc(X2546)))
| ~ iLEQ(suc(X2546),suc(X2545))
| ~ 'E'(f(X2546),f(suc(X2546)))
| ~ 'E'('0',f(suc(suc(X2545))))
| ~ 'E'(f(X2543),f(suc(X2543)))
| ~ 'E'('0',f(X2544))
| ~ 'E'('0',f(X2546))
| ~ 'E'('0',f(suc(X2543)))
| ~ 'E'('0',f(X2548))
| ~ 'E'(f(X2545),f(suc(X2545)))
| ~ 'E'('0',f(suc(suc(X2548))))
| ~ 'E'('0',f(X2545))
| ~ 'E'('0',f(suc(X2548)))
| ~ 'E'('0',f(suc(X2547)))
| ~ 'E'('0',f(suc(suc(X2546))))
| ~ 'E'('0',f(suc(suc(X2547))))
| ~ 'E'('0',f(X2543))
| ~ 'E'('0',f(suc(X2545)))
| ~ iLEQ(suc(X2548),suc(X2544))
| 'E'(f(X2546),f(suc(suc(X2546))))
| 'E'(f(X2543),f(suc(suc(X2543))))
| 'E'(f(X2548),f(suc(suc(X2548))))
| 'E'(f(X2545),f(suc(suc(X2545))))
| 'E'(f(X2544),f(suc(suc(X2544))))
| 'E'(f(X2547),f(suc(suc(X2547)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_433) ).
cnf(c156,plain,
( ~ 'E'(f(X2586),f(suc(X2586)))
| ~ iLEQ(suc(X2586),suc(X2585))
| ~ 'E'('0',f(suc(suc(X2586))))
| ~ iLEQ(suc(X2584),suc(X2586))
| ~ 'E'('0',f(X2586))
| ~ 'E'('0',f(suc(suc(X2584))))
| ~ 'E'(f(X2584),f(suc(X2584)))
| ~ 'E'(f(X2582),f(suc(X2582)))
| ~ iLEQ(suc(X2586),suc(X2582))
| ~ 'E'('0',f(suc(X2584)))
| ~ 'E'('0',f(suc(X2585)))
| ~ iLEQ(suc(X2585),suc(X2583))
| ~ 'E'(f(X2585),f(suc(X2585)))
| ~ 'E'('0',f(suc(suc(X2583))))
| ~ 'E'('0',f(X2584))
| ~ 'E'('0',f(X2585))
| ~ 'E'('0',f(suc(X2586)))
| ~ 'E'('0',f(X2582))
| ~ 'E'(f(X2583),f(suc(X2583)))
| ~ 'E'('0',f(suc(suc(X2582))))
| ~ 'E'('0',f(X2583))
| ~ 'E'('0',f(suc(X2582)))
| ~ 'E'('0',f(suc(suc(X2585))))
| ~ 'E'('0',f(suc(X2583)))
| ~ iLEQ(suc(X2582),suc(X2584))
| 'E'(f(X2585),f(suc(suc(X2585))))
| 'E'(f(X2586),f(suc(suc(X2586))))
| 'E'(f(X2582),f(suc(suc(X2582))))
| 'E'(f(X2583),f(suc(suc(X2583))))
| 'E'(f(X2584),f(suc(suc(X2584)))) ),
inference(factor,[status(thm)],[clause_433]) ).
cnf(c191,plain,
( ~ 'E'(f(X2587),f(suc(X2587)))
| ~ iLEQ(suc(X2587),suc(X2590))
| ~ 'E'('0',f(suc(suc(X2587))))
| ~ iLEQ(suc(X2589),suc(X2587))
| ~ 'E'('0',f(X2587))
| ~ 'E'('0',f(suc(suc(X2589))))
| ~ 'E'(f(X2589),f(suc(X2589)))
| ~ 'E'(f(X2590),f(suc(X2590)))
| ~ 'E'('0',f(suc(X2589)))
| ~ 'E'('0',f(suc(X2590)))
| ~ iLEQ(suc(X2590),suc(X2588))
| ~ 'E'('0',f(suc(suc(X2588))))
| ~ 'E'('0',f(X2589))
| ~ 'E'('0',f(X2590))
| ~ 'E'('0',f(suc(X2587)))
| ~ 'E'(f(X2588),f(suc(X2588)))
| ~ 'E'('0',f(suc(suc(X2590))))
| ~ 'E'('0',f(X2588))
| ~ 'E'('0',f(suc(X2588)))
| ~ iLEQ(suc(X2590),suc(X2589))
| 'E'(f(X2590),f(suc(suc(X2590))))
| 'E'(f(X2587),f(suc(suc(X2587))))
| 'E'(f(X2588),f(suc(suc(X2588))))
| 'E'(f(X2589),f(suc(suc(X2589)))) ),
inference(factor,[status(thm)],[c156]) ).
cnf(c196,plain,
( ~ 'E'(f(X2591),f(suc(X2591)))
| ~ iLEQ(suc(X2591),suc(X2591))
| ~ 'E'('0',f(suc(suc(X2591))))
| ~ iLEQ(suc(X2593),suc(X2591))
| ~ 'E'('0',f(X2591))
| ~ 'E'('0',f(suc(suc(X2593))))
| ~ 'E'(f(X2593),f(suc(X2593)))
| ~ 'E'('0',f(suc(X2593)))
| ~ 'E'('0',f(suc(X2591)))
| ~ iLEQ(suc(X2591),suc(X2592))
| ~ 'E'('0',f(suc(suc(X2592))))
| ~ 'E'('0',f(X2593))
| ~ 'E'(f(X2592),f(suc(X2592)))
| ~ 'E'('0',f(X2592))
| ~ 'E'('0',f(suc(X2592)))
| ~ iLEQ(suc(X2591),suc(X2593))
| 'E'(f(X2591),f(suc(suc(X2591))))
| 'E'(f(X2592),f(suc(suc(X2592))))
| 'E'(f(X2593),f(suc(suc(X2593)))) ),
inference(factor,[status(thm)],[c191]) ).
cnf(c206,plain,
( ~ 'E'(f(X2601),f(suc(X2601)))
| ~ iLEQ(suc(X2601),suc(X2601))
| ~ 'E'('0',f(suc(suc(X2601))))
| ~ iLEQ(suc(X2600),suc(X2601))
| ~ 'E'('0',f(X2601))
| ~ 'E'('0',f(suc(suc(X2600))))
| ~ 'E'(f(X2600),f(suc(X2600)))
| ~ 'E'('0',f(suc(X2600)))
| ~ 'E'('0',f(suc(X2601)))
| ~ 'E'('0',f(X2600))
| ~ iLEQ(suc(X2601),suc(X2600))
| 'E'(f(X2601),f(suc(suc(X2601))))
| 'E'(f(X2600),f(suc(suc(X2600)))) ),
inference(factor,[status(thm)],[c196]) ).
cnf(c209,plain,
( ~ 'E'(f(X2602),f(suc(X2602)))
| ~ iLEQ(suc(X2602),suc(X2602))
| ~ 'E'('0',f(suc(suc(X2602))))
| ~ 'E'('0',f(X2602))
| ~ 'E'('0',f(suc(X2602)))
| 'E'(f(X2602),f(suc(suc(X2602)))) ),
inference(factor,[status(thm)],[c206]) ).
cnf(c211,plain,
( ~ 'E'(f(X2603),f(suc(X2603)))
| ~ iLEQ(suc(X2603),suc(X2603))
| ~ 'E'('0',f(X2603))
| ~ 'E'('0',f(suc(X2603)))
| 'E'(f(X2603),f(suc(suc(X2603)))) ),
inference(resolution,[status(thm)],[c209,clause_6244]) ).
cnf(c212,plain,
( ~ iLEQ(suc(X2604),suc(X2604))
| ~ 'E'('0',f(X2604))
| ~ 'E'('0',f(suc(X2604)))
| 'E'(f(X2604),f(suc(suc(X2604)))) ),
inference(resolution,[status(thm)],[c211,c42]) ).
cnf(c213,plain,
( ~ iLEQ(suc(X2605),suc(X2605))
| ~ 'E'('0',f(X2605))
| 'E'(f(X2605),f(suc(suc(X2605)))) ),
inference(resolution,[status(thm)],[c212,clause_6244]) ).
cnf(c214,plain,
( ~ 'E'('0',f(X2612))
| 'E'(f(X2612),f(suc(suc(X2612)))) ),
inference(resolution,[status(thm)],[c213,c17]) ).
cnf(c218,plain,
'E'(f(X2613),f(suc(suc(X2613)))),
inference(resolution,[status(thm)],[c214,clause_6244]) ).
cnf(clause_4547,axiom,
( ~ 'E'('0',f(suc(suc(suc(X5061)))))
| ~ 'E'(f(X5061),f(suc(suc(X5061))))
| ~ 'E'(f(X5062),f(suc(X5062)))
| ~ iLEQ(suc(X5062),suc(X5061))
| ~ 'E'('0',f(suc(suc(X5058))))
| ~ iLEQ(suc(X5059),suc(X5062))
| ~ 'E'('0',f(X5062))
| ~ 'E'('0',f(suc(suc(suc(X5060)))))
| ~ 'E'('0',f(suc(suc(X5059))))
| ~ 'E'('0',f(suc(suc(suc(X5059)))))
| ~ 'E'(f(X5059),f(suc(X5059)))
| ~ 'E'('0',f(suc(suc(suc(X5063)))))
| ~ 'E'(f(X5063),f(suc(X5063)))
| ~ iLEQ(suc(X5058),suc(X5063))
| ~ 'E'(f(X5058),f(suc(suc(X5058))))
| ~ 'E'('0',f(suc(X5059)))
| ~ 'E'('0',f(suc(X5061)))
| ~ iLEQ(suc(X5061),suc(X5060))
| ~ 'E'('0',f(suc(suc(suc(X5058)))))
| ~ 'E'(f(X5061),f(suc(X5061)))
| ~ 'E'('0',f(suc(suc(X5060))))
| ~ 'E'(f(X5058),f(suc(X5058)))
| ~ 'E'('0',f(X5059))
| ~ 'E'('0',f(X5061))
| ~ 'E'('0',f(suc(X5058)))
| ~ 'E'('0',f(X5063))
| ~ 'E'(f(X5060),f(suc(X5060)))
| ~ 'E'('0',f(suc(suc(X5063))))
| ~ 'E'(f(X5063),f(suc(suc(X5063))))
| ~ 'E'('0',f(X5060))
| ~ 'E'('0',f(suc(suc(suc(X5062)))))
| ~ 'E'('0',f(suc(X5063)))
| ~ 'E'('0',f(suc(X5062)))
| ~ 'E'('0',f(suc(suc(X5061))))
| ~ 'E'('0',f(suc(suc(X5062))))
| ~ 'E'('0',f(X5058))
| ~ 'E'(f(X5060),f(suc(suc(X5060))))
| ~ 'E'(f(X5059),f(suc(suc(X5059))))
| ~ 'E'('0',f(suc(X5060)))
| ~ iLEQ(suc(X5063),suc(X5059))
| ~ 'E'(f(X5062),f(suc(suc(X5062)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4547) ).
cnf(c219,plain,
( ~ 'E'('0',f(suc(suc(suc(X5064)))))
| ~ 'E'(f(X5064),f(suc(suc(X5064))))
| ~ 'E'(f(X5064),f(suc(X5064)))
| ~ iLEQ(suc(X5064),suc(X5064))
| ~ 'E'('0',f(suc(suc(X5068))))
| ~ iLEQ(suc(X5067),suc(X5064))
| ~ 'E'('0',f(X5064))
| ~ 'E'('0',f(suc(suc(suc(X5065)))))
| ~ 'E'('0',f(suc(suc(X5067))))
| ~ 'E'('0',f(suc(suc(suc(X5067)))))
| ~ 'E'(f(X5067),f(suc(X5067)))
| ~ 'E'('0',f(suc(suc(suc(X5066)))))
| ~ 'E'(f(X5066),f(suc(X5066)))
| ~ iLEQ(suc(X5068),suc(X5066))
| ~ 'E'(f(X5068),f(suc(suc(X5068))))
| ~ 'E'('0',f(suc(X5067)))
| ~ 'E'('0',f(suc(X5064)))
| ~ iLEQ(suc(X5064),suc(X5065))
| ~ 'E'('0',f(suc(suc(suc(X5068)))))
| ~ 'E'('0',f(suc(suc(X5065))))
| ~ 'E'(f(X5068),f(suc(X5068)))
| ~ 'E'('0',f(X5067))
| ~ 'E'('0',f(suc(X5068)))
| ~ 'E'('0',f(X5066))
| ~ 'E'(f(X5065),f(suc(X5065)))
| ~ 'E'('0',f(suc(suc(X5066))))
| ~ 'E'(f(X5066),f(suc(suc(X5066))))
| ~ 'E'('0',f(X5065))
| ~ 'E'('0',f(suc(X5066)))
| ~ 'E'('0',f(suc(suc(X5064))))
| ~ 'E'('0',f(X5068))
| ~ 'E'(f(X5065),f(suc(suc(X5065))))
| ~ 'E'(f(X5067),f(suc(suc(X5067))))
| ~ 'E'('0',f(suc(X5065)))
| ~ iLEQ(suc(X5066),suc(X5067)) ),
inference(factor,[status(thm)],[clause_4547]) ).
cnf(c225,plain,
( ~ 'E'('0',f(suc(suc(suc(X5072)))))
| ~ 'E'(f(X5072),f(suc(suc(X5072))))
| ~ 'E'(f(X5072),f(suc(X5072)))
| ~ iLEQ(suc(X5072),suc(X5072))
| ~ 'E'('0',f(suc(suc(X5070))))
| ~ 'E'('0',f(X5072))
| ~ 'E'('0',f(suc(suc(suc(X5069)))))
| ~ 'E'('0',f(suc(suc(X5072))))
| ~ 'E'('0',f(suc(suc(suc(X5071)))))
| ~ 'E'(f(X5071),f(suc(X5071)))
| ~ iLEQ(suc(X5070),suc(X5071))
| ~ 'E'(f(X5070),f(suc(suc(X5070))))
| ~ 'E'('0',f(suc(X5072)))
| ~ iLEQ(suc(X5072),suc(X5069))
| ~ 'E'('0',f(suc(suc(suc(X5070)))))
| ~ 'E'('0',f(suc(suc(X5069))))
| ~ 'E'(f(X5070),f(suc(X5070)))
| ~ 'E'('0',f(suc(X5070)))
| ~ 'E'('0',f(X5071))
| ~ 'E'(f(X5069),f(suc(X5069)))
| ~ 'E'('0',f(suc(suc(X5071))))
| ~ 'E'(f(X5071),f(suc(suc(X5071))))
| ~ 'E'('0',f(X5069))
| ~ 'E'('0',f(suc(X5071)))
| ~ 'E'('0',f(X5070))
| ~ 'E'(f(X5069),f(suc(suc(X5069))))
| ~ 'E'('0',f(suc(X5069)))
| ~ iLEQ(suc(X5071),suc(X5072)) ),
inference(factor,[status(thm)],[c219]) ).
cnf(c230,plain,
( ~ 'E'('0',f(suc(suc(suc(X5075)))))
| ~ 'E'(f(X5075),f(suc(suc(X5075))))
| ~ 'E'(f(X5075),f(suc(X5075)))
| ~ iLEQ(suc(X5075),suc(X5075))
| ~ 'E'('0',f(suc(suc(X5073))))
| ~ 'E'('0',f(X5075))
| ~ 'E'('0',f(suc(suc(X5075))))
| ~ 'E'('0',f(suc(suc(suc(X5074)))))
| ~ 'E'(f(X5074),f(suc(X5074)))
| ~ iLEQ(suc(X5073),suc(X5074))
| ~ 'E'(f(X5073),f(suc(suc(X5073))))
| ~ 'E'('0',f(suc(X5075)))
| ~ 'E'('0',f(suc(suc(suc(X5073)))))
| ~ 'E'(f(X5073),f(suc(X5073)))
| ~ 'E'('0',f(suc(X5073)))
| ~ 'E'('0',f(X5074))
| ~ 'E'('0',f(suc(suc(X5074))))
| ~ 'E'(f(X5074),f(suc(suc(X5074))))
| ~ 'E'('0',f(suc(X5074)))
| ~ 'E'('0',f(X5073))
| ~ iLEQ(suc(X5074),suc(X5075)) ),
inference(factor,[status(thm)],[c225]) ).
cnf(c234,plain,
( ~ 'E'('0',f(suc(suc(suc(X5076)))))
| ~ 'E'(f(X5076),f(suc(suc(X5076))))
| ~ 'E'(f(X5076),f(suc(X5076)))
| ~ iLEQ(suc(X5076),suc(X5076))
| ~ 'E'('0',f(suc(suc(X5077))))
| ~ 'E'('0',f(X5076))
| ~ 'E'('0',f(suc(suc(X5076))))
| ~ iLEQ(suc(X5077),suc(X5076))
| ~ 'E'(f(X5077),f(suc(suc(X5077))))
| ~ 'E'('0',f(suc(X5076)))
| ~ 'E'('0',f(suc(suc(suc(X5077)))))
| ~ 'E'(f(X5077),f(suc(X5077)))
| ~ 'E'('0',f(suc(X5077)))
| ~ 'E'('0',f(X5077)) ),
inference(factor,[status(thm)],[c230]) ).
cnf(c237,plain,
( ~ 'E'('0',f(suc(suc(suc(X5078)))))
| ~ 'E'(f(X5078),f(suc(suc(X5078))))
| ~ 'E'(f(X5078),f(suc(X5078)))
| ~ iLEQ(suc(X5078),suc(X5078))
| ~ 'E'('0',f(suc(suc(X5078))))
| ~ 'E'('0',f(X5078))
| ~ 'E'('0',f(suc(X5078))) ),
inference(factor,[status(thm)],[c234]) ).
cnf(c242,plain,
( ~ 'E'('0',f(suc(suc(suc(X5085)))))
| ~ 'E'(f(X5085),f(suc(X5085)))
| ~ iLEQ(suc(X5085),suc(X5085))
| ~ 'E'('0',f(suc(suc(X5085))))
| ~ 'E'('0',f(X5085))
| ~ 'E'('0',f(suc(X5085))) ),
inference(resolution,[status(thm)],[c237,c218]) ).
cnf(c243,plain,
( ~ 'E'(f(X5086),f(suc(X5086)))
| ~ iLEQ(suc(X5086),suc(X5086))
| ~ 'E'('0',f(suc(suc(X5086))))
| ~ 'E'('0',f(X5086))
| ~ 'E'('0',f(suc(X5086))) ),
inference(resolution,[status(thm)],[c242,clause_6244]) ).
cnf(c244,plain,
( ~ 'E'(f(X5087),f(suc(X5087)))
| ~ iLEQ(suc(X5087),suc(X5087))
| ~ 'E'('0',f(X5087))
| ~ 'E'('0',f(suc(X5087))) ),
inference(resolution,[status(thm)],[c243,clause_6244]) ).
cnf(c245,plain,
( ~ iLEQ(suc(X5088),suc(X5088))
| ~ 'E'('0',f(X5088))
| ~ 'E'('0',f(suc(X5088))) ),
inference(resolution,[status(thm)],[c244,c42]) ).
cnf(c246,plain,
( ~ iLEQ(suc(X5089),suc(X5089))
| ~ 'E'('0',f(X5089)) ),
inference(resolution,[status(thm)],[c245,clause_6244]) ).
cnf(c247,plain,
~ 'E'('0',f(X5096)),
inference(resolution,[status(thm)],[c246,c17]) ).
cnf(c248,plain,
$false,
inference(resolution,[status(thm)],[c247,clause_6244]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SYO647-1 : TPTP v8.1.2. Released v7.3.0.
% 0.09/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n018.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 17:53:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 35.70/35.89 % Version: 1.5
% 35.70/35.89 % SZS status Unsatisfiable
% 35.70/35.89 % SZS output start CNFRefutation
% See solution above
% 35.70/35.90
% 35.70/35.90 % Initial clauses : 733
% 35.70/35.90 % Processed clauses : 102
% 35.70/35.90 % Factors computed : 188
% 35.70/35.90 % Resolvents computed: 61
% 35.70/35.90 % Tautologies deleted: 22
% 35.70/35.90 % Forward subsumed : 837
% 35.70/35.90 % Backward subsumed : 97
% 35.70/35.90 % -------- CPU Time ---------
% 35.70/35.90 % User time : 35.503 s
% 35.70/35.90 % System time : 0.028 s
% 35.70/35.90 % Total time : 35.531 s
%------------------------------------------------------------------------------