%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NUM925+7 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n013.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:15 EDT 2022
% Result : Unknown 1.07s 1.28s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM925+7 : TPTP v8.1.0. Released v5.3.0.
% 0.12/0.13 % Command : sos-script %s
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jul 7 04:48:59 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.55 ----- Otter 3.2, August 2001 -----
% 0.19/0.55 The process was started by sandbox on n013.cluster.edu,
% 0.19/0.55 Thu Jul 7 04:49:00 2022
% 0.19/0.55 The command was "./sos". The process ID is 21272.
% 0.19/0.55
% 0.19/0.55 set(prolog_style_variables).
% 0.19/0.55 set(auto).
% 0.19/0.55 dependent: set(auto1).
% 0.19/0.55 dependent: set(process_input).
% 0.19/0.55 dependent: clear(print_kept).
% 0.19/0.55 dependent: clear(print_new_demod).
% 0.19/0.55 dependent: clear(print_back_demod).
% 0.19/0.55 dependent: clear(print_back_sub).
% 0.19/0.55 dependent: set(control_memory).
% 0.19/0.55 dependent: assign(max_mem, 12000).
% 0.19/0.55 dependent: assign(pick_given_ratio, 4).
% 0.19/0.55 dependent: assign(stats_level, 1).
% 0.19/0.55 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.55 dependent: assign(sos_limit, 5000).
% 0.19/0.55 dependent: assign(max_weight, 60).
% 0.19/0.55 clear(print_given).
% 0.19/0.55
% 0.19/0.55 formula_list(usable).
% 0.19/0.55
% 0.19/0.55 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=7.
% 0.19/0.55
% 0.19/0.55 This ia a non-Horn set with equality. The strategy will be
% 0.19/0.55 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.19/0.55 unit deletion, with positive clauses in sos and nonpositive
% 0.19/0.55 clauses in usable.
% 0.19/0.55
% 0.19/0.55 dependent: set(knuth_bendix).
% 0.19/0.55 dependent: set(para_from).
% 0.19/0.55 dependent: set(para_into).
% 0.19/0.55 dependent: clear(para_from_right).
% 0.19/0.55 dependent: clear(para_into_right).
% 0.19/0.55 dependent: set(para_from_vars).
% 0.19/0.55 dependent: set(eq_units_both_ways).
% 0.19/0.55 dependent: set(dynamic_demod_all).
% 0.19/0.55 dependent: set(dynamic_demod).
% 0.19/0.55 dependent: set(order_eq).
% 0.19/0.55 dependent: set(back_demod).
% 0.19/0.55 dependent: set(lrpo).
% 0.19/0.55 dependent: set(hyper_res).
% 0.19/0.55 dependent: set(unit_deletion).
% 0.19/0.55 dependent: set(factor).
% 0.19/0.55
% 0.19/0.55 ------------> process usable:
% 0.19/0.55 Following clause subsumed by 73 during input processing: 0 [flip.2] {-} -number_ring(A)|one_one(A)=number_number_of(A,bit1(pls)).
% 0.19/0.55 Following clause subsumed by 80 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.19/0.55 Following clause subsumed by 81 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.19/0.55 Following clause subsumed by 83 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.19/0.55 Following clause subsumed by 84 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.19/0.55 Following clause subsumed by 106 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.19/0.55 Following clause subsumed by 107 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.19/0.55 Following clause subsumed by 129 during input processing: 0 [flip.1] {-} bit1(A)!=pls.
% 0.19/0.55 Following clause subsumed by 132 during input processing: 0 [flip.1,flip.2] {-} bit0(A)!=pls|ti(int,A)=pls.
% 0.19/0.55 Following clause subsumed by 133 during input processing: 0 [flip.1,flip.2] {-} bit0(A)=pls|ti(int,A)!=pls.
% 0.19/0.55 Following clause subsumed by 138 during input processing: 0 [] {-} -number_ring(A)|zero_zero(A)=number_number_of(A,pls).
% 0.19/0.55 Following clause subsumed by 149 during input processing: 0 [] {-} -number_ring(A)|number_number_of(A,plus_plus(int,B,C))=plus_plus(A,number_number_of(A,B),number_number_of(A,C)).
% 0.19/0.55 Following clause subsumed by 179 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),A)).
% 0.19/0.55 Following clause subsumed by 183 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|B!=A.
% 0.19/0.55 Following clause subsumed by 182 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|A!=B.
% 0.19/0.55 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),zero_zero(nat))).
% 0.19/0.55 Following clause subsumed by 190 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),plus_plus(nat,A,B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A)).
% 0.19/0.55 Following clause subsumed by 191 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),plus_plus(nat,A,B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),B)).
% 0.19/0.55 Following clause subsumed by 183 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.19/0.55 Following clause subsumed by 177 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),zero_zero(nat))).
% 0.19/0.55 Following clause subsumed by 198 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.19/0.55 Following clause subsumed by 200 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.19/0.55 Following clause subsumed by 199 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.19/0.55 Following clause subsumed by 198 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.19/0.55 Following clause subsumed by 200 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.19/0.55 Following clause subsumed by 199 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.19/0.55 Following clause subsumed by 202 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(nat,int,semiring_1_of_nat(int),A)),hAPP(nat,int,semiring_1_of_nat(int),B)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B)).
% 0.19/0.55 Following clause subsumed by 203 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(nat,int,semiring_1_of_nat(int),A)),hAPP(nat,int,semiring_1_of_nat(int),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B)).
% 0.19/0.55 Following clause subsumed by 98 during input processing: 0 [] {-} hAPP(nat,int,semiring_1_of_nat(int),A)!=hAPP(nat,int,semiring_1_of_nat(int),B)|A=B.
% 0.19/0.55 Following clause subsumed by 99 during input processing: 0 [] {-} hAPP(nat,int,semiring_1_of_nat(int),A)=hAPP(nat,int,semiring_1_of_nat(int),B)|A!=B.
% 0.19/0.55 Following clause subsumed by 222 during input processing: 0 [] {-} -zero_neq_one(A)|zero_zero(A)!=one_one(A).
% 0.19/0.55 Following clause subsumed by 226 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),hAPP(nat,A,semiring_1_of_nat(A),B)),hAPP(nat,A,semiring_1_of_nat(A),C))).
% 0.19/0.55 Following clause subsumed by 225 during input processing: 0 [] {-} -linordered_semidom(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),hAPP(nat,A,semiring_1_of_nat(A),B)),hAPP(nat,A,semiring_1_of_nat(A),C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.19/0.56 Following clause subsumed by 237 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.19/0.56 Following clause subsumed by 238 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.19/0.56 Following clause subsumed by 262 during input processing: 0 [] {-} -cancel_semigroup_add(A)|plus_plus(A,B,C)!=plus_plus(A,D,C)|ti(A,B)=ti(A,D).
% 0.19/0.56 Following clause subsumed by 264 during input processing: 0 [] {-} -cancel_semigroup_add(A)|plus_plus(A,B,C)!=plus_plus(A,B,D)|ti(A,C)=ti(A,D).
% 0.19/0.56 Following clause subsumed by 270 during input processing: 0 [flip.2] {-} -comm_semiring_1(A)|plus_plus(A,plus_plus(A,B,C),D)=plus_plus(A,B,plus_plus(A,C,D)).
% 0.19/0.56 Following clause subsumed by 285 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),plus_plus(A,B,C)),plus_plus(A,B,D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),C),D)).
% 0.19/0.56 Following clause subsumed by 286 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),plus_plus(A,B,C)),plus_plus(A,D,C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),D)).
% 0.19/0.56 Following clause subsumed by 308 during input processing: 0 [] {-} -comm_semiring_1(A)|times_times(A,times_times(A,B,C),D)=times_times(A,B,times_times(A,C,D)).
% 0.19/0.56 Following clause subsumed by 308 during input processing: 0 [] {-} -comm_semiring_1(A)|times_times(A,times_times(A,B,C),times_times(A,D,E))=times_times(A,B,times_times(A,C,times_times(A,D,E))).
% 0.19/0.56 Following clause subsumed by 306 during input processing: 0 [] {-} -comm_semiring_1(A)|times_times(A,times_times(A,B,C),times_times(A,D,E))=times_times(A,D,times_times(A,times_times(A,B,C),E)).
% 0.19/0.56 Following clause subsumed by 322 during input processing: 0 [flip.2] {-} -number_ring(A)|number_number_of(A,times_times(int,B,C))=times_times(A,number_number_of(A,B),number_number_of(A,C)).
% 0.19/0.56 Following clause subsumed by 338 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)),times_times(A,B,C))).
% 0.19/0.56 Following clause subsumed by 336 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),times_times(A,B,C)),zero_zero(A))).
% 0.19/0.56 Following clause subsumed by 336 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),times_times(A,C,B)),zero_zero(A))).
% 0.19/0.56 Following clause subsumed by 335 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),times_times(A,B,C)),zero_zero(A))).
% 0.19/0.56 Following clause subsumed by 325 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_eq(int),zero_zero(int)),B))|nat_1(A)!=nat_1(B)|ti(int,A)=ti(int,B).
% 0.19/0.56 Following clause subsumed by 326 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_eq(int),zero_zero(int)),B))|nat_1(A)=nat_1(B)|ti(int,A)!=ti(int,B).
% 0.19/0.56 Following clause subsumed by 402 during input processing: 0 [] {-} nat_1(A)=zero_zero(nat)| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),zero_zero(int))).
% 0.19/0.56 Following clause subsumed by 405 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),A))|hAPP(nat,int,semiring_1_of_nat(int),nat_1(A))=ti(int,A).
% 0.19/0.56 Following clause subsumed by 426 during input processing: 0 [] {-} -no_zero_divisors(A)|times_times(A,B,C)!=zero_zero(A)|ti(A,B)=zero_zero(A)|ti(A,C)=zero_zero(A).
% 0.19/0.56 Following clause subsumed by 437 during input processing: 0 [] {-} -comm_semiring_1(A)|times_times(A,plus_plus(A,B,C),D)=plus_plus(A,times_times(A,B,D),times_times(A,C,D)).
% 0.19/0.56 Following clause subsumed by 433 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)=ti(A,C)|ti(A,D)=ti(A,E)|plus_plus(A,times_times(A,B,D),times_times(A,C,E))!=plus_plus(A,times_times(A,B,E),times_times(A,C,D)).
% 0.19/0.56 Following clause subsumed by 434 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|plus_plus(A,times_times(A,B,D),times_times(A,C,E))=plus_plus(A,times_times(A,B,E),times_times(A,C,D)).
% 0.19/0.56 Following clause subsumed by 435 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|plus_plus(A,times_times(A,D,B),times_times(A,E,C))=plus_plus(A,times_times(A,D,C),times_times(A,E,B)).
% 0.19/0.56 Following clause subsumed by 445 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),plus_plus(A,B,C)),plus_plus(A,B,D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),C),D)).
% 0.19/0.56 Following clause subsumed by 446 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),plus_plus(A,B,C)),plus_plus(A,D,C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),B),D)).
% 0.19/0.56 Following clause subsumed by 457 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.19/0.56 Following clause subsumed by 458 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.19/0.56 Following clause subsumed by 459 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.19/0.56 Following clause subsumed by 460 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.19/0.56 Following clause subsumed by 477 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.19/0.56 Following clause subsumed by 490 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_eq(int),zero_zero(int)),B))|nat_1(plus_plus(int,A,B))=plus_plus(nat,nat_1(A),nat_1(B)).
% 0.19/0.56 Following clause subsumed by 495 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),A))|nat_1(hAPP(nat,int,power_power(int,A),B))=hAPP(nat,nat,power_power(nat,nat_1(A)),B).
% 0.19/0.56 Following clause subsumed by 517 during input processing: 0 [] {-} -linord581940658strict(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),times_times(A,B,C)),times_times(A,B,D)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),C),D)).
% 0.19/0.57 Following clause subsumed by 518 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),times_times(A,B,C)),times_times(A,B,D)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),D),C)).
% 0.19/0.57 Following clause subsumed by 522 during input processing: 0 [] {-} -linord20386208strict(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),zero_zero(A)),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),times_times(A,B,C)),zero_zero(A))).
% 0.19/0.57 Following clause subsumed by 512 during input processing: 0 [] {-} -linord581940658strict(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),D),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),times_times(A,C,D)),times_times(A,B,D))).
% 0.19/0.57 Following clause subsumed by 518 during input processing: 0 [] {-} -linord581940658strict(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),D),zero_zero(A)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less(A),times_times(A,D,C)),times_times(A,D,B))).
% 0.19/0.57 Following clause subsumed by 568 during input processing: 0 [] {-} -linordered_semidom(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),zero_zero(A)),hAPP(nat,A,semiring_1_of_nat(A),B))).
% 0.19/0.57 Following clause subsumed by 574 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.19/0.57 Following clause subsumed by 575 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.19/0.57 Following clause subsumed by 598 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),nat_1(A)),nat_1(B)))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.19/0.57 Following clause subsumed by 618 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,A,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.19/0.57 Following clause subsumed by 619 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,A,minus_minus(nat,B,C)))|B!=plus_plus(nat,C,D)|hBOOL(hAPP(nat,bool,A,D)).
% 0.19/0.57 Following clause subsumed by 636 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.19/0.57 Following clause subsumed by 637 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.19/0.57 Following clause subsumed by 638 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.19/0.57 Following clause subsumed by 639 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.19/0.57 Following clause subsumed by 650 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),plus_plus(int,A,one_one(int))),B)).
% 0.19/0.57 Following clause subsumed by 673 during input processing: 0 [] {-} -monoid_mult(A)| -number(A)|hAPP(nat,A,power_power(A,number_number_of(A,B)),number_number_of(nat,bit0(bit1(pls))))=times_times(A,number_number_of(A,B),number_number_of(A,B)).
% 0.19/0.57 Following clause subsumed by 613 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.19/0.57 Following clause subsumed by 700 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),times_times(nat,A,B)),times_times(nat,C,B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),C)).
% 0.19/0.57 Following clause subsumed by 701 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),times_times(nat,A,B)),times_times(nat,A,C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.19/0.57 Following clause subsumed by 699 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.19/0.57 Following clause subsumed by 699 during input processing: 0 [] {-} A!=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.19/0.57 Following clause subsumed by 730 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.19/0.57 Following clause subsumed by 731 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.19/0.57 Following clause subsumed by 730 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.19/0.57 Following clause subsumed by 699 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|A!=B.
% 0.19/0.57 Following clause subsumed by 730 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.19/0.57 Following clause subsumed by 182 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|A!=B.
% 0.19/0.57 Following clause subsumed by 731 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))|A=B.
% 0.19/0.57 Following clause subsumed by 734 during input processing: 0 [] {-} -hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less_eq(real),A),B))|hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less(real),A),B))|A=B.
% 0.19/0.57 Following clause subsumed by 732 during input processing: 0 [] {-} hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less_eq(real),A),B))| -hBOOL(hAPP(real,bool,hAPP(real,fun(real,bool),ord_less(real),A),B)).
% 0.19/0.57 Following clause subsumed by 736 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),plus_plus(nat,A,B)),C))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),C)).
% 0.19/0.57 Following clause subsumed by 737 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),plus_plus(nat,A,B)),C))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.19/0.57 Following clause subsumed by 747 during input processing: 0 [] {-} times_times(nat,A,B)!=one_one(nat)|A=one_one(nat).
% 0.19/0.57 Following clause subsumed by 748 during input processing: 0 [] {-} times_times(nat,A,B)!=one_one(nat)|B=one_one(nat).
% 0.19/0.57 Following clause subsumed by 749 during input processing: 0 [] {-} times_times(nat,A,B)=one_one(nat)|A!=one_one(nat)|B!=one_one(nat).
% 0.19/0.57 Following clause subsumed by 766 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),times_times(nat,A,B)),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.19/0.57 Following clause subsumed by 765 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),times_times(nat,A,B)),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.41/0.58 Following clause subsumed by 782 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|minus_minus(nat,A,B)=zero_zero(nat).
% 0.41/0.58 Following clause subsumed by 786 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(nat),minus_minus(nat,B,A)),minus_minus(nat,C,A)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.41/0.58 Following clause subsumed by 793 during input processing: 0 [flip.2] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|plus_plus(nat,C,minus_minus(nat,B,A))=minus_minus(nat,plus_plus(nat,C,B),A).
% 0.41/0.58 Following clause subsumed by 799 during input processing: 0 [flip.2] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B))|plus_plus(nat,minus_minus(nat,B,A),C)=minus_minus(nat,plus_plus(nat,B,C),A).
% 0.41/0.58 Following clause subsumed by 800 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),A)),hAPP(nat,int,semiring_1_of_nat(int),B)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.41/0.58 Following clause subsumed by 801 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(nat,int,semiring_1_of_nat(int),A)),hAPP(nat,int,semiring_1_of_nat(int),B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),A),B)).
% 0.41/0.58 Following clause subsumed by 812 during input processing: 0 [flip.3] {-} -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_eq(int),zero_zero(int)),B))|nat_1(times_times(int,A,B))=times_times(nat,nat_1(A),nat_1(B)).
% 0.41/0.58 Following clause subsumed by 715 during input processing: 0 [] {-} A!=zero_zero(nat)|times_times(nat,A,B)=zero_zero(nat).
% 0.41/0.58 Following clause subsumed by 252 during input processing: 0 [] {-} A!=zero_zero(nat)|hAPP(nat,nat,power_power(nat,B),A)=one_one(nat).
% 0.41/0.58 Following clause subsumed by 882 during input processing: 0 [] {-} bit0(A)!=min.
% 0.41/0.58 Following clause subsumed by 884 during input processing: 0 [] {-} pls!=min.
% 0.41/0.58 Following clause subsumed by 886 during input processing: 0 [] {-} bit1(A)!=min|ti(int,A)=min.
% 0.41/0.58 Following clause subsumed by 888 during input processing: 0 [] {-} bit1(A)=min|ti(int,A)!=min.
% 0.41/0.58 Following clause subsumed by 899 during input processing: 0 [] {-} times_times(int,A,B)!=one_one(int)|ti(int,A)=one_one(int)|ti(int,A)=number_number_of(int,min).
% 0.41/0.58 Following clause subsumed by 846 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.41/0.58 Following clause subsumed by 914 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.41/0.58 Following clause subsumed by 915 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.41/0.58 Following clause subsumed by 911 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),times_times(nat,A,B)),times_times(nat,C,B)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),C)).
% 0.41/0.58 Following clause subsumed by 925 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),hAPP(nat,int,semiring_1_of_nat(int),A)),hAPP(nat,int,semiring_1_of_nat(int),B))).
% 0.41/0.58 Following clause subsumed by 924 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),hAPP(nat,int,semiring_1_of_nat(int),A)),hAPP(nat,int,semiring_1_of_nat(int),B))).
% 0.41/0.58 Following clause subsumed by 942 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(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.41/0.58 Following clause subsumed by 942 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(times_times(int,B,C),zero_zero(int)),A)).
% 0.41/0.58 Following clause subsumed by 970 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.41/0.58 Following clause subsumed by 966 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 969 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 970 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 978 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|A!=B.
% 0.41/0.58 Following clause subsumed by 978 during input processing: 0 [] {-} A!=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B)).
% 0.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 975 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.41/0.58 Following clause subsumed by 978 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|A!=B.
% 0.41/0.58 Following clause subsumed by 979 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),A),B))|B!=A.
% 0.41/0.58 Following clause subsumed by 989 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,zcong(A,B),C))| -hBOOL(hAPP(int,bool,zcong(B,A),C)).
% 0.41/0.58 Following clause subsumed by 803 during input processing: 0 [] {-} -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),minus_minus(int,B,one_one(int))))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)).
% 0.41/0.58 Following clause subsumed by 941 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.41/0.58 Following clause subsumed by 835 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,zprime,B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),B),times_times(int,A,C)))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),B),A))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),B),C)).
% 0.41/0.58 Following clause subsumed by 857 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),times_times(int,A,B)),times_times(int,A,C))).
% 0.41/0.58 Following clause subsumed by 1022 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),plus_plus(A,D,E)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),plus_plus(A,minus_minus(A,D,times_times(A,F,C)),E))).
% 0.41/0.58 Following clause subsumed by 1021 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),plus_plus(A,D,E)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),dvd_dvd(A),B),plus_plus(A,minus_minus(A,D,times_times(A,F,C)),E))).
% 0.41/0.58 Following clause subsumed by 717 during input processing: 0 [] {-} times_times(nat,A,B)!=times_times(nat,A,C)|A=zero_zero(nat)|B=C.
% 0.41/0.58 Following clause subsumed by 719 during input processing: 0 [] {-} times_times(nat,A,B)=times_times(nat,A,C)|A!=zero_zero(nat).
% 0.41/0.58 Following clause subsumed by 718 during input processing: 0 [] {-} times_times(nat,A,B)=times_times(nat,A,C)|B!=C.
% 0.41/0.58 Following clause subsumed by 770 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),times_times(nat,A,B)),times_times(nat,A,C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.41/0.58 Following clause subsumed by 765 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),times_times(nat,A,B)),times_times(nat,A,C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),C)).
% 0.41/0.58 Following clause subsumed by 718 during input processing: 0 [] {-} -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),A))|times_times(nat,A,B)=times_times(nat,A,C)|B!=C.
% 0.41/0.58 Following clause subsumed by 912 during input processing: 0 [] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),times_times(nat,A,B)),times_times(nat,A,C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.41/0.58 Following clause subsumed by 944 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),times_times(nat,A,B)),times_times(nat,A,C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.41/0.58 Following clause subsumed by 912 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),times_times(nat,A,B)),times_times(nat,A,C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),dvd_dvd(nat),B),C)).
% 0.48/0.64 Following clause subsumed by 708 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),times_times(nat,A,B)),times_times(nat,A,C)))|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.48/0.64 Following clause subsumed by 701 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),times_times(nat,A,B)),times_times(nat,A,C)))| -hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),B),C)).
% 0.48/0.64 Following clause subsumed by 131 during input processing: 0 [copy,130,flip.1] {-} bit0(A)!=bit1(B).
% 0.48/0.64 Following clause subsumed by 130 during input processing: 0 [copy,131,flip.1] {-} bit1(A)!=bit0(B).
% 0.48/0.64 170 back subsumes 71.
% 0.48/0.64 171 back subsumes 72.
% 0.48/0.64 223 back subsumes 65.
% 0.48/0.64 239 back subsumes 143.
% 0.48/0.64 240 back subsumes 144.
% 0.48/0.64 241 back subsumes 145.
% 0.48/0.64 470 back subsumes 468.
% 0.48/0.64 471 back subsumes 469.
% 0.48/0.64 543 back subsumes 539.
% 0.48/0.64 600 back subsumes 597.
% 0.48/0.64 600 back subsumes 470.
% 0.48/0.64 609 back subsumes 607.
% 0.48/0.64 610 back subsumes 608.
% 0.48/0.64 691 back subsumes 170.
% 0.48/0.64 759 back subsumes 754.
% 0.48/0.64 815 back subsumes 809.
% 0.48/0.64 816 back subsumes 810.
% 0.48/0.64 903 back subsumes 642.
% 0.48/0.64 965 back subsumes 964.
% 0.48/0.64 965 back subsumes 963.
% 0.48/0.64 974 back subsumes 971.
% 0.48/0.64 974 back subsumes 966.
% 0.48/0.64 974 back subsumes 965.
% 0.48/0.64 976 back subsumes 973.
% 0.48/0.64 976 back subsumes 967.
% 0.48/0.64 977 back subsumes 972.
% 0.48/0.64 977 back subsumes 968.
% 0.48/0.64 978 back subsumes 969.
% 0.48/0.64 978 back subsumes 928.
% 0.48/0.64 979 back subsumes 970.
% 0.48/0.64 Following clause subsumed by 150 during input processing: 0 [copy,1134,flip.1] {-} plus_plus(int,plus_plus(int,one_one(int),A),A)!=zero_zero(int).
% 0.48/0.64 1255 back subsumes 1253.
% 0.48/0.64
% 0.48/0.64 ------------> process sos:
% 0.48/0.64 Following clause subsumed by 1418 during input processing: 0 [demod,1428] {-} plus_plus(int,pls,A)=plus_plus(int,A,pls).
% 0.48/0.64 Following clause subsumed by 1418 during input processing: 0 [demod,1387,1425,1428] {-} plus_plus(int,pls,A)=plus_plus(int,A,pls).
% 0.48/0.64 Following clause subsumed by 1458 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.48/0.64 Following clause subsumed by 1458 during input processing: 0 [factor_simp] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),A),B))|A=B|hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),B),A)).
% 0.48/0.64 Following clause subsumed by 1464 during input processing: 0 [demod,1398,1398] {-} 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.48/0.64 Following clause subsumed by 1393 during input processing: 0 [] {-} plus_plus(int,hAPP(nat,int,semiring_1_of_nat(int),A),hAPP(nat,int,semiring_1_of_nat(int),B))=hAPP(nat,int,semiring_1_of_nat(int),plus_plus(nat,A,B)).
% 0.48/0.64 Following clause subsumed by 1388 during input processing: 0 [] {-} hAPP(nat,int,power_power(int,hAPP(nat,int,semiring_1_of_nat(int),A)),B)=hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,power_power(nat,A),B)).
% 0.48/0.64 Following clause subsumed by 1454 during input processing: 0 [demod,1398,1412,1490] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),number_number_of(nat,pls)),tn)).
% 0.48/0.64 Following clause subsumed by 1491 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),pls)).
% 0.48/0.64 Following clause subsumed by 1491 during input processing: 0 [demod,1387,1457,1387,1457] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),plus_plus(int,pls,pls)),plus_plus(int,pls,pls))).
% 0.48/0.64 Following clause subsumed by 1400 during input processing: 0 [demod,1387,1457,1542,1398] {-} number_number_of(nat,pls)=number_number_of(nat,pls).
% 0.48/0.64 Following clause subsumed by 1547 during input processing: 0 [demod,1412,1409,1457,1545] {-} number_number_of(nat,bit1(pls))=number_number_of(nat,bit1(pls)).
% 0.48/0.64 Following clause subsumed by 1554 during input processing: 0 [demod,1387,1457] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),plus_plus(int,pls,pls)),hAPP(nat,int,semiring_1_of_nat(int),A))).
% 0.48/0.64 Following clause subsumed by 1547 during input processing: 0 [demod,1457,1545] {-} number_number_of(nat,bit1(bit1(pls)))=number_number_of(nat,bit1(bit1(pls))).
% 0.48/0.65 Following clause subsumed by 1594 during input processing: 0 [demod,1409,1457,1416,1433,1433,1416,1457,1416,1416,1416,1536,1566,1523,1523,1536,1566,1523,1523,1536,1566,1523,1523,1536,1566,1523,1523,1523,1416,1416,1416,1416,1416,1416,1416,1416,1409,1457,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),plus_plus(int,bit1(pls),plus_plus(int,pls,hAPP(nat,int,semiring_1_of_nat(int),n)))),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,bit1(pls),pls)))))))))))))))).
% 0.48/0.65 Following clause subsumed by 1596 during input processing: 0 [demod,1433,1433,1416,1457,1416,1416,1416,1536,1566,1523,1523,1536,1566,1523,1523,1536,1566,1523,1523,1536,1566,1523,1523,1523,1416,1416,1416,1416,1416,1416,1416,1416,1409,1457,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1409,1457,1416,1534,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1566,1523,1523,1523,1416,1416,1534,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1566,1523,1523,1523,1416,1416,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1523,1536,1536,1523,1536,1566,1523,1523,1523,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416,1416] {-} hBOOL(hAPP(int,bool,twoSqu658283162sum2sq,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,bit1(pls)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,bit1(pls)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,bit1(pls)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,bit1(pls)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,bit1(pls),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,pls),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,pls),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,pls),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,pls),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,hAPP(nat,int,semiring_1_of_nat(int),n)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,hAPP(nat,int,semiring_1_of_nat(int),n)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,hAPP(nat,int,semiring_1_of_nat(int),n)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,hAPP(nat,int,semiring_1_of_nat(int),n)),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,hAPP(nat,int,semiring_1_of_nat(int),n),pls)))))))))))))))))))))))))))))))))))))))))))))))))))).
% 0.48/0.65 Following clause subsumed by 1598 during input processing: 0 [demod,1398] {-} hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),number_number_of(nat,pls)),A)).
% 0.48/0.65 Following clause subsumed by 1672 during input processing: 0 [] {-} times_times(int,hAPP(nat,int,semiring_1_of_nat(int),A),hAPP(nat,int,semiring_1_of_nat(int),B))=hAPP(nat,int,semiring_1_of_nat(int),times_times(nat,A,B)).
% 0.59/0.78 Following clause subsumed by 1715 during input processing: 0 [demod,1433,1433,1416,1457,1626,1631,1536,1566,1523,1523,1536,1566,1523,1523,1526,1566,1523,1523,1566,1523,1523,1416,1416,1416,1416,1416,1416,1523,1409,1457,1626,1433,1457,1626,1720] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),dvd_dvd(int),plus_plus(int,minus_minus(int,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,m,plus_plus(int,pls,plus_plus(int,pls,m))))))))))),pls),minus_minus(int,bit1(pls),pls))),plus_plus(int,minus_minus(int,plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,$c5),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,$c5),plus_plus(int,pls,plus_plus(int,pls,plus_plus(int,times_times(int,m,$c5),plus_plus(int,pls,plus_plus(int,pls,times_times(int,m,$c5)))))))))))),pls),minus_minus(int,plus_plus(int,pls,plus_plus(int,pls,$c5)),pls)))).
% 0.59/0.78 Following clause subsumed by 1491 during input processing: 0 [] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min),min)).
% 0.59/0.78 Following clause subsumed by 1491 during input processing: 0 [demod,1387,1457,1626,1457,1626] {-} hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),minus_minus(int,pls,pls)),minus_minus(int,pls,pls))).
% 0.59/0.78 Following clause subsumed by 1389 during input processing: 0 [copy,1388,flip.1] {-} hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,power_power(nat,A),B))=hAPP(nat,int,power_power(int,hAPP(nat,int,semiring_1_of_nat(int),A)),B).
% 0.59/0.78 Following clause subsumed by 1388 during input processing: 0 [copy,1389,flip.1] {-} hAPP(nat,int,power_power(int,hAPP(nat,int,semiring_1_of_nat(int),A)),B)=hAPP(nat,int,semiring_1_of_nat(int),hAPP(nat,nat,power_power(nat,A),B)).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1400,flip.1] {-} number_number_of(nat,pls)=number_number_of(nat,pls).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1414,flip.1] {-} number_number_of(nat,bit1(pls))=number_number_of(nat,bit1(pls)).
% 0.59/0.78 Following clause subsumed by 1417 during input processing: 0 [copy,1417,flip.1] {-} plus_plus(int,A,plus_plus(int,B,C))=plus_plus(int,B,plus_plus(int,A,C)).
% 0.59/0.78 Following clause subsumed by 1418 during input processing: 0 [copy,1418,flip.1] {-} plus_plus(int,A,B)=plus_plus(int,B,A).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1435,flip.1,demod,1626,1626] {-} minus_minus(int,A,pls)=minus_minus(int,A,pls).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1452,flip.1] {-} pls=pls.
% 0.59/0.78 Following clause subsumed by 1459 during input processing: 0 [copy,1459,flip.1] {-} plus_plus(nat,A,B)=plus_plus(nat,B,A).
% 0.59/0.78 Following clause subsumed by 1460 during input processing: 0 [copy,1460,flip.1] {-} plus_plus(nat,A,plus_plus(nat,B,C))=plus_plus(nat,B,plus_plus(nat,A,C)).
% 0.59/0.78 1491 back subsumes 1256.
% 0.59/0.78 Following clause subsumed by 1492 during input processing: 0 [copy,1492,flip.1] {-} times_times(int,A,B)=times_times(int,B,A).
% 0.59/0.78 1493 back subsumes 820.
% 0.59/0.78 Following clause subsumed by 1496 during input processing: 0 [copy,1496,flip.1] {-} minus_minus(nat,minus_minus(nat,A,B),C)=minus_minus(nat,minus_minus(nat,A,C),B).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1547,flip.1] {-} number_number_of(nat,A)=number_number_of(nat,A).
% 0.59/0.78 1547 back subsumes 1414.
% 0.59/0.78 1547 back subsumes 1400.
% 0.59/0.78 1613 back subsumes 1239.
% 0.59/0.78 Following clause subsumed by 1616 during input processing: 0 [copy,1616,flip.1] {-} times_times(nat,A,B)=times_times(nat,B,A).
% 0.59/0.78 Following clause subsumed by 1673 during input processing: 0 [copy,1672,flip.1] {-} hAPP(nat,int,semiring_1_of_nat(int),times_times(nat,A,B))=times_times(int,hAPP(nat,int,semiring_1_of_nat(int),A),hAPP(nat,int,semiring_1_of_nat(int),B)).
% 0.59/0.78 Following clause subsumed by 1672 during input processing: 0 [copy,1673,flip.1] {-} times_times(int,hAPP(nat,int,semiring_1_of_nat(int),A),hAPP(nat,int,semiring_1_of_nat(int),B))=hAPP(nat,int,semiring_1_of_nat(int),times_times(nat,A,B)).
% 0.59/0.78 Following clause subsumed by 1708 during input processing: 0 [copy,1708,flip.1] {-} times_times(real,A,B)=times_times(real,B,A).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1743,flip.1] {-} minus_minus(int,min,plus_plus(int,A,A))=minus_minus(int,min,plus_plus(int,A,A)).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1810,flip.1] {-} plus_plus(nat,times_times(nat,A,B),plus_plus(nat,times_times(nat,C,B),D))=plus_plus(nat,times_times(nat,A,B),plus_plus(nat,times_times(nat,C,B),D)).
% 0.59/0.78 Following clause subsumed by 1973 during input processing: 0 [copy,1973,flip.1] {-} A=A.
% 0.59/0.78 1973 back subsumes 1810.
% 0.59/0.78 1973 back subsumes 1743.
% 0.59/0.78 1973 back subsumes 1547.
% 0.59/0.78 1973 back subsumes 1452.
% 0.59/0.78 1973 back subsumes 1289.
% 0.59/0.78 1973 back subsumes 1278.
% 0.69/0.86 1973 back subsumes 1257.
% 0.69/0.86 1973 back subsumes 1242.
% 0.69/0.86 1973 back subsumes 1241.
% 0.69/0.86 1973 back subsumes 1229.
% 0.69/0.86 1973 back subsumes 1142.
% 0.69/0.86 Following clause subsumed by 1393 during input processing: 0 [copy,2108,flip.1] {-} plus_plus(int,hAPP(nat,int,semiring_1_of_nat(int),A),hAPP(nat,int,semiring_1_of_nat(int),B))=hAPP(nat,int,semiring_1_of_nat(int),plus_plus(nat,A,B)).
% 0.69/0.86 Following clause subsumed by 2420 during input processing: 0 [copy,2419,flip.1] {-} bit1(A)!=plus_plus(int,B,B).
% 0.69/0.86 Following clause subsumed by 2419 during input processing: 0 [copy,2420,flip.1] {-} plus_plus(int,A,A)!=bit1(B).
% 0.69/0.86 Following clause subsumed by 1440 during input processing: 0 [copy,2437,flip.1] {-} plus_plus(int,A,plus_plus(int,A,bit1(B)))=plus_plus(int,bit1(A),plus_plus(int,B,B)).
% 0.69/0.86 Following clause subsumed by 2444 during input processing: 0 [copy,2438,flip.1] {-} bit1(A)=plus_plus(int,bit1(pls),plus_plus(int,A,A)).
% 0.69/0.86 Following clause subsumed by 2438 during input processing: 0 [copy,2444,flip.1] {-} plus_plus(int,bit1(pls),plus_plus(int,A,A))=bit1(A).
% 0.69/0.86 Following clause subsumed by 1504 during input processing: 0 [copy,2456,flip.1] {-} minus_minus(nat,A,A)=number_number_of(nat,pls).
% 0.69/0.86 Following clause subsumed by 1517 during input processing: 0 [copy,2457,flip.1] {-} minus_minus(nat,minus_minus(nat,A,B),C)=minus_minus(nat,A,plus_plus(nat,B,C)).
% 0.69/0.86 Following clause subsumed by 1549 during input processing: 0 [copy,2464,flip.1] {-} minus_minus(nat,A,plus_plus(nat,A,B))=number_number_of(nat,pls).
% 0.69/0.86 Following clause subsumed by 1661 during input processing: 0 [copy,2511,flip.1] {-} hAPP(nat,int,power_power(int,hAPP(nat,int,power_power(int,A),B)),C)=hAPP(nat,int,power_power(int,A),times_times(nat,B,C)).
% 0.69/0.86 Following clause subsumed by 1967 during input processing: 0 [copy,2523,flip.1] {-} if(A,fTrue,B,C)=ti(A,B).
% 0.69/0.86 Following clause subsumed by 1968 during input processing: 0 [copy,2524,flip.1] {-} if(A,fFalse,B,C)=ti(A,C).
% 0.69/0.86 Following clause subsumed by 1973 during input processing: 0 [copy,2540,flip.1,demod,2719,2719,2765,2719,2719] {-} abs_abs(int,hAPP(nat,int,power_power(int,A),plus_plus(nat,number_number_of(nat,plus_plus(int,pls,minus_minus(int,pls,min))),number_number_of(nat,plus_plus(int,pls,minus_minus(int,pls,min))))))=abs_abs(int,hAPP(nat,int,power_power(int,A),plus_plus(nat,number_number_of(nat,plus_plus(int,pls,minus_minus(int,pls,min))),number_number_of(nat,plus_plus(int,pls,minus_minus(int,pls,min)))))).
% 0.69/0.86 Following clause subsumed by 1973 during input processing: 0 [copy,2550,flip.1,demod,2719,2719,1416,2719,2719,2722] {-} hAPP(nat,int,power_power(int,A),number_number_of(nat,plus_plus(int,pls,plus_plus(int,minus_minus(int,pls,min),minus_minus(int,plus_plus(int,pls,minus_minus(int,pls,min)),min)))))=hAPP(nat,int,power_power(int,A),number_number_of(nat,plus_plus(int,pls,plus_plus(int,minus_minus(int,pls,min),minus_minus(int,plus_plus(int,pls,minus_minus(int,pls,min)),min))))).
% 0.69/0.86 2605 back subsumes 204.
% 0.69/0.86 Following clause subsumed by 2357 during input processing: 0 [copy,2710,flip.1] {-} plus_plus(int,A,plus_plus(int,B,plus_plus(int,A,B)))=plus_plus(int,A,plus_plus(int,A,plus_plus(int,B,B))).
% 0.69/0.86 Following clause subsumed by 2894 during input processing: 0 [copy,2890,flip.1] {-} plus_plus(int,minus_minus(int,pls,min),plus_plus(int,A,A))=plus_plus(int,A,minus_minus(int,A,min)).
% 0.69/0.86 Following clause subsumed by 2890 during input processing: 0 [copy,2894,flip.1] {-} plus_plus(int,A,minus_minus(int,A,min))=plus_plus(int,minus_minus(int,pls,min),plus_plus(int,A,A)).
% 0.69/0.86 Following clause subsumed by 2983 during input processing: 0 [copy,2895,flip.1] {-} plus_plus(int,A,plus_plus(int,A,plus_plus(int,B,minus_minus(int,B,min))))=plus_plus(int,A,plus_plus(int,minus_minus(int,A,min),plus_plus(int,B,B))).
% 0.69/0.86 Following clause subsumed by 2905 during input processing: 0 [copy,2904,flip.1] {-} plus_plus(int,A,A)!=plus_plus(int,B,minus_minus(int,B,min)).
% 0.69/0.86 Following clause subsumed by 2904 during input processing: 0 [copy,2905,flip.1] {-} plus_plus(int,A,minus_minus(int,A,min))!=plus_plus(int,B,B).
% 0.69/0.86 Following clause subsumed by 2895 during input processing: 0 [copy,2983,flip.1] {-} plus_plus(int,A,plus_plus(int,minus_minus(int,A,min),plus_plus(int,B,B)))=plus_plus(int,A,plus_plus(int,A,plus_plus(int,B,minus_minus(int,B,min)))).
% 0.69/0.86 Following clause subsumed by 3024 during input processing: 0 [copy,3023,flip.1] {-} plus_plus(int,A,plus_plus(int,minus_minus(int,A,min),plus_plus(int,B,minus_minus(int,B,min))))=plus_plus(int,A,plus_plus(int,B,plus_plus(int,pls,plus_plus(int,minus_minus(int,pls,min),plus_plus(int,pls,plus_plus(int,A,minus_minus(int,B,min))))))).
% 0.69/0.86 Following clause subsumed by 3023 during input processing: 0 [copy,3024,flip.1] {-} plus_plus(int,A,plus_plus(int,B,plus_plus(int,pls,plus_plus(int,minus_minus(int,pls,min),plus_plus(int,pls,plus_plus(int,A,minus_minus(int,B,min)))))))=plus_plus(int,A,plus_plus(int,minus_minus(int,A,min),plus_plus(int,B,minus_minus(int,B,min)))).
% 0.69/0.86 Following clause subsumed by 3030 during input processing: 0 [copy,3027,flip.1] {-} minus_minus(int,plus_plus(int,times_times(int,A,A),times_times(int,B,A)),plus_plus(int,times_times(int,A,B),times_times(int,B,B)))=minus_minus(int,hAPP(nat,int,power_power(int,A),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min)))),hAPP(nat,int,power_power(int,B),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min))))).
% 0.69/0.86 Following clause subsumed by 3029 during input processing: 0 [copy,3028,flip.1] {-} minus_minus(nat,hAPP(nat,nat,power_power(nat,A),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min)))),hAPP(nat,nat,power_power(nat,B),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min)))))=minus_minus(nat,plus_plus(nat,times_times(nat,A,A),times_times(nat,B,A)),plus_plus(nat,times_times(nat,A,B),times_times(nat,B,B))).
% 0.69/0.86 Following clause subsumed by 3028 during input processing: 0 [copy,3029,flip.1] {-} minus_minus(nat,plus_plus(nat,times_times(nat,A,A),times_times(nat,B,A)),plus_plus(nat,times_times(nat,A,B),times_times(nat,B,B)))=minus_minus(nat,hAPP(nat,nat,power_power(nat,A),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min)))),hAPP(nat,nat,power_power(nat,B),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min))))).
% 0.69/0.86 Following clause subsumed by 3027 during input processing: 0 [copy,3030,flip.1] {-} minus_minus(int,hAPP(nat,int,power_power(int,A),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min)))),hAPP(nat,int,power_power(int,B),plus_plus(nat,number_number_of(nat,minus_minus(int,pls,min)),number_number_of(nat,minus_minus(int,pls,min)))))=minus_minus(int,plus_plus(int,times_times(int,A,A),times_times(int,B,A)),plus_plus(int,times_times(int,A,B),times_times(int,B,B))).
% 0.69/0.86 Following clause subsumed by 2968 during input processing: 0 [copy,3061,flip.1] {-} minus_minus(int,min,plus_plus(int,A,minus_minus(int,A,min)))=minus_minus(int,plus_plus(int,min,min),plus_plus(int,A,A)).
% 0.69/0.86 Following clause subsumed by 2982 during input processing: 0 [copy,3069,flip.1] {-} plus_plus(int,times_times(int,A,B),minus_minus(int,times_times(int,A,B),times_times(int,min,B)))=plus_plus(int,times_times(int,A,B),plus_plus(int,times_times(int,A,B),B)).
% 0.69/0.86 Following clause subsumed by 2984 during input processing: 0 [copy,3070,flip.1] {-} plus_plus(int,A,plus_plus(int,B,minus_minus(int,plus_plus(int,A,B),min)))=plus_plus(int,A,plus_plus(int,minus_minus(int,A,min),plus_plus(int,B,B))).
% 0.69/0.86
% 0.69/0.86 ======= end of input processing =======
% 1.07/1.27
% 1.07/1.27 Stopped by limit on insertions
% 1.07/1.27
% 1.07/1.27
% 1.07/1.27
% 1.07/1.27 Aborting on detection of an error:
% 1.07/1.27
% 1.07/1.27 Too many clauses (whew!).
% 1.07/1.27
%------------------------------------------------------------------------------