%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG091+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 02:04:56 PM UTC 2026
% Result : Theorem 0.10s 0.41s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 26 ( 11 unt; 1 def)
% Number of atoms : 87 ( 19 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 107 ( 46 ~; 36 |; 24 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 28 ( 18 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,hypothesis,
( aElementOf0(sdtpldt0(xl,xn),xJ)
& aElementOf0(sdtpldt0(xk,xm),xI) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
( aElementOf0(sdtasdt0(xz,xl),xJ)
& aElementOf0(sdtasdt0(xz,xk),xI) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
sdtasdt0(xz,xx) = sdtpldt0(sdtasdt0(xz,xk),sdtasdt0(xz,xl)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,conjecture,
( ( aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = sdtasdt0(xz,xx)
& aElementOf0(W1,xJ)
& aElementOf0(W0,xI) ) )
& ( aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(xx,xy)
& aElementOf0(W1,xJ)
& aElementOf0(W0,xI) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ ( ( aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = sdtasdt0(xz,xx)
& aElementOf0(W1,xJ)
& aElementOf0(W0,xI) ) )
& ( aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(xx,xy)
& aElementOf0(W1,xJ)
& aElementOf0(W0,xI) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f145,plain,
aElementOf0(sdtpldt0(xk,xm),xI),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f146,plain,
aElementOf0(sdtpldt0(xl,xn),xJ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f147,plain,
aElementOf0(sdtasdt0(xz,xk),xI),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f148,plain,
aElementOf0(sdtasdt0(xz,xl),xJ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f149,plain,
sdtpldt0(xx,xy) = sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f150,plain,
sdtasdt0(xz,xx) = sdtpldt0(sdtasdt0(xz,xk),sdtasdt0(xz,xl)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f151,plain,
( ( ~ aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != sdtasdt0(xz,xx)
| ~ aElementOf0(W1,xJ)
| ~ aElementOf0(W0,xI) ) )
| ( ~ aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != sdtpldt0(xx,xy)
| ~ aElementOf0(W1,xJ)
| ~ aElementOf0(W0,xI) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f152,definition,
( sP2_prd
<=> ( ~ aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != sdtpldt0(xx,xy)
| ~ aElementOf0(W1,xJ)
| ~ aElementOf0(W0,xI) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f153,plain,
( ( ~ aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != sdtasdt0(xz,xx)
| ~ aElementOf0(W1,xJ)
| ~ aElementOf0(W0,xI) ) )
| sP2_prd ),
inference(formula_renaming,[status(thm)],[f151,f152]) ).
fof(f154,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) != sdtasdt0(xz,xx)
| ~ aElementOf0(X1,xJ)
| ~ aElementOf0(X0,xI)
| sP2_prd ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f167,plain,
( ( aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
| ? [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(xx,xy)
& aElementOf0(W1,xJ)
& aElementOf0(W0,xI) )
| sP2_prd )
& ( ( ~ aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != sdtpldt0(xx,xy)
| ~ aElementOf0(W1,xJ)
| ~ aElementOf0(W0,xI) ) )
| ~ sP2_prd ) ),
inference(NNF_transformation,[status(thm)],[f152]) ).
fof(f168,plain,
( ( aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
| ( sdtpldt0(sK15_skl,sK16_skl) = sdtpldt0(xx,xy)
& aElementOf0(sK16_skl,xJ)
& aElementOf0(sK15_skl,xI) )
| sP2_prd )
& ( ( ~ aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))
& ! [W0,W1] :
( sdtpldt0(W0,W1) != sdtpldt0(xx,xy)
| ~ aElementOf0(W1,xJ)
| ~ aElementOf0(W0,xI) ) )
| ~ sP2_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(W0,sK15_skl),skolemize(W1,sK16_skl)],[f167]) ).
fof(f169,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) != sdtpldt0(xx,xy)
| ~ aElementOf0(X1,xJ)
| ~ aElementOf0(X0,xI)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f423,plain,
( ~ aElementOf0(sdtpldt0(xl,xn),xJ)
| ~ aElementOf0(sdtpldt0(xk,xm),xI)
| ~ sP2_prd ),
inference(resolution,[status(thm)],[f149,f169]) ).
fof(f436,plain,
( ~ aElementOf0(sdtpldt0(xl,xn),xJ)
| ~ sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f423,f145]) ).
fof(f457,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) != sdtasdt0(xz,xx)
| ~ aElementOf0(X1,xJ)
| ~ aElementOf0(X0,xI) ),
inference(backward_subsumption_resolution,[status(thm)],[f154,f459]) ).
fof(f459,plain,
~ sP2_prd,
inference(forward_subsumption_resolution,[status(thm)],[f436,f146]) ).
fof(f515,plain,
( ~ aElementOf0(sdtasdt0(xz,xl),xJ)
| ~ aElementOf0(sdtasdt0(xz,xk),xI) ),
inference(resolution,[status(thm)],[f457,f150]) ).
fof(f520,plain,
~ aElementOf0(sdtasdt0(xz,xl),xJ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f147]) ).
fof(f525,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f520,f148]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG091+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 04:19:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.43 % Elapsed time: 0.061291 seconds
% 0.10/0.43 % CPU time: 0.233630 seconds
% 0.10/0.43 % Total memory used: 84.704 MB
% 0.10/0.43 % Net memory used: 84.462 MB
%------------------------------------------------------------------------------