%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET042-3 : TPTP v9.3.1. Released v1.0.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:01 PM UTC 2026
% Result : Unsatisfiable 34.01s 4.75s
% Output : CNFRefutation 34.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 34
% Syntax : Number of formulae : 129 ( 34 unt; 16 def)
% Number of atoms : 268 ( 24 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 265 ( 126 ~; 123 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 17 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 84 ( 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( little_set(X)
| ~ member(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [U,X,Y] :
( U != X
| ~ little_set(U)
| member(U,non_ordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,Y,Z] :
( X != ordered_pair(Y,Z)
| ~ little_set(Z)
| ~ little_set(Y)
| ordered_pair_predicate(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [Z,X,Y] :
( ~ member(second(Z),Y)
| ~ member(first(Z),X)
| ~ ordered_pair_predicate(Z)
| ~ little_set(Z)
| member(Z,cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [Z] : ~ member(Z,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
little_set(infinity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
member(empty_set,infinity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [Z] :
( member(f18(Z),Z)
| relation(Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [X] :
( member(ordered_pair(f19(X),f21(X)),X)
| single_valued_set(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [X] :
( member(f24(X),X)
| X = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [Z,X] :
( member(f27(Z,X),X)
| ~ member(Z,range_of(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,axiom,
! [X,Y] :
( first(ordered_pair(X,Y)) = X
| ~ little_set(Y)
| ~ little_set(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [X,Y] :
( second(ordered_pair(X,Y)) = Y
| ~ little_set(Y)
| ~ little_set(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [X,Y] : little_set(ordered_pair(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [X] :
( little_set(X)
| ~ ordered_pair_predicate(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
member(a,set_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
member(b,set_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,negated_conjecture,
~ member(ordered_pair(a,b),cross_product(set_a,set_b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,plain,
! [X] :
( little_set(X)
| ! [Y] : ~ member(X,Y) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f172,plain,
! [X0,X1] :
( little_set(X0)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f178,plain,
! [U,X] :
( U != X
| ~ little_set(U)
| ! [Y] : member(U,non_ordered_pair(X,Y)) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f179,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f188,plain,
! [X0,X1,X2] :
( X0 != ordered_pair(X1,X2)
| ~ little_set(X2)
| ~ little_set(X1)
| ordered_pair_predicate(X0) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f224,plain,
! [Z,Y] :
( ~ member(second(Z),Y)
| ! [X] :
( ~ member(first(Z),X)
| ~ ordered_pair_predicate(Z)
| ~ little_set(Z)
| member(Z,cross_product(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f225,plain,
! [X0,X1,X2] :
( ~ member(second(X0),X2)
| ~ member(first(X0),X1)
| ~ ordered_pair_predicate(X0)
| ~ little_set(X0)
| member(X0,cross_product(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f245,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f247,plain,
little_set(infinity),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f248,plain,
member(empty_set,infinity),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f267,plain,
! [X0] :
( member(f18(X0),X0)
| relation(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f275,plain,
! [X0] :
( member(ordered_pair(f19(X0),f21(X0)),X0)
| single_valued_set(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f291,plain,
! [X0] :
( member(f24(X0),X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f297,plain,
! [X0,X1] :
( member(f27(X0,X1),X1)
| ~ member(X0,range_of(X1)) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f355,plain,
! [X0,X1] :
( first(ordered_pair(X0,X1)) = X0
| ~ little_set(X1)
| ~ little_set(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f356,plain,
! [X0,X1] :
( second(ordered_pair(X0,X1)) = X1
| ~ little_set(X1)
| ~ little_set(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f360,plain,
! [X0,X1] : little_set(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f361,plain,
! [X0] :
( little_set(X0)
| ~ ordered_pair_predicate(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f384,plain,
member(a,set_a),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f385,plain,
member(b,set_b),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f386,plain,
~ member(ordered_pair(a,b),cross_product(set_a,set_b)),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f387,plain,
! [X0,X1] :
( ~ little_set(X0)
| member(X0,non_ordered_pair(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f179]) ).
fof(f389,plain,
! [X0,X1] :
( ~ little_set(X1)
| ~ little_set(X0)
| ordered_pair_predicate(ordered_pair(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f188]) ).
fof(f452,plain,
! [X0,X1,X2] : member(ordered_pair(X0,X1),non_ordered_pair(ordered_pair(X0,X1),X2)),
inference(resolution,[status(thm)],[f360,f387]) ).
fof(f495,plain,
! [X0,X1,X2] :
( ~ member(second(X0),X2)
| ~ member(first(X0),X1)
| ~ ordered_pair_predicate(X0)
| member(X0,cross_product(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f225,f361]) ).
fof(f540,plain,
! [X0,X1,X2,X3] :
( ~ member(second(ordered_pair(X0,X1)),X3)
| ~ member(first(ordered_pair(X0,X1)),X2)
| member(ordered_pair(X0,X1),cross_product(X2,X3))
| ~ little_set(X1)
| ~ little_set(X0) ),
inference(resolution,[status(thm)],[f389,f495]) ).
fof(f709,definition,
( sQ3_spl
<=> little_set(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f711,plain,
( sQ3_spl
| ~ little_set(empty_set) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f1191,plain,
( ~ member(second(ordered_pair(a,b)),set_b)
| ~ member(first(ordered_pair(a,b)),set_a)
| ~ little_set(b)
| ~ little_set(a) ),
inference(resolution,[status(thm)],[f540,f386]) ).
fof(f1194,definition,
( sQ16_spl
<=> little_set(a) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1195,plain,
( ~ sQ16_spl
| little_set(a) ),
inference(component_clause,[status(thm)],[f1194]) ).
fof(f1196,plain,
( sQ16_spl
| ~ little_set(a) ),
inference(component_clause,[status(thm)],[f1194]) ).
fof(f1197,definition,
( sQ17_spl
<=> little_set(b) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1198,plain,
( ~ sQ17_spl
| little_set(b) ),
inference(component_clause,[status(thm)],[f1197]) ).
fof(f1199,plain,
( sQ17_spl
| ~ little_set(b) ),
inference(component_clause,[status(thm)],[f1197]) ).
fof(f1200,definition,
( sQ18_spl
<=> member(first(ordered_pair(a,b)),set_a) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1202,plain,
( sQ18_spl
| ~ member(first(ordered_pair(a,b)),set_a) ),
inference(component_clause,[status(thm)],[f1200]) ).
fof(f1203,definition,
( sQ19_spl
<=> member(second(ordered_pair(a,b)),set_b) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1205,plain,
( sQ19_spl
| ~ member(second(ordered_pair(a,b)),set_b) ),
inference(component_clause,[status(thm)],[f1203]) ).
fof(f1206,plain,
( ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f1191,f1194,f1197,f1200,f1203]) ).
fof(f1209,plain,
! [X0] :
( sQ17_spl
| ~ member(b,X0) ),
inference(resolution,[status(thm)],[f1199,f172]) ).
fof(f1212,plain,
! [X0] :
( sQ16_spl
| ~ member(a,X0) ),
inference(resolution,[status(thm)],[f1196,f172]) ).
fof(f1237,plain,
( sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f385,f1209]) ).
fof(f1238,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f1237]) ).
fof(f1243,plain,
( sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f384,f1212]) ).
fof(f1244,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1243]) ).
fof(f1436,plain,
! [X0] :
( sQ3_spl
| ~ member(empty_set,X0) ),
inference(resolution,[status(thm)],[f711,f172]) ).
fof(f1437,plain,
( sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f248,f1436]) ).
fof(f1439,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f1437]) ).
fof(f1546,plain,
relation(empty_set),
inference(resolution,[status(thm)],[f267,f245]) ).
fof(f2063,plain,
single_valued_set(empty_set),
inference(resolution,[status(thm)],[f245,f275]) ).
fof(f2094,definition,
( sQ40_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f2096,plain,
( sQ40_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f2094]) ).
fof(f2098,definition,
( sQ41_spl
<=> single_valued_set(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f2100,plain,
( sQ41_spl
| ~ single_valued_set(empty_set) ),
inference(component_clause,[status(thm)],[f2098]) ).
fof(f2411,plain,
! [X0] : ~ member(X0,range_of(empty_set)),
inference(resolution,[status(thm)],[f297,f245]) ).
fof(f2572,definition,
( sQ54_spl
<=> range_of(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2574,plain,
( sQ54_spl
| range_of(empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f2572]) ).
fof(f2630,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2096,f1546]) ).
fof(f2631,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f2630]) ).
fof(f2759,definition,
! [X0] :
( sQ58_spl
<=> ~ member(ordered_pair(estin,empty_set),X0) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2760,plain,
! [X0] :
( ~ sQ58_spl
| ~ member(ordered_pair(estin,empty_set),X0) ),
inference(component_clause,[status(thm)],[f2759]) ).
fof(f2769,plain,
( ~ sQ58_spl
| $false ),
inference(resolution,[status(thm)],[f2760,f452]) ).
fof(f2775,plain,
~ sQ58_spl,
inference(contradiction_clause,[status(thm)],[f2769]) ).
fof(f3819,plain,
! [X0] :
( ~ sQ17_spl
| first(ordered_pair(X0,b)) = X0
| ~ little_set(X0) ),
inference(resolution,[status(thm)],[f355,f1198]) ).
fof(f3851,plain,
! [X0] :
( ~ sQ17_spl
| second(ordered_pair(X0,b)) = b
| ~ little_set(X0) ),
inference(resolution,[status(thm)],[f356,f1198]) ).
fof(f4337,plain,
( ~ sQ16_spl
| ~ sQ17_spl
| first(ordered_pair(a,b)) = a ),
inference(resolution,[status(thm)],[f3819,f1195]) ).
fof(f5454,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2063,f2100]) ).
fof(f5455,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f5454]) ).
fof(f5748,definition,
( sQ107_spl
<=> set_a = empty_set ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f5749,plain,
( ~ sQ107_spl
| set_a = empty_set ),
inference(component_clause,[status(thm)],[f5748]) ).
fof(f5973,plain,
range_of(empty_set) = empty_set,
inference(resolution,[status(thm)],[f2411,f291]) ).
fof(f6002,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5973,f2574]) ).
fof(f6003,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f6002]) ).
fof(f8541,plain,
( ~ sQ107_spl
| member(a,empty_set) ),
inference(backward_demodulation,[status(thm)],[f5749,f384]) ).
fof(f8549,plain,
( ~ sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8541,f245]) ).
fof(f8550,plain,
~ sQ107_spl,
inference(contradiction_clause,[status(thm)],[f8549]) ).
fof(f9277,definition,
( sQ161_spl
<=> little_set(infinity) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f9279,plain,
( sQ161_spl
| ~ little_set(infinity) ),
inference(component_clause,[status(thm)],[f9277]) ).
fof(f9416,plain,
( sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9279,f247]) ).
fof(f9417,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f9416]) ).
fof(f10143,definition,
( sQ180_spl
<=> set_b = empty_set ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f10144,plain,
( ~ sQ180_spl
| set_b = empty_set ),
inference(component_clause,[status(thm)],[f10143]) ).
fof(f10179,plain,
( ~ sQ180_spl
| member(b,empty_set) ),
inference(backward_demodulation,[status(thm)],[f10144,f385]) ).
fof(f10182,plain,
( ~ sQ180_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10179,f245]) ).
fof(f10183,plain,
~ sQ180_spl,
inference(contradiction_clause,[status(thm)],[f10182]) ).
fof(f10348,definition,
( sQ189_spl
<=> infinity = empty_set ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f10349,plain,
( ~ sQ189_spl
| infinity = empty_set ),
inference(component_clause,[status(thm)],[f10348]) ).
fof(f10646,plain,
( ~ sQ189_spl
| member(empty_set,empty_set) ),
inference(backward_demodulation,[status(thm)],[f10349,f248]) ).
fof(f12667,plain,
( ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10646,f245]) ).
fof(f12668,plain,
~ sQ189_spl,
inference(contradiction_clause,[status(thm)],[f12667]) ).
fof(f17126,definition,
! [X0] :
( sQ274_spl
<=> ~ member(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f17127,plain,
! [X0] :
( ~ sQ274_spl
| ~ member(empty_set,X0) ),
inference(component_clause,[status(thm)],[f17126]) ).
fof(f17130,plain,
( ~ sQ274_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f248,f17127]) ).
fof(f17148,plain,
~ sQ274_spl,
inference(contradiction_clause,[status(thm)],[f17130]) ).
fof(f17355,plain,
( sQ18_spl
| ~ sQ16_spl
| ~ sQ17_spl
| ~ member(a,set_a) ),
inference(backward_demodulation,[status(thm)],[f4337,f1202]) ).
fof(f17377,plain,
( sQ18_spl
| ~ sQ16_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17355,f384]) ).
fof(f17378,plain,
( sQ18_spl
| ~ sQ16_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f17377]) ).
fof(f17786,definition,
! [X1] :
( sQ304_spl
<=> member(set_b,X1) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f17787,plain,
! [X0] :
( ~ sQ304_spl
| member(set_b,X0) ),
inference(component_clause,[status(thm)],[f17786]) ).
fof(f17794,definition,
! [X1] :
( sQ306_spl
<=> member(set_a,X1) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f17795,plain,
! [X0] :
( ~ sQ306_spl
| member(set_a,X0) ),
inference(component_clause,[status(thm)],[f17794]) ).
fof(f18315,plain,
( ~ sQ306_spl
| $false ),
inference(resolution,[status(thm)],[f17795,f245]) ).
fof(f18328,plain,
~ sQ306_spl,
inference(contradiction_clause,[status(thm)],[f18315]) ).
fof(f18492,plain,
( ~ sQ304_spl
| $false ),
inference(resolution,[status(thm)],[f17787,f245]) ).
fof(f18505,plain,
~ sQ304_spl,
inference(contradiction_clause,[status(thm)],[f18492]) ).
fof(f20594,plain,
( ~ sQ16_spl
| ~ sQ17_spl
| second(ordered_pair(a,b)) = b ),
inference(resolution,[status(thm)],[f3851,f1195]) ).
fof(f21704,plain,
( sQ19_spl
| ~ sQ16_spl
| ~ sQ17_spl
| ~ member(b,set_b) ),
inference(backward_demodulation,[status(thm)],[f20594,f1205]) ).
fof(f21734,plain,
( sQ19_spl
| ~ sQ16_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21704,f385]) ).
fof(f21735,plain,
( sQ19_spl
| ~ sQ16_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f21734]) ).
fof(f21736,plain,
$false,
inference(sat_refutation,[status(thm)],[f1206,f1238,f1244,f1439,f2631,f2775,f5455,f6003,f8550,f9417,f10183,f12668,f17148,f17378,f18328,f18505,f21735]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET042-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 04:46:42 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.16/0.39 % Drodi V4.1.1
% 34.01/4.75 % Refutation found
% 34.01/4.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 34.01/4.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.99/4.82 % Elapsed time: 4.429813 seconds
% 0.99/4.82 % CPU time: 34.631781 seconds
% 0.99/4.82 % Total memory used: 336.148 MB
% 0.99/4.82 % Net memory used: 311.820 MB
%------------------------------------------------------------------------------