%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO646-1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:03 EDT 2024
% Result : Unsatisfiable 12.48s 12.67s
% Output : Refutation 12.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 7
% Syntax : Number of clauses : 45 ( 6 unt; 15 nHn; 39 RR)
% Number of literals : 338 ( 0 equ; 279 neg)
% Maximal clause size : 34 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-1 aty)
% Number of variables : 71 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1543,axiom,
'E'('0',f(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1543) ).
cnf(clause_1558,axiom,
( ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X3)))
| 'E'(f(X3),f(suc(X3)))
| iLEQ(suc(X3),suc(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1558) ).
cnf(c0,plain,
( ~ 'E'('0',f(X4))
| 'E'(f(X4),f(suc(X4)))
| iLEQ(suc(X4),suc(X4)) ),
inference(resolution,[status(thm)],[clause_1558,clause_1543]) ).
cnf(c1,plain,
( 'E'(f(X5),f(suc(X5)))
| iLEQ(suc(X5),suc(X5)) ),
inference(resolution,[status(thm)],[c0,clause_1543]) ).
cnf(clause_1548,axiom,
( ~ 'E'('0',f(suc(suc(X6))))
| ~ 'E'('0',f(suc(X6)))
| ~ 'E'(f(X6),f(suc(X6)))
| ~ 'E'('0',f(X6))
| 'E'(f(X6),f(suc(suc(X6))))
| iLEQ(suc(X6),suc(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1548) ).
cnf(c2,plain,
( ~ 'E'('0',f(suc(suc(X12))))
| ~ 'E'('0',f(suc(X12)))
| ~ 'E'('0',f(X12))
| 'E'(f(X12),f(suc(suc(X12))))
| iLEQ(suc(X12),suc(X12)) ),
inference(resolution,[status(thm)],[clause_1548,c1]) ).
cnf(c4,plain,
( ~ 'E'('0',f(suc(X13)))
| ~ 'E'('0',f(X13))
| 'E'(f(X13),f(suc(suc(X13))))
| iLEQ(suc(X13),suc(X13)) ),
inference(resolution,[status(thm)],[c2,clause_1543]) ).
cnf(c5,plain,
( ~ 'E'('0',f(X14))
| 'E'(f(X14),f(suc(suc(X14))))
| iLEQ(suc(X14),suc(X14)) ),
inference(resolution,[status(thm)],[c4,clause_1543]) ).
cnf(c6,plain,
( 'E'(f(X15),f(suc(suc(X15))))
| iLEQ(suc(X15),suc(X15)) ),
inference(resolution,[status(thm)],[c5,clause_1543]) ).
cnf(clause_806,axiom,
( ~ 'E'('0',f(suc(suc(X16))))
| ~ 'E'(f(X16),f(suc(suc(X16))))
| ~ 'E'('0',f(suc(suc(suc(X16)))))
| ~ 'E'(f(X16),f(suc(X16)))
| ~ 'E'('0',f(suc(X16)))
| ~ 'E'('0',f(X16))
| iLEQ(suc(X16),suc(X16)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_806) ).
cnf(c8,plain,
( ~ 'E'('0',f(suc(suc(X22))))
| ~ 'E'(f(X22),f(suc(suc(X22))))
| ~ 'E'(f(X22),f(suc(X22)))
| ~ 'E'('0',f(suc(X22)))
| ~ 'E'('0',f(X22))
| iLEQ(suc(X22),suc(X22)) ),
inference(resolution,[status(thm)],[clause_806,clause_1543]) ).
cnf(c10,plain,
( ~ 'E'('0',f(suc(suc(X23))))
| ~ 'E'(f(X23),f(suc(X23)))
| ~ 'E'('0',f(suc(X23)))
| ~ 'E'('0',f(X23))
| iLEQ(suc(X23),suc(X23)) ),
inference(resolution,[status(thm)],[c8,c6]) ).
cnf(c11,plain,
( ~ 'E'('0',f(suc(suc(X24))))
| ~ 'E'('0',f(suc(X24)))
| ~ 'E'('0',f(X24))
| iLEQ(suc(X24),suc(X24)) ),
inference(resolution,[status(thm)],[c10,c1]) ).
cnf(c12,plain,
( ~ 'E'('0',f(suc(X25)))
| ~ 'E'('0',f(X25))
| iLEQ(suc(X25),suc(X25)) ),
inference(resolution,[status(thm)],[c11,clause_1543]) ).
cnf(c13,plain,
( ~ 'E'('0',f(X26))
| iLEQ(suc(X26),suc(X26)) ),
inference(resolution,[status(thm)],[c12,clause_1543]) ).
cnf(c14,plain,
iLEQ(suc(X32),suc(X32)),
inference(resolution,[status(thm)],[c13,clause_1543]) ).
cnf(clause_891,axiom,
( ~ iLEQ(suc(X36),suc(X33))
| ~ iLEQ(suc(X34),suc(X36))
| ~ 'E'('0',f(X36))
| ~ iLEQ(suc(X35),suc(X37))
| ~ 'E'('0',f(suc(X34)))
| ~ 'E'('0',f(suc(X33)))
| ~ 'E'('0',f(X34))
| ~ 'E'('0',f(X33))
| ~ 'E'('0',f(suc(X35)))
| ~ 'E'('0',f(X37))
| ~ 'E'('0',f(suc(X37)))
| ~ 'E'('0',f(suc(X36)))
| ~ 'E'('0',f(X35))
| ~ iLEQ(suc(X37),suc(X34))
| 'E'(f(X36),f(suc(X36)))
| 'E'(f(X34),f(suc(X34)))
| 'E'(f(X37),f(suc(X37)))
| 'E'(f(X33),f(suc(X33)))
| 'E'(f(X35),f(suc(X35))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_891) ).
cnf(c17,plain,
( ~ iLEQ(suc(X40),suc(X38))
| ~ iLEQ(suc(X38),suc(X40))
| ~ 'E'('0',f(X40))
| ~ iLEQ(suc(X39),suc(X40))
| ~ 'E'('0',f(suc(X38)))
| ~ 'E'('0',f(X38))
| ~ 'E'('0',f(suc(X39)))
| ~ 'E'('0',f(suc(X40)))
| ~ 'E'('0',f(X39))
| 'E'(f(X40),f(suc(X40)))
| 'E'(f(X38),f(suc(X38)))
| 'E'(f(X39),f(suc(X39))) ),
inference(factor,[status(thm)],[clause_891]) ).
cnf(c21,plain,
( ~ iLEQ(suc(X42),suc(X42))
| ~ 'E'('0',f(X42))
| ~ iLEQ(suc(X41),suc(X42))
| ~ 'E'('0',f(suc(X42)))
| ~ 'E'('0',f(suc(X41)))
| ~ 'E'('0',f(X41))
| 'E'(f(X42),f(suc(X42)))
| 'E'(f(X41),f(suc(X41))) ),
inference(factor,[status(thm)],[c17]) ).
cnf(c27,plain,
( ~ iLEQ(suc(X43),suc(X43))
| ~ 'E'('0',f(X43))
| ~ 'E'('0',f(suc(X43)))
| 'E'(f(X43),f(suc(X43))) ),
inference(factor,[status(thm)],[c21]) ).
cnf(c29,plain,
( ~ iLEQ(suc(X49),suc(X49))
| ~ 'E'('0',f(X49))
| 'E'(f(X49),f(suc(X49))) ),
inference(resolution,[status(thm)],[c27,clause_1543]) ).
cnf(c42,plain,
( ~ 'E'('0',f(X50))
| 'E'(f(X50),f(suc(X50))) ),
inference(resolution,[status(thm)],[c29,c14]) ).
cnf(c43,plain,
'E'(f(X51),f(suc(X51))),
inference(resolution,[status(thm)],[c42,clause_1543]) ).
cnf(clause_0,axiom,
( ~ 'E'(f(X1449),f(suc(X1449)))
| ~ iLEQ(suc(X1449),suc(X1446))
| ~ 'E'('0',f(suc(suc(X1448))))
| ~ iLEQ(suc(X1447),suc(X1449))
| ~ 'E'('0',f(X1449))
| ~ 'E'('0',f(suc(suc(X1447))))
| ~ 'E'(f(X1447),f(suc(X1447)))
| ~ 'E'(f(X1450),f(suc(X1450)))
| ~ iLEQ(suc(X1448),suc(X1450))
| ~ 'E'('0',f(suc(X1447)))
| ~ 'E'('0',f(suc(X1446)))
| ~ 'E'(f(X1446),f(suc(X1446)))
| ~ 'E'(f(X1448),f(suc(X1448)))
| ~ 'E'('0',f(X1447))
| ~ 'E'('0',f(X1446))
| ~ 'E'('0',f(suc(X1448)))
| ~ 'E'('0',f(X1450))
| ~ 'E'('0',f(suc(suc(X1450))))
| ~ 'E'('0',f(suc(X1450)))
| ~ 'E'('0',f(suc(X1449)))
| ~ 'E'('0',f(suc(suc(X1446))))
| ~ 'E'('0',f(suc(suc(X1449))))
| ~ 'E'('0',f(X1448))
| ~ iLEQ(suc(X1450),suc(X1447))
| 'E'(f(X1446),f(suc(suc(X1446))))
| 'E'(f(X1448),f(suc(suc(X1448))))
| 'E'(f(X1450),f(suc(suc(X1450))))
| 'E'(f(X1447),f(suc(suc(X1447))))
| 'E'(f(X1449),f(suc(suc(X1449)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_0) ).
cnf(c318,plain,
( ~ 'E'(f(X1454),f(suc(X1454)))
| ~ iLEQ(suc(X1454),suc(X1451))
| ~ 'E'('0',f(suc(suc(X1454))))
| ~ iLEQ(suc(X1452),suc(X1454))
| ~ 'E'('0',f(X1454))
| ~ 'E'('0',f(suc(suc(X1452))))
| ~ 'E'(f(X1452),f(suc(X1452)))
| ~ 'E'(f(X1453),f(suc(X1453)))
| ~ iLEQ(suc(X1454),suc(X1453))
| ~ 'E'('0',f(suc(X1452)))
| ~ 'E'('0',f(suc(X1451)))
| ~ 'E'(f(X1451),f(suc(X1451)))
| ~ 'E'('0',f(X1452))
| ~ 'E'('0',f(X1451))
| ~ 'E'('0',f(suc(X1454)))
| ~ 'E'('0',f(X1453))
| ~ 'E'('0',f(suc(suc(X1453))))
| ~ 'E'('0',f(suc(X1453)))
| ~ 'E'('0',f(suc(suc(X1451))))
| ~ iLEQ(suc(X1453),suc(X1452))
| 'E'(f(X1451),f(suc(suc(X1451))))
| 'E'(f(X1454),f(suc(suc(X1454))))
| 'E'(f(X1453),f(suc(suc(X1453))))
| 'E'(f(X1452),f(suc(suc(X1452)))) ),
inference(factor,[status(thm)],[clause_0]) ).
cnf(c338,plain,
( ~ 'E'(f(X1457),f(suc(X1457)))
| ~ iLEQ(suc(X1457),suc(X1456))
| ~ 'E'('0',f(suc(suc(X1457))))
| ~ iLEQ(suc(X1455),suc(X1457))
| ~ 'E'('0',f(X1457))
| ~ 'E'('0',f(suc(suc(X1455))))
| ~ 'E'(f(X1455),f(suc(X1455)))
| ~ 'E'(f(X1456),f(suc(X1456)))
| ~ 'E'('0',f(suc(X1455)))
| ~ 'E'('0',f(suc(X1456)))
| ~ 'E'('0',f(X1455))
| ~ 'E'('0',f(X1456))
| ~ 'E'('0',f(suc(X1457)))
| ~ 'E'('0',f(suc(suc(X1456))))
| ~ iLEQ(suc(X1456),suc(X1455))
| 'E'(f(X1456),f(suc(suc(X1456))))
| 'E'(f(X1457),f(suc(suc(X1457))))
| 'E'(f(X1455),f(suc(suc(X1455)))) ),
inference(factor,[status(thm)],[c318]) ).
cnf(c341,plain,
( ~ 'E'(f(X1459),f(suc(X1459)))
| ~ iLEQ(suc(X1459),suc(X1459))
| ~ 'E'('0',f(suc(suc(X1459))))
| ~ iLEQ(suc(X1458),suc(X1459))
| ~ 'E'('0',f(X1459))
| ~ 'E'('0',f(suc(suc(X1458))))
| ~ 'E'(f(X1458),f(suc(X1458)))
| ~ 'E'('0',f(suc(X1458)))
| ~ 'E'('0',f(suc(X1459)))
| ~ 'E'('0',f(X1458))
| ~ iLEQ(suc(X1459),suc(X1458))
| 'E'(f(X1459),f(suc(suc(X1459))))
| 'E'(f(X1458),f(suc(suc(X1458)))) ),
inference(factor,[status(thm)],[c338]) ).
cnf(c348,plain,
( ~ 'E'(f(X1460),f(suc(X1460)))
| ~ iLEQ(suc(X1460),suc(X1460))
| ~ 'E'('0',f(suc(suc(X1460))))
| ~ 'E'('0',f(X1460))
| ~ 'E'('0',f(suc(X1460)))
| 'E'(f(X1460),f(suc(suc(X1460)))) ),
inference(factor,[status(thm)],[c341]) ).
cnf(c350,plain,
( ~ 'E'(f(X1461),f(suc(X1461)))
| ~ iLEQ(suc(X1461),suc(X1461))
| ~ 'E'('0',f(X1461))
| ~ 'E'('0',f(suc(X1461)))
| 'E'(f(X1461),f(suc(suc(X1461)))) ),
inference(resolution,[status(thm)],[c348,clause_1543]) ).
cnf(c351,plain,
( ~ iLEQ(suc(X1467),suc(X1467))
| ~ 'E'('0',f(X1467))
| ~ 'E'('0',f(suc(X1467)))
| 'E'(f(X1467),f(suc(suc(X1467)))) ),
inference(resolution,[status(thm)],[c350,c43]) ).
cnf(c353,plain,
( ~ iLEQ(suc(X1468),suc(X1468))
| ~ 'E'('0',f(X1468))
| 'E'(f(X1468),f(suc(suc(X1468)))) ),
inference(resolution,[status(thm)],[c351,clause_1543]) ).
cnf(c354,plain,
( ~ 'E'('0',f(X1469))
| 'E'(f(X1469),f(suc(suc(X1469)))) ),
inference(resolution,[status(thm)],[c353,c14]) ).
cnf(c355,plain,
'E'(f(X1470),f(suc(suc(X1470)))),
inference(resolution,[status(thm)],[c354,clause_1543]) ).
cnf(clause_1238,axiom,
( ~ 'E'('0',f(suc(suc(suc(X616)))))
| ~ 'E'(f(X616),f(suc(suc(X616))))
| ~ 'E'(f(X619),f(suc(X619)))
| ~ iLEQ(suc(X619),suc(X616))
| ~ 'E'('0',f(suc(suc(X618))))
| ~ iLEQ(suc(X617),suc(X619))
| ~ 'E'('0',f(X619))
| ~ 'E'('0',f(suc(suc(X617))))
| ~ 'E'('0',f(suc(suc(suc(X617)))))
| ~ 'E'(f(X617),f(suc(X617)))
| ~ 'E'('0',f(suc(suc(suc(X620)))))
| ~ 'E'(f(X620),f(suc(X620)))
| ~ iLEQ(suc(X618),suc(X620))
| ~ 'E'(f(X618),f(suc(suc(X618))))
| ~ 'E'('0',f(suc(X617)))
| ~ 'E'('0',f(suc(X616)))
| ~ 'E'('0',f(suc(suc(suc(X618)))))
| ~ 'E'(f(X616),f(suc(X616)))
| ~ 'E'(f(X618),f(suc(X618)))
| ~ 'E'('0',f(X617))
| ~ 'E'('0',f(X616))
| ~ 'E'('0',f(suc(X618)))
| ~ 'E'('0',f(X620))
| ~ 'E'('0',f(suc(suc(X620))))
| ~ 'E'(f(X620),f(suc(suc(X620))))
| ~ 'E'('0',f(suc(suc(suc(X619)))))
| ~ 'E'('0',f(suc(X620)))
| ~ 'E'('0',f(suc(X619)))
| ~ 'E'('0',f(suc(suc(X616))))
| ~ 'E'('0',f(suc(suc(X619))))
| ~ 'E'('0',f(X618))
| ~ 'E'(f(X617),f(suc(suc(X617))))
| ~ iLEQ(suc(X620),suc(X617))
| ~ 'E'(f(X619),f(suc(suc(X619)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1238) ).
cnf(c103,plain,
( ~ 'E'('0',f(suc(suc(suc(X1841)))))
| ~ 'E'(f(X1841),f(suc(suc(X1841))))
| ~ 'E'(f(X1841),f(suc(X1841)))
| ~ iLEQ(suc(X1841),suc(X1841))
| ~ 'E'('0',f(suc(suc(X1842))))
| ~ iLEQ(suc(X1839),suc(X1841))
| ~ 'E'('0',f(X1841))
| ~ 'E'('0',f(suc(suc(X1839))))
| ~ 'E'('0',f(suc(suc(suc(X1839)))))
| ~ 'E'(f(X1839),f(suc(X1839)))
| ~ 'E'('0',f(suc(suc(suc(X1840)))))
| ~ 'E'(f(X1840),f(suc(X1840)))
| ~ iLEQ(suc(X1842),suc(X1840))
| ~ 'E'(f(X1842),f(suc(suc(X1842))))
| ~ 'E'('0',f(suc(X1839)))
| ~ 'E'('0',f(suc(X1841)))
| ~ 'E'('0',f(suc(suc(suc(X1842)))))
| ~ 'E'(f(X1842),f(suc(X1842)))
| ~ 'E'('0',f(X1839))
| ~ 'E'('0',f(suc(X1842)))
| ~ 'E'('0',f(X1840))
| ~ 'E'('0',f(suc(suc(X1840))))
| ~ 'E'(f(X1840),f(suc(suc(X1840))))
| ~ 'E'('0',f(suc(X1840)))
| ~ 'E'('0',f(suc(suc(X1841))))
| ~ 'E'('0',f(X1842))
| ~ 'E'(f(X1839),f(suc(suc(X1839))))
| ~ iLEQ(suc(X1840),suc(X1839)) ),
inference(factor,[status(thm)],[clause_1238]) ).
cnf(c357,plain,
( ~ 'E'('0',f(suc(suc(suc(X1843)))))
| ~ 'E'(f(X1843),f(suc(suc(X1843))))
| ~ 'E'(f(X1843),f(suc(X1843)))
| ~ iLEQ(suc(X1843),suc(X1843))
| ~ 'E'('0',f(suc(suc(X1845))))
| ~ 'E'('0',f(X1843))
| ~ 'E'('0',f(suc(suc(X1843))))
| ~ 'E'('0',f(suc(suc(suc(X1844)))))
| ~ 'E'(f(X1844),f(suc(X1844)))
| ~ iLEQ(suc(X1845),suc(X1844))
| ~ 'E'(f(X1845),f(suc(suc(X1845))))
| ~ 'E'('0',f(suc(X1843)))
| ~ 'E'('0',f(suc(suc(suc(X1845)))))
| ~ 'E'(f(X1845),f(suc(X1845)))
| ~ 'E'('0',f(suc(X1845)))
| ~ 'E'('0',f(X1844))
| ~ 'E'('0',f(suc(suc(X1844))))
| ~ 'E'(f(X1844),f(suc(suc(X1844))))
| ~ 'E'('0',f(suc(X1844)))
| ~ 'E'('0',f(X1845))
| ~ iLEQ(suc(X1844),suc(X1843)) ),
inference(factor,[status(thm)],[c103]) ).
cnf(c361,plain,
( ~ 'E'('0',f(suc(suc(suc(X1846)))))
| ~ 'E'(f(X1846),f(suc(suc(X1846))))
| ~ 'E'(f(X1846),f(suc(X1846)))
| ~ iLEQ(suc(X1846),suc(X1846))
| ~ 'E'('0',f(suc(suc(X1847))))
| ~ 'E'('0',f(X1846))
| ~ 'E'('0',f(suc(suc(X1846))))
| ~ iLEQ(suc(X1847),suc(X1846))
| ~ 'E'(f(X1847),f(suc(suc(X1847))))
| ~ 'E'('0',f(suc(X1846)))
| ~ 'E'('0',f(suc(suc(suc(X1847)))))
| ~ 'E'(f(X1847),f(suc(X1847)))
| ~ 'E'('0',f(suc(X1847)))
| ~ 'E'('0',f(X1847)) ),
inference(factor,[status(thm)],[c357]) ).
cnf(c364,plain,
( ~ 'E'('0',f(suc(suc(suc(X1848)))))
| ~ 'E'(f(X1848),f(suc(suc(X1848))))
| ~ 'E'(f(X1848),f(suc(X1848)))
| ~ iLEQ(suc(X1848),suc(X1848))
| ~ 'E'('0',f(suc(suc(X1848))))
| ~ 'E'('0',f(X1848))
| ~ 'E'('0',f(suc(X1848))) ),
inference(factor,[status(thm)],[c361]) ).
cnf(c369,plain,
( ~ 'E'('0',f(suc(suc(suc(X1854)))))
| ~ 'E'(f(X1854),f(suc(X1854)))
| ~ iLEQ(suc(X1854),suc(X1854))
| ~ 'E'('0',f(suc(suc(X1854))))
| ~ 'E'('0',f(X1854))
| ~ 'E'('0',f(suc(X1854))) ),
inference(resolution,[status(thm)],[c364,c355]) ).
cnf(c370,plain,
( ~ 'E'(f(X1855),f(suc(X1855)))
| ~ iLEQ(suc(X1855),suc(X1855))
| ~ 'E'('0',f(suc(suc(X1855))))
| ~ 'E'('0',f(X1855))
| ~ 'E'('0',f(suc(X1855))) ),
inference(resolution,[status(thm)],[c369,clause_1543]) ).
cnf(c371,plain,
( ~ 'E'(f(X1856),f(suc(X1856)))
| ~ iLEQ(suc(X1856),suc(X1856))
| ~ 'E'('0',f(X1856))
| ~ 'E'('0',f(suc(X1856))) ),
inference(resolution,[status(thm)],[c370,clause_1543]) ).
cnf(c372,plain,
( ~ iLEQ(suc(X1857),suc(X1857))
| ~ 'E'('0',f(X1857))
| ~ 'E'('0',f(suc(X1857))) ),
inference(resolution,[status(thm)],[c371,c43]) ).
cnf(c373,plain,
( ~ iLEQ(suc(X1858),suc(X1858))
| ~ 'E'('0',f(X1858)) ),
inference(resolution,[status(thm)],[c372,clause_1543]) ).
cnf(c374,plain,
~ 'E'('0',f(X1864)),
inference(resolution,[status(thm)],[c373,c14]) ).
cnf(c375,plain,
$false,
inference(resolution,[status(thm)],[c374,clause_1543]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO646-1 : TPTP v8.1.2. Released v7.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 18:11:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 12.48/12.67 % Version: 1.5
% 12.48/12.67 % SZS status Unsatisfiable
% 12.48/12.67 % SZS output start CNFRefutation
% See solution above
% 12.48/12.67
% 12.48/12.67 % Initial clauses : 247
% 12.48/12.67 % Processed clauses : 175
% 12.48/12.67 % Factors computed : 267
% 12.48/12.67 % Resolvents computed: 109
% 12.48/12.67 % Tautologies deleted: 30
% 12.48/12.67 % Forward subsumed : 354
% 12.48/12.67 % Backward subsumed : 170
% 12.48/12.67 % -------- CPU Time ---------
% 12.48/12.67 % User time : 12.294 s
% 12.48/12.67 % System time : 0.023 s
% 12.48/12.67 % Total time : 12.317 s
%------------------------------------------------------------------------------