%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM283-1.005 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:35:28 EDT 2024
% Result : Unsatisfiable 110.93s 111.08s
% Output : Refutation 110.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 7
% Syntax : Number of clauses : 59 ( 44 unt; 0 nHn; 33 RR)
% Number of literals : 76 ( 0 equ; 18 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 121 ( 23 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 46 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_factorial,negated_conjecture,
~ factorial(s(s(s(s(s(n0))))),X13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_factorial) ).
cnf(factorial_0,axiom,
factorial(n0,s(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',factorial_0) ).
cnf(times1,axiom,
product(s(n0),X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',times1) ).
cnf(factorial,axiom,
( ~ factorial(X17,X18)
| ~ product(s(X17),X18,X16)
| factorial(s(X17),X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',factorial) ).
cnf(c8,plain,
( ~ factorial(n0,X20)
| factorial(s(n0),X20) ),
inference(resolution,[status(thm)],[factorial,times1]) ).
cnf(c12,plain,
factorial(s(n0),s(n0)),
inference(resolution,[status(thm)],[c8,factorial_0]) ).
cnf(add_0,axiom,
sum(X2,n0,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_0) ).
cnf(add,axiom,
( ~ sum(X5,X4,X6)
| sum(X5,s(X4),s(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add) ).
cnf(c0,plain,
sum(X7,s(n0),s(X7)),
inference(resolution,[status(thm)],[add,add_0]) ).
cnf(times,axiom,
( ~ sum(X8,X9,X11)
| ~ product(X10,X9,X8)
| product(s(X10),X9,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',times) ).
cnf(c2,plain,
( ~ sum(X14,X14,X15)
| product(s(s(n0)),X14,X15) ),
inference(resolution,[status(thm)],[times,times1]) ).
cnf(c5,plain,
product(s(s(n0)),s(n0),s(s(n0))),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(c13,plain,
( ~ factorial(s(n0),s(n0))
| factorial(s(s(n0)),s(s(n0))) ),
inference(resolution,[status(thm)],[c5,factorial]) ).
cnf(c27,plain,
factorial(s(s(n0)),s(s(n0))),
inference(resolution,[status(thm)],[c13,c12]) ).
cnf(c1,plain,
sum(X12,s(s(n0)),s(s(X12))),
inference(resolution,[status(thm)],[c0,add]) ).
cnf(c4,plain,
product(s(s(n0)),s(s(n0)),s(s(s(s(n0))))),
inference(resolution,[status(thm)],[c2,c1]) ).
cnf(c17,plain,
( ~ sum(s(s(s(s(n0)))),s(s(n0)),X31)
| product(s(s(s(n0))),s(s(n0)),X31) ),
inference(resolution,[status(thm)],[c4,times]) ).
cnf(c45,plain,
product(s(s(s(n0))),s(s(n0)),s(s(s(s(s(s(n0))))))),
inference(resolution,[status(thm)],[c17,c1]) ).
cnf(c48,plain,
( ~ factorial(s(s(n0)),s(s(n0)))
| factorial(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[c45,factorial]) ).
cnf(c70,plain,
factorial(s(s(s(n0))),s(s(s(s(s(s(n0))))))),
inference(resolution,[status(thm)],[c48,c27]) ).
cnf(c3,plain,
sum(X19,s(s(s(n0))),s(s(s(X19)))),
inference(resolution,[status(thm)],[c1,add]) ).
cnf(c10,plain,
sum(X22,s(s(s(s(n0)))),s(s(s(s(X22))))),
inference(resolution,[status(thm)],[c3,add]) ).
cnf(c20,plain,
sum(X25,s(s(s(s(s(n0))))),s(s(s(s(s(X25)))))),
inference(resolution,[status(thm)],[c10,add]) ).
cnf(c31,plain,
sum(X29,s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(X29))))))),
inference(resolution,[status(thm)],[c20,add]) ).
cnf(c43,plain,
product(s(s(n0)),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
inference(resolution,[status(thm)],[c31,c2]) ).
cnf(c85,plain,
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(n0)))))),X63)
| product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),X63) ),
inference(resolution,[status(thm)],[c43,times]) ).
cnf(c146,plain,
product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),
inference(resolution,[status(thm)],[c85,c31]) ).
cnf(c178,plain,
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(s(s(s(n0)))))),X103)
| product(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))),X103) ),
inference(resolution,[status(thm)],[c146,times]) ).
cnf(c270,plain,
product(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c178,c31]) ).
cnf(c271,plain,
( ~ factorial(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| factorial(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))) ),
inference(resolution,[status(thm)],[c270,factorial]) ).
cnf(c301,plain,
factorial(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c271,c70]) ).
cnf(c42,plain,
sum(X34,s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(X34)))))))),
inference(resolution,[status(thm)],[c31,add]) ).
cnf(c58,plain,
sum(X39,s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(X39))))))))),
inference(resolution,[status(thm)],[c42,add]) ).
cnf(c71,plain,
sum(X45,s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(s(s(X45)))))))))),
inference(resolution,[status(thm)],[c58,add]) ).
cnf(c92,plain,
sum(X49,s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(s(X49))))))))))),
inference(resolution,[status(thm)],[c71,add]) ).
cnf(c107,plain,
sum(X54,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),s(s(s(s(s(s(s(s(s(s(s(X54)))))))))))),
inference(resolution,[status(thm)],[c92,add]) ).
cnf(c121,plain,
sum(X61,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(X61))))))))))))),
inference(resolution,[status(thm)],[c107,add]) ).
cnf(c141,plain,
sum(X66,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(X66)))))))))))))),
inference(resolution,[status(thm)],[c121,add]) ).
cnf(c155,plain,
sum(X73,s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(X73))))))))))))))),
inference(resolution,[status(thm)],[c141,add]) ).
cnf(c179,plain,
sum(X79,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X79)))))))))))))))),
inference(resolution,[status(thm)],[c155,add]) ).
cnf(c196,plain,
sum(X84,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X84))))))))))))))))),
inference(resolution,[status(thm)],[c179,add]) ).
cnf(c214,plain,
sum(X92,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X92)))))))))))))))))),
inference(resolution,[status(thm)],[c196,add]) ).
cnf(c235,plain,
sum(X98,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X98))))))))))))))))))),
inference(resolution,[status(thm)],[c214,add]) ).
cnf(c258,plain,
sum(X105,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X105)))))))))))))))))))),
inference(resolution,[status(thm)],[c235,add]) ).
cnf(c276,plain,
sum(X113,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X113))))))))))))))))))))),
inference(resolution,[status(thm)],[c258,add]) ).
cnf(c302,plain,
sum(X118,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X118)))))))))))))))))))))),
inference(resolution,[status(thm)],[c276,add]) ).
cnf(c318,plain,
sum(X126,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X126))))))))))))))))))))))),
inference(resolution,[status(thm)],[c302,add]) ).
cnf(c344,plain,
sum(X134,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X134)))))))))))))))))))))))),
inference(resolution,[status(thm)],[c318,add]) ).
cnf(c367,plain,
sum(X143,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X143))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c344,add]) ).
cnf(c392,plain,
product(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c367,c2]) ).
cnf(c583,plain,
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X293)
| product(s(s(s(n0))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X293) ),
inference(resolution,[status(thm)],[c392,times]) ).
cnf(c848,plain,
product(s(s(s(n0))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c583,c367]) ).
cnf(c1039,plain,
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X481)
| product(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X481) ),
inference(resolution,[status(thm)],[c848,times]) ).
cnf(c1418,plain,
product(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c1039,c367]) ).
cnf(c1420,plain,
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X601)
| product(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X601) ),
inference(resolution,[status(thm)],[c1418,times]) ).
cnf(c1783,plain,
product(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c1420,c367]) ).
cnf(c1784,plain,
( ~ factorial(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))
| factorial(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ),
inference(resolution,[status(thm)],[c1783,factorial]) ).
cnf(c1841,plain,
factorial(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
inference(resolution,[status(thm)],[c1784,c301]) ).
cnf(c1842,plain,
$false,
inference(resolution,[status(thm)],[c1841,prove_factorial]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUM283-1.005 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n008.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 16:44:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 110.93/111.08 % Version: 1.5
% 110.93/111.08 % SZS status Unsatisfiable
% 110.93/111.08 % SZS output start CNFRefutation
% See solution above
% 110.93/111.08
% 110.93/111.08 % Initial clauses : 7
% 110.93/111.08 % Processed clauses : 1653
% 110.93/111.08 % Factors computed : 0
% 110.93/111.08 % Resolvents computed: 1843
% 110.93/111.08 % Tautologies deleted: 0
% 110.93/111.08 % Forward subsumed : 21
% 110.93/111.08 % Backward subsumed : 4
% 110.93/111.08 % -------- CPU Time ---------
% 110.93/111.08 % User time : 110.687 s
% 110.93/111.08 % System time : 0.049 s
% 110.93/111.08 % Total time : 110.736 s
%------------------------------------------------------------------------------