%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM021+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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 01:03:31 PM UTC 2026
% Result : Theorem 29.14s 4.12s
% Output : Proof 29.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 8
% Syntax : Number of formulae : 52 ( 20 unt; 3 def)
% Number of atoms : 183 ( 13 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 212 ( 81 ~; 86 |; 39 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-3 aty)
% Number of variables : 63 ( 4 sgn 31 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,definition,
! [W0,W1,W2] :
( ( aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( sdtmndtplgtdt0(W0,W1,W2)
<=> ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCDef) ).
fof(f5_nnf,plain,
! [W0,W1,W2] :
( ( ( ( ! [W3] :
( ~ sdtmndtplgtdt0(W3,W1,W2)
| ~ aReductOfIn0(W3,W0,W1)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,W1) )
| sdtmndtplgtdt0(W0,W1,W2) )
& ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1)
| ~ sdtmndtplgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [W0,W1,W2,W3] :
( ( ( ( ( ~ sdtmndtplgtdt0(W3,W1,W2)
| ~ aReductOfIn0(W3,W0,W1)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,W1) )
| sdtmndtplgtdt0(W0,W1,W2) )
& ( ( sdtmndtplgtdt0(sk0(W0,W1,W2),W1,W2)
& aReductOfIn0(sk0(W0,W1,W2),W0,W1)
& aElement0(sk0(W0,W1,W2)) )
| aReductOfIn0(W2,W0,W1)
| ~ sdtmndtplgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f5_nnf]) ).
cnf(c6,plain,
( aReductOfIn0(sk0(X0,X1,X2),X0,X1)
| aReductOfIn0(X2,X0,X1)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f12,definition,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aNormalFormOfIn0(W2,W0,W1)
<=> ( ~ ? [W3] : aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNFRDef) ).
fof(f12_nnf,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] : aReductOfIn0(W3,W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ( ( ! [W3] : ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [W0,W1,W2,W3] :
( ( ( aReductOfIn0(sk11(W0,W1,W2),W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ( ( ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f12_nnf]) ).
cnf(c38,plain,
( aElement0(X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f21,hypothesis,
( sdtmndtasgtdt0(xv,xR,xw)
& sdtmndtasgtdt0(xu,xR,xw)
& aElement0(xw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__799) ).
fof(f21_nnf,plain,
( sdtmndtasgtdt0(xv,xR,xw)
& sdtmndtasgtdt0(xu,xR,xw)
& aElement0(xw) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( sdtmndtasgtdt0(xv,xR,xw)
& sdtmndtasgtdt0(xu,xR,xw)
& aElement0(xw) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c60,plain,
aElement0(xw),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p96,plain,
( aElement0(X1)
| ~ aNormalFormOfIn0(X1,xw,X0)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c38,c60]) ).
fof(f14,hypothesis,
aRewritingSystem0(xR),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__656) ).
fof(f14_nnf,plain,
aRewritingSystem0(xR),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c43,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(p106,plain,
( aElement0(X0)
| ~ aNormalFormOfIn0(X0,xw,xR) ),
inference(resolution,[status(thm)],[p96,c43]) ).
fof(f22,hypothesis,
aNormalFormOfIn0(xd,xw,xR),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__818) ).
fof(f22_nnf,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c63,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(p107,plain,
aElement0(xd),
inference(resolution,[status(thm)],[p106,c63]) ).
cnf(p15378,plain,
( aReductOfIn0(sk0(xd,X0,X1),xd,X0)
| aReductOfIn0(X1,xd,X0)
| ~ sdtmndtplgtdt0(xd,X0,X1)
| ~ aElement0(X1)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c6,p107]) ).
cnf(p16237,plain,
( aReductOfIn0(sk0(xd,xR,X0),xd,xR)
| aReductOfIn0(X0,xd,xR)
| ~ sdtmndtplgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p15378,c43]) ).
fof(f23,hypothesis,
( sdtmndtasgtdt0(xd,xR,xx)
& sdtmndtasgtdt0(xb,xR,xx)
& aElement0(xx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__850) ).
fof(f23_nnf,plain,
( sdtmndtasgtdt0(xd,xR,xx)
& sdtmndtasgtdt0(xb,xR,xx)
& aElement0(xx) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( sdtmndtasgtdt0(xd,xR,xx)
& sdtmndtasgtdt0(xb,xR,xx)
& aElement0(xx) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c64,plain,
aElement0(xx),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p16244,plain,
( aReductOfIn0(sk0(xd,xR,xx),xd,xR)
| aReductOfIn0(xx,xd,xR)
| ~ sdtmndtplgtdt0(xd,xR,xx) ),
inference(resolution,[status(thm)],[p16237,c64]) ).
fof(f7,definition,
! [W0,W1,W2] :
( ( aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( sdtmndtasgtdt0(W0,W1,W2)
<=> ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCRDef) ).
fof(f7_nnf,plain,
! [W0,W1,W2] :
( ( ( ( ~ sdtmndtplgtdt0(W0,W1,W2)
& W0 != W2 )
| sdtmndtasgtdt0(W0,W1,W2) )
& ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2
| ~ sdtmndtasgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [W0,W1,W2] :
( ( ( ( ~ sdtmndtplgtdt0(W0,W1,W2)
& W0 != W2 )
| sdtmndtasgtdt0(W0,W1,W2) )
& ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2
| ~ sdtmndtasgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c11,plain,
( sdtmndtplgtdt0(X0,X1,X2)
| X0 = X2
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p5107,plain,
( sdtmndtplgtdt0(xd,X0,X1)
| xd = X1
| ~ sdtmndtasgtdt0(xd,X0,X1)
| ~ aElement0(X1)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c11,p107]) ).
cnf(p5520,plain,
( sdtmndtplgtdt0(xd,xR,X0)
| xd = X0
| ~ sdtmndtasgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p5107,c43]) ).
cnf(p5527,plain,
( sdtmndtplgtdt0(xd,xR,xx)
| xd = xx
| ~ sdtmndtasgtdt0(xd,xR,xx) ),
inference(resolution,[status(thm)],[p5520,c64]) ).
cnf(c66,plain,
sdtmndtasgtdt0(xd,xR,xx),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p5572,plain,
( sdtmndtplgtdt0(xd,xR,xx)
| xd = xx ),
inference(resolution,[status(thm)],[p5527,c66]) ).
cnf(p16330,plain,
( xd = xx
| aReductOfIn0(sk0(xd,xR,xx),xd,xR)
| aReductOfIn0(xx,xd,xR) ),
inference(resolution,[status(thm)],[p16244,p5572]) ).
cnf(c40,plain,
( ~ aReductOfIn0(X3,X2,X1)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p144,plain,
( ~ aReductOfIn0(X2,X1,X0)
| ~ aNormalFormOfIn0(X1,xw,X0)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c40,c60]) ).
cnf(p155,plain,
( ~ aReductOfIn0(X1,X0,xR)
| ~ aNormalFormOfIn0(X0,xw,xR) ),
inference(resolution,[status(thm)],[p144,c43]) ).
cnf(p156,plain,
~ aReductOfIn0(X0,xd,xR),
inference(resolution,[status(thm)],[p155,c63]) ).
cnf(p16331,plain,
( xd = xx
| aReductOfIn0(xx,xd,xR) ),
inference(resolution,[status(thm)],[p16330,p156]) ).
cnf(p16332,plain,
xd = xx,
inference(resolution,[status(thm)],[p16331,p156]) ).
cnf(c65,plain,
sdtmndtasgtdt0(xb,xR,xx),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p16333,plain,
sdtmndtasgtdt0(xb,xR,xd),
inference(superposition,[status(thm)],[p16332,c65]) ).
fof(f24,conjecture,
sdtmndtasgtdt0(xb,xR,xd),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f24_neg,negated_conjecture,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f24_nnf,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(nnf_transformation,[status(thm)],[f24_neg]) ).
fof(f24_sk,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c67,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p17351,plain,
$false,
inference(resolution,[status(thm)],[p16333,c67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM021+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 07:50:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 29.14/4.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.14/4.12 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------