%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM013+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 : n017.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:17 PM UTC 2026
% Result : Theorem 0.16s 0.48s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 94 ( 7 unt; 13 def)
% Number of atoms : 498 ( 19 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 691 ( 287 ~; 273 |; 102 &)
% ( 15 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 12 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 155 ( 128 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aReductOfIn0(W2,W0,W1)
=> aElement0(W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,definition,
! [W0,W1,W2] :
( ( aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( sdtmndtplgtdt0(W0,W1,W2)
<=> ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,definition,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aNormalFormOfIn0(W2,W0,W1)
<=> ( ~ ? [W3] : aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,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) ) )
& aRewritingSystem0(xR) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,conjecture,
! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ~ ? [W3] : aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) ) ) )
=> ? [W1] :
( aNormalFormOfIn0(W1,W0,xR)
| ( ~ ? [W2] : aReductOfIn0(W2,W1,xR)
& ( sdtmndtasgtdt0(W0,xR,W1)
| sdtmndtplgtdt0(W0,xR,W1)
| ? [W2] :
( sdtmndtplgtdt0(W2,xR,W1)
& aReductOfIn0(W2,W0,xR)
& aElement0(W2) )
| aReductOfIn0(W1,W0,xR)
| W0 = W1 )
& aElement0(W1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
~ ! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ~ ? [W3] : aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) ) ) )
=> ? [W1] :
( aNormalFormOfIn0(W1,W0,xR)
| ( ~ ? [W2] : aReductOfIn0(W2,W1,xR)
& ( sdtmndtasgtdt0(W0,xR,W1)
| sdtmndtplgtdt0(W0,xR,W1)
| ? [W2] :
( sdtmndtplgtdt0(W2,xR,W1)
& aReductOfIn0(W2,W0,xR)
& aElement0(W2) )
| aReductOfIn0(W1,W0,xR)
| W0 = W1 )
& aElement0(W1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f15]) ).
fof(f23,plain,
! [W0,W1] :
( ! [W2] :
( aElement0(W2)
| ~ aReductOfIn0(W2,W0,W1) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f24,plain,
! [X0,X1,X2] :
( aElement0(X2)
| ~ aReductOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f29,plain,
! [W0,W1,W2] :
( ( sdtmndtplgtdt0(W0,W1,W2)
<=> ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f30,plain,
! [W0,W1,W2] :
( ( ( ( ! [W3] :
( ~ sdtmndtplgtdt0(W3,W1,W2)
| ~ aReductOfIn0(W3,W0,W1)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,W1) )
| sdtmndtplgtdt0(W0,W1,W2) )
& ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1)
| ~ sdtmndtplgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [W0,W1,W2] :
( ( ( ( ! [W3] :
( ~ sdtmndtplgtdt0(W3,W1,W2)
| ~ aReductOfIn0(W3,W0,W1)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,W1) )
| sdtmndtplgtdt0(W0,W1,W2) )
& ( ( sdtmndtplgtdt0(sK0_skl(W2,W1,W0),W1,W2)
& aReductOfIn0(sK0_skl(W2,W1,W0),W0,W1)
& aElement0(sK0_skl(W2,W1,W0)) )
| aReductOfIn0(W2,W0,W1)
| ~ sdtmndtplgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W3,sK0_skl(W2,W1,W0))],[f30]) ).
fof(f36,plain,
! [X0,X1,X2,X3] :
( ~ sdtmndtplgtdt0(X3,X1,X2)
| ~ aReductOfIn0(X3,X0,X1)
| ~ aElement0(X3)
| sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f80,plain,
! [W0,W1] :
( ! [W2] :
( aNormalFormOfIn0(W2,W0,W1)
<=> ( ! [W3] : ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f81,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] : aReductOfIn0(W3,W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ( ( ! [W3] : ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] : aReductOfIn0(W3,W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ! [W2] :
( ( ! [W3] : ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(miniscoping,[status(thm)],[f81]) ).
fof(f83,plain,
! [W0,W1] :
( ( ! [W2] :
( aReductOfIn0(sK11_skl(W2,W1,W0),W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ! [W2] :
( ( ! [W3] : ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(W3,sK11_skl(W2,W1,W0))],[f82]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( ~ aReductOfIn0(X3,X2,X1)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f88,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) )
& aRewritingSystem0(xR) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f89,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [X0,X1] :
( iLess0(X1,X0)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f94,plain,
? [W0] :
( ! [W1] :
( ~ aNormalFormOfIn0(W1,W0,xR)
& ( ? [W2] : aReductOfIn0(W2,W1,xR)
| ( ~ sdtmndtasgtdt0(W0,xR,W1)
& ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR)
& W0 != W1 )
| ~ aElement0(W1) ) )
& ! [W1] :
( ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ! [W3] : ~ aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) )
| ~ iLess0(W1,W0)
| ~ aElement0(W1) )
& aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f95,plain,
? [W0] :
( ! [W1] : ~ aNormalFormOfIn0(W1,W0,xR)
& ! [W1] :
( ? [W2] : aReductOfIn0(W2,W1,xR)
| ( ~ sdtmndtasgtdt0(W0,xR,W1)
& ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR)
& W0 != W1 )
| ~ aElement0(W1) )
& ! [W1] :
( ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ! [W3] : ~ aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) )
| ~ iLess0(W1,W0)
| ~ aElement0(W1) )
& aElement0(W0) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f96,plain,
( ! [W1] : ~ aNormalFormOfIn0(W1,sK12_skl,xR)
& ! [W1] :
( aReductOfIn0(sK15_skl(W1),W1,xR)
| ( ~ sdtmndtasgtdt0(sK12_skl,xR,W1)
& ~ sdtmndtplgtdt0(sK12_skl,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,sK12_skl,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,sK12_skl,xR)
& sK12_skl != W1 )
| ~ aElement0(W1) )
& ! [W1] :
( ( aNormalFormOfIn0(sK13_skl(W1),W1,xR)
& ! [W3] : ~ aReductOfIn0(W3,sK13_skl(W1),xR)
& sdtmndtasgtdt0(W1,xR,sK13_skl(W1))
& ( ( sdtmndtplgtdt0(W1,xR,sK13_skl(W1))
& ( ( sdtmndtplgtdt0(sK14_skl(W1),xR,sK13_skl(W1))
& aReductOfIn0(sK14_skl(W1),W1,xR)
& aElement0(sK14_skl(W1)) )
| aReductOfIn0(sK13_skl(W1),W1,xR) ) )
| W1 = sK13_skl(W1) )
& aElement0(sK13_skl(W1)) )
| ~ iLess0(W1,sK12_skl)
| ~ aElement0(W1) )
& aElement0(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(W0,sK12_skl),skolemize(W2,sK13_skl(W1)),skolemize(W3,sK14_skl(W1)),skolemize(W2,sK15_skl(W1))],[f95]) ).
fof(f97,plain,
aElement0(sK12_skl),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f98,plain,
! [X0] :
( aElement0(sK13_skl(X0))
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f102,plain,
! [X0] :
( sdtmndtplgtdt0(X0,xR,sK13_skl(X0))
| X0 = sK13_skl(X0)
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f104,plain,
! [X0,X1] :
( ~ aReductOfIn0(X1,sK13_skl(X0),xR)
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f105,plain,
! [X0] :
( aNormalFormOfIn0(sK13_skl(X0),X0,xR)
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f106,plain,
! [X0] :
( aReductOfIn0(sK15_skl(X0),X0,xR)
| sK12_skl != X0
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f107,plain,
! [X0] :
( aReductOfIn0(sK15_skl(X0),X0,xR)
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f109,plain,
! [X0] :
( aReductOfIn0(sK15_skl(X0),X0,xR)
| ~ sdtmndtplgtdt0(sK12_skl,xR,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f114,plain,
( aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR)
| ~ aElement0(sK12_skl) ),
inference(destructive_equality_resolution,[status(thm)],[f106]) ).
fof(f115,plain,
aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR),
inference(forward_subsumption_resolution,[status(thm)],[f114,f97]) ).
fof(f117,plain,
! [X0,X1,X2,X3] :
( ~ sdtmndtplgtdt0(X3,X1,X2)
| ~ aReductOfIn0(X3,X0,X1)
| sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f36,f24]) ).
fof(f122,definition,
( sQ1_spl
<=> aRewritingSystem0(xR) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f124,plain,
( sQ1_spl
| ~ aRewritingSystem0(xR) ),
inference(component_clause,[status(thm)],[f122]) ).
fof(f128,plain,
! [X0] :
( ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| ~ aElement0(sK12_skl)
| aNormalFormOfIn0(sK13_skl(X0),X0,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f105,f90]) ).
fof(f132,definition,
( sQ3_spl
<=> aElement0(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f134,plain,
( sQ3_spl
| ~ aElement0(sK12_skl) ),
inference(component_clause,[status(thm)],[f132]) ).
fof(f136,definition,
! [X0] :
( sQ4_spl
<=> ( ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| aNormalFormOfIn0(sK13_skl(X0),X0,xR)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f137,plain,
! [X0] :
( ~ sQ4_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| aNormalFormOfIn0(sK13_skl(X0),X0,xR)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f139,plain,
( ~ sQ3_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f128,f136,f132]) ).
fof(f140,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f134,f97]) ).
fof(f141,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f140]) ).
fof(f143,plain,
! [X0] :
( ~ sQ4_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| aNormalFormOfIn0(sK13_skl(X0),X0,xR)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f137]) ).
fof(f159,plain,
! [X0] :
( ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(sK12_skl,xR,sK13_skl(X0))
| ~ aElement0(sK13_skl(X0)) ),
inference(resolution,[status(thm)],[f109,f104]) ).
fof(f160,plain,
! [X0] :
( ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(sK12_skl,xR,sK13_skl(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f159,f98]) ).
fof(f161,plain,
! [X0,X1] :
( ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(sK13_skl(X0))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl)
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f160,f117]) ).
fof(f163,definition,
! [X0,X1] :
( sQ8_spl
<=> ( ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(sK13_skl(X0))
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f164,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(sK13_skl(X0))
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f163]) ).
fof(f166,plain,
( ~ sQ1_spl
| ~ sQ3_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f161,f163,f132,f122]) ).
fof(f171,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f124,f89]) ).
fof(f172,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f164,f98]) ).
fof(f229,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ aReductOfIn0(X1,sK13_skl(X0),xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(X0)
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f143,f86]) ).
fof(f231,definition,
! [X0,X1] :
( sQ19_spl
<=> ( ~ aReductOfIn0(X1,sK13_skl(X0),xR)
| ~ aElement0(X0)
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f232,plain,
! [X0,X1] :
( ~ sQ19_spl
| ~ aReductOfIn0(X1,sK13_skl(X0),xR)
| ~ aElement0(X0)
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f234,plain,
( ~ sQ4_spl
| ~ sQ1_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f229,f231,f122,f136]) ).
fof(f235,plain,
! [X0,X1] :
( ~ sQ19_spl
| ~ aReductOfIn0(X1,sK13_skl(X0),xR)
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f232]) ).
fof(f240,plain,
! [X0] :
( ~ sQ19_spl
| ~ aReductOfIn0(sK13_skl(X0),sK12_skl,xR)
| ~ aElement0(sK13_skl(X0))
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f235,f107]) ).
fof(f255,plain,
! [X0] :
( ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| ~ aElement0(sK12_skl)
| sdtmndtplgtdt0(X0,xR,sK13_skl(X0))
| X0 = sK13_skl(X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f102,f90]) ).
fof(f260,definition,
! [X0] :
( sQ23_spl
<=> ( ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| sdtmndtplgtdt0(X0,xR,sK13_skl(X0))
| X0 = sK13_skl(X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f261,plain,
! [X0] :
( ~ sQ23_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| sdtmndtplgtdt0(X0,xR,sK13_skl(X0))
| X0 = sK13_skl(X0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f263,plain,
( ~ sQ3_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f255,f260,f132]) ).
fof(f265,plain,
! [X0] :
( ~ sQ23_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| sdtmndtplgtdt0(X0,xR,sK13_skl(X0))
| X0 = sK13_skl(X0)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f261]) ).
fof(f480,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| ~ aElement0(sK12_skl)
| ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f173,f90]) ).
fof(f489,definition,
! [X0,X1] :
( sQ64_spl
<=> ( ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f490,plain,
! [X0,X1] :
( ~ sQ64_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f492,plain,
( ~ sQ8_spl
| ~ sQ3_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f480,f489,f132,f163]) ).
fof(f495,plain,
! [X0,X1] :
( ~ sQ64_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ sdtmndtplgtdt0(X1,xR,sK13_skl(X0))
| ~ aReductOfIn0(X1,sK12_skl,xR)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f490]) ).
fof(f770,plain,
! [X0] :
( ~ sQ64_spl
| ~ aReductOfIn0(X0,sK12_skl,xR)
| ~ sdtmndtplgtdt0(sK15_skl(sK12_skl),xR,sK13_skl(X0))
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f495,f115]) ).
fof(f791,plain,
( ~ sQ23_spl
| ~ sQ64_spl
| ~ aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR)
| sK15_skl(sK12_skl) = sK13_skl(sK15_skl(sK12_skl))
| ~ aElement0(sK15_skl(sK12_skl))
| ~ aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR)
| ~ aElement0(sK15_skl(sK12_skl)) ),
inference(resolution,[status(thm)],[f770,f265]) ).
fof(f795,definition,
( sQ111_spl
<=> aElement0(sK15_skl(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f796,plain,
( ~ sQ111_spl
| aElement0(sK15_skl(sK12_skl)) ),
inference(component_clause,[status(thm)],[f795]) ).
fof(f797,plain,
( sQ111_spl
| ~ aElement0(sK15_skl(sK12_skl)) ),
inference(component_clause,[status(thm)],[f795]) ).
fof(f798,definition,
( sQ112_spl
<=> aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( sQ112_spl
| ~ aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR) ),
inference(component_clause,[status(thm)],[f798]) ).
fof(f807,definition,
( sQ115_spl
<=> sK15_skl(sK12_skl) = sK13_skl(sK15_skl(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f808,plain,
( ~ sQ115_spl
| sK15_skl(sK12_skl) = sK13_skl(sK15_skl(sK12_skl)) ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f811,plain,
( ~ sQ23_spl
| ~ sQ64_spl
| sQ115_spl
| ~ sQ112_spl
| ~ sQ111_spl ),
inference(split_clause,[status(thm)],[f791,f795,f798,f807,f489,f260]) ).
fof(f825,plain,
! [X0,X1] :
( sQ111_spl
| ~ aReductOfIn0(sK15_skl(sK12_skl),X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f797,f24]) ).
fof(f826,plain,
! [X0] :
( sQ111_spl
| ~ aReductOfIn0(sK15_skl(sK12_skl),X0,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f825,f89]) ).
fof(f827,plain,
( sQ111_spl
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f826,f115]) ).
fof(f832,plain,
( sQ111_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f827,f132,f795]) ).
fof(f837,plain,
( sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f800,f115]) ).
fof(f838,plain,
sQ112_spl,
inference(contradiction_clause,[status(thm)],[f837]) ).
fof(f844,plain,
( ~ sQ115_spl
| ~ sQ19_spl
| ~ aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR)
| ~ aElement0(sK13_skl(sK15_skl(sK12_skl)))
| ~ aReductOfIn0(sK15_skl(sK12_skl),sK12_skl,xR)
| ~ aElement0(sK15_skl(sK12_skl)) ),
inference(paramodulation,[status(thm)],[f808,f240]) ).
fof(f883,definition,
( sQ125_spl
<=> aElement0(sK13_skl(sK15_skl(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( sQ125_spl
| ~ aElement0(sK13_skl(sK15_skl(sK12_skl))) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f886,plain,
( ~ sQ115_spl
| ~ sQ19_spl
| ~ sQ125_spl
| ~ sQ112_spl
| ~ sQ111_spl ),
inference(split_clause,[status(thm)],[f844,f795,f798,f883,f231,f807]) ).
fof(f929,plain,
( sQ125_spl
| ~ sQ115_spl
| ~ aElement0(sK15_skl(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f808,f885]) ).
fof(f930,plain,
( sQ125_spl
| ~ sQ115_spl
| ~ sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f929,f796]) ).
fof(f931,plain,
( sQ125_spl
| ~ sQ115_spl
| ~ sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f930]) ).
fof(f932,plain,
$false,
inference(sat_refutation,[status(thm)],[f139,f141,f166,f172,f234,f263,f492,f811,f832,f838,f886,f931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : COM013+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n017.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 14:09:28 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.48 % Refutation found
% 0.16/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/0.53 % Elapsed time: 0.088282 seconds
% 0.21/0.53 % CPU time: 0.337027 seconds
% 0.21/0.53 % Total memory used: 85.851 MB
% 0.21/0.53 % Net memory used: 85.531 MB
%------------------------------------------------------------------------------