%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM449+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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 : Fri Sep 25 02:20:04 PM UTC 2026
% Result : Theorem 262.61s 37.93s
% Output : Proof 262.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 16
% Syntax : Number of formulae : 133 ( 91 unt; 3 def)
% Number of atoms : 592 ( 175 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 668 ( 209 ~; 185 |; 233 &)
% ( 12 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 32 ( 32 usr; 9 con; 0-4 aty)
% Number of variables : 169 ( 2 sgn 82 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
! [W0] :
( ( ! [W1] :
( aElementOf0(W1,W0)
=> ( isClosed0(W1)
& aSubsetOf0(W1,cS1395) ) )
& isFinite0(W0)
& aSet0(W0) )
=> isClosed0(sbsmnsldt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mUnionSClosed) ).
fof(f39_nnf,plain,
! [W0] :
( isClosed0(sbsmnsldt0(W0))
| ? [W1] :
( ( ~ isClosed0(W1)
| ~ aSubsetOf0(W1,cS1395) )
& aElementOf0(W1,W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [W0] :
( isClosed0(sbsmnsldt0(W0))
| ( ( ~ isClosed0(sk14(W0))
| ~ aSubsetOf0(sk14(W0),cS1395) )
& aElementOf0(sk14(W0),W0) )
| ~ isFinite0(W0)
| ~ aSet0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f39_nnf]) ).
cnf(c132,plain,
( isClosed0(sbsmnsldt0(X0))
| ~ isClosed0(sk14(X0))
| ~ aSubsetOf0(sk14(X0),cS1395)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t184,plain,
ifeq(aSet0(X1),true,ifeq(isFinite0(X1),true,ifeq(aSubsetOf0(sk14(X1),cS1395),true,ifeq(isClosed0(sk14(X1)),true,isClosed0(sbsmnsldt0(X1)),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c132]) ).
cnf(t389,plain,
ifeq(aSet0(X1),true,ifeq(isFinite0(X1),true,ifeq(aSubsetOf0(sk14(X1),cS1395),true,ifeq(isClosed0(sk14(X1)),true,isClosed0(sbsmnsldt0(X1)),true),true),true),true) = true,
inference(orient,[status(thm)],[t184]) ).
fof(f40,axiom,
! [W0,W1] :
( ( W1 != sz00
& aInteger0(W1)
& aInteger0(W0) )
=> ( isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArSeqClosed) ).
fof(f40_nnf,plain,
! [W0,W1] :
( ( isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) )
| W1 = sz00
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [W0,W1] :
( ( isClosed0(szAzrzSzezqlpdtcmdtrp0(W0,W1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),cS1395) )
| W1 = sz00
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c133,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS1395)
| X1 = sz00
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t149,plain,
ifeq(aInteger0(X1),true,ifeq(aInteger0(X2),true,or(eq(X2,sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),cS1395)),true),true) = true,
inference(equality_encoding,[status(esa)],[c133]) ).
cnf(t318,plain,
ifeq(aInteger0(X1),true,ifeq(aInteger0(X2),true,or(eq(X2,sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),cS1395)),true),true) = true,
inference(orient,[status(thm)],[t149]) ).
fof(f1,axiom,
aInteger0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntZero) ).
fof(f1_nnf,plain,
aInteger0(sz00),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
aInteger0(sz00),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(t2,plain,
aInteger0(sz00) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t834,plain,
aInteger0(sz00) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t870,plain,
true = ifeq(true,true,ifeq(aInteger0(X1),true,or(eq(X1,sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X1),cS1395)),true),true),
inference(cp,[status(thm)],[t318,t834]) ).
cnf(t52,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t52]) ).
cnf(t334448,plain,
true = ifeq(aInteger0(X1),true,or(eq(X1,sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X1),cS1395)),true),
inference(step,[status(thm)],[t870,t256]) ).
cnf(t328781,plain,
ifeq(aInteger0(X1),true,or(eq(X1,sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X1),cS1395)),true) = true,
inference(orient,[status(thm)],[t334448]) ).
fof(f41,hypothesis,
( 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('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2046) ).
fof(f41_nnf,plain,
( xS = cS2043
& ! [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)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) ) )
& ( ? [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)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) )
| ~ aElementOf0(W0,xS) ) )
& aSet0(xS) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [W0,W2,W3,W1] :
( xS = cS2043
& ( aElementOf0(W0,xS)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,W1) != W0
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& sdtasdt0(W1,sk17(W0,W1,W2)) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(sk17(W0,W1,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) )
& ( ( szAzrzSzezqlpdtcmdtrp0(sz00,sk15(W0)) = W0
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,sk15(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,sk15(W0))
& ~ aDivisorOf0(sk15(W0),sdtpldt0(W2,smndt0(sz00)))
& ( sdtasdt0(sk15(W0),W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sz00,sk15(W0))
& aDivisorOf0(sk15(W0),sdtpldt0(W2,smndt0(sz00)))
& sdtasdt0(sk15(W0),sk16(W0,W2)) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(sk16(W0,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,sk15(W0))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sk15(W0)))
& isPrime0(sk15(W0))
& sk15(W0) != sz00
& aInteger0(sk15(W0)) )
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16,sk17])],[f41_nnf]) ).
cnf(c136,plain,
( aInteger0(sk15(X0))
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t85,plain,
ifeq(aElementOf0(X1,xS),true,aInteger0(sk15(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c136]) ).
cnf(t276,plain,
ifeq(aElementOf0(X1,xS),true,aInteger0(sk15(X1)),true) = true,
inference(orient,[status(thm)],[t85]) ).
cnf(c131,plain,
( isClosed0(sbsmnsldt0(X0))
| aElementOf0(sk14(X0),X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t145,plain,
ifeq(aSet0(X1),true,ifeq(isFinite0(X1),true,or(aElementOf0(sk14(X1),X1),isClosed0(sbsmnsldt0(X1))),true),true) = true,
inference(equality_encoding,[status(esa)],[c131]) ).
cnf(t390,plain,
ifeq(aSet0(X1),true,ifeq(isFinite0(X1),true,or(aElementOf0(sk14(X1),X1),isClosed0(sbsmnsldt0(X1))),true),true) = true,
inference(orient,[status(thm)],[t145]) ).
fof(f44,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('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f44_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(negated_conjecture,[status(cth)],[f44]) ).
fof(f44_nnf,plain,
( ~ isClosed0(sbsmnsldt0(xS))
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sbsmnsldt0(xS)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(sbsmnsldt0(xS)))
& aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ! [W2] :
( ( 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) )
& ( ( 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)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& ! [W0] :
( ( ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS)) ),
inference(nnf_transformation,[status(thm)],[f44_neg]) ).
fof(f44_sk,plain,
! [W0,W1,W2,W3] :
( ~ isClosed0(sbsmnsldt0(xS))
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sk20,W1),stldt0(sbsmnsldt0(xS)))
& ~ aElementOf0(sk22(W1),stldt0(sbsmnsldt0(xS)))
& aElementOf0(sk22(W1),szAzrzSzezqlpdtcmdtrp0(sk20,W1))
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sk20,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sk20,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sk20)))
& ( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sk20))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sk20,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sk20)))
& sdtasdt0(W1,sk21(W1,W2)) = sdtpldt0(W2,smndt0(sk20))
& aInteger0(sk21(W1,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sk20,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sk20,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(sk20,stldt0(sbsmnsldt0(xS)))
& ( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS)
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ( ( aElementOf0(W0,sk19(W0))
& aElementOf0(sk19(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19,sk20,sk21,sk22])],[f44_nnf]) ).
cnf(c196,plain,
~ isClosed0(sbsmnsldt0(xS)),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(t14,plain,
isClosed0(sbsmnsldt0(xS)) = false,
inference(equality_encoding,[status(esa)],[c196]) ).
cnf(t3356,plain,
isClosed0(sbsmnsldt0(xS)) = false,
inference(orient,[status(thm)],[t14]) ).
cnf(t3359,plain,
true = ifeq(aSet0(xS),true,ifeq(isFinite0(xS),true,or(aElementOf0(sk14(xS),xS),false),true),true),
inference(cp,[status(thm)],[t390,t3356]) ).
cnf(c135,plain,
aSet0(xS),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t4,plain,
aSet0(xS) = true,
inference(equality_encoding,[status(esa)],[c135]) ).
cnf(t2262,plain,
aSet0(xS) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t330503,plain,
true = ifeq(true,true,ifeq(isFinite0(xS),true,or(aElementOf0(sk14(xS),xS),false),true),true),
inference(step,[status(thm)],[t3359,t2262]) ).
cnf(t330504,plain,
true = ifeq(isFinite0(xS),true,or(aElementOf0(sk14(xS),xS),false),true),
inference(step,[status(thm)],[t330503,t256]) ).
fof(f43,hypothesis,
isFinite0(xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2117) ).
fof(f43_nnf,plain,
isFinite0(xS),
inference(nnf_transformation,[status(thm)],[f43]) ).
cnf(c173,plain,
isFinite0(xS),
inference(cnf_transformation,[status(esa)],[f43_nnf]) ).
cnf(t5,plain,
isFinite0(xS) = true,
inference(equality_encoding,[status(esa)],[c173]) ).
cnf(t2446,plain,
isFinite0(xS) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t330505,plain,
true = ifeq(true,true,or(aElementOf0(sk14(xS),xS),false),true),
inference(step,[status(thm)],[t330504,t2446]) ).
cnf(t330506,plain,
true = or(aElementOf0(sk14(xS),xS),false),
inference(step,[status(thm)],[t330505,t256]) ).
cnf(t15,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t262,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t15]) ).
cnf(t330507,plain,
true = aElementOf0(sk14(xS),xS),
inference(step,[status(thm)],[t330506,t262]) ).
cnf(t3997,plain,
aElementOf0(sk14(xS),xS) = true,
inference(orient,[status(thm)],[t330507]) ).
cnf(t4000,plain,
true = ifeq(true,true,aInteger0(sk15(sk14(xS))),true),
inference(cp,[status(thm)],[t276,t3997]) ).
cnf(t330509,plain,
true = aInteger0(sk15(sk14(xS))),
inference(step,[status(thm)],[t4000,t256]) ).
cnf(t4077,plain,
aInteger0(sk15(sk14(xS))) = true,
inference(orient,[status(thm)],[t330509]) ).
cnf(t330037,plain,
true = ifeq(true,true,or(eq(sk15(sk14(xS)),sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))),cS1395)),true),
inference(cp,[status(thm)],[t328781,t4077]) ).
cnf(t334457,plain,
true = or(eq(sk15(sk14(xS)),sz00),aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))),cS1395)),
inference(step,[status(thm)],[t330037,t256]) ).
cnf(t66,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t2778,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t66]) ).
cnf(c137,plain,
( sk15(X0) != sz00
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t104,plain,
or(not(aElementOf0(X1,xS)),not(eq(sk15(X1),sz00))) = true,
inference(equality_encoding,[status(esa)],[c137]) ).
cnf(t2127,plain,
or(not(aElementOf0(X1,xS)),not(eq(sk15(X1),sz00))) = true,
inference(orient,[status(thm)],[t104]) ).
cnf(t4002,plain,
true = or(not(true),not(eq(sk15(sk14(xS)),sz00))),
inference(cp,[status(thm)],[t2127,t3997]) ).
cnf(t7,plain,
not(true) = false,
introduced(definition) ).
cnf(t3346,plain,
not(true) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t330559,plain,
true = or(false,not(eq(sk15(sk14(xS)),sz00))),
inference(step,[status(thm)],[t4002,t3346]) ).
cnf(t17,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t263,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t17]) ).
cnf(t330560,plain,
true = not(eq(sk15(sk14(xS)),sz00)),
inference(step,[status(thm)],[t330559,t263]) ).
cnf(t5498,plain,
not(eq(sk15(sk14(xS)),sz00)) = true,
inference(orient,[status(thm)],[t330560]) ).
cnf(t5499,plain,
false = ifeq(true,true,eq(sk15(sk14(xS)),sz00),false),
inference(cp,[status(thm)],[t2778,t5498]) ).
cnf(t330561,plain,
false = eq(sk15(sk14(xS)),sz00),
inference(step,[status(thm)],[t5499,t256]) ).
cnf(t5500,plain,
eq(sk15(sk14(xS)),sz00) = false,
inference(orient,[status(thm)],[t330561]) ).
cnf(t334458,plain,
true = or(false,aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))),cS1395)),
inference(step,[status(thm)],[t334457,t5500]) ).
cnf(t334459,plain,
true = aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))),cS1395),
inference(step,[status(thm)],[t334458,t263]) ).
cnf(c148,plain,
( szAzrzSzezqlpdtcmdtrp0(sz00,sk15(X0)) = X0
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t91,plain,
ifeq(aElementOf0(X1,xS),true,szAzrzSzezqlpdtcmdtrp0(sz00,sk15(X1)),X1) = X1,
inference(equality_encoding,[status(esa)],[c148]) ).
cnf(t257,plain,
ifeq(aElementOf0(X1,xS),true,szAzrzSzezqlpdtcmdtrp0(sz00,sk15(X1)),X1) = X1,
inference(orient,[status(thm)],[t91]) ).
cnf(t3998,plain,
sk14(xS) = ifeq(true,true,szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))),sk14(xS)),
inference(cp,[status(thm)],[t257,t3997]) ).
cnf(t330527,plain,
sk14(xS) = szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))),
inference(step,[status(thm)],[t3998,t256]) ).
cnf(t5034,plain,
szAzrzSzezqlpdtcmdtrp0(sz00,sk15(sk14(xS))) = sk14(xS),
inference(orient,[status(thm)],[t330527]) ).
cnf(t334460,plain,
true = aSubsetOf0(sk14(xS),cS1395),
inference(step,[status(thm)],[t334459,t5034]) ).
cnf(t330255,plain,
aSubsetOf0(sk14(xS),cS1395) = true,
inference(orient,[status(thm)],[t334460]) ).
cnf(t330334,plain,
true = ifeq(aSet0(xS),true,ifeq(isFinite0(xS),true,ifeq(true,true,ifeq(isClosed0(sk14(xS)),true,isClosed0(sbsmnsldt0(xS)),true),true),true),true),
inference(cp,[status(thm)],[t389,t330255]) ).
cnf(t334463,plain,
true = ifeq(true,true,ifeq(isFinite0(xS),true,ifeq(true,true,ifeq(isClosed0(sk14(xS)),true,isClosed0(sbsmnsldt0(xS)),true),true),true),true),
inference(step,[status(thm)],[t330334,t2262]) ).
cnf(t334464,plain,
true = ifeq(isFinite0(xS),true,ifeq(true,true,ifeq(isClosed0(sk14(xS)),true,isClosed0(sbsmnsldt0(xS)),true),true),true),
inference(step,[status(thm)],[t334463,t256]) ).
cnf(t334465,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(isClosed0(sk14(xS)),true,isClosed0(sbsmnsldt0(xS)),true),true),true),
inference(step,[status(thm)],[t334464,t2446]) ).
cnf(t334466,plain,
true = ifeq(true,true,ifeq(isClosed0(sk14(xS)),true,isClosed0(sbsmnsldt0(xS)),true),true),
inference(step,[status(thm)],[t334465,t256]) ).
cnf(t334467,plain,
true = ifeq(isClosed0(sk14(xS)),true,isClosed0(sbsmnsldt0(xS)),true),
inference(step,[status(thm)],[t334466,t256]) ).
cnf(c134,plain,
( isClosed0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
| X1 = sz00
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t142,plain,
ifeq(aInteger0(X1),true,ifeq(aInteger0(X2),true,or(eq(X2,sz00),isClosed0(szAzrzSzezqlpdtcmdtrp0(X1,X2))),true),true) = true,
inference(equality_encoding,[status(esa)],[c134]) ).
cnf(t320,plain,
ifeq(aInteger0(X1),true,ifeq(aInteger0(X2),true,or(eq(X2,sz00),isClosed0(szAzrzSzezqlpdtcmdtrp0(X1,X2))),true),true) = true,
inference(orient,[status(thm)],[t142]) ).
cnf(t5039,plain,
true = ifeq(aInteger0(sz00),true,ifeq(aInteger0(sk15(sk14(xS))),true,or(eq(sk15(sk14(xS)),sz00),isClosed0(sk14(xS))),true),true),
inference(cp,[status(thm)],[t320,t5034]) ).
cnf(t333588,plain,
true = ifeq(true,true,ifeq(aInteger0(sk15(sk14(xS))),true,or(eq(sk15(sk14(xS)),sz00),isClosed0(sk14(xS))),true),true),
inference(step,[status(thm)],[t5039,t834]) ).
cnf(t333589,plain,
true = ifeq(aInteger0(sk15(sk14(xS))),true,or(eq(sk15(sk14(xS)),sz00),isClosed0(sk14(xS))),true),
inference(step,[status(thm)],[t333588,t256]) ).
cnf(t333590,plain,
true = ifeq(true,true,or(eq(sk15(sk14(xS)),sz00),isClosed0(sk14(xS))),true),
inference(step,[status(thm)],[t333589,t4077]) ).
cnf(t333591,plain,
true = or(eq(sk15(sk14(xS)),sz00),isClosed0(sk14(xS))),
inference(step,[status(thm)],[t333590,t256]) ).
cnf(t333592,plain,
true = or(false,isClosed0(sk14(xS))),
inference(step,[status(thm)],[t333591,t5500]) ).
cnf(t333593,plain,
true = isClosed0(sk14(xS)),
inference(step,[status(thm)],[t333592,t263]) ).
cnf(t259008,plain,
isClosed0(sk14(xS)) = true,
inference(orient,[status(thm)],[t333593]) ).
cnf(t334468,plain,
true = ifeq(true,true,isClosed0(sbsmnsldt0(xS)),true),
inference(step,[status(thm)],[t334467,t259008]) ).
cnf(t334469,plain,
true = isClosed0(sbsmnsldt0(xS)),
inference(step,[status(thm)],[t334468,t256]) ).
cnf(t334470,plain,
true = false,
inference(step,[status(thm)],[t334469,t3356]) ).
cnf(t330357,plain,
false = true,
inference(orient,[status(thm)],[t334470]) ).
fof(f17,definition,
! [W0] :
( aInteger0(W0)
=> ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivisor) ).
fof(f17_nnf,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ( ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [W0,W1,W2] :
( ( ( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2)
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ( ( sdtasdt0(W1,sk0(W0,W1)) = W0
& aInteger0(sk0(W0,W1))
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f17_nnf]) ).
cnf(c24,plain,
( X1 != sz00
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f24,axiom,
! [W0] :
( aInteger0(W0)
=> ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) )
<=> ( W0 != smndt0(sz10)
& W0 != sz10 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPrimeDivisor) ).
fof(f24_nnf,plain,
! [W0] :
( ( ( W0 = smndt0(sz10)
| W0 = sz10
| ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) ) )
& ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| ! [W1] :
( ~ isPrime0(W1)
| ~ aDivisorOf0(W1,W0) ) ) )
| ~ aInteger0(W0) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [W0,W1] :
( ( ( W0 = smndt0(sz10)
| W0 = sz10
| ( isPrime0(sk1(W0))
& aDivisorOf0(sk1(W0),W0) ) )
& ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| ~ isPrime0(W1)
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f24_nnf]) ).
cnf(c36,plain,
( X0 != sz10
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(c37,plain,
( X0 != smndt0(sz10)
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f32,definition,
! [W0] :
( aSubsetOf0(W0,cS1395)
=> ! [W1] :
( W1 = stldt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( ~ aElementOf0(W2,W0)
& aInteger0(W2) ) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mComplement) ).
fof(f32_nnf,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ( ~ aElementOf0(W2,W0)
& aInteger0(W2)
& ~ aElementOf0(W2,W1) )
| ( ( aElementOf0(W2,W0)
| ~ aInteger0(W2) )
& aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = stldt0(W0) )
& ( ( ! [W2] :
( ( aElementOf0(W2,W0)
| ~ aInteger0(W2)
| aElementOf0(W2,W1) )
& ( ( ~ aElementOf0(W2,W0)
& aInteger0(W2) )
| ~ aElementOf0(W2,W1) ) )
& aSet0(W1) )
| W1 != stldt0(W0) ) )
| ~ aSubsetOf0(W0,cS1395) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [W0,W1,W2] :
( ( ( ( ~ aElementOf0(sk9(W0,W1),W0)
& aInteger0(sk9(W0,W1))
& ~ aElementOf0(sk9(W0,W1),W1) )
| ( ( aElementOf0(sk9(W0,W1),W0)
| ~ aInteger0(sk9(W0,W1)) )
& aElementOf0(sk9(W0,W1),W1) )
| ~ aSet0(W1)
| W1 = stldt0(W0) )
& ( ( ( aElementOf0(W2,W0)
| ~ aInteger0(W2)
| aElementOf0(W2,W1) )
& ( ( ~ aElementOf0(W2,W0)
& aInteger0(W2) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != stldt0(W0) ) )
| ~ aSubsetOf0(W0,cS1395) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f32_nnf]) ).
cnf(c102,plain,
( ~ aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| X1 != stldt0(X0)
| ~ aSubsetOf0(X0,cS1395) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
fof(f34,definition,
! [W0] :
( aSubsetOf0(W0,cS1395)
=> ( isOpen0(W0)
<=> ! [W1] :
( aElementOf0(W1,W0)
=> ? [W2] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0)
& W2 != sz00
& aInteger0(W2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mOpen) ).
fof(f34_nnf,plain,
! [W0] :
( ( ( ? [W1] :
( ! [W2] :
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0)
| W2 = sz00
| ~ aInteger0(W2) )
& aElementOf0(W1,W0) )
| isOpen0(W0) )
& ( ! [W1] :
( ? [W2] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,W2),W0)
& W2 != sz00
& aInteger0(W2) )
| ~ aElementOf0(W1,W0) )
| ~ isOpen0(W0) ) )
| ~ aSubsetOf0(W0,cS1395) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [W0,W1,W2] :
( ( ( ( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sk12(W0),W2),W0)
| W2 = sz00
| ~ aInteger0(W2) )
& aElementOf0(sk12(W0),W0) )
| isOpen0(W0) )
& ( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W1,sk11(W0,W1)),W0)
& sk11(W0,W1) != sz00
& aInteger0(sk11(W0,W1)) )
| ~ aElementOf0(W1,W0)
| ~ isOpen0(W0) ) )
| ~ aSubsetOf0(W0,cS1395) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11,sk12])],[f34_nnf]) ).
cnf(c121,plain,
( sk11(X0,X1) != sz00
| ~ aElementOf0(X1,X0)
| ~ isOpen0(X0)
| ~ aSubsetOf0(X0,cS1395) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f42,hypothesis,
( 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('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2079) ).
fof(f42_nnf,plain,
( stldt0(sbsmnsldt0(xS)) = cS2076
& ! [W0] :
( ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( W0 = smndt0(sz10)
| W0 = sz10
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& ! [W0] :
( ( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( ( ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS)) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [W0,W1] :
( stldt0(sbsmnsldt0(xS)) = cS2076
& ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( W0 = smndt0(sz10)
| W0 = sz10
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS)
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ( ( aElementOf0(W0,sk18(W0))
& aElementOf0(sk18(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18])],[f42_nnf]) ).
cnf(c167,plain,
( ~ aElementOf0(X0,sbsmnsldt0(xS))
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(c180,plain,
( ~ aElementOf0(X0,sbsmnsldt0(xS))
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(c195,plain,
~ isOpen0(stldt0(sbsmnsldt0(xS))),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c24,c36,c37,c102,c121,c137,c167,c180,c195,c196]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t330357]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM449+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 04:08:06 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 262.61/37.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 262.61/37.93 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------