%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW222+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.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 : Fri Sep 25 03:29:17 PM UTC 2026
% Result : Theorem 51.08s 7.92s
% Output : CNFRefutation 51.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 35
% Syntax : Number of formulae : 129 ( 85 unt; 13 def)
% Number of atoms : 241 ( 106 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 130 ( 60 ~; 53 |; 4 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 14 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-3 aty)
% Number of variables : 134 ( 0 sgn 134 !; 0 ?; 51 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_w) ).
fof(f5,axiom,
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))) )
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__0960_A_060_Acmod_A_Iw_A_N_Az_J_A_G_Acmod_A_Iw_A_N_Az_J_A_060_Ad_061_061_062_Acmod_A_Ipoly_Ap_Aw_A_N_Apoly_Ap_Az_J_A_060_Aabs_A_Icmod_A_Ipoly_Ap_Az_J_A_N_A_N_As_J_A_P_A2_096) ).
fof(f7,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_e2) ).
fof(f21,axiom,
! [X0,X1] :
( class_RealVector_Oreal__normed__vector(X1)
=> ( c_RealVector_Onorm__class_Onorm(X1,X0) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
<=> X0 = c_Groups_Ozero__class_Ozero(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__eq__zero) ).
fof(f35,axiom,
! [X0,X1] :
( class_RealVector_Oreal__normed__vector(X1)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0))
<=> X0 != c_Groups_Ozero__class_Ozero(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zero__less__norm__iff) ).
fof(f75,axiom,
! [X0,X1,X2] :
( class_RealVector_Oreal__normed__vector(X2)
=> c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)) = c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__minus__commute) ).
fof(f121,axiom,
! [X0,X1,X2] :
( class_Groups_Oab__group__add(X2)
=> ( X1 = X0
<=> c_Groups_Ominus__class_Ominus(X2,X1,X0) = c_Groups_Ozero__class_Ozero(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_eq__iff__diff__eq__0) ).
fof(f218,axiom,
! [X0,X1] :
( class_Groups_Omonoid__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__left) ).
fof(f231,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_diff__add__cancel) ).
fof(f307,axiom,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__real__def) ).
fof(f309,axiom,
! [X0,X1] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__minus__add__cancel) ).
fof(f437,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__assoc) ).
fof(f438,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__left__commute) ).
fof(f454,axiom,
! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit1__def) ).
fof(f458,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls) ).
fof(f459,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls__right) ).
fof(f460,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(f1162,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1177,axiom,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Oab__group__add) ).
fof(f1181,axiom,
class_Groups_Omonoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Omonoid__add) ).
fof(f1183,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ogroup__add) ).
fof(f1251,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1252,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(negated_conjecture,[status(cth)],[f1251]) ).
fof(f1255,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(flattening,[],[f1252]) ).
fof(f1257,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
inference(ennf_transformation,[],[f5]) ).
fof(f1258,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
inference(flattening,[],[f1257]) ).
fof(f1279,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| ( c_RealVector_Onorm__class_Onorm(X1,X0) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
<=> X0 = c_Groups_Ozero__class_Ozero(X1) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f1283,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0))
<=> X0 != c_Groups_Ozero__class_Ozero(X1) ) ),
inference(ennf_transformation,[],[f35]) ).
fof(f1319,plain,
! [X0,X1,X2] :
( ~ class_RealVector_Oreal__normed__vector(X2)
| c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)) = c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X0,X1)) ),
inference(ennf_transformation,[],[f75]) ).
fof(f1358,plain,
! [X0,X1,X2] :
( ~ class_Groups_Oab__group__add(X2)
| ( X1 = X0
<=> c_Groups_Ominus__class_Ominus(X2,X1,X0) = c_Groups_Ozero__class_Ozero(X2) ) ),
inference(ennf_transformation,[],[f121]) ).
fof(f1484,plain,
! [X0,X1] :
( ~ class_Groups_Omonoid__add(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0 ),
inference(ennf_transformation,[],[f218]) ).
fof(f1502,plain,
! [X0,X1,X2] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
inference(ennf_transformation,[],[f231]) ).
fof(f2235,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| ( ( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_RealVector_Onorm__class_Onorm(X1,X0)
| X0 = c_Groups_Ozero__class_Ozero(X1) )
& ( c_Groups_Ozero__class_Ozero(X1) != X0
| c_RealVector_Onorm__class_Onorm(X1,X0) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) ) ),
inference(nnf_transformation,[],[f1279]) ).
fof(f2240,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| ( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0))
| X0 != c_Groups_Ozero__class_Ozero(X1) )
& ( c_Groups_Ozero__class_Ozero(X1) = X0
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0)) ) ) ),
inference(nnf_transformation,[],[f1283]) ).
fof(f2272,plain,
! [X0,X1,X2] :
( ~ class_Groups_Oab__group__add(X2)
| ( ( X0 != X1
| c_Groups_Ominus__class_Ominus(X2,X1,X0) = c_Groups_Ozero__class_Ozero(X2) )
& ( c_Groups_Ozero__class_Ozero(X2) != c_Groups_Ominus__class_Ominus(X2,X1,X0)
| X1 = X0 ) ) ),
inference(nnf_transformation,[],[f1358]) ).
fof(f2659,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____),
inference(cnf_transformation,[],[f3]) ).
fof(f2661,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
inference(cnf_transformation,[],[f1258]) ).
fof(f2663,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(cnf_transformation,[],[f7]) ).
fof(f2682,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| c_Groups_Ozero__class_Ozero(X1) != X0
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(X1,X0) ),
inference(cnf_transformation,[],[f2235]) ).
fof(f2701,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| c_Groups_Ozero__class_Ozero(X1) = X0
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0)) ),
inference(cnf_transformation,[],[f2240]) ).
fof(f2759,plain,
! [X2,X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X2)
| c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)) = c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X0,X1)) ),
inference(cnf_transformation,[],[f1319]) ).
fof(f2825,plain,
! [X2,X0,X1] :
( ~ class_Groups_Oab__group__add(X2)
| X0 != X1
| c_Groups_Ozero__class_Ozero(X2) = c_Groups_Ominus__class_Ominus(X2,X1,X0) ),
inference(cnf_transformation,[],[f2272]) ).
fof(f2964,plain,
! [X0,X1] :
( ~ class_Groups_Omonoid__add(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0 ),
inference(cnf_transformation,[],[f1484]) ).
fof(f2980,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f1502]) ).
fof(f3091,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0),
inference(cnf_transformation,[],[f307]) ).
fof(f3093,plain,
! [X0,X1] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))),
inference(cnf_transformation,[],[f309]) ).
fof(f3261,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)),
inference(cnf_transformation,[],[f437]) ).
fof(f3262,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
inference(cnf_transformation,[],[f438]) ).
fof(f3282,plain,
! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
inference(cnf_transformation,[],[f454]) ).
fof(f3286,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
inference(cnf_transformation,[],[f458]) ).
fof(f3287,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
inference(cnf_transformation,[],[f459]) ).
fof(f3288,plain,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(cnf_transformation,[],[f460]) ).
fof(f4375,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1162]) ).
fof(f4390,plain,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1177]) ).
fof(f4394,plain,
class_Groups_Omonoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1181]) ).
fof(f4396,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1183]) ).
fof(f4464,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(cnf_transformation,[],[f1255]) ).
fof(f4465,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))) ),
inference(definition_unfolding,[],[f2661,f3288,f3282]) ).
fof(f4467,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(definition_unfolding,[],[f2663,f3288,f3282]) ).
fof(f4766,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(definition_unfolding,[],[f4464,f3288,f3282]) ).
fof(f4767,plain,
! [X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ozero__class_Ozero(X1)) ),
inference(equality_resolution,[],[f2682]) ).
fof(f4788,plain,
! [X2,X1] :
( ~ class_Groups_Oab__group__add(X2)
| c_Groups_Ozero__class_Ozero(X2) = c_Groups_Ominus__class_Ominus(X2,X1,X1) ),
inference(equality_resolution,[],[f2825]) ).
tcf(c_51,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____),
inference(cnf_transformation,[],[f2659]) ).
tcf(c_53,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))) ),
inference(cnf_transformation,[],[f4465]) ).
tcf(c_55,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(cnf_transformation,[],[f4467]) ).
tcf(c_73,plain,
! [X0: $i] :
( ( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) )
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[],[f4767]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,X1))
| ( c_Groups_Ozero__class_Ozero(X0) = X1 )
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[],[f2701]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)) = c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X2,X1)) )
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[],[f2759]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i] :
( ( c_Groups_Ominus__class_Ominus(X0,X1,X1) = c_Groups_Ozero__class_Ozero(X0) )
| ~ class_Groups_Oab__group__add(X0) ),
inference(cnf_transformation,[],[f4788]) ).
tcf(c_341,plain,
! [X0: $i,X1: $i] :
( ( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1) = X1 )
| ~ class_Groups_Omonoid__add(X0) ),
inference(cnf_transformation,[],[f2964]) ).
tcf(c_357,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2),X2) = X1 )
| ~ class_Groups_Ogroup__add(X0) ),
inference(cnf_transformation,[],[f2980]) ).
tcf(c_468,plain,
! [X0: $i,X1: $i] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),
inference(cnf_transformation,[],[f3091]) ).
tcf(c_470,plain,
! [X0: $i,X1: $i] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
inference(cnf_transformation,[],[f3093]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i,X2: $i] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X1),X2) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X2)),
inference(cnf_transformation,[],[f3261]) ).
tcf(c_638,plain,
! [X0: $i,X1: $i,X2: $i] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X2)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X2)),
inference(cnf_transformation,[],[f3262]) ).
tcf(c_659,plain,
! [X0: $i] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
inference(cnf_transformation,[],[f3286]) ).
tcf(c_660,plain,
! [X0: $i] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
inference(cnf_transformation,[],[f3287]) ).
tcf(c_1716,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f4375]) ).
tcf(c_1731,plain,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f4390]) ).
tcf(c_1735,plain,
class_Groups_Omonoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f4394]) ).
tcf(c_1737,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f4396]) ).
tcf(c_1805,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(cnf_transformation,[],[f4766]) ).
tcf(c_2789,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))),
inference(global_subsumption_just,[status(thm)],[c_53,c_51,c_1805,c_53]) ).
tcf(c_3107,plain,
! [X0: $i] :
( ( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) )
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(prop_impl_just,[status(thm)],[c_73]) ).
tcf(c_3113,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)) = c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X2,X1)) )
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(prop_impl_just,[status(thm)],[c_145]) ).
tcf(c_3467,plain,
! [X0: $i,X1: $i] :
( ( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1) = X1 )
| ~ class_Groups_Omonoid__add(X0) ),
inference(prop_impl_just,[status(thm)],[c_341]) ).
tcf(c_15646,plain,
! [X0: $i,X1: $i] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)),
inference(light_normalisation,[status(thm)],[c_470,c_468]) ).
tcf(c_15647,plain,
! [X0: $i,X1: $i] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)),
inference(light_normalisation,[status(thm)],[c_15646,c_468]) ).
tcf(c_19696,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
inference(demodulation,[status(thm)],[c_55,c_637,c_638,c_659,c_660,c_15647]) ).
tcf(c_19780,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
inference(demodulation,[status(thm)],[c_1805,c_637,c_638,c_659,c_660,c_15647]) ).
tcf(c_20485,plain,
! [X0: $i,X1: $i] :
( ( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1) = X1 )
| ( X0 != tc_Complex_Ocomplex ) ),
inference(resolution_lifted,[status(thm)],[c_3467,c_1735]) ).
tcf(c_20486,plain,
! [X0: $i] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0) = X0,
inference(unflattening,[status(thm)],[c_20485]) ).
tcf(c_25799,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)) = c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X2,X1)) )
| ( X0 != tc_Complex_Ocomplex ) ),
inference(resolution_lifted,[status(thm)],[c_3113,c_1716]) ).
tcf(c_25800,plain,
! [X0: $i,X1: $i] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0)),
inference(unflattening,[status(thm)],[c_25799]) ).
tcf(c_25816,plain,
! [X0: $i,X1: $i] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,X1))
| ( c_Groups_Ozero__class_Ozero(X0) = X1 )
| ( X0 != tc_Complex_Ocomplex ) ),
inference(resolution_lifted,[status(thm)],[c_92,c_1716]) ).
tcf(c_25817,plain,
! [X0: $i] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))
| ( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ) ),
inference(unflattening,[status(thm)],[c_25816]) ).
tcf(c_25834,plain,
! [X0: $i] :
( ( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) )
| ( X0 != tc_Complex_Ocomplex ) ),
inference(resolution_lifted,[status(thm)],[c_3107,c_1716]) ).
tcf(c_25835,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(unflattening,[status(thm)],[c_25834]) ).
tcf(c_50737,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____))),
inference(demodulation,[status(thm)],[c_2789,c_25800]) ).
tcf(c_54737,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
inference(demodulation,[status(thm)],[c_19780,c_25800]) ).
tcf(c_69145,plain,
! [X0: $i] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))
| ( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ) ),
inference(prop_impl_just,[status(thm)],[c_25817]) ).
tcf(c_94049,definition,
iPr_def_10 = c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_94050,definition,
iPr_def_11 = hAPP(iPr_def_10,v_z____),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_94051,definition,
iPr_def_12 = hAPP(iPr_def_10,v_wa____),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_94052,definition,
iPr_def_13 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,iPr_def_11,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_94053,definition,
iPr_def_14 = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_94054,definition,
iPr_def_15 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_94055,definition,
iPr_def_16 = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_94056,definition,
iPr_def_17 = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,iPr_def_15,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_94057,definition,
iPr_def_18 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_94058,definition,
iPr_def_19 = c_Groups_Oone__class_Oone(tc_Int_Oint),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_94059,definition,
iPr_def_20 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,iPr_def_19,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_94060,definition,
iPr_def_21 = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_94061,definition,
iPr_def_22 = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,iPr_def_18,iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_94062,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,iPr_def_14,iPr_def_22),
inference(demodulation,[status(thm)],[c_54737,c_94058,c_94059,c_94060,c_94055,c_94054,c_94056,c_94057,c_94061,c_94051,c_94049,c_94050,c_94052,c_94053]) ).
tcf(c_113534,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),iPr_def_22),
inference(light_normalisation,[status(thm)],[c_19696,c_94049,c_94050,c_94054,c_94055,c_94056,c_94057,c_94058,c_94059,c_94060,c_94061]) ).
tcf(c_114642,plain,
! [X0: $i] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(superposition,[status(thm)],[c_1731,c_207]) ).
tcf(c_117956,plain,
c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(superposition,[status(thm)],[c_69145,c_50737]) ).
tcf(c_118362,plain,
! [X0: $i,X1: $i] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1),X1) = X0,
inference(superposition,[status(thm)],[c_1737,c_357]) ).
tcf(c_120112,plain,
c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),v_wa____) = v_z____,
inference(superposition,[status(thm)],[c_117956,c_118362]) ).
tcf(c_120134,plain,
v_wa____ = v_z____,
inference(demodulation,[status(thm)],[c_120112,c_20486]) ).
tcf(c_120137,plain,
hAPP(iPr_def_10,v_z____) = iPr_def_12,
inference(demodulation,[status(thm)],[c_94051,c_120134]) ).
tcf(c_120138,plain,
iPr_def_11 = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_120137,c_94050]) ).
tcf(c_120143,plain,
c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,iPr_def_11,iPr_def_11) = iPr_def_13,
inference(demodulation,[status(thm)],[c_94052,c_120138]) ).
tcf(c_120308,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = iPr_def_13,
inference(demodulation,[status(thm)],[c_120143,c_114642]) ).
tcf(c_120325,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,iPr_def_13) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_25835,c_120308]) ).
tcf(c_120330,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_120325,c_94053]) ).
tcf(c_120448,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,iPr_def_14,iPr_def_22),
inference(demodulation,[status(thm)],[c_113534,c_120330]) ).
tcf(c_120450,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_120448,c_94062]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW222+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n013.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 21:46:36 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.42
% 0.14/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.42
% 0.14/0.42 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 51.08/7.92 % SZS status Started for theBenchmark.p
% 51.08/7.92 ERROR - "ProverProcess:heur/397442:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 51.08/7.92 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 51.08/7.92 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 64 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 4 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 8 --inst_learning_loop_flag true --inst_learning_start 2 --inst_lit_activity_flag false --inst_lit_sel "[-split]" --inst_lit_sel_side num_lit --inst_orphan_elimination false --inst_passive_queue_type priority_queues --inst_passive_queues "[[+conj_symb]]" --inst_passive_queues_freq "[50]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.8199321230744955 --inst_solver_per_active 4 --inst_sos_flag false --inst_start_prop_sim_after_learn 7 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out__tz46jz6/wlog94kn 2>> /export/starexec/sandbox/tmp/iprover_out__tz46jz6/wlog94kn_error
% 51.08/7.92 % SZS status Theorem for theBenchmark.p
% 51.08/7.92
% 51.08/7.92 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 51.08/7.92
% 51.08/7.92 % ------ iProver source info
% 51.08/7.92
% 51.08/7.92 % git: date: 2026-07-19 20:42:38 +0200
% 51.08/7.92 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 51.08/7.92 % git: non_committed_changes: false
% 51.08/7.92
% 51.08/7.92 % ------ Parsing...
% 51.08/7.92 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 51.08/7.92
% 51.08/7.92 % ------ Preprocessing... sup_sim: 223 sf_s rm: 17 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 99 sf_s rm: 21 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 21 0s sf_e pe_s pe_e %
% 51.08/7.92
% 51.08/7.92 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 51.08/7.92
% 51.08/7.92 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 51.08/7.92 % ------ Proving...
% 51.08/7.92 % ------ Problem Properties
% 51.08/7.92
% 51.08/7.92 %
% 51.08/7.92 % clauses 1332
% 51.08/7.92 % conjectures 0
% 51.08/7.92 % EPR 178
% 51.08/7.92 % Horn 1182
% 51.08/7.92 % unary 444
% 51.08/7.92 % binary 465
% 51.08/7.92 % lits 2840
% 51.08/7.92 % lits eq 692
% 51.08/7.92 % fd_pure 0
% 51.08/7.92 % fd_pseudo 0
% 51.08/7.92 % fd_cond 62
% 51.08/7.92 % fd_pseudo_cond 66
% 51.08/7.92 % AC symbols 0
% 51.08/7.92
% 51.08/7.92 % ------ Schedule dynamic 5 is on
% 51.08/7.92
% 51.08/7.92 % ------ no conjectures: strip conj schedule
% 51.08/7.92
% 51.08/7.92 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 51.08/7.92
% 51.08/7.92
% 51.08/7.92 % ------
% 51.08/7.92 % Current options:
% 51.08/7.92 % ------
% 51.08/7.92
% 51.08/7.92
% 51.08/7.92 %
% 51.08/7.92
% 51.08/7.92 % ------ Proving...
% 51.08/7.92 %
% 51.08/7.92
% 51.08/7.92 % SZS status Theorem for theBenchmark.p
% 51.08/7.92
% 51.08/7.92 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 51.08/7.92
% 51.08/7.92
%------------------------------------------------------------------------------