%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:16:23 AM UTC 2026
% Result : Unsatisfiable 2.67s 0.72s
% Output : CNFRefutation 2.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 7
% Syntax : Number of formulae : 69 ( 45 unt; 0 def)
% Number of atoms : 106 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 84 ( 47 ~; 37 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 49 ( 9 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 : 92 ( 9 sgn 13 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(add_0,axiom,
! [VAR_0] : sum(VAR_0,n0,VAR_0),
file('theBenchmark.p',add_0) ).
cnf(c_1,plain,
sum(A,n0,A),
inference(clausify,[status(thm)],[add_0]) ).
fof(add,axiom,
! [VAR_0,VAR_1,VAR_2] :
( sum(VAR_0,s(VAR_1),s(VAR_2))
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',add) ).
cnf(c_2,plain,
( sum(A,s(B),s(C))
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[add]) ).
fof(times1,axiom,
! [VAR_0] : product(s(n0),VAR_0,VAR_0),
file('theBenchmark.p',times1) ).
cnf(c_3,plain,
product(s(n0),A,A),
inference(clausify,[status(thm)],[times1]) ).
fof(times,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( product(s(VAR_3),VAR_1,VAR_2)
| ~ product(VAR_3,VAR_1,VAR_0)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',times) ).
cnf(c_4,plain,
( product(s(D),B,C)
| ~ product(D,B,A)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[times]) ).
fof(factorial_0,axiom,
factorial(n0,s(n0)),
file('theBenchmark.p',factorial_0) ).
cnf(c_5,plain,
factorial(n0,s(n0)),
inference(clausify,[status(thm)],[factorial_0]) ).
fof(factorial,axiom,
! [VAR_0,VAR_1,VAR_2] :
( factorial(s(VAR_0),VAR_2)
| ~ product(s(VAR_0),VAR_1,VAR_2)
| ~ factorial(VAR_0,VAR_1) ),
file('theBenchmark.p',factorial) ).
cnf(c_6,plain,
( factorial(s(A),C)
| ~ product(s(A),B,C)
| ~ factorial(A,B) ),
inference(clausify,[status(thm)],[factorial]) ).
fof(prove_factorial,axiom,
! [VAR_0] : ~ factorial(s(s(s(s(s(n0))))),VAR_0),
file('theBenchmark.p',prove_factorial) ).
cnf(c_7,plain,
~ factorial(s(s(s(s(s(n0))))),A),
inference(clausify,[status(thm)],[prove_factorial]) ).
cnf(c_8,plain,
sum(A,s(n0),s(A)),
inference(resolve,[status(thm)],[c_2,c_1]) ).
cnf(c_1506,plain,
( factorial(s(n0),A)
| ~ product(s(n0),s(n0),A) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_10,plain,
factorial(s(n0),s(n0)),
inference(resolve,[status(thm)],[c_1506,c_3]) ).
cnf(c_11,plain,
( ~ product(s(s(s(s(s(n0))))),A,B)
| ~ factorial(s(s(s(s(n0)))),A) ),
inference(resolve,[status(thm)],[c_7,c_6]) ).
cnf(c_1507,plain,
( product(s(A),s(n0),s(B))
| ~ product(A,s(n0),B) ),
inference(resolve,[status(thm)],[c_4,c_8]) ).
cnf(c_12,plain,
product(s(s(n0)),s(n0),s(s(n0))),
inference(resolve,[status(thm)],[c_1507,c_3]) ).
cnf(c_13,plain,
sum(A,s(s(n0)),s(s(A))),
inference(resolve,[status(thm)],[c_2,c_8]) ).
cnf(c_15,plain,
( ~ product(s(s(s(s(n0)))),A,B)
| ~ sum(B,A,C)
| ~ factorial(s(s(s(s(n0)))),A) ),
inference(resolve,[status(thm)],[c_11,c_4]) ).
cnf(c_20,plain,
( ~ product(s(s(s(n0))),A,D)
| ~ sum(D,A,B)
| ~ sum(B,A,C)
| ~ factorial(s(s(s(s(n0)))),A) ),
inference(resolve,[status(thm)],[c_15,c_4]) ).
cnf(c_1508,plain,
( product(s(A),s(s(n0)),s(s(B)))
| ~ product(A,s(s(n0)),B) ),
inference(resolve,[status(thm)],[c_4,c_13]) ).
cnf(c_28,plain,
product(s(s(n0)),s(s(n0)),s(s(s(s(n0))))),
inference(resolve,[status(thm)],[c_1508,c_3]) ).
cnf(c_29,plain,
sum(A,s(s(s(n0))),s(s(s(A)))),
inference(resolve,[status(thm)],[c_2,c_13]) ).
cnf(c_1509,plain,
( factorial(s(s(n0)),A)
| ~ product(s(s(n0)),s(n0),A) ),
inference(resolve,[status(thm)],[c_6,c_10]) ).
cnf(c_30,plain,
factorial(s(s(n0)),s(s(n0))),
inference(resolve,[status(thm)],[c_1509,c_12]) ).
cnf(c_49,plain,
sum(A,s(s(s(s(n0)))),s(s(s(s(A))))),
inference(resolve,[status(thm)],[c_2,c_29]) ).
cnf(c_1510,plain,
( product(s(A),s(s(n0)),s(s(B)))
| ~ product(A,s(s(n0)),B) ),
inference(resolve,[status(thm)],[c_4,c_13]) ).
cnf(c_65,plain,
product(s(s(s(n0))),s(s(n0)),s(s(s(s(s(s(n0))))))),
inference(resolve,[status(thm)],[c_1510,c_28]) ).
cnf(c_79,plain,
sum(A,s(s(s(s(s(n0))))),s(s(s(s(s(A)))))),
inference(resolve,[status(thm)],[c_2,c_49]) ).
cnf(c_98,plain,
sum(A,s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(A))))))),
inference(resolve,[status(thm)],[c_2,c_79]) ).
cnf(c_1511,plain,
( factorial(s(s(s(n0))),A)
| ~ product(s(s(s(n0))),s(s(n0)),A) ),
inference(resolve,[status(thm)],[c_6,c_30]) ).
cnf(c_102,plain,
factorial(s(s(s(n0))),s(s(s(s(s(s(n0))))))),
inference(resolve,[status(thm)],[c_1511,c_65]) ).
cnf(c_114,plain,
( ~ product(s(s(n0)),A,E)
| ~ sum(E,A,D)
| ~ sum(D,A,B)
| ~ sum(B,A,C)
| ~ factorial(s(s(s(s(n0)))),A) ),
inference(resolve,[status(thm)],[c_20,c_4]) ).
cnf(c_1512,plain,
( product(s(A),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(B)))))))
| ~ product(A,s(s(s(s(s(s(n0)))))),B) ),
inference(resolve,[status(thm)],[c_4,c_98]) ).
cnf(c_130,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(resolve,[status(thm)],[c_1512,c_3]) ).
cnf(c_131,plain,
sum(A,s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(A)))))))),
inference(resolve,[status(thm)],[c_2,c_98]) ).
cnf(c_169,plain,
sum(A,s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(A))))))))),
inference(resolve,[status(thm)],[c_2,c_131]) ).
cnf(c_206,plain,
sum(A,s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(s(s(A)))))))))),
inference(resolve,[status(thm)],[c_2,c_169]) ).
cnf(c_251,plain,
sum(A,s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(s(A))))))))))),
inference(resolve,[status(thm)],[c_2,c_206]) ).
cnf(c_1513,plain,
( product(s(A),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(B)))))))
| ~ product(A,s(s(s(s(s(s(n0)))))),B) ),
inference(resolve,[status(thm)],[c_4,c_98]) ).
cnf(c_286,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(resolve,[status(thm)],[c_1513,c_130]) ).
cnf(c_325,plain,
sum(A,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),s(s(s(s(s(s(s(s(s(s(s(A)))))))))))),
inference(resolve,[status(thm)],[c_2,c_251]) ).
cnf(c_381,plain,
sum(A,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(A))))))))))))),
inference(resolve,[status(thm)],[c_2,c_325]) ).
cnf(c_485,plain,
sum(A,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(A)))))))))))))),
inference(resolve,[status(thm)],[c_2,c_381]) ).
cnf(c_525,plain,
sum(A,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(A))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_485]) ).
cnf(c_1514,plain,
( product(s(A),s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(B)))))))
| ~ product(A,s(s(s(s(s(s(n0)))))),B) ),
inference(resolve,[status(thm)],[c_4,c_98]) ).
cnf(c_540,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(resolve,[status(thm)],[c_1514,c_286]) ).
cnf(c_581,plain,
sum(A,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(A)))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_525]) ).
cnf(c_702,plain,
sum(A,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(A))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_581]) ).
cnf(c_761,plain,
sum(A,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(A)))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_702]) ).
cnf(c_1515,plain,
( factorial(s(s(s(s(n0)))),A)
| ~ product(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))),A) ),
inference(resolve,[status(thm)],[c_6,c_102]) ).
cnf(c_778,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(resolve,[status(thm)],[c_1515,c_540]) ).
cnf(c_841,plain,
sum(A,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(A))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_761]) ).
cnf(c_985,plain,
sum(A,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(A)))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_841]) ).
cnf(c_1033,plain,
sum(A,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(A))))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_985]) ).
cnf(c_1159,plain,
sum(A,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(A)))))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_1033]) ).
cnf(c_1284,plain,
sum(A,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(A))))))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_1159]) ).
cnf(c_1377,plain,
sum(A,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(A)))))))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_1284]) ).
cnf(c_1409,plain,
sum(A,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(A))))))))))))))))))))))))),
inference(resolve,[status(thm)],[c_2,c_1377]) ).
cnf(c_1516,plain,
( product(s(A),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(B)))))))))))))))))))))))))
| ~ product(A,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)))))))))))))))))))))))),B) ),
inference(resolve,[status(thm)],[c_4,c_1409]) ).
cnf(c_1502,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(resolve,[status(thm)],[c_1516,c_3]) ).
cnf(c_1517,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)))))))))))))))))))))))),D)
| ~ sum(D,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)))))))))))))))))))))))),C)
| ~ sum(C,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)))))))))))))))))))))))),A)
| ~ sum(A,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)))))))))))))))))))))))),B) ),
inference(resolve,[status(thm)],[c_114,c_778]) ).
cnf(c_1518,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)))))))))))))))))))))))),C)
| ~ sum(C,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)))))))))))))))))))))))),A)
| ~ sum(A,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)))))))))))))))))))))))),B) ),
inference(resolve,[status(thm)],[c_1517,c_1409]) ).
cnf(c_1519,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)))))))))))))))))))))))),A)
| ~ sum(A,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)))))))))))))))))))))))),B) ),
inference(resolve,[status(thm)],[c_1518,c_1409]) ).
cnf(c_1504,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)))))))))))))))))))))))),A),
inference(resolve,[status(thm)],[c_1519,c_1409]) ).
cnf(c_1505,plain,
$false,
inference(resolve,[status(thm)],[c_1504,c_1502]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 02:23:48 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.02/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.36 % Process 202163 was started by sandbox2 on n019,
% 0.02/0.36 % Sat Sep 26 02:23:48 2026
% 0.02/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.36
% 0.02/0.36 % From the command line: assign(max_seconds, 300).
% 2.67/0.72
% 2.67/0.72 % SZS status Unsatisfiable for theBenchmark
% 2.67/0.72
% 2.67/0.72 % Proof 1 at 0.29 (+ 0.05) seconds.
% 2.67/0.72 % Length of proof is 48.
% 2.67/0.72 % Level of proof is 26.
% 2.67/0.72 % Maximum clause weight is 78.000.
% 2.67/0.72 % Given clauses 355.
% 2.67/0.72
% 2.67/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------