%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SWW477+3 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 01:27:03 EDT 2022
% Result : Unknown 0.94s 1.15s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW477+3 : TPTP v8.1.0. Released v5.3.0.
% 0.11/0.13 % Command : sos-script %s
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sun Jun 5 17:38:08 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.81/0.99 ----- Otter 3.2, August 2001 -----
% 0.81/0.99 The process was started by sandbox2 on n027.cluster.edu,
% 0.81/0.99 Sun Jun 5 17:38:08 2022
% 0.81/0.99 The command was "./sos". The process ID is 12065.
% 0.81/0.99
% 0.81/0.99 set(prolog_style_variables).
% 0.81/0.99 set(auto).
% 0.81/0.99 dependent: set(auto1).
% 0.81/0.99 dependent: set(process_input).
% 0.81/0.99 dependent: clear(print_kept).
% 0.81/0.99 dependent: clear(print_new_demod).
% 0.81/0.99 dependent: clear(print_back_demod).
% 0.81/0.99 dependent: clear(print_back_sub).
% 0.81/0.99 dependent: set(control_memory).
% 0.81/0.99 dependent: assign(max_mem, 12000).
% 0.81/0.99 dependent: assign(pick_given_ratio, 4).
% 0.81/0.99 dependent: assign(stats_level, 1).
% 0.81/0.99 dependent: assign(pick_semantic_ratio, 3).
% 0.81/0.99 dependent: assign(sos_limit, 5000).
% 0.81/0.99 dependent: assign(max_weight, 60).
% 0.81/0.99 clear(print_given).
% 0.81/0.99
% 0.81/0.99 formula_list(usable).
% 0.81/0.99
% 0.81/0.99 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=10.
% 0.81/0.99
% 0.81/0.99 This ia a non-Horn set with equality. The strategy will be
% 0.81/0.99 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.81/0.99 unit deletion, with positive clauses in sos and nonpositive
% 0.81/0.99 clauses in usable.
% 0.81/0.99
% 0.81/0.99 dependent: set(knuth_bendix).
% 0.81/0.99 dependent: set(para_from).
% 0.81/0.99 dependent: set(para_into).
% 0.81/0.99 dependent: clear(para_from_right).
% 0.81/0.99 dependent: clear(para_into_right).
% 0.81/0.99 dependent: set(para_from_vars).
% 0.81/0.99 dependent: set(eq_units_both_ways).
% 0.81/0.99 dependent: set(dynamic_demod_all).
% 0.81/0.99 dependent: set(dynamic_demod).
% 0.81/0.99 dependent: set(order_eq).
% 0.81/0.99 dependent: set(back_demod).
% 0.81/0.99 dependent: set(lrpo).
% 0.81/0.99 dependent: set(hyper_res).
% 0.81/0.99 dependent: set(unit_deletion).
% 0.81/0.99 dependent: set(factor).
% 0.81/0.99
% 0.81/0.99 ------------> process usable:
% 0.81/0.99 Following clause subsumed by 11 during input processing: 0 [flip.1] {-} nt!=boolean.
% 0.81/0.99 Following clause subsumed by 27 during input processing: 0 [] {-} void!=nt.
% 0.81/0.99 Following clause subsumed by 29 during input processing: 0 [] {-} void!=boolean.
% 0.81/0.99 Following clause subsumed by 32 during input processing: 0 [] {-} hAPP_P295788316har_ty(hAPP_l848957697har_ty(produc1002914035har_ty,A),B)!=hAPP_P295788316har_ty(hAPP_l848957697har_ty(produc1002914035har_ty,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 33 during input processing: 0 [] {-} hAPP_P295788316har_ty(hAPP_l848957697har_ty(produc1002914035har_ty,A),B)!=hAPP_P295788316har_ty(hAPP_l848957697har_ty(produc1002914035har_ty,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 34 during input processing: 0 [] {-} hAPP_t1875766236har_ty(hAPP_l1948972481har_ty(produc251930284har_ty,A),B)!=hAPP_t1875766236har_ty(hAPP_l1948972481har_ty(produc251930284har_ty,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 35 during input processing: 0 [] {-} hAPP_t1875766236har_ty(hAPP_l1948972481har_ty(produc251930284har_ty,A),B)!=hAPP_t1875766236har_ty(hAPP_l1948972481har_ty(produc251930284har_ty,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 36 during input processing: 0 [] {-} hAPP_P976385092ar_val(hAPP_P800634639ar_val(produc1317546007ar_val,A),B)!=hAPP_P976385092ar_val(hAPP_P800634639ar_val(produc1317546007ar_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 37 during input processing: 0 [] {-} hAPP_P976385092ar_val(hAPP_P800634639ar_val(produc1317546007ar_val,A),B)!=hAPP_P976385092ar_val(hAPP_P800634639ar_val(produc1317546007ar_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 38 during input processing: 0 [] {-} hAPP_P1342907945t_char(hAPP_P91410073t_char(produc1897818327t_char,A),B)!=hAPP_P1342907945t_char(hAPP_P91410073t_char(produc1897818327t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 39 during input processing: 0 [] {-} hAPP_P1342907945t_char(hAPP_P91410073t_char(produc1897818327t_char,A),B)!=hAPP_P1342907945t_char(hAPP_P91410073t_char(produc1897818327t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 40 during input processing: 0 [] {-} hAPP_P1247668062t_char(hAPP_P1756548163t_char(produc635935767t_char,A),B)!=hAPP_P1247668062t_char(hAPP_P1756548163t_char(produc635935767t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 41 during input processing: 0 [] {-} hAPP_P1247668062t_char(hAPP_P1756548163t_char(produc635935767t_char,A),B)!=hAPP_P1247668062t_char(hAPP_P1756548163t_char(produc635935767t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 42 during input processing: 0 [] {-} hAPP_P579374437t_char(hAPP_P777914897t_char(produc1431439831t_char,A),B)!=hAPP_P579374437t_char(hAPP_P777914897t_char(produc1431439831t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 43 during input processing: 0 [] {-} hAPP_P579374437t_char(hAPP_P777914897t_char(produc1431439831t_char,A),B)!=hAPP_P579374437t_char(hAPP_P777914897t_char(produc1431439831t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 44 during input processing: 0 [] {-} hAPP_P991802092t_char(hAPP_P1958775007t_char(produc1641293463t_char,A),B)!=hAPP_P991802092t_char(hAPP_P1958775007t_char(produc1641293463t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 45 during input processing: 0 [] {-} hAPP_P991802092t_char(hAPP_P1958775007t_char(produc1641293463t_char,A),B)!=hAPP_P991802092t_char(hAPP_P1958775007t_char(produc1641293463t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 46 during input processing: 0 [] {-} hAPP_P1657265855t_char(hAPP_P1071727823t_char(produc2080520419t_char,A),B)!=hAPP_P1657265855t_char(hAPP_P1071727823t_char(produc2080520419t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 47 during input processing: 0 [] {-} hAPP_P1657265855t_char(hAPP_P1071727823t_char(produc2080520419t_char,A),B)!=hAPP_P1657265855t_char(hAPP_P1071727823t_char(produc2080520419t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 48 during input processing: 0 [] {-} hAPP_P330218428on_val(hAPP_P1875010047on_val(produc499151895on_val,A),B)!=hAPP_P330218428on_val(hAPP_P1875010047on_val(produc499151895on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 49 during input processing: 0 [] {-} hAPP_P330218428on_val(hAPP_P1875010047on_val(produc499151895on_val,A),B)!=hAPP_P330218428on_val(hAPP_P1875010047on_val(produc499151895on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 50 during input processing: 0 [] {-} hAPP_P47773639al_val(hAPP_P1874979071al_val(produc1244920211al_val,A),B)!=hAPP_P47773639al_val(hAPP_P1874979071al_val(produc1244920211al_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 51 during input processing: 0 [] {-} hAPP_P47773639al_val(hAPP_P1874979071al_val(produc1244920211al_val,A),B)!=hAPP_P47773639al_val(hAPP_P1874979071al_val(produc1244920211al_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 52 during input processing: 0 [] {-} hAPP_P2123720426al_val(hAPP_P1538518401al_val(produc1924279125al_val,A),B)!=hAPP_P2123720426al_val(hAPP_P1538518401al_val(produc1924279125al_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 53 during input processing: 0 [] {-} hAPP_P2123720426al_val(hAPP_P1538518401al_val(produc1924279125al_val,A),B)!=hAPP_P2123720426al_val(hAPP_P1538518401al_val(produc1924279125al_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 54 during input processing: 0 [] {-} hAPP_P1220989409t_char(hAPP_P1668407995t_char(produc1299387215t_char,A),B)!=hAPP_P1220989409t_char(hAPP_P1668407995t_char(produc1299387215t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 55 during input processing: 0 [] {-} hAPP_P1220989409t_char(hAPP_P1668407995t_char(produc1299387215t_char,A),B)!=hAPP_P1220989409t_char(hAPP_P1668407995t_char(produc1299387215t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 56 during input processing: 0 [] {-} hAPP_P1333668416t_char(hAPP_P1859316965t_char(produc57279289t_char,A),B)!=hAPP_P1333668416t_char(hAPP_P1859316965t_char(produc57279289t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 57 during input processing: 0 [] {-} hAPP_P1333668416t_char(hAPP_P1859316965t_char(produc57279289t_char,A),B)!=hAPP_P1333668416t_char(hAPP_P1859316965t_char(produc57279289t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 58 during input processing: 0 [] {-} hAPP_P1539798428t_char(hAPP_P719127871t_char(produc24551831t_char,A),B)!=hAPP_P1539798428t_char(hAPP_P719127871t_char(produc24551831t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 59 during input processing: 0 [] {-} hAPP_P1539798428t_char(hAPP_P719127871t_char(produc24551831t_char,A),B)!=hAPP_P1539798428t_char(hAPP_P719127871t_char(produc24551831t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 60 during input processing: 0 [] {-} hAPP_P1758592847on_val(hAPP_P2015431471on_val(produc1951691075on_val,A),B)!=hAPP_P1758592847on_val(hAPP_P2015431471on_val(produc1951691075on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 61 during input processing: 0 [] {-} hAPP_P1758592847on_val(hAPP_P2015431471on_val(produc1951691075on_val,A),B)!=hAPP_P1758592847on_val(hAPP_P2015431471on_val(produc1951691075on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 62 during input processing: 0 [] {-} hAPP_P1486793863on_val(hAPP_P2077211775on_val(produc1564932627on_val,A),B)!=hAPP_P1486793863on_val(hAPP_P2077211775on_val(produc1564932627on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 63 during input processing: 0 [] {-} hAPP_P1486793863on_val(hAPP_P2077211775on_val(produc1564932627on_val,A),B)!=hAPP_P1486793863on_val(hAPP_P2077211775on_val(produc1564932627on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 64 during input processing: 0 [] {-} hAPP_P291613419on_val(hAPP_P265246237on_val(produc870913623on_val,A),B)!=hAPP_P291613419on_val(hAPP_P265246237on_val(produc870913623on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 65 during input processing: 0 [] {-} hAPP_P291613419on_val(hAPP_P265246237on_val(produc870913623on_val,A),B)!=hAPP_P291613419on_val(hAPP_P265246237on_val(produc870913623on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 66 during input processing: 0 [] {-} hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,A),B)!=hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 67 during input processing: 0 [] {-} hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,A),B)!=hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 68 during input processing: 0 [] {-} hAPP_P242904598t_char(hAPP_l1388836853t_char(produc1331140167t_char,A),B)!=hAPP_P242904598t_char(hAPP_l1388836853t_char(produc1331140167t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 69 during input processing: 0 [] {-} hAPP_P242904598t_char(hAPP_l1388836853t_char(produc1331140167t_char,A),B)!=hAPP_P242904598t_char(hAPP_l1388836853t_char(produc1331140167t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 70 during input processing: 0 [] {-} hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A),B)!=hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 71 during input processing: 0 [] {-} hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A),B)!=hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 72 during input processing: 0 [] {-} hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A),B)!=hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 73 during input processing: 0 [] {-} hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A),B)!=hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 74 during input processing: 0 [] {-} hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A),B)!=hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 75 during input processing: 0 [] {-} hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A),B)!=hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 76 during input processing: 0 [] {-} hAPP_P658340954on_val(hAPP_P1526035745on_val(produc1611380469on_val,A),B)!=hAPP_P658340954on_val(hAPP_P1526035745on_val(produc1611380469on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 77 during input processing: 0 [] {-} hAPP_P658340954on_val(hAPP_P1526035745on_val(produc1611380469on_val,A),B)!=hAPP_P658340954on_val(hAPP_P1526035745on_val(produc1611380469on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 78 during input processing: 0 [] {-} hAPP_P1963616220on_val(hAPP_l1275479261on_val(produc379668296on_val,A),B)!=hAPP_P1963616220on_val(hAPP_l1275479261on_val(produc379668296on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 79 during input processing: 0 [] {-} hAPP_P1963616220on_val(hAPP_l1275479261on_val(produc379668296on_val,A),B)!=hAPP_P1963616220on_val(hAPP_l1275479261on_val(produc379668296on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 80 during input processing: 0 [] {-} hAPP_P767818445t_char(hAPP_l1873467853t_char(produc921874948t_char,A),B)!=hAPP_P767818445t_char(hAPP_l1873467853t_char(produc921874948t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 81 during input processing: 0 [] {-} hAPP_P767818445t_char(hAPP_l1873467853t_char(produc921874948t_char,A),B)!=hAPP_P767818445t_char(hAPP_l1873467853t_char(produc921874948t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 82 during input processing: 0 [] {-} hAPP_P1392904962t_char(hAPP_l14371579t_char(produc1909267824t_char,A),B)!=hAPP_P1392904962t_char(hAPP_l14371579t_char(produc1909267824t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 83 during input processing: 0 [] {-} hAPP_P1392904962t_char(hAPP_l14371579t_char(produc1909267824t_char,A),B)!=hAPP_P1392904962t_char(hAPP_l14371579t_char(produc1909267824t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 84 during input processing: 0 [] {-} hAPP_e1752110927t_char(hAPP_l1859255743t_char(produc1916172923t_char,A),B)!=hAPP_e1752110927t_char(hAPP_l1859255743t_char(produc1916172923t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 85 during input processing: 0 [] {-} hAPP_e1752110927t_char(hAPP_l1859255743t_char(produc1916172923t_char,A),B)!=hAPP_e1752110927t_char(hAPP_l1859255743t_char(produc1916172923t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 86 during input processing: 0 [] {-} -is_bop(A)| -is_bop(B)|hAPP_P929466802al_val(hAPP_b1229254591al_val(produc621191550al_val,A),C)!=hAPP_P929466802al_val(hAPP_b1229254591al_val(produc621191550al_val,B),D)|A=B.
% 0.81/0.99 Following clause subsumed by 87 during input processing: 0 [] {-} -is_bop(A)| -is_bop(B)|hAPP_P929466802al_val(hAPP_b1229254591al_val(produc621191550al_val,A),C)!=hAPP_P929466802al_val(hAPP_b1229254591al_val(produc621191550al_val,B),D)|C=D.
% 0.81/0.99 Following clause subsumed by 88 during input processing: 0 [] {-} hAPP_v852496844al_val(hAPP_v1519391al_val(product_Pair_val_val,A),B)!=hAPP_v852496844al_val(hAPP_v1519391al_val(product_Pair_val_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 89 during input processing: 0 [] {-} hAPP_v852496844al_val(hAPP_v1519391al_val(product_Pair_val_val,A),B)!=hAPP_v852496844al_val(hAPP_v1519391al_val(product_Pair_val_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 90 during input processing: 0 [] {-} hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,A),B)!=hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 91 during input processing: 0 [] {-} hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,A),B)!=hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 92 during input processing: 0 [] {-} hAPP_l2100324114t_char(hAPP_l208357873t_char(produc5062597t_char,A),B)!=hAPP_l2100324114t_char(hAPP_l208357873t_char(produc5062597t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 93 during input processing: 0 [] {-} hAPP_l2100324114t_char(hAPP_l208357873t_char(produc5062597t_char,A),B)!=hAPP_l2100324114t_char(hAPP_l208357873t_char(produc5062597t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 94 during input processing: 0 [] {-} hAPP_P1224499548t_char(hAPP_l902950593t_char(produc822965838t_char,A),B)!=hAPP_P1224499548t_char(hAPP_l902950593t_char(produc822965838t_char,C),D)|A=C.
% 0.81/0.99 Following clause subsumed by 95 during input processing: 0 [] {-} hAPP_P1224499548t_char(hAPP_l902950593t_char(produc822965838t_char,A),B)!=hAPP_P1224499548t_char(hAPP_l902950593t_char(produc822965838t_char,C),D)|B=D.
% 0.81/0.99 Following clause subsumed by 96 during input processing: 0 [] {-} hAPP_P1423780764t_char(hAPP_l309186817t_char(produc1483578759t_char,A),B)!=hAPP_P1423780764t_char(hAPP_l309186817t_char(produc1483578759t_char,C),D)|A=C.
% 0.81/1.00 Following clause subsumed by 97 during input processing: 0 [] {-} hAPP_P1423780764t_char(hAPP_l309186817t_char(produc1483578759t_char,A),B)!=hAPP_P1423780764t_char(hAPP_l309186817t_char(produc1483578759t_char,C),D)|B=D.
% 0.81/1.00 Following clause subsumed by 98 during input processing: 0 [] {-} hAPP_l277216047t_char(hAPP_l352172327t_char(produc1152259904t_char,A),B)!=hAPP_l277216047t_char(hAPP_l352172327t_char(produc1152259904t_char,C),D)|A=C.
% 0.81/1.00 Following clause subsumed by 99 during input processing: 0 [] {-} hAPP_l277216047t_char(hAPP_l352172327t_char(produc1152259904t_char,A),B)!=hAPP_l277216047t_char(hAPP_l352172327t_char(produc1152259904t_char,C),D)|B=D.
% 0.81/1.00 Following clause subsumed by 100 during input processing: 0 [] {-} hAPP_e952791821t_char(hAPP_l796364813t_char(produc1147572817t_char,A),B)!=hAPP_e952791821t_char(hAPP_l796364813t_char(produc1147572817t_char,C),D)|A=C.
% 0.81/1.00 Following clause subsumed by 101 during input processing: 0 [] {-} hAPP_e952791821t_char(hAPP_l796364813t_char(produc1147572817t_char,A),B)!=hAPP_e952791821t_char(hAPP_l796364813t_char(produc1147572817t_char,C),D)|B=D.
% 0.81/1.00 Following clause subsumed by 102 during input processing: 0 [] {-} hAPP_v48258637ar_val(hAPP_P1321848547ar_val(produc2036181286ar_val,A),B)!=hAPP_v48258637ar_val(hAPP_P1321848547ar_val(produc2036181286ar_val,C),D)|A=C.
% 0.81/1.00 Following clause subsumed by 103 during input processing: 0 [] {-} hAPP_v48258637ar_val(hAPP_P1321848547ar_val(produc2036181286ar_val,A),B)!=hAPP_v48258637ar_val(hAPP_P1321848547ar_val(produc2036181286ar_val,C),D)|B=D.
% 0.81/1.00 Following clause subsumed by 458 during input processing: 0 [] {-} -hBOOL(hAPP_P748443392y_bool(hAPP_l1665608433y_bool(A,B),C))|hBOOL(hAPP_P831231943y_bool(hAPP_f1134484787y_bool(produc802464979y_bool,A),hAPP_P295788316har_ty(hAPP_l848957697har_ty(produc1002914035har_ty,B),C))).
% 0.81/1.00 Following clause subsumed by 459 during input processing: 0 [] {-} -hBOOL(hAPP_ty_bool(hAPP_l1734756650y_bool(A,B),C))|hBOOL(hAPP_P748443392y_bool(hAPP_f695389733y_bool(produc1322037260y_bool,A),hAPP_t1875766236har_ty(hAPP_l1948972481har_ty(produc251930284har_ty,B),C))).
% 0.81/1.00 Following clause subsumed by 460 during input processing: 0 [] {-} -hBOOL(hAPP_P1070896250l_bool(hAPP_P1236192325l_bool(A,B),C))|hBOOL(hAPP_P439015943l_bool(hAPP_f1653906803l_bool(produc891186911l_bool,A),hAPP_P976385092ar_val(hAPP_P800634639ar_val(produc1317546007ar_val,B),C))).
% 0.81/1.00 Following clause subsumed by 461 during input processing: 0 [] {-} -hBOOL(hAPP_P2014166431r_bool(hAPP_P1939418767r_bool(A,B),C))|hBOOL(hAPP_P1002912327r_bool(hAPP_f1728305001r_bool(produc1946648479r_bool,A),hAPP_P1342907945t_char(hAPP_P91410073t_char(produc1897818327t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 462 during input processing: 0 [] {-} -hBOOL(hAPP_P828904212r_bool(hAPP_P225001977r_bool(A,B),C))|hBOOL(hAPP_P801803911r_bool(hAPP_f1760165311r_bool(produc1458513631r_bool,A),hAPP_P1247668062t_char(hAPP_P1756548163t_char(produc635935767t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 463 during input processing: 0 [] {-} -hBOOL(hAPP_P659547099r_bool(hAPP_P194929415r_bool(A,B),C))|hBOOL(hAPP_P929449287r_bool(hAPP_f1774800369r_bool(produc1113940127r_bool,A),hAPP_P579374437t_char(hAPP_P777914897t_char(produc1431439831t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 464 during input processing: 0 [] {-} -hBOOL(hAPP_P1680401186r_bool(hAPP_P1117344277r_bool(A,B),C))|hBOOL(hAPP_P975284999r_bool(hAPP_f72760099r_bool(produc310626655r_bool,A),hAPP_P991802092t_char(hAPP_P1958775007t_char(produc1641293463t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 465 during input processing: 0 [] {-} -hBOOL(hAPP_P449474095r_bool(hAPP_P663876415r_bool(A,B),C))|hBOOL(hAPP_P2010574925r_bool(hAPP_f39862969r_bool(produc1131232171r_bool,A),hAPP_P1657265855t_char(hAPP_P1071727823t_char(produc2080520419t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 466 during input processing: 0 [] {-} -hBOOL(hAPP_P1235399154l_bool(hAPP_P416784693l_bool(A,B),C))|hBOOL(hAPP_P124632071l_bool(hAPP_f834198659l_bool(produc870083295l_bool,A),hAPP_P330218428on_val(hAPP_P1875010047on_val(produc499151895on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP_P929938951l_bool(hAPP_P1815899455l_bool(A,B),C))|hBOOL(hAPP_P2123002749l_bool(hAPP_f1774252649l_bool(produc506816603l_bool,A),hAPP_P47773639al_val(hAPP_P1874979071al_val(produc1244920211al_val,B),C))).
% 0.81/1.00 Following clause subsumed by 468 during input processing: 0 [] {-} -hBOOL(hAPP_P943837928l_bool(hAPP_P323054207l_bool(A,B),C))|hBOOL(hAPP_P738987199l_bool(hAPP_f463140843l_bool(produc1296464157l_bool,A),hAPP_P2123720426al_val(hAPP_P1538518401al_val(produc1924279125al_val,B),C))).
% 0.81/1.00 Following clause subsumed by 469 during input processing: 0 [] {-} -hBOOL(hAPP_P2118621157r_bool(hAPP_P357098431r_bool(A,B),C))|hBOOL(hAPP_P1183499705r_bool(hAPP_f523402917r_bool(produc22827031r_bool,A),hAPP_P1220989409t_char(hAPP_P1668407995t_char(produc1299387215t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 470 during input processing: 0 [] {-} -hBOOL(hAPP_P1907982426r_bool(hAPP_P1214880255r_bool(A,B),C))|hBOOL(hAPP_P1240100515r_bool(hAPP_f1377529935r_bool(produc1470355201r_bool,A),hAPP_P1333668416t_char(hAPP_P1859316965t_char(produc57279289t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 471 during input processing: 0 [] {-} -hBOOL(hAPP_P92196306r_bool(hAPP_P1928969845r_bool(A,B),C))|hBOOL(hAPP_P824029447r_bool(hAPP_f655949763r_bool(produc1294339167r_bool,A),hAPP_P1539798428t_char(hAPP_P719127871t_char(produc24551831t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 472 during input processing: 0 [] {-} -hBOOL(hAPP_P1333315679l_bool(hAPP_P220718911l_bool(A,B),C))|hBOOL(hAPP_P2028072621l_bool(hAPP_f1600283417l_bool(produc376173579l_bool,A),hAPP_P1758592847on_val(hAPP_P2015431471on_val(produc1951691075on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 473 during input processing: 0 [] {-} -hBOOL(hAPP_P282169671l_bool(hAPP_P2062527807l_bool(A,B),C))|hBOOL(hAPP_P378063101l_bool(hAPP_f1363805417l_bool(produc1229156571l_bool,A),hAPP_P1486793863on_val(hAPP_P2077211775on_val(produc1564932627on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 474 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_P1988153107l_bool(A,B),C))|hBOOL(hAPP_P1221872711l_bool(hAPP_f662143077l_bool(produc1193275679l_bool,A),hAPP_P291613419on_val(hAPP_P265246237on_val(produc870913623on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 475 during input processing: 0 [] {-} -hBOOL(hAPP_ty_bool(hAPP_P1845004857y_bool(A,B),C))|hBOOL(hAPP_P27757617y_bool(hAPP_f201105125y_bool(produc1851383869y_bool,A),hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,B),C))).
% 0.81/1.00 Following clause subsumed by 476 during input processing: 0 [] {-} -hBOOL(hAPP_P1187139874r_bool(hAPP_l165010689r_bool(A,B),C))|hBOOL(hAPP_P1384137393r_bool(hAPP_f433337307r_bool(produc65850127r_bool,A),hAPP_P242904598t_char(hAPP_l1388836853t_char(produc1331140167t_char,B),C))).
% 0.81/1.00 Following clause subsumed by 477 during input processing: 0 [] {-} -hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(A,B),C))|hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,A),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 478 during input processing: 0 [] {-} -hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(A,B),C))|hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,A),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 479 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(A,B),C))|hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,A),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 480 during input processing: 0 [] {-} -hBOOL(hAPP_P71593144l_bool(hAPP_P1183008383l_bool(A,B),C))|hBOOL(hAPP_P1333315679l_bool(hAPP_f1525114763l_bool(produc70644925l_bool,A),hAPP_P658340954on_val(hAPP_P1526035745on_val(produc1611380469on_val,B),C))).
% 0.81/1.00 Following clause subsumed by 481 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(A,B),C))|hBOOL(hAPP_P71593144l_bool(hAPP_f1634841927l_bool(produc1491230096l_bool,A),hAPP_P1963616220on_val(hAPP_l1275479261on_val(produc379668296on_val,B),C))).
% 0.81/1.01 Following clause subsumed by 482 during input processing: 0 [] {-} -hBOOL(hAPP_P1907982426r_bool(hAPP_l217977712r_bool(A,B),C))|hBOOL(hAPP_P92196306r_bool(hAPP_f1613448899r_bool(produc2027921764r_bool,A),hAPP_P767818445t_char(hAPP_l1873467853t_char(produc921874948t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 483 during input processing: 0 [] {-} -hBOOL(hAPP_P2118621157r_bool(hAPP_l1987619678r_bool(A,B),C))|hBOOL(hAPP_P1907982426r_bool(hAPP_f102021095r_bool(produc154616760r_bool,A),hAPP_P1392904962t_char(hAPP_l14371579t_char(produc1909267824t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 484 during input processing: 0 [] {-} -hBOOL(hAPP_e544220455r_bool(hAPP_l1062423959r_bool(A,B),C))|hBOOL(hAPP_P2118621157r_bool(hAPP_f1697332217r_bool(produc21910851r_bool,A),hAPP_e1752110927t_char(hAPP_l1859255743t_char(produc1916172923t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 485 during input processing: 0 [] {-} -hBOOL(hAPP_P929938951l_bool(hAPP_b97269396l_bool(A,B),C))|hBOOL(hAPP_P943837928l_bool(hAPP_f340876351l_bool(produc1326056646l_bool,A),hAPP_P929466802al_val(hAPP_b1229254591al_val(produc621191550al_val,B),C))).
% 0.81/1.01 Following clause subsumed by 486 during input processing: 0 [] {-} -hBOOL(hAPP_val_bool(hAPP_v1392248405l_bool(A,B),C))|hBOOL(hAPP_P929938951l_bool(hAPP_f1534412387l_bool(produc769963999l_bool,A),hAPP_v852496844al_val(hAPP_v1519391al_val(product_Pair_val_val,B),C))).
% 0.81/1.01 Following clause subsumed by 487 during input processing: 0 [] {-} -hBOOL(hAPP_f1715346603l_bool(hAPP_l465799708l_bool(A,B),C))|hBOOL(hAPP_P1235399154l_bool(hAPP_f1443410953l_bool(produc392960766l_bool,A),hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,B),C))).
% 0.81/1.01 Following clause subsumed by 488 during input processing: 0 [] {-} -hBOOL(hAPP_list_char_bool(hAPP_l1361600383r_bool(A,B),C))|hBOOL(hAPP_P449474095r_bool(hAPP_f2132060507r_bool(produc1704639885r_bool,A),hAPP_l2100324114t_char(hAPP_l208357873t_char(produc5062597t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 489 during input processing: 0 [] {-} -hBOOL(hAPP_P659547099r_bool(hAPP_l2140727500r_bool(A,B),C))|hBOOL(hAPP_P1680401186r_bool(hAPP_f952817385r_bool(produc723279022r_bool,A),hAPP_P1224499548t_char(hAPP_l902950593t_char(produc822965838t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 490 during input processing: 0 [] {-} -hBOOL(hAPP_P828904212r_bool(hAPP_l1342015621r_bool(A,B),C))|hBOOL(hAPP_P659547099r_bool(hAPP_f252398939r_bool(produc1324280167r_bool,A),hAPP_P1423780764t_char(hAPP_l309186817t_char(produc1483578759t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 491 during input processing: 0 [] {-} -hBOOL(hAPP_l902158906r_bool(hAPP_l24694616r_bool(A,B),C))|hBOOL(hAPP_P828904212r_bool(hAPP_f895126887r_bool(produc1596557472r_bool,A),hAPP_l277216047t_char(hAPP_l352172327t_char(produc1152259904t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 492 during input processing: 0 [] {-} -hBOOL(hAPP_e544220455r_bool(hAPP_l214204733r_bool(A,B),C))|hBOOL(hAPP_P2014166431r_bool(hAPP_f1484794973r_bool(produc1732333873r_bool,A),hAPP_e952791821t_char(hAPP_l796364813t_char(produc1147572817t_char,B),C))).
% 0.81/1.01 Following clause subsumed by 493 during input processing: 0 [] {-} -hBOOL(hAPP_val_bool(hAPP_P486515074l_bool(A,B),C))|hBOOL(hAPP_P1070896250l_bool(hAPP_f1663301111l_bool(produc1873777030l_bool,A),hAPP_v48258637ar_val(hAPP_P1321848547ar_val(produc2036181286ar_val,B),C))).
% 0.81/1.01 Following clause subsumed by 701 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,A),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C)))|hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(A,B),C)).
% 0.81/1.01 Following clause subsumed by 477 during input processing: 0 [] {-} hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,A),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C)))| -hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(A,B),C)).
% 0.86/1.07 Following clause subsumed by 701 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,A),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C)))|hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(A,B),C)).
% 0.86/1.07 Following clause subsumed by 477 during input processing: 0 [] {-} hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,A),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C)))| -hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(A,B),C)).
% 0.86/1.07 Following clause subsumed by 1070 during input processing: 0 [] {-} bool(A)!=unit.
% 0.86/1.07 Following clause subsumed by 1181 during input processing: 0 [] {-} bool(A)!=null.
% 0.86/1.07 Following clause subsumed by 1183 during input processing: 0 [] {-} unit!=null.
% 0.86/1.07 Following clause subsumed by 1212 during input processing: 0 [] {-} -hBOOL(wf_pro755087577t_char(wwf_J_mdecl,A))| -hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(eval(A,B,C),D),E))|hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),C)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,D),E)),transi2024712006on_val(red(A)))).
% 0.86/1.07 Following clause subsumed by 1286 during input processing: 0 [] {-} -hBOOL(wf_pro755087577t_char(wwf_J_mdecl,A))| -hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),C)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,D),E)),transi2024712006on_val(red(A))))| -hBOOL(final_list_char(D))|hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(eval(A,B,C),D),E)).
% 0.86/1.07 Following clause subsumed by 1344 during input processing: 0 [flip.1] {-} addr(A)!=null.
% 0.86/1.07 Following clause subsumed by 1348 during input processing: 0 [] {-} addr(A)!=unit.
% 0.86/1.07 Following clause subsumed by 1374 during input processing: 0 [] {-} void!=integer.
% 0.86/1.07 Following clause subsumed by 1376 during input processing: 0 [] {-} nt!=integer.
% 0.86/1.07 Following clause subsumed by 1378 during input processing: 0 [] {-} integer!=boolean.
% 0.86/1.07 Following clause subsumed by 1401 during input processing: 0 [flip.1] {-} c_Expr_Obop_OEq!=add.
% 0.86/1.07 Following clause subsumed by 1497 during input processing: 0 [] {-} hAPP_list_char_ty(class,A)!=void.
% 0.86/1.07 Following clause subsumed by 1500 during input processing: 0 [flip.1] {-} hAPP_list_char_ty(class,A)!=boolean.
% 0.86/1.07 Following clause subsumed by 1502 during input processing: 0 [] {-} hAPP_list_char_ty(class,A)!=nt.
% 0.86/1.07 Following clause subsumed by 1504 during input processing: 0 [] {-} hAPP_list_char_ty(class,A)!=integer.
% 0.86/1.07 Following clause subsumed by 1564 during input processing: 0 [] {-} -hBOOL(hAPP_ty_bool(wTrt_1(A,B,C,D),E))|hBOOL(hAPP_ty_bool(wTrt(A,B,C,D),E)).
% 0.86/1.07 Following clause subsumed by 1565 during input processing: 0 [] {-} -hBOOL(hAPP_ty_bool(wTrt(A,B,C,D),E))|hBOOL(hAPP_ty_bool(wTrt_1(A,B,C,D),E)).
% 0.86/1.07 Following clause subsumed by 1621 during input processing: 0 [] {-} -hBOOL(wTrts(A,B,C,D,E))|hBOOL(wTrts_1(A,B,C,D,E)).
% 0.86/1.07 Following clause subsumed by 1622 during input processing: 0 [] {-} -hBOOL(wTrts_1(A,B,C,D,E))|hBOOL(wTrts(A,B,C,D,E)).
% 0.86/1.07 Following clause subsumed by 1628 during input processing: 0 [] {-} -is_bool(A)|A=fTrue|A=fFalse.
% 0.86/1.07 Following clause subsumed by 19 during input processing: 0 [copy,18,flip.1] {-} fAss_list_char(A,B,C,D)!=fAcc_list_char(E,F,G).
% 0.86/1.07 Following clause subsumed by 18 during input processing: 0 [copy,19,flip.1] {-} fAcc_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.86/1.07 Following clause subsumed by 495 during input processing: 0 [copy,494,flip.1] {-} throw_list_char(A)!=hAPP_v834067052t_char(val_list_char,B).
% 0.86/1.07 Following clause subsumed by 494 during input processing: 0 [copy,495,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=throw_list_char(B).
% 0.86/1.07 Following clause subsumed by 501 during input processing: 0 [copy,496,flip.1] {-} while_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.86/1.07 Following clause subsumed by 500 during input processing: 0 [copy,497,flip.1] {-} while_list_char(A,B)!=throw_list_char(C).
% 0.86/1.07 Following clause subsumed by 576 during input processing: 0 [copy,498,flip.1] {-} cond_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.86/1.07 Following clause subsumed by 575 during input processing: 0 [copy,499,flip.1] {-} cond_list_char(A,B,C)!=throw_list_char(D).
% 0.86/1.07 Following clause subsumed by 497 during input processing: 0 [copy,500,flip.1] {-} throw_list_char(A)!=while_list_char(B,C).
% 0.86/1.07 Following clause subsumed by 496 during input processing: 0 [copy,501,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=while_list_char(B,C).
% 0.86/1.07 Following clause subsumed by 577 during input processing: 0 [copy,574,flip.1] {-} cond_list_char(A,B,C)!=while_list_char(D,E).
% 0.86/1.07 Following clause subsumed by 499 during input processing: 0 [copy,575,flip.1] {-} throw_list_char(A)!=cond_list_char(B,C,D).
% 0.86/1.07 Following clause subsumed by 498 during input processing: 0 [copy,576,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=cond_list_char(B,C,D).
% 0.86/1.07 Following clause subsumed by 574 during input processing: 0 [copy,577,flip.1] {-} while_list_char(A,B)!=cond_list_char(C,D,E).
% 0.86/1.07 Following clause subsumed by 703 during input processing: 0 [copy,702,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=fAss_list_char(B,C,D,E).
% 0.86/1.07 Following clause subsumed by 702 during input processing: 0 [copy,703,flip.1] {-} fAss_list_char(A,B,C,D)!=hAPP_v834067052t_char(val_list_char,E).
% 0.86/1.07 Following clause subsumed by 705 during input processing: 0 [copy,704,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=fAcc_list_char(B,C,D).
% 0.86/1.07 Following clause subsumed by 704 during input processing: 0 [copy,705,flip.1] {-} fAcc_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.86/1.07 Following clause subsumed by 707 during input processing: 0 [copy,706,flip.1] {-} throw_list_char(A)!=fAss_list_char(B,C,D,E).
% 0.86/1.07 Following clause subsumed by 706 during input processing: 0 [copy,707,flip.1] {-} fAss_list_char(A,B,C,D)!=throw_list_char(E).
% 0.86/1.07 Following clause subsumed by 709 during input processing: 0 [copy,708,flip.1] {-} throw_list_char(A)!=fAcc_list_char(B,C,D).
% 0.86/1.07 Following clause subsumed by 708 during input processing: 0 [copy,709,flip.1] {-} fAcc_list_char(A,B,C)!=throw_list_char(D).
% 0.86/1.07 Following clause subsumed by 712 during input processing: 0 [copy,710,flip.1] {-} cond_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.86/1.07 Following clause subsumed by 713 during input processing: 0 [copy,711,flip.1] {-} while_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.86/1.07 Following clause subsumed by 710 during input processing: 0 [copy,712,flip.1] {-} fAss_list_char(A,B,C,D)!=cond_list_char(E,F,G).
% 0.86/1.07 Following clause subsumed by 711 during input processing: 0 [copy,713,flip.1] {-} fAss_list_char(A,B,C,D)!=while_list_char(E,F).
% 0.86/1.07 Following clause subsumed by 715 during input processing: 0 [copy,714,flip.1] {-} cond_list_char(A,B,C)!=fAcc_list_char(D,E,F).
% 0.86/1.07 Following clause subsumed by 714 during input processing: 0 [copy,715,flip.1] {-} fAcc_list_char(A,B,C)!=cond_list_char(D,E,F).
% 0.86/1.07 Following clause subsumed by 717 during input processing: 0 [copy,716,flip.1] {-} while_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.86/1.07 Following clause subsumed by 716 during input processing: 0 [copy,717,flip.1] {-} fAcc_list_char(A,B,C)!=while_list_char(D,E).
% 0.86/1.07 Following clause subsumed by 1077 during input processing: 0 [copy,1076,flip.1] {-} cast_list_char(A,B)!=seq_list_char(C,D).
% 0.86/1.07 Following clause subsumed by 1076 during input processing: 0 [copy,1077,flip.1] {-} seq_list_char(A,B)!=cast_list_char(C,D).
% 0.86/1.07 Following clause subsumed by 1082 during input processing: 0 [copy,1078,flip.1] {-} binOp_list_char(A,B,C)!=seq_list_char(D,E).
% 0.86/1.07 Following clause subsumed by 1083 during input processing: 0 [copy,1079,flip.1] {-} binOp_list_char(A,B,C)!=cast_list_char(D,E).
% 0.86/1.07 Following clause subsumed by 1085 during input processing: 0 [copy,1080,flip.1] {-} tryCatch_list_char(A,B,C,D)!=seq_list_char(E,F).
% 0.86/1.07 Following clause subsumed by 1086 during input processing: 0 [copy,1081,flip.1] {-} tryCatch_list_char(A,B,C,D)!=cast_list_char(E,F).
% 0.86/1.07 Following clause subsumed by 1078 during input processing: 0 [copy,1082,flip.1] {-} seq_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.86/1.08 Following clause subsumed by 1079 during input processing: 0 [copy,1083,flip.1] {-} cast_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.86/1.08 Following clause subsumed by 1087 during input processing: 0 [copy,1084,flip.1] {-} tryCatch_list_char(A,B,C,D)!=binOp_list_char(E,F,G).
% 0.86/1.08 Following clause subsumed by 1080 during input processing: 0 [copy,1085,flip.1] {-} seq_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.86/1.08 Following clause subsumed by 1081 during input processing: 0 [copy,1086,flip.1] {-} cast_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.86/1.08 Following clause subsumed by 1084 during input processing: 0 [copy,1087,flip.1] {-} binOp_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.86/1.08 Following clause subsumed by 1107 during input processing: 0 [copy,1103,flip.1] {-} seq_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.86/1.08 Following clause subsumed by 1108 during input processing: 0 [copy,1104,flip.1] {-} cast_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.86/1.08 Following clause subsumed by 1109 during input processing: 0 [copy,1105,flip.1] {-} binOp_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.86/1.08 Following clause subsumed by 1110 during input processing: 0 [copy,1106,flip.1] {-} tryCatch_list_char(A,B,C,D)!=hAPP_v834067052t_char(val_list_char,E).
% 0.86/1.08 Following clause subsumed by 1103 during input processing: 0 [copy,1107,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=seq_list_char(B,C).
% 0.86/1.08 Following clause subsumed by 1104 during input processing: 0 [copy,1108,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=cast_list_char(B,C).
% 0.86/1.08 Following clause subsumed by 1105 during input processing: 0 [copy,1109,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=binOp_list_char(B,C,D).
% 0.86/1.08 Following clause subsumed by 1106 during input processing: 0 [copy,1110,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=tryCatch_list_char(B,C,D,E).
% 0.86/1.08 Following clause subsumed by 1115 during input processing: 0 [copy,1111,flip.1] {-} seq_list_char(A,B)!=throw_list_char(C).
% 0.86/1.08 Following clause subsumed by 1116 during input processing: 0 [copy,1112,flip.1] {-} cast_list_char(A,B)!=throw_list_char(C).
% 0.86/1.08 Following clause subsumed by 1117 during input processing: 0 [copy,1113,flip.1] {-} binOp_list_char(A,B,C)!=throw_list_char(D).
% 0.86/1.08 Following clause subsumed by 1118 during input processing: 0 [copy,1114,flip.1] {-} tryCatch_list_char(A,B,C,D)!=throw_list_char(E).
% 0.86/1.08 Following clause subsumed by 1111 during input processing: 0 [copy,1115,flip.1] {-} throw_list_char(A)!=seq_list_char(B,C).
% 0.86/1.08 Following clause subsumed by 1112 during input processing: 0 [copy,1116,flip.1] {-} throw_list_char(A)!=cast_list_char(B,C).
% 0.86/1.08 Following clause subsumed by 1113 during input processing: 0 [copy,1117,flip.1] {-} throw_list_char(A)!=binOp_list_char(B,C,D).
% 0.86/1.08 Following clause subsumed by 1114 during input processing: 0 [copy,1118,flip.1] {-} throw_list_char(A)!=tryCatch_list_char(B,C,D,E).
% 0.86/1.08 Following clause subsumed by 1120 during input processing: 0 [copy,1119,flip.1] {-} fAss_list_char(A,B,C,D)!=tryCatch_list_char(E,F,G,H).
% 0.86/1.08 Following clause subsumed by 1119 during input processing: 0 [copy,1120,flip.1] {-} tryCatch_list_char(A,B,C,D)!=fAss_list_char(E,F,G,H).
% 0.86/1.08 Following clause subsumed by 1124 during input processing: 0 [copy,1121,flip.1] {-} binOp_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.86/1.08 Following clause subsumed by 1125 during input processing: 0 [copy,1122,flip.1] {-} cast_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.86/1.08 Following clause subsumed by 1126 during input processing: 0 [copy,1123,flip.1] {-} seq_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.86/1.08 Following clause subsumed by 1121 during input processing: 0 [copy,1124,flip.1] {-} fAss_list_char(A,B,C,D)!=binOp_list_char(E,F,G).
% 0.86/1.08 Following clause subsumed by 1122 during input processing: 0 [copy,1125,flip.1] {-} fAss_list_char(A,B,C,D)!=cast_list_char(E,F).
% 0.86/1.08 Following clause subsumed by 1123 during input processing: 0 [copy,1126,flip.1] {-} fAss_list_char(A,B,C,D)!=seq_list_char(E,F).
% 0.86/1.08 Following clause subsumed by 1129 during input processing: 0 [copy,1127,flip.1] {-} cond_list_char(A,B,C)!=seq_list_char(D,E).
% 0.86/1.10 Following clause subsumed by 1130 during input processing: 0 [copy,1128,flip.1] {-} cond_list_char(A,B,C)!=cast_list_char(D,E).
% 0.86/1.10 Following clause subsumed by 1127 during input processing: 0 [copy,1129,flip.1] {-} seq_list_char(A,B)!=cond_list_char(C,D,E).
% 0.86/1.10 Following clause subsumed by 1128 during input processing: 0 [copy,1130,flip.1] {-} cast_list_char(A,B)!=cond_list_char(C,D,E).
% 0.86/1.10 Following clause subsumed by 1132 during input processing: 0 [copy,1131,flip.1] {-} binOp_list_char(A,B,C)!=cond_list_char(D,E,F).
% 0.86/1.10 Following clause subsumed by 1131 during input processing: 0 [copy,1132,flip.1] {-} cond_list_char(A,B,C)!=binOp_list_char(D,E,F).
% 0.86/1.10 Following clause subsumed by 1134 during input processing: 0 [copy,1133,flip.1] {-} tryCatch_list_char(A,B,C,D)!=cond_list_char(E,F,G).
% 0.86/1.10 Following clause subsumed by 1133 during input processing: 0 [copy,1134,flip.1] {-} cond_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.86/1.10 Following clause subsumed by 1136 during input processing: 0 [copy,1135,flip.1] {-} fAcc_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.86/1.10 Following clause subsumed by 1135 during input processing: 0 [copy,1136,flip.1] {-} tryCatch_list_char(A,B,C,D)!=fAcc_list_char(E,F,G).
% 0.86/1.10 Following clause subsumed by 1138 during input processing: 0 [copy,1137,flip.1] {-} fAcc_list_char(A,B,C)!=binOp_list_char(D,E,F).
% 0.86/1.10 Following clause subsumed by 1137 during input processing: 0 [copy,1138,flip.1] {-} binOp_list_char(A,B,C)!=fAcc_list_char(D,E,F).
% 0.86/1.10 Following clause subsumed by 1141 during input processing: 0 [copy,1139,flip.1] {-} cast_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.86/1.10 Following clause subsumed by 1142 during input processing: 0 [copy,1140,flip.1] {-} seq_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.86/1.10 Following clause subsumed by 1139 during input processing: 0 [copy,1141,flip.1] {-} fAcc_list_char(A,B,C)!=cast_list_char(D,E).
% 0.86/1.10 Following clause subsumed by 1140 during input processing: 0 [copy,1142,flip.1] {-} fAcc_list_char(A,B,C)!=seq_list_char(D,E).
% 0.86/1.10 Following clause subsumed by 1145 during input processing: 0 [copy,1143,flip.1] {-} while_list_char(A,B)!=seq_list_char(C,D).
% 0.86/1.10 Following clause subsumed by 1146 during input processing: 0 [copy,1144,flip.1] {-} while_list_char(A,B)!=cast_list_char(C,D).
% 0.86/1.10 Following clause subsumed by 1143 during input processing: 0 [copy,1145,flip.1] {-} seq_list_char(A,B)!=while_list_char(C,D).
% 0.86/1.10 Following clause subsumed by 1144 during input processing: 0 [copy,1146,flip.1] {-} cast_list_char(A,B)!=while_list_char(C,D).
% 0.86/1.10 Following clause subsumed by 1149 during input processing: 0 [copy,1147,flip.1] {-} binOp_list_char(A,B,C)!=while_list_char(D,E).
% 0.86/1.10 Following clause subsumed by 1150 during input processing: 0 [copy,1148,flip.1] {-} tryCatch_list_char(A,B,C,D)!=while_list_char(E,F).
% 0.86/1.10 Following clause subsumed by 1147 during input processing: 0 [copy,1149,flip.1] {-} while_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.86/1.10 Following clause subsumed by 1148 during input processing: 0 [copy,1150,flip.1] {-} while_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.86/1.10 1292 back subsumes 1285.
% 0.86/1.10 Following clause subsumed by 1346 during input processing: 0 [copy,1345,flip.1] {-} bool(A)!=addr(B).
% 0.86/1.10 Following clause subsumed by 1345 during input processing: 0 [copy,1346,flip.1] {-} addr(A)!=bool(B).
% 0.86/1.10 1402 back subsumes 1397.
% 0.86/1.10
% 0.86/1.10 ------------> process sos:
% 0.86/1.10 Following clause subsumed by 1918 during input processing: 0 [] {-} hBOOL(hAPP_ty_bool(wTrt(p,ha,e,fAss_list_char(ea,f,d,e_2)),t)).
% 0.86/1.10 Following clause subsumed by 1917 during input processing: 0 [] {-} hBOOL(hAPP_P159683425l_bool(typeSa1700205512_sconf(p,e),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),la))).
% 0.86/1.10 Following clause subsumed by 2319 during input processing: 0 [demod,2375] {-} hAPP_P1228500987ion_ty(hAPP_f46308763ion_ty(produc1577326610ion_ty,A),hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,B),C))=hAPP_f652398900ion_ty(hAPP_l2000496933ion_ty(A,B),C).
% 0.94/1.14 Following clause subsumed by 2385 during input processing: 0 [demod,2318,2377] {-} hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,A),hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,B),C))=hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,A),hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,B),C)).
% 0.94/1.14 Following clause subsumed by 2319 during input processing: 0 [demod,2375] {-} hAPP_P1228500987ion_ty(hAPP_f46308763ion_ty(produc1577326610ion_ty,A),hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,B),C))=hAPP_f652398900ion_ty(hAPP_l2000496933ion_ty(A,B),C).
% 0.94/1.14 Following clause subsumed by 2677 during input processing: 0 [copy,2385,flip.1] {-} hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,A),hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,B),C))=hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,A),hAPP_t708040077har_ty(hAPP_P827589667har_ty(produc1265154397har_ty,B),C)).
% 0.94/1.14 Following clause subsumed by 2677 during input processing: 0 [copy,2677,flip.1] {-} A=A.
% 0.94/1.14 2677 back subsumes 2385.
% 0.94/1.14 2677 back subsumes 1812.
% 0.94/1.14 2677 back subsumes 1784.
% 0.94/1.14 2677 back subsumes 1755.
% 0.94/1.14 2677 back subsumes 1743.
% 0.94/1.14 2677 back subsumes 1720.
% 0.94/1.14 2677 back subsumes 1719.
% 0.94/1.14 2677 back subsumes 1718.
% 0.94/1.14 2677 back subsumes 1717.
% 0.94/1.14 2677 back subsumes 1716.
% 0.94/1.14 2677 back subsumes 1715.
% 0.94/1.14 2677 back subsumes 1714.
% 0.94/1.14 2677 back subsumes 1713.
% 0.94/1.14 2677 back subsumes 1712.
% 0.94/1.14 2677 back subsumes 1711.
% 0.94/1.14 2677 back subsumes 1710.
% 0.94/1.14 2677 back subsumes 1709.
% 0.94/1.14 2677 back subsumes 1708.
% 0.94/1.14 2677 back subsumes 1707.
% 0.94/1.14 2677 back subsumes 1706.
% 0.94/1.14 2677 back subsumes 1705.
% 0.94/1.14 2677 back subsumes 1704.
% 0.94/1.14 2677 back subsumes 1703.
% 0.94/1.14 2677 back subsumes 1702.
% 0.94/1.14 2677 back subsumes 1701.
% 0.94/1.14 2677 back subsumes 1700.
% 0.94/1.14 2677 back subsumes 1699.
% 0.94/1.14 2677 back subsumes 1698.
% 0.94/1.14 2677 back subsumes 1697.
% 0.94/1.14 2677 back subsumes 1696.
% 0.94/1.14 2677 back subsumes 1695.
% 0.94/1.14 2677 back subsumes 1694.
% 0.94/1.14 2677 back subsumes 1693.
% 0.94/1.14 2677 back subsumes 1692.
% 0.94/1.14 2677 back subsumes 1691.
% 0.94/1.14 2677 back subsumes 1690.
% 0.94/1.14 2677 back subsumes 1689.
% 0.94/1.14 2677 back subsumes 1688.
% 0.94/1.14 2677 back subsumes 1687.
% 0.94/1.14 2677 back subsumes 1686.
% 0.94/1.14 2677 back subsumes 1685.
% 0.94/1.14 2677 back subsumes 1636.
% 0.94/1.14 Following clause subsumed by 2319 during input processing: 0 [copy,2702,flip.1] {-} hAPP_P1228500987ion_ty(hAPP_f46308763ion_ty(produc1577326610ion_ty,A),hAPP_f900686428on_val(hAPP_l1786340417on_val(produc823076510on_val,B),C))=hAPP_f652398900ion_ty(hAPP_l2000496933ion_ty(A,B),C).
% 0.94/1.14 Following clause subsumed by 2379 during input processing: 0 [copy,2771,flip.1] {-} hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,A),hAPP_P71962758har_ty(hAPP_f909647877har_ty(produc1626136111har_ty,B),C))=hAPP_P1057393871ar_val(hAPP_f528845893ar_val(produc2026840771ar_val,hAPP_f1286352408ar_val(hAPP_f922986761ar_val(cOMBB_491542469t_char,hAPP_f1061710805ar_val(cOMBB_239784108val_ty,hAPP_f1295640803ar_val(produc1553344466ar_val,A))),B)),C).
% 0.94/1.14 Following clause subsumed by 2381 during input processing: 0 [copy,2772,flip.1] {-} hAPP_P1409535266har_ty(hAPP_f533118691har_ty(produc1582135574har_ty,A),hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,B),C))=hAPP_P385447595har_ty(hAPP_f513000995har_ty(produc448987860har_ty,hAPP_f1820012432har_ty(hAPP_f1720458941har_ty(cOMBB_424865560t_char,hAPP_f393578581har_ty(cOMBB_1320677736_ty_ty,hAPP_f533118691har_ty(produc1582135574har_ty,A))),B)),C).
% 0.94/1.14 Following clause subsumed by 2383 during input processing: 0 [copy,2773,flip.1] {-} hAPP_P532450504ar_val(hAPP_f65736581ar_val(produc615345852ar_val,A),hAPP_P385447595har_ty(hAPP_f513000995har_ty(produc448987860har_ty,B),C))=hAPP_P841862366ar_val(hAPP_f1295640803ar_val(produc1553344466ar_val,hAPP_f1582750480ar_val(hAPP_f1761801623ar_val(cOMBB_510504510t_char,hAPP_f1675912277ar_val(cOMBB_351318850val_ty,hAPP_f65736581ar_val(produc615345852ar_val,A))),B)),C).
% 0.94/1.14 Following clause subsumed by 2570 during input processing: 0 [copy,2787,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1935223905l_bool(hAPP_f1589017327l_bool(cOMBB_558176806on_val,A),B),C)=hAPP_P929938951l_bool(A,hAPP_f1181212006al_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2571 during input processing: 0 [copy,2788,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1189972950l_bool(hAPP_f86617653l_bool(cOMBB_165135181on_val,A),B),C)=hAPP_P748443392y_bool(A,hAPP_f1746527929har_ty(B,C)).
% 0.94/1.14 Following clause subsumed by 2574 during input processing: 0 [copy,2789,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f2061154754l_bool(hAPP_f1777594159l_bool(cOMBB_448128005on_val,A),B),C)=hAPP_P943837928l_bool(A,hAPP_f384373191al_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2575 during input processing: 0 [copy,2790,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f603925568l_bool(hAPP_f181262431l_bool(cOMBC_832625297y_bool,A),B),C)=hAPP_f1001225811y_bool(hAPP_f2060496320y_bool(A,C),B).
% 0.94/1.14 Following clause subsumed by 2576 during input processing: 0 [copy,2791,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1326058377l_bool(hAPP_f1804599279l_bool(cOMBB_678146046on_val,A),B),C)=hAPP_P449474095r_bool(A,hAPP_f338074126t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2577 during input processing: 0 [copy,2792,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1468279871l_bool(hAPP_f737797743l_bool(cOMBB_1733006024on_val,A),B),C)=hAPP_P2118621157r_bool(A,hAPP_f1555843780t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2578 during input processing: 0 [copy,2793,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1787894864l_bool(hAPP_f975490601l_bool(cOMBB_844549459on_val,A),B),C)=hAPP_P1070896250l_bool(A,hAPP_f901144627ar_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2581 during input processing: 0 [copy,2794,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1390791157l_bool(hAPP_f99607667l_bool(cOMBB_1334418926on_val,A),B),C)=hAPP_P2014166431r_bool(A,hAPP_f1953285592t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2586 during input processing: 0 [copy,2795,flip.1] {-} hAPP_t931865635har_ty(hAPP_f1734435490har_ty(hAPP_f393578581har_ty(cOMBB_1320677736_ty_ty,A),B),C)=hAPP_P1409535266har_ty(A,hAPP_t97533526ar_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2587 during input processing: 0 [copy,2796,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1645102644l_bool(hAPP_f962366127l_bool(cOMBB_95569939on_val,A),B),C)=hAPP_P1907982426r_bool(A,hAPP_f1911830329t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2597 during input processing: 0 [copy,2797,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1937467848l_bool(hAPP_f2020099865l_bool(cOMBB_1543649755on_val,A),B),C)=hAPP_P1235399154l_bool(A,hAPP_f2106552235on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2598 during input processing: 0 [copy,2798,flip.1] {-} hAPP_f1145256474l_bool(hAPP_f1452292669l_bool(hAPP_f1977633121l_bool(cOMBB_1303934920on_val,A),B),C)=hAPP_b589554111l_bool(A,hAPP_f61040418l_bool(B,C)).
% 0.94/1.14 Following clause subsumed by 2599 during input processing: 0 [copy,2799,flip.1] {-} hAPP_l1836284219ar_val(hAPP_f1286352408ar_val(hAPP_f922986761ar_val(cOMBB_491542469t_char,A),B),C)=hAPP_f151191262ar_val(A,hAPP_l826728946har_ty(B,C)).
% 0.94/1.14 Following clause subsumed by 2600 during input processing: 0 [copy,2800,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1212990632l_bool(hAPP_f764883801l_bool(cOMBB_1837440507on_val,A),B),C)=hAPP_P92196306r_bool(A,hAPP_f848628235t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2601 during input processing: 0 [copy,2801,flip.1] {-} hAPP_f652398900ion_ty(hAPP_f2110071953ion_ty(hAPP_f69964139ion_ty(cOMBB_2041093409on_val,A),B),C)=hAPP_P1228500987ion_ty(A,hAPP_f900686428on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2605 during input processing: 0 [copy,2802,flip.1] {-} hAPP_P221287148ar_val(hAPP_f2096521338ar_val(hAPP_f1210767211ar_val(cOMBB_1905001812t_char,A),B),C)=hAPP_f151191262ar_val(A,hAPP_P827589667har_ty(B,C)).
% 0.94/1.14 Following clause subsumed by 2606 during input processing: 0 [copy,2803,flip.1] {-} hAPP_P901867449har_ty(hAPP_f1820012432har_ty(hAPP_f1720458941har_ty(cOMBB_424865560t_char,A),B),C)=hAPP_f1734435490har_ty(A,hAPP_P221287148ar_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2611 during input processing: 0 [copy,2804,flip.1] {-} hAPP_P289594851ar_val(hAPP_f1240485169ar_val(hAPP_f332422699ar_val(cOMBB_388225803t_char,A),B),C)=hAPP_f1951920661ar_val(A,hAPP_P1321848547ar_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2612 during input processing: 0 [copy,2805,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f550652027l_bool(hAPP_f838396643l_bool(cOMBC_2027949654l_bool,A),B),C)=hAPP_f603925568l_bool(hAPP_f1617787571l_bool(A,C),B).
% 0.94/1.14 Following clause subsumed by 2613 during input processing: 0 [copy,2806,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1008932791l_bool(hAPP_f2057883639l_bool(cOMBB_1750801836on_val,A),B),C)=hAPP_P159683425l_bool(A,hAPP_f1727192346on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2614 during input processing: 0 [copy,2807,flip.1] {-} hAPP_P2118621157r_bool(hAPP_f1915623807r_bool(hAPP_f1346522053r_bool(cOMBB_1115744685t_char,A),B),C)=hAPP_P159683425l_bool(A,hAPP_P214139537on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2615 during input processing: 0 [copy,2808,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1474698986l_bool(hAPP_f1809473245l_bool(cOMBB_1452070457on_val,A),B),C)=hAPP_P828904212r_bool(A,hAPP_f268764237t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2618 during input processing: 0 [copy,2809,flip.1] {-} hAPP_f1175813647l_bool(cOMBS_570216337l_bool(A,B),C)=hAPP_f1074020887l_bool(hAPP_f1492320500l_bool(A,C),hAPP_f1175813647l_bool(B,C)).
% 0.94/1.14 Following clause subsumed by 2625 during input processing: 0 [copy,2810,flip.1] {-} hAPP_P1907982426r_bool(hAPP_f1957179113r_bool(hAPP_f1096084527r_bool(cOMBB_1980206754t_char,A),B),C)=hAPP_P159683425l_bool(A,hAPP_P216502748on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2626 during input processing: 0 [copy,2811,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f318082871l_bool(hAPP_f1233687287l_bool(cOMBB_171276332on_val,A),B),C)=hAPP_P1708370145l_bool(A,hAPP_f1926378906on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2627 during input processing: 0 [copy,2812,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f679593521l_bool(hAPP_f2114578667l_bool(cOMBB_914590898on_val,A),B),C)=hAPP_P659547099r_bool(A,hAPP_f596349460t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2628 during input processing: 0 [copy,2813,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1617838686l_bool(hAPP_f1740025881l_bool(cOMBB_1511810527on_val,A),B),C)=hAPP_f1189972950l_bool(A,hAPP_f993605148har_ty(B,C)).
% 0.94/1.14 Following clause subsumed by 2629 during input processing: 0 [copy,2814,flip.1] {-} hAPP_f1492320500l_bool(hAPP_f1523875321l_bool(hAPP_f592397849l_bool(cOMBB_1718333400on_val,A),B),C)=hAPP_f1863694447l_bool(A,hAPP_f1145256474l_bool(B,C)).
% 0.94/1.14 Following clause subsumed by 2630 during input processing: 0 [copy,2815,flip.1] {-} hAPP_l1062423959r_bool(hAPP_f1339377933r_bool(hAPP_f1165187701r_bool(cOMBB_1124198201st_val,A),B),C)=hAPP_f716957699r_bool(A,hAPP_l1870161525on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2631 during input processing: 0 [copy,2816,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f828778154l_bool(hAPP_f1572306499l_bool(cOMBB_1210977579on_val,A),B),C)=hAPP_f2061154754l_bool(A,hAPP_f1779904442al_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2632 during input processing: 0 [copy,2817,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f502623122l_bool(hAPP_f1000925999l_bool(cOMBB_1466435125on_val,A),B),C)=hAPP_P71593144l_bool(A,hAPP_f637291415on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2633 during input processing: 0 [copy,2818,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1996106275l_bool(hAPP_f1550515381l_bool(cOMBB_2040779506on_val,A),B),C)=hAPP_f1326058377l_bool(A,hAPP_f1628326017t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2634 during input processing: 0 [copy,2819,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1576637933l_bool(hAPP_f154583625l_bool(cOMBB_335252392on_val,A),B),C)=hAPP_f1468279871l_bool(A,hAPP_f1297079863t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2639 during input processing: 0 [copy,2820,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1812276580l_bool(hAPP_f1292837529l_bool(cOMBB_238112345on_val,A),B),C)=hAPP_f1787894864l_bool(A,hAPP_f1925626518ar_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2648 during input processing: 0 [copy,2821,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1145600492l_bool(hAPP_f630712985l_bool(cOMBB_1962662865on_val,A),B),C)=hAPP_f1937467848l_bool(A,hAPP_f1614126606on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2649 during input processing: 0 [copy,2822,flip.1] {-} hAPP_f1617787571l_bool(hAPP_f857351829l_bool(hAPP_f348318673l_bool(cOMBB_1518282696on_val,A),B),C)=hAPP_f181262431l_bool(A,hAPP_f1213370163y_bool(B,C)).
% 0.94/1.14 Following clause subsumed by 2650 during input processing: 0 [copy,2823,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1089411340l_bool(hAPP_f2012169497l_bool(cOMBB_1443356337on_val,A),B),C)=hAPP_f1212990632l_bool(A,hAPP_f78832750t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2651 during input processing: 0 [copy,2824,flip.1] {-} hAPP_P159683425l_bool(hAPP_f1301559543l_bool(hAPP_f1825030711l_bool(cOMBB_877741809on_val,A),B),C)=hAPP_P159683425l_bool(A,hAPP_P1776198677on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2652 during input processing: 0 [copy,2825,flip.1] {-} hAPP_l217977712r_bool(hAPP_f829041291r_bool(hAPP_f1691034591r_bool(cOMBB_889837233t_char,A),B),C)=hAPP_f1957179113r_bool(A,hAPP_l451552092on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2653 during input processing: 0 [copy,2826,flip.1] {-} hAPP_P1708370145l_bool(hAPP_f1712766199l_bool(hAPP_f881985847l_bool(cOMBB_1083177073on_val,A),B),C)=hAPP_P159683425l_bool(A,hAPP_P789556885on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2656 during input processing: 0 [copy,2827,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1363667773l_bool(hAPP_f1050935001l_bool(cOMBB_1153617344on_val,A),B),C)=hAPP_f1008932791l_bool(A,hAPP_f1849790461on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2657 during input processing: 0 [copy,2828,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f337607754l_bool(hAPP_f1546157465l_bool(cOMBB_955482355on_val,A),B),C)=hAPP_f1474698986l_bool(A,hAPP_f371326384t_char(B,C)).
% 0.94/1.14 Following clause subsumed by 2658 during input processing: 0 [copy,2829,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f850751421l_bool(hAPP_f399538905l_bool(cOMBB_1466889536on_val,A),B),C)=hAPP_f318082871l_bool(A,hAPP_f1840640125on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2662 during input processing: 0 [copy,2830,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f556306650l_bool(hAPP_f1538372259l_bool(cOMBB_157777659on_val,A),B),C)=hAPP_f502623122l_bool(A,hAPP_f336970122on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2666 during input processing: 0 [copy,2831,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f524589473l_bool(hAPP_f2052660463l_bool(cOMBB_1292453606on_val,A),B),C)=hAPP_P282169671l_bool(A,hAPP_f602593190on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2667 during input processing: 0 [copy,2832,flip.1] {-} hAPP_f1033709212l_bool(hAPP_f1546656185l_bool(hAPP_f28987375l_bool(cOMBB_132741582on_val,A),B),C)=hAPP_P1333315679l_bool(A,hAPP_f1416324670on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2668 during input processing: 0 [copy,2833,flip.1] {-} hAPP_e1833980889l_bool(hAPP_f653692369l_bool(hAPP_f516738477l_bool(cOMBB_819439237t_char,A),B),C)=hAPP_f1301559543l_bool(A,hAPP_e108155315on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2671 during input processing: 0 [copy,2834,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f927043595l_bool(hAPP_f1043869573l_bool(cOMBB_1259202826on_val,A),B),C)=hAPP_f524589473l_bool(A,hAPP_f600512025on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2672 during input processing: 0 [copy,2835,flip.1] {-} hAPP_f1175813647l_bool(hAPP_f1505175539l_bool(hAPP_f924423253l_bool(cOMBB_1330725154on_val,A),B),C)=hAPP_f1546656185l_bool(A,hAPP_f865889457on_val(B,C)).
% 0.94/1.14 Following clause subsumed by 2676 during input processing: 0 [copy,2836,flip.1] {-} hAPP_P1183008383l_bool(hAPP_f1909521165l_bool(hAPP_f1779944471l_bool(cOMBB_607314500on_val,A),B),C)=hAPP_f1540354981l_bool(A,hAPP_P308812685on_val(B,C)).
% 0.94/1.14
% 0.94/1.14 ======= end of input processing =======
% 0.94/1.15
% 0.94/1.15 SEGMENTATION FAULT!! This is probably caused by a
% 0.94/1.15 bug in Otter. Please send copy of the input file to
% 0.94/1.15 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.94/1.15 using, and send any other info that might be useful.
% 0.94/1.15
% 0.94/1.15
% 0.94/1.15 SEGMENTATION FAULT!! This is probably caused by a
% 0.94/1.15 bug in Otter. Please send copy of the input file to
% 0.94/1.15 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.94/1.15 using, and send any other info that might be useful.
% 0.94/1.15
% 0.94/1.15
% 0.94/1.15 The job finished Sun Jun 5 17:38:09 2022
%------------------------------------------------------------------------------