SOS---2.0.UNK-Non.f

%------------------------------------------------------------------------------
% File     : SOS---2.0
% Problem  : SCT170+3 : TPTP v8.1.0. Released v5.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : sos-script %s

% Computer : n025.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:31 EDT 2022

% Result   : Unknown 2.11s 2.33s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SCT170+3 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.12  % Command  : sos-script %s
% 0.13/0.33  % Computer : n025.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Sat Jul  2 03:05:54 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.35/0.92  ----- Otter 3.2, August 2001 -----
% 0.35/0.92  The process was started by sandbox on n025.cluster.edu,
% 0.35/0.92  Sat Jul  2 03:05:54 2022
% 0.35/0.92  The command was "./sos".  The process ID is 11326.
% 0.35/0.92  
% 0.35/0.92  set(prolog_style_variables).
% 0.35/0.92  set(auto).
% 0.35/0.92     dependent: set(auto1).
% 0.35/0.92     dependent: set(process_input).
% 0.35/0.92     dependent: clear(print_kept).
% 0.35/0.92     dependent: clear(print_new_demod).
% 0.35/0.92     dependent: clear(print_back_demod).
% 0.35/0.92     dependent: clear(print_back_sub).
% 0.35/0.92     dependent: set(control_memory).
% 0.35/0.92     dependent: assign(max_mem, 12000).
% 0.35/0.92     dependent: assign(pick_given_ratio, 4).
% 0.35/0.92     dependent: assign(stats_level, 1).
% 0.35/0.92     dependent: assign(pick_semantic_ratio, 3).
% 0.35/0.92     dependent: assign(sos_limit, 5000).
% 0.35/0.92     dependent: assign(max_weight, 60).
% 0.35/0.92  clear(print_given).
% 0.35/0.92  
% 0.35/0.92  formula_list(usable).
% 0.35/0.92  
% 0.35/0.92  SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=14.
% 0.35/0.92  
% 0.35/0.92  This ia a non-Horn set with equality.  The strategy will be
% 0.35/0.92  Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.35/0.92  unit deletion, with positive clauses in sos and nonpositive
% 0.35/0.92  clauses in usable.
% 0.35/0.92  
% 0.35/0.92     dependent: set(knuth_bendix).
% 0.35/0.92     dependent: set(para_from).
% 0.35/0.92     dependent: set(para_into).
% 0.35/0.92     dependent: clear(para_from_right).
% 0.35/0.92     dependent: clear(para_into_right).
% 0.35/0.92     dependent: set(para_from_vars).
% 0.35/0.92     dependent: set(eq_units_both_ways).
% 0.35/0.92     dependent: set(dynamic_demod_all).
% 0.35/0.92     dependent: set(dynamic_demod).
% 0.35/0.92     dependent: set(order_eq).
% 0.35/0.92     dependent: set(back_demod).
% 0.35/0.92     dependent: set(lrpo).
% 0.35/0.92     dependent: set(hyper_res).
% 0.35/0.92     dependent: set(unit_deletion).
% 0.35/0.92     dependent: set(factor).
% 0.35/0.92  
% 0.35/0.92  ------------> process usable:
% 0.35/0.92    Following clause subsumed by 133 during input processing: 0 [] {-} hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,A),B)!=hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,C),D)|A=C.
% 0.35/0.92    Following clause subsumed by 134 during input processing: 0 [] {-} hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,A),B)!=hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,C),D)|B=D.
% 0.35/0.92    Following clause subsumed by 136 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.35/0.92    Following clause subsumed by 137 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.35/0.92    Following clause subsumed by 156 during input processing: 0 [] {-} -is_Arr1861959080le_alt(A)| -is_Arr1861959080le_alt(B)| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,C),arrow_1681063817le_Lin))|A=B| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,A),B)),C))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),A)),C)).
% 0.35/0.92    Following clause subsumed by 192 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,A),B)!=nil_Ar126264853le_alt.
% 0.35/0.92    Following clause subsumed by 198 during input processing: 0 [flip.1] {-} hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,B),A)!=A.
% 0.35/0.92    Following clause subsumed by 207 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.35/0.92    Following clause subsumed by 227 during input processing: 0 [] {-} -hBOOL(hAPP_f2042909150l_bool(hAPP_f1073701219l_bool(member547554753lt_nat,A),pi_Pro264071722lt_nat(B,C)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_P339823136lt_nat(A,D)),hAPP_P2136891882t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 228 during input processing: 0 [] {-} -hBOOL(hAPP_f2017347493l_bool(hAPP_f137298509l_bool(member1567747746le_alt,A),pi_Pro2035602019le_alt(B,C)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,D),B))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,hAPP_P1095651821le_alt(A,D)),hAPP_P2082381915t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 229 during input processing: 0 [] {-} -hBOOL(hAPP_f969456697l_bool(hAPP_f1857700889l_bool(member1549237916le_alt,A),pi_Pro610394757le_alt(B,C)))| -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,D),B))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,hAPP_P1257947515le_alt(A,D)),hAPP_P1711233733t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 230 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.35/0.92    Following clause subsumed by 231 during input processing: 0 [] {-} -hBOOL(hAPP_f1534526009l_bool(hAPP_f2069145881l_bool(member1258861596ol_nat,A),pi_fun770049925ol_nat(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_f1418366331ol_nat(A,D)),hAPP_f1628730575t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 232 during input processing: 0 [] {-} -hBOOL(hAPP_f1976794890l_bool(hAPP_f1603005581l_bool(member1603119111le_alt,A),pi_fun553016520le_alt(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,hAPP_f40547922le_alt(A,D)),hAPP_f996881846t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 233 during input processing: 0 [] {-} -hBOOL(hAPP_f899439636l_bool(hAPP_f2103233871l_bool(member1620122743le_alt,A),pi_fun462417760le_alt(B,C)))| -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,D),B))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,hAPP_f666924118le_alt(A,D)),hAPP_f228695594t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 234 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.35/0.92    Following clause subsumed by 235 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.35/0.92    Following clause subsumed by 236 during input processing: 0 [] {-} -hBOOL(hAPP_f16559284l_bool(hAPP_f2142494605l_bool(member1846971697ol_nat,A),pi_fun1597968236ol_nat(B,C)))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_f816335862ol_nat(A,D)),hAPP_f856106132t_bool(C,D))).
% 0.35/0.92    Following clause subsumed by 237 during input processing: 0 [] {-} -hBOOL(hAPP_f1732944975l_bool(hAPP_f671616325l_bool(member1636995890le_alt,A),pi_fun380945313le_alt(B,C)))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,D),B))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,hAPP_f1619707799le_alt(A,D)),hAPP_f1865483825t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 238 during input processing: 0 [] {-} -hBOOL(hAPP_f68732431l_bool(hAPP_f1556434125l_bool(member1366121996le_alt,A),pi_fun1792636103le_alt(B,C)))| -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,D),B))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,hAPP_f1054274129le_alt(A,D)),hAPP_f1663053423t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 239 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.35/0.93    Following clause subsumed by 240 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.35/0.93    Following clause subsumed by 241 during input processing: 0 [] {-} -hBOOL(hAPP_f570668343l_bool(hAPP_f2111526677l_bool(member1881985050ol_nat,A),pi_fun2080023171ol_nat(B,C)))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,D),B))|hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,hAPP_f1416261241ol_nat(A,D)),hAPP_f1593910865t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 242 during input processing: 0 [] {-} -hBOOL(hAPP_f236193164l_bool(hAPP_f652666381l_bool(member1535903113le_alt,A),pi_fun90241866le_alt(B,C)))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,D),B))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,hAPP_f53317332le_alt(A,D)),hAPP_f5761716t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 243 during input processing: 0 [] {-} -hBOOL(hAPP_f1424540178l_bool(hAPP_f452990795l_bool(member1870621557le_alt,A),pi_fun684211550le_alt(B,C)))| -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,D),B))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,hAPP_f1800079444le_alt(A,D)),hAPP_f239852716t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 244 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.35/0.93    Following clause subsumed by 245 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.35/0.93    Following clause subsumed by 208 during input processing: 0 [] {-} -hBOOL(hAPP_f2115479956l_bool(hAPP_f975710927l_bool(member24871799le_alt,A),pi_nat249006182le_alt(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_n324757596le_alt(A,D)),hAPP_n588788980t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 209 during input processing: 0 [] {-} -hBOOL(hAPP_f1468796453l_bool(hAPP_f1867424333l_bool(member290075938le_alt,A),pi_Pro492447587le_alt(B,C)))| -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,D),B))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_P1699981037le_alt(A,D)),hAPP_P1861769507t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 210 during input processing: 0 [] {-} -hBOOL(hAPP_f1276380911l_bool(hAPP_f1868812933l_bool(member26406738le_alt,A),pi_Arr55294401le_alt(B,C)))| -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,D),B))|hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(A,D)),hAPP_A568203993t_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 211 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.35/0.93    Following clause subsumed by 212 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.35/0.93    Following clause subsumed by 213 during input processing: 0 [] {-} -hBOOL(hAPP_f903371257l_bool(hAPP_f1546082457l_bool(member1494731740t_bool,A),pi_nat1317494091t_bool(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,hAPP_n1965810497t_bool(A,D)),hAPP_n2095207769l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 214 during input processing: 0 [] {-} -hBOOL(hAPP_f799496074l_bool(hAPP_f105614477l_bool(member2043543687t_bool,A),pi_Pro531915080t_bool(B,C)))| -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,D),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,hAPP_P19446482t_bool(A,D)),hAPP_P139894920l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 215 during input processing: 0 [] {-} -hBOOL(hAPP_f1271753300l_bool(hAPP_f1254328783l_bool(member1986685623t_bool,A),pi_Arr1600668070t_bool(B,C)))| -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,D),B))|hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,hAPP_A1805174428t_bool(A,D)),hAPP_A1928120382l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 216 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.35/0.93    Following clause subsumed by 217 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.35/0.93    Following clause subsumed by 218 during input processing: 0 [] {-} -hBOOL(hAPP_f307807922l_bool(hAPP_f491986957l_bool(member107042095t_bool,A),pi_nat1370421354t_bool(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_n588788980t_bool(A,D)),hAPP_n1674354836l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 219 during input processing: 0 [] {-} -hBOOL(hAPP_f354239713l_bool(hAPP_f720124009l_bool(member1139774916t_bool,A),pi_Pro623007021t_bool(B,C)))| -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_P1861769507t_bool(A,D)),hAPP_P1905961381l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 220 during input processing: 0 [] {-} -hBOOL(hAPP_f1525366679l_bool(hAPP_f586020557l_bool(member1055039380t_bool,A),pi_Arr1306565967t_bool(B,C)))| -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,D),B))|hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A568203993t_bool(A,D)),hAPP_A187815023l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 221 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.35/0.93    Following clause subsumed by 222 during input processing: 0 [] {-} -hBOOL(hAPP_f2835579l_bool(hAPP_f1229756829l_bool(member379339614t_bool,A),pi_nat955432909t_bool(B,C)))| -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,D),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,hAPP_n291670979t_bool(A,D)),hAPP_n295497947l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 223 during input processing: 0 [] {-} -hBOOL(hAPP_f1508559628l_bool(hAPP_f984565261l_bool(member1329875721t_bool,A),pi_Pro1636653258t_bool(B,C)))| -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,D),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,hAPP_P1599728724t_bool(A,D)),hAPP_P1606644490l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 224 during input processing: 0 [] {-} -hBOOL(hAPP_f196630486l_bool(hAPP_f1212866771l_bool(member392258873t_bool,A),pi_Arr44017448t_bool(B,C)))| -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,D),B))|hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,hAPP_A1159885342t_bool(A,D)),hAPP_A366518464l_bool(C,D))).
% 0.35/0.93    Following clause subsumed by 225 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.35/0.93    Following clause subsumed by 226 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.35/0.93    Following clause subsumed by 246 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.35/0.93    Following clause subsumed by 247 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.35/0.93    Following clause subsumed by 485 during input processing: 0 [] {-} -hBOOL(hAPP_P606313927t_bool(A,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C)))|hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(produc212588606t_bool(A),B),C)).
% 0.35/0.93    Following clause subsumed by 484 during input processing: 0 [] {-} -hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(produc212588606t_bool(A),B),C))|hBOOL(hAPP_P606313927t_bool(A,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C))).
% 0.35/0.93    Following clause subsumed by 487 during input processing: 0 [] {-} -hBOOL(hAPP_l1386638586t_bool(hAPP_l1747810175t_bool(produc231070560t_bool(A),B),C))|hBOOL(hAPP_P1327827171t_bool(A,hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,B),C))).
% 0.35/0.93    Following clause subsumed by 484 during input processing: 0 [] {-} -hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(produc212588606t_bool(A),B),C))|hBOOL(hAPP_P606313927t_bool(A,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C))).
% 0.35/0.94    Following clause subsumed by 484 during input processing: 0 [] {-} -hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(produc212588606t_bool(A),B),C))|hBOOL(hAPP_P606313927t_bool(A,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C))).
% 0.35/0.94    Following clause subsumed by 485 during input processing: 0 [] {-} hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(produc212588606t_bool(A),B),C))| -hBOOL(hAPP_P606313927t_bool(A,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C))).
% 0.35/0.94    Following clause subsumed by 490 during input processing: 0 [] {-} A!=nil_Ar126264853le_alt|hBOOL(hAPP_l1386638586t_bool(null_A361035805le_alt,A)).
% 0.35/0.94    Following clause subsumed by 489 during input processing: 0 [] {-} A=nil_Ar126264853le_alt| -hBOOL(hAPP_l1386638586t_bool(null_A361035805le_alt,A)).
% 0.35/0.94    Following clause subsumed by 501 during input processing: 0 [] {-} -is_Arr1861959080le_alt(A)|B!=nil_Ar126264853le_alt|last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,A),B))=A.
% 0.35/0.94    Following clause subsumed by 533 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)=hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,C),D)|hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),E)!=C|B!=hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,E),D).
% 0.35/0.94    Following clause subsumed by 550 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)!=nil_Ar126264853le_alt|A=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 552 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)!=nil_Ar126264853le_alt|B=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 554 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)=nil_Ar126264853le_alt|A!=nil_Ar126264853le_alt|B!=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 556 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)!=A|B=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 558 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)=A|B!=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 560 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)!=B|A=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 562 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B)=B|A!=nil_Ar126264853le_alt.
% 0.35/0.94    Following clause subsumed by 548 during input processing: 0 [] {-} hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,A),B)=hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,C),D)|hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,A),E)!=C|B!=hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,E),D).
% 0.35/0.94    Following clause subsumed by 584 during input processing: 0 [] {-} A!=nil_Ar126264853le_alt|last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,B),A))=last_A57386030le_alt(B).
% 0.35/0.94    Following clause subsumed by 710 during input processing: 0 [] {-} -hBOOL(hAPP_P606313927t_bool(hAPP_f791205069t_bool(produc2022255647t_bool,A),hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C)))|hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(A,B),C)).
% 0.35/0.94    Following clause subsumed by 711 during input processing: 0 [] {-} hBOOL(hAPP_P606313927t_bool(hAPP_f791205069t_bool(produc2022255647t_bool,A),hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C)))| -hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(A,B),C)).
% 0.35/0.94    Following clause subsumed by 711 during input processing: 0 [] {-} -hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(A,B),C))|hBOOL(hAPP_P606313927t_bool(hAPP_f791205069t_bool(produc2022255647t_bool,A),hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C))).
% 0.35/0.98    Following clause subsumed by 756 during input processing: 0 [] {-} -hBOOL(hAPP_l1386638586t_bool(hAPP_l1747810175t_bool(A,B),C))|hBOOL(hAPP_P1327827171t_bool(hAPP_f1331183759t_bool(produc1102988737t_bool,A),hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,B),C))).
% 0.35/0.98    Following clause subsumed by 711 during input processing: 0 [] {-} -hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(A,B),C))|hBOOL(hAPP_P606313927t_bool(hAPP_f791205069t_bool(produc2022255647t_bool,A),hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C))).
% 0.35/0.98    Following clause subsumed by 710 during input processing: 0 [] {-} -hBOOL(hAPP_P606313927t_bool(hAPP_f791205069t_bool(produc2022255647t_bool,A),hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,B),C)))|hBOOL(hAPP_A862370221t_bool(hAPP_A1664620203t_bool(A,B),C)).
% 0.35/0.98    Following clause subsumed by 546 during input processing: 0 [] {-} -hBOOL(hAPP_l1386638586t_bool(hAPP_l1747810175t_bool(equal_499625528le_alt,A),B))|A=B.
% 0.35/0.98    Following clause subsumed by 547 during input processing: 0 [] {-} hBOOL(hAPP_l1386638586t_bool(hAPP_l1747810175t_bool(equal_499625528le_alt,A),B))|A!=B.
% 0.35/0.98    Following clause subsumed by 948 during input processing: 0 [] {-} hAPP_l726444215le_alt(rev_Ar2093961333le_alt,A)!=nil_Ar126264853le_alt|A=nil_Ar126264853le_alt.
% 0.35/0.98    Following clause subsumed by 950 during input processing: 0 [] {-} hAPP_l726444215le_alt(rev_Ar2093961333le_alt,A)=nil_Ar126264853le_alt|A!=nil_Ar126264853le_alt.
% 0.35/0.98    Following clause subsumed by 1051 during input processing: 0 [] {-} -hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A),set_nat(B)))|hAPP_l248265089st_nat(hAPP_n280362926st_nat(insert_nat,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1052 during input processing: 0 [] {-} -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,A),set_Ar1565008694le_alt(B)))|hAPP_l726444215le_alt(hAPP_A408086601le_alt(insert960637483le_alt,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1053 during input processing: 0 [] {-} -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,A),set_Pr1404309362le_alt(B)))|hAPP_l1493873365le_alt(hAPP_P734992695le_alt(insert178756925le_alt,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1054 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),set_Ar219761597e_indi(B)))|hAPP_l54953109e_indi(hAPP_A974963564e_indi(insert915800584e_indi,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1055 during input processing: 0 [] {-} -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,A),set_bool(B)))|hAPP_l1189022293t_bool(hAPP_b994696797t_bool(insert_bool,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1056 during input processing: 0 [] {-} -hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),set_fu335223357t_bool(B)))|hAPP_l210315413t_bool(hAPP_f1812326636t_bool(insert1946138248t_bool,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1057 during input processing: 0 [] {-} -hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),set_fu1384968698t_bool(B)))|hAPP_l1075146559t_bool(hAPP_f613335309t_bool(insert202184175t_bool,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1058 during input processing: 0 [] {-} -hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),set_fu1865467835t_bool(B)))|hAPP_l1660244757t_bool(hAPP_f726713198t_bool(insert1665396998t_bool,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1059 during input processing: 0 [] {-} -hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,A),set_Pr604701398le_alt(B)))|hAPP_l1766111573le_alt(hAPP_P1057207891le_alt(insert256706849le_alt,A),B)=B.
% 0.35/0.98    Following clause subsumed by 1655 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.35/0.98    Following clause subsumed by 1656 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.35/0.98    Following clause subsumed by 1623 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.35/0.98    Following clause subsumed by 1624 during input processing: 0 [] {-} -hBOOL(hAPP_f2013399995l_bool(hAPP_f1721660479l_bool(ord_le893483153t_bool,A),B))| -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,C),A))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,C),B)).
% 0.35/0.98    Following clause subsumed by 1625 during input processing: 0 [] {-} -hBOOL(hAPP_f1634113933l_bool(hAPP_f310455147l_bool(ord_le340789135t_bool,A),B))| -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,C),A))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,C),B)).
% 0.35/0.98    Following clause subsumed by 1626 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,C),A))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,C),B)).
% 0.35/0.98    Following clause subsumed by 1627 during input processing: 0 [] {-} -hBOOL(hAPP_f387058535l_bool(hAPP_f612708895l_bool(ord_le742797417l_bool,A),B))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,C),A))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,C),B)).
% 0.35/0.98    Following clause subsumed by 1628 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.35/0.98    Following clause subsumed by 1629 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.35/0.98    Following clause subsumed by 1630 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.35/0.98    Following clause subsumed by 1631 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.35/0.98    Following clause subsumed by 1623 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.35/0.98    Following clause subsumed by 1624 during input processing: 0 [] {-} -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,A),B))| -hBOOL(hAPP_f2013399995l_bool(hAPP_f1721660479l_bool(ord_le893483153t_bool,B),C))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,A),C)).
% 0.35/0.98    Following clause subsumed by 1625 during input processing: 0 [] {-} -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,A),B))| -hBOOL(hAPP_f1634113933l_bool(hAPP_f310455147l_bool(ord_le340789135t_bool,B),C))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,A),C)).
% 0.35/0.98    Following clause subsumed by 1626 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,B),C))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),C)).
% 0.35/0.98    Following clause subsumed by 1627 during input processing: 0 [] {-} -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,A),B))| -hBOOL(hAPP_f387058535l_bool(hAPP_f612708895l_bool(ord_le742797417l_bool,B),C))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,A),C)).
% 0.35/0.98    Following clause subsumed by 1628 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.35/0.98    Following clause subsumed by 1629 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.35/0.98    Following clause subsumed by 1630 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.35/0.98    Following clause subsumed by 1631 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.35/0.98    Following clause subsumed by 1656 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.35/0.98    Following clause subsumed by 1623 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.35/0.98    Following clause subsumed by 1624 during input processing: 0 [] {-} -hBOOL(hAPP_f2013399995l_bool(hAPP_f1721660479l_bool(ord_le893483153t_bool,A),B))| -hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,C),A))|hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,C),B)).
% 0.35/0.98    Following clause subsumed by 1625 during input processing: 0 [] {-} -hBOOL(hAPP_f1634113933l_bool(hAPP_f310455147l_bool(ord_le340789135t_bool,A),B))| -hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,C),A))|hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,C),B)).
% 0.35/0.98    Following clause subsumed by 1626 during input processing: 0 [] {-} -hBOOL(hAPP_f1599966040l_bool(hAPP_f384959233l_bool(ord_le249613274i_bool,A),B))| -hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,C),A))|hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,C),B)).
% 0.35/0.98    Following clause subsumed by 1627 during input processing: 0 [] {-} -hBOOL(hAPP_f387058535l_bool(hAPP_f612708895l_bool(ord_le742797417l_bool,A),B))| -hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,C),A))|hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,C),B)).
% 0.35/0.98    Following clause subsumed by 1628 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.35/0.98    Following clause subsumed by 1629 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.35/0.98    Following clause subsumed by 1630 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.35/0.98    Following clause subsumed by 1631 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.35/0.98    Following clause subsumed by 1662 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.35/0.98    Following clause subsumed by 1656 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.35/0.98    Following clause subsumed by 1677 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.35/0.98    Following clause subsumed by 1679 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.35/0.98    Following clause subsumed by 1681 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.35/0.98    Following clause subsumed by 1683 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.35/0.98    Following clause subsumed by 1685 during input processing: 0 [] {-} -is_fun1393352280t_bool(A)| -hBOOL(hAPP_f2013399995l_bool(hAPP_f1721660479l_bool(ord_le893483153t_bool,top_to2076077793t_bool),A))|A=top_to2076077793t_bool.
% 0.35/0.98    Following clause subsumed by 1687 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.35/0.98    Following clause subsumed by 1692 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=A.
% 0.35/0.98    Following clause subsumed by 1693 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=hAPP_nat_nat(suc,B)|A=B.
% 0.35/0.98    Following clause subsumed by 1695 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),A)).
% 0.35/0.98    Following clause subsumed by 1697 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|B!=A.
% 0.35/0.98    Following clause subsumed by 1696 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.35/0.98    Following clause subsumed by 1662 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.35/0.98    Following clause subsumed by 1655 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.35/0.98    Following clause subsumed by 1656 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.35/0.98    Following clause subsumed by 1700 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.35/0.98    Following clause subsumed by 1698 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.35/0.98    Following clause subsumed by 1690 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.35/0.98    Following clause subsumed by 1700 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.35/0.98    Following clause subsumed by 1703 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.35/0.98    Following clause subsumed by 1662 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.35/0.98    Following clause subsumed by 1711 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(suc,B))).
% 0.35/0.98    Following clause subsumed by 1710 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.35/0.98    Following clause subsumed by 1689 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.35/0.98    Following clause subsumed by 1662 during input processing: 0 [] {-} A!=B|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B)).
% 0.35/0.98    Following clause subsumed by 1689 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.35/0.98    Following clause subsumed by 1715 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.35/0.98    Following clause subsumed by 1689 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.35/0.98    Following clause subsumed by 1662 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|A!=B.
% 0.35/0.98    Following clause subsumed by 1689 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.35/0.98    Following clause subsumed by 1696 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),B))|A!=B.
% 0.35/0.98    Following clause subsumed by 1715 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.35/0.98    Following clause subsumed by 1717 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.35/0.98    Following clause subsumed by 1716 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.35/0.98    Following clause subsumed by 1719 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.35/0.98    Following clause subsumed by 1716 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.35/0.98    Following clause subsumed by 1706 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.35/0.98    Following clause subsumed by 1717 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.35/0.99    Following clause subsumed by 1737 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(plus_plus_nat(C),B))).
% 0.35/0.99    Following clause subsumed by 1736 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(plus_plus_nat(B),C))).
% 0.35/0.99    Following clause subsumed by 1746 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(plus_plus_nat(B),C))).
% 0.35/0.99    Following clause subsumed by 1747 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(plus_plus_nat(C),B))).
% 0.35/0.99    Following clause subsumed by 1756 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C)).
% 0.35/0.99    Following clause subsumed by 1755 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(plus_plus_nat(A),B)),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.35/0.99    Following clause subsumed by 1769 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(A,hAPP_nat_nat(minus_minus_nat(B),C)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C))|hBOOL(hAPP_nat_bool(A,zero_zero_nat)).
% 0.35/0.99    Following clause subsumed by 1770 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(A,hAPP_nat_nat(minus_minus_nat(B),C)))|B!=hAPP_nat_nat(plus_plus_nat(C),D)|hBOOL(hAPP_nat_bool(A,D)).
% 0.35/0.99    Following clause subsumed by 1768 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.35/0.99    Following clause subsumed by 1697 during input processing: 0 [] {-} A!=zero_zero_nat| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 0.35/0.99    Following clause subsumed by 1768 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,A),zero_zero_nat)).
% 0.35/0.99    Following clause subsumed by 1662 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),zero_zero_nat))|A!=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1793 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|hAPP_nat_nat(minus_minus_nat(A),B)=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1795 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(minus_minus_nat(B),A)),hAPP_nat_nat(minus_minus_nat(C),A)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,B),C)).
% 0.35/0.99    Following clause subsumed by 1802 during input processing: 0 [flip.1] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1802 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1802 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1802 during input processing: 0 [flip.1] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1802 during input processing: 0 [] {-} hAPP_nat_nat(suc,A)!=zero_zero_nat.
% 0.35/0.99    Following clause subsumed by 1806 during input processing: 0 [flip.2] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))|hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(plus_plus_nat(C),B)),A)=hAPP_nat_nat(plus_plus_nat(C),hAPP_nat_nat(minus_minus_nat(B),A)).
% 0.35/0.99    Following clause subsumed by 1817 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),B))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),C))|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(minus_minus_nat(B),A)),hAPP_nat_nat(minus_minus_nat(C),A)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,B),C)).
% 1.50/1.72    Following clause subsumed by 1825 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.
% 1.50/1.72    Following clause subsumed by 1832 during input processing: 0 [] {-} hAPP_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.
% 1.50/1.72    Following clause subsumed by 1834 during input processing: 0 [] {-} hAPP_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).
% 1.50/1.72    Following clause subsumed by 1836 during input processing: 0 [] {-} hAPP_nat_nat(plus_plus_nat(A),B)!=hAPP_nat_nat(suc,zero_zero_nat)|B=zero_zero_nat|A=zero_zero_nat.
% 1.50/1.72    Following clause subsumed by 1838 during input processing: 0 [] {-} hAPP_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).
% 1.50/1.72    Following clause subsumed by 1840 during input processing: 0 [] {-} hAPP_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.
% 1.50/1.72    Following clause subsumed by 1842 during input processing: 0 [] {-} hAPP_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).
% 1.50/1.72    Following clause subsumed by 1736 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 1.50/1.72    Following clause subsumed by 1737 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),hAPP_nat_nat(plus_plus_nat(A),B)))| -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),B)).
% 1.50/1.72    Following clause subsumed by 1860 during input processing: 0 [] {-} -hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A))|hAPP_nat_nat(suc,hAPP_nat_nat(minus_minus_nat(A),one_one_nat))=A.
% 1.50/1.72    Following clause subsumed by 1863 during input processing: 0 [] {-} -is_bool(A)|A=fTrue|A=fFalse.
% 1.50/1.72    Following clause subsumed by 1863 during input processing: 0 [] {-} -is_bool(A)|A=fTrue|A=fFalse.
% 1.50/1.72  1293 back subsumes 1258.
% 1.50/1.72  1293 back subsumes 1222.
% 1.50/1.72  1296 back subsumes 1262.
% 1.50/1.72  1296 back subsumes 1226.
% 1.50/1.72  1299 back subsumes 1266.
% 1.50/1.72  1299 back subsumes 1230.
% 1.50/1.72  1302 back subsumes 1270.
% 1.50/1.72  1302 back subsumes 1234.
% 1.50/1.72  1305 back subsumes 1274.
% 1.50/1.72  1305 back subsumes 1238.
% 1.50/1.72  1308 back subsumes 1278.
% 1.50/1.72  1308 back subsumes 1242.
% 1.50/1.72  1311 back subsumes 1282.
% 1.50/1.72  1311 back subsumes 1246.
% 1.50/1.72  1314 back subsumes 1286.
% 1.50/1.72  1314 back subsumes 1250.
% 1.50/1.72  1317 back subsumes 1290.
% 1.50/1.72  1317 back subsumes 1254.
% 1.50/1.72  1662 back subsumes 1661.
% 1.50/1.72  1706 back subsumes 1705.
% 1.50/1.72  1957 back subsumes 1953.
% 1.50/1.72  2001 back subsumes 1998.
% 1.50/1.72  2001 back subsumes 1994.
% 1.50/1.72  2001 back subsumes 1982.
% 1.50/1.72  2011 back subsumes 1984.
% 1.50/1.72  2013 back subsumes 1986.
% 1.50/1.72  2019 back subsumes 2015.
% 1.50/1.72  2019 back subsumes 1995.
% 1.50/1.72  2020 back subsumes 2016.
% 1.50/1.72  2020 back subsumes 1996.
% 1.50/1.72  
% 1.50/1.72  ------------> process sos:
% 1.50/1.72    Following clause subsumed by 2885 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A),top_top_fun_nat_bool)).
% 1.50/1.72    Following clause subsumed by 2886 during input processing: 0 [] {-} hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,A),top_to772840767t_bool)).
% 1.50/1.72    Following clause subsumed by 2887 during input processing: 0 [] {-} hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,A),top_to1647826457l_bool)).
% 1.50/1.72    Following clause subsumed by 2888 during input processing: 0 [] {-} hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),top_to1576102282i_bool)).
% 1.50/1.72    Following clause subsumed by 2889 during input processing: 0 [] {-} hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,A),top_to2076077793t_bool)).
% 1.50/1.72    Following clause subsumed by 2890 during input processing: 0 [] {-} hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,A),top_to565915683t_bool)).
% 1.50/1.73    Following clause subsumed by 2891 during input processing: 0 [] {-} hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),top_to522745736l_bool)).
% 1.50/1.73    Following clause subsumed by 2892 during input processing: 0 [] {-} hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),top_to1853035173l_bool)).
% 1.50/1.73    Following clause subsumed by 2893 during input processing: 0 [] {-} hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),top_to1714702858l_bool)).
% 1.50/1.73    Following clause subsumed by 2910 during input processing: 0 [] {-} A=nil_Ar126264853le_alt|last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,B),A))=last_A57386030le_alt(A).
% 1.50/1.73    Following clause subsumed by 2885 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,$c6),top_top_fun_nat_bool)).
% 1.50/1.73    Following clause subsumed by 2886 during input processing: 0 [] {-} hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,$c7),top_to772840767t_bool)).
% 1.50/1.73    Following clause subsumed by 2887 during input processing: 0 [] {-} hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,$c8),top_to1647826457l_bool)).
% 1.50/1.73    Following clause subsumed by 2888 during input processing: 0 [] {-} hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,$c9),top_to1576102282i_bool)).
% 1.50/1.73    Following clause subsumed by 2889 during input processing: 0 [] {-} hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,$c10),top_to2076077793t_bool)).
% 1.50/1.73    Following clause subsumed by 2890 during input processing: 0 [] {-} hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,$c11),top_to565915683t_bool)).
% 1.50/1.73    Following clause subsumed by 2891 during input processing: 0 [] {-} hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,$c12),top_to522745736l_bool)).
% 1.50/1.73    Following clause subsumed by 2892 during input processing: 0 [] {-} hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,$c13),top_to1853035173l_bool)).
% 1.50/1.73    Following clause subsumed by 2893 during input processing: 0 [] {-} hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,$c14),top_to1714702858l_bool)).
% 1.50/1.73    Following clause subsumed by 2956 during input processing: 0 [] {-} hAPP_P1056860425le_alt(hAPP_f1078809103le_alt(produc748227559le_alt,A),hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,B),C))=hAPP_l391088160le_alt(hAPP_l1869074853le_alt(A,B),C).
% 1.50/1.73    Following clause subsumed by 3015 during input processing: 0 [] {-} A=nil_Ar126264853le_alt|hd_Arr805754088le_alt(hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B))=hd_Arr805754088le_alt(A).
% 1.50/1.73    Following clause subsumed by 3087 during input processing: 0 [] {-} hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A),set_nat(B)))|hAPP_l248265089st_nat(hAPP_n280362926st_nat(insert_nat,A),B)=hAPP_l248265089st_nat(hAPP_n280362926st_nat(cons_nat,A),B).
% 1.50/1.73    Following clause subsumed by 3088 during input processing: 0 [] {-} hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,A),set_Ar1565008694le_alt(B)))|hAPP_l726444215le_alt(hAPP_A408086601le_alt(insert960637483le_alt,A),B)=hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,A),B).
% 1.50/1.73    Following clause subsumed by 3089 during input processing: 0 [] {-} hBOOL(hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(member1020705648le_alt,A),set_Pr1404309362le_alt(B)))|hAPP_l1493873365le_alt(hAPP_P734992695le_alt(insert178756925le_alt,A),B)=hAPP_l1493873365le_alt(hAPP_P734992695le_alt(cons_P893004579le_alt,A),B).
% 1.50/1.73    Following clause subsumed by 3090 during input processing: 0 [] {-} hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,A),set_Ar219761597e_indi(B)))|hAPP_l54953109e_indi(hAPP_A974963564e_indi(insert915800584e_indi,A),B)=hAPP_l54953109e_indi(hAPP_A974963564e_indi(cons_A104257774e_indi,A),B).
% 1.57/1.77    Following clause subsumed by 3091 during input processing: 0 [] {-} hBOOL(hAPP_f387058535l_bool(hAPP_b1787118453l_bool(member_bool,A),set_bool(B)))|hAPP_l1189022293t_bool(hAPP_b994696797t_bool(insert_bool,A),B)=hAPP_l1189022293t_bool(hAPP_b994696797t_bool(cons_bool,A),B).
% 1.57/1.77    Following clause subsumed by 3092 during input processing: 0 [] {-} hBOOL(hAPP_f250445784l_bool(hAPP_f1253375959l_bool(member520425275t_bool,A),set_fu335223357t_bool(B)))|hAPP_l210315413t_bool(hAPP_f1812326636t_bool(insert1946138248t_bool,A),B)=hAPP_l210315413t_bool(hAPP_f1812326636t_bool(cons_f14678382t_bool,A),B).
% 1.57/1.77    Following clause subsumed by 3093 during input processing: 0 [] {-} hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,A),set_fu1384968698t_bool(B)))|hAPP_l1075146559t_bool(hAPP_f613335309t_bool(insert202184175t_bool,A),B)=hAPP_l1075146559t_bool(hAPP_f613335309t_bool(cons_f1416466313t_bool,A),B).
% 1.57/1.77    Following clause subsumed by 3094 during input processing: 0 [] {-} hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,A),set_fu1865467835t_bool(B)))|hAPP_l1660244757t_bool(hAPP_f726713198t_bool(insert1665396998t_bool,A),B)=hAPP_l1660244757t_bool(hAPP_f726713198t_bool(cons_f1803648492t_bool,A),B).
% 1.57/1.77    Following clause subsumed by 3095 during input processing: 0 [] {-} hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,A),set_Pr604701398le_alt(B)))|hAPP_l1766111573le_alt(hAPP_P1057207891le_alt(insert256706849le_alt,A),B)=hAPP_l1766111573le_alt(hAPP_P1057207891le_alt(cons_P993230855le_alt,A),B).
% 1.57/1.77    Following clause subsumed by 3134 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.57/1.77    Following clause subsumed by 3149 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.57/1.77    Following clause subsumed by 3149 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.57/1.77    Following clause subsumed by 3133 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,A),A)).
% 1.57/1.77    Following clause subsumed by 3134 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.57/1.77    Following clause subsumed by 3196 during input processing: 0 [] {-} A=zero_zero_nat|hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),A)).
% 1.57/1.77    Following clause subsumed by 3170 during input processing: 0 [] {-} hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,zero_zero_nat),A)).
% 1.57/1.77  2866 back subsumes 519.
% 1.57/1.77  2867 back subsumes 521.
% 1.57/1.77  2868 back subsumes 523.
% 1.57/1.77  2869 back subsumes 525.
% 1.57/1.77  2870 back subsumes 527.
% 1.57/1.77  2871 back subsumes 529.
% 1.57/1.77  2882 back subsumes 502.
% 1.57/1.77    Following clause subsumed by 3367 during input processing: 0 [copy,2991,flip.1] {-} equal_499625528le_alt=equal_499625528le_alt.
% 1.57/1.77    Following clause subsumed by 3367 during input processing: 0 [copy,3045,flip.1] {-} nil_Ar126264853le_alt=nil_Ar126264853le_alt.
% 1.57/1.77    Following clause subsumed by 3367 during input processing: 0 [copy,3053,flip.1] {-} hAPP_l726444215le_alt(butlas1262502241le_alt,hAPP_l726444215le_alt(hAPP_n2139729636le_alt(drop_A186780501le_alt,A),B))=hAPP_l726444215le_alt(butlas1262502241le_alt,hAPP_l726444215le_alt(hAPP_n2139729636le_alt(drop_A186780501le_alt,A),B)).
% 1.57/1.77    Following clause subsumed by 3367 during input processing: 0 [copy,3057,flip.1] {-} hAPP_l726444215le_alt(tl_Arr1453005548le_alt,hAPP_l726444215le_alt(hAPP_n2139729636le_alt(drop_A186780501le_alt,A),B))=hAPP_l726444215le_alt(tl_Arr1453005548le_alt,hAPP_l726444215le_alt(hAPP_n2139729636le_alt(drop_A186780501le_alt,A),B)).
% 1.57/1.77  3059 back subsumes 2265.
% 1.57/1.77  3060 back subsumes 2416.
% 1.57/1.77  3060 back subsumes 2280.
% 1.57/1.77  3133 back subsumes 2306.
% 1.57/1.77  3133 back subsumes 2297.
% 1.57/1.77  3133 back subsumes 2296.
% 1.57/1.77  3133 back subsumes 2295.
% 1.57/1.77  3137 back subsumes 2294.
% 1.57/1.77    Following clause subsumed by 3367 during input processing: 0 [copy,3160,flip.1] {-} hAPP_nat_nat(suc,hAPP_nat_nat(plus_plus_nat(A),B))=hAPP_nat_nat(suc,hAPP_nat_nat(plus_plus_nat(A),B)).
% 1.93/2.15    Following clause subsumed by 3165 during input processing: 0 [copy,3165,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C))=hAPP_nat_nat(plus_plus_nat(B),hAPP_nat_nat(plus_plus_nat(A),C)).
% 1.93/2.15    Following clause subsumed by 3166 during input processing: 0 [copy,3166,flip.1] {-} hAPP_nat_nat(plus_plus_nat(A),B)=hAPP_nat_nat(plus_plus_nat(B),A).
% 1.93/2.15    Following clause subsumed by 3202 during input processing: 0 [copy,3202,flip.1] {-} hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(minus_minus_nat(A),B)),C)=hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(minus_minus_nat(A),C)),B).
% 1.93/2.15    Following clause subsumed by 3367 during input processing: 0 [copy,3367,flip.1] {-} A=A.
% 1.93/2.15  3367 back subsumes 3160.
% 1.93/2.15  3367 back subsumes 3057.
% 1.93/2.15  3367 back subsumes 3053.
% 1.93/2.15  3367 back subsumes 3045.
% 1.93/2.15  3367 back subsumes 2991.
% 1.93/2.15  3367 back subsumes 2428.
% 1.93/2.15  3367 back subsumes 2356.
% 1.93/2.15  3367 back subsumes 2355.
% 1.93/2.15  3367 back subsumes 2351.
% 1.93/2.15  3367 back subsumes 2349.
% 1.93/2.15  3367 back subsumes 2347.
% 1.93/2.15  3367 back subsumes 2343.
% 1.93/2.15  3367 back subsumes 2342.
% 1.93/2.15  3367 back subsumes 2339.
% 1.93/2.15  3367 back subsumes 2319.
% 1.93/2.15  3367 back subsumes 2318.
% 1.93/2.15  3367 back subsumes 2317.
% 1.93/2.15  3367 back subsumes 2316.
% 1.93/2.15  3367 back subsumes 2315.
% 1.93/2.15  3367 back subsumes 2314.
% 1.93/2.15  3367 back subsumes 2313.
% 1.93/2.15  3367 back subsumes 2304.
% 1.93/2.15  3367 back subsumes 2303.
% 1.93/2.15  3367 back subsumes 2293.
% 1.93/2.15  3367 back subsumes 2199.
% 1.93/2.15  3367 back subsumes 2198.
% 1.93/2.15  3367 back subsumes 2197.
% 1.93/2.15  3367 back subsumes 2195.
% 1.93/2.15  3367 back subsumes 2149.
% 1.93/2.15  3367 back subsumes 2147.
% 1.93/2.15  3367 back subsumes 2146.
% 1.93/2.15  3367 back subsumes 2145.
% 1.93/2.15  3367 back subsumes 2136.
% 1.93/2.15  3367 back subsumes 2135.
% 1.93/2.15  3367 back subsumes 2134.
% 1.93/2.15  3367 back subsumes 2131.
% 1.93/2.15  3367 back subsumes 2076.
% 1.93/2.15  3367 back subsumes 2075.
% 1.93/2.15  3367 back subsumes 2069.
% 1.93/2.15  3367 back subsumes 2045.
% 1.93/2.15  3367 back subsumes 2036.
% 1.93/2.15  3367 back subsumes 2027.
% 1.93/2.15    Following clause subsumed by 3426 during input processing: 0 [copy,3380,flip.1] {-} partit327648526le_alt(A,hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),C))=hAPP_P1056860425le_alt(hAPP_f1078809103le_alt(produc49943708le_alt,hAPP_f746471349le_alt(hAPP_f628327744le_alt(cOMBS_1294827559le_alt,hAPP_f1291559232le_alt(hAPP_f749699165le_alt(cOMBB_1450165017le_alt,cOMBS_1399042523le_alt),hAPP_f469186021le_alt(hAPP_f1933751673le_alt(cOMBB_1193902096le_alt,hAPP_f1939049849le_alt(cOMBB_723746886le_alt,if_Pro1306781203le_alt(hAPP_A862370221t_bool(A,C)))),hAPP_f1790240989le_alt(hAPP_f1013417831le_alt(cOMBB_2052911494le_alt,produc237774329le_alt),hAPP_A408086601le_alt(cons_A1216297413le_alt,C))))),hAPP_f1790240989le_alt(hAPP_f1792349771le_alt(cOMBC_1330649024le_alt,hAPP_f1318121625le_alt(hAPP_f634775919le_alt(cOMBB_576205818le_alt,cOMBB_1818168801le_alt),produc237774329le_alt)),hAPP_A408086601le_alt(cons_A1216297413le_alt,C)))),partit327648526le_alt(A,B)).
% 1.93/2.15    Following clause subsumed by 3425 during input processing: 0 [copy,3381,flip.1] {-} hAPP_P1056860425le_alt(hAPP_f1078809103le_alt(produc49943708le_alt,A),hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,B),C))=hAPP_l391088160le_alt(hAPP_l1869074853le_alt(A,B),C).
% 1.93/2.15    Following clause subsumed by 3381 during input processing: 0 [copy,3425,flip.1] {-} hAPP_l391088160le_alt(hAPP_l1869074853le_alt(A,B),C)=hAPP_P1056860425le_alt(hAPP_f1078809103le_alt(produc49943708le_alt,A),hAPP_l391088160le_alt(hAPP_l1869074853le_alt(produc237774329le_alt,B),C)).
% 1.93/2.15    Following clause subsumed by 3380 during input processing: 0 [copy,3426,flip.1] {-} hAPP_P1056860425le_alt(hAPP_f1078809103le_alt(produc49943708le_alt,hAPP_f746471349le_alt(hAPP_f628327744le_alt(cOMBS_1294827559le_alt,hAPP_f1291559232le_alt(hAPP_f749699165le_alt(cOMBB_1450165017le_alt,cOMBS_1399042523le_alt),hAPP_f469186021le_alt(hAPP_f1933751673le_alt(cOMBB_1193902096le_alt,hAPP_f1939049849le_alt(cOMBB_723746886le_alt,if_Pro1306781203le_alt(hAPP_A862370221t_bool(A,B)))),hAPP_f1790240989le_alt(hAPP_f1013417831le_alt(cOMBB_2052911494le_alt,produc237774329le_alt),hAPP_A408086601le_alt(cons_A1216297413le_alt,B))))),hAPP_f1790240989le_alt(hAPP_f1792349771le_alt(cOMBC_1330649024le_alt,hAPP_f1318121625le_alt(hAPP_f634775919le_alt(cOMBB_576205818le_alt,cOMBB_1818168801le_alt),produc237774329le_alt)),hAPP_A408086601le_alt(cons_A1216297413le_alt,B)))),partit327648526le_alt(A,C))=partit327648526le_alt(A,hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),C),B)).
% 1.93/2.15    Following clause subsumed by 2977 during input processing: 0 [copy,3433,flip.1] {-} hAPP_l726444215le_alt(tl_Arr1453005548le_alt,hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B))=hAPP_l726444215le_alt(list_c380068407le_alt(hAPP_l726444215le_alt(tl_Arr1453005548le_alt,B),hAPP_f1608056749le_alt(cOMBK_1696648346le_alt,hAPP_l568342716le_alt(hAPP_f1294513379le_alt(cOMBC_1058495865le_alt,append1166636842le_alt),B))),A).
% 1.93/2.15    Following clause subsumed by 3434 during input processing: 0 [copy,3434,flip.1] {-} hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,hAPP_f1777336662le_alt(hAPP_f939319677le_alt(cOMBB_881934114le_alt,append1166636842le_alt),replic351609551le_alt(A))),hAPP_A832564074le_alt(replic351609551le_alt(B),C)),C)=hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,hAPP_f1777336662le_alt(hAPP_f939319677le_alt(cOMBB_881934114le_alt,append1166636842le_alt),replic351609551le_alt(B))),hAPP_A832564074le_alt(replic351609551le_alt(A),C)),C).
% 1.93/2.15    Following clause subsumed by 3488 during input processing: 0 [copy,3437,flip.1] {-} hAPP_A832564074le_alt(hAPP_n49391885le_alt(list_u1050032253le_alt(hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),C))),hAPP_l1872264749lt_nat(size_s1873794948le_alt,A)),D)=hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),D)).
% 1.93/2.15    Following clause subsumed by 3041 during input processing: 0 [copy,3441,flip.1] {-} hAPP_l726444215le_alt(rev_Ar2093961333le_alt,hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),B))=hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,hAPP_l726444215le_alt(rev_Ar2093961333le_alt,B)),hAPP_l726444215le_alt(rev_Ar2093961333le_alt,A)).
% 1.93/2.15    Following clause subsumed by 3486 during input processing: 0 [copy,3444,flip.1] {-} hAPP_A832564074le_alt(hAPP_n49391885le_alt(list_u1050032253le_alt(hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),A),B)),C),D)=hAPP_n1875670159le_alt(nat_ca14895078le_alt(hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),A),D),hAPP_f402821245le_alt(hAPP_f548810715le_alt(cOMBB_903467948lt_nat,hAPP_A408086601le_alt(cons_A1216297413le_alt,B)),hAPP_A1043896845le_alt(hAPP_f1956511609le_alt(cOMBC_1697899890le_alt,list_u1050032253le_alt(A)),D))),C).
% 1.93/2.15    Following clause subsumed by 3485 during input processing: 0 [copy,3445,flip.1] {-} hAPP_l726444215le_alt(hAPP_n2139729636le_alt(drop_A186780501le_alt,A),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),C))=hAPP_n1875670159le_alt(nat_ca14895078le_alt(hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),C),hAPP_l382792410le_alt(hAPP_f2068969285le_alt(cOMBC_1511969967le_alt,drop_A186780501le_alt),B)),A).
% 1.93/2.15    Following clause subsumed by 3484 during input processing: 0 [copy,3446,flip.1] {-} hAPP_l726444215le_alt(hAPP_n2139729636le_alt(take_A1601602045le_alt,A),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),C))=hAPP_n1875670159le_alt(nat_ca14895078le_alt(nil_Ar126264853le_alt,hAPP_f402821245le_alt(hAPP_f548810715le_alt(cOMBB_903467948lt_nat,hAPP_A408086601le_alt(cons_A1216297413le_alt,C)),hAPP_l382792410le_alt(hAPP_f2068969285le_alt(cOMBC_1511969967le_alt,take_A1601602045le_alt),B))),A).
% 1.93/2.15    Following clause subsumed by 3176 during input processing: 0 [copy,3451,flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(ord_min_nat,hAPP_nat_nat(minus_minus_nat(A),B)),hAPP_nat_nat(minus_minus_nat(C),B))=hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(hAPP_nat_fun_nat_nat(ord_min_nat,A),C)),B).
% 1.93/2.15    Following clause subsumed by 3181 during input processing: 0 [copy,3452,flip.1] {-} hAPP_nat_nat(minus_minus_nat(hAPP_nat_nat(minus_minus_nat(A),B)),C)=hAPP_nat_nat(minus_minus_nat(A),hAPP_nat_nat(plus_plus_nat(B),C)).
% 1.93/2.15    Following clause subsumed by 3216 during input processing: 0 [copy,3459,flip.1] {-} hAPP_nat_nat(hAPP_nat_fun_nat_nat(ord_min_nat,A),hAPP_nat_nat(suc,B))=hAPP_nat_nat(nat_case_nat(zero_zero_nat,hAPP_f1914919701at_nat(hAPP_f1585078997at_nat(cOMBB_nat_nat_nat,suc),hAPP_nat_fun_nat_nat(hAPP_f416620757at_nat(cOMBC_nat_nat_nat,ord_min_nat),B))),A).
% 1.93/2.15    Following clause subsumed by 3255 during input processing: 0 [copy,3469,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.93/2.15    Following clause subsumed by 3256 during input processing: 0 [copy,3470,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.93/2.15    Following clause subsumed by 3261 during input processing: 0 [copy,3471,flip.1] {-} hAPP_bool_bool(hAPP_b589554111l_bool(hAPP_f1897201897l_bool(cOMBC_bool_bool_bool,A),B),C)=hAPP_bool_bool(hAPP_b589554111l_bool(A,C),B).
% 1.93/2.15    Following clause subsumed by 3264 during input processing: 0 [copy,3472,flip.1] {-} hAPP_bool_bool(hAPP_f961197973l_bool(hAPP_f1996228283l_bool(cOMBC_1455277858l_bool,A),B),C)=hAPP_f387058535l_bool(hAPP_b1787118453l_bool(A,C),B).
% 1.93/2.15    Following clause subsumed by 3265 during input processing: 0 [copy,3473,flip.1] {-} hAPP_A862370221t_bool(hAPP_f2014742713t_bool(hAPP_f27970449t_bool(cOMBB_2104979073le_alt,A),B),C)=hAPP_bool_bool(A,hAPP_A862370221t_bool(B,C)).
% 1.93/2.15    Following clause subsumed by 3266 during input processing: 0 [copy,3474,flip.1] {-} hAPP_A1785763630i_bool(hAPP_f580451669i_bool(hAPP_f1250179763i_bool(cOMBB_1141363506e_indi,A),B),C)=hAPP_bool_bool(A,hAPP_A1785763630i_bool(B,C)).
% 1.93/2.15    Following clause subsumed by 3267 during input processing: 0 [copy,3475,flip.1] {-} hAPP_A862370221t_bool(hAPP_A1664620203t_bool(hAPP_f825175477t_bool(cOMBC_1628726426t_bool,A),B),C)=hAPP_A862370221t_bool(hAPP_A1664620203t_bool(A,C),B).
% 1.93/2.15    Following clause subsumed by 3268 during input processing: 0 [copy,3476,flip.1] {-} hAPP_A1785763630i_bool(hAPP_A313542399i_bool(hAPP_f585152361i_bool(cOMBC_1428934564i_bool,A),B),C)=hAPP_A1785763630i_bool(hAPP_A313542399i_bool(A,C),B).
% 1.93/2.15    Following clause subsumed by 3269 during input processing: 0 [copy,3477,flip.1] {-} hAPP_n1875670159le_alt(hAPP_A1043896845le_alt(hAPP_f1956511609le_alt(cOMBC_1697899890le_alt,A),B),C)=hAPP_A832564074le_alt(hAPP_n49391885le_alt(A,C),B).
% 1.93/2.15    Following clause subsumed by 3270 during input processing: 0 [copy,3478,flip.1] {-} hAPP_A862370221t_bool(hAPP_f2014742713t_bool(hAPP_f1382209403t_bool(cOMBC_1745481870l_bool,A),B),C)=hAPP_f2013399995l_bool(hAPP_A297543629l_bool(A,C),B).
% 1.93/2.15    Following clause subsumed by 3275 during input processing: 0 [copy,3479,flip.1] {-} hAPP_P606313927t_bool(hAPP_f515126293t_bool(hAPP_f600409331t_bool(cOMBB_433601099le_alt,A),B),C)=hAPP_bool_bool(A,hAPP_P606313927t_bool(B,C)).
% 1.93/2.15    Following clause subsumed by 3276 during input processing: 0 [copy,3480,flip.1] {-} hAPP_A1785763630i_bool(hAPP_f580451669i_bool(hAPP_f712459161i_bool(cOMBC_1781321570l_bool,A),B),C)=hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(A,C),B).
% 1.93/2.15    Following clause subsumed by 3281 during input processing: 0 [copy,3481,flip.1] {-} hAPP_n1875670159le_alt(hAPP_l382792410le_alt(hAPP_f2068969285le_alt(cOMBC_1511969967le_alt,A),B),C)=hAPP_l726444215le_alt(hAPP_n2139729636le_alt(A,C),B).
% 1.93/2.15    Following clause subsumed by 3286 during input processing: 0 [copy,3482,flip.1] {-} hAPP_A862370221t_bool(hAPP_f1457563459t_bool(hAPP_f724700817t_bool(cOMBB_164218871le_alt,A),B),C)=hAPP_P606313927t_bool(A,hAPP_A702847159le_alt(B,C)).
% 1.93/2.17    Following clause subsumed by 3287 during input processing: 0 [copy,3483,flip.1] {-} hAPP_P1327827171t_bool(hAPP_f1642286869t_bool(hAPP_f62793075t_bool(cOMBB_1604919143le_alt,A),B),C)=hAPP_bool_bool(A,hAPP_P1327827171t_bool(B,C)).
% 1.93/2.17    Following clause subsumed by 3446 during input processing: 0 [copy,3484,flip.1] {-} hAPP_n1875670159le_alt(nat_ca14895078le_alt(nil_Ar126264853le_alt,hAPP_f402821245le_alt(hAPP_f548810715le_alt(cOMBB_903467948lt_nat,hAPP_A408086601le_alt(cons_A1216297413le_alt,A)),hAPP_l382792410le_alt(hAPP_f2068969285le_alt(cOMBC_1511969967le_alt,take_A1601602045le_alt),B))),C)=hAPP_l726444215le_alt(hAPP_n2139729636le_alt(take_A1601602045le_alt,C),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),A)).
% 1.93/2.17    Following clause subsumed by 3445 during input processing: 0 [copy,3485,flip.1] {-} hAPP_n1875670159le_alt(nat_ca14895078le_alt(hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),A),B),hAPP_l382792410le_alt(hAPP_f2068969285le_alt(cOMBC_1511969967le_alt,drop_A186780501le_alt),A)),C)=hAPP_l726444215le_alt(hAPP_n2139729636le_alt(drop_A186780501le_alt,C),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),A),B)).
% 1.93/2.17    Following clause subsumed by 3444 during input processing: 0 [copy,3486,flip.1] {-} hAPP_n1875670159le_alt(nat_ca14895078le_alt(hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),A),B),hAPP_f402821245le_alt(hAPP_f548810715le_alt(cOMBB_903467948lt_nat,hAPP_A408086601le_alt(cons_A1216297413le_alt,C)),hAPP_A1043896845le_alt(hAPP_f1956511609le_alt(cOMBC_1697899890le_alt,list_u1050032253le_alt(A)),B))),D)=hAPP_A832564074le_alt(hAPP_n49391885le_alt(list_u1050032253le_alt(hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),A),C)),D),B).
% 1.93/2.17    Following clause subsumed by 3437 during input processing: 0 [copy,3488,flip.1] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),C))=hAPP_A832564074le_alt(hAPP_n49391885le_alt(list_u1050032253le_alt(hAPP_l726444215le_alt(hAPP_l568342716le_alt(append1166636842le_alt,A),hAPP_A832564074le_alt(hAPP_l618618165le_alt(hAPP_f657005563le_alt(cOMBC_1919297930le_alt,cons_A1216297413le_alt),B),D))),hAPP_l1872264749lt_nat(size_s1873794948le_alt,A)),C).
% 1.93/2.17  3604 back subsumes 3439.
% 1.93/2.17    Following clause subsumed by 3293 during input processing: 0 [copy,3690,flip.1] {-} hAPP_A1664620203t_bool(hAPP_f825175477t_bool(hAPP_f57507985t_bool(cOMBB_1171600517le_alt,A),B),C)=hAPP_f2014742713t_bool(A,hAPP_A1664620203t_bool(B,C)).
% 1.93/2.17    Following clause subsumed by 3294 during input processing: 0 [copy,3691,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.93/2.17    Following clause subsumed by 3295 during input processing: 0 [copy,3692,flip.1] {-} hAPP_l726444215le_alt(hAPP_l568342716le_alt(hAPP_f1294513379le_alt(cOMBC_1058495865le_alt,A),B),C)=hAPP_l726444215le_alt(hAPP_l568342716le_alt(A,C),B).
% 1.93/2.17    Following clause subsumed by 3300 during input processing: 0 [copy,3693,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.93/2.17    Following clause subsumed by 3301 during input processing: 0 [copy,3694,flip.1] {-} hAPP_P606313927t_bool(hAPP_P1267694911t_bool(hAPP_f135580393t_bool(cOMBC_607108822t_bool,A),B),C)=hAPP_P606313927t_bool(hAPP_P1267694911t_bool(A,C),B).
% 1.93/2.17    Following clause subsumed by 3302 during input processing: 0 [copy,3695,flip.1] {-} hAPP_l1386638586t_bool(hAPP_f318645548t_bool(hAPP_f1728064559t_bool(cOMBC_1740746827l_bool,A),B),C)=hAPP_f1634113933l_bool(hAPP_l578398296l_bool(A,C),B).
% 2.11/2.32    Following clause subsumed by 3303 during input processing: 0 [copy,3696,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).
% 2.11/2.32  3733 back subsumes 3731.
% 2.11/2.32  3733 back subsumes 3730.
% 2.11/2.32  3733 back subsumes 3722.
% 2.11/2.32  3738 back subsumes 3734.
% 2.11/2.32  3750 back subsumes 3748.
% 2.11/2.32  3750 back subsumes 3745.
% 2.11/2.32  3760 back subsumes 3757.
% 2.11/2.32  3760 back subsumes 3729.
% 2.11/2.32  3760 back subsumes 3726.
% 2.11/2.32  3760 back subsumes 3725.
% 2.11/2.32  3760 back subsumes 3721.
% 2.11/2.32  3761 back subsumes 3758.
% 2.11/2.32  3761 back subsumes 3728.
% 2.11/2.32  3761 back subsumes 3727.
% 2.11/2.32  3781 back subsumes 3780.
% 2.11/2.32  3783 back subsumes 3782.
% 2.11/2.32  3787 back subsumes 3784.
% 2.11/2.32  3788 back subsumes 3785.
% 2.11/2.32  3802 back subsumes 3797.
% 2.11/2.32  3802 back subsumes 3793.
% 2.11/2.32  3816 back subsumes 3815.
% 2.11/2.32  3824 back subsumes 3820.
% 2.11/2.32  3839 back subsumes 3834.
% 2.11/2.32  3839 back subsumes 3827.
% 2.11/2.32  3841 back subsumes 3840.
% 2.11/2.32  3848 back subsumes 3846.
% 2.11/2.32  3848 back subsumes 3843.
% 2.11/2.32  3851 back subsumes 3850.
% 2.11/2.32  3857 back subsumes 3855.
% 2.11/2.32  3857 back subsumes 3853.
% 2.11/2.32    Following clause subsumed by 3312 during input processing: 0 [copy,4044,flip.1] {-} hAPP_l391088160le_alt(hAPP_f216801278le_alt(hAPP_f1349184697le_alt(cOMBB_1818168801le_alt,A),B),C)=hAPP_l391088160le_alt(A,hAPP_l726444215le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3313 during input processing: 0 [copy,4045,flip.1] {-} hAPP_f592646513l_bool(hAPP_f863359027l_bool(hAPP_f495827653l_bool(cOMBC_1136104858l_bool,A),B),C)=hAPP_f592646513l_bool(hAPP_f863359027l_bool(A,C),B).
% 2.11/2.32    Following clause subsumed by 3314 during input processing: 0 [copy,4046,flip.1] {-} hAPP_A1664620203t_bool(hAPP_f231379647t_bool(hAPP_f1460305297t_bool(cOMBB_2048157563le_alt,A),B),C)=hAPP_f1457563459t_bool(A,hAPP_A1505516597le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3315 during input processing: 0 [copy,4047,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).
% 2.11/2.32    Following clause subsumed by 3318 during input processing: 0 [copy,4048,flip.1] {-} hAPP_P1327827171t_bool(hAPP_P163071551t_bool(hAPP_f2139078121t_bool(cOMBC_1470522126t_bool,A),B),C)=hAPP_P1327827171t_bool(hAPP_P163071551t_bool(A,C),B).
% 2.11/2.32    Following clause subsumed by 3321 during input processing: 0 [copy,4049,flip.1] {-} hAPP_A187815023l_bool(hAPP_f1539445765l_bool(hAPP_f1688983057l_bool(cOMBB_84213429le_alt,A),B),C)=hAPP_P229966473l_bool(A,hAPP_A702847159le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3324 during input processing: 0 [copy,4050,flip.1] {-} hAPP_P1327827171t_bool(hAPP_f1642286869t_bool(hAPP_f1297597679t_bool(cOMBC_188453282l_bool,A),B),C)=hAPP_f1634113933l_bool(hAPP_P1610428353l_bool(A,C),B).
% 2.11/2.32    Following clause subsumed by 3325 during input processing: 0 [copy,4051,flip.1] {-} hAPP_l1869074853le_alt(hAPP_f1790240989le_alt(hAPP_f1013417831le_alt(cOMBB_2052911494le_alt,A),B),C)=hAPP_l1869074853le_alt(A,hAPP_l726444215le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3328 during input processing: 0 [copy,4052,flip.1] {-} hAPP_l391088160le_alt(hAPP_f1514103381le_alt(hAPP_f1564521144le_alt(cOMBS_1399042523le_alt,A),B),C)=hAPP_P1056860425le_alt(hAPP_l693571982le_alt(A,C),hAPP_l391088160le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3335 during input processing: 0 [copy,4053,flip.1] {-} hAPP_f965095724l_bool(hAPP_f1577179519l_bool(hAPP_f1688301673l_bool(cOMBC_2105056416l_bool,A),B),C)=hAPP_f965095724l_bool(hAPP_f1577179519l_bool(A,C),B).
% 2.11/2.32    Following clause subsumed by 3340 during input processing: 0 [copy,4054,flip.1] {-} hAPP_l1869074853le_alt(hAPP_f1790240989le_alt(hAPP_f1792349771le_alt(cOMBC_1330649024le_alt,A),B),C)=hAPP_f216801278le_alt(hAPP_l489874441le_alt(A,C),B).
% 2.11/2.32    Following clause subsumed by 3341 during input processing: 0 [copy,4055,flip.1] {-} hAPP_A1553574765l_bool(hAPP_f156764033l_bool(hAPP_f778758417l_bool(cOMBB_2112722489le_alt,A),B),C)=hAPP_f1539445765l_bool(A,hAPP_A1505516597le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3342 during input processing: 0 [copy,4056,flip.1] {-} hAPP_A621939144t_bool(hAPP_f210227915t_bool(hAPP_f758198165t_bool(cOMBB_1769989562e_indi,A),B),C)=hAPP_f344580165t_bool(A,hAPP_A1677245848t_bool(B,C)).
% 2.11/2.32    Following clause subsumed by 3354 during input processing: 0 [copy,4057,flip.1] {-} hAPP_l1629075165l_bool(hAPP_f370419053l_bool(hAPP_f1953650287l_bool(cOMBB_283473102le_alt,A),B),C)=hAPP_f170721165l_bool(A,hAPP_l1869074853le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3355 during input processing: 0 [copy,4058,flip.1] {-} hAPP_l1288188215t_bool(hAPP_f1152779391t_bool(hAPP_f991870303t_bool(cOMBB_353715312le_alt,A),B),C)=hAPP_f1728064559t_bool(A,hAPP_l1629075165l_bool(B,C)).
% 2.11/2.32    Following clause subsumed by 3358 during input processing: 0 [copy,4059,flip.1] {-} hAPP_l1406283231le_alt(hAPP_f469186021le_alt(hAPP_f1933751673le_alt(cOMBB_1193902096le_alt,A),B),C)=hAPP_f2001490223le_alt(A,hAPP_l1869074853le_alt(B,C)).
% 2.11/2.32    Following clause subsumed by 3359 during input processing: 0 [copy,4060,flip.1] {-} hAPP_f312250286l_bool(hAPP_f1577576703l_bool(hAPP_f1556356969l_bool(cOMBC_1576836772l_bool,A),B),C)=hAPP_f312250286l_bool(hAPP_f1577576703l_bool(A,C),B).
% 2.11/2.32  
% 2.11/2.32  ======= end of input processing =======
% 2.11/2.32  
% 2.11/2.32  SEGMENTATION FAULT!!  This is probably caused by a
% 2.11/2.32  bug in Otter.  Please send copy of the input file to
% 2.11/2.32  otter@mcs.anl.gov, let us know what version of Otter you are
% 2.11/2.32  using, and send any other info that might be useful.
% 2.11/2.32  
% 2.11/2.32  
% 2.11/2.32  SEGMENTATION FAULT!!  This is probably caused by a
% 2.11/2.32  bug in Otter.  Please send copy of the input file to
% 2.11/2.32  otter@mcs.anl.gov, let us know what version of Otter you are
% 2.11/2.32  using, and send any other info that might be useful.
% 2.11/2.32  
% 2.11/2.32  
% 2.11/2.32  The job finished Sat Jul  2 03:05:56 2022
%------------------------------------------------------------------------------