%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM599+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:41:08 PM UTC 2026
% Result : Theorem 213.76s 27.51s
% Output : CNFRefutation 189.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 71
% Syntax : Number of formulae : 315 ( 73 unt; 46 def)
% Number of atoms : 801 ( 127 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 810 ( 324 ~; 310 |; 100 &)
% ( 53 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 51 ( 49 usr; 44 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 13 con; 0-3 aty)
% Number of variables : 151 ( 138 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> W0 != szszuzczcdt0(W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,definition,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
slbdtrb0(sz00) = slcrc0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sbrdtbr0(slbdtrb0(W0)) = W0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( ( isCountable0(W1)
& aSubsetOf0(W1,szDzozmdt0(W0)) )
=> ( ! [W2,W3] :
( ( W2 != W3
& aElementOf0(W3,szDzozmdt0(W0))
& aElementOf0(W2,szDzozmdt0(W0)) )
=> sdtlpdtrp0(W0,W2) != sdtlpdtrp0(W0,W3) )
=> isCountable0(sdtlcdtrc0(W0,W1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aFunction0(xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
xK != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,hypothesis,
! [W0,W1] :
( ( W0 != W1
& aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> szmzizndt0(sdtlpdtrp0(xN,W0)) != szmzizndt0(sdtlpdtrp0(xN,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ! [W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& aSet0(W1) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,hypothesis,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ? [W1] :
( ? [W2] :
( ! [W3] :
( ( aElementOf0(W3,slbdtsldtrb0(W2,xk))
& aSet0(W3) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W3) = W1 )
& isCountable0(W2)
& aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aElementOf0(W1,xT) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ! [W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
& aSet0(W1) )
=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
( isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,hypothesis,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,hypothesis,
( isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,conjecture,
isCountable0(xO),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,negated_conjecture,
~ isCountable0(xO),
inference(negated_conjecture,[status(cth)],[f97]) ).
fof(f109,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f110,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f112,plain,
( ! [W0] :
( aElementOf0(sK0_skl(W0),W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f111]) ).
fof(f113,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f123,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f124,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f126,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f125]) ).
fof(f127,plain,
! [X0,X1] :
( ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f128,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X1)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X0)
| ~ aSubsetOf0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f133,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f134,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f175,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f176,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f177,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f178,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f179,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szszuzczcdt0(X0) != sz00 ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f187,plain,
! [W0] :
( W0 != szszuzczcdt0(W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f188,plain,
! [X0] :
( szszuzczcdt0(X0) != X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f219,plain,
! [W0] :
( ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f220,plain,
! [W0] :
( ( ( W0 != slcrc0
| sbrdtbr0(W0) = sz00 )
& ( W0 = slcrc0
| sbrdtbr0(W0) != sz00 ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f219]) ).
fof(f222,plain,
! [X0] :
( X0 != slcrc0
| sbrdtbr0(X0) = sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f251,plain,
! [W0] :
( ! [W1] :
( W1 = slbdtrb0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) ) )
& aSet0(W1) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f252,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| aElementOf0(W2,W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ( ( ! [W2] :
( ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) ) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f251]) ).
fof(f253,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| aElementOf0(W2,W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ! [W1] :
( ( ! [W2] :
( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f252]) ).
fof(f254,plain,
! [W0] :
( ( ! [W1] :
( ( ( ( sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)
& aElementOf0(sK8_skl(W1,W0),szNzAzT0) )
| aElementOf0(sK8_skl(W1,W0),W1) )
& ( ~ sdtlseqdt0(szszuzczcdt0(sK8_skl(W1,W0)),W0)
| ~ aElementOf0(sK8_skl(W1,W0),szNzAzT0)
| ~ aElementOf0(sK8_skl(W1,W0),W1) ) )
| ~ aSet0(W1)
| W1 = slbdtrb0(W0) )
& ! [W1] :
( ( ! [W2] :
( ~ sdtlseqdt0(szszuzczcdt0(W2),W0)
| ~ aElementOf0(W2,szNzAzT0)
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtlseqdt0(szszuzczcdt0(W2),W0)
& aElementOf0(W2,szNzAzT0) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slbdtrb0(W0) ) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W2,sK8_skl(W1,W0))],[f253]) ).
fof(f255,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slbdtrb0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f264,plain,
slbdtrb0(sz00) = slcrc0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f278,plain,
! [W0] :
( sbrdtbr0(slbdtrb0(W0)) = W0
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f279,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| sbrdtbr0(slbdtrb0(X0)) = X0 ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f307,plain,
! [W0] :
( aSet0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f308,plain,
! [X0] :
( ~ aFunction0(X0)
| aSet0(szDzozmdt0(X0)) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f346,plain,
! [W0] :
( ! [W1] :
( isCountable0(sdtlcdtrc0(W0,W1))
| ? [W2,W3] :
( sdtlpdtrp0(W0,W2) = sdtlpdtrp0(W0,W3)
& W2 != W3
& aElementOf0(W3,szDzozmdt0(W0))
& aElementOf0(W2,szDzozmdt0(W0)) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f347,plain,
! [W0] :
( ! [W1] :
( isCountable0(sdtlcdtrc0(W0,W1))
| ( sdtlpdtrp0(W0,sK17_skl(W1,W0)) = sdtlpdtrp0(W0,sK18_skl(W1,W0))
& sK17_skl(W1,W0) != sK18_skl(W1,W0)
& aElementOf0(sK18_skl(W1,W0),szDzozmdt0(W0))
& aElementOf0(sK17_skl(W1,W0),szDzozmdt0(W0)) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(W2,sK17_skl(W1,W0)),skolemize(W3,sK18_skl(W1,W0))],[f346]) ).
fof(f348,plain,
! [X0,X1] :
( ~ aFunction0(X1)
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,szDzozmdt0(X1))
| isCountable0(sdtlcdtrc0(X1,X0))
| aElementOf0(sK17_skl(X0,X1),szDzozmdt0(X1)) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f349,plain,
! [X0,X1] :
( isCountable0(sdtlcdtrc0(X1,X0))
| ~ aFunction0(X1)
| ~ isCountable0(X0)
| ~ aSubsetOf0(X0,szDzozmdt0(X1))
| aElementOf0(sK18_skl(X0,X1),szDzozmdt0(X1)) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f350,plain,
! [X0,X1] :
( ~ isCountable0(X1)
| ~ aFunction0(X0)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| sK17_skl(X1,X0) != sK18_skl(X1,X0)
| isCountable0(sdtlcdtrc0(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f351,plain,
! [X0,X1] :
( ~ aFunction0(X0)
| ~ isCountable0(X1)
| isCountable0(sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| sdtlpdtrp0(X0,sK18_skl(X1,X0)) = sdtlpdtrp0(X0,sK17_skl(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f357,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f358,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f360,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f370,plain,
xK != sz00,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f371,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f373,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f375,plain,
szDzozmdt0(xN) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f384,plain,
! [W0,W1] :
( szmzizndt0(sdtlpdtrp0(xN,W0)) != szmzizndt0(sdtlpdtrp0(xN,W1))
| W0 = W1
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f385,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| szmzizndt0(sdtlpdtrp0(xN,X0)) != szmzizndt0(sdtlpdtrp0(xN,X1))
| X0 = X1
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f388,plain,
( ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f390,plain,
szNzAzT0 = szDzozmdt0(xC),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f398,plain,
! [W0] :
( ? [W1] :
( ? [W2] :
( ! [W3] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W3) = W1
| ~ aElementOf0(W3,slbdtsldtrb0(W2,xk))
| ~ aSet0(W3) )
& isCountable0(W2)
& aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aElementOf0(W1,xT) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f399,plain,
! [W0] :
( ( ! [W3] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W3) = sK21_skl(W0)
| ~ aElementOf0(W3,slbdtsldtrb0(sK22_skl(W0),xk))
| ~ aSet0(W3) )
& isCountable0(sK22_skl(W0))
& aSubsetOf0(sK22_skl(W0),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& aElementOf0(sK21_skl(W0),xT) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(W1,sK21_skl(W0)),skolemize(W2,sK22_skl(W0))],[f398]) ).
fof(f400,plain,
! [X0] :
( aElementOf0(sK21_skl(X0),xT)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f408,plain,
( ! [W0] :
( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f409,plain,
aFunction0(xe),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f410,plain,
szDzozmdt0(xe) = szNzAzT0,
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f411,plain,
! [X0] :
( sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f412,plain,
( ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)
| ~ aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))
| ~ aSet0(W1) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xd) = szNzAzT0
& aFunction0(xd) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f413,plain,
aFunction0(xd),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f414,plain,
szNzAzT0 = szDzozmdt0(xd),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f418,plain,
isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f419,plain,
aSet0(xO),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f420,plain,
sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) = xO,
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f421,plain,
aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f423,plain,
~ isCountable0(xO),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f447,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f113]) ).
fof(f450,plain,
( sbrdtbr0(slcrc0) = sz00
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f222]) ).
fof(f451,plain,
sz00 = sbrdtbr0(slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f450,f447]) ).
fof(f456,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(slbdtrb0(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f255]) ).
fof(f482,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f114]) ).
fof(f491,definition,
( sQ1_spl
<=> aFunction0(xd) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ1_spl
| ~ aFunction0(xd) ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f496,plain,
szszuzczcdt0(sz00) != sz00,
inference(resolution,[status(thm)],[f177,f188]) ).
fof(f529,definition,
( sQ9_spl
<=> aFunction0(xe) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( sQ9_spl
| ~ aFunction0(xe) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f540,plain,
( aSet0(szNzAzT0)
| ~ aFunction0(xd) ),
inference(paramodulation,[status(thm)],[f414,f308]) ).
fof(f541,definition,
( sQ10_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( sQ10_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f540,f491,f541]) ).
fof(f548,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f413]) ).
fof(f549,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f548]) ).
fof(f552,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f531,f409]) ).
fof(f553,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f552]) ).
fof(f639,plain,
sz00 != szszuzczcdt0(xK),
inference(resolution,[status(thm)],[f180,f357]) ).
fof(f675,definition,
( sQ29_spl
<=> slcrc0 = xT ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f676,plain,
( ~ sQ29_spl
| slcrc0 = xT ),
inference(component_clause,[status(thm)],[f675]) ).
fof(f693,plain,
xK = sbrdtbr0(slbdtrb0(xK)),
inference(resolution,[status(thm)],[f279,f357]) ).
fof(f700,definition,
( sQ32_spl
<=> aSet0(slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( sQ32_spl
| ~ aSet0(slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f708,definition,
( sQ34_spl
<=> aSet0(slbdtrb0(xK)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( sQ34_spl
| ~ aSet0(slbdtrb0(xK)) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f905,definition,
( sQ43_spl
<=> aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f907,plain,
( sQ43_spl
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f905]) ).
fof(f918,plain,
( ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe))
| ~ aFunction0(xe)
| ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe) != sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)
| isCountable0(xO) ),
inference(paramodulation,[status(thm)],[f420,f350]) ).
fof(f919,definition,
( sQ45_spl
<=> isCountable0(xO) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f920,plain,
( ~ sQ45_spl
| isCountable0(xO) ),
inference(component_clause,[status(thm)],[f919]) ).
fof(f922,definition,
( sQ46_spl
<=> sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe) = sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f925,definition,
( sQ47_spl
<=> isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f927,plain,
( sQ47_spl
| ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(component_clause,[status(thm)],[f925]) ).
fof(f928,plain,
( ~ sQ43_spl
| ~ sQ9_spl
| ~ sQ47_spl
| ~ sQ46_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f918,f919,f922,f925,f529,f905]) ).
fof(f929,plain,
( sQ43_spl
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f907]) ).
fof(f930,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f929,f421]) ).
fof(f931,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f930]) ).
fof(f932,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f927,f418]) ).
fof(f933,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f932]) ).
fof(f935,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f920,f423]) ).
fof(f936,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f935]) ).
fof(f1029,plain,
! [X0] :
( sz00 != szszuzczcdt0(szszuzczcdt0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f179,f180]) ).
fof(f1053,plain,
szszuzczcdt0(szszuzczcdt0(xK)) != sz00,
inference(resolution,[status(thm)],[f1029,f357]) ).
fof(f1062,plain,
( isCountable0(xO)
| ~ aFunction0(xe)
| ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe))
| aElementOf0(sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szDzozmdt0(xe)) ),
inference(paramodulation,[status(thm)],[f420,f349]) ).
fof(f1063,definition,
( sQ60_spl
<=> aElementOf0(sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
( ~ sQ60_spl
| aElementOf0(sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f1063]) ).
fof(f1066,plain,
( sQ45_spl
| ~ sQ9_spl
| ~ sQ47_spl
| ~ sQ43_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1062,f1063,f905,f925,f529,f919]) ).
fof(f1067,plain,
( ~ sQ60_spl
| aElementOf0(sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f1064]) ).
fof(f1111,definition,
( sQ68_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1113,plain,
( sQ68_spl
| ~ aSet0(xS) ),
inference(component_clause,[status(thm)],[f1111]) ).
fof(f1481,definition,
( sQ84_spl
<=> aSubsetOf0(szNzAzT0,szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1482,plain,
( ~ sQ84_spl
| aSubsetOf0(szNzAzT0,szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1483,plain,
( sQ84_spl
| ~ aSubsetOf0(szNzAzT0,szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1488,plain,
( sQ84_spl
| ~ aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f414,f1483]) ).
fof(f1497,plain,
( sQ84_spl
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f1488,f134]) ).
fof(f1498,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1497,f175]) ).
fof(f1499,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f1498]) ).
fof(f1500,plain,
( ~ sQ84_spl
| aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f414,f1482]) ).
fof(f1537,plain,
( ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlpdtrp0(xe,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) = sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe))
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe))
| isCountable0(xO)
| ~ aFunction0(xe) ),
inference(paramodulation,[status(thm)],[f420,f351]) ).
fof(f1538,definition,
( sQ92_spl
<=> sdtlpdtrp0(xe,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) = sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1539,plain,
( ~ sQ92_spl
| sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) = sdtlpdtrp0(xe,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) ),
inference(component_clause,[status(thm)],[f1538]) ).
fof(f1541,plain,
( ~ sQ47_spl
| sQ92_spl
| ~ sQ43_spl
| sQ45_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1537,f529,f919,f905,f1538,f925]) ).
fof(f2124,definition,
( sQ151_spl
<=> aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2125,plain,
( ~ sQ151_spl
| aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f2124]) ).
fof(f2126,plain,
( sQ151_spl
| ~ aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f2124]) ).
fof(f2148,plain,
( sQ151_spl
| ~ aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f2126]) ).
fof(f2179,plain,
! [X0] :
( sQ151_spl
| ~ aSet0(szNzAzT0)
| ~ aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),X0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f2148,f128]) ).
fof(f2188,definition,
! [X0] :
( sQ160_spl
<=> ( ~ aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),X0)
| ~ aSubsetOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f2189,plain,
! [X0] :
( ~ sQ160_spl
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),X0) ),
inference(component_clause,[status(thm)],[f2188]) ).
fof(f2191,plain,
( sQ151_spl
| ~ sQ10_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f2179,f2188,f541,f2124]) ).
fof(f2242,definition,
( sQ167_spl
<=> isCountable0(sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f2243,plain,
( ~ sQ167_spl
| isCountable0(sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))) ),
inference(component_clause,[status(thm)],[f2242]) ).
fof(f2254,plain,
( ~ sQ167_spl
| isCountable0(xO) ),
inference(forward_demodulation,[status(thm)],[f420,f2243]) ).
fof(f2255,plain,
( ~ sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2254,f423]) ).
fof(f2256,plain,
~ sQ167_spl,
inference(contradiction_clause,[status(thm)],[f2255]) ).
fof(f2285,plain,
( ~ sQ160_spl
| ~ aFunction0(xe)
| ~ isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aSubsetOf0(sdtlbdtrb0(xd,szDzizrdt0(xd)),szDzozmdt0(xe))
| isCountable0(sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))))
| ~ aSubsetOf0(szDzozmdt0(xe),szNzAzT0) ),
inference(resolution,[status(thm)],[f2189,f348]) ).
fof(f2291,definition,
( sQ169_spl
<=> aSubsetOf0(szDzozmdt0(xe),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f2293,plain,
( sQ169_spl
| ~ aSubsetOf0(szDzozmdt0(xe),szNzAzT0) ),
inference(component_clause,[status(thm)],[f2291]) ).
fof(f2294,plain,
( ~ sQ160_spl
| ~ sQ9_spl
| ~ sQ47_spl
| ~ sQ43_spl
| sQ167_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f2285,f2291,f2242,f905,f925,f529,f2188]) ).
fof(f2307,plain,
( sQ169_spl
| ~ aSubsetOf0(szNzAzT0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f2293]) ).
fof(f2308,plain,
( sQ169_spl
| ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2307,f1500]) ).
fof(f2309,plain,
( sQ169_spl
| ~ sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f2308]) ).
fof(f2310,plain,
( ~ sQ151_spl
| aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f2125]) ).
fof(f2632,definition,
! [X0] :
( sQ194_spl
<=> X0 = sK0_skl(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2633,plain,
! [X0] :
( ~ sQ194_spl
| X0 = sK0_skl(slcrc0) ),
inference(component_clause,[status(thm)],[f2632]) ).
fof(f2642,plain,
! [X0,X1] :
( ~ sQ194_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f2633,f2633]) ).
fof(f2672,plain,
( ~ sQ194_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1053,f2642]) ).
fof(f2696,plain,
~ sQ194_spl,
inference(contradiction_clause,[status(thm)],[f2672]) ).
fof(f2727,plain,
! [X0] :
( sQ68_spl
| ~ aSubsetOf0(xS,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f1113,f127]) ).
fof(f2732,definition,
! [X0] :
( sQ204_spl
<=> ~ aSet0(X0) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f2733,plain,
! [X0] :
( ~ sQ204_spl
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f2732]) ).
fof(f2738,plain,
( ~ sQ204_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f447,f2733]) ).
fof(f2746,plain,
~ sQ204_spl,
inference(contradiction_clause,[status(thm)],[f2738]) ).
fof(f2825,definition,
( sQ208_spl
<=> aElementOf0(sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f2826,plain,
( ~ sQ208_spl
| aElementOf0(sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)),slcrc0) ),
inference(component_clause,[status(thm)],[f2825]) ).
fof(f2832,plain,
( ~ sQ208_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2826,f482]) ).
fof(f2833,plain,
~ sQ208_spl,
inference(contradiction_clause,[status(thm)],[f2832]) ).
fof(f2873,plain,
( sQ68_spl
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f2727,f358]) ).
fof(f2880,definition,
( sQ213_spl
<=> aSubsetOf0(xS,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2882,plain,
( sQ213_spl
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(component_clause,[status(thm)],[f2880]) ).
fof(f2887,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2873,f175]) ).
fof(f2888,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f2887]) ).
fof(f2889,plain,
( sQ213_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2882,f358]) ).
fof(f2890,plain,
sQ213_spl,
inference(contradiction_clause,[status(thm)],[f2889]) ).
fof(f3351,plain,
! [X0] :
( ~ sQ29_spl
| ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(sK21_skl(X0),slcrc0) ),
inference(backward_demodulation,[status(thm)],[f676,f400]) ).
fof(f3371,plain,
( ~ sQ29_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f357,f3386]) ).
fof(f3386,plain,
! [X0] :
( ~ sQ29_spl
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3351,f482]) ).
fof(f3387,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f3371]) ).
fof(f3510,definition,
( sQ254_spl
<=> aElementOf0(sz00,szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f3512,plain,
( sQ254_spl
| ~ aElementOf0(sz00,szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f3510]) ).
fof(f3514,plain,
( sQ254_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f3512]) ).
fof(f3515,plain,
( sQ254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3514,f177]) ).
fof(f3516,plain,
sQ254_spl,
inference(contradiction_clause,[status(thm)],[f3515]) ).
fof(f3834,definition,
( sQ285_spl
<=> aFunction0(xc) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f3836,plain,
( sQ285_spl
| ~ aFunction0(xc) ),
inference(component_clause,[status(thm)],[f3834]) ).
fof(f3851,plain,
( sQ285_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3836,f360]) ).
fof(f3852,plain,
sQ285_spl,
inference(contradiction_clause,[status(thm)],[f3851]) ).
fof(f3854,plain,
aSet0(slbdtrb0(xK)),
inference(resolution,[status(thm)],[f456,f357]) ).
fof(f3855,plain,
aSet0(slbdtrb0(xk)),
inference(resolution,[status(thm)],[f456,f371]) ).
fof(f3860,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3854,f710]) ).
fof(f3861,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f3860]) ).
fof(f3864,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3855,f702]) ).
fof(f3865,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f3864]) ).
fof(f3915,definition,
( sQ292_spl
<=> isCountable0(szDzozmdt0(xe)) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f3917,plain,
( sQ292_spl
| ~ isCountable0(szDzozmdt0(xe)) ),
inference(component_clause,[status(thm)],[f3915]) ).
fof(f3928,definition,
( sQ296_spl
<=> isCountable0(szDzozmdt0(xN)) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f3930,plain,
( sQ296_spl
| ~ isCountable0(szDzozmdt0(xN)) ),
inference(component_clause,[status(thm)],[f3928]) ).
fof(f3941,definition,
( sQ300_spl
<=> isCountable0(szDzozmdt0(xC)) ),
introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition]) ).
fof(f3943,plain,
( sQ300_spl
| ~ isCountable0(szDzozmdt0(xC)) ),
inference(component_clause,[status(thm)],[f3941]) ).
fof(f3948,definition,
( sQ302_spl
<=> isCountable0(szDzozmdt0(xd)) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f3950,plain,
( sQ302_spl
| ~ isCountable0(szDzozmdt0(xd)) ),
inference(component_clause,[status(thm)],[f3948]) ).
fof(f3955,plain,
( sQ292_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f410,f3917]) ).
fof(f3956,plain,
( sQ292_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3955,f176]) ).
fof(f3957,plain,
sQ292_spl,
inference(contradiction_clause,[status(thm)],[f3956]) ).
fof(f3958,plain,
( sQ300_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f390,f3943]) ).
fof(f3959,plain,
( sQ300_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3958,f176]) ).
fof(f3960,plain,
sQ300_spl,
inference(contradiction_clause,[status(thm)],[f3959]) ).
fof(f3962,plain,
( sQ302_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f414,f3950]) ).
fof(f3963,plain,
( sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3962,f176]) ).
fof(f3964,plain,
sQ302_spl,
inference(contradiction_clause,[status(thm)],[f3963]) ).
fof(f3967,plain,
( sQ296_spl
| ~ isCountable0(szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f375,f3930]) ).
fof(f3968,plain,
( sQ296_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3967,f176]) ).
fof(f3969,plain,
sQ296_spl,
inference(contradiction_clause,[status(thm)],[f3968]) ).
fof(f4320,definition,
( sQ338_spl
<=> sdtlpdtrp0(xc,sK16_skl(xc,szDzozmdt0(xc),xc)) = sdtlpdtrp0(xc,sK16_skl(xc,szDzozmdt0(xc),xc)) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f4322,plain,
( sQ338_spl
| sdtlpdtrp0(xc,sK16_skl(xc,szDzozmdt0(xc),xc)) != sdtlpdtrp0(xc,sK16_skl(xc,szDzozmdt0(xc),xc)) ),
inference(component_clause,[status(thm)],[f4320]) ).
fof(f4336,plain,
( sQ338_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4322]) ).
fof(f4337,plain,
sQ338_spl,
inference(contradiction_clause,[status(thm)],[f4336]) ).
fof(f4406,definition,
( sQ352_spl
<=> slbdtrb0(xK) = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f4407,plain,
( ~ sQ352_spl
| slcrc0 = slbdtrb0(xK) ),
inference(component_clause,[status(thm)],[f4406]) ).
fof(f4429,plain,
( ~ sQ352_spl
| xK = sbrdtbr0(slcrc0) ),
inference(backward_demodulation,[status(thm)],[f4407,f693]) ).
fof(f4430,plain,
( ~ sQ352_spl
| xK = sz00 ),
inference(forward_demodulation,[status(thm)],[f451,f4429]) ).
fof(f4431,plain,
( ~ sQ352_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4430,f370]) ).
fof(f4432,plain,
~ sQ352_spl,
inference(contradiction_clause,[status(thm)],[f4431]) ).
fof(f6136,definition,
( sQ510_spl
<=> aElementOf0(szmzizndt0(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ510_spl])],[split_symbol_definition]) ).
fof(f6137,plain,
( ~ sQ510_spl
| aElementOf0(szmzizndt0(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f6136]) ).
fof(f6144,plain,
( ~ sQ510_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6137,f482]) ).
fof(f6145,plain,
~ sQ510_spl,
inference(contradiction_clause,[status(thm)],[f6144]) ).
fof(f6221,definition,
( sQ518_spl
<=> aElementOf0(szmzazxdt0(slcrc0),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ518_spl])],[split_symbol_definition]) ).
fof(f6222,plain,
( ~ sQ518_spl
| aElementOf0(szmzazxdt0(slcrc0),slcrc0) ),
inference(component_clause,[status(thm)],[f6221]) ).
fof(f6235,plain,
( ~ sQ518_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6222,f482]) ).
fof(f6236,plain,
~ sQ518_spl,
inference(contradiction_clause,[status(thm)],[f6235]) ).
fof(f6365,plain,
( ~ sQ60_spl
| sdtlpdtrp0(xe,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) = szmzizndt0(sdtlpdtrp0(xN,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe))) ),
inference(resolution,[status(thm)],[f411,f1067]) ).
fof(f6370,plain,
( ~ sQ151_spl
| szmzizndt0(sdtlpdtrp0(xN,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe))) = sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) ),
inference(resolution,[status(thm)],[f411,f2310]) ).
fof(f6388,plain,
( ~ sQ60_spl
| ~ sQ92_spl
| szmzizndt0(sdtlpdtrp0(xN,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe))) = sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) ),
inference(forward_demodulation,[status(thm)],[f1539,f6365]) ).
fof(f6563,definition,
( sQ553_spl
<=> aElementOf0(szszuzczcdt0(xK),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition]) ).
fof(f6565,plain,
( sQ553_spl
| ~ aElementOf0(szszuzczcdt0(xK),szNzAzT0) ),
inference(component_clause,[status(thm)],[f6563]) ).
fof(f6702,plain,
( sQ553_spl
| ~ aElementOf0(xK,szNzAzT0) ),
inference(resolution,[status(thm)],[f179,f6565]) ).
fof(f6711,plain,
( sQ553_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6702,f357]) ).
fof(f6712,plain,
sQ553_spl,
inference(contradiction_clause,[status(thm)],[f6711]) ).
fof(f6860,definition,
( sQ589_spl
<=> xK = sz00 ),
introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition]) ).
fof(f6861,plain,
( ~ sQ589_spl
| xK = sz00 ),
inference(component_clause,[status(thm)],[f6860]) ).
fof(f6896,definition,
( sQ599_spl
<=> szszuzczcdt0(sz00) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ599_spl])],[split_symbol_definition]) ).
fof(f6897,plain,
( ~ sQ599_spl
| szszuzczcdt0(sz00) = sz00 ),
inference(component_clause,[status(thm)],[f6896]) ).
fof(f6910,definition,
( sQ603_spl
<=> szszuzczcdt0(xK) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ603_spl])],[split_symbol_definition]) ).
fof(f6911,plain,
( ~ sQ603_spl
| szszuzczcdt0(xK) = sz00 ),
inference(component_clause,[status(thm)],[f6910]) ).
fof(f6924,plain,
( ~ sQ599_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6897,f496]) ).
fof(f6925,plain,
~ sQ599_spl,
inference(contradiction_clause,[status(thm)],[f6924]) ).
fof(f6928,plain,
( ~ sQ589_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6861,f370]) ).
fof(f6929,plain,
~ sQ589_spl,
inference(contradiction_clause,[status(thm)],[f6928]) ).
fof(f6991,plain,
( ~ sQ603_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6911,f639]) ).
fof(f6992,plain,
~ sQ603_spl,
inference(contradiction_clause,[status(thm)],[f6991]) ).
fof(f7728,definition,
( sQ670_spl
<=> aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ670_spl])],[split_symbol_definition]) ).
fof(f7729,plain,
( ~ sQ670_spl
| aElementOf0(sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe),slcrc0) ),
inference(component_clause,[status(thm)],[f7728]) ).
fof(f7753,plain,
( ~ sQ670_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7729,f482]) ).
fof(f7754,plain,
~ sQ670_spl,
inference(contradiction_clause,[status(thm)],[f7753]) ).
fof(f8174,definition,
( sQ704_spl
<=> aElementOf0(sK4_skl(sz00),slbdtrb0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition]) ).
fof(f8175,plain,
( ~ sQ704_spl
| aElementOf0(sK4_skl(sz00),slbdtrb0(sz00)) ),
inference(component_clause,[status(thm)],[f8174]) ).
fof(f8184,plain,
( ~ sQ704_spl
| aElementOf0(sK4_skl(sz00),slcrc0) ),
inference(forward_demodulation,[status(thm)],[f264,f8175]) ).
fof(f8185,plain,
( ~ sQ704_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8184,f482]) ).
fof(f8186,plain,
~ sQ704_spl,
inference(contradiction_clause,[status(thm)],[f8185]) ).
fof(f8972,plain,
aSubsetOf0(slbdtrb0(xk),slbdtrb0(xk)),
inference(resolution,[status(thm)],[f134,f3855]) ).
fof(f8976,plain,
aSubsetOf0(xO,xO),
inference(resolution,[status(thm)],[f134,f419]) ).
fof(f9209,definition,
( sQ717_spl
<=> aSubsetOf0(xO,xO) ),
introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition]) ).
fof(f9211,plain,
( sQ717_spl
| ~ aSubsetOf0(xO,xO) ),
inference(component_clause,[status(thm)],[f9209]) ).
fof(f9225,plain,
( sQ717_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9211,f8976]) ).
fof(f9226,plain,
sQ717_spl,
inference(contradiction_clause,[status(thm)],[f9225]) ).
fof(f9374,definition,
( sQ747_spl
<=> aSubsetOf0(slbdtrb0(xk),slbdtrb0(xk)) ),
introduced(definition,[new_symbols(definition,[sQ747_spl])],[split_symbol_definition]) ).
fof(f9376,plain,
( sQ747_spl
| ~ aSubsetOf0(slbdtrb0(xk),slbdtrb0(xk)) ),
inference(component_clause,[status(thm)],[f9374]) ).
fof(f9378,plain,
( sQ747_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9376,f8972]) ).
fof(f9379,plain,
sQ747_spl,
inference(contradiction_clause,[status(thm)],[f9378]) ).
fof(f10341,definition,
( sQ822_spl
<=> aElementOf0(szszuzczcdt0(sbrdtbr0(szNzAzT0)),slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ822_spl])],[split_symbol_definition]) ).
fof(f10342,plain,
( ~ sQ822_spl
| aElementOf0(szszuzczcdt0(sbrdtbr0(szNzAzT0)),slcrc0) ),
inference(component_clause,[status(thm)],[f10341]) ).
fof(f10351,plain,
( ~ sQ822_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10342,f482]) ).
fof(f10352,plain,
~ sQ822_spl,
inference(contradiction_clause,[status(thm)],[f10351]) ).
fof(f11077,plain,
! [X0] :
( ~ sQ60_spl
| szmzizndt0(sdtlpdtrp0(xN,X0)) != szmzizndt0(sdtlpdtrp0(xN,sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)))
| X0 = sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f385,f1067]) ).
fof(f11084,plain,
! [X0] :
( ~ sQ60_spl
| ~ sQ92_spl
| ~ aElementOf0(X0,szNzAzT0)
| sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) != szmzizndt0(sdtlpdtrp0(xN,X0))
| X0 = sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe) ),
inference(forward_demodulation,[status(thm)],[f6388,f11077]) ).
fof(f11416,definition,
! [X0] :
( sQ906_spl
<=> ( ~ aSubsetOf0(xO,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ906_spl])],[split_symbol_definition]) ).
fof(f11417,plain,
! [X0] :
( ~ sQ906_spl
| ~ aSet0(X0)
| ~ aSubsetOf0(xO,X0) ),
inference(component_clause,[status(thm)],[f11416]) ).
fof(f11549,plain,
( ~ sQ906_spl
| ~ aSet0(xO) ),
inference(resolution,[status(thm)],[f11417,f8976]) ).
fof(f11555,plain,
( ~ sQ906_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11549,f419]) ).
fof(f11556,plain,
~ sQ906_spl,
inference(contradiction_clause,[status(thm)],[f11555]) ).
fof(f11788,plain,
( ~ sQ151_spl
| ~ sQ60_spl
| ~ sQ92_spl
| sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) != szmzizndt0(sdtlpdtrp0(xN,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)))
| sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe) = sK18_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe) ),
inference(resolution,[status(thm)],[f11084,f2310]) ).
fof(f11842,definition,
( sQ947_spl
<=> sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) = szmzizndt0(sdtlpdtrp0(xN,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe))) ),
introduced(definition,[new_symbols(definition,[sQ947_spl])],[split_symbol_definition]) ).
fof(f11844,plain,
( sQ947_spl
| sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) != szmzizndt0(sdtlpdtrp0(xN,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe))) ),
inference(component_clause,[status(thm)],[f11842]) ).
fof(f11845,plain,
( ~ sQ151_spl
| ~ sQ60_spl
| ~ sQ92_spl
| ~ sQ947_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f11788,f922,f11842,f1538,f1063,f2124]) ).
fof(f12035,plain,
( sQ947_spl
| ~ sQ151_spl
| sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) != sdtlpdtrp0(xe,sK17_skl(sdtlbdtrb0(xd,szDzizrdt0(xd)),xe)) ),
inference(forward_demodulation,[status(thm)],[f6370,f11844]) ).
fof(f12036,plain,
( sQ947_spl
| ~ sQ151_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f12035]) ).
fof(f12037,plain,
( sQ947_spl
| ~ sQ151_spl ),
inference(contradiction_clause,[status(thm)],[f12036]) ).
fof(f12038,plain,
$false,
inference(sat_refutation,[status(thm)],[f544,f549,f553,f928,f931,f933,f936,f1066,f1499,f1541,f2191,f2256,f2294,f2309,f2696,f2746,f2833,f2888,f2890,f3387,f3516,f3852,f3861,f3865,f3957,f3960,f3964,f3969,f4337,f4432,f6145,f6236,f6712,f6925,f6929,f6992,f7754,f8186,f9226,f9379,f10352,f11556,f11845,f12037]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM599+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n002.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 02:46:18 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.39 % Drodi V4.1.1
% 213.76/27.51 % Refutation found
% 213.76/27.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 213.76/27.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 198.72/28.75 % Elapsed time: 28.154588 seconds
% 198.72/28.75 % CPU time: 209.586874 seconds
% 198.72/28.75 % Total memory used: 524.045 MB
% 198.72/28.75 % Net memory used: 471.246 MB
%------------------------------------------------------------------------------