%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB044+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:37:14 PM UTC 2026
% Result : Theorem 242.02s 30.93s
% Output : CNFRefutation 242.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 9
% Syntax : Number of formulae : 73 ( 19 unt; 0 def)
% Number of atoms : 274 ( 31 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 306 ( 105 ~; 111 |; 75 &)
% ( 10 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 16 con; 0-3 aty)
% Number of variables : 158 ( 140 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_domain,P,C) )
=> icext(C,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_range,P,C) )
=> icext(C,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f295,axiom,
! [Z,S1,A1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> X = A1 )
& ic(Z) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,X) )
& ic(C)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f345,axiom,
! [X,Y] :
( iext(uri_owl_differentFrom,X,Y)
<=> X != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f392,axiom,
! [P] :
( icext(uri_owl_AsymmetricProperty,P)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> ~ iext(P,Y,X) )
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [X2,X3,X0,X1] :
( iext(uri_rdf_rest,X3,uri_rdf_nil)
& iext(uri_rdf_first,X3,uri_ex_x)
& iext(uri_rdf_rest,X1,uri_rdf_nil)
& iext(uri_rdf_first,X1,uri_ex_y)
& iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& iext(uri_owl_oneOf,X2,X3)
& iext(uri_rdfs_range,uri_ex_p,X0)
& iext(uri_rdfs_domain,uri_ex_p,X2)
& iext(uri_owl_oneOf,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f592,plain,
! [X,C] :
( ( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f593,plain,
( ! [X,C] :
( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ! [X,C] :
( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(miniscoping,[status(thm)],[f592]) ).
fof(f595,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f625,plain,
! [P,C,X,Y] :
( icext(C,X)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f626,plain,
! [C,X] :
( icext(C,X)
| ! [P] :
( ! [Y] : ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f625]) ).
fof(f627,plain,
! [X0,X1,X2,X3] :
( icext(X1,X2)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f626]) ).
fof(f643,plain,
! [P,C,X,Y] :
( icext(C,Y)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_range,P,C) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f644,plain,
! [C,Y] :
( icext(C,Y)
| ! [P] :
( ! [X] : ~ iext(P,X,Y)
| ~ iext(uri_rdfs_range,P,C) ) ),
inference(miniscoping,[status(thm)],[f643]) ).
fof(f645,plain,
! [X0,X1,X2,X3] :
( icext(X1,X3)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_range,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f644]) ).
fof(f1211,plain,
! [Z,S1,A1] :
( ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> X = A1 )
& ic(Z) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(pre_NNF_transformation,[status(thm)],[f295]) ).
fof(f1212,plain,
! [Z,S1,A1] :
( ( ( ? [X] :
( ( X = A1
| icext(Z,X) )
& ( X != A1
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ! [X] :
( ( X != A1
| icext(Z,X) )
& ( X = A1
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(NNF_transformation,[status(thm)],[f1211]) ).
fof(f1213,plain,
! [S1,A1] :
( ( ! [Z] :
( ? [X] :
( ( X = A1
| icext(Z,X) )
& ( X != A1
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( X != A1
| icext(Z,X) )
& ! [X] :
( X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(miniscoping,[status(thm)],[f1212]) ).
fof(f1214,plain,
! [S1,A1] :
( ( ! [Z] :
( ( ( sK10_skl(Z,A1,S1) = A1
| icext(Z,sK10_skl(Z,A1,S1)) )
& ( sK10_skl(Z,A1,S1) != A1
| ~ icext(Z,sK10_skl(Z,A1,S1)) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( X != A1
| icext(Z,X) )
& ! [X] :
( X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1213]) ).
fof(f1216,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,X0)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1214]) ).
fof(f1713,plain,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f341]) ).
fof(f1714,plain,
! [P,C] :
( ( ? [X,Y] :
( ~ icext(C,X)
& iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ( ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(NNF_transformation,[status(thm)],[f1713]) ).
fof(f1715,plain,
( ! [P,C] :
( ? [X] :
( ~ icext(C,X)
& ? [Y] : iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f1714]) ).
fof(f1716,plain,
( ! [P,C] :
( ( ~ icext(C,sK111_skl(C,P))
& iext(P,sK111_skl(C,P),sK112_skl(C,P)) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK111_skl,sK112_skl]),skolemize(X,sK111_skl(C,P)),skolemize(Y,sK112_skl(C,P))],[f1715]) ).
fof(f1717,plain,
! [X0,X1] :
( ip(X0)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1716]) ).
fof(f1749,plain,
! [X,Y] :
( ( X = Y
| iext(uri_owl_differentFrom,X,Y) )
& ( X != Y
| ~ iext(uri_owl_differentFrom,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f345]) ).
fof(f1750,plain,
( ! [X,Y] :
( X = Y
| iext(uri_owl_differentFrom,X,Y) )
& ! [X,Y] :
( X != Y
| ~ iext(uri_owl_differentFrom,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1749]) ).
fof(f1751,plain,
! [X0,X1] :
( X0 != X1
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1750]) ).
fof(f2008,plain,
! [P] :
( icext(uri_owl_AsymmetricProperty,P)
<=> ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f392]) ).
fof(f2009,plain,
! [P] :
( ( ? [X,Y] :
( iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2008]) ).
fof(f2010,plain,
( ! [P] :
( ? [X,Y] :
( iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ! [P] :
( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2009]) ).
fof(f2011,plain,
( ! [P] :
( ( iext(P,sK169_skl(P),sK168_skl(P))
& iext(P,sK168_skl(P),sK169_skl(P)) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ! [P] :
( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK168_skl,sK169_skl]),skolemize(X,sK168_skl(P)),skolemize(Y,sK169_skl(P))],[f2010]) ).
fof(f2014,plain,
! [X0] :
( iext(X0,sK168_skl(X0),sK169_skl(X0))
| ~ ip(X0)
| icext(uri_owl_AsymmetricProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2011]) ).
fof(f2015,plain,
! [X0] :
( iext(X0,sK169_skl(X0),sK168_skl(X0))
| ~ ip(X0)
| icext(uri_owl_AsymmetricProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2011]) ).
fof(f2405,plain,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2406,plain,
? [X3] :
( iext(uri_rdf_rest,X3,uri_rdf_nil)
& iext(uri_rdf_first,X3,uri_ex_x)
& ? [X1] :
( iext(uri_rdf_rest,X1,uri_rdf_nil)
& iext(uri_rdf_first,X1,uri_ex_y)
& iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& ? [X2] :
( iext(uri_owl_oneOf,X2,X3)
& ? [X0] :
( iext(uri_rdfs_range,uri_ex_p,X0)
& iext(uri_rdfs_domain,uri_ex_p,X2)
& iext(uri_owl_oneOf,X0,X1) ) ) ) ),
inference(miniscoping,[status(thm)],[f561]) ).
fof(f2407,plain,
( iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK199_skl,uri_ex_x)
& iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK200_skl,uri_ex_y)
& iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& iext(uri_owl_oneOf,sK201_skl,sK199_skl)
& iext(uri_rdfs_range,uri_ex_p,sK202_skl)
& iext(uri_rdfs_domain,uri_ex_p,sK201_skl)
& iext(uri_owl_oneOf,sK202_skl,sK200_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl,sK202_skl]),skolemize(X3,sK199_skl),skolemize(X1,sK200_skl),skolemize(X2,sK201_skl),skolemize(X0,sK202_skl)],[f2406]) ).
fof(f2408,plain,
iext(uri_owl_oneOf,sK202_skl,sK200_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2409,plain,
iext(uri_rdfs_domain,uri_ex_p,sK201_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2410,plain,
iext(uri_rdfs_range,uri_ex_p,sK202_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2411,plain,
iext(uri_owl_oneOf,sK201_skl,sK199_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2413,plain,
iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2414,plain,
iext(uri_rdf_first,sK200_skl,uri_ex_y),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2415,plain,
iext(uri_rdf_rest,sK200_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2416,plain,
iext(uri_rdf_first,sK199_skl,uri_ex_x),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2417,plain,
iext(uri_rdf_rest,sK199_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2517,plain,
! [X0] : ~ iext(uri_owl_differentFrom,X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f1751]) ).
fof(f3261,plain,
! [X0,X1] :
( X1 = uri_ex_x
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK199_skl)
| ~ iext(uri_rdf_rest,sK199_skl,uri_rdf_nil) ),
inference(resolution,[status(thm)],[f1216,f2416]) ).
fof(f3262,plain,
! [X0,X1] :
( X1 = uri_ex_y
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK200_skl)
| ~ iext(uri_rdf_rest,sK200_skl,uri_rdf_nil) ),
inference(resolution,[status(thm)],[f1216,f2414]) ).
fof(f3263,plain,
! [X0,X1] :
( X1 = uri_ex_x
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK199_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3261,f2417]) ).
fof(f3264,plain,
! [X0,X1] :
( X1 = uri_ex_y
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK200_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3262,f2415]) ).
fof(f10293,plain,
! [X0] :
( X0 = uri_ex_y
| ~ icext(sK202_skl,X0) ),
inference(resolution,[status(thm)],[f2408,f3264]) ).
fof(f10332,plain,
! [X0,X1] :
( icext(sK201_skl,X0)
| ~ iext(uri_ex_p,X0,X1) ),
inference(resolution,[status(thm)],[f2409,f627]) ).
fof(f10334,plain,
ip(uri_ex_p),
inference(resolution,[status(thm)],[f2409,f1717]) ).
fof(f10350,plain,
( iext(uri_ex_p,sK169_skl(uri_ex_p),sK168_skl(uri_ex_p))
| icext(uri_owl_AsymmetricProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10334,f2015]) ).
fof(f10351,plain,
( iext(uri_ex_p,sK168_skl(uri_ex_p),sK169_skl(uri_ex_p))
| icext(uri_owl_AsymmetricProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10334,f2014]) ).
fof(f10401,plain,
( icext(sK201_skl,sK169_skl(uri_ex_p))
| icext(uri_owl_AsymmetricProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10350,f10332]) ).
fof(f10469,plain,
! [X0,X1] :
( icext(sK202_skl,X1)
| ~ iext(uri_ex_p,X0,X1) ),
inference(resolution,[status(thm)],[f2410,f645]) ).
fof(f10483,plain,
( icext(uri_owl_AsymmetricProperty,uri_ex_p)
| icext(sK202_skl,sK169_skl(uri_ex_p)) ),
inference(resolution,[status(thm)],[f10469,f10351]) ).
fof(f10485,plain,
( sK169_skl(uri_ex_p) = uri_ex_y
| icext(uri_owl_AsymmetricProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10483,f10293]) ).
fof(f10490,plain,
( iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty)
| sK169_skl(uri_ex_p) = uri_ex_y ),
inference(resolution,[status(thm)],[f10485,f595]) ).
fof(f10491,plain,
sK169_skl(uri_ex_p) = uri_ex_y,
inference(forward_subsumption_resolution,[status(thm)],[f10490,f2405]) ).
fof(f10496,plain,
( icext(sK201_skl,uri_ex_y)
| icext(uri_owl_AsymmetricProperty,uri_ex_p) ),
inference(backward_demodulation,[status(thm)],[f10491,f10401]) ).
fof(f10522,plain,
( iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty)
| icext(sK201_skl,uri_ex_y) ),
inference(resolution,[status(thm)],[f10496,f595]) ).
fof(f10523,plain,
icext(sK201_skl,uri_ex_y),
inference(forward_subsumption_resolution,[status(thm)],[f10522,f2405]) ).
fof(f10551,plain,
! [X0] :
( X0 = uri_ex_x
| ~ icext(sK201_skl,X0) ),
inference(resolution,[status(thm)],[f2411,f3263]) ).
fof(f10560,plain,
uri_ex_y = uri_ex_x,
inference(resolution,[status(thm)],[f10551,f10523]) ).
fof(f10805,plain,
iext(uri_owl_differentFrom,uri_ex_x,uri_ex_x),
inference(forward_demodulation,[status(thm)],[f10560,f2413]) ).
fof(f10806,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10805,f2517]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB044+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n011.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 07:43:56 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 242.02/30.93 % Refutation found
% 242.02/30.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 242.02/30.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 242.02/31.00 % Elapsed time: 30.629665 seconds
% 242.02/31.00 % CPU time: 242.610298 seconds
% 242.02/31.00 % Total memory used: 508.676 MB
% 242.02/31.00 % Net memory used: 479.936 MB
%------------------------------------------------------------------------------