%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG370-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 : n026.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 11:49:17 AM UTC 2026
% Result : Unsatisfiable 0.22s 0.68s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 18
% Syntax : Number of formulae : 65 ( 19 unt; 7 def)
% Number of atoms : 126 ( 15 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 111 ( 50 ~; 54 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-3 aty)
% Number of variables : 33 ( 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f80,axiom,
c_HOL_Oord__class_Oless(v_da____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [V_z,V_w] :
( ~ c_lessequals(V_z,V_w,tc_RealDef_Oreal)
| ~ c_lessequals(V_w,V_z,tc_RealDef_Oreal)
| V_z = V_w ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,axiom,
! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [V_x,V_y] :
( ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal)
| V_x = V_y
| c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f311,axiom,
! [V_i,V_k,V_j] :
( ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal)
| ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)
| c_lessequals(V_i,V_k,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f321,axiom,
! [V_w,V_z] :
( c_lessequals(V_z,V_w,tc_RealDef_Oreal)
| c_lessequals(V_w,V_z,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f364,axiom,
! [V_x,V_y] : c_RealVector_Odist__class_Odist(V_x,V_y,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_x,V_y,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f383,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f422,axiom,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f423,axiom,
c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f424,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f746,plain,
c_HOL_Oord__class_Oless(v_da____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f761,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(X1,X0,tc_RealDef_Oreal)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f956,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f957,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f1133,plain,
! [V_i,V_j] :
( ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal)
| ! [V_k] :
( ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)
| c_lessequals(V_i,V_k,tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f311]) ).
fof(f1134,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X0,X2,tc_RealDef_Oreal)
| ~ c_lessequals(X2,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1133]) ).
fof(f1150,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f1226,plain,
! [X0,X1] : c_RealVector_Odist__class_Odist(X0,X1,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f1247,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f1318,plain,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f1319,plain,
c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f1320,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f424]) ).
fof(f1521,plain,
c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f1226,f1319]) ).
fof(f1522,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f1226,f1320]) ).
fof(f1530,plain,
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = v_e ),
inference(resolution,[status(thm)],[f957,f1522]) ).
fof(f1532,definition,
( sQ0_spl
<=> c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = v_e ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1533,plain,
( ~ sQ0_spl
| c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = v_e ),
inference(component_clause,[status(thm)],[f1532]) ).
fof(f1535,definition,
( sQ1_spl
<=> c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1537,plain,
( sQ1_spl
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1535]) ).
fof(f1538,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1530,f1532,f1535]) ).
fof(f1540,plain,
( ~ sQ0_spl
| c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1533,f1521]) ).
fof(f1606,plain,
( ~ sQ0_spl
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal) = v_e ),
inference(resolution,[status(thm)],[f1540,f761]) ).
fof(f1607,definition,
( sQ4_spl
<=> c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal) = v_e ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1608,plain,
( ~ sQ4_spl
| c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal) = v_e ),
inference(component_clause,[status(thm)],[f1607]) ).
fof(f1610,definition,
( sQ5_spl
<=> c_lessequals(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1611,plain,
( ~ sQ5_spl
| c_lessequals(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1610]) ).
fof(f1612,plain,
( sQ5_spl
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1610]) ).
fof(f1613,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1606,f1607,f1610,f1532]) ).
fof(f1616,plain,
( sQ5_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1612,f956]) ).
fof(f1617,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1616,f1318]) ).
fof(f1618,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1617]) ).
fof(f1620,plain,
( ~ sQ4_spl
| c_HOL_Oord__class_Oless(v_e,v_e,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1608,f1318]) ).
fof(f1624,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1620,f1247]) ).
fof(f1625,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1624]) ).
fof(f1626,plain,
( ~ sQ5_spl
| ~ c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| v_e = c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1611,f761]) ).
fof(f1627,definition,
( sQ6_spl
<=> c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1629,plain,
( sQ6_spl
| ~ c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1627]) ).
fof(f1630,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1626,f1607,f1627,f1610]) ).
fof(f1631,plain,
! [X0] :
( sQ6_spl
| ~ c_lessequals(v_e,X0,tc_RealDef_Oreal)
| ~ c_lessequals(X0,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1629,f1134]) ).
fof(f1658,definition,
( sQ9_spl
<=> v_da____ = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1659,plain,
( ~ sQ9_spl
| v_da____ = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1658]) ).
fof(f1661,definition,
( sQ10_spl
<=> c_lessequals(v_da____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
( sQ10_spl
| ~ c_lessequals(v_da____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1661]) ).
fof(f1667,plain,
( sQ10_spl
| ~ c_HOL_Oord__class_Oless(v_da____,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1663,f956]) ).
fof(f1668,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1667,f746]) ).
fof(f1669,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1668]) ).
fof(f1677,plain,
( ~ sQ9_spl
| c_HOL_Oord__class_Oless(v_da____,v_da____,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1659,f746]) ).
fof(f1686,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1677,f1247]) ).
fof(f1687,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1686]) ).
fof(f1730,plain,
! [X0] :
( sQ6_spl
| c_lessequals(X0,v_e,tc_RealDef_Oreal)
| ~ c_lessequals(X0,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1631,f1150]) ).
fof(f1810,plain,
( sQ6_spl
| sQ1_spl
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1537,f1730]) ).
fof(f1814,plain,
( sQ6_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1810,f1521]) ).
fof(f1815,plain,
( sQ6_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1814]) ).
fof(f1816,plain,
$false,
inference(sat_refutation,[status(thm)],[f1538,f1613,f1618,f1625,f1630,f1669,f1687,f1815]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG370-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n026.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Mon Sep 21 13:20:37 UTC 2026
% 0.17/0.47 % CPUTime :
% 0.22/0.56 % Drodi V4.1.1
% 0.22/0.68 % Refutation found
% 0.22/0.68 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.22/0.72 % Elapsed time: 0.233641 seconds
% 0.22/0.72 % CPU time: 0.997455 seconds
% 0.22/0.72 % Total memory used: 140.130 MB
% 0.22/0.72 % Net memory used: 139.458 MB
%------------------------------------------------------------------------------