%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM542+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:25:56 PM UTC 2026
% Result : Theorem 10.17s 2.25s
% Output : CNFRefutation 10.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 21
% Syntax : Number of formulae : 225 ( 20 unt; 7 def)
% Number of atoms : 1048 ( 73 equ)
% Maximal formula atoms : 24 ( 4 avg)
% Number of connectives : 1300 ( 477 ~; 509 |; 235 &)
% ( 45 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 6 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 311 ( 0 sgn 297 !; 14 ?; 83 :)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(f15,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aSet0(X0) )
=> ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& aSet0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefCons) ).
fof(f17,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> sdtpldt0(sdtmndt0(X0,X1),X1) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mConsDiff) ).
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(f28,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> X0 != szszuzczcdt0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNatNSucc) ).
fof(f32,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( sdtlseqdt0(X0,X1)
<=> sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccLess) ).
fof(f33,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sdtlseqdt0(X0,szszuzczcdt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessSucc) ).
fof(f35,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X0)
& sdtlseqdt0(X0,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessASymm) ).
fof(f36,axiom,
! [X0,X1,X2] :
( ( aElementOf0(X2,szNzAzT0)
& aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X0,X1) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessTrans) ).
fof(f37,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessTotal) ).
fof(f50,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
<=> ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& aSet0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSeg) ).
fof(f53,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( X0 = X1
| aElementOf0(X0,slbdtrb0(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegSucc) ).
fof(f54,axiom,
( aElementOf0(xn,szNzAzT0)
& aElementOf0(xm,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1964) ).
fof(f55,conjecture,
( ( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
=> aElementOf0(X0,slbdtrb0(xn)) )
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xn)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm)) )
=> sdtlseqdt0(xm,xn) )
& ( sdtlseqdt0(xm,xn)
=> ( ( ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm)) )
=> ( ( ! [X0] :
( aElementOf0(X0,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xn)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xn)) )
=> ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
| ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
=> aElementOf0(X0,slbdtrb0(xn)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f56,negated_conjecture,
~ ( ( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
=> aElementOf0(X0,slbdtrb0(xn)) )
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xn)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm)) )
=> sdtlseqdt0(xm,xn) )
& ( sdtlseqdt0(xm,xn)
=> ( ( ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm)) )
=> ( ( ! [X0] :
( aElementOf0(X0,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xn)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xn)) )
=> ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
| ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
=> aElementOf0(X0,slbdtrb0(xn)) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
~ ( ( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X5] :
( aElementOf0(X5,slbdtrb0(xm))
=> aElementOf0(X5,slbdtrb0(xn)) )
& ! [X4] :
( aElementOf0(X4,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X4),xn)
& aElementOf0(X4,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ! [X3] :
( aElementOf0(X3,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X3),xm)
& aElementOf0(X3,szNzAzT0) ) )
& aSet0(slbdtrb0(xm)) )
=> sdtlseqdt0(xm,xn) )
& ( sdtlseqdt0(xm,xn)
=> ( ( ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm)) )
=> ( ( ! [X1] :
( aElementOf0(X1,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X1),xn)
& aElementOf0(X1,szNzAzT0) ) )
& aSet0(slbdtrb0(xn)) )
=> ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
| ! [X2] :
( aElementOf0(X2,slbdtrb0(xm))
=> aElementOf0(X2,slbdtrb0(xn)) ) ) ) ) ) ),
inference(rectify,[],[f56]) ).
fof(f63,plain,
( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X5] :
( ~ aElementOf0(X5,slbdtrb0(xm))
| aElementOf0(X5,slbdtrb0(xn)) )
& ! [X4] :
( aElementOf0(X4,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X4),xn)
& aElementOf0(X4,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ! [X3] :
( aElementOf0(X3,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X3),xm)
& aElementOf0(X3,szNzAzT0) ) )
& aSet0(slbdtrb0(xm))
& ~ sdtlseqdt0(xm,xn) )
| ( sdtlseqdt0(xm,xn)
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm))
& ! [X1] :
( aElementOf0(X1,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X1),xn)
& aElementOf0(X1,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ? [X2] :
( aElementOf0(X2,slbdtrb0(xm))
& ~ aElementOf0(X2,slbdtrb0(xn)) ) ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f64,plain,
( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X5] :
( ~ aElementOf0(X5,slbdtrb0(xm))
| aElementOf0(X5,slbdtrb0(xn)) )
& ! [X4] :
( aElementOf0(X4,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X4),xn)
& aElementOf0(X4,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ! [X3] :
( aElementOf0(X3,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X3),xm)
& aElementOf0(X3,szNzAzT0) ) )
& aSet0(slbdtrb0(xm))
& ~ sdtlseqdt0(xm,xn) )
| ( sdtlseqdt0(xm,xn)
& ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& aSet0(slbdtrb0(xm))
& ! [X1] :
( aElementOf0(X1,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X1),xn)
& aElementOf0(X1,szNzAzT0) ) )
& aSet0(slbdtrb0(xn))
& ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ? [X2] :
( aElementOf0(X2,slbdtrb0(xm))
& ~ aElementOf0(X2,slbdtrb0(xn)) ) ) ),
inference(flattening,[],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ),
inference(ennf_transformation,[],[f37]) ).
fof(f66,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ),
inference(flattening,[],[f65]) ).
fof(f67,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(X0,szszuzczcdt0(X0)) ),
inference(ennf_transformation,[],[f33]) ).
fof(f68,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( sdtlseqdt0(X0,X1)
<=> sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)) ) ),
inference(ennf_transformation,[],[f32]) ).
fof(f69,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( sdtlseqdt0(X0,X1)
<=> sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)) ) ),
inference(flattening,[],[f68]) ).
fof(f70,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| X0 != szszuzczcdt0(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f80,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(ennf_transformation,[],[f36]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(flattening,[],[f81]) ).
fof(f83,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f35]) ).
fof(f84,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f83]) ).
fof(f86,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( X0 = X1
| aElementOf0(X0,slbdtrb0(X1)) ) ) ),
inference(ennf_transformation,[],[f53]) ).
fof(f87,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( X0 = X1
| aElementOf0(X0,slbdtrb0(X1)) ) ) ),
inference(flattening,[],[f86]) ).
fof(f89,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
<=> ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f98,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f119,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ~ aElementOf0(X1,X0)
| sdtpldt0(sdtmndt0(X0,X1),X1) = X0 ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f124,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& aSet0(X2) ) ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f125,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& aSet0(X2) ) ) ),
inference(flattening,[],[f124]) ).
fof(f139,plain,
( ~ sP4
| ( sdtlseqdt0(xm,xn)
& sP2
& aSet0(slbdtrb0(xm))
& sP3
& aSet0(slbdtrb0(xn))
& ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ? [X2] :
( aElementOf0(X2,slbdtrb0(xm))
& ~ aElementOf0(X2,slbdtrb0(xn)) ) ) ),
inference(nnf_transformation,[],[f131]) ).
fof(f140,plain,
( ~ sP4
| ( sdtlseqdt0(xm,xn)
& sP2
& aSet0(slbdtrb0(xm))
& sP3
& aSet0(slbdtrb0(xn))
& ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ? [X0] :
( aElementOf0(X0,slbdtrb0(xm))
& ~ aElementOf0(X0,slbdtrb0(xn)) ) ) ),
inference(rectify,[],[f139]) ).
fof(f141,plain,
( ~ sP4
| ( sdtlseqdt0(xm,xn)
& sP2
& aSet0(slbdtrb0(xm))
& sP3
& aSet0(slbdtrb0(xn))
& ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& aElementOf0(sK9,slbdtrb0(xm))
& ~ aElementOf0(sK9,slbdtrb0(xn)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X0,sK9)],[f140]) ).
fof(f142,plain,
( ~ sP3
| ! [X1] :
( ( ~ aElementOf0(X1,slbdtrb0(xn))
| ( sdtlseqdt0(szszuzczcdt0(X1),xn)
& aElementOf0(X1,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X1),xn)
| ~ aElementOf0(X1,szNzAzT0)
| aElementOf0(X1,slbdtrb0(xn)) ) ) ),
inference(nnf_transformation,[],[f130]) ).
fof(f143,plain,
( ~ sP3
| ! [X1] :
( ( ~ aElementOf0(X1,slbdtrb0(xn))
| ( sdtlseqdt0(szszuzczcdt0(X1),xn)
& aElementOf0(X1,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X1),xn)
| ~ aElementOf0(X1,szNzAzT0)
| aElementOf0(X1,slbdtrb0(xn)) ) ) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
( ~ sP3
| ! [X0] :
( ( ~ aElementOf0(X0,slbdtrb0(xn))
| ( sdtlseqdt0(szszuzczcdt0(X0),xn)
& aElementOf0(X0,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xn)) ) ) ),
inference(rectify,[],[f143]) ).
fof(f145,plain,
( ~ sP2
| ! [X0] :
( ( ~ aElementOf0(X0,slbdtrb0(xm))
| ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xm)) ) ) ),
inference(nnf_transformation,[],[f129]) ).
fof(f146,plain,
( ~ sP2
| ! [X0] :
( ( ~ aElementOf0(X0,slbdtrb0(xm))
| ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xm)) ) ) ),
inference(flattening,[],[f145]) ).
fof(f147,plain,
( ~ sP1
| ! [X3] :
( ( ~ aElementOf0(X3,slbdtrb0(xm))
| ( sdtlseqdt0(szszuzczcdt0(X3),xm)
& aElementOf0(X3,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),xm)
| ~ aElementOf0(X3,szNzAzT0)
| aElementOf0(X3,slbdtrb0(xm)) ) ) ),
inference(nnf_transformation,[],[f128]) ).
fof(f148,plain,
( ~ sP1
| ! [X3] :
( ( ~ aElementOf0(X3,slbdtrb0(xm))
| ( sdtlseqdt0(szszuzczcdt0(X3),xm)
& aElementOf0(X3,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),xm)
| ~ aElementOf0(X3,szNzAzT0)
| aElementOf0(X3,slbdtrb0(xm)) ) ) ),
inference(flattening,[],[f147]) ).
fof(f149,plain,
( ~ sP1
| ! [X0] :
( ( ~ aElementOf0(X0,slbdtrb0(xm))
| ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xm)) ) ) ),
inference(rectify,[],[f148]) ).
fof(f153,plain,
( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X0] :
( ~ aElementOf0(X0,slbdtrb0(xm))
| aElementOf0(X0,slbdtrb0(xn)) )
& sP0
& aSet0(slbdtrb0(xn))
& sP1
& aSet0(slbdtrb0(xm))
& ~ sdtlseqdt0(xm,xn) )
| sP4 ),
inference(rectify,[],[f132]) ).
fof(f154,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( ( ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| sdtlseqdt0(X0,X1) ) ) ),
inference(nnf_transformation,[],[f69]) ).
fof(f155,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(nnf_transformation,[],[f80]) ).
fof(f156,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(rectify,[],[f156]) ).
fof(f158,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ( aElementOf0(sK10(X0,X1),X1)
& ~ aElementOf0(sK10(X0,X1),X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f157]) ).
fof(f159,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( ( ~ aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| X0 = X1
| aElementOf0(X0,slbdtrb0(X1)) )
& ( ( X0 != X1
& ~ aElementOf0(X0,slbdtrb0(X1)) )
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1))) ) ) ),
inference(nnf_transformation,[],[f87]) ).
fof(f160,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ( ( ~ aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| X0 = X1
| aElementOf0(X0,slbdtrb0(X1)) )
& ( ( X0 != X1
& ~ aElementOf0(X0,slbdtrb0(X1)) )
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1))) ) ) ),
inference(flattening,[],[f159]) ).
fof(f161,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X2] :
( ( ~ aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0)
| aElementOf0(X2,X1) ) )
& aSet0(X1) ) )
& ( ? [X2] :
( ( aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ aElementOf0(X2,X1)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f162,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X2] :
( ( ~ aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0)
| aElementOf0(X2,X1) ) )
& aSet0(X1) ) )
& ( ? [X2] :
( ( aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ aElementOf0(X2,X1)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(flattening,[],[f161]) ).
fof(f163,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X3] :
( ( ~ aElementOf0(X3,X1)
| ( sdtlseqdt0(szszuzczcdt0(X3),X0)
& aElementOf0(X3,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),X0)
| ~ aElementOf0(X3,szNzAzT0)
| aElementOf0(X3,X1) ) )
& aSet0(X1) ) )
& ( ? [X2] :
( ( aElementOf0(X2,X1)
| ( sdtlseqdt0(szszuzczcdt0(X2),X0)
& aElementOf0(X2,szNzAzT0) ) )
& ( ~ aElementOf0(X2,X1)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(rectify,[],[f162]) ).
fof(f164,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ! [X1] :
( ( slbdtrb0(X0) != X1
| ( ! [X3] :
( ( ~ aElementOf0(X3,X1)
| ( sdtlseqdt0(szszuzczcdt0(X3),X0)
& aElementOf0(X3,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),X0)
| ~ aElementOf0(X3,szNzAzT0)
| aElementOf0(X3,X1) ) )
& aSet0(X1) ) )
& ( ( ( aElementOf0(sK11(X0,X1),X1)
| ( sdtlseqdt0(szszuzczcdt0(sK11(X0,X1)),X0)
& aElementOf0(sK11(X0,X1),szNzAzT0) ) )
& ( ~ aElementOf0(sK11(X0,X1),X1)
| ~ sdtlseqdt0(szszuzczcdt0(sK11(X0,X1)),X0)
| ~ aElementOf0(sK11(X0,X1),szNzAzT0) ) )
| ~ aSet0(X1)
| X1 = slbdtrb0(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f163]) ).
fof(f185,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f54]) ).
fof(f186,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f54]) ).
fof(f187,plain,
( ~ sP4
| sdtlseqdt0(xm,xn) ),
inference(cnf_transformation,[],[f141]) ).
fof(f188,plain,
( ~ sP4
| sP2 ),
inference(cnf_transformation,[],[f141]) ).
fof(f189,plain,
( ~ sP4
| aSet0(slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f190,plain,
( ~ sP4
| sP3 ),
inference(cnf_transformation,[],[f141]) ).
fof(f192,plain,
( ~ sP4
| ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f193,plain,
( ~ sP4
| aElementOf0(sK9,slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f194,plain,
( ~ sP4
| ~ aElementOf0(sK9,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f195,plain,
! [X0] :
( ~ sP3
| ~ aElementOf0(X0,slbdtrb0(xn))
| sdtlseqdt0(szszuzczcdt0(X0),xn) ),
inference(cnf_transformation,[],[f144]) ).
fof(f196,plain,
! [X0] :
( ~ sP3
| ~ aElementOf0(X0,slbdtrb0(xn))
| aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f197,plain,
! [X0] :
( ~ sP3
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f144]) ).
fof(f199,plain,
! [X0] :
( ~ sP2
| ~ aElementOf0(X0,slbdtrb0(xm))
| aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f200,plain,
! [X0] :
( ~ sP2
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f146]) ).
fof(f202,plain,
! [X0] :
( ~ sP1
| ~ aElementOf0(X0,slbdtrb0(xm))
| aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f203,plain,
! [X0] :
( ~ sP1
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f149]) ).
fof(f208,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtrb0(xm))
| aElementOf0(X0,slbdtrb0(xn))
| sP4 ),
inference(cnf_transformation,[],[f153]) ).
fof(f209,plain,
( sP0
| sP4 ),
inference(cnf_transformation,[],[f153]) ).
fof(f211,plain,
( sP1
| sP4 ),
inference(cnf_transformation,[],[f153]) ).
fof(f212,plain,
( aSet0(slbdtrb0(xm))
| sP4 ),
inference(cnf_transformation,[],[f153]) ).
fof(f213,plain,
( ~ sdtlseqdt0(xm,xn)
| sP4 ),
inference(cnf_transformation,[],[f153]) ).
fof(f214,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f215,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sdtlseqdt0(X0,szszuzczcdt0(X0)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f217,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f218,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(X0) != X0 ),
inference(cnf_transformation,[],[f70]) ).
fof(f226,plain,
! [X0,X1] :
( ~ aSet0(X0)
| aElementOf0(sK10(X0,X1),X1)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f227,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(sK10(X0,X1),X0)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f228,plain,
! [X2,X0,X1] :
( ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(cnf_transformation,[],[f82]) ).
fof(f229,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f84]) ).
fof(f233,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1))
| aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1))) ),
inference(cnf_transformation,[],[f160]) ).
fof(f236,plain,
! [X3,X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| slbdtrb0(X0) != X1
| ~ aElementOf0(X3,X1)
| sdtlseqdt0(szszuzczcdt0(X3),X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f237,plain,
! [X3,X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| slbdtrb0(X0) != X1
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,szNzAzT0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f239,plain,
! [X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| slbdtrb0(X0) != X1
| aSet0(X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f255,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(szszuzczcdt0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f272,plain,
! [X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X1,X0)
| sdtpldt0(sdtmndt0(X0,X1),X1) = X0 ),
inference(cnf_transformation,[],[f119]) ).
fof(f300,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(slbdtrb0(X0)) ),
inference(equality_resolution,[],[f239]) ).
fof(f302,plain,
! [X3,X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X3,slbdtrb0(X0))
| aElementOf0(X3,szNzAzT0) ),
inference(equality_resolution,[],[f237]) ).
fof(f303,plain,
! [X3,X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X3,slbdtrb0(X0))
| sdtlseqdt0(szszuzczcdt0(X3),X0) ),
inference(equality_resolution,[],[f236]) ).
tcf(c_49,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f186]) ).
tcf(c_50,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f185]) ).
tcf(c_51,plain,
( ~ sP4
| ~ aElementOf0(sK9,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_52,plain,
( aElementOf0(sK9,slbdtrb0(xm))
| ~ sP4 ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_53,plain,
( ~ sP4
| ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_55,plain,
( sP3
| ~ sP4 ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_56,plain,
( aSet0(slbdtrb0(xm))
| ~ sP4 ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_57,plain,
( sP2
| ~ sP4 ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_58,plain,
( sdtlseqdt0(xm,xn)
| ~ sP4 ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_59,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xn))
| ~ sP3
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_60,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ sP3
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_61,plain,
! [X0: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ sP3
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_62,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xm))
| ~ sP2
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_63,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ sP2
| ~ aElementOf0(X0,slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_65,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xm))
| ~ sP1
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_66,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ sP1
| ~ aElementOf0(X0,slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_71,negated_conjecture,
( sP4
| ~ sdtlseqdt0(xm,xn) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_72,negated_conjecture,
( sP4
| aSet0(slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_73,negated_conjecture,
( sP1
| sP4 ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_75,negated_conjecture,
( sP0
| sP4 ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_76,negated_conjecture,
! [X0: $i] :
( sP4
| aElementOf0(X0,slbdtrb0(xn))
| ~ aElementOf0(X0,slbdtrb0(xm)) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(szszuzczcdt0(X1),X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_79,plain,
! [X0: $i] :
( sdtlseqdt0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_82,plain,
! [X0: $i] :
( ~ aElementOf0(X0,szNzAzT0)
| ( szszuzczcdt0(X0) != X0 ) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(X1,X0)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aElementOf0(sK10(X0,X1),X0) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(X1,X0)
| aElementOf0(sK10(X0,X1),X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] :
( sdtlseqdt0(X0,X2)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_103,plain,
! [X0: $i] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_118,plain,
! [X0: $i] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i] :
( ( sdtpldt0(sdtmndt0(X1,X0),X0) = X1 )
| ~ aSet0(X1)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_234,negated_conjecture,
aSet0(slbdtrb0(xm)),
inference(global_subsumption_just,[status(thm)],[c_72,c_72,c_56]) ).
tcf(c_236,plain,
aSet0(slbdtrb0(xm)),
inference(global_subsumption_just,[status(thm)],[c_56,c_234]) ).
tcf(c_267,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xm))
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_65,c_73,c_57,c_65,c_62]) ).
tcf(c_268,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xm))
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm) ),
inference(renaming,[status(thm)],[c_267]) ).
tcf(c_270,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xm))
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_62,c_268]) ).
tcf(c_271,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xm))
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xm) ),
inference(renaming,[status(thm)],[c_270]) ).
tcf(c_274,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_95,c_105,c_95]) ).
tcf(c_11578,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(X1),szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(superposition,[status(thm)],[c_274,c_106]) ).
tcf(c_11941,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(slbdtrb0(X0),X1)
| sdtlseqdt0(szszuzczcdt0(sK10(X1,slbdtrb0(X0))),X0)
| ~ aSet0(X1)
| ~ aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_89,c_106]) ).
tcf(c_12020,plain,
( aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_12026,plain,
( sdtlseqdt0(xn,szszuzczcdt0(xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_12029,plain,
( ~ aElementOf0(xn,szNzAzT0)
| ( szszuzczcdt0(xn) != xn ) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_12184,plain,
( aElementOf0(xn,slbdtrb0(xm))
| ~ aElementOf0(xn,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_12333,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11578,c_118]) ).
tcf(c_12551,plain,
! [X0: $i] :
( sdtlseqdt0(xm,X0)
| sdtlseqdt0(szszuzczcdt0(X0),xm)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_12774,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(slbdtrb0(X0),X1)
| sdtlseqdt0(szszuzczcdt0(sK10(X1,slbdtrb0(X0))),X0)
| ~ aSet0(X1)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_11941,c_103,c_11941]) ).
tcf(c_12787,plain,
! [X0: $i] :
( aSubsetOf0(slbdtrb0(xm),X0)
| aElementOf0(sK10(X0,slbdtrb0(xm)),slbdtrb0(xm))
| ~ aSet0(X0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(sK10(X0,slbdtrb0(xm)),szNzAzT0) ),
inference(superposition,[status(thm)],[c_12774,c_271]) ).
tcf(c_12796,plain,
! [X0: $i] :
( aSubsetOf0(slbdtrb0(xm),X0)
| aElementOf0(sK10(X0,slbdtrb0(xm)),slbdtrb0(xm))
| ~ aSet0(X0)
| ~ aElementOf0(sK10(X0,slbdtrb0(xm)),szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12787,c_49]) ).
tcf(c_12837,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(superposition,[status(thm)],[c_12333,c_80]) ).
tcf(c_14993,plain,
( ( xm = xn )
| ~ sP4
| ~ sdtlseqdt0(xn,xm)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(superposition,[status(thm)],[c_58,c_93]) ).
tcf(c_15053,plain,
( ( xm = xn )
| ~ sP4
| ~ sdtlseqdt0(xn,xm) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14993,c_50,c_49]) ).
tcf(c_16052,plain,
( ( szszuzczcdt0(xn) = xn )
| ~ aElementOf0(xn,szNzAzT0)
| ~ sdtlseqdt0(xn,szszuzczcdt0(xn))
| ~ sdtlseqdt0(szszuzczcdt0(xn),xn)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_17446,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(xm,X1)
| ~ sdtlseqdt0(xm,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(superposition,[status(thm)],[c_49,c_92]) ).
tcf(c_18498,plain,
( sdtlseqdt0(xm,xn)
| sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_12551]) ).
tcf(c_21129,plain,
( sP4
| aElementOf0(xn,slbdtrb0(xn))
| ~ aElementOf0(xn,slbdtrb0(xm)) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_22138,plain,
! [X0: $i,X1: $i] :
( sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_12837,c_105,c_12837]) ).
tcf(c_26728,plain,
! [X0: $i] :
( sdtlseqdt0(xm,X0)
| ~ sdtlseqdt0(xm,xn)
| ~ sdtlseqdt0(xn,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_50,c_17446]) ).
fof(f127,definition,
( ~ sP0
| ! [X4] :
( aElementOf0(X4,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X4),xn)
& aElementOf0(X4,szNzAzT0) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f128,definition,
( ~ sP1
| ! [X3] :
( aElementOf0(X3,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X3),xm)
& aElementOf0(X3,szNzAzT0) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f129,definition,
( ~ sP2
| ! [X0] :
( aElementOf0(X0,slbdtrb0(xm))
<=> ( sdtlseqdt0(szszuzczcdt0(X0),xm)
& aElementOf0(X0,szNzAzT0) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f130,definition,
( ~ sP3
| ! [X1] :
( aElementOf0(X1,slbdtrb0(xn))
<=> ( sdtlseqdt0(szszuzczcdt0(X1),xn)
& aElementOf0(X1,szNzAzT0) ) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f131,definition,
( ~ sP4
| ( sdtlseqdt0(xm,xn)
& sP2
& aSet0(slbdtrb0(xm))
& sP3
& aSet0(slbdtrb0(xn))
& ~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ? [X2] :
( aElementOf0(X2,slbdtrb0(xm))
& ~ aElementOf0(X2,slbdtrb0(xn)) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f132,plain,
( ( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn))
& ! [X5] :
( ~ aElementOf0(X5,slbdtrb0(xm))
| aElementOf0(X5,slbdtrb0(xn)) )
& sP0
& aSet0(slbdtrb0(xn))
& sP1
& aSet0(slbdtrb0(xm))
& ~ sdtlseqdt0(xm,xn) )
| sP4 ),
inference(definition_folding,[],[f64,f131,f130,f129,f128,f127]) ).
fof(f136,definition,
! [X2,X0,X1] :
( sP7(X2,X0,X1)
<=> ( ! [X3] :
( aElementOf0(X3,X2)
<=> ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& aSet0(X2) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f137,definition,
! [X1,X0] :
( ~ sP8(X1,X0)
| ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> sP7(X2,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f138,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aSet0(X0)
| sP8(X1,X0) ),
inference(definition_folding,[],[f125,f137,f136]) ).
fof(f150,plain,
( ~ sP0
| ! [X4] :
( ( ~ aElementOf0(X4,slbdtrb0(xn))
| ( sdtlseqdt0(szszuzczcdt0(X4),xn)
& aElementOf0(X4,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X4),xn)
| ~ aElementOf0(X4,szNzAzT0)
| aElementOf0(X4,slbdtrb0(xn)) ) ) ),
inference(nnf_transformation,[],[f127]) ).
fof(f151,plain,
( ~ sP0
| ! [X4] :
( ( ~ aElementOf0(X4,slbdtrb0(xn))
| ( sdtlseqdt0(szszuzczcdt0(X4),xn)
& aElementOf0(X4,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X4),xn)
| ~ aElementOf0(X4,szNzAzT0)
| aElementOf0(X4,slbdtrb0(xn)) ) ) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
( ~ sP0
| ! [X0] :
( ( ~ aElementOf0(X0,slbdtrb0(xn))
| ( sdtlseqdt0(szszuzczcdt0(X0),xn)
& aElementOf0(X0,szNzAzT0) ) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xn)) ) ) ),
inference(rectify,[],[f151]) ).
fof(f181,plain,
! [X2,X0,X1] :
( ( ~ sP7(X2,X0,X1)
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& ( ( X1 != X3
& ~ aElementOf0(X3,X0) )
| ~ aElement0(X3)
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& ( ~ aElementOf0(X3,X2)
| ( X1 != X3
& ~ aElementOf0(X3,X0) )
| ~ aElement0(X3) ) )
| ~ aSet0(X2)
| sP7(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f136]) ).
fof(f182,plain,
! [X2,X0,X1] :
( ( ~ sP7(X2,X0,X1)
| ( ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& ( ( X1 != X3
& ~ aElementOf0(X3,X0) )
| ~ aElement0(X3)
| aElementOf0(X3,X2) ) )
& aSet0(X2) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X2)
| ( ( X3 = X1
| aElementOf0(X3,X0) )
& aElement0(X3) ) )
& ( ~ aElementOf0(X3,X2)
| ( X1 != X3
& ~ aElementOf0(X3,X0) )
| ~ aElement0(X3) ) )
| ~ aSet0(X2)
| sP7(X2,X0,X1) ) ),
inference(flattening,[],[f181]) ).
fof(f183,plain,
! [X0,X1,X2] :
( ( ~ sP7(X0,X1,X2)
| ( ! [X4] :
( ( ~ aElementOf0(X4,X0)
| ( ( X2 = X4
| aElementOf0(X4,X1) )
& aElement0(X4) ) )
& ( ( X2 != X4
& ~ aElementOf0(X4,X1) )
| ~ aElement0(X4)
| aElementOf0(X4,X0) ) )
& aSet0(X0) ) )
& ( ? [X3] :
( ( aElementOf0(X3,X0)
| ( ( X2 = X3
| aElementOf0(X3,X1) )
& aElement0(X3) ) )
& ( ~ aElementOf0(X3,X0)
| ( X2 != X3
& ~ aElementOf0(X3,X1) )
| ~ aElement0(X3) ) )
| ~ aSet0(X0)
| sP7(X0,X1,X2) ) ),
inference(rectify,[],[f182]) ).
fof(f184,plain,
! [X0,X1,X2] :
( ( ~ sP7(X0,X1,X2)
| ( ! [X4] :
( ( ~ aElementOf0(X4,X0)
| ( ( X2 = X4
| aElementOf0(X4,X1) )
& aElement0(X4) ) )
& ( ( X2 != X4
& ~ aElementOf0(X4,X1) )
| ~ aElement0(X4)
| aElementOf0(X4,X0) ) )
& aSet0(X0) ) )
& ( ( ( aElementOf0(sK16(X0,X1,X2),X0)
| ( ( sK16(X0,X1,X2) = X2
| aElementOf0(sK16(X0,X1,X2),X1) )
& aElement0(sK16(X0,X1,X2)) ) )
& ( ~ aElementOf0(sK16(X0,X1,X2),X0)
| ( sK16(X0,X1,X2) != X2
& ~ aElementOf0(sK16(X0,X1,X2),X1) )
| ~ aElement0(sK16(X0,X1,X2)) ) )
| ~ aSet0(X0)
| sP7(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X3,sK16(X0,X1,X2))],[f183]) ).
fof(f204,plain,
! [X0] :
( ~ sP0
| ~ aElementOf0(X0,slbdtrb0(xn))
| sdtlseqdt0(szszuzczcdt0(X0),xn) ),
inference(cnf_transformation,[],[f152]) ).
fof(f205,plain,
! [X0] :
( ~ sP0
| ~ aElementOf0(X0,slbdtrb0(xn))
| aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f206,plain,
! [X0] :
( ~ sP0
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(X0,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f152]) ).
fof(f293,plain,
! [X2,X0,X1] :
( aElementOf0(sK16(X0,X1,X2),X0)
| sK16(X0,X1,X2) = X2
| aElementOf0(sK16(X0,X1,X2),X1)
| ~ aSet0(X0)
| sP7(X0,X1,X2) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_68,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xn))
| ~ sP0
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_69,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ sP0
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_70,plain,
! [X0: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ sP0
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP7(X0,X1,X2)
| aElementOf0(sK16(X0,X1,X2),X1)
| aElementOf0(sK16(X0,X1,X2),X0)
| ( sK16(X0,X1,X2) = X2 )
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_244,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(global_subsumption_just,[status(thm)],[c_69,c_75,c_55,c_69,c_60]) ).
tcf(c_247,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(xm)) ),
inference(global_subsumption_just,[status(thm)],[c_66,c_57,c_76,c_63,c_244]) ).
tcf(c_254,plain,
! [X0: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(global_subsumption_just,[status(thm)],[c_70,c_75,c_55,c_70,c_61]) ).
tcf(c_264,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xn))
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_68,c_75,c_55,c_68,c_59]) ).
tcf(c_265,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xn))
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn) ),
inference(renaming,[status(thm)],[c_264]) ).
tcf(c_272,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xn))
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_59,c_265]) ).
tcf(c_273,plain,
! [X0: $i] :
( aElementOf0(X0,slbdtrb0(xn))
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X0),xn) ),
inference(renaming,[status(thm)],[c_272]) ).
tcf(c_4700,plain,
! [X0: $i] :
( sdtlseqdt0(szszuzczcdt0(X0),xn)
| ~ aElementOf0(X0,slbdtrb0(xn)) ),
inference(prop_impl_just,[status(thm)],[c_254]) ).
tcf(c_4724,plain,
! [X0: $i] :
( ~ aElementOf0(X0,slbdtrb0(xm))
| aElementOf0(X0,szNzAzT0) ),
inference(prop_impl_just,[status(thm)],[c_247]) ).
tcf(c_4725,plain,
! [X0: $i] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,slbdtrb0(xm)) ),
inference(renaming,[status(thm)],[c_4724]) ).
tcf(c_10945,plain,
( aElementOf0(sK9,szNzAzT0)
| ~ sP4 ),
inference(superposition,[status(thm)],[c_52,c_4725]) ).
tcf(c_11331,plain,
! [X0: $i] :
( sdtlseqdt0(xn,X0)
| aElementOf0(X0,slbdtrb0(xn))
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[status(thm)],[c_78,c_273]) ).
tcf(c_11339,plain,
! [X0: $i] :
( sdtlseqdt0(xn,X0)
| aElementOf0(X0,slbdtrb0(xn))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11331,c_50]) ).
tcf(c_11700,plain,
( sdtlseqdt0(xn,sK9)
| ~ sP4
| ~ aElementOf0(sK9,szNzAzT0) ),
inference(superposition,[status(thm)],[c_11339,c_51]) ).
tcf(c_11749,plain,
( sdtlseqdt0(xn,sK9)
| ~ sP4 ),
inference(global_subsumption_just,[status(thm)],[c_11700,c_10945,c_11700]) ).
tcf(c_11938,plain,
! [X0: $i] :
( aSubsetOf0(slbdtrb0(xm),X0)
| aElementOf0(sK10(X0,slbdtrb0(xm)),szNzAzT0)
| ~ aSet0(X0)
| ~ aSet0(slbdtrb0(xm)) ),
inference(superposition,[status(thm)],[c_89,c_4725]) ).
tcf(c_11975,plain,
! [X0: $i] :
( aSubsetOf0(slbdtrb0(xm),X0)
| aElementOf0(sK10(X0,slbdtrb0(xm)),szNzAzT0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11938,c_236]) ).
tcf(c_18783,plain,
! [X0: $i,X1: $i] :
( sP4
| sP7(X0,slbdtrb0(xm),X1)
| aElementOf0(sK16(X0,slbdtrb0(xm),X1),X0)
| aElementOf0(sK16(X0,slbdtrb0(xm),X1),slbdtrb0(xn))
| ( sK16(X0,slbdtrb0(xm),X1) = X1 )
| ~ aSet0(X0) ),
inference(superposition,[status(thm)],[c_155,c_76]) ).
tcf(c_19643,plain,
! [X0: $i,X1: $i] :
( sP4
| sP7(X0,slbdtrb0(xm),X1)
| aElementOf0(sK16(X0,slbdtrb0(xm),X1),slbdtrb0(xn))
| ( sK16(X0,slbdtrb0(xm),X1) = X1 )
| ( sdtpldt0(sdtmndt0(X0,sK16(X0,slbdtrb0(xm),X1)),sK16(X0,slbdtrb0(xm),X1)) = X0 )
| ~ aSet0(X0) ),
inference(superposition,[status(thm)],[c_18783,c_136]) ).
tcf(c_21121,plain,
( sdtlseqdt0(szszuzczcdt0(xn),xn)
| ~ aElementOf0(xn,slbdtrb0(xn)) ),
inference(instantiation,[status(thm)],[c_4700]) ).
tcf(c_21394,plain,
sP4,
inference(global_subsumption_just,[status(thm)],[c_19643,c_50,c_49,c_71,c_12020,c_12026,c_12029,c_12184,c_16052,c_18498,c_21121,c_21129]) ).
tcf(c_21396,plain,
( ( xm = xn )
| ~ sdtlseqdt0(xn,xm) ),
inference(backward_subsumption_resolution,[status(thm)],[c_15053,c_21394]) ).
tcf(c_21399,plain,
sdtlseqdt0(xn,sK9),
inference(backward_subsumption_resolution,[status(thm)],[c_11749,c_21394]) ).
tcf(c_21408,plain,
aElementOf0(sK9,szNzAzT0),
inference(backward_subsumption_resolution,[status(thm)],[c_10945,c_21394]) ).
tcf(c_21409,plain,
sdtlseqdt0(xm,xn),
inference(backward_subsumption_resolution,[status(thm)],[c_58,c_21394]) ).
tcf(c_21410,plain,
~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xn)),
inference(backward_subsumption_resolution,[status(thm)],[c_53,c_21394]) ).
tcf(c_21411,plain,
aElementOf0(sK9,slbdtrb0(xm)),
inference(backward_subsumption_resolution,[status(thm)],[c_52,c_21394]) ).
tcf(c_21433,plain,
! [X0: $i] :
( aSubsetOf0(slbdtrb0(xm),X0)
| aElementOf0(sK10(X0,slbdtrb0(xm)),slbdtrb0(xm))
| ~ aSet0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_12796,c_11975,c_12796]) ).
tcf(c_21443,plain,
( aSubsetOf0(slbdtrb0(xm),slbdtrb0(xm))
| ~ aSet0(slbdtrb0(xm)) ),
inference(superposition,[status(thm)],[c_21433,c_88]) ).
tcf(c_21450,plain,
aSubsetOf0(slbdtrb0(xm),slbdtrb0(xm)),
inference(forward_subsumption_resolution,[status(thm)],[c_21443,c_236]) ).
tcf(c_22146,plain,
( sdtlseqdt0(sK9,xm)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(superposition,[status(thm)],[c_21411,c_22138]) ).
tcf(c_22165,plain,
sdtlseqdt0(sK9,xm),
inference(forward_subsumption_resolution,[status(thm)],[c_22146,c_49]) ).
tcf(c_22548,plain,
( ( xm = sK9 )
| ~ sdtlseqdt0(xm,sK9)
| ~ aElementOf0(sK9,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(superposition,[status(thm)],[c_22165,c_93]) ).
tcf(c_22549,plain,
( ( xm = sK9 )
| ~ sdtlseqdt0(xm,sK9) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22548,c_21408,c_49]) ).
tcf(c_26763,plain,
! [X0: $i] :
( sdtlseqdt0(xm,X0)
| ~ sdtlseqdt0(xn,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26728,c_21409]) ).
tcf(c_26980,plain,
( sdtlseqdt0(xm,sK9)
| ~ sdtlseqdt0(xn,sK9) ),
inference(superposition,[status(thm)],[c_21408,c_26763]) ).
tcf(c_26991,plain,
sdtlseqdt0(xm,sK9),
inference(forward_subsumption_resolution,[status(thm)],[c_26980,c_21399]) ).
tcf(c_27089,plain,
xm = sK9,
inference(backward_subsumption_resolution,[status(thm)],[c_22549,c_26991]) ).
tcf(c_27129,plain,
sdtlseqdt0(xn,xm),
inference(demodulation,[status(thm)],[c_21399,c_27089]) ).
tcf(c_27131,plain,
xm = xn,
inference(backward_subsumption_resolution,[status(thm)],[c_21396,c_27129]) ).
tcf(c_27167,plain,
~ aSubsetOf0(slbdtrb0(xm),slbdtrb0(xm)),
inference(demodulation,[status(thm)],[c_21410,c_27131]) ).
tcf(c_27200,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_27167,c_21450]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM542+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.36 % Computer : n011.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Thu Sep 24 04:31:58 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 10.17/2.25 % SZS status Started for theBenchmark.p
% 10.17/2.25 % SZS status Theorem for theBenchmark.p
% 10.17/2.25
% 10.17/2.25 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.17/2.25
% 10.17/2.25 % ------ iProver source info
% 10.17/2.25
% 10.17/2.25 % git: date: 2026-07-19 20:42:38 +0200
% 10.17/2.25 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.17/2.25 % git: non_committed_changes: false
% 10.17/2.25
% 10.17/2.25 % ------ Parsing...
% 10.17/2.25 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.17/2.25
% 10.17/2.25 % ------ Preprocessing... sup_sim: 0 sf_s rm: 5 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 10.17/2.25
% 10.17/2.25 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.17/2.25
% 10.17/2.25 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 10.17/2.25 % ------ Proving...
% 10.17/2.25 % ------ Problem Properties
% 10.17/2.25
% 10.17/2.25 %
% 10.17/2.25 % clauses 100
% 10.17/2.25 % conjectures 3
% 10.17/2.25 % EPR 33
% 10.17/2.25 % Horn 80
% 10.17/2.25 % unary 13
% 10.17/2.25 % binary 25
% 10.17/2.25 % lits 301
% 10.17/2.25 % lits eq 31
% 10.17/2.25 % fd_pure 0
% 10.17/2.25 % fd_pseudo 0
% 10.17/2.25 % fd_cond 3
% 10.17/2.25 % fd_pseudo_cond 11
% 10.17/2.25 % AC symbols 0
% 10.17/2.25
% 10.17/2.25 % ------ Schedule dynamic 5 is on
% 10.17/2.25
% 10.17/2.25 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.17/2.25
% 10.17/2.25
% 10.17/2.25 % ------
% 10.17/2.25 % Current options:
% 10.17/2.25 % ------
% 10.17/2.25
% 10.17/2.25
% 10.17/2.25 %
% 10.17/2.25
% 10.17/2.25 % ------ Proving...
% 10.17/2.25 %
% 10.17/2.25
% 10.17/2.25 % SZS status Theorem for theBenchmark.p
% 10.17/2.25
% 10.17/2.25 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.17/2.25
% 10.17/2.25
%------------------------------------------------------------------------------