%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NUM926+3 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n029.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 : Mon Jul 18 14:23:18 EDT 2022
% Result : Unknown 0.85s 1.04s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM926+3 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n029.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Thu Jul 7 20:55:14 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.39/0.56 ----- Otter 3.2, August 2001 -----
% 0.39/0.56 The process was started by sandbox2 on n029.cluster.edu,
% 0.39/0.56 Thu Jul 7 20:55:14 2022
% 0.39/0.56 The command was "./sos". The process ID is 4058.
% 0.39/0.56
% 0.39/0.56 set(prolog_style_variables).
% 0.39/0.56 set(auto).
% 0.39/0.56 dependent: set(auto1).
% 0.39/0.56 dependent: set(process_input).
% 0.39/0.56 dependent: clear(print_kept).
% 0.39/0.56 dependent: clear(print_new_demod).
% 0.39/0.56 dependent: clear(print_back_demod).
% 0.39/0.56 dependent: clear(print_back_sub).
% 0.39/0.56 dependent: set(control_memory).
% 0.39/0.56 dependent: assign(max_mem, 12000).
% 0.39/0.56 dependent: assign(pick_given_ratio, 4).
% 0.39/0.56 dependent: assign(stats_level, 1).
% 0.39/0.56 dependent: assign(pick_semantic_ratio, 3).
% 0.39/0.56 dependent: assign(sos_limit, 5000).
% 0.39/0.56 dependent: assign(max_weight, 60).
% 0.39/0.56 clear(print_given).
% 0.39/0.56
% 0.39/0.56 formula_list(usable).
% 0.39/0.56
% 0.39/0.56 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=1, max_lits=10.
% 0.39/0.56
% 0.39/0.56 This ia a non-Horn set with equality. The strategy will be
% 0.39/0.56 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.39/0.56 unit deletion, with positive clauses in sos and nonpositive
% 0.39/0.56 clauses in usable.
% 0.39/0.56
% 0.39/0.56 dependent: set(knuth_bendix).
% 0.39/0.56 dependent: set(para_from).
% 0.39/0.56 dependent: set(para_into).
% 0.39/0.56 dependent: clear(para_from_right).
% 0.39/0.56 dependent: clear(para_into_right).
% 0.39/0.56 dependent: set(para_from_vars).
% 0.39/0.56 dependent: set(eq_units_both_ways).
% 0.39/0.56 dependent: set(dynamic_demod_all).
% 0.39/0.56 dependent: set(dynamic_demod).
% 0.39/0.56 dependent: set(order_eq).
% 0.39/0.56 dependent: set(back_demod).
% 0.39/0.56 dependent: set(lrpo).
% 0.39/0.56 dependent: set(hyper_res).
% 0.39/0.56 dependent: set(unit_deletion).
% 0.39/0.56 dependent: set(factor).
% 0.39/0.56
% 0.39/0.56 There is a clause for symmetry of equality, so it is
% 0.39/0.56 assumed that equality is fully axiomatized; therefore,
% 0.39/0.56 paramodulation is disabled.
% 0.39/0.56
% 0.39/0.56 dependent: clear(para_from).
% 0.39/0.56 dependent: clear(para_into).
% 0.39/0.56
% 0.39/0.56 ------------> process usable:
% 0.39/0.56 Following clause subsumed by 40 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit1(A)),bit1(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.56 Following clause subsumed by 41 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit1(A)),bit1(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.56 Following clause subsumed by 42 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit1(A)),bit1(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.56 Following clause subsumed by 43 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit1(A)),bit1(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.56 Following clause subsumed by 45 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit0(A)),bit0(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.56 Following clause subsumed by 46 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit0(A)),bit0(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.56 Following clause subsumed by 47 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit0(A)),bit0(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.56 Following clause subsumed by 48 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit0(A)),bit0(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.56 Following clause subsumed by 31 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,number_number_of_int(A)),number_number_of_int(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.56 Following clause subsumed by 32 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,number_number_of_int(A)),number_number_of_int(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 35 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,number_number_of_int(A)),number_number_of_int(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.57 Following clause subsumed by 36 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,number_number_of_int(A)),number_number_of_int(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.57 Following clause subsumed by 57 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit1(A)),bit0(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 58 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit1(A)),bit0(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 59 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit0(A)),bit1(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.57 Following clause subsumed by 60 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit0(A)),bit1(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.57 Following clause subsumed by 61 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(A),one_one_int)),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 85 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit1(A)),bit0(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 86 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,bit1(A)),bit0(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 93 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit0(A)),bit1(B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.57 Following clause subsumed by 94 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,bit0(A)),bit1(B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B)).
% 0.39/0.57 Following clause subsumed by 118 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -is_int(C)| -is_int(D)|C=D|A=B|hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),A)),hAPP_int_int(times_times_int(D),B))!=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),B)),hAPP_int_int(times_times_int(D),A)).
% 0.39/0.57 Following clause subsumed by 119 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -is_int(C)| -is_int(D)|C!=D|hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),A)),hAPP_int_int(times_times_int(D),B))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),B)),hAPP_int_int(times_times_int(D),A)).
% 0.39/0.57 Following clause subsumed by 120 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -is_int(C)| -is_int(D)|A!=B|hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),A)),hAPP_int_int(times_times_int(D),B))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),B)),hAPP_int_int(times_times_int(D),A)).
% 0.39/0.57 Following clause subsumed by 121 during input processing: 0 [] {-} A=B|C=D|hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),D))!=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),D)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.39/0.57 Following clause subsumed by 122 during input processing: 0 [] {-} A!=B|hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),D))=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),D)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.39/0.57 Following clause subsumed by 123 during input processing: 0 [] {-} A!=B|hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(C),A)),hAPP_nat_nat(times_times_nat(D),B))=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(C),B)),hAPP_nat_nat(times_times_nat(D),A)).
% 0.39/0.57 Following clause subsumed by 124 during input processing: 0 [] {-} A=B|C=D|hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),C)),hAPP_real_real(times_times_real(B),D))!=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),D)),hAPP_real_real(times_times_real(B),C)).
% 0.39/0.57 Following clause subsumed by 125 during input processing: 0 [] {-} A!=B|hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),C)),hAPP_real_real(times_times_real(B),D))=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),D)),hAPP_real_real(times_times_real(B),C)).
% 0.39/0.57 Following clause subsumed by 126 during input processing: 0 [] {-} A!=B|hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(C),A)),hAPP_real_real(times_times_real(D),B))=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(C),B)),hAPP_real_real(times_times_real(D),A)).
% 0.39/0.57 Following clause subsumed by 129 during input processing: 0 [flip.1] {-} bit1(A)!=pls.
% 0.39/0.57 Following clause subsumed by 127 during input processing: 0 [] {-} -is_int(A)|hAPP_int_int(times_times_int(A),one_one_int)=A.
% 0.39/0.57 Following clause subsumed by 128 during input processing: 0 [] {-} -is_int(A)|hAPP_int_int(times_times_int(one_one_int),A)=A.
% 0.39/0.57 Following clause subsumed by 157 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(power_power_int(A),B)),hAPP_nat_int(power_power_int(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.57 Following clause subsumed by 158 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,one_one_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(power_power_nat(A),B)),hAPP_nat_nat(power_power_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.57 Following clause subsumed by 159 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,one_one_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_nat_real(power_power_real(A),B)),hAPP_nat_real(power_power_real(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.57 Following clause subsumed by 164 during input processing: 0 [] {-} -is_int(A)|A=zero_zero_int|hAPP_nat_int(power_power_int(A),B)!=zero_zero_int.
% 0.39/0.57 Following clause subsumed by 170 during input processing: 0 [] {-} A=zero_zero_real|hAPP_nat_real(power_power_real(A),B)!=zero_zero_real.
% 0.39/0.57 Following clause subsumed by 198 during input processing: 0 [] {-} -is_int(A)|hAPP_int_int(plus_plus_int(zero_zero_int),A)=A.
% 0.39/0.57 Following clause subsumed by 199 during input processing: 0 [] {-} -is_int(A)|hAPP_int_int(plus_plus_int(A),zero_zero_int)=A.
% 0.39/0.57 Following clause subsumed by 27 during input processing: 0 [] {-} -is_int(A)|hAPP_nat_int(power_power_int(A),one_one_nat)=A.
% 0.39/0.57 Following clause subsumed by 170 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))!=zero_zero_real|A=zero_zero_real.
% 0.39/0.57 Following clause subsumed by 164 during input processing: 0 [] {-} -is_int(A)|hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))!=zero_zero_int|A=zero_zero_int.
% 0.39/0.57 Following clause subsumed by 233 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls))))))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),B))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),B)).
% 0.39/0.57 Following clause subsumed by 232 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(power_power_nat(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_nat(power_power_nat(B),number_number_of_nat(bit0(bit1(pls))))))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.39/0.57 Following clause subsumed by 231 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls))))))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 352 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,one_one_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_nat_real(power_power_real(A),B)),hAPP_nat_real(power_power_real(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.39/0.57 Following clause subsumed by 354 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,one_one_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(power_power_nat(A),B)),hAPP_nat_nat(power_power_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.39/0.57 Following clause subsumed by 356 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(power_power_int(A),B)),hAPP_nat_int(power_power_int(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.39/0.57 Following clause subsumed by 353 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,one_one_real),C))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_nat_real(power_power_real(C),A)),hAPP_nat_real(power_power_real(C),B))).
% 0.39/0.57 Following clause subsumed by 355 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,one_one_nat),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(power_power_nat(C),A)),hAPP_nat_nat(power_power_nat(C),B))).
% 0.39/0.57 Following clause subsumed by 357 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),C))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(power_power_int(C),A)),hAPP_nat_int(power_power_int(C),B))).
% 0.39/0.57 Following clause subsumed by 224 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.57 Following clause subsumed by 373 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),B)))|B=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.57 Following clause subsumed by 374 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),B)))|B!=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 224 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.57 Following clause subsumed by 373 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),number_number_of_nat(B))))|number_number_of_nat(B)=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.57 Following clause subsumed by 374 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),number_number_of_nat(B))))|number_number_of_nat(B)!=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 224 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),number_number_of_nat(B))))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.57 Following clause subsumed by 382 during input processing: 0 [flip.1] {-} pls!=min.
% 0.39/0.57 Following clause subsumed by 383 during input processing: 0 [flip.1] {-} bit0(A)!=min.
% 0.39/0.57 Following clause subsumed by 406 during input processing: 0 [] {-} -is_int(A)| -is_int(B)|hAPP_int_int(times_times_int(A),B)!=one_one_int|A=one_one_int|A=number_number_of_int(min).
% 0.39/0.57 Following clause subsumed by 423 during input processing: 0 [flip.1] {-} number_number_of_nat(A)!=zero_zero_nat|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),pls)).
% 0.39/0.57 Following clause subsumed by 424 during input processing: 0 [flip.1] {-} number_number_of_nat(A)=zero_zero_nat| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),pls)).
% 0.39/0.57 Following clause subsumed by 425 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(zcong(A,B),C))| -hBOOL(hAPP_int_bool(zcong(B,A),C)).
% 0.39/0.57 Following clause subsumed by 23 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B))|A=B|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.57 Following clause subsumed by 170 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(A),number_number_of_nat(B))!=zero_zero_real|A=zero_zero_real.
% 0.39/0.57 Following clause subsumed by 171 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(A),number_number_of_nat(B))!=zero_zero_real|number_number_of_nat(B)!=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 172 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(A),number_number_of_nat(B))=zero_zero_real|A!=zero_zero_real|number_number_of_nat(B)=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 167 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),number_number_of_nat(B))!=zero_zero_nat|A=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 168 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),number_number_of_nat(B))!=zero_zero_nat|number_number_of_nat(B)!=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 169 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),number_number_of_nat(B))=zero_zero_nat|A!=zero_zero_nat|number_number_of_nat(B)=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 164 during input processing: 0 [] {-} -is_int(A)|hAPP_nat_int(power_power_int(A),number_number_of_nat(B))!=zero_zero_int|A=zero_zero_int.
% 0.39/0.57 Following clause subsumed by 165 during input processing: 0 [] {-} -is_int(A)|hAPP_nat_int(power_power_int(A),number_number_of_nat(B))!=zero_zero_int|number_number_of_nat(B)!=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 166 during input processing: 0 [] {-} -is_int(A)|hAPP_nat_int(power_power_int(A),number_number_of_nat(B))=zero_zero_int|A!=zero_zero_int|number_number_of_nat(B)=zero_zero_nat.
% 0.39/0.57 Following clause subsumed by 217 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(power_power_int(A),B))).
% 0.39/0.57 Following clause subsumed by 193 during input processing: 0 [] {-} number_number_of_nat(A)!=zero_zero_nat|hAPP_nat_real(power_power_real(zero_zero_real),number_number_of_nat(A))=one_one_real.
% 0.39/0.57 Following clause subsumed by 192 during input processing: 0 [] {-} number_number_of_nat(A)!=zero_zero_nat|hAPP_nat_nat(power_power_nat(zero_zero_nat),number_number_of_nat(A))=one_one_nat.
% 0.39/0.57 Following clause subsumed by 191 during input processing: 0 [] {-} number_number_of_nat(A)!=zero_zero_nat|hAPP_nat_int(power_power_int(zero_zero_int),number_number_of_nat(A))=one_one_int.
% 0.39/0.57 Following clause subsumed by 483 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(zcong(A,zero_zero_int),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,B),A)).
% 0.39/0.57 Following clause subsumed by 484 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(zcong(A,zero_zero_int),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,B),A)).
% 0.39/0.57 Following clause subsumed by 446 during input processing: 0 [] {-} -is_int(A)| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B))| -hBOOL(hAPP_int_bool(zcong(A,zero_zero_int),B))|A=zero_zero_int.
% 0.39/0.57 Following clause subsumed by 487 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(zprime,A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),B))| -hBOOL(hAPP_int_bool(zcong(hAPP_int_int(times_times_int(B),C),zero_zero_int),A))|hBOOL(hAPP_int_bool(zcong(B,zero_zero_int),A))|hBOOL(hAPP_int_bool(zcong(C,zero_zero_int),A)).
% 0.39/0.57 Following clause subsumed by 487 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(zprime,A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),B))|hBOOL(hAPP_int_bool(zcong(B,zero_zero_int),A))|hBOOL(hAPP_int_bool(zcong(C,zero_zero_int),A))| -hBOOL(hAPP_int_bool(zcong(hAPP_int_int(times_times_int(B),C),zero_zero_int),A)).
% 0.39/0.57 Following clause subsumed by 253 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(zprime,A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,A),hAPP_nat_int(power_power_int(B),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),C))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,A),B)).
% 0.39/0.58 Following clause subsumed by 322 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_real|A=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 323 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_real|B=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 324 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls)))))=zero_zero_real|A!=zero_zero_real|B!=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 24 during input processing: 0 [] {-} -is_int(A)| -is_int(B)|A=B|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),A)).
% 0.39/0.58 Following clause subsumed by 429 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),B))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),B))|A=B.
% 0.39/0.58 Following clause subsumed by 503 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),B))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),B)).
% 0.39/0.58 Following clause subsumed by 429 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),B))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),B))|A=B.
% 0.39/0.58 Following clause subsumed by 515 during input processing: 0 [] {-} A=zero_zero_real|B=zero_zero_real|hAPP_real_real(times_times_real(A),B)!=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 516 during input processing: 0 [] {-} A=zero_zero_nat|B=zero_zero_nat|hAPP_nat_nat(times_times_nat(A),B)!=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 517 during input processing: 0 [] {-} -is_int(A)| -is_int(B)|B=zero_zero_int|A=zero_zero_int|hAPP_int_int(times_times_int(B),A)!=zero_zero_int.
% 0.39/0.58 Following clause subsumed by 515 during input processing: 0 [] {-} hAPP_real_real(times_times_real(A),B)!=zero_zero_real|A=zero_zero_real|B=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 517 during input processing: 0 [] {-} -is_int(A)| -is_int(B)|hAPP_int_int(times_times_int(A),B)!=zero_zero_int|A=zero_zero_int|B=zero_zero_int.
% 0.39/0.58 Following clause subsumed by 502 during input processing: 0 [] {-} zero_zero_real!=one_one_real.
% 0.39/0.58 Following clause subsumed by 216 during input processing: 0 [] {-} zero_zero_int!=one_one_int.
% 0.39/0.58 Following clause subsumed by 502 during input processing: 0 [flip.1] {-} zero_zero_real!=one_one_real.
% 0.39/0.58 Following clause subsumed by 522 during input processing: 0 [flip.1] {-} zero_zero_nat!=one_one_nat.
% 0.39/0.58 Following clause subsumed by 216 during input processing: 0 [flip.1] {-} zero_zero_int!=one_one_int.
% 0.39/0.58 Following clause subsumed by 168 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)!=zero_zero_nat|B!=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 167 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)!=zero_zero_nat|A=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 169 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)=zero_zero_nat|B=zero_zero_nat|A!=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 190 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(power_power_nat(A),C)),hAPP_nat_nat(power_power_nat(B),C))).
% 0.39/0.58 Following clause subsumed by 438 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(times_times_int(A),B))).
% 0.39/0.58 Following clause subsumed by 578 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),B))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),C))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(times_times_real(C),A)),hAPP_real_real(times_times_real(C),B))).
% 0.39/0.58 Following clause subsumed by 579 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(C),A)),hAPP_nat_nat(times_times_nat(C),B))).
% 0.39/0.58 Following clause subsumed by 580 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),C))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(times_times_int(C),A)),hAPP_int_int(times_times_int(C),B))).
% 0.39/0.58 Following clause subsumed by 566 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,B),zero_zero_real))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_real_real(times_times_real(A),B))).
% 0.39/0.58 Following clause subsumed by 567 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(times_times_int(A),B))).
% 0.39/0.58 Following clause subsumed by 560 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),B))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(times_times_real(A),B)),zero_zero_real)).
% 0.39/0.58 Following clause subsumed by 562 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),zero_zero_nat))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(A),B)),zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 564 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(times_times_int(A),B)),zero_zero_int)).
% 0.39/0.58 Following clause subsumed by 560 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,B),zero_zero_real))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(times_times_real(B),A)),zero_zero_real)).
% 0.39/0.58 Following clause subsumed by 562 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),zero_zero_nat))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(B),A)),zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 564 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(times_times_int(B),A)),zero_zero_int)).
% 0.39/0.58 Following clause subsumed by 559 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,B),zero_zero_real))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(times_times_real(A),B)),zero_zero_real)).
% 0.39/0.58 Following clause subsumed by 561 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),zero_zero_nat))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(A),B)),zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 563 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(times_times_int(A),B)),zero_zero_int)).
% 0.39/0.58 Following clause subsumed by 565 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),B))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_real_real(times_times_real(A),B))).
% 0.39/0.58 Following clause subsumed by 438 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(times_times_int(A),B))).
% 0.39/0.58 Following clause subsumed by 559 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(times_times_real(A),B)),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,B),zero_zero_real)).
% 0.39/0.58 Following clause subsumed by 560 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(times_times_real(A),B)),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),B)).
% 0.39/0.58 Following clause subsumed by 563 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(times_times_int(A),B)),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B),zero_zero_int)).
% 0.39/0.58 Following clause subsumed by 564 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(times_times_int(A),B)),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B)).
% 0.39/0.58 Following clause subsumed by 565 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_real_real(times_times_real(A),B)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),B)).
% 0.39/0.58 Following clause subsumed by 566 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_real_real(times_times_real(A),B)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,B),zero_zero_real)).
% 0.39/0.58 Following clause subsumed by 438 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(times_times_int(A),B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B)).
% 0.39/0.58 Following clause subsumed by 567 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(times_times_int(A),B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B),zero_zero_int)).
% 0.39/0.58 Following clause subsumed by 260 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),C))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(C),A)),hAPP_int_int(times_times_int(C),B))).
% 0.39/0.58 Following clause subsumed by 605 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),B))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),C))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(C),A)),hAPP_real_real(times_times_real(C),B))).
% 0.39/0.58 Following clause subsumed by 606 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(C),A)),hAPP_nat_nat(times_times_nat(C),B))).
% 0.39/0.58 Following clause subsumed by 260 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),C))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(C),A)),hAPP_int_int(times_times_int(C),B))).
% 0.39/0.58 Following clause subsumed by 601 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),zero_zero_real))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(A),C)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,C),B)).
% 0.39/0.58 Following clause subsumed by 602 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(A),C)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,C),B)).
% 0.39/0.58 Following clause subsumed by 259 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(times_times_int(A),B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),B)).
% 0.39/0.58 Following clause subsumed by 612 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),zero_zero_real))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(B),A)),zero_zero_real)).
% 0.39/0.58 Following clause subsumed by 613 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),zero_zero_nat))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(B),A)),zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 614 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(B),A)),zero_zero_int)).
% 0.39/0.58 Following clause subsumed by 605 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(A),C)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),C)).
% 0.39/0.58 Following clause subsumed by 260 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(A),C)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),C)).
% 0.39/0.58 Following clause subsumed by 605 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(A),C)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),C)).
% 0.39/0.58 Following clause subsumed by 601 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(A),C)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,C),B)).
% 0.39/0.58 Following clause subsumed by 260 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(A),C)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),C)).
% 0.39/0.58 Following clause subsumed by 602 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(A),C)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,C),B)).
% 0.39/0.58 Following clause subsumed by 607 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(C),B)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),B))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),C)).
% 0.39/0.58 Following clause subsumed by 603 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(C),B)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,C),A)).
% 0.39/0.58 Following clause subsumed by 609 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(C),B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),B))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),C)).
% 0.39/0.58 Following clause subsumed by 604 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(C),B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,C),A)).
% 0.39/0.58 Following clause subsumed by 555 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(C),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 607 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(B),A)),hAPP_real_real(times_times_real(C),A)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),C)).
% 0.39/0.58 Following clause subsumed by 625 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),B))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),hAPP_real_real(times_times_real(A),B))).
% 0.39/0.58 Following clause subsumed by 605 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),C))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(A),C))).
% 0.39/0.58 Following clause subsumed by 247 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),A)),hAPP_real_real(times_times_real(B),B))!=zero_zero_real|A=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 248 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),A)),hAPP_real_real(times_times_real(B),B))!=zero_zero_real|B=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 249 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),A)),hAPP_real_real(times_times_real(B),B))=zero_zero_real|A!=zero_zero_real|B!=zero_zero_real.
% 0.39/0.58 Following clause subsumed by 514 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)=one_one_nat|B!=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 676 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 677 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),A)).
% 0.39/0.58 Following clause subsumed by 678 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),A)).
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),A)).
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),A)).
% 0.39/0.58 Following clause subsumed by 507 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|B!=A.
% 0.39/0.58 Following clause subsumed by 508 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A!=B.
% 0.39/0.58 Following clause subsumed by 508 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A!=B.
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,C),A)).
% 0.39/0.58 Following clause subsumed by 500 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A=B.
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A=B.
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|A=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A)).
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A=B.
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|B=A.
% 0.39/0.58 Following clause subsumed by 507 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|B!=A.
% 0.39/0.58 Following clause subsumed by 507 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} A=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A)).
% 0.39/0.58 Following clause subsumed by 508 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A!=B.
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|B=A.
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A))|A=B.
% 0.39/0.58 Following clause subsumed by 507 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|A!=B.
% 0.39/0.58 Following clause subsumed by 507 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 508 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A)).
% 0.39/0.58 Following clause subsumed by 506 during input processing: 0 [] {-} A=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),A)).
% 0.39/0.58 Following clause subsumed by 696 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(minus_minus_nat(B),A)),hAPP_nat_nat(minus_minus_nat(C),A)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.58 Following clause subsumed by 672 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 702 during input processing: 0 [] {-} A!=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.58 Following clause subsumed by 672 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 205 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=A|B=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 692 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),zero_zero_nat))|A!=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 710 during input processing: 0 [] {-} hAPP_nat_nat(minus_minus_nat(A),B)=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 516 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)!=zero_zero_nat|A=zero_zero_nat|B=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 513 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)=zero_zero_nat|A!=zero_zero_nat.
% 0.39/0.58 Following clause subsumed by 676 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.39/0.58 Following clause subsumed by 430 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A=B.
% 0.39/0.58 Following clause subsumed by 430 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A=B.
% 0.39/0.58 Following clause subsumed by 731 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 692 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A!=B.
% 0.39/0.58 Following clause subsumed by 731 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 430 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 731 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 692 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.39/0.58 Following clause subsumed by 749 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 748 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.58 Following clause subsumed by 756 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(plus_plus_nat(C),B)),A)=hAPP_nat_nat(plus_plus_nat(C),hAPP_nat_nat(minus_minus_nat(B),A)).
% 0.39/0.58 Following clause subsumed by 507 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),one_one_nat))|A!=one_one_nat.
% 0.39/0.58 Following clause subsumed by 556 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)!=one_one_nat|A=one_one_nat.
% 0.39/0.58 Following clause subsumed by 557 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)!=one_one_nat|B=one_one_nat.
% 0.39/0.58 Following clause subsumed by 558 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)=one_one_nat|A!=one_one_nat|B!=one_one_nat.
% 0.39/0.58 Following clause subsumed by 556 during input processing: 0 [flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)!=one_one_nat|A=one_one_nat.
% 0.39/0.58 Following clause subsumed by 557 during input processing: 0 [flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)!=one_one_nat|B=one_one_nat.
% 0.39/0.58 Following clause subsumed by 558 during input processing: 0 [flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)=one_one_nat|A!=one_one_nat|B!=one_one_nat.
% 0.39/0.58 Following clause subsumed by 723 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.39/0.58 Following clause subsumed by 724 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),B)).
% 0.39/0.58 Following clause subsumed by 770 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(A,hAPP_nat_nat(minus_minus_nat(B),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C))|hBOOL(hAPP_nat_bool(A,zero_zero_nat)).
% 0.39/0.58 Following clause subsumed by 771 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(A,hAPP_nat_nat(minus_minus_nat(B),C)))|B!=hAPP_nat_nat(plus_plus_nat(C),D)|hBOOL(hAPP_nat_bool(A,D)).
% 0.39/0.58 Following clause subsumed by 606 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(C),A)),hAPP_nat_nat(times_times_nat(C),B))).
% 0.39/0.58 Following clause subsumed by 608 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C))).
% 0.39/0.58 Following clause subsumed by 608 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(C),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.39/0.58 Following clause subsumed by 606 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.39/0.58 Following clause subsumed by 626 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(times_times_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),B)).
% 0.39/0.58 Following clause subsumed by 766 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 767 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(C),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.39/0.59 Following clause subsumed by 713 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)!=hAPP_nat_nat(times_times_nat(A),C)|A=zero_zero_nat|B=C.
% 0.39/0.59 Following clause subsumed by 715 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(A),C)|A!=zero_zero_nat.
% 0.39/0.59 Following clause subsumed by 714 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(A),C)|B!=C.
% 0.39/0.59 Following clause subsumed by 714 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))|hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(A),C)|B!=C.
% 0.39/0.59 Following clause subsumed by 783 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 606 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 554 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 789 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 554 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 790 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 766 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 187 during input processing: 0 [] {-} -is_int(A)|A=zero_zero_int|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,B),C))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(A),C))).
% 0.39/0.59 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),hAPP_int_int(minus_minus_int(B),one_one_int)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)).
% 0.39/0.59 Following clause subsumed by 436 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(zcong(A,hAPP_int_int(times_times_int(B),multInv(C,D))),C))|hBOOL(hAPP_int_bool(zcong(hAPP_int_int(times_times_int(A),D),hAPP_int_int(times_times_int(hAPP_int_int(times_times_int(B),multInv(C,D))),D)),C)).
% 0.39/0.59 Following clause subsumed by 189 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,hAPP_nat_int(power_power_int(B),A)),hAPP_nat_int(power_power_int(C),A)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,B),C)).
% 0.39/0.59 Following clause subsumed by 524 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,zero_zero_nat),A))|A=zero_zero_nat.
% 0.39/0.59 Following clause subsumed by 524 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,zero_zero_nat),A))|A=zero_zero_nat.
% 0.39/0.59 Following clause subsumed by 508 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,zero_zero_nat),A))|A!=zero_zero_nat.
% 0.39/0.59 Following clause subsumed by 524 during input processing: 0 [] {-} A=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,zero_zero_nat),A)).
% 0.39/0.59 Following clause subsumed by 508 during input processing: 0 [] {-} A!=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),zero_zero_nat))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,zero_zero_nat),A)).
% 0.39/0.59 Following clause subsumed by 764 during input processing: 0 [] {-} A=one_one_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),one_one_nat)).
% 0.39/0.59 Following clause subsumed by 507 during input processing: 0 [] {-} A!=one_one_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,one_one_nat),A))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),one_one_nat)).
% 0.39/0.59 Following clause subsumed by 764 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),one_one_nat))|A=one_one_nat.
% 0.39/0.59 Following clause subsumed by 507 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),one_one_nat))|A!=one_one_nat.
% 0.39/0.59 Following clause subsumed by 764 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),one_one_nat))|A=one_one_nat.
% 0.39/0.59 Following clause subsumed by 659 during input processing: 0 [] {-} A=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(power_power_nat(B),A)),hAPP_nat_nat(power_power_nat(C),A)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 190 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,hAPP_nat_nat(power_power_nat(B),A)),hAPP_nat_nat(power_power_nat(C),A)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,B),C)).
% 0.39/0.59 Following clause subsumed by 897 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,hAPP_nat_int(power_power_int(A),B)),hAPP_nat_int(power_power_int(C),B)))|B=zero_zero_nat|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(dvd_dvd_int,A),C)).
% 0.39/0.59 Following clause subsumed by 650 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|B=zero_zero_nat.
% 0.39/0.59 Following clause subsumed by 797 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))|hAPP_nat_nat(times_times_nat(A),B)!=hAPP_nat_nat(times_times_nat(A),C)|B=C.
% 0.39/0.59 Following clause subsumed by 917 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))|hBOOL(hAPP_int_bool(zcong(B,C),A))|hAPP_int_int(div_mod_int(B),A)!=hAPP_int_int(div_mod_int(C),A).
% 0.39/0.59 Following clause subsumed by 924 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(div_mod_int(B),A))).
% 0.39/0.59 Following clause subsumed by 908 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),A))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(div_mod_int(B),A)),A)).
% 0.39/0.59 Following clause subsumed by 926 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(div_mod_int(B),A)),zero_zero_int)).
% 0.59/0.79 Following clause subsumed by 907 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),hAPP_int_int(div_mod_int(B),A))).
% 0.59/0.79 Following clause subsumed by 1076 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|hAPP_nat_nat(div_mod_nat(A),B)=A.
% 0.59/0.79 Following clause subsumed by 1079 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(zcong(A,zero_zero_int),B))|standardRes(B,A)!=zero_zero_int.
% 0.59/0.79 Following clause subsumed by 1080 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(zcong(A,zero_zero_int),B))|standardRes(B,A)=zero_zero_int.
% 0.59/0.79 Following clause subsumed by 131 during input processing: 0 [copy,130,flip.1] {-} bit0(A)!=bit1(B).
% 0.59/0.79 Following clause subsumed by 130 during input processing: 0 [copy,131,flip.1] {-} bit1(A)!=bit0(B).
% 0.59/0.79 410 back subsumes 289.
% 0.59/0.79 485 back subsumes 453.
% 0.59/0.79 514 back subsumes 192.
% 0.59/0.79 672 back subsumes 623.
% 0.59/0.79 672 back subsumes 613.
% 0.59/0.79 685 back subsumes 684.
% 0.59/0.79 685 back subsumes 681.
% 0.59/0.79 686 back subsumes 683.
% 0.59/0.79 686 back subsumes 682.
% 0.59/0.79 724 back subsumes 648.
% 0.59/0.79 734 back subsumes 733.
% 0.59/0.79 765 back subsumes 572.
% 0.59/0.79 765 back subsumes 569.
% 0.59/0.79 766 back subsumes 579.
% 0.59/0.79 767 back subsumes 582.
% 0.59/0.79 784 back subsumes 618.
% 0.59/0.79 785 back subsumes 621.
% 0.59/0.79 1106 back subsumes 1105.
% 0.59/0.79 1198 back subsumes 1181.
% 0.59/0.79 1200 back subsumes 1103.
% 0.59/0.79 1272 back subsumes 1262.
% 0.59/0.79 1275 back subsumes 1267.
% 0.59/0.79 1311 back subsumes 1232.
% 0.59/0.79 1311 back subsumes 1231.
% 0.59/0.79 1311 back subsumes 1230.
% 0.59/0.79 1311 back subsumes 1225.
% 0.59/0.79 1311 back subsumes 1224.
% 0.59/0.79 1311 back subsumes 1220.
% 0.59/0.79 1311 back subsumes 1218.
% 0.59/0.79 1311 back subsumes 1215.
% 0.59/0.79 1311 back subsumes 1209.
% 0.59/0.79 1311 back subsumes 1207.
% 0.59/0.79 1311 back subsumes 1149.
% 0.59/0.79 Following clause subsumed by 1098 during input processing: 0 [copy,1515,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls)))))!=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int).
% 0.59/0.79
% 0.59/0.79 ------------> process sos:
% 0.59/0.79 Following clause subsumed by 1661 during input processing: 0 [] {-} hAPP_nat_int(power_power_int(hAPP_nat_int(power_power_int(A),B)),C)=hAPP_nat_int(power_power_int(A),hAPP_nat_nat(times_times_nat(B),C)).
% 0.59/0.79 Following clause subsumed by 1659 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),pls)).
% 0.59/0.79 Following clause subsumed by 1710 during input processing: 0 [demod,1704] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),C))=hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),C)).
% 0.59/0.79 Following clause subsumed by 1718 during input processing: 0 [] {-} hAPP_int_int(times_times_int(A),B)=hAPP_int_int(times_times_int(B),A).
% 0.59/0.79 Following clause subsumed by 1736 during input processing: 0 [demod,1730] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C)).
% 0.59/0.79 Following clause subsumed by 1741 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(plus_plus_int(B),hAPP_int_int(plus_plus_int(A),C)).
% 0.59/0.79 Following clause subsumed by 1744 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(A),B)=hAPP_int_int(plus_plus_int(B),A).
% 0.59/0.79 Following clause subsumed by 1638 during input processing: 0 [] {-} hAPP_nat_int(power_power_int(A),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),B))=hAPP_nat_int(power_power_int(hAPP_nat_int(power_power_int(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.59/0.79 Following clause subsumed by 1640 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(A),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),B))=hAPP_nat_real(power_power_real(hAPP_nat_real(power_power_real(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.59/0.79 Following clause subsumed by 1642 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),B))=hAPP_nat_nat(power_power_nat(hAPP_nat_nat(power_power_nat(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.59/0.79 Following clause subsumed by 1750 during input processing: 0 [] {-} hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(A),B)),C)=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),C)),hAPP_int_int(times_times_int(B),C)).
% 0.59/0.79 Following clause subsumed by 1750 during input processing: 0 [] {-} hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_int(C))=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),number_number_of_int(C))),hAPP_int_int(times_times_int(B),number_number_of_int(C))).
% 0.59/0.79 Following clause subsumed by 1751 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(A),B)),number_number_of_nat(C))=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),number_number_of_nat(C))),hAPP_nat_nat(times_times_nat(B),number_number_of_nat(C))).
% 0.59/0.79 Following clause subsumed by 1752 during input processing: 0 [] {-} hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(A),B)),number267125858f_real(C))=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),number267125858f_real(C))),hAPP_real_real(times_times_real(B),number267125858f_real(C))).
% 0.59/0.79 Following clause subsumed by 1784 during input processing: 0 [demod,1755] {-} hAPP_int_int(times_times_int(number_number_of_int(A)),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(times_times_int(number_number_of_int(A)),hAPP_int_int(plus_plus_int(B),C)).
% 0.59/0.79 Following clause subsumed by 1782 during input processing: 0 [] {-} hAPP_int_int(times_times_int(number_number_of_int(A)),number_number_of_int(B))=number_number_of_int(hAPP_int_int(times_times_int(A),B)).
% 0.59/0.79 Following clause subsumed by 1785 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(number_number_of_int(A)),number_number_of_int(B))=number_number_of_int(hAPP_int_int(plus_plus_int(A),B)).
% 0.59/0.79 Following clause subsumed by 1686 during input processing: 0 [demod,1684] {-} one_one_nat=one_one_nat.
% 0.59/0.79 Following clause subsumed by 1843 during input processing: 0 [demod,1839] {-} one_one_int=one_one_int.
% 0.59/0.79 Following clause subsumed by 1845 during input processing: 0 [demod,1841] {-} one_one_real=one_one_real.
% 0.59/0.79 Following clause subsumed by 1843 during input processing: 0 [demod,1839] {-} one_one_int=one_one_int.
% 0.59/0.79 Following clause subsumed by 1677 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),A)=hAPP_nat_nat(plus_plus_nat(A),A).
% 0.59/0.79 Following clause subsumed by 1863 during input processing: 0 [demod,1781] {-} hAPP_int_int(times_times_int(number_number_of_int(bit0(bit1(pls)))),A)=bit0(A).
% 0.59/0.79 Following clause subsumed by 1864 during input processing: 0 [] {-} hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),A)=hAPP_real_real(plus_plus_real(A),A).
% 0.59/0.79 Following clause subsumed by 1745 during input processing: 0 [demod,1679] {-} hAPP_nat_nat(plus_plus_nat(A),A)=hAPP_nat_nat(plus_plus_nat(A),A).
% 0.59/0.79 Following clause subsumed by 1746 during input processing: 0 [demod,1869] {-} hAPP_real_real(plus_plus_real(A),A)=hAPP_real_real(plus_plus_real(A),A).
% 0.59/0.79 Following clause subsumed by 1933 during input processing: 0 [demod,1928,1925] {-} pls=pls.
% 0.59/0.79 Following clause subsumed by 1935 during input processing: 0 [demod,1931] {-} zero_zero_real=zero_zero_real.
% 0.59/0.79 Following clause subsumed by 1933 during input processing: 0 [demod,1925,1928] {-} pls=pls.
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1667] {-} A=A.
% 0.59/0.79 Following clause subsumed by 1719 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(power_power_nat(A),B)),A)=hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(power_power_nat(A),B)).
% 0.59/0.79 Following clause subsumed by 1720 during input processing: 0 [] {-} hAPP_real_real(times_times_real(hAPP_nat_real(power_power_real(A),B)),A)=hAPP_real_real(times_times_real(A),hAPP_nat_real(power_power_real(A),B)).
% 0.59/0.79 Following clause subsumed by 1718 during input processing: 0 [] {-} hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),B)),A)=hAPP_int_int(times_times_int(A),hAPP_nat_int(power_power_int(A),B)).
% 0.59/0.79 Following clause subsumed by 1772 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(hAPP_nat_nat(times_times_nat(A),B)),C)=hAPP_nat_nat(times_times_nat(hAPP_nat_nat(power_power_nat(A),C)),hAPP_nat_nat(power_power_nat(B),C)).
% 0.59/0.79 Following clause subsumed by 1771 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(hAPP_real_real(times_times_real(A),B)),C)=hAPP_real_real(times_times_real(hAPP_nat_real(power_power_real(A),C)),hAPP_nat_real(power_power_real(B),C)).
% 0.59/0.79 Following clause subsumed by 1770 during input processing: 0 [] {-} hAPP_nat_int(power_power_int(hAPP_int_int(times_times_int(A),B)),C)=hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),C)),hAPP_nat_int(power_power_int(B),C)).
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1675] {-} hAPP_nat_nat(power_power_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(power_power_nat(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1673] {-} hAPP_nat_real(power_power_real(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_real(power_power_real(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.59/0.79 Following clause subsumed by 1676 during input processing: 0 [] {-} hAPP_nat_int(power_power_int(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),B)),hAPP_nat_int(power_power_int(A),C)).
% 0.59/0.79 Following clause subsumed by 1943 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls))))))).
% 0.59/0.79 Following clause subsumed by 1941 during input processing: 0 [demod,1925] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls))))))).
% 0.59/0.79 Following clause subsumed by 1945 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls)))))))|A=zero_zero_real.
% 0.59/0.79 Following clause subsumed by 1947 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls)))))))|B=zero_zero_real.
% 0.59/0.79 Following clause subsumed by 1659 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,min),min)).
% 0.59/0.79 Following clause subsumed by 1965 during input processing: 0 [demod,1628] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))))|A=zero_zero_real.
% 0.59/0.79 Following clause subsumed by 1987 during input processing: 0 [demod,1925] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,min),pls)).
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1990] {-} one_one_real=one_one_real.
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1992] {-} one_one_nat=one_one_nat.
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1994] {-} one_one_int=one_one_int.
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1937] {-} zero_zero_nat=zero_zero_nat.
% 0.59/0.79 Following clause subsumed by 1954 during input processing: 0 [demod,1937] {-} zero_zero_nat=zero_zero_nat.
% 0.59/0.79 Following clause subsumed by 1659 during input processing: 0 [demod,1925,1925] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),pls)).
% 0.59/0.80 Following clause subsumed by 1902 during input processing: 0 [] {-} number_number_of_nat(A)=zero_zero_nat|hAPP_nat_real(power_power_real(zero_zero_real),number_number_of_nat(A))=zero_zero_real.
% 0.59/0.80 Following clause subsumed by 1901 during input processing: 0 [] {-} number_number_of_nat(A)=zero_zero_nat|hAPP_nat_nat(power_power_nat(zero_zero_nat),number_number_of_nat(A))=zero_zero_nat.
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,2024] {-} hAPP_int_int(times_times_int(number_number_of_int(A)),hAPP_int_int(minus_minus_int(B),C))=hAPP_int_int(times_times_int(number_number_of_int(A)),hAPP_int_int(minus_minus_int(B),C)).
% 0.59/0.80 Following clause subsumed by 2025 during input processing: 0 [] {-} hAPP_int_int(times_times_int(hAPP_int_int(minus_minus_int(A),B)),number_number_of_int(C))=hAPP_int_int(minus_minus_int(hAPP_int_int(times_times_int(A),number_number_of_int(C))),hAPP_int_int(times_times_int(B),number_number_of_int(C))).
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1708] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),C))=hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),C)).
% 0.59/0.80 Following clause subsumed by 1720 during input processing: 0 [] {-} hAPP_real_real(times_times_real(A),B)=hAPP_real_real(times_times_real(B),A).
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1769] {-} A=A.
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1914] {-} zero_zero_real=zero_zero_real.
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1912] {-} zero_zero_nat=zero_zero_nat.
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1908] {-} zero_zero_real=zero_zero_real.
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1906] {-} zero_zero_nat=zero_zero_nat.
% 0.59/0.80 Following clause subsumed by 1954 during input processing: 0 [demod,1925,1776,1925] {-} pls=pls.
% 0.59/0.80 Following clause subsumed by 1752 during input processing: 0 [] {-} hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(A),B)),C)=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),C)),hAPP_real_real(times_times_real(B),C)).
% 0.59/0.80 Following clause subsumed by 1751 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(A),B)),C)=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.59/0.80 Following clause subsumed by 1750 during input processing: 0 [] {-} hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(A),B)),C)=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),C)),hAPP_int_int(times_times_int(B),C)).
% 0.59/0.80 Following clause subsumed by 1752 during input processing: 0 [] {-} hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(A),B)),C)=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),C)),hAPP_real_real(times_times_real(B),C)).
% 0.59/0.80 Following clause subsumed by 1962 during input processing: 0 [demod,1628] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls)))))).
% 0.59/0.80 Following clause subsumed by 1964 during input processing: 0 [demod,1925,1626] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls)))))).
% 0.59/0.80 Following clause subsumed by 2067 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),A)).
% 0.59/0.80 Following clause subsumed by 2111 during input processing: 0 [] {-} A=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),A)).
% 0.59/0.80 Following clause subsumed by 2111 during input processing: 0 [] {-} A=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),A)).
% 0.59/0.80 Following clause subsumed by 1745 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(B),A).
% 0.59/0.83 Following clause subsumed by 1742 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(plus_plus_nat(B),hAPP_nat_nat(plus_plus_nat(A),C)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1732] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1706] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),C)).
% 0.59/0.83 Following clause subsumed by 1719 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(B),A).
% 0.59/0.83 Following clause subsumed by 2128 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1920] {-} A=A.
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1916] {-} A=A.
% 0.59/0.83 Following clause subsumed by 2100 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),A)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1906] {-} zero_zero_nat=zero_zero_nat.
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1912] {-} zero_zero_nat=zero_zero_nat.
% 0.59/0.83 Following clause subsumed by 1751 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(A),B)),C)=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1758] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1763] {-} A=A.
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,1767] {-} A=A.
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,2084] {-} hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(C),B)),D))=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(C),B)),D)).
% 0.59/0.83 Following clause subsumed by 1659 during input processing: 0 [demod,1925,1928] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),pls)).
% 0.59/0.83 Following clause subsumed by 2062 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),zero_zero_nat)).
% 0.59/0.83 Following clause subsumed by 2062 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,A),zero_zero_nat)).
% 0.59/0.83 Following clause subsumed by 2097 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,one_one_nat),A)).
% 0.59/0.83 Following clause subsumed by 2097 during input processing: 0 [] {-} A=one_one_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(dvd_dvd_nat,one_one_nat),A)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [demod,2158] {-} hAPP_int_int(div_mod_int(hAPP_int_int(times_times_int(A),B)),C)=hAPP_int_int(div_mod_int(hAPP_int_int(times_times_int(A),B)),C).
% 0.59/0.83 Following clause subsumed by 2177 during input processing: 0 [flip.2] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|hAPP_nat_nat(div_mod_nat(hAPP_nat_nat(minus_minus_nat(A),B)),B)=hAPP_nat_nat(div_mod_nat(A),B).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [] {-} A=A.
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1632,flip.1] {-} hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))=hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls)))).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1634,flip.1] {-} hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))=hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls)))).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1636,flip.1] {-} hAPP_nat_nat(power_power_nat(A),number_number_of_nat(bit0(bit1(pls))))=hAPP_nat_nat(power_power_nat(A),number_number_of_nat(bit0(bit1(pls)))).
% 0.59/0.83 1659 back subsumes 1385.
% 0.59/0.83 1659 back subsumes 1384.
% 0.59/0.83 1659 back subsumes 1383.
% 0.59/0.83 1659 back subsumes 1382.
% 0.59/0.83 1659 back subsumes 1298.
% 0.59/0.83 1659 back subsumes 1297.
% 0.59/0.83 1659 back subsumes 1294.
% 0.59/0.83 1659 back subsumes 1291.
% 0.59/0.83 1659 back subsumes 1233.
% 0.59/0.83 1659 back subsumes 1200.
% 0.59/0.83 1659 back subsumes 1154.
% 0.59/0.83 1660 back subsumes 600.
% 0.59/0.83 1660 back subsumes 597.
% 0.59/0.83 1660 back subsumes 592.
% 0.59/0.83 1660 back subsumes 589.
% 0.59/0.83 1660 back subsumes 431.
% 0.59/0.83 Following clause subsumed by 1974 during input processing: 0 [copy,1661,flip.1] {-} hAPP_nat_int(power_power_int(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_int(power_power_int(hAPP_nat_int(power_power_int(A),B)),C).
% 0.59/0.83 Following clause subsumed by 1973 during input processing: 0 [copy,1662,flip.1] {-} hAPP_nat_real(power_power_real(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_real(power_power_real(hAPP_nat_real(power_power_real(A),B)),C).
% 0.59/0.83 Following clause subsumed by 1972 during input processing: 0 [copy,1663,flip.1] {-} hAPP_nat_nat(power_power_nat(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_nat(power_power_nat(hAPP_nat_nat(power_power_nat(A),B)),C).
% 0.59/0.83 Following clause subsumed by 1676 during input processing: 0 [copy,1671,flip.1] {-} hAPP_nat_int(power_power_int(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),B)),hAPP_nat_int(power_power_int(A),C)).
% 0.59/0.83 Following clause subsumed by 1671 during input processing: 0 [copy,1676,flip.1] {-} hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),B)),hAPP_nat_int(power_power_int(A),C))=hAPP_nat_int(power_power_int(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.59/0.83 Following clause subsumed by 1800 during input processing: 0 [copy,1677,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),A)=hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),A).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1686,flip.1] {-} one_one_nat=one_one_nat.
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1710,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),C))=hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),C)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1712,flip.1] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),C)).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1714,flip.1] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),C))=hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),C)).
% 0.59/0.83 Following clause subsumed by 1715 during input processing: 0 [copy,1715,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),C))=hAPP_int_int(times_times_int(B),hAPP_int_int(times_times_int(A),C)).
% 0.59/0.83 Following clause subsumed by 1716 during input processing: 0 [copy,1716,flip.1] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_nat(times_times_nat(B),hAPP_nat_nat(times_times_nat(A),C)).
% 0.59/0.83 Following clause subsumed by 1717 during input processing: 0 [copy,1717,flip.1] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),C))=hAPP_real_real(times_times_real(B),hAPP_real_real(times_times_real(A),C)).
% 0.59/0.83 Following clause subsumed by 1718 during input processing: 0 [copy,1718,flip.1] {-} hAPP_int_int(times_times_int(A),B)=hAPP_int_int(times_times_int(B),A).
% 0.59/0.83 Following clause subsumed by 1719 during input processing: 0 [copy,1719,flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(B),A).
% 0.59/0.83 Following clause subsumed by 1720 during input processing: 0 [copy,1720,flip.1] {-} hAPP_real_real(times_times_real(A),B)=hAPP_real_real(times_times_real(B),A).
% 0.59/0.83 Following clause subsumed by 1954 during input processing: 0 [copy,1736,flip.1] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C)).
% 0.66/0.84 Following clause subsumed by 1954 during input processing: 0 [copy,1738,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.66/0.84 Following clause subsumed by 1954 during input processing: 0 [copy,1740,flip.1] {-} hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(B),C))=hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(B),C)).
% 0.66/0.84 Following clause subsumed by 1741 during input processing: 0 [copy,1741,flip.1] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(plus_plus_int(B),hAPP_int_int(plus_plus_int(A),C)).
% 0.66/0.84 Following clause subsumed by 1742 during input processing: 0 [copy,1742,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(plus_plus_nat(B),hAPP_nat_nat(plus_plus_nat(A),C)).
% 0.66/0.84 Following clause subsumed by 1743 during input processing: 0 [copy,1743,flip.1] {-} hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(B),C))=hAPP_real_real(plus_plus_real(B),hAPP_real_real(plus_plus_real(A),C)).
% 0.66/0.84 Following clause subsumed by 1744 during input processing: 0 [copy,1744,flip.1] {-} hAPP_int_int(plus_plus_int(A),B)=hAPP_int_int(plus_plus_int(B),A).
% 0.66/0.84 1744 back subsumes 1533.
% 0.66/0.84 1744 back subsumes 1527.
% 0.66/0.84 1744 back subsumes 1133.
% 0.66/0.84 1744 back subsumes 1127.
% 0.66/0.84 Following clause subsumed by 1745 during input processing: 0 [copy,1745,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(B),A).
% 0.66/0.84 Following clause subsumed by 1746 during input processing: 0 [copy,1746,flip.1] {-} hAPP_real_real(plus_plus_real(A),B)=hAPP_real_real(plus_plus_real(B),A).
% 0.66/0.84 Following clause subsumed by 1750 during input processing: 0 [copy,1747,flip.1] {-} hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(A),B)),C)=hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),C)),hAPP_int_int(times_times_int(B),C)).
% 0.66/0.84 Following clause subsumed by 1751 during input processing: 0 [copy,1748,flip.1] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(A),B)),C)=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.66/0.84 Following clause subsumed by 1752 during input processing: 0 [copy,1749,flip.1] {-} hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(A),B)),C)=hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),C)),hAPP_real_real(times_times_real(B),C)).
% 0.66/0.84 Following clause subsumed by 1747 during input processing: 0 [copy,1750,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),B)),hAPP_int_int(times_times_int(C),B))=hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(A),C)),B).
% 0.66/0.84 Following clause subsumed by 1748 during input processing: 0 [copy,1751,flip.1] {-} hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),B)),hAPP_nat_nat(times_times_nat(C),B))=hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(A),C)),B).
% 0.66/0.84 Following clause subsumed by 1749 during input processing: 0 [copy,1752,flip.1] {-} hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),B)),hAPP_real_real(times_times_real(C),B))=hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(A),C)),B).
% 0.66/0.84 Following clause subsumed by 1814 during input processing: 0 [copy,1782,flip.1] {-} number_number_of_int(hAPP_int_int(times_times_int(A),B))=hAPP_int_int(times_times_int(number_number_of_int(A)),number_number_of_int(B)).
% 0.66/0.84 1782 back subsumes 140.
% 0.66/0.84 Following clause subsumed by 1954 during input processing: 0 [copy,1784,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(times_times_int(A),hAPP_int_int(plus_plus_int(B),C)).
% 0.66/0.84 Following clause subsumed by 1823 during input processing: 0 [copy,1785,flip.1] {-} number_number_of_int(hAPP_int_int(plus_plus_int(A),B))=hAPP_int_int(plus_plus_int(number_number_of_int(A)),number_number_of_int(B)).
% 0.66/0.84 1785 back subsumes 143.
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1788,flip.1] {-} hAPP_nat_nat(times_times_nat(number_number_of_nat(A)),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(times_times_nat(number_number_of_nat(A)),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1790,flip.1] {-} hAPP_real_real(times_times_real(number267125858f_real(A)),hAPP_real_real(plus_plus_real(B),C))=hAPP_real_real(times_times_real(number267125858f_real(A)),hAPP_real_real(plus_plus_real(B),C)).
% 0.75/0.95 Following clause subsumed by 1677 during input processing: 0 [copy,1800,flip.1] {-} hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),A)=hAPP_nat_nat(plus_plus_nat(A),A).
% 0.75/0.95 Following clause subsumed by 1864 during input processing: 0 [copy,1802,flip.1] {-} hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),A)=hAPP_real_real(plus_plus_real(A),A).
% 0.75/0.95 Following clause subsumed by 1815 during input processing: 0 [copy,1813,flip.1] {-} number267125858f_real(hAPP_int_int(times_times_int(A),B))=hAPP_real_real(times_times_real(number267125858f_real(A)),number267125858f_real(B)).
% 0.75/0.95 1813 back subsumes 142.
% 0.75/0.95 Following clause subsumed by 1782 during input processing: 0 [copy,1814,flip.1] {-} hAPP_int_int(times_times_int(number_number_of_int(A)),number_number_of_int(B))=number_number_of_int(hAPP_int_int(times_times_int(A),B)).
% 0.75/0.95 Following clause subsumed by 1813 during input processing: 0 [copy,1815,flip.1] {-} hAPP_real_real(times_times_real(number267125858f_real(A)),number267125858f_real(B))=number267125858f_real(hAPP_int_int(times_times_int(A),B)).
% 0.75/0.95 Following clause subsumed by 1824 during input processing: 0 [copy,1822,flip.1] {-} number267125858f_real(hAPP_int_int(plus_plus_int(A),B))=hAPP_real_real(plus_plus_real(number267125858f_real(A)),number267125858f_real(B)).
% 0.75/0.95 1822 back subsumes 145.
% 0.75/0.95 Following clause subsumed by 1785 during input processing: 0 [copy,1823,flip.1] {-} hAPP_int_int(plus_plus_int(number_number_of_int(A)),number_number_of_int(B))=number_number_of_int(hAPP_int_int(plus_plus_int(A),B)).
% 0.75/0.95 Following clause subsumed by 1822 during input processing: 0 [copy,1824,flip.1] {-} hAPP_real_real(plus_plus_real(number267125858f_real(A)),number267125858f_real(B))=number267125858f_real(hAPP_int_int(plus_plus_int(A),B)).
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1843,flip.1] {-} one_one_int=one_one_int.
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1845,flip.1] {-} one_one_real=one_one_real.
% 0.75/0.95 Following clause subsumed by 1798 during input processing: 0 [copy,1863,flip.1,demod,1874] {-} bit0(A)=hAPP_int_int(times_times_int(bit0(one_one_int)),A).
% 0.75/0.95 Following clause subsumed by 1802 during input processing: 0 [copy,1864,flip.1] {-} hAPP_real_real(plus_plus_real(A),A)=hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),A).
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1871,flip.1] {-} bit0(A)=bit0(A).
% 0.75/0.95 1871 back subsumes 1116.
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1876,flip.1] {-} number_number_of_nat(bit0(bit1(pls)))=number_number_of_nat(bit0(bit1(pls))).
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1878,flip.1] {-} number267125858f_real(bit0(bit1(pls)))=number267125858f_real(bit0(bit1(pls))).
% 0.75/0.95 Following clause subsumed by 2198 during input processing: 0 [copy,1885,flip.1] {-} hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls))))),hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),hAPP_real_real(times_times_real(A),B))))=hAPP_nat_real(power_power_real(hAPP_real_real(plus_plus_real(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1933,flip.1] {-} pls=pls.
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1935,flip.1] {-} zero_zero_real=zero_zero_real.
% 0.75/0.95 Following clause subsumed by 1954 during input processing: 0 [copy,1954,flip.1] {-} A=A.
% 0.75/0.95 1954 back subsumes 1935.
% 0.75/0.95 1954 back subsumes 1933.
% 0.75/0.95 1954 back subsumes 1878.
% 0.75/0.95 1954 back subsumes 1876.
% 0.78/0.96 1954 back subsumes 1871.
% 0.78/0.96 1954 back subsumes 1845.
% 0.78/0.96 1954 back subsumes 1843.
% 0.78/0.96 1954 back subsumes 1790.
% 0.78/0.96 1954 back subsumes 1788.
% 0.78/0.96 1954 back subsumes 1784.
% 0.78/0.96 1954 back subsumes 1740.
% 0.78/0.96 1954 back subsumes 1738.
% 0.78/0.96 1954 back subsumes 1736.
% 0.78/0.96 1954 back subsumes 1714.
% 0.78/0.96 1954 back subsumes 1712.
% 0.78/0.96 1954 back subsumes 1710.
% 0.78/0.96 1954 back subsumes 1686.
% 0.78/0.96 1954 back subsumes 1636.
% 0.78/0.96 1954 back subsumes 1634.
% 0.78/0.96 1954 back subsumes 1632.
% 0.78/0.96 1954 back subsumes 1380.
% 0.78/0.96 1954 back subsumes 1339.
% 0.78/0.96 1954 back subsumes 1338.
% 0.78/0.96 1954 back subsumes 1337.
% 0.78/0.96 1954 back subsumes 1334.
% 0.78/0.96 1954 back subsumes 1333.
% 0.78/0.96 1954 back subsumes 1240.
% 0.78/0.96 1954 back subsumes 1183.
% 0.78/0.96 1954 back subsumes 1182.
% 0.78/0.96 1954 back subsumes 1148.
% 0.78/0.96 1954 back subsumes 1147.
% 0.78/0.96 1954 back subsumes 1136.
% 0.78/0.96 1954 back subsumes 1130.
% 0.78/0.96 1954 back subsumes 1123.
% 0.78/0.96 1954 back subsumes 1115.
% 0.78/0.96 1954 back subsumes 1114.
% 0.78/0.96 1954 back subsumes 1113.
% 0.78/0.96 1954 back subsumes 1112.
% 0.78/0.96 1954 back subsumes 1111.
% 0.78/0.96 1954 back subsumes 1110.
% 0.78/0.96 1954 back subsumes 1109.
% 0.78/0.96 1954 back subsumes 1107.
% 0.78/0.96 1954 back subsumes 1106.
% 0.78/0.96 Following clause subsumed by 1663 during input processing: 0 [copy,1972,flip.1] {-} hAPP_nat_nat(power_power_nat(hAPP_nat_nat(power_power_nat(A),B)),C)=hAPP_nat_nat(power_power_nat(A),hAPP_nat_nat(times_times_nat(B),C)).
% 0.78/0.96 Following clause subsumed by 1662 during input processing: 0 [copy,1973,flip.1] {-} hAPP_nat_real(power_power_real(hAPP_nat_real(power_power_real(A),B)),C)=hAPP_nat_real(power_power_real(A),hAPP_nat_nat(times_times_nat(B),C)).
% 0.78/0.96 Following clause subsumed by 1661 during input processing: 0 [copy,1974,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_nat_int(power_power_int(A),B)),C)=hAPP_nat_int(power_power_int(A),hAPP_nat_nat(times_times_nat(B),C)).
% 0.78/0.96 2062 back subsumes 898.
% 0.78/0.96 2097 back subsumes 899.
% 0.78/0.96 2100 back subsumes 584.
% 0.78/0.96 2100 back subsumes 218.
% 0.78/0.96 Following clause subsumed by 2101 during input processing: 0 [copy,2101,flip.1] {-} hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(minus_minus_nat(A),B)),C)=hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(minus_minus_nat(A),C)),B).
% 0.78/0.96 2102 back subsumes 1156.
% 0.78/0.96 2103 back subsumes 596.
% 0.78/0.96 2103 back subsumes 593.
% 0.78/0.96 2103 back subsumes 588.
% 0.78/0.96 2103 back subsumes 585.
% 0.78/0.96 2121 back subsumes 1341.
% 0.78/0.96 2121 back subsumes 1155.
% 0.78/0.96 Following clause subsumed by 2301 during input processing: 0 [copy,2194,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(times_times_int(A),B))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls)))))).
% 0.78/0.96 Following clause subsumed by 2300 during input processing: 0 [copy,2195,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_nat(bit1(bit1(pls))))=hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit1(bit1(pls))))),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit1(bit1(pls)))),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),B)),hAPP_int_int(times_times_int(A),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls)))))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit1(bit1(pls)))))).
% 0.78/0.96 Following clause subsumed by 2299 during input processing: 0 [copy,2196,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(times_times_int(A),B)))).
% 0.78/0.97 Following clause subsumed by 2307 during input processing: 0 [copy,2197,flip.1] {-} hAPP_nat_nat(power_power_nat(hAPP_nat_nat(plus_plus_nat(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(power_power_nat(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(power_power_nat(B),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),hAPP_nat_nat(times_times_nat(A),B)))).
% 0.78/0.97 Following clause subsumed by 1885 during input processing: 0 [copy,2198,flip.1] {-} hAPP_nat_real(power_power_real(hAPP_real_real(plus_plus_real(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls))))),hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),hAPP_real_real(times_times_real(A),B)))).
% 0.78/0.97 2249 back subsumes 2214.
% 0.78/0.97 2255 back subsumes 2219.
% 0.78/0.97 2255 back subsumes 2218.
% 0.78/0.97 Following clause subsumed by 1638 during input processing: 0 [copy,2278,flip.1] {-} hAPP_nat_int(power_power_int(A),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),B))=hAPP_nat_int(power_power_int(hAPP_nat_int(power_power_int(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 1640 during input processing: 0 [copy,2279,flip.1] {-} hAPP_nat_real(power_power_real(A),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),B))=hAPP_nat_real(power_power_real(hAPP_nat_real(power_power_real(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 1642 during input processing: 0 [copy,2280,flip.1] {-} hAPP_nat_nat(power_power_nat(A),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),B))=hAPP_nat_nat(power_power_nat(hAPP_nat_nat(power_power_nat(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 1646 during input processing: 0 [copy,2281,flip.1] {-} hAPP_real_real(plus_plus_real(one_one_real),number267125858f_real(A))=number267125858f_real(hAPP_int_int(plus_plus_int(bit1(pls)),A)).
% 0.78/0.97 Following clause subsumed by 2287 during input processing: 0 [copy,2287,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),hAPP_int_int(times_times_int(C),D)))=hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(C),hAPP_int_int(times_times_int(B),D))).
% 0.78/0.97 Following clause subsumed by 2288 during input processing: 0 [copy,2288,flip.1] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),hAPP_nat_nat(times_times_nat(C),D)))=hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(C),hAPP_nat_nat(times_times_nat(B),D))).
% 0.78/0.97 Following clause subsumed by 2289 during input processing: 0 [copy,2289,flip.1] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),hAPP_real_real(times_times_real(C),D)))=hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(C),hAPP_real_real(times_times_real(B),D))).
% 0.78/0.97 Following clause subsumed by 2293 during input processing: 0 [copy,2290,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),hAPP_int_int(times_times_int(C),D)))=hAPP_int_int(times_times_int(C),hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),D))).
% 0.78/0.97 Following clause subsumed by 2294 during input processing: 0 [copy,2291,flip.1] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),hAPP_nat_nat(times_times_nat(C),D)))=hAPP_nat_nat(times_times_nat(C),hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),D))).
% 0.78/0.97 Following clause subsumed by 2295 during input processing: 0 [copy,2292,flip.1] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),hAPP_real_real(times_times_real(C),D)))=hAPP_real_real(times_times_real(C),hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),D))).
% 0.78/0.97 Following clause subsumed by 2290 during input processing: 0 [copy,2293,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),hAPP_int_int(times_times_int(C),D)))=hAPP_int_int(times_times_int(B),hAPP_int_int(times_times_int(C),hAPP_int_int(times_times_int(A),D))).
% 0.78/0.97 Following clause subsumed by 2291 during input processing: 0 [copy,2294,flip.1] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),hAPP_nat_nat(times_times_nat(C),D)))=hAPP_nat_nat(times_times_nat(B),hAPP_nat_nat(times_times_nat(C),hAPP_nat_nat(times_times_nat(A),D))).
% 0.78/0.97 Following clause subsumed by 2292 during input processing: 0 [copy,2295,flip.1] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),hAPP_real_real(times_times_real(C),D)))=hAPP_real_real(times_times_real(B),hAPP_real_real(times_times_real(C),hAPP_real_real(times_times_real(A),D))).
% 0.78/0.97 Following clause subsumed by 2296 during input processing: 0 [copy,2296,flip.1] {-} hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(B),C))=hAPP_int_int(times_times_int(A),hAPP_int_int(times_times_int(C),B)).
% 0.78/0.97 Following clause subsumed by 2297 during input processing: 0 [copy,2297,flip.1] {-} hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(B),C))=hAPP_nat_nat(times_times_nat(A),hAPP_nat_nat(times_times_nat(C),B)).
% 0.78/0.97 Following clause subsumed by 2298 during input processing: 0 [copy,2298,flip.1] {-} hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(B),C))=hAPP_real_real(times_times_real(A),hAPP_real_real(times_times_real(C),B)).
% 0.78/0.97 Following clause subsumed by 2196 during input processing: 0 [copy,2299,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(times_times_int(A),B))))=hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 2195 during input processing: 0 [copy,2300,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit1(bit1(pls))))),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit1(bit1(pls)))),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),B)),hAPP_int_int(times_times_int(A),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls)))))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit1(bit1(pls))))))=hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_nat(bit1(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 2194 during input processing: 0 [copy,2301,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(times_times_int(A),B))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls))))))=hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 2197 during input processing: 0 [copy,2307,flip.1] {-} hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(power_power_nat(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(power_power_nat(B),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls)))),hAPP_nat_nat(times_times_nat(A),B))))=hAPP_nat_nat(power_power_nat(hAPP_nat_nat(plus_plus_nat(A),B)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/0.97 Following clause subsumed by 2308 during input processing: 0 [copy,2308,flip.1] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),hAPP_int_int(plus_plus_int(C),D)))=hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(C),hAPP_int_int(plus_plus_int(B),D))).
% 0.78/0.97 Following clause subsumed by 2309 during input processing: 0 [copy,2309,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),hAPP_nat_nat(plus_plus_nat(C),D)))=hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(C),hAPP_nat_nat(plus_plus_nat(B),D))).
% 0.78/0.97 Following clause subsumed by 2310 during input processing: 0 [copy,2310,flip.1] {-} hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(B),hAPP_real_real(plus_plus_real(C),D)))=hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(C),hAPP_real_real(plus_plus_real(B),D))).
% 0.78/0.97 Following clause subsumed by 2311 during input processing: 0 [copy,2311,flip.1] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C))=hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(C),B)).
% 0.78/0.97 Following clause subsumed by 2312 during input processing: 0 [copy,2312,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(C),B)).
% 0.78/0.97 Following clause subsumed by 2313 during input processing: 0 [copy,2313,flip.1] {-} hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(B),C))=hAPP_real_real(plus_plus_real(A),hAPP_real_real(plus_plus_real(C),B)).
% 0.78/0.97 Following clause subsumed by 1770 during input processing: 0 [copy,2325,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(times_times_int(A),B)),C)=hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),C)),hAPP_nat_int(power_power_int(B),C)).
% 0.78/0.97 Following clause subsumed by 1771 during input processing: 0 [copy,2326,flip.1] {-} hAPP_nat_real(power_power_real(hAPP_real_real(times_times_real(A),B)),C)=hAPP_real_real(times_times_real(hAPP_nat_real(power_power_real(A),C)),hAPP_nat_real(power_power_real(B),C)).
% 0.78/0.97 Following clause subsumed by 1772 during input processing: 0 [copy,2327,flip.1] {-} hAPP_nat_nat(power_power_nat(hAPP_nat_nat(times_times_nat(A),B)),C)=hAPP_nat_nat(times_times_nat(hAPP_nat_nat(power_power_nat(A),C)),hAPP_nat_nat(power_power_nat(B),C)).
% 0.78/0.97 Following clause subsumed by 1777 during input processing: 0 [copy,2328,flip.1] {-} hAPP_int_int(times_times_int(bit0(A)),B)=bit0(hAPP_int_int(times_times_int(A),B)).
% 0.78/0.97 Following clause subsumed by 1778 during input processing: 0 [copy,2329,flip.1] {-} hAPP_int_int(plus_plus_int(bit0(A)),bit0(B))=bit0(hAPP_int_int(plus_plus_int(A),B)).
% 0.78/0.97 Following clause subsumed by 1791 during input processing: 0 [copy,2336,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),B)),B)=hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(A),one_one_int)),B).
% 0.78/0.97 Following clause subsumed by 1792 during input processing: 0 [copy,2337,flip.1] {-} hAPP_nat_nat(plus_plus_nat(hAPP_nat_nat(times_times_nat(A),B)),B)=hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(A),one_one_nat)),B).
% 0.78/0.97 Following clause subsumed by 1793 during input processing: 0 [copy,2338,flip.1] {-} hAPP_real_real(plus_plus_real(hAPP_real_real(times_times_real(A),B)),B)=hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(A),one_one_real)),B).
% 0.78/0.97 Following clause subsumed by 1794 during input processing: 0 [copy,2339,flip.1] {-} hAPP_int_int(plus_plus_int(A),hAPP_int_int(times_times_int(B),A))=hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(B),one_one_int)),A).
% 0.78/0.97 Following clause subsumed by 1795 during input processing: 0 [copy,2340,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(times_times_nat(B),A))=hAPP_nat_nat(times_times_nat(hAPP_nat_nat(plus_plus_nat(B),one_one_nat)),A).
% 0.78/0.97 Following clause subsumed by 1796 during input processing: 0 [copy,2341,flip.1] {-} hAPP_real_real(plus_plus_real(A),hAPP_real_real(times_times_real(B),A))=hAPP_real_real(times_times_real(hAPP_real_real(plus_plus_real(B),one_one_real)),A).
% 0.78/0.97 Following clause subsumed by 1798 during input processing: 0 [copy,2342,flip.1] {-} bit0(A)=hAPP_int_int(times_times_int(bit0(one_one_int)),A).
% 0.78/0.97 Following clause subsumed by 1825 during input processing: 0 [copy,2343,flip.1] {-} hAPP_int_int(plus_plus_int(bit1(A)),bit0(B))=bit1(hAPP_int_int(plus_plus_int(A),B)).
% 0.78/0.97 Following clause subsumed by 1826 during input processing: 0 [copy,2344,flip.1] {-} hAPP_int_int(plus_plus_int(bit0(A)),bit1(B))=bit1(hAPP_int_int(plus_plus_int(A),B)).
% 0.78/0.97 Following clause subsumed by 1828 during input processing: 0 [copy,2345,flip.1] {-} bit1(A)=hAPP_int_int(plus_plus_int(one_one_int),bit0(A)).
% 0.78/0.97 Following clause subsumed by 1830 during input processing: 0 [copy,2346,flip.1] {-} number_number_of_int(bit1(A))=hAPP_int_int(plus_plus_int(one_one_int),bit0(number_number_of_int(A))).
% 0.78/1.03 Following clause subsumed by 1846 during input processing: 0 [copy,2347,flip.1] {-} hAPP_int_int(times_times_int(bit1(A)),B)=hAPP_int_int(plus_plus_int(bit0(hAPP_int_int(times_times_int(A),B))),B).
% 0.78/1.03 Following clause subsumed by 1848 during input processing: 0 [copy,2348,flip.1] {-} hAPP_int_int(times_times_int(bit0(one_one_int)),number_number_of_int(A))=number_number_of_int(bit0(A)).
% 0.78/1.03 Following clause subsumed by 1850 during input processing: 0 [copy,2349,flip.1] {-} hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),number267125858f_real(A))=number267125858f_real(bit0(A)).
% 0.78/1.03 Following clause subsumed by 1886 during input processing: 0 [copy,2377,flip.1] {-} hAPP_real_real(times_times_real(number267125858f_real(bit0(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls)))))=hAPP_nat_real(power_power_real(hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),A)),number_number_of_nat(bit0(bit1(pls)))).
% 0.78/1.03 2389 back subsumes 2009.
% 0.78/1.03 2521 back subsumes 2514.
% 0.78/1.03 2521 back subsumes 2492.
% 0.78/1.03 2521 back subsumes 2407.
% 0.78/1.03 2521 back subsumes 2403.
% 0.78/1.03 2521 back subsumes 2400.
% 0.78/1.03 2521 back subsumes 2209.
% 0.78/1.03 2521 back subsumes 2203.
% 0.78/1.03 2738 back subsumes 2220.
% 0.78/1.03 2739 back subsumes 2225.
% 0.78/1.03 2753 back subsumes 2227.
% 0.78/1.03 Following clause subsumed by 1949 during input processing: 0 [copy,2757,flip.1] {-} number_number_of_int(bit0(A))=hAPP_int_int(plus_plus_int(pls),bit0(number_number_of_int(A))).
% 0.78/1.03 Following clause subsumed by 2021 during input processing: 0 [copy,2768,flip.1] {-} hAPP_int_int(minus_minus_int(bit0(A)),bit0(B))=bit0(hAPP_int_int(minus_minus_int(A),B)).
% 0.78/1.03 Following clause subsumed by 2025 during input processing: 0 [copy,2769,flip.1] {-} hAPP_int_int(times_times_int(hAPP_int_int(minus_minus_int(A),B)),C)=hAPP_int_int(minus_minus_int(hAPP_int_int(times_times_int(A),C)),hAPP_int_int(times_times_int(B),C)).
% 0.78/1.03 Following clause subsumed by 2029 during input processing: 0 [copy,2770,flip.1] {-} hAPP_real_real(times_times_real(hAPP_real_real(minus_minus_real(A),B)),number267125858f_real(C))=hAPP_real_real(minus_minus_real(hAPP_real_real(times_times_real(A),number267125858f_real(C))),hAPP_real_real(times_times_real(B),number267125858f_real(C))).
% 0.78/1.03 Following clause subsumed by 2030 during input processing: 0 [copy,2771,flip.1] {-} hAPP_int_int(minus_minus_int(bit1(A)),bit0(B))=bit1(hAPP_int_int(minus_minus_int(A),B)).
% 0.78/1.03 Following clause subsumed by 2031 during input processing: 0 [copy,2772,flip.1] {-} hAPP_int_int(minus_minus_int(bit1(A)),bit1(B))=bit0(hAPP_int_int(minus_minus_int(A),B)).
% 0.78/1.03 Following clause subsumed by 2035 during input processing: 0 [copy,2773,flip.1] {-} hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(hAPP_int_int(minus_minus_int(A),hAPP_int_int(times_times_int(B),C))),D)),hAPP_int_int(times_times_int(hAPP_int_int(minus_minus_int(E),hAPP_int_int(times_times_int(B),F))),G))=hAPP_int_int(minus_minus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(A),D)),hAPP_int_int(times_times_int(E),G))),hAPP_int_int(times_times_int(B),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(C),D)),hAPP_int_int(times_times_int(F),G)))).
% 0.78/1.03 Following clause subsumed by 2036 during input processing: 0 [copy,2774,flip.1] {-} hAPP_real_real(plus_plus_real(number267125858f_real(A)),hAPP_real_real(minus_minus_real(number267125858f_real(B)),C))=hAPP_real_real(minus_minus_real(number267125858f_real(hAPP_int_int(plus_plus_int(A),B))),C).
% 0.78/1.03 Following clause subsumed by 2037 during input processing: 0 [copy,2775,flip.1] {-} hAPP_int_int(plus_plus_int(number_number_of_int(A)),hAPP_int_int(minus_minus_int(number_number_of_int(B)),C))=hAPP_int_int(minus_minus_int(number_number_of_int(hAPP_int_int(plus_plus_int(A),B))),C).
% 0.78/1.03 Following clause subsumed by 2042 during input processing: 0 [copy,2778,flip.1] {-} hAPP_int_int(minus_minus_int(min),bit1(A))=bit0(hAPP_int_int(minus_minus_int(min),A)).
% 0.85/1.03 Following clause subsumed by 2051 during input processing: 0 [copy,2779,flip.1] {-} hAPP_nat_real(power_power_real(hAPP_real_real(minus_minus_real(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_real_real(minus_minus_real(hAPP_real_real(plus_plus_real(hAPP_nat_real(power_power_real(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_real(power_power_real(B),number_number_of_nat(bit0(bit1(pls)))))),hAPP_real_real(times_times_real(number267125858f_real(bit0(bit1(pls)))),hAPP_real_real(times_times_real(A),B))).
% 0.85/1.03 Following clause subsumed by 2053 during input processing: 0 [copy,2780,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(minus_minus_int(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_int_int(minus_minus_int(hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls)))))),hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(times_times_int(A),B))).
% 0.85/1.03 Following clause subsumed by 2055 during input processing: 0 [copy,2781,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(minus_minus_int(A),B)),number_number_of_nat(bit0(bit1(pls))))=hAPP_int_int(plus_plus_int(hAPP_int_int(minus_minus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(times_times_int(A),B)))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls))))).
% 0.85/1.03 Following clause subsumed by 2057 during input processing: 0 [copy,2782,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_int_int(minus_minus_int(A),B)),number_number_of_nat(bit1(bit1(pls))))=hAPP_int_int(minus_minus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(minus_minus_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit1(bit1(pls))))),hAPP_int_int(times_times_int(number_number_of_int(bit1(bit1(pls)))),hAPP_int_int(times_times_int(hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls))))),B)))),hAPP_int_int(times_times_int(number_number_of_int(bit1(bit1(pls)))),hAPP_int_int(times_times_int(A),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit0(bit1(pls)))))))),hAPP_nat_int(power_power_int(B),number_number_of_nat(bit1(bit1(pls))))).
% 0.85/1.03 Following clause subsumed by 2088 during input processing: 0 [copy,2783,flip.1] {-} hAPP_real_real(minus_minus_real(hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(C),D))=hAPP_real_real(plus_plus_real(hAPP_real_real(minus_minus_real(A),C)),hAPP_real_real(minus_minus_real(B),D)).
% 0.85/1.03 Following clause subsumed by 2089 during input processing: 0 [copy,2784,flip.1] {-} hAPP_int_int(minus_minus_int(hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(C),D))=hAPP_int_int(plus_plus_int(hAPP_int_int(minus_minus_int(A),C)),hAPP_int_int(minus_minus_int(B),D)).
% 0.85/1.03 Following clause subsumed by 2116 during input processing: 0 [copy,2785,flip.1] {-} hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(minus_minus_nat(A),B)),C)=hAPP_nat_nat(minus_minus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 0.85/1.03 Following clause subsumed by 2124 during input processing: 0 [copy,2786,flip.1] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(minus_minus_nat(A),B)),C)=hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.85/1.03 Following clause subsumed by 2173 during input processing: 0 [copy,2813,flip.1] {-} hAPP_int_int(div_mod_int(number_number_of_int(bit0(A))),number_number_of_int(bit0(B)))=hAPP_int_int(times_times_int(bit0(one_one_int)),hAPP_int_int(div_mod_int(number_number_of_int(A)),number_number_of_int(B))).
% 0.85/1.03 Following clause subsumed by 2180 during input processing: 0 [copy,2814,flip.1] {-} standardRes(A,B)=hAPP_int_int(div_mod_int(B),A).
% 0.85/1.03 Following clause subsumed by 2181 during input processing: 0 [copy,2815,flip.1] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(div_mod_nat(A),B)),C)=hAPP_nat_nat(div_mod_nat(hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C)).
% 0.85/1.03 Following clause subsumed by 2190 during input processing: 0 [copy,2816,flip.1] {-} hAPP_int_bool(cOMBC_int_int_bool(A,B),C)=hAPP_int_bool(hAPP_i1948725293t_bool(A,C),B).
% 0.85/1.03 Following clause subsumed by 2193 during input processing: 0 [copy,2817,flip.1] {-} hAPP_i68813070l_bool(cOMBB_1652995168ol_int(A,B),C)=hAPP_b589554111l_bool(A,hAPP_int_bool(B,C)).
% 0.85/1.03 Following clause subsumed by 2758 during input processing: 0 [copy,2832,flip.1] {-} hAPP_real_real(plus_plus_real(one_one_real),number267125858f_real(bit0(A)))=number267125858f_real(bit1(A)).
% 0.85/1.03
% 0.85/1.03 ======= end of input processing =======
% 0.85/1.04
% 0.85/1.04 SEGMENTATION FAULT!! This is probably caused by a
% 0.85/1.04 bug in Otter. Please send copy of the input file to
% 0.85/1.04 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.85/1.04 using, and send any other info that might be useful.
% 0.85/1.04
% 0.85/1.04
% 0.85/1.04 SEGMENTATION FAULT!! This is probably caused by a
% 0.85/1.04 bug in Otter. Please send copy of the input file to
% 0.85/1.04 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.85/1.04 using, and send any other info that might be useful.
% 0.85/1.04
% 0.85/1.04
% 0.85/1.04 The job finished Thu Jul 7 20:55:15 2022
%------------------------------------------------------------------------------