%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : ITP005+5 : TPTP v8.1.0. Bugfixed v7.5.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 : Sun Jul 17 00:35:23 EDT 2022
% Result : Timeout 287.66s 287.88s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : ITP005+5 : TPTP v8.1.0. Bugfixed v7.5.0.
% 0.11/0.12 % Command : sos-script %s
% 0.11/0.33 % Computer : n027.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Thu Jun 2 11:55:05 EDT 2022
% 0.11/0.33 % CPUTime :
% 2.32/2.59 ----- Otter 3.2, August 2001 -----
% 2.32/2.59 The process was started by sandbox on n027.cluster.edu,
% 2.32/2.59 Thu Jun 2 11:55:05 2022
% 2.32/2.59 The command was "./sos". The process ID is 27903.
% 2.32/2.59
% 2.32/2.59 set(prolog_style_variables).
% 2.32/2.59 set(auto).
% 2.32/2.59 dependent: set(auto1).
% 2.32/2.59 dependent: set(process_input).
% 2.32/2.59 dependent: clear(print_kept).
% 2.32/2.59 dependent: clear(print_new_demod).
% 2.32/2.59 dependent: clear(print_back_demod).
% 2.32/2.59 dependent: clear(print_back_sub).
% 2.32/2.59 dependent: set(control_memory).
% 2.32/2.59 dependent: assign(max_mem, 12000).
% 2.32/2.59 dependent: assign(pick_given_ratio, 4).
% 2.32/2.59 dependent: assign(stats_level, 1).
% 2.32/2.59 dependent: assign(pick_semantic_ratio, 3).
% 2.32/2.59 dependent: assign(sos_limit, 5000).
% 2.32/2.59 dependent: assign(max_weight, 60).
% 2.32/2.59 clear(print_given).
% 2.32/2.59
% 2.32/2.59 formula_list(usable).
% 2.32/2.59
% 2.32/2.59 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=18.
% 2.32/2.59
% 2.32/2.59 This ia a non-Horn set with equality. The strategy will be
% 2.32/2.59 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 2.32/2.59 unit deletion, with positive clauses in sos and nonpositive
% 2.32/2.59 clauses in usable.
% 2.32/2.59
% 2.32/2.59 dependent: set(knuth_bendix).
% 2.32/2.59 dependent: set(para_from).
% 2.32/2.59 dependent: set(para_into).
% 2.32/2.59 dependent: clear(para_from_right).
% 2.32/2.59 dependent: clear(para_into_right).
% 2.32/2.59 dependent: set(para_from_vars).
% 2.32/2.59 dependent: set(eq_units_both_ways).
% 2.32/2.59 dependent: set(dynamic_demod_all).
% 2.32/2.59 dependent: set(dynamic_demod).
% 2.32/2.59 dependent: set(order_eq).
% 2.32/2.59 dependent: set(back_demod).
% 2.32/2.59 dependent: set(lrpo).
% 2.32/2.59 dependent: set(hyper_res).
% 2.32/2.59 dependent: set(unit_deletion).
% 2.32/2.59 dependent: set(factor).
% 2.32/2.59
% 2.32/2.59 ------------> process usable:
% 2.32/2.59 Following clause subsumed by 119 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,A)|ap(f48(B,A,C),D)=ap(C,D).
% 2.32/2.59 Following clause subsumed by 18 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -p(ap(c_2Ebool_2E_21(A),B))| -mem(C,A)|p(ap(B,C)).
% 2.32/2.59 Following clause subsumed by 27 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(c_2Ebool_2E_3F(A),B))| -mem(C,A)| -p(ap(B,C)).
% 2.32/2.59 Following clause subsumed by 7 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)|ap(k(B,C),D)=C.
% 2.32/2.59 Following clause subsumed by 127 during input processing: 0 [propositional] {-} -ne(A)| -mem(B,A)|B=B.
% 2.32/2.59 Following clause subsumed by 128 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)|B!=C|C=B.
% 2.32/2.59 Following clause subsumed by 128 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)|B=C|C!=B.
% 2.32/2.59 Following clause subsumed by 261 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))| -p(A)|p(B).
% 2.32/2.59 Following clause subsumed by 262 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))|p(A)|p(C).
% 2.32/2.59 Following clause subsumed by 263 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))|p(A)| -p(C).
% 2.32/2.59 Following clause subsumed by 264 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))| -p(B)| -p(A).
% 2.32/2.59 Following clause subsumed by 265 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))| -p(B)| -p(C).
% 2.32/2.59 Following clause subsumed by 262 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))|p(A)|p(C).
% 2.32/2.59 Following clause subsumed by 261 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))|p(B)| -p(A).
% 2.32/2.59 Following clause subsumed by 264 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))| -p(A)| -p(B).
% 2.32/2.59 Following clause subsumed by 263 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),C))|p(A)| -p(C).
% 2.41/2.65 Following clause subsumed by 266 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(A)|p(C)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),E),A),C))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),E),B),D)).
% 2.41/2.65 Following clause subsumed by 265 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)| -p(B)| -p(D)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),E),A),C))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),E),B),D)).
% 2.41/2.65 Following clause subsumed by 378 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)|C!=D|p(ap(B,D))| -p(ap(B,C)).
% 2.41/2.65 Following clause subsumed by 373 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)|D!=C|p(ap(B,D))| -p(ap(B,C)).
% 2.41/2.65 Following clause subsumed by 135 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)|ap(ap(ap(c_2Ebool_2ECOND(A),c_2Ebool_2ET),B),C)=B.
% 2.41/2.65 Following clause subsumed by 136 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)|ap(ap(ap(c_2Ebool_2ECOND(A),c_2Ebool_2EF),B),C)=C.
% 2.41/2.65 Following clause subsumed by 137 during input processing: 0 [] {-} -ne(A)| -mem(B,bool)| -mem(C,A)|ap(ap(ap(c_2Ebool_2ECOND(A),B),C),C)=C.
% 2.41/2.65 Following clause subsumed by 337 during input processing: 0 [] {-} -ne(A)| -mem(B,bool)| -mem(C,bool)| -mem(D,A)| -mem(E,A)| -mem(F,A)| -mem(G,A)|p(B)|p(C)|F!=G|ap(ap(ap(c_2Ebool_2ECOND(A),B),D),F)=ap(ap(ap(c_2Ebool_2ECOND(A),C),E),G).
% 2.41/2.65 Following clause subsumed by 338 during input processing: 0 [] {-} -ne(A)| -mem(B,bool)| -mem(C,bool)| -mem(D,A)| -mem(E,A)| -mem(F,A)| -mem(G,A)| -p(B)| -p(C)|D!=E|ap(ap(ap(c_2Ebool_2ECOND(A),B),D),F)=ap(ap(ap(c_2Ebool_2ECOND(A),C),E),G).
% 2.41/2.65 Following clause subsumed by 400 during input processing: 0 [] {-} -mem(A,arr(bool,bool))| -mem(B,bool)|p(ap(A,B))| -p(ap(A,c_2Ebool_2ET))| -p(ap(A,c_2Ebool_2EF)).
% 2.41/2.65 Following clause subsumed by 476 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(ty_2Ebool_2Eitself(A),bool))| -mem(C,ty_2Ebool_2Eitself(A))|p(ap(B,C))| -p(ap(B,c_2Ebool_2Ethe__value(A))).
% 2.41/2.65 Following clause subsumed by 266 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(C)|p(E)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 367 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(C)| -p(D)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 368 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)| -p(B)|p(E)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 265 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)| -p(B)| -p(D)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 262 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(A)|p(E)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 263 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(A)| -p(D)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 261 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(C)| -p(A)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 266 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(C)|p(E)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.41/2.65 Following clause subsumed by 367 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)|p(C)| -p(D)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.51/2.69 Following clause subsumed by 264 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)| -p(B)| -p(A)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.51/2.69 Following clause subsumed by 368 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)| -p(B)|p(E)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.51/2.69 Following clause subsumed by 265 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -mem(E,bool)| -p(B)| -p(D)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),C),E))|p(ap(ap(ap(c_2Ebool_2ECOND(bool),A),B),D)).
% 2.51/2.69 Following clause subsumed by 135 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)|ap(ap(ap(c_2Ebool_2ECOND(A),c_2Ebool_2ET),B),C)=B.
% 2.51/2.69 Following clause subsumed by 136 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)|ap(ap(ap(c_2Ebool_2ECOND(A),c_2Ebool_2EF),B),C)=C.
% 2.51/2.69 Following clause subsumed by 137 during input processing: 0 [] {-} -ne(A)| -mem(B,bool)| -mem(C,A)|ap(ap(ap(c_2Ebool_2ECOND(A),B),C),C)=C.
% 2.51/2.69 Following clause subsumed by 263 during input processing: 0 [factor_simp,factor_simp] {-} -mem(B,bool)| -mem(C,bool)| -mem(D,bool)|p(B)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))| -p(D).
% 2.51/2.69 Following clause subsumed by 264 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)|p(A)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))| -p(C)| -p(B).
% 2.51/2.69 Following clause subsumed by 265 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)|p(A)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))| -p(C)| -p(D).
% 2.51/2.69 Following clause subsumed by 261 during input processing: 0 [factor_simp,factor_simp] {-} -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -p(B)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))|p(C).
% 2.51/2.69 Following clause subsumed by 262 during input processing: 0 [] {-} -mem(A,bool)| -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -p(A)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))|p(B)|p(D).
% 2.51/2.69 Following clause subsumed by 263 during input processing: 0 [factor_simp,factor_simp] {-} -mem(D,bool)| -mem(B,bool)| -mem(C,bool)| -p(D)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))|p(B).
% 2.51/2.69 Following clause subsumed by 264 during input processing: 0 [factor_simp,factor_simp] {-} -mem(B,bool)| -mem(C,bool)| -mem(D,bool)| -p(B)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))| -p(C).
% 2.51/2.69 Following clause subsumed by 265 during input processing: 0 [factor_simp,factor_simp] {-} -mem(C,bool)| -mem(B,bool)| -mem(D,bool)| -p(C)|p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))| -p(D).
% 2.51/2.69 Following clause subsumed by 261 during input processing: 0 [factor_simp,factor_simp] {-} -mem(C,bool)| -mem(B,bool)| -mem(D,bool)|p(C)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))| -p(B).
% 2.51/2.69 Following clause subsumed by 266 during input processing: 0 [factor_simp,factor_simp] {-} -mem(C,bool)| -mem(B,bool)| -mem(D,bool)|p(C)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))|p(D).
% 2.51/2.69 Following clause subsumed by 262 during input processing: 0 [factor_simp,factor_simp] {-} -mem(B,bool)| -mem(C,bool)| -mem(D,bool)|p(B)| -p(ap(ap(ap(c_2Ebool_2ECOND(bool),B),C),D))|p(D).
% 2.51/2.69 Following clause subsumed by 552 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,B))|ap(C,ap(ap(c_2EnormalForms_2EEXT__POINT(A,B),C),D))!=ap(D,ap(ap(c_2EnormalForms_2EEXT__POINT(A,B),C),D))|C=D.
% 2.51/2.69 Following clause subsumed by 554 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -p(ap(B,ap(c_2EnormalForms_2EUNIV__POINT(A),B)))| -mem(C,A)|p(ap(B,C)).
% 2.51/2.69 Following clause subsumed by 639 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,B)| -mem(E,A)|ap(C,E)!=D|ap(ap(ap(c_2Ecombin_2EUPDATE(A,B),E),D),C)=C.
% 2.51/2.69 Following clause subsumed by 650 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,A)| -mem(E,B)| -mem(F,B)|ap(ap(ap(c_2Ecombin_2EUPDATE(A,B),D),E),C)!=ap(ap(ap(c_2Ecombin_2EUPDATE(A,B),D),F),C)|E=F.
% 6.84/7.10 Following clause subsumed by 663 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,A)))| -p(ap(c_2Ecombin_2EASSOC(A),B))| -mem(C,A)| -mem(D,A)| -mem(E,A)|ap(ap(B,ap(ap(B,C),D)),E)=ap(ap(B,C),ap(ap(B,D),E)).
% 6.84/7.10 Following clause subsumed by 726 during input processing: 0 [] {-} -mem(A,arr(ty_2Eone_2Eone,bool))| -mem(B,ty_2Eone_2Eone)|p(ap(A,B))| -p(ap(A,c_2Eone_2Eone)).
% 6.84/7.10 Following clause subsumed by 769 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,A)|ap(c_2Esum_2EINL(A,B),D)!=ap(c_2Esum_2EINL(A,B),C)|D=C.
% 6.84/7.10 Following clause subsumed by 770 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,A)|ap(c_2Esum_2EINL(A,B),D)=ap(c_2Esum_2EINL(A,B),C)|D!=C.
% 6.84/7.10 Following clause subsumed by 771 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,B)|ap(c_2Esum_2EINR(A,B),D)!=ap(c_2Esum_2EINR(A,B),C)|D=C.
% 6.84/7.10 Following clause subsumed by 772 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,B)|ap(c_2Esum_2EINR(A,B),D)=ap(c_2Esum_2EINR(A,B),C)|D!=C.
% 6.84/7.10 Following clause subsumed by 773 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)|ap(c_2Esum_2EINR(A,B),D)!=ap(c_2Esum_2EINL(A,B),C).
% 6.84/7.10 Following clause subsumed by 813 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,ty_2Esum_2Esum(A,B))|p(ap(c_2Esum_2EISL(A,B),C))|p(ap(c_2Esum_2EISR(A,B),C)).
% 6.84/7.10 Following clause subsumed by 813 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,ty_2Esum_2Esum(A,B))|p(ap(c_2Esum_2EISR(A,B),C))|p(ap(c_2Esum_2EISL(A,B),C)).
% 6.84/7.10 Following clause subsumed by 862 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,ty_2Esum_2Esum(A,B))| -p(ap(c_2Esum_2EISR(A,B),C))| -p(ap(c_2Esum_2EISL(A,B),C)).
% 6.84/7.10 Following clause subsumed by 987 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -p(ap(c_2Erelation_2Esymmetric(A),B))| -mem(C,A)| -mem(D,A)|p(ap(ap(B,C),D))| -p(ap(ap(B,D),C)).
% 6.84/7.10 Following clause subsumed by 1081 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),C)).
% 6.84/7.10 Following clause subsumed by 1099 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|p(ap(c_2Erelation_2Etransitive(A),ap(c_2Erelation_2ERTC(A),B))).
% 6.84/7.10 Following clause subsumed by 1100 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|p(ap(c_2Erelation_2Ereflexive(A),ap(c_2Erelation_2ERTC(A),B))).
% 6.84/7.10 Following clause subsumed by 1101 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|p(ap(c_2Erelation_2Ereflexive(A),ap(c_2Erelation_2ERC(A),B))).
% 6.84/7.10 Following clause subsumed by 1079 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)| -p(ap(ap(B,C),D))|p(ap(ap(ap(c_2Erelation_2ETC(A),B),C),D)).
% 6.84/7.10 Following clause subsumed by 1083 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)| -p(ap(ap(B,C),D))|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D)).
% 6.84/7.10 Following clause subsumed by 1059 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)| -p(ap(ap(B,C),D))|p(ap(ap(ap(c_2Erelation_2ERC(A),B),C),D)).
% 6.84/7.10 Following clause subsumed by 1081 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),C)).
% 6.84/7.10 Following clause subsumed by 1407 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ETC(A),B),C),D))| -mem(E,A)| -p(ap(ap(B,C),E))| -p(ap(ap(ap(c_2Erelation_2ERTC(A),B),E),D)).
% 6.84/7.10 Following clause subsumed by 1414 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|ap(c_2Erelation_2ERC(A),ap(c_2Erelation_2ERC(A),B))=ap(c_2Erelation_2ERC(A),B).
% 6.84/7.10 Following clause subsumed by 1082 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))| -mem(E,A)| -p(ap(ap(B,C),E))| -p(ap(ap(ap(c_2Erelation_2ERTC(A),B),E),D)).
% 6.84/7.10 Following clause subsumed by 1427 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))|C!=D.
% 8.94/9.19 Following clause subsumed by 1348 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))| -p(ap(ap(ap(c_2Erelation_2ETC(A),B),C),D)).
% 8.94/9.19 Following clause subsumed by 1427 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))|C!=D.
% 8.94/9.19 Following clause subsumed by 1392 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))| -mem(E,A)| -p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),E))| -p(ap(ap(B,E),D)).
% 8.94/9.19 Following clause subsumed by 1098 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))| -mem(E,A)| -p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),E))| -p(ap(ap(ap(c_2Erelation_2ERTC(A),B),E),D)).
% 8.94/9.19 Following clause subsumed by 1079 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ETC(A),B),C),D))| -p(ap(ap(B,C),D)).
% 8.94/9.19 Following clause subsumed by 1079 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ETC(A),B),C),D))| -p(ap(ap(B,C),D)).
% 8.94/9.19 Following clause subsumed by 2046 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|p(ap(c_2Erelation_2EWF(A),ap(c_2Erelation_2ETC(A),B)))| -p(ap(c_2Erelation_2EWF(A),B)).
% 8.94/9.19 Following clause subsumed by 2137 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|ap(c_2Erelation_2ESC(A),ap(c_2Erelation_2Einv(A,A),B))=ap(c_2Erelation_2ESC(A),B).
% 8.94/9.19 Following clause subsumed by 2135 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|ap(c_2Erelation_2ERC(A),ap(c_2Erelation_2Einv(A,A),B))=ap(c_2Erelation_2Einv(A,A),ap(c_2Erelation_2ERC(A),B)).
% 8.94/9.19 Following clause subsumed by 2139 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|ap(c_2Erelation_2ETC(A),ap(c_2Erelation_2Einv(A,A),B))=ap(c_2Erelation_2Einv(A,A),ap(c_2Erelation_2ETC(A),B)).
% 8.94/9.19 Following clause subsumed by 2141 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))|ap(c_2Erelation_2EEQC(A),ap(c_2Erelation_2Einv(A,A),B))=ap(c_2Erelation_2EEQC(A),B).
% 8.94/9.19 Following clause subsumed by 2224 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,arr(B,bool)))| -mem(D,arr(A,arr(B,bool)))|C=D| -p(ap(ap(c_2Erelation_2ERSUBSET(A,B),C),D))| -p(ap(ap(c_2Erelation_2ERSUBSET(A,B),D),C)).
% 8.94/9.19 Following clause subsumed by 2255 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -p(ap(c_2Erelation_2EWeakLinearOrder(A),B))|p(ap(c_2Erelation_2EWeakOrder(A),B)).
% 8.94/9.19 Following clause subsumed by 2402 during input processing: 0 [] {-} -ne(A)| -mem(B,A)|ap(c_2Eoption_2ESOME(A),B)!=c_2Eoption_2ENONE(A).
% 8.94/9.19 Following clause subsumed by 2399 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)| -mem(G,A)|ap(c_2Eoption_2ESOME(A),F)!=ap(c_2Eoption_2ESOME(A),G)|F=G.
% 8.94/9.19 Following clause subsumed by 2400 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)| -mem(G,A)|ap(c_2Eoption_2ESOME(A),F)=ap(c_2Eoption_2ESOME(A),G)|F!=G.
% 8.94/9.19 Following clause subsumed by 2413 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)|ap(c_2Eoption_2ETHE(A),ap(c_2Eoption_2ESOME(A),F))=F.
% 8.94/9.19 Following clause subsumed by 2402 during input processing: 0 [flip.7] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)|ap(c_2Eoption_2ESOME(A),F)!=c_2Eoption_2ENONE(A).
% 8.94/9.19 Following clause subsumed by 2402 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)|ap(c_2Eoption_2ESOME(A),F)!=c_2Eoption_2ENONE(A).
% 8.94/9.19 Following clause subsumed by 2406 during input processing: 0 [propositional] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)|p(ap(c_2Eoption_2EIS__SOME(A),ap(c_2Eoption_2ESOME(A),F))).
% 9.32/9.56 Following clause subsumed by 2408 during input processing: 0 [propositional] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -p(ap(c_2Eoption_2EIS__SOME(A),c_2Eoption_2ENONE(A))).
% 9.32/9.56 Following clause subsumed by 2425 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))| -p(ap(c_2Eoption_2EIS__NONE(A),F))|F=c_2Eoption_2ENONE(A).
% 9.32/9.56 Following clause subsumed by 2426 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))|p(ap(c_2Eoption_2EIS__NONE(A),F))|F!=c_2Eoption_2ENONE(A).
% 9.32/9.56 Following clause subsumed by 2427 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))|p(ap(c_2Eoption_2EIS__SOME(A),F))|F=c_2Eoption_2ENONE(A).
% 9.32/9.56 Following clause subsumed by 2428 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))| -p(ap(c_2Eoption_2EIS__SOME(A),F))|F!=c_2Eoption_2ENONE(A).
% 9.32/9.56 Following clause subsumed by 2429 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))|ap(ap(ap(c_2Eoption_2Eoption__CASE(A,ty_2Eoption_2Eoption(A)),F),c_2Eoption_2ENONE(A)),c_2Eoption_2ESOME(A))=F.
% 9.32/9.56 Following clause subsumed by 2430 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))|ap(ap(ap(c_2Eoption_2Eoption__CASE(A,ty_2Eoption_2Eoption(A)),F),F),c_2Eoption_2ESOME(A))=F.
% 9.32/9.56 Following clause subsumed by 2385 during input processing: 0 [factor_simp,factor_simp] {-} -ne(A)| -ne(B)| -mem(F,B)| -mem(G,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))|ap(ap(ap(c_2Eoption_2Eoption__CASE(A,B),c_2Eoption_2ENONE(A)),F),G)=F.
% 9.32/9.56 Following clause subsumed by 2386 during input processing: 0 [factor_simp,factor_simp] {-} -ne(A)| -ne(B)| -mem(G,B)| -mem(H,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(F,A)|ap(ap(ap(c_2Eoption_2Eoption__CASE(A,B),ap(c_2Eoption_2ESOME(A),F)),G),H)=ap(H,F).
% 9.32/9.56 Following clause subsumed by 2403 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(F,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))| -mem(G,A)|ap(ap(c_2Eoption_2EOPTION__MAP(A,B),F),ap(c_2Eoption_2ESOME(A),G))=ap(c_2Eoption_2ESOME(B),ap(F,G)).
% 9.32/9.56 Following clause subsumed by 2404 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(F,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))|ap(ap(c_2Eoption_2EOPTION__MAP(A,B),F),c_2Eoption_2ENONE(A))=c_2Eoption_2ENONE(B).
% 9.32/9.56 Following clause subsumed by 2415 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(E,ty_2Eoption_2Eoption(A))|ap(c_2Eoption_2EOPTION__JOIN(A),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(A)))=c_2Eoption_2ENONE(A).
% 9.32/9.56 Following clause subsumed by 2416 during input processing: 0 [factor_simp] {-} -ne(A)| -ne(B)| -mem(C,B)| -mem(D,arr(A,B))| -mem(F,ty_2Eoption_2Eoption(A))|ap(c_2Eoption_2EOPTION__JOIN(A),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(A)),F))=F.
% 9.32/9.56 Following clause subsumed by 2471 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(B,A))| -mem(D,ty_2Eoption_2Eoption(B))|ap(ap(c_2Eoption_2EOPTION__MAP(B,A),C),D)!=c_2Eoption_2ENONE(A)|D=c_2Eoption_2ENONE(B).
% 9.32/9.56 Following clause subsumed by 2472 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(B,A))| -mem(D,ty_2Eoption_2Eoption(B))|ap(ap(c_2Eoption_2EOPTION__MAP(B,A),C),D)=c_2Eoption_2ENONE(A)|D!=c_2Eoption_2ENONE(B).
% 9.32/9.56 Following clause subsumed by 2672 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)| -mem(E,A)| -mem(F,B)|ap(ap(c_2Epair_2E_2C(A,B),C),D)!=ap(ap(c_2Epair_2E_2C(A,B),E),F)|C=E.
% 9.32/9.56 Following clause subsumed by 2673 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)| -mem(E,A)| -mem(F,B)|ap(ap(c_2Epair_2E_2C(A,B),C),D)!=ap(ap(c_2Epair_2E_2C(A,B),E),F)|D=F.
% 21.24/21.44 Following clause subsumed by 2674 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)| -mem(E,A)| -mem(F,B)|ap(ap(c_2Epair_2E_2C(A,B),C),D)=ap(ap(c_2Epair_2E_2C(A,B),E),F)|C!=E|D!=F.
% 21.24/21.44 Following clause subsumed by 2692 during input processing: 0 [] {-} -ne(A)| -ne(B)| -ne(C)| -mem(D,arr(A,arr(B,C)))| -mem(E,ty_2Epair_2Eprod(A,B))|ap(ap(c_2Epair_2EUNCURRY(A,B,C),D),E)=ap(ap(D,ap(c_2Epair_2EFST(A,B),E)),ap(c_2Epair_2ESND(A,B),E)).
% 21.24/21.44 Following clause subsumed by 2864 during input processing: 0 [] {-} -ne(A)| -ne(B)| -ne(C)| -mem(D,B)| -mem(E,C)| -mem(F,arr(B,arr(C,A)))|ap(ap(c_2Epair_2Epair__CASE(A,B,C),ap(ap(c_2Epair_2E_2C(B,C),D),E)),F)=ap(ap(F,D),E).
% 21.24/21.44 Following clause subsumed by 715 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(c_2Enum_2ESUC,A)!=ap(c_2Enum_2ESUC,B)|A=B.
% 21.24/21.44 Following clause subsumed by 3150 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,A)),ap(c_2Enum_2ESUC,B)))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.24/21.44 Following clause subsumed by 3149 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,A)),ap(c_2Enum_2ESUC,B)))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.24/21.44 Following clause subsumed by 3163 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,B))).
% 21.24/21.44 Following clause subsumed by 3164 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,B)))|A=B|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.24/21.44 Following clause subsumed by 3165 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,B)))|A!=B.
% 21.24/21.44 Following clause subsumed by 3163 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,B)))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.24/21.44 Following clause subsumed by 3164 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,B)))|A=B|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.24/21.44 Following clause subsumed by 3168 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|A!=B.
% 21.24/21.44 Following clause subsumed by 3162 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,A))).
% 21.24/21.44 Following clause subsumed by 3249 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,arr(A,bool)))| -mem(D,A)| -p(ap(c_2Eposet_2Eposet(A),ap(ap(c_2Epair_2E_2C(arr(A,bool),arr(A,arr(A,bool))),B),C)))| -p(ap(B,D))|p(ap(ap(C,D),D)).
% 21.24/21.44 Following clause subsumed by 3250 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,arr(A,bool)))| -mem(D,A)| -mem(E,A)| -p(ap(c_2Eposet_2Eposet(A),ap(ap(c_2Epair_2E_2C(arr(A,bool),arr(A,arr(A,bool))),B),C)))| -p(ap(B,D))| -p(ap(B,E))| -p(ap(ap(C,D),E))| -p(ap(ap(C,E),D))|D=E.
% 21.24/21.44 Following clause subsumed by 3251 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,arr(A,bool)))| -mem(D,A)| -mem(E,A)| -mem(F,A)| -p(ap(c_2Eposet_2Eposet(A),ap(ap(c_2Epair_2E_2C(arr(A,bool),arr(A,arr(A,bool))),B),C)))| -p(ap(B,D))| -p(ap(B,E))| -p(ap(B,F))| -p(ap(ap(C,D),E))| -p(ap(ap(C,E),F))|p(ap(ap(C,D),F)).
% 21.24/21.44 Following clause subsumed by 714 during input processing: 0 [flip.2] {-} -mem(A,ty_2Enum_2Enum)|ap(c_2Enum_2ESUC,A)!=c_2Enum_2E0.
% 21.24/21.44 Following clause subsumed by 3583 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,c_2Enum_2E0),B)=B.
% 21.24/21.44 Following clause subsumed by 3628 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,B),c_2Enum_2E0)=B.
% 21.24/21.44 Following clause subsumed by 3584 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,A)),B)=ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,A),B)).
% 21.30/21.49 Following clause subsumed by 3630 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),ap(c_2Enum_2ESUC,B))=ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,A),B)).
% 21.30/21.49 Following clause subsumed by 3631 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),B)=ap(ap(c_2Earithmetic_2E_2B,B),A).
% 21.30/21.49 Following clause subsumed by 3637 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|A=c_2Enum_2E0.
% 21.30/21.49 Following clause subsumed by 3638 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|A!=c_2Enum_2E0.
% 21.30/21.49 Following clause subsumed by 3150 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,A)),ap(c_2Enum_2ESUC,B)))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.30/21.49 Following clause subsumed by 3150 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,A)),ap(c_2Enum_2ESUC,B)))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.30/21.49 Following clause subsumed by 3149 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,A)),ap(c_2Enum_2ESUC,B)))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.30/21.49 Following clause subsumed by 3647 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,A)),B)).
% 21.30/21.49 Following clause subsumed by 3648 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,A)),B))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.30/21.49 Following clause subsumed by 3649 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))|p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(c_2Enum_2ESUC,B))).
% 21.30/21.49 Following clause subsumed by 3656 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|p(ap(ap(c_2Earithmetic_2E_3C_3D,B),A)).
% 21.30/21.49 Following clause subsumed by 3656 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))|p(ap(ap(c_2Eprim__rec_2E_3C,B),A)).
% 21.30/21.49 Following clause subsumed by 3666 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))| -p(ap(ap(c_2Eprim__rec_2E_3C,B),A)).
% 21.30/21.49 Following clause subsumed by 3666 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,B),A)).
% 21.30/21.49 Following clause subsumed by 3591 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2D,c_2Enum_2E0),A)=c_2Enum_2E0.
% 21.30/21.49 Following clause subsumed by 3594 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,c_2Enum_2E0),B)=c_2Enum_2E0.
% 21.30/21.49 Following clause subsumed by 3678 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,B),c_2Enum_2E0)=c_2Enum_2E0.
% 21.30/21.49 Following clause subsumed by 3681 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),B)=B.
% 21.30/21.49 Following clause subsumed by 3682 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,B),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))=B.
% 21.30/21.49 Following clause subsumed by 3596 during input processing: 0 [flip.3] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,A),B)),B)=ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,A)),B).
% 21.46/21.70 Following clause subsumed by 3680 during input processing: 0 [flip.3] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),ap(ap(c_2Earithmetic_2E_2A,A),B))=ap(ap(c_2Earithmetic_2E_2A,A),ap(c_2Enum_2ESUC,B)).
% 21.46/21.70 Following clause subsumed by 3683 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,A),B)=ap(ap(c_2Earithmetic_2E_2A,B),A).
% 21.46/21.70 Following clause subsumed by 3657 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),B)!=A|B=c_2Enum_2E0.
% 21.46/21.70 Following clause subsumed by 3645 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))| -p(ap(ap(c_2Eprim__rec_2E_3C,B),ap(c_2Enum_2ESUC,A))).
% 21.46/21.70 Following clause subsumed by 3709 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,A),C)),ap(ap(c_2Earithmetic_2E_2B,B),C)))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.46/21.70 Following clause subsumed by 3708 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,A),C)),ap(ap(c_2Earithmetic_2E_2B,B),C)))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.46/21.70 Following clause subsumed by 3709 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,A),C)),ap(ap(c_2Earithmetic_2E_2B,B),C)))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.46/21.70 Following clause subsumed by 3708 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,A),C)),ap(ap(c_2Earithmetic_2E_2B,B),C)))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 21.46/21.70 Following clause subsumed by 3603 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B)).
% 21.46/21.70 Following clause subsumed by 3712 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),C)!=ap(ap(c_2Earithmetic_2E_2B,B),C)|A=B.
% 21.46/21.70 Following clause subsumed by 3713 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),C)=ap(ap(c_2Earithmetic_2E_2B,B),C)|A!=B.
% 21.46/21.70 Following clause subsumed by 3655 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|A=B|p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|p(ap(ap(c_2Eprim__rec_2E_3C,B),A)).
% 21.46/21.70 Following clause subsumed by 3827 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(ap(c_2Earithmetic_2E_2A,A),B)))| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B)).
% 21.46/21.70 Following clause subsumed by 3836 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -p(ap(c_2Earithmetic_2EODD,A))| -p(ap(c_2Earithmetic_2EEVEN,A)).
% 21.46/21.70 Following clause subsumed by 3837 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|p(ap(c_2Earithmetic_2EODD,A))|p(ap(c_2Earithmetic_2EEVEN,A)).
% 21.46/21.70 Following clause subsumed by 3837 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|p(ap(c_2Earithmetic_2EEVEN,A))|p(ap(c_2Earithmetic_2EODD,A)).
% 21.46/21.70 Following clause subsumed by 3836 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -p(ap(c_2Earithmetic_2EEVEN,A))| -p(ap(c_2Earithmetic_2EODD,A)).
% 21.46/21.70 Following clause subsumed by 3870 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B))| -p(ap(c_2Earithmetic_2EEVEN,A))|p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2EEXP,A),B))).
% 21.46/21.70 Following clause subsumed by 3873 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B))| -p(ap(c_2Earithmetic_2EODD,A))|p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2EEXP,A),B))).
% 21.83/22.02 Following clause subsumed by 3604 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|A!=B|p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B)).
% 21.83/22.02 Following clause subsumed by 3732 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|A=B| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,B),A)).
% 21.83/22.02 Following clause subsumed by 3875 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,A),B)),ap(ap(c_2Earithmetic_2E_2B,A),C)))|p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C)).
% 21.83/22.02 Following clause subsumed by 3876 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,A),B)),ap(ap(c_2Earithmetic_2E_2B,A),C)))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C)).
% 21.83/22.02 Following clause subsumed by 3714 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,B),A)),ap(ap(c_2Earithmetic_2E_2B,C),A)))|p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C)).
% 21.83/22.02 Following clause subsumed by 3715 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,B),A)),ap(ap(c_2Earithmetic_2E_2B,C),A)))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C)).
% 21.83/22.02 Following clause subsumed by 3791 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,B)),A)).
% 21.83/22.02 Following clause subsumed by 3792 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,B)),A)).
% 21.83/22.02 Following clause subsumed by 3721 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,A),B)),ap(ap(c_2Earithmetic_2E_2A,C),B)))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),C)).
% 21.83/22.02 Following clause subsumed by 3754 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,A),B)),C)=ap(ap(c_2Earithmetic_2E_2D,A),ap(ap(c_2Earithmetic_2E_2B,B),C)).
% 21.83/22.02 Following clause subsumed by 3767 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(ap(c_2Earithmetic_2E_2D,B),C)))|p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,A),C)),B)).
% 21.83/22.02 Following clause subsumed by 3667 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),c_2Enum_2E0))|A=c_2Enum_2E0.
% 21.83/22.02 Following clause subsumed by 3668 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,A),c_2Enum_2E0))|A!=c_2Enum_2E0.
% 21.83/22.02 Following clause subsumed by 3970 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B))|p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EMOD,A),B)),B)).
% 21.83/22.02 Following clause subsumed by 4002 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,B),A)),A)=ap(ap(c_2Earithmetic_2EMOD,B),A).
% 21.83/22.02 Following clause subsumed by 4003 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,A),B)),A)=ap(ap(c_2Earithmetic_2EMOD,B),A).
% 21.83/22.02 Following clause subsumed by 3979 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B))|ap(ap(c_2Earithmetic_2EMOD,A),B)=A| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 22.44/22.66 Following clause subsumed by 4066 during input processing: 0 [flip.5] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|ap(ap(c_2Earithmetic_2EMOD,ap(c_2Enum_2ESUC,B)),A)=ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2EMOD,B),A))|ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2EDIV,B),A))),A)=ap(c_2Enum_2ESUC,B).
% 22.44/22.66 Following clause subsumed by 4069 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A))|ap(ap(c_2Earithmetic_2EMOD,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A)=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)).
% 22.44/22.66 Following clause subsumed by 4073 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,B),C)),A)=ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2EMOD,B),A)),C)| -p(ap(ap(c_2Eprim__rec_2E_3C,C),ap(ap(c_2Earithmetic_2E_2D,A),ap(ap(c_2Earithmetic_2EMOD,B),A)))).
% 22.44/22.66 Following clause subsumed by 4136 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EEXP,A),B)),ap(ap(c_2Earithmetic_2EEXP,A),C)))| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C)).
% 22.44/22.66 Following clause subsumed by 4151 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,A),ap(ap(c_2Earithmetic_2EEXP,B),A)))| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),B)).
% 22.44/22.66 Following clause subsumed by 4297 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EABS__DIFF,A),B)=ap(ap(c_2Earithmetic_2EABS__DIFF,B),A).
% 22.44/22.66 Following clause subsumed by 3618 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,A))| -mem(C,A)|ap(ap(ap(c_2Earithmetic_2EFUNPOW(A),B),c_2Enum_2E0),C)=C.
% 22.44/22.66 Following clause subsumed by 3620 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)| -p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A),B),c_2Enum_2E0),C),D))|C=D.
% 22.44/22.66 Following clause subsumed by 3621 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A),B),c_2Enum_2E0),C),D))|C!=D.
% 22.44/22.66 Following clause subsumed by 4328 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,ty_2Enum_2Enum)| -mem(D,ty_2Enum_2Enum)| -mem(E,A)| -mem(F,A)|p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A),B),ap(ap(c_2Earithmetic_2E_2B,C),D)),E),F))| -mem(G,A)| -p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A),B),C),E),G))| -p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A),B),D),G),F)).
% 22.44/22.66 Following clause subsumed by 4339 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,A)| -mem(D,A)|p(ap(ap(ap(c_2Erelation_2ERTC(A),B),C),D))| -mem(E,ty_2Enum_2Enum)| -p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A),B),E),C),D)).
% 22.44/22.66 Following clause subsumed by 4367 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2A,A),B)))| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B))| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A)).
% 22.44/22.66 Following clause subsumed by 3637 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(ap(c_2Earithmetic_2EMODEQ,A),B),C))|A=c_2Enum_2E0|p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A)).
% 22.44/22.66 Following clause subsumed by 4410 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(ap(c_2Earithmetic_2EMODEQ,A),B),C))| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))|ap(ap(c_2Earithmetic_2EMOD,B),A)!=ap(ap(c_2Earithmetic_2EMOD,C),A).
% 22.92/23.11 Following clause subsumed by 4409 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),A))| -p(ap(ap(ap(c_2Earithmetic_2EMODEQ,A),B),C))|ap(ap(c_2Earithmetic_2EMOD,B),A)=ap(ap(c_2Earithmetic_2EMOD,C),A).
% 22.92/23.11 Following clause subsumed by 4421 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(ap(c_2Earithmetic_2EMODEQ,A),B),C))| -p(ap(ap(ap(c_2Earithmetic_2EMODEQ,A),C),B)).
% 22.92/23.11 Following clause subsumed by 4468 during input processing: 0 [] {-} -mem(A,arr(ty_2Enum_2Enum,bool))| -mem(B,ty_2Enum_2Enum)| -p(ap(A,B))|p(ap(A,ap(c_2Ewhile_2ELEAST,A))).
% 22.92/23.11 Following clause subsumed by 4468 during input processing: 0 [] {-} -mem(A,arr(ty_2Enum_2Enum,bool))| -mem(B,ty_2Enum_2Enum)| -p(ap(A,B))|p(ap(A,ap(c_2Ewhile_2ELEAST,A))).
% 22.92/23.11 Following clause subsumed by 4469 during input processing: 0 [factor_simp,factor_simp] {-} -mem(A,arr(ty_2Enum_2Enum,bool))| -mem(C,ty_2Enum_2Enum)| -p(ap(A,C))| -p(ap(ap(c_2Eprim__rec_2E_3C,C),ap(c_2Ewhile_2ELEAST,A))).
% 22.92/23.11 Following clause subsumed by 4468 during input processing: 0 [] {-} -mem(A,arr(ty_2Enum_2Enum,bool))| -mem(B,ty_2Enum_2Enum)| -p(ap(A,B))|p(ap(A,ap(c_2Ewhile_2ELEAST,A))).
% 22.92/23.11 Following clause subsumed by 4469 during input processing: 0 [factor_simp,factor_simp] {-} -mem(A,arr(ty_2Enum_2Enum,bool))| -mem(C,ty_2Enum_2Enum)| -p(ap(A,C))| -p(ap(ap(c_2Eprim__rec_2E_3C,C),ap(c_2Ewhile_2ELEAST,A))).
% 22.92/23.11 Following clause subsumed by 4493 during input processing: 0 [] {-} -mem(A,arr(ty_2Enum_2Enum,bool))| -mem(B,arr(ty_2Eoption_2Eoption(ty_2Enum_2Enum),bool))| -p(ap(B,c_2Eoption_2ENONE(ty_2Enum_2Enum)))| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,C),$f583(A,B)))| -p(ap(A,C))|p(ap(B,ap(c_2Ewhile_2EOLEAST,A))).
% 22.92/23.11 Following clause subsumed by 3583 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,c_2Enum_2E0),A)=A.
% 22.92/23.11 Following clause subsumed by 3628 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2B,A),c_2Enum_2E0)=A.
% 22.92/23.11 Following clause subsumed by 3594 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,c_2Enum_2E0),A)=c_2Enum_2E0.
% 22.92/23.11 Following clause subsumed by 3678 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,A),c_2Enum_2E0)=c_2Enum_2E0.
% 22.92/23.11 Following clause subsumed by 3591 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2D,c_2Enum_2E0),A)=c_2Enum_2E0.
% 22.92/23.11 Following clause subsumed by 3669 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2D,A),c_2Enum_2E0)=A.
% 22.92/23.11 Following clause subsumed by 3597 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EEXP,A),c_2Enum_2E0)=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)).
% 22.92/23.11 Following clause subsumed by 4555 during input processing: 0 [flip.2] {-} -mem(A,ty_2Enum_2Enum)|ap(c_2Earithmetic_2ENUMERAL,A)!=c_2Enum_2E0|A=c_2Earithmetic_2EZERO.
% 22.92/23.11 Following clause subsumed by 4556 during input processing: 0 [flip.2] {-} -mem(A,ty_2Enum_2Enum)|ap(c_2Earithmetic_2ENUMERAL,A)=c_2Enum_2E0|A!=c_2Earithmetic_2EZERO.
% 22.92/23.11 Following clause subsumed by 3147 during input processing: 0 [propositional] {-} -mem(A,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,A),c_2Enum_2E0)).
% 22.92/23.11 Following clause subsumed by 3651 during input processing: 0 [propositional] {-} -mem(A,ty_2Enum_2Enum)|p(ap(ap(c_2Earithmetic_2E_3C_3D,c_2Enum_2E0),A)).
% 22.92/23.11 Following clause subsumed by 3613 during input processing: 0 [] {-} -p(ap(c_2Earithmetic_2EODD,c_2Enum_2E0)).
% 22.92/23.11 Following clause subsumed by 4611 during input processing: 0 [propositional,factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(c_2Earithmetic_2EBIT1,B)!=c_2Earithmetic_2EZERO.
% 22.92/23.11 Following clause subsumed by 4613 during input processing: 0 [propositional,factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(c_2Earithmetic_2EBIT2,B)!=c_2Earithmetic_2EZERO.
% 23.51/23.73 Following clause subsumed by 4670 during input processing: 0 [factor_simp,factor_simp] {-} -mem(D,ty_2Enum_2Enum)| -mem(B,bool)|ap(ap(ap(c_2Enumeral_2EiSUB,B),c_2Earithmetic_2EZERO),D)=c_2Earithmetic_2EZERO.
% 23.51/23.73 Following clause subsumed by 3618 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,A))| -mem(C,A)| -mem(D,ty_2Enum_2Enum)|ap(ap(ap(c_2Earithmetic_2EFUNPOW(A),B),c_2Enum_2E0),C)=C.
% 23.51/23.73 Following clause subsumed by 4214 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EMIN,c_2Enum_2E0),B)=c_2Enum_2E0.
% 23.51/23.73 Following clause subsumed by 4213 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EMIN,B),c_2Enum_2E0)=c_2Enum_2E0.
% 23.51/23.73 Following clause subsumed by 4216 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EMAX,c_2Enum_2E0),B)=B.
% 23.51/23.73 Following clause subsumed by 4215 during input processing: 0 [factor_simp] {-} -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EMAX,B),c_2Enum_2E0)=B.
% 23.51/23.73 Following clause subsumed by 4712 during input processing: 0 [factor_simp,factor_simp] {-} -mem(C,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,c_2Earithmetic_2EZERO),C)=c_2Earithmetic_2EZERO.
% 23.51/23.73 Following clause subsumed by 4714 during input processing: 0 [factor_simp,factor_simp] {-} -mem(C,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2A,C),c_2Earithmetic_2EZERO)=c_2Earithmetic_2EZERO.
% 23.51/23.73 Following clause subsumed by 4912 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -mem(D,ty_2Enum_2Enum)|ap(ap(c_2Eind__type_2ENUMPAIR,A),B)!=ap(ap(c_2Eind__type_2ENUMPAIR,C),D)|A=C.
% 23.51/23.73 Following clause subsumed by 4138 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A))| -p(ap(ap(c_2Eprim__rec_2E_3C,B),C))|p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EEXP,A),B)),ap(ap(c_2Earithmetic_2EEXP,A),C))).
% 23.51/23.73 Following clause subsumed by 4137 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A))|p(ap(ap(c_2Eprim__rec_2E_3C,B),C))| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EEXP,A),B)),ap(ap(c_2Earithmetic_2EEXP,A),C))).
% 23.51/23.73 Following clause subsumed by 4136 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C))|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EEXP,A),B)),ap(ap(c_2Earithmetic_2EEXP,A),C))).
% 23.51/23.73 Following clause subsumed by 4135 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),A))|p(ap(ap(c_2Earithmetic_2E_3C_3D,B),C))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EEXP,A),B)),ap(ap(c_2Earithmetic_2EEXP,A),C))).
% 23.51/23.73 Following clause subsumed by 4158 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),C))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B))|p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EEXP,A),C)),ap(ap(c_2Earithmetic_2EEXP,B),C))).
% 23.51/23.73 Following clause subsumed by 4156 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),C))|p(ap(ap(c_2Eprim__rec_2E_3C,A),B))| -p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EEXP,A),C)),ap(ap(c_2Earithmetic_2EEXP,B),C))).
% 23.51/23.73 Following clause subsumed by 4160 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),C))| -p(ap(ap(c_2Earithmetic_2E_3C_3D,A),B))|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EEXP,A),C)),ap(ap(c_2Earithmetic_2EEXP,B),C))).
% 24.94/25.17 Following clause subsumed by 4171 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EEXP,ap(ap(c_2Earithmetic_2EEXP,A),B)),C)=ap(ap(c_2Earithmetic_2EEXP,A),ap(ap(c_2Earithmetic_2E_2A,B),C)).
% 24.94/25.17 Following clause subsumed by 5128 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)|p(ap(ap(ap(c_2Egcd_2Eis__gcd,A),B),C))| -p(ap(ap(ap(c_2Egcd_2Eis__gcd,B),A),C)).
% 24.94/25.17 Following clause subsumed by 5154 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Egcd_2Egcd,c_2Enum_2E0),A)=A.
% 24.94/25.17 Following clause subsumed by 5154 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Egcd_2Egcd,c_2Enum_2E0),A)=A.
% 24.94/25.17 Following clause subsumed by 5175 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Egcd_2Egcd,A),ap(ap(c_2Earithmetic_2E_2B,A),B))=ap(ap(c_2Egcd_2Egcd,A),B).
% 24.94/25.17 Following clause subsumed by 5177 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(c_2Egcd_2Egcd,ap(ap(c_2Earithmetic_2E_2B,A),B)),A)=ap(ap(c_2Egcd_2Egcd,A),B).
% 24.94/25.17 Following clause subsumed by 5327 during input processing: 0 [flip.2] {-} -mem(A,ty_2Enum_2Enum)|ap(c_2Enumpair_2Etri,A)!=c_2Enum_2E0|A=c_2Enum_2E0.
% 24.94/25.17 Following clause subsumed by 5328 during input processing: 0 [flip.2] {-} -mem(A,ty_2Enum_2Enum)|ap(c_2Enumpair_2Etri,A)=c_2Enum_2E0|A!=c_2Enum_2E0.
% 24.94/25.17 Following clause subsumed by 5329 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enumpair_2Etri,A)),ap(c_2Enumpair_2Etri,B)))| -p(ap(ap(c_2Eprim__rec_2E_3C,A),B)).
% 24.94/25.17 Following clause subsumed by 3752 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,A)),A)=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)).
% 24.94/25.17 Following clause subsumed by 4072 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)| -p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),B))|p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EMOD,A),B)),A)).
% 24.94/25.17 Following clause subsumed by 5490 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EMOD,A),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))|ap(ap(c_2Earithmetic_2EMOD,A),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))=c_2Enum_2E0.
% 24.94/25.17 Following clause subsumed by 5491 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)|ap(ap(c_2Earithmetic_2EMOD,A),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))!=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))|ap(ap(c_2Earithmetic_2EMOD,A),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))!=c_2Enum_2E0.
% 24.94/25.17 Following clause subsumed by 5519 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(ap(c_2Ebit_2EBITS,A),A),B)=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))|ap(ap(ap(c_2Ebit_2EBITS,A),A),B)=c_2Enum_2E0.
% 24.94/25.17 Following clause subsumed by 5520 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(ap(c_2Ebit_2EBITS,A),A),B)!=ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))|ap(ap(ap(c_2Ebit_2EBITS,A),A),B)!=c_2Enum_2E0.
% 24.94/25.17 Following clause subsumed by 5673 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,arr(A,bool))| -p(ap(ap(c_2Ebool_2EIN(A),B),C))|p(ap(C,B)).
% 24.94/25.17 Following clause subsumed by 5674 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,arr(A,bool))|p(ap(ap(c_2Ebool_2EIN(A),B),C))| -p(ap(C,B)).
% 24.94/25.17 Following clause subsumed by 5678 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|B!=C| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(A),D),C))| -p(ap(ap(c_2Ebool_2EIN(A),D),B)).
% 25.60/25.85 Following clause subsumed by 5679 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|B!=C| -mem(D,A)| -p(ap(ap(c_2Ebool_2EIN(A),D),C))|p(ap(ap(c_2Ebool_2EIN(A),D),B)).
% 25.60/25.85 Following clause subsumed by 5748 during input processing: 0 [flip.2] {-} -ne(A)|c_2Epred__set_2EUNIV(A)!=c_2Epred__set_2EEMPTY(A).
% 25.60/25.85 Following clause subsumed by 5751 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|B!=c_2Epred__set_2EUNIV(A)| -mem(C,A)|p(ap(ap(c_2Ebool_2EIN(A),C),B)).
% 25.60/25.85 Following clause subsumed by 5752 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))| -mem(D,A)| -p(ap(ap(c_2Ebool_2EIN(A),D),B))|p(ap(ap(c_2Ebool_2EIN(A),D),C)).
% 25.60/25.85 Following clause subsumed by 5762 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),C),B))|B=C.
% 25.60/25.85 Following clause subsumed by 5769 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))|B!=C.
% 25.60/25.85 Following clause subsumed by 5770 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(A),C),B))|B!=C.
% 25.60/25.85 Following clause subsumed by 5847 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))|ap(ap(c_2Epred__set_2EINTER(A),B),C)=B.
% 25.60/25.85 Following clause subsumed by 5864 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|p(ap(ap(c_2Epred__set_2EDISJOINT(A),B),C))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),C),B)).
% 25.60/25.85 Following clause subsumed by 5860 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),B),C))| -mem(D,A)| -p(ap(ap(c_2Ebool_2EIN(A),D),B))| -p(ap(ap(c_2Ebool_2EIN(A),D),C)).
% 25.60/25.85 Following clause subsumed by 5871 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),B),B))|B=c_2Epred__set_2EEMPTY(A).
% 25.60/25.85 Following clause subsumed by 5870 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(ap(c_2Epred__set_2EDISJOINT(A),B),B))|B!=c_2Epred__set_2EEMPTY(A).
% 25.60/25.85 Following clause subsumed by 5872 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -mem(D,arr(A,bool))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),ap(ap(c_2Epred__set_2EUNION(A),B),C)),D))|p(ap(ap(c_2Epred__set_2EDISJOINT(A),B),D)).
% 25.60/25.85 Following clause subsumed by 5873 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -mem(D,arr(A,bool))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),ap(ap(c_2Epred__set_2EUNION(A),B),C)),D))|p(ap(ap(c_2Epred__set_2EDISJOINT(A),C),D)).
% 25.60/25.85 Following clause subsumed by 5874 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -mem(D,arr(A,bool))|p(ap(ap(c_2Epred__set_2EDISJOINT(A),ap(ap(c_2Epred__set_2EUNION(A),B),C)),D))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),B),D))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),C),D)).
% 25.60/25.85 Following clause subsumed by 5929 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,arr(A,bool))| -p(ap(ap(c_2Ebool_2EIN(A),B),C))|ap(ap(c_2Epred__set_2EINSERT(A),B),C)=C.
% 25.60/25.85 Following clause subsumed by 5934 during input processing: 0 [flip.4] {-} -ne(A)| -mem(B,A)| -mem(C,arr(A,bool))|ap(ap(c_2Epred__set_2EINSERT(A),B),C)!=c_2Epred__set_2EEMPTY(A).
% 25.60/25.85 Following clause subsumed by 5976 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)|p(ap(ap(c_2Ebool_2EIN(A),C),B))|ap(ap(c_2Epred__set_2EDELETE(A),B),C)=B.
% 25.60/25.85 Following clause subsumed by 5970 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(A),C),B))|p(ap(ap(c_2Ebool_2EIN(A),D),B))| -p(ap(ap(c_2Ebool_2EIN(A),C),ap(ap(c_2Epred__set_2EDELETE(A),B),D)))|p(ap(ap(c_2Ebool_2EIN(A),D),ap(ap(c_2Epred__set_2EDELETE(A),B),C))).
% 27.62/27.81 Following clause subsumed by 5970 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(A),C),B))|p(ap(ap(c_2Ebool_2EIN(A),D),B))|p(ap(ap(c_2Ebool_2EIN(A),C),ap(ap(c_2Epred__set_2EDELETE(A),B),D)))| -p(ap(ap(c_2Ebool_2EIN(A),D),ap(ap(c_2Epred__set_2EDELETE(A),B),C))).
% 27.62/27.81 Following clause subsumed by 5978 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)| -p(ap(ap(c_2Ebool_2EIN(A),C),B))| -p(ap(ap(c_2Ebool_2EIN(A),D),B))|p(ap(ap(c_2Ebool_2EIN(A),C),ap(ap(c_2Epred__set_2EDELETE(A),B),D)))| -p(ap(ap(c_2Ebool_2EIN(A),D),ap(ap(c_2Epred__set_2EDELETE(A),B),C))).
% 27.62/27.81 Following clause subsumed by 5970 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)| -p(ap(ap(c_2Ebool_2EIN(A),C),B))|p(ap(ap(c_2Ebool_2EIN(A),D),B))| -p(ap(ap(c_2Ebool_2EIN(A),C),ap(ap(c_2Epred__set_2EDELETE(A),B),D)))| -p(ap(ap(c_2Ebool_2EIN(A),D),ap(ap(c_2Epred__set_2EDELETE(A),B),C))).
% 27.62/27.81 Following clause subsumed by 5979 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(A),C),B))| -p(ap(ap(c_2Ebool_2EIN(A),D),B))|p(ap(ap(c_2Ebool_2EIN(A),C),ap(ap(c_2Epred__set_2EDELETE(A),B),D)))|p(ap(ap(c_2Ebool_2EIN(A),D),ap(ap(c_2Epred__set_2EDELETE(A),B),C))).
% 27.62/27.81 Following clause subsumed by 5970 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(A),C),B))| -p(ap(ap(c_2Ebool_2EIN(A),D),B))| -p(ap(ap(c_2Ebool_2EIN(A),C),ap(ap(c_2Epred__set_2EDELETE(A),B),D)))| -p(ap(ap(c_2Ebool_2EIN(A),D),ap(ap(c_2Epred__set_2EDELETE(A),B),C))).
% 27.62/27.81 Following clause subsumed by 5779 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2EPSUBSET(A),B),C))|p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C)).
% 27.62/27.81 Following clause subsumed by 6003 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -mem(D,A)|p(ap(ap(c_2Epred__set_2EDISJOINT(A),ap(ap(c_2Epred__set_2EDELETE(A),B),D)),C))| -p(ap(ap(c_2Epred__set_2EDISJOINT(A),ap(ap(c_2Epred__set_2EDELETE(A),C),D)),B)).
% 27.62/27.81 Following clause subsumed by 6037 during input processing: 0 [flip.3] {-} -ne(A)| -mem(B,A)|ap(ap(c_2Epred__set_2EINSERT(A),B),c_2Epred__set_2EEMPTY(A))!=c_2Epred__set_2EEMPTY(A).
% 27.62/27.81 Following clause subsumed by 6111 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(ap(ap(c_2Epred__set_2EINJ(A,B),C),D),E))| -mem(F,A)| -p(ap(ap(c_2Ebool_2EIN(A),F),D))|p(ap(ap(c_2Ebool_2EIN(B),ap(C,F)),E)).
% 27.62/27.81 Following clause subsumed by 6112 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(ap(ap(c_2Epred__set_2EINJ(A,B),C),D),E))| -mem(F,A)| -mem(G,A)| -p(ap(ap(c_2Ebool_2EIN(A),F),D))| -p(ap(ap(c_2Ebool_2EIN(A),G),D))|ap(C,F)!=ap(C,G)|F=G.
% 27.62/27.81 Following clause subsumed by 6225 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,bool))| -mem(D,arr(B,bool))| -mem(E,arr(A,B))| -mem(F,A)| -p(ap(ap(c_2Ebool_2EIN(arr(A,B)),E),ap(ap(c_2Epred__set_2EFUNSET(A,B),C),D)))| -p(ap(ap(c_2Ebool_2EIN(A),F),C))|p(ap(ap(c_2Ebool_2EIN(B),ap(E,F)),D)).
% 27.62/27.81 Following clause subsumed by 6277 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(ap(ap(c_2Epred__set_2EINJ(A,B),C),D),E))| -mem(F,A)| -mem(G,B)|ap(ap(ap(c_2Epred__set_2ELINV__OPT(A,B),C),D),G)!=ap(c_2Eoption_2ESOME(A),F)|p(ap(ap(c_2Ebool_2EIN(A),F),D)).
% 27.62/27.81 Following clause subsumed by 6405 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(A),ap(c_2Epred__set_2EREST(A),B)))| -p(ap(c_2Epred__set_2EFINITE(A),B)).
% 27.62/27.81 Following clause subsumed by 6411 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(c_2Epred__set_2EFINITE(A),B))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),C),B))|p(ap(c_2Epred__set_2EFINITE(A),C)).
% 27.62/27.81 Following clause subsumed by 6417 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))|mem($f746(A,B,C),B)| -mem(D,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),D)).
% 28.40/28.64 Following clause subsumed by 6417 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -p(ap(c_2Epred__set_2EFINITE(A),ap(c_2Epred__set_2EGSPEC(A,A),f274(B,A,$f746(A,B,C),C))))| -mem(D,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),D)).
% 28.40/28.64 Following clause subsumed by 6417 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))|mem($f748(A,B,C),A)| -mem(D,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),D)).
% 28.40/28.64 Following clause subsumed by 6417 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))|mem($f747(A,B,C),A)| -mem(D,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),D)).
% 28.40/28.64 Following clause subsumed by 6417 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))|ap(C,$f748(A,B,C))=ap(C,$f747(A,B,C))|$f748(A,B,C)=$f747(A,B,C)| -mem(D,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),D)).
% 28.40/28.64 Following clause subsumed by 6417 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))|ap(C,$f748(A,B,C))!=ap(C,$f747(A,B,C))|$f748(A,B,C)!=$f747(A,B,C)| -mem(D,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),D)).
% 28.40/28.64 Following clause subsumed by 6432 during input processing: 0 [] {-} -ne(A)|ap(c_2Epred__set_2ECARD(A),c_2Epred__set_2EEMPTY(A))=c_2Enum_2E0.
% 28.40/28.64 Following clause subsumed by 6433 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -p(ap(c_2Epred__set_2EFINITE(A),B))| -mem(C,A)|ap(c_2Epred__set_2ECARD(A),ap(ap(c_2Epred__set_2EINSERT(A),C),B))=ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2EIN(A),C),B)),ap(c_2Epred__set_2ECARD(A),B)),ap(c_2Enum_2ESUC,ap(c_2Epred__set_2ECARD(A),B))).
% 28.40/28.64 Following clause subsumed by 6416 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -p(ap(c_2Epred__set_2ESING(A),B))|p(ap(c_2Epred__set_2EFINITE(A),B)).
% 28.40/28.64 Following clause subsumed by 6451 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(c_2Epred__set_2EFINITE(A),D))| -p(ap(ap(ap(c_2Epred__set_2EBIJ(A,B),C),D),E))|p(ap(c_2Epred__set_2EFINITE(B),E)).
% 28.40/28.64 Following clause subsumed by 6454 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(c_2Epred__set_2EFINITE(A),D))| -p(ap(ap(ap(c_2Epred__set_2EBIJ(A,B),C),D),E))|ap(c_2Epred__set_2ECARD(A),D)=ap(c_2Epred__set_2ECARD(B),E).
% 28.40/28.64 Following clause subsumed by 6454 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,bool))| -p(ap(c_2Epred__set_2EFINITE(A),C))| -mem(D,arr(B,bool))| -mem(E,arr(A,B))| -p(ap(ap(ap(c_2Epred__set_2EBIJ(A,B),E),C),D))| -p(ap(c_2Epred__set_2EFINITE(B),D))|ap(c_2Epred__set_2ECARD(A),C)=ap(c_2Epred__set_2ECARD(B),D).
% 28.40/28.64 Following clause subsumed by 6460 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,bool))| -mem(D,arr(A,B))| -mem(E,arr(B,bool))| -p(ap(c_2Epred__set_2EFINITE(A),C))| -p(ap(ap(ap(c_2Epred__set_2ESURJ(A,B),D),C),E))|p(ap(c_2Epred__set_2EFINITE(B),E)).
% 28.40/28.64 Following clause subsumed by 6467 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(ap(ap(c_2Epred__set_2EINJ(A,B),C),D),E))| -p(ap(c_2Epred__set_2EFINITE(A),D))|ap(c_2Epred__set_2ECARD(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D))=ap(c_2Epred__set_2ECARD(A),D).
% 28.40/28.64 Following clause subsumed by 6411 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(A),B))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))| -p(ap(c_2Epred__set_2EFINITE(A),C)).
% 28.40/28.64 Following clause subsumed by 6425 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))| -p(ap(ap(ap(c_2Epred__set_2EINJ(A,B),C),D),E))|p(ap(c_2Epred__set_2EFINITE(A),D))| -p(ap(c_2Epred__set_2EFINITE(B),E)).
% 30.03/30.21 Following clause subsumed by 6710 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,bool))| -mem(D,arr(B,bool))|p(ap(c_2Epred__set_2EFINITE(ty_2Epair_2Eprod(A,B)),ap(ap(c_2Epred__set_2ECROSS(A,B),C),D)))| -p(ap(c_2Epred__set_2EFINITE(A),C))| -p(ap(c_2Epred__set_2EFINITE(B),D)).
% 30.03/30.21 Following clause subsumed by 6741 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|ap(ap(c_2Epred__set_2EINTER(A),ap(c_2Epred__set_2ECOMPL(A),B)),B)=c_2Epred__set_2EEMPTY(A).
% 30.03/30.21 Following clause subsumed by 6886 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,arr(A,bool)))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2Eequiv__on(A),B),C))| -mem(D,A)| -mem(E,A)| -p(ap(ap(c_2Ebool_2EIN(A),D),C))| -p(ap(ap(c_2Ebool_2EIN(A),E),C))|p(ap(ap(B,D),E))| -p(ap(ap(B,E),D)).
% 30.03/30.21 Following clause subsumed by 5769 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|B!=C|p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C)).
% 30.03/30.21 Following clause subsumed by 5770 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|B!=C|p(ap(ap(c_2Epred__set_2ESUBSET(A),C),B)).
% 30.03/30.21 Following clause subsumed by 5762 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|B=C| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),C),B)).
% 30.03/30.21 Following clause subsumed by 5779 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2EPSUBSET(A),B),C))|p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C)).
% 30.03/30.21 Following clause subsumed by 6703 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,arr(A,bool))| -mem(E,arr(B,bool))|ap(ap(c_2Epred__set_2ECROSS(A,B),c_2Epred__set_2EEMPTY(A)),E)=c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A,B)).
% 30.03/30.21 Following clause subsumed by 6406 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(c_2Epred__set_2EFINITE(A),B))| -p(ap(c_2Epred__set_2EFINITE(A),ap(c_2Epred__set_2EREST(A),B))).
% 30.03/30.21 Following clause subsumed by 7107 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|ap(ap(c_2Epred__set_2Echooser(A),B),c_2Enum_2E0)=ap(c_2Epred__set_2ECHOICE(A),B).
% 30.03/30.21 Following clause subsumed by 7125 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C))| -p(ap(c_2Epred__set_2Ecountable(A),C))|p(ap(c_2Epred__set_2Ecountable(A),B)).
% 30.03/30.21 Following clause subsumed by 7150 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|p(ap(c_2Epred__set_2Ecountable(A),ap(ap(c_2Epred__set_2EUNION(A),B),C)))| -p(ap(c_2Epred__set_2Ecountable(A),B))| -p(ap(c_2Epred__set_2Ecountable(A),C)).
% 30.03/30.21 Following clause subsumed by 7126 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,B))| -mem(D,arr(A,bool))| -p(ap(ap(ap(c_2Epred__set_2EINJ(A,B),C),D),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))|p(ap(c_2Epred__set_2Ecountable(B),ap(ap(c_2Epred__set_2EIMAGE(A,B),C),D)))| -p(ap(c_2Epred__set_2Ecountable(A),D)).
% 30.03/30.21 Following clause subsumed by 7143 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,arr(A,bool))| -mem(D,arr(B,bool))|p(ap(c_2Epred__set_2Ecountable(ty_2Epair_2Eprod(A,B)),ap(ap(c_2Epred__set_2ECROSS(A,B),C),D)))| -p(ap(c_2Epred__set_2Ecountable(A),C))| -p(ap(c_2Epred__set_2Ecountable(B),D)).
% 30.03/30.21 Following clause subsumed by 7133 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(c_2Epred__set_2Ecountable(A),B))| -p(ap(c_2Epred__set_2EFINITE(A),B)).
% 30.03/30.21 Following clause subsumed by 7123 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))|p(ap(c_2Epred__set_2Ecountable(A),B))|B!=c_2Epred__set_2EEMPTY(A).
% 30.03/30.21 Following clause subsumed by 5848 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|ap(ap(c_2Epred__set_2EINTER(A),B),C)!=B|p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C)).
% 30.03/30.21 Following clause subsumed by 5847 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|ap(ap(c_2Epred__set_2EINTER(A),B),C)=B| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),C)).
% 30.03/30.21 Following clause subsumed by 5849 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))|ap(ap(c_2Epred__set_2EINTER(A),B),C)=C| -p(ap(ap(c_2Epred__set_2ESUBSET(A),C),B)).
% 32.71/32.95 Following clause subsumed by 5989 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,arr(A,bool))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),ap(ap(c_2Epred__set_2EDELETE(A),B),C)),D))|p(ap(ap(c_2Epred__set_2ESUBSET(A),B),ap(ap(c_2Epred__set_2EINSERT(A),C),D))).
% 32.71/32.95 Following clause subsumed by 5988 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,A)| -mem(D,arr(A,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(A),ap(ap(c_2Epred__set_2EDELETE(A),B),C)),D))| -p(ap(ap(c_2Epred__set_2ESUBSET(A),B),ap(ap(c_2Epred__set_2EINSERT(A),C),D))).
% 32.71/32.95 Following clause subsumed by 5912 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)| -mem(D,arr(A,bool))| -p(ap(ap(c_2Ebool_2EIN(A),B),ap(ap(c_2Epred__set_2EINSERT(A),C),D)))|B=C|p(ap(ap(c_2Ebool_2EIN(A),B),D)).
% 32.71/32.95 Following clause subsumed by 5913 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)| -mem(D,arr(A,bool))|p(ap(ap(c_2Ebool_2EIN(A),B),ap(ap(c_2Epred__set_2EINSERT(A),C),D)))|B!=C.
% 32.71/32.95 Following clause subsumed by 5914 during input processing: 0 [] {-} -ne(A)| -mem(B,A)| -mem(C,A)| -mem(D,arr(A,bool))|p(ap(ap(c_2Ebool_2EIN(A),B),ap(ap(c_2Epred__set_2EINSERT(A),C),D)))|B=C| -p(ap(ap(c_2Ebool_2EIN(A),B),D)).
% 32.71/32.95 Following clause subsumed by 6410 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(A,bool))| -mem(C,arr(A,bool))| -p(ap(c_2Epred__set_2EFINITE(A),B))|p(ap(c_2Epred__set_2EFINITE(A),ap(ap(c_2Epred__set_2EINTER(A),B),C))).
% 32.71/32.95 Following clause subsumed by 7324 during input processing: 0 [] {-} -mem(A,ty_2Enum_2Enum)| -mem(B,ty_2Enum_2Enum)|ap(ap(ap(c_2Enumeral__bit_2EBIT__REV,c_2Enum_2E0),A),B)=B.
% 32.71/32.95 Following clause subsumed by 7328 during input processing: 0 [] {-} -mem(A,arr(ty_2Enum_2Enum,arr(bool,bool)))| -mem(B,ty_2Enum_2Enum)| -mem(C,ty_2Enum_2Enum)| -mem(D,ty_2Enum_2Enum)| -mem(E,ty_2Enum_2Enum)|ap(ap(ap(ap(ap(ap(c_2Enumeral__bit_2EBIT__MODF,c_2Enum_2E0),A),B),C),D),E)=E.
% 32.71/32.95 Following clause subsumed by 7496 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)| -mem(E,arr(ty_2Epair_2Eprod(A,B),bool))| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,B)),ap(ap(c_2Epair_2E_2C(A,B),C),D)),E))|p(ap(ap(c_2Ebool_2EIN(A),C),ap(c_2Eset__relation_2Edomain(A,B),E))).
% 32.71/32.95 Following clause subsumed by 7499 during input processing: 0 [] {-} -ne(A)| -ne(B)| -mem(C,A)| -mem(D,B)| -mem(E,arr(ty_2Epair_2Eprod(A,B),bool))| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,B)),ap(ap(c_2Epair_2E_2C(A,B),C),D)),E))|p(ap(ap(c_2Ebool_2EIN(B),D),ap(c_2Eset__relation_2Erange(B,A),E))).
% 32.71/32.95 Following clause subsumed by 7564 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(ty_2Epair_2Eprod(A,A),bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),ap(c_2Eset__relation_2Etc(A),B)))| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),B)).
% 32.71/32.95 Following clause subsumed by 7565 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(ty_2Epair_2Eprod(A,A),bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),ap(c_2Eset__relation_2Etc(A),B)))| -mem(E,A)| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),E)),ap(c_2Eset__relation_2Etc(A),B)))| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),E),D)),ap(c_2Eset__relation_2Etc(A),B))).
% 32.71/32.95 Following clause subsumed by 7564 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(ty_2Epair_2Eprod(A,A),bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),ap(c_2Eset__relation_2Etc(A),B)))| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),B)).
% 32.71/32.95 Following clause subsumed by 7564 during input processing: 0 [] {-} -ne(A)| -mem(B,arr(ty_2Epair_2Eprod(A,A),bool))| -mem(C,A)| -mem(D,A)|p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),ap(c_2Eset__relation_2Etc(A),B)))| -p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A,A)),ap(ap(c_2Epair_2E_2C(A,A),C),D)),B)).
% 280.61/280.84 Following clause subsumed by 52 during input processing: 0 [copy,52,flip.1] {-} i(bool)=i(bool).
% 280.61/280.84 3759 back subsumes 3758.
% 280.61/280.84 3936 back subsumes 3795.
% 280.61/280.84 3937 back subsumes 3796.
% 280.61/280.84 3939 back subsumes 3789.
% 280.61/280.84 3954 back subsumes 3706.
% 280.61/280.84 6449 back subsumes 6447.
% 280.61/280.84 6857 back subsumes 5948.
% 280.61/280.84 7218 back subsumes 6825.
% 280.61/280.84 8029 back subsumes 8027.
% 280.61/280.84 8033 back subsumes 8031.
% 280.61/280.84 8073 back subsumes 8072.
% 280.61/280.84 8073 back subsumes 8069.
% 280.61/280.84 8074 back subsumes 8067.
% 280.61/280.84 8074 back subsumes 8064.
% 280.61/280.84 10987 back subsumes 10957.
% 280.61/280.84 10987 back subsumes 10824.
% 280.61/280.84 11010 back subsumes 11009.
% 280.61/280.84 11329 back subsumes 11018.
% 280.61/280.84 11330 back subsumes 11017.
% 280.61/280.84 12071 back subsumes 12069.
% 280.61/280.84 16746 back subsumes 16719.
% 280.61/280.84 16762 back subsumes 16732.
% 280.61/280.84
% 280.61/280.84 ------------> process sos:
% 280.61/280.84 Following clause subsumed by 19328 during input processing: 0 [demod,19278,19326,19294,19326] {-} ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)=ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO).
% 280.61/280.84 Following clause subsumed by 19335 during input processing: 0 [demod,19278,19400,19278] {-} c_2Earithmetic_2EZERO=c_2Earithmetic_2EZERO.
% 280.61/280.84 Following clause subsumed by 19335 during input processing: 0 [demod,19447,19453,19278] {-} c_2Earithmetic_2EZERO=c_2Earithmetic_2EZERO.
% 280.61/280.84 Following clause subsumed by 19328 during input processing: 0 [demod,19447,19459,19294,19326] {-} ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)=ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO).
% 280.61/280.84 Following clause subsumed by 19503 during input processing: 0 [copy,19328,flip.1] {-} ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)=ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO).
% 280.61/280.84 19333 back subsumes 4726.
% 280.61/280.84 Following clause subsumed by 19503 during input processing: 0 [copy,19335,flip.1] {-} c_2Earithmetic_2EZERO=c_2Earithmetic_2EZERO.
% 280.61/280.84 Following clause subsumed by 19503 during input processing: 0 [copy,19503,flip.1] {-} A=A.
% 280.61/280.84 19503 back subsumes 19335.
% 280.61/280.84 19503 back subsumes 19328.
% 280.61/280.84 19503 back subsumes 19129.
% 280.61/280.84 19503 back subsumes 19128.
% 280.61/280.84 19503 back subsumes 19125.
% 280.61/280.84 19503 back subsumes 19124.
% 280.61/280.84 19503 back subsumes 19123.
% 280.61/280.84 19503 back subsumes 19120.
% 280.61/280.84 19503 back subsumes 19118.
% 280.61/280.84 19503 back subsumes 19117.
% 280.61/280.84 19503 back subsumes 19116.
% 280.61/280.84 19503 back subsumes 19115.
% 280.61/280.84 19503 back subsumes 19114.
% 280.61/280.84 19503 back subsumes 19113.
% 280.61/280.84 19503 back subsumes 19112.
% 280.61/280.84 19503 back subsumes 19095.
% 280.61/280.84 19503 back subsumes 19092.
% 280.61/280.84 19503 back subsumes 19083.
% 280.61/280.84 19503 back subsumes 19064.
% 280.61/280.84 19503 back subsumes 19061.
% 280.61/280.84 19503 back subsumes 19052.
% 280.61/280.84 19503 back subsumes 18967.
% 280.61/280.84 19503 back subsumes 18966.
% 280.61/280.84 19503 back subsumes 18965.
% 280.61/280.84 19503 back subsumes 18964.
% 280.61/280.84 19503 back subsumes 18961.
% 280.61/280.84 19503 back subsumes 18956.
% 280.61/280.84 19503 back subsumes 18953.
% 280.61/280.84 19503 back subsumes 18948.
% 280.61/280.84 19503 back subsumes 18945.
% 280.61/280.84 19503 back subsumes 18936.
% 280.61/280.84 19503 back subsumes 18935.
% 280.61/280.84 19503 back subsumes 18934.
% 280.61/280.84 19503 back subsumes 18933.
% 280.61/280.84 19503 back subsumes 18912.
% 280.61/280.84 19503 back subsumes 18911.
% 280.61/280.84 19503 back subsumes 18910.
% 280.61/280.84 19503 back subsumes 18909.
% 280.61/280.84 19503 back subsumes 18908.
% 280.61/280.84 19503 back subsumes 18857.
% 280.61/280.84 19503 back subsumes 18856.
% 280.61/280.84 19503 back subsumes 18855.
% 280.61/280.84 19503 back subsumes 18850.
% 280.61/280.84 19503 back subsumes 18849.
% 280.61/280.84 19503 back subsumes 18845.
% 280.61/280.84 19503 back subsumes 18844.
% 280.61/280.84 19503 back subsumes 18843.
% 280.61/280.84 19503 back subsumes 18842.
% 280.61/280.84 19503 back subsumes 18841.
% 280.61/280.84 19503 back subsumes 18829.
% 280.61/280.84 19503 back subsumes 18828.
% 280.61/280.84 19503 back subsumes 18827.
% 280.61/280.84 19503 back subsumes 18826.
% 280.61/280.84 19503 back subsumes 18825.
% 280.61/280.84 19503 back subsumes 18824.
% 280.61/280.84 19503 back subsumes 18823.
% 280.61/280.84 19503 back subsumes 18816.
% 280.61/280.84 19503 back subsumes 18813.
% 280.61/280.84 19503 back subsumes 18812.
% 280.61/280.84 19503 back subsumes 18752.
% 280.61/280.84 19503 back subsumes 18751.
% 280.61/280.84 19503 back subsumes 18748.
% 280.61/280.84 19503 back subsumes 18743.
% 280.61/280.84 19503 back subsumes 18742.
% 280.61/280.84 19503 back subsumes 18739.
% 280.61/280.84 19503 back subsumes 18705.
% 280.61/280.84 19503 back subsumes 18704.
% 280.61/280.84 19503 back subsumes 18702.
% 280.61/280.84 19503 back subsumes 18701.
% 280.61/280.84 19503 back subsumes 18672.
% 280.61/280.84 19503 back subsumes 18671.
% 280.61/280.84 19503 back subsumes 18670.
% 280.61/280.84 19503 back subsumes 18667.
% 280.61/280.84 19503 back subsumes 18666.
% 280.61/280.84 19503 back subsumes 18665.
% 280.61/280.84 19503 back subsumes 18651.
% 280.61/280.84 19503 back subsumes 18650.
% 280.61/280.84 19503 back subsumes 18649.
% 280.61/280.84 19503 back subsumes 18646.
% 280.61/280.84 19503 back subsumes 18645.
% 280.61/280.84 19503 back subsumes 18644.
% 280.61/280.84 19503 back subsumes 18641.
% 280.61/280.84 19503 back subsumes 18640.
% 280.61/280.84 19503 back subsumes 18639.
% 280.61/280.84 19503 back subsumes 18638.
% 280.61/280.84 19503 back subsumes 18637.
% 280.61/280.84 19503 back subsumes 18630.
% 280.61/280.84 19503 back subsumes 18627.
% 280.78/281.01 19503 back subsumes 18626.
% 280.78/281.01 19503 back subsumes 18618.
% 280.78/281.01 19503 back subsumes 18612.
% 280.78/281.01 19503 back subsumes 18611.
% 280.78/281.01 19503 back subsumes 18610.
% 280.78/281.01 19503 back subsumes 18609.
% 280.78/281.01 19503 back subsumes 18608.
% 280.78/281.01 19503 back subsumes 18607.
% 280.78/281.01 19503 back subsumes 18566.
% 280.78/281.01 19503 back subsumes 18565.
% 280.78/281.01 19503 back subsumes 18564.
% 280.78/281.01 19503 back subsumes 18563.
% 280.78/281.01 19503 back subsumes 18562.
% 280.78/281.01 19503 back subsumes 18561.
% 280.78/281.01 19503 back subsumes 18560.
% 280.78/281.01 19503 back subsumes 18559.
% 280.78/281.01 19503 back subsumes 18558.
% 280.78/281.01 19503 back subsumes 18555.
% 280.78/281.01 19503 back subsumes 18554.
% 280.78/281.01 19503 back subsumes 18553.
% 280.78/281.01 19503 back subsumes 18552.
% 280.78/281.01 19503 back subsumes 18551.
% 280.78/281.01 19503 back subsumes 18550.
% 280.78/281.01 19503 back subsumes 18472.
% 280.78/281.01 19503 back subsumes 18382.
% 280.78/281.01 19503 back subsumes 18361.
% 280.78/281.01 19503 back subsumes 18360.
% 280.78/281.01 19503 back subsumes 18359.
% 280.78/281.01 19503 back subsumes 18347.
% 280.78/281.01 19503 back subsumes 18346.
% 280.78/281.01 19503 back subsumes 18345.
% 280.78/281.01 19503 back subsumes 18344.
% 280.78/281.01 19503 back subsumes 18326.
% 280.78/281.01 19503 back subsumes 18277.
% 280.78/281.01 19503 back subsumes 18274.
% 280.78/281.01 19503 back subsumes 18273.
% 280.78/281.01 19503 back subsumes 18272.
% 280.78/281.01 19503 back subsumes 18218.
% 280.78/281.01 19503 back subsumes 17949.
% 280.78/281.01 19503 back subsumes 17813.
% 280.78/281.01 19503 back subsumes 17812.
% 280.78/281.01 19503 back subsumes 17811.
% 280.78/281.01 19503 back subsumes 17810.
% 280.78/281.01 19503 back subsumes 17808.
% 280.78/281.01 19503 back subsumes 17722.
% 280.78/281.01 19503 back subsumes 17709.
% 280.78/281.01 19503 back subsumes 17696.
% 280.78/281.01 19503 back subsumes 17669.
% 280.78/281.01 19503 back subsumes 17668.
% 280.78/281.01 19503 back subsumes 17665.
% 280.78/281.01 19503 back subsumes 17664.
% 280.78/281.01 19503 back subsumes 17661.
% 280.78/281.01 19503 back subsumes 17660.
% 280.78/281.01 19503 back subsumes 17657.
% 280.78/281.01 19503 back subsumes 17656.
% 280.78/281.01 19503 back subsumes 17619.
% 280.78/281.01 19503 back subsumes 17618.
% 280.78/281.01 19503 back subsumes 17616.
% 280.78/281.01 19503 back subsumes 17486.
% 280.78/281.01 19503 back subsumes 17483.
% 280.78/281.01 19503 back subsumes 17482.
% 280.78/281.01 19503 back subsumes 17479.
% 280.78/281.01 19503 back subsumes 17476.
% 280.78/281.01 19503 back subsumes 17475.
% 280.78/281.01 19503 back subsumes 17472.
% 280.78/281.01 19503 back subsumes 17469.
% 280.78/281.01 19503 back subsumes 17468.
% 280.78/281.01 19503 back subsumes 17465.
% 280.78/281.01 19503 back subsumes 17462.
% 280.78/281.01 19503 back subsumes 17461.
% 280.78/281.01 19503 back subsumes 17458.
% 280.78/281.01 19503 back subsumes 17455.
% 280.78/281.01 19503 back subsumes 17454.
% 280.78/281.02 19503 back subsumes 17426.
% 280.78/281.02 19503 back subsumes 17425.
% 280.78/281.02 19503 back subsumes 17295.
% 280.78/281.02 19503 back subsumes 17284.
% 280.78/281.02 19503 back subsumes 17283.
% 280.78/281.02 19503 back subsumes 17279.
% 280.78/281.02 19503 back subsumes 17277.
% 280.78/281.02 19503 back subsumes 17275.
% 280.78/281.02 19503 back subsumes 17271.
% 280.78/281.02 19503 back subsumes 17270.
% 280.78/281.02 19503 back subsumes 17267.
% 280.78/281.02 19503 back subsumes 17264.
% 280.78/281.02 19503 back subsumes 17263.
% 280.78/281.02 19503 back subsumes 17259.
% 280.78/281.02 19503 back subsumes 17257.
% 280.78/281.02 19503 back subsumes 17255.
% 280.78/281.02 19503 back subsumes 17251.
% 280.78/281.02 19503 back subsumes 17250.
% 280.78/281.02 19503 back subsumes 17247.
% 280.78/281.02 19503 back subsumes 17241.
% 280.78/281.02 19503 back subsumes 17238.
% 280.78/281.02 19503 back subsumes 17237.
% 280.78/281.02 19503 back subsumes 17159.
% 280.78/281.02 19503 back subsumes 17158.
% 280.78/281.02 19503 back subsumes 17157.
% 280.78/281.02 19503 back subsumes 17155.
% 280.78/281.02 19503 back subsumes 17153.
% 280.78/281.02 19503 back subsumes 17149.
% 280.78/281.02 19503 back subsumes 17132.
% 280.78/281.02 19503 back subsumes 17131.
% 280.78/281.02 19503 back subsumes 17124.
% 280.78/281.02 19503 back subsumes 17123.
% 280.78/281.02 19503 back subsumes 17120.
% 280.78/281.02 19503 back subsumes 17118.
% 280.78/281.02 19503 back subsumes 17117.
% 280.78/281.02 19503 back subsumes 17110.
% 280.78/281.02 19503 back subsumes 17109.
% 280.78/281.02 19503 back subsumes 17108.
% 280.78/281.02 19503 back subsumes 17107.
% 280.78/281.02 19503 back subsumes 17106.
% 280.78/281.02 19503 back subsumes 17105.
% 280.78/281.02 19503 back subsumes 17102.
% 280.78/281.02 19503 back subsumes 17101.
% 280.78/281.02 19503 back subsumes 17097.
% 280.78/281.02 19503 back subsumes 17095.
% 280.78/281.02 19503 back subsumes 17093.
% 280.78/281.02 19503 back subsumes 17089.
% 280.78/281.02 19503 back subsumes 17088.
% 280.78/281.02 19503 back subsumes 17085.
% 280.78/281.02 19503 back subsumes 16939.
% 280.78/281.02 19503 back subsumes 16784.
% 280.78/281.02 19503 back subsumes 16607.
% 280.78/281.02 19503 back subsumes 16601.
% 280.78/281.02 19503 back subsumes 16598.
% 280.78/281.02 19503 back subsumes 16597.
% 280.78/281.02 19503 back subsumes 16594.
% 280.78/281.02 19503 back subsumes 16591.
% 280.78/281.02 19503 back subsumes 16590.
% 280.78/281.02 19503 back subsumes 16587.
% 280.78/281.02 19503 back subsumes 16586.
% 280.78/281.02 19503 back subsumes 16585.
% 280.78/281.02 19503 back subsumes 16584.
% 280.78/281.02 19503 back subsumes 16573.
% 280.78/281.02 19503 back subsumes 16536.
% 280.78/281.02 19503 back subsumes 16535.
% 280.78/281.02 19503 back subsumes 16534.
% 280.78/281.02 19503 back subsumes 16450.
% 280.78/281.02 19503 back subsumes 16442.
% 280.78/281.02 19503 back subsumes 16374.
% 280.78/281.02 19503 back subsumes 16366.
% 280.78/281.02 19503 back subsumes 16355.
% 280.78/281.02 19503 back subsumes 16354.
% 280.78/281.02 19503 back subsumes 16353.
% 280.78/281.02 19503 back subsumes 16351.
% 280.78/281.02 19503 back subsumes 16350.
% 280.78/281.02 19503 back subsumes 16349.
% 280.78/281.02 19503 back subsumes 16347.
% 280.78/281.02 19503 back subsumes 16346.
% 280.78/281.02 19503 back subsumes 16345.
% 281.19/281.41 19503 back subsumes 16343.
% 281.19/281.41 19503 back subsumes 16342.
% 281.19/281.41 19503 back subsumes 16341.
% 281.19/281.41 19503 back subsumes 16331.
% 281.19/281.41 19503 back subsumes 16330.
% 281.19/281.41 19503 back subsumes 16329.
% 281.19/281.41 19503 back subsumes 16327.
% 281.19/281.41 19503 back subsumes 16325.
% 281.19/281.41 19503 back subsumes 16324.
% 281.19/281.41 19503 back subsumes 16250.
% 281.19/281.41 19503 back subsumes 16247.
% 281.19/281.41 19503 back subsumes 16244.
% 281.19/281.41 19503 back subsumes 16192.
% 281.19/281.41 19503 back subsumes 16189.
% 281.19/281.41 19503 back subsumes 16186.
% 281.19/281.41 19503 back subsumes 16135.
% 281.19/281.41 19503 back subsumes 16130.
% 281.19/281.41 19503 back subsumes 16121.
% 281.19/281.41 19503 back subsumes 16077.
% 281.19/281.41 19503 back subsumes 16076.
% 281.19/281.41 19503 back subsumes 16075.
% 281.19/281.41 19503 back subsumes 16074.
% 281.19/281.41 19503 back subsumes 16073.
% 281.19/281.41 19503 back subsumes 16072.
% 281.19/281.41 19503 back subsumes 16071.
% 281.19/281.41 19503 back subsumes 16070.
% 281.19/281.41 19503 back subsumes 15912.
% 281.19/281.41 19503 back subsumes 15911.
% 281.19/281.41 19503 back subsumes 15910.
% 281.19/281.41 19503 back subsumes 15909.
% 281.19/281.41 19503 back subsumes 15908.
% 281.19/281.41 19503 back subsumes 15907.
% 281.19/281.41 19503 back subsumes 15906.
% 281.19/281.41 19503 back subsumes 15905.
% 281.19/281.41 19503 back subsumes 15712.
% 281.19/281.41 19503 back subsumes 15711.
% 281.19/281.41 19503 back subsumes 15710.
% 281.19/281.41 19503 back subsumes 15709.
% 281.19/281.41 19503 back subsumes 15708.
% 281.19/281.41 19503 back subsumes 15707.
% 281.19/281.41 19503 back subsumes 15706.
% 281.19/281.41 19503 back subsumes 15705.
% 281.19/281.41 19503 back subsumes 15704.
% 281.19/281.41 19503 back subsumes 15703.
% 281.19/281.41 19503 back subsumes 15702.
% 281.19/281.41 19503 back subsumes 15701.
% 281.19/281.41 19503 back subsumes 15700.
% 281.19/281.41 19503 back subsumes 15699.
% 281.19/281.41 19503 back subsumes 15698.
% 281.19/281.41 19503 back subsumes 15697.
% 281.19/281.41 19503 back subsumes 15453.
% 281.19/281.41 19503 back subsumes 15452.
% 281.19/281.41 19503 back subsumes 15432.
% 281.19/281.41 19503 back subsumes 15416.
% 281.19/281.41 19503 back subsumes 15415.
% 281.19/281.41 19503 back subsumes 15414.
% 281.19/281.41 19503 back subsumes 15413.
% 281.19/281.41 19503 back subsumes 15412.
% 281.19/281.41 19503 back subsumes 15411.
% 281.19/281.41 19503 back subsumes 15410.
% 281.19/281.41 19503 back subsumes 15409.
% 281.19/281.41 19503 back subsumes 15403.
% 281.19/281.41 19503 back subsumes 15346.
% 281.19/281.41 19503 back subsumes 15345.
% 281.19/281.41 19503 back subsumes 15344.
% 281.19/281.41 19503 back subsumes 15343.
% 281.19/281.41 19503 back subsumes 15342.
% 281.19/281.41 19503 back subsumes 15341.
% 281.19/281.41 19503 back subsumes 15340.
% 281.19/281.41 19503 back subsumes 15339.
% 281.19/281.41 19503 back subsumes 15338.
% 281.19/281.41 19503 back subsumes 15337.
% 281.19/281.41 19503 back subsumes 15336.
% 281.19/281.41 19503 back subsumes 15332.
% 281.19/281.41 19503 back subsumes 15329.
% 281.19/281.41 19503 back subsumes 15326.
% 281.19/281.41 19503 back subsumes 15319.
% 281.19/281.41 19503 back subsumes 15318.
% 281.19/281.41 19503 back subsumes 15315.
% 281.19/281.41 19503 back subsumes 15314.
% 281.19/281.41 19503 back subsumes 15311.
% 281.19/281.41 19503 back subsumes 15310.
% 281.19/281.41 19503 back subsumes 15058.
% 281.19/281.41 19503 back subsumes 15055.
% 281.19/281.41 19503 back subsumes 15052.
% 281.19/281.41 19503 back subsumes 15026.
% 281.19/281.41 19503 back subsumes 15025.
% 281.19/281.41 19503 back subsumes 15024.
% 281.19/281.41 19503 back subsumes 15023.
% 281.19/281.41 19503 back subsumes 15022.
% 281.19/281.41 19503 back subsumes 14911.
% 281.19/281.41 19503 back subsumes 14910.
% 281.19/281.41 19503 back subsumes 14909.
% 281.19/281.41 19503 back subsumes 14907.
% 281.19/281.41 19503 back subsumes 14819.
% 281.19/281.41 19503 back subsumes 14639.
% 281.19/281.41 19503 back subsumes 14459.
% 281.19/281.41 19503 back subsumes 14449.
% 281.19/281.41 19503 back subsumes 14448.
% 281.19/281.41 19503 back subsumes 14411.
% 281.19/281.41 19503 back subsumes 14017.
% 281.19/281.41 19503 back subsumes 13816.
% 281.19/281.41 19503 back subsumes 13627.
% 281.19/281.41 19503 back subsumes 13623.
% 281.19/281.41 19503 back subsumes 13619.
% 281.19/281.41 19503 back subsumes 13615.
% 281.19/281.41 19503 back subsumes 13553.
% 281.19/281.41 19503 back subsumes 13549.
% 281.19/281.41 19503 back subsumes 13548.
% 281.19/281.41 19503 back subsumes 13547.
% 281.19/281.41 19503 back subsumes 13540.
% 281.19/281.41 19503 back subsumes 13507.
% 281.19/281.41 19503 back subsumes 13503.
% 281.19/281.41 19503 back subsumes 13494.
% 281.19/281.41 19503 back subsumes 13440.
% 281.19/281.41 19503 back subsumes 13385.
% 281.19/281.41 19503 back subsumes 13371.
% 281.19/281.41 19503 back subsumes 13314.
% 281.19/281.41 19503 back subsumes 13313.
% 281.19/281.41 19503 back subsumes 13312.
% 281.19/281.41 19503 back subsumes 13311.
% 281.19/281.41 19503 back subsumes 13310.
% 281.19/281.41 19503 back subsumes 13309.
% 281.19/281.41 19503 back subsumes 13145.
% 281.19/281.41 19503 back subsumes 13139.
% 281.19/281.41 19503 back subsumes 13133.
% 281.19/281.41 19503 back subsumes 13127.
% 281.19/281.41 19503 back subsumes 13121.
% 281.19/281.41 19503 back subsumes 13074.
% 281.19/281.41 19503 back subsumes 13071.
% 281.19/281.41 19503 back subsumes 12993.
% 281.19/281.41 19503 back subsumes 12932.
% 281.19/281.41 19503 back subsumes 12875.
% 281.19/281.41 19503 back subsumes 12866.
% 281.19/281.41 19503 back subsumes 12855.
% 281.19/281.41 19503 back subsumes 12846.
% 281.19/281.41 19503 back subsumes 12833.
% 281.19/281.41 19503 back subsumes 12832.
% 281.19/281.41 19503 back subsumes 12819.
% 281.19/281.41 19503 back subsumes 12629.
% 281.19/281.41 19503 back subsumes 12584.
% 281.19/281.41 19503 back subsumes 12415.
% 281.19/281.41 19503 back subsumes 12398.
% 281.19/281.41 19503 back subsumes 12395.
% 281.19/281.41 19503 back subsumes 12394.
% 281.19/281.41 19503 back subsumes 12393.
% 281.19/281.41 19503 back subsumes 12375.
% 281.19/281.41 19503 back subsumes 12364.
% 281.19/281.41 19503 back subsumes 12360.
% 281.19/281.41 19503 back subsumes 12359.
% 281.19/281.41 19503 back subsumes 12358.
% 281.63/281.90 19503 back subsumes 12357.
% 281.63/281.90 19503 back subsumes 12356.
% 281.63/281.90 19503 back subsumes 12351.
% 281.63/281.90 19503 back subsumes 12337.
% 281.63/281.90 19503 back subsumes 12328.
% 281.63/281.90 19503 back subsumes 12253.
% 281.63/281.90 19503 back subsumes 12246.
% 281.63/281.90 19503 back subsumes 12166.
% 281.63/281.90 19503 back subsumes 12165.
% 281.63/281.90 19503 back subsumes 12164.
% 281.63/281.90 19503 back subsumes 12163.
% 281.63/281.90 19503 back subsumes 12145.
% 281.63/281.90 19503 back subsumes 12144.
% 281.63/281.90 19503 back subsumes 11977.
% 281.63/281.90 19503 back subsumes 11752.
% 281.63/281.90 19503 back subsumes 11663.
% 281.63/281.90 19503 back subsumes 11660.
% 281.63/281.90 19503 back subsumes 11653.
% 281.63/281.90 19503 back subsumes 11652.
% 281.63/281.90 19503 back subsumes 11636.
% 281.63/281.90 19503 back subsumes 11207.
% 281.63/281.90 19503 back subsumes 11164.
% 281.63/281.90 19503 back subsumes 11161.
% 281.63/281.90 19503 back subsumes 11158.
% 281.63/281.90 19503 back subsumes 11155.
% 281.63/281.90 19503 back subsumes 11138.
% 281.63/281.90 19503 back subsumes 11128.
% 281.63/281.90 19503 back subsumes 11118.
% 281.63/281.90 19503 back subsumes 11115.
% 281.63/281.90 19503 back subsumes 11112.
% 281.63/281.90 19503 back subsumes 11106.
% 281.63/281.90 19503 back subsumes 11100.
% 281.63/281.90 19503 back subsumes 11097.
% 281.63/281.90 19503 back subsumes 11092.
% 281.63/281.90 19503 back subsumes 11089.
% 281.63/281.90 19503 back subsumes 11066.
% 281.63/281.90 19503 back subsumes 11035.
% 281.63/281.90 19503 back subsumes 11032.
% 281.63/281.90 19503 back subsumes 10995.
% 281.63/281.90 19503 back subsumes 10987.
% 281.63/281.90 19503 back subsumes 10981.
% 281.63/281.90 19503 back subsumes 10958.
% 281.63/281.90 19503 back subsumes 10838.
% 281.63/281.90 19503 back subsumes 10817.
% 281.63/281.90 19503 back subsumes 10559.
% 281.63/281.90 19503 back subsumes 10555.
% 281.63/281.90 19503 back subsumes 10551.
% 281.63/281.90 19503 back subsumes 10547.
% 281.63/281.90 19503 back subsumes 10522.
% 281.63/281.90 19503 back subsumes 10520.
% 281.63/281.90 19503 back subsumes 10518.
% 281.63/281.90 19503 back subsumes 10135.
% 281.63/281.90 19503 back subsumes 10008.
% 281.63/281.90 19503 back subsumes 9995.
% 281.63/281.90 19503 back subsumes 9981.
% 281.63/281.90 19503 back subsumes 9933.
% 281.63/281.90 19503 back subsumes 9862.
% 281.63/281.90 19503 back subsumes 9859.
% 281.63/281.90 19503 back subsumes 9856.
% 281.63/281.90 19503 back subsumes 9853.
% 281.63/281.90 19503 back subsumes 9843.
% 281.63/281.90 19503 back subsumes 9603.
% 281.63/281.90 19503 back subsumes 9600.
% 281.63/281.90 19503 back subsumes 9597.
% 281.63/281.90 19503 back subsumes 9594.
% 281.63/281.90 19503 back subsumes 9181.
% 281.63/281.90 19503 back subsumes 9178.
% 281.63/281.90 19503 back subsumes 9175.
% 281.63/281.90 19503 back subsumes 9172.
% 281.63/281.90 19503 back subsumes 9165.
% 281.63/281.90 19503 back subsumes 9162.
% 281.63/281.90 19503 back subsumes 9159.
% 281.63/281.90 19503 back subsumes 9156.
% 281.63/281.90 19503 back subsumes 8800.
% 281.63/281.90 19503 back subsumes 8797.
% 281.63/281.90 19503 back subsumes 8757.
% 281.63/281.90 19503 back subsumes 8755.
% 281.63/281.90 19503 back subsumes 8721.
% 281.63/281.90 19503 back subsumes 8695.
% 281.63/281.90 19503 back subsumes 8691.
% 281.63/281.90 19503 back subsumes 8530.
% 281.63/281.90 19503 back subsumes 8528.
% 281.63/281.90 19503 back subsumes 8438.
% 281.63/281.90 19503 back subsumes 8435.
% 281.63/281.90 19503 back subsumes 8432.
% 281.63/281.90 19503 back subsumes 8429.
% 281.63/281.91 19503 back subsumes 8426.
% 281.63/281.91 19503 back subsumes 8423.
% 281.63/281.91 19503 back subsumes 8420.
% 281.63/281.91 19503 back subsumes 8417.
% 281.63/281.91 19503 back subsumes 8414.
% 281.63/281.91 19503 back subsumes 8372.
% 281.63/281.91 19503 back subsumes 8368.
% 281.63/281.91 19503 back subsumes 8364.
% 281.63/281.91 19503 back subsumes 7940.
% 281.63/281.91 19503 back subsumes 7938.
% 281.63/281.91 19503 back subsumes 7936.
% 281.63/281.91 19503 back subsumes 7934.
% 281.63/281.91 19503 back subsumes 7932.
% 281.63/281.91 19503 back subsumes 7898.
% 281.63/281.91 19503 back subsumes 7897.
% 281.63/281.91 19503 back subsumes 7896.
% 281.63/281.91 19503 back subsumes 7895.
% 281.63/281.91 19503 back subsumes 127.
% 281.63/281.91 19503 back subsumes 52.
% 281.63/281.91 Following clause subsumed by 19140 during input processing: 0 [copy,19504,flip.1] {-} ap(f1(A),B)=ap(ap(c_2Emin_2E_3D(arr(A,bool)),B),k(A,c_2Ebool_2ET)).
% 281.63/281.91 Following clause subsumed by 19141 during input processing: 0 [copy,19505,flip.1] {-} ap(f2(A),B)=ap(B,ap(c_2Emin_2E_40(A),B)).
% 281.63/281.91 Following clause subsumed by 19162 during input processing: 0 [copy,19514,flip.1] {-} ap(f12(A),B)=ap(ap(c_2Ebool_2E_2F_5C,ap(c_2Ebool_2E_3F(A),B)),ap(c_2Ebool_2E_21(A),f11(A,B))).
% 281.63/281.91 Following clause subsumed by 19165 during input processing: 0 [copy,19515,flip.1] {-} ap(f18(A),B)=f17(A,B).
% 281.63/281.91 Following clause subsumed by 19166 during input processing: 0 [copy,19516,flip.1] {-} ap(f21(A,B),C)=ap(c_2Ebool_2E_21(B),f20(A,B,C)).
% 281.63/281.91 Following clause subsumed by 19167 during input processing: 0 [copy,19517,flip.1] {-} ap(f24(A,B),C)=ap(c_2Ebool_2E_21(B),f23(A,B,C)).
% 281.63/281.91 Following clause subsumed by 19172 during input processing: 0 [copy,19518,flip.1] {-} ap(f33(A),B)=f32(A,B).
% 281.63/281.91 Following clause subsumed by 19173 during input processing: 0 [copy,19519,flip.1] {-} ap(f36(A),B)=f35(A,B).
% 281.63/281.91 Following clause subsumed by 19174 during input processing: 0 [copy,19520,flip.1] {-} ap(f39(A),B)=f38(A,B).
% 281.63/281.91 Following clause subsumed by 19175 during input processing: 0 [copy,19521,flip.1] {-} ap(f44(A),B)=f43(A,B).
% 287.66/287.88 Following clause subsumed by 19176 during input processing: 0 [copy,19522,flip.1] {-} ap(f46(A),B)=f45(A,B).
% 287.66/287.88 Following clause subsumed by 19191 during input processing: 0 [copy,19525,flip.1] {-} ap(f68(A,B),C)=k(A,C).
% 287.66/287.88 Following clause subsumed by 19231 during input processing: 0 [copy,19531,flip.1] {-} ap(f115(A,B),C)=ap(c_2Ebool_2E_3F(B),f114(A,B,C)).
% 287.66/287.88 Following clause subsumed by 19232 during input processing: 0 [copy,19532,flip.1] {-} ap(f120(A,B),C)=ap(c_2Ebool_2E_3F(B),f119(A,B,C)).
% 287.66/287.88 19742 back subsumes 19741.
% 287.66/287.88 21101 back subsumes 4729.
% 287.66/287.88 Following clause subsumed by 19362 during input processing: 0 [copy,21354,flip.1] {-} ap(f219(A),B)=ap(c_2Ebool_2E_21(arr(arr(ty_2Enum_2Enum,arr(A,bool)),bool)),f218(A,B)).
% 287.66/287.88 Following clause subsumed by 19466 during input processing: 0 [copy,21409,flip.1] {-} ap(f291(A),B)=ap(ap(c_2Epair_2E_2C(A,bool),B),c_2Ebool_2EF).
% 287.66/287.88 Following clause subsumed by 19467 during input processing: 0 [copy,21410,flip.1] {-} ap(f292(A),B)=ap(ap(c_2Epair_2E_2C(A,bool),B),c_2Ebool_2ET).
% 287.66/287.88 Following clause subsumed by 19499 during input processing: 0 [copy,21440,flip.1] {-} ap(f343(A),B)=f342(A,B).
% 287.66/287.88
% 287.66/287.88 ======= end of input processing =======
% 287.73/287.98
% 287.73/287.98 SEGMENTATION FAULT!! This is probably caused by a
% 287.73/287.98 bug in Otter. Please send copy of the input file to
% 287.73/287.98 otter@mcs.anl.gov, let us know what version of Otter you are
% 287.73/287.98 using, and send any other info that might be useful.
% 287.73/287.98
% 287.73/287.98
% 287.73/287.98 SEGMENTATION FAULT!! This is probably caused by a
% 287.73/287.98 bug in Otter. Please send copy of the input file to
% 287.73/287.98 otter@mcs.anl.gov, let us know what version of Otter you are
% 287.73/287.98 using, and send any other info that might be useful.
% 287.73/287.98
% 287.73/287.98
% 287.73/287.98 The job finished Thu Jun 2 11:59:52 2022
%------------------------------------------------------------------------------