%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU189+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 : n007.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.14s 0.65s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 15
% Syntax : Number of formulae : 71 ( 8 unt; 8 def)
% Number of atoms : 174 ( 51 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 178 ( 75 ~; 74 |; 11 &)
% ( 10 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 9 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 17 ( 15 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,axiom,
empty(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_rng(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,lemma,
! [A] :
( relation(A)
=> ( ( relation_rng(A) = empty_set
| relation_dom(A) = empty_set )
=> A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,conjecture,
! [A] :
( relation(A)
=> ( relation_dom(A) = empty_set
<=> relation_rng(A) = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( relation_dom(A) = empty_set
<=> relation_rng(A) = empty_set ) ),
inference(negated_conjecture,[status(cth)],[f157]) ).
fof(f368,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f384,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f66]) ).
fof(f385,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f386,plain,
! [A] :
( ~ empty(relation_rng(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f387,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f388,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f390,plain,
! [X0] :
( relation(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f615,plain,
relation_dom(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f616,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f622,plain,
! [A] :
( A = empty_set
| ( relation_rng(A) != empty_set
& relation_dom(A) != empty_set )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f156]) ).
fof(f623,plain,
! [X0] :
( X0 = empty_set
| relation_dom(X0) != empty_set
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f622]) ).
fof(f624,plain,
! [X0] :
( X0 = empty_set
| relation_rng(X0) != empty_set
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f622]) ).
fof(f625,plain,
? [A] :
( ( relation_dom(A) = empty_set
<~> relation_rng(A) = empty_set )
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f158]) ).
fof(f626,plain,
? [A] :
( ( relation_rng(A) != empty_set
| relation_dom(A) != empty_set )
& ( relation_rng(A) = empty_set
| relation_dom(A) = empty_set )
& relation(A) ),
inference(NNF_transformation,[status(thm)],[f625]) ).
fof(f627,plain,
( ( relation_rng(sK49_skl) != empty_set
| relation_dom(sK49_skl) != empty_set )
& ( relation_rng(sK49_skl) = empty_set
| relation_dom(sK49_skl) = empty_set )
& relation(sK49_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl]),skolemize(A,sK49_skl)],[f626]) ).
fof(f628,plain,
relation(sK49_skl),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f629,plain,
( relation_rng(sK49_skl) = empty_set
| relation_dom(sK49_skl) = empty_set ),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f630,plain,
( relation_rng(sK49_skl) != empty_set
| relation_dom(sK49_skl) != empty_set ),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f676,definition,
( sQ0_spl
<=> relation_dom(sK49_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f677,plain,
( ~ sQ0_spl
| relation_dom(sK49_skl) = empty_set ),
inference(component_clause,[status(thm)],[f676]) ).
fof(f678,plain,
( sQ0_spl
| relation_dom(sK49_skl) != empty_set ),
inference(component_clause,[status(thm)],[f676]) ).
fof(f679,definition,
( sQ1_spl
<=> relation_rng(sK49_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f680,plain,
( ~ sQ1_spl
| relation_rng(sK49_skl) = empty_set ),
inference(component_clause,[status(thm)],[f679]) ).
fof(f681,plain,
( sQ1_spl
| relation_rng(sK49_skl) != empty_set ),
inference(component_clause,[status(thm)],[f679]) ).
fof(f682,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f629,f676,f679]) ).
fof(f683,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f630,f676,f679]) ).
fof(f731,definition,
( sQ2_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f733,plain,
( sQ2_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f731]) ).
fof(f736,definition,
( sQ3_spl
<=> empty(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f741,plain,
( relation(empty_set)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f615,f390]) ).
fof(f742,definition,
( sQ4_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f746,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f741,f731,f742]) ).
fof(f752,plain,
( ~ sQ0_spl
| ~ empty(empty_set)
| ~ relation(sK49_skl)
| empty(sK49_skl) ),
inference(paramodulation,[status(thm)],[f677,f385]) ).
fof(f754,definition,
( sQ5_spl
<=> relation(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( sQ5_spl
| ~ relation(sK49_skl) ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f757,plain,
( ~ sQ0_spl
| ~ sQ2_spl
| ~ sQ5_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f752,f736,f754,f731,f676]) ).
fof(f759,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f756,f628]) ).
fof(f760,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f759]) ).
fof(f761,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f733,f368]) ).
fof(f762,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f761]) ).
fof(f784,plain,
( ~ sQ0_spl
| sK49_skl = empty_set
| ~ relation(sK49_skl) ),
inference(resolution,[status(thm)],[f623,f677]) ).
fof(f785,plain,
( empty_set = empty_set
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f623,f615]) ).
fof(f788,definition,
( sQ6_spl
<=> sK49_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( ~ sQ6_spl
| sK49_skl = empty_set ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f791,plain,
( ~ sQ0_spl
| sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f784,f754,f788,f676]) ).
fof(f792,definition,
( sQ7_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( sQ7_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f785,f742,f792]) ).
fof(f798,plain,
( ~ sQ1_spl
| ~ empty(empty_set)
| ~ relation(sK49_skl)
| empty(sK49_skl) ),
inference(paramodulation,[status(thm)],[f680,f387]) ).
fof(f801,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| ~ sQ5_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f798,f736,f754,f731,f679]) ).
fof(f805,plain,
( ~ sQ1_spl
| sK49_skl = empty_set
| ~ relation(sK49_skl) ),
inference(resolution,[status(thm)],[f624,f680]) ).
fof(f809,plain,
( ~ sQ1_spl
| sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f805,f754,f788,f679]) ).
fof(f815,plain,
( sQ0_spl
| ~ sQ6_spl
| relation_dom(sK49_skl) != sK49_skl ),
inference(backward_demodulation,[status(thm)],[f789,f678]) ).
fof(f819,plain,
( ~ sQ6_spl
| relation_rng(empty_set) = sK49_skl ),
inference(backward_demodulation,[status(thm)],[f789,f616]) ).
fof(f820,plain,
( ~ sQ6_spl
| relation_dom(empty_set) = sK49_skl ),
inference(backward_demodulation,[status(thm)],[f789,f615]) ).
fof(f827,plain,
( ~ sQ6_spl
| relation_rng(sK49_skl) = sK49_skl ),
inference(forward_demodulation,[status(thm)],[f789,f819]) ).
fof(f828,plain,
( ~ sQ6_spl
| relation_dom(sK49_skl) = sK49_skl ),
inference(forward_demodulation,[status(thm)],[f789,f820]) ).
fof(f861,plain,
( ~ sQ6_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f828,f815]) ).
fof(f862,plain,
( ~ sQ6_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f861]) ).
fof(f863,plain,
( sQ1_spl
| ~ sQ6_spl
| relation_rng(sK49_skl) != sK49_skl ),
inference(forward_demodulation,[status(thm)],[f789,f681]) ).
fof(f871,plain,
( sQ1_spl
| ~ sQ6_spl
| sK49_skl != sK49_skl ),
inference(forward_demodulation,[status(thm)],[f827,f863]) ).
fof(f872,plain,
( sQ1_spl
| ~ sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f871]) ).
fof(f873,plain,
( sQ1_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f872]) ).
fof(f874,plain,
$false,
inference(sat_refutation,[status(thm)],[f682,f683,f746,f757,f760,f762,f791,f795,f801,f809,f862,f873]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU189+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.61 % Computer : n007.cluster.edu
% 0.14/0.61 % Model : x86_64 x86_64
% 0.14/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.61 % Memory : 8046.5625MB
% 0.14/0.61 % OS : Linux 6.8.0-71-generic
% 0.14/0.61 % CPULimit : 300
% 0.14/0.61 % WCLimit : 300
% 0.14/0.61 % DateTime : Mon Sep 21 05:54:21 UTC 2026
% 0.14/0.62 % CPUTime :
% 0.14/0.63 % Drodi V4.1.1
% 0.14/0.65 % Refutation found
% 0.14/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.18/0.72 % Elapsed time: 0.094993 seconds
% 0.18/0.72 % CPU time: 0.161539 seconds
% 0.18/0.72 % Total memory used: 64.102 MB
% 0.18/0.72 % Net memory used: 63.996 MB
%------------------------------------------------------------------------------