%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SWW212+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n020.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 : Thu Jul 21 01:26:21 EDT 2022
% Result : Unknown 0.37s 0.62s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWW212+1 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n020.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 : Mon Jun 6 07:02:07 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.35/0.52 ----- Otter 3.2, August 2001 -----
% 0.35/0.52 The process was started by sandbox2 on n020.cluster.edu,
% 0.35/0.52 Mon Jun 6 07:02:07 2022
% 0.35/0.52 The command was "./sos". The process ID is 23649.
% 0.35/0.52
% 0.35/0.52 set(prolog_style_variables).
% 0.35/0.52 set(auto).
% 0.35/0.52 dependent: set(auto1).
% 0.35/0.52 dependent: set(process_input).
% 0.35/0.52 dependent: clear(print_kept).
% 0.35/0.52 dependent: clear(print_new_demod).
% 0.35/0.52 dependent: clear(print_back_demod).
% 0.35/0.52 dependent: clear(print_back_sub).
% 0.35/0.52 dependent: set(control_memory).
% 0.35/0.52 dependent: assign(max_mem, 12000).
% 0.35/0.52 dependent: assign(pick_given_ratio, 4).
% 0.35/0.52 dependent: assign(stats_level, 1).
% 0.35/0.52 dependent: assign(pick_semantic_ratio, 3).
% 0.35/0.52 dependent: assign(sos_limit, 5000).
% 0.35/0.52 dependent: assign(max_weight, 60).
% 0.35/0.52 clear(print_given).
% 0.35/0.52
% 0.35/0.52 formula_list(usable).
% 0.35/0.52
% 0.35/0.52 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=7.
% 0.35/0.52
% 0.35/0.52 This ia a non-Horn set with equality. The strategy will be
% 0.35/0.52 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.35/0.52 unit deletion, with positive clauses in sos and nonpositive
% 0.35/0.52 clauses in usable.
% 0.35/0.52
% 0.35/0.52 dependent: set(knuth_bendix).
% 0.35/0.52 dependent: set(para_from).
% 0.35/0.52 dependent: set(para_into).
% 0.35/0.52 dependent: clear(para_from_right).
% 0.35/0.52 dependent: clear(para_into_right).
% 0.35/0.52 dependent: set(para_from_vars).
% 0.35/0.52 dependent: set(eq_units_both_ways).
% 0.35/0.52 dependent: set(dynamic_demod_all).
% 0.35/0.52 dependent: set(dynamic_demod).
% 0.35/0.52 dependent: set(order_eq).
% 0.35/0.52 dependent: set(back_demod).
% 0.35/0.52 dependent: set(lrpo).
% 0.35/0.52 dependent: set(hyper_res).
% 0.35/0.52 dependent: set(unit_deletion).
% 0.35/0.52 dependent: set(factor).
% 0.35/0.52
% 0.35/0.52 ------------> process usable:
% 0.35/0.52 Following clause subsumed by 30 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless__eq(A,B,C)| -c_Orderings_Oord__class_Oless__eq(A,C,B)|B=C.
% 0.35/0.52 Following clause subsumed by 30 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless__eq(A,B,C)| -c_Orderings_Oord__class_Oless__eq(A,C,B)|C=B.
% 0.35/0.52 Following clause subsumed by 28 during input processing: 0 [] {-} -class_Orderings_Oord(A)| -c_Orderings_Oord__class_Oless__eq(tc_fun(B,A),C,D)|c_Orderings_Oord__class_Oless__eq(A,hAPP(C,E),hAPP(D,E)).
% 0.35/0.52 Following clause subsumed by 30 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_Orderings_Oord__class_Oless__eq(A,B,C)| -c_Orderings_Oord__class_Oless__eq(A,C,B).
% 0.35/0.52 Following clause subsumed by 27 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless__eq(A,B,C)|c_Orderings_Oord__class_Oless__eq(A,C,B).
% 0.35/0.52 Following clause subsumed by 28 during input processing: 0 [] {-} -class_Orderings_Oord(A)| -c_Orderings_Oord__class_Oless__eq(tc_fun(B,A),C,D)|c_Orderings_Oord__class_Oless__eq(A,hAPP(C,E),hAPP(D,E)).
% 0.35/0.52 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)| -c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.52 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)| -c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.52 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)| -c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.52 Following clause subsumed by 51 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)|B!=C.
% 0.35/0.52 Following clause subsumed by 41 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.52 Following clause subsumed by 41 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless(A,C,B)|C=B.
% 0.35/0.52 Following clause subsumed by 41 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless(A,B,C)|B=C|c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.52 Following clause subsumed by 41 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless(A,C,B)|B=C.
% 0.35/0.53 Following clause subsumed by 41 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.53 Following clause subsumed by 54 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B!=C| -c_Orderings_Oord__class_Oless(A,B,C).
% 0.35/0.53 Following clause subsumed by 64 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless__eq(A,B,C)|c_Orderings_Oord__class_Oless(A,B,C)|B=C.
% 0.35/0.53 Following clause subsumed by 54 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -c_Orderings_Oord__class_Oless__eq(A,B,C)| -c_Orderings_Oord__class_Oless(A,B,C)|B!=C.
% 0.35/0.53 Following clause subsumed by 63 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_Orderings_Oord__class_Oless__eq(A,C,B)|c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.53 Following clause subsumed by 64 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_Orderings_Oord__class_Oless__eq(A,B,C)|c_Orderings_Oord__class_Oless(A,B,C).
% 0.35/0.53 Following clause subsumed by 65 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless(A,B,C)| -c_Orderings_Oord__class_Oless__eq(A,B,C)|B=C.
% 0.35/0.53 Following clause subsumed by 69 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless__eq(A,C,B).
% 0.35/0.53 Following clause subsumed by 64 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless__eq(A,B,C)|c_Orderings_Oord__class_Oless(A,B,C)|B=C.
% 0.35/0.53 Following clause subsumed by 38 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_Orderings_Oord__class_Oless__eq(A,B,C)|B!=C.
% 0.35/0.53 Following clause subsumed by 66 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless__eq(A,B,C).
% 0.35/0.53 Following clause subsumed by 70 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless__eq(A,B,C).
% 0.35/0.53 Following clause subsumed by 51 during input processing: 0 [] {-} -class_Orderings_Oorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)|B!=C.
% 0.35/0.53 Following clause subsumed by 64 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_Orderings_Oord__class_Oless(A,B,C)| -c_Orderings_Oord__class_Oless__eq(A,B,C)|B=C.
% 0.35/0.53 Following clause subsumed by 69 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless__eq(A,B,C)|c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.53 Following clause subsumed by 69 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless__eq(A,B,C)|c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.53 Following clause subsumed by 67 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -c_Orderings_Oord__class_Oless__eq(A,B,C)| -c_Orderings_Oord__class_Oless(A,C,B).
% 0.35/0.53 Following clause subsumed by 69 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_Orderings_Oord__class_Oless(A,B,C)|c_Orderings_Oord__class_Oless__eq(A,C,B).
% 0.35/0.53 Following clause subsumed by 67 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -c_Orderings_Oord__class_Oless(A,B,C)| -c_Orderings_Oord__class_Oless__eq(A,C,B).
% 0.35/0.53 Following clause subsumed by 80 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B).
% 0.35/0.53 Following clause subsumed by 79 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B)| -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B)|A=B.
% 0.35/0.53 Following clause subsumed by 101 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),B)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.35/0.53 Following clause subsumed by 103 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)).
% 0.35/0.53 Following clause subsumed by 103 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)).
% 0.35/0.53 Following clause subsumed by 104 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,A).
% 0.35/0.53 Following clause subsumed by 107 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|B!=A.
% 0.35/0.53 Following clause subsumed by 106 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|A!=B.
% 0.35/0.53 Following clause subsumed by 122 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))|A!=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.35/0.53 Following clause subsumed by 106 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|A!=B.
% 0.35/0.53 Following clause subsumed by 127 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|A=B.
% 0.35/0.53 Following clause subsumed by 126 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B).
% 0.35/0.53 Following clause subsumed by 122 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|A!=B.
% 0.35/0.53 Following clause subsumed by 126 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B).
% 0.35/0.53 Following clause subsumed by 127 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|A=B|c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B).
% 0.35/0.53 Following clause subsumed by 126 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B).
% 0.35/0.53 Following clause subsumed by 122 during input processing: 0 [] {-} A!=B|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B).
% 0.35/0.53 Following clause subsumed by 129 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,C)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),B),A),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),C),A))| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,C).
% 0.35/0.53 Following clause subsumed by 102 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,C)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),B),A),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),C),A))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,C).
% 0.35/0.53 Following clause subsumed by 126 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B).
% 0.35/0.53 Following clause subsumed by 180 during input processing: 0 [] {-} -class_Groups_Ocancel__semigroup__add(A)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C)!=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),D)|C=D.
% 0.35/0.53 Following clause subsumed by 182 during input processing: 0 [] {-} -class_Groups_Ocancel__semigroup__add(A)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C)!=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),D),C)|B=D.
% 0.35/0.53 Following clause subsumed by 195 during input processing: 0 [] {-} -class_Groups_Oordered__ab__semigroup__add__imp__le(A)| -c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),D),C))|c_Orderings_Oord__class_Oless__eq(A,B,D).
% 0.35/0.53 Following clause subsumed by 197 during input processing: 0 [] {-} -class_Groups_Oordered__ab__semigroup__add__imp__le(A)| -c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),D))|c_Orderings_Oord__class_Oless__eq(A,C,D).
% 0.35/0.53 Following clause subsumed by 202 during input processing: 0 [] {-} -class_Groups_Oordered__ab__semigroup__add__imp__le(A)| -c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),D),C))|c_Orderings_Oord__class_Oless(A,B,D).
% 0.35/0.53 Following clause subsumed by 204 during input processing: 0 [] {-} -class_Groups_Oordered__ab__semigroup__add__imp__le(A)| -c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),D))|c_Orderings_Oord__class_Oless(A,C,D).
% 0.35/0.53 Following clause subsumed by 211 during input processing: 0 [] {-} A=B|hAPP(c_Complex_ORe,A)!=hAPP(c_Complex_ORe,B)|hAPP(c_Complex_OIm,A)!=hAPP(c_Complex_OIm,B).
% 0.35/0.53 Following clause subsumed by 267 during input processing: 0 [] {-} -class_RealVector_Ometric__space(A)|c_SEQ_Oconvergent(A,B)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially).
% 0.35/0.53 Following clause subsumed by 285 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),C),B)).
% 0.35/0.53 Following clause subsumed by 286 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),C)).
% 0.35/0.53 Following clause subsumed by 297 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B),C)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,C).
% 0.35/0.53 Following clause subsumed by 298 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B),C)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,C).
% 0.35/0.53 Following clause subsumed by 295 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),C),B)).
% 0.35/0.53 Following clause subsumed by 296 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),C)).
% 0.35/0.53 Following clause subsumed by 286 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A).
% 0.35/0.53 Following clause subsumed by 285 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),B).
% 0.35/0.53 Following clause subsumed by 324 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),C),B)),A)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),C),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),B),A)).
% 0.35/0.53 Following clause subsumed by 332 during input processing: 0 [] {-} -hBOOL(hAPP(A,hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),B),C)))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,C)|hBOOL(hAPP(A,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))).
% 0.35/0.53 Following clause subsumed by 333 during input processing: 0 [] {-} -hBOOL(hAPP(A,hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),B),C)))|B!=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),C),D)|hBOOL(hAPP(A,D)).
% 0.35/0.53 Following clause subsumed by 348 during input processing: 0 [] {-} -class_Rings_Ozero__neq__one(A)|c_Groups_Ozero__class_Ozero(A)!=c_Groups_Oone__class_Oone(A).
% 0.35/0.53 Following clause subsumed by 362 during input processing: 0 [] {-} -c_Limits_Otendsto(tc_Nat_Onat,tc_Complex_Ocomplex,A,B,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,tc_RealDef_Oreal,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,A),hAPP(c_Complex_ORe,B),c_Limits_Osequentially).
% 0.35/0.53 Following clause subsumed by 363 during input processing: 0 [] {-} -c_Limits_Otendsto(tc_Nat_Onat,tc_Complex_Ocomplex,A,B,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,tc_RealDef_Oreal,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_OIm,A),hAPP(c_Complex_OIm,B),c_Limits_Osequentially).
% 0.35/0.53 Following clause subsumed by 364 during input processing: 0 [] {-} -c_Limits_Otendsto(tc_Nat_Onat,tc_RealDef_Oreal,A,B,c_Limits_Osequentially)| -c_Limits_Otendsto(tc_Nat_Onat,tc_RealDef_Oreal,C,D,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,tc_Complex_Ocomplex,c_COMBS(tc_Nat_Onat,tc_RealDef_Oreal,tc_Complex_Ocomplex,c_COMBB(tc_RealDef_Oreal,tc_fun(tc_RealDef_Oreal,tc_Complex_Ocomplex),tc_Nat_Onat,c_Complex_Ocomplex_OComplex,A),C),hAPP(hAPP(c_Complex_Ocomplex_OComplex,B),D),c_Limits_Osequentially).
% 0.35/0.53 Following clause subsumed by 356 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__vector(A)| -c_Limits_Otendsto(B,tc_RealDef_Oreal,c_COMBB(A,tc_RealDef_Oreal,B,c_RealVector_Onorm__class_Onorm(A),C),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),D)|c_Limits_Otendsto(B,A,C,c_Groups_Ozero__class_Ozero(A),D).
% 0.35/0.53 Following clause subsumed by 357 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__vector(A)|c_Limits_Otendsto(B,tc_RealDef_Oreal,c_COMBB(A,tc_RealDef_Oreal,B,c_RealVector_Onorm__class_Onorm(A),C),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),D)| -c_Limits_Otendsto(B,A,C,c_Groups_Ozero__class_Ozero(A),D).
% 0.35/0.53 Following clause subsumed by 267 during input processing: 0 [] {-} -class_RealVector_Ometric__space(A)|c_SEQ_Oconvergent(A,B)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,c_SEQ_Olim(A,B),c_Limits_Osequentially).
% 0.35/0.53 Following clause subsumed by 305 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,B)|B!=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),C).
% 0.35/0.53 Following clause subsumed by 416 during input processing: 0 [] {-} -class_Rings_Olinordered__semidom(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Oone__class_Oone(A),B)| -c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Power_Opower__class_Opower(A),B),C),hAPP(hAPP(c_Power_Opower__class_Opower(A),B),D))|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,C,D).
% 0.35/0.53 Following clause subsumed by 445 during input processing: 0 [] {-} -class_Rings_Olinordered__semidom(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Oone__class_Oone(A),B)| -c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Power_Opower__class_Opower(A),B),C),hAPP(hAPP(c_Power_Opower__class_Opower(A),B),D))|c_Orderings_Oord__class_Oless(tc_Nat_Onat,C,D).
% 0.35/0.53 Following clause subsumed by 444 during input processing: 0 [] {-} -class_Rings_Olinordered__semidom(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Oone__class_Oone(A),B)|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Power_Opower__class_Opower(A),B),C),hAPP(hAPP(c_Power_Opower__class_Opower(A),B),D))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,C,D).
% 0.35/0.53 Following clause subsumed by 466 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),c_Groups_Oone__class_Oone(tc_Int_Oint)),B)| -c_Orderings_Oord__class_Oless(tc_Int_Oint,A,B).
% 0.35/0.53 Following clause subsumed by 456 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,c_RComplete_Onatfloor(A))| -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,B),A).
% 0.35/0.53 Following clause subsumed by 505 during input processing: 0 [flip.2] {-} -class_Rings_Ocomm__semiring__1(A)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C)),D)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),C),D)).
% 0.35/0.53 Following clause subsumed by 502 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(A),B)| -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealDef_Oreal(tc_Nat_Onat,B)).
% 0.37/0.54 Following clause subsumed by 422 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Nat_Onat),A),B))|B=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A).
% 0.37/0.54 Following clause subsumed by 424 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Nat_Onat),A),B))|B!=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.54 Following clause subsumed by 423 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Nat_Onat),A),B))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A).
% 0.37/0.54 Following clause subsumed by 544 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__field(A)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,A,c_COMBC(tc_Nat_Onat,A,A,c_COMBB(A,tc_fun(A,A),tc_Nat_Onat,c_Rings_Oinverse__class_Odivide(A),B),D),hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),C),D),c_Limits_Osequentially).
% 0.37/0.54 Following clause subsumed by 560 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__field(A)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially)| -c_Limits_Otendsto(tc_Nat_Onat,A,D,E,c_Limits_Osequentially)|E=c_Groups_Ozero__class_Ozero(A)|c_Limits_Otendsto(tc_Nat_Onat,A,c_COMBS(tc_Nat_Onat,A,A,c_COMBB(A,tc_fun(A,A),tc_Nat_Onat,c_Rings_Oinverse__class_Odivide(A),B),D),hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),C),E),c_Limits_Osequentially).
% 0.37/0.54 Following clause subsumed by 614 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__field(A)| -c_Series_Osums(A,B,C)|c_Series_Osums(A,c_COMBC(tc_Nat_Onat,A,A,c_COMBB(A,tc_fun(A,A),tc_Nat_Onat,c_Rings_Oinverse__class_Odivide(A),B),D),hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),C),D)).
% 0.37/0.54 Following clause subsumed by 612 during input processing: 0 [flip.2] {-} -c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,A,B)|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Int_Oint),B),A)=c_Nat__Transfer_Otsub(B,A).
% 0.37/0.54 Following clause subsumed by 625 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),A)|c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Divides_Odiv__class_Odiv(tc_Int_Oint,B,A),c_Groups_Ozero__class_Ozero(tc_Int_Oint))| -c_Orderings_Oord__class_Oless(tc_Int_Oint,B,c_Groups_Ozero__class_Ozero(tc_Int_Oint)).
% 0.37/0.54 Following clause subsumed by 637 during input processing: 0 [] {-} c_Divides_Odiv__class_Odiv(tc_Int_Oint,A,B)=c_Groups_Ozero__class_Ozero(tc_Int_Oint)| -c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),A)| -c_Orderings_Oord__class_Oless(tc_Int_Oint,A,B).
% 0.37/0.54 Following clause subsumed by 632 during input processing: 0 [] {-} c_Divides_Odiv__class_Odiv(tc_Int_Oint,A,B)=c_Groups_Ozero__class_Ozero(tc_Int_Oint)| -c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,A,c_Groups_Ozero__class_Ozero(tc_Int_Oint))| -c_Orderings_Oord__class_Oless(tc_Int_Oint,B,A).
% 0.37/0.54 Following clause subsumed by 666 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)| -c_Series_Osums(A,B,C)|c_Series_Osums(A,c_COMBB(A,A,tc_Nat_Onat,hAPP(c_Groups_Otimes__class_Otimes(A),D),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),C)).
% 0.37/0.54 Following clause subsumed by 667 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)| -c_Series_Osums(A,B,C)|c_Series_Osums(A,c_COMBC(tc_Nat_Onat,A,A,c_COMBB(A,tc_fun(A,A),tc_Nat_Onat,c_Groups_Otimes__class_Otimes(A),B),D),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D)).
% 0.37/0.54 Following clause subsumed by 707 during input processing: 0 [flip.2] {-} -class_Rings_Ocomm__semiring__1(A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C)),D)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D)).
% 0.37/0.54 Following clause subsumed by 715 during input processing: 0 [] {-} -class_Rings_Ono__zero__divisors(A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C)!=c_Groups_Ozero__class_Ozero(A)|B=c_Groups_Ozero__class_Ozero(A)|C=c_Groups_Ozero__class_Ozero(A).
% 0.37/0.54 Following clause subsumed by 716 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),c_Groups_Ozero__class_Ozero(A))=c_Groups_Ozero__class_Ozero(A).
% 0.37/0.54 Following clause subsumed by 717 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),c_Groups_Ozero__class_Ozero(A)),B)=c_Groups_Ozero__class_Ozero(A).
% 0.37/0.54 Following clause subsumed by 719 during input processing: 0 [] {-} -class_Rings_Odivision__ring(A)|B=c_Groups_Ozero__class_Ozero(A)|hAPP(c_Rings_Oinverse__class_Oinverse(A),B)!=c_Groups_Ozero__class_Ozero(A).
% 0.37/0.54 Following clause subsumed by 730 during input processing: 0 [] {-} -class_Rings_Odivision__ring__inverse__zero(A)|hAPP(c_Rings_Oinverse__class_Oinverse(A),B)!=hAPP(c_Rings_Oinverse__class_Oinverse(A),C)|B=C.
% 0.37/0.54 Following clause subsumed by 737 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),hAPP(hAPP(c_Groups_Ominus__class_Ominus(A),B),C)),D)=hAPP(hAPP(c_Groups_Ominus__class_Ominus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D)).
% 0.37/0.54 Following clause subsumed by 739 during input processing: 0 [flip.2] {-} -class_RealVector_Oreal__normed__algebra(A)|hAPP(hAPP(c_Groups_Ominus__class_Ominus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),hAPP(hAPP(c_Groups_Ominus__class_Ominus(A),C),D)).
% 0.37/0.54 Following clause subsumed by 743 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C)),D)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D)).
% 0.37/0.54 Following clause subsumed by 745 during input processing: 0 [flip.2] {-} -class_RealVector_Oreal__normed__algebra(A)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),C),D)).
% 0.37/0.54 Following clause subsumed by 756 during input processing: 0 [] {-} -class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(A)|B=C|D=E|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),E))!=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),E)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D)).
% 0.37/0.54 Following clause subsumed by 757 during input processing: 0 [] {-} -class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(A)|B!=C|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),E))=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),E)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D)).
% 0.37/0.54 Following clause subsumed by 758 during input processing: 0 [] {-} -class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(A)|B!=C|hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),B)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),E),C))=hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),E),B)).
% 0.37/0.54 Following clause subsumed by 792 during input processing: 0 [] {-} -class_Rings_Oordered__ring(A)| -c_Orderings_Oord__class_Oless__eq(A,B,c_Groups_Ozero__class_Ozero(A))| -c_Orderings_Oord__class_Oless__eq(A,C,c_Groups_Ozero__class_Ozero(A))|c_Orderings_Oord__class_Oless__eq(A,c_Groups_Ozero__class_Ozero(A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C)).
% 0.37/0.54 Following clause subsumed by 790 during input processing: 0 [] {-} -class_Rings_Oordered__cancel__semiring(A)| -c_Orderings_Oord__class_Oless__eq(A,B,c_Groups_Ozero__class_Ozero(A))| -c_Orderings_Oord__class_Oless__eq(A,c_Groups_Ozero__class_Ozero(A),C)|c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),c_Groups_Ozero__class_Ozero(A)).
% 0.37/0.54 Following clause subsumed by 790 during input processing: 0 [] {-} -class_Rings_Oordered__cancel__semiring(A)| -c_Orderings_Oord__class_Oless__eq(A,c_Groups_Ozero__class_Ozero(A),B)| -c_Orderings_Oord__class_Oless__eq(A,C,c_Groups_Ozero__class_Ozero(A))|c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),B),c_Groups_Ozero__class_Ozero(A)).
% 0.37/0.54 Following clause subsumed by 789 during input processing: 0 [] {-} -class_Rings_Oordered__cancel__semiring(A)| -c_Orderings_Oord__class_Oless__eq(A,c_Groups_Ozero__class_Ozero(A),B)| -c_Orderings_Oord__class_Oless__eq(A,C,c_Groups_Ozero__class_Ozero(A))|c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),c_Groups_Ozero__class_Ozero(A)).
% 0.37/0.54 Following clause subsumed by 814 during input processing: 0 [] {-} -class_Rings_Olinordered__ring__strict(A)| -c_Orderings_Oord__class_Oless(A,B,c_Groups_Ozero__class_Ozero(A))|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D))| -c_Orderings_Oord__class_Oless(A,D,C).
% 0.37/0.54 Following clause subsumed by 820 during input processing: 0 [] {-} -class_Rings_Olinordered__semiring__strict(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)| -c_Orderings_Oord__class_Oless(A,C,c_Groups_Ozero__class_Ozero(A))|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),B),c_Groups_Ozero__class_Ozero(A)).
% 0.37/0.54 Following clause subsumed by 827 during input processing: 0 [] {-} -class_Rings_Olinordered__ring__strict(A)|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D))| -c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)| -c_Orderings_Oord__class_Oless(A,C,D).
% 0.37/0.54 Following clause subsumed by 814 during input processing: 0 [] {-} -class_Rings_Olinordered__ring__strict(A)|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D))| -c_Orderings_Oord__class_Oless(A,B,c_Groups_Ozero__class_Ozero(A))| -c_Orderings_Oord__class_Oless(A,D,C).
% 0.37/0.54 Following clause subsumed by 815 during input processing: 0 [] {-} -class_Rings_Olinordered__ring__strict(A)|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),C))| -c_Orderings_Oord__class_Oless(A,C,c_Groups_Ozero__class_Ozero(A))| -c_Orderings_Oord__class_Oless(A,D,B).
% 0.37/0.54 Following clause subsumed by 852 during input processing: 0 [] {-} -class_Rings_Odivision__ring(A)|B=c_Groups_Ozero__class_Ozero(A)|hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),C),B)=D|C!=hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),B).
% 0.37/0.54 Following clause subsumed by 851 during input processing: 0 [] {-} -class_Rings_Odivision__ring(A)|B=c_Groups_Ozero__class_Ozero(A)|C=hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),D),B)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),B)!=D.
% 0.37/0.54 Following clause subsumed by 869 during input processing: 0 [] {-} -class_Divides_Osemiring__div(A)|B=c_Groups_Ozero__class_Ozero(A)|c_Divides_Odiv__class_Odiv(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),B),D))=c_Divides_Odiv__class_Odiv(A,C,D).
% 0.37/0.54 Following clause subsumed by 733 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,A,c_COMBB(A,A,tc_Nat_Onat,hAPP(c_Groups_Otimes__class_Otimes(A),D),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),C),c_Limits_Osequentially).
% 0.37/0.55 Following clause subsumed by 734 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,A,c_COMBC(tc_Nat_Onat,A,A,c_COMBB(A,tc_fun(A,A),tc_Nat_Onat,c_Groups_Otimes__class_Otimes(A),B),D),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),D),c_Limits_Osequentially).
% 0.37/0.55 Following clause subsumed by 735 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__algebra(A)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially)| -c_Limits_Otendsto(tc_Nat_Onat,A,D,E,c_Limits_Osequentially)|c_Limits_Otendsto(tc_Nat_Onat,A,c_COMBS(tc_Nat_Onat,A,A,c_COMBB(A,tc_fun(A,A),tc_Nat_Onat,c_Groups_Otimes__class_Otimes(A),B),D),hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),E),c_Limits_Osequentially).
% 0.37/0.55 Following clause subsumed by 788 during input processing: 0 [] {-} -class_Rings_Odivision__ring(A)|B=c_Groups_Ozero__class_Ozero(A)|hAPP(c_Rings_Oinverse__class_Oinverse(A),B)=hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),c_Groups_Oone__class_Oone(A)),B).
% 0.37/0.55 Following clause subsumed by 944 during input processing: 0 [] {-} -class_Fields_Olinordered__field(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)| -c_Orderings_Oord__class_Oless(A,C,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),B))|c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),C),B),D).
% 0.37/0.55 Following clause subsumed by 942 during input processing: 0 [] {-} -class_Fields_Olinordered__field(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)| -c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),B),D)|c_Orderings_Oord__class_Oless(A,C,hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),D),B)).
% 0.37/0.55 Following clause subsumed by 885 during input processing: 0 [] {-} -class_RealVector_Oreal__normed__div__algebra(A)| -c_Limits_Otendsto(tc_Nat_Onat,A,B,C,c_Limits_Osequentially)|C=c_Groups_Ozero__class_Ozero(A)|c_Limits_Otendsto(tc_Nat_Onat,A,c_COMBB(A,A,tc_Nat_Onat,c_Rings_Oinverse__class_Oinverse(A),B),hAPP(c_Rings_Oinverse__class_Oinverse(A),C),c_Limits_Osequentially).
% 0.37/0.55 Following clause subsumed by 997 during input processing: 0 [] {-} -class_Fields_Olinordered__field(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)|c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),C),B),D)| -c_Orderings_Oord__class_Oless__eq(A,C,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),D),B)).
% 0.37/0.55 Following clause subsumed by 996 during input processing: 0 [] {-} -class_Fields_Olinordered__field(A)| -c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)|c_Orderings_Oord__class_Oless__eq(A,C,hAPP(hAPP(c_Rings_Oinverse__class_Odivide(A),D),B))| -c_Orderings_Oord__class_Oless__eq(A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(A),C),B),D).
% 0.37/0.55 Following clause subsumed by 1046 during input processing: 0 [] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)!=c_Groups_Oone__class_Oone(tc_Nat_Onat)|A=c_Groups_Oone__class_Oone(tc_Nat_Onat).
% 0.37/0.55 Following clause subsumed by 1048 during input processing: 0 [] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)!=c_Groups_Oone__class_Oone(tc_Nat_Onat)|B=c_Groups_Oone__class_Oone(tc_Nat_Onat).
% 0.37/0.55 Following clause subsumed by 1050 during input processing: 0 [] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)=c_Groups_Oone__class_Oone(tc_Nat_Onat)|A!=c_Groups_Oone__class_Oone(tc_Nat_Onat)|B!=c_Groups_Oone__class_Oone(tc_Nat_Onat).
% 0.37/0.55 Following clause subsumed by 1059 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),C)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),B),C)).
% 0.37/0.58 Following clause subsumed by 1056 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),C)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),C),A),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),C),B)).
% 0.37/0.58 Following clause subsumed by 1044 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),C),B))| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,C).
% 0.37/0.58 Following clause subsumed by 1043 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C))| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,C).
% 0.37/0.58 Following clause subsumed by 1040 during input processing: 0 [] {-} A!=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.58 Following clause subsumed by 1036 during input processing: 0 [] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)!=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C)|A=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|B=C.
% 0.37/0.58 Following clause subsumed by 1038 during input processing: 0 [] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C)|A!=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.58 Following clause subsumed by 1037 during input processing: 0 [] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C)|B!=C.
% 0.37/0.58 Following clause subsumed by 1055 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C))|c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,C).
% 0.37/0.58 Following clause subsumed by 1056 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C))| -c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,C).
% 0.37/0.58 Following clause subsumed by 1037 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C)|B!=C.
% 0.37/0.58 Following clause subsumed by 1066 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C))|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,C).
% 0.37/0.58 Following clause subsumed by 1043 during input processing: 0 [] {-} -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C))| -c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,C).
% 0.37/0.58 38 back subsumes 36.
% 0.37/0.58 54 back subsumes 52.
% 0.37/0.58 107 back subsumes 105.
% 0.37/0.58 226 back subsumes 222.
% 0.37/0.58 240 back subsumes 238.
% 0.37/0.58 241 back subsumes 239.
% 0.37/0.58 356 back subsumes 275.
% 0.37/0.58 357 back subsumes 276.
% 0.37/0.58 368 back subsumes 256.
% 0.37/0.58 369 back subsumes 260.
% 0.37/0.58 370 back subsumes 262.
% 0.37/0.58 371 back subsumes 257.
% 0.37/0.58 644 back subsumes 642.
% 0.37/0.58 707 back subsumes 705.
% 0.37/0.58 708 back subsumes 704.
% 0.37/0.58 1025 back subsumes 441.
% 0.37/0.58 1287 back subsumes 1269.
% 0.37/0.58 1288 back subsumes 1270.
% 0.37/0.58 Following clause subsumed by 482 during input processing: 0 [copy,1298,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),A)),A)!=c_Groups_Ozero__class_Ozero(tc_Int_Oint).
% 0.37/0.58 1375 back subsumes 1370.
% 0.37/0.58
% 0.37/0.58 ------------> process sos:
% 0.37/0.61 Following clause subsumed by 1511 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),v_r).
% 0.37/0.61 Following clause subsumed by 1517 during input processing: 0 [] {-} A=B|c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,A).
% 0.37/0.61 Following clause subsumed by 1516 during input processing: 0 [] {-} A=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A).
% 0.37/0.61 Following clause subsumed by 1517 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless(tc_Nat_Onat,A,B)|A=B|c_Orderings_Oord__class_Oless(tc_Nat_Onat,B,A)|hBOOL(hAPP(hAPP(C,B),A)).
% 0.37/0.61 Following clause subsumed by 1515 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),A).
% 0.37/0.61 Following clause subsumed by 1515 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_RComplete_Onatceiling(A)).
% 0.37/0.61 Following clause subsumed by 1515 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_RComplete_Onatfloor(A)).
% 0.37/0.61 Following clause subsumed by 1681 during input processing: 0 [] {-} c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),c_Groups_Ozero__class_Ozero(tc_Int_Oint)).
% 0.37/0.61 Following clause subsumed by 1697 during input processing: 0 [] {-} hAPP(hAPP(c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),hAPP(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal),B)).
% 0.37/0.61 Following clause subsumed by 1656 during input processing: 0 [] {-} hBOOL(hAPP(A,c_Divides_Odiv__class_Odiv(tc_Int_Oint,B,C)))|C=c_Groups_Ozero__class_Ozero(tc_Int_Oint)|c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),C)|c_Orderings_Oord__class_Oless(tc_Int_Oint,C,c_Groups_Ozero__class_Ozero(tc_Int_Oint)).
% 0.37/0.61 Following clause subsumed by 1523 during input processing: 0 [copy,1523,flip.1] {-} hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),B)),C)=hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),C)),B).
% 0.37/0.61 1524 back subsumes 1497.
% 0.37/0.61 1524 back subsumes 1301.
% 0.37/0.61 1524 back subsumes 1280.
% 0.37/0.61 1524 back subsumes 1277.
% 0.37/0.61 1524 back subsumes 1273.
% 0.37/0.61 1524 back subsumes 1272.
% 0.37/0.61 1526 back subsumes 1254.
% 0.37/0.61 Following clause subsumed by 2027 during input processing: 0 [copy,1614,flip.1] {-} c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex).
% 0.37/0.61 Following clause subsumed by 2027 during input processing: 0 [copy,1616,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),A),B)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),A),B).
% 0.37/0.61 Following clause subsumed by 1621 during input processing: 0 [copy,1621,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),A).
% 0.37/0.61 Following clause subsumed by 1622 during input processing: 0 [copy,1622,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),C))=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),C)).
% 0.37/0.61 Following clause subsumed by 2027 during input processing: 0 [copy,1632,flip.1] {-} c_Complex_Oii=c_Complex_Oii.
% 0.37/0.61 Following clause subsumed by 2027 during input processing: 0 [copy,1647,flip.1] {-} c_RealDef_Oreal(tc_Nat_Onat,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Nat_Onat),A),B))=c_RealDef_Oreal(tc_Nat_Onat,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Nat_Onat),A),B)).
% 0.37/0.61 1680 back subsumes 1348.
% 0.37/0.61 1680 back subsumes 647.
% 0.37/0.61 Following clause subsumed by 1682 during input processing: 0 [copy,1682,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),B)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),B),A).
% 0.37/0.61 Following clause subsumed by 1683 during input processing: 0 [copy,1683,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),B),C))=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),B),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),C)).
% 0.37/0.61 Following clause subsumed by 1703 during input processing: 0 [copy,1703,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),B),A).
% 0.37/0.61 Following clause subsumed by 2027 during input processing: 0 [copy,1787,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),A),B).
% 0.37/0.61 Following clause subsumed by 1791 during input processing: 0 [copy,1791,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),B),A).
% 0.37/0.61 Following clause subsumed by 1794 during input processing: 0 [copy,1794,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),B),A).
% 0.37/0.61 Following clause subsumed by 2027 during input processing: 0 [copy,2027,flip.1] {-} A=A.
% 0.37/0.61 2027 back subsumes 1787.
% 0.37/0.61 2027 back subsumes 1647.
% 0.37/0.61 2027 back subsumes 1632.
% 0.37/0.61 2027 back subsumes 1616.
% 0.37/0.61 2027 back subsumes 1614.
% 0.37/0.61 2027 back subsumes 1360.
% 0.37/0.61 2027 back subsumes 1359.
% 0.37/0.61 2027 back subsumes 1358.
% 0.37/0.61 2027 back subsumes 1300.
% 0.37/0.61 2027 back subsumes 1299.
% 0.37/0.61 2027 back subsumes 1297.
% 0.37/0.61 2027 back subsumes 1284.
% 0.37/0.61 2027 back subsumes 1271.
% 0.37/0.61 2027 back subsumes 1252.
% 0.37/0.61 2027 back subsumes 1251.
% 0.37/0.61 2027 back subsumes 1250.
% 0.37/0.61 2027 back subsumes 1249.
% 0.37/0.61 2027 back subsumes 1248.
% 0.37/0.61 2027 back subsumes 1241.
% 0.37/0.61 2027 back subsumes 1240.
% 0.37/0.61 Following clause subsumed by 1522 during input processing: 0 [copy,2028,flip.1] {-} hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),A)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.61 Following clause subsumed by 1529 during input processing: 0 [copy,2029,flip.1] {-} hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(hAPP(c_Complex_Ocomplex_OComplex,A),B)),hAPP(hAPP(c_Complex_Ocomplex_OComplex,C),D))=hAPP(hAPP(c_Complex_Ocomplex_OComplex,hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),A),C)),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),B),D)).
% 0.37/0.61 Following clause subsumed by 1533 during input processing: 0 [copy,2030,flip.1] {-} c_Complex_Ocomplex_Ocomplex__size(hAPP(hAPP(c_Complex_Ocomplex_OComplex,A),B))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.61 Following clause subsumed by 1545 during input processing: 0 [copy,2136,flip.1] {-} c_Nat_Osize__class_Osize(tc_Complex_Ocomplex,hAPP(hAPP(c_Complex_Ocomplex_OComplex,A),B))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.61 Following clause subsumed by 1546 during input processing: 0 [copy,2137,flip.1] {-} c_Complex_Ocomplex_Ocomplex__rec(A,B,hAPP(hAPP(c_Complex_Ocomplex_OComplex,C),D))=hAPP(hAPP(B,C),D).
% 0.37/0.61 Following clause subsumed by 1547 during input processing: 0 [copy,2138,flip.1] {-} c_Complex_Ocomplex_Ocomplex__case(A,B,hAPP(hAPP(c_Complex_Ocomplex_OComplex,C),D))=hAPP(hAPP(B,C),D).
% 0.37/0.61 Following clause subsumed by 1587 during input processing: 0 [copy,2139,flip.1] {-} hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),B)),C)=hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),B),C)).
% 0.37/0.61 Following clause subsumed by 1592 during input processing: 0 [copy,2140,flip.1] {-} hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat).
% 0.37/0.61 Following clause subsumed by 1603 during input processing: 0 [copy,2144,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),hAPP(hAPP(c_Complex_Ocomplex_OComplex,A),B)),hAPP(hAPP(c_Complex_Ocomplex_OComplex,C),D))=hAPP(hAPP(c_Complex_Ocomplex_OComplex,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),C)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),B),D)).
% 0.37/0.61 Following clause subsumed by 2177 during input processing: 0 [copy,2176,flip.1] {-} hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),A))!=c_Groups_Ozero__class_Ozero(tc_Int_Oint).
% 0.37/0.61 Following clause subsumed by 2176 during input processing: 0 [copy,2177,flip.1] {-} c_Groups_Ozero__class_Ozero(tc_Int_Oint)!=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),A)).
% 0.37/0.61 Following clause subsumed by 1697 during input processing: 0 [copy,2180,flip.1] {-} hAPP(hAPP(c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),hAPP(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal),B)).
% 0.37/0.61 Following clause subsumed by 1704 during input processing: 0 [copy,2181,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B)),C)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),A),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),B),C)).
% 0.37/0.61 Following clause subsumed by 1710 during input processing: 0 [copy,2182,flip.1] {-} hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),hAPP(A,B)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),hAPP(A,C)),hAPP(A,B))),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),C),B))),B))=hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),hAPP(A,C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),hAPP(A,C)),hAPP(A,B))),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal),C),B))),C)).
% 0.37/0.61 Following clause subsumed by 1711 during input processing: 0 [copy,2183,flip.1] {-} c_Divides_Odiv__class_Odiv(tc_Nat_Onat,A,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),B),C))=c_Divides_Odiv__class_Odiv(tc_Nat_Onat,c_Divides_Odiv__class_Odiv(tc_Nat_Onat,A,B),C).
% 0.37/0.61 Following clause subsumed by 1718 during input processing: 0 [copy,2184,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),A),B)),C)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Int_Oint),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),A),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),B),C)).
% 0.37/0.61 Following clause subsumed by 1725 during input processing: 0 [copy,2185,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Int_Oint),A),B)),C)=hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Int_Oint),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),A),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),B),C)).
% 0.37/0.61 Following clause subsumed by 1726 during input processing: 0 [copy,2186,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B)),C)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),B),C)).
% 0.37/0.61 Following clause subsumed by 1732 during input processing: 0 [copy,2187,flip.1] {-} hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),A),B)),C)=hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),A),C)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Nat_Onat),B),C)).
% 0.37/0.61 Following clause subsumed by 1788 during input processing: 0 [copy,2188,flip.1] {-} hAPP(hAPP(c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex),A),B)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),A),hAPP(c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex),B)).
% 0.37/0.61 Following clause subsumed by 2025 during input processing: 0 [copy,2189,flip.1] {-} hAPP(c_COMBC(A,B,C,D,E),F)=hAPP(hAPP(D,F),E).
% 0.37/0.61 Following clause subsumed by 2026 during input processing: 0 [copy,2190,flip.1] {-} hAPP(c_COMBS(A,B,C,D,E),F)=hAPP(hAPP(D,F),hAPP(E,F)).
% 0.37/0.61
% 0.37/0.61 ======= end of input processing =======
% 0.37/0.62
% 0.37/0.62 SEGMENTATION FAULT!! This is probably caused by a
% 0.37/0.62 bug in Otter. Please send copy of the input file to
% 0.37/0.62 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.37/0.62 using, and send any other info that might be useful.
% 0.37/0.62
% 0.37/0.62
% 0.37/0.62 SEGMENTATION FAULT!! This is probably caused by a
% 0.37/0.62 bug in Otter. Please send copy of the input file to
% 0.37/0.62 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.37/0.62 using, and send any other info that might be useful.
% 0.37/0.62
% 0.37/0.62
% 0.37/0.62 The job finished Mon Jun 6 07:02:07 2022
%------------------------------------------------------------------------------