%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU186+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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.26s 0.56s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 10
% Syntax : Number of formulae : 54 ( 11 unt; 3 def)
% Number of atoms : 212 ( 85 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 255 ( 97 ~; 92 |; 45 &)
% ( 13 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 4 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 121 ( 103 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( relation(A)
<=> ! [B] :
~ ( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ( A = empty_set
=> ( B = set_meet(A)
<=> B = empty_set ) )
& ( A != empty_set
=> ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(D,A)
=> in(C,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,conjecture,
! [A] :
( relation(A)
=> ( ! [B,C] : ~ in(ordered_pair(B,C),A)
=> A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f148,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( ! [B,C] : ~ in(ordered_pair(B,C),A)
=> A = empty_set ) ),
inference(negated_conjecture,[status(cth)],[f147]) ).
fof(f166,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f167,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f180,plain,
! [A] :
( relation(A)
<=> ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f181,plain,
! [A] :
( ( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(NNF_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
( ! [A] :
( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ! [A] :
( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(miniscoping,[status(thm)],[f181]) ).
fof(f183,plain,
( ! [A] :
( ( ! [C,D] : sK2_skl(A) != ordered_pair(C,D)
& in(sK2_skl(A),A) )
| relation(A) )
& ! [A] :
( ! [B] :
( B = ordered_pair(sK0_skl(B,A),sK1_skl(B,A))
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A)),skolemize(B,sK2_skl(A))],[f182]) ).
fof(f184,plain,
! [X0,X1] :
( X1 = ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0))
| ~ in(X1,X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f187,plain,
! [A,B] :
( ( ( B = set_meet(A)
<=> B = empty_set )
| A != empty_set )
& ( ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(C,D)
| ~ in(D,A) ) ) )
| A = empty_set ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f188,plain,
! [A,B] :
( ( ( ( B != empty_set
| B = set_meet(A) )
& ( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ( ( ( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ( ! [C] :
( ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f187]) ).
fof(f189,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(miniscoping,[status(thm)],[f188]) ).
fof(f190,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( in(sK4_skl(B,A),D)
| ~ in(D,A) )
| in(sK4_skl(B,A),B) )
& ( ( ~ in(sK4_skl(B,A),sK5_skl(B,A))
& in(sK5_skl(B,A),A) )
| ~ in(sK4_skl(B,A),B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ( ~ in(C,sK3_skl(C,B,A))
& in(sK3_skl(C,B,A),A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(D,sK3_skl(C,B,A)),skolemize(C,sK4_skl(B,A)),skolemize(D,sK5_skl(B,A))],[f189]) ).
fof(f192,plain,
! [X0,X1,X2] :
( in(sK3_skl(X2,X1,X0),X0)
| in(X2,X1)
| X1 != set_meet(X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f199,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f200,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f201,plain,
( ! [A,B] :
( ( ( sK6_skl(B,A) = A
| in(sK6_skl(B,A),B) )
& ( sK6_skl(B,A) != A
| ~ in(sK6_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(C,sK6_skl(B,A))],[f200]) ).
fof(f203,plain,
! [X0,X1,X2] :
( X2 != X1
| in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f361,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f434,plain,
( relation(sK40_skl)
& ~ empty(sK40_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(A,sK40_skl)],[f87]) ).
fof(f435,plain,
~ empty(sK40_skl),
inference(cnf_transformation,[status(thm)],[f434]) ).
fof(f592,plain,
? [A] :
( A != empty_set
& ! [B,C] : ~ in(ordered_pair(B,C),A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f148]) ).
fof(f593,plain,
( sK47_skl != empty_set
& ! [B,C] : ~ in(ordered_pair(B,C),sK47_skl)
& relation(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl]),skolemize(A,sK47_skl)],[f592]) ).
fof(f594,plain,
relation(sK47_skl),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f595,plain,
! [X0,X1] : ~ in(ordered_pair(X0,X1),sK47_skl),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f596,plain,
sK47_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f653,plain,
! [X0,X1] :
( in(sK3_skl(X1,set_meet(X0),X0),X0)
| in(X1,set_meet(X0))
| X0 = empty_set ),
inference(destructive_equality_resolution,[status(thm)],[f192]) ).
fof(f658,plain,
! [X0] : in(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f203]) ).
fof(f715,plain,
! [X0] : ~ in(singleton(X0),X0),
inference(resolution,[status(thm)],[f658,f167]) ).
fof(f737,plain,
! [X0] :
( in(sK3_skl(singleton(set_meet(X0)),set_meet(X0),X0),X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f715,f653]) ).
fof(f741,plain,
! [X0] :
( sK3_skl(singleton(set_meet(X0)),set_meet(X0),X0) = ordered_pair(sK0_skl(sK3_skl(singleton(set_meet(X0)),set_meet(X0),X0),X0),sK1_skl(sK3_skl(singleton(set_meet(X0)),set_meet(X0),X0),X0))
| ~ relation(X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f737,f184]) ).
fof(f836,plain,
( sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl) = ordered_pair(sK0_skl(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl))
| sK47_skl = empty_set ),
inference(resolution,[status(thm)],[f741,f594]) ).
fof(f840,definition,
( sQ17_spl
<=> sK40_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( ~ sQ17_spl
| sK40_skl = empty_set ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f858,definition,
( sQ22_spl
<=> sK47_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f859,plain,
( ~ sQ22_spl
| sK47_skl = empty_set ),
inference(component_clause,[status(thm)],[f858]) ).
fof(f861,definition,
( sQ23_spl
<=> sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl) = ordered_pair(sK0_skl(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f862,plain,
( ~ sQ23_spl
| sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl) = ordered_pair(sK0_skl(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl)) ),
inference(component_clause,[status(thm)],[f861]) ).
fof(f864,plain,
( sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f836,f858,f861]) ).
fof(f865,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f859,f596]) ).
fof(f866,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f865]) ).
fof(f870,plain,
( ~ sQ17_spl
| ~ empty(empty_set) ),
inference(backward_demodulation,[status(thm)],[f841,f435]) ).
fof(f871,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f870,f361]) ).
fof(f872,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f871]) ).
fof(f896,plain,
( ~ sQ23_spl
| ~ in(sK3_skl(singleton(set_meet(sK47_skl)),set_meet(sK47_skl),sK47_skl),sK47_skl) ),
inference(paramodulation,[status(thm)],[f862,f595]) ).
fof(f897,plain,
( ~ sQ23_spl
| sK47_skl = empty_set ),
inference(resolution,[status(thm)],[f896,f737]) ).
fof(f898,plain,
( ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f897,f858,f861]) ).
fof(f899,plain,
$false,
inference(sat_refutation,[status(thm)],[f864,f866,f872,f898]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU186+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n015.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 05:58:36 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 0.26/0.56 % Refutation found
% 0.26/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.26/0.58 % Elapsed time: 0.118176 seconds
% 0.26/0.58 % CPU time: 0.551472 seconds
% 0.26/0.58 % Total memory used: 117.997 MB
% 0.26/0.58 % Net memory used: 117.268 MB
%------------------------------------------------------------------------------