%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM563+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:01 PM UTC 2026
% Result : Theorem 64.96s 8.70s
% Output : CNFRefutation 53.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 73 ( 13 unt; 3 def)
% Number of atoms : 394 ( 79 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 479 ( 158 ~; 147 |; 147 &)
% ( 9 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 142 ( 120 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [W0] :
( aSet0(W0)
=> ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
=> aElementOf0(W0,xT) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
=> aElementOf0(W0,szDzozmdt0(xc)) )
& ( aElementOf0(W0,szDzozmdt0(xc))
=> ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) )
& aFunction0(xc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,conjecture,
( xK = sz00
=> ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,xS) )
& aSet0(W1) ) ) )
& aElementOf0(W0,xT) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
~ ( xK = sz00
=> ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,xS) )
& aSet0(W1) ) ) )
& aElementOf0(W0,xT) ) ),
inference(negated_conjecture,[status(cth)],[f78]) ).
fof(f90,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f91,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f93,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))],[f92]) ).
fof(f94,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f104,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(f105,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)],[f104]) ).
fof(f106,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)],[f105]) ).
fof(f107,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))],[f106]) ).
fof(f110,plain,
! [X0,X1] :
( aElementOf0(sK1_skl(X1,X0),X1)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f114,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f115,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f200,plain,
! [W0] :
( ( sbrdtbr0(W0) = sz00
<=> W0 = slcrc0 )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f201,plain,
! [W0] :
( ( ( W0 != slcrc0
| sbrdtbr0(W0) = sz00 )
& ( W0 = slcrc0
| sbrdtbr0(W0) != sz00 ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [X0] :
( X0 = slcrc0
| sbrdtbr0(X0) != sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f203,plain,
! [X0] :
( X0 != slcrc0
| sbrdtbr0(X0) = sz00
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f339,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f340,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f343,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f344,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
<=> ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) ) )
& aFunction0(xc) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f345,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ( ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( ( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) ) )
& aFunction0(xc) ),
inference(NNF_transformation,[status(thm)],[f344]) ).
fof(f346,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ? [W1] :
( sdtlpdtrp0(xc,W1) = W0
& aElementOf0(W1,szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& ! [W0] :
( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) )
& aFunction0(xc) ),
inference(miniscoping,[status(thm)],[f345]) ).
fof(f347,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& ! [W0] :
( aElementOf0(W0,xT)
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xc,W1) != W0
| ~ aElementOf0(W1,szDzozmdt0(xc)) )
| aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& ! [W0] :
( ( sdtlpdtrp0(xc,sK20_skl(W0)) = W0
& aElementOf0(sK20_skl(W0),szDzozmdt0(xc)) )
| ~ aElementOf0(W0,sdtlcdtrc0(xc,szDzozmdt0(xc))) )
& aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& ! [W0] :
( aElementOf0(W0,szDzozmdt0(xc))
| sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xS)
& ( ( ~ aElementOf0(sK19_skl(W0),xS)
& aElementOf0(sK19_skl(W0),W0) )
| ~ aSet0(W0) ) ) )
& ! [W0] :
( ( sbrdtbr0(W0) = xK
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aElementOf0(W0,szDzozmdt0(xc)) )
& aFunction0(xc) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W1,sK19_skl(W0)),skolemize(W1,sK20_skl(W0))],[f346]) ).
fof(f355,plain,
! [X0] :
( aElementOf0(X0,szDzozmdt0(xc))
| sbrdtbr0(X0) != xK
| ~ aSubsetOf0(X0,xS) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f360,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,X1) != X0
| ~ aElementOf0(X1,szDzozmdt0(xc))
| aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f361,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f372,plain,
( ! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(xc,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
| ~ aElementOf0(W0,xT) )
& xK = sz00 ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f373,definition,
! [W1] :
( sP4_prd(W1)
<=> ( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f374,plain,
( ! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(xc,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| sP4_prd(W1) )
| ~ aElementOf0(W0,xT) )
& xK = sz00 ),
inference(formula_renaming,[status(thm)],[f372,f373]) ).
fof(f375,plain,
( ! [W0] :
( ! [W1] :
( ( sdtlpdtrp0(xc,sK23_skl(W1,W0)) != W0
& aElementOf0(sK23_skl(W1,W0),slbdtsldtrb0(W1,xK))
& sbrdtbr0(sK23_skl(W1,W0)) = xK
& aSubsetOf0(sK23_skl(W1,W0),W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,sK23_skl(W1,W0)) )
& aSet0(sK23_skl(W1,W0)) )
| sP4_prd(W1) )
| ~ aElementOf0(W0,xT) )
& xK = sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W2,sK23_skl(W1,W0))],[f374]) ).
fof(f376,plain,
xK = sz00,
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f377,plain,
! [X0,X1] :
( aSet0(sK23_skl(X1,X0))
| sP4_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f380,plain,
! [X0,X1] :
( sbrdtbr0(sK23_skl(X1,X0)) = xK
| sP4_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f382,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK23_skl(X1,X0)) != X0
| sP4_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f434,plain,
! [W1] :
( ( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP4_prd(W1) )
& ( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) )
| ~ sP4_prd(W1) ) ),
inference(NNF_transformation,[status(thm)],[f373]) ).
fof(f435,plain,
( ! [W1] :
( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP4_prd(W1) )
& ! [W1] :
( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) )
| ~ sP4_prd(W1) ) ),
inference(miniscoping,[status(thm)],[f434]) ).
fof(f436,plain,
( ! [W1] :
( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP4_prd(W1) )
& ! [W1] :
( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ( ~ aElementOf0(sK35_skl(W1),xS)
& aElementOf0(sK35_skl(W1),W1) )
| ~ aSet0(W1) ) )
| ~ sP4_prd(W1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(W2,sK35_skl(W1))],[f435]) ).
fof(f439,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xS)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f458,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f94]) ).
fof(f459,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f95]) ).
fof(f470,plain,
( sbrdtbr0(slcrc0) = sz00
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f203]) ).
fof(f498,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xc))
| aElementOf0(sdtlpdtrp0(xc,X0),sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(destructive_equality_resolution,[status(thm)],[f360]) ).
fof(f524,plain,
( ~ isCountable0(xS)
| ~ sP4_prd(xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f115,f439]) ).
fof(f525,plain,
( ~ isCountable0(xS)
| ~ sP4_prd(xS) ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f340]) ).
fof(f532,plain,
! [X0] :
( ~ aSet0(slcrc0)
| aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f110,f459]) ).
fof(f534,plain,
! [X0] :
( aSubsetOf0(slcrc0,X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f532,f458]) ).
fof(f542,plain,
~ sP4_prd(xS),
inference(forward_subsumption_resolution,[status(thm)],[f525,f343]) ).
fof(f545,plain,
! [X0,X1] :
( sbrdtbr0(sK23_skl(X1,X0)) = sz00
| sP4_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(forward_demodulation,[status(thm)],[f376,f380]) ).
fof(f584,plain,
sbrdtbr0(slcrc0) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f470,f458]) ).
fof(f603,plain,
! [X0,X1] :
( sP4_prd(X0)
| ~ aElementOf0(X1,xT)
| sK23_skl(X0,X1) = slcrc0
| sbrdtbr0(sK23_skl(X0,X1)) != sz00 ),
inference(resolution,[status(thm)],[f202,f377]) ).
fof(f606,plain,
! [X0,X1] :
( sP4_prd(X0)
| ~ aElementOf0(X1,xT)
| sK23_skl(X0,X1) = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f603,f545]) ).
fof(f628,plain,
! [X0] :
( ~ aElementOf0(X0,xT)
| sK23_skl(xS,X0) = slcrc0 ),
inference(resolution,[status(thm)],[f606,f542]) ).
fof(f635,plain,
! [X0] :
( sdtlpdtrp0(xc,sK23_skl(xS,X0)) != X0
| ~ aElementOf0(X0,xT) ),
inference(resolution,[status(thm)],[f382,f542]) ).
fof(f956,plain,
! [X0] :
( aElementOf0(X0,szDzozmdt0(xc))
| sbrdtbr0(X0) != sz00
| ~ aSubsetOf0(X0,xS) ),
inference(forward_demodulation,[status(thm)],[f376,f355]) ).
fof(f958,plain,
( ~ aSet0(xS)
| aElementOf0(slcrc0,szDzozmdt0(xc))
| sbrdtbr0(slcrc0) != sz00 ),
inference(resolution,[status(thm)],[f956,f534]) ).
fof(f960,plain,
( ~ aSet0(xS)
| aElementOf0(slcrc0,szDzozmdt0(xc))
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f584,f958]) ).
fof(f961,plain,
( ~ aSet0(xS)
| aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(trivial_equality_resolution,[status(thm)],[f960]) ).
fof(f962,plain,
aElementOf0(slcrc0,szDzozmdt0(xc)),
inference(forward_subsumption_resolution,[status(thm)],[f961,f340]) ).
fof(f1058,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xc))
| aElementOf0(sdtlpdtrp0(xc,X0),xT) ),
inference(resolution,[status(thm)],[f361,f498]) ).
fof(f1756,plain,
aElementOf0(sdtlpdtrp0(xc,slcrc0),xT),
inference(resolution,[status(thm)],[f1058,f962]) ).
fof(f1776,plain,
sdtlpdtrp0(xc,sK23_skl(xS,sdtlpdtrp0(xc,slcrc0))) != sdtlpdtrp0(xc,slcrc0),
inference(resolution,[status(thm)],[f1756,f635]) ).
fof(f1777,plain,
sK23_skl(xS,sdtlpdtrp0(xc,slcrc0)) = slcrc0,
inference(resolution,[status(thm)],[f1756,f628]) ).
fof(f21160,plain,
sdtlpdtrp0(xc,slcrc0) != sdtlpdtrp0(xc,slcrc0),
inference(forward_demodulation,[status(thm)],[f1777,f1776]) ).
fof(f21161,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f21160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM563+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 02:41:46 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 64.96/8.70 % Refutation found
% 64.96/8.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 64.96/8.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 53.34/8.76 % Elapsed time: 8.374497 seconds
% 53.34/8.76 % CPU time: 66.073105 seconds
% 53.34/8.76 % Total memory used: 404.555 MB
% 53.34/8.76 % Net memory used: 366.051 MB
%------------------------------------------------------------------------------