%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG337-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:50:02 AM UTC 2026
% Result : Unsatisfiable 47.83s 7.36s
% Output : CNFRefutation 47.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 21
% Syntax : Number of formulae : 91 ( 74 unt; 0 def)
% Number of atoms : 108 ( 80 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 50 ( 33 ~; 17 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 121 ( 0 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_class__semiring_Osemiring__rules_I21_J_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(VAR_1,VAR_2,VAR_0),VAR_3,VAR_0) = c_HOL_Oplus__class_Oplus(VAR_1,c_HOL_Oplus__class_Oplus(VAR_2,VAR_3,VAR_0),VAR_0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(VAR_0) ),
file('theBenchmark.p',cls_class__semiring_Osemiring__rules_I21_J_0) ).
cnf(c_28,plain,
( c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(B,C,A),D,A) = c_HOL_Oplus__class_Oplus(B,c_HOL_Oplus__class_Oplus(C,D,A),A)
| ~ class_Ring__and__Field_Ocomm__semiring__1(A) ),
inference(clausify,[status(thm)],[cls_class__semiring_Osemiring__rules_I21_J_0]) ).
fof(cls_class__semiring_Osemiring__rules_I24_J_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_HOL_Oplus__class_Oplus(VAR_1,VAR_2,VAR_0) = c_HOL_Oplus__class_Oplus(VAR_2,VAR_1,VAR_0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(VAR_0) ),
file('theBenchmark.p',cls_class__semiring_Osemiring__rules_I24_J_0) ).
cnf(c_47,plain,
( c_HOL_Oplus__class_Oplus(B,C,A) = c_HOL_Oplus__class_Oplus(C,B,A)
| ~ class_Ring__and__Field_Ocomm__semiring__1(A) ),
inference(clausify,[status(thm)],[cls_class__semiring_Osemiring__rules_I24_J_0]) ).
fof(clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1) ).
cnf(c_79,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1]) ).
fof(clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add) ).
cnf(c_232,plain,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add]) ).
fof(cls_diff__add__cancel_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(VAR_1,VAR_2,VAR_0),VAR_2,VAR_0) = VAR_1
| ~ class_OrderedGroup_Ogroup__add(VAR_0) ),
file('theBenchmark.p',cls_diff__add__cancel_0) ).
cnf(c_233,plain,
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(B,C,A),C,A) = B
| ~ class_OrderedGroup_Ogroup__add(A) ),
inference(clausify,[status(thm)],[cls_diff__add__cancel_0]) ).
fof(cls_diff__minus__eq__add_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_HOL_Ominus__class_Ominus(VAR_1,c_HOL_Ouminus__class_Ouminus(VAR_2,VAR_0),VAR_0) = c_HOL_Oplus__class_Oplus(VAR_1,VAR_2,VAR_0)
| ~ class_OrderedGroup_Ogroup__add(VAR_0) ),
file('theBenchmark.p',cls_diff__minus__eq__add_0) ).
cnf(c_238,plain,
( c_HOL_Ominus__class_Ominus(B,c_HOL_Ouminus__class_Ouminus(C,A),A) = c_HOL_Oplus__class_Oplus(B,C,A)
| ~ class_OrderedGroup_Ogroup__add(A) ),
inference(clausify,[status(thm)],[cls_diff__minus__eq__add_0]) ).
fof(cls_zadd__assoc_0,axiom,
! [VAR_0,VAR_1,VAR_2] : c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(VAR_0,VAR_1,tc_Int_Oint),VAR_2,tc_Int_Oint) = c_HOL_Oplus__class_Oplus(VAR_0,c_HOL_Oplus__class_Oplus(VAR_1,VAR_2,tc_Int_Oint),tc_Int_Oint),
file('theBenchmark.p',cls_zadd__assoc_0) ).
cnf(c_666,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(A,B,tc_Int_Oint),C,tc_Int_Oint) = c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(B,C,tc_Int_Oint),tc_Int_Oint),
inference(clausify,[status(thm)],[cls_zadd__assoc_0]) ).
fof(cls_minus__diff__eq_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(VAR_1,VAR_2,VAR_0),VAR_0) = c_HOL_Ominus__class_Ominus(VAR_2,VAR_1,VAR_0)
| ~ class_OrderedGroup_Oab__group__add(VAR_0) ),
file('theBenchmark.p',cls_minus__diff__eq_0) ).
cnf(c_1116,plain,
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(B,C,A),A) = c_HOL_Ominus__class_Ominus(C,B,A)
| ~ class_OrderedGroup_Oab__group__add(A) ),
inference(clausify,[status(thm)],[cls_minus__diff__eq_0]) ).
fof(cls_Bit0__def_0,axiom,
! [VAR_0] : c_Int_OBit0(VAR_0) = c_HOL_Oplus__class_Oplus(VAR_0,VAR_0,tc_Int_Oint),
file('theBenchmark.p',cls_Bit0__def_0) ).
cnf(c_1118,plain,
c_Int_OBit0(A) = c_HOL_Oplus__class_Oplus(A,A,tc_Int_Oint),
inference(clausify,[status(thm)],[cls_Bit0__def_0]) ).
fof(cls_real__divide__def_0,axiom,
! [VAR_0,VAR_1] : c_HOL_Oinverse__class_Odivide(VAR_0,VAR_1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(VAR_0,c_HOL_Oinverse__class_Oinverse(VAR_1,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('theBenchmark.p',cls_real__divide__def_0) ).
cnf(c_1280,plain,
c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(A,c_HOL_Oinverse__class_Oinverse(B,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(clausify,[status(thm)],[cls_real__divide__def_0]) ).
cnf(c_1281,plain,
c_HOL_Otimes__class_Otimes(A,c_HOL_Oinverse__class_Oinverse(B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal),
inference(copy,[status(thm)],[c_1280]) ).
fof(cls_real__diff__def_0,axiom,
! [VAR_0,VAR_1] : c_HOL_Ominus__class_Ominus(VAR_0,VAR_1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(VAR_0,c_HOL_Ouminus__class_Ouminus(VAR_1,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('theBenchmark.p',cls_real__diff__def_0) ).
cnf(c_1287,plain,
c_HOL_Ominus__class_Ominus(A,B,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(A,c_HOL_Ouminus__class_Ouminus(B,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(clausify,[status(thm)],[cls_real__diff__def_0]) ).
cnf(c_1288,plain,
c_HOL_Oplus__class_Oplus(A,c_HOL_Ouminus__class_Ouminus(B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(A,B,tc_RealDef_Oreal),
inference(copy,[status(thm)],[c_1287]) ).
fof(cls_one__add__one__is__two_0,axiom,
! [VAR_0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(VAR_0),c_HOL_Oone__class_Oone(VAR_0),VAR_0) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),VAR_0)
| ~ class_Int_Onumber__ring(VAR_0) ),
file('theBenchmark.p',cls_one__add__one__is__two_0) ).
cnf(c_1384,plain,
( c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(A),c_HOL_Oone__class_Oone(A),A) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),A)
| ~ class_Int_Onumber__ring(A) ),
inference(clausify,[status(thm)],[cls_one__add__one__is__two_0]) ).
cnf(c_10602,plain,
( c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(A),c_HOL_Oone__class_Oone(A),A) = c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),A)
| ~ class_Int_Onumber__ring(A) ),
inference(paramod,[status(thm)],[c_1118,c_1384]) ).
cnf(c_1385,plain,
( c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),A) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(A),c_HOL_Oone__class_Oone(A),A)
| ~ class_Int_Onumber__ring(A) ),
inference(copy,[status(thm)],[c_10602]) ).
fof(cls_real__sum__of__halves_0,axiom,
! [VAR_0] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(VAR_0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(VAR_0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = VAR_0,
file('theBenchmark.p',cls_real__sum__of__halves_0) ).
cnf(c_1436,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(A,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(A,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = A,
inference(clausify,[status(thm)],[cls_real__sum__of__halves_0]) ).
cnf(c_10603,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(A,c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(A,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = A,
inference(paramod,[status(thm)],[c_1118,c_1436]) ).
cnf(c_1437,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(A,c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(A,c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = A,
inference(paramod,[status(thm)],[c_1118,c_10603]) ).
fof(cls_real__add__mult__distrib_0,axiom,
! [VAR_0,VAR_1,VAR_2] : c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(VAR_0,VAR_1,tc_RealDef_Oreal),VAR_2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(VAR_0,VAR_2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(VAR_1,VAR_2,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('theBenchmark.p',cls_real__add__mult__distrib_0) ).
cnf(c_1445,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal),C,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,C,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(B,C,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(clausify,[status(thm)],[cls_real__add__mult__distrib_0]) ).
cnf(c_1446,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,B,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(C,B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(A,C,tc_RealDef_Oreal),B,tc_RealDef_Oreal),
inference(copy,[status(thm)],[c_1445]) ).
fof(cls_divide_Odiff_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(VAR_1,VAR_2,VAR_0),VAR_3,VAR_0) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(VAR_1,VAR_3,VAR_0),c_HOL_Oinverse__class_Odivide(VAR_2,VAR_3,VAR_0),VAR_0)
| ~ class_RealVector_Oreal__normed__field(VAR_0) ),
file('theBenchmark.p',cls_divide_Odiff_0) ).
cnf(c_1464,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(B,C,A),D,A) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(B,D,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)
| ~ class_RealVector_Oreal__normed__field(A) ),
inference(clausify,[status(thm)],[cls_divide_Odiff_0]) ).
cnf(c_1465,plain,
( c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(B,C,A),c_HOL_Oinverse__class_Odivide(D,C,A),A) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(B,D,A),C,A)
| ~ class_RealVector_Oreal__normed__field(A) ),
inference(copy,[status(thm)],[c_1464]) ).
fof(cls_CHAINED_0,axiom,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('theBenchmark.p',cls_CHAINED_0) ).
cnf(c_1505,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(clausify,[status(thm)],[cls_CHAINED_0]) ).
cnf(c_10604,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1118,c_1505]) ).
cnf(c_10605,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1118,c_10604]) ).
cnf(c_10606,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_666,c_10605]) ).
cnf(c_1506,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1118,c_10606]) ).
fof(cls_CHAINED_0_01,axiom,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('theBenchmark.p',cls_CHAINED_0_01) ).
cnf(c_1507,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(clausify,[status(thm)],[cls_CHAINED_0_01]) ).
cnf(c_10607,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1118,c_1507]) ).
cnf(c_10608,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1118,c_10607]) ).
cnf(c_10609,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_666,c_10608]) ).
cnf(c_1508,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1118,c_10609]) ).
fof(cls_conjecture_0,axiom,
c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_1509,plain,
c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
cnf(c_10610,plain,
c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1118,c_1509]) ).
cnf(c_10611,plain,
c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1118,c_10610]) ).
cnf(c_10612,plain,
c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_666,c_10611]) ).
cnf(c_10613,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1508,c_10612]) ).
cnf(c_10614,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1118,c_10613]) ).
cnf(c_10615,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1118,c_10614]) ).
cnf(c_10616,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_666,c_10615]) ).
cnf(c_1510,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1506,c_10616]) ).
fof(clsarity_RealDef__Oreal__RealVector_Oreal__normed__field,axiom,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
file('theBenchmark.p',clsarity_RealDef__Oreal__RealVector_Oreal__normed__field) ).
cnf(c_1615,plain,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[clsarity_RealDef__Oreal__RealVector_Oreal__normed__field]) ).
fof(clsarity_RealDef__Oreal__OrderedGroup_Oab__group__add,axiom,
class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal),
file('theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Oab__group__add) ).
cnf(c_1623,plain,
class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[clsarity_RealDef__Oreal__OrderedGroup_Oab__group__add]) ).
fof(clsarity_RealDef__Oreal__Int_Onumber__ring,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('theBenchmark.p',clsarity_RealDef__Oreal__Int_Onumber__ring) ).
cnf(c_1640,plain,
class_Int_Onumber__ring(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[clsarity_RealDef__Oreal__Int_Onumber__ring]) ).
cnf(c_1763,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal),C,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(B,C,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_79,c_28]) ).
cnf(c_1784,plain,
c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(B,A,tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_79,c_47]) ).
cnf(c_2518,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(A,B,tc_RealDef_Oreal),B,tc_RealDef_Oreal) = A,
inference(resolve,[status(thm)],[c_233,c_232]) ).
cnf(c_2519,plain,
c_HOL_Oplus__class_Oplus(A,c_HOL_Ominus__class_Ominus(B,A,tc_RealDef_Oreal),tc_RealDef_Oreal) = B,
inference(paramod,[status(thm)],[c_1784,c_2518]) ).
cnf(c_2528,plain,
c_HOL_Ominus__class_Ominus(A,c_HOL_Ouminus__class_Ouminus(B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_238,c_232]) ).
cnf(c_2785,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_1784,c_1510]) ).
cnf(c_10617,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(C,c_HOL_Oinverse__class_Oinverse(B,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(A,C,tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(B,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1281,c_1446]) ).
cnf(c_10618,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(C,B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(A,C,tc_RealDef_Oreal),c_HOL_Oinverse__class_Oinverse(B,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1281,c_10617]) ).
cnf(c_4610,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(C,B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(A,C,tc_RealDef_Oreal),B,tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1281,c_10618]) ).
cnf(c_4621,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(A,A,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = A,
inference(paramod,[status(thm)],[c_4610,c_1437]) ).
cnf(c_5259,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(C,B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(A,C,tc_RealDef_Oreal),B,tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_1615,c_1465]) ).
cnf(c_5263,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_5259,c_2785]) ).
cnf(c_5283,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(A,B,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(B,A,tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_1623,c_1116]) ).
cnf(c_5334,plain,
c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_1640,c_1385]) ).
cnf(c_5361,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_5334,c_5263]) ).
cnf(c_5408,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(A,A,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = A,
inference(paramod,[status(thm)],[c_5334,c_4621]) ).
cnf(c_10619,plain,
c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(B,c_HOL_Ouminus__class_Ouminus(C,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal),C,tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1763,c_1288]) ).
cnf(c_10620,plain,
c_HOL_Oplus__class_Oplus(A,c_HOL_Ominus__class_Ominus(B,C,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal),C,tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_1288,c_10619]) ).
cnf(c_6441,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(A,B,tc_RealDef_Oreal),C,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(A,c_HOL_Ominus__class_Ominus(B,C,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(copy,[status(thm)],[c_10620]) ).
cnf(c_6445,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_6441,c_5361]) ).
cnf(c_10621,plain,
c_HOL_Ominus__class_Ominus(A,c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(B,A,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = B,
inference(paramod,[status(thm)],[c_2519,c_2528]) ).
cnf(c_10600,plain,
c_HOL_Ominus__class_Ominus(A,c_HOL_Ominus__class_Ominus(A,B,tc_RealDef_Oreal),tc_RealDef_Oreal) = B,
inference(paramod,[status(thm)],[c_5283,c_10621]) ).
cnf(c_10622,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) != v_x____,
inference(paramod,[status(thm)],[c_10600,c_6445]) ).
cnf(c_10623,plain,
v_x____ != v_x____,
inference(paramod,[status(thm)],[c_5408,c_10622]) ).
cnf(c_10601,plain,
$false,
inference(copy,[status(thm)],[c_10623]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG337-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n001.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sat Sep 26 21:58:59 UTC 2026
% 0.18/0.41 % CPUTime :
% 0.18/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.41 % Process 2755175 was started by sandbox on n001,
% 0.18/0.41 % Sat Sep 26 21:58:59 2026
% 0.18/0.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.49
% 0.18/0.49 % From the command line: assign(max_seconds, 300).
% 47.83/7.36
% 47.83/7.36 % given #500 (I,wt=51): 1315 -class_Ring__and__Field_Opordered__ring(A) | c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,C,A),D,A),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(E,C,A),F,A),A) | -c_lessequals(D,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(E,B,A),C,A),F,A),A) # tptp_name(cls_le__add__iff2_1) # clausal_fof(1). [assumption].
% 47.83/7.36
% 47.83/7.36 % given #1000 (I,wt=28): 2284 c_HOL_Oord__class_Oless(A,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),B,tc_RealDef_Oreal) | -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(B,A,tc_RealDef_Oreal),tc_RealDef_Oreal). [copy(2283),unit_del(a,1606)].
% 47.83/7.36
% 47.83/7.36 % SZS status Unsatisfiable for theBenchmark
% 47.83/7.36
% 47.83/7.36 % Proof 1 at 5.69 (+ 0.60) seconds.
% 47.83/7.36 % Length of proof is 48.
% 47.83/7.36 % Level of proof is 7.
% 47.83/7.36 % Maximum clause weight is 114.000.
% 47.83/7.36 % Given clauses 1129.
% 47.83/7.36
% 47.83/7.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------