%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO666-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:06 EDT 2024
% Result : Unsatisfiable 218.55s 218.71s
% Output : Refutation 218.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of clauses : 48 ( 9 unt; 19 nHn; 38 RR)
% Number of literals : 188 ( 0 equ; 131 neg)
% Maximal clause size : 17 ( 3 avg)
% Maximal term depth : 3 ( 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 : 55 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_98,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_98) ).
cnf(clause_42,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_42) ).
cnf(clause_83,axiom,
'LE'(f(X2),s(s('0'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_83) ).
cnf(clause_185,axiom,
( ~ 'LE'(f(X13),s(s('0')))
| 'E'(s('0'),f(X13))
| 'LE'(f(X13),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_185) ).
cnf(c10,plain,
( 'E'(s('0'),f(X14))
| 'LE'(f(X14),s('0')) ),
inference(resolution,[status(thm)],[clause_185,clause_83]) ).
cnf(c13,plain,
( 'E'(s('0'),f(X15))
| 'E'('0',f(X15))
| 'LE'(f(X15),'0') ),
inference(resolution,[status(thm)],[c10,clause_42]) ).
cnf(c17,plain,
( 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c13,clause_98]) ).
cnf(clause_70,axiom,
( ~ 'E'(s('0'),f(X12))
| ~ 'E'(s('0'),f(suc(X12)))
| iLEQ(suc(X12),suc(X12)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_70) ).
cnf(clause_29,axiom,
( ~ 'LE'(f(suc(X16)),s(s('0')))
| 'E'(s('0'),f(suc(X16)))
| 'LE'(f(X16),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_29) ).
cnf(c18,plain,
( 'E'(s('0'),f(suc(X17)))
| 'LE'(f(X17),s('0')) ),
inference(resolution,[status(thm)],[clause_29,clause_83]) ).
cnf(c19,plain,
( 'LE'(f(X19),s('0'))
| ~ 'E'(s('0'),f(X19))
| iLEQ(suc(X19),suc(X19)) ),
inference(resolution,[status(thm)],[c18,clause_70]) ).
cnf(c28,plain,
( 'LE'(f(X20),s('0'))
| iLEQ(suc(X20),suc(X20)) ),
inference(resolution,[status(thm)],[c19,c10]) ).
cnf(c33,plain,
( iLEQ(suc(X27),suc(X27))
| 'E'('0',f(X27))
| 'LE'(f(X27),'0') ),
inference(resolution,[status(thm)],[c28,clause_42]) ).
cnf(c52,plain,
( iLEQ(suc(z),suc(z))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c33,clause_98]) ).
cnf(c20,plain,
( 'E'(s('0'),f(suc(X18)))
| 'E'('0',f(X18))
| 'LE'(f(X18),'0') ),
inference(resolution,[status(thm)],[c18,clause_42]) ).
cnf(c25,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c20,clause_98]) ).
cnf(clause_12,axiom,
( ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(X4)))
| iLEQ(suc(X4),suc(X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_12) ).
cnf(clause_123,axiom,
( ~ 'LE'(f(suc(X5)),s('0'))
| 'E'('0',f(suc(X5)))
| 'LE'(f(X5),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_123) ).
cnf(c12,plain,
( 'E'(s('0'),f(suc(X28)))
| 'E'('0',f(suc(X28)))
| 'LE'(f(X28),'0') ),
inference(resolution,[status(thm)],[c10,clause_123]) ).
cnf(c57,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c12,clause_98]) ).
cnf(c60,plain,
( 'E'(s('0'),f(suc(z)))
| ~ 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c57,clause_12]) ).
cnf(c108,plain,
( 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c60,c25]) ).
cnf(clause_102,axiom,
( ~ iLEQ(suc(X11),suc(X7))
| ~ 'E'('0',f(suc(X9)))
| ~ 'E'('0',f(suc(X11)))
| ~ iLEQ(suc(X7),suc(X8))
| ~ 'E'('0',f(suc(X7)))
| ~ 'E'('0',f(X9))
| ~ 'E'('0',f(suc(X10)))
| ~ 'E'('0',f(X7))
| ~ iLEQ(suc(X6),suc(X11))
| ~ 'E'('0',f(X11))
| ~ iLEQ(suc(X10),suc(X6))
| ~ 'E'('0',f(suc(X8)))
| ~ 'E'('0',f(X10))
| ~ iLEQ(suc(X9),suc(X10))
| ~ 'E'('0',f(suc(X6)))
| ~ 'E'('0',f(X8))
| ~ 'E'('0',f(X6)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_102) ).
cnf(c0,plain,
( ~ iLEQ(suc(X30),suc(X33))
| ~ 'E'('0',f(suc(X32)))
| ~ 'E'('0',f(suc(X30)))
| ~ iLEQ(suc(X33),suc(X31))
| ~ 'E'('0',f(suc(X33)))
| ~ 'E'('0',f(X32))
| ~ 'E'('0',f(suc(X34)))
| ~ 'E'('0',f(X33))
| ~ iLEQ(suc(X32),suc(X30))
| ~ 'E'('0',f(X30))
| ~ iLEQ(suc(X34),suc(X32))
| ~ 'E'('0',f(suc(X31)))
| ~ 'E'('0',f(X34))
| ~ iLEQ(suc(X32),suc(X34))
| ~ 'E'('0',f(X31)) ),
inference(factor,[status(thm)],[clause_102]) ).
cnf(c71,plain,
( ~ iLEQ(suc(X280),suc(X281))
| ~ 'E'('0',f(suc(X281)))
| ~ 'E'('0',f(suc(X280)))
| ~ iLEQ(suc(X281),suc(X282))
| ~ 'E'('0',f(X281))
| ~ 'E'('0',f(suc(X282)))
| ~ iLEQ(suc(X281),suc(X280))
| ~ 'E'('0',f(X280))
| ~ iLEQ(suc(X282),suc(X281))
| ~ 'E'('0',f(X282)) ),
inference(factor,[status(thm)],[c0]) ).
cnf(c1378,plain,
( ~ iLEQ(suc(X283),suc(X283))
| ~ 'E'('0',f(suc(X283)))
| ~ 'E'('0',f(X283)) ),
inference(factor,[status(thm)],[c71]) ).
cnf(c1427,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| 'E'(s('0'),f(suc(z))) ),
inference(resolution,[status(thm)],[c1378,c57]) ).
cnf(c1440,plain,
( ~ 'E'('0',f(z))
| 'E'(s('0'),f(suc(z))) ),
inference(resolution,[status(thm)],[c1427,c108]) ).
cnf(c1452,plain,
'E'(s('0'),f(suc(z))),
inference(resolution,[status(thm)],[c1440,c25]) ).
cnf(clause_179,axiom,
( ~ 'E'(s('0'),f(X26))
| ~ iLEQ(suc(X21),suc(X24))
| ~ 'E'(s('0'),f(X25))
| ~ 'E'(s('0'),f(suc(X25)))
| ~ iLEQ(suc(X23),suc(X21))
| ~ 'E'(s('0'),f(X21))
| ~ 'E'(s('0'),f(suc(X21)))
| ~ iLEQ(suc(X26),suc(X23))
| ~ 'E'(s('0'),f(suc(X26)))
| ~ iLEQ(suc(X24),suc(X22))
| ~ 'E'(s('0'),f(suc(X23)))
| ~ 'E'(s('0'),f(X22))
| ~ 'E'(s('0'),f(suc(X24)))
| ~ iLEQ(suc(X25),suc(X26))
| ~ 'E'(s('0'),f(X23))
| ~ 'E'(s('0'),f(X24))
| ~ 'E'(s('0'),f(suc(X22))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_179) ).
cnf(c39,plain,
( ~ 'E'(s('0'),f(X162))
| ~ iLEQ(suc(X158),suc(X161))
| ~ 'E'(s('0'),f(X160))
| ~ 'E'(s('0'),f(suc(X160)))
| ~ iLEQ(suc(X159),suc(X158))
| ~ 'E'(s('0'),f(X158))
| ~ 'E'(s('0'),f(suc(X158)))
| ~ iLEQ(suc(X162),suc(X159))
| ~ 'E'(s('0'),f(suc(X162)))
| ~ iLEQ(suc(X161),suc(X158))
| ~ 'E'(s('0'),f(suc(X159)))
| ~ 'E'(s('0'),f(suc(X161)))
| ~ iLEQ(suc(X160),suc(X162))
| ~ 'E'(s('0'),f(X159))
| ~ 'E'(s('0'),f(X161)) ),
inference(factor,[status(thm)],[clause_179]) ).
cnf(c577,plain,
( ~ 'E'(s('0'),f(X2534))
| ~ iLEQ(suc(X2533),suc(X2533))
| ~ 'E'(s('0'),f(X2535))
| ~ 'E'(s('0'),f(suc(X2535)))
| ~ iLEQ(suc(X2536),suc(X2533))
| ~ 'E'(s('0'),f(X2533))
| ~ 'E'(s('0'),f(suc(X2533)))
| ~ iLEQ(suc(X2534),suc(X2536))
| ~ 'E'(s('0'),f(suc(X2534)))
| ~ 'E'(s('0'),f(suc(X2536)))
| ~ iLEQ(suc(X2535),suc(X2534))
| ~ 'E'(s('0'),f(X2536)) ),
inference(factor,[status(thm)],[c39]) ).
cnf(c8495,plain,
( ~ 'E'(s('0'),f(X2657))
| ~ iLEQ(suc(X2656),suc(X2656))
| ~ 'E'(s('0'),f(X2658))
| ~ 'E'(s('0'),f(suc(X2658)))
| ~ 'E'(s('0'),f(X2656))
| ~ 'E'(s('0'),f(suc(X2656)))
| ~ iLEQ(suc(X2657),suc(X2656))
| ~ 'E'(s('0'),f(suc(X2657)))
| ~ iLEQ(suc(X2658),suc(X2657)) ),
inference(factor,[status(thm)],[c577]) ).
cnf(c9109,plain,
( ~ 'E'(s('0'),f(X2659))
| ~ iLEQ(suc(X2659),suc(X2659))
| ~ 'E'(s('0'),f(X2660))
| ~ 'E'(s('0'),f(suc(X2660)))
| ~ 'E'(s('0'),f(suc(X2659)))
| ~ iLEQ(suc(X2660),suc(X2659)) ),
inference(factor,[status(thm)],[c8495]) ).
cnf(c9137,plain,
( ~ 'E'(s('0'),f(X2661))
| ~ iLEQ(suc(X2661),suc(X2661))
| ~ 'E'(s('0'),f(suc(X2661))) ),
inference(factor,[status(thm)],[c9109]) ).
cnf(c9174,plain,
( ~ 'E'(s('0'),f(z))
| ~ iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c9137,c1452]) ).
cnf(c9230,plain,
( ~ 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c9174,c52]) ).
cnf(c9248,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c9230,c17]) ).
cnf(c9189,plain,
( ~ 'E'(s('0'),f(X2719))
| ~ iLEQ(suc(X2719),suc(X2719))
| 'LE'(f(X2719),s('0')) ),
inference(resolution,[status(thm)],[c9137,c18]) ).
cnf(c9801,plain,
( ~ 'E'(s('0'),f(X2723))
| 'LE'(f(X2723),s('0')) ),
inference(resolution,[status(thm)],[c9189,c28]) ).
cnf(c9802,plain,
'LE'(f(X2724),s('0')),
inference(resolution,[status(thm)],[c9801,c10]) ).
cnf(c9810,plain,
( 'E'('0',f(suc(X2725)))
| 'LE'(f(X2725),'0') ),
inference(resolution,[status(thm)],[c9802,clause_123]) ).
cnf(c9820,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c9810,clause_98]) ).
cnf(c9821,plain,
( ~ 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c9820,clause_12]) ).
cnf(c9827,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c9821,c9248]) ).
cnf(c9826,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c9820,c1378]) ).
cnf(c9838,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c9826,c9827]) ).
cnf(c9839,plain,
$false,
inference(resolution,[status(thm)],[c9838,c9248]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SYO666-1 : TPTP v8.1.2. Released v7.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n003.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:10:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 218.55/218.71 % Version: 1.5
% 218.55/218.71 % SZS status Unsatisfiable
% 218.55/218.71 % SZS output start CNFRefutation
% See solution above
% 218.55/218.71
% 218.55/218.71 % Initial clauses : 10
% 218.55/218.71 % Processed clauses : 420
% 218.55/218.71 % Factors computed : 825
% 218.55/218.71 % Resolvents computed: 9016
% 218.55/218.71 % Tautologies deleted: 200
% 218.55/218.71 % Forward subsumed : 1735
% 218.55/218.71 % Backward subsumed : 317
% 218.55/218.71 % -------- CPU Time ---------
% 218.55/218.71 % User time : 218.278 s
% 218.55/218.71 % System time : 0.079 s
% 218.55/218.71 % Total time : 218.357 s
%------------------------------------------------------------------------------