%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG111+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:00 PM UTC 2026
% Result : Theorem 0.20s 15.60s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 13
% Syntax : Number of formulae : 74 ( 8 unt; 11 def)
% Number of atoms : 417 ( 116 equ)
% Maximal formula atoms : 33 ( 5 avg)
% Number of connectives : 507 ( 164 ~; 154 |; 166 &)
% ( 11 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 10 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 11 con; 0-2 aty)
% Number of variables : 139 ( 75 !; 64 ?)
% Comments :
%------------------------------------------------------------------------------
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/sandbox/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
! [W0] :
( ( W0 != sz00
& aElementOf0(W0,xI)
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) )
=> ( ! [W1] :
( ( W1 != sz00
& ( aElementOf0(W1,xI)
| ? [W2,W3] :
( sdtpldt0(W2,W3) = W1
& aElementOf0(W3,slsdtgt0(xb))
& aElementOf0(W2,slsdtgt0(xa)) ) ) )
=> ( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
=> ? [W2] :
( ! [W3] :
( ( W3 != sz00
& ( aElementOf0(W3,xI)
| ? [W4,W5] :
( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,slsdtgt0(xb))
& aElementOf0(W4,slsdtgt0(xa)) ) ) )
=> ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2)) )
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) ) ) )
=> ? [W1] :
( ! [W2] :
( ( W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) )
& W1 != sz00
& ( aElementOf0(W1,xI)
| ? [W2,W3] :
( sdtpldt0(W2,W3) = W1
& aElementOf0(W3,slsdtgt0(xb))
& aElementOf0(W2,slsdtgt0(xa)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ ! [W0] :
( ( W0 != sz00
& aElementOf0(W0,xI)
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) )
=> ( ! [W1] :
( ( W1 != sz00
& ( aElementOf0(W1,xI)
| ? [W2,W3] :
( sdtpldt0(W2,W3) = W1
& aElementOf0(W3,slsdtgt0(xb))
& aElementOf0(W2,slsdtgt0(xa)) ) ) )
=> ( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
=> ? [W2] :
( ! [W3] :
( ( W3 != sz00
& ( aElementOf0(W3,xI)
| ? [W4,W5] :
( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,slsdtgt0(xb))
& aElementOf0(W4,slsdtgt0(xa)) ) ) )
=> ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2)) )
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) ) ) )
=> ? [W1] :
( ! [W2] :
( ( W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) )
& W1 != sz00
& ( aElementOf0(W1,xI)
| ? [W2,W3] :
( sdtpldt0(W2,W3) = W1
& aElementOf0(W3,slsdtgt0(xb))
& aElementOf0(W2,slsdtgt0(xa)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f239,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(sK30_skl),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f266,plain,
? [W0] :
( ! [W1] :
( ? [W2] :
( iLess0(sbrdtbr0(W2),sbrdtbr0(W1))
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
| W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) ) )
& ! [W1] :
( ? [W2] :
( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
| W3 = sz00
| ( ~ aElementOf0(W3,xI)
& ! [W4,W5] :
( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,slsdtgt0(xb))
| ~ aElementOf0(W4,slsdtgt0(xa)) ) ) )
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
| ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
| W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) ) )
& W0 != sz00
& aElementOf0(W0,xI)
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f267,definition,
! [W2] :
( sP4_prd(W2)
<=> ( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
| W3 = sz00
| ( ~ aElementOf0(W3,xI)
& ! [W4,W5] :
( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,slsdtgt0(xb))
| ~ aElementOf0(W4,slsdtgt0(xa)) ) ) )
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f268,definition,
! [W1] :
( sP5_prd(W1)
<=> ( W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f269,plain,
? [W0] :
( ! [W1] :
( ? [W2] :
( iLess0(sbrdtbr0(W2),sbrdtbr0(W1))
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
| sP5_prd(W1) )
& ! [W1] :
( ? [W2] : sP4_prd(W2)
| ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
| W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) ) )
& W0 != sz00
& aElementOf0(W0,xI)
& ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) ),
inference(formula_renaming,[status(thm)],[f266,f268,f267]) ).
fof(f270,plain,
( ! [W1] :
( ( iLess0(sbrdtbr0(sK40_skl(W1)),sbrdtbr0(W1))
& sK40_skl(W1) != sz00
& aElementOf0(sK40_skl(W1),xI)
& sdtpldt0(sK41_skl(W1),sK42_skl(W1)) = sK40_skl(W1)
& aElementOf0(sK42_skl(W1),slsdtgt0(xb))
& aElementOf0(sK41_skl(W1),slsdtgt0(xa)) )
| sP5_prd(W1) )
& ! [W1] :
( sP4_prd(sK39_skl(W1))
| ~ iLess0(sbrdtbr0(W1),sbrdtbr0(sK36_skl))
| W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) ) )
& sK36_skl != sz00
& aElementOf0(sK36_skl,xI)
& sdtpldt0(sK37_skl,sK38_skl) = sK36_skl
& aElementOf0(sK38_skl,slsdtgt0(xb))
& aElementOf0(sK37_skl,slsdtgt0(xa)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl,sK38_skl,sK39_skl,sK40_skl,sK41_skl,sK42_skl]),skolemize(W0,sK36_skl),skolemize(W1,sK37_skl),skolemize(W2,sK38_skl),skolemize(W2,sK39_skl(W1)),skolemize(W2,sK40_skl(W1)),skolemize(W3,sK41_skl(W1)),skolemize(W4,sK42_skl(W1))],[f269]) ).
fof(f274,plain,
aElementOf0(sK36_skl,xI),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f275,plain,
sK36_skl != sz00,
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f277,plain,
! [X0] :
( sP4_prd(sK39_skl(X0))
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK36_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f281,plain,
! [X0] :
( aElementOf0(sK40_skl(X0),xI)
| sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f282,plain,
! [X0] :
( sK40_skl(X0) != sz00
| sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f283,plain,
! [X0] :
( iLess0(sbrdtbr0(sK40_skl(X0)),sbrdtbr0(X0))
| sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f312,plain,
! [W2] :
( ( ? [W3] :
( iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
& W3 != sz00
& ( aElementOf0(W3,xI)
| ? [W4,W5] :
( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,slsdtgt0(xb))
& aElementOf0(W4,slsdtgt0(xa)) ) ) )
| W2 = sz00
| ~ aElementOf0(W2,xI)
| ! [W3,W4] :
( sdtpldt0(W3,W4) != W2
| ~ aElementOf0(W4,slsdtgt0(xb))
| ~ aElementOf0(W3,slsdtgt0(xa)) )
| sP4_prd(W2) )
& ( ( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
| W3 = sz00
| ( ~ aElementOf0(W3,xI)
& ! [W4,W5] :
( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,slsdtgt0(xb))
| ~ aElementOf0(W4,slsdtgt0(xa)) ) ) )
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
| ~ sP4_prd(W2) ) ),
inference(NNF_transformation,[status(thm)],[f267]) ).
fof(f313,plain,
( ! [W2] :
( ? [W3] :
( iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
& W3 != sz00
& ( aElementOf0(W3,xI)
| ? [W4,W5] :
( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,slsdtgt0(xb))
& aElementOf0(W4,slsdtgt0(xa)) ) ) )
| W2 = sz00
| ~ aElementOf0(W2,xI)
| ! [W3,W4] :
( sdtpldt0(W3,W4) != W2
| ~ aElementOf0(W4,slsdtgt0(xb))
| ~ aElementOf0(W3,slsdtgt0(xa)) )
| sP4_prd(W2) )
& ! [W2] :
( ( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
| W3 = sz00
| ( ~ aElementOf0(W3,xI)
& ! [W4,W5] :
( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,slsdtgt0(xb))
| ~ aElementOf0(W4,slsdtgt0(xa)) ) ) )
& W2 != sz00
& aElementOf0(W2,xI)
& ? [W3,W4] :
( sdtpldt0(W3,W4) = W2
& aElementOf0(W4,slsdtgt0(xb))
& aElementOf0(W3,slsdtgt0(xa)) ) )
| ~ sP4_prd(W2) ) ),
inference(miniscoping,[status(thm)],[f312]) ).
fof(f314,plain,
( ! [W2] :
( ( iLess0(sbrdtbr0(sK46_skl(W2)),sbrdtbr0(W2))
& sK46_skl(W2) != sz00
& ( aElementOf0(sK46_skl(W2),xI)
| ( sdtpldt0(sK47_skl(W2),sK48_skl(W2)) = sK46_skl(W2)
& aElementOf0(sK48_skl(W2),slsdtgt0(xb))
& aElementOf0(sK47_skl(W2),slsdtgt0(xa)) ) ) )
| W2 = sz00
| ~ aElementOf0(W2,xI)
| ! [W3,W4] :
( sdtpldt0(W3,W4) != W2
| ~ aElementOf0(W4,slsdtgt0(xb))
| ~ aElementOf0(W3,slsdtgt0(xa)) )
| sP4_prd(W2) )
& ! [W2] :
( ( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
| W3 = sz00
| ( ~ aElementOf0(W3,xI)
& ! [W4,W5] :
( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,slsdtgt0(xb))
| ~ aElementOf0(W4,slsdtgt0(xa)) ) ) )
& W2 != sz00
& aElementOf0(W2,xI)
& sdtpldt0(sK44_skl(W2),sK45_skl(W2)) = W2
& aElementOf0(sK45_skl(W2),slsdtgt0(xb))
& aElementOf0(sK44_skl(W2),slsdtgt0(xa)) )
| ~ sP4_prd(W2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl,sK45_skl,sK46_skl,sK47_skl,sK48_skl]),skolemize(W3,sK44_skl(W2)),skolemize(W4,sK45_skl(W2)),skolemize(W3,sK46_skl(W2)),skolemize(W4,sK47_skl(W2)),skolemize(W5,sK48_skl(W2))],[f313]) ).
fof(f318,plain,
! [X0] :
( aElementOf0(X0,xI)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f319,plain,
! [X0] :
( X0 != sz00
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f321,plain,
! [X0,X1] :
( ~ iLess0(sbrdtbr0(X1),sbrdtbr0(X0))
| X1 = sz00
| ~ aElementOf0(X1,xI)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f327,plain,
! [W1] :
( ( ( W1 != sz00
& ( aElementOf0(W1,xI)
| ? [W2,W3] :
( sdtpldt0(W2,W3) = W1
& aElementOf0(W3,slsdtgt0(xb))
& aElementOf0(W2,slsdtgt0(xa)) ) ) )
| sP5_prd(W1) )
& ( W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) )
| ~ sP5_prd(W1) ) ),
inference(NNF_transformation,[status(thm)],[f268]) ).
fof(f328,plain,
( ! [W1] :
( ( W1 != sz00
& ( aElementOf0(W1,xI)
| ? [W2,W3] :
( sdtpldt0(W2,W3) = W1
& aElementOf0(W3,slsdtgt0(xb))
& aElementOf0(W2,slsdtgt0(xa)) ) ) )
| sP5_prd(W1) )
& ! [W1] :
( W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) )
| ~ sP5_prd(W1) ) ),
inference(miniscoping,[status(thm)],[f327]) ).
fof(f329,plain,
( ! [W1] :
( ( W1 != sz00
& ( aElementOf0(W1,xI)
| ( sdtpldt0(sK49_skl(W1),sK50_skl(W1)) = W1
& aElementOf0(sK50_skl(W1),slsdtgt0(xb))
& aElementOf0(sK49_skl(W1),slsdtgt0(xa)) ) ) )
| sP5_prd(W1) )
& ! [W1] :
( W1 = sz00
| ( ~ aElementOf0(W1,xI)
& ! [W2,W3] :
( sdtpldt0(W2,W3) != W1
| ~ aElementOf0(W3,slsdtgt0(xb))
| ~ aElementOf0(W2,slsdtgt0(xa)) ) )
| ~ sP5_prd(W1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl]),skolemize(W2,sK49_skl(W1)),skolemize(W3,sK50_skl(W1))],[f328]) ).
fof(f331,plain,
! [X0] :
( X0 = sz00
| ~ aElementOf0(X0,xI)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f371,plain,
~ sP4_prd(sz00),
inference(destructive_equality_resolution,[status(thm)],[f319]) ).
fof(f811,definition,
( sQ26_spl
<=> aElement0(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( sQ26_spl
| ~ aElement0(sK30_skl) ),
inference(component_clause,[status(thm)],[f811]) ).
fof(f1006,plain,
( sP4_prd(sK39_skl(sK40_skl(sK36_skl)))
| sK40_skl(sK36_skl) = sz00
| ~ aElementOf0(sK40_skl(sK36_skl),xI)
| sP5_prd(sK36_skl) ),
inference(resolution,[status(thm)],[f283,f277]) ).
fof(f1007,definition,
( sQ51_spl
<=> sP5_prd(sK36_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1008,plain,
( ~ sQ51_spl
| sP5_prd(sK36_skl) ),
inference(component_clause,[status(thm)],[f1007]) ).
fof(f1009,plain,
( sQ51_spl
| ~ sP5_prd(sK36_skl) ),
inference(component_clause,[status(thm)],[f1007]) ).
fof(f1010,definition,
( sQ52_spl
<=> aElementOf0(sK40_skl(sK36_skl),xI) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( sQ52_spl
| ~ aElementOf0(sK40_skl(sK36_skl),xI) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,definition,
( sQ53_spl
<=> sK40_skl(sK36_skl) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1014,plain,
( ~ sQ53_spl
| sK40_skl(sK36_skl) = sz00 ),
inference(component_clause,[status(thm)],[f1013]) ).
fof(f1016,definition,
( sQ54_spl
<=> sP4_prd(sK39_skl(sK40_skl(sK36_skl))) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1017,plain,
( ~ sQ54_spl
| sP4_prd(sK39_skl(sK40_skl(sK36_skl))) ),
inference(component_clause,[status(thm)],[f1016]) ).
fof(f1019,plain,
( sQ54_spl
| sQ53_spl
| ~ sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1006,f1007,f1010,f1013,f1016]) ).
fof(f1020,plain,
( ~ sQ51_spl
| sK36_skl = sz00
| ~ aElementOf0(sK36_skl,xI) ),
inference(resolution,[status(thm)],[f1008,f331]) ).
fof(f1021,definition,
( sQ55_spl
<=> aElementOf0(sK36_skl,xI) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1023,plain,
( sQ55_spl
| ~ aElementOf0(sK36_skl,xI) ),
inference(component_clause,[status(thm)],[f1021]) ).
fof(f1024,definition,
( sQ56_spl
<=> sK36_skl = sz00 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1025,plain,
( ~ sQ56_spl
| sK36_skl = sz00 ),
inference(component_clause,[status(thm)],[f1024]) ).
fof(f1027,plain,
( ~ sQ51_spl
| sQ56_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f1020,f1021,f1024,f1007]) ).
fof(f1028,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1025,f275]) ).
fof(f1029,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f1028]) ).
fof(f1030,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1023,f274]) ).
fof(f1031,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f1030]) ).
fof(f1033,plain,
( sQ51_spl
| sK40_skl(sK36_skl) != sz00 ),
inference(resolution,[status(thm)],[f1009,f282]) ).
fof(f1064,plain,
( ~ sQ54_spl
| aElementOf0(sK39_skl(sK40_skl(sK36_skl)),xI) ),
inference(resolution,[status(thm)],[f1017,f318]) ).
fof(f1065,plain,
( sQ52_spl
| sP5_prd(sK36_skl) ),
inference(resolution,[status(thm)],[f1012,f281]) ).
fof(f1066,plain,
( sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1065,f1007,f1010]) ).
fof(f1067,plain,
( ~ sQ53_spl
| sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1014,f1033]) ).
fof(f1068,plain,
( ~ sQ53_spl
| sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f1067]) ).
fof(f1071,plain,
! [X0] :
( sP5_prd(X0)
| sK40_skl(X0) = sz00
| ~ aElementOf0(sK40_skl(X0),xI)
| ~ sP4_prd(X0) ),
inference(resolution,[status(thm)],[f321,f283]) ).
fof(f1072,plain,
! [X0] :
( sP5_prd(X0)
| sK40_skl(X0) = sz00
| ~ sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1071,f281]) ).
fof(f1210,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f813,f249]) ).
fof(f1211,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1210]) ).
fof(f1230,plain,
! [X0] :
( sP5_prd(X0)
| ~ sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1072,f282]) ).
fof(f1231,plain,
( ~ sQ54_spl
| sP5_prd(sK39_skl(sK40_skl(sK36_skl))) ),
inference(resolution,[status(thm)],[f1230,f1017]) ).
fof(f1232,plain,
( ~ sQ54_spl
| sK39_skl(sK40_skl(sK36_skl)) = sz00
| ~ aElementOf0(sK39_skl(sK40_skl(sK36_skl)),xI) ),
inference(resolution,[status(thm)],[f1231,f331]) ).
fof(f1233,definition,
( sQ66_spl
<=> aElementOf0(sK39_skl(sK40_skl(sK36_skl)),xI) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1235,plain,
( sQ66_spl
| ~ aElementOf0(sK39_skl(sK40_skl(sK36_skl)),xI) ),
inference(component_clause,[status(thm)],[f1233]) ).
fof(f1236,definition,
( sQ67_spl
<=> sK39_skl(sK40_skl(sK36_skl)) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1237,plain,
( ~ sQ67_spl
| sK39_skl(sK40_skl(sK36_skl)) = sz00 ),
inference(component_clause,[status(thm)],[f1236]) ).
fof(f1239,plain,
( ~ sQ54_spl
| sQ67_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f1232,f1233,f1236,f1016]) ).
fof(f1240,plain,
( sQ66_spl
| ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1235,f1064]) ).
fof(f1241,plain,
( sQ66_spl
| ~ sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f1240]) ).
fof(f1244,plain,
( ~ sQ54_spl
| ~ sQ67_spl
| sP4_prd(sz00) ),
inference(backward_demodulation,[status(thm)],[f1237,f1017]) ).
fof(f1245,plain,
( ~ sQ54_spl
| ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1244,f371]) ).
fof(f1246,plain,
( ~ sQ54_spl
| ~ sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f1245]) ).
fof(f1247,plain,
$false,
inference(sat_refutation,[status(thm)],[f1019,f1027,f1029,f1031,f1066,f1068,f1211,f1239,f1241,f1246]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG111+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/15.43 % Computer : n006.cluster.edu
% 0.15/15.43 % Model : x86_64 x86_64
% 0.15/15.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/15.43 % Memory : 8046.5625MB
% 0.15/15.43 % OS : Linux 6.8.0-71-generic
% 0.15/15.43 % CPULimit : 300
% 0.15/15.43 % WCLimit : 300
% 0.15/15.43 % DateTime : Mon Sep 21 04:20:43 UTC 2026
% 0.15/15.44 % CPUTime :
% 0.15/15.46 % Drodi V4.1.1
% 0.20/15.60 % Refutation found
% 0.20/15.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/15.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.20/15.63 % Elapsed time: 0.169586 seconds
% 0.20/15.63 % CPU time: 1.057027 seconds
% 0.20/15.63 % Total memory used: 121.969 MB
% 0.20/15.63 % Net memory used: 121.172 MB
%------------------------------------------------------------------------------