%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO661-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 14.05s 14.26s
% Output : Refutation 14.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 16
% Syntax : Number of clauses : 60 ( 10 unt; 28 nHn; 49 RR)
% Number of literals : 226 ( 0 equ; 145 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 : 53 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_93,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_93) ).
cnf(clause_0,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_0) ).
cnf(clause_72,axiom,
'LE'(f(X2),s(s('0'))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_72) ).
cnf(clause_118,axiom,
( ~ 'LE'(f(X5),s(s('0')))
| 'E'(s('0'),f(X5))
| 'LE'(f(X5),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_118) ).
cnf(c0,plain,
( 'E'(s('0'),f(X9))
| 'LE'(f(X9),s('0')) ),
inference(resolution,[status(thm)],[clause_118,clause_72]) ).
cnf(clause_119,axiom,
( ~ 'LE'(f(suc(X14)),s(s('0')))
| 'E'(s('0'),f(suc(X14)))
| 'LE'(f(X14),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_119) ).
cnf(c16,plain,
( 'E'(s('0'),f(suc(X15)))
| 'LE'(f(X15),s('0')) ),
inference(resolution,[status(thm)],[clause_119,clause_72]) ).
cnf(clause_85,axiom,
( ~ 'E'(s('0'),f(X29))
| ~ 'E'(s('0'),f(suc(X29)))
| 'E'(f(X29),f(suc(X29)))
| iLEQ(suc(X29),suc(X29)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_85) ).
cnf(c103,plain,
( ~ 'E'(s('0'),f(X32))
| 'E'(f(X32),f(suc(X32)))
| iLEQ(suc(X32),suc(X32))
| 'LE'(f(X32),s('0')) ),
inference(resolution,[status(thm)],[clause_85,c16]) ).
cnf(c128,plain,
( 'E'(f(X36),f(suc(X36)))
| iLEQ(suc(X36),suc(X36))
| 'LE'(f(X36),s('0')) ),
inference(resolution,[status(thm)],[c103,c0]) ).
cnf(clause_106,axiom,
( ~ 'E'(s('0'),f(suc(X18)))
| ~ 'E'(s('0'),f(X19))
| ~ 'E'(s('0'),f(X17))
| ~ 'E'(s('0'),f(suc(X19)))
| ~ 'E'(s('0'),f(suc(X17)))
| ~ 'E'(s('0'),f(X18))
| ~ iLEQ(suc(X17),suc(X18))
| ~ iLEQ(suc(X18),suc(X19))
| 'E'(f(X17),f(suc(X17)))
| 'E'(f(X18),f(suc(X18)))
| 'E'(f(X19),f(suc(X19))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_106) ).
cnf(c23,plain,
( ~ 'E'(s('0'),f(suc(X155)))
| ~ 'E'(s('0'),f(X154))
| ~ 'E'(s('0'),f(X155))
| ~ 'E'(s('0'),f(suc(X154)))
| ~ iLEQ(suc(X155),suc(X155))
| ~ iLEQ(suc(X155),suc(X154))
| 'E'(f(X155),f(suc(X155)))
| 'E'(f(X154),f(suc(X154))) ),
inference(factor,[status(thm)],[clause_106]) ).
cnf(c1120,plain,
( ~ 'E'(s('0'),f(suc(X156)))
| ~ 'E'(s('0'),f(X156))
| ~ iLEQ(suc(X156),suc(X156))
| 'E'(f(X156),f(suc(X156))) ),
inference(factor,[status(thm)],[c23]) ).
cnf(c1167,plain,
( ~ 'E'(s('0'),f(X174))
| ~ iLEQ(suc(X174),suc(X174))
| 'E'(f(X174),f(suc(X174)))
| 'LE'(f(X174),s('0')) ),
inference(resolution,[status(thm)],[c1120,c16]) ).
cnf(c1422,plain,
( ~ 'E'(s('0'),f(X175))
| 'E'(f(X175),f(suc(X175)))
| 'LE'(f(X175),s('0')) ),
inference(resolution,[status(thm)],[c1167,c128]) ).
cnf(c1427,plain,
( 'E'(f(X176),f(suc(X176)))
| 'LE'(f(X176),s('0')) ),
inference(resolution,[status(thm)],[c1422,c0]) ).
cnf(clause_33,axiom,
( ~ 'LE'(f(suc(suc(X26))),s(s('0')))
| 'E'(s('0'),f(suc(suc(X26))))
| 'LE'(f(X26),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_33) ).
cnf(c73,plain,
( 'E'(s('0'),f(suc(suc(X27))))
| 'LE'(f(X27),s('0')) ),
inference(resolution,[status(thm)],[clause_33,clause_72]) ).
cnf(clause_25,axiom,
( ~ 'E'(s('0'),f(suc(suc(X95))))
| ~ 'E'(s('0'),f(suc(X95)))
| ~ 'E'(f(X95),f(suc(X95)))
| ~ 'E'(s('0'),f(X95))
| iLEQ(suc(X95),suc(X95)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_25) ).
cnf(c633,plain,
( ~ 'E'(s('0'),f(suc(X310)))
| ~ 'E'(f(X310),f(suc(X310)))
| ~ 'E'(s('0'),f(X310))
| iLEQ(suc(X310),suc(X310))
| 'LE'(f(X310),s('0')) ),
inference(resolution,[status(thm)],[clause_25,c73]) ).
cnf(c2723,plain,
( ~ 'E'(s('0'),f(suc(X311)))
| ~ 'E'(s('0'),f(X311))
| iLEQ(suc(X311),suc(X311))
| 'LE'(f(X311),s('0')) ),
inference(resolution,[status(thm)],[c633,c1427]) ).
cnf(c2766,plain,
( ~ 'E'(s('0'),f(X315))
| iLEQ(suc(X315),suc(X315))
| 'LE'(f(X315),s('0')) ),
inference(resolution,[status(thm)],[c2723,c16]) ).
cnf(c2814,plain,
( iLEQ(suc(X316),suc(X316))
| 'LE'(f(X316),s('0')) ),
inference(resolution,[status(thm)],[c2766,c0]) ).
cnf(clause_8,axiom,
( ~ 'E'(s('0'),f(suc(X23)))
| ~ 'E'(s('0'),f(X24))
| ~ 'E'(s('0'),f(suc(suc(X22))))
| ~ 'E'(s('0'),f(X22))
| ~ 'E'(s('0'),f(suc(X24)))
| ~ 'E'(s('0'),f(suc(X22)))
| ~ 'E'(s('0'),f(suc(suc(X24))))
| ~ 'E'(f(X24),f(suc(X24)))
| ~ 'E'(f(X22),f(suc(X22)))
| ~ 'E'(s('0'),f(suc(suc(X23))))
| ~ 'E'(s('0'),f(X23))
| ~ 'E'(f(X23),f(suc(X23)))
| ~ iLEQ(suc(X22),suc(X23))
| ~ iLEQ(suc(X23),suc(X24)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8) ).
cnf(c47,plain,
( ~ 'E'(s('0'),f(suc(X263)))
| ~ 'E'(s('0'),f(X264))
| ~ 'E'(s('0'),f(suc(suc(X263))))
| ~ 'E'(s('0'),f(X263))
| ~ 'E'(s('0'),f(suc(X264)))
| ~ 'E'(s('0'),f(suc(suc(X264))))
| ~ 'E'(f(X264),f(suc(X264)))
| ~ 'E'(f(X263),f(suc(X263)))
| ~ iLEQ(suc(X263),suc(X263))
| ~ iLEQ(suc(X263),suc(X264)) ),
inference(factor,[status(thm)],[clause_8]) ).
cnf(c2073,plain,
( ~ 'E'(s('0'),f(suc(X595)))
| ~ 'E'(s('0'),f(X595))
| ~ 'E'(s('0'),f(suc(suc(X595))))
| ~ 'E'(f(X595),f(suc(X595)))
| ~ iLEQ(suc(X595),suc(X595)) ),
inference(factor,[status(thm)],[c47]) ).
cnf(c5348,plain,
( ~ 'E'(s('0'),f(suc(X596)))
| ~ 'E'(s('0'),f(X596))
| ~ 'E'(f(X596),f(suc(X596)))
| ~ iLEQ(suc(X596),suc(X596))
| 'LE'(f(X596),s('0')) ),
inference(resolution,[status(thm)],[c2073,c73]) ).
cnf(c5375,plain,
( ~ 'E'(s('0'),f(suc(X597)))
| ~ 'E'(s('0'),f(X597))
| ~ iLEQ(suc(X597),suc(X597))
| 'LE'(f(X597),s('0')) ),
inference(resolution,[status(thm)],[c5348,c1427]) ).
cnf(c5434,plain,
( ~ 'E'(s('0'),f(X598))
| ~ iLEQ(suc(X598),suc(X598))
| 'LE'(f(X598),s('0')) ),
inference(resolution,[status(thm)],[c5375,c16]) ).
cnf(c5443,plain,
( ~ 'E'(s('0'),f(X599))
| 'LE'(f(X599),s('0')) ),
inference(resolution,[status(thm)],[c5434,c2814]) ).
cnf(c5474,plain,
'LE'(f(X603),s('0')),
inference(resolution,[status(thm)],[c5443,c0]) ).
cnf(c5518,plain,
( 'E'('0',f(X604))
| 'LE'(f(X604),'0') ),
inference(resolution,[status(thm)],[c5474,clause_0]) ).
cnf(c5527,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c5518,clause_93]) ).
cnf(clause_57,axiom,
( ~ 'LE'(f(suc(X4)),s('0'))
| 'E'('0',f(suc(X4)))
| 'LE'(f(X4),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_57) ).
cnf(c5520,plain,
( 'E'('0',f(suc(X605)))
| 'LE'(f(X605),'0') ),
inference(resolution,[status(thm)],[c5474,clause_57]) ).
cnf(c5539,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c5520,clause_93]) ).
cnf(clause_51,axiom,
( ~ 'LE'(f(suc(suc(X12))),s('0'))
| 'E'('0',f(suc(suc(X12))))
| 'LE'(f(X12),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_51) ).
cnf(c5519,plain,
( 'E'('0',f(suc(suc(X609))))
| 'LE'(f(X609),'0') ),
inference(resolution,[status(thm)],[c5474,clause_51]) ).
cnf(c5552,plain,
'E'('0',f(suc(suc(z)))),
inference(resolution,[status(thm)],[c5519,clause_93]) ).
cnf(clause_148,axiom,
( ~ 'E'('0',f(suc(suc(X82))))
| ~ 'E'('0',f(suc(X82)))
| ~ 'E'(f(X82),f(suc(X82)))
| ~ 'E'('0',f(X82))
| iLEQ(suc(X82),suc(X82)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_148) ).
cnf(clause_109,axiom,
( ~ 'E'('0',f(X25))
| ~ 'E'('0',f(suc(X25)))
| 'E'(f(X25),f(suc(X25)))
| iLEQ(suc(X25),suc(X25)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_109) ).
cnf(c5544,plain,
( ~ 'E'('0',f(z))
| 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c5539,clause_109]) ).
cnf(c5560,plain,
( 'E'(f(z),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c5544,c5527]) ).
cnf(c5561,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)],[c5560,clause_148]) ).
cnf(c5687,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5561,c5552]) ).
cnf(c5690,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5687,c5539]) ).
cnf(c5693,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c5690,c5527]) ).
cnf(clause_20,axiom,
( ~ 'E'('0',f(suc(X75)))
| ~ 'E'('0',f(suc(X73)))
| ~ iLEQ(suc(X74),suc(X73))
| ~ 'E'('0',f(X75))
| ~ 'E'('0',f(X73))
| ~ 'E'('0',f(X74))
| ~ 'E'('0',f(suc(X74)))
| ~ iLEQ(suc(X75),suc(X74))
| 'E'(f(X75),f(suc(X75)))
| 'E'(f(X74),f(suc(X74)))
| 'E'(f(X73),f(suc(X73))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
cnf(c396,plain,
( ~ 'E'('0',f(suc(X76)))
| ~ iLEQ(suc(X76),suc(X76))
| ~ 'E'('0',f(X76))
| 'E'(f(X76),f(suc(X76))) ),
inference(factor,[status(thm)],[clause_20]) ).
cnf(c5572,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5560,c396]) ).
cnf(c5574,plain,
( 'E'(f(z),f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5572,c5539]) ).
cnf(c5577,plain,
'E'(f(z),f(suc(z))),
inference(resolution,[status(thm)],[c5574,c5527]) ).
cnf(clause_204,axiom,
( ~ 'E'('0',f(suc(suc(X65))))
| ~ 'E'('0',f(suc(X66)))
| ~ 'E'('0',f(suc(suc(X66))))
| ~ 'E'('0',f(suc(X64)))
| ~ iLEQ(suc(X65),suc(X64))
| ~ 'E'('0',f(X66))
| ~ 'E'('0',f(X64))
| ~ 'E'('0',f(suc(suc(X64))))
| ~ 'E'(f(X65),f(suc(X65)))
| ~ 'E'('0',f(X65))
| ~ 'E'('0',f(suc(X65)))
| ~ 'E'(f(X64),f(suc(X64)))
| ~ iLEQ(suc(X66),suc(X65))
| ~ 'E'(f(X66),f(suc(X66))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_204) ).
cnf(c351,plain,
( ~ 'E'('0',f(suc(suc(X1238))))
| ~ 'E'('0',f(suc(X1238)))
| ~ 'E'('0',f(suc(X1239)))
| ~ iLEQ(suc(X1238),suc(X1239))
| ~ 'E'('0',f(X1238))
| ~ 'E'('0',f(X1239))
| ~ 'E'('0',f(suc(suc(X1239))))
| ~ 'E'(f(X1238),f(suc(X1238)))
| ~ 'E'(f(X1239),f(suc(X1239)))
| ~ iLEQ(suc(X1238),suc(X1238)) ),
inference(factor,[status(thm)],[clause_204]) ).
cnf(c5884,plain,
( ~ 'E'('0',f(suc(suc(X1240))))
| ~ 'E'('0',f(suc(X1240)))
| ~ iLEQ(suc(X1240),suc(X1240))
| ~ 'E'('0',f(X1240))
| ~ 'E'(f(X1240),f(suc(X1240))) ),
inference(factor,[status(thm)],[c351]) ).
cnf(c5894,plain,
( ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5884,c5577]) ).
cnf(c5899,plain,
( ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5894,c5552]) ).
cnf(c5902,plain,
( ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c5899,c5693]) ).
cnf(c5904,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c5902,c5539]) ).
cnf(c5907,plain,
$false,
inference(resolution,[status(thm)],[c5904,c5527]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO661-1 : TPTP v8.1.2. Released v7.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n020.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 18:09:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 14.05/14.26 % Version: 1.5
% 14.05/14.26 % SZS status Unsatisfiable
% 14.05/14.26 % SZS output start CNFRefutation
% See solution above
% 14.05/14.26
% 14.05/14.26 % Initial clauses : 28
% 14.05/14.26 % Processed clauses : 349
% 14.05/14.26 % Factors computed : 208
% 14.05/14.26 % Resolvents computed: 5707
% 14.05/14.26 % Tautologies deleted: 37
% 14.05/14.26 % Forward subsumed : 1348
% 14.05/14.26 % Backward subsumed : 271
% 14.05/14.26 % -------- CPU Time ---------
% 14.05/14.26 % User time : 13.870 s
% 14.05/14.26 % System time : 0.048 s
% 14.05/14.26 % Total time : 13.918 s
%------------------------------------------------------------------------------