%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET014-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:08:51 PM UTC 2026
% Result : Unsatisfiable 15.42s 2.52s
% Output : CNFRefutation 10.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 28
% Syntax : Number of formulae : 105 ( 22 unt; 12 def)
% Number of atoms : 208 ( 12 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 203 ( 100 ~; 91 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 13 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 106 ( 106 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( little_set(X)
| ~ member(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( X = Y
| little_set(f1(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( X = Y
| member(f1(X,Y),Y)
| member(f1(X,Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Z,X,Y] :
( ~ member(Z,Y)
| ~ member(Z,X)
| member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Z,X] :
( member(Z,X)
| ~ little_set(Z)
| member(Z,complement(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] : union(X,Y) = complement(intersection(complement(X),complement(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Z] : ~ member(Z,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Z] :
( ~ little_set(Z)
| member(Z,universal_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subset(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,Y] :
( member(f17(X,Y),X)
| subset(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,Y] :
( ~ member(f17(X,Y),Y)
| subset(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
subset(as,cs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
subset(bs,cs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ subset(union(as,bs),cs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,plain,
! [X] :
( little_set(X)
| ! [Y] : ~ member(X,Y) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1] :
( little_set(X0)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( X0 = X1
| little_set(f1(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
! [X0,X1] :
( X0 = X1
| member(f1(X0,X1),X1)
| member(f1(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f26,plain,
! [Z,Y] :
( member(Z,Y)
| ! [X] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f27,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f28,plain,
! [Z,Y] :
( ~ member(Z,Y)
| ! [X] :
( ~ member(Z,X)
| member(Z,intersection(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f31,plain,
! [X0,X1] :
( member(X0,X1)
| ~ little_set(X0)
| member(X0,complement(X1)) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f32,plain,
! [X0,X1] : union(X0,X1) = complement(intersection(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f33,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f34,plain,
! [X0] :
( ~ little_set(X0)
| member(X0,universal_set) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f35,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subset(X,Y) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f36,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( member(f17(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f38,plain,
! [X0,X1] :
( ~ member(f17(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f39,plain,
subset(as,cs),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f40,plain,
subset(bs,cs),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f41,plain,
~ subset(union(as,bs),cs),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f68,plain,
! [X0,X1] :
( X0 = X1
| member(f1(X0,X1),universal_set) ),
inference(resolution,[status(thm)],[f34,f21]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ subset(X2,X1)
| ~ member(X0,complement(X1)) ),
inference(resolution,[status(thm)],[f30,f36]) ).
fof(f78,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,X3)
| ~ subset(X3,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(resolution,[status(thm)],[f29,f36]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,X1)
| member(X0,complement(X1)) ),
inference(resolution,[status(thm)],[f31,f20]) ).
fof(f81,plain,
! [X0] :
( ~ member(X0,bs)
| ~ member(X0,complement(cs)) ),
inference(resolution,[status(thm)],[f74,f40]) ).
fof(f88,plain,
! [X0,X1] :
( ~ member(X0,as)
| ~ member(X0,X1)
| member(X0,intersection(X1,cs)) ),
inference(resolution,[status(thm)],[f78,f39]) ).
fof(f98,plain,
! [X0,X1] :
( ~ member(f1(X0,X1),complement(universal_set))
| X0 = X1 ),
inference(resolution,[status(thm)],[f68,f30]) ).
fof(f103,plain,
member(f17(union(as,bs),cs),union(as,bs)),
inference(resolution,[status(thm)],[f37,f41]) ).
fof(f128,definition,
( sQ1_spl
<=> member(f1(empty_set,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f129,plain,
( ~ sQ1_spl
| member(f1(empty_set,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f128]) ).
fof(f230,plain,
! [X0,X1] :
( ~ member(X0,bs)
| ~ member(X0,X1)
| member(X0,intersection(X1,cs)) ),
inference(resolution,[status(thm)],[f40,f78]) ).
fof(f312,plain,
! [X0] :
( member(f17(union(as,bs),cs),X0)
| member(f17(union(as,bs),cs),complement(X0)) ),
inference(resolution,[status(thm)],[f103,f80]) ).
fof(f368,plain,
~ member(f17(union(as,bs),cs),cs),
inference(resolution,[status(thm)],[f38,f41]) ).
fof(f372,plain,
! [X0,X1,X2] :
( ~ member(X0,intersection(complement(X1),complement(X2)))
| ~ member(X0,union(X1,X2)) ),
inference(paramodulation,[status(thm)],[f32,f30]) ).
fof(f381,plain,
! [X0] :
( ~ member(f17(union(as,bs),cs),X0)
| ~ subset(X0,cs) ),
inference(resolution,[status(thm)],[f368,f36]) ).
fof(f466,definition,
! [X0] :
( sQ20_spl
<=> ~ member(f17(union(as,bs),cs),X0) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f467,plain,
! [X0] :
( ~ sQ20_spl
| ~ member(f17(union(as,bs),cs),X0) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f541,definition,
( sQ24_spl
<=> member(f17(union(as,bs),cs),bs) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f604,plain,
~ member(f17(union(as,bs),cs),intersection(complement(as),complement(bs))),
inference(resolution,[status(thm)],[f372,f103]) ).
fof(f676,plain,
! [X0] :
( X0 = empty_set
| member(f1(X0,empty_set),X0) ),
inference(resolution,[status(thm)],[f33,f22]) ).
fof(f780,plain,
! [X0] :
( member(f17(X0,cs),X0)
| ~ member(f17(union(as,bs),cs),X0) ),
inference(resolution,[status(thm)],[f381,f37]) ).
fof(f781,plain,
! [X0] :
( ~ member(f17(X0,cs),cs)
| ~ member(f17(union(as,bs),cs),X0) ),
inference(resolution,[status(thm)],[f381,f38]) ).
fof(f867,plain,
! [X0] :
( ~ sQ20_spl
| member(f17(union(as,bs),cs),complement(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f312,f467]) ).
fof(f877,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f867,f467]) ).
fof(f878,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f877]) ).
fof(f1015,plain,
( ~ member(f17(union(as,bs),cs),complement(bs))
| ~ member(f17(union(as,bs),cs),complement(as)) ),
inference(resolution,[status(thm)],[f604,f29]) ).
fof(f1020,definition,
( sQ48_spl
<=> member(f17(union(as,bs),cs),complement(as)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1022,plain,
( sQ48_spl
| ~ member(f17(union(as,bs),cs),complement(as)) ),
inference(component_clause,[status(thm)],[f1020]) ).
fof(f1028,definition,
( sQ50_spl
<=> member(f17(union(as,bs),cs),complement(bs)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
( sQ50_spl
| ~ member(f17(union(as,bs),cs),complement(bs)) ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1031,plain,
( ~ sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1015,f1020,f1028]) ).
fof(f1199,definition,
! [X0] :
( sQ57_spl
<=> member(f1(bs,empty_set),X0) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1200,plain,
! [X0] :
( ~ sQ57_spl
| member(f1(bs,empty_set),X0) ),
inference(component_clause,[status(thm)],[f1199]) ).
fof(f1221,plain,
( ~ sQ57_spl
| ~ member(f1(bs,empty_set),complement(cs)) ),
inference(resolution,[status(thm)],[f1200,f81]) ).
fof(f1230,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1221,f1200]) ).
fof(f1231,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1230]) ).
fof(f1374,definition,
( sQ64_spl
<=> member(f17(union(as,bs),cs),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1375,plain,
( ~ sQ64_spl
| member(f17(union(as,bs),cs),empty_set) ),
inference(component_clause,[status(thm)],[f1374]) ).
fof(f1393,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1375,f33]) ).
fof(f1394,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f1393]) ).
fof(f1448,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f129,f33]) ).
fof(f1449,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1448]) ).
fof(f1537,definition,
! [X0] :
( sQ72_spl
<=> member(f1(empty_set,empty_set),X0) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
! [X0] :
( ~ sQ72_spl
| member(f1(empty_set,empty_set),X0) ),
inference(component_clause,[status(thm)],[f1537]) ).
fof(f1636,plain,
! [X0,X1] :
( member(X0,cs)
| ~ member(X0,as)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f88,f27]) ).
fof(f1641,plain,
( ~ sQ72_spl
| ~ member(f1(empty_set,empty_set),complement(cs)) ),
inference(resolution,[status(thm)],[f1538,f81]) ).
fof(f1650,plain,
( ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1641,f1538]) ).
fof(f1651,plain,
~ sQ72_spl,
inference(contradiction_clause,[status(thm)],[f1650]) ).
fof(f1654,plain,
( complement(universal_set) = empty_set
| complement(universal_set) = empty_set ),
inference(resolution,[status(thm)],[f98,f676]) ).
fof(f1666,definition,
( sQ78_spl
<=> complement(universal_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1669,plain,
sQ78_spl,
inference(split_clause,[status(thm)],[f1654,f1666]) ).
fof(f2252,plain,
! [X0,X1] :
( member(X0,cs)
| ~ member(X0,bs)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f230,f27]) ).
fof(f2296,plain,
! [X0] :
( ~ member(f17(union(as,bs),cs),as)
| ~ member(f17(union(as,bs),cs),X0) ),
inference(resolution,[status(thm)],[f1636,f368]) ).
fof(f2308,definition,
( sQ93_spl
<=> member(f17(union(as,bs),cs),as) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f2311,plain,
( ~ sQ93_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f2296,f466,f2308]) ).
fof(f2450,plain,
! [X0] :
( ~ member(f17(union(as,bs),cs),bs)
| ~ member(f17(union(as,bs),cs),X0) ),
inference(resolution,[status(thm)],[f2252,f368]) ).
fof(f2456,plain,
( ~ sQ24_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f2450,f466,f541]) ).
fof(f2485,definition,
( sQ106_spl
<=> member(f17(union(as,bs),cs),cs) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2510,plain,
( ~ member(f17(union(as,bs),cs),cs)
| ~ member(f17(union(as,bs),cs),cs) ),
inference(resolution,[status(thm)],[f781,f780]) ).
fof(f2516,plain,
~ sQ106_spl,
inference(split_clause,[status(thm)],[f2510,f2485]) ).
fof(f2620,definition,
( sQ119_spl
<=> member(f1(universal_set,universal_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f2621,plain,
( ~ sQ119_spl
| member(f1(universal_set,universal_set),empty_set) ),
inference(component_clause,[status(thm)],[f2620]) ).
fof(f2650,plain,
( ~ sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2621,f33]) ).
fof(f2651,plain,
~ sQ119_spl,
inference(contradiction_clause,[status(thm)],[f2650]) ).
fof(f3292,plain,
! [X0] :
( sQ48_spl
| ~ member(f17(union(as,bs),cs),X0)
| member(f17(union(as,bs),cs),as) ),
inference(resolution,[status(thm)],[f1022,f80]) ).
fof(f3296,plain,
( sQ48_spl
| sQ20_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f3292,f2308,f466,f1020]) ).
fof(f4358,plain,
( sQ50_spl
| member(f17(union(as,bs),cs),bs) ),
inference(resolution,[status(thm)],[f1030,f312]) ).
fof(f4361,plain,
( sQ50_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f4358,f541,f1028]) ).
fof(f4363,plain,
$false,
inference(sat_refutation,[status(thm)],[f878,f1031,f1231,f1394,f1449,f1651,f1669,f2311,f2456,f2516,f2651,f3296,f4361]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET014-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n001.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % 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:47:43 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 15.42/2.52 % Refutation found
% 15.42/2.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 15.42/2.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.03/2.57 % Elapsed time: 2.118270 seconds
% 10.03/2.57 % CPU time: 16.339254 seconds
% 10.03/2.57 % Total memory used: 253.173 MB
% 10.03/2.57 % Net memory used: 241.050 MB
%------------------------------------------------------------------------------