%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW203+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:39:36 PM UTC 2026
% Result : Theorem 145.72s 27.83s
% Output : Refutation 145.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 79
% Syntax : Number of formulae : 432 ( 296 unt; 0 def)
% Number of atoms : 615 ( 315 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 314 ( 131 ~; 135 |; 16 &)
% ( 6 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 8 con; 0-3 aty)
% Number of variables : 516 ( 516 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096) ).
fof(f7,axiom,
! [X0] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__abs) ).
fof(f12,axiom,
! [X0,X1] : c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(X1),c_Complex_OIm(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Im_Odiff) ).
fof(f13,axiom,
! [X0,X1] : c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_ORe(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Re_Odiff) ).
fof(f15,axiom,
! [X0,X1] :
( class_Groups_Ocomm__monoid__add(X1)
=> c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add_Ocomm__neutral) ).
fof(f18,axiom,
! [X0,X1] :
( class_Groups_Ocomm__monoid__add(X1)
=> c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__0) ).
fof(f23,axiom,
! [X0,X1] :
( class_Groups_Ogroup__add(X1)
=> c_Groups_Ominus__class_Ominus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_diff__0__right) ).
fof(f40,axiom,
! [X0,X1] :
( class_Groups_Oordered__ab__group__add__abs(X1)
=> c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1),c_Groups_Oabs__class_Oabs(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__ge__zero) ).
fof(f41,axiom,
! [X0,X1] : c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_ORe(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Re_Oadd) ).
fof(f46,axiom,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0))
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__ge__0__iff) ).
fof(f64,axiom,
! [X0,X1] :
( c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = X0
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1)
=> c_NthRoot_Osqrt(X0) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__unique) ).
fof(f66,axiom,
! [X0] :
( c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = X0
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__pow2__iff) ).
fof(f85,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__le__iff) ).
fof(f86,axiom,
! [X0,X1] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,X0)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__power) ).
fof(f135,axiom,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1)
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__le__trans) ).
fof(f136,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
=> X1 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__le__antisym) ).
fof(f144,axiom,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit0__def) ).
fof(f194,axiom,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__commute) ).
fof(f197,axiom,
! [X0,X1,X2,X3] :
( class_Groups_Oab__semigroup__mult(X3)
=> c_Groups_Otimes__class_Otimes(X3,c_Groups_Otimes__class_Otimes(X3,X2,X1),X0) = c_Groups_Otimes__class_Otimes(X3,X2,c_Groups_Otimes__class_Otimes(X3,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ab__semigroup__mult__class_Omult__ac_I1_J) ).
fof(f220,axiom,
! [X0,X1] : c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__mult) ).
fof(f221,axiom,
! [X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_OIm(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(X1),c_Complex_ORe(X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__Im__mult) ).
fof(f222,axiom,
! [X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_ORe(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(X1),c_Complex_OIm(X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__Re__mult) ).
fof(f229,axiom,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__Re__le__cmod) ).
fof(f231,axiom,
! [X0] : c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__abs2) ).
fof(f236,axiom,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(X0)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__Re__le__cmod) ).
fof(f324,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> c_Groups_Otimes__class_Otimes(X1,X0,X0) = c_Power_Opower__class_Opower(X1,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
fof(f350,axiom,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(f358,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Groups_Otimes__class_Otimes(X2,X1,X0) = c_Groups_Otimes__class_Otimes(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(f359,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f367,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> c_Groups_Otimes__class_Otimes(X1,c_Groups_Ozero__class_Ozero(X1),X0) = c_Groups_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J) ).
fof(f399,axiom,
! [X0,X1,X2] :
( class_RealVector_Oreal__normed__div__algebra(X2)
=> c_RealVector_Onorm__class_Onorm(X2,c_Power_Opower__class_Opower(X2,X1,X0)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__power) ).
fof(f401,axiom,
! [X0,X1,X2] :
( class_RealVector_Oreal__normed__algebra(X2)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,c_Groups_Otimes__class_Otimes(X2,X1,X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_RealVector_Onorm__class_Onorm(X2,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__mult__ineq) ).
fof(f446,axiom,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__norm) ).
fof(f450,axiom,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocnj(X0))) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__mod__mult__cnj) ).
fof(f459,axiom,
! [X0,X1] : c_Complex_OIm(c_Complex_Ocomplex_OComplex(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Im) ).
fof(f460,axiom,
! [X0,X1] : c_Complex_ORe(c_Complex_Ocomplex_OComplex(X1,X0)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Re) ).
fof(f504,axiom,
! [X0] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__surj) ).
fof(f507,axiom,
! [X0,X1,X2,X3] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X3,X2),c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X3,X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__add) ).
fof(f514,axiom,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocnj(X0))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__In__mult__cnj__zero) ).
fof(f519,axiom,
! [X0,X1,X2,X3] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X3,X2),c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X0)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__mult) ).
fof(f521,axiom,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocnj(X0)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__mod__sqrt__Re__mult__cnj) ).
fof(f524,axiom,
c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_semiring__norm_I115_J) ).
fof(f535,axiom,
! [X0] : c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Re__complex__of__real) ).
fof(f541,axiom,
! [X0] : c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Im__complex__of__real) ).
fof(f546,axiom,
! [X0] : c_RealVector_Oof__real(tc_Complex_Ocomplex,X0) = c_Complex_Ocomplex_OComplex(X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__of__real__def) ).
fof(f550,axiom,
! [X0,X1] :
( class_RealVector_Oreal__normed__algebra__1(X1)
=> c_RealVector_Onorm__class_Onorm(X1,c_RealVector_Oof__real(X1,X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__of__real) ).
fof(f554,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X2),c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__of__real__add__Complex) ).
fof(f574,axiom,
! [X0,X1,X2] :
( class_Rings_Oring(X2)
=> c_Groups_Otimes__class_Otimes(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),X0) = c_Groups_Otimes__class_Otimes(X2,X1,c_Groups_Ouminus__class_Ouminus(X2,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__mult__commute) ).
fof(f577,axiom,
! [X0,X1,X2] :
( class_Rings_Oring(X2)
=> c_Groups_Ouminus__class_Ouminus(X2,c_Groups_Otimes__class_Otimes(X2,X1,X0)) = c_Groups_Otimes__class_Otimes(X2,X1,c_Groups_Ouminus__class_Ouminus(X2,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__mult__right) ).
fof(f584,axiom,
! [X0,X1] :
( class_Groups_Ogroup__add(X1)
=> c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__minus) ).
fof(f590,axiom,
! [X0,X1] :
( class_RealVector_Oreal__normed__vector(X1)
=> c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_RealVector_Onorm__class_Onorm(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__minus__cancel) ).
fof(f611,axiom,
! [X0] :
( class_Groups_Ogroup__add(X0)
=> c_Groups_Ouminus__class_Ouminus(X0,c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__zero) ).
fof(f615,axiom,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_i__mult__Complex) ).
fof(f633,axiom,
! [X0,X1] :
( class_Groups_Ogroup__add(X1)
=> c_Groups_Ominus__class_Ominus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = c_Groups_Ouminus__class_Ouminus(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_diff__0) ).
fof(f648,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),X0)
<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__le__interval__iff) ).
fof(f660,axiom,
c_Complex_ORe(c_Complex_Oii) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__Re__i) ).
fof(f670,axiom,
! [X0] : c_Complex_Ocnj(X0) = c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_cnj__def) ).
fof(f674,axiom,
! [X0] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),c_Complex_Oii) = c_Complex_Ocomplex_OComplex(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__of__real__i) ).
fof(f691,axiom,
! [X0] : c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Re_Ominus) ).
fof(f692,axiom,
! [X0] : c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Im_Ominus) ).
fof(f695,axiom,
! [X0] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__i__mult__minus) ).
fof(f696,axiom,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__diff__def) ).
fof(f814,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__less__def) ).
fof(f886,axiom,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__lt__0__iff) ).
fof(f946,axiom,
! [X0] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) )
& ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__abs__def) ).
fof(f1102,axiom,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs) ).
fof(f1109,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__RealVector_Oreal__normed__vector) ).
fof(f1128,axiom,
class_Groups_Ocomm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Ocomm__monoid__add) ).
fof(f1131,axiom,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Ocomm__semiring__1) ).
fof(f1145,axiom,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Ogroup__add) ).
fof(f1161,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra) ).
fof(f1163,axiom,
class_RealVector_Oreal__normed__algebra__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra__1) ).
fof(f1164,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra) ).
fof(f1167,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1174,axiom,
class_Groups_Oab__semigroup__mult(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Oab__semigroup__mult) ).
fof(f1179,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(f1190,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ogroup__add) ).
fof(f1199,axiom,
class_Rings_Oring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Oring) ).
fof(f1202,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1203,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))))),
inference(negated_conjecture,[status(cth)],[f1202]) ).
fof(f1204,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))))),
inference(flattening,[],[f1203]) ).
fof(f1210,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0
| ~ class_Groups_Ocomm__monoid__add(X1) ),
inference(ennf_transformation,[],[f15]) ).
fof(f1213,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0
| ~ class_Groups_Ocomm__monoid__add(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f1218,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0
| ~ class_Groups_Ogroup__add(X1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f1239,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1),c_Groups_Oabs__class_Oabs(X1,X0))
| ~ class_Groups_Oordered__ab__group__add__abs(X1) ),
inference(ennf_transformation,[],[f40]) ).
fof(f1265,plain,
! [X0,X1] :
( c_NthRoot_Osqrt(X0) = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(ennf_transformation,[],[f64]) ).
fof(f1266,plain,
! [X0,X1] :
( c_NthRoot_Osqrt(X0) = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(flattening,[],[f1265]) ).
fof(f1318,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1) ),
inference(ennf_transformation,[],[f135]) ).
fof(f1319,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1) ),
inference(flattening,[],[f1318]) ).
fof(f1320,plain,
! [X0,X1] :
( X1 = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(ennf_transformation,[],[f136]) ).
fof(f1321,plain,
! [X0,X1] :
( X1 = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(flattening,[],[f1320]) ).
fof(f1345,plain,
! [X0,X1,X2,X3] :
( c_Groups_Otimes__class_Otimes(X3,c_Groups_Otimes__class_Otimes(X3,X2,X1),X0) = c_Groups_Otimes__class_Otimes(X3,X2,c_Groups_Otimes__class_Otimes(X3,X1,X0))
| ~ class_Groups_Oab__semigroup__mult(X3) ),
inference(ennf_transformation,[],[f197]) ).
fof(f1453,plain,
! [X0,X1] :
( c_Groups_Otimes__class_Otimes(X1,X0,X0) = c_Power_Opower__class_Opower(X1,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f324]) ).
fof(f1470,plain,
! [X0,X1,X2] :
( c_Groups_Otimes__class_Otimes(X2,X1,X0) = c_Groups_Otimes__class_Otimes(X2,X0,X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f358]) ).
fof(f1471,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f359]) ).
fof(f1478,plain,
! [X0,X1] :
( c_Groups_Otimes__class_Otimes(X1,c_Groups_Ozero__class_Ozero(X1),X0) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f367]) ).
fof(f1511,plain,
! [X0,X1,X2] :
( c_RealVector_Onorm__class_Onorm(X2,c_Power_Opower__class_Opower(X2,X1,X0)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),X0)
| ~ class_RealVector_Oreal__normed__div__algebra(X2) ),
inference(ennf_transformation,[],[f399]) ).
fof(f1513,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,c_Groups_Otimes__class_Otimes(X2,X1,X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_RealVector_Onorm__class_Onorm(X2,X0)))
| ~ class_RealVector_Oreal__normed__algebra(X2) ),
inference(ennf_transformation,[],[f401]) ).
fof(f1616,plain,
! [X0,X1] :
( c_RealVector_Onorm__class_Onorm(X1,c_RealVector_Oof__real(X1,X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)
| ~ class_RealVector_Oreal__normed__algebra__1(X1) ),
inference(ennf_transformation,[],[f550]) ).
fof(f1636,plain,
! [X0,X1,X2] :
( c_Groups_Otimes__class_Otimes(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),X0) = c_Groups_Otimes__class_Otimes(X2,X1,c_Groups_Ouminus__class_Ouminus(X2,X0))
| ~ class_Rings_Oring(X2) ),
inference(ennf_transformation,[],[f574]) ).
fof(f1639,plain,
! [X0,X1,X2] :
( c_Groups_Ouminus__class_Ouminus(X2,c_Groups_Otimes__class_Otimes(X2,X1,X0)) = c_Groups_Otimes__class_Otimes(X2,X1,c_Groups_Ouminus__class_Ouminus(X2,X0))
| ~ class_Rings_Oring(X2) ),
inference(ennf_transformation,[],[f577]) ).
fof(f1646,plain,
! [X0,X1] :
( c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = X0
| ~ class_Groups_Ogroup__add(X1) ),
inference(ennf_transformation,[],[f584]) ).
fof(f1649,plain,
! [X0,X1] :
( c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_RealVector_Onorm__class_Onorm(X1,X0)
| ~ class_RealVector_Oreal__normed__vector(X1) ),
inference(ennf_transformation,[],[f590]) ).
fof(f1671,plain,
! [X0] :
( c_Groups_Ouminus__class_Ouminus(X0,c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(X0)
| ~ class_Groups_Ogroup__add(X0) ),
inference(ennf_transformation,[],[f611]) ).
fof(f1698,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = c_Groups_Ouminus__class_Ouminus(X1,X0)
| ~ class_Groups_Ogroup__add(X1) ),
inference(ennf_transformation,[],[f633]) ).
fof(f2122,plain,
! [X0] :
( ( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) )
& ( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ) ),
inference(ennf_transformation,[],[f946]) ).
fof(f2229,plain,
! [X0] :
( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) )
& ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0)) ) ),
inference(nnf_transformation,[],[f46]) ).
fof(f2239,plain,
! [X0] :
( ( c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) )
& ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != X0 ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f2243,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) )
& ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0)) ) ),
inference(nnf_transformation,[],[f85]) ).
fof(f2393,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) )
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),X0) ) ),
inference(nnf_transformation,[],[f648]) ).
fof(f2394,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) )
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),X0) ) ),
inference(flattening,[],[f2393]) ).
fof(f2452,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| X0 = X1 )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
& X1 != X0 )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ) ),
inference(nnf_transformation,[],[f814]) ).
fof(f2453,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| X0 = X1 )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
& X1 != X0 )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ) ),
inference(flattening,[],[f2452]) ).
fof(f2476,plain,
! [X0] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) )
& ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ) ),
inference(nnf_transformation,[],[f886]) ).
fof(f2565,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))),
inference(cnf_transformation,[],[f1]) ).
fof(f2571,plain,
! [X0] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f7]) ).
fof(f2576,plain,
! [X0,X1] : c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(X1),c_Complex_OIm(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f2577,plain,
! [X0,X1] : c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_ORe(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f2580,plain,
! [X0,X1] :
( ~ class_Groups_Ocomm__monoid__add(X1)
| c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
inference(cnf_transformation,[],[f1210]) ).
fof(f2584,plain,
! [X0,X1] :
( ~ class_Groups_Ocomm__monoid__add(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0 ),
inference(cnf_transformation,[],[f1213]) ).
fof(f2591,plain,
! [X0,X1] :
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ominus__class_Ominus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
inference(cnf_transformation,[],[f1218]) ).
fof(f2618,plain,
! [X0,X1] :
( ~ class_Groups_Oordered__ab__group__add__abs(X1)
| c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1),c_Groups_Oabs__class_Oabs(X1,X0)) ),
inference(cnf_transformation,[],[f1239]) ).
fof(f2619,plain,
! [X0,X1] : c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_ORe(X0)),
inference(cnf_transformation,[],[f41]) ).
fof(f2625,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0)) ),
inference(cnf_transformation,[],[f2229]) ).
fof(f2626,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) ),
inference(cnf_transformation,[],[f2229]) ).
fof(f2653,plain,
! [X0,X1] :
( c_NthRoot_Osqrt(X0) = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(cnf_transformation,[],[f1266]) ).
fof(f2655,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(cnf_transformation,[],[f2239]) ).
fof(f2678,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f2679,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[],[f2243]) ).
fof(f2680,plain,
! [X0,X1] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,X0)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),X0),
inference(cnf_transformation,[],[f86]) ).
fof(f2746,plain,
! [X2,X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X0) ),
inference(cnf_transformation,[],[f1319]) ).
fof(f2747,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f1321]) ).
fof(f2758,plain,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(cnf_transformation,[],[f144]) ).
fof(f2820,plain,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),
inference(cnf_transformation,[],[f194]) ).
fof(f2823,plain,
! [X2,X3,X0,X1] :
( ~ class_Groups_Oab__semigroup__mult(X3)
| c_Groups_Otimes__class_Otimes(X3,c_Groups_Otimes__class_Otimes(X3,X2,X1),X0) = c_Groups_Otimes__class_Otimes(X3,X2,c_Groups_Otimes__class_Otimes(X3,X1,X0)) ),
inference(cnf_transformation,[],[f1345]) ).
fof(f2854,plain,
! [X0,X1] : c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0)),
inference(cnf_transformation,[],[f220]) ).
fof(f2855,plain,
! [X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_OIm(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(X1),c_Complex_ORe(X0))),
inference(cnf_transformation,[],[f221]) ).
fof(f2856,plain,
! [X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(X1),c_Complex_ORe(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(X1),c_Complex_OIm(X0))),
inference(cnf_transformation,[],[f222]) ).
fof(f2865,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)),
inference(cnf_transformation,[],[f229]) ).
fof(f2869,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)),
inference(cnf_transformation,[],[f231]) ).
fof(f2876,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(X0)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)),
inference(cnf_transformation,[],[f236]) ).
fof(f2980,plain,
! [X0,X1] :
( c_Power_Opower__class_Opower(X1,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Otimes__class_Otimes(X1,X0,X0)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(cnf_transformation,[],[f1453]) ).
fof(f3008,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f350]) ).
fof(f3016,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Groups_Otimes__class_Otimes(X2,X1,X0) = c_Groups_Otimes__class_Otimes(X2,X0,X1) ),
inference(cnf_transformation,[],[f1470]) ).
fof(f3017,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
inference(cnf_transformation,[],[f1471]) ).
fof(f3026,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Ozero__class_Ozero(X1) = c_Groups_Otimes__class_Otimes(X1,c_Groups_Ozero__class_Ozero(X1),X0) ),
inference(cnf_transformation,[],[f1478]) ).
fof(f3064,plain,
! [X2,X0,X1] :
( ~ class_RealVector_Oreal__normed__div__algebra(X2)
| c_RealVector_Onorm__class_Onorm(X2,c_Power_Opower__class_Opower(X2,X1,X0)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),X0) ),
inference(cnf_transformation,[],[f1511]) ).
fof(f3067,plain,
! [X2,X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,c_Groups_Otimes__class_Otimes(X2,X1,X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_RealVector_Onorm__class_Onorm(X2,X0)))
| ~ class_RealVector_Oreal__normed__algebra(X2) ),
inference(cnf_transformation,[],[f1513]) ).
fof(f3139,plain,
! [X0,X1] : c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0)),
inference(cnf_transformation,[],[f446]) ).
fof(f3145,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocnj(X0))) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),
inference(cnf_transformation,[],[f450]) ).
fof(f3158,plain,
! [X0,X1] : c_Complex_OIm(c_Complex_Ocomplex_OComplex(X1,X0)) = X0,
inference(cnf_transformation,[],[f459]) ).
fof(f3159,plain,
! [X0,X1] : c_Complex_ORe(c_Complex_Ocomplex_OComplex(X1,X0)) = X1,
inference(cnf_transformation,[],[f460]) ).
fof(f3224,plain,
! [X0] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0)) = X0,
inference(cnf_transformation,[],[f504]) ).
fof(f3229,plain,
! [X2,X3,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X3,X2),c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X3,X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0)),
inference(cnf_transformation,[],[f507]) ).
fof(f3238,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocnj(X0))),
inference(cnf_transformation,[],[f514]) ).
fof(f3245,plain,
! [X2,X3,X0,X1] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X3,X2),c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X0)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1))),
inference(cnf_transformation,[],[f519]) ).
fof(f3247,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocnj(X0)))),
inference(cnf_transformation,[],[f521]) ).
fof(f3250,plain,
c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))) = c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(cnf_transformation,[],[f524]) ).
fof(f3261,plain,
! [X0] : c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)) = X0,
inference(cnf_transformation,[],[f535]) ).
fof(f3269,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),
inference(cnf_transformation,[],[f541]) ).
fof(f3276,plain,
! [X0] : c_RealVector_Oof__real(tc_Complex_Ocomplex,X0) = c_Complex_Ocomplex_OComplex(X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(cnf_transformation,[],[f546]) ).
fof(f3280,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__algebra__1(X1)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(X1,c_RealVector_Oof__real(X1,X0)) ),
inference(cnf_transformation,[],[f1616]) ).
fof(f3284,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X2),c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1),X0),
inference(cnf_transformation,[],[f554]) ).
fof(f3308,plain,
! [X2,X0,X1] :
( ~ class_Rings_Oring(X2)
| c_Groups_Otimes__class_Otimes(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),X0) = c_Groups_Otimes__class_Otimes(X2,X1,c_Groups_Ouminus__class_Ouminus(X2,X0)) ),
inference(cnf_transformation,[],[f1636]) ).
fof(f3311,plain,
! [X2,X0,X1] :
( ~ class_Rings_Oring(X2)
| c_Groups_Otimes__class_Otimes(X2,X1,c_Groups_Ouminus__class_Ouminus(X2,X0)) = c_Groups_Ouminus__class_Ouminus(X2,c_Groups_Otimes__class_Otimes(X2,X1,X0)) ),
inference(cnf_transformation,[],[f1639]) ).
fof(f3321,plain,
! [X0,X1] :
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f1646]) ).
fof(f3327,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| c_RealVector_Onorm__class_Onorm(X1,X0) = c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) ),
inference(cnf_transformation,[],[f1649]) ).
fof(f3355,plain,
! [X0] :
( ~ class_Groups_Ogroup__add(X0)
| c_Groups_Ozero__class_Ozero(X0) = c_Groups_Ouminus__class_Ouminus(X0,c_Groups_Ozero__class_Ozero(X0)) ),
inference(cnf_transformation,[],[f1671]) ).
fof(f3359,plain,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Ocomplex_OComplex(X1,X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1),
inference(cnf_transformation,[],[f615]) ).
fof(f3385,plain,
! [X0,X1] :
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ouminus__class_Ouminus(X1,X0) = c_Groups_Ominus__class_Ominus(X1,c_Groups_Ozero__class_Ozero(X1),X0) ),
inference(cnf_transformation,[],[f1698]) ).
fof(f3410,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1) ),
inference(cnf_transformation,[],[f2394]) ).
fof(f3443,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Complex_ORe(c_Complex_Oii),
inference(cnf_transformation,[],[f660]) ).
fof(f3457,plain,
! [X0] : c_Complex_Ocnj(X0) = c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))),
inference(cnf_transformation,[],[f670]) ).
fof(f3461,plain,
! [X0] : c_Complex_Ocomplex_OComplex(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),c_Complex_Oii),
inference(cnf_transformation,[],[f674]) ).
fof(f3478,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),
inference(cnf_transformation,[],[f691]) ).
fof(f3479,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),
inference(cnf_transformation,[],[f692]) ).
fof(f3482,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)),
inference(cnf_transformation,[],[f695]) ).
fof(f3483,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),
inference(cnf_transformation,[],[f696]) ).
fof(f3665,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[],[f2453]) ).
fof(f3766,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cnf_transformation,[],[f2476]) ).
fof(f3767,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cnf_transformation,[],[f2476]) ).
fof(f3867,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ),
inference(cnf_transformation,[],[f2122]) ).
fof(f4135,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1102]) ).
fof(f4142,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1109]) ).
fof(f4161,plain,
class_Groups_Ocomm__monoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1128]) ).
fof(f4164,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1131]) ).
fof(f4178,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1145]) ).
fof(f4194,plain,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1161]) ).
fof(f4196,plain,
class_RealVector_Oreal__normed__algebra__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1163]) ).
fof(f4197,plain,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1164]) ).
fof(f4200,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1167]) ).
fof(f4207,plain,
class_Groups_Oab__semigroup__mult(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1174]) ).
fof(f4212,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1179]) ).
fof(f4223,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1190]) ).
fof(f4232,plain,
class_Rings_Oring(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1199]) ).
fof(f4235,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))))),
inference(cnf_transformation,[],[f1204]) ).
fof(f4236,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))))),
inference(definition_unfolding,[],[f2565,f2758,f2758,f2758,f2758,f2758,f2758]) ).
fof(f4242,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls))))),
inference(definition_unfolding,[],[f2571,f2758]) ).
fof(f4258,plain,
! [X0,X1] :
( c_NthRoot_Osqrt(X0) = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(definition_unfolding,[],[f2653,f2758]) ).
fof(f4261,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(definition_unfolding,[],[f2655,f2758]) ).
fof(f4320,plain,
! [X0,X1] :
( c_Groups_Otimes__class_Otimes(X1,X0,X0) = c_Power_Opower__class_Opower(X1,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls))))
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(definition_unfolding,[],[f2980,f2758]) ).
fof(f4321,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),
inference(definition_unfolding,[],[f3139,f2758,f2758]) ).
fof(f4323,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))))) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),
inference(definition_unfolding,[],[f3145,f3457,f2758]) ).
fof(f4337,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))))),
inference(definition_unfolding,[],[f3238,f3457]) ).
fof(f4338,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0)))))),
inference(definition_unfolding,[],[f3247,f3457]) ).
fof(f4340,plain,
c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls))),
inference(definition_unfolding,[],[f3250,f2758]) ).
fof(f4390,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))))),
inference(definition_unfolding,[],[f4235,f2758,f2758]) ).
fof(f4411,plain,
! [X1] :
( c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls))))) = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1) ),
inference(equality_resolution,[],[f4258]) ).
fof(f4621,plain,
! [X0] : c_RealVector_Oof__real(tc_Complex_Ocomplex,X0) = c_Complex_Ocomplex_OComplex(X0,c_Complex_ORe(c_Complex_Oii)),
inference(forward_demodulation,[],[f3276,f3443]) ).
fof(f4624,plain,
! [X0] : c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)) = c_Complex_ORe(c_Complex_Oii),
inference(forward_demodulation,[],[f3269,f3443]) ).
fof(f4631,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)))))),
inference(forward_demodulation,[],[f4338,f3479]) ).
fof(f4634,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))))),
inference(forward_demodulation,[],[f4337,f3479]) ).
fof(f4650,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))))) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
inference(forward_demodulation,[],[f4323,f4340]) ).
fof(f4654,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),
inference(forward_demodulation,[],[f4321,f4340]) ).
fof(f4665,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Otimes__class_Otimes(X1,X0,X0) = c_Power_Opower__class_Opower(X1,X0,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) ),
inference(forward_demodulation,[],[f4320,f4340]) ).
fof(f4719,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0)
| c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))) != X0 ),
inference(forward_demodulation,[],[f4261,f3443]) ).
fof(f4722,plain,
! [X1] :
( c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1) ),
inference(forward_demodulation,[],[f4411,f4340]) ).
fof(f4735,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0)) ),
inference(forward_demodulation,[],[f2625,f3443]) ).
fof(f4736,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) ),
inference(forward_demodulation,[],[f2626,f3443]) ).
fof(f4746,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
inference(forward_demodulation,[],[f4242,f4340]) ).
fof(f4752,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))))),
inference(forward_demodulation,[],[f4236,f4340]) ).
fof(f4771,plain,
! [X0] : c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))))),
inference(forward_demodulation,[],[f4634,f3443]) ).
fof(f4781,plain,
! [X0] : c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))))),
inference(forward_demodulation,[],[f4650,f3479]) ).
fof(f4805,plain,
! [X0] :
( c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls))))) != X0
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(forward_demodulation,[],[f4719,f2680]) ).
fof(f4808,plain,
! [X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1)
| c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X1,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) = X1 ),
inference(forward_demodulation,[],[f4722,f3443]) ).
fof(f4809,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(forward_demodulation,[],[f4735,f3443]) ).
fof(f4810,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(forward_demodulation,[],[f4736,f3443]) ).
fof(f4821,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_x),c_Complex_OIm(v_y)))))),
inference(forward_demodulation,[],[f4752,f4654]) ).
fof(f4846,plain,
! [X0] :
( c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) != X0
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(forward_demodulation,[],[f4805,f4340]) ).
fof(f4849,plain,
! [X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1) = X1 ),
inference(forward_demodulation,[],[f4808,f4746]) ).
fof(f4852,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4821,f2576]) ).
fof(f4860,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) != X0 ),
inference(forward_demodulation,[],[f4846,f4746]) ).
fof(f4864,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Complex_ORe(c_Complex_Oii)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4852,f3443]) ).
fof(f4868,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Complex_ORe(c_Complex_Oii)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Complex_ORe(c_Complex_Oii))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4864,f4654]) ).
fof(f4869,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)),c_Complex_ORe(c_Complex_Oii)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4868,f4621]) ).
fof(f4870,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Complex_ORe(c_Complex_Oii)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4869,f2577]) ).
fof(f4871,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Complex_ORe(c_Complex_Oii)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4870,f4654]) ).
fof(f4872,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Complex_ORe(c_Complex_Oii)),c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4871,f3229]) ).
fof(f4873,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4872,f4621]) ).
fof(f4874,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Complex_ORe(c_Complex_Oii)),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4873,f3284]) ).
fof(f4875,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y),c_Complex_Oii)),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(forward_demodulation,[],[f4874,f2619]) ).
fof(f4998,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = X0,
inference(resolution,[],[f2580,f4161]) ).
fof(f5003,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Complex_ORe(c_Complex_Oii)) = X0,
inference(forward_demodulation,[],[f4998,f3443]) ).
fof(f5010,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) = X0,
inference(resolution,[],[f2584,f4161]) ).
fof(f5015,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) = X0,
inference(forward_demodulation,[],[f5010,f3443]) ).
fof(f5028,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = X0,
inference(resolution,[],[f2591,f4178]) ).
fof(f5030,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,c_Complex_ORe(c_Complex_Oii)) = X0,
inference(forward_demodulation,[],[f5028,f3443]) ).
fof(f5038,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)),
inference(resolution,[],[f2618,f4135]) ).
fof(f5039,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)),
inference(forward_demodulation,[],[f5038,f3443]) ).
fof(f5179,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = X0,
inference(resolution,[],[f3321,f4223]) ).
fof(f5186,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(resolution,[],[f3355,f4178]) ).
fof(f5188,plain,
c_Complex_ORe(c_Complex_Oii) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii)),
inference(forward_demodulation,[],[f5186,f3443]) ).
fof(f5189,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),
inference(forward_demodulation,[],[f5188,f3478]) ).
fof(f5234,plain,
! [X0,X1] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0))),
inference(superposition,[],[f3479,f3158]) ).
fof(f5360,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)) ),
inference(superposition,[],[f2678,f2869]) ).
fof(f5465,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0),
inference(resolution,[],[f3026,f4164]) ).
fof(f5470,plain,
! [X0] : c_Complex_ORe(c_Complex_Oii) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0),
inference(forward_demodulation,[],[f5465,f3443]) ).
fof(f5478,plain,
! [X0] : c_Complex_ORe(c_Complex_Oii) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_ORe(c_Complex_Oii)),
inference(superposition,[],[f2820,f5470]) ).
fof(f5912,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii)),
inference(resolution,[],[f4849,f2865]) ).
fof(f6200,plain,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X0) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,X1),
inference(resolution,[],[f3016,f4212]) ).
fof(f6203,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),
inference(resolution,[],[f3017,f4164]) ).
fof(f6365,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),
inference(resolution,[],[f3280,f4196]) ).
fof(f6375,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
inference(resolution,[],[f3327,f4142]) ).
fof(f6376,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),
inference(resolution,[],[f3327,f4200]) ).
fof(f6377,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
inference(forward_demodulation,[],[f6375,f3008]) ).
fof(f6378,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
inference(forward_demodulation,[],[f6377,f3008]) ).
fof(f6416,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0),
inference(resolution,[],[f3385,f4178]) ).
fof(f6418,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0),
inference(forward_demodulation,[],[f6416,f3443]) ).
fof(f6550,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),
inference(superposition,[],[f3483,f5179]) ).
fof(f6619,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_NthRoot_Osqrt(X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0)) ),
inference(resolution,[],[f3766,f3867]) ).
fof(f6628,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Complex_ORe(c_Complex_Oii))
| c_NthRoot_Osqrt(X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0)) ),
inference(forward_demodulation,[],[f6619,f3443]) ).
fof(f6637,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(resolution,[],[f3767,f3665]) ).
fof(f6642,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Complex_ORe(c_Complex_Oii))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[],[f6637,f3443]) ).
fof(f6646,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Complex_ORe(c_Complex_Oii))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Complex_ORe(c_Complex_Oii)) ),
inference(forward_demodulation,[],[f6642,f3443]) ).
fof(f7082,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0)
| c_NthRoot_Osqrt(X0) != c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0)) ),
inference(resolution,[],[f4809,f4860]) ).
fof(f7107,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))),
inference(superposition,[],[f6378,f3479]) ).
fof(f7230,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(superposition,[],[f4390,f2576]) ).
fof(f7236,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_x),c_Complex_ORe(v_y))))),
inference(forward_demodulation,[],[f7230,f6203]) ).
fof(f7249,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f7236,f2577]) ).
fof(f7257,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f7249,f6203]) ).
fof(f7259,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f7257,f4340]) ).
fof(f7260,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f7259,f4654]) ).
fof(f7261,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f7260,f3224]) ).
fof(f7271,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(X0),c_Complex_ORe(c_Complex_Oii)) = c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),
inference(superposition,[],[f2577,f5189]) ).
fof(f7277,plain,
! [X0] : c_Complex_ORe(X0) = c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(superposition,[],[f5030,f2577]) ).
fof(f7287,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(X0),c_Complex_ORe(c_Complex_Oii)) = c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(forward_demodulation,[],[f7271,f6550]) ).
fof(f7293,plain,
! [X0] : c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,c_Complex_Oii)) = c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(forward_demodulation,[],[f7287,f2577]) ).
fof(f7298,plain,
! [X0] : c_Complex_ORe(X0) = c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(forward_demodulation,[],[f7293,f7277]) ).
fof(f15923,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,X0) = c_Power_Opower__class_Opower(tc_Complex_Ocomplex,X0,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
inference(resolution,[],[f4665,f4212]) ).
fof(f18774,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Power_Opower__class_Opower(tc_Complex_Ocomplex,X0,X1)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),X1),
inference(resolution,[],[f3064,f4194]) ).
fof(f20083,plain,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),X1) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1)),
inference(resolution,[],[f3308,f4232]) ).
fof(f20175,plain,
! [X0,X1] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,X1)) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1)),
inference(resolution,[],[f3311,f4232]) ).
fof(f22501,plain,
! [X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X2),c_Complex_ORe(c_Complex_Oii))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X2) ),
inference(global_subsumption,[],[f7082,f6646,f6628]) ).
fof(f22515,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),X1) ),
inference(resolution,[],[f22501,f2746]) ).
fof(f22718,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(resolution,[],[f22515,f5039]) ).
fof(f23440,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1) ),
inference(global_subsumption,[],[f22718,f5360]) ).
fof(f23522,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1) ),
inference(superposition,[],[f23440,f2854]) ).
fof(f23524,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1) ),
inference(forward_demodulation,[],[f23522,f2869]) ).
fof(f26306,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Complex_OIm(X0))))),
inference(superposition,[],[f4631,f5179]) ).
fof(f26313,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii) = c_NthRoot_Osqrt(c_Complex_ORe(c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),c_Complex_ORe(c_Complex_Oii)))),
inference(superposition,[],[f4631,f3359]) ).
fof(f26379,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii) = c_NthRoot_Osqrt(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)))),
inference(forward_demodulation,[],[f26313,f3159]) ).
fof(f26386,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Complex_OIm(X0)))))),
inference(forward_demodulation,[],[f26306,f20083]) ).
fof(f26398,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii) = c_NthRoot_Osqrt(c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)))),
inference(forward_demodulation,[],[f26379,f3479]) ).
fof(f26405,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Complex_OIm(X0)))))),
inference(forward_demodulation,[],[f26386,f20175]) ).
fof(f26410,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii) = c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii)),
inference(forward_demodulation,[],[f26398,f5179]) ).
fof(f26416,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Complex_OIm(X0)))))),
inference(forward_demodulation,[],[f26405,f6376]) ).
fof(f27145,plain,
! [X2,X0,X1] : c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,X1),X2) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X2)),
inference(resolution,[],[f2823,f4207]) ).
fof(f31292,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1) = X1 ),
inference(global_subsumption,[],[f23524,f4849]) ).
fof(f31680,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii))
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ),
inference(superposition,[],[f31292,f5912]) ).
fof(f31685,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii)))
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ),
inference(forward_demodulation,[],[f31680,f26410]) ).
fof(f31794,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii)))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(global_subsumption,[],[f31685,f4860]) ).
fof(f31847,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Complex_OIm(c_Complex_Oii)) ),
inference(resolution,[],[f31794,f2678]) ).
fof(f31929,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Complex_OIm(c_Complex_Oii))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0) ),
inference(resolution,[],[f31847,f4809]) ).
fof(f53967,plain,
! [X2,X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1),X2)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X2)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Ocomplex_OComplex(X0,X1)),c_Complex_ORe(X2))),
inference(superposition,[],[f2855,f3159]) ).
fof(f53968,plain,
! [X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X1)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),c_Complex_ORe(X1))),
inference(superposition,[],[f2855,f3261]) ).
fof(f53977,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0))),
inference(superposition,[],[f2855,f5470]) ).
fof(f54056,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)),
inference(forward_demodulation,[],[f53977,f5015]) ).
fof(f54065,plain,
! [X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X1)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_ORe(X1))),
inference(forward_demodulation,[],[f53968,f4624]) ).
fof(f54066,plain,
! [X2,X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1),X2)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X2)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Complex_ORe(X2))),
inference(forward_demodulation,[],[f53967,f3158]) ).
fof(f54092,plain,
! [X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X1)),c_Complex_ORe(c_Complex_Oii)),
inference(forward_demodulation,[],[f54065,f5470]) ).
fof(f54113,plain,
! [X0,X1] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X1)),
inference(forward_demodulation,[],[f54092,f5003]) ).
fof(f54218,plain,
! [X0] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(X0),c_Complex_OIm(c_Complex_Oii))),
inference(superposition,[],[f2856,f5478]) ).
fof(f54224,plain,
! [X2,X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0),X2)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Ocomplex_OComplex(X1,X0)),c_Complex_ORe(X2)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X2))),
inference(superposition,[],[f2856,f3158]) ).
fof(f54225,plain,
! [X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),c_Complex_ORe(X1)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(X1))),
inference(superposition,[],[f2856,f4624]) ).
fof(f54271,plain,
! [X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),c_Complex_ORe(X1)),c_Complex_ORe(c_Complex_Oii)),
inference(forward_demodulation,[],[f54225,f5470]) ).
fof(f54272,plain,
! [X2,X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X1,X0),X2)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Complex_ORe(X2)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_OIm(X2))),
inference(forward_demodulation,[],[f54224,f3159]) ).
fof(f54276,plain,
! [X0] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(X0),c_Complex_OIm(c_Complex_Oii))),
inference(forward_demodulation,[],[f54218,f6418]) ).
fof(f54302,plain,
! [X0,X1] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),c_Complex_ORe(X1)),
inference(forward_demodulation,[],[f54271,f5030]) ).
fof(f54324,plain,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Complex_ORe(X1)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0),X1)),
inference(forward_demodulation,[],[f54302,f3261]) ).
fof(f71356,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) != X0 ),
inference(global_subsumption,[],[f4860,f4810]) ).
fof(f71387,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),X1)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) != X0
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X1) ),
inference(resolution,[],[f71356,f2746]) ).
fof(f76732,plain,
! [X0,X1] :
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) != X0
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X1))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(resolution,[],[f71387,f2679]) ).
fof(f82246,plain,
! [X0] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii) != c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),X0) ),
inference(superposition,[],[f76732,f5912]) ).
fof(f82253,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),X0) ),
inference(trivial_inequality_removal,[],[f82246]) ).
fof(f82258,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii)),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(X0)) ),
inference(forward_demodulation,[],[f82253,f26410]) ).
fof(f82419,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii)))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii))) ),
inference(resolution,[],[f82258,f31929]) ).
fof(f82628,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_NthRoot_Osqrt(c_Complex_OIm(c_Complex_Oii))),
inference(duplicate_literal_removal,[],[f82419]) ).
fof(f82716,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Complex_Oii)),
inference(resolution,[],[f82628,f4809]) ).
fof(f82748,plain,
c_Complex_OIm(c_Complex_Oii) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii)),
inference(resolution,[],[f82716,f4849]) ).
fof(f83275,plain,
c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),c_Complex_ORe(c_Complex_Oii))),
inference(superposition,[],[f4781,f3359]) ).
fof(f83458,plain,
c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))))),
inference(forward_demodulation,[],[f83275,f4621]) ).
fof(f83520,plain,
c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)))),
inference(forward_demodulation,[],[f83458,f6365]) ).
fof(f83551,plain,
c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),
inference(forward_demodulation,[],[f83520,f6378]) ).
fof(f83565,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii)) = c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Oii),c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
inference(forward_demodulation,[],[f83551,f7107]) ).
fof(f83576,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Power_Opower__class_Opower(tc_Complex_Ocomplex,c_Complex_Oii,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
inference(forward_demodulation,[],[f83565,f18774]) ).
fof(f83583,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),
inference(forward_demodulation,[],[f83576,f15923]) ).
fof(f83589,plain,
c_Complex_OIm(c_Complex_Oii) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),
inference(forward_demodulation,[],[f83583,f82748]) ).
fof(f83603,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_OIm(c_Complex_Oii)),
inference(superposition,[],[f2876,f83589]) ).
fof(f83677,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)))
| ~ class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex) ),
inference(superposition,[],[f3067,f83589]) ).
fof(f83709,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
inference(forward_subsumption_resolution,[],[f83677,f4197]) ).
fof(f83726,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[],[f83709,f27145]) ).
fof(f83731,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[],[f83726,f3482]) ).
fof(f83733,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[],[f83731,f6376]) ).
fof(f84462,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii)),c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(resolution,[],[f83603,f3410]) ).
fof(f84488,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(forward_demodulation,[],[f84462,f3479]) ).
fof(f85156,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
inference(superposition,[],[f83733,f6365]) ).
fof(f85295,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),X0),
inference(resolution,[],[f85156,f3410]) ).
fof(f86156,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
inference(superposition,[],[f85295,f6378]) ).
fof(f95981,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(c_Complex_Oii))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii))),
inference(superposition,[],[f86156,f82748]) ).
fof(f96008,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(c_Complex_Oii))),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),
inference(forward_demodulation,[],[f95981,f3479]) ).
fof(f96019,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),
inference(forward_demodulation,[],[f96008,f54276]) ).
fof(f96485,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))
| c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)) ),
inference(resolution,[],[f96019,f2747]) ).
fof(f96503,plain,
c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),
inference(forward_subsumption_resolution,[],[f96485,f84488]) ).
fof(f96530,plain,
c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(superposition,[],[f3478,f96503]) ).
fof(f96536,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))))),
inference(superposition,[],[f4771,f96503]) ).
fof(f96549,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))))))),
inference(forward_demodulation,[],[f96536,f27145]) ).
fof(f96554,plain,
c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(forward_demodulation,[],[f96530,f3479]) ).
fof(f96569,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))))),
inference(forward_demodulation,[],[f96549,f3482]) ).
fof(f96572,plain,
c_Complex_OIm(c_Complex_Oii) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(forward_demodulation,[],[f96554,f5179]) ).
fof(f96581,plain,
c_Complex_ORe(c_Complex_Oii) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))),
inference(forward_demodulation,[],[f96569,f5234]) ).
fof(f96589,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))),
inference(forward_demodulation,[],[f96581,f3479]) ).
fof(f96594,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),
inference(forward_demodulation,[],[f96589,f5179]) ).
fof(f96825,plain,
c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(superposition,[],[f3479,f96594]) ).
fof(f96829,plain,
c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(forward_demodulation,[],[f96825,f3478]) ).
fof(f96848,plain,
c_Complex_ORe(c_Complex_Oii) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),
inference(forward_demodulation,[],[f96829,f5189]) ).
fof(f97122,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_ORe(X0))),
inference(superposition,[],[f2855,f96572]) ).
fof(f97124,plain,
! [X0] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_OIm(X0))),
inference(superposition,[],[f2856,f96572]) ).
fof(f97170,plain,
! [X0] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))),X0)),
inference(forward_demodulation,[],[f97124,f54272]) ).
fof(f97172,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))),X0)),
inference(forward_demodulation,[],[f97122,f54066]) ).
fof(f97200,plain,
! [X0] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f97170,f96848]) ).
fof(f97202,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f97172,f96848]) ).
fof(f97221,plain,
! [X0] : c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_OIm(c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f97200,f4621]) ).
fof(f97223,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_OIm(c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f97202,f4621]) ).
fof(f97240,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f97221,f54324]) ).
fof(f97242,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f97223,f54113]) ).
fof(f97255,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)) = c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[],[f97240,f20083]) ).
fof(f97257,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[],[f97242,f20083]) ).
fof(f97267,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),X0))),
inference(forward_demodulation,[],[f97255,f20175]) ).
fof(f97269,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),X0))),
inference(forward_demodulation,[],[f97257,f20175]) ).
fof(f97275,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)))),
inference(forward_demodulation,[],[f97267,f27145]) ).
fof(f97276,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)))),
inference(forward_demodulation,[],[f97269,f27145]) ).
fof(f97280,plain,
! [X0] : c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_ORe(X0)),
inference(forward_demodulation,[],[f97275,f3482]) ).
fof(f97281,plain,
! [X0] : c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)),
inference(forward_demodulation,[],[f97276,f3482]) ).
fof(f97284,plain,
! [X0] : c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)),
inference(forward_demodulation,[],[f97280,f54056]) ).
fof(f97285,plain,
! [X0] : c_Complex_OIm(X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)),
inference(forward_demodulation,[],[f97281,f5179]) ).
fof(f97288,plain,
! [X0] : c_Complex_ORe(X0) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)),
inference(forward_demodulation,[],[f97284,f5179]) ).
fof(f97304,plain,
! [X0] : c_Complex_ORe(X0) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(superposition,[],[f97288,f6200]) ).
fof(f97332,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0))),
inference(superposition,[],[f3479,f97288]) ).
fof(f97338,plain,
! [X0] : c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0))),
inference(forward_demodulation,[],[f97332,f3478]) ).
fof(f98598,plain,
! [X2,X3,X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X3),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X2)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1),c_Complex_Ocomplex_OComplex(X2,X3))),
inference(superposition,[],[f3158,f3245]) ).
fof(f98943,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))),
inference(superposition,[],[f3479,f97304]) ).
fof(f98949,plain,
! [X0] : c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))),
inference(forward_demodulation,[],[f98943,f3478]) ).
fof(f100645,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_OIm(X0)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Complex_ORe(X0))),
inference(superposition,[],[f2855,f96848]) ).
fof(f100669,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_ORe(c_Complex_Oii)),c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0)))),
inference(forward_demodulation,[],[f100645,f98598]) ).
fof(f100701,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_ORe(c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f100669,f3224]) ).
fof(f100728,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)))),X0)),
inference(forward_demodulation,[],[f100701,f4621]) ).
fof(f100751,plain,
! [X0] : c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii))),c_Complex_OIm(X0)),
inference(forward_demodulation,[],[f100728,f54113]) ).
fof(f100770,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii)),X0)),
inference(forward_demodulation,[],[f100751,f96572]) ).
fof(f100789,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))),
inference(forward_demodulation,[],[f100770,f20083]) ).
fof(f100802,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Oii),X0))),
inference(forward_demodulation,[],[f100789,f20175]) ).
fof(f100811,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0)))),
inference(forward_demodulation,[],[f100802,f27145]) ).
fof(f100818,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii),c_Complex_OIm(X0)) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0))),
inference(forward_demodulation,[],[f100811,f97338]) ).
fof(f100822,plain,
! [X0] : c_Complex_OIm(X0) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,X0))),
inference(forward_demodulation,[],[f100818,f97285]) ).
fof(f101120,plain,
! [X0] : c_Complex_OIm(X0) = c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))),
inference(superposition,[],[f100822,f6200]) ).
fof(f101935,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)),c_Complex_Ocomplex_OComplex(c_Complex_OIm(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)))))))),
inference(superposition,[],[f4631,f101120]) ).
fof(f101984,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_OIm(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))))))))),
inference(forward_demodulation,[],[f101935,f20083]) ).
fof(f102027,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii),c_Complex_Ocomplex_OComplex(c_Complex_OIm(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))))))))),
inference(forward_demodulation,[],[f101984,f20175]) ).
fof(f102058,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Complex_Oii,c_Complex_Ocomplex_OComplex(c_Complex_OIm(X0),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)))))))))),
inference(forward_demodulation,[],[f102027,f27145]) ).
fof(f102084,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))))),c_Complex_OIm(X0)))))),
inference(forward_demodulation,[],[f102058,f3359]) ).
fof(f102108,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))))),c_Complex_OIm(X0)))))),
inference(forward_demodulation,[],[f102084,f3479]) ).
fof(f102124,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))) = c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))),c_Complex_OIm(X0)))))),
inference(forward_demodulation,[],[f102108,f5179]) ).
fof(f102134,plain,
! [X0] : c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Complex_OIm(X0)))))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii))),
inference(forward_demodulation,[],[f102124,f98949]) ).
fof(f102140,plain,
! [X0] : c_NthRoot_Osqrt(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),c_Complex_OIm(X0)))))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(forward_demodulation,[],[f102134,f6376]) ).
fof(f102145,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X0,c_Complex_Oii)),
inference(forward_demodulation,[],[f102140,f26416]) ).
fof(f104198,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)),
inference(superposition,[],[f102145,f3461]) ).
fof(f104375,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),X0)),
inference(forward_demodulation,[],[f104198,f3443]) ).
fof(f104390,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),X0)),
inference(forward_demodulation,[],[f104375,f6365]) ).
fof(f106442,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y),c_Complex_Oii)),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))))),
inference(superposition,[],[f4875,f6365]) ).
fof(f106443,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y),c_Complex_Oii)),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f106442,f104390]) ).
fof(f106469,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f106443,f7298]) ).
fof(f106493,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_ORe(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Complex_OIm(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_x,v_y))))),
inference(forward_demodulation,[],[f106469,f3224]) ).
fof(f106513,plain,
$false,
inference(forward_subsumption_resolution,[],[f106493,f7261]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW203+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 13:18:01 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.50/1.95 % (1772342)Will run a generic schedule for satisfiability detection.
% 10.50/1.95 % (1772348)% WARNING: option uhcvi not known.
% 10.50/1.95 % (1772347)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=534360145_2999 on theBenchmark for (2999ds/0Mi)
% 10.50/1.95 % (1772348)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=670637861:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 10.50/1.95 % (1772350)dis+10_1_sil=32000:sp=arity:random_seed=2591971680:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 10.50/1.95 % (1772349)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=959820397:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 10.50/1.95 % (1772351)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1151758503:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 10.50/1.95 % (1772352)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2194497628:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 10.50/1.95 % (1772353)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2691010191:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 10.50/1.95 % (1772350)Instruction limit reached!
% 10.50/1.95 % (1772350)------------------------------
% 10.50/1.95 % (1772350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.50/1.95 % (1772350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.50/1.95 % (1772350)CaDiCaL version: 2.1.3
% 10.50/1.95 % (1772350)Termination reason: Instruction limit
% 10.50/1.95 % (1772350)Termination phase: Saturation
% 10.50/1.95 % (1772350)Time elapsed: 0.053 s
% 10.50/1.95 % (1772350)Peak memory usage: 14 MB
% 10.50/1.95 % (1772350)Instructions burned: 104 (million)
% 10.50/1.95 % (1772351)Instruction limit reached!
% 10.50/1.95 % (1772351)------------------------------
% 10.50/1.95 % (1772351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.50/1.95 % (1772351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.50/1.95 % (1772351)CaDiCaL version: 2.1.3
% 10.50/1.95 % (1772351)Termination reason: Instruction limit
% 10.50/1.95 % (1772351)Termination phase: Saturation
% 10.50/1.95 % (1772351)Time elapsed: 0.055 s
% 10.50/1.95 % (1772351)Peak memory usage: 14 MB
% 10.50/1.95 % (1772351)Instructions burned: 117 (million)
% 10.50/1.95 % (1772352)Instruction limit reached!
% 10.50/1.95 % (1772352)------------------------------
% 10.50/1.95 % (1772352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.50/1.95 % (1772352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.50/1.95 % (1772352)CaDiCaL version: 2.1.3
% 10.50/1.95 % (1772352)Termination reason: Instruction limit
% 10.50/1.95 % (1772352)Termination phase: Saturation
% 10.50/1.95 % (1772352)Time elapsed: 0.067 s
% 10.50/1.95 % (1772352)Peak memory usage: 14 MB
% 10.50/1.95 % (1772352)Instructions burned: 131 (million)
% 10.50/1.95 % (1772361)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=344289515:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 10.50/1.95 % (1772362)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1905380628:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 10.50/1.95 % (1772363)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1448824266:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 10.50/1.95 % (1772353)Instruction limit reached!
% 10.50/1.95 % (1772353)------------------------------
% 10.50/1.95 % (1772353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.50/1.95 % (1772353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.50/1.95 % (1772353)CaDiCaL version: 2.1.3
% 10.50/1.95 % (1772353)Termination reason: Instruction limit
% 10.50/1.95 % (1772353)Termination phase: Saturation
% 10.50/1.95 % (1772353)Time elapsed: 0.088 s
% 10.50/1.95 % (1772353)Peak memory usage: 15 MB
% 10.50/1.95 % (1772353)Instructions burned: 159 (million)
% 10.50/1.95 % (1772367)ott-21_1_sil=16000:fs=off:random_seed=1348028864:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 10.50/1.95 % (1772362)Instruction limit reached!
% 10.50/1.95 % (1772362)------------------------------
% 10.50/1.95 % (1772362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.50/1.95 % (1772362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.50/1.95 % (1772362)CaDiCaL version: 2.1.3
% 41.06/6.11 % (1772362)Termination reason: Instruction limit
% 41.06/6.11 % (1772362)Termination phase: Saturation
% 41.06/6.11 % (1772362)Time elapsed: 0.062 s
% 41.06/6.11 % (1772362)Peak memory usage: 14 MB
% 41.06/6.11 % (1772362)Instructions burned: 131 (million)
% 41.06/6.11 % (1772369)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3456188004:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 41.06/6.11 % (1772367)Instruction limit reached!
% 41.06/6.11 % (1772367)------------------------------
% 41.06/6.11 % (1772367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.06/6.11 % (1772367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.11 % (1772367)CaDiCaL version: 2.1.3
% 41.06/6.11 % (1772367)Termination reason: Instruction limit
% 41.06/6.11 % (1772367)Termination phase: Saturation
% 41.06/6.11 % (1772367)Time elapsed: 0.088 s
% 41.06/6.11 % (1772367)Peak memory usage: 14 MB
% 41.06/6.11 % (1772367)Instructions burned: 181 (million)
% 41.06/6.11 % (1772371)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=192536287:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.06/6.11 % (1772363)Instruction limit reached!
% 41.06/6.11 % (1772363)------------------------------
% 41.06/6.11 % (1772363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.06/6.11 % (1772363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.11 % (1772363)CaDiCaL version: 2.1.3
% 41.06/6.11 % (1772363)Termination reason: Instruction limit
% 41.06/6.11 % (1772363)Termination phase: Saturation
% 41.06/6.11 % (1772363)Time elapsed: 0.192 s
% 41.06/6.11 % (1772363)Peak memory usage: 18 MB
% 41.06/6.11 % (1772363)Instructions burned: 685 (million)
% 41.06/6.11 % (1772373)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1738781143:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 41.06/6.11 % TRYING [1]
% 41.06/6.11 % TRYING [2]
% 41.06/6.11 % TRYING [1]
% 41.06/6.11 % TRYING [2]
% 41.06/6.11 % (1772361)Instruction limit reached!
% 41.06/6.11 % (1772361)------------------------------
% 41.06/6.11 % (1772361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.06/6.11 % (1772361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.11 % (1772361)CaDiCaL version: 2.1.3
% 41.06/6.11 % (1772361)Termination reason: Instruction limit
% 41.06/6.11 % (1772361)Termination phase: Finite model building constraint generation
% 41.06/6.11 % (1772361)Time elapsed: 0.337 s
% 41.06/6.11 % (1772361)Peak memory usage: 23 MB
% 41.06/6.11 % (1772361)Instructions burned: 715 (million)
% 41.06/6.11 % (1772375)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=411313904:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.06/6.11 % (1772369)Instruction limit reached!
% 41.06/6.11 % (1772369)------------------------------
% 41.06/6.11 % (1772369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.06/6.11 % (1772369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.11 % (1772369)CaDiCaL version: 2.1.3
% 41.06/6.11 % (1772369)Termination reason: Instruction limit
% 41.06/6.11 % (1772369)Termination phase: Saturation
% 41.06/6.11 % (1772369)Time elapsed: 0.292 s
% 41.06/6.11 % (1772369)Peak memory usage: 16 MB
% 41.06/6.11 % (1772369)Instructions burned: 478 (million)
% 41.06/6.11 % (1772377)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1616430621:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 41.06/6.11 % TRYING [3]
% 41.06/6.11 % TRYING [1]
% 41.06/6.11 % TRYING [2]
% 41.06/6.11 % (1772371)Instruction limit reached!
% 41.06/6.11 % (1772371)------------------------------
% 41.06/6.11 % (1772371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.06/6.11 % (1772371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.06/6.11 % (1772371)CaDiCaL version: 2.1.3
% 41.06/6.11 % (1772371)Termination reason: Instruction limit
% 41.06/6.11 % (1772371)Termination phase: Finite model building constraint generation
% 41.06/6.11 % (1772371)Time elapsed: 0.403 s
% 41.06/6.11 % (1772371)Peak memory usage: 33 MB
% 41.06/6.11 % (1772371)Instructions burned: 867 (million)
% 41.06/6.11 % (1772379)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3484008114:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 41.06/6.11 % (1772373)Instruction limit reached!
% 41.06/6.11 % (1772373)------------------------------
% 41.06/6.11 % (1772373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.89/12.56 % (1772373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/12.56 % (1772373)CaDiCaL version: 2.1.3
% 86.89/12.56 % (1772373)Termination reason: Instruction limit
% 86.89/12.56 % (1772373)Termination phase: Saturation
% 86.89/12.56 % (1772373)Time elapsed: 0.386 s
% 86.89/12.56 % (1772373)Peak memory usage: 23 MB
% 86.89/12.56 % (1772373)Instructions burned: 1182 (million)
% 86.89/12.56 % (1772381)fmb+10_1_sil=64000:random_seed=2186585227:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 86.89/12.56 % (1772377)Instruction limit reached!
% 86.89/12.56 % (1772377)------------------------------
% 86.89/12.56 % (1772377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.89/12.56 % (1772377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/12.56 % (1772377)CaDiCaL version: 2.1.3
% 86.89/12.56 % (1772377)Termination reason: Instruction limit
% 86.89/12.56 % (1772377)Termination phase: Saturation
% 86.89/12.56 % (1772377)Time elapsed: 0.381 s
% 86.89/12.56 % (1772377)Peak memory usage: 20 MB
% 86.89/12.56 % (1772377)Instructions burned: 695 (million)
% 86.89/12.56 % TRYING [1]
% 86.89/12.56 % (1772375)Instruction limit reached!
% 86.89/12.56 % (1772375)------------------------------
% 86.89/12.56 % (1772375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.89/12.56 % (1772375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/12.56 % (1772375)CaDiCaL version: 2.1.3
% 86.89/12.56 % (1772375)Termination reason: Instruction limit
% 86.89/12.56 % (1772375)Termination phase: Finite model building constraint generation
% 86.89/12.56 % (1772375)Time elapsed: 0.434 s
% 86.89/12.56 % (1772375)Peak memory usage: 52 MB
% 86.89/12.56 % (1772375)Instructions burned: 891 (million)
% 86.89/12.56 % (1772383)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=266426708:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 86.89/12.56 % TRYING [2]
% 86.89/12.56 % (1772385)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3648876559:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 86.89/12.56 % (1772379)Instruction limit reached!
% 86.89/12.56 % (1772379)------------------------------
% 86.89/12.56 % (1772379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.89/12.56 % (1772379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/12.56 % (1772379)CaDiCaL version: 2.1.3
% 86.89/12.56 % (1772379)Termination reason: Instruction limit
% 86.89/12.56 % (1772379)Termination phase: Saturation
% 86.89/12.56 % (1772379)Time elapsed: 0.468 s
% 86.89/12.56 % (1772379)Peak memory usage: 21 MB
% 86.89/12.56 % (1772379)Instructions burned: 881 (million)
% 86.89/12.56 % (1772387)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3933054566:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 86.89/12.56 % (1772383)Cannot represent all propositional literals internally
% 86.89/12.56 % (1772383)Refutation not found, incomplete strategy
% 86.89/12.56 % (1772383)------------------------------
% 86.89/12.56 % (1772383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.89/12.56 % (1772383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/12.56 % (1772383)CaDiCaL version: 2.1.3
% 86.89/12.56 % (1772383)Termination reason: Refutation not found, incomplete strategy
% 86.89/12.56 % (1772383)Time elapsed: 0.319 s
% 86.89/12.56 % (1772383)Peak memory usage: 23 MB
% 86.89/12.56 % (1772383)Instructions burned: 664 (million)
% 86.89/12.56 % (1772383)------------------------------
% 86.89/12.56 % (1772383)------------------------------
% 86.89/12.56 % (1772389)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=791544761:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 86.89/12.56 % TRYING [8]
% 86.89/12.56 % TRYING [3]
% 86.89/12.56 % (1772385)Instruction limit reached!
% 86.89/12.56 % (1772385)------------------------------
% 86.89/12.56 % (1772385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.89/12.56 % (1772385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/12.56 % (1772385)CaDiCaL version: 2.1.3
% 86.89/12.56 % (1772385)Termination reason: Instruction limit
% 86.89/12.56 % (1772385)Termination phase: Finite model building constraint generation
% 86.89/12.56 % (1772385)Time elapsed: 0.413 s
% 86.89/12.56 % (1772385)Peak memory usage: 40 MB
% 86.89/12.56 % (1772385)Instructions burned: 923 (million)
% 86.89/12.56 % (1772391)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=744912275:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 86.89/12.56 % TRYING [4]
% 86.89/12.56 % (1772391)Cannot represent all propositional literals internally
% 145.72/27.83 % (1772391)Refutation not found, incomplete strategy
% 145.72/27.83 % (1772391)------------------------------
% 145.72/27.83 % (1772391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772391)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772391)Termination reason: Refutation not found, incomplete strategy
% 145.72/27.83 % (1772391)Time elapsed: 0.339 s
% 145.72/27.83 % (1772391)Peak memory usage: 23 MB
% 145.72/27.83 % (1772391)Instructions burned: 692 (million)
% 145.72/27.83 % (1772391)------------------------------
% 145.72/27.83 % (1772391)------------------------------
% 145.72/27.83 % (1772393)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4057498000:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 145.72/27.83 % (1772389)Instruction limit reached!
% 145.72/27.83 % (1772389)------------------------------
% 145.72/27.83 % (1772389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772389)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772389)Termination reason: Instruction limit
% 145.72/27.83 % (1772389)Termination phase: Saturation
% 145.72/27.83 % (1772389)Time elapsed: 0.759 s
% 145.72/27.83 % (1772389)Peak memory usage: 28 MB
% 145.72/27.83 % (1772389)Instructions burned: 1473 (million)
% 145.72/27.83 % (1772395)ott-2_1_sil=16000:newcnf=on:random_seed=3726191757:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 145.72/27.83 % (1772395)Instruction limit reached!
% 145.72/27.83 % (1772395)------------------------------
% 145.72/27.83 % (1772395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772395)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772395)Termination reason: Instruction limit
% 145.72/27.83 % (1772395)Termination phase: Saturation
% 145.72/27.83 % (1772395)Time elapsed: 0.467 s
% 145.72/27.83 % (1772395)Peak memory usage: 18 MB
% 145.72/27.83 % (1772395)Instructions burned: 870 (million)
% 145.72/27.83 % (1772397)ott+10_1_sil=32000:tgt=ground:random_seed=2600073333:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 145.72/27.83 % (1772393)Instruction limit reached!
% 145.72/27.83 % (1772393)------------------------------
% 145.72/27.83 % (1772393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772393)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772393)Termination reason: Instruction limit
% 145.72/27.83 % (1772393)Termination phase: Finite model building preprocessing
% 145.72/27.83 % (1772393)Time elapsed: 1.071 s
% 145.72/27.83 % (1772393)Peak memory usage: 35 MB
% 145.72/27.83 % (1772393)Instructions burned: 2174 (million)
% 145.72/27.83 % (1772399)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3445693369:i=54282_2971 on theBenchmark for (2971ds/54282Mi)
% 145.72/27.83 % TRYING [1]
% 145.72/27.83 % TRYING [2]
% 145.72/27.83 % TRYING [3]
% 145.72/27.83 % TRYING [4]
% 145.72/27.83 % (1772387)Instruction limit reached!
% 145.72/27.83 % (1772387)------------------------------
% 145.72/27.83 % (1772387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772387)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772387)Termination reason: Instruction limit
% 145.72/27.83 % (1772387)Termination phase: Saturation
% 145.72/27.83 % (1772387)Time elapsed: 2.927 s
% 145.72/27.83 % (1772387)Peak memory usage: 40 MB
% 145.72/27.83 % (1772387)Instructions burned: 5131 (million)
% 145.72/27.83 % (1772401)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1074590122:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi)
% 145.72/27.83 % TRYING [4]
% 145.72/27.83 % (1772397)Instruction limit reached!
% 145.72/27.83 % (1772397)------------------------------
% 145.72/27.83 % (1772397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772397)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772397)Termination reason: Instruction limit
% 145.72/27.83 % (1772397)Termination phase: Saturation
% 145.72/27.83 % (1772397)Time elapsed: 3.316 s
% 145.72/27.83 % (1772397)Peak memory usage: 41 MB
% 145.72/27.83 % (1772397)Instructions burned: 5114 (million)
% 145.72/27.83 % (1772403)dis+21_1_sil=32000:sas=cadical:random_seed=1919393082:i=3773:amm=off_2941 on theBenchmark for (2941ds/3773Mi)
% 145.72/27.83 % TRYING [5]
% 145.72/27.83 % (1772401)Instruction limit reached!
% 145.72/27.83 % (1772401)------------------------------
% 145.72/27.83 % (1772401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772401)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772401)Termination reason: Instruction limit
% 145.72/27.83 % (1772401)Termination phase: Saturation
% 145.72/27.83 % (1772401)Time elapsed: 1.868 s
% 145.72/27.83 % (1772401)Peak memory usage: 35 MB
% 145.72/27.83 % (1772401)Instructions burned: 3513 (million)
% 145.72/27.83 % (1772405)ott+11_1_sil=16000:gs=on:random_seed=2675287403:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2939 on theBenchmark for (2939ds/2251Mi)
% 145.72/27.83 % (1772381)Instruction limit reached!
% 145.72/27.83 % (1772381)------------------------------
% 145.72/27.83 % (1772381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772381)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772381)Termination reason: Instruction limit
% 145.72/27.83 % (1772381)Termination phase: Finite model building SAT solving
% 145.72/27.83 % (1772381)Time elapsed: 5.400 s
% 145.72/27.83 % (1772381)Peak memory usage: 564 MB
% 145.72/27.83 % (1772381)Instructions burned: 22069 (million)
% 145.72/27.83 % (1772407)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1135342677:fmbsr=1.6:i=67534_2938 on theBenchmark for (2938ds/67534Mi)
% 145.72/27.83 % (1772405)Instruction limit reached!
% 145.72/27.83 % (1772405)------------------------------
% 145.72/27.83 % (1772405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772405)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772405)Termination reason: Instruction limit
% 145.72/27.83 % (1772405)Termination phase: Saturation
% 145.72/27.83 % (1772405)Time elapsed: 1.447 s
% 145.72/27.83 % (1772405)Peak memory usage: 35 MB
% 145.72/27.83 % (1772405)Instructions burned: 2252 (million)
% 145.72/27.83 % (1772409)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1963426134:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi)
% 145.72/27.83 % (1772403)Instruction limit reached!
% 145.72/27.83 % (1772403)------------------------------
% 145.72/27.83 % (1772403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772403)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772403)Termination reason: Instruction limit
% 145.72/27.83 % (1772403)Termination phase: Saturation
% 145.72/27.83 % (1772403)Time elapsed: 2.212 s
% 145.72/27.83 % (1772403)Peak memory usage: 42 MB
% 145.72/27.83 % (1772403)Instructions burned: 3774 (million)
% 145.72/27.83 % (1772411)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2488871871:i=29340_2918 on theBenchmark for (2918ds/29340Mi)
% 145.72/27.83 % TRYING [7]
% 145.72/27.83 % TRYING [5]
% 145.72/27.83 % (1772409)Instruction limit reached!
% 145.72/27.83 % (1772409)------------------------------
% 145.72/27.83 % (1772409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772409)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772409)Termination reason: Instruction limit
% 145.72/27.83 % (1772409)Termination phase: Saturation
% 145.72/27.83 % (1772409)Time elapsed: 2.140 s
% 145.72/27.83 % (1772409)Peak memory usage: 50 MB
% 145.72/27.83 % (1772409)Instructions burned: 4593 (million)
% 145.72/27.83 % (1772413)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2010067968:i=5211_2903 on theBenchmark for (2903ds/5211Mi)
% 145.72/27.83 % (1772413)Instruction limit reached!
% 145.72/27.83 % (1772413)------------------------------
% 145.72/27.83 % (1772413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772413)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772413)Termination reason: Instruction limit
% 145.72/27.83 % (1772413)Termination phase: Saturation
% 145.72/27.83 % (1772413)Time elapsed: 2.635 s
% 145.72/27.83 % (1772413)Peak memory usage: 48 MB
% 145.72/27.83 % (1772413)Instructions burned: 5211 (million)
% 145.72/27.83 % (1772415)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1797597760:i=5497:nm=2_2876 on theBenchmark for (2876ds/5497Mi)
% 145.72/27.83 % (1772415)Cannot represent all propositional literals internally
% 145.72/27.83 % (1772415)Refutation not found, incomplete strategy
% 145.72/27.83 % (1772415)------------------------------
% 145.72/27.83 % (1772415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772415)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772415)Termination reason: Refutation not found, incomplete strategy
% 145.72/27.83 % (1772415)Time elapsed: 0.334 s
% 145.72/27.83 % (1772415)Peak memory usage: 23 MB
% 145.72/27.83 % (1772415)Instructions burned: 680 (million)
% 145.72/27.83 % (1772415)------------------------------
% 145.72/27.83 % (1772415)------------------------------
% 145.72/27.83 % (1772417)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1310474554:fmbsr=2:i=46332_2873 on theBenchmark for (2873ds/46332Mi)
% 145.72/27.83 % TRYING [15]
% 145.72/27.83 % (1772407)Instruction limit reached!
% 145.72/27.83 % (1772407)------------------------------
% 145.72/27.83 % (1772407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772407)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772407)Termination reason: Instruction limit
% 145.72/27.83 % (1772407)Termination phase: Finite model building constraint generation
% 145.72/27.83 % (1772407)Time elapsed: 12.560 s
% 145.72/27.83 % (1772407)Peak memory usage: 3679 MB
% 145.72/27.83 % (1772407)Instructions burned: 67539 (million)
% 145.72/27.83 % (1772419)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2487472347:i=14071_2809 on theBenchmark for (2809ds/14071Mi)
% 145.72/27.83 % TRYING [12]
% 145.72/27.83 % TRYING [6]
% 145.72/27.83 % (1772419)Instruction limit reached!
% 145.72/27.83 % (1772419)------------------------------
% 145.72/27.83 % (1772419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772419)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772419)Termination reason: Instruction limit
% 145.72/27.83 % (1772419)Termination phase: Finite model building constraint generation
% 145.72/27.83 % (1772419)Time elapsed: 2.685 s
% 145.72/27.83 % (1772419)Peak memory usage: 823 MB
% 145.72/27.83 % (1772419)Instructions burned: 14078 (million)
% 145.72/27.83 % (1772421)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=363268332:i=22565:add=on:rawr=on_2781 on theBenchmark for (2781ds/22565Mi)
% 145.72/27.83 % (1772411)Instruction limit reached!
% 145.72/27.83 % (1772411)------------------------------
% 145.72/27.83 % (1772411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772411)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772411)Termination reason: Instruction limit
% 145.72/27.83 % (1772411)Termination phase: Saturation
% 145.72/27.83 % (1772411)Time elapsed: 14.577 s
% 145.72/27.83 % (1772411)Peak memory usage: 104 MB
% 145.72/27.83 % (1772411)Instructions burned: 29342 (million)
% 145.72/27.83 % (1772425)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=602018706:i=8173:av=off_2772 on theBenchmark for (2772ds/8173Mi)
% 145.72/27.83 % (1772399)Instruction limit reached!
% 145.72/27.83 % (1772399)------------------------------
% 145.72/27.83 % (1772399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.83 % (1772399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.83 % (1772399)CaDiCaL version: 2.1.3
% 145.72/27.83 % (1772399)Termination reason: Instruction limit
% 145.72/27.83 % (1772399)Termination phase: Finite model building constraint generation
% 145.72/27.83 % (1772399)Time elapsed: 20.994 s
% 145.72/27.83 % (1772399)Peak memory usage: 2200 MB
% 145.72/27.83 % (1772399)Instructions burned: 54282 (million)
% 145.72/27.83 % (1772427)dis+10_16:1_sil=16000:random_seed=2576287269:i=9155:fsr=off_2758 on theBenchmark for (2758ds/9155Mi)
% 145.72/27.83 % (1772425) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1772342-1772425"...
% 145.72/27.83 % (1772425)...printing done.
% 145.72/27.83 % (1772425)Refutation found. Thanks to Tanya!
% 145.72/27.83 % SZS status Theorem for theBenchmark
% 145.72/27.83 % SZS output start Proof for theBenchmark
% See solution above
% 145.72/27.84 % (1772425)------------------------------
% 145.72/27.84 % (1772425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.72/27.84 % (1772425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.72/27.84 % (1772425)CaDiCaL version: 2.1.3
% 145.72/27.84 % (1772425)Termination reason: Refutation
% 145.72/27.84 % (1772425)Time elapsed: 4.479 s
% 145.72/27.84 % (1772425)Peak memory usage: 54 MB
% 145.72/27.84 % (1772425)Instructions burned: 7285 (million)
% 145.72/27.84 % (1772342)Success in time 27.604 s
% 145.72/27.84 % Vampire exiting
%------------------------------------------------------------------------------