%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM578+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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 : Fri Sep 25 02:20:26 PM UTC 2026
% Result : Theorem 25.53s 4.34s
% Output : Proof 25.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 26 ( 6 unt; 0 def)
% Number of atoms : 75 ( 31 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 85 ( 36 ~; 27 |; 13 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 12 ( 0 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f85,conjecture,
( ! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W0),W1)
=> ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) )
=> ( xi != xj
=> szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,xj)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f85_neg,negated_conjecture,
~ ( ! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W0),W1)
=> ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) )
=> ( xi != xj
=> szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,xj)) ) ),
inference(negated_conjecture,[status(cth)],[f85]) ).
fof(f85_nnf,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& xi != xj
& ! [W0,W1] :
( ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
| ~ sdtlseqdt0(szszuzczcdt0(W0),W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ) ),
inference(nnf_transformation,[status(thm)],[f85_neg]) ).
fof(f85_sk,plain,
! [W0,W1] :
( szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj))
& xi != xj
& ( ( szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
| ~ sdtlseqdt0(szszuzczcdt0(W0),W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ) ),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c195,plain,
szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
fof(f84,hypothesis,
( xi != xj
=> ( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3856_02) ).
fof(f84_nnf,plain,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi)
| xi = xj ),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi)
| xi = xj ),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c191,plain,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| sdtlseqdt0(szszuzczcdt0(xj),xi)
| xi = xj ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
fof(f83,hypothesis,
( aElementOf0(xj,szNzAzT0)
& aElementOf0(xi,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3856) ).
fof(f83_nnf,plain,
( aElementOf0(xj,szNzAzT0)
& aElementOf0(xi,szNzAzT0) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
( aElementOf0(xj,szNzAzT0)
& aElementOf0(xi,szNzAzT0) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c190,plain,
aElementOf0(xj,szNzAzT0),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(c193,plain,
( szmzizndt0(sdtlpdtrp0(xN,X1)) != szmzizndt0(sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(szszuzczcdt0(X0),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(p270,plain,
( szmzizndt0(sdtlpdtrp0(xN,X0)) != szmzizndt0(sdtlpdtrp0(xN,xj))
| ~ sdtlseqdt0(szszuzczcdt0(xj),X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[c190,c193]) ).
cnf(c189,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(p295,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,xj))
| ~ sdtlseqdt0(szszuzczcdt0(xj),xi) ),
inference(resolution,[status(thm)],[p270,c189]) ).
cnf(p1826,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,xj))
| sdtlseqdt0(szszuzczcdt0(xi),xj)
| xi = xj ),
inference(resolution,[status(thm)],[c191,p295]) ).
cnf(p1828,plain,
( sdtlseqdt0(szszuzczcdt0(xi),xj)
| xi = xj ),
inference(resolution,[status(thm)],[p1826,c195]) ).
cnf(p244,plain,
( szmzizndt0(sdtlpdtrp0(xN,X0)) != szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ sdtlseqdt0(szszuzczcdt0(xi),X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[c189,c193]) ).
cnf(p279,plain,
( szmzizndt0(sdtlpdtrp0(xN,xj)) != szmzizndt0(sdtlpdtrp0(xN,xi))
| ~ sdtlseqdt0(szszuzczcdt0(xi),xj) ),
inference(resolution,[status(thm)],[c190,p244]) ).
cnf(p1829,plain,
( szmzizndt0(sdtlpdtrp0(xN,xj)) != szmzizndt0(sdtlpdtrp0(xN,xi))
| xi = xj ),
inference(resolution,[status(thm)],[p1828,p279]) ).
cnf(p1831,plain,
( szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,xi))
| xi = xj ),
inference(superposition,[status(thm)],[c195,p1829]) ).
cnf(p1832,plain,
xi = xj,
inference(equality_resolution,[status(thm)],[p1831]) ).
cnf(c194,plain,
xi != xj,
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(p1906,plain,
$false,
inference(resolution,[status(thm)],[p1832,c194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM578+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 04:43:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 25.53/4.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.53/4.34 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------