%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : COM022+4 : 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:19 PM UTC 2026
% Result : Theorem 0.14s 5.42s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 7
% Syntax : Number of formulae : 64 ( 13 unt; 4 def)
% Number of atoms : 694 ( 83 equ)
% Maximal formula atoms : 96 ( 10 avg)
% Number of connectives : 798 ( 168 ~; 253 |; 364 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 3 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% Number of variables : 121 ( 53 !; 68 ?)
% 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
aRewritingSystem0(xR),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
( ( ( ( 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) ) )
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ~ ? [W4] : aReductOfIn0(W4,W3,xR)
& 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 )
& aElement0(W3) )
& 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 )
& 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 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& ( ( sdtmndtplgtdt0(W0,xR,xb)
& ( ? [W1] :
( sdtmndtplgtdt0(W1,xR,xb)
& aReductOfIn0(W1,W0,xR)
& aElement0(W1) )
| aReductOfIn0(xb,W0,xR) ) )
| W0 = xb )
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) ) )
=> ( ( sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb ) )
=> ? [W0] :
( ( sdtmndtasgtdt0(xc,xR,W0)
| sdtmndtplgtdt0(xc,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xc,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xc,xR)
| xc = 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ( ( ( ( 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) ) )
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ~ ? [W4] : aReductOfIn0(W4,W3,xR)
& 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 )
& aElement0(W3) )
& 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 )
& 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 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& ( ( sdtmndtplgtdt0(W0,xR,xb)
& ( ? [W1] :
( sdtmndtplgtdt0(W1,xR,xb)
& aReductOfIn0(W1,W0,xR)
& aElement0(W1) )
| aReductOfIn0(xb,W0,xR) ) )
| W0 = xb )
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) ) )
=> ( ( sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb ) )
=> ? [W0] :
( ( sdtmndtasgtdt0(xc,xR,W0)
| sdtmndtplgtdt0(xc,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xc,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xc,xR)
| xc = 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)],[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(f46,plain,
! [X0,X1,X2] :
( X0 != X2
| sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f95,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f116,plain,
aElement0(xb),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f117,plain,
aElement0(xc),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f177,plain,
( ! [W0] :
( ( ~ sdtmndtasgtdt0(xc,xR,W0)
& ~ sdtmndtplgtdt0(xc,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xc,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xc,xR)
& xc != 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) )
& sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb )
& ( ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ! [W4] : ~ aReductOfIn0(W4,W3,xR)
& 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 )
& aElement0(W3) )
& 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 )
& 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 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& ( ( sdtmndtplgtdt0(W0,xR,xb)
& ( ? [W1] :
( sdtmndtplgtdt0(W1,xR,xb)
& aReductOfIn0(W1,W0,xR)
& aElement0(W1) )
| aReductOfIn0(xb,W0,xR) ) )
| W0 = xb )
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| ( ~ 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) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f178,definition,
( sP1_prd
<=> ( ( ~ 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) ) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f179,definition,
! [W0] :
( sP2_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,[sP2_prd])],[]) ).
fof(f180,plain,
( ! [W0] :
( ( ~ sdtmndtasgtdt0(xc,xR,W0)
& ~ sdtmndtplgtdt0(xc,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xc,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xc,xR)
& xc != W0 )
| sP2_prd(W0)
| ~ aElement0(W0) )
& sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb )
& ( ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ! [W4] : ~ aReductOfIn0(W4,W3,xR)
& 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 )
& aElement0(W3) )
& 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 )
& 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 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& sdtmndtasgtdt0(W0,xR,xb)
& ( ( sdtmndtplgtdt0(W0,xR,xb)
& ( ? [W1] :
( sdtmndtplgtdt0(W1,xR,xb)
& aReductOfIn0(W1,W0,xR)
& aElement0(W1) )
| aReductOfIn0(xb,W0,xR) ) )
| W0 = xb )
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| sP1_prd ) ),
inference(formula_renaming,[status(thm)],[f177,f179,f178]) ).
fof(f181,plain,
( ! [W0] :
( ( ~ sdtmndtasgtdt0(xc,xR,W0)
& ~ sdtmndtplgtdt0(xc,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xc,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xc,xR)
& xc != W0 )
| sP2_prd(W0)
| ~ aElement0(W0) )
& sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(sK31_skl,xR,xc)
& aReductOfIn0(sK31_skl,xa,xR)
& aElement0(sK31_skl) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(sK30_skl,xR,xb)
& aReductOfIn0(sK30_skl,xa,xR)
& aElement0(sK30_skl) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb )
& ( ( sdtmndtasgtdt0(xc,xR,sK26_skl)
& ( ( sdtmndtplgtdt0(xc,xR,sK26_skl)
& ( ( sdtmndtplgtdt0(sK29_skl,xR,sK26_skl)
& aReductOfIn0(sK29_skl,xc,xR)
& aElement0(sK29_skl) )
| aReductOfIn0(sK26_skl,xc,xR) ) )
| xc = sK26_skl )
& sdtmndtasgtdt0(xb,xR,sK26_skl)
& ( ( sdtmndtplgtdt0(xb,xR,sK26_skl)
& ( ( sdtmndtplgtdt0(sK28_skl,xR,sK26_skl)
& aReductOfIn0(sK28_skl,xb,xR)
& aElement0(sK28_skl) )
| aReductOfIn0(sK26_skl,xb,xR) ) )
| xb = sK26_skl )
& aNormalFormOfIn0(sK26_skl,sK23_skl,xR)
& ! [W4] : ~ aReductOfIn0(W4,sK26_skl,xR)
& sdtmndtasgtdt0(sK23_skl,xR,sK26_skl)
& ( ( sdtmndtplgtdt0(sK23_skl,xR,sK26_skl)
& ( ( sdtmndtplgtdt0(sK27_skl,xR,sK26_skl)
& aReductOfIn0(sK27_skl,sK23_skl,xR)
& aElement0(sK27_skl) )
| aReductOfIn0(sK26_skl,sK23_skl,xR) ) )
| sK23_skl = sK26_skl )
& aElement0(sK26_skl)
& sdtmndtasgtdt0(sK21_skl,xR,sK23_skl)
& ( ( sdtmndtplgtdt0(sK21_skl,xR,sK23_skl)
& ( ( sdtmndtplgtdt0(sK25_skl,xR,sK23_skl)
& aReductOfIn0(sK25_skl,sK21_skl,xR)
& aElement0(sK25_skl) )
| aReductOfIn0(sK23_skl,sK21_skl,xR) ) )
| sK21_skl = sK23_skl )
& sdtmndtasgtdt0(sK19_skl,xR,sK23_skl)
& ( ( sdtmndtplgtdt0(sK19_skl,xR,sK23_skl)
& ( ( sdtmndtplgtdt0(sK24_skl,xR,sK23_skl)
& aReductOfIn0(sK24_skl,sK19_skl,xR)
& aElement0(sK24_skl) )
| aReductOfIn0(sK23_skl,sK19_skl,xR) ) )
| sK19_skl = sK23_skl )
& aElement0(sK23_skl)
& sdtmndtasgtdt0(sK21_skl,xR,xc)
& ( ( sdtmndtplgtdt0(sK21_skl,xR,xc)
& ( ( sdtmndtplgtdt0(sK22_skl,xR,xc)
& aReductOfIn0(sK22_skl,sK21_skl,xR)
& aElement0(sK22_skl) )
| aReductOfIn0(xc,sK21_skl,xR) ) )
| sK21_skl = xc )
& aReductOfIn0(sK21_skl,xa,xR)
& aElement0(sK21_skl)
& sdtmndtasgtdt0(sK19_skl,xR,xb)
& ( ( sdtmndtplgtdt0(sK19_skl,xR,xb)
& ( ( sdtmndtplgtdt0(sK20_skl,xR,xb)
& aReductOfIn0(sK20_skl,sK19_skl,xR)
& aElement0(sK20_skl) )
| aReductOfIn0(xb,sK19_skl,xR) ) )
| sK19_skl = xb )
& aReductOfIn0(sK19_skl,xa,xR)
& aElement0(sK19_skl) )
| sP1_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl]),skolemize(W0,sK19_skl),skolemize(W1,sK20_skl),skolemize(W1,sK21_skl),skolemize(W2,sK22_skl),skolemize(W2,sK23_skl),skolemize(W3,sK24_skl),skolemize(W3,sK25_skl),skolemize(W3,sK26_skl),skolemize(W4,sK27_skl),skolemize(W4,sK28_skl),skolemize(W4,sK29_skl),skolemize(W0,sK30_skl),skolemize(W0,sK31_skl)],[f180]) ).
fof(f207,plain,
( aElement0(sK26_skl)
| sP1_prd ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f219,plain,
( sdtmndtasgtdt0(xb,xR,sK26_skl)
| sP1_prd ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f224,plain,
( sdtmndtasgtdt0(xc,xR,sK26_skl)
| sP1_prd ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f228,plain,
( sdtmndtplgtdt0(xa,xR,xb)
| xa = xb ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f233,plain,
( sdtmndtplgtdt0(xa,xR,xc)
| xa = xc ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f235,plain,
! [X0] :
( xc != X0
| sP2_prd(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f238,plain,
! [X0] :
( ~ sdtmndtplgtdt0(xc,xR,X0)
| sP2_prd(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f239,plain,
! [X0] :
( ~ sdtmndtasgtdt0(xc,xR,X0)
| sP2_prd(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f251,definition,
( sP3_prd
<=> ( ~ sdtmndtplgtdt0(xa,xR,xb)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xb)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xb,xa,xR) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f252,plain,
( sP1_prd
<=> ( ( ~ sdtmndtplgtdt0(xa,xR,xc)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xc)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xc,xa,xR) )
| sP3_prd ) ),
inference(formula_renaming,[status(thm)],[f178,f251]) ).
fof(f253,plain,
( ( ( ( sdtmndtplgtdt0(xa,xR,xc)
| ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) )
& ~ sP3_prd )
| sP1_prd )
& ( ( ~ sdtmndtplgtdt0(xa,xR,xc)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xc)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xc,xa,xR) )
| sP3_prd
| ~ sP1_prd ) ),
inference(NNF_transformation,[status(thm)],[f252]) ).
fof(f254,plain,
( ( ( ( sdtmndtplgtdt0(xa,xR,xc)
| ( sdtmndtplgtdt0(sK33_skl,xR,xc)
& aReductOfIn0(sK33_skl,xa,xR)
& aElement0(sK33_skl) )
| aReductOfIn0(xc,xa,xR) )
& ~ sP3_prd )
| sP1_prd )
& ( ( ~ sdtmndtplgtdt0(xa,xR,xc)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xc)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xc,xa,xR) )
| sP3_prd
| ~ sP1_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(W0,sK33_skl)],[f253]) ).
fof(f257,plain,
( ~ sdtmndtplgtdt0(xa,xR,xc)
| sP3_prd
| ~ sP1_prd ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f262,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
| sP2_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 )
| ~ sP2_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f179]) ).
fof(f263,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
| sP2_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 )
| ~ sP2_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f262]) ).
fof(f264,plain,
( ! [W0] :
( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ( sdtmndtplgtdt0(sK34_skl(W0),xR,W0)
& aReductOfIn0(sK34_skl(W0),xb,xR)
& aElement0(sK34_skl(W0)) )
| aReductOfIn0(W0,xb,xR)
| xb = W0
| sP2_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 )
| ~ sP2_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f263]) ).
fof(f265,plain,
! [X0] :
( xb != X0
| ~ sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f268,plain,
! [X0] :
( ~ sdtmndtplgtdt0(xb,xR,X0)
| ~ sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f269,plain,
! [X0] :
( ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f273,plain,
( ( sdtmndtplgtdt0(xa,xR,xb)
| ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR)
| sP3_prd )
& ( ( ~ sdtmndtplgtdt0(xa,xR,xb)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xb)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xb,xa,xR) )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f251]) ).
fof(f274,plain,
( ( sdtmndtplgtdt0(xa,xR,xb)
| ( sdtmndtplgtdt0(sK35_skl,xR,xb)
& aReductOfIn0(sK35_skl,xa,xR)
& aElement0(sK35_skl) )
| aReductOfIn0(xb,xa,xR)
| sP3_prd )
& ( ( ~ sdtmndtplgtdt0(xa,xR,xb)
& ! [W0] :
( ~ sdtmndtplgtdt0(W0,xR,xb)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xb,xa,xR) )
| ~ sP3_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(W0,sK35_skl)],[f273]) ).
fof(f277,plain,
( ~ sdtmndtplgtdt0(xa,xR,xb)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f281,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X2,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2) ),
inference(destructive_equality_resolution,[status(thm)],[f46]) ).
fof(f282,plain,
! [X0,X1] :
( sdtmndtasgtdt0(X0,X1,X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f281]) ).
fof(f306,plain,
( xc != xc
| sP2_prd(xc) ),
inference(resolution,[status(thm)],[f235,f117]) ).
fof(f313,plain,
sP2_prd(xc),
inference(trivial_equality_resolution,[status(thm)],[f306]) ).
fof(f314,plain,
xb != xc,
inference(resolution,[status(thm)],[f313,f265]) ).
fof(f332,plain,
( sP1_prd
| ~ sP2_prd(sK26_skl) ),
inference(resolution,[status(thm)],[f269,f219]) ).
fof(f338,plain,
! [X0] :
( sdtmndtasgtdt0(xb,X0,xb)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[f282,f116]) ).
fof(f346,plain,
sdtmndtasgtdt0(xb,xR,xb),
inference(resolution,[status(thm)],[f338,f95]) ).
fof(f347,plain,
~ sP2_prd(xb),
inference(resolution,[status(thm)],[f346,f269]) ).
fof(f382,plain,
( ~ sP3_prd
| xa = xb ),
inference(resolution,[status(thm)],[f228,f277]) ).
fof(f397,plain,
( xa = xc
| sP3_prd
| ~ sP1_prd ),
inference(resolution,[status(thm)],[f257,f233]) ).
fof(f413,plain,
( sP1_prd
| sP2_prd(sK26_skl)
| ~ aElement0(sK26_skl) ),
inference(resolution,[status(thm)],[f239,f224]) ).
fof(f414,plain,
( sP1_prd
| sP2_prd(sK26_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f207]) ).
fof(f417,plain,
( xa = xc
| sP3_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f397,f418]) ).
fof(f418,plain,
sP1_prd,
inference(forward_subsumption_resolution,[status(thm)],[f414,f332]) ).
fof(f419,plain,
( xa = xb
| xa = xc ),
inference(resolution,[status(thm)],[f417,f382]) ).
fof(f420,plain,
( xa = xc
| sdtmndtplgtdt0(xb,xR,xc)
| xa = xc ),
inference(paramodulation,[status(thm)],[f419,f233]) ).
fof(f433,plain,
( sdtmndtplgtdt0(xb,xR,xc)
| xa = xc ),
inference(duplicate_literals_removal,[status(thm)],[f420]) ).
fof(f440,plain,
( ~ sP2_prd(xc)
| xa = xc ),
inference(resolution,[status(thm)],[f433,f268]) ).
fof(f445,plain,
xa = xc,
inference(forward_subsumption_resolution,[status(thm)],[f440,f313]) ).
fof(f457,plain,
( sdtmndtplgtdt0(xc,xR,xb)
| xa = xb ),
inference(backward_demodulation,[status(thm)],[f445,f228]) ).
fof(f469,plain,
( sdtmndtplgtdt0(xc,xR,xb)
| xc = xb ),
inference(forward_demodulation,[status(thm)],[f445,f457]) ).
fof(f470,plain,
sdtmndtplgtdt0(xc,xR,xb),
inference(forward_subsumption_resolution,[status(thm)],[f469,f314]) ).
fof(f475,plain,
( sP2_prd(xb)
| ~ aElement0(xb) ),
inference(resolution,[status(thm)],[f470,f238]) ).
fof(f480,plain,
sP2_prd(xb),
inference(forward_subsumption_resolution,[status(thm)],[f475,f116]) ).
fof(f484,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f480,f347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM022+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n013.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 14:14:57 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.40 % Drodi V4.1.1
% 0.14/5.42 % Refutation found
% 0.14/5.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/5.44 % Elapsed time: 0.053697 seconds
% 0.14/5.44 % CPU time: 0.163904 seconds
% 0.14/5.44 % Total memory used: 56.782 MB
% 0.14/5.44 % Net memory used: 56.661 MB
%------------------------------------------------------------------------------