%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV884-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:49:43 PM UTC 2026
% Result : Unsatisfiable 10.29s 1.81s
% Output : CNFRefutation 11.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 30
% Syntax : Number of formulae : 100 ( 31 unt; 11 def)
% Number of atoms : 176 ( 5 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 140 ( 64 ~; 65 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-4 aty)
% Number of variables : 104 ( 104 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f53,axiom,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f408,axiom,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f409,axiom,
! [V_c,V_A,T_a,V_B] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f418,axiom,
! [V_c,V_A,V_B,T_a] :
( ~ c_in(V_c,V_A,T_a)
| c_in(V_c,V_B,T_a)
| c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f986,axiom,
! [V_x,V_A,T_a,V_B] :
( ~ c_in(V_x,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f993,axiom,
! [V_h,V_F,T_a,T_b] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1020,axiom,
! [V_x,V_S,T_a] :
( ~ hBOOL(hAPP(V_S,V_x))
| c_in(V_x,V_S,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1021,axiom,
! [V_S,V_x,T_a] :
( ~ c_in(V_x,V_S,T_a)
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1051,axiom,
! [V_x,V_A,T_aa,V_f,T_a] :
( c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a)
| ~ c_in(V_x,V_A,T_aa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1056,negated_conjecture,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1057,negated_conjecture,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1060,negated_conjecture,
c_in(v_pn,v_U,tc_Com_Opname),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1062,negated_conjecture,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1085,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1086,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1092,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1101,axiom,
class_Divides_Osemiring__div(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1103,axiom,
class_Ring__and__Field_Odvd(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1108,axiom,
class_Orderings_Obot(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1206,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f1792,plain,
! [V_c,V_B,T_a] :
( ! [V_A] : ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(miniscoping,[status(thm)],[f408]) ).
fof(f1793,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1792]) ).
fof(f1794,plain,
! [V_c,V_A,T_a] :
( ! [V_B] : ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| c_in(V_c,V_A,T_a) ),
inference(miniscoping,[status(thm)],[f409]) ).
fof(f1795,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X1,X3,tc_fun(X2,tc_bool)),X2)
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1794]) ).
fof(f1812,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,V_A,T_a)
| ! [V_B] :
( c_in(V_c,V_B,T_a)
| c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ) ),
inference(miniscoping,[status(thm)],[f418]) ).
fof(f1813,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X0,X1,X3)
| c_in(X0,X2,X3)
| c_in(X0,c_HOL_Ominus__class_Ominus(X1,X2,tc_fun(X3,tc_bool)),X3) ),
inference(cnf_transformation,[status(thm)],[f1812]) ).
fof(f2694,plain,
! [V_x,T_a,V_B] :
( ~ c_in(V_x,V_B,T_a)
| ! [V_A] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ) ),
inference(miniscoping,[status(thm)],[f986]) ).
fof(f2695,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| c_lessequals(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool)) ),
inference(cnf_transformation,[status(thm)],[f2694]) ).
fof(f2703,plain,
! [V_F,T_a] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| ! [V_h,T_b] : c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
inference(miniscoping,[status(thm)],[f993]) ).
fof(f2704,plain,
! [X0,X1,X2,X3] :
( ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ofinite(c_Set_Oimage(X0,X1,X2,X3),X3) ),
inference(cnf_transformation,[status(thm)],[f2703]) ).
fof(f2740,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : c_in(V_x,V_S,T_a) ),
inference(miniscoping,[status(thm)],[f1020]) ).
fof(f2741,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X1,X0))
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2740]) ).
fof(f2742,plain,
! [V_S,V_x] :
( ! [T_a] : ~ c_in(V_x,V_S,T_a)
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f1021]) ).
fof(f2743,plain,
! [X0,X1,X2] :
( ~ c_in(X1,X0,X2)
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f2742]) ).
fof(f2792,plain,
! [V_x,V_A,T_aa] :
( ! [V_f,T_a] : c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a)
| ~ c_in(V_x,V_A,T_aa) ),
inference(miniscoping,[status(thm)],[f1051]) ).
fof(f2793,plain,
! [X0,X1,X2,X3,X4] :
( c_in(hAPP(X3,X0),c_Set_Oimage(X3,X1,X2,X4),X4)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2792]) ).
fof(f2802,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
inference(cnf_transformation,[status(thm)],[f1056]) ).
fof(f2803,plain,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(cnf_transformation,[status(thm)],[f1057]) ).
fof(f2806,plain,
c_in(v_pn,v_U,tc_Com_Opname),
inference(cnf_transformation,[status(thm)],[f1060]) ).
fof(f2808,plain,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f2841,plain,
class_Ring__and__Field_Oordered__semidom(tc_nat),
inference(cnf_transformation,[status(thm)],[f1085]) ).
fof(f2842,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f2848,plain,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
inference(cnf_transformation,[status(thm)],[f1092]) ).
fof(f2857,plain,
class_Divides_Osemiring__div(tc_nat),
inference(cnf_transformation,[status(thm)],[f1101]) ).
fof(f2859,plain,
class_Ring__and__Field_Odvd(tc_nat),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f2864,plain,
class_Orderings_Obot(tc_nat),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f3351,plain,
! [X0] :
( c_in(v_pn,X0,tc_Com_Opname)
| c_in(v_pn,c_HOL_Ominus__class_Ominus(v_U,X0,tc_fun(tc_Com_Opname,tc_bool)),tc_Com_Opname) ),
inference(resolution,[status(thm)],[f1813,f2806]) ).
fof(f3399,plain,
! [X0] :
( c_in(v_pn,v_U,tc_Com_Opname)
| c_in(v_pn,X0,tc_Com_Opname) ),
inference(resolution,[status(thm)],[f3351,f1795]) ).
fof(f3402,definition,
! [X0] :
( sQ9_spl
<=> c_in(v_pn,X0,tc_Com_Opname) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f3403,plain,
! [X0] :
( ~ sQ9_spl
| c_in(v_pn,X0,tc_Com_Opname) ),
inference(component_clause,[status(thm)],[f3402]) ).
fof(f3405,definition,
( sQ10_spl
<=> c_in(v_pn,v_U,tc_Com_Opname) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f3406,plain,
( ~ sQ10_spl
| c_in(v_pn,v_U,tc_Com_Opname) ),
inference(component_clause,[status(thm)],[f3405]) ).
fof(f3408,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f3399,f3402,f3405]) ).
fof(f3410,plain,
! [X0] :
( ~ sQ9_spl
| ~ c_in(v_pn,X0,tc_Com_Opname) ),
inference(resolution,[status(thm)],[f3403,f1793]) ).
fof(f3412,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3410,f3403]) ).
fof(f3413,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f3412]) ).
fof(f3540,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Oone__class_Oone(tc_nat),
inference(resolution,[status(thm)],[f1206,f2848]) ).
fof(f4084,definition,
( sQ46_spl
<=> c_Finite__Set_Ofinite(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f4086,plain,
( sQ46_spl
| ~ c_Finite__Set_Ofinite(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a) ),
inference(component_clause,[status(thm)],[f4084]) ).
fof(f4131,definition,
( sQ52_spl
<=> c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f4133,plain,
( sQ52_spl
| ~ c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
inference(component_clause,[status(thm)],[f4131]) ).
fof(f4135,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4133,f2803]) ).
fof(f4136,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f4135]) ).
fof(f4149,definition,
( sQ53_spl
<=> class_Ring__and__Field_Odvd(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f4151,plain,
( sQ53_spl
| ~ class_Ring__and__Field_Odvd(tc_nat) ),
inference(component_clause,[status(thm)],[f4149]) ).
fof(f4156,definition,
( sQ55_spl
<=> class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f4158,plain,
( sQ55_spl
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ),
inference(component_clause,[status(thm)],[f4156]) ).
fof(f4164,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4158,f2842]) ).
fof(f4165,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f4164]) ).
fof(f4329,plain,
( sQ46_spl
| ~ c_Finite__Set_Ofinite(v_U,tc_Com_Opname) ),
inference(resolution,[status(thm)],[f4086,f2704]) ).
fof(f4331,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4329,f2802]) ).
fof(f4332,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f4331]) ).
fof(f4384,plain,
( ~ sQ10_spl
| hBOOL(hAPP(v_U,v_pn)) ),
inference(resolution,[status(thm)],[f2743,f3406]) ).
fof(f4398,plain,
! [X0] :
( ~ sQ10_spl
| c_in(v_pn,v_U,X0) ),
inference(resolution,[status(thm)],[f4384,f2741]) ).
fof(f4528,definition,
( sQ71_spl
<=> class_Divides_Osemiring__div(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f4530,plain,
( sQ71_spl
| ~ class_Divides_Osemiring__div(tc_nat) ),
inference(component_clause,[status(thm)],[f4528]) ).
fof(f4535,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4530,f2857]) ).
fof(f4536,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f4535]) ).
fof(f5331,plain,
( ~ c_in(hAPP(v_mgt__call,v_pn),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a)
| ~ c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
inference(resolution,[status(thm)],[f2695,f2808]) ).
fof(f5335,definition,
( sQ98_spl
<=> c_in(hAPP(v_mgt__call,v_pn),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f5337,plain,
( sQ98_spl
| ~ c_in(hAPP(v_mgt__call,v_pn),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a) ),
inference(component_clause,[status(thm)],[f5335]) ).
fof(f5338,plain,
( ~ sQ98_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f5331,f4131,f5335]) ).
fof(f5491,definition,
( sQ104_spl
<=> c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f5492,plain,
( ~ sQ104_spl
| c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(component_clause,[status(thm)],[f5491]) ).
fof(f5758,definition,
( sQ112_spl
<=> class_Orderings_Obot(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f5760,plain,
( sQ112_spl
| ~ class_Orderings_Obot(tc_nat) ),
inference(component_clause,[status(thm)],[f5758]) ).
fof(f5765,definition,
( sQ114_spl
<=> class_Ring__and__Field_Oordered__semidom(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f5767,plain,
( sQ114_spl
| ~ class_Ring__and__Field_Oordered__semidom(tc_nat) ),
inference(component_clause,[status(thm)],[f5765]) ).
fof(f5776,plain,
( sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5767,f2841]) ).
fof(f5777,plain,
sQ114_spl,
inference(contradiction_clause,[status(thm)],[f5776]) ).
fof(f5778,plain,
( ~ sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5492,f3540]) ).
fof(f5779,plain,
~ sQ104_spl,
inference(contradiction_clause,[status(thm)],[f5778]) ).
fof(f5855,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4151,f2859]) ).
fof(f5856,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f5855]) ).
fof(f6002,plain,
( sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5760,f2864]) ).
fof(f6003,plain,
sQ112_spl,
inference(contradiction_clause,[status(thm)],[f6002]) ).
fof(f6032,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| c_in(hAPP(X0,v_pn),c_Set_Oimage(X0,v_U,X1,X2),X2) ),
inference(resolution,[status(thm)],[f2793,f4398]) ).
fof(f6038,plain,
( sQ98_spl
| ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5337,f6032]) ).
fof(f6039,plain,
( sQ98_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f6038]) ).
fof(f6040,plain,
$false,
inference(sat_refutation,[status(thm)],[f3408,f3413,f4136,f4165,f4332,f4536,f5338,f5777,f5779,f5856,f6003,f6039]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV884-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n010.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 09:30:25 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.38 % Drodi V4.1.1
% 10.29/1.81 % Refutation found
% 10.29/1.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.29/1.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.06/1.87 % Elapsed time: 1.512319 seconds
% 11.06/1.87 % CPU time: 11.487320 seconds
% 11.06/1.87 % Total memory used: 292.379 MB
% 11.06/1.87 % Net memory used: 283.206 MB
%------------------------------------------------------------------------------