%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM019+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 12:10:18 PM UTC 2026
% Result : Theorem 68.56s 9.08s
% Output : CNFRefutation 28.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 47
% Syntax : Number of formulae : 208 ( 53 unt; 37 def)
% Number of atoms : 811 ( 60 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 896 ( 293 ~; 326 |; 233 &)
% ( 37 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 37 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 13 con; 0-3 aty)
% Number of variables : 129 ( 97 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [W0,W1,W2,W3] :
( ( aElement0(W3)
& aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( ( sdtmndtasgtdt0(W2,W1,W3)
& sdtmndtasgtdt0(W0,W1,W2) )
=> sdtmndtasgtdt0(W0,W1,W3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
aRewritingSystem0(xR),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
( 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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,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) )
=> ( iLess0(W0,xa)
=> ? [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') ).
fof(f20,hypothesis,
( 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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
( 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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
( sdtmndtasgtdt0(xv,xR,xw)
& ( ( sdtmndtplgtdt0(xv,xR,xw)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xw)
& aReductOfIn0(W0,xv,xR)
& aElement0(W0) )
| aReductOfIn0(xw,xv,xR) ) )
| xv = xw )
& sdtmndtasgtdt0(xu,xR,xw)
& ( ( sdtmndtplgtdt0(xu,xR,xw)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xw)
& aReductOfIn0(W0,xu,xR)
& aElement0(W0) )
| aReductOfIn0(xw,xu,xR) ) )
| xu = xw )
& aElement0(xw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
( aNormalFormOfIn0(xd,xw,xR)
& ~ ? [W0] : aReductOfIn0(W0,xd,xR)
& sdtmndtasgtdt0(xw,xR,xd)
& ( ( sdtmndtplgtdt0(xw,xR,xd)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xd)
& aReductOfIn0(W0,xw,xR)
& aElement0(W0) )
| aReductOfIn0(xd,xw,xR) ) )
| xw = xd )
& aElement0(xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,conjecture,
( sdtmndtasgtdt0(xb,xR,xd)
| sdtmndtplgtdt0(xb,xR,xd)
| ? [W0] :
( sdtmndtplgtdt0(W0,xR,xd)
& aReductOfIn0(W0,xb,xR)
& aElement0(W0) )
| aReductOfIn0(xd,xb,xR)
| xb = xd ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
~ ( sdtmndtasgtdt0(xb,xR,xd)
| sdtmndtplgtdt0(xb,xR,xd)
| ? [W0] :
( sdtmndtplgtdt0(W0,xR,xd)
& aReductOfIn0(W0,xb,xR)
& aElement0(W0) )
| aReductOfIn0(xd,xb,xR)
| xb = xd ),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f53,plain,
! [W0,W1,W2,W3] :
( sdtmndtasgtdt0(W0,W1,W3)
| ~ sdtmndtasgtdt0(W2,W1,W3)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W3)
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f54,plain,
! [X0,X1,X2,X3] :
( sdtmndtasgtdt0(X0,X1,X3)
| ~ sdtmndtasgtdt0(X2,X1,X3)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X3)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f100,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f101,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)
& ! [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) )
| ~ aReductOfIn0(W2,W0,xR)
| ~ aReductOfIn0(W1,W0,xR)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f102,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)
& ! [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) )
| ! [W0] :
( ~ aReductOfIn0(W2,W0,xR)
| ~ aReductOfIn0(W1,W0,xR)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ) ) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,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)
& ! [W1,W2] :
( ( sdtmndtasgtdt0(W2,xR,sK13_skl(W2,W1))
& ( ( sdtmndtplgtdt0(W2,xR,sK13_skl(W2,W1))
& ( ( sdtmndtplgtdt0(sK15_skl(W2,W1),xR,sK13_skl(W2,W1))
& aReductOfIn0(sK15_skl(W2,W1),W2,xR)
& aElement0(sK15_skl(W2,W1)) )
| aReductOfIn0(sK13_skl(W2,W1),W2,xR) ) )
| W2 = sK13_skl(W2,W1) )
& sdtmndtasgtdt0(W1,xR,sK13_skl(W2,W1))
& ( ( sdtmndtplgtdt0(W1,xR,sK13_skl(W2,W1))
& ( ( sdtmndtplgtdt0(sK14_skl(W2,W1),xR,sK13_skl(W2,W1))
& aReductOfIn0(sK14_skl(W2,W1),W1,xR)
& aElement0(sK14_skl(W2,W1)) )
| aReductOfIn0(sK13_skl(W2,W1),W1,xR) ) )
| W1 = sK13_skl(W2,W1) )
& aElement0(sK13_skl(W2,W1)) )
| ! [W0] :
( ~ aReductOfIn0(W2,W0,xR)
| ~ aReductOfIn0(W1,W0,xR)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W3,sK13_skl(W2,W1)),skolemize(W4,sK14_skl(W2,W1)),skolemize(W4,sK15_skl(W2,W1))],[f102]) ).
fof(f115,plain,
isLocallyConfluent0(xR),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f116,plain,
! [X0,X1] :
( iLess0(X1,X0)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f119,plain,
isTerminating0(xR),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f120,plain,
aElement0(xa),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f121,plain,
aElement0(xb),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f122,plain,
aElement0(xc),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f123,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) )
| ~ iLess0(W0,xa)
| ( ~ 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(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f124,definition,
! [W0,W1] :
( sP0_prd(W1,W0)
<=> ( ~ 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 ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f125,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) )
| ~ iLess0(W0,xa)
| ( ~ 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 )
| sP0_prd(W1,W0)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(formula_renaming,[status(thm)],[f123,f124]) ).
fof(f126,plain,
! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W2,xR,sK16_skl(W2,W1,W0))
& ( ( sdtmndtplgtdt0(W2,xR,sK16_skl(W2,W1,W0))
& ( ( sdtmndtplgtdt0(sK18_skl(W2,W1,W0),xR,sK16_skl(W2,W1,W0))
& aReductOfIn0(sK18_skl(W2,W1,W0),W2,xR)
& aElement0(sK18_skl(W2,W1,W0)) )
| aReductOfIn0(sK16_skl(W2,W1,W0),W2,xR) ) )
| W2 = sK16_skl(W2,W1,W0) )
& sdtmndtasgtdt0(W1,xR,sK16_skl(W2,W1,W0))
& ( ( sdtmndtplgtdt0(W1,xR,sK16_skl(W2,W1,W0))
& ( ( sdtmndtplgtdt0(sK17_skl(W2,W1,W0),xR,sK16_skl(W2,W1,W0))
& aReductOfIn0(sK17_skl(W2,W1,W0),W1,xR)
& aElement0(sK17_skl(W2,W1,W0)) )
| aReductOfIn0(sK16_skl(W2,W1,W0),W1,xR) ) )
| W1 = sK16_skl(W2,W1,W0) )
& aElement0(sK16_skl(W2,W1,W0)) )
| ~ iLess0(W0,xa)
| ( ~ 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 )
| sP0_prd(W1,W0)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(W3,sK16_skl(W2,W1,W0)),skolemize(W4,sK17_skl(W2,W1,W0)),skolemize(W4,sK18_skl(W2,W1,W0))],[f125]) ).
fof(f173,plain,
! [X0,X1,X2] :
( aReductOfIn0(sK17_skl(X2,X1,X0),X1,xR)
| aReductOfIn0(sK16_skl(X2,X1,X0),X1,xR)
| X1 = sK16_skl(X2,X1,X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X2)
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f180,plain,
! [X0,X1,X2] :
( sdtmndtplgtdt0(X2,xR,sK16_skl(X2,X1,X0))
| X2 = sK16_skl(X2,X1,X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X2)
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f191,plain,
( sdtmndtasgtdt0(xu,xR,xb)
& ( ( sdtmndtplgtdt0(xu,xR,xb)
& ( ( sdtmndtplgtdt0(sK21_skl,xR,xb)
& aReductOfIn0(sK21_skl,xu,xR)
& aElement0(sK21_skl) )
| aReductOfIn0(xb,xu,xR) ) )
| xu = xb )
& aReductOfIn0(xu,xa,xR)
& aElement0(xu) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W0,sK21_skl)],[f20]) ).
fof(f192,plain,
aElement0(xu),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
aReductOfIn0(xu,xa,xR),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f198,plain,
sdtmndtasgtdt0(xu,xR,xb),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f199,plain,
( sdtmndtasgtdt0(xv,xR,xc)
& ( ( sdtmndtplgtdt0(xv,xR,xc)
& ( ( sdtmndtplgtdt0(sK22_skl,xR,xc)
& aReductOfIn0(sK22_skl,xv,xR)
& aElement0(sK22_skl) )
| aReductOfIn0(xc,xv,xR) ) )
| xv = xc )
& aReductOfIn0(xv,xa,xR)
& aElement0(xv) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(W0,sK22_skl)],[f21]) ).
fof(f200,plain,
aElement0(xv),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f207,plain,
( sdtmndtasgtdt0(xv,xR,xw)
& ( ( sdtmndtplgtdt0(xv,xR,xw)
& ( ( sdtmndtplgtdt0(sK24_skl,xR,xw)
& aReductOfIn0(sK24_skl,xv,xR)
& aElement0(sK24_skl) )
| aReductOfIn0(xw,xv,xR) ) )
| xv = xw )
& sdtmndtasgtdt0(xu,xR,xw)
& ( ( sdtmndtplgtdt0(xu,xR,xw)
& ( ( sdtmndtplgtdt0(sK23_skl,xR,xw)
& aReductOfIn0(sK23_skl,xu,xR)
& aElement0(sK23_skl) )
| aReductOfIn0(xw,xu,xR) ) )
| xu = xw )
& aElement0(xw) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(W0,sK23_skl),skolemize(W0,sK24_skl)],[f22]) ).
fof(f208,plain,
aElement0(xw),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f213,plain,
sdtmndtasgtdt0(xu,xR,xw),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f219,plain,
( aNormalFormOfIn0(xd,xw,xR)
& ! [W0] : ~ aReductOfIn0(W0,xd,xR)
& sdtmndtasgtdt0(xw,xR,xd)
& ( ( sdtmndtplgtdt0(xw,xR,xd)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xd)
& aReductOfIn0(W0,xw,xR)
& aElement0(W0) )
| aReductOfIn0(xd,xw,xR) ) )
| xw = xd )
& aElement0(xd) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f220,plain,
( aNormalFormOfIn0(xd,xw,xR)
& ! [W0] : ~ aReductOfIn0(W0,xd,xR)
& sdtmndtasgtdt0(xw,xR,xd)
& ( ( sdtmndtplgtdt0(xw,xR,xd)
& ( ( sdtmndtplgtdt0(sK25_skl,xR,xd)
& aReductOfIn0(sK25_skl,xw,xR)
& aElement0(sK25_skl) )
| aReductOfIn0(xd,xw,xR) ) )
| xw = xd )
& aElement0(xd) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(W0,sK25_skl)],[f219]) ).
fof(f221,plain,
aElement0(xd),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f226,plain,
sdtmndtasgtdt0(xw,xR,xd),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f227,plain,
! [X0] : ~ aReductOfIn0(X0,xd,xR),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f229,plain,
( ~ sdtmndtasgtdt0(xb,xR,xd)
& ~ sdtmndtplgtdt0(xb,xR,xd)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xd)
| ~ aReductOfIn0(W0,xb,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xd,xb,xR)
& xb != xd ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f230,plain,
xb != xd,
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f231,plain,
~ aReductOfIn0(xd,xb,xR),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f233,plain,
~ sdtmndtplgtdt0(xb,xR,xd),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f234,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f235,plain,
! [W0,W1] :
( ( 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
| sP0_prd(W1,W0) )
& ( ( ~ 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 )
| ~ sP0_prd(W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f124]) ).
fof(f236,plain,
( ! [W0,W1] :
( 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
| sP0_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ 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 )
| ~ sP0_prd(W1,W0) ) ),
inference(miniscoping,[status(thm)],[f235]) ).
fof(f237,plain,
( ! [W0,W1] :
( sdtmndtasgtdt0(W0,xR,W1)
| sdtmndtplgtdt0(W0,xR,W1)
| ( sdtmndtplgtdt0(sK26_skl(W1,W0),xR,W1)
& aReductOfIn0(sK26_skl(W1,W0),W0,xR)
& aElement0(sK26_skl(W1,W0)) )
| aReductOfIn0(W1,W0,xR)
| W0 = W1
| sP0_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ 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 )
| ~ sP0_prd(W1,W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(W3,sK26_skl(W1,W0))],[f236]) ).
fof(f238,plain,
! [X0,X1] :
( X1 != X0
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f239,plain,
! [X0,X1] :
( ~ aReductOfIn0(X0,X1,xR)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f242,plain,
! [X0,X1] :
( ~ sdtmndtasgtdt0(X1,xR,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f415,plain,
! [X0] : ~ sP0_prd(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f238]) ).
fof(f496,definition,
( sQ38_spl
<=> aElement0(xu) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( sQ38_spl
| ~ aElement0(xu) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
( sQ39_spl
<=> aRewritingSystem0(xR) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( sQ39_spl
| ~ aRewritingSystem0(xR) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,definition,
( sQ40_spl
<=> aElement0(xb) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ40_spl
| ~ aElement0(xb) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f531,definition,
( sQ42_spl
<=> aElement0(xa) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( sQ42_spl
| ~ aElement0(xa) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f549,definition,
( sQ46_spl
<=> aElement0(xw) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f551,plain,
( sQ46_spl
| ~ aElement0(xw) ),
inference(component_clause,[status(thm)],[f549]) ).
fof(f552,definition,
( sQ47_spl
<=> aElement0(xd) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( sQ47_spl
| ~ aElement0(xd) ),
inference(component_clause,[status(thm)],[f552]) ).
fof(f585,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f501,f100]) ).
fof(f586,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f585]) ).
fof(f589,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f120]) ).
fof(f590,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f591,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f121]) ).
fof(f592,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f591]) ).
fof(f602,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f554,f221]) ).
fof(f603,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f602]) ).
fof(f642,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f551,f208]) ).
fof(f643,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f642]) ).
fof(f702,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f498,f192]) ).
fof(f703,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f702]) ).
fof(f735,plain,
! [X0,X1] :
( sdtmndtplgtdt0(X1,xR,sK16_skl(X1,xd,X0))
| X1 = sK16_skl(X1,xd,X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f221,f180]) ).
fof(f993,definition,
( sQ91_spl
<=> isLocallyConfluent0(xR) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f995,plain,
( sQ91_spl
| ~ isLocallyConfluent0(xR) ),
inference(component_clause,[status(thm)],[f993]) ).
fof(f1071,definition,
( sQ98_spl
<=> sdtmndtasgtdt0(xu,xR,xd) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1072,plain,
( ~ sQ98_spl
| sdtmndtasgtdt0(xu,xR,xd) ),
inference(component_clause,[status(thm)],[f1071]) ).
fof(f1128,definition,
( sQ108_spl
<=> isTerminating0(xR) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1130,plain,
( sQ108_spl
| ~ isTerminating0(xR) ),
inference(component_clause,[status(thm)],[f1128]) ).
fof(f1143,plain,
( sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1130,f119]) ).
fof(f1144,plain,
sQ108_spl,
inference(contradiction_clause,[status(thm)],[f1143]) ).
fof(f1349,definition,
( sQ144_spl
<=> aReductOfIn0(sK11_skl(xd,xR,xd),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1350,plain,
( ~ sQ144_spl
| aReductOfIn0(sK11_skl(xd,xR,xd),xd,xR) ),
inference(component_clause,[status(thm)],[f1349]) ).
fof(f1356,definition,
( sQ146_spl
<=> aReductOfIn0(sK11_skl(xd,xR,xu),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1357,plain,
( ~ sQ146_spl
| aReductOfIn0(sK11_skl(xd,xR,xu),xd,xR) ),
inference(component_clause,[status(thm)],[f1356]) ).
fof(f1407,definition,
( sQ155_spl
<=> sP0_prd(xd,xu) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1410,definition,
( sQ156_spl
<=> iLess0(xu,xa) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1449,definition,
( sQ162_spl
<=> sP0_prd(xd,xd) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1450,plain,
( ~ sQ162_spl
| sP0_prd(xd,xd) ),
inference(component_clause,[status(thm)],[f1449]) ).
fof(f1504,definition,
( sQ173_spl
<=> xd = sK16_skl(xb,xd,xu) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1505,plain,
( ~ sQ173_spl
| xd = sK16_skl(xb,xd,xu) ),
inference(component_clause,[status(thm)],[f1504]) ).
fof(f1522,plain,
( ~ sQ162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1450,f415]) ).
fof(f1523,plain,
~ sQ162_spl,
inference(contradiction_clause,[status(thm)],[f1522]) ).
fof(f1527,plain,
( sdtmndtplgtdt0(xb,xR,sK16_skl(xb,xd,xu))
| xb = sK16_skl(xb,xd,xu)
| ~ iLess0(xu,xa)
| sP0_prd(xd,xu)
| ~ aElement0(xb)
| ~ aElement0(xu) ),
inference(resolution,[status(thm)],[f735,f198]) ).
fof(f1537,definition,
( sQ178_spl
<=> xb = sK16_skl(xb,xd,xu) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
( ~ sQ178_spl
| xb = sK16_skl(xb,xd,xu) ),
inference(component_clause,[status(thm)],[f1537]) ).
fof(f1540,definition,
( sQ179_spl
<=> sdtmndtplgtdt0(xb,xR,sK16_skl(xb,xd,xu)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1541,plain,
( ~ sQ179_spl
| sdtmndtplgtdt0(xb,xR,sK16_skl(xb,xd,xu)) ),
inference(component_clause,[status(thm)],[f1540]) ).
fof(f1543,plain,
( sQ179_spl
| sQ178_spl
| ~ sQ156_spl
| sQ155_spl
| ~ sQ40_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1527,f496,f502,f1407,f1410,f1537,f1540]) ).
fof(f1701,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f995,f115]) ).
fof(f1702,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f1701]) ).
fof(f1767,definition,
( sQ199_spl
<=> aElement0(xv) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1769,plain,
( sQ199_spl
| ~ aElement0(xv) ),
inference(component_clause,[status(thm)],[f1767]) ).
fof(f1770,definition,
( sQ200_spl
<=> aElement0(xc) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f1772,plain,
( sQ200_spl
| ~ aElement0(xc) ),
inference(component_clause,[status(thm)],[f1770]) ).
fof(f1813,plain,
( sQ200_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1772,f122]) ).
fof(f1814,plain,
sQ200_spl,
inference(contradiction_clause,[status(thm)],[f1813]) ).
fof(f1815,plain,
( sQ199_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1769,f200]) ).
fof(f1816,plain,
sQ199_spl,
inference(contradiction_clause,[status(thm)],[f1815]) ).
fof(f2000,plain,
( ~ sQ173_spl
| ~ sQ178_spl
| xd = xb ),
inference(forward_demodulation,[status(thm)],[f1538,f1505]) ).
fof(f2001,plain,
( ~ sQ173_spl
| ~ sQ178_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2000,f230]) ).
fof(f2002,plain,
( ~ sQ173_spl
| ~ sQ178_spl ),
inference(contradiction_clause,[status(thm)],[f2001]) ).
fof(f2013,plain,
( ~ sQ146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1357,f227]) ).
fof(f2014,plain,
~ sQ146_spl,
inference(contradiction_clause,[status(thm)],[f2013]) ).
fof(f2015,plain,
( ~ sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1350,f227]) ).
fof(f2016,plain,
~ sQ144_spl,
inference(contradiction_clause,[status(thm)],[f2015]) ).
fof(f2048,definition,
( sQ232_spl
<=> xb = xd ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f2049,plain,
( ~ sQ232_spl
| xb = xd ),
inference(component_clause,[status(thm)],[f2048]) ).
fof(f2051,definition,
( sQ233_spl
<=> aReductOfIn0(xd,xb,xR) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f2052,plain,
( ~ sQ233_spl
| aReductOfIn0(xd,xb,xR) ),
inference(component_clause,[status(thm)],[f2051]) ).
fof(f2054,definition,
( sQ234_spl
<=> sdtmndtplgtdt0(xb,xR,xd) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f2055,plain,
( ~ sQ234_spl
| sdtmndtplgtdt0(xb,xR,xd) ),
inference(component_clause,[status(thm)],[f2054]) ).
fof(f2057,definition,
( sQ235_spl
<=> sdtmndtasgtdt0(xb,xR,xd) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f2058,plain,
( ~ sQ235_spl
| sdtmndtasgtdt0(xb,xR,xd) ),
inference(component_clause,[status(thm)],[f2057]) ).
fof(f2562,definition,
( sQ321_spl
<=> sP0_prd(xu,xu) ),
introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition]) ).
fof(f2563,plain,
( ~ sQ321_spl
| sP0_prd(xu,xu) ),
inference(component_clause,[status(thm)],[f2562]) ).
fof(f2598,definition,
( sQ327_spl
<=> sP0_prd(xu,xa) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f2599,plain,
( ~ sQ327_spl
| sP0_prd(xu,xa) ),
inference(component_clause,[status(thm)],[f2598]) ).
fof(f2838,plain,
( ~ sQ321_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2563,f415]) ).
fof(f2839,plain,
~ sQ321_spl,
inference(contradiction_clause,[status(thm)],[f2838]) ).
fof(f2931,plain,
( ~ sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2058,f234]) ).
fof(f2932,plain,
~ sQ235_spl,
inference(contradiction_clause,[status(thm)],[f2931]) ).
fof(f2933,plain,
( ~ sQ234_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2055,f233]) ).
fof(f2934,plain,
~ sQ234_spl,
inference(contradiction_clause,[status(thm)],[f2933]) ).
fof(f2935,plain,
( ~ sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2052,f231]) ).
fof(f2936,plain,
~ sQ233_spl,
inference(contradiction_clause,[status(thm)],[f2935]) ).
fof(f2937,plain,
( ~ sQ232_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2049,f230]) ).
fof(f2938,plain,
~ sQ232_spl,
inference(contradiction_clause,[status(thm)],[f2937]) ).
fof(f3073,plain,
~ sP0_prd(xu,xa),
inference(resolution,[status(thm)],[f193,f239]) ).
fof(f3075,plain,
( iLess0(xu,xa)
| ~ aElement0(xu)
| ~ aElement0(xa) ),
inference(resolution,[status(thm)],[f193,f116]) ).
fof(f3115,plain,
( ~ sQ327_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3073,f2599]) ).
fof(f3116,plain,
~ sQ327_spl,
inference(contradiction_clause,[status(thm)],[f3115]) ).
fof(f3121,plain,
( sQ156_spl
| ~ sQ38_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3075,f531,f496,f1410]) ).
fof(f3658,plain,
~ sP0_prd(xd,xw),
inference(resolution,[status(thm)],[f226,f242]) ).
fof(f3663,plain,
! [X0] :
( sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ aElement0(xd)
| ~ aElement0(xw)
| ~ aRewritingSystem0(xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f226,f54]) ).
fof(f3688,definition,
( sQ422_spl
<=> sP0_prd(xd,xw) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f3689,plain,
( ~ sQ422_spl
| sP0_prd(xd,xw) ),
inference(component_clause,[status(thm)],[f3688]) ).
fof(f3711,definition,
( sQ428_spl
<=> aReductOfIn0(sK11_skl(xd,xR,xw),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f3712,plain,
( ~ sQ428_spl
| aReductOfIn0(sK11_skl(xd,xR,xw),xd,xR) ),
inference(component_clause,[status(thm)],[f3711]) ).
fof(f3727,definition,
! [X0] :
( sQ432_spl
<=> ( sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f3728,plain,
! [X0] :
( ~ sQ432_spl
| sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f3727]) ).
fof(f3730,plain,
( ~ sQ47_spl
| ~ sQ46_spl
| ~ sQ39_spl
| sQ432_spl ),
inference(split_clause,[status(thm)],[f3663,f3727,f499,f549,f552]) ).
fof(f3732,plain,
( ~ sQ422_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3689,f3658]) ).
fof(f3733,plain,
~ sQ422_spl,
inference(contradiction_clause,[status(thm)],[f3732]) ).
fof(f3734,plain,
( ~ sQ428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3712,f227]) ).
fof(f3735,plain,
~ sQ428_spl,
inference(contradiction_clause,[status(thm)],[f3734]) ).
fof(f3942,plain,
! [X0,X1] :
( aReductOfIn0(sK17_skl(X1,xd,X0),xd,xR)
| aReductOfIn0(sK16_skl(X1,xd,X0),xd,xR)
| xd = sK16_skl(X1,xd,X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f173,f221]) ).
fof(f3943,plain,
! [X0,X1] :
( aReductOfIn0(sK17_skl(X1,xd,X0),xd,xR)
| xd = sK16_skl(X1,xd,X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3942,f227]) ).
fof(f4906,plain,
! [X0,X1] :
( xd = sK16_skl(X1,xd,X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3943,f227]) ).
fof(f6416,definition,
( sQ614_spl
<=> aReductOfIn0(xd,xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f6417,plain,
( ~ sQ614_spl
| aReductOfIn0(xd,xd,xR) ),
inference(component_clause,[status(thm)],[f6416]) ).
fof(f6423,definition,
( sQ616_spl
<=> aReductOfIn0(sK0_skl(xd,xR,xd),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f6424,plain,
( ~ sQ616_spl
| aReductOfIn0(sK0_skl(xd,xR,xd),xd,xR) ),
inference(component_clause,[status(thm)],[f6423]) ).
fof(f6431,plain,
( ~ sQ614_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6417,f227]) ).
fof(f6432,plain,
~ sQ614_spl,
inference(contradiction_clause,[status(thm)],[f6431]) ).
fof(f6433,plain,
( ~ sQ616_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6424,f227]) ).
fof(f6434,plain,
~ sQ616_spl,
inference(contradiction_clause,[status(thm)],[f6433]) ).
fof(f7316,definition,
( sQ730_spl
<=> aReductOfIn0(xa,xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition]) ).
fof(f7317,plain,
( ~ sQ730_spl
| aReductOfIn0(xa,xd,xR) ),
inference(component_clause,[status(thm)],[f7316]) ).
fof(f7323,definition,
( sQ732_spl
<=> aReductOfIn0(sK0_skl(xa,xR,xd),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ732_spl])],[split_symbol_definition]) ).
fof(f7324,plain,
( ~ sQ732_spl
| aReductOfIn0(sK0_skl(xa,xR,xd),xd,xR) ),
inference(component_clause,[status(thm)],[f7323]) ).
fof(f7331,plain,
( ~ sQ730_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7317,f227]) ).
fof(f7332,plain,
~ sQ730_spl,
inference(contradiction_clause,[status(thm)],[f7331]) ).
fof(f7334,plain,
( ~ sQ732_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7324,f227]) ).
fof(f7335,plain,
~ sQ732_spl,
inference(contradiction_clause,[status(thm)],[f7334]) ).
fof(f7391,plain,
( xd = sK16_skl(xb,xd,xu)
| ~ iLess0(xu,xa)
| sP0_prd(xd,xu)
| ~ aElement0(xb)
| ~ aElement0(xu) ),
inference(resolution,[status(thm)],[f4906,f198]) ).
fof(f7396,plain,
( sQ173_spl
| ~ sQ156_spl
| sQ155_spl
| ~ sQ40_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f7391,f496,f502,f1407,f1410,f1504]) ).
fof(f7535,plain,
( ~ sQ98_spl
| ~ sP0_prd(xd,xu) ),
inference(resolution,[status(thm)],[f1072,f242]) ).
fof(f7542,definition,
( sQ756_spl
<=> aReductOfIn0(sK16_skl(xd,xd,xu),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ756_spl])],[split_symbol_definition]) ).
fof(f7543,plain,
( ~ sQ756_spl
| aReductOfIn0(sK16_skl(xd,xd,xu),xd,xR) ),
inference(component_clause,[status(thm)],[f7542]) ).
fof(f7549,definition,
( sQ758_spl
<=> aReductOfIn0(sK18_skl(xd,xd,xu),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ758_spl])],[split_symbol_definition]) ).
fof(f7550,plain,
( ~ sQ758_spl
| aReductOfIn0(sK18_skl(xd,xd,xu),xd,xR) ),
inference(component_clause,[status(thm)],[f7549]) ).
fof(f7567,plain,
( ~ sQ98_spl
| ~ sQ155_spl ),
inference(split_clause,[status(thm)],[f7535,f1407,f1071]) ).
fof(f7574,plain,
( ~ sQ756_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7543,f227]) ).
fof(f7575,plain,
~ sQ756_spl,
inference(contradiction_clause,[status(thm)],[f7574]) ).
fof(f7576,plain,
( ~ sQ758_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7550,f227]) ).
fof(f7577,plain,
~ sQ758_spl,
inference(contradiction_clause,[status(thm)],[f7576]) ).
fof(f7617,definition,
( sQ766_spl
<=> aReductOfIn0(sK18_skl(xd,xd,sK25_skl),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ766_spl])],[split_symbol_definition]) ).
fof(f7618,plain,
( ~ sQ766_spl
| aReductOfIn0(sK18_skl(xd,xd,sK25_skl),xd,xR) ),
inference(component_clause,[status(thm)],[f7617]) ).
fof(f7674,plain,
( ~ sQ766_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7618,f227]) ).
fof(f7675,plain,
~ sQ766_spl,
inference(contradiction_clause,[status(thm)],[f7674]) ).
fof(f8177,definition,
( sQ833_spl
<=> aReductOfIn0(sK18_skl(xd,xd,sK0_skl(xd,xR,xw)),xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ833_spl])],[split_symbol_definition]) ).
fof(f8178,plain,
( ~ sQ833_spl
| aReductOfIn0(sK18_skl(xd,xd,sK0_skl(xd,xR,xw)),xd,xR) ),
inference(component_clause,[status(thm)],[f8177]) ).
fof(f8234,plain,
( ~ sQ833_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8178,f227]) ).
fof(f8235,plain,
~ sQ833_spl,
inference(contradiction_clause,[status(thm)],[f8234]) ).
fof(f8318,plain,
( ~ sQ432_spl
| sdtmndtasgtdt0(xu,xR,xd)
| ~ aElement0(xu) ),
inference(resolution,[status(thm)],[f213,f3728]) ).
fof(f8339,plain,
( ~ sQ432_spl
| sQ98_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f8318,f496,f1071,f3727]) ).
fof(f8398,plain,
( ~ sQ179_spl
| ~ sQ173_spl
| sdtmndtplgtdt0(xb,xR,xd) ),
inference(forward_demodulation,[status(thm)],[f1505,f1541]) ).
fof(f8399,plain,
( ~ sQ179_spl
| ~ sQ173_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8398,f233]) ).
fof(f8400,plain,
( ~ sQ179_spl
| ~ sQ173_spl ),
inference(contradiction_clause,[status(thm)],[f8399]) ).
fof(f8401,plain,
$false,
inference(sat_refutation,[status(thm)],[f586,f590,f592,f603,f643,f703,f1144,f1523,f1543,f1702,f1814,f1816,f2002,f2014,f2016,f2839,f2932,f2934,f2936,f2938,f3116,f3121,f3730,f3733,f3735,f6432,f6434,f7332,f7335,f7396,f7567,f7575,f7577,f7675,f8235,f8339,f8400]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM019+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n005.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Mon Sep 21 14:14:48 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 68.56/9.08 % Refutation found
% 68.56/9.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 68.56/9.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 28.21/9.13 % Elapsed time: 8.752324 seconds
% 28.21/9.13 % CPU time: 69.085079 seconds
% 28.21/9.13 % Total memory used: 288.029 MB
% 28.21/9.13 % Net memory used: 263.190 MB
%------------------------------------------------------------------------------