%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM432+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:59 AM UTC 2026
% Result : Theorem 198.09s 36.76s
% Output : CNFRefutation 198.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 48 ( 21 unt; 0 def)
% Number of atoms : 129 ( 27 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 140 ( 59 ~; 62 |; 13 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn 8 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mIntNeg,axiom,
! [W0] :
( aInteger0(W0)
=> aInteger0(smndt0(W0)) ),
file('theBenchmark.p',mIntNeg) ).
fof(mIntPlus,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> aInteger0(sdtpldt0(W0,W1)) ),
file('theBenchmark.p',mIntPlus) ).
fof(mDivisor,axiom,
! [W0] :
( aInteger0(W0)
=> ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ),
file('theBenchmark.p',mDivisor) ).
fof(mEquMod,axiom,
! [W0,W1,W2] :
( ( W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ),
file('theBenchmark.p',mEquMod) ).
fof(m__818,axiom,
( aInteger0(xc)
& xq != sz00
& aInteger0(xq)
& aInteger0(xb)
& aInteger0(xa) ),
file('theBenchmark.p',m__818) ).
fof(m__876,axiom,
( sdtasdt0(xq,xn) = sdtpldt0(xa,smndt0(xb))
& aInteger0(xn) ),
file('theBenchmark.p',m__876) ).
fof(m__899,axiom,
( sdtasdt0(xq,xm) = sdtpldt0(xb,smndt0(xc))
& aInteger0(xm) ),
file('theBenchmark.p',m__899) ).
fof(m__,conjecture,
sdteqdtlpzmzozddtrp0(xa,xc,xq),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ sdteqdtlpzmzozddtrp0(xa,xc,xq),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_27,plain,
( aInteger0(smndt0(A))
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mIntNeg]) ).
cnf(c_28,plain,
( aInteger0(sdtpldt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mIntPlus]) ).
cnf(c_55,plain,
( sdtasdt0(B,C) != A
| ~ aInteger0(C)
| B = sz00
| ~ aInteger0(B)
| aDivisorOf0(B,A)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mDivisor]) ).
cnf(c_56,plain,
( sdtasdt0(B,C) != A
| ~ aInteger0(C)
| sz00 = B
| ~ aInteger0(B)
| aDivisorOf0(B,A)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_55]) ).
cnf(c_59,plain,
( ~ aDivisorOf0(C,sdtpldt0(A,smndt0(B)))
| sdteqdtlpzmzozddtrp0(A,B,C)
| C = sz00
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mEquMod]) ).
cnf(c_60,plain,
( ~ aDivisorOf0(C,sdtpldt0(A,smndt0(B)))
| sdteqdtlpzmzozddtrp0(A,B,C)
| sz00 = C
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_59]) ).
cnf(c_65,plain,
aInteger0(xa),
inference(clausify,[status(thm)],[m__818]) ).
cnf(c_67,plain,
aInteger0(xq),
inference(clausify,[status(thm)],[m__818]) ).
cnf(c_68,plain,
xq != sz00,
inference(clausify,[status(thm)],[m__818]) ).
cnf(c_69,plain,
aInteger0(xc),
inference(clausify,[status(thm)],[m__818]) ).
cnf(c_72,plain,
aInteger0(xn),
inference(clausify,[status(thm)],[m__876]) ).
cnf(c_75,plain,
aInteger0(xm),
inference(clausify,[status(thm)],[m__899]) ).
fof(m__924,axiom,
sdtasdt0(xq,sdtpldt0(xn,xm)) = sdtpldt0(xa,smndt0(xc)),
file('theBenchmark.p',m__924) ).
cnf(c_78,plain,
sdtasdt0(xq,sdtpldt0(xn,xm)) = sdtpldt0(xa,smndt0(xc)),
inference(clausify,[status(thm)],[m__924]) ).
cnf(c_79,plain,
sdtpldt0(xa,smndt0(xc)) = sdtasdt0(xq,sdtpldt0(xn,xm)),
inference(copy,[status(thm)],[c_78]) ).
cnf(c_80,negated_conjecture,
~ sdteqdtlpzmzozddtrp0(xa,xc,xq),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_938,plain,
aInteger0(smndt0(xc)),
inference(resolve,[status(thm)],[c_69,c_27]) ).
cnf(c_9026,plain,
( aInteger0(sdtpldt0(xn,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_28,c_72]) ).
cnf(c_2528,plain,
aInteger0(sdtpldt0(xn,xm)),
inference(resolve,[status(thm)],[c_9026,c_75]) ).
cnf(c_9027,plain,
( A != sdtasdt0(B,C)
| ~ aInteger0(C)
| sz00 = B
| ~ aInteger0(B)
| aDivisorOf0(B,A)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_56]) ).
cnf(c_9028,plain,
( ~ aInteger0(sdtpldt0(xn,xm))
| sz00 = xq
| ~ aInteger0(xq)
| aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc)))
| ~ aInteger0(sdtpldt0(xa,smndt0(xc))) ),
inference(resolve,[status(thm)],[c_79,c_9027]) ).
cnf(c_9029,plain,
( ~ aInteger0(sdtpldt0(xn,xm))
| sz00 = xq
| ~ aInteger0(xq)
| aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc)))
| ~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))) ),
inference(paramod,[status(thm)],[c_79,c_9028]) ).
cnf(c_9030,plain,
( ~ aInteger0(sdtpldt0(xn,xm))
| sz00 = xq
| ~ aInteger0(xq)
| aDivisorOf0(xq,sdtasdt0(xq,sdtpldt0(xn,xm)))
| ~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))) ),
inference(paramod,[status(thm)],[c_79,c_9029]) ).
cnf(c_9031,plain,
( ~ aInteger0(sdtpldt0(xn,xm))
| xq = sz00
| ~ aInteger0(xq)
| aDivisorOf0(xq,sdtasdt0(xq,sdtpldt0(xn,xm)))
| ~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))) ),
inference(copy,[status(thm)],[c_9030]) ).
cnf(c_9032,plain,
( ~ aInteger0(sdtpldt0(xn,xm))
| xq = sz00
| aDivisorOf0(xq,sdtasdt0(xq,sdtpldt0(xn,xm)))
| ~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))) ),
inference(resolve,[status(thm)],[c_67,c_9031]) ).
cnf(c_9033,plain,
( ~ aInteger0(sdtpldt0(xn,xm))
| aDivisorOf0(xq,sdtasdt0(xq,sdtpldt0(xn,xm)))
| ~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))) ),
inference(resolve,[status(thm)],[c_68,c_9032]) ).
cnf(c_2570,plain,
( aDivisorOf0(xq,sdtasdt0(xq,sdtpldt0(xn,xm)))
| ~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))) ),
inference(resolve,[status(thm)],[c_2528,c_9033]) ).
cnf(c_9034,plain,
( ~ aDivisorOf0(B,sdtpldt0(xa,smndt0(A)))
| sdteqdtlpzmzozddtrp0(xa,A,B)
| sz00 = B
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_60,c_65]) ).
cnf(c_9035,plain,
( ~ aDivisorOf0(A,sdtpldt0(xa,smndt0(xc)))
| sdteqdtlpzmzozddtrp0(xa,xc,A)
| sz00 = A
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_9034,c_69]) ).
cnf(c_9036,plain,
( ~ aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc)))
| sdteqdtlpzmzozddtrp0(xa,xc,xq)
| sz00 = xq ),
inference(resolve,[status(thm)],[c_9035,c_67]) ).
cnf(c_9037,plain,
sz00 != xq,
inference(copy,[status(thm)],[c_68]) ).
cnf(c_9038,plain,
( ~ aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc)))
| sdteqdtlpzmzozddtrp0(xa,xc,xq) ),
inference(resolve,[status(thm)],[c_9036,c_9037]) ).
cnf(c_9039,negated_conjecture,
~ aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))),
inference(resolve,[status(thm)],[c_9038,c_80]) ).
cnf(c_2573,negated_conjecture,
~ aDivisorOf0(xq,sdtasdt0(xq,sdtpldt0(xn,xm))),
inference(paramod,[status(thm)],[c_79,c_9039]) ).
cnf(c_2574,plain,
~ aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))),
inference(resolve,[status(thm)],[c_2573,c_2570]) ).
cnf(c_9040,plain,
( aInteger0(sdtpldt0(xa,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_28,c_65]) ).
cnf(c_9041,plain,
aInteger0(sdtpldt0(xa,smndt0(xc))),
inference(resolve,[status(thm)],[c_9040,c_938]) ).
cnf(c_9042,plain,
aInteger0(sdtasdt0(xq,sdtpldt0(xn,xm))),
inference(paramod,[status(thm)],[c_79,c_9041]) ).
cnf(c_9025,plain,
$false,
inference(resolve,[status(thm)],[c_2574,c_9042]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM432+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/10.62 % Computer : n002.cluster.edu
% 0.12/10.62 % Model : x86_64 x86_64
% 0.12/10.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.62 % Memory : 8046.5625MB
% 0.12/10.62 % OS : Linux 6.8.0-71-generic
% 0.12/10.62 % CPULimit : 300
% 0.12/10.62 % WCLimit : 300
% 0.12/10.62 % DateTime : Sat Sep 26 02:45:21 UTC 2026
% 0.12/10.62 % CPUTime :
% 0.12/10.62 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/10.62 % Process 668568 was started by sandbox2 on n002,
% 0.12/10.62 % Sat Sep 26 02:45:21 2026
% 0.12/10.62 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/10.64
% 0.12/10.64 % From the command line: assign(max_seconds, 300).
% 198.09/36.76
% 198.09/36.76 % SZS status Theorem for theBenchmark
% 198.09/36.76
% 198.09/36.76 % Proof 1 at 1.48 (+ 0.51) seconds.
% 198.09/36.76 % Length of proof is 29.
% 198.09/36.76 % Level of proof is 5.
% 198.09/36.76 % Maximum clause weight is 19.000.
% 198.09/36.76 % Given clauses 87.
% 198.09/36.76
% 198.09/36.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------