%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM578+3 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:57:53 PM UTC 2026
% Result : Theorem 25.92s 15.16s
% Output : CNFRefutation 26.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 5
% Syntax : Number of formulae : 42 ( 9 unt; 0 def)
% Number of atoms : 218 ( 23 equ)
% Maximal formula atoms : 39 ( 5 avg)
% Number of connectives : 259 ( 83 ~; 78 |; 63 &)
% ( 4 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 65 ( 0 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
( ! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(X1),X2)
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X1))
& X3 != szmzizndt0(sdtlpdtrp0(xN,X1)) ) )
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X2))
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSubsetOf0(sdtlpdtrp0(xN,X2),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ~ ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X2)),sdtlpdtrp0(xN,X2))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X2))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X2)),X3) ) )
=> ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X2)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X2)),X3) ) )
| szmzizndt0(sdtlpdtrp0(xN,X2)) = szmzizndt0(sdtlpdtrp0(xN,X1)) ) ) ) ) )
=> ( xi != xj
=> ~ ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xj))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(mLessTotal,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLessTotal) ).
fof(m__3856,hypothesis,
( aElementOf0(xi,szNzAzT0)
& aElementOf0(xj,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3856) ).
fof(mLessASymm,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLessASymm) ).
fof(c_0_4,plain,
! [X2,X1] :
( epred1_2(X1,X2)
<=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X1))
& X3 != szmzizndt0(sdtlpdtrp0(xN,X1)) ) )
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X2))
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSubsetOf0(sdtlpdtrp0(xN,X2),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ~ ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X2)),sdtlpdtrp0(xN,X2))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X2))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X2)),X3) ) )
=> ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X2)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X2)),X3) ) )
| szmzizndt0(sdtlpdtrp0(xN,X2)) = szmzizndt0(sdtlpdtrp0(xN,X1)) ) ) ) ),
introduced(definition) ).
fof(c_0_5,negated_conjecture,
~ ( ! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(X1),X2)
=> epred1_2(X1,X2) ) )
=> ( xi != xj
=> ~ ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,xj))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1) )
& szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)) ) ) ),
inference(apply_def,[status(thm)],[inference(assume_negation,[status(cth)],[m__]),c_0_4]) ).
fof(c_0_6,negated_conjecture,
! [X388,X389,X390,X391] :
( ( ~ aElementOf0(X388,szNzAzT0)
| ~ aElementOf0(X389,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X388),X389)
| epred1_2(X388,X389) )
& xi != xj
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& ( ~ aElementOf0(X390,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X390) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj))
& ( ~ aElementOf0(X391,sdtlpdtrp0(xN,xj))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X391) )
& szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])]) ).
fof(c_0_7,plain,
! [X252,X253] :
( ~ aElementOf0(X252,szNzAzT0)
| ~ aElementOf0(X253,szNzAzT0)
| sdtlseqdt0(X252,X253)
| sdtlseqdt0(szszuzczcdt0(X253),X252) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessTotal])]) ).
fof(c_0_8,plain,
! [X2,X1] :
( epred1_2(X1,X2)
=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
<=> ( aElement0(X3)
& aElementOf0(X3,sdtlpdtrp0(xN,X1))
& X3 != szmzizndt0(sdtlpdtrp0(xN,X1)) ) )
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X2))
=> aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))) )
& aSubsetOf0(sdtlpdtrp0(xN,X2),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
& ~ ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X2)),sdtlpdtrp0(xN,X2))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X2))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X2)),X3) ) )
=> ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X2)),sdtlpdtrp0(xN,X1))
& ! [X3] :
( aElementOf0(X3,sdtlpdtrp0(xN,X1))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X2)),X3) ) )
| szmzizndt0(sdtlpdtrp0(xN,X2)) = szmzizndt0(sdtlpdtrp0(xN,X1)) ) ) ) ),
inference(split_equiv,[status(thm)],[c_0_4]) ).
cnf(c_0_9,negated_conjecture,
( epred1_2(X1,X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X1),X2) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_10,hypothesis,
aElementOf0(xi,szNzAzT0),
inference(split_conjunct,[status(thm)],[m__3856]) ).
cnf(c_0_11,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X2),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_12,hypothesis,
aElementOf0(xj,szNzAzT0),
inference(split_conjunct,[status(thm)],[m__3856]) ).
fof(c_0_13,plain,
! [X392,X393,X394,X395,X396,X397,X398] :
( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X393)),sdtlpdtrp0(xN,X393))
| ~ epred1_2(X393,X392) )
& ( ~ aElementOf0(X394,sdtlpdtrp0(xN,X393))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X393)),X394)
| ~ epred1_2(X393,X392) )
& ( aSet0(sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( aElement0(X395)
| ~ aElementOf0(X395,sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( aElementOf0(X395,sdtlpdtrp0(xN,X393))
| ~ aElementOf0(X395,sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( X395 != szmzizndt0(sdtlpdtrp0(xN,X393))
| ~ aElementOf0(X395,sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( ~ aElement0(X396)
| ~ aElementOf0(X396,sdtlpdtrp0(xN,X393))
| X396 = szmzizndt0(sdtlpdtrp0(xN,X393))
| aElementOf0(X396,sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( ~ aElementOf0(X397,sdtlpdtrp0(xN,X392))
| aElementOf0(X397,sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( aSubsetOf0(sdtlpdtrp0(xN,X392),sdtmndt0(sdtlpdtrp0(xN,X393),szmzizndt0(sdtlpdtrp0(xN,X393))))
| ~ epred1_2(X393,X392) )
& ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X392)),sdtlpdtrp0(xN,X392))
| ~ epred1_2(X393,X392) )
& ( ~ aElementOf0(X398,sdtlpdtrp0(xN,X392))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X392)),X398)
| ~ epred1_2(X393,X392) )
& ( aElementOf0(esk32_2(X392,X393),sdtlpdtrp0(xN,X393))
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X392)),sdtlpdtrp0(xN,X393))
| ~ epred1_2(X393,X392) )
& ( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X392)),esk32_2(X392,X393))
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X392)),sdtlpdtrp0(xN,X393))
| ~ epred1_2(X393,X392) )
& ( szmzizndt0(sdtlpdtrp0(xN,X392)) != szmzizndt0(sdtlpdtrp0(xN,X393))
| ~ epred1_2(X393,X392) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])])]) ).
cnf(c_0_14,hypothesis,
( epred1_2(X1,xi)
| ~ sdtlseqdt0(szszuzczcdt0(X1),xi)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_9,c_0_10]) ).
cnf(c_0_15,hypothesis,
( sdtlseqdt0(szszuzczcdt0(xj),X1)
| sdtlseqdt0(X1,xj)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
cnf(c_0_16,plain,
( aElementOf0(esk32_2(X1,X2),sdtlpdtrp0(xN,X2))
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X2))
| ~ epred1_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_17,negated_conjecture,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj)),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_18,hypothesis,
( epred1_2(xj,xi)
| ~ sdtlseqdt0(szszuzczcdt0(xj),xi) ),
inference(spm,[status(thm)],[c_0_14,c_0_12]) ).
cnf(c_0_19,hypothesis,
( sdtlseqdt0(szszuzczcdt0(xj),xi)
| sdtlseqdt0(xi,xj) ),
inference(spm,[status(thm)],[c_0_15,c_0_10]) ).
cnf(c_0_20,negated_conjecture,
( aElementOf0(esk32_2(xi,xj),sdtlpdtrp0(xN,xj))
| ~ epred1_2(xj,xi) ),
inference(spm,[status(thm)],[c_0_16,c_0_17]) ).
cnf(c_0_21,hypothesis,
( epred1_2(xj,xi)
| sdtlseqdt0(xi,xj) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
fof(c_0_22,plain,
! [X247,X248] :
( ~ aElementOf0(X247,szNzAzT0)
| ~ aElementOf0(X248,szNzAzT0)
| ~ sdtlseqdt0(X247,X248)
| ~ sdtlseqdt0(X248,X247)
| X247 = X248 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mLessASymm])]) ).
cnf(c_0_23,negated_conjecture,
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xj)) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_24,hypothesis,
( sdtlseqdt0(xi,xj)
| aElementOf0(esk32_2(xi,xj),sdtlpdtrp0(xN,xj)) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_25,hypothesis,
( epred1_2(X1,xj)
| ~ sdtlseqdt0(szszuzczcdt0(X1),xj)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_9,c_0_12]) ).
cnf(c_0_26,hypothesis,
( sdtlseqdt0(szszuzczcdt0(xi),X1)
| sdtlseqdt0(X1,xi)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_11,c_0_10]) ).
cnf(c_0_27,plain,
( X1 = X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_28,plain,
( ~ sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),esk32_2(X1,X2))
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X2))
| ~ epred1_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_29,negated_conjecture,
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),esk32_2(xi,xj))
| sdtlseqdt0(xi,xj) ),
inference(spm,[status(thm)],[c_0_23,c_0_24]) ).
cnf(c_0_30,hypothesis,
( epred1_2(xi,xj)
| ~ sdtlseqdt0(szszuzczcdt0(xi),xj) ),
inference(spm,[status(thm)],[c_0_25,c_0_10]) ).
cnf(c_0_31,hypothesis,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(xj,xi) ),
inference(spm,[status(thm)],[c_0_26,c_0_12]) ).
cnf(c_0_32,hypothesis,
( X1 = xi
| ~ sdtlseqdt0(xi,X1)
| ~ sdtlseqdt0(X1,xi)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[c_0_27,c_0_10]) ).
cnf(c_0_33,plain,
sdtlseqdt0(xi,xj),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_17])]),c_0_21]) ).
cnf(c_0_34,negated_conjecture,
xi != xj,
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_35,plain,
( szmzizndt0(sdtlpdtrp0(xN,X1)) != szmzizndt0(sdtlpdtrp0(xN,X2))
| ~ epred1_2(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_36,negated_conjecture,
szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_37,hypothesis,
( epred1_2(xi,xj)
| sdtlseqdt0(xj,xi) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_38,hypothesis,
~ sdtlseqdt0(xj,xi),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_12])]),c_0_34]) ).
cnf(c_0_39,negated_conjecture,
( szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,X1))
| ~ epred1_2(X1,xj) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_40,hypothesis,
epred1_2(xi,xj),
inference(sr,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_41,hypothesis,
$false,
inference(spm,[status(thm)],[c_0_39,c_0_40]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM578+3 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n013.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 00:51:56 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 25.92/15.16 % Version : CSE_E---1.7
% 25.92/15.16 % Problem : theBenchmark.p
% 25.92/15.16 % SZS status Theorem for theBenchmark.p
% 25.92/15.16 % SZS output start CNFRefutation
% See solution above
% 26.00/15.20 % Total time : 12.793s
%------------------------------------------------------------------------------