%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NUM926+7 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 14:23:19 EDT 2022
% Result : Unknown 0.77s 0.94s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM926+7 : TPTP v8.1.0. Released v5.3.0.
% 0.11/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n026.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Wed Jul 6 09:24:38 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.45/0.62 ----- Otter 3.2, August 2001 -----
% 0.45/0.62 The process was started by sandbox on n026.cluster.edu,
% 0.45/0.62 Wed Jul 6 09:24:38 2022
% 0.45/0.62 The command was "./sos". The process ID is 9880.
% 0.45/0.62
% 0.45/0.62 set(prolog_style_variables).
% 0.45/0.62 set(auto).
% 0.45/0.62 dependent: set(auto1).
% 0.45/0.62 dependent: set(process_input).
% 0.45/0.62 dependent: clear(print_kept).
% 0.45/0.62 dependent: clear(print_new_demod).
% 0.45/0.62 dependent: clear(print_back_demod).
% 0.45/0.62 dependent: clear(print_back_sub).
% 0.45/0.62 dependent: set(control_memory).
% 0.45/0.62 dependent: assign(max_mem, 12000).
% 0.45/0.62 dependent: assign(pick_given_ratio, 4).
% 0.45/0.62 dependent: assign(stats_level, 1).
% 0.45/0.62 dependent: assign(pick_semantic_ratio, 3).
% 0.45/0.62 dependent: assign(sos_limit, 5000).
% 0.45/0.62 dependent: assign(max_weight, 60).
% 0.45/0.62 clear(print_given).
% 0.45/0.62
% 0.45/0.62 formula_list(usable).
% 0.45/0.62
% 0.45/0.62 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=7.
% 0.45/0.62
% 0.45/0.62 This ia a non-Horn set with equality. The strategy will be
% 0.45/0.62 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.45/0.62 unit deletion, with positive clauses in sos and nonpositive
% 0.45/0.62 clauses in usable.
% 0.45/0.62
% 0.45/0.62 dependent: set(knuth_bendix).
% 0.45/0.62 dependent: set(para_from).
% 0.45/0.62 dependent: set(para_into).
% 0.45/0.62 dependent: clear(para_from_right).
% 0.45/0.62 dependent: clear(para_into_right).
% 0.45/0.62 dependent: set(para_from_vars).
% 0.45/0.62 dependent: set(eq_units_both_ways).
% 0.45/0.62 dependent: set(dynamic_demod_all).
% 0.45/0.62 dependent: set(dynamic_demod).
% 0.45/0.62 dependent: set(order_eq).
% 0.45/0.62 dependent: set(back_demod).
% 0.45/0.62 dependent: set(lrpo).
% 0.45/0.62 dependent: set(hyper_res).
% 0.45/0.62 dependent: set(unit_deletion).
% 0.45/0.62 dependent: set(factor).
% 0.45/0.62
% 0.45/0.62 ------------> process usable:
% 0.45/0.62 Following clause subsumed by 64 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit1(A)),bit1(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.45/0.62 Following clause subsumed by 65 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit1(A)),bit1(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.45/0.62 Following clause subsumed by 66 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit1(A)),bit1(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.45/0.62 Following clause subsumed by 67 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit1(A)),bit1(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.45/0.62 Following clause subsumed by 69 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit0(A)),bit0(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.45/0.62 Following clause subsumed by 70 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit0(A)),bit0(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.45/0.62 Following clause subsumed by 71 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit0(A)),bit0(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.45/0.62 Following clause subsumed by 72 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit0(A)),bit0(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.45/0.62 Following clause subsumed by 85 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit1(A)),bit0(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.45/0.62 Following clause subsumed by 86 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit1(A)),bit0(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.45/0.62 Following clause subsumed by 87 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit0(A)),bit1(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.45/0.62 Following clause subsumed by 88 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit0(A)),bit1(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.46/0.63 Following clause subsumed by 89 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,plus_plus(int,A),one_one(int))),B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.46/0.63 Following clause subsumed by 98 during input processing: 0 [flip.2] {-} -comm_semiring_1(A)|hAPP(A,A,times_times(A,hAPP(A,A,times_times(A,B),C)),D)=hAPP(A,A,times_times(A,B),hAPP(A,A,times_times(A,C),D)).
% 0.46/0.63 Following clause subsumed by 105 during input processing: 0 [flip.2] {-} -comm_semiring_1(A)|hAPP(A,A,plus_plus(A,hAPP(A,A,plus_plus(A,B),C)),D)=hAPP(A,A,plus_plus(A,B),hAPP(A,A,plus_plus(A,C),D)).
% 0.46/0.63 Following clause subsumed by 118 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit1(A)),bit0(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.46/0.63 Following clause subsumed by 119 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),bit1(A)),bit0(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.46/0.63 Following clause subsumed by 126 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit0(A)),bit1(B)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.46/0.63 Following clause subsumed by 127 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),bit0(A)),bit1(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B)).
% 0.46/0.63 Following clause subsumed by 144 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)=ti(A,C)|ti(A,D)=ti(A,E)|hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,B),D)),hAPP(A,A,times_times(A,C),E))!=hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,B),E)),hAPP(A,A,times_times(A,C),D)).
% 0.46/0.63 Following clause subsumed by 145 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,B),D)),hAPP(A,A,times_times(A,C),E))=hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,B),E)),hAPP(A,A,times_times(A,C),D)).
% 0.46/0.63 Following clause subsumed by 146 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,D),B)),hAPP(A,A,times_times(A,E),C))=hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,D),C)),hAPP(A,A,times_times(A,E),B)).
% 0.46/0.63 Following clause subsumed by 154 during input processing: 0 [flip.1] {-} bit1(A)!=pls.
% 0.46/0.63 Following clause subsumed by 157 during input processing: 0 [flip.1,flip.2] {-} bit0(A)!=pls|ti(int,A)=pls.
% 0.46/0.63 Following clause subsumed by 158 during input processing: 0 [flip.1,flip.2] {-} bit0(A)=pls|ti(int,A)!=pls.
% 0.46/0.63 Following clause subsumed by 185 during input processing: 0 [] {-} -number_ring(A)|one_one(A)=number_number_of(A,bit1(pls)).
% 0.46/0.63 Following clause subsumed by 196 during input processing: 0 [] {-} -linordered_semidom(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),one_one(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(nat,A,power_power(A,B),C)),hAPP(nat,A,power_power(A,B),D)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),C),D)).
% 0.46/0.63 Following clause subsumed by 242 during input processing: 0 [flip.2] {-} -number_ring(A)|zero_zero(A)=number_number_of(A,pls).
% 0.46/0.63 Following clause subsumed by 210 during input processing: 0 [] {-} -ring_11004092258visors(A)|hAPP(nat,A,power_power(A,B),number_number_of(nat,bit0(bit1(pls))))!=zero_zero(A)|ti(A,B)=zero_zero(A).
% 0.46/0.63 Following clause subsumed by 232 during input processing: 0 [] {-} -linordered_semidom(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(nat,A,power_power(A,B),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,A,power_power(A,C),number_number_of(nat,bit0(bit1(pls))))))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),C)).
% 0.46/0.63 Following clause subsumed by 317 during input processing: 0 [] {-} -linordered_semidom(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),one_one(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(nat,A,power_power(A,B),C)),hAPP(nat,A,power_power(A,B),D)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),C),D)).
% 0.46/0.63 Following clause subsumed by 318 during input processing: 0 [] {-} -linordered_semidom(A)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),one_one(A)),D))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(nat,A,power_power(A,D),B)),hAPP(nat,A,power_power(A,D),C))).
% 0.46/0.63 Following clause subsumed by 332 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,power_power(nat,A),B)))|B=zero_zero(nat)|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.46/0.63 Following clause subsumed by 334 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,power_power(nat,A),B)))|B!=zero_zero(nat).
% 0.46/0.63 Following clause subsumed by 333 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,power_power(nat,A),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.46/0.63 Following clause subsumed by 332 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,power_power(nat,A),number_number_of(nat,B))))|number_number_of(nat,B)=zero_zero(nat)|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.46/0.63 Following clause subsumed by 334 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,power_power(nat,A),number_number_of(nat,B))))|number_number_of(nat,B)!=zero_zero(nat).
% 0.46/0.63 Following clause subsumed by 333 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,power_power(nat,A),number_number_of(nat,B))))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.46/0.63 Following clause subsumed by 336 during input processing: 0 [flip.1,flip.2] {-} bit1(A)!=min|ti(int,A)=min.
% 0.46/0.63 Following clause subsumed by 337 during input processing: 0 [flip.1,flip.2] {-} bit1(A)=min|ti(int,A)!=min.
% 0.46/0.63 Following clause subsumed by 338 during input processing: 0 [flip.1] {-} pls!=min.
% 0.46/0.63 Following clause subsumed by 339 during input processing: 0 [flip.1] {-} bit0(A)!=min.
% 0.46/0.63 Following clause subsumed by 364 during input processing: 0 [] {-} hAPP(int,int,times_times(int,A),B)!=one_one(int)|ti(int,A)=one_one(int)|ti(int,A)=number_number_of(int,min).
% 0.46/0.63 Following clause subsumed by 379 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,zcong(A,B),C))| -hBOOL(hAPP(int,bool,zcong(B,A),C)).
% 0.46/0.63 Following clause subsumed by 199 during input processing: 0 [] {-} -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_neq_one(A)|hAPP(nat,A,power_power(A,B),number_number_of(nat,C))!=zero_zero(A)|ti(A,B)=zero_zero(A).
% 0.46/0.63 Following clause subsumed by 200 during input processing: 0 [] {-} -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_neq_one(A)|hAPP(nat,A,power_power(A,B),number_number_of(nat,C))!=zero_zero(A)|number_number_of(nat,C)!=zero_zero(nat).
% 0.46/0.63 Following clause subsumed by 201 during input processing: 0 [] {-} -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_neq_one(A)|hAPP(nat,A,power_power(A,B),number_number_of(nat,C))=zero_zero(A)|ti(A,B)!=zero_zero(A)|number_number_of(nat,C)=zero_zero(nat).
% 0.46/0.63 Following clause subsumed by 211 during input processing: 0 [] {-} -power(A)| -semiring_0(A)|number_number_of(nat,B)!=zero_zero(nat)|hAPP(nat,A,power_power(A,zero_zero(A)),number_number_of(nat,B))=one_one(A).
% 0.46/0.63 Following clause subsumed by 212 during input processing: 0 [] {-} -power(A)| -semiring_0(A)|number_number_of(nat,B)=zero_zero(nat)|hAPP(nat,A,power_power(A,zero_zero(A)),number_number_of(nat,B))=zero_zero(A).
% 0.46/0.63 Following clause subsumed by 441 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,zcong(A,zero_zero(int)),B))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),B),A)).
% 0.46/0.64 Following clause subsumed by 442 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,zcong(A,zero_zero(int)),B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),B),A)).
% 0.46/0.64 Following clause subsumed by 399 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),A))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B))| -hBOOL(hAPP(int,bool,zcong(A,zero_zero(int)),B))|ti(int,A)=zero_zero(int).
% 0.46/0.64 Following clause subsumed by 445 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,zprime,A))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),B))| -hBOOL(hAPP(int,bool,zcong(hAPP(int,int,times_times(int,B),C),zero_zero(int)),A))|hBOOL(hAPP(int,bool,zcong(B,zero_zero(int)),A))|hBOOL(hAPP(int,bool,zcong(C,zero_zero(int)),A)).
% 0.46/0.64 Following clause subsumed by 445 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,zprime,A))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),B))|hBOOL(hAPP(int,bool,zcong(B,zero_zero(int)),A))|hBOOL(hAPP(int,bool,zcong(C,zero_zero(int)),A))| -hBOOL(hAPP(int,bool,zcong(hAPP(int,int,times_times(int,B),C),zero_zero(int)),A)).
% 0.46/0.64 Following clause subsumed by 241 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,zprime,A))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),A),hAPP(nat,int,power_power(int,B),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),C))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),A),B)).
% 0.46/0.64 Following clause subsumed by 464 during input processing: 0 [] {-} -hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less(real),A),B))|hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less_eq(real),A),B)).
% 0.46/0.64 Following clause subsumed by 463 during input processing: 0 [] {-} hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less(real),A),B))| -hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less_eq(real),A),B))|A=B.
% 0.46/0.64 Following clause subsumed by 474 during input processing: 0 [] {-} -no_zero_divisors(A)|ti(A,B)=zero_zero(A)|ti(A,C)=zero_zero(A)|hAPP(A,A,times_times(A,B),C)!=zero_zero(A).
% 0.46/0.64 Following clause subsumed by 480 during input processing: 0 [flip.2] {-} -zero_neq_one(A)|zero_zero(A)!=one_one(A).
% 0.46/0.64 Following clause subsumed by 514 during input processing: 0 [] {-} -ordered_ring(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),B),zero_zero(A)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),C),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),hAPP(A,A,times_times(A,B),C))).
% 0.46/0.64 Following clause subsumed by 512 during input processing: 0 [] {-} -ordere453448008miring(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),B),zero_zero(A)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,times_times(A,B),C)),zero_zero(A))).
% 0.46/0.64 Following clause subsumed by 512 during input processing: 0 [] {-} -ordere453448008miring(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),C),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,times_times(A,C),B)),zero_zero(A))).
% 0.46/0.64 Following clause subsumed by 511 during input processing: 0 [] {-} -ordere453448008miring(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),C),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,times_times(A,B),C)),zero_zero(A))).
% 0.46/0.64 Following clause subsumed by 536 during input processing: 0 [] {-} -linord581940658strict(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,times_times(A,B),C)),hAPP(A,A,times_times(A,B),D)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),D),C)).
% 0.46/0.64 Following clause subsumed by 542 during input processing: 0 [] {-} -linord20386208strict(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),zero_zero(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),C),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,times_times(A,C),B)),zero_zero(A))).
% 0.46/0.64 Following clause subsumed by 549 during input processing: 0 [] {-} -linord581940658strict(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,times_times(A,B),C)),hAPP(A,A,times_times(A,B),D)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),zero_zero(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),C),D)).
% 0.46/0.64 Following clause subsumed by 536 during input processing: 0 [] {-} -linord581940658strict(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,times_times(A,B),C)),hAPP(A,A,times_times(A,B),D)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),zero_zero(A)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),D),C)).
% 0.46/0.64 Following clause subsumed by 537 during input processing: 0 [] {-} -linord581940658strict(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,times_times(A,B),C)),hAPP(A,A,times_times(A,D),C)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),C),zero_zero(A)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),D),B)).
% 0.46/0.64 Following clause subsumed by 503 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,C),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),C)).
% 0.46/0.64 Following clause subsumed by 473 during input processing: 0 [] {-} hAPP(nat,nat,power_power(nat,A),B)=one_one(nat)|B!=zero_zero(nat).
% 0.46/0.64 Following clause subsumed by 639 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B)).
% 0.46/0.64 Following clause subsumed by 640 during input processing: 0 [] {-} A!=B| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),A)).
% 0.46/0.64 Following clause subsumed by 641 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),A)).
% 0.46/0.64 Following clause subsumed by 468 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|B!=A.
% 0.46/0.64 Following clause subsumed by 469 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A!=B.
% 0.46/0.64 Following clause subsumed by 469 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A!=B.
% 0.46/0.64 Following clause subsumed by 647 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),C),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),C),A)).
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A=B.
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A=B.
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|A=B| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A)).
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A=B.
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|B=A.
% 0.46/0.64 Following clause subsumed by 468 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|B!=A.
% 0.46/0.64 Following clause subsumed by 468 during input processing: 0 [] {-} A!=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B)).
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} A=B| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A)).
% 0.46/0.64 Following clause subsumed by 469 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A!=B.
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|B=A.
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A))|A=B.
% 0.46/0.64 Following clause subsumed by 468 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|A!=B.
% 0.46/0.64 Following clause subsumed by 468 during input processing: 0 [] {-} A!=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B)).
% 0.46/0.64 Following clause subsumed by 469 during input processing: 0 [] {-} A!=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A)).
% 0.46/0.64 Following clause subsumed by 467 during input processing: 0 [] {-} A=B| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),A)).
% 0.46/0.64 Following clause subsumed by 665 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),C))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,minus_minus(nat,B),A)),hAPP(nat,nat,minus_minus(nat,C),A)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.46/0.64 Following clause subsumed by 635 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),zero_zero(nat))).
% 0.46/0.64 Following clause subsumed by 671 during input processing: 0 [] {-} A!=zero_zero(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.46/0.64 Following clause subsumed by 635 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),zero_zero(nat))).
% 0.46/0.64 Following clause subsumed by 661 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),zero_zero(nat)))|A!=zero_zero(nat).
% 0.46/0.64 Following clause subsumed by 680 during input processing: 0 [] {-} hAPP(nat,nat,minus_minus(nat,A),B)=zero_zero(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.46/0.64 Following clause subsumed by 472 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)=zero_zero(nat)|A!=zero_zero(nat).
% 0.46/0.64 Following clause subsumed by 639 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|A!=B.
% 0.46/0.64 Following clause subsumed by 703 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|A=B.
% 0.46/0.64 Following clause subsumed by 702 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B)).
% 0.46/0.64 Following clause subsumed by 661 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|A!=B.
% 0.46/0.64 Following clause subsumed by 702 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.46/0.64 Following clause subsumed by 703 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|A=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B)).
% 0.46/0.65 Following clause subsumed by 702 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.46/0.65 Following clause subsumed by 661 during input processing: 0 [] {-} A!=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.46/0.65 Following clause subsumed by 721 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,plus_plus(nat,A),B)),C))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),C)).
% 0.46/0.65 Following clause subsumed by 720 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,plus_plus(nat,A),B)),C))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 728 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|hAPP(nat,nat,minus_minus(nat,hAPP(nat,nat,plus_plus(nat,C),B)),A)=hAPP(nat,nat,plus_plus(nat,C),hAPP(nat,nat,minus_minus(nat,B),A)).
% 0.46/0.65 Following clause subsumed by 468 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),one_one(nat)))|A!=one_one(nat).
% 0.46/0.65 Following clause subsumed by 504 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)!=one_one(nat)|A=one_one(nat).
% 0.46/0.65 Following clause subsumed by 505 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)!=one_one(nat)|B=one_one(nat).
% 0.46/0.65 Following clause subsumed by 506 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)=one_one(nat)|A!=one_one(nat)|B!=one_one(nat).
% 0.46/0.65 Following clause subsumed by 694 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,plus_plus(nat,A),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.46/0.65 Following clause subsumed by 695 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),hAPP(nat,nat,plus_plus(nat,A),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),B)).
% 0.46/0.65 Following clause subsumed by 745 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,A,hAPP(nat,nat,minus_minus(nat,B),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C))|hBOOL(hAPP(nat,bool,A,zero_zero(nat))).
% 0.46/0.65 Following clause subsumed by 746 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,A,hAPP(nat,nat,minus_minus(nat,B),C)))|B!=hAPP(nat,nat,plus_plus(nat,C),D)|hBOOL(hAPP(nat,bool,A,D)).
% 0.46/0.65 Following clause subsumed by 756 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,C),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),B))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),C)).
% 0.46/0.65 Following clause subsumed by 755 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 738 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 739 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,C),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),C)).
% 0.46/0.65 Following clause subsumed by 684 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)!=hAPP(nat,nat,times_times(nat,A),C)|A=zero_zero(nat)|B=C.
% 0.46/0.65 Following clause subsumed by 686 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)=hAPP(nat,nat,times_times(nat,A),C)|A!=zero_zero(nat).
% 0.46/0.65 Following clause subsumed by 685 during input processing: 0 [] {-} hAPP(nat,nat,times_times(nat,A),B)=hAPP(nat,nat,times_times(nat,A),C)|B!=C.
% 0.46/0.65 Following clause subsumed by 685 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))|hAPP(nat,nat,times_times(nat,A),B)=hAPP(nat,nat,times_times(nat,A),C)|B!=C.
% 0.46/0.65 Following clause subsumed by 760 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 755 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 502 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 767 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 502 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 768 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 738 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),hAPP(nat,nat,times_times(nat,A),B)),hAPP(nat,nat,times_times(nat,A),C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.46/0.65 Following clause subsumed by 208 during input processing: 0 [] {-} ti(int,A)=zero_zero(int)|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),B),C))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),hAPP(int,int,times_times(int,A),B)),hAPP(int,int,times_times(int,A),C))).
% 0.46/0.65 Following clause subsumed by 803 during input processing: 0 [] {-} -comm_ring(A)| -dvd(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),hAPP(A,A,plus_plus(A,D),E)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),hAPP(A,A,plus_plus(A,hAPP(A,A,minus_minus(A,D),hAPP(A,A,times_times(A,F),C))),E))).
% 0.46/0.65 Following clause subsumed by 802 during input processing: 0 [] {-} -comm_ring(A)| -dvd(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),hAPP(A,A,plus_plus(A,D),E)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),hAPP(A,A,plus_plus(A,hAPP(A,A,minus_minus(A,D),hAPP(A,A,times_times(A,F),C))),E))).
% 0.46/0.65 Following clause subsumed by 424 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),hAPP(int,int,minus_minus(int,B),one_one(int))))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.46/0.66 Following clause subsumed by 821 during input processing: 0 [] {-} -cancel_semigroup_add(A)|hAPP(A,A,plus_plus(A,B),C)!=hAPP(A,A,plus_plus(A,B),D)|ti(A,C)=ti(A,D).
% 0.46/0.66 Following clause subsumed by 823 during input processing: 0 [] {-} -cancel_semigroup_add(A)|hAPP(A,A,plus_plus(A,B),C)!=hAPP(A,A,plus_plus(A,D),C)|ti(A,B)=ti(A,D).
% 0.46/0.66 Following clause subsumed by 836 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,plus_plus(A,B),C)),hAPP(A,A,plus_plus(A,D),C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),B),D)).
% 0.46/0.66 Following clause subsumed by 838 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,plus_plus(A,B),C)),hAPP(A,A,plus_plus(A,B),D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),C),D)).
% 0.46/0.66 Following clause subsumed by 843 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,plus_plus(A,B),C)),hAPP(A,A,plus_plus(A,D),C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),D)).
% 0.46/0.66 Following clause subsumed by 845 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(A,A,plus_plus(A,B),C)),hAPP(A,A,plus_plus(A,B),D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),C),D)).
% 0.46/0.66 Following clause subsumed by 891 during input processing: 0 [] {-} -ordere216010020id_add(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),B))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),zero_zero(A)),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),zero_zero(A)),hAPP(A,A,plus_plus(A,B),C))).
% 0.46/0.66 Following clause subsumed by 389 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,zcong(A,hAPP(int,int,times_times(int,B),multInv(C,D))),C))|hBOOL(hAPP(int,bool,zcong(hAPP(int,int,times_times(int,A),D),hAPP(int,int,times_times(int,hAPP(int,int,times_times(int,B),multInv(C,D))),D)),C)).
% 0.46/0.66 Following clause subsumed by 951 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),zero_zero(nat)),A))|A=zero_zero(nat).
% 0.46/0.66 Following clause subsumed by 469 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),zero_zero(nat)),A))|A!=zero_zero(nat).
% 0.46/0.66 Following clause subsumed by 951 during input processing: 0 [] {-} A=zero_zero(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),zero_zero(nat)),A)).
% 0.46/0.66 Following clause subsumed by 469 during input processing: 0 [] {-} A!=zero_zero(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),zero_zero(nat)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),zero_zero(nat)),A)).
% 0.46/0.66 Following clause subsumed by 736 during input processing: 0 [] {-} A=one_one(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),one_one(nat))).
% 0.46/0.66 Following clause subsumed by 468 during input processing: 0 [] {-} A!=one_one(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),one_one(nat)),A))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),one_one(nat))).
% 0.46/0.66 Following clause subsumed by 736 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),one_one(nat)))|A=one_one(nat).
% 0.46/0.66 Following clause subsumed by 468 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),one_one(nat)))|A!=one_one(nat).
% 0.46/0.66 Following clause subsumed by 736 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),one_one(nat)))|A=one_one(nat).
% 0.46/0.66 Following clause subsumed by 594 during input processing: 0 [] {-} A=zero_zero(nat)| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),hAPP(nat,nat,power_power(nat,B),A)),hAPP(nat,nat,power_power(nat,C),A)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.46/0.66 Following clause subsumed by 510 during input processing: 0 [] {-} A=zero_zero(nat)|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),hAPP(nat,nat,power_power(nat,B),A)),hAPP(nat,nat,power_power(nat,C),A)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.46/0.66 Following clause subsumed by 949 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),hAPP(nat,int,power_power(int,A),B)),hAPP(nat,int,power_power(int,C),B)))|B=zero_zero(nat)|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),A),C)).
% 0.46/0.66 Following clause subsumed by 579 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|B=zero_zero(nat).
% 0.46/0.66 Following clause subsumed by 778 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))|hAPP(nat,nat,times_times(nat,A),B)!=hAPP(nat,nat,times_times(nat,A),C)|B=C.
% 0.46/0.66 Following clause subsumed by 957 during input processing: 0 [] {-} -real_normed_algebra(A)|hAPP(A,A,times_times(A,B),zero_zero(A))=zero_zero(A).
% 0.46/0.66 Following clause subsumed by 958 during input processing: 0 [] {-} -real_normed_algebra(A)|hAPP(A,A,times_times(A,zero_zero(A)),B)=zero_zero(A).
% 0.46/0.66 Following clause subsumed by 959 during input processing: 0 [] {-} -real_normed_algebra(A)|hAPP(A,A,times_times(A,hAPP(A,A,plus_plus(A,B),C)),D)=hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,B),D)),hAPP(A,A,times_times(A,C),D)).
% 0.46/0.66 Following clause subsumed by 961 during input processing: 0 [flip.2] {-} -real_normed_algebra(A)|hAPP(A,A,plus_plus(A,hAPP(A,A,times_times(A,B),C)),hAPP(A,A,times_times(A,B),D))=hAPP(A,A,times_times(A,B),hAPP(A,A,plus_plus(A,C),D)).
% 0.46/0.66 Following clause subsumed by 963 during input processing: 0 [flip.2] {-} -real_normed_algebra(A)|hAPP(A,A,minus_minus(A,hAPP(A,A,times_times(A,B),C)),hAPP(A,A,times_times(A,B),D))=hAPP(A,A,times_times(A,B),hAPP(A,A,minus_minus(A,C),D)).
% 0.46/0.66 Following clause subsumed by 964 during input processing: 0 [] {-} -real_normed_algebra(A)|hAPP(A,A,times_times(A,hAPP(A,A,minus_minus(A,B),C)),D)=hAPP(A,A,minus_minus(A,hAPP(A,A,times_times(A,B),D)),hAPP(A,A,times_times(A,C),D)).
% 0.46/0.66 Following clause subsumed by 974 during input processing: 0 [] {-} -semiring_div(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),C))|hAPP(A,A,div_mod(A,C),B)=zero_zero(A).
% 0.46/0.66 Following clause subsumed by 990 during input processing: 0 [] {-} -semiring_div(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),hAPP(A,A,div_mod(A,D),C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),D)).
% 0.46/0.66 Following clause subsumed by 991 during input processing: 0 [] {-} -semiring_div(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),hAPP(A,A,div_mod(A,D),C)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),D)).
% 0.46/0.66 Following clause subsumed by 996 during input processing: 0 [] {-} -semiring_div(A)|hAPP(A,A,div_mod(A,hAPP(A,A,plus_plus(A,B),hAPP(A,A,div_mod(A,C),D))),D)=hAPP(A,A,div_mod(A,hAPP(A,A,plus_plus(A,B),C)),D).
% 0.46/0.66 Following clause subsumed by 998 during input processing: 0 [] {-} -semiring_div(A)|hAPP(A,A,div_mod(A,hAPP(A,A,plus_plus(A,hAPP(A,A,div_mod(A,B),C)),D)),C)=hAPP(A,A,div_mod(A,hAPP(A,A,plus_plus(A,B),D)),C).
% 0.46/0.66 Following clause subsumed by 1005 during input processing: 0 [] {-} -semiring_div(A)|hAPP(A,A,div_mod(A,hAPP(A,A,times_times(A,hAPP(A,A,div_mod(A,B),C)),D)),C)=hAPP(A,A,div_mod(A,hAPP(A,A,times_times(A,B),D)),C).
% 0.46/0.66 Following clause subsumed by 974 during input processing: 0 [] {-} -semiring_div(A)| -number(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),number_number_of(A,B)),number_number_of(A,C)))|hAPP(A,A,div_mod(A,number_number_of(A,C)),number_number_of(A,B))=zero_zero(A).
% 0.46/0.66 Following clause subsumed by 975 during input processing: 0 [] {-} -semiring_div(A)| -number(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),number_number_of(A,B)),number_number_of(A,C)))|hAPP(A,A,div_mod(A,number_number_of(A,C)),number_number_of(A,B))!=zero_zero(A).
% 0.46/0.66 Following clause subsumed by 984 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),A))|hBOOL(hAPP(int,bool,zcong(B,C),A))|hAPP(int,int,div_mod(int,B),A)!=hAPP(int,int,div_mod(int,C),A).
% 0.54/0.73 Following clause subsumed by 1023 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),A))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,div_mod(int,B),A))).
% 0.54/0.73 Following clause subsumed by 977 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),A))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,div_mod(int,B),A)),A)).
% 0.54/0.73 Following clause subsumed by 1025 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),zero_zero(int)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,div_mod(int,B),A)),zero_zero(int))).
% 0.54/0.73 Following clause subsumed by 976 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),zero_zero(int)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),hAPP(int,int,div_mod(int,B),A))).
% 0.54/0.73 Following clause subsumed by 1083 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|hAPP(nat,nat,div_mod(nat,A),B)=A.
% 0.54/0.73 Following clause subsumed by 1086 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,zcong(A,zero_zero(int)),B))|standardRes(B,A)!=zero_zero(int).
% 0.54/0.73 Following clause subsumed by 1087 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,zcong(A,zero_zero(int)),B))|standardRes(B,A)=zero_zero(int).
% 0.54/0.73 44 back subsumes 41.
% 0.54/0.73 98 back subsumes 96.
% 0.54/0.73 99 back subsumes 95.
% 0.54/0.73 Following clause subsumed by 156 during input processing: 0 [copy,155,flip.1] {-} bit0(A)!=bit1(B).
% 0.54/0.73 Following clause subsumed by 155 during input processing: 0 [copy,156,flip.1] {-} bit1(A)!=bit0(B).
% 0.54/0.73 368 back subsumes 276.
% 0.54/0.73 443 back subsumes 406.
% 0.54/0.73 646 back subsumes 645.
% 0.54/0.73 646 back subsumes 644.
% 0.54/0.73 653 back subsumes 650.
% 0.54/0.73 653 back subsumes 647.
% 0.54/0.73 653 back subsumes 646.
% 0.54/0.73 654 back subsumes 652.
% 0.54/0.73 654 back subsumes 648.
% 0.54/0.73 655 back subsumes 651.
% 0.54/0.73 655 back subsumes 649.
% 0.54/0.73 706 back subsumes 705.
% 0.54/0.73 770 back subsumes 211.
% 0.54/0.73 874 back subsumes 870.
% 0.54/0.73 892 back subsumes 816.
% 0.54/0.73 Following clause subsumed by 252 during input processing: 0 [copy,1124,flip.1] {-} hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),A)),A)!=zero_zero(int).
% 0.54/0.73 Following clause subsumed by 1106 during input processing: 0 [copy,1271,flip.1] {-} hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,B),number_number_of(nat,bit0(bit1(pls)))))!=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)).
% 0.54/0.73
% 0.54/0.73 ------------> process sos:
% 0.54/0.73 Following clause subsumed by 1412 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),pls)).
% 0.54/0.73 Following clause subsumed by 1453 during input processing: 0 [demod,1518,1437] {-} hAPP(int,int,plus_plus(int,pls),A)=number_number_of(int,A).
% 0.54/0.73 Following clause subsumed by 1412 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min),min)).
% 0.54/0.73 Following clause subsumed by 1538 during input processing: 0 [demod,1518] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),min),pls)).
% 0.54/0.73 Following clause subsumed by 1412 during input processing: 0 [demod,1518,1518] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),pls)).
% 0.54/0.73 Following clause subsumed by 1637 during input processing: 0 [] {-} A=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),A)).
% 0.54/0.73 Following clause subsumed by 1637 during input processing: 0 [] {-} A=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),A)).
% 0.54/0.73 Following clause subsumed by 1662 during input processing: 0 [demod,1542,1542] {-} A=number_number_of(nat,pls)|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),number_number_of(nat,pls)),A)).
% 0.71/0.91 Following clause subsumed by 1623 during input processing: 0 [demod,1542] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),number_number_of(nat,pls)),A)).
% 0.71/0.91 Following clause subsumed by 1714 during input processing: 0 [demod,1425,1425] {-} A=number_number_of(nat,bit1(pls))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),number_number_of(nat,bit1(pls))),A)).
% 0.71/0.91 Following clause subsumed by 1778 during input processing: 0 [flip.2] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|hAPP(nat,nat,div_mod(nat,hAPP(nat,nat,minus_minus(nat,A),B)),B)=hAPP(nat,nat,div_mod(nat,A),B).
% 0.71/0.91 Following clause subsumed by 1720 during input processing: 0 [demod,1782] {-} hBOOL(hAPP(int,bool,zcong(A,hAPP(int,int,div_mod(int,A),B)),B)).
% 0.71/0.91 1412 back subsumes 1260.
% 0.71/0.91 1412 back subsumes 1259.
% 0.71/0.91 1412 back subsumes 1258.
% 0.74/0.91 1412 back subsumes 1156.
% 0.74/0.91 1412 back subsumes 1138.
% 0.74/0.91 1413 back subsumes 384.
% 0.74/0.91 Following clause subsumed by 1951 during input processing: 0 [copy,1427,flip.1] {-} number_number_of(nat,bit1(pls))=number_number_of(nat,bit1(pls)).
% 0.74/0.91 Following clause subsumed by 1434 during input processing: 0 [copy,1434,flip.1] {-} hAPP(int,int,times_times(int,A),B)=hAPP(int,int,times_times(int,B),A).
% 0.74/0.91 Following clause subsumed by 1440 during input processing: 0 [copy,1440,flip.1] {-} hAPP(int,int,plus_plus(int,A),hAPP(int,int,plus_plus(int,B),C))=hAPP(int,int,plus_plus(int,B),hAPP(int,int,plus_plus(int,A),C)).
% 0.74/0.91 Following clause subsumed by 1441 during input processing: 0 [copy,1441,flip.1] {-} hAPP(int,int,plus_plus(int,A),B)=hAPP(int,int,plus_plus(int,B),A).
% 0.74/0.91 Following clause subsumed by 1951 during input processing: 0 [copy,1520,flip.1,demod,1567,1567] {-} hAPP(int,int,minus_minus(int,A),pls)=hAPP(int,int,minus_minus(int,A),pls).
% 0.74/0.91 Following clause subsumed by 1951 during input processing: 0 [copy,1544,flip.1] {-} number_number_of(nat,pls)=number_number_of(nat,pls).
% 0.74/0.91 Following clause subsumed by 1951 during input processing: 0 [copy,1589,flip.1] {-} hAPP(int,int,minus_minus(int,min),hAPP(int,int,plus_plus(int,A),A))=hAPP(int,int,minus_minus(int,min),hAPP(int,int,plus_plus(int,A),A)).
% 0.74/0.91 Following clause subsumed by 1610 during input processing: 0 [copy,1610,flip.1] {-} hAPP(real,real,times_times(real,A),B)=hAPP(real,real,times_times(real,B),A).
% 0.74/0.91 Following clause subsumed by 1625 during input processing: 0 [copy,1625,flip.1] {-} hAPP(nat,nat,minus_minus(nat,hAPP(nat,nat,minus_minus(nat,A),B)),C)=hAPP(nat,nat,minus_minus(nat,hAPP(nat,nat,minus_minus(nat,A),C)),B).
% 0.74/0.91 Following clause subsumed by 1638 during input processing: 0 [copy,1638,flip.1] {-} hAPP(nat,nat,plus_plus(nat,A),B)=hAPP(nat,nat,plus_plus(nat,B),A).
% 0.74/0.91 Following clause subsumed by 1639 during input processing: 0 [copy,1639,flip.1] {-} hAPP(nat,nat,plus_plus(nat,A),hAPP(nat,nat,plus_plus(nat,B),C))=hAPP(nat,nat,plus_plus(nat,B),hAPP(nat,nat,plus_plus(nat,A),C)).
% 0.74/0.91 1651 back subsumes 1227.
% 0.74/0.91 Following clause subsumed by 1656 during input processing: 0 [copy,1656,flip.1] {-} hAPP(nat,nat,times_times(nat,A),B)=hAPP(nat,nat,times_times(nat,B),A).
% 0.74/0.91 1712 back subsumes 1710.
% 0.74/0.91 Following clause subsumed by 1951 during input processing: 0 [copy,1727,flip.1] {-} hAPP(int,int,div_mod(int,hAPP(int,int,times_times(int,A),B)),C)=hAPP(int,int,div_mod(int,hAPP(int,int,times_times(int,A),B)),C).
% 0.74/0.91 Following clause subsumed by 1951 during input processing: 0 [copy,1951,flip.1] {-} A=A.
% 0.74/0.91 1951 back subsumes 1727.
% 0.74/0.91 1951 back subsumes 1589.
% 0.74/0.91 1951 back subsumes 1544.
% 0.74/0.91 1951 back subsumes 1427.
% 0.74/0.91 1951 back subsumes 1225.
% 0.74/0.91 1951 back subsumes 1224.
% 0.74/0.91 1951 back subsumes 1223.
% 0.74/0.91 1951 back subsumes 1219.
% 0.74/0.91 1951 back subsumes 1161.
% 0.74/0.91 1951 back subsumes 1160.
% 0.74/0.91 Following clause subsumed by 2143 during input processing: 0 [copy,1954,flip.1] {-} hAPP(int,int,times_times(int,A),hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))=hAPP(nat,int,power_power(int,A),number_number_of(nat,bit1(bit1(pls)))).
% 0.74/0.91 Following clause subsumed by 1415 during input processing: 0 [copy,1955,flip.1] {-} hAPP(nat,int,power_power(int,hAPP(nat,int,power_power(int,A),B)),C)=hAPP(nat,int,power_power(int,A),hAPP(nat,nat,times_times(nat,B),C)).
% 0.74/0.93 Following clause subsumed by 1416 during input processing: 0 [copy,1956,flip.1] {-} hAPP(nat,int,power_power(int,A),hAPP(nat,nat,plus_plus(nat,B),C))=hAPP(int,int,times_times(int,hAPP(nat,int,power_power(int,A),B)),hAPP(nat,int,power_power(int,A),C)).
% 0.74/0.93 Following clause subsumed by 2142 during input processing: 0 [copy,1957,flip.1] {-} hAPP(nat,nat,times_times(nat,number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))),A)=hAPP(nat,nat,plus_plus(nat,A),A).
% 0.74/0.93 Following clause subsumed by 2472 during input processing: 0 [copy,2136,flip.1] {-} hAPP(int,int,plus_plus(int,pls),A)=hAPP(int,int,minus_minus(int,A),pls).
% 0.74/0.93 Following clause subsumed by 1957 during input processing: 0 [copy,2142,flip.1] {-} hAPP(nat,nat,plus_plus(nat,A),A)=hAPP(nat,nat,times_times(nat,number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))),A).
% 0.74/0.93 Following clause subsumed by 1954 during input processing: 0 [copy,2143,flip.1] {-} hAPP(nat,int,power_power(int,A),number_number_of(nat,bit1(bit1(pls))))=hAPP(int,int,times_times(int,A),hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))).
% 0.74/0.93 Following clause subsumed by 2209 during input processing: 0 [copy,2208,flip.1] {-} bit1(A)!=hAPP(int,int,plus_plus(int,B),B).
% 0.74/0.93 Following clause subsumed by 2208 during input processing: 0 [copy,2209,flip.1] {-} hAPP(int,int,plus_plus(int,A),A)!=bit1(B).
% 0.74/0.93 Following clause subsumed by 2241 during input processing: 0 [copy,2234,flip.1] {-} hAPP(int,int,times_times(int,bit1(pls)),A)=hAPP(int,int,minus_minus(int,A),pls).
% 0.74/0.93 Following clause subsumed by 2471 during input processing: 0 [copy,2235,flip.1] {-} hAPP(int,int,times_times(int,hAPP(int,int,minus_minus(int,A),pls)),hAPP(int,int,minus_minus(int,B),pls))=hAPP(int,int,minus_minus(int,hAPP(int,int,times_times(int,A),B)),pls).
% 0.74/0.93 Following clause subsumed by 1465 during input processing: 0 [copy,2236,flip.1] {-} hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,A),B)),C)=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,A),C)),hAPP(int,int,times_times(int,B),C)).
% 0.74/0.93 Following clause subsumed by 2470 during input processing: 0 [copy,2237,flip.1] {-} hAPP(int,int,plus_plus(int,hAPP(int,int,minus_minus(int,A),pls)),hAPP(int,int,minus_minus(int,B),pls))=hAPP(int,int,minus_minus(int,hAPP(int,int,plus_plus(int,A),B)),pls).
% 0.74/0.93 Following clause subsumed by 1476 during input processing: 0 [copy,2238,flip.1] {-} hAPP(int,int,plus_plus(int,A),hAPP(int,int,plus_plus(int,A),bit1(B)))=hAPP(int,int,plus_plus(int,bit1(A)),hAPP(int,int,plus_plus(int,B),B)).
% 0.74/0.93 Following clause subsumed by 2240 during input processing: 0 [copy,2239,flip.1] {-} bit1(A)=hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(int,int,plus_plus(int,A),A)).
% 0.74/0.93 Following clause subsumed by 2239 during input processing: 0 [copy,2240,flip.1] {-} hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(int,int,plus_plus(int,A),A))=bit1(A).
% 0.74/0.93 Following clause subsumed by 2234 during input processing: 0 [copy,2241,flip.1] {-} hAPP(int,int,minus_minus(int,A),pls)=hAPP(int,int,times_times(int,bit1(pls)),A).
% 0.74/0.93 Following clause subsumed by 1482 during input processing: 0 [copy,2288,flip.1] {-} hAPP(int,int,times_times(int,bit1(A)),B)=hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,A),hAPP(int,int,plus_plus(int,B),B))),B).
% 0.74/0.93 Following clause subsumed by 1496 during input processing: 0 [copy,2290,flip.1] {-} hAPP(real,real,times_times(real,number_number_of(real,hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(int,int,plus_plus(int,bit1(pls)),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))),hAPP(nat,real,power_power(real,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))=hAPP(nat,real,power_power(real,hAPP(real,real,times_times(real,number_number_of(real,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))),A)),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))).
% 0.74/0.93 Following clause subsumed by 2237 during input processing: 0 [copy,2470,flip.1] {-} hAPP(int,int,minus_minus(int,hAPP(int,int,plus_plus(int,A),B)),pls)=hAPP(int,int,plus_plus(int,hAPP(int,int,minus_minus(int,A),pls)),hAPP(int,int,minus_minus(int,B),pls)).
% 0.74/0.93 Following clause subsumed by 2235 during input processing: 0 [copy,2471,flip.1] {-} hAPP(int,int,minus_minus(int,hAPP(int,int,times_times(int,A),B)),pls)=hAPP(int,int,times_times(int,hAPP(int,int,minus_minus(int,A),pls)),hAPP(int,int,minus_minus(int,B),pls)).
% 0.74/0.93 Following clause subsumed by 2136 during input processing: 0 [copy,2472,flip.1] {-} hAPP(int,int,minus_minus(int,A),pls)=hAPP(int,int,plus_plus(int,pls),A).
% 0.74/0.93 Following clause subsumed by 1574 during input processing: 0 [copy,2481,flip.1] {-} hAPP(int,int,times_times(int,hAPP(int,int,minus_minus(int,A),B)),C)=hAPP(int,int,minus_minus(int,hAPP(int,int,times_times(int,A),C)),hAPP(int,int,times_times(int,B),C)).
% 0.74/0.93 Following clause subsumed by 1584 during input processing: 0 [copy,2482,flip.1] {-} hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,minus_minus(int,A),hAPP(int,int,times_times(int,B),C))),D)),hAPP(int,int,times_times(int,hAPP(int,int,minus_minus(int,E),hAPP(int,int,times_times(int,B),F))),G))=hAPP(int,int,minus_minus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,A),D)),hAPP(int,int,times_times(int,E),G))),hAPP(int,int,times_times(int,B),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,C),D)),hAPP(int,int,times_times(int,F),G)))).
% 0.74/0.93 Following clause subsumed by 1597 during input processing: 0 [copy,2483,flip.1] {-} hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,A),B)),hAPP(int,int,minus_minus(int,A),B))=hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(nat,int,power_power(int,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))).
% 0.74/0.93 Following clause subsumed by 1618 during input processing: 0 [copy,2486,flip.1] {-} hAPP(nat,nat,minus_minus(nat,hAPP(nat,nat,power_power(nat,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(nat,nat,power_power(nat,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))=hAPP(nat,nat,times_times(nat,hAPP(nat,nat,plus_plus(nat,A),B)),hAPP(nat,nat,minus_minus(nat,A),B)).
% 0.74/0.93 Following clause subsumed by 1619 during input processing: 0 [copy,2487,flip.1] {-} hAPP(real,real,times_times(real,hAPP(real,real,plus_plus(real,A),B)),C)=hAPP(real,real,plus_plus(real,hAPP(real,real,times_times(real,A),C)),hAPP(real,real,times_times(real,B),C)).
% 0.74/0.93 Following clause subsumed by 1635 during input processing: 0 [copy,2488,flip.1] {-} hAPP(nat,nat,minus_minus(nat,A),A)=number_number_of(nat,pls).
% 0.74/0.93 Following clause subsumed by 1646 during input processing: 0 [copy,2489,flip.1] {-} hAPP(nat,nat,minus_minus(nat,hAPP(nat,nat,minus_minus(nat,A),B)),C)=hAPP(nat,nat,minus_minus(nat,A),hAPP(nat,nat,plus_plus(nat,B),C)).
% 0.74/0.93 Following clause subsumed by 1657 during input processing: 0 [copy,2490,flip.1] {-} hAPP(nat,nat,times_times(nat,hAPP(nat,nat,minus_minus(nat,A),B)),C)=hAPP(nat,nat,minus_minus(nat,hAPP(nat,nat,times_times(nat,A),C)),hAPP(nat,nat,times_times(nat,B),C)).
% 0.74/0.93 Following clause subsumed by 1681 during input processing: 0 [copy,2491,flip.1] {-} hAPP(nat,nat,times_times(nat,hAPP(nat,nat,plus_plus(nat,A),B)),C)=hAPP(nat,nat,plus_plus(nat,hAPP(nat,nat,times_times(nat,A),C)),hAPP(nat,nat,times_times(nat,B),C)).
% 0.74/0.93 Following clause subsumed by 2500 during input processing: 0 [copy,2493,flip.1] {-} hAPP(int,int,div_mod(int,hAPP(int,int,plus_plus(int,A),A)),hAPP(int,int,plus_plus(int,B),B))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,div_mod(int,A),B)).
% 0.74/0.93 Following clause subsumed by 1783 during input processing: 0 [copy,2494,flip.1] {-} hAPP(nat,nat,times_times(nat,hAPP(nat,nat,div_mod(nat,A),B)),C)=hAPP(nat,nat,div_mod(nat,hAPP(nat,nat,times_times(nat,A),C)),hAPP(nat,nat,times_times(nat,B),C)).
% 0.74/0.93 Following clause subsumed by 1948 during input processing: 0 [copy,2495,flip.1] {-} hAPP(A,B,combb(C,B,A,D,E),F)=hAPP(C,B,D,hAPP(A,C,E,F)).
% 0.74/0.93 Following clause subsumed by 1949 during input processing: 0 [copy,2496,flip.1] {-} hAPP(A,B,combc(A,C,B,D,E),F)=hAPP(C,B,hAPP(A,fun(C,B),D,F),E).
% 0.74/0.93 Following clause subsumed by 1950 during input processing: 0 [copy,2497,flip.1] {-} hAPP(A,B,combs(A,C,B,D,E),F)=hAPP(C,B,hAPP(A,fun(C,B),D,F),hAPP(A,C,E,F)).
% 0.74/0.93 Following clause subsumed by 2493 during input processing: 0 [copy,2500,flip.1] {-} hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,div_mod(int,A),B))=hAPP(int,int,div_mod(int,hAPP(int,int,plus_plus(int,A),A)),hAPP(int,int,plus_plus(int,B),B)).
% 0.74/0.93 Following clause subsumed by 2137 during input processing: 0 [copy,2507,flip.1] {-} hAPP(int,int,plus_plus(int,A),hAPP(int,int,plus_plus(int,B),hAPP(int,int,plus_plus(int,A),B)))=hAPP(int,int,plus_plus(int,A),hAPP(int,int,plus_plus(int,A),hAPP(int,int,plus_plus(int,B),B))).
% 0.74/0.93 Following clause subsumed by 2138 during input processing: 0 [copy,2508,flip.1] {-} hAPP(int,int,times_times(int,A),hAPP(int,int,plus_plus(int,B),B))=hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,A),A)),B).
% 0.74/0.93 Following clause subsumed by 2289 during input processing: 0 [copy,2509,flip.1] {-} hAPP(real,real,plus_plus(real,hAPP(real,real,plus_plus(real,hAPP(nat,real,power_power(real,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(nat,real,power_power(real,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))),hAPP(real,real,times_times(real,number_number_of(real,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))),hAPP(real,real,times_times(real,A),B)))=hAPP(nat,real,power_power(real,hAPP(real,real,plus_plus(real,A),B)),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))).
% 0.74/0.93 Following clause subsumed by 2484 during input processing: 0 [copy,2511,flip.1] {-} hAPP(int,int,plus_plus(int,hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,times_times(int,A),B)))),hAPP(nat,int,power_power(int,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))=hAPP(nat,int,power_power(int,hAPP(int,int,minus_minus(int,A),B)),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))).
% 0.74/0.93 Following clause subsumed by 2485 during input processing: 0 [copy,2512,flip.1] {-} hAPP(int,int,minus_minus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,bit1(bit1(pls))))),hAPP(int,int,times_times(int,bit1(bit1(pls))),hAPP(int,int,times_times(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),B)))),hAPP(int,int,times_times(int,bit1(bit1(pls))),hAPP(int,int,times_times(int,A),hAPP(nat,int,power_power(int,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))))),hAPP(nat,int,power_power(int,B),number_number_of(nat,bit1(bit1(pls)))))=hAPP(nat,int,power_power(int,hAPP(int,int,minus_minus(int,A),B)),number_number_of(nat,bit1(bit1(pls)))).
% 0.74/0.93 Following clause subsumed by 2498 during input processing: 0 [copy,2513,flip.1] {-} hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,A),B)),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))=hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))),hAPP(int,int,times_times(int,A),B))),hAPP(nat,int,power_power(int,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))).
% 0.77/0.93 Following clause subsumed by 2499 during input processing: 0 [copy,2514,flip.1] {-} hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,A),B)),number_number_of(nat,bit1(bit1(pls))))=hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,bit1(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit1(bit1(pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),B)),hAPP(int,int,times_times(int,A),hAPP(nat,int,power_power(int,B),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls)))))))),hAPP(nat,int,power_power(int,B),number_number_of(nat,bit1(bit1(pls)))))).
% 0.77/0.93
% 0.77/0.93 ======= end of input processing =======
% 0.77/0.94
% 0.77/0.94 SEGMENTATION FAULT!! This is probably caused by a
% 0.77/0.94 bug in Otter. Please send copy of the input file to
% 0.77/0.94 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.77/0.94 using, and send any other info that might be useful.
% 0.77/0.94
% 0.77/0.94
% 0.77/0.94 SEGMENTATION FAULT!! This is probably caused by a
% 0.77/0.94 bug in Otter. Please send copy of the input file to
% 0.77/0.94 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.77/0.94 using, and send any other info that might be useful.
% 0.77/0.94
% 0.77/0.94
% 0.77/0.94 The job finished Wed Jul 6 09:24:39 2022
%------------------------------------------------------------------------------