%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM020+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 : 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 : Thu Sep 24 12:10:19 PM UTC 2026
% Result : Theorem 24.57s 3.62s
% Output : CNFRefutation 16.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 13
% Syntax : Number of formulae : 126 ( 19 unt; 2 def)
% Number of atoms : 888 ( 80 equ)
% Maximal formula atoms : 33 ( 7 avg)
% Number of connectives : 1168 ( 406 ~; 471 |; 280 &)
% ( 2 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 14 con; 0-3 aty)
% Number of variables : 211 ( 172 !; 39 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [W0,W1,W2,W3] :
( ( aElement0(W3)
& aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( ( sdtmndtplgtdt0(W2,W1,W3)
& sdtmndtplgtdt0(W0,W1,W2) )
=> sdtmndtplgtdt0(W0,W1,W3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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(f19,hypothesis,
( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) )
& sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) ),
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(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,
? [W0] :
( ( sdtmndtasgtdt0(xd,xR,W0)
| sdtmndtplgtdt0(xd,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xd,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xd,xR)
| xd = W0 )
& ( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xb,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xb,xR)
| xb = W0 )
& aElement0(W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
~ ? [W0] :
( ( sdtmndtasgtdt0(xd,xR,W0)
| sdtmndtplgtdt0(xd,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xd,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xd,xR)
| xd = W0 )
& ( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xb,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xb,xR)
| xb = W0 )
& aElement0(W0) ),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f46,plain,
! [W0,W1,W2,W3] :
( sdtmndtplgtdt0(W0,W1,W3)
| ~ sdtmndtplgtdt0(W2,W1,W3)
| ~ sdtmndtplgtdt0(W0,W1,W2)
| ~ aElement0(W3)
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f47,plain,
! [X0,X1,X2,X3] :
( sdtmndtplgtdt0(X0,X1,X3)
| ~ sdtmndtplgtdt0(X2,X1,X3)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X3)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
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(f116,plain,
! [X0,X1] :
( iLess0(X1,X0)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f118,plain,
! [X0,X1] :
( iLess0(X1,X0)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
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(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(f127,plain,
! [X0,X1,X2] :
( aElement0(sK16_skl(X2,X1,X0))
| ~ iLess0(X0,xa)
| X0 != X2
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f132,plain,
! [X0,X1,X2] :
( sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1,X0))
| ~ iLess0(X0,xa)
| X0 != X2
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f137,plain,
! [X0,X1,X2] :
( sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1,X0))
| ~ iLess0(X0,xa)
| X0 != X2
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f160,plain,
! [X0,X1,X2] :
( aElement0(sK16_skl(X2,X1,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X2)
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f165,plain,
! [X0,X1,X2] :
( sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X2)
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f170,plain,
! [X0,X1,X2] :
( sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X2)
| sP0_prd(X1,X0)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f182,plain,
( sdtmndtplgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(sK20_skl,xR,xc)
& aReductOfIn0(sK20_skl,xa,xR)
& aElement0(sK20_skl) )
| aReductOfIn0(xc,xa,xR) )
& sdtmndtplgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(sK19_skl,xR,xb)
& aReductOfIn0(sK19_skl,xa,xR)
& aElement0(sK19_skl) )
| aReductOfIn0(xb,xa,xR) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W0,sK19_skl),skolemize(W0,sK20_skl)],[f19]) ).
fof(f186,plain,
sdtmndtplgtdt0(xa,xR,xb),
inference(cnf_transformation,[status(thm)],[f182]) ).
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(f197,plain,
( sdtmndtplgtdt0(xu,xR,xb)
| xu = xb ),
inference(cnf_transformation,[status(thm)],[f191]) ).
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(f212,plain,
( sdtmndtplgtdt0(xu,xR,xw)
| xu = 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(f225,plain,
( sdtmndtplgtdt0(xw,xR,xd)
| xw = xd ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f226,plain,
sdtmndtasgtdt0(xw,xR,xd),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f229,plain,
! [W0] :
( ( ~ sdtmndtasgtdt0(xd,xR,W0)
& ~ sdtmndtplgtdt0(xd,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xd,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xd,xR)
& xd != W0 )
| ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f230,definition,
! [W0] :
( sP1_prd(W0)
<=> ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f231,plain,
! [W0] :
( ( ~ sdtmndtasgtdt0(xd,xR,W0)
& ~ sdtmndtplgtdt0(xd,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xd,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xd,xR)
& xd != W0 )
| sP1_prd(W0)
| ~ aElement0(W0) ),
inference(formula_renaming,[status(thm)],[f229,f230]) ).
fof(f236,plain,
! [X0] :
( ~ sdtmndtasgtdt0(xd,xR,X0)
| sP1_prd(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f237,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(f238,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)],[f237]) ).
fof(f239,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))],[f238]) ).
fof(f243,plain,
! [X0,X1] :
( ~ sdtmndtplgtdt0(X1,xR,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f244,plain,
! [X0,X1] :
( ~ sdtmndtasgtdt0(X1,xR,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f248,plain,
! [W0] :
( ( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xb,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xb,xR)
| xb = W0
| sP1_prd(W0) )
& ( ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 )
| ~ sP1_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f230]) ).
fof(f249,plain,
( ! [W0] :
( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xb,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xb,xR)
| xb = W0
| sP1_prd(W0) )
& ! [W0] :
( ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 )
| ~ sP1_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f248]) ).
fof(f250,plain,
( ! [W0] :
( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ( sdtmndtplgtdt0(sK27_skl(W0),xR,W0)
& aReductOfIn0(sK27_skl(W0),xb,xR)
& aElement0(sK27_skl(W0)) )
| aReductOfIn0(W0,xb,xR)
| xb = W0
| sP1_prd(W0) )
& ! [W0] :
( ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 )
| ~ sP1_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(W1,sK27_skl(W0))],[f249]) ).
fof(f255,plain,
! [X0] :
( ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ sP1_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f261,plain,
! [X2,X1] :
( aElement0(sK16_skl(X2,X1,X2))
| ~ iLess0(X2,xa)
| sP0_prd(X1,X2)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f127]) ).
fof(f262,plain,
! [X0,X1] :
( aElement0(sK16_skl(X0,X1,X0))
| ~ iLess0(X0,xa)
| sP0_prd(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f261]) ).
fof(f271,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1,X2))
| ~ iLess0(X2,xa)
| sP0_prd(X1,X2)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f132]) ).
fof(f272,plain,
! [X0,X1] :
( sdtmndtasgtdt0(X1,xR,sK16_skl(X0,X1,X0))
| ~ iLess0(X0,xa)
| sP0_prd(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f271]) ).
fof(f281,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1,X2))
| ~ iLess0(X2,xa)
| sP0_prd(X1,X2)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f137]) ).
fof(f282,plain,
! [X0,X1] :
( sdtmndtasgtdt0(X0,xR,sK16_skl(X0,X1,X0))
| ~ iLess0(X0,xa)
| sP0_prd(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f281]) ).
fof(f306,plain,
! [X0,X1,X2] :
( sdtmndtplgtdt0(X0,xR,X2)
| ~ sdtmndtplgtdt0(X1,xR,X2)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f47,f100]) ).
fof(f311,plain,
! [X0,X1,X2] :
( sdtmndtasgtdt0(X0,xR,X2)
| ~ sdtmndtasgtdt0(X1,xR,X2)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f54,f100]) ).
fof(f333,plain,
( iLess0(xu,xa)
| ~ aElement0(xu)
| ~ aElement0(xa) ),
inference(resolution,[status(thm)],[f116,f193]) ).
fof(f338,plain,
( iLess0(xu,xa)
| ~ aElement0(xu) ),
inference(forward_subsumption_resolution,[status(thm)],[f333,f120]) ).
fof(f341,plain,
iLess0(xu,xa),
inference(forward_subsumption_resolution,[status(thm)],[f338,f192]) ).
fof(f362,plain,
( iLess0(xb,xa)
| ~ aElement0(xb)
| ~ aElement0(xa) ),
inference(resolution,[status(thm)],[f118,f186]) ).
fof(f373,plain,
( iLess0(xb,xa)
| ~ aElement0(xb) ),
inference(forward_subsumption_resolution,[status(thm)],[f362,f120]) ).
fof(f394,plain,
iLess0(xb,xa),
inference(forward_subsumption_resolution,[status(thm)],[f373,f121]) ).
fof(f825,plain,
! [X0] :
( sP1_prd(sK16_skl(X0,xd,X0))
| ~ aElement0(sK16_skl(X0,xd,X0))
| ~ iLess0(X0,xa)
| sP0_prd(xd,X0)
| ~ aElement0(xd)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f272,f236]) ).
fof(f828,plain,
! [X0] :
( sP1_prd(sK16_skl(X0,xd,X0))
| ~ aElement0(sK16_skl(X0,xd,X0))
| ~ iLess0(X0,xa)
| sP0_prd(xd,X0)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f221]) ).
fof(f866,plain,
! [X0] :
( ~ iLess0(X0,xa)
| sP0_prd(xd,X0)
| ~ aElement0(xd)
| ~ aElement0(X0)
| sP1_prd(sK16_skl(X0,xd,X0))
| ~ iLess0(X0,xa)
| sP0_prd(xd,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f828,f262]) ).
fof(f867,plain,
! [X0] :
( ~ aElement0(xd)
| sP1_prd(sK16_skl(X0,xd,X0))
| ~ iLess0(X0,xa)
| sP0_prd(xd,X0)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f866]) ).
fof(f868,plain,
! [X0] :
( sP1_prd(sK16_skl(X0,xd,X0))
| ~ iLess0(X0,xa)
| sP0_prd(xd,X0)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f867,f221]) ).
fof(f950,plain,
! [X0] :
( ~ sP1_prd(sK16_skl(xb,X0,xb))
| ~ iLess0(xb,xa)
| sP0_prd(X0,xb)
| ~ aElement0(X0)
| ~ aElement0(xb) ),
inference(resolution,[status(thm)],[f282,f255]) ).
fof(f953,plain,
! [X0] :
( ~ sP1_prd(sK16_skl(xb,X0,xb))
| ~ iLess0(xb,xa)
| sP0_prd(X0,xb)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f950,f121]) ).
fof(f956,plain,
! [X0] :
( ~ sP1_prd(sK16_skl(xb,X0,xb))
| sP0_prd(X0,xb)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f953,f394]) ).
fof(f957,plain,
( ~ iLess0(xb,xa)
| sP0_prd(xd,xb)
| ~ aElement0(xb)
| sP0_prd(xd,xb)
| ~ aElement0(xd) ),
inference(resolution,[status(thm)],[f956,f868]) ).
fof(f958,plain,
( ~ iLess0(xb,xa)
| ~ aElement0(xb)
| sP0_prd(xd,xb)
| ~ aElement0(xd) ),
inference(duplicate_literals_removal,[status(thm)],[f957]) ).
fof(f959,plain,
( ~ iLess0(xb,xa)
| ~ aElement0(xb)
| sP0_prd(xd,xb) ),
inference(forward_subsumption_resolution,[status(thm)],[f958,f221]) ).
fof(f960,plain,
( ~ iLess0(xb,xa)
| sP0_prd(xd,xb) ),
inference(forward_subsumption_resolution,[status(thm)],[f959,f121]) ).
fof(f961,plain,
sP0_prd(xd,xb),
inference(resolution,[status(thm)],[f960,f394]) ).
fof(f967,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(resolution,[status(thm)],[f961,f244]) ).
fof(f1705,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xd)
| ~ aElement0(X0)
| ~ aElement0(xb) ),
inference(resolution,[status(thm)],[f311,f967]) ).
fof(f1713,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xd)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1705,f121]) ).
fof(f1716,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1713,f221]) ).
fof(f1719,plain,
( ~ sdtmndtasgtdt0(xb,xR,xw)
| ~ aElement0(xw) ),
inference(resolution,[status(thm)],[f1716,f226]) ).
fof(f1723,plain,
~ sdtmndtasgtdt0(xb,xR,xw),
inference(forward_subsumption_resolution,[status(thm)],[f1719,f208]) ).
fof(f2809,plain,
! [X0,X1] :
( sP1_prd(sK16_skl(X1,xd,X0))
| ~ aElement0(sK16_skl(X1,xd,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(xd)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f165,f236]) ).
fof(f2815,plain,
! [X0,X1] :
( sP1_prd(sK16_skl(X1,xd,X0))
| ~ aElement0(sK16_skl(X1,xd,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2809,f221]) ).
fof(f2864,plain,
! [X0,X1] :
( ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(xd)
| ~ aElement0(X0)
| sP1_prd(sK16_skl(X1,xd,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f2815,f160]) ).
fof(f2868,plain,
! [X0,X1] :
( ~ aElement0(xd)
| sP1_prd(sK16_skl(X1,xd,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2864]) ).
fof(f2869,plain,
! [X0,X1] :
( sP1_prd(sK16_skl(X1,xd,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| sP0_prd(xd,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2868,f221]) ).
fof(f3260,plain,
! [X0,X1] :
( ~ sP1_prd(sK16_skl(xb,X1,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,xb)
| sP0_prd(X1,X0)
| ~ aElement0(xb)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f170,f255]) ).
fof(f3266,plain,
! [X0,X1] :
( ~ sP1_prd(sK16_skl(xb,X1,X0))
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,xb)
| sP0_prd(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3260,f121]) ).
fof(f4708,plain,
! [X0] :
( sP1_prd(sK16_skl(X0,xd,xu))
| ~ sdtmndtplgtdt0(xu,xR,X0)
| sP0_prd(xd,xu)
| ~ aElement0(X0)
| ~ aElement0(xu) ),
inference(resolution,[status(thm)],[f2869,f341]) ).
fof(f4715,plain,
! [X0] :
( sP1_prd(sK16_skl(X0,xd,xu))
| ~ sdtmndtplgtdt0(xu,xR,X0)
| sP0_prd(xd,xu)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4708,f192]) ).
fof(f4776,plain,
( ~ iLess0(xu,xa)
| ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu)
| ~ aElement0(xd)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu)
| ~ aElement0(xb) ),
inference(resolution,[status(thm)],[f4715,f3266]) ).
fof(f4786,plain,
( ~ iLess0(xu,xa)
| ~ aElement0(xd)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu)
| ~ aElement0(xb) ),
inference(duplicate_literals_removal,[status(thm)],[f4776]) ).
fof(f4787,plain,
( ~ iLess0(xu,xa)
| ~ aElement0(xd)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu) ),
inference(forward_subsumption_resolution,[status(thm)],[f4786,f121]) ).
fof(f5670,plain,
( ~ iLess0(xu,xa)
| ~ aElement0(xd)
| ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu) ),
inference(forward_subsumption_resolution,[status(thm)],[f4787,f192]) ).
fof(f5671,plain,
( ~ iLess0(xu,xa)
| ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu) ),
inference(resolution,[status(thm)],[f5670,f221]) ).
fof(f5672,plain,
( ~ sdtmndtplgtdt0(xu,xR,xb)
| sP0_prd(xd,xu) ),
inference(forward_subsumption_resolution,[status(thm)],[f5671,f341]) ).
fof(f5673,plain,
( xu = xb
| sP0_prd(xd,xu) ),
inference(resolution,[status(thm)],[f5672,f197]) ).
fof(f5681,plain,
( ~ sdtmndtplgtdt0(xu,xR,xd)
| xu = xb ),
inference(resolution,[status(thm)],[f5673,f243]) ).
fof(f5683,plain,
( ~ sdtmndtasgtdt0(xu,xR,xd)
| xu = xb ),
inference(resolution,[status(thm)],[f5673,f244]) ).
fof(f5684,plain,
! [X0] :
( ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd)
| ~ aElement0(X0)
| ~ aElement0(xu)
| xu = xb ),
inference(resolution,[status(thm)],[f5681,f306]) ).
fof(f5687,plain,
! [X0] :
( ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd)
| ~ aElement0(X0)
| xu = xb ),
inference(forward_subsumption_resolution,[status(thm)],[f5684,f192]) ).
fof(f5804,plain,
! [X0] :
( ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(X0)
| xu = xb ),
inference(forward_subsumption_resolution,[status(thm)],[f5687,f221]) ).
fof(f5811,plain,
( xw = xd
| ~ sdtmndtplgtdt0(xu,xR,xw)
| ~ aElement0(xw)
| xu = xb ),
inference(resolution,[status(thm)],[f5804,f225]) ).
fof(f5818,plain,
( xw = xd
| ~ sdtmndtplgtdt0(xu,xR,xw)
| xu = xb ),
inference(forward_subsumption_resolution,[status(thm)],[f5811,f208]) ).
fof(f5824,plain,
( xu = xw
| xw = xd
| xu = xb ),
inference(resolution,[status(thm)],[f5818,f212]) ).
fof(f5834,plain,
( xu = xw
| xu = xb
| ~ sdtmndtasgtdt0(xu,xR,xw)
| xu = xb ),
inference(paramodulation,[status(thm)],[f5824,f5683]) ).
fof(f5919,plain,
( xu = xw
| ~ sdtmndtasgtdt0(xu,xR,xw)
| xu = xb ),
inference(duplicate_literals_removal,[status(thm)],[f5834]) ).
fof(f5920,plain,
( xu = xw
| xu = xb ),
inference(forward_subsumption_resolution,[status(thm)],[f5919,f213]) ).
fof(f5995,plain,
( xu = xb
| sdtmndtasgtdt0(xu,xR,xd) ),
inference(paramodulation,[status(thm)],[f5920,f226]) ).
fof(f6006,plain,
xu = xb,
inference(forward_subsumption_resolution,[status(thm)],[f5995,f5683]) ).
fof(f6091,plain,
sdtmndtasgtdt0(xb,xR,xw),
inference(backward_demodulation,[status(thm)],[f6006,f213]) ).
fof(f6154,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6091,f1723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM020+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n003.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 : Mon Sep 21 14:16:16 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 24.57/3.62 % Refutation found
% 24.57/3.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.57/3.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.79/3.67 % Elapsed time: 3.276914 seconds
% 16.79/3.67 % CPU time: 25.663076 seconds
% 16.79/3.67 % Total memory used: 215.804 MB
% 16.79/3.67 % Net memory used: 199.950 MB
%------------------------------------------------------------------------------