%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG408-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 : n007.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:22 AM UTC 2026
% Result : Unsatisfiable 57.88s 7.87s
% Output : CNFRefutation 29.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 20
% Syntax : Number of formulae : 82 ( 27 unt; 0 def)
% Number of atoms : 195 ( 51 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 213 ( 100 ~; 113 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-3 aty)
% Number of variables : 66 ( 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f61,axiom,
! [T_a,V_x] :
( V_x = c_HOL_Ozero__class_Ozero(T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(V_x,T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [T_a,V_x] :
( V_x = c_HOL_Ozero__class_Ozero(T_a)
| c_RealVector_Onorm__class_Onorm(V_x,T_a) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [T_a,V_n,V_x] :
( ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(V_x,V_n,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ c_Parity_Oeven__odd__class_Oeven(V_n,tc_nat)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f241,axiom,
! [T_a,V_x,V_n] :
( c_Parity_Oeven__odd__class_Oeven(V_n,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(V_x,V_n,T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f390,axiom,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(V_x,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f391,axiom,
! [V_x] :
( c_Parity_Oeven__odd__class_Oeven(V_x,tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Suc(V_x),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f654,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f948,axiom,
! [T_a,V_a,V_n] :
( V_a = c_HOL_Ozero__class_Ozero(T_a)
| c_Power_Opower__class_Opower(V_a,V_n,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f954,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/sandbox/benchmark/theBenchmark.p') ).
fof(f960,axiom,
! [V_z,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal)
| ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(c_HOL_Otimes__class_Otimes(V_z,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1074,axiom,
! [V_n] : c_Suc(V_n) = c_HOL_Oplus__class_Oplus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1126,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/sandbox/benchmark/theBenchmark.p') ).
fof(f1226,axiom,
v_w____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1227,axiom,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1230,axiom,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1231,negated_conjecture,
~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1337,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1373,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1419,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1603,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f1783,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(X0)
| c_RealVector_Onorm__class_Onorm(X1,X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f1786,plain,
! [T_a,V_n] :
( ! [V_x] : ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(V_x,V_n,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ c_Parity_Oeven__odd__class_Oeven(V_n,tc_nat)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f1787,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(X2,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ c_Parity_Oeven__odd__class_Oeven(X1,tc_nat)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f1786]) ).
fof(f1841,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f1885,plain,
! [V_n] :
( c_Parity_Oeven__odd__class_Oeven(V_n,tc_nat)
| ! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(V_x,V_n,T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ) ),
inference(miniscoping,[status(thm)],[f241]) ).
fof(f1886,plain,
! [X0,X1,X2] :
( c_Parity_Oeven__odd__class_Oeven(X2,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_Power_Opower__class_Opower(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f1885]) ).
fof(f2122,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(X0),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f2123,plain,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(X0,tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Suc(X0),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f2529,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f654]) ).
fof(f3003,plain,
! [T_a,V_a] :
( V_a = c_HOL_Ozero__class_Ozero(T_a)
| ! [V_n] : c_Power_Opower__class_Opower(V_a,V_n,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(T_a) ),
inference(miniscoping,[status(thm)],[f948]) ).
fof(f3004,plain,
! [X0,X1,X2] :
( X1 = c_HOL_Ozero__class_Ozero(X0)
| c_Power_Opower__class_Opower(X1,X2,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(X0) ),
inference(cnf_transformation,[status(thm)],[f3003]) ).
fof(f3014,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)],[f954]) ).
fof(f3023,plain,
! [V_z] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal)
| ! [V_x,V_y] :
( ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(c_HOL_Otimes__class_Otimes(V_z,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f960]) ).
fof(f3024,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(X1,X2,tc_RealDef_Oreal)
| c_lessequals(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f3023]) ).
fof(f3209,plain,
! [X0] : c_Suc(X0) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(cnf_transformation,[status(thm)],[f1074]) ).
fof(f3295,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1126]) ).
fof(f3480,plain,
v_w____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1226]) ).
fof(f3481,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1227]) ).
fof(f3484,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1230]) ).
fof(f3485,plain,
~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1231]) ).
fof(f3591,plain,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1337]) ).
fof(f3627,plain,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1373]) ).
fof(f3673,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1419]) ).
fof(f3904,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3014,f3295]) ).
fof(f3946,plain,
! [X0,X1] :
( X1 = X0
| c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3904,f3014]) ).
fof(f3948,plain,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(duplicate_literals_removal,[status(thm)],[f3946]) ).
fof(f10537,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3209,f3484]) ).
fof(f10582,plain,
~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3209,f3485]) ).
fof(f10873,plain,
~ c_lessequals(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f10537,f10582]) ).
fof(f10952,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f10873,f3024]) ).
fof(f10963,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f10952,f3024]) ).
fof(f10974,plain,
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f10963,f1841]) ).
fof(f10975,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f10974,f3024]) ).
fof(f10986,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f10975,f3481]) ).
fof(f11079,plain,
( c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f10986,f3948]) ).
fof(f15640,plain,
( c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1787,f11079]) ).
fof(f15647,plain,
( c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f15640,f3627]) ).
fof(f21650,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3004,f15647]) ).
fof(f21657,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f21650,f3591]) ).
fof(f23289,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1886,f21657]) ).
fof(f23290,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1886,f10986]) ).
fof(f23323,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f23289,f3627]) ).
fof(f23324,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f23290,f3627]) ).
fof(f23337,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f23323,f1841]) ).
fof(f23338,plain,
( v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat) ),
inference(resolution,[status(thm)],[f23337,f1783]) ).
fof(f23339,plain,
( v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f23338,f2122]) ).
fof(f23340,plain,
( v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f23339,f3673]) ).
fof(f23341,plain,
( c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f23340,f2123]) ).
fof(f23342,plain,
c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f23341,f3480]) ).
fof(f23676,plain,
( c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f23324,f3948]) ).
fof(f24229,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Parity_Oeven__odd__class_Oeven(c_Suc(v_k____),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f23676,f1787]) ).
fof(f24239,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f24229,f2122]) ).
fof(f24244,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f24239,f3627]) ).
fof(f24245,plain,
( v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| ~ c_Parity_Oeven__odd__class_Oeven(v_k____,tc_nat)
| c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f24244,f1603]) ).
fof(f24249,plain,
( v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f24245,f23342]) ).
fof(f24253,plain,
( v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f24249,f3673]) ).
fof(f24254,plain,
( v_t____ = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal)
| v_w____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f24253,f3004]) ).
fof(f24301,plain,
( v_t____ = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f24254,f3480]) ).
fof(f24611,plain,
c_HOL_Oord__class_Oless(v_t____,v_t____,tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f24613,f1841]) ).
fof(f24613,plain,
v_t____ = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f24301,f3591]) ).
fof(f24844,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f24611,f2529]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG408-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 13:17:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.23/0.47 % Drodi V4.1.1
% 57.88/7.87 % Refutation found
% 57.88/7.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 57.88/7.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 55.67/9.11 % Elapsed time: 8.520409 seconds
% 55.67/9.11 % CPU time: 57.543570 seconds
% 55.67/9.11 % Total memory used: 509.104 MB
% 55.67/9.11 % Net memory used: 488.312 MB
%------------------------------------------------------------------------------