%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET121-7 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:09:26 PM UTC 2026
% Result : Unsatisfiable 4.70s 1.06s
% Output : CNFRefutation 4.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of formulae : 93 ( 26 unt; 11 def)
% Number of atoms : 185 ( 53 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 154 ( 62 ~; 81 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 12 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 62 ( 62 !; 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(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U,V,X,Y] :
( member(V,Y)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
member(null_class,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [X] : member(singleton(X),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [Y,Z,X] :
( X = Z
| X = Y
| ~ member(X,universal_class)
| unordered_pair(Y,Z) != singleton(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [X,Y] : member(ordered_pair(X,Y),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,axiom,
! [X] :
( first(X) = X
| member(ordered_pair(first(X),second(X)),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,axiom,
! [X] :
( second(X) = X
| member(ordered_pair(first(X),second(X)),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,axiom,
! [X] :
( first(X) = X
| ordered_pair(first(X),second(X)) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,axiom,
! [X] :
( second(X) = X
| ordered_pair(first(X),second(X)) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,negated_conjecture,
~ member(y,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,negated_conjecture,
first(ordered_pair(x,y)) != ordered_pair(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f171,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f174,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f185,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f189,plain,
! [V,Y] :
( member(V,Y)
| ! [U,X] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f190,plain,
! [X0,X1,X2,X3] :
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f295,plain,
member(null_class,universal_class),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f316,plain,
! [X0] : member(singleton(X0),universal_class),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f325,plain,
! [Z,X] :
( X = Z
| ! [Y] :
( X = Y
| ~ member(X,universal_class)
| unordered_pair(Y,Z) != singleton(X) ) ),
inference(miniscoping,[status(thm)],[f129]) ).
fof(f326,plain,
! [X0,X1,X2] :
( X2 = X1
| X2 = X0
| ~ member(X2,universal_class)
| unordered_pair(X0,X1) != singleton(X2) ),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f342,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f356,plain,
! [X0] :
( first(X0) = X0
| member(ordered_pair(first(X0),second(X0)),cross_product(universal_class,universal_class)) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f357,plain,
! [X0] :
( second(X0) = X0
| member(ordered_pair(first(X0),second(X0)),cross_product(universal_class,universal_class)) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f358,plain,
! [X0] :
( first(X0) = X0
| ordered_pair(first(X0),second(X0)) = X0 ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f359,plain,
! [X0] :
( second(X0) = X0
| ordered_pair(first(X0),second(X0)) = X0 ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f372,plain,
~ member(y,universal_class),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f373,plain,
first(ordered_pair(x,y)) != ordered_pair(x,y),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f389,definition,
( sQ2_spl
<=> member(ordered_pair(x,y),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f391,plain,
( sQ2_spl
| ~ member(ordered_pair(x,y),universal_class) ),
inference(component_clause,[status(thm)],[f389]) ).
fof(f403,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f391,f342]) ).
fof(f404,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f403]) ).
fof(f405,plain,
! [X0] :
( ~ member(y,X0)
| ~ subclass(X0,universal_class) ),
inference(resolution,[status(thm)],[f171,f372]) ).
fof(f406,plain,
! [X0] : ~ member(y,X0),
inference(forward_subsumption_resolution,[status(thm)],[f405,f174]) ).
fof(f419,plain,
! [X0] :
( ordered_pair(x,y) = X0
| ~ member(ordered_pair(x,y),universal_class)
| unordered_pair(first(ordered_pair(x,y)),X0) != singleton(ordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f326,f373]) ).
fof(f427,definition,
! [X0] :
( sQ6_spl
<=> ( ordered_pair(x,y) = X0
| unordered_pair(first(ordered_pair(x,y)),X0) != singleton(ordered_pair(x,y)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f428,plain,
! [X0] :
( ~ sQ6_spl
| ordered_pair(x,y) = X0
| unordered_pair(first(ordered_pair(x,y)),X0) != singleton(ordered_pair(x,y)) ),
inference(component_clause,[status(thm)],[f427]) ).
fof(f430,plain,
( ~ sQ2_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f419,f427,f389]) ).
fof(f509,plain,
! [X0] :
( first(X0) = X0
| first(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f358,f356]) ).
fof(f510,plain,
! [X0] :
( first(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(duplicate_literals_removal,[status(thm)],[f509]) ).
fof(f511,plain,
! [X0] :
( second(X0) = X0
| second(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f359,f357]) ).
fof(f513,plain,
! [X0] :
( second(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(duplicate_literals_removal,[status(thm)],[f511]) ).
fof(f548,definition,
( sQ18_spl
<=> second(ordered_pair(x,y)) = ordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f549,plain,
( ~ sQ18_spl
| second(ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f550,plain,
( sQ18_spl
| second(ordered_pair(x,y)) != ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f552,definition,
( sQ19_spl
<=> first(ordered_pair(x,y)) = ordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f553,plain,
( ~ sQ19_spl
| first(ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f552]) ).
fof(f684,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f553,f373]) ).
fof(f685,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f684]) ).
fof(f694,definition,
( sQ31_spl
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f696,plain,
( sQ31_spl
| ~ member(null_class,universal_class) ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f768,definition,
( sQ39_spl
<=> member(ordered_pair(y,y),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f770,plain,
( sQ39_spl
| ~ member(ordered_pair(y,y),universal_class) ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f791,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f770,f342]) ).
fof(f792,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f791]) ).
fof(f961,definition,
( sQ48_spl
<=> member(singleton(null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f963,plain,
( sQ48_spl
| ~ member(singleton(null_class),universal_class) ),
inference(component_clause,[status(thm)],[f961]) ).
fof(f972,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f696,f295]) ).
fof(f973,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f972]) ).
fof(f974,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f963,f316]) ).
fof(f975,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f974]) ).
fof(f978,plain,
( ~ sQ18_spl
| first(ordered_pair(x,y)) = ordered_pair(x,y)
| member(ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)),cross_product(universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f549,f356]) ).
fof(f980,plain,
( ~ sQ18_spl
| first(ordered_pair(x,y)) = ordered_pair(x,y)
| ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(paramodulation,[status(thm)],[f549,f358]) ).
fof(f981,definition,
( sQ51_spl
<=> member(ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)),cross_product(universal_class,universal_class)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( ~ sQ51_spl
| member(ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)),cross_product(universal_class,universal_class)) ),
inference(component_clause,[status(thm)],[f981]) ).
fof(f985,plain,
( ~ sQ18_spl
| sQ19_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f978,f981,f552,f548]) ).
fof(f986,definition,
( sQ52_spl
<=> ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)) = ordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f987,plain,
( ~ sQ52_spl
| ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f986]) ).
fof(f990,plain,
( ~ sQ18_spl
| sQ19_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f980,f986,f552,f548]) ).
fof(f997,plain,
( ~ sQ6_spl
| sQ18_spl
| unordered_pair(first(ordered_pair(x,y)),second(ordered_pair(x,y))) != singleton(ordered_pair(x,y)) ),
inference(resolution,[status(thm)],[f550,f428]) ).
fof(f1032,plain,
( ~ sQ51_spl
| ~ sQ52_spl
| member(ordered_pair(x,y),cross_product(universal_class,universal_class)) ),
inference(backward_demodulation,[status(thm)],[f987,f982]) ).
fof(f1257,definition,
( sQ82_spl
<=> member(singleton(ordered_pair(x,y)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1259,plain,
( sQ82_spl
| ~ member(singleton(ordered_pair(x,y)),universal_class) ),
inference(component_clause,[status(thm)],[f1257]) ).
fof(f1277,definition,
( sQ87_spl
<=> member(singleton(first(ordered_pair(x,y))),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1279,plain,
( sQ87_spl
| ~ member(singleton(first(ordered_pair(x,y))),universal_class) ),
inference(component_clause,[status(thm)],[f1277]) ).
fof(f1286,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1259,f316]) ).
fof(f1287,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f1286]) ).
fof(f1314,plain,
( sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1279,f316]) ).
fof(f1315,plain,
sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1314]) ).
fof(f3368,plain,
! [X0,X1,X2] : ~ member(ordered_pair(X0,y),cross_product(X1,X2)),
inference(resolution,[status(thm)],[f190,f406]) ).
fof(f3370,plain,
( ~ sQ51_spl
| ~ sQ52_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1032,f3368]) ).
fof(f3371,plain,
( ~ sQ51_spl
| ~ sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f3370]) ).
fof(f5558,plain,
! [X0] : second(ordered_pair(X0,y)) = ordered_pair(X0,y),
inference(resolution,[status(thm)],[f3368,f513]) ).
fof(f5559,plain,
! [X0] : first(ordered_pair(X0,y)) = ordered_pair(X0,y),
inference(resolution,[status(thm)],[f3368,f510]) ).
fof(f5567,plain,
( ~ sQ6_spl
| sQ18_spl
| unordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)) != singleton(ordered_pair(x,y)) ),
inference(backward_demodulation,[status(thm)],[f5558,f997]) ).
fof(f5695,plain,
( ~ sQ6_spl
| sQ18_spl
| unordered_pair(ordered_pair(x,y),ordered_pair(x,y)) != singleton(ordered_pair(x,y)) ),
inference(forward_demodulation,[status(thm)],[f5559,f5567]) ).
fof(f5696,plain,
( ~ sQ6_spl
| sQ18_spl
| singleton(ordered_pair(x,y)) != singleton(ordered_pair(x,y)) ),
inference(forward_demodulation,[status(thm)],[f185,f5695]) ).
fof(f5697,plain,
( ~ sQ6_spl
| sQ18_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5696]) ).
fof(f5698,plain,
( ~ sQ6_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f5697]) ).
fof(f5699,plain,
$false,
inference(sat_refutation,[status(thm)],[f404,f430,f685,f792,f973,f975,f985,f990,f1287,f1315,f3371,f5698]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET121-7 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n008.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 04:55:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 4.70/1.06 % Refutation found
% 4.70/1.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.70/1.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.70/1.10 % Elapsed time: 0.727931 seconds
% 4.70/1.10 % CPU time: 5.350158 seconds
% 4.70/1.10 % Total memory used: 159.999 MB
% 4.70/1.10 % Net memory used: 154.163 MB
%------------------------------------------------------------------------------