%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM569+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 : 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 : Tue Sep 29 12:24:51 PM UTC 2026
% Result : Theorem 23.02s 14.82s
% Output : Refutation 23.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 21
% Syntax : Number of formulae : 192 ( 12 unt; 7 def)
% Number of atoms : 1020 ( 194 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 1258 ( 430 ~; 478 |; 278 &)
% ( 30 <=>; 42 =>; 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 : 301 ( 280 !; 21 ?)
% 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(f75,axiom,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,xS)
=> aElementOf0(X0,szNzAzT0) )
& aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3435) ).
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,conjecture,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( iLess0(X1,X0)
=> ( aSet0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> aElementOf0(X2,szNzAzT0) )
& aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X1)) ) ) )
=> ( ( ( 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__) ).
fof(f83,negated_conjecture,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( iLess0(X1,X0)
=> ( aSet0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> aElementOf0(X2,szNzAzT0) )
& aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X1)) ) ) )
=> ( ( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f82]) ).
fof(f93,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(f94,plain,
~ ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( iLess0(X1,X0)
=> ( aSet0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
=> aElementOf0(X2,szNzAzT0) )
& aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X1)) ) ) )
=> ( ( ( aSet0(sdtlpdtrp0(xN,X0))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X0))
=> aElementOf0(X3,szNzAzT0) ) )
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
& isCountable0(sdtlpdtrp0(xN,X0)) ) ) ),
inference(rectify,[],[f83]) ).
fof(f95,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f109,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(f110,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,[],[f109]) ).
fof(f111,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(f112,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,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ! [X1] :
( sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f114,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| aElementOf0(X0,X1)
| ~ aElement0(X0)
| ~ aSet0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f115,plain,
! [X0,X1] :
( sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| aElementOf0(X0,X1)
| ~ aElement0(X0)
| ~ aSet0(X1) ),
inference(flattening,[],[f114]) ).
fof(f124,plain,
! [X0] :
( ( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
& szszuzczcdt0(X0) != sz00 )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f127,plain,
! [X0] :
( X0 = sz00
| ? [X1] :
( aElementOf0(X1,szNzAzT0)
& X0 = szszuzczcdt0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f128,plain,
! [X0] :
( X0 = sz00
| ? [X1] :
( aElementOf0(X1,szNzAzT0)
& X0 = szszuzczcdt0(X1) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f127]) ).
fof(f142,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f160,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(f162,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(f163,plain,
! [X0,X1] :
( ( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
<=> ( aElementOf0(X0,slbdtrb0(X1))
| X0 = X1 ) )
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f162]) ).
fof(f194,plain,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) )
& aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
inference(ennf_transformation,[],[f75]) ).
fof(f199,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,[],[f93]) ).
fof(f200,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,[],[f199]) ).
fof(f201,plain,
? [X0] :
( ( ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X3] :
( ~ aElementOf0(X3,szNzAzT0)
& aElementOf0(X3,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0)) )
& ! [X1] :
( ( aSet0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X1)) )
& aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X1)) )
| ~ iLess0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0) )
& aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f202,plain,
? [X0] :
( ( ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X3] :
( ~ aElementOf0(X3,szNzAzT0)
& aElementOf0(X3,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0)) )
& ! [X1] :
( ( aSet0(sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X1)) )
& aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X1)) )
| ~ iLess0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0) )
& aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f201]) ).
fof(f203,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(f204,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(f205,plain,
! [X0,X1] :
( sP1(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f110,f204,f203]) ).
fof(f206,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(f207,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(f208,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(definition_folding,[],[f112,f207,f206]) ).
fof(f214,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(f215,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(f216,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,[],[f200,f215,f214]) ).
fof(f225,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,[],[f204]) ).
fof(f226,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,[],[f225]) ).
fof(f227,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,[],[f203]) ).
fof(f228,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,[],[f227]) ).
fof(f229,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,[],[f228]) ).
fof(f230,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))],[f229]) ).
fof(f231,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,[],[f207]) ).
fof(f232,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,[],[f231]) ).
fof(f233,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,[],[f206]) ).
fof(f234,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,[],[f233]) ).
fof(f235,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,[],[f234]) ).
fof(f236,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))],[f235]) ).
fof(f237,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))],[f128]) ).
fof(f250,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,[],[f160]) ).
fof(f251,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,[],[f250]) ).
fof(f252,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,[],[f251]) ).
fof(f253,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))],[f252]) ).
fof(f254,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,[],[f163]) ).
fof(f255,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,[],[f254]) ).
fof(f292,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,[],[f215]) ).
fof(f293,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,[],[f292]) ).
fof(f294,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,[],[f214]) ).
fof(f295,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,[],[f294]) ).
fof(f296,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,[],[f295]) ).
fof(f297,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))],[f216]) ).
fof(f298,plain,
? [X0] :
( ( ( ( ~ aSet0(sdtlpdtrp0(xN,X0))
| ? [X1] :
( ~ aElementOf0(X1,szNzAzT0)
& aElementOf0(X1,sdtlpdtrp0(xN,X0)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,X0)) )
& ! [X2] :
( ( aSet0(sdtlpdtrp0(xN,X2))
& ! [X3] :
( aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X2)) )
& aSubsetOf0(sdtlpdtrp0(xN,X2),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X2)) )
| ~ iLess0(X2,X0)
| ~ aElementOf0(X2,szNzAzT0) )
& aElementOf0(X0,szNzAzT0) ),
inference(rectify,[],[f202]) ).
fof(f299,plain,
( ( ( ( ~ aSet0(sdtlpdtrp0(xN,sK40))
| ( ~ aElementOf0(sK41,szNzAzT0)
& aElementOf0(sK41,sdtlpdtrp0(xN,sK40)) ) )
& ~ aSubsetOf0(sdtlpdtrp0(xN,sK40),szNzAzT0) )
| ~ isCountable0(sdtlpdtrp0(xN,sK40)) )
& ! [X2] :
( ( aSet0(sdtlpdtrp0(xN,X2))
& ! [X3] :
( aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X2)) )
& aSubsetOf0(sdtlpdtrp0(xN,X2),szNzAzT0)
& isCountable0(sdtlpdtrp0(xN,X2)) )
| ~ iLess0(X2,sK40)
| ~ aElementOf0(X2,szNzAzT0) )
& aElementOf0(sK40,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40,sK41]),skolemize(X0,sK40),skolemize(X1,sK41)],[f298]) ).
fof(f300,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f315,plain,
! [X2,X0,X1] :
( sP0(X2,X1,X0)
| sdtpldt0(X1,X0) != X2
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f226]) ).
fof(f319,plain,
! [X2,X0,X1,X4] :
( aElementOf0(X4,X0)
| ~ aElement0(X4)
| X2 != X4
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f230]) ).
fof(f321,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f326,plain,
! [X0,X1] :
( sP1(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f205]) ).
fof(f327,plain,
! [X2,X0,X1] :
( sP2(X2,X1,X0)
| sdtmndt0(X1,X0) != X2
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f232]) ).
fof(f329,plain,
! [X2,X0,X1,X4] :
( X2 != X4
| ~ aElementOf0(X4,X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f236]) ).
fof(f333,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| aSet0(X0) ),
inference(cnf_transformation,[],[f236]) ).
fof(f338,plain,
! [X0,X1] :
( sP3(X1,X0)
| ~ aSet0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f339,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f340,plain,
! [X0,X1] :
( aElementOf0(X0,X1)
| sdtmndt0(sdtpldt0(X1,X0),X0) = X1
| ~ aElement0(X0)
| ~ aSet0(X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f346,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f349,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f351,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(sK14(X0)) = X0
| sz00 = X0 ),
inference(cnf_transformation,[],[f237]) ).
fof(f352,plain,
! [X0] :
( aElementOf0(sK14(X0),szNzAzT0)
| sz00 = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f363,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f386,plain,
! [X0,X1] :
( aSet0(X1)
| slbdtrb0(X0) != X1
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f253]) ).
fof(f393,plain,
! [X0,X1] :
( aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))
| X0 != X1
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f446,plain,
isCountable0(xS),
inference(cnf_transformation,[],[f194]) ).
fof(f447,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[],[f194]) ).
fof(f500,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f502,plain,
! [X2,X0] :
( aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f503,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f504,plain,
! [X0] :
( ~ sP9(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f509,plain,
! [X0,X1] :
( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f512,plain,
! [X0] :
( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f515,plain,
xS = sdtlpdtrp0(xN,sz00),
inference(cnf_transformation,[],[f297]) ).
fof(f518,plain,
aElementOf0(sK40,szNzAzT0),
inference(cnf_transformation,[],[f299]) ).
fof(f519,plain,
! [X2] :
( isCountable0(sdtlpdtrp0(xN,X2))
| ~ iLess0(X2,sK40)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(cnf_transformation,[],[f299]) ).
fof(f520,plain,
! [X2] :
( aSubsetOf0(sdtlpdtrp0(xN,X2),szNzAzT0)
| ~ iLess0(X2,sK40)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(cnf_transformation,[],[f299]) ).
fof(f521,plain,
! [X2,X3] :
( ~ aElementOf0(X3,sdtlpdtrp0(xN,X2))
| aElementOf0(X3,szNzAzT0)
| ~ iLess0(X2,sK40)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(cnf_transformation,[],[f299]) ).
fof(f523,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,sK40),szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,sK40)) ),
inference(cnf_transformation,[],[f299]) ).
fof(f524,plain,
( ~ aSet0(sdtlpdtrp0(xN,sK40))
| aElementOf0(sK41,sdtlpdtrp0(xN,sK40))
| ~ isCountable0(sdtlpdtrp0(xN,sK40)) ),
inference(cnf_transformation,[],[f299]) ).
fof(f525,plain,
( ~ aSet0(sdtlpdtrp0(xN,sK40))
| ~ aElementOf0(sK41,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,sK40)) ),
inference(cnf_transformation,[],[f299]) ).
fof(f529,plain,
! [X0,X1] :
( sP0(sdtpldt0(X1,X0),X1,X0)
| ~ sP1(X0,X1) ),
inference(equality_resolution,[],[f315]) ).
fof(f530,plain,
! [X0,X1,X4] :
( ~ sP0(X0,X1,X4)
| ~ aElement0(X4)
| aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f319]) ).
fof(f531,plain,
! [X0,X1] :
( sP2(sdtmndt0(X1,X0),X1,X0)
| ~ sP3(X0,X1) ),
inference(equality_resolution,[],[f327]) ).
fof(f532,plain,
! [X0,X1,X4] :
( ~ sP2(X0,X1,X4)
| ~ aElementOf0(X4,X0) ),
inference(equality_resolution,[],[f329]) ).
fof(f538,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(slbdtrb0(X0)) ),
inference(equality_resolution,[],[f386]) ).
fof(f542,plain,
! [X1] :
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(equality_resolution,[],[f393]) ).
fof(f569,definition,
sF42 = sdtlpdtrp0(xN,sK40),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f570,plain,
sdtlpdtrp0(xN,sK40) = sF42,
inference(reorient_equations,[],[f569]) ).
fof(f571,plain,
( ~ aElementOf0(sK41,szNzAzT0)
| ~ aSet0(sF42)
| ~ isCountable0(sF42) ),
inference(definition_folding,[],[f525,f570,f570]) ).
fof(f572,plain,
( aElementOf0(sK41,sF42)
| ~ aSet0(sF42)
| ~ isCountable0(sF42) ),
inference(definition_folding,[],[f524,f570,f570,f570]) ).
fof(f573,plain,
( ~ aSubsetOf0(sF42,szNzAzT0)
| ~ isCountable0(sF42) ),
inference(definition_folding,[],[f523,f570,f570]) ).
fof(f574,plain,
! [X1] :
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(duplicate_literal_removal,[],[f542]) ).
fof(f620,plain,
( aElement0(sK41)
| ~ aSet0(sF42)
| ~ aSet0(sF42)
| ~ isCountable0(sF42) ),
inference(resolution,[],[f300,f572]) ).
fof(f621,plain,
( ~ isCountable0(sF42)
| ~ aSet0(sF42)
| aElement0(sK41) ),
inference(duplicate_literal_removal,[],[f620]) ).
fof(f632,plain,
! [X0] :
( aSet0(slbdtrb0(szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f349,f538]) ).
fof(f680,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElement0(X0)
| ~ aSet0(slbdtrb0(szszuzczcdt0(X0))) ),
inference(resolution,[],[f574,f300]) ).
fof(f683,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElement0(X0) ),
inference(forward_subsumption_resolution,[],[f680,f632]) ).
fof(f759,plain,
! [X0,X1] :
( aSet0(sdtpldt0(X1,X0))
| ~ sP1(X0,X1) ),
inference(resolution,[],[f529,f321]) ).
fof(f766,plain,
! [X0,X1] :
( aSet0(sdtmndt0(X1,X0))
| ~ sP3(X0,X1) ),
inference(resolution,[],[f531,f333]) ).
fof(f909,plain,
( sK40 = szszuzczcdt0(sK14(sK40))
| sz00 = sK40 ),
inference(resolution,[],[f351,f518]) ).
fof(f918,plain,
( ~ aElementOf0(sK14(sK40),szNzAzT0)
| iLess0(sK14(sK40),sK40)
| sz00 = sK40 ),
inference(superposition,[],[f363,f909]) ).
fof(f919,plain,
( isCountable0(sdtlpdtrp0(xN,sK40))
| ~ sP9(sK14(sK40))
| sz00 = sK40 ),
inference(superposition,[],[f500,f909]) ).
fof(f920,plain,
( aSet0(sdtlpdtrp0(xN,sK40))
| ~ sP9(sK14(sK40))
| sz00 = sK40 ),
inference(superposition,[],[f503,f909]) ).
fof(f922,plain,
( ~ sP9(sK14(sK40))
| aSet0(sF42)
| sz00 = sK40 ),
inference(forward_demodulation,[],[f920,f570]) ).
fof(f923,plain,
( ~ sP9(sK14(sK40))
| isCountable0(sF42)
| sz00 = sK40 ),
inference(forward_demodulation,[],[f919,f570]) ).
fof(f1001,plain,
( iLess0(sK14(sK40),sK40)
| sz00 = sK40
| sz00 = sK40
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(resolution,[],[f918,f352]) ).
fof(f1002,plain,
( iLess0(sK14(sK40),sK40)
| sz00 = sK40
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(duplicate_literal_removal,[],[f1001]) ).
fof(f1003,plain,
( iLess0(sK14(sK40),sK40)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f1002,f518]) ).
fof(f1025,plain,
( sF42 = sdtpldt0(sdtmndt0(sF42,sK41),sK41)
| ~ aSet0(sF42)
| ~ aSet0(sF42)
| ~ isCountable0(sF42) ),
inference(resolution,[],[f339,f572]) ).
fof(f1026,plain,
( ~ isCountable0(sF42)
| ~ aSet0(sF42)
| sF42 = sdtpldt0(sdtmndt0(sF42,sK41),sK41) ),
inference(duplicate_literal_removal,[],[f1025]) ).
fof(f1212,plain,
! [X0] :
( sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ iLess0(X0,sK40)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[],[f512,f520]) ).
fof(f1215,plain,
! [X0] :
( sP9(X0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ iLess0(X0,sK40) ),
inference(duplicate_literal_removal,[],[f1212]) ).
fof(f1217,plain,
! [X0] :
( ~ iLess0(X0,sK40)
| ~ aElementOf0(X0,szNzAzT0)
| sP9(X0) ),
inference(forward_subsumption_resolution,[],[f1215,f519]) ).
fof(f1220,plain,
( ~ aElementOf0(sK14(sK40),szNzAzT0)
| sP9(sK14(sK40))
| sz00 = sK40 ),
inference(resolution,[],[f1217,f1003]) ).
fof(f1251,plain,
( szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK41),sK41)
| ~ aElement0(sK41)
| ~ aSet0(szNzAzT0)
| ~ aSet0(sF42)
| ~ isCountable0(sF42) ),
inference(resolution,[],[f340,f571]) ).
fof(f1255,plain,
( szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK41),sK41)
| ~ aSet0(szNzAzT0)
| ~ aSet0(sF42)
| ~ isCountable0(sF42) ),
inference(forward_subsumption_resolution,[],[f1251,f621]) ).
fof(f1280,plain,
( ~ isCountable0(sF42)
| ~ aSet0(sF42)
| szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK41),sK41) ),
inference(forward_subsumption_resolution,[],[f1255,f346]) ).
fof(f1283,plain,
( sP9(sK14(sK40))
| sz00 = sK40
| sz00 = sK40
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(resolution,[],[f1220,f352]) ).
fof(f1285,plain,
( sP9(sK14(sK40))
| sz00 = sK40
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(duplicate_literal_removal,[],[f1283]) ).
fof(f1287,plain,
( sP9(sK14(sK40))
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f1285,f518]) ).
fof(f1296,plain,
( sz00 = sK40
| isCountable0(sF42)
| sz00 = sK40 ),
inference(resolution,[],[f1287,f923]) ).
fof(f1297,plain,
( sz00 = sK40
| aSet0(sF42)
| sz00 = sK40 ),
inference(resolution,[],[f1287,f922]) ).
fof(f1299,plain,
( aSet0(sF42)
| sz00 = sK40 ),
inference(duplicate_literal_removal,[],[f1297]) ).
fof(f1300,plain,
( isCountable0(sF42)
| sz00 = sK40 ),
inference(duplicate_literal_removal,[],[f1296]) ).
fof(f1319,plain,
( sz00 = sK40
| ~ aSet0(sF42)
| sF42 = sdtpldt0(sdtmndt0(sF42,sK41),sK41) ),
inference(resolution,[],[f1300,f1026]) ).
fof(f1320,plain,
( sz00 = sK40
| ~ aSet0(sF42)
| aElement0(sK41) ),
inference(resolution,[],[f1300,f621]) ).
fof(f1323,plain,
( aElement0(sK41)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f1320,f1299]) ).
fof(f1324,plain,
( sF42 = sdtpldt0(sdtmndt0(sF42,sK41),sK41)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f1319,f1299]) ).
fof(f1438,plain,
( sP0(sF42,sdtmndt0(sF42,sK41),sK41)
| ~ sP1(sK41,sdtmndt0(sF42,sK41))
| sz00 = sK40 ),
inference(superposition,[],[f529,f1324]) ).
fof(f1455,plain,
( ~ aSet0(sF42)
| szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK41),sK41)
| sz00 = sK40 ),
inference(resolution,[],[f1280,f1300]) ).
fof(f1456,plain,
( szNzAzT0 = sdtmndt0(sdtpldt0(szNzAzT0,sK41),sK41)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f1455,f1299]) ).
fof(f1488,plain,
( sP2(szNzAzT0,sdtpldt0(szNzAzT0,sK41),sK41)
| ~ sP3(sK41,sdtpldt0(szNzAzT0,sK41))
| sz00 = sK40 ),
inference(superposition,[],[f531,f1456]) ).
fof(f2491,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1)))
| ~ sP9(X1)
| aElementOf0(X0,sdtlpdtrp0(xN,X1))
| ~ sP8(X1) ),
inference(resolution,[],[f502,f509]) ).
fof(f2506,plain,
! [X0,X1] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1)))
| ~ sP9(X1)
| aElementOf0(X0,sdtlpdtrp0(xN,X1)) ),
inference(forward_subsumption_resolution,[],[f2491,f504]) ).
fof(f3318,plain,
( ~ sP1(sK41,sdtmndt0(sF42,sK41))
| sz00 = sK40
| ~ aElement0(sK41)
| aElementOf0(sK41,sF42) ),
inference(resolution,[],[f1438,f530]) ).
fof(f3322,plain,
( ~ sP1(sK41,sdtmndt0(sF42,sK41))
| sz00 = sK40
| aElementOf0(sK41,sF42) ),
inference(forward_subsumption_resolution,[],[f3318,f1323]) ).
fof(f3331,plain,
( sz00 = sK40
| aElementOf0(sK41,sF42)
| ~ aSet0(sdtmndt0(sF42,sK41))
| ~ aElement0(sK41) ),
inference(resolution,[],[f3322,f326]) ).
fof(f3332,plain,
( ~ aSet0(sdtmndt0(sF42,sK41))
| aElementOf0(sK41,sF42)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f3331,f1323]) ).
fof(f3577,plain,
( ~ sP3(sK41,sdtpldt0(szNzAzT0,sK41))
| sz00 = sK40
| ~ aElementOf0(sK41,szNzAzT0) ),
inference(resolution,[],[f1488,f532]) ).
fof(f3580,plain,
( sz00 = sK40
| ~ aElementOf0(sK41,szNzAzT0)
| ~ aSet0(sdtpldt0(szNzAzT0,sK41))
| ~ aElement0(sK41) ),
inference(resolution,[],[f3577,f338]) ).
fof(f3581,plain,
( ~ aSet0(sdtpldt0(szNzAzT0,sK41))
| ~ aElementOf0(sK41,szNzAzT0)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f3580,f1323]) ).
fof(f4979,plain,
( ~ sP1(sK41,szNzAzT0)
| ~ aElementOf0(sK41,szNzAzT0)
| sz00 = sK40 ),
inference(resolution,[],[f759,f3581]) ).
fof(f4986,plain,
( ~ aElementOf0(sK41,szNzAzT0)
| sz00 = sK40
| ~ aSet0(szNzAzT0)
| ~ aElement0(sK41) ),
inference(resolution,[],[f4979,f326]) ).
fof(f4987,plain,
( ~ aElementOf0(sK41,szNzAzT0)
| sz00 = sK40
| ~ aSet0(szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f4986,f683]) ).
fof(f4988,plain,
( ~ aElementOf0(sK41,szNzAzT0)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f4987,f346]) ).
fof(f4990,plain,
( ~ sP3(sK41,sF42)
| aElementOf0(sK41,sF42)
| sz00 = sK40 ),
inference(resolution,[],[f766,f3332]) ).
fof(f5006,plain,
( aElementOf0(sK41,sF42)
| sz00 = sK40
| ~ aSet0(sF42)
| ~ aElement0(sK41) ),
inference(resolution,[],[f4990,f338]) ).
fof(f5007,plain,
( aElementOf0(sK41,sF42)
| sz00 = sK40
| ~ aElement0(sK41) ),
inference(forward_subsumption_resolution,[],[f5006,f1299]) ).
fof(f5008,plain,
( aElementOf0(sK41,sF42)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f5007,f1323]) ).
fof(f8991,plain,
! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,sK40))
| ~ sP9(sK14(sK40))
| aElementOf0(X0,sdtlpdtrp0(xN,sK14(sK40)))
| sz00 = sK40 ),
inference(superposition,[],[f2506,f909]) ).
fof(f8994,plain,
! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,sK40))
| aElementOf0(X0,sdtlpdtrp0(xN,sK14(sK40)))
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f8991,f1287]) ).
fof(f9017,plain,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,sK14(sK40)))
| ~ aElementOf0(X0,sF42)
| sz00 = sK40 ),
inference(forward_demodulation,[],[f8994,f570]) ).
fof(f10325,plain,
! [X0] :
( ~ aElementOf0(X0,sF42)
| sz00 = sK40
| aElementOf0(X0,szNzAzT0)
| ~ iLess0(sK14(sK40),sK40)
| ~ aElementOf0(sK14(sK40),szNzAzT0) ),
inference(resolution,[],[f9017,f521]) ).
fof(f10336,plain,
! [X0] :
( ~ aElementOf0(sK14(sK40),szNzAzT0)
| sz00 = sK40
| aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sF42) ),
inference(forward_subsumption_resolution,[],[f10325,f918]) ).
fof(f19131,plain,
! [X0] :
( sz00 = sK40
| aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sF42)
| sz00 = sK40
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(resolution,[],[f10336,f352]) ).
fof(f19136,plain,
! [X0] :
( sz00 = sK40
| aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,sF42)
| ~ aElementOf0(sK40,szNzAzT0) ),
inference(duplicate_literal_removal,[],[f19131]) ).
fof(f19141,plain,
! [X0] :
( ~ aElementOf0(X0,sF42)
| aElementOf0(X0,szNzAzT0)
| sz00 = sK40 ),
inference(forward_subsumption_resolution,[],[f19136,f518]) ).
fof(f19278,plain,
( aElementOf0(sK41,szNzAzT0)
| sz00 = sK40
| sz00 = sK40 ),
inference(resolution,[],[f19141,f5008]) ).
fof(f19280,plain,
( aElementOf0(sK41,szNzAzT0)
| sz00 = sK40 ),
inference(duplicate_literal_removal,[],[f19278]) ).
fof(f19289,plain,
sz00 = sK40,
inference(forward_subsumption_resolution,[],[f19280,f4988]) ).
fof(f19318,plain,
sdtlpdtrp0(xN,sz00) = sF42,
inference(superposition,[],[f570,f19289]) ).
fof(f19650,plain,
xS = sF42,
inference(forward_demodulation,[],[f19318,f515]) ).
fof(f19892,plain,
( ~ aSubsetOf0(xS,szNzAzT0)
| ~ isCountable0(xS) ),
inference(superposition,[],[f573,f19650]) ).
fof(f20067,plain,
~ isCountable0(xS),
inference(forward_subsumption_resolution,[],[f19892,f447]) ).
fof(f20087,plain,
$false,
inference(forward_subsumption_resolution,[],[f20067,f446]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM569+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/10.38 % Computer : n011.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Sun Sep 27 20:33:11 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/10.41 Running first-order model finding
% 0.13/10.41 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
% 13.98/12.45 % (2738905)Will run a generic schedule for satisfiability detection.
% 13.98/12.45 % (2738916)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3625414395:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.98/12.45 % (2738911)% WARNING: option uhcvi not known.
% 13.98/12.45 % (2738911)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2911606992:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.98/12.45 % (2738910)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1981190298_2999 on theBenchmark for (2999ds/0Mi)
% 13.98/12.45 % (2738912)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2715102749:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.98/12.45 % (2738913)dis+10_1_sil=32000:sp=arity:random_seed=1514689446:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.98/12.45 % (2738914)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3213356271:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.98/12.45 % (2738915)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1527492787:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.98/12.45 % TRYING [1]
% 13.98/12.45 % TRYING [2]
% 13.98/12.45 % TRYING [3]
% 13.98/12.45 % (2738916)Instruction limit reached!
% 13.98/12.45 % (2738916)------------------------------
% 13.98/12.45 % (2738916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/12.45 % (2738916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/12.45 % (2738916)CaDiCaL version: 2.1.3
% 13.98/12.45 % (2738916)Termination reason: Instruction limit
% 13.98/12.45 % (2738916)Termination phase: Saturation
% 13.98/12.45 % (2738916)Time elapsed: 0.060 s
% 13.98/12.45 % (2738916)Peak memory usage: 15 MB
% 13.98/12.45 % (2738916)Instructions burned: 160 (million)
% 13.98/12.45 % (2738924)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=82160012:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.98/12.45 % (2738913)Instruction limit reached!
% 13.98/12.45 % (2738913)------------------------------
% 13.98/12.45 % (2738913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/12.45 % (2738913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/12.45 % (2738913)CaDiCaL version: 2.1.3
% 13.98/12.45 % (2738913)Termination reason: Instruction limit
% 13.98/12.45 % (2738913)Termination phase: Saturation
% 13.98/12.45 % (2738913)Time elapsed: 0.071 s
% 13.98/12.45 % (2738913)Peak memory usage: 13 MB
% 13.98/12.45 % (2738913)Instructions burned: 104 (million)
% 13.98/12.45 % TRYING [1]
% 13.98/12.45 % (2738914)Instruction limit reached!
% 13.98/12.45 % (2738914)------------------------------
% 13.98/12.45 % (2738914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/12.45 % (2738914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/12.45 % (2738914)CaDiCaL version: 2.1.3
% 13.98/12.45 % (2738914)Termination reason: Instruction limit
% 13.98/12.45 % (2738914)Termination phase: Saturation
% 13.98/12.45 % (2738914)Time elapsed: 0.074 s
% 13.98/12.45 % (2738914)Peak memory usage: 13 MB
% 13.98/12.45 % (2738914)Instructions burned: 116 (million)
% 13.98/12.45 % TRYING [2]
% 13.98/12.45 % TRYING [3]
% 13.98/12.45 % (2738915)Instruction limit reached!
% 13.98/12.45 % (2738915)------------------------------
% 13.98/12.45 % (2738915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/12.45 % (2738915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/12.45 % (2738915)CaDiCaL version: 2.1.3
% 13.98/12.45 % (2738915)Termination reason: Instruction limit
% 13.98/12.45 % (2738915)Termination phase: Saturation
% 13.98/12.45 % (2738915)Time elapsed: 0.082 s
% 13.98/12.45 % (2738915)Peak memory usage: 13 MB
% 13.98/12.45 % (2738915)Instructions burned: 131 (million)
% 13.98/12.45 % (2738926)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3489316573:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.98/12.45 % TRYING [4]
% 13.98/12.45 % (2738927)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=2413996511:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.98/12.45 % TRYING [4]
% 13.98/12.45 % (2738928)ott-21_1_sil=16000:fs=off:random_seed=2296600189:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.98/12.45 % TRYING [5]
% 13.98/12.45 % (2738926)Instruction limit reached!
% 13.98/12.45 % (2738926)------------------------------
% 13.98/12.45 % (2738926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738926)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738926)Termination reason: Instruction limit
% 23.02/14.82 % (2738926)Termination phase: Saturation
% 23.02/14.82 % (2738926)Time elapsed: 0.089 s
% 23.02/14.82 % (2738926)Peak memory usage: 13 MB
% 23.02/14.82 % (2738926)Instructions burned: 131 (million)
% 23.02/14.82 % (2738932)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4174828806:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 23.02/14.82 % (2738928)Instruction limit reached!
% 23.02/14.82 % (2738928)------------------------------
% 23.02/14.82 % (2738928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738928)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738928)Termination reason: Instruction limit
% 23.02/14.82 % (2738928)Termination phase: Saturation
% 23.02/14.82 % (2738928)Time elapsed: 0.106 s
% 23.02/14.82 % (2738928)Peak memory usage: 13 MB
% 23.02/14.82 % (2738928)Instructions burned: 181 (million)
% 23.02/14.82 % (2738924)Instruction limit reached!
% 23.02/14.82 % (2738924)------------------------------
% 23.02/14.82 % (2738924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738924)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738924)Termination reason: Instruction limit
% 23.02/14.82 % (2738924)Termination phase: Finite model building SAT solving
% 23.02/14.82 % (2738924)Time elapsed: 0.153 s
% 23.02/14.82 % (2738924)Peak memory usage: 36 MB
% 23.02/14.82 % (2738924)Instructions burned: 716 (million)
% 23.02/14.82 % TRYING [5]
% 23.02/14.82 % (2738934)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3680175529:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 23.02/14.82 % (2738935)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3770421746:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 23.02/14.82 % TRYING [1]
% 23.02/14.82 % TRYING [2]
% 23.02/14.82 % TRYING [3]
% 23.02/14.82 % TRYING [4]
% 23.02/14.82 % (2738927)Instruction limit reached!
% 23.02/14.82 % (2738927)------------------------------
% 23.02/14.82 % (2738927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738927)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738927)Termination reason: Instruction limit
% 23.02/14.82 % (2738927)Termination phase: Saturation
% 23.02/14.82 % (2738927)Time elapsed: 0.373 s
% 23.02/14.82 % (2738927)Peak memory usage: 18 MB
% 23.02/14.82 % (2738927)Instructions burned: 685 (million)
% 23.02/14.82 % (2738938)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4064900110:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 23.02/14.82 % (2738932)Instruction limit reached!
% 23.02/14.82 % (2738932)------------------------------
% 23.02/14.82 % (2738932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738932)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738932)Termination reason: Instruction limit
% 23.02/14.82 % (2738932)Termination phase: Saturation
% 23.02/14.82 % (2738932)Time elapsed: 0.335 s
% 23.02/14.82 % (2738932)Peak memory usage: 15 MB
% 23.02/14.82 % (2738932)Instructions burned: 477 (million)
% 23.02/14.82 % (2738940)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=1631229353: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)
% 23.02/14.82 % TRYING [6]
% 23.02/14.82 % (2738934)Instruction limit reached!
% 23.02/14.82 % (2738934)------------------------------
% 23.02/14.82 % (2738934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738934)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738934)Termination reason: Instruction limit
% 23.02/14.82 % (2738934)Termination phase: Finite model building SAT solving
% 23.02/14.82 % (2738934)Time elapsed: 0.382 s
% 23.02/14.82 % (2738934)Peak memory usage: 28 MB
% 23.02/14.82 % (2738934)Instructions burned: 867 (million)
% 23.02/14.82 % (2738935)Instruction limit reached!
% 23.02/14.82 % (2738935)------------------------------
% 23.02/14.82 % (2738935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738935)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738935)Termination reason: Instruction limit
% 23.02/14.82 % (2738935)Termination phase: Saturation
% 23.02/14.82 % (2738935)Time elapsed: 0.401 s
% 23.02/14.82 % (2738935)Peak memory usage: 26 MB
% 23.02/14.82 % (2738935)Instructions burned: 1179 (million)
% 23.02/14.82 % (2738942)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2188262639:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 23.02/14.82 % (2738943)fmb+10_1_sil=64000:random_seed=2481739091:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 23.02/14.82 % TRYING [1]
% 23.02/14.82 % TRYING [2]
% 23.02/14.82 % TRYING [3]
% 23.02/14.82 % TRYING [4]
% 23.02/14.82 % TRYING [5]
% 23.02/14.82 % (2738940)Instruction limit reached!
% 23.02/14.82 % (2738940)------------------------------
% 23.02/14.82 % (2738940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738940)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738940)Termination reason: Instruction limit
% 23.02/14.82 % (2738940)Termination phase: Saturation
% 23.02/14.82 % (2738940)Time elapsed: 0.340 s
% 23.02/14.82 % (2738940)Peak memory usage: 17 MB
% 23.02/14.82 % (2738940)Instructions burned: 693 (million)
% 23.02/14.82 % (2738938)Instruction limit reached!
% 23.02/14.82 % (2738938)------------------------------
% 23.02/14.82 % (2738938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738938)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738938)Termination reason: Instruction limit
% 23.02/14.82 % (2738938)Termination phase: Finite model building constraint generation
% 23.02/14.82 % (2738938)Time elapsed: 0.419 s
% 23.02/14.82 % (2738938)Peak memory usage: 107 MB
% 23.02/14.82 % (2738938)Instructions burned: 889 (million)
% 23.02/14.82 % (2738946)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1148563348:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 23.02/14.82 % TRYING [20]
% 23.02/14.82 % (2738948)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3517888133:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 23.02/14.82 % TRYING [8]
% 23.02/14.82 % TRYING [6]
% 23.02/14.82 % (2738942)Instruction limit reached!
% 23.02/14.82 % (2738942)------------------------------
% 23.02/14.82 % (2738942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738942)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738942)Termination reason: Instruction limit
% 23.02/14.82 % (2738942)Termination phase: Saturation
% 23.02/14.82 % (2738942)Time elapsed: 0.502 s
% 23.02/14.82 % (2738942)Peak memory usage: 21 MB
% 23.02/14.82 % (2738942)Instructions burned: 881 (million)
% 23.02/14.82 % (2738950)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4029622963:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 23.02/14.82 % (2738948)Instruction limit reached!
% 23.02/14.82 % (2738948)------------------------------
% 23.02/14.82 % (2738948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738948)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738948)Termination reason: Instruction limit
% 23.02/14.82 % (2738948)Termination phase: Finite model building constraint generation
% 23.02/14.82 % (2738948)Time elapsed: 0.307 s
% 23.02/14.82 % (2738948)Peak memory usage: 56 MB
% 23.02/14.82 % (2738948)Instructions burned: 921 (million)
% 23.02/14.82 % (2738952)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=309162658:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 23.02/14.82 % TRYING [7]
% 23.02/14.82 % TRYING [7]
% 23.02/14.82 % (2738952)Instruction limit reached!
% 23.02/14.82 % (2738952)------------------------------
% 23.02/14.82 % (2738952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738952)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738952)Termination reason: Instruction limit
% 23.02/14.82 % (2738952)Termination phase: Saturation
% 23.02/14.82 % (2738952)Time elapsed: 0.673 s
% 23.02/14.82 % (2738952)Peak memory usage: 21 MB
% 23.02/14.82 % (2738952)Instructions burned: 1473 (million)
% 23.02/14.82 % (2738954)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1536089828:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 23.02/14.82 % (2738954)Cannot represent all propositional literals internally
% 23.02/14.82 % (2738954)Refutation not found, incomplete strategy
% 23.02/14.82 % (2738954)------------------------------
% 23.02/14.82 % (2738954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738954)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738954)Termination reason: Refutation not found, incomplete strategy
% 23.02/14.82 % (2738954)Time elapsed: 0.023 s
% 23.02/14.82 % (2738954)Peak memory usage: 11 MB
% 23.02/14.82 % (2738954)Instructions burned: 45 (million)
% 23.02/14.82 % (2738954)------------------------------
% 23.02/14.82 % (2738954)------------------------------
% 23.02/14.82 % (2738956)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2232306089:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 23.02/14.82 % TRYING [16]
% 23.02/14.82 % (2738956)Instruction limit reached!
% 23.02/14.82 % (2738956)------------------------------
% 23.02/14.82 % (2738956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738956)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738956)Termination reason: Instruction limit
% 23.02/14.82 % (2738956)Termination phase: Finite model building constraint generation
% 23.02/14.82 % (2738956)Time elapsed: 0.783 s
% 23.02/14.82 % (2738956)Peak memory usage: 127 MB
% 23.02/14.82 % (2738956)Instructions burned: 2177 (million)
% 23.02/14.82 % (2738958)ott-2_1_sil=16000:newcnf=on:random_seed=2049726370:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 23.02/14.82 % (2738958)Instruction limit reached!
% 23.02/14.82 % (2738958)------------------------------
% 23.02/14.82 % (2738958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738958)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738958)Termination reason: Instruction limit
% 23.02/14.82 % (2738958)Termination phase: Saturation
% 23.02/14.82 % (2738958)Time elapsed: 0.555 s
% 23.02/14.82 % (2738958)Peak memory usage: 20 MB
% 23.02/14.82 % (2738958)Instructions burned: 869 (million)
% 23.02/14.82 % (2738960)ott+10_1_sil=32000:tgt=ground:random_seed=770384494:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 23.02/14.82 % TRYING [8]
% 23.02/14.82 % (2738950)Instruction limit reached!
% 23.02/14.82 % (2738950)------------------------------
% 23.02/14.82 % (2738950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738950)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738950)Termination reason: Instruction limit
% 23.02/14.82 % (2738950)Termination phase: Saturation
% 23.02/14.82 % (2738950)Time elapsed: 3.097 s
% 23.02/14.82 % (2738950)Peak memory usage: 38 MB
% 23.02/14.82 % (2738950)Instructions burned: 5131 (million)
% 23.02/14.82 % (2738962)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1930199145:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 23.02/14.82 % (2738946)Instruction limit reached!
% 23.02/14.82 % (2738946)------------------------------
% 23.02/14.82 % (2738946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738946)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738946)Termination reason: Instruction limit
% 23.02/14.82 % (2738946)Termination phase: Finite model building constraint generation
% 23.02/14.82 % (2738946)Time elapsed: 3.363 s
% 23.02/14.82 % (2738946)Peak memory usage: 562 MB
% 23.02/14.82 % (2738946)Instructions burned: 9516 (million)
% 23.02/14.82 % (2738960) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2738905-2738960"...
% 23.02/14.82 % (2738960)...printing done.
% 23.02/14.82 % TRYING [1]
% 23.02/14.82 % TRYING [2]
% 23.02/14.82 % (2738960)Refutation found. Thanks to Tanya!
% 23.02/14.82 % SZS status Theorem for theBenchmark
% 23.02/14.82 % SZS output start Proof for theBenchmark
% See solution above
% 23.02/14.82 % (2738960)------------------------------
% 23.02/14.82 % (2738960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.02/14.82 % (2738960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.02/14.82 % (2738960)CaDiCaL version: 2.1.3
% 23.02/14.82 % (2738960)Termination reason: Refutation
% 23.02/14.82 % (2738960)Time elapsed: 0.890 s
% 23.02/14.82 % (2738960)Peak memory usage: 26 MB
% 23.02/14.82 % (2738960)Instructions burned: 1412 (million)
% 23.02/14.82 % (2738905)Success in time 4.399 s
% 23.02/14.82 % Vampire exiting
%------------------------------------------------------------------------------