%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM448+5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:17:01 AM UTC 2026
% Result : Theorem 115.48s 16.12s
% Output : CNFRefutation 115.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 4
% Syntax : Number of formulae : 78 ( 9 unt; 0 def)
% Number of atoms : 495 ( 157 equ)
% Maximal formula atoms : 102 ( 6 avg)
% Number of connectives : 640 ( 223 ~; 273 |; 123 &)
% ( 7 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-2 aty)
% Number of variables : 119 ( 0 sgn 75 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mIntNeg,axiom,
! [W0] :
( aInteger0(W0)
=> aInteger0(smndt0(W0)) ),
file('theBenchmark.p',mIntNeg) ).
fof(mPrimeDivisor,axiom,
! [W0] :
( aInteger0(W0)
=> ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) )
<=> ( W0 != smndt0(sz10)
& W0 != sz10 ) ) ),
file('theBenchmark.p',mPrimeDivisor) ).
fof(m__,conjecture,
( ! [W0] :
( aInteger0(W0)
=> ( ( ? [W1] :
( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) )
=> ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) ) )
& ( ( aElementOf0(W0,sbsmnsldt0(xS))
| ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
=> ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( ( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS))) )
=> ( stldt0(sbsmnsldt0(xS)) = cS2076
| ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( W0 = smndt0(sz10)
| W0 = sz10 ) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ! [W0] :
( aInteger0(W0)
=> ( ( ? [W1] :
( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) )
=> ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) ) )
& ( ( aElementOf0(W0,sbsmnsldt0(xS))
| ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
=> ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( ( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS))) )
=> ( stldt0(sbsmnsldt0(xS)) = cS2076
| ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( W0 = smndt0(sz10)
| W0 = sz10 ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_23,plain,
! [W0] :
( ( ( smndt0(sz10) = W0
| sz10 = W0
| ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) ) )
& ( ( smndt0(sz10) != W0
& sz10 != W0 )
| ! [X0] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,W0) ) ) )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mPrimeDivisor]) ).
fof(sk_mPrimeDivisor_sk,plain,
! [W0] :
( ( ( smndt0(sz10) = W0
| sz10 = W0
| ( isPrime0(sK0(W0))
& aDivisorOf0(sK0(W0),W0) ) )
& ( ( smndt0(sz10) != W0
& sz10 != W0 )
| ! [X0] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,W0) ) ) )
| ~ aInteger0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W1,sK0(W0))],[nnf_23]) ).
fof(sk_mPrimeDivisor,plain,
( ! [VAR_0] :
( smndt0(sz10) = VAR_0
| sz10 = VAR_0
| isPrime0(sK0(VAR_0))
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( smndt0(sz10) = VAR_0
| sz10 = VAR_0
| aDivisorOf0(sK0(VAR_0),VAR_0)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( smndt0(sz10) != VAR_0
| ~ isPrime0(VAR_1)
| ~ aDivisorOf0(VAR_1,VAR_0)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sz10 != VAR_0
| ~ isPrime0(VAR_1)
| ~ aDivisorOf0(VAR_1,VAR_0)
| ~ aInteger0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mPrimeDivisor_sk]) ).
cnf(c_42,plain,
( smndt0(sz10) = A
| sz10 = A
| isPrime0(sK0(A))
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimeDivisor]) ).
cnf(c_43,plain,
( smndt0(sz10) != A
| ~ isPrime0(B)
| ~ aDivisorOf0(B,A)
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimeDivisor]) ).
cnf(c_44,plain,
( sz10 != A
| ~ isPrime0(B)
| ~ aDivisorOf0(B,A)
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimeDivisor]) ).
fof(nnf_41,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ? [W0] :
( ( ( smndt0(sz10) != W0
& sz10 != W0 )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( smndt0(sz10) = W0
| sz10 = W0
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& ! [X0] :
( ( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| aElementOf0(X0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(X0,sbsmnsldt0(xS))
& aInteger0(X0) )
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X7] :
( ( ! [W1] :
( ~ aElementOf0(X7,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(X7)
| aElementOf0(X7,sbsmnsldt0(xS)) )
& ( ( ? [X8] :
( aElementOf0(X7,X8)
& aElementOf0(X8,xS) )
& aInteger0(X7) )
| ~ aElementOf0(X7,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( ( ( ( aElementOf0(X1,sbsmnsldt0(xS))
& ? [X6] :
( aElementOf0(X1,X6)
& aElementOf0(X6,xS) ) )
| ! [X5] :
( ~ isPrime0(X5)
| ( ~ aDivisorOf0(X5,X1)
& ( ! [W2] :
( sdtasdt0(X5,W2) != X1
| ~ aInteger0(W2) )
| X5 = sz00
| ~ aInteger0(X5) ) ) ) )
& ( ? [X3] :
( isPrime0(X3)
& aDivisorOf0(X3,X1)
& ? [X4] :
( sdtasdt0(X3,X4) = X1
& aInteger0(X4) )
& X3 != sz00
& aInteger0(X3) )
| ( ~ aElementOf0(X1,sbsmnsldt0(xS))
& ! [X2] :
( ~ aElementOf0(X1,X2)
| ~ aElementOf0(X2,xS) ) ) ) )
| ~ aInteger0(X1) ) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ( ( smndt0(sz10) != sK2
& sz10 != sK2 )
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) )
& ( smndt0(sz10) = sK2
| sz10 = sK2
| aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) )
& ! [X0] :
( ( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| aElementOf0(X0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(X0,sbsmnsldt0(xS))
& aInteger0(X0) )
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X7] :
( ( ! [W1] :
( ~ aElementOf0(X7,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(X7)
| aElementOf0(X7,sbsmnsldt0(xS)) )
& ( ( aElementOf0(X7,sK5(X7))
& aElementOf0(sK5(X7),xS)
& aInteger0(X7) )
| ~ aElementOf0(X7,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( ( ( ( aElementOf0(X1,sbsmnsldt0(xS))
& aElementOf0(X1,sK4(X1))
& aElementOf0(sK4(X1),xS) )
| ! [X5] :
( ~ isPrime0(X5)
| ( ~ aDivisorOf0(X5,X1)
& ( ! [W2] :
( sdtasdt0(X5,W2) != X1
| ~ aInteger0(W2) )
| X5 = sz00
| ~ aInteger0(X5) ) ) ) )
& ( ( isPrime0(sK1(X1))
& aDivisorOf0(sK1(X1),X1)
& sdtasdt0(sK1(X1),sK3(X1)) = X1
& aInteger0(sK3(X1))
& sK1(X1) != sz00
& aInteger0(sK1(X1)) )
| ( ~ aElementOf0(X1,sbsmnsldt0(xS))
& ! [X2] :
( ~ aElementOf0(X1,X2)
| ~ aElementOf0(X2,xS) ) ) ) )
| ~ aInteger0(X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK3,sK4,sK5,sK2]),skolemize(X3,sK1(X1)),skolemize(X4,sK3(X1)),skolemize(X6,sK4(X1)),skolemize(X8,sK5(X7)),skolemize(W0,sK2)],[nnf_41]) ).
fof(sk_m___neg,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ( smndt0(sz10) != sK2
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) )
& ( sz10 != sK2
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) )
& ( smndt0(sz10) = sK2
| sz10 = sK2
| aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0)
| aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( aInteger0(VAR_0)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0)
| aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sK5(VAR_0))
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& ! [VAR_0] :
( aElementOf0(sK5(VAR_0),xS)
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& ! [VAR_0] :
( aInteger0(VAR_0)
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ isPrime0(VAR_1)
| ~ aDivisorOf0(VAR_1,VAR_0)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_0,sK4(VAR_0))
| ~ isPrime0(VAR_1)
| ~ aDivisorOf0(VAR_1,VAR_0)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElementOf0(sK4(VAR_0),xS)
| ~ isPrime0(VAR_1)
| ~ aDivisorOf0(VAR_1,VAR_0)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ isPrime0(VAR_1)
| sdtasdt0(VAR_1,VAR_2) != VAR_0
| ~ aInteger0(VAR_2)
| VAR_1 = sz00
| ~ aInteger0(VAR_1)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_0,sK4(VAR_0))
| ~ isPrime0(VAR_1)
| sdtasdt0(VAR_1,VAR_2) != VAR_0
| ~ aInteger0(VAR_2)
| VAR_1 = sz00
| ~ aInteger0(VAR_1)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(sK4(VAR_0),xS)
| ~ isPrime0(VAR_1)
| sdtasdt0(VAR_1,VAR_2) != VAR_0
| ~ aInteger0(VAR_2)
| VAR_1 = sz00
| ~ aInteger0(VAR_1)
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( isPrime0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( aDivisorOf0(sK1(VAR_0),VAR_0)
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( sdtasdt0(sK1(VAR_0),sK3(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( aInteger0(sK3(VAR_0))
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( sK1(VAR_0) != sz00
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( aInteger0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS))
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( isPrime0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aDivisorOf0(sK1(VAR_0),VAR_0)
| ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(sK1(VAR_0),sK3(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aInteger0(sK3(VAR_0))
| ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK1(VAR_0) != sz00
| ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aInteger0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,xS)
| ~ aInteger0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_57,negated_conjecture,
( isPrime0(sK1(A))
| ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_63,negated_conjecture,
( aElementOf0(A,sbsmnsldt0(xS))
| ~ isPrime0(B)
| ~ aDivisorOf0(B,A)
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
fof(mIntOne,axiom,
aInteger0(sz10),
file('theBenchmark.p',mIntOne) ).
cnf(c_65,plain,
aInteger0(sz10),
inference(clausify,[status(thm)],[mIntOne]) ).
cnf(c_66,plain,
( aInteger0(smndt0(A))
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mIntNeg]) ).
cnf(c_110,plain,
( smndt0(sz10) = A
| sz10 = A
| aDivisorOf0(sK0(A),A)
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimeDivisor]) ).
cnf(c_211,negated_conjecture,
( aDivisorOf0(sK1(A),A)
| ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_218,negated_conjecture,
( aInteger0(A)
| ~ aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_219,negated_conjecture,
( ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_220,negated_conjecture,
( aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A)
| aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_221,negated_conjecture,
( smndt0(sz10) = sK2
| sz10 = sK2
| aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_17376,negated_conjecture,
( smndt0(sz10) = sK2
| sK2 = sz10
| aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(copy,[status(thm)],[c_221]) ).
cnf(c_222,negated_conjecture,
( sK2 = smndt0(sz10)
| sK2 = sz10
| aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(copy,[status(thm)],[c_17376]) ).
cnf(c_223,negated_conjecture,
( sz10 != sK2
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_224,negated_conjecture,
( sK2 != sz10
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(copy,[status(thm)],[c_223]) ).
cnf(c_225,negated_conjecture,
( smndt0(sz10) != sK2
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_226,negated_conjecture,
( sK2 != smndt0(sz10)
| ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS))) ),
inference(copy,[status(thm)],[c_225]) ).
cnf(c_268,negated_conjecture,
( smndt0(sz10) != B
| ~ aDivisorOf0(sK1(A),B)
| ~ aInteger0(B)
| ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_57,c_43]) ).
cnf(c_269,negated_conjecture,
( sz10 != B
| ~ aDivisorOf0(sK1(A),B)
| ~ aInteger0(B)
| ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_57,c_44]) ).
cnf(c_293,negated_conjecture,
( smndt0(sz10) = B
| sz10 = B
| ~ aInteger0(B)
| aElementOf0(A,sbsmnsldt0(xS))
| ~ aDivisorOf0(sK0(B),A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_63,c_42]) ).
cnf(c_438,plain,
( smndt0(sz10) != A
| ~ aDivisorOf0(sK1(A),A)
| ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_268]) ).
cnf(c_439,plain,
( sz10 != A
| ~ aDivisorOf0(sK1(A),A)
| ~ aElementOf0(A,sbsmnsldt0(xS))
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_269]) ).
cnf(c_504,plain,
( smndt0(sz10) = A
| sz10 = A
| aElementOf0(A,sbsmnsldt0(xS))
| ~ aDivisorOf0(sK0(A),A)
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_293]) ).
cnf(c_612,plain,
aInteger0(smndt0(sz10)),
inference(resolve,[status(thm)],[c_66,c_65]) ).
cnf(c_1013,plain,
( aDivisorOf0(sK1(sz10),sz10)
| ~ aElementOf0(sz10,sbsmnsldt0(xS)) ),
inference(resolve,[status(thm)],[c_211,c_65]) ).
cnf(c_1173,plain,
( aElementOf0(sz10,sbsmnsldt0(xS))
| aElementOf0(sz10,stldt0(sbsmnsldt0(xS))) ),
inference(resolve,[status(thm)],[c_220,c_65]) ).
cnf(c_1175,plain,
( ~ aElementOf0(sK2,sbsmnsldt0(xS))
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_222,c_219]) ).
cnf(c_1176,plain,
( aInteger0(sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_222,c_218]) ).
cnf(c_17377,plain,
( ~ aDivisorOf0(sK1(smndt0(sz10)),smndt0(sz10))
| ~ aElementOf0(smndt0(sz10),sbsmnsldt0(xS))
| ~ aInteger0(smndt0(sz10)) ),
inference(xxres,[status(thm)],[c_438]) ).
cnf(c_1927,plain,
( ~ aDivisorOf0(sK1(smndt0(sz10)),smndt0(sz10))
| ~ aElementOf0(smndt0(sz10),sbsmnsldt0(xS)) ),
inference(resolve,[status(thm)],[c_612,c_17377]) ).
cnf(c_17378,plain,
( sz10 != sz10
| ~ aDivisorOf0(sK1(sz10),sz10)
| ~ aElementOf0(sz10,sbsmnsldt0(xS)) ),
inference(resolve,[status(thm)],[c_439,c_65]) ).
cnf(c_1928,plain,
( ~ aDivisorOf0(sK1(sz10),sz10)
| ~ aElementOf0(sz10,sbsmnsldt0(xS)) ),
inference(copy,[status(thm)],[c_17378]) ).
cnf(c_2419,plain,
( aElementOf0(smndt0(sz10),sbsmnsldt0(xS))
| aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(xS))) ),
inference(resolve,[status(thm)],[c_612,c_220]) ).
cnf(c_17379,plain,
( smndt0(sz10) = sK2
| sz10 = sK2
| aDivisorOf0(sK0(sK2),sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_1176,c_110]) ).
cnf(c_17380,plain,
( smndt0(sz10) = sK2
| sK2 = sz10
| aDivisorOf0(sK0(sK2),sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17379]) ).
cnf(c_17381,plain,
( sK2 = smndt0(sz10)
| sK2 = sz10
| aDivisorOf0(sK0(sK2),sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17380]) ).
cnf(c_17382,plain,
( sK2 = smndt0(sz10)
| aDivisorOf0(sK0(sK2),sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17381]) ).
cnf(c_5254,plain,
( aDivisorOf0(sK0(sK2),sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17382]) ).
cnf(c_17383,plain,
( smndt0(sz10) = sK2
| sz10 = sK2
| aElementOf0(sK2,sbsmnsldt0(xS))
| ~ aInteger0(sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_5254,c_504]) ).
cnf(c_17384,plain,
( smndt0(sz10) = sK2
| sK2 = sz10
| aElementOf0(sK2,sbsmnsldt0(xS))
| ~ aInteger0(sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17383]) ).
cnf(c_17385,plain,
( sK2 = smndt0(sz10)
| sK2 = sz10
| aElementOf0(sK2,sbsmnsldt0(xS))
| ~ aInteger0(sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17384]) ).
cnf(c_17386,plain,
( sK2 = smndt0(sz10)
| aElementOf0(sK2,sbsmnsldt0(xS))
| ~ aInteger0(sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17385]) ).
cnf(c_10736,plain,
( aElementOf0(sK2,sbsmnsldt0(xS))
| ~ aInteger0(sK2)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17386]) ).
cnf(c_17387,plain,
( sK2 = smndt0(sz10)
| sK2 = sz10
| aElementOf0(sK2,sbsmnsldt0(xS))
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_10736,c_1176]) ).
cnf(c_17388,plain,
( sK2 = smndt0(sz10)
| aElementOf0(sK2,sbsmnsldt0(xS))
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17387]) ).
cnf(c_13171,plain,
( aElementOf0(sK2,sbsmnsldt0(xS))
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17388]) ).
cnf(c_17389,plain,
( sK2 = smndt0(sz10)
| sK2 = sz10
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_13171,c_1175]) ).
cnf(c_17390,plain,
( sK2 = smndt0(sz10)
| sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17389]) ).
cnf(c_13180,plain,
( sK2 = smndt0(sz10)
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17390]) ).
cnf(c_13182,plain,
( ~ aElementOf0(sK2,stldt0(sbsmnsldt0(xS)))
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_13180,c_226]) ).
cnf(c_17391,plain,
( ~ aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(xS)))
| sK2 = sz10
| sK2 = sz10 ),
inference(paramod,[status(thm)],[c_13180,c_13182]) ).
cnf(c_13507,plain,
( ~ aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(xS)))
| sK2 = sz10 ),
inference(copy,[status(thm)],[c_17391]) ).
cnf(c_16632,plain,
( sK2 = sz10
| aElementOf0(smndt0(sz10),sbsmnsldt0(xS)) ),
inference(resolve,[status(thm)],[c_2419,c_13507]) ).
cnf(c_16692,plain,
( ~ aDivisorOf0(sK1(smndt0(sz10)),smndt0(sz10))
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_16632,c_1927]) ).
cnf(c_17392,negated_conjecture,
( aDivisorOf0(sK1(smndt0(sz10)),smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_16632,c_211]) ).
cnf(c_16714,negated_conjecture,
( aDivisorOf0(sK1(smndt0(sz10)),smndt0(sz10))
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_612,c_17392]) ).
cnf(c_17393,plain,
( sK2 = sz10
| sK2 = sz10 ),
inference(resolve,[status(thm)],[c_16714,c_16692]) ).
cnf(c_17281,plain,
sK2 = sz10,
inference(copy,[status(thm)],[c_17393]) ).
cnf(c_17394,negated_conjecture,
( sK2 != sz10
| ~ aElementOf0(sz10,stldt0(sbsmnsldt0(xS))) ),
inference(paramod,[status(thm)],[c_17281,c_224]) ).
cnf(c_17395,negated_conjecture,
( sz10 != sz10
| ~ aElementOf0(sz10,stldt0(sbsmnsldt0(xS))) ),
inference(paramod,[status(thm)],[c_17281,c_17394]) ).
cnf(c_17283,negated_conjecture,
~ aElementOf0(sz10,stldt0(sbsmnsldt0(xS))),
inference(copy,[status(thm)],[c_17395]) ).
cnf(c_17286,negated_conjecture,
aElementOf0(sz10,sbsmnsldt0(xS)),
inference(resolve,[status(thm)],[c_17283,c_1173]) ).
cnf(c_17350,plain,
~ aDivisorOf0(sK1(sz10),sz10),
inference(resolve,[status(thm)],[c_17286,c_1928]) ).
cnf(c_17396,plain,
aDivisorOf0(sK1(sz10),sz10),
inference(resolve,[status(thm)],[c_17286,c_1013]) ).
cnf(c_17375,plain,
$false,
inference(resolve,[status(thm)],[c_17350,c_17396]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM448+5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 02:47:15 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2314727 was started by sandbox on n010,
% 0.09/0.37 % Sat Sep 26 02:47:15 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 115.48/16.12
% 115.48/16.12 % given #500 (I,wt=40): 589 -aInteger0(A) | -aInteger0(f19(xS)) | f19(xS) = sz00 | sdtasdt0(f19(xS),f19(xS)) != A | aElementOf0(A,sbsmnsldt0(xS)) | -aInteger0(xS) | -aElementOf0(xS,xS). [factor(484,g,h)].
% 115.48/16.12
% 115.48/16.12 % given #1000 (T,wt=22): 9511 c1 = sz10 | c1 = smndt0(sz10) | -aDivisorOf0(sz00,sdtpldt0(c1,sz00)). [resolve(4890,c,695,a)].
% 115.48/16.12
% 115.48/16.12 % given #1500 (T,wt=24): 10768 sz10 = sz00 | smndt0(sz10) = sz00 | -aSubsetOf0(sbsmnsldt0(xS),xS) | aElementOf0(sz00,xS). [resolve(6700,c,955,b)].
% 115.48/16.12
% 115.48/16.12 % given #2000 (T,wt=25): 15183 sz10 = sz00 | -aDivisorOf0(sdtasdt0(f1(sz10,sz10),sz00),sz00). [resolve(3983,b,694,b(flip))].
% 115.48/16.12
% 115.48/16.12 % SZS status Theorem for theBenchmark
% 115.48/16.12
% 115.48/16.12 % Proof 1 at 5.93 (+ 1.35) seconds.
% 115.48/16.12 % Length of proof is 49.
% 115.48/16.12 % Level of proof is 16.
% 115.48/16.12 % Maximum clause weight is 29.000.
% 115.48/16.12 % Given clauses 2135.
% 115.48/16.12
% 115.48/16.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------