%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO685-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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 56.45s 56.66s
% Output : Refutation 56.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 37
% Syntax : Number of clauses : 135 ( 13 unt; 78 nHn; 103 RR)
% Number of literals : 462 ( 0 equ; 256 neg)
% Maximal clause size : 9 ( 3 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 : 127 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_96,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_96) ).
cnf(clause_173,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_173) ).
cnf(clause_184,axiom,
( ~ 'LE'(f(X5),s(s('0')))
| 'E'(s('0'),f(X5))
| 'LE'(f(X5),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_184) ).
cnf(clause_125,axiom,
( ~ 'LE'(f(X10),s(s(s('0'))))
| 'E'(s(s('0')),f(X10))
| 'LE'(f(X10),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_125) ).
cnf(clause_95,axiom,
( ~ 'LE'(f(X15),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(X15))
| 'LE'(f(X15),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_95) ).
cnf(clause_53,axiom,
'LE'(f(X2),s(s(s(s(s('0')))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_53) ).
cnf(clause_113,axiom,
( ~ 'LE'(f(X21),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(X21))
| 'LE'(f(X21),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_113) ).
cnf(c0,plain,
( 'E'(s(s(s(s('0')))),f(X22))
| 'LE'(f(X22),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[clause_113,clause_53]) ).
cnf(clause_130,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X12))
| ~ 'E'(s(s(s(s('0')))),f(suc(X12)))
| 'E'(f(X12),f(suc(X12)))
| iLEQ(suc(X12),suc(X12)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_130) ).
cnf(clause_191,axiom,
( ~ 'LE'(f(suc(X35)),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(X35)))
| 'LE'(f(X35),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_191) ).
cnf(c46,plain,
( 'E'(s(s(s(s('0')))),f(suc(X36)))
| 'LE'(f(X36),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[clause_191,clause_53]) ).
cnf(c48,plain,
( 'LE'(f(X41),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(X41))
| 'E'(f(X41),f(suc(X41)))
| iLEQ(suc(X41),suc(X41)) ),
inference(resolution,[status(thm)],[c46,clause_130]) ).
cnf(c73,plain,
( 'LE'(f(X42),s(s(s(s('0')))))
| 'E'(f(X42),f(suc(X42)))
| iLEQ(suc(X42),suc(X42)) ),
inference(resolution,[status(thm)],[c48,c0]) ).
cnf(clause_34,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X141))
| ~ iLEQ(suc(X142),suc(X141))
| ~ 'E'(s(s(s(s('0')))),f(suc(X141)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X142)))
| ~ 'E'(s(s(s(s('0')))),f(X142))
| 'E'(f(X142),f(suc(X142)))
| 'E'(f(X141),f(suc(X141))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_34) ).
cnf(c907,plain,
( ~ 'E'(s(s(s(s('0')))),f(X143))
| ~ iLEQ(suc(X143),suc(X143))
| ~ 'E'(s(s(s(s('0')))),f(suc(X143)))
| 'E'(f(X143),f(suc(X143))) ),
inference(factor,[status(thm)],[clause_34]) ).
cnf(c967,plain,
( ~ 'E'(s(s(s(s('0')))),f(X157))
| ~ iLEQ(suc(X157),suc(X157))
| 'E'(f(X157),f(suc(X157)))
| 'LE'(f(X157),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c907,c46]) ).
cnf(c1169,plain,
( ~ iLEQ(suc(X158),suc(X158))
| 'E'(f(X158),f(suc(X158)))
| 'LE'(f(X158),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c967,c0]) ).
cnf(c1191,plain,
( 'E'(f(X159),f(suc(X159)))
| 'LE'(f(X159),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c1169,c73]) ).
cnf(clause_79,axiom,
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X51))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X51)))
| ~ 'E'(f(X51),f(suc(X51)))
| ~ 'E'(s(s(s(s('0')))),f(X51))
| iLEQ(suc(X51),suc(X51)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_79) ).
cnf(clause_93,axiom,
( ~ 'LE'(f(suc(suc(X52))),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X52))))
| 'LE'(f(X52),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_93) ).
cnf(c150,plain,
( 'E'(s(s(s(s('0')))),f(suc(suc(X53))))
| 'LE'(f(X53),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[clause_93,clause_53]) ).
cnf(c152,plain,
( 'LE'(f(X389),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X389)))
| ~ 'E'(f(X389),f(suc(X389)))
| ~ 'E'(s(s(s(s('0')))),f(X389))
| iLEQ(suc(X389),suc(X389)) ),
inference(resolution,[status(thm)],[c150,clause_79]) ).
cnf(c5443,plain,
( 'LE'(f(X391),s(s(s(s('0')))))
| ~ 'E'(f(X391),f(suc(X391)))
| ~ 'E'(s(s(s(s('0')))),f(X391))
| iLEQ(suc(X391),suc(X391)) ),
inference(resolution,[status(thm)],[c152,c46]) ).
cnf(c5600,plain,
( 'LE'(f(X392),s(s(s(s('0')))))
| ~ 'E'(f(X392),f(suc(X392)))
| iLEQ(suc(X392),suc(X392)) ),
inference(resolution,[status(thm)],[c5443,c0]) ).
cnf(c5614,plain,
( 'LE'(f(X393),s(s(s(s('0')))))
| iLEQ(suc(X393),suc(X393)) ),
inference(resolution,[status(thm)],[c5600,c1191]) ).
cnf(clause_183,axiom,
( ~ 'E'(s(s(s(s('0')))),f(X169))
| ~ iLEQ(suc(X170),suc(X169))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X169))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X169)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X170))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X170)))
| ~ 'E'(f(X170),f(suc(X170)))
| ~ 'E'(s(s(s(s('0')))),f(X170))
| ~ 'E'(f(X169),f(suc(X169))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_183) ).
cnf(c1290,plain,
( ~ 'E'(s(s(s(s('0')))),f(X934))
| ~ iLEQ(suc(X934),suc(X934))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X934))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X934)))
| ~ 'E'(f(X934),f(suc(X934))) ),
inference(factor,[status(thm)],[clause_183]) ).
cnf(c25064,plain,
( ~ 'E'(s(s(s(s('0')))),f(X935))
| ~ iLEQ(suc(X935),suc(X935))
| ~ 'E'(s(s(s(s('0')))),f(suc(X935)))
| ~ 'E'(f(X935),f(suc(X935)))
| 'LE'(f(X935),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c1290,c150]) ).
cnf(c25119,plain,
( ~ 'E'(s(s(s(s('0')))),f(X936))
| ~ iLEQ(suc(X936),suc(X936))
| ~ 'E'(f(X936),f(suc(X936)))
| 'LE'(f(X936),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c25064,c46]) ).
cnf(c25319,plain,
( ~ iLEQ(suc(X937),suc(X937))
| ~ 'E'(f(X937),f(suc(X937)))
| 'LE'(f(X937),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c25119,c0]) ).
cnf(c25344,plain,
( ~ iLEQ(suc(X939),suc(X939))
| 'LE'(f(X939),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[c25319,c1191]) ).
cnf(c25680,plain,
'LE'(f(X940),s(s(s(s('0'))))),
inference(resolution,[status(thm)],[c25344,c5614]) ).
cnf(c25700,plain,
( 'E'(s(s(s('0'))),f(X941))
| 'LE'(f(X941),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c25680,clause_95]) ).
cnf(clause_28,axiom,
( ~ 'E'(s(s(s('0'))),f(X20))
| ~ 'E'(s(s(s('0'))),f(suc(X20)))
| 'E'(f(X20),f(suc(X20)))
| iLEQ(suc(X20),suc(X20)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_28) ).
cnf(clause_111,axiom,
( ~ 'LE'(f(suc(X19)),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(X19)))
| 'LE'(f(X19),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_111) ).
cnf(c25699,plain,
( 'E'(s(s(s('0'))),f(suc(X942)))
| 'LE'(f(X942),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c25680,clause_111]) ).
cnf(c25773,plain,
( 'LE'(f(X959),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(X959))
| 'E'(f(X959),f(suc(X959)))
| iLEQ(suc(X959),suc(X959)) ),
inference(resolution,[status(thm)],[c25699,clause_28]) ).
cnf(c26933,plain,
( 'LE'(f(X960),s(s(s('0'))))
| 'E'(f(X960),f(suc(X960)))
| iLEQ(suc(X960),suc(X960)) ),
inference(resolution,[status(thm)],[c25773,c25700]) ).
cnf(clause_49,axiom,
( ~ iLEQ(suc(X78),suc(X79))
| ~ 'E'(s(s(s('0'))),f(suc(X78)))
| ~ 'E'(s(s(s('0'))),f(X79))
| ~ 'E'(s(s(s('0'))),f(X78))
| ~ 'E'(s(s(s('0'))),f(suc(X79)))
| 'E'(f(X78),f(suc(X78)))
| 'E'(f(X79),f(suc(X79))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_49) ).
cnf(c349,plain,
( ~ iLEQ(suc(X80),suc(X80))
| ~ 'E'(s(s(s('0'))),f(suc(X80)))
| ~ 'E'(s(s(s('0'))),f(X80))
| 'E'(f(X80),f(suc(X80))) ),
inference(factor,[status(thm)],[clause_49]) ).
cnf(c25795,plain,
( 'LE'(f(X962),s(s(s('0'))))
| ~ iLEQ(suc(X962),suc(X962))
| ~ 'E'(s(s(s('0'))),f(X962))
| 'E'(f(X962),f(suc(X962))) ),
inference(resolution,[status(thm)],[c25699,c349]) ).
cnf(c27063,plain,
( 'LE'(f(X964),s(s(s('0'))))
| ~ iLEQ(suc(X964),suc(X964))
| 'E'(f(X964),f(suc(X964))) ),
inference(resolution,[status(thm)],[c25795,c25700]) ).
cnf(c27248,plain,
( 'LE'(f(X965),s(s(s('0'))))
| 'E'(f(X965),f(suc(X965))) ),
inference(resolution,[status(thm)],[c27063,c26933]) ).
cnf(clause_190,axiom,
( ~ 'E'(s(s(s('0'))),f(suc(suc(X45))))
| ~ 'E'(s(s(s('0'))),f(suc(X45)))
| ~ 'E'(f(X45),f(suc(X45)))
| ~ 'E'(s(s(s('0'))),f(X45))
| iLEQ(suc(X45),suc(X45)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_190) ).
cnf(clause_52,axiom,
( ~ 'LE'(f(suc(suc(X28))),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(suc(X28))))
| 'LE'(f(X28),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_52) ).
cnf(c25698,plain,
( 'E'(s(s(s('0'))),f(suc(suc(X943))))
| 'LE'(f(X943),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c25680,clause_52]) ).
cnf(c25852,plain,
( 'LE'(f(X1288),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X1288)))
| ~ 'E'(f(X1288),f(suc(X1288)))
| ~ 'E'(s(s(s('0'))),f(X1288))
| iLEQ(suc(X1288),suc(X1288)) ),
inference(resolution,[status(thm)],[c25698,clause_190]) ).
cnf(c38710,plain,
( 'LE'(f(X1289),s(s(s('0'))))
| ~ 'E'(f(X1289),f(suc(X1289)))
| ~ 'E'(s(s(s('0'))),f(X1289))
| iLEQ(suc(X1289),suc(X1289)) ),
inference(resolution,[status(thm)],[c25852,c25699]) ).
cnf(c38755,plain,
( 'LE'(f(X1290),s(s(s('0'))))
| ~ 'E'(f(X1290),f(suc(X1290)))
| iLEQ(suc(X1290),suc(X1290)) ),
inference(resolution,[status(thm)],[c38710,c25700]) ).
cnf(c38825,plain,
( 'LE'(f(X1291),s(s(s('0'))))
| iLEQ(suc(X1291),suc(X1291)) ),
inference(resolution,[status(thm)],[c38755,c27248]) ).
cnf(clause_73,axiom,
( ~ iLEQ(suc(X162),suc(X163))
| ~ 'E'(s(s(s('0'))),f(suc(X162)))
| ~ 'E'(s(s(s('0'))),f(X163))
| ~ 'E'(s(s(s('0'))),f(X162))
| ~ 'E'(f(X163),f(suc(X163)))
| ~ 'E'(s(s(s('0'))),f(suc(X163)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X163))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X162))))
| ~ 'E'(f(X162),f(suc(X162))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_73) ).
cnf(c1212,plain,
( ~ iLEQ(suc(X334),suc(X334))
| ~ 'E'(s(s(s('0'))),f(suc(X334)))
| ~ 'E'(s(s(s('0'))),f(X334))
| ~ 'E'(f(X334),f(suc(X334)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X334)))) ),
inference(factor,[status(thm)],[clause_73]) ).
cnf(c25885,plain,
( 'LE'(f(X1386),s(s(s('0'))))
| ~ iLEQ(suc(X1386),suc(X1386))
| ~ 'E'(s(s(s('0'))),f(suc(X1386)))
| ~ 'E'(s(s(s('0'))),f(X1386))
| ~ 'E'(f(X1386),f(suc(X1386))) ),
inference(resolution,[status(thm)],[c25698,c1212]) ).
cnf(c42095,plain,
( 'LE'(f(X1387),s(s(s('0'))))
| ~ iLEQ(suc(X1387),suc(X1387))
| ~ 'E'(s(s(s('0'))),f(X1387))
| ~ 'E'(f(X1387),f(suc(X1387))) ),
inference(resolution,[status(thm)],[c25885,c25699]) ).
cnf(c42140,plain,
( 'LE'(f(X1388),s(s(s('0'))))
| ~ iLEQ(suc(X1388),suc(X1388))
| ~ 'E'(f(X1388),f(suc(X1388))) ),
inference(resolution,[status(thm)],[c42095,c25700]) ).
cnf(c42211,plain,
( 'LE'(f(X1390),s(s(s('0'))))
| ~ iLEQ(suc(X1390),suc(X1390)) ),
inference(resolution,[status(thm)],[c42140,c27248]) ).
cnf(c42416,plain,
'LE'(f(X1391),s(s(s('0')))),
inference(resolution,[status(thm)],[c42211,c38825]) ).
cnf(c42438,plain,
( 'E'(s(s('0')),f(X1392))
| 'LE'(f(X1392),s(s('0'))) ),
inference(resolution,[status(thm)],[c42416,clause_125]) ).
cnf(clause_115,axiom,
( ~ 'E'(s(s('0')),f(suc(X149)))
| ~ 'E'(s(s('0')),f(X149))
| ~ 'E'(s(s('0')),f(suc(X148)))
| ~ iLEQ(suc(X148),suc(X149))
| ~ 'E'(s(s('0')),f(X148))
| 'E'(f(X148),f(suc(X148)))
| 'E'(f(X149),f(suc(X149))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_115) ).
cnf(c1042,plain,
( ~ 'E'(s(s('0')),f(suc(X150)))
| ~ 'E'(s(s('0')),f(X150))
| ~ iLEQ(suc(X150),suc(X150))
| 'E'(f(X150),f(suc(X150))) ),
inference(factor,[status(thm)],[clause_115]) ).
cnf(clause_86,axiom,
( ~ 'LE'(f(suc(X14)),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(X14)))
| 'LE'(f(X14),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_86) ).
cnf(c42437,plain,
( 'E'(s(s('0')),f(suc(X1393)))
| 'LE'(f(X1393),s(s('0'))) ),
inference(resolution,[status(thm)],[c42416,clause_86]) ).
cnf(c42500,plain,
( 'LE'(f(X1417),s(s('0')))
| ~ 'E'(s(s('0')),f(X1417))
| ~ iLEQ(suc(X1417),suc(X1417))
| 'E'(f(X1417),f(suc(X1417))) ),
inference(resolution,[status(thm)],[c42437,c1042]) ).
cnf(c43512,plain,
( 'LE'(f(X1418),s(s('0')))
| ~ iLEQ(suc(X1418),suc(X1418))
| 'E'(f(X1418),f(suc(X1418))) ),
inference(resolution,[status(thm)],[c42500,c42438]) ).
cnf(clause_143,axiom,
( ~ 'E'(s(s('0')),f(X6))
| ~ 'E'(s(s('0')),f(suc(X6)))
| 'E'(f(X6),f(suc(X6)))
| iLEQ(suc(X6),suc(X6)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_143) ).
cnf(c42515,plain,
( 'LE'(f(X1419),s(s('0')))
| ~ 'E'(s(s('0')),f(X1419))
| 'E'(f(X1419),f(suc(X1419)))
| iLEQ(suc(X1419),suc(X1419)) ),
inference(resolution,[status(thm)],[c42437,clause_143]) ).
cnf(c43569,plain,
( 'LE'(f(X1420),s(s('0')))
| 'E'(f(X1420),f(suc(X1420)))
| iLEQ(suc(X1420),suc(X1420)) ),
inference(resolution,[status(thm)],[c42515,c42438]) ).
cnf(c43581,plain,
( 'LE'(f(X1421),s(s('0')))
| 'E'(f(X1421),f(suc(X1421))) ),
inference(resolution,[status(thm)],[c43569,c43512]) ).
cnf(clause_40,axiom,
( ~ 'E'(s(s('0')),f(suc(suc(X62))))
| ~ 'E'(s(s('0')),f(suc(X62)))
| ~ 'E'(f(X62),f(suc(X62)))
| ~ 'E'(s(s('0')),f(X62))
| iLEQ(suc(X62),suc(X62)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_40) ).
cnf(clause_97,axiom,
( ~ 'LE'(f(suc(suc(X16))),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(suc(X16))))
| 'LE'(f(X16),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_97) ).
cnf(c42439,plain,
( 'E'(s(s('0')),f(suc(suc(X1394))))
| 'LE'(f(X1394),s(s('0'))) ),
inference(resolution,[status(thm)],[c42416,clause_97]) ).
cnf(c42538,plain,
( 'LE'(f(X1691),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1691)))
| ~ 'E'(f(X1691),f(suc(X1691)))
| ~ 'E'(s(s('0')),f(X1691))
| iLEQ(suc(X1691),suc(X1691)) ),
inference(resolution,[status(thm)],[c42439,clause_40]) ).
cnf(c49537,plain,
( 'LE'(f(X1692),s(s('0')))
| ~ 'E'(f(X1692),f(suc(X1692)))
| ~ 'E'(s(s('0')),f(X1692))
| iLEQ(suc(X1692),suc(X1692)) ),
inference(resolution,[status(thm)],[c42538,c42437]) ).
cnf(c49650,plain,
( 'LE'(f(X1693),s(s('0')))
| ~ 'E'(f(X1693),f(suc(X1693)))
| iLEQ(suc(X1693),suc(X1693)) ),
inference(resolution,[status(thm)],[c49537,c42438]) ).
cnf(c49670,plain,
( 'LE'(f(X1694),s(s('0')))
| iLEQ(suc(X1694),suc(X1694)) ),
inference(resolution,[status(thm)],[c49650,c43581]) ).
cnf(clause_74,axiom,
( ~ 'E'(s(s('0')),f(suc(X39)))
| ~ 'E'(s(s('0')),f(X39))
| ~ 'E'(s(s('0')),f(suc(X38)))
| ~ 'E'(s(s('0')),f(suc(suc(X38))))
| ~ iLEQ(suc(X38),suc(X39))
| ~ 'E'(f(X38),f(suc(X38)))
| ~ 'E'(f(X39),f(suc(X39)))
| ~ 'E'(s(s('0')),f(X38))
| ~ 'E'(s(s('0')),f(suc(suc(X39)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_74) ).
cnf(c60,plain,
( ~ 'E'(s(s('0')),f(suc(X66)))
| ~ 'E'(s(s('0')),f(X66))
| ~ 'E'(s(s('0')),f(suc(suc(X66))))
| ~ iLEQ(suc(X66),suc(X66))
| ~ 'E'(f(X66),f(suc(X66))) ),
inference(factor,[status(thm)],[clause_74]) ).
cnf(c42571,plain,
( 'LE'(f(X1779),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1779)))
| ~ 'E'(s(s('0')),f(X1779))
| ~ iLEQ(suc(X1779),suc(X1779))
| ~ 'E'(f(X1779),f(suc(X1779))) ),
inference(resolution,[status(thm)],[c42439,c60]) ).
cnf(c50571,plain,
( 'LE'(f(X1780),s(s('0')))
| ~ 'E'(s(s('0')),f(X1780))
| ~ iLEQ(suc(X1780),suc(X1780))
| ~ 'E'(f(X1780),f(suc(X1780))) ),
inference(resolution,[status(thm)],[c42571,c42437]) ).
cnf(c50638,plain,
( 'LE'(f(X1783),s(s('0')))
| ~ 'E'(s(s('0')),f(X1783))
| ~ iLEQ(suc(X1783),suc(X1783)) ),
inference(resolution,[status(thm)],[c50571,c43581]) ).
cnf(c50739,plain,
( 'LE'(f(X1784),s(s('0')))
| ~ iLEQ(suc(X1784),suc(X1784)) ),
inference(resolution,[status(thm)],[c50638,c42438]) ).
cnf(c50764,plain,
'LE'(f(X1785),s(s('0'))),
inference(resolution,[status(thm)],[c50739,c49670]) ).
cnf(c50770,plain,
( 'E'(s('0'),f(X1786))
| 'LE'(f(X1786),s('0')) ),
inference(resolution,[status(thm)],[c50764,clause_184]) ).
cnf(clause_204,axiom,
( ~ 'E'(s('0'),f(X13))
| ~ 'E'(s('0'),f(suc(X13)))
| 'E'(f(X13),f(suc(X13)))
| iLEQ(suc(X13),suc(X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_204) ).
cnf(clause_30,axiom,
( ~ 'LE'(f(suc(X8)),s(s('0')))
| 'E'(s('0'),f(suc(X8)))
| 'LE'(f(X8),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
cnf(c50769,plain,
( 'E'(s('0'),f(suc(X1787)))
| 'LE'(f(X1787),s('0')) ),
inference(resolution,[status(thm)],[c50764,clause_30]) ).
cnf(c50797,plain,
( 'LE'(f(X1810),s('0'))
| ~ 'E'(s('0'),f(X1810))
| 'E'(f(X1810),f(suc(X1810)))
| iLEQ(suc(X1810),suc(X1810)) ),
inference(resolution,[status(thm)],[c50769,clause_204]) ).
cnf(c51273,plain,
( 'LE'(f(X1811),s('0'))
| 'E'(f(X1811),f(suc(X1811)))
| iLEQ(suc(X1811),suc(X1811)) ),
inference(resolution,[status(thm)],[c50797,c50770]) ).
cnf(clause_87,axiom,
( ~ iLEQ(suc(X127),suc(X128))
| ~ 'E'(s('0'),f(suc(X128)))
| ~ 'E'(s('0'),f(X128))
| ~ 'E'(s('0'),f(suc(X127)))
| ~ 'E'(s('0'),f(X127))
| 'E'(f(X127),f(suc(X127)))
| 'E'(f(X128),f(suc(X128))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_87) ).
cnf(c822,plain,
( ~ iLEQ(suc(X129),suc(X129))
| ~ 'E'(s('0'),f(suc(X129)))
| ~ 'E'(s('0'),f(X129))
| 'E'(f(X129),f(suc(X129))) ),
inference(factor,[status(thm)],[clause_87]) ).
cnf(c50811,plain,
( 'LE'(f(X1814),s('0'))
| ~ iLEQ(suc(X1814),suc(X1814))
| ~ 'E'(s('0'),f(X1814))
| 'E'(f(X1814),f(suc(X1814))) ),
inference(resolution,[status(thm)],[c50769,c822]) ).
cnf(c51325,plain,
( 'LE'(f(X1815),s('0'))
| ~ iLEQ(suc(X1815),suc(X1815))
| 'E'(f(X1815),f(suc(X1815))) ),
inference(resolution,[status(thm)],[c50811,c50770]) ).
cnf(c51328,plain,
( 'LE'(f(X1816),s('0'))
| 'E'(f(X1816),f(suc(X1816))) ),
inference(resolution,[status(thm)],[c51325,c51273]) ).
cnf(clause_175,axiom,
( ~ iLEQ(suc(X71),suc(X72))
| ~ 'E'(f(X71),f(suc(X71)))
| ~ 'E'(s('0'),f(suc(X72)))
| ~ 'E'(s('0'),f(suc(suc(X72))))
| ~ 'E'(s('0'),f(X72))
| ~ 'E'(s('0'),f(suc(suc(X71))))
| ~ 'E'(s('0'),f(suc(X71)))
| ~ 'E'(f(X72),f(suc(X72)))
| ~ 'E'(s('0'),f(X71)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_175) ).
cnf(c320,plain,
( ~ iLEQ(suc(X74),suc(X74))
| ~ 'E'(f(X74),f(suc(X74)))
| ~ 'E'(s('0'),f(suc(X74)))
| ~ 'E'(s('0'),f(suc(suc(X74))))
| ~ 'E'(s('0'),f(X74)) ),
inference(factor,[status(thm)],[clause_175]) ).
cnf(clause_116,axiom,
( ~ 'LE'(f(suc(suc(X11))),s(s('0')))
| 'E'(s('0'),f(suc(suc(X11))))
| 'LE'(f(X11),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_116) ).
cnf(c50771,plain,
( 'E'(s('0'),f(suc(suc(X1790))))
| 'LE'(f(X1790),s('0')) ),
inference(resolution,[status(thm)],[c50764,clause_116]) ).
cnf(c50825,plain,
( 'LE'(f(X1990),s('0'))
| ~ iLEQ(suc(X1990),suc(X1990))
| ~ 'E'(f(X1990),f(suc(X1990)))
| ~ 'E'(s('0'),f(suc(X1990)))
| ~ 'E'(s('0'),f(X1990)) ),
inference(resolution,[status(thm)],[c50771,c320]) ).
cnf(c52557,plain,
( 'LE'(f(X1991),s('0'))
| ~ iLEQ(suc(X1991),suc(X1991))
| ~ 'E'(f(X1991),f(suc(X1991)))
| ~ 'E'(s('0'),f(X1991)) ),
inference(resolution,[status(thm)],[c50825,c50769]) ).
cnf(c52581,plain,
( 'LE'(f(X1992),s('0'))
| ~ iLEQ(suc(X1992),suc(X1992))
| ~ 'E'(s('0'),f(X1992)) ),
inference(resolution,[status(thm)],[c52557,c51328]) ).
cnf(c52621,plain,
( 'LE'(f(X1993),s('0'))
| ~ iLEQ(suc(X1993),suc(X1993)) ),
inference(resolution,[status(thm)],[c52581,c50770]) ).
cnf(clause_61,axiom,
( ~ 'E'(s('0'),f(suc(suc(X18))))
| ~ 'E'(s('0'),f(suc(X18)))
| ~ 'E'(f(X18),f(suc(X18)))
| ~ 'E'(s('0'),f(X18))
| iLEQ(suc(X18),suc(X18)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_61) ).
cnf(c50829,plain,
( 'LE'(f(X2019),s('0'))
| ~ 'E'(s('0'),f(suc(X2019)))
| ~ 'E'(f(X2019),f(suc(X2019)))
| ~ 'E'(s('0'),f(X2019))
| iLEQ(suc(X2019),suc(X2019)) ),
inference(resolution,[status(thm)],[c50771,clause_61]) ).
cnf(c52630,plain,
( 'LE'(f(X2020),s('0'))
| ~ 'E'(s('0'),f(suc(X2020)))
| ~ 'E'(s('0'),f(X2020))
| iLEQ(suc(X2020),suc(X2020)) ),
inference(resolution,[status(thm)],[c50829,c51328]) ).
cnf(c52654,plain,
( 'LE'(f(X2021),s('0'))
| ~ 'E'(s('0'),f(X2021))
| iLEQ(suc(X2021),suc(X2021)) ),
inference(resolution,[status(thm)],[c52630,c50769]) ).
cnf(c52695,plain,
( 'LE'(f(X2022),s('0'))
| iLEQ(suc(X2022),suc(X2022)) ),
inference(resolution,[status(thm)],[c52654,c50770]) ).
cnf(c52700,plain,
'LE'(f(X2025),s('0')),
inference(resolution,[status(thm)],[c52695,c52621]) ).
cnf(c52703,plain,
( 'E'('0',f(X2026))
| 'LE'(f(X2026),'0') ),
inference(resolution,[status(thm)],[c52700,clause_173]) ).
cnf(c52712,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c52703,clause_96]) ).
cnf(clause_168,axiom,
( ~ 'LE'(f(suc(X4)),s('0'))
| 'E'('0',f(suc(X4)))
| 'LE'(f(X4),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_168) ).
cnf(c52702,plain,
( 'E'('0',f(suc(X2027)))
| 'LE'(f(X2027),'0') ),
inference(resolution,[status(thm)],[c52700,clause_168]) ).
cnf(c52721,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c52702,clause_96]) ).
cnf(clause_169,axiom,
( ~ iLEQ(suc(X25),suc(X24))
| ~ 'E'('0',f(X25))
| ~ 'E'('0',f(suc(X25)))
| ~ 'E'('0',f(suc(X24)))
| ~ 'E'('0',f(X24))
| 'E'(f(X25),f(suc(X25)))
| 'E'(f(X24),f(suc(X24))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_169) ).
cnf(c10,plain,
( ~ iLEQ(suc(X26),suc(X26))
| ~ 'E'('0',f(X26))
| ~ 'E'('0',f(suc(X26)))
| 'E'(f(X26),f(suc(X26))) ),
inference(factor,[status(thm)],[clause_169]) ).
cnf(c52723,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| 'E'(f(z),f(suc(z))) ),
inference(resolution,[status(thm)],[c52721,c10]) ).
cnf(clause_19,axiom,
( ~ 'E'('0',f(X9))
| ~ 'E'('0',f(suc(X9)))
| 'E'(f(X9),f(suc(X9)))
| iLEQ(suc(X9),suc(X9)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
cnf(c52724,plain,
( ~ 'E'('0',f(z))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c52721,clause_19]) ).
cnf(c52741,plain,
( 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c52724,c52712]) ).
cnf(c52746,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c52741,c52723]) ).
cnf(c52748,plain,
'E'(f(z),f(suc(z))),
inference(resolution,[status(thm)],[c52746,c52712]) ).
cnf(clause_105,axiom,
( ~ 'E'(f(X135),f(suc(X135)))
| ~ 'E'('0',f(suc(suc(X135))))
| ~ iLEQ(suc(X134),suc(X135))
| ~ 'E'('0',f(X134))
| ~ 'E'('0',f(suc(X134)))
| ~ 'E'('0',f(suc(suc(X134))))
| ~ 'E'('0',f(suc(X135)))
| ~ 'E'('0',f(X135))
| ~ 'E'(f(X134),f(suc(X134))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_105) ).
cnf(c851,plain,
( ~ 'E'(f(X136),f(suc(X136)))
| ~ 'E'('0',f(suc(suc(X136))))
| ~ iLEQ(suc(X136),suc(X136))
| ~ 'E'('0',f(X136))
| ~ 'E'('0',f(suc(X136))) ),
inference(factor,[status(thm)],[clause_105]) ).
cnf(clause_11,axiom,
( ~ 'LE'(f(suc(suc(X7))),s('0'))
| 'E'('0',f(suc(suc(X7))))
| 'LE'(f(X7),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11) ).
cnf(c52704,plain,
( 'E'('0',f(suc(suc(X2030))))
| 'LE'(f(X2030),'0') ),
inference(resolution,[status(thm)],[c52700,clause_11]) ).
cnf(c52733,plain,
'E'('0',f(suc(suc(z)))),
inference(resolution,[status(thm)],[c52704,clause_96]) ).
cnf(c52735,plain,
( ~ 'E'(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c52733,c851]) ).
cnf(c52787,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c52735,c52748]) ).
cnf(c52790,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c52787,c52721]) ).
cnf(clause_44,axiom,
( ~ 'E'('0',f(suc(suc(X17))))
| ~ 'E'('0',f(suc(X17)))
| ~ 'E'(f(X17),f(suc(X17)))
| ~ 'E'('0',f(X17))
| iLEQ(suc(X17),suc(X17)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44) ).
cnf(c52743,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)],[c52741,clause_44]) ).
cnf(c52810,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c52743,c52733]) ).
cnf(c52813,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c52810,c52721]) ).
cnf(c52815,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c52813,c52712]) ).
cnf(c52817,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c52815,c52790]) ).
cnf(c52819,plain,
$false,
inference(resolution,[status(thm)],[c52817,c52712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYO685-1 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.35 % Computer : n002.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed May 8 17:58:08 EDT 2024
% 0.12/0.35 % CPUTime :
% 56.45/56.66 % Version: 1.5
% 56.45/56.66 % SZS status Unsatisfiable
% 56.45/56.66 % SZS output start CNFRefutation
% See solution above
% 56.45/56.66
% 56.45/56.66 % Initial clauses : 47
% 56.45/56.66 % Processed clauses : 1151
% 56.45/56.66 % Factors computed : 107
% 56.45/56.66 % Resolvents computed: 52714
% 56.45/56.66 % Tautologies deleted: 21
% 56.45/56.66 % Forward subsumed : 1172
% 56.45/56.66 % Backward subsumed : 1075
% 56.45/56.66 % -------- CPU Time ---------
% 56.45/56.66 % User time : 56.045 s
% 56.45/56.66 % System time : 0.261 s
% 56.45/56.66 % Total time : 56.306 s
%------------------------------------------------------------------------------