%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM449+6 : 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 : n008.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:02 AM UTC 2026
% Result : Theorem 20.37s 8.63s
% Output : CNFRefutation 20.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 47 ( 14 unt; 0 def)
% Number of atoms : 383 ( 68 equ)
% Maximal formula atoms : 102 ( 8 avg)
% Number of connectives : 482 ( 146 ~; 173 |; 135 &)
% ( 4 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 117 ( 0 sgn 84 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mUnionSClosed,axiom,
! [W0] :
( ( ! [W1] :
( aElementOf0(W1,W0)
=> ( isClosed0(W1)
& aSubsetOf0(W1,cS1395) ) )
& isFinite0(W0)
& aSet0(W0) )
=> isClosed0(sbsmnsldt0(W0)) ),
file('theBenchmark.p',mUnionSClosed) ).
fof(mArSeqClosed,axiom,
! [W0,W1] :
( ( W1 != sz00
& aInteger0(W1)
& aInteger0(W0) )
=> ( isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) ) ),
file('theBenchmark.p',mArSeqClosed) ).
fof(m__2046,axiom,
( xS = cS2043
& ! [W0] :
( ( ? [W1] :
( ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
=> szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 )
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) )
=> aElementOf0(W0,xS) )
& ( aElementOf0(W0,xS)
=> ? [W1] :
( szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0
& ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) ) ) )
& aSet0(xS) ),
file('theBenchmark.p',m__2046) ).
fof(m__,conjecture,
( ( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( isClosed0(sbsmnsldt0(xS))
| ( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
=> ( isOpen0(stldt0(sbsmnsldt0(xS)))
| ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
=> ? [W1] :
( ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( isClosed0(sbsmnsldt0(xS))
| ( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
=> ( isOpen0(stldt0(sbsmnsldt0(xS)))
| ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
=> ? [W1] :
( ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sbsmnsldt0(xS))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_38,plain,
! [W0] :
( isClosed0(sbsmnsldt0(W0))
| ? [W1] :
( ( ~ isClosed0(W1)
| ~ aSubsetOf0(W1,cS1395) )
& aElementOf0(W1,W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(fof_nnf,[status(thm)],[mUnionSClosed]) ).
fof(sk_mUnionSClosed_sk,plain,
! [W0] :
( isClosed0(sbsmnsldt0(W0))
| ( ( ~ isClosed0(sK0(W0))
| ~ aSubsetOf0(sK0(W0),cS1395) )
& aElementOf0(sK0(W0),W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W1,sK0(W0))],[nnf_38]) ).
fof(sk_mUnionSClosed,plain,
( ! [VAR_0] :
( isClosed0(sbsmnsldt0(VAR_0))
| ~ isClosed0(sK0(VAR_0))
| ~ aSubsetOf0(sK0(VAR_0),cS1395)
| ~ isFinite0(VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( isClosed0(sbsmnsldt0(VAR_0))
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ isFinite0(VAR_0)
| ~ aSet0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mUnionSClosed_sk]) ).
cnf(c_57,plain,
( isClosed0(sbsmnsldt0(A))
| ~ isClosed0(sK0(A))
| ~ aSubsetOf0(sK0(A),cS1395)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(split_conjunct,[status(thm)],[sk_mUnionSClosed]) ).
fof(m__2117,axiom,
isFinite0(xS),
file('theBenchmark.p',m__2117) ).
cnf(c_58,plain,
isFinite0(xS),
inference(clausify,[status(thm)],[m__2117]) ).
cnf(c_59,plain,
( isClosed0(sbsmnsldt0(A))
| aElementOf0(sK0(A),A)
| ~ isFinite0(A)
| ~ aSet0(A) ),
inference(split_conjunct,[status(thm)],[sk_mUnionSClosed]) ).
cnf(c_60,plain,
( isClosed0(sbsmnsldt0(xS))
| aElementOf0(sK0(xS),xS)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_59,c_58]) ).
cnf(c_61,plain,
( isClosed0(sbsmnsldt0(xS))
| ~ isClosed0(sK0(xS))
| ~ aSubsetOf0(sK0(xS),cS1395)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_57,c_58]) ).
fof(mIntZero,axiom,
aInteger0(sz00),
file('theBenchmark.p',mIntZero) ).
cnf(c_62,plain,
aInteger0(sz00),
inference(clausify,[status(thm)],[mIntZero]) ).
cnf(c_182,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(A,B),cS1395)
| B = sz00
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mArSeqClosed]) ).
cnf(c_183,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(A,B),cS1395)
| sz00 = B
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_182]) ).
cnf(c_184,plain,
( isClosed0(szAzrzSzezqlpdtcmdtrp0(A,B))
| B = sz00
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mArSeqClosed]) ).
cnf(c_185,plain,
( isClosed0(szAzrzSzezqlpdtcmdtrp0(A,B))
| sz00 = B
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_184]) ).
fof(nnf_40,plain,
( cS2043 = xS
& ! [W0] :
( ( aElementOf0(W0,xS)
| ! [W1] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,W1) != W0
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [X4] :
( sdtasdt0(W1,X4) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(X4) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) ) )
& ( ? [X0] :
( szAzrzSzezqlpdtcmdtrp0(sz00,X0) = W0
& ! [X1] :
( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0))
| ( ~ sdteqdtlpzmzozddtrp0(X1,sz00,X0)
& ~ aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))
& ! [X3] :
( sdtasdt0(X0,X3) != sdtpldt0(X1,smndt0(sz00))
| ~ aInteger0(X3) ) )
| ~ aInteger0(X1) )
& ( ( sdteqdtlpzmzozddtrp0(X1,sz00,X0)
& aDivisorOf0(X0,sdtpldt0(X1,smndt0(sz00)))
& ? [X2] :
( sdtasdt0(X0,X2) = sdtpldt0(X1,smndt0(sz00))
& aInteger0(X2) )
& aInteger0(X1) )
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,X0)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X0))
& isPrime0(X0)
& X0 != sz00
& aInteger0(X0) )
| ~ aElementOf0(W0,xS) ) )
& aSet0(xS) ),
inference(fof_nnf,[status(thm)],[m__2046]) ).
fof(sk_m__2046_sk,plain,
( cS2043 = xS
& ! [W0] :
( ( aElementOf0(W0,xS)
| ! [W1] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,W1) != W0
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& sdtasdt0(W1,sK3(W0,W1,W2)) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(sK3(W0,W1,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) ) )
& ( ( szAzrzSzezqlpdtcmdtrp0(sz00,sK1(W0)) = W0
& ! [X1] :
( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(X1,sz00,sK1(W0))
& ~ aDivisorOf0(sK1(W0),sdtpldt0(X1,smndt0(sz00)))
& ! [X3] :
( sdtasdt0(sK1(W0),X3) != sdtpldt0(X1,smndt0(sz00))
| ~ aInteger0(X3) ) )
| ~ aInteger0(X1) )
& ( ( sdteqdtlpzmzozddtrp0(X1,sz00,sK1(W0))
& aDivisorOf0(sK1(W0),sdtpldt0(X1,smndt0(sz00)))
& sdtasdt0(sK1(W0),sK2(W0,X1)) = sdtpldt0(X1,smndt0(sz00))
& aInteger0(sK2(W0,X1))
& aInteger0(X1) )
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(W0))) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK1(W0)))
& isPrime0(sK1(W0))
& sK1(W0) != sz00
& aInteger0(sK1(W0)) )
| ~ aElementOf0(W0,xS) ) )
& aSet0(xS) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1(W0)),skolemize(X2,sK2(W0,X1)),skolemize(X4,sK3(W0,W1,W2))],[nnf_40]) ).
fof(sk_m__2046,plain,
( cS2043 = xS
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0) != VAR_1
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ sdteqdtlpzmzozddtrp0(VAR_1,sz00,VAR_0)
| ~ aInteger0(VAR_1)
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ aDivisorOf0(VAR_0,sdtpldt0(VAR_1,smndt0(sz00)))
| ~ aInteger0(VAR_1)
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( aElementOf0(VAR_3,xS)
| aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| sdtasdt0(VAR_0,VAR_2) != sdtpldt0(VAR_1,smndt0(sz00))
| ~ aInteger0(VAR_2)
| ~ aInteger0(VAR_1)
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| sdteqdtlpzmzozddtrp0(VAR_1,sz00,VAR_0)
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| aDivisorOf0(VAR_0,sdtpldt0(VAR_1,smndt0(sz00)))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| sdtasdt0(VAR_0,sK3(VAR_2,VAR_0,VAR_1)) = sdtpldt0(VAR_1,smndt0(sz00))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| aInteger0(sK3(VAR_2,VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_2,xS)
| aInteger0(VAR_1)
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,VAR_0))
| ~ isPrime0(VAR_0)
| VAR_0 = sz00
| ~ aInteger0(VAR_0) )
& ! [VAR_0] :
( szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)) = VAR_0
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ sdteqdtlpzmzozddtrp0(VAR_1,sz00,sK1(VAR_0))
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aDivisorOf0(sK1(VAR_0),sdtpldt0(VAR_1,smndt0(sz00)))
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| sdtasdt0(sK1(VAR_0),VAR_2) != sdtpldt0(VAR_1,smndt0(sz00))
| ~ aInteger0(VAR_2)
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( sdteqdtlpzmzozddtrp0(VAR_1,sz00,sK1(VAR_0))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( aDivisorOf0(sK1(VAR_0),sdtpldt0(VAR_1,smndt0(sz00)))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(sK1(VAR_0),sK2(VAR_0,VAR_1)) = sdtpldt0(VAR_1,smndt0(sz00))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( aInteger0(sK2(VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0,VAR_1] :
( aInteger0(VAR_1)
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0] :
( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK1(VAR_0)))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0] :
( isPrime0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0] :
( sK1(VAR_0) != sz00
| ~ aElementOf0(VAR_0,xS) )
& ! [VAR_0] :
( aInteger0(sK1(VAR_0))
| ~ aElementOf0(VAR_0,xS) )
& aSet0(xS) ),
inference(cnf_transformation,[status(thm)],[sk_m__2046_sk]) ).
cnf(c_186,plain,
aSet0(xS),
inference(split_conjunct,[status(thm)],[sk_m__2046]) ).
cnf(c_187,plain,
( aInteger0(sK1(A))
| ~ aElementOf0(A,xS) ),
inference(split_conjunct,[status(thm)],[sk_m__2046]) ).
cnf(c_188,plain,
( sK1(A) != sz00
| ~ aElementOf0(A,xS) ),
inference(split_conjunct,[status(thm)],[sk_m__2046]) ).
cnf(c_198,plain,
( szAzrzSzezqlpdtcmdtrp0(sz00,sK1(A)) = A
| ~ aElementOf0(A,xS) ),
inference(split_conjunct,[status(thm)],[sk_m__2046]) ).
cnf(c_249,negated_conjecture,
~ isClosed0(sbsmnsldt0(xS)),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_13900,plain,
( isClosed0(sbsmnsldt0(xS))
| ~ isClosed0(sK0(xS))
| ~ aSubsetOf0(sK0(xS),cS1395) ),
inference(resolve,[status(thm)],[c_186,c_61]) ).
cnf(c_359,negated_conjecture,
( ~ isClosed0(sK0(xS))
| ~ aSubsetOf0(sK0(xS),cS1395) ),
inference(resolve,[status(thm)],[c_249,c_13900]) ).
cnf(c_13901,plain,
( isClosed0(sbsmnsldt0(xS))
| aElementOf0(sK0(xS),xS) ),
inference(resolve,[status(thm)],[c_186,c_60]) ).
cnf(c_360,negated_conjecture,
aElementOf0(sK0(xS),xS),
inference(resolve,[status(thm)],[c_249,c_13901]) ).
cnf(c_697,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,A),cS1395)
| sz00 = A
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_183,c_62]) ).
cnf(c_700,plain,
( isClosed0(szAzrzSzezqlpdtcmdtrp0(sz00,A))
| sz00 = A
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_185,c_62]) ).
cnf(c_1090,plain,
szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sK0(xS))) = sK0(xS),
inference(resolve,[status(thm)],[c_360,c_198]) ).
cnf(c_1100,plain,
sK1(sK0(xS)) != sz00,
inference(resolve,[status(thm)],[c_360,c_188]) ).
cnf(c_1101,plain,
aInteger0(sK1(sK0(xS))),
inference(resolve,[status(thm)],[c_360,c_187]) ).
cnf(c_13902,plain,
( isClosed0(szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sK0(xS))))
| sz00 = sK1(sK0(xS)) ),
inference(resolve,[status(thm)],[c_1101,c_700]) ).
cnf(c_13903,plain,
( isClosed0(sK0(xS))
| sz00 = sK1(sK0(xS)) ),
inference(paramod,[status(thm)],[c_1090,c_13902]) ).
cnf(c_13904,plain,
( isClosed0(sK0(xS))
| sK1(sK0(xS)) = sz00 ),
inference(copy,[status(thm)],[c_13903]) ).
cnf(c_7914,plain,
isClosed0(sK0(xS)),
inference(resolve,[status(thm)],[c_1100,c_13904]) ).
cnf(c_8212,negated_conjecture,
~ aSubsetOf0(sK0(xS),cS1395),
inference(resolve,[status(thm)],[c_7914,c_359]) ).
cnf(c_13905,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sK0(xS))),cS1395)
| sz00 = sK1(sK0(xS)) ),
inference(resolve,[status(thm)],[c_697,c_1101]) ).
cnf(c_13906,plain,
( aSubsetOf0(sK0(xS),cS1395)
| sz00 = sK1(sK0(xS)) ),
inference(paramod,[status(thm)],[c_1090,c_13905]) ).
cnf(c_13907,plain,
( aSubsetOf0(sK0(xS),cS1395)
| sK1(sK0(xS)) = sz00 ),
inference(copy,[status(thm)],[c_13906]) ).
cnf(c_13908,plain,
aSubsetOf0(sK0(xS),cS1395),
inference(resolve,[status(thm)],[c_1100,c_13907]) ).
cnf(c_13899,plain,
$false,
inference(resolve,[status(thm)],[c_8212,c_13908]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM449+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.60 % Computer : n008.cluster.edu
% 0.10/5.60 % Model : x86_64 x86_64
% 0.10/5.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.60 % Memory : 8046.5625MB
% 0.10/5.60 % OS : Linux 6.8.0-71-generic
% 0.10/5.60 % CPULimit : 300
% 0.10/5.60 % WCLimit : 300
% 0.14/5.60 % DateTime : Sat Sep 26 02:48:31 UTC 2026
% 0.14/5.60 % CPUTime :
% 0.14/5.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/5.60 % Process 2630337 was started by sandbox2 on n008,
% 0.14/5.60 % Sat Sep 26 02:48:31 2026
% 0.14/5.60 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/5.62
% 0.14/5.62 % From the command line: assign(max_seconds, 300).
% 20.37/8.63
% 20.37/8.63 % given #500 (F,wt=26): 4165 -aDivisorOf0(f16(f15(xS)),smndt0(c1)) | smndt0(c1) != smndt0(sz10). [resolve(2124,a,360,a)].
% 20.37/8.63
% 20.37/8.63 % SZS status Theorem for theBenchmark
% 20.37/8.63
% 20.37/8.63 % Proof 1 at 2.52 (+ 0.43) seconds.
% 20.37/8.63 % Length of proof is 29.
% 20.37/8.63 % Level of proof is 7.
% 20.37/8.63 % Maximum clause weight is 28.000.
% 20.37/8.63 % Given clauses 910.
% 20.37/8.63
% 20.37/8.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------