%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM566+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 : n015.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 1.23s 0.71s
% Output : CNFRefutation 1.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of formulae : 66 ( 13 unt; 2 def)
% Number of atoms : 390 ( 51 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 472 ( 148 ~; 138 |; 164 &)
% ( 4 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-2 aty)
% Number of variables : 130 ( 107 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ),
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,hypothesis,
xK = sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
( aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00))
& aSubsetOf0(slcrc0,xS)
& ! [W0] :
( aElementOf0(W0,slcrc0)
=> aElementOf0(W0,xS) )
& ~ ? [W0] : aElementOf0(W0,slcrc0)
& aSet0(slcrc0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xS,sz00))
| ( sbrdtbr0(W0) = sz00
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSet0(W0) ) ) ) )
=> ( sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0)
& ~ ? [W1] : aElementOf0(W1,slcrc0)
& aSet0(slcrc0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,conjecture,
? [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(f82,negated_conjecture,
~ ? [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)],[f81]) ).
fof(f117,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f118,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f319,plain,
! [W0] :
( ! [W1] :
( aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0)))
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f320,plain,
! [X0,X1] :
( aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f342,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f343,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f346,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f347,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(f348,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)],[f347]) ).
fof(f349,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)],[f348]) ).
fof(f350,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))],[f349]) ).
fof(f351,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f359,plain,
szDzozmdt0(xc) = slbdtsldtrb0(xS,xK),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f364,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f375,plain,
xK = sz00,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f376,plain,
( aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00))
& aSubsetOf0(slcrc0,xS)
& ! [W0] :
( aElementOf0(W0,xS)
| ~ aElementOf0(W0,slcrc0) )
& ! [W0] : ~ aElementOf0(W0,slcrc0)
& aSet0(slcrc0) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f381,plain,
aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f382,plain,
! [W0] :
( ( sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0)
& ! [W1] : ~ aElementOf0(W1,slcrc0)
& aSet0(slcrc0) )
| ( ~ aElementOf0(W0,slbdtsldtrb0(xS,sz00))
& ( sbrdtbr0(W0) != sz00
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f80]) ).
fof(f383,definition,
! [W0] :
( sP4_prd(W0)
<=> ( ~ aElementOf0(W0,slbdtsldtrb0(xS,sz00))
& ( sbrdtbr0(W0) != sz00
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f384,plain,
! [W0] :
( ( sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0)
& ! [W1] : ~ aElementOf0(W1,slcrc0)
& aSet0(slcrc0) )
| sP4_prd(W0) ),
inference(formula_renaming,[status(thm)],[f382,f383]) ).
fof(f387,plain,
! [X0] :
( sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0)
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f388,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) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f389,definition,
! [W1] :
( sP5_prd(W1)
<=> ( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f390,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) )
| sP5_prd(W1) )
| ~ aElementOf0(W0,xT) ),
inference(formula_renaming,[status(thm)],[f388,f389]) ).
fof(f391,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)) )
| sP5_prd(W1) )
| ~ aElementOf0(W0,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W2,sK23_skl(W1,W0))],[f390]) ).
fof(f396,plain,
! [X0,X1] :
( aElementOf0(sK23_skl(X1,X0),slbdtsldtrb0(X1,xK))
| sP5_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f397,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK23_skl(X1,X0)) != X0
| sP5_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f449,plain,
! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xS,sz00))
| ( sbrdtbr0(W0) = sz00
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ) )
| sP4_prd(W0) )
& ( ( ~ aElementOf0(W0,slbdtsldtrb0(xS,sz00))
& ( sbrdtbr0(W0) != sz00
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) )
| ~ sP4_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f383]) ).
fof(f450,plain,
( ! [W0] :
( aElementOf0(W0,slbdtsldtrb0(xS,sz00))
| ( sbrdtbr0(W0) = sz00
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ) )
| sP4_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,slbdtsldtrb0(xS,sz00))
& ( sbrdtbr0(W0) != sz00
| ( ~ aSubsetOf0(W0,xS)
& ( ? [W1] :
( ~ aElementOf0(W1,xS)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) )
| ~ sP4_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f449]) ).
fof(f451,plain,
( ! [W0] :
( aElementOf0(W0,slbdtsldtrb0(xS,sz00))
| ( sbrdtbr0(W0) = sz00
& ( aSubsetOf0(W0,xS)
| ( ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ) )
| sP4_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,slbdtsldtrb0(xS,sz00))
& ( sbrdtbr0(W0) != sz00
| ( ~ aSubsetOf0(W0,xS)
& ( ( ~ aElementOf0(sK35_skl(W0),xS)
& aElementOf0(sK35_skl(W0),W0) )
| ~ aSet0(W0) ) ) ) )
| ~ sP4_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(W1,sK35_skl(W0))],[f450]) ).
fof(f455,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xS,sz00))
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f451]) ).
fof(f459,plain,
! [W1] :
( ( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP5_prd(W1) )
& ( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) )
| ~ sP5_prd(W1) ) ),
inference(NNF_transformation,[status(thm)],[f389]) ).
fof(f460,plain,
( ! [W1] :
( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP5_prd(W1) )
& ! [W1] :
( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) )
| ~ sP5_prd(W1) ) ),
inference(miniscoping,[status(thm)],[f459]) ).
fof(f461,plain,
( ! [W1] :
( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP5_prd(W1) )
& ! [W1] :
( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ( ~ aElementOf0(sK36_skl(W1),xS)
& aElementOf0(sK36_skl(W1),W1) )
| ~ aSet0(W1) ) )
| ~ sP5_prd(W1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(W2,sK36_skl(W1))],[f460]) ).
fof(f464,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xS)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f573,plain,
( ~ isCountable0(xS)
| ~ sP5_prd(xS)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f118,f464]) ).
fof(f575,plain,
( ~ isCountable0(xS)
| ~ sP5_prd(xS) ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f343]) ).
fof(f576,plain,
~ sP5_prd(xS),
inference(forward_subsumption_resolution,[status(thm)],[f575,f346]) ).
fof(f641,plain,
! [X0] :
( aElementOf0(sK23_skl(xS,X0),szDzozmdt0(xc))
| sP5_prd(xS)
| ~ aElementOf0(X0,xT) ),
inference(paramodulation,[status(thm)],[f359,f396]) ).
fof(f642,plain,
! [X0] :
( aElementOf0(sK23_skl(xS,X0),szDzozmdt0(xc))
| ~ aElementOf0(X0,xT) ),
inference(forward_subsumption_resolution,[status(thm)],[f641,f576]) ).
fof(f698,plain,
aElementOf0(slcrc0,slbdtsldtrb0(xS,xK)),
inference(forward_demodulation,[status(thm)],[f375,f381]) ).
fof(f699,plain,
aElementOf0(slcrc0,szDzozmdt0(xc)),
inference(forward_demodulation,[status(thm)],[f359,f698]) ).
fof(f861,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xS,xK))
| ~ sP4_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f375,f455]) ).
fof(f862,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xc))
| ~ sP4_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f359,f861]) ).
fof(f863,plain,
~ sP4_prd(slcrc0),
inference(resolution,[status(thm)],[f862,f699]) ).
fof(f864,plain,
! [X0] :
( ~ aElementOf0(X0,xT)
| ~ sP4_prd(sK23_skl(xS,X0)) ),
inference(resolution,[status(thm)],[f862,f642]) ).
fof(f1028,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xc))
| ~ aFunction0(xc)
| aElementOf0(sdtlpdtrp0(xc,X0),xT) ),
inference(resolution,[status(thm)],[f364,f320]) ).
fof(f1035,plain,
! [X0] :
( ~ aElementOf0(X0,szDzozmdt0(xc))
| aElementOf0(sdtlpdtrp0(xc,X0),xT) ),
inference(forward_subsumption_resolution,[status(thm)],[f1028,f351]) ).
fof(f1275,plain,
! [X0,X1] :
( sP4_prd(X1)
| sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,X1)
| sP4_prd(X0) ),
inference(paramodulation,[status(thm)],[f387,f387]) ).
fof(f2058,plain,
! [X0] :
( sP4_prd(X0)
| ~ aElementOf0(slcrc0,szDzozmdt0(xc))
| aElementOf0(sdtlpdtrp0(xc,X0),xT) ),
inference(paramodulation,[status(thm)],[f387,f1035]) ).
fof(f2060,plain,
! [X0] :
( sP4_prd(X0)
| aElementOf0(sdtlpdtrp0(xc,X0),xT) ),
inference(forward_subsumption_resolution,[status(thm)],[f2058,f699]) ).
fof(f2276,plain,
! [X0,X1] :
( sP5_prd(X0)
| ~ aElementOf0(sdtlpdtrp0(xc,X1),xT)
| sP4_prd(X1)
| sP4_prd(sK23_skl(X0,sdtlpdtrp0(xc,X1))) ),
inference(resolution,[status(thm)],[f1275,f397]) ).
fof(f2310,plain,
! [X0,X1] :
( sP5_prd(X0)
| sP4_prd(X1)
| sP4_prd(sK23_skl(X0,sdtlpdtrp0(xc,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2276,f2060]) ).
fof(f2338,plain,
! [X0] :
( ~ aElementOf0(sdtlpdtrp0(xc,X0),xT)
| sP5_prd(xS)
| sP4_prd(X0) ),
inference(resolution,[status(thm)],[f2310,f864]) ).
fof(f2343,plain,
! [X0] :
( ~ aElementOf0(sdtlpdtrp0(xc,X0),xT)
| sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2338,f576]) ).
fof(f2354,plain,
! [X0] : sP4_prd(X0),
inference(forward_subsumption_resolution,[status(thm)],[f2343,f2060]) ).
fof(f2355,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f863,f2354]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM566+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n015.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:43:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 1.23/0.71 % Refutation found
% 1.23/0.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.23/0.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.23/0.73 % Elapsed time: 0.367342 seconds
% 1.23/0.73 % CPU time: 2.572552 seconds
% 1.23/0.73 % Total memory used: 147.378 MB
% 1.23/0.73 % Net memory used: 144.371 MB
%------------------------------------------------------------------------------