%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO680-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:08 EDT 2024
% Result : Unsatisfiable 1.05s 1.25s
% Output : Refutation 1.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 18
% Syntax : Number of clauses : 81 ( 11 unt; 41 nHn; 57 RR)
% Number of literals : 231 ( 0 equ; 115 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 5 ( 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 : 74 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_66,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_66) ).
cnf(clause_96,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_96) ).
cnf(clause_6,axiom,
( ~ 'LE'(f(X7),s(s('0')))
| 'E'(s('0'),f(X7))
| 'LE'(f(X7),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
cnf(clause_51,axiom,
( ~ 'LE'(f(X10),s(s(s('0'))))
| 'E'(s(s('0')),f(X10))
| 'LE'(f(X10),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_51) ).
cnf(clause_104,axiom,
'LE'(f(X2),s(s(s(s('0'))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_104) ).
cnf(clause_127,axiom,
( ~ 'LE'(f(X16),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(X16))
| 'LE'(f(X16),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_127) ).
cnf(c4,plain,
( 'E'(s(s(s('0'))),f(X17))
| 'LE'(f(X17),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_127,clause_104]) ).
cnf(clause_14,axiom,
( ~ 'E'(s(s(s('0'))),f(X11))
| ~ 'E'(s(s(s('0'))),f(suc(X11)))
| iLEQ(suc(X11),suc(X11)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14) ).
cnf(clause_102,axiom,
( ~ 'LE'(f(suc(X26)),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(X26)))
| 'LE'(f(X26),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_102) ).
cnf(c40,plain,
( 'E'(s(s(s('0'))),f(suc(X27)))
| 'LE'(f(X27),s(s(s('0')))) ),
inference(resolution,[status(thm)],[clause_102,clause_104]) ).
cnf(c41,plain,
( 'LE'(f(X31),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(X31))
| iLEQ(suc(X31),suc(X31)) ),
inference(resolution,[status(thm)],[c40,clause_14]) ).
cnf(c51,plain,
( 'LE'(f(X32),s(s(s('0'))))
| iLEQ(suc(X32),suc(X32)) ),
inference(resolution,[status(thm)],[c41,c4]) ).
cnf(c56,plain,
( iLEQ(suc(X33),suc(X33))
| 'E'(s(s('0')),f(X33))
| 'LE'(f(X33),s(s('0'))) ),
inference(resolution,[status(thm)],[c51,clause_51]) ).
cnf(c7,plain,
( 'E'(s(s(s('0'))),f(X18))
| 'E'(s(s('0')),f(X18))
| 'LE'(f(X18),s(s('0'))) ),
inference(resolution,[status(thm)],[c4,clause_51]) ).
cnf(c45,plain,
( 'E'(s(s(s('0'))),f(suc(X35)))
| 'E'(s(s('0')),f(X35))
| 'LE'(f(X35),s(s('0'))) ),
inference(resolution,[status(thm)],[c40,clause_51]) ).
cnf(clause_5,axiom,
( ~ 'E'(s(s('0')),f(X8))
| ~ 'E'(s(s('0')),f(suc(X8)))
| iLEQ(suc(X8),suc(X8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5) ).
cnf(clause_84,axiom,
( ~ 'LE'(f(suc(X15)),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(X15)))
| 'LE'(f(X15),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_84) ).
cnf(c6,plain,
( 'E'(s(s(s('0'))),f(suc(X24)))
| 'E'(s(s('0')),f(suc(X24)))
| 'LE'(f(X24),s(s('0'))) ),
inference(resolution,[status(thm)],[c4,clause_84]) ).
cnf(c28,plain,
( 'E'(s(s(s('0'))),f(suc(X79)))
| 'LE'(f(X79),s(s('0')))
| ~ 'E'(s(s('0')),f(X79))
| iLEQ(suc(X79),suc(X79)) ),
inference(resolution,[status(thm)],[c6,clause_5]) ).
cnf(c292,plain,
( 'E'(s(s(s('0'))),f(suc(X80)))
| 'LE'(f(X80),s(s('0')))
| iLEQ(suc(X80),suc(X80)) ),
inference(resolution,[status(thm)],[c28,c45]) ).
cnf(clause_20,axiom,
( ~ 'E'(s(s('0')),f(suc(X13)))
| ~ 'E'(s(s('0')),f(X13))
| ~ iLEQ(suc(X13),suc(X12))
| ~ 'E'(s(s('0')),f(suc(X14)))
| ~ 'E'(s(s('0')),f(suc(X12)))
| ~ iLEQ(suc(X14),suc(X13))
| ~ 'E'(s(s('0')),f(X12))
| ~ 'E'(s(s('0')),f(X14)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
cnf(c0,plain,
( ~ 'E'(s(s('0')),f(suc(X45)))
| ~ 'E'(s(s('0')),f(X45))
| ~ iLEQ(suc(X45),suc(X45))
| ~ 'E'(s(s('0')),f(suc(X44)))
| ~ iLEQ(suc(X44),suc(X45))
| ~ 'E'(s(s('0')),f(X44)) ),
inference(factor,[status(thm)],[clause_20]) ).
cnf(c102,plain,
( ~ 'E'(s(s('0')),f(suc(X47)))
| ~ 'E'(s(s('0')),f(X47))
| ~ iLEQ(suc(X47),suc(X47)) ),
inference(factor,[status(thm)],[c0]) ).
cnf(c115,plain,
( ~ 'E'(s(s('0')),f(X100))
| ~ iLEQ(suc(X100),suc(X100))
| 'E'(s(s(s('0'))),f(suc(X100)))
| 'LE'(f(X100),s(s('0'))) ),
inference(resolution,[status(thm)],[c102,c6]) ).
cnf(c412,plain,
( ~ iLEQ(suc(X101),suc(X101))
| 'E'(s(s(s('0'))),f(suc(X101)))
| 'LE'(f(X101),s(s('0'))) ),
inference(resolution,[status(thm)],[c115,c45]) ).
cnf(c432,plain,
( 'E'(s(s(s('0'))),f(suc(X102)))
| 'LE'(f(X102),s(s('0'))) ),
inference(resolution,[status(thm)],[c412,c292]) ).
cnf(clause_71,axiom,
( ~ iLEQ(suc(X22),suc(X21))
| ~ 'E'(s(s(s('0'))),f(X21))
| ~ 'E'(s(s(s('0'))),f(X22))
| ~ iLEQ(suc(X20),suc(X22))
| ~ 'E'(s(s(s('0'))),f(X20))
| ~ 'E'(s(s(s('0'))),f(suc(X22)))
| ~ 'E'(s(s(s('0'))),f(suc(X21)))
| ~ 'E'(s(s(s('0'))),f(suc(X20))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_71) ).
cnf(c17,plain,
( ~ iLEQ(suc(X111),suc(X110))
| ~ 'E'(s(s(s('0'))),f(X110))
| ~ 'E'(s(s(s('0'))),f(X111))
| ~ iLEQ(suc(X111),suc(X111))
| ~ 'E'(s(s(s('0'))),f(suc(X111)))
| ~ 'E'(s(s(s('0'))),f(suc(X110))) ),
inference(factor,[status(thm)],[clause_71]) ).
cnf(c498,plain,
( ~ iLEQ(suc(X112),suc(X112))
| ~ 'E'(s(s(s('0'))),f(X112))
| ~ 'E'(s(s(s('0'))),f(suc(X112))) ),
inference(factor,[status(thm)],[c17]) ).
cnf(c514,plain,
( ~ iLEQ(suc(X113),suc(X113))
| ~ 'E'(s(s(s('0'))),f(X113))
| 'LE'(f(X113),s(s('0'))) ),
inference(resolution,[status(thm)],[c498,c432]) ).
cnf(c528,plain,
( ~ iLEQ(suc(X114),suc(X114))
| 'LE'(f(X114),s(s('0')))
| 'E'(s(s('0')),f(X114)) ),
inference(resolution,[status(thm)],[c514,c7]) ).
cnf(c541,plain,
( 'LE'(f(X115),s(s('0')))
| 'E'(s(s('0')),f(X115)) ),
inference(resolution,[status(thm)],[c528,c56]) ).
cnf(c515,plain,
( ~ iLEQ(suc(X144),suc(X144))
| ~ 'E'(s(s(s('0'))),f(X144))
| 'LE'(f(X144),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c498,c40]) ).
cnf(c724,plain,
( ~ iLEQ(suc(X145),suc(X145))
| 'LE'(f(X145),s(s(s('0')))) ),
inference(resolution,[status(thm)],[c515,c4]) ).
cnf(c734,plain,
'LE'(f(X147),s(s(s('0')))),
inference(resolution,[status(thm)],[c724,c51]) ).
cnf(c736,plain,
( 'E'(s(s('0')),f(suc(X148)))
| 'LE'(f(X148),s(s('0'))) ),
inference(resolution,[status(thm)],[c734,clause_84]) ).
cnf(c739,plain,
( 'LE'(f(X150),s(s('0')))
| ~ 'E'(s(s('0')),f(X150))
| iLEQ(suc(X150),suc(X150)) ),
inference(resolution,[status(thm)],[c736,clause_5]) ).
cnf(c752,plain,
( 'LE'(f(X151),s(s('0')))
| iLEQ(suc(X151),suc(X151)) ),
inference(resolution,[status(thm)],[c739,c541]) ).
cnf(c741,plain,
( 'LE'(f(X154),s(s('0')))
| ~ 'E'(s(s('0')),f(X154))
| ~ iLEQ(suc(X154),suc(X154)) ),
inference(resolution,[status(thm)],[c736,c102]) ).
cnf(c764,plain,
( 'LE'(f(X155),s(s('0')))
| ~ iLEQ(suc(X155),suc(X155)) ),
inference(resolution,[status(thm)],[c741,c541]) ).
cnf(c769,plain,
'LE'(f(X156),s(s('0'))),
inference(resolution,[status(thm)],[c764,c752]) ).
cnf(c776,plain,
( 'E'(s('0'),f(X157))
| 'LE'(f(X157),s('0')) ),
inference(resolution,[status(thm)],[c769,clause_6]) ).
cnf(clause_91,axiom,
( ~ 'E'(s('0'),f(X6))
| ~ 'E'(s('0'),f(suc(X6)))
| iLEQ(suc(X6),suc(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_91) ).
cnf(clause_15,axiom,
( ~ 'LE'(f(suc(X9)),s(s('0')))
| 'E'(s('0'),f(suc(X9)))
| 'LE'(f(X9),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
cnf(c777,plain,
( 'E'(s('0'),f(suc(X161)))
| 'LE'(f(X161),s('0')) ),
inference(resolution,[status(thm)],[c769,clause_15]) ).
cnf(c782,plain,
( 'LE'(f(X168),s('0'))
| ~ 'E'(s('0'),f(X168))
| iLEQ(suc(X168),suc(X168)) ),
inference(resolution,[status(thm)],[c777,clause_91]) ).
cnf(c803,plain,
( 'LE'(f(X169),s('0'))
| iLEQ(suc(X169),suc(X169)) ),
inference(resolution,[status(thm)],[c782,c776]) ).
cnf(c805,plain,
( iLEQ(suc(X170),suc(X170))
| 'E'('0',f(X170))
| 'LE'(f(X170),'0') ),
inference(resolution,[status(thm)],[c803,clause_96]) ).
cnf(c808,plain,
( iLEQ(suc(z),suc(z))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c805,clause_66]) ).
cnf(c781,plain,
( 'E'(s('0'),f(X162))
| 'E'('0',f(X162))
| 'LE'(f(X162),'0') ),
inference(resolution,[status(thm)],[c776,clause_96]) ).
cnf(c790,plain,
( 'E'(s('0'),f(z))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c781,clause_66]) ).
cnf(c785,plain,
( 'E'(s('0'),f(suc(X164)))
| 'E'('0',f(X164))
| 'LE'(f(X164),'0') ),
inference(resolution,[status(thm)],[c777,clause_96]) ).
cnf(c795,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c785,clause_66]) ).
cnf(clause_114,axiom,
( ~ 'LE'(f(suc(X5)),s('0'))
| 'E'('0',f(suc(X5)))
| 'LE'(f(X5),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_114) ).
cnf(c780,plain,
( 'E'(s('0'),f(suc(X172)))
| 'E'('0',f(suc(X172)))
| 'LE'(f(X172),'0') ),
inference(resolution,[status(thm)],[c776,clause_114]) ).
cnf(c813,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[c780,clause_66]) ).
cnf(clause_109,axiom,
( ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(X4)))
| iLEQ(suc(X4),suc(X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_109) ).
cnf(c817,plain,
( 'E'(s('0'),f(suc(z)))
| ~ 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c813,clause_109]) ).
cnf(c849,plain,
( 'E'(s('0'),f(suc(z)))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c817,c808]) ).
cnf(clause_144,axiom,
( ~ 'E'('0',f(suc(X30)))
| ~ iLEQ(suc(X30),suc(X28))
| ~ iLEQ(suc(X29),suc(X30))
| ~ 'E'('0',f(suc(X28)))
| ~ 'E'('0',f(X30))
| ~ 'E'('0',f(suc(X29)))
| ~ 'E'('0',f(X28))
| ~ 'E'('0',f(X29)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_144) ).
cnf(c46,plain,
( ~ 'E'('0',f(suc(X214)))
| ~ iLEQ(suc(X214),suc(X213))
| ~ iLEQ(suc(X214),suc(X214))
| ~ 'E'('0',f(suc(X213)))
| ~ 'E'('0',f(X214))
| ~ 'E'('0',f(X213)) ),
inference(factor,[status(thm)],[clause_144]) ).
cnf(c916,plain,
( ~ 'E'('0',f(suc(X215)))
| ~ iLEQ(suc(X215),suc(X215))
| ~ 'E'('0',f(X215)) ),
inference(factor,[status(thm)],[c46]) ).
cnf(c935,plain,
( ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z))
| 'E'(s('0'),f(suc(z))) ),
inference(resolution,[status(thm)],[c916,c849]) ).
cnf(c954,plain,
( ~ 'E'('0',f(z))
| 'E'(s('0'),f(suc(z))) ),
inference(resolution,[status(thm)],[c935,c813]) ).
cnf(c974,plain,
'E'(s('0'),f(suc(z))),
inference(resolution,[status(thm)],[c954,c795]) ).
cnf(clause_21,axiom,
( ~ iLEQ(suc(X36),suc(X37))
| ~ 'E'(s('0'),f(suc(X38)))
| ~ iLEQ(suc(X38),suc(X36))
| ~ 'E'(s('0'),f(suc(X37)))
| ~ 'E'(s('0'),f(X38))
| ~ 'E'(s('0'),f(X37))
| ~ 'E'(s('0'),f(suc(X36)))
| ~ 'E'(s('0'),f(X36)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_21) ).
cnf(c72,plain,
( ~ iLEQ(suc(X258),suc(X257))
| ~ 'E'(s('0'),f(suc(X258)))
| ~ iLEQ(suc(X258),suc(X258))
| ~ 'E'(s('0'),f(suc(X257)))
| ~ 'E'(s('0'),f(X258))
| ~ 'E'(s('0'),f(X257)) ),
inference(factor,[status(thm)],[clause_21]) ).
cnf(c1089,plain,
( ~ iLEQ(suc(X259),suc(X259))
| ~ 'E'(s('0'),f(suc(X259)))
| ~ 'E'(s('0'),f(X259)) ),
inference(factor,[status(thm)],[c72]) ).
cnf(c1106,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z)) ),
inference(resolution,[status(thm)],[c1089,c974]) ).
cnf(c1111,plain,
( ~ iLEQ(suc(z),suc(z))
| 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c1106,c790]) ).
cnf(c1117,plain,
'E'('0',f(z)),
inference(resolution,[status(thm)],[c1111,c808]) ).
cnf(c1100,plain,
( ~ iLEQ(suc(X290),suc(X290))
| ~ 'E'(s('0'),f(X290))
| 'LE'(f(X290),s('0')) ),
inference(resolution,[status(thm)],[c1089,c777]) ).
cnf(c1220,plain,
( ~ iLEQ(suc(X291),suc(X291))
| 'LE'(f(X291),s('0')) ),
inference(resolution,[status(thm)],[c1100,c776]) ).
cnf(c1228,plain,
'LE'(f(X293),s('0')),
inference(resolution,[status(thm)],[c1220,c803]) ).
cnf(c1230,plain,
( 'E'('0',f(suc(X294)))
| 'LE'(f(X294),'0') ),
inference(resolution,[status(thm)],[c1228,clause_114]) ).
cnf(c1238,plain,
'E'('0',f(suc(z))),
inference(resolution,[status(thm)],[c1230,clause_66]) ).
cnf(c1241,plain,
( ~ 'E'('0',f(z))
| iLEQ(suc(z),suc(z)) ),
inference(resolution,[status(thm)],[c1238,clause_109]) ).
cnf(c1244,plain,
iLEQ(suc(z),suc(z)),
inference(resolution,[status(thm)],[c1241,c1117]) ).
cnf(c1246,plain,
( ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[c1244,c916]) ).
cnf(c1247,plain,
~ 'E'('0',f(z)),
inference(resolution,[status(thm)],[c1246,c1238]) ).
cnf(c1250,plain,
$false,
inference(resolution,[status(thm)],[c1247,c1117]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : SYO680-1 : TPTP v8.1.2. Released v7.3.0.
% 0.13/0.14 % 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:04:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.05/1.25 % Version: 1.5
% 1.05/1.25 % SZS status Unsatisfiable
% 1.05/1.25 % SZS output start CNFRefutation
% See solution above
% 1.05/1.25
% 1.05/1.25 % Initial clauses : 18
% 1.05/1.25 % Processed clauses : 200
% 1.05/1.25 % Factors computed : 53
% 1.05/1.25 % Resolvents computed: 1199
% 1.05/1.25 % Tautologies deleted: 4
% 1.05/1.25 % Forward subsumed : 162
% 1.05/1.25 % Backward subsumed : 152
% 1.05/1.25 % -------- CPU Time ---------
% 1.05/1.25 % User time : 0.851 s
% 1.05/1.25 % System time : 0.016 s
% 1.05/1.25 % Total time : 0.867 s
%------------------------------------------------------------------------------