%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC153+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:40:11 PM UTC 2026
% Result : Theorem 0.16s 5.49s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 17
% Syntax : Number of formulae : 79 ( 20 unt; 15 def)
% Number of atoms : 354 ( 26 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 442 ( 167 ~; 164 |; 76 &)
% ( 15 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 16 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 96 ( 64 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssItem(X6)
=> ! [X7] :
( ssList(X7)
=> ! [X8] :
( ssList(X8)
=> ! [X9] :
( ssList(X9)
=> ( ( leq(X5,X6)
& ! [X10] :
( ssItem(X10)
=> ( ( leq(X5,X10)
& leq(X10,X6) )
| ~ memberP(X8,X10) ) ) )
| ~ leq(X6,X5)
| app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) != U ) ) ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ? [X4] :
( ( ~ leq(X4,Z)
| ~ leq(Y,X4) )
& memberP(X2,X4)
& ssItem(X4) )
| ~ leq(Y,Z) )
& leq(Z,Y)
& app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) = W
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
| W != U
| X != V ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssItem(X6)
=> ! [X7] :
( ssList(X7)
=> ! [X8] :
( ssList(X8)
=> ! [X9] :
( ssList(X9)
=> ( ( leq(X5,X6)
& ! [X10] :
( ssItem(X10)
=> ( ( leq(X5,X10)
& leq(X10,X6) )
| ~ memberP(X8,X10) ) ) )
| ~ leq(X6,X5)
| app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) != U ) ) ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ? [X4] :
( ( ~ leq(X4,Z)
| ~ leq(Y,X4) )
& memberP(X2,X4)
& ssItem(X4) )
| ~ leq(Y,Z) )
& leq(Z,Y)
& app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) = W
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
| W != U
| X != V ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f223,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( ( ~ leq(X5,X6)
| ? [X10] :
( ( ~ leq(X5,X10)
| ~ leq(X10,X6) )
& memberP(X8,X10)
& ssItem(X10) ) )
& leq(X6,X5)
& app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) = U
& ssList(X9) )
& ssList(X8) )
& ssList(X7) )
& ssItem(X6) )
& ssItem(X5) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ! [X4] :
( ( leq(X4,Z)
& leq(Y,X4) )
| ~ memberP(X2,X4)
| ~ ssItem(X4) )
& leq(Y,Z) )
| ~ leq(Z,Y)
| app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) != W
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(Z) )
| ~ ssItem(Y) )
& W = U
& X = V
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( ( ~ leq(X5,X6)
| ? [X10] :
( ( ~ leq(X5,X10)
| ~ leq(X10,X6) )
& memberP(X8,X10)
& ssItem(X10) ) )
& leq(X6,X5)
& app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) = U
& ssList(X9) )
& ssList(X8) )
& ssList(X7) )
& ssItem(X6) )
& ssItem(X5) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ( ! [X4] :
( ( leq(X4,Z)
& leq(Y,X4) )
| ~ memberP(X2,X4)
| ~ ssItem(X4) )
& leq(Y,Z) )
| ~ leq(Z,Y)
| ! [X3] :
( app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) != W
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(Z) )
| ~ ssItem(Y) )
& W = U
& X = V
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(miniscoping,[status(thm)],[f415]) ).
fof(f417,plain,
( ( ~ leq(sK51_skl,sK52_skl)
| ( ( ~ leq(sK51_skl,sK56_skl)
| ~ leq(sK56_skl,sK52_skl) )
& memberP(sK54_skl,sK56_skl)
& ssItem(sK56_skl) ) )
& leq(sK52_skl,sK51_skl)
& app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK47_skl
& ssList(sK55_skl)
& ssList(sK54_skl)
& ssList(sK53_skl)
& ssItem(sK52_skl)
& ssItem(sK51_skl)
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ( ! [X4] :
( ( leq(X4,Z)
& leq(Y,X4) )
| ~ memberP(X2,X4)
| ~ ssItem(X4) )
& leq(Y,Z) )
| ~ leq(Z,Y)
| ! [X3] :
( app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) != sK49_skl
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(Z) )
| ~ ssItem(Y) )
& sK49_skl = sK47_skl
& sK50_skl = sK48_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl,sK56_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(X5,sK51_skl),skolemize(X6,sK52_skl),skolemize(X7,sK53_skl),skolemize(X8,sK54_skl),skolemize(X9,sK55_skl),skolemize(X10,sK56_skl)],[f416]) ).
fof(f423,plain,
sK49_skl = sK47_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f424,plain,
! [X0,X1,X2,X3,X4] :
( leq(X0,X1)
| ~ leq(X1,X0)
| app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4) != sK49_skl
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f425,plain,
! [X0,X1,X2,X3,X4,X5] :
( leq(X0,X5)
| ~ memberP(X3,X5)
| ~ ssItem(X5)
| ~ leq(X1,X0)
| app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4) != sK49_skl
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f426,plain,
! [X0,X1,X2,X3,X4,X5] :
( leq(X5,X1)
| ~ memberP(X3,X5)
| ~ ssItem(X5)
| ~ leq(X1,X0)
| app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4) != sK49_skl
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f427,plain,
ssItem(sK51_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f428,plain,
ssItem(sK52_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f429,plain,
ssList(sK53_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f430,plain,
ssList(sK54_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f431,plain,
ssList(sK55_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f432,plain,
app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK47_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f433,plain,
leq(sK52_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f434,plain,
( ~ leq(sK51_skl,sK52_skl)
| ssItem(sK56_skl) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f435,plain,
( ~ leq(sK51_skl,sK52_skl)
| memberP(sK54_skl,sK56_skl) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f436,plain,
( ~ leq(sK51_skl,sK52_skl)
| ~ leq(sK51_skl,sK56_skl)
| ~ leq(sK56_skl,sK52_skl) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f437,definition,
( sQ0_spl
<=> ssItem(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f440,definition,
( sQ1_spl
<=> leq(sK51_skl,sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f434,f437,f440]) ).
fof(f444,definition,
( sQ2_spl
<=> memberP(sK54_skl,sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f445,plain,
( ~ sQ2_spl
| memberP(sK54_skl,sK56_skl) ),
inference(component_clause,[status(thm)],[f444]) ).
fof(f447,plain,
( ~ sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f435,f444,f440]) ).
fof(f448,definition,
( sQ3_spl
<=> leq(sK56_skl,sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f451,definition,
( sQ4_spl
<=> leq(sK51_skl,sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f436,f448,f451,f440]) ).
fof(f489,plain,
app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK49_skl,
inference(forward_demodulation,[status(thm)],[f423,f432]) ).
fof(f490,plain,
( leq(sK51_skl,sK52_skl)
| ~ leq(sK52_skl,sK51_skl)
| ~ ssList(sK55_skl)
| ~ ssList(sK54_skl)
| ~ ssList(sK53_skl)
| ~ ssItem(sK52_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f424,f489]) ).
fof(f493,definition,
( sQ5_spl
<=> ssItem(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( sQ5_spl
| ~ ssItem(sK51_skl) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,definition,
( sQ6_spl
<=> ssItem(sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( sQ6_spl
| ~ ssItem(sK52_skl) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
( sQ7_spl
<=> ssList(sK53_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( sQ7_spl
| ~ ssList(sK53_skl) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,definition,
( sQ8_spl
<=> ssList(sK54_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ8_spl
| ~ ssList(sK54_skl) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f505,definition,
( sQ9_spl
<=> ssList(sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ9_spl
| ~ ssList(sK55_skl) ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f508,definition,
( sQ10_spl
<=> leq(sK52_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( sQ10_spl
| ~ leq(sK52_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( sQ1_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f490,f493,f496,f499,f502,f505,f508,f440]) ).
fof(f523,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f431]) ).
fof(f524,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f523]) ).
fof(f525,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f498,f428]) ).
fof(f526,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f527,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f510,f433]) ).
fof(f528,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f529,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f430]) ).
fof(f530,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f529]) ).
fof(f531,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f495,f427]) ).
fof(f532,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f531]) ).
fof(f533,plain,
! [X0] :
( leq(sK51_skl,X0)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0)
| ~ leq(sK52_skl,sK51_skl)
| ~ ssList(sK55_skl)
| ~ ssList(sK54_skl)
| ~ ssList(sK53_skl)
| ~ ssItem(sK52_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f425,f489]) ).
fof(f536,definition,
! [X0] :
( sQ14_spl
<=> ( leq(sK51_skl,X0)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f537,plain,
! [X0] :
( ~ sQ14_spl
| leq(sK51_skl,X0)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,plain,
( sQ14_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f533,f493,f496,f499,f502,f505,f508,f536]) ).
fof(f548,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f501,f429]) ).
fof(f549,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f548]) ).
fof(f559,definition,
! [X0] :
( sQ19_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f560,plain,
! [X0] :
( ~ sQ19_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f566,plain,
! [X0] :
( ~ sQ19_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f560]) ).
fof(f575,plain,
( ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f431,f566]) ).
fof(f581,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f575]) ).
fof(f583,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| leq(sK51_skl,sK56_skl)
| ~ ssItem(sK56_skl) ),
inference(resolution,[status(thm)],[f537,f445]) ).
fof(f584,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f583,f437,f451,f536,f444]) ).
fof(f591,plain,
! [X0] :
( leq(X0,sK52_skl)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0)
| ~ leq(sK52_skl,sK51_skl)
| ~ ssList(sK55_skl)
| ~ ssList(sK54_skl)
| ~ ssList(sK53_skl)
| ~ ssItem(sK52_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f426,f489]) ).
fof(f594,definition,
! [X0] :
( sQ23_spl
<=> ( leq(X0,sK52_skl)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f595,plain,
! [X0] :
( ~ sQ23_spl
| leq(X0,sK52_skl)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f594]) ).
fof(f597,plain,
( sQ23_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f591,f493,f496,f499,f502,f505,f508,f594]) ).
fof(f604,definition,
( sQ25_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( sQ25_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f630,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f606,f223]) ).
fof(f631,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f630]) ).
fof(f713,plain,
( ~ sQ2_spl
| ~ sQ23_spl
| leq(sK56_skl,sK52_skl)
| ~ ssItem(sK56_skl) ),
inference(resolution,[status(thm)],[f595,f445]) ).
fof(f714,plain,
( ~ sQ2_spl
| ~ sQ23_spl
| sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f713,f437,f448,f594,f444]) ).
fof(f715,plain,
$false,
inference(sat_refutation,[status(thm)],[f443,f447,f454,f511,f524,f526,f528,f530,f532,f539,f549,f581,f584,f597,f631,f714]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC153+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.44 % Computer : n019.cluster.edu
% 0.16/5.44 % Model : x86_64 x86_64
% 0.16/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.44 % Memory : 8046.5625MB
% 0.16/5.44 % OS : Linux 6.8.0-71-generic
% 0.16/5.44 % CPULimit : 300
% 0.16/5.44 % WCLimit : 300
% 0.16/5.44 % DateTime : Mon Sep 21 08:00:40 UTC 2026
% 0.16/5.44 % CPUTime :
% 0.16/5.47 % Drodi V4.1.1
% 0.16/5.49 % Refutation found
% 0.16/5.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/5.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/5.53 % Elapsed time: 0.074054 seconds
% 0.21/5.53 % CPU time: 0.211884 seconds
% 0.21/5.53 % Total memory used: 80.230 MB
% 0.21/5.53 % Net memory used: 80.106 MB
%------------------------------------------------------------------------------