%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM023+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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:32 PM UTC 2026
% Result : Theorem 15.75s 2.45s
% Output : Proof 15.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 62 ( 23 unt; 1 def)
% Number of atoms : 394 ( 54 equ)
% Maximal formula atoms : 33 ( 6 avg)
% Number of connectives : 529 ( 197 ~; 184 |; 143 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-4 aty)
% Number of variables : 116 ( 1 sgn 34 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,hypothesis,
! [W0,W1,W2] :
( ( ( sdtmndtasgtdt0(W0,xR,W2)
| sdtmndtplgtdt0(W0,xR,W2)
| ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR)
| W0 = W2 )
& ( sdtmndtasgtdt0(W0,xR,W1)
| sdtmndtplgtdt0(W0,xR,W1)
| ? [W3] :
( sdtmndtplgtdt0(W3,xR,W1)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W1,W0,xR)
| W0 = W1 )
& aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ? [W3] :
( sdtmndtasgtdt0(W2,xR,W3)
& ( ( sdtmndtplgtdt0(W2,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR) ) )
| W2 = W3 )
& sdtmndtasgtdt0(W1,xR,W3)
& ( ( sdtmndtplgtdt0(W1,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W1,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W1,xR) ) )
| W1 = W3 )
& aElement0(W3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__715) ).
fof(f16_nnf,plain,
! [W0,W1,W2] :
( ? [W3] :
( sdtmndtasgtdt0(W2,xR,W3)
& ( ( sdtmndtplgtdt0(W2,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR) ) )
| W2 = W3 )
& sdtmndtasgtdt0(W1,xR,W3)
& ( ( sdtmndtplgtdt0(W1,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W1,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W1,xR) ) )
| W1 = W3 )
& aElement0(W3) )
| ( ~ sdtmndtasgtdt0(W0,xR,W2)
& ~ sdtmndtplgtdt0(W0,xR,W2)
& ! [W3] :
( ~ sdtmndtplgtdt0(W3,xR,W2)
| ~ aReductOfIn0(W3,W0,xR)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,xR)
& W0 != W2 )
| ( ~ sdtmndtasgtdt0(W0,xR,W1)
& ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W3] :
( ~ sdtmndtplgtdt0(W3,xR,W1)
| ~ aReductOfIn0(W3,W0,xR)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W1,W0,xR)
& W0 != W1 )
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [W0,W1,W2,W3] :
( ( sdtmndtasgtdt0(W2,xR,sk16(W0,W1,W2))
& ( ( sdtmndtplgtdt0(W2,xR,sk16(W0,W1,W2))
& ( ( sdtmndtplgtdt0(sk18(W0,W1,W2),xR,sk16(W0,W1,W2))
& aReductOfIn0(sk18(W0,W1,W2),W2,xR)
& aElement0(sk18(W0,W1,W2)) )
| aReductOfIn0(sk16(W0,W1,W2),W2,xR) ) )
| W2 = sk16(W0,W1,W2) )
& sdtmndtasgtdt0(W1,xR,sk16(W0,W1,W2))
& ( ( sdtmndtplgtdt0(W1,xR,sk16(W0,W1,W2))
& ( ( sdtmndtplgtdt0(sk17(W0,W1,W2),xR,sk16(W0,W1,W2))
& aReductOfIn0(sk17(W0,W1,W2),W1,xR)
& aElement0(sk17(W0,W1,W2)) )
| aReductOfIn0(sk16(W0,W1,W2),W1,xR) ) )
| W1 = sk16(W0,W1,W2) )
& aElement0(sk16(W0,W1,W2)) )
| ( ~ sdtmndtasgtdt0(W0,xR,W2)
& ~ sdtmndtplgtdt0(W0,xR,W2)
& ( ~ sdtmndtplgtdt0(W3,xR,W2)
| ~ aReductOfIn0(W3,W0,xR)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,xR)
& W0 != W2 )
| ( ~ sdtmndtasgtdt0(W0,xR,W1)
& ~ sdtmndtplgtdt0(W0,xR,W1)
& ( ~ sdtmndtplgtdt0(W3,xR,W1)
| ~ aReductOfIn0(W3,W0,xR)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W1,W0,xR)
& W0 != W1 )
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16,sk17,sk18])],[f16_nnf]) ).
cnf(c334,plain,
( sdtmndtasgtdt0(X2,xR,sk16(X0,X1,X2))
| ~ sdtmndtasgtdt0(X0,xR,X2)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi329,axiom,
ifeq(aElement0(X0),true,ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X0,xR,X1),true,ifeq(sdtmndtasgtdt0(X0,xR,X2),true,sdtmndtasgtdt0(X2,xR,sk16(X0,X1,X2)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c334]) ).
fof(f17,conjecture,
( isConfluent0(xR)
| ! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W0,xR,W2)
& ( ( sdtmndtplgtdt0(W0,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR) ) )
| W0 = W2 )
& sdtmndtasgtdt0(W0,xR,W1)
& ( ( sdtmndtplgtdt0(W0,xR,W1)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W1)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W1,W0,xR) ) )
| W0 = W1 )
& aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ? [W3] :
( ( sdtmndtasgtdt0(W2,xR,W3)
| sdtmndtplgtdt0(W2,xR,W3)
| ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR)
| W2 = W3 )
& ( sdtmndtasgtdt0(W1,xR,W3)
| sdtmndtplgtdt0(W1,xR,W3)
| ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W1,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W1,xR)
| W1 = W3 )
& aElement0(W3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f17_neg,negated_conjecture,
~ ( isConfluent0(xR)
| ! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W0,xR,W2)
& ( ( sdtmndtplgtdt0(W0,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR) ) )
| W0 = W2 )
& sdtmndtasgtdt0(W0,xR,W1)
& ( ( sdtmndtplgtdt0(W0,xR,W1)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W1)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W1,W0,xR) ) )
| W0 = W1 )
& aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ? [W3] :
( ( sdtmndtasgtdt0(W2,xR,W3)
| sdtmndtplgtdt0(W2,xR,W3)
| ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR)
| W2 = W3 )
& ( sdtmndtasgtdt0(W1,xR,W3)
| sdtmndtplgtdt0(W1,xR,W3)
| ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W1,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W1,xR)
| W1 = W3 )
& aElement0(W3) ) ) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f17_nnf,plain,
( ~ isConfluent0(xR)
& ? [W0,W1,W2] :
( ! [W3] :
( ( ~ sdtmndtasgtdt0(W2,xR,W3)
& ~ sdtmndtplgtdt0(W2,xR,W3)
& ! [W4] :
( ~ sdtmndtplgtdt0(W4,xR,W3)
| ~ aReductOfIn0(W4,W2,xR)
| ~ aElement0(W4) )
& ~ aReductOfIn0(W3,W2,xR)
& W2 != W3 )
| ( ~ sdtmndtasgtdt0(W1,xR,W3)
& ~ sdtmndtplgtdt0(W1,xR,W3)
& ! [W4] :
( ~ sdtmndtplgtdt0(W4,xR,W3)
| ~ aReductOfIn0(W4,W1,xR)
| ~ aElement0(W4) )
& ~ aReductOfIn0(W3,W1,xR)
& W1 != W3 )
| ~ aElement0(W3) )
& sdtmndtasgtdt0(W0,xR,W2)
& ( ( sdtmndtplgtdt0(W0,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR) ) )
| W0 = W2 )
& sdtmndtasgtdt0(W0,xR,W1)
& ( ( sdtmndtplgtdt0(W0,xR,W1)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W1)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W1,W0,xR) ) )
| W0 = W1 )
& aElement0(W2)
& aElement0(W1)
& aElement0(W0) ) ),
inference(nnf_transformation,[status(thm)],[f17_neg]) ).
fof(f17_sk,plain,
! [W3,W4] :
( ~ isConfluent0(xR)
& ( ( ~ sdtmndtasgtdt0(sk21,xR,W3)
& ~ sdtmndtplgtdt0(sk21,xR,W3)
& ( ~ sdtmndtplgtdt0(W4,xR,W3)
| ~ aReductOfIn0(W4,sk21,xR)
| ~ aElement0(W4) )
& ~ aReductOfIn0(W3,sk21,xR)
& sk21 != W3 )
| ( ~ sdtmndtasgtdt0(sk20,xR,W3)
& ~ sdtmndtplgtdt0(sk20,xR,W3)
& ( ~ sdtmndtplgtdt0(W4,xR,W3)
| ~ aReductOfIn0(W4,sk20,xR)
| ~ aElement0(W4) )
& ~ aReductOfIn0(W3,sk20,xR)
& sk20 != W3 )
| ~ aElement0(W3) )
& sdtmndtasgtdt0(sk19,xR,sk21)
& ( ( sdtmndtplgtdt0(sk19,xR,sk21)
& ( ( sdtmndtplgtdt0(sk23,xR,sk21)
& aReductOfIn0(sk23,sk19,xR)
& aElement0(sk23) )
| aReductOfIn0(sk21,sk19,xR) ) )
| sk19 = sk21 )
& sdtmndtasgtdt0(sk19,xR,sk20)
& ( ( sdtmndtplgtdt0(sk19,xR,sk20)
& ( ( sdtmndtplgtdt0(sk22,xR,sk20)
& aReductOfIn0(sk22,sk19,xR)
& aElement0(sk22) )
| aReductOfIn0(sk20,sk19,xR) ) )
| sk19 = sk20 )
& aElement0(sk21)
& aElement0(sk20)
& aElement0(sk19) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19,sk20,sk21,sk22,sk23])],[f17_nnf]) ).
cnf(c335,plain,
aElement0(sk19),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi330,negated_conjecture,
aElement0(sk19) = true,
inference(equality_encoding,[status(esa)],[c335]) ).
cnf(c336,plain,
aElement0(sk20),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi331,negated_conjecture,
aElement0(sk20) = true,
inference(equality_encoding,[status(esa)],[c336]) ).
cnf(c337,plain,
aElement0(sk21),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi332,negated_conjecture,
aElement0(sk21) = true,
inference(equality_encoding,[status(esa)],[c337]) ).
cnf(c342,plain,
sdtmndtasgtdt0(sk19,xR,sk20),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi337,negated_conjecture,
sdtmndtasgtdt0(sk19,xR,sk20) = true,
inference(equality_encoding,[status(esa)],[c342]) ).
cnf(c347,plain,
sdtmndtasgtdt0(sk19,xR,sk21),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi342,negated_conjecture,
sdtmndtasgtdt0(sk19,xR,sk21) = true,
inference(equality_encoding,[status(esa)],[c347]) ).
cnf(h27,plain,
sdtmndtasgtdt0(sk21,xR,sk16(sk19,sk20,sk21)) = true,
inference(hyper_resolution,[status(thm)],[hi329,hi330,hi331,hi332,hi337,hi342]) ).
cnf(c329,plain,
( sdtmndtasgtdt0(X1,xR,sk16(X0,X1,X2))
| ~ sdtmndtasgtdt0(X0,xR,X2)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi324,axiom,
ifeq(aElement0(X0),true,ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X0,xR,X1),true,ifeq(sdtmndtasgtdt0(X0,xR,X2),true,sdtmndtasgtdt0(X1,xR,sk16(X0,X1,X2)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c329]) ).
cnf(h41,plain,
sdtmndtasgtdt0(sk20,xR,sk16(sk19,sk20,sk21)) = true,
inference(hyper_resolution,[status(thm)],[hi324,hi330,hi331,hi332,hi337,hi342]) ).
cnf(c324,plain,
( aElement0(sk16(X0,X1,X2))
| ~ sdtmndtasgtdt0(X0,xR,X2)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi319,axiom,
ifeq(aElement0(X0),true,ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X0,xR,X1),true,ifeq(sdtmndtasgtdt0(X0,xR,X2),true,aElement0(sk16(X0,X1,X2)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c324]) ).
cnf(h55,plain,
aElement0(sk16(sk19,sk20,sk21)) = true,
inference(hyper_resolution,[status(thm)],[hi319,hi330,hi331,hi332,hi337,hi342]) ).
cnf(c372,plain,
( ~ sdtmndtasgtdt0(sk21,xR,X3)
| ~ sdtmndtasgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi368,negated_conjecture,
ifeq(aElement0(X0),true,ifeq(sdtmndtasgtdt0(sk20,xR,X0),true,ifeq(sdtmndtasgtdt0(sk21,xR,X0),true,false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c372]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi368,h55,h41,h27]) ).
cnf(t14148,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
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(c40,plain,
( ~ aReductOfIn0(X3,X2,X1)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(c348,plain,
( sk21 != X3
| sk20 != X3
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c349,plain,
( ~ aReductOfIn0(X3,sk21,xR)
| sk20 != X3
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c350,plain,
( ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk21,xR)
| ~ aElement0(X4)
| sk20 != X3
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c351,plain,
( ~ sdtmndtplgtdt0(sk21,xR,X3)
| sk20 != X3
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c352,plain,
( ~ sdtmndtasgtdt0(sk21,xR,X3)
| sk20 != X3
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c353,plain,
( sk21 != X3
| ~ aReductOfIn0(X3,sk20,xR)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c354,plain,
( ~ aReductOfIn0(X3,sk21,xR)
| ~ aReductOfIn0(X3,sk20,xR)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c355,plain,
( ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk21,xR)
| ~ aElement0(X4)
| ~ aReductOfIn0(X3,sk20,xR)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c356,plain,
( ~ sdtmndtplgtdt0(sk21,xR,X3)
| ~ aReductOfIn0(X3,sk20,xR)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c357,plain,
( ~ sdtmndtasgtdt0(sk21,xR,X3)
| ~ aReductOfIn0(X3,sk20,xR)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c358,plain,
( sk21 != X3
| ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk20,xR)
| ~ aElement0(X4)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c359,plain,
( ~ aReductOfIn0(X3,sk21,xR)
| ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk20,xR)
| ~ aElement0(X4)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c360,plain,
( ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk21,xR)
| ~ aElement0(X4)
| ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk20,xR)
| ~ aElement0(X4)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c361,plain,
( ~ sdtmndtplgtdt0(sk21,xR,X3)
| ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk20,xR)
| ~ aElement0(X4)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c362,plain,
( ~ sdtmndtasgtdt0(sk21,xR,X3)
| ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk20,xR)
| ~ aElement0(X4)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c363,plain,
( sk21 != X3
| ~ sdtmndtplgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c364,plain,
( ~ aReductOfIn0(X3,sk21,xR)
| ~ sdtmndtplgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c365,plain,
( ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk21,xR)
| ~ aElement0(X4)
| ~ sdtmndtplgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c366,plain,
( ~ sdtmndtplgtdt0(sk21,xR,X3)
| ~ sdtmndtplgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c367,plain,
( ~ sdtmndtasgtdt0(sk21,xR,X3)
| ~ sdtmndtplgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c368,plain,
( sk21 != X3
| ~ sdtmndtasgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c369,plain,
( ~ aReductOfIn0(X3,sk21,xR)
| ~ sdtmndtasgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c370,plain,
( ~ sdtmndtplgtdt0(X4,xR,X3)
| ~ aReductOfIn0(X4,sk21,xR)
| ~ aElement0(X4)
| ~ sdtmndtasgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c371,plain,
( ~ sdtmndtplgtdt0(sk21,xR,X3)
| ~ sdtmndtasgtdt0(sk20,xR,X3)
| ~ aElement0(X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c373,plain,
~ isConfluent0(xR),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c40,c348,c349,c350,c351,c352,c353,c354,c355,c356,c357,c358,c359,c360,c361,c362,c363,c364,c365,c366,c367,c368,c369,c370,c371,c372,c373]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t14148]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM023+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n011.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 07:49:28 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 15.75/2.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.75/2.45 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------