%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO651-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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 186.64s 186.87s
% Output : Refutation 186.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 15
% Syntax : Number of clauses : 73 ( 4 unt; 54 nHn; 59 RR)
% Number of literals : 424 ( 0 equ; 286 neg)
% Maximal clause size : 26 ( 5 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 : 83 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1829,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1829) ).
cnf(clause_3530,axiom,
'LE'(f(X2),s('0')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3530) ).
cnf(clause_2386,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2386) ).
cnf(c0,plain,
( 'E'('0',f(X4))
| 'LE'(f(X4),'0') ),
inference(resolution,[status(thm)],[clause_2386,clause_3530]) ).
cnf(clause_2650,axiom,
( ~ 'LE'(f(suc(X8)),s('0'))
| 'E'('0',f(suc(X8)))
| 'LE'(f(X8),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2650) ).
cnf(c11,plain,
( 'E'('0',f(suc(X9)))
| 'LE'(f(X9),'0') ),
inference(resolution,[status(thm)],[clause_2650,clause_3530]) ).
cnf(clause_3112,axiom,
( ~ 'LE'(f(suc(suc(X10))),s('0'))
| 'E'('0',f(suc(suc(X10))))
| 'LE'(f(X10),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3112) ).
cnf(c14,plain,
( 'E'('0',f(suc(suc(X11))))
| 'LE'(f(X11),'0') ),
inference(resolution,[status(thm)],[clause_3112,clause_3530]) ).
cnf(clause_636,axiom,
( ~ 'E'('0',f(X15))
| ~ 'E'('0',f(suc(X15)))
| 'E'(f(X15),f(suc(X15)))
| iLEQ(suc(X15),suc(X15)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_636) ).
cnf(c32,plain,
( ~ 'E'('0',f(X17))
| 'E'(f(X17),f(suc(X17)))
| iLEQ(suc(X17),suc(X17))
| 'LE'(f(X17),'0') ),
inference(resolution,[status(thm)],[clause_636,c11]) ).
cnf(c39,plain,
( 'E'(f(X18),f(suc(X18)))
| iLEQ(suc(X18),suc(X18))
| 'LE'(f(X18),'0') ),
inference(resolution,[status(thm)],[c32,c0]) ).
cnf(clause_2887,axiom,
( ~ iLEQ(suc(X143),suc(X144))
| ~ 'E'('0',f(suc(X142)))
| ~ 'E'('0',f(suc(X143)))
| ~ 'E'('0',f(X143))
| ~ iLEQ(suc(X144),suc(X142))
| ~ 'E'('0',f(X144))
| ~ 'E'('0',f(X142))
| ~ 'E'('0',f(suc(X144)))
| 'E'(f(X143),f(suc(X143)))
| 'E'(f(X144),f(suc(X144)))
| 'E'(f(X142),f(suc(X142))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2887) ).
cnf(c388,plain,
( ~ iLEQ(suc(X146),suc(X147))
| ~ 'E'('0',f(suc(X147)))
| ~ 'E'('0',f(suc(X146)))
| ~ 'E'('0',f(X146))
| ~ iLEQ(suc(X147),suc(X147))
| ~ 'E'('0',f(X147))
| 'E'(f(X146),f(suc(X146)))
| 'E'(f(X147),f(suc(X147))) ),
inference(factor,[status(thm)],[clause_2887]) ).
cnf(c401,plain,
( ~ iLEQ(suc(X148),suc(X148))
| ~ 'E'('0',f(suc(X148)))
| ~ 'E'('0',f(X148))
| 'E'(f(X148),f(suc(X148))) ),
inference(factor,[status(thm)],[c388]) ).
cnf(c419,plain,
( ~ iLEQ(suc(X152),suc(X152))
| ~ 'E'('0',f(X152))
| 'E'(f(X152),f(suc(X152)))
| 'LE'(f(X152),'0') ),
inference(resolution,[status(thm)],[c401,c11]) ).
cnf(c454,plain,
( ~ 'E'('0',f(X156))
| 'E'(f(X156),f(suc(X156)))
| 'LE'(f(X156),'0') ),
inference(resolution,[status(thm)],[c419,c39]) ).
cnf(c480,plain,
( 'E'(f(X157),f(suc(X157)))
| 'LE'(f(X157),'0') ),
inference(resolution,[status(thm)],[c454,c0]) ).
cnf(clause_3293,axiom,
( ~ 'LE'(f(suc(suc(suc(X24)))),s('0'))
| 'E'('0',f(suc(suc(suc(X24)))))
| 'LE'(f(X24),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3293) ).
cnf(c51,plain,
( 'E'('0',f(suc(suc(suc(X25)))))
| 'LE'(f(X25),'0') ),
inference(resolution,[status(thm)],[clause_3293,clause_3530]) ).
cnf(clause_2993,axiom,
( ~ 'E'('0',f(suc(suc(X61))))
| ~ 'E'('0',f(suc(X61)))
| ~ 'E'(f(X61),f(suc(X61)))
| ~ 'E'('0',f(X61))
| 'E'(f(X61),f(suc(suc(X61))))
| iLEQ(suc(X61),suc(X61)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2993) ).
cnf(c172,plain,
( ~ 'E'('0',f(suc(suc(X68))))
| ~ 'E'('0',f(suc(X68)))
| ~ 'E'('0',f(X68))
| 'E'(f(X68),f(suc(suc(X68))))
| iLEQ(suc(X68),suc(X68))
| 'LE'(f(X68),'0') ),
inference(resolution,[status(thm)],[clause_2993,c39]) ).
cnf(c215,plain,
( ~ 'E'('0',f(suc(X72)))
| ~ 'E'('0',f(X72))
| 'E'(f(X72),f(suc(suc(X72))))
| iLEQ(suc(X72),suc(X72))
| 'LE'(f(X72),'0') ),
inference(resolution,[status(thm)],[c172,c14]) ).
cnf(c228,plain,
( ~ 'E'('0',f(X73))
| 'E'(f(X73),f(suc(suc(X73))))
| iLEQ(suc(X73),suc(X73))
| 'LE'(f(X73),'0') ),
inference(resolution,[status(thm)],[c215,c11]) ).
cnf(c232,plain,
( 'E'(f(X74),f(suc(suc(X74))))
| iLEQ(suc(X74),suc(X74))
| 'LE'(f(X74),'0') ),
inference(resolution,[status(thm)],[c228,c0]) ).
cnf(clause_3827,axiom,
( ~ 'E'('0',f(suc(suc(suc(X212)))))
| ~ 'E'('0',f(suc(X212)))
| ~ 'E'('0',f(suc(suc(X212))))
| ~ 'E'('0',f(X212))
| ~ 'E'(f(X212),f(suc(suc(X212))))
| ~ 'E'(f(X212),f(suc(X212)))
| 'E'(f(X212),f(suc(suc(suc(X212)))))
| iLEQ(suc(X212),suc(X212)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3827) ).
cnf(c656,plain,
( ~ 'E'('0',f(suc(suc(suc(X356)))))
| ~ 'E'('0',f(suc(X356)))
| ~ 'E'('0',f(suc(suc(X356))))
| ~ 'E'('0',f(X356))
| ~ 'E'(f(X356),f(suc(X356)))
| 'E'(f(X356),f(suc(suc(suc(X356)))))
| iLEQ(suc(X356),suc(X356))
| 'LE'(f(X356),'0') ),
inference(resolution,[status(thm)],[clause_3827,c232]) ).
cnf(c1025,plain,
( ~ 'E'('0',f(suc(X357)))
| ~ 'E'('0',f(suc(suc(X357))))
| ~ 'E'('0',f(X357))
| ~ 'E'(f(X357),f(suc(X357)))
| 'E'(f(X357),f(suc(suc(suc(X357)))))
| iLEQ(suc(X357),suc(X357))
| 'LE'(f(X357),'0') ),
inference(resolution,[status(thm)],[c656,c51]) ).
cnf(c1033,plain,
( ~ 'E'('0',f(suc(X358)))
| ~ 'E'('0',f(suc(suc(X358))))
| ~ 'E'('0',f(X358))
| 'E'(f(X358),f(suc(suc(suc(X358)))))
| iLEQ(suc(X358),suc(X358))
| 'LE'(f(X358),'0') ),
inference(resolution,[status(thm)],[c1025,c480]) ).
cnf(c1041,plain,
( ~ 'E'('0',f(suc(X359)))
| ~ 'E'('0',f(X359))
| 'E'(f(X359),f(suc(suc(suc(X359)))))
| iLEQ(suc(X359),suc(X359))
| 'LE'(f(X359),'0') ),
inference(resolution,[status(thm)],[c1033,c14]) ).
cnf(c1054,plain,
( ~ 'E'('0',f(X360))
| 'E'(f(X360),f(suc(suc(suc(X360)))))
| iLEQ(suc(X360),suc(X360))
| 'LE'(f(X360),'0') ),
inference(resolution,[status(thm)],[c1041,c11]) ).
cnf(c1066,plain,
( 'E'(f(X363),f(suc(suc(suc(X363)))))
| iLEQ(suc(X363),suc(X363))
| 'LE'(f(X363),'0') ),
inference(resolution,[status(thm)],[c1054,c0]) ).
cnf(clause_1772,axiom,
( ~ 'E'('0',f(suc(suc(suc(X16)))))
| ~ 'E'('0',f(suc(X16)))
| ~ 'E'(f(X16),f(suc(suc(suc(X16)))))
| ~ 'E'('0',f(suc(suc(X16))))
| ~ 'E'('0',f(X16))
| ~ 'E'(f(X16),f(suc(suc(X16))))
| ~ 'E'(f(X16),f(suc(X16)))
| ~ 'E'('0',f(suc(suc(suc(suc(X16))))))
| iLEQ(suc(X16),suc(X16)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1772) ).
cnf(clause_619,axiom,
( ~ 'LE'(f(suc(suc(suc(suc(X29))))),s('0'))
| 'E'('0',f(suc(suc(suc(suc(X29))))))
| 'LE'(f(X29),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_619) ).
cnf(c71,plain,
( 'E'('0',f(suc(suc(suc(suc(X30))))))
| 'LE'(f(X30),'0') ),
inference(resolution,[status(thm)],[clause_619,clause_3530]) ).
cnf(c74,plain,
( 'LE'(f(X434),'0')
| ~ 'E'('0',f(suc(suc(suc(X434)))))
| ~ 'E'('0',f(suc(X434)))
| ~ 'E'(f(X434),f(suc(suc(suc(X434)))))
| ~ 'E'('0',f(suc(suc(X434))))
| ~ 'E'('0',f(X434))
| ~ 'E'(f(X434),f(suc(suc(X434))))
| ~ 'E'(f(X434),f(suc(X434)))
| iLEQ(suc(X434),suc(X434)) ),
inference(resolution,[status(thm)],[c71,clause_1772]) ).
cnf(c1195,plain,
( 'LE'(f(X437),'0')
| ~ 'E'('0',f(suc(suc(suc(X437)))))
| ~ 'E'('0',f(suc(X437)))
| ~ 'E'('0',f(suc(suc(X437))))
| ~ 'E'('0',f(X437))
| ~ 'E'(f(X437),f(suc(suc(X437))))
| ~ 'E'(f(X437),f(suc(X437)))
| iLEQ(suc(X437),suc(X437)) ),
inference(resolution,[status(thm)],[c74,c1066]) ).
cnf(c1202,plain,
( 'LE'(f(X438),'0')
| ~ 'E'('0',f(suc(suc(suc(X438)))))
| ~ 'E'('0',f(suc(X438)))
| ~ 'E'('0',f(suc(suc(X438))))
| ~ 'E'('0',f(X438))
| ~ 'E'(f(X438),f(suc(X438)))
| iLEQ(suc(X438),suc(X438)) ),
inference(resolution,[status(thm)],[c1195,c232]) ).
cnf(c1208,plain,
( 'LE'(f(X439),'0')
| ~ '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)) ),
inference(resolution,[status(thm)],[c1202,c51]) ).
cnf(c1216,plain,
( 'LE'(f(X440),'0')
| ~ 'E'('0',f(suc(X440)))
| ~ 'E'('0',f(suc(suc(X440))))
| ~ 'E'('0',f(X440))
| iLEQ(suc(X440),suc(X440)) ),
inference(resolution,[status(thm)],[c1208,c480]) ).
cnf(c1224,plain,
( 'LE'(f(X441),'0')
| ~ 'E'('0',f(suc(X441)))
| ~ 'E'('0',f(X441))
| iLEQ(suc(X441),suc(X441)) ),
inference(resolution,[status(thm)],[c1216,c14]) ).
cnf(c1237,plain,
( 'LE'(f(X444),'0')
| ~ 'E'('0',f(X444))
| iLEQ(suc(X444),suc(X444)) ),
inference(resolution,[status(thm)],[c1224,c11]) ).
cnf(c1255,plain,
( 'LE'(f(X445),'0')
| iLEQ(suc(X445),suc(X445)) ),
inference(resolution,[status(thm)],[c1237,c0]) ).
cnf(clause_2612,axiom,
( ~ 'E'('0',f(suc(suc(X119))))
| ~ iLEQ(suc(X118),suc(X119))
| ~ 'E'('0',f(suc(X117)))
| ~ 'E'('0',f(suc(X118)))
| ~ 'E'(f(X117),f(suc(X117)))
| ~ 'E'('0',f(suc(suc(X118))))
| ~ 'E'('0',f(X118))
| ~ 'E'('0',f(suc(suc(X117))))
| ~ iLEQ(suc(X119),suc(X117))
| ~ 'E'(f(X118),f(suc(X118)))
| ~ 'E'('0',f(X119))
| ~ 'E'('0',f(X117))
| ~ 'E'(f(X119),f(suc(X119)))
| ~ 'E'('0',f(suc(X119)))
| 'E'(f(X118),f(suc(suc(X118))))
| 'E'(f(X119),f(suc(suc(X119))))
| 'E'(f(X117),f(suc(suc(X117)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2612) ).
cnf(c323,plain,
( ~ 'E'('0',f(suc(suc(X1372))))
| ~ iLEQ(suc(X1373),suc(X1372))
| ~ 'E'('0',f(suc(X1372)))
| ~ 'E'('0',f(suc(X1373)))
| ~ 'E'(f(X1372),f(suc(X1372)))
| ~ 'E'('0',f(suc(suc(X1373))))
| ~ 'E'('0',f(X1373))
| ~ iLEQ(suc(X1372),suc(X1372))
| ~ 'E'(f(X1373),f(suc(X1373)))
| ~ 'E'('0',f(X1372))
| 'E'(f(X1373),f(suc(suc(X1373))))
| 'E'(f(X1372),f(suc(suc(X1372)))) ),
inference(factor,[status(thm)],[clause_2612]) ).
cnf(c2850,plain,
( ~ 'E'('0',f(suc(suc(X1374))))
| ~ iLEQ(suc(X1374),suc(X1374))
| ~ 'E'('0',f(suc(X1374)))
| ~ 'E'(f(X1374),f(suc(X1374)))
| ~ 'E'('0',f(X1374))
| 'E'(f(X1374),f(suc(suc(X1374)))) ),
inference(factor,[status(thm)],[c323]) ).
cnf(c2863,plain,
( ~ 'E'('0',f(suc(suc(X1375))))
| ~ iLEQ(suc(X1375),suc(X1375))
| ~ 'E'('0',f(suc(X1375)))
| ~ 'E'('0',f(X1375))
| 'E'(f(X1375),f(suc(suc(X1375))))
| 'LE'(f(X1375),'0') ),
inference(resolution,[status(thm)],[c2850,c480]) ).
cnf(c2871,plain,
( ~ iLEQ(suc(X1376),suc(X1376))
| ~ 'E'('0',f(suc(X1376)))
| ~ 'E'('0',f(X1376))
| 'E'(f(X1376),f(suc(suc(X1376))))
| 'LE'(f(X1376),'0') ),
inference(resolution,[status(thm)],[c2863,c14]) ).
cnf(c2884,plain,
( ~ iLEQ(suc(X1380),suc(X1380))
| ~ 'E'('0',f(X1380))
| 'E'(f(X1380),f(suc(suc(X1380))))
| 'LE'(f(X1380),'0') ),
inference(resolution,[status(thm)],[c2871,c11]) ).
cnf(c2889,plain,
( ~ 'E'('0',f(X1381))
| 'E'(f(X1381),f(suc(suc(X1381))))
| 'LE'(f(X1381),'0') ),
inference(resolution,[status(thm)],[c2884,c1255]) ).
cnf(c2914,plain,
( 'E'(f(X1382),f(suc(suc(X1382))))
| 'LE'(f(X1382),'0') ),
inference(resolution,[status(thm)],[c2889,c0]) ).
cnf(clause_3274,axiom,
( ~ 'E'('0',f(suc(suc(suc(X92)))))
| ~ 'E'('0',f(suc(suc(X93))))
| ~ iLEQ(suc(X92),suc(X93))
| ~ 'E'('0',f(suc(X91)))
| ~ 'E'('0',f(suc(X92)))
| ~ 'E'(f(X91),f(suc(X91)))
| ~ 'E'('0',f(suc(suc(X92))))
| ~ 'E'('0',f(X92))
| ~ 'E'('0',f(suc(suc(X91))))
| ~ 'E'('0',f(suc(suc(suc(X93)))))
| ~ 'E'(f(X92),f(suc(suc(X92))))
| ~ iLEQ(suc(X93),suc(X91))
| ~ 'E'(f(X92),f(suc(X92)))
| ~ 'E'('0',f(X93))
| ~ 'E'(f(X91),f(suc(suc(X91))))
| ~ 'E'(f(X93),f(suc(suc(X93))))
| ~ 'E'('0',f(suc(suc(suc(X91)))))
| ~ 'E'('0',f(X91))
| ~ 'E'(f(X93),f(suc(X93)))
| ~ 'E'('0',f(suc(X93)))
| 'E'(f(X92),f(suc(suc(suc(X92)))))
| 'E'(f(X93),f(suc(suc(suc(X93)))))
| 'E'(f(X91),f(suc(suc(suc(X91))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3274) ).
cnf(c261,plain,
( ~ 'E'('0',f(suc(suc(suc(X1261)))))
| ~ 'E'('0',f(suc(suc(X1262))))
| ~ iLEQ(suc(X1261),suc(X1262))
| ~ 'E'('0',f(suc(X1261)))
| ~ 'E'(f(X1261),f(suc(X1261)))
| ~ 'E'('0',f(suc(suc(X1261))))
| ~ 'E'('0',f(X1261))
| ~ 'E'('0',f(suc(suc(suc(X1262)))))
| ~ 'E'(f(X1261),f(suc(suc(X1261))))
| ~ iLEQ(suc(X1262),suc(X1261))
| ~ 'E'('0',f(X1262))
| ~ 'E'(f(X1262),f(suc(suc(X1262))))
| ~ 'E'(f(X1262),f(suc(X1262)))
| ~ 'E'('0',f(suc(X1262)))
| 'E'(f(X1261),f(suc(suc(suc(X1261)))))
| 'E'(f(X1262),f(suc(suc(suc(X1262))))) ),
inference(factor,[status(thm)],[clause_3274]) ).
cnf(c2673,plain,
( ~ 'E'('0',f(suc(suc(suc(X1293)))))
| ~ 'E'('0',f(suc(suc(X1293))))
| ~ iLEQ(suc(X1293),suc(X1293))
| ~ 'E'('0',f(suc(X1293)))
| ~ 'E'(f(X1293),f(suc(X1293)))
| ~ 'E'('0',f(X1293))
| ~ 'E'(f(X1293),f(suc(suc(X1293))))
| 'E'(f(X1293),f(suc(suc(suc(X1293))))) ),
inference(factor,[status(thm)],[c261]) ).
cnf(c2991,plain,
( 'LE'(f(X1477),'0')
| ~ 'E'('0',f(suc(suc(suc(X1477)))))
| ~ 'E'('0',f(suc(suc(X1477))))
| ~ iLEQ(suc(X1477),suc(X1477))
| ~ 'E'('0',f(suc(X1477)))
| ~ 'E'(f(X1477),f(suc(X1477)))
| ~ 'E'('0',f(X1477))
| 'E'(f(X1477),f(suc(suc(suc(X1477))))) ),
inference(resolution,[status(thm)],[c2914,c2673]) ).
cnf(c3300,plain,
( 'LE'(f(X1478),'0')
| ~ 'E'('0',f(suc(suc(X1478))))
| ~ iLEQ(suc(X1478),suc(X1478))
| ~ 'E'('0',f(suc(X1478)))
| ~ 'E'(f(X1478),f(suc(X1478)))
| ~ 'E'('0',f(X1478))
| 'E'(f(X1478),f(suc(suc(suc(X1478))))) ),
inference(resolution,[status(thm)],[c2991,c51]) ).
cnf(c3308,plain,
( 'LE'(f(X1479),'0')
| ~ 'E'('0',f(suc(suc(X1479))))
| ~ iLEQ(suc(X1479),suc(X1479))
| ~ 'E'('0',f(suc(X1479)))
| ~ 'E'('0',f(X1479))
| 'E'(f(X1479),f(suc(suc(suc(X1479))))) ),
inference(resolution,[status(thm)],[c3300,c480]) ).
cnf(c3316,plain,
( 'LE'(f(X1482),'0')
| ~ iLEQ(suc(X1482),suc(X1482))
| ~ 'E'('0',f(suc(X1482)))
| ~ 'E'('0',f(X1482))
| 'E'(f(X1482),f(suc(suc(suc(X1482))))) ),
inference(resolution,[status(thm)],[c3308,c14]) ).
cnf(c3336,plain,
( 'LE'(f(X1483),'0')
| ~ iLEQ(suc(X1483),suc(X1483))
| ~ 'E'('0',f(X1483))
| 'E'(f(X1483),f(suc(suc(suc(X1483))))) ),
inference(resolution,[status(thm)],[c3316,c11]) ).
cnf(c3341,plain,
( 'LE'(f(X1484),'0')
| ~ 'E'('0',f(X1484))
| 'E'(f(X1484),f(suc(suc(suc(X1484))))) ),
inference(resolution,[status(thm)],[c3336,c1255]) ).
cnf(c3364,plain,
( 'LE'(f(X1485),'0')
| 'E'(f(X1485),f(suc(suc(suc(X1485))))) ),
inference(resolution,[status(thm)],[c3341,c0]) ).
cnf(clause_3360,axiom,
( ~ 'E'('0',f(suc(suc(suc(X293)))))
| ~ 'E'('0',f(suc(suc(X294))))
| ~ iLEQ(suc(X293),suc(X294))
| ~ 'E'('0',f(suc(X292)))
| ~ 'E'('0',f(suc(X293)))
| ~ 'E'(f(X292),f(suc(X292)))
| ~ 'E'(f(X293),f(suc(suc(suc(X293)))))
| ~ 'E'('0',f(suc(suc(X293))))
| ~ 'E'('0',f(X293))
| ~ 'E'('0',f(suc(suc(X292))))
| ~ 'E'('0',f(suc(suc(suc(X294)))))
| ~ 'E'(f(X293),f(suc(suc(X293))))
| ~ iLEQ(suc(X294),suc(X292))
| ~ 'E'(f(X293),f(suc(X293)))
| ~ 'E'('0',f(suc(suc(suc(suc(X294))))))
| ~ 'E'(f(X294),f(suc(suc(suc(X294)))))
| ~ 'E'(f(X292),f(suc(suc(suc(X292)))))
| ~ 'E'('0',f(X294))
| ~ 'E'(f(X292),f(suc(suc(X292))))
| ~ 'E'(f(X294),f(suc(suc(X294))))
| ~ 'E'('0',f(suc(suc(suc(X292)))))
| ~ 'E'('0',f(X292))
| ~ 'E'('0',f(suc(suc(suc(suc(X292))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X293))))))
| ~ 'E'(f(X294),f(suc(X294)))
| ~ 'E'('0',f(suc(X294))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3360) ).
cnf(c894,plain,
( ~ 'E'('0',f(suc(suc(suc(X4062)))))
| ~ 'E'('0',f(suc(suc(X4062))))
| ~ iLEQ(suc(X4062),suc(X4062))
| ~ 'E'('0',f(suc(X4061)))
| ~ 'E'('0',f(suc(X4062)))
| ~ 'E'(f(X4061),f(suc(X4061)))
| ~ 'E'(f(X4062),f(suc(suc(suc(X4062)))))
| ~ 'E'('0',f(X4062))
| ~ 'E'('0',f(suc(suc(X4061))))
| ~ 'E'(f(X4062),f(suc(suc(X4062))))
| ~ iLEQ(suc(X4062),suc(X4061))
| ~ 'E'(f(X4062),f(suc(X4062)))
| ~ 'E'('0',f(suc(suc(suc(suc(X4062))))))
| ~ 'E'(f(X4061),f(suc(suc(suc(X4061)))))
| ~ 'E'(f(X4061),f(suc(suc(X4061))))
| ~ 'E'('0',f(suc(suc(suc(X4061)))))
| ~ 'E'('0',f(X4061))
| ~ 'E'('0',f(suc(suc(suc(suc(X4061)))))) ),
inference(factor,[status(thm)],[clause_3360]) ).
cnf(c9068,plain,
( ~ 'E'('0',f(suc(suc(suc(X4063)))))
| ~ 'E'('0',f(suc(suc(X4063))))
| ~ iLEQ(suc(X4063),suc(X4063))
| ~ 'E'('0',f(suc(X4063)))
| ~ 'E'(f(X4063),f(suc(X4063)))
| ~ 'E'(f(X4063),f(suc(suc(suc(X4063)))))
| ~ 'E'('0',f(X4063))
| ~ 'E'(f(X4063),f(suc(suc(X4063))))
| ~ 'E'('0',f(suc(suc(suc(suc(X4063)))))) ),
inference(factor,[status(thm)],[c894]) ).
cnf(c9078,plain,
( ~ 'E'('0',f(suc(suc(suc(X4064)))))
| ~ 'E'('0',f(suc(suc(X4064))))
| ~ iLEQ(suc(X4064),suc(X4064))
| ~ 'E'('0',f(suc(X4064)))
| ~ 'E'(f(X4064),f(suc(X4064)))
| ~ 'E'(f(X4064),f(suc(suc(suc(X4064)))))
| ~ 'E'('0',f(X4064))
| ~ 'E'(f(X4064),f(suc(suc(X4064))))
| 'LE'(f(X4064),'0') ),
inference(resolution,[status(thm)],[c9068,c71]) ).
cnf(c9086,plain,
( ~ 'E'('0',f(suc(suc(suc(X4065)))))
| ~ 'E'('0',f(suc(suc(X4065))))
| ~ iLEQ(suc(X4065),suc(X4065))
| ~ 'E'('0',f(suc(X4065)))
| ~ 'E'(f(X4065),f(suc(X4065)))
| ~ 'E'('0',f(X4065))
| ~ 'E'(f(X4065),f(suc(suc(X4065))))
| 'LE'(f(X4065),'0') ),
inference(resolution,[status(thm)],[c9078,c3364]) ).
cnf(c9097,plain,
( ~ 'E'('0',f(suc(suc(suc(X4066)))))
| ~ 'E'('0',f(suc(suc(X4066))))
| ~ iLEQ(suc(X4066),suc(X4066))
| ~ 'E'('0',f(suc(X4066)))
| ~ 'E'(f(X4066),f(suc(X4066)))
| ~ 'E'('0',f(X4066))
| 'LE'(f(X4066),'0') ),
inference(resolution,[status(thm)],[c9086,c2914]) ).
cnf(c9104,plain,
( ~ 'E'('0',f(suc(suc(X4067))))
| ~ iLEQ(suc(X4067),suc(X4067))
| ~ 'E'('0',f(suc(X4067)))
| ~ 'E'(f(X4067),f(suc(X4067)))
| ~ 'E'('0',f(X4067))
| 'LE'(f(X4067),'0') ),
inference(resolution,[status(thm)],[c9097,c51]) ).
cnf(c9112,plain,
( ~ 'E'('0',f(suc(suc(X4070))))
| ~ iLEQ(suc(X4070),suc(X4070))
| ~ 'E'('0',f(suc(X4070)))
| ~ 'E'('0',f(X4070))
| 'LE'(f(X4070),'0') ),
inference(resolution,[status(thm)],[c9104,c480]) ).
cnf(c9126,plain,
( ~ iLEQ(suc(X4071),suc(X4071))
| ~ 'E'('0',f(suc(X4071)))
| ~ 'E'('0',f(X4071))
| 'LE'(f(X4071),'0') ),
inference(resolution,[status(thm)],[c9112,c14]) ).
cnf(c9139,plain,
( ~ iLEQ(suc(X4072),suc(X4072))
| ~ 'E'('0',f(X4072))
| 'LE'(f(X4072),'0') ),
inference(resolution,[status(thm)],[c9126,c11]) ).
cnf(c9143,plain,
( ~ 'E'('0',f(X4073))
| 'LE'(f(X4073),'0') ),
inference(resolution,[status(thm)],[c9139,c1255]) ).
cnf(c9167,plain,
'LE'(f(X4074),'0'),
inference(resolution,[status(thm)],[c9143,c0]) ).
cnf(c9169,plain,
$false,
inference(resolution,[status(thm)],[c9167,clause_1829]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYO651-1 : TPTP v8.1.2. Released v7.3.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n015.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 17:46:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 186.64/186.87 % Version: 1.5
% 186.64/186.87 % SZS status Unsatisfiable
% 186.64/186.87 % SZS output start CNFRefutation
% See solution above
% 186.64/186.87
% 186.64/186.87 % Initial clauses : 75
% 186.64/186.87 % Processed clauses : 974
% 186.64/186.87 % Factors computed : 826
% 186.64/186.87 % Resolvents computed: 8346
% 186.64/186.87 % Tautologies deleted: 4
% 186.64/186.87 % Forward subsumed : 2604
% 186.64/186.88 % Backward subsumed : 629
% 186.64/186.88 % -------- CPU Time ---------
% 186.64/186.88 % User time : 186.403 s
% 186.64/186.88 % System time : 0.100 s
% 186.64/186.88 % Total time : 186.503 s
%------------------------------------------------------------------------------