%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM577+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:41:04 PM UTC 2026
% Result : Theorem 189.31s 34.29s
% Output : CNFRefutation 80.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 9
% Syntax : Number of formulae : 66 ( 8 unt; 3 def)
% Number of atoms : 446 ( 31 equ)
% Maximal formula atoms : 24 ( 6 avg)
% Number of connectives : 569 ( 189 ~; 166 |; 177 &)
% ( 12 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 2 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 113 ( 100 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W1,W0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> aElementOf0(W2,sdtlpdtrp0(xN,W1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
( aElementOf0(xm,szNzAzT0)
& aElementOf0(xn,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,conjecture,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
=> ( ~ ( szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xn))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)) )
& ( ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
=> ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,negated_conjecture,
~ ( sdtlseqdt0(szszuzczcdt0(xn),xm)
=> ( ~ ( szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xn))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)) )
& ( ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
=> ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f168,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f169,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f385,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f386,definition,
! [W0] :
( sP4_prd(W0)
<=> ( ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f387,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(formula_renaming,[status(thm)],[f385,f386]) ).
fof(f388,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( ( W1 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0))
| ~ aElement0(W1)
| aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) )
| ~ aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(NNF_transformation,[status(thm)],[f387]) ).
fof(f389,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( W1 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0))
| ~ aElement0(W1)
| aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ! [W1] :
( ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) )
| ~ aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(miniscoping,[status(thm)],[f388]) ).
fof(f398,plain,
! [X0,X1] :
( X1 != szmzizndt0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| sP4_prd(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f389]) ).
fof(f401,plain,
! [X0,X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| sP4_prd(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f389]) ).
fof(f404,plain,
! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aSet0(sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f407,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f408,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f409,plain,
! [W0,W1] :
( ( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) ) )
| ~ sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f410,plain,
! [X0,X1,X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f416,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f417,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f418,plain,
( ( ( szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xn))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)) )
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [W0] :
( ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) ) )
& sdtlseqdt0(szszuzczcdt0(xn),xm) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f419,definition,
( sP5_prd
<=> ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [W0] :
( ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f420,plain,
( ( ( szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xn))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)) )
| sP5_prd )
& sdtlseqdt0(szszuzczcdt0(xn),xm) ),
inference(formula_renaming,[status(thm)],[f418,f419]) ).
fof(f421,plain,
sdtlseqdt0(szszuzczcdt0(xn),xm),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f422,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))
| sP5_prd ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f426,plain,
( szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn))
| sP5_prd ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f478,plain,
! [W0] :
( ( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
| sP4_prd(W0) )
& ( ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ sP4_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f386]) ).
fof(f479,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
| sP4_prd(W0) )
& ! [W0] :
( ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ sP4_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f478]) ).
fof(f480,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
| sP4_prd(W0) )
& ! [W0] :
( ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ( ~ aElementOf0(sK34_skl(W0),szNzAzT0)
& aElementOf0(sK34_skl(W0),sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ sP4_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f479]) ).
fof(f483,plain,
! [X0] :
( ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f480]) ).
fof(f487,definition,
! [W0] :
( sP8_prd(W0)
<=> ( W0 != szmzizndt0(sdtlpdtrp0(xN,xn))
& aElementOf0(W0,sdtlpdtrp0(xN,xn))
& aElement0(W0) ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f488,plain,
( sP5_prd
<=> ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [W0] :
( ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
<=> sP8_prd(W0) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) ) ),
inference(formula_renaming,[status(thm)],[f419,f487]) ).
fof(f489,plain,
( ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
| ? [W0] :
( ( sP8_prd(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ( ~ sP8_prd(W0)
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) )
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ? [W0] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
& aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| sP5_prd )
& ( ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [W0] :
( ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& ! [W0] :
( ( ~ sP8_prd(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ( sP8_prd(W0)
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) )
| ~ sP5_prd ) ),
inference(NNF_transformation,[status(thm)],[f488]) ).
fof(f490,plain,
( ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
| ? [W0] :
( ( sP8_prd(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ( ~ sP8_prd(W0)
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) )
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ? [W0] :
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
& aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| sP5_prd )
& ( ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [W0] :
( ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
& ! [W0] :
( ~ sP8_prd(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ! [W0] :
( sP8_prd(W0)
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) )
| ~ sP5_prd ) ),
inference(miniscoping,[status(thm)],[f489]) ).
fof(f491,plain,
( ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ! [W0] :
( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xm)) )
| ( ( sP8_prd(sK37_skl)
| aElementOf0(sK37_skl,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ( ~ sP8_prd(sK37_skl)
| ~ aElementOf0(sK37_skl,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) )
| ~ aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),sK36_skl)
& aElementOf0(sK36_skl,sdtlpdtrp0(xN,xn)) )
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
| sP5_prd )
& ( ( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ~ aElementOf0(sK35_skl,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(sK35_skl,sdtlpdtrp0(xN,xm))
& ! [W0] :
( ~ sP8_prd(W0)
| aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& ! [W0] :
( sP8_prd(W0)
| ~ aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ! [W0] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn)) )
| ~ sP5_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl,sK37_skl]),skolemize(W0,sK35_skl),skolemize(W0,sK36_skl),skolemize(W0,sK37_skl)],[f490]) ).
fof(f497,plain,
( aElementOf0(sK35_skl,sdtlpdtrp0(xN,xm))
| ~ sP5_prd ),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f498,plain,
( ~ aElementOf0(sK35_skl,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
| ~ sP5_prd ),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f566,plain,
! [X0] :
( ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| sP4_prd(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f398]) ).
fof(f1345,plain,
! [X0] :
( sP5_prd
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f410,f422]) ).
fof(f1346,plain,
! [X0] :
( ~ sP5_prd
| aElementOf0(sK35_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f410,f497]) ).
fof(f1355,plain,
! [X0] :
( sP5_prd
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1345,f417]) ).
fof(f1356,plain,
! [X0] :
( ~ sP5_prd
| aElementOf0(sK35_skl,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1346,f417]) ).
fof(f3624,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ sP4_prd(X0) ),
inference(resolution,[status(thm)],[f483,f407]) ).
fof(f3627,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3624,f408]) ).
fof(f17693,plain,
! [X0] :
( ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f566,f3627]) ).
fof(f17758,plain,
! [X0,X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f401,f3627]) ).
fof(f17766,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f17758,f17693]) ).
fof(f17772,plain,
( ~ sP5_prd
| ~ aElementOf0(sK35_skl,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f17758,f498]) ).
fof(f17786,plain,
! [X0] :
( ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(duplicate_literals_removal,[status(thm)],[f17766]) ).
fof(f17791,plain,
( ~ sP5_prd
| ~ aElementOf0(sK35_skl,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(forward_subsumption_resolution,[status(thm)],[f17772,f416]) ).
fof(f17804,plain,
( ~ sP5_prd
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ sP5_prd ),
inference(resolution,[status(thm)],[f17791,f1356]) ).
fof(f17806,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ sP5_prd ),
inference(duplicate_literals_removal,[status(thm)],[f17804]) ).
fof(f17807,plain,
( ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ sP5_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f17806,f421]) ).
fof(f17808,plain,
( ~ aElementOf0(xn,szNzAzT0)
| ~ sP5_prd ),
inference(resolution,[status(thm)],[f17807,f169]) ).
fof(f17810,plain,
~ sP5_prd,
inference(forward_subsumption_resolution,[status(thm)],[f17808,f416]) ).
fof(f17842,plain,
szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(backward_subsumption_resolution,[status(thm)],[f426,f17810]) ).
fof(f21494,plain,
! [X0] :
( sP5_prd
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f17842,f1355]) ).
fof(f21495,plain,
! [X0] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X0,xm)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21494,f17810]) ).
fof(f48084,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f17786,f21495]) ).
fof(f48092,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f48084,f416]) ).
fof(f48101,plain,
~ aElementOf0(szszuzczcdt0(xn),szNzAzT0),
inference(forward_subsumption_resolution,[status(thm)],[f48092,f421]) ).
fof(f48102,plain,
~ aElementOf0(xn,szNzAzT0),
inference(resolution,[status(thm)],[f48101,f169]) ).
fof(f48104,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f48102,f416]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM577+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/10.34 % Computer : n012.cluster.edu
% 0.07/10.34 % Model : x86_64 x86_64
% 0.07/10.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/10.34 % Memory : 8046.5625MB
% 0.07/10.34 % OS : Linux 6.8.0-71-generic
% 0.07/10.35 % CPULimit : 300
% 0.07/10.35 % WCLimit : 300
% 0.07/10.35 % DateTime : Mon Sep 21 02:41:33 UTC 2026
% 0.07/10.35 % CPUTime :
% 0.07/10.36 % Drodi V4.1.1
% 189.31/34.29 % Refutation found
% 189.31/34.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 189.31/34.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 89.71/35.55 % Elapsed time: 24.988010 seconds
% 89.71/35.55 % CPU time: 185.313853 seconds
% 89.71/35.55 % Total memory used: 546.817 MB
% 89.71/35.55 % Net memory used: 501.727 MB
%------------------------------------------------------------------------------