%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO671-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:07 EDT 2024
% Result : Unsatisfiable 263.77s 264.09s
% Output : Refutation 263.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 23
% Syntax : Number of clauses : 88 ( 11 unt; 46 nHn; 70 RR)
% Number of literals : 347 ( 0 equ; 220 neg)
% Maximal clause size : 14 ( 3 avg)
% Maximal term depth : 4 ( 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 : 87 ( 3 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_211,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_211) ).
cnf(clause_307,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_307) ).
cnf(clause_326,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_326) ).
cnf(clause_421,axiom,
'LE'(f(X2),s(s(s('0')))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_421) ).
cnf(clause_261,axiom,
( ~ 'LE'(f(X12),s(s(s('0'))))
| 'E'(s(s('0')),f(X12))
| 'LE'(f(X12),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_261) ).
cnf(c4,plain,
( 'E'(s(s('0')),f(X13))
| 'LE'(f(X13),s(s('0'))) ),
inference(resolution,[status(thm)],[clause_261,clause_421]) ).
cnf(clause_26,axiom,
( ~ 'E'(s(s('0')),f(X28))
| ~ 'E'(s(s('0')),f(suc(X28)))
| 'E'(f(X28),f(suc(X28)))
| iLEQ(suc(X28),suc(X28)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26) ).
cnf(clause_183,axiom,
( ~ 'LE'(f(suc(X27)),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(X27)))
| 'LE'(f(X27),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_183) ).
cnf(c52,plain,
( 'E'(s(s('0')),f(suc(X29)))
| 'LE'(f(X29),s(s('0'))) ),
inference(resolution,[status(thm)],[clause_183,clause_421]) ).
cnf(c60,plain,
( 'LE'(f(X43),s(s('0')))
| ~ 'E'(s(s('0')),f(X43))
| 'E'(f(X43),f(suc(X43)))
| iLEQ(suc(X43),suc(X43)) ),
inference(resolution,[status(thm)],[c52,clause_26]) ).
cnf(c173,plain,
( 'LE'(f(X44),s(s('0')))
| 'E'(f(X44),f(suc(X44)))
| iLEQ(suc(X44),suc(X44)) ),
inference(resolution,[status(thm)],[c60,c4]) ).
cnf(clause_217,axiom,
( ~ 'LE'(f(suc(suc(X33))),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(suc(X33))))
| 'LE'(f(X33),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_217) ).
cnf(c90,plain,
( 'E'(s(s('0')),f(suc(suc(X34))))
| 'LE'(f(X34),s(s('0'))) ),
inference(resolution,[status(thm)],[clause_217,clause_421]) ).
cnf(clause_91,axiom,
( ~ 'E'(s(s('0')),f(suc(suc(X112))))
| ~ 'E'(s(s('0')),f(suc(X112)))
| ~ 'E'(f(X112),f(suc(X112)))
| ~ 'E'(s(s('0')),f(X112))
| iLEQ(suc(X112),suc(X112)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_91) ).
cnf(c1152,plain,
( ~ 'E'(s(s('0')),f(suc(X190)))
| ~ 'E'(f(X190),f(suc(X190)))
| ~ 'E'(s(s('0')),f(X190))
| iLEQ(suc(X190),suc(X190))
| 'LE'(f(X190),s(s('0'))) ),
inference(resolution,[status(thm)],[clause_91,c90]) ).
cnf(c2748,plain,
( ~ 'E'(f(X191),f(suc(X191)))
| ~ 'E'(s(s('0')),f(X191))
| iLEQ(suc(X191),suc(X191))
| 'LE'(f(X191),s(s('0'))) ),
inference(resolution,[status(thm)],[c1152,c52]) ).
cnf(c2847,plain,
( ~ 'E'(f(X192),f(suc(X192)))
| iLEQ(suc(X192),suc(X192))
| 'LE'(f(X192),s(s('0'))) ),
inference(resolution,[status(thm)],[c2748,c4]) ).
cnf(c2877,plain,
( iLEQ(suc(X193),suc(X193))
| 'LE'(f(X193),s(s('0'))) ),
inference(resolution,[status(thm)],[c2847,c173]) ).
cnf(clause_20,axiom,
( ~ 'E'(s(s('0')),f(X45))
| ~ 'E'(s(s('0')),f(suc(X47)))
| ~ 'E'(s(s('0')),f(X47))
| ~ 'E'(s(s('0')),f(suc(suc(X46))))
| ~ 'E'(s(s('0')),f(suc(X45)))
| ~ iLEQ(suc(X47),suc(X46))
| ~ 'E'(s(s('0')),f(X46))
| ~ 'E'(f(X46),f(suc(X46)))
| ~ 'E'(f(X45),f(suc(X45)))
| ~ 'E'(f(X47),f(suc(X47)))
| ~ iLEQ(suc(X45),suc(X47))
| ~ 'E'(s(s('0')),f(suc(suc(X45))))
| ~ 'E'(s(s('0')),f(suc(X46)))
| ~ 'E'(s(s('0')),f(suc(suc(X47)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
cnf(c188,plain,
( ~ 'E'(s(s('0')),f(X769))
| ~ 'E'(s(s('0')),f(suc(X768)))
| ~ 'E'(s(s('0')),f(X768))
| ~ 'E'(s(s('0')),f(suc(suc(X768))))
| ~ 'E'(s(s('0')),f(suc(X769)))
| ~ iLEQ(suc(X768),suc(X768))
| ~ 'E'(f(X768),f(suc(X768)))
| ~ 'E'(f(X769),f(suc(X769)))
| ~ iLEQ(suc(X769),suc(X768))
| ~ 'E'(s(s('0')),f(suc(suc(X769)))) ),
inference(factor,[status(thm)],[clause_20]) ).
cnf(c17990,plain,
( ~ 'E'(s(s('0')),f(X770))
| ~ 'E'(s(s('0')),f(suc(X770)))
| ~ 'E'(s(s('0')),f(suc(suc(X770))))
| ~ iLEQ(suc(X770),suc(X770))
| ~ 'E'(f(X770),f(suc(X770))) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c18142,plain,
( ~ 'E'(s(s('0')),f(X771))
| ~ 'E'(s(s('0')),f(suc(X771)))
| ~ iLEQ(suc(X771),suc(X771))
| ~ 'E'(f(X771),f(suc(X771)))
| 'LE'(f(X771),s(s('0'))) ),
inference(resolution,[status(thm)],[c17990,c90]) ).
cnf(c18240,plain,
( ~ 'E'(s(s('0')),f(X772))
| ~ iLEQ(suc(X772),suc(X772))
| ~ 'E'(f(X772),f(suc(X772)))
| 'LE'(f(X772),s(s('0'))) ),
inference(resolution,[status(thm)],[c18142,c52]) ).
cnf(clause_311,axiom,
( ~ 'E'(s(s('0')),f(X64))
| ~ 'E'(s(s('0')),f(suc(X66)))
| ~ 'E'(s(s('0')),f(X66))
| ~ 'E'(s(s('0')),f(suc(X64)))
| ~ iLEQ(suc(X66),suc(X65))
| ~ 'E'(s(s('0')),f(X65))
| ~ iLEQ(suc(X64),suc(X66))
| ~ 'E'(s(s('0')),f(suc(X65)))
| 'E'(f(X64),f(suc(X64)))
| 'E'(f(X66),f(suc(X66)))
| 'E'(f(X65),f(suc(X65))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_311) ).
cnf(c370,plain,
( ~ 'E'(s(s('0')),f(X1483))
| ~ 'E'(s(s('0')),f(suc(X1484)))
| ~ 'E'(s(s('0')),f(X1484))
| ~ 'E'(s(s('0')),f(suc(X1483)))
| ~ iLEQ(suc(X1484),suc(X1484))
| ~ iLEQ(suc(X1483),suc(X1484))
| 'E'(f(X1483),f(suc(X1483)))
| 'E'(f(X1484),f(suc(X1484))) ),
inference(factor,[status(thm)],[clause_311]) ).
cnf(c42590,plain,
( ~ 'E'(s(s('0')),f(X1485))
| ~ 'E'(s(s('0')),f(suc(X1485)))
| ~ iLEQ(suc(X1485),suc(X1485))
| 'E'(f(X1485),f(suc(X1485))) ),
inference(factor,[status(thm)],[c370]) ).
cnf(c42783,plain,
( ~ 'E'(s(s('0')),f(X1486))
| ~ iLEQ(suc(X1486),suc(X1486))
| 'E'(f(X1486),f(suc(X1486)))
| 'LE'(f(X1486),s(s('0'))) ),
inference(resolution,[status(thm)],[c42590,c52]) ).
cnf(c42827,plain,
( ~ iLEQ(suc(X1487),suc(X1487))
| 'E'(f(X1487),f(suc(X1487)))
| 'LE'(f(X1487),s(s('0'))) ),
inference(resolution,[status(thm)],[c42783,c4]) ).
cnf(c43026,plain,
( 'E'(f(X1488),f(suc(X1488)))
| 'LE'(f(X1488),s(s('0'))) ),
inference(resolution,[status(thm)],[c42827,c2877]) ).
cnf(c43106,plain,
( 'LE'(f(X1492),s(s('0')))
| ~ 'E'(s(s('0')),f(X1492))
| ~ iLEQ(suc(X1492),suc(X1492)) ),
inference(resolution,[status(thm)],[c43026,c18240]) ).
cnf(c43358,plain,
( 'LE'(f(X1493),s(s('0')))
| ~ iLEQ(suc(X1493),suc(X1493)) ),
inference(resolution,[status(thm)],[c43106,c4]) ).
cnf(c43556,plain,
'LE'(f(X1494),s(s('0'))),
inference(resolution,[status(thm)],[c43358,c2877]) ).
cnf(c43611,plain,
( 'E'(s('0'),f(X1495))
| 'LE'(f(X1495),s('0')) ),
inference(resolution,[status(thm)],[c43556,clause_326]) ).
cnf(clause_138,axiom,
( ~ 'LE'(f(suc(X10)),s(s('0')))
| 'E'(s('0'),f(suc(X10)))
| 'LE'(f(X10),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_138) ).
cnf(c43610,plain,
( 'E'(s('0'),f(suc(X1496)))
| 'LE'(f(X1496),s('0')) ),
inference(resolution,[status(thm)],[c43556,clause_138]) ).
cnf(clause_60,axiom,
( ~ 'E'(s('0'),f(X25))
| ~ 'E'(s('0'),f(suc(X25)))
| 'E'(f(X25),f(suc(X25)))
| iLEQ(suc(X25),suc(X25)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_60) ).
cnf(c43673,plain,
( 'LE'(f(X1533),s('0'))
| ~ 'E'(s('0'),f(X1533))
| 'E'(f(X1533),f(suc(X1533)))
| iLEQ(suc(X1533),suc(X1533)) ),
inference(resolution,[status(thm)],[c43610,clause_60]) ).
cnf(c45052,plain,
( 'LE'(f(X1534),s('0'))
| 'E'(f(X1534),f(suc(X1534)))
| iLEQ(suc(X1534),suc(X1534)) ),
inference(resolution,[status(thm)],[c43673,c43611]) ).
cnf(clause_37,axiom,
( ~ 'E'(s('0'),f(suc(suc(X77))))
| ~ 'E'(s('0'),f(suc(X77)))
| ~ 'E'(f(X77),f(suc(X77)))
| ~ 'E'(s('0'),f(X77))
| iLEQ(suc(X77),suc(X77)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_37) ).
cnf(clause_18,axiom,
( ~ 'LE'(f(suc(suc(X20))),s(s('0')))
| 'E'(s('0'),f(suc(suc(X20))))
| 'LE'(f(X20),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18) ).
cnf(c43612,plain,
( 'E'(s('0'),f(suc(suc(X1499))))
| 'LE'(f(X1499),s('0')) ),
inference(resolution,[status(thm)],[c43556,clause_18]) ).
cnf(c43847,plain,
( 'LE'(f(X1769),s('0'))
| ~ 'E'(s('0'),f(suc(X1769)))
| ~ 'E'(f(X1769),f(suc(X1769)))
| ~ 'E'(s('0'),f(X1769))
| iLEQ(suc(X1769),suc(X1769)) ),
inference(resolution,[status(thm)],[c43612,clause_37]) ).
cnf(c46897,plain,
( 'LE'(f(X1773),s('0'))
| ~ 'E'(s('0'),f(suc(X1773)))
| ~ 'E'(s('0'),f(X1773))
| iLEQ(suc(X1773),suc(X1773)) ),
inference(resolution,[status(thm)],[c43847,c45052]) ).
cnf(c46930,plain,
( 'LE'(f(X1774),s('0'))
| ~ 'E'(s('0'),f(X1774))
| iLEQ(suc(X1774),suc(X1774)) ),
inference(resolution,[status(thm)],[c46897,c43610]) ).
cnf(c46935,plain,
( 'LE'(f(X1775),s('0'))
| iLEQ(suc(X1775),suc(X1775)) ),
inference(resolution,[status(thm)],[c46930,c43611]) ).
cnf(clause_219,axiom,
( ~ 'E'(s('0'),f(X60))
| ~ 'E'(s('0'),f(suc(X60)))
| ~ 'E'(s('0'),f(suc(X58)))
| ~ iLEQ(suc(X58),suc(X59))
| ~ 'E'(s('0'),f(X59))
| ~ iLEQ(suc(X59),suc(X60))
| ~ 'E'(f(X59),f(suc(X59)))
| ~ 'E'(s('0'),f(suc(suc(X59))))
| ~ 'E'(s('0'),f(suc(X59)))
| ~ 'E'(s('0'),f(suc(suc(X58))))
| ~ 'E'(f(X58),f(suc(X58)))
| ~ 'E'(f(X60),f(suc(X60)))
| ~ 'E'(s('0'),f(X58))
| ~ 'E'(s('0'),f(suc(suc(X60)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_219) ).
cnf(c280,plain,
( ~ 'E'(s('0'),f(X1161))
| ~ 'E'(s('0'),f(suc(X1161)))
| ~ 'E'(s('0'),f(suc(X1162)))
| ~ iLEQ(suc(X1162),suc(X1161))
| ~ iLEQ(suc(X1161),suc(X1161))
| ~ 'E'(f(X1161),f(suc(X1161)))
| ~ 'E'(s('0'),f(suc(suc(X1161))))
| ~ 'E'(s('0'),f(suc(suc(X1162))))
| ~ 'E'(f(X1162),f(suc(X1162)))
| ~ 'E'(s('0'),f(X1162)) ),
inference(factor,[status(thm)],[clause_219]) ).
cnf(c30457,plain,
( ~ 'E'(s('0'),f(X1163))
| ~ 'E'(s('0'),f(suc(X1163)))
| ~ iLEQ(suc(X1163),suc(X1163))
| ~ 'E'(f(X1163),f(suc(X1163)))
| ~ 'E'(s('0'),f(suc(suc(X1163)))) ),
inference(factor,[status(thm)],[c280]) ).
cnf(c43868,plain,
( 'LE'(f(X1849),s('0'))
| ~ 'E'(s('0'),f(X1849))
| ~ 'E'(s('0'),f(suc(X1849)))
| ~ iLEQ(suc(X1849),suc(X1849))
| ~ 'E'(f(X1849),f(suc(X1849))) ),
inference(resolution,[status(thm)],[c43612,c30457]) ).
cnf(clause_340,axiom,
( ~ 'E'(s('0'),f(X132))
| ~ 'E'(s('0'),f(suc(X132)))
| ~ 'E'(s('0'),f(suc(X130)))
| ~ iLEQ(suc(X130),suc(X131))
| ~ 'E'(s('0'),f(X131))
| ~ iLEQ(suc(X131),suc(X132))
| ~ 'E'(s('0'),f(suc(X131)))
| ~ 'E'(s('0'),f(X130))
| 'E'(f(X130),f(suc(X130)))
| 'E'(f(X131),f(suc(X131)))
| 'E'(f(X132),f(suc(X132))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_340) ).
cnf(c1433,plain,
( ~ 'E'(s('0'),f(X5356))
| ~ 'E'(s('0'),f(suc(X5356)))
| ~ 'E'(s('0'),f(suc(X5357)))
| ~ iLEQ(suc(X5357),suc(X5356))
| ~ iLEQ(suc(X5356),suc(X5356))
| ~ 'E'(s('0'),f(X5357))
| 'E'(f(X5357),f(suc(X5357)))
| 'E'(f(X5356),f(suc(X5356))) ),
inference(factor,[status(thm)],[clause_340]) ).
cnf(c76996,plain,
( ~ 'E'(s('0'),f(X5358))
| ~ 'E'(s('0'),f(suc(X5358)))
| ~ iLEQ(suc(X5358),suc(X5358))
| 'E'(f(X5358),f(suc(X5358))) ),
inference(factor,[status(thm)],[c1433]) ).
cnf(c77090,plain,
( ~ 'E'(s('0'),f(X5381))
| ~ iLEQ(suc(X5381),suc(X5381))
| 'E'(f(X5381),f(suc(X5381)))
| 'LE'(f(X5381),s('0')) ),
inference(resolution,[status(thm)],[c76996,c43610]) ).
cnf(c79138,plain,
( ~ 'E'(s('0'),f(X5384))
| 'E'(f(X5384),f(suc(X5384)))
| 'LE'(f(X5384),s('0')) ),
inference(resolution,[status(thm)],[c77090,c46935]) ).
cnf(c79249,plain,
( 'E'(f(X5385),f(suc(X5385)))
| 'LE'(f(X5385),s('0')) ),
inference(resolution,[status(thm)],[c79138,c43611]) ).
cnf(c79373,plain,
( 'LE'(f(X5400),s('0'))
| ~ 'E'(s('0'),f(X5400))
| ~ 'E'(s('0'),f(suc(X5400)))
| ~ iLEQ(suc(X5400),suc(X5400)) ),
inference(resolution,[status(thm)],[c79249,c43868]) ).
cnf(c80674,plain,
( 'LE'(f(X5403),s('0'))
| ~ 'E'(s('0'),f(X5403))
| ~ iLEQ(suc(X5403),suc(X5403)) ),
inference(resolution,[status(thm)],[c79373,c43610]) ).
cnf(c80784,plain,
( 'LE'(f(X5404),s('0'))
| ~ 'E'(s('0'),f(X5404)) ),
inference(resolution,[status(thm)],[c80674,c46935]) ).
cnf(c80836,plain,
'LE'(f(X5405),s('0')),
inference(resolution,[status(thm)],[c80784,c43611]) ).
cnf(c80893,plain,
( 'E'('0',f(X5406))
| 'LE'(f(X5406),'0') ),
inference(resolution,[status(thm)],[c80836,clause_307]) ).
cnf(c80937,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c80893,clause_211]) ).
cnf(clause_353,axiom,
( ~ 'LE'(f(suc(X4)),s('0'))
| 'E'('0',f(suc(X4)))
| 'LE'(f(X4),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_353) ).
cnf(c80894,plain,
( 'E'('0',f(suc(X5410)))
| 'LE'(f(X5410),'0') ),
inference(resolution,[status(thm)],[c80836,clause_353]) ).
cnf(c80986,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c80894,clause_211]) ).
cnf(clause_72,axiom,
( ~ 'LE'(f(suc(suc(X9))),s('0'))
| 'E'('0',f(suc(suc(X9))))
| 'LE'(f(X9),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_72) ).
cnf(c80892,plain,
( 'E'('0',f(suc(suc(X5411))))
| 'LE'(f(X5411),'0') ),
inference(resolution,[status(thm)],[c80836,clause_72]) ).
cnf(c81034,plain,
'E'('0',f(suc(suc(z)))),
inference(resolution,[status(thm)],[c80892,clause_211]) ).
cnf(clause_116,axiom,
( ~ 'E'('0',f(suc(suc(X75))))
| ~ 'E'('0',f(suc(X75)))
| ~ 'E'(f(X75),f(suc(X75)))
| ~ 'E'('0',f(X75))
| iLEQ(suc(X75),suc(X75)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_116) ).
cnf(clause_86,axiom,
( ~ 'E'('0',f(X11))
| ~ 'E'('0',f(suc(X11)))
| 'E'(f(X11),f(suc(X11)))
| iLEQ(suc(X11),suc(X11)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_86) ).
cnf(c80990,plain,
( ~ 'E'('0',f(z))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c80986,clause_86]) ).
cnf(c81060,plain,
( 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c80990,c80937]) ).
cnf(c81077,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)],[c81060,clause_116]) ).
cnf(c81924,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c81077,c81034]) ).
cnf(c81927,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c81924,c80986]) ).
cnf(c81930,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c81927,c80937]) ).
cnf(clause_83,axiom,
( ~ 'E'('0',f(X70))
| ~ 'E'('0',f(suc(suc(X70))))
| ~ 'E'('0',f(suc(suc(X72))))
| ~ 'E'('0',f(suc(X70)))
| ~ 'E'('0',f(X71))
| ~ 'E'('0',f(suc(suc(X71))))
| ~ 'E'(f(X70),f(suc(X70)))
| ~ 'E'('0',f(suc(X71)))
| ~ 'E'(f(X71),f(suc(X71)))
| ~ 'E'('0',f(suc(X72)))
| ~ 'E'('0',f(X72))
| ~ 'E'(f(X72),f(suc(X72)))
| ~ iLEQ(suc(X71),suc(X70))
| ~ iLEQ(suc(X70),suc(X72)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_83) ).
cnf(c450,plain,
( ~ 'E'('0',f(X1813))
| ~ 'E'('0',f(suc(suc(X1813))))
| ~ 'E'('0',f(suc(X1813)))
| ~ 'E'('0',f(X1814))
| ~ 'E'('0',f(suc(suc(X1814))))
| ~ 'E'(f(X1813),f(suc(X1813)))
| ~ 'E'('0',f(suc(X1814)))
| ~ 'E'(f(X1814),f(suc(X1814)))
| ~ iLEQ(suc(X1814),suc(X1813))
| ~ iLEQ(suc(X1813),suc(X1813)) ),
inference(factor,[status(thm)],[clause_83]) ).
cnf(c47318,plain,
( ~ 'E'('0',f(X1834))
| ~ 'E'('0',f(suc(suc(X1834))))
| ~ 'E'('0',f(suc(X1834)))
| ~ 'E'(f(X1834),f(suc(X1834)))
| ~ iLEQ(suc(X1834),suc(X1834)) ),
inference(factor,[status(thm)],[c450]) ).
cnf(clause_16,axiom,
( ~ 'E'('0',f(X52))
| ~ 'E'('0',f(suc(X52)))
| ~ 'E'('0',f(X53))
| ~ 'E'('0',f(suc(X53)))
| ~ 'E'('0',f(suc(X54)))
| ~ 'E'('0',f(X54))
| ~ iLEQ(suc(X53),suc(X52))
| ~ iLEQ(suc(X52),suc(X54))
| 'E'(f(X53),f(suc(X53)))
| 'E'(f(X52),f(suc(X52)))
| 'E'(f(X54),f(suc(X54))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
cnf(c244,plain,
( ~ 'E'('0',f(X55))
| ~ 'E'('0',f(suc(X55)))
| ~ iLEQ(suc(X55),suc(X55))
| 'E'(f(X55),f(suc(X55))) ),
inference(factor,[status(thm)],[clause_16]) ).
cnf(c81080,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c81060,c244]) ).
cnf(c81089,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c81080,c80986]) ).
cnf(c81092,plain,
'E'(f(z),f(suc(z))),
inference(resolution,[status(thm)],[c81089,c80937]) ).
cnf(c81110,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c81092,c47318]) ).
cnf(c81936,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c81110,c81034]) ).
cnf(c81939,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c81936,c81930]) ).
cnf(c81945,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c81939,c80986]) ).
cnf(c81948,plain,
$false,
inference(resolution,[status(thm)],[c81945,c80937]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYO671-1 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n006.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 18:04:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 263.77/264.09 % Version: 1.5
% 263.77/264.09 % SZS status Unsatisfiable
% 263.77/264.09 % SZS output start CNFRefutation
% See solution above
% 263.77/264.09
% 263.77/264.09 % Initial clauses : 41
% 263.77/264.09 % Processed clauses : 1533
% 263.77/264.09 % Factors computed : 1033
% 263.77/264.09 % Resolvents computed: 80916
% 263.77/264.09 % Tautologies deleted: 254
% 263.77/264.09 % Forward subsumed : 5977
% 263.77/264.09 % Backward subsumed : 1380
% 263.77/264.09 % -------- CPU Time ---------
% 263.77/264.09 % User time : 263.238 s
% 263.77/264.09 % System time : 0.454 s
% 263.77/264.09 % Total time : 263.692 s
%------------------------------------------------------------------------------