%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NUM925+2 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n027.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:13 EDT 2022
% Result : Unknown 0.48s 0.72s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM925+2 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jul 6 19:31:13 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.45 ----- Otter 3.2, August 2001 -----
% 0.19/0.45 The process was started by sandbox on n027.cluster.edu,
% 0.19/0.45 Wed Jul 6 19:31:13 2022
% 0.19/0.45 The command was "./sos". The process ID is 10128.
% 0.19/0.45
% 0.19/0.45 set(prolog_style_variables).
% 0.19/0.45 set(auto).
% 0.19/0.45 dependent: set(auto1).
% 0.19/0.45 dependent: set(process_input).
% 0.19/0.45 dependent: clear(print_kept).
% 0.19/0.45 dependent: clear(print_new_demod).
% 0.19/0.45 dependent: clear(print_back_demod).
% 0.19/0.45 dependent: clear(print_back_sub).
% 0.19/0.45 dependent: set(control_memory).
% 0.19/0.45 dependent: assign(max_mem, 12000).
% 0.19/0.45 dependent: assign(pick_given_ratio, 4).
% 0.19/0.45 dependent: assign(stats_level, 1).
% 0.19/0.45 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.45 dependent: assign(sos_limit, 5000).
% 0.19/0.45 dependent: assign(max_weight, 60).
% 0.19/0.45 clear(print_given).
% 0.19/0.45
% 0.19/0.45 formula_list(usable).
% 0.19/0.45
% 0.19/0.45 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=1, max_lits=5.
% 0.19/0.45
% 0.19/0.45 This ia a non-Horn set with equality. The strategy will be
% 0.19/0.45 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.19/0.45 unit deletion, with positive clauses in sos and nonpositive
% 0.19/0.45 clauses in usable.
% 0.19/0.45
% 0.19/0.45 dependent: set(knuth_bendix).
% 0.19/0.45 dependent: set(para_from).
% 0.19/0.45 dependent: set(para_into).
% 0.19/0.45 dependent: clear(para_from_right).
% 0.19/0.45 dependent: clear(para_into_right).
% 0.19/0.45 dependent: set(para_from_vars).
% 0.19/0.45 dependent: set(eq_units_both_ways).
% 0.19/0.45 dependent: set(dynamic_demod_all).
% 0.19/0.45 dependent: set(dynamic_demod).
% 0.19/0.45 dependent: set(order_eq).
% 0.19/0.45 dependent: set(back_demod).
% 0.19/0.45 dependent: set(lrpo).
% 0.19/0.45 dependent: set(hyper_res).
% 0.19/0.45 dependent: set(unit_deletion).
% 0.19/0.45 dependent: set(factor).
% 0.19/0.45
% 0.19/0.45 There is a clause for symmetry of equality, so it is
% 0.19/0.45 assumed that equality is fully axiomatized; therefore,
% 0.19/0.45 paramodulation is disabled.
% 0.19/0.45
% 0.19/0.45 dependent: clear(para_from).
% 0.19/0.45 dependent: clear(para_into).
% 0.19/0.45
% 0.19/0.45 ------------> process usable:
% 0.19/0.45 Following clause subsumed by 14 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.19/0.45 Following clause subsumed by 15 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.19/0.45 Following clause subsumed by 20 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.19/0.45 Following clause subsumed by 21 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.19/0.45 Following clause subsumed by 23 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.19/0.45 Following clause subsumed by 24 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.19/0.45 Following clause subsumed by 58 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.19/0.45 Following clause subsumed by 59 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.19/0.45 Following clause subsumed by 87 during input processing: 0 [flip.1] {-} bit1(A)!=pls.
% 0.19/0.45 Following clause subsumed by 4 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.19/0.45 Following clause subsumed by 5 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.19/0.45 Following clause subsumed by 6 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.19/0.45 Following clause subsumed by 135 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),A)).
% 0.19/0.45 Following clause subsumed by 139 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|B!=A.
% 0.19/0.45 Following clause subsumed by 138 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.19/0.45 Following clause subsumed by 133 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.19/0.45 Following clause subsumed by 146 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.19/0.45 Following clause subsumed by 147 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.19/0.45 Following clause subsumed by 139 during input processing: 0 [] {-} A!=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.19/0.45 Following clause subsumed by 133 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.19/0.45 Following clause subsumed by 154 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.19/0.45 Following clause subsumed by 156 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.19/0.45 Following clause subsumed by 155 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.19/0.45 Following clause subsumed by 154 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.19/0.45 Following clause subsumed by 156 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.19/0.45 Following clause subsumed by 155 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.19/0.45 Following clause subsumed by 158 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 159 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 46 during input processing: 0 [] {-} hAPP_nat_int(semiri1621563631at_int,A)!=hAPP_nat_int(semiri1621563631at_int,B)|A=B.
% 0.19/0.45 Following clause subsumed by 47 during input processing: 0 [] {-} hAPP_nat_int(semiri1621563631at_int,A)=hAPP_nat_int(semiri1621563631at_int,B)|A!=B.
% 0.19/0.45 Following clause subsumed by 46 during input processing: 0 [] {-} hAPP_nat_int(semiri1621563631at_int,A)!=hAPP_nat_int(semiri1621563631at_int,B)|A=B.
% 0.19/0.45 Following clause subsumed by 47 during input processing: 0 [] {-} hAPP_nat_int(semiri1621563631at_int,A)=hAPP_nat_int(semiri1621563631at_int,B)|A!=B.
% 0.19/0.45 Following clause subsumed by 115 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,A)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.19/0.45 Following clause subsumed by 116 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,A)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.19/0.45 Following clause subsumed by 134 during input processing: 0 [flip.1] {-} zero_zero_real!=one_one_real.
% 0.19/0.45 Following clause subsumed by 96 during input processing: 0 [flip.1] {-} zero_zero_int!=one_one_int.
% 0.19/0.45 Following clause subsumed by 134 during input processing: 0 [] {-} zero_zero_real!=one_one_real.
% 0.19/0.45 Following clause subsumed by 176 during input processing: 0 [] {-} zero_zero_nat!=one_one_nat.
% 0.19/0.45 Following clause subsumed by 96 during input processing: 0 [] {-} zero_zero_int!=one_one_int.
% 0.19/0.45 Following clause subsumed by 158 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 159 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 180 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,hAPP_nat_real(semiri132038758t_real,A)),hAPP_nat_real(semiri132038758t_real,B))).
% 0.19/0.45 Following clause subsumed by 182 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,hAPP_nat_nat(semiri984289939at_nat,A)),hAPP_nat_nat(semiri984289939at_nat,B))).
% 0.19/0.45 Following clause subsumed by 159 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,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B))).
% 0.19/0.45 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_nat_real(semiri132038758t_real,A)),hAPP_nat_real(semiri132038758t_real,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 181 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(semiri984289939at_nat,A)),hAPP_nat_nat(semiri984289939at_nat,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 158 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.19/0.45 Following clause subsumed by 147 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),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),hAPP_nat_nat(plus_plus_nat(A),C))).
% 0.19/0.45 Following clause subsumed by 133 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,one_one_nat),zero_zero_nat)).
% 0.19/0.45 Following clause subsumed by 155 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,zero_zero_nat),hAPP_nat_nat(power_power_nat(A),B))).
% 0.19/0.45 Following clause subsumed by 195 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.19/0.45 Following clause subsumed by 197 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.19/0.45 Following clause subsumed by 199 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.19/0.45 Following clause subsumed by 196 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.19/0.45 Following clause subsumed by 198 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.19/0.45 Following clause subsumed by 200 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.19/0.45 Following clause subsumed by 177 during input processing: 0 [] {-} hAPP_nat_real(power_power_real(A),B)!=zero_zero_real|A=zero_zero_real.
% 0.19/0.45 Following clause subsumed by 178 during input processing: 0 [] {-} hAPP_nat_int(power_power_int(A),B)!=zero_zero_int|A=zero_zero_int.
% 0.19/0.45 Following clause subsumed by 133 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(semiri984289939at_nat,A)),zero_zero_nat)).
% 0.19/0.45 Following clause subsumed by 72 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,A)),zero_zero_int)).
% 0.19/0.45 Following clause subsumed by 44 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(plus_plus_real(A),A)),zero_zero_real))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),zero_zero_real)).
% 0.19/0.45 Following clause subsumed by 45 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(plus_plus_real(A),A)),zero_zero_real))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),zero_zero_real)).
% 0.19/0.45 Following clause subsumed by 42 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),A)),zero_zero_int))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),zero_zero_int)).
% 0.19/0.45 Following clause subsumed by 43 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),A)),zero_zero_int))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),zero_zero_int)).
% 0.19/0.45 Following clause subsumed by 142 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=hAPP_nat_nat(plus_plus_nat(C),B)|A=C.
% 0.19/0.45 Following clause subsumed by 140 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=hAPP_nat_nat(plus_plus_nat(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 229 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(A),B)!=hAPP_real_real(plus_plus_real(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 140 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=hAPP_nat_nat(plus_plus_nat(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 230 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(A),B)!=hAPP_int_int(plus_plus_int(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 227 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(A),B)!=hAPP_real_real(plus_plus_real(C),B)|A=C.
% 0.19/0.45 Following clause subsumed by 142 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=hAPP_nat_nat(plus_plus_nat(C),B)|A=C.
% 0.19/0.45 Following clause subsumed by 143 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(C),B)|A!=C.
% 0.19/0.45 Following clause subsumed by 228 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(A),B)!=hAPP_int_int(plus_plus_int(C),B)|A=C.
% 0.19/0.45 Following clause subsumed by 229 during input processing: 0 [] {-} hAPP_real_real(plus_plus_real(A),B)!=hAPP_real_real(plus_plus_real(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 140 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=hAPP_nat_nat(plus_plus_nat(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 141 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(A),C)|B!=C.
% 0.19/0.45 Following clause subsumed by 230 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(A),B)!=hAPP_int_int(plus_plus_int(A),C)|B=C.
% 0.19/0.45 Following clause subsumed by 163 during input processing: 0 [flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=A|B=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 85 during input processing: 0 [flip.1] {-} hAPP_real_real(plus_plus_real(A),A)!=zero_zero_real|A=zero_zero_real.
% 0.19/0.45 Following clause subsumed by 86 during input processing: 0 [flip.1] {-} hAPP_real_real(plus_plus_real(A),A)=zero_zero_real|A!=zero_zero_real.
% 0.19/0.45 Following clause subsumed by 83 during input processing: 0 [flip.1] {-} hAPP_int_int(plus_plus_int(A),A)!=zero_zero_int|A=zero_zero_int.
% 0.19/0.45 Following clause subsumed by 84 during input processing: 0 [flip.1] {-} hAPP_int_int(plus_plus_int(A),A)=zero_zero_int|A!=zero_zero_int.
% 0.19/0.45 Following clause subsumed by 144 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.19/0.45 Following clause subsumed by 149 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,C),D))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(A),C)),hAPP_nat_nat(plus_plus_nat(B),D))).
% 0.19/0.45 Following clause subsumed by 145 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,hAPP_nat_nat(plus_plus_nat(C),A)),hAPP_nat_nat(plus_plus_nat(C),B))).
% 0.19/0.45 Following clause subsumed by 148 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,hAPP_nat_nat(plus_plus_nat(A),C)),hAPP_nat_nat(plus_plus_nat(B),C))).
% 0.19/0.45 Following clause subsumed by 25 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,hAPP_int_int(plus_plus_int(A),C)),hAPP_int_int(plus_plus_int(B),C))).
% 0.19/0.45 Following clause subsumed by 251 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(A),C)))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),C)).
% 0.19/0.45 Following clause subsumed by 258 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(A),C)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,B),C)).
% 0.19/0.45 Following clause subsumed by 144 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.19/0.45 Following clause subsumed by 145 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.19/0.45 Following clause subsumed by 252 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(A),C)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),C)).
% 0.19/0.45 Following clause subsumed by 259 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(A),C)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,B),C)).
% 0.19/0.45 Following clause subsumed by 253 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(C),B)))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),C)).
% 0.19/0.45 Following clause subsumed by 260 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(C),B)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,A),C)).
% 0.19/0.45 Following clause subsumed by 254 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(C),B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.19/0.45 Following clause subsumed by 148 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(C),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.19/0.45 Following clause subsumed by 255 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(C),B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),C)).
% 0.19/0.45 Following clause subsumed by 25 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(C),B)))| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),C)).
% 0.19/0.45 Following clause subsumed by 204 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)!=zero_zero_nat|B!=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 203 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)!=zero_zero_nat|A=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 205 during input processing: 0 [] {-} hAPP_nat_nat(power_power_nat(A),B)=zero_zero_nat|B=zero_zero_nat|A!=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 133 during input processing: 0 [unit_del,133,factor_simp] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),zero_zero_nat)).
% 0.19/0.45 Following clause subsumed by 183 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(plus_plus_real(A),B))).
% 0.19/0.45 Following clause subsumed by 146 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,zero_zero_nat),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B))).
% 0.19/0.45 Following clause subsumed by 184 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,zero_zero_int),B))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(A),B))).
% 0.19/0.45 Following clause subsumed by 271 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,hAPP_real_real(plus_plus_real(A),C)),hAPP_real_real(plus_plus_real(B),C))).
% 0.19/0.45 Following clause subsumed by 273 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,hAPP_nat_nat(plus_plus_nat(A),C)),hAPP_nat_nat(plus_plus_nat(B),C))).
% 0.19/0.45 Following clause subsumed by 275 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,hAPP_int_int(plus_plus_int(A),C)),hAPP_int_int(plus_plus_int(B),C))).
% 0.19/0.45 Following clause subsumed by 277 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,hAPP_real_real(plus_plus_real(C),A)),hAPP_real_real(plus_plus_real(C),B))).
% 0.19/0.45 Following clause subsumed by 279 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,hAPP_nat_nat(plus_plus_nat(C),A)),hAPP_nat_nat(plus_plus_nat(C),B))).
% 0.19/0.45 Following clause subsumed by 281 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,hAPP_int_int(plus_plus_int(C),A)),hAPP_int_int(plus_plus_int(C),B))).
% 0.19/0.45 Following clause subsumed by 270 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(C),B)))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),C)).
% 0.19/0.45 Following clause subsumed by 272 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(C),B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.19/0.45 Following clause subsumed by 274 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(C),B)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),C)).
% 0.19/0.45 Following clause subsumed by 276 during input processing: 0 [] {-} -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,hAPP_real_real(plus_plus_real(A),B)),hAPP_real_real(plus_plus_real(A),C)))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,B),C)).
% 0.19/0.45 Following clause subsumed by 278 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.19/0.45 Following clause subsumed by 280 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(A),B)),hAPP_int_int(plus_plus_int(A),C)))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,B),C)).
% 0.19/0.45 Following clause subsumed by 288 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.19/0.45 Following clause subsumed by 289 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.19/0.45 Following clause subsumed by 290 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.19/0.45 Following clause subsumed by 291 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.19/0.45 Following clause subsumed by 281 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,hAPP_int_int(plus_plus_int(C),A)),hAPP_int_int(plus_plus_int(C),B))).
% 0.19/0.45 Following clause subsumed by 296 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.19/0.45 Following clause subsumed by 297 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.19/0.45 Following clause subsumed by 318 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.19/0.45 Following clause subsumed by 320 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.19/0.45 Following clause subsumed by 322 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.19/0.45 Following clause subsumed by 164 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,zero_zero_nat),B))|hAPP_nat_nat(plus_plus_nat(A),B)!=zero_zero_nat|A=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 165 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,zero_zero_nat),B))|hAPP_nat_nat(plus_plus_nat(A),B)!=zero_zero_nat|B=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 166 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,zero_zero_nat),B))|hAPP_nat_nat(plus_plus_nat(A),B)=zero_zero_nat|A!=zero_zero_nat|B!=zero_zero_nat.
% 0.19/0.45 Following clause subsumed by 381 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.19/0.45 Following clause subsumed by 382 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.19/0.45 Following clause subsumed by 351 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(plus_plus_int(A),B))).
% 0.19/0.45 Following clause subsumed by 360 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_eq_int,C),D))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(A),C)),hAPP_int_int(plus_plus_int(B),D))).
% 0.19/0.46 Following clause subsumed by 372 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.19/0.46 Following clause subsumed by 146 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,zero_zero_nat),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B))).
% 0.19/0.46 Following clause subsumed by 147 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_nat,zero_zero_nat),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B))).
% 0.19/0.46 Following clause subsumed by 147 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_nat,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),hAPP_nat_nat(plus_plus_nat(A),C))).
% 0.19/0.46 Following clause subsumed by 133 during input processing: 0 [unit_del,133] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),zero_zero_nat)).
% 0.19/0.46 Following clause subsumed by 133 during input processing: 0 [unit_del,133] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),zero_zero_nat))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),zero_zero_nat)).
% 0.19/0.46 Following clause subsumed by 424 during input processing: 0 [] {-} number_number_of_nat(A)!=zero_zero_nat|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),pls)).
% 0.19/0.46 Following clause subsumed by 426 during input processing: 0 [] {-} number_number_of_nat(A)=zero_zero_nat| -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),pls)).
% 0.19/0.46 Following clause subsumed by 431 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.19/0.46 Following clause subsumed by 432 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.19/0.46 Following clause subsumed by 433 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.19/0.46 Following clause subsumed by 434 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.19/0.46 Following clause subsumed by 442 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_eq_int,hAPP_int_int(plus_plus_int(A),one_one_int)),B)).
% 0.19/0.46 Following clause subsumed by 420 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.19/0.46 Following clause subsumed by 421 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.19/0.46 Following clause subsumed by 422 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.19/0.46 Following clause subsumed by 476 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.19/0.46 Following clause subsumed by 478 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.19/0.46 Following clause subsumed by 476 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.19/0.46 Following clause subsumed by 477 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A!=B.
% 0.19/0.46 Following clause subsumed by 476 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.19/0.46 Following clause subsumed by 138 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.19/0.46 Following clause subsumed by 478 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.19/0.46 Following clause subsumed by 477 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.19/0.46 Following clause subsumed by 482 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.19/0.46 Following clause subsumed by 481 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.19/0.46 Following clause subsumed by 278 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.19/0.46 Following clause subsumed by 279 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),hAPP_nat_nat(plus_plus_nat(A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.19/0.46 Following clause subsumed by 273 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,hAPP_nat_nat(plus_plus_nat(A),C)),hAPP_nat_nat(plus_plus_nat(B),C))).
% 0.19/0.46 Following clause subsumed by 283 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,C),D))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),C)),hAPP_nat_nat(plus_plus_nat(B),D))).
% 0.19/0.46 Following clause subsumed by 491 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.19/0.46 Following clause subsumed by 490 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.19/0.46 Following clause subsumed by 277 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,hAPP_real_real(plus_plus_real(C),A)),hAPP_real_real(plus_plus_real(C),B))).
% 0.19/0.46 Following clause subsumed by 302 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.19/0.46 Following clause subsumed by 303 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.19/0.46 Following clause subsumed by 302 during input processing: 0 [] {-} -hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.19/0.46 Following clause subsumed by 303 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.19/0.46 Following clause subsumed by 501 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,C),A))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,C),B)).
% 0.19/0.46 Following clause subsumed by 479 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,C),A))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,C),B)).
% 0.19/0.46 Following clause subsumed by 292 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,C),A))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,C),B)).
% 0.19/0.46 Following clause subsumed by 502 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,B),A))|B=A.
% 0.19/0.46 Following clause subsumed by 480 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,B),A))|B=A.
% 0.19/0.46 Following clause subsumed by 293 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,B),A))|B=A.
% 0.19/0.46 Following clause subsumed by 501 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,B),C))|hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),C)).
% 0.19/0.46 Following clause subsumed by 479 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,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.19/0.46 Following clause subsumed by 292 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,B),C))|hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),C)).
% 0.19/0.46 Following clause subsumed by 502 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,B),A))|A=B.
% 0.19/0.46 Following clause subsumed by 480 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,B),A))|A=B.
% 0.19/0.46 Following clause subsumed by 293 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,B),A))|A=B.
% 0.19/0.46 Following clause subsumed by 502 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,B),A))|B=A.
% 0.19/0.47 Following clause subsumed by 483 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,B),A))|B!=A.
% 0.19/0.47 Following clause subsumed by 480 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,B),A))|B=A.
% 0.19/0.47 Following clause subsumed by 477 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,B),A))|B!=A.
% 0.19/0.47 Following clause subsumed by 293 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,B),A))|B=A.
% 0.19/0.47 Following clause subsumed by 528 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),sqrt(A)))| -hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_real,zero_zero_real),A)).
% 0.19/0.47 Following clause subsumed by 89 during input processing: 0 [copy,88,flip.1] {-} bit0(A)!=bit1(B).
% 0.19/0.47 Following clause subsumed by 88 during input processing: 0 [copy,89,flip.1] {-} bit1(A)!=bit0(B).
% 0.19/0.47 97 back subsumes 7.
% 0.19/0.47 103 back subsumes 9.
% 0.19/0.47 124 back subsumes 11.
% 0.19/0.47 125 back subsumes 12.
% 0.19/0.47 126 back subsumes 13.
% 0.19/0.47 177 back subsumes 103.
% 0.19/0.47 178 back subsumes 97.
% 0.19/0.47 201 back subsumes 104.
% 0.19/0.47 202 back subsumes 105.
% 0.19/0.47 203 back subsumes 100.
% 0.19/0.47 204 back subsumes 101.
% 0.19/0.47 205 back subsumes 102.
% 0.19/0.47 206 back subsumes 98.
% 0.19/0.47 207 back subsumes 99.
% 0.19/0.47 216 back subsumes 125.
% 0.19/0.47 349 back subsumes 340.
% 0.19/0.47 350 back subsumes 341.
% 0.19/0.47 351 back subsumes 342.
% 0.19/0.47 411 back subsumes 407.
% 0.19/0.47 413 back subsumes 408.
% 0.19/0.47 414 back subsumes 409.
% 0.19/0.47 415 back subsumes 410.
% 0.19/0.47 477 back subsumes 475.
% 0.19/0.47 488 back subsumes 353.
% 0.19/0.47 489 back subsumes 350.
% 0.19/0.47 524 back subsumes 523.
% 0.19/0.47
% 0.19/0.47 ------------> process sos:
% 0.19/0.47 Following clause subsumed by 632 during input processing: 0 [demod,627] {-} one_one_int=one_one_int.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,680] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,640,676,676] {-} pls=pls.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,655] {-} zero_zero_nat=zero_zero_nat.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,640,676,676] {-} pls=pls.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,688] {-} zero_zero_real=zero_zero_real.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,640,676] {-} pls=pls.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,688] {-} zero_zero_real=zero_zero_real.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,640,676,680] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,640,676,678] {-} A=A.
% 0.19/0.47 Following clause subsumed by 637 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,627] {-} one_one_int=one_one_int.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,664] {-} one_one_nat=one_one_nat.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,630] {-} one_one_real=one_one_real.
% 0.19/0.47 Following clause subsumed by 757 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.19/0.47 Following clause subsumed by 757 during input processing: 0 [factor_simp] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),A)).
% 0.19/0.47 Following clause subsumed by 762 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.19/0.47 Following clause subsumed by 636 during input processing: 0 [] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,651] {-} hAPP_int_int(plus_plus_int(hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B))=hAPP_int_int(plus_plus_int(hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,653] {-} one_one_int=one_one_int.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,643] {-} hAPP_nat_int(power_power_int(hAPP_nat_int(semiri1621563631at_int,A)),B)=hAPP_nat_int(power_power_int(hAPP_nat_int(semiri1621563631at_int,A)),B).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,653] {-} one_one_int=one_one_int.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,651] {-} hAPP_int_int(plus_plus_int(hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B))=hAPP_int_int(plus_plus_int(hAPP_nat_int(semiri1621563631at_int,A)),hAPP_nat_int(semiri1621563631at_int,B)).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,643] {-} hAPP_nat_int(power_power_int(hAPP_nat_int(semiri1621563631at_int,A)),B)=hAPP_nat_int(power_power_int(hAPP_nat_int(semiri1621563631at_int,A)),B).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,659,676,676] {-} pls=pls.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,659,676] {-} pls=pls.
% 0.19/0.47 Following clause subsumed by 751 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),number_number_of_nat(bit0(bit1(pls))))).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,806] {-} one_one_real=one_one_real.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,808] {-} one_one_nat=one_one_nat.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,810] {-} one_one_int=one_one_int.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,761] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,668] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,826] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,761] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,668] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,826] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,761] {-} 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.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,668] {-} 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.19/0.47 Following clause subsumed by 759 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.19/0.47 Following clause subsumed by 669 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.19/0.47 Following clause subsumed by 758 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(B),A).
% 0.19/0.47 Following clause subsumed by 670 during input processing: 0 [] {-} hAPP_int_int(plus_plus_int(A),B)=hAPP_int_int(plus_plus_int(B),A).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,694] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,765] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,678] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,694] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,765] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,678] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,694] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,765] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,678] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,691] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,767] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,680] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,691] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,767] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,680] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,691] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,767] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,676,680] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,769] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,771] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [demod,773] {-} A=A.
% 0.19/0.47 Following clause subsumed by 834 during input processing: 0 [demod,676,676] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),pls)).
% 0.19/0.47 Following clause subsumed by 845 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,zero_zero_real),hAPP_nat_real(semiri132038758t_real,A))).
% 0.19/0.47 Following clause subsumed by 846 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),hAPP_nat_nat(semiri984289939at_nat,A))).
% 0.19/0.47 Following clause subsumed by 848 during input processing: 0 [demod,676] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(semiri1621563631at_int,A))).
% 0.19/0.47 Following clause subsumed by 840 during input processing: 0 [demod,676] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),one_one_int)).
% 0.19/0.47 Following clause subsumed by 848 during input processing: 0 [demod,676] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(semiri1621563631at_int,A))).
% 0.19/0.47 Following clause subsumed by 848 during input processing: 0 [demod,676] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(semiri1621563631at_int,A))).
% 0.19/0.47 Following clause subsumed by 670 during input processing: 0 [demod,858,756,756] {-} hAPP_int_int(plus_plus_int(A),one_one_int)=hAPP_int_int(plus_plus_int(one_one_int),A).
% 0.19/0.47 Following clause subsumed by 835 during input processing: 0 [demod,676,756] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),pls)).
% 0.19/0.47 Following clause subsumed by 878 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),A)).
% 0.19/0.47 Following clause subsumed by 885 during input processing: 0 [] {-} hBOOL(hAPP_real_bool(hAPP_r1134773055l_bool(ord_less_eq_real,A),A)).
% 0.19/0.47 Following clause subsumed by 879 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),A)).
% 0.19/0.47 Following clause subsumed by 835 during input processing: 0 [] {-} hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,A),A)).
% 0.19/0.47 Following clause subsumed by 886 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,B),A)).
% 0.19/0.47 Following clause subsumed by 880 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,B),A)).
% 0.19/0.47 Following clause subsumed by 836 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,B),A)).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [] {-} A=A.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,615,flip.1,demod,756,756] {-} bit0(bit1(pls))=bit0(bit1(pls)).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,619,flip.1] {-} number267125858f_real(bit0(bit1(pls)))=number267125858f_real(bit0(bit1(pls))).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,632,flip.1] {-} one_one_int=one_one_int.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,634,flip.1] {-} one_one_real=one_one_real.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,637,flip.1,demod,756,756,756] {-} hAPP_int_int(plus_plus_int(A),B)=hAPP_int_int(plus_plus_int(A),B).
% 0.19/0.47 637 back subsumes 569.
% 0.19/0.47 637 back subsumes 448.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,645,flip.1] {-} hAPP_nat_int(power_power_int(hAPP_nat_int(semiri1621563631at_int,A)),B)=hAPP_nat_int(power_power_int(hAPP_nat_int(semiri1621563631at_int,A)),B).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,657,flip.1] {-} zero_zero_nat=zero_zero_nat.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,661,flip.1] {-} number_number_of_nat(bit0(bit1(pls)))=number_number_of_nat(bit0(bit1(pls))).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,666,flip.1] {-} one_one_nat=one_one_nat.
% 0.19/0.47 Following clause subsumed by 669 during input processing: 0 [copy,669,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.19/0.47 Following clause subsumed by 670 during input processing: 0 [copy,670,flip.1] {-} hAPP_int_int(plus_plus_int(A),B)=hAPP_int_int(plus_plus_int(B),A).
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,686,flip.1] {-} A=A.
% 0.19/0.47 686 back subsumes 666.
% 0.19/0.47 686 back subsumes 661.
% 0.19/0.47 686 back subsumes 657.
% 0.19/0.47 686 back subsumes 645.
% 0.19/0.47 686 back subsumes 634.
% 0.19/0.47 686 back subsumes 632.
% 0.19/0.47 686 back subsumes 619.
% 0.19/0.47 686 back subsumes 615.
% 0.19/0.47 686 back subsumes 579.
% 0.19/0.47 686 back subsumes 576.
% 0.19/0.47 686 back subsumes 572.
% 0.19/0.47 686 back subsumes 571.
% 0.19/0.47 686 back subsumes 565.
% 0.19/0.47 686 back subsumes 564.
% 0.19/0.47 686 back subsumes 556.
% 0.19/0.47 Following clause subsumed by 703 during input processing: 0 [copy,701,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.19/0.47 701 back subsumes 446.
% 0.19/0.47 Following clause subsumed by 686 during input processing: 0 [copy,702,flip.1,demod,756,756,756] {-} hAPP_int_int(plus_plus_int(A),B)=hAPP_int_int(plus_plus_int(A),B).
% 0.19/0.47 Following clause subsumed by 701 during input processing: 0 [copy,703,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.19/0.47 Following clause subsumed by 987 during input processing: 0 [copy,730,flip.1,demod,756,756] {-} hAPP_int_int(plus_plus_int(one_one_int),bit0(A))=bit1(A).
% 0.19/0.47 746 back subsumes 623.
% 0.19/0.47 747 back subsumes 624.
% 0.19/0.47 Following clause subsumed by 758 during input processing: 0 [copy,758,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(B),A).
% 0.19/0.47 Following clause subsumed by 759 during input processing: 0 [copy,759,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.19/0.48 Following clause subsumed by 817 during input processing: 0 [copy,817,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.19/0.48 Following clause subsumed by 819 during input processing: 0 [copy,819,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.19/0.48 Following clause subsumed by 822 during input processing: 0 [copy,822,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.19/0.48 Following clause subsumed by 824 during input processing: 0 [copy,824,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.19/0.48 Following clause subsumed by 827 during input processing: 0 [copy,827,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.19/0.48 Following clause subsumed by 828 during input processing: 0 [copy,828,flip.1] {-} hAPP_real_real(plus_plus_real(A),B)=hAPP_real_real(plus_plus_real(B),A).
% 0.19/0.48 835 back subsumes 834.
% 0.19/0.48 878 back subsumes 846.
% 0.19/0.48 878 back subsumes 838.
% 0.19/0.48 878 back subsumes 371.
% 0.19/0.48 879 back subsumes 561.
% 0.19/0.48 885 back subsumes 560.
% 0.19/0.48 Following clause subsumed by 681 during input processing: 0 [copy,981,flip.1] {-} hAPP_int_int(plus_plus_int(bit0(A)),bit0(B))=bit0(hAPP_int_int(plus_plus_int(A),B)).
% 0.19/0.48 Following clause subsumed by 704 during input processing: 0 [copy,985,flip.1] {-} hAPP_int_int(plus_plus_int(bit1(A)),bit0(B))=bit1(hAPP_int_int(plus_plus_int(A),B)).
% 0.19/0.48 Following clause subsumed by 705 during input processing: 0 [copy,986,flip.1] {-} hAPP_int_int(plus_plus_int(bit0(A)),bit1(B))=bit1(hAPP_int_int(plus_plus_int(A),B)).
% 0.19/0.48 Following clause subsumed by 707 during input processing: 0 [copy,987,flip.1] {-} bit1(A)=hAPP_int_int(plus_plus_int(one_one_int),bit0(A)).
% 0.19/0.48 993 back subsumes 956.
% 0.19/0.48 993 back subsumes 955.
% 0.19/0.48 993 back subsumes 240.
% 0.19/0.48 993 back subsumes 239.
% 0.19/0.48 993 back subsumes 238.
% 0.19/0.48 993 back subsumes 237.
% 0.19/0.48 993 back subsumes 236.
% 0.19/0.48 993 back subsumes 235.
% 0.19/0.48 993 back subsumes 224.
% 0.19/0.48 993 back subsumes 223.
% 0.19/0.48 993 back subsumes 222.
% 0.19/0.48 993 back subsumes 221.
% 0.19/0.48 993 back subsumes 37.
% 0.19/0.48 993 back subsumes 36.
% 0.19/0.48 993 back subsumes 33.
% 0.19/0.48 993 back subsumes 32.
% 0.19/0.48 Following clause subsumed by 1000 during input processing: 0 [copy,1000,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.19/0.48 Following clause subsumed by 1001 during input processing: 0 [copy,1001,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.19/0.48 Following clause subsumed by 862 during input processing: 0 [copy,1011,flip.1] {-} number267125858f_real(hAPP_int_int(plus_plus_int(A),one_one_int))=hAPP_real_real(plus_plus_real(one_one_real),number267125858f_real(A)).
% 0.19/0.48 Following clause subsumed by 864 during input processing: 0 [copy,1012,flip.1] {-} hAPP_int_int(plus_plus_int(bit1(A)),bit1(B))=bit0(hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),one_one_int))).
% 0.19/0.48 Following clause subsumed by 1086 during input processing: 0 [copy,1013,flip.1] {-} number267125858f_real(hAPP_int_int(plus_plus_int(one_one_int),A))=hAPP_real_real(plus_plus_real(one_one_real),number267125858f_real(A)).
% 0.19/0.48 Following clause subsumed by 1013 during input processing: 0 [copy,1086,flip.1] {-} hAPP_real_real(plus_plus_real(one_one_real),number267125858f_real(A))=number267125858f_real(hAPP_int_int(plus_plus_int(one_one_int),A)).
% 0.19/0.48 Following clause subsumed by 1002 during input processing: 0 [copy,1102,flip.1] {-} hAPP_real_real(plus_plus_real(one_one_real),number267125858f_real(bit0(A)))=number267125858f_real(bit1(A)).
% 0.19/0.48
% 0.19/0.48 ======= end of input processing =======
% 0.39/0.63
% 0.39/0.63
% 0.39/0.63 Failed to model usable list: disabling FINDER
% 0.39/0.63
% 0.39/0.63
% 0.39/0.63
% 0.39/0.63 -------------- Softie stats --------------
% 0.39/0.63
% 0.39/0.63 UPDATE_STOP: 300
% 0.39/0.63 SFINDER_TIME_LIMIT: 2
% 0.39/0.63 SHORT_CLAUSE_CUTOFF: 4
% 0.39/0.63 number of clauses in intial UL: 345
% 0.39/0.63 number of clauses initially in problem: 672
% 0.39/0.63 percentage of clauses intially in UL: 51
% 0.39/0.63 percentage of distinct symbols occuring in initial UL: 8
% 0.39/0.63 percent of all initial clauses that are short: 99
% 0.39/0.63 absolute distinct symbol count: 703
% 0.39/0.63 distinct predicate count: 193
% 0.39/0.63 distinct function count: 95
% 0.39/0.63 distinct constant count: 415
% 0.39/0.63
% 0.39/0.63 ---------- no more Softie stats ----------
% 0.39/0.63
% 0.39/0.63
% 0.39/0.63
% 0.39/0.63 =========== start of search ===========
% 0.48/0.72 hAPP_nat_nat(plus_plus_nat(number_number_of_nat(bit1(one_one_int))),number_number_of_nat(bit0(one_one_int)))=number_number_of_nat(hAPP_int_int(plus_plus_int(bit1(one_one_int)),bit0(one_one_int))).
% 0.48/0.72
% 0.48/0.72 ------------- memory usage ------------
% 0.48/0.72 119 mallocs of 32700 bytes each, 3800.1 K.
% 0.48/0.72 type (bytes each) gets frees in use avail bytes
% 0.48/0.72 sym_ent ( 304) 467 0 467 0 138.6 K
% 0.48/0.72 term ( 32) 249245 229891 19354 23 605.5 K
% 0.48/0.72 rel ( 40) 213564 193040 20524 22 802.6 K
% 0.48/0.72 term_ptr ( 16) 83544 18152 65392 0 1021.8 K
% 0.48/0.72 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 0.48/0.72 fpa_head ( 24) 7293 866 6427 0 150.6 K
% 0.48/0.72 fpa_tree ( 56) 33839 33839 0 47 2.6 K
% 0.48/0.72 context (1288) 30605 30605 0 6 7.5 K
% 0.48/0.72 trail ( 24) 82669 82669 0 8 0.2 K
% 0.48/0.72 imd_tree ( 32) 562 141 421 6 13.3 K
% 0.48/0.72 imd_pos (4024) 14072 14072 0 3 11.8 K
% 0.48/0.72 is_tree ( 24) 9074 1836 7238 0 169.6 K
% 0.48/0.72 is_pos (2424) 175116 175116 0 8 18.9 K
% 0.48/0.72 fsub_pos ( 16) 15741 15741 0 1 0.0 K
% 0.48/0.72 literal ( 32) 18637 13100 5537 1 173.1 K
% 0.48/0.72 clause ( 88) 8288 5482 2806 1 241.2 K
% 0.48/0.72 list ( 272) 719 712 7 2 2.4 K
% 0.48/0.72 clash_nd ( 80) 2145 2145 0 3 0.2 K
% 0.48/0.72 clause_ptr ( 16) 2967 768 2199 2 34.4 K
% 0.48/0.72 int_ptr ( 16) 32027 25489 6538 5 102.2 K
% 0.48/0.72 ci_ptr ( 24) 0 0 0 0 0.0 K
% 0.48/0.72 link_node ( 120) 0 0 0 0 0.0 K
% 0.48/0.72 ans_lit_node( 24) 0 0 0 0 0.0 K
% 0.48/0.72 formula_box( 168) 0 0 0 0 0.0 K
% 0.48/0.72 formula( 40) 5734 5734 0 3555 138.9 K
% 0.48/0.72 formula_ptr( 16) 709 709 0 709 11.1 K
% 0.48/0.72 cl_attribute( 24) 0 0 0 0 0.0 K
% 0.48/0.72
% 0.48/0.72 ********** is_delete, can't find end.
% 0.48/0.72 0.00
% 0.48/0.72 back subsume 0.00
% 0.48/0.72 factor time 0.00
% 0.48/0.72 FINDER time 0.00
% 0.48/0.72 unindex time 0.00
% 0.48/0.72
% 0.48/0.72 Forward subsumption counts, subsumer:number_subsumed.
% 0.48/0.72 1:0 2:0 3:0 4:1 5:1 6:1 7:0 8:0 9:0 10:0
% 0.48/0.72 11:0 12:0 13:0 14:1 15:1 16:0 17:0 18:0 19:0 20:1
% 0.48/0.72 21:1 22:1 23:1 24:2 25:2 26:0 27:0 28:0 29:0 30:0
% 0.48/0.72 31:0 32:0 33:0 34:0 35:0 36:0 37:0 38:0 39:0 40:0
% 0.48/0.72 41:0 42:1 43:2 44:1 45:2 46:2 47:2 48:0 49:0 50:0
% 0.48/0.72 51:0 52:0 53:0 54:0 55:0 56:1 57:1 58:1 59:1 60:2
% 0.48/0.72 61:3 62:1 63:2 64:0 65:0 66:0 67:0 68:0 69:0 70:0
% 0.48/0.72 71:0 72:1 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 0.48/0.72 81:0 82:0 83:3 84:3 85:3 86:3 87:1 88:1 89:1 90:3
% 0.48/0.72 91:3 92:0 93:0 94:0 95:0 96:2 97:0 98:0 99:0
% 0.48/0.72 All others: 4503.
% 0.48/0.72
% 0.48/0.72 ********** ABNORMAL END **********
% 0.48/0.72
% 0.48/0.72 ********** is_delete, can't find end.
%------------------------------------------------------------------------------