%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM023+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 : n009.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 232.03s 29.74s
% Output : Proof 232.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 7
% Syntax : Number of formulae : 128 ( 109 unt; 2 def)
% Number of atoms : 249 ( 100 equ)
% Maximal formula atoms : 19 ( 1 avg)
% Number of connectives : 198 ( 77 ~; 74 |; 41 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-4 aty)
% Number of variables : 126 ( 3 sgn 34 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,definition,
! [W0] :
( aRewritingSystem0(W0)
=> ( isConfluent0(W0)
<=> ! [W1,W2,W3] :
( ( sdtmndtasgtdt0(W1,W0,W3)
& sdtmndtasgtdt0(W1,W0,W2)
& aElement0(W3)
& aElement0(W2)
& aElement0(W1) )
=> ? [W4] :
( sdtmndtasgtdt0(W3,W0,W4)
& sdtmndtasgtdt0(W2,W0,W4)
& aElement0(W4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCRDef) ).
fof(f9_nnf,plain,
! [W0] :
( ( ( ? [W1,W2,W3] :
( ! [W4] :
( ~ sdtmndtasgtdt0(W3,W0,W4)
| ~ sdtmndtasgtdt0(W2,W0,W4)
| ~ aElement0(W4) )
& sdtmndtasgtdt0(W1,W0,W3)
& sdtmndtasgtdt0(W1,W0,W2)
& aElement0(W3)
& aElement0(W2)
& aElement0(W1) )
| isConfluent0(W0) )
& ( ! [W1,W2,W3] :
( ? [W4] :
( sdtmndtasgtdt0(W3,W0,W4)
& sdtmndtasgtdt0(W2,W0,W4)
& aElement0(W4) )
| ~ sdtmndtasgtdt0(W1,W0,W3)
| ~ sdtmndtasgtdt0(W1,W0,W2)
| ~ aElement0(W3)
| ~ aElement0(W2)
| ~ aElement0(W1) )
| ~ isConfluent0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [W0,W1,W2,W3,W4] :
( ( ( ( ( ~ sdtmndtasgtdt0(sk4(W0),W0,W4)
| ~ sdtmndtasgtdt0(sk3(W0),W0,W4)
| ~ aElement0(W4) )
& sdtmndtasgtdt0(sk2(W0),W0,sk4(W0))
& sdtmndtasgtdt0(sk2(W0),W0,sk3(W0))
& aElement0(sk4(W0))
& aElement0(sk3(W0))
& aElement0(sk2(W0)) )
| isConfluent0(W0) )
& ( ( sdtmndtasgtdt0(W3,W0,sk1(W0,W1,W2,W3))
& sdtmndtasgtdt0(W2,W0,sk1(W0,W1,W2,W3))
& aElement0(sk1(W0,W1,W2,W3)) )
| ~ sdtmndtasgtdt0(W1,W0,W3)
| ~ sdtmndtasgtdt0(W1,W0,W2)
| ~ aElement0(W3)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ isConfluent0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3,sk4])],[f9_nnf]) ).
cnf(c23,plain,
( ~ sdtmndtasgtdt0(sk4(X0),X0,X4)
| ~ sdtmndtasgtdt0(sk3(X0),X0,X4)
| ~ aElement0(X4)
| isConfluent0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t51,plain,
ifeq(aRewritingSystem0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(sk3(X1),X1,X2),true,ifeq(sdtmndtasgtdt0(sk4(X1),X1,X2),true,isConfluent0(X1),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t95,plain,
ifeq(aRewritingSystem0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(sk3(X1),X1,X2),true,ifeq(sdtmndtasgtdt0(sk4(X1),X1,X2),true,isConfluent0(X1),true),true),true),true) = true,
inference(orient,[status(thm)],[t51]) ).
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(t0,plain,
aRewritingSystem0(xR) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t119,plain,
aRewritingSystem0(xR) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t144,plain,
true = ifeq(true,true,ifeq(aElement0(X1),true,ifeq(sdtmndtasgtdt0(sk3(xR),xR,X1),true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,X1),true,isConfluent0(xR),true),true),true),true),
inference(cp,[status(thm)],[t95,t119]) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t71,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t72523,plain,
true = ifeq(aElement0(X1),true,ifeq(sdtmndtasgtdt0(sk3(xR),xR,X1),true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,X1),true,isConfluent0(xR),true),true),true),
inference(step,[status(thm)],[t144,t71]) ).
fof(f17,conjecture,
isConfluent0(xR),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f17_neg,negated_conjecture,
~ isConfluent0(xR),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f17_nnf,plain,
~ isConfluent0(xR),
inference(nnf_transformation,[status(thm)],[f17_neg]) ).
fof(f17_sk,plain,
~ isConfluent0(xR),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c49,plain,
~ isConfluent0(xR),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t1,plain,
isConfluent0(xR) = false,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(t189,plain,
isConfluent0(xR) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t72524,plain,
true = ifeq(aElement0(X1),true,ifeq(sdtmndtasgtdt0(sk3(xR),xR,X1),true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,X1),true,false,true),true),true),
inference(step,[status(thm)],[t72523,t189]) ).
cnf(t2792,plain,
ifeq(aElement0(X1),true,ifeq(sdtmndtasgtdt0(sk3(xR),xR,X1),true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,X1),true,false,true),true),true) = true,
inference(orient,[status(thm)],[t72524]) ).
fof(f16,hypothesis,
! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W0,xR,W2)
& sdtmndtasgtdt0(W0,xR,W1)
& aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ? [W3] :
( sdtmndtasgtdt0(W2,xR,W3)
& sdtmndtasgtdt0(W1,xR,W3)
& aElement0(W3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__715) ).
fof(f16_nnf,plain,
! [W0,W1,W2] :
( ? [W3] :
( sdtmndtasgtdt0(W2,xR,W3)
& sdtmndtasgtdt0(W1,xR,W3)
& aElement0(W3) )
| ~ sdtmndtasgtdt0(W0,xR,W2)
| ~ sdtmndtasgtdt0(W0,xR,W1)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W2,xR,sk13(W0,W1,W2))
& sdtmndtasgtdt0(W1,xR,sk13(W0,W1,W2))
& aElement0(sk13(W0,W1,W2)) )
| ~ sdtmndtasgtdt0(W0,xR,W2)
| ~ sdtmndtasgtdt0(W0,xR,W1)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f16_nnf]) ).
cnf(c48,plain,
( sdtmndtasgtdt0(X2,xR,sk13(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(t61,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,ifeq(sdtmndtasgtdt0(X1,xR,X3),true,sdtmndtasgtdt0(X3,xR,sk13(X1,X2,X3)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t76,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,ifeq(sdtmndtasgtdt0(X1,xR,X3),true,sdtmndtasgtdt0(X3,xR,sk13(X1,X2,X3)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t61]) ).
cnf(c20,plain,
( aElement0(sk4(X0))
| isConfluent0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t30,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),aElement0(sk4(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t107,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),aElement0(sk4(X1))),true) = true,
inference(orient,[status(thm)],[t30]) ).
cnf(t192,plain,
true = ifeq(aRewritingSystem0(xR),true,or(false,aElement0(sk4(xR))),true),
inference(cp,[status(thm)],[t107,t189]) ).
cnf(t71842,plain,
true = ifeq(true,true,or(false,aElement0(sk4(xR))),true),
inference(step,[status(thm)],[t192,t119]) ).
cnf(t71843,plain,
true = or(false,aElement0(sk4(xR))),
inference(step,[status(thm)],[t71842,t71]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t74,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t71844,plain,
true = aElement0(sk4(xR)),
inference(step,[status(thm)],[t71843,t74]) ).
cnf(t207,plain,
aElement0(sk4(xR)) = true,
inference(orient,[status(thm)],[t71844]) ).
cnf(t252,plain,
true = ifeq(aElement0(X1),true,ifeq(true,true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X1,xR,sk4(xR)),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,sdtmndtasgtdt0(X2,xR,sk13(X1,sk4(xR),X2)),true),true),true),true),true),
inference(cp,[status(thm)],[t76,t207]) ).
cnf(t75634,plain,
true = ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X1,xR,sk4(xR)),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,sdtmndtasgtdt0(X2,xR,sk13(X1,sk4(xR),X2)),true),true),true),true),
inference(step,[status(thm)],[t252,t71]) ).
cnf(t70843,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X1,xR,sk4(xR)),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,sdtmndtasgtdt0(X2,xR,sk13(X1,sk4(xR),X2)),true),true),true),true) = true,
inference(orient,[status(thm)],[t75634]) ).
cnf(c21,plain,
( sdtmndtasgtdt0(sk2(X0),X0,sk3(X0))
| isConfluent0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t36,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),sdtmndtasgtdt0(sk2(X1),X1,sk3(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t108,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),sdtmndtasgtdt0(sk2(X1),X1,sk3(X1))),true) = true,
inference(orient,[status(thm)],[t36]) ).
cnf(t191,plain,
true = ifeq(aRewritingSystem0(xR),true,or(false,sdtmndtasgtdt0(sk2(xR),xR,sk3(xR))),true),
inference(cp,[status(thm)],[t108,t189]) ).
cnf(t71854,plain,
true = ifeq(true,true,or(false,sdtmndtasgtdt0(sk2(xR),xR,sk3(xR))),true),
inference(step,[status(thm)],[t191,t119]) ).
cnf(t71855,plain,
true = or(false,sdtmndtasgtdt0(sk2(xR),xR,sk3(xR))),
inference(step,[status(thm)],[t71854,t71]) ).
cnf(t71856,plain,
true = sdtmndtasgtdt0(sk2(xR),xR,sk3(xR)),
inference(step,[status(thm)],[t71855,t74]) ).
cnf(t425,plain,
sdtmndtasgtdt0(sk2(xR),xR,sk3(xR)) = true,
inference(orient,[status(thm)],[t71856]) ).
cnf(t71208,plain,
true = ifeq(aElement0(sk2(xR)),true,ifeq(aElement0(sk3(xR)),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),true),
inference(cp,[status(thm)],[t70843,t425]) ).
cnf(c18,plain,
( aElement0(sk2(X0))
| isConfluent0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t28,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),aElement0(sk2(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t105,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),aElement0(sk2(X1))),true) = true,
inference(orient,[status(thm)],[t28]) ).
cnf(t194,plain,
true = ifeq(aRewritingSystem0(xR),true,or(false,aElement0(sk2(xR))),true),
inference(cp,[status(thm)],[t105,t189]) ).
cnf(t71848,plain,
true = ifeq(true,true,or(false,aElement0(sk2(xR))),true),
inference(step,[status(thm)],[t194,t119]) ).
cnf(t71849,plain,
true = or(false,aElement0(sk2(xR))),
inference(step,[status(thm)],[t71848,t71]) ).
cnf(t71850,plain,
true = aElement0(sk2(xR)),
inference(step,[status(thm)],[t71849,t74]) ).
cnf(t337,plain,
aElement0(sk2(xR)) = true,
inference(orient,[status(thm)],[t71850]) ).
cnf(t75635,plain,
true = ifeq(true,true,ifeq(aElement0(sk3(xR)),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),true),
inference(step,[status(thm)],[t71208,t337]) ).
cnf(t75636,plain,
true = ifeq(aElement0(sk3(xR)),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),
inference(step,[status(thm)],[t75635,t71]) ).
cnf(c19,plain,
( aElement0(sk3(X0))
| isConfluent0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t29,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),aElement0(sk3(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t106,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),aElement0(sk3(X1))),true) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t193,plain,
true = ifeq(aRewritingSystem0(xR),true,or(false,aElement0(sk3(xR))),true),
inference(cp,[status(thm)],[t106,t189]) ).
cnf(t71845,plain,
true = ifeq(true,true,or(false,aElement0(sk3(xR))),true),
inference(step,[status(thm)],[t193,t119]) ).
cnf(t71846,plain,
true = or(false,aElement0(sk3(xR))),
inference(step,[status(thm)],[t71845,t71]) ).
cnf(t71847,plain,
true = aElement0(sk3(xR)),
inference(step,[status(thm)],[t71846,t74]) ).
cnf(t272,plain,
aElement0(sk3(xR)) = true,
inference(orient,[status(thm)],[t71847]) ).
cnf(t75637,plain,
true = ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),
inference(step,[status(thm)],[t75636,t272]) ).
cnf(t75638,plain,
true = ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),
inference(step,[status(thm)],[t75637,t71]) ).
cnf(c22,plain,
( sdtmndtasgtdt0(sk2(X0),X0,sk4(X0))
| isConfluent0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t37,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),sdtmndtasgtdt0(sk2(X1),X1,sk4(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t109,plain,
ifeq(aRewritingSystem0(X1),true,or(isConfluent0(X1),sdtmndtasgtdt0(sk2(X1),X1,sk4(X1))),true) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(t190,plain,
true = ifeq(aRewritingSystem0(xR),true,or(false,sdtmndtasgtdt0(sk2(xR),xR,sk4(xR))),true),
inference(cp,[status(thm)],[t109,t189]) ).
cnf(t71851,plain,
true = ifeq(true,true,or(false,sdtmndtasgtdt0(sk2(xR),xR,sk4(xR))),true),
inference(step,[status(thm)],[t190,t119]) ).
cnf(t71852,plain,
true = or(false,sdtmndtasgtdt0(sk2(xR),xR,sk4(xR))),
inference(step,[status(thm)],[t71851,t71]) ).
cnf(t71853,plain,
true = sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),
inference(step,[status(thm)],[t71852,t74]) ).
cnf(t404,plain,
sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)) = true,
inference(orient,[status(thm)],[t71853]) ).
cnf(t75639,plain,
true = ifeq(true,true,ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),
inference(step,[status(thm)],[t75638,t404]) ).
cnf(t75640,plain,
true = ifeq(true,true,sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),
inference(step,[status(thm)],[t75639,t71]) ).
cnf(t75641,plain,
true = sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),
inference(step,[status(thm)],[t75640,t71]) ).
cnf(t71209,plain,
sdtmndtasgtdt0(sk3(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))) = true,
inference(orient,[status(thm)],[t75641]) ).
cnf(t71219,plain,
true = ifeq(aElement0(sk13(sk2(xR),sk4(xR),sk3(xR))),true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true,false,true),true),true),
inference(cp,[status(thm)],[t2792,t71209]) ).
cnf(c46,plain,
( aElement0(sk13(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(t56,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,ifeq(sdtmndtasgtdt0(X1,xR,X3),true,aElement0(sk13(X1,X2,X3)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(t75,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,ifeq(sdtmndtasgtdt0(X1,xR,X3),true,aElement0(sk13(X1,X2,X3)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t409,plain,
true = ifeq(aElement0(sk2(xR)),true,ifeq(aElement0(sk4(xR)),true,ifeq(aElement0(X1),true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true),true),true),true),
inference(cp,[status(thm)],[t75,t404]) ).
cnf(t73044,plain,
true = ifeq(true,true,ifeq(aElement0(sk4(xR)),true,ifeq(aElement0(X1),true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true),true),true),true),
inference(step,[status(thm)],[t409,t337]) ).
cnf(t73045,plain,
true = ifeq(aElement0(sk4(xR)),true,ifeq(aElement0(X1),true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true),true),true),
inference(step,[status(thm)],[t73044,t71]) ).
cnf(t73046,plain,
true = ifeq(true,true,ifeq(aElement0(X1),true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true),true),true),
inference(step,[status(thm)],[t73045,t207]) ).
cnf(t73047,plain,
true = ifeq(aElement0(X1),true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true),true),
inference(step,[status(thm)],[t73046,t71]) ).
cnf(t73048,plain,
true = ifeq(aElement0(X1),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true),
inference(step,[status(thm)],[t73047,t71]) ).
cnf(t4105,plain,
ifeq(aElement0(X1),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,X1),true,aElement0(sk13(sk2(xR),sk4(xR),X1)),true),true) = true,
inference(orient,[status(thm)],[t73048]) ).
cnf(t4117,plain,
true = ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk3(xR)),true,aElement0(sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),
inference(cp,[status(thm)],[t4105,t272]) ).
cnf(t73055,plain,
true = ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk3(xR)),true,aElement0(sk13(sk2(xR),sk4(xR),sk3(xR))),true),
inference(step,[status(thm)],[t4117,t71]) ).
cnf(t73056,plain,
true = ifeq(true,true,aElement0(sk13(sk2(xR),sk4(xR),sk3(xR))),true),
inference(step,[status(thm)],[t73055,t425]) ).
cnf(t73057,plain,
true = aElement0(sk13(sk2(xR),sk4(xR),sk3(xR))),
inference(step,[status(thm)],[t73056,t71]) ).
cnf(t4566,plain,
aElement0(sk13(sk2(xR),sk4(xR),sk3(xR))) = true,
inference(orient,[status(thm)],[t73057]) ).
cnf(t75644,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true,false,true),true),true),
inference(step,[status(thm)],[t71219,t4566]) ).
cnf(t75645,plain,
true = ifeq(true,true,ifeq(sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true,false,true),true),
inference(step,[status(thm)],[t75644,t71]) ).
cnf(t75646,plain,
true = ifeq(sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true,false,true),
inference(step,[status(thm)],[t75645,t71]) ).
cnf(c47,plain,
( sdtmndtasgtdt0(X1,xR,sk13(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(t60,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,ifeq(sdtmndtasgtdt0(X1,xR,X3),true,sdtmndtasgtdt0(X2,xR,sk13(X1,X2,X3)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t77,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,ifeq(sdtmndtasgtdt0(X1,xR,X3),true,sdtmndtasgtdt0(X2,xR,sk13(X1,X2,X3)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t60]) ).
cnf(t249,plain,
true = ifeq(aElement0(X1),true,ifeq(true,true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X1,xR,sk4(xR)),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,sdtmndtasgtdt0(sk4(xR),xR,sk13(X1,sk4(xR),X2)),true),true),true),true),true),
inference(cp,[status(thm)],[t77,t207]) ).
cnf(t75123,plain,
true = ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X1,xR,sk4(xR)),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,sdtmndtasgtdt0(sk4(xR),xR,sk13(X1,sk4(xR),X2)),true),true),true),true),
inference(step,[status(thm)],[t249,t71]) ).
cnf(t40735,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(sdtmndtasgtdt0(X1,xR,sk4(xR)),true,ifeq(sdtmndtasgtdt0(X1,xR,X2),true,sdtmndtasgtdt0(sk4(xR),xR,sk13(X1,sk4(xR),X2)),true),true),true),true) = true,
inference(orient,[status(thm)],[t75123]) ).
cnf(t40947,plain,
true = ifeq(aElement0(sk2(xR)),true,ifeq(aElement0(sk3(xR)),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),true),
inference(cp,[status(thm)],[t40735,t425]) ).
cnf(t75145,plain,
true = ifeq(true,true,ifeq(aElement0(sk3(xR)),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),true),
inference(step,[status(thm)],[t40947,t337]) ).
cnf(t75146,plain,
true = ifeq(aElement0(sk3(xR)),true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),
inference(step,[status(thm)],[t75145,t71]) ).
cnf(t75147,plain,
true = ifeq(true,true,ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),true),
inference(step,[status(thm)],[t75146,t272]) ).
cnf(t75148,plain,
true = ifeq(sdtmndtasgtdt0(sk2(xR),xR,sk4(xR)),true,ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),
inference(step,[status(thm)],[t75147,t71]) ).
cnf(t75149,plain,
true = ifeq(true,true,ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),true),
inference(step,[status(thm)],[t75148,t404]) ).
cnf(t75150,plain,
true = ifeq(true,true,sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),true),
inference(step,[status(thm)],[t75149,t71]) ).
cnf(t75151,plain,
true = sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))),
inference(step,[status(thm)],[t75150,t71]) ).
cnf(t41116,plain,
sdtmndtasgtdt0(sk4(xR),xR,sk13(sk2(xR),sk4(xR),sk3(xR))) = true,
inference(orient,[status(thm)],[t75151]) ).
cnf(t75647,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t75646,t41116]) ).
cnf(t75648,plain,
true = false,
inference(step,[status(thm)],[t75647,t71]) ).
cnf(t71257,plain,
false = true,
inference(orient,[status(thm)],[t75648]) ).
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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c40,c49]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t71257]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM023+1 : 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.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 07:49:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 232.03/29.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 232.03/29.74 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------