%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV618-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 : Tue Sep 29 01:19:06 PM UTC 2026
% Result : Unsatisfiable 11.54s 2.36s
% Output : Refutation 12.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 54
% Syntax : Number of formulae : 257 ( 89 unt; 18 def)
% Number of atoms : 521 ( 257 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 477 ( 213 ~; 256 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 9 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 15 con; 0-4 aty)
% Number of variables : 203 ( 0 sgn 203 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) = c_HOL_Otimes__class_Otimes(X1,X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__mult__commute_0) ).
fof(f166,axiom,
c_SetInterval_Oord__class_OlessThan(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lessThan__0_0) ).
fof(f273,axiom,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__algebra(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__left_Ozero_0) ).
fof(f274,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ class_RealVector_Oreal__normed__algebra(X0) ),
inference(reorient_equations,[],[f273]) ).
fof(f523,axiom,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(X0),X1,X0) = X1
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I11_J_0) ).
fof(f567,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0),X3) = hAPP(c_Power_Opower__class_Opower(X1,X0),c_HOL_Otimes__class_Otimes(X2,X3,tc_nat)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Opwr__pwr_0) ).
fof(f568,plain,
! [X2,X3,X0,X1] :
( hAPP(c_Power_Opower__class_Opower(X1,X0),c_HOL_Otimes__class_Otimes(X2,X3,tc_nat)) = hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0),X3)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(reorient_equations,[],[f567]) ).
fof(f580,axiom,
! [X2,X3,X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__frac__num_0) ).
fof(f596,axiom,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__less__one_0) ).
fof(f629,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| X1 = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X2,X0)
| X2 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_divide__eq__eq_0) ).
fof(f630,plain,
! [X2,X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X2,X0) = X1
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Ozero__class_Ozero(X0) = X2 ),
inference(reorient_equations,[],[f629]) ).
fof(f681,axiom,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f697,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0) = hAPP(c_Power_Opower__class_Opower(X1,X0),c_Suc(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I27_J_0) ).
fof(f698,plain,
! [X2,X0,X1] :
( hAPP(c_Power_Opower__class_Opower(X1,X0),c_Suc(X2)) = c_HOL_Otimes__class_Otimes(X1,hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(reorient_equations,[],[f697]) ).
fof(f797,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_Finite__Set_Osetsum(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_setsum__empty_0) ).
fof(f798,plain,
! [X2,X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_Finite__Set_Osetsum(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(reorient_equations,[],[f797]) ).
fof(f808,axiom,
! [X0,X1] :
( c_HOL_Oinverse__class_Oinverse(X1,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(X0),X1,X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inverse__eq__divide_0) ).
fof(f814,axiom,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_SetInterval_Oord__class_OlessThan(X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeast0LessThan_0) ).
fof(f816,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_k,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_k_I1_J_0) ).
fof(f817,axiom,
c_HOL_Oord__class_Oless(v_k,v_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_k_I2_J_0) ).
fof(f843,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(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)
| X1 = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_geometric__sum_0) ).
fof(f844,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(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)
| c_HOL_Oone__class_Oone(X0) = X1 ),
inference(reorient_equations,[],[f843]) ).
fof(f845,axiom,
! [X0,X1] :
( 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)
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__summation_0) ).
fof(f846,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = 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_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
inference(reorient_equations,[],[f845]) ).
fof(f847,axiom,
! [X0] : c_FFT__Mirabelle_Oroot(X0) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__nonzero_0) ).
fof(f848,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_FFT__Mirabelle_Oroot(X0),
inference(reorient_equations,[],[f847]) ).
fof(f854,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Omonoid__mult(X0)
| hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(X0),X0),X1) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__one_0) ).
fof(f855,plain,
! [X0,X1] :
( c_HOL_Oone__class_Oone(X0) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(X0),X0),X1)
| ~ class_OrderedGroup_Omonoid__mult(X0) ),
inference(reorient_equations,[],[f854]) ).
fof(f866,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| hAPP(c_Power_Opower__class_Opower(X1,X0),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Opwr__0_0) ).
fof(f867,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Oone__class_Oone(X0) = hAPP(c_Power_Opower__class_Opower(X1,X0),c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(reorient_equations,[],[f866]) ).
fof(f870,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oring__1__no__zero__divisors(X0)
| hAPP(c_Power_Opower__class_Opower(X1,X0),X2) != c_HOL_Ozero__class_Ozero(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_field__power__not__zero_0) ).
fof(f871,plain,
! [X2,X0,X1] :
( hAPP(c_Power_Opower__class_Opower(X1,X0),X2) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(X0)
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f870]) ).
fof(f874,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X0),X3) = c_HOL_Oinverse__class_Odivide(hAPP(c_Power_Opower__class_Opower(X1,X0),X3),hAPP(c_Power_Opower__class_Opower(X2,X0),X3),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__divide_0) ).
fof(f875,axiom,
! [X0] : hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X0) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__unity_0) ).
fof(f876,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X0),
inference(reorient_equations,[],[f875]) ).
fof(f879,axiom,
! [X2,X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(X0),hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(X0),X1,X0),X0),X2)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__one__over_0) ).
fof(f884,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Oinverse__class_Odivide(X1,X1,X0) = c_HOL_Oone__class_Oone(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_divide__self_0) ).
fof(f885,plain,
! [X0,X1] :
( c_HOL_Oone__class_Oone(X0) = c_HOL_Oinverse__class_Odivide(X1,X1,X0)
| ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f884]) ).
fof(f894,axiom,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__field(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_divide_Ozero_0) ).
fof(f895,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ class_RealVector_Oreal__normed__field(X0) ),
inference(reorient_equations,[],[f894]) ).
fof(f896,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_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f897,plain,
c_HOL_Ozero__class_Ozero(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(reorient_equations,[],[f896]) ).
fof(f910,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Ring__and__Field_Oordered__semidom) ).
fof(f975,axiom,
class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Oring__1__no__zero__divisors) ).
fof(f978,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero) ).
fof(f979,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f980,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__algebra) ).
fof(f985,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__field) ).
fof(f986,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__add) ).
fof(f992,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult) ).
fof(f995,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
fof(f1005,definition,
sF0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1006,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1005]) ).
fof(f1007,definition,
sF1 = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1008,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF1,
inference(reorient_equations,[],[f1007]) ).
fof(f1009,definition,
sF2 = c_FFT__Mirabelle_Oroot(v_n),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1010,plain,
c_FFT__Mirabelle_Oroot(v_n) = sF2,
inference(reorient_equations,[],[f1009]) ).
fof(f1011,definition,
sF3 = c_HOL_Oinverse__class_Odivide(sF1,sF2,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1012,plain,
c_HOL_Oinverse__class_Odivide(sF1,sF2,tc_Complex_Ocomplex) = sF3,
inference(reorient_equations,[],[f1011]) ).
fof(f1013,definition,
sF4 = c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1014,plain,
c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex) = sF4,
inference(reorient_equations,[],[f1013]) ).
fof(f1015,definition,
sF5 = hAPP(sF4,v_k),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1016,plain,
hAPP(sF4,v_k) = sF5,
inference(reorient_equations,[],[f1015]) ).
fof(f1017,definition,
sF6 = c_Power_Opower__class_Opower(sF5,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1018,plain,
c_Power_Opower__class_Opower(sF5,tc_Complex_Ocomplex) = sF6,
inference(reorient_equations,[],[f1017]) ).
fof(f1019,definition,
sF7 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1020,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF7,
inference(reorient_equations,[],[f1019]) ).
fof(f1021,definition,
sF8 = c_SetInterval_Oord__class_OatLeastLessThan(sF7,v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1022,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF7,v_n,tc_nat) = sF8,
inference(reorient_equations,[],[f1021]) ).
fof(f1023,definition,
sF9 = c_Finite__Set_Osetsum(sF6,sF8,tc_nat,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1024,plain,
c_Finite__Set_Osetsum(sF6,sF8,tc_nat,tc_Complex_Ocomplex) = sF9,
inference(reorient_equations,[],[f1023]) ).
fof(f1025,plain,
sF0 != sF9,
inference(definition_folding,[],[f897,f1024,f1022,f1020,f1018,f1016,f1014,f1012,f1010,f1008,f1006]) ).
fof(f1027,plain,
! [X2,X0,X1] :
( 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) = c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(X1,X0),c_SetInterval_Oord__class_OlessThan(X2,tc_nat),tc_nat,X0)
| ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Oone__class_Oone(X0) = X1 ),
inference(backward_demodulation,[],[f844,f814]) ).
fof(f1028,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = 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_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
inference(backward_demodulation,[],[f846,f814]) ).
fof(f1032,plain,
! [X0] : c_FFT__Mirabelle_Oroot(X0) != sF0,
inference(backward_demodulation,[],[f848,f1006]) ).
fof(f1033,plain,
! [X0] : hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X0) = sF1,
inference(backward_demodulation,[],[f876,f1008]) ).
fof(f1034,plain,
sF3 = c_HOL_Oinverse__class_Odivide(sF1,c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1012,f1010]) ).
fof(f1048,plain,
c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)) = c_SetInterval_Oord__class_OlessThan(sF7,tc_nat),
inference(backward_demodulation,[],[f166,f1020]) ).
fof(f1070,plain,
! [X0] : c_SetInterval_Oord__class_OlessThan(X0,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF7,X0,tc_nat),
inference(backward_demodulation,[],[f814,f1020]) ).
fof(f1071,plain,
c_HOL_Oord__class_Oless(sF7,v_k,tc_nat),
inference(backward_demodulation,[],[f816,f1020]) ).
fof(f1079,plain,
! [X0,X1] :
( c_HOL_Oone__class_Oone(X0) = hAPP(c_Power_Opower__class_Opower(X1,X0),sF7)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(backward_demodulation,[],[f867,f1020]) ).
fof(f1082,plain,
! [X0,X1] :
( sF0 = 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_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat) ),
inference(forward_demodulation,[],[f1028,f1006]) ).
fof(f1087,plain,
sF8 = c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),
inference(backward_demodulation,[],[f1022,f1070]) ).
fof(f1100,plain,
! [X0,X1] :
( sF0 = 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_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(sF7,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
inference(forward_demodulation,[],[f1082,f1020]) ).
fof(f1106,plain,
! [X0] :
( sF0 = c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),X0),tc_Complex_Ocomplex),sF8,tc_nat,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(sF7,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(superposition,[],[f1100,f1087]) ).
fof(f1107,plain,
! [X0] :
( sF0 = c_HOL_Oinverse__class_Odivide(sF0,X0,tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex) ),
inference(superposition,[],[f895,f1006]) ).
fof(f1117,plain,
! [X0] : sF0 = c_HOL_Oinverse__class_Odivide(sF0,X0,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f1107,f985]) ).
fof(f1123,plain,
! [X0,X1] :
( hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Oinverse__class_Odivide(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),hAPP(sF4,X1),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(superposition,[],[f874,f1014]) ).
fof(f1126,plain,
! [X0,X1] :
( hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Oinverse__class_Odivide(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),hAPP(sF4,X1),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f1123,f978]) ).
fof(f1132,plain,
! [X0,X1] : hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1) = c_HOL_Oinverse__class_Odivide(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),hAPP(sF4,X1),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f1126,f995]) ).
fof(f1137,plain,
! [X0] :
( c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(superposition,[],[f808,f1008]) ).
fof(f1138,plain,
! [X0] : c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,X0,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f1137,f995]) ).
fof(f1139,plain,
sF3 = c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),
inference(backward_demodulation,[],[f1034,f1138]) ).
fof(f1144,plain,
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(superposition,[],[f885,f1138]) ).
fof(f1154,plain,
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(forward_subsumption_resolution,[],[f1144,f995]) ).
fof(f1156,plain,
( sF1 = c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(forward_demodulation,[],[f1154,f1008]) ).
fof(f1158,plain,
( sF0 = sF1
| sF1 = c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex) ),
inference(forward_demodulation,[],[f1156,f1006]) ).
fof(f1160,definition,
( spl10_3
<=> sF1 = c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition]) ).
fof(f1162,plain,
( sF1 = c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex)
| ~ spl10_3 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1164,definition,
( spl10_4
<=> sF0 = sF1 ),
introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition]) ).
fof(f1165,plain,
( sF0 != sF1
| spl10_4 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1166,plain,
( sF0 = sF1
| ~ spl10_4 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1168,plain,
( spl10_3
| spl10_4 ),
inference(avatar_split_clause,[],[f1158,f1164,f1160]) ).
fof(f1173,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(sF1,hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(sF1,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(superposition,[],[f879,f1008]) ).
fof(f1182,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(sF1,hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(sF1,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f1173,f978]) ).
fof(f1183,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(sF1,hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(sF1,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1),
inference(forward_subsumption_resolution,[],[f1182,f995]) ).
fof(f1184,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(sF1,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(forward_demodulation,[],[f1183,f1138]) ).
fof(f1185,plain,
! [X0,X1] : 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(forward_demodulation,[],[f1184,f1138]) ).
fof(f1187,plain,
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(sF6,sF7)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f1079,f1018]) ).
fof(f1198,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(sF6,sF7),
inference(forward_subsumption_resolution,[],[f1187,f979]) ).
fof(f1200,plain,
sF1 = hAPP(sF6,sF7),
inference(forward_demodulation,[],[f1198,f1008]) ).
fof(f1231,plain,
! [X0,X1] :
( hAPP(sF4,c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)) = hAPP(c_Power_Opower__class_Opower(hAPP(sF4,X0),tc_Complex_Ocomplex),X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f568,f1014]) ).
fof(f1257,plain,
! [X0,X1] : hAPP(sF4,c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)) = hAPP(c_Power_Opower__class_Opower(hAPP(sF4,X0),tc_Complex_Ocomplex),X1),
inference(forward_subsumption_resolution,[],[f1231,f979]) ).
fof(f1311,plain,
! [X0] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(sF6,X0),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF5 ),
inference(superposition,[],[f1027,f1018]) ).
fof(f1326,plain,
! [X0] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(sF6,X0),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF5 ),
inference(forward_subsumption_resolution,[],[f1311,f995]) ).
fof(f1329,plain,
! [X0] :
( c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(sF6,X0),sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF5 ),
inference(forward_demodulation,[],[f1326,f1008]) ).
fof(f1332,plain,
! [X0] :
( sF1 = sF5
| c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(sF6,X0),sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(forward_demodulation,[],[f1329,f1008]) ).
fof(f1342,definition,
( spl10_8
<=> ! [X0] : c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(sF6,X0),sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl10_8])],[avatar_definition]) ).
fof(f1343,plain,
( ! [X0] : c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(sF6,X0),sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl10_8 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1345,definition,
( spl10_9
<=> sF1 = sF5 ),
introduced(definition,[new_symbols(definition,[spl10_9])],[avatar_definition]) ).
fof(f1347,plain,
( sF1 = sF5
| ~ spl10_9 ),
inference(avatar_component_clause,[],[f1345]) ).
fof(f1348,plain,
( spl10_8
| spl10_9 ),
inference(avatar_split_clause,[],[f1332,f1345,f1342]) ).
fof(f1427,plain,
! [X0] : hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),X0) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),X0),tc_Complex_Ocomplex),
inference(superposition,[],[f1185,f1139]) ).
fof(f1451,plain,
! [X0] : hAPP(sF4,X0) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),X0),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1427,f1014]) ).
fof(f1465,plain,
c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex) = hAPP(sF4,v_n),
inference(superposition,[],[f1451,f1033]) ).
fof(f1472,plain,
( sF1 = hAPP(sF4,v_n)
| ~ spl10_3 ),
inference(forward_demodulation,[],[f1465,f1162]) ).
fof(f1481,plain,
! [X0] :
( c_HOL_Otimes__class_Otimes(sF1,X0,tc_Complex_Ocomplex) = X0
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f523,f1008]) ).
fof(f1488,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF1,X0,tc_Complex_Ocomplex) = X0,
inference(forward_subsumption_resolution,[],[f1481,f979]) ).
fof(f1538,plain,
( c_HOL_Oord__class_Oless(sF7,c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(tc_nat) ),
inference(superposition,[],[f596,f1020]) ).
fof(f1541,plain,
c_HOL_Oord__class_Oless(sF7,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f1538,f910]) ).
fof(f1609,plain,
! [X0] :
( sF1 = hAPP(c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex),X0)
| ~ class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex) ),
inference(superposition,[],[f855,f1008]) ).
fof(f1623,plain,
! [X0] : sF1 = hAPP(c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex),X0),
inference(forward_subsumption_resolution,[],[f1609,f992]) ).
fof(f1697,plain,
! [X0] : hAPP(c_Power_Opower__class_Opower(sF5,tc_Complex_Ocomplex),X0) = hAPP(sF4,c_HOL_Otimes__class_Otimes(v_k,X0,tc_nat)),
inference(superposition,[],[f1257,f1016]) ).
fof(f1725,plain,
! [X0] : hAPP(sF6,X0) = hAPP(sF4,c_HOL_Otimes__class_Otimes(v_k,X0,tc_nat)),
inference(forward_demodulation,[],[f1697,f1018]) ).
fof(f1746,plain,
! [X0] : hAPP(sF6,X0) = hAPP(sF4,c_HOL_Otimes__class_Otimes(X0,v_k,tc_nat)),
inference(superposition,[],[f1725,f29]) ).
fof(f1832,plain,
! [X0] : hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0) = c_HOL_Oinverse__class_Odivide(hAPP(sF4,X0),hAPP(sF4,X0),tc_Complex_Ocomplex),
inference(superposition,[],[f1132,f1014]) ).
fof(f2049,plain,
! [X0] :
( sF0 = c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(superposition,[],[f630,f1117]) ).
fof(f2050,plain,
! [X0] :
( sF1 = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(superposition,[],[f630,f1138]) ).
fof(f2068,plain,
! [X0] :
( sF1 = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_subsumption_resolution,[],[f2050,f978]) ).
fof(f2069,plain,
! [X0] :
( sF0 = c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_subsumption_resolution,[],[f2049,f978]) ).
fof(f2076,plain,
! [X0] :
( sF1 = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_subsumption_resolution,[],[f2068,f995]) ).
fof(f2077,plain,
! [X0] :
( sF0 = c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_subsumption_resolution,[],[f2069,f995]) ).
fof(f2084,plain,
! [X0] :
( sF1 = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| sF0 = X0 ),
inference(forward_demodulation,[],[f2076,f1006]) ).
fof(f2085,plain,
! [X0] :
( sF0 = c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex)
| sF0 = X0 ),
inference(forward_demodulation,[],[f2077,f1006]) ).
fof(f2132,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex) = X0
| ~ spl10_4 ),
inference(backward_demodulation,[],[f1488,f1166]) ).
fof(f2151,plain,
( ! [X0] :
( sF0 = X0
| sF0 = X0 )
| ~ spl10_4 ),
inference(backward_demodulation,[],[f2085,f2132]) ).
fof(f2152,plain,
( ! [X0] : sF0 = X0
| ~ spl10_4 ),
inference(duplicate_literal_removal,[],[f2151]) ).
fof(f2337,plain,
( c_HOL_Oord__class_Oless(sF0,c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ spl10_4 ),
inference(superposition,[],[f1541,f2152]) ).
fof(f2346,plain,
( c_HOL_Oord__class_Oless(sF0,sF0,tc_nat)
| ~ spl10_4 ),
inference(forward_demodulation,[],[f2337,f2152]) ).
fof(f2419,plain,
( $false
| ~ spl10_4 ),
inference(forward_subsumption_resolution,[],[f2346,f681]) ).
fof(f2420,plain,
~ spl10_4,
inference(avatar_contradiction_clause,[],[f2419]) ).
fof(f2428,plain,
( sF1 = hAPP(sF4,v_k)
| ~ spl10_9 ),
inference(forward_demodulation,[],[f1016,f1347]) ).
fof(f2429,plain,
( sF6 = c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex)
| ~ spl10_9 ),
inference(forward_demodulation,[],[f1018,f1347]) ).
fof(f3471,plain,
( sF1 = c_HOL_Otimes__class_Otimes(sF3,c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex)
| c_FFT__Mirabelle_Oroot(v_n) = sF0 ),
inference(superposition,[],[f2084,f1139]) ).
fof(f3478,plain,
sF1 = c_HOL_Otimes__class_Otimes(sF3,c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f3471,f1032]) ).
fof(f3552,plain,
! [X0] :
( sF0 = c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex) ),
inference(superposition,[],[f274,f1006]) ).
fof(f3564,plain,
! [X0] : sF0 = c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f3552,f980]) ).
fof(f3807,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(sF4,X0)
| ~ class_Ring__and__Field_Oring__1__no__zero__divisors(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF3 ),
inference(superposition,[],[f871,f1014]) ).
fof(f3830,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(sF4,X0)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF3 ),
inference(forward_subsumption_resolution,[],[f3807,f975]) ).
fof(f3838,plain,
! [X0] :
( sF0 != hAPP(sF4,X0)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF3 ),
inference(forward_demodulation,[],[f3830,f1006]) ).
fof(f3843,plain,
! [X0] :
( sF0 = sF3
| sF0 != hAPP(sF4,X0) ),
inference(forward_demodulation,[],[f3838,f1006]) ).
fof(f3846,definition,
( spl10_24
<=> ! [X0] : sF0 != hAPP(sF4,X0) ),
introduced(definition,[new_symbols(definition,[spl10_24])],[avatar_definition]) ).
fof(f3847,plain,
( ! [X0] : sF0 != hAPP(sF4,X0)
| ~ spl10_24 ),
inference(avatar_component_clause,[],[f3846]) ).
fof(f3849,definition,
( spl10_25
<=> sF0 = sF3 ),
introduced(definition,[new_symbols(definition,[spl10_25])],[avatar_definition]) ).
fof(f3851,plain,
( sF0 = sF3
| ~ spl10_25 ),
inference(avatar_component_clause,[],[f3849]) ).
fof(f3852,plain,
( spl10_24
| spl10_25 ),
inference(avatar_split_clause,[],[f3843,f3849,f3846]) ).
fof(f4391,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF1,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(superposition,[],[f580,f1138]) ).
fof(f4430,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF1,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f4391,f978]) ).
fof(f4440,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF1,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f4430,f995]) ).
fof(f4448,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f4440,f1488]) ).
fof(f4451,plain,
! [X0] :
( sF1 = c_HOL_Oinverse__class_Odivide(X0,X0,tc_Complex_Ocomplex)
| sF0 = X0 ),
inference(backward_demodulation,[],[f2084,f4448]) ).
fof(f4465,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(sF1,X1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| sF0 = X0 ),
inference(superposition,[],[f580,f4451]) ).
fof(f4487,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(sF1,X1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| sF0 = X0 ),
inference(forward_subsumption_resolution,[],[f4465,f978]) ).
fof(f4499,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(sF1,X1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| sF0 = X0 ),
inference(forward_subsumption_resolution,[],[f4487,f995]) ).
fof(f4507,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X1
| sF0 = X0 ),
inference(forward_demodulation,[],[f4499,f1488]) ).
fof(f4526,plain,
( c_FFT__Mirabelle_Oroot(v_n) = c_HOL_Oinverse__class_Odivide(sF1,sF3,tc_Complex_Ocomplex)
| sF0 = sF3 ),
inference(superposition,[],[f4507,f3478]) ).
fof(f4533,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1
| sF0 = X1 ),
inference(superposition,[],[f630,f4507]) ).
fof(f4540,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1
| sF0 = X1 ),
inference(forward_subsumption_resolution,[],[f4533,f978]) ).
fof(f4545,plain,
( c_FFT__Mirabelle_Oroot(v_n) = c_HOL_Oinverse__class_Oinverse(sF3,tc_Complex_Ocomplex)
| sF0 = sF3 ),
inference(forward_demodulation,[],[f4526,f1138]) ).
fof(f4556,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1
| sF0 = X1 ),
inference(forward_subsumption_resolution,[],[f4540,f995]) ).
fof(f4562,definition,
( spl10_29
<=> c_FFT__Mirabelle_Oroot(v_n) = c_HOL_Oinverse__class_Oinverse(sF3,tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl10_29])],[avatar_definition]) ).
fof(f4564,plain,
( c_FFT__Mirabelle_Oroot(v_n) = c_HOL_Oinverse__class_Oinverse(sF3,tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(avatar_component_clause,[],[f4562]) ).
fof(f4565,plain,
( spl10_25
| spl10_29 ),
inference(avatar_split_clause,[],[f4545,f4562,f3849]) ).
fof(f4574,plain,
! [X0,X1] :
( sF0 = X1
| c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex)
| sF0 = X1 ),
inference(forward_demodulation,[],[f4556,f1006]) ).
fof(f4575,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex)
| sF0 = X1 ),
inference(duplicate_literal_removal,[],[f4574]) ).
fof(f4602,plain,
( sF1 = c_HOL_Otimes__class_Otimes(sF0,c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex)
| ~ spl10_25 ),
inference(backward_demodulation,[],[f3478,f3851]) ).
fof(f4617,plain,
( sF0 = sF1
| ~ spl10_25 ),
inference(forward_demodulation,[],[f4602,f3564]) ).
fof(f4646,plain,
( $false
| spl10_4
| ~ spl10_25 ),
inference(forward_subsumption_resolution,[],[f4617,f1165]) ).
fof(f4647,plain,
( spl10_4
| ~ spl10_25 ),
inference(avatar_contradiction_clause,[],[f4646]) ).
fof(f4998,plain,
( sF1 = c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(v_n),sF3,tc_Complex_Ocomplex)
| c_FFT__Mirabelle_Oroot(v_n) = sF0 ),
inference(superposition,[],[f4575,f3478]) ).
fof(f5001,plain,
sF1 = c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(v_n),sF3,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f4998,f1032]) ).
fof(f5006,plain,
( ! [X0] : hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),X0) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),X0),tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(superposition,[],[f1185,f4564]) ).
fof(f5007,plain,
( ! [X0] : hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),X0) = c_HOL_Oinverse__class_Oinverse(hAPP(sF4,X0),tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(forward_demodulation,[],[f5006,f1014]) ).
fof(f5078,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF3,X0,tc_Complex_Ocomplex),
inference(superposition,[],[f4448,f1139]) ).
fof(f5081,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(v_n),X0,tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(superposition,[],[f4448,f4564]) ).
fof(f5116,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(hAPP(sF4,X0),hAPP(sF4,X0),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_FFT__Mirabelle_Oroot(v_n),sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0)
| ~ spl10_29 ),
inference(backward_demodulation,[],[f1832,f5081]) ).
fof(f5125,plain,
( ! [X0] : hAPP(c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex),X0) = c_HOL_Oinverse__class_Odivide(hAPP(sF4,X0),hAPP(sF4,X0),tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(forward_demodulation,[],[f5116,f5001]) ).
fof(f6140,plain,
( c_HOL_Oinverse__class_Oinverse(sF1,tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k)
| ~ spl10_9
| ~ spl10_29 ),
inference(superposition,[],[f5007,f2428]) ).
fof(f6154,plain,
( sF1 = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k)
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(forward_demodulation,[],[f6140,f1162]) ).
fof(f6164,plain,
( sF0 = c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex),sF8,tc_nat,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(sF7,v_k,tc_nat)
| ~ c_HOL_Oord__class_Oless(v_k,v_n,tc_nat)
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(superposition,[],[f1106,f6154]) ).
fof(f6206,plain,
( sF0 = c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex),sF8,tc_nat,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(v_k,v_n,tc_nat)
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(forward_subsumption_resolution,[],[f6164,f1071]) ).
fof(f6220,plain,
( sF0 = c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(sF1,tc_Complex_Ocomplex),sF8,tc_nat,tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(forward_subsumption_resolution,[],[f6206,f817]) ).
fof(f6231,plain,
( sF0 = c_Finite__Set_Osetsum(sF6,sF8,tc_nat,tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(forward_demodulation,[],[f6220,f2429]) ).
fof(f6235,plain,
( sF0 = sF9
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(backward_demodulation,[],[f1024,f6231]) ).
fof(f6236,plain,
( $false
| ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(forward_subsumption_resolution,[],[f6235,f1025]) ).
fof(f6237,plain,
( ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(avatar_contradiction_clause,[],[f6236]) ).
fof(f6294,plain,
( ! [X0] : sF1 = c_HOL_Oinverse__class_Odivide(hAPP(sF4,X0),hAPP(sF4,X0),tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(forward_demodulation,[],[f5125,f1623]) ).
fof(f6380,definition,
( spl10_48
<=> sF0 = sF5 ),
introduced(definition,[new_symbols(definition,[spl10_48])],[avatar_definition]) ).
fof(f6381,plain,
( sF0 != sF5
| spl10_48 ),
inference(avatar_component_clause,[],[f6380]) ).
fof(f6386,plain,
( sF0 != sF5
| ~ spl10_24 ),
inference(superposition,[],[f3847,f1016]) ).
fof(f6389,plain,
( ~ spl10_48
| ~ spl10_24 ),
inference(avatar_split_clause,[],[f6386,f3846,f6380]) ).
fof(f6412,plain,
( c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(sF7,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(sF1,sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl10_8 ),
inference(superposition,[],[f1343,f1200]) ).
fof(f6427,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(sF1,sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Finite__Set_Osetsum(sF6,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat,tc_Complex_Ocomplex)
| ~ spl10_8 ),
inference(forward_demodulation,[],[f6412,f1048]) ).
fof(f6551,plain,
( sF1 = c_HOL_Oinverse__class_Odivide(sF5,sF5,tc_Complex_Ocomplex)
| ~ spl10_29 ),
inference(superposition,[],[f6294,f1016]) ).
fof(f7092,plain,
! [X0] :
( hAPP(sF6,c_Suc(X0)) = c_HOL_Otimes__class_Otimes(sF5,hAPP(sF6,X0),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f698,f1018]) ).
fof(f7145,plain,
! [X0] :
( hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),c_Suc(X0)) = c_HOL_Oinverse__class_Odivide(hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),X0),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f5078,f698]) ).
fof(f7159,plain,
! [X0] : hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),c_Suc(X0)) = c_HOL_Oinverse__class_Odivide(hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),X0),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f7145,f979]) ).
fof(f7186,plain,
! [X0] : hAPP(sF6,c_Suc(X0)) = c_HOL_Otimes__class_Otimes(sF5,hAPP(sF6,X0),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f7092,f979]) ).
fof(f7188,plain,
! [X0] : hAPP(sF4,c_Suc(X0)) = c_HOL_Oinverse__class_Odivide(hAPP(sF4,X0),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f7159,f1014]) ).
fof(f7213,plain,
( c_HOL_Oinverse__class_Odivide(sF1,c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex) = hAPP(sF4,c_Suc(v_n))
| ~ spl10_3 ),
inference(superposition,[],[f7188,f1472]) ).
fof(f7228,plain,
( c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex) = hAPP(sF4,c_Suc(v_n))
| ~ spl10_3 ),
inference(forward_demodulation,[],[f7213,f1138]) ).
fof(f7235,plain,
( sF3 = hAPP(sF4,c_Suc(v_n))
| ~ spl10_3 ),
inference(forward_demodulation,[],[f7228,f1139]) ).
fof(f7248,plain,
( ! [X0] : hAPP(c_Power_Opower__class_Opower(sF3,tc_Complex_Ocomplex),X0) = hAPP(sF4,c_HOL_Otimes__class_Otimes(c_Suc(v_n),X0,tc_nat))
| ~ spl10_3 ),
inference(superposition,[],[f1257,f7235]) ).
fof(f7249,plain,
( ! [X0] : hAPP(sF4,X0) = hAPP(sF4,c_HOL_Otimes__class_Otimes(c_Suc(v_n),X0,tc_nat))
| ~ spl10_3 ),
inference(forward_demodulation,[],[f7248,f1014]) ).
fof(f7412,plain,
( hAPP(sF4,v_k) = hAPP(sF6,c_Suc(v_n))
| ~ spl10_3 ),
inference(superposition,[],[f1746,f7249]) ).
fof(f7423,plain,
( sF5 = hAPP(sF6,c_Suc(v_n))
| ~ spl10_3 ),
inference(forward_demodulation,[],[f7412,f1016]) ).
fof(f7459,plain,
! [X0] :
( hAPP(sF6,X0) = c_HOL_Oinverse__class_Odivide(hAPP(sF6,c_Suc(X0)),sF5,tc_Complex_Ocomplex)
| sF0 = sF5 ),
inference(superposition,[],[f4507,f7186]) ).
fof(f7460,plain,
( ! [X0] : hAPP(sF6,X0) = c_HOL_Oinverse__class_Odivide(hAPP(sF6,c_Suc(X0)),sF5,tc_Complex_Ocomplex)
| spl10_48 ),
inference(forward_subsumption_resolution,[],[f7459,f6381]) ).
fof(f7468,plain,
( c_HOL_Oinverse__class_Odivide(sF5,sF5,tc_Complex_Ocomplex) = hAPP(sF6,v_n)
| ~ spl10_3
| spl10_48 ),
inference(superposition,[],[f7460,f7423]) ).
fof(f7480,plain,
( sF1 = hAPP(sF6,v_n)
| ~ spl10_3
| ~ spl10_29
| spl10_48 ),
inference(forward_demodulation,[],[f7468,f6551]) ).
fof(f7498,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(sF1,sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Finite__Set_Osetsum(sF6,c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(superposition,[],[f1343,f7480]) ).
fof(f7503,plain,
( c_Finite__Set_Osetsum(sF6,sF8,tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(sF1,sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(forward_demodulation,[],[f7498,f1087]) ).
fof(f7507,plain,
( sF9 = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(sF1,sF1,tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(sF5,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(forward_demodulation,[],[f7503,f1024]) ).
fof(f7508,plain,
( sF9 = c_Finite__Set_Osetsum(sF6,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat,tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(backward_demodulation,[],[f6427,f7507]) ).
fof(f7516,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF9
| ~ class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex)
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(superposition,[],[f7508,f798]) ).
fof(f7519,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF9
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(forward_subsumption_resolution,[],[f7516,f986]) ).
fof(f7522,plain,
( sF0 = sF9
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(forward_demodulation,[],[f7519,f1006]) ).
fof(f7525,plain,
( $false
| ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(forward_subsumption_resolution,[],[f7522,f1025]) ).
fof(f7526,plain,
( ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(avatar_contradiction_clause,[],[f7525]) ).
cnf(s3,plain,
( spl10_3
| spl10_4 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s6,plain,
( spl10_8
| spl10_9 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s23,plain,
~ spl10_4,
inference(sat_conversion,[],[f2420]) ).
cnf(s44,plain,
( spl10_24
| spl10_25 ),
inference(sat_conversion,[],[f3852]) ).
cnf(s51,plain,
( spl10_25
| spl10_29 ),
inference(sat_conversion,[],[f4565]) ).
cnf(s52,plain,
( spl10_4
| ~ spl10_25 ),
inference(sat_conversion,[],[f4647]) ).
cnf(s64,plain,
( ~ spl10_3
| ~ spl10_9
| ~ spl10_29 ),
inference(sat_conversion,[],[f6237]) ).
cnf(s67,plain,
( ~ spl10_24
| ~ spl10_48 ),
inference(sat_conversion,[],[f6389]) ).
cnf(s74,plain,
( ~ spl10_3
| ~ spl10_8
| ~ spl10_29
| spl10_48 ),
inference(sat_conversion,[],[f7526]) ).
cnf(s78,plain,
~ spl10_25,
inference(rat,[],[s52,s23]) ).
cnf(s79,plain,
spl10_29,
inference(rat,[],[s51,s78]) ).
cnf(s80,plain,
spl10_24,
inference(rat,[],[s44,s78]) ).
cnf(s81,plain,
~ spl10_48,
inference(rat,[],[s67,s80]) ).
cnf(s84,plain,
spl10_3,
inference(rat,[],[s3,s23]) ).
cnf(s85,plain,
~ spl10_8,
inference(rat,[],[s74,s81,s79,s84]) ).
cnf(s86,plain,
~ spl10_9,
inference(rat,[],[s64,s79,s84]) ).
cnf(s87,plain,
$false,
inference(rat,[],[s6,s86,s85]) ).
fof(f7527,plain,
$false,
inference(avatar_sat_refutation,[],[s87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV618-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n001.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 12:09:18 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.54/2.36 % (307364)Input is clausal, will run a generic CNF schedule.
% 11.54/2.36 % (307373)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=964868754:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.54/2.36 % (307374)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2592607046:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.54/2.36 % (307372)lrs+10_1_sil=8000:sp=occurrence:random_seed=295044306:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.54/2.36 % (307371)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4095290912:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.54/2.36 % (307375)dis-21_1_sil=8000:lcm=predicate:random_seed=3299683352:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.54/2.36 % (307370)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2669283156:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.54/2.36 % (307369)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=323901390:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.54/2.36 % (307373)Instruction limit reached!
% 11.54/2.36 % (307373)------------------------------
% 11.54/2.36 % (307373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307373)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307373)Termination reason: Instruction limit
% 11.54/2.36 % (307373)Termination phase: Saturation
% 11.54/2.36 % (307373)Time elapsed: 0.042 s
% 11.54/2.36 % (307373)Peak memory usage: 89 MB
% 11.54/2.36 % (307373)Instructions burned: 117 (million)
% 11.54/2.36 % (307375)Instruction limit reached!
% 11.54/2.36 % (307375)------------------------------
% 11.54/2.36 % (307375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307375)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307375)Termination reason: Instruction limit
% 11.54/2.36 % (307375)Termination phase: Saturation
% 11.54/2.36 % (307375)Time elapsed: 0.068 s
% 11.54/2.36 % (307375)Peak memory usage: 90 MB
% 11.54/2.36 % (307375)Instructions burned: 118 (million)
% 11.54/2.36 % (307374)Instruction limit reached!
% 11.54/2.36 % (307374)------------------------------
% 11.54/2.36 % (307374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307374)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307374)Termination reason: Instruction limit
% 11.54/2.36 % (307374)Termination phase: Saturation
% 11.54/2.36 % (307374)Time elapsed: 0.071 s
% 11.54/2.36 % (307374)Peak memory usage: 90 MB
% 11.54/2.36 % (307374)Instructions burned: 183 (million)
% 11.54/2.36 % (307372)Instruction limit reached!
% 11.54/2.36 % (307372)------------------------------
% 11.54/2.36 % (307372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307372)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307372)Termination reason: Instruction limit
% 11.54/2.36 % (307372)Termination phase: Saturation
% 11.54/2.36 % (307372)Time elapsed: 0.071 s
% 11.54/2.36 % (307372)Peak memory usage: 89 MB
% 11.54/2.36 % (307372)Instructions burned: 108 (million)
% 11.54/2.36 % (307383)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1405126978:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.54/2.36 % (307383)Refutation not found, incomplete strategy
% 11.54/2.36 % (307383)------------------------------
% 11.54/2.36 % (307383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307383)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307383)Termination reason: Refutation not found, incomplete strategy
% 11.54/2.36 % (307383)Time elapsed: 0.010 s
% 11.54/2.36 % (307383)Peak memory usage: 88 MB
% 11.54/2.36 % (307383)Instructions burned: 13 (million)
% 11.54/2.36 % (307386)lrs+10_64_to=lpo:sil=8000:random_seed=1303367322:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 11.54/2.36 % (307386)Instruction limit reached!
% 11.54/2.36 % (307386)------------------------------
% 11.54/2.36 % (307386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307386)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307386)Termination reason: Instruction limit
% 11.54/2.36 % (307386)Termination phase: Saturation
% 11.54/2.36 % (307386)Time elapsed: 0.043 s
% 11.54/2.36 % (307386)Peak memory usage: 89 MB
% 11.54/2.36 % (307386)Instructions burned: 127 (million)
% 11.54/2.36 % (307385)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=775768828:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.54/2.36 % (307384)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2057173642:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.54/2.36 % (307384)Instruction limit reached!
% 11.54/2.36 % (307384)------------------------------
% 11.54/2.36 % (307384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307384)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307384)Termination reason: Instruction limit
% 11.54/2.36 % (307384)Termination phase: Saturation
% 11.54/2.36 % (307384)Time elapsed: 0.102 s
% 11.54/2.36 % (307384)Peak memory usage: 91 MB
% 11.54/2.36 % (307384)Instructions burned: 189 (million)
% 11.54/2.36 % (307391)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3264626557:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.54/2.36 % (307385)Instruction limit reached!
% 11.54/2.36 % (307385)------------------------------
% 11.54/2.36 % (307385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307385)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307385)Termination reason: Instruction limit
% 11.54/2.36 % (307385)Termination phase: Saturation
% 11.54/2.36 % (307385)Time elapsed: 0.124 s
% 11.54/2.36 % (307385)Peak memory usage: 90 MB
% 11.54/2.36 % (307385)Instructions burned: 220 (million)
% 11.54/2.36 % (307383)------------------------------
% 11.54/2.36 % (307383)------------------------------
% 11.54/2.36 % (307391)Instruction limit reached!
% 11.54/2.36 % (307391)------------------------------
% 11.54/2.36 % (307391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307391)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307391)Termination reason: Instruction limit
% 11.54/2.36 % (307391)Termination phase: Saturation
% 11.54/2.36 % (307391)Time elapsed: 0.072 s
% 11.54/2.36 % (307391)Peak memory usage: 90 MB
% 11.54/2.36 % (307391)Instructions burned: 194 (million)
% 11.54/2.36 % (307392)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1449589132:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 11.54/2.36 % (307394)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1080265278:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 11.54/2.36 % (307395)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3593578860:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 11.54/2.36 % (307396)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3950644922:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 11.54/2.36 % (307396)Refutation not found, incomplete strategy
% 11.54/2.36 % (307396)------------------------------
% 11.54/2.36 % (307396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307396)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307396)Termination reason: Refutation not found, incomplete strategy
% 11.54/2.36 % (307396)Time elapsed: 0.010 s
% 11.54/2.36 % (307396)Peak memory usage: 88 MB
% 11.54/2.36 % (307396)Instructions burned: 15 (million)
% 11.54/2.36 % (307392)Instruction limit reached!
% 11.54/2.36 % (307392)------------------------------
% 11.54/2.36 % (307392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307392)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307392)Termination reason: Instruction limit
% 11.54/2.36 % (307392)Termination phase: Saturation
% 11.54/2.36 % (307392)Time elapsed: 0.101 s
% 11.54/2.36 % (307392)Peak memory usage: 90 MB
% 11.54/2.36 % (307392)Instructions burned: 157 (million)
% 11.54/2.36 % (307395)Instruction limit reached!
% 11.54/2.36 % (307395)------------------------------
% 11.54/2.36 % (307395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307395)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307395)Termination reason: Instruction limit
% 11.54/2.36 % (307395)Termination phase: Saturation
% 11.54/2.36 % (307395)Time elapsed: 0.030 s
% 11.54/2.36 % (307395)Peak memory usage: 89 MB
% 11.54/2.36 % (307395)Instructions burned: 108 (million)
% 11.54/2.36 % (307402)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4189843064:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 11.54/2.36 % (307401)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3481522136:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 11.54/2.36 % (307396)------------------------------
% 11.54/2.36 % (307396)------------------------------
% 11.54/2.36 % (307401)Instruction limit reached!
% 11.54/2.36 % (307401)------------------------------
% 11.54/2.36 % (307401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307401)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307401)Termination reason: Instruction limit
% 11.54/2.36 % (307401)Termination phase: Saturation
% 11.54/2.36 % (307401)Time elapsed: 0.144 s
% 11.54/2.36 % (307401)Peak memory usage: 89 MB
% 11.54/2.36 % (307401)Instructions burned: 243 (million)
% 11.54/2.36 % (307405)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1382352280:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 11.54/2.36 % (307406)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3036883341:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 11.54/2.36 % (307405)Instruction limit reached!
% 11.54/2.36 % (307405)------------------------------
% 11.54/2.36 % (307405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307405)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307405)Termination reason: Instruction limit
% 11.54/2.36 % (307405)Termination phase: Saturation
% 11.54/2.36 % (307405)Time elapsed: 0.088 s
% 11.54/2.36 % (307405)Peak memory usage: 90 MB
% 11.54/2.36 % (307405)Instructions burned: 135 (million)
% 11.54/2.36 % (307371)First to succeed.
% 11.54/2.36 % (307371)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-307364"
% 11.54/2.36 % (307409)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=755715288:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 11.54/2.36 % (307406)Instruction limit reached!
% 11.54/2.36 % (307406)------------------------------
% 11.54/2.36 % (307406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307406)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307406)Termination reason: Instruction limit
% 11.54/2.36 % (307406)Termination phase: Saturation
% 11.54/2.36 % (307406)Time elapsed: 0.280 s
% 11.54/2.36 % (307406)Peak memory usage: 93 MB
% 11.54/2.36 % (307406)Instructions burned: 500 (million)
% 11.54/2.36 % (307409)Instruction limit reached!
% 11.54/2.36 % (307409)------------------------------
% 11.54/2.36 % (307409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.36 % (307409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.36 % (307409)CaDiCaL version: 2.1.3
% 11.54/2.36 % (307409)Termination reason: Instruction limit
% 11.54/2.36 % (307409)Termination phase: Saturation
% 11.54/2.36 % (307409)Time elapsed: 0.127 s
% 11.54/2.36 % (307409)Peak memory usage: 91 MB
% 11.54/2.36 % (307409)Instructions burned: 192 (million)
% 11.54/2.36 % (307371)Refutation found. Thanks to Tanya!
% 11.54/2.36 % SZS status Unsatisfiable for theBenchmark
% 11.54/2.36 % SZS output start Proof for theBenchmark
% See solution above
% 12.29/2.56 % (307371)------------------------------
% 12.29/2.56 % (307371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.29/2.56 % (307371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.29/2.56 % (307371)CaDiCaL version: 2.1.3
% 12.29/2.56 % (307371)Termination reason: Refutation
% 12.29/2.56 % (307371)Time elapsed: 1.214 s
% 12.29/2.56 % (307371)Peak memory usage: 139 MB
% 12.29/2.56 % (307371)Instructions burned: 1880 (million)
% 12.29/2.56 % (307371)------------------------------
% 12.29/2.56 % (307371)------------------------------
% 12.29/2.56 % (307364)Success in time 1.68 s
% 12.29/2.56 % Vampire exiting
%------------------------------------------------------------------------------