%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU187+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:19:35 PM UTC 2026
% Result : Theorem 0.10s 0.45s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 10
% Syntax : Number of formulae : 48 ( 4 unt; 5 def)
% Number of atoms : 172 ( 46 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 196 ( 72 ~; 84 |; 24 &)
% ( 14 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-3 aty)
% Number of variables : 91 ( 73 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,conjecture,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,negated_conjecture,
~ ( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
inference(negated_conjecture,[status(cth)],[f151]) ).
fof(f209,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f210,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f209]) ).
fof(f211,plain,
( ! [A] :
( in(sK7_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f210]) ).
fof(f212,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f271,plain,
! [A] :
( ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f272,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f271]) ).
fof(f273,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f272]) ).
fof(f274,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK19_skl(B,A),sK20_skl(B,A)),A)
| in(sK19_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK19_skl(B,A),D),A)
| ~ in(sK19_skl(B,A),B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(C,sK18_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(D,sK18_skl(C,B,A)),skolemize(C,sK19_skl(B,A)),skolemize(D,sK20_skl(B,A))],[f273]) ).
fof(f278,plain,
! [X0,X1] :
( in(ordered_pair(sK19_skl(X1,X0),sK20_skl(X1,X0)),X0)
| in(sK19_skl(X1,X0),X1)
| X1 = relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f298,plain,
! [A] :
( ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f299,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f299]) ).
fof(f301,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK27_skl(B,A),sK26_skl(B,A)),A)
| in(sK26_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK26_skl(B,A)),A)
| ~ in(sK26_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK25_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl,sK27_skl]),skolemize(D,sK25_skl(C,B,A)),skolemize(C,sK26_skl(B,A)),skolemize(D,sK27_skl(B,A))],[f300]) ).
fof(f305,plain,
! [X0,X1] :
( in(ordered_pair(sK27_skl(X1,X0),sK26_skl(X1,X0)),X0)
| in(sK26_skl(X1,X0),X1)
| X1 = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f377,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f605,plain,
( relation_rng(empty_set) != empty_set
| relation_dom(empty_set) != empty_set ),
inference(pre_NNF_transformation,[status(thm)],[f152]) ).
fof(f606,plain,
( relation_rng(empty_set) != empty_set
| relation_dom(empty_set) != empty_set ),
inference(cnf_transformation,[status(thm)],[f605]) ).
fof(f657,definition,
( sQ0_spl
<=> relation_dom(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( sQ0_spl
| relation_dom(empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f657]) ).
fof(f660,definition,
( sQ1_spl
<=> relation_rng(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f662,plain,
( sQ1_spl
| relation_rng(empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f660]) ).
fof(f663,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f606,f657,f660]) ).
fof(f673,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f212]) ).
fof(f857,plain,
! [X0] :
( in(sK19_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f278,f673]) ).
fof(f860,definition,
( sQ7_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f862,plain,
( sQ7_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f860]) ).
fof(f863,definition,
! [X0] :
( sQ8_spl
<=> ( in(sK19_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f864,plain,
! [X0] :
( ~ sQ8_spl
| in(sK19_skl(X0,empty_set),X0)
| X0 = relation_dom(empty_set) ),
inference(component_clause,[status(thm)],[f863]) ).
fof(f866,plain,
( sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f857,f860,f863]) ).
fof(f867,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f862,f377]) ).
fof(f868,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f867]) ).
fof(f884,plain,
! [X0] :
( in(sK26_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f305,f673]) ).
fof(f887,definition,
! [X0] :
( sQ9_spl
<=> ( in(sK26_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f888,plain,
! [X0] :
( ~ sQ9_spl
| in(sK26_skl(X0,empty_set),X0)
| X0 = relation_rng(empty_set) ),
inference(component_clause,[status(thm)],[f887]) ).
fof(f890,plain,
( sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f884,f860,f887]) ).
fof(f910,plain,
( ~ sQ8_spl
| empty_set = relation_dom(empty_set) ),
inference(resolution,[status(thm)],[f864,f673]) ).
fof(f913,plain,
( ~ sQ8_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f910,f659]) ).
fof(f914,plain,
( ~ sQ8_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f913]) ).
fof(f923,plain,
( ~ sQ9_spl
| empty_set = relation_rng(empty_set) ),
inference(resolution,[status(thm)],[f888,f673]) ).
fof(f926,plain,
( ~ sQ9_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f662]) ).
fof(f927,plain,
( ~ sQ9_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f926]) ).
fof(f928,plain,
$false,
inference(sat_refutation,[status(thm)],[f663,f866,f868,f890,f914,f927]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU187+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n014.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 05:56:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.45 % Refutation found
% 0.10/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.48 % Elapsed time: 0.111018 seconds
% 0.10/0.48 % CPU time: 0.516355 seconds
% 0.10/0.48 % Total memory used: 120.622 MB
% 0.10/0.48 % Net memory used: 119.546 MB
%------------------------------------------------------------------------------