%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM021+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 : n026.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.21s 5.53s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 16
% Syntax : Number of formulae : 69 ( 16 unt; 11 def)
% Number of atoms : 251 ( 13 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 313 ( 131 ~; 129 |; 36 &)
% ( 14 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 9 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-3 aty)
% Number of variables : 81 ( 75 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(f15,hypothesis,
aRewritingSystem0(xR),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
( sdtmndtasgtdt0(xv,xR,xw)
& sdtmndtasgtdt0(xu,xR,xw)
& aElement0(xw) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
aNormalFormOfIn0(xd,xw,xR),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
( sdtmndtasgtdt0(xd,xR,xx)
& sdtmndtasgtdt0(xb,xR,xx)
& aElement0(xx) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,conjecture,
sdtmndtasgtdt0(xb,xR,xd),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(negated_conjecture,[status(cth)],[f25]) ).
fof(f39,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(f40,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)],[f39]) ).
fof(f41,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))],[f40]) ).
fof(f43,plain,
! [X0,X1,X2] :
( aReductOfIn0(sK0_skl(X2,X1,X0),X0,X1)
| aReductOfIn0(X2,X0,X1)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f49,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(f50,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)],[f49]) ).
fof(f51,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)],[f50]) ).
fof(f90,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(f91,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)],[f90]) ).
fof(f92,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)],[f91]) ).
fof(f93,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))],[f92]) ).
fof(f94,plain,
! [X0,X1,X2] :
( aElement0(X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( ~ aReductOfIn0(X3,X2,X1)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f101,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f120,plain,
aElement0(xw),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f123,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f124,plain,
aElement0(xx),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f125,plain,
sdtmndtasgtdt0(xb,xR,xx),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f126,plain,
sdtmndtasgtdt0(xd,xR,xx),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f127,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f178,definition,
( sQ1_spl
<=> aRewritingSystem0(xR) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( sQ1_spl
| ~ aRewritingSystem0(xR) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f196,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f180,f101]) ).
fof(f197,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f196]) ).
fof(f213,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aNormalFormOfIn0(X1,X0,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f94,f101]) ).
fof(f214,plain,
( aElement0(xd)
| ~ aElement0(xw) ),
inference(resolution,[status(thm)],[f213,f123]) ).
fof(f215,definition,
( sQ7_spl
<=> aElement0(xw) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( sQ7_spl
| ~ aElement0(xw) ),
inference(component_clause,[status(thm)],[f215]) ).
fof(f218,definition,
( sQ8_spl
<=> aElement0(xd) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f221,plain,
( sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f214,f215,f218]) ).
fof(f222,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f120]) ).
fof(f223,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f222]) ).
fof(f291,definition,
( sQ20_spl
<=> aElement0(xx) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ20_spl
| ~ aElement0(xx) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f311,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f293,f124]) ).
fof(f312,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f311]) ).
fof(f327,plain,
! [X0,X1,X2] :
( ~ aReductOfIn0(X2,X1,xR)
| ~ aNormalFormOfIn0(X1,X0,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f96,f101]) ).
fof(f328,plain,
! [X0] :
( ~ aReductOfIn0(X0,xd,xR)
| ~ aElement0(xw) ),
inference(resolution,[status(thm)],[f327,f123]) ).
fof(f329,definition,
! [X0] :
( sQ26_spl
<=> ~ aReductOfIn0(X0,xd,xR) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f330,plain,
! [X0] :
( ~ sQ26_spl
| ~ aReductOfIn0(X0,xd,xR) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,plain,
( sQ26_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f328,f215,f329]) ).
fof(f333,plain,
! [X0] :
( ~ sQ26_spl
| aReductOfIn0(X0,xd,xR)
| ~ sdtmndtplgtdt0(xd,xR,X0)
| ~ aElement0(X0)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xd) ),
inference(resolution,[status(thm)],[f330,f43]) ).
fof(f335,definition,
! [X0] :
( sQ27_spl
<=> ( aReductOfIn0(X0,xd,xR)
| ~ sdtmndtplgtdt0(xd,xR,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f336,plain,
! [X0] :
( ~ sQ27_spl
| aReductOfIn0(X0,xd,xR)
| ~ sdtmndtplgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,plain,
( ~ sQ26_spl
| sQ27_spl
| ~ sQ1_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f333,f218,f178,f335,f329]) ).
fof(f343,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ26_spl
| ~ sdtmndtplgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f336,f330]) ).
fof(f356,plain,
! [X0,X1] :
( sdtmndtplgtdt0(X0,xR,X1)
| X0 = X1
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f51,f101]) ).
fof(f460,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ26_spl
| ~ aElement0(X0)
| xd = X0
| ~ sdtmndtasgtdt0(xd,xR,X0)
| ~ aElement0(X0)
| ~ aElement0(xd) ),
inference(resolution,[status(thm)],[f356,f343]) ).
fof(f462,definition,
! [X0] :
( sQ45_spl
<=> ( ~ aElement0(X0)
| xd = X0
| ~ sdtmndtasgtdt0(xd,xR,X0)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f463,plain,
! [X0] :
( ~ sQ45_spl
| ~ aElement0(X0)
| xd = X0
| ~ sdtmndtasgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( ~ sQ27_spl
| ~ sQ26_spl
| sQ45_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f460,f218,f462,f329,f335]) ).
fof(f466,plain,
! [X0] :
( ~ sQ45_spl
| xd = X0
| ~ sdtmndtasgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f463]) ).
fof(f486,plain,
( ~ sQ45_spl
| xd = xx
| ~ aElement0(xx) ),
inference(resolution,[status(thm)],[f466,f126]) ).
fof(f493,definition,
( sQ48_spl
<=> xd = xx ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( ~ sQ48_spl
| xd = xx ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,plain,
( ~ sQ45_spl
| sQ48_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f486,f291,f493,f462]) ).
fof(f551,plain,
( ~ sQ48_spl
| ~ sdtmndtasgtdt0(xb,xR,xx) ),
inference(backward_demodulation,[status(thm)],[f494,f127]) ).
fof(f554,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f551,f125]) ).
fof(f555,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f554]) ).
fof(f556,plain,
$false,
inference(sat_refutation,[status(thm)],[f197,f221,f223,f312,f332,f338,f465,f496,f555]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COM021+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.43 % Computer : n026.cluster.edu
% 0.15/5.43 % Model : x86_64 x86_64
% 0.15/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.43 % Memory : 8046.5625MB
% 0.15/5.43 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Mon Sep 21 14:17:43 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.45 % Drodi V4.1.1
% 0.21/5.53 % Refutation found
% 0.21/5.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/5.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/5.56 % Elapsed time: 0.104080 seconds
% 0.21/5.56 % CPU time: 0.577400 seconds
% 0.21/5.56 % Total memory used: 88.491 MB
% 0.21/5.56 % Net memory used: 88.037 MB
%------------------------------------------------------------------------------