%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM066-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 01:38:36 PM UTC 2026
% Result : Unsatisfiable 4.80s 6.45s
% Output : CNFRefutation 1.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 18
% Syntax : Number of formulae : 64 ( 18 unt; 7 def)
% Number of atoms : 142 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 158 ( 80 ~; 71 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 8 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 61 ( 61 !; 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(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U,X,V,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X,Y] :
( member(ordered_pair(X,Y),element_relation)
| ~ member(X,Y)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
inductive(omega),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [Xr,Y,U,V] :
( member(least(Xr,U),U)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [Xr,Y,U,V] :
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,negated_conjecture,
well_ordering(element_relation,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,negated_conjecture,
subclass(u,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,negated_conjecture,
member(v,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,negated_conjecture,
member(v,least(element_relation,u)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f164,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f167,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(X0,X2),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f189,plain,
! [X0,X1] :
( member(ordered_pair(X0,X1),element_relation)
| ~ member(X0,X1)
| ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class)) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f221,plain,
inductive(omega),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f307,plain,
! [Xr,U] :
( member(least(Xr,U),U)
| ! [V] : ~ member(V,U)
| ! [Y] :
( ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ) ),
inference(miniscoping,[status(thm)],[f125]) ).
fof(f308,plain,
! [X0,X1,X2,X3] :
( member(least(X0,X2),X2)
| ~ member(X3,X2)
| ~ subclass(X2,X1)
| ~ well_ordering(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f311,plain,
! [Xr,U,V] :
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ! [Y] :
( ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ) ),
inference(miniscoping,[status(thm)],[f127]) ).
fof(f312,plain,
! [X0,X1,X2,X3] :
( ~ member(ordered_pair(X3,least(X0,X2)),X0)
| ~ member(X3,X2)
| ~ subclass(X2,X1)
| ~ well_ordering(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f350,plain,
well_ordering(element_relation,y),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f351,plain,
subclass(u,y),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f352,plain,
member(v,u),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f353,plain,
member(v,least(element_relation,u)),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f383,plain,
! [X0,X1] :
( ~ member(ordered_pair(X1,least(element_relation,X0)),element_relation)
| ~ member(X1,X0)
| ~ subclass(X0,y) ),
inference(resolution,[status(thm)],[f312,f350]) ).
fof(f384,plain,
! [X0] :
( ~ member(ordered_pair(X0,least(element_relation,u)),element_relation)
| ~ member(X0,u) ),
inference(resolution,[status(thm)],[f383,f351]) ).
fof(f400,plain,
! [X0] :
( ~ member(X0,least(element_relation,u))
| ~ member(ordered_pair(X0,least(element_relation,u)),cross_product(universal_class,universal_class))
| ~ member(X0,u) ),
inference(resolution,[status(thm)],[f384,f189]) ).
fof(f468,definition,
( sQ7_spl
<=> inductive(omega) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( sQ7_spl
| ~ inductive(omega) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f680,plain,
! [X0] :
( ~ member(X0,least(element_relation,u))
| ~ member(X0,u)
| ~ member(least(element_relation,u),universal_class)
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f184,f400]) ).
fof(f683,definition,
! [X0] :
( sQ17_spl
<=> ( ~ member(X0,least(element_relation,u))
| ~ member(X0,u)
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f684,plain,
! [X0] :
( ~ sQ17_spl
| ~ member(X0,least(element_relation,u))
| ~ member(X0,u)
| ~ member(X0,universal_class) ),
inference(component_clause,[status(thm)],[f683]) ).
fof(f686,definition,
( sQ18_spl
<=> member(least(element_relation,u),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( sQ18_spl
| ~ member(least(element_relation,u),universal_class) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,plain,
( ~ sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f680,f683,f686]) ).
fof(f723,plain,
! [X0] :
( member(v,X0)
| ~ subclass(u,X0) ),
inference(resolution,[status(thm)],[f164,f352]) ).
fof(f795,plain,
! [X0,X1] :
( member(least(element_relation,X0),X0)
| ~ member(X1,X0)
| ~ subclass(X0,y) ),
inference(resolution,[status(thm)],[f308,f350]) ).
fof(f894,definition,
( sQ31_spl
<=> member(least(element_relation,u),u) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f895,plain,
( ~ sQ31_spl
| member(least(element_relation,u),u) ),
inference(component_clause,[status(thm)],[f894]) ).
fof(f1094,plain,
member(v,universal_class),
inference(resolution,[status(thm)],[f723,f167]) ).
fof(f1098,plain,
! [X0] :
( ~ sQ31_spl
| member(least(element_relation,u),X0)
| ~ subclass(u,X0) ),
inference(resolution,[status(thm)],[f895,f164]) ).
fof(f1252,plain,
( ~ sQ31_spl
| member(least(element_relation,u),universal_class) ),
inference(resolution,[status(thm)],[f1098,f167]) ).
fof(f1255,plain,
! [X0] :
( member(least(element_relation,u),u)
| ~ member(X0,u) ),
inference(resolution,[status(thm)],[f795,f351]) ).
fof(f1257,definition,
! [X0] :
( sQ43_spl
<=> ~ member(X0,u) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1258,plain,
! [X0] :
( ~ sQ43_spl
| ~ member(X0,u) ),
inference(component_clause,[status(thm)],[f1257]) ).
fof(f1260,plain,
( sQ31_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1255,f1257,f894]) ).
fof(f1269,plain,
( ~ sQ43_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f352,f1258]) ).
fof(f1276,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f1269]) ).
fof(f1367,definition,
( sQ49_spl
<=> member(v,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1369,plain,
( sQ49_spl
| ~ member(v,universal_class) ),
inference(component_clause,[status(thm)],[f1367]) ).
fof(f1374,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1369,f1094]) ).
fof(f1375,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1374]) ).
fof(f2140,plain,
( ~ sQ17_spl
| ~ member(v,u)
| ~ member(v,universal_class) ),
inference(resolution,[status(thm)],[f684,f353]) ).
fof(f2151,definition,
( sQ87_spl
<=> member(v,u) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2153,plain,
( sQ87_spl
| ~ member(v,u) ),
inference(component_clause,[status(thm)],[f2151]) ).
fof(f2154,plain,
( ~ sQ17_spl
| ~ sQ87_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f2140,f1367,f2151,f683]) ).
fof(f2155,plain,
( sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2153,f352]) ).
fof(f2156,plain,
sQ87_spl,
inference(contradiction_clause,[status(thm)],[f2155]) ).
fof(f2193,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f470,f221]) ).
fof(f2194,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f2193]) ).
fof(f2348,plain,
( ~ sQ31_spl
| sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1252,f688]) ).
fof(f2349,plain,
( ~ sQ31_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f2348]) ).
fof(f2350,plain,
$false,
inference(sat_refutation,[status(thm)],[f689,f1260,f1276,f1375,f2154,f2156,f2194,f2349]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM066-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.66 % Computer : n017.cluster.edu
% 0.18/5.66 % Model : x86_64 x86_64
% 0.18/5.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.66 % Memory : 8046.5625MB
% 0.18/5.66 % OS : Linux 6.8.0-71-generic
% 0.18/5.66 % CPULimit : 300
% 0.18/5.66 % WCLimit : 300
% 0.18/5.66 % DateTime : Mon Sep 21 01:58:03 UTC 2026
% 0.18/5.67 % CPUTime :
% 0.18/5.69 % Drodi V4.1.1
% 4.80/6.45 % Refutation found
% 4.80/6.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.80/6.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.15/6.48 % Elapsed time: 0.796206 seconds
% 1.15/6.48 % CPU time: 5.949782 seconds
% 1.15/6.48 % Total memory used: 162.828 MB
% 1.15/6.48 % Net memory used: 155.178 MB
%------------------------------------------------------------------------------