%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM441+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 : n005.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:02 PM UTC 2026
% Result : Theorem 64.05s 8.52s
% Output : Proof 64.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 78 ( 37 unt; 3 def)
% Number of atoms : 735 ( 100 equ)
% Maximal formula atoms : 74 ( 9 avg)
% Number of connectives : 937 ( 280 ~; 237 |; 366 &)
% ( 22 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 7 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 8 con; 0-4 aty)
% Number of variables : 167 ( 2 sgn 107 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f37,axiom,
! [W0,W1] :
( ( isOpen0(W1)
& isOpen0(W0)
& aSubsetOf0(W1,cS1395)
& aSubsetOf0(W0,cS1395) )
=> isOpen0(sdtslmnbsdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mInterOpen) ).
fof(f37_nnf,plain,
! [W0,W1] :
( isOpen0(sdtslmnbsdt0(W0,W1))
| ~ isOpen0(W1)
| ~ isOpen0(W0)
| ~ aSubsetOf0(W1,cS1395)
| ~ aSubsetOf0(W0,cS1395) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [W0,W1] :
( isOpen0(sdtslmnbsdt0(W0,W1))
| ~ isOpen0(W1)
| ~ isOpen0(W0)
| ~ aSubsetOf0(W1,cS1395)
| ~ aSubsetOf0(W0,cS1395) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c129,plain,
( isOpen0(sdtslmnbsdt0(X0,X1))
| ~ isOpen0(X1)
| ~ isOpen0(X0)
| ~ aSubsetOf0(X1,cS1395)
| ~ aSubsetOf0(X0,cS1395) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(t195,plain,
ifeq(aSubsetOf0(X1,cS1395),true,ifeq(aSubsetOf0(X2,cS1395),true,ifeq(isOpen0(X1),true,ifeq(isOpen0(X2),true,isOpen0(sdtslmnbsdt0(X1,X2)),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c129]) ).
cnf(t505,plain,
ifeq(aSubsetOf0(X1,cS1395),true,ifeq(aSubsetOf0(X2,cS1395),true,ifeq(isOpen0(X1),true,ifeq(isOpen0(X2),true,isOpen0(sdtslmnbsdt0(X1,X2)),true),true),true),true) = true,
inference(orient,[status(thm)],[t195]) ).
fof(f39,hypothesis,
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aElementOf0(W0,stldt0(xB))
& aElementOf0(W0,stldt0(xA))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
<=> ( ~ aElementOf0(W0,xB)
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
<=> ( ~ aElementOf0(W0,xA)
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [W0] :
( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
<=> ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
=> aElementOf0(W0,cS1395) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
<=> ( ~ aElementOf0(W0,xB)
& aInteger0(W0) ) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
=> aElementOf0(W0,cS1395) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
<=> ( ~ aElementOf0(W0,xA)
& aInteger0(W0) ) )
& aSet0(stldt0(xA)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1883) ).
fof(f39_nnf,plain,
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [W0] :
( ( ~ aElementOf0(W0,stldt0(xB))
| ~ aElementOf0(W0,stldt0(xA))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ( aElementOf0(W0,stldt0(xB))
& aElementOf0(W0,stldt0(xA))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ! [W0] :
( ( aElementOf0(W0,xB)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xB)) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) ) )
& ! [W0] :
( ( aElementOf0(W0,xA)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xA)) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) ) )
& ! [W0] :
( ( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [W0] :
( ( ( ~ aElementOf0(W0,xB)
& ~ aElementOf0(W0,xA) )
| ~ aInteger0(W0)
| aElementOf0(W0,sdtbsmnsldt0(xA,xB)) )
& ( ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,stldt0(xB)) )
& ! [W0] :
( ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,xB)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xB)) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) ) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,stldt0(xA)) )
& ! [W0] :
( ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,xA)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xA)) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) ) )
& aSet0(stldt0(xA)) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [W0] :
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ( ~ aElementOf0(W0,stldt0(xB))
| ~ aElementOf0(W0,stldt0(xA))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ( aElementOf0(W0,stldt0(xB))
& aElementOf0(W0,stldt0(xA))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( aElementOf0(W0,xB)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xB)) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) )
& ( aElementOf0(W0,xA)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xA)) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) )
& ( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ( ( ~ aElementOf0(W0,xB)
& ~ aElementOf0(W0,xA) )
| ~ aInteger0(W0)
| aElementOf0(W0,sdtbsmnsldt0(xA,xB)) )
& ( ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,stldt0(xB)) )
& ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) )
& aSet0(cS1395)
& ( aElementOf0(W0,xB)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xB)) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,stldt0(xA)) )
& ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) )
& aSet0(cS1395)
& ( aElementOf0(W0,xA)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xA)) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) )
& aSet0(stldt0(xA)) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c217,plain,
stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t60,plain,
sdtslmnbsdt0(stldt0(xA),stldt0(xB)) = stldt0(sdtbsmnsldt0(xA,xB)),
inference(equality_encoding,[status(esa)],[c217]) ).
cnf(t1828,plain,
sdtslmnbsdt0(stldt0(xA),stldt0(xB)) = stldt0(sdtbsmnsldt0(xA,xB)),
inference(orient,[status(thm)],[t60]) ).
cnf(t1833,plain,
true = ifeq(aSubsetOf0(stldt0(xA),cS1395),true,ifeq(aSubsetOf0(stldt0(xB),cS1395),true,ifeq(isOpen0(stldt0(xA)),true,ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),true),true),true),
inference(cp,[status(thm)],[t505,t1828]) ).
cnf(c188,plain,
aSubsetOf0(stldt0(xA),cS1395),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t33,plain,
aSubsetOf0(stldt0(xA),cS1395) = true,
inference(equality_encoding,[status(esa)],[c188]) ).
cnf(t1436,plain,
aSubsetOf0(stldt0(xA),cS1395) = true,
inference(orient,[status(thm)],[t33]) ).
cnf(t4687,plain,
true = ifeq(true,true,ifeq(aSubsetOf0(stldt0(xB),cS1395),true,ifeq(isOpen0(stldt0(xA)),true,ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),true),true),true),
inference(step,[status(thm)],[t1833,t1436]) ).
cnf(t39,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t39]) ).
cnf(t4688,plain,
true = ifeq(aSubsetOf0(stldt0(xB),cS1395),true,ifeq(isOpen0(stldt0(xA)),true,ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),true),true),
inference(step,[status(thm)],[t4687,t256]) ).
cnf(c197,plain,
aSubsetOf0(stldt0(xB),cS1395),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t34,plain,
aSubsetOf0(stldt0(xB),cS1395) = true,
inference(equality_encoding,[status(esa)],[c197]) ).
cnf(t1386,plain,
aSubsetOf0(stldt0(xB),cS1395) = true,
inference(orient,[status(thm)],[t34]) ).
cnf(t4689,plain,
true = ifeq(true,true,ifeq(isOpen0(stldt0(xA)),true,ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),true),true),
inference(step,[status(thm)],[t4688,t1386]) ).
cnf(t4690,plain,
true = ifeq(isOpen0(stldt0(xA)),true,ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),true),
inference(step,[status(thm)],[t4689,t256]) ).
fof(f38,hypothesis,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
=> ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(xB)) )
& ! [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(xB))
<=> ( ~ aElementOf0(W0,xB)
& aInteger0(W0) ) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
=> ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(xA)) )
& ! [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(xA))
<=> ( ~ aElementOf0(W0,xA)
& aInteger0(W0) ) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [W0] :
( aElementOf0(W0,xB)
=> aElementOf0(W0,cS1395) )
& aSet0(xB)
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [W0] :
( aElementOf0(W0,xA)
=> aElementOf0(W0,cS1395) )
& aSet0(xA)
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1826) ).
fof(f38_nnf,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [W0] :
( ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB))
& ! [W2] :
( aElementOf0(W2,stldt0(xB))
| ~ 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(xB)) )
& ! [W0] :
( ( aElementOf0(W0,xB)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xB)) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) ) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [W0] :
( ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA))
& ! [W2] :
( aElementOf0(W2,stldt0(xA))
| ~ 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(xA)) )
& ! [W0] :
( ( aElementOf0(W0,xA)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xA)) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) ) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,xB) )
& aSet0(xB)
& ! [W0] :
( ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,xA) )
& aSet0(xA)
& ! [W0] :
( ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [W0,W2,W3] :
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sk16(W0)),stldt0(xB))
& ( aElementOf0(W2,stldt0(xB))
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sk16(W0))) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sk16(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,sk16(W0))
& ~ aDivisorOf0(sk16(W0),sdtpldt0(W2,smndt0(W0)))
& ( sdtasdt0(sk16(W0),W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,W0,sk16(W0))
& aDivisorOf0(sk16(W0),sdtpldt0(W2,smndt0(W0)))
& sdtasdt0(sk16(W0),sk17(W0,W2)) = sdtpldt0(W2,smndt0(W0))
& aInteger0(sk17(W0,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sk16(W0))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sk16(W0)))
& sk16(W0) != sz00
& aInteger0(sk16(W0)) )
| ~ aElementOf0(W0,stldt0(xB)) )
& ( aElementOf0(W0,xB)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xB)) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sk14(W0)),stldt0(xA))
& ( aElementOf0(W2,stldt0(xA))
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sk14(W0))) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sk14(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,sk14(W0))
& ~ aDivisorOf0(sk14(W0),sdtpldt0(W2,smndt0(W0)))
& ( sdtasdt0(sk14(W0),W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,W0,sk14(W0))
& aDivisorOf0(sk14(W0),sdtpldt0(W2,smndt0(W0)))
& sdtasdt0(sk14(W0),sk15(W0,W2)) = sdtpldt0(W2,smndt0(W0))
& aInteger0(sk15(W0,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sk14(W0))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sk14(W0)))
& sk14(W0) != sz00
& aInteger0(sk14(W0)) )
| ~ aElementOf0(W0,stldt0(xA)) )
& ( aElementOf0(W0,xA)
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(xA)) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,xB) )
& aSet0(xB)
& ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,xA) )
& aSet0(xA)
& ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) )
& aSet0(cS1395) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14,sk15,sk16,sk17])],[f38_nnf]) ).
cnf(c159,plain,
isOpen0(stldt0(xA)),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t20,plain,
isOpen0(stldt0(xA)) = true,
inference(equality_encoding,[status(esa)],[c159]) ).
cnf(t1654,plain,
isOpen0(stldt0(xA)) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t4691,plain,
true = ifeq(true,true,ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),true),
inference(step,[status(thm)],[t4690,t1654]) ).
cnf(t4692,plain,
true = ifeq(isOpen0(stldt0(xB)),true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),
inference(step,[status(thm)],[t4691,t256]) ).
cnf(c178,plain,
isOpen0(stldt0(xB)),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t21,plain,
isOpen0(stldt0(xB)) = true,
inference(equality_encoding,[status(esa)],[c178]) ).
cnf(t1644,plain,
isOpen0(stldt0(xB)) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(t4693,plain,
true = ifeq(true,true,isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),true),
inference(step,[status(thm)],[t4692,t1644]) ).
cnf(t4694,plain,
true = isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),
inference(step,[status(thm)],[t4693,t256]) ).
fof(f40,conjecture,
( ( ! [W0] :
( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
<=> ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) )
=> ( isClosed0(sdtbsmnsldt0(xA,xB))
| ( ( ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB))) )
=> ( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [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(sdtbsmnsldt0(xA,xB)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f40_neg,negated_conjecture,
~ ( ( ! [W0] :
( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
<=> ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) )
=> ( isClosed0(sdtbsmnsldt0(xA,xB))
| ( ( ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB))) )
=> ( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [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(sdtbsmnsldt0(xA,xB)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f40_nnf,plain,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB)))
& 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(sdtbsmnsldt0(xA,xB))) )
& ! [W0] :
( ( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [W0] :
( ( ( ~ aElementOf0(W0,xB)
& ~ aElementOf0(W0,xA) )
| ~ aInteger0(W0)
| aElementOf0(W0,sdtbsmnsldt0(xA,xB)) )
& ( ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(nnf_transformation,[status(thm)],[f40_neg]) ).
fof(f40_sk,plain,
! [W0,W1,W2,W3] :
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sk18,W1),stldt0(sdtbsmnsldt0(xA,xB)))
& ~ aElementOf0(sk20(W1),stldt0(sdtbsmnsldt0(xA,xB)))
& aElementOf0(sk20(W1),szAzrzSzezqlpdtcmdtrp0(sk18,W1))
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sk18,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sk18,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sk18)))
& ( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sk18))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sk18,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sk18)))
& sdtasdt0(W1,sk19(W1,W2)) = sdtpldt0(W2,smndt0(sk18))
& aInteger0(sk19(W1,W2))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sk18,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sk18,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(sk18,stldt0(sdtbsmnsldt0(xA,xB)))
& ( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ( ( ~ aElementOf0(W0,xB)
& ~ aElementOf0(W0,xA) )
| ~ aInteger0(W0)
| aElementOf0(W0,sdtbsmnsldt0(xA,xB)) )
& ( ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18,sk19,sk20])],[f40_nnf]) ).
cnf(c240,plain,
~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t40,plain,
isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) = false,
inference(equality_encoding,[status(esa)],[c240]) ).
cnf(t1999,plain,
isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) = false,
inference(orient,[status(thm)],[t40]) ).
cnf(t4695,plain,
true = false,
inference(step,[status(thm)],[t4694,t1999]) ).
cnf(t4595,plain,
false = true,
inference(orient,[status(thm)],[t4695]) ).
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]) ).
cnf(c144,plain,
( ~ aElementOf0(X0,xA)
| ~ aElementOf0(X0,stldt0(xA)) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c147,plain,
( sk14(X0) != sz00
| ~ aElementOf0(X0,stldt0(xA)) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c163,plain,
( ~ aElementOf0(X0,xB)
| ~ aElementOf0(X0,stldt0(xB)) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c166,plain,
( sk16(X0) != sz00
| ~ aElementOf0(X0,stldt0(xB)) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c182,plain,
( ~ aElementOf0(X0,xA)
| ~ aElementOf0(X0,stldt0(xA)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(c191,plain,
( ~ aElementOf0(X0,xB)
| ~ aElementOf0(X0,stldt0(xB)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(c205,plain,
( ~ aElementOf0(X0,sdtbsmnsldt0(xA,xB))
| ~ aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(c208,plain,
( ~ aElementOf0(X0,xA)
| ~ aElementOf0(X0,stldt0(xA)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(c211,plain,
( ~ aElementOf0(X0,xB)
| ~ aElementOf0(X0,stldt0(xB)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(c225,plain,
( ~ aElementOf0(X0,sdtbsmnsldt0(xA,xB))
| ~ aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(c241,plain,
~ isClosed0(sdtbsmnsldt0(xA,xB)),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c24,c36,c37,c102,c121,c144,c147,c163,c166,c182,c191,c205,c208,c211,c225,c240,c241]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4595]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM441+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 03:59:47 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 64.05/8.52 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.05/8.52 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------