%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM537+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:17:19 AM UTC 2026
% Result : Theorem 8.38s 1.80s
% Output : CNFRefutation 8.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 7
% Syntax : Number of formulae : 91 ( 18 unt; 0 def)
% Number of atoms : 926 ( 181 equ)
% Maximal formula atoms : 530 ( 10 avg)
% Number of connectives : 1319 ( 484 ~; 605 |; 200 &)
% ( 12 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 127 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 279 ( 0 sgn 208 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mDefCons,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtpldt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( ( W3 = W1
| aElementOf0(W3,W0) )
& aElement0(W3) ) )
& aSet0(W2) ) ) ),
file('theBenchmark.p',mDefCons) ).
fof(mDefDiff,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) ) ),
file('theBenchmark.p',mDefDiff) ).
fof(mConsDiff,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ),
file('theBenchmark.p',mConsDiff) ).
fof(m__679,axiom,
( aSet0(xS)
& aElement0(xx) ),
file('theBenchmark.p',m__679) ).
fof(m__,conjecture,
( ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xS,xx))
<=> ( ( W0 = xx
| aElementOf0(W0,xS) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))
<=> ( W0 != xx
& aElementOf0(W0,sdtpldt0(xS,xx))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) )
=> ( aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))
=> aElementOf0(W0,xS) ) ) ) )
& ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xS,xx))
<=> ( ( W0 = xx
| aElementOf0(W0,xS) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))
<=> ( W0 != xx
& aElementOf0(W0,sdtpldt0(xS,xx))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) )
=> ( aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))
| ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx)) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xS,xx))
<=> ( ( W0 = xx
| aElementOf0(W0,xS) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))
<=> ( W0 != xx
& aElementOf0(W0,sdtpldt0(xS,xx))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) )
=> ( aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))
=> aElementOf0(W0,xS) ) ) ) )
& ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(xS,xx))
<=> ( ( W0 = xx
| aElementOf0(W0,xS) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx))
<=> ( W0 != xx
& aElementOf0(W0,sdtpldt0(xS,xx))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) )
=> ( aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))
| ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx)) ) ) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_18,plain,
( ( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
& ? [W0] :
( ~ aElementOf0(W0,xS)
& aElementOf0(W0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [X4] :
( ( xx = X4
| ~ aElementOf0(X4,sdtpldt0(xS,xx))
| ~ aElement0(X4)
| aElementOf0(X4,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ( xx != X4
& aElementOf0(X4,sdtpldt0(xS,xx))
& aElement0(X4) )
| ~ aElementOf0(X4,sdtmndt0(sdtpldt0(xS,xx),xx)) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))
& ! [X3] :
( ( ( xx != X3
& ~ aElementOf0(X3,xS) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(xS,xx)) )
& ( ( ( xx = X3
| aElementOf0(X3,xS) )
& aElement0(X3) )
| ~ aElementOf0(X3,sdtpldt0(xS,xx)) ) )
& aSet0(sdtpldt0(xS,xx)) )
| ( ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))
& ? [X2] :
( ~ aElementOf0(X2,sdtmndt0(sdtpldt0(xS,xx),xx))
& aElementOf0(X2,xS) )
& ! [X1] :
( ( xx = X1
| ~ aElementOf0(X1,sdtpldt0(xS,xx))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ( xx != X1
& aElementOf0(X1,sdtpldt0(xS,xx))
& aElement0(X1) )
| ~ aElementOf0(X1,sdtmndt0(sdtpldt0(xS,xx),xx)) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))
& ! [X0] :
( ( ( xx != X0
& ~ aElementOf0(X0,xS) )
| ~ aElement0(X0)
| aElementOf0(X0,sdtpldt0(xS,xx)) )
& ( ( ( xx = X0
| aElementOf0(X0,xS) )
& aElement0(X0) )
| ~ aElementOf0(X0,sdtpldt0(xS,xx)) ) )
& aSet0(sdtpldt0(xS,xx)) ) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( ( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
& ~ aElementOf0(sK1,xS)
& aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
& ! [X4] :
( ( xx = X4
| ~ aElementOf0(X4,sdtpldt0(xS,xx))
| ~ aElement0(X4)
| aElementOf0(X4,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ( xx != X4
& aElementOf0(X4,sdtpldt0(xS,xx))
& aElement0(X4) )
| ~ aElementOf0(X4,sdtmndt0(sdtpldt0(xS,xx),xx)) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))
& ! [X3] :
( ( ( xx != X3
& ~ aElementOf0(X3,xS) )
| ~ aElement0(X3)
| aElementOf0(X3,sdtpldt0(xS,xx)) )
& ( ( ( xx = X3
| aElementOf0(X3,xS) )
& aElement0(X3) )
| ~ aElementOf0(X3,sdtpldt0(xS,xx)) ) )
& aSet0(sdtpldt0(xS,xx)) )
| ( ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))
& ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx))
& aElementOf0(sK0,xS)
& ! [X1] :
( ( xx = X1
| ~ aElementOf0(X1,sdtpldt0(xS,xx))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ( xx != X1
& aElementOf0(X1,sdtpldt0(xS,xx))
& aElement0(X1) )
| ~ aElementOf0(X1,sdtmndt0(sdtpldt0(xS,xx),xx)) ) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))
& ! [X0] :
( ( ( xx != X0
& ~ aElementOf0(X0,xS) )
| ~ aElement0(X0)
| aElementOf0(X0,sdtpldt0(xS,xx)) )
& ( ( ( xx = X0
| aElementOf0(X0,xS) )
& aElement0(X0) )
| ~ aElementOf0(X0,sdtpldt0(xS,xx)) ) )
& aSet0(sdtpldt0(xS,xx)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X2,sK0),skolemize(W0,sK1)],[nnf_18]) ).
fof(sk_m___neg,plain,
( ( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ~ aElementOf0(sK1,xS)
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ~ aElementOf0(sK1,xS)
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| aElementOf0(sK0,xS) )
& ( ~ aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) )
& ( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElementOf0(VAR_0,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(sdtpldt0(xS,xx),xx)) )
& aSet0(sdtmndt0(sdtpldt0(xS,xx),xx))
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,sdtpldt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(xS,xx)) )
& aSet0(sdtpldt0(xS,xx)) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_31,negated_conjecture,
( ~ aElementOf0(sK1,xS)
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_32,negated_conjecture,
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_42,negated_conjecture,
( ~ aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_43,negated_conjecture,
( aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(sK0,xS) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_55,negated_conjecture,
( xx = B
| ~ aElementOf0(B,sdtpldt0(xS,xx))
| ~ aElement0(B)
| aElementOf0(B,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_66,negated_conjecture,
( xx != B
| ~ aElementOf0(B,sdtmndt0(sdtpldt0(xS,xx),xx))
| xx != A
| ~ aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_76,negated_conjecture,
( aElementOf0(B,sdtpldt0(xS,xx))
| ~ aElementOf0(B,sdtmndt0(sdtpldt0(xS,xx),xx))
| aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_101,negated_conjecture,
( ~ aElementOf0(B,xS)
| ~ aElement0(B)
| aElementOf0(B,sdtpldt0(xS,xx))
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_107,negated_conjecture,
( xx = B
| aElementOf0(B,xS)
| ~ aElementOf0(B,sdtpldt0(xS,xx))
| xx = A
| aElementOf0(A,xS)
| ~ aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_113,negated_conjecture,
aSet0(sdtpldt0(xS,xx)),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
fof(m__679_02,axiom,
~ aElementOf0(xx,xS),
file('theBenchmark.p',m__679_02) ).
cnf(c_114,plain,
~ aElementOf0(xx,xS),
inference(clausify,[status(thm)],[m__679_02]) ).
cnf(c_115,plain,
aSet0(xS),
inference(clausify,[status(thm)],[m__679]) ).
cnf(c_116,plain,
aElement0(xx),
inference(clausify,[status(thm)],[m__679]) ).
cnf(c_117,plain,
( sdtpldt0(sdtmndt0(A,B),B) = A
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mConsDiff]) ).
cnf(c_123,plain,
( D != B
| ~ aElementOf0(D,C)
| sdtmndt0(A,B) != C
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_124,plain,
( aElementOf0(D,A)
| ~ aElementOf0(D,C)
| sdtmndt0(A,B) != C
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_126,plain,
( aSet0(C)
| sdtmndt0(A,B) != C
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefDiff]) ).
cnf(c_131,plain,
( D != B
| ~ aElement0(D)
| aElementOf0(D,C)
| sdtpldt0(A,B) != C
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefCons]) ).
cnf(c_133,plain,
( D = B
| aElementOf0(D,A)
| ~ aElementOf0(D,C)
| sdtpldt0(A,B) != C
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefCons]) ).
cnf(c_148,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_8785,plain,
( xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElement0(A)
| xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(factor,[status(thm)],[c_55]) ).
cnf(c_8786,plain,
( xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_8785]) ).
cnf(c_8787,plain,
( xx = A
| xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_8786]) ).
cnf(c_154,plain,
( xx = A
| ~ aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_8787]) ).
cnf(c_8788,plain,
( xx != A
| xx != A
| ~ aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(factor,[status(thm)],[c_66]) ).
cnf(c_155,plain,
( xx != A
| ~ aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_8788]) ).
cnf(c_8789,plain,
( aElementOf0(A,sdtpldt0(xS,xx))
| aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(factor,[status(thm)],[c_76]) ).
cnf(c_156,plain,
( aElementOf0(A,sdtpldt0(xS,xx))
| ~ aElementOf0(A,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_8789]) ).
cnf(c_8790,plain,
( ~ aElementOf0(A,xS)
| ~ aElement0(A)
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(factor,[status(thm)],[c_101]) ).
cnf(c_8791,plain,
( ~ aElementOf0(A,xS)
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(copy,[status(thm)],[c_8790]) ).
cnf(c_160,plain,
( ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(copy,[status(thm)],[c_8791]) ).
cnf(c_8792,plain,
( xx = A
| aElementOf0(A,xS)
| xx = A
| aElementOf0(A,xS)
| ~ aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(factor,[status(thm)],[c_107]) ).
cnf(c_8793,plain,
( xx = A
| xx = A
| aElementOf0(A,xS)
| ~ aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(copy,[status(thm)],[c_8792]) ).
cnf(c_161,plain,
( xx = A
| aElementOf0(A,xS)
| ~ aElementOf0(A,sdtpldt0(xS,xx)) ),
inference(copy,[status(thm)],[c_8793]) ).
cnf(c_173,plain,
( sdtpldt0(sdtmndt0(xS,A),A) = xS
| ~ aElementOf0(A,xS) ),
inference(resolve,[status(thm)],[c_117,c_115]) ).
cnf(c_8794,plain,
( C != xx
| ~ aElementOf0(C,B)
| sdtmndt0(A,xx) != B
| ~ aSet0(A) ),
inference(resolve,[status(thm)],[c_123,c_116]) ).
cnf(c_198,plain,
( xx != C
| ~ aElementOf0(C,B)
| sdtmndt0(A,xx) != B
| ~ aSet0(A) ),
inference(copy,[status(thm)],[c_8794]) ).
cnf(c_208,plain,
( aElementOf0(C,A)
| ~ aElementOf0(C,sdtmndt0(A,B))
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_124]) ).
cnf(c_222,plain,
( aSet0(sdtmndt0(A,B))
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_126]) ).
cnf(c_241,plain,
( xx != B
| aElementOf0(xx,C)
| sdtpldt0(A,B) != C
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(resolve,[status(thm)],[c_131,c_116]) ).
cnf(c_257,plain,
( C = B
| aElementOf0(C,A)
| ~ aElementOf0(C,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aSet0(A) ),
inference(xxres,[status(thm)],[c_133]) ).
cnf(c_319,plain,
( aElement0(A)
| ~ aElementOf0(A,xS) ),
inference(resolve,[status(thm)],[c_148,c_115]) ).
cnf(c_8795,negated_conjecture,
( aElementOf0(sK0,xS)
| xx != sK1 ),
inference(resolve,[status(thm)],[c_155,c_43]) ).
cnf(c_322,negated_conjecture,
( aElementOf0(sK0,xS)
| sK1 != xx ),
inference(copy,[status(thm)],[c_8795]) ).
cnf(c_324,plain,
( aElementOf0(sK0,xS)
| aElementOf0(sK1,sdtpldt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_156,c_43]) ).
cnf(c_1352,plain,
( xx != B
| ~ aElementOf0(B,A)
| sdtmndt0(sdtpldt0(xS,xx),xx) != A ),
inference(resolve,[status(thm)],[c_198,c_113]) ).
cnf(c_1637,plain,
( aSet0(sdtmndt0(xS,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_222,c_115]) ).
cnf(c_8796,plain,
( xx = sK1
| aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) ),
inference(resolve,[status(thm)],[c_324,c_161]) ).
cnf(c_5016,plain,
( sK1 = xx
| aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) ),
inference(copy,[status(thm)],[c_8796]) ).
cnf(c_8797,negated_conjecture,
( aElementOf0(sK0,xS)
| sK1 = xx
| aElementOf0(sK0,xS) ),
inference(resolve,[status(thm)],[c_5016,c_42]) ).
cnf(c_5117,negated_conjecture,
( sK1 = xx
| aElementOf0(sK0,xS) ),
inference(copy,[status(thm)],[c_8797]) ).
cnf(c_8798,plain,
( aElementOf0(sK0,xS)
| aElementOf0(sK0,xS) ),
inference(resolve,[status(thm)],[c_5117,c_322]) ).
cnf(c_5168,plain,
aElementOf0(sK0,xS),
inference(copy,[status(thm)],[c_8798]) ).
cnf(c_5205,plain,
aElement0(sK0),
inference(resolve,[status(thm)],[c_5168,c_319]) ).
cnf(c_5216,plain,
sdtpldt0(sdtmndt0(xS,sK0),sK0) = xS,
inference(resolve,[status(thm)],[c_5168,c_173]) ).
cnf(c_8799,plain,
( ~ aElement0(sK0)
| aElementOf0(sK0,sdtpldt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_5168,c_160]) ).
cnf(c_5217,plain,
aElementOf0(sK0,sdtpldt0(xS,xx)),
inference(resolve,[status(thm)],[c_5205,c_8799]) ).
cnf(c_5397,plain,
aSet0(sdtmndt0(xS,sK0)),
inference(resolve,[status(thm)],[c_5205,c_1637]) ).
cnf(c_8800,plain,
( xx = sK0
| ~ aElementOf0(sK0,sdtpldt0(xS,xx))
| aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(resolve,[status(thm)],[c_5205,c_154]) ).
cnf(c_8801,plain,
( sK0 = xx
| ~ aElementOf0(sK0,sdtpldt0(xS,xx))
| aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_8800]) ).
cnf(c_5459,plain,
( sK0 = xx
| aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)) ),
inference(resolve,[status(thm)],[c_5217,c_8801]) ).
cnf(c_8802,plain,
( xx != sK0
| aElementOf0(xx,xS)
| ~ aElement0(sK0)
| ~ aSet0(sdtmndt0(xS,sK0)) ),
inference(resolve,[status(thm)],[c_5216,c_241]) ).
cnf(c_8803,plain,
( sK0 != xx
| aElementOf0(xx,xS)
| ~ aElement0(sK0)
| ~ aSet0(sdtmndt0(xS,sK0)) ),
inference(copy,[status(thm)],[c_8802]) ).
cnf(c_8804,plain,
( sK0 != xx
| aElementOf0(xx,xS)
| ~ aElement0(sK0) ),
inference(resolve,[status(thm)],[c_5397,c_8803]) ).
cnf(c_8805,plain,
( sK0 != xx
| aElementOf0(xx,xS) ),
inference(resolve,[status(thm)],[c_5205,c_8804]) ).
cnf(c_7180,plain,
sK0 != xx,
inference(resolve,[status(thm)],[c_114,c_8805]) ).
cnf(c_7200,plain,
aElementOf0(sK0,sdtmndt0(sdtpldt0(xS,xx),xx)),
inference(resolve,[status(thm)],[c_7180,c_5459]) ).
cnf(c_7204,negated_conjecture,
aElementOf0(sK1,sdtmndt0(sdtpldt0(xS,xx),xx)),
inference(resolve,[status(thm)],[c_7200,c_32]) ).
cnf(c_7205,negated_conjecture,
~ aElementOf0(sK1,xS),
inference(resolve,[status(thm)],[c_7200,c_31]) ).
cnf(c_8806,negated_conjecture,
( xx != sK1
| sdtmndt0(sdtpldt0(xS,xx),xx) != sdtmndt0(sdtpldt0(xS,xx),xx) ),
inference(resolve,[status(thm)],[c_7204,c_1352]) ).
cnf(c_8807,negated_conjecture,
( sK1 != xx
| sdtmndt0(sdtpldt0(xS,xx),xx) != sdtmndt0(sdtpldt0(xS,xx),xx) ),
inference(copy,[status(thm)],[c_8806]) ).
cnf(c_8234,negated_conjecture,
sK1 != xx,
inference(copy,[status(thm)],[c_8807]) ).
cnf(c_8808,negated_conjecture,
( aElementOf0(sK1,sdtpldt0(xS,xx))
| ~ aElement0(xx)
| ~ aSet0(sdtpldt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_7204,c_208]) ).
cnf(c_8809,negated_conjecture,
( aElementOf0(sK1,sdtpldt0(xS,xx))
| ~ aElement0(xx) ),
inference(resolve,[status(thm)],[c_113,c_8808]) ).
cnf(c_8243,negated_conjecture,
aElementOf0(sK1,sdtpldt0(xS,xx)),
inference(resolve,[status(thm)],[c_116,c_8809]) ).
cnf(c_8810,plain,
( sK1 = xx
| aElementOf0(sK1,xS)
| ~ aElement0(xx)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_8243,c_257]) ).
cnf(c_8811,plain,
( sK1 = xx
| aElementOf0(sK1,xS)
| ~ aElement0(xx) ),
inference(resolve,[status(thm)],[c_115,c_8810]) ).
cnf(c_8812,plain,
( sK1 = xx
| aElementOf0(sK1,xS) ),
inference(resolve,[status(thm)],[c_116,c_8811]) ).
cnf(c_8813,negated_conjecture,
sK1 = xx,
inference(resolve,[status(thm)],[c_7205,c_8812]) ).
cnf(c_8784,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_8234,c_8813]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM537+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 03:07:08 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2658938 was started by sandbox2 on n007,
% 0.13/0.36 % Sat Sep 26 03:07:08 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.39
% 0.13/0.39 % From the command line: assign(max_seconds, 300).
% 8.38/1.80
% 8.38/1.80 % given #500 (A,wt=15): 272 -aSet0(A) | -aSet0(B) | -aSubsetOf0(xS,A) | -aSubsetOf0(A,B) | aSubsetOf0(xS,B). [resolve(136,a,115,a)].
% 8.38/1.80
% 8.38/1.80 % SZS status Theorem for theBenchmark
% 8.38/1.80
% 8.38/1.80 % Proof 1 at 1.05 (+ 0.29) seconds.
% 8.38/1.80 % Length of proof is 57.
% 8.38/1.80 % Level of proof is 13.
% 8.38/1.80 % Maximum clause weight is 40.000.
% 8.38/1.80 % Given clauses 572.
% 8.38/1.80
% 8.38/1.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------