%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 07:50:30 AM UTC 2026
% Result : Theorem 1.82s 0.62s
% Output : CNFRefutation 1.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 11
% Syntax : Number of formulae : 138 ( 33 unt; 0 def)
% Number of atoms : 575 ( 66 equ)
% Maximal formula atoms : 95 ( 4 avg)
% Number of connectives : 688 ( 251 ~; 278 |; 123 &)
% ( 1 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-3 aty)
% Number of variables : 103 ( 0 sgn 54 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mARefl,axiom,
! [W0] :
( aElement0(W0)
=> sdtlseqdt0(W0,W0) ),
file('theBenchmark.p',mARefl) ).
fof(mASymm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mASymm) ).
fof(mDefCLat,axiom,
! [W0] :
( aCompleteLattice0(W0)
<=> ( ! [W1] :
( aSubsetOf0(W1,W0)
=> ? [W2] :
( ? [W3] : aSupremumOfIn0(W3,W1,W0)
& aInfimumOfIn0(W2,W1,W0) ) )
& aSet0(W0) ) ),
file('theBenchmark.p',mDefCLat) ).
fof(mImgSort,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElementOf0(sdtlpdtrp0(W0,W1),szRzazndt0(W0)) ) ),
file('theBenchmark.p',mImgSort) ).
fof(m__1123,axiom,
( 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('theBenchmark.p',m__1123) ).
fof(m__1144,axiom,
( xS = cS1142(xf)
& ! [W0] :
( ( ( aFixedPointOf0(W0,xf)
| ( sdtlpdtrp0(xf,W0) = W0
& aElementOf0(W0,szDzozmdt0(xf)) ) )
=> aElementOf0(W0,xS) )
& ( aElementOf0(W0,xS)
=> ( aFixedPointOf0(W0,xf)
& sdtlpdtrp0(xf,W0) = W0
& aElementOf0(W0,szDzozmdt0(xf)) ) ) )
& aSet0(xS) ),
file('theBenchmark.p',m__1144) ).
fof(m__1244,axiom,
( 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('theBenchmark.p',m__1244) ).
fof(m__1261,axiom,
( aInfimumOfIn0(xp,xP,xU)
& ! [W0] :
( ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
=> sdtlseqdt0(W0,xp) )
& aLowerBoundOfIn0(xp,xP,xU)
& ! [W0] :
( aElementOf0(W0,xP)
=> sdtlseqdt0(xp,W0) )
& aElementOf0(xp,xU)
& aElementOf0(xp,xU) ),
file('theBenchmark.p',m__1261) ).
fof(m__1299,axiom,
( aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU)
& ! [W0] :
( aElementOf0(W0,xT)
=> sdtlseqdt0(W0,sdtlpdtrp0(xf,xp)) )
& aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU)
& ! [W0] :
( aElementOf0(W0,xP)
=> sdtlseqdt0(sdtlpdtrp0(xf,xp),W0) ) ),
file('theBenchmark.p',m__1299) ).
fof(m__,conjecture,
( ( aSupremumOfIn0(xp,xT,xS)
| ( ! [W0] :
( ( aUpperBoundOfIn0(W0,xT,xS)
& ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) )
& aElementOf0(W0,xS) )
=> sdtlseqdt0(xp,W0) )
& ( aUpperBoundOfIn0(xp,xT,xS)
| ! [W0] :
( aElementOf0(W0,xT)
=> sdtlseqdt0(W0,xp) ) ) ) )
& ( aFixedPointOf0(xp,xf)
| ( sdtlpdtrp0(xf,xp) = xp
& aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( aSupremumOfIn0(xp,xT,xS)
| ( ! [W0] :
( ( aUpperBoundOfIn0(W0,xT,xS)
& ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) )
& aElementOf0(W0,xS) )
=> sdtlseqdt0(xp,W0) )
& ( aUpperBoundOfIn0(xp,xT,xS)
| ! [W0] :
( aElementOf0(W0,xT)
=> sdtlseqdt0(W0,xp) ) ) ) )
& ( aFixedPointOf0(xp,xf)
| ( sdtlpdtrp0(xf,xp) = xp
& aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_36,plain,
aCompleteLattice0(xU),
inference(clausify,[status(thm)],[m__1123]) ).
cnf(c_38,plain,
( aSet0(A)
| ~ aCompleteLattice0(A) ),
inference(clausify,[status(thm)],[mDefCLat]) ).
cnf(c_39,plain,
aFunction0(xf),
inference(clausify,[status(thm)],[m__1123]) ).
cnf(c_48,plain,
( aElementOf0(sdtlpdtrp0(A,B),szRzazndt0(A))
| ~ aElementOf0(B,szDzozmdt0(A))
| ~ aFunction0(A) ),
inference(clausify,[status(thm)],[mImgSort]) ).
cnf(c_54,plain,
aSet0(xU),
inference(resolve,[status(thm)],[c_38,c_36]) ).
cnf(c_61,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_66,plain,
( sdtlseqdt0(A,A)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mARefl]) ).
cnf(c_67,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mASymm]) ).
cnf(c_131,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,A),sdtlpdtrp0(xf,B))
| ~ sdtlseqdt0(A,B)
| ~ aElementOf0(B,szDzozmdt0(xf))
| ~ aElementOf0(A,szDzozmdt0(xf)) ),
inference(clausify,[status(thm)],[m__1123]) ).
cnf(c_132,plain,
szRzazndt0(xf) = szDzozmdt0(xf),
inference(clausify,[status(thm)],[m__1123]) ).
cnf(c_133,plain,
szRzazndt0(xf) = xU,
inference(clausify,[status(thm)],[m__1123]) ).
cnf(c_134,plain,
szDzozmdt0(xf) = xU,
inference(paramod,[status(thm)],[c_132,c_133]) ).
cnf(c_136,plain,
aSet0(xS),
inference(clausify,[status(thm)],[m__1144]) ).
cnf(c_137,plain,
( aElementOf0(A,szDzozmdt0(xf))
| ~ aElementOf0(A,xS) ),
inference(clausify,[status(thm)],[m__1144]) ).
cnf(c_138,plain,
( aElementOf0(A,xU)
| ~ aElementOf0(A,xS) ),
inference(paramod,[status(thm)],[c_134,c_137]) ).
cnf(c_139,plain,
( sdtlpdtrp0(xf,A) = A
| ~ aElementOf0(A,xS) ),
inference(clausify,[status(thm)],[m__1144]) ).
cnf(c_144,plain,
cS1142(xf) = xS,
inference(clausify,[status(thm)],[m__1144]) ).
cnf(c_145,plain,
xS = cS1142(xf),
inference(copy,[status(thm)],[c_144]) ).
fof(nnf_27,plain,
( cS1241(xU,xf,xT) = xP
& ! [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)
& ! [X0] :
( sdtlseqdt0(X0,W0)
| ~ aElementOf0(X0,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
| ~ aElementOf0(W0,xP) ) )
& aSet0(xP) ),
inference(fof_nnf,[status(thm)],[m__1244]) ).
fof(sk_m__1244_sk,plain,
( cS1241(xU,xf,xT) = xP
& ! [W0] :
( ( aElementOf0(W0,xP)
| ( ~ aUpperBoundOfIn0(W0,xT,xU)
& ~ sdtlseqdt0(sK0(W0),W0)
& aElementOf0(sK0(W0),xT) )
| ~ sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
| ~ aElementOf0(W0,xU) )
& ( ( aUpperBoundOfIn0(W0,xT,xU)
& ! [X0] :
( sdtlseqdt0(X0,W0)
| ~ aElementOf0(X0,xT) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
| ~ aElementOf0(W0,xP) ) )
& aSet0(xP) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W1,sK0(W0))],[nnf_27]) ).
fof(sk_m__1244,plain,
( cS1241(xU,xf,xT) = xP
& ! [VAR_0] :
( aElementOf0(VAR_0,xP)
| ~ aUpperBoundOfIn0(VAR_0,xT,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,VAR_0),VAR_0)
| ~ aElementOf0(VAR_0,xU) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xP)
| ~ sdtlseqdt0(sK0(VAR_0),VAR_0)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,VAR_0),VAR_0)
| ~ aElementOf0(VAR_0,xU) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xP)
| aElementOf0(sK0(VAR_0),xT)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,VAR_0),VAR_0)
| ~ aElementOf0(VAR_0,xU) )
& ! [VAR_0] :
( aUpperBoundOfIn0(VAR_0,xT,xU)
| ~ aElementOf0(VAR_0,xP) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,VAR_0)
| ~ aElementOf0(VAR_1,xT)
| ~ aElementOf0(VAR_0,xP) )
& ! [VAR_0] :
( sdtlseqdt0(sdtlpdtrp0(xf,VAR_0),VAR_0)
| ~ aElementOf0(VAR_0,xP) )
& ! [VAR_0] :
( aElementOf0(VAR_0,xU)
| ~ aElementOf0(VAR_0,xP) )
& aSet0(xP) ),
inference(cnf_transformation,[status(thm)],[sk_m__1244_sk]) ).
cnf(c_156,plain,
( aElementOf0(A,xP)
| aElementOf0(sK0(A),xT)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,A),A)
| ~ aElementOf0(A,xU) ),
inference(split_conjunct,[status(thm)],[sk_m__1244]) ).
cnf(c_157,plain,
( aElementOf0(A,xP)
| ~ sdtlseqdt0(sK0(A),A)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,A),A)
| ~ aElementOf0(A,xU) ),
inference(split_conjunct,[status(thm)],[sk_m__1244]) ).
cnf(c_158,plain,
( aElementOf0(A,xP)
| ~ aUpperBoundOfIn0(A,xT,xU)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,A),A)
| ~ aElementOf0(A,xU) ),
inference(split_conjunct,[status(thm)],[sk_m__1244]) ).
cnf(c_160,plain,
aElementOf0(xp,xU),
inference(clausify,[status(thm)],[m__1261]) ).
cnf(c_161,plain,
( sdtlseqdt0(xp,A)
| ~ aElementOf0(A,xP) ),
inference(clausify,[status(thm)],[m__1261]) ).
cnf(c_165,plain,
( sdtlseqdt0(A,xp)
| ~ aLowerBoundOfIn0(A,xP,xU) ),
inference(clausify,[status(thm)],[m__1261]) ).
cnf(c_168,plain,
aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU),
inference(clausify,[status(thm)],[m__1299]) ).
cnf(c_169,plain,
( sdtlseqdt0(A,sdtlpdtrp0(xf,xp))
| ~ aElementOf0(A,xT) ),
inference(clausify,[status(thm)],[m__1299]) ).
cnf(c_170,plain,
aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU),
inference(clausify,[status(thm)],[m__1299]) ).
fof(nnf_30,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
& ( ? [W0] :
( ~ sdtlseqdt0(xp,W0)
& aUpperBoundOfIn0(W0,xT,xS)
& ! [W1] :
( sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,xT) )
& aElementOf0(W0,xS) )
| ( ~ aUpperBoundOfIn0(xp,xT,xS)
& ? [X0] :
( ~ sdtlseqdt0(X0,xp)
& aElementOf0(X0,xT) ) ) ) )
| ( ~ aFixedPointOf0(xp,xf)
& ( sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
& ( ( ~ sdtlseqdt0(xp,sK2)
& aUpperBoundOfIn0(sK2,xT,xS)
& ! [W1] :
( sdtlseqdt0(W1,sK2)
| ~ aElementOf0(W1,xT) )
& aElementOf0(sK2,xS) )
| ( ~ aUpperBoundOfIn0(xp,xT,xS)
& ~ sdtlseqdt0(sK1,xp)
& aElementOf0(sK1,xT) ) ) )
| ( ~ aFixedPointOf0(xp,xf)
& ( sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(W0,sK2)],[nnf_30]) ).
fof(sk_m___neg,plain,
( ( ~ aSupremumOfIn0(xp,xT,xS)
| ~ aFixedPointOf0(xp,xf) )
& ( ~ sdtlseqdt0(xp,sK2)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| ~ aFixedPointOf0(xp,xf) )
& ( aUpperBoundOfIn0(sK2,xT,xS)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| ~ aFixedPointOf0(xp,xf) )
& ! [VAR_0] :
( sdtlseqdt0(VAR_0,sK2)
| ~ aElementOf0(VAR_0,xT)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| ~ aFixedPointOf0(xp,xf) )
& ( aElementOf0(sK2,xS)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| ~ aFixedPointOf0(xp,xf) )
& ( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp)
| ~ aFixedPointOf0(xp,xf) )
& ( aUpperBoundOfIn0(sK2,xT,xS)
| ~ sdtlseqdt0(sK1,xp)
| ~ aFixedPointOf0(xp,xf) )
& ! [VAR_0] :
( sdtlseqdt0(VAR_0,sK2)
| ~ aElementOf0(VAR_0,xT)
| ~ sdtlseqdt0(sK1,xp)
| ~ aFixedPointOf0(xp,xf) )
& ( aElementOf0(sK2,xS)
| ~ sdtlseqdt0(sK1,xp)
| ~ aFixedPointOf0(xp,xf) )
& ( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT)
| ~ aFixedPointOf0(xp,xf) )
& ( aUpperBoundOfIn0(sK2,xT,xS)
| aElementOf0(sK1,xT)
| ~ aFixedPointOf0(xp,xf) )
& ! [VAR_0] :
( sdtlseqdt0(VAR_0,sK2)
| ~ aElementOf0(VAR_0,xT)
| aElementOf0(sK1,xT)
| ~ aFixedPointOf0(xp,xf) )
& ( aElementOf0(sK2,xS)
| aElementOf0(sK1,xT)
| ~ aFixedPointOf0(xp,xf) )
& ( ~ aSupremumOfIn0(xp,xT,xS)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( ~ sdtlseqdt0(xp,sK2)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( aUpperBoundOfIn0(sK2,xT,xS)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ! [VAR_0] :
( sdtlseqdt0(VAR_0,sK2)
| ~ aElementOf0(VAR_0,xT)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( aElementOf0(sK2,xS)
| ~ aUpperBoundOfIn0(xp,xT,xS)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( aUpperBoundOfIn0(sK2,xT,xS)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ! [VAR_0] :
( sdtlseqdt0(VAR_0,sK2)
| ~ aElementOf0(VAR_0,xT)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( aElementOf0(sK2,xS)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( aUpperBoundOfIn0(sK2,xT,xS)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ! [VAR_0] :
( sdtlseqdt0(VAR_0,sK2)
| ~ aElementOf0(VAR_0,xT)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) )
& ( aElementOf0(sK2,xS)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_171,negated_conjecture,
( aElementOf0(sK2,xS)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_3313,negated_conjecture,
( aElementOf0(sK2,xS)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_134,c_171]) ).
cnf(c_3314,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_145,c_3313]) ).
cnf(c_172,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp ),
inference(resolve,[status(thm)],[c_160,c_3314]) ).
cnf(c_173,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_3315,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_134,c_173]) ).
cnf(c_174,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp ),
inference(resolve,[status(thm)],[c_160,c_3315]) ).
cnf(c_177,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_3316,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_134,c_177]) ).
cnf(c_178,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT)
| sdtlpdtrp0(xf,xp) != xp ),
inference(resolve,[status(thm)],[c_160,c_3316]) ).
cnf(c_179,negated_conjecture,
( aElementOf0(sK2,xS)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_3317,negated_conjecture,
( aElementOf0(sK2,xS)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_134,c_179]) ).
cnf(c_3318,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_145,c_3317]) ).
cnf(c_180,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp ),
inference(resolve,[status(thm)],[c_160,c_3318]) ).
cnf(c_181,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_3319,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_134,c_181]) ).
cnf(c_182,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp ),
inference(resolve,[status(thm)],[c_160,c_3319]) ).
cnf(c_185,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,szDzozmdt0(xf)) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_3320,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp
| ~ aElementOf0(xp,xU) ),
inference(paramod,[status(thm)],[c_134,c_185]) ).
cnf(c_186,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp)
| sdtlpdtrp0(xf,xp) != xp ),
inference(resolve,[status(thm)],[c_160,c_3320]) ).
cnf(c_226,plain,
( aElementOf0(sdtlpdtrp0(xf,A),szRzazndt0(xf))
| ~ aElementOf0(A,szDzozmdt0(xf)) ),
inference(resolve,[status(thm)],[c_39,c_48]) ).
cnf(c_3321,plain,
( aElementOf0(sdtlpdtrp0(xf,A),szRzazndt0(xf))
| ~ aElementOf0(A,xU) ),
inference(paramod,[status(thm)],[c_134,c_226]) ).
cnf(c_3322,plain,
( aElementOf0(sdtlpdtrp0(xf,A),szDzozmdt0(xf))
| ~ aElementOf0(A,xU) ),
inference(paramod,[status(thm)],[c_132,c_3321]) ).
cnf(c_227,plain,
( aElementOf0(sdtlpdtrp0(xf,A),xU)
| ~ aElementOf0(A,xU) ),
inference(paramod,[status(thm)],[c_134,c_3322]) ).
cnf(c_3323,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,A),sdtlpdtrp0(xf,B))
| ~ sdtlseqdt0(A,B)
| ~ aElementOf0(B,szDzozmdt0(xf))
| ~ aElementOf0(A,xU) ),
inference(paramod,[status(thm)],[c_134,c_131]) ).
cnf(c_244,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,A),sdtlpdtrp0(xf,B))
| ~ sdtlseqdt0(A,B)
| ~ aElementOf0(B,xU)
| ~ aElementOf0(A,xU) ),
inference(paramod,[status(thm)],[c_134,c_3323]) ).
cnf(c_248,plain,
( sdtlpdtrp0(xf,A) = A
| ~ aElementOf0(A,cS1142(xf)) ),
inference(paramod,[status(thm)],[c_145,c_139]) ).
cnf(c_249,plain,
( aElementOf0(A,xU)
| ~ aElementOf0(A,cS1142(xf)) ),
inference(paramod,[status(thm)],[c_145,c_138]) ).
cnf(c_250,plain,
aSet0(cS1142(xf)),
inference(paramod,[status(thm)],[c_145,c_136]) ).
cnf(c_251,plain,
( aElement0(A)
| ~ aElementOf0(A,xU) ),
inference(resolve,[status(thm)],[c_61,c_54]) ).
cnf(c_3324,plain,
( aElement0(xp)
| ~ aSet0(xU) ),
inference(resolve,[status(thm)],[c_160,c_61]) ).
cnf(c_492,plain,
aElement0(xp),
inference(resolve,[status(thm)],[c_54,c_3324]) ).
cnf(c_501,plain,
sdtlseqdt0(sdtlpdtrp0(xf,xp),xp),
inference(resolve,[status(thm)],[c_168,c_165]) ).
cnf(c_512,plain,
( aElementOf0(sdtlpdtrp0(xf,xp),xP)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp))
| ~ aElementOf0(sdtlpdtrp0(xf,xp),xU) ),
inference(resolve,[status(thm)],[c_170,c_158]) ).
cnf(c_525,plain,
aElementOf0(sdtlpdtrp0(xf,xp),xU),
inference(resolve,[status(thm)],[c_227,c_160]) ).
cnf(c_528,plain,
( aElementOf0(sdtlpdtrp0(xf,xp),xP)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp)) ),
inference(resolve,[status(thm)],[c_525,c_512]) ).
cnf(c_604,plain,
( aElement0(A)
| ~ aElementOf0(A,cS1142(xf)) ),
inference(resolve,[status(thm)],[c_250,c_61]) ).
cnf(c_3325,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp))
| ~ aElementOf0(xp,xU)
| ~ aElementOf0(sdtlpdtrp0(xf,xp),xU) ),
inference(resolve,[status(thm)],[c_501,c_244]) ).
cnf(c_3326,plain,
( sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp))
| ~ aElementOf0(xp,xU) ),
inference(resolve,[status(thm)],[c_525,c_3325]) ).
cnf(c_667,plain,
sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp)),
inference(resolve,[status(thm)],[c_160,c_3326]) ).
cnf(c_3327,plain,
( sdtlpdtrp0(xf,xp) = xp
| ~ sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))
| ~ aElement0(sdtlpdtrp0(xf,xp))
| ~ aElement0(xp) ),
inference(resolve,[status(thm)],[c_501,c_67]) ).
cnf(c_670,plain,
( sdtlpdtrp0(xf,xp) = xp
| ~ sdtlseqdt0(xp,sdtlpdtrp0(xf,xp))
| ~ aElement0(sdtlpdtrp0(xf,xp)) ),
inference(resolve,[status(thm)],[c_492,c_3327]) ).
cnf(c_671,plain,
aElementOf0(sdtlpdtrp0(xf,xp),xP),
inference(resolve,[status(thm)],[c_667,c_528]) ).
cnf(c_672,plain,
aElement0(sdtlpdtrp0(xf,xp)),
inference(resolve,[status(thm)],[c_525,c_251]) ).
cnf(c_706,plain,
( sdtlpdtrp0(xf,xp) = xp
| ~ sdtlseqdt0(xp,sdtlpdtrp0(xf,xp)) ),
inference(resolve,[status(thm)],[c_672,c_670]) ).
cnf(c_717,plain,
sdtlseqdt0(xp,sdtlpdtrp0(xf,xp)),
inference(resolve,[status(thm)],[c_671,c_161]) ).
cnf(c_733,plain,
sdtlpdtrp0(xf,xp) = xp,
inference(resolve,[status(thm)],[c_717,c_706]) ).
cnf(c_3328,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp)
| xp != xp ),
inference(paramod,[status(thm)],[c_733,c_186]) ).
cnf(c_765,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| ~ sdtlseqdt0(sK1,xp) ),
inference(copy,[status(thm)],[c_3328]) ).
cnf(c_3329,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| ~ sdtlseqdt0(sK1,xp)
| xp != xp ),
inference(paramod,[status(thm)],[c_733,c_182]) ).
cnf(c_767,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| ~ sdtlseqdt0(sK1,xp) ),
inference(copy,[status(thm)],[c_3329]) ).
cnf(c_3330,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| ~ sdtlseqdt0(sK1,xp)
| xp != xp ),
inference(paramod,[status(thm)],[c_733,c_180]) ).
cnf(c_768,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| ~ sdtlseqdt0(sK1,xp) ),
inference(copy,[status(thm)],[c_3330]) ).
cnf(c_3331,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT)
| xp != xp ),
inference(paramod,[status(thm)],[c_733,c_178]) ).
cnf(c_769,negated_conjecture,
( ~ sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT) ),
inference(copy,[status(thm)],[c_3331]) ).
cnf(c_3332,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| aElementOf0(sK1,xT)
| xp != xp ),
inference(paramod,[status(thm)],[c_733,c_174]) ).
cnf(c_771,negated_conjecture,
( sdtlseqdt0(A,sK2)
| ~ aElementOf0(A,xT)
| aElementOf0(sK1,xT) ),
inference(copy,[status(thm)],[c_3332]) ).
cnf(c_3333,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| aElementOf0(sK1,xT)
| xp != xp ),
inference(paramod,[status(thm)],[c_733,c_172]) ).
cnf(c_772,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| aElementOf0(sK1,xT) ),
inference(copy,[status(thm)],[c_3333]) ).
cnf(c_774,plain,
( sdtlseqdt0(A,xp)
| ~ aElementOf0(A,xT) ),
inference(paramod,[status(thm)],[c_733,c_169]) ).
cnf(c_889,plain,
( sdtlseqdt0(sK1,xp)
| aElementOf0(sK2,cS1142(xf)) ),
inference(resolve,[status(thm)],[c_772,c_774]) ).
cnf(c_915,plain,
( aElement0(sK2)
| aElementOf0(sK1,xT) ),
inference(resolve,[status(thm)],[c_772,c_604]) ).
cnf(c_939,plain,
( sdtlseqdt0(sK1,xp)
| aElement0(sK2) ),
inference(resolve,[status(thm)],[c_915,c_774]) ).
cnf(c_986,plain,
( aElementOf0(sK2,cS1142(xf))
| aElement0(sK2) ),
inference(resolve,[status(thm)],[c_939,c_768]) ).
cnf(c_3334,plain,
( aElement0(sK2)
| aElement0(sK2) ),
inference(resolve,[status(thm)],[c_986,c_604]) ).
cnf(c_1896,plain,
aElement0(sK2),
inference(copy,[status(thm)],[c_3334]) ).
cnf(c_1909,plain,
sdtlseqdt0(sK2,sK2),
inference(resolve,[status(thm)],[c_1896,c_66]) ).
cnf(c_3335,negated_conjecture,
( aElementOf0(sK2,cS1142(xf))
| aElementOf0(sK2,cS1142(xf)) ),
inference(resolve,[status(thm)],[c_889,c_768]) ).
cnf(c_1976,negated_conjecture,
aElementOf0(sK2,cS1142(xf)),
inference(copy,[status(thm)],[c_3335]) ).
cnf(c_1982,plain,
aElementOf0(sK2,xU),
inference(resolve,[status(thm)],[c_1976,c_249]) ).
cnf(c_1983,plain,
sdtlpdtrp0(xf,sK2) = sK2,
inference(resolve,[status(thm)],[c_1976,c_248]) ).
cnf(c_3336,plain,
( aElementOf0(sK2,xP)
| ~ sdtlseqdt0(sK0(sK2),sK2)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,sK2),sK2) ),
inference(resolve,[status(thm)],[c_1982,c_157]) ).
cnf(c_3337,plain,
( aElementOf0(sK2,xP)
| ~ sdtlseqdt0(sK0(sK2),sK2)
| ~ sdtlseqdt0(sK2,sK2) ),
inference(paramod,[status(thm)],[c_1983,c_3336]) ).
cnf(c_2047,plain,
( aElementOf0(sK2,xP)
| ~ sdtlseqdt0(sK0(sK2),sK2) ),
inference(resolve,[status(thm)],[c_1909,c_3337]) ).
cnf(c_3338,plain,
( aElementOf0(sK2,xP)
| aElementOf0(sK0(sK2),xT)
| ~ sdtlseqdt0(sdtlpdtrp0(xf,sK2),sK2) ),
inference(resolve,[status(thm)],[c_1982,c_156]) ).
cnf(c_3339,plain,
( aElementOf0(sK2,xP)
| aElementOf0(sK0(sK2),xT)
| ~ sdtlseqdt0(sK2,sK2) ),
inference(paramod,[status(thm)],[c_1983,c_3338]) ).
cnf(c_2048,plain,
( aElementOf0(sK2,xP)
| aElementOf0(sK0(sK2),xT) ),
inference(resolve,[status(thm)],[c_1909,c_3339]) ).
cnf(c_2152,plain,
( sdtlseqdt0(xp,sK2)
| aElementOf0(sK0(sK2),xT) ),
inference(resolve,[status(thm)],[c_2048,c_161]) ).
cnf(c_2509,plain,
( sdtlseqdt0(sK0(sK2),sK2)
| ~ sdtlseqdt0(sK1,xp)
| sdtlseqdt0(xp,sK2) ),
inference(resolve,[status(thm)],[c_2152,c_767]) ).
cnf(c_2533,plain,
( aElementOf0(sK1,xT)
| aElementOf0(sK0(sK2),xT) ),
inference(resolve,[status(thm)],[c_2152,c_769]) ).
cnf(c_3340,negated_conjecture,
( sdtlseqdt0(sK0(sK2),sK2)
| aElementOf0(sK1,xT)
| aElementOf0(sK1,xT) ),
inference(resolve,[status(thm)],[c_2533,c_771]) ).
cnf(c_2609,negated_conjecture,
( sdtlseqdt0(sK0(sK2),sK2)
| aElementOf0(sK1,xT) ),
inference(copy,[status(thm)],[c_3340]) ).
cnf(c_2973,plain,
( aElementOf0(sK2,xP)
| aElementOf0(sK1,xT) ),
inference(resolve,[status(thm)],[c_2609,c_2047]) ).
cnf(c_3008,plain,
( sdtlseqdt0(xp,sK2)
| aElementOf0(sK1,xT) ),
inference(resolve,[status(thm)],[c_2973,c_161]) ).
cnf(c_3341,negated_conjecture,
( aElementOf0(sK1,xT)
| aElementOf0(sK1,xT) ),
inference(resolve,[status(thm)],[c_3008,c_769]) ).
cnf(c_3168,negated_conjecture,
aElementOf0(sK1,xT),
inference(copy,[status(thm)],[c_3341]) ).
cnf(c_3170,plain,
sdtlseqdt0(sK1,xp),
inference(resolve,[status(thm)],[c_3168,c_774]) ).
cnf(c_3200,plain,
( sdtlseqdt0(sK0(sK2),sK2)
| sdtlseqdt0(xp,sK2) ),
inference(resolve,[status(thm)],[c_3170,c_2509]) ).
cnf(c_3204,negated_conjecture,
~ sdtlseqdt0(xp,sK2),
inference(resolve,[status(thm)],[c_3170,c_765]) ).
cnf(c_3207,negated_conjecture,
sdtlseqdt0(sK0(sK2),sK2),
inference(resolve,[status(thm)],[c_3204,c_3200]) ).
cnf(c_3237,plain,
aElementOf0(sK2,xP),
inference(resolve,[status(thm)],[c_3207,c_2047]) ).
cnf(c_3342,plain,
sdtlseqdt0(xp,sK2),
inference(resolve,[status(thm)],[c_3237,c_161]) ).
cnf(c_3312,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3204,c_3342]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT387+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 21:39:15 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2607303 was started by sandbox on n009,
% 0.13/0.36 % Fri Sep 25 21:39:15 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 1.82/0.62
% 1.82/0.62 % SZS status Theorem for theBenchmark
% 1.82/0.62
% 1.82/0.62 % Proof 1 at 0.19 (+ 0.04) seconds.
% 1.82/0.62 % Length of proof is 101.
% 1.82/0.62 % Level of proof is 26.
% 1.82/0.62 % Maximum clause weight is 27.000.
% 1.82/0.62 % Given clauses 415.
% 1.82/0.62
% 1.82/0.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------