%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NUM923+5 : TPTP v8.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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 : 300s % DateTime : Wed Jul 27 13:10:12 EDT 2022 % Result : Unknown 3.74s 3.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM923+5 : TPTP v8.1.0. Released v5.3.0. % 0.07/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 09:38:10 EDT 2022 % 0.13/0.34 % CPUTime : % 3.67/3.81 ----- Otter 3.3f, August 2004 ----- % 3.67/3.81 The process was started by sandbox2 on n011.cluster.edu, % 3.67/3.81 Wed Jul 27 09:38:11 2022 % 3.67/3.81 The command was "./otter". The process ID is 32748. % 3.67/3.81 % 3.67/3.81 set(prolog_style_variables). % 3.67/3.81 set(auto). % 3.67/3.81 dependent: set(auto1). % 3.67/3.81 dependent: set(process_input). % 3.67/3.81 dependent: clear(print_kept). % 3.67/3.81 dependent: clear(print_new_demod). % 3.67/3.81 dependent: clear(print_back_demod). % 3.67/3.81 dependent: clear(print_back_sub). % 3.67/3.81 dependent: set(control_memory). % 3.67/3.81 dependent: assign(max_mem, 12000). % 3.67/3.81 dependent: assign(pick_given_ratio, 4). % 3.67/3.81 dependent: assign(stats_level, 1). % 3.67/3.81 dependent: assign(max_seconds, 10800). % 3.67/3.81 clear(print_given). % 3.67/3.81 % 3.67/3.81 formula_list(usable). % 3.67/3.81 all A (A=A). % 3.67/3.81 all X_a (minus(X_a)->ti(fun(X_a,fun(X_a,X_a)),minus_minus(X_a))=minus_minus(X_a)). % 3.67/3.81 all X_a (ab_semigroup_add(X_a)->ti(fun(X_a,fun(X_a,X_a)),plus_plus(X_a))=plus_plus(X_a)). % 3.67/3.81 all X_a (cancel_semigroup_add(X_a)->ti(fun(X_a,fun(X_a,X_a)),plus_plus(X_a))=plus_plus(X_a)). % 3.67/3.81 all X_a (semiring(X_a)->ti(fun(X_a,fun(X_a,X_a)),times_times(X_a))=times_times(X_a)). % 3.67/3.81 all X_a (ab_semigroup_mult(X_a)->ti(fun(X_a,fun(X_a,X_a)),times_times(X_a))=times_times(X_a)). % 3.67/3.81 all X_a (ti(X_a,undefined(X_a))=undefined(X_a)). % 3.67/3.81 all X_b (ord(X_b)->ti(fun(X_b,fun(X_b,bool)),ord_less_e_q(X_b))=ord_less_e_q(X_b)). % 3.67/3.81 all X_a X_b (ti(fun(X_a,fun(X_b,product_prod(X_a,X_b))),product_Pair(X_a,X_b))=product_Pair(X_a,X_b)). % 3.67/3.81 all X_b X_c X_a (ti(fun(fun(product_prod(X_b,X_c),X_a),fun(X_b,fun(X_c,X_a))),product_curry(X_b,X_c,X_a))=product_curry(X_b,X_c,X_a)). % 3.67/3.81 all X_b X_c X_a (ti(fun(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a)),produc1605651328_split(X_b,X_c,X_a))=produc1605651328_split(X_b,X_c,X_a)). % 3.67/3.81 all X_b X_c X_a (ti(fun(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a)),product_prod_rec(X_b,X_c,X_a))=product_prod_rec(X_b,X_c,X_a)). % 3.67/3.81 ti(fun(int,bool),twoSqu33214720sum2sq)=twoSqu33214720sum2sq. % 3.67/3.81 ti(fun(product_prod(int,int),int),twoSqu930276342sum2sq)=twoSqu930276342sum2sq. % 3.67/3.81 all X_c X_a B_1_1 B_2_1 (hAPP(X_c,X_a,ti(fun(X_c,X_a),B_1_1),B_2_1)=hAPP(X_c,X_a,B_1_1,B_2_1)). % 3.67/3.81 all X_c X_a B_1_1 B_2_1 (hAPP(X_c,X_a,B_1_1,ti(X_c,B_2_1))=hAPP(X_c,X_a,B_1_1,B_2_1)). % 3.67/3.81 all X_a X_c B_1_1 B_2_1 (ti(X_a,hAPP(X_c,X_a,B_1_1,B_2_1))=hAPP(X_c,X_a,B_1_1,B_2_1)). % 3.67/3.81 all B_1_1 (hBOOL(ti(bool,B_1_1))<->hBOOL(B_1_1)). % 3.67/3.81 ti(int,a)=a. % 3.67/3.81 ti(int,b)=b. % 3.67/3.81 ti(int,p)=p. % 3.67/3.81 ti(int,q)=q. % 3.67/3.81 all A_1 R B M C_1 D N (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A_1),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),R),B))),M)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),C_1),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),R),D))),N))=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A_1),M)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),C_1),N))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),R),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),M)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),D),N))))). % 3.67/3.81 all X_a (ring(X_a)-> (all X_1 Y A_1 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Y)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Y),B))),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),A_1)),B))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all X_1 Y A_1 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Y)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),A_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Y),B))),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),A_1)),B))),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Y),B)))))). % 3.67/3.81 all X_a (ring(X_a)-> (all Aa E C Ba D_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)<->ti(X_a,C)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Ba),Aa)),E)),D_1)))). % 3.67/3.81 all X_a (ring(X_a)-> (all Aa E C Ba D_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)<->hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)),E)),C)=ti(X_a,D_1)))). % 3.67/3.81 all X_2 (hBOOL(hAPP(int,bool,twoSqu33214720sum2sq,X_2))<-> (exists A_2 B_1 (hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),A_2),B_1))=X_2))). % 3.67/3.81 all A_1 B C_1 (hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A_1),B)=C_1->A_1=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),C_1),B)). % 3.67/3.81 all W Z1 Z2 (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),Z1),Z2))=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z1)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z2))). % 3.67/3.81 all Z1 Z2 W (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),Z1),Z2)),W)=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),W)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z2),W))). % 3.67/3.81 all W Z1 Z2 (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z1)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z2))). % 3.67/3.81 all Z1 Z2 W (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2)),W)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),W)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z2),W))). % 3.67/3.81 all X_a (group_add(X_a)-> (all A_1 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),A_1),B)),B)=ti(X_a,A_1)))). % 3.67/3.81 all X_a (ab_semigroup_mult(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),C_1))))). % 3.67/3.81 all X_a (cancel_semigroup_add(X_a)-> (all B A_1 C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),A_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)->ti(X_a,B)=ti(X_a,C_1)))). % 3.67/3.81 all X_a (cancel146912293up_add(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)->ti(X_a,B)=ti(X_a,C_1)))). % 3.67/3.81 all X_a (cancel_semigroup_add(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)->ti(X_a,B)=ti(X_a,C_1)))). % 3.67/3.81 all X_a (cancel_semigroup_add(X_a)-> (all Ba Aa C (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Ba),Aa)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Aa)<->ti(X_a,Ba)=ti(X_a,C)))). % 3.67/3.81 all X_a (cancel_semigroup_add(X_a)-> (all Aa Ba C (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),Ba)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),C)<->ti(X_a,Ba)=ti(X_a,C)))). % 3.67/3.81 all X_a (ab_semigroup_add(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1))))). % 3.67/3.81 all X_a (ab_group_add(X_a)-> (all Aa Ba C D_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C),D_1)-> (ti(X_a,Aa)=ti(X_a,Ba)<->ti(X_a,C)=ti(X_a,D_1))))). % 3.67/3.81 all Z1 Z2 Z3 (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),Z2)),Z3)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z2),Z3))). % 3.67/3.81 all Z W (hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z),W)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z)). % 3.67/3.81 all Z1 Z2 Z3 (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2)),Z3)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z2),Z3))). % 3.67/3.81 all X_1 Y Z (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X_1),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Y),Z))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Y),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X_1),Z))). % 3.67/3.81 all Z W (hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z),W)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),W),Z)). % 3.67/3.81 all X_a (semiring(X_a)-> (all A_1 E_2 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),E_2)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),E_2)),C_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),E_2)),C_1)))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all X_1 Y Ya (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),X_1),Y)),Ya)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Ya)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Y),Ya))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all A_1 A_4 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),A_4)),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_4),B))))). % 3.67/3.81 all X_a (comm_semiring(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),C_1))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all Xa X_1 Y (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),X_1),Y))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),X_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),Y))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all A_1 B B_3 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),B_3))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B_3))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all X_1 Y Ya (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),Y)),Ya)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Ya)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Y),Ya))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all A_1 A_4 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),A_1),A_4)),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_4),B))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all Xa X_1 Y (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),Y))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),X_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),Y))))). % 3.67/3.81 all X_a (real_normed_algebra(X_a)-> (all A_1 B B_3 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),B),B_3))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B_3))))). % 3.67/3.81 all X_a (ab_group_add(X_a)-> (all A_1 C_1 B D (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C_1),D))))). % 3.67/3.81 all X_a (group_add(X_a)-> (all A_1 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),B)=ti(X_a,A_1)))). % 3.67/3.81 all X_a (semiri456707255roduct(X_a)-> (all W_1 Y_2 X_2 Z_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Y_2)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Z_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Z_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Y_2))<->ti(X_a,W_1)=ti(X_a,X_2)|ti(X_a,Y_2)=ti(X_a,Z_1)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 M B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),M)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),M))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),M)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),C_1))))). % 3.67/3.81 all X_a (semiri456707255roduct(X_a)-> (all C D_1 Aa Ba (ti(X_a,Aa)!=ti(X_a,Ba)&ti(X_a,C)!=ti(X_a,D_1)<->hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),D_1))!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),D_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),C))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all X_1 Y Z (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Y),Z))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Y)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Z))))). % 3.67/3.81 all X_b X_a (minus(X_a)-> (all A_5 B_4 X_2 (hAPP(X_b,X_a,hAPP(fun(X_b,X_a),fun(X_b,X_a),hAPP(fun(X_b,X_a),fun(fun(X_b,X_a),fun(X_b,X_a)),minus_minus(fun(X_b,X_a)),A_5),B_4),X_2)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_b,X_a,A_5,X_2)),hAPP(X_b,X_a,B_4,X_2))))). % 3.67/3.81 all X_a X_b (minus(X_b)-> (all A_5 B_4 X (hAPP(X_a,X_b,hAPP(fun(X_a,X_b),fun(X_a,X_b),hAPP(fun(X_a,X_b),fun(fun(X_a,X_b),fun(X_a,X_b)),minus_minus(fun(X_a,X_b)),A_5),B_4),X)=hAPP(X_b,X_b,hAPP(X_b,fun(X_b,X_b),minus_minus(X_b),hAPP(X_a,X_b,A_5,X)),hAPP(X_a,X_b,B_4,X))))). % 3.67/3.81 all X_b X_a A_1 B A_4 B_3 (hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_1),B)=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_4),B_3)-> -(ti(X_a,A_1)=ti(X_a,A_4)->ti(X_b,B)!=ti(X_b,B_3))). % 3.67/3.81 all X_b X_a Aa Ba A_3 B_2 (hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_3),B_2)<->ti(X_a,Aa)=ti(X_a,A_3)&ti(X_b,Ba)=ti(X_b,B_2)). % 3.67/3.81 all X_a (ab_sem1668676832m_mult(X_a)-> (all A_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),A_1)=ti(X_a,A_1)))). % 3.67/3.81 all X_a (ab_sem1668676832m_mult(X_a)-> (all X_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),X_1)=ti(X_a,X_1)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),A_1)))). % 3.67/3.81 all X_a (ab_sem1668676832m_mult(X_a)-> (all A_1 B (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Rx Ry (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ry))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Rx Ry (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Rx)),Ry)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Ly Rx (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),Rx)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ly),Rx))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Ly Rx (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),Rx)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Rx)),Ly)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Ly Rx Ry (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ly),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry)))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Ly Rx Ry (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),Ry))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all Lx Ly Rx Ry (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Rx)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ly),Ry))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 C_1 D (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),D))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 C_1 D (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),D)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1))))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 B C_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),B)))). % 3.67/3.81 all X_a (comm_semiring_1(X_a)-> (all A_1 B C_1 D (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),D))))). % 3.67/3.81 all X_a X_b P_1 ((all X1 hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,X1)))<-> (all A_2 B_1 hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_2),B_1))))). % 3.67/3.81 all X_b X_c X_a F1 Aa Ba (hAPP(product_prod(X_b,X_c),X_a,hAPP(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a),product_prod_rec(X_b,X_c,X_a),F1),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),Aa),Ba))=hAPP(X_c,X_a,hAPP(X_b,fun(X_c,X_a),F1,Aa),Ba)). % 3.67/3.81 all X_a X_b P_1 ((exists X1 hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,X1)))<-> (exists A_2 B_1 hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_2),B_1))))). % 3.67/3.81 all X_a X_b X_c X_d X_e X_f X_2 P_1 ((all A_2 B_1 C_2 D_2 E_1 F_1 hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),bool,P_1,hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),A_2),hAPP(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),B_1),hAPP(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),hAPP(X_c,fun(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_Pair(X_c,product_prod(X_d,product_prod(X_e,X_f))),C_2),hAPP(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f)),hAPP(X_d,fun(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f))),product_Pair(X_d,product_prod(X_e,X_f)),D_2),hAPP(X_f,product_prod(X_e,X_f),hAPP(X_e,fun(X_f,product_prod(X_e,X_f)),product_Pair(X_e,X_f),E_1),F_1))))))))->hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),bool,P_1,X_2))). % 3.67/3.81 all X_a X_b X_c X_d X_e X_f Y (-(all A_2 B_1 C_2 D_2 E_1 F_1 (ti(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),Y)!=hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),A_2),hAPP(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),B_1),hAPP(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),hAPP(X_c,fun(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_Pair(X_c,product_prod(X_d,product_prod(X_e,X_f))),C_2),hAPP(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f)),hAPP(X_d,fun(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f))),product_Pair(X_d,product_prod(X_e,X_f)),D_2),hAPP(X_f,product_prod(X_e,X_f),hAPP(X_e,fun(X_f,product_prod(X_e,X_f)),product_Pair(X_e,X_f),E_1),F_1)))))))). % 3.67/3.81 all X_a X_b X_c X_d X_e Y (-(all A_2 B_1 C_2 D_2 E_1 (ti(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),Y)!=hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),A_2),hAPP(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,X_e))),B_1),hAPP(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e)),hAPP(X_c,fun(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e))),product_Pair(X_c,product_prod(X_d,X_e)),C_2),hAPP(X_e,product_prod(X_d,X_e),hAPP(X_d,fun(X_e,product_prod(X_d,X_e)),product_Pair(X_d,X_e),D_2),E_1))))))). % 3.67/3.81 all X_a X_b X_c X_d X_e X_2 P_1 ((all A_2 B_1 C_2 D_2 E_1 hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),bool,P_1,hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),A_2),hAPP(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,X_e))),B_1),hAPP(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e)),hAPP(X_c,fun(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e))),product_Pair(X_c,product_prod(X_d,X_e)),C_2),hAPP(X_e,product_prod(X_d,X_e),hAPP(X_d,fun(X_e,product_prod(X_d,X_e)),product_Pair(X_d,X_e),D_2),E_1)))))))->hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),bool,P_1,X_2))). % 3.67/3.81 all X_a X_b X_c X_d Y (-(all A_2 B_1 C_2 D_2 (ti(product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),Y)!=hAPP(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d)))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,X_d))),A_2),hAPP(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d)),hAPP(X_b,fun(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d))),product_Pair(X_b,product_prod(X_c,X_d)),B_1),hAPP(X_d,product_prod(X_c,X_d),hAPP(X_c,fun(X_d,product_prod(X_c,X_d)),product_Pair(X_c,X_d),C_2),D_2)))))). % 3.67/3.81 all X_a X_b X_c X_d X_2 P_1 ((all A_2 B_1 C_2 D_2 hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),bool,P_1,hAPP(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d)))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,X_d))),A_2),hAPP(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d)),hAPP(X_b,fun(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d))),product_Pair(X_b,product_prod(X_c,X_d)),B_1),hAPP(X_d,product_prod(X_c,X_d),hAPP(X_c,fun(X_d,product_prod(X_c,X_d)),product_Pair(X_c,X_d),C_2),D_2))))))->hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),bool,P_1,X_2))). % 3.67/3.81 all X_a X_b X_c X_2 P_1 ((all A_2 B_1 C_2 hBOOL(hAPP(product_prod(X_a,product_prod(X_b,X_c)),bool,P_1,hAPP(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c)),hAPP(X_a,fun(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c))),product_Pair(X_a,product_prod(X_b,X_c)),A_2),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),B_1),C_2)))))->hBOOL(hAPP(product_prod(X_a,product_prod(X_b,X_c)),bool,P_1,X_2))). % 3.67/3.81 all X_a X_b X_c Y (-(all A_2 B_1 C_2 (ti(product_prod(X_a,product_prod(X_b,X_c)),Y)!=hAPP(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c)),hAPP(X_a,fun(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c))),product_Pair(X_a,product_prod(X_b,X_c)),A_2),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),B_1),C_2))))). % 3.67/3.81 all X_a X_b Y (-(all A_2 B_1 (ti(product_prod(X_a,X_b),Y)!=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_2),B_1)))). % 3.67/3.81 all X_a X_b F G ((all X (hAPP(X_a,X_b,F,X)=hAPP(X_a,X_b,G,X)))->ti(fun(X_a,X_b),F)=ti(fun(X_a,X_b),G)). % 3.67/3.81 all X_a X_b P (-(all X Y_1 (ti(product_prod(X_a,X_b),P)!=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),X),Y_1)))). % 3.67/3.81 all X_b X_c X_a C Aa Ba (hAPP(product_prod(X_b,X_c),X_a,hAPP(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a),produc1605651328_split(X_b,X_c,X_a),C),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),Aa),Ba))=hAPP(X_c,X_a,hAPP(X_b,fun(X_c,X_a),C,Aa),Ba)). % 3.67/3.81 all X_a X_b F Aa Ba (hBOOL(hAPP(product_prod(X_a,X_b),bool,F,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)))->hBOOL(hAPP(X_b,bool,hAPP(X_a,fun(X_b,bool),hAPP(fun(product_prod(X_a,X_b),bool),fun(X_a,fun(X_b,bool)),product_curry(X_a,X_b,bool),F),Aa),Ba))). % 3.67/3.81 all X_b X_a F Aa Ba (hBOOL(hAPP(X_b,bool,hAPP(X_a,fun(X_b,bool),hAPP(fun(product_prod(X_a,X_b),bool),fun(X_a,fun(X_b,bool)),product_curry(X_a,X_b,bool),F),Aa),Ba))->hBOOL(hAPP(product_prod(X_a,X_b),bool,F,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)))). % 3.67/3.81 all X_b X_a F Aa Ba (hBOOL(hAPP(X_b,bool,hAPP(X_a,fun(X_b,bool),hAPP(fun(product_prod(X_a,X_b),bool),fun(X_a,fun(X_b,bool)),product_curry(X_a,X_b,bool),F),Aa),Ba))->hBOOL(hAPP(product_prod(X_a,X_b),bool,F,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)))). % 3.67/3.81 all X_c X_a X_b F Aa Ba (hAPP(X_c,X_a,hAPP(X_b,fun(X_c,X_a),hAPP(fun(product_prod(X_b,X_c),X_a),fun(X_b,fun(X_c,X_a)),product_curry(X_b,X_c,X_a),F),Aa),Ba)=hAPP(product_prod(X_b,X_c),X_a,F,hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),Aa),Ba))). % 3.67/3.81 all X_a (ordered_ring(X_a)-> (all Aa E C Ba D_1 (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)))<->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)),E)),C)),D_1))))). % 3.67/3.81 all X_a (ordered_ring(X_a)-> (all Aa E C Ba D_1 (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)))<->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Ba),Aa)),E)),D_1)))))). % 3.67/3.81 all K I J (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),I),J))->hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K),I)),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K),J)))). % 3.67/3.81 all X_a (ordered_ab_group_add(X_a)-> (all Aa Ba C D_1 (hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C),D_1)-> (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba))<->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C),D_1)))))). % 3.67/3.81 all X_a (ordere236663937imp_le(X_a)-> (all C_1 A_1 B (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),B)))->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))))). % 3.67/3.81 all X_a (ordere236663937imp_le(X_a)-> (all A_1 C_1 B (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1)))->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))))). % 3.67/3.81 all X_a (ordere779506340up_add(X_a)-> (all C_1 D A_1 B (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))-> (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C_1),D))->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),D))))))). % 3.67/3.81 all X_a (ordere779506340up_add(X_a)-> (all C_1 A_1 B (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),B)))))). % 3.67/3.81 all X_a (ordere779506340up_add(X_a)-> (all C_1 A_1 B (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1)))))). % 3.67/3.81 all X_a (ordere236663937imp_le(X_a)-> (all C Aa Ba (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Aa)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Ba)))<->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba))))). % 3.67/3.81 all X_a (ordere236663937imp_le(X_a)-> (all Aa C Ba (hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Ba),C)))<->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba))))). % 3.67/3.81 all X_a (preorder(X_a)-> (all X_1 hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),X_1),X_1)))). % 3.67/3.81 all X_a (linorder(X_a)-> (all X_1 Y (-hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),X_1),Y))->hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Y),X_1))))). % 3.67/3.81 all W hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),W),W)). % 3.67/3.81 all Z W (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),Z),W))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),W),Z))). % 3.67/3.81 all K I J (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),I),J))-> (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),J),K))->hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),I),K)))). % 3.67/3.81 all Z W (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),Z),W))-> (hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),W),Z))->Z=W)). % 3.67/3.81 all X_a X_b (ord(X_b)-> (all F G (hBOOL(hAPP(fun(X_a,X_b),bool,hAPP(fun(X_a,X_b),fun(fun(X_a,X_b),bool),ord_less_e_q(fun(X_a,X_b)),F),G))<-> (all X hBOOL(hAPP(X_b,bool,hAPP(X_b,fun(X_b,bool),ord_less_e_q(X_b),hAPP(X_a,X_b,F,X)),hAPP(X_a,X_b,G,X))))))). % 3.67/3.81 all T_2 T_1 (preorder(T_1)->preorder(fun(T_2,T_1))). % 3.67/3.81 all T_2 T_1 (ord(T_1)->ord(fun(T_2,T_1))). % 3.67/3.81 all T_2 T_1 (minus(T_1)->minus(fun(T_2,T_1))). % 3.67/3.81 semiri456707255roduct(int). % 3.67/3.81 ordere236663937imp_le(int). % 3.67/3.81 ordere779506340up_add(int). % 3.67/3.81 cancel146912293up_add(int). % 3.67/3.81 ordered_ab_group_add(int). % 3.67/3.81 cancel_semigroup_add(int). % 3.67/3.81 ab_semigroup_mult(int). % 3.67/3.81 ab_semigroup_add(int). % 3.67/3.81 comm_semiring_1(int). % 3.67/3.81 comm_semiring(int). % 3.67/3.81 ab_group_add(int). % 3.67/3.81 ordered_ring(int). % 3.67/3.81 preorder(int). % 3.67/3.81 linorder(int). % 3.67/3.81 group_add(int). % 3.67/3.81 semiring(int). % 3.67/3.81 ord(int). % 3.67/3.81 minus(int). % 3.67/3.81 ring(int). % 3.67/3.81 preorder(bool). % 3.67/3.81 ord(bool). % 3.67/3.81 minus(bool). % 3.67/3.81 all T A (ti(T,ti(T,A))=ti(T,A)). % 3.67/3.81 hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),a),b))),hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),p),q)))!=hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),a),p)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),b),q))),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),a),q)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),b),p)))). % 3.67/3.81 end_of_list. % 3.67/3.81 % 3.67/3.81 -------> usable clausifies to: % 3.67/3.81 % 3.67/3.81 list(usable). % 3.67/3.81 0 [] A=A. % 3.67/3.81 0 [] -minus(X_a)|ti(fun(X_a,fun(X_a,X_a)),minus_minus(X_a))=minus_minus(X_a). % 3.67/3.81 0 [] -ab_semigroup_add(X_a)|ti(fun(X_a,fun(X_a,X_a)),plus_plus(X_a))=plus_plus(X_a). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|ti(fun(X_a,fun(X_a,X_a)),plus_plus(X_a))=plus_plus(X_a). % 3.67/3.81 0 [] -semiring(X_a)|ti(fun(X_a,fun(X_a,X_a)),times_times(X_a))=times_times(X_a). % 3.67/3.81 0 [] -ab_semigroup_mult(X_a)|ti(fun(X_a,fun(X_a,X_a)),times_times(X_a))=times_times(X_a). % 3.67/3.81 0 [] ti(X_a,undefined(X_a))=undefined(X_a). % 3.67/3.81 0 [] -ord(X_b)|ti(fun(X_b,fun(X_b,bool)),ord_less_e_q(X_b))=ord_less_e_q(X_b). % 3.67/3.81 0 [] ti(fun(X_a,fun(X_b,product_prod(X_a,X_b))),product_Pair(X_a,X_b))=product_Pair(X_a,X_b). % 3.67/3.81 0 [] ti(fun(fun(product_prod(X_b,X_c),X_a),fun(X_b,fun(X_c,X_a))),product_curry(X_b,X_c,X_a))=product_curry(X_b,X_c,X_a). % 3.67/3.81 0 [] ti(fun(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a)),produc1605651328_split(X_b,X_c,X_a))=produc1605651328_split(X_b,X_c,X_a). % 3.67/3.81 0 [] ti(fun(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a)),product_prod_rec(X_b,X_c,X_a))=product_prod_rec(X_b,X_c,X_a). % 3.67/3.81 0 [] ti(fun(int,bool),twoSqu33214720sum2sq)=twoSqu33214720sum2sq. % 3.67/3.81 0 [] ti(fun(product_prod(int,int),int),twoSqu930276342sum2sq)=twoSqu930276342sum2sq. % 3.67/3.81 0 [] hAPP(X_c,X_a,ti(fun(X_c,X_a),B_1_1),B_2_1)=hAPP(X_c,X_a,B_1_1,B_2_1). % 3.67/3.81 0 [] hAPP(X_c,X_a,B_1_1,ti(X_c,B_2_1))=hAPP(X_c,X_a,B_1_1,B_2_1). % 3.67/3.81 0 [] ti(X_a,hAPP(X_c,X_a,B_1_1,B_2_1))=hAPP(X_c,X_a,B_1_1,B_2_1). % 3.67/3.81 0 [] -hBOOL(ti(bool,B_1_1))|hBOOL(B_1_1). % 3.67/3.81 0 [] hBOOL(ti(bool,B_1_1))| -hBOOL(B_1_1). % 3.67/3.81 0 [] ti(int,a)=a. % 3.67/3.81 0 [] ti(int,b)=b. % 3.67/3.81 0 [] ti(int,p)=p. % 3.67/3.81 0 [] ti(int,q)=q. % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A_1),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),R),B))),M)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),C_1),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),R),D))),N))=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A_1),M)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),C_1),N))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),R),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),M)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),D),N)))). % 3.67/3.81 0 [] -ring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Y)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Y),B))),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),A_1)),B)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Y)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),A_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Y),B))),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),A_1)),B))),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Y),B))). % 3.67/3.81 0 [] -ring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)|ti(X_a,C)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Ba),Aa)),E)),D_1). % 3.67/3.81 0 [] -ring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)|ti(X_a,C)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Ba),Aa)),E)),D_1). % 3.67/3.81 0 [] -ring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)),E)),C)=ti(X_a,D_1). % 3.67/3.81 0 [] -ring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)),E)),C)!=ti(X_a,D_1). % 3.67/3.81 0 [] -hBOOL(hAPP(int,bool,twoSqu33214720sum2sq,X_2))|hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),$f2(X_2)),$f1(X_2)))=X_2. % 3.67/3.81 0 [] hBOOL(hAPP(int,bool,twoSqu33214720sum2sq,X_2))|hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),A_2),B_1))!=X_2. % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A_1),B)!=C_1|A_1=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),C_1),B). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),Z1),Z2))=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z1)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z2)). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),Z1),Z2)),W)=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),W)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z2),W)). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z1)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z2)). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2)),W)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),W)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z2),W)). % 3.67/3.81 0 [] -group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),A_1),B)),B)=ti(X_a,A_1). % 3.67/3.81 0 [] -ab_semigroup_mult(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),C_1)). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),A_1)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)|ti(X_a,B)=ti(X_a,C_1). % 3.67/3.81 0 [] -cancel146912293up_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)|ti(X_a,B)=ti(X_a,C_1). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)|ti(X_a,B)=ti(X_a,C_1). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Ba),Aa)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Aa)|ti(X_a,Ba)=ti(X_a,C). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Ba),Aa)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Aa)|ti(X_a,Ba)!=ti(X_a,C). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),Ba)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),C)|ti(X_a,Ba)=ti(X_a,C). % 3.67/3.81 0 [] -cancel_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),Ba)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),C)|ti(X_a,Ba)!=ti(X_a,C). % 3.67/3.81 0 [] -ab_semigroup_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1)). % 3.67/3.81 0 [] -ab_group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C),D_1)|ti(X_a,Aa)!=ti(X_a,Ba)|ti(X_a,C)=ti(X_a,D_1). % 3.67/3.81 0 [] -ab_group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C),D_1)|ti(X_a,Aa)=ti(X_a,Ba)|ti(X_a,C)!=ti(X_a,D_1). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),Z2)),Z3)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z1),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z2),Z3)). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z),W)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),Z2)),Z3)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z1),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z2),Z3)). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X_1),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Y),Z))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Y),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X_1),Z)). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z),W)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),W),Z). % 3.67/3.81 0 [] -semiring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),E_2)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),E_2)),C_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),E_2)),C_1). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),X_1),Y)),Ya)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Ya)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Y),Ya)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),A_4)),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_4),B)). % 3.67/3.81 0 [] -comm_semiring(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),C_1)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),X_1),Y))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),X_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),Y)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),B_3))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B_3)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),Y)),Ya)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Ya)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Y),Ya)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),A_1),A_4)),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_4),B)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),X_1),Y))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),X_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Xa),Y)). % 3.67/3.81 0 [] -real_normed_algebra(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),B),B_3))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B_3)). % 3.67/3.81 0 [] -ab_group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C_1),D)). % 3.67/3.81 0 [] -group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),B)=ti(X_a,A_1). % 3.67/3.81 0 [] -semiri456707255roduct(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Y_2)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Z_1))!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Z_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Y_2))|ti(X_a,W_1)=ti(X_a,X_2)|ti(X_a,Y_2)=ti(X_a,Z_1). % 3.67/3.81 0 [] -semiri456707255roduct(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Y_2)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Z_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Z_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Y_2))|ti(X_a,W_1)!=ti(X_a,X_2). % 3.67/3.81 0 [] -semiri456707255roduct(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Y_2)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Z_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),W_1),Z_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_2),Y_2))|ti(X_a,Y_2)!=ti(X_a,Z_1). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),M)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),M))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),M). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),C_1)). % 3.67/3.81 0 [] -semiri456707255roduct(X_a)|ti(X_a,Aa)=ti(X_a,Ba)|ti(X_a,C)=ti(X_a,D_1)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),D_1))!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),D_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),C)). % 3.67/3.81 0 [] -semiri456707255roduct(X_a)|ti(X_a,Aa)!=ti(X_a,Ba)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),D_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),D_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),C)). % 3.67/3.81 0 [] -semiri456707255roduct(X_a)|ti(X_a,C)!=ti(X_a,D_1)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),D_1))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),D_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),C)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Y),Z))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Y)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),Z)). % 3.67/3.81 0 [] -minus(X_a)|hAPP(X_b,X_a,hAPP(fun(X_b,X_a),fun(X_b,X_a),hAPP(fun(X_b,X_a),fun(fun(X_b,X_a),fun(X_b,X_a)),minus_minus(fun(X_b,X_a)),A_5),B_4),X_2)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),hAPP(X_b,X_a,A_5,X_2)),hAPP(X_b,X_a,B_4,X_2)). % 3.67/3.81 0 [] -minus(X_b)|hAPP(X_a,X_b,hAPP(fun(X_a,X_b),fun(X_a,X_b),hAPP(fun(X_a,X_b),fun(fun(X_a,X_b),fun(X_a,X_b)),minus_minus(fun(X_a,X_b)),A_5),B_4),X)=hAPP(X_b,X_b,hAPP(X_b,fun(X_b,X_b),minus_minus(X_b),hAPP(X_a,X_b,A_5,X)),hAPP(X_a,X_b,B_4,X)). % 3.67/3.81 0 [] hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_1),B)!=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_4),B_3)|ti(X_a,A_1)=ti(X_a,A_4). % 3.67/3.81 0 [] hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_1),B)!=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_4),B_3)|ti(X_b,B)=ti(X_b,B_3). % 3.67/3.81 0 [] hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)!=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_3),B_2)|ti(X_a,Aa)=ti(X_a,A_3). % 3.67/3.81 0 [] hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)!=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_3),B_2)|ti(X_b,Ba)=ti(X_b,B_2). % 3.67/3.81 0 [] hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_3),B_2)|ti(X_a,Aa)!=ti(X_a,A_3)|ti(X_b,Ba)!=ti(X_b,B_2). % 3.67/3.81 0 [] -ab_sem1668676832m_mult(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),A_1)=ti(X_a,A_1). % 3.67/3.81 0 [] -ab_sem1668676832m_mult(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),X_1),X_1)=ti(X_a,X_1). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),B),A_1). % 3.67/3.81 0 [] -ab_sem1668676832m_mult(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),A_1),B). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ry)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Rx)),Ry). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),Rx)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ly),Rx)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),Rx)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Rx)),Ly). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ly),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),Ry)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Ly)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Rx),Ry))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Lx),Rx)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ly),Ry)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),D)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),D). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1)). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),C_1)=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),B). % 3.67/3.81 0 [] -comm_semiring_1(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),B)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),D))=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),D)). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,$f3(X_a,X_b,P_1)))|hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_2),B_1))). % 3.67/3.81 0 [] hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,X1))| -hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),$f5(X_a,X_b,P_1)),$f4(X_a,X_b,P_1)))). % 3.67/3.81 0 [] hAPP(product_prod(X_b,X_c),X_a,hAPP(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a),product_prod_rec(X_b,X_c,X_a),F1),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),Aa),Ba))=hAPP(X_c,X_a,hAPP(X_b,fun(X_c,X_a),F1,Aa),Ba). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,X1))|hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),$f7(X_a,X_b,P_1)),$f6(X_a,X_b,P_1)))). % 3.67/3.81 0 [] hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,$f8(X_a,X_b,P_1)))| -hBOOL(hAPP(product_prod(X_a,X_b),bool,P_1,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),A_2),B_1))). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),bool,P_1,hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),$f14(X_a,X_b,X_c,X_d,X_e,X_f,X_2,P_1)),hAPP(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),$f13(X_a,X_b,X_c,X_d,X_e,X_f,X_2,P_1)),hAPP(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),hAPP(X_c,fun(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_Pair(X_c,product_prod(X_d,product_prod(X_e,X_f))),$f12(X_a,X_b,X_c,X_d,X_e,X_f,X_2,P_1)),hAPP(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f)),hAPP(X_d,fun(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f))),product_Pair(X_d,product_prod(X_e,X_f)),$f11(X_a,X_b,X_c,X_d,X_e,X_f,X_2,P_1)),hAPP(X_f,product_prod(X_e,X_f),hAPP(X_e,fun(X_f,product_prod(X_e,X_f)),product_Pair(X_e,X_f),$f10(X_a,X_b,X_c,X_d,X_e,X_f,X_2,P_1)),$f9(X_a,X_b,X_c,X_d,X_e,X_f,X_2,P_1))))))))|hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),bool,P_1,X_2)). % 3.67/3.81 0 [] ti(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),Y)=hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),$f20(X_a,X_b,X_c,X_d,X_e,X_f,Y)),hAPP(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),product_prod(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),$f19(X_a,X_b,X_c,X_d,X_e,X_f,Y)),hAPP(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f))),hAPP(X_c,fun(product_prod(X_d,product_prod(X_e,X_f)),product_prod(X_c,product_prod(X_d,product_prod(X_e,X_f)))),product_Pair(X_c,product_prod(X_d,product_prod(X_e,X_f))),$f18(X_a,X_b,X_c,X_d,X_e,X_f,Y)),hAPP(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f)),hAPP(X_d,fun(product_prod(X_e,X_f),product_prod(X_d,product_prod(X_e,X_f))),product_Pair(X_d,product_prod(X_e,X_f)),$f17(X_a,X_b,X_c,X_d,X_e,X_f,Y)),hAPP(X_f,product_prod(X_e,X_f),hAPP(X_e,fun(X_f,product_prod(X_e,X_f)),product_Pair(X_e,X_f),$f16(X_a,X_b,X_c,X_d,X_e,X_f,Y)),$f15(X_a,X_b,X_c,X_d,X_e,X_f,Y)))))). % 3.67/3.81 0 [] ti(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),Y)=hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),$f25(X_a,X_b,X_c,X_d,X_e,Y)),hAPP(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,X_e))),$f24(X_a,X_b,X_c,X_d,X_e,Y)),hAPP(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e)),hAPP(X_c,fun(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e))),product_Pair(X_c,product_prod(X_d,X_e)),$f23(X_a,X_b,X_c,X_d,X_e,Y)),hAPP(X_e,product_prod(X_d,X_e),hAPP(X_d,fun(X_e,product_prod(X_d,X_e)),product_Pair(X_d,X_e),$f22(X_a,X_b,X_c,X_d,X_e,Y)),$f21(X_a,X_b,X_c,X_d,X_e,Y))))). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),bool,P_1,hAPP(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),$f30(X_a,X_b,X_c,X_d,X_e,X_2,P_1)),hAPP(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e))),hAPP(X_b,fun(product_prod(X_c,product_prod(X_d,X_e)),product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),product_Pair(X_b,product_prod(X_c,product_prod(X_d,X_e))),$f29(X_a,X_b,X_c,X_d,X_e,X_2,P_1)),hAPP(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e)),hAPP(X_c,fun(product_prod(X_d,X_e),product_prod(X_c,product_prod(X_d,X_e))),product_Pair(X_c,product_prod(X_d,X_e)),$f28(X_a,X_b,X_c,X_d,X_e,X_2,P_1)),hAPP(X_e,product_prod(X_d,X_e),hAPP(X_d,fun(X_e,product_prod(X_d,X_e)),product_Pair(X_d,X_e),$f27(X_a,X_b,X_c,X_d,X_e,X_2,P_1)),$f26(X_a,X_b,X_c,X_d,X_e,X_2,P_1)))))))|hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,product_prod(X_d,X_e)))),bool,P_1,X_2)). % 3.67/3.81 0 [] ti(product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),Y)=hAPP(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d)))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,X_d))),$f34(X_a,X_b,X_c,X_d,Y)),hAPP(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d)),hAPP(X_b,fun(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d))),product_Pair(X_b,product_prod(X_c,X_d)),$f33(X_a,X_b,X_c,X_d,Y)),hAPP(X_d,product_prod(X_c,X_d),hAPP(X_c,fun(X_d,product_prod(X_c,X_d)),product_Pair(X_c,X_d),$f32(X_a,X_b,X_c,X_d,Y)),$f31(X_a,X_b,X_c,X_d,Y)))). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),bool,P_1,hAPP(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),hAPP(X_a,fun(product_prod(X_b,product_prod(X_c,X_d)),product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d)))),product_Pair(X_a,product_prod(X_b,product_prod(X_c,X_d))),$f38(X_a,X_b,X_c,X_d,X_2,P_1)),hAPP(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d)),hAPP(X_b,fun(product_prod(X_c,X_d),product_prod(X_b,product_prod(X_c,X_d))),product_Pair(X_b,product_prod(X_c,X_d)),$f37(X_a,X_b,X_c,X_d,X_2,P_1)),hAPP(X_d,product_prod(X_c,X_d),hAPP(X_c,fun(X_d,product_prod(X_c,X_d)),product_Pair(X_c,X_d),$f36(X_a,X_b,X_c,X_d,X_2,P_1)),$f35(X_a,X_b,X_c,X_d,X_2,P_1))))))|hBOOL(hAPP(product_prod(X_a,product_prod(X_b,product_prod(X_c,X_d))),bool,P_1,X_2)). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,product_prod(X_b,X_c)),bool,P_1,hAPP(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c)),hAPP(X_a,fun(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c))),product_Pair(X_a,product_prod(X_b,X_c)),$f41(X_a,X_b,X_c,X_2,P_1)),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),$f40(X_a,X_b,X_c,X_2,P_1)),$f39(X_a,X_b,X_c,X_2,P_1)))))|hBOOL(hAPP(product_prod(X_a,product_prod(X_b,X_c)),bool,P_1,X_2)). % 3.67/3.81 0 [] ti(product_prod(X_a,product_prod(X_b,X_c)),Y)=hAPP(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c)),hAPP(X_a,fun(product_prod(X_b,X_c),product_prod(X_a,product_prod(X_b,X_c))),product_Pair(X_a,product_prod(X_b,X_c)),$f44(X_a,X_b,X_c,Y)),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),$f43(X_a,X_b,X_c,Y)),$f42(X_a,X_b,X_c,Y))). % 3.67/3.81 0 [] ti(product_prod(X_a,X_b),Y)=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),$f46(X_a,X_b,Y)),$f45(X_a,X_b,Y)). % 3.67/3.81 0 [] hAPP(X_a,X_b,F,$f47(X_a,X_b,F,G))!=hAPP(X_a,X_b,G,$f47(X_a,X_b,F,G))|ti(fun(X_a,X_b),F)=ti(fun(X_a,X_b),G). % 3.67/3.81 0 [] ti(product_prod(X_a,X_b),P)=hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),$f49(X_a,X_b,P)),$f48(X_a,X_b,P)). % 3.67/3.81 0 [] hAPP(product_prod(X_b,X_c),X_a,hAPP(fun(X_b,fun(X_c,X_a)),fun(product_prod(X_b,X_c),X_a),produc1605651328_split(X_b,X_c,X_a),C),hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),Aa),Ba))=hAPP(X_c,X_a,hAPP(X_b,fun(X_c,X_a),C,Aa),Ba). % 3.67/3.81 0 [] -hBOOL(hAPP(product_prod(X_a,X_b),bool,F,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba)))|hBOOL(hAPP(X_b,bool,hAPP(X_a,fun(X_b,bool),hAPP(fun(product_prod(X_a,X_b),bool),fun(X_a,fun(X_b,bool)),product_curry(X_a,X_b,bool),F),Aa),Ba)). % 3.67/3.81 0 [] -hBOOL(hAPP(X_b,bool,hAPP(X_a,fun(X_b,bool),hAPP(fun(product_prod(X_a,X_b),bool),fun(X_a,fun(X_b,bool)),product_curry(X_a,X_b,bool),F),Aa),Ba))|hBOOL(hAPP(product_prod(X_a,X_b),bool,F,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba))). % 3.67/3.81 0 [] -hBOOL(hAPP(X_b,bool,hAPP(X_a,fun(X_b,bool),hAPP(fun(product_prod(X_a,X_b),bool),fun(X_a,fun(X_b,bool)),product_curry(X_a,X_b,bool),F),Aa),Ba))|hBOOL(hAPP(product_prod(X_a,X_b),bool,F,hAPP(X_b,product_prod(X_a,X_b),hAPP(X_a,fun(X_b,product_prod(X_a,X_b)),product_Pair(X_a,X_b),Aa),Ba))). % 3.67/3.81 0 [] hAPP(X_c,X_a,hAPP(X_b,fun(X_c,X_a),hAPP(fun(product_prod(X_b,X_c),X_a),fun(X_b,fun(X_c,X_a)),product_curry(X_b,X_c,X_a),F),Aa),Ba)=hAPP(product_prod(X_b,X_c),X_a,F,hAPP(X_c,product_prod(X_b,X_c),hAPP(X_b,fun(X_c,product_prod(X_b,X_c)),product_Pair(X_b,X_c),Aa),Ba)). % 3.67/3.81 0 [] -ordered_ring(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)),E)),C)),D_1)). % 3.67/3.81 0 [] -ordered_ring(X_a)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)))| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)),E)),C)),D_1)). % 3.67/3.81 0 [] -ordered_ring(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Ba),Aa)),E)),D_1))). % 3.67/3.81 0 [] -ordered_ring(X_a)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Aa),E)),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),Ba),E)),D_1)))| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),times_times(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Ba),Aa)),E)),D_1))). % 3.67/3.81 0 [] -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),I),J))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K),I)),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K),J))). % 3.67/3.81 0 [] -ordered_ab_group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C),D_1)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C),D_1)). % 3.67/3.81 0 [] -ordered_ab_group_add(X_a)|hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),Aa),Ba)!=hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),minus_minus(X_a),C),D_1)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba))| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C),D_1)). % 3.67/3.81 0 [] -ordere236663937imp_le(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),B)))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B)). % 3.67/3.81 0 [] -ordere236663937imp_le(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1)))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B)). % 3.67/3.81 0 [] -ordere779506340up_add(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),C_1),D))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),D))). % 3.67/3.81 0 [] -ordere779506340up_add(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),A_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C_1),B))). % 3.67/3.81 0 [] -ordere779506340up_add(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),A_1),B))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),A_1),C_1)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),B),C_1))). % 3.67/3.81 0 [] -ordere236663937imp_le(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Aa)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Ba)))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba)). % 3.67/3.81 0 [] -ordere236663937imp_le(X_a)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Aa)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),C),Ba)))| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba)). % 3.67/3.81 0 [] -ordere236663937imp_le(X_a)| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Ba),C)))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba)). % 3.67/3.81 0 [] -ordere236663937imp_le(X_a)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Aa),C)),hAPP(X_a,X_a,hAPP(X_a,fun(X_a,X_a),plus_plus(X_a),Ba),C)))| -hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Aa),Ba)). % 3.67/3.81 0 [] -preorder(X_a)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),X_1),X_1)). % 3.67/3.81 0 [] -linorder(X_a)|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),X_1),Y))|hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),ord_less_e_q(X_a),Y),X_1)). % 3.67/3.81 0 [] hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),W),W)). % 3.67/3.81 0 [] hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),Z),W))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),W),Z)). % 3.67/3.81 0 [] -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),I),J))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),J),K))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),I),K)). % 3.67/3.81 0 [] -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),Z),W))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),W),Z))|Z=W. % 3.67/3.81 0 [] -ord(X_b)| -hBOOL(hAPP(fun(X_a,X_b),bool,hAPP(fun(X_a,X_b),fun(fun(X_a,X_b),bool),ord_less_e_q(fun(X_a,X_b)),F),G))|hBOOL(hAPP(X_b,bool,hAPP(X_b,fun(X_b,bool),ord_less_e_q(X_b),hAPP(X_a,X_b,F,X)),hAPP(X_a,X_b,G,X))). % 3.67/3.81 0 [] -ord(X_b)|hBOOL(hAPP(fun(X_a,X_b),bool,hAPP(fun(X_a,X_b),fun(fun(X_a,X_b),bool),ord_less_e_q(fun(X_a,X_b)),F),G))| -hBOOL(hAPP(X_b,bool,hAPP(X_b,fun(X_b,bool),ord_less_e_q(X_b),hAPP(X_a,X_b,F,$f50(X_a,X_b,F,G))),hAPP(X_a,X_b,G,$f50(X_a,X_b,F,G)))). % 3.67/3.81 0 [] -preorder(T_1)|preorder(fun(T_2,T_1)). % 3.67/3.81 0 [] -ord(T_1)|ord(fun(T_2,T_1)). % 3.67/3.81 0 [] -minus(T_1)|minus(fun(T_2,T_1)). % 3.67/3.81 0 [] semiri456707255roduct(int). % 3.67/3.81 0 [] ordere236663937imp_le(int). % 3.67/3.81 0 [] ordere779506340up_add(int). % 3.67/3.81 0 [] cancel146912293up_add(int). % 3.67/3.81 0 [] ordered_ab_group_add(int). % 3.67/3.81 0 [] cancel_semigroup_add(int). % 3.67/3.81 0 [] ab_semigroup_mult(int). % 3.67/3.81 0 [] ab_semigroup_add(int). % 3.67/3.81 0 [] comm_semiring_1(int). % 3.67/3.81 0 [] comm_semiring(int). % 3.67/3.81 0 [] ab_group_add(int). % 3.67/3.81 0 [] ordered_ring(int). % 3.67/3.81 0 [] preorder(int). % 3.67/3.81 0 [] linorder(int). % 3.67/3.81 0 [] group_add(int). % 3.67/3.81 0 [] semiring(int). % 3.67/3.81 0 [] ord(int). % 3.67/3.81 0 [] minus(int). % 3.67/3.81 0 [] ring(int). % 3.67/3.81 0 [] preorder(bool). % 3.67/3.81 0 [] ord(bool). % 3.67/3.81 0 [] minus(bool). % 3.67/3.81 0 [] ti(T,ti(T,A))=ti(T,A). % 3.67/3.81 0 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),a),b))),hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),p),q)))!=hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),a),p)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),b),q))),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),a),q)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),b),p)))). % 3.67/3.82 end_of_list. % 3.67/3.82 % 3.67/3.82 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 3.67/3.82 % 3.67/3.82 This ia a non-Horn set with equality. The strategy will be % 3.67/3.82 Knuth-Bendix, ordered hyper_res, factoring, and unit % 3.67/3.82 deletion, with positive clauses in sos and nonpositive % 3.67/3.82 clauses in usable. % 3.67/3.82 % 3.67/3.82 dependent: set(knuth_bendix). % 3.67/3.82 dependent: set(anl_eq). % 3.67/3.82 dependent: set(para_from). % 3.67/3.82 dependent: set(para_into). % 3.67/3.82 dependent: clear(para_from_right). % 3.67/3.82 dependent: clear(para_into_right). % 3.67/3.82 dependent: set(para_from_vars). % 3.67/3.82 dependent: set(eq_units_both_ways). % 3.67/3.82 dependent: set(dynamic_demod_all). % 3.67/3.82 dependent: set(dynamic_demod). % 3.67/3.82 dependent: set(order_eq). % 3.67/3.82 dependent: set(back_demod). % 3.67/3.82 dependent: set(lrpo). % 3.67/3.82 dependent: set(hyper_res). % 3.67/3.82 dependent: set(unit_deletion). % 3.67/3.82 dependent: set(factor). % 3.67/3.82 % 3.67/3.82 ------------> process usable: % 3.67/3.82 ** KEPT (pick-wt=13): 1 [] -minus(A)|ti(fun(A,fun(A,A)),minus_minus(A))=minus_minus(A). % 3.67/3.82 ** KEPT (pick-wt=13): 2 [] -ab_semigroup_add(A)|ti(fun(A,fun(A,A)),plus_plus(A))=plus_plus(A). % 3.67/3.82 ** KEPT (pick-wt=13): 3 [] -cancel_semigroup_add(A)|ti(fun(A,fun(A,A)),plus_plus(A))=plus_plus(A). % 3.67/3.82 ** KEPT (pick-wt=13): 4 [] -semiring(A)|ti(fun(A,fun(A,A)),times_times(A))=times_times(A). % 3.67/3.82 ** KEPT (pick-wt=13): 5 [] -ab_semigroup_mult(A)|ti(fun(A,fun(A,A)),times_times(A))=times_times(A). % 3.67/3.82 ** KEPT (pick-wt=13): 6 [] -ord(A)|ti(fun(A,fun(A,bool)),ord_less_e_q(A))=ord_less_e_q(A). % 3.67/3.82 ** KEPT (pick-wt=6): 7 [] -hBOOL(ti(bool,A))|hBOOL(A). % 3.67/3.82 ** KEPT (pick-wt=6): 8 [] hBOOL(ti(bool,A))| -hBOOL(A). % 3.67/3.82 ** KEPT (pick-wt=93): 10 [copy,9,flip.2] -ring(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),C),D))),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),E)),D))=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),D)). % 3.67/3.82 ** KEPT (pick-wt=137): 12 [copy,11,flip.2] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),D),E))),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)),E))),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),D),E)))=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),E)). % 3.67/3.82 ** KEPT (pick-wt=87): 13 [] -ring(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)|ti(A,D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),E),B)),C)),F). % 3.67/3.82 ** KEPT (pick-wt=87): 14 [] -ring(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)|ti(A,D)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),E),B)),C)),F). % 3.67/3.82 ** KEPT (pick-wt=87): 15 [] -ring(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),E)),C)),D)=ti(A,F). % 3.67/3.82 ** KEPT (pick-wt=87): 16 [] -ring(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),E)),C)),D)!=ti(A,F). % 3.67/3.82 ** KEPT (pick-wt=33): 17 [] -hBOOL(hAPP(int,bool,twoSqu33214720sum2sq,A))|hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),$f2(A)),$f1(A)))=A. % 3.67/3.82 ** KEPT (pick-wt=31): 18 [] hBOOL(hAPP(int,bool,twoSqu33214720sum2sq,A))|hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),B),C))!=A. % 3.67/3.82 ** KEPT (pick-wt=28): 19 [] hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A),B)!=C|A=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),C),B). % 3.67/3.82 ** KEPT (pick-wt=29): 20 [] -group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)),C)=ti(A,B). % 3.67/3.82 ** KEPT (pick-wt=49): 21 [] -ab_semigroup_mult(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.67/3.82 ** KEPT (pick-wt=34): 22 [] -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)|ti(A,B)=ti(A,D). % 3.67/3.82 ** KEPT (pick-wt=34): 23 [] -cancel146912293up_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)|ti(A,C)=ti(A,D). % 3.67/3.82 ** KEPT (pick-wt=34): 24 [] -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)|ti(A,C)=ti(A,D). % 3.67/3.82 Following clause subsumed by 22 during input processing: 0 [] -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)|ti(A,B)=ti(A,D). % 3.67/3.82 ** KEPT (pick-wt=34): 25 [] -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)|ti(A,B)!=ti(A,D). % 3.67/3.82 Following clause subsumed by 24 during input processing: 0 [] -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)|ti(A,C)=ti(A,D). % 3.67/3.82 ** KEPT (pick-wt=34): 26 [] -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)|ti(A,C)!=ti(A,D). % 3.67/3.82 ** KEPT (pick-wt=49): 27 [] -ab_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)). % 3.67/3.82 ** KEPT (pick-wt=41): 28 [] -ab_group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),D),E)|ti(A,B)!=ti(A,C)|ti(A,D)=ti(A,E). % 3.67/3.82 ** KEPT (pick-wt=41): 29 [] -ab_group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),D),E)|ti(A,B)=ti(A,C)|ti(A,D)!=ti(A,E). % 3.67/3.82 ** KEPT (pick-wt=82): 31 [copy,30,flip.2] -semiring(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)),E)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)),E)). % 3.67/3.82 ** KEPT (pick-wt=60): 32 [] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.67/3.82 Following clause subsumed by 32 during input processing: 0 [] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.67/3.82 ** KEPT (pick-wt=60): 33 [] -comm_semiring(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=60): 35 [copy,34,flip.2] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)). % 3.74/3.82 Following clause subsumed by 35 during input processing: 0 [flip.2] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=60): 36 [] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 Following clause subsumed by 36 during input processing: 0 [] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=60): 38 [copy,37,flip.2] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),C),D)). % 3.74/3.82 Following clause subsumed by 38 during input processing: 0 [flip.2] -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=71): 39 [] -ab_group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),C),E)). % 3.74/3.82 ** KEPT (pick-wt=29): 40 [] -group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),C)=ti(A,B). % 3.74/3.82 ** KEPT (pick-wt=85): 41 [] -semiri456707255roduct(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),C))|ti(A,B)=ti(A,D)|ti(A,C)=ti(A,E). % 3.74/3.82 ** KEPT (pick-wt=78): 42 [] -semiri456707255roduct(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),C))|ti(A,B)!=ti(A,D). % 3.74/3.82 ** KEPT (pick-wt=78): 43 [] -semiri456707255roduct(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),C))|ti(A,C)!=ti(A,E). % 3.74/3.82 ** KEPT (pick-wt=60): 44 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),C))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)),C). % 3.74/3.82 ** KEPT (pick-wt=60): 45 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 Following clause subsumed by 41 during input processing: 0 [] -semiri456707255roduct(A)|ti(A,B)=ti(A,C)|ti(A,D)=ti(A,E)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),E))!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 Following clause subsumed by 42 during input processing: 0 [] -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),E))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 Following clause subsumed by 43 during input processing: 0 [] -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),B)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),B)). % 3.74/3.82 ** KEPT (pick-wt=60): 47 [copy,46,flip.2] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=51): 48 [] -minus(A)|hAPP(B,A,hAPP(fun(B,A),fun(B,A),hAPP(fun(B,A),fun(fun(B,A),fun(B,A)),minus_minus(fun(B,A)),C),D),E)=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(B,A,C,E)),hAPP(B,A,D,E)). % 3.74/3.82 Following clause subsumed by 48 during input processing: 0 [] -minus(A)|hAPP(B,A,hAPP(fun(B,A),fun(B,A),hAPP(fun(B,A),fun(fun(B,A),fun(B,A)),minus_minus(fun(B,A)),C),D),E)=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(B,A,C,E)),hAPP(B,A,D,E)). % 3.74/3.82 ** KEPT (pick-wt=42): 49 [] hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)!=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(B,C)=ti(B,E). % 3.74/3.82 ** KEPT (pick-wt=42): 50 [] hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)!=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(A,D)=ti(A,F). % 3.74/3.82 Following clause subsumed by 49 during input processing: 0 [] hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)!=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(B,C)=ti(B,E). % 3.74/3.82 Following clause subsumed by 50 during input processing: 0 [] hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)!=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(A,D)=ti(A,F). % 3.74/3.82 ** KEPT (pick-wt=49): 51 [] hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(B,C)!=ti(B,E)|ti(A,D)!=ti(A,F). % 3.74/3.82 ** KEPT (pick-wt=18): 52 [] -ab_sem1668676832m_mult(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),B)=ti(A,B). % 3.74/3.82 Following clause subsumed by 52 during input processing: 0 [] -ab_sem1668676832m_mult(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),B)=ti(A,B). % 3.74/3.82 ** KEPT (pick-wt=27): 53 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),B). % 3.74/3.82 ** KEPT (pick-wt=38): 54 [] -ab_sem1668676832m_mult(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C). % 3.74/3.82 ** KEPT (pick-wt=49): 55 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)). % 3.74/3.82 ** KEPT (pick-wt=49): 57 [copy,56,flip.2] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 Following clause subsumed by 57 during input processing: 0 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=49): 58 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),C). % 3.74/3.82 Following clause subsumed by 57 during input processing: 0 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))). % 3.74/3.82 Following clause subsumed by 55 during input processing: 0 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),E)). % 3.74/3.82 ** KEPT (pick-wt=71): 59 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),E)). % 3.74/3.82 ** KEPT (pick-wt=27): 60 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),B). % 3.74/3.82 ** KEPT (pick-wt=49): 61 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)). % 3.74/3.82 ** KEPT (pick-wt=49): 63 [copy,62,flip.2] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)). % 3.74/3.82 Following clause subsumed by 63 during input processing: 0 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=49): 64 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)),C). % 3.74/3.82 ** KEPT (pick-wt=71): 65 [] -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),E)). % 3.74/3.82 ** KEPT (pick-wt=35): 66 [] -hBOOL(hAPP(product_prod(A,B),bool,C,$f3(A,B,C)))|hBOOL(hAPP(product_prod(A,B),bool,C,hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),D),E))). % 3.74/3.82 ** KEPT (pick-wt=38): 67 [] hBOOL(hAPP(product_prod(A,B),bool,C,D))| -hBOOL(hAPP(product_prod(A,B),bool,C,hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),$f5(A,B,C)),$f4(A,B,C)))). % 3.74/3.82 ** KEPT (pick-wt=38): 68 [] -hBOOL(hAPP(product_prod(A,B),bool,C,D))|hBOOL(hAPP(product_prod(A,B),bool,C,hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),$f7(A,B,C)),$f6(A,B,C)))). % 3.74/3.82 ** KEPT (pick-wt=35): 69 [] hBOOL(hAPP(product_prod(A,B),bool,C,$f8(A,B,C)))| -hBOOL(hAPP(product_prod(A,B),bool,C,hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),D),E))). % 3.74/3.82 ** KEPT (pick-wt=260): 70 [] -hBOOL(hAPP(product_prod(A,product_prod(B,product_prod(C,product_prod(D,product_prod(E,F))))),bool,G,hAPP(product_prod(B,product_prod(C,product_prod(D,product_prod(E,F)))),product_prod(A,product_prod(B,product_prod(C,product_prod(D,product_prod(E,F))))),hAPP(A,fun(product_prod(B,product_prod(C,product_prod(D,product_prod(E,F)))),product_prod(A,product_prod(B,product_prod(C,product_prod(D,product_prod(E,F)))))),product_Pair(A,product_prod(B,product_prod(C,product_prod(D,product_prod(E,F))))),$f14(A,B,C,D,E,F,H,G)),hAPP(product_prod(C,product_prod(D,product_prod(E,F))),product_prod(B,product_prod(C,product_prod(D,product_prod(E,F)))),hAPP(B,fun(product_prod(C,product_prod(D,product_prod(E,F))),product_prod(B,product_prod(C,product_prod(D,product_prod(E,F))))),product_Pair(B,product_prod(C,product_prod(D,product_prod(E,F)))),$f13(A,B,C,D,E,F,H,G)),hAPP(product_prod(D,product_prod(E,F)),product_prod(C,product_prod(D,product_prod(E,F))),hAPP(C,fun(product_prod(D,product_prod(E,F)),product_prod(C,product_prod(D,product_prod(E,F)))),product_Pair(C,product_prod(D,product_prod(E,F))),$f12(A,B,C,D,E,F,H,G)),hAPP(product_prod(E,F),product_prod(D,product_prod(E,F)),hAPP(D,fun(product_prod(E,F),product_prod(D,product_prod(E,F))),product_Pair(D,product_prod(E,F)),$f11(A,B,C,D,E,F,H,G)),hAPP(F,product_prod(E,F),hAPP(E,fun(F,product_prod(E,F)),product_Pair(E,F),$f10(A,B,C,D,E,F,H,G)),$f9(A,B,C,D,E,F,H,G))))))))|hBOOL(hAPP(product_prod(A,product_prod(B,product_prod(C,product_prod(D,product_prod(E,F))))),bool,G,H)). % 3.74/3.82 ** KEPT (pick-wt=187): 71 [] -hBOOL(hAPP(product_prod(A,product_prod(B,product_prod(C,product_prod(D,E)))),bool,F,hAPP(product_prod(B,product_prod(C,product_prod(D,E))),product_prod(A,product_prod(B,product_prod(C,product_prod(D,E)))),hAPP(A,fun(product_prod(B,product_prod(C,product_prod(D,E))),product_prod(A,product_prod(B,product_prod(C,product_prod(D,E))))),product_Pair(A,product_prod(B,product_prod(C,product_prod(D,E)))),$f30(A,B,C,D,E,G,F)),hAPP(product_prod(C,product_prod(D,E)),product_prod(B,product_prod(C,product_prod(D,E))),hAPP(B,fun(product_prod(C,product_prod(D,E)),product_prod(B,product_prod(C,product_prod(D,E)))),product_Pair(B,product_prod(C,product_prod(D,E))),$f29(A,B,C,D,E,G,F)),hAPP(product_prod(D,E),product_prod(C,product_prod(D,E)),hAPP(C,fun(product_prod(D,E),product_prod(C,product_prod(D,E))),product_Pair(C,product_prod(D,E)),$f28(A,B,C,D,E,G,F)),hAPP(E,product_prod(D,E),hAPP(D,fun(E,product_prod(D,E)),product_Pair(D,E),$f27(A,B,C,D,E,G,F)),$f26(A,B,C,D,E,G,F)))))))|hBOOL(hAPP(product_prod(A,product_prod(B,product_prod(C,product_prod(D,E)))),bool,F,G)). % 3.74/3.82 ** KEPT (pick-wt=126): 72 [] -hBOOL(hAPP(product_prod(A,product_prod(B,product_prod(C,D))),bool,E,hAPP(product_prod(B,product_prod(C,D)),product_prod(A,product_prod(B,product_prod(C,D))),hAPP(A,fun(product_prod(B,product_prod(C,D)),product_prod(A,product_prod(B,product_prod(C,D)))),product_Pair(A,product_prod(B,product_prod(C,D))),$f38(A,B,C,D,F,E)),hAPP(product_prod(C,D),product_prod(B,product_prod(C,D)),hAPP(B,fun(product_prod(C,D),product_prod(B,product_prod(C,D))),product_Pair(B,product_prod(C,D)),$f37(A,B,C,D,F,E)),hAPP(D,product_prod(C,D),hAPP(C,fun(D,product_prod(C,D)),product_Pair(C,D),$f36(A,B,C,D,F,E)),$f35(A,B,C,D,F,E))))))|hBOOL(hAPP(product_prod(A,product_prod(B,product_prod(C,D))),bool,E,F)). % 3.74/3.82 ** KEPT (pick-wt=77): 73 [] -hBOOL(hAPP(product_prod(A,product_prod(B,C)),bool,D,hAPP(product_prod(B,C),product_prod(A,product_prod(B,C)),hAPP(A,fun(product_prod(B,C),product_prod(A,product_prod(B,C))),product_Pair(A,product_prod(B,C)),$f41(A,B,C,E,D)),hAPP(C,product_prod(B,C),hAPP(B,fun(C,product_prod(B,C)),product_Pair(B,C),$f40(A,B,C,E,D)),$f39(A,B,C,E,D)))))|hBOOL(hAPP(product_prod(A,product_prod(B,C)),bool,D,E)). % 3.74/3.82 ** KEPT (pick-wt=30): 74 [] hAPP(A,B,C,$f47(A,B,C,D))!=hAPP(A,B,D,$f47(A,B,C,D))|ti(fun(A,B),C)=ti(fun(A,B),D). % 3.74/3.82 ** KEPT (pick-wt=51): 75 [] -hBOOL(hAPP(product_prod(A,B),bool,C,hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),D),E)))|hBOOL(hAPP(B,bool,hAPP(A,fun(B,bool),hAPP(fun(product_prod(A,B),bool),fun(A,fun(B,bool)),product_curry(A,B,bool),C),D),E)). % 3.74/3.82 ** KEPT (pick-wt=51): 76 [] -hBOOL(hAPP(A,bool,hAPP(B,fun(A,bool),hAPP(fun(product_prod(B,A),bool),fun(B,fun(A,bool)),product_curry(B,A,bool),C),D),E))|hBOOL(hAPP(product_prod(B,A),bool,C,hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),D),E))). % 3.74/3.82 Following clause subsumed by 76 during input processing: 0 [] -hBOOL(hAPP(A,bool,hAPP(B,fun(A,bool),hAPP(fun(product_prod(B,A),bool),fun(B,fun(A,bool)),product_curry(B,A,bool),C),D),E))|hBOOL(hAPP(product_prod(B,A),bool,C,hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),D),E))). % 3.74/3.82 ** KEPT (pick-wt=105): 77 [] -ordered_ring(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),E)),C)),D)),F)). % 3.74/3.82 ** KEPT (pick-wt=105): 78 [] -ordered_ring(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),E)),C)),D)),F)). % 3.74/3.82 ** KEPT (pick-wt=105): 79 [] -ordered_ring(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),D),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),E),B)),C)),F))). % 3.74/3.82 ** KEPT (pick-wt=105): 80 [] -ordered_ring(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C)),F)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),D),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),E),B)),C)),F))). % 3.74/3.82 ** KEPT (pick-wt=48): 81 [] -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),A),B))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),C),A)),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),C),B))). % 3.74/3.82 ** KEPT (pick-wt=53): 82 [] -ordered_ab_group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),D),E)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),D),E)). % 3.74/3.82 ** KEPT (pick-wt=53): 83 [] -ordered_ab_group_add(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),D),E)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),D),E)). % 3.74/3.82 ** KEPT (pick-wt=50): 84 [] -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=50): 85 [] -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),D)). % 3.74/3.82 ** KEPT (pick-wt=63): 86 [] -ordere779506340up_add(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),C))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),D),E))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),E))). % 3.74/3.82 ** KEPT (pick-wt=50): 87 [] -ordere779506340up_add(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),B)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C))). % 3.74/3.82 ** KEPT (pick-wt=50): 88 [] -ordere779506340up_add(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D))). % 3.74/3.82 Following clause subsumed by 84 during input processing: 0 [] -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),C),D)). % 3.74/3.82 ** KEPT (pick-wt=50): 89 [] -ordere236663937imp_le(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),C),D)). % 3.74/3.82 Following clause subsumed by 85 during input processing: 0 [] -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),D)). % 3.74/3.82 ** KEPT (pick-wt=50): 90 [] -ordere236663937imp_le(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),D)). % 3.74/3.82 ** KEPT (pick-wt=15): 91 [] -preorder(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),B)). % 3.74/3.82 ** KEPT (pick-wt=28): 92 [] -linorder(A)|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),B),C))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),C),B)). % 3.74/3.82 ** KEPT (pick-wt=39): 93 [] -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),A),B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),B),C))|hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),A),C)). % 3.74/3.82 ** KEPT (pick-wt=29): 94 [] -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),A),B))| -hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_e_q(int),B),A))|A=B. % 3.74/3.82 ** KEPT (pick-wt=44): 95 [] -ord(A)| -hBOOL(hAPP(fun(B,A),bool,hAPP(fun(B,A),fun(fun(B,A),bool),ord_less_e_q(fun(B,A)),C),D))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(B,A,C,E)),hAPP(B,A,D,E))). % 3.74/3.82 ** KEPT (pick-wt=52): 96 [] -ord(A)|hBOOL(hAPP(fun(B,A),bool,hAPP(fun(B,A),fun(fun(B,A),bool),ord_less_e_q(fun(B,A)),C),D))| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_e_q(A),hAPP(B,A,C,$f50(B,A,C,D))),hAPP(B,A,D,$f50(B,A,C,D)))). % 3.74/3.82 ** KEPT (pick-wt=6): 97 [] -preorder(A)|preorder(fun(B,A)). % 3.74/3.82 ** KEPT (pick-wt=6): 98 [] -ord(A)|ord(fun(B,A)). % 3.74/3.82 ** KEPT (pick-wt=6): 99 [] -minus(A)|minus(fun(B,A)). % 3.74/3.82 ** KEPT (pick-wt=146): 101 [copy,100,flip.1] hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),a),p)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),b),q))),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),a),q)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),b),p))))!=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),a),b))),hAPP(product_prod(int,int),int,twoSqu930276342sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),p),q))). % 3.74/3.82 % 3.74/3.82 ------------> process sos: % 3.74/3.82 ** KEPT (pick-wt=3): 107 [] A=A. % 3.74/3.82 ** KEPT (pick-wt=7): 108 [] ti(A,undefined(A))=undefined(A). % 3.74/3.82 ---> New Demodulator: 109 [new_demod,108] ti(A,undefined(A))=undefined(A). % 3.74/3.82 ** KEPT (pick-wt=15): 110 [] ti(fun(A,fun(B,product_prod(A,B))),product_Pair(A,B))=product_Pair(A,B). % 3.74/3.82 ---> New Demodulator: 111 [new_demod,110] ti(fun(A,fun(B,product_prod(A,B))),product_Pair(A,B))=product_Pair(A,B). % 3.74/3.82 ** KEPT (pick-wt=21): 112 [] ti(fun(fun(product_prod(A,B),C),fun(A,fun(B,C))),product_curry(A,B,C))=product_curry(A,B,C). % 3.74/3.82 ---> New Demodulator: 113 [new_demod,112] ti(fun(fun(product_prod(A,B),C),fun(A,fun(B,C))),product_curry(A,B,C))=product_curry(A,B,C). % 3.74/3.82 ** KEPT (pick-wt=21): 114 [] ti(fun(fun(A,fun(B,C)),fun(product_prod(A,B),C)),produc1605651328_split(A,B,C))=produc1605651328_split(A,B,C). % 3.74/3.82 ---> New Demodulator: 115 [new_demod,114] ti(fun(fun(A,fun(B,C)),fun(product_prod(A,B),C)),produc1605651328_split(A,B,C))=produc1605651328_split(A,B,C). % 3.74/3.82 ** KEPT (pick-wt=21): 116 [] ti(fun(fun(A,fun(B,C)),fun(product_prod(A,B),C)),product_prod_rec(A,B,C))=product_prod_rec(A,B,C). % 3.74/3.82 ---> New Demodulator: 117 [new_demod,116] ti(fun(fun(A,fun(B,C)),fun(product_prod(A,B),C)),product_prod_rec(A,B,C))=product_prod_rec(A,B,C). % 3.74/3.82 ** KEPT (pick-wt=7): 118 [] ti(fun(int,bool),twoSqu33214720sum2sq)=twoSqu33214720sum2sq. % 3.74/3.82 ---> New Demodulator: 119 [new_demod,118] ti(fun(int,bool),twoSqu33214720sum2sq)=twoSqu33214720sum2sq. % 3.74/3.82 ** KEPT (pick-wt=9): 120 [] ti(fun(product_prod(int,int),int),twoSqu930276342sum2sq)=twoSqu930276342sum2sq. % 3.74/3.82 ---> New Demodulator: 121 [new_demod,120] ti(fun(product_prod(int,int),int),twoSqu930276342sum2sq)=twoSqu930276342sum2sq. % 3.74/3.82 ** KEPT (pick-wt=15): 122 [] hAPP(A,B,ti(fun(A,B),C),D)=hAPP(A,B,C,D). % 3.74/3.82 ---> New Demodulator: 123 [new_demod,122] hAPP(A,B,ti(fun(A,B),C),D)=hAPP(A,B,C,D). % 3.74/3.82 ** KEPT (pick-wt=13): 124 [] hAPP(A,B,C,ti(A,D))=hAPP(A,B,C,D). % 3.74/3.82 ---> New Demodulator: 125 [new_demod,124] hAPP(A,B,C,ti(A,D))=hAPP(A,B,C,D). % 3.74/3.82 ** KEPT (pick-wt=13): 126 [] ti(A,hAPP(B,A,C,D))=hAPP(B,A,C,D). % 3.74/3.82 ---> New Demodulator: 127 [new_demod,126] ti(A,hAPP(B,A,C,D))=hAPP(B,A,C,D). % 3.74/3.82 ** KEPT (pick-wt=5): 128 [] ti(int,a)=a. % 3.74/3.82 ---> New Demodulator: 129 [new_demod,128] ti(int,a)=a. % 3.74/3.82 ** KEPT (pick-wt=5): 130 [] ti(int,b)=b. % 3.74/3.82 ---> New Demodulator: 131 [new_demod,130] ti(int,b)=b. % 3.74/3.82 ** KEPT (pick-wt=5): 132 [] ti(int,p)=p. % 3.74/3.82 ---> New Demodulator: 133 [new_demod,132] ti(int,p)=p. % 3.74/3.82 ** KEPT (pick-wt=5): 134 [] ti(int,q)=q. % 3.74/3.82 ---> New Demodulator: 135 [new_demod,134] ti(int,q)=q. % 3.74/3.82 ** KEPT (pick-wt=168): 136 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C))),D)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),E),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),F))),G))=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),D)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),E),G))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),C),D)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),F),G)))). % 3.74/3.82 ** KEPT (pick-wt=58): 138 [copy,137,flip.1] hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C))=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),B),C)). % 3.74/3.82 ---> New Demodulator: 139 [new_demod,138] hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C))=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),B),C)). % 3.74/3.82 ** KEPT (pick-wt=58): 140 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C)). % 3.74/3.82 ** KEPT (pick-wt=58): 142 [copy,141,flip.1] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C))=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),C)). % 3.74/3.82 ---> New Demodulator: 143 [new_demod,142] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),hAPP(in % 3.74/3.83 Search stopped in tp_alloc by max_mem option. % 3.74/3.83 t,int,hAPP(int,fun(int,int),times_times(int),A),C))=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),C)). % 3.74/3.83 ** KEPT (pick-wt=58): 144 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C)). % 3.74/3.83 ** KEPT (pick-wt=47): 145 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C)). % 3.74/3.83 ---> New Demodulator: 146 [new_demod,145] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C)). % 3.74/3.83 ** KEPT (pick-wt=25): 147 [] hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),A). % 3.74/3.83 ** KEPT (pick-wt=47): 148 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),C)). % 3.74/3.83 ---> New Demodulator: 149 [new_demod,148] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),C)). % 3.74/3.83 ** KEPT (pick-wt=47): 150 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),C))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),C)). % 3.74/3.83 ** KEPT (pick-wt=25): 151 [] hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),A). % 3.74/3.83 ** KEPT (pick-wt=50): 152 [] hAPP(product_prod(A,B),C,hAPP(fun(A,fun(B,C)),fun(product_prod(A,B),C),product_prod_rec(A,B,C),D),hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),E),F))=hAPP(B,C,hAPP(A,fun(B,C),D,E),F). % 3.74/3.83 ---> New Demodulator: 153 [new_demod,152] hAPP(product_prod(A,B),C,hAPP(fun(A,fun(B,C)),fun(product_prod(A,B),C),product_prod_rec(A,B,C),D),hAPP(B,product_prod(A,B),hAPP(A,fun(B,product_prod(A,B)),product_Pair(A,B),E),F))=hAPP(B,C,hAPP(A,fun(B,C),D,E),F). % 3.74/3.83 % 3.74/3.83 Search stopped in tp_alloc by max_mem option. % 3.74/3.83 % 3.74/3.83 ============ end of search ============ % 3.74/3.83 % 3.74/3.83 -------------- statistics ------------- % 3.74/3.83 clauses given 0 % 3.74/3.83 clauses generated 6 % 3.74/3.83 clauses kept 123 % 3.74/3.83 clauses forward subsumed 20 % 3.74/3.83 clauses back subsumed 0 % 3.74/3.83 Kbytes malloced 11718 % 3.74/3.83 % 3.74/3.83 ----------- times (seconds) ----------- % 3.74/3.83 user CPU time 0.02 (0 hr, 0 min, 0 sec) % 3.74/3.83 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 3.74/3.83 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.74/3.83 % 3.74/3.83 Process 32748 finished Wed Jul 27 09:38:14 2022 % 3.74/3.83 Otter interrupted % 3.74/3.83 PROOF NOT FOUND %------------------------------------------------------------------------------