%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV883-1 : TPTP v9.3.1. Released v4.1.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 02:49:43 PM UTC 2026
% Result : Unsatisfiable 257.90s 33.00s
% Output : CNFRefutation 218.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 18
% Syntax : Number of formulae : 62 ( 25 unt; 0 def)
% Number of atoms : 120 ( 21 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 122 ( 64 ~; 58 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-4 aty)
% Number of variables : 100 ( 100 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f404,axiom,
! [V_pn] :
( ~ c_in(V_pn,v_U,tc_Com_Opname)
| v_wt(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f439,axiom,
! [V_G,V_pn] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(hAPP(v_mgt__call,V_pn),V_G,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a)))
| hBOOL(hAPP(hAPP(v_P,V_G),c_Set_Oinsert(hAPP(v_mgt__call,V_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f491,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f519,axiom,
! [V_m,V_n] : c_HOL_Ominus__class_Ominus(c_Suc(V_m),c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f527,axiom,
! [V_m,V_n] :
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_HOL_Ominus__class_Ominus(c_Suc(V_m),V_n,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f536,axiom,
! [V_B,T_b,V_f,V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ c_lessequals(V_B,c_Set_Oimage(V_f,V_A,T_a,T_b),tc_fun(T_b,tc_bool))
| c_Finite__Set_Ofinite(V_B,T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f543,axiom,
! [V_x,V_S,T_a] :
( ~ hBOOL(hAPP(V_S,V_x))
| c_in(V_x,V_S,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f544,axiom,
! [V_S,V_x,T_a] :
( ~ c_in(V_x,V_S,T_a)
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f545,axiom,
! [V_x,V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_in(V_x,V_A,T_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_A,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(V_A,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f583,axiom,
! [V_x,V_A,T_b,V_f,T_a] :
( c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)
| ~ c_in(V_x,V_A,T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f587,negated_conjecture,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f588,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f589,negated_conjecture,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f590,negated_conjecture,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f591,negated_conjecture,
c_in(v_pn,v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f592,negated_conjecture,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f593,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_P,v_G),c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f594,negated_conjecture,
! [V_G,V_c] :
( ~ v_wt(V_c)
| hBOOL(hAPP(hAPP(v_P,V_G),c_Set_Oinsert(v_mgt(V_c),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),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))
| c_Finite__Set_Ocard(V_G,t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1245,plain,
! [X0] :
( ~ c_in(X0,v_U,tc_Com_Opname)
| v_wt(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom)) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f1301,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(hAPP(v_mgt__call,X1),X0,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a)))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(hAPP(v_mgt__call,X1),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f1386,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)],[f491]) ).
fof(f1387,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X3,X1,X2)
| c_lessequals(c_Set_Oinsert(X3,X0,X2),X1,tc_fun(X2,tc_bool))
| ~ c_lessequals(X0,X1,tc_fun(X2,tc_bool)) ),
inference(cnf_transformation,[status(thm)],[f1386]) ).
fof(f1423,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,X1,tc_nat) = c_HOL_Ominus__class_Ominus(c_Suc(X0),c_Suc(X1),tc_nat),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f1434,plain,
! [X0,X1] :
( ~ c_lessequals(X1,X0,tc_nat)
| c_HOL_Ominus__class_Ominus(c_Suc(X0),X1,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat)) ),
inference(cnf_transformation,[status(thm)],[f527]) ).
fof(f1448,plain,
! [V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ! [V_B,T_b] :
( ! [V_f] : ~ c_lessequals(V_B,c_Set_Oimage(V_f,V_A,T_a,T_b),tc_fun(T_b,tc_bool))
| c_Finite__Set_Ofinite(V_B,T_b) ) ),
inference(miniscoping,[status(thm)],[f536]) ).
fof(f1449,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_Finite__Set_Ofinite(X3,X4)
| ~ c_lessequals(X0,c_Set_Oimage(X2,X3,X4,X1),tc_fun(X1,tc_bool))
| c_Finite__Set_Ofinite(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1448]) ).
fof(f1458,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)],[f543]) ).
fof(f1459,plain,
! [X0,X1,X2] :
( c_in(X1,X0,X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1458]) ).
fof(f1460,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)],[f544]) ).
fof(f1461,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(X1,X0))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1460]) ).
fof(f1462,plain,
! [V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ! [V_x] :
( c_in(V_x,V_A,T_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_A,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(V_A,T_a)) ) ),
inference(miniscoping,[status(thm)],[f545]) ).
fof(f1463,plain,
! [X0,X1,X2] :
( c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| ~ c_Finite__Set_Ofinite(X1,X2)
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1462]) ).
fof(f1522,plain,
! [V_x,V_A,T_b] :
( ! [V_f,T_a] : c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)
| ~ c_in(V_x,V_A,T_b) ),
inference(miniscoping,[status(thm)],[f583]) ).
fof(f1523,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_in(X1,X2,X3)
| c_in(hAPP(X0,X1),c_Set_Oimage(X0,X2,X3,X4),X4) ),
inference(cnf_transformation,[status(thm)],[f1522]) ).
fof(f1530,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f1531,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)],[f588]) ).
fof(f1532,plain,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
inference(cnf_transformation,[status(thm)],[f589]) ).
fof(f1533,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
inference(cnf_transformation,[status(thm)],[f590]) ).
fof(f1534,plain,
c_in(v_pn,v_U,tc_Com_Opname),
inference(cnf_transformation,[status(thm)],[f591]) ).
fof(f1535,plain,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f1536,plain,
~ hBOOL(hAPP(hAPP(v_P,v_G),c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f1537,plain,
! [V_c] :
( ~ v_wt(V_c)
| ! [V_G] :
( hBOOL(hAPP(hAPP(v_P,V_G),c_Set_Oinsert(v_mgt(V_c),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),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))
| c_Finite__Set_Ocard(V_G,t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f594]) ).
fof(f1538,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat) != c_Finite__Set_Ocard(X0,t_a)
| ~ c_lessequals(X0,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))
| ~ v_wt(X1)
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(v_mgt(X1),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(cnf_transformation,[status(thm)],[f1537]) ).
fof(f1582,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) = c_Suc(c_Finite__Set_Ocard(v_G,t_a))
| ~ c_Finite__Set_Ofinite(v_G,t_a) ),
inference(resolution,[status(thm)],[f1535,f1463]) ).
fof(f1591,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X0,X1,X3)
| c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f1461,f1459]) ).
fof(f1626,plain,
( ~ c_Finite__Set_Ofinite(v_U,tc_Com_Opname)
| c_Finite__Set_Ofinite(v_G,t_a) ),
inference(resolution,[status(thm)],[f1449,f1531]) ).
fof(f1627,plain,
c_Finite__Set_Ofinite(v_G,t_a),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f1530]) ).
fof(f1640,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) = c_Suc(c_Finite__Set_Ocard(v_G,t_a)),
inference(backward_subsumption_resolution,[status(thm)],[f1582,f1627]) ).
fof(f1738,plain,
! [X0] :
( c_lessequals(c_Set_Oinsert(X0,v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))
| ~ c_in(X0,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a) ),
inference(resolution,[status(thm)],[f1387,f1531]) ).
fof(f1740,plain,
! [X0] :
( ~ c_in(X0,v_U,tc_Com_Opname)
| c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,X0),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
inference(resolution,[status(thm)],[f1738,f1523]) ).
fof(f1857,plain,
! [X0] : c_in(v_pn,v_U,X0),
inference(resolution,[status(thm)],[f1591,f1534]) ).
fof(f2202,plain,
c_HOL_Ominus__class_Ominus(c_Suc(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a)),c_Suc(v_na),tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat)),
inference(resolution,[status(thm)],[f1434,f1532]) ).
fof(f2208,plain,
c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat)),
inference(forward_demodulation,[status(thm)],[f1423,f2202]) ).
fof(f2209,plain,
c_Suc(c_Finite__Set_Ocard(v_G,t_a)) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat),
inference(forward_demodulation,[status(thm)],[f1533,f2208]) ).
fof(f2525,plain,
! [X0,X1] :
( ~ v_wt(X1)
| c_Suc(c_Finite__Set_Ocard(v_G,t_a)) != c_Finite__Set_Ocard(X0,t_a)
| ~ c_lessequals(X0,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(v_mgt(X1),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(backward_demodulation,[status(thm)],[f2209,f1538]) ).
fof(f3302,plain,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(resolution,[status(thm)],[f1301,f1536]) ).
fof(f4753,plain,
! [X0,X1] :
( c_Finite__Set_Ocard(X0,t_a) != c_Suc(c_Finite__Set_Ocard(v_G,t_a))
| ~ c_in(X1,v_U,tc_Com_Opname)
| ~ c_lessequals(X0,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(resolution,[status(thm)],[f1245,f2525]) ).
fof(f5352,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_Suc(c_Finite__Set_Ocard(v_G,t_a))
| ~ c_in(v_pn,v_U,tc_Com_Opname)
| ~ 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(resolution,[status(thm)],[f4753,f3302]) ).
fof(f5355,plain,
( c_Suc(c_Finite__Set_Ocard(v_G,t_a)) != c_Suc(c_Finite__Set_Ocard(v_G,t_a))
| ~ c_in(v_pn,v_U,tc_Com_Opname)
| ~ 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(forward_demodulation,[status(thm)],[f1640,f5352]) ).
fof(f5356,plain,
( ~ c_in(v_pn,v_U,tc_Com_Opname)
| ~ 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(trivial_equality_resolution,[status(thm)],[f5355]) ).
fof(f5357,plain,
~ c_in(v_pn,v_U,tc_Com_Opname),
inference(forward_subsumption_resolution,[status(thm)],[f5356,f1740]) ).
fof(f5522,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5357,f1857]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV883-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n004.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 09:30:04 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 257.90/33.00 % Refutation found
% 257.90/33.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 257.90/33.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 34.46/34.24 % Elapsed time: 33.670382 seconds
% 34.46/34.24 % CPU time: 250.754165 seconds
% 34.46/34.24 % Total memory used: 813.172 MB
% 34.46/34.24 % Net memory used: 738.282 MB
%------------------------------------------------------------------------------