%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET119-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 : n006.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:25 PM UTC 2026
% Result : Unsatisfiable 7.41s 1.48s
% Output : CNFRefutation 7.41s
% 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(f14,axiom,
! [U,V,X,Y] :
( member(U,X)
| ~ 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(f166,negated_conjecture,
~ member(x,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,negated_conjecture,
first(ordered_pair(x,y)) != ordered_pair(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f169,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f172,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f183,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f185,plain,
! [U,X] :
( member(U,X)
| ! [V,Y] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f186,plain,
! [X0,X1,X2,X3] :
( member(X0,X2)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f293,plain,
member(null_class,universal_class),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f314,plain,
! [X0] : member(singleton(X0),universal_class),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f323,plain,
! [Z,X] :
( X = Z
| ! [Y] :
( X = Y
| ~ member(X,universal_class)
| unordered_pair(Y,Z) != singleton(X) ) ),
inference(miniscoping,[status(thm)],[f129]) ).
fof(f324,plain,
! [X0,X1,X2] :
( X2 = X1
| X2 = X0
| ~ member(X2,universal_class)
| unordered_pair(X0,X1) != singleton(X2) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f340,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f354,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(f355,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(f356,plain,
! [X0] :
( first(X0) = X0
| ordered_pair(first(X0),second(X0)) = X0 ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f357,plain,
! [X0] :
( second(X0) = X0
| ordered_pair(first(X0),second(X0)) = X0 ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f366,plain,
~ member(x,universal_class),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f367,plain,
first(ordered_pair(x,y)) != ordered_pair(x,y),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f383,definition,
( sQ2_spl
<=> member(ordered_pair(x,y),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( sQ2_spl
| ~ member(ordered_pair(x,y),universal_class) ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f397,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f385,f340]) ).
fof(f398,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f397]) ).
fof(f399,plain,
! [X0] :
( ~ member(x,X0)
| ~ subclass(X0,universal_class) ),
inference(resolution,[status(thm)],[f169,f366]) ).
fof(f400,plain,
! [X0] : ~ member(x,X0),
inference(forward_subsumption_resolution,[status(thm)],[f399,f172]) ).
fof(f415,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)],[f324,f367]) ).
fof(f423,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(f424,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)],[f423]) ).
fof(f426,plain,
( ~ sQ2_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f415,f423,f383]) ).
fof(f503,plain,
! [X0] :
( first(X0) = X0
| first(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f356,f354]) ).
fof(f504,plain,
! [X0] :
( first(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(duplicate_literals_removal,[status(thm)],[f503]) ).
fof(f505,plain,
! [X0] :
( second(X0) = X0
| second(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f357,f355]) ).
fof(f507,plain,
! [X0] :
( second(X0) = X0
| member(X0,cross_product(universal_class,universal_class)) ),
inference(duplicate_literals_removal,[status(thm)],[f505]) ).
fof(f540,definition,
( sQ18_spl
<=> second(ordered_pair(x,y)) = ordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f541,plain,
( ~ sQ18_spl
| second(ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f542,plain,
( sQ18_spl
| second(ordered_pair(x,y)) != ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f544,definition,
( sQ19_spl
<=> first(ordered_pair(x,y)) = ordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f545,plain,
( ~ sQ19_spl
| first(ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f675,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f367]) ).
fof(f676,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f675]) ).
fof(f693,definition,
( sQ31_spl
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( sQ31_spl
| ~ member(null_class,universal_class) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f761,definition,
( sQ39_spl
<=> member(ordered_pair(x,x),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( sQ39_spl
| ~ member(ordered_pair(x,x),universal_class) ),
inference(component_clause,[status(thm)],[f761]) ).
fof(f784,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f763,f340]) ).
fof(f785,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f784]) ).
fof(f956,definition,
( sQ49_spl
<=> member(singleton(null_class),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f958,plain,
( sQ49_spl
| ~ member(singleton(null_class),universal_class) ),
inference(component_clause,[status(thm)],[f956]) ).
fof(f967,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f293]) ).
fof(f968,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f967]) ).
fof(f969,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f958,f314]) ).
fof(f970,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f969]) ).
fof(f973,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)],[f541,f354]) ).
fof(f975,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)],[f541,f356]) ).
fof(f976,definition,
( sQ52_spl
<=> member(ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)),cross_product(universal_class,universal_class)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f977,plain,
( ~ sQ52_spl
| member(ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)),cross_product(universal_class,universal_class)) ),
inference(component_clause,[status(thm)],[f976]) ).
fof(f980,plain,
( ~ sQ18_spl
| sQ19_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f973,f976,f544,f540]) ).
fof(f981,definition,
( sQ53_spl
<=> ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)) = ordered_pair(x,y) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( ~ sQ53_spl
| ordered_pair(first(ordered_pair(x,y)),ordered_pair(x,y)) = ordered_pair(x,y) ),
inference(component_clause,[status(thm)],[f981]) ).
fof(f985,plain,
( ~ sQ18_spl
| sQ19_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f975,f981,f544,f540]) ).
fof(f992,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)],[f542,f424]) ).
fof(f1027,plain,
( ~ sQ52_spl
| ~ sQ53_spl
| member(ordered_pair(x,y),cross_product(universal_class,universal_class)) ),
inference(backward_demodulation,[status(thm)],[f982,f977]) ).
fof(f1255,definition,
( sQ83_spl
<=> member(singleton(ordered_pair(x,y)),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1257,plain,
( sQ83_spl
| ~ member(singleton(ordered_pair(x,y)),universal_class) ),
inference(component_clause,[status(thm)],[f1255]) ).
fof(f1275,definition,
( sQ88_spl
<=> member(singleton(first(ordered_pair(x,y))),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1277,plain,
( sQ88_spl
| ~ member(singleton(first(ordered_pair(x,y))),universal_class) ),
inference(component_clause,[status(thm)],[f1275]) ).
fof(f1284,plain,
( sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1257,f314]) ).
fof(f1285,plain,
sQ83_spl,
inference(contradiction_clause,[status(thm)],[f1284]) ).
fof(f3108,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1277,f314]) ).
fof(f3109,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f3108]) ).
fof(f3431,plain,
! [X0,X1,X2] : ~ member(ordered_pair(x,X0),cross_product(X1,X2)),
inference(resolution,[status(thm)],[f186,f400]) ).
fof(f3433,plain,
( ~ sQ52_spl
| ~ sQ53_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1027,f3431]) ).
fof(f3434,plain,
( ~ sQ52_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f3433]) ).
fof(f5457,plain,
! [X0] : second(ordered_pair(x,X0)) = ordered_pair(x,X0),
inference(resolution,[status(thm)],[f3431,f507]) ).
fof(f5458,plain,
! [X0] : first(ordered_pair(x,X0)) = ordered_pair(x,X0),
inference(resolution,[status(thm)],[f3431,f504]) ).
fof(f5486,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)],[f5457,f992]) ).
fof(f5649,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)],[f5458,f5486]) ).
fof(f5650,plain,
( ~ sQ6_spl
| sQ18_spl
| singleton(ordered_pair(x,y)) != singleton(ordered_pair(x,y)) ),
inference(forward_demodulation,[status(thm)],[f183,f5649]) ).
fof(f5651,plain,
( ~ sQ6_spl
| sQ18_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5650]) ).
fof(f5652,plain,
( ~ sQ6_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f5651]) ).
fof(f5653,plain,
$false,
inference(sat_refutation,[status(thm)],[f398,f426,f676,f785,f968,f970,f980,f985,f1285,f3109,f3434,f5652]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET119-7 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n006.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 04:54:12 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 7.41/1.48 % Refutation found
% 7.41/1.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 7.41/1.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.41/1.51 % Elapsed time: 1.068100 seconds
% 7.41/1.51 % CPU time: 7.990320 seconds
% 7.41/1.51 % Total memory used: 181.677 MB
% 7.41/1.51 % Net memory used: 172.902 MB
%------------------------------------------------------------------------------