%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO650-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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 6.37s 6.54s
% Output : Refutation 6.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 12
% Syntax : Number of clauses : 50 ( 4 unt; 34 nHn; 39 RR)
% Number of literals : 248 ( 0 equ; 160 neg)
% Maximal clause size : 20 ( 4 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 : 57 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_206,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_206) ).
cnf(clause_406,axiom,
'LE'(f(X2),s('0')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_406) ).
cnf(clause_278,axiom,
( ~ 'LE'(f(X3),s('0'))
| 'E'('0',f(X3))
| 'LE'(f(X3),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_278) ).
cnf(c0,plain,
( 'E'('0',f(X4))
| 'LE'(f(X4),'0') ),
inference(resolution,[status(thm)],[clause_278,clause_406]) ).
cnf(clause_313,axiom,
( ~ 'LE'(f(suc(X8)),s('0'))
| 'E'('0',f(suc(X8)))
| 'LE'(f(X8),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_313) ).
cnf(c2,plain,
( 'E'('0',f(suc(X9)))
| 'LE'(f(X9),'0') ),
inference(resolution,[status(thm)],[clause_313,clause_406]) ).
cnf(clause_359,axiom,
( ~ 'LE'(f(suc(suc(X10))),s('0'))
| 'E'('0',f(suc(suc(X10))))
| 'LE'(f(X10),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_359) ).
cnf(c4,plain,
( 'E'('0',f(suc(suc(X11))))
| 'LE'(f(X11),'0') ),
inference(resolution,[status(thm)],[clause_359,clause_406]) ).
cnf(clause_64,axiom,
( ~ 'E'('0',f(X15))
| ~ 'E'('0',f(suc(X15)))
| 'E'(f(X15),f(suc(X15)))
| iLEQ(suc(X15),suc(X15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_64) ).
cnf(c17,plain,
( ~ 'E'('0',f(X19))
| 'E'(f(X19),f(suc(X19)))
| iLEQ(suc(X19),suc(X19))
| 'LE'(f(X19),'0') ),
inference(resolution,[status(thm)],[clause_64,c2]) ).
cnf(c35,plain,
( 'E'(f(X20),f(suc(X20)))
| iLEQ(suc(X20),suc(X20))
| 'LE'(f(X20),'0') ),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(clause_376,axiom,
( ~ 'LE'(f(suc(suc(suc(X26)))),s('0'))
| 'E'('0',f(suc(suc(suc(X26)))))
| 'LE'(f(X26),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_376) ).
cnf(c45,plain,
( 'E'('0',f(suc(suc(suc(X27)))))
| 'LE'(f(X27),'0') ),
inference(resolution,[status(thm)],[clause_376,clause_406]) ).
cnf(clause_189,axiom,
( ~ 'E'('0',f(suc(suc(suc(X58)))))
| ~ 'E'('0',f(suc(X58)))
| ~ 'E'('0',f(suc(suc(X58))))
| ~ 'E'('0',f(X58))
| ~ 'E'(f(X58),f(suc(suc(X58))))
| ~ 'E'(f(X58),f(suc(X58)))
| iLEQ(suc(X58),suc(X58)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_189) ).
cnf(clause_345,axiom,
( ~ 'E'('0',f(suc(suc(X59))))
| ~ 'E'('0',f(suc(X59)))
| ~ 'E'(f(X59),f(suc(X59)))
| ~ 'E'('0',f(X59))
| 'E'(f(X59),f(suc(suc(X59))))
| iLEQ(suc(X59),suc(X59)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_345) ).
cnf(c113,plain,
( ~ 'E'('0',f(suc(suc(X60))))
| ~ 'E'('0',f(suc(X60)))
| ~ 'E'('0',f(X60))
| 'E'(f(X60),f(suc(suc(X60))))
| iLEQ(suc(X60),suc(X60))
| 'LE'(f(X60),'0') ),
inference(resolution,[status(thm)],[clause_345,c35]) ).
cnf(c117,plain,
( ~ 'E'('0',f(suc(X61)))
| ~ 'E'('0',f(X61))
| 'E'(f(X61),f(suc(suc(X61))))
| iLEQ(suc(X61),suc(X61))
| 'LE'(f(X61),'0') ),
inference(resolution,[status(thm)],[c113,c4]) ).
cnf(c128,plain,
( ~ 'E'('0',f(X62))
| 'E'(f(X62),f(suc(suc(X62))))
| iLEQ(suc(X62),suc(X62))
| 'LE'(f(X62),'0') ),
inference(resolution,[status(thm)],[c117,c2]) ).
cnf(c137,plain,
( 'E'(f(X66),f(suc(suc(X66))))
| iLEQ(suc(X66),suc(X66))
| 'LE'(f(X66),'0') ),
inference(resolution,[status(thm)],[c128,c0]) ).
cnf(c149,plain,
( iLEQ(suc(X94),suc(X94))
| 'LE'(f(X94),'0')
| ~ 'E'('0',f(suc(suc(suc(X94)))))
| ~ 'E'('0',f(suc(X94)))
| ~ 'E'('0',f(suc(suc(X94))))
| ~ 'E'('0',f(X94))
| ~ 'E'(f(X94),f(suc(X94))) ),
inference(resolution,[status(thm)],[c137,clause_189]) ).
cnf(c202,plain,
( iLEQ(suc(X95),suc(X95))
| 'LE'(f(X95),'0')
| ~ 'E'('0',f(suc(X95)))
| ~ 'E'('0',f(suc(suc(X95))))
| ~ 'E'('0',f(X95))
| ~ 'E'(f(X95),f(suc(X95))) ),
inference(resolution,[status(thm)],[c149,c45]) ).
cnf(c208,plain,
( iLEQ(suc(X96),suc(X96))
| 'LE'(f(X96),'0')
| ~ 'E'('0',f(suc(X96)))
| ~ 'E'('0',f(suc(suc(X96))))
| ~ 'E'('0',f(X96)) ),
inference(resolution,[status(thm)],[c202,c35]) ).
cnf(c213,plain,
( iLEQ(suc(X100),suc(X100))
| 'LE'(f(X100),'0')
| ~ 'E'('0',f(suc(X100)))
| ~ 'E'('0',f(X100)) ),
inference(resolution,[status(thm)],[c208,c4]) ).
cnf(c226,plain,
( iLEQ(suc(X101),suc(X101))
| 'LE'(f(X101),'0')
| ~ 'E'('0',f(X101)) ),
inference(resolution,[status(thm)],[c213,c2]) ).
cnf(c235,plain,
( iLEQ(suc(X102),suc(X102))
| 'LE'(f(X102),'0') ),
inference(resolution,[status(thm)],[c226,c0]) ).
cnf(clause_333,axiom,
( ~ iLEQ(suc(X90),suc(X89))
| ~ 'E'('0',f(suc(X91)))
| ~ 'E'('0',f(suc(X90)))
| ~ 'E'('0',f(X90))
| ~ iLEQ(suc(X89),suc(X91))
| ~ 'E'('0',f(X89))
| ~ 'E'('0',f(X91))
| ~ 'E'('0',f(suc(X89)))
| 'E'(f(X90),f(suc(X90)))
| 'E'(f(X89),f(suc(X89)))
| 'E'(f(X91),f(suc(X91))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_333) ).
cnf(c189,plain,
( ~ iLEQ(suc(X163),suc(X162))
| ~ 'E'('0',f(suc(X162)))
| ~ 'E'('0',f(suc(X163)))
| ~ 'E'('0',f(X163))
| ~ iLEQ(suc(X162),suc(X162))
| ~ 'E'('0',f(X162))
| 'E'(f(X163),f(suc(X163)))
| 'E'(f(X162),f(suc(X162))) ),
inference(factor,[status(thm)],[clause_333]) ).
cnf(c368,plain,
( ~ iLEQ(suc(X164),suc(X164))
| ~ 'E'('0',f(suc(X164)))
| ~ 'E'('0',f(X164))
| 'E'(f(X164),f(suc(X164))) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c384,plain,
( ~ iLEQ(suc(X167),suc(X167))
| ~ 'E'('0',f(X167))
| 'E'(f(X167),f(suc(X167)))
| 'LE'(f(X167),'0') ),
inference(resolution,[status(thm)],[c368,c2]) ).
cnf(c404,plain,
( ~ 'E'('0',f(X168))
| 'E'(f(X168),f(suc(X168)))
| 'LE'(f(X168),'0') ),
inference(resolution,[status(thm)],[c384,c235]) ).
cnf(c415,plain,
( 'E'(f(X171),f(suc(X171)))
| 'LE'(f(X171),'0') ),
inference(resolution,[status(thm)],[c404,c0]) ).
cnf(clause_309,axiom,
( ~ 'E'('0',f(suc(suc(X63))))
| ~ iLEQ(suc(X64),suc(X63))
| ~ 'E'('0',f(suc(X65)))
| ~ 'E'('0',f(suc(X64)))
| ~ 'E'(f(X65),f(suc(X65)))
| ~ 'E'('0',f(suc(suc(X64))))
| ~ 'E'('0',f(X64))
| ~ 'E'('0',f(suc(suc(X65))))
| ~ iLEQ(suc(X63),suc(X65))
| ~ 'E'(f(X64),f(suc(X64)))
| ~ 'E'('0',f(X63))
| ~ 'E'('0',f(X65))
| ~ 'E'(f(X63),f(suc(X63)))
| ~ 'E'('0',f(suc(X63)))
| 'E'(f(X64),f(suc(suc(X64))))
| 'E'(f(X63),f(suc(suc(X63))))
| 'E'(f(X65),f(suc(suc(X65)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_309) ).
cnf(c138,plain,
( ~ 'E'('0',f(suc(suc(X458))))
| ~ iLEQ(suc(X457),suc(X458))
| ~ 'E'('0',f(suc(X458)))
| ~ 'E'('0',f(suc(X457)))
| ~ 'E'(f(X458),f(suc(X458)))
| ~ 'E'('0',f(suc(suc(X457))))
| ~ 'E'('0',f(X457))
| ~ iLEQ(suc(X458),suc(X458))
| ~ 'E'(f(X457),f(suc(X457)))
| ~ 'E'('0',f(X458))
| 'E'(f(X457),f(suc(suc(X457))))
| 'E'(f(X458),f(suc(suc(X458)))) ),
inference(factor,[status(thm)],[clause_309]) ).
cnf(c1132,plain,
( ~ 'E'('0',f(suc(suc(X459))))
| ~ iLEQ(suc(X459),suc(X459))
| ~ 'E'('0',f(suc(X459)))
| ~ 'E'(f(X459),f(suc(X459)))
| ~ 'E'('0',f(X459))
| 'E'(f(X459),f(suc(suc(X459)))) ),
inference(factor,[status(thm)],[c138]) ).
cnf(c1145,plain,
( ~ 'E'('0',f(suc(suc(X464))))
| ~ iLEQ(suc(X464),suc(X464))
| ~ 'E'('0',f(suc(X464)))
| ~ 'E'('0',f(X464))
| 'E'(f(X464),f(suc(suc(X464))))
| 'LE'(f(X464),'0') ),
inference(resolution,[status(thm)],[c1132,c415]) ).
cnf(c1197,plain,
( ~ iLEQ(suc(X465),suc(X465))
| ~ 'E'('0',f(suc(X465)))
| ~ 'E'('0',f(X465))
| 'E'(f(X465),f(suc(suc(X465))))
| 'LE'(f(X465),'0') ),
inference(resolution,[status(thm)],[c1145,c4]) ).
cnf(c1204,plain,
( ~ iLEQ(suc(X466),suc(X466))
| ~ 'E'('0',f(X466))
| 'E'(f(X466),f(suc(suc(X466))))
| 'LE'(f(X466),'0') ),
inference(resolution,[status(thm)],[c1197,c2]) ).
cnf(c1207,plain,
( ~ 'E'('0',f(X470))
| 'E'(f(X470),f(suc(suc(X470))))
| 'LE'(f(X470),'0') ),
inference(resolution,[status(thm)],[c1204,c235]) ).
cnf(c1222,plain,
( 'E'(f(X471),f(suc(suc(X471))))
| 'LE'(f(X471),'0') ),
inference(resolution,[status(thm)],[c1207,c0]) ).
cnf(clause_135,axiom,
( ~ 'E'('0',f(suc(suc(suc(X104)))))
| ~ 'E'('0',f(suc(suc(X103))))
| ~ iLEQ(suc(X104),suc(X103))
| ~ 'E'('0',f(suc(X105)))
| ~ 'E'('0',f(suc(X104)))
| ~ 'E'(f(X105),f(suc(X105)))
| ~ 'E'('0',f(suc(suc(X104))))
| ~ 'E'('0',f(X104))
| ~ 'E'('0',f(suc(suc(X105))))
| ~ 'E'('0',f(suc(suc(suc(X103)))))
| ~ 'E'(f(X104),f(suc(suc(X104))))
| ~ iLEQ(suc(X103),suc(X105))
| ~ 'E'(f(X104),f(suc(X104)))
| ~ 'E'('0',f(X103))
| ~ 'E'(f(X105),f(suc(suc(X105))))
| ~ 'E'(f(X103),f(suc(suc(X103))))
| ~ 'E'('0',f(suc(suc(suc(X105)))))
| ~ 'E'('0',f(X105))
| ~ 'E'(f(X103),f(suc(X103)))
| ~ 'E'('0',f(suc(X103))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_135) ).
cnf(c237,plain,
( ~ 'E'('0',f(suc(suc(suc(X793)))))
| ~ 'E'('0',f(suc(suc(X794))))
| ~ iLEQ(suc(X793),suc(X794))
| ~ 'E'('0',f(suc(X793)))
| ~ 'E'(f(X793),f(suc(X793)))
| ~ 'E'('0',f(suc(suc(X793))))
| ~ 'E'('0',f(X793))
| ~ 'E'('0',f(suc(suc(suc(X794)))))
| ~ 'E'(f(X793),f(suc(suc(X793))))
| ~ iLEQ(suc(X794),suc(X793))
| ~ 'E'('0',f(X794))
| ~ 'E'(f(X794),f(suc(suc(X794))))
| ~ 'E'(f(X794),f(suc(X794)))
| ~ 'E'('0',f(suc(X794))) ),
inference(factor,[status(thm)],[clause_135]) ).
cnf(c1867,plain,
( ~ 'E'('0',f(suc(suc(suc(X795)))))
| ~ 'E'('0',f(suc(suc(X795))))
| ~ iLEQ(suc(X795),suc(X795))
| ~ 'E'('0',f(suc(X795)))
| ~ 'E'(f(X795),f(suc(X795)))
| ~ 'E'('0',f(X795))
| ~ 'E'(f(X795),f(suc(suc(X795)))) ),
inference(factor,[status(thm)],[c237]) ).
cnf(c1885,plain,
( ~ 'E'('0',f(suc(suc(suc(X796)))))
| ~ 'E'('0',f(suc(suc(X796))))
| ~ iLEQ(suc(X796),suc(X796))
| ~ 'E'('0',f(suc(X796)))
| ~ 'E'(f(X796),f(suc(X796)))
| ~ 'E'('0',f(X796))
| 'LE'(f(X796),'0') ),
inference(resolution,[status(thm)],[c1867,c1222]) ).
cnf(c1889,plain,
( ~ 'E'('0',f(suc(suc(X797))))
| ~ iLEQ(suc(X797),suc(X797))
| ~ 'E'('0',f(suc(X797)))
| ~ 'E'(f(X797),f(suc(X797)))
| ~ 'E'('0',f(X797))
| 'LE'(f(X797),'0') ),
inference(resolution,[status(thm)],[c1885,c45]) ).
cnf(c1897,plain,
( ~ 'E'('0',f(suc(suc(X798))))
| ~ iLEQ(suc(X798),suc(X798))
| ~ 'E'('0',f(suc(X798)))
| ~ 'E'('0',f(X798))
| 'LE'(f(X798),'0') ),
inference(resolution,[status(thm)],[c1889,c415]) ).
cnf(c1904,plain,
( ~ iLEQ(suc(X799),suc(X799))
| ~ 'E'('0',f(suc(X799)))
| ~ 'E'('0',f(X799))
| 'LE'(f(X799),'0') ),
inference(resolution,[status(thm)],[c1897,c4]) ).
cnf(c1911,plain,
( ~ iLEQ(suc(X802),suc(X802))
| ~ 'E'('0',f(X802))
| 'LE'(f(X802),'0') ),
inference(resolution,[status(thm)],[c1904,c2]) ).
cnf(c1928,plain,
( ~ 'E'('0',f(X803))
| 'LE'(f(X803),'0') ),
inference(resolution,[status(thm)],[c1911,c235]) ).
cnf(c1935,plain,
'LE'(f(X804),'0'),
inference(resolution,[status(thm)],[c1928,c0]) ).
cnf(c1942,plain,
$false,
inference(resolution,[status(thm)],[c1935,clause_206]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYO650-1 : TPTP v8.1.2. Released v7.3.0.
% 0.13/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n017.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 17:55:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 6.37/6.54 % Version: 1.5
% 6.37/6.54 % SZS status Unsatisfiable
% 6.37/6.54 % SZS output start CNFRefutation
% See solution above
% 6.37/6.54
% 6.37/6.54 % Initial clauses : 36
% 6.37/6.54 % Processed clauses : 277
% 6.37/6.54 % Factors computed : 149
% 6.37/6.54 % Resolvents computed: 1794
% 6.37/6.54 % Tautologies deleted: 0
% 6.37/6.54 % Forward subsumed : 584
% 6.37/6.54 % Backward subsumed : 188
% 6.37/6.54 % -------- CPU Time ---------
% 6.37/6.54 % User time : 6.168 s
% 6.37/6.54 % System time : 0.020 s
% 6.37/6.54 % Total time : 6.188 s
%------------------------------------------------------------------------------