%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU188+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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.09s 0.38s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 56 ( 16 unt; 5 def)
% Number of atoms : 118 ( 34 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 107 ( 45 ~; 42 |; 8 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-1 aty)
% Number of variables : 16 ( 13 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f20,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_dom(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( ( relation(A)
& ~ empty(A) )
=> ~ empty(relation_rng(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,conjecture,
! [A] :
( relation(A)
=> ( ( relation_rng(A) = empty_set
| relation_dom(A) = empty_set )
=> A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( ( relation_rng(A) = empty_set
| relation_dom(A) = empty_set )
=> A = empty_set ) ),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f33,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,plain,
! [A] :
( ~ empty(relation_dom(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f67,plain,
! [X0] :
( ~ empty(relation_dom(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [A] :
( ~ empty(relation_rng(A))
| ~ relation(A)
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f69,plain,
! [X0] :
( ~ empty(relation_rng(X0))
| ~ relation(X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f76,plain,
( relation(sK7_skl)
& empty(sK7_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f24]) ).
fof(f77,plain,
empty(sK7_skl),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
empty(sK8_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f25]) ).
fof(f80,plain,
empty(sK8_skl),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f93,plain,
? [A] :
( A != empty_set
& ( relation_rng(A) = empty_set
| relation_dom(A) = empty_set )
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f94,plain,
( sK13_skl != empty_set
& ( relation_rng(sK13_skl) = empty_set
| relation_dom(sK13_skl) = empty_set )
& relation(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f93]) ).
fof(f95,plain,
relation(sK13_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
( relation_rng(sK13_skl) = empty_set
| relation_dom(sK13_skl) = empty_set ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f97,plain,
sK13_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f99,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f106,definition,
( sQ0_spl
<=> relation_dom(sK13_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f107,plain,
( ~ sQ0_spl
| relation_dom(sK13_skl) = empty_set ),
inference(component_clause,[status(thm)],[f106]) ).
fof(f109,definition,
( sQ1_spl
<=> relation_rng(sK13_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f110,plain,
( ~ sQ1_spl
| relation_rng(sK13_skl) = empty_set ),
inference(component_clause,[status(thm)],[f109]) ).
fof(f112,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f96,f106,f109]) ).
fof(f122,definition,
( sQ2_spl
<=> empty(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f123,plain,
( ~ sQ2_spl
| empty(sK13_skl) ),
inference(component_clause,[status(thm)],[f122]) ).
fof(f140,plain,
sK7_skl = empty_set,
inference(resolution,[status(thm)],[f77,f99]) ).
fof(f142,plain,
sK8_skl = empty_set,
inference(resolution,[status(thm)],[f80,f99]) ).
fof(f144,plain,
( ~ sQ0_spl
| relation_dom(sK13_skl) = sK7_skl ),
inference(backward_demodulation,[status(thm)],[f140,f107]) ).
fof(f145,plain,
! [X0] :
( X0 = sK7_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f140,f99]) ).
fof(f148,plain,
sK13_skl != sK7_skl,
inference(backward_demodulation,[status(thm)],[f140,f97]) ).
fof(f149,plain,
sK8_skl = empty_set,
inference(backward_demodulation,[status(thm)],[f152,f140]) ).
fof(f152,plain,
sK8_skl = sK7_skl,
inference(forward_demodulation,[status(thm)],[f140,f142]) ).
fof(f153,plain,
sK13_skl != sK8_skl,
inference(forward_demodulation,[status(thm)],[f152,f148]) ).
fof(f162,plain,
( ~ sQ0_spl
| relation_dom(sK13_skl) = sK8_skl ),
inference(forward_demodulation,[status(thm)],[f152,f144]) ).
fof(f166,definition,
( sQ5_spl
<=> relation(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( sQ5_spl
| ~ relation(sK13_skl) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f177,definition,
( sQ8_spl
<=> empty(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( sQ8_spl
| ~ empty(sK8_skl) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f181,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f168,f95]) ).
fof(f182,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f181]) ).
fof(f184,plain,
( ~ sQ1_spl
| relation_rng(sK13_skl) = sK8_skl ),
inference(forward_demodulation,[status(thm)],[f149,f110]) ).
fof(f189,plain,
! [X0] :
( X0 = sK8_skl
| ~ empty(X0) ),
inference(forward_demodulation,[status(thm)],[f152,f145]) ).
fof(f203,plain,
( ~ sQ1_spl
| ~ empty(sK8_skl)
| ~ relation(sK13_skl)
| empty(sK13_skl) ),
inference(paramodulation,[status(thm)],[f184,f69]) ).
fof(f204,plain,
( ~ sQ1_spl
| ~ sQ8_spl
| ~ sQ5_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f203,f122,f166,f177,f109]) ).
fof(f205,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f179,f80]) ).
fof(f206,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f205]) ).
fof(f210,plain,
( ~ sQ0_spl
| ~ empty(sK8_skl)
| ~ relation(sK13_skl)
| empty(sK13_skl) ),
inference(paramodulation,[status(thm)],[f162,f67]) ).
fof(f215,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| ~ sQ5_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f210,f122,f166,f177,f106]) ).
fof(f221,plain,
( ~ sQ2_spl
| sK13_skl = sK8_skl ),
inference(resolution,[status(thm)],[f123,f189]) ).
fof(f223,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f221,f153]) ).
fof(f224,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f223]) ).
fof(f225,plain,
$false,
inference(sat_refutation,[status(thm)],[f112,f182,f204,f206,f215,f224]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU188+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:01:44 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.38 % Refutation found
% 0.09/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.41 % Elapsed time: 0.040159 seconds
% 0.09/0.41 % CPU time: 0.078020 seconds
% 0.09/0.41 % Total memory used: 16.138 MB
% 0.09/0.41 % Net memory used: 16.121 MB
%------------------------------------------------------------------------------