%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT388+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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 01:03:57 PM UTC 2026
% Result : Theorem 0.18s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT388+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n006.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 20 23:57:42 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 0.18/0.51 % Refutation found
% 0.18/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.51 fof(f30,hypothesis,(
% 0.18/0.51 ( aElementOf0(xp,szDzozmdt0(xf))& sdtlpdtrp0(xf,xp) = xp& aFixedPointOf0(xp,xf)& (! [W0] :( aElementOf0(W0,xT)=> sdtlseqdt0(W0,xp) ))& aUpperBoundOfIn0(xp,xT,xS)& (! [W0] :( ( ( aElementOf0(W0,xS)& (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ) ))| aUpperBoundOfIn0(W0,xT,xS) )=> sdtlseqdt0(xp,W0) ))& aSupremumOfIn0(xp,xT,xS) ) ),
% 0.18/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f31,conjecture,(
% 0.18/0.51 (? [W0] :( ( aElementOf0(W0,xS)& ( ( aElementOf0(W0,xS)& (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ) ))| aUpperBoundOfIn0(W0,xT,xS) )& (! [W1] :( ( aElementOf0(W1,xS)& (! [W2] :( aElementOf0(W2,xT)=> sdtlseqdt0(W2,W1) ))& aUpperBoundOfIn0(W1,xT,xS) )=> sdtlseqdt0(W0,W1) ) ))| aSupremumOfIn0(W0,xT,xS) ) )),
% 0.18/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f32,negated_conjecture,(
% 0.18/0.51 ~((? [W0] :( ( aElementOf0(W0,xS)& ( ( aElementOf0(W0,xS)& (! [W1] :( aElementOf0(W1,xT)=> sdtlseqdt0(W1,W0) ) ))| aUpperBoundOfIn0(W0,xT,xS) )& (! [W1] :( ( aElementOf0(W1,xS)& (! [W2] :( aElementOf0(W2,xT)=> sdtlseqdt0(W2,W1) ))& aUpperBoundOfIn0(W1,xT,xS) )=> sdtlseqdt0(W0,W1) ) ))| aSupremumOfIn0(W0,xT,xS) ) ))),
% 0.18/0.51 inference(negated_conjecture,[status(cth)],[f31])).
% 0.18/0.51 fof(f206,plain,(
% 0.18/0.51 (((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(![W0]: (~aElementOf0(W0,xT)|sdtlseqdt0(W0,xp))))&aUpperBoundOfIn0(xp,xT,xS))&(![W0]: (((~aElementOf0(W0,xS)|(?[W1]: (aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0))))&~aUpperBoundOfIn0(W0,xT,xS))|sdtlseqdt0(xp,W0))))&aSupremumOfIn0(xp,xT,xS)),
% 0.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.18/0.51 fof(f207,plain,(
% 0.18/0.51 (((((aElementOf0(xp,szDzozmdt0(xf))&sdtlpdtrp0(xf,xp)=xp)&aFixedPointOf0(xp,xf))&(![W0]: (~aElementOf0(W0,xT)|sdtlseqdt0(W0,xp))))&aUpperBoundOfIn0(xp,xT,xS))&(![W0]: (((~aElementOf0(W0,xS)|(aElementOf0(sK17_skl(W0),xT)&~sdtlseqdt0(sK17_skl(W0),W0)))&~aUpperBoundOfIn0(W0,xT,xS))|sdtlseqdt0(xp,W0))))&aSupremumOfIn0(xp,xT,xS)),
% 0.18/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(W1,sK17_skl(W0))],[f206])).
% 0.18/0.51 fof(f216,plain,(
% 0.18/0.51 aSupremumOfIn0(xp,xT,xS)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f207])).
% 0.18/0.51 fof(f217,plain,(
% 0.18/0.51 (![W0]: (((~aElementOf0(W0,xS)|((~aElementOf0(W0,xS)|(?[W1]: (aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0))))&~aUpperBoundOfIn0(W0,xT,xS)))|(?[W1]: (((aElementOf0(W1,xS)&(![W2]: (~aElementOf0(W2,xT)|sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))&~sdtlseqdt0(W0,W1))))&~aSupremumOfIn0(W0,xT,xS)))),
% 0.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.18/0.51 fof(f218,definition,(
% 0.18/0.51 ![W0]: (sP1_prd(W0)<=>((~aElementOf0(W0,xS)|(?[W1]: (aElementOf0(W1,xT)&~sdtlseqdt0(W1,W0))))&~aUpperBoundOfIn0(W0,xT,xS)))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.18/0.51 fof(f219,plain,(
% 0.18/0.51 ![W0]: (((~aElementOf0(W0,xS)|sP1_prd(W0))|(?[W1]: (((aElementOf0(W1,xS)&(![W2]: (~aElementOf0(W2,xT)|sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))&~sdtlseqdt0(W0,W1))))&~aSupremumOfIn0(W0,xT,xS))),
% 0.18/0.51 inference(formula_renaming,[status(thm)],[f217,f218])).
% 0.18/0.51 fof(f220,plain,(
% 0.18/0.51 (![W0]: ((~aElementOf0(W0,xS)|sP1_prd(W0))|(?[W1]: (((aElementOf0(W1,xS)&(![W2]: (~aElementOf0(W2,xT)|sdtlseqdt0(W2,W1))))&aUpperBoundOfIn0(W1,xT,xS))&~sdtlseqdt0(W0,W1)))))&(![W0]: ~aSupremumOfIn0(W0,xT,xS))),
% 0.18/0.51 inference(miniscoping,[status(thm)],[f219])).
% 0.18/0.51 fof(f221,plain,(
% 0.18/0.51 (![W0]: ((~aElementOf0(W0,xS)|sP1_prd(W0))|(((aElementOf0(sK18_skl(W0),xS)&(![W2]: (~aElementOf0(W2,xT)|sdtlseqdt0(W2,sK18_skl(W0)))))&aUpperBoundOfIn0(sK18_skl(W0),xT,xS))&~sdtlseqdt0(W0,sK18_skl(W0)))))&(![W0]: ~aSupremumOfIn0(W0,xT,xS))),
% 0.18/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(W1,sK18_skl(W0))],[f220])).
% 0.18/0.51 fof(f226,plain,(
% 0.18/0.51 ![X0]: (~aSupremumOfIn0(X0,xT,xS))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f221])).
% 0.18/0.51 fof(f245,plain,(
% 0.18/0.51 $false),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f216,f226])).
% 0.18/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.58 % Elapsed time: 0.107650 seconds
% 0.22/0.58 % CPU time: 0.115702 seconds
% 0.22/0.58 % Total memory used: 13.419 MB
% 0.22/0.58 % Net memory used: 13.406 MB
%------------------------------------------------------------------------------