%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV621-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 02:49:14 PM UTC 2026
% Result : Unsatisfiable 31.99s 4.67s
% Output : CNFRefutation 31.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 87
% Syntax : Number of formulae : 301 ( 108 unt; 38 def)
% Number of atoms : 546 ( 135 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 454 ( 209 ~; 207 |; 0 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 54 ( 52 usr; 39 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-4 aty)
% Number of variables : 168 ( 168 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [T_a,V_y,V_x] :
( hBOOL(hAPP(c_lessequals(V_x,T_a),V_y))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [V_m,V_n] : c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) = c_HOL_Otimes__class_Otimes(V_n,V_m,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [V_m,V_n] :
( V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_m))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_n))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [T_a] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,axiom,
! [V_y,V_x] :
( V_x = V_y
| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,tc_nat),V_y))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,tc_nat),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,axiom,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n))
| ~ hBOOL(hAPP(c_lessequals(V_n,tc_nat),V_m))
| V_m = V_n ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f217,axiom,
! [V_x] : hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,tc_nat),c_Suc(V_x))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f370,axiom,
! [T_a] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(T_a),T_a) = c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f372,axiom,
! [T_a,V_a] :
( c_HOL_Otimes__class_Otimes(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__mult(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f384,axiom,
! [V_n] : c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f385,axiom,
! [V_m] : c_HOL_Otimes__class_Otimes(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f489,axiom,
! [V_n] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f497,axiom,
! [V_n] : hBOOL(hAPP(c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_n)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f518,axiom,
! [T_a,V_a,V_b] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),T_a) = c_HOL_Oinverse__class_Odivide(V_b,V_a,T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f536,axiom,
! [V_n] : c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f545,axiom,
! [T_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),T_a),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f547,axiom,
! [T_a,V_a,V_n] :
( V_a = c_HOL_Ozero__class_Ozero(T_a)
| c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(V_a,T_a),V_n),T_a) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),T_a),V_n)
| ~ class_Ring__and__Field_Odivision__ring(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f617,axiom,
! [V_n] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),V_n)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f625,axiom,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n))
| hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f656,axiom,
! [V_x] : hBOOL(hAPP(c_lessequals(V_x,tc_nat),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f728,axiom,
hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f729,axiom,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f748,axiom,
! [V_n,V_k] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_k,tc_nat),V_n))
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),tc_Complex_Ocomplex),V_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f754,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f756,axiom,
! [T_a,V_a] :
( c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f760,axiom,
! [T_a,V_x] :
( hAPP(c_Power_Opower__class_Opower(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f767,axiom,
! [T_a,V_a,V_b,V_c] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(V_a,V_c,T_a),c_HOL_Oinverse__class_Odivide(V_b,V_c,T_a),T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f769,axiom,
! [T_a,V_x] :
( c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f788,axiom,
! [T_a,V_x,V_n] :
( V_x = c_HOL_Oone__class_Oone(T_a)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(V_x,T_a),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,T_a) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(V_x,T_a),V_n),c_HOL_Oone__class_Oone(T_a),T_a),c_HOL_Ominus__class_Ominus(V_x,c_HOL_Oone__class_Oone(T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f789,negated_conjecture,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f801,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f802,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f803,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f807,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f810,axiom,
class_Ring__and__Field_Omult__zero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f812,axiom,
class_OrderedGroup_Omonoid__mult(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f815,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f820,axiom,
class_HOL_Oord(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f838,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f851,axiom,
class_Ring__and__Field_Omult__zero(tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f869,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f870,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f876,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f878,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f879,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f882,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f883,axiom,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f887,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f925,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_lessequals(X2,X0),X1))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f942,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) = c_HOL_Otimes__class_Otimes(X1,X0,tc_nat),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f994,plain,
! [V_n] :
( V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ! [V_m] : c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(miniscoping,[status(thm)],[f66]) ).
fof(f995,plain,
! [X0,X1] :
( X1 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(cnf_transformation,[status(thm)],[f994]) ).
fof(f1014,plain,
! [V_m] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_m))
| ! [V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_n))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat))) ) ),
inference(miniscoping,[status(thm)],[f81]) ).
fof(f1015,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X1))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(X0,X1,tc_nat))) ),
inference(cnf_transformation,[status(thm)],[f1014]) ).
fof(f1160,plain,
! [X0] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f1196,plain,
! [X0,X1] :
( X1 = X0
| hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1)) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f1200,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_lessequals(X0,tc_nat),X1))
| ~ hBOOL(hAPP(c_lessequals(X1,tc_nat),X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f1217,plain,
! [X0] : hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),c_Suc(X0))),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f1472,plain,
! [X0] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(X0),X0) = c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f1475,plain,
! [T_a] :
( ! [V_a] : c_HOL_Otimes__class_Otimes(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__mult(T_a) ),
inference(miniscoping,[status(thm)],[f372]) ).
fof(f1476,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(X0),X0) = X1
| ~ class_OrderedGroup_Omonoid__mult(X0) ),
inference(cnf_transformation,[status(thm)],[f1475]) ).
fof(f1493,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f1494,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f1652,plain,
! [X0] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(cnf_transformation,[status(thm)],[f489]) ).
fof(f1661,plain,
! [X0] : hBOOL(hAPP(c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0)),
inference(cnf_transformation,[status(thm)],[f497]) ).
fof(f1702,plain,
! [T_a] :
( ! [V_a,V_b] : c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),T_a) = c_HOL_Oinverse__class_Odivide(V_b,V_a,T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(miniscoping,[status(thm)],[f518]) ).
fof(f1703,plain,
! [X0,X1,X2] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X0) = c_HOL_Oinverse__class_Odivide(X2,X1,X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f1702]) ).
fof(f1735,plain,
! [X0] : c_FFT__Mirabelle_Oroot(X0) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f536]) ).
fof(f1745,plain,
! [X0] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),X0),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(thm)],[f545]) ).
fof(f1747,plain,
! [T_a,V_a] :
( V_a = c_HOL_Ozero__class_Ozero(T_a)
| ! [V_n] : c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(V_a,T_a),V_n),T_a) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),T_a),V_n)
| ~ class_Ring__and__Field_Odivision__ring(T_a) ),
inference(miniscoping,[status(thm)],[f547]) ).
fof(f1748,plain,
! [X0,X1,X2] :
( X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X1,X0),X0),X2)
| ~ class_Ring__and__Field_Odivision__ring(X0) ),
inference(cnf_transformation,[status(thm)],[f1747]) ).
fof(f1860,plain,
! [X0] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X0)),
inference(cnf_transformation,[status(thm)],[f617]) ).
fof(f1869,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1))
| hBOOL(hAPP(c_lessequals(X0,tc_nat),X1)) ),
inference(cnf_transformation,[status(thm)],[f625]) ).
fof(f1920,plain,
! [X0] : hBOOL(hAPP(c_lessequals(X0,tc_nat),X0)),
inference(cnf_transformation,[status(thm)],[f656]) ).
fof(f2032,plain,
hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)),
inference(cnf_transformation,[status(thm)],[f728]) ).
fof(f2033,plain,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n)),
inference(cnf_transformation,[status(thm)],[f729]) ).
fof(f2060,plain,
! [V_k] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k))
| ! [V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_k,tc_nat),V_n))
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),tc_Complex_Ocomplex),V_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ),
inference(miniscoping,[status(thm)],[f748]) ).
fof(f2061,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X1))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0))
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(cnf_transformation,[status(thm)],[f2060]) ).
fof(f2071,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)],[f754]) ).
fof(f2073,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(miniscoping,[status(thm)],[f756]) ).
fof(f2074,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(X0),X0) = X1
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f2073]) ).
fof(f2081,plain,
! [T_a] :
( ! [V_x] : hAPP(c_Power_Opower__class_Opower(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f760]) ).
fof(f2082,plain,
! [X0,X1] :
( hAPP(c_Power_Opower__class_Opower(X1,X0),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f2081]) ).
fof(f2093,plain,
! [T_a] :
( ! [V_a,V_b,V_c] : c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(V_a,V_c,T_a),c_HOL_Oinverse__class_Odivide(V_b,V_c,T_a),T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(miniscoping,[status(thm)],[f767]) ).
fof(f2094,plain,
! [X0,X1,X2,X3] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X2,X0),X3,X0) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X1,X3,X0),c_HOL_Oinverse__class_Odivide(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f2093]) ).
fof(f2097,plain,
! [T_a] :
( ! [V_x] : c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
inference(miniscoping,[status(thm)],[f769]) ).
fof(f2098,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X1,X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_OrderedGroup_Oab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f2097]) ).
fof(f2132,plain,
! [T_a,V_x] :
( V_x = c_HOL_Oone__class_Oone(T_a)
| ! [V_n] : c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(V_x,T_a),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,T_a) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(V_x,T_a),V_n),c_HOL_Oone__class_Oone(T_a),T_a),c_HOL_Ominus__class_Ominus(V_x,c_HOL_Oone__class_Oone(T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(miniscoping,[status(thm)],[f788]) ).
fof(f2133,plain,
! [X0,X1,X2] :
( X1 = c_HOL_Oone__class_Oone(X0)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(X1,X0),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat),tc_nat,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(X1,X0),X2),c_HOL_Oone__class_Oone(X0),X0),c_HOL_Ominus__class_Ominus(X1,c_HOL_Oone__class_Oone(X0),X0),X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f2132]) ).
fof(f2134,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f789]) ).
fof(f2152,plain,
class_Ring__and__Field_Ono__zero__divisors(tc_nat),
inference(cnf_transformation,[status(thm)],[f801]) ).
fof(f2153,plain,
class_Ring__and__Field_Oordered__semidom(tc_nat),
inference(cnf_transformation,[status(thm)],[f802]) ).
fof(f2154,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_nat),
inference(cnf_transformation,[status(thm)],[f803]) ).
fof(f2158,plain,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
inference(cnf_transformation,[status(thm)],[f807]) ).
fof(f2161,plain,
class_Ring__and__Field_Omult__zero(tc_nat),
inference(cnf_transformation,[status(thm)],[f810]) ).
fof(f2163,plain,
class_OrderedGroup_Omonoid__mult(tc_nat),
inference(cnf_transformation,[status(thm)],[f812]) ).
fof(f2166,plain,
class_Orderings_Olinorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f815]) ).
fof(f2171,plain,
class_HOL_Oord(tc_nat),
inference(cnf_transformation,[status(thm)],[f820]) ).
fof(f2189,plain,
class_Ring__and__Field_Ono__zero__divisors(tc_Int_Oint),
inference(cnf_transformation,[status(thm)],[f838]) ).
fof(f2202,plain,
class_Ring__and__Field_Omult__zero(tc_Int_Oint),
inference(cnf_transformation,[status(thm)],[f851]) ).
fof(f2220,plain,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f869]) ).
fof(f2221,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f870]) ).
fof(f2227,plain,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f876]) ).
fof(f2229,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f878]) ).
fof(f2230,plain,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f879]) ).
fof(f2233,plain,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f882]) ).
fof(f2234,plain,
class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f883]) ).
fof(f2238,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f887]) ).
fof(f2316,definition,
( sQ4_spl
<=> class_Orderings_Olinorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2318,plain,
( sQ4_spl
| ~ class_Orderings_Olinorder(tc_nat) ),
inference(component_clause,[status(thm)],[f2316]) ).
fof(f2487,definition,
! [X0] :
( sQ20_spl
<=> hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f2488,plain,
! [X0] :
( ~ sQ20_spl
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0)) ),
inference(component_clause,[status(thm)],[f2487]) ).
fof(f2797,plain,
! [X0] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(X0,v_k,tc_nat))) ),
inference(resolution,[status(thm)],[f2032,f1015]) ).
fof(f2806,plain,
! [X0] : hAPP(c_Power_Opower__class_Opower(X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(tc_nat),
inference(resolution,[status(thm)],[f2154,f2082]) ).
fof(f2883,plain,
! [X0,X1] :
( X0 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(paramodulation,[status(thm)],[f942,f995]) ).
fof(f2910,plain,
! [X0,X1,X2] : c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X0,X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2094,f2238]) ).
fof(f2915,plain,
! [X0,X1] :
( X0 = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f2133,f2238]) ).
fof(f3220,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2166,f2318]) ).
fof(f3221,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f3220]) ).
fof(f4327,definition,
! [X0] :
( sQ120_spl
<=> ( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),tc_nat))) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f4328,plain,
! [X0] :
( ~ sQ120_spl
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),tc_nat))) ),
inference(component_clause,[status(thm)],[f4327]) ).
fof(f4374,plain,
! [X0] :
( ~ sQ120_spl
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat))) ),
inference(forward_demodulation,[status(thm)],[f1493,f4328]) ).
fof(f4375,plain,
! [X0] :
( ~ sQ120_spl
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))) ),
inference(forward_demodulation,[status(thm)],[f1494,f4374]) ).
fof(f4376,plain,
! [X0] :
( ~ sQ120_spl
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4375,f1652]) ).
fof(f4857,plain,
c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f1160,f2221]) ).
fof(f4867,definition,
( sQ134_spl
<=> class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f4868,plain,
( ~ sQ134_spl
| class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f4867]) ).
fof(f4869,plain,
( sQ134_spl
| ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f4867]) ).
fof(f5531,plain,
hBOOL(hAPP(c_lessequals(v_k,tc_nat),v_n)),
inference(resolution,[status(thm)],[f2033,f1869]) ).
fof(f5532,plain,
( ~ hBOOL(hAPP(c_lessequals(v_n,tc_nat),v_k))
| v_n = v_k ),
inference(resolution,[status(thm)],[f5531,f1200]) ).
fof(f5536,definition,
( sQ149_spl
<=> v_n = v_k ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f5537,plain,
( ~ sQ149_spl
| v_n = v_k ),
inference(component_clause,[status(thm)],[f5536]) ).
fof(f5539,definition,
( sQ150_spl
<=> hBOOL(hAPP(c_lessequals(v_n,tc_nat),v_k)) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f5541,plain,
( sQ150_spl
| ~ hBOOL(hAPP(c_lessequals(v_n,tc_nat),v_k)) ),
inference(component_clause,[status(thm)],[f5539]) ).
fof(f5542,plain,
( ~ sQ150_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f5532,f5536,f5539]) ).
fof(f5577,plain,
( ~ sQ149_spl
| hBOOL(hAPP(c_HOL_Oord__class_Oless(v_n,tc_nat),v_n)) ),
inference(backward_demodulation,[status(thm)],[f5537,f2033]) ).
fof(f5641,plain,
( ~ sQ149_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5577,f1860]) ).
fof(f5647,plain,
~ sQ149_spl,
inference(contradiction_clause,[status(thm)],[f5641]) ).
fof(f6349,definition,
( sQ169_spl
<=> class_Ring__and__Field_Oordered__semidom(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f6351,plain,
( sQ169_spl
| ~ class_Ring__and__Field_Oordered__semidom(tc_nat) ),
inference(component_clause,[status(thm)],[f6349]) ).
fof(f6360,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6351,f2153]) ).
fof(f6361,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f6360]) ).
fof(f6680,definition,
( sQ183_spl
<=> class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f6682,plain,
( sQ183_spl
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f6680]) ).
fof(f6692,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6682,f2221]) ).
fof(f6693,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f6692]) ).
fof(f7695,plain,
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1472,f2238]) ).
fof(f7696,definition,
( sQ215_spl
<=> c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f7697,plain,
( ~ sQ215_spl
| c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f7696]) ).
fof(f7699,plain,
( sQ215_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f7695,f6680,f7696]) ).
fof(f7701,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = X0,
inference(resolution,[status(thm)],[f1476,f2163]) ).
fof(f8220,plain,
( sQ134_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2227,f4869]) ).
fof(f8221,plain,
sQ134_spl,
inference(contradiction_clause,[status(thm)],[f8220]) ).
fof(f10528,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2071,f2230]) ).
fof(f10530,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Oone__class_Oone(tc_nat),
inference(resolution,[status(thm)],[f2071,f2158]) ).
fof(f10769,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1703,f2238]) ).
fof(f10770,definition,
! [X0,X1] :
( sQ308_spl
<=> c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f10771,plain,
! [X0,X1] :
( ~ sQ308_spl
| c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f10770]) ).
fof(f10773,plain,
( sQ308_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f10769,f6680,f10770]) ).
fof(f10875,definition,
( sQ312_spl
<=> hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat))) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f11133,plain,
! [X0,X1] :
( ~ sQ134_spl
| X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) ),
inference(resolution,[status(thm)],[f1748,f4868]) ).
fof(f11314,plain,
( ~ class_Ring__and__Field_Oordered__semidom(tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat)
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat))) ),
inference(resolution,[status(thm)],[f1196,f1745]) ).
fof(f11324,definition,
( sQ339_spl
<=> c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition]) ).
fof(f11325,plain,
( ~ sQ339_spl
| c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(component_clause,[status(thm)],[f11324]) ).
fof(f11327,plain,
( ~ sQ169_spl
| sQ339_spl
| sQ312_spl ),
inference(split_clause,[status(thm)],[f11314,f10875,f11324,f6349]) ).
fof(f11331,plain,
( ~ sQ339_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11325,f10530]) ).
fof(f11332,plain,
~ sQ339_spl,
inference(contradiction_clause,[status(thm)],[f11331]) ).
fof(f11378,definition,
( sQ349_spl
<=> class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f11380,plain,
( sQ349_spl
| ~ class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f11378]) ).
fof(f11381,definition,
( sQ350_spl
<=> class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition]) ).
fof(f11383,plain,
( sQ350_spl
| ~ class_Ring__and__Field_Omult__zero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f11381]) ).
fof(f11388,definition,
( sQ352_spl
<=> class_Ring__and__Field_Ono__zero__divisors(tc_Int_Oint) ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f11390,plain,
( sQ352_spl
| ~ class_Ring__and__Field_Ono__zero__divisors(tc_Int_Oint) ),
inference(component_clause,[status(thm)],[f11388]) ).
fof(f11391,definition,
( sQ353_spl
<=> class_Ring__and__Field_Omult__zero(tc_Int_Oint) ),
introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition]) ).
fof(f11393,plain,
( sQ353_spl
| ~ class_Ring__and__Field_Omult__zero(tc_Int_Oint) ),
inference(component_clause,[status(thm)],[f11391]) ).
fof(f11398,definition,
( sQ355_spl
<=> class_Ring__and__Field_Ono__zero__divisors(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition]) ).
fof(f11400,plain,
( sQ355_spl
| ~ class_Ring__and__Field_Ono__zero__divisors(tc_nat) ),
inference(component_clause,[status(thm)],[f11398]) ).
fof(f11401,definition,
( sQ356_spl
<=> class_Ring__and__Field_Omult__zero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f11403,plain,
( sQ356_spl
| ~ class_Ring__and__Field_Omult__zero(tc_nat) ),
inference(component_clause,[status(thm)],[f11401]) ).
fof(f11408,plain,
( sQ356_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11403,f2161]) ).
fof(f11409,plain,
sQ356_spl,
inference(contradiction_clause,[status(thm)],[f11408]) ).
fof(f11410,plain,
( sQ355_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11400,f2152]) ).
fof(f11411,plain,
sQ355_spl,
inference(contradiction_clause,[status(thm)],[f11410]) ).
fof(f11412,plain,
( sQ353_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11393,f2202]) ).
fof(f11413,plain,
sQ353_spl,
inference(contradiction_clause,[status(thm)],[f11412]) ).
fof(f11414,plain,
( sQ352_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11390,f2189]) ).
fof(f11415,plain,
sQ352_spl,
inference(contradiction_clause,[status(thm)],[f11414]) ).
fof(f11416,plain,
( sQ350_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11383,f2234]) ).
fof(f11417,plain,
sQ350_spl,
inference(contradiction_clause,[status(thm)],[f11416]) ).
fof(f11418,plain,
( sQ349_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11380,f2220]) ).
fof(f11419,plain,
sQ349_spl,
inference(contradiction_clause,[status(thm)],[f11418]) ).
fof(f11546,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat) = X0,
inference(paramodulation,[status(thm)],[f942,f7701]) ).
fof(f11743,definition,
( sQ372_spl
<=> v_k = c_HOL_Ozero__class_Ozero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f11744,plain,
( ~ sQ372_spl
| v_k = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(component_clause,[status(thm)],[f11743]) ).
fof(f11760,plain,
( ~ sQ372_spl
| hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_k)) ),
inference(backward_demodulation,[status(thm)],[f11744,f2032]) ).
fof(f11800,plain,
( ~ sQ372_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11760,f1860]) ).
fof(f11801,plain,
~ sQ372_spl,
inference(contradiction_clause,[status(thm)],[f11800]) ).
fof(f11921,definition,
( sQ377_spl
<=> c_HOL_Ozero__class_Ozero(tc_nat) = hAPP(c_Power_Opower__class_Opower(v_k,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition]) ).
fof(f11922,plain,
( ~ sQ377_spl
| c_HOL_Ozero__class_Ozero(tc_nat) = hAPP(c_Power_Opower__class_Opower(v_k,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(component_clause,[status(thm)],[f11921]) ).
fof(f12210,definition,
( sQ380_spl
<=> hAPP(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition]) ).
fof(f12211,plain,
( ~ sQ380_spl
| hAPP(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(component_clause,[status(thm)],[f12210]) ).
fof(f12215,plain,
( ~ sQ380_spl
| c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(forward_demodulation,[status(thm)],[f2806,f12211]) ).
fof(f12216,plain,
( ~ sQ380_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12215,f10530]) ).
fof(f12217,plain,
~ sQ380_spl,
inference(contradiction_clause,[status(thm)],[f12216]) ).
fof(f12565,plain,
( sQ150_spl
| hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n))
| ~ class_Orderings_Olinorder(tc_nat) ),
inference(resolution,[status(thm)],[f5541,f925]) ).
fof(f12576,definition,
( sQ416_spl
<=> hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n)) ),
introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition]) ).
fof(f12579,plain,
( sQ150_spl
| sQ416_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f12565,f2316,f12576,f5539]) ).
fof(f12631,definition,
( sQ422_spl
<=> hBOOL(hAPP(c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f12633,plain,
( sQ422_spl
| ~ hBOOL(hAPP(c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)) ),
inference(component_clause,[status(thm)],[f12631]) ).
fof(f12640,plain,
( sQ422_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12633,f1661]) ).
fof(f12641,plain,
sQ422_spl,
inference(contradiction_clause,[status(thm)],[f12640]) ).
fof(f12707,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat)))
| hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)) ),
inference(paramodulation,[status(thm)],[f11546,f2797]) ).
fof(f12718,definition,
( sQ428_spl
<=> hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f12721,plain,
( ~ sQ312_spl
| sQ428_spl ),
inference(split_clause,[status(thm)],[f12707,f12718,f10875]) ).
fof(f12760,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0,
inference(resolution,[status(thm)],[f2074,f2238]) ).
fof(f12767,definition,
( sQ430_spl
<=> c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f12768,plain,
( ~ sQ430_spl
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f12767]) ).
fof(f12772,plain,
( ~ sQ430_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12768,f10528]) ).
fof(f12773,plain,
~ sQ430_spl,
inference(contradiction_clause,[status(thm)],[f12772]) ).
fof(f12801,definition,
( sQ434_spl
<=> hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))) ),
introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition]) ).
fof(f12803,plain,
( sQ434_spl
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))) ),
inference(component_clause,[status(thm)],[f12801]) ).
fof(f12889,plain,
( ~ sQ20_spl
| $false ),
inference(resolution,[status(thm)],[f2488,f1652]) ).
fof(f12895,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f12889]) ).
fof(f12969,plain,
( ~ sQ120_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2032,f4376]) ).
fof(f12982,plain,
~ sQ120_spl,
inference(contradiction_clause,[status(thm)],[f12969]) ).
fof(f13064,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2098,f2233]) ).
fof(f13413,plain,
( sQ434_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12803,f1217]) ).
fof(f13414,plain,
sQ434_spl,
inference(contradiction_clause,[status(thm)],[f13413]) ).
fof(f13778,definition,
! [X0,X1] :
( sQ478_spl
<=> c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ478_spl])],[split_symbol_definition]) ).
fof(f13779,plain,
! [X0,X1] :
( ~ sQ478_spl
| c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(component_clause,[status(thm)],[f13778]) ).
fof(f13863,plain,
( ~ sQ377_spl
| c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Oone__class_Oone(tc_nat) ),
inference(forward_demodulation,[status(thm)],[f2806,f11922]) ).
fof(f13864,plain,
( ~ sQ377_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13863,f10530]) ).
fof(f13865,plain,
~ sQ377_spl,
inference(contradiction_clause,[status(thm)],[f13864]) ).
fof(f13874,plain,
c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
inference(resolution,[status(thm)],[f2883,f11546]) ).
fof(f13886,definition,
! [X0] :
( sQ481_spl
<=> X0 != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition]) ).
fof(f13887,plain,
! [X0] :
( ~ sQ481_spl
| X0 != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(component_clause,[status(thm)],[f13886]) ).
fof(f13891,plain,
( ~ sQ481_spl
| $false ),
inference(destructive_equality_resolution,[status(thm)],[f13887]) ).
fof(f13892,plain,
~ sQ481_spl,
inference(contradiction_clause,[status(thm)],[f13891]) ).
fof(f14037,definition,
( sQ484_spl
<=> hBOOL(hAPP(c_lessequals(c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat))) ),
introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition]) ).
fof(f14039,plain,
( sQ484_spl
| ~ hBOOL(hAPP(c_lessequals(c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat))) ),
inference(component_clause,[status(thm)],[f14037]) ).
fof(f14043,plain,
( sQ484_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14039,f1920]) ).
fof(f14044,plain,
sQ484_spl,
inference(contradiction_clause,[status(thm)],[f14043]) ).
fof(f14084,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f13064,f2910]) ).
fof(f14092,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f13064,f14084]) ).
fof(f14132,plain,
hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2915,f2134]) ).
fof(f14155,definition,
( sQ493_spl
<=> c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition]) ).
fof(f14157,plain,
( sQ493_spl
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f14155]) ).
fof(f14162,plain,
( sQ493_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f14157]) ).
fof(f14163,plain,
sQ493_spl,
inference(contradiction_clause,[status(thm)],[f14162]) ).
fof(f14219,plain,
! [X0] :
( ~ sQ308_spl
| c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f14092,f10771]) ).
fof(f14222,plain,
! [X0] :
( ~ sQ308_spl
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f4857,f14219]) ).
fof(f14261,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f14132,f2134]) ).
fof(f14265,plain,
( ~ sQ134_spl
| c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k) ),
inference(paramodulation,[status(thm)],[f14132,f11133]) ).
fof(f14268,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f14132,f14261]) ).
fof(f14269,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f14132,f14268]) ).
fof(f14270,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f13064,f14269]) ).
fof(f14271,plain,
( ~ sQ308_spl
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f14222,f14270]) ).
fof(f14281,definition,
( sQ497_spl
<=> c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k) ),
introduced(definition,[new_symbols(definition,[sQ497_spl])],[split_symbol_definition]) ).
fof(f14282,plain,
( ~ sQ497_spl
| c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k) ),
inference(component_clause,[status(thm)],[f14281]) ).
fof(f14284,definition,
( sQ498_spl
<=> c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ498_spl])],[split_symbol_definition]) ).
fof(f14285,plain,
( ~ sQ498_spl
| c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f14284]) ).
fof(f14287,plain,
( ~ sQ134_spl
| sQ498_spl
| sQ497_spl ),
inference(split_clause,[status(thm)],[f14265,f14281,f14284,f4867]) ).
fof(f14299,plain,
( ~ sQ497_spl
| ~ sQ215_spl
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k) ),
inference(forward_demodulation,[status(thm)],[f7697,f14282]) ).
fof(f14300,plain,
( ~ sQ497_spl
| ~ sQ215_spl
| ~ sQ308_spl
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k) ),
inference(forward_demodulation,[status(thm)],[f10771,f14299]) ).
fof(f14301,plain,
( ~ sQ497_spl
| ~ sQ215_spl
| ~ sQ308_spl
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k) ),
inference(forward_demodulation,[status(thm)],[f12760,f14300]) ).
fof(f14305,plain,
( ~ sQ497_spl
| ~ sQ215_spl
| ~ sQ308_spl
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n))
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f14301,f2061]) ).
fof(f14312,definition,
( sQ502_spl
<=> c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f14313,plain,
( ~ sQ502_spl
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f14312]) ).
fof(f14315,plain,
( ~ sQ497_spl
| ~ sQ215_spl
| ~ sQ308_spl
| ~ sQ428_spl
| ~ sQ416_spl
| sQ502_spl ),
inference(split_clause,[status(thm)],[f14305,f14312,f12576,f12718,f10770,f7696,f14281]) ).
fof(f14328,definition,
( sQ506_spl
<=> c_FFT__Mirabelle_Oroot(v_n) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f14329,plain,
( ~ sQ506_spl
| c_FFT__Mirabelle_Oroot(v_n) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f14328]) ).
fof(f14343,plain,
( ~ sQ506_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14329,f1735]) ).
fof(f14344,plain,
~ sQ506_spl,
inference(contradiction_clause,[status(thm)],[f14343]) ).
fof(f14348,plain,
( ~ sQ502_spl
| ~ sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14313,f14271]) ).
fof(f14349,plain,
( ~ sQ502_spl
| ~ sQ308_spl ),
inference(contradiction_clause,[status(thm)],[f14348]) ).
fof(f14680,definition,
( sQ537_spl
<=> class_HOL_Oord(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ537_spl])],[split_symbol_definition]) ).
fof(f14682,plain,
( sQ537_spl
| ~ class_HOL_Oord(tc_nat) ),
inference(component_clause,[status(thm)],[f14680]) ).
fof(f14683,definition,
( sQ538_spl
<=> class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition]) ).
fof(f14685,plain,
( sQ538_spl
| ~ class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f14683]) ).
fof(f14694,plain,
( sQ538_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14685,f2229]) ).
fof(f14695,plain,
sQ538_spl,
inference(contradiction_clause,[status(thm)],[f14694]) ).
fof(f14696,plain,
( sQ537_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14682,f2171]) ).
fof(f14697,plain,
sQ537_spl,
inference(contradiction_clause,[status(thm)],[f14696]) ).
fof(f16100,plain,
! [X0,X1] :
( ~ sQ478_spl
| c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) != c_HOL_Oone__class_Oone(tc_nat) ),
inference(forward_demodulation,[status(thm)],[f13874,f13779]) ).
fof(f16101,plain,
( ~ sQ478_spl
| $false ),
inference(resolution,[status(thm)],[f16100,f11546]) ).
fof(f16112,plain,
~ sQ478_spl,
inference(contradiction_clause,[status(thm)],[f16101]) ).
fof(f16115,definition,
( sQ633_spl
<=> c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Oone__class_Oone(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition]) ).
fof(f16117,plain,
( sQ633_spl
| c_HOL_Oone__class_Oone(tc_nat) != c_HOL_Oone__class_Oone(tc_nat) ),
inference(component_clause,[status(thm)],[f16115]) ).
fof(f16119,plain,
( sQ633_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16117]) ).
fof(f16120,plain,
sQ633_spl,
inference(contradiction_clause,[status(thm)],[f16119]) ).
fof(f16431,definition,
( sQ656_spl
<=> c_FFT__Mirabelle_Oroot(v_k) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f16432,plain,
( ~ sQ656_spl
| c_FFT__Mirabelle_Oroot(v_k) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f16431]) ).
fof(f16443,plain,
( ~ sQ656_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16432,f1735]) ).
fof(f16444,plain,
~ sQ656_spl,
inference(contradiction_clause,[status(thm)],[f16443]) ).
fof(f16771,plain,
( ~ sQ498_spl
| ~ sQ308_spl
| c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f14285,f10771]) ).
fof(f16773,plain,
( ~ sQ498_spl
| ~ sQ308_spl
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f4857,f16771]) ).
fof(f16774,plain,
( ~ sQ498_spl
| ~ sQ308_spl
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_FFT__Mirabelle_Oroot(v_n) ),
inference(forward_demodulation,[status(thm)],[f12760,f16773]) ).
fof(f16775,plain,
( ~ sQ498_spl
| ~ sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16774,f1735]) ).
fof(f16776,plain,
( ~ sQ498_spl
| ~ sQ308_spl ),
inference(contradiction_clause,[status(thm)],[f16775]) ).
fof(f16777,plain,
$false,
inference(sat_refutation,[status(thm)],[f3221,f5542,f5647,f6361,f6693,f7699,f8221,f10773,f11327,f11332,f11409,f11411,f11413,f11415,f11417,f11419,f11801,f12217,f12579,f12641,f12721,f12773,f12895,f12982,f13414,f13865,f13892,f14044,f14163,f14287,f14315,f14344,f14349,f14695,f14697,f16112,f16120,f16444,f16776]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV621-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n026.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 09:17:21 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.28/0.57 % Drodi V4.1.1
% 31.99/4.67 % Refutation found
% 31.99/4.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 31.99/4.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 31.99/4.76 % Elapsed time: 4.294513 seconds
% 31.99/4.76 % CPU time: 32.830107 seconds
% 31.99/4.76 % Total memory used: 360.474 MB
% 31.99/4.76 % Net memory used: 349.332 MB
%------------------------------------------------------------------------------