%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG408-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 09:19:57 AM UTC 2026
% Result : Unsatisfiable 9.87s 2.32s
% Output : Refutation 11.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 34
% Syntax : Number of formulae : 140 ( 83 unt; 18 def)
% Number of atoms : 236 ( 70 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 196 ( 100 ~; 93 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 4 prp; 0-3 aty)
% Number of functors : 32 ( 32 usr; 23 con; 0-3 aty)
% Number of variables : 72 ( 0 sgn 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1120,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_HOL_Otimes__class_Otimes(X1,X2,X0),c_HOL_Otimes__class_Otimes(X1,X3,X0),X0)
| ~ class_Ring__and__Field_Omult__mono1(X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ c_lessequals(X2,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__mono1_0) ).
fof(f1202,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__less__def_0) ).
fof(f1327,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Ozero__class_Ozero(X0),c_Power_Opower__class_Opower(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__le__power__iff_1) ).
fof(f1335,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X1,X2,X0),X1,X0) = c_Power_Opower__class_Opower(X1,c_Suc(X2),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I28_J_0) ).
fof(f1336,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(X1,c_Suc(X2),X0) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X1,X2,X0),X1,X0) ),
inference(reorient_equations,[],[f1335]) ).
fof(f1351,axiom,
! [X0,X1] :
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_norm__ge__zero_0) ).
fof(f1357,axiom,
! [X0] : c_Suc(X0) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1_0) ).
fof(f1470,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I17_J_0) ).
fof(f1471,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0) ),
inference(reorient_equations,[],[f1470]) ).
fof(f1509,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,X2,X0) = c_HOL_Otimes__class_Otimes(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I7_J_0) ).
fof(f1510,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X2,X1,X0) = c_HOL_Otimes__class_Otimes(X1,X2,X0) ),
inference(reorient_equations,[],[f1509]) ).
fof(f1529,axiom,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f1531,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_03) ).
fof(f1532,axiom,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_04) ).
fof(f1533,negated_conjecture,
~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1675,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__idom) ).
fof(f1680,axiom,
class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Omult__mono1) ).
fof(f1717,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1721,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1868,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X1,X2,X0),X1,X0) = c_Power_Opower__class_Opower(X1,c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat),X0) ),
inference(definition_unfolding,[],[f1336,f1357]) ).
fof(f1870,definition,
sF0 = c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1871,plain,
c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1870]) ).
fof(f1872,definition,
sF1 = c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1873,plain,
c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex) = sF1,
inference(reorient_equations,[],[f1872]) ).
fof(f1874,definition,
sF2 = c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1875,plain,
c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex) = sF2,
inference(reorient_equations,[],[f1874]) ).
fof(f1876,definition,
sF3 = c_HOL_Otimes__class_Otimes(sF2,sF1,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1877,plain,
c_HOL_Otimes__class_Otimes(sF2,sF1,tc_Complex_Ocomplex) = sF3,
inference(reorient_equations,[],[f1876]) ).
fof(f1878,definition,
sF4 = c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1879,plain,
c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex) = sF4,
inference(reorient_equations,[],[f1878]) ).
fof(f1880,definition,
sF5 = c_HOL_Otimes__class_Otimes(sF3,sF4,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1881,plain,
c_HOL_Otimes__class_Otimes(sF3,sF4,tc_Complex_Ocomplex) = sF5,
inference(reorient_equations,[],[f1880]) ).
fof(f1882,definition,
sF6 = c_RealVector_Onorm__class_Onorm(sF5,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1883,plain,
c_RealVector_Onorm__class_Onorm(sF5,tc_Complex_Ocomplex) = sF6,
inference(reorient_equations,[],[f1882]) ).
fof(f1884,definition,
sF7 = c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1885,plain,
c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal) = sF7,
inference(reorient_equations,[],[f1884]) ).
fof(f1886,definition,
sF8 = c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1887,plain,
c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex) = sF8,
inference(reorient_equations,[],[f1886]) ).
fof(f1888,definition,
sF9 = c_HOL_Oone__class_Oone(tc_nat),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1889,plain,
c_HOL_Oone__class_Oone(tc_nat) = sF9,
inference(reorient_equations,[],[f1888]) ).
fof(f1890,definition,
sF10 = c_HOL_Oplus__class_Oplus(v_k____,sF9,tc_nat),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1891,plain,
c_HOL_Oplus__class_Oplus(v_k____,sF9,tc_nat) = sF10,
inference(reorient_equations,[],[f1890]) ).
fof(f1892,definition,
sF11 = c_Power_Opower__class_Opower(sF8,sF10,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1893,plain,
c_Power_Opower__class_Opower(sF8,sF10,tc_RealDef_Oreal) = sF11,
inference(reorient_equations,[],[f1892]) ).
fof(f1894,definition,
sF12 = c_HOL_Otimes__class_Otimes(sF11,v_m____,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1895,plain,
c_HOL_Otimes__class_Otimes(sF11,v_m____,tc_RealDef_Oreal) = sF12,
inference(reorient_equations,[],[f1894]) ).
fof(f1896,definition,
sF13 = c_HOL_Otimes__class_Otimes(v_t____,sF12,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1897,plain,
c_HOL_Otimes__class_Otimes(v_t____,sF12,tc_RealDef_Oreal) = sF13,
inference(reorient_equations,[],[f1896]) ).
fof(f1898,definition,
sF14 = c_HOL_Otimes__class_Otimes(sF7,sF13,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1899,plain,
c_HOL_Otimes__class_Otimes(sF7,sF13,tc_RealDef_Oreal) = sF14,
inference(reorient_equations,[],[f1898]) ).
fof(f1900,plain,
~ c_lessequals(sF6,sF14,tc_RealDef_Oreal),
inference(definition_folding,[],[f1533,f1899,f1897,f1895,f1893,f1891,f1889,f1887,f1885,f1883,f1881,f1879,f1873,f1871,f1877,f1873,f1871,f1875,f1873,f1871]) ).
fof(f1979,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal),
inference(superposition,[],[f1529,f1871]) ).
fof(f1980,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1979,f1873]) ).
fof(f1981,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1980,f1879]) ).
fof(f2147,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex),
inference(resolution,[],[f1717,f1510]) ).
fof(f2401,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF8,tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(superposition,[],[f1351,f1887]) ).
fof(f2404,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF8,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f2401,f1721]) ).
fof(f2523,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1532,f1871]) ).
fof(f2525,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1532,f2147]) ).
fof(f2528,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2525,f1871]) ).
fof(f2530,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2523,f1873]) ).
fof(f2535,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,sF9,tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2528,f1889]) ).
fof(f2537,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2530,f1879]) ).
fof(f2542,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),sF10,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2535,f1891]) ).
fof(f2544,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,sF9,tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2537,f1889]) ).
fof(f2549,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF8,sF10,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2542,f1887]) ).
fof(f2551,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),sF10,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2544,f1891]) ).
fof(f2556,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2549,f1893]) ).
fof(f2558,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF8,sF10,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2551,f1887]) ).
fof(f2563,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2556,f1885]) ).
fof(f2565,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2558,f1893]) ).
fof(f2570,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,v_k____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2565,f1885]) ).
fof(f2575,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF2,sF1,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2570,f1875]) ).
fof(f2580,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(sF3,sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2575,f1877]) ).
fof(f2585,plain,
c_RealVector_Onorm__class_Onorm(sF5,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2580,f1881]) ).
fof(f2590,plain,
sF6 = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2585,f1883]) ).
fof(f2779,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),
inference(resolution,[],[f1868,f1717]) ).
fof(f2780,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,c_HOL_Oplus__class_Oplus(X1,sF9,tc_nat),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2779,f1889]) ).
fof(f2786,plain,
! [X0] : c_Power_Opower__class_Opower(X0,sF10,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),
inference(superposition,[],[f2780,f1891]) ).
fof(f2790,plain,
c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,sF9,tc_nat),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f2563,f2780]) ).
fof(f2806,plain,
c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),sF10,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(v_w____,sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2790,f1891]) ).
fof(f2809,plain,
c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),sF10,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f2806,f2147]) ).
fof(f2811,plain,
c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,sF10,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2809,f1873]) ).
fof(f2813,plain,
c_HOL_Otimes__class_Otimes(sF7,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,sF10,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2811,f1879]) ).
fof(f2815,plain,
sF6 = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,sF10,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2813,f2590]) ).
fof(f2930,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal) ),
inference(superposition,[],[f1327,f1885]) ).
fof(f2933,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF8,tc_RealDef_Oreal) ),
inference(superposition,[],[f1327,f1893]) ).
fof(f2970,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF8,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f2933,f1675]) ).
fof(f2985,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f2930,f1675]) ).
fof(f2988,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f2970,f2404]) ).
fof(f2990,definition,
( spl15_27
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_27])],[avatar_definition]) ).
fof(f2991,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)
| ~ spl15_27 ),
inference(avatar_component_clause,[],[f2990]) ).
fof(f2992,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)
| spl15_27 ),
inference(avatar_component_clause,[],[f2990]) ).
fof(f2994,definition,
( spl15_28
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_28])],[avatar_definition]) ).
fof(f2997,plain,
( ~ spl15_27
| spl15_28 ),
inference(avatar_split_clause,[],[f2985,f2994,f2990]) ).
fof(f3419,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(resolution,[],[f1471,f1717]) ).
fof(f3433,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,sF10,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(superposition,[],[f3419,f2786]) ).
fof(f4036,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(superposition,[],[f1120,f1532]) ).
fof(f4099,plain,
! [X0] :
( c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,X0,tc_RealDef_Oreal),sF13,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)
| ~ c_lessequals(X0,sF12,tc_RealDef_Oreal) ),
inference(superposition,[],[f1120,f1897]) ).
fof(f4128,plain,
! [X0] :
( c_lessequals(c_HOL_Otimes__class_Otimes(sF11,X0,tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Omult__mono1(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ c_lessequals(X0,v_m____,tc_RealDef_Oreal) ),
inference(superposition,[],[f1120,f1895]) ).
fof(f4139,plain,
! [X0] :
( c_lessequals(c_HOL_Otimes__class_Otimes(sF11,X0,tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ c_lessequals(X0,v_m____,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f4128,f1680]) ).
fof(f4388,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f4036,f1680]) ).
fof(f4432,plain,
! [X0] :
( c_lessequals(c_HOL_Otimes__class_Otimes(sF11,X0,tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ c_lessequals(X0,v_m____,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f4139,f2988]) ).
fof(f4478,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4388,f1885]) ).
fof(f4539,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4478,f3419]) ).
fof(f4610,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),sF10,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4539,f3433]) ).
fof(f4641,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),sF10,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4610,f1871]) ).
fof(f4643,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,sF10,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4641,f1873]) ).
fof(f4645,plain,
! [X0] :
( c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF1,sF10,tc_Complex_Ocomplex),sF4,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4643,f1879]) ).
fof(f4647,plain,
! [X0] :
( c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4645,f2815]) ).
fof(f4904,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4647,f1885]) ).
fof(f4930,definition,
( spl15_161
<=> ! [X0] :
( c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[spl15_161])],[avatar_definition]) ).
fof(f4931,plain,
( ! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) )
| ~ spl15_161 ),
inference(avatar_component_clause,[],[f4930]) ).
fof(f5032,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(sF0,v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f4904,f1871]) ).
fof(f5034,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_s____,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f5032,f1873]) ).
fof(f5036,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f5034,f1879]) ).
fof(f5038,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,sF9,tc_nat),tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f5036,f1889]) ).
fof(f5040,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),sF10,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f5038,f1891]) ).
fof(f5042,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(sF8,sF10,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f5040,f1887]) ).
fof(f5044,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f5042,f1893]) ).
fof(f5046,plain,
( ~ spl15_28
| spl15_161 ),
inference(avatar_split_clause,[],[f5044,f4930,f2994]) ).
fof(f5527,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),
inference(resolution,[],[f1531,f1202]) ).
fof(f5529,plain,
( $false
| spl15_27 ),
inference(forward_subsumption_resolution,[],[f5527,f2992]) ).
fof(f5530,plain,
spl15_27,
inference(avatar_contradiction_clause,[],[f5529]) ).
fof(f5537,plain,
! [X0] :
( c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,X0,tc_RealDef_Oreal),sF13,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal)
| ~ c_lessequals(X0,sF12,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f4099,f1680]) ).
fof(f5633,plain,
( ! [X0] :
( c_lessequals(c_HOL_Otimes__class_Otimes(v_t____,X0,tc_RealDef_Oreal),sF13,tc_RealDef_Oreal)
| ~ c_lessequals(X0,sF12,tc_RealDef_Oreal) )
| ~ spl15_27 ),
inference(forward_subsumption_resolution,[],[f5537,f2991]) ).
fof(f5740,plain,
( c_lessequals(sF6,c_HOL_Otimes__class_Otimes(sF7,sF13,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ spl15_27
| ~ spl15_161 ),
inference(resolution,[],[f4931,f5633]) ).
fof(f5763,plain,
( c_lessequals(sF6,sF14,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ spl15_27
| ~ spl15_161 ),
inference(forward_demodulation,[],[f5740,f1899]) ).
fof(f5768,plain,
( ~ c_lessequals(c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ spl15_27
| ~ spl15_161 ),
inference(forward_subsumption_resolution,[],[f5763,f1900]) ).
fof(f5771,plain,
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(sF4,tc_Complex_Ocomplex),v_m____,tc_RealDef_Oreal)
| ~ spl15_27
| ~ spl15_161 ),
inference(resolution,[],[f5768,f4432]) ).
fof(f5778,plain,
( $false
| ~ spl15_27
| ~ spl15_161 ),
inference(forward_subsumption_resolution,[],[f5771,f1981]) ).
fof(f5779,plain,
( ~ spl15_27
| ~ spl15_161 ),
inference(avatar_contradiction_clause,[],[f5778]) ).
cnf(s18,plain,
( ~ spl15_27
| spl15_28 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s189,plain,
( ~ spl15_28
| spl15_161 ),
inference(sat_conversion,[],[f5046]) ).
cnf(s267,plain,
spl15_27,
inference(sat_conversion,[],[f5530]) ).
cnf(s277,plain,
( ~ spl15_27
| ~ spl15_161 ),
inference(sat_conversion,[],[f5779]) ).
cnf(s278,plain,
~ spl15_161,
inference(rat,[],[s277,s267]) ).
cnf(s279,plain,
~ spl15_28,
inference(rat,[],[s189,s278]) ).
cnf(s282,plain,
$false,
inference(rat,[],[s18,s279,s267]) ).
fof(f5780,plain,
$false,
inference(avatar_sat_refutation,[],[s282]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG408-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 20:20:43 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.87/2.32 % (1947796)Input is clausal, will run a generic CNF schedule.
% 9.87/2.32 % (1947803)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3739633847:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.87/2.32 % (1947806)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1071071988:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.87/2.32 % (1947804)lrs+10_1_sil=8000:sp=occurrence:random_seed=1906244777:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.87/2.32 % (1947802)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=75547555:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.87/2.32 % (1947807)dis-21_1_sil=8000:lcm=predicate:random_seed=732060530: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)
% 9.87/2.32 % (1947805)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=313100224:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.87/2.32 % (1947801)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=1385505707:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.87/2.32 % (1947807)Instruction limit reached!
% 9.87/2.32 % (1947807)------------------------------
% 9.87/2.32 % (1947807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947807)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947807)Termination reason: Instruction limit
% 9.87/2.32 % (1947807)Termination phase: Saturation
% 9.87/2.32 % (1947807)Time elapsed: 0.063 s
% 9.87/2.32 % (1947807)Peak memory usage: 90 MB
% 9.87/2.32 % (1947807)Instructions burned: 119 (million)
% 9.87/2.32 % (1947804)Instruction limit reached!
% 9.87/2.32 % (1947804)------------------------------
% 9.87/2.32 % (1947804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947804)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947804)Termination reason: Instruction limit
% 9.87/2.32 % (1947804)Termination phase: Saturation
% 9.87/2.32 % (1947804)Time elapsed: 0.069 s
% 9.87/2.32 % (1947804)Peak memory usage: 90 MB
% 9.87/2.32 % (1947804)Instructions burned: 107 (million)
% 9.87/2.32 % (1947805)Instruction limit reached!
% 9.87/2.32 % (1947805)------------------------------
% 9.87/2.32 % (1947805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947805)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947805)Termination reason: Instruction limit
% 9.87/2.32 % (1947805)Termination phase: Saturation
% 9.87/2.32 % (1947805)Time elapsed: 0.069 s
% 9.87/2.32 % (1947805)Peak memory usage: 90 MB
% 9.87/2.32 % (1947805)Instructions burned: 114 (million)
% 9.87/2.32 % (1947806)Instruction limit reached!
% 9.87/2.32 % (1947806)------------------------------
% 9.87/2.32 % (1947806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947806)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947806)Termination reason: Instruction limit
% 9.87/2.32 % (1947806)Termination phase: Saturation
% 9.87/2.32 % (1947806)Time elapsed: 0.111 s
% 9.87/2.32 % (1947806)Peak memory usage: 90 MB
% 9.87/2.32 % (1947806)Instructions burned: 180 (million)
% 9.87/2.32 % (1947815)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=2690354810:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.87/2.32 % (1947817)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1988553101:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.87/2.32 % (1947816)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=677920564: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)
% 9.87/2.32 % (1947818)lrs+10_64_to=lpo:sil=8000:random_seed=3982320994:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 9.87/2.32 % (1947815)Instruction limit reached!
% 9.87/2.32 % (1947815)------------------------------
% 9.87/2.32 % (1947815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947815)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947815)Termination reason: Instruction limit
% 9.87/2.32 % (1947815)Termination phase: Saturation
% 9.87/2.32 % (1947815)Time elapsed: 0.084 s
% 9.87/2.32 % (1947815)Peak memory usage: 90 MB
% 9.87/2.32 % (1947815)Instructions burned: 144 (million)
% 9.87/2.32 % (1947816)Instruction limit reached!
% 9.87/2.32 % (1947816)------------------------------
% 9.87/2.32 % (1947816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947816)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947816)Termination reason: Instruction limit
% 9.87/2.32 % (1947816)Termination phase: Saturation
% 9.87/2.32 % (1947816)Time elapsed: 0.097 s
% 9.87/2.32 % (1947816)Peak memory usage: 91 MB
% 9.87/2.32 % (1947816)Instructions burned: 191 (million)
% 9.87/2.32 % (1947818)Instruction limit reached!
% 9.87/2.32 % (1947818)------------------------------
% 9.87/2.32 % (1947818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947818)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947818)Termination reason: Instruction limit
% 9.87/2.32 % (1947818)Termination phase: Saturation
% 9.87/2.32 % (1947818)Time elapsed: 0.075 s
% 9.87/2.32 % (1947818)Peak memory usage: 91 MB
% 9.87/2.32 % (1947818)Instructions burned: 126 (million)
% 9.87/2.32 % (1947817)Instruction limit reached!
% 9.87/2.32 % (1947817)------------------------------
% 9.87/2.32 % (1947817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947817)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947817)Termination reason: Instruction limit
% 9.87/2.32 % (1947817)Termination phase: Saturation
% 9.87/2.32 % (1947817)Time elapsed: 0.125 s
% 9.87/2.32 % (1947817)Peak memory usage: 91 MB
% 9.87/2.32 % (1947817)Instructions burned: 220 (million)
% 9.87/2.32 % (1947823)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2912966386:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 9.87/2.32 % (1947824)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1829627260:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 9.87/2.32 % (1947826)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=1231838071:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 9.87/2.32 % (1947825)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3934026034:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 9.87/2.32 % (1947824)Instruction limit reached!
% 9.87/2.32 % (1947824)------------------------------
% 9.87/2.32 % (1947824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947824)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947824)Termination reason: Instruction limit
% 9.87/2.32 % (1947824)Termination phase: Saturation
% 9.87/2.32 % (1947824)Time elapsed: 0.090 s
% 9.87/2.32 % (1947824)Peak memory usage: 92 MB
% 9.87/2.32 % (1947824)Instructions burned: 158 (million)
% 9.87/2.32 % (1947826)Instruction limit reached!
% 9.87/2.32 % (1947826)------------------------------
% 9.87/2.32 % (1947826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947826)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947826)Termination reason: Instruction limit
% 9.87/2.32 % (1947826)Termination phase: Saturation
% 9.87/2.32 % (1947826)Time elapsed: 0.063 s
% 9.87/2.32 % (1947826)Peak memory usage: 89 MB
% 9.87/2.32 % (1947826)Instructions burned: 107 (million)
% 9.87/2.32 % (1947823)Instruction limit reached!
% 9.87/2.32 % (1947823)------------------------------
% 9.87/2.32 % (1947823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947823)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947823)Termination reason: Instruction limit
% 9.87/2.32 % (1947823)Termination phase: Saturation
% 9.87/2.32 % (1947823)Time elapsed: 0.118 s
% 9.87/2.32 % (1947823)Peak memory usage: 91 MB
% 9.87/2.32 % (1947823)Instructions burned: 196 (million)
% 9.87/2.32 % (1947832)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1203878591:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 9.87/2.32 % (1947831)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=143456572:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 9.87/2.32 % (1947833)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2143423087:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 9.87/2.32 % (1947831)Instruction limit reached!
% 9.87/2.32 % (1947831)------------------------------
% 9.87/2.32 % (1947831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947831)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947831)Termination reason: Instruction limit
% 9.87/2.32 % (1947831)Termination phase: Saturation
% 9.87/2.32 % (1947831)Time elapsed: 0.062 s
% 9.87/2.32 % (1947831)Peak memory usage: 90 MB
% 9.87/2.32 % (1947831)Instructions burned: 108 (million)
% 9.87/2.32 % (1947832)Instruction limit reached!
% 9.87/2.32 % (1947832)------------------------------
% 9.87/2.32 % (1947832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947832)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947832)Termination reason: Instruction limit
% 9.87/2.32 % (1947832)Termination phase: Saturation
% 9.87/2.32 % (1947832)Time elapsed: 0.139 s
% 9.87/2.32 % (1947832)Peak memory usage: 90 MB
% 9.87/2.32 % (1947832)Instructions burned: 242 (million)
% 9.87/2.32 % (1947837)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2652878059:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 9.87/2.32 % (1947837)Instruction limit reached!
% 9.87/2.32 % (1947837)------------------------------
% 9.87/2.32 % (1947837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947837)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947837)Termination reason: Instruction limit
% 9.87/2.32 % (1947837)Termination phase: Saturation
% 9.87/2.32 % (1947837)Time elapsed: 0.066 s
% 9.87/2.32 % (1947837)Peak memory usage: 89 MB
% 9.87/2.32 % (1947837)Instructions burned: 135 (million)
% 9.87/2.32 % (1947838)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2929705526:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 9.87/2.32 % (1947801)First to succeed.
% 9.87/2.32 % (1947801)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1947796"
% 9.87/2.32 % (1947840)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3994031917:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 9.87/2.32 % (1947840)Instruction limit reached!
% 9.87/2.32 % (1947840)------------------------------
% 9.87/2.32 % (1947840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947840)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947840)Termination reason: Instruction limit
% 9.87/2.32 % (1947840)Termination phase: Saturation
% 9.87/2.32 % (1947840)Time elapsed: 0.118 s
% 9.87/2.32 % (1947840)Peak memory usage: 92 MB
% 9.87/2.32 % (1947840)Instructions burned: 191 (million)
% 9.87/2.32 % (1947838)Instruction limit reached!
% 9.87/2.32 % (1947838)------------------------------
% 9.87/2.32 % (1947838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.32 % (1947838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.32 % (1947838)CaDiCaL version: 2.1.3
% 9.87/2.32 % (1947838)Termination reason: Instruction limit
% 9.87/2.32 % (1947838)Termination phase: Saturation
% 9.87/2.32 % (1947838)Time elapsed: 0.331 s
% 9.87/2.32 % (1947838)Peak memory usage: 96 MB
% 9.87/2.32 % (1947838)Instructions burned: 500 (million)
% 9.87/2.32 % (1947801)Refutation found. Thanks to Tanya!
% 9.87/2.32 % SZS status Unsatisfiable for theBenchmark
% 9.87/2.32 % SZS output start Proof for theBenchmark
% See solution above
% 11.92/2.52 % (1947801)------------------------------
% 11.92/2.52 % (1947801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.92/2.52 % (1947801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.92/2.52 % (1947801)CaDiCaL version: 2.1.3
% 11.92/2.52 % (1947801)Termination reason: Refutation
% 11.92/2.52 % (1947801)Time elapsed: 1.148 s
% 11.92/2.52 % (1947801)Peak memory usage: 145 MB
% 11.92/2.52 % (1947801)Instructions burned: 1839 (million)
% 11.92/2.52 % (1947801)------------------------------
% 11.92/2.52 % (1947801)------------------------------
% 11.92/2.52 % (1947796)Success in time 1.64 s
% 11.92/2.52 % Vampire exiting
%------------------------------------------------------------------------------