%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG092+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:04:56 PM UTC 2026
% Result : Theorem 0.28s 0.72s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 20
% Syntax : Number of formulae : 99 ( 13 unt; 16 def)
% Number of atoms : 580 ( 65 equ)
% Maximal formula atoms : 39 ( 5 avg)
% Number of connectives : 667 ( 186 ~; 175 |; 262 &)
% ( 21 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 14 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 6 con; 0-3 aty)
% Number of variables : 263 ( 169 !; 94 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aElement0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,definition,
! [W0] :
( aIdeal0(W0)
<=> ( ! [W1] :
( aElementOf0(W1,W0)
=> ( ! [W2] :
( aElement0(W2)
=> aElementOf0(sdtasdt0(W2,W1),W0) )
& ! [W2] :
( aElementOf0(W2,W0)
=> aElementOf0(sdtpldt0(W1,W2),W0) ) ) )
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
( aIdeal0(xJ)
& ! [W0] :
( aElementOf0(W0,xJ)
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xJ) )
& ! [W1] :
( aElementOf0(W1,xJ)
=> aElementOf0(sdtpldt0(W0,W1),xJ) ) ) )
& aSet0(xJ)
& 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/sandbox/benchmark/theBenchmark.p') ).
fof(f26,conjecture,
( ! [W0,W1,W2] :
( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W1
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W0
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) )
=> ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) ) )
& aSet0(sdtpldt1(xI,xJ)) )
=> ( aIdeal0(sdtpldt1(xI,xJ))
| ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ)) )
& ! [W1] :
( aElementOf0(W1,sdtpldt1(xI,xJ))
=> aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
~ ( ! [W0,W1,W2] :
( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W1
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W0
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) )
=> ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) ) )
& aSet0(sdtpldt1(xI,xJ)) )
=> ( aIdeal0(sdtpldt1(xI,xJ))
| ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ)) )
& ! [W1] :
( aElementOf0(W1,sdtpldt1(xI,xJ))
=> aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ)) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f31,plain,
aElement0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f71,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f72,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f101,plain,
! [W0] :
( aIdeal0(W0)
<=> ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f102,plain,
! [W0] :
( ( ? [W1] :
( ( ? [W2] :
( ~ aElementOf0(sdtasdt0(W2,W1),W0)
& aElement0(W2) )
| ? [W2] :
( ~ aElementOf0(sdtpldt0(W1,W2),W0)
& aElementOf0(W2,W0) ) )
& aElementOf0(W1,W0) )
| ~ aSet0(W0)
| aIdeal0(W0) )
& ( ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aIdeal0(W0) ) ),
inference(NNF_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
( ! [W0] :
( ? [W1] :
( ( ? [W2] :
( ~ aElementOf0(sdtasdt0(W2,W1),W0)
& aElement0(W2) )
| ? [W2] :
( ~ aElementOf0(sdtpldt0(W1,W2),W0)
& aElementOf0(W2,W0) ) )
& aElementOf0(W1,W0) )
| ~ aSet0(W0)
| aIdeal0(W0) )
& ! [W0] :
( ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aIdeal0(W0) ) ),
inference(miniscoping,[status(thm)],[f102]) ).
fof(f104,plain,
( ! [W0] :
( ( ( ( ~ aElementOf0(sdtasdt0(sK10_skl(W0),sK8_skl(W0)),W0)
& aElement0(sK10_skl(W0)) )
| ( ~ aElementOf0(sdtpldt0(sK8_skl(W0),sK9_skl(W0)),W0)
& aElementOf0(sK9_skl(W0),W0) ) )
& aElementOf0(sK8_skl(W0),W0) )
| ~ aSet0(W0)
| aIdeal0(W0) )
& ! [W0] :
( ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aIdeal0(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl]),skolemize(W1,sK8_skl(W0)),skolemize(W2,sK9_skl(W0)),skolemize(W2,sK10_skl(W0))],[f103]) ).
fof(f108,plain,
! [X0] :
( aElementOf0(sK8_skl(X0),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f113,plain,
( aIdeal0(xJ)
& ! [W0] :
( ( ! [W1] :
( aElementOf0(sdtasdt0(W1,W0),xJ)
| ~ aElement0(W1) )
& ! [W1] :
( aElementOf0(sdtpldt0(W0,W1),xJ)
| ~ aElementOf0(W1,xJ) ) )
| ~ aElementOf0(W0,xJ) )
& aSet0(xJ)
& 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)],[f25]) ).
fof(f118,plain,
aSet0(xJ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f122,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [W0] :
( ( ? [W1] :
( ~ aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ))
& aElement0(W1) )
| ? [W1] :
( ~ aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& aElementOf0(W1,sdtpldt1(xI,xJ)) ) )
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) ) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| ~ aElement0(W2)
| ( ~ aElementOf0(W1,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W1
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ( ~ aElementOf0(W0,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W0
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f123,definition,
! [W0,W1,W2] :
( sP2_prd(W2,W1,W0)
<=> ( ~ aElement0(W2)
| ( ~ aElementOf0(W1,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W1
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ( ~ aElementOf0(W0,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W0
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f124,definition,
! [W0,W1] :
( sP3_prd(W1,W0)
<=> ( ~ aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& aElementOf0(W1,sdtpldt1(xI,xJ)) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f125,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [W0] :
( ( ? [W1] :
( ~ aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ))
& aElement0(W1) )
| ? [W1] : sP3_prd(W1,W0) )
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) ) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| sP2_prd(W2,W1,W0) ) ),
inference(formula_renaming,[status(thm)],[f122,f124,f123]) ).
fof(f126,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [W0] :
( ( ? [W1] :
( ~ aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ))
& aElement0(W1) )
| ? [W1] : sP3_prd(W1,W0) )
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( ( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,xJ)
| ~ aElementOf0(W1,xI) )
| aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ( ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) )
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) ) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| sP2_prd(W2,W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [W0] :
( ( ? [W1] :
( ~ aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ))
& aElement0(W1) )
| ? [W1] : sP3_prd(W1,W0) )
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,xJ)
| ~ aElementOf0(W1,xI) )
| aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) )
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& ? [W5,W6] :
( sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| sP2_prd(W2,W1,W0) ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ( ( ~ aElementOf0(sdtasdt0(sK23_skl,sK21_skl),sdtpldt1(xI,xJ))
& aElement0(sK23_skl) )
| sP3_prd(sK22_skl,sK21_skl) )
& aElementOf0(sK21_skl,sdtpldt1(xI,xJ))
& ! [W0] :
( ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,xJ)
| ~ aElementOf0(W1,xI) )
| aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( ( sdtpldt0(sK19_skl(W0),sK20_skl(W0)) = W0
& aElementOf0(sK20_skl(W0),xJ)
& aElementOf0(sK19_skl(W0),xI) )
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& sdtpldt0(sK17_skl(W2,W1,W0),sK18_skl(W2,W1,W0)) = sdtasdt0(W2,W0)
& aElementOf0(sK18_skl(W2,W1,W0),xJ)
& aElementOf0(sK17_skl(W2,W1,W0),xI)
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& sdtpldt0(sK15_skl(W2,W1,W0),sK16_skl(W2,W1,W0)) = sdtpldt0(W0,W1)
& aElementOf0(sK16_skl(W2,W1,W0),xJ)
& aElementOf0(sK15_skl(W2,W1,W0),xI)
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(sK11_skl(W2,W1,W0),sK13_skl(W2,W1,W0)),sdtpldt0(sK12_skl(W2,W1,W0),sK14_skl(W2,W1,W0)))
& aElementOf0(sdtasdt0(W2,sK12_skl(W2,W1,W0)),xJ)
& aElementOf0(sdtasdt0(W2,sK11_skl(W2,W1,W0)),xI)
& aElementOf0(sdtpldt0(sK12_skl(W2,W1,W0),sK14_skl(W2,W1,W0)),xJ)
& aElementOf0(sdtpldt0(sK11_skl(W2,W1,W0),sK13_skl(W2,W1,W0)),xI)
& W1 = sdtpldt0(sK13_skl(W2,W1,W0),sK14_skl(W2,W1,W0))
& aElementOf0(sK14_skl(W2,W1,W0),xJ)
& aElementOf0(sK13_skl(W2,W1,W0),xI)
& W0 = sdtpldt0(sK11_skl(W2,W1,W0),sK12_skl(W2,W1,W0))
& aElementOf0(sK12_skl(W2,W1,W0),xJ)
& aElementOf0(sK11_skl(W2,W1,W0),xI) )
| sP2_prd(W2,W1,W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl]),skolemize(W3,sK11_skl(W2,W1,W0)),skolemize(W4,sK12_skl(W2,W1,W0)),skolemize(W5,sK13_skl(W2,W1,W0)),skolemize(W6,sK14_skl(W2,W1,W0)),skolemize(W7,sK15_skl(W2,W1,W0)),skolemize(W8,sK16_skl(W2,W1,W0)),skolemize(W7,sK17_skl(W2,W1,W0)),skolemize(W8,sK18_skl(W2,W1,W0)),skolemize(W1,sK19_skl(W0)),skolemize(W2,sK20_skl(W0)),skolemize(W0,sK21_skl),skolemize(W1,sK22_skl),skolemize(W1,sK23_skl)],[f127]) ).
fof(f143,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(X2,X1),sdtpldt1(xI,xJ))
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f147,plain,
! [X0,X1,X2] :
( aElementOf0(sdtasdt0(X0,X2),sdtpldt1(xI,xJ))
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f148,plain,
aSet0(sdtpldt1(xI,xJ)),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f150,plain,
! [X0] :
( aElementOf0(sK20_skl(X0),xJ)
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f153,plain,
aElementOf0(sK21_skl,sdtpldt1(xI,xJ)),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f154,plain,
( aElement0(sK23_skl)
| sP3_prd(sK22_skl,sK21_skl) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f155,plain,
( ~ aElementOf0(sdtasdt0(sK23_skl,sK21_skl),sdtpldt1(xI,xJ))
| sP3_prd(sK22_skl,sK21_skl) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f156,plain,
~ aIdeal0(sdtpldt1(xI,xJ)),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f168,plain,
! [W0,W1,W2] :
( ( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W1
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W0
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) )
| sP2_prd(W2,W1,W0) )
& ( ~ aElement0(W2)
| ( ~ aElementOf0(W1,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W1
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ( ~ aElementOf0(W0,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W0
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ~ sP2_prd(W2,W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f123]) ).
fof(f169,plain,
( ! [W0,W1,W2] :
( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W1
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W0
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) )
| sP2_prd(W2,W1,W0) )
& ! [W0,W1,W2] :
( ~ aElement0(W2)
| ( ~ aElementOf0(W1,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W1
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ( ~ aElementOf0(W0,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W0
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ~ sP2_prd(W2,W1,W0) ) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f170,plain,
( ! [W0,W1,W2] :
( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ( sdtpldt0(sK26_skl(W2,W1,W0),sK27_skl(W2,W1,W0)) = W1
& aElementOf0(sK27_skl(W2,W1,W0),xJ)
& aElementOf0(sK26_skl(W2,W1,W0),xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ( sdtpldt0(sK24_skl(W2,W1,W0),sK25_skl(W2,W1,W0)) = W0
& aElementOf0(sK25_skl(W2,W1,W0),xJ)
& aElementOf0(sK24_skl(W2,W1,W0),xI) ) ) )
| sP2_prd(W2,W1,W0) )
& ! [W0,W1,W2] :
( ~ aElement0(W2)
| ( ~ aElementOf0(W1,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W1
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ( ~ aElementOf0(W0,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W0
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ~ sP2_prd(W2,W1,W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl,sK27_skl]),skolemize(W3,sK24_skl(W2,W1,W0)),skolemize(W4,sK25_skl(W2,W1,W0)),skolemize(W3,sK26_skl(W2,W1,W0)),skolemize(W4,sK27_skl(W2,W1,W0))],[f169]) ).
fof(f174,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f182,plain,
! [W0,W1] :
( ( aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
| ~ aElementOf0(W1,sdtpldt1(xI,xJ))
| sP3_prd(W1,W0) )
& ( ( ~ aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& aElementOf0(W1,sdtpldt1(xI,xJ)) )
| ~ sP3_prd(W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f124]) ).
fof(f183,plain,
( ! [W0,W1] :
( aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
| ~ aElementOf0(W1,sdtpldt1(xI,xJ))
| sP3_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& aElementOf0(W1,sdtpldt1(xI,xJ)) )
| ~ sP3_prd(W1,W0) ) ),
inference(miniscoping,[status(thm)],[f182]) ).
fof(f184,plain,
! [X0,X1] :
( aElementOf0(X0,sdtpldt1(xI,xJ))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f185,plain,
! [X0,X1] :
( ~ aElementOf0(sdtpldt0(X1,X0),sdtpldt1(xI,xJ))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f187,definition,
( sQ0_spl
<=> sP3_prd(sK22_skl,sK21_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f188,plain,
( ~ sQ0_spl
| sP3_prd(sK22_skl,sK21_skl) ),
inference(component_clause,[status(thm)],[f187]) ).
fof(f190,definition,
( sQ1_spl
<=> aElement0(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( ~ sQ1_spl
| aElement0(sK23_skl) ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f154,f187,f190]) ).
fof(f194,definition,
( sQ2_spl
<=> aElementOf0(sdtasdt0(sK23_skl,sK21_skl),sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( sQ2_spl
| ~ aElementOf0(sdtasdt0(sK23_skl,sK21_skl),sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,plain,
( ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f155,f187,f194]) ).
fof(f222,definition,
( sQ5_spl
<=> aSet0(sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( sQ5_spl
| ~ aSet0(sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f233,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f224,f148]) ).
fof(f234,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f233]) ).
fof(f244,definition,
( sQ9_spl
<=> aSet0(xJ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f246,plain,
( sQ9_spl
| ~ aSet0(xJ) ),
inference(component_clause,[status(thm)],[f244]) ).
fof(f258,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f246,f118]) ).
fof(f259,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f258]) ).
fof(f307,definition,
( sQ19_spl
<=> aIdeal0(sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( ~ sQ19_spl
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f332,plain,
( ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ))
| aElementOf0(sK20_skl(sK8_skl(sdtpldt1(xI,xJ))),xJ) ),
inference(resolution,[status(thm)],[f150,f108]) ).
fof(f339,definition,
( sQ25_spl
<=> aElementOf0(sK20_skl(sK8_skl(sdtpldt1(xI,xJ))),xJ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( ~ sQ25_spl
| aElementOf0(sK20_skl(sK8_skl(sdtpldt1(xI,xJ))),xJ) ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,plain,
( ~ sQ5_spl
| sQ19_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f332,f339,f307,f222]) ).
fof(f355,definition,
( sQ28_spl
<=> aElement0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( sQ28_spl
| ~ aElement0(sz00) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f381,plain,
( ~ sQ25_spl
| aElement0(sK20_skl(sK8_skl(sdtpldt1(xI,xJ))))
| ~ aSet0(xJ) ),
inference(resolution,[status(thm)],[f340,f72]) ).
fof(f382,definition,
( sQ33_spl
<=> aElement0(sK20_skl(sK8_skl(sdtpldt1(xI,xJ)))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f383,plain,
( ~ sQ33_spl
| aElement0(sK20_skl(sK8_skl(sdtpldt1(xI,xJ)))) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f385,plain,
( ~ sQ25_spl
| sQ33_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f381,f244,f382,f339]) ).
fof(f401,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f156]) ).
fof(f402,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f401]) ).
fof(f431,plain,
! [X0,X1,X2] :
( ~ sP3_prd(X1,X2)
| sP2_prd(X0,X1,X2) ),
inference(resolution,[status(thm)],[f143,f185]) ).
fof(f638,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f31]) ).
fof(f639,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f638]) ).
fof(f680,definition,
! [X4] :
( sQ60_spl
<=> ~ aElement0(X4) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f681,plain,
! [X0] :
( ~ sQ60_spl
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f718,plain,
( ~ sQ33_spl
| ~ sQ60_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f383,f681]) ).
fof(f812,definition,
! [X2] :
( sQ65_spl
<=> ~ aElementOf0(X2,sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f813,plain,
! [X0] :
( ~ sQ65_spl
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f812]) ).
fof(f826,plain,
( ~ sQ33_spl
| ~ sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f829,plain,
( ~ sQ65_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f153,f813]) ).
fof(f833,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f829]) ).
fof(f870,plain,
! [X0,X1] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ sP2_prd(X0,X1,sK21_skl) ),
inference(resolution,[status(thm)],[f174,f153]) ).
fof(f1074,definition,
! [X0,X1] :
( sQ87_spl
<=> ~ aElementOf0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1075,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ aElementOf0(X0,X1) ),
inference(component_clause,[status(thm)],[f1074]) ).
fof(f1312,plain,
( ~ sQ87_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f153,f1075]) ).
fof(f1331,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1312]) ).
fof(f1601,plain,
! [X0] :
( ~ aElement0(X0)
| ~ sP2_prd(X0,sK21_skl,sK21_skl) ),
inference(resolution,[status(thm)],[f870,f153]) ).
fof(f1602,plain,
! [X0,X1,X2] :
( ~ sP3_prd(X1,X2)
| ~ aElement0(X0)
| ~ sP2_prd(X0,X1,sK21_skl) ),
inference(resolution,[status(thm)],[f870,f184]) ).
fof(f1628,plain,
! [X0,X1,X2] :
( ~ sP3_prd(X1,sK21_skl)
| ~ sP3_prd(X1,X2)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f1602,f431]) ).
fof(f1635,definition,
! [X1,X2] :
( sQ117_spl
<=> ( ~ sP3_prd(X1,sK21_skl)
| ~ sP3_prd(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1636,plain,
! [X0,X1] :
( ~ sQ117_spl
| ~ sP3_prd(X0,sK21_skl)
| ~ sP3_prd(X0,X1) ),
inference(component_clause,[status(thm)],[f1635]) ).
fof(f1638,plain,
( sQ117_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1628,f680,f1635]) ).
fof(f1639,plain,
! [X0] :
( ~ sQ0_spl
| ~ sQ117_spl
| ~ sP3_prd(sK22_skl,X0) ),
inference(resolution,[status(thm)],[f1636,f188]) ).
fof(f1640,plain,
( ~ sQ0_spl
| ~ sQ117_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f188,f1639]) ).
fof(f1641,plain,
( ~ sQ0_spl
| ~ sQ117_spl ),
inference(contradiction_clause,[status(thm)],[f1640]) ).
fof(f1662,plain,
! [X0] :
( sQ2_spl
| sP2_prd(sK23_skl,X0,sK21_skl) ),
inference(resolution,[status(thm)],[f196,f147]) ).
fof(f1669,plain,
( sQ2_spl
| ~ aElement0(sK23_skl) ),
inference(resolution,[status(thm)],[f1662,f1601]) ).
fof(f1671,plain,
( sQ2_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1669,f191]) ).
fof(f1672,plain,
( sQ2_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1671]) ).
fof(f1673,plain,
$false,
inference(sat_refutation,[status(thm)],[f193,f197,f234,f259,f342,f385,f402,f639,f826,f833,f1331,f1638,f1641,f1672]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG092+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n018.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 04:20:59 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.28/0.72 % Refutation found
% 0.28/0.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.28/0.75 % Elapsed time: 0.302018 seconds
% 0.28/0.75 % CPU time: 2.053011 seconds
% 0.28/0.75 % Total memory used: 109.030 MB
% 0.28/0.75 % Net memory used: 107.143 MB
%------------------------------------------------------------------------------