%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM450+6 : 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 : n017.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 0.14s 15.83s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 27 ( 7 unt; 0 def)
% Number of atoms : 411 ( 43 equ)
% Maximal formula atoms : 115 ( 15 avg)
% Number of connectives : 551 ( 167 ~; 150 |; 203 &)
% ( 11 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-2 aty)
% Number of variables : 145 ( 0 sgn 111 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__2079,axiom,
( stldt0(sbsmnsldt0(xS)) = cS2076
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( W0 = smndt0(sz10)
| W0 = sz10 ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) ),
file('theBenchmark.p',m__2079) ).
fof(m__2144,axiom,
( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
=> ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sbsmnsldt0(xS))) )
& ! [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))
& W1 != sz00
& aInteger0(W1) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS))
& isClosed0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
=> ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sbsmnsldt0(xS))) )
& ! [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))
& W1 != sz00
& aInteger0(W1) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) ),
file('theBenchmark.p',m__2144) ).
fof(m__,conjecture,
? [W0] :
( ( ( ! [W1] :
( ( ( ( sdteqdtlpzmzozddtrp0(W1,sz10,W0)
| aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))
| ? [W2] :
( sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10))
& aInteger0(W2) ) )
& aInteger0(W1) )
=> aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
& ( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))
=> ( sdteqdtlpzmzozddtrp0(W1,sz10,W0)
& aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))
& ? [W2] :
( sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10))
& aInteger0(W2) )
& aInteger0(W1) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
=> ( ( ! [W1] :
( aElementOf0(W1,sbsmnsldt0(xS))
<=> ( ? [W2] :
( aElementOf0(W1,W2)
& aElementOf0(W2,xS) )
& aInteger0(W1) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( ! [W1] :
( aElementOf0(W1,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W1,sbsmnsldt0(xS))
& aInteger0(W1) ) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))
| ! [W1] :
( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))
=> aElementOf0(W1,stldt0(sbsmnsldt0(xS))) ) ) ) ) )
& W0 != sz00
& aInteger0(W0) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( ( ( ! [W1] :
( ( ( ( sdteqdtlpzmzozddtrp0(W1,sz10,W0)
| aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))
| ? [W2] :
( sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10))
& aInteger0(W2) ) )
& aInteger0(W1) )
=> aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
& ( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))
=> ( sdteqdtlpzmzozddtrp0(W1,sz10,W0)
& aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))
& ? [W2] :
( sdtasdt0(W0,W2) = sdtpldt0(W1,smndt0(sz10))
& aInteger0(W2) )
& aInteger0(W1) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
=> ( ( ! [W1] :
( aElementOf0(W1,sbsmnsldt0(xS))
<=> ( ? [W2] :
( aElementOf0(W1,W2)
& aElementOf0(W2,xS) )
& aInteger0(W1) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( ! [W1] :
( aElementOf0(W1,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W1,sbsmnsldt0(xS))
& aInteger0(W1) ) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))
| ! [W1] :
( aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0))
=> aElementOf0(W1,stldt0(sbsmnsldt0(xS))) ) ) ) ) )
& W0 != sz00
& aInteger0(W0) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_211,plain,
( sz10 != A
| aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(clausify,[status(thm)],[m__2079]) ).
cnf(c_213,plain,
stldt0(sbsmnsldt0(xS)) = cS2076,
inference(clausify,[status(thm)],[m__2079]) ).
fof(nnf_42,plain,
( ! [W0] :
( ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))
& ! [W2] :
( aElementOf0(W2,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
| ( ~ sdteqdtlpzmzozddtrp0(X2,W0,W1)
& ~ aDivisorOf0(W1,sdtpldt0(X2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(X2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(X2) )
& ( ( sdteqdtlpzmzozddtrp0(X2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(X2,smndt0(W0)))
& ? [X0] :
( sdtasdt0(W1,X0) = sdtpldt0(X2,smndt0(W0))
& aInteger0(X0) )
& aInteger0(X2) )
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1))
& W1 != sz00
& aInteger0(W1) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [X1] :
( ( aElementOf0(X1,sbsmnsldt0(xS))
| ~ aInteger0(X1)
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(X1,sbsmnsldt0(xS))
& aInteger0(X1) )
| ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& ! [X13] :
( ( ! [X15] :
( ~ aElementOf0(X13,X15)
| ~ aElementOf0(X15,xS) )
| ~ aInteger0(X13)
| aElementOf0(X13,sbsmnsldt0(xS)) )
& ( ( ? [X14] :
( aElementOf0(X13,X14)
& aElementOf0(X14,xS) )
& aInteger0(X13) )
| ~ aElementOf0(X13,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& isClosed0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& ! [X7] :
( ? [X8] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X7,X8),stldt0(sbsmnsldt0(xS)))
& ! [X12] :
( aElementOf0(X12,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X7,X8)) )
& ! [X9] :
( ( aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(X7,X8))
| ( ~ sdteqdtlpzmzozddtrp0(X9,X7,X8)
& ~ aDivisorOf0(X8,sdtpldt0(X9,smndt0(X7)))
& ! [X11] :
( sdtasdt0(X8,X11) != sdtpldt0(X9,smndt0(X7))
| ~ aInteger0(X11) ) )
| ~ aInteger0(X9) )
& ( ( sdteqdtlpzmzozddtrp0(X9,X7,X8)
& aDivisorOf0(X8,sdtpldt0(X9,smndt0(X7)))
& ? [X10] :
( sdtasdt0(X8,X10) = sdtpldt0(X9,smndt0(X7))
& aInteger0(X10) )
& aInteger0(X9) )
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(X7,X8)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X7,X8))
& X8 != sz00
& aInteger0(X8) )
| ~ aElementOf0(X7,stldt0(sbsmnsldt0(xS))) )
& ! [X6] :
( ( aElementOf0(X6,sbsmnsldt0(xS))
| ~ aInteger0(X6)
| aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(X6,sbsmnsldt0(xS))
& aInteger0(X6) )
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ) )
& ! [X3] :
( ( ! [X5] :
( ~ aElementOf0(X3,X5)
| ~ aElementOf0(X5,xS) )
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(xS)) )
& ( ( ? [X4] :
( aElementOf0(X3,X4)
& aElementOf0(X4,xS) )
& aInteger0(X3) )
| ~ aElementOf0(X3,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS)) ),
inference(fof_nnf,[status(thm)],[m__2144]) ).
fof(sk_m__2144_sk,plain,
( ! [W0] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK0(W0)),stldt0(sbsmnsldt0(xS)))
& ! [W2] :
( aElementOf0(W2,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK0(W0))) )
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(W0,sK0(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(X2,W0,sK0(W0))
& ~ aDivisorOf0(sK0(W0),sdtpldt0(X2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(sK0(W0),W3) != sdtpldt0(X2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(X2) )
& ( ( sdteqdtlpzmzozddtrp0(X2,W0,sK0(W0))
& aDivisorOf0(sK0(W0),sdtpldt0(X2,smndt0(W0)))
& sdtasdt0(sK0(W0),sK6(W0,X2)) = sdtpldt0(X2,smndt0(W0))
& aInteger0(sK6(W0,X2))
& aInteger0(X2) )
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(W0,sK0(W0))) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK0(W0)))
& sK0(W0) != sz00
& aInteger0(sK0(W0)) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [X1] :
( ( aElementOf0(X1,sbsmnsldt0(xS))
| ~ aInteger0(X1)
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(X1,sbsmnsldt0(xS))
& aInteger0(X1) )
| ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& ! [X13] :
( ( ! [X15] :
( ~ aElementOf0(X13,X15)
| ~ aElementOf0(X15,xS) )
| ~ aInteger0(X13)
| aElementOf0(X13,sbsmnsldt0(xS)) )
& ( ( aElementOf0(X13,sK5(X13))
& aElementOf0(sK5(X13),xS)
& aInteger0(X13) )
| ~ aElementOf0(X13,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& isClosed0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& ! [X7] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X7,sK3(X7)),stldt0(sbsmnsldt0(xS)))
& ! [X12] :
( aElementOf0(X12,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X7,sK3(X7))) )
& ! [X9] :
( ( aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(X7,sK3(X7)))
| ( ~ sdteqdtlpzmzozddtrp0(X9,X7,sK3(X7))
& ~ aDivisorOf0(sK3(X7),sdtpldt0(X9,smndt0(X7)))
& ! [X11] :
( sdtasdt0(sK3(X7),X11) != sdtpldt0(X9,smndt0(X7))
| ~ aInteger0(X11) ) )
| ~ aInteger0(X9) )
& ( ( sdteqdtlpzmzozddtrp0(X9,X7,sK3(X7))
& aDivisorOf0(sK3(X7),sdtpldt0(X9,smndt0(X7)))
& sdtasdt0(sK3(X7),sK4(X7,X9)) = sdtpldt0(X9,smndt0(X7))
& aInteger0(sK4(X7,X9))
& aInteger0(X9) )
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(X7,sK3(X7))) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X7,sK3(X7)))
& sK3(X7) != sz00
& aInteger0(sK3(X7)) )
| ~ aElementOf0(X7,stldt0(sbsmnsldt0(xS))) )
& ! [X6] :
( ( aElementOf0(X6,sbsmnsldt0(xS))
| ~ aInteger0(X6)
| aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(X6,sbsmnsldt0(xS))
& aInteger0(X6) )
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ) )
& ! [X3] :
( ( ! [X5] :
( ~ aElementOf0(X3,X5)
| ~ aElementOf0(X5,xS) )
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(xS)) )
& ( ( aElementOf0(X3,sK2(X3))
& aElementOf0(sK2(X3),xS)
& aInteger0(X3) )
| ~ aElementOf0(X3,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK0,sK6]),skolemize(X4,sK2(X3)),skolemize(X8,sK3(X7)),skolemize(X10,sK4(X7,X9)),skolemize(X14,sK5(X13)),skolemize(W1,sK0(W0)),skolemize(X0,sK6(W0,X2))],[nnf_42]) ).
fof(sk_m__2144,plain,
( ! [VAR_0] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ sdteqdtlpzmzozddtrp0(VAR_1,VAR_0,sK0(VAR_0))
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aDivisorOf0(sK0(VAR_0),sdtpldt0(VAR_1,smndt0(VAR_0)))
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| sdtasdt0(sK0(VAR_0),VAR_2) != sdtpldt0(VAR_1,smndt0(VAR_0))
| ~ aInteger0(VAR_2)
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( sdteqdtlpzmzozddtrp0(VAR_1,VAR_0,sK0(VAR_0))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aDivisorOf0(sK0(VAR_0),sdtpldt0(VAR_1,smndt0(VAR_0)))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(sK0(VAR_0),sK6(VAR_0,VAR_1)) = sdtpldt0(VAR_1,smndt0(VAR_0))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aInteger0(sK6(VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aInteger0(VAR_1)
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( aSet0(szAzrzSzezqlpdtcmdtrp0(VAR_0,sK0(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( sK0(VAR_0) != sz00
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( aInteger0(sK0(VAR_0))
| ~ aElementOf0(VAR_0,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))) )
& ! [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)) )
& isClosed0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& ! [VAR_0] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ sdteqdtlpzmzozddtrp0(VAR_1,VAR_0,sK3(VAR_0))
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aDivisorOf0(sK3(VAR_0),sdtpldt0(VAR_1,smndt0(VAR_0)))
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| sdtasdt0(sK3(VAR_0),VAR_2) != sdtpldt0(VAR_1,smndt0(VAR_0))
| ~ aInteger0(VAR_2)
| ~ aInteger0(VAR_1)
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( sdteqdtlpzmzozddtrp0(VAR_1,VAR_0,sK3(VAR_0))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aDivisorOf0(sK3(VAR_0),sdtpldt0(VAR_1,smndt0(VAR_0)))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(sK3(VAR_0),sK4(VAR_0,VAR_1)) = sdtpldt0(VAR_1,smndt0(VAR_0))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aInteger0(sK4(VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0,VAR_1] :
( aInteger0(VAR_1)
| ~ aElementOf0(VAR_1,szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( aSet0(szAzrzSzezqlpdtcmdtrp0(VAR_0,sK3(VAR_0)))
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( sK3(VAR_0) != sz00
| ~ aElementOf0(VAR_0,stldt0(sbsmnsldt0(xS))) )
& ! [VAR_0] :
( aInteger0(sK3(VAR_0))
| ~ aElementOf0(VAR_0,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))) )
& ! [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,sK2(VAR_0))
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& ! [VAR_0] :
( aElementOf0(sK2(VAR_0),xS)
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& ! [VAR_0] :
( aInteger0(VAR_0)
| ~ aElementOf0(VAR_0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(cnf_transformation,[status(thm)],[sk_m__2144_sk]) ).
cnf(c_256,plain,
( aInteger0(sK0(A))
| ~ aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m__2144]) ).
cnf(c_257,plain,
( aInteger0(sK0(A))
| ~ aElementOf0(A,cS2076) ),
inference(paramod,[status(thm)],[c_213,c_256]) ).
cnf(c_258,plain,
( sK0(A) != sz00
| ~ aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m__2144]) ).
cnf(c_259,plain,
( sK0(A) != sz00
| ~ aElementOf0(A,cS2076) ),
inference(paramod,[status(thm)],[c_213,c_258]) ).
cnf(c_280,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(A,sK0(A)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(A,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[sk_m__2144]) ).
cnf(c_1798,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(A,sK0(A)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(A,cS2076) ),
inference(paramod,[status(thm)],[c_213,c_280]) ).
cnf(c_281,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(A,sK0(A)),cS2076)
| ~ aElementOf0(A,cS2076) ),
inference(paramod,[status(thm)],[c_213,c_1798]) ).
cnf(c_299,negated_conjecture,
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,A),stldt0(sbsmnsldt0(xS)))
| sz00 = A
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_300,negated_conjecture,
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,A),cS2076)
| sz00 = A
| ~ aInteger0(A) ),
inference(paramod,[status(thm)],[c_213,c_299]) ).
cnf(c_413,plain,
( sz10 != A
| aElementOf0(A,cS2076) ),
inference(paramod,[status(thm)],[c_213,c_211]) ).
cnf(c_1114,plain,
aElementOf0(sz10,cS2076),
inference(xxres,[status(thm)],[c_413]) ).
cnf(c_1588,plain,
aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,sK0(sz10)),cS2076),
inference(resolve,[status(thm)],[c_1114,c_281]) ).
cnf(c_1599,plain,
sK0(sz10) != sz00,
inference(resolve,[status(thm)],[c_1114,c_259]) ).
cnf(c_1600,plain,
aInteger0(sK0(sz10)),
inference(resolve,[status(thm)],[c_1114,c_257]) ).
cnf(c_1799,negated_conjecture,
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,sK0(sz10)),cS2076)
| sz00 = sK0(sz10) ),
inference(resolve,[status(thm)],[c_1600,c_300]) ).
cnf(c_1800,negated_conjecture,
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,sK0(sz10)),cS2076)
| sK0(sz10) = sz00 ),
inference(copy,[status(thm)],[c_1799]) ).
cnf(c_1801,negated_conjecture,
~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,sK0(sz10)),cS2076),
inference(resolve,[status(thm)],[c_1599,c_1800]) ).
cnf(c_1797,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1588,c_1801]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM450+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/15.39 % Computer : n017.cluster.edu
% 0.09/15.39 % Model : x86_64 x86_64
% 0.09/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.39 % Memory : 8046.5625MB
% 0.09/15.39 % OS : Linux 6.8.0-71-generic
% 0.09/15.39 % CPULimit : 300
% 0.09/15.39 % WCLimit : 300
% 0.09/15.39 % DateTime : Sat Sep 26 02:43:04 UTC 2026
% 0.09/15.39 % CPUTime :
% 0.09/15.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/15.39 % Process 3818041 was started by sandbox on n017,
% 0.09/15.39 % Sat Sep 26 02:43:04 2026
% 0.09/15.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/15.42
% 0.14/15.42 % From the command line: assign(max_seconds, 300).
% 0.14/15.83
% 0.14/15.83 % SZS status Theorem for theBenchmark
% 0.14/15.83
% 0.14/15.83 % Proof 1 at 0.23 (+ 0.05) seconds.
% 0.14/15.83 % Length of proof is 19.
% 0.14/15.83 % Level of proof is 5.
% 0.14/15.83 % Maximum clause weight is 24.000.
% 0.14/15.83 % Given clauses 346.
% 0.14/15.83
% 0.14/15.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------