%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM017+4 : 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 : n003.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:39 AM UTC 2026
% Result : Theorem 115.41s 16.18s
% Output : CNFRefutation 115.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 5
% Syntax : Number of formulae : 36 ( 10 unt; 0 def)
% Number of atoms : 312 ( 20 equ)
% Maximal formula atoms : 96 ( 8 avg)
% Number of connectives : 418 ( 142 ~; 182 |; 91 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-3 aty)
% Number of variables : 91 ( 0 sgn 57 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__656_01,axiom,
( isTerminating0(xR)
& ! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( ( sdtmndtplgtdt0(W0,xR,W1)
| ? [W2] :
( sdtmndtplgtdt0(W2,xR,W1)
& aReductOfIn0(W2,W0,xR)
& aElement0(W2) )
| aReductOfIn0(W1,W0,xR) )
=> iLess0(W1,W0) ) )
& isLocallyConfluent0(xR)
& ! [W0,W1,W2] :
( ( aReductOfIn0(W2,W0,xR)
& aReductOfIn0(W1,W0,xR)
& 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('theBenchmark.p',m__656_01) ).
fof(m__731,axiom,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
file('theBenchmark.p',m__731) ).
fof(m__755,axiom,
( sdtmndtasgtdt0(xu,xR,xb)
& ( ( sdtmndtplgtdt0(xu,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xu,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xu,xR) ) )
| xu = xb )
& aReductOfIn0(xu,xa,xR)
& aElement0(xu) ),
file('theBenchmark.p',m__755) ).
fof(m__779,axiom,
( sdtmndtasgtdt0(xv,xR,xc)
& ( ( sdtmndtplgtdt0(xv,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xv,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xv,xR) ) )
| xv = xc )
& aReductOfIn0(xv,xa,xR)
& aElement0(xv) ),
file('theBenchmark.p',m__779) ).
fof(m__,conjecture,
? [W0] :
( ( sdtmndtasgtdt0(xv,xR,W0)
| sdtmndtplgtdt0(xv,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xv,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xv,xR)
| xv = W0 )
& ( sdtmndtasgtdt0(xu,xR,W0)
| sdtmndtplgtdt0(xu,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xu,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xu,xR)
| xu = W0 )
& aElement0(W0) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( ( sdtmndtasgtdt0(xv,xR,W0)
| sdtmndtplgtdt0(xv,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xv,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xv,xR)
| xv = W0 )
& ( sdtmndtasgtdt0(xu,xR,W0)
| sdtmndtplgtdt0(xu,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xu,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xu,xR)
| xu = W0 )
& aElement0(W0) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_90,negated_conjecture,
( ~ sdtmndtasgtdt0(xv,xR,A)
| ~ sdtmndtasgtdt0(xu,xR,A)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_120,plain,
aReductOfIn0(xv,xa,xR),
inference(clausify,[status(thm)],[m__779]) ).
cnf(c_121,plain,
aElement0(xv),
inference(clausify,[status(thm)],[m__779]) ).
cnf(c_127,plain,
aReductOfIn0(xu,xa,xR),
inference(clausify,[status(thm)],[m__755]) ).
cnf(c_128,plain,
aElement0(xu),
inference(clausify,[status(thm)],[m__755]) ).
cnf(c_414,plain,
aElement0(xa),
inference(clausify,[status(thm)],[m__731]) ).
fof(nnf_15,plain,
( isTerminating0(xR)
& ! [W0,W1] :
( iLess0(W1,W0)
| ( ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR) )
| ~ aElement0(W1)
| ~ aElement0(W0) )
& isLocallyConfluent0(xR)
& ! [X0,X1,X2] :
( ? [W3] :
( sdtmndtasgtdt0(X2,xR,W3)
& ( ( sdtmndtplgtdt0(X2,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,X2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,X2,xR) ) )
| W3 = X2 )
& sdtmndtasgtdt0(X1,xR,W3)
& ( ( sdtmndtplgtdt0(X1,xR,W3)
& ( ? [X3] :
( sdtmndtplgtdt0(X3,xR,W3)
& aReductOfIn0(X3,X1,xR)
& aElement0(X3) )
| aReductOfIn0(W3,X1,xR) ) )
| W3 = X1 )
& aElement0(W3) )
| ~ aReductOfIn0(X2,X0,xR)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ) ),
inference(fof_nnf,[status(thm)],[m__656_01]) ).
fof(sk_m__656_01_sk,plain,
( isTerminating0(xR)
& ! [W0,W1] :
( iLess0(W1,W0)
| ( ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR) )
| ~ aElement0(W1)
| ~ aElement0(W0) )
& isLocallyConfluent0(xR)
& ! [X0,X1,X2] :
( ( sdtmndtasgtdt0(X2,xR,sK0(X0,X1,X2))
& ( ( sdtmndtplgtdt0(X2,xR,sK0(X0,X1,X2))
& ( ( sdtmndtplgtdt0(sK4(X0,X1,X2),xR,sK0(X0,X1,X2))
& aReductOfIn0(sK4(X0,X1,X2),X2,xR)
& aElement0(sK4(X0,X1,X2)) )
| aReductOfIn0(sK0(X0,X1,X2),X2,xR) ) )
| sK0(X0,X1,X2) = X2 )
& sdtmndtasgtdt0(X1,xR,sK0(X0,X1,X2))
& ( ( sdtmndtplgtdt0(X1,xR,sK0(X0,X1,X2))
& ( ( sdtmndtplgtdt0(sK3(X0,X1,X2),xR,sK0(X0,X1,X2))
& aReductOfIn0(sK3(X0,X1,X2),X1,xR)
& aElement0(sK3(X0,X1,X2)) )
| aReductOfIn0(sK0(X0,X1,X2),X1,xR) ) )
| sK0(X0,X1,X2) = X1 )
& aElement0(sK0(X0,X1,X2)) )
| ~ aReductOfIn0(X2,X0,xR)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3,sK4]),skolemize(W3,sK0(X0,X1,X2)),skolemize(X3,sK3(X0,X1,X2)),skolemize(W4,sK4(X0,X1,X2))],[nnf_15]) ).
fof(sk_m__656_01,plain,
( isTerminating0(xR)
& ! [VAR_0,VAR_1] :
( iLess0(VAR_1,VAR_0)
| ~ sdtmndtplgtdt0(VAR_0,xR,VAR_1)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( iLess0(VAR_1,VAR_0)
| ~ sdtmndtplgtdt0(VAR_2,xR,VAR_1)
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1] :
( iLess0(VAR_1,VAR_0)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& isLocallyConfluent0(xR)
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtasgtdt0(VAR_2,xR,sK0(VAR_0,VAR_1,VAR_2))
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtplgtdt0(VAR_2,xR,sK0(VAR_0,VAR_1,VAR_2))
| sK0(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtplgtdt0(sK4(VAR_0,VAR_1,VAR_2),xR,sK0(VAR_0,VAR_1,VAR_2))
| aReductOfIn0(sK0(VAR_0,VAR_1,VAR_2),VAR_2,xR)
| sK0(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aReductOfIn0(sK4(VAR_0,VAR_1,VAR_2),VAR_2,xR)
| aReductOfIn0(sK0(VAR_0,VAR_1,VAR_2),VAR_2,xR)
| sK0(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElement0(sK4(VAR_0,VAR_1,VAR_2))
| aReductOfIn0(sK0(VAR_0,VAR_1,VAR_2),VAR_2,xR)
| sK0(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtasgtdt0(VAR_1,xR,sK0(VAR_0,VAR_1,VAR_2))
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtplgtdt0(VAR_1,xR,sK0(VAR_0,VAR_1,VAR_2))
| sK0(VAR_0,VAR_1,VAR_2) = VAR_1
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sdtmndtplgtdt0(sK3(VAR_0,VAR_1,VAR_2),xR,sK0(VAR_0,VAR_1,VAR_2))
| aReductOfIn0(sK0(VAR_0,VAR_1,VAR_2),VAR_1,xR)
| sK0(VAR_0,VAR_1,VAR_2) = VAR_1
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aReductOfIn0(sK3(VAR_0,VAR_1,VAR_2),VAR_1,xR)
| aReductOfIn0(sK0(VAR_0,VAR_1,VAR_2),VAR_1,xR)
| sK0(VAR_0,VAR_1,VAR_2) = VAR_1
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElement0(sK3(VAR_0,VAR_1,VAR_2))
| aReductOfIn0(sK0(VAR_0,VAR_1,VAR_2),VAR_1,xR)
| sK0(VAR_0,VAR_1,VAR_2) = VAR_1
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( aElement0(sK0(VAR_0,VAR_1,VAR_2))
| ~ aReductOfIn0(VAR_2,VAR_0,xR)
| ~ aReductOfIn0(VAR_1,VAR_0,xR)
| ~ aElement0(VAR_2)
| ~ aElement0(VAR_1)
| ~ aElement0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__656_01_sk]) ).
cnf(c_420,plain,
( sdtmndtasgtdt0(C,xR,sK0(A,B,C))
| ~ aReductOfIn0(C,A,xR)
| ~ aReductOfIn0(B,A,xR)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__656_01]) ).
cnf(c_425,plain,
( sdtmndtasgtdt0(B,xR,sK0(A,B,C))
| ~ aReductOfIn0(C,A,xR)
| ~ aReductOfIn0(B,A,xR)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__656_01]) ).
cnf(c_430,plain,
( aElement0(sK0(A,B,C))
| ~ aReductOfIn0(C,A,xR)
| ~ aReductOfIn0(B,A,xR)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__656_01]) ).
cnf(c_19952,plain,
( sdtmndtasgtdt0(A,xR,sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A)
| ~ aElement0(xu)
| ~ aElement0(xa) ),
inference(resolve,[status(thm)],[c_420,c_127]) ).
cnf(c_19953,plain,
( sdtmndtasgtdt0(A,xR,sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A)
| ~ aElement0(xu) ),
inference(resolve,[status(thm)],[c_414,c_19952]) ).
cnf(c_2264,plain,
( sdtmndtasgtdt0(A,xR,sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_128,c_19953]) ).
cnf(c_19954,plain,
( sdtmndtasgtdt0(xu,xR,sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A)
| ~ aElement0(xu)
| ~ aElement0(xa) ),
inference(resolve,[status(thm)],[c_425,c_127]) ).
cnf(c_19955,plain,
( sdtmndtasgtdt0(xu,xR,sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A)
| ~ aElement0(xu) ),
inference(resolve,[status(thm)],[c_414,c_19954]) ).
cnf(c_2318,plain,
( sdtmndtasgtdt0(xu,xR,sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_128,c_19955]) ).
cnf(c_19956,plain,
( aElement0(sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A)
| ~ aElement0(xu)
| ~ aElement0(xa) ),
inference(resolve,[status(thm)],[c_430,c_127]) ).
cnf(c_19957,plain,
( aElement0(sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A)
| ~ aElement0(xu) ),
inference(resolve,[status(thm)],[c_414,c_19956]) ).
cnf(c_2366,plain,
( aElement0(sK0(xa,xu,A))
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_128,c_19957]) ).
cnf(c_19958,plain,
( aElement0(sK0(xa,xu,xv))
| ~ aElement0(xv) ),
inference(resolve,[status(thm)],[c_2366,c_120]) ).
cnf(c_11834,plain,
aElement0(sK0(xa,xu,xv)),
inference(resolve,[status(thm)],[c_121,c_19958]) ).
cnf(c_19959,plain,
( sdtmndtasgtdt0(xv,xR,sK0(xa,xu,xv))
| ~ aElement0(xv) ),
inference(resolve,[status(thm)],[c_2264,c_120]) ).
cnf(c_19573,plain,
sdtmndtasgtdt0(xv,xR,sK0(xa,xu,xv)),
inference(resolve,[status(thm)],[c_121,c_19959]) ).
cnf(c_19960,negated_conjecture,
( ~ sdtmndtasgtdt0(xu,xR,sK0(xa,xu,xv))
| ~ aElement0(sK0(xa,xu,xv)) ),
inference(resolve,[status(thm)],[c_19573,c_90]) ).
cnf(c_19611,negated_conjecture,
~ sdtmndtasgtdt0(xu,xR,sK0(xa,xu,xv)),
inference(resolve,[status(thm)],[c_11834,c_19960]) ).
cnf(c_19961,plain,
( sdtmndtasgtdt0(xu,xR,sK0(xa,xu,xv))
| ~ aElement0(xv) ),
inference(resolve,[status(thm)],[c_2318,c_120]) ).
cnf(c_19962,plain,
sdtmndtasgtdt0(xu,xR,sK0(xa,xu,xv)),
inference(resolve,[status(thm)],[c_121,c_19961]) ).
cnf(c_19951,plain,
$false,
inference(resolve,[status(thm)],[c_19611,c_19962]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM017+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 23:23:40 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 4068020 was started by sandbox2 on n003,
% 0.13/0.36 % Sat Sep 26 23:23:40 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.42
% 0.13/0.42 % From the command line: assign(max_seconds, 300).
% 115.41/16.18
% 115.41/16.18 % given #500 (I,wt=28): 1010 -aElement0(A) | -aElement0(B) | -aReductOfIn0(B,A,xR) | -iLess0(A,xa) | f17(A,B,A) = B | sdtmndtplgtdt0(B,xR,f17(A,B,A)). [factor(352,a,c),xx(d)].
% 115.41/16.18
% 115.41/16.18 % given #1000 (A,wt=21): 1338 aReductOfIn0(xc,xa,xR) | -aElement0(c2) | aReductOfIn0(xc,c2,xR) | sdtmndtplgtdt0(f1(c2,xR,xc),xR,xc). [resolve(130,b,65,c),unit_del(c,412)].
% 115.41/16.18
% 115.41/16.18 % given #1500 (A,wt=25): 1603 -aElement0(A) | xa != A | -iLess0(xa,xa) | f17(xa,xb,A) = A | sdtmndtplgtdt0(A,xR,f17(xa,xb,A)). [resolve(237,d,133,a),flip(d),unit_del(a,414),unit_del(b,413)].
% 115.41/16.18
% 115.41/16.18 % given #2000 (T,wt=15): 12215 -aElement0(c2) | aElement0(f14(xa,c2,xv)) | aReductOfIn0(xc,xa,xR). [resolve(2379,b,131,b)].
% 115.41/16.18
% 115.41/16.18 % given #2500 (T,wt=16): 6917 -isConfluent0(xR) | aElement0(f2(xR,xa,f13(xR,xb),xa)). [resolve(6890,a,439,d),unit_del(b,414),unit_del(c,4048),unit_del(d,2406)].
% 115.41/16.18
% 115.41/16.18 % given #3000 (T,wt=16): 18970 sdtmndtasgtdt0(xc,xR,f17(xv,xc,f17(xv,xv,xc))). [resolve(2255,b,2802,a),unit_del(a,2814)].
% 115.41/16.18
% 115.41/16.18 % SZS status Theorem for theBenchmark
% 115.41/16.18
% 115.41/16.18 % Proof 1 at 6.20 (+ 1.38) seconds.
% 115.41/16.18 % Length of proof is 21.
% 115.41/16.18 % Level of proof is 5.
% 115.41/16.18 % Maximum clause weight is 25.000.
% 115.41/16.18 % Given clauses 3242.
% 115.41/16.18
% 115.41/16.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------