%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM023+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Sun Sep 27 06:59:41 AM UTC 2026
% Result : Theorem 3.43s 0.81s
% Output : CNFRefutation 3.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 4
% Syntax : Number of formulae : 52 ( 15 unt; 0 def)
% Number of atoms : 248 ( 0 equ)
% Maximal formula atoms : 44 ( 4 avg)
% Number of connectives : 336 ( 140 ~; 150 |; 42 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-4 aty)
% Number of variables : 85 ( 0 sgn 51 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mCRDef,axiom,
! [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('theBenchmark.p',mCRDef) ).
fof(m__715,axiom,
! [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('theBenchmark.p',m__715) ).
fof(m__,conjecture,
isConfluent0(xR),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ isConfluent0(xR),
inference(assume_negation,[status(cth)],[m__]) ).
fof(m__656,axiom,
aRewritingSystem0(xR),
file('theBenchmark.p',m__656) ).
cnf(c_18,plain,
aRewritingSystem0(xR),
inference(clausify,[status(thm)],[m__656]) ).
fof(nnf_10,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) )
& ( ! [X0,X1,X2] :
( ? [X3] :
( sdtmndtasgtdt0(X2,W0,X3)
& sdtmndtasgtdt0(X1,W0,X3)
& aElement0(X3) )
| ~ sdtmndtasgtdt0(X0,W0,X2)
| ~ sdtmndtasgtdt0(X0,W0,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) )
| ~ isConfluent0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(fof_nnf,[status(thm)],[mCRDef]) ).
fof(sk_mCRDef_sk,plain,
! [W0] :
( ( ( ( ! [W4] :
( ~ sdtmndtasgtdt0(sK1(W0),W0,W4)
| ~ sdtmndtasgtdt0(sK0(W0),W0,W4)
| ~ aElement0(W4) )
& sdtmndtasgtdt0(sK2(W0),W0,sK1(W0))
& sdtmndtasgtdt0(sK2(W0),W0,sK0(W0))
& aElement0(sK1(W0))
& aElement0(sK0(W0))
& aElement0(sK2(W0)) )
| isConfluent0(W0) )
& ( ! [X0,X1,X2] :
( ( sdtmndtasgtdt0(X2,W0,sK4(W0,X0,X1,X2))
& sdtmndtasgtdt0(X1,W0,sK4(W0,X0,X1,X2))
& aElement0(sK4(W0,X0,X1,X2)) )
| ~ sdtmndtasgtdt0(X0,W0,X2)
| ~ sdtmndtasgtdt0(X0,W0,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) )
| ~ isConfluent0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK2,sK0,sK1]),skolemize(X3,sK4(W0,X0,X1,X2)),skolemize(W1,sK2(W0)),skolemize(W2,sK0(W0)),skolemize(W3,sK1(W0))],[nnf_10]) ).
fof(sk_mCRDef,plain,
( ! [VAR_0,VAR_1] :
( ~ sdtmndtasgtdt0(sK1(VAR_0),VAR_0,VAR_1)
| ~ sdtmndtasgtdt0(sK0(VAR_0),VAR_0,VAR_1)
| ~ aElement0(VAR_1)
| isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0] :
( sdtmndtasgtdt0(sK2(VAR_0),VAR_0,sK1(VAR_0))
| isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0] :
( sdtmndtasgtdt0(sK2(VAR_0),VAR_0,sK0(VAR_0))
| isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0] :
( aElement0(sK1(VAR_0))
| isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0] :
( aElement0(sK0(VAR_0))
| isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0] :
( aElement0(sK2(VAR_0))
| isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( sdtmndtasgtdt0(VAR_3,VAR_0,sK4(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ sdtmndtasgtdt0(VAR_1,VAR_0,VAR_3)
| ~ sdtmndtasgtdt0(VAR_1,VAR_0,VAR_2)
| ~ aElement0(VAR_3)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( sdtmndtasgtdt0(VAR_2,VAR_0,sK4(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ sdtmndtasgtdt0(VAR_1,VAR_0,VAR_3)
| ~ sdtmndtasgtdt0(VAR_1,VAR_0,VAR_2)
| ~ aElement0(VAR_3)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( aElement0(sK4(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ sdtmndtasgtdt0(VAR_1,VAR_0,VAR_3)
| ~ sdtmndtasgtdt0(VAR_1,VAR_0,VAR_2)
| ~ aElement0(VAR_3)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ isConfluent0(VAR_0)
| ~ aRewritingSystem0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mCRDef_sk]) ).
cnf(c_38,plain,
( ~ sdtmndtasgtdt0(sK1(A),A,B)
| ~ sdtmndtasgtdt0(sK0(A),A,B)
| ~ aElement0(B)
| isConfluent0(A)
| ~ aRewritingSystem0(A) ),
inference(split_conjunct,[status(thm)],[sk_mCRDef]) ).
cnf(c_39,plain,
( sdtmndtasgtdt0(sK2(A),A,sK1(A))
| isConfluent0(A)
| ~ aRewritingSystem0(A) ),
inference(split_conjunct,[status(thm)],[sk_mCRDef]) ).
cnf(c_40,plain,
( sdtmndtasgtdt0(sK2(A),A,sK0(A))
| isConfluent0(A)
| ~ aRewritingSystem0(A) ),
inference(split_conjunct,[status(thm)],[sk_mCRDef]) ).
cnf(c_41,plain,
( aElement0(sK1(A))
| isConfluent0(A)
| ~ aRewritingSystem0(A) ),
inference(split_conjunct,[status(thm)],[sk_mCRDef]) ).
cnf(c_42,plain,
( aElement0(sK0(A))
| isConfluent0(A)
| ~ aRewritingSystem0(A) ),
inference(split_conjunct,[status(thm)],[sk_mCRDef]) ).
cnf(c_43,plain,
( aElement0(sK2(A))
| isConfluent0(A)
| ~ aRewritingSystem0(A) ),
inference(split_conjunct,[status(thm)],[sk_mCRDef]) ).
fof(nnf_16,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(fof_nnf,[status(thm)],[m__715]) ).
fof(sk_m__715_sk,plain,
! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W2,xR,sK3(W0,W1,W2))
& sdtmndtasgtdt0(W1,xR,sK3(W0,W1,W2))
& aElement0(sK3(W0,W1,W2)) )
| ~ sdtmndtasgtdt0(W0,xR,W2)
| ~ sdtmndtasgtdt0(W0,xR,W1)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(W3,sK3(W0,W1,W2))],[nnf_16]) ).
fof(sk_m__715,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtasgtdt0(VAR_2,xR,sK3(VAR_0,VAR_1,VAR_2))
| ~ sdtmndtasgtdt0(VAR_0,xR,VAR_2)
| ~ sdtmndtasgtdt0(VAR_0,xR,VAR_1)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtasgtdt0(VAR_1,xR,sK3(VAR_0,VAR_1,VAR_2))
| ~ sdtmndtasgtdt0(VAR_0,xR,VAR_2)
| ~ sdtmndtasgtdt0(VAR_0,xR,VAR_1)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElement0(sK3(VAR_0,VAR_1,VAR_2))
| ~ sdtmndtasgtdt0(VAR_0,xR,VAR_2)
| ~ sdtmndtasgtdt0(VAR_0,xR,VAR_1)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__715_sk]) ).
cnf(c_60,plain,
( aElement0(sK3(A,B,C))
| ~ sdtmndtasgtdt0(A,xR,C)
| ~ sdtmndtasgtdt0(A,xR,B)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__715]) ).
cnf(c_61,plain,
( sdtmndtasgtdt0(B,xR,sK3(A,B,C))
| ~ sdtmndtasgtdt0(A,xR,C)
| ~ sdtmndtasgtdt0(A,xR,B)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__715]) ).
cnf(c_62,plain,
( sdtmndtasgtdt0(C,xR,sK3(A,B,C))
| ~ sdtmndtasgtdt0(A,xR,C)
| ~ sdtmndtasgtdt0(A,xR,B)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__715]) ).
cnf(c_63,negated_conjecture,
~ isConfluent0(xR),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_76,plain,
( ~ sdtmndtasgtdt0(sK1(xR),xR,A)
| ~ sdtmndtasgtdt0(sK0(xR),xR,A)
| ~ aElement0(A)
| isConfluent0(xR) ),
inference(resolve,[status(thm)],[c_18,c_38]) ).
cnf(c_77,negated_conjecture,
( ~ sdtmndtasgtdt0(sK1(xR),xR,A)
| ~ sdtmndtasgtdt0(sK0(xR),xR,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_63,c_76]) ).
cnf(c_78,plain,
( sdtmndtasgtdt0(sK2(xR),xR,sK1(xR))
| isConfluent0(xR) ),
inference(resolve,[status(thm)],[c_18,c_39]) ).
cnf(c_79,negated_conjecture,
sdtmndtasgtdt0(sK2(xR),xR,sK1(xR)),
inference(resolve,[status(thm)],[c_63,c_78]) ).
cnf(c_80,plain,
( sdtmndtasgtdt0(sK2(xR),xR,sK0(xR))
| isConfluent0(xR) ),
inference(resolve,[status(thm)],[c_18,c_40]) ).
cnf(c_81,negated_conjecture,
sdtmndtasgtdt0(sK2(xR),xR,sK0(xR)),
inference(resolve,[status(thm)],[c_63,c_80]) ).
cnf(c_82,plain,
( aElement0(sK1(xR))
| isConfluent0(xR) ),
inference(resolve,[status(thm)],[c_18,c_41]) ).
cnf(c_83,negated_conjecture,
aElement0(sK1(xR)),
inference(resolve,[status(thm)],[c_63,c_82]) ).
cnf(c_84,plain,
( aElement0(sK0(xR))
| isConfluent0(xR) ),
inference(resolve,[status(thm)],[c_18,c_42]) ).
cnf(c_85,negated_conjecture,
aElement0(sK0(xR)),
inference(resolve,[status(thm)],[c_63,c_84]) ).
cnf(c_86,plain,
( aElement0(sK2(xR))
| isConfluent0(xR) ),
inference(resolve,[status(thm)],[c_18,c_43]) ).
cnf(c_87,negated_conjecture,
aElement0(sK2(xR)),
inference(resolve,[status(thm)],[c_63,c_86]) ).
cnf(c_931,plain,
( sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(sK1(xR))
| ~ aElement0(A)
| ~ aElement0(sK2(xR)) ),
inference(resolve,[status(thm)],[c_79,c_62]) ).
cnf(c_932,plain,
( sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(sK1(xR))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_87,c_931]) ).
cnf(c_130,plain,
( sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_83,c_932]) ).
cnf(c_933,plain,
( sdtmndtasgtdt0(A,xR,sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(sK1(xR))
| ~ aElement0(A)
| ~ aElement0(sK2(xR)) ),
inference(resolve,[status(thm)],[c_79,c_61]) ).
cnf(c_934,plain,
( sdtmndtasgtdt0(A,xR,sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(sK1(xR))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_87,c_933]) ).
cnf(c_132,plain,
( sdtmndtasgtdt0(A,xR,sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_83,c_934]) ).
cnf(c_935,plain,
( aElement0(sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(sK1(xR))
| ~ aElement0(A)
| ~ aElement0(sK2(xR)) ),
inference(resolve,[status(thm)],[c_79,c_60]) ).
cnf(c_936,plain,
( aElement0(sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(sK1(xR))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_87,c_935]) ).
cnf(c_134,plain,
( aElement0(sK3(sK2(xR),A,sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_83,c_936]) ).
cnf(c_937,plain,
( sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,sK0(xR)) ),
inference(resolve,[status(thm)],[c_130,c_85]) ).
cnf(c_498,plain,
sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR))),
inference(resolve,[status(thm)],[c_81,c_937]) ).
cnf(c_938,plain,
( sdtmndtasgtdt0(sK0(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,sK0(xR)) ),
inference(resolve,[status(thm)],[c_132,c_85]) ).
cnf(c_512,plain,
sdtmndtasgtdt0(sK0(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR))),
inference(resolve,[status(thm)],[c_81,c_938]) ).
cnf(c_939,plain,
( aElement0(sK3(sK2(xR),sK0(xR),sK1(xR)))
| ~ sdtmndtasgtdt0(sK2(xR),xR,sK0(xR)) ),
inference(resolve,[status(thm)],[c_134,c_85]) ).
cnf(c_534,plain,
aElement0(sK3(sK2(xR),sK0(xR),sK1(xR))),
inference(resolve,[status(thm)],[c_81,c_939]) ).
cnf(c_940,plain,
( ~ sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR)))
| ~ sdtmndtasgtdt0(sK0(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR))) ),
inference(resolve,[status(thm)],[c_534,c_77]) ).
cnf(c_941,plain,
~ sdtmndtasgtdt0(sK1(xR),xR,sK3(sK2(xR),sK0(xR),sK1(xR))),
inference(resolve,[status(thm)],[c_512,c_940]) ).
cnf(c_930,plain,
$false,
inference(resolve,[status(thm)],[c_498,c_941]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM023+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n009.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 26 23:23:00 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 1411222 was started by sandbox2 on n009,
% 0.07/0.35 % Sat Sep 26 23:23:00 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.35
% 0.12/0.35 % From the command line: assign(max_seconds, 300).
% 3.43/0.81
% 3.43/0.81 % SZS status Theorem for theBenchmark
% 3.43/0.81
% 3.43/0.81 % Proof 1 at 0.43 (+ 0.02) seconds.
% 3.43/0.81 % Length of proof is 33.
% 3.43/0.81 % Level of proof is 6.
% 3.43/0.81 % Maximum clause weight is 25.000.
% 3.43/0.81 % Given clauses 136.
% 3.43/0.81
% 3.43/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------