%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM013+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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.19s 0.61s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 25
% Syntax : Number of formulae : 114 ( 11 unt; 21 def)
% Number of atoms : 452 ( 5 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 583 ( 245 ~; 244 |; 51 &)
% ( 25 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 18 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 140 ( 126 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aReductOfIn0(W2,W0,W1)
=> aElement0(W2) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,definition,
! [W0,W1,W2] :
( ( aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( sdtmndtasgtdt0(W0,W1,W2)
<=> ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2 ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,definition,
! [W0] :
( aRewritingSystem0(W0)
=> ( isTerminating0(W0)
<=> ! [W1,W2] :
( ( aElement0(W2)
& aElement0(W1) )
=> ( sdtmndtplgtdt0(W1,W0,W2)
=> iLess0(W2,W1) ) ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
( isTerminating0(xR)
& aRewritingSystem0(xR) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,conjecture,
! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] : aNormalFormOfIn0(W2,W1,xR) ) )
=> ? [W1] : aNormalFormOfIn0(W1,W0,xR) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
~ ! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] : aNormalFormOfIn0(W2,W1,xR) ) )
=> ? [W1] : aNormalFormOfIn0(W1,W0,xR) ) ),
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(f35,plain,
! [X0,X1,X2] :
( ~ aReductOfIn0(X2,X0,X1)
| sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f39,plain,
! [W0,W1,W2] :
( ( sdtmndtasgtdt0(W0,W1,W2)
<=> ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2 ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f40,plain,
! [W0,W1,W2] :
( ( ( ( ~ sdtmndtplgtdt0(W0,W1,W2)
& W0 != W2 )
| sdtmndtasgtdt0(W0,W1,W2) )
& ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2
| ~ sdtmndtasgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f42,plain,
! [X0,X1,X2] :
( X0 != X2
| sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ~ sdtmndtplgtdt0(X0,X1,X2)
| sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f44,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(f45,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)],[f44]) ).
fof(f72,plain,
! [W0] :
( ( isTerminating0(W0)
<=> ! [W1,W2] :
( iLess0(W2,W1)
| ~ sdtmndtplgtdt0(W1,W0,W2)
| ~ aElement0(W2)
| ~ aElement0(W1) ) )
| ~ aRewritingSystem0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f73,plain,
! [W0] :
( ( ( ? [W1,W2] :
( ~ iLess0(W2,W1)
& sdtmndtplgtdt0(W1,W0,W2)
& aElement0(W2)
& aElement0(W1) )
| isTerminating0(W0) )
& ( ! [W1,W2] :
( iLess0(W2,W1)
| ~ sdtmndtplgtdt0(W1,W0,W2)
| ~ aElement0(W2)
| ~ aElement0(W1) )
| ~ isTerminating0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(NNF_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
! [W0] :
( ( ( ( ~ iLess0(sK10_skl(W0),sK9_skl(W0))
& sdtmndtplgtdt0(sK9_skl(W0),W0,sK10_skl(W0))
& aElement0(sK10_skl(W0))
& aElement0(sK9_skl(W0)) )
| isTerminating0(W0) )
& ( ! [W1,W2] :
( iLess0(W2,W1)
| ~ sdtmndtplgtdt0(W1,W0,W2)
| ~ aElement0(W2)
| ~ aElement0(W1) )
| ~ isTerminating0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(W1,sK9_skl(W0)),skolemize(W2,sK10_skl(W0))],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( iLess0(X2,X1)
| ~ sdtmndtplgtdt0(X1,X0,X2)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ isTerminating0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
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(f84,plain,
! [X0,X1,X2] :
( aElement0(X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( sdtmndtasgtdt0(X0,X1,X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
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(f87,plain,
! [X0,X1,X2] :
( aReductOfIn0(sK11_skl(X2,X1,X0),X2,X1)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f88,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f89,plain,
isTerminating0(xR),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f90,plain,
? [W0] :
( ! [W1] : ~ aNormalFormOfIn0(W1,W0,xR)
& ! [W1] :
( ? [W2] : aNormalFormOfIn0(W2,W1,xR)
| ~ iLess0(W1,W0)
| ~ aElement0(W1) )
& aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f91,plain,
( ! [W1] : ~ aNormalFormOfIn0(W1,sK12_skl,xR)
& ! [W1] :
( aNormalFormOfIn0(sK13_skl(W1),W1,xR)
| ~ iLess0(W1,sK12_skl)
| ~ aElement0(W1) )
& aElement0(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(W0,sK12_skl),skolemize(W2,sK13_skl(W1))],[f90]) ).
fof(f92,plain,
aElement0(sK12_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [X0] :
( aNormalFormOfIn0(sK13_skl(X0),X0,xR)
| ~ iLess0(X0,sK12_skl)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f94,plain,
! [X0] : ~ aNormalFormOfIn0(X0,sK12_skl,xR),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ~ aReductOfIn0(X2,X0,X1)
| sdtmndtplgtdt0(X0,X1,X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f35,f24]) ).
fof(f97,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X2,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f42]) ).
fof(f98,plain,
! [X0,X1] :
( sdtmndtasgtdt0(X0,X1,X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f97]) ).
fof(f102,plain,
! [X0] :
( sdtmndtasgtdt0(sK12_skl,X0,sK12_skl)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[f98,f92]) ).
fof(f103,plain,
sdtmndtasgtdt0(sK12_skl,xR,sK12_skl),
inference(resolution,[status(thm)],[f102,f88]) ).
fof(f105,definition,
( sQ0_spl
<=> aElement0(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f107,plain,
( sQ0_spl
| ~ aElement0(sK12_skl) ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f108,definition,
( sQ1_spl
<=> aRewritingSystem0(xR) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f110,plain,
( sQ1_spl
| ~ aRewritingSystem0(xR) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f142,definition,
( sQ9_spl
<=> isTerminating0(xR) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f144,plain,
( sQ9_spl
| ~ isTerminating0(xR) ),
inference(component_clause,[status(thm)],[f142]) ).
fof(f149,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f107,f92]) ).
fof(f150,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f149]) ).
fof(f151,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f110,f88]) ).
fof(f152,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f151]) ).
fof(f153,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f144,f89]) ).
fof(f154,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f153]) ).
fof(f582,plain,
( aReductOfIn0(sK11_skl(sK12_skl,xR,sK12_skl),sK12_skl,xR)
| ~ aElement0(sK12_skl)
| aNormalFormOfIn0(sK12_skl,sK12_skl,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f87,f103]) ).
fof(f597,definition,
( sQ87_spl
<=> aNormalFormOfIn0(sK12_skl,sK12_skl,xR) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( ~ sQ87_spl
| aNormalFormOfIn0(sK12_skl,sK12_skl,xR) ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f600,definition,
( sQ88_spl
<=> aReductOfIn0(sK11_skl(sK12_skl,xR,sK12_skl),sK12_skl,xR) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f601,plain,
( ~ sQ88_spl
| aReductOfIn0(sK11_skl(sK12_skl,xR,sK12_skl),sK12_skl,xR) ),
inference(component_clause,[status(thm)],[f600]) ).
fof(f603,plain,
( sQ88_spl
| sQ87_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f582,f105,f108,f597,f600]) ).
fof(f604,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f94]) ).
fof(f605,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f604]) ).
fof(f667,plain,
( ~ sQ88_spl
| sdtmndtplgtdt0(sK12_skl,xR,sK11_skl(sK12_skl,xR,sK12_skl))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f601,f95]) ).
fof(f668,plain,
( ~ sQ88_spl
| aElement0(sK11_skl(sK12_skl,xR,sK12_skl))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f601,f24]) ).
fof(f685,definition,
( sQ103_spl
<=> sdtmndtplgtdt0(sK12_skl,xR,sK11_skl(sK12_skl,xR,sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f686,plain,
( ~ sQ103_spl
| sdtmndtplgtdt0(sK12_skl,xR,sK11_skl(sK12_skl,xR,sK12_skl)) ),
inference(component_clause,[status(thm)],[f685]) ).
fof(f688,plain,
( ~ sQ88_spl
| sQ103_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f667,f105,f108,f685,f600]) ).
fof(f689,definition,
( sQ104_spl
<=> aElement0(sK11_skl(sK12_skl,xR,sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( ~ sQ88_spl
| sQ104_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f668,f105,f108,f689,f600]) ).
fof(f693,plain,
( ~ sQ103_spl
| sdtmndtasgtdt0(sK12_skl,xR,sK11_skl(sK12_skl,xR,sK12_skl))
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f686,f43]) ).
fof(f698,plain,
( ~ sQ103_spl
| iLess0(sK11_skl(sK12_skl,xR,sK12_skl),sK12_skl)
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl))
| ~ aElement0(sK12_skl)
| ~ isTerminating0(xR)
| ~ aRewritingSystem0(xR) ),
inference(resolution,[status(thm)],[f686,f75]) ).
fof(f699,definition,
( sQ105_spl
<=> sdtmndtasgtdt0(sK12_skl,xR,sK11_skl(sK12_skl,xR,sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f700,plain,
( ~ sQ105_spl
| sdtmndtasgtdt0(sK12_skl,xR,sK11_skl(sK12_skl,xR,sK12_skl)) ),
inference(component_clause,[status(thm)],[f699]) ).
fof(f702,plain,
( ~ sQ103_spl
| sQ105_spl
| ~ sQ104_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f693,f105,f108,f689,f699,f685]) ).
fof(f716,definition,
( sQ109_spl
<=> iLess0(sK11_skl(sK12_skl,xR,sK12_skl),sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f717,plain,
( ~ sQ109_spl
| iLess0(sK11_skl(sK12_skl,xR,sK12_skl),sK12_skl) ),
inference(component_clause,[status(thm)],[f716]) ).
fof(f719,plain,
( ~ sQ103_spl
| sQ109_spl
| ~ sQ104_spl
| ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f698,f108,f142,f105,f689,f716,f685]) ).
fof(f858,plain,
( ~ sQ109_spl
| aNormalFormOfIn0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),sK11_skl(sK12_skl,xR,sK12_skl),xR)
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl)) ),
inference(resolution,[status(thm)],[f717,f93]) ).
fof(f859,definition,
( sQ129_spl
<=> aNormalFormOfIn0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),sK11_skl(sK12_skl,xR,sK12_skl),xR) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( ~ sQ129_spl
| aNormalFormOfIn0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),sK11_skl(sK12_skl,xR,sK12_skl),xR) ),
inference(component_clause,[status(thm)],[f859]) ).
fof(f862,plain,
( ~ sQ109_spl
| sQ129_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f858,f689,f859,f716]) ).
fof(f867,plain,
! [X0] :
( ~ sQ105_spl
| sdtmndtasgtdt0(sK12_skl,xR,X0)
| ~ sdtmndtasgtdt0(sK11_skl(sK12_skl,xR,sK12_skl),xR,X0)
| ~ aElement0(X0)
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f700,f45]) ).
fof(f888,definition,
! [X0] :
( sQ135_spl
<=> ( sdtmndtasgtdt0(sK12_skl,xR,X0)
| ~ sdtmndtasgtdt0(sK11_skl(sK12_skl,xR,sK12_skl),xR,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f889,plain,
! [X0] :
( ~ sQ135_spl
| sdtmndtasgtdt0(sK12_skl,xR,X0)
| ~ sdtmndtasgtdt0(sK11_skl(sK12_skl,xR,sK12_skl),xR,X0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f888]) ).
fof(f891,plain,
( ~ sQ105_spl
| sQ135_spl
| ~ sQ104_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f867,f105,f108,f689,f888,f699]) ).
fof(f1219,plain,
! [X0] :
( ~ sQ129_spl
| ~ aReductOfIn0(X0,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl)) ),
inference(resolution,[status(thm)],[f860,f86]) ).
fof(f1220,plain,
( ~ sQ129_spl
| sdtmndtasgtdt0(sK11_skl(sK12_skl,xR,sK12_skl),xR,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl)) ),
inference(resolution,[status(thm)],[f860,f85]) ).
fof(f1221,plain,
( ~ sQ129_spl
| aElement0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)))
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK11_skl(sK12_skl,xR,sK12_skl)) ),
inference(resolution,[status(thm)],[f860,f84]) ).
fof(f1222,definition,
! [X0] :
( sQ197_spl
<=> ~ aReductOfIn0(X0,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
! [X0] :
( ~ sQ197_spl
| ~ aReductOfIn0(X0,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR) ),
inference(component_clause,[status(thm)],[f1222]) ).
fof(f1225,plain,
( ~ sQ129_spl
| sQ197_spl
| ~ sQ1_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f1219,f689,f108,f1222,f859]) ).
fof(f1226,definition,
( sQ198_spl
<=> sdtmndtasgtdt0(sK11_skl(sK12_skl,xR,sK12_skl),xR,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1227,plain,
( ~ sQ198_spl
| sdtmndtasgtdt0(sK11_skl(sK12_skl,xR,sK12_skl),xR,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl))) ),
inference(component_clause,[status(thm)],[f1226]) ).
fof(f1229,plain,
( ~ sQ129_spl
| sQ198_spl
| ~ sQ1_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f1220,f689,f108,f1226,f859]) ).
fof(f1230,definition,
( sQ199_spl
<=> aElement0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1233,plain,
( ~ sQ129_spl
| sQ199_spl
| ~ sQ1_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f1221,f689,f108,f1230,f859]) ).
fof(f1542,plain,
( ~ sQ135_spl
| ~ sQ198_spl
| sdtmndtasgtdt0(sK12_skl,xR,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)))
| ~ aElement0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl))) ),
inference(resolution,[status(thm)],[f1227,f889]) ).
fof(f1549,definition,
( sQ248_spl
<=> sdtmndtasgtdt0(sK12_skl,xR,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition]) ).
fof(f1550,plain,
( ~ sQ248_spl
| sdtmndtasgtdt0(sK12_skl,xR,sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl))) ),
inference(component_clause,[status(thm)],[f1549]) ).
fof(f1552,plain,
( ~ sQ135_spl
| ~ sQ198_spl
| sQ248_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f1542,f1230,f1549,f1226,f888]) ).
fof(f1695,plain,
( ~ sQ248_spl
| aReductOfIn0(sK11_skl(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR,sK12_skl),sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR)
| ~ aElement0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)))
| aNormalFormOfIn0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),sK12_skl,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(sK12_skl) ),
inference(resolution,[status(thm)],[f1550,f87]) ).
fof(f1701,definition,
( sQ276_spl
<=> aNormalFormOfIn0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),sK12_skl,xR) ),
introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition]) ).
fof(f1702,plain,
( ~ sQ276_spl
| aNormalFormOfIn0(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),sK12_skl,xR) ),
inference(component_clause,[status(thm)],[f1701]) ).
fof(f1704,definition,
( sQ277_spl
<=> aReductOfIn0(sK11_skl(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR,sK12_skl),sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f1705,plain,
( ~ sQ277_spl
| aReductOfIn0(sK11_skl(sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR,sK12_skl),sK13_skl(sK11_skl(sK12_skl,xR,sK12_skl)),xR) ),
inference(component_clause,[status(thm)],[f1704]) ).
fof(f1707,plain,
( ~ sQ248_spl
| sQ277_spl
| ~ sQ199_spl
| sQ276_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1695,f105,f108,f1701,f1230,f1704,f1549]) ).
fof(f1731,plain,
( ~ sQ276_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1702,f94]) ).
fof(f1732,plain,
~ sQ276_spl,
inference(contradiction_clause,[status(thm)],[f1731]) ).
fof(f1749,plain,
( ~ sQ277_spl
| ~ sQ197_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1705,f1223]) ).
fof(f1750,plain,
( ~ sQ277_spl
| ~ sQ197_spl ),
inference(contradiction_clause,[status(thm)],[f1749]) ).
fof(f1751,plain,
$false,
inference(sat_refutation,[status(thm)],[f150,f152,f154,f603,f605,f688,f692,f702,f719,f862,f891,f1225,f1229,f1233,f1552,f1707,f1732,f1750]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COM013+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n013.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 14:13:52 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.50 % Drodi V4.1.1
% 0.19/0.61 % Refutation found
% 0.19/0.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.24/0.65 % Elapsed time: 0.161925 seconds
% 0.24/0.65 % CPU time: 0.937034 seconds
% 0.24/0.65 % Total memory used: 85.041 MB
% 0.24/0.65 % Net memory used: 84.534 MB
%------------------------------------------------------------------------------