%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SWV634-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:39:43 EDT 2022
% Result : Unknown 0.58s 0.84s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV634-1 : TPTP v8.1.0. Released v4.1.0.
% 0.11/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 15 15:56:23 EDT 2022
% 0.18/0.33 % CPUTime :
% 0.18/0.52 ----- Otter 3.2, August 2001 -----
% 0.18/0.52 The process was started by sandbox2 on n009.cluster.edu,
% 0.18/0.52 Wed Jun 15 15:56:23 2022
% 0.18/0.52 The command was "./sos". The process ID is 4470.
% 0.18/0.52
% 0.18/0.52 set(prolog_style_variables).
% 0.18/0.52 set(auto).
% 0.18/0.52 dependent: set(auto1).
% 0.18/0.52 dependent: set(process_input).
% 0.18/0.52 dependent: clear(print_kept).
% 0.18/0.52 dependent: clear(print_new_demod).
% 0.18/0.52 dependent: clear(print_back_demod).
% 0.18/0.52 dependent: clear(print_back_sub).
% 0.18/0.52 dependent: set(control_memory).
% 0.18/0.52 dependent: assign(max_mem, 12000).
% 0.18/0.52 dependent: assign(pick_given_ratio, 4).
% 0.18/0.52 dependent: assign(stats_level, 1).
% 0.18/0.52 dependent: assign(pick_semantic_ratio, 3).
% 0.18/0.52 dependent: assign(sos_limit, 5000).
% 0.18/0.52 dependent: assign(max_weight, 60).
% 0.18/0.52 clear(print_given).
% 0.18/0.52
% 0.18/0.52 list(usable).
% 0.18/0.52
% 0.18/0.52 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=7.
% 0.18/0.52
% 0.18/0.52 This ia a non-Horn set with equality. The strategy will be
% 0.18/0.52 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.18/0.52 unit deletion, with positive clauses in sos and nonpositive
% 0.18/0.52 clauses in usable.
% 0.18/0.52
% 0.18/0.52 dependent: set(knuth_bendix).
% 0.18/0.52 dependent: set(para_from).
% 0.18/0.52 dependent: set(para_into).
% 0.18/0.52 dependent: clear(para_from_right).
% 0.18/0.52 dependent: clear(para_into_right).
% 0.18/0.52 dependent: set(para_from_vars).
% 0.18/0.52 dependent: set(eq_units_both_ways).
% 0.18/0.52 dependent: set(dynamic_demod_all).
% 0.18/0.52 dependent: set(dynamic_demod).
% 0.18/0.52 dependent: set(order_eq).
% 0.18/0.52 dependent: set(back_demod).
% 0.18/0.52 dependent: set(lrpo).
% 0.18/0.52 dependent: set(hyper_res).
% 0.18/0.52 dependent: set(unit_deletion).
% 0.18/0.52 dependent: set(factor).
% 0.18/0.52
% 0.18/0.52 ------------> process usable:
% 0.18/0.52 Following clause subsumed by 19 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_HOL_Oord__class_Oless(B,C,A)|c_HOL_Oord__class_Oless(C,B,A).
% 0.18/0.52 Following clause subsumed by 19 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|C=B|c_HOL_Oord__class_Oless(C,B,A).
% 0.18/0.52 Following clause subsumed by 21 during input processing: 0 [] {-} A=B| -c_Ring__and__Field_Odvd__class_Odvd(B,A,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat).
% 0.18/0.52 Following clause subsumed by 21 during input processing: 0 [] {-} -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)|B=A| -c_Ring__and__Field_Odvd__class_Odvd(B,A,tc_nat).
% 0.18/0.52 Following clause subsumed by 21 during input processing: 0 [] {-} A=B| -c_Ring__and__Field_Odvd__class_Odvd(B,A,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat).
% 0.18/0.52 Following clause subsumed by 21 during input processing: 0 [] {-} A=B| -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(B,A,tc_nat).
% 0.18/0.52 Following clause subsumed by 21 during input processing: 0 [] {-} -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)|B=A| -c_Ring__and__Field_Odvd__class_Odvd(B,A,tc_nat).
% 0.18/0.52 Following clause subsumed by 21 during input processing: 0 [] {-} -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(B,A,tc_nat)|B=A.
% 0.18/0.52 Following clause subsumed by 20 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_lessequals(C,B,A)| -c_lessequals(B,C,A).
% 0.18/0.52 Following clause subsumed by 19 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|c_HOL_Oord__class_Oless(C,B,A)|C=B.
% 0.18/0.52 Following clause subsumed by 20 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_lessequals(C,B,A)| -c_lessequals(B,C,A).
% 0.18/0.52 Following clause subsumed by 25 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)|B=c_HOL_Ozero__class_Ozero(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(C,B,A),B,A)=C.
% 0.18/0.52 Following clause subsumed by 25 during input processing: 0 [flip.3] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(B,C,A),C,A)=B|C=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.52 Following clause subsumed by 25 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(B,C,A),C,A)=B|C=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 72 during input processing: 0 [] {-} -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ominus__class_Ominus(B,B,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 104 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__semiring__strict(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A).
% 0.18/0.53 Following clause subsumed by 124 during input processing: 0 [] {-} c_Suc(A)!=A.
% 0.18/0.53 Following clause subsumed by 131 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),C,A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(D,C,A),A).
% 0.18/0.53 Following clause subsumed by 134 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),C,A).
% 0.18/0.53 Following clause subsumed by 183 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_lessequals(B,c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A)| -c_lessequals(c_HOL_Otimes__class_Otimes(B,D,A),C,A).
% 0.18/0.53 Following clause subsumed by 184 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,C,A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(D,C,A),A).
% 0.18/0.53 Following clause subsumed by 190 during input processing: 0 [] {-} c_HOL_Oplus__class_Oplus(A,B,tc_nat)!=A|B=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.53 Following clause subsumed by 192 during input processing: 0 [] {-} c_Nat_Osemiring__1__class_Oof__nat(A,tc_Int_Oint)!=c_Nat_Osemiring__1__class_Oof__nat(B,tc_Int_Oint)|A=B.
% 0.18/0.53 Following clause subsumed by 86 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(A),c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(A),B,A),A).
% 0.18/0.53 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(C,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),C,A).
% 0.18/0.53 Following clause subsumed by 201 during input processing: 0 [] {-} -class_Divides_Osemiring__div(A)|c_Ring__and__Field_Odvd__class_Odvd(B,C,A)| -c_Ring__and__Field_Odvd__class_Odvd(B,c_Divides_Odiv__class_Omod(C,D,A),A)| -c_Ring__and__Field_Odvd__class_Odvd(B,D,A).
% 0.18/0.53 Following clause subsumed by 202 during input processing: 0 [] {-} -class_Divides_Osemiring__div(A)|c_Ring__and__Field_Odvd__class_Odvd(B,c_Divides_Odiv__class_Omod(C,D,A),A)| -c_Ring__and__Field_Odvd__class_Odvd(B,D,A)| -c_Ring__and__Field_Odvd__class_Odvd(B,C,A).
% 0.18/0.53 Following clause subsumed by 209 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,c_HOL_Oplus__class_Oplus(B,C,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(A,B,tc_nat).
% 0.18/0.53 Following clause subsumed by 210 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,c_HOL_Oplus__class_Oplus(B,C,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(A,C,tc_nat).
% 0.18/0.53 Following clause subsumed by 218 during input processing: 0 [flip.1] {-} c_Suc(A)!=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.53 Following clause subsumed by 225 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Int_Onumber__ring(A)|c_HOL_Oinverse__class_Oinverse(B,A)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(A),B,A).
% 0.18/0.53 Following clause subsumed by 262 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(B,C,A).
% 0.18/0.53 Following clause subsumed by 262 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)|B=C| -c_lessequals(B,C,A).
% 0.18/0.53 Following clause subsumed by 262 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(B,C,A)|B=C.
% 0.18/0.53 Following clause subsumed by 263 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(B,C,A).
% 0.18/0.53 Following clause subsumed by 264 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)|C=B| -c_lessequals(B,C,A).
% 0.18/0.53 Following clause subsumed by 270 during input processing: 0 [] {-} -class_Ring__and__Field_Opordered__ring(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),c_HOL_Otimes__class_Otimes(B,C,A),A)| -c_lessequals(C,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.53 Following clause subsumed by 215 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(B,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(C,c_Int_Onumber__class_Onumber__of(B,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.53 Following clause subsumed by 210 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),B,tc_nat).
% 0.18/0.53 Following clause subsumed by 209 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat).
% 0.18/0.53 Following clause subsumed by 184 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),A).
% 0.18/0.53 Following clause subsumed by 186 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(C,A),D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A)| -c_lessequals(c_HOL_Oinverse__class_Odivide(B,D,A),c_Int_Onumber__class_Onumber__of(C,A),A).
% 0.18/0.53 Following clause subsumed by 225 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)|c_HOL_Oinverse__class_Oinverse(B,A)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(A),B,A)|B=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 314 during input processing: 0 [] {-} c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)| -c_Parity_Oeven__odd__class_Oeven(B,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(A,tc_nat).
% 0.18/0.53 Following clause subsumed by 316 during input processing: 0 [] {-} c_Parity_Oeven__odd__class_Oeven(A,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(B,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat).
% 0.18/0.53 Following clause subsumed by 315 during input processing: 0 [] {-} c_Parity_Oeven__odd__class_Oeven(A,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(B,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(B,A,tc_nat),tc_nat).
% 0.18/0.53 Following clause subsumed by 315 during input processing: 0 [] {-} -c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)|c_Parity_Oeven__odd__class_Oeven(B,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(A,tc_nat).
% 0.18/0.53 Following clause subsumed by 316 during input processing: 0 [] {-} -c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)| -c_Parity_Oeven__odd__class_Oeven(B,tc_nat)|c_Parity_Oeven__odd__class_Oeven(A,tc_nat).
% 0.18/0.53 Following clause subsumed by 314 during input processing: 0 [] {-} -c_Parity_Oeven__odd__class_Oeven(A,tc_nat)| -c_Parity_Oeven__odd__class_Oeven(B,tc_nat)|c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(B,A,tc_nat),tc_nat).
% 0.18/0.53 Following clause subsumed by 324 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_HOL_Oinverse__class_Odivide(B,C,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A).
% 0.18/0.53 Following clause subsumed by 323 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_HOL_Oinverse__class_Odivide(B,C,A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.53 Following clause subsumed by 127 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A)|c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat).
% 0.18/0.53 Following clause subsumed by 347 during input processing: 0 [flip.2] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|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).
% 0.18/0.53 Following clause subsumed by 347 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|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).
% 0.18/0.53 Following clause subsumed by 358 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,B,A)|c_lessequals(B,B,A).
% 0.18/0.53 Following clause subsumed by 358 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_lessequals(B,C,A)|c_HOL_Oord__class_Oless(C,B,A).
% 0.18/0.53 Following clause subsumed by 358 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|c_lessequals(C,B,A).
% 0.18/0.53 Following clause subsumed by 360 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -c_lessequals(B,C,A)| -c_HOL_Oord__class_Oless(C,B,A).
% 0.18/0.53 Following clause subsumed by 361 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)|c_HOL_Oinverse__class_Odivide(B,B,A)=c_HOL_Oone__class_Oone(A)|B=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 361 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(B,B,A)=c_HOL_Oone__class_Oone(A)|B=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 166 during input processing: 0 [flip.2] {-} -class_Divides_Osemiring__div(A)|c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(B,c_Divides_Odiv__class_Omod(C,D,A),A),D,A)=c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(B,C,A),D,A).
% 0.18/0.53 Following clause subsumed by 167 during input processing: 0 [flip.2] {-} -class_Divides_Osemiring__div(A)|c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(c_Divides_Odiv__class_Omod(B,D,A),C,A),D,A)=c_Divides_Odiv__class_Omod(c_HOL_Oplus__class_Oplus(B,C,A),D,A).
% 0.18/0.53 Following clause subsumed by 389 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,C,A),A)| -c_Parity_Oeven__odd__class_Oeven(C,tc_nat).
% 0.18/0.53 Following clause subsumed by 394 during input processing: 0 [] {-} -class_OrderedGroup_Ogroup__add(A)|c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(B,A),B,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 409 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(B,c_HOL_Ozero__class_Ozero(A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 126 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A)|c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat)|c_Int_Onumber__class_Onumber__of(C,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.53 Following clause subsumed by 423 during input processing: 0 [flip.2] {-} -class_OrderedGroup_Oab__group__add(A)|c_HOL_Oplus__class_Oplus(B,c_HOL_Ouminus__class_Ouminus(C,A),A)=c_HOL_Ominus__class_Ominus(B,C,A).
% 0.18/0.53 Following clause subsumed by 409 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(A),c_HOL_Ozero__class_Ozero(A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.53 Following clause subsumed by 443 during input processing: 0 [] {-} -class_OrderedGroup_Opordered__ab__group__add__abs(A)|c_lessequals(c_HOL_Oabs__class_Oabs(B,A),C,A)| -c_lessequals(c_HOL_Ouminus__class_Ouminus(B,A),C,A)| -c_lessequals(B,C,A).
% 0.18/0.53 Following clause subsumed by 446 during input processing: 0 [] {-} c_HOL_Oplus__class_Oplus(A,B,tc_nat)!=c_HOL_Oplus__class_Oplus(A,C,tc_nat)|B=C.
% 0.18/0.53 Following clause subsumed by 455 during input processing: 0 [] {-} -class_Ring__and__Field_Opordered__cancel__semiring(A)|c_lessequals(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(C,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),B,A).
% 0.18/0.53 Following clause subsumed by 456 during input processing: 0 [] {-} -class_Ring__and__Field_Opordered__cancel__semiring(A)|c_lessequals(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),C,A)| -c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.53 Following clause subsumed by 456 during input processing: 0 [] {-} -class_Ring__and__Field_Opordered__cancel__semiring(A)|c_lessequals(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),C,A).
% 0.18/0.53 Following clause subsumed by 129 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(C,A),D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,D,A),c_Int_Onumber__class_Onumber__of(C,A),A).
% 0.18/0.53 Following clause subsumed by 133 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),A).
% 0.18/0.53 Following clause subsumed by 43 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),B,A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.53 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(B,c_HOL_Oinverse__class_Odivide(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(D,A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(C,c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),C,A).
% 0.18/0.53 Following clause subsumed by 46 during input processing: 0 [] {-} -class_Ring__and__Field_Ozero__neq__one(A)|c_HOL_Ozero__class_Ozero(A)!=c_HOL_Oone__class_Oone(A).
% 0.18/0.53 Following clause subsumed by 16 during input processing: 0 [] {-} -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)|c_Ring__and__Field_Odvd__class_Odvd(A,C,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(C,A,tc_nat)|c_Ring__and__Field_Odvd__class_Odvd(C,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(B,C,tc_nat).
% 0.18/0.53 Following clause subsumed by 306 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(C,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(D,c_Int_Onumber__class_Onumber__of(C,A),A),B,A).
% 0.18/0.53 Following clause subsumed by 307 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(C,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A).
% 0.18/0.53 Following clause subsumed by 310 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(C,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Oinverse__class_Odivide(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.53 Following clause subsumed by 311 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(B,c_HOL_Oinverse__class_Odivide(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(D,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A).
% 0.18/0.53 Following clause subsumed by 389 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat).
% 0.18/0.53 Following clause subsumed by 492 during input processing: 0 [] {-} -c_HOL_Oord__class_Oless(A,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat).
% 0.18/0.53 Following clause subsumed by 87 during input processing: 0 [] {-} -class_Ring__and__Field_Osemiring__0(A)| -class_Power_Opower(A)|c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(A),c_HOL_Ozero__class_Ozero(tc_nat),A)=c_HOL_Oone__class_Oone(A).
% 0.18/0.53 Following clause subsumed by 134 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(B,c_HOL_Oinverse__class_Odivide(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),C,A).
% 0.18/0.53 Following clause subsumed by 131 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Oinverse__class_Odivide(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.53 Following clause subsumed by 133 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.53 Following clause subsumed by 129 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(B,c_HOL_Otimes__class_Otimes(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(D,A),A),C,A).
% 0.18/0.53 Following clause subsumed by 510 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_HOL_Oinverse__class_Oinverse(B,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A).
% 0.18/0.53 Following clause subsumed by 183 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(B,c_HOL_Oinverse__class_Odivide(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),C,A).
% 0.18/0.53 Following clause subsumed by 185 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_lessequals(B,c_HOL_Oinverse__class_Odivide(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.53 Following clause subsumed by 184 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.53 Following clause subsumed by 186 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(B,c_HOL_Otimes__class_Otimes(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_lessequals(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(D,A),A),C,A).
% 0.18/0.53 Following clause subsumed by 531 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__ring__strict(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(D,C,A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(D,B,A).
% 0.18/0.54 Following clause subsumed by 534 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__ring__strict(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(B,D,A),A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(D,C,A).
% 0.18/0.54 Following clause subsumed by 535 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__ring__strict(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(B,D,A),A)| -c_HOL_Oord__class_Oless(C,D,A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A).
% 0.18/0.54 Following clause subsumed by 534 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__ring__strict(A)|c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(B,D,A),A)| -c_HOL_Oord__class_Oless(D,C,A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.54 Following clause subsumed by 539 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Otimes__class_Otimes(A,C,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat)| -c_HOL_Oord__class_Oless(B,C,tc_nat).
% 0.18/0.54 Following clause subsumed by 539 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Otimes__class_Otimes(A,C,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(B,C,tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat).
% 0.18/0.54 Following clause subsumed by 541 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Otimes__class_Otimes(C,B,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(A,C,tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),B,tc_nat).
% 0.18/0.54 Following clause subsumed by 374 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(B,tc_nat),tc_nat)|c_Int_Onumber__class_Onumber__of(B,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)|c_lessequals(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.54 Following clause subsumed by 548 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__semidom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Nat_Osemiring__1__class_Oof__nat(B,A),A).
% 0.18/0.54 Following clause subsumed by 554 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(A),B,A)=B.
% 0.18/0.54 Following clause subsumed by 570 during input processing: 0 [flip.2] {-} -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B.
% 0.18/0.54 Following clause subsumed by 570 during input processing: 0 [flip.2] {-} -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B.
% 0.18/0.54 Following clause subsumed by 570 during input processing: 0 [] {-} -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B.
% 0.18/0.54 Following clause subsumed by 575 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_Suc(A),c_Suc(B),tc_nat)| -c_HOL_Oord__class_Oless(A,B,tc_nat).
% 0.18/0.54 Following clause subsumed by 577 during input processing: 0 [] {-} -class_OrderedGroup_Opordered__ab__group__add(A)|c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(B,A),C,A)| -c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(C,A),B,A).
% 0.18/0.54 Following clause subsumed by 578 during input processing: 0 [] {-} -class_OrderedGroup_Opordered__ab__group__add(A)|c_HOL_Oord__class_Oless(B,c_HOL_Ouminus__class_Ouminus(C,A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Ouminus__class_Ouminus(B,A),A).
% 0.18/0.54 Following clause subsumed by 146 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|B=c_HOL_Ozero__class_Ozero(A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat)| -c_lessequals(c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.54 Following clause subsumed by 216 during input processing: 0 [flip.2] {-} -class_Ring__and__Field_Oring(A)|c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(E,C,A),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(B,E,A),C,A),D,A),A)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,C,A),D,A).
% 0.18/0.54 Following clause subsumed by 43 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),B,A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),A).
% 0.18/0.54 Following clause subsumed by 391 during input processing: 0 [flip.2] {-} -class_Int_Onumber__ring(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(A),A)=c_Int_Onumber__class_Onumber__of(c_Int_OMin,A).
% 0.18/0.54 Following clause subsumed by 306 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,A),A)|c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(D,C,A),c_Int_Onumber__class_Onumber__of(B,A),A).
% 0.18/0.54 Following clause subsumed by 307 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)|c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A).
% 0.18/0.54 Following clause subsumed by 309 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),B,A)| -c_HOL_Oord__class_Oless(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),A).
% 0.18/0.54 Following clause subsumed by 617 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Oplus__class_Oplus(B,C,A)=c_HOL_Oplus__class_Oplus(C,B,A).
% 0.18/0.54 Following clause subsumed by 641 during input processing: 0 [] {-} c_Suc(A)!=c_Suc(B)|A=B.
% 0.18/0.54 Following clause subsumed by 636 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A).
% 0.18/0.54 Following clause subsumed by 637 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),C,A).
% 0.18/0.54 Following clause subsumed by 310 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(D,C,A),A).
% 0.18/0.54 Following clause subsumed by 311 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A).
% 0.18/0.54 Following clause subsumed by 313 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),C,A).
% 0.18/0.54 Following clause subsumed by 634 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(C,A),D,A),A)| -c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(C,A),c_HOL_Oinverse__class_Odivide(B,D,A),A).
% 0.18/0.54 Following clause subsumed by 635 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A).
% 0.18/0.54 Following clause subsumed by 579 during input processing: 0 [] {-} -class_OrderedGroup_Opordered__ab__group__add(A)|c_lessequals(c_HOL_Ouminus__class_Ouminus(B,A),C,A)| -c_lessequals(c_HOL_Ouminus__class_Ouminus(C,A),B,A).
% 0.18/0.54 Following clause subsumed by 662 during input processing: 0 [] {-} -class_OrderedGroup_Opordered__ab__group__add(A)|c_lessequals(B,c_HOL_Ouminus__class_Ouminus(C,A),A)| -c_lessequals(C,c_HOL_Ouminus__class_Ouminus(B,A),A).
% 0.18/0.54 Following clause subsumed by 16 during input processing: 0 [] {-} -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)|c_Ring__and__Field_Odvd__class_Odvd(A,C,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(C,A,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(B,C,tc_nat).
% 0.18/0.54 Following clause subsumed by 16 during input processing: 0 [] {-} -c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(C,A,tc_nat)|c_Ring__and__Field_Odvd__class_Odvd(C,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(B,C,tc_nat).
% 0.18/0.54 Following clause subsumed by 674 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Otimes__class_Otimes(B,c_HOL_Ozero__class_Ozero(A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 675 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),B,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 673 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),B,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 679 during input processing: 0 [] {-} -class_Ring__and__Field_Oidom(A)| -class_Int_Onumber__ring(A)|c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(D,E,A),A)!=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,E,A),c_HOL_Otimes__class_Otimes(D,C,A),A)|C=E|B=D.
% 0.18/0.54 Following clause subsumed by 690 during input processing: 0 [flip.2] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(B,C,A),A)=c_HOL_Otimes__class_Otimes(B,c_HOL_Ouminus__class_Ouminus(C,A),A).
% 0.18/0.54 Following clause subsumed by 692 during input processing: 0 [flip.2] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(B,C,A),A)=c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(B,A),C,A).
% 0.18/0.54 Following clause subsumed by 697 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(B,C,A),D,A)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,D,A),c_HOL_Otimes__class_Otimes(C,D,A),A).
% 0.18/0.54 Following clause subsumed by 698 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Otimes__class_Otimes(B,c_HOL_Oplus__class_Oplus(C,D,A),A)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(B,D,A),A).
% 0.18/0.54 Following clause subsumed by 694 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(B,C,A),D,A)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,D,A),c_HOL_Otimes__class_Otimes(C,D,A),A).
% 0.18/0.54 Following clause subsumed by 708 during input processing: 0 [] {-} -class_Ring__and__Field_Ono__zero__divisors(A)|c_HOL_Otimes__class_Otimes(B,C,A)!=c_HOL_Ozero__class_Ozero(A)|B=c_HOL_Ozero__class_Ozero(A)|C=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 714 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(A),B,A)=B.
% 0.18/0.54 Following clause subsumed by 719 during input processing: 0 [] {-} -class_Ring__and__Field_Oidom(A)| -class_Int_Onumber__ring(A)|c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(B,D,A),A)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(B,D,A),c_HOL_Otimes__class_Otimes(B,C,A),A).
% 0.18/0.54 Following clause subsumed by 722 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Otimes__class_Otimes(B,c_HOL_Ominus__class_Ominus(C,D,A),A)=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(B,D,A),A).
% 0.18/0.54 Following clause subsumed by 723 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(B,C,A),D,A)=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(B,D,A),c_HOL_Otimes__class_Otimes(C,D,A),A).
% 0.18/0.54 Following clause subsumed by 710 during input processing: 0 [flip.2] {-} -class_Divides_Osemiring__div(A)|c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(c_Divides_Odiv__class_Omod(B,D,A),C,A),D,A)=c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(B,C,A),D,A).
% 0.18/0.54 Following clause subsumed by 649 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,A),A),c_Int_Onumber__class_Onumber__of(B,A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 25 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),C,A),C,A)=c_Int_Onumber__class_Onumber__of(B,A)|C=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 728 during input processing: 0 [flip.4] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),c_Int_Onumber__class_Onumber__of(C,A),A)=B|c_Int_Onumber__class_Onumber__of(C,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 25 during input processing: 0 [flip.4] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),C,A),C,A)=c_Int_Onumber__class_Onumber__of(B,A)|C=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 729 during input processing: 0 [flip.5] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_Int_Onumber__class_Onumber__of(B,A)!=c_HOL_Ozero__class_Ozero(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),C,A),C,A)=c_Int_Onumber__class_Onumber__of(B,A).
% 0.18/0.54 Following clause subsumed by 25 during input processing: 0 [flip.4] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(C,A),A),c_Int_Onumber__class_Onumber__of(C,A),A)=B|c_Int_Onumber__class_Onumber__of(C,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 25 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(C,A),A),c_Int_Onumber__class_Onumber__of(C,A),A)=B|c_Int_Onumber__class_Onumber__of(C,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 649 during input processing: 0 [flip.4] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,A),A),c_Int_Onumber__class_Onumber__of(B,A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 661 during input processing: 0 [] {-} A=B|c_HOL_Oord__class_Oless(A,B,tc_nat)| -c_HOL_Oord__class_Oless(A,c_Suc(B),tc_nat).
% 0.18/0.54 Following clause subsumed by 312 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),C,A).
% 0.18/0.54 Following clause subsumed by 340 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_Int_Onumber__class_Onumber__of(B,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,tc_nat),A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.54 Following clause subsumed by 750 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(B,C,A),C,A)=B|C=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 769 during input processing: 0 [] {-} -c_HOL_Oord__class_Oless(A,A,tc_nat).
% 0.18/0.54 Following clause subsumed by 218 during input processing: 0 [] {-} c_Suc(A)!=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.54 Following clause subsumed by 218 during input processing: 0 [] {-} c_Suc(A)!=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.54 Following clause subsumed by 807 during input processing: 0 [] {-} c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Otimes__class_Otimes(C,A,tc_nat),c_HOL_Otimes__class_Otimes(C,B,tc_nat),tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),C,tc_nat).
% 0.18/0.54 Following clause subsumed by 233 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A)|c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat)|c_Int_Onumber__class_Onumber__of(C,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),A).
% 0.18/0.54 Following clause subsumed by 360 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -class_Int_Onumber(A)| -c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(B,A),c_Int_Onumber__class_Onumber__of(C,A),A)| -c_lessequals(c_Int_Onumber__class_Onumber__of(C,A),c_Int_Onumber__class_Onumber__of(B,A),A).
% 0.18/0.54 Following clause subsumed by 358 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -class_Int_Onumber(A)|c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_Int_Onumber__class_Onumber__of(C,A),A)|c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(C,A),c_Int_Onumber__class_Onumber__of(B,A),A).
% 0.18/0.54 Following clause subsumed by 461 during input processing: 0 [] {-} -class_Int_Onumber(A)| -class_Divides_Osemiring__div(A)|c_Divides_Odiv__class_Omod(c_Int_Onumber__class_Onumber__of(B,A),c_Int_Onumber__class_Onumber__of(C,A),A)=c_HOL_Ozero__class_Ozero(A)| -c_Ring__and__Field_Odvd__class_Odvd(c_Int_Onumber__class_Onumber__of(C,A),c_Int_Onumber__class_Onumber__of(B,A),A).
% 0.18/0.54 Following clause subsumed by 462 during input processing: 0 [] {-} -class_Int_Onumber(A)| -class_Divides_Osemiring__div(A)|c_Divides_Odiv__class_Omod(c_Int_Onumber__class_Onumber__of(B,A),c_Int_Onumber__class_Onumber__of(C,A),A)!=c_HOL_Ozero__class_Ozero(A)|c_Ring__and__Field_Odvd__class_Odvd(c_Int_Onumber__class_Onumber__of(C,A),c_Int_Onumber__class_Onumber__of(B,A),A).
% 0.18/0.54 Following clause subsumed by 297 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A)|c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat).
% 0.18/0.54 Following clause subsumed by 769 during input processing: 0 [] {-} -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat).
% 0.18/0.54 Following clause subsumed by 810 during input processing: 0 [] {-} -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.54 Following clause subsumed by 830 during input processing: 0 [flip.1] {-} c_Int_OPls!=c_Int_OMin.
% 0.18/0.54 Following clause subsumed by 832 during input processing: 0 [] {-} c_Int_OBit0(A)!=c_Int_OMin.
% 0.18/0.54 Following clause subsumed by 416 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_Power_Opower__class_Opower(c_HOL_Oabs__class_Oabs(B,A),c_Int_Onumber__class_Onumber__of(C,tc_nat),A)=c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat).
% 0.18/0.54 Following clause subsumed by 93 during input processing: 0 [] {-} -class_Ring__and__Field_Ozero__neq__one(A)| -class_Ring__and__Field_Ono__zero__divisors(A)| -class_Ring__and__Field_Omult__zero(A)| -class_Power_Opower(A)|c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,tc_nat),A)=c_HOL_Ozero__class_Ozero(A)|c_Int_Onumber__class_Onumber__of(B,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.54 Following clause subsumed by 94 during input processing: 0 [] {-} -class_Ring__and__Field_Osemiring__0(A)| -class_Power_Opower(A)|c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,tc_nat),A)=c_HOL_Ozero__class_Ozero(A)|c_Int_Onumber__class_Onumber__of(B,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.18/0.55 Following clause subsumed by 376 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|B=c_HOL_Ozero__class_Ozero(A)|c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.55 Following clause subsumed by 375 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.55 Following clause subsumed by 848 during input processing: 0 [] {-} c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Otimes__class_Otimes(C,D,tc_nat),tc_nat)!=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,D,tc_nat),c_HOL_Otimes__class_Otimes(C,B,tc_nat),tc_nat)|B=D|A=C.
% 0.18/0.55 Following clause subsumed by 849 during input processing: 0 [] {-} c_HOL_Otimes__class_Otimes(A,B,tc_nat)!=c_HOL_Otimes__class_Otimes(A,C,tc_nat)|A=c_HOL_Ozero__class_Ozero(tc_nat)|B=C.
% 0.18/0.55 Following clause subsumed by 48 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__semidom(A)|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),A),c_Power_Opower__class_Opower(C,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),A),A).
% 0.18/0.55 Following clause subsumed by 878 during input processing: 0 [flip.2] {-} -class_Int_Onumber__ring(A)|c_HOL_Ozero__class_Ozero(A)=c_Int_Onumber__class_Onumber__of(c_Int_OPls,A).
% 0.18/0.55 Following clause subsumed by 887 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_Power_Opower__class_Opower(B,c_Suc(C),A)=c_HOL_Otimes__class_Otimes(B,c_Power_Opower__class_Opower(B,C,A),A).
% 0.18/0.55 Following clause subsumed by 887 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_Power_Opower__class_Opower(B,c_Suc(C),A)=c_HOL_Otimes__class_Otimes(B,c_Power_Opower__class_Opower(B,C,A),A).
% 0.18/0.55 Following clause subsumed by 896 during input processing: 0 [flip.3] {-} -class_Ring__and__Field_Ofield(A)| -class_Int_Onumber__ring(A)|c_HOL_Otimes__class_Otimes(B,c_HOL_Oinverse__class_Oinverse(C,A),A)=c_HOL_Oinverse__class_Odivide(B,C,A).
% 0.18/0.55 Following clause subsumed by 225 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Int_Onumber(A)|c_HOL_Oinverse__class_Oinverse(c_Int_Onumber__class_Onumber__of(B,A),A)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(A),c_Int_Onumber__class_Onumber__of(B,A),A).
% 0.18/0.55 Following clause subsumed by 905 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__semidom(A)|c_HOL_Oord__class_Oless(B,C,tc_nat)| -c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(D,B,A),c_Power_Opower__class_Opower(D,C,A),A)| -c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(A),D,A).
% 0.18/0.55 Following clause subsumed by 906 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__semidom(A)|c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(B,C,A),c_Power_Opower__class_Opower(B,D,A),A)| -c_HOL_Oord__class_Oless(C,D,tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(A),B,A).
% 0.18/0.55 Following clause subsumed by 557 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(C,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(B,A),D,A),C,A).
% 0.18/0.55 Following clause subsumed by 558 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(C,D,A),A)| -c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(D,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),D,A).
% 0.18/0.55 Following clause subsumed by 559 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_lessequals(c_Int_Onumber__class_Onumber__of(B,A),c_HOL_Oinverse__class_Odivide(D,C,A),A).
% 0.18/0.55 Following clause subsumed by 467 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),D,A)| -c_lessequals(c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),B,A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(C,A),A).
% 0.18/0.55 Following clause subsumed by 469 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(B,c_HOL_Oinverse__class_Odivide(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(C,c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A).
% 0.18/0.55 Following clause subsumed by 920 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A).
% 0.18/0.55 Following clause subsumed by 919 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(B,C,A),c_HOL_Ozero__class_Ozero(A),A)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A)| -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(A),A).
% 0.18/0.55 Following clause subsumed by 468 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)|c_HOL_Oord__class_Oless(C,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),A).
% 0.18/0.55 Following clause subsumed by 467 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,C,A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(D,A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(D,A),C,A),B,A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),C,A).
% 0.18/0.55 Following clause subsumed by 560 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(C,A),A),D,A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),D,A)| -c_lessequals(c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),B,A)| -c_lessequals(B,c_HOL_Otimes__class_Otimes(D,c_Int_Onumber__class_Onumber__of(C,A),A),A).
% 0.18/0.55 Following clause subsumed by 557 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__field(A)| -class_Ring__and__Field_Odivision__by__zero(A)| -class_Int_Onumber(A)|c_lessequals(B,c_HOL_Oinverse__class_Odivide(C,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_lessequals(B,c_HOL_Ozero__class_Ozero(A),A)| -c_lessequals(C,c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),A)| -c_lessequals(c_HOL_Otimes__class_Otimes(B,c_Int_Onumber__class_Onumber__of(D,A),A),C,A).
% 0.18/0.55 Following clause subsumed by 466 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A),A)|B=c_HOL_Ozero__class_Ozero(A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(C,tc_nat),tc_nat).
% 0.18/0.55 Following clause subsumed by 278 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_Int_Onumber__class_Onumber__of(B,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(A),c_Int_Onumber__class_Onumber__of(B,tc_nat),A),A)| -c_Parity_Oeven__odd__class_Oeven(c_Int_Onumber__class_Onumber__of(B,tc_nat),tc_nat).
% 0.18/0.55 Following clause subsumed by 409 during input processing: 0 [flip.3] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(B,c_HOL_Ozero__class_Ozero(A),A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.55 Following clause subsumed by 587 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,C,A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),B,A)|c_Parity_Oeven__odd__class_Oeven(C,tc_nat).
% 0.18/0.55 Following clause subsumed by 955 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),B,A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,C,A),A)|c_Parity_Oeven__odd__class_Oeven(C,tc_nat).
% 0.18/0.55 Following clause subsumed by 587 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,C,A),A)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),B,A)|c_Parity_Oeven__odd__class_Oeven(C,tc_nat).
% 0.18/0.55 Following clause subsumed by 955 during input processing: 0 [] {-} -class_Ring__and__Field_Oordered__idom(A)|c_lessequals(c_HOL_Ozero__class_Ozero(A),B,A)|c_Parity_Oeven__odd__class_Oeven(C,tc_nat)| -c_lessequals(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,C,A),A).
% 0.18/0.55 Following clause subsumed by 649 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Ring__and__Field_Odivision__by__zero(A)|c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),B,A),B,A)=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.55 Following clause subsumed by 16 during input processing: 0 [] {-} c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(C,B,tc_nat)|c_Ring__and__Field_Odvd__class_Odvd(C,A,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(A,C,tc_nat).
% 0.18/0.55 Following clause subsumed by 16 during input processing: 0 [] {-} c_Ring__and__Field_Odvd__class_Odvd(A,B,tc_nat)|c_Ring__and__Field_Odvd__class_Odvd(B,C,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(C,B,tc_nat)| -c_Ring__and__Field_Odvd__class_Odvd(A,C,tc_nat).
% 0.18/0.55 Following clause subsumed by 966 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_HOL_Oord__class_Oless(B,C,A)| -c_HOL_Oord__class_Oless(C,B,A).
% 0.18/0.55 Following clause subsumed by 840 during input processing: 0 [] {-} -class_Ring__and__Field_Ozero__neq__one(A)| -class_Ring__and__Field_Ono__zero__divisors(A)| -class_Ring__and__Field_Omult__zero(A)| -class_Power_Opower(A)|c_Power_Opower__class_Opower(B,c_Int_Onumber__class_Onumber__of(C,tc_nat),A)!=c_HOL_Ozero__class_Ozero(A)|B=c_HOL_Ozero__class_Ozero(A).
% 0.18/0.55 Following clause subsumed by 990 during input processing: 0 [] {-} -class_Ring__and__Field_Ofield(A)| -class_Int_Onumber__ring(A)|c_HOL_Oinverse__class_Odivide(B,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),A),A)=B.
% 0.39/0.58 Following clause subsumed by 1019 during input processing: 0 [] {-} c_Int_OBit1(A)!=c_Int_OPls.
% 0.39/0.58 Following clause subsumed by 1027 during input processing: 0 [flip.2] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(B,C,A),D,A)=c_HOL_Otimes__class_Otimes(B,c_HOL_Otimes__class_Otimes(C,D,A),A).
% 0.39/0.58 Following clause subsumed by 1027 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(B,C,A),D,A)=c_HOL_Otimes__class_Otimes(B,c_HOL_Otimes__class_Otimes(C,D,A),A).
% 0.39/0.58 Following clause subsumed by 1028 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(D,E,A),A)=c_HOL_Otimes__class_Otimes(D,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(B,C,A),E,A),A).
% 0.39/0.58 Following clause subsumed by 1027 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(B,C,A),c_HOL_Otimes__class_Otimes(D,E,A),A)=c_HOL_Otimes__class_Otimes(B,c_HOL_Otimes__class_Otimes(C,c_HOL_Otimes__class_Otimes(D,E,A),A),A).
% 0.39/0.58 Following clause subsumed by 1043 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|c_HOL_Otimes__class_Otimes(B,C,A)=c_HOL_Otimes__class_Otimes(C,B,A).
% 0.39/0.58 16 back subsumes 15.
% 0.39/0.58 133 back subsumes 130.
% 0.39/0.58 134 back subsumes 132.
% 0.39/0.58 155 back subsumes 154.
% 0.39/0.58 183 back subsumes 156.
% 0.39/0.58 185 back subsumes 157.
% 0.39/0.58 308 back subsumes 254.
% 0.39/0.58 308 back subsumes 230.
% 0.39/0.58 309 back subsumes 229.
% 0.39/0.58 312 back subsumes 253.
% 0.39/0.58 313 back subsumes 228.
% 0.39/0.58 360 back subsumes 359.
% 0.39/0.58 468 back subsumes 279.
% 0.39/0.58 469 back subsumes 159.
% 0.39/0.58 470 back subsumes 280.
% 0.39/0.58 470 back subsumes 158.
% 0.39/0.58 558 back subsumes 92.
% 0.39/0.58 559 back subsumes 91.
% 0.39/0.58 560 back subsumes 80.
% 0.39/0.58 561 back subsumes 90.
% 0.39/0.58 561 back subsumes 81.
% 0.39/0.58 562 back subsumes 89.
% 0.39/0.58 562 back subsumes 82.
% 0.39/0.58 587 back subsumes 193.
% 0.39/0.58 630 back subsumes 479.
% 0.39/0.58 630 back subsumes 227.
% 0.39/0.58 631 back subsumes 480.
% 0.39/0.58 631 back subsumes 226.
% 0.39/0.58 632 back subsumes 610.
% 0.39/0.58 632 back subsumes 608.
% 0.39/0.58 633 back subsumes 609.
% 0.39/0.58 633 back subsumes 250.
% 0.39/0.58 634 back subsumes 481.
% 0.39/0.58 635 back subsumes 482.
% 0.39/0.58 636 back subsumes 611.
% 0.39/0.58 637 back subsumes 249.
% 0.39/0.58 750 back subsumes 728.
% 0.39/0.58 778 back subsumes 777.
% 0.39/0.58 803 back subsumes 417.
% 0.39/0.58 816 back subsumes 815.
% 0.39/0.58 853 back subsumes 808.
% 0.39/0.58 855 back subsumes 540.
% 0.39/0.58 855 back subsumes 413.
% 0.39/0.58 913 back subsumes 603.
% 0.39/0.58 913 back subsumes 260.
% 0.39/0.58 914 back subsumes 604.
% 0.39/0.58 914 back subsumes 261.
% 0.39/0.58 915 back subsumes 747.
% 0.39/0.58 915 back subsumes 605.
% 0.39/0.58 916 back subsumes 746.
% 0.39/0.58 916 back subsumes 606.
% 0.39/0.58 955 back subsumes 194.
% 0.39/0.58 Following clause subsumed by 1047 during input processing: 0 [copy,1025,flip.1] {-} c_Int_OBit0(A)!=c_Int_OBit1(B).
% 0.39/0.58 1031 back subsumes 1020.
% 0.39/0.58 Following clause subsumed by 1025 during input processing: 0 [copy,1047,flip.1] {-} c_Int_OBit1(A)!=c_Int_OBit0(B).
% 0.39/0.58 1115 back subsumes 1114.
% 0.39/0.58
% 0.39/0.58 ------------> process sos:
% 0.39/0.58 Following clause subsumed by 1235 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,c_Suc(A),tc_nat).
% 0.39/0.58 Following clause subsumed by 1238 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,B,tc_nat)|c_HOL_Oord__class_Oless(B,A,tc_nat)|B=A.
% 0.39/0.58 Following clause subsumed by 1237 during input processing: 0 [] {-} c_Ring__and__Field_Odvd__class_Odvd(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat).
% 0.39/0.58 Following clause subsumed by 1248 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,c_Suc(c_HOL_Oplus__class_Oplus(A,B,tc_nat)),tc_nat).
% 0.39/0.58 Following clause subsumed by 1262 during input processing: 0 [] {-} c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)|c_Parity_Oeven__odd__class_Oeven(B,tc_nat)|c_Parity_Oeven__odd__class_Oeven(A,tc_nat).
% 0.39/0.58 Following clause subsumed by 1262 during input processing: 0 [] {-} c_Parity_Oeven__odd__class_Oeven(A,tc_nat)|c_Parity_Oeven__odd__class_Oeven(B,tc_nat)|c_Parity_Oeven__odd__class_Oeven(c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1275 during input processing: 0 [demod,1253] {-} c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1237 during input processing: 0 [] {-} c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1271 during input processing: 0 [demod,1253,1270,1253] {-} c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),B,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1253,1270,1253] {-} c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1271 during input processing: 0 [demod,1253,1253] {-} c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),B,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(A,B,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1284,1253,1291] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1284,1253,1291,1284,1253,1291,1284,1291] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1306] {-} c_Int_OMin=c_Int_OMin.
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1284,1328,1284,1328] {-} c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat)=c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1284,1331,1284,1331] {-} c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat)=c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1311] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.39/0.58 Following clause subsumed by 1297 during input processing: 0 [] {-} c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Otimes__class_Otimes(A,C,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,C,tc_nat),c_HOL_Otimes__class_Otimes(A,B,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1297 during input processing: 0 [] {-} c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Otimes__class_Otimes(A,C,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,C,tc_nat),c_HOL_Otimes__class_Otimes(A,B,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1333,1270] {-} c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(C,B,tc_nat),D,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(A,B,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(C,B,tc_nat),D,tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1339] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1253,1253,1253,1351,1270,1270] {-} c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat),tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat),tc_nat),tc_nat).
% 0.39/0.58 Following clause subsumed by 1293 during input processing: 0 [demod,1284,1284,1253,1291,1296,1284,1253,1291] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1357] {-} c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1357,1270,1253,1253] {-} c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat),tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1378,1284] {-} c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat)=c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1348] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1348] {-} c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1367,1375,1335,1339,1339] {-} c_HOL_Oplus__class_Oplus(A,A,tc_nat)=c_HOL_Oplus__class_Oplus(A,A,tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1367,1375,1333,1337,1337] {-} c_HOL_Oplus__class_Oplus(A,A,tc_nat)=c_HOL_Oplus__class_Oplus(A,A,tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1367,1375,1333,1337,1337,1367,1375,1333,1337,1337,1335,1367,1375,1333,1337,1337,1367,1375,1333,1337,1337] {-} c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(c_HOL_Oplus__class_Oplus(v_m,v_m,tc_nat)),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_i,v_j,tc_nat),c_HOL_Otimes__class_Otimes(v_i,v_j,tc_nat),tc_nat),tc_Complex_Ocomplex)=c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(c_HOL_Oplus__class_Oplus(v_m,v_m,tc_nat)),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_i,v_j,tc_nat),c_HOL_Otimes__class_Otimes(v_i,v_j,tc_nat),tc_nat),tc_Complex_Ocomplex).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [demod,1386] {-} c_Int_OPls=c_Int_OPls.
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [] {-} A=A.
% 0.41/0.59 Following clause subsumed by 1297 during input processing: 0 [copy,1255,flip.1] {-} c_HOL_Oplus__class_Oplus(A,c_HOL_Oone__class_Oone(tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat).
% 0.41/0.59 Following clause subsumed by 1271 during input processing: 0 [copy,1271,flip.1] {-} c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(B,C,tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(B,c_HOL_Oplus__class_Oplus(A,C,tc_nat),tc_nat).
% 0.41/0.59 Following clause subsumed by 1293 during input processing: 0 [copy,1293,flip.1] {-} A=A.
% 0.41/0.59 1293 back subsumes 1229.
% 0.41/0.59 1293 back subsumes 1103.
% 0.41/0.59 1293 back subsumes 1083.
% 0.41/0.59 1293 back subsumes 1082.
% 0.41/0.59 1293 back subsumes 1081.
% 0.41/0.59 1293 back subsumes 1053.
% 0.41/0.59 1293 back subsumes 1052.
% 0.41/0.59 1293 back subsumes 1051.
% 0.41/0.59 1293 back subsumes 1050.
% 0.41/0.59 Following clause subsumed by 1297 during input processing: 0 [copy,1297,flip.1] {-} c_HOL_Oplus__class_Oplus(A,B,tc_nat)=c_HOL_Oplus__class_Oplus(B,A,tc_nat).
% 0.41/0.59 1297 back subsumes 1255.
% 0.41/0.59 1381 back subsumes 1131.
% 0.41/0.59 Following clause subsumed by 1389 during input processing: 0 [copy,1389,flip.1] {-} c_HOL_Otimes__class_Otimes(A,B,tc_nat)=c_HOL_Otimes__class_Otimes(B,A,tc_nat).
% 0.41/0.59 Following clause subsumed by 1362 during input processing: 0 [copy,1684,flip.1] {-} c_Divides_Odiv__class_Omod(c_HOL_Otimes__class_Otimes(A,B,tc_nat),A,tc_nat)=c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat).
% 0.41/0.59 Following clause subsumed by 1364 during input processing: 0 [copy,1685,flip.1] {-} c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),A,tc_nat),tc_nat).
% 0.41/0.59 Following clause subsumed by 1697 during input processing: 0 [copy,1696,flip.1] {-} c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),A,tc_Complex_Ocomplex)=c_FFT__Mirabelle_Oroot(c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat)).
% 0.41/0.59 Following clause subsumed by 1696 during input processing: 0 [copy,1697,flip.1] {-} c_FFT__Mirabelle_Oroot(c_Int_Onumber__class_Onumber__of(c_Int_OMin,tc_nat))=c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),A,tc_Complex_Ocomplex).
% 0.41/0.59
% 0.41/0.59 ======= end of input processing =======
% 0.58/0.83
% 0.58/0.83
% 0.58/0.83
% 0.58/0.83 Aborting on detection of an error:
% 0.58/0.83
% 0.58/0.83 Too many clauses (whew!).
% 0.58/0.83
%------------------------------------------------------------------------------