%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET510-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:10:02 PM UTC 2026
% Result : Unsatisfiable 0.21s 20.62s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 19
% Syntax : Number of formulae : 66 ( 13 unt; 6 def)
% Number of atoms : 140 ( 34 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 130 ( 56 ~; 68 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 7 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 69 ( 69 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( X = Y
| ~ subclass(Y,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Z,X,Y] :
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( intersection(X,regular(X)) = null_class
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,negated_conjecture,
singleton(universal_class) != null_class,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f115,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f117,plain,
! [X0,X1] :
( subclass(X0,X1)
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f118,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f121,plain,
! [X0,X1] :
( X0 = X1
| ~ subclass(X1,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f122,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f123,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f129,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f141,plain,
! [Z,X] :
( member(Z,X)
| ! [Y] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f142,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f145,plain,
! [X0,X1,X2] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f174,plain,
member(omega,universal_class),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f188,plain,
! [X0] :
( member(regular(X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f189,plain,
! [X0] :
( intersection(X0,regular(X0)) = null_class
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f245,plain,
singleton(universal_class) != null_class,
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f253,plain,
! [X0,X1] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f118,f115]) ).
fof(f263,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f129,f123]) ).
fof(f264,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f263]) ).
fof(f328,plain,
! [X0] :
( regular(singleton(X0)) = X0
| singleton(X0) = null_class ),
inference(resolution,[status(thm)],[f188,f264]) ).
fof(f630,plain,
regular(singleton(universal_class)) = universal_class,
inference(resolution,[status(thm)],[f328,f245]) ).
fof(f670,definition,
( sQ30_spl
<=> singleton(universal_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f671,plain,
( ~ sQ30_spl
| singleton(universal_class) = null_class ),
inference(component_clause,[status(thm)],[f670]) ).
fof(f677,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f245]) ).
fof(f678,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f677]) ).
fof(f730,definition,
( sQ36_spl
<=> member(omega,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f732,plain,
( sQ36_spl
| ~ member(omega,universal_class) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f734,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f174]) ).
fof(f735,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f734]) ).
fof(f737,plain,
( intersection(singleton(universal_class),universal_class) = null_class
| singleton(universal_class) = null_class ),
inference(paramodulation,[status(thm)],[f630,f189]) ).
fof(f745,definition,
( sQ38_spl
<=> intersection(singleton(universal_class),universal_class) = null_class ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f746,plain,
( ~ sQ38_spl
| intersection(singleton(universal_class),universal_class) = null_class ),
inference(component_clause,[status(thm)],[f745]) ).
fof(f748,plain,
( sQ38_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f737,f670,f745]) ).
fof(f750,plain,
! [X0] :
( ~ sQ38_spl
| member(X0,null_class)
| ~ member(X0,universal_class)
| ~ member(X0,singleton(universal_class)) ),
inference(paramodulation,[status(thm)],[f746,f145]) ).
fof(f752,plain,
! [X0] :
( ~ sQ38_spl
| member(X0,singleton(universal_class))
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f746,f142]) ).
fof(f754,plain,
! [X0] :
( ~ sQ38_spl
| member(X0,null_class)
| ~ member(X0,singleton(universal_class)) ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f253]) ).
fof(f776,plain,
! [X0] :
( ~ sQ38_spl
| subclass(X0,null_class)
| ~ member(not_subclass_element(X0,null_class),singleton(universal_class)) ),
inference(resolution,[status(thm)],[f754,f117]) ).
fof(f777,plain,
! [X0] :
( ~ sQ38_spl
| subclass(X0,singleton(universal_class))
| ~ member(not_subclass_element(X0,singleton(universal_class)),null_class) ),
inference(resolution,[status(thm)],[f752,f117]) ).
fof(f816,definition,
! [X0] :
( sQ42_spl
<=> universal_class = X0 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f817,plain,
! [X0] :
( ~ sQ42_spl
| universal_class = X0 ),
inference(component_clause,[status(thm)],[f816]) ).
fof(f820,plain,
! [X0,X1] :
( ~ sQ42_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f817,f817]) ).
fof(f892,plain,
( ~ sQ42_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f245,f820]) ).
fof(f893,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f892]) ).
fof(f933,plain,
( ~ sQ38_spl
| subclass(singleton(universal_class),null_class)
| subclass(singleton(universal_class),null_class) ),
inference(resolution,[status(thm)],[f776,f116]) ).
fof(f935,definition,
( sQ43_spl
<=> subclass(singleton(universal_class),null_class) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( ~ sQ38_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f933,f935,f745]) ).
fof(f961,plain,
( ~ sQ38_spl
| subclass(null_class,singleton(universal_class))
| subclass(null_class,singleton(universal_class)) ),
inference(resolution,[status(thm)],[f777,f116]) ).
fof(f963,definition,
( sQ44_spl
<=> subclass(null_class,singleton(universal_class)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f964,plain,
( ~ sQ44_spl
| subclass(null_class,singleton(universal_class)) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,plain,
( ~ sQ38_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f961,f963,f745]) ).
fof(f1034,plain,
( ~ sQ44_spl
| singleton(universal_class) = null_class
| ~ subclass(singleton(universal_class),null_class) ),
inference(resolution,[status(thm)],[f121,f964]) ).
fof(f1043,plain,
( ~ sQ44_spl
| sQ30_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1034,f935,f670,f963]) ).
fof(f1048,plain,
$false,
inference(sat_refutation,[status(thm)],[f678,f735,f748,f893,f938,f966,f1043]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET510-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/20.46 % Computer : n019.cluster.edu
% 0.17/20.46 % Model : x86_64 x86_64
% 0.17/20.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/20.46 % Memory : 8046.5625MB
% 0.17/20.46 % OS : Linux 6.8.0-71-generic
% 0.17/20.46 % CPULimit : 300
% 0.17/20.46 % WCLimit : 300
% 0.17/20.46 % DateTime : Mon Sep 21 05:22:40 UTC 2026
% 0.17/20.46 % CPUTime :
% 0.17/20.47 % Drodi V4.1.1
% 0.21/20.62 % Refutation found
% 0.21/20.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/20.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/20.64 % Elapsed time: 0.173255 seconds
% 0.21/20.64 % CPU time: 1.013450 seconds
% 0.21/20.64 % Total memory used: 121.283 MB
% 0.21/20.64 % Net memory used: 120.206 MB
%------------------------------------------------------------------------------