%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW478+1 : TPTP v8.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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 : Mon Jun 24 18:09:44 EDT 2024 % Result : Theorem 0.54s 0.90s % Output : CNFRefutation 0.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW478+1 : TPTP v8.2.0. Released v5.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Jun 19 08:29:24 EDT 2024 % 0.13/0.33 % CPUTime : % 0.53/0.59 start to proof:theBenchmark % 0.54/0.86 %------------------------------------------- % 0.54/0.86 % File :CSE---1.7 % 0.54/0.86 % Problem :theBenchmark % 0.54/0.86 % Transform :cnf % 0.54/0.86 % Format :tptp:raw % 0.54/0.87 % Command :java -jar mcs_scs.jar %d %s % 0.54/0.87 % 0.54/0.87 % Result :Theorem 0.070000s % 0.54/0.87 % Output :CNFRefutation 0.070000s % 0.54/0.87 %------------------------------------------- % 0.54/0.87 %------------------------------------------------------------------------------ % 0.54/0.87 % File : SWW478+1 : TPTP v8.2.0. Released v5.3.0. % 0.54/0.87 % Domain : Software Verification % 0.54/0.87 % Problem : Java type soundness line 479, 100 axioms selected % 0.54/0.87 % Version : Especial. % 0.54/0.87 % English : % 0.54/0.87 % 0.54/0.87 % Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.54/0.87 % : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe % 0.54/0.87 % Source : [Bla11] % 0.54/0.87 % Names : jinja_100_fofmg_l479 [Bla11] % 0.54/0.87 % 0.54/0.87 % Status : Theorem % 0.54/0.87 % Rating : 0.06 v8.1.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.17 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0 % 0.54/0.87 % Syntax : Number of formulae : 213 ( 92 unt; 0 def) % 0.54/0.87 % Number of atoms : 410 ( 181 equ) % 0.54/0.87 % Maximal formula atoms : 5 ( 1 avg) % 0.54/0.87 % Number of connectives : 276 ( 79 ~; 6 |; 19 &) % 0.54/0.87 % ( 48 <=>; 124 =>; 0 <=; 0 <~>) % 0.54/0.87 % Maximal formula depth : 15 ( 6 avg) % 0.54/0.87 % Maximal term depth : 10 ( 2 avg) % 0.54/0.87 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 0.54/0.87 % Number of functors : 196 ( 196 usr; 62 con; 0-5 aty) % 0.54/0.87 % Number of variables : 781 ( 771 !; 10 ?) % 0.54/0.87 % SPC : FOF_THM_RFO_SEQ % 0.54/0.87 % 0.54/0.87 % Comments : This file was generated by Isabelle (most likely Sledgehammer) % 0.54/0.87 % 2011-08-09 16:05:57 % 0.54/0.87 % : Encoded with monomorphized guards. % 0.54/0.87 %------------------------------------------------------------------------------ % 0.54/0.87 %----Explicit typings (14) % 0.54/0.87 fof(gsy_c_SmallStep_Oassigned,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(assigned(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_TypeRel_Owiden_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__,axiom, % 0.54/0.87 ! [B_1_1,B_2_1,B_3] : is_bool(widen_2090681816t_char(B_1_1,B_2_1,B_3)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_WellForm_Owf__prog_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__Stri,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(wf_pro755087577t_char(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_WellTypeRT_OWTrt,axiom, % 0.54/0.87 ! [B_1_1,B_2_1,B_3,B_4,B_5] : is_bool(wTrt(B_1_1,B_2_1,B_3,B_4,B_5)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : % 0.54/0.87 ( is_bool(B_2_1) % 0.54/0.87 => is_bool(hAPP_bool_bool(B_1_1,B_2_1)) ) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__fun_Itc__List__Olist_Itc__String__Ochar_J_Mtc__Option__Ooption,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(hAPP_f1001225811y_bool(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__fun_Itc__List__Olist_Itc__String__Ochar_J_Mtc__Option__Ooption_001,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(hAPP_f1033709212l_bool(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_Itc__List__O,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(hAPP_f61040418l_bool(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__Ochar_J_J_M,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(hAPP_P1708370145l_bool(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(hAPP_P159683425l_bool(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_hAPP_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(hAPP_P282169671l_bool(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_member_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__Ochar_J_J,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(member840932460on_val(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_member_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_,axiom, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(member763590124on_val(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 fof(gsy_c_member_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String_,hypothesis, % 0.54/0.87 ! [B_1_1,B_2_1] : is_bool(member773094996on_val(B_1_1,B_2_1)) ). % 0.54/0.87 % 0.54/0.87 %----Relevant facts (167) % 0.54/0.87 fof(fact_0_InitBlockRed_I3_J,axiom, % 0.54/0.87 hAPP_l207779698on_val(l_a,v_1) = some_val(v_2) ). % 0.54/0.87 % 0.54/0.87 fof(fact_1_InitBlockRed_I1_J,axiom, % 0.54/0.87 hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,some_val(v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a))),red(p))) ). % 0.54/0.87 % 0.54/0.87 fof(fact_2_fun__upd__triv,axiom, % 0.54/0.87 ! [F,X_1] : fun_up1149430426on_val(F,X_1,hAPP_l207779698on_val(F,X_1)) = F ). % 0.54/0.87 % 0.54/0.87 fof(fact_3_fun__upd__triv,axiom, % 0.54/0.87 ! [F,X_1] : fun_up424764369ion_ty(F,X_1,hAPP_l512744617ion_ty(F,X_1)) = F ). % 0.54/0.87 % 0.54/0.87 fof(fact_4_assms,axiom, % 0.54/0.87 hBOOL(wf_pro755087577t_char(wf_J_mdecl,p)) ). % 0.54/0.87 % 0.54/0.87 fof(fact_5_map__upd__Some__unfold,axiom, % 0.54/0.87 ! [M,A_10,B_1,X_1,Y_1] : % 0.54/0.87 ( hAPP_l207779698on_val(fun_up1149430426on_val(M,A_10,some_val(B_1)),X_1) = some_val(Y_1) % 0.54/0.87 <=> ( ( X_1 = A_10 % 0.54/0.87 & B_1 = Y_1 ) % 0.54/0.87 | ( X_1 != A_10 % 0.54/0.87 & hAPP_l207779698on_val(M,X_1) = some_val(Y_1) ) ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_6_map__upd__Some__unfold,axiom, % 0.54/0.87 ! [M,A_10,B_1,X_1,Y_1] : % 0.54/0.87 ( hAPP_l512744617ion_ty(fun_up424764369ion_ty(M,A_10,some_ty(B_1)),X_1) = some_ty(Y_1) % 0.54/0.87 <=> ( ( X_1 = A_10 % 0.54/0.87 & B_1 = Y_1 ) % 0.54/0.87 | ( X_1 != A_10 % 0.54/0.87 & hAPP_l512744617ion_ty(M,X_1) = some_ty(Y_1) ) ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_7_map__upd__triv,axiom, % 0.54/0.87 ! [T,K,X_1] : % 0.54/0.87 ( hAPP_l207779698on_val(T,K) = some_val(X_1) % 0.54/0.87 => fun_up1149430426on_val(T,K,some_val(X_1)) = T ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_8_map__upd__triv,axiom, % 0.54/0.87 ! [T,K,X_1] : % 0.54/0.87 ( hAPP_l512744617ion_ty(T,K) = some_ty(X_1) % 0.54/0.87 => fun_up424764369ion_ty(T,K,some_ty(X_1)) = T ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_9_map__upd__eqD1,axiom, % 0.54/0.87 ! [M,A_10,X_1,N,Y_1] : % 0.54/0.87 ( fun_up1149430426on_val(M,A_10,some_val(X_1)) = fun_up1149430426on_val(N,A_10,some_val(Y_1)) % 0.54/0.87 => X_1 = Y_1 ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_10_map__upd__eqD1,axiom, % 0.54/0.87 ! [M,A_10,X_1,N,Y_1] : % 0.54/0.87 ( fun_up424764369ion_ty(M,A_10,some_ty(X_1)) = fun_up424764369ion_ty(N,A_10,some_ty(Y_1)) % 0.54/0.87 => X_1 = Y_1 ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_11_InitBlockRed_I2_J,axiom, % 0.54/0.87 ! [Ta,Ea] : % 0.54/0.87 ( hBOOL(hAPP_P159683425l_bool(typeSa1234865140_sconf(p,Ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,some_val(v))))) % 0.54/0.87 => ( hBOOL(wTrt(p,ha,Ea,ea,Ta)) % 0.54/0.87 => ? [T_5] : % 0.54/0.87 ( hBOOL(wTrt(p,h_a,Ea,e_a,T_5)) % 0.54/0.87 & hBOOL(widen_2090681816t_char(p,T_5,Ta)) ) ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_12_prod__induct4,axiom, % 0.54/0.87 ! [X_1,Pa] : % 0.54/0.87 ( ! [A_15,B,C_1,D_1] : hBOOL(hAPP_P282169671l_bool(Pa,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,C_1),D_1))))) % 0.54/0.87 => hBOOL(hAPP_P282169671l_bool(Pa,X_1)) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_13_prod__cases4,axiom, % 0.54/0.87 ! [Y_1] : % 0.54/0.87 ~ ! [A_15,B,C_1,D_1] : Y_1 != hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,C_1),D_1))) ). % 0.54/0.87 % 0.54/0.87 fof(fact_14_InitBlockRed_I4_J,axiom, % 0.54/0.87 hBOOL(hAPP_P159683425l_bool(typeSa1234865140_sconf(p,e),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),la))) ). % 0.54/0.87 % 0.54/0.87 fof(fact_15_Pair__inject,axiom, % 0.54/0.87 ! [A_10,B_1,A_9,B_2] : % 0.54/0.87 ( hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1) = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_9),B_2) % 0.54/0.87 => ~ ( A_10 = A_9 % 0.54/0.87 => B_1 != B_2 ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_16_Pair__inject,axiom, % 0.54/0.87 ! [A_10,B_1,A_9,B_2] : % 0.54/0.87 ( hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1) = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_9),B_2) % 0.54/0.87 => ~ ( A_10 = A_9 % 0.54/0.87 => B_1 != B_2 ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_17_Pair__inject,axiom, % 0.54/0.87 ! [A_10,B_1,A_9,B_2] : % 0.54/0.87 ( hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1) = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_9),B_2) % 0.54/0.87 => ~ ( A_10 = A_9 % 0.54/0.87 => B_1 != B_2 ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_18_Pair__eq,axiom, % 0.54/0.87 ! [A_10,B_1,A_9,B_2] : % 0.54/0.87 ( hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1) = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_9),B_2) % 0.54/0.87 <=> ( A_10 = A_9 % 0.54/0.87 & B_1 = B_2 ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_19_Pair__eq,axiom, % 0.54/0.87 ! [A_10,B_1,A_9,B_2] : % 0.54/0.87 ( hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1) = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_9),B_2) % 0.54/0.87 <=> ( A_10 = A_9 % 0.54/0.87 & B_1 = B_2 ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_20_Pair__eq,axiom, % 0.54/0.87 ! [A_10,B_1,A_9,B_2] : % 0.54/0.87 ( hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1) = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_9),B_2) % 0.54/0.87 <=> ( A_10 = A_9 % 0.54/0.87 & B_1 = B_2 ) ) ). % 0.54/0.87 % 0.54/0.87 fof(fact_21_split__paired__All,axiom, % 0.54/0.88 ! [Pa] : % 0.54/0.88 ( ! [X1] : hBOOL(hAPP_P282169671l_bool(Pa,X1)) % 0.54/0.88 <=> ! [A_15,B] : hBOOL(hAPP_P282169671l_bool(Pa,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),B))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_22_split__paired__All,axiom, % 0.54/0.88 ! [Pa] : % 0.54/0.88 ( ! [X1] : hBOOL(hAPP_P1708370145l_bool(Pa,X1)) % 0.54/0.88 <=> ! [A_15,B] : hBOOL(hAPP_P1708370145l_bool(Pa,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),B))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_23_split__paired__All,axiom, % 0.54/0.88 ! [Pa] : % 0.54/0.88 ( ! [X1] : hBOOL(hAPP_P159683425l_bool(Pa,X1)) % 0.54/0.88 <=> ! [A_15,B] : hBOOL(hAPP_P159683425l_bool(Pa,hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_15),B))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_24_fun__upd__def,axiom, % 0.54/0.88 ! [F,B_1,A_10,X] : % 0.54/0.88 ( ( X = A_10 % 0.54/0.88 => hAPP_l207779698on_val(fun_up1149430426on_val(F,A_10,B_1),X) = B_1 ) % 0.54/0.88 & ( X != A_10 % 0.54/0.88 => hAPP_l207779698on_val(fun_up1149430426on_val(F,A_10,B_1),X) = hAPP_l207779698on_val(F,X) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_25_fun__upd__def,axiom, % 0.54/0.88 ! [F,B_1,A_10,X] : % 0.54/0.88 ( ( X = A_10 % 0.54/0.88 => hAPP_l512744617ion_ty(fun_up424764369ion_ty(F,A_10,B_1),X) = B_1 ) % 0.54/0.88 & ( X != A_10 % 0.54/0.88 => hAPP_l512744617ion_ty(fun_up424764369ion_ty(F,A_10,B_1),X) = hAPP_l512744617ion_ty(F,X) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_26_fun__upd__idem,axiom, % 0.54/0.88 ! [F,X_1,Y_1] : % 0.54/0.88 ( hAPP_l207779698on_val(F,X_1) = Y_1 % 0.54/0.88 => fun_up1149430426on_val(F,X_1,Y_1) = F ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_27_fun__upd__idem,axiom, % 0.54/0.88 ! [F,X_1,Y_1] : % 0.54/0.88 ( hAPP_l512744617ion_ty(F,X_1) = Y_1 % 0.54/0.88 => fun_up424764369ion_ty(F,X_1,Y_1) = F ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_28_fun__upd__other,axiom, % 0.54/0.88 ! [F,Y_1,Z,X_1] : % 0.54/0.88 ( Z != X_1 % 0.54/0.88 => hAPP_l207779698on_val(fun_up1149430426on_val(F,X_1,Y_1),Z) = hAPP_l207779698on_val(F,Z) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_29_fun__upd__other,axiom, % 0.54/0.88 ! [F,Y_1,Z,X_1] : % 0.54/0.88 ( Z != X_1 % 0.54/0.88 => hAPP_l512744617ion_ty(fun_up424764369ion_ty(F,X_1,Y_1),Z) = hAPP_l512744617ion_ty(F,Z) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_30_fun__upd__twist,axiom, % 0.54/0.88 ! [M,B_1,D,A_10,C] : % 0.54/0.88 ( A_10 != C % 0.54/0.88 => fun_up1149430426on_val(fun_up1149430426on_val(M,A_10,B_1),C,D) = fun_up1149430426on_val(fun_up1149430426on_val(M,C,D),A_10,B_1) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_31_fun__upd__twist,axiom, % 0.54/0.88 ! [M,B_1,D,A_10,C] : % 0.54/0.88 ( A_10 != C % 0.54/0.88 => fun_up424764369ion_ty(fun_up424764369ion_ty(M,A_10,B_1),C,D) = fun_up424764369ion_ty(fun_up424764369ion_ty(M,C,D),A_10,B_1) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_32_fun__upd__apply,axiom, % 0.54/0.88 ! [F,Y_1,Z,X_1] : % 0.54/0.88 ( ( Z = X_1 % 0.54/0.88 => hAPP_l207779698on_val(fun_up1149430426on_val(F,X_1,Y_1),Z) = Y_1 ) % 0.54/0.88 & ( Z != X_1 % 0.54/0.88 => hAPP_l207779698on_val(fun_up1149430426on_val(F,X_1,Y_1),Z) = hAPP_l207779698on_val(F,Z) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_33_fun__upd__apply,axiom, % 0.54/0.88 ! [F,Y_1,Z,X_1] : % 0.54/0.88 ( ( Z = X_1 % 0.54/0.88 => hAPP_l512744617ion_ty(fun_up424764369ion_ty(F,X_1,Y_1),Z) = Y_1 ) % 0.54/0.88 & ( Z != X_1 % 0.54/0.88 => hAPP_l512744617ion_ty(fun_up424764369ion_ty(F,X_1,Y_1),Z) = hAPP_l512744617ion_ty(F,Z) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_34_fun__upd__same,axiom, % 0.54/0.88 ! [F,X_1,Y_1] : hAPP_l207779698on_val(fun_up1149430426on_val(F,X_1,Y_1),X_1) = Y_1 ). % 0.54/0.88 % 0.54/0.88 fof(fact_35_fun__upd__same,axiom, % 0.54/0.88 ! [F,X_1,Y_1] : hAPP_l512744617ion_ty(fun_up424764369ion_ty(F,X_1,Y_1),X_1) = Y_1 ). % 0.54/0.88 % 0.54/0.88 fof(fact_36_fun__upd__upd,axiom, % 0.54/0.88 ! [F,X_1,Y_1,Z] : fun_up1149430426on_val(fun_up1149430426on_val(F,X_1,Y_1),X_1,Z) = fun_up1149430426on_val(F,X_1,Z) ). % 0.54/0.88 % 0.54/0.88 fof(fact_37_fun__upd__upd,axiom, % 0.54/0.88 ! [F,X_1,Y_1,Z] : fun_up424764369ion_ty(fun_up424764369ion_ty(F,X_1,Y_1),X_1,Z) = fun_up424764369ion_ty(F,X_1,Z) ). % 0.54/0.88 % 0.54/0.88 fof(fact_38_fun__upd__idem__iff,axiom, % 0.54/0.88 ! [F,X_1,Y_1] : % 0.54/0.88 ( fun_up1149430426on_val(F,X_1,Y_1) = F % 0.54/0.88 <=> hAPP_l207779698on_val(F,X_1) = Y_1 ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_39_fun__upd__idem__iff,axiom, % 0.54/0.88 ! [F,X_1,Y_1] : % 0.54/0.88 ( fun_up424764369ion_ty(F,X_1,Y_1) = F % 0.54/0.88 <=> hAPP_l512744617ion_ty(F,X_1) = Y_1 ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_40_widen__refl,axiom, % 0.54/0.88 ! [P_3,T_4] : hBOOL(widen_2090681816t_char(P_3,T_4,T_4)) ). % 0.54/0.88 % 0.54/0.88 fof(fact_41_red__preserves__hconf,axiom, % 0.54/0.88 ! [Ea,Ta,Eb,Hb,Lb,E_b,H_b,L_b,Pa] : % 0.54/0.88 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))),red(Pa))) % 0.54/0.88 => ( hBOOL(wTrt(Pa,Hb,Ea,Eb,Ta)) % 0.54/0.88 => ( hBOOL(hAPP_f61040418l_bool(hconf_97414254t_char(Pa),Hb)) % 0.54/0.88 => hBOOL(hAPP_f61040418l_bool(hconf_97414254t_char(Pa),H_b)) ) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_42_red__preserves__lconf,axiom, % 0.54/0.88 ! [Ea,Ta,Eb,Hb,Lb,E_b,H_b,L_b,Pa] : % 0.54/0.88 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))),red(Pa))) % 0.54/0.88 => ( hBOOL(wTrt(Pa,Hb,Ea,Eb,Ta)) % 0.54/0.88 => ( hBOOL(hAPP_f1001225811y_bool(hAPP_f2060496320y_bool(hAPP_f1213370163y_bool(lconf_496643946t_char(Pa),Hb),Lb),Ea)) % 0.54/0.88 => hBOOL(hAPP_f1001225811y_bool(hAPP_f2060496320y_bool(hAPP_f1213370163y_bool(lconf_496643946t_char(Pa),H_b),L_b),Ea)) ) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_43_prod__cases3,axiom, % 0.54/0.88 ! [Y_1] : % 0.54/0.88 ~ ! [A_15,B,C_1] : Y_1 != hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),C_1)) ). % 0.54/0.88 % 0.54/0.88 fof(fact_44_prod__cases3,axiom, % 0.54/0.88 ! [Y_1] : % 0.54/0.88 ~ ! [A_15,B,C_1] : Y_1 != hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C_1)) ). % 0.54/0.88 % 0.54/0.88 fof(fact_45_prod__induct3,axiom, % 0.54/0.88 ! [X_1,Pa] : % 0.54/0.88 ( ! [A_15,B,C_1] : hBOOL(hAPP_P282169671l_bool(Pa,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,B),C_1)))) % 0.54/0.88 => hBOOL(hAPP_P282169671l_bool(Pa,X_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_46_prod__induct3,axiom, % 0.54/0.88 ! [X_1,Pa] : % 0.54/0.88 ( ! [A_15,B,C_1] : hBOOL(hAPP_P1708370145l_bool(Pa,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,B),C_1)))) % 0.54/0.88 => hBOOL(hAPP_P1708370145l_bool(Pa,X_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_47_red__preserves__sconf,axiom, % 0.54/0.88 ! [Ea,Ta,Eb,S,E_b,S_1,Pa] : % 0.54/0.88 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),S_1)),red(Pa))) % 0.54/0.88 => ( hBOOL(wTrt(Pa,hp(S),Ea,Eb,Ta)) % 0.54/0.88 => ( hBOOL(hAPP_P159683425l_bool(typeSa1234865140_sconf(Pa,Ea),S)) % 0.54/0.88 => hBOOL(hAPP_P159683425l_bool(typeSa1234865140_sconf(Pa,Ea),S_1)) ) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_48_pred__equals__eq2,axiom, % 0.54/0.88 ! [S_3,R_1] : % 0.54/0.88 ( ! [X,Xa] : % 0.54/0.88 ( hBOOL(member840932460on_val(hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Xa),R_1)) % 0.54/0.88 <=> hBOOL(member840932460on_val(hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Xa),S_3)) ) % 0.54/0.88 <=> R_1 = S_3 ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_49_pred__equals__eq2,axiom, % 0.54/0.88 ! [S_3,R_1] : % 0.54/0.88 ( ! [X,Xa] : % 0.54/0.88 ( hBOOL(member763590124on_val(hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Xa),R_1)) % 0.54/0.88 <=> hBOOL(member763590124on_val(hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Xa),S_3)) ) % 0.54/0.88 <=> R_1 = S_3 ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_50_pred__equals__eq2,axiom, % 0.54/0.88 ! [S_3,R_1] : % 0.54/0.88 ( ! [X,Xa] : % 0.54/0.88 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Xa),R_1)) % 0.54/0.88 <=> hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Xa),S_3)) ) % 0.54/0.88 <=> R_1 = S_3 ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_51_prod_Oexhaust,axiom, % 0.54/0.88 ! [Y_1] : % 0.54/0.88 ~ ! [A_15,B] : Y_1 != hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),B) ). % 0.54/0.88 % 0.54/0.88 fof(fact_52_prod_Oexhaust,axiom, % 0.54/0.88 ! [Y_1] : % 0.54/0.88 ~ ! [A_15,B] : Y_1 != hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),B) ). % 0.54/0.88 % 0.54/0.88 fof(fact_53_prod_Oexhaust,axiom, % 0.54/0.88 ! [Y_1] : % 0.54/0.88 ~ ! [A_15,B] : Y_1 != hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_15),B) ). % 0.54/0.88 % 0.54/0.88 fof(fact_54_widen__trans,axiom, % 0.54/0.88 ! [T_3,P_2,S_2,U_1] : % 0.54/0.88 ( hBOOL(widen_2090681816t_char(P_2,S_2,U_1)) % 0.54/0.88 => ( hBOOL(widen_2090681816t_char(P_2,U_1,T_3)) % 0.54/0.88 => hBOOL(widen_2090681816t_char(P_2,S_2,T_3)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_55_InitBlockRed_I5_J,axiom, % 0.54/0.88 hBOOL(wTrt(p,ha,e,block_list_char(v_1,t_1,seq_list_char(lAss_list_char(v_1,val_list_char(v)),ea)),t)) ). % 0.54/0.88 % 0.54/0.88 fof(fact_56_split__paired__Ex,axiom, % 0.54/0.88 ! [Pa] : % 0.54/0.88 ( ? [X1] : hBOOL(hAPP_P282169671l_bool(Pa,X1)) % 0.54/0.88 <=> ? [A_15,B] : hBOOL(hAPP_P282169671l_bool(Pa,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),B))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_57_split__paired__Ex,axiom, % 0.54/0.88 ! [Pa] : % 0.54/0.88 ( ? [X1] : hBOOL(hAPP_P1708370145l_bool(Pa,X1)) % 0.54/0.88 <=> ? [A_15,B] : hBOOL(hAPP_P1708370145l_bool(Pa,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),B))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_58_split__paired__Ex,axiom, % 0.54/0.88 ! [Pa] : % 0.54/0.88 ( ? [X1] : hBOOL(hAPP_P159683425l_bool(Pa,X1)) % 0.54/0.88 <=> ? [A_15,B] : hBOOL(hAPP_P159683425l_bool(Pa,hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_15),B))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_59_PairE,axiom, % 0.54/0.88 ! [P_1] : % 0.54/0.88 ~ ! [X,Y] : P_1 != hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Y) ). % 0.54/0.88 % 0.54/0.88 fof(fact_60_PairE,axiom, % 0.54/0.88 ! [P_1] : % 0.54/0.88 ~ ! [X,Y] : P_1 != hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Y) ). % 0.54/0.88 % 0.54/0.88 fof(fact_61_PairE,axiom, % 0.54/0.88 ! [P_1] : % 0.54/0.88 ~ ! [X,Y] : P_1 != hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Y) ). % 0.54/0.88 % 0.54/0.88 fof(fact_62_internal__split__conv,axiom, % 0.54/0.88 ! [C,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc2128769400l_bool,C),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1))) % 0.54/0.88 <=> hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(C,A_10),B_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_63_sconf__def,axiom, % 0.54/0.88 ! [Pa,Ea,S] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(typeSa1234865140_sconf(Pa,Ea),S)) % 0.54/0.88 <=> hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,cOMBS_570216337l_bool(hAPP_f1523875321l_bool(hAPP_f592397849l_bool(cOMBB_1718333400on_val,cOMBB_383678192on_val),hAPP_f1452292669l_bool(hAPP_f1977633121l_bool(cOMBB_1303934920on_val,fconj),hconf_97414254t_char(Pa))),hAPP_f550652027l_bool(hAPP_f838396643l_bool(cOMBC_2027949654l_bool,hAPP_f857351829l_bool(hAPP_f348318673l_bool(cOMBB_1518282696on_val,cOMBC_832625297y_bool),lconf_496643946t_char(Pa))),Ea))),S)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_64_prod__caseI,axiom, % 0.54/0.88 ! [F1,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(F1,A_10),B_1)) % 0.54/0.88 => hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,F1),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_65_prod__caseI,axiom, % 0.54/0.88 ! [F1,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(F1,A_10),B_1)) % 0.54/0.88 => hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,F1),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_66_prod__caseI,axiom, % 0.54/0.88 ! [F1,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(F1,A_10),B_1)) % 0.54/0.88 => hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F1),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_67_splitI,axiom, % 0.54/0.88 ! [F,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(F,A_10),B_1)) % 0.54/0.88 => hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,F),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_68_splitI,axiom, % 0.54/0.88 ! [F,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(F,A_10),B_1)) % 0.54/0.88 => hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,F),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_69_splitI,axiom, % 0.54/0.88 ! [F,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(F,A_10),B_1)) % 0.54/0.88 => hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1))) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_70_splitD,axiom, % 0.54/0.88 ! [F,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,F),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1))) % 0.54/0.88 => hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(F,A_10),B_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_71_splitD,axiom, % 0.54/0.88 ! [F,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,F),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1))) % 0.54/0.88 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(F,A_10),B_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_72_splitD,axiom, % 0.54/0.88 ! [F,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1))) % 0.54/0.88 => hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(F,A_10),B_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_73_split__weak__cong,axiom, % 0.54/0.88 ! [C,P_1,Q_2] : % 0.54/0.88 ( P_1 = Q_2 % 0.54/0.88 => ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,C),P_1)) % 0.54/0.88 <=> hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,C),Q_2)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_74_split__weak__cong,axiom, % 0.54/0.88 ! [C,P_1,Q_2] : % 0.54/0.88 ( P_1 = Q_2 % 0.54/0.88 => ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,C),P_1)) % 0.54/0.88 <=> hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,C),Q_2)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_75_split__weak__cong,axiom, % 0.54/0.88 ! [C,P_1,Q_2] : % 0.54/0.88 ( P_1 = Q_2 % 0.54/0.88 => ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,C),P_1)) % 0.54/0.88 <=> hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,C),Q_2)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_76_internal__split__def,axiom, % 0.54/0.88 produc399384568l_bool = produc1815960045l_bool ). % 0.54/0.88 % 0.54/0.88 fof(fact_77_internal__split__def,axiom, % 0.54/0.88 produc1988544340l_bool = produc1911463199l_bool ). % 0.54/0.88 % 0.54/0.88 fof(fact_78_internal__split__def,axiom, % 0.54/0.88 produc2128769400l_bool = produc1958875245l_bool ). % 0.54/0.88 % 0.54/0.88 fof(fact_79_split__twice,axiom, % 0.54/0.88 ! [F,G,P_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F),hAPP_P789556885on_val(hAPP_f1520199827on_val(produc1174947465on_val,G),P_1))) % 0.54/0.88 <=> hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,hAPP_f653692369l_bool(hAPP_f516738477l_bool(cOMBB_819439237t_char,hAPP_f1825030711l_bool(cOMBB_877741809on_val,hAPP_f2121594859l_bool(produc1958875245l_bool,F))),G)),P_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_80_split__twice,axiom, % 0.54/0.88 ! [F,G,P_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F),hAPP_P1760219823on_val(hAPP_f394183983on_val(produc1003071703on_val,G),P_1))) % 0.54/0.88 <=> hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,hAPP_f1241216909l_bool(hAPP_f1438732387l_bool(cOMBB_635947099on_val,hAPP_f881985847l_bool(cOMBB_1083177073on_val,hAPP_f2121594859l_bool(produc1958875245l_bool,F))),G)),P_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_81_split__twice,axiom, % 0.54/0.88 ! [F,G,P_1] : % 0.54/0.88 ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,F),hAPP_P604205461on_val(hAPP_f1309113673on_val(produc901351817on_val,G),P_1))) % 0.54/0.88 <=> hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,hAPP_f850751421l_bool(hAPP_f399538905l_bool(cOMBB_1466889536on_val,hAPP_f1233687287l_bool(cOMBB_171276332on_val,hAPP_f1930574389l_bool(produc1815960045l_bool,F))),G)),P_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_82_split__twice,axiom, % 0.54/0.88 ! [F,G,P_1] : % 0.54/0.88 ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,F),hAPP_P2024243179on_val(hAPP_f204556415on_val(produc1148763895on_val,G),P_1))) % 0.54/0.88 <=> hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,hAPP_f927043595l_bool(hAPP_f1043869573l_bool(cOMBB_1259202826on_val,hAPP_f2052660463l_bool(cOMBB_1292453606on_val,hAPP_f635218277l_bool(produc1911463199l_bool,F))),G)),P_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_83_split__part,axiom, % 0.54/0.88 ! [Pa,Q_1,X] : % 0.54/0.88 ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,hAPP_f546724245l_bool(hAPP_f917296015l_bool(cOMBB_740252943t_char,hAPP_f1308714617l_bool(cOMBB_338347573on_val,hAPP_b589554111l_bool(fconj,Pa))),Q_1)),X)) % 0.54/0.88 <=> ( hBOOL(Pa) % 0.54/0.88 & hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,Q_1),X)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_84_split__part,axiom, % 0.54/0.88 ! [Pa,Q_1,X] : % 0.54/0.88 ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,hAPP_f641257349l_bool(hAPP_f2032347769l_bool(cOMBB_466903633on_val,hAPP_f1560238713l_bool(cOMBB_672625589on_val,hAPP_b589554111l_bool(fconj,Pa))),Q_1)),X)) % 0.54/0.88 <=> ( hBOOL(Pa) % 0.54/0.88 & hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,Q_1),X)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_85_split__part,axiom, % 0.54/0.88 ! [Pa,Q_1,X] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,hAPP_f555424277l_bool(hAPP_f1734879897l_bool(cOMBB_1522540928on_val,hAPP_f1863694447l_bool(cOMBB_383678192on_val,hAPP_b589554111l_bool(fconj,Pa))),Q_1)),X)) % 0.54/0.88 <=> ( hBOOL(Pa) % 0.54/0.88 & hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,Q_1),X)) ) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_86_prod_Osimps_I2_J,axiom, % 0.54/0.88 ! [F1,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F1),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1))) % 0.54/0.88 <=> hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(F1,A_10),B_1)) ) ). % 0.54/0.88 % 0.54/0.88 fof(fact_87_prod_Osimps_I2_J,axiom, % 0.54/0.88 ! [F1,A_10,B_1] : % 0.54/0.88 ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,F1),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1))) % 0.54/0.88 <=> hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(F1,A_10),B_1)) ) ). % 0.54/0.88 % 0.54/0.89 fof(fact_88_prod_Osimps_I2_J,axiom, % 0.54/0.89 ! [F1,A_10,B_1] : % 0.54/0.89 ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,F1),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1))) % 0.54/0.89 <=> hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(F1,A_10),B_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_89_split__conv,axiom, % 0.54/0.89 ! [F,A_10,B_1] : % 0.54/0.89 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,F),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1))) % 0.54/0.89 <=> hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(F,A_10),B_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_90_split__conv,axiom, % 0.54/0.89 ! [F,A_10,B_1] : % 0.54/0.89 ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,F),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1))) % 0.54/0.89 <=> hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(F,A_10),B_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_91_split__conv,axiom, % 0.54/0.89 ! [F,A_10,B_1] : % 0.54/0.89 ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,F),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1))) % 0.54/0.89 <=> hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(F,A_10),B_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_92_split__eta,axiom, % 0.54/0.89 ! [F] : hAPP_f2121594859l_bool(produc1958875245l_bool,hAPP_f1363667773l_bool(hAPP_f1050935001l_bool(cOMBB_1153617344on_val,hAPP_f2057883639l_bool(cOMBB_1750801836on_val,F)),produc899768717on_val)) = F ). % 0.54/0.89 % 0.54/0.89 fof(fact_93_split__eta,axiom, % 0.54/0.89 ! [F] : hAPP_f635218277l_bool(produc1911463199l_bool,hAPP_f1342895119l_bool(hAPP_f639265145l_bool(cOMBB_364363975on_val,hAPP_f365540729l_bool(cOMBB_1466662571on_val,F)),produc1441475159on_val)) = F ). % 0.54/0.89 % 0.54/0.89 fof(fact_94_split__eta,axiom, % 0.54/0.89 ! [F] : hAPP_f1930574389l_bool(produc1815960045l_bool,hAPP_f439412817l_bool(hAPP_f1725502637l_bool(cOMBB_1027621637t_char,hAPP_f10074679l_bool(cOMBB_1759207793on_val,F)),produc1259058957on_val)) = F ). % 0.54/0.89 % 0.54/0.89 fof(fact_95_red__reds_OInitBlockRed,axiom, % 0.54/0.89 ! [Ta,V_a,Eb,Hb,Lb,Va_1,Va,E_b,H_b,L_b,Pa] : % 0.54/0.89 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),fun_up1149430426on_val(Lb,Va_1,some_val(Va))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))),red(Pa))) % 0.54/0.89 => ( hAPP_l207779698on_val(L_b,Va_1) = some_val(V_a) % 0.54/0.89 => hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(Va)),Eb))),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(V_a)),E_b))),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),fun_up1149430426on_val(L_b,Va_1,hAPP_l207779698on_val(Lb,Va_1))))),red(Pa))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_96_red__reds_ORedInitBlock,axiom, % 0.54/0.89 ! [Va_1,Ta,Va,U,S,Pa] : hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(Va)),val_list_char(U)))),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,val_list_char(U)),S)),red(Pa))) ). % 0.54/0.89 % 0.54/0.89 fof(fact_97_splitI2,axiom, % 0.54/0.89 ! [C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),B) % 0.54/0.89 => hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(C,A_15),B)) ) % 0.54/0.89 => hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,C),P_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_98_splitI2,axiom, % 0.54/0.89 ! [C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),B) % 0.54/0.89 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(C,A_15),B)) ) % 0.54/0.89 => hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,C),P_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_99_splitI2,axiom, % 0.54/0.89 ! [C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_15),B) % 0.54/0.89 => hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(C,A_15),B)) ) % 0.54/0.89 => hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,C),P_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_100_splitE,axiom, % 0.54/0.89 ! [C,P_1] : % 0.54/0.89 ( hBOOL(hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,C),P_1)) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Y) % 0.54/0.89 => ~ hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(C,X),Y)) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_101_splitE,axiom, % 0.54/0.89 ! [C,P_1] : % 0.54/0.89 ( hBOOL(hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,C),P_1)) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Y) % 0.54/0.89 => ~ hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(C,X),Y)) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_102_splitE,axiom, % 0.54/0.89 ! [C,P_1] : % 0.54/0.89 ( hBOOL(hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,C),P_1)) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Y) % 0.54/0.89 => ~ hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(C,X),Y)) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_103_WTrtBlock,axiom, % 0.54/0.89 ! [Pa,Hb,Ea,Va_1,Ta,Eb,T_a] : % 0.54/0.89 ( hBOOL(wTrt(Pa,Hb,fun_up424764369ion_ty(Ea,Va_1,some_ty(Ta)),Eb,T_a)) % 0.54/0.89 => hBOOL(wTrt(Pa,Hb,Ea,block_list_char(Va_1,Ta,Eb),T_a)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_104_mem__splitI,axiom, % 0.54/0.89 ! [Z,C,A_10,B_1] : % 0.54/0.89 ( hBOOL(member763590124on_val(Z,hAPP_P595502227l_bool(hAPP_P1134042693l_bool(C,A_10),B_1))) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P1826803705l_bool(hAPP_f444383845l_bool(produc376702929l_bool,C),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1)))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_105_mem__splitI,axiom, % 0.54/0.89 ! [Z,C,A_10,B_1] : % 0.54/0.89 ( hBOOL(member840932460on_val(Z,hAPP_P1116729363l_bool(hAPP_P1953518277l_bool(C,A_10),B_1))) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P678729081l_bool(hAPP_f1591648613l_bool(produc20018513l_bool,C),hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_10),B_1)))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_106_mem__splitI,axiom, % 0.54/0.89 ! [Z,C,A_10,B_1] : % 0.54/0.89 ( hBOOL(member763590124on_val(Z,hAPP_P1988153107l_bool(hAPP_e500528395l_bool(C,A_10),B_1))) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P595502227l_bool(hAPP_f468299289l_bool(produc2036005791l_bool,C),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1)))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_107_mem__splitI,axiom, % 0.54/0.89 ! [Z,C,A_10,B_1] : % 0.54/0.89 ( hBOOL(member840932460on_val(Z,hAPP_P1638898323l_bool(hAPP_e592495499l_bool(C,A_10),B_1))) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P1116729363l_bool(hAPP_f1760682521l_bool(produc1275132703l_bool,C),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_10),B_1)))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_108_mem__splitI,axiom, % 0.54/0.89 ! [Z,C,A_10,B_1] : % 0.54/0.89 ( hBOOL(member763590124on_val(Z,hAPP_f396019662l_bool(hAPP_f2135509569l_bool(C,A_10),B_1))) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P1988153107l_bool(hAPP_f1276548047l_bool(produc121041439l_bool,C),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1)))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_109_mem__splitI,axiom, % 0.54/0.89 ! [Z,C,A_10,B_1] : % 0.54/0.89 ( hBOOL(member840932460on_val(Z,hAPP_f2011777102l_bool(hAPP_f2144092865l_bool(C,A_10),B_1))) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P1638898323l_bool(hAPP_f833559503l_bool(produc334393759l_bool,C),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_10),B_1)))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_110_WTrtSeq,axiom, % 0.54/0.89 ! [E_2,T_2,Pa,Hb,Ea,E_1,T_1] : % 0.54/0.89 ( hBOOL(wTrt(Pa,Hb,Ea,E_1,T_1)) % 0.54/0.89 => ( hBOOL(wTrt(Pa,Hb,Ea,E_2,T_2)) % 0.54/0.89 => hBOOL(wTrt(Pa,Hb,Ea,seq_list_char(E_1,E_2),T_2)) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_111_red__reds_OSeqRed,axiom, % 0.54/0.89 ! [E_2,Eb,S,E_b,S_1,Pa] : % 0.54/0.89 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),S_1)),red(Pa))) % 0.54/0.89 => hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,seq_list_char(Eb,E_2)),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,seq_list_char(E_b,E_2)),S_1)),red(Pa))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_112_red__reds_OLAssRed,axiom, % 0.54/0.89 ! [Va_1,Eb,S,E_b,S_1,Pa] : % 0.54/0.89 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),S_1)),red(Pa))) % 0.54/0.89 => hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,lAss_list_char(Va_1,Eb)),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,lAss_list_char(Va_1,E_b)),S_1)),red(Pa))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_113_red__reds_ORedSeq,axiom, % 0.54/0.89 ! [Va,E_2,S,Pa] : hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,seq_list_char(val_list_char(Va),E_2)),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_2),S)),red(Pa))) ). % 0.54/0.89 % 0.54/0.89 fof(fact_114_red__reds_ORedBlock,axiom, % 0.54/0.89 ! [Va_1,Ta,U,S,Pa] : hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,block_list_char(Va_1,Ta,val_list_char(U))),S)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,val_list_char(U)),S)),red(Pa))) ). % 0.54/0.89 % 0.54/0.89 fof(fact_115_mem__splitE,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( hBOOL(member763590124on_val(Z,hAPP_P1826803705l_bool(hAPP_f444383845l_bool(produc376702929l_bool,C),P_1))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Y) % 0.54/0.89 => ~ hBOOL(member763590124on_val(Z,hAPP_P595502227l_bool(hAPP_P1134042693l_bool(C,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_116_mem__splitE,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( hBOOL(member840932460on_val(Z,hAPP_P678729081l_bool(hAPP_f1591648613l_bool(produc20018513l_bool,C),P_1))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Y) % 0.54/0.89 => ~ hBOOL(member840932460on_val(Z,hAPP_P1116729363l_bool(hAPP_P1953518277l_bool(C,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_117_mem__splitE,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( hBOOL(member763590124on_val(Z,hAPP_P595502227l_bool(hAPP_f468299289l_bool(produc2036005791l_bool,C),P_1))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Y) % 0.54/0.89 => ~ hBOOL(member763590124on_val(Z,hAPP_P1988153107l_bool(hAPP_e500528395l_bool(C,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_118_mem__splitE,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( hBOOL(member840932460on_val(Z,hAPP_P1116729363l_bool(hAPP_f1760682521l_bool(produc1275132703l_bool,C),P_1))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Y) % 0.54/0.89 => ~ hBOOL(member840932460on_val(Z,hAPP_P1638898323l_bool(hAPP_e592495499l_bool(C,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_119_mem__splitE,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( hBOOL(member763590124on_val(Z,hAPP_P1988153107l_bool(hAPP_f1276548047l_bool(produc121041439l_bool,C),P_1))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Y) % 0.54/0.89 => ~ hBOOL(member763590124on_val(Z,hAPP_f396019662l_bool(hAPP_f2135509569l_bool(C,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_120_mem__splitE,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( hBOOL(member840932460on_val(Z,hAPP_P1638898323l_bool(hAPP_f833559503l_bool(produc334393759l_bool,C),P_1))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( P_1 = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Y) % 0.54/0.89 => ~ hBOOL(member840932460on_val(Z,hAPP_f2011777102l_bool(hAPP_f2144092865l_bool(C,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_121_mem__splitI2,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),B) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P595502227l_bool(hAPP_P1134042693l_bool(C,A_15),B))) ) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P1826803705l_bool(hAPP_f444383845l_bool(produc376702929l_bool,C),P_1))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_122_mem__splitI2,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,A_15),B) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P1116729363l_bool(hAPP_P1953518277l_bool(C,A_15),B))) ) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P678729081l_bool(hAPP_f1591648613l_bool(produc20018513l_bool,C),P_1))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_123_mem__splitI2,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),B) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P1988153107l_bool(hAPP_e500528395l_bool(C,A_15),B))) ) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P595502227l_bool(hAPP_f468299289l_bool(produc2036005791l_bool,C),P_1))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_124_mem__splitI2,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,A_15),B) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P1638898323l_bool(hAPP_e592495499l_bool(C,A_15),B))) ) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P1116729363l_bool(hAPP_f1760682521l_bool(produc1275132703l_bool,C),P_1))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_125_mem__splitI2,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_15),B) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_f396019662l_bool(hAPP_f2135509569l_bool(C,A_15),B))) ) % 0.54/0.89 => hBOOL(member763590124on_val(Z,hAPP_P1988153107l_bool(hAPP_f1276548047l_bool(produc121041439l_bool,C),P_1))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_126_mem__splitI2,axiom, % 0.54/0.89 ! [Z,C,P_1] : % 0.54/0.89 ( ! [A_15,B] : % 0.54/0.89 ( P_1 = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,A_15),B) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_f2011777102l_bool(hAPP_f2144092865l_bool(C,A_15),B))) ) % 0.54/0.89 => hBOOL(member840932460on_val(Z,hAPP_P1638898323l_bool(hAPP_f833559503l_bool(produc334393759l_bool,C),P_1))) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_127_red__reds_ORedLAss,axiom, % 0.54/0.89 ! [Va_1,Va,Hb,Lb,Pa] : hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,lAss_list_char(Va_1,val_list_char(Va))),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,val_list_char(unit)),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),fun_up1149430426on_val(Lb,Va_1,some_val(Va))))),red(Pa))) ). % 0.54/0.89 % 0.54/0.89 fof(fact_128_cond__split__eta,axiom, % 0.54/0.89 ! [G,F] : % 0.54/0.89 ( ! [X,Y] : % 0.54/0.89 ( hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(F,X),Y)) % 0.54/0.89 <=> hBOOL(hAPP_P159683425l_bool(G,hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Y))) ) % 0.54/0.89 => hAPP_f2121594859l_bool(produc1958875245l_bool,F) = G ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_129_cond__split__eta,axiom, % 0.54/0.89 ! [G,F] : % 0.54/0.89 ( ! [X,Y] : % 0.54/0.89 ( hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(F,X),Y)) % 0.54/0.89 <=> hBOOL(hAPP_P282169671l_bool(G,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Y))) ) % 0.54/0.89 => hAPP_f635218277l_bool(produc1911463199l_bool,F) = G ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_130_cond__split__eta,axiom, % 0.54/0.89 ! [G,F] : % 0.54/0.89 ( ! [X,Y] : % 0.54/0.89 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(F,X),Y)) % 0.54/0.89 <=> hBOOL(hAPP_P1708370145l_bool(G,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Y))) ) % 0.54/0.89 => hAPP_f1930574389l_bool(produc1815960045l_bool,F) = G ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_131_splitE2,axiom, % 0.54/0.89 ! [Q_1,Pa,Z] : % 0.54/0.89 ( hBOOL(hAPP_bool_bool(Q_1,hAPP_P159683425l_bool(hAPP_f2121594859l_bool(produc1958875245l_bool,Pa),Z))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( Z = hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,X),Y) % 0.54/0.89 => ~ hBOOL(hAPP_bool_bool(Q_1,hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(Pa,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_132_splitE2,axiom, % 0.54/0.89 ! [Q_1,Pa,Z] : % 0.54/0.89 ( hBOOL(hAPP_bool_bool(Q_1,hAPP_P282169671l_bool(hAPP_f635218277l_bool(produc1911463199l_bool,Pa),Z))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( Z = hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,X),Y) % 0.54/0.89 => ~ hBOOL(hAPP_bool_bool(Q_1,hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(Pa,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_133_splitE2,axiom, % 0.54/0.89 ! [Q_1,Pa,Z] : % 0.54/0.89 ( hBOOL(hAPP_bool_bool(Q_1,hAPP_P1708370145l_bool(hAPP_f1930574389l_bool(produc1815960045l_bool,Pa),Z))) % 0.54/0.89 => ~ ! [X,Y] : % 0.54/0.89 ( Z = hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Y) % 0.54/0.89 => ~ hBOOL(hAPP_bool_bool(Q_1,hAPP_P159683425l_bool(hAPP_e1833980889l_bool(Pa,X),Y))) ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_134_exp_Osimps_I143_J,axiom, % 0.54/0.89 ! [A_14,Ty_7,Exp_13,A_13,Exp_12] : block_list_char(A_14,Ty_7,Exp_13) != lAss_list_char(A_13,Exp_12) ). % 0.54/0.89 % 0.54/0.89 fof(fact_135_exp_Osimps_I196_J,axiom, % 0.54/0.89 ! [A_12,Ty_6,Exp_11,Exp1_7,Exp2_7] : block_list_char(A_12,Ty_6,Exp_11) != seq_list_char(Exp1_7,Exp2_7) ). % 0.54/0.89 % 0.54/0.89 fof(fact_136_exp_Osimps_I3_J,axiom, % 0.54/0.89 ! [Val_7,Val_6] : % 0.54/0.89 ( val_list_char(Val_7) = val_list_char(Val_6) % 0.54/0.89 <=> Val_7 = Val_6 ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_137_exp_Osimps_I11_J,axiom, % 0.54/0.89 ! [Exp1_6,Exp2_6,Exp1_5,Exp2_5] : % 0.54/0.89 ( seq_list_char(Exp1_6,Exp2_6) = seq_list_char(Exp1_5,Exp2_5) % 0.54/0.89 <=> ( Exp1_6 = Exp1_5 % 0.54/0.89 & Exp2_6 = Exp2_5 ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_138_exp_Osimps_I6_J,axiom, % 0.54/0.89 ! [A_10,Exp_10,A_9,Exp_9] : % 0.54/0.89 ( lAss_list_char(A_10,Exp_10) = lAss_list_char(A_9,Exp_9) % 0.54/0.89 <=> ( A_10 = A_9 % 0.54/0.89 & Exp_10 = Exp_9 ) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_139_mem__def,axiom, % 0.54/0.89 ! [X_1,A_11] : % 0.54/0.89 ( hBOOL(member763590124on_val(X_1,A_11)) % 0.54/0.89 <=> hBOOL(hAPP_P159683425l_bool(A_11,X_1)) ) ). % 0.54/0.89 % 0.54/0.89 fof(fact_140_mem__def,axiom, % 0.54/0.90 ! [X_1,A_11] : % 0.54/0.90 ( hBOOL(member840932460on_val(X_1,A_11)) % 0.54/0.90 <=> hBOOL(hAPP_P1708370145l_bool(A_11,X_1)) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_141_mem__def,axiom, % 0.54/0.90 ! [X_1,A_11] : % 0.54/0.90 ( hBOOL(member773094996on_val(X_1,A_11)) % 0.54/0.90 <=> hBOOL(hAPP_P282169671l_bool(A_11,X_1)) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_142_exp_Osimps_I10_J,axiom, % 0.54/0.90 ! [A_10,Ty_5,Exp_10,A_9,Ty_4,Exp_9] : % 0.54/0.90 ( block_list_char(A_10,Ty_5,Exp_10) = block_list_char(A_9,Ty_4,Exp_9) % 0.54/0.90 <=> ( A_10 = A_9 % 0.54/0.90 & Ty_5 = Ty_4 % 0.54/0.90 & Exp_10 = Exp_9 ) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_143_exp_Osimps_I84_J,axiom, % 0.54/0.90 ! [Val_5,Exp1_4,Exp2_4] : val_list_char(Val_5) != seq_list_char(Exp1_4,Exp2_4) ). % 0.54/0.90 % 0.54/0.90 fof(fact_144_exp_Osimps_I74_J,axiom, % 0.54/0.90 ! [Val_4,A_8,Exp_8] : val_list_char(Val_4) != lAss_list_char(A_8,Exp_8) ). % 0.54/0.90 % 0.54/0.90 fof(fact_145_exp_Osimps_I85_J,axiom, % 0.54/0.90 ! [Exp1_3,Exp2_3,Val_3] : seq_list_char(Exp1_3,Exp2_3) != val_list_char(Val_3) ). % 0.54/0.90 % 0.54/0.90 fof(fact_146_exp_Osimps_I75_J,axiom, % 0.54/0.90 ! [A_7,Exp_7,Val_2] : lAss_list_char(A_7,Exp_7) != val_list_char(Val_2) ). % 0.54/0.90 % 0.54/0.90 fof(fact_147_exp_Osimps_I82_J,axiom, % 0.54/0.90 ! [Val_1,A_6,Ty_3,Exp_6] : val_list_char(Val_1) != block_list_char(A_6,Ty_3,Exp_6) ). % 0.54/0.90 % 0.54/0.90 fof(fact_148_exp_Osimps_I83_J,axiom, % 0.54/0.90 ! [A_5,Ty_2,Exp_5,Val] : block_list_char(A_5,Ty_2,Exp_5) != val_list_char(Val) ). % 0.54/0.90 % 0.54/0.90 fof(fact_149_exp_Osimps_I145_J,axiom, % 0.54/0.90 ! [Exp1_2,Exp2_2,A_4,Exp_4] : seq_list_char(Exp1_2,Exp2_2) != lAss_list_char(A_4,Exp_4) ). % 0.54/0.90 % 0.54/0.90 fof(fact_150_exp_Osimps_I144_J,axiom, % 0.54/0.90 ! [A_3,Exp_3,Exp1_1,Exp2_1] : lAss_list_char(A_3,Exp_3) != seq_list_char(Exp1_1,Exp2_1) ). % 0.54/0.90 % 0.54/0.90 fof(fact_151_exp_Osimps_I197_J,axiom, % 0.54/0.90 ! [Exp1,Exp2,A_2,Ty_1,Exp_2] : seq_list_char(Exp1,Exp2) != block_list_char(A_2,Ty_1,Exp_2) ). % 0.54/0.90 % 0.54/0.90 fof(fact_152_exp_Osimps_I142_J,axiom, % 0.54/0.90 ! [A_1,Exp_1,A,Ty,Exp] : lAss_list_char(A_1,Exp_1) != block_list_char(A,Ty,Exp) ). % 0.54/0.90 % 0.54/0.90 fof(fact_153_redp__redsp_OInitBlockRed,axiom, % 0.54/0.90 ! [Ta,V_a,Pa,Eb,Hb,Lb,Va_1,Va,E_b,H_b,L_b] : % 0.54/0.90 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,Eb,hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),fun_up1149430426on_val(Lb,Va_1,some_val(Va)))),E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))) % 0.54/0.90 => ( hAPP_l207779698on_val(L_b,Va_1) = some_val(V_a) % 0.54/0.90 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(Va)),Eb)),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb)),block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(V_a)),E_b))),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),fun_up1149430426on_val(L_b,Va_1,hAPP_l207779698on_val(Lb,Va_1))))) ) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_154_red__reds_OBlockRedSome,axiom, % 0.54/0.90 ! [Ta,Va,Eb,Hb,Lb,Va_1,E_b,H_b,L_b,Pa] : % 0.54/0.90 ( hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Eb),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),fun_up1149430426on_val(Lb,Va_1,none_val)))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))),red(Pa))) % 0.54/0.90 => ( hAPP_l207779698on_val(L_b,Va_1) = some_val(Va) % 0.54/0.90 => ( ~ hBOOL(assigned(Va_1,Eb)) % 0.54/0.90 => hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,block_list_char(Va_1,Ta,Eb)),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(Va)),E_b))),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),fun_up1149430426on_val(L_b,Va_1,hAPP_l207779698on_val(Lb,Va_1))))),red(Pa))) ) ) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_155_redp__redsp_OSeqRed,axiom, % 0.54/0.90 ! [E_2,Pa,Eb,S,E_b,S_1] : % 0.54/0.90 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,Eb,S),E_b),S_1)) % 0.54/0.90 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,seq_list_char(Eb,E_2),S),seq_list_char(E_b,E_2)),S_1)) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_156_redp__redsp_OLAssRed,axiom, % 0.54/0.90 ! [Va_1,Pa,Eb,S,E_b,S_1] : % 0.54/0.90 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,Eb,S),E_b),S_1)) % 0.54/0.90 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,lAss_list_char(Va_1,Eb),S),lAss_list_char(Va_1,E_b)),S_1)) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_157_redp__redsp_OBlockRedNone,axiom, % 0.54/0.90 ! [Ta,Pa,Eb,Hb,Lb,Va_1,E_b,H_b,L_b] : % 0.54/0.90 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,Eb,hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),fun_up1149430426on_val(Lb,Va_1,none_val))),E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))) % 0.54/0.90 => ( hAPP_l207779698on_val(L_b,Va_1) = none_val % 0.54/0.90 => ( ~ hBOOL(assigned(Va_1,Eb)) % 0.54/0.90 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,block_list_char(Va_1,Ta,Eb),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb)),block_list_char(Va_1,Ta,E_b)),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),fun_up1149430426on_val(L_b,Va_1,hAPP_l207779698on_val(Lb,Va_1))))) ) ) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_158_redp__redsp_ORedSeq,axiom, % 0.54/0.90 ! [Pa,Va,E_2,S] : hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,seq_list_char(val_list_char(Va),E_2),S),E_2),S)) ). % 0.54/0.90 % 0.54/0.90 fof(fact_159_map__upd__nonempty,axiom, % 0.54/0.90 ! [T,K,X_1] : % 0.54/0.90 ~ ! [X] : hAPP_l207779698on_val(fun_up1149430426on_val(T,K,some_val(X_1)),X) = none_val ). % 0.54/0.90 % 0.54/0.90 fof(fact_160_map__upd__nonempty,axiom, % 0.54/0.90 ! [T,K,X_1] : % 0.54/0.90 ~ ! [X] : hAPP_l512744617ion_ty(fun_up424764369ion_ty(T,K,some_ty(X_1)),X) = none_ty ). % 0.54/0.90 % 0.54/0.90 fof(fact_161_redp__redsp_ORedBlock,axiom, % 0.54/0.90 ! [Pa,Va_1,Ta,U,S] : hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,block_list_char(Va_1,Ta,val_list_char(U)),S),val_list_char(U)),S)) ). % 0.54/0.90 % 0.54/0.90 fof(fact_162_empty__upd__none,axiom, % 0.54/0.90 ! [X_1,X] : hAPP_l207779698on_val(fun_up1149430426on_val(cOMBK_1097134891t_char(none_val),X_1,none_val),X) = none_val ). % 0.54/0.90 % 0.54/0.90 fof(fact_163_empty__upd__none,axiom, % 0.54/0.90 ! [X_1,X] : hAPP_l512744617ion_ty(fun_up424764369ion_ty(cOMBK_1294242658t_char(none_ty),X_1,none_ty),X) = none_ty ). % 0.54/0.90 % 0.54/0.90 fof(fact_164_redp__redsp_OBlockRedSome,axiom, % 0.54/0.90 ! [Ta,Va,Pa,Eb,Hb,Lb,Va_1,E_b,H_b,L_b] : % 0.54/0.90 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,Eb,hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),fun_up1149430426on_val(Lb,Va_1,none_val))),E_b),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),L_b))) % 0.54/0.90 => ( hAPP_l207779698on_val(L_b,Va_1) = some_val(Va) % 0.54/0.90 => ( ~ hBOOL(assigned(Va_1,Eb)) % 0.54/0.90 => hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,block_list_char(Va_1,Ta,Eb),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,Hb),Lb)),block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(Va)),E_b))),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,H_b),fun_up1149430426on_val(L_b,Va_1,hAPP_l207779698on_val(Lb,Va_1))))) ) ) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_165_redp__red__eq,axiom, % 0.54/0.90 ! [Pa,X,Xa,Xb,Xc] : % 0.54/0.90 ( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,X,Xa),Xb),Xc)) % 0.54/0.90 <=> hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,X),Xa)),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,Xb),Xc)),red(Pa))) ) ). % 0.54/0.90 % 0.54/0.90 fof(fact_166_redp__redsp_ORedInitBlock,axiom, % 0.54/0.90 ! [Pa,Va_1,Ta,Va,U,S] : hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(redp(Pa,block_list_char(Va_1,Ta,seq_list_char(lAss_list_char(Va_1,val_list_char(Va)),val_list_char(U))),S),val_list_char(U)),S)) ). % 0.54/0.90 % 0.54/0.90 %----Helper facts (31) % 0.54/0.90 fof(help_fconj_1_1_U,axiom, % 0.54/0.90 ! [Q,P] : % 0.54/0.90 ( ~ hBOOL(P) % 0.54/0.90 | ~ hBOOL(Q) % 0.54/0.90 | hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fconj,P),Q)) ) ). % 0.54/0.90 % 0.54/0.90 fof(help_fconj_2_1_U,axiom, % 0.54/0.90 ! [P,Q] : % 0.54/0.90 ( ~ hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fconj,P),Q)) % 0.54/0.90 | hBOOL(P) ) ). % 0.54/0.90 % 0.54/0.90 fof(help_fconj_3_1_U,axiom, % 0.54/0.90 ! [P,Q] : % 0.54/0.90 ( ~ hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fconj,P),Q)) % 0.54/0.90 | hBOOL(Q) ) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBK_1_1_COMBK_000tc__Option__Ooption_Itc__Type__Oty_J_000tc__List__Olist_,axiom, % 0.54/0.90 ! [P,Q] : hAPP_l512744617ion_ty(cOMBK_1294242658t_char(P),Q) = P ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBK_1_1_COMBK_000tc__Option__Ooption_Itc__Value__Oval_J_000tc__List__Olis,axiom, % 0.54/0.90 ! [P,Q] : hAPP_l207779698on_val(cOMBK_1097134891t_char(P),Q) = P ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__List__O,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1033709212l_bool(hAPP_f1074020887l_bool(hAPP_f1863694447l_bool(cOMBB_383678192on_val,P),Q),R) = hAPP_bool_bool(P,hAPP_f1033709212l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBC_1_1_COMBC_000tc__fun_Itc__List__Olist_Itc__String__Ochar_J_Mtc__Optio,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1033709212l_bool(hAPP_f603925568l_bool(hAPP_f181262431l_bool(cOMBC_832625297y_bool,P),Q),R) = hAPP_f1001225811y_bool(hAPP_f2060496320y_bool(P,R),Q) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1145256474l_bool(hAPP_f1452292669l_bool(hAPP_f1977633121l_bool(cOMBB_1303934920on_val,P),Q),R) = hAPP_b589554111l_bool(P,hAPP_f61040418l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__prod_Itc__fun_It,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P159683425l_bool(hAPP_f2134824737l_bool(hAPP_f1308714617l_bool(cOMBB_338347573on_val,P),Q),R) = hAPP_bool_bool(P,hAPP_P159683425l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__prod_Itc__Expr__,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P1708370145l_bool(hAPP_f926562337l_bool(hAPP_f1560238713l_bool(cOMBB_672625589on_val,P),Q),R) = hAPP_bool_bool(P,hAPP_P1708370145l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1175813647l_bool(hAPP_f550652027l_bool(hAPP_f838396643l_bool(cOMBC_2027949654l_bool,P),Q),R) = hAPP_f603925568l_bool(hAPP_f1617787571l_bool(P,R),Q) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1033709212l_bool(hAPP_f1008932791l_bool(hAPP_f2057883639l_bool(cOMBB_1750801836on_val,P),Q),R) = hAPP_P159683425l_bool(P,hAPP_f1727192346on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1175813647l_bool(hAPP_f555424277l_bool(hAPP_f1734879897l_bool(cOMBB_1522540928on_val,P),Q),R) = hAPP_f1074020887l_bool(P,hAPP_f1175813647l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1175813647l_bool(cOMBS_570216337l_bool(P,Q),R) = hAPP_f1074020887l_bool(hAPP_f1492320500l_bool(P,R),hAPP_f1175813647l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1033709212l_bool(hAPP_f318082871l_bool(hAPP_f1233687287l_bool(cOMBB_171276332on_val,P),Q),R) = hAPP_P1708370145l_bool(P,hAPP_f1926378906on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Obool_J_000tc__fun_Itc,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1492320500l_bool(hAPP_f1523875321l_bool(hAPP_f592397849l_bool(cOMBB_1718333400on_val,P),Q),R) = hAPP_f1863694447l_bool(P,hAPP_f1145256474l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_002,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1617787571l_bool(hAPP_f857351829l_bool(hAPP_f348318673l_bool(cOMBB_1518282696on_val,P),Q),R) = hAPP_f181262431l_bool(P,hAPP_f1213370163y_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It_003,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P159683425l_bool(hAPP_f1301559543l_bool(hAPP_f1825030711l_bool(cOMBB_877741809on_val,P),Q),R) = hAPP_P159683425l_bool(P,hAPP_P1776198677on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O_004,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P159683425l_bool(hAPP_f489055607l_bool(hAPP_f10074679l_bool(cOMBB_1759207793on_val,P),Q),R) = hAPP_P1708370145l_bool(P,hAPP_P604205461on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It_005,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P1708370145l_bool(hAPP_f1712766199l_bool(hAPP_f881985847l_bool(cOMBB_1083177073on_val,P),Q),R) = hAPP_P159683425l_bool(P,hAPP_P789556885on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__O,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_e1833980889l_bool(hAPP_f546724245l_bool(hAPP_f917296015l_bool(cOMBB_740252943t_char,P),Q),R) = hAPP_f2134824737l_bool(P,hAPP_e1833980889l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_006,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1175813647l_bool(hAPP_f1363667773l_bool(hAPP_f1050935001l_bool(cOMBB_1153617344on_val,P),Q),R) = hAPP_f1008932791l_bool(P,hAPP_f1849790461on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_007,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1175813647l_bool(hAPP_f850751421l_bool(hAPP_f399538905l_bool(cOMBB_1466889536on_val,P),Q),R) = hAPP_f318082871l_bool(P,hAPP_f1840640125on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc_,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1033709212l_bool(hAPP_f524589473l_bool(hAPP_f2052660463l_bool(cOMBB_1292453606on_val,P),Q),R) = hAPP_P282169671l_bool(P,hAPP_f602593190on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__O_008,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_e1833980889l_bool(hAPP_f653692369l_bool(hAPP_f516738477l_bool(cOMBB_819439237t_char,P),Q),R) = hAPP_f1301559543l_bool(P,hAPP_e108155315on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__O_009,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_e1833980889l_bool(hAPP_f439412817l_bool(hAPP_f1725502637l_bool(cOMBB_1027621637t_char,P),Q),R) = hAPP_f489055607l_bool(P,hAPP_e1659493427on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__010,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P1708370145l_bool(hAPP_f204771371l_bool(hAPP_f365540729l_bool(cOMBB_1466662571on_val,P),Q),R) = hAPP_P282169671l_bool(P,hAPP_P1886180715on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P1116729363l_bool(hAPP_f641257349l_bool(hAPP_f2032347769l_bool(cOMBB_466903633on_val,P),Q),R) = hAPP_f926562337l_bool(P,hAPP_P1116729363l_bool(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__fun_Itc__List__Olist_Itc__String__Ochar_J_M_011,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_f1175813647l_bool(hAPP_f927043595l_bool(hAPP_f1043869573l_bool(cOMBB_1259202826on_val,P),Q),R) = hAPP_f524589473l_bool(P,hAPP_f600512025on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc___012,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P1116729363l_bool(hAPP_f1241216909l_bool(hAPP_f1438732387l_bool(cOMBB_635947099on_val,P),Q),R) = hAPP_f1712766199l_bool(P,hAPP_P2083594489on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 fof(help_COMBB_1_1_COMBB_000tc__fun_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc___013,axiom, % 0.54/0.90 ! [P,Q,R] : hAPP_P1116729363l_bool(hAPP_f1342895119l_bool(hAPP_f639265145l_bool(cOMBB_364363975on_val,P),Q),R) = hAPP_f204771371l_bool(P,hAPP_P1870962205on_val(Q,R)) ). % 0.54/0.90 % 0.54/0.90 %----Conjectures (1) % 0.54/0.90 fof(conj_0,conjecture, % 0.54/0.90 hBOOL(member773094996on_val(hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,some_val(v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a))),red(p))) ). % 0.54/0.90 % 0.54/0.90 %------------------------------------------------------------------------------ % 0.54/0.90 %------------------------------------------- % 0.54/0.90 % Proof found % 0.54/0.90 % SZS status Theorem for theBenchmark % 0.54/0.90 % SZS output start Proof % 0.54/0.90 %ClaNum:768(EqnAxiom:478) % 0.54/0.90 %VarNum:1851(SingletonVarNum:822) % 0.54/0.90 %MaxLitNum:4 % 0.54/0.90 %MaxfuncDepth:7 % 0.54/0.90 %SharedTerms:103 % 0.54/0.90 %goalClause: 570 % 0.54/0.90 %singleGoalClaCount:1 % 0.54/0.90 [479]E(a1,a278) % 0.54/0.90 [480]E(a2,a282) % 0.54/0.90 [481]E(a277,a279) % 0.54/0.90 [482]E(f4(a3,a285),f286(a298)) % 0.54/0.90 [485]P1(f302(a299,a262)) % 0.54/0.90 [553]P1(f267(f159(f155(a275,f165(f164(a270,a44),f180(f179(a287,a257),f101(a265,a285,f286(a296))))),f165(f164(a270,a45),f180(f179(a287,a258),a3))),f290(a262))) % 0.54/0.90 [570]~P1(f267(f159(f155(a275,f165(f164(a270,a44),f180(f179(a287,a257),f101(a265,a285,f286(a296))))),f165(f164(a270,a45),f180(f179(a287,a258),a3))),f290(a262))) % 0.54/0.90 [542]P1(f36(f293(a262,a43),f180(f179(a287,a257),a265))) % 0.54/0.90 [550]P1(f301(a262,a257,a43,f13(a285,a294,f288(f259(a285,f300(a296)),a44)),a295)) % 0.54/0.90 [497]E(f180(f179(a287,f37(x4971)),f84(x4971)),x4971) % 0.54/0.90 [498]E(f180(f179(a287,f85(x4981)),f100(x4981)),x4981) % 0.54/0.90 [499]E(f165(f164(a270,f38(x4991)),f82(x4991)),x4991) % 0.54/0.90 [500]E(f165(f164(a270,f86(x5001)),f99(x5001)),x5001) % 0.54/0.90 [501]E(f159(f155(a275,f39(x5011)),f81(x5011)),x5011) % 0.54/0.90 [502]E(f159(f155(a275,f87(x5021)),f98(x5021)),x5021) % 0.54/0.90 [537]E(f165(f164(a270,f41(x5371)),f180(f179(a287,f66(x5371)),f67(x5371))),x5371) % 0.54/0.90 [538]E(f159(f155(a275,f42(x5381)),f165(f164(a270,f63(x5381)),f65(x5381))),x5381) % 0.54/0.90 [539]E(f223(a1,f193(f185(a15,f211(a8,x5391)),a287)),x5391) % 0.54/0.90 [540]E(f249(a277,f194(f248(a24,f227(a16,x5401)),a275)),x5401) % 0.54/0.90 [541]E(f217(a2,f233(f204(a12,f177(a23,x5411)),a270)),x5411) % 0.54/0.90 [545]E(f159(f155(a275,f102(x5451)),f165(f164(a270,f116(x5451)),f180(f179(a287,f127(x5451)),f138(x5451)))),x5451) % 0.54/0.90 [486]P2(f6(x4861,x4862)) % 0.54/0.90 [487]P2(f302(x4871,x4872)) % 0.54/0.90 [488]P2(f34(x4881,x4882)) % 0.54/0.90 [489]P2(f175(x4891,x4892)) % 0.54/0.90 [490]P2(f178(x4901,x4902)) % 0.54/0.90 [491]P2(f35(x4911,x4912)) % 0.54/0.90 [492]P2(f36(x4921,x4922)) % 0.54/0.90 [493]P2(f154(x4931,x4932)) % 0.54/0.90 [494]P2(f263(x4941,x4942)) % 0.54/0.90 [495]P2(f264(x4951,x4952)) % 0.54/0.90 [496]P2(f267(x4961,x4962)) % 0.54/0.90 [507]P1(f303(x5071,x5072,x5072)) % 0.54/0.90 [483]E(f4(f5(x4831),x4832),x4831) % 0.54/0.90 [484]E(f256(f33(x4841),x4842),x4841) % 0.54/0.90 [503]E(f101(x5031,x5032,f4(x5031,x5032)),x5031) % 0.54/0.90 [504]E(f150(x5041,x5042,f256(x5041,x5042)),x5041) % 0.54/0.90 [510]E(f4(f101(f5(a268),x5101,a268),x5102),a268) % 0.54/0.90 [511]E(f256(f150(f33(a269),x5111,a269),x5112),a269) % 0.54/0.90 [506]P2(f303(x5061,x5062,x5063)) % 0.54/0.90 [556]~E(f300(x5561),f259(x5562,x5563)) % 0.54/0.90 [557]~E(f300(x5571),f288(x5572,x5573)) % 0.54/0.90 [558]~E(f259(x5581,x5582),f300(x5583)) % 0.54/0.90 [559]~E(f288(x5591,x5592),f300(x5593)) % 0.54/0.90 [505]E(f183(f181(x5051,x5052),f182(x5053,x5052)),f182(f40(x5051,x5053),x5052)) % 0.54/0.90 [508]E(f4(f101(x5081,x5082,x5083),x5082),x5083) % 0.54/0.90 [509]E(f256(f150(x5091,x5092,x5093),x5092),x5093) % 0.54/0.90 [568]~E(f4(f101(x5681,x5682,f286(x5683)),f46(x5681,x5682,x5683)),a268) % 0.54/0.90 [569]~E(f256(f150(x5691,x5692,f292(x5693)),f53(x5691,x5692,x5693)),a269) % 0.54/0.90 [512]E(f175(f183(f210(a7,x5121),x5122),x5123),f167(x5121,f175(x5122,x5123))) % 0.54/0.90 [513]E(f175(f176(f211(a8,x5131),x5132),x5133),f36(x5131,f180(x5132,x5133))) % 0.54/0.90 [514]E(f175(f220(f187(a9,x5141),x5142),x5143),f35(x5141,f212(x5142,x5143))) % 0.54/0.90 [515]E(f175(f226(f213(a10,x5151),x5152),x5153),f154(x5151,f237(x5152,x5153))) % 0.54/0.90 [516]E(f35(f244(f198(a25,x5161),x5162),x5163),f167(x5161,f35(x5162,x5163))) % 0.54/0.90 [517]E(f35(f201(f245(a11,x5171),x5172),x5173),f36(x5171,f168(x5172,x5173))) % 0.54/0.90 [518]E(f35(f214(f227(a16,x5181),x5182),x5183),f154(x5181,f159(x5182,x5183))) % 0.54/0.90 [519]E(f36(f221(f189(a22,x5191),x5192),x5193),f167(x5191,f36(x5192,x5193))) % 0.54/0.90 [520]E(f36(f190(f205(a28,x5201),x5202),x5203),f36(x5201,f156(x5202,x5203))) % 0.54/0.90 [521]E(f36(f229(f177(a23,x5211),x5212),x5213),f35(x5211,f165(x5212,x5213))) % 0.54/0.90 [522]E(f182(f246(f230(a18,x5221),x5222),x5223),f220(x5221,f209(x5222,x5223))) % 0.54/0.90 [523]E(f182(f255(f184(a14,x5231),x5232),x5233),f226(x5231,f238(x5232,x5233))) % 0.54/0.90 [524]E(f182(f239(f206(a19,x5241),x5242),x5243),f183(x5241,f182(x5242,x5243))) % 0.54/0.90 [525]E(f182(f193(f185(a15,x5251),x5252),x5253),f176(x5251,f179(x5252,x5253))) % 0.54/0.90 [526]E(f151(f191(f196(a26,x5261),x5262),x5263),f201(x5261,f160(x5262,x5263))) % 0.54/0.90 [527]E(f151(f247(f215(a27,x5271),x5272),x5273),f244(x5271,f151(x5272,x5273))) % 0.54/0.90 [528]E(f151(f194(f248(a24,x5281),x5282),x5283),f214(x5281,f155(x5282,x5283))) % 0.54/0.90 [529]E(f172(f250(f236(a29,x5291),x5292),x5293),f190(x5291,f171(x5292,x5293))) % 0.54/0.90 [530]E(f172(f240(f254(a30,x5301),x5302),x5303),f221(x5301,f172(x5302,x5303))) % 0.54/0.90 [531]E(f172(f233(f204(a12,x5311),x5312),x5313),f229(x5311,f164(x5312,x5313))) % 0.54/0.90 [532]E(f186(f197(f216(a17,x5321),x5322),x5323),f170(x5321,f178(x5322,x5323))) % 0.54/0.90 [533]E(f202(f253(f228(a20,x5331),x5332),x5333),f207(x5331,f188(x5332,x5333))) % 0.54/0.90 [534]E(f181(f199(f242(a21,x5341),x5342),x5343),f210(x5341,f186(x5342,x5343))) % 0.54/0.90 [535]E(f175(f243(f207(a31,x5351),x5352),x5353),f34(f222(x5351,x5353),x5352)) % 0.54/0.90 [536]E(f182(f241(f251(a32,x5361),x5362),x5363),f243(f202(x5361,x5363),x5362)) % 0.54/0.90 [561]~E(f288(x5611,x5612),f259(x5613,x5614)) % 0.54/0.90 [562]~E(f300(x5621),f13(x5622,x5623,x5624)) % 0.54/0.90 [563]~E(f13(x5631,x5632,x5633),f300(x5634)) % 0.54/0.90 [543]E(f101(f101(x5431,x5432,x5433),x5432,x5434),f101(x5431,x5432,x5434)) % 0.54/0.90 [544]E(f150(f150(x5441,x5442,x5443),x5442,x5444),f150(x5441,x5442,x5444)) % 0.54/0.90 [548]P1(f267(f159(f155(a275,f165(f164(a270,f288(f300(x5481),x5482)),x5483)),f165(f164(a270,x5482),x5483)),f290(x5484))) % 0.54/0.90 [546]P1(f36(f172(f289(x5461,f288(f300(x5462),x5463),x5464),x5463),x5464)) % 0.54/0.90 [549]P2(f301(x5491,x5492,x5493,x5494,x5495)) % 0.54/0.90 [564]~E(f259(x5641,x5642),f13(x5643,x5644,x5645)) % 0.54/0.90 [565]~E(f288(x5651,x5652),f13(x5653,x5654,x5655)) % 0.54/0.90 [566]~E(f13(x5661,x5662,x5663),f259(x5664,x5665)) % 0.54/0.90 [567]~E(f13(x5671,x5672,x5673),f288(x5674,x5675)) % 0.54/0.90 [552]P1(f267(f159(f155(a275,f165(f164(a270,f13(x5521,x5522,f300(x5523))),x5524)),f165(f164(a270,f300(x5523)),x5524)),f290(x5525))) % 0.54/0.90 [554]P1(f267(f159(f155(a275,f165(f164(a270,f259(x5541,f300(x5542))),f180(f179(a287,x5543),x5544))),f165(f164(a270,f300(a297)),f180(f179(a287,x5543),f101(x5544,x5541,f286(x5542))))),f290(x5545))) % 0.54/0.90 [547]P1(f36(f172(f289(x5471,f13(x5472,x5473,f300(x5474)),x5475),f300(x5474)),x5475)) % 0.54/0.90 [555]P1(f267(f159(f155(a275,f165(f164(a270,f13(x5551,x5552,f288(f259(x5551,f300(x5553)),f300(x5554)))),x5555)),f165(f164(a270,f300(x5554)),x5555)),f290(x5556))) % 0.54/0.90 [551]P1(f36(f172(f289(x5511,f13(x5512,x5513,f288(f259(x5512,f300(x5514)),f300(x5515))),x5516),f300(x5515)),x5516)) % 0.54/0.90 [571]E(x5711,x5712)+~E(f300(x5711),f300(x5712)) % 0.54/0.90 [572]~P2(x5722)+P2(f167(x5721,x5722)) % 0.54/0.90 [577]~P1(f263(x5772,x5771))+P1(f35(x5771,x5772)) % 0.54/0.90 [578]~P1(f264(x5782,x5781))+P1(f36(x5781,x5782)) % 0.54/0.90 [579]~P1(f267(x5792,x5791))+P1(f154(x5791,x5792)) % 0.54/0.90 [580]~P1(f35(x5802,x5801))+P1(f263(x5801,x5802)) % 0.54/0.90 [581]~P1(f36(x5812,x5811))+P1(f264(x5811,x5812)) % 0.54/0.90 [582]~P1(f154(x5822,x5821))+P1(f267(x5821,x5822)) % 0.54/0.90 [604]P1(x6041)+~P1(f167(f170(a149,x6042),x6041)) % 0.54/0.90 [605]P1(x6051)+~P1(f167(f170(a149,x6051),x6052)) % 0.54/0.90 [623]E(f180(f179(a287,f103(x6231,x6232)),f109(x6231,x6232)),x6232)+P1(f36(f223(a1,x6231),x6232)) % 0.54/0.90 [624]E(f165(f164(a270,f104(x6241,x6242)),f108(x6241,x6242)),x6242)+P1(f35(f217(a2,x6241),x6242)) % 0.54/0.90 [625]E(f159(f155(a275,f105(x6251,x6252)),f106(x6251,x6252)),x6252)+P1(f154(f249(a277,x6251),x6252)) % 0.54/0.90 [630]E(f180(f179(a287,f110(x6301,x6302)),f115(x6301,x6302)),x6302)+~P1(f36(f223(a1,x6301),x6302)) % 0.54/0.90 [631]E(f165(f164(a270,f111(x6311,x6312)),f114(x6311,x6312)),x6312)+~P1(f35(f217(a2,x6311),x6312)) % 0.54/0.90 [632]E(f159(f155(a275,f112(x6321,x6322)),f113(x6321,x6322)),x6322)+~P1(f154(f249(a277,x6321),x6322)) % 0.54/0.90 [661]P1(f175(f182(x6611,f110(x6611,x6612)),f115(x6611,x6612)))+~P1(f36(f223(a1,x6611),x6612)) % 0.54/0.90 [662]P1(f35(f151(x6621,f112(x6621,x6622)),f113(x6621,x6622)))+~P1(f154(f249(a277,x6621),x6622)) % 0.54/0.90 [663]P1(f36(f172(x6631,f111(x6631,x6632)),f114(x6631,x6632)))+~P1(f35(f217(a2,x6631),x6632)) % 0.54/0.90 [677]~P1(f36(f172(x6771,f104(x6771,x6772)),f108(x6771,x6772)))+P1(f35(f217(a2,x6771),x6772)) % 0.54/0.90 [678]~P1(f175(f182(x6781,f103(x6781,x6782)),f109(x6781,x6782)))+P1(f36(f223(a1,x6781),x6782)) % 0.54/0.90 [679]~P1(f35(f151(x6791,f105(x6791,x6792)),f106(x6791,x6792)))+P1(f154(f249(a277,x6791),x6792)) % 0.54/0.90 [640]~P1(f35(x6401,x6402))+P1(f35(x6401,f165(f164(a270,f88(x6401)),f92(x6401)))) % 0.54/0.90 [641]~P1(f36(x6411,x6412))+P1(f36(x6411,f180(f179(a287,f93(x6411)),f95(x6411)))) % 0.54/0.90 [642]~P1(f154(x6421,x6422))+P1(f154(x6421,f159(f155(a275,f89(x6421)),f90(x6421)))) % 0.54/0.90 [664]P1(f35(x6641,x6642))+~P1(f35(x6641,f165(f164(a270,f59(x6641)),f60(x6641)))) % 0.54/0.90 [665]P1(f36(x6651,x6652))+~P1(f36(x6651,f180(f179(a287,f61(x6651)),f62(x6651)))) % 0.54/0.90 [666]P1(f154(x6661,x6662))+~P1(f154(x6661,f159(f155(a275,f56(x6661)),f57(x6661)))) % 0.54/0.90 [733]P1(f35(x7331,x7332))+~P1(f35(x7331,f165(f164(a270,f69(x7332,x7331)),f180(f179(a287,f73(x7332,x7331)),f74(x7332,x7331))))) % 0.54/0.90 [734]P1(f154(x7341,x7342))+~P1(f154(x7341,f159(f155(a275,f70(x7342,x7341)),f165(f164(a270,f71(x7342,x7341)),f72(x7342,x7341))))) % 0.54/0.90 [754]P1(f154(x7541,x7542))+~P1(f154(x7541,f159(f155(a275,f75(x7542,x7541)),f165(f164(a270,f83(x7542,x7541)),f180(f179(a287,f96(x7542,x7541)),f107(x7542,x7541)))))) % 0.54/0.90 [584]~E(f4(x5841,x5842),x5843)+E(f101(x5841,x5842,x5843),x5841) % 0.54/0.90 [586]~E(f256(x5861,x5862),x5863)+E(f150(x5861,x5862,x5863),x5861) % 0.54/0.90 [590]~E(f101(x5901,x5902,x5903),x5901)+E(f4(x5901,x5902),x5903) % 0.54/0.90 [591]~E(f150(x5911,x5912,x5913),x5911)+E(f256(x5911,x5912),x5913) % 0.54/0.90 [637]~P1(f35(x6371,f54(x6371)))+P1(f35(x6371,f165(f164(a270,x6372),x6373))) % 0.54/0.90 [638]~P1(f36(x6381,f58(x6381)))+P1(f36(x6381,f180(f179(a287,x6382),x6383))) % 0.54/0.90 [639]~P1(f154(x6391,f55(x6391)))+P1(f154(x6391,f159(f155(a275,x6392),x6393))) % 0.54/0.90 [643]P1(f35(x6431,f94(x6431)))+~P1(f35(x6431,f165(f164(a270,x6432),x6433))) % 0.54/0.90 [644]P1(f36(x6441,f97(x6441)))+~P1(f36(x6441,f180(f179(a287,x6442),x6443))) % 0.54/0.90 [645]P1(f154(x6451,f91(x6451)))+~P1(f154(x6451,f159(f155(a275,x6452),x6453))) % 0.54/0.90 [651]~P1(f36(f172(x6511,x6512),x6513))+P1(f35(f217(a2,x6511),f165(f164(a270,x6512),x6513))) % 0.54/0.90 [652]~P1(f175(f182(x6521,x6522),x6523))+P1(f36(f223(a278,x6521),f180(f179(a287,x6522),x6523))) % 0.54/0.90 [656]~P1(f175(f182(x6561,x6562),x6563))+P1(f36(f223(a1,x6561),f180(f179(a287,x6562),x6563))) % 0.54/0.90 [660]~P1(f35(f151(x6601,x6602),x6603))+P1(f154(f249(a277,x6601),f159(f155(a275,x6602),x6603))) % 0.54/0.90 [667]P1(f175(f182(x6671,x6672),x6673))+~P1(f36(f223(a278,x6671),f180(f179(a287,x6672),x6673))) % 0.54/0.90 [670]P1(f175(f182(x6701,x6702),x6703))+~P1(f36(f223(a1,x6701),f180(f179(a287,x6702),x6703))) % 0.54/0.90 [673]P1(f35(f151(x6731,x6732),x6733))+~P1(f154(f249(a277,x6731),f159(f155(a275,x6732),x6733))) % 0.54/0.90 [676]P1(f36(f172(x6761,x6762),x6763))+~P1(f35(f217(a2,x6761),f165(f164(a270,x6762),x6763))) % 0.54/0.90 [681]E(f180(f179(a287,f139(x6811,x6812,x6813)),f140(x6811,x6812,x6813)),x6813)+P1(f264(x6811,f161(f192(a271,x6812),x6813))) % 0.54/0.90 [682]E(f180(f179(a287,f141(x6821,x6822,x6823)),f142(x6821,x6822,x6823)),x6823)+P1(f263(x6821,f153(f252(a283,x6822),x6823))) % 0.54/0.90 [683]E(f165(f164(a270,f128(x6831,x6832,x6833)),f135(x6831,x6832,x6833)),x6833)+P1(f264(x6831,f166(f234(a280,x6832),x6833))) % 0.54/0.90 [684]E(f165(f164(a270,f136(x6841,x6842,x6843)),f137(x6841,x6842,x6843)),x6843)+P1(f263(x6841,f151(f208(a276,x6842),x6843))) % 0.54/0.90 [685]E(f159(f155(a275,f129(x6851,x6852,x6853)),f132(x6851,x6852,x6853)),x6853)+P1(f264(x6851,f158(f235(a284,x6852),x6853))) % 0.54/0.90 [686]E(f159(f155(a275,f133(x6861,x6862,x6863)),f134(x6861,x6862,x6863)),x6863)+P1(f263(x6861,f169(f203(a281,x6862),x6863))) % 0.54/0.90 [687]E(f180(f179(a287,f117(x6871,x6872,x6873)),f126(x6871,x6872,x6873)),x6873)+~P1(f264(x6871,f161(f192(a271,x6872),x6873))) % 0.54/0.90 [688]E(f180(f179(a287,f130(x6881,x6882,x6883)),f131(x6881,x6882,x6883)),x6883)+~P1(f263(x6881,f153(f252(a283,x6882),x6883))) % 0.54/0.90 [689]E(f180(f179(a287,f47(x6891,x6892,x6893)),f48(x6891,x6892,x6893)),x6893)+~P1(f167(x6891,f36(f223(a1,x6892),x6893))) % 0.54/0.90 [690]E(f165(f164(a270,f118(x6901,x6902,x6903)),f123(x6901,x6902,x6903)),x6903)+~P1(f264(x6901,f166(f234(a280,x6902),x6903))) % 0.54/0.90 [691]E(f165(f164(a270,f124(x6911,x6912,x6913)),f125(x6911,x6912,x6913)),x6913)+~P1(f263(x6911,f151(f208(a276,x6912),x6913))) % 0.54/0.90 [692]E(f165(f164(a270,f49(x6921,x6922,x6923)),f52(x6921,x6922,x6923)),x6923)+~P1(f167(x6921,f35(f217(a2,x6922),x6923))) % 0.54/0.90 [693]E(f159(f155(a275,f119(x6931,x6932,x6933)),f120(x6931,x6932,x6933)),x6933)+~P1(f264(x6931,f158(f235(a284,x6932),x6933))) % 0.54/0.90 [694]E(f159(f155(a275,f121(x6941,x6942,x6943)),f122(x6941,x6942,x6943)),x6943)+~P1(f263(x6941,f169(f203(a281,x6942),x6943))) % 0.89/0.91 [695]E(f159(f155(a275,f50(x6951,x6952,x6953)),f51(x6951,x6952,x6953)),x6953)+~P1(f167(x6951,f154(f249(a277,x6952),x6953))) % 0.89/0.91 [719]P1(f167(x7191,f175(f182(x7192,f47(x7191,x7192,x7193)),f48(x7191,x7192,x7193))))+~P1(f167(x7191,f36(f223(a1,x7192),x7193))) % 0.89/0.91 [720]P1(f167(x7201,f35(f151(x7202,f50(x7201,x7202,x7203)),f51(x7201,x7202,x7203))))+~P1(f167(x7201,f154(f249(a277,x7202),x7203))) % 0.89/0.91 [721]P1(f167(x7211,f36(f172(x7212,f49(x7211,x7212,x7213)),f52(x7211,x7212,x7213))))+~P1(f167(x7211,f35(f217(a2,x7212),x7213))) % 0.89/0.91 [722]P1(f263(x7221,f151(f162(x7222,f121(x7221,x7222,x7223)),f122(x7221,x7222,x7223))))+~P1(f263(x7221,f169(f203(a281,x7222),x7223))) % 0.89/0.91 [723]P1(f263(x7231,f153(f173(x7232,f124(x7231,x7232,x7233)),f125(x7231,x7232,x7233))))+~P1(f263(x7231,f151(f208(a276,x7232),x7233))) % 0.89/0.91 [724]P1(f263(x7241,f218(f224(x7242,f130(x7241,x7242,x7243)),f131(x7241,x7242,x7243))))+~P1(f263(x7241,f153(f252(a283,x7242),x7243))) % 0.89/0.91 [725]P1(f264(x7251,f166(f152(x7252,f119(x7251,x7252,x7253)),f120(x7251,x7252,x7253))))+~P1(f264(x7251,f158(f235(a284,x7252),x7253))) % 0.89/0.91 [726]P1(f264(x7261,f161(f174(x7262,f118(x7261,x7262,x7263)),f123(x7261,x7262,x7263))))+~P1(f264(x7261,f166(f234(a280,x7262),x7263))) % 0.89/0.91 [727]P1(f264(x7271,f231(f225(x7272,f117(x7271,x7272,x7273)),f126(x7271,x7272,x7273))))+~P1(f264(x7271,f161(f192(a271,x7272),x7273))) % 0.89/0.91 [742]~P1(f263(x7421,f153(f173(x7422,f136(x7421,x7422,x7423)),f137(x7421,x7422,x7423))))+P1(f263(x7421,f151(f208(a276,x7422),x7423))) % 0.89/0.91 [743]~P1(f263(x7431,f151(f162(x7432,f133(x7431,x7432,x7433)),f134(x7431,x7432,x7433))))+P1(f263(x7431,f169(f203(a281,x7432),x7433))) % 0.89/0.91 [744]~P1(f263(x7441,f218(f224(x7442,f141(x7441,x7442,x7443)),f142(x7441,x7442,x7443))))+P1(f263(x7441,f153(f252(a283,x7442),x7443))) % 0.89/0.91 [745]~P1(f264(x7451,f161(f174(x7452,f128(x7451,x7452,x7453)),f135(x7451,x7452,x7453))))+P1(f264(x7451,f166(f234(a280,x7452),x7453))) % 0.89/0.91 [746]~P1(f264(x7461,f166(f152(x7462,f129(x7461,x7462,x7463)),f132(x7461,x7462,x7463))))+P1(f264(x7461,f158(f235(a284,x7462),x7463))) % 0.89/0.91 [747]~P1(f264(x7471,f231(f225(x7472,f139(x7471,x7472,x7473)),f140(x7471,x7472,x7473))))+P1(f264(x7471,f161(f192(a271,x7472),x7473))) % 0.89/0.91 [728]~P1(f36(f223(a1,x7281),f168(f200(a272,x7282),x7283)))+P1(f35(f217(a2,f250(f236(a29,f205(a28,f223(a1,x7281))),x7282)),x7283)) % 0.89/0.91 [729]~P1(f35(f217(a2,x7291),f165(f195(a291,x7292),x7293)))+P1(f36(f223(a1,f246(f230(a18,f187(a9,f217(a2,x7291))),x7292)),x7293)) % 0.89/0.91 [730]~P1(f154(f249(a277,x7301),f163(f219(a273,x7302),x7303)))+P1(f36(f223(a1,f255(f184(a14,f213(a10,f249(a277,x7301))),x7302)),x7303)) % 0.89/0.91 [731]~P1(f36(f223(a1,x7311),f157(f232(a274,x7312),x7313)))+P1(f154(f249(a277,f191(f196(a26,f245(a11,f223(a1,x7311))),x7312)),x7313)) % 0.89/0.91 [736]P1(x7361)+~P1(f35(f217(a2,f240(f254(a30,f189(a22,f170(a149,x7361))),x7362)),x7363)) % 0.89/0.91 [737]P1(x7371)+~P1(f36(f223(a1,f239(f206(a19,f210(a7,f170(a149,x7371))),x7372)),x7373)) % 0.89/0.91 [738]P1(x7381)+~P1(f154(f249(a277,f247(f215(a27,f198(a25,f170(a149,x7381))),x7382)),x7383)) % 0.89/0.91 [739]P1(f35(f217(a2,x7391),x7392))+~P1(f35(f217(a2,f240(f254(a30,f189(a22,f170(a149,x7393))),x7391)),x7392)) % 0.89/0.91 [740]P1(f36(f223(a1,x7401),x7402))+~P1(f36(f223(a1,f239(f206(a19,f210(a7,f170(a149,x7403))),x7401)),x7402)) % 0.89/0.91 [741]P1(f154(f249(a277,x7411),x7412))+~P1(f154(f249(a277,f247(f215(a27,f198(a25,f170(a149,x7413))),x7411)),x7412)) % 0.89/0.91 [748]P1(f35(f217(a2,x7481),f165(f195(a291,x7482),x7483)))+~P1(f36(f223(a1,f246(f230(a18,f187(a9,f217(a2,x7481))),x7482)),x7483)) % 0.89/0.91 [749]P1(f36(f223(a1,x7491),f168(f200(a272,x7492),x7493)))+~P1(f35(f217(a2,f250(f236(a29,f205(a28,f223(a1,x7491))),x7492)),x7493)) % 0.89/0.91 [750]P1(f36(f223(a1,x7501),f157(f232(a274,x7502),x7503)))+~P1(f154(f249(a277,f191(f196(a26,f245(a11,f223(a1,x7501))),x7502)),x7503)) % 0.89/0.91 [751]P1(f154(f249(a277,x7511),f163(f219(a273,x7512),x7513)))+~P1(f36(f223(a1,f255(f184(a14,f213(a10,f249(a277,x7511))),x7512)),x7513)) % 0.89/0.91 [756]~P1(f36(f293(x7561,x7562),x7563))+P1(f36(f223(a1,f40(f199(f242(a21,a7),f197(f216(a17,a149),f260(x7561))),f241(f251(a32,f253(f228(a20,a31),f266(x7561))),x7562))),x7563)) % 0.89/0.91 [761]P1(f36(f293(x7611,x7612),x7613))+~P1(f36(f223(a1,f40(f199(f242(a21,a7),f197(f216(a17,a149),f260(x7611))),f241(f251(a32,f253(f228(a20,a31),f266(x7611))),x7612))),x7613)) % 0.89/0.91 [573]E(x5731,x5732)+~E(f259(x5733,x5731),f259(x5734,x5732)) % 0.89/0.91 [574]E(x5741,x5742)+~E(f259(x5741,x5743),f259(x5742,x5744)) % 0.89/0.91 [575]E(x5751,x5752)+~E(f288(x5753,x5751),f288(x5754,x5752)) % 0.89/0.91 [576]E(x5761,x5762)+~E(f288(x5761,x5763),f288(x5762,x5764)) % 0.89/0.91 [593]E(x5931,x5932)+~E(f180(f179(a287,x5933),x5931),f180(f179(a287,x5934),x5932)) % 0.89/0.91 [595]E(x5951,x5952)+~E(f180(f179(a287,x5951),x5953),f180(f179(a287,x5952),x5954)) % 0.89/0.91 [597]E(x5971,x5972)+~E(f165(f164(a270,x5973),x5971),f165(f164(a270,x5974),x5972)) % 0.89/0.91 [599]E(x5991,x5992)+~E(f165(f164(a270,x5991),x5993),f165(f164(a270,x5992),x5994)) % 0.89/0.91 [601]E(x6011,x6012)+~E(f159(f155(a275,x6013),x6011),f159(f155(a275,x6014),x6012)) % 0.89/0.91 [603]E(x6031,x6032)+~E(f159(f155(a275,x6031),x6033),f159(f155(a275,x6032),x6034)) % 0.89/0.91 [607]~E(x6074,x6072)+E(f4(f101(x6071,x6072,x6073),x6074),x6073) % 0.89/0.91 [609]~E(x6094,x6092)+E(f256(f150(x6091,x6092,x6093),x6094),x6093) % 0.89/0.91 [612]E(x6121,x6122)+E(f4(f101(x6123,x6122,x6124),x6121),f4(x6123,x6121)) % 0.89/0.91 [615]E(x6151,x6152)+E(f256(f150(x6153,x6152,x6154),x6151),f256(x6153,x6151)) % 0.89/0.91 [699]~P1(f263(x6991,f153(f173(x6992,x6993),x6994)))+P1(f263(x6991,f151(f208(a276,x6992),f165(f164(a270,x6993),x6994)))) % 0.89/0.91 [700]~P1(f263(x7001,f151(f162(x7002,x7003),x7004)))+P1(f263(x7001,f169(f203(a281,x7002),f159(f155(a275,x7003),x7004)))) % 0.89/0.91 [701]~P1(f263(x7011,f218(f224(x7012,x7013),x7014)))+P1(f263(x7011,f153(f252(a283,x7012),f180(f179(a287,x7013),x7014)))) % 0.89/0.91 [702]~P1(f264(x7021,f161(f174(x7022,x7023),x7024)))+P1(f264(x7021,f166(f234(a280,x7022),f165(f164(a270,x7023),x7024)))) % 0.89/0.91 [703]~P1(f264(x7031,f166(f152(x7032,x7033),x7034)))+P1(f264(x7031,f158(f235(a284,x7032),f159(f155(a275,x7033),x7034)))) % 0.89/0.91 [704]~P1(f264(x7041,f231(f225(x7042,x7043),x7044)))+P1(f264(x7041,f161(f192(a271,x7042),f180(f179(a287,x7043),x7044)))) % 0.89/0.91 [626]E(x6261,x6262)+~E(f101(x6263,x6264,f286(x6261)),f101(x6265,x6264,f286(x6262))) % 0.89/0.91 [627]E(x6271,x6272)+~E(f150(x6273,x6274,f292(x6271)),f150(x6275,x6274,f292(x6272))) % 0.89/0.91 [646]E(x6461,x6462)+E(f101(f101(x6463,x6461,x6464),x6462,x6465),f101(f101(x6463,x6462,x6465),x6461,x6464)) % 0.89/0.91 [647]E(x6471,x6472)+E(f150(f150(x6473,x6471,x6474),x6472,x6475),f150(f150(x6473,x6472,x6475),x6471,x6474)) % 0.89/0.91 [732]P1(f267(f159(f155(a275,f165(f164(a270,x7321),x7322)),f165(f164(a270,x7323),x7324)),f290(x7325)))+~P1(f36(f172(f289(x7325,x7321,x7322),x7323),x7324)) % 0.89/0.91 [735]~P1(f267(f159(f155(a275,f165(f164(a270,x7352),x7353)),f165(f164(a270,x7354),x7355)),f290(x7351)))+P1(f36(f172(f289(x7351,x7352,x7353),x7354),x7355)) % 0.89/0.91 [620]E(x6201,x6202)+~E(f13(x6203,x6204,x6201),f13(x6205,x6206,x6202)) % 0.89/0.91 [621]E(x6211,x6212)+~E(f13(x6213,x6211,x6214),f13(x6215,x6212,x6216)) % 0.89/0.91 [622]E(x6221,x6222)+~E(f13(x6221,x6223,x6224),f13(x6222,x6225,x6226)) % 0.89/0.91 [752]P1(f267(f159(f155(a275,f165(f164(a270,f259(x7521,x7522)),x7523)),f165(f164(a270,f259(x7521,x7524)),x7525)),f290(x7526)))+~P1(f267(f159(f155(a275,f165(f164(a270,x7522),x7523)),f165(f164(a270,x7524),x7525)),f290(x7526))) % 0.89/0.91 [753]P1(f267(f159(f155(a275,f165(f164(a270,f288(x7531,x7532)),x7533)),f165(f164(a270,f288(x7534,x7532)),x7535)),f290(x7536)))+~P1(f267(f159(f155(a275,f165(f164(a270,x7531),x7533)),f165(f164(a270,x7534),x7535)),f290(x7536))) % 0.89/0.91 [717]~P1(f36(f172(f289(x7171,x7173,x7174),x7175),x7176))+P1(f36(f172(f289(x7171,f259(x7172,x7173),x7174),f259(x7172,x7175)),x7176)) % 0.89/0.91 [718]~P1(f36(f172(f289(x7181,x7182,x7184),x7185),x7186))+P1(f36(f172(f289(x7181,f288(x7182,x7183),x7184),f288(x7185,x7183)),x7186)) % 0.89/0.91 [758]P1(f301(x7581,x7582,x7583,f13(x7584,x7585,x7586),x7587))+~P1(f301(x7581,x7582,f150(x7583,x7584,f292(x7585)),x7586,x7587)) % 0.89/0.91 [589]~P1(x5892)+~P1(x5891)+P1(f167(f170(a149,x5891),x5892)) % 0.89/0.91 [696]E(f223(a1,x6961),x6962)+P1(f175(f182(x6961,f143(x6962,x6961)),f144(x6962,x6961)))+P1(f36(x6962,f180(f179(a287,f143(x6962,x6961)),f144(x6962,x6961)))) % 0.89/0.91 [697]E(f249(a277,x6971),x6972)+P1(f35(f151(x6971,f145(x6972,x6971)),f146(x6972,x6971)))+P1(f154(x6972,f159(f155(a275,f145(x6972,x6971)),f146(x6972,x6971)))) % 0.89/0.91 [698]E(f217(a2,x6981),x6982)+P1(f36(f172(x6981,f147(x6982,x6981)),f148(x6982,x6981)))+P1(f35(x6982,f165(f164(a270,f147(x6982,x6981)),f148(x6982,x6981)))) % 0.89/0.91 [705]E(x7051,x7052)+P1(f263(f165(f164(a270,f68(x7051,x7052)),f76(x7051,x7052)),x7051))+P1(f263(f165(f164(a270,f68(x7051,x7052)),f76(x7051,x7052)),x7052)) % 0.89/0.91 [706]E(x7061,x7062)+P1(f264(f180(f179(a287,f77(x7061,x7062)),f78(x7061,x7062)),x7061))+P1(f264(f180(f179(a287,f77(x7061,x7062)),f78(x7061,x7062)),x7062)) % 0.89/0.91 [707]E(x7071,x7072)+P1(f267(f159(f155(a275,f79(x7071,x7072)),f80(x7071,x7072)),x7071))+P1(f267(f159(f155(a275,f79(x7071,x7072)),f80(x7071,x7072)),x7072)) % 0.89/0.91 [708]E(f223(a1,x7081),x7082)+~P1(f175(f182(x7081,f143(x7082,x7081)),f144(x7082,x7081)))+~P1(f36(x7082,f180(f179(a287,f143(x7082,x7081)),f144(x7082,x7081)))) % 0.89/0.91 [709]E(f249(a277,x7091),x7092)+~P1(f35(f151(x7091,f145(x7092,x7091)),f146(x7092,x7091)))+~P1(f154(x7092,f159(f155(a275,f145(x7092,x7091)),f146(x7092,x7091)))) % 0.89/0.91 [710]E(f217(a2,x7101),x7102)+~P1(f36(f172(x7101,f147(x7102,x7101)),f148(x7102,x7101)))+~P1(f35(x7102,f165(f164(a270,f147(x7102,x7101)),f148(x7102,x7101)))) % 0.89/0.91 [711]E(x7111,x7112)+~P1(f263(f165(f164(a270,f68(x7111,x7112)),f76(x7111,x7112)),x7111))+~P1(f263(f165(f164(a270,f68(x7111,x7112)),f76(x7111,x7112)),x7112)) % 0.89/0.91 [712]E(x7121,x7122)+~P1(f264(f180(f179(a287,f77(x7121,x7122)),f78(x7121,x7122)),x7121))+~P1(f264(f180(f179(a287,f77(x7121,x7122)),f78(x7121,x7122)),x7122)) % 0.89/0.91 [713]E(x7131,x7132)+~P1(f267(f159(f155(a275,f79(x7131,x7132)),f80(x7131,x7132)),x7131))+~P1(f267(f159(f155(a275,f79(x7131,x7132)),f80(x7131,x7132)),x7132)) % 0.89/0.91 [755]~P1(f301(a262,a257,x7552,a44,x7551))+P1(f303(a262,f64(x7551,x7552),x7551))+~P1(f36(f293(a262,x7552),f180(f179(a287,a257),f101(a265,a285,f286(a296))))) % 0.89/0.91 [759]~P1(f301(a262,a257,x7591,a44,x7592))+P1(f301(a262,a258,x7591,a45,f64(x7592,x7591)))+~P1(f36(f293(a262,x7591),f180(f179(a287,a257),f101(a265,a285,f286(a296))))) % 0.89/0.91 [714]~P1(x7141)+~P1(f35(f217(a2,x7142),x7143))+P1(f35(f217(a2,f240(f254(a30,f189(a22,f170(a149,x7141))),x7142)),x7143)) % 0.89/0.91 [715]~P1(x7151)+~P1(f36(f223(a1,x7152),x7153))+P1(f36(f223(a1,f239(f206(a19,f210(a7,f170(a149,x7151))),x7152)),x7153)) % 0.89/0.91 [716]~P1(x7161)+~P1(f154(f249(a277,x7162),x7163))+P1(f154(f249(a277,f247(f215(a27,f198(a25,f170(a149,x7161))),x7162)),x7163)) % 0.89/0.91 [680]~P1(f303(x6801,x6802,x6804))+P1(f303(x6801,x6802,x6803))+~P1(f303(x6801,x6804,x6803)) % 0.89/0.91 [616]~E(x6163,x6165)+~E(x6164,x6162)+E(f4(f101(x6161,x6162,f286(x6163)),x6164),f286(x6165)) % 0.89/0.91 [617]~E(x6173,x6175)+~E(x6174,x6172)+E(f256(f150(x6171,x6172,f292(x6173)),x6174),f292(x6175)) % 0.89/0.91 [618]E(x6181,x6182)+~E(f4(x6183,x6181),f286(x6185))+E(f4(f101(x6183,x6182,f286(x6184)),x6181),f286(x6185)) % 0.89/0.91 [619]E(x6191,x6192)+~E(f256(x6193,x6191),f292(x6195))+E(f256(f150(x6193,x6192,f292(x6194)),x6191),f292(x6195)) % 0.89/0.91 [628]E(x6281,x6282)+~E(x6283,x6284)+~E(f4(f101(x6285,x6284,f286(x6281)),x6283),f286(x6282)) % 0.89/0.91 [629]E(x6291,x6292)+~E(x6293,x6294)+~E(f256(f150(x6295,x6294,f292(x6291)),x6293),f292(x6292)) % 0.89/0.91 [633]E(x6331,x6332)+E(f4(x6333,x6334),f286(x6331))+~E(f4(f101(x6333,x6335,f286(x6332)),x6334),f286(x6331)) % 0.89/0.91 [634]E(x6341,x6342)+E(f256(x6343,x6344),f292(x6341))+~E(f256(f150(x6343,x6345,f292(x6342)),x6344),f292(x6341)) % 0.89/0.91 [635]E(x6351,x6352)+E(f4(x6353,x6351),f286(x6354))+~E(f4(f101(x6353,x6352,f286(x6355)),x6351),f286(x6354)) % 0.89/0.91 [636]E(x6361,x6362)+E(f256(x6363,x6361),f292(x6364))+~E(f256(f150(x6363,x6362,f292(x6365)),x6361),f292(x6364)) % 0.89/0.91 [765]~P1(f301(x7651,x7652,x7653,x7655,x7656))+~P1(f301(x7651,x7652,x7653,x7654,x7657))+P1(f301(x7651,x7652,x7653,f288(x7654,x7655),x7656)) % 0.89/0.91 [768]~E(f4(x76810,x7681),f286(x7687))+~P1(f267(f159(f155(a275,f165(f164(a270,x7684),f180(f179(a287,x7685),f101(x7686,x7681,f286(x7683))))),f165(f164(a270,x7688),f180(f179(a287,x7689),x76810))),f290(x76811)))+P1(f267(f159(f155(a275,f165(f164(a270,f13(x7681,x7682,f288(f259(x7681,f300(x7683)),x7684))),f180(f179(a287,x7685),x7686))),f165(f164(a270,f13(x7681,x7682,f288(f259(x7681,f300(x7687)),x7688))),f180(f179(a287,x7689),f101(x76810,x7681,f4(x7686,x7681))))),f290(x76811))) % 0.89/0.91 [766]~E(f4(x76611,x7662),f286(x7668))+~P1(f36(f172(f289(x7661,x7665,f180(f179(a287,x7666),f101(x7667,x7662,f286(x7664)))),x7669),f180(f179(a287,x76610),x76611)))+P1(f36(f172(f289(x7661,f13(x7662,x7663,f288(f259(x7662,f300(x7664)),x7665)),f180(f179(a287,x7666),x7667)),f13(x7662,x7663,f288(f259(x7662,f300(x7668)),x7669))),f180(f179(a287,x76610),f101(x76611,x7662,f4(x7667,x7662))))) % 0.89/0.91 [757]P1(f36(f293(x7571,x7572),x7573))+~P1(f301(x7571,f261(x7574),x7572,x7575,x7576))+~P1(f36(f293(x7571,x7572),x7574))+~P1(f267(f159(f155(a275,f165(f164(a270,x7575),x7574)),f165(f164(a270,x7577),x7573)),f290(x7571))) % 0.89/0.91 [762]~P1(f301(x7621,x7623,x7624,x7625,x7626))+P1(f178(f260(x7621),x7622))+~P1(f178(f260(x7621),x7623))+~P1(f267(f159(f155(a275,f165(f164(a270,x7625),f180(f179(a287,x7623),x7627))),f165(f164(a270,x7628),f180(f179(a287,x7622),x7629))),f290(x7621))) % 0.89/0.91 [760]~E(f4(x7609,x7601),a268)+P1(f6(x7601,x7602))+~P1(f36(f172(f289(x7603,x7602,f180(f179(a287,x7605),f101(x7606,x7601,a268))),x7607),f180(f179(a287,x7608),x7609)))+P1(f36(f172(f289(x7603,f13(x7601,x7604,x7602),f180(f179(a287,x7605),x7606)),f13(x7601,x7604,x7607)),f180(f179(a287,x7608),f101(x7609,x7601,f4(x7606,x7601))))) % 0.89/0.91 [764]~P1(f301(x7641,x7645,x7644,x7646,x7647))+~P1(f267(f159(f155(a275,f165(f164(a270,x7646),f180(f179(a287,x7645),x7648))),f165(f164(a270,x7649),f180(f179(a287,x7642),x7643))),f290(x7641)))+P1(f34(f222(f188(f266(x7641),x7642),x7643),x7644))+~P1(f34(f222(f188(f266(x7641),x7645),x7648),x7644)) % 0.89/0.91 [767]~E(f4(x7679,x7671),f286(x7676))+P1(f6(x7671,x7672))+~P1(f267(f159(f155(a275,f165(f164(a270,x7672),f180(f179(a287,x7674),f101(x7675,x7671,a268)))),f165(f164(a270,x7677),f180(f179(a287,x7678),x7679))),f290(x76710)))+P1(f267(f159(f155(a275,f165(f164(a270,f13(x7671,x7673,x7672)),f180(f179(a287,x7674),x7675))),f165(f164(a270,f13(x7671,x7673,f288(f259(x7671,f300(x7676)),x7677))),f180(f179(a287,x7678),f101(x7679,x7671,f4(x7675,x7671))))),f290(x76710))) % 0.89/0.91 [763]~E(f4(x76310,x7631),f286(x7637))+P1(f6(x7631,x7632))+~P1(f36(f172(f289(x7633,x7632,f180(f179(a287,x7635),f101(x7636,x7631,a268))),x7638),f180(f179(a287,x7639),x76310)))+P1(f36(f172(f289(x7633,f13(x7631,x7634,x7632),f180(f179(a287,x7635),x7636)),f13(x7631,x7634,f288(f259(x7631,f300(x7637)),x7638))),f180(f179(a287,x7639),f101(x76310,x7631,f4(x7636,x7631))))) % 0.89/0.91 %EqnAxiom % 0.89/0.91 [1]E(x11,x11) % 0.89/0.91 [2]E(x22,x21)+~E(x21,x22) % 0.89/0.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.89/0.91 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43)) % 0.89/0.91 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52)) % 0.89/0.91 [6]~E(x61,x62)+E(f286(x61),f286(x62)) % 0.89/0.91 [7]~E(x71,x72)+E(f5(x71),f5(x72)) % 0.89/0.91 [8]~E(x81,x82)+E(f267(x81,x83),f267(x82,x83)) % 0.89/0.91 [9]~E(x91,x92)+E(f267(x93,x91),f267(x93,x92)) % 0.89/0.91 [10]~E(x101,x102)+E(f33(x101),f33(x102)) % 0.89/0.91 [11]~E(x111,x112)+E(f256(x111,x113),f256(x112,x113)) % 0.89/0.91 [12]~E(x121,x122)+E(f256(x123,x121),f256(x123,x122)) % 0.89/0.91 [13]~E(x131,x132)+E(f302(x131,x133),f302(x132,x133)) % 0.89/0.91 [14]~E(x141,x142)+E(f302(x143,x141),f302(x143,x142)) % 0.89/0.91 [15]~E(x151,x152)+E(f6(x151,x153),f6(x152,x153)) % 0.89/0.91 [16]~E(x161,x162)+E(f6(x163,x161),f6(x163,x162)) % 0.89/0.91 [17]~E(x171,x172)+E(f179(x171,x173),f179(x172,x173)) % 0.89/0.91 [18]~E(x181,x182)+E(f179(x183,x181),f179(x183,x182)) % 0.89/0.91 [19]~E(x191,x192)+E(f34(x191,x193),f34(x192,x193)) % 0.89/0.91 [20]~E(x201,x202)+E(f34(x203,x201),f34(x203,x202)) % 0.89/0.91 [21]~E(x211,x212)+E(f175(x211,x213),f175(x212,x213)) % 0.89/0.91 [22]~E(x221,x222)+E(f175(x223,x221),f175(x223,x222)) % 0.89/0.91 [23]~E(x231,x232)+E(f178(x231,x233),f178(x232,x233)) % 0.89/0.91 [24]~E(x241,x242)+E(f178(x243,x241),f178(x243,x242)) % 0.89/0.91 [25]~E(x251,x252)+E(f35(x251,x253),f35(x252,x253)) % 0.89/0.91 [26]~E(x261,x262)+E(f35(x263,x261),f35(x263,x262)) % 0.89/0.91 [27]~E(x271,x272)+E(f36(x271,x273),f36(x272,x273)) % 0.89/0.91 [28]~E(x281,x282)+E(f36(x283,x281),f36(x283,x282)) % 0.89/0.91 [29]~E(x291,x292)+E(f154(x291,x293),f154(x292,x293)) % 0.89/0.91 [30]~E(x301,x302)+E(f154(x303,x301),f154(x303,x302)) % 0.89/0.91 [31]~E(x311,x312)+E(f263(x311,x313),f263(x312,x313)) % 0.89/0.91 [32]~E(x321,x322)+E(f263(x323,x321),f263(x323,x322)) % 0.89/0.91 [33]~E(x331,x332)+E(f264(x331,x333),f264(x332,x333)) % 0.89/0.91 [34]~E(x341,x342)+E(f264(x343,x341),f264(x343,x342)) % 0.89/0.91 [35]~E(x351,x352)+E(f300(x351),f300(x352)) % 0.89/0.91 [36]~E(x361,x362)+E(f37(x361),f37(x362)) % 0.89/0.91 [37]~E(x371,x372)+E(f188(x371,x373),f188(x372,x373)) % 0.89/0.91 [38]~E(x381,x382)+E(f188(x383,x381),f188(x383,x382)) % 0.89/0.91 [39]~E(x391,x392)+E(f84(x391),f84(x392)) % 0.89/0.91 [40]~E(x401,x402)+E(f180(x401,x403),f180(x402,x403)) % 0.89/0.91 [41]~E(x411,x412)+E(f180(x413,x411),f180(x413,x412)) % 0.89/0.91 [42]~E(x421,x422)+E(f85(x421),f85(x422)) % 0.89/0.91 [43]~E(x431,x432)+E(f266(x431),f266(x432)) % 0.89/0.91 [44]~E(x441,x442)+E(f100(x441),f100(x442)) % 0.89/0.91 [45]~E(x451,x452)+E(f249(x451,x453),f249(x452,x453)) % 0.89/0.91 [46]~E(x461,x462)+E(f249(x463,x461),f249(x463,x462)) % 0.89/0.91 [47]~E(x471,x472)+E(f38(x471),f38(x472)) % 0.89/0.91 [48]~E(x481,x482)+E(f164(x481,x483),f164(x482,x483)) % 0.89/0.91 [49]~E(x491,x492)+E(f164(x493,x491),f164(x493,x492)) % 0.89/0.91 [50]~E(x501,x502)+E(f82(x501),f82(x502)) % 0.89/0.91 [51]~E(x511,x512)+E(f165(x511,x513),f165(x512,x513)) % 0.89/0.91 [52]~E(x521,x522)+E(f165(x523,x521),f165(x523,x522)) % 0.89/0.91 [53]~E(x531,x532)+E(f86(x531),f86(x532)) % 0.89/0.91 [54]~E(x541,x542)+E(f288(x541,x543),f288(x542,x543)) % 0.89/0.91 [55]~E(x551,x552)+E(f288(x553,x551),f288(x553,x552)) % 0.89/0.91 [56]~E(x561,x562)+E(f99(x561),f99(x562)) % 0.89/0.91 [57]~E(x571,x572)+E(f122(x571,x573,x574),f122(x572,x573,x574)) % 0.89/0.91 [58]~E(x581,x582)+E(f122(x583,x581,x584),f122(x583,x582,x584)) % 0.89/0.91 [59]~E(x591,x592)+E(f122(x593,x594,x591),f122(x593,x594,x592)) % 0.89/0.91 [60]~E(x601,x602)+E(f39(x601),f39(x602)) % 0.89/0.91 [61]~E(x611,x612)+E(f155(x611,x613),f155(x612,x613)) % 0.89/0.91 [62]~E(x621,x622)+E(f155(x623,x621),f155(x623,x622)) % 0.89/0.91 [63]~E(x631,x632)+E(f81(x631),f81(x632)) % 0.89/0.91 [64]~E(x641,x642)+E(f159(x641,x643),f159(x642,x643)) % 0.89/0.91 [65]~E(x651,x652)+E(f159(x653,x651),f159(x653,x652)) % 0.89/0.91 [66]~E(x661,x662)+E(f87(x661),f87(x662)) % 0.89/0.91 [67]~E(x671,x672)+E(f223(x671,x673),f223(x672,x673)) % 0.89/0.91 [68]~E(x681,x682)+E(f223(x683,x681),f223(x683,x682)) % 0.89/0.91 [69]~E(x691,x692)+E(f98(x691),f98(x692)) % 0.89/0.91 [70]~E(x701,x702)+E(f125(x701,x703,x704),f125(x702,x703,x704)) % 0.89/0.91 [71]~E(x711,x712)+E(f125(x713,x711,x714),f125(x713,x712,x714)) % 0.89/0.91 [72]~E(x721,x722)+E(f125(x723,x724,x721),f125(x723,x724,x722)) % 0.89/0.91 [73]~E(x731,x732)+E(f290(x731),f290(x732)) % 0.89/0.91 [74]~E(x741,x742)+E(f101(x741,x743,x744),f101(x742,x743,x744)) % 0.89/0.91 [75]~E(x751,x752)+E(f101(x753,x751,x754),f101(x753,x752,x754)) % 0.89/0.91 [76]~E(x761,x762)+E(f101(x763,x764,x761),f101(x763,x764,x762)) % 0.89/0.91 [77]~E(x771,x772)+E(f48(x771,x773,x774),f48(x772,x773,x774)) % 0.89/0.91 [78]~E(x781,x782)+E(f48(x783,x781,x784),f48(x783,x782,x784)) % 0.89/0.91 [79]~E(x791,x792)+E(f48(x793,x794,x791),f48(x793,x794,x792)) % 0.89/0.91 [80]~E(x801,x802)+E(f150(x801,x803,x804),f150(x802,x803,x804)) % 0.89/0.91 [81]~E(x811,x812)+E(f150(x813,x811,x814),f150(x813,x812,x814)) % 0.89/0.91 [82]~E(x821,x822)+E(f150(x823,x824,x821),f150(x823,x824,x822)) % 0.89/0.91 [83]~E(x831,x832)+E(f181(x831,x833),f181(x832,x833)) % 0.89/0.91 [84]~E(x841,x842)+E(f181(x843,x841),f181(x843,x842)) % 0.89/0.91 [85]~E(x851,x852)+E(f182(x851,x853),f182(x852,x853)) % 0.89/0.91 [86]~E(x861,x862)+E(f182(x863,x861),f182(x863,x862)) % 0.89/0.91 [87]~E(x871,x872)+E(f183(x871,x873),f183(x872,x873)) % 0.89/0.91 [88]~E(x881,x882)+E(f183(x883,x881),f183(x883,x882)) % 0.89/0.91 [89]~E(x891,x892)+E(f40(x891,x893),f40(x892,x893)) % 0.89/0.91 [90]~E(x901,x902)+E(f40(x903,x901),f40(x903,x902)) % 0.89/0.91 [91]~E(x911,x912)+E(f199(x911,x913),f199(x912,x913)) % 0.89/0.91 [92]~E(x921,x922)+E(f199(x923,x921),f199(x923,x922)) % 0.89/0.91 [93]~E(x931,x932)+E(f303(x931,x933,x934),f303(x932,x933,x934)) % 0.89/0.91 [94]~E(x941,x942)+E(f303(x943,x941,x944),f303(x943,x942,x944)) % 0.89/0.91 [95]~E(x951,x952)+E(f303(x953,x954,x951),f303(x953,x954,x952)) % 0.89/0.91 [96]~E(x961,x962)+E(f119(x961,x963,x964),f119(x962,x963,x964)) % 0.89/0.91 [97]~E(x971,x972)+E(f119(x973,x971,x974),f119(x973,x972,x974)) % 0.89/0.91 [98]~E(x981,x982)+E(f119(x983,x984,x981),f119(x983,x984,x982)) % 0.89/0.91 [99]~E(x991,x992)+E(f123(x991,x993,x994),f123(x992,x993,x994)) % 0.89/0.91 [100]~E(x1001,x1002)+E(f123(x1003,x1001,x1004),f123(x1003,x1002,x1004)) % 0.89/0.91 [101]~E(x1011,x1012)+E(f123(x1013,x1014,x1011),f123(x1013,x1014,x1012)) % 0.89/0.91 [102]~E(x1021,x1022)+E(f217(x1021,x1023),f217(x1022,x1023)) % 0.89/0.91 [103]~E(x1031,x1032)+E(f217(x1033,x1031),f217(x1033,x1032)) % 0.89/0.91 [104]~E(x1041,x1042)+E(f60(x1041),f60(x1042)) % 0.89/0.91 [105]~E(x1051,x1052)+E(f259(x1051,x1053),f259(x1052,x1053)) % 0.89/0.91 [106]~E(x1061,x1062)+E(f259(x1063,x1061),f259(x1063,x1062)) % 0.89/0.91 [107]~E(x1071,x1072)+E(f255(x1071,x1073),f255(x1072,x1073)) % 0.89/0.91 [108]~E(x1081,x1082)+E(f255(x1083,x1081),f255(x1083,x1082)) % 0.89/0.91 [109]~E(x1091,x1092)+E(f167(x1091,x1093),f167(x1092,x1093)) % 0.89/0.91 [110]~E(x1101,x1102)+E(f167(x1103,x1101),f167(x1103,x1102)) % 0.89/0.91 [111]~E(x1111,x1112)+E(f146(x1111,x1113),f146(x1112,x1113)) % 0.89/0.91 [112]~E(x1121,x1122)+E(f146(x1123,x1121),f146(x1123,x1122)) % 0.89/0.91 [113]~E(x1131,x1132)+E(f13(x1131,x1133,x1134),f13(x1132,x1133,x1134)) % 0.89/0.91 [114]~E(x1141,x1142)+E(f13(x1143,x1141,x1144),f13(x1143,x1142,x1144)) % 0.89/0.91 [115]~E(x1151,x1152)+E(f13(x1153,x1154,x1151),f13(x1153,x1154,x1152)) % 0.89/0.91 [116]~E(x1161,x1162)+E(f166(x1161,x1163),f166(x1162,x1163)) % 0.89/0.91 [117]~E(x1171,x1172)+E(f166(x1173,x1171),f166(x1173,x1172)) % 0.89/0.91 [118]~E(x1181,x1182)+E(f74(x1181,x1183),f74(x1182,x1183)) % 0.89/0.91 [119]~E(x1191,x1192)+E(f74(x1193,x1191),f74(x1193,x1192)) % 0.89/0.91 [120]~E(x1201,x1202)+E(f210(x1201,x1203),f210(x1202,x1203)) % 0.89/0.91 [121]~E(x1211,x1212)+E(f210(x1213,x1211),f210(x1213,x1212)) % 0.89/0.91 [122]~E(x1221,x1222)+E(f153(x1221,x1223),f153(x1222,x1223)) % 0.89/0.91 [123]~E(x1231,x1232)+E(f153(x1233,x1231),f153(x1233,x1232)) % 0.89/0.91 [124]~E(x1241,x1242)+E(f172(x1241,x1243),f172(x1242,x1243)) % 0.89/0.91 [125]~E(x1251,x1252)+E(f172(x1253,x1251),f172(x1253,x1252)) % 0.89/0.91 [126]~E(x1261,x1262)+E(f118(x1261,x1263,x1264),f118(x1262,x1263,x1264)) % 0.89/0.91 [127]~E(x1271,x1272)+E(f118(x1273,x1271,x1274),f118(x1273,x1272,x1274)) % 0.89/0.91 [128]~E(x1281,x1282)+E(f118(x1283,x1284,x1281),f118(x1283,x1284,x1282)) % 0.89/0.91 [129]~E(x1291,x1292)+E(f208(x1291,x1293),f208(x1292,x1293)) % 0.89/0.91 [130]~E(x1301,x1302)+E(f208(x1303,x1301),f208(x1303,x1302)) % 0.89/0.91 [131]~E(x1311,x1312)+E(f211(x1311,x1313),f211(x1312,x1313)) % 0.89/0.91 [132]~E(x1321,x1322)+E(f211(x1323,x1321),f211(x1323,x1322)) % 0.89/0.91 [133]~E(x1331,x1332)+E(f176(x1331,x1333),f176(x1332,x1333)) % 0.89/0.91 [134]~E(x1341,x1342)+E(f176(x1343,x1341),f176(x1343,x1342)) % 0.89/0.91 [135]~E(x1351,x1352)+E(f289(x1351,x1353,x1354),f289(x1352,x1353,x1354)) % 0.89/0.91 [136]~E(x1361,x1362)+E(f289(x1363,x1361,x1364),f289(x1363,x1362,x1364)) % 0.89/0.91 [137]~E(x1371,x1372)+E(f289(x1373,x1374,x1371),f289(x1373,x1374,x1372)) % 0.89/0.91 [138]~E(x1381,x1382)+E(f151(x1381,x1383),f151(x1382,x1383)) % 0.89/0.91 [139]~E(x1391,x1392)+E(f151(x1393,x1391),f151(x1393,x1392)) % 0.89/0.91 [140]~E(x1401,x1402)+E(f145(x1401,x1403),f145(x1402,x1403)) % 0.89/0.91 [141]~E(x1411,x1412)+E(f145(x1413,x1411),f145(x1413,x1412)) % 0.89/0.91 [142]~E(x1421,x1422)+E(f187(x1421,x1423),f187(x1422,x1423)) % 0.89/0.91 [143]~E(x1431,x1432)+E(f187(x1433,x1431),f187(x1433,x1432)) % 0.89/0.91 [144]~E(x1441,x1442)+E(f220(x1441,x1443),f220(x1442,x1443)) % 0.89/0.91 [145]~E(x1451,x1452)+E(f220(x1453,x1451),f220(x1453,x1452)) % 0.89/0.91 [146]~E(x1461,x1462)+E(f224(x1461,x1463),f224(x1462,x1463)) % 0.89/0.91 [147]~E(x1471,x1472)+E(f224(x1473,x1471),f224(x1473,x1472)) % 0.89/0.91 [148]~E(x1481,x1482)+E(f212(x1481,x1483),f212(x1482,x1483)) % 0.89/0.91 [149]~E(x1491,x1492)+E(f212(x1493,x1491),f212(x1493,x1492)) % 0.89/0.91 [150]~E(x1501,x1502)+E(f47(x1501,x1503,x1504),f47(x1502,x1503,x1504)) % 0.89/0.91 [151]~E(x1511,x1512)+E(f47(x1513,x1511,x1514),f47(x1513,x1512,x1514)) % 0.89/0.91 [152]~E(x1521,x1522)+E(f47(x1523,x1524,x1521),f47(x1523,x1524,x1522)) % 0.89/0.91 [153]~E(x1531,x1532)+E(f213(x1531,x1533),f213(x1532,x1533)) % 0.89/0.91 [154]~E(x1541,x1542)+E(f213(x1543,x1541),f213(x1543,x1542)) % 0.89/0.91 [155]~E(x1551,x1552)+E(f226(x1551,x1553),f226(x1552,x1553)) % 0.89/0.91 [156]~E(x1561,x1562)+E(f226(x1563,x1561),f226(x1563,x1562)) % 0.89/0.91 [157]~E(x1571,x1572)+E(f293(x1571,x1573),f293(x1572,x1573)) % 0.89/0.91 [158]~E(x1581,x1582)+E(f293(x1583,x1581),f293(x1583,x1582)) % 0.89/0.91 [159]~E(x1591,x1592)+E(f237(x1591,x1593),f237(x1592,x1593)) % 0.89/0.91 [160]~E(x1601,x1602)+E(f237(x1603,x1601),f237(x1603,x1602)) % 0.89/0.91 [161]~E(x1611,x1612)+E(f170(x1611,x1613),f170(x1612,x1613)) % 0.89/0.91 [162]~E(x1621,x1622)+E(f170(x1623,x1621),f170(x1623,x1622)) % 0.89/0.91 [163]~E(x1631,x1632)+E(f198(x1631,x1633),f198(x1632,x1633)) % 0.89/0.91 [164]~E(x1641,x1642)+E(f198(x1643,x1641),f198(x1643,x1642)) % 0.89/0.91 [165]~E(x1651,x1652)+E(f244(x1651,x1653),f244(x1652,x1653)) % 0.89/0.91 [166]~E(x1661,x1662)+E(f244(x1663,x1661),f244(x1663,x1662)) % 0.89/0.91 [167]~E(x1671,x1672)+E(f161(x1671,x1673),f161(x1672,x1673)) % 0.89/0.91 [168]~E(x1681,x1682)+E(f161(x1683,x1681),f161(x1683,x1682)) % 0.89/0.91 [169]~E(x1691,x1692)+E(f89(x1691),f89(x1692)) % 0.89/0.91 [170]~E(x1701,x1702)+E(f71(x1701,x1703),f71(x1702,x1703)) % 0.89/0.91 [171]~E(x1711,x1712)+E(f71(x1713,x1711),f71(x1713,x1712)) % 0.89/0.91 [172]~E(x1721,x1722)+E(f245(x1721,x1723),f245(x1722,x1723)) % 0.89/0.91 [173]~E(x1731,x1732)+E(f245(x1733,x1731),f245(x1733,x1732)) % 0.89/0.91 [174]~E(x1741,x1742)+E(f201(x1741,x1743),f201(x1742,x1743)) % 0.89/0.91 [175]~E(x1751,x1752)+E(f201(x1753,x1751),f201(x1753,x1752)) % 0.89/0.91 [176]~E(x1761,x1762)+E(f205(x1761,x1763),f205(x1762,x1763)) % 0.89/0.91 [177]~E(x1771,x1772)+E(f205(x1773,x1771),f205(x1773,x1772)) % 0.89/0.91 [178]~E(x1781,x1782)+E(f168(x1781,x1783),f168(x1782,x1783)) % 0.89/0.91 [179]~E(x1791,x1792)+E(f168(x1793,x1791),f168(x1793,x1792)) % 0.89/0.91 [180]~E(x1801,x1802)+E(f234(x1801,x1803),f234(x1802,x1803)) % 0.89/0.91 [181]~E(x1811,x1812)+E(f234(x1813,x1811),f234(x1813,x1812)) % 0.89/0.91 [182]~E(x1821,x1822)+E(f227(x1821,x1823),f227(x1822,x1823)) % 0.89/0.91 [183]~E(x1831,x1832)+E(f227(x1833,x1831),f227(x1833,x1832)) % 0.89/0.91 [184]~E(x1841,x1842)+E(f214(x1841,x1843),f214(x1842,x1843)) % 0.89/0.91 [185]~E(x1851,x1852)+E(f214(x1853,x1851),f214(x1853,x1852)) % 0.89/0.91 [186]~E(x1861,x1862)+E(f246(x1861,x1863),f246(x1862,x1863)) % 0.89/0.91 [187]~E(x1871,x1872)+E(f246(x1873,x1871),f246(x1873,x1872)) % 0.89/0.91 [188]~E(x1881,x1882)+E(f152(x1881,x1883),f152(x1882,x1883)) % 0.89/0.91 [189]~E(x1891,x1892)+E(f152(x1893,x1891),f152(x1893,x1892)) % 0.89/0.91 [190]~E(x1901,x1902)+E(f158(x1901,x1903),f158(x1902,x1903)) % 0.89/0.91 [191]~E(x1911,x1912)+E(f158(x1913,x1911),f158(x1913,x1912)) % 0.89/0.91 [192]~E(x1921,x1922)+E(f189(x1921,x1923),f189(x1922,x1923)) % 0.89/0.91 [193]~E(x1931,x1932)+E(f189(x1933,x1931),f189(x1933,x1932)) % 0.89/0.91 [194]~E(x1941,x1942)+E(f221(x1941,x1943),f221(x1942,x1943)) % 0.89/0.91 [195]~E(x1951,x1952)+E(f221(x1953,x1951),f221(x1953,x1952)) % 0.89/0.91 [196]~E(x1961,x1962)+E(f68(x1961,x1963),f68(x1962,x1963)) % 0.89/0.91 [197]~E(x1971,x1972)+E(f68(x1973,x1971),f68(x1973,x1972)) % 0.89/0.91 [198]~E(x1981,x1982)+E(f251(x1981,x1983),f251(x1982,x1983)) % 0.89/0.91 [199]~E(x1991,x1992)+E(f251(x1993,x1991),f251(x1993,x1992)) % 0.89/0.91 [200]~E(x2001,x2002)+E(f109(x2001,x2003),f109(x2002,x2003)) % 0.89/0.91 [201]~E(x2011,x2012)+E(f109(x2013,x2011),f109(x2013,x2012)) % 0.89/0.91 [202]~E(x2021,x2022)+E(f132(x2021,x2023,x2024),f132(x2022,x2023,x2024)) % 0.89/0.91 [203]~E(x2031,x2032)+E(f132(x2033,x2031,x2034),f132(x2033,x2032,x2034)) % 0.89/0.91 [204]~E(x2041,x2042)+E(f132(x2043,x2044,x2041),f132(x2043,x2044,x2042)) % 0.89/0.91 [205]~E(x2051,x2052)+E(f190(x2051,x2053),f190(x2052,x2053)) % 0.89/0.91 [206]~E(x2061,x2062)+E(f190(x2063,x2061),f190(x2063,x2062)) % 0.89/0.91 [207]~E(x2071,x2072)+E(f78(x2071,x2073),f78(x2072,x2073)) % 0.89/0.91 [208]~E(x2081,x2082)+E(f78(x2083,x2081),f78(x2083,x2082)) % 0.89/0.91 [209]~E(x2091,x2092)+E(f156(x2091,x2093),f156(x2092,x2093)) % 0.89/0.91 [210]~E(x2101,x2102)+E(f156(x2103,x2101),f156(x2103,x2102)) % 0.89/0.91 [211]~E(x2111,x2112)+E(f195(x2111,x2113),f195(x2112,x2113)) % 0.89/0.91 [212]~E(x2121,x2122)+E(f195(x2123,x2121),f195(x2123,x2122)) % 0.89/0.91 [213]~E(x2131,x2132)+E(f177(x2131,x2133),f177(x2132,x2133)) % 0.89/0.91 [214]~E(x2141,x2142)+E(f177(x2143,x2141),f177(x2143,x2142)) % 0.89/0.91 [215]~E(x2151,x2152)+E(f229(x2151,x2153),f229(x2152,x2153)) % 0.89/0.91 [216]~E(x2161,x2162)+E(f229(x2163,x2161),f229(x2163,x2162)) % 0.89/0.91 [217]~E(x2171,x2172)+E(f203(x2171,x2173),f203(x2172,x2173)) % 0.89/0.91 [218]~E(x2181,x2182)+E(f203(x2183,x2181),f203(x2183,x2182)) % 0.89/0.91 [219]~E(x2191,x2192)+E(f144(x2191,x2193),f144(x2192,x2193)) % 0.89/0.91 [220]~E(x2201,x2202)+E(f144(x2203,x2201),f144(x2203,x2202)) % 0.89/0.91 [221]~E(x2211,x2212)+E(f56(x2211),f56(x2212)) % 0.89/0.91 [222]~E(x2221,x2222)+E(f230(x2221,x2223),f230(x2222,x2223)) % 0.89/0.91 [223]~E(x2231,x2232)+E(f230(x2233,x2231),f230(x2233,x2232)) % 0.89/0.91 [224]~E(x2241,x2242)+E(f215(x2241,x2243),f215(x2242,x2243)) % 0.89/0.91 [225]~E(x2251,x2252)+E(f215(x2253,x2251),f215(x2253,x2252)) % 0.89/0.91 [226]~E(x2261,x2262)+E(f103(x2261,x2263),f103(x2262,x2263)) % 0.89/0.91 [227]~E(x2271,x2272)+E(f103(x2273,x2271),f103(x2273,x2272)) % 0.89/0.91 [228]~E(x2281,x2282)+E(f209(x2281,x2283),f209(x2282,x2283)) % 0.89/0.91 [229]~E(x2291,x2292)+E(f209(x2293,x2291),f209(x2293,x2292)) % 0.89/0.91 [230]~E(x2301,x2302)+E(f301(x2301,x2303,x2304,x2305,x2306),f301(x2302,x2303,x2304,x2305,x2306)) % 0.89/0.91 [231]~E(x2311,x2312)+E(f301(x2313,x2311,x2314,x2315,x2316),f301(x2313,x2312,x2314,x2315,x2316)) % 0.89/0.91 [232]~E(x2321,x2322)+E(f301(x2323,x2324,x2321,x2325,x2326),f301(x2323,x2324,x2322,x2325,x2326)) % 0.89/0.91 [233]~E(x2331,x2332)+E(f301(x2333,x2334,x2335,x2331,x2336),f301(x2333,x2334,x2335,x2332,x2336)) % 0.89/0.91 [234]~E(x2341,x2342)+E(f301(x2343,x2344,x2345,x2346,x2341),f301(x2343,x2344,x2345,x2346,x2342)) % 0.89/0.91 [235]~E(x2351,x2352)+E(f184(x2351,x2353),f184(x2352,x2353)) % 0.89/0.91 [236]~E(x2361,x2362)+E(f184(x2363,x2361),f184(x2363,x2362)) % 0.89/0.91 [237]~E(x2371,x2372)+E(f91(x2371),f91(x2372)) % 0.89/0.91 [238]~E(x2381,x2382)+E(f129(x2381,x2383,x2384),f129(x2382,x2383,x2384)) % 0.89/0.91 [239]~E(x2391,x2392)+E(f129(x2393,x2391,x2394),f129(x2393,x2392,x2394)) % 0.89/0.91 [240]~E(x2401,x2402)+E(f129(x2403,x2404,x2401),f129(x2403,x2404,x2402)) % 0.89/0.91 [241]~E(x2411,x2412)+E(f238(x2411,x2413),f238(x2412,x2413)) % 0.89/0.91 [242]~E(x2421,x2422)+E(f238(x2423,x2421),f238(x2423,x2422)) % 0.89/0.91 [243]~E(x2431,x2432)+E(f49(x2431,x2433,x2434),f49(x2432,x2433,x2434)) % 0.89/0.91 [244]~E(x2441,x2442)+E(f49(x2443,x2441,x2444),f49(x2443,x2442,x2444)) % 0.89/0.91 [245]~E(x2451,x2452)+E(f49(x2453,x2454,x2451),f49(x2453,x2454,x2452)) % 0.89/0.91 [246]~E(x2461,x2462)+E(f206(x2461,x2463),f206(x2462,x2463)) % 0.89/0.91 [247]~E(x2471,x2472)+E(f206(x2473,x2471),f206(x2473,x2472)) % 0.89/0.91 [248]~E(x2481,x2482)+E(f239(x2481,x2483),f239(x2482,x2483)) % 0.89/0.91 [249]~E(x2491,x2492)+E(f239(x2493,x2491),f239(x2493,x2492)) % 0.89/0.91 [250]~E(x2501,x2502)+E(f141(x2501,x2503,x2504),f141(x2502,x2503,x2504)) % 0.89/0.91 [251]~E(x2511,x2512)+E(f141(x2513,x2511,x2514),f141(x2513,x2512,x2514)) % 0.89/0.91 [252]~E(x2521,x2522)+E(f141(x2523,x2524,x2521),f141(x2523,x2524,x2522)) % 0.89/0.91 [253]~E(x2531,x2532)+E(f241(x2531,x2533),f241(x2532,x2533)) % 0.89/0.91 [254]~E(x2541,x2542)+E(f241(x2543,x2541),f241(x2543,x2542)) % 0.89/0.91 [255]~E(x2551,x2552)+E(f200(x2551,x2553),f200(x2552,x2553)) % 0.89/0.91 [256]~E(x2561,x2562)+E(f200(x2563,x2561),f200(x2563,x2562)) % 0.89/0.91 [257]~E(x2571,x2572)+E(f185(x2571,x2573),f185(x2572,x2573)) % 0.89/0.91 [258]~E(x2581,x2582)+E(f185(x2583,x2581),f185(x2583,x2582)) % 0.89/0.91 [259]~E(x2591,x2592)+E(f193(x2591,x2593),f193(x2592,x2593)) % 0.89/0.91 [260]~E(x2601,x2602)+E(f193(x2603,x2601),f193(x2603,x2602)) % 0.89/0.91 [261]~E(x2611,x2612)+E(f50(x2611,x2613,x2614),f50(x2612,x2613,x2614)) % 0.89/0.91 [262]~E(x2621,x2622)+E(f50(x2623,x2621,x2624),f50(x2623,x2622,x2624)) % 0.89/0.91 [263]~E(x2631,x2632)+E(f50(x2633,x2634,x2631),f50(x2633,x2634,x2632)) % 0.89/0.91 [264]~E(x2641,x2642)+E(f292(x2641),f292(x2642)) % 0.89/0.91 [265]~E(x2651,x2652)+E(f261(x2651),f261(x2652)) % 0.89/0.91 [266]~E(x2661,x2662)+E(f196(x2661,x2663),f196(x2662,x2663)) % 0.89/0.91 [267]~E(x2671,x2672)+E(f196(x2673,x2671),f196(x2673,x2672)) % 0.89/0.91 [268]~E(x2681,x2682)+E(f191(x2681,x2683),f191(x2682,x2683)) % 0.89/0.91 [269]~E(x2691,x2692)+E(f191(x2693,x2691),f191(x2693,x2692)) % 0.89/0.91 [270]~E(x2701,x2702)+E(f231(x2701,x2703),f231(x2702,x2703)) % 0.89/0.91 [271]~E(x2711,x2712)+E(f231(x2713,x2711),f231(x2713,x2712)) % 0.89/0.91 [272]~E(x2721,x2722)+E(f160(x2721,x2723),f160(x2722,x2723)) % 0.89/0.91 [273]~E(x2731,x2732)+E(f160(x2733,x2731),f160(x2733,x2732)) % 0.89/0.91 [274]~E(x2741,x2742)+E(f260(x2741),f260(x2742)) % 0.89/0.91 [275]~E(x2751,x2752)+E(f169(x2751,x2753),f169(x2752,x2753)) % 0.89/0.91 [276]~E(x2761,x2762)+E(f169(x2763,x2761),f169(x2763,x2762)) % 0.89/0.91 [277]~E(x2771,x2772)+E(f247(x2771,x2773),f247(x2772,x2773)) % 0.89/0.91 [278]~E(x2781,x2782)+E(f247(x2783,x2781),f247(x2783,x2782)) % 0.89/0.91 [279]~E(x2791,x2792)+E(f134(x2791,x2793,x2794),f134(x2792,x2793,x2794)) % 0.89/0.91 [280]~E(x2801,x2802)+E(f134(x2803,x2801,x2804),f134(x2803,x2802,x2804)) % 0.89/0.91 [281]~E(x2811,x2812)+E(f134(x2813,x2814,x2811),f134(x2813,x2814,x2812)) % 0.89/0.91 [282]~E(x2821,x2822)+E(f54(x2821),f54(x2822)) % 0.89/0.91 [283]~E(x2831,x2832)+E(f218(x2831,x2833),f218(x2832,x2833)) % 0.89/0.91 [284]~E(x2841,x2842)+E(f218(x2843,x2841),f218(x2843,x2842)) % 0.89/0.91 [285]~E(x2851,x2852)+E(f248(x2851,x2853),f248(x2852,x2853)) % 0.89/0.91 [286]~E(x2861,x2862)+E(f248(x2863,x2861),f248(x2863,x2862)) % 0.89/0.91 [287]~E(x2871,x2872)+E(f194(x2871,x2873),f194(x2872,x2873)) % 0.89/0.91 [288]~E(x2881,x2882)+E(f194(x2883,x2881),f194(x2883,x2882)) % 0.89/0.91 [289]~E(x2891,x2892)+E(f120(x2891,x2893,x2894),f120(x2892,x2893,x2894)) % 0.89/0.91 [290]~E(x2901,x2902)+E(f120(x2903,x2901,x2904),f120(x2903,x2902,x2904)) % 0.89/0.91 [291]~E(x2911,x2912)+E(f120(x2913,x2914,x2911),f120(x2913,x2914,x2912)) % 0.89/0.91 [292]~E(x2921,x2922)+E(f148(x2921,x2923),f148(x2922,x2923)) % 0.89/0.91 [293]~E(x2931,x2932)+E(f148(x2933,x2931),f148(x2933,x2932)) % 0.89/0.91 [294]~E(x2941,x2942)+E(f192(x2941,x2943),f192(x2942,x2943)) % 0.89/0.91 [295]~E(x2951,x2952)+E(f192(x2953,x2951),f192(x2953,x2952)) % 0.89/0.91 [296]~E(x2961,x2962)+E(f236(x2961,x2963),f236(x2962,x2963)) % 0.89/0.91 [297]~E(x2971,x2972)+E(f236(x2973,x2971),f236(x2973,x2972)) % 0.89/0.91 [298]~E(x2981,x2982)+E(f250(x2981,x2983),f250(x2982,x2983)) % 0.89/0.91 [299]~E(x2991,x2992)+E(f250(x2993,x2991),f250(x2993,x2992)) % 0.89/0.91 [300]~E(x3001,x3002)+E(f90(x3001),f90(x3002)) % 0.89/0.91 [301]~E(x3011,x3012)+E(f171(x3011,x3013),f171(x3012,x3013)) % 0.89/0.91 [302]~E(x3021,x3022)+E(f171(x3023,x3021),f171(x3023,x3022)) % 0.89/0.91 [303]~E(x3031,x3032)+E(f253(x3031,x3033),f253(x3032,x3033)) % 0.89/0.91 [304]~E(x3041,x3042)+E(f253(x3043,x3041),f253(x3043,x3042)) % 0.89/0.91 [305]~E(x3051,x3052)+E(f254(x3051,x3053),f254(x3052,x3053)) % 0.89/0.91 [306]~E(x3061,x3062)+E(f254(x3063,x3061),f254(x3063,x3062)) % 0.89/0.91 [307]~E(x3071,x3072)+E(f240(x3071,x3073),f240(x3072,x3073)) % 0.89/0.91 [308]~E(x3081,x3082)+E(f240(x3083,x3081),f240(x3083,x3082)) % 0.89/0.91 [309]~E(x3091,x3092)+E(f128(x3091,x3093,x3094),f128(x3092,x3093,x3094)) % 0.89/0.91 [310]~E(x3101,x3102)+E(f128(x3103,x3101,x3104),f128(x3103,x3102,x3104)) % 0.89/0.91 [311]~E(x3111,x3112)+E(f128(x3113,x3114,x3111),f128(x3113,x3114,x3112)) % 0.89/0.91 [312]~E(x3121,x3122)+E(f135(x3121,x3123,x3124),f135(x3122,x3123,x3124)) % 0.89/0.91 [313]~E(x3131,x3132)+E(f135(x3133,x3131,x3134),f135(x3133,x3132,x3134)) % 0.89/0.91 [314]~E(x3141,x3142)+E(f135(x3143,x3144,x3141),f135(x3143,x3144,x3142)) % 0.89/0.91 [315]~E(x3151,x3152)+E(f77(x3151,x3153),f77(x3152,x3153)) % 0.89/0.91 [316]~E(x3161,x3162)+E(f77(x3163,x3161),f77(x3163,x3162)) % 0.89/0.91 [317]~E(x3171,x3172)+E(f204(x3171,x3173),f204(x3172,x3173)) % 0.89/0.91 [318]~E(x3181,x3182)+E(f204(x3183,x3181),f204(x3183,x3182)) % 0.89/0.91 [319]~E(x3191,x3192)+E(f233(x3191,x3193),f233(x3192,x3193)) % 0.89/0.91 [320]~E(x3201,x3202)+E(f233(x3203,x3201),f233(x3203,x3202)) % 0.89/0.91 [321]~E(x3211,x3212)+E(f235(x3211,x3213),f235(x3212,x3213)) % 0.89/0.91 [322]~E(x3221,x3222)+E(f235(x3223,x3221),f235(x3223,x3222)) % 0.89/0.91 [323]~E(x3231,x3232)+E(f76(x3231,x3233),f76(x3232,x3233)) % 0.89/0.91 [324]~E(x3241,x3242)+E(f76(x3243,x3241),f76(x3243,x3242)) % 0.89/0.91 [325]~E(x3251,x3252)+E(f110(x3251,x3253),f110(x3252,x3253)) % 0.89/0.91 [326]~E(x3261,x3262)+E(f110(x3263,x3261),f110(x3263,x3262)) % 0.89/0.91 [327]~E(x3271,x3272)+E(f216(x3271,x3273),f216(x3272,x3273)) % 0.89/0.91 [328]~E(x3281,x3282)+E(f216(x3283,x3281),f216(x3283,x3282)) % 0.89/0.91 [329]~E(x3291,x3292)+E(f197(x3291,x3293),f197(x3292,x3293)) % 0.89/0.91 [330]~E(x3301,x3302)+E(f197(x3303,x3301),f197(x3303,x3302)) % 0.89/0.91 [331]~E(x3311,x3312)+E(f186(x3311,x3313),f186(x3312,x3313)) % 0.89/0.91 [332]~E(x3321,x3322)+E(f186(x3323,x3321),f186(x3323,x3322)) % 0.89/0.91 [333]~E(x3331,x3332)+E(f95(x3331),f95(x3332)) % 0.89/0.91 [334]~E(x3341,x3342)+E(f157(x3341,x3343),f157(x3342,x3343)) % 0.89/0.91 [335]~E(x3351,x3352)+E(f157(x3353,x3351),f157(x3353,x3352)) % 0.89/0.91 [336]~E(x3361,x3362)+E(f228(x3361,x3363),f228(x3362,x3363)) % 0.89/0.91 [337]~E(x3371,x3372)+E(f228(x3373,x3371),f228(x3373,x3372)) % 0.89/0.91 [338]~E(x3381,x3382)+E(f142(x3381,x3383,x3384),f142(x3382,x3383,x3384)) % 0.89/0.91 [339]~E(x3391,x3392)+E(f142(x3393,x3391,x3394),f142(x3393,x3392,x3394)) % 0.89/0.91 [340]~E(x3401,x3402)+E(f142(x3403,x3404,x3401),f142(x3403,x3404,x3402)) % 0.89/0.91 [341]~E(x3411,x3412)+E(f202(x3411,x3413),f202(x3412,x3413)) % 0.89/0.91 [342]~E(x3421,x3422)+E(f202(x3423,x3421),f202(x3423,x3422)) % 0.89/0.91 [343]~E(x3431,x3432)+E(f163(x3431,x3433),f163(x3432,x3433)) % 0.89/0.91 [344]~E(x3441,x3442)+E(f163(x3443,x3441),f163(x3443,x3442)) % 0.89/0.91 [345]~E(x3451,x3452)+E(f207(x3451,x3453),f207(x3452,x3453)) % 0.89/0.91 [346]~E(x3461,x3462)+E(f207(x3463,x3461),f207(x3463,x3462)) % 0.89/0.91 [347]~E(x3471,x3472)+E(f242(x3471,x3473),f242(x3472,x3473)) % 0.89/0.91 [348]~E(x3481,x3482)+E(f242(x3483,x3481),f242(x3483,x3482)) % 0.89/0.91 [349]~E(x3491,x3492)+E(f80(x3491,x3493),f80(x3492,x3493)) % 0.89/0.91 [350]~E(x3501,x3502)+E(f80(x3503,x3501),f80(x3503,x3502)) % 0.89/0.91 [351]~E(x3511,x3512)+E(f232(x3511,x3513),f232(x3512,x3513)) % 0.89/0.91 [352]~E(x3521,x3522)+E(f232(x3523,x3521),f232(x3523,x3522)) % 0.89/0.91 [353]~E(x3531,x3532)+E(f140(x3531,x3533,x3534),f140(x3532,x3533,x3534)) % 0.89/0.91 [354]~E(x3541,x3542)+E(f140(x3543,x3541,x3544),f140(x3543,x3542,x3544)) % 0.89/0.91 [355]~E(x3551,x3552)+E(f140(x3553,x3554,x3551),f140(x3553,x3554,x3552)) % 0.89/0.91 [356]~E(x3561,x3562)+E(f252(x3561,x3563),f252(x3562,x3563)) % 0.89/0.91 [357]~E(x3571,x3572)+E(f252(x3573,x3571),f252(x3573,x3572)) % 0.89/0.91 [358]~E(x3581,x3582)+E(f115(x3581,x3583),f115(x3582,x3583)) % 0.89/0.91 [359]~E(x3591,x3592)+E(f115(x3593,x3591),f115(x3593,x3592)) % 0.89/0.91 [360]~E(x3601,x3602)+E(f243(x3601,x3603),f243(x3602,x3603)) % 0.89/0.91 [361]~E(x3611,x3612)+E(f243(x3613,x3611),f243(x3613,x3612)) % 0.89/0.91 [362]~E(x3621,x3622)+E(f88(x3621),f88(x3622)) % 0.89/0.91 [363]~E(x3631,x3632)+E(f222(x3631,x3633),f222(x3632,x3633)) % 0.89/0.91 [364]~E(x3641,x3642)+E(f222(x3643,x3641),f222(x3643,x3642)) % 0.89/0.91 [365]~E(x3651,x3652)+E(f130(x3651,x3653,x3654),f130(x3652,x3653,x3654)) % 0.89/0.91 [366]~E(x3661,x3662)+E(f130(x3663,x3661,x3664),f130(x3663,x3662,x3664)) % 0.89/0.91 [367]~E(x3671,x3672)+E(f130(x3673,x3674,x3671),f130(x3673,x3674,x3672)) % 0.89/0.91 [368]~E(x3681,x3682)+E(f126(x3681,x3683,x3684),f126(x3682,x3683,x3684)) % 0.89/0.91 [369]~E(x3691,x3692)+E(f126(x3693,x3691,x3694),f126(x3693,x3692,x3694)) % 0.89/0.91 [370]~E(x3701,x3702)+E(f126(x3703,x3704,x3701),f126(x3703,x3704,x3702)) % 0.89/0.91 [371]~E(x3711,x3712)+E(f162(x3711,x3713),f162(x3712,x3713)) % 0.89/0.91 [372]~E(x3721,x3722)+E(f162(x3723,x3721),f162(x3723,x3722)) % 0.89/0.91 [373]~E(x3731,x3732)+E(f133(x3731,x3733,x3734),f133(x3732,x3733,x3734)) % 0.89/0.91 [374]~E(x3741,x3742)+E(f133(x3743,x3741,x3744),f133(x3743,x3742,x3744)) % 0.89/0.91 [375]~E(x3751,x3752)+E(f133(x3753,x3754,x3751),f133(x3753,x3754,x3752)) % 0.89/0.91 [376]~E(x3761,x3762)+E(f225(x3761,x3763),f225(x3762,x3763)) % 0.89/0.91 [377]~E(x3771,x3772)+E(f225(x3773,x3771),f225(x3773,x3772)) % 0.89/0.91 [378]~E(x3781,x3782)+E(f108(x3781,x3783),f108(x3782,x3783)) % 0.89/0.91 [379]~E(x3791,x3792)+E(f108(x3793,x3791),f108(x3793,x3792)) % 0.89/0.91 [380]~E(x3801,x3802)+E(f41(x3801),f41(x3802)) % 0.89/0.91 [381]~E(x3811,x3812)+E(f139(x3811,x3813,x3814),f139(x3812,x3813,x3814)) % 0.89/0.91 [382]~E(x3821,x3822)+E(f139(x3823,x3821,x3824),f139(x3823,x3822,x3824)) % 0.89/0.91 [383]~E(x3831,x3832)+E(f139(x3833,x3834,x3831),f139(x3833,x3834,x3832)) % 0.89/0.91 [384]~E(x3841,x3842)+E(f66(x3841),f66(x3842)) % 0.89/0.91 [385]~E(x3851,x3852)+E(f114(x3851,x3853),f114(x3852,x3853)) % 0.89/0.91 [386]~E(x3861,x3862)+E(f114(x3863,x3861),f114(x3863,x3862)) % 0.89/0.91 [387]~E(x3871,x3872)+E(f67(x3871),f67(x3872)) % 0.89/0.91 [388]~E(x3881,x3882)+E(f79(x3881,x3883),f79(x3882,x3883)) % 0.89/0.91 [389]~E(x3891,x3892)+E(f79(x3893,x3891),f79(x3893,x3892)) % 0.89/0.91 [390]~E(x3901,x3902)+E(f143(x3901,x3903),f143(x3902,x3903)) % 0.89/0.91 [391]~E(x3911,x3912)+E(f143(x3913,x3911),f143(x3913,x3912)) % 0.89/0.91 [392]~E(x3921,x3922)+E(f42(x3921),f42(x3922)) % 0.89/0.91 [393]~E(x3931,x3932)+E(f72(x3931,x3933),f72(x3932,x3933)) % 0.89/0.91 [394]~E(x3941,x3942)+E(f72(x3943,x3941),f72(x3943,x3942)) % 0.89/0.91 [395]~E(x3951,x3952)+E(f63(x3951),f63(x3952)) % 0.89/0.91 [396]~E(x3961,x3962)+E(f113(x3961,x3963),f113(x3962,x3963)) % 0.89/0.91 [397]~E(x3971,x3972)+E(f113(x3973,x3971),f113(x3973,x3972)) % 0.89/0.91 [398]~E(x3981,x3982)+E(f65(x3981),f65(x3982)) % 0.89/0.91 [399]~E(x3991,x3992)+E(f137(x3991,x3993,x3994),f137(x3992,x3993,x3994)) % 0.89/0.91 [400]~E(x4001,x4002)+E(f137(x4003,x4001,x4004),f137(x4003,x4002,x4004)) % 0.89/0.91 [401]~E(x4011,x4012)+E(f137(x4013,x4014,x4011),f137(x4013,x4014,x4012)) % 0.89/0.91 [402]~E(x4021,x4022)+E(f105(x4021,x4023),f105(x4022,x4023)) % 0.89/0.91 [403]~E(x4031,x4032)+E(f105(x4033,x4031),f105(x4033,x4032)) % 0.89/0.91 [404]~E(x4041,x4042)+E(f147(x4041,x4043),f147(x4042,x4043)) % 0.89/0.91 [405]~E(x4051,x4052)+E(f147(x4053,x4051),f147(x4053,x4052)) % 0.89/0.91 [406]~E(x4061,x4062)+E(f104(x4061,x4063),f104(x4062,x4063)) % 0.89/0.91 [407]~E(x4071,x4072)+E(f104(x4073,x4071),f104(x4073,x4072)) % 0.89/0.91 [408]~E(x4081,x4082)+E(f94(x4081),f94(x4082)) % 0.89/0.91 [409]~E(x4091,x4092)+E(f136(x4091,x4093,x4094),f136(x4092,x4093,x4094)) % 0.89/0.91 [410]~E(x4101,x4102)+E(f136(x4103,x4101,x4104),f136(x4103,x4102,x4104)) % 0.89/0.91 [411]~E(x4111,x4112)+E(f136(x4113,x4114,x4111),f136(x4113,x4114,x4112)) % 0.89/0.91 [412]~E(x4121,x4122)+E(f111(x4121,x4123),f111(x4122,x4123)) % 0.89/0.91 [413]~E(x4131,x4132)+E(f111(x4133,x4131),f111(x4133,x4132)) % 0.89/0.91 [414]~E(x4141,x4142)+E(f174(x4141,x4143),f174(x4142,x4143)) % 0.89/0.91 [415]~E(x4151,x4152)+E(f174(x4153,x4151),f174(x4153,x4152)) % 0.89/0.91 [416]~E(x4161,x4162)+E(f83(x4161,x4163),f83(x4162,x4163)) % 0.89/0.91 [417]~E(x4171,x4172)+E(f83(x4173,x4171),f83(x4173,x4172)) % 0.89/0.91 [418]~E(x4181,x4182)+E(f97(x4181),f97(x4182)) % 0.89/0.91 [419]~E(x4191,x4192)+E(f121(x4191,x4193,x4194),f121(x4192,x4193,x4194)) % 0.89/0.91 [420]~E(x4201,x4202)+E(f121(x4203,x4201,x4204),f121(x4203,x4202,x4204)) % 0.89/0.91 [421]~E(x4211,x4212)+E(f121(x4213,x4214,x4211),f121(x4213,x4214,x4212)) % 0.89/0.91 [422]~E(x4221,x4222)+E(f92(x4221),f92(x4222)) % 0.89/0.91 [423]~E(x4231,x4232)+E(f131(x4231,x4233,x4234),f131(x4232,x4233,x4234)) % 0.89/0.91 [424]~E(x4241,x4242)+E(f131(x4243,x4241,x4244),f131(x4243,x4242,x4244)) % 0.89/0.91 [425]~E(x4251,x4252)+E(f131(x4253,x4254,x4251),f131(x4253,x4254,x4252)) % 0.89/0.91 [426]~E(x4261,x4262)+E(f53(x4261,x4263,x4264),f53(x4262,x4263,x4264)) % 0.89/0.91 [427]~E(x4271,x4272)+E(f53(x4273,x4271,x4274),f53(x4273,x4272,x4274)) % 0.89/0.91 [428]~E(x4281,x4282)+E(f53(x4283,x4284,x4281),f53(x4283,x4284,x4282)) % 0.89/0.91 [429]~E(x4291,x4292)+E(f117(x4291,x4293,x4294),f117(x4292,x4293,x4294)) % 0.89/0.91 [430]~E(x4301,x4302)+E(f117(x4303,x4301,x4304),f117(x4303,x4302,x4304)) % 0.89/0.91 [431]~E(x4311,x4312)+E(f117(x4313,x4314,x4311),f117(x4313,x4314,x4312)) % 0.89/0.91 [432]~E(x4321,x4322)+E(f70(x4321,x4323),f70(x4322,x4323)) % 0.89/0.91 [433]~E(x4331,x4332)+E(f70(x4333,x4331),f70(x4333,x4332)) % 0.89/0.91 [434]~E(x4341,x4342)+E(f57(x4341),f57(x4342)) % 0.89/0.91 [435]~E(x4351,x4352)+E(f62(x4351),f62(x4352)) % 0.89/0.91 [436]~E(x4361,x4362)+E(f58(x4361),f58(x4362)) % 0.89/0.91 [437]~E(x4371,x4372)+E(f96(x4371,x4373),f96(x4372,x4373)) % 0.89/0.91 [438]~E(x4381,x4382)+E(f96(x4383,x4381),f96(x4383,x4382)) % 0.89/0.91 [439]~E(x4391,x4392)+E(f51(x4391,x4393,x4394),f51(x4392,x4393,x4394)) % 0.89/0.91 [440]~E(x4401,x4402)+E(f51(x4403,x4401,x4404),f51(x4403,x4402,x4404)) % 0.89/0.91 [441]~E(x4411,x4412)+E(f51(x4413,x4414,x4411),f51(x4413,x4414,x4412)) % 0.89/0.91 [442]~E(x4421,x4422)+E(f59(x4421),f59(x4422)) % 0.89/0.91 [443]~E(x4431,x4432)+E(f52(x4431,x4433,x4434),f52(x4432,x4433,x4434)) % 0.89/0.91 [444]~E(x4441,x4442)+E(f52(x4443,x4441,x4444),f52(x4443,x4442,x4444)) % 0.89/0.91 [445]~E(x4451,x4452)+E(f52(x4453,x4454,x4451),f52(x4453,x4454,x4452)) % 0.89/0.91 [446]~E(x4461,x4462)+E(f64(x4461,x4463),f64(x4462,x4463)) % 0.89/0.91 [447]~E(x4471,x4472)+E(f64(x4473,x4471),f64(x4473,x4472)) % 0.89/0.91 [448]~E(x4481,x4482)+E(f102(x4481),f102(x4482)) % 0.89/0.91 [449]~E(x4491,x4492)+E(f173(x4491,x4493),f173(x4492,x4493)) % 0.89/0.91 [450]~E(x4501,x4502)+E(f173(x4503,x4501),f173(x4503,x4502)) % 0.89/0.91 [451]~E(x4511,x4512)+E(f116(x4511),f116(x4512)) % 0.89/0.91 [452]~E(x4521,x4522)+E(f61(x4521),f61(x4522)) % 0.89/0.91 [453]~E(x4531,x4532)+E(f127(x4531),f127(x4532)) % 0.89/0.91 [454]~E(x4541,x4542)+E(f219(x4541,x4543),f219(x4542,x4543)) % 0.89/0.91 [455]~E(x4551,x4552)+E(f219(x4553,x4551),f219(x4553,x4552)) % 0.89/0.91 [456]~E(x4561,x4562)+E(f138(x4561),f138(x4562)) % 0.89/0.91 [457]~E(x4571,x4572)+E(f55(x4571),f55(x4572)) % 0.89/0.91 [458]~E(x4581,x4582)+E(f69(x4581,x4583),f69(x4582,x4583)) % 0.89/0.91 [459]~E(x4591,x4592)+E(f69(x4593,x4591),f69(x4593,x4592)) % 0.89/0.91 [460]~E(x4601,x4602)+E(f112(x4601,x4603),f112(x4602,x4603)) % 0.89/0.91 [461]~E(x4611,x4612)+E(f112(x4613,x4611),f112(x4613,x4612)) % 0.89/0.91 [462]~E(x4621,x4622)+E(f75(x4621,x4623),f75(x4622,x4623)) % 0.89/0.91 [463]~E(x4631,x4632)+E(f75(x4633,x4631),f75(x4633,x4632)) % 0.89/0.91 [464]~E(x4641,x4642)+E(f107(x4641,x4643),f107(x4642,x4643)) % 0.89/0.91 [465]~E(x4651,x4652)+E(f107(x4653,x4651),f107(x4653,x4652)) % 0.89/0.91 [466]~E(x4661,x4662)+E(f124(x4661,x4663,x4664),f124(x4662,x4663,x4664)) % 0.89/0.91 [467]~E(x4671,x4672)+E(f124(x4673,x4671,x4674),f124(x4673,x4672,x4674)) % 0.89/0.91 [468]~E(x4681,x4682)+E(f124(x4683,x4684,x4681),f124(x4683,x4684,x4682)) % 0.89/0.91 [469]~E(x4691,x4692)+E(f46(x4691,x4693,x4694),f46(x4692,x4693,x4694)) % 0.89/0.91 [470]~E(x4701,x4702)+E(f46(x4703,x4701,x4704),f46(x4703,x4702,x4704)) % 0.89/0.91 [471]~E(x4711,x4712)+E(f46(x4713,x4714,x4711),f46(x4713,x4714,x4712)) % 0.89/0.91 [472]~E(x4721,x4722)+E(f106(x4721,x4723),f106(x4722,x4723)) % 0.89/0.91 [473]~E(x4731,x4732)+E(f106(x4733,x4731),f106(x4733,x4732)) % 0.89/0.91 [474]~E(x4741,x4742)+E(f73(x4741,x4743),f73(x4742,x4743)) % 0.89/0.91 [475]~E(x4751,x4752)+E(f73(x4753,x4751),f73(x4753,x4752)) % 0.89/0.91 [476]~E(x4761,x4762)+E(f93(x4761),f93(x4762)) % 0.89/0.91 [477]~P1(x4771)+P1(x4772)+~E(x4771,x4772) % 0.89/0.91 [478]~P2(x4781)+P2(x4782)+~E(x4781,x4782) % 0.89/0.91 % 0.89/0.91 %------------------------------------------- % 0.89/0.91 cnf(789,plain, % 0.89/0.91 ($false), % 0.89/0.91 inference(scs_inference,[],[570,553]), % 0.89/0.91 ['proof']). % 0.89/0.91 % SZS output end Proof % 0.89/0.91 % Total time :0.070000s %------------------------------------------------------------------------------