%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR109+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 12:13:46 PM UTC 2026
% Result : Theorem 94.82s 18.14s
% Output : CNFRefutation 25.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 5
% Syntax : Number of formulae : 85 ( 37 unt; 0 def)
% Number of atoms : 239 ( 0 equ)
% Maximal formula atoms : 22 ( 2 avg)
% Number of connectives : 222 ( 68 ~; 66 |; 84 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 83 ( 53 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [V__X,V__Y] :
( s__subclass(V__X,V__Y)
=> ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [V__X,V__Y,V__Z] :
( ( s__instance(V__X,s__SetOrClass)
& s__instance(V__Y,s__SetOrClass) )
=> ( ( s__instance(V__Z,V__X)
& s__subclass(V__X,V__Y) )
=> s__instance(V__Z,V__Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26088,axiom,
s__subclass(s__Reptile,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37983,axiom,
( s__subclass(s__Reptile,s__Animal)
=> ? [V_C1,V_C2,V_C3,V_C4,V_C5,V_C6,V_C7,V_C8,V_C9,V_C10] :
( s__instance(s__Creature50_1,V_C1)
& s__subclass(V_C10,s__Reptile)
& s__subclass(V_C9,V_C10)
& s__subclass(V_C8,V_C9)
& s__subclass(V_C7,V_C8)
& s__subclass(V_C6,V_C7)
& s__subclass(V_C5,V_C6)
& s__subclass(V_C4,V_C5)
& s__subclass(V_C3,V_C4)
& s__subclass(V_C2,V_C3)
& s__subclass(V_C1,V_C2)
& s__instance(V_C10,s__SetOrClass)
& s__instance(V_C9,s__SetOrClass)
& s__instance(V_C8,s__SetOrClass)
& s__instance(V_C7,s__SetOrClass)
& s__instance(V_C6,s__SetOrClass)
& s__instance(V_C5,s__SetOrClass)
& s__instance(V_C4,s__SetOrClass)
& s__instance(V_C3,s__SetOrClass)
& s__instance(V_C2,s__SetOrClass)
& s__instance(V_C1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37984,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37985,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f37984]) ).
fof(f38025,plain,
! [V__X,V__Y] :
( ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) )
| ~ s__subclass(V__X,V__Y) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f38026,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f38025]) ).
fof(f38027,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f38025]) ).
fof(f38028,plain,
! [V__X,V__Y,V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y)
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f38029,plain,
! [V__X,V__Y] :
( ! [V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y) )
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(miniscoping,[status(thm)],[f38028]) ).
fof(f38030,plain,
! [X0,X1,X2] :
( ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X1)
| s__instance(X2,X0)
| ~ s__subclass(X1,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f38029]) ).
fof(f74777,plain,
s__subclass(s__Reptile,s__Animal),
inference(cnf_transformation,[status(thm)],[f26088]) ).
fof(f86672,plain,
( ? [V_C1,V_C2,V_C3,V_C4,V_C5,V_C6,V_C7,V_C8,V_C9,V_C10] :
( s__instance(s__Creature50_1,V_C1)
& s__subclass(V_C10,s__Reptile)
& s__subclass(V_C9,V_C10)
& s__subclass(V_C8,V_C9)
& s__subclass(V_C7,V_C8)
& s__subclass(V_C6,V_C7)
& s__subclass(V_C5,V_C6)
& s__subclass(V_C4,V_C5)
& s__subclass(V_C3,V_C4)
& s__subclass(V_C2,V_C3)
& s__subclass(V_C1,V_C2)
& s__instance(V_C10,s__SetOrClass)
& s__instance(V_C9,s__SetOrClass)
& s__instance(V_C8,s__SetOrClass)
& s__instance(V_C7,s__SetOrClass)
& s__instance(V_C6,s__SetOrClass)
& s__instance(V_C5,s__SetOrClass)
& s__instance(V_C4,s__SetOrClass)
& s__instance(V_C3,s__SetOrClass)
& s__instance(V_C2,s__SetOrClass)
& s__instance(V_C1,s__SetOrClass) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(pre_NNF_transformation,[status(thm)],[f37983]) ).
fof(f86673,plain,
( ? [V_C1] :
( s__instance(s__Creature50_1,V_C1)
& ? [V_C10] :
( s__subclass(V_C10,s__Reptile)
& ? [V_C9] :
( s__subclass(V_C9,V_C10)
& ? [V_C8] :
( s__subclass(V_C8,V_C9)
& ? [V_C7] :
( s__subclass(V_C7,V_C8)
& ? [V_C6] :
( s__subclass(V_C6,V_C7)
& ? [V_C5] :
( s__subclass(V_C5,V_C6)
& ? [V_C4] :
( s__subclass(V_C4,V_C5)
& ? [V_C3] :
( s__subclass(V_C3,V_C4)
& ? [V_C2] :
( s__subclass(V_C2,V_C3)
& s__subclass(V_C1,V_C2)
& s__instance(V_C10,s__SetOrClass)
& s__instance(V_C9,s__SetOrClass)
& s__instance(V_C8,s__SetOrClass)
& s__instance(V_C7,s__SetOrClass)
& s__instance(V_C6,s__SetOrClass)
& s__instance(V_C5,s__SetOrClass)
& s__instance(V_C4,s__SetOrClass)
& s__instance(V_C3,s__SetOrClass)
& s__instance(V_C2,s__SetOrClass)
& s__instance(V_C1,s__SetOrClass) ) ) ) ) ) ) ) ) ) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(miniscoping,[status(thm)],[f86672]) ).
fof(f86674,plain,
( ( s__instance(s__Creature50_1,sK1485_skl)
& s__subclass(sK1486_skl,s__Reptile)
& s__subclass(sK1487_skl,sK1486_skl)
& s__subclass(sK1488_skl,sK1487_skl)
& s__subclass(sK1489_skl,sK1488_skl)
& s__subclass(sK1490_skl,sK1489_skl)
& s__subclass(sK1491_skl,sK1490_skl)
& s__subclass(sK1492_skl,sK1491_skl)
& s__subclass(sK1493_skl,sK1492_skl)
& s__subclass(sK1494_skl,sK1493_skl)
& s__subclass(sK1485_skl,sK1494_skl)
& s__instance(sK1486_skl,s__SetOrClass)
& s__instance(sK1487_skl,s__SetOrClass)
& s__instance(sK1488_skl,s__SetOrClass)
& s__instance(sK1489_skl,s__SetOrClass)
& s__instance(sK1490_skl,s__SetOrClass)
& s__instance(sK1491_skl,s__SetOrClass)
& s__instance(sK1492_skl,s__SetOrClass)
& s__instance(sK1493_skl,s__SetOrClass)
& s__instance(sK1494_skl,s__SetOrClass)
& s__instance(sK1485_skl,s__SetOrClass) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1485_skl,sK1486_skl,sK1487_skl,sK1488_skl,sK1489_skl,sK1490_skl,sK1491_skl,sK1492_skl,sK1493_skl,sK1494_skl]),skolemize(V_C1,sK1485_skl),skolemize(V_C10,sK1486_skl),skolemize(V_C9,sK1487_skl),skolemize(V_C8,sK1488_skl),skolemize(V_C7,sK1489_skl),skolemize(V_C6,sK1490_skl),skolemize(V_C5,sK1491_skl),skolemize(V_C4,sK1492_skl),skolemize(V_C3,sK1493_skl),skolemize(V_C2,sK1494_skl)],[f86673]) ).
fof(f86678,plain,
( s__instance(sK1492_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86681,plain,
( s__instance(sK1489_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86683,plain,
( s__instance(sK1487_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86684,plain,
( s__instance(sK1486_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86685,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1485_skl,sK1494_skl) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86686,plain,
( s__subclass(sK1494_skl,sK1493_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86687,plain,
( s__subclass(sK1493_skl,sK1492_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86688,plain,
( s__subclass(sK1492_skl,sK1491_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86689,plain,
( s__subclass(sK1491_skl,sK1490_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86690,plain,
( s__subclass(sK1490_skl,sK1489_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86691,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1489_skl,sK1488_skl) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86692,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1488_skl,sK1487_skl) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86693,plain,
( s__subclass(sK1487_skl,sK1486_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86694,plain,
( s__subclass(sK1486_skl,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86695,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__instance(s__Creature50_1,sK1485_skl) ),
inference(cnf_transformation,[status(thm)],[f86674]) ).
fof(f86696,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[status(thm)],[f37985]) ).
fof(f87235,plain,
s__instance(s__Creature50_1,sK1485_skl),
inference(backward_subsumption_resolution,[status(thm)],[f86695,f74777]) ).
fof(f87392,plain,
s__subclass(sK1491_skl,sK1490_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86689,f74777]) ).
fof(f87395,plain,
s__instance(sK1491_skl,s__SetOrClass),
inference(resolution,[status(thm)],[f87392,f38026]) ).
fof(f87766,plain,
s__instance(sK1487_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f86683,f74777]) ).
fof(f87827,plain,
s__subclass(sK1490_skl,sK1489_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86690,f74777]) ).
fof(f87832,plain,
s__instance(sK1490_skl,s__SetOrClass),
inference(resolution,[status(thm)],[f87827,f38026]) ).
fof(f88033,plain,
s__subclass(sK1493_skl,sK1492_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86687,f74777]) ).
fof(f88037,plain,
s__instance(sK1493_skl,s__SetOrClass),
inference(resolution,[status(thm)],[f88033,f38026]) ).
fof(f88401,plain,
s__instance(sK1489_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f86681,f74777]) ).
fof(f88732,plain,
s__instance(sK1492_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f86678,f74777]) ).
fof(f88902,plain,
s__subclass(sK1485_skl,sK1494_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86685,f74777]) ).
fof(f88906,plain,
s__instance(sK1485_skl,s__SetOrClass),
inference(resolution,[status(thm)],[f88902,f38026]) ).
fof(f90361,plain,
s__instance(sK1494_skl,s__SetOrClass),
inference(resolution,[status(thm)],[f38027,f88902]) ).
fof(f91333,plain,
s__subclass(sK1489_skl,sK1488_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86691,f74777]) ).
fof(f91338,plain,
s__instance(sK1488_skl,s__SetOrClass),
inference(resolution,[status(thm)],[f91333,f38027]) ).
fof(f92263,plain,
s__subclass(sK1492_skl,sK1491_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86688,f74777]) ).
fof(f92275,plain,
s__subclass(sK1494_skl,sK1493_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86686,f74777]) ).
fof(f93402,plain,
s__instance(sK1486_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f86684,f74777]) ).
fof(f95104,plain,
! [X0,X1,X2] :
( ~ s__instance(X2,X0)
| s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[status(thm)],[f38030,f38027]) ).
fof(f95158,plain,
! [X0,X1] :
( ~ s__instance(X1,sK1486_skl)
| s__instance(X1,X0)
| ~ s__subclass(sK1486_skl,X0) ),
inference(resolution,[status(thm)],[f95104,f93402]) ).
fof(f95221,plain,
! [X0,X1] :
( ~ s__instance(X1,sK1488_skl)
| s__instance(X1,X0)
| ~ s__subclass(sK1488_skl,X0) ),
inference(resolution,[status(thm)],[f95104,f91338]) ).
fof(f95246,plain,
! [X0,X1] :
( ~ s__subclass(sK1494_skl,X1)
| ~ s__instance(X0,sK1494_skl)
| s__instance(X0,X1) ),
inference(resolution,[status(thm)],[f95104,f90361]) ).
fof(f95264,plain,
! [X0,X1] :
( s__instance(X1,X0)
| ~ s__instance(X1,sK1485_skl)
| ~ s__subclass(sK1485_skl,X0) ),
inference(resolution,[status(thm)],[f95104,f88906]) ).
fof(f95267,plain,
! [X0,X1] :
( ~ s__instance(X0,sK1492_skl)
| ~ s__subclass(sK1492_skl,X1)
| s__instance(X0,X1) ),
inference(resolution,[status(thm)],[f95104,f88732]) ).
fof(f95271,plain,
! [X0,X1] :
( s__instance(X1,X0)
| ~ s__instance(X1,sK1489_skl)
| ~ s__subclass(sK1489_skl,X0) ),
inference(resolution,[status(thm)],[f95104,f88401]) ).
fof(f95276,plain,
! [X0,X1] :
( ~ s__instance(X1,sK1493_skl)
| s__instance(X1,X0)
| ~ s__subclass(sK1493_skl,X0) ),
inference(resolution,[status(thm)],[f95104,f88037]) ).
fof(f95281,plain,
! [X0,X1] :
( s__instance(X1,X0)
| ~ s__instance(X1,sK1490_skl)
| ~ s__subclass(sK1490_skl,X0) ),
inference(resolution,[status(thm)],[f95104,f87832]) ).
fof(f95282,plain,
! [X0,X1] :
( ~ s__subclass(sK1487_skl,X1)
| s__instance(X0,X1)
| ~ s__instance(X0,sK1487_skl) ),
inference(resolution,[status(thm)],[f95104,f87766]) ).
fof(f95289,plain,
! [X0,X1] :
( ~ s__subclass(sK1491_skl,X1)
| ~ s__instance(X0,sK1491_skl)
| s__instance(X0,X1) ),
inference(resolution,[status(thm)],[f95104,f87395]) ).
fof(f95941,plain,
s__subclass(sK1486_skl,s__Reptile),
inference(forward_subsumption_resolution,[status(thm)],[f86694,f74777]) ).
fof(f96667,plain,
s__subclass(sK1488_skl,sK1487_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86692,f74777]) ).
fof(f103011,plain,
! [X0] :
( s__instance(s__Creature50_1,X0)
| ~ s__subclass(sK1485_skl,X0) ),
inference(resolution,[status(thm)],[f95264,f87235]) ).
fof(f103017,plain,
s__instance(s__Creature50_1,sK1494_skl),
inference(resolution,[status(thm)],[f103011,f88902]) ).
fof(f103018,plain,
! [X0] :
( s__instance(s__Creature50_1,X0)
| ~ s__subclass(sK1494_skl,X0) ),
inference(resolution,[status(thm)],[f103017,f95246]) ).
fof(f103053,plain,
s__instance(s__Creature50_1,sK1493_skl),
inference(resolution,[status(thm)],[f103018,f92275]) ).
fof(f103054,plain,
! [X0] :
( ~ s__subclass(sK1493_skl,X0)
| s__instance(s__Creature50_1,X0) ),
inference(resolution,[status(thm)],[f103053,f95276]) ).
fof(f103099,plain,
s__instance(s__Creature50_1,sK1492_skl),
inference(resolution,[status(thm)],[f103054,f88033]) ).
fof(f103118,plain,
! [X0] :
( ~ s__subclass(sK1492_skl,X0)
| s__instance(s__Creature50_1,X0) ),
inference(resolution,[status(thm)],[f103099,f95267]) ).
fof(f103129,plain,
s__instance(s__Creature50_1,sK1491_skl),
inference(resolution,[status(thm)],[f103118,f92263]) ).
fof(f103135,plain,
! [X0] :
( s__instance(s__Creature50_1,X0)
| ~ s__subclass(sK1491_skl,X0) ),
inference(resolution,[status(thm)],[f103129,f95289]) ).
fof(f103141,plain,
s__instance(s__Creature50_1,sK1490_skl),
inference(resolution,[status(thm)],[f103135,f87392]) ).
fof(f103371,plain,
! [X0] :
( ~ s__subclass(sK1490_skl,X0)
| s__instance(s__Creature50_1,X0) ),
inference(resolution,[status(thm)],[f95281,f103141]) ).
fof(f103393,plain,
s__instance(s__Creature50_1,sK1489_skl),
inference(resolution,[status(thm)],[f103371,f87827]) ).
fof(f103394,plain,
! [X0] :
( s__instance(s__Creature50_1,X0)
| ~ s__subclass(sK1489_skl,X0) ),
inference(resolution,[status(thm)],[f103393,f95271]) ).
fof(f103400,plain,
s__instance(s__Creature50_1,sK1488_skl),
inference(resolution,[status(thm)],[f103394,f91333]) ).
fof(f103402,plain,
! [X0] :
( s__instance(s__Creature50_1,X0)
| ~ s__subclass(sK1488_skl,X0) ),
inference(resolution,[status(thm)],[f103400,f95221]) ).
fof(f103403,plain,
s__instance(s__Creature50_1,sK1487_skl),
inference(resolution,[status(thm)],[f103402,f96667]) ).
fof(f103404,plain,
! [X0] :
( ~ s__subclass(sK1487_skl,X0)
| s__instance(s__Creature50_1,X0) ),
inference(resolution,[status(thm)],[f103403,f95282]) ).
fof(f103976,plain,
s__subclass(sK1487_skl,sK1486_skl),
inference(forward_subsumption_resolution,[status(thm)],[f86693,f74777]) ).
fof(f103977,plain,
s__instance(s__Creature50_1,sK1486_skl),
inference(resolution,[status(thm)],[f103976,f103404]) ).
fof(f103985,plain,
! [X0] :
( ~ s__subclass(sK1486_skl,X0)
| s__instance(s__Creature50_1,X0) ),
inference(resolution,[status(thm)],[f103977,f95158]) ).
fof(f103986,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolution,[status(thm)],[f103985,f95941]) ).
fof(f103987,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f103986,f86696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n004.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 15:01:57 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.95/6.20 % Drodi V4.1.1
% 94.82/18.14 % Refutation found
% 94.82/18.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 94.82/18.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 25.88/18.71 % Elapsed time: 13.300182 seconds
% 25.88/18.71 % CPU time: 96.068573 seconds
% 25.88/18.71 % Total memory used: 1.927 GB
% 25.88/18.71 % Net memory used: 1.918 GB
%------------------------------------------------------------------------------