%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SWV892-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n006.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 : Wed Jul 20 21:40:34 EDT 2022
% Result : Unknown 4.70s 4.95s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV892-1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.14 % Command : sos-script %s
% 0.13/0.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Tue Jun 14 16:52:26 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.21/0.46 ----- Otter 3.2, August 2001 -----
% 0.21/0.46 The process was started by sandbox on n006.cluster.edu,
% 0.21/0.46 Tue Jun 14 16:52:26 2022
% 0.21/0.46 The command was "./sos". The process ID is 6533.
% 0.21/0.46
% 0.21/0.46 set(prolog_style_variables).
% 0.21/0.46 set(auto).
% 0.21/0.46 dependent: set(auto1).
% 0.21/0.46 dependent: set(process_input).
% 0.21/0.46 dependent: clear(print_kept).
% 0.21/0.46 dependent: clear(print_new_demod).
% 0.21/0.46 dependent: clear(print_back_demod).
% 0.21/0.46 dependent: clear(print_back_sub).
% 0.21/0.46 dependent: set(control_memory).
% 0.21/0.46 dependent: assign(max_mem, 12000).
% 0.21/0.46 dependent: assign(pick_given_ratio, 4).
% 0.21/0.46 dependent: assign(stats_level, 1).
% 0.21/0.46 dependent: assign(pick_semantic_ratio, 3).
% 0.21/0.46 dependent: assign(sos_limit, 5000).
% 0.21/0.46 dependent: assign(max_weight, 60).
% 0.21/0.46 clear(print_given).
% 0.21/0.46
% 0.21/0.46 list(usable).
% 0.21/0.46
% 0.21/0.46 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=7.
% 0.21/0.46
% 0.21/0.46 This ia a non-Horn set with equality. The strategy will be
% 0.21/0.46 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.21/0.46 unit deletion, with positive clauses in sos and nonpositive
% 0.21/0.46 clauses in usable.
% 0.21/0.46
% 0.21/0.46 dependent: set(knuth_bendix).
% 0.21/0.46 dependent: set(para_from).
% 0.21/0.46 dependent: set(para_into).
% 0.21/0.46 dependent: clear(para_from_right).
% 0.21/0.46 dependent: clear(para_into_right).
% 0.21/0.46 dependent: set(para_from_vars).
% 0.21/0.46 dependent: set(eq_units_both_ways).
% 0.21/0.46 dependent: set(dynamic_demod_all).
% 0.21/0.46 dependent: set(dynamic_demod).
% 0.21/0.46 dependent: set(order_eq).
% 0.21/0.46 dependent: set(back_demod).
% 0.21/0.46 dependent: set(lrpo).
% 0.21/0.46 dependent: set(hyper_res).
% 0.21/0.46 dependent: set(unit_deletion).
% 0.21/0.46 dependent: set(factor).
% 0.21/0.46
% 0.21/0.46 ------------> process usable:
% 0.21/0.46 Following clause subsumed by 3 during input processing: 0 [] {-} -class_Lattices_Olower__semilattice(A)|c_lessequals(B,c_Lattices_Olower__semilattice__class_Oinf(C,D,A),A)| -c_lessequals(B,D,A)| -c_lessequals(B,C,A).
% 0.21/0.46 Following clause subsumed by 3 during input processing: 0 [] {-} -class_Lattices_Olower__semilattice(A)|c_lessequals(B,c_Lattices_Olower__semilattice__class_Oinf(C,D,A),A)| -c_lessequals(B,D,A)| -c_lessequals(B,C,A).
% 0.21/0.46 Following clause subsumed by 22 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_lessequals(C,B,A)| -c_lessequals(B,C,A).
% 0.21/0.46 Following clause subsumed by 22 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|B=C| -c_lessequals(C,B,A)| -c_lessequals(B,C,A).
% 0.21/0.46 Following clause subsumed by 23 during input processing: 0 [] {-} A=B| -c_lessequals(B,A,tc_fun(C,tc_bool))| -c_lessequals(A,B,tc_fun(C,tc_bool)).
% 0.21/0.46 Following clause subsumed by 39 during input processing: 0 [] {-} c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(B,C)| -c_Finite__Set_Ofinite(A,C).
% 0.21/0.46 Following clause subsumed by 53 during input processing: 0 [] {-} c_lessequals(A,c_Lattices_Olower__semilattice__class_Oinf(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))| -c_lessequals(A,C,tc_fun(D,tc_bool))| -c_lessequals(A,B,tc_fun(D,tc_bool)).
% 0.21/0.46 Following clause subsumed by 56 during input processing: 0 [] {-} -class_Lattices_Oupper__semilattice(A)|c_lessequals(B,C,A)| -c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(D,B,A),C,A).
% 0.21/0.46 Following clause subsumed by 57 during input processing: 0 [] {-} -class_Lattices_Oupper__semilattice(A)|c_lessequals(B,C,A)| -c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(B,D,A),C,A).
% 0.21/0.46 Following clause subsumed by 68 during input processing: 0 [] {-} hBOOL(hAPP(A,B))| -c_lessequals(C,A,tc_fun(D,tc_bool))| -hBOOL(hAPP(C,B)).
% 0.21/0.46 Following clause subsumed by 71 during input processing: 0 [] {-} c_Finite__Set_Ofinite(A,B)| -c_lessequals(A,C,tc_fun(B,tc_bool))| -c_Finite__Set_Ofinite(C,B).
% 0.21/0.46 Following clause subsumed by 81 during input processing: 0 [] {-} -c_lessequals(A,B,tc_fun(C,tc_bool))|c_lessequals(c_Set_Oimage(D,A,C,E),c_Set_Oimage(D,B,C,E),tc_fun(E,tc_bool)).
% 0.21/0.46 Following clause subsumed by 83 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(B,C,A)|C=B.
% 0.21/0.46 Following clause subsumed by 85 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)|B=C| -c_lessequals(B,C,A).
% 0.21/0.47 Following clause subsumed by 84 during input processing: 0 [] {-} A=B|c_HOL_Oord__class_Oless(A,B,tc_fun(C,tc_bool))| -c_lessequals(A,B,tc_fun(C,tc_bool)).
% 0.21/0.47 Following clause subsumed by 85 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)|B=C| -c_lessequals(B,C,A).
% 0.21/0.47 Following clause subsumed by 85 during input processing: 0 [] {-} -class_Orderings_Oorder(A)|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(B,C,A)|B=C.
% 0.21/0.47 Following clause subsumed by 86 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_HOL_Oord__class_Oless(B,C,A)| -c_lessequals(B,C,A).
% 0.21/0.47 Following clause subsumed by 45 during input processing: 0 [] {-} c_lessequals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lessequals(A,C,tc_fun(D,tc_bool))|hBOOL(hAPP(hAPP(c_in(D),B),A)).
% 0.21/0.47 Following clause subsumed by 92 during input processing: 0 [] {-} c_lessequals(A,B,tc_fun(C,tc_bool))|hBOOL(hAPP(hAPP(c_in(C),D),A))| -c_lessequals(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool)).
% 0.21/0.47 Following clause subsumed by 45 during input processing: 0 [] {-} c_lessequals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lessequals(A,C,tc_fun(D,tc_bool))|hBOOL(hAPP(hAPP(c_in(D),B),A)).
% 0.21/0.47 Following clause subsumed by 109 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,B,A)|c_lessequals(B,B,A).
% 0.21/0.47 Following clause subsumed by 109 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_lessequals(B,C,A)|c_HOL_Oord__class_Oless(C,B,A).
% 0.21/0.47 Following clause subsumed by 111 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)| -c_lessequals(B,C,A)| -c_HOL_Oord__class_Oless(C,B,A).
% 0.21/0.47 Following clause subsumed by 109 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|c_lessequals(C,B,A).
% 0.21/0.47 Following clause subsumed by 123 during input processing: 0 [] {-} c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))| -c_lessequals(B,D,tc_fun(C,tc_bool))| -c_lessequals(A,D,tc_fun(C,tc_bool)).
% 0.21/0.47 Following clause subsumed by 124 during input processing: 0 [] {-} -class_Lattices_Oupper__semilattice(A)|c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)| -c_lessequals(C,D,A)| -c_lessequals(B,D,A).
% 0.21/0.47 Following clause subsumed by 124 during input processing: 0 [] {-} -class_Lattices_Oupper__semilattice(A)|c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)| -c_lessequals(C,D,A)| -c_lessequals(B,D,A).
% 0.21/0.47 Following clause subsumed by 138 during input processing: 0 [] {-} -class_Lattices_Olower__semilattice(A)|c_lessequals(B,C,A)| -c_lessequals(B,c_Lattices_Olower__semilattice__class_Oinf(C,D,A),A).
% 0.21/0.47 Following clause subsumed by 139 during input processing: 0 [] {-} -class_Lattices_Olower__semilattice(A)|c_lessequals(B,C,A)| -c_lessequals(B,c_Lattices_Olower__semilattice__class_Oinf(D,C,A),A).
% 0.21/0.47 Following clause subsumed by 154 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),C))| -c_lessequals(D,C,tc_fun(A,tc_bool))| -hBOOL(hAPP(hAPP(c_in(A),B),D)).
% 0.21/0.47 Following clause subsumed by 154 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),C))| -hBOOL(hAPP(hAPP(c_in(A),B),D))| -c_lessequals(D,C,tc_fun(A,tc_bool)).
% 0.21/0.47 Following clause subsumed by 154 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),C))| -hBOOL(hAPP(hAPP(c_in(A),B),D))| -c_lessequals(D,C,tc_fun(A,tc_bool)).
% 0.21/0.47 Following clause subsumed by 45 during input processing: 0 [] {-} c_lessequals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lessequals(A,C,tc_fun(D,tc_bool))| -c_lessequals(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)).
% 0.21/0.47 Following clause subsumed by 106 during input processing: 0 [] {-} c_Finite__Set_Ocard(c_Set_Oimage(A,B,C,D),D)=c_Finite__Set_Ocard(B,C)| -c_Fun_Oinj__on(A,B,C,D)| -c_Finite__Set_Ofinite(B,C).
% 0.21/0.47 Following clause subsumed by 174 during input processing: 0 [] {-} c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(A,C)| -c_Finite__Set_Ofinite(B,C).
% 0.21/0.47 Following clause subsumed by 208 during input processing: 0 [] {-} c_Option_Ooption_OSome(A,B)!=c_Option_Ooption_ONone(B).
% 0.21/0.47 Following clause subsumed by 237 during input processing: 0 [] {-} c_lessequals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -hBOOL(hAPP(hAPP(c_in(D),B),A))| -c_lessequals(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)).
% 0.21/0.47 Following clause subsumed by 256 during input processing: 0 [] {-} c_Option_Ooption_ONone(A)!=c_Option_Ooption_OSome(B,A).
% 0.21/0.47 Following clause subsumed by 186 during input processing: 0 [] {-} c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool))|hBOOL(hAPP(hAPP(c_in(C),A),B)).
% 0.21/0.47 Following clause subsumed by 269 during input processing: 0 [] {-} c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OSKIP.
% 0.21/0.47 Following clause subsumed by 287 during input processing: 0 [] {-} hAPP(A,B)!=c_Option_Ooption_OSome(C,D)|hAPP(c_Map_Omap__add(E,A,F,D),B)=c_Option_Ooption_OSome(C,D).
% 0.21/0.47 Following clause subsumed by 300 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Lattices_Olower__semilattice__class_Oinf(C,D,tc_fun(A,tc_bool))))| -hBOOL(hAPP(hAPP(c_in(A),B),D))| -hBOOL(hAPP(hAPP(c_in(A),B),C)).
% 0.21/0.47 Following clause subsumed by 302 during input processing: 0 [] {-} hBOOL(hAPP(A,B))| -hBOOL(hAPP(hAPP(c_in(C),B),D))| -hBOOL(hAPP(A,c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__3(D,A,C)))|hBOOL(hAPP(hAPP(c_in(C),c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__3(D,E,C)),D)).
% 0.21/0.47 Following clause subsumed by 301 during input processing: 0 [] {-} hBOOL(hAPP(A,B))| -hBOOL(hAPP(hAPP(c_in(C),B),D))| -hBOOL(hAPP(E,c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__3(D,E,C)))|hBOOL(hAPP(hAPP(c_in(C),c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__3(D,A,C)),D)).
% 0.21/0.47 Following clause subsumed by 304 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Set_Oinsert(C,D,A)))| -hBOOL(hAPP(hAPP(c_in(A),B),D)).
% 0.21/0.47 Following clause subsumed by 307 during input processing: 0 [] {-} hBOOL(hAPP(A,B))| -hBOOL(hAPP(hAPP(c_in(C),B),c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)))).
% 0.21/0.47 Following clause subsumed by 307 during input processing: 0 [] {-} -hBOOL(hAPP(hAPP(c_in(A),B),c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)))).
% 0.21/0.47 Following clause subsumed by 307 during input processing: 0 [] {-} -hBOOL(hAPP(hAPP(c_in(A),B),c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)))).
% 0.21/0.47 Following clause subsumed by 306 during input processing: 0 [factor_simp] {-} hBOOL(hAPP(hAPP(c_in(A),c_ATP__Linkup_Osko__Set__XbexCI__1__1(B,C,A)),B))| -hBOOL(hAPP(hAPP(c_in(A),E),B))| -hBOOL(hAPP(C,E)).
% 0.21/0.47 Following clause subsumed by 172 during input processing: 0 [flip.1] {-} c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OSKIP.
% 0.21/0.47 Following clause subsumed by 331 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|c_HOL_Oord__class_Oless(C,B,A)|C=B.
% 0.21/0.47 Following clause subsumed by 331 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|C=B|c_HOL_Oord__class_Oless(C,B,A).
% 0.21/0.47 Following clause subsumed by 331 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_HOL_Oord__class_Oless(B,C,A)|c_HOL_Oord__class_Oless(C,B,A).
% 0.21/0.47 Following clause subsumed by 322 during input processing: 0 [] {-} c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OSKIP.
% 0.21/0.47 Following clause subsumed by 291 during input processing: 0 [] {-} c_Com_Ocom_OBODY(A)!=c_Com_Ocom_OSKIP.
% 0.21/0.47 Following clause subsumed by 345 during input processing: 0 [] {-} c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OSKIP.
% 0.21/0.47 Following clause subsumed by 360 during input processing: 0 [flip.1] {-} c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OSKIP.
% 0.21/0.47 Following clause subsumed by 391 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_HOL_Oord__class_Oless(B,C,A)| -c_HOL_Oord__class_Oless(C,B,A).
% 0.21/0.48 Following clause subsumed by 397 during input processing: 0 [factor_simp] {-} hBOOL(hAPP(A,B))| -hBOOL(hAPP(hAPP(c_in(C),B),D))| -hBOOL(hAPP(A,c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__3(D,A,C))).
% 0.21/0.48 Following clause subsumed by 399 during input processing: 0 [factor_simp] {-} hBOOL(hAPP(A,B))| -hBOOL(hAPP(hAPP(c_in(C),B),D))|hBOOL(hAPP(hAPP(c_in(C),c_ATP__Linkup_Osko__Complete__Lattice__Xball__conj__distrib__1__3(D,A,C)),D)).
% 0.21/0.48 Following clause subsumed by 299 during input processing: 0 [] {-} hBOOL(hAPP(A,c_ATP__Linkup_Osko__Set__XbexCI__1__1(B,A,C)))| -hBOOL(hAPP(hAPP(c_in(C),D),B))| -hBOOL(hAPP(A,D)).
% 0.21/0.48 Following clause subsumed by 407 during input processing: 0 [] {-} hAPP(A,B)!=hAPP(A,C)| -hBOOL(hAPP(hAPP(c_in(D),C),E))| -hBOOL(hAPP(hAPP(c_in(D),B),E))| -c_Fun_Oinj__on(A,E,D,F)|B=C.
% 0.21/0.48 Following clause subsumed by 407 during input processing: 0 [] {-} hAPP(A,B)!=hAPP(A,C)| -hBOOL(hAPP(hAPP(c_in(D),C),E))| -hBOOL(hAPP(hAPP(c_in(D),B),E))| -c_Fun_Oinj__on(A,E,D,F)|B=C.
% 0.21/0.48 Following clause subsumed by 407 during input processing: 0 [] {-} hAPP(A,B)!=hAPP(A,C)| -c_Fun_Oinj__on(A,D,E,F)|B=C| -hBOOL(hAPP(hAPP(c_in(E),C),D))| -hBOOL(hAPP(hAPP(c_in(E),B),D)).
% 0.21/0.48 Following clause subsumed by 307 during input processing: 0 [] {-} -hBOOL(hAPP(A,B))| -hBOOL(hAPP(hAPP(c_in(C),B),c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)))).
% 0.21/0.48 Following clause subsumed by 413 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_HOL_Ominus__class_Ominus(C,D,tc_fun(A,tc_bool))))|hBOOL(hAPP(hAPP(c_in(A),B),D))| -hBOOL(hAPP(hAPP(c_in(A),B),C)).
% 0.21/0.48 Following clause subsumed by 419 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(C,D,E,tc_fun(A,tc_bool))))| -hBOOL(hAPP(hAPP(c_in(A),B),hAPP(D,F)))| -hBOOL(hAPP(hAPP(c_in(E),F),C)).
% 0.21/0.48 Following clause subsumed by 423 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Set_Ovimage(C,D,A,E)))| -hBOOL(hAPP(hAPP(c_in(E),hAPP(C,B)),D)).
% 0.21/0.48 Following clause subsumed by 423 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Set_Ovimage(C,D,A,E)))| -hBOOL(hAPP(hAPP(c_in(E),hAPP(C,B)),D)).
% 0.21/0.48 Following clause subsumed by 424 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),hAPP(B,C)),D))| -hBOOL(hAPP(hAPP(c_in(E),C),c_Set_Ovimage(B,D,E,A))).
% 0.21/0.48 Following clause subsumed by 435 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(A,B,C,tc_fun(D,tc_fun(E,tc_bool))),F),G))| -hBOOL(hAPP(hAPP(hAPP(B,H),F),G))| -hBOOL(hAPP(hAPP(c_in(C),H),A)).
% 0.21/0.48 Following clause subsumed by 436 during input processing: 0 [] {-} hBOOL(hAPP(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(A,B,C,tc_fun(D,tc_bool)),E))| -hBOOL(hAPP(hAPP(B,F),E))| -hBOOL(hAPP(hAPP(c_in(C),F),A)).
% 0.21/0.48 Following clause subsumed by 441 during input processing: 0 [] {-} -hBOOL(hAPP(hAPP(c_in(A),B),C))|hBOOL(hAPP(hAPP(c_in(D),hAPP(E,B)),c_Set_Oimage(E,C,A,D))).
% 0.21/0.48 Following clause subsumed by 441 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),hAPP(B,C)),c_Set_Oimage(B,D,E,A)))| -hBOOL(hAPP(hAPP(c_in(E),C),D)).
% 0.21/0.48 Following clause subsumed by 441 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),hAPP(B,C)),c_Set_Oimage(B,D,E,A)))| -hBOOL(hAPP(hAPP(c_in(E),C),D)).
% 0.21/0.48 111 back subsumes 110.
% 0.21/0.48 Following clause subsumed by 378 during input processing: 0 [copy,173,flip.1] {-} c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OBODY(C).
% 0.21/0.48 Following clause subsumed by 276 during input processing: 0 [copy,175,flip.1] {-} c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OBODY(D).
% 0.21/0.48 Following clause subsumed by 219 during input processing: 0 [copy,178,flip.1] {-} c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OWhile(D,E).
% 0.21/0.48 Following clause subsumed by 194 during input processing: 0 [copy,180,flip.1] {-} c_Com_Ocom_OBODY(A)!=c_Com_Ocom_OAss(B,C).
% 0.21/0.48 Following clause subsumed by 369 during input processing: 0 [copy,183,flip.1] {-} c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OSemi(C,D).
% 0.21/0.48 Following clause subsumed by 201 during input processing: 0 [copy,184,flip.1] {-} c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OSemi(D,E).
% 0.21/0.48 Following clause subsumed by 350 during input processing: 0 [copy,186,flip.1] {-} c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oinsert(B,C,A).
% 0.21/0.48 Following clause subsumed by 279 during input processing: 0 [copy,187,flip.1] {-} c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OSemi(D,E).
% 0.21/0.48 Following clause subsumed by 211 during input processing: 0 [copy,191,flip.1] {-} c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OLocal(C,D,E).
% 0.21/0.48 Following clause subsumed by 180 during input processing: 0 [copy,194,flip.1] {-} c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OBODY(C).
% 0.21/0.48 Following clause subsumed by 283 during input processing: 0 [copy,195,flip.1] {-} c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OCond(C,D,E).
% 0.21/0.48 Following clause subsumed by 244 during input processing: 0 [copy,196,flip.1] {-} c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OCond(D,E,F).
% 0.21/0.48 Following clause subsumed by 184 during input processing: 0 [copy,201,flip.1] {-} c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OCond(C,D,E).
% 0.21/0.48 Following clause subsumed by 256 during input processing: 0 [copy,208,flip.1] {-} c_Option_Ooption_ONone(A)!=c_Option_Ooption_OSome(B,A).
% 0.21/0.48 Following clause subsumed by 348 during input processing: 0 [copy,210,flip.1] {-} c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OAss(C,D).
% 0.21/0.48 Following clause subsumed by 191 during input processing: 0 [copy,211,flip.1] {-} c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OAss(D,E).
% 0.21/0.48 Following clause subsumed by 214 during input processing: 0 [copy,213,flip.1] {-} c_Com_Ocom_OBODY(A)!=c_Com_Ocom_OCond(B,C,D).
% 0.21/0.48 Following clause subsumed by 213 during input processing: 0 [copy,214,flip.1] {-} c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OBODY(D).
% 0.21/0.48 Following clause subsumed by 178 during input processing: 0 [copy,219,flip.1] {-} c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OLocal(C,D,E).
% 0.21/0.48 Following clause subsumed by 329 during input processing: 0 [copy,242,flip.1] {-} c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OAss(C,D).
% 0.21/0.48 Following clause subsumed by 196 during input processing: 0 [copy,244,flip.1] {-} c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OLocal(D,E,F).
% 0.21/0.48 Following clause subsumed by 255 during input processing: 0 [copy,247,flip.1] {-} c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OBODY(C).
% 0.21/0.48 Following clause subsumed by 247 during input processing: 0 [copy,255,flip.1] {-} c_Com_Ocom_OBODY(A)!=c_Com_Ocom_OSemi(B,C).
% 0.21/0.48 Following clause subsumed by 208 during input processing: 0 [copy,256,flip.1] {-} c_Option_Ooption_OSome(A,B)!=c_Option_Ooption_ONone(B).
% 0.21/0.48 Following clause subsumed by 175 during input processing: 0 [copy,276,flip.1] {-} c_Com_Ocom_OBODY(A)!=c_Com_Ocom_OLocal(B,C,D).
% 0.21/0.48 Following clause subsumed by 187 during input processing: 0 [copy,279,flip.1] {-} c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OLocal(C,D,E).
% 0.21/0.48 Following clause subsumed by 195 during input processing: 0 [copy,283,flip.1] {-} c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OWhile(D,E).
% 0.21/0.48 Following clause subsumed by 315 during input processing: 0 [copy,289,flip.1] {-} c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OCond(C,D,E).
% 0.21/0.48 Following clause subsumed by 289 during input processing: 0 [copy,315,flip.1] {-} c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OAss(D,E).
% 0.21/0.48 Following clause subsumed by 242 during input processing: 0 [copy,329,flip.1] {-} c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OSemi(C,D).
% 0.21/0.48 Following clause subsumed by 210 during input processing: 0 [copy,348,flip.1] {-} c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OWhile(C,D).
% 0.21/0.48 Following clause subsumed by 186 during input processing: 0 [copy,350,flip.1] {-} c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)).
% 0.21/0.48 Following clause subsumed by 183 during input processing: 0 [copy,369,flip.1] {-} c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OWhile(C,D).
% 0.21/0.48 Following clause subsumed by 173 during input processing: 0 [copy,378,flip.1] {-} c_Com_Ocom_OBODY(A)!=c_Com_Ocom_OWhile(B,C).
% 0.21/0.48 397 back subsumes 302.
% 0.21/0.48 399 back subsumes 301.
% 0.21/0.48 406 back subsumes 285.
% 0.21/0.48
% 0.21/0.48 ------------> process sos:
% 0.21/0.48 Following clause subsumed by 557 during input processing: 0 [demod,555] {-} C=C.
% 0.21/0.48 Following clause subsumed by 557 during input processing: 0 [demod,553] {-} A=A.
% 0.21/0.48 Following clause subsumed by 587 during input processing: 0 [] {-} c_lessequals(A,A,tc_fun(B,tc_bool)).
% 0.21/0.48 Following clause subsumed by 557 during input processing: 0 [demod,555] {-} c_Option_Ooption_OSome(C,D)=c_Option_Ooption_OSome(C,D).
% 0.21/0.49 Following clause subsumed by 589 during input processing: 0 [] {-} hAPP(c_Fun_Ofun__upd(A,B,C,D,E),F)=hAPP(A,F)|F=B.
% 0.21/0.49 Following clause subsumed by 557 during input processing: 0 [demod,561] {-} c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)).
% 0.21/0.49 Following clause subsumed by 557 during input processing: 0 [demod,602] {-} c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(B,c_COMBB(E,A,D,tc_fun(F,tc_bool),C),C,tc_fun(F,tc_bool))=c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(B,c_COMBB(E,A,D,tc_fun(F,tc_bool),C),C,tc_fun(F,tc_bool)).
% 0.21/0.49 Following clause subsumed by 557 during input processing: 0 [demod,646] {-} c_Hoare__Mirabelle_OMGT(v_c)=c_Hoare__Mirabelle_OMGT(v_c).
% 0.21/0.49 Following clause subsumed by 686 during input processing: 0 [] {-} c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)=c_Set_Oinsert(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C).
% 0.21/0.49 Following clause subsumed by 739 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Set_Oinsert(B,C,A))).
% 0.21/0.49 Following clause subsumed by 739 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(c_in(A),B),c_Set_Oinsert(B,C,A))).
% 0.21/0.49 Following clause subsumed by 720 during input processing: 0 [demod,734] {-} hBOOL(hAPP(c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),A),B)).
% 0.21/0.49 Following clause subsumed by 557 during input processing: 0 [] {-} A=A.
% 0.21/0.49 Following clause subsumed by 557 during input processing: 0 [copy,557,flip.1] {-} A=A.
% 0.21/0.49 557 back subsumes 536.
% 0.21/0.49 557 back subsumes 535.
% 0.21/0.49 557 back subsumes 520.
% 0.21/0.49 557 back subsumes 519.
% 0.21/0.49 557 back subsumes 518.
% 0.21/0.49 557 back subsumes 517.
% 0.21/0.49 557 back subsumes 489.
% 0.21/0.49 557 back subsumes 481.
% 0.21/0.49 557 back subsumes 480.
% 0.21/0.49 566 back subsumes 551.
% 0.21/0.49 587 back subsumes 496.
% 0.21/0.49 Following clause subsumed by 699 during input processing: 0 [copy,593,flip.1] {-} c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Set_Oimage(c_COMBK(B,A,C),c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,A).
% 0.21/0.49 Following clause subsumed by 622 during input processing: 0 [copy,622,flip.1] {-} c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(A,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)).
% 0.21/0.49 Following clause subsumed by 640 during input processing: 0 [copy,640,flip.1] {-} c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,A,tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 784 during input processing: 0 [copy,648,flip.1,demod,727,655] {-} c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),A),C,tc_fun(A,tc_bool))=c_Set_Oinsert(B,C,A).
% 0.21/0.49 664 back subsumes 506.
% 0.21/0.49 664 back subsumes 505.
% 0.21/0.49 Following clause subsumed by 678 during input processing: 0 [copy,678,flip.1] {-} c_Lattices_Olower__semilattice__class_Oinf(A,c_Lattices_Olower__semilattice__class_Oinf(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))=c_Lattices_Olower__semilattice__class_Oinf(B,c_Lattices_Olower__semilattice__class_Oinf(A,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)).
% 0.21/0.49 Following clause subsumed by 686 during input processing: 0 [copy,686,flip.1] {-} c_Set_Oinsert(A,c_Set_Oinsert(B,C,D),D)=c_Set_Oinsert(B,c_Set_Oinsert(A,C,D),D).
% 0.21/0.49 Following clause subsumed by 699 during input processing: 0 [copy,692,flip.1] {-} c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Set_Oimage(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,A).
% 0.21/0.49 692 back subsumes 593.
% 0.21/0.49 Following clause subsumed by 694 during input processing: 0 [copy,694,flip.1] {-} c_Lattices_Olower__semilattice__class_Oinf(A,B,tc_fun(C,tc_bool))=c_Lattices_Olower__semilattice__class_Oinf(B,A,tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 692 during input processing: 0 [copy,699,flip.1] {-} c_Set_Oimage(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B,C)=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)).
% 0.21/0.49 739 back subsumes 731.
% 0.21/0.49 751 back subsumes 750.
% 0.21/0.49 Following clause subsumed by 571 during input processing: 0 [copy,775,flip.1] {-} c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,B,C),D,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,c_Set_Oinsert(A,D,C),tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 588 during input processing: 0 [copy,782,flip.1] {-} c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,C,tc_fun(E,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(A,D,C,tc_fun(E,tc_bool)),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(B,D,C,tc_fun(E,tc_bool)),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 590 during input processing: 0 [copy,783,flip.1] {-} c_Set_Oimage(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D,E)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(A,B,D,E),c_Set_Oimage(A,C,D,E),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 592 during input processing: 0 [copy,784,flip.1] {-} c_Set_Oinsert(A,B,C)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),B,tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 598 during input processing: 0 [copy,785,flip.1] {-} c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Set_Oinsert(A,B,C),D,C,tc_fun(E,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(hAPP(D,A),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(B,D,C,tc_fun(E,tc_bool)),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 812 during input processing: 0 [copy,786,flip.1] {-} c_HOL_Ominus__class_Ominus(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Lattices_Olower__semilattice__class_Oinf(B,A,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)),c_HOL_Ominus__class_Ominus(c_Lattices_Olower__semilattice__class_Oinf(A,C,tc_fun(D,tc_bool)),B,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)).
% 0.21/0.49 Following clause subsumed by 614 during input processing: 0 [copy,787,flip.1] {-} c_Map_Odom(c_Map_Omap__add(A,B,C,D),C,D)=c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(B,C,D),c_Map_Odom(A,C,D),tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 643 during input processing: 0 [copy,790,flip.1] {-} c_Set_Ovimage(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),E,D)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Ovimage(A,B,E,D),c_Set_Ovimage(A,C,E,D),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 650 during input processing: 0 [copy,791,flip.1] {-} c_Set_Ovimage(A,c_Set_Oinsert(B,C,D),E,D)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Ovimage(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),E,D),c_Set_Ovimage(A,C,E,D),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 653 during input processing: 0 [copy,792,flip.1] {-} c_Set_Ovimage(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),E,D)=c_HOL_Ominus__class_Ominus(c_Set_Ovimage(A,B,E,D),c_Set_Ovimage(A,C,E,D),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 656 during input processing: 0 [copy,798,flip.1] {-} c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,C,tc_fun(D,tc_bool)),c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)).
% 0.21/0.49 Following clause subsumed by 657 during input processing: 0 [copy,799,flip.1] {-} c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)).
% 0.21/0.49 Following clause subsumed by 672 during input processing: 0 [copy,806,flip.1] {-} c_HOL_Ominus__class_Ominus(A,A,tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)).
% 0.21/0.49 Following clause subsumed by 679 during input processing: 0 [copy,807,flip.1] {-} c_Map_Odom(c_Fun_Ofun__upd(A,B,c_Option_Ooption_ONone(C),D,tc_Option_Ooption(C)),D,C)=c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)).
% 0.21/0.49 Following clause subsumed by 689 during input processing: 0 [copy,808,flip.1] {-} hAPP(hAPP(c_COMBC(A,B,C,D),E),F)=hAPP(hAPP(A,F),E).
% 0.21/0.49 Following clause subsumed by 811 during input processing: 0 [copy,809,flip.1] {-} c_HOL_Ominus__class_Ominus(c_Lattices_Olower__semilattice__class_Oinf(A,B,tc_fun(C,tc_bool)),A,tc_fun(C,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 705 during input processing: 0 [copy,810,flip.1] {-} c_Set_Ovimage(A,c_Lattices_Olower__semilattice__class_Oinf(B,C,tc_fun(D,tc_bool)),E,D)=c_Lattices_Olower__semilattice__class_Oinf(c_Set_Ovimage(A,B,E,D),c_Set_Ovimage(A,C,E,D),tc_fun(E,tc_bool)).
% 0.21/0.49 Following clause subsumed by 809 during input processing: 0 [copy,811,flip.1] {-} c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_HOL_Ominus__class_Ominus(c_Lattices_Olower__semilattice__class_Oinf(B,C,tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool)).
% 0.21/0.49 Following clause subsumed by 786 during input processing: 0 [copy,812,flip.1] {-} c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Lattices_Olower__semilattice__class_Oinf(B,A,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)),c_HOL_Ominus__class_Ominus(c_Lattices_Olower__semilattice__class_Oinf(A,D,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Lattices_Oupper__semilattice__class_Osup(B,D,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)).
% 0.21/0.49 Following clause subsumed by 719 during input processing: 0 [copy,816,flip.1] {-} c_Set_Oinsert(A,c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),C,B,tc_fun(D,tc_bool)),D)=c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D).
% 0.21/0.49 Following clause subsumed by 735 during input processing: 0 [copy,821,flip.1] {-} c_Set_Ovimage(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),C,B)=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)).
% 0.21/0.49
% 0.21/0.49 ======= end of input processing =======
% 0.45/0.66
% 0.45/0.66
% 0.45/0.66 Failed to model usable list: disabling FINDER
% 0.45/0.66
% 0.45/0.66
% 0.45/0.66
% 0.45/0.66 -------------- Softie stats --------------
% 0.45/0.66
% 0.45/0.66 UPDATE_STOP: 300
% 0.45/0.66 SFINDER_TIME_LIMIT: 2
% 0.45/0.66 SHORT_CLAUSE_CUTOFF: 4
% 0.45/0.66 number of clauses in intial UL: 485
% 0.45/0.66 number of clauses initially in problem: 716
% 0.45/0.66 percentage of clauses intially in UL: 67
% 0.45/0.66 percentage of distinct symbols occuring in initial UL: 66
% 0.45/0.66 percent of all initial clauses that are short: 99
% 0.45/0.66 absolute distinct symbol count: 136
% 0.45/0.66 distinct predicate count: 28
% 0.45/0.66 distinct function count: 90
% 0.45/0.66 distinct constant count: 18
% 0.45/0.66
% 0.45/0.66 ---------- no more Softie stats ----------
% 0.45/0.66
% 0.45/0.66
% 0.45/0.66
% 0.45/0.66 =========== start of search ===========
% 2.22/2.49
% 2.22/2.49
% 2.22/2.49 Changing weight limit from 60 to 53.
% 2.22/2.49
% 2.22/2.49 Resetting weight limit to 53 after 35 givens.
% 2.22/2.49
% 3.50/3.72
% 3.50/3.72
% 3.50/3.72 Changing weight limit from 53 to 45.
% 3.50/3.72
% 3.50/3.72 Resetting weight limit to 45 after 40 givens.
% 3.50/3.72
% 4.11/4.35
% 4.11/4.35
% 4.11/4.35 Changing weight limit from 45 to 35.
% 4.11/4.35
% 4.11/4.35 Resetting weight limit to 35 after 45 givens.
% 4.11/4.35
% 4.35/4.57
% 4.35/4.57
% 4.35/4.57 Changing weight limit from 35 to 30.
% 4.35/4.57
% 4.35/4.57 Resetting weight limit to 30 after 50 givens.
% 4.35/4.57
% 4.51/4.69
% 4.51/4.69
% 4.51/4.69 Changing weight limit from 30 to 28.
% 4.51/4.69
% 4.51/4.69 Resetting weight limit to 28 after 55 givens.
% 4.51/4.69
% 4.64/4.86
% 4.64/4.86
% 4.64/4.86 Changing weight limit from 28 to 25.
% 4.64/4.86
% 4.64/4.86 Resetting weight limit to 25 after 60 givens.
% 4.64/4.86
% 4.70/4.94 c_Fun_Ofun__upd(c_Fun_Ofun__upd(A,B,c_Option_Ooption_OSome(C,D),E,F),B,c_Option_Ooption_OSome(C,D),G,tc_Option_Ooption(D))=c_Fun_Ofun__upd(A,B,c_Option_Ooption_OSome(C,D),E,F).
% 4.70/4.94
% 4.70/4.94 ------------- memory usage ------------
% 4.70/4.94 478 mallocs of 32700 bytes each, 15264.3 K.
% 4.70/4.94 type (bytes each) gets frees in use avail bytes
% 4.70/4.94 sym_ent ( 304) 290 0 290 0 86.1 K
% 4.70/4.94 term ( 32) 555766 526417 29349 14526 1371.1 K
% 4.70/4.94 rel ( 40) 495989 448967 47022 45467 3612.9 K
% 4.70/4.94 term_ptr ( 16) 662132 506336 155796 204707 5632.9 K
% 4.70/4.94 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 4.70/4.94 fpa_head ( 24) 19929 7951 11978 4760 392.3 K
% 4.70/4.94 fpa_tree ( 56) 30288 30288 0 1951 106.7 K
% 4.70/4.94 context (1288) 83710 83710 0 7 8.8 K
% 4.70/4.94 trail ( 24) 3512228 3512228 0 14 0.3 K
% 4.70/4.94 imd_tree ( 32) 1034 212 822 24 26.4 K
% 4.70/4.94 imd_pos (4024) 101697 101697 0 14 55.0 K
% 4.70/4.94 is_tree ( 24) 71003 53325 17678 40789 1370.3 K
% 4.70/4.94 is_pos (2424) 4558414 4558414 0 32 75.8 K
% 4.70/4.94 fsub_pos ( 16) 64430 64430 0 1 0.0 K
% 4.70/4.94 literal ( 32) 47828 32143 15685 3501 599.6 K
% 4.70/4.94 clause ( 88) 17337 10624 6713 623 630.4 K
% 4.70/4.94 list ( 272) 10 3 7 1 2.1 K
% 4.70/4.94 clash_nd ( 80) 900 900 0 5 0.4 K
% 4.70/4.94 clause_ptr ( 16) 11046 4915 6131 622 105.5 K
% 4.70/4.94 int_ptr ( 16) 120773 71686 49087 5920 859.5 K
% 4.70/4.94 ci_ptr ( 24) 0 0 0 0 0.0 K
% 4.70/4.94 link_node ( 120) 0 0 0 0 0.0 K
% 4.70/4.94 ans_lit_node( 24) 0 0 0 0 0.0 K
% 4.70/4.94 formula_box( 168) 0 0 0 0 0.0 K
% 4.70/4.94 formula( 40) 0 0 0 0 0.0 K
% 4.70/4.94 formula_ptr( 16) 0 0 0 0 0.0 K
% 4.70/4.94 cl_attribute( 24) 0 0 0 0 0.0 K
% 4.70/4.94
% 4.70/4.94 ********** is_delete, can't find end.
% 4.70/4.94 0
% 4.70/4.94 conflict time 0.00
% 4.70/4.94 new demod time 0.00
% 4.70/4.94 post_process time 0.00
% 4.70/4.94 back demod time 0.00
% 4.70/4.94 back subsume 0.00
% 4.70/4.94 factor time 0.00
% 4.70/4.94 FINDER time 0.00
% 4.70/4.94 unindex time 0.00
% 4.70/4.94
% 4.70/4.94 Forward subsumption counts, subsumer:number_subsumed.
% 4.70/4.94 1:0 2:0 3:2 4:0 5:0 6:0 7:4 8:0 9:0 10:0
% 4.70/4.94 11:0 12:0 13:1 14:0 15:0 16:0 17:0 18:0 19:0 20:0
% 4.70/4.94 21:0 22:7 23:6 24:0 25:0 26:0 27:0 28:0 29:0 30:0
% 4.70/4.94 31:0 32:0 33:0 34:0 35:0 36:0 37:0 38:0 39:1 40:0
% 4.70/4.94 41:0 42:0 43:0 44:0 45:3 46:0 47:0 48:0 49:0 50:0
% 4.70/4.94 51:0 52:0 53:1 54:0 55:0 56:1 57:1 58:0 59:0 60:0
% 4.70/4.94 61:0 62:0 63:0 64:0 65:0 66:0 67:0 68:1 69:0 70:0
% 4.70/4.94 71:1 72:0 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 4.70/4.94 81:1 82:0 83:6 84:1 85:8 86:1 87:1 88:0 89:0 90:0
% 4.70/4.94 91:0 92:1 93:0 94:0 95:0 96:0 97:0 98:0 99:0
% 4.70/4.94 All others: 2264.
% 4.70/4.94
% 4.70/4.94 ********** ABNORMAL END **********
% 4.70/4.94
% 4.70/4.94 ********** is_delete, can't find end.
%------------------------------------------------------------------------------