%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM450+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Thu Sep 24 01:40:34 PM UTC 2026
% Result : Theorem 3.26s 0.97s
% Output : CNFRefutation 3.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 60 ( 15 unt; 5 def)
% Number of atoms : 660 ( 85 equ)
% Maximal formula atoms : 70 ( 11 avg)
% Number of connectives : 851 ( 251 ~; 205 |; 353 &)
% ( 22 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 6 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 4 con; 0-2 aty)
% Number of variables : 193 ( 147 !; 46 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f43,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') ).
fof(f45,hypothesis,
( ! [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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,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(negated_conjecture,[status(cth)],[f46]) ).
fof(f250,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)],[f43]) ).
fof(f251,plain,
( stldt0(sbsmnsldt0(xS)) = cS2076
& ! [W0] :
( ( W0 != smndt0(sz10)
& W0 != sz10 )
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( W0 = smndt0(sz10)
| W0 = sz10
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ 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)) )
& ! [W0] :
( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(miniscoping,[status(thm)],[f250]) ).
fof(f252,plain,
( stldt0(sbsmnsldt0(xS)) = cS2076
& ! [W0] :
( ( W0 != smndt0(sz10)
& W0 != sz10 )
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( W0 = smndt0(sz10)
| W0 = sz10
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ 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)) )
& ! [W0] :
( ( aElementOf0(W0,sK18_skl(W0))
& aElementOf0(sK18_skl(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(W1,sK18_skl(W0))],[f251]) ).
fof(f263,plain,
! [X0] :
( X0 != sz10
| aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f264,plain,
! [X0] :
( X0 != smndt0(sz10)
| aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f265,plain,
stldt0(sbsmnsldt0(xS)) = cS2076,
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f267,plain,
( ! [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,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] :
( ? [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,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)) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f268,plain,
( ! [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))
& 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)],[f267]) ).
fof(f269,plain,
( ! [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) )
& ! [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))) )
& ! [W0] :
( ( ~ 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)) )
& ! [W0] :
( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& 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) )
& ! [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))) )
& ! [W0] :
( ( ~ 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)) )
& ! [W0] :
( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(miniscoping,[status(thm)],[f268]) ).
fof(f270,plain,
( ! [W0] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)),stldt0(sbsmnsldt0(xS)))
& ! [W2] :
( aElementOf0(W2,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0))) )
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,sK23_skl(W0))
& ~ aDivisorOf0(sK23_skl(W0),sdtpldt0(W2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(sK23_skl(W0),W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,W0,sK23_skl(W0))
& aDivisorOf0(sK23_skl(W0),sdtpldt0(W2,smndt0(W0)))
& sdtasdt0(sK23_skl(W0),sK24_skl(W2,W0)) = sdtpldt0(W2,smndt0(W0))
& aInteger0(sK24_skl(W2,W0))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK23_skl(W0)))
& sK23_skl(W0) != sz00
& aInteger0(sK23_skl(W0)) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ 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)) )
& ! [W0] :
( ( aElementOf0(W0,sK22_skl(W0))
& aElementOf0(sK22_skl(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& isClosed0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)),stldt0(sbsmnsldt0(xS)))
& ! [W2] :
( aElementOf0(W2,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0))) )
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,sK20_skl(W0))
& ~ aDivisorOf0(sK20_skl(W0),sdtpldt0(W2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(sK20_skl(W0),W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,W0,sK20_skl(W0))
& aDivisorOf0(sK20_skl(W0),sdtpldt0(W2,smndt0(W0)))
& sdtasdt0(sK20_skl(W0),sK21_skl(W2,W0)) = sdtpldt0(W2,smndt0(W0))
& aInteger0(sK21_skl(W2,W0))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,sK20_skl(W0)))
& sK20_skl(W0) != sz00
& aInteger0(sK20_skl(W0)) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ 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)) )
& ! [W0] :
( ( aElementOf0(W0,sK19_skl(W0))
& aElementOf0(sK19_skl(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0)),skolemize(W3,sK21_skl(W2,W0)),skolemize(W1,sK22_skl(W0)),skolemize(W1,sK23_skl(W0)),skolemize(W3,sK24_skl(W2,W0))],[f269]) ).
fof(f279,plain,
! [X0] :
( aInteger0(sK20_skl(X0))
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f280,plain,
! [X0] :
( sK20_skl(X0) != sz00
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f291,plain,
! [X0] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,sK20_skl(X0)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f303,plain,
! [X0] :
( sK23_skl(X0) != sz00
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f315,plain,
! [W0] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))
& ? [W1] :
( ~ aElementOf0(W1,stldt0(sbsmnsldt0(xS)))
& aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
& ! [W1] :
( aElementOf0(W1,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W1,sbsmnsldt0(xS))
& aInteger0(W1) ) )
& ! [W1] :
( aElementOf0(W1,sbsmnsldt0(xS))
<=> ( ? [W2] :
( aElementOf0(W1,W2)
& aElementOf0(W2,xS) )
& aInteger0(W1) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W1] :
( ( 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) )
& ( ( 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)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
| W0 = sz00
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f316,plain,
! [W0] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))
& ? [W1] :
( ~ aElementOf0(W1,stldt0(sbsmnsldt0(xS)))
& aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
& ! [W1] :
( ( aElementOf0(W1,sbsmnsldt0(xS))
| ~ aInteger0(W1)
| aElementOf0(W1,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W1,sbsmnsldt0(xS))
& aInteger0(W1) )
| ~ aElementOf0(W1,stldt0(sbsmnsldt0(xS))) ) )
& ! [W1] :
( ( ! [W2] :
( ~ aElementOf0(W1,W2)
| ~ aElementOf0(W2,xS) )
| ~ aInteger0(W1)
| aElementOf0(W1,sbsmnsldt0(xS)) )
& ( ( ? [W2] :
( aElementOf0(W1,W2)
& aElementOf0(W2,xS) )
& aInteger0(W1) )
| ~ aElementOf0(W1,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W1] :
( ( 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) )
& ( ( 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)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
| W0 = sz00
| ~ aInteger0(W0) ),
inference(NNF_transformation,[status(thm)],[f315]) ).
fof(f317,plain,
! [W0] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))
& ? [W1] :
( ~ aElementOf0(W1,stldt0(sbsmnsldt0(xS)))
& aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
& ! [W1] :
( aElementOf0(W1,sbsmnsldt0(xS))
| ~ aInteger0(W1)
| aElementOf0(W1,stldt0(sbsmnsldt0(xS))) )
& ! [W1] :
( ( ~ aElementOf0(W1,sbsmnsldt0(xS))
& aInteger0(W1) )
| ~ aElementOf0(W1,stldt0(sbsmnsldt0(xS))) )
& ! [W1] :
( ! [W2] :
( ~ aElementOf0(W1,W2)
| ~ aElementOf0(W2,xS) )
| ~ aInteger0(W1)
| aElementOf0(W1,sbsmnsldt0(xS)) )
& ! [W1] :
( ( ? [W2] :
( aElementOf0(W1,W2)
& aElementOf0(W2,xS) )
& aInteger0(W1) )
| ~ aElementOf0(W1,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& ! [W1] :
( 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) )
& ! [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)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
| W0 = sz00
| ~ aInteger0(W0) ),
inference(miniscoping,[status(thm)],[f316]) ).
fof(f318,plain,
! [W0] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,W0),stldt0(sbsmnsldt0(xS)))
& ~ aElementOf0(sK27_skl(W0),stldt0(sbsmnsldt0(xS)))
& aElementOf0(sK27_skl(W0),szAzrzSzezqlpdtcmdtrp0(sz10,W0))
& ! [W1] :
( aElementOf0(W1,sbsmnsldt0(xS))
| ~ aInteger0(W1)
| aElementOf0(W1,stldt0(sbsmnsldt0(xS))) )
& ! [W1] :
( ( ~ aElementOf0(W1,sbsmnsldt0(xS))
& aInteger0(W1) )
| ~ aElementOf0(W1,stldt0(sbsmnsldt0(xS))) )
& ! [W1] :
( ! [W2] :
( ~ aElementOf0(W1,W2)
| ~ aElementOf0(W2,xS) )
| ~ aInteger0(W1)
| aElementOf0(W1,sbsmnsldt0(xS)) )
& ! [W1] :
( ( aElementOf0(W1,sK26_skl(W1,W0))
& aElementOf0(sK26_skl(W1,W0),xS)
& aInteger0(W1) )
| ~ aElementOf0(W1,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& ! [W1] :
( 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) )
& ! [W1] :
( ( sdteqdtlpzmzozddtrp0(W1,sz10,W0)
& aDivisorOf0(W0,sdtpldt0(W1,smndt0(sz10)))
& sdtasdt0(W0,sK25_skl(W1,W0)) = sdtpldt0(W1,smndt0(sz10))
& aInteger0(sK25_skl(W1,W0))
& aInteger0(W1) )
| ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,W0)) )
| W0 = sz00
| ~ aInteger0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl,sK27_skl]),skolemize(W2,sK25_skl(W1,W0)),skolemize(W2,sK26_skl(W1,W0)),skolemize(W1,sK27_skl(W0))],[f317]) ).
fof(f338,plain,
! [X0] :
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X0),stldt0(sbsmnsldt0(xS)))
| X0 = sz00
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f434,plain,
aElementOf0(sz10,stldt0(sbsmnsldt0(xS))),
inference(destructive_equality_resolution,[status(thm)],[f263]) ).
fof(f435,plain,
aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(xS))),
inference(destructive_equality_resolution,[status(thm)],[f264]) ).
fof(f803,plain,
aElementOf0(sz10,cS2076),
inference(forward_demodulation,[status(thm)],[f265,f434]) ).
fof(f1234,plain,
! [X0] :
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,X0),cS2076)
| X0 = sz00
| ~ aInteger0(X0) ),
inference(forward_demodulation,[status(thm)],[f265,f338]) ).
fof(f1235,plain,
aElementOf0(smndt0(sz10),cS2076),
inference(forward_demodulation,[status(thm)],[f265,f435]) ).
fof(f1599,plain,
! [X0] :
( aInteger0(sK20_skl(X0))
| ~ aElementOf0(X0,cS2076) ),
inference(forward_demodulation,[status(thm)],[f265,f279]) ).
fof(f1607,plain,
! [X0] :
( sK20_skl(X0) != sz00
| ~ aElementOf0(X0,cS2076) ),
inference(forward_demodulation,[status(thm)],[f265,f280]) ).
fof(f1850,plain,
sK20_skl(sz10) != sz00,
inference(resolution,[status(thm)],[f803,f1607]) ).
fof(f1851,plain,
aInteger0(sK20_skl(sz10)),
inference(resolution,[status(thm)],[f803,f1599]) ).
fof(f1859,plain,
! [X0] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,sK20_skl(X0)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X0,cS2076) ),
inference(forward_demodulation,[status(thm)],[f265,f291]) ).
fof(f1860,plain,
! [X0] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,sK20_skl(X0)),cS2076)
| ~ aElementOf0(X0,cS2076) ),
inference(forward_demodulation,[status(thm)],[f265,f1859]) ).
fof(f1925,plain,
sK20_skl(smndt0(sz10)) != sz00,
inference(resolution,[status(thm)],[f1235,f1607]) ).
fof(f1937,plain,
! [X0] :
( sK23_skl(X0) != sz00
| ~ aElementOf0(X0,cS2076) ),
inference(forward_demodulation,[status(thm)],[f265,f303]) ).
fof(f1938,plain,
sK23_skl(smndt0(sz10)) != sz00,
inference(resolution,[status(thm)],[f1937,f1235]) ).
fof(f2015,definition,
( sQ128_spl
<=> aInteger0(sK20_skl(sz10)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f2017,plain,
( sQ128_spl
| ~ aInteger0(sK20_skl(sz10)) ),
inference(component_clause,[status(thm)],[f2015]) ).
fof(f2018,definition,
( sQ129_spl
<=> sK20_skl(sz10) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2019,plain,
( ~ sQ129_spl
| sK20_skl(sz10) = sz00 ),
inference(component_clause,[status(thm)],[f2018]) ).
fof(f2024,definition,
( sQ131_spl
<=> aElementOf0(sz10,cS2076) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f2026,plain,
( sQ131_spl
| ~ aElementOf0(sz10,cS2076) ),
inference(component_clause,[status(thm)],[f2024]) ).
fof(f2037,plain,
( sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2026,f803]) ).
fof(f2038,plain,
sQ131_spl,
inference(contradiction_clause,[status(thm)],[f2037]) ).
fof(f2233,plain,
( ~ sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2019,f1850]) ).
fof(f2234,plain,
~ sQ129_spl,
inference(contradiction_clause,[status(thm)],[f2233]) ).
fof(f2237,plain,
( sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2017,f1851]) ).
fof(f2238,plain,
sQ128_spl,
inference(contradiction_clause,[status(thm)],[f2237]) ).
fof(f2276,definition,
( sQ159_spl
<=> sK20_skl(smndt0(sz10)) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f2277,plain,
( ~ sQ159_spl
| sK20_skl(smndt0(sz10)) = sz00 ),
inference(component_clause,[status(thm)],[f2276]) ).
fof(f2280,plain,
( ~ sQ159_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2277,f1925]) ).
fof(f2281,plain,
~ sQ159_spl,
inference(contradiction_clause,[status(thm)],[f2280]) ).
fof(f2309,definition,
( sQ161_spl
<=> sK23_skl(smndt0(sz10)) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f2310,plain,
( ~ sQ161_spl
| sK23_skl(smndt0(sz10)) = sz00 ),
inference(component_clause,[status(thm)],[f2309]) ).
fof(f2359,plain,
( ~ sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2310,f1938]) ).
fof(f2360,plain,
~ sQ161_spl,
inference(contradiction_clause,[status(thm)],[f2359]) ).
fof(f2710,plain,
( ~ aElementOf0(sz10,cS2076)
| sK20_skl(sz10) = sz00
| ~ aInteger0(sK20_skl(sz10)) ),
inference(resolution,[status(thm)],[f1234,f1860]) ).
fof(f2712,plain,
( ~ sQ131_spl
| sQ129_spl
| ~ sQ128_spl ),
inference(split_clause,[status(thm)],[f2710,f2015,f2018,f2024]) ).
fof(f2713,plain,
$false,
inference(sat_refutation,[status(thm)],[f2038,f2234,f2238,f2281,f2360,f2712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM450+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n014.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 02:30:20 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 3.26/0.97 % Refutation found
% 3.26/0.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.26/0.97 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.26/1.00 % Elapsed time: 0.535291 seconds
% 3.26/1.00 % CPU time: 3.800207 seconds
% 3.26/1.00 % Total memory used: 139.706 MB
% 3.26/1.00 % Net memory used: 136.411 MB
%------------------------------------------------------------------------------