%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SCT171+3 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 22:12:35 EDT 2022
% Result : Unknown 1.84s 2.07s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SCT171+3 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.13 % Command : sos-script %s
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sat Jul 2 06:32:15 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.53/0.71 ----- Otter 3.2, August 2001 -----
% 0.53/0.71 The process was started by sandbox on n020.cluster.edu,
% 0.53/0.71 Sat Jul 2 06:32:15 2022
% 0.53/0.71 The command was "./sos". The process ID is 28992.
% 0.53/0.71
% 0.53/0.71 set(prolog_style_variables).
% 0.53/0.71 set(auto).
% 0.53/0.71 dependent: set(auto1).
% 0.53/0.71 dependent: set(process_input).
% 0.53/0.71 dependent: clear(print_kept).
% 0.53/0.71 dependent: clear(print_new_demod).
% 0.53/0.71 dependent: clear(print_back_demod).
% 0.53/0.71 dependent: clear(print_back_sub).
% 0.53/0.71 dependent: set(control_memory).
% 0.53/0.71 dependent: assign(max_mem, 12000).
% 0.53/0.71 dependent: assign(pick_given_ratio, 4).
% 0.53/0.71 dependent: assign(stats_level, 1).
% 0.53/0.71 dependent: assign(pick_semantic_ratio, 3).
% 0.53/0.71 dependent: assign(sos_limit, 5000).
% 0.53/0.71 dependent: assign(max_weight, 60).
% 0.53/0.71 clear(print_given).
% 0.53/0.71
% 0.53/0.71 formula_list(usable).
% 0.53/0.71
% 0.53/0.71 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=1, max_lits=14.
% 0.53/0.71
% 0.53/0.71 This ia a non-Horn set with equality. The strategy will be
% 0.53/0.71 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.53/0.71 unit deletion, with positive clauses in sos and nonpositive
% 0.53/0.71 clauses in usable.
% 0.53/0.71
% 0.53/0.71 dependent: set(knuth_bendix).
% 0.53/0.71 dependent: set(para_from).
% 0.53/0.71 dependent: set(para_into).
% 0.53/0.71 dependent: clear(para_from_right).
% 0.53/0.71 dependent: clear(para_into_right).
% 0.53/0.71 dependent: set(para_from_vars).
% 0.53/0.71 dependent: set(eq_units_both_ways).
% 0.53/0.71 dependent: set(dynamic_demod_all).
% 0.53/0.71 dependent: set(dynamic_demod).
% 0.53/0.71 dependent: set(order_eq).
% 0.53/0.71 dependent: set(back_demod).
% 0.53/0.71 dependent: set(lrpo).
% 0.53/0.71 dependent: set(hyper_res).
% 0.53/0.71 dependent: set(unit_deletion).
% 0.53/0.71 dependent: set(factor).
% 0.53/0.71
% 0.53/0.71 There is a clause for symmetry of equality, so it is
% 0.53/0.71 assumed that equality is fully axiomatized; therefore,
% 0.53/0.71 paramodulation is disabled.
% 0.53/0.71
% 0.53/0.71 dependent: clear(para_from).
% 0.53/0.71 dependent: clear(para_into).
% 0.53/0.71
% 0.53/0.71 ------------> process usable:
% 0.53/0.71 Following clause subsumed by 99 during input processing: 0 [] {-} -is_Arr1861959080le_alt(A)| -is_Arr1861959080le_alt(B)| -is_Arr1861959080le_alt(C)| -is_Arr1861959080le_alt(D)|hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,A),B)!=hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,C),D)|A=C.
% 0.53/0.71 Following clause subsumed by 100 during input processing: 0 [] {-} -is_Arr1861959080le_alt(A)| -is_Arr1861959080le_alt(B)| -is_Arr1861959080le_alt(C)| -is_Arr1861959080le_alt(D)|hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,A),B)!=hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,C),D)|B=D.
% 0.53/0.71 Following clause subsumed by 161 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,e),d)),hAPP_A568203993t_bool(hAPP_f393984045t_bool(arrow_1644373103_mktop,hAPP_A1677245848t_bool(p,A)),e)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,b),a)),lab)).
% 0.53/0.71 Following clause subsumed by 181 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),C)).
% 0.53/0.71 Following clause subsumed by 182 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),C))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),C)).
% 0.53/0.71 Following clause subsumed by 183 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),C))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),C)).
% 0.53/0.71 Following clause subsumed by 184 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,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.53/0.71 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 178 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 180 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,B),A)).
% 0.53/0.71 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 178 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 180 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,B),A)).
% 0.53/0.71 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),A))|hBOOL(C).
% 0.53/0.71 Following clause subsumed by 178 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),A))|hBOOL(C).
% 0.53/0.71 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),A))|hBOOL(C).
% 0.53/0.71 Following clause subsumed by 180 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,B),A))|hBOOL(C).
% 0.53/0.71 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 178 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),A)).
% 0.53/0.71 Following clause subsumed by 180 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,B),A)).
% 0.53/0.71 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),A)).
% 0.54/0.73 Following clause subsumed by 178 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),A)).
% 0.54/0.73 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),A)).
% 0.54/0.73 Following clause subsumed by 180 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,B),A)).
% 0.54/0.73 Following clause subsumed by 205 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|A!=B.
% 0.54/0.73 Following clause subsumed by 206 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|A!=B.
% 0.54/0.73 Following clause subsumed by 207 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|A!=B.
% 0.54/0.73 Following clause subsumed by 208 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.54/0.73 Following clause subsumed by 208 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,B),A))|B!=A.
% 0.54/0.73 Following clause subsumed by 180 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,B),A)).
% 0.54/0.73 Following clause subsumed by 208 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.54/0.73 Following clause subsumed by 208 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.54/0.73 Following clause subsumed by 204 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),A)).
% 0.54/0.73 Following clause subsumed by 160 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),e)),hAPP_A568203993t_bool(hAPP_f393984045t_bool(arrow_1644373103_mktop,hAPP_A1677245848t_bool(p,A)),e)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,n),one_one_nat)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lba)).
% 0.54/0.73 Following clause subsumed by 160 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),e)),hAPP_A568203993t_bool(hAPP_f393984045t_bool(arrow_1644373103_mktop,hAPP_A1677245848t_bool(p,A)),e)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lab))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lba)).
% 0.56/0.75 Following clause subsumed by 160 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hAPP_A1637648121di_nat(h,A)!=n|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),e)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_230821333_above,hAPP_A1677245848t_bool(p,A)),c),e)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,n),one_one_nat)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lba)).
% 0.56/0.75 Following clause subsumed by 160 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hAPP_A1637648121di_nat(h,A)!=n|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),e)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_230821333_above,hAPP_A1677245848t_bool(p,A)),c),e)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lab))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lba)).
% 0.56/0.75 Following clause subsumed by 160 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hAPP_A1637648121di_nat(h,A)=n|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),e)),hAPP_A568203993t_bool(hAPP_f393984045t_bool(arrow_1495666017_mkbot,hAPP_A1677245848t_bool(p,A)),e)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,n),one_one_nat)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lba)).
% 0.56/0.75 Following clause subsumed by 160 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_A1637648121di_nat(h,A)),n))|hAPP_A1637648121di_nat(h,A)=n|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),e)),hAPP_A568203993t_bool(hAPP_f393984045t_bool(arrow_1495666017_mkbot,hAPP_A1677245848t_bool(p,A)),e)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lab))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),lba)).
% 0.56/0.75 Following clause subsumed by 361 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))|hBOOL(B)| -hBOOL(A).
% 0.56/0.75 Following clause subsumed by 347 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),C))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 348 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),C))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 349 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),C))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 350 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),C))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 351 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),C))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 352 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),C))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 353 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),C))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 354 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,B),C))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 355 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.56/0.75 Following clause subsumed by 356 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 357 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 358 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 359 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 360 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 361 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))| -hBOOL(A)|hBOOL(B).
% 0.56/0.75 Following clause subsumed by 361 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))|hBOOL(A)| -hBOOL(B).
% 0.56/0.75 Following clause subsumed by 362 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 363 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 364 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 365 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.56/0.75 Following clause subsumed by 366 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A))|A=B.
% 0.56/0.75 Following clause subsumed by 382 during input processing: 0 [] {-} hBOOL(A)|hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,C),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,C),A)).
% 0.56/0.75 Following clause subsumed by 383 during input processing: 0 [] {-} -hBOOL(A)| -hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,C),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,C),A)).
% 0.56/0.75 Following clause subsumed by 371 during input processing: 0 [] {-} hBOOL(A)|hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),C))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 372 during input processing: 0 [] {-} -hBOOL(A)| -hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),C))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),C)).
% 0.56/0.75 Following clause subsumed by 357 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 358 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 359 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 360 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 361 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))| -hBOOL(B)|hBOOL(A).
% 0.56/0.75 Following clause subsumed by 361 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))|hBOOL(B)| -hBOOL(A).
% 0.56/0.75 Following clause subsumed by 362 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 363 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 364 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 365 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.56/0.75 Following clause subsumed by 366 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A))|B=A.
% 0.56/0.75 Following clause subsumed by 339 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_f592646513l_bool(A,C)),hAPP_f592646513l_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 340 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_f312250286l_bool(A,C)),hAPP_f312250286l_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 341 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_f965095724l_bool(A,C)),hAPP_f965095724l_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 342 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_P606313927t_bool(A,C)),hAPP_P606313927t_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 343 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_A1785763630i_bool(A,C)),hAPP_A1785763630i_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 344 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_P1676879539t_bool(A,C)),hAPP_P1676879539t_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 345 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|hBOOL(hAPP_f2013399995l_bool(hAPP_f1721660479l_bool(ord_le893483153t_bool,hAPP_A1664620203t_bool(A,C)),hAPP_A1664620203t_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 346 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_nat_bool(A,C)),hAPP_nat_bool(B,C))).
% 0.56/0.75 Following clause subsumed by 418 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|A!=B|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B)).
% 0.56/0.75 Following clause subsumed by 357 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|A=B| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),A)).
% 0.56/0.75 Following clause subsumed by 419 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|A!=B|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B)).
% 0.56/0.75 Following clause subsumed by 358 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|A=B| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),A)).
% 0.56/0.75 Following clause subsumed by 420 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|A!=B|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B)).
% 0.56/0.75 Following clause subsumed by 359 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|A=B| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),A)).
% 0.56/0.75 Following clause subsumed by 421 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|A!=B|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 360 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|A=B| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 422 during input processing: 0 [] {-} -hBOOL(A)| -hBOOL(B)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 422 during input processing: 0 [] {-} -hBOOL(A)| -hBOOL(B)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 361 during input processing: 0 [] {-} -hBOOL(A)|hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 361 during input processing: 0 [] {-} hBOOL(A)| -hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 423 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|A!=B|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 362 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|A=B| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 424 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|A!=B|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 363 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|A=B| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 425 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)|A!=B|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 364 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)|A=B| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 426 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.56/0.76 Following clause subsumed by 365 during input processing: 0 [] {-} A=B| -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.56/0.76 Following clause subsumed by 427 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 366 during input processing: 0 [] {-} A=B| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 339 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -is_fun961089132t_bool(C)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_f592646513l_bool(A,C)),hAPP_f592646513l_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 340 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_f312250286l_bool(A,C)),hAPP_f312250286l_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 341 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_f965095724l_bool(A,C)),hAPP_f965095724l_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 342 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_P606313927t_bool(A,C)),hAPP_P606313927t_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 343 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -is_Arr43961803e_indi(C)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_A1785763630i_bool(A,C)),hAPP_A1785763630i_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 344 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_P1676879539t_bool(A,C)),hAPP_P1676879539t_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 345 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -is_Arr1861959080le_alt(C)|hBOOL(hAPP_f2013399995l_bool(hAPP_f1721660479l_bool(ord_le893483153t_bool,hAPP_A1664620203t_bool(A,C)),hAPP_A1664620203t_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 346 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,hAPP_nat_bool(A,C)),hAPP_nat_bool(B,C))).
% 0.56/0.76 Following clause subsumed by 445 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,B),A)).
% 0.56/0.76 Following clause subsumed by 206 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 207 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 205 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 208 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 462 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 470 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 472 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.56/0.76 Following clause subsumed by 445 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,B),A)).
% 0.56/0.76 Following clause subsumed by 447 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 446 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 424 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 449 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 448 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 423 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 452 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 450 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 418 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 455 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 453 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 419 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 458 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 456 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 420 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 461 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 459 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 421 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 465 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B))| -hBOOL(A)|hBOOL(B).
% 0.56/0.76 Following clause subsumed by 466 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B))|hBOOL(A)| -hBOOL(B).
% 0.56/0.76 Following clause subsumed by 462 during input processing: 0 [] {-} hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 422 during input processing: 0 [] {-} hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(A)| -hBOOL(B).
% 0.56/0.76 Following clause subsumed by 469 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 467 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 425 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 471 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 470 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 427 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 473 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.56/0.76 Following clause subsumed by 472 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.56/0.76 Following clause subsumed by 426 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A!=B.
% 0.56/0.76 Following clause subsumed by 473 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.56/0.76 Following clause subsumed by 426 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.56/0.76 Following clause subsumed by 447 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|A=B| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 449 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|A=B| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 452 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|A=B| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 455 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|A=B| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 458 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|A=B| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 461 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|A=B| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 465 during input processing: 0 [] {-} -hBOOL(A)|hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 466 during input processing: 0 [] {-} hBOOL(A)| -hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 469 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)|A=B| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 471 during input processing: 0 [] {-} A=B| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 473 during input processing: 0 [] {-} A=B| -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.56/0.76 Following clause subsumed by 466 during input processing: 0 [] {-} -hBOOL(A)|hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 465 during input processing: 0 [] {-} hBOOL(A)| -hBOOL(B)| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,B),A)).
% 0.56/0.76 Following clause subsumed by 445 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,B),A)).
% 0.56/0.76 Following clause subsumed by 474 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 477 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 480 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 483 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 486 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 489 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 462 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 494 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 470 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 472 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.56/0.76 Following clause subsumed by 473 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.56/0.76 Following clause subsumed by 208 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.56/0.76 Following clause subsumed by 447 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 449 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 452 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 455 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 458 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 461 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 465 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B))| -hBOOL(A)|hBOOL(B).
% 0.56/0.76 Following clause subsumed by 466 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B))|hBOOL(A)| -hBOOL(B).
% 0.56/0.76 Following clause subsumed by 469 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 471 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|A=B.
% 0.56/0.76 Following clause subsumed by 473 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.56/0.76 Following clause subsumed by 447 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|A=B|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 449 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|A=B|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 452 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|A=B|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 455 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|A=B|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 458 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|A=B|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 461 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|A=B|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 465 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(A)|hBOOL(B)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 466 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(A)| -hBOOL(B)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 469 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|A=B|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 471 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|A=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 473 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.56/0.76 Following clause subsumed by 500 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|B=A|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 501 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|B=A|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 502 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|B=A|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 503 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|B=A|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 504 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|B=A|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 505 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|B=A|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 466 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(B)|hBOOL(A)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 465 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(B)| -hBOOL(A)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 506 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -is_fun2093718614t_bool(B)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|B=A|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 507 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|B=A|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B)).
% 0.56/0.76 Following clause subsumed by 508 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|B=A|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.56/0.76 Following clause subsumed by 519 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,B),C))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 520 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,B),C))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 521 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,B),C))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 522 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,B),C))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 523 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,B),C))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 524 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,B),C))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 525 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,B),C))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,A),C)).
% 0.56/0.76 Following clause subsumed by 526 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,B),C))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),C)).
% 0.56/0.77 Following clause subsumed by 527 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),C)).
% 0.56/0.77 Following clause subsumed by 528 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,B),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.56/0.77 Following clause subsumed by 509 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,C),A))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 510 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,C),A))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 511 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,C),A))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 512 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,C),A))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 513 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,C),A))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 514 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,C),A))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 515 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))| -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,C),A))|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 516 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,C),A))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 517 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,C),A))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,C),B)).
% 0.56/0.77 Following clause subsumed by 518 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,C),A))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,C),B)).
% 0.56/0.77 Following clause subsumed by 422 during input processing: 0 [] {-} hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,top_top_bool),A))| -hBOOL(A)| -hBOOL(top_top_bool).
% 0.56/0.77 Following clause subsumed by 436 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,top_top_fun_nat_bool),A))|A!=top_top_fun_nat_bool.
% 0.56/0.77 Following clause subsumed by 529 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,top_to1853035173l_bool),A))|A=top_to1853035173l_bool.
% 0.56/0.77 Following clause subsumed by 531 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,top_to522745736l_bool),A))|A=top_to522745736l_bool.
% 0.56/0.77 Following clause subsumed by 533 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,top_to1714702858l_bool),A))|A=top_to1714702858l_bool.
% 0.56/0.77 Following clause subsumed by 535 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,top_top_bool),A))| -hBOOL(A)|hBOOL(top_top_bool).
% 0.56/0.77 Following clause subsumed by 536 during input processing: 0 [] {-} -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,top_top_bool),A))|hBOOL(A)| -hBOOL(top_top_bool).
% 0.56/0.77 Following clause subsumed by 537 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,top_to565915683t_bool),A))|A=top_to565915683t_bool.
% 0.56/0.77 Following clause subsumed by 539 during input processing: 0 [] {-} -is_fun2093718614t_bool(A)| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,top_to178429151t_bool),A))|A=top_to178429151t_bool.
% 0.56/0.77 Following clause subsumed by 541 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,top_to1576102282i_bool),A))|A=top_to1576102282i_bool.
% 0.56/0.77 Following clause subsumed by 543 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,top_top_fun_nat_bool),A))|A=top_top_fun_nat_bool.
% 0.56/0.77 Following clause subsumed by 544 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,top_to1257323279t_bool),A))|A=top_to1257323279t_bool.
% 0.56/0.77 Following clause subsumed by 546 during input processing: 0 [] {-} -is_Arr43961803e_indi(A)| -is_Arr43961803e_indi(B)| -hBOOL(hAPP_f1599966040l_bool(inj_on1073981917di_nat(C),D))|A=B| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),D))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,B),D))|hAPP_A1637648121di_nat(C,A)!=hAPP_A1637648121di_nat(C,B).
% 0.56/0.77 Following clause subsumed by 548 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(inj_on_nat_nat(A),B))|C=D| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hAPP_nat_nat(A,C)!=hAPP_nat_nat(A,D).
% 0.56/0.77 Following clause subsumed by 546 during input processing: 0 [] {-} -is_Arr43961803e_indi(A)| -is_Arr43961803e_indi(B)| -hBOOL(hAPP_f1599966040l_bool(inj_on1073981917di_nat(C),D))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,B),D))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),D))|hAPP_A1637648121di_nat(C,B)!=hAPP_A1637648121di_nat(C,A)|B=A.
% 0.56/0.77 Following clause subsumed by 548 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(inj_on_nat_nat(A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hAPP_nat_nat(A,C)!=hAPP_nat_nat(A,D)|C=D.
% 0.56/0.77 Following clause subsumed by 546 during input processing: 0 [] {-} -is_Arr43961803e_indi(A)| -is_Arr43961803e_indi(B)| -hBOOL(hAPP_f1599966040l_bool(inj_on1073981917di_nat(C),D))|hAPP_A1637648121di_nat(C,A)!=hAPP_A1637648121di_nat(C,B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),D))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,B),D))|A=B.
% 0.56/0.77 Following clause subsumed by 548 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(inj_on_nat_nat(A),B))|hAPP_nat_nat(A,C)!=hAPP_nat_nat(A,D)| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|C=D.
% 0.56/0.77 Following clause subsumed by 288 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),pi_Pro666468413t_bool(B,C)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,D),B))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,hAPP_P606313927t_bool(A,D)),hAPP_P324742453l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 303 during input processing: 0 [] {-} -hBOOL(hAPP_f1306865520l_bool(hAPP_f407092109l_bool(member234128621e_indi,A),pi_Pro1270767662e_indi(B,C)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,D),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,hAPP_P710098616e_indi(A,D)),hAPP_P1875867302i_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 304 during input processing: 0 [] {-} -hBOOL(hAPP_f22590837l_bool(hAPP_f1847883341l_bool(member2079083634t_unit,A),pi_Pro1122146355t_unit(B,C)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,D),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,hAPP_P1844795325t_unit(A,D)),hAPP_P332578347t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 305 during input processing: 0 [] {-} -hBOOL(hAPP_f1725204053l_bool(hAPP_f666018637l_bool(member905797074e_indi,A),pi_fun753830419e_indi(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,hAPP_f836059805e_indi(A,D)),hAPP_f1948454017i_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 306 during input processing: 0 [] {-} -hBOOL(hAPP_f597137892l_bool(hAPP_f1175923213l_bool(member989885409l_bool,A),pi_fun823343522l_bool(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,hAPP_f965095724l_bool(A,D)),hAPP_f839832464l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 307 during input processing: 0 [] {-} -hBOOL(hAPP_f770608346l_bool(hAPP_f974155917l_bool(member88647127t_unit,A),pi_fun1877263000t_unit(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,hAPP_f2008177698t_unit(A,D)),hAPP_f1891021702t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 308 during input processing: 0 [] {-} -hBOOL(hAPP_f10461143l_bool(hAPP_f1339774669l_bool(member832622164e_indi,A),pi_fun1002945429e_indi(B,C)))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,D),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,hAPP_f1693298207e_indi(A,D)),hAPP_f1552576127i_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 309 during input processing: 0 [] {-} -hBOOL(hAPP_f859154022l_bool(hAPP_f976491405l_bool(member2061588323l_bool,A),pi_fun52649508l_bool(B,C)))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,D),B))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,hAPP_f312250286l_bool(A,D)),hAPP_f1624277646l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 310 during input processing: 0 [] {-} -hBOOL(hAPP_f1644647260l_bool(hAPP_f1633671693l_bool(member872366937t_unit,A),pi_fun321364250t_unit(B,C)))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,D),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,hAPP_f646804644t_unit(A,D)),hAPP_f1866147972t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 311 during input processing: 0 [] {-} -hBOOL(hAPP_f560831258l_bool(hAPP_f1153917531l_bool(member1036419453e_indi,A),pi_fun896360044e_indi(B,C)))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,D),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,hAPP_f1582908258e_indi(A,D)),hAPP_f244157820i_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 312 during input processing: 0 [] {-} -hBOOL(hAPP_f167218729l_bool(hAPP_f1666015481l_bool(member880664588l_bool,A),pi_fun1575168891l_bool(B,C)))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,D),B))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,hAPP_f592646513l_bool(A,D)),hAPP_f210572555l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 313 during input processing: 0 [] {-} -hBOOL(hAPP_f866275871l_bool(hAPP_f1093990629l_bool(member1860104450t_unit,A),pi_fun308431217t_unit(B,C)))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,D),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,hAPP_f932121959t_unit(A,D)),hAPP_f1710744577t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 314 during input processing: 0 [] {-} -hBOOL(hAPP_f795156475l_bool(hAPP_f586217629l_bool(member1934698718e_indi,A),pi_nat660525389e_indi(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,hAPP_n1951273283e_indi(A,D)),hAPP_n821919323i_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 315 during input processing: 0 [] {-} -hBOOL(hAPP_f1637334154l_bool(hAPP_f1951378235l_bool(member_fun_nat_bool,A),pi_nat_bool(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,hAPP_nat_bool(A,D)),hAPP_n1006566506l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 316 during input processing: 0 [] {-} -hBOOL(hAPP_f537623936l_bool(hAPP_f1598887207l_bool(member1024687843t_unit,A),pi_nat_Product_unit(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,hAPP_n633340360t_unit(A,D)),hAPP_n454528608t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 289 during input processing: 0 [] {-} -hBOOL(hAPP_f1837019376l_bool(hAPP_f721935245l_bool(member797673069le_alt,A),pi_Arr1199386158le_alt(B,C)))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,D),B))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A638717112le_alt(A,D)),hAPP_A1677245848t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 290 during input processing: 0 [] {-} -hBOOL(hAPP_f1351174655l_bool(hAPP_f2127575245l_bool(member1463820796le_alt,A),pi_boo115158845le_alt(B,C)))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,D),B))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_b55004359le_alt(A,D)),hAPP_b1703662281t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 291 during input processing: 0 [] {-} -hBOOL(hAPP_f415146997l_bool(hAPP_f1868437069l_bool(member1648671474le_alt,A),pi_Pro1928973619le_alt(B,C)))| -hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,D),B))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_P504138941le_alt(A,D)),hAPP_P1341894483t_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 292 during input processing: 0 [] {-} -hBOOL(hAPP_f1252760917l_bool(hAPP_f40035149l_bool(member855864530t_bool,A),pi_Arr2020412179t_bool(B,C)))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,D),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,hAPP_A2102641565t_bool(A,D)),hAPP_A1952883197l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 293 during input processing: 0 [] {-} -hBOOL(hAPP_f599145828l_bool(hAPP_f2116028941l_bool(member2056165217t_bool,A),pi_boo175444770t_bool(B,C)))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,D),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,hAPP_b317196972t_bool(A,D)),hAPP_b1048178734l_bool(C,D))).
% 0.56/0.77 Following clause subsumed by 294 during input processing: 0 [] {-} -hBOOL(hAPP_f844512602l_bool(hAPP_f1228804237l_bool(member2075448919t_bool,A),pi_Pro610293528t_bool(B,C)))| -hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,D),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,hAPP_P741208226t_bool(A,D)),hAPP_P254387896l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 295 during input processing: 0 [] {-} -hBOOL(hAPP_f785974231l_bool(hAPP_f937842381l_bool(member383660628t_bool,A),pi_Arr1936979349t_bool(B,C)))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,D),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,hAPP_A479848479t_bool(A,D)),hAPP_A1112981887l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 296 during input processing: 0 [] {-} -hBOOL(hAPP_f651410150l_bool(hAPP_f742962061l_bool(member478669795t_bool,A),pi_boo1117000868t_bool(B,C)))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,D),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,hAPP_b1376601646t_bool(A,D)),hAPP_b517355696l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 297 during input processing: 0 [] {-} -hBOOL(hAPP_f1508442332l_bool(hAPP_f792869389l_bool(member1323987161t_bool,A),pi_Pro1880661658t_bool(B,C)))| -hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,D),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,hAPP_P58618404t_bool(A,D)),hAPP_P1171466554l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 298 during input processing: 0 [] {-} -hBOOL(hAPP_f817604743l_bool(hAPP_f1345320373l_bool(member357566570t_bool,A),pi_boo538701011t_bool(B,C)))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_b1703662281t_bool(A,D)),hAPP_b1812770943l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 299 during input processing: 0 [] {-} -hBOOL(hAPP_f1846209297l_bool(hAPP_f1865430217l_bool(member27872244t_bool,A),pi_Pro718203741t_bool(B,C)))| -hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_P1341894483t_bool(A,D)),hAPP_P1294997365l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 300 during input processing: 0 [] {-} -hBOOL(hAPP_f1632652727l_bool(hAPP_f87193621l_bool(member616133274di_nat,A),pi_Arr346900227di_nat(B,C)))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_A1637648121di_nat(A,D)),hAPP_A2046586321t_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 301 during input processing: 0 [] {-} -hBOOL(hAPP_f67777128l_bool(hAPP_f144393719l_bool(member_fun_bool_nat,A),pi_bool_nat(B,C)))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_bool_nat(A,D)),hAPP_b1013836512t_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 302 during input processing: 0 [] {-} -hBOOL(hAPP_f339859954l_bool(hAPP_f1950626059l_bool(member87760213it_nat,A),pi_Product_unit_nat(B,C)))| -hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_P426034740it_nat(A,D)),hAPP_P32877782t_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 317 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),pi_fun150026276t_bool(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_f412050202t_bool(A,D)),hAPP_f1277514478l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 318 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),pi_Arr990697634t_bool(B,C)))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(A,D)),hAPP_A60074736l_bool(C,D))).
% 0.56/0.78 Following clause subsumed by 584 during input processing: 0 [] {-} -is_Arr43961803e_indi(A)| -is_Arr43961803e_indi(B)| -hBOOL(hAPP_f1599966040l_bool(inj_on1073981917di_nat(C),top_to1576102282i_bool))|hAPP_A1637648121di_nat(C,A)!=hAPP_A1637648121di_nat(C,B)|A=B.
% 0.56/0.78 Following clause subsumed by 586 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(inj_on_nat_nat(A),top_top_fun_nat_bool))|hAPP_nat_nat(A,B)!=hAPP_nat_nat(A,C)|B=C.
% 0.56/0.78 Following clause subsumed by 474 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 475 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 476 during input processing: 0 [] {-} hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 477 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 478 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 479 during input processing: 0 [] {-} hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 480 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 481 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 482 during input processing: 0 [] {-} hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 483 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 484 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 485 during input processing: 0 [] {-} hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 486 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 487 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 488 during input processing: 0 [] {-} hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 489 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 490 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 491 during input processing: 0 [] {-} hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 494 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 495 during input processing: 0 [] {-} -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 496 during input processing: 0 [] {-} hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1393483395t_bool,A),B))| -hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,A),B))|hBOOL(hAPP_f324780729l_bool(hAPP_f1377535679l_bool(ord_le1546299023t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 470 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.78 Following clause subsumed by 497 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 498 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.78 Following clause subsumed by 775 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)|B=C.
% 0.56/0.78 Following clause subsumed by 774 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)|A=C.
% 0.56/0.78 Following clause subsumed by 775 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)|B=C.
% 0.56/0.78 Following clause subsumed by 780 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.56/0.78 Following clause subsumed by 783 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.56/0.78 Following clause subsumed by 781 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.56/0.78 Following clause subsumed by 784 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.56/0.78 Following clause subsumed by 785 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.56/0.80 Following clause subsumed by 788 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.56/0.80 Following clause subsumed by 786 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.56/0.80 Following clause subsumed by 789 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),C)).
% 0.56/0.80 Following clause subsumed by 357 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 358 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 359 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 360 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 362 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 363 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 366 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A))|A=B.
% 0.56/0.80 Following clause subsumed by 446 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 206 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 447 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 448 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 207 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 449 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 450 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 451 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 452 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 453 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 454 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 455 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 456 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 457 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 458 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 459 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 460 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 461 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 470 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 205 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 471 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 447 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 446 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 424 during input processing: 0 [] {-} -is_fun1568535512t_bool(A)| -is_fun1568535512t_bool(B)|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 449 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 448 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 423 during input processing: 0 [] {-} -is_fun1236654035i_bool(A)| -is_fun1236654035i_bool(B)|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 452 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 450 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 418 during input processing: 0 [] {-} -is_fun279392540l_bool(A)| -is_fun279392540l_bool(B)|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 455 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 453 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 419 during input processing: 0 [] {-} -is_fun158382675l_bool(A)| -is_fun158382675l_bool(B)|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))|A!=B.
% 0.56/0.80 Following clause subsumed by 458 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|A=B.
% 0.56/0.80 Following clause subsumed by 456 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B)).
% 0.56/0.80 Following clause subsumed by 420 during input processing: 0 [] {-} -is_fun288122577l_bool(A)| -is_fun288122577l_bool(B)|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))|A!=B.
% 0.56/0.81 Following clause subsumed by 461 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|A=B.
% 0.56/0.81 Following clause subsumed by 459 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 421 during input processing: 0 [] {-} -is_fun961089132t_bool(A)| -is_fun961089132t_bool(B)|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))|A!=B.
% 0.56/0.81 Following clause subsumed by 471 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|A=B.
% 0.56/0.81 Following clause subsumed by 470 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 427 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))|A!=B.
% 0.56/0.81 Following clause subsumed by 474 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 477 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 480 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 483 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 486 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 489 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 470 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 509 during input processing: 0 [] {-} -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),B))| -hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,B),C))|hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1976645739t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 510 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),C))|hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le1013403878i_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 511 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),C))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 512 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),C))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 513 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),C))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 514 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),C))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 517 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 521 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,B),C))|hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le119953481l_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 522 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,B),C))|hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le1006840166l_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 523 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,B),C))|hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1929173732l_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 524 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,B),C))|hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le906188671t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 527 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le382113706t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 427 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 436 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.81 Following clause subsumed by 356 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 1221 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),A))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),B)).
% 0.56/0.81 Following clause subsumed by 1220 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,C),A))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,C),B)).
% 0.56/0.81 Following clause subsumed by 1219 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,C),A))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,C),B)).
% 0.56/0.81 Following clause subsumed by 1218 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,C),A))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,C),B)).
% 0.56/0.81 Following clause subsumed by 1217 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,C),A))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,C),B)).
% 0.56/0.81 Following clause subsumed by 1221 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),C))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A),C)).
% 0.56/0.81 Following clause subsumed by 1220 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,B),C))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 1219 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,B),C))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 1218 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,B),C))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),C)).
% 0.56/0.81 Following clause subsumed by 1217 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,B),C))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,A),C)).
% 0.56/0.81 Following clause subsumed by 1221 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),A))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C),B)).
% 0.56/0.81 Following clause subsumed by 1220 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),B))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,C),A))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,C),B)).
% 0.56/0.81 Following clause subsumed by 1219 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),B))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,C),A))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,C),B)).
% 0.56/0.81 Following clause subsumed by 1218 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),B))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,C),A))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,C),B)).
% 0.56/0.81 Following clause subsumed by 1217 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),B))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,C),A))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,C),B)).
% 0.56/0.81 Following clause subsumed by 436 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.81 Following clause subsumed by 427 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 1222 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(A,B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),C))|hBOOL(hAPP_nat_bool(C,B)).
% 0.56/0.81 Following clause subsumed by 427 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B)).
% 0.56/0.81 Following clause subsumed by 436 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.81 Following clause subsumed by 366 during input processing: 0 [] {-} A=B| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),B))| -hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,B),A)).
% 0.56/0.81 Following clause subsumed by 212 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),A)).
% 0.56/0.81 Following clause subsumed by 208 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.56/0.81 Following clause subsumed by 204 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),A)).
% 0.56/0.81 Following clause subsumed by 212 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),A)).
% 0.56/0.81 Following clause subsumed by 204 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|B!=A.
% 0.56/0.81 Following clause subsumed by 208 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.56/0.81 Following clause subsumed by 775 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)|B=C.
% 0.56/0.81 Following clause subsumed by 777 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)|B!=C.
% 0.56/0.81 Following clause subsumed by 774 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)|A=C.
% 0.56/0.81 Following clause subsumed by 776 during input processing: 0 [] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B)|A!=C.
% 0.56/0.81 Following clause subsumed by 426 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.56/0.81 Following clause subsumed by 355 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.56/0.81 Following clause subsumed by 365 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.56/0.81 Following clause subsumed by 785 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.56/0.81 Following clause subsumed by 788 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.56/0.81 Following clause subsumed by 789 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(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C))).
% 0.56/0.81 Following clause subsumed by 787 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(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),D))).
% 0.56/0.81 Following clause subsumed by 472 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.56/0.81 Following clause subsumed by 208 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.56/0.81 Following clause subsumed by 473 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.56/0.81 Following clause subsumed by 473 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.56/0.81 Following clause subsumed by 472 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.56/0.81 Following clause subsumed by 426 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A!=B.
% 0.56/0.81 Following clause subsumed by 472 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.56/0.81 Following clause subsumed by 473 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.56/0.81 Following clause subsumed by 472 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.56/0.81 Following clause subsumed by 426 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.56/0.81 Following clause subsumed by 780 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.56/0.81 Following clause subsumed by 783 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.56/0.81 Following clause subsumed by 784 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(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C))).
% 0.56/0.81 Following clause subsumed by 782 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(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),D))).
% 0.56/0.81 Following clause subsumed by 1213 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.56/0.81 Following clause subsumed by 1212 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.56/0.81 Following clause subsumed by 1242 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),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C))).
% 0.56/0.81 Following clause subsumed by 1243 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),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B))).
% 0.56/0.81 Following clause subsumed by 472 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.56/0.81 Following clause subsumed by 1236 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,A),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,C),B))).
% 0.56/0.81 Following clause subsumed by 1235 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,A),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C))).
% 0.56/0.81 Following clause subsumed by 1254 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.56/0.81 Following clause subsumed by 204 during input processing: 0 [] {-} A!=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.56/0.81 Following clause subsumed by 1254 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.56/0.81 Following clause subsumed by 426 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),zero_zero_nat))|A!=zero_zero_nat.
% 0.56/0.81 Following clause subsumed by 1235 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.56/0.81 Following clause subsumed by 1236 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),B)).
% 0.56/0.81 Following clause subsumed by 1271 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=hAPP_nat_nat(suc,B)|A=B.
% 0.56/0.81 Following clause subsumed by 1273 during input processing: 0 [flip.1] {-} hAPP_nat_nat(suc,A)!=A.
% 0.56/0.81 Following clause subsumed by 1274 during input processing: 0 [flip.1] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.56/0.81 Following clause subsumed by 1274 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.56/0.81 Following clause subsumed by 1274 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.56/0.81 Following clause subsumed by 1274 during input processing: 0 [flip.1] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.56/0.81 Following clause subsumed by 1274 during input processing: 0 [flip.1] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.56/0.81 Following clause subsumed by 1277 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,A),hAPP_nat_nat(suc,B)))|A=B.
% 0.56/0.81 Following clause subsumed by 1275 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(suc,A)),hAPP_nat_nat(suc,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.56/0.81 Following clause subsumed by 1270 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(suc,A)),hAPP_nat_nat(suc,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.56/0.81 Following clause subsumed by 1277 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),hAPP_nat_nat(suc,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A=B.
% 0.56/0.81 Following clause subsumed by 1280 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),hAPP_nat_nat(suc,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.56/0.81 Following clause subsumed by 1286 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),hAPP_nat_nat(suc,B)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A=hAPP_nat_nat(suc,B).
% 0.64/0.82 Following clause subsumed by 1287 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),hAPP_nat_nat(suc,B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.64/0.82 Following clause subsumed by 426 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),hAPP_nat_nat(suc,B)))|A!=hAPP_nat_nat(suc,B).
% 0.64/0.82 Following clause subsumed by 1283 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),hAPP_nat_nat(suc,zero_zero_nat)))|A!=zero_zero_nat.
% 0.64/0.82 Following clause subsumed by 1301 during input processing: 0 [flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(suc,zero_zero_nat)|A=hAPP_nat_nat(suc,zero_zero_nat)|A=zero_zero_nat.
% 0.64/0.82 Following clause subsumed by 1302 during input processing: 0 [flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(suc,zero_zero_nat)|A=hAPP_nat_nat(suc,zero_zero_nat)|B=hAPP_nat_nat(suc,zero_zero_nat).
% 0.64/0.82 Following clause subsumed by 1303 during input processing: 0 [flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(suc,zero_zero_nat)|B=zero_zero_nat|A=zero_zero_nat.
% 0.64/0.82 Following clause subsumed by 1304 during input processing: 0 [flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)!=hAPP_nat_nat(suc,zero_zero_nat)|B=zero_zero_nat|B=hAPP_nat_nat(suc,zero_zero_nat).
% 0.64/0.82 Following clause subsumed by 1305 during input processing: 0 [flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)=hAPP_nat_nat(suc,zero_zero_nat)|A!=hAPP_nat_nat(suc,zero_zero_nat)|B!=zero_zero_nat.
% 0.64/0.82 Following clause subsumed by 1306 during input processing: 0 [flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)=hAPP_nat_nat(suc,zero_zero_nat)|A!=zero_zero_nat|B!=hAPP_nat_nat(suc,zero_zero_nat).
% 0.64/0.82 Following clause subsumed by 1311 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,A)),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.64/0.82 Following clause subsumed by 1310 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,A)),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.64/0.82 Following clause subsumed by 1313 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),hAPP_nat_nat(suc,B))).
% 0.64/0.82 Following clause subsumed by 1310 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,hAPP_nat_nat(suc,A)),B)).
% 0.64/0.82 Following clause subsumed by 1283 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,B),hAPP_nat_nat(suc,A)))|B!=A.
% 0.64/0.82 Following clause subsumed by 1311 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,A)),B))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B)).
% 0.64/0.82 Following clause subsumed by 1351 during input processing: 0 [flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)!=one_one_nat|A=one_one_nat.
% 0.64/0.82 Following clause subsumed by 1352 during input processing: 0 [flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)!=one_one_nat|B=one_one_nat.
% 0.64/0.82 Following clause subsumed by 1353 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.64/0.82 Following clause subsumed by 1369 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.86/1.11 Following clause subsumed by 1368 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.86/1.11 Following clause subsumed by 1373 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(times_times_nat(hAPP_nat_nat(suc,A)),B)),hAPP_nat_nat(times_times_nat(hAPP_nat_nat(suc,A)),C)))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 0.86/1.11 Following clause subsumed by 1349 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(times_times_nat(hAPP_nat_nat(suc,A)),B)),hAPP_nat_nat(times_times_nat(hAPP_nat_nat(suc,A)),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.86/1.11 Following clause subsumed by 1348 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.86/1.11 Following clause subsumed by 1349 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.86/1.11 Following clause subsumed by 1388 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.86/1.11 Following clause subsumed by 1349 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.86/1.11 Following clause subsumed by 1373 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.86/1.11 Following clause subsumed by 1368 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.86/1.11 Following clause subsumed by 1360 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.86/1.11 Following clause subsumed by 1359 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.86/1.11 Following clause subsumed by 1361 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.86/1.11 Following clause subsumed by 1360 during input processing: 0 [] {-} hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(A),C)|B!=C.
% 0.86/1.11 Following clause subsumed by 1401 during input processing: 0 [] {-} -is_bool(A)|A=fTrue|A=fFalse.
% 0.86/1.11 Following clause subsumed by 1401 during input processing: 0 [] {-} -is_bool(A)|A=fTrue|A=fFalse.
% 0.86/1.11 172 back subsumes 171.
% 0.86/1.11 205 back subsumes 151.
% 0.86/1.11 206 back subsumes 153.
% 0.86/1.11 207 back subsumes 150.
% 0.86/1.11 418 back subsumes 407.
% 0.86/1.11 419 back subsumes 408.
% 0.86/1.11 420 back subsumes 409.
% 0.86/1.11 421 back subsumes 410.
% 0.86/1.11 422 back subsumes 412.
% 0.86/1.11 423 back subsumes 413.
% 0.86/1.11 424 back subsumes 414.
% 0.86/1.11 425 back subsumes 415.
% 0.86/1.11 426 back subsumes 416.
% 0.86/1.11 427 back subsumes 417.
% 0.86/1.11 463 back subsumes 145.
% 0.86/1.11 464 back subsumes 146.
% 0.86/1.11 474 back subsumes 446.
% 0.86/1.11 477 back subsumes 448.
% 0.86/1.11 480 back subsumes 450.
% 0.86/1.11 483 back subsumes 453.
% 0.86/1.11 486 back subsumes 456.
% 0.86/1.11 489 back subsumes 459.
% 0.86/1.11 494 back subsumes 467.
% 0.86/1.11 1235 back subsumes 271.
% 0.86/1.11 1283 back subsumes 1282.
% 1.42/1.61 1360 back subsumes 1355.
% 1.42/1.61 1440 back subsumes 95.
% 1.42/1.61 1470 back subsumes 1466.
% 1.42/1.61 1650 back subsumes 1647.
% 1.42/1.61 1650 back subsumes 1643.
% 1.42/1.61 1650 back subsumes 1631.
% 1.42/1.61 1660 back subsumes 1633.
% 1.42/1.61 1662 back subsumes 1635.
% 1.42/1.61 1668 back subsumes 1664.
% 1.42/1.61 1668 back subsumes 1644.
% 1.42/1.61 1669 back subsumes 1665.
% 1.42/1.61 1669 back subsumes 1645.
% 1.42/1.61
% 1.42/1.61 ------------> process sos:
% 1.42/1.61 Following clause subsumed by 1992 during input processing: 0 [] {-} hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,A),top_to1647826457l_bool)).
% 1.42/1.61 Following clause subsumed by 1993 during input processing: 0 [] {-} hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),top_to1576102282i_bool)).
% 1.42/1.61 Following clause subsumed by 1994 during input processing: 0 [] {-} hBOOL(hAPP_f2028818269l_bool(hAPP_P607165281l_bool(member_Product_unit,A),top_to1257323279t_bool)).
% 1.42/1.61 Following clause subsumed by 1995 during input processing: 0 [] {-} hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,A),top_to565915683t_bool)).
% 1.42/1.61 Following clause subsumed by 1996 during input processing: 0 [] {-} hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),top_to522745736l_bool)).
% 1.42/1.61 Following clause subsumed by 1997 during input processing: 0 [] {-} hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),top_to1714702858l_bool)).
% 1.42/1.61 Following clause subsumed by 1998 during input processing: 0 [] {-} hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),top_to1853035173l_bool)).
% 1.42/1.61 Following clause subsumed by 1999 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A),top_top_fun_nat_bool)).
% 1.42/1.61 Following clause subsumed by 2014 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)).
% 1.42/1.61 Following clause subsumed by 2014 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,B),A))|B=A.
% 1.42/1.61 Following clause subsumed by 2014 during input processing: 0 [] {-} 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)).
% 1.42/1.61 Following clause subsumed by 2014 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,B),A))|A=B.
% 1.42/1.61 Following clause subsumed by 2014 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)).
% 1.42/1.61 Following clause subsumed by 2060 during input processing: 0 [] {-} hBOOL(A)|hBOOL(B)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B)).
% 1.42/1.61 Following clause subsumed by 2060 during input processing: 0 [] {-} hBOOL(A)|hBOOL(B)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,B),A)).
% 1.42/1.61 Following clause subsumed by 2059 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)).
% 1.42/1.61 Following clause subsumed by 2064 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,B),A)).
% 1.42/1.61 Following clause subsumed by 2064 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,B),A)).
% 1.42/1.61 Following clause subsumed by 2060 during input processing: 0 [] {-} hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,A),B))|hBOOL(A)|hBOOL(B).
% 1.42/1.61 Following clause subsumed by 2064 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,B),A)).
% 1.42/1.63 Following clause subsumed by 2064 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,B),A)).
% 1.42/1.63 Following clause subsumed by 2060 during input processing: 0 [] {-} hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(ord_less_eq_bool,top_top_bool),A))|hBOOL(A)|hBOOL(top_top_bool).
% 1.42/1.63 Following clause subsumed by 2065 during input processing: 0 [] {-} hBOOL(hAPP_f1749234559l_bool(hAPP_f1581553471l_bool(ord_le2085964885l_bool,A),top_to1853035173l_bool)).
% 1.42/1.63 Following clause subsumed by 2066 during input processing: 0 [] {-} hBOOL(hAPP_f777333846l_bool(hAPP_f1146952189l_bool(ord_le1069525464l_bool,A),top_to522745736l_bool)).
% 1.42/1.63 Following clause subsumed by 2067 during input processing: 0 [] {-} hBOOL(hAPP_f250445784l_bool(hAPP_f43523585l_bool(ord_le2009287770l_bool,A),top_to1714702858l_bool)).
% 1.42/1.63 Following clause subsumed by 2069 during input processing: 0 [] {-} hBOOL(hAPP_f592646513l_bool(hAPP_f863359027l_bool(ord_le1004900979t_bool,A),top_to565915683t_bool)).
% 1.42/1.63 Following clause subsumed by 2071 during input processing: 0 [] {-} hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),top_to1576102282i_bool)).
% 1.42/1.63 Following clause subsumed by 2072 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),top_top_fun_nat_bool)).
% 1.42/1.63 Following clause subsumed by 2073 during input processing: 0 [] {-} hBOOL(hAPP_f2028818269l_bool(hAPP_f272527115l_bool(ord_le1874503007t_bool,A),top_to1257323279t_bool)).
% 1.42/1.63 Following clause subsumed by 2054 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,A),A)).
% 1.42/1.63 Following clause subsumed by 2014 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)).
% 1.42/1.63 Following clause subsumed by 2014 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)).
% 1.42/1.63 Following clause subsumed by 2014 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)).
% 1.42/1.63 Following clause subsumed by 2053 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),A)).
% 1.42/1.63 Following clause subsumed by 2059 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)).
% 1.42/1.63 Following clause subsumed by 2166 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 1.42/1.63 Following clause subsumed by 2165 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),A)).
% 1.42/1.63 1973 back subsumes 259.
% 1.42/1.63 1974 back subsumes 155.
% 1.42/1.63 1985 back subsumes 116.
% 1.42/1.63 1986 back subsumes 118.
% 1.42/1.63 1987 back subsumes 120.
% 1.42/1.63 1988 back subsumes 122.
% 1.42/1.63 1989 back subsumes 124.
% 1.42/1.63 1990 back subsumes 126.
% 1.42/1.63 1991 back subsumes 128.
% 1.42/1.63 2005 back subsumes 278.
% 1.42/1.63 2005 back subsumes 275.
% 1.42/1.63 2005 back subsumes 272.
% 1.42/1.63 2005 back subsumes 269.
% 1.42/1.63 2005 back subsumes 266.
% 1.42/1.63 2005 back subsumes 263.
% 1.42/1.63 2005 back subsumes 260.
% 1.42/1.63 2006 back subsumes 164.
% 1.42/1.63 2006 back subsumes 163.
% 1.42/1.63 2006 back subsumes 162.
% 1.42/1.63 2038 back subsumes 258.
% 1.42/1.63 2049 back subsumes 1685.
% 1.42/1.63 2053 back subsumes 1710.
% 1.42/1.63 2053 back subsumes 1709.
% 1.42/1.63 2053 back subsumes 1708.
% 1.42/1.63 2060 back subsumes 411.
% 1.42/1.63 2064 back subsumes 499.
% 1.42/1.63 Following clause subsumed by 2140 during input processing: 0 [copy,2140,flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),A).
% 1.42/1.63 Following clause subsumed by 2141 during input processing: 0 [copy,2141,flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C))=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),C)).
% 1.73/1.93 Following clause subsumed by 2347 during input processing: 0 [copy,2143,flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C))=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),C)).
% 1.73/1.93 Following clause subsumed by 2347 during input processing: 0 [copy,2180,flip.1,demod,2193,2193] {-} hAPP_f22106695ol_nat(finite_card_nat,hAPP_n1699378549t_bool(hAPP_f229349961t_bool(cOMBC_nat_nat_bool,ord_less_eq_nat),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)))=hAPP_f22106695ol_nat(finite_card_nat,hAPP_n1699378549t_bool(hAPP_f229349961t_bool(cOMBC_nat_nat_bool,ord_less_eq_nat),hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B))).
% 1.73/1.93 Following clause subsumed by 2249 during input processing: 0 [copy,2249,flip.1] {-} hAPP_nat_nat(times_times_nat(A),B)=hAPP_nat_nat(times_times_nat(B),A).
% 1.73/1.93 Following clause subsumed by 2347 during input processing: 0 [copy,2266,flip.1] {-} zero_zero_nat=zero_zero_nat.
% 1.73/1.93 Following clause subsumed by 2347 during input processing: 0 [copy,2347,flip.1] {-} A=A.
% 1.73/1.93 2347 back subsumes 2266.
% 1.73/1.93 2347 back subsumes 2143.
% 1.73/1.93 2347 back subsumes 1871.
% 1.73/1.93 2347 back subsumes 1815.
% 1.73/1.93 2347 back subsumes 1814.
% 1.73/1.93 2347 back subsumes 1810.
% 1.73/1.93 2347 back subsumes 1808.
% 1.73/1.93 2347 back subsumes 1806.
% 1.73/1.93 2347 back subsumes 1802.
% 1.73/1.93 2347 back subsumes 1801.
% 1.73/1.93 2347 back subsumes 1798.
% 1.73/1.93 2347 back subsumes 1699.
% 1.73/1.93 2347 back subsumes 1698.
% 1.73/1.93 2347 back subsumes 1697.
% 1.73/1.93 2347 back subsumes 1696.
% 1.73/1.93 2347 back subsumes 1695.
% 1.73/1.93 2347 back subsumes 1694.
% 1.73/1.93 2347 back subsumes 1693.
% 1.73/1.93 2347 back subsumes 1680.
% 1.73/1.93 2347 back subsumes 1679.
% 1.73/1.93 2347 back subsumes 1678.
% 1.73/1.93 2347 back subsumes 1677.
% 1.73/1.93 2347 back subsumes 1676.
% 1.73/1.93 2347 back subsumes 1675.
% 1.73/1.93 2347 back subsumes 1674.
% 1.73/1.93 2347 back subsumes 1673.
% 1.73/1.93 2347 back subsumes 1672.
% 1.73/1.93 2347 back subsumes 1605.
% 1.73/1.93 2347 back subsumes 1604.
% 1.73/1.93 2347 back subsumes 1599.
% 1.73/1.93 2347 back subsumes 1598.
% 1.73/1.93 2347 back subsumes 1548.
% 1.73/1.93 2347 back subsumes 1533.
% 1.73/1.93 2347 back subsumes 1524.
% 1.73/1.93 Following clause subsumed by 2234 during input processing: 0 [copy,2449,flip.1] {-} hAPP_nat_nat(times_times_nat(hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,A),B)),C)=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,hAPP_nat_nat(times_times_nat(A),C)),hAPP_nat_nat(times_times_nat(B),C)).
% 1.73/1.93 Following clause subsumed by 2246 during input processing: 0 [copy,2450,flip.1] {-} hAPP_nat_nat(times_times_nat(hAPP_f22106695ol_nat(finite_card_nat,hAPP_n1699378549t_bool(hAPP_f229349961t_bool(cOMBC_nat_nat_bool,ord_less_eq_nat),A))),B)=hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,B),hAPP_nat_nat(times_times_nat(A),B)).
% 1.73/1.93 Following clause subsumed by 2292 during input processing: 0 [copy,2453,flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(hAPP_f416620757at_nat(cOMBC_nat_nat_nat,A),B),C)=hAPP_nat_nat(hAPP_nat_fun_nat_nat(A,C),B).
% 1.73/1.93 Following clause subsumed by 2293 during input processing: 0 [copy,2454,flip.1] {-} hAPP_nat_bool(hAPP_n1699378549t_bool(hAPP_f229349961t_bool(cOMBC_nat_nat_bool,A),B),C)=hAPP_nat_bool(hAPP_n1699378549t_bool(A,C),B).
% 1.73/1.93 Following clause subsumed by 2302 during input processing: 0 [copy,2455,flip.1] {-} hAPP_n1699378549t_bool(hAPP_f618557131t_bool(cOMBB_800536526ol_nat(A),B),C)=hAPP_n1699378549t_bool(A,hAPP_nat_nat(B,C)).
% 1.73/1.93 Following clause subsumed by 2305 during input processing: 0 [copy,2456,flip.1] {-} hAPP_n1006566506l_bool(hAPP_f1146629647l_bool(cOMBB_1015721476ol_nat(A),B),C)=hAPP_b589554111l_bool(A,hAPP_nat_bool(B,C)).
% 1.73/1.93 Following clause subsumed by 2311 during input processing: 0 [copy,2457,flip.1] {-} hAPP_n215258509l_bool(hAPP_f66927821l_bool(cOMBB_1146692694ol_nat(A),B),C)=hAPP_n215258509l_bool(A,hAPP_nat_nat(B,C)).
% 1.73/1.93 Following clause subsumed by 2312 during input processing: 0 [copy,2458,flip.1] {-} hAPP_A2046586321t_bool(hAPP_f224734595t_bool(cOMBB_1883918730e_indi(A),B),C)=hAPP_n1699378549t_bool(A,hAPP_A1637648121di_nat(B,C)).
% 1.73/1.93 Following clause subsumed by 2317 during input processing: 0 [copy,2459,flip.1] {-} hAPP_A862370221t_bool(hAPP_f1663053423t_bool(hAPP_f653880381t_bool(cOMBC_1635684702l_bool,A),B),C)=hAPP_f592646513l_bool(hAPP_A187815023l_bool(A,C),B).
% 1.84/2.06 Following clause subsumed by 2320 during input processing: 0 [copy,2460,flip.1] {-} hAPP_A1677245848t_bool(hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,A),B),C)=hAPP_A568203993t_bool(hAPP_A1625428400t_bool(A,C),B).
% 1.84/2.06 Following clause subsumed by 2321 during input processing: 0 [copy,2461,flip.1] {-} hAPP_A1664620203t_bool(hAPP_f1617919085t_bool(hAPP_f2058969401t_bool(cOMBC_364043868t_bool,A),B),C)=hAPP_f1663053423t_bool(hAPP_A572596845t_bool(A,C),B).
% 1.84/2.06 2479 back subsumes 2477.
% 1.84/2.06 2479 back subsumes 2474.
% 1.84/2.06 2485 back subsumes 2481.
% 1.84/2.06 2507 back subsumes 2506.
% 1.84/2.06 2509 back subsumes 2508.
% 1.84/2.06 2513 back subsumes 2512.
% 1.84/2.06 2518 back subsumes 2514.
% 1.84/2.06 2533 back subsumes 2528.
% 1.84/2.06 2533 back subsumes 2521.
% 1.84/2.06 2537 back subsumes 2536.
% 1.84/2.06 2539 back subsumes 2538.
% 1.84/2.06 2543 back subsumes 2540.
% 1.84/2.06 2544 back subsumes 2541.
% 1.84/2.06 2558 back subsumes 2553.
% 1.84/2.06 2558 back subsumes 2549.
% 1.84/2.06 2584 back subsumes 2583.
% 1.84/2.06 2591 back subsumes 2589.
% 1.84/2.06 2591 back subsumes 2586.
% 1.84/2.06 2594 back subsumes 2593.
% 1.84/2.06 2600 back subsumes 2598.
% 1.84/2.06 2600 back subsumes 2596.
% 1.84/2.06 Following clause subsumed by 2325 during input processing: 0 [copy,2691,flip.1] {-} hAPP_A1625428400t_bool(hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,A),B),C)=hAPP_A1941004017t_bool(hAPP_A621939144t_bool(A,C),B).
% 1.84/2.06 Following clause subsumed by 2328 during input processing: 0 [copy,2692,flip.1] {-} hAPP_A187815023l_bool(hAPP_f1539445765l_bool(cOMBB_84213429le_alt(A),B),C)=hAPP_P229966473l_bool(A,hAPP_A702847159le_alt(B,C)).
% 1.84/2.06 Following clause subsumed by 2329 during input processing: 0 [copy,2693,flip.1] {-} hAPP_A1677245848t_bool(hAPP_f329301088t_bool(hAPP_f573120177t_bool(cOMBC_633721483t_bool,A),B),C)=hAPP_f515126293t_bool(hAPP_A1102281708t_bool(A,C),B).
% 1.84/2.06 Following clause subsumed by 2330 during input processing: 0 [copy,2694,flip.1] {-} hAPP_A1677245848t_bool(hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(A),B),C)=hAPP_f515126293t_bool(hAPP_A1102281708t_bool(A,C),hAPP_A1677245848t_bool(B,C)).
% 1.84/2.06 Following clause subsumed by 2333 during input processing: 0 [copy,2695,flip.1] {-} hAPP_A1625428400t_bool(hAPP_f721938099t_bool(cOMBB_2032668066e_indi(A),B),C)=hAPP_f393984045t_bool(A,hAPP_A1677245848t_bool(B,C)).
% 1.84/2.06 Following clause subsumed by 2336 during input processing: 0 [copy,2696,flip.1] {-} hAPP_A1553574765l_bool(hAPP_f156764033l_bool(cOMBB_2112722489le_alt(A),B),C)=hAPP_f1539445765l_bool(A,hAPP_A1505516597le_alt(B,C)).
% 1.84/2.06 Following clause subsumed by 2337 during input processing: 0 [copy,2697,flip.1] {-} hAPP_A621939144t_bool(hAPP_f210227915t_bool(cOMBB_1769989562e_indi(A),B),C)=hAPP_f344580165t_bool(A,hAPP_A1677245848t_bool(B,C)).
% 1.84/2.06 Following clause subsumed by 2342 during input processing: 0 [copy,2698,flip.1] {-} hAPP_A1102281708t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(A),B),C)=hAPP_A1102281708t_bool(hAPP_f1909278132t_bool(hAPP_f1297018969t_bool(cOMBC_510421983t_bool,A),hAPP_A1677245848t_bool(B,C)),C).
% 1.84/2.06 Following clause subsumed by 2343 during input processing: 0 [copy,2699,flip.1] {-} hAPP_A572596845t_bool(hAPP_f1324249913t_bool(cOMBB_747702273le_alt(A),B),C)=hAPP_f653880381t_bool(A,hAPP_A1553574765l_bool(B,C)).
% 1.84/2.06 Following clause subsumed by 2344 during input processing: 0 [copy,2700,flip.1] {-} hAPP_A1455239488t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(A),B),C)=hAPP_b1588041841t_bool(A,hAPP_A1785763630i_bool(B,C)).
% 1.84/2.06
% 1.84/2.06 ======= end of input processing =======
% 1.84/2.06
% 1.84/2.06 SEGMENTATION FAULT!! This is probably caused by a
% 1.84/2.06 bug in Otter. Please send copy of the input file to
% 1.84/2.06 otter@mcs.anl.gov, let us know what version of Otter you are
% 1.84/2.06 using, and send any other info that might be useful.
% 1.84/2.06
% 1.84/2.06
% 1.84/2.06 SEGMENTATION FAULT!! This is probably caused by a
% 1.84/2.06 bug in Otter. Please send copy of the input file to
% 1.84/2.06 otter@mcs.anl.gov, let us know what version of Otter you are
% 1.84/2.06 using, and send any other info that might be useful.
% 1.84/2.06
% 1.84/2.06
% 1.84/2.06 The job finished Sat Jul 2 06:32:17 2022
%------------------------------------------------------------------------------