%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SWW475+3 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n026.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:01 EDT 2022
% Result : Unknown 0.84s 1.02s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : SWW475+3 : TPTP v8.1.0. Released v5.3.0.
% 0.12/0.14 % Command : sos-script %s
% 0.14/0.35 % Computer : n026.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Sun Jun 5 04:17:14 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.70/0.88 ----- Otter 3.2, August 2001 -----
% 0.70/0.88 The process was started by sandbox on n026.cluster.edu,
% 0.70/0.88 Sun Jun 5 04:17:14 2022
% 0.70/0.88 The command was "./sos". The process ID is 5254.
% 0.70/0.88
% 0.70/0.88 set(prolog_style_variables).
% 0.70/0.88 set(auto).
% 0.70/0.88 dependent: set(auto1).
% 0.70/0.88 dependent: set(process_input).
% 0.70/0.88 dependent: clear(print_kept).
% 0.70/0.88 dependent: clear(print_new_demod).
% 0.70/0.88 dependent: clear(print_back_demod).
% 0.70/0.88 dependent: clear(print_back_sub).
% 0.70/0.88 dependent: set(control_memory).
% 0.70/0.88 dependent: assign(max_mem, 12000).
% 0.70/0.88 dependent: assign(pick_given_ratio, 4).
% 0.70/0.88 dependent: assign(stats_level, 1).
% 0.70/0.88 dependent: assign(pick_semantic_ratio, 3).
% 0.70/0.88 dependent: assign(sos_limit, 5000).
% 0.70/0.88 dependent: assign(max_weight, 60).
% 0.70/0.88 clear(print_given).
% 0.70/0.88
% 0.70/0.88 formula_list(usable).
% 0.70/0.88
% 0.70/0.88 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=10.
% 0.70/0.88
% 0.70/0.88 This ia a non-Horn set with equality. The strategy will be
% 0.70/0.88 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.70/0.88 unit deletion, with positive clauses in sos and nonpositive
% 0.70/0.88 clauses in usable.
% 0.70/0.88
% 0.70/0.88 dependent: set(knuth_bendix).
% 0.70/0.88 dependent: set(para_from).
% 0.70/0.88 dependent: set(para_into).
% 0.70/0.88 dependent: clear(para_from_right).
% 0.70/0.88 dependent: clear(para_into_right).
% 0.70/0.88 dependent: set(para_from_vars).
% 0.70/0.88 dependent: set(eq_units_both_ways).
% 0.70/0.88 dependent: set(dynamic_demod_all).
% 0.70/0.88 dependent: set(dynamic_demod).
% 0.70/0.88 dependent: set(order_eq).
% 0.70/0.88 dependent: set(back_demod).
% 0.70/0.88 dependent: set(lrpo).
% 0.70/0.88 dependent: set(hyper_res).
% 0.70/0.88 dependent: set(unit_deletion).
% 0.70/0.88 dependent: set(factor).
% 0.70/0.88
% 0.70/0.88 ------------> process usable:
% 0.70/0.88 Following clause subsumed by 86 during input processing: 0 [] {-} produc1002914035har_ty(A,B)!=produc1002914035har_ty(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 87 during input processing: 0 [] {-} produc1002914035har_ty(A,B)!=produc1002914035har_ty(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 89 during input processing: 0 [] {-} produc1265154397har_ty(A,B)!=produc1265154397har_ty(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 90 during input processing: 0 [] {-} produc1265154397har_ty(A,B)!=produc1265154397har_ty(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 92 during input processing: 0 [] {-} produc251930284har_ty(A,B)!=produc251930284har_ty(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 93 during input processing: 0 [] {-} produc251930284har_ty(A,B)!=produc251930284har_ty(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 95 during input processing: 0 [] {-} produc1897818327t_char(A,B)!=produc1897818327t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 96 during input processing: 0 [] {-} produc1897818327t_char(A,B)!=produc1897818327t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 98 during input processing: 0 [] {-} produc2080520419t_char(A,B)!=produc2080520419t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 99 during input processing: 0 [] {-} produc2080520419t_char(A,B)!=produc2080520419t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 101 during input processing: 0 [] {-} produc499151895on_val(A,B)!=produc499151895on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 102 during input processing: 0 [] {-} produc499151895on_val(A,B)!=produc499151895on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 104 during input processing: 0 [] {-} produc1244920211al_val(A,B)!=produc1244920211al_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 105 during input processing: 0 [] {-} produc1244920211al_val(A,B)!=produc1244920211al_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 107 during input processing: 0 [] {-} produc1924279125al_val(A,B)!=produc1924279125al_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 108 during input processing: 0 [] {-} produc1924279125al_val(A,B)!=produc1924279125al_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 110 during input processing: 0 [] {-} produc1299387215t_char(A,B)!=produc1299387215t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 111 during input processing: 0 [] {-} produc1299387215t_char(A,B)!=produc1299387215t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 113 during input processing: 0 [] {-} produc57279289t_char(A,B)!=produc57279289t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 114 during input processing: 0 [] {-} produc57279289t_char(A,B)!=produc57279289t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 116 during input processing: 0 [] {-} produc24551831t_char(A,B)!=produc24551831t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 117 during input processing: 0 [] {-} produc24551831t_char(A,B)!=produc24551831t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 119 during input processing: 0 [] {-} produc1951691075on_val(A,B)!=produc1951691075on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 120 during input processing: 0 [] {-} produc1951691075on_val(A,B)!=produc1951691075on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 122 during input processing: 0 [] {-} produc870913623on_val(A,B)!=produc870913623on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 123 during input processing: 0 [] {-} produc870913623on_val(A,B)!=produc870913623on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 125 during input processing: 0 [] {-} produc1564932627on_val(A,B)!=produc1564932627on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 126 during input processing: 0 [] {-} produc1564932627on_val(A,B)!=produc1564932627on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 128 during input processing: 0 [] {-} produc1441475159on_val(A,B)!=produc1441475159on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 129 during input processing: 0 [] {-} produc1441475159on_val(A,B)!=produc1441475159on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 131 during input processing: 0 [] {-} produc1259058957on_val(A,B)!=produc1259058957on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 132 during input processing: 0 [] {-} produc1259058957on_val(A,B)!=produc1259058957on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 134 during input processing: 0 [] {-} produc899768717on_val(A,B)!=produc899768717on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 135 during input processing: 0 [] {-} produc899768717on_val(A,B)!=produc899768717on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 137 during input processing: 0 [] {-} produc1611380469on_val(A,B)!=produc1611380469on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 138 during input processing: 0 [] {-} produc1611380469on_val(A,B)!=produc1611380469on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 140 during input processing: 0 [] {-} produc379668296on_val(A,B)!=produc379668296on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 141 during input processing: 0 [] {-} produc379668296on_val(A,B)!=produc379668296on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 143 during input processing: 0 [] {-} produc921874948t_char(A,B)!=produc921874948t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 144 during input processing: 0 [] {-} produc921874948t_char(A,B)!=produc921874948t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 146 during input processing: 0 [] {-} produc1909267824t_char(A,B)!=produc1909267824t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 147 during input processing: 0 [] {-} produc1909267824t_char(A,B)!=produc1909267824t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 149 during input processing: 0 [] {-} produc1916172923t_char(A,B)!=produc1916172923t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 150 during input processing: 0 [] {-} produc1916172923t_char(A,B)!=produc1916172923t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 152 during input processing: 0 [] {-} -is_bop(A)| -is_bop(B)|produc621191550al_val(A,C)!=produc621191550al_val(B,D)|A=B.
% 0.70/0.88 Following clause subsumed by 153 during input processing: 0 [] {-} -is_bop(A)| -is_bop(B)|produc621191550al_val(A,C)!=produc621191550al_val(B,D)|C=D.
% 0.70/0.88 Following clause subsumed by 155 during input processing: 0 [] {-} product_Pair_val_val(A,B)!=product_Pair_val_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 156 during input processing: 0 [] {-} product_Pair_val_val(A,B)!=product_Pair_val_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 158 during input processing: 0 [] {-} produc823076510on_val(A,B)!=produc823076510on_val(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 159 during input processing: 0 [] {-} produc823076510on_val(A,B)!=produc823076510on_val(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 161 during input processing: 0 [] {-} produc5062597t_char(A,B)!=produc5062597t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 162 during input processing: 0 [] {-} produc5062597t_char(A,B)!=produc5062597t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 164 during input processing: 0 [] {-} produc1147572817t_char(A,B)!=produc1147572817t_char(C,D)|A=C.
% 0.70/0.88 Following clause subsumed by 165 during input processing: 0 [] {-} produc1147572817t_char(A,B)!=produc1147572817t_char(C,D)|B=D.
% 0.70/0.88 Following clause subsumed by 254 during input processing: 0 [] {-} -hBOOL(hAPP_P748443392y_bool(hAPP_l1665608433y_bool(produc166740340y_bool(A),B),C))|hBOOL(hAPP_P831231943y_bool(A,produc1002914035har_ty(B,C))).
% 0.70/0.88 Following clause subsumed by 255 during input processing: 0 [] {-} -hBOOL(hAPP_ty_bool(hAPP_P1845004857y_bool(produc1215659230y_bool(A),B),C))|hBOOL(hAPP_P27757617y_bool(A,produc1265154397har_ty(B,C))).
% 0.70/0.88 Following clause subsumed by 256 during input processing: 0 [] {-} -hBOOL(hAPP_ty_bool(hAPP_l1734756650y_bool(produc2091768109y_bool(A),B),C))|hBOOL(hAPP_P748443392y_bool(A,produc251930284har_ty(B,C))).
% 0.70/0.88 Following clause subsumed by 257 during input processing: 0 [] {-} -hBOOL(hAPP_P2014166431r_bool(hAPP_P1939418767r_bool(produc1295142846r_bool(A),B),C))|hBOOL(hAPP_P1002912327r_bool(A,produc1897818327t_char(B,C))).
% 0.70/0.88 Following clause subsumed by 258 during input processing: 0 [] {-} -hBOOL(hAPP_P449474095r_bool(hAPP_P663876415r_bool(produc715708746r_bool(A),B),C))|hBOOL(hAPP_P2010574925r_bool(A,produc2080520419t_char(B,C))).
% 0.70/0.88 Following clause subsumed by 259 during input processing: 0 [] {-} -hBOOL(hAPP_P1235399154l_bool(hAPP_P416784693l_bool(produc1996970750l_bool(A),B),C))|hBOOL(hAPP_P124632071l_bool(A,produc499151895on_val(B,C))).
% 0.70/0.88 Following clause subsumed by 260 during input processing: 0 [] {-} -hBOOL(hAPP_P929938951l_bool(hAPP_P1815899455l_bool(produc1034940666l_bool(A),B),C))|hBOOL(hAPP_P2123002749l_bool(A,produc1244920211al_val(B,C))).
% 0.70/0.88 Following clause subsumed by 261 during input processing: 0 [] {-} -hBOOL(hAPP_P943837928l_bool(hAPP_P323054207l_bool(produc1969754044l_bool(A),B),C))|hBOOL(hAPP_P738987199l_bool(A,produc1924279125al_val(B,C))).
% 0.70/0.88 Following clause subsumed by 262 during input processing: 0 [] {-} -hBOOL(hAPP_P2118621157r_bool(hAPP_P357098431r_bool(produc1535899062r_bool(A),B),C))|hBOOL(hAPP_P1183499705r_bool(A,produc1299387215t_char(B,C))).
% 0.70/0.88 Following clause subsumed by 263 during input processing: 0 [] {-} -hBOOL(hAPP_P1907982426r_bool(hAPP_P1214880255r_bool(produc1268552608r_bool(A),B),C))|hBOOL(hAPP_P1240100515r_bool(A,produc57279289t_char(B,C))).
% 0.70/0.88 Following clause subsumed by 264 during input processing: 0 [] {-} -hBOOL(hAPP_P92196306r_bool(hAPP_P1928969845r_bool(produc17861502r_bool(A),B),C))|hBOOL(hAPP_P824029447r_bool(A,produc24551831t_char(B,C))).
% 0.70/0.88 Following clause subsumed by 265 during input processing: 0 [] {-} -hBOOL(hAPP_P1333315679l_bool(hAPP_P220718911l_bool(produc971707818l_bool(A),B),C))|hBOOL(hAPP_P2028072621l_bool(A,produc1951691075on_val(B,C))).
% 0.70/0.88 Following clause subsumed by 266 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_P1988153107l_bool(produc1073654846l_bool(A),B),C))|hBOOL(hAPP_P1221872711l_bool(A,produc870913623on_val(B,C))).
% 0.70/0.88 Following clause subsumed by 267 during input processing: 0 [] {-} -hBOOL(hAPP_P282169671l_bool(hAPP_P2062527807l_bool(produc1497005946l_bool(A),B),C))|hBOOL(hAPP_P378063101l_bool(A,produc1564932627on_val(B,C))).
% 0.70/0.88 Following clause subsumed by 268 during input processing: 0 [] {-} -hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(produc1159035454l_bool(A),B),C))|hBOOL(hAPP_P282169671l_bool(A,produc1441475159on_val(B,C))).
% 0.70/0.88 Following clause subsumed by 269 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(produc1911975310l_bool(A),B),C))|hBOOL(hAPP_P1708370145l_bool(A,produc1259058957on_val(B,C))).
% 0.70/0.88 Following clause subsumed by 270 during input processing: 0 [] {-} -hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(produc2062775566l_bool(A),B),C))|hBOOL(hAPP_P159683425l_bool(A,produc899768717on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 271 during input processing: 0 [] {-} -hBOOL(hAPP_P71593144l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(A),B),C))|hBOOL(hAPP_P1333315679l_bool(A,produc1611380469on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 272 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(A),B),C))|hBOOL(hAPP_P71593144l_bool(A,produc379668296on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 273 during input processing: 0 [] {-} -hBOOL(hAPP_P1907982426r_bool(hAPP_l217977712r_bool(produc1574020101r_bool(A),B),C))|hBOOL(hAPP_P92196306r_bool(A,produc921874948t_char(B,C))).
% 0.70/0.89 Following clause subsumed by 274 during input processing: 0 [] {-} -hBOOL(hAPP_P2118621157r_bool(hAPP_l1987619678r_bool(produc156891095r_bool(A),B),C))|hBOOL(hAPP_P1907982426r_bool(A,produc1909267824t_char(B,C))).
% 0.70/0.89 Following clause subsumed by 275 during input processing: 0 [] {-} -hBOOL(hAPP_e544220455r_bool(hAPP_l1062423959r_bool(produc550034914r_bool(A),B),C))|hBOOL(hAPP_P2118621157r_bool(A,produc1916172923t_char(B,C))).
% 0.70/0.89 Following clause subsumed by 276 during input processing: 0 [] {-} -hBOOL(hAPP_P929938951l_bool(hAPP_b97269396l_bool(produc1555310053l_bool(A),B),C))|hBOOL(hAPP_P943837928l_bool(A,produc621191550al_val(B,C))).
% 0.70/0.89 Following clause subsumed by 277 during input processing: 0 [] {-} -hBOOL(hAPP_val_bool(hAPP_v1392248405l_bool(produc886919678l_bool(A),B),C))|hBOOL(hAPP_P929938951l_bool(A,product_Pair_val_val(B,C))).
% 0.70/0.89 Following clause subsumed by 278 during input processing: 0 [] {-} -hBOOL(hAPP_f1715346603l_bool(hAPP_l465799708l_bool(produc481748255l_bool(A),B),C))|hBOOL(hAPP_P1235399154l_bool(A,produc823076510on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 279 during input processing: 0 [] {-} -hBOOL(hAPP_list_char_bool(hAPP_l1361600383r_bool(produc95371820r_bool(A),B),C))|hBOOL(hAPP_P449474095r_bool(A,produc5062597t_char(B,C))).
% 0.70/0.89 Following clause subsumed by 280 during input processing: 0 [] {-} -hBOOL(hAPP_e544220455r_bool(hAPP_l214204733r_bool(produc288369490r_bool(A),B),C))|hBOOL(hAPP_P2014166431r_bool(A,produc1147572817t_char(B,C))).
% 0.70/0.89 Following clause subsumed by 268 during input processing: 0 [] {-} -hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(produc1159035454l_bool(A),B),C))|hBOOL(hAPP_P282169671l_bool(A,produc1441475159on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 239 during input processing: 0 [] {-} hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(produc1159035454l_bool(A),B),C))| -hBOOL(hAPP_P282169671l_bool(A,produc1441475159on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 269 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(produc1911975310l_bool(A),B),C))|hBOOL(hAPP_P1708370145l_bool(A,produc1259058957on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 240 during input processing: 0 [] {-} hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(produc1911975310l_bool(A),B),C))| -hBOOL(hAPP_P1708370145l_bool(A,produc1259058957on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 270 during input processing: 0 [] {-} -hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(produc2062775566l_bool(A),B),C))|hBOOL(hAPP_P159683425l_bool(A,produc899768717on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 241 during input processing: 0 [] {-} hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(produc2062775566l_bool(A),B),C))| -hBOOL(hAPP_P159683425l_bool(A,produc899768717on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 271 during input processing: 0 [] {-} -hBOOL(hAPP_P71593144l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(A),B),C))|hBOOL(hAPP_P1333315679l_bool(A,produc1611380469on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 242 during input processing: 0 [] {-} hBOOL(hAPP_P71593144l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(A),B),C))| -hBOOL(hAPP_P1333315679l_bool(A,produc1611380469on_val(B,C))).
% 0.70/0.89 Following clause subsumed by 272 during input processing: 0 [] {-} -hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(A),B),C))|hBOOL(hAPP_P71593144l_bool(A,produc379668296on_val(B,C))).
% 0.70/0.91 Following clause subsumed by 243 during input processing: 0 [] {-} hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(A),B),C))| -hBOOL(hAPP_P71593144l_bool(A,produc379668296on_val(B,C))).
% 0.70/0.91 Following clause subsumed by 273 during input processing: 0 [] {-} -hBOOL(hAPP_P1907982426r_bool(hAPP_l217977712r_bool(produc1574020101r_bool(A),B),C))|hBOOL(hAPP_P92196306r_bool(A,produc921874948t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 244 during input processing: 0 [] {-} hBOOL(hAPP_P1907982426r_bool(hAPP_l217977712r_bool(produc1574020101r_bool(A),B),C))| -hBOOL(hAPP_P92196306r_bool(A,produc921874948t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 274 during input processing: 0 [] {-} -hBOOL(hAPP_P2118621157r_bool(hAPP_l1987619678r_bool(produc156891095r_bool(A),B),C))|hBOOL(hAPP_P1907982426r_bool(A,produc1909267824t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 245 during input processing: 0 [] {-} hBOOL(hAPP_P2118621157r_bool(hAPP_l1987619678r_bool(produc156891095r_bool(A),B),C))| -hBOOL(hAPP_P1907982426r_bool(A,produc1909267824t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 275 during input processing: 0 [] {-} -hBOOL(hAPP_e544220455r_bool(hAPP_l1062423959r_bool(produc550034914r_bool(A),B),C))|hBOOL(hAPP_P2118621157r_bool(A,produc1916172923t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 246 during input processing: 0 [] {-} hBOOL(hAPP_e544220455r_bool(hAPP_l1062423959r_bool(produc550034914r_bool(A),B),C))| -hBOOL(hAPP_P2118621157r_bool(A,produc1916172923t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 276 during input processing: 0 [] {-} -hBOOL(hAPP_P929938951l_bool(hAPP_b97269396l_bool(produc1555310053l_bool(A),B),C))|hBOOL(hAPP_P943837928l_bool(A,produc621191550al_val(B,C))).
% 0.70/0.91 Following clause subsumed by 247 during input processing: 0 [] {-} hBOOL(hAPP_P929938951l_bool(hAPP_b97269396l_bool(produc1555310053l_bool(A),B),C))| -hBOOL(hAPP_P943837928l_bool(A,produc621191550al_val(B,C))).
% 0.70/0.91 Following clause subsumed by 277 during input processing: 0 [] {-} -hBOOL(hAPP_val_bool(hAPP_v1392248405l_bool(produc886919678l_bool(A),B),C))|hBOOL(hAPP_P929938951l_bool(A,product_Pair_val_val(B,C))).
% 0.70/0.91 Following clause subsumed by 248 during input processing: 0 [] {-} hBOOL(hAPP_val_bool(hAPP_v1392248405l_bool(produc886919678l_bool(A),B),C))| -hBOOL(hAPP_P929938951l_bool(A,product_Pair_val_val(B,C))).
% 0.70/0.91 Following clause subsumed by 278 during input processing: 0 [] {-} -hBOOL(hAPP_f1715346603l_bool(hAPP_l465799708l_bool(produc481748255l_bool(A),B),C))|hBOOL(hAPP_P1235399154l_bool(A,produc823076510on_val(B,C))).
% 0.70/0.91 Following clause subsumed by 249 during input processing: 0 [] {-} hBOOL(hAPP_f1715346603l_bool(hAPP_l465799708l_bool(produc481748255l_bool(A),B),C))| -hBOOL(hAPP_P1235399154l_bool(A,produc823076510on_val(B,C))).
% 0.70/0.91 Following clause subsumed by 279 during input processing: 0 [] {-} -hBOOL(hAPP_list_char_bool(hAPP_l1361600383r_bool(produc95371820r_bool(A),B),C))|hBOOL(hAPP_P449474095r_bool(A,produc5062597t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 250 during input processing: 0 [] {-} hBOOL(hAPP_list_char_bool(hAPP_l1361600383r_bool(produc95371820r_bool(A),B),C))| -hBOOL(hAPP_P449474095r_bool(A,produc5062597t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 280 during input processing: 0 [] {-} -hBOOL(hAPP_e544220455r_bool(hAPP_l214204733r_bool(produc288369490r_bool(A),B),C))|hBOOL(hAPP_P2014166431r_bool(A,produc1147572817t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 251 during input processing: 0 [] {-} hBOOL(hAPP_e544220455r_bool(hAPP_l214204733r_bool(produc288369490r_bool(A),B),C))| -hBOOL(hAPP_P2014166431r_bool(A,produc1147572817t_char(B,C))).
% 0.70/0.91 Following clause subsumed by 928 during input processing: 0 [] {-} bool(A)!=null.
% 0.70/0.91 Following clause subsumed by 1060 during input processing: 0 [] {-} unit!=null.
% 0.70/0.91 Following clause subsumed by 1062 during input processing: 0 [] {-} bool(A)!=unit.
% 0.70/0.91 Following clause subsumed by 1134 during input processing: 0 [flip.1] {-} cons_val(B,A)!=A.
% 0.70/0.91 Following clause subsumed by 1135 during input processing: 0 [flip.1] {-} cons_ty(B,A)!=A.
% 0.70/0.91 Following clause subsumed by 1136 during input processing: 0 [flip.1] {-} cons_list_char(B,A)!=A.
% 0.76/0.94 Following clause subsumed by 1137 during input processing: 0 [flip.1] {-} cons_exp_list_char(B,A)!=A.
% 0.76/0.94 Following clause subsumed by 1138 during input processing: 0 [] {-} append590652462har_ty(A,B)=append590652462har_ty(C,D)|append590652462har_ty(A,E)!=C|B!=append590652462har_ty(E,D).
% 0.76/0.94 Following clause subsumed by 1139 during input processing: 0 [] {-} append_exp_list_char(A,B)=append_exp_list_char(C,D)|append_exp_list_char(A,E)!=C|B!=append_exp_list_char(E,D).
% 0.76/0.94 Following clause subsumed by 1241 during input processing: 0 [] {-} addr(A)!=null.
% 0.76/0.94 Following clause subsumed by 1244 during input processing: 0 [flip.1] {-} addr(A)!=unit.
% 0.76/0.94 Following clause subsumed by 1531 during input processing: 0 [flip.1] {-} c_Expr_Obop_OEq!=add.
% 0.76/0.94 Following clause subsumed by 1548 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.76/0.94 Following clause subsumed by 1549 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.76/0.94 Following clause subsumed by 1564 during input processing: 0 [] {-} hAPP_list_char_ty(class,A)!=nt.
% 0.76/0.94 Following clause subsumed by 1573 during input processing: 0 [flip.1] {-} hAPP_list_char_ty(class,A)!=void.
% 0.76/0.94 Following clause subsumed by 1576 during input processing: 0 [] {-} void!=nt.
% 0.76/0.94 Following clause subsumed by 1621 during input processing: 0 [] {-} void!=boolean.
% 0.76/0.94 Following clause subsumed by 1623 during input processing: 0 [] {-} nt!=boolean.
% 0.76/0.94 Following clause subsumed by 1624 during input processing: 0 [flip.1] {-} hAPP_list_char_ty(class,A)!=boolean.
% 0.76/0.94 Following clause subsumed by 1625 during input processing: 0 [] {-} -hBOOL(wTrts_1(A,B,C,D,E))|hBOOL(wTrts(A,B,C,D,E)).
% 0.76/0.94 Following clause subsumed by 1626 during input processing: 0 [] {-} -hBOOL(wTrts(A,B,C,D,E))|hBOOL(wTrts_1(A,B,C,D,E)).
% 0.76/0.94 Following clause subsumed by 1532 during input processing: 0 [] {-} -is_bop(A)| -hBOOL(hAPP_ty_bool(wTrt(B,C,D,binOp_list_char(E,A,F)),G))|A=c_Expr_Obop_OEq|A=add.
% 0.76/0.94 Following clause subsumed by 1662 during input processing: 0 [] {-} integer!=boolean.
% 0.76/0.94 Following clause subsumed by 1664 during input processing: 0 [] {-} hAPP_list_char_ty(class,A)!=integer.
% 0.76/0.94 Following clause subsumed by 1665 during input processing: 0 [flip.1] {-} nt!=integer.
% 0.76/0.94 Following clause subsumed by 1666 during input processing: 0 [flip.1] {-} void!=integer.
% 0.76/0.94 Following clause subsumed by 1684 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(produc1441475159on_val(produc1259058957on_val(B,C),produc1259058957on_val(D,E)),transi2024712006on_val(red(A)))).
% 0.76/0.94 Following clause subsumed by 1272 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(final_list_char(D)).
% 0.76/0.94 Following clause subsumed by 1688 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(produc1441475159on_val(produc1259058957on_val(B,C),produc1259058957on_val(D,E)),transi2024712006on_val(red(A))))| -hBOOL(final_list_char(D)).
% 0.76/0.94 Following clause subsumed by 1700 during input processing: 0 [] {-} -is_bool(A)|A=fTrue|A=fFalse.
% 0.76/0.94 Following clause subsumed by 299 during input processing: 0 [copy,294,flip.1] {-} cast_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.76/0.94 Following clause subsumed by 304 during input processing: 0 [copy,295,flip.1] {-} call_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.76/0.94 Following clause subsumed by 305 during input processing: 0 [copy,296,flip.1] {-} cond_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.76/0.94 Following clause subsumed by 306 during input processing: 0 [copy,297,flip.1] {-} fAcc_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.76/0.94 Following clause subsumed by 307 during input processing: 0 [copy,298,flip.1] {-} binOp_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.76/0.94 Following clause subsumed by 294 during input processing: 0 [copy,299,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=cast_list_char(B,C).
% 0.76/0.94 Following clause subsumed by 308 during input processing: 0 [copy,300,flip.1] {-} call_list_char(A,B,C)!=cast_list_char(D,E).
% 0.76/0.94 Following clause subsumed by 309 during input processing: 0 [copy,301,flip.1] {-} cond_list_char(A,B,C)!=cast_list_char(D,E).
% 0.76/0.94 Following clause subsumed by 310 during input processing: 0 [copy,302,flip.1] {-} fAcc_list_char(A,B,C)!=cast_list_char(D,E).
% 0.76/0.94 Following clause subsumed by 311 during input processing: 0 [copy,303,flip.1] {-} binOp_list_char(A,B,C)!=cast_list_char(D,E).
% 0.76/0.94 Following clause subsumed by 295 during input processing: 0 [copy,304,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=call_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 296 during input processing: 0 [copy,305,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=cond_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 297 during input processing: 0 [copy,306,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=fAcc_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 298 during input processing: 0 [copy,307,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=binOp_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 300 during input processing: 0 [copy,308,flip.1] {-} cast_list_char(A,B)!=call_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 301 during input processing: 0 [copy,309,flip.1] {-} cast_list_char(A,B)!=cond_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 302 during input processing: 0 [copy,310,flip.1] {-} cast_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 303 during input processing: 0 [copy,311,flip.1] {-} cast_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 315 during input processing: 0 [copy,312,flip.1] {-} cond_list_char(A,B,C)!=call_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 318 during input processing: 0 [copy,313,flip.1] {-} fAcc_list_char(A,B,C)!=call_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 321 during input processing: 0 [copy,314,flip.1] {-} binOp_list_char(A,B,C)!=call_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 312 during input processing: 0 [copy,315,flip.1] {-} call_list_char(A,B,C)!=cond_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 319 during input processing: 0 [copy,316,flip.1] {-} fAcc_list_char(A,B,C)!=cond_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 322 during input processing: 0 [copy,317,flip.1] {-} binOp_list_char(A,B,C)!=cond_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 313 during input processing: 0 [copy,318,flip.1] {-} call_list_char(A,B,C)!=fAcc_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 316 during input processing: 0 [copy,319,flip.1] {-} cond_list_char(A,B,C)!=fAcc_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 323 during input processing: 0 [copy,320,flip.1] {-} binOp_list_char(A,B,C)!=fAcc_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 314 during input processing: 0 [copy,321,flip.1] {-} call_list_char(A,B,C)!=binOp_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 317 during input processing: 0 [copy,322,flip.1] {-} cond_list_char(A,B,C)!=binOp_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 320 during input processing: 0 [copy,323,flip.1] {-} fAcc_list_char(A,B,C)!=binOp_list_char(D,E,F).
% 0.76/0.94 Following clause subsumed by 384 during input processing: 0 [copy,345,flip.1] {-} tryCatch_list_char(A,B,C,D)!=hAPP_v834067052t_char(val_list_char,E).
% 0.76/0.94 Following clause subsumed by 345 during input processing: 0 [copy,384,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=tryCatch_list_char(B,C,D,E).
% 0.76/0.94 Following clause subsumed by 390 during input processing: 0 [copy,385,flip.1] {-} tryCatch_list_char(A,B,C,D)!=cast_list_char(E,F).
% 0.76/0.94 Following clause subsumed by 391 during input processing: 0 [copy,386,flip.1] {-} tryCatch_list_char(A,B,C,D)!=call_list_char(E,F,G).
% 0.76/0.94 Following clause subsumed by 392 during input processing: 0 [copy,387,flip.1] {-} tryCatch_list_char(A,B,C,D)!=cond_list_char(E,F,G).
% 0.76/0.94 Following clause subsumed by 393 during input processing: 0 [copy,388,flip.1] {-} tryCatch_list_char(A,B,C,D)!=fAcc_list_char(E,F,G).
% 0.76/0.94 Following clause subsumed by 394 during input processing: 0 [copy,389,flip.1] {-} tryCatch_list_char(A,B,C,D)!=binOp_list_char(E,F,G).
% 0.76/0.94 Following clause subsumed by 385 during input processing: 0 [copy,390,flip.1] {-} cast_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.76/0.94 Following clause subsumed by 386 during input processing: 0 [copy,391,flip.1] {-} call_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.76/0.94 Following clause subsumed by 387 during input processing: 0 [copy,392,flip.1] {-} cond_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.76/0.94 Following clause subsumed by 388 during input processing: 0 [copy,393,flip.1] {-} fAcc_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.76/0.94 Following clause subsumed by 389 during input processing: 0 [copy,394,flip.1] {-} binOp_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.76/0.94 Following clause subsumed by 937 during input processing: 0 [copy,936,flip.1] {-} while_list_char(A,B)!=throw_list_char(C).
% 0.76/0.94 Following clause subsumed by 936 during input processing: 0 [copy,937,flip.1] {-} throw_list_char(A)!=while_list_char(B,C).
% 0.76/0.94 Following clause subsumed by 944 during input processing: 0 [copy,943,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=throw_list_char(B).
% 0.76/0.94 Following clause subsumed by 943 during input processing: 0 [copy,944,flip.1] {-} throw_list_char(A)!=hAPP_v834067052t_char(val_list_char,B).
% 0.76/0.94 Following clause subsumed by 946 during input processing: 0 [copy,945,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=while_list_char(B,C).
% 0.76/0.94 Following clause subsumed by 945 during input processing: 0 [copy,946,flip.1] {-} while_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.76/0.94 Following clause subsumed by 948 during input processing: 0 [copy,947,flip.1] {-} throw_list_char(A)!=call_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 947 during input processing: 0 [copy,948,flip.1] {-} call_list_char(A,B,C)!=throw_list_char(D).
% 0.76/0.94 Following clause subsumed by 950 during input processing: 0 [copy,949,flip.1] {-} throw_list_char(A)!=binOp_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 949 during input processing: 0 [copy,950,flip.1] {-} binOp_list_char(A,B,C)!=throw_list_char(D).
% 0.76/0.94 Following clause subsumed by 953 during input processing: 0 [copy,951,flip.1] {-} throw_list_char(A)!=cond_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 954 during input processing: 0 [copy,952,flip.1] {-} throw_list_char(A)!=cast_list_char(B,C).
% 0.76/0.94 Following clause subsumed by 951 during input processing: 0 [copy,953,flip.1] {-} cond_list_char(A,B,C)!=throw_list_char(D).
% 0.76/0.94 Following clause subsumed by 952 during input processing: 0 [copy,954,flip.1] {-} cast_list_char(A,B)!=throw_list_char(C).
% 0.76/0.94 Following clause subsumed by 956 during input processing: 0 [copy,955,flip.1] {-} throw_list_char(A)!=fAcc_list_char(B,C,D).
% 0.76/0.94 Following clause subsumed by 955 during input processing: 0 [copy,956,flip.1] {-} fAcc_list_char(A,B,C)!=throw_list_char(D).
% 0.76/0.94 Following clause subsumed by 958 during input processing: 0 [copy,957,flip.1] {-} throw_list_char(A)!=tryCatch_list_char(B,C,D,E).
% 0.76/0.94 Following clause subsumed by 957 during input processing: 0 [copy,958,flip.1] {-} tryCatch_list_char(A,B,C,D)!=throw_list_char(E).
% 0.76/0.94 Following clause subsumed by 960 during input processing: 0 [copy,959,flip.1] {-} while_list_char(A,B)!=call_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 959 during input processing: 0 [copy,960,flip.1] {-} call_list_char(A,B,C)!=while_list_char(D,E).
% 0.76/0.94 Following clause subsumed by 962 during input processing: 0 [copy,961,flip.1] {-} while_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 961 during input processing: 0 [copy,962,flip.1] {-} binOp_list_char(A,B,C)!=while_list_char(D,E).
% 0.76/0.94 Following clause subsumed by 964 during input processing: 0 [copy,963,flip.1] {-} while_list_char(A,B)!=cond_list_char(C,D,E).
% 0.76/0.94 Following clause subsumed by 963 during input processing: 0 [copy,964,flip.1] {-} cond_list_char(A,B,C)!=while_list_char(D,E).
% 0.76/0.95 Following clause subsumed by 966 during input processing: 0 [copy,965,flip.1] {-} cast_list_char(A,B)!=while_list_char(C,D).
% 0.76/0.95 Following clause subsumed by 965 during input processing: 0 [copy,966,flip.1] {-} while_list_char(A,B)!=cast_list_char(C,D).
% 0.76/0.95 Following clause subsumed by 968 during input processing: 0 [copy,967,flip.1] {-} while_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.76/0.95 Following clause subsumed by 967 during input processing: 0 [copy,968,flip.1] {-} fAcc_list_char(A,B,C)!=while_list_char(D,E).
% 0.76/0.95 Following clause subsumed by 970 during input processing: 0 [copy,969,flip.1] {-} while_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.76/0.95 Following clause subsumed by 969 during input processing: 0 [copy,970,flip.1] {-} tryCatch_list_char(A,B,C,D)!=while_list_char(E,F).
% 0.76/0.95 Following clause subsumed by 1001 during input processing: 0 [copy,999,flip.1] {-} lAss_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.76/0.95 Following clause subsumed by 1002 during input processing: 0 [copy,1000,flip.1] {-} seq_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.76/0.95 Following clause subsumed by 999 during input processing: 0 [copy,1001,flip.1] {-} fAss_list_char(A,B,C,D)!=lAss_list_char(E,F).
% 0.76/0.95 Following clause subsumed by 1000 during input processing: 0 [copy,1002,flip.1] {-} fAss_list_char(A,B,C,D)!=seq_list_char(E,F).
% 0.76/0.95 Following clause subsumed by 1004 during input processing: 0 [copy,1003,flip.1] {-} seq_list_char(A,B)!=lAss_list_char(C,D).
% 0.76/0.95 Following clause subsumed by 1003 during input processing: 0 [copy,1004,flip.1] {-} lAss_list_char(A,B)!=seq_list_char(C,D).
% 0.76/0.95 Following clause subsumed by 1008 during input processing: 0 [copy,1005,flip.1] {-} seq_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.76/0.95 Following clause subsumed by 1009 during input processing: 0 [copy,1006,flip.1] {-} lAss_list_char(A,B)!=hAPP_v834067052t_char(val_list_char,C).
% 0.76/0.95 Following clause subsumed by 1010 during input processing: 0 [copy,1007,flip.1] {-} fAss_list_char(A,B,C,D)!=hAPP_v834067052t_char(val_list_char,E).
% 0.76/0.95 Following clause subsumed by 1005 during input processing: 0 [copy,1008,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=seq_list_char(B,C).
% 0.76/0.95 Following clause subsumed by 1006 during input processing: 0 [copy,1009,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=lAss_list_char(B,C).
% 0.76/0.95 Following clause subsumed by 1007 during input processing: 0 [copy,1010,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=fAss_list_char(B,C,D,E).
% 0.76/0.95 Following clause subsumed by 1014 during input processing: 0 [copy,1011,flip.1] {-} throw_list_char(A)!=fAss_list_char(B,C,D,E).
% 0.76/0.95 Following clause subsumed by 1015 during input processing: 0 [copy,1012,flip.1] {-} throw_list_char(A)!=lAss_list_char(B,C).
% 0.76/0.95 Following clause subsumed by 1016 during input processing: 0 [copy,1013,flip.1] {-} throw_list_char(A)!=seq_list_char(B,C).
% 0.76/0.95 Following clause subsumed by 1011 during input processing: 0 [copy,1014,flip.1] {-} fAss_list_char(A,B,C,D)!=throw_list_char(E).
% 0.76/0.95 Following clause subsumed by 1012 during input processing: 0 [copy,1015,flip.1] {-} lAss_list_char(A,B)!=throw_list_char(C).
% 0.76/0.95 Following clause subsumed by 1013 during input processing: 0 [copy,1016,flip.1] {-} seq_list_char(A,B)!=throw_list_char(C).
% 0.76/0.95 Following clause subsumed by 1019 during input processing: 0 [copy,1017,flip.1] {-} call_list_char(A,B,C)!=seq_list_char(D,E).
% 0.76/0.95 Following clause subsumed by 1020 during input processing: 0 [copy,1018,flip.1] {-} call_list_char(A,B,C)!=lAss_list_char(D,E).
% 0.76/0.95 Following clause subsumed by 1017 during input processing: 0 [copy,1019,flip.1] {-} seq_list_char(A,B)!=call_list_char(C,D,E).
% 0.76/0.95 Following clause subsumed by 1018 during input processing: 0 [copy,1020,flip.1] {-} lAss_list_char(A,B)!=call_list_char(C,D,E).
% 0.76/0.95 Following clause subsumed by 1022 during input processing: 0 [copy,1021,flip.1] {-} fAss_list_char(A,B,C,D)!=call_list_char(E,F,G).
% 0.76/0.95 Following clause subsumed by 1021 during input processing: 0 [copy,1022,flip.1] {-} call_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.76/0.95 Following clause subsumed by 1025 during input processing: 0 [copy,1023,flip.1] {-} binOp_list_char(A,B,C)!=seq_list_char(D,E).
% 0.77/0.95 Following clause subsumed by 1026 during input processing: 0 [copy,1024,flip.1] {-} binOp_list_char(A,B,C)!=lAss_list_char(D,E).
% 0.77/0.95 Following clause subsumed by 1023 during input processing: 0 [copy,1025,flip.1] {-} seq_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.77/0.95 Following clause subsumed by 1024 during input processing: 0 [copy,1026,flip.1] {-} lAss_list_char(A,B)!=binOp_list_char(C,D,E).
% 0.77/0.95 Following clause subsumed by 1028 during input processing: 0 [copy,1027,flip.1] {-} fAss_list_char(A,B,C,D)!=binOp_list_char(E,F,G).
% 0.77/0.95 Following clause subsumed by 1027 during input processing: 0 [copy,1028,flip.1] {-} binOp_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.77/0.95 Following clause subsumed by 1030 during input processing: 0 [copy,1029,flip.1] {-} cast_list_char(A,B)!=seq_list_char(C,D).
% 0.77/0.95 Following clause subsumed by 1029 during input processing: 0 [copy,1030,flip.1] {-} seq_list_char(A,B)!=cast_list_char(C,D).
% 0.77/0.95 Following clause subsumed by 1032 during input processing: 0 [copy,1031,flip.1] {-} lAss_list_char(A,B)!=cast_list_char(C,D).
% 0.77/0.95 Following clause subsumed by 1031 during input processing: 0 [copy,1032,flip.1] {-} cast_list_char(A,B)!=lAss_list_char(C,D).
% 0.77/0.95 Following clause subsumed by 1036 during input processing: 0 [copy,1033,flip.1] {-} cond_list_char(A,B,C)!=seq_list_char(D,E).
% 0.77/0.95 Following clause subsumed by 1037 during input processing: 0 [copy,1034,flip.1] {-} cond_list_char(A,B,C)!=lAss_list_char(D,E).
% 0.77/0.95 Following clause subsumed by 1039 during input processing: 0 [copy,1035,flip.1] {-} fAss_list_char(A,B,C,D)!=cast_list_char(E,F).
% 0.77/0.95 Following clause subsumed by 1033 during input processing: 0 [copy,1036,flip.1] {-} seq_list_char(A,B)!=cond_list_char(C,D,E).
% 0.77/0.95 Following clause subsumed by 1034 during input processing: 0 [copy,1037,flip.1] {-} lAss_list_char(A,B)!=cond_list_char(C,D,E).
% 0.77/0.95 Following clause subsumed by 1040 during input processing: 0 [copy,1038,flip.1] {-} fAss_list_char(A,B,C,D)!=cond_list_char(E,F,G).
% 0.77/0.95 Following clause subsumed by 1035 during input processing: 0 [copy,1039,flip.1] {-} cast_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.77/0.95 Following clause subsumed by 1038 during input processing: 0 [copy,1040,flip.1] {-} cond_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.77/0.95 Following clause subsumed by 1043 during input processing: 0 [copy,1041,flip.1] {-} fAcc_list_char(A,B,C)!=seq_list_char(D,E).
% 0.77/0.95 Following clause subsumed by 1044 during input processing: 0 [copy,1042,flip.1] {-} fAcc_list_char(A,B,C)!=lAss_list_char(D,E).
% 0.77/0.95 Following clause subsumed by 1041 during input processing: 0 [copy,1043,flip.1] {-} seq_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.77/0.95 Following clause subsumed by 1042 during input processing: 0 [copy,1044,flip.1] {-} lAss_list_char(A,B)!=fAcc_list_char(C,D,E).
% 0.77/0.95 Following clause subsumed by 1046 during input processing: 0 [copy,1045,flip.1] {-} fAss_list_char(A,B,C,D)!=fAcc_list_char(E,F,G).
% 0.77/0.95 Following clause subsumed by 1045 during input processing: 0 [copy,1046,flip.1] {-} fAcc_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.77/0.95 Following clause subsumed by 1049 during input processing: 0 [copy,1047,flip.1] {-} tryCatch_list_char(A,B,C,D)!=seq_list_char(E,F).
% 0.77/0.95 Following clause subsumed by 1050 during input processing: 0 [copy,1048,flip.1] {-} tryCatch_list_char(A,B,C,D)!=lAss_list_char(E,F).
% 0.77/0.95 Following clause subsumed by 1047 during input processing: 0 [copy,1049,flip.1] {-} seq_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.77/0.95 Following clause subsumed by 1048 during input processing: 0 [copy,1050,flip.1] {-} lAss_list_char(A,B)!=tryCatch_list_char(C,D,E,F).
% 0.77/0.95 Following clause subsumed by 1052 during input processing: 0 [copy,1051,flip.1] {-} tryCatch_list_char(A,B,C,D)!=fAss_list_char(E,F,G,H).
% 0.77/0.95 Following clause subsumed by 1051 during input processing: 0 [copy,1052,flip.1] {-} fAss_list_char(A,B,C,D)!=tryCatch_list_char(E,F,G,H).
% 0.77/0.95 Following clause subsumed by 1054 during input processing: 0 [copy,1053,flip.1] {-} while_list_char(A,B)!=fAss_list_char(C,D,E,F).
% 0.77/0.95 Following clause subsumed by 1053 during input processing: 0 [copy,1054,flip.1] {-} fAss_list_char(A,B,C,D)!=while_list_char(E,F).
% 0.77/0.97 Following clause subsumed by 1057 during input processing: 0 [copy,1055,flip.1] {-} lAss_list_char(A,B)!=while_list_char(C,D).
% 0.77/0.97 Following clause subsumed by 1058 during input processing: 0 [copy,1056,flip.1] {-} seq_list_char(A,B)!=while_list_char(C,D).
% 0.77/0.97 Following clause subsumed by 1055 during input processing: 0 [copy,1057,flip.1] {-} while_list_char(A,B)!=lAss_list_char(C,D).
% 0.77/0.97 Following clause subsumed by 1056 during input processing: 0 [copy,1058,flip.1] {-} while_list_char(A,B)!=seq_list_char(C,D).
% 0.77/0.97 Following clause subsumed by 1097 during input processing: 0 [copy,1096,flip.1] {-} hAPP_v834067052t_char(val_list_char,A)!=block_list_char(B,C,D).
% 0.77/0.97 Following clause subsumed by 1096 during input processing: 0 [copy,1097,flip.1] {-} block_list_char(A,B,C)!=hAPP_v834067052t_char(val_list_char,D).
% 0.77/0.97 Following clause subsumed by 1099 during input processing: 0 [copy,1098,flip.1] {-} block_list_char(A,B,C)!=throw_list_char(D).
% 0.77/0.97 Following clause subsumed by 1098 during input processing: 0 [copy,1099,flip.1] {-} throw_list_char(A)!=block_list_char(B,C,D).
% 0.77/0.97 Following clause subsumed by 1102 during input processing: 0 [copy,1100,flip.1] {-} block_list_char(A,B,C)!=seq_list_char(D,E).
% 0.77/0.97 Following clause subsumed by 1103 during input processing: 0 [copy,1101,flip.1] {-} block_list_char(A,B,C)!=lAss_list_char(D,E).
% 0.77/0.97 Following clause subsumed by 1100 during input processing: 0 [copy,1102,flip.1] {-} seq_list_char(A,B)!=block_list_char(C,D,E).
% 0.77/0.97 Following clause subsumed by 1101 during input processing: 0 [copy,1103,flip.1] {-} lAss_list_char(A,B)!=block_list_char(C,D,E).
% 0.77/0.97 Following clause subsumed by 1105 during input processing: 0 [copy,1104,flip.1] {-} call_list_char(A,B,C)!=block_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1104 during input processing: 0 [copy,1105,flip.1] {-} block_list_char(A,B,C)!=call_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1107 during input processing: 0 [copy,1106,flip.1] {-} fAss_list_char(A,B,C,D)!=block_list_char(E,F,G).
% 0.77/0.97 Following clause subsumed by 1106 during input processing: 0 [copy,1107,flip.1] {-} block_list_char(A,B,C)!=fAss_list_char(D,E,F,G).
% 0.77/0.97 Following clause subsumed by 1109 during input processing: 0 [copy,1108,flip.1] {-} binOp_list_char(A,B,C)!=block_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1108 during input processing: 0 [copy,1109,flip.1] {-} block_list_char(A,B,C)!=binOp_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1111 during input processing: 0 [copy,1110,flip.1] {-} cond_list_char(A,B,C)!=block_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1110 during input processing: 0 [copy,1111,flip.1] {-} block_list_char(A,B,C)!=cond_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1113 during input processing: 0 [copy,1112,flip.1] {-} cast_list_char(A,B)!=block_list_char(C,D,E).
% 0.77/0.97 Following clause subsumed by 1112 during input processing: 0 [copy,1113,flip.1] {-} block_list_char(A,B,C)!=cast_list_char(D,E).
% 0.77/0.97 Following clause subsumed by 1115 during input processing: 0 [copy,1114,flip.1] {-} fAcc_list_char(A,B,C)!=block_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1114 during input processing: 0 [copy,1115,flip.1] {-} block_list_char(A,B,C)!=fAcc_list_char(D,E,F).
% 0.77/0.97 Following clause subsumed by 1117 during input processing: 0 [copy,1116,flip.1] {-} block_list_char(A,B,C)!=while_list_char(D,E).
% 0.77/0.97 Following clause subsumed by 1116 during input processing: 0 [copy,1117,flip.1] {-} while_list_char(A,B)!=block_list_char(C,D,E).
% 0.77/0.97 Following clause subsumed by 1119 during input processing: 0 [copy,1118,flip.1] {-} block_list_char(A,B,C)!=tryCatch_list_char(D,E,F,G).
% 0.77/0.97 Following clause subsumed by 1118 during input processing: 0 [copy,1119,flip.1] {-} tryCatch_list_char(A,B,C,D)!=block_list_char(E,F,G).
% 0.77/0.97 Following clause subsumed by 1243 during input processing: 0 [copy,1242,flip.1] {-} bool(A)!=addr(B).
% 0.77/0.97 Following clause subsumed by 1242 during input processing: 0 [copy,1243,flip.1] {-} addr(A)!=bool(B).
% 0.77/0.97
% 0.77/0.97 ------------> process sos:
% 0.77/0.97 Following clause subsumed by 2442 during input processing: 0 [copy,2442,flip.1] {-} A=A.
% 0.77/0.97 2442 back subsumes 1872.
% 0.77/0.97 2442 back subsumes 1842.
% 0.77/0.97 2442 back subsumes 1761.
% 0.77/0.97 2442 back subsumes 1752.
% 0.77/0.97 2442 back subsumes 1727.
% 0.77/0.97
% 0.77/0.97 ======= end of input processing =======
% 0.84/1.01
% 0.84/1.01 SEGMENTATION FAULT!! This is probably caused by a
% 0.84/1.01 bug in Otter. Please send copy of the input file to
% 0.84/1.01 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.84/1.01 using, and send any other info that might be useful.
% 0.84/1.01
% 0.84/1.01
% 0.84/1.01 SEGMENTATION FAULT!! This is probably caused by a
% 0.84/1.01 bug in Otter. Please send copy of the input file to
% 0.84/1.01 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.84/1.01 using, and send any other info that might be useful.
% 0.84/1.01
% 0.84/1.01
% 0.84/1.01 The job finished Sun Jun 5 04:17:15 2022
%------------------------------------------------------------------------------