%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM022+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 0.09s 0.40s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 21
% Syntax : Number of formulae : 98 ( 13 unt; 18 def)
% Number of atoms : 349 ( 13 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 393 ( 142 ~; 145 |; 78 &)
% ( 20 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 17 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-3 aty)
% Number of variables : 69 ( 52 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
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/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(f15,hypothesis,
aRewritingSystem0(xR),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
( ( ( sdtmndtplgtdt0(xa,xR,xc)
& sdtmndtplgtdt0(xa,xR,xb) )
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& sdtmndtasgtdt0(xb,xR,W3)
& aNormalFormOfIn0(W3,W2,xR) )
& sdtmndtasgtdt0(W1,xR,W2)
& sdtmndtasgtdt0(W0,xR,W2)
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) ) )
=> ( ( sdtmndtasgtdt0(xa,xR,xc)
& sdtmndtasgtdt0(xa,xR,xb) )
=> ? [W0] :
( sdtmndtasgtdt0(xc,xR,W0)
& sdtmndtasgtdt0(xb,xR,W0)
& aElement0(W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ( ( ( sdtmndtplgtdt0(xa,xR,xc)
& sdtmndtplgtdt0(xa,xR,xb) )
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& sdtmndtasgtdt0(xb,xR,W3)
& aNormalFormOfIn0(W3,W2,xR) )
& sdtmndtasgtdt0(W1,xR,W2)
& sdtmndtasgtdt0(W0,xR,W2)
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) ) )
=> ( ( sdtmndtasgtdt0(xa,xR,xc)
& sdtmndtasgtdt0(xa,xR,xb) )
=> ? [W0] :
( sdtmndtasgtdt0(xc,xR,W0)
& sdtmndtasgtdt0(xb,xR,W0)
& aElement0(W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f43,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(f44,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)],[f43]) ).
fof(f45,plain,
! [X0,X1,X2] :
( sdtmndtplgtdt0(X0,X1,X2)
| X0 = X2
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( X0 != X2
| sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f84,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(f85,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)],[f84]) ).
fof(f86,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)],[f85]) ).
fof(f87,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))],[f86]) ).
fof(f88,plain,
! [X0,X1,X2] :
( aElement0(X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f95,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f98,plain,
aElement0(xa),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f99,plain,
aElement0(xb),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f100,plain,
aElement0(xc),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f106,plain,
( ! [W0] :
( ~ sdtmndtasgtdt0(xc,xR,W0)
| ~ sdtmndtasgtdt0(xb,xR,W0)
| ~ aElement0(W0) )
& sdtmndtasgtdt0(xa,xR,xc)
& sdtmndtasgtdt0(xa,xR,xb)
& ( ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& sdtmndtasgtdt0(xb,xR,W3)
& aNormalFormOfIn0(W3,W2,xR) )
& sdtmndtasgtdt0(W1,xR,W2)
& sdtmndtasgtdt0(W0,xR,W2)
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f107,plain,
( ! [W0] :
( ~ sdtmndtasgtdt0(xc,xR,W0)
| ~ sdtmndtasgtdt0(xb,xR,W0)
| ~ aElement0(W0) )
& sdtmndtasgtdt0(xa,xR,xc)
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtasgtdt0(xc,xR,sK17_skl)
& sdtmndtasgtdt0(xb,xR,sK17_skl)
& aNormalFormOfIn0(sK17_skl,sK16_skl,xR)
& sdtmndtasgtdt0(sK15_skl,xR,sK16_skl)
& sdtmndtasgtdt0(sK14_skl,xR,sK16_skl)
& aElement0(sK16_skl)
& sdtmndtasgtdt0(sK15_skl,xR,xc)
& aReductOfIn0(sK15_skl,xa,xR)
& aElement0(sK15_skl)
& sdtmndtasgtdt0(sK14_skl,xR,xb)
& aReductOfIn0(sK14_skl,xa,xR)
& aElement0(sK14_skl) )
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(W0,sK14_skl),skolemize(W1,sK15_skl),skolemize(W2,sK16_skl),skolemize(W3,sK17_skl)],[f106]) ).
fof(f114,plain,
( aElement0(sK16_skl)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f117,plain,
( aNormalFormOfIn0(sK17_skl,sK16_skl,xR)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f118,plain,
( sdtmndtasgtdt0(xb,xR,sK17_skl)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f119,plain,
( sdtmndtasgtdt0(xc,xR,sK17_skl)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f120,plain,
sdtmndtasgtdt0(xa,xR,xb),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f121,plain,
sdtmndtasgtdt0(xa,xR,xc),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f122,plain,
! [X0] :
( ~ sdtmndtasgtdt0(xc,xR,X0)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f123,definition,
( sQ0_spl
<=> sdtmndtplgtdt0(xa,xR,xb) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f125,plain,
( sQ0_spl
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(component_clause,[status(thm)],[f123]) ).
fof(f126,definition,
( sQ1_spl
<=> sdtmndtplgtdt0(xa,xR,xc) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f128,plain,
( sQ1_spl
| ~ sdtmndtplgtdt0(xa,xR,xc) ),
inference(component_clause,[status(thm)],[f126]) ).
fof(f153,definition,
( sQ8_spl
<=> aElement0(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( ~ sQ8_spl
| aElement0(sK16_skl) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f156,plain,
( sQ8_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f114,f123,f126,f153]) ).
fof(f165,definition,
( sQ11_spl
<=> aNormalFormOfIn0(sK17_skl,sK16_skl,xR) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f166,plain,
( ~ sQ11_spl
| aNormalFormOfIn0(sK17_skl,sK16_skl,xR) ),
inference(component_clause,[status(thm)],[f165]) ).
fof(f168,plain,
( sQ11_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f117,f123,f126,f165]) ).
fof(f169,definition,
( sQ12_spl
<=> sdtmndtasgtdt0(xb,xR,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f172,plain,
( sQ12_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f118,f123,f126,f169]) ).
fof(f173,definition,
( sQ13_spl
<=> sdtmndtasgtdt0(xc,xR,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( ~ sQ13_spl
| sdtmndtasgtdt0(xc,xR,sK17_skl) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f176,plain,
( sQ13_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f119,f123,f126,f173]) ).
fof(f177,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X2,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f46]) ).
fof(f178,plain,
! [X0,X1] :
( sdtmndtasgtdt0(X0,X1,X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f177]) ).
fof(f184,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aNormalFormOfIn0(X1,X0,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f95,f88]) ).
fof(f186,plain,
! [X0] :
( sdtmndtasgtdt0(X0,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f178,f95]) ).
fof(f187,plain,
( ~ sdtmndtasgtdt0(xb,xR,xc)
| ~ aElement0(xc)
| ~ aElement0(xc) ),
inference(resolution,[status(thm)],[f186,f122]) ).
fof(f188,plain,
( ~ sdtmndtasgtdt0(xc,xR,xb)
| ~ aElement0(xb)
| ~ aElement0(xb) ),
inference(resolution,[status(thm)],[f186,f122]) ).
fof(f189,definition,
( sQ14_spl
<=> aElement0(xc) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( sQ14_spl
| ~ aElement0(xc) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f192,definition,
( sQ15_spl
<=> sdtmndtasgtdt0(xb,xR,xc) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f194,plain,
( sQ15_spl
| ~ sdtmndtasgtdt0(xb,xR,xc) ),
inference(component_clause,[status(thm)],[f192]) ).
fof(f195,plain,
( ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f187,f189,f192]) ).
fof(f196,definition,
( sQ16_spl
<=> aElement0(xb) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( sQ16_spl
| ~ aElement0(xb) ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,definition,
( sQ17_spl
<=> sdtmndtasgtdt0(xc,xR,xb) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f201,plain,
( sQ17_spl
| ~ sdtmndtasgtdt0(xc,xR,xb) ),
inference(component_clause,[status(thm)],[f199]) ).
fof(f202,plain,
( ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f188,f196,f199]) ).
fof(f203,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f198,f99]) ).
fof(f204,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f203]) ).
fof(f205,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f191,f100]) ).
fof(f206,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f205]) ).
fof(f226,plain,
! [X0,X1] :
( sdtmndtplgtdt0(X0,xR,X1)
| X0 = X1
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f45,f95]) ).
fof(f227,plain,
( sQ1_spl
| xa = xc
| ~ sdtmndtasgtdt0(xa,xR,xc)
| ~ aElement0(xc)
| ~ aElement0(xa) ),
inference(resolution,[status(thm)],[f226,f128]) ).
fof(f229,definition,
( sQ21_spl
<=> aElement0(xa) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( sQ21_spl
| ~ aElement0(xa) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f232,definition,
( sQ22_spl
<=> sdtmndtasgtdt0(xa,xR,xc) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( sQ22_spl
| ~ sdtmndtasgtdt0(xa,xR,xc) ),
inference(component_clause,[status(thm)],[f232]) ).
fof(f235,definition,
( sQ23_spl
<=> xa = xc ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f236,plain,
( ~ sQ23_spl
| xa = xc ),
inference(component_clause,[status(thm)],[f235]) ).
fof(f238,plain,
( sQ1_spl
| sQ23_spl
| ~ sQ22_spl
| ~ sQ14_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f227,f229,f189,f232,f235,f126]) ).
fof(f239,plain,
( sQ0_spl
| xa = xb
| ~ sdtmndtasgtdt0(xa,xR,xb)
| ~ aElement0(xb)
| ~ aElement0(xa) ),
inference(resolution,[status(thm)],[f125,f226]) ).
fof(f240,definition,
( sQ24_spl
<=> sdtmndtasgtdt0(xa,xR,xb) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f242,plain,
( sQ24_spl
| ~ sdtmndtasgtdt0(xa,xR,xb) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
( sQ25_spl
<=> xa = xb ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( ~ sQ25_spl
| xa = xb ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,plain,
( sQ0_spl
| sQ25_spl
| ~ sQ24_spl
| ~ sQ16_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f239,f229,f196,f240,f243,f123]) ).
fof(f247,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f231,f98]) ).
fof(f248,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f247]) ).
fof(f249,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f242,f120]) ).
fof(f250,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f249]) ).
fof(f251,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f234,f121]) ).
fof(f252,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f251]) ).
fof(f256,plain,
( sQ17_spl
| ~ sQ23_spl
| ~ sdtmndtasgtdt0(xa,xR,xb) ),
inference(backward_demodulation,[status(thm)],[f236,f201]) ).
fof(f260,plain,
( sQ17_spl
| ~ sQ23_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f256,f240,f235,f199]) ).
fof(f274,plain,
( sQ15_spl
| ~ sQ25_spl
| ~ sdtmndtasgtdt0(xa,xR,xc) ),
inference(forward_demodulation,[status(thm)],[f244,f194]) ).
fof(f276,plain,
( sQ15_spl
| ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f121,f274]) ).
fof(f277,plain,
( sQ15_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f276]) ).
fof(f307,definition,
( sQ33_spl
<=> aElement0(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f309,plain,
( sQ33_spl
| ~ aElement0(sK17_skl) ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f315,plain,
! [X0] :
( sQ33_spl
| ~ aNormalFormOfIn0(sK17_skl,X0,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f309,f184]) ).
fof(f316,plain,
( ~ sQ13_spl
| ~ sdtmndtasgtdt0(xb,xR,sK17_skl)
| ~ aElement0(sK17_skl) ),
inference(resolution,[status(thm)],[f174,f122]) ).
fof(f317,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f316,f307,f169,f173]) ).
fof(f356,plain,
( ~ sQ11_spl
| sQ33_spl
| ~ aElement0(sK16_skl) ),
inference(resolution,[status(thm)],[f315,f166]) ).
fof(f357,plain,
( ~ sQ11_spl
| sQ33_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f356,f154]) ).
fof(f358,plain,
( ~ sQ11_spl
| sQ33_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f357]) ).
fof(f359,plain,
$false,
inference(sat_refutation,[status(thm)],[f156,f168,f172,f176,f195,f202,f204,f206,f238,f246,f248,f250,f252,f260,f277,f317,f358]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM022+1 : 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.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:14:40 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.40 % Refutation found
% 0.09/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.44 % Elapsed time: 0.061654 seconds
% 0.09/0.44 % CPU time: 0.175168 seconds
% 0.09/0.44 % Total memory used: 83.638 MB
% 0.09/0.44 % Net memory used: 83.546 MB
%------------------------------------------------------------------------------