%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : ITP001+4 : TPTP v8.2.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n014.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 09:07:41 EDT 2024
% Result : Theorem 0.55s 0.72s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ITP001+4 : TPTP v8.2.0. Bugfixed v7.5.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n014.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 00:21:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.50/0.58 start to proof:theBenchmark
% 0.55/0.70 %-------------------------------------------
% 0.55/0.70 % File :CSE---1.7
% 0.55/0.70 % Problem :theBenchmark
% 0.55/0.70 % Transform :cnf
% 0.55/0.70 % Format :tptp:raw
% 0.55/0.70 % Command :java -jar mcs_scs.jar %d %s
% 0.55/0.70
% 0.55/0.70 % Result :Theorem 0.020000s
% 0.55/0.70 % Output :CNFRefutation 0.020000s
% 0.55/0.70 %-------------------------------------------
% 0.55/0.70 %------------------------------------------------------------------------------
% 0.55/0.70 % File : ITP001+4 : TPTP v8.2.0. Bugfixed v7.5.0.
% 0.55/0.70 % Domain : Interactive Theorem Proving
% 0.55/0.70 % Problem : HOL4 syntactic export of thm_2Ebool_2ETRUTH.p, chainy mode
% 0.55/0.70 % Version : [BG+19] axioms.
% 0.55/0.70 % English :
% 0.55/0.70
% 0.55/0.70 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.55/0.70 % : [Gau20] Gauthier (2020), Email to Geoff Sutcliffe
% 0.55/0.70 % Source : [BG+19]
% 0.55/0.70 % Names : thm_2Ebool_2ETRUTH.p [Gau20]
% 0.55/0.70 % : HL400001+4.p [TPAP]
% 0.55/0.70
% 0.55/0.70 % Status : Theorem
% 0.55/0.70 % Rating : 0.08 v8.1.0, 0.03 v7.5.0
% 0.55/0.70 % Syntax : Number of formulae : 87 ( 39 unt; 0 def)
% 0.55/0.70 % Number of atoms : 181 ( 68 equ)
% 0.55/0.70 % Maximal formula atoms : 9 ( 2 avg)
% 0.55/0.70 % Number of connectives : 102 ( 8 ~; 8 |; 14 &)
% 0.55/0.70 % ( 43 <=>; 29 =>; 0 <=; 0 <~>)
% 0.55/0.70 % Maximal formula depth : 12 ( 5 avg)
% 0.55/0.70 % Maximal term depth : 14 ( 2 avg)
% 0.55/0.70 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty)
% 0.55/0.70 % Number of functors : 54 ( 54 usr; 29 con; 0-3 aty)
% 0.55/0.71 % Number of variables : 243 ( 237 !; 6 ?)
% 0.55/0.71 % SPC : FOF_THM_RFO_SEQ
% 0.55/0.71
% 0.55/0.71 % Comments :
% 0.55/0.71 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.55/0.71 %------------------------------------------------------------------------------
% 0.55/0.71 include('Axioms/ITP001/ITP002+4.ax').
% 0.55/0.71 %------------------------------------------------------------------------------
% 0.55/0.71 fof(reserved_2Eho_2Eeq__ext,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0f_2E0,V1g_2E0] :
% 0.55/0.71 ( ! [V2x_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0),s(A_27a,V2x_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0)))
% 0.55/0.71 => s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0) = s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Eboolext,axiom,
% 0.55/0.71 ! [V0_2E0,V1_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,V0_2E0))
% 0.55/0.71 <=> p(s(tyop_2Emin_2Ebool,V1_2E0)) )
% 0.55/0.71 => s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Etruth,axiom,
% 0.55/0.71 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Enotfalse,axiom,
% 0.55/0.71 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Ebool__cases__ax,axiom,
% 0.55/0.71 ! [V0t_2E0] :
% 0.55/0.71 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
% 0.55/0.71 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Ei__thm,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27a),combin_i_2E0),s(A_27a,V0x_2E0))) = s(A_27a,V0x_2E0) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Ek__thm,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0x_2E0,V1y_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27a)),combin_k_2E0),s(A_27a,V0x_2E0))),s(A_27b,V1y_2E0))) = s(A_27a,V0x_2E0) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Eho_2Es__thm,axiom,
% 0.55/0.71 ! [A_27a,A_27b,A_27c,V0f_2E0,V1g_2E0,V2x_2E0] : s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27c),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c))),combin_s_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0))),s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0))),s(A_27a,V2x_2E0))) = s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27c),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0),s(A_27a,V2x_2E0))),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))))) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Elogic_2E_2F_5C,axiom,
% 0.55/0.71 ! [V0_2E0,V1_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0))))
% 0.55/0.71 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0))
% 0.55/0.71 & p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Elogic_2E_5C_2F,axiom,
% 0.55/0.71 ! [V0_2E0,V1_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0))))
% 0.55/0.71 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0))
% 0.55/0.71 | p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Elogic_2E_7E,axiom,
% 0.55/0.71 ! [V0_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0))))
% 0.55/0.71 <=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Elogic_2E_3D_3D_3E,axiom,
% 0.55/0.71 ! [V0_2E0,V1_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0))))
% 0.55/0.71 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Elogic_2E_3D,axiom,
% 0.55/0.71 ! [A_27a,V0_2E0,V1_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(A_27a,V0_2E0),s(A_27a,V1_2E0))))
% 0.55/0.71 <=> s(A_27a,V0_2E0) = s(A_27a,V1_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Equant_2E_21,axiom,
% 0.55/0.71 ! [A_27a,V0f_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0))))
% 0.55/0.71 <=> ! [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(reserved_2Equant_2E_3F,axiom,
% 0.55/0.71 ! [A_27a,V0f_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0))))
% 0.55/0.71 <=> ? [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom,
% 0.55/0.71 ! [X0_2E0,X1_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0))
% 0.55/0.71 & p(s(tyop_2Emin_2Ebool,X1_2E0)) )
% 0.55/0.71 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom,
% 0.55/0.71 ! [X0_2E0,X1_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0))
% 0.55/0.71 | p(s(tyop_2Emin_2Ebool,X1_2E0)) )
% 0.55/0.71 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom,
% 0.55/0.71 ! [X0_2E0] :
% 0.55/0.71 ( ~ p(s(tyop_2Emin_2Ebool,X0_2E0))
% 0.55/0.71 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom,
% 0.55/0.71 ! [X0_2E0,X1_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,X1_2E0)) )
% 0.55/0.71 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0] :
% 0.55/0.71 ( s(A_27a,X0_2E0) = s(A_27a,X1_2E0)
% 0.55/0.71 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(A_27a,X0_2E0))),s(A_27a,X1_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2E_3F_21_2E1_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_21_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Emin_2E_40_2E1_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0] : s(A_27a,c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(A_27a,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),A_27a),c_2Emin_2E_40_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2EBOUNDED_2E1,axiom,
% 0.55/0.71 ! [X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EBOUNDED_2E1(s(tyop_2Emin_2Ebool,X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2EBOUNDED_2E0),s(tyop_2Emin_2Ebool,X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2EDATATYPE_2E1_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EDATATYPE_2E1(s(A_27a,X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),c_2Ebool_2EDATATYPE_2E0),s(A_27a,X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2EONE__ONE_2E1_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 0.55/0.71 ! [A_27a,A_27b,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Ebool_2EONE__ONE_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2EONE__ONE_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind,axiom,
% 0.55/0.71 ! [X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),tyop_2Emin_2Ebool),c_2Ebool_2EONE__ONE_2E0),s(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2EONTO_2E1_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 0.55/0.71 ! [A_27a,A_27b,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Ebool_2EONTO_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq1_2Ec_2Ebool_2EONTO_2E1_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind,axiom,
% 0.55/0.71 ! [X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),tyop_2Emin_2Ebool),c_2Ebool_2EONTO_2E0),s(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),X0_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2EIN_2E2_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EIN_2E2(s(A_27a,X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Ebool_2EIN_2E0),s(A_27a,X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2ELET_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 0.55/0.71 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(A_27b,c_2Ebool_2ELET_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(A_27a,X1_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27b)),c_2Ebool_2ELET_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(A_27a,X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2ERES__EXISTS_2E2_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Ebool_2ERES__EXISTS_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2ERES__EXISTS__UNIQUE_2E2_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Ebool_2ERES__EXISTS__UNIQUE_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2ERES__FORALL_2E2_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Ebool_2ERES__FORALL_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2ERES__SELECT_2E2_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0] : s(A_27a,c_2Ebool_2ERES__SELECT_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) = s(A_27a,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),A_27a),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),A_27a)),c_2Ebool_2ERES__SELECT_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2ETYPE__DEFINITION_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 0.55/0.71 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2ETYPE__DEFINITION_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(A_27b,A_27a),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,A_27a),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,A_27a),tyop_2Emin_2Ebool)),c_2Ebool_2ETYPE__DEFINITION_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,A_27a),X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq2_2Ec_2Ebool_2Eliteral__case_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 0.55/0.71 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(A_27b,c_2Ebool_2Eliteral__case_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(A_27a,X1_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27b)),c_2Ebool_2Eliteral__case_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(A_27a,X1_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(arityeq3_2Ec_2Ebool_2ECOND_2E3_2Emono_2EA_27a,axiom,
% 0.55/0.71 ! [A_27a,X0_2E0,X1_2E0,X2_2E0] : s(A_27a,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,X0_2E0),s(A_27a,X1_2E0),s(A_27a,X2_2E0))) = s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27a),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,A_27a)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,A_27a))),c_2Ebool_2ECOND_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(A_27a,X1_2E0))),s(A_27a,X2_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EBOOL__CASES__AX,axiom,
% 0.55/0.71 ! [V0t_2E0] :
% 0.55/0.71 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
% 0.55/0.71 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EETA__AX,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0M_2E0,V1x_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0M_2E0),s(A_27a,V1x_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0M_2E0),s(A_27a,V1x_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ESELECT__AX,axiom,
% 0.55/0.71 ! [A_27a,V0P_2E0,V1x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V1x_2E0))))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0)))))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EINFINITY__AX,axiom,
% 0.55/0.71 ? [V0f_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),V0f_2E0))))
% 0.55/0.71 & ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Eind,tyop_2Emin_2Eind),V0f_2E0)))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ET__DEF,axiom,
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
% 0.55/0.71 <=> ! [V0x_2E0] : s(tyop_2Emin_2Ebool,V0x_2E0) = s(tyop_2Emin_2Ebool,V0x_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EFORALL__DEF,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))
% 0.55/0.71 <=> ! [V1x_2E0] : s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(A_27a,V1x_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EEXISTS__DEF,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(A_27a,c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EAND__DEF,axiom,
% 0.55/0.71 ! [V0x_2E0,V1x_27_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,V0x_2E0))
% 0.55/0.71 & p(s(tyop_2Emin_2Ebool,V1x_27_2E0)) )
% 0.55/0.71 <=> ! [V2t_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,V0x_2E0))
% 0.55/0.71 => ( p(s(tyop_2Emin_2Ebool,V1x_27_2E0))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,V2t_2E0)) ) )
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,V2t_2E0)) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EOR__DEF,axiom,
% 0.55/0.71 ! [V0x_2E0,V1x_27_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,V0x_2E0))
% 0.55/0.71 | p(s(tyop_2Emin_2Ebool,V1x_27_2E0)) )
% 0.55/0.71 <=> ! [V2t_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,V0x_2E0))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,V2t_2E0)) )
% 0.55/0.71 => ( ( p(s(tyop_2Emin_2Ebool,V1x_27_2E0))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,V2t_2E0)) )
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,V2t_2E0)) ) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EF__DEF,axiom,
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
% 0.55/0.71 <=> ! [V0t_2E0] : p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ENOT__DEF,axiom,
% 0.55/0.71 ! [V0x_2E0] :
% 0.55/0.71 ( ~ p(s(tyop_2Emin_2Ebool,V0x_2E0))
% 0.55/0.71 <=> ( p(s(tyop_2Emin_2Ebool,V0x_2E0))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EEXISTS__UNIQUE__DEF,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))
% 0.55/0.71 <=> ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))
% 0.55/0.71 & ! [V1x_2E0,V2y_2E0] :
% 0.55/0.71 ( ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(A_27a,V1x_2E0))))
% 0.55/0.71 & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(A_27a,V2y_2E0)))) )
% 0.55/0.71 => s(A_27a,V1x_2E0) = s(A_27a,V2y_2E0) ) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ELET__DEF,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0x_2E0,V1x_27_2E0] : s(A_27b,c_2Ebool_2ELET_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V1x_27_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V1x_27_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ECOND__DEF,axiom,
% 0.55/0.71 ! [A_27a,F0_2E0] :
% 0.55/0.71 ( ! [V0x_2E0,V1x_27_2E0,V2x_27_27_2E0,V3x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)))),F0_2E0),s(tyop_2Emin_2Ebool,V0x_2E0))),s(A_27a,V1x_27_2E0))),s(A_27a,V2x_27_27_2E0))),s(A_27a,V3x_2E0))))
% 0.55/0.71 <=> ( ( s(tyop_2Emin_2Ebool,V0x_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
% 0.55/0.71 => s(A_27a,V3x_2E0) = s(A_27a,V1x_27_2E0) )
% 0.55/0.71 & ( s(tyop_2Emin_2Ebool,V0x_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
% 0.55/0.71 => s(A_27a,V3x_2E0) = s(A_27a,V2x_27_27_2E0) ) ) )
% 0.55/0.71 => ! [V0x_2E0,V1x_27_2E0,V2x_27_27_2E0] : s(A_27a,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,V0x_2E0),s(A_27a,V1x_27_2E0),s(A_27a,V2x_27_27_2E0))) = s(A_27a,c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)))),F0_2E0),s(tyop_2Emin_2Ebool,V0x_2E0))),s(A_27a,V1x_27_2E0))),s(A_27a,V2x_27_27_2E0))))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EONE__ONE__DEF,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EONE__ONE_2E1(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0))))
% 0.55/0.71 <=> ! [V1x1_2E0,V2x2_2E0] :
% 0.55/0.71 ( s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V1x1_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V2x2_2E0)))
% 0.55/0.71 => s(A_27a,V1x1_2E0) = s(A_27a,V2x2_2E0) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EONTO__DEF,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EONTO_2E1(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0))))
% 0.55/0.71 <=> ! [V1y_2E0] :
% 0.55/0.71 ? [V2x_2E0] : s(A_27b,V1y_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V2x_2E0))) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ETYPE__DEFINITION,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0x_2E0,V1x_27_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ETYPE__DEFINITION_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27b,A_27a),V1x_27_2E0))))
% 0.55/0.71 <=> ( ! [V2x_27_2E0,V3x_27_27_2E0] :
% 0.55/0.71 ( s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V1x_27_2E0),s(A_27b,V2x_27_2E0))) = s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V1x_27_2E0),s(A_27b,V3x_27_27_2E0)))
% 0.55/0.71 => s(A_27b,V2x_27_2E0) = s(A_27b,V3x_27_27_2E0) )
% 0.55/0.71 & ! [V4x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(A_27a,V4x_2E0))))
% 0.55/0.71 <=> ? [V5x_27_2E0] : s(A_27a,V4x_2E0) = s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V1x_27_2E0),s(A_27b,V5x_27_2E0))) ) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2Eliteral__case__DEF,axiom,
% 0.55/0.71 ! [A_27a,A_27b,V0x_2E0,V1x_27_2E0] : s(A_27b,c_2Ebool_2Eliteral__case_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V1x_27_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0x_2E0),s(A_27a,V1x_27_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2EIN__DEF,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0,V1x_27_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EIN_2E2(s(A_27a,V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V0x_2E0))) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ERES__FORALL__DEF,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0,V1x_27_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))))
% 0.55/0.71 <=> ! [V2x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EIN_2E2(s(A_27a,V2x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))
% 0.55/0.71 => p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V2x_2E0)))) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ERES__EXISTS__DEF,axiom,
% 0.55/0.71 ! [A_27a,V0x_2E0,V1x_27_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))))
% 0.55/0.71 <=> ? [V2x_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EIN_2E2(s(A_27a,V2x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))
% 0.55/0.71 & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V2x_2E0)))) ) ) ).
% 0.55/0.71
% 0.55/0.71 fof(thm_2Ebool_2ERES__EXISTS__UNIQUE__DEF,axiom,
% 0.55/0.71 ! [A_27a,F2_2E0,F1_2E0,F0_2E0] :
% 0.55/0.71 ( ! [V1x_27_2E0,V3x_2E0,V4y_2E0] :
% 0.55/0.71 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),F2_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))),s(A_27a,V3x_2E0))),s(A_27a,V4y_2E0))))
% 0.55/0.71 <=> ( ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V3x_2E0))))
% 0.55/0.71 & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V4y_2E0)))) )
% 0.55/0.71 => s(A_27a,V3x_2E0) = s(A_27a,V4y_2E0) ) )
% 0.55/0.71 => ( ! [V0x_2E0,V1x_27_2E0,V3x_2E0] : s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),F1_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))),s(A_27a,V3x_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),F2_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))),s(A_27a,V3x_2E0)))))
% 0.55/0.71 => ( ! [V1x_27_2E0,V2x_2E0] : s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),F0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))),s(A_27a,V2x_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V2x_2E0)))
% 0.55/0.72 => ! [V0x_2E0,V1x_27_2E0] :
% 0.55/0.72 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__EXISTS__UNIQUE_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))))
% 0.55/0.72 <=> ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),F0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))))))
% 0.55/0.72 & p(s(tyop_2Emin_2Ebool,c_2Ebool_2ERES__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),F1_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0)))))) ) ) ) ) ) ).
% 0.55/0.72
% 0.55/0.72 fof(thm_2Ebool_2ERES__SELECT__DEF,axiom,
% 0.55/0.72 ! [A_27a,F0_2E0] :
% 0.55/0.72 ( ! [V0x_2E0,V1x_27_2E0,V2x_2E0] :
% 0.55/0.72 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),F0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))),s(A_27a,V2x_2E0))))
% 0.55/0.72 <=> ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EIN_2E2(s(A_27a,V2x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))))
% 0.55/0.72 & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0),s(A_27a,V2x_2E0)))) ) )
% 0.55/0.72 => ! [V0x_2E0,V1x_27_2E0] : s(A_27a,c_2Ebool_2ERES__SELECT_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))) = s(A_27a,c_2Emin_2E_40_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool))),F0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0x_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1x_27_2E0))))) ) ).
% 0.55/0.72
% 0.55/0.72 fof(thm_2Ebool_2EBOUNDED__DEF,axiom,
% 0.55/0.72 ! [V0x_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EBOUNDED_2E1(s(tyop_2Emin_2Ebool,V0x_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ).
% 0.55/0.72
% 0.55/0.72 fof(thm_2Ebool_2EDATATYPE__TAG__DEF,axiom,
% 0.55/0.72 ! [A_27a,V0x_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2EDATATYPE_2E1(s(A_27a,V0x_2E0))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ).
% 0.55/0.72
% 0.55/0.72 fof(thm_2Ebool_2ETRUTH,conjecture,
% 0.55/0.72 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ).
% 0.55/0.72
% 0.55/0.72 %------------------------------------------------------------------------------
% 0.55/0.72 %-------------------------------------------
% 0.55/0.72 % Proof found
% 0.55/0.72 % SZS status Theorem for theBenchmark
% 0.55/0.72 % SZS output start Proof
% 0.55/0.72 %ClaNum:312(EqnAxiom:149)
% 0.55/0.72 %VarNum:2637(SingletonVarNum:375)
% 0.55/0.72 %MaxLitNum:9
% 0.55/0.72 %MaxfuncDepth:6
% 0.55/0.72 %SharedTerms:57
% 0.55/0.72 %goalClause: 187
% 0.55/0.72 %singleGoalClaCount:1
% 0.55/0.72 [152]P1(f29(a1,a2))
% 0.55/0.72 [187]~P1(f29(a1,a2))
% 0.55/0.72 [189]~P1(f29(a1,a13))
% 0.55/0.72 [158]P1(f29(a1,f10(f29(f92(a93,a93),a51))))
% 0.55/0.72 [190]~P1(f29(a1,f18(f29(f92(a93,a93),a51))))
% 0.55/0.72 [153]E(f29(a1,f3(f29(a1,x1531))),f29(a1,a2))
% 0.55/0.72 [157]E(f29(a1,f4(f29(f92(a1,a1),a5),f29(a1,x1571))),f29(a1,f3(f29(a1,x1571))))
% 0.55/0.72 [154]E(f29(a1,f6(f29(x1541,x1542))),f29(a1,a2))
% 0.55/0.72 [156]E(f29(x1561,f4(f29(f92(x1561,x1561),a30),f29(x1561,x1562))),f29(x1561,x1562))
% 0.55/0.72 [159]E(f29(a1,f4(f29(f92(x1591,a1),a7),f29(x1591,x1592))),f29(a1,f6(f29(x1591,x1592))))
% 0.55/0.72 [166]E(f29(a1,f4(f29(f92(f92(x1661,a1),a1),a32),f29(f92(x1661,a1),x1662))),f29(a1,f33(f29(f92(x1661,a1),x1662))))
% 0.55/0.72 [168]E(f29(a1,f4(f29(f92(f92(x1681,a1),a1),a34),f29(f92(x1681,a1),x1682))),f29(a1,f39(f29(f92(x1681,a1),x1682))))
% 0.55/0.72 [169]E(f29(a1,f4(f29(f92(f92(x1691,a1),a1),a35),f29(f92(x1691,a1),x1692))),f29(a1,f38(f29(f92(x1691,a1),x1692))))
% 0.55/0.72 [170]E(f29(x1701,f4(f29(f92(f92(x1701,a1),x1701),a45),f29(f92(x1701,a1),x1702))),f29(x1701,f50(f29(f92(x1701,a1),x1702))))
% 0.55/0.72 [173]E(f29(a1,f4(f29(f92(x1731,a1),x1732),f29(x1731,f50(f29(f92(x1731,a1),x1732))))),f29(a1,f39(f29(f92(x1731,a1),x1732))))
% 0.55/0.72 [160]E(f29(a1,f11(f29(x1601,x1602),f29(f92(x1601,a1),x1603))),f29(a1,f4(f29(f92(x1601,a1),x1603),f29(x1601,x1602))))
% 0.55/0.72 [171]E(f29(a1,f4(f29(f92(f92(x1711,x1712),a1),a16),f29(f92(x1711,x1712),x1713))),f29(a1,f10(f29(f92(x1711,x1712),x1713))))
% 0.55/0.72 [172]E(f29(a1,f4(f29(f92(f92(x1721,x1722),a1),a17),f29(f92(x1721,x1722),x1723))),f29(a1,f18(f29(f92(x1721,x1722),x1723))))
% 0.55/0.72 [178]E(f29(a1,f4(f29(f92(f92(x1781,a1),a1),f4(f29(f92(x1781,f92(f92(x1781,a1),a1)),a12),f29(x1781,x1782))),f29(f92(x1781,a1),x1783))),f29(a1,f11(f29(x1781,x1782),f29(f92(x1781,a1),x1783))))
% 0.55/0.72 [179]E(f29(a1,f4(f29(f92(f92(x1791,a1),a1),f4(f29(f92(f92(x1791,a1),f92(f92(x1791,a1),a1)),a19),f29(f92(x1791,a1),x1792))),f29(f92(x1791,a1),x1793))),f29(a1,f20(f29(f92(x1791,a1),x1792),f29(f92(x1791,a1),x1793))))
% 0.55/0.72 [180]E(f29(a1,f4(f29(f92(f92(x1801,a1),a1),f4(f29(f92(f92(x1801,a1),f92(f92(x1801,a1),a1)),a21),f29(f92(x1801,a1),x1802))),f29(f92(x1801,a1),x1803))),f29(a1,f22(f29(f92(x1801,a1),x1802),f29(f92(x1801,a1),x1803))))
% 0.55/0.72 [181]E(f29(a1,f4(f29(f92(f92(x1811,a1),a1),f4(f29(f92(f92(x1811,a1),f92(f92(x1811,a1),a1)),a23),f29(f92(x1811,a1),x1812))),f29(f92(x1811,a1),x1813))),f29(a1,f24(f29(f92(x1811,a1),x1812),f29(f92(x1811,a1),x1813))))
% 0.55/0.72 [182]E(f29(x1821,f4(f29(f92(f92(x1821,a1),x1821),f4(f29(f92(f92(x1821,a1),f92(f92(x1821,a1),x1821)),a25),f29(f92(x1821,a1),x1822))),f29(f92(x1821,a1),x1823))),f29(x1821,f26(f29(f92(x1821,a1),x1822),f29(f92(x1821,a1),x1823))))
% 0.55/0.72 [161]E(f29(x1611,f14(f29(f92(x1612,x1611),x1613),f29(x1612,x1614))),f29(x1611,f4(f29(f92(x1612,x1611),x1613),f29(x1612,x1614))))
% 0.55/0.72 [162]E(f29(x1621,f31(f29(f92(x1622,x1621),x1623),f29(x1622,x1624))),f29(x1621,f4(f29(f92(x1622,x1621),x1623),f29(x1622,x1624))))
% 0.55/0.72 [175]E(f29(x1751,f4(f29(f92(x1752,x1751),f4(f29(f92(x1751,f92(x1752,x1751)),a52),f29(x1751,x1753))),f29(x1752,x1754))),f29(x1751,x1753))
% 0.55/0.72 [176]E(f29(x1761,f4(f29(f92(x1762,x1761),f4(f29(f92(f92(x1762,x1761),f92(x1762,x1761)),a15),f29(f92(x1762,x1761),x1763))),f29(x1762,x1764))),f29(x1761,f14(f29(f92(x1762,x1761),x1763),f29(x1762,x1764))))
% 0.55/0.72 [177]E(f29(x1771,f4(f29(f92(x1772,x1771),f4(f29(f92(f92(x1772,x1771),f92(x1772,x1771)),a40),f29(f92(x1772,x1771),x1773))),f29(x1772,x1774))),f29(x1771,f31(f29(f92(x1772,x1771),x1773),f29(x1772,x1774))))
% 0.55/0.72 [184]E(f29(x1841,f4(f29(f92(x1841,x1841),f4(f29(f92(x1841,f92(x1841,x1841)),f4(f29(f92(a1,f92(x1841,f92(x1841,x1841))),a8),f29(a1,x1842))),f29(x1841,x1843))),f29(x1841,x1844))),f29(x1841,f9(f29(a1,x1842),f29(x1841,x1843),f29(x1841,x1844))))
% 0.55/0.72 [183]E(f29(a1,f4(f29(f92(f92(x1831,x1832),a1),f4(f29(f92(f92(x1832,a1),f92(f92(x1831,x1832),a1)),a27),f29(f92(x1832,a1),x1833))),f29(f92(x1831,x1832),x1834))),f29(a1,f28(f29(f92(x1832,a1),x1833),f29(f92(x1831,x1832),x1834))))
% 0.55/0.72 [185]E(f29(x1851,f4(f29(f92(x1852,x1851),f4(f29(f92(f92(x1852,x1853),f92(x1852,x1851)),f4(f29(f92(f92(x1852,f92(x1853,x1851)),f92(f92(x1852,x1853),f92(x1852,x1851))),a53),f29(f92(x1852,f92(x1853,x1851)),x1854))),f29(f92(x1852,x1853),x1855))),f29(x1852,x1856))),f29(x1851,f4(f29(f92(x1853,x1851),f4(f29(f92(x1852,f92(x1853,x1851)),x1854),f29(x1852,x1856))),f29(x1853,f4(f29(f92(x1852,x1853),x1855),f29(x1852,x1856))))))
% 0.55/0.72 [186]E(f29(x1861,f4(f29(f92(x1862,x1861),f4(f29(f92(f92(x1862,x1863),f92(x1862,x1861)),f4(f29(f92(f92(x1862,f92(x1863,x1861)),f92(f92(x1862,x1863),f92(x1862,x1861))),a53),f29(f92(x1862,f92(x1863,x1861)),x1864))),f29(f92(x1862,x1863),x1865))),f29(x1862,x1866))),f29(x1861,f4(f29(f92(x1863,x1861),f4(f29(f92(x1862,f92(x1863,x1861)),x1864),f29(x1862,x1866))),f29(x1863,f4(f29(f92(x1862,x1863),x1865),f29(x1862,x1866))))))
% 0.55/0.72 [194]P1(f29(a1,a13))+~P1(f29(a1,a54))
% 0.55/0.72 [193]E(f29(a1,x1931),f29(a1,a13))+E(f29(a1,x1931),f29(a1,a2))
% 0.55/0.72 [204]P1(f29(a1,x2041))+P1(f29(a1,f41(f29(a1,x2041))))
% 0.55/0.72 [207]~P1(f29(a1,x2071))+~P1(f29(a1,f41(f29(a1,x2071))))
% 0.55/0.72 [225]P1(f29(a1,x2251))+P1(f29(a1,f4(f29(f92(a1,a1),a44),f29(a1,x2251))))
% 0.55/0.72 [233]~P1(f29(a1,x2331))+~P1(f29(a1,f4(f29(f92(a1,a1),a44),f29(a1,x2331))))
% 0.55/0.72 [201]P1(f29(a1,x2011))+~P1(f29(a1,f55(x2012,x2011)))
% 0.55/0.72 [202]P1(f29(a1,x2021))+~P1(f29(a1,f55(x2021,x2022)))
% 0.55/0.72 [209]P1(f29(a1,x2091))+P1(f29(a1,f46(f29(a1,x2091),f29(a1,x2092))))
% 0.55/0.72 [211]~P1(f29(a1,x2112))+P1(f29(a1,f42(f29(a1,x2111),f29(a1,x2112))))
% 0.55/0.72 [213]~P1(f29(a1,x2131))+P1(f29(a1,f42(f29(a1,x2131),f29(a1,x2132))))
% 0.55/0.72 [215]~P1(f29(a1,x2152))+P1(f29(a1,f46(f29(a1,x2151),f29(a1,x2152))))
% 0.55/0.72 [221]P1(f29(a1,x2211))+~P1(f29(a1,f36(f29(a1,x2212),f29(a1,x2211))))
% 0.55/0.72 [223]P1(f29(a1,x2231))+~P1(f29(a1,f36(f29(a1,x2231),f29(a1,x2232))))
% 0.55/0.72 [264]P1(f29(a1,x2641))+P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a49),f29(a1,x2641))),f29(a1,x2642))))
% 0.55/0.72 [266]~P1(f29(a1,x2662))+P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a43),f29(a1,x2661))),f29(a1,x2662))))
% 0.55/0.72 [268]~P1(f29(a1,x2681))+P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a43),f29(a1,x2681))),f29(a1,x2682))))
% 0.55/0.72 [270]~P1(f29(a1,x2702))+P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a49),f29(a1,x2701))),f29(a1,x2702))))
% 0.55/0.72 [276]P1(f29(a1,x2761))+~P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a37),f29(a1,x2762))),f29(a1,x2761))))
% 0.55/0.72 [278]P1(f29(a1,x2781))+~P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a37),f29(a1,x2781))),f29(a1,x2782))))
% 0.55/0.72 [236]~P1(f29(a1,f38(f29(f92(x2361,a1),x2362))))+P1(f29(a1,f39(f29(f92(x2361,a1),x2362))))
% 0.55/0.72 [237]~E(f29(a1,f4(f29(f92(x2371,a1),x2372),f29(x2371,f91(x2371,x2372)))),f29(a1,a2))+P1(f29(a1,f33(f29(f92(x2371,a1),x2372))))
% 0.55/0.72 [244]P1(f29(a1,f4(f29(f92(x2441,a1),x2442),f29(x2441,f68(x2441,x2442)))))+~P1(f29(a1,f39(f29(f92(x2441,a1),x2442))))
% 0.55/0.72 [245]P1(f29(a1,f4(f29(f92(x2451,a1),x2452),f29(x2451,f87(x2451,x2452)))))+~P1(f29(a1,f39(f29(f92(x2451,a1),x2452))))
% 0.55/0.72 [247]~P1(f29(a1,f4(f29(f92(x2471,a1),x2472),f29(x2471,f69(x2471,x2472)))))+P1(f29(a1,f33(f29(f92(x2471,a1),x2472))))
% 0.55/0.72 [248]~P1(f29(a1,f4(f29(f92(x2481,a1),x2482),f29(x2481,f88(x2481,x2482)))))+P1(f29(a1,f33(f29(f92(x2481,a1),x2482))))
% 0.55/0.72 [217]~E(f29(x2171,x2172),f29(x2171,x2173))+P1(f29(a1,f47(f29(x2171,x2172),f29(x2171,x2173))))
% 0.55/0.72 [229]E(f29(x2291,x2292),f29(x2291,x2293))+~P1(f29(a1,f47(f29(x2291,x2292),f29(x2291,x2293))))
% 0.55/0.72 [274]~E(f29(x2741,x2742),f29(x2741,x2743))+P1(f29(a1,f4(f29(f92(x2741,a1),f4(f29(f92(x2741,f92(x2741,a1)),a48),f29(x2741,x2742))),f29(x2741,x2743))))
% 0.55/0.72 [284]E(f29(x2841,x2842),f29(x2841,x2843))+~P1(f29(a1,f4(f29(f92(x2841,a1),f4(f29(f92(x2841,f92(x2841,a1)),a48),f29(x2841,x2842))),f29(x2841,x2843))))
% 0.55/0.72 [234]~E(f29(x2341,f57(x2341,x2342,x2343)),f29(x2341,f64(x2341,x2342,x2343)))+P1(f29(a1,f10(f29(f92(x2341,x2342),x2343))))
% 0.55/0.72 [235]E(f29(a1,f4(f29(f92(x2351,a1),x2352),f29(x2351,x2353))),f29(a1,a2))+~P1(f29(a1,f33(f29(f92(x2351,a1),x2352))))
% 0.55/0.72 [241]P1(f29(a1,f4(f29(f92(x2411,a1),x2412),f29(x2411,x2413))))+~P1(f29(a1,f33(f29(f92(x2411,a1),x2412))))
% 0.55/0.72 [243]~P1(f29(a1,f4(f29(f92(x2431,a1),x2432),f29(x2431,x2433))))+P1(f29(a1,f39(f29(f92(x2431,a1),x2432))))
% 0.55/0.72 [251]E(f29(x2511,f4(f29(f92(x2512,x2511),x2513),f29(x2512,f57(x2512,x2511,x2513)))),f29(x2511,f4(f29(f92(x2512,x2511),x2513),f29(x2512,f64(x2512,x2511,x2513)))))+P1(f29(a1,f10(f29(f92(x2512,x2511),x2513))))
% 0.55/0.72 [254]P1(f29(a1,f24(f29(f92(x2541,a1),x2542),f29(f92(x2541,a1),x2543))))+P1(f29(a1,f11(f29(x2541,f70(x2541,x2542,x2543)),f29(f92(x2541,a1),x2542))))
% 0.55/0.72 [258]~P1(f29(a1,f20(f29(f92(x2581,a1),x2582),f29(f92(x2581,a1),x2583))))+P1(f29(a1,f11(f29(x2581,f76(x2581,x2582,x2583)),f29(f92(x2581,a1),x2582))))
% 0.55/0.72 [259]P1(f29(a1,f4(f29(f92(x2591,a1),x2592),f29(x2591,f76(x2591,x2593,x2592)))))+~P1(f29(a1,f20(f29(f92(x2591,a1),x2593),f29(f92(x2591,a1),x2592))))
% 0.55/0.72 [261]~P1(f29(a1,f4(f29(f92(x2611,a1),x2613),f29(x2611,f70(x2611,x2612,x2613)))))+P1(f29(a1,f24(f29(f92(x2611,a1),x2612),f29(f92(x2611,a1),x2613))))
% 0.55/0.72 [260]~P1(f29(a1,f4(f29(f92(x2601,a1),x2602),f29(x2601,x2603))))+P1(f29(a1,f4(f29(f92(x2601,a1),x2602),f29(x2601,f50(f29(f92(x2601,a1),x2602))))))
% 0.55/0.72 [238]~E(f29(x2382,f4(f29(f92(x2381,x2382),x2383),f29(x2381,x2384))),f29(x2382,f66(x2381,x2382,x2383)))+P1(f29(a1,f18(f29(f92(x2381,x2382),x2383))))
% 0.55/0.72 [262]E(f29(x2621,f4(f29(f92(x2622,x2621),x2623),f29(x2622,f67(x2622,x2621,x2623,x2624)))),f29(x2621,x2624))+~P1(f29(a1,f18(f29(f92(x2622,x2621),x2623))))
% 0.55/0.72 [285]E(f29(f92(x2851,x2852),x2853),f29(f92(x2851,x2852),x2854))+~E(f29(x2852,f4(f29(f92(x2851,x2852),x2853),f29(x2851,f65(x2851,x2852,x2853,x2854)))),f29(x2852,f4(f29(f92(x2851,x2852),x2854),f29(x2851,f65(x2851,x2852,x2853,x2854)))))
% 0.55/0.72 [286]E(f29(f92(x2861,x2862),x2863),f29(f92(x2861,x2862),x2864))+~E(f29(x2862,f4(f29(f92(x2861,x2862),x2863),f29(x2861,f89(x2861,x2862,x2863,x2864)))),f29(x2862,f4(f29(f92(x2861,x2862),x2864),f29(x2861,f89(x2861,x2862,x2863,x2864)))))
% 0.55/0.72 [197]E(f29(a1,x1971),f29(a1,x1972))+P1(f29(a1,x1971))+P1(f29(a1,x1972))
% 0.55/0.72 [200]E(f29(a1,x2001),f29(a1,x2002))+~P1(f29(a1,x2001))+~P1(f29(a1,x2002))
% 0.55/0.72 [205]P1(f29(a1,x2051))+P1(f29(a1,x2052))+~P1(f29(a1,f56(x2052,x2051)))
% 0.55/0.72 [219]~P1(f29(a1,x2191))+~P1(f29(a1,x2192))+P1(f29(a1,f36(f29(a1,x2191),f29(a1,x2192))))
% 0.55/0.72 [227]P1(f29(a1,x2271))+P1(f29(a1,x2272))+~P1(f29(a1,f42(f29(a1,x2272),f29(a1,x2271))))
% 0.55/0.72 [231]P1(f29(a1,x2311))+~P1(f29(a1,x2312))+~P1(f29(a1,f46(f29(a1,x2312),f29(a1,x2311))))
% 0.55/0.72 [272]~P1(f29(a1,x2721))+~P1(f29(a1,x2722))+P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a37),f29(a1,x2721))),f29(a1,x2722))))
% 0.55/0.72 [280]P1(f29(a1,x2801))+P1(f29(a1,x2802))+~P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a43),f29(a1,x2802))),f29(a1,x2801))))
% 0.55/0.72 [282]P1(f29(a1,x2821))+~P1(f29(a1,x2822))+~P1(f29(a1,f4(f29(f92(a1,a1),f4(f29(f92(a1,f92(a1,a1)),a49),f29(a1,x2822))),f29(a1,x2821))))
% 0.55/0.72 [239]~E(f29(x2391,f58(x2391,x2392)),f29(x2391,f59(x2391,x2392)))+~P1(f29(a1,f39(f29(f92(x2391,a1),x2392))))+P1(f29(a1,f38(f29(f92(x2391,a1),x2392))))
% 0.55/0.72 [249]P1(f29(a1,f4(f29(f92(x2491,a1),x2492),f29(x2491,f59(x2491,x2492)))))+~P1(f29(a1,f39(f29(f92(x2491,a1),x2492))))+P1(f29(a1,f38(f29(f92(x2491,a1),x2492))))
% 0.55/0.72 [250]P1(f29(a1,f4(f29(f92(x2501,a1),x2502),f29(x2501,f58(x2501,x2502)))))+~P1(f29(a1,f39(f29(f92(x2501,a1),x2502))))+P1(f29(a1,f38(f29(f92(x2501,a1),x2502))))
% 0.55/0.72 [256]~P1(f29(a1,f4(f29(f92(x2561,a1),x2563),f29(x2561,x2564))))+~P1(f29(a1,f11(f29(x2561,x2564),f29(f92(x2561,a1),x2562))))+P1(f29(a1,f20(f29(f92(x2561,a1),x2562),f29(f92(x2561,a1),x2563))))
% 0.55/0.72 [257]P1(f29(a1,f4(f29(f92(x2571,a1),x2572),f29(x2571,x2573))))+~P1(f29(a1,f11(f29(x2571,x2573),f29(f92(x2571,a1),x2574))))+~P1(f29(a1,f24(f29(f92(x2571,a1),x2574),f29(f92(x2571,a1),x2572))))
% 0.55/0.72 [292]E(f29(x2921,f50(f29(f92(x2921,a1),f4(f29(f92(f92(x2921,a1),f92(x2921,a1)),f4(f29(f92(f92(x2921,a1),f92(f92(x2921,a1),f92(x2921,a1))),x2922),f29(f92(x2921,a1),x2923))),f29(f92(x2921,a1),x2924))))),f29(x2921,f26(f29(f92(x2921,a1),x2923),f29(f92(x2921,a1),x2924))))+P1(f29(a1,f11(f29(x2921,f90(x2921,x2922)),f29(f92(x2921,a1),f77(x2921,x2922)))))+P1(f29(a1,f4(f29(f92(x2921,a1),f4(f29(f92(f92(x2921,a1),f92(x2921,a1)),f4(f29(f92(f92(x2921,a1),f92(f92(x2921,a1),f92(x2921,a1))),x2922),f29(f92(x2921,a1),f77(x2921,x2922)))),f29(f92(x2921,a1),f86(x2921,x2922)))),f29(x2921,f90(x2921,x2922)))))
% 0.55/0.72 [293]E(f29(x2931,f50(f29(f92(x2931,a1),f4(f29(f92(f92(x2931,a1),f92(x2931,a1)),f4(f29(f92(f92(x2931,a1),f92(f92(x2931,a1),f92(x2931,a1))),x2932),f29(f92(x2931,a1),x2933))),f29(f92(x2931,a1),x2934))))),f29(x2931,f26(f29(f92(x2931,a1),x2933),f29(f92(x2931,a1),x2934))))+P1(f29(a1,f4(f29(f92(x2931,a1),f86(x2931,x2932)),f29(x2931,f90(x2931,x2932)))))+P1(f29(a1,f4(f29(f92(x2931,a1),f4(f29(f92(f92(x2931,a1),f92(x2931,a1)),f4(f29(f92(f92(x2931,a1),f92(f92(x2931,a1),f92(x2931,a1))),x2932),f29(f92(x2931,a1),f77(x2931,x2932)))),f29(f92(x2931,a1),f86(x2931,x2932)))),f29(x2931,f90(x2931,x2932)))))
% 0.55/0.72 [246]E(f29(x2461,x2462),f29(x2461,x2463))+~E(f29(x2464,f4(f29(f92(x2461,x2464),x2465),f29(x2461,x2462))),f29(x2464,f4(f29(f92(x2461,x2464),x2465),f29(x2461,x2463))))+~P1(f29(a1,f10(f29(f92(x2461,x2464),x2465))))
% 0.55/0.72 [289]E(f29(x2891,f4(f29(f92(x2892,x2891),x2893),f29(x2892,f74(x2891,x2892,x2894,x2893,x2895)))),f29(x2891,x2895))+~P1(f29(a1,f4(f29(f92(x2891,a1),x2894),f29(x2891,x2895))))+~P1(f29(a1,f28(f29(f92(x2891,a1),x2894),f29(f92(x2892,x2891),x2893))))
% 0.55/0.72 [252]E(f29(x2521,x2522),f29(x2521,x2523))+~E(f29(x2524,f4(f29(f92(x2521,x2524),x2525),f29(x2521,x2522))),f29(x2524,f4(f29(f92(x2521,x2524),x2525),f29(x2521,x2523))))+~P1(f29(a1,f28(f29(f92(x2524,a1),x2526),f29(f92(x2521,x2524),x2525))))
% 0.55/0.72 [253]~E(f29(x2531,x2533),f29(x2531,f4(f29(f92(x2534,x2531),x2535),f29(x2534,x2536))))+P1(f29(a1,f4(f29(f92(x2531,a1),x2532),f29(x2531,x2533))))+~P1(f29(a1,f28(f29(f92(x2531,a1),x2532),f29(f92(x2534,x2531),x2535))))
% 0.55/0.72 [255]E(f29(x2551,x2552),f29(x2551,x2553))+~P1(f29(a1,f4(f29(f92(x2551,a1),x2554),f29(x2551,x2552))))+~P1(f29(a1,f4(f29(f92(x2551,a1),x2554),f29(x2551,x2553))))+~P1(f29(a1,f38(f29(f92(x2551,a1),x2554))))
% 0.55/0.72 [287]~E(f29(x2872,f73(x2871,x2872,x2874,x2873)),f29(x2872,f75(x2871,x2872,x2874,x2873)))+E(f29(x2871,f4(f29(f92(x2872,x2871),x2873),f29(x2872,f71(x2871,x2872,x2874,x2873)))),f29(x2871,f72(x2871,x2872,x2874,x2873)))+P1(f29(a1,f4(f29(f92(x2871,a1),x2874),f29(x2871,f72(x2871,x2872,x2874,x2873)))))+P1(f29(a1,f28(f29(f92(x2871,a1),x2874),f29(f92(x2872,x2871),x2873))))
% 0.55/0.72 [290]E(f29(x2901,f4(f29(f92(x2902,x2901),x2903),f29(x2902,f73(x2901,x2902,x2904,x2903)))),f29(x2901,f4(f29(f92(x2902,x2901),x2903),f29(x2902,f75(x2901,x2902,x2904,x2903)))))+E(f29(x2901,f4(f29(f92(x2902,x2901),x2903),f29(x2902,f71(x2901,x2902,x2904,x2903)))),f29(x2901,f72(x2901,x2902,x2904,x2903)))+P1(f29(a1,f4(f29(f92(x2901,a1),x2904),f29(x2901,f72(x2901,x2902,x2904,x2903)))))+P1(f29(a1,f28(f29(f92(x2901,a1),x2904),f29(f92(x2902,x2901),x2903))))
% 0.55/0.72 [294]E(f29(x2941,f50(f29(f92(x2941,a1),f4(f29(f92(f92(x2941,a1),f92(x2941,a1)),f4(f29(f92(f92(x2941,a1),f92(f92(x2941,a1),f92(x2941,a1))),x2942),f29(f92(x2941,a1),x2943))),f29(f92(x2941,a1),x2944))))),f29(x2941,f26(f29(f92(x2941,a1),x2943),f29(f92(x2941,a1),x2944))))+~P1(f29(a1,f4(f29(f92(x2941,a1),f86(x2941,x2942)),f29(x2941,f90(x2941,x2942)))))+~P1(f29(a1,f11(f29(x2941,f90(x2941,x2942)),f29(f92(x2941,a1),f77(x2941,x2942)))))+~P1(f29(a1,f4(f29(f92(x2941,a1),f4(f29(f92(f92(x2941,a1),f92(x2941,a1)),f4(f29(f92(f92(x2941,a1),f92(f92(x2941,a1),f92(x2941,a1))),x2942),f29(f92(x2941,a1),f77(x2941,x2942)))),f29(f92(x2941,a1),f86(x2941,x2942)))),f29(x2941,f90(x2941,x2942)))))
% 0.55/0.72 [288]~E(f29(x2883,f73(x2881,x2883,x2882,x2884)),f29(x2883,f75(x2881,x2883,x2882,x2884)))+~E(f29(x2881,f72(x2881,x2883,x2882,x2884)),f29(x2881,f4(f29(f92(x2883,x2881),x2884),f29(x2883,x2885))))+~P1(f29(a1,f4(f29(f92(x2881,a1),x2882),f29(x2881,f72(x2881,x2883,x2882,x2884)))))+P1(f29(a1,f28(f29(f92(x2881,a1),x2882),f29(f92(x2883,x2881),x2884))))
% 0.55/0.72 [291]~E(f29(x2911,f72(x2911,x2912,x2914,x2913)),f29(x2911,f4(f29(f92(x2912,x2911),x2913),f29(x2912,x2915))))+E(f29(x2911,f4(f29(f92(x2912,x2911),x2913),f29(x2912,f73(x2911,x2912,x2914,x2913)))),f29(x2911,f4(f29(f92(x2912,x2911),x2913),f29(x2912,f75(x2911,x2912,x2914,x2913)))))+~P1(f29(a1,f4(f29(f92(x2911,a1),x2914),f29(x2911,f72(x2911,x2912,x2914,x2913)))))+P1(f29(a1,f28(f29(f92(x2911,a1),x2914),f29(f92(x2912,x2911),x2913))))
% 0.55/0.72 [307]E(f29(x3071,f60(x3071,x3072)),f29(x3071,f62(x3071,x3072)))+~E(f29(a1,f61(x3071,x3072)),f29(a1,a2))+E(f29(x3071,f50(f29(f92(x3071,a1),f4(f29(f92(x3071,f92(x3071,a1)),f4(f29(f92(x3071,f92(x3071,f92(x3071,a1))),f4(f29(f92(a1,f92(x3071,f92(x3071,f92(x3071,a1)))),x3072),f29(a1,x3073))),f29(x3071,x3074))),f29(x3071,x3075))))),f29(x3071,f9(f29(a1,x3073),f29(x3071,x3074),f29(x3071,x3075))))+P1(f29(a1,f4(f29(f92(x3071,a1),f4(f29(f92(x3071,f92(x3071,a1)),f4(f29(f92(x3071,f92(x3071,f92(x3071,a1))),f4(f29(f92(a1,f92(x3071,f92(x3071,f92(x3071,a1)))),x3072),f29(a1,f61(x3071,x3072)))),f29(x3071,f60(x3071,x3072)))),f29(x3071,f63(x3071,x3072)))),f29(x3071,f62(x3071,x3072)))))
% 0.55/0.72 [308]E(f29(x3081,f63(x3081,x3082)),f29(x3081,f62(x3081,x3082)))+~E(f29(a1,f61(x3081,x3082)),f29(a1,a13))+E(f29(x3081,f50(f29(f92(x3081,a1),f4(f29(f92(x3081,f92(x3081,a1)),f4(f29(f92(x3081,f92(x3081,f92(x3081,a1))),f4(f29(f92(a1,f92(x3081,f92(x3081,f92(x3081,a1)))),x3082),f29(a1,x3083))),f29(x3081,x3084))),f29(x3081,x3085))))),f29(x3081,f9(f29(a1,x3083),f29(x3081,x3084),f29(x3081,x3085))))+P1(f29(a1,f4(f29(f92(x3081,a1),f4(f29(f92(x3081,f92(x3081,a1)),f4(f29(f92(x3081,f92(x3081,f92(x3081,a1))),f4(f29(f92(a1,f92(x3081,f92(x3081,f92(x3081,a1)))),x3082),f29(a1,f61(x3081,x3082)))),f29(x3081,f60(x3081,x3082)))),f29(x3081,f63(x3081,x3082)))),f29(x3081,f62(x3081,x3082)))))
% 0.55/0.72 [309]E(f29(a1,f61(x3091,x3092)),f29(a1,a13))+E(f29(a1,f61(x3091,x3092)),f29(a1,a2))+E(f29(x3091,f50(f29(f92(x3091,a1),f4(f29(f92(x3091,f92(x3091,a1)),f4(f29(f92(x3091,f92(x3091,f92(x3091,a1))),f4(f29(f92(a1,f92(x3091,f92(x3091,f92(x3091,a1)))),x3092),f29(a1,x3093))),f29(x3091,x3094))),f29(x3091,x3095))))),f29(x3091,f9(f29(a1,x3093),f29(x3091,x3094),f29(x3091,x3095))))+~P1(f29(a1,f4(f29(f92(x3091,a1),f4(f29(f92(x3091,f92(x3091,a1)),f4(f29(f92(x3091,f92(x3091,f92(x3091,a1))),f4(f29(f92(a1,f92(x3091,f92(x3091,f92(x3091,a1)))),x3092),f29(a1,f61(x3091,x3092)))),f29(x3091,f60(x3091,x3092)))),f29(x3091,f63(x3091,x3092)))),f29(x3091,f62(x3091,x3092)))))
% 0.55/0.72 [310]~E(f29(x3101,f63(x3101,x3102)),f29(x3101,f62(x3101,x3102)))+E(f29(a1,f61(x3101,x3102)),f29(a1,a2))+E(f29(x3101,f50(f29(f92(x3101,a1),f4(f29(f92(x3101,f92(x3101,a1)),f4(f29(f92(x3101,f92(x3101,f92(x3101,a1))),f4(f29(f92(a1,f92(x3101,f92(x3101,f92(x3101,a1)))),x3102),f29(a1,x3103))),f29(x3101,x3104))),f29(x3101,x3105))))),f29(x3101,f9(f29(a1,x3103),f29(x3101,x3104),f29(x3101,x3105))))+~P1(f29(a1,f4(f29(f92(x3101,a1),f4(f29(f92(x3101,f92(x3101,a1)),f4(f29(f92(x3101,f92(x3101,f92(x3101,a1))),f4(f29(f92(a1,f92(x3101,f92(x3101,f92(x3101,a1)))),x3102),f29(a1,f61(x3101,x3102)))),f29(x3101,f60(x3101,x3102)))),f29(x3101,f63(x3101,x3102)))),f29(x3101,f62(x3101,x3102)))))
% 0.55/0.72 [311]~E(f29(x3111,f60(x3111,x3112)),f29(x3111,f62(x3111,x3112)))+E(f29(a1,f61(x3111,x3112)),f29(a1,a13))+E(f29(x3111,f50(f29(f92(x3111,a1),f4(f29(f92(x3111,f92(x3111,a1)),f4(f29(f92(x3111,f92(x3111,f92(x3111,a1))),f4(f29(f92(a1,f92(x3111,f92(x3111,f92(x3111,a1)))),x3112),f29(a1,x3113))),f29(x3111,x3114))),f29(x3111,x3115))))),f29(x3111,f9(f29(a1,x3113),f29(x3111,x3114),f29(x3111,x3115))))+~P1(f29(a1,f4(f29(f92(x3111,a1),f4(f29(f92(x3111,f92(x3111,a1)),f4(f29(f92(x3111,f92(x3111,f92(x3111,a1))),f4(f29(f92(a1,f92(x3111,f92(x3111,f92(x3111,a1)))),x3112),f29(a1,f61(x3111,x3112)))),f29(x3111,f60(x3111,x3112)))),f29(x3111,f63(x3111,x3112)))),f29(x3111,f62(x3111,x3112)))))
% 0.55/0.72 [312]~E(f29(x3121,f60(x3121,x3122)),f29(x3121,f62(x3121,x3122)))+~E(f29(x3121,f63(x3121,x3122)),f29(x3121,f62(x3121,x3122)))+E(f29(x3121,f50(f29(f92(x3121,a1),f4(f29(f92(x3121,f92(x3121,a1)),f4(f29(f92(x3121,f92(x3121,f92(x3121,a1))),f4(f29(f92(a1,f92(x3121,f92(x3121,f92(x3121,a1)))),x3122),f29(a1,x3123))),f29(x3121,x3124))),f29(x3121,x3125))))),f29(x3121,f9(f29(a1,x3123),f29(x3121,x3124),f29(x3121,x3125))))+~P1(f29(a1,f4(f29(f92(x3121,a1),f4(f29(f92(x3121,f92(x3121,a1)),f4(f29(f92(x3121,f92(x3121,f92(x3121,a1))),f4(f29(f92(a1,f92(x3121,f92(x3121,f92(x3121,a1)))),x3122),f29(a1,f61(x3121,x3122)))),f29(x3121,f60(x3121,x3122)))),f29(x3121,f63(x3121,x3122)))),f29(x3121,f62(x3121,x3122)))))
% 0.55/0.72 [296]~E(f29(x2961,f78(x2961,x2965)),f29(x2961,f79(x2961,x2965)))+~E(f29(a1,f4(f29(f92(x2961,a1),f4(f29(f92(f92(x2961,a1),f92(x2961,a1)),x2963),f29(f92(x2961,a1),f81(x2961,x2965,x2966,x2963)))),f29(x2961,f85(x2961,x2965,x2966,x2963)))),f29(a1,f4(f29(f92(x2961,a1),f81(x2961,x2965,x2966,x2963)),f29(x2961,f85(x2961,x2965,x2966,x2963)))))+~E(f29(a1,f4(f29(f92(x2961,a1),f4(f29(f92(f92(x2961,a1),f92(x2961,a1)),f4(f29(f92(f92(x2961,a1),f92(f92(x2961,a1),f92(x2961,a1))),x2966),f29(f92(x2961,a1),f82(x2961,x2965,x2966)))),f29(f92(x2961,a1),f83(x2961,x2965,x2966)))),f29(x2961,f84(x2961,x2965,x2966)))),f29(a1,f24(f29(f92(x2961,a1),f82(x2961,x2965,x2966)),f29(f92(x2961,a1),f4(f29(f92(x2961,f92(x2961,a1)),f4(f29(f92(f92(x2961,a1),f92(x2961,f92(x2961,a1))),x2965),f29(f92(x2961,a1),f83(x2961,x2965,x2966)))),f29(x2961,f84(x2961,x2965,x2966)))))))+~P1(f29(a1,f4(f29(f92(x2961,a1),f4(f29(f92(x2961,f92(x2961,a1)),f4(f29(f92(f92(x2961,a1),f92(x2961,f92(x2961,a1))),x2965),f29(f92(x2961,a1),f80(x2961,x2965)))),f29(x2961,f79(x2961,x2965)))),f29(x2961,f78(x2961,x2965)))))+~P1(f29(a1,f22(f29(f92(x2961,a1),x2962),f29(f92(x2961,a1),x2964))))+P1(f29(a1,f20(f29(f92(x2961,a1),x2962),f29(f92(x2961,a1),f4(f29(f92(f92(x2961,a1),f92(x2961,a1)),x2963),f29(f92(x2961,a1),x2964))))))
% 0.55/0.72 [297]~E(f29(a1,f4(f29(f92(x2971,a1),f4(f29(f92(f92(x2971,a1),f92(x2971,a1)),x2974),f29(f92(x2971,a1),f81(x2971,x2972,x2976,x2974)))),f29(x2971,f85(x2971,x2972,x2976,x2974)))),f29(a1,f4(f29(f92(x2971,a1),f81(x2971,x2972,x2976,x2974)),f29(x2971,f85(x2971,x2972,x2976,x2974)))))+~E(f29(a1,f4(f29(f92(x2971,a1),f4(f29(f92(f92(x2971,a1),f92(x2971,a1)),f4(f29(f92(f92(x2971,a1),f92(f92(x2971,a1),f92(x2971,a1))),x2976),f29(f92(x2971,a1),f82(x2971,x2972,x2976)))),f29(f92(x2971,a1),f83(x2971,x2972,x2976)))),f29(x2971,f84(x2971,x2972,x2976)))),f29(a1,f24(f29(f92(x2971,a1),f82(x2971,x2972,x2976)),f29(f92(x2971,a1),f4(f29(f92(x2971,f92(x2971,a1)),f4(f29(f92(f92(x2971,a1),f92(x2971,f92(x2971,a1))),x2972),f29(f92(x2971,a1),f83(x2971,x2972,x2976)))),f29(x2971,f84(x2971,x2972,x2976)))))))+~P1(f29(a1,f4(f29(f92(x2971,a1),f4(f29(f92(x2971,f92(x2971,a1)),f4(f29(f92(f92(x2971,a1),f92(x2971,f92(x2971,a1))),x2972),f29(f92(x2971,a1),f80(x2971,x2972)))),f29(x2971,f79(x2971,x2972)))),f29(x2971,f78(x2971,x2972)))))+~P1(f29(a1,f22(f29(f92(x2971,a1),x2973),f29(f92(x2971,a1),x2975))))+P1(f29(a1,f4(f29(f92(x2971,a1),f80(x2971,x2972)),f29(x2971,f79(x2971,x2972)))))+P1(f29(a1,f20(f29(f92(x2971,a1),x2973),f29(f92(x2971,a1),f4(f29(f92(f92(x2971,a1),f92(x2971,a1)),x2974),f29(f92(x2971,a1),x2975))))))
% 0.55/0.72 [298]~E(f29(a1,f4(f29(f92(x2981,a1),f4(f29(f92(f92(x2981,a1),f92(x2981,a1)),x2984),f29(f92(x2981,a1),f81(x2981,x2982,x2986,x2984)))),f29(x2981,f85(x2981,x2982,x2986,x2984)))),f29(a1,f4(f29(f92(x2981,a1),f81(x2981,x2982,x2986,x2984)),f29(x2981,f85(x2981,x2982,x2986,x2984)))))+~E(f29(a1,f4(f29(f92(x2981,a1),f4(f29(f92(f92(x2981,a1),f92(x2981,a1)),f4(f29(f92(f92(x2981,a1),f92(f92(x2981,a1),f92(x2981,a1))),x2986),f29(f92(x2981,a1),f82(x2981,x2982,x2986)))),f29(f92(x2981,a1),f83(x2981,x2982,x2986)))),f29(x2981,f84(x2981,x2982,x2986)))),f29(a1,f24(f29(f92(x2981,a1),f82(x2981,x2982,x2986)),f29(f92(x2981,a1),f4(f29(f92(x2981,f92(x2981,a1)),f4(f29(f92(f92(x2981,a1),f92(x2981,f92(x2981,a1))),x2982),f29(f92(x2981,a1),f83(x2981,x2982,x2986)))),f29(x2981,f84(x2981,x2982,x2986)))))))+~P1(f29(a1,f4(f29(f92(x2981,a1),f4(f29(f92(x2981,f92(x2981,a1)),f4(f29(f92(f92(x2981,a1),f92(x2981,f92(x2981,a1))),x2982),f29(f92(x2981,a1),f80(x2981,x2982)))),f29(x2981,f79(x2981,x2982)))),f29(x2981,f78(x2981,x2982)))))+~P1(f29(a1,f22(f29(f92(x2981,a1),x2983),f29(f92(x2981,a1),x2985))))+P1(f29(a1,f4(f29(f92(x2981,a1),f80(x2981,x2982)),f29(x2981,f78(x2981,x2982)))))+P1(f29(a1,f20(f29(f92(x2981,a1),x2983),f29(f92(x2981,a1),f4(f29(f92(f92(x2981,a1),f92(x2981,a1)),x2984),f29(f92(x2981,a1),x2985))))))
% 0.55/0.72 [300]~E(f29(x3001,f78(x3001,x3005)),f29(x3001,f79(x3001,x3005)))+~E(f29(a1,f4(f29(f92(x3001,a1),f4(f29(f92(f92(x3001,a1),f92(x3001,a1)),x3006),f29(f92(x3001,a1),f81(x3001,x3005,x3003,x3006)))),f29(x3001,f85(x3001,x3005,x3003,x3006)))),f29(a1,f4(f29(f92(x3001,a1),f81(x3001,x3005,x3003,x3006)),f29(x3001,f85(x3001,x3005,x3003,x3006)))))+~E(f29(a1,f4(f29(f92(x3001,a1),f4(f29(f92(f92(x3001,a1),f92(x3001,a1)),f4(f29(f92(f92(x3001,a1),f92(f92(x3001,a1),f92(x3001,a1))),x3003),f29(f92(x3001,a1),f82(x3001,x3005,x3003)))),f29(f92(x3001,a1),f83(x3001,x3005,x3003)))),f29(x3001,f84(x3001,x3005,x3003)))),f29(a1,f24(f29(f92(x3001,a1),f82(x3001,x3005,x3003)),f29(f92(x3001,a1),f4(f29(f92(x3001,f92(x3001,a1)),f4(f29(f92(f92(x3001,a1),f92(x3001,f92(x3001,a1))),x3005),f29(f92(x3001,a1),f83(x3001,x3005,x3003)))),f29(x3001,f84(x3001,x3005,x3003)))))))+~P1(f29(a1,f4(f29(f92(x3001,a1),f4(f29(f92(x3001,f92(x3001,a1)),f4(f29(f92(f92(x3001,a1),f92(x3001,f92(x3001,a1))),x3005),f29(f92(x3001,a1),f80(x3001,x3005)))),f29(x3001,f79(x3001,x3005)))),f29(x3001,f78(x3001,x3005)))))+~P1(f29(a1,f22(f29(f92(x3001,a1),x3002),f29(f92(x3001,a1),x3004))))+P1(f29(a1,f24(f29(f92(x3001,a1),x3002),f29(f92(x3001,a1),f4(f29(f92(f92(x3001,a1),f92(x3001,a1)),f4(f29(f92(f92(x3001,a1),f92(f92(x3001,a1),f92(x3001,a1))),x3003),f29(f92(x3001,a1),x3002))),f29(f92(x3001,a1),x3004))))))
% 0.55/0.72 [301]~E(f29(a1,f4(f29(f92(x3011,a1),f4(f29(f92(f92(x3011,a1),f92(x3011,a1)),x3016),f29(f92(x3011,a1),f81(x3011,x3012,x3014,x3016)))),f29(x3011,f85(x3011,x3012,x3014,x3016)))),f29(a1,f4(f29(f92(x3011,a1),f81(x3011,x3012,x3014,x3016)),f29(x3011,f85(x3011,x3012,x3014,x3016)))))+~E(f29(a1,f4(f29(f92(x3011,a1),f4(f29(f92(f92(x3011,a1),f92(x3011,a1)),f4(f29(f92(f92(x3011,a1),f92(f92(x3011,a1),f92(x3011,a1))),x3014),f29(f92(x3011,a1),f82(x3011,x3012,x3014)))),f29(f92(x3011,a1),f83(x3011,x3012,x3014)))),f29(x3011,f84(x3011,x3012,x3014)))),f29(a1,f24(f29(f92(x3011,a1),f82(x3011,x3012,x3014)),f29(f92(x3011,a1),f4(f29(f92(x3011,f92(x3011,a1)),f4(f29(f92(f92(x3011,a1),f92(x3011,f92(x3011,a1))),x3012),f29(f92(x3011,a1),f83(x3011,x3012,x3014)))),f29(x3011,f84(x3011,x3012,x3014)))))))+~P1(f29(a1,f4(f29(f92(x3011,a1),f4(f29(f92(x3011,f92(x3011,a1)),f4(f29(f92(f92(x3011,a1),f92(x3011,f92(x3011,a1))),x3012),f29(f92(x3011,a1),f80(x3011,x3012)))),f29(x3011,f79(x3011,x3012)))),f29(x3011,f78(x3011,x3012)))))+~P1(f29(a1,f22(f29(f92(x3011,a1),x3013),f29(f92(x3011,a1),x3015))))+P1(f29(a1,f4(f29(f92(x3011,a1),f80(x3011,x3012)),f29(x3011,f79(x3011,x3012)))))+P1(f29(a1,f24(f29(f92(x3011,a1),x3013),f29(f92(x3011,a1),f4(f29(f92(f92(x3011,a1),f92(x3011,a1)),f4(f29(f92(f92(x3011,a1),f92(f92(x3011,a1),f92(x3011,a1))),x3014),f29(f92(x3011,a1),x3013))),f29(f92(x3011,a1),x3015))))))
% 0.55/0.72 [302]~E(f29(a1,f4(f29(f92(x3021,a1),f4(f29(f92(f92(x3021,a1),f92(x3021,a1)),x3026),f29(f92(x3021,a1),f81(x3021,x3022,x3024,x3026)))),f29(x3021,f85(x3021,x3022,x3024,x3026)))),f29(a1,f4(f29(f92(x3021,a1),f81(x3021,x3022,x3024,x3026)),f29(x3021,f85(x3021,x3022,x3024,x3026)))))+~E(f29(a1,f4(f29(f92(x3021,a1),f4(f29(f92(f92(x3021,a1),f92(x3021,a1)),f4(f29(f92(f92(x3021,a1),f92(f92(x3021,a1),f92(x3021,a1))),x3024),f29(f92(x3021,a1),f82(x3021,x3022,x3024)))),f29(f92(x3021,a1),f83(x3021,x3022,x3024)))),f29(x3021,f84(x3021,x3022,x3024)))),f29(a1,f24(f29(f92(x3021,a1),f82(x3021,x3022,x3024)),f29(f92(x3021,a1),f4(f29(f92(x3021,f92(x3021,a1)),f4(f29(f92(f92(x3021,a1),f92(x3021,f92(x3021,a1))),x3022),f29(f92(x3021,a1),f83(x3021,x3022,x3024)))),f29(x3021,f84(x3021,x3022,x3024)))))))+~P1(f29(a1,f4(f29(f92(x3021,a1),f4(f29(f92(x3021,f92(x3021,a1)),f4(f29(f92(f92(x3021,a1),f92(x3021,f92(x3021,a1))),x3022),f29(f92(x3021,a1),f80(x3021,x3022)))),f29(x3021,f79(x3021,x3022)))),f29(x3021,f78(x3021,x3022)))))+~P1(f29(a1,f22(f29(f92(x3021,a1),x3023),f29(f92(x3021,a1),x3025))))+P1(f29(a1,f4(f29(f92(x3021,a1),f80(x3021,x3022)),f29(x3021,f78(x3021,x3022)))))+P1(f29(a1,f24(f29(f92(x3021,a1),x3023),f29(f92(x3021,a1),f4(f29(f92(f92(x3021,a1),f92(x3021,a1)),f4(f29(f92(f92(x3021,a1),f92(f92(x3021,a1),f92(x3021,a1))),x3024),f29(f92(x3021,a1),x3023))),f29(f92(x3021,a1),x3025))))))
% 0.55/0.72 [304]~E(f29(x3041,f78(x3041,x3044)),f29(x3041,f79(x3041,x3044)))+~E(f29(a1,f4(f29(f92(x3041,a1),f4(f29(f92(f92(x3041,a1),f92(x3041,a1)),x3045),f29(f92(x3041,a1),f81(x3041,x3044,x3046,x3045)))),f29(x3041,f85(x3041,x3044,x3046,x3045)))),f29(a1,f4(f29(f92(x3041,a1),f81(x3041,x3044,x3046,x3045)),f29(x3041,f85(x3041,x3044,x3046,x3045)))))+~E(f29(a1,f4(f29(f92(x3041,a1),f4(f29(f92(f92(x3041,a1),f92(x3041,a1)),f4(f29(f92(f92(x3041,a1),f92(f92(x3041,a1),f92(x3041,a1))),x3046),f29(f92(x3041,a1),f82(x3041,x3044,x3046)))),f29(f92(x3041,a1),f83(x3041,x3044,x3046)))),f29(x3041,f84(x3041,x3044,x3046)))),f29(a1,f24(f29(f92(x3041,a1),f82(x3041,x3044,x3046)),f29(f92(x3041,a1),f4(f29(f92(x3041,f92(x3041,a1)),f4(f29(f92(f92(x3041,a1),f92(x3041,f92(x3041,a1))),x3044),f29(f92(x3041,a1),f83(x3041,x3044,x3046)))),f29(x3041,f84(x3041,x3044,x3046)))))))+~P1(f29(a1,f4(f29(f92(x3041,a1),f4(f29(f92(x3041,f92(x3041,a1)),f4(f29(f92(f92(x3041,a1),f92(x3041,f92(x3041,a1))),x3044),f29(f92(x3041,a1),f80(x3041,x3044)))),f29(x3041,f79(x3041,x3044)))),f29(x3041,f78(x3041,x3044)))))+P1(f29(a1,f22(f29(f92(x3041,a1),x3042),f29(f92(x3041,a1),x3043))))+~P1(f29(a1,f24(f29(f92(x3041,a1),x3042),f29(f92(x3041,a1),f4(f29(f92(f92(x3041,a1),f92(x3041,a1)),f4(f29(f92(f92(x3041,a1),f92(f92(x3041,a1),f92(x3041,a1))),x3046),f29(f92(x3041,a1),x3042))),f29(f92(x3041,a1),x3043))))))+~P1(f29(a1,f20(f29(f92(x3041,a1),x3042),f29(f92(x3041,a1),f4(f29(f92(f92(x3041,a1),f92(x3041,a1)),x3045),f29(f92(x3041,a1),x3043))))))
% 0.55/0.72 [305]~E(f29(a1,f4(f29(f92(x3051,a1),f4(f29(f92(f92(x3051,a1),f92(x3051,a1)),x3055),f29(f92(x3051,a1),f81(x3051,x3054,x3056,x3055)))),f29(x3051,f85(x3051,x3054,x3056,x3055)))),f29(a1,f4(f29(f92(x3051,a1),f81(x3051,x3054,x3056,x3055)),f29(x3051,f85(x3051,x3054,x3056,x3055)))))+~E(f29(a1,f4(f29(f92(x3051,a1),f4(f29(f92(f92(x3051,a1),f92(x3051,a1)),f4(f29(f92(f92(x3051,a1),f92(f92(x3051,a1),f92(x3051,a1))),x3056),f29(f92(x3051,a1),f82(x3051,x3054,x3056)))),f29(f92(x3051,a1),f83(x3051,x3054,x3056)))),f29(x3051,f84(x3051,x3054,x3056)))),f29(a1,f24(f29(f92(x3051,a1),f82(x3051,x3054,x3056)),f29(f92(x3051,a1),f4(f29(f92(x3051,f92(x3051,a1)),f4(f29(f92(f92(x3051,a1),f92(x3051,f92(x3051,a1))),x3054),f29(f92(x3051,a1),f83(x3051,x3054,x3056)))),f29(x3051,f84(x3051,x3054,x3056)))))))+~P1(f29(a1,f4(f29(f92(x3051,a1),f4(f29(f92(x3051,f92(x3051,a1)),f4(f29(f92(f92(x3051,a1),f92(x3051,f92(x3051,a1))),x3054),f29(f92(x3051,a1),f80(x3051,x3054)))),f29(x3051,f79(x3051,x3054)))),f29(x3051,f78(x3051,x3054)))))+P1(f29(a1,f4(f29(f92(x3051,a1),f80(x3051,x3054)),f29(x3051,f79(x3051,x3054)))))+P1(f29(a1,f22(f29(f92(x3051,a1),x3052),f29(f92(x3051,a1),x3053))))+~P1(f29(a1,f24(f29(f92(x3051,a1),x3052),f29(f92(x3051,a1),f4(f29(f92(f92(x3051,a1),f92(x3051,a1)),f4(f29(f92(f92(x3051,a1),f92(f92(x3051,a1),f92(x3051,a1))),x3056),f29(f92(x3051,a1),x3052))),f29(f92(x3051,a1),x3053))))))+~P1(f29(a1,f20(f29(f92(x3051,a1),x3052),f29(f92(x3051,a1),f4(f29(f92(f92(x3051,a1),f92(x3051,a1)),x3055),f29(f92(x3051,a1),x3053))))))
% 0.55/0.72 [306]~E(f29(a1,f4(f29(f92(x3061,a1),f4(f29(f92(f92(x3061,a1),f92(x3061,a1)),x3065),f29(f92(x3061,a1),f81(x3061,x3064,x3066,x3065)))),f29(x3061,f85(x3061,x3064,x3066,x3065)))),f29(a1,f4(f29(f92(x3061,a1),f81(x3061,x3064,x3066,x3065)),f29(x3061,f85(x3061,x3064,x3066,x3065)))))+~E(f29(a1,f4(f29(f92(x3061,a1),f4(f29(f92(f92(x3061,a1),f92(x3061,a1)),f4(f29(f92(f92(x3061,a1),f92(f92(x3061,a1),f92(x3061,a1))),x3066),f29(f92(x3061,a1),f82(x3061,x3064,x3066)))),f29(f92(x3061,a1),f83(x3061,x3064,x3066)))),f29(x3061,f84(x3061,x3064,x3066)))),f29(a1,f24(f29(f92(x3061,a1),f82(x3061,x3064,x3066)),f29(f92(x3061,a1),f4(f29(f92(x3061,f92(x3061,a1)),f4(f29(f92(f92(x3061,a1),f92(x3061,f92(x3061,a1))),x3064),f29(f92(x3061,a1),f83(x3061,x3064,x3066)))),f29(x3061,f84(x3061,x3064,x3066)))))))+~P1(f29(a1,f4(f29(f92(x3061,a1),f4(f29(f92(x3061,f92(x3061,a1)),f4(f29(f92(f92(x3061,a1),f92(x3061,f92(x3061,a1))),x3064),f29(f92(x3061,a1),f80(x3061,x3064)))),f29(x3061,f79(x3061,x3064)))),f29(x3061,f78(x3061,x3064)))))+P1(f29(a1,f4(f29(f92(x3061,a1),f80(x3061,x3064)),f29(x3061,f78(x3061,x3064)))))+P1(f29(a1,f22(f29(f92(x3061,a1),x3062),f29(f92(x3061,a1),x3063))))+~P1(f29(a1,f24(f29(f92(x3061,a1),x3062),f29(f92(x3061,a1),f4(f29(f92(f92(x3061,a1),f92(x3061,a1)),f4(f29(f92(f92(x3061,a1),f92(f92(x3061,a1),f92(x3061,a1))),x3066),f29(f92(x3061,a1),x3062))),f29(f92(x3061,a1),x3063))))))+~P1(f29(a1,f20(f29(f92(x3061,a1),x3062),f29(f92(x3061,a1),f4(f29(f92(f92(x3061,a1),f92(x3061,a1)),x3065),f29(f92(x3061,a1),x3063))))))
% 0.55/0.72 [295]E(f29(x2951,f78(x2951,x2952)),f29(x2951,f79(x2951,x2952)))+~E(f29(a1,f4(f29(f92(x2951,a1),f4(f29(f92(f92(x2951,a1),f92(x2951,a1)),x2954),f29(f92(x2951,a1),f81(x2951,x2952,x2956,x2954)))),f29(x2951,f85(x2951,x2952,x2956,x2954)))),f29(a1,f4(f29(f92(x2951,a1),f81(x2951,x2952,x2956,x2954)),f29(x2951,f85(x2951,x2952,x2956,x2954)))))+~E(f29(a1,f4(f29(f92(x2951,a1),f4(f29(f92(f92(x2951,a1),f92(x2951,a1)),f4(f29(f92(f92(x2951,a1),f92(f92(x2951,a1),f92(x2951,a1))),x2956),f29(f92(x2951,a1),f82(x2951,x2952,x2956)))),f29(f92(x2951,a1),f83(x2951,x2952,x2956)))),f29(x2951,f84(x2951,x2952,x2956)))),f29(a1,f24(f29(f92(x2951,a1),f82(x2951,x2952,x2956)),f29(f92(x2951,a1),f4(f29(f92(x2951,f92(x2951,a1)),f4(f29(f92(f92(x2951,a1),f92(x2951,f92(x2951,a1))),x2952),f29(f92(x2951,a1),f83(x2951,x2952,x2956)))),f29(x2951,f84(x2951,x2952,x2956)))))))+~P1(f29(a1,f4(f29(f92(x2951,a1),f80(x2951,x2952)),f29(x2951,f78(x2951,x2952)))))+~P1(f29(a1,f4(f29(f92(x2951,a1),f80(x2951,x2952)),f29(x2951,f79(x2951,x2952)))))+P1(f29(a1,f4(f29(f92(x2951,a1),f4(f29(f92(x2951,f92(x2951,a1)),f4(f29(f92(f92(x2951,a1),f92(x2951,f92(x2951,a1))),x2952),f29(f92(x2951,a1),f80(x2951,x2952)))),f29(x2951,f79(x2951,x2952)))),f29(x2951,f78(x2951,x2952)))))+~P1(f29(a1,f22(f29(f92(x2951,a1),x2953),f29(f92(x2951,a1),x2955))))+P1(f29(a1,f20(f29(f92(x2951,a1),x2953),f29(f92(x2951,a1),f4(f29(f92(f92(x2951,a1),f92(x2951,a1)),x2954),f29(f92(x2951,a1),x2955))))))
% 0.55/0.72 [299]E(f29(x2991,f78(x2991,x2992)),f29(x2991,f79(x2991,x2992)))+~E(f29(a1,f4(f29(f92(x2991,a1),f4(f29(f92(f92(x2991,a1),f92(x2991,a1)),x2996),f29(f92(x2991,a1),f81(x2991,x2992,x2994,x2996)))),f29(x2991,f85(x2991,x2992,x2994,x2996)))),f29(a1,f4(f29(f92(x2991,a1),f81(x2991,x2992,x2994,x2996)),f29(x2991,f85(x2991,x2992,x2994,x2996)))))+~E(f29(a1,f4(f29(f92(x2991,a1),f4(f29(f92(f92(x2991,a1),f92(x2991,a1)),f4(f29(f92(f92(x2991,a1),f92(f92(x2991,a1),f92(x2991,a1))),x2994),f29(f92(x2991,a1),f82(x2991,x2992,x2994)))),f29(f92(x2991,a1),f83(x2991,x2992,x2994)))),f29(x2991,f84(x2991,x2992,x2994)))),f29(a1,f24(f29(f92(x2991,a1),f82(x2991,x2992,x2994)),f29(f92(x2991,a1),f4(f29(f92(x2991,f92(x2991,a1)),f4(f29(f92(f92(x2991,a1),f92(x2991,f92(x2991,a1))),x2992),f29(f92(x2991,a1),f83(x2991,x2992,x2994)))),f29(x2991,f84(x2991,x2992,x2994)))))))+~P1(f29(a1,f22(f29(f92(x2991,a1),x2993),f29(f92(x2991,a1),x2995))))+~P1(f29(a1,f4(f29(f92(x2991,a1),f80(x2991,x2992)),f29(x2991,f78(x2991,x2992)))))+~P1(f29(a1,f4(f29(f92(x2991,a1),f80(x2991,x2992)),f29(x2991,f79(x2991,x2992)))))+P1(f29(a1,f4(f29(f92(x2991,a1),f4(f29(f92(x2991,f92(x2991,a1)),f4(f29(f92(f92(x2991,a1),f92(x2991,f92(x2991,a1))),x2992),f29(f92(x2991,a1),f80(x2991,x2992)))),f29(x2991,f79(x2991,x2992)))),f29(x2991,f78(x2991,x2992)))))+P1(f29(a1,f24(f29(f92(x2991,a1),x2993),f29(f92(x2991,a1),f4(f29(f92(f92(x2991,a1),f92(x2991,a1)),f4(f29(f92(f92(x2991,a1),f92(f92(x2991,a1),f92(x2991,a1))),x2994),f29(f92(x2991,a1),x2993))),f29(f92(x2991,a1),x2995))))))
% 0.55/0.72 [303]E(f29(x3031,f78(x3031,x3032)),f29(x3031,f79(x3031,x3032)))+~E(f29(a1,f4(f29(f92(x3031,a1),f4(f29(f92(f92(x3031,a1),f92(x3031,a1)),x3035),f29(f92(x3031,a1),f81(x3031,x3032,x3036,x3035)))),f29(x3031,f85(x3031,x3032,x3036,x3035)))),f29(a1,f4(f29(f92(x3031,a1),f81(x3031,x3032,x3036,x3035)),f29(x3031,f85(x3031,x3032,x3036,x3035)))))+~E(f29(a1,f4(f29(f92(x3031,a1),f4(f29(f92(f92(x3031,a1),f92(x3031,a1)),f4(f29(f92(f92(x3031,a1),f92(f92(x3031,a1),f92(x3031,a1))),x3036),f29(f92(x3031,a1),f82(x3031,x3032,x3036)))),f29(f92(x3031,a1),f83(x3031,x3032,x3036)))),f29(x3031,f84(x3031,x3032,x3036)))),f29(a1,f24(f29(f92(x3031,a1),f82(x3031,x3032,x3036)),f29(f92(x3031,a1),f4(f29(f92(x3031,f92(x3031,a1)),f4(f29(f92(f92(x3031,a1),f92(x3031,f92(x3031,a1))),x3032),f29(f92(x3031,a1),f83(x3031,x3032,x3036)))),f29(x3031,f84(x3031,x3032,x3036)))))))+~P1(f29(a1,f4(f29(f92(x3031,a1),f80(x3031,x3032)),f29(x3031,f78(x3031,x3032)))))+~P1(f29(a1,f4(f29(f92(x3031,a1),f80(x3031,x3032)),f29(x3031,f79(x3031,x3032)))))+P1(f29(a1,f4(f29(f92(x3031,a1),f4(f29(f92(x3031,f92(x3031,a1)),f4(f29(f92(f92(x3031,a1),f92(x3031,f92(x3031,a1))),x3032),f29(f92(x3031,a1),f80(x3031,x3032)))),f29(x3031,f79(x3031,x3032)))),f29(x3031,f78(x3031,x3032)))))+P1(f29(a1,f22(f29(f92(x3031,a1),x3033),f29(f92(x3031,a1),x3034))))+~P1(f29(a1,f24(f29(f92(x3031,a1),x3033),f29(f92(x3031,a1),f4(f29(f92(f92(x3031,a1),f92(x3031,a1)),f4(f29(f92(f92(x3031,a1),f92(f92(x3031,a1),f92(x3031,a1))),x3036),f29(f92(x3031,a1),x3033))),f29(f92(x3031,a1),x3034))))))+~P1(f29(a1,f20(f29(f92(x3031,a1),x3033),f29(f92(x3031,a1),f4(f29(f92(f92(x3031,a1),f92(x3031,a1)),x3035),f29(f92(x3031,a1),x3034))))))
% 0.55/0.72 %EqnAxiom
% 0.55/0.72 [1]E(x11,x11)
% 0.55/0.72 [2]E(x22,x21)+~E(x21,x22)
% 0.55/0.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.55/0.72 [4]~E(x41,x42)+E(f29(x41,x43),f29(x42,x43))
% 0.55/0.72 [5]~E(x51,x52)+E(f29(x53,x51),f29(x53,x52))
% 0.55/0.72 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 0.55/0.72 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 0.55/0.72 [8]~E(x81,x82)+E(f62(x81,x83),f62(x82,x83))
% 0.55/0.72 [9]~E(x91,x92)+E(f62(x93,x91),f62(x93,x92))
% 0.55/0.72 [10]~E(x101,x102)+E(f79(x101,x103),f79(x102,x103))
% 0.55/0.72 [11]~E(x111,x112)+E(f79(x113,x111),f79(x113,x112))
% 0.55/0.72 [12]~E(x121,x122)+E(f3(x121),f3(x122))
% 0.55/0.72 [13]~E(x131,x132)+E(f63(x131,x133),f63(x132,x133))
% 0.55/0.72 [14]~E(x141,x142)+E(f63(x143,x141),f63(x143,x142))
% 0.55/0.72 [15]~E(x151,x152)+E(f80(x151,x153),f80(x152,x153))
% 0.55/0.72 [16]~E(x161,x162)+E(f80(x163,x161),f80(x163,x162))
% 0.55/0.72 [17]~E(x171,x172)+E(f60(x171,x173),f60(x172,x173))
% 0.55/0.72 [18]~E(x181,x182)+E(f60(x183,x181),f60(x183,x182))
% 0.55/0.72 [19]~E(x191,x192)+E(f6(x191),f6(x192))
% 0.55/0.72 [20]~E(x201,x202)+E(f92(x201,x203),f92(x202,x203))
% 0.55/0.72 [21]~E(x211,x212)+E(f92(x213,x211),f92(x213,x212))
% 0.55/0.72 [22]~E(x221,x222)+E(f61(x221,x223),f61(x222,x223))
% 0.55/0.72 [23]~E(x231,x232)+E(f61(x233,x231),f61(x233,x232))
% 0.55/0.72 [24]~E(x241,x242)+E(f24(x241,x243),f24(x242,x243))
% 0.55/0.72 [25]~E(x251,x252)+E(f24(x253,x251),f24(x253,x252))
% 0.55/0.72 [26]~E(x261,x262)+E(f90(x261,x263),f90(x262,x263))
% 0.55/0.72 [27]~E(x271,x272)+E(f90(x273,x271),f90(x273,x272))
% 0.55/0.72 [28]~E(x281,x282)+E(f46(x281,x283),f46(x282,x283))
% 0.55/0.72 [29]~E(x291,x292)+E(f46(x293,x291),f46(x293,x292))
% 0.55/0.72 [30]~E(x301,x302)+E(f78(x301,x303),f78(x302,x303))
% 0.55/0.72 [31]~E(x311,x312)+E(f78(x313,x311),f78(x313,x312))
% 0.55/0.72 [32]~E(x321,x322)+E(f86(x321,x323),f86(x322,x323))
% 0.55/0.72 [33]~E(x331,x332)+E(f86(x333,x331),f86(x333,x332))
% 0.55/0.72 [34]~E(x341,x342)+E(f77(x341,x343),f77(x342,x343))
% 0.55/0.72 [35]~E(x351,x352)+E(f77(x353,x351),f77(x353,x352))
% 0.55/0.72 [36]~E(x361,x362)+E(f11(x361,x363),f11(x362,x363))
% 0.55/0.72 [37]~E(x371,x372)+E(f11(x373,x371),f11(x373,x372))
% 0.55/0.72 [38]~E(x381,x382)+E(f22(x381,x383),f22(x382,x383))
% 0.55/0.72 [39]~E(x391,x392)+E(f22(x393,x391),f22(x393,x392))
% 0.55/0.72 [40]~E(x401,x402)+E(f81(x401,x403,x404,x405),f81(x402,x403,x404,x405))
% 0.55/0.72 [41]~E(x411,x412)+E(f81(x413,x411,x414,x415),f81(x413,x412,x414,x415))
% 0.55/0.72 [42]~E(x421,x422)+E(f81(x423,x424,x421,x425),f81(x423,x424,x422,x425))
% 0.55/0.72 [43]~E(x431,x432)+E(f81(x433,x434,x435,x431),f81(x433,x434,x435,x432))
% 0.55/0.72 [44]~E(x441,x442)+E(f26(x441,x443),f26(x442,x443))
% 0.55/0.72 [45]~E(x451,x452)+E(f26(x453,x451),f26(x453,x452))
% 0.55/0.72 [46]~E(x461,x462)+E(f50(x461),f50(x462))
% 0.55/0.72 [47]~E(x471,x472)+E(f42(x471,x473),f42(x472,x473))
% 0.55/0.72 [48]~E(x481,x482)+E(f42(x483,x481),f42(x483,x482))
% 0.55/0.72 [49]~E(x491,x492)+E(f82(x491,x493,x494),f82(x492,x493,x494))
% 0.55/0.72 [50]~E(x501,x502)+E(f82(x503,x501,x504),f82(x503,x502,x504))
% 0.55/0.72 [51]~E(x511,x512)+E(f82(x513,x514,x511),f82(x513,x514,x512))
% 0.55/0.72 [52]~E(x521,x522)+E(f84(x521,x523,x524),f84(x522,x523,x524))
% 0.55/0.72 [53]~E(x531,x532)+E(f84(x533,x531,x534),f84(x533,x532,x534))
% 0.55/0.72 [54]~E(x541,x542)+E(f84(x543,x544,x541),f84(x543,x544,x542))
% 0.55/0.72 [55]~E(x551,x552)+E(f72(x551,x553,x554,x555),f72(x552,x553,x554,x555))
% 0.55/0.72 [56]~E(x561,x562)+E(f72(x563,x561,x564,x565),f72(x563,x562,x564,x565))
% 0.55/0.72 [57]~E(x571,x572)+E(f72(x573,x574,x571,x575),f72(x573,x574,x572,x575))
% 0.55/0.72 [58]~E(x581,x582)+E(f72(x583,x584,x585,x581),f72(x583,x584,x585,x582))
% 0.55/0.72 [59]~E(x591,x592)+E(f70(x591,x593,x594),f70(x592,x593,x594))
% 0.55/0.72 [60]~E(x601,x602)+E(f70(x603,x601,x604),f70(x603,x602,x604))
% 0.55/0.72 [61]~E(x611,x612)+E(f70(x613,x614,x611),f70(x613,x614,x612))
% 0.55/0.72 [62]~E(x621,x622)+E(f85(x621,x623,x624,x625),f85(x622,x623,x624,x625))
% 0.55/0.72 [63]~E(x631,x632)+E(f85(x633,x631,x634,x635),f85(x633,x632,x634,x635))
% 0.55/0.72 [64]~E(x641,x642)+E(f85(x643,x644,x641,x645),f85(x643,x644,x642,x645))
% 0.55/0.72 [65]~E(x651,x652)+E(f85(x653,x654,x655,x651),f85(x653,x654,x655,x652))
% 0.55/0.72 [66]~E(x661,x662)+E(f31(x661,x663),f31(x662,x663))
% 0.55/0.72 [67]~E(x671,x672)+E(f31(x673,x671),f31(x673,x672))
% 0.55/0.72 [68]~E(x681,x682)+E(f28(x681,x683),f28(x682,x683))
% 0.55/0.72 [69]~E(x691,x692)+E(f28(x693,x691),f28(x693,x692))
% 0.55/0.72 [70]~E(x701,x702)+E(f9(x701,x703,x704),f9(x702,x703,x704))
% 0.55/0.72 [71]~E(x711,x712)+E(f9(x713,x711,x714),f9(x713,x712,x714))
% 0.55/0.72 [72]~E(x721,x722)+E(f9(x723,x724,x721),f9(x723,x724,x722))
% 0.55/0.72 [73]~E(x731,x732)+E(f36(x731,x733),f36(x732,x733))
% 0.55/0.72 [74]~E(x741,x742)+E(f36(x743,x741),f36(x743,x742))
% 0.55/0.72 [75]~E(x751,x752)+E(f33(x751),f33(x752))
% 0.55/0.72 [76]~E(x761,x762)+E(f10(x761),f10(x762))
% 0.55/0.72 [77]~E(x771,x772)+E(f83(x771,x773,x774),f83(x772,x773,x774))
% 0.55/0.72 [78]~E(x781,x782)+E(f83(x783,x781,x784),f83(x783,x782,x784))
% 0.55/0.72 [79]~E(x791,x792)+E(f83(x793,x794,x791),f83(x793,x794,x792))
% 0.55/0.72 [80]~E(x801,x802)+E(f14(x801,x803),f14(x802,x803))
% 0.55/0.72 [81]~E(x811,x812)+E(f14(x813,x811),f14(x813,x812))
% 0.55/0.72 [82]~E(x821,x822)+E(f39(x821),f39(x822))
% 0.55/0.72 [83]~E(x831,x832)+E(f75(x831,x833,x834,x835),f75(x832,x833,x834,x835))
% 0.55/0.72 [84]~E(x841,x842)+E(f75(x843,x841,x844,x845),f75(x843,x842,x844,x845))
% 0.55/0.72 [85]~E(x851,x852)+E(f75(x853,x854,x851,x855),f75(x853,x854,x852,x855))
% 0.55/0.72 [86]~E(x861,x862)+E(f75(x863,x864,x865,x861),f75(x863,x864,x865,x862))
% 0.55/0.72 [87]~E(x871,x872)+E(f20(x871,x873),f20(x872,x873))
% 0.55/0.72 [88]~E(x881,x882)+E(f20(x883,x881),f20(x883,x882))
% 0.55/0.72 [89]~E(x891,x892)+E(f88(x891,x893),f88(x892,x893))
% 0.55/0.72 [90]~E(x901,x902)+E(f88(x903,x901),f88(x903,x902))
% 0.55/0.72 [91]~E(x911,x912)+E(f64(x911,x913,x914),f64(x912,x913,x914))
% 0.55/0.72 [92]~E(x921,x922)+E(f64(x923,x921,x924),f64(x923,x922,x924))
% 0.55/0.72 [93]~E(x931,x932)+E(f64(x933,x934,x931),f64(x933,x934,x932))
% 0.55/0.72 [94]~E(x941,x942)+E(f73(x941,x943,x944,x945),f73(x942,x943,x944,x945))
% 0.55/0.72 [95]~E(x951,x952)+E(f73(x953,x951,x954,x955),f73(x953,x952,x954,x955))
% 0.55/0.72 [96]~E(x961,x962)+E(f73(x963,x964,x961,x965),f73(x963,x964,x962,x965))
% 0.55/0.72 [97]~E(x971,x972)+E(f73(x973,x974,x975,x971),f73(x973,x974,x975,x972))
% 0.55/0.72 [98]~E(x981,x982)+E(f18(x981),f18(x982))
% 0.55/0.72 [99]~E(x991,x992)+E(f58(x991,x993),f58(x992,x993))
% 0.55/0.72 [100]~E(x1001,x1002)+E(f58(x1003,x1001),f58(x1003,x1002))
% 0.55/0.72 [101]~E(x1011,x1012)+E(f91(x1011,x1013),f91(x1012,x1013))
% 0.55/0.72 [102]~E(x1021,x1022)+E(f91(x1023,x1021),f91(x1023,x1022))
% 0.55/0.72 [103]~E(x1031,x1032)+E(f47(x1031,x1033),f47(x1032,x1033))
% 0.55/0.72 [104]~E(x1041,x1042)+E(f47(x1043,x1041),f47(x1043,x1042))
% 0.55/0.72 [105]~E(x1051,x1052)+E(f67(x1051,x1053,x1054,x1055),f67(x1052,x1053,x1054,x1055))
% 0.55/0.72 [106]~E(x1061,x1062)+E(f67(x1063,x1061,x1064,x1065),f67(x1063,x1062,x1064,x1065))
% 0.55/0.72 [107]~E(x1071,x1072)+E(f67(x1073,x1074,x1071,x1075),f67(x1073,x1074,x1072,x1075))
% 0.55/0.72 [108]~E(x1081,x1082)+E(f67(x1083,x1084,x1085,x1081),f67(x1083,x1084,x1085,x1082))
% 0.55/0.72 [109]~E(x1091,x1092)+E(f38(x1091),f38(x1092))
% 0.55/0.72 [110]~E(x1101,x1102)+E(f87(x1101,x1103),f87(x1102,x1103))
% 0.55/0.72 [111]~E(x1111,x1112)+E(f87(x1113,x1111),f87(x1113,x1112))
% 0.55/0.72 [112]~E(x1121,x1122)+E(f65(x1121,x1123,x1124,x1125),f65(x1122,x1123,x1124,x1125))
% 0.55/0.72 [113]~E(x1131,x1132)+E(f65(x1133,x1131,x1134,x1135),f65(x1133,x1132,x1134,x1135))
% 0.55/0.72 [114]~E(x1141,x1142)+E(f65(x1143,x1144,x1141,x1145),f65(x1143,x1144,x1142,x1145))
% 0.55/0.72 [115]~E(x1151,x1152)+E(f65(x1153,x1154,x1155,x1151),f65(x1153,x1154,x1155,x1152))
% 0.55/0.72 [116]~E(x1161,x1162)+E(f59(x1161,x1163),f59(x1162,x1163))
% 0.55/0.72 [117]~E(x1171,x1172)+E(f59(x1173,x1171),f59(x1173,x1172))
% 0.55/0.72 [118]~E(x1181,x1182)+E(f56(x1181,x1183),f56(x1182,x1183))
% 0.55/0.72 [119]~E(x1191,x1192)+E(f56(x1193,x1191),f56(x1193,x1192))
% 0.55/0.72 [120]~E(x1201,x1202)+E(f55(x1201,x1203),f55(x1202,x1203))
% 0.55/0.72 [121]~E(x1211,x1212)+E(f55(x1213,x1211),f55(x1213,x1212))
% 0.55/0.72 [122]~E(x1221,x1222)+E(f69(x1221,x1223),f69(x1222,x1223))
% 0.55/0.72 [123]~E(x1231,x1232)+E(f69(x1233,x1231),f69(x1233,x1232))
% 0.55/0.72 [124]~E(x1241,x1242)+E(f71(x1241,x1243,x1244,x1245),f71(x1242,x1243,x1244,x1245))
% 0.55/0.72 [125]~E(x1251,x1252)+E(f71(x1253,x1251,x1254,x1255),f71(x1253,x1252,x1254,x1255))
% 0.55/0.72 [126]~E(x1261,x1262)+E(f71(x1263,x1264,x1261,x1265),f71(x1263,x1264,x1262,x1265))
% 0.55/0.72 [127]~E(x1271,x1272)+E(f71(x1273,x1274,x1275,x1271),f71(x1273,x1274,x1275,x1272))
% 0.55/0.72 [128]~E(x1281,x1282)+E(f76(x1281,x1283,x1284),f76(x1282,x1283,x1284))
% 0.55/0.72 [129]~E(x1291,x1292)+E(f76(x1293,x1291,x1294),f76(x1293,x1292,x1294))
% 0.55/0.72 [130]~E(x1301,x1302)+E(f76(x1303,x1304,x1301),f76(x1303,x1304,x1302))
% 0.55/0.72 [131]~E(x1311,x1312)+E(f89(x1311,x1313,x1314,x1315),f89(x1312,x1313,x1314,x1315))
% 0.55/0.72 [132]~E(x1321,x1322)+E(f89(x1323,x1321,x1324,x1325),f89(x1323,x1322,x1324,x1325))
% 0.55/0.72 [133]~E(x1331,x1332)+E(f89(x1333,x1334,x1331,x1335),f89(x1333,x1334,x1332,x1335))
% 0.55/0.72 [134]~E(x1341,x1342)+E(f89(x1343,x1344,x1345,x1341),f89(x1343,x1344,x1345,x1342))
% 0.55/0.72 [135]~E(x1351,x1352)+E(f57(x1351,x1353,x1354),f57(x1352,x1353,x1354))
% 0.55/0.72 [136]~E(x1361,x1362)+E(f57(x1363,x1361,x1364),f57(x1363,x1362,x1364))
% 0.55/0.72 [137]~E(x1371,x1372)+E(f57(x1373,x1374,x1371),f57(x1373,x1374,x1372))
% 0.55/0.72 [138]~E(x1381,x1382)+E(f41(x1381),f41(x1382))
% 0.55/0.72 [139]~E(x1391,x1392)+E(f66(x1391,x1393,x1394),f66(x1392,x1393,x1394))
% 0.55/0.72 [140]~E(x1401,x1402)+E(f66(x1403,x1401,x1404),f66(x1403,x1402,x1404))
% 0.55/0.72 [141]~E(x1411,x1412)+E(f66(x1413,x1414,x1411),f66(x1413,x1414,x1412))
% 0.55/0.72 [142]~E(x1421,x1422)+E(f74(x1421,x1423,x1424,x1425,x1426),f74(x1422,x1423,x1424,x1425,x1426))
% 0.55/0.72 [143]~E(x1431,x1432)+E(f74(x1433,x1431,x1434,x1435,x1436),f74(x1433,x1432,x1434,x1435,x1436))
% 0.55/0.72 [144]~E(x1441,x1442)+E(f74(x1443,x1444,x1441,x1445,x1446),f74(x1443,x1444,x1442,x1445,x1446))
% 0.55/0.72 [145]~E(x1451,x1452)+E(f74(x1453,x1454,x1455,x1451,x1456),f74(x1453,x1454,x1455,x1452,x1456))
% 0.55/0.72 [146]~E(x1461,x1462)+E(f74(x1463,x1464,x1465,x1466,x1461),f74(x1463,x1464,x1465,x1466,x1462))
% 0.55/0.72 [147]~E(x1471,x1472)+E(f68(x1471,x1473),f68(x1472,x1473))
% 0.55/0.72 [148]~E(x1481,x1482)+E(f68(x1483,x1481),f68(x1483,x1482))
% 0.55/0.72 [149]~P1(x1491)+P1(x1492)+~E(x1491,x1492)
% 0.55/0.72
% 0.55/0.72 %-------------------------------------------
% 0.55/0.72 cnf(320,plain,
% 0.55/0.72 ($false),
% 0.55/0.72 inference(scs_inference,[],[187,152]),
% 0.55/0.72 ['proof']).
% 0.55/0.72 % SZS output end Proof
% 0.55/0.72 % Total time :0.020000s
%------------------------------------------------------------------------------