%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT385+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 : n020.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:03:04 PM UTC 2026
% Result : Theorem 0.15s 0.41s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 13
% Syntax : Number of formulae : 67 ( 8 unt; 9 def)
% Number of atoms : 455 ( 15 equ)
% Maximal formula atoms : 37 ( 6 avg)
% Number of connectives : 549 ( 161 ~; 151 |; 204 &)
% ( 10 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 7 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-3 aty)
% Number of variables : 132 ( 103 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szRzazndt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( ( aElementOf0(W1,szDzozmdt0(xf))
& aElementOf0(W0,szDzozmdt0(xf)) )
=> ( sdtlseqdt0(W0,W1)
=> sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)) ) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ( aSubsetOf0(W0,xU)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xU) )
& aSet0(W0) ) )
=> ? [W1] :
( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( ( aUpperBoundOfIn0(W3,W0,xU)
| ( ! [W4] :
( aElementOf0(W4,W0)
=> sdtlseqdt0(W4,W3) )
& aElementOf0(W3,xU) ) )
=> sdtlseqdt0(W2,W3) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( aElementOf0(W3,W0)
=> sdtlseqdt0(W3,W2) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( ( aLowerBoundOfIn0(W2,W0,xU)
| ( ! [W3] :
( aElementOf0(W3,W0)
=> sdtlseqdt0(W2,W3) )
& aElementOf0(W2,xU) ) )
=> sdtlseqdt0(W2,W1) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) ) )
& aSet0(xU) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( ( ( ( aUpperBoundOfIn0(W0,xT,xU)
| ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) ) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
=> aElementOf0(W0,xP) )
& ( aElementOf0(W0,xP)
=> ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) ) ) )
& aSet0(xP) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,conjecture,
? [W0] :
( aInfimumOfIn0(W0,xP,xU)
| ( ! [W1] :
( ( aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( aElementOf0(W2,xP)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU) )
=> sdtlseqdt0(W1,W0) )
& ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
& aElementOf0(W0,xU) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
~ ? [W0] :
( aInfimumOfIn0(W0,xP,xU)
| ( ! [W1] :
( ( aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( aElementOf0(W2,xP)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU) )
=> sdtlseqdt0(W1,W0) )
& ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
& aElementOf0(W0,xU) ) ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f43,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f44,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f45,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f46,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f45]) ).
fof(f49,plain,
! [X0,X1] :
( aElementOf0(sK1_skl(X1,X0),X1)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f50,plain,
! [X0,X1] :
( ~ aElementOf0(sK1_skl(X1,X0),X0)
| ~ aSet0(X1)
| aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f111,plain,
! [W0] :
( aSet0(szRzazndt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f112,plain,
! [X0] :
( aSet0(szRzazndt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f134,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ? [W1] :
( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W2,W3)
| ( ~ aUpperBoundOfIn0(W3,W0,xU)
& ( ? [W4] :
( ~ sdtlseqdt0(W4,W3)
& aElementOf0(W4,W0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W3,W2)
| ~ aElementOf0(W3,W0) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W2,W1)
| ( ~ aLowerBoundOfIn0(W2,W0,xU)
& ( ? [W3] :
( ~ sdtlseqdt0(W2,W3)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W2,xU) ) ) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) )
| ( ~ aSubsetOf0(W0,xU)
& ( ? [W1] :
( ~ aElementOf0(W1,xU)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) )
& aSet0(xU) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f135,definition,
! [W0] :
( sP0_prd(W0)
<=> ( ~ aSubsetOf0(W0,xU)
& ( ? [W1] :
( ~ aElementOf0(W1,xU)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f136,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ? [W1] :
( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W2,W3)
| ( ~ aUpperBoundOfIn0(W3,W0,xU)
& ( ? [W4] :
( ~ sdtlseqdt0(W4,W3)
& aElementOf0(W4,W0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W3,W2)
| ~ aElementOf0(W3,W0) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W2,W1)
| ( ~ aLowerBoundOfIn0(W2,W0,xU)
& ( ? [W3] :
( ~ sdtlseqdt0(W2,W3)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W2,xU) ) ) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) )
| sP0_prd(W0) )
& aSet0(xU) ),
inference(formula_renaming,[status(thm)],[f134,f135]) ).
fof(f137,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W2,W3)
| ( ~ aUpperBoundOfIn0(W3,W0,xU)
& ( ? [W4] :
( ~ sdtlseqdt0(W4,W3)
& aElementOf0(W4,W0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( sdtlseqdt0(W3,W2)
| ~ aElementOf0(W3,W0) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& ? [W1] :
( aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W2,W1)
| ( ~ aLowerBoundOfIn0(W2,W0,xU)
& ( ? [W3] :
( ~ sdtlseqdt0(W2,W3)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W2,xU) ) ) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) ) )
| sP0_prd(W0) )
& aSet0(xU) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f138,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ( aSupremumOfIn0(sK13_skl(W0),W0,xU)
& ! [W3] :
( sdtlseqdt0(sK13_skl(W0),W3)
| ( ~ aUpperBoundOfIn0(W3,W0,xU)
& ( ( ~ sdtlseqdt0(sK14_skl(W3,W0),W3)
& aElementOf0(sK14_skl(W3,W0),W0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(sK13_skl(W0),W0,xU)
& ! [W3] :
( sdtlseqdt0(W3,sK13_skl(W0))
| ~ aElementOf0(W3,W0) )
& aElementOf0(sK13_skl(W0),xU)
& aElementOf0(sK13_skl(W0),xU)
& aInfimumOfIn0(sK11_skl(W0),W0,xU)
& ! [W2] :
( sdtlseqdt0(W2,sK11_skl(W0))
| ( ~ aLowerBoundOfIn0(W2,W0,xU)
& ( ( ~ sdtlseqdt0(W2,sK12_skl(W2,W0))
& aElementOf0(sK12_skl(W2,W0),W0) )
| ~ aElementOf0(W2,xU) ) ) )
& aLowerBoundOfIn0(sK11_skl(W0),W0,xU)
& ! [W2] :
( sdtlseqdt0(sK11_skl(W0),W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(sK11_skl(W0),xU)
& aElementOf0(sK11_skl(W0),xU) )
| sP0_prd(W0) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(W1,sK11_skl(W0)),skolemize(W3,sK12_skl(W2,W0)),skolemize(W2,sK13_skl(W0)),skolemize(W4,sK14_skl(W3,W0))],[f137]) ).
fof(f147,plain,
! [X0] :
( aInfimumOfIn0(sK11_skl(X0),X0,xU)
| sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f157,plain,
aFunction0(xf),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f161,plain,
szRzazndt0(xf) = xU,
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f176,plain,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( ( aElementOf0(W0,xP)
| ( ~ aUpperBoundOfIn0(W0,xT,xU)
& ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aElementOf0(W1,xT) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
| ~ aElementOf0(W0,xU) )
& ( ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
| ~ aElementOf0(W0,xP) ) )
& aSet0(xP) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f177,plain,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( aElementOf0(W0,xP)
| ( ~ aUpperBoundOfIn0(W0,xT,xU)
& ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aElementOf0(W1,xT) ) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
| ~ aElementOf0(W0,xU) )
& ! [W0] :
( ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
| ~ aElementOf0(W0,xP) )
& aSet0(xP) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f178,plain,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( aElementOf0(W0,xP)
| ( ~ aUpperBoundOfIn0(W0,xT,xU)
& ~ sdtlseqdt0(sK15_skl(W0),W0)
& aElementOf0(sK15_skl(W0),xT) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
| ~ aElementOf0(W0,xU) )
& ! [W0] :
( ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
| ~ aElementOf0(W0,xP) )
& aSet0(xP) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(W1,sK15_skl(W0))],[f177]) ).
fof(f179,plain,
aSet0(xP),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [X0] :
( aElementOf0(X0,xU)
| ~ aElementOf0(X0,xP) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f188,plain,
! [W0] :
( ~ aInfimumOfIn0(W0,xP,xU)
& ( ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,xP) )
& aElementOf0(W1,xU) )
| ( ~ aLowerBoundOfIn0(W0,xP,xU)
& ( ? [W1] :
( ~ sdtlseqdt0(W0,W1)
& aElementOf0(W1,xP) )
| ~ aElementOf0(W0,xU) ) )
| ~ aElementOf0(W0,xU) ) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f189,definition,
! [W0] :
( sP1_prd(W0)
<=> ( ~ aLowerBoundOfIn0(W0,xP,xU)
& ( ? [W1] :
( ~ sdtlseqdt0(W0,W1)
& aElementOf0(W1,xP) )
| ~ aElementOf0(W0,xU) ) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f190,plain,
! [W0] :
( ~ aInfimumOfIn0(W0,xP,xU)
& ( ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,xP) )
& aElementOf0(W1,xU) )
| sP1_prd(W0)
| ~ aElementOf0(W0,xU) ) ),
inference(formula_renaming,[status(thm)],[f188,f189]) ).
fof(f191,plain,
( ! [W0] : ~ aInfimumOfIn0(W0,xP,xU)
& ! [W0] :
( ? [W1] :
( ~ sdtlseqdt0(W1,W0)
& aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,xP) )
& aElementOf0(W1,xU) )
| sP1_prd(W0)
| ~ aElementOf0(W0,xU) ) ),
inference(miniscoping,[status(thm)],[f190]) ).
fof(f192,plain,
( ! [W0] : ~ aInfimumOfIn0(W0,xP,xU)
& ! [W0] :
( ( ~ sdtlseqdt0(sK16_skl(W0),W0)
& aLowerBoundOfIn0(sK16_skl(W0),xP,xU)
& ! [W2] :
( sdtlseqdt0(sK16_skl(W0),W2)
| ~ aElementOf0(W2,xP) )
& aElementOf0(sK16_skl(W0),xU) )
| sP1_prd(W0)
| ~ aElementOf0(W0,xU) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(W1,sK16_skl(W0))],[f191]) ).
fof(f197,plain,
! [X0] : ~ aInfimumOfIn0(X0,xP,xU),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f198,plain,
! [W0] :
( ( aSubsetOf0(W0,xU)
| ( ! [W1] :
( aElementOf0(W1,xU)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| sP0_prd(W0) )
& ( ( ~ aSubsetOf0(W0,xU)
& ( ? [W1] :
( ~ aElementOf0(W1,xU)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) )
| ~ sP0_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f135]) ).
fof(f199,plain,
( ! [W0] :
( aSubsetOf0(W0,xU)
| ( ! [W1] :
( aElementOf0(W1,xU)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| sP0_prd(W0) )
& ! [W0] :
( ( ~ aSubsetOf0(W0,xU)
& ( ? [W1] :
( ~ aElementOf0(W1,xU)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) )
| ~ sP0_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f200,plain,
( ! [W0] :
( aSubsetOf0(W0,xU)
| ( ! [W1] :
( aElementOf0(W1,xU)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| sP0_prd(W0) )
& ! [W0] :
( ( ~ aSubsetOf0(W0,xU)
& ( ( ~ aElementOf0(sK17_skl(W0),xU)
& aElementOf0(sK17_skl(W0),W0) )
| ~ aSet0(W0) ) )
| ~ sP0_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(W1,sK17_skl(W0))],[f199]) ).
fof(f203,plain,
! [X0] :
( ~ aSubsetOf0(X0,xU)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f242,plain,
( aSet0(xU)
| ~ aFunction0(xf) ),
inference(paramodulation,[status(thm)],[f161,f112]) ).
fof(f243,definition,
( sQ5_spl
<=> aFunction0(xf) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f245,plain,
( sQ5_spl
| ~ aFunction0(xf) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,definition,
( sQ6_spl
<=> aSet0(xU) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f242,f243,f246]) ).
fof(f250,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f157]) ).
fof(f251,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f250]) ).
fof(f273,definition,
( sQ8_spl
<=> aSet0(xP) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f275,plain,
( sQ8_spl
| ~ aSet0(xP) ),
inference(component_clause,[status(thm)],[f273]) ).
fof(f276,definition,
( sQ9_spl
<=> aElementOf0(sK1_skl(xP,xU),xP) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f277,plain,
( ~ sQ9_spl
| aElementOf0(sK1_skl(xP,xU),xP) ),
inference(component_clause,[status(thm)],[f276]) ).
fof(f288,plain,
( ~ sQ9_spl
| aElementOf0(sK1_skl(xP,xU),xU) ),
inference(resolution,[status(thm)],[f277,f180]) ).
fof(f296,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f275,f179]) ).
fof(f297,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f296]) ).
fof(f318,plain,
( ~ sQ9_spl
| ~ aSet0(xP)
| aSubsetOf0(xP,xU)
| ~ aSet0(xU) ),
inference(resolution,[status(thm)],[f288,f50]) ).
fof(f325,definition,
( sQ15_spl
<=> aSubsetOf0(xP,xU) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( ~ sQ15_spl
| aSubsetOf0(xP,xU) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f328,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ15_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f318,f246,f325,f273,f276]) ).
fof(f387,definition,
( sQ28_spl
<=> sP0_prd(xP) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f388,plain,
( ~ sQ28_spl
| sP0_prd(xP) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f389,plain,
( sQ28_spl
| ~ sP0_prd(xP) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f405,plain,
( ~ sQ28_spl
| ~ aSubsetOf0(xP,xU) ),
inference(resolution,[status(thm)],[f388,f203]) ).
fof(f406,plain,
( ~ sQ28_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f405,f326]) ).
fof(f407,plain,
( ~ sQ28_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f406]) ).
fof(f414,plain,
( sQ28_spl
| aInfimumOfIn0(sK11_skl(xP),xP,xU) ),
inference(resolution,[status(thm)],[f389,f147]) ).
fof(f417,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f197]) ).
fof(f418,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f417]) ).
fof(f435,plain,
( ~ sQ28_spl
| aElementOf0(sK1_skl(xP,xU),xP)
| ~ aSet0(xP)
| ~ aSet0(xU) ),
inference(resolution,[status(thm)],[f405,f49]) ).
fof(f436,plain,
( ~ sQ28_spl
| sQ9_spl
| ~ sQ8_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f435,f246,f273,f276,f387]) ).
fof(f437,plain,
$false,
inference(sat_refutation,[status(thm)],[f249,f251,f297,f328,f407,f418,f436]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT385+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 23:58:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.39 % Drodi V4.1.1
% 0.15/0.41 % Refutation found
% 0.15/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.44 % Elapsed time: 0.055672 seconds
% 0.15/0.44 % CPU time: 0.174421 seconds
% 0.15/0.44 % Total memory used: 71.282 MB
% 0.15/0.44 % Net memory used: 71.114 MB
%------------------------------------------------------------------------------