%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG122+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 02:05:03 PM UTC 2026
% Result : Theorem 0.19s 0.65s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 29
% Syntax : Number of formulae : 117 ( 26 unt; 16 def)
% Number of atoms : 529 ( 123 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 581 ( 169 ~; 166 |; 209 &)
% ( 25 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 15 prp; 0-3 aty)
% Number of functors : 32 ( 32 usr; 18 con; 0-3 aty)
% Number of variables : 169 ( 122 !; 47 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> aElement0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0] :
( aElement0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [W0] :
( aElement0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,definition,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( W1 = slsdtgt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) ) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aElement0(xb)
& aElement0(xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( ( aDivisorOf0(W0,xb)
| doDivides0(W0,xb)
| ? [W1] :
( sdtasdt0(W0,W1) = xb
& aElement0(W1) ) )
& ( aDivisorOf0(W0,xa)
| ( ( doDivides0(W0,xa)
| ? [W1] :
( sdtasdt0(W0,W1) = xa
& aElement0(W1) ) )
& aElement0(W0) ) ) )
=> ( doDivides0(W0,xc)
& ? [W1] :
( sdtasdt0(W0,W1) = xc
& aElement0(W1) ) ) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& ? [W0] :
( sdtasdt0(xc,W0) = xb
& aElement0(W0) )
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& ? [W0] :
( sdtasdt0(xc,W0) = xa
& aElement0(W0) )
& aElement0(xc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( aElementOf0(W0,xI)
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) ) )
& aIdeal0(xI)
& ! [W0] :
( aElementOf0(W0,xI)
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xI) )
& ! [W1] :
( aElementOf0(W1,xI)
=> aElementOf0(sdtpldt0(W0,W1),xI) ) ) )
& aSet0(xI) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( aElementOf0(xb,slsdtgt0(xb))
& ? [W0] :
( sdtasdt0(xb,W0) = xb
& aElement0(W0) )
& aElementOf0(sz00,slsdtgt0(xb))
& ? [W0] :
( sdtasdt0(xb,W0) = sz00
& aElement0(W0) )
& aElementOf0(xa,slsdtgt0(xa))
& ? [W0] :
( sdtasdt0(xa,W0) = xa
& aElement0(W0) )
& aElementOf0(sz00,slsdtgt0(xa))
& ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( ! [W0] :
( ( W0 != sz00
& ( aElementOf0(W0,xI)
| ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) ) )
=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [W0,W1] :
( sdtpldt0(W0,W1) = xu
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
( ( iLess0(sbrdtbr0(xr),sbrdtbr0(xu))
| xr = sz00 )
& xb = sdtpldt0(sdtasdt0(xq,xu),xr)
& aElement0(xr)
& aElement0(xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
( aElementOf0(smndt0(sdtasdt0(xq,xu)),xI)
& ? [W0,W1] :
( sdtpldt0(W0,W1) = smndt0(sdtasdt0(xq,xu))
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,conjecture,
xr = sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,negated_conjecture,
xr != sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb),
inference(negated_conjecture,[status(cth)],[f54]) ).
fof(f65,plain,
! [W0,W1] :
( aElement0(sdtasdt0(W0,W1))
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f66,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f69,plain,
! [W0,W1,W2] :
( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2))
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f70,plain,
! [X0,X1,X2] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f73,plain,
! [X0] :
( X0 = sdtpldt0(sz00,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [W0] :
( ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f76,plain,
! [X0] :
( sz00 = sdtpldt0(smndt0(X0),X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f99,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f100,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f195,plain,
! [W0] :
( ! [W1] :
( W1 = slsdtgt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) ) )
& aSet0(W1) ) )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f196,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| aElementOf0(W2,W1) )
& ( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slsdtgt0(W0) )
& ( ( ! [W2] :
( ( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| aElementOf0(W2,W1) )
& ( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| ~ aElementOf0(W2,W1) ) )
& aSet0(W1) )
| W1 != slsdtgt0(W0) ) )
| ~ aElement0(W0) ),
inference(NNF_transformation,[status(thm)],[f195]) ).
fof(f197,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| aElementOf0(W2,W1) )
& ( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slsdtgt0(W0) )
& ! [W1] :
( ( ! [W2] :
( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| aElementOf0(W2,W1) )
& ! [W2] :
( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slsdtgt0(W0) ) )
| ~ aElement0(W0) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f198,plain,
! [W0] :
( ( ! [W1] :
( ( ( ( sdtasdt0(W0,sK19_skl(W1,W0)) = sK18_skl(W1,W0)
& aElement0(sK19_skl(W1,W0)) )
| aElementOf0(sK18_skl(W1,W0),W1) )
& ( ! [W3] :
( sdtasdt0(W0,W3) != sK18_skl(W1,W0)
| ~ aElement0(W3) )
| ~ aElementOf0(sK18_skl(W1,W0),W1) ) )
| ~ aSet0(W1)
| W1 = slsdtgt0(W0) )
& ! [W1] :
( ( ! [W2] :
( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtasdt0(W0,sK17_skl(W2,W1,W0)) = W2
& aElement0(sK17_skl(W2,W1,W0)) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slsdtgt0(W0) ) )
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(W3,sK17_skl(W2,W1,W0)),skolemize(W2,sK18_skl(W1,W0)),skolemize(W3,sK19_skl(W1,W0))],[f197]) ).
fof(f199,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slsdtgt0(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f208,plain,
aElement0(xa),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f211,plain,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( doDivides0(W0,xc)
& ? [W1] :
( sdtasdt0(W0,W1) = xc
& aElement0(W1) ) )
| ( ~ aDivisorOf0(W0,xb)
& ~ doDivides0(W0,xb)
& ! [W1] :
( sdtasdt0(W0,W1) != xb
| ~ aElement0(W1) ) )
| ( ~ aDivisorOf0(W0,xa)
& ( ( ~ doDivides0(W0,xa)
& ! [W1] :
( sdtasdt0(W0,W1) != xa
| ~ aElement0(W1) ) )
| ~ aElement0(W0) ) ) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& ? [W0] :
( sdtasdt0(xc,W0) = xb
& aElement0(W0) )
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& ? [W0] :
( sdtasdt0(xc,W0) = xa
& aElement0(W0) )
& aElement0(xc) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f212,definition,
! [W0] :
( sP3_prd(W0)
<=> ( ( ~ aDivisorOf0(W0,xb)
& ~ doDivides0(W0,xb)
& ! [W1] :
( sdtasdt0(W0,W1) != xb
| ~ aElement0(W1) ) )
| ( ~ aDivisorOf0(W0,xa)
& ( ( ~ doDivides0(W0,xa)
& ! [W1] :
( sdtasdt0(W0,W1) != xa
| ~ aElement0(W1) ) )
| ~ aElement0(W0) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f213,plain,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( doDivides0(W0,xc)
& ? [W1] :
( sdtasdt0(W0,W1) = xc
& aElement0(W1) ) )
| sP3_prd(W0) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& ? [W0] :
( sdtasdt0(xc,W0) = xb
& aElement0(W0) )
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& ? [W0] :
( sdtasdt0(xc,W0) = xa
& aElement0(W0) )
& aElement0(xc) ),
inference(formula_renaming,[status(thm)],[f211,f212]) ).
fof(f214,plain,
( aGcdOfAnd0(xc,xa,xb)
& ! [W0] :
( ( doDivides0(W0,xc)
& sdtasdt0(W0,sK22_skl(W0)) = xc
& aElement0(sK22_skl(W0)) )
| sP3_prd(W0) )
& aDivisorOf0(xc,xb)
& doDivides0(xc,xb)
& sdtasdt0(xc,sK21_skl) = xb
& aElement0(sK21_skl)
& aElement0(xc)
& aDivisorOf0(xc,xa)
& doDivides0(xc,xa)
& sdtasdt0(xc,sK20_skl) = xa
& aElement0(sK20_skl)
& aElement0(xc) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl]),skolemize(W0,sK20_skl),skolemize(W0,sK21_skl),skolemize(W1,sK22_skl(W0))],[f213]) ).
fof(f215,plain,
aElement0(xc),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f216,plain,
aElement0(sK20_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f229,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( aElementOf0(W0,xI)
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) ) )
& aIdeal0(xI)
& ! [W0] :
( ( ! [W1] :
( aElementOf0(sdtasdt0(W1,W0),xI)
| ~ aElement0(W1) )
& ! [W1] :
( aElementOf0(sdtpldt0(W0,W1),xI)
| ~ aElementOf0(W1,xI) ) )
| ~ aElementOf0(W0,xI) )
& aSet0(xI) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f230,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( ( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) )
| aElementOf0(W0,xI) )
& ( ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) ) )
& ! [W0] :
( ( ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xb)) )
& ( ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xb)) ) )
& ! [W0] :
( ( ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xa)) )
& ( ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xa)) ) )
& aIdeal0(xI)
& ! [W0] :
( ( ! [W1] :
( aElementOf0(sdtasdt0(W1,W0),xI)
| ~ aElement0(W1) )
& ! [W1] :
( aElementOf0(sdtpldt0(W0,W1),xI)
| ~ aElementOf0(W1,xI) ) )
| ~ aElementOf0(W0,xI) )
& aSet0(xI) ),
inference(NNF_transformation,[status(thm)],[f229]) ).
fof(f231,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) )
| aElementOf0(W0,xI) )
& ! [W0] :
( ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) )
& ! [W0] :
( ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xb)) )
& ! [W0] :
( ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xb)) )
& ! [W0] :
( ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xa)) )
& ! [W0] :
( ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) )
| ~ aElementOf0(W0,slsdtgt0(xa)) )
& aIdeal0(xI)
& ! [W0] :
( ( ! [W1] :
( aElementOf0(sdtasdt0(W1,W0),xI)
| ~ aElement0(W1) )
& ! [W1] :
( aElementOf0(sdtpldt0(W0,W1),xI)
| ~ aElementOf0(W1,xI) ) )
| ~ aElementOf0(W0,xI) )
& aSet0(xI) ),
inference(miniscoping,[status(thm)],[f230]) ).
fof(f232,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) )
| aElementOf0(W0,xI) )
& ! [W0] :
( ( sdtpldt0(sK25_skl(W0),sK26_skl(W0)) = W0
& aElementOf0(sK26_skl(W0),slsdtgt0(xb))
& aElementOf0(sK25_skl(W0),slsdtgt0(xa)) )
| ~ aElementOf0(W0,xI) )
& ! [W0] :
( ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xb)) )
& ! [W0] :
( ( sdtasdt0(xb,sK24_skl(W0)) = W0
& aElement0(sK24_skl(W0)) )
| ~ aElementOf0(W0,slsdtgt0(xb)) )
& ! [W0] :
( ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) )
| aElementOf0(W0,slsdtgt0(xa)) )
& ! [W0] :
( ( sdtasdt0(xa,sK23_skl(W0)) = W0
& aElement0(sK23_skl(W0)) )
| ~ aElementOf0(W0,slsdtgt0(xa)) )
& aIdeal0(xI)
& ! [W0] :
( ( ! [W1] :
( aElementOf0(sdtasdt0(W1,W0),xI)
| ~ aElement0(W1) )
& ! [W1] :
( aElementOf0(sdtpldt0(W0,W1),xI)
| ~ aElementOf0(W1,xI) ) )
| ~ aElementOf0(W0,xI) )
& aSet0(xI) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(W1,sK23_skl(W0)),skolemize(W1,sK24_skl(W0)),skolemize(W1,sK25_skl(W0)),skolemize(W2,sK26_skl(W0))],[f231]) ).
fof(f233,plain,
aSet0(xI),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f248,plain,
( aElementOf0(xb,slsdtgt0(xb))
& sdtasdt0(xb,sK30_skl) = xb
& aElement0(sK30_skl)
& aElementOf0(sz00,slsdtgt0(xb))
& sdtasdt0(xb,sK29_skl) = sz00
& aElement0(sK29_skl)
& aElementOf0(xa,slsdtgt0(xa))
& sdtasdt0(xa,sK28_skl) = xa
& aElement0(sK28_skl)
& aElementOf0(sz00,slsdtgt0(xa))
& sdtasdt0(xa,sK27_skl) = sz00
& aElement0(sK27_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl,sK29_skl,sK30_skl]),skolemize(W0,sK27_skl),skolemize(W0,sK28_skl),skolemize(W0,sK29_skl),skolemize(W0,sK30_skl)],[f43]) ).
fof(f249,plain,
aElement0(sK27_skl),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f252,plain,
aElement0(sK28_skl),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f275,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| W0 = sz00
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [W0,W1] :
( sdtpldt0(W0,W1) = xu
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f276,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| W0 = sz00
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& sdtpldt0(sK36_skl,sK37_skl) = xu
& aElementOf0(sK37_skl,slsdtgt0(xb))
& aElementOf0(sK36_skl,slsdtgt0(xa)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl]),skolemize(W0,sK36_skl),skolemize(W1,sK37_skl)],[f275]) ).
fof(f280,plain,
aElementOf0(xu,xI),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f301,plain,
aElement0(xq),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f302,plain,
aElement0(xr),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f303,plain,
xb = sdtpldt0(sdtasdt0(xq,xu),xr),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f306,plain,
( aElementOf0(smndt0(sdtasdt0(xq,xu)),xI)
& sdtpldt0(sK41_skl,sK42_skl) = smndt0(sdtasdt0(xq,xu))
& aElementOf0(sK42_skl,slsdtgt0(xb))
& aElementOf0(sK41_skl,slsdtgt0(xa)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl]),skolemize(W0,sK41_skl),skolemize(W1,sK42_skl)],[f52]) ).
fof(f309,plain,
sdtpldt0(sK41_skl,sK42_skl) = smndt0(sdtasdt0(xq,xu)),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f310,plain,
aElementOf0(smndt0(sdtasdt0(xq,xu)),xI),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f319,plain,
xr != sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f422,plain,
! [X0] :
( aSet0(slsdtgt0(X0))
| ~ aElement0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f199]) ).
fof(f433,plain,
aElementOf0(sdtpldt0(sK41_skl,sK42_skl),xI),
inference(forward_demodulation,[status(thm)],[f309,f310]) ).
fof(f434,plain,
xr != sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),xb),
inference(forward_demodulation,[status(thm)],[f309,f319]) ).
fof(f444,definition,
( sQ13_spl
<=> aElement0(sdtasdt0(xq,xu)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f446,plain,
( sQ13_spl
| ~ aElement0(sdtasdt0(xq,xu)) ),
inference(component_clause,[status(thm)],[f444]) ).
fof(f447,definition,
( sQ14_spl
<=> aElement0(xr) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( sQ14_spl
| ~ aElement0(xr) ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f463,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f449,f302]) ).
fof(f464,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f463]) ).
fof(f465,plain,
( sQ13_spl
| ~ aElement0(xu)
| ~ aElement0(xq) ),
inference(resolution,[status(thm)],[f446,f66]) ).
fof(f466,definition,
( sQ18_spl
<=> aElement0(xq) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( sQ18_spl
| ~ aElement0(xq) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ19_spl
<=> aElement0(xu) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( sQ13_spl
| ~ sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f465,f466,f469,f444]) ).
fof(f473,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f301]) ).
fof(f474,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f473]) ).
fof(f621,plain,
( sz00 = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),sdtasdt0(xq,xu))
| ~ aElement0(sdtasdt0(xq,xu)) ),
inference(paramodulation,[status(thm)],[f309,f76]) ).
fof(f624,definition,
( sQ50_spl
<=> sz00 = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),sdtasdt0(xq,xu)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( ~ sQ50_spl
| sz00 = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),sdtasdt0(xq,xu)) ),
inference(component_clause,[status(thm)],[f624]) ).
fof(f627,plain,
( sQ50_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f621,f444,f624]) ).
fof(f632,definition,
( sQ52_spl
<=> aElement0(sdtpldt0(sK41_skl,sK42_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f772,plain,
( aElement0(xu)
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f100,f280]) ).
fof(f774,plain,
( aElement0(sdtpldt0(sK41_skl,sK42_skl))
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f100,f433]) ).
fof(f775,definition,
( sQ66_spl
<=> aSet0(xI) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( sQ66_spl
| ~ aSet0(xI) ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f778,plain,
( sQ19_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f772,f775,f469]) ).
fof(f780,plain,
( sQ52_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f774,f775,f632]) ).
fof(f781,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f233]) ).
fof(f782,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f781]) ).
fof(f803,plain,
! [X0] :
( ~ sQ50_spl
| sdtpldt0(sz00,X0) = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),sdtpldt0(sdtasdt0(xq,xu),X0))
| ~ aElement0(X0)
| ~ aElement0(sdtasdt0(xq,xu))
| ~ aElement0(sdtpldt0(sK41_skl,sK42_skl)) ),
inference(paramodulation,[status(thm)],[f625,f70]) ).
fof(f815,definition,
! [X0] :
( sQ71_spl
<=> ( sdtpldt0(sz00,X0) = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),sdtpldt0(sdtasdt0(xq,xu),X0))
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f816,plain,
! [X0] :
( ~ sQ71_spl
| sdtpldt0(sz00,X0) = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),sdtpldt0(sdtasdt0(xq,xu),X0))
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f815]) ).
fof(f818,plain,
( ~ sQ50_spl
| sQ71_spl
| ~ sQ13_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f803,f632,f444,f815,f624]) ).
fof(f915,definition,
( sQ79_spl
<=> aElement0(sK20_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f917,plain,
( sQ79_spl
| ~ aElement0(sK20_skl) ),
inference(component_clause,[status(thm)],[f915]) ).
fof(f921,definition,
( sQ81_spl
<=> aElement0(xc) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ81_spl
| ~ aElement0(xc) ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f943,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f917,f216]) ).
fof(f944,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f943]) ).
fof(f945,plain,
( sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f215]) ).
fof(f946,plain,
sQ81_spl,
inference(contradiction_clause,[status(thm)],[f945]) ).
fof(f954,definition,
( sQ86_spl
<=> aElement0(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( sQ86_spl
| ~ aElement0(sK27_skl) ),
inference(component_clause,[status(thm)],[f954]) ).
fof(f982,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f956,f249]) ).
fof(f983,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f982]) ).
fof(f1087,definition,
( sQ111_spl
<=> aSet0(slsdtgt0(xa)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1089,plain,
( sQ111_spl
| ~ aSet0(slsdtgt0(xa)) ),
inference(component_clause,[status(thm)],[f1087]) ).
fof(f1098,definition,
( sQ112_spl
<=> aElement0(sK28_skl) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1100,plain,
( sQ112_spl
| ~ aElement0(sK28_skl) ),
inference(component_clause,[status(thm)],[f1098]) ).
fof(f1126,plain,
( sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1100,f252]) ).
fof(f1127,plain,
sQ112_spl,
inference(contradiction_clause,[status(thm)],[f1126]) ).
fof(f1130,plain,
( sQ111_spl
| ~ aElement0(xa) ),
inference(resolution,[status(thm)],[f1089,f422]) ).
fof(f1131,plain,
( sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1130,f208]) ).
fof(f1132,plain,
sQ111_spl,
inference(contradiction_clause,[status(thm)],[f1131]) ).
fof(f1337,plain,
( ~ sQ71_spl
| sdtpldt0(sz00,xr) = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),xb)
| ~ aElement0(xr) ),
inference(paramodulation,[status(thm)],[f303,f816]) ).
fof(f1350,definition,
( sQ153_spl
<=> sdtpldt0(sz00,xr) = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),xb) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1351,plain,
( ~ sQ153_spl
| sdtpldt0(sz00,xr) = sdtpldt0(sdtpldt0(sK41_skl,sK42_skl),xb) ),
inference(component_clause,[status(thm)],[f1350]) ).
fof(f1353,plain,
( ~ sQ71_spl
| sQ153_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1337,f447,f1350,f815]) ).
fof(f1354,plain,
( ~ sQ153_spl
| xr != sdtpldt0(sz00,xr) ),
inference(backward_demodulation,[status(thm)],[f1351,f434]) ).
fof(f1355,plain,
( ~ sQ153_spl
| ~ aElement0(xr) ),
inference(resolution,[status(thm)],[f1354,f73]) ).
fof(f1356,plain,
( ~ sQ153_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1355,f447,f1350]) ).
fof(f1357,plain,
$false,
inference(sat_refutation,[status(thm)],[f464,f472,f474,f627,f778,f780,f782,f818,f944,f946,f983,f1127,f1132,f1353,f1356]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG122+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n019.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 04:22:05 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.50 % Drodi V4.1.1
% 0.19/0.65 % Refutation found
% 0.19/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.69 % Elapsed time: 0.216477 seconds
% 0.27/0.69 % CPU time: 1.113121 seconds
% 0.27/0.69 % Total memory used: 122.384 MB
% 0.27/0.69 % Net memory used: 121.398 MB
%------------------------------------------------------------------------------