%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM570+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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 : Tue Sep 29 12:24:51 PM UTC 2026
% Result : Theorem 14.59s 4.51s
% Output : Refutation 14.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 22
% Syntax : Number of formulae : 191 ( 18 unt; 7 def)
% Number of atoms : 965 ( 158 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 1236 ( 462 ~; 456 |; 256 &)
% ( 30 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-3 aty)
% Number of variables : 294 ( 275 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f15,axiom,
! [X0,X1] :
( ( aSet0(X0)
& aElement0(X1) )
=> ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefCons) ).
fof(f16,axiom,
! [X0,X1] :
( ( aSet0(X0)
& aElement0(X1) )
=> ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
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(f18,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aSet0(X1) )
=> ( ~ aElementOf0(X0,X1)
=> sdtmndt0(sdtpldt0(X1,X0),X0) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDiffCons) ).
fof(f23,axiom,
( aSet0(szNzAzT0)
& isCountable0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNATSet) ).
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNum) ).
fof(f27,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( X0 = sz00
| ? [X1] :
( aElementOf0(X1,szNzAzT0)
& X0 = szszuzczcdt0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNatExtra) ).
fof(f39,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> iLess0(X0,szszuzczcdt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIH) ).
fof(f50,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
<=> ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSeg) ).
fof(f53,axiom,
! [X0,X1] :
( ( aElementOf0(X0,szNzAzT0)
& aElementOf0(X1,szNzAzT0) )
=> ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( aElementOf0(X0,slbdtrb0(X1))
| X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSegSucc) ).
fof(f81,axiom,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( ( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,X0)) )
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& X1 != szmzizndt0(sdtlpdtrp0(xN,X0)) ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3623) ).
fof(f82,axiom,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3702) ).
fof(f83,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( iLess0(X0,xi)
=> ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3671) ).
fof(f84,conjecture,
( xi != sz00
=> ( ? [X0] :
( aElementOf0(X0,szNzAzT0)
& szszuzczcdt0(X0) = xi )
& ( ( aSet0(sdtlpdtrp0(xN,xi))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> aElementOf0(X0,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,xi)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f85,negated_conjecture,
~ ( xi != sz00
=> ( ? [X0] :
( aElementOf0(X0,szNzAzT0)
& szszuzczcdt0(X0) = xi )
& ( ( aSet0(sdtlpdtrp0(xN,xi))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> aElementOf0(X0,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,xi)) ) ),
inference(negated_conjecture,[status(cth)],[f84]) ).
fof(f95,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( ( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,X0)) )
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) ) ) ) ),
inference(rectify,[],[f81]) ).
fof(f96,plain,
~ ( xi != sz00
=> ( ? [X0] :
( aElementOf0(X0,szNzAzT0)
& szszuzczcdt0(X0) = xi )
& ( ( aSet0(sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> aElementOf0(X1,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,xi)) ) ),
inference(rectify,[],[f85]) ).
fof(f97,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f111,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f15]) ).
fof(f112,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f114,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f113]) ).
fof(f115,plain,
! [X0] :
( ! [X1] :
( sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f116,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| aElementOf0(X0,X1)
| ~ aElement0(X0)
| ~ aSet0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f117,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| aElementOf0(X0,X1)
| ~ aElement0(X0)
| ~ aSet0(X1) ),
inference(flattening,[],[f116]) ).
fof(f126,plain,
! [X0] :
( ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f129,plain,
! [X0] :
( X0 = sz00
| ? [X1] :
( aElementOf0(X1,szNzAzT0)
& X0 = szszuzczcdt0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f130,plain,
! [X0] :
( X0 = sz00
| ? [X1] :
( aElementOf0(X1,szNzAzT0)
& X0 = szszuzczcdt0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f129]) ).
fof(f144,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f162,plain,
! [X0] :
( ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
<=> ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) ) ) ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f164,plain,
! [X0,X1] :
( ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( aElementOf0(X0,slbdtrb0(X1))
| X0 = X1 ) )
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f165,plain,
! [X0,X1] :
( ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( aElementOf0(X0,slbdtrb0(X1))
| X0 = X1 ) )
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f164]) ).
fof(f201,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f95]) ).
fof(f202,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(flattening,[],[f201]) ).
fof(f203,plain,
! [X0] :
( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
| ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f204,plain,
! [X0] :
( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X0)) )
| ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f203]) ).
fof(f205,plain,
( ( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(X0) != xi )
| ( ( ~ aSet0(sdtlpdtrp0(xN,xi))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,xi)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,xi)) )
& xi != sz00 ),
inference(ennf_transformation,[],[f96]) ).
fof(f206,definition,
! [X2,X0,X1] :
( sP0(X2,X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f207,definition,
! [X1,X0] :
( ! [X2] :
( X2 = sdtpldt0(X0,X1)
<=> sP0(X2,X0,X1) )
| ~ sP1(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f208,plain,
! [X0,X1] :
( sP1(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f112,f207,f206]) ).
fof(f209,definition,
! [X2,X0,X1] :
( sP2(X2,X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f210,definition,
! [X1,X0] :
( ! [X2] :
( X2 = sdtmndt0(X0,X1)
<=> sP2(X2,X0,X1) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f211,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f114,f210,f209]) ).
fof(f217,definition,
! [X0] :
( ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 ) )
| ~ sP8(X0) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f218,definition,
! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP8(X0)
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ sP9(X0) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f219,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( sP9(X0)
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(definition_folding,[],[f202,f218,f217]) ).
fof(f228,plain,
! [X1,X0] :
( ! [X2] :
( ( X2 = sdtpldt0(X0,X1)
| ~ sP0(X2,X0,X1) )
& ( sP0(X2,X0,X1)
| sdtpldt0(X0,X1) != X2 ) )
| ~ sP1(X1,X0) ),
inference(nnf_transformation,[],[f207]) ).
fof(f229,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtpldt0(X1,X0) = X2
| ~ sP0(X2,X1,X0) )
& ( sP0(X2,X1,X0)
| sdtpldt0(X1,X0) != X2 ) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f228]) ).
fof(f230,plain,
! [X2,X0,X1] :
( ( sP0(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ( ~ aElementOf0(X3,X0)
& X1 != X3 )
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ( ~ aElementOf0(X3,X0)
& X1 != X3 ) )
& ( ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP0(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f206]) ).
fof(f231,plain,
! [X2,X0,X1] :
( ( sP0(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ( ~ aElementOf0(X3,X0)
& X1 != X3 )
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ( ~ aElementOf0(X3,X0)
& X1 != X3 ) )
& ( ( aElement0(X3)
& ( aElementOf0(X3,X0)
| X3 = X1 ) )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP0(X2,X0,X1) ) ),
inference(flattening,[],[f230]) ).
fof(f232,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ~ aSet0(X0)
| ? [X3] :
( ( ~ aElement0(X3)
| ( ~ aElementOf0(X3,X1)
& X2 != X3 )
| ~ aElementOf0(X3,X0) )
& ( ( aElement0(X3)
& ( aElementOf0(X3,X1)
| X2 = X3 ) )
| aElementOf0(X3,X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ( ~ aElementOf0(X4,X1)
& X2 != X4 ) )
& ( ( aElement0(X4)
& ( aElementOf0(X4,X1)
| X2 = X4 ) )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f231]) ).
fof(f233,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ~ aSet0(X0)
| ( ( ~ aElement0(sK12(X0,X1,X2))
| ( ~ aElementOf0(sK12(X0,X1,X2),X1)
& sK12(X0,X1,X2) != X2 )
| ~ aElementOf0(sK12(X0,X1,X2),X0) )
& ( ( aElement0(sK12(X0,X1,X2))
& ( aElementOf0(sK12(X0,X1,X2),X1)
| sK12(X0,X1,X2) = X2 ) )
| aElementOf0(sK12(X0,X1,X2),X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ( ~ aElementOf0(X4,X1)
& X2 != X4 ) )
& ( ( aElement0(X4)
& ( aElementOf0(X4,X1)
| X2 = X4 ) )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X3,sK12(X0,X1,X2))],[f232]) ).
fof(f234,plain,
! [X1,X0] :
( ! [X2] :
( ( X2 = sdtmndt0(X0,X1)
| ~ sP2(X2,X0,X1) )
& ( sP2(X2,X0,X1)
| sdtmndt0(X0,X1) != X2 ) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f210]) ).
fof(f235,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtmndt0(X1,X0) = X2
| ~ sP2(X2,X1,X0) )
& ( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2 ) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f234]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ( sP2(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP2(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f209]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ( sP2(X2,X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3
| ~ aElementOf0(X3,X2) )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aElement0(X3)
| ~ aElementOf0(X3,X0)
| X1 = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,X0)
& X3 != X1 )
| ~ aElementOf0(X3,X2) ) ) )
| ~ sP2(X2,X0,X1) ) ),
inference(flattening,[],[f236]) ).
fof(f238,plain,
! [X0,X1,X2] :
( ( sP2(X0,X1,X2)
| ~ aSet0(X0)
| ? [X3] :
( ( ~ aElement0(X3)
| ~ aElementOf0(X3,X1)
| X2 = X3
| ~ aElementOf0(X3,X0) )
& ( ( aElement0(X3)
& aElementOf0(X3,X1)
& X2 != X3 )
| aElementOf0(X3,X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ~ aElementOf0(X4,X1)
| X2 = X4 )
& ( ( aElement0(X4)
& aElementOf0(X4,X1)
& X2 != X4 )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP2(X0,X1,X2) ) ),
inference(rectify,[],[f237]) ).
fof(f239,plain,
! [X0,X1,X2] :
( ( sP2(X0,X1,X2)
| ~ aSet0(X0)
| ( ( ~ aElement0(sK13(X0,X1,X2))
| ~ aElementOf0(sK13(X0,X1,X2),X1)
| sK13(X0,X1,X2) = X2
| ~ aElementOf0(sK13(X0,X1,X2),X0) )
& ( ( aElement0(sK13(X0,X1,X2))
& aElementOf0(sK13(X0,X1,X2),X1)
& sK13(X0,X1,X2) != X2 )
| aElementOf0(sK13(X0,X1,X2),X0) ) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( aElementOf0(X4,X0)
| ~ aElement0(X4)
| ~ aElementOf0(X4,X1)
| X2 = X4 )
& ( ( aElement0(X4)
& aElementOf0(X4,X1)
& X2 != X4 )
| ~ aElementOf0(X4,X0) ) ) )
| ~ sP2(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1,X2))],[f238]) ).
fof(f240,plain,
! [X0] :
( X0 = sz00
| ( aElementOf0(sK14(X0),szNzAzT0)
& szszuzczcdt0(sK14(X0)) = X0 )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X1,sK14(X0))],[f130]) ).
fof(f253,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ? [X2] :
( ( ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,X1) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| aElementOf0(X2,X1) ) ) )
& ( ( aSet0(X1)
& ! [X2] :
( ( aElementOf0(X2,X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| ~ aElementOf0(X2,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(nnf_transformation,[],[f162]) ).
fof(f254,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ? [X2] :
( ( ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,X1) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| aElementOf0(X2,X1) ) ) )
& ( ( aSet0(X1)
& ! [X2] :
( ( aElementOf0(X2,X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| ~ aElementOf0(X2,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f253]) ).
fof(f255,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ? [X2] :
( ( ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,X1) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| aElementOf0(X2,X1) ) ) )
& ( ( aSet0(X1)
& ! [X3] :
( ( aElementOf0(X3,X1)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X0) )
& ( ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X0) )
| ~ aElementOf0(X3,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(rectify,[],[f254]) ).
fof(f256,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ( ( ~ aElementOf0(sK18(X0,X1),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(sK18(X0,X1)),X0)
| ~ aElementOf0(sK18(X0,X1),X1) )
& ( ( aElementOf0(sK18(X0,X1),szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(sK18(X0,X1)),X0) )
| aElementOf0(sK18(X0,X1),X1) ) ) )
& ( ( aSet0(X1)
& ! [X3] :
( ( aElementOf0(X3,X1)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X0) )
& ( ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X0) )
| ~ aElementOf0(X3,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0,X1))],[f255]) ).
fof(f257,plain,
! [X0,X1] :
( ( ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| ( ~ aElementOf0(X0,slbdtrb0(X1))
& X0 != X1 ) )
& ( aElementOf0(X0,slbdtrb0(X1))
| X0 = X1
| ~ aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1))) ) )
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(nnf_transformation,[],[f165]) ).
fof(f258,plain,
! [X0,X1] :
( ( ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| ( ~ aElementOf0(X0,slbdtrb0(X1))
& X0 != X1 ) )
& ( aElementOf0(X0,slbdtrb0(X1))
| X0 = X1
| ~ aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1))) ) )
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f257]) ).
fof(f295,plain,
! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X2] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP8(X0)
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X4] :
( aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ sP9(X0) ),
inference(nnf_transformation,[],[f218]) ).
fof(f296,plain,
! [X0] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
& ! [X1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& sP8(X0)
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X2] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) )
| ~ sP9(X0) ),
inference(rectify,[],[f295]) ).
fof(f297,plain,
! [X0] :
( ! [X3] :
( ( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElement0(X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 )
| ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| ~ sP8(X0) ),
inference(nnf_transformation,[],[f217]) ).
fof(f298,plain,
! [X0] :
( ! [X3] :
( ( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElement0(X3)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X3 )
& ( ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X3 )
| ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| ~ sP8(X0) ),
inference(flattening,[],[f297]) ).
fof(f299,plain,
! [X0] :
( ! [X1] :
( ( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElement0(X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| szmzizndt0(sdtlpdtrp0(xN,X0)) = X1 )
& ( ( aElement0(X1)
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& szmzizndt0(sdtlpdtrp0(xN,X0)) != X1 )
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) )
| ~ sP8(X0) ),
inference(rectify,[],[f298]) ).
fof(f300,plain,
( aFunction0(xN)
& szDzozmdt0(xN) = szNzAzT0
& sdtlpdtrp0(xN,sz00) = xS
& ! [X0] :
( sP9(X0)
| ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ( ~ aElementOf0(sK39(X0),szNzAzT0)
& aElementOf0(sK39(X0),sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X1,sK39(X0))],[f219]) ).
fof(f301,plain,
( ( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(X0) != xi )
| ( ( ~ aSet0(sdtlpdtrp0(xN,xi))
| ( ~ aElementOf0(sK40,szNzAzT0)
& aElementOf0(sK40,sdtlpdtrp0(xN,xi)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,xi)) )
& xi != sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(X1,sK40)],[f205]) ).
fof(f302,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f317,plain,
! [X2,X0,X1] :
( sP0(X2,X1,X0)
| sdtpldt0(X1,X0) != X2
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f229]) ).
fof(f321,plain,
! [X2,X0,X1,X4] :
( aElementOf0(X4,X0)
| ~ aElement0(X4)
| X2 != X4
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f233]) ).
fof(f323,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f233]) ).
fof(f328,plain,
! [X0,X1] :
( sP1(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f329,plain,
! [X2,X0,X1] :
( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f235]) ).
fof(f331,plain,
! [X2,X0,X1,X4] :
( X2 != X4
| ~ aElementOf0(X4,X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f239]) ).
fof(f335,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f239]) ).
fof(f340,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f211]) ).
fof(f341,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f342,plain,
! [X0,X1] :
( aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| ~ aElement0(X0)
| ~ aSet0(X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f348,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f351,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f353,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(sK14(X0)) = X0
| sz00 = X0 ),
inference(cnf_transformation,[],[f240]) ).
fof(f354,plain,
! [X0] :
( aElementOf0(sK14(X0),szNzAzT0)
| sz00 = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f240]) ).
fof(f365,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f388,plain,
! [X0,X1] :
( aSet0(X1)
| slbdtrb0(X0) != X1
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f256]) ).
fof(f395,plain,
! [X0,X1] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| X0 != X1
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f258]) ).
fof(f502,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f504,plain,
! [X2,X0] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f505,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f506,plain,
! [X0] :
( ~ sP9(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f511,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f299]) ).
fof(f514,plain,
! [X0] :
( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f300]) ).
fof(f520,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[],[f82]) ).
fof(f521,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f204]) ).
fof(f522,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f204]) ).
fof(f523,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| aElementOf0(X1,szNzAzT0)
| ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f204]) ).
fof(f525,plain,
sz00 != xi,
inference(cnf_transformation,[],[f301]) ).
fof(f527,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(X0) != xi
| ~ aSet0(sdtlpdtrp0(xN,xi))
| aElementOf0(sK40,sdtlpdtrp0(xN,xi))
| ~ isCountable0(sdtlpdtrp0(xN,xi)) ),
inference(cnf_transformation,[],[f301]) ).
fof(f528,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(X0) != xi
| ~ aSet0(sdtlpdtrp0(xN,xi))
| ~ aElementOf0(sK40,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,xi)) ),
inference(cnf_transformation,[],[f301]) ).
fof(f532,plain,
! [X0,X1] :
( sP0(sdtpldt0(X1,X0),X1,X0)
| ~ sP1(X0,X1) ),
inference(equality_resolution,[],[f317]) ).
fof(f533,plain,
! [X0,X1,X4] :
( ~ sP0(X0,X1,X4)
| ~ aElement0(X4)
| aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f321]) ).
fof(f534,plain,
! [X0,X1] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ sP3(X0,X1) ),
inference(equality_resolution,[],[f329]) ).
fof(f535,plain,
! [X0,X1,X4] :
( ~ sP2(X0,X1,X4)
| ~ aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f331]) ).
fof(f541,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(slbdtrb0(X0)) ),
inference(equality_resolution,[],[f388]) ).
fof(f545,plain,
! [X1] :
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(equality_resolution,[],[f395]) ).
fof(f572,definition,
sF41 = sdtlpdtrp0(xN,xi),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f573,plain,
sdtlpdtrp0(xN,xi) = sF41,
inference(reorient_equations,[],[f572]) ).
fof(f574,plain,
! [X0] :
( szszuzczcdt0(X0) != xi
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSet0(sF41)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ isCountable0(sF41) ),
inference(definition_folding,[],[f528,f573,f573]) ).
fof(f575,plain,
! [X0] :
( szszuzczcdt0(X0) != xi
| ~ aElementOf0(X0,szNzAzT0)
| ~ aSet0(sF41)
| aElementOf0(sK40,sF41)
| ~ isCountable0(sF41) ),
inference(definition_folding,[],[f527,f573,f573,f573]) ).
fof(f577,plain,
! [X1] :
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(duplicate_literal_removal,[],[f545]) ).
fof(f621,plain,
! [X0] :
( aSet0(slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f351,f541]) ).
fof(f671,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElement0(X0)
| ~ aSet0(slbdtrb0(szszuzczcdt0(X0))) ),
inference(resolution,[],[f577,f302]) ).
fof(f674,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElement0(X0) ),
inference(forward_subsumption_resolution,[],[f671,f621]) ).
fof(f737,plain,
! [X0,X1] :
( aSet0(sdtpldt0(X1,X0))
| ~ sP1(X0,X1) ),
inference(resolution,[],[f532,f323]) ).
fof(f749,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtmndt0(X1,X0))
| ~ sP3(X0,X1) ),
inference(resolution,[],[f534,f535]) ).
fof(f750,plain,
! [X0,X1] :
( aSet0(sdtmndt0(X1,X0))
| ~ sP3(X0,X1) ),
inference(resolution,[],[f534,f335]) ).
fof(f875,plain,
( xi = szszuzczcdt0(sK14(xi))
| sz00 = xi ),
inference(resolution,[],[f353,f520]) ).
fof(f882,plain,
xi = szszuzczcdt0(sK14(xi)),
inference(forward_subsumption_resolution,[],[f875,f525]) ).
fof(f890,plain,
( ~ aElementOf0(sK14(xi),szNzAzT0)
| iLess0(sK14(xi),xi) ),
inference(superposition,[],[f365,f882]) ).
fof(f891,plain,
( isCountable0(sdtlpdtrp0(xN,xi))
| ~ sP9(sK14(xi)) ),
inference(superposition,[],[f502,f882]) ).
fof(f892,plain,
( aSet0(sdtlpdtrp0(xN,xi))
| ~ sP9(sK14(xi)) ),
inference(superposition,[],[f505,f882]) ).
fof(f893,plain,
( xi != xi
| ~ aElementOf0(sK14(xi),szNzAzT0)
| ~ aSet0(sF41)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ isCountable0(sF41) ),
inference(superposition,[],[f574,f882]) ).
fof(f894,plain,
( xi != xi
| ~ aElementOf0(sK14(xi),szNzAzT0)
| ~ aSet0(sF41)
| aElementOf0(sK40,sF41)
| ~ isCountable0(sF41) ),
inference(superposition,[],[f575,f882]) ).
fof(f902,plain,
( ~ aElementOf0(sK14(xi),szNzAzT0)
| ~ aSet0(sF41)
| aElementOf0(sK40,sF41)
| ~ isCountable0(sF41) ),
inference(trivial_inequality_removal,[],[f894]) ).
fof(f903,plain,
( ~ aElementOf0(sK14(xi),szNzAzT0)
| ~ aSet0(sF41)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ isCountable0(sF41) ),
inference(trivial_inequality_removal,[],[f893]) ).
fof(f905,plain,
( ~ sP9(sK14(xi))
| aSet0(sF41) ),
inference(forward_demodulation,[],[f892,f573]) ).
fof(f906,plain,
( ~ sP9(sK14(xi))
| isCountable0(sF41) ),
inference(forward_demodulation,[],[f891,f573]) ).
fof(f977,plain,
( iLess0(sK14(xi),xi)
| sz00 = xi
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[],[f890,f354]) ).
fof(f978,plain,
( iLess0(sK14(xi),xi)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f977,f525]) ).
fof(f979,plain,
iLess0(sK14(xi),xi),
inference(forward_subsumption_resolution,[],[f978,f520]) ).
fof(f1034,plain,
( ~ aSet0(sF41)
| aElementOf0(sK40,sF41)
| ~ isCountable0(sF41)
| sz00 = xi
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[],[f902,f354]) ).
fof(f1035,plain,
( ~ aSet0(sF41)
| aElementOf0(sK40,sF41)
| ~ isCountable0(sF41)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f1034,f525]) ).
fof(f1036,plain,
( aElementOf0(sK40,sF41)
| ~ aSet0(sF41)
| ~ isCountable0(sF41) ),
inference(forward_subsumption_resolution,[],[f1035,f520]) ).
fof(f1053,plain,
( ~ aSet0(sF41)
| ~ isCountable0(sF41)
| sF41 = sdtpldt0(sdtmndt0(sF41,sK40),sK40)
| ~ aSet0(sF41) ),
inference(resolution,[],[f1036,f341]) ).
fof(f1054,plain,
( ~ aSet0(sF41)
| ~ isCountable0(sF41)
| aElement0(sK40)
| ~ aSet0(sF41) ),
inference(resolution,[],[f1036,f302]) ).
fof(f1055,plain,
( ~ isCountable0(sF41)
| ~ aSet0(sF41)
| aElement0(sK40) ),
inference(duplicate_literal_removal,[],[f1054]) ).
fof(f1056,plain,
( ~ isCountable0(sF41)
| ~ aSet0(sF41)
| sF41 = sdtpldt0(sdtmndt0(sF41,sK40),sK40) ),
inference(duplicate_literal_removal,[],[f1053]) ).
fof(f1067,plain,
( ~ aSet0(sF41)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ isCountable0(sF41)
| sz00 = xi
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[],[f903,f354]) ).
fof(f1068,plain,
( ~ aSet0(sF41)
| ~ aElementOf0(sK40,szNzAzT0)
| ~ isCountable0(sF41)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f1067,f525]) ).
fof(f1069,plain,
( ~ aElementOf0(sK40,szNzAzT0)
| ~ aSet0(sF41)
| ~ isCountable0(sF41) ),
inference(forward_subsumption_resolution,[],[f1068,f520]) ).
fof(f1192,plain,
! [X0] :
( sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f514,f522]) ).
fof(f1195,plain,
! [X0] :
( sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ iLess0(X0,xi) ),
inference(duplicate_literal_removal,[],[f1192]) ).
fof(f1197,plain,
! [X0] :
( ~ iLess0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0)
| sP9(X0) ),
inference(forward_subsumption_resolution,[],[f1195,f521]) ).
fof(f1249,plain,
( szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK40),sK40)
| ~ aElement0(sK40)
| ~ aSet0(szNzAzT0)
| ~ aSet0(sF41)
| ~ isCountable0(sF41) ),
inference(resolution,[],[f342,f1069]) ).
fof(f1253,plain,
( szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK40),sK40)
| ~ aSet0(szNzAzT0)
| ~ aSet0(sF41)
| ~ isCountable0(sF41) ),
inference(forward_subsumption_resolution,[],[f1249,f1055]) ).
fof(f1279,plain,
( ~ isCountable0(sF41)
| ~ aSet0(sF41)
| szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK40),sK40) ),
inference(forward_subsumption_resolution,[],[f1253,f348]) ).
fof(f2551,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1)))
| ~ sP9(X1)
| aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ sP8(X1) ),
inference(resolution,[],[f504,f511]) ).
fof(f2566,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1)))
| ~ sP9(X1)
| aElementOf0(X0,sdtlpdtrp0(xN,X1)) ),
inference(forward_subsumption_resolution,[],[f2551,f506]) ).
fof(f4793,plain,
( ~ aElementOf0(sK14(xi),szNzAzT0)
| sP9(sK14(xi)) ),
inference(resolution,[],[f1197,f979]) ).
fof(f4795,plain,
( sP9(sK14(xi))
| sz00 = xi
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[],[f4793,f354]) ).
fof(f4799,plain,
( sP9(sK14(xi))
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f4795,f525]) ).
fof(f4800,plain,
sP9(sK14(xi)),
inference(forward_subsumption_resolution,[],[f4799,f520]) ).
fof(f4830,plain,
isCountable0(sF41),
inference(resolution,[],[f4800,f906]) ).
fof(f4831,plain,
aSet0(sF41),
inference(resolution,[],[f4800,f905]) ).
fof(f4881,plain,
( ~ aSet0(sF41)
| szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK40),sK40) ),
inference(resolution,[],[f4830,f1279]) ).
fof(f4882,plain,
( ~ aSet0(sF41)
| sF41 = sdtpldt0(sdtmndt0(sF41,sK40),sK40) ),
inference(resolution,[],[f4830,f1056]) ).
fof(f4883,plain,
( ~ aSet0(sF41)
| aElement0(sK40) ),
inference(resolution,[],[f4830,f1055]) ).
fof(f4885,plain,
aElement0(sK40),
inference(forward_subsumption_resolution,[],[f4883,f4831]) ).
fof(f4886,plain,
sF41 = sdtpldt0(sdtmndt0(sF41,sK40),sK40),
inference(forward_subsumption_resolution,[],[f4882,f4831]) ).
fof(f4887,plain,
szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK40),sK40),
inference(forward_subsumption_resolution,[],[f4881,f4831]) ).
fof(f4935,plain,
( sP0(sF41,sdtmndt0(sF41,sK40),sK40)
| ~ sP1(sK40,sdtmndt0(sF41,sK40)) ),
inference(superposition,[],[f532,f4886]) ).
fof(f4944,plain,
( ~ sP3(sK40,sdtpldt0(szNzAzT0,sK40))
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(superposition,[],[f749,f4887]) ).
fof(f4978,plain,
( ~ aElementOf0(sK40,szNzAzT0)
| ~ aSet0(sdtpldt0(szNzAzT0,sK40))
| ~ aElement0(sK40) ),
inference(resolution,[],[f4944,f340]) ).
fof(f4979,plain,
( ~ aSet0(sdtpldt0(szNzAzT0,sK40))
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f4978,f674]) ).
fof(f5023,plain,
( ~ sP1(sK40,szNzAzT0)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(resolution,[],[f4979,f737]) ).
fof(f5046,plain,
( ~ aElementOf0(sK40,szNzAzT0)
| ~ aSet0(szNzAzT0)
| ~ aElement0(sK40) ),
inference(resolution,[],[f5023,f328]) ).
fof(f5047,plain,
( ~ aElementOf0(sK40,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f5046,f674]) ).
fof(f5048,plain,
~ aElementOf0(sK40,szNzAzT0),
inference(forward_subsumption_resolution,[],[f5047,f348]) ).
fof(f5135,plain,
( ~ sP1(sK40,sdtmndt0(sF41,sK40))
| ~ aElement0(sK40)
| aElementOf0(sK40,sF41) ),
inference(resolution,[],[f4935,f533]) ).
fof(f5139,plain,
( ~ sP1(sK40,sdtmndt0(sF41,sK40))
| aElementOf0(sK40,sF41) ),
inference(forward_subsumption_resolution,[],[f5135,f4885]) ).
fof(f5167,plain,
( aElementOf0(sK40,sF41)
| ~ aSet0(sdtmndt0(sF41,sK40))
| ~ aElement0(sK40) ),
inference(resolution,[],[f5139,f328]) ).
fof(f5168,plain,
( ~ aSet0(sdtmndt0(sF41,sK40))
| aElementOf0(sK40,sF41) ),
inference(forward_subsumption_resolution,[],[f5167,f4885]) ).
fof(f5180,plain,
( ~ sP3(sK40,sF41)
| aElementOf0(sK40,sF41) ),
inference(resolution,[],[f5168,f750]) ).
fof(f5187,plain,
( aElementOf0(sK40,sF41)
| ~ aSet0(sF41)
| ~ aElement0(sK40) ),
inference(resolution,[],[f5180,f340]) ).
fof(f5188,plain,
( aElementOf0(sK40,sF41)
| ~ aElement0(sK40) ),
inference(forward_subsumption_resolution,[],[f5187,f4831]) ).
fof(f5189,plain,
aElementOf0(sK40,sF41),
inference(forward_subsumption_resolution,[],[f5188,f4885]) ).
fof(f8270,plain,
! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| ~ sP9(sK14(xi))
| aElementOf0(X0,sdtlpdtrp0(xN,sK14(xi))) ),
inference(superposition,[],[f2566,f882]) ).
fof(f8275,plain,
! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| aElementOf0(X0,sdtlpdtrp0(xN,sK14(xi))) ),
inference(forward_subsumption_resolution,[],[f8270,f4800]) ).
fof(f8295,plain,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,sK14(xi)))
| ~ aElementOf0(X0,sF41) ),
inference(forward_demodulation,[],[f8275,f573]) ).
fof(f8298,plain,
! [X0] :
( ~ aElementOf0(X0,sF41)
| aElementOf0(X0,szNzAzT0)
| ~ iLess0(sK14(xi),xi)
| ~ aElementOf0(sK14(xi),szNzAzT0) ),
inference(resolution,[],[f8295,f523]) ).
fof(f8308,plain,
! [X0] :
( ~ aElementOf0(sK14(xi),szNzAzT0)
| aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sF41) ),
inference(forward_subsumption_resolution,[],[f8298,f890]) ).
fof(f8313,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sF41)
| sz00 = xi
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[],[f8308,f354]) ).
fof(f8318,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sF41)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f8313,f525]) ).
fof(f8319,plain,
! [X0] :
( ~ aElementOf0(X0,sF41)
| aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f8318,f520]) ).
fof(f8328,plain,
aElementOf0(sK40,szNzAzT0),
inference(resolution,[],[f8319,f5189]) ).
fof(f8372,plain,
$false,
inference(forward_subsumption_resolution,[],[f8328,f5048]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM570+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n018.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 20:35:24 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.03/2.73 % (2702267)Will run a generic schedule for satisfiability detection.
% 16.03/2.73 % (2702277)% WARNING: option uhcvi not known.
% 16.03/2.73 % (2702277)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1692981228:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.03/2.73 % (2702276)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1127284598_2999 on theBenchmark for (2999ds/0Mi)
% 16.03/2.73 % (2702281)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2650116907:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.03/2.73 % (2702278)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=954179990:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.03/2.73 % (2702279)dis+10_1_sil=32000:sp=arity:random_seed=1613168886:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.03/2.73 % (2702280)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=159865129:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.03/2.73 % (2702282)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2667253474:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.03/2.73 % TRYING [1]
% 16.03/2.73 % TRYING [2]
% 16.03/2.73 % TRYING [3]
% 16.03/2.73 % TRYING [4]
% 16.03/2.73 % (2702279)Instruction limit reached!
% 16.03/2.73 % (2702279)------------------------------
% 16.03/2.73 % (2702279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.73 % (2702279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.73 % (2702279)CaDiCaL version: 2.1.3
% 16.03/2.73 % (2702279)Termination reason: Instruction limit
% 16.03/2.73 % (2702279)Termination phase: Saturation
% 16.03/2.73 % (2702279)Time elapsed: 0.068 s
% 16.03/2.73 % (2702279)Peak memory usage: 13 MB
% 16.03/2.73 % (2702279)Instructions burned: 103 (million)
% 16.03/2.73 % (2702280)Instruction limit reached!
% 16.03/2.73 % (2702280)------------------------------
% 16.03/2.73 % (2702280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.73 % (2702280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.73 % (2702280)CaDiCaL version: 2.1.3
% 16.03/2.73 % (2702280)Termination reason: Instruction limit
% 16.03/2.73 % (2702280)Termination phase: Saturation
% 16.03/2.73 % (2702280)Time elapsed: 0.074 s
% 16.03/2.73 % (2702280)Peak memory usage: 13 MB
% 16.03/2.73 % (2702280)Instructions burned: 118 (million)
% 16.03/2.73 % (2702281)Instruction limit reached!
% 16.03/2.73 % (2702281)------------------------------
% 16.03/2.73 % (2702281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.73 % (2702281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.73 % (2702281)CaDiCaL version: 2.1.3
% 16.03/2.73 % (2702281)Termination reason: Instruction limit
% 16.03/2.73 % (2702281)Termination phase: Saturation
% 16.03/2.73 % (2702281)Time elapsed: 0.081 s
% 16.03/2.73 % (2702281)Peak memory usage: 13 MB
% 16.03/2.73 % (2702281)Instructions burned: 132 (million)
% 16.03/2.73 % (2702290)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1353642398:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.03/2.73 % (2702291)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2479634604:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.03/2.73 % (2702292)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2937052496:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.03/2.73 % TRYING [1]
% 16.03/2.73 % (2702282)Instruction limit reached!
% 16.03/2.73 % (2702282)------------------------------
% 16.03/2.73 % (2702282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.73 % TRYING [2]
% 16.03/2.73 % (2702282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.73 % (2702282)CaDiCaL version: 2.1.3
% 16.03/2.73 % (2702282)Termination reason: Instruction limit
% 16.03/2.73 % (2702282)Termination phase: Saturation
% 16.03/2.73 % (2702282)Time elapsed: 0.109 s
% 16.03/2.73 % (2702282)Peak memory usage: 14 MB
% 16.03/2.73 % (2702282)Instructions burned: 159 (million)
% 16.03/2.73 % TRYING [3]
% 16.03/2.73 % (2702296)ott-21_1_sil=16000:fs=off:random_seed=1241628191:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.03/2.73 % TRYING [4]
% 16.03/2.73 % (2702291)Instruction limit reached!
% 16.03/2.73 % (2702291)------------------------------
% 16.03/2.73 % (2702291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.73 % (2702291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702291)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702291)Termination reason: Instruction limit
% 14.59/4.51 % (2702291)Termination phase: Saturation
% 14.59/4.51 % (2702291)Time elapsed: 0.088 s
% 14.59/4.51 % (2702291)Peak memory usage: 13 MB
% 14.59/4.51 % (2702291)Instructions burned: 131 (million)
% 14.59/4.51 % TRYING [5]
% 14.59/4.51 % (2702298)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3572560767:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 14.59/4.51 % TRYING [5]
% 14.59/4.51 % (2702296)Instruction limit reached!
% 14.59/4.51 % (2702296)------------------------------
% 14.59/4.51 % (2702296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702296)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702296)Termination reason: Instruction limit
% 14.59/4.51 % (2702296)Termination phase: Saturation
% 14.59/4.51 % (2702296)Time elapsed: 0.105 s
% 14.59/4.51 % (2702296)Peak memory usage: 13 MB
% 14.59/4.51 % (2702296)Instructions burned: 180 (million)
% 14.59/4.51 % (2702300)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2583444887:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 14.59/4.51 % TRYING [1]
% 14.59/4.51 % TRYING [2]
% 14.59/4.51 % TRYING [3]
% 14.59/4.51 % (2702290)Instruction limit reached!
% 14.59/4.51 % (2702290)------------------------------
% 14.59/4.51 % (2702290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702290)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702290)Termination reason: Instruction limit
% 14.59/4.51 % (2702290)Termination phase: Finite model building SAT solving
% 14.59/4.51 % (2702290)Time elapsed: 0.281 s
% 14.59/4.51 % (2702290)Peak memory usage: 37 MB
% 14.59/4.51 % (2702290)Instructions burned: 715 (million)
% 14.59/4.51 % (2702302)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1422930924:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 14.59/4.51 % (2702292)Instruction limit reached!
% 14.59/4.51 % (2702292)------------------------------
% 14.59/4.51 % (2702292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702292)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702292)Termination reason: Instruction limit
% 14.59/4.51 % (2702292)Termination phase: Saturation
% 14.59/4.51 % (2702292)Time elapsed: 0.318 s
% 14.59/4.51 % (2702292)Peak memory usage: 17 MB
% 14.59/4.51 % (2702292)Instructions burned: 685 (million)
% 14.59/4.51 % TRYING [4]
% 14.59/4.51 % (2702304)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1981929395:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 14.59/4.51 % (2702298)Instruction limit reached!
% 14.59/4.51 % (2702298)------------------------------
% 14.59/4.51 % (2702298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702298)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702298)Termination reason: Instruction limit
% 14.59/4.51 % (2702298)Termination phase: Saturation
% 14.59/4.51 % (2702298)Time elapsed: 0.337 s
% 14.59/4.51 % (2702298)Peak memory usage: 15 MB
% 14.59/4.51 % (2702298)Instructions burned: 477 (million)
% 14.59/4.51 % TRYING [6]
% 14.59/4.51 % (2702306)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2053154020:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 14.59/4.51 % (2702300)Instruction limit reached!
% 14.59/4.51 % (2702300)------------------------------
% 14.59/4.51 % (2702300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702300)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702300)Termination reason: Instruction limit
% 14.59/4.51 % (2702300)Termination phase: Finite model building SAT solving
% 14.59/4.51 % (2702300)Time elapsed: 0.385 s
% 14.59/4.51 % (2702300)Peak memory usage: 28 MB
% 14.59/4.51 % (2702300)Instructions burned: 865 (million)
% 14.59/4.51 % (2702308)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=108380105:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 14.59/4.51 % (2702304)Instruction limit reached!
% 14.59/4.51 % (2702304)------------------------------
% 14.59/4.51 % (2702304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702304)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702304)Termination reason: Instruction limit
% 14.59/4.51 % (2702304)Termination phase: Finite model building constraint generation
% 14.59/4.51 % (2702304)Time elapsed: 0.415 s
% 14.59/4.51 % (2702304)Peak memory usage: 106 MB
% 14.59/4.51 % (2702304)Instructions burned: 890 (million)
% 14.59/4.51 % (2702310)fmb+10_1_sil=64000:random_seed=1185850495:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 14.59/4.51 % TRYING [1]
% 14.59/4.51 % TRYING [2]
% 14.59/4.51 % TRYING [3]
% 14.59/4.51 % TRYING [4]
% 14.59/4.51 % (2702306)Instruction limit reached!
% 14.59/4.51 % (2702306)------------------------------
% 14.59/4.51 % (2702306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702306)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702306)Termination reason: Instruction limit
% 14.59/4.51 % (2702306)Termination phase: Saturation
% 14.59/4.51 % (2702306)Time elapsed: 0.451 s
% 14.59/4.51 % (2702306)Peak memory usage: 23 MB
% 14.59/4.51 % (2702306)Instructions burned: 692 (million)
% 14.59/4.51 % (2702312)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4017449773:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 14.59/4.51 % TRYING [20]
% 14.59/4.51 % (2702308)Instruction limit reached!
% 14.59/4.51 % (2702308)------------------------------
% 14.59/4.51 % (2702308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702308)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702308)Termination reason: Instruction limit
% 14.59/4.51 % (2702308)Termination phase: Saturation
% 14.59/4.51 % (2702308)Time elapsed: 0.472 s
% 14.59/4.51 % (2702308)Peak memory usage: 20 MB
% 14.59/4.51 % (2702308)Instructions burned: 879 (million)
% 14.59/4.51 % (2702302)Instruction limit reached!
% 14.59/4.51 % (2702302)------------------------------
% 14.59/4.51 % (2702302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702302)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702302)Termination reason: Instruction limit
% 14.59/4.51 % (2702302)Termination phase: Saturation
% 14.59/4.51 % (2702302)Time elapsed: 0.752 s
% 14.59/4.51 % (2702302)Peak memory usage: 26 MB
% 14.59/4.51 % (2702302)Instructions burned: 1179 (million)
% 14.59/4.51 % TRYING [5]
% 14.59/4.51 % (2702314)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=871453129:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 14.59/4.51 % (2702315)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2409989219:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 14.59/4.51 % TRYING [8]
% 14.59/4.51 % (2702314)Instruction limit reached!
% 14.59/4.51 % (2702314)------------------------------
% 14.59/4.51 % (2702314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702314)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702314)Termination reason: Instruction limit
% 14.59/4.51 % (2702314)Termination phase: Finite model building constraint generation
% 14.59/4.51 % (2702314)Time elapsed: 0.307 s
% 14.59/4.51 % (2702314)Peak memory usage: 56 MB
% 14.59/4.51 % (2702314)Instructions burned: 923 (million)
% 14.59/4.51 % (2702318)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=775890830:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 14.59/4.51 % TRYING [6]
% 14.59/4.51 % TRYING [7]
% 14.59/4.51 % (2702318)Instruction limit reached!
% 14.59/4.51 % (2702318)------------------------------
% 14.59/4.51 % (2702318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702318)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702318)Termination reason: Instruction limit
% 14.59/4.51 % (2702318)Termination phase: Saturation
% 14.59/4.51 % (2702318)Time elapsed: 0.718 s
% 14.59/4.51 % (2702318)Peak memory usage: 25 MB
% 14.59/4.51 % (2702318)Instructions burned: 1472 (million)
% 14.59/4.51 % (2702320)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1061754277:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 14.59/4.51 % (2702320)Cannot represent all propositional literals internally
% 14.59/4.51 % (2702320)Refutation not found, incomplete strategy
% 14.59/4.51 % (2702320)------------------------------
% 14.59/4.51 % (2702320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702320)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702320)Termination reason: Refutation not found, incomplete strategy
% 14.59/4.51 % (2702320)Time elapsed: 0.023 s
% 14.59/4.51 % (2702320)Peak memory usage: 11 MB
% 14.59/4.51 % (2702320)Instructions burned: 45 (million)
% 14.59/4.51 % (2702320)------------------------------
% 14.59/4.51 % (2702320)------------------------------
% 14.59/4.51 % (2702322)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3027417094:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 14.59/4.51 % TRYING [16]
% 14.59/4.51 % TRYING [7]
% 14.59/4.51 % (2702322)Instruction limit reached!
% 14.59/4.51 % (2702322)------------------------------
% 14.59/4.51 % (2702322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702322)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702322)Termination reason: Instruction limit
% 14.59/4.51 % (2702322)Termination phase: Finite model building constraint generation
% 14.59/4.51 % (2702322)Time elapsed: 0.773 s
% 14.59/4.51 % (2702322)Peak memory usage: 127 MB
% 14.59/4.51 % (2702322)Instructions burned: 2176 (million)
% 14.59/4.51 % (2702324)ott-2_1_sil=16000:newcnf=on:random_seed=3183097299:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi)
% 14.59/4.51 % (2702324)Instruction limit reached!
% 14.59/4.51 % (2702324)------------------------------
% 14.59/4.51 % (2702324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.51 % (2702324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.51 % (2702324)CaDiCaL version: 2.1.3
% 14.59/4.51 % (2702324)Termination reason: Instruction limit
% 14.59/4.51 % (2702324)Termination phase: Saturation
% 14.59/4.51 % (2702324)Time elapsed: 0.562 s
% 14.59/4.51 % (2702324)Peak memory usage: 21 MB
% 14.59/4.51 % (2702324)Instructions burned: 870 (million)
% 14.59/4.51 % (2702326)ott+10_1_sil=32000:tgt=ground:random_seed=1975553943:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 14.59/4.51 % (2702326) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2702267-2702326"...
% 14.59/4.51 % (2702326)...printing done.
% 14.59/4.51 % (2702326)Refutation found. Thanks to Tanya!
% 14.59/4.51 % SZS status Theorem for theBenchmark
% 14.59/4.51 % SZS output start Proof for theBenchmark
% See solution above
% 14.59/4.52 % (2702326)------------------------------
% 14.59/4.52 % (2702326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/4.52 % (2702326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/4.52 % (2702326)CaDiCaL version: 2.1.3
% 14.59/4.52 % (2702326)Termination reason: Refutation
% 14.59/4.52 % (2702326)Time elapsed: 0.290 s
% 14.59/4.52 % (2702326)Peak memory usage: 17 MB
% 14.59/4.52 % (2702326)Instructions burned: 453 (million)
% 14.59/4.52 % (2702267)Success in time 4.088 s
% 14.59/4.52 % Vampire exiting
%------------------------------------------------------------------------------