%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM535+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 55.03s 9.52s
% Output : CNFRefutation 55.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 4
% Syntax : Number of formulae : 62 ( 12 unt; 0 def)
% Number of atoms : 831 ( 148 equ)
% Maximal formula atoms : 530 ( 13 avg)
% Number of connectives : 1188 ( 419 ~; 555 |; 192 &)
% ( 8 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 126 ( 6 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 : 227 ( 0 sgn 198 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(m__,conjecture,
( ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(xS,xx))
<=> ( W0 != xx
& aElementOf0(W0,xS)
& aElement0(W0) ) )
& aSet0(sdtmndt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))
<=> ( ( W0 = xx
| aElementOf0(W0,sdtmndt0(xS,xx)) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) )
=> ( aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| ! [W0] :
( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))
=> aElementOf0(W0,xS) ) ) ) )
& ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(xS,xx))
<=> ( W0 != xx
& aElementOf0(W0,xS)
& aElement0(W0) ) )
& aSet0(sdtmndt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))
<=> ( ( W0 = xx
| aElementOf0(W0,sdtmndt0(xS,xx)) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) )
=> ( aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))
| ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx)) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(xS,xx))
<=> ( W0 != xx
& aElementOf0(W0,xS)
& aElement0(W0) ) )
& aSet0(sdtmndt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))
<=> ( ( W0 = xx
| aElementOf0(W0,sdtmndt0(xS,xx)) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) )
=> ( aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| ! [W0] :
( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))
=> aElementOf0(W0,xS) ) ) ) )
& ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(xS,xx))
<=> ( W0 != xx
& aElementOf0(W0,xS)
& aElement0(W0) ) )
& aSet0(sdtmndt0(xS,xx)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))
<=> ( ( W0 = xx
| aElementOf0(W0,sdtmndt0(xS,xx)) )
& aElement0(W0) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) )
=> ( aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))
| ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx)) ) ) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_16,plain,
( ( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
& ? [W0] :
( ~ aElementOf0(W0,xS)
& aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [X4] :
( ( ( xx != X4
& ~ aElementOf0(X4,sdtmndt0(xS,xx)) )
| ~ aElement0(X4)
| aElementOf0(X4,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ( ( xx = X4
| aElementOf0(X4,sdtmndt0(xS,xx)) )
& aElement0(X4) )
| ~ aElementOf0(X4,sdtpldt0(sdtmndt0(xS,xx),xx)) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))
& ! [X3] :
( ( xx = X3
| ~ aElementOf0(X3,xS)
| ~ aElement0(X3)
| aElementOf0(X3,sdtmndt0(xS,xx)) )
& ( ( xx != X3
& aElementOf0(X3,xS)
& aElement0(X3) )
| ~ aElementOf0(X3,sdtmndt0(xS,xx)) ) )
& aSet0(sdtmndt0(xS,xx)) )
| ( ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))
& ? [X2] :
( ~ aElementOf0(X2,sdtpldt0(sdtmndt0(xS,xx),xx))
& aElementOf0(X2,xS) )
& ! [X1] :
( ( ( xx != X1
& ~ aElementOf0(X1,sdtmndt0(xS,xx)) )
| ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ( ( xx = X1
| aElementOf0(X1,sdtmndt0(xS,xx)) )
& aElement0(X1) )
| ~ aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))
& ! [X0] :
( ( xx = X0
| ~ aElementOf0(X0,xS)
| ~ aElement0(X0)
| aElementOf0(X0,sdtmndt0(xS,xx)) )
& ( ( xx != X0
& aElementOf0(X0,xS)
& aElement0(X0) )
| ~ aElementOf0(X0,sdtmndt0(xS,xx)) ) )
& aSet0(sdtmndt0(xS,xx)) ) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( ( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
& ~ aElementOf0(sK1,xS)
& aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
& ! [X4] :
( ( ( xx != X4
& ~ aElementOf0(X4,sdtmndt0(xS,xx)) )
| ~ aElement0(X4)
| aElementOf0(X4,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ( ( xx = X4
| aElementOf0(X4,sdtmndt0(xS,xx)) )
& aElement0(X4) )
| ~ aElementOf0(X4,sdtpldt0(sdtmndt0(xS,xx),xx)) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))
& ! [X3] :
( ( xx = X3
| ~ aElementOf0(X3,xS)
| ~ aElement0(X3)
| aElementOf0(X3,sdtmndt0(xS,xx)) )
& ( ( xx != X3
& aElementOf0(X3,xS)
& aElement0(X3) )
| ~ aElementOf0(X3,sdtmndt0(xS,xx)) ) )
& aSet0(sdtmndt0(xS,xx)) )
| ( ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))
& ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx))
& aElementOf0(sK0,xS)
& ! [X1] :
( ( ( xx != X1
& ~ aElementOf0(X1,sdtmndt0(xS,xx)) )
| ~ aElement0(X1)
| aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ( ( xx = X1
| aElementOf0(X1,sdtmndt0(xS,xx)) )
& aElement0(X1) )
| ~ aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) ) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))
& ! [X0] :
( ( xx = X0
| ~ aElementOf0(X0,xS)
| ~ aElement0(X0)
| aElementOf0(X0,sdtmndt0(xS,xx)) )
& ( ( xx != X0
& aElementOf0(X0,xS)
& aElement0(X0) )
| ~ aElementOf0(X0,sdtmndt0(xS,xx)) ) )
& aSet0(sdtmndt0(xS,xx)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X2,sK0),skolemize(W0,sK1)],[nnf_16]) ).
fof(sk_m___neg,plain,
( ( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ~ aElementOf0(sK1,xS)
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ~ aElementOf0(sK1,xS)
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| aElementOf0(sK0,xS) )
& ( ~ aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) )
& ( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| aElementOf0(sK0,xS) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| aElementOf0(VAR_0,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtpldt0(sdtmndt0(xS,xx),xx)) )
& aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx = VAR_0
| ~ aElementOf0(VAR_0,xS)
| ~ aElement0(VAR_0)
| aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| xx != VAR_0
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElementOf0(VAR_0,xS)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( ~ aElementOf0(sK1,xS)
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0] :
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx = VAR_1
| ~ aElementOf0(VAR_1,xS)
| ~ aElement0(VAR_1)
| aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( xx != VAR_1
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElementOf0(VAR_1,xS)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& ! [VAR_0,VAR_1] :
( aElement0(VAR_1)
| ~ aElementOf0(VAR_1,sdtmndt0(xS,xx))
| aElement0(VAR_0)
| ~ aElementOf0(VAR_0,sdtmndt0(xS,xx)) )
& aSet0(sdtmndt0(xS,xx)) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_29,negated_conjecture,
( ~ aElementOf0(sK1,xS)
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_30,negated_conjecture,
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_40,negated_conjecture,
( ~ aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_41,negated_conjecture,
( aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,xS) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_53,negated_conjecture,
( xx != B
| ~ aElement0(B)
| aElementOf0(B,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx != A
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_64,negated_conjecture,
( ~ aElementOf0(B,sdtmndt0(xS,xx))
| ~ aElement0(B)
| aElementOf0(B,sdtpldt0(sdtmndt0(xS,xx),xx))
| ~ aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_74,negated_conjecture,
( xx = B
| aElementOf0(B,sdtmndt0(xS,xx))
| ~ aElementOf0(B,sdtpldt0(sdtmndt0(xS,xx),xx))
| xx = A
| aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_92,negated_conjecture,
( xx = B
| ~ aElementOf0(B,xS)
| ~ aElement0(B)
| aElementOf0(B,sdtmndt0(xS,xx))
| xx = A
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_105,negated_conjecture,
( aElementOf0(B,xS)
| ~ aElementOf0(B,sdtmndt0(xS,xx))
| aElementOf0(A,xS)
| ~ aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
fof(m__617_02,axiom,
aElementOf0(xx,xS),
file('theBenchmark.p',m__617_02) ).
cnf(c_112,plain,
aElementOf0(xx,xS),
inference(clausify,[status(thm)],[m__617_02]) ).
fof(m__617,axiom,
aSet0(xS),
file('theBenchmark.p',m__617) ).
cnf(c_113,plain,
aSet0(xS),
inference(clausify,[status(thm)],[m__617]) ).
cnf(c_144,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_5220,plain,
( xx != A
| ~ aElement0(A)
| xx != A
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(factor,[status(thm)],[c_53]) ).
cnf(c_5221,plain,
( xx != A
| xx != A
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5220]) ).
cnf(c_149,plain,
( xx != A
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5221]) ).
cnf(c_5222,plain,
( ~ aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElement0(A)
| ~ aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(factor,[status(thm)],[c_64]) ).
cnf(c_5223,plain,
( ~ aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5222]) ).
cnf(c_151,plain,
( ~ aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElement0(A)
| aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5223]) ).
cnf(c_5224,plain,
( xx = A
| aElementOf0(A,sdtmndt0(xS,xx))
| xx = A
| aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(factor,[status(thm)],[c_74]) ).
cnf(c_5225,plain,
( xx = A
| xx = A
| aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5224]) ).
cnf(c_152,plain,
( xx = A
| aElementOf0(A,sdtmndt0(xS,xx))
| ~ aElementOf0(A,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5225]) ).
cnf(c_5226,plain,
( xx = A
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| xx = A
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(factor,[status(thm)],[c_92]) ).
cnf(c_5227,plain,
( xx = A
| ~ aElementOf0(A,xS)
| xx = A
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5226]) ).
cnf(c_5228,plain,
( xx = A
| xx = A
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5227]) ).
cnf(c_155,plain,
( xx = A
| ~ aElementOf0(A,xS)
| ~ aElement0(A)
| aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5228]) ).
cnf(c_5229,plain,
( aElementOf0(A,xS)
| aElementOf0(A,xS)
| ~ aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(factor,[status(thm)],[c_105]) ).
cnf(c_157,plain,
( aElementOf0(A,xS)
| ~ aElementOf0(A,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5229]) ).
cnf(c_5230,negated_conjecture,
( aElementOf0(sK0,xS)
| xx = sK1
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_152,c_41]) ).
cnf(c_247,negated_conjecture,
( aElementOf0(sK0,xS)
| sK1 = xx
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5230]) ).
cnf(c_5231,plain,
( ~ aElementOf0(xx,xS)
| aElementOf0(sK0,xS)
| aElementOf0(sK0,xS)
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(paramod,[status(thm)],[c_247,c_40]) ).
cnf(c_5232,plain,
( ~ aElementOf0(xx,xS)
| aElementOf0(sK0,xS)
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5231]) ).
cnf(c_2340,plain,
( aElementOf0(sK0,xS)
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_112,c_5232]) ).
cnf(c_2369,plain,
( aElementOf0(sK1,xS)
| aElementOf0(sK0,xS) ),
inference(resolve,[status(thm)],[c_2340,c_157]) ).
cnf(c_5233,negated_conjecture,
( aElementOf0(sK0,xS)
| aElementOf0(sK0,xS) ),
inference(resolve,[status(thm)],[c_2369,c_40]) ).
cnf(c_2397,negated_conjecture,
aElementOf0(sK0,xS),
inference(copy,[status(thm)],[c_5233]) ).
cnf(c_5234,plain,
( xx = sK0
| ~ aElement0(sK0)
| aElementOf0(sK0,sdtmndt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_2397,c_155]) ).
cnf(c_2398,plain,
( sK0 = xx
| ~ aElement0(sK0)
| aElementOf0(sK0,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5234]) ).
cnf(c_5235,plain,
( aElement0(sK0)
| ~ aSet0(xS) ),
inference(resolve,[status(thm)],[c_2397,c_144]) ).
cnf(c_2399,plain,
aElement0(sK0),
inference(resolve,[status(thm)],[c_113,c_5235]) ).
cnf(c_2405,plain,
( sK0 = xx
| aElementOf0(sK0,sdtmndt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_2399,c_2398]) ).
cnf(c_5236,plain,
( xx != sK0
| aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(resolve,[status(thm)],[c_2399,c_149]) ).
cnf(c_2461,plain,
( sK0 != xx
| aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(copy,[status(thm)],[c_5236]) ).
cnf(c_5237,plain,
( ~ aElement0(sK0)
| aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx))
| sK0 = xx ),
inference(resolve,[status(thm)],[c_2405,c_151]) ).
cnf(c_2678,plain,
( aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx))
| sK0 = xx ),
inference(resolve,[status(thm)],[c_2399,c_5237]) ).
cnf(c_5238,plain,
( aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx))
| aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)) ),
inference(resolve,[status(thm)],[c_2678,c_2461]) ).
cnf(c_4681,plain,
aElementOf0(sK0,sdtpldt0(sdtmndt0(xS,xx),xx)),
inference(copy,[status(thm)],[c_5238]) ).
cnf(c_4691,negated_conjecture,
aElementOf0(sK1,sdtpldt0(sdtmndt0(xS,xx),xx)),
inference(resolve,[status(thm)],[c_4681,c_30]) ).
cnf(c_4692,negated_conjecture,
~ aElementOf0(sK1,xS),
inference(resolve,[status(thm)],[c_4681,c_29]) ).
cnf(c_5239,negated_conjecture,
( xx = sK1
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(resolve,[status(thm)],[c_4691,c_152]) ).
cnf(c_4747,negated_conjecture,
( sK1 = xx
| aElementOf0(sK1,sdtmndt0(xS,xx)) ),
inference(copy,[status(thm)],[c_5239]) ).
cnf(c_5240,plain,
( aElementOf0(sK1,xS)
| sK1 = xx ),
inference(resolve,[status(thm)],[c_4747,c_157]) ).
cnf(c_5194,negated_conjecture,
sK1 = xx,
inference(resolve,[status(thm)],[c_4692,c_5240]) ).
cnf(c_5241,plain,
~ aElementOf0(xx,xS),
inference(paramod,[status(thm)],[c_5194,c_4692]) ).
cnf(c_5219,plain,
$false,
inference(resolve,[status(thm)],[c_112,c_5241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM535+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n002.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sat Sep 26 03:11:05 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.46 % Process 704757 was started by sandbox on n002,
% 0.18/0.46 % Sat Sep 26 03:11:05 2026
% 0.18/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.22/0.49
% 0.22/0.49 % From the command line: assign(max_seconds, 300).
% 55.03/9.52
% 55.03/9.52 % given #500 (F,wt=12): 3174 sdtmndt0(sdtmndt0(slcrc0,c1),f1(xS)) != xS | f1(xS) != xx. [resolve(2505,a,284,a),flip(b)].
% 55.03/9.52
% 55.03/9.52 % SZS status Theorem for theBenchmark
% 55.03/9.52
% 55.03/9.52 % Proof 1 at 0.64 (+ 0.22) seconds.
% 55.03/9.52 % Length of proof is 34.
% 55.03/9.52 % Level of proof is 14.
% 55.03/9.52 % Maximum clause weight is 30.000.
% 55.03/9.52 % Given clauses 576.
% 55.03/9.52
% 55.03/9.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------